%------------------------------------------------------------------------------
% File : ET---2.0
% Problem : SCT165+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_ET %s %d
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 21:23:31 EDT 2022
% Result : Theorem 0.35s 8.55s
% Output : CNFRefutation 0.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 16
% Syntax : Number of formulae : 63 ( 23 unt; 0 def)
% Number of atoms : 138 ( 24 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 131 ( 56 ~; 50 |; 9 &)
% ( 5 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-4 aty)
% Number of functors : 21 ( 21 usr; 5 con; 0-4 aty)
% Number of variables : 143 ( 33 sgn 81 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_rev__finite__subset,axiom,
! [X15,X14,X12] :
( c_Finite__Set_Ofinite(X12,X14)
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X12,tc_HOL_Obool),X15),X14))
=> c_Finite__Set_Ofinite(X12,X15) ) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_rev__finite__subset) ).
fof(fact_subset__UNIV,axiom,
! [X15,X12] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X12,tc_HOL_Obool),X15),c_Orderings_Otop__class_Otop(tc_fun(X12,tc_HOL_Obool)))),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_subset__UNIV) ).
fof(fact_less__irrefl__nat,axiom,
! [X24] : ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X24),X24)),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_less__irrefl__nat) ).
fof(fact_finite__nat__set__iff__bounded,axiom,
! [X51] :
( c_Finite__Set_Ofinite(tc_Nat_Onat,X51)
<=> ? [X5] :
! [X3] :
( hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X3),X51))
=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X3),X5)) ) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_finite__nat__set__iff__bounded) ).
fof(fact_finite__option__UNIV,axiom,
! [X12] :
( c_Finite__Set_Ofinite(tc_Option_Ooption(X12),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X12),tc_HOL_Obool)))
<=> c_Finite__Set_Ofinite(X12,c_Orderings_Otop__class_Otop(tc_fun(X12,tc_HOL_Obool))) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_finite__option__UNIV) ).
fof(fact_finite,axiom,
! [X15,X12] :
( class_Finite__Set_Ofinite(X12)
=> c_Finite__Set_Ofinite(X12,X15) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_finite) ).
fof(fact_gr__implies__not0,axiom,
! [X24,X23] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X23),X24))
=> X24 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_gr__implies__not0) ).
fof(fact_add__lessD1,axiom,
! [X25,X19,X20] :
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),X20),X19)),X25))
=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X20),X25)) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_add__lessD1) ).
fof(fact_plus__nat_Oadd__0,axiom,
! [X24] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X24) = X24,
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_plus__nat_Oadd__0) ).
fof(fact_mem__def,axiom,
! [X15,X9,X12] :
( hBOOL(hAPP(hAPP(c_member(X12),X9),X15))
<=> hBOOL(hAPP(X15,X9)) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_mem__def) ).
fof(arity_Product____Type__Ounit__Finite__Set_Ofinite,axiom,
class_Finite__Set_Ofinite(tc_Product__Type_Ounit),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',arity_Product____Type__Ounit__Finite__Set_Ofinite) ).
fof(fact_neq0__conv,axiom,
! [X10] :
( X10 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
<=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X10)) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_neq0__conv) ).
fof(fact_finite__imageD,axiom,
! [X15,X2,X18,X12] :
( c_Finite__Set_Ofinite(X12,c_Set_Oimage(X18,X12,X2,X15))
=> ( c_Fun_Oinj__on(X18,X12,X2,X15)
=> c_Finite__Set_Ofinite(X18,X15) ) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_finite__imageD) ).
fof(help_c__COMBK__1,axiom,
! [X82,X81,X18,X12] : hAPP(hAPP(c_COMBK(X12,X18),X81),X82) = X81,
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',help_c__COMBK__1) ).
fof(fact_inj__on__def,axiom,
! [X15,X2,X18,X12] :
( c_Fun_Oinj__on(X12,X18,X2,X15)
<=> ! [X3] :
( hBOOL(hAPP(hAPP(c_member(X12),X3),X15))
=> ! [X49] :
( hBOOL(hAPP(hAPP(c_member(X12),X49),X15))
=> ( hAPP(X2,X3) = hAPP(X2,X49)
=> X3 = X49 ) ) ) ),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_inj__on__def) ).
fof(fact_n_I1_J,axiom,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),v_n____),c_Finite__Set_Ocard(tc_Arrow__Order__Mirabelle_Oindi,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))))),
file('/export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p',fact_n_I1_J) ).
fof(c_0_16,plain,
! [X16,X17,X18] :
( ~ c_Finite__Set_Ofinite(X18,X17)
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X18,tc_HOL_Obool),X16),X17))
| c_Finite__Set_Ofinite(X18,X16) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_rev__finite__subset])]) ).
fof(c_0_17,plain,
! [X16,X17] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X17,tc_HOL_Obool),X16),c_Orderings_Otop__class_Otop(tc_fun(X17,tc_HOL_Obool)))),
inference(variable_rename,[status(thm)],[fact_subset__UNIV]) ).
fof(c_0_18,plain,
! [X25] : ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X25),X25)),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[fact_less__irrefl__nat])]) ).
fof(c_0_19,plain,
! [X52,X54,X52,X55] :
( ( ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X52)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X54),X52))
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X54),esk41_1(X52))) )
& ( hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk42_2(X52,X55)),X52))
| c_Finite__Set_Ofinite(tc_Nat_Onat,X52) )
& ( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),esk42_2(X52,X55)),X55))
| c_Finite__Set_Ofinite(tc_Nat_Onat,X52) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_finite__nat__set__iff__bounded])])])])])])]) ).
cnf(c_0_20,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)],[c_0_16]) ).
cnf(c_0_21,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_17]) ).
fof(c_0_22,plain,
! [X13,X13] :
( ( ~ c_Finite__Set_Ofinite(tc_Option_Ooption(X13),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X13),tc_HOL_Obool)))
| c_Finite__Set_Ofinite(X13,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool))) )
& ( ~ c_Finite__Set_Ofinite(X13,c_Orderings_Otop__class_Otop(tc_fun(X13,tc_HOL_Obool)))
| c_Finite__Set_Ofinite(tc_Option_Ooption(X13),c_Orderings_Otop__class_Otop(tc_fun(tc_Option_Ooption(X13),tc_HOL_Obool))) ) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_finite__option__UNIV])])])]) ).
fof(c_0_23,plain,
! [X16,X17] :
( ~ class_Finite__Set_Ofinite(X17)
| c_Finite__Set_Ofinite(X17,X16) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_finite])]) ).
fof(c_0_24,plain,
! [X25,X26] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X26),X25))
| X25 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_gr__implies__not0])])])]) ).
fof(c_0_25,plain,
! [X26,X27,X28] :
( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),X28),X27)),X26))
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X28),X26)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_add__lessD1])]) ).
fof(c_0_26,plain,
! [X25] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X25) = X25,
inference(variable_rename,[status(thm)],[fact_plus__nat_Oadd__0]) ).
cnf(c_0_27,plain,
~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X1)),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_28,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),esk41_1(X2)))
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X1),X2))
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X2) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
fof(c_0_29,plain,
! [X16,X17,X18,X16,X17,X18] :
( ( ~ hBOOL(hAPP(hAPP(c_member(X18),X17),X16))
| hBOOL(hAPP(X16,X17)) )
& ( ~ hBOOL(hAPP(X16,X17))
| hBOOL(hAPP(hAPP(c_member(X18),X17),X16)) ) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_mem__def])])])]) ).
cnf(c_0_30,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)],[c_0_20,c_0_21]) ).
cnf(c_0_31,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)],[c_0_22]) ).
cnf(c_0_32,plain,
( c_Finite__Set_Ofinite(X1,X2)
| ~ class_Finite__Set_Ofinite(X1) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_33,plain,
class_Finite__Set_Ofinite(tc_Product__Type_Ounit),
inference(split_conjunct,[status(thm)],[arity_Product____Type__Ounit__Finite__Set_Ofinite]) ).
cnf(c_0_34,plain,
( X1 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
cnf(c_0_35,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X1),X2))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),X1),X3)),X2)) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_36,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_37,plain,
( ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X1)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),esk41_1(X1)),X1)) ),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_38,plain,
( hBOOL(hAPP(hAPP(c_member(X1),X2),X3))
| ~ hBOOL(hAPP(X3,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
fof(c_0_39,plain,
! [X11,X11] :
( ( X11 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X11)) )
& ( ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X11))
| X11 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_neq0__conv])])])]) ).
fof(c_0_40,plain,
! [X19,X20,X21,X22] :
( ~ c_Finite__Set_Ofinite(X22,c_Set_Oimage(X21,X22,X20,X19))
| ~ c_Fun_Oinj__on(X21,X22,X20,X19)
| c_Finite__Set_Ofinite(X21,X19) ),
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(X1),X2)
| ~ c_Finite__Set_Ofinite(X1,c_Orderings_Otop__class_Otop(tc_fun(X1,tc_HOL_Obool))) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
cnf(c_0_42,plain,
c_Finite__Set_Ofinite(tc_Product__Type_Ounit,X1),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
fof(c_0_43,plain,
! [X83,X84,X85,X86] : hAPP(hAPP(c_COMBK(X86,X85),X84),X83) = X84,
inference(variable_rename,[status(thm)],[help_c__COMBK__1]) ).
fof(c_0_44,plain,
! [X50,X51,X52,X53,X54,X55,X50,X51,X52,X53] :
( ( ~ c_Fun_Oinj__on(X53,X52,X51,X50)
| ~ hBOOL(hAPP(hAPP(c_member(X53),X54),X50))
| ~ hBOOL(hAPP(hAPP(c_member(X53),X55),X50))
| hAPP(X51,X54) != hAPP(X51,X55)
| X54 = X55 )
& ( hBOOL(hAPP(hAPP(c_member(X53),esk25_4(X50,X51,X52,X53)),X50))
| c_Fun_Oinj__on(X53,X52,X51,X50) )
& ( hBOOL(hAPP(hAPP(c_member(X53),esk26_4(X50,X51,X52,X53)),X50))
| c_Fun_Oinj__on(X53,X52,X51,X50) )
& ( hAPP(X51,esk25_4(X50,X51,X52,X53)) = hAPP(X51,esk26_4(X50,X51,X52,X53))
| c_Fun_Oinj__on(X53,X52,X51,X50) )
& ( esk25_4(X50,X51,X52,X53) != esk26_4(X50,X51,X52,X53)
| c_Fun_Oinj__on(X53,X52,X51,X50) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fact_inj__on__def])])])])])])]) ).
cnf(c_0_45,plain,
( esk41_1(X1) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X1)
| ~ hBOOL(hAPP(hAPP(c_member(tc_Nat_Onat),X2),X1)) ),
inference(spm,[status(thm)],[c_0_34,c_0_28]) ).
cnf(c_0_46,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X1))
| ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),X2),X1)) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_47,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),v_n____),c_Finite__Set_Ocard(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)],[fact_n_I1_J]) ).
cnf(c_0_48,plain,
( ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X1)
| ~ hBOOL(hAPP(X1,esk41_1(X1))) ),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_49,plain,
( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),X1))
| X1 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_50,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)],[c_0_40]) ).
cnf(c_0_51,plain,
c_Finite__Set_Ofinite(tc_Option_Ooption(tc_Product__Type_Ounit),X1),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_52,plain,
hAPP(hAPP(c_COMBK(X1,X2),X3),X4) = X3,
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_53,plain,
( c_Fun_Oinj__on(X1,X2,X3,X4)
| hAPP(X3,esk25_4(X4,X3,X2,X1)) = hAPP(X3,esk26_4(X4,X3,X2,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_54,plain,
( c_Fun_Oinj__on(X1,X2,X3,X4)
| esk25_4(X4,X3,X2,X1) != esk26_4(X4,X3,X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_55,plain,
( esk41_1(X1) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,X1)
| ~ hBOOL(hAPP(X1,X2)) ),
inference(spm,[status(thm)],[c_0_45,c_0_38]) ).
cnf(c_0_56,plain,
hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),c_Finite__Set_Ocard(tc_Arrow__Order__Mirabelle_Oindi,c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oindi,tc_HOL_Obool))))),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_57,plain,
( esk41_1(hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Finite__Set_Ofinite(tc_Nat_Onat,hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) ),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
cnf(c_0_58,plain,
( c_Finite__Set_Ofinite(X1,X2)
| ~ c_Fun_Oinj__on(X1,tc_Option_Ooption(tc_Product__Type_Ounit),X3,X2) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_59,plain,
c_Fun_Oinj__on(X1,X2,c_COMBK(X3,X4),X5),
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_60,plain,
~ c_Finite__Set_Ofinite(tc_Nat_Onat,hAPP(c_Orderings_Oord__class_Oless(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_56]),c_0_57]) ).
cnf(c_0_61,plain,
c_Finite__Set_Ofinite(X1,X2),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_62,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60,c_0_61])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SCT165+1 : TPTP v8.1.0. Released v5.2.0.
% 0.08/0.14 % Command : run_ET %s %d
% 0.14/0.36 % Computer : n021.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Fri Jul 1 22:17:44 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.35/8.55 # Running protocol protocol_eprover_63dc1b1eb7d762c2f3686774d32795976f981b97 for 23 seconds:
% 0.35/8.55 # Preprocessing time : 0.419 s
% 0.35/8.55
% 0.35/8.55 # Proof found!
% 0.35/8.55 # SZS status Theorem
% 0.35/8.55 # SZS output start CNFRefutation
% See solution above
% 0.35/8.55 # Proof object total steps : 63
% 0.35/8.55 # Proof object clause steps : 33
% 0.35/8.55 # Proof object formula steps : 30
% 0.35/8.55 # Proof object conjectures : 0
% 0.35/8.55 # Proof object clause conjectures : 0
% 0.35/8.55 # Proof object formula conjectures : 0
% 0.35/8.55 # Proof object initial clauses used : 17
% 0.35/8.55 # Proof object initial formulas used : 16
% 0.35/8.55 # Proof object generating inferences : 15
% 0.35/8.55 # Proof object simplifying inferences : 5
% 0.35/8.55 # Training examples: 0 positive, 0 negative
% 0.35/8.55 # Parsed axioms : 533
% 0.35/8.55 # Removed by relevancy pruning/SinE : 0
% 0.35/8.55 # Initial clauses : 927
% 0.35/8.55 # Removed in clause preprocessing : 100
% 0.35/8.55 # Initial clauses in saturation : 827
% 0.35/8.55 # Processed clauses : 12665
% 0.35/8.55 # ...of these trivial : 313
% 0.35/8.55 # ...subsumed : 8322
% 0.35/8.55 # ...remaining for further processing : 4030
% 0.35/8.55 # Other redundant clauses eliminated : 481
% 0.35/8.55 # Clauses deleted for lack of memory : 60985
% 0.35/8.55 # Backward-subsumed : 136
% 0.35/8.55 # Backward-rewritten : 768
% 0.35/8.55 # Generated clauses : 185709
% 0.35/8.55 # ...of the previous two non-trivial : 174244
% 0.35/8.55 # Contextual simplify-reflections : 3850
% 0.35/8.55 # Paramodulations : 185089
% 0.35/8.55 # Factorizations : 15
% 0.35/8.55 # Equation resolutions : 610
% 0.35/8.55 # Current number of processed clauses : 3061
% 0.35/8.55 # Positive orientable unit clauses : 467
% 0.35/8.55 # Positive unorientable unit clauses: 36
% 0.35/8.55 # Negative unit clauses : 191
% 0.35/8.55 # Non-unit-clauses : 2367
% 0.35/8.55 # Current number of unprocessed clauses: 90251
% 0.35/8.55 # ...number of literals in the above : 295152
% 0.35/8.55 # Current number of archived formulas : 0
% 0.35/8.55 # Current number of archived clauses : 905
% 0.35/8.55 # Clause-clause subsumption calls (NU) : 4296689
% 0.35/8.55 # Rec. Clause-clause subsumption calls : 1283409
% 0.35/8.55 # Non-unit clause-clause subsumptions : 8345
% 0.35/8.55 # Unit Clause-clause subsumption calls : 62460
% 0.35/8.55 # Rewrite failures with RHS unbound : 431
% 0.35/8.55 # BW rewrite match attempts : 33076
% 0.35/8.55 # BW rewrite match successes : 727
% 0.35/8.55 # Condensation attempts : 0
% 0.35/8.55 # Condensation successes : 0
% 0.35/8.55 # Termbank termtop insertions : 10349757
% 0.35/8.55
% 0.35/8.55 # -------------------------------------------------
% 0.35/8.55 # User time : 7.131 s
% 0.35/8.55 # System time : 0.092 s
% 0.35/8.55 # Total time : 7.223 s
% 0.35/8.55 # Maximum resident set size: 149932 pages
% 0.37/23.49 eprover: CPU time limit exceeded, terminating
% 0.37/23.49 eprover: CPU time limit exceeded, terminating
% 0.37/23.50 eprover: CPU time limit exceeded, terminating
% 0.37/23.51 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.51 eprover: No such file or directory
% 0.37/23.51 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.51 eprover: No such file or directory
% 0.37/23.51 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.51 eprover: No such file or directory
% 0.37/23.52 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.52 eprover: No such file or directory
% 0.37/23.52 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.52 eprover: No such file or directory
% 0.37/23.52 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.52 eprover: No such file or directory
% 0.37/23.52 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.52 eprover: No such file or directory
% 0.37/23.52 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.52 eprover: No such file or directory
% 0.37/23.53 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.53 eprover: No such file or directory
% 0.37/23.53 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.53 eprover: No such file or directory
% 0.37/23.53 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.53 eprover: No such file or directory
% 0.37/23.53 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.53 eprover: No such file or directory
% 0.37/23.53 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.53 eprover: No such file or directory
% 0.37/23.53 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.53 eprover: No such file or directory
% 0.37/23.54 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.54 eprover: No such file or directory
% 0.37/23.54 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.54 eprover: No such file or directory
% 0.37/23.54 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.54 eprover: No such file or directory
% 0.37/23.54 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.54 eprover: No such file or directory
% 0.37/23.54 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.54 eprover: No such file or directory
% 0.37/23.54 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.54 eprover: No such file or directory
% 0.37/23.55 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.55 eprover: No such file or directory
% 0.37/23.55 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.55 eprover: No such file or directory
% 0.37/23.55 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.55 eprover: No such file or directory
% 0.37/23.55 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.55 eprover: No such file or directory
% 0.37/23.55 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.55 eprover: No such file or directory
% 0.37/23.55 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.55 eprover: No such file or directory
% 0.37/23.56 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.56 eprover: No such file or directory
% 0.37/23.56 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.56 eprover: No such file or directory
% 0.37/23.56 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.56 eprover: No such file or directory
% 0.37/23.56 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.56 eprover: No such file or directory
% 0.37/23.56 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.56 eprover: No such file or directory
% 0.37/23.56 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 0.37/23.56 eprover: No such file or directory
% 0.37/23.57 eprover: Cannot stat file /export/starexec/sandbox2/solver/bin/../tmp/theBenchmark.p
% 0.37/23.57 eprover: No such file or directory
%------------------------------------------------------------------------------