%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SCT162+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:08:35 PM UTC 2026
% Result : ContradictoryAxioms 13.59s 2.27s
% Output : CNFRefutation 13.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 18
% Syntax : Number of formulae : 72 ( 28 unt; 0 def)
% Number of atoms : 147 ( 48 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 127 ( 52 ~; 50 |; 7 &)
% ( 3 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-4 aty)
% Number of functors : 18 ( 18 usr; 4 con; 0-4 aty)
% Number of variables : 154 ( 26 sgn 80 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_finite__code,axiom,
! [X7,X5] :
( class_Finite__Set_Ofinite(X5)
=> c_Finite__Set_Ofinite(X5,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_finite__code) ).
fof(arity_fun__Finite__Set_Ofinite,axiom,
! [X86,X85] :
( ( class_Finite__Set_Ofinite(X86)
& class_Finite__Set_Ofinite(X85) )
=> class_Finite__Set_Ofinite(tc_fun(X85,X86)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_fun__Finite__Set_Ofinite) ).
fof(fact_rev__finite__subset,axiom,
! [X7,X6,X5] :
( c_Finite__Set_Ofinite(X5,X6)
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool),X7),X6))
=> c_Finite__Set_Ofinite(X5,X7) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_rev__finite__subset) ).
fof(fact_subset__UNIV,axiom,
! [X7,X5] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X5,tc_HOL_Obool),X7),c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_subset__UNIV) ).
fof(fact_finite__option__UNIV,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('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_finite__option__UNIV) ).
fof(arity_HOL__Obool__Finite__Set_Ofinite,axiom,
class_Finite__Set_Ofinite(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_HOL__Obool__Finite__Set_Ofinite) ).
fof(arity_Product____Type__Ounit__Finite__Set_Ofinite,axiom,
class_Finite__Set_Ofinite(tc_Product__Type_Ounit),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Product____Type__Ounit__Finite__Set_Ofinite) ).
fof(fact_Suc__inject,axiom,
! [X15,X16] :
( hAPP(c_Nat_OSuc,X16) = hAPP(c_Nat_OSuc,X15)
=> X16 = X15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Suc__inject) ).
fof(fact_gr0__conv__Suc,axiom,
! [X8] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X8))
<=> ? [X52] : X8 = hAPP(c_Nat_OSuc,X52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_gr0__conv__Suc) ).
fof(fact_zero__less__Suc,axiom,
! [X13] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(c_Nat_OSuc,X13))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_zero__less__Suc) ).
fof(fact_top__apply,axiom,
! [X20,X28,X5] :
( class_Orderings_Otop(X5)
=> hAPP(c_Orderings_Otop__class_Otop(tc_fun(X28,X5)),X20) = c_Orderings_Otop__class_Otop(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_top__apply) ).
fof(fact_finite__imageD,axiom,
! [X7,X2,X28,X5] :
( c_Finite__Set_Ofinite(X5,c_Set_Oimage(X28,X5,X2,X7))
=> ( c_Fun_Oinj__on(X28,X5,X2,X7)
=> c_Finite__Set_Ofinite(X28,X7) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_finite__imageD) ).
fof(fact_inj__on__def,axiom,
! [X7,X2,X28,X5] :
( c_Fun_Oinj__on(X5,X28,X2,X7)
<=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(X5),X3),X7))
=> ! [X41] :
( hBOOL(hAPP(hAPP(c_member(X5),X41),X7))
=> ( hAPP(X2,X3) = hAPP(X2,X41)
=> X3 = X41 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_inj__on__def) ).
fof(fact_Zero__not__Suc,axiom,
! [X17] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != hAPP(c_Nat_OSuc,X17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_Zero__not__Suc) ).
fof(fact_ext,axiom,
! [X1,X2] :
( ! [X3] : hAPP(X2,X3) = hAPP(X1,X3)
=> X2 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_ext) ).
fof(arity_HOL__Obool__Orderings_Otop,axiom,
class_Orderings_Otop(tc_HOL_Obool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_HOL__Obool__Orderings_Otop) ).
fof(fact_surj__f__inv__f,axiom,
! [X23,X2,X5,X28] :
( c_Set_Oimage(X28,X5,X2,c_Orderings_Otop__class_Otop(tc_fun(X28,tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool))
=> hAPP(X2,hAPP(c_Hilbert__Choice_Oinv__into(X28,X5,c_Orderings_Otop__class_Otop(tc_fun(X28,tc_HOL_Obool)),X2),X23)) = X23 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_surj__f__inv__f) ).
fof(fact_finite__UNIV__inj__surj,axiom,
! [X2,X5] :
( c_Finite__Set_Ofinite(X5,c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)))
=> ( c_Fun_Oinj__on(X5,X5,X2,c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)))
=> c_Set_Oimage(X5,X5,X2,c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(X5,tc_HOL_Obool)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_finite__UNIV__inj__surj) ).
fof(c_0_18,plain,
! [X988,X989] :
( c_Finite__Set_Ofinite(X989,X988)
| ~ class_Finite__Set_Ofinite(X989) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_finite__code])])]) ).
fof(c_0_19,plain,
! [X1659,X1660] :
( class_Finite__Set_Ofinite(tc_fun(X1660,X1659))
| ~ class_Finite__Set_Ofinite(X1659)
| ~ class_Finite__Set_Ofinite(X1660) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[arity_fun__Finite__Set_Ofinite])])]) ).
fof(c_0_20,plain,
! [X992,X993,X994] :
( c_Finite__Set_Ofinite(X994,X992)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X994,tc_HOL_Obool),X992),X993))
| ~ c_Finite__Set_Ofinite(X994,X993) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_rev__finite__subset])])]) ).
fof(c_0_21,plain,
! [X725,X726] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X726,tc_HOL_Obool),X725),c_Orderings_Otop__class_Otop(tc_fun(X726,tc_HOL_Obool)))),
inference(variable_rename,[status(thm)],[fact_subset__UNIV]) ).
cnf(c_0_22,plain,
( ~ class_Finite__Set_Ofinite(X1)
| c_Finite__Set_Ofinite(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_23,plain,
( ~ class_Finite__Set_Ofinite(X2)
| ~ class_Finite__Set_Ofinite(X1)
| class_Finite__Set_Ofinite(tc_fun(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_24,plain,
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,tc_HOL_Obool),X3),X2))
| ~ c_Finite__Set_Ofinite(X1,X2)
| c_Finite__Set_Ofinite(X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_25,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)],[c_0_21]) ).
fof(c_0_26,plain,
! [X998] :
( ( c_Finite__Set_Ofinite(tc_Option_Ooption(X998),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X998),tc_HOL_Obool)))
| ~ c_Finite__Set_Ofinite(X998,c_Orderings_Otop__class_Otop(tc_fun(X998,tc_HOL_Obool))) )
& ( c_Finite__Set_Ofinite(X998,c_Orderings_Otop__class_Otop(tc_fun(X998,tc_HOL_Obool)))
| ~ c_Finite__Set_Ofinite(tc_Option_Ooption(X998),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X998),tc_HOL_Obool))) ) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_finite__option__UNIV])])]) ).
cnf(c_0_27,plain,
( ~ class_Finite__Set_Ofinite(X1)
| ~ class_Finite__Set_Ofinite(X2)
| c_Finite__Set_Ofinite(tc_fun(X1,X2),X3) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_28,plain,
class_Finite__Set_Ofinite(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Finite__Set_Ofinite]) ).
cnf(c_0_29,plain,
( ~ c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| c_Finite__Set_Ofinite(X1,X2) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_30,plain,
( ~ c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| c_Finite__Set_Ofinite(tc_Option_Ooption(X1),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X1),tc_HOL_Obool))) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_31,plain,
( ~ class_Finite__Set_Ofinite(X1)
| c_Finite__Set_Ofinite(tc_fun(X1,tc_HOL_Obool),X2) ),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_32,plain,
class_Finite__Set_Ofinite(tc_Product__Type_Ounit),
inference(split_conjunct,[status(thm)],[arity_Product____Type__Ounit__Finite__Set_Ofinite]) ).
cnf(c_0_33,plain,
( ~ c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| c_Finite__Set_Ofinite(tc_Option_Ooption(X1),X2) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
cnf(c_0_34,plain,
c_Finite__Set_Ofinite(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool),X1),
inference(spm,[status(thm)],[c_0_31,c_0_32]) ).
cnf(c_0_35,plain,
c_Finite__Set_Ofinite(tc_Option_Ooption(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool)),X1),
inference(spm,[status(thm)],[c_0_33,c_0_34]) ).
fof(c_0_36,plain,
! [X1257,X1258] :
( X1258 = X1257
| hAPP(c_Nat_OSuc,X1258) != hAPP(c_Nat_OSuc,X1257) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_Suc__inject])])]) ).
fof(c_0_37,plain,
! [X1313,X1315,X1316] :
( ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X1315))
| X1315 != hAPP(c_Nat_OSuc,X1316) )
& ( X1313 = hAPP(c_Nat_OSuc,esk33_1(X1313))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X1313)) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_gr0__conv__Suc])])])])])]) ).
fof(c_0_38,plain,
! [X1250] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(c_Nat_OSuc,X1250))),
inference(variable_rename,[status(thm)],[fact_zero__less__Suc]) ).
fof(c_0_39,plain,
! [X149,X150,X151] :
( hAPP(c_Orderings_Otop__class_Otop(tc_fun(X150,X151)),X149) = c_Orderings_Otop__class_Otop(X151)
| ~ class_Orderings_Otop(X151) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_top__apply])])]) ).
fof(c_0_40,plain,
! [X1441,X1442,X1443,X1444] :
( c_Finite__Set_Ofinite(X1443,X1441)
| ~ c_Fun_Oinj__on(X1443,X1444,X1442,X1441)
| ~ c_Finite__Set_Ofinite(X1444,c_Set_Oimage(X1443,X1444,X1442,X1441)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_finite__imageD])])]) ).
cnf(c_0_41,plain,
c_Finite__Set_Ofinite(tc_Option_Ooption(tc_Option_Ooption(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool))),X1),
inference(spm,[status(thm)],[c_0_33,c_0_35]) ).
cnf(c_0_42,plain,
( hAPP(c_Nat_OSuc,X1) != hAPP(c_Nat_OSuc,X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_43,plain,
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X1))
| X1 = hAPP(c_Nat_OSuc,esk33_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_44,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),hAPP(c_Nat_OSuc,X1))),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
fof(c_0_45,plain,
! [X319,X320,X321,X322,X323,X324,X325,X326,X327,X328] :
( ( c_Fun_Oinj__on(X328,X327,X326,X325)
| esk5_4(X325,X326,X327,X328) != esk6_4(X325,X326,X327,X328) )
& ( c_Fun_Oinj__on(X328,X327,X326,X325)
| hAPP(X326,esk5_4(X325,X326,X327,X328)) = hAPP(X326,esk6_4(X325,X326,X327,X328)) )
& ( c_Fun_Oinj__on(X328,X327,X326,X325)
| hBOOL(hAPP(hAPP(c_member(X328),esk6_4(X325,X326,X327,X328)),X325)) )
& ( c_Fun_Oinj__on(X328,X327,X326,X325)
| hBOOL(hAPP(hAPP(c_member(X328),esk5_4(X325,X326,X327,X328)),X325)) )
& ( X323 = X324
| hAPP(X320,X323) != hAPP(X320,X324)
| ~ hBOOL(hAPP(hAPP(c_member(X322),X324),X319))
| ~ hBOOL(hAPP(hAPP(c_member(X322),X323),X319))
| ~ c_Fun_Oinj__on(X322,X321,X320,X319) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inj__on__def])])])])])])]) ).
fof(c_0_46,plain,
! [X17] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != hAPP(c_Nat_OSuc,X17),
inference(fof_simplification,[status(thm)],[fact_Zero__not__Suc]) ).
fof(c_0_47,plain,
! [X89,X90] :
( X90 = X89
| hAPP(X90,esk1_2(X89,X90)) != hAPP(X89,esk1_2(X89,X90)) ),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_ext])])])]) ).
cnf(c_0_48,plain,
( ~ class_Orderings_Otop(X1)
| hAPP(c_Orderings_Otop__class_Otop(tc_fun(X2,X1)),X3) = c_Orderings_Otop__class_Otop(X1) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_49,plain,
class_Orderings_Otop(tc_HOL_Obool),
inference(split_conjunct,[status(thm)],[arity_HOL__Obool__Orderings_Otop]) ).
cnf(c_0_50,plain,
( ~ c_Fun_Oinj__on(X2,X1,X3,X4)
| ~ c_Finite__Set_Ofinite(X1,c_Set_Oimage(X2,X1,X3,X4))
| c_Finite__Set_Ofinite(X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_51,plain,
c_Finite__Set_Ofinite(tc_Option_Ooption(tc_Option_Ooption(tc_Option_Ooption(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool)))),X1),
inference(spm,[status(thm)],[c_0_33,c_0_41]) ).
cnf(c_0_52,plain,
esk33_1(hAPP(c_Nat_OSuc,X1)) = X1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43])]),c_0_44])]) ).
cnf(c_0_53,plain,
( c_Fun_Oinj__on(X4,X3,X1,X2)
| hAPP(X1,esk5_4(X2,X1,X3,X4)) = hAPP(X1,esk6_4(X2,X1,X3,X4)) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
cnf(c_0_54,plain,
( esk5_4(X1,X2,X3,X4) != esk6_4(X1,X2,X3,X4)
| c_Fun_Oinj__on(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
fof(c_0_55,plain,
! [X1251] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != hAPP(c_Nat_OSuc,X1251),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[c_0_46])]) ).
fof(c_0_56,plain,
! [X1496,X1497,X1498,X1499] :
( hAPP(X1497,hAPP(c_Hilbert__Choice_Oinv__into(X1499,X1498,c_Orderings_Otop__class_Otop(tc_fun(X1499,tc_HOL_Obool)),X1497),X1496)) = X1496
| c_Set_Oimage(X1499,X1498,X1497,c_Orderings_Otop__class_Otop(tc_fun(X1499,tc_HOL_Obool))) != c_Orderings_Otop__class_Otop(tc_fun(X1498,tc_HOL_Obool)) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_surj__f__inv__f])])]) ).
cnf(c_0_57,plain,
( hAPP(X1,esk1_2(X2,X1)) != hAPP(X2,esk1_2(X2,X1))
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_58,plain,
hAPP(c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)),X2) = c_Orderings_Otop__class_Otop(tc_HOL_Obool),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
fof(c_0_59,plain,
! [X1607,X1608] :
( c_Set_Oimage(X1608,X1608,X1607,c_Orderings_Otop__class_Otop(tc_fun(X1608,tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(X1608,tc_HOL_Obool))
| ~ c_Fun_Oinj__on(X1608,X1608,X1607,c_Orderings_Otop__class_Otop(tc_fun(X1608,tc_HOL_Obool)))
| ~ c_Finite__Set_Ofinite(X1608,c_Orderings_Otop__class_Otop(tc_fun(X1608,tc_HOL_Obool))) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_finite__UNIV__inj__surj])])]) ).
cnf(c_0_60,plain,
( ~ c_Fun_Oinj__on(X1,tc_Option_Ooption(tc_Option_Ooption(tc_Option_Ooption(tc_fun(tc_Product__Type_Ounit,tc_HOL_Obool)))),X3,X2)
| c_Finite__Set_Ofinite(X1,X2) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_61,plain,
c_Fun_Oinj__on(X1,X2,c_Nat_OSuc,X3),
inference(csr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_53]),c_0_52]),c_0_54]) ).
cnf(c_0_62,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != hAPP(c_Nat_OSuc,X1),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
cnf(c_0_63,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),X4)) = X4 ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_64,plain,
( hAPP(X1,esk1_2(c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool)),X1)) != c_Orderings_Otop__class_Otop(tc_HOL_Obool)
| X1 = c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool)) ),
inference(spm,[status(thm)],[c_0_57,c_0_58]) ).
cnf(c_0_65,plain,
( ~ c_Fun_Oinj__on(X1,X1,X2,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| ~ c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| c_Set_Oimage(X1,X1,X2,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
cnf(c_0_66,plain,
c_Finite__Set_Ofinite(X1,X2),
inference(spm,[status(thm)],[c_0_60,c_0_61]) ).
cnf(c_0_67,plain,
c_Set_Oimage(X1,X2,c_Nat_OSuc,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))) != c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool)),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_63])]) ).
cnf(c_0_68,plain,
c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)) = c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool)),
inference(spm,[status(thm)],[c_0_64,c_0_58]) ).
cnf(c_0_69,plain,
( ~ c_Fun_Oinj__on(X1,X1,X2,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)))
| c_Set_Oimage(X1,X1,X2,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))) = c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_65,c_0_66])]) ).
cnf(c_0_70,plain,
c_Set_Oimage(X1,X2,c_Nat_OSuc,c_Orderings_Otop__class_Otop(tc_fun(X3,tc_HOL_Obool))) != c_Orderings_Otop__class_Otop(tc_fun(X2,tc_HOL_Obool)),
inference(spm,[status(thm)],[c_0_67,c_0_68]) ).
cnf(c_0_71,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_61]),c_0_70]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT162+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n015.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 04:38:36 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 Running first-order theorem proving
% 0.15/0.42 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.59/2.27 % Version: 3.5.1
% 13.59/2.27 % Preprocessing class: FSLSSMSMSSSNFFN.
% 13.59/2.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.59/2.27 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 13.59/2.27 % Starting new_bool_3 with 300s (1) cores
% 13.59/2.27 % Starting new_bool_1 with 300s (1) cores
% 13.59/2.27 % Starting sh5l with 300s (1) cores
% 13.59/2.27 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 568632 completed with status 0
% 13.59/2.27 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 13.59/2.27 % Preprocessing class: FSLSSMSMSSSNFFN.
% 13.59/2.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.59/2.27 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 13.59/2.27 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 13.59/2.27 % No SInE strategy applied
% 13.59/2.27 % Search class: FGHSM-FSLM32-DFFFFFNN
% 13.59/2.27 % Scheduled 13 strats onto 5 cores with 1500 seconds (1500 total)
% 13.59/2.27 % Starting SubtermCWHack with 136s (1) cores
% 13.59/2.27 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 13.59/2.27 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 113s (1) cores
% 13.59/2.27 % Starting G-E--_300_C18_F1_SE_CS_SP_PS_S0Y with 113s (1) cores
% 13.59/2.27 % Starting U----_206c_05_B11_00_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 113s (1) cores
% 13.59/2.27 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 568642 completed with status 0
% 13.59/2.27 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 13.59/2.27 % Preprocessing class: FSLSSMSMSSSNFFN.
% 13.59/2.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 13.59/2.27 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 13.59/2.27 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 13.59/2.27 % No SInE strategy applied
% 13.59/2.27 % Search class: FGHSM-FSLM32-DFFFFFNN
% 13.59/2.27 % Scheduled 13 strats onto 5 cores with 1500 seconds (1500 total)
% 13.59/2.27 % Starting SubtermCWHack with 136s (1) cores
% 13.59/2.27 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 13.59/2.27 % Preprocessing time : 0.010 s
% 13.59/2.27 % Presaturation interreduction done
% 13.59/2.27
% 13.59/2.27 % Proof found!
% 13.59/2.27 % SZS status ContradictoryAxioms
% 13.59/2.27 % SZS output start CNFRefutation
% See solution above
% 13.59/2.27 % Parsed axioms : 532
% 13.59/2.27 % Removed by relevancy pruning/SinE : 0
% 13.59/2.27 % Initial clauses : 788
% 13.59/2.27 % Removed in clause preprocessing : 50
% 13.59/2.27 % Initial clauses in saturation : 738
% 13.59/2.27 % Processed clauses : 8872
% 13.59/2.27 % ...of these trivial : 106
% 13.59/2.27 % ...subsumed : 5906
% 13.59/2.27 % ...remaining for further processing : 2860
% 13.59/2.27 % Other redundant clauses eliminated : 740
% 13.59/2.27 % Clauses deleted for lack of memory : 0
% 13.59/2.27 % Backward-subsumed : 120
% 13.59/2.27 % Backward-rewritten : 462
% 13.59/2.27 % Generated clauses : 57427
% 13.59/2.27 % ...of the previous two non-redundant : 51759
% 13.59/2.27 % ...aggressively subsumed : 0
% 13.59/2.27 % Contextual simplify-reflections : 11
% 13.59/2.27 % Paramodulations : 56657
% 13.59/2.27 % Factorizations : 8
% 13.59/2.27 % NegExts : 0
% 13.59/2.27 % Equation resolutions : 774
% 13.59/2.27 % Disequality decompositions : 0
% 13.59/2.27 % Total rewrite steps : 23209
% 13.59/2.27 % ...of those cached : 20509
% 13.59/2.27 % Propositional unsat checks : 0
% 13.59/2.27 % Propositional check models : 0
% 13.59/2.27 % Propositional check unsatisfiable : 0
% 13.59/2.27 % Propositional clauses : 0
% 13.59/2.27 % Propositional clauses after purity: 0
% 13.59/2.27 % Propositional unsat core size : 0
% 13.59/2.27 % Propositional preprocessing time : 0.000
% 13.59/2.27 % Propositional encoding time : 0.000
% 13.59/2.27 % Propositional solver time : 0.000
% 13.59/2.27 % Success case prop preproc time : 0.000
% 13.59/2.27 % Success case prop encoding time : 0.000
% 13.59/2.27 % Success case prop solver time : 0.000
% 13.59/2.27 % Current number of processed clauses : 1644
% 13.59/2.27 % Positive orientable unit clauses : 214
% 13.59/2.27 % Positive unorientable unit clauses: 11
% 13.59/2.27 % Negative unit clauses : 245
% 13.59/2.27 % Non-unit-clauses : 1174
% 13.59/2.27 % Current number of unprocessed clauses: 43754
% 13.59/2.27 % ...number of literals in the above : 126957
% 13.59/2.27 % Current number of archived formulas : 0
% 13.59/2.27 % Current number of archived clauses : 1121
% 13.59/2.27 % Clause-clause subsumption calls (NU) : 356871
% 13.59/2.27 % Rec. Clause-clause subsumption calls : 176018
% 13.59/2.27 % Non-unit clause-clause subsumptions : 2755
% 13.59/2.27 % Unit Clause-clause subsumption calls : 23208
% 13.59/2.27 % Rewrite failures with RHS unbound : 276
% 13.59/2.27 % BW rewrite match attempts : 5688
% 13.59/2.27 % BW rewrite match successes : 360
% 13.59/2.27 % Condensation attempts : 0
% 13.59/2.27 % Condensation successes : 0
% 13.59/2.27 % Termbank termtop insertions : 1411506
% 13.59/2.27 % Search garbage collected termcells : 11508
% 13.59/2.27
% 13.59/2.27 % -------------------------------------------------
% 13.59/2.27 % User time : 1.703 s
% 13.59/2.27 % System time : 0.053 s
% 13.59/2.27 % Total time : 1.756 s
% 13.59/2.27 % Maximum resident set size: 7148 pages
% 13.59/2.27
% 13.59/2.27 % -------------------------------------------------
% 13.59/2.27 % User time : 8.150 s
% 13.59/2.27 % System time : 0.282 s
% 13.59/2.27 % Total time : 8.433 s
% 13.59/2.27 % Maximum resident set size: 5376 pages
% 13.59/2.27 % E exiting
%------------------------------------------------------------------------------