%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SCT147+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sun Mar 6 14:28:28 EST 2011
% Result : Theorem 16.66s
% Output : CNFRefutation 16.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 13
% Syntax : Number of formulae : 87 ( 25 unt; 0 def)
% Number of atoms : 221 ( 14 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 228 ( 94 ~; 93 |; 27 &)
% ( 8 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 10 con; 0-4 aty)
% Number of variables : 228 ( 48 sgn 118 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(20,axiom,
! [X37] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X37)))
<=> hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X37))) ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_iff) ).
fof(33,axiom,
! [X11,X17,X18,X3] :
( hBOOL(hAPP(hAPP(c_member(X3),X18),c_Set_Oinsert(X3,X17,X11)))
<=> ( X18 = X17
| hBOOL(hAPP(hAPP(c_member(X3),X18),X11)) ) ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_insert__iff) ).
fof(47,axiom,
! [X4,X18,X3] : hBOOL(hAPP(hAPP(c_member(tc_prod(X3,X3)),hAPP(hAPP(c_Product__Type_OPair(X3,X3),X18),X18)),c_Transitive__Closure_Ortrancl(X3,X4))),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_rtrancl_Ortrancl__refl) ).
fof(122,axiom,
! [X18,X4,X3] : hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X3,X4),X18),X18)),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_rtranclp_Oequations_I1_J) ).
fof(133,axiom,
! [X11,X6,X3] :
( hBOOL(hAPP(hAPP(c_member(X3),X6),X11))
<=> hBOOL(hAPP(X11,X6)) ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_mem__def) ).
fof(268,axiom,
! [X18,X8,X3] : c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X8,c_Set_Oinsert(X3,X18,X8)),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_subset__insertI) ).
fof(330,axiom,
! [X37] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X37)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
<=> hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X37))) ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact__096ALL_Ai_O_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_J_Aa_Ac_092_060_094esub_062_Aa_J_A_061_A_Ia_A_060_092_060_094bsub_062P_Ai_092_060_094esub_062_Ab_J_096) ).
fof(355,axiom,
! [X11,X18,X3] :
( hBOOL(hAPP(hAPP(c_member(X3),X18),X11))
=> c_Set_Oinsert(X3,X18,X11) = X11 ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_insert__absorb) ).
fof(377,axiom,
! [X17,X18,X78] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X78),c_Arrow__Order__Mirabelle_OLin))
=> ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X18),X17)),X78))
=> ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X17),X18)),X78)) ) ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_Lin__irrefl) ).
fof(415,axiom,
class_Orderings_Oord(tc_HOL_Obool),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',arity_HOL__Obool__Orderings_Oord) ).
fof(478,axiom,
! [X36,X9,X3,X10] :
( class_Orderings_Oord(X10)
=> ( c_Orderings_Oord__class_Oless__eq(tc_fun(X3,X10),X9,X36)
<=> ! [X12] : c_Orderings_Oord__class_Oless__eq(X10,hAPP(X9,X12),hAPP(X36,X12)) ) ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_le__fun__def) ).
fof(489,axiom,
! [X8,X11,X6,X3] :
( c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),c_Set_Oinsert(X3,X6,X11),X8)
<=> ( hBOOL(hAPP(hAPP(c_member(X3),X6),X8))
& c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X11,X8) ) ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',fact_insert__subset) ).
fof(501,conjecture,
! [X37] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X37)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
<=> hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X37))) ),
file('/tmp/tmp26zDYE/sel_SCT147+1.p_1',conj_0) ).
fof(525,negated_conjecture,
~ ! [X37] :
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X37)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
<=> hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X37))) ),
inference(assume_negation,[status(cth)],[501]) ).
fof(579,plain,
! [X17,X18,X78] :
( hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X78),c_Arrow__Order__Mirabelle_OLin))
=> ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X18),X17)),X78))
=> ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X17),X18)),X78)) ) ),
inference(fof_simplification,[status(thm)],[377,theory(equality)]) ).
fof(684,plain,
! [X37] :
( ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X37)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X37))) )
& ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X37)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X37))) ) ),
inference(fof_nnf,[status(thm)],[20]) ).
fof(685,plain,
! [X38] :
( ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X38)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X38))) )
& ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X38)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X38))) ) ),
inference(variable_rename,[status(thm)],[684]) ).
cnf(686,plain,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X1)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X1))) ),
inference(split_conjunct,[status(thm)],[685]) ).
cnf(687,plain,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X1)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X1))) ),
inference(split_conjunct,[status(thm)],[685]) ).
fof(736,plain,
! [X11,X17,X18,X3] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X3),X18),c_Set_Oinsert(X3,X17,X11)))
| X18 = X17
| hBOOL(hAPP(hAPP(c_member(X3),X18),X11)) )
& ( ( X18 != X17
& ~ hBOOL(hAPP(hAPP(c_member(X3),X18),X11)) )
| hBOOL(hAPP(hAPP(c_member(X3),X18),c_Set_Oinsert(X3,X17,X11))) ) ),
inference(fof_nnf,[status(thm)],[33]) ).
fof(737,plain,
! [X19,X20,X21,X22] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X22),X21),c_Set_Oinsert(X22,X20,X19)))
| X21 = X20
| hBOOL(hAPP(hAPP(c_member(X22),X21),X19)) )
& ( ( X21 != X20
& ~ hBOOL(hAPP(hAPP(c_member(X22),X21),X19)) )
| hBOOL(hAPP(hAPP(c_member(X22),X21),c_Set_Oinsert(X22,X20,X19))) ) ),
inference(variable_rename,[status(thm)],[736]) ).
fof(738,plain,
! [X19,X20,X21,X22] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X22),X21),c_Set_Oinsert(X22,X20,X19)))
| X21 = X20
| hBOOL(hAPP(hAPP(c_member(X22),X21),X19)) )
& ( X21 != X20
| hBOOL(hAPP(hAPP(c_member(X22),X21),c_Set_Oinsert(X22,X20,X19))) )
& ( ~ hBOOL(hAPP(hAPP(c_member(X22),X21),X19))
| hBOOL(hAPP(hAPP(c_member(X22),X21),c_Set_Oinsert(X22,X20,X19))) ) ),
inference(distribute,[status(thm)],[737]) ).
cnf(741,plain,
( hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| X2 = X4
| ~ hBOOL(hAPP(hAPP(c_member(X1),X2),c_Set_Oinsert(X1,X4,X3))) ),
inference(split_conjunct,[status(thm)],[738]) ).
fof(784,plain,
! [X19,X20,X21] : hBOOL(hAPP(hAPP(c_member(tc_prod(X21,X21)),hAPP(hAPP(c_Product__Type_OPair(X21,X21),X20),X20)),c_Transitive__Closure_Ortrancl(X21,X19))),
inference(variable_rename,[status(thm)],[47]) ).
cnf(785,plain,
hBOOL(hAPP(hAPP(c_member(tc_prod(X1,X1)),hAPP(hAPP(c_Product__Type_OPair(X1,X1),X2),X2)),c_Transitive__Closure_Ortrancl(X1,X3))),
inference(split_conjunct,[status(thm)],[784]) ).
fof(1053,plain,
! [X19,X20,X21] : hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X21,X20),X19),X19)),
inference(variable_rename,[status(thm)],[122]) ).
cnf(1054,plain,
hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(X1,X2),X3),X3)),
inference(split_conjunct,[status(thm)],[1053]) ).
fof(1082,plain,
! [X11,X6,X3] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X3),X6),X11))
| hBOOL(hAPP(X11,X6)) )
& ( ~ hBOOL(hAPP(X11,X6))
| hBOOL(hAPP(hAPP(c_member(X3),X6),X11)) ) ),
inference(fof_nnf,[status(thm)],[133]) ).
fof(1083,plain,
! [X12,X13,X14] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X14),X13),X12))
| hBOOL(hAPP(X12,X13)) )
& ( ~ hBOOL(hAPP(X12,X13))
| hBOOL(hAPP(hAPP(c_member(X14),X13),X12)) ) ),
inference(variable_rename,[status(thm)],[1082]) ).
cnf(1084,plain,
( hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| ~ hBOOL(hAPP(X3,X2)) ),
inference(split_conjunct,[status(thm)],[1083]) ).
cnf(1085,plain,
( hBOOL(hAPP(X1,X2))
| ~ hBOOL(hAPP(hAPP(c_member(X3),X2),X1)) ),
inference(split_conjunct,[status(thm)],[1083]) ).
fof(1581,plain,
! [X19,X20,X21] : c_Orderings_Oord__class_Oless__eq(tc_fun(X21,tc_HOL_Obool),X20,c_Set_Oinsert(X21,X19,X20)),
inference(variable_rename,[status(thm)],[268]) ).
cnf(1582,plain,
c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2,c_Set_Oinsert(X1,X3,X2)),
inference(split_conjunct,[status(thm)],[1581]) ).
fof(1797,plain,
! [X37] :
( ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X37)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X37))) )
& ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X37)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X37)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____))) ) ),
inference(fof_nnf,[status(thm)],[330]) ).
fof(1798,plain,
! [X38] :
( ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X38)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X38))) )
& ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X38)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X38)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____))) ) ),
inference(variable_rename,[status(thm)],[1797]) ).
cnf(1799,plain,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X1)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X1))) ),
inference(split_conjunct,[status(thm)],[1798]) ).
cnf(1800,plain,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,X1)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X1)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____))) ),
inference(split_conjunct,[status(thm)],[1798]) ).
fof(1882,plain,
! [X11,X18,X3] :
( ~ hBOOL(hAPP(hAPP(c_member(X3),X18),X11))
| c_Set_Oinsert(X3,X18,X11) = X11 ),
inference(fof_nnf,[status(thm)],[355]) ).
fof(1883,plain,
! [X19,X20,X21] :
( ~ hBOOL(hAPP(hAPP(c_member(X21),X20),X19))
| c_Set_Oinsert(X21,X20,X19) = X19 ),
inference(variable_rename,[status(thm)],[1882]) ).
cnf(1884,plain,
( c_Set_Oinsert(X1,X2,X3) = X3
| ~ hBOOL(hAPP(hAPP(c_member(X1),X2),X3)) ),
inference(split_conjunct,[status(thm)],[1883]) ).
fof(1976,plain,
! [X17,X18,X78] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X78),c_Arrow__Order__Mirabelle_OLin))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X18),X17)),X78))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X17),X18)),X78)) ),
inference(fof_nnf,[status(thm)],[579]) ).
fof(1977,plain,
! [X79,X80,X81] :
( ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X81),c_Arrow__Order__Mirabelle_OLin))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X80),X79)),X81))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X79),X80)),X81)) ),
inference(variable_rename,[status(thm)],[1976]) ).
cnf(1978,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X2)),X3))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2),X1)),X3))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),X3),c_Arrow__Order__Mirabelle_OLin)) ),
inference(split_conjunct,[status(thm)],[1977]) ).
cnf(2102,plain,
class_Orderings_Oord(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[415]) ).
fof(2332,plain,
! [X36,X9,X3,X10] :
( ~ class_Orderings_Oord(X10)
| ( ( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X3,X10),X9,X36)
| ! [X12] : c_Orderings_Oord__class_Oless__eq(X10,hAPP(X9,X12),hAPP(X36,X12)) )
& ( ? [X12] : ~ c_Orderings_Oord__class_Oless__eq(X10,hAPP(X9,X12),hAPP(X36,X12))
| c_Orderings_Oord__class_Oless__eq(tc_fun(X3,X10),X9,X36) ) ) ),
inference(fof_nnf,[status(thm)],[478]) ).
fof(2333,plain,
! [X37,X38,X39,X40] :
( ~ class_Orderings_Oord(X40)
| ( ( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X39,X40),X38,X37)
| ! [X41] : c_Orderings_Oord__class_Oless__eq(X40,hAPP(X38,X41),hAPP(X37,X41)) )
& ( ? [X42] : ~ c_Orderings_Oord__class_Oless__eq(X40,hAPP(X38,X42),hAPP(X37,X42))
| c_Orderings_Oord__class_Oless__eq(tc_fun(X39,X40),X38,X37) ) ) ),
inference(variable_rename,[status(thm)],[2332]) ).
fof(2334,plain,
! [X37,X38,X39,X40] :
( ~ class_Orderings_Oord(X40)
| ( ( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X39,X40),X38,X37)
| ! [X41] : c_Orderings_Oord__class_Oless__eq(X40,hAPP(X38,X41),hAPP(X37,X41)) )
& ( ~ c_Orderings_Oord__class_Oless__eq(X40,hAPP(X38,esk93_4(X37,X38,X39,X40)),hAPP(X37,esk93_4(X37,X38,X39,X40)))
| c_Orderings_Oord__class_Oless__eq(tc_fun(X39,X40),X38,X37) ) ) ),
inference(skolemize,[status(esa)],[2333]) ).
fof(2335,plain,
! [X37,X38,X39,X40,X41] :
( ( ( c_Orderings_Oord__class_Oless__eq(X40,hAPP(X38,X41),hAPP(X37,X41))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X39,X40),X38,X37) )
& ( ~ c_Orderings_Oord__class_Oless__eq(X40,hAPP(X38,esk93_4(X37,X38,X39,X40)),hAPP(X37,esk93_4(X37,X38,X39,X40)))
| c_Orderings_Oord__class_Oless__eq(tc_fun(X39,X40),X38,X37) ) )
| ~ class_Orderings_Oord(X40) ),
inference(shift_quantors,[status(thm)],[2334]) ).
fof(2336,plain,
! [X37,X38,X39,X40,X41] :
( ( c_Orderings_Oord__class_Oless__eq(X40,hAPP(X38,X41),hAPP(X37,X41))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X39,X40),X38,X37)
| ~ class_Orderings_Oord(X40) )
& ( ~ c_Orderings_Oord__class_Oless__eq(X40,hAPP(X38,esk93_4(X37,X38,X39,X40)),hAPP(X37,esk93_4(X37,X38,X39,X40)))
| c_Orderings_Oord__class_Oless__eq(tc_fun(X39,X40),X38,X37)
| ~ class_Orderings_Oord(X40) ) ),
inference(distribute,[status(thm)],[2335]) ).
cnf(2337,plain,
( c_Orderings_Oord__class_Oless__eq(tc_fun(X2,X1),X3,X4)
| ~ class_Orderings_Oord(X1)
| ~ c_Orderings_Oord__class_Oless__eq(X1,hAPP(X3,esk93_4(X4,X3,X2,X1)),hAPP(X4,esk93_4(X4,X3,X2,X1))) ),
inference(split_conjunct,[status(thm)],[2336]) ).
cnf(2338,plain,
( c_Orderings_Oord__class_Oless__eq(X1,hAPP(X3,X5),hAPP(X4,X5))
| ~ class_Orderings_Oord(X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X2,X1),X3,X4) ),
inference(split_conjunct,[status(thm)],[2336]) ).
fof(2377,plain,
! [X8,X11,X6,X3] :
( ( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),c_Set_Oinsert(X3,X6,X11),X8)
| ( hBOOL(hAPP(hAPP(c_member(X3),X6),X8))
& c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X11,X8) ) )
& ( ~ hBOOL(hAPP(hAPP(c_member(X3),X6),X8))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X11,X8)
| c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),c_Set_Oinsert(X3,X6,X11),X8) ) ),
inference(fof_nnf,[status(thm)],[489]) ).
fof(2378,plain,
! [X12,X13,X14,X15] :
( ( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),c_Set_Oinsert(X15,X14,X13),X12)
| ( hBOOL(hAPP(hAPP(c_member(X15),X14),X12))
& c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),X13,X12) ) )
& ( ~ hBOOL(hAPP(hAPP(c_member(X15),X14),X12))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),X13,X12)
| c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),c_Set_Oinsert(X15,X14,X13),X12) ) ),
inference(variable_rename,[status(thm)],[2377]) ).
fof(2379,plain,
! [X12,X13,X14,X15] :
( ( hBOOL(hAPP(hAPP(c_member(X15),X14),X12))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),c_Set_Oinsert(X15,X14,X13),X12) )
& ( c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),X13,X12)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),c_Set_Oinsert(X15,X14,X13),X12) )
& ( ~ hBOOL(hAPP(hAPP(c_member(X15),X14),X12))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),X13,X12)
| c_Orderings_Oord__class_Oless__eq(tc_fun(X15,tc_HOL_Obool),c_Set_Oinsert(X15,X14,X13),X12) ) ),
inference(distribute,[status(thm)],[2378]) ).
cnf(2382,plain,
( hBOOL(hAPP(hAPP(c_member(X1),X2),X4))
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),c_Set_Oinsert(X1,X2,X3),X4) ),
inference(split_conjunct,[status(thm)],[2379]) ).
fof(2426,negated_conjecture,
? [X37] :
( ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X37)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X37))) )
& ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X37)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X37))) ) ),
inference(fof_nnf,[status(thm)],[525]) ).
fof(2427,negated_conjecture,
? [X38] :
( ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X38)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X38))) )
& ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,X38)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,X38))) ) ),
inference(variable_rename,[status(thm)],[2426]) ).
fof(2428,negated_conjecture,
( ( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,esk97_0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,esk97_0))) )
& ( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,esk97_0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,esk97_0))) ) ),
inference(skolemize,[status(esa)],[2427]) ).
cnf(2429,negated_conjecture,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,esk97_0)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,esk97_0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____))) ),
inference(split_conjunct,[status(thm)],[2428]) ).
cnf(2430,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,esk97_0)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,esk97_0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____))) ),
inference(split_conjunct,[status(thm)],[2428]) ).
cnf(3144,plain,
( X1 = X2
| hBOOL(hAPP(hAPP(c_member(X3),X1),X4))
| ~ hBOOL(hAPP(c_Set_Oinsert(X3,X2,X4),X1)) ),
inference(spm,[status(thm)],[741,1084,theory(equality)]) ).
cnf(3537,plain,
( c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2),hAPP(c_Set_Oinsert(X3,X4,X1),X2))
| ~ class_Orderings_Oord(tc_HOL_Obool) ),
inference(spm,[status(thm)],[2338,1582,theory(equality)]) ).
cnf(3542,plain,
( c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2),hAPP(c_Set_Oinsert(X3,X4,X1),X2))
| $false ),
inference(rw,[status(thm)],[3537,2102,theory(equality)]) ).
cnf(3543,plain,
c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2),hAPP(c_Set_Oinsert(X3,X4,X1),X2)),
inference(cn,[status(thm)],[3542,theory(equality)]) ).
cnf(6929,negated_conjecture,
( hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,esk97_0)))
| hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,esk97_0))) ),
inference(spm,[status(thm)],[1800,2429,theory(equality)]) ).
cnf(8453,plain,
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X1),X1)),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,X2)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,X2)),c_Arrow__Order__Mirabelle_OLin)) ),
inference(spm,[status(thm)],[1978,785,theory(equality)]) ).
cnf(8508,plain,
( $false
| ~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,X2)),c_Arrow__Order__Mirabelle_OLin)) ),
inference(rw,[status(thm)],[8453,785,theory(equality)]) ).
cnf(8509,plain,
~ hBOOL(hAPP(hAPP(c_member(tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_HOL_Obool)),c_Transitive__Closure_Ortrancl(tc_Arrow__Order__Mirabelle_Oalt,X2)),c_Arrow__Order__Mirabelle_OLin)),
inference(cn,[status(thm)],[8508,theory(equality)]) ).
cnf(42082,plain,
( c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2,c_Set_Oinsert(X3,X4,X2))
| ~ class_Orderings_Oord(tc_HOL_Obool) ),
inference(spm,[status(thm)],[2337,3543,theory(equality)]) ).
cnf(42110,plain,
( c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2,c_Set_Oinsert(X3,X4,X2))
| $false ),
inference(rw,[status(thm)],[42082,2102,theory(equality)]) ).
cnf(42111,plain,
c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2,c_Set_Oinsert(X3,X4,X2)),
inference(cn,[status(thm)],[42110,theory(equality)]) ).
cnf(51461,plain,
hBOOL(hAPP(hAPP(c_member(X1),X2),c_Set_Oinsert(X3,X4,c_Set_Oinsert(X1,X2,X5)))),
inference(spm,[status(thm)],[2382,42111,theory(equality)]) ).
cnf(52913,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,c_Set_Oinsert(X3,X4,X5)),X4)),
inference(spm,[status(thm)],[1085,51461,theory(equality)]) ).
cnf(118344,plain,
( X1 = X2
| hBOOL(hAPP(hAPP(c_member(X3),X1),c_Set_Oinsert(X4,X1,X5))) ),
inference(spm,[status(thm)],[3144,52913,theory(equality)]) ).
cnf(118426,plain,
( hBOOL(X4)
| hBOOL(hAPP(hAPP(c_member(X5),X4),c_Set_Oinsert(X6,X4,X7))) ),
inference(spm,[status(thm)],[1054,118344,theory(equality)]) ).
cnf(121336,plain,
( hBOOL(hAPP(hAPP(c_member(X3),X2),c_Set_Oinsert(X4,X2,X5)))
| ~ hBOOL(X2) ),
inference(spm,[status(thm)],[8509,118344,theory(equality)]) ).
cnf(144908,plain,
hBOOL(hAPP(hAPP(c_member(X5),X4),c_Set_Oinsert(X6,X4,X7))),
inference(csr,[status(thm)],[118426,121336]) ).
cnf(144918,plain,
( hBOOL(hAPP(hAPP(c_member(X1),X2),X4))
| ~ hBOOL(hAPP(hAPP(c_member(X3),X2),X4)) ),
inference(spm,[status(thm)],[144908,1884,theory(equality)]) ).
cnf(212207,negated_conjecture,
hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,esk97_0))),
inference(csr,[status(thm)],[6929,686]) ).
cnf(212252,negated_conjecture,
hBOOL(hAPP(hAPP(c_member(X1),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,esk97_0))),
inference(spm,[status(thm)],[144918,212207,theory(equality)]) ).
cnf(212421,negated_conjecture,
hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(v_P_H____,esk97_0))),
inference(spm,[status(thm)],[687,212252,theory(equality)]) ).
cnf(213199,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,esk97_0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____)))
| $false ),
inference(rw,[status(thm)],[2430,212421,theory(equality)]) ).
cnf(213200,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_b____),v_a____)),hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(hAPP(hAPP(c_Arrow__Order__Mirabelle_Obelow,hAPP(v_P____,esk97_0)),v_c____),v_b____)),v_b____),v_a____)),v_a____),v_c____))),
inference(cn,[status(thm)],[213199,theory(equality)]) ).
cnf(213252,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),hAPP(hAPP(c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_a____),v_b____)),hAPP(v_P____,esk97_0))),
inference(spm,[status(thm)],[213200,1799,theory(equality)]) ).
cnf(213306,negated_conjecture,
$false,
inference(rw,[status(thm)],[213252,212252,theory(equality)]) ).
cnf(213307,negated_conjecture,
$false,
inference(cn,[status(thm)],[213306,theory(equality)]) ).
cnf(213308,negated_conjecture,
$false,
213307,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWW/SCT147+1.p
% --creating new selector for []
% -running prover on /tmp/tmp26zDYE/sel_SCT147+1.p_1 with time limit 29
% -prover status Theorem
% Problem SCT147+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWW/SCT147+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWW/SCT147+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------