%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SCT161+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Mon Mar 7 00:33:36 EST 2011
% Result : Theorem 44.45s
% Output : Solution 44.45s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP10840/SCT161+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% WARNING: TreeLimitedRun lost 0.21s, total lost is 0.21s
% found
% SZS status THM for /tmp/SystemOnTPTP10840/SCT161+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP10840/SCT161+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 11024
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.95 CPU 2.03 WC
% PrfWatch: 3.94 CPU 4.03 WC
% PrfWatch: 5.94 CPU 6.04 WC
% PrfWatch: 7.92 CPU 8.05 WC
% PrfWatch: 9.92 CPU 10.05 WC
% PrfWatch: 11.91 CPU 12.06 WC
% PrfWatch: 13.91 CPU 14.07 WC
% PrfWatch: 15.89 CPU 16.07 WC
% PrfWatch: 17.89 CPU 18.08 WC
% PrfWatch: 19.89 CPU 20.09 WC
% # Preprocessing time : 0.116 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 21.88 CPU 22.09 WC
% PrfWatch: 23.87 CPU 24.10 WC
% PrfWatch: 25.87 CPU 26.11 WC
% PrfWatch: 27.86 CPU 28.11 WC
% PrfWatch: 29.69 CPU 30.12 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,![X4]:![X5]:hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)),X4)),file('/tmp/SRASS.s.p', fact_top1I)).
% fof(16, axiom,![X17]:![X5]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool),X17),c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)))),file('/tmp/SRASS.s.p', fact_subset__UNIV)).
% fof(20, axiom,c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))),file('/tmp/SRASS.s.p', fact_finite__indi)).
% fof(61, axiom,![X4]:![X20]:![X5]:(class_Orderings_Otop(X5)=>hAPP(c_Orderings_Otop__class_Otop(tc_fun(X20,X5)),X4)=c_Orderings_Otop__class_Otop(X5)),file('/tmp/SRASS.s.p', fact_top__apply)).
% fof(98, axiom,![X19]:![X4]:![X5]:(class_Orderings_Olinorder(X5)=>(~(X4=X19)<=>(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X5),X4),X19))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X5),X19),X4))))),file('/tmp/SRASS.s.p', fact_linorder__neq__iff)).
% fof(155, axiom,![X5]:(c_Finite__Set_Ofinite(tc_Option_Ooption(X5),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X5),tc_HOL_Obool)))<=>c_Finite__Set_Ofinite(X5,c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)))),file('/tmp/SRASS.s.p', fact_finite__option__UNIV)).
% fof(160, axiom,![X16]:![X17]:![X5]:(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool),X17),X16))=>(c_Finite__Set_Ofinite(X5,X16)=>c_Finite__Set_Ofinite(X5,X17))),file('/tmp/SRASS.s.p', fact_finite__subset)).
% fof(171, axiom,![X43]:(c_Finite__Set_Ofinite(tc_Nat_Onat,X43)<=>?[X36]:![X3]:(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X3),X43))=>hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X3),X36)))),file('/tmp/SRASS.s.p', fact_finite__nat__set__iff__bounded)).
% fof(207, axiom,![X17]:![X4]:![X5]:(hBOOL(hAPP(hAPP(c_member(X5),X4),X17))<=>hBOOL(hAPP(X17,X4))),file('/tmp/SRASS.s.p', fact_mem__def)).
% fof(246, axiom,class_Orderings_Oorder(tc_HOL_Obool),file('/tmp/SRASS.s.p', arity_HOL__Obool__Orderings_Oorder)).
% fof(247, axiom,![X53]:![X5]:hAPP(c_COMBI(X5),X53)=X53,file('/tmp/SRASS.s.p', help_c__COMBI__1)).
% fof(248, axiom,![X54]:![X53]:![X20]:![X5]:hAPP(hAPP(c_COMBK(X5,X20),X53),X54)=X53,file('/tmp/SRASS.s.p', help_c__COMBK__1)).
% fof(264, axiom,class_Orderings_Olinorder(tc_Nat_Onat),file('/tmp/SRASS.s.p', arity_Nat__Onat__Orderings_Olinorder)).
% fof(267, axiom,class_Orderings_Otop(tc_HOL_Obool),file('/tmp/SRASS.s.p', arity_HOL__Obool__Orderings_Otop)).
% fof(268, axiom,class_Orderings_Oord(tc_HOL_Obool),file('/tmp/SRASS.s.p', arity_HOL__Obool__Orderings_Oord)).
% fof(309, axiom,![X4]:![X19]:![X5]:(class_Orderings_Oorder(X5)=>(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X19),X4))=>(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X4),X19))<=>X4=X19))),file('/tmp/SRASS.s.p', fact_order__antisym__conv)).
% fof(363, axiom,![X17]:![X2]:![X20]:![X5]:(c_Finite__Set_Ofinite(X5,c_Set_Oimage(X20,X5,X2,X17))=>(c_Fun_Oinj__on(X20,X5,X2,X17)=>c_Finite__Set_Ofinite(X20,X17))),file('/tmp/SRASS.s.p', fact_finite__imageD)).
% fof(382, axiom,![X17]:![X2]:![X20]:![X5]:(c_Fun_Oinj__on(X5,X20,X2,X17)<=>![X3]:(hBOOL(hAPP(hAPP(c_member(X5),X3),X17))=>![X61]:(hBOOL(hAPP(hAPP(c_member(X5),X61),X17))=>(hAPP(X2,X3)=hAPP(X2,X61)=>X3=X61)))),file('/tmp/SRASS.s.p', fact_inj__on__def)).
% fof(392, axiom,![X1]:![X2]:![X5]:![X20]:(class_Orderings_Oord(X20)=>(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,X20),X2),X1))<=>![X3]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X20,hAPP(X2,X3)),hAPP(X1,X3))))),file('/tmp/SRASS.s.p', fact_le__fun__def)).
% fof(606, plain,![X6]:![X7]:hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X7,tc_HOL_Obool)),X6)),inference(variable_rename,[status(thm)],[2])).
% cnf(607,plain,(hBOOL(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)),X2))),inference(split_conjunct,[status(thm)],[606])).
% fof(660, plain,![X18]:![X19]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X19,tc_HOL_Obool),X18),c_Orderings_Otop__class_Otop(tc_fun(X19,tc_HOL_Obool)))),inference(variable_rename,[status(thm)],[16])).
% cnf(661,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))))),inference(split_conjunct,[status(thm)],[660])).
% cnf(671,plain,(c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool)))),inference(split_conjunct,[status(thm)],[20])).
% fof(806, plain,![X4]:![X20]:![X5]:(~(class_Orderings_Otop(X5))|hAPP(c_Orderings_Otop__class_Otop(tc_fun(X20,X5)),X4)=c_Orderings_Otop__class_Otop(X5)),inference(fof_nnf,[status(thm)],[61])).
% fof(807, plain,![X21]:![X22]:![X23]:(~(class_Orderings_Otop(X23))|hAPP(c_Orderings_Otop__class_Otop(tc_fun(X22,X23)),X21)=c_Orderings_Otop__class_Otop(X23)),inference(variable_rename,[status(thm)],[806])).
% cnf(808,plain,(hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,X2)),X3)=c_Orderings_Otop__class_Otop(X2)|~class_Orderings_Otop(X2)),inference(split_conjunct,[status(thm)],[807])).
% fof(915, plain,![X19]:![X4]:![X5]:(~(class_Orderings_Olinorder(X5))|((X4=X19|(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X5),X4),X19))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X5),X19),X4))))&((~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X5),X4),X19)))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X5),X19),X4))))|~(X4=X19)))),inference(fof_nnf,[status(thm)],[98])).
% fof(916, plain,![X20]:![X21]:![X22]:(~(class_Orderings_Olinorder(X22))|((X21=X20|(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X22),X21),X20))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X22),X20),X21))))&((~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X22),X21),X20)))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X22),X20),X21))))|~(X21=X20)))),inference(variable_rename,[status(thm)],[915])).
% fof(917, plain,![X20]:![X21]:![X22]:(((X21=X20|(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X22),X21),X20))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X22),X20),X21))))|~(class_Orderings_Olinorder(X22)))&(((~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X22),X21),X20)))|~(X21=X20))|~(class_Orderings_Olinorder(X22)))&((~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X22),X20),X21)))|~(X21=X20))|~(class_Orderings_Olinorder(X22))))),inference(distribute,[status(thm)],[916])).
% cnf(918,plain,(~class_Orderings_Olinorder(X1)|X2!=X3|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X1),X3),X2))),inference(split_conjunct,[status(thm)],[917])).
% fof(1134, plain,![X5]:((~(c_Finite__Set_Ofinite(tc_Option_Ooption(X5),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X5),tc_HOL_Obool))))|c_Finite__Set_Ofinite(X5,c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool))))&(~(c_Finite__Set_Ofinite(X5,c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool))))|c_Finite__Set_Ofinite(tc_Option_Ooption(X5),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X5),tc_HOL_Obool))))),inference(fof_nnf,[status(thm)],[155])).
% fof(1135, plain,![X6]:((~(c_Finite__Set_Ofinite(tc_Option_Ooption(X6),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X6),tc_HOL_Obool))))|c_Finite__Set_Ofinite(X6,c_Orderings_Otop__class_Otop(tc_fun(X6,tc_HOL_Obool))))&(~(c_Finite__Set_Ofinite(X6,c_Orderings_Otop__class_Otop(tc_fun(X6,tc_HOL_Obool))))|c_Finite__Set_Ofinite(tc_Option_Ooption(X6),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X6),tc_HOL_Obool))))),inference(variable_rename,[status(thm)],[1134])).
% cnf(1136,plain,(c_Finite__Set_Ofinite(tc_Option_Ooption(X1),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X1),tc_HOL_Obool)))|~c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),inference(split_conjunct,[status(thm)],[1135])).
% fof(1150, plain,![X16]:![X17]:![X5]:(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool),X17),X16)))|(~(c_Finite__Set_Ofinite(X5,X16))|c_Finite__Set_Ofinite(X5,X17))),inference(fof_nnf,[status(thm)],[160])).
% fof(1151, plain,![X18]:![X19]:![X20]:(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X20,tc_HOL_Obool),X19),X18)))|(~(c_Finite__Set_Ofinite(X20,X18))|c_Finite__Set_Ofinite(X20,X19))),inference(variable_rename,[status(thm)],[1150])).
% cnf(1152,plain,(c_Finite__Set_Ofinite(X1,X2)|~c_Finite__Set_Ofinite(X1,X3)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2),X3))),inference(split_conjunct,[status(thm)],[1151])).
% fof(1186, plain,![X43]:((~(c_Finite__Set_Ofinite(tc_Nat_Onat,X43))|?[X36]:![X3]:(~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X3),X43)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X3),X36))))&(![X36]:?[X3]:(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X3),X43))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X3),X36))))|c_Finite__Set_Ofinite(tc_Nat_Onat,X43))),inference(fof_nnf,[status(thm)],[171])).
% fof(1187, plain,![X44]:((~(c_Finite__Set_Ofinite(tc_Nat_Onat,X44))|?[X45]:![X46]:(~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X46),X44)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X46),X45))))&(![X47]:?[X48]:(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X48),X44))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X48),X47))))|c_Finite__Set_Ofinite(tc_Nat_Onat,X44))),inference(variable_rename,[status(thm)],[1186])).
% fof(1188, plain,![X44]:((~(c_Finite__Set_Ofinite(tc_Nat_Onat,X44))|![X46]:(~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X46),X44)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X46),esk11_1(X44)))))&(![X47]:(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk12_2(X44,X47)),X44))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),esk12_2(X44,X47)),X47))))|c_Finite__Set_Ofinite(tc_Nat_Onat,X44))),inference(skolemize,[status(esa)],[1187])).
% fof(1189, plain,![X44]:![X46]:![X47]:(((hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk12_2(X44,X47)),X44))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),esk12_2(X44,X47)),X47))))|c_Finite__Set_Ofinite(tc_Nat_Onat,X44))&((~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X46),X44)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X46),esk11_1(X44))))|~(c_Finite__Set_Ofinite(tc_Nat_Onat,X44)))),inference(shift_quantors,[status(thm)],[1188])).
% fof(1190, plain,![X44]:![X46]:![X47]:(((hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk12_2(X44,X47)),X44))|c_Finite__Set_Ofinite(tc_Nat_Onat,X44))&(~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),esk12_2(X44,X47)),X47)))|c_Finite__Set_Ofinite(tc_Nat_Onat,X44)))&((~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X46),X44)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X46),esk11_1(X44))))|~(c_Finite__Set_Ofinite(tc_Nat_Onat,X44)))),inference(distribute,[status(thm)],[1189])).
% cnf(1191,plain,(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),esk11_1(X1)))|~c_Finite__Set_Ofinite(tc_Nat_Onat,X1)|~hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X2),X1))),inference(split_conjunct,[status(thm)],[1190])).
% fof(1323, plain,![X17]:![X4]:![X5]:((~(hBOOL(hAPP(hAPP(c_member(X5),X4),X17)))|hBOOL(hAPP(X17,X4)))&(~(hBOOL(hAPP(X17,X4)))|hBOOL(hAPP(hAPP(c_member(X5),X4),X17)))),inference(fof_nnf,[status(thm)],[207])).
% fof(1324, plain,![X18]:![X19]:![X20]:((~(hBOOL(hAPP(hAPP(c_member(X20),X19),X18)))|hBOOL(hAPP(X18,X19)))&(~(hBOOL(hAPP(X18,X19)))|hBOOL(hAPP(hAPP(c_member(X20),X19),X18)))),inference(variable_rename,[status(thm)],[1323])).
% cnf(1325,plain,(hBOOL(hAPP(hAPP(c_member(X1),X2),X3))|~hBOOL(hAPP(X3,X2))),inference(split_conjunct,[status(thm)],[1324])).
% cnf(1471,plain,(class_Orderings_Oorder(tc_HOL_Obool)),inference(split_conjunct,[status(thm)],[246])).
% fof(1472, plain,![X54]:![X55]:hAPP(c_COMBI(X55),X54)=X54,inference(variable_rename,[status(thm)],[247])).
% cnf(1473,plain,(hAPP(c_COMBI(X1),X2)=X2),inference(split_conjunct,[status(thm)],[1472])).
% fof(1474, plain,![X55]:![X56]:![X57]:![X58]:hAPP(hAPP(c_COMBK(X58,X57),X56),X55)=X56,inference(variable_rename,[status(thm)],[248])).
% cnf(1475,plain,(hAPP(hAPP(c_COMBK(X1,X2),X3),X4)=X3),inference(split_conjunct,[status(thm)],[1474])).
% cnf(1520,plain,(class_Orderings_Olinorder(tc_Nat_Onat)),inference(split_conjunct,[status(thm)],[264])).
% cnf(1523,plain,(class_Orderings_Otop(tc_HOL_Obool)),inference(split_conjunct,[status(thm)],[267])).
% cnf(1524,plain,(class_Orderings_Oord(tc_HOL_Obool)),inference(split_conjunct,[status(thm)],[268])).
% fof(1673, plain,![X4]:![X19]:![X5]:(~(class_Orderings_Oorder(X5))|(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X19),X4)))|((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X4),X19)))|X4=X19)&(~(X4=X19)|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X5,X4),X19)))))),inference(fof_nnf,[status(thm)],[309])).
% fof(1674, plain,![X20]:![X21]:![X22]:(~(class_Orderings_Oorder(X22))|(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X22,X21),X20)))|((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X22,X20),X21)))|X20=X21)&(~(X20=X21)|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X22,X20),X21)))))),inference(variable_rename,[status(thm)],[1673])).
% fof(1675, plain,![X20]:![X21]:![X22]:((((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X22,X20),X21)))|X20=X21)|~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X22,X21),X20))))|~(class_Orderings_Oorder(X22)))&(((~(X20=X21)|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X22,X20),X21)))|~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X22,X21),X20))))|~(class_Orderings_Oorder(X22)))),inference(distribute,[status(thm)],[1674])).
% cnf(1677,plain,(X3=X2|~class_Orderings_Oorder(X1)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,X2),X3))|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,X3),X2))),inference(split_conjunct,[status(thm)],[1675])).
% fof(1840, plain,![X17]:![X2]:![X20]:![X5]:(~(c_Finite__Set_Ofinite(X5,c_Set_Oimage(X20,X5,X2,X17)))|(~(c_Fun_Oinj__on(X20,X5,X2,X17))|c_Finite__Set_Ofinite(X20,X17))),inference(fof_nnf,[status(thm)],[363])).
% fof(1841, plain,![X21]:![X22]:![X23]:![X24]:(~(c_Finite__Set_Ofinite(X24,c_Set_Oimage(X23,X24,X22,X21)))|(~(c_Fun_Oinj__on(X23,X24,X22,X21))|c_Finite__Set_Ofinite(X23,X21))),inference(variable_rename,[status(thm)],[1840])).
% cnf(1842,plain,(c_Finite__Set_Ofinite(X1,X2)|~c_Fun_Oinj__on(X1,X3,X4,X2)|~c_Finite__Set_Ofinite(X3,c_Set_Oimage(X1,X3,X4,X2))),inference(split_conjunct,[status(thm)],[1841])).
% fof(1899, plain,![X17]:![X2]:![X20]:![X5]:((~(c_Fun_Oinj__on(X5,X20,X2,X17))|![X3]:(~(hBOOL(hAPP(hAPP(c_member(X5),X3),X17)))|![X61]:(~(hBOOL(hAPP(hAPP(c_member(X5),X61),X17)))|(~(hAPP(X2,X3)=hAPP(X2,X61))|X3=X61))))&(?[X3]:(hBOOL(hAPP(hAPP(c_member(X5),X3),X17))&?[X61]:(hBOOL(hAPP(hAPP(c_member(X5),X61),X17))&(hAPP(X2,X3)=hAPP(X2,X61)&~(X3=X61))))|c_Fun_Oinj__on(X5,X20,X2,X17))),inference(fof_nnf,[status(thm)],[382])).
% fof(1900, plain,![X62]:![X63]:![X64]:![X65]:((~(c_Fun_Oinj__on(X65,X64,X63,X62))|![X66]:(~(hBOOL(hAPP(hAPP(c_member(X65),X66),X62)))|![X67]:(~(hBOOL(hAPP(hAPP(c_member(X65),X67),X62)))|(~(hAPP(X63,X66)=hAPP(X63,X67))|X66=X67))))&(?[X68]:(hBOOL(hAPP(hAPP(c_member(X65),X68),X62))&?[X69]:(hBOOL(hAPP(hAPP(c_member(X65),X69),X62))&(hAPP(X63,X68)=hAPP(X63,X69)&~(X68=X69))))|c_Fun_Oinj__on(X65,X64,X63,X62))),inference(variable_rename,[status(thm)],[1899])).
% fof(1901, plain,![X62]:![X63]:![X64]:![X65]:((~(c_Fun_Oinj__on(X65,X64,X63,X62))|![X66]:(~(hBOOL(hAPP(hAPP(c_member(X65),X66),X62)))|![X67]:(~(hBOOL(hAPP(hAPP(c_member(X65),X67),X62)))|(~(hAPP(X63,X66)=hAPP(X63,X67))|X66=X67))))&((hBOOL(hAPP(hAPP(c_member(X65),esk46_4(X62,X63,X64,X65)),X62))&(hBOOL(hAPP(hAPP(c_member(X65),esk47_4(X62,X63,X64,X65)),X62))&(hAPP(X63,esk46_4(X62,X63,X64,X65))=hAPP(X63,esk47_4(X62,X63,X64,X65))&~(esk46_4(X62,X63,X64,X65)=esk47_4(X62,X63,X64,X65)))))|c_Fun_Oinj__on(X65,X64,X63,X62))),inference(skolemize,[status(esa)],[1900])).
% fof(1902, plain,![X62]:![X63]:![X64]:![X65]:![X66]:![X67]:((((~(hBOOL(hAPP(hAPP(c_member(X65),X67),X62)))|(~(hAPP(X63,X66)=hAPP(X63,X67))|X66=X67))|~(hBOOL(hAPP(hAPP(c_member(X65),X66),X62))))|~(c_Fun_Oinj__on(X65,X64,X63,X62)))&((hBOOL(hAPP(hAPP(c_member(X65),esk46_4(X62,X63,X64,X65)),X62))&(hBOOL(hAPP(hAPP(c_member(X65),esk47_4(X62,X63,X64,X65)),X62))&(hAPP(X63,esk46_4(X62,X63,X64,X65))=hAPP(X63,esk47_4(X62,X63,X64,X65))&~(esk46_4(X62,X63,X64,X65)=esk47_4(X62,X63,X64,X65)))))|c_Fun_Oinj__on(X65,X64,X63,X62))),inference(shift_quantors,[status(thm)],[1901])).
% fof(1903, plain,![X62]:![X63]:![X64]:![X65]:![X66]:![X67]:((((~(hBOOL(hAPP(hAPP(c_member(X65),X67),X62)))|(~(hAPP(X63,X66)=hAPP(X63,X67))|X66=X67))|~(hBOOL(hAPP(hAPP(c_member(X65),X66),X62))))|~(c_Fun_Oinj__on(X65,X64,X63,X62)))&((hBOOL(hAPP(hAPP(c_member(X65),esk46_4(X62,X63,X64,X65)),X62))|c_Fun_Oinj__on(X65,X64,X63,X62))&((hBOOL(hAPP(hAPP(c_member(X65),esk47_4(X62,X63,X64,X65)),X62))|c_Fun_Oinj__on(X65,X64,X63,X62))&((hAPP(X63,esk46_4(X62,X63,X64,X65))=hAPP(X63,esk47_4(X62,X63,X64,X65))|c_Fun_Oinj__on(X65,X64,X63,X62))&(~(esk46_4(X62,X63,X64,X65)=esk47_4(X62,X63,X64,X65))|c_Fun_Oinj__on(X65,X64,X63,X62)))))),inference(distribute,[status(thm)],[1902])).
% cnf(1904,plain,(c_Fun_Oinj__on(X1,X2,X3,X4)|esk46_4(X4,X3,X2,X1)!=esk47_4(X4,X3,X2,X1)),inference(split_conjunct,[status(thm)],[1903])).
% cnf(1905,plain,(c_Fun_Oinj__on(X1,X2,X3,X4)|hAPP(X3,esk46_4(X4,X3,X2,X1))=hAPP(X3,esk47_4(X4,X3,X2,X1))),inference(split_conjunct,[status(thm)],[1903])).
% fof(1941, plain,![X1]:![X2]:![X5]:![X20]:(~(class_Orderings_Oord(X20))|((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,X20),X2),X1)))|![X3]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X20,hAPP(X2,X3)),hAPP(X1,X3))))&(?[X3]:~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X20,hAPP(X2,X3)),hAPP(X1,X3))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,X20),X2),X1))))),inference(fof_nnf,[status(thm)],[392])).
% fof(1942, plain,![X21]:![X22]:![X23]:![X24]:(~(class_Orderings_Oord(X24))|((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X23,X24),X22),X21)))|![X25]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X24,hAPP(X22,X25)),hAPP(X21,X25))))&(?[X26]:~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X24,hAPP(X22,X26)),hAPP(X21,X26))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X23,X24),X22),X21))))),inference(variable_rename,[status(thm)],[1941])).
% fof(1943, plain,![X21]:![X22]:![X23]:![X24]:(~(class_Orderings_Oord(X24))|((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X23,X24),X22),X21)))|![X25]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X24,hAPP(X22,X25)),hAPP(X21,X25))))&(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X24,hAPP(X22,esk49_4(X21,X22,X23,X24))),hAPP(X21,esk49_4(X21,X22,X23,X24)))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X23,X24),X22),X21))))),inference(skolemize,[status(esa)],[1942])).
% fof(1944, plain,![X21]:![X22]:![X23]:![X24]:![X25]:(((hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X24,hAPP(X22,X25)),hAPP(X21,X25)))|~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X23,X24),X22),X21))))&(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X24,hAPP(X22,esk49_4(X21,X22,X23,X24))),hAPP(X21,esk49_4(X21,X22,X23,X24)))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X23,X24),X22),X21))))|~(class_Orderings_Oord(X24))),inference(shift_quantors,[status(thm)],[1943])).
% fof(1945, plain,![X21]:![X22]:![X23]:![X24]:![X25]:(((hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X24,hAPP(X22,X25)),hAPP(X21,X25)))|~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X23,X24),X22),X21))))|~(class_Orderings_Oord(X24)))&((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X24,hAPP(X22,esk49_4(X21,X22,X23,X24))),hAPP(X21,esk49_4(X21,X22,X23,X24)))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X23,X24),X22),X21)))|~(class_Orderings_Oord(X24)))),inference(distribute,[status(thm)],[1944])).
% cnf(1946,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X2,X1),X3),X4))|~class_Orderings_Oord(X1)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,hAPP(X3,esk49_4(X4,X3,X2,X1))),hAPP(X4,esk49_4(X4,X3,X2,X1))))),inference(split_conjunct,[status(thm)],[1945])).
% cnf(1947,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X1,hAPP(X3,X5)),hAPP(X4,X5)))|~class_Orderings_Oord(X1)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X2,X1),X3),X4))),inference(split_conjunct,[status(thm)],[1945])).
% cnf(2533,plain,(~class_Orderings_Olinorder(X1)|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(X1),X2),X2))),inference(er,[status(thm)],[918,theory(equality)])).
% cnf(2644,plain,(hBOOL(c_Orderings_Otop__class_Otop(tc_HOL_Obool))|~class_Orderings_Otop(tc_HOL_Obool)),inference(spm,[status(thm)],[607,808,theory(equality)])).
% cnf(2645,plain,(hBOOL(c_Orderings_Otop__class_Otop(tc_HOL_Obool))|$false),inference(rw,[status(thm)],[2644,1523,theory(equality)])).
% cnf(2646,plain,(hBOOL(c_Orderings_Otop__class_Otop(tc_HOL_Obool))),inference(cn,[status(thm)],[2645,theory(equality)])).
% cnf(5362,plain,(~class_Orderings_Olinorder(tc_Nat_Onat)|~c_Finite__Set_Ofinite(tc_Nat_Onat,X1)|~hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk11_1(X1)),X1))),inference(spm,[status(thm)],[2533,1191,theory(equality)])).
% cnf(5378,plain,($false|~c_Finite__Set_Ofinite(tc_Nat_Onat,X1)|~hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk11_1(X1)),X1))),inference(rw,[status(thm)],[5362,1520,theory(equality)])).
% cnf(5379,plain,(~c_Finite__Set_Ofinite(tc_Nat_Onat,X1)|~hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk11_1(X1)),X1))),inference(cn,[status(thm)],[5378,theory(equality)])).
% cnf(7017,plain,(hAPP(c_COMBI(X1),esk47_4(X2,c_COMBI(X1),X3,X4))=esk46_4(X2,c_COMBI(X1),X3,X4)|c_Fun_Oinj__on(X4,X3,c_COMBI(X1),X2)),inference(spm,[status(thm)],[1473,1905,theory(equality)])).
% cnf(7284,plain,(esk47_4(X2,c_COMBI(X1),X3,X4)=esk46_4(X2,c_COMBI(X1),X3,X4)|c_Fun_Oinj__on(X4,X3,c_COMBI(X1),X2)),inference(rw,[status(thm)],[7017,1473,theory(equality)])).
% cnf(10367,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2)),hAPP(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)),X2)))|~class_Orderings_Oord(tc_HOL_Obool)),inference(spm,[status(thm)],[1947,661,theory(equality)])).
% cnf(10377,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2)),hAPP(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)),X2)))|$false),inference(rw,[status(thm)],[10367,1524,theory(equality)])).
% cnf(10378,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2)),hAPP(c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)),X2)))),inference(cn,[status(thm)],[10377,theory(equality)])).
% cnf(27201,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2),c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))|~class_Orderings_Oord(tc_HOL_Obool)),inference(spm,[status(thm)],[1946,10378,theory(equality)])).
% cnf(27204,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2)),c_Orderings_Otop__class_Otop(tc_HOL_Obool)))|~class_Orderings_Otop(tc_HOL_Obool)),inference(spm,[status(thm)],[10378,808,theory(equality)])).
% cnf(27232,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X3),hAPP(c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)),X4)))),inference(spm,[status(thm)],[10378,1475,theory(equality)])).
% cnf(27265,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2),c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))|$false),inference(rw,[status(thm)],[27201,1524,theory(equality)])).
% cnf(27266,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2),c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))),inference(cn,[status(thm)],[27265,theory(equality)])).
% cnf(27267,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2)),c_Orderings_Otop__class_Otop(tc_HOL_Obool)))|$false),inference(rw,[status(thm)],[27204,1523,theory(equality)])).
% cnf(27268,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,hAPP(X1,X2)),c_Orderings_Otop__class_Otop(tc_HOL_Obool)))),inference(cn,[status(thm)],[27267,theory(equality)])).
% cnf(27271,plain,(c_Finite__Set_Ofinite(X1,X2)|~c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))),inference(spm,[status(thm)],[1152,27266,theory(equality)])).
% cnf(27734,plain,(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,X2),c_Orderings_Otop__class_Otop(tc_HOL_Obool)))),inference(spm,[status(thm)],[27268,1473,theory(equality)])).
% cnf(27821,plain,(c_Orderings_Otop__class_Otop(tc_HOL_Obool)=X1|~class_Orderings_Oorder(tc_HOL_Obool)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,c_Orderings_Otop__class_Otop(tc_HOL_Obool)),X1))),inference(spm,[status(thm)],[1677,27734,theory(equality)])).
% cnf(27830,plain,(c_Orderings_Otop__class_Otop(tc_HOL_Obool)=X1|$false|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,c_Orderings_Otop__class_Otop(tc_HOL_Obool)),X1))),inference(rw,[status(thm)],[27821,1471,theory(equality)])).
% cnf(27831,plain,(c_Orderings_Otop__class_Otop(tc_HOL_Obool)=X1|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool,c_Orderings_Otop__class_Otop(tc_HOL_Obool)),X1))),inference(cn,[status(thm)],[27830,theory(equality)])).
% cnf(45635,plain,(c_Finite__Set_Ofinite(tc_Option_Ooption(X1),X2)|~c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),inference(spm,[status(thm)],[27271,1136,theory(equality)])).
% cnf(45638,plain,(c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,X1)),inference(spm,[status(thm)],[27271,671,theory(equality)])).
% cnf(55150,plain,(c_Orderings_Otop__class_Otop(tc_HOL_Obool)=hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)),X2)),inference(spm,[status(thm)],[27831,27232,theory(equality)])).
% cnf(70652,plain,(c_Finite__Set_Ofinite(tc_Option_Ooption(tc_Arrow__Order__Mirabelle_Oindi),X1)),inference(spm,[status(thm)],[45635,45638,theory(equality)])).
% cnf(70658,plain,(c_Finite__Set_Ofinite(tc_Option_Ooption(tc_Option_Ooption(tc_Arrow__Order__Mirabelle_Oindi)),X1)),inference(spm,[status(thm)],[45635,70652,theory(equality)])).
% cnf(70669,plain,(c_Finite__Set_Ofinite(X1,X2)|~c_Fun_Oinj__on(X1,tc_Option_Ooption(tc_Option_Ooption(tc_Arrow__Order__Mirabelle_Oindi)),X3,X2)),inference(spm,[status(thm)],[1842,70658,theory(equality)])).
% cnf(118423,plain,(~c_Finite__Set_Ofinite(tc_Nat_Onat,X1)|~hBOOL(hAPP(X1,esk11_1(X1)))),inference(spm,[status(thm)],[5379,1325,theory(equality)])).
% cnf(118735,plain,(~c_Finite__Set_Ofinite(tc_Nat_Onat,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))|~hBOOL(c_Orderings_Otop__class_Otop(tc_HOL_Obool))),inference(spm,[status(thm)],[118423,55150,theory(equality)])).
% cnf(118854,plain,(~c_Finite__Set_Ofinite(tc_Nat_Onat,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))|$false),inference(rw,[status(thm)],[118735,2646,theory(equality)])).
% cnf(118855,plain,(~c_Finite__Set_Ofinite(tc_Nat_Onat,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),inference(cn,[status(thm)],[118854,theory(equality)])).
% cnf(577852,plain,(c_Fun_Oinj__on(X4,X3,c_COMBI(X1),X2)),inference(csr,[status(thm)],[7284,1904])).
% cnf(577853,plain,(c_Finite__Set_Ofinite(X1,X2)),inference(spm,[status(thm)],[70669,577852,theory(equality)])).
% cnf(578465,plain,($false),inference(rw,[status(thm)],[118855,577853,theory(equality)])).
% cnf(578466,plain,($false),inference(cn,[status(thm)],[578465,theory(equality)])).
% cnf(578467,plain,($false),578466,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 15395
% # ...of these trivial : 554
% # ...subsumed : 11183
% # ...remaining for further processing: 3658
% # Other redundant clauses eliminated : 2121
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 55
% # Backward-rewritten : 469
% # Generated clauses : 437129
% # ...of the previous two non-trivial : 409251
% # Contextual simplify-reflections : 1530
% # Paramodulations : 434804
% # Factorizations : 62
% # Equation resolutions : 2269
% # Current number of processed clauses: 2473
% # Positive orientable unit clauses: 468
% # Positive unorientable unit clauses: 42
% # Negative unit clauses : 109
% # Non-unit-clauses : 1854
% # Current number of unprocessed clauses: 308734
% # ...number of literals in the above : 1044616
% # Clause-clause subsumption calls (NU) : 314881
% # Rec. Clause-clause subsumption calls : 205649
% # Unit Clause-clause subsumption calls : 11742
% # Rewrite failures with RHS unbound : 525
% # Indexed BW rewrite attempts : 9997
% # Indexed BW rewrite successes : 459
% # Backwards rewriting index: 1649 leaves, 2.65+/-7.118 terms/leaf
% # Paramod-from index: 509 leaves, 2.27+/-4.750 terms/leaf
% # Paramod-into index: 1461 leaves, 2.44+/-5.620 terms/leaf
% # -------------------------------------------------
% # User time : 20.812 s
% # System time : 0.524 s
% # Total time : 21.336 s
% # Maximum resident set size: 0 pages
% PrfWatch: 29.84 CPU 30.35 WC
% FINAL PrfWatch: 29.84 CPU 30.35 WC
% SZS output end Solution for /tmp/SystemOnTPTP10840/SCT161+1.tptp
%
%------------------------------------------------------------------------------