%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SCT167+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 : 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 : Mon Mar 7 00:25:14 EST 2011
% Result : Theorem 32.06s
% Output : Solution 32.06s
% 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/SystemOnTPTP8214/SCT167+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% WARNING: TreeLimitedRun lost 0.68s, total lost is 0.68s
% found
% SZS status THM for /tmp/SystemOnTPTP8214/SCT167+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP8214/SCT167+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 8302
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.93 CPU 2.01 WC
% PrfWatch: 3.93 CPU 4.02 WC
% PrfWatch: 5.57 CPU 6.05 WC
% PrfWatch: 7.09 CPU 8.09 WC
% PrfWatch: 8.69 CPU 10.09 WC
% PrfWatch: 10.69 CPU 12.10 WC
% # Preprocessing time : 0.189 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 12.68 CPU 14.10 WC
% PrfWatch: 14.67 CPU 16.11 WC
% # SZS output start CNFRefutation.
% fof(7, axiom,![X1]:![X2]:![X3]:(hBOOL(hAPP(hAPP(c_member(X3),X2),X1))<=>hBOOL(hAPP(X1,X2))),file('/tmp/SRASS.s.p', fact_mem__def)).
% fof(10, axiom,![X7]:~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X7),X7))),file('/tmp/SRASS.s.p', fact_less__irrefl__nat)).
% fof(76, axiom,![X40]:(c_Finite__Set_Ofinite(tc_Nat_Onat,X40)<=>?[X9]:![X34]:(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X34),X40))=>hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X34),X9)))),file('/tmp/SRASS.s.p', fact_finite__nat__set__iff__bounded)).
% fof(81, axiom,![X16]:![X2]:(~(X2=X16)|hBOOL(hAPP(hAPP(c_fequal,X2),X16))),file('/tmp/SRASS.s.p', help_c__fequal__2)).
% fof(106, axiom,![X12]:![X39]:![X22]:![X3]:![X48]:![X13]:hAPP(c_COMBS(X13,X48,X3,X22,X39),X12)=hAPP(hAPP(X22,X12),hAPP(X39,X12)),file('/tmp/SRASS.s.p', help_c__COMBS__1)).
% fof(137, axiom,![X13]:![X2]:![X25]:![X3]:hBOOL(hAPP(hAPP(c_member(X3),hAPP(X25,X2)),c_Set_Oimage(X13,X3,X25,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool))))),file('/tmp/SRASS.s.p', fact_rangeI)).
% fof(142, 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(155, axiom,![X1]:![X3]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X1),c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))),file('/tmp/SRASS.s.p', fact_subset__UNIV)).
% fof(164, axiom,![X1]:![X5]:![X3]:(c_Finite__Set_Ofinite(X3,X5)=>(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X1),X5))=>c_Finite__Set_Ofinite(X3,X1))),file('/tmp/SRASS.s.p', fact_rev__finite__subset)).
% fof(249, axiom,![X25]:![X5]:![X13]:![X1]:![X3]:(c_Finite__Set_Ofinite(X3,X1)=>(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X13,tc_HOL_Obool),X5),c_Set_Oimage(X3,X13,X25,X1)))=>c_Finite__Set_Ofinite(X13,X5))),file('/tmp/SRASS.s.p', fact_finite__surj)).
% fof(258, axiom,class_Orderings_Oord(tc_HOL_Obool),file('/tmp/SRASS.s.p', arity_HOL__Obool__Orderings_Oord)).
% fof(297, axiom,![X3]:(c_Finite__Set_Ofinite(tc_Option_Ooption(X3),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X3),tc_HOL_Obool)))<=>c_Finite__Set_Ofinite(X3,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))),file('/tmp/SRASS.s.p', fact_finite__option__UNIV)).
% fof(346, axiom,![X25]:![X3]:![X13]:(c_Set_Oimage(X13,X3,X25,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))<=>![X34]:hAPP(X25,hAPP(c_Hilbert__Choice_Oinv__into(X13,X3,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool)),X25),X34))=X34),file('/tmp/SRASS.s.p', fact_surj__iff__all)).
% fof(358, axiom,![X70]:![X3]:hAPP(c_COMBI(X3),X70)=X70,file('/tmp/SRASS.s.p', help_c__COMBI__1)).
% fof(362, axiom,![X55]:![X25]:![X3]:![X13]:(class_Orderings_Oord(X13)=>(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X3,X13),X25),X55))<=>![X34]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X13,hAPP(X25,X34)),hAPP(X55,X34))))),file('/tmp/SRASS.s.p', fact_le__fun__def)).
% fof(448, axiom,![X1]:![X25]:![X13]:![X16]:![X3]:(hBOOL(hAPP(hAPP(c_member(X3),X16),c_Set_Oimage(X13,X3,X25,X1)))=>hAPP(X25,hAPP(c_Hilbert__Choice_Oinv__into(X13,X3,X1,X25),X16))=X16),file('/tmp/SRASS.s.p', fact_f__inv__into__f)).
% fof(537, plain,![X7]:~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X7),X7))),inference(fof_simplification,[status(thm)],[10,theory(equality)])).
% fof(611, plain,![X1]:![X2]:![X3]:((~(hBOOL(hAPP(hAPP(c_member(X3),X2),X1)))|hBOOL(hAPP(X1,X2)))&(~(hBOOL(hAPP(X1,X2)))|hBOOL(hAPP(hAPP(c_member(X3),X2),X1)))),inference(fof_nnf,[status(thm)],[7])).
% fof(612, plain,![X4]:![X5]:![X6]:((~(hBOOL(hAPP(hAPP(c_member(X6),X5),X4)))|hBOOL(hAPP(X4,X5)))&(~(hBOOL(hAPP(X4,X5)))|hBOOL(hAPP(hAPP(c_member(X6),X5),X4)))),inference(variable_rename,[status(thm)],[611])).
% cnf(613,plain,(hBOOL(hAPP(hAPP(c_member(X1),X2),X3))|~hBOOL(hAPP(X3,X2))),inference(split_conjunct,[status(thm)],[612])).
% fof(621, plain,![X8]:~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X8),X8))),inference(variable_rename,[status(thm)],[537])).
% cnf(622,plain,(~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X1))),inference(split_conjunct,[status(thm)],[621])).
% fof(976, plain,![X40]:((~(c_Finite__Set_Ofinite(tc_Nat_Onat,X40))|?[X9]:![X34]:(~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X34),X40)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X34),X9))))&(![X9]:?[X34]:(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X34),X40))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X34),X9))))|c_Finite__Set_Ofinite(tc_Nat_Onat,X40))),inference(fof_nnf,[status(thm)],[76])).
% fof(977, plain,![X41]:((~(c_Finite__Set_Ofinite(tc_Nat_Onat,X41))|?[X42]:![X43]:(~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X43),X41)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X43),X42))))&(![X44]:?[X45]:(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X45),X41))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X45),X44))))|c_Finite__Set_Ofinite(tc_Nat_Onat,X41))),inference(variable_rename,[status(thm)],[976])).
% fof(978, plain,![X41]:((~(c_Finite__Set_Ofinite(tc_Nat_Onat,X41))|![X43]:(~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X43),X41)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X43),esk19_1(X41)))))&(![X44]:(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk20_2(X41,X44)),X41))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),esk20_2(X41,X44)),X44))))|c_Finite__Set_Ofinite(tc_Nat_Onat,X41))),inference(skolemize,[status(esa)],[977])).
% fof(979, plain,![X41]:![X43]:![X44]:(((hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk20_2(X41,X44)),X41))&~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),esk20_2(X41,X44)),X44))))|c_Finite__Set_Ofinite(tc_Nat_Onat,X41))&((~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X43),X41)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X43),esk19_1(X41))))|~(c_Finite__Set_Ofinite(tc_Nat_Onat,X41)))),inference(shift_quantors,[status(thm)],[978])).
% fof(980, plain,![X41]:![X43]:![X44]:(((hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk20_2(X41,X44)),X41))|c_Finite__Set_Ofinite(tc_Nat_Onat,X41))&(~(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),esk20_2(X41,X44)),X44)))|c_Finite__Set_Ofinite(tc_Nat_Onat,X41)))&((~(hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X43),X41)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X43),esk19_1(X41))))|~(c_Finite__Set_Ofinite(tc_Nat_Onat,X41)))),inference(distribute,[status(thm)],[979])).
% cnf(981,plain,(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),esk19_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)],[980])).
% fof(998, plain,![X17]:![X18]:(~(X18=X17)|hBOOL(hAPP(hAPP(c_fequal,X18),X17))),inference(variable_rename,[status(thm)],[81])).
% cnf(999,plain,(hBOOL(hAPP(hAPP(c_fequal,X1),X2))|X1!=X2),inference(split_conjunct,[status(thm)],[998])).
% fof(1102, plain,![X49]:![X50]:![X51]:![X52]:![X53]:![X54]:hAPP(c_COMBS(X54,X53,X52,X51,X50),X49)=hAPP(hAPP(X51,X49),hAPP(X50,X49)),inference(variable_rename,[status(thm)],[106])).
% cnf(1103,plain,(hAPP(c_COMBS(X1,X2,X3,X4,X5),X6)=hAPP(hAPP(X4,X6),hAPP(X5,X6))),inference(split_conjunct,[status(thm)],[1102])).
% fof(1219, plain,![X26]:![X27]:![X28]:![X29]:hBOOL(hAPP(hAPP(c_member(X29),hAPP(X28,X27)),c_Set_Oimage(X26,X29,X28,c_Orderings_Otop__class_Otop(tc_fun(X26,tc_HOL_Obool))))),inference(variable_rename,[status(thm)],[137])).
% cnf(1220,plain,(hBOOL(hAPP(hAPP(c_member(X1),hAPP(X2,X3)),c_Set_Oimage(X4,X1,X2,c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool)))))),inference(split_conjunct,[status(thm)],[1219])).
% cnf(1239,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)],[142])).
% fof(1281, plain,![X4]:![X5]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool),X4),c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)))),inference(variable_rename,[status(thm)],[155])).
% cnf(1282,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)],[1281])).
% fof(1307, plain,![X1]:![X5]:![X3]:(~(c_Finite__Set_Ofinite(X3,X5))|(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X3,tc_HOL_Obool),X1),X5)))|c_Finite__Set_Ofinite(X3,X1))),inference(fof_nnf,[status(thm)],[164])).
% fof(1308, plain,![X6]:![X7]:![X8]:(~(c_Finite__Set_Ofinite(X8,X7))|(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X8,tc_HOL_Obool),X6),X7)))|c_Finite__Set_Ofinite(X8,X6))),inference(variable_rename,[status(thm)],[1307])).
% cnf(1309,plain,(c_Finite__Set_Ofinite(X1,X2)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2),X3))|~c_Finite__Set_Ofinite(X1,X3)),inference(split_conjunct,[status(thm)],[1308])).
% fof(1618, plain,![X25]:![X5]:![X13]:![X1]:![X3]:(~(c_Finite__Set_Ofinite(X3,X1))|(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X13,tc_HOL_Obool),X5),c_Set_Oimage(X3,X13,X25,X1))))|c_Finite__Set_Ofinite(X13,X5))),inference(fof_nnf,[status(thm)],[249])).
% fof(1619, plain,![X26]:![X27]:![X28]:![X29]:![X30]:(~(c_Finite__Set_Ofinite(X30,X29))|(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X28,tc_HOL_Obool),X27),c_Set_Oimage(X30,X28,X26,X29))))|c_Finite__Set_Ofinite(X28,X27))),inference(variable_rename,[status(thm)],[1618])).
% cnf(1620,plain,(c_Finite__Set_Ofinite(X1,X2)|~hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X2),c_Set_Oimage(X3,X1,X4,X5)))|~c_Finite__Set_Ofinite(X3,X5)),inference(split_conjunct,[status(thm)],[1619])).
% cnf(1639,plain,(class_Orderings_Oord(tc_HOL_Obool)),inference(split_conjunct,[status(thm)],[258])).
% fof(1725, plain,![X3]:((~(c_Finite__Set_Ofinite(tc_Option_Ooption(X3),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X3),tc_HOL_Obool))))|c_Finite__Set_Ofinite(X3,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))&(~(c_Finite__Set_Ofinite(X3,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))))|c_Finite__Set_Ofinite(tc_Option_Ooption(X3),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X3),tc_HOL_Obool))))),inference(fof_nnf,[status(thm)],[297])).
% fof(1726, plain,![X4]:((~(c_Finite__Set_Ofinite(tc_Option_Ooption(X4),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X4),tc_HOL_Obool))))|c_Finite__Set_Ofinite(X4,c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool))))&(~(c_Finite__Set_Ofinite(X4,c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool))))|c_Finite__Set_Ofinite(tc_Option_Ooption(X4),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X4),tc_HOL_Obool))))),inference(variable_rename,[status(thm)],[1725])).
% cnf(1727,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)],[1726])).
% fof(1878, plain,![X25]:![X3]:![X13]:((~(c_Set_Oimage(X13,X3,X25,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))|![X34]:hAPP(X25,hAPP(c_Hilbert__Choice_Oinv__into(X13,X3,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool)),X25),X34))=X34)&(?[X34]:~(hAPP(X25,hAPP(c_Hilbert__Choice_Oinv__into(X13,X3,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool)),X25),X34))=X34)|c_Set_Oimage(X13,X3,X25,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))),inference(fof_nnf,[status(thm)],[346])).
% fof(1879, plain,![X35]:![X36]:![X37]:((~(c_Set_Oimage(X37,X36,X35,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X36,tc_HOL_Obool)))|![X38]:hAPP(X35,hAPP(c_Hilbert__Choice_Oinv__into(X37,X36,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)),X35),X38))=X38)&(?[X39]:~(hAPP(X35,hAPP(c_Hilbert__Choice_Oinv__into(X37,X36,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)),X35),X39))=X39)|c_Set_Oimage(X37,X36,X35,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X36,tc_HOL_Obool)))),inference(variable_rename,[status(thm)],[1878])).
% fof(1880, plain,![X35]:![X36]:![X37]:((~(c_Set_Oimage(X37,X36,X35,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X36,tc_HOL_Obool)))|![X38]:hAPP(X35,hAPP(c_Hilbert__Choice_Oinv__into(X37,X36,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)),X35),X38))=X38)&(~(hAPP(X35,hAPP(c_Hilbert__Choice_Oinv__into(X37,X36,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)),X35),esk43_3(X35,X36,X37)))=esk43_3(X35,X36,X37))|c_Set_Oimage(X37,X36,X35,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X36,tc_HOL_Obool)))),inference(skolemize,[status(esa)],[1879])).
% fof(1881, plain,![X35]:![X36]:![X37]:![X38]:((hAPP(X35,hAPP(c_Hilbert__Choice_Oinv__into(X37,X36,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)),X35),X38))=X38|~(c_Set_Oimage(X37,X36,X35,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X36,tc_HOL_Obool))))&(~(hAPP(X35,hAPP(c_Hilbert__Choice_Oinv__into(X37,X36,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)),X35),esk43_3(X35,X36,X37)))=esk43_3(X35,X36,X37))|c_Set_Oimage(X37,X36,X35,c_Orderings_Otop__class_Otop(tc_fun(X37,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X36,tc_HOL_Obool)))),inference(shift_quantors,[status(thm)],[1880])).
% cnf(1882,plain,(c_Set_Oimage(X1,X2,X3,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool))|hAPP(X3,hAPP(c_Hilbert__Choice_Oinv__into(X1,X2,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)),X3),esk43_3(X3,X2,X1)))!=esk43_3(X3,X2,X1)),inference(split_conjunct,[status(thm)],[1881])).
% fof(1915, plain,![X71]:![X72]:hAPP(c_COMBI(X72),X71)=X71,inference(variable_rename,[status(thm)],[358])).
% cnf(1916,plain,(hAPP(c_COMBI(X1),X2)=X2),inference(split_conjunct,[status(thm)],[1915])).
% fof(1925, plain,![X55]:![X25]:![X3]:![X13]:(~(class_Orderings_Oord(X13))|((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X3,X13),X25),X55)))|![X34]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X13,hAPP(X25,X34)),hAPP(X55,X34))))&(?[X34]:~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X13,hAPP(X25,X34)),hAPP(X55,X34))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X3,X13),X25),X55))))),inference(fof_nnf,[status(thm)],[362])).
% fof(1926, plain,![X56]:![X57]:![X58]:![X59]:(~(class_Orderings_Oord(X59))|((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X58,X59),X57),X56)))|![X60]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X59,hAPP(X57,X60)),hAPP(X56,X60))))&(?[X61]:~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X59,hAPP(X57,X61)),hAPP(X56,X61))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X58,X59),X57),X56))))),inference(variable_rename,[status(thm)],[1925])).
% fof(1927, plain,![X56]:![X57]:![X58]:![X59]:(~(class_Orderings_Oord(X59))|((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X58,X59),X57),X56)))|![X60]:hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X59,hAPP(X57,X60)),hAPP(X56,X60))))&(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X59,hAPP(X57,esk44_4(X56,X57,X58,X59))),hAPP(X56,esk44_4(X56,X57,X58,X59)))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X58,X59),X57),X56))))),inference(skolemize,[status(esa)],[1926])).
% fof(1928, plain,![X56]:![X57]:![X58]:![X59]:![X60]:(((hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X59,hAPP(X57,X60)),hAPP(X56,X60)))|~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X58,X59),X57),X56))))&(~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X59,hAPP(X57,esk44_4(X56,X57,X58,X59))),hAPP(X56,esk44_4(X56,X57,X58,X59)))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X58,X59),X57),X56))))|~(class_Orderings_Oord(X59))),inference(shift_quantors,[status(thm)],[1927])).
% fof(1929, plain,![X56]:![X57]:![X58]:![X59]:![X60]:(((hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X59,hAPP(X57,X60)),hAPP(X56,X60)))|~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X58,X59),X57),X56))))|~(class_Orderings_Oord(X59)))&((~(hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(X59,hAPP(X57,esk44_4(X56,X57,X58,X59))),hAPP(X56,esk44_4(X56,X57,X58,X59)))))|hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X58,X59),X57),X56)))|~(class_Orderings_Oord(X59)))),inference(distribute,[status(thm)],[1928])).
% cnf(1930,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,esk44_4(X4,X3,X2,X1))),hAPP(X4,esk44_4(X4,X3,X2,X1))))),inference(split_conjunct,[status(thm)],[1929])).
% cnf(1931,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)],[1929])).
% fof(2214, plain,![X1]:![X25]:![X13]:![X16]:![X3]:(~(hBOOL(hAPP(hAPP(c_member(X3),X16),c_Set_Oimage(X13,X3,X25,X1))))|hAPP(X25,hAPP(c_Hilbert__Choice_Oinv__into(X13,X3,X1,X25),X16))=X16),inference(fof_nnf,[status(thm)],[448])).
% fof(2215, plain,![X26]:![X27]:![X28]:![X29]:![X30]:(~(hBOOL(hAPP(hAPP(c_member(X30),X29),c_Set_Oimage(X28,X30,X27,X26))))|hAPP(X27,hAPP(c_Hilbert__Choice_Oinv__into(X28,X30,X26,X27),X29))=X29),inference(variable_rename,[status(thm)],[2214])).
% cnf(2216,plain,(hAPP(X1,hAPP(c_Hilbert__Choice_Oinv__into(X2,X3,X4,X1),X5))=X5|~hBOOL(hAPP(hAPP(c_member(X3),X5),c_Set_Oimage(X2,X3,X1,X4)))),inference(split_conjunct,[status(thm)],[2215])).
% cnf(2611,plain,(hBOOL(hAPP(hAPP(c_fequal,X1),X1))),inference(er,[status(thm)],[999,theory(equality)])).
% cnf(4142,plain,(hBOOL(hAPP(hAPP(c_member(X1),X3),c_Set_Oimage(X4,X1,c_COMBI(X2),c_Orderings_Otop__class_Otop(tc_fun(X4,tc_HOL_Obool)))))),inference(spm,[status(thm)],[1220,1916,theory(equality)])).
% cnf(4583,plain,(hAPP(c_COMBS(X1,X2,X3,X4,c_COMBI(X5)),X6)=hAPP(hAPP(X4,X6),X6)),inference(spm,[status(thm)],[1103,1916,theory(equality)])).
% cnf(4957,plain,(~c_Finite__Set_Ofinite(tc_Nat_Onat,X1)|~hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk19_1(X1)),X1))),inference(spm,[status(thm)],[622,981,theory(equality)])).
% cnf(5081,plain,(c_Finite__Set_Ofinite(X1,X2)|~c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))),inference(spm,[status(thm)],[1309,1282,theory(equality)])).
% cnf(9795,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)],[1931,1282,theory(equality)])).
% cnf(9805,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)],[9795,1639,theory(equality)])).
% cnf(9806,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)],[9805,theory(equality)])).
% cnf(30624,plain,(c_Finite__Set_Ofinite(tc_Arrow__Order__Mirabelle_Oindi,X1)),inference(spm,[status(thm)],[5081,1239,theory(equality)])).
% cnf(33994,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)],[1930,9806,theory(equality)])).
% cnf(34064,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)],[33994,1639,theory(equality)])).
% cnf(34065,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)],[34064,theory(equality)])).
% cnf(34071,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)],[1309,34065,theory(equality)])).
% cnf(45507,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)],[34071,1727,theory(equality)])).
% cnf(59138,plain,(hAPP(c_COMBI(X1),hAPP(c_Hilbert__Choice_Oinv__into(X2,X3,c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool)),c_COMBI(X1)),X4))=X4),inference(spm,[status(thm)],[2216,4142,theory(equality)])).
% cnf(59160,plain,(hAPP(c_Hilbert__Choice_Oinv__into(X2,X3,c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool)),c_COMBI(X1)),X4)=X4),inference(rw,[status(thm)],[59138,1916,theory(equality)])).
% cnf(86941,plain,(c_Finite__Set_Ofinite(tc_Option_Ooption(tc_Arrow__Order__Mirabelle_Oindi),X1)),inference(spm,[status(thm)],[45507,30624,theory(equality)])).
% cnf(86950,plain,(c_Finite__Set_Ofinite(tc_Option_Ooption(tc_Option_Ooption(tc_Arrow__Order__Mirabelle_Oindi)),X1)),inference(spm,[status(thm)],[45507,86941,theory(equality)])).
% cnf(94434,plain,(hBOOL(hAPP(c_COMBS(X2,X3,X4,c_fequal,c_COMBI(X5)),X1))),inference(spm,[status(thm)],[2611,4583,theory(equality)])).
% cnf(127036,plain,(c_Set_Oimage(X1,X2,c_COMBI(X3),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool))|hAPP(c_COMBI(X3),esk43_3(c_COMBI(X3),X2,X1))!=esk43_3(c_COMBI(X3),X2,X1)),inference(spm,[status(thm)],[1882,59160,theory(equality)])).
% cnf(127075,plain,(c_Set_Oimage(X1,X2,c_COMBI(X3),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool))|$false),inference(rw,[status(thm)],[127036,1916,theory(equality)])).
% cnf(127076,plain,(c_Set_Oimage(X1,X2,c_COMBI(X3),c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))=c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool))),inference(cn,[status(thm)],[127075,theory(equality)])).
% cnf(149723,plain,(~c_Finite__Set_Ofinite(tc_Nat_Onat,X1)|~hBOOL(hAPP(X1,esk19_1(X1)))),inference(spm,[status(thm)],[4957,613,theory(equality)])).
% cnf(151480,plain,(~c_Finite__Set_Ofinite(tc_Nat_Onat,c_COMBS(X1,X2,X3,c_fequal,c_COMBI(X4)))),inference(spm,[status(thm)],[149723,94434,theory(equality)])).
% cnf(286103,plain,(c_Finite__Set_Ofinite(X1,X2)|~c_Finite__Set_Ofinite(X3,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))|~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(spm,[status(thm)],[1620,127076,theory(equality)])).
% cnf(286166,plain,(c_Finite__Set_Ofinite(X1,X2)|~c_Finite__Set_Ofinite(X3,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))|$false),inference(rw,[status(thm)],[286103,34065,theory(equality)])).
% cnf(286167,plain,(c_Finite__Set_Ofinite(X1,X2)|~c_Finite__Set_Ofinite(X3,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool)))),inference(cn,[status(thm)],[286166,theory(equality)])).
% cnf(286201,plain,(c_Finite__Set_Ofinite(X1,X2)),inference(spm,[status(thm)],[286167,86950,theory(equality)])).
% cnf(286602,plain,($false),inference(rw,[status(thm)],[151480,286201,theory(equality)])).
% cnf(286603,plain,($false),inference(cn,[status(thm)],[286602,theory(equality)])).
% cnf(286604,plain,($false),286603,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 10490
% # ...of these trivial : 343
% # ...subsumed : 7250
% # ...remaining for further processing: 2897
% # Other redundant clauses eliminated : 990
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 59
% # Backward-rewritten : 323
% # Generated clauses : 208902
% # ...of the previous two non-trivial : 190997
% # Contextual simplify-reflections : 1323
% # Paramodulations : 207794
% # Factorizations : 19
% # Equation resolutions : 1092
% # Current number of processed clauses: 1869
% # Positive orientable unit clauses: 466
% # Positive unorientable unit clauses: 36
% # Negative unit clauses : 120
% # Non-unit-clauses : 1247
% # Current number of unprocessed clauses: 162103
% # ...number of literals in the above : 535145
% # Clause-clause subsumption calls (NU) : 315926
% # Rec. Clause-clause subsumption calls : 219727
% # Unit Clause-clause subsumption calls : 12288
% # Rewrite failures with RHS unbound : 414
% # Indexed BW rewrite attempts : 16802
% # Indexed BW rewrite successes : 362
% # Backwards rewriting index: 1422 leaves, 2.74+/-8.136 terms/leaf
% # Paramod-from index: 349 leaves, 2.55+/-7.353 terms/leaf
% # Paramod-into index: 1279 leaves, 2.52+/-6.805 terms/leaf
% # -------------------------------------------------
% # User time : 10.978 s
% # System time : 0.318 s
% # Total time : 11.296 s
% # Maximum resident set size: 0 pages
% PrfWatch: 16.13 CPU 17.57 WC
% FINAL PrfWatch: 16.13 CPU 17.57 WC
% SZS output end Solution for /tmp/SystemOnTPTP8214/SCT167+1.tptp
%
%------------------------------------------------------------------------------