%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SYO582+1 : TPTP v9.2.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n028.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 : 300s
% DateTime : Tue May 5 05:53:48 PM UTC 2026
% Result : CounterSatisfiable 1.24s 1.73s
% Output : Saturation 1.24s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(sos_16,axiom,
( ! [X22] :
( b48_buttercup10229(X22)
=> k04_buttercup10225(X22) )
& ? [X23] :
( k04_buttercup10225(X23)
& ~ b48_buttercup10229(X23) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_16) ).
fof(sos_12,axiom,
( ! [X13] :
( b48_buttercup10227(X13)
=> k04_buttercup10225(X13) )
& ? [X14] :
( k04_buttercup10225(X14)
& ~ b48_buttercup10227(X14) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_12) ).
fof(sos_15,axiom,
( ! [X20] :
( k04_buttercup10516(X20)
=> b48_buttercup10417(X20) )
& ? [X21] :
( b48_buttercup10417(X21)
& ~ k04_buttercup10516(X21) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_15) ).
fof(sos_17,axiom,
( ! [X24] :
( b48_buttercup10515(X24)
=> k04_buttercup10516(X24) )
& ? [X25] :
( k04_buttercup10516(X25)
& ~ b48_buttercup10515(X25) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_17) ).
fof(goals_38,conjecture,
( ! [X49] :
( k04_buttercup10225(X49)
<=> b48_buttercup10519(X49) )
| ( ! [X50] :
( b48_buttercup10519(X50)
=> k04_buttercup10225(X50) )
& ? [X51] :
( k04_buttercup10225(X51)
& ~ b48_buttercup10519(X51) ) )
| ? [X52,X53,X54] :
( k04_buttercup10225(X52)
& b48_buttercup10519(X52)
& k04_buttercup10225(X53)
& ~ b48_buttercup10519(X53)
& ~ k04_buttercup10225(X54)
& b48_buttercup10519(X54) )
| ! [X55] :
( k04_buttercup10225(X55)
=> ~ b48_buttercup10519(X55) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_38) ).
fof(sos_30,axiom,
? [X41] : b48_buttercup10229(X41),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_30) ).
fof(sos_29,axiom,
? [X40] : b48_buttercup10227(X40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_29) ).
fof(sos_22,axiom,
? [X33] : k04_buttercup10225(X33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(sos_21,axiom,
? [X30,X31,X32] :
( k04_buttercup10419(X30)
& b48_buttercup10417(X30)
& k04_buttercup10419(X31)
& ~ b48_buttercup10417(X31)
& ~ k04_buttercup10419(X32)
& b48_buttercup10417(X32) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
fof(sos_03,axiom,
! [X3] :
( b48_buttercup10519(X3)
=> b48_buttercup10515(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_03) ).
fof(sos_01,axiom,
! [X1] :
( k04_buttercup10517(X1)
=> k04_buttercup10516(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
fof(sos_20,axiom,
! [X29] :
( k04_buttercup10517(X29)
<=> b48_buttercup10421(X29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_20) ).
fof(sos_14,axiom,
? [X17,X18,X19] :
( k04_buttercup10419(X17)
& b48_buttercup10222(X17)
& k04_buttercup10419(X18)
& ~ b48_buttercup10222(X18)
& ~ k04_buttercup10419(X19)
& b48_buttercup10222(X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(sos_18,axiom,
( ! [X26] :
( k04_buttercup10225(X26)
=> b48_buttercup10222(X26) )
& ? [X27] :
( b48_buttercup10222(X27)
& ~ k04_buttercup10225(X27) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_18) ).
fof(sos_05,axiom,
! [X5] :
( b48_buttercup10521(X5)
=> b48_buttercup10515(X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_05) ).
fof(sos_26,axiom,
? [X37] : b48_buttercup10521(X37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_26) ).
fof(sos_02,axiom,
! [X2] :
( b48_buttercup10518(X2)
=> b48_buttercup10515(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(sos_36,axiom,
? [X47] : b48_buttercup10518(X47),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_36) ).
fof(sos_04,axiom,
! [X4] :
( b48_buttercup10520(X4)
=> b48_buttercup10515(X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_04) ).
fof(sos_37,axiom,
? [X48] : b48_buttercup10520(X48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_37) ).
fof(sos_23,axiom,
? [X34] : k04_buttercup10517(X34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_23) ).
fof(sos_13,axiom,
( ! [X15] :
( b48_buttercup10228(X15)
=> k04_buttercup10419(X15) )
& ? [X16] :
( k04_buttercup10419(X16)
& ~ b48_buttercup10228(X16) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_13) ).
fof(sos_11,axiom,
( ! [X11] :
( b48_buttercup10422(X11)
=> k04_buttercup10419(X11) )
& ? [X12] :
( k04_buttercup10419(X12)
& ~ b48_buttercup10422(X12) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_11) ).
fof(sos_35,axiom,
? [X46] : b48_buttercup10519(X46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
fof(sos_19,axiom,
~ ! [X28] :
( k04_buttercup10419(X28)
<=> b48_buttercup10421(X28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_19) ).
fof(sos_06,axiom,
! [X6] :
( b48_buttercup10421(X6)
=> b48_buttercup10417(X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_06) ).
fof(sos_33,axiom,
? [X44] : b48_buttercup10515(X44),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_33) ).
fof(sos_28,axiom,
? [X39] : b48_buttercup10421(X39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_28) ).
fof(sos_34,axiom,
? [X45] : b48_buttercup10228(X45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(sos_27,axiom,
? [X38] : b48_buttercup10422(X38),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_27) ).
fof(sos_10,axiom,
! [X10] :
( b48_buttercup10229(X10)
=> b48_buttercup10222(X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_10) ).
fof(sos_09,axiom,
! [X9] :
( b48_buttercup10228(X9)
=> b48_buttercup10222(X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_09) ).
fof(sos_08,axiom,
! [X8] :
( b48_buttercup10227(X8)
=> b48_buttercup10222(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
fof(sos_07,axiom,
! [X7] :
( b48_buttercup10422(X7)
=> b48_buttercup10417(X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(sos_24,axiom,
? [X35] : k04_buttercup10516(X35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
fof(sos_25,axiom,
? [X36] : k04_buttercup10419(X36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_25) ).
fof(sos_32,axiom,
? [X43] : b48_buttercup10222(X43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_32) ).
fof(sos_31,axiom,
? [X42] : b48_buttercup10417(X42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_31) ).
fof(c_0_38,plain,
( ! [X22] :
( b48_buttercup10229(X22)
=> k04_buttercup10225(X22) )
& ? [X23] :
( k04_buttercup10225(X23)
& ~ b48_buttercup10229(X23) ) ),
inference(fof_simplification,[status(thm)],[sos_16]) ).
fof(c_0_39,plain,
( ! [X13] :
( b48_buttercup10227(X13)
=> k04_buttercup10225(X13) )
& ? [X14] :
( k04_buttercup10225(X14)
& ~ b48_buttercup10227(X14) ) ),
inference(fof_simplification,[status(thm)],[sos_12]) ).
fof(c_0_40,plain,
( ! [X20] :
( k04_buttercup10516(X20)
=> b48_buttercup10417(X20) )
& ? [X21] :
( b48_buttercup10417(X21)
& ~ k04_buttercup10516(X21) ) ),
inference(fof_simplification,[status(thm)],[sos_15]) ).
fof(c_0_41,plain,
( ! [X24] :
( b48_buttercup10515(X24)
=> k04_buttercup10516(X24) )
& ? [X25] :
( k04_buttercup10516(X25)
& ~ b48_buttercup10515(X25) ) ),
inference(fof_simplification,[status(thm)],[sos_17]) ).
fof(c_0_42,negated_conjecture,
~ ( ! [X49] :
( k04_buttercup10225(X49)
<=> b48_buttercup10519(X49) )
| ( ! [X50] :
( b48_buttercup10519(X50)
=> k04_buttercup10225(X50) )
& ? [X51] :
( k04_buttercup10225(X51)
& ~ b48_buttercup10519(X51) ) )
| ? [X52,X53,X54] :
( k04_buttercup10225(X52)
& b48_buttercup10519(X52)
& k04_buttercup10225(X53)
& ~ b48_buttercup10519(X53)
& ~ k04_buttercup10225(X54)
& b48_buttercup10519(X54) )
| ! [X55] :
( k04_buttercup10225(X55)
=> ~ b48_buttercup10519(X55) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[goals_38])]) ).
fof(c_0_43,plain,
! [X132] :
( ( ~ b48_buttercup10229(X132)
| k04_buttercup10225(X132) )
& k04_buttercup10225(esk8_0)
& ~ b48_buttercup10229(esk8_0) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_38])])])]) ).
fof(c_0_44,plain,
b48_buttercup10229(esk23_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_30])]) ).
fof(c_0_45,plain,
! [X123] :
( ( ~ b48_buttercup10227(X123)
| k04_buttercup10225(X123) )
& k04_buttercup10225(esk2_0)
& ~ b48_buttercup10227(esk2_0) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_39])])])]) ).
fof(c_0_46,plain,
b48_buttercup10227(esk22_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_29])]) ).
fof(c_0_47,plain,
! [X130] :
( ( ~ k04_buttercup10516(X130)
| b48_buttercup10417(X130) )
& b48_buttercup10417(esk7_0)
& ~ k04_buttercup10516(esk7_0) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_40])])])]) ).
fof(c_0_48,plain,
! [X134] :
( ( ~ b48_buttercup10515(X134)
| k04_buttercup10516(X134) )
& k04_buttercup10516(esk9_0)
& ~ b48_buttercup10515(esk9_0) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_41])])])]) ).
fof(c_0_49,negated_conjecture,
! [X161,X162,X163,X164] :
( ( ~ k04_buttercup10225(esk31_0)
| ~ b48_buttercup10519(esk31_0) )
& ( k04_buttercup10225(esk31_0)
| b48_buttercup10519(esk31_0) )
& ( b48_buttercup10519(esk32_0)
| ~ k04_buttercup10225(X161)
| b48_buttercup10519(X161) )
& ( ~ k04_buttercup10225(esk32_0)
| ~ k04_buttercup10225(X161)
| b48_buttercup10519(X161) )
& ( ~ k04_buttercup10225(X162)
| ~ b48_buttercup10519(X162)
| ~ k04_buttercup10225(X163)
| b48_buttercup10519(X163)
| k04_buttercup10225(X164)
| ~ b48_buttercup10519(X164) )
& k04_buttercup10225(esk33_0)
& b48_buttercup10519(esk33_0) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_42])])])])]) ).
cnf(c_0_50,plain,
( k04_buttercup10225(X1)
| ~ b48_buttercup10229(X1) ),
inference(split_conjunct,[status(thm)],[c_0_43]),
[final] ).
cnf(c_0_51,plain,
b48_buttercup10229(esk23_0),
inference(split_conjunct,[status(thm)],[c_0_44]),
[final] ).
cnf(c_0_52,plain,
( k04_buttercup10225(X1)
| ~ b48_buttercup10227(X1) ),
inference(split_conjunct,[status(thm)],[c_0_45]),
[final] ).
cnf(c_0_53,plain,
b48_buttercup10227(esk22_0),
inference(split_conjunct,[status(thm)],[c_0_46]),
[final] ).
fof(c_0_54,plain,
k04_buttercup10225(esk15_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_22])]) ).
fof(c_0_55,plain,
? [X30,X31,X32] :
( k04_buttercup10419(X30)
& b48_buttercup10417(X30)
& k04_buttercup10419(X31)
& ~ b48_buttercup10417(X31)
& ~ k04_buttercup10419(X32)
& b48_buttercup10417(X32) ),
inference(fof_simplification,[status(thm)],[sos_21]) ).
cnf(c_0_56,plain,
( b48_buttercup10417(X1)
| ~ k04_buttercup10516(X1) ),
inference(split_conjunct,[status(thm)],[c_0_47]),
[final] ).
cnf(c_0_57,plain,
( k04_buttercup10516(X1)
| ~ b48_buttercup10515(X1) ),
inference(split_conjunct,[status(thm)],[c_0_48]),
[final] ).
fof(c_0_58,plain,
! [X113] :
( ~ b48_buttercup10519(X113)
| b48_buttercup10515(X113) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_03])]) ).
cnf(c_0_59,negated_conjecture,
( b48_buttercup10519(X2)
| k04_buttercup10225(X3)
| ~ k04_buttercup10225(X1)
| ~ b48_buttercup10519(X1)
| ~ k04_buttercup10225(X2)
| ~ b48_buttercup10519(X3) ),
inference(split_conjunct,[status(thm)],[c_0_49]),
[final] ).
cnf(c_0_60,plain,
k04_buttercup10225(esk23_0),
inference(spm,[status(thm)],[c_0_50,c_0_51]),
[final] ).
cnf(c_0_61,plain,
k04_buttercup10225(esk22_0),
inference(spm,[status(thm)],[c_0_52,c_0_53]),
[final] ).
cnf(c_0_62,plain,
k04_buttercup10225(esk2_0),
inference(split_conjunct,[status(thm)],[c_0_45]),
[final] ).
cnf(c_0_63,plain,
k04_buttercup10225(esk8_0),
inference(split_conjunct,[status(thm)],[c_0_43]),
[final] ).
cnf(c_0_64,plain,
k04_buttercup10225(esk15_0),
inference(split_conjunct,[status(thm)],[c_0_54]),
[final] ).
fof(c_0_65,plain,
! [X111] :
( ~ k04_buttercup10517(X111)
| k04_buttercup10516(X111) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_01])]) ).
fof(c_0_66,plain,
! [X139] :
( ( ~ k04_buttercup10517(X139)
| b48_buttercup10421(X139) )
& ( ~ b48_buttercup10421(X139)
| k04_buttercup10517(X139) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_20])]) ).
fof(c_0_67,plain,
( k04_buttercup10419(esk12_0)
& b48_buttercup10417(esk12_0)
& k04_buttercup10419(esk13_0)
& ~ b48_buttercup10417(esk13_0)
& ~ k04_buttercup10419(esk14_0)
& b48_buttercup10417(esk14_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[c_0_55])]) ).
cnf(c_0_68,plain,
( b48_buttercup10417(X1)
| ~ b48_buttercup10515(X1) ),
inference(spm,[status(thm)],[c_0_56,c_0_57]),
[final] ).
cnf(c_0_69,plain,
( b48_buttercup10515(X1)
| ~ b48_buttercup10519(X1) ),
inference(split_conjunct,[status(thm)],[c_0_58]),
[final] ).
cnf(c_0_70,plain,
~ k04_buttercup10516(esk7_0),
inference(split_conjunct,[status(thm)],[c_0_47]),
[final] ).
fof(c_0_71,plain,
? [X17,X18,X19] :
( k04_buttercup10419(X17)
& b48_buttercup10222(X17)
& k04_buttercup10419(X18)
& ~ b48_buttercup10222(X18)
& ~ k04_buttercup10419(X19)
& b48_buttercup10222(X19) ),
inference(fof_simplification,[status(thm)],[sos_14]) ).
fof(c_0_72,plain,
( ! [X26] :
( k04_buttercup10225(X26)
=> b48_buttercup10222(X26) )
& ? [X27] :
( b48_buttercup10222(X27)
& ~ k04_buttercup10225(X27) ) ),
inference(fof_simplification,[status(thm)],[sos_18]) ).
fof(c_0_73,plain,
! [X115] :
( ~ b48_buttercup10521(X115)
| b48_buttercup10515(X115) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_05])]) ).
fof(c_0_74,plain,
b48_buttercup10521(esk19_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_26])]) ).
fof(c_0_75,plain,
! [X112] :
( ~ b48_buttercup10518(X112)
| b48_buttercup10515(X112) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_02])]) ).
fof(c_0_76,plain,
b48_buttercup10518(esk29_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_36])]) ).
fof(c_0_77,plain,
! [X114] :
( ~ b48_buttercup10520(X114)
| b48_buttercup10515(X114) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_04])]) ).
fof(c_0_78,plain,
b48_buttercup10520(esk30_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_37])]) ).
fof(c_0_79,plain,
k04_buttercup10517(esk16_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_23])]) ).
fof(c_0_80,plain,
( ! [X15] :
( b48_buttercup10228(X15)
=> k04_buttercup10419(X15) )
& ? [X16] :
( k04_buttercup10419(X16)
& ~ b48_buttercup10228(X16) ) ),
inference(fof_simplification,[status(thm)],[sos_13]) ).
fof(c_0_81,plain,
( ! [X11] :
( b48_buttercup10422(X11)
=> k04_buttercup10419(X11) )
& ? [X12] :
( k04_buttercup10419(X12)
& ~ b48_buttercup10422(X12) ) ),
inference(fof_simplification,[status(thm)],[sos_11]) ).
cnf(c_0_82,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk23_0)
| ~ k04_buttercup10225(X2)
| ~ b48_buttercup10519(X1)
| ~ b48_buttercup10519(X2) ),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_83,negated_conjecture,
k04_buttercup10225(esk33_0),
inference(split_conjunct,[status(thm)],[c_0_49]),
[final] ).
cnf(c_0_84,negated_conjecture,
b48_buttercup10519(esk33_0),
inference(split_conjunct,[status(thm)],[c_0_49]),
[final] ).
fof(c_0_85,plain,
b48_buttercup10519(esk28_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_35])]) ).
cnf(c_0_86,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk22_0)
| ~ k04_buttercup10225(X2)
| ~ b48_buttercup10519(X1)
| ~ b48_buttercup10519(X2) ),
inference(spm,[status(thm)],[c_0_59,c_0_61]) ).
cnf(c_0_87,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk2_0)
| ~ k04_buttercup10225(X2)
| ~ b48_buttercup10519(X1)
| ~ b48_buttercup10519(X2) ),
inference(spm,[status(thm)],[c_0_59,c_0_62]) ).
cnf(c_0_88,negated_conjecture,
( b48_buttercup10519(esk32_0)
| b48_buttercup10519(X1)
| ~ k04_buttercup10225(X1) ),
inference(split_conjunct,[status(thm)],[c_0_49]),
[final] ).
cnf(c_0_89,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk8_0)
| ~ k04_buttercup10225(X2)
| ~ b48_buttercup10519(X1)
| ~ b48_buttercup10519(X2) ),
inference(spm,[status(thm)],[c_0_59,c_0_63]) ).
cnf(c_0_90,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk15_0)
| ~ k04_buttercup10225(X2)
| ~ b48_buttercup10519(X1)
| ~ b48_buttercup10519(X2) ),
inference(spm,[status(thm)],[c_0_59,c_0_64]) ).
cnf(c_0_91,plain,
( k04_buttercup10516(X1)
| ~ k04_buttercup10517(X1) ),
inference(split_conjunct,[status(thm)],[c_0_65]),
[final] ).
cnf(c_0_92,plain,
( k04_buttercup10517(X1)
| ~ b48_buttercup10421(X1) ),
inference(split_conjunct,[status(thm)],[c_0_66]),
[final] ).
fof(c_0_93,plain,
( ( ~ k04_buttercup10419(esk11_0)
| ~ b48_buttercup10421(esk11_0) )
& ( k04_buttercup10419(esk11_0)
| b48_buttercup10421(esk11_0) ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_19])])]) ).
cnf(c_0_94,plain,
~ b48_buttercup10417(esk13_0),
inference(split_conjunct,[status(thm)],[c_0_67]),
[final] ).
cnf(c_0_95,plain,
( b48_buttercup10417(X1)
| ~ b48_buttercup10519(X1) ),
inference(spm,[status(thm)],[c_0_68,c_0_69]),
[final] ).
fof(c_0_96,plain,
! [X116] :
( ~ b48_buttercup10421(X116)
| b48_buttercup10417(X116) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_06])]) ).
cnf(c_0_97,plain,
~ b48_buttercup10515(esk7_0),
inference(spm,[status(thm)],[c_0_70,c_0_57]),
[final] ).
cnf(c_0_98,plain,
~ b48_buttercup10515(esk9_0),
inference(split_conjunct,[status(thm)],[c_0_48]),
[final] ).
fof(c_0_99,plain,
( k04_buttercup10419(esk4_0)
& b48_buttercup10222(esk4_0)
& k04_buttercup10419(esk5_0)
& ~ b48_buttercup10222(esk5_0)
& ~ k04_buttercup10419(esk6_0)
& b48_buttercup10222(esk6_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[c_0_71])]) ).
fof(c_0_100,plain,
! [X136] :
( ( ~ k04_buttercup10225(X136)
| b48_buttercup10222(X136) )
& b48_buttercup10222(esk10_0)
& ~ k04_buttercup10225(esk10_0) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_72])])])]) ).
cnf(c_0_101,plain,
( b48_buttercup10515(X1)
| ~ b48_buttercup10521(X1) ),
inference(split_conjunct,[status(thm)],[c_0_73]),
[final] ).
cnf(c_0_102,plain,
b48_buttercup10521(esk19_0),
inference(split_conjunct,[status(thm)],[c_0_74]),
[final] ).
fof(c_0_103,plain,
b48_buttercup10515(esk26_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_33])]) ).
cnf(c_0_104,plain,
( b48_buttercup10515(X1)
| ~ b48_buttercup10518(X1) ),
inference(split_conjunct,[status(thm)],[c_0_75]),
[final] ).
cnf(c_0_105,plain,
b48_buttercup10518(esk29_0),
inference(split_conjunct,[status(thm)],[c_0_76]),
[final] ).
cnf(c_0_106,plain,
( b48_buttercup10515(X1)
| ~ b48_buttercup10520(X1) ),
inference(split_conjunct,[status(thm)],[c_0_77]),
[final] ).
cnf(c_0_107,plain,
b48_buttercup10520(esk30_0),
inference(split_conjunct,[status(thm)],[c_0_78]),
[final] ).
fof(c_0_108,plain,
b48_buttercup10421(esk21_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_28])]) ).
cnf(c_0_109,plain,
k04_buttercup10517(esk16_0),
inference(split_conjunct,[status(thm)],[c_0_79]),
[final] ).
fof(c_0_110,plain,
! [X125] :
( ( ~ b48_buttercup10228(X125)
| k04_buttercup10419(X125) )
& k04_buttercup10419(esk3_0)
& ~ b48_buttercup10228(esk3_0) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_80])])])]) ).
fof(c_0_111,plain,
b48_buttercup10228(esk27_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_34])]) ).
fof(c_0_112,plain,
! [X121] :
( ( ~ b48_buttercup10422(X121)
| k04_buttercup10419(X121) )
& k04_buttercup10419(esk1_0)
& ~ b48_buttercup10422(esk1_0) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_81])])])]) ).
fof(c_0_113,plain,
b48_buttercup10422(esk20_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_27])]) ).
fof(c_0_114,plain,
! [X120] :
( ~ b48_buttercup10229(X120)
| b48_buttercup10222(X120) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_10])]) ).
fof(c_0_115,plain,
! [X119] :
( ~ b48_buttercup10228(X119)
| b48_buttercup10222(X119) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_09])]) ).
fof(c_0_116,plain,
! [X118] :
( ~ b48_buttercup10227(X118)
| b48_buttercup10222(X118) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_08])]) ).
fof(c_0_117,plain,
! [X117] :
( ~ b48_buttercup10422(X117)
| b48_buttercup10417(X117) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_07])]) ).
fof(c_0_118,plain,
k04_buttercup10516(esk17_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_24])]) ).
cnf(c_0_119,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk23_0)
| ~ b48_buttercup10519(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_83]),c_0_84])]),
[final] ).
cnf(c_0_120,plain,
b48_buttercup10519(esk28_0),
inference(split_conjunct,[status(thm)],[c_0_85]),
[final] ).
cnf(c_0_121,negated_conjecture,
( k04_buttercup10225(esk31_0)
| b48_buttercup10519(esk31_0) ),
inference(split_conjunct,[status(thm)],[c_0_49]),
[final] ).
cnf(c_0_122,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk22_0)
| ~ b48_buttercup10519(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_83]),c_0_84])]),
[final] ).
cnf(c_0_123,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk2_0)
| ~ b48_buttercup10519(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_83]),c_0_84])]),
[final] ).
cnf(c_0_124,negated_conjecture,
( b48_buttercup10519(esk32_0)
| b48_buttercup10519(esk2_0) ),
inference(spm,[status(thm)],[c_0_88,c_0_62]),
[final] ).
cnf(c_0_125,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk8_0)
| ~ b48_buttercup10519(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_83]),c_0_84])]),
[final] ).
cnf(c_0_126,negated_conjecture,
( b48_buttercup10519(esk32_0)
| b48_buttercup10519(esk8_0) ),
inference(spm,[status(thm)],[c_0_88,c_0_63]),
[final] ).
cnf(c_0_127,negated_conjecture,
( k04_buttercup10225(X1)
| b48_buttercup10519(esk15_0)
| ~ b48_buttercup10519(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_83]),c_0_84])]),
[final] ).
cnf(c_0_128,plain,
( k04_buttercup10516(X1)
| ~ b48_buttercup10421(X1) ),
inference(spm,[status(thm)],[c_0_91,c_0_92]),
[final] ).
cnf(c_0_129,plain,
( k04_buttercup10419(esk11_0)
| b48_buttercup10421(esk11_0) ),
inference(split_conjunct,[status(thm)],[c_0_93]),
[final] ).
cnf(c_0_130,plain,
~ b48_buttercup10519(esk13_0),
inference(spm,[status(thm)],[c_0_94,c_0_95]),
[final] ).
cnf(c_0_131,negated_conjecture,
( b48_buttercup10519(X1)
| ~ k04_buttercup10225(esk32_0)
| ~ k04_buttercup10225(X1) ),
inference(split_conjunct,[status(thm)],[c_0_49]),
[final] ).
cnf(c_0_132,plain,
( b48_buttercup10417(X1)
| ~ b48_buttercup10421(X1) ),
inference(split_conjunct,[status(thm)],[c_0_96]),
[final] ).
cnf(c_0_133,plain,
~ b48_buttercup10519(esk7_0),
inference(spm,[status(thm)],[c_0_97,c_0_69]),
[final] ).
cnf(c_0_134,plain,
~ b48_buttercup10519(esk9_0),
inference(spm,[status(thm)],[c_0_98,c_0_69]),
[final] ).
cnf(c_0_135,negated_conjecture,
( ~ k04_buttercup10225(esk31_0)
| ~ b48_buttercup10519(esk31_0) ),
inference(split_conjunct,[status(thm)],[c_0_49]),
[final] ).
cnf(c_0_136,plain,
~ b48_buttercup10222(esk5_0),
inference(split_conjunct,[status(thm)],[c_0_99]),
[final] ).
cnf(c_0_137,plain,
( b48_buttercup10222(X1)
| ~ k04_buttercup10225(X1) ),
inference(split_conjunct,[status(thm)],[c_0_100]),
[final] ).
cnf(c_0_138,plain,
b48_buttercup10515(esk19_0),
inference(spm,[status(thm)],[c_0_101,c_0_102]),
[final] ).
cnf(c_0_139,plain,
b48_buttercup10515(esk26_0),
inference(split_conjunct,[status(thm)],[c_0_103]),
[final] ).
cnf(c_0_140,plain,
b48_buttercup10515(esk29_0),
inference(spm,[status(thm)],[c_0_104,c_0_105]),
[final] ).
cnf(c_0_141,plain,
b48_buttercup10515(esk30_0),
inference(spm,[status(thm)],[c_0_106,c_0_107]),
[final] ).
cnf(c_0_142,plain,
b48_buttercup10421(esk21_0),
inference(split_conjunct,[status(thm)],[c_0_108]),
[final] ).
cnf(c_0_143,plain,
k04_buttercup10516(esk16_0),
inference(spm,[status(thm)],[c_0_91,c_0_109]),
[final] ).
cnf(c_0_144,plain,
( k04_buttercup10419(X1)
| ~ b48_buttercup10228(X1) ),
inference(split_conjunct,[status(thm)],[c_0_110]),
[final] ).
cnf(c_0_145,plain,
b48_buttercup10228(esk27_0),
inference(split_conjunct,[status(thm)],[c_0_111]),
[final] ).
cnf(c_0_146,plain,
( k04_buttercup10419(X1)
| ~ b48_buttercup10422(X1) ),
inference(split_conjunct,[status(thm)],[c_0_112]),
[final] ).
cnf(c_0_147,plain,
b48_buttercup10422(esk20_0),
inference(split_conjunct,[status(thm)],[c_0_113]),
[final] ).
cnf(c_0_148,plain,
( b48_buttercup10222(X1)
| ~ b48_buttercup10229(X1) ),
inference(split_conjunct,[status(thm)],[c_0_114]),
[final] ).
cnf(c_0_149,plain,
( b48_buttercup10222(X1)
| ~ b48_buttercup10228(X1) ),
inference(split_conjunct,[status(thm)],[c_0_115]),
[final] ).
cnf(c_0_150,plain,
( b48_buttercup10222(X1)
| ~ b48_buttercup10227(X1) ),
inference(split_conjunct,[status(thm)],[c_0_116]),
[final] ).
cnf(c_0_151,plain,
( b48_buttercup10417(X1)
| ~ b48_buttercup10422(X1) ),
inference(split_conjunct,[status(thm)],[c_0_117]),
[final] ).
cnf(c_0_152,plain,
k04_buttercup10516(esk9_0),
inference(split_conjunct,[status(thm)],[c_0_48]),
[final] ).
cnf(c_0_153,plain,
k04_buttercup10516(esk17_0),
inference(split_conjunct,[status(thm)],[c_0_118]),
[final] ).
cnf(c_0_154,plain,
( b48_buttercup10421(X1)
| ~ k04_buttercup10517(X1) ),
inference(split_conjunct,[status(thm)],[c_0_66]),
[final] ).
fof(c_0_155,plain,
k04_buttercup10419(esk18_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_25])]) ).
fof(c_0_156,plain,
b48_buttercup10222(esk25_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_32])]) ).
fof(c_0_157,plain,
b48_buttercup10417(esk24_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[sos_31])]) ).
cnf(c_0_158,negated_conjecture,
( k04_buttercup10225(esk28_0)
| b48_buttercup10519(esk23_0) ),
inference(spm,[status(thm)],[c_0_119,c_0_120]),
[final] ).
cnf(c_0_159,negated_conjecture,
( k04_buttercup10225(esk31_0)
| b48_buttercup10519(esk23_0) ),
inference(spm,[status(thm)],[c_0_119,c_0_121]),
[final] ).
cnf(c_0_160,negated_conjecture,
( k04_buttercup10225(esk28_0)
| b48_buttercup10519(esk22_0) ),
inference(spm,[status(thm)],[c_0_122,c_0_120]),
[final] ).
cnf(c_0_161,negated_conjecture,
( k04_buttercup10225(esk31_0)
| b48_buttercup10519(esk22_0) ),
inference(spm,[status(thm)],[c_0_122,c_0_121]),
[final] ).
cnf(c_0_162,negated_conjecture,
( k04_buttercup10225(esk28_0)
| b48_buttercup10519(esk2_0) ),
inference(spm,[status(thm)],[c_0_123,c_0_120]),
[final] ).
cnf(c_0_163,negated_conjecture,
( k04_buttercup10225(esk31_0)
| b48_buttercup10519(esk2_0) ),
inference(spm,[status(thm)],[c_0_123,c_0_121]),
[final] ).
cnf(c_0_164,negated_conjecture,
( k04_buttercup10225(esk32_0)
| b48_buttercup10519(esk2_0) ),
inference(spm,[status(thm)],[c_0_123,c_0_124]),
[final] ).
cnf(c_0_165,negated_conjecture,
( k04_buttercup10225(esk28_0)
| b48_buttercup10519(esk8_0) ),
inference(spm,[status(thm)],[c_0_125,c_0_120]),
[final] ).
cnf(c_0_166,negated_conjecture,
( k04_buttercup10225(esk31_0)
| b48_buttercup10519(esk8_0) ),
inference(spm,[status(thm)],[c_0_125,c_0_121]),
[final] ).
cnf(c_0_167,negated_conjecture,
( k04_buttercup10225(esk32_0)
| b48_buttercup10519(esk8_0) ),
inference(spm,[status(thm)],[c_0_125,c_0_126]),
[final] ).
cnf(c_0_168,negated_conjecture,
( k04_buttercup10225(esk28_0)
| b48_buttercup10519(esk15_0) ),
inference(spm,[status(thm)],[c_0_127,c_0_120]),
[final] ).
cnf(c_0_169,negated_conjecture,
( k04_buttercup10225(esk31_0)
| b48_buttercup10519(esk15_0) ),
inference(spm,[status(thm)],[c_0_127,c_0_121]),
[final] ).
cnf(c_0_170,negated_conjecture,
( b48_buttercup10519(esk32_0)
| b48_buttercup10519(esk23_0) ),
inference(spm,[status(thm)],[c_0_88,c_0_60]),
[final] ).
cnf(c_0_171,negated_conjecture,
( b48_buttercup10519(esk32_0)
| b48_buttercup10519(esk22_0) ),
inference(spm,[status(thm)],[c_0_88,c_0_61]),
[final] ).
cnf(c_0_172,plain,
( k04_buttercup10419(esk11_0)
| k04_buttercup10516(esk11_0) ),
inference(spm,[status(thm)],[c_0_128,c_0_129]),
[final] ).
cnf(c_0_173,negated_conjecture,
( ~ k04_buttercup10225(esk32_0)
| ~ k04_buttercup10225(esk13_0) ),
inference(spm,[status(thm)],[c_0_130,c_0_131]),
[final] ).
cnf(c_0_174,negated_conjecture,
( b48_buttercup10519(esk32_0)
| b48_buttercup10519(esk15_0) ),
inference(spm,[status(thm)],[c_0_88,c_0_64]),
[final] ).
cnf(c_0_175,plain,
( k04_buttercup10419(esk11_0)
| b48_buttercup10417(esk11_0) ),
inference(spm,[status(thm)],[c_0_132,c_0_129]),
[final] ).
cnf(c_0_176,negated_conjecture,
( ~ k04_buttercup10225(esk32_0)
| ~ k04_buttercup10225(esk7_0) ),
inference(spm,[status(thm)],[c_0_133,c_0_131]),
[final] ).
cnf(c_0_177,negated_conjecture,
( ~ k04_buttercup10225(esk32_0)
| ~ k04_buttercup10225(esk9_0) ),
inference(spm,[status(thm)],[c_0_134,c_0_131]),
[final] ).
cnf(c_0_178,negated_conjecture,
( ~ k04_buttercup10225(esk31_0)
| ~ k04_buttercup10225(esk32_0) ),
inference(spm,[status(thm)],[c_0_135,c_0_131]),
[final] ).
cnf(c_0_179,plain,
( ~ k04_buttercup10419(esk11_0)
| ~ b48_buttercup10421(esk11_0) ),
inference(split_conjunct,[status(thm)],[c_0_93]),
[final] ).
cnf(c_0_180,plain,
~ k04_buttercup10225(esk5_0),
inference(spm,[status(thm)],[c_0_136,c_0_137]),
[final] ).
cnf(c_0_181,plain,
~ k04_buttercup10225(esk10_0),
inference(split_conjunct,[status(thm)],[c_0_100]),
[final] ).
cnf(c_0_182,plain,
~ k04_buttercup10419(esk14_0),
inference(split_conjunct,[status(thm)],[c_0_67]),
[final] ).
cnf(c_0_183,plain,
~ k04_buttercup10419(esk6_0),
inference(split_conjunct,[status(thm)],[c_0_99]),
[final] ).
cnf(c_0_184,plain,
~ b48_buttercup10229(esk8_0),
inference(split_conjunct,[status(thm)],[c_0_43]),
[final] ).
cnf(c_0_185,plain,
~ b48_buttercup10228(esk3_0),
inference(split_conjunct,[status(thm)],[c_0_110]),
[final] ).
cnf(c_0_186,plain,
~ b48_buttercup10227(esk2_0),
inference(split_conjunct,[status(thm)],[c_0_45]),
[final] ).
cnf(c_0_187,plain,
~ b48_buttercup10422(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_112]),
[final] ).
cnf(c_0_188,plain,
b48_buttercup10417(esk19_0),
inference(spm,[status(thm)],[c_0_68,c_0_138]),
[final] ).
cnf(c_0_189,plain,
b48_buttercup10417(esk26_0),
inference(spm,[status(thm)],[c_0_68,c_0_139]),
[final] ).
cnf(c_0_190,plain,
b48_buttercup10417(esk29_0),
inference(spm,[status(thm)],[c_0_68,c_0_140]),
[final] ).
cnf(c_0_191,plain,
b48_buttercup10417(esk30_0),
inference(spm,[status(thm)],[c_0_68,c_0_141]),
[final] ).
cnf(c_0_192,plain,
k04_buttercup10516(esk21_0),
inference(spm,[status(thm)],[c_0_128,c_0_142]),
[final] ).
cnf(c_0_193,plain,
b48_buttercup10417(esk16_0),
inference(spm,[status(thm)],[c_0_56,c_0_143]),
[final] ).
cnf(c_0_194,plain,
k04_buttercup10419(esk27_0),
inference(spm,[status(thm)],[c_0_144,c_0_145]),
[final] ).
cnf(c_0_195,plain,
k04_buttercup10419(esk20_0),
inference(spm,[status(thm)],[c_0_146,c_0_147]),
[final] ).
cnf(c_0_196,plain,
b48_buttercup10222(esk23_0),
inference(spm,[status(thm)],[c_0_148,c_0_51]),
[final] ).
cnf(c_0_197,plain,
b48_buttercup10222(esk27_0),
inference(spm,[status(thm)],[c_0_149,c_0_145]),
[final] ).
cnf(c_0_198,plain,
b48_buttercup10222(esk22_0),
inference(spm,[status(thm)],[c_0_150,c_0_53]),
[final] ).
cnf(c_0_199,plain,
b48_buttercup10417(esk20_0),
inference(spm,[status(thm)],[c_0_151,c_0_147]),
[final] ).
cnf(c_0_200,plain,
b48_buttercup10417(esk21_0),
inference(spm,[status(thm)],[c_0_132,c_0_142]),
[final] ).
cnf(c_0_201,plain,
b48_buttercup10417(esk9_0),
inference(spm,[status(thm)],[c_0_56,c_0_152]),
[final] ).
cnf(c_0_202,plain,
b48_buttercup10417(esk17_0),
inference(spm,[status(thm)],[c_0_56,c_0_153]),
[final] ).
cnf(c_0_203,plain,
b48_buttercup10421(esk16_0),
inference(spm,[status(thm)],[c_0_154,c_0_109]),
[final] ).
cnf(c_0_204,plain,
k04_buttercup10419(esk18_0),
inference(split_conjunct,[status(thm)],[c_0_155]),
[final] ).
cnf(c_0_205,plain,
k04_buttercup10419(esk13_0),
inference(split_conjunct,[status(thm)],[c_0_67]),
[final] ).
cnf(c_0_206,plain,
k04_buttercup10419(esk12_0),
inference(split_conjunct,[status(thm)],[c_0_67]),
[final] ).
cnf(c_0_207,plain,
k04_buttercup10419(esk5_0),
inference(split_conjunct,[status(thm)],[c_0_99]),
[final] ).
cnf(c_0_208,plain,
k04_buttercup10419(esk4_0),
inference(split_conjunct,[status(thm)],[c_0_99]),
[final] ).
cnf(c_0_209,plain,
k04_buttercup10419(esk3_0),
inference(split_conjunct,[status(thm)],[c_0_110]),
[final] ).
cnf(c_0_210,plain,
k04_buttercup10419(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_112]),
[final] ).
cnf(c_0_211,plain,
b48_buttercup10222(esk25_0),
inference(split_conjunct,[status(thm)],[c_0_156]),
[final] ).
cnf(c_0_212,plain,
b48_buttercup10222(esk10_0),
inference(split_conjunct,[status(thm)],[c_0_100]),
[final] ).
cnf(c_0_213,plain,
b48_buttercup10222(esk6_0),
inference(split_conjunct,[status(thm)],[c_0_99]),
[final] ).
cnf(c_0_214,plain,
b48_buttercup10222(esk4_0),
inference(split_conjunct,[status(thm)],[c_0_99]),
[final] ).
cnf(c_0_215,plain,
b48_buttercup10417(esk24_0),
inference(split_conjunct,[status(thm)],[c_0_157]),
[final] ).
cnf(c_0_216,plain,
b48_buttercup10417(esk14_0),
inference(split_conjunct,[status(thm)],[c_0_67]),
[final] ).
cnf(c_0_217,plain,
b48_buttercup10417(esk12_0),
inference(split_conjunct,[status(thm)],[c_0_67]),
[final] ).
cnf(c_0_218,plain,
b48_buttercup10417(esk7_0),
inference(split_conjunct,[status(thm)],[c_0_47]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO582+1 : TPTP v9.2.1. Released v5.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n028.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 09:14:01 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 1.24/1.73 % Version : CSE_E---1.7
% 1.24/1.73 % Problem : theBenchmark.p
% 1.24/1.73 % SZS status CounterSatisfiable for theBenchmark.p
% 1.24/1.73 % SZS output start Saturation
% See solution above
% 1.24/1.73 % Total time : 1.376s
%------------------------------------------------------------------------------