%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : KRS102+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 01:01:30 PM UTC 2026
% Result : Unsatisfiable 0.15s 5.87s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 27
% Syntax : Number of formulae : 179 ( 28 unt; 0 def)
% Number of atoms : 454 ( 390 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 352 ( 77 ~; 248 |; 18 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 36 ( 0 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_8,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iF
| X3 = iT ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_8) ).
fof(axiom_77,axiom,
iT != iF,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_77) ).
fof(axiom_6,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iminus5
| X3 = iplus5 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
fof(axiom_9,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iminus8
| X3 = iplus8 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
fof(axiom_4,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iminus2
| X3 = iplus2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
fof(axiom_49,axiom,
( iT = iminus3
| iT = iminus8
| iT = iplus5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_49) ).
fof(axiom_3,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iplus4
| X3 = iminus4 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
fof(axiom_7,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iminus3
| X3 = iplus3 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
fof(axiom_42,axiom,
( iT = iminus3
| iT = iplus2
| iT = iplus8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_42) ).
fof(axiom_45,axiom,
( iT = iminus3
| iT = iminus8
| iT = iminus5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_45) ).
fof(axiom_5,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iminus7
| X3 = iplus7 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
fof(axiom_10,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iplus6
| X3 = iminus6 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_10) ).
fof(axiom_22,axiom,
( iT = iplus4
| iT = iplus6
| iT = iplus3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_22) ).
fof(axiom_39,axiom,
( iT = iminus4
| iT = iplus6
| iT = iplus3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_39) ).
fof(axiom_11,axiom,
! [X3] :
( cTorF(X3)
<=> ( X3 = iplus9
| X3 = iminus9 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_11) ).
fof(axiom_58,axiom,
( iT = iplus9
| iT = iplus7
| iT = iminus4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_58) ).
fof(axiom_14,axiom,
( iT = iminus7
| iT = iplus9
| iT = iminus6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_14) ).
fof(axiom_51,axiom,
( iT = iplus9
| iT = iminus2
| iT = iplus6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_51) ).
fof(axiom_18,axiom,
( iT = iplus4
| iT = iminus9
| iT = iplus3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(axiom_15,axiom,
( iT = iplus7
| iT = iminus3
| iT = iplus8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_15) ).
fof(axiom_46,axiom,
( iT = iplus4
| iT = iplus9
| iT = iplus3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_46) ).
fof(axiom_40,axiom,
( iT = iminus4
| iT = iminus9
| iT = iminus8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_40) ).
fof(axiom_36,axiom,
( iT = iminus7
| iT = iminus3
| iT = iminus4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_36) ).
fof(axiom_31,axiom,
( iT = iminus4
| iT = iplus2
| iT = iplus8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_31) ).
fof(axiom_26,axiom,
( iT = iminus2
| iT = iminus9
| iT = iplus3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_26) ).
fof(axiom_56,axiom,
( iT = iplus4
| iT = iminus2
| iT = iminus6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_56) ).
fof(axiom_27,axiom,
( iT = iminus7
| iT = iminus2
| iT = iplus6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_27) ).
fof(c_0_27,plain,
! [X22] :
( ( cTorF(X22)
| X22 != iF )
& ( cTorF(X22)
| X22 != iT )
& ( X22 = iF
| X22 = iT
| ~ cTorF(X22) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_8])])])]) ).
fof(c_0_28,plain,
iT != iF,
inference(fof_simplification,[status(thm)],[axiom_77]) ).
fof(c_0_29,plain,
! [X20] :
( ( cTorF(X20)
| X20 != iminus5 )
& ( cTorF(X20)
| X20 != iplus5 )
& ( X20 = iminus5
| X20 = iplus5
| ~ cTorF(X20) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_6])])])]) ).
cnf(c_0_30,plain,
( X1 != iF
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
fof(c_0_31,plain,
! [X23] :
( ( cTorF(X23)
| X23 != iminus8 )
& ( cTorF(X23)
| X23 != iplus8 )
& ( X23 = iminus8
| X23 = iplus8
| ~ cTorF(X23) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_9])])])]) ).
fof(c_0_32,plain,
iT != iF,
inference(fof_nnf,[status(thm)],[c_0_28]) ).
cnf(c_0_33,plain,
( ~ cTorF(X1)
| X1 = iminus5
| X1 = iplus5 ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_34,plain,
cTorF(iF),
inference(er,[status(thm)],[c_0_30]) ).
cnf(c_0_35,plain,
( ~ cTorF(X1)
| X1 = iminus8
| X1 = iplus8 ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_36,plain,
iT != iF,
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_37,plain,
( iF = iplus5
| iF = iminus5 ),
inference(spm,[status(thm)],[c_0_33,c_0_34]) ).
fof(c_0_38,plain,
! [X18] :
( ( cTorF(X18)
| X18 != iminus2 )
& ( cTorF(X18)
| X18 != iplus2 )
& ( X18 = iminus2
| X18 = iplus2
| ~ cTorF(X18) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_4])])])]) ).
cnf(c_0_39,plain,
( iF = iplus8
| iF = iminus8 ),
inference(spm,[status(thm)],[c_0_35,c_0_34]) ).
cnf(c_0_40,plain,
( iplus5 != iT
| iF = iminus5 ),
inference(spm,[status(thm)],[c_0_36,c_0_37]) ).
cnf(c_0_41,plain,
( iT = iminus3
| iT = iminus8
| iT = iplus5 ),
inference(split_conjunct,[status(thm)],[axiom_49]) ).
fof(c_0_42,plain,
! [X17] :
( ( cTorF(X17)
| X17 != iplus4 )
& ( cTorF(X17)
| X17 != iminus4 )
& ( X17 = iplus4
| X17 = iminus4
| ~ cTorF(X17) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_3])])])]) ).
fof(c_0_43,plain,
! [X21] :
( ( cTorF(X21)
| X21 != iminus3 )
& ( cTorF(X21)
| X21 != iplus3 )
& ( X21 = iminus3
| X21 = iplus3
| ~ cTorF(X21) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_7])])])]) ).
cnf(c_0_44,plain,
( X1 != iplus2
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_45,plain,
( iplus8 != iT
| iF = iminus8 ),
inference(spm,[status(thm)],[c_0_36,c_0_39]) ).
cnf(c_0_46,plain,
( iT = iminus3
| iT = iplus2
| iT = iplus8 ),
inference(split_conjunct,[status(thm)],[axiom_42]) ).
cnf(c_0_47,plain,
( iF = iminus5
| iminus3 = iT
| iminus8 = iT ),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_48,plain,
( iT = iminus3
| iT = iminus8
| iT = iminus5 ),
inference(split_conjunct,[status(thm)],[axiom_45]) ).
cnf(c_0_49,plain,
( ~ cTorF(X1)
| X1 = iplus4
| X1 = iminus4 ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
fof(c_0_50,plain,
! [X19] :
( ( cTorF(X19)
| X19 != iminus7 )
& ( cTorF(X19)
| X19 != iplus7 )
& ( X19 = iminus7
| X19 = iplus7
| ~ cTorF(X19) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_5])])])]) ).
fof(c_0_51,plain,
! [X24] :
( ( cTorF(X24)
| X24 != iplus6 )
& ( cTorF(X24)
| X24 != iminus6 )
& ( X24 = iplus6
| X24 = iminus6
| ~ cTorF(X24) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_10])])])]) ).
cnf(c_0_52,plain,
( ~ cTorF(X1)
| X1 = iminus2
| X1 = iplus2 ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_53,plain,
( ~ cTorF(X1)
| X1 = iminus3
| X1 = iplus3 ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_54,plain,
cTorF(iplus2),
inference(er,[status(thm)],[c_0_44]) ).
cnf(c_0_55,plain,
( iF = iminus8
| iplus2 = iT
| iminus3 = iT ),
inference(spm,[status(thm)],[c_0_45,c_0_46]) ).
cnf(c_0_56,plain,
( iminus8 = iT
| iminus3 = iT ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_47]),c_0_48]) ).
cnf(c_0_57,plain,
( iF = iminus4
| iF = iplus4 ),
inference(spm,[status(thm)],[c_0_49,c_0_34]) ).
cnf(c_0_58,plain,
( ~ cTorF(X1)
| X1 = iminus7
| X1 = iplus7 ),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
cnf(c_0_59,plain,
( ~ cTorF(X1)
| X1 = iplus6
| X1 = iminus6 ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_60,plain,
( iF = iplus2
| iF = iminus2 ),
inference(spm,[status(thm)],[c_0_52,c_0_34]) ).
cnf(c_0_61,plain,
( iplus2 = iplus3
| iminus3 = iplus2 ),
inference(spm,[status(thm)],[c_0_53,c_0_54]) ).
cnf(c_0_62,plain,
( iminus3 = iT
| iplus2 = iT ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_55]),c_0_56]) ).
cnf(c_0_63,plain,
( iplus4 != iT
| iF = iminus4 ),
inference(spm,[status(thm)],[c_0_36,c_0_57]) ).
cnf(c_0_64,plain,
( iT = iplus4
| iT = iplus6
| iT = iplus3 ),
inference(split_conjunct,[status(thm)],[axiom_22]) ).
cnf(c_0_65,plain,
( X1 != iT
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_66,plain,
( iF = iplus7
| iF = iminus7 ),
inference(spm,[status(thm)],[c_0_58,c_0_34]) ).
cnf(c_0_67,plain,
( iF = iminus6
| iF = iplus6 ),
inference(spm,[status(thm)],[c_0_59,c_0_34]) ).
cnf(c_0_68,plain,
( iplus2 != iminus2
| iF = iminus2 ),
inference(ef,[status(thm)],[c_0_60]) ).
cnf(c_0_69,plain,
( iplus2 = iT
| iplus2 = iplus3 ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
cnf(c_0_70,plain,
( iplus2 != iT
| iF = iminus2 ),
inference(spm,[status(thm)],[c_0_36,c_0_60]) ).
cnf(c_0_71,plain,
( iF = iminus4
| iplus3 = iT
| iplus6 = iT ),
inference(spm,[status(thm)],[c_0_63,c_0_64]) ).
cnf(c_0_72,plain,
( iT = iminus4
| iT = iplus6
| iT = iplus3 ),
inference(split_conjunct,[status(thm)],[axiom_39]) ).
fof(c_0_73,plain,
! [X25] :
( ( cTorF(X25)
| X25 != iplus9 )
& ( cTorF(X25)
| X25 != iminus9 )
& ( X25 = iplus9
| X25 = iminus9
| ~ cTorF(X25) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_11])])])]) ).
cnf(c_0_74,plain,
cTorF(iT),
inference(er,[status(thm)],[c_0_65]) ).
cnf(c_0_75,plain,
( iplus7 != iT
| iF = iminus7 ),
inference(spm,[status(thm)],[c_0_36,c_0_66]) ).
cnf(c_0_76,plain,
( iT = iplus9
| iT = iplus7
| iT = iminus4 ),
inference(split_conjunct,[status(thm)],[axiom_58]) ).
cnf(c_0_77,plain,
( iminus6 != iT
| iF = iplus6 ),
inference(spm,[status(thm)],[c_0_36,c_0_67]) ).
cnf(c_0_78,plain,
( iT = iminus7
| iT = iplus9
| iT = iminus6 ),
inference(split_conjunct,[status(thm)],[axiom_14]) ).
cnf(c_0_79,plain,
( iminus2 != iplus3
| iF = iminus2 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_69]),c_0_70]) ).
cnf(c_0_80,plain,
( iT = iplus9
| iT = iminus2
| iT = iplus6 ),
inference(split_conjunct,[status(thm)],[axiom_51]) ).
cnf(c_0_81,plain,
( iplus6 = iT
| iplus3 = iT ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_71]),c_0_72]) ).
cnf(c_0_82,plain,
( ~ cTorF(X1)
| X1 = iplus9
| X1 = iminus9 ),
inference(split_conjunct,[status(thm)],[c_0_73]) ).
cnf(c_0_83,plain,
( iminus4 = iT
| iplus4 = iT ),
inference(spm,[status(thm)],[c_0_49,c_0_74]) ).
cnf(c_0_84,plain,
( iF = iminus7
| iminus4 = iT
| iplus9 = iT ),
inference(spm,[status(thm)],[c_0_75,c_0_76]) ).
cnf(c_0_85,plain,
( iF = iplus6
| iminus7 = iT
| iplus9 = iT ),
inference(spm,[status(thm)],[c_0_77,c_0_78]) ).
cnf(c_0_86,plain,
( iplus6 = iT
| iplus9 = iT ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_79,c_0_80]),c_0_36]),c_0_81]) ).
cnf(c_0_87,plain,
( iF = iminus9
| iF = iplus9 ),
inference(spm,[status(thm)],[c_0_82,c_0_34]) ).
cnf(c_0_88,plain,
( iF = iminus4
| iminus4 = iT ),
inference(spm,[status(thm)],[c_0_63,c_0_83]) ).
cnf(c_0_89,plain,
( iminus7 != iT
| iplus9 = iT
| iminus4 = iT ),
inference(spm,[status(thm)],[c_0_36,c_0_84]) ).
cnf(c_0_90,plain,
( iplus9 = iT
| iminus7 = iT ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_85]),c_0_86]) ).
cnf(c_0_91,plain,
( X1 != iplus3
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_92,plain,
( iminus9 != iT
| iF = iplus9 ),
inference(spm,[status(thm)],[c_0_36,c_0_87]) ).
cnf(c_0_93,plain,
( iT = iplus4
| iT = iminus9
| iT = iplus3 ),
inference(split_conjunct,[status(thm)],[axiom_18]) ).
cnf(c_0_94,plain,
( X1 != iminus2
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_95,plain,
( iminus4 = iT
| iminus9 = iminus4
| iF = iplus9 ),
inference(spm,[status(thm)],[c_0_88,c_0_87]) ).
cnf(c_0_96,plain,
( iminus4 = iT
| iplus9 = iT ),
inference(spm,[status(thm)],[c_0_89,c_0_90]) ).
cnf(c_0_97,plain,
( iT = iplus7
| iT = iminus3
| iT = iplus8 ),
inference(split_conjunct,[status(thm)],[axiom_15]) ).
cnf(c_0_98,plain,
cTorF(iplus3),
inference(er,[status(thm)],[c_0_91]) ).
cnf(c_0_99,plain,
( iF = iplus9
| iplus4 = iT
| iplus3 = iT ),
inference(spm,[status(thm)],[c_0_92,c_0_93]) ).
cnf(c_0_100,plain,
( iT = iplus4
| iT = iplus9
| iT = iplus3 ),
inference(split_conjunct,[status(thm)],[axiom_46]) ).
cnf(c_0_101,plain,
cTorF(iminus2),
inference(er,[status(thm)],[c_0_94]) ).
cnf(c_0_102,plain,
( iminus4 = iT
| iplus8 = iminus4
| iF = iminus8 ),
inference(spm,[status(thm)],[c_0_88,c_0_39]) ).
cnf(c_0_103,plain,
( iT = iminus4
| iT = iminus9
| iT = iminus8 ),
inference(split_conjunct,[status(thm)],[axiom_40]) ).
cnf(c_0_104,plain,
( iminus9 = iminus4
| iminus4 = iT ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_95]),c_0_96]) ).
cnf(c_0_105,plain,
( iF = iminus7
| iminus3 = iT
| iplus8 = iT ),
inference(spm,[status(thm)],[c_0_75,c_0_97]) ).
cnf(c_0_106,plain,
( iplus2 = iminus4
| iplus2 = iplus4 ),
inference(spm,[status(thm)],[c_0_49,c_0_54]) ).
cnf(c_0_107,plain,
( iplus3 = iminus4
| iplus4 = iplus3 ),
inference(spm,[status(thm)],[c_0_49,c_0_98]) ).
cnf(c_0_108,plain,
( iplus3 = iT
| iplus4 = iT ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_99]),c_0_100]) ).
cnf(c_0_109,plain,
( iminus2 = iminus4
| iminus2 = iplus4 ),
inference(spm,[status(thm)],[c_0_49,c_0_101]) ).
cnf(c_0_110,plain,
( X1 != iminus4
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
cnf(c_0_111,plain,
( iminus8 != iT
| iplus8 = iminus4
| iminus4 = iT ),
inference(spm,[status(thm)],[c_0_36,c_0_102]) ).
cnf(c_0_112,plain,
( iminus4 = iT
| iminus8 = iT ),
inference(spm,[status(thm)],[c_0_103,c_0_104]) ).
cnf(c_0_113,plain,
( iminus7 != iT
| iplus8 = iT
| iminus3 = iT ),
inference(spm,[status(thm)],[c_0_36,c_0_105]) ).
cnf(c_0_114,plain,
( iT = iminus7
| iT = iminus3
| iT = iminus4 ),
inference(split_conjunct,[status(thm)],[axiom_36]) ).
cnf(c_0_115,plain,
( iplus4 != iT
| iF = iminus2
| iplus2 = iminus4 ),
inference(spm,[status(thm)],[c_0_70,c_0_106]) ).
cnf(c_0_116,plain,
( iplus3 = iT
| iplus3 = iminus4 ),
inference(spm,[status(thm)],[c_0_107,c_0_108]) ).
cnf(c_0_117,plain,
( iplus4 != iplus3
| iF = iplus4
| iminus2 = iminus4 ),
inference(spm,[status(thm)],[c_0_79,c_0_109]) ).
cnf(c_0_118,plain,
cTorF(iminus4),
inference(er,[status(thm)],[c_0_110]) ).
cnf(c_0_119,plain,
( iminus4 = iT
| iplus8 = iminus4 ),
inference(spm,[status(thm)],[c_0_111,c_0_112]) ).
cnf(c_0_120,plain,
( iminus3 = iT
| iplus8 = iT
| iminus4 = iT ),
inference(spm,[status(thm)],[c_0_113,c_0_114]) ).
cnf(c_0_121,plain,
( iplus2 = iminus4
| iF = iminus2
| iplus3 = iminus4 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_115,c_0_107]),c_0_116]) ).
cnf(c_0_122,plain,
( iminus2 = iminus4
| iF = iplus3
| iplus3 = iminus4 ),
inference(spm,[status(thm)],[c_0_117,c_0_107]) ).
cnf(c_0_123,plain,
( iplus3 = iminus4
| iminus3 = iminus4 ),
inference(spm,[status(thm)],[c_0_53,c_0_118]) ).
cnf(c_0_124,plain,
( iminus4 = iT
| iminus3 = iT ),
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
cnf(c_0_125,plain,
( iminus2 != iT
| iplus3 = iminus4
| iplus2 = iminus4 ),
inference(spm,[status(thm)],[c_0_36,c_0_121]) ).
cnf(c_0_126,plain,
( iplus3 = iminus4
| iminus2 = iminus4 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_122]),c_0_116]) ).
cnf(c_0_127,plain,
( iminus4 = iT
| iplus3 = iminus4 ),
inference(spm,[status(thm)],[c_0_123,c_0_124]) ).
cnf(c_0_128,plain,
( iT = iminus4
| iT = iplus2
| iT = iplus8 ),
inference(split_conjunct,[status(thm)],[axiom_31]) ).
cnf(c_0_129,plain,
( iplus2 = iplus3
| iminus2 = iplus3 ),
inference(spm,[status(thm)],[c_0_52,c_0_98]) ).
cnf(c_0_130,plain,
( iplus2 = iminus4
| iplus3 = iminus4 ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_125,c_0_126]),c_0_127]) ).
cnf(c_0_131,plain,
( iF = iminus8
| iminus4 = iT
| iplus2 = iT ),
inference(spm,[status(thm)],[c_0_45,c_0_128]) ).
cnf(c_0_132,plain,
( iminus2 = iplus3
| iplus3 = iminus4 ),
inference(spm,[status(thm)],[c_0_129,c_0_130]) ).
cnf(c_0_133,plain,
( iminus8 != iT
| iplus2 = iT
| iminus4 = iT ),
inference(spm,[status(thm)],[c_0_36,c_0_131]) ).
cnf(c_0_134,plain,
( X1 != iminus8
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_135,plain,
( iplus3 != iT
| iplus2 = iT ),
inference(ef,[status(thm)],[c_0_69]) ).
cnf(c_0_136,plain,
iplus3 = iminus4,
inference(spm,[status(thm)],[c_0_126,c_0_132]) ).
cnf(c_0_137,plain,
( iminus4 = iT
| iplus2 = iT ),
inference(spm,[status(thm)],[c_0_133,c_0_112]) ).
cnf(c_0_138,plain,
cTorF(iminus8),
inference(er,[status(thm)],[c_0_134]) ).
cnf(c_0_139,plain,
( iT = iminus2
| iT = iminus9
| iT = iplus3 ),
inference(split_conjunct,[status(thm)],[axiom_26]) ).
cnf(c_0_140,plain,
iplus2 = iT,
inference(csr,[status(thm)],[inference(rw,[status(thm)],[c_0_135,c_0_136]),c_0_137]) ).
cnf(c_0_141,plain,
( iplus2 = iT
| iminus2 = iT ),
inference(spm,[status(thm)],[c_0_52,c_0_74]) ).
cnf(c_0_142,plain,
( iminus8 = iplus3
| iminus3 = iminus8 ),
inference(spm,[status(thm)],[c_0_53,c_0_138]) ).
cnf(c_0_143,plain,
( iF = iplus3
| iF = iminus3 ),
inference(spm,[status(thm)],[c_0_53,c_0_34]) ).
cnf(c_0_144,plain,
( iF = iplus9
| iminus2 = iT
| iplus3 = iT ),
inference(spm,[status(thm)],[c_0_92,c_0_139]) ).
cnf(c_0_145,plain,
iF = iminus2,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_70,c_0_140])]) ).
cnf(c_0_146,plain,
( X1 != iminus3
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_147,plain,
( iF = iminus2
| iminus2 = iT ),
inference(spm,[status(thm)],[c_0_70,c_0_141]) ).
cnf(c_0_148,plain,
( iminus8 = iT
| iminus8 = iplus3 ),
inference(spm,[status(thm)],[c_0_142,c_0_56]) ).
cnf(c_0_149,plain,
( iminus3 != iT
| iF = iplus3 ),
inference(spm,[status(thm)],[c_0_36,c_0_143]) ).
cnf(c_0_150,plain,
( iplus9 != iT
| iplus3 = iT
| iminus2 = iT ),
inference(spm,[status(thm)],[c_0_36,c_0_144]) ).
cnf(c_0_151,plain,
iminus2 != iT,
inference(rw,[status(thm)],[c_0_36,c_0_145]) ).
cnf(c_0_152,plain,
( iT = iplus4
| iT = iminus2
| iT = iminus6 ),
inference(split_conjunct,[status(thm)],[axiom_56]) ).
cnf(c_0_153,plain,
( ~ cTorF(X1)
| X1 = iF
| X1 = iT ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_154,plain,
cTorF(iminus3),
inference(er,[status(thm)],[c_0_146]) ).
cnf(c_0_155,plain,
( iminus2 = iT
| iplus8 = iminus2
| iF = iminus8 ),
inference(spm,[status(thm)],[c_0_147,c_0_39]) ).
cnf(c_0_156,plain,
( iplus3 != iT
| iminus8 = iT ),
inference(ef,[status(thm)],[c_0_148]) ).
cnf(c_0_157,plain,
( iminus3 != iT
| iminus2 = iminus4 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_149,c_0_136]),c_0_145]) ).
cnf(c_0_158,plain,
iminus4 = iT,
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_150,c_0_136]),c_0_151]),c_0_96]) ).
cnf(c_0_159,plain,
( X1 != iplus6
| cTorF(X1) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
cnf(c_0_160,plain,
( iF = iplus6
| iplus4 = iT
| iminus2 = iT ),
inference(spm,[status(thm)],[c_0_77,c_0_152]) ).
cnf(c_0_161,plain,
( iplus4 != iT
| iminus2 = iminus4 ),
inference(rw,[status(thm)],[c_0_63,c_0_145]) ).
cnf(c_0_162,plain,
( iminus3 = iT
| iF = iminus3 ),
inference(spm,[status(thm)],[c_0_153,c_0_154]) ).
cnf(c_0_163,plain,
( iminus8 != iT
| iplus8 = iminus2
| iminus2 = iT ),
inference(spm,[status(thm)],[c_0_36,c_0_155]) ).
cnf(c_0_164,plain,
iminus8 = iT,
inference(csr,[status(thm)],[inference(rw,[status(thm)],[c_0_156,c_0_136]),c_0_112]) ).
cnf(c_0_165,plain,
iminus3 != iT,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_157,c_0_158]),c_0_151]) ).
cnf(c_0_166,plain,
iminus2 = iplus4,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_109,c_0_158]),c_0_151]) ).
cnf(c_0_167,plain,
cTorF(iplus6),
inference(er,[status(thm)],[c_0_159]) ).
cnf(c_0_168,plain,
( iplus6 != iT
| iminus2 = iT
| iplus4 = iT ),
inference(spm,[status(thm)],[c_0_36,c_0_160]) ).
cnf(c_0_169,plain,
iplus4 != iT,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_161,c_0_158]),c_0_151]) ).
cnf(c_0_170,plain,
( iminus7 = iminus3
| iminus3 = iT
| iplus8 = iT ),
inference(spm,[status(thm)],[c_0_162,c_0_105]) ).
cnf(c_0_171,plain,
iplus8 = iminus2,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_163,c_0_164])]),c_0_151]) ).
cnf(c_0_172,plain,
iminus3 = iplus4,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_162,c_0_165]),c_0_145]),c_0_166]) ).
cnf(c_0_173,plain,
( iplus6 = iT
| iF = iplus6 ),
inference(spm,[status(thm)],[c_0_153,c_0_167]) ).
cnf(c_0_174,plain,
iplus6 != iT,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_168,c_0_166])]),c_0_169]) ).
cnf(c_0_175,plain,
( iT = iminus7
| iT = iminus2
| iT = iplus6 ),
inference(split_conjunct,[status(thm)],[axiom_27]) ).
cnf(c_0_176,plain,
iminus7 = iplus4,
inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_170,c_0_165]),c_0_171]),c_0_151]),c_0_172]) ).
cnf(c_0_177,plain,
iplus4 = iplus6,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_173,c_0_174]),c_0_145]),c_0_166]) ).
cnf(c_0_178,plain,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[c_0_175,c_0_151]),c_0_176]),c_0_177])]),c_0_174]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS102+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/5.38 % Computer : n009.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sun Sep 20 22:53:33 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/5.43 Running first-order theorem proving
% 0.15/5.43 Running: /export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p
% 0.15/5.87 % Version: 3.5.1
% 0.15/5.87 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.15/5.87 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/5.87 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.15/5.87 % Starting new_bool_3 with 300s (1) cores
% 0.15/5.87 % Starting new_bool_1 with 300s (1) cores
% 0.15/5.87 % Starting sh5l with 300s (1) cores
% 0.15/5.87 % new_bool_1 with pid 228875 completed with status 9
% 0.15/5.87 % sh5l with pid 228876 completed with status 9
% 0.15/5.87 % new_bool_3 with pid 228874 completed with status 9
% 0.15/5.87 % C07_19_nc_SOS_SAT001_MinMin_p005000_rr with pid 228873 completed with status 0
% 0.15/5.87 % Result found by C07_19_nc_SOS_SAT001_MinMin_p005000_rr
% 0.15/5.87 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.15/5.87 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/5.87 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.15/5.87 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.15/5.87 % No SInE strategy applied
% 0.15/5.87 % Search class: FGHSF-FFMM00-SFFFFFNN
% 0.15/5.87 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.15/5.87 % Starting SubtermCWHack with 136s (1) cores
% 0.15/5.87 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 0.15/5.87 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S0Y with 136s (1) cores
% 0.15/5.87 % Starting new_bool_3 with 136s (1) cores
% 0.15/5.87 % Starting new_bool_1 with 136s (1) cores
% 0.15/5.87 % new_bool_3 with pid 228889 completed with status 0
% 0.15/5.87 % Result found by new_bool_3
% 0.15/5.87 % Preprocessing class: FSLSSMSMSSSNFFN.
% 0.15/5.87 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/5.87 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 0.15/5.87 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.15/5.87 % No SInE strategy applied
% 0.15/5.87 % Search class: FGHSF-FFMM00-SFFFFFNN
% 0.15/5.87 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.15/5.87 % Starting SubtermCWHack with 136s (1) cores
% 0.15/5.87 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 151s (1) cores
% 0.15/5.87 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S0Y with 136s (1) cores
% 0.15/5.87 % Starting new_bool_3 with 136s (1) cores
% 0.15/5.87 % Preprocessing time : 0.002 s
% 0.15/5.87 % Presaturation interreduction done
% 0.15/5.87
% 0.15/5.87 % Proof found!
% 0.15/5.87 % SZS status Unsatisfiable
% 0.15/5.87 % SZS output start CNFRefutation
% See solution above
% 0.15/5.87 % Parsed axioms : 83
% 0.15/5.87 % Removed by relevancy pruning/SinE : 0
% 0.15/5.87 % Initial clauses : 105
% 0.15/5.87 % Removed in clause preprocessing : 26
% 0.15/5.87 % Initial clauses in saturation : 79
% 0.15/5.87 % Processed clauses : 2341
% 0.15/5.87 % ...of these trivial : 127
% 0.15/5.87 % ...subsumed : 723
% 0.15/5.87 % ...remaining for further processing : 1490
% 0.15/5.87 % Other redundant clauses eliminated : 20
% 0.15/5.87 % Clauses deleted for lack of memory : 0
% 0.15/5.87 % Backward-subsumed : 136
% 0.15/5.87 % Backward-rewritten : 1169
% 0.15/5.87 % Generated clauses : 38210
% 0.15/5.87 % ...of the previous two non-redundant : 35517
% 0.15/5.87 % ...aggressively subsumed : 0
% 0.15/5.87 % Contextual simplify-reflections : 30
% 0.15/5.87 % Paramodulations : 37750
% 0.15/5.87 % Factorizations : 389
% 0.15/5.87 % NegExts : 0
% 0.15/5.87 % Equation resolutions : 20
% 0.15/5.87 % Disequality decompositions : 0
% 0.15/5.87 % Total rewrite steps : 2995
% 0.15/5.87 % ...of those cached : 2960
% 0.15/5.87 % Propositional unsat checks : 0
% 0.15/5.87 % Propositional check models : 0
% 0.15/5.87 % Propositional check unsatisfiable : 0
% 0.15/5.87 % Propositional clauses : 0
% 0.15/5.87 % Propositional clauses after purity: 0
% 0.15/5.87 % Propositional unsat core size : 0
% 0.15/5.87 % Propositional preprocessing time : 0.000
% 0.15/5.87 % Propositional encoding time : 0.000
% 0.15/5.87 % Propositional solver time : 0.000
% 0.15/5.87 % Success case prop preproc time : 0.000
% 0.15/5.87 % Success case prop encoding time : 0.000
% 0.15/5.87 % Success case prop solver time : 0.000
% 0.15/5.87 % Current number of processed clauses : 35
% 0.15/5.87 % Positive orientable unit clauses : 20
% 0.15/5.87 % Positive unorientable unit clauses: 0
% 0.15/5.87 % Negative unit clauses : 2
% 0.15/5.87 % Non-unit-clauses : 13
% 0.15/5.87 % Current number of unprocessed clauses: 33114
% 0.15/5.87 % ...number of literals in the above : 144719
% 0.15/5.87 % Current number of archived formulas : 0
% 0.15/5.87 % Current number of archived clauses : 1436
% 0.15/5.87 % Clause-clause subsumption calls (NU) : 62445
% 0.15/5.87 % Rec. Clause-clause subsumption calls : 42772
% 0.15/5.87 % Non-unit clause-clause subsumptions : 832
% 0.15/5.87 % Unit Clause-clause subsumption calls : 338
% 0.15/5.87 % Rewrite failures with RHS unbound : 0
% 0.15/5.87 % BW rewrite match attempts : 19
% 0.15/5.87 % BW rewrite match successes : 19
% 0.15/5.87 % Condensation attempts : 0
% 0.15/5.87 % Condensation successes : 0
% 0.15/5.87 % Termbank termtop insertions : 212284
% 0.15/5.87 % Search garbage collected termcells : 398
% 0.15/5.87
% 0.15/5.87 % -------------------------------------------------
% 0.15/5.87 % User time : 0.389 s
% 0.15/5.87 % System time : 0.030 s
% 0.15/5.87 % Total time : 0.419 s
% 0.15/5.87 % Maximum resident set size: 3680 pages
% 0.15/5.87
% 0.15/5.87 % -------------------------------------------------
% 0.15/5.87 % User time : 1.987 s
% 0.15/5.87 % System time : 0.171 s
% 0.15/5.87 % Total time : 2.158 s
% 0.15/5.87 % Maximum resident set size: 4864 pages
% 0.15/5.87 % E exiting
%------------------------------------------------------------------------------