%------------------------------------------------------------------------------
% File     : COL002-0 : TPTP v7.2.0. Released v3.2.0.
% Domain   : Combinatory Logic
% Axioms   : Combinators
% Version  : [Pau06] axioms.
% English  :

% Refs     : [Pau06] Paulson (2006), Email to G. Sutcliffe
% Source   : [Pau06]
% Names    : Comb.ax [Pau06]

% Status   : Satisfiable
% Syntax   : Number of clauses     :   25 (   8 non-Horn;  11 unit;  21 RR)
%            Number of atoms       :   63 (  35 equality)
%            Maximal clause size   :    5 (   3 average)
%            Number of predicates  :    2 (   0 propositional; 2-3 arity)
%            Number of functors    :   13 (   5 constant; 0-4 arity)
%            Number of variables   :   58 (  16 singleton)
%            Maximal term depth    :    5 (   2 average)
% SPC      : 

% Comments : Requires MSC001-0.ax, MSC001-2.ax
%------------------------------------------------------------------------------
cnf(cls_Comb_OAp__contractE_0,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_r = c_Comb_Ocomb_Oop_A_D_D(V_p,v_sko__uR_H(V_p,V_q,V_r))
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uR8(V_p,V_q,V_r)),v_sko__uR9(V_p,V_q,V_r))
    | V_r = c_Comb_Ocomb_Oop_A_D_D(v_sko__uR__(V_p,V_q,V_r),V_q) )).

cnf(cls_Comb_OAp__contractE_1,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_q,v_sko__uR_H(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uR8(V_p,V_q,V_r)),v_sko__uR9(V_p,V_q,V_r))
    | V_r = c_Comb_Ocomb_Oop_A_D_D(v_sko__uR__(V_p,V_q,V_r),V_q) )).

cnf(cls_Comb_OAp__contractE_2,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_p,v_sko__uR__(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_r = c_Comb_Ocomb_Oop_A_D_D(V_p,v_sko__uR_H(V_p,V_q,V_r))
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uR8(V_p,V_q,V_r)),v_sko__uR9(V_p,V_q,V_r)) )).

cnf(cls_Comb_OAp__contractE_3,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_q,v_sko__uR_H(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_p,v_sko__uR__(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uR8(V_p,V_q,V_r)),v_sko__uR9(V_p,V_q,V_r)) )).

cnf(cls_Comb_OAp__contractE_4,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_r = c_Comb_Ocomb_Oop_A_D_D(V_p,v_sko__uR_H(V_p,V_q,V_r))
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)
    | V_r = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uR8(V_p,V_q,V_r),V_q),c_Comb_Ocomb_Oop_A_D_D(v_sko__uR9(V_p,V_q,V_r),V_q))
    | V_r = c_Comb_Ocomb_Oop_A_D_D(v_sko__uR__(V_p,V_q,V_r),V_q) )).

cnf(cls_Comb_OAp__contractE_5,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_q,v_sko__uR_H(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)
    | V_r = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uR8(V_p,V_q,V_r),V_q),c_Comb_Ocomb_Oop_A_D_D(v_sko__uR9(V_p,V_q,V_r),V_q))
    | V_r = c_Comb_Ocomb_Oop_A_D_D(v_sko__uR__(V_p,V_q,V_r),V_q) )).

cnf(cls_Comb_OAp__contractE_6,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_p,v_sko__uR__(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_r = c_Comb_Ocomb_Oop_A_D_D(V_p,v_sko__uR_H(V_p,V_q,V_r))
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)
    | V_r = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uR8(V_p,V_q,V_r),V_q),c_Comb_Ocomb_Oop_A_D_D(v_sko__uR9(V_p,V_q,V_r),V_q)) )).

cnf(cls_Comb_OAp__contractE_7,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_q,v_sko__uR_H(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_p,v_sko__uR__(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)
    | V_r = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(v_sko__uR8(V_p,V_q,V_r),V_q),c_Comb_Ocomb_Oop_A_D_D(v_sko__uR9(V_p,V_q,V_r),V_q)) )).

cnf(cls_Comb_OI__contract__E_0,axiom,
    ( ~ c_in(c_Pair(c_Comb_OI,V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )).

cnf(cls_Comb_OK1__contractD_0,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x),V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | V_z = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uR7(V_x,V_z)) )).

cnf(cls_Comb_OK1__contractD_1,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x),V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(V_x,v_sko__uR7(V_x,V_z),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )).

cnf(cls_Comb_OK__contractE_0,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_OK,V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )).

cnf(cls_Comb_OS__contractE_0,axiom,
    ( ~ c_in(c_Pair(c_Comb_Ocomb_OS,V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )).

cnf(cls_Comb_Ocomb_Odistinct__1__iff1_0,axiom,
    ( c_Comb_Ocomb_OK != c_Comb_Ocomb_OS )).

cnf(cls_Comb_Ocomb_Odistinct__2__iff1_0,axiom,
    ( c_Comb_Ocomb_OS != c_Comb_Ocomb_OK )).

cnf(cls_Comb_Ocomb_Odistinct__3__iff1_0,axiom,
    ( c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) )).

cnf(cls_Comb_Ocomb_Odistinct__4__iff1_0,axiom,
    ( c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OK )).

cnf(cls_Comb_Ocomb_Odistinct__5__iff1_0,axiom,
    ( c_Comb_Ocomb_OS != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) )).

cnf(cls_Comb_Ocomb_Odistinct__6__iff1_0,axiom,
    ( c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OS )).

cnf(cls_Comb_Ocomb_Oinject__iff1_0,axiom,
    ( c_Comb_Ocomb_Oop_A_D_D(V_comb1,V_comb2) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H)
    | V_comb1 = V_comb1_H )).

cnf(cls_Comb_Ocomb_Oinject__iff1_1,axiom,
    ( c_Comb_Ocomb_Oop_A_D_D(V_comb1,V_comb2) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H)
    | V_comb2 = V_comb2_H )).

cnf(cls_Comb_Ocontract_OAp1_0,axiom,
    ( ~ c_in(c_Pair(V_x,V_y,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_x,V_z),c_Comb_Ocomb_Oop_A_D_D(V_y,V_z),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )).

cnf(cls_Comb_Ocontract_OAp2_0,axiom,
    ( ~ c_in(c_Pair(V_x,V_y,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
    | c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_z,V_x),c_Comb_Ocomb_Oop_A_D_D(V_z,V_y),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )).

cnf(cls_Comb_Ocontract_OK_0,axiom,
    ( c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x),V_y),V_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )).

cnf(cls_Comb_Ocontract_OS_0,axiom,
    ( c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,V_x),V_y),V_z),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(V_x,V_z),c_Comb_Ocomb_Oop_A_D_D(V_y,V_z)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) )).

%------------------------------------------------------------------------------