%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : BOO008-3 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n002.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 04:11:05 PM UTC 2026
% Result : Satisfiable 8.63s 5.96s
% Output : Saturation 8.63s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(distributivity5,axiom,
( product(X3,X5,X7)
| ~ sum(X1,X2,X3)
| ~ sum(X1,X4,X5)
| ~ product(X2,X4,X6)
| ~ sum(X1,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity5) ).
cnf(multiplicative_inverse1,axiom,
product(inverse(X1),X1,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_inverse1) ).
cnf(closure_of_addition,axiom,
sum(X1,X2,add(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_addition) ).
cnf(additive_identity2,axiom,
sum(X1,additive_identity,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity2) ).
cnf(multiplicative_identity1,axiom,
sum(multiplicative_identity,X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_identity1) ).
cnf(distributivity1,axiom,
( sum(X3,X5,X7)
| ~ product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X2,X4,X6)
| ~ product(X1,X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity1) ).
cnf(multiplicative_inverse2,axiom,
product(X1,inverse(X1),additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_inverse2) ).
cnf(additive_inverse2,axiom,
sum(X1,inverse(X1),multiplicative_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_inverse2) ).
cnf(closure_of_multiplication,axiom,
product(X1,X2,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_multiplication) ).
cnf(commutativity_of_multiplication,axiom,
( product(X2,X1,X3)
| ~ product(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_multiplication) ).
cnf(additive_identity1,axiom,
sum(additive_identity,X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity1) ).
cnf(commutativity_of_addition,axiom,
( sum(X2,X1,X3)
| ~ sum(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_addition) ).
cnf(multiplicative_identity2,axiom,
sum(X1,multiplicative_identity,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_identity2) ).
cnf(distributivity2,axiom,
( product(X1,X6,X7)
| ~ product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X2,X4,X6)
| ~ sum(X3,X5,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity2) ).
cnf(x_plus_y__plus_z,hypothesis,
sum(x_plus_y,z,x_plus_y__plus_z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_plus_y__plus_z) ).
cnf(distributivity6,axiom,
( sum(X1,X6,X7)
| ~ sum(X1,X2,X3)
| ~ sum(X1,X4,X5)
| ~ product(X2,X4,X6)
| ~ product(X3,X5,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',distributivity6) ).
cnf(x_plus__y_plus_z,hypothesis,
sum(x,y_plus_z,x__plus_y_plus_z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',x_plus__y_plus_z) ).
cnf(prove_equality,negated_conjecture,
x__plus_y_plus_z != x_plus_y__plus_z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_equality) ).
cnf(c_0_18,axiom,
( product(X3,X5,X7)
| ~ sum(X1,X2,X3)
| ~ sum(X1,X4,X5)
| ~ product(X2,X4,X6)
| ~ sum(X1,X6,X7) ),
distributivity5 ).
cnf(c_0_19,axiom,
product(inverse(X1),X1,additive_identity),
multiplicative_inverse1 ).
cnf(c_0_20,plain,
( product(X1,X2,X3)
| ~ sum(X4,inverse(X5),X1)
| ~ sum(X4,additive_identity,X3)
| ~ sum(X4,X5,X2) ),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_21,axiom,
sum(X1,X2,add(X1,X2)),
closure_of_addition ).
cnf(c_0_22,plain,
( product(X1,add(X2,X3),X4)
| ~ sum(X2,inverse(X3),X1)
| ~ sum(X2,additive_identity,X4) ),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
cnf(c_0_23,axiom,
sum(X1,additive_identity,X1),
additive_identity2 ).
cnf(c_0_24,axiom,
sum(multiplicative_identity,X1,X1),
multiplicative_identity1 ).
cnf(c_0_25,axiom,
( sum(X3,X5,X7)
| ~ product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X2,X4,X6)
| ~ product(X1,X6,X7) ),
distributivity1 ).
cnf(c_0_26,axiom,
product(X1,inverse(X1),additive_identity),
multiplicative_inverse2 ).
cnf(c_0_27,plain,
( product(X1,add(X2,X3),X2)
| ~ sum(X2,inverse(X3),X1) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_28,axiom,
sum(X1,inverse(X1),multiplicative_identity),
additive_inverse2 ).
cnf(c_0_29,plain,
( product(X1,X2,X3)
| ~ sum(multiplicative_identity,inverse(X2),X1)
| ~ sum(multiplicative_identity,additive_identity,X3) ),
inference(spm,[status(thm)],[c_0_20,c_0_24]) ).
cnf(c_0_30,axiom,
product(X1,X2,multiply(X1,X2)),
closure_of_multiplication ).
cnf(c_0_31,plain,
( sum(X1,X2,additive_identity)
| ~ product(X3,X4,X2)
| ~ product(X3,X5,X1)
| ~ sum(X5,X4,inverse(X3)) ),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_32,axiom,
( product(X2,X1,X3)
| ~ product(X1,X2,X3) ),
commutativity_of_multiplication ).
cnf(c_0_33,plain,
product(multiplicative_identity,add(X1,X1),X1),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_34,plain,
( product(X1,X2,multiplicative_identity)
| ~ sum(multiplicative_identity,inverse(X2),X1) ),
inference(spm,[status(thm)],[c_0_29,c_0_23]) ).
cnf(c_0_35,plain,
( product(X1,X2,X3)
| ~ sum(X4,multiply(X5,X6),X3)
| ~ sum(X4,X6,X2)
| ~ sum(X4,X5,X1) ),
inference(spm,[status(thm)],[c_0_18,c_0_30]) ).
cnf(c_0_36,axiom,
sum(additive_identity,X1,X1),
additive_identity1 ).
cnf(c_0_37,plain,
( sum(X1,additive_identity,additive_identity)
| ~ product(X2,X3,X1)
| ~ sum(X3,inverse(X2),inverse(X2)) ),
inference(spm,[status(thm)],[c_0_31,c_0_26]) ).
cnf(c_0_38,plain,
product(add(X1,X1),multiplicative_identity,X1),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_39,plain,
product(inverse(X1),X1,multiplicative_identity),
inference(spm,[status(thm)],[c_0_34,c_0_24]) ).
cnf(c_0_40,plain,
( product(X1,X2,X3)
| ~ sum(additive_identity,multiply(X4,X2),X3)
| ~ sum(additive_identity,X4,X1) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_41,axiom,
( sum(X2,X1,X3)
| ~ sum(X1,X2,X3) ),
commutativity_of_addition ).
cnf(c_0_42,plain,
sum(X1,additive_identity,additive_identity),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_38]),c_0_24])]) ).
cnf(c_0_43,plain,
product(X1,inverse(X1),multiplicative_identity),
inference(spm,[status(thm)],[c_0_32,c_0_39]) ).
cnf(c_0_44,plain,
( product(X1,X2,X3)
| ~ sum(additive_identity,multiply(X1,X2),X3) ),
inference(spm,[status(thm)],[c_0_40,c_0_36]) ).
cnf(c_0_45,plain,
sum(additive_identity,X1,additive_identity),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_46,plain,
( sum(X1,X2,multiplicative_identity)
| ~ product(X3,X4,X2)
| ~ product(X3,X5,X1)
| ~ sum(X5,X4,inverse(X3)) ),
inference(spm,[status(thm)],[c_0_25,c_0_43]) ).
cnf(c_0_47,plain,
product(X1,X2,additive_identity),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_48,axiom,
sum(X1,multiplicative_identity,X1),
multiplicative_identity2 ).
cnf(c_0_49,axiom,
( product(X1,X6,X7)
| ~ product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X2,X4,X6)
| ~ sum(X3,X5,X7) ),
distributivity2 ).
cnf(c_0_50,plain,
product(X1,X2,multiply(X2,X1)),
inference(spm,[status(thm)],[c_0_32,c_0_30]) ).
cnf(c_0_51,plain,
( sum(X1,additive_identity,multiplicative_identity)
| ~ product(X2,X3,X1)
| ~ sum(X3,X4,inverse(X2)) ),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_52,plain,
( product(X1,X2,X3)
| ~ sum(X2,inverse(multiplicative_identity),X1)
| ~ sum(X2,additive_identity,X3) ),
inference(spm,[status(thm)],[c_0_20,c_0_48]) ).
cnf(c_0_53,plain,
( product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X5,multiply(X6,X1),X3)
| ~ sum(X4,X6,X2) ),
inference(spm,[status(thm)],[c_0_49,c_0_50]) ).
cnf(c_0_54,plain,
( sum(X1,additive_identity,multiplicative_identity)
| ~ sum(multiplicative_identity,X2,inverse(add(X1,X1))) ),
inference(spm,[status(thm)],[c_0_51,c_0_38]) ).
cnf(c_0_55,plain,
( product(X1,X2,X2)
| ~ sum(X2,inverse(multiplicative_identity),X1) ),
inference(spm,[status(thm)],[c_0_52,c_0_23]) ).
cnf(c_0_56,plain,
( product(X1,X2,X3)
| ~ sum(additive_identity,multiply(X4,X1),X3)
| ~ sum(X5,X4,X2) ),
inference(spm,[status(thm)],[c_0_53,c_0_47]) ).
cnf(c_0_57,plain,
sum(X1,additive_identity,multiplicative_identity),
inference(spm,[status(thm)],[c_0_54,c_0_24]) ).
cnf(c_0_58,plain,
product(multiplicative_identity,multiplicative_identity,multiplicative_identity),
inference(spm,[status(thm)],[c_0_55,c_0_28]) ).
cnf(c_0_59,plain,
( product(X1,X2,X3)
| ~ sum(additive_identity,multiply(multiplicative_identity,X1),X3) ),
inference(spm,[status(thm)],[c_0_56,c_0_48]) ).
cnf(c_0_60,plain,
sum(additive_identity,X1,multiplicative_identity),
inference(spm,[status(thm)],[c_0_41,c_0_57]) ).
cnf(c_0_61,plain,
( product(X1,X2,X3)
| ~ sum(X2,multiply(X4,additive_identity),X3)
| ~ sum(X2,X4,X1) ),
inference(spm,[status(thm)],[c_0_35,c_0_23]) ).
cnf(c_0_62,plain,
( product(multiplicative_identity,X1,X2)
| ~ product(multiplicative_identity,X3,X4)
| ~ sum(X4,multiplicative_identity,X2)
| ~ sum(X3,multiplicative_identity,X1) ),
inference(spm,[status(thm)],[c_0_49,c_0_58]) ).
cnf(c_0_63,plain,
product(X1,X2,multiplicative_identity),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_64,plain,
( product(X1,X1,X2)
| ~ sum(X1,multiply(additive_identity,additive_identity),X2) ),
inference(spm,[status(thm)],[c_0_61,c_0_23]) ).
cnf(c_0_65,plain,
( product(multiplicative_identity,X1,X2)
| ~ sum(add(X3,X3),multiplicative_identity,X1)
| ~ sum(X3,multiplicative_identity,X2) ),
inference(spm,[status(thm)],[c_0_62,c_0_33]) ).
cnf(c_0_66,plain,
( sum(X1,multiplicative_identity,additive_identity)
| ~ product(X2,X3,X1)
| ~ sum(X3,inverse(X2),inverse(X2)) ),
inference(spm,[status(thm)],[c_0_31,c_0_43]) ).
cnf(c_0_67,plain,
( sum(X1,multiplicative_identity,multiplicative_identity)
| ~ product(X2,X3,X1)
| ~ sum(X3,X4,inverse(X2)) ),
inference(spm,[status(thm)],[c_0_46,c_0_63]) ).
cnf(c_0_68,hypothesis,
sum(x_plus_y,z,x_plus_y__plus_z),
x_plus_y__plus_z ).
cnf(c_0_69,axiom,
( sum(X1,X6,X7)
| ~ sum(X1,X2,X3)
| ~ sum(X1,X4,X5)
| ~ product(X2,X4,X6)
| ~ product(X3,X5,X7) ),
distributivity6 ).
cnf(c_0_70,plain,
product(multiplicative_identity,multiplicative_identity,multiply(additive_identity,additive_identity)),
inference(spm,[status(thm)],[c_0_64,c_0_24]) ).
cnf(c_0_71,plain,
( product(multiplicative_identity,X1,X2)
| ~ sum(add(X2,X2),multiplicative_identity,X1) ),
inference(spm,[status(thm)],[c_0_65,c_0_48]) ).
cnf(c_0_72,plain,
sum(X1,multiplicative_identity,additive_identity),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_38]),c_0_24])]) ).
cnf(c_0_73,plain,
( sum(X1,multiplicative_identity,multiplicative_identity)
| ~ sum(multiplicative_identity,X2,inverse(add(X1,X1))) ),
inference(spm,[status(thm)],[c_0_67,c_0_38]) ).
cnf(c_0_74,hypothesis,
( product(X1,x_plus_y__plus_z,X2)
| ~ sum(x_plus_y,inverse(z),X1)
| ~ sum(x_plus_y,additive_identity,X2) ),
inference(spm,[status(thm)],[c_0_20,c_0_68]) ).
cnf(c_0_75,plain,
( sum(X1,X2,multiply(additive_identity,additive_identity))
| ~ product(X3,X4,X2)
| ~ sum(X1,X4,multiplicative_identity)
| ~ sum(X1,X3,multiplicative_identity) ),
inference(spm,[status(thm)],[c_0_69,c_0_70]) ).
cnf(c_0_76,plain,
product(multiplicative_identity,additive_identity,X1),
inference(spm,[status(thm)],[c_0_71,c_0_72]) ).
cnf(c_0_77,plain,
sum(X1,multiplicative_identity,multiplicative_identity),
inference(spm,[status(thm)],[c_0_73,c_0_24]) ).
cnf(c_0_78,hypothesis,
( product(X1,x_plus_y__plus_z,x_plus_y)
| ~ sum(x_plus_y,inverse(z),X1) ),
inference(spm,[status(thm)],[c_0_74,c_0_23]) ).
cnf(c_0_79,plain,
sum(X1,X2,multiply(additive_identity,additive_identity)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_76]),c_0_57]),c_0_77])]) ).
cnf(c_0_80,hypothesis,
product(multiply(additive_identity,additive_identity),x_plus_y__plus_z,x_plus_y),
inference(spm,[status(thm)],[c_0_78,c_0_79]) ).
cnf(c_0_81,plain,
sum(X1,X2,add(X2,X1)),
inference(spm,[status(thm)],[c_0_41,c_0_21]) ).
cnf(c_0_82,hypothesis,
sum(x,y_plus_z,x__plus_y_plus_z),
x_plus__y_plus_z ).
cnf(c_0_83,plain,
product(multiplicative_identity,multiplicative_identity,X1),
inference(spm,[status(thm)],[c_0_71,c_0_77]) ).
cnf(c_0_84,hypothesis,
( sum(X1,X2,x_plus_y)
| ~ product(X3,X4,X2)
| ~ sum(X1,X4,x_plus_y__plus_z) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_80]),c_0_79])]) ).
cnf(c_0_85,plain,
product(add(inverse(multiplicative_identity),X1),X1,X1),
inference(spm,[status(thm)],[c_0_55,c_0_81]) ).
cnf(c_0_86,hypothesis,
( product(X1,x__plus_y_plus_z,X2)
| ~ sum(x,inverse(y_plus_z),X1)
| ~ sum(x,additive_identity,X2) ),
inference(spm,[status(thm)],[c_0_20,c_0_82]) ).
cnf(c_0_87,plain,
( product(multiplicative_identity,X1,X2)
| ~ sum(multiplicative_identity,multiplicative_identity,X1)
| ~ sum(X3,multiplicative_identity,X2) ),
inference(spm,[status(thm)],[c_0_62,c_0_83]) ).
cnf(c_0_88,hypothesis,
( sum(X1,multiplicative_identity,x_plus_y)
| ~ sum(X1,X2,x_plus_y__plus_z) ),
inference(spm,[status(thm)],[c_0_84,c_0_63]) ).
cnf(c_0_89,plain,
( product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X4,inverse(X1),X2)
| ~ sum(X5,additive_identity,X3) ),
inference(spm,[status(thm)],[c_0_49,c_0_26]) ).
cnf(c_0_90,plain,
product(X1,add(inverse(multiplicative_identity),X1),X1),
inference(spm,[status(thm)],[c_0_32,c_0_85]) ).
cnf(c_0_91,hypothesis,
( product(X1,x__plus_y_plus_z,x)
| ~ sum(x,inverse(y_plus_z),X1) ),
inference(spm,[status(thm)],[c_0_86,c_0_23]) ).
cnf(c_0_92,plain,
( product(multiplicative_identity,X1,X2)
| ~ sum(multiplicative_identity,multiplicative_identity,X1) ),
inference(spm,[status(thm)],[c_0_87,c_0_48]) ).
cnf(c_0_93,hypothesis,
sum(multiplicative_identity,multiplicative_identity,x_plus_y),
inference(spm,[status(thm)],[c_0_88,c_0_24]) ).
cnf(c_0_94,plain,
( product(X1,X2,X3)
| ~ sum(add(inverse(multiplicative_identity),X1),inverse(X1),X2)
| ~ sum(X1,additive_identity,X3) ),
inference(spm,[status(thm)],[c_0_89,c_0_90]) ).
cnf(c_0_95,hypothesis,
product(multiply(additive_identity,additive_identity),x__plus_y_plus_z,x),
inference(spm,[status(thm)],[c_0_91,c_0_79]) ).
cnf(c_0_96,hypothesis,
product(multiplicative_identity,x_plus_y,X1),
inference(spm,[status(thm)],[c_0_92,c_0_93]) ).
cnf(c_0_97,plain,
( product(X1,X2,X1)
| ~ sum(add(inverse(multiplicative_identity),X1),inverse(X1),X2) ),
inference(spm,[status(thm)],[c_0_94,c_0_23]) ).
cnf(c_0_98,hypothesis,
( sum(X1,X2,x)
| ~ product(X3,X4,X2)
| ~ sum(X1,X4,x__plus_y_plus_z) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_95]),c_0_79])]) ).
cnf(c_0_99,hypothesis,
product(x_plus_y,multiplicative_identity,X1),
inference(spm,[status(thm)],[c_0_32,c_0_96]) ).
cnf(c_0_100,plain,
product(X1,multiply(additive_identity,additive_identity),X1),
inference(spm,[status(thm)],[c_0_97,c_0_79]) ).
cnf(c_0_101,plain,
( product(X1,X2,X3)
| ~ product(X1,X4,X5)
| ~ sum(X4,inverse(X1),X2)
| ~ sum(X5,multiplicative_identity,X3) ),
inference(spm,[status(thm)],[c_0_49,c_0_43]) ).
cnf(c_0_102,hypothesis,
( sum(X1,X2,x)
| ~ sum(X1,multiplicative_identity,x__plus_y_plus_z) ),
inference(spm,[status(thm)],[c_0_98,c_0_99]) ).
cnf(c_0_103,plain,
( sum(X1,X2,X3)
| ~ product(X3,X4,X2)
| ~ product(X3,X5,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_100]),c_0_79])]) ).
cnf(c_0_104,plain,
( product(X1,X2,X3)
| ~ sum(X4,inverse(X1),X2)
| ~ sum(multiplicative_identity,multiplicative_identity,X3) ),
inference(spm,[status(thm)],[c_0_101,c_0_63]) ).
cnf(c_0_105,hypothesis,
sum(x__plus_y_plus_z,X1,x),
inference(spm,[status(thm)],[c_0_102,c_0_48]) ).
cnf(c_0_106,plain,
( sum(X1,multiplicative_identity,X2)
| ~ product(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_103,c_0_63]) ).
cnf(c_0_107,hypothesis,
( product(X1,x,X2)
| ~ sum(multiplicative_identity,multiplicative_identity,X2) ),
inference(spm,[status(thm)],[c_0_104,c_0_105]) ).
cnf(c_0_108,plain,
sum(multiplicative_identity,multiplicative_identity,X1),
inference(spm,[status(thm)],[c_0_106,c_0_63]) ).
cnf(c_0_109,plain,
( sum(X1,X2,X2)
| ~ product(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_103,c_0_100]) ).
cnf(c_0_110,hypothesis,
product(X1,x,X2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_107,c_0_108])]) ).
cnf(c_0_111,hypothesis,
sum(X1,X2,X2),
inference(spm,[status(thm)],[c_0_109,c_0_110]) ).
cnf(c_0_112,plain,
( product(X1,X2,X3)
| ~ sum(X4,inverse(X1),X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_104,c_0_108])]) ).
cnf(c_0_113,hypothesis,
sum(X1,X2,X1),
inference(spm,[status(thm)],[c_0_41,c_0_111]) ).
cnf(c_0_114,hypothesis,
product(X1,X2,X3),
inference(spm,[status(thm)],[c_0_112,c_0_113]),
[final] ).
cnf(c_0_115,negated_conjecture,
x__plus_y_plus_z != x_plus_y__plus_z,
prove_equality,
[final] ).
cnf(c_0_116,plain,
sum(X1,X2,X3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_103,c_0_114]),c_0_114])]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : BOO008-3 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n002.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 10:44:46 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 8.63/5.96 % Version : CSE_E---1.7
% 8.63/5.96 % Problem : theBenchmark.p
% 8.63/5.96 % SZS status Satisfiable for theBenchmark.p
% 8.63/5.96 % SZS output start Saturation
% See solution above
% 8.63/6.00 % Total time : 4.369s
%------------------------------------------------------------------------------