%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM848+2 : TPTP v9.2.1. Released v4.1.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 : n024.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:58:43 PM UTC 2026
% Result : Theorem 0.17s 1.51s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_23)
% Comments :
%------------------------------------------------------------------------------
fof('holds(286, 441, 4)',conjecture,
vplus(vmul(vd436,vd437),vplus(vmul(vd436,vd439),vd436)) = vplus(vmul(vd436,vd437),vmul(vd436,vsucc(vd439))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(286, 441, 4)') ).
fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
! [X13,X14] :
( vplus(X13,vsucc(X14)) = vsucc(vplus(X13,X14))
& vplus(X13,v1) = vsucc(X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))') ).
fof('qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))',axiom,
! [X1,X2] :
( vmul(X1,vsucc(X2)) = vplus(vmul(X1,X2),X1)
& vmul(X1,v1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))') ).
fof('ass(cond(52, 0), 0)',axiom,
! [X7,X8] : vplus(vsucc(X7),X8) = vsucc(vplus(X7,X8)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(52, 0), 0)') ).
fof('ass(cond(43, 0), 0)',axiom,
! [X9] : vplus(v1,X9) = vsucc(X9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(43, 0), 0)') ).
fof('ass(cond(20, 0), 0)',axiom,
! [X15] :
( X15 != v1
=> X15 = vsucc(vskolem2(X15)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(20, 0), 0)') ).
fof('holds(286, 441, 1)',axiom,
vmul(vd436,vsucc(vplus(vd437,vd439))) = vplus(vmul(vd436,vplus(vd437,vd439)),vd436),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(286, 441, 1)') ).
fof('holds(286, 441, 0)',axiom,
vmul(vd436,vplus(vd437,vsucc(vd439))) = vmul(vd436,vsucc(vplus(vd437,vd439))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(286, 441, 0)') ).
fof('ass(cond(33, 0), 0)',axiom,
! [X10,X11,X12] : vplus(vplus(X10,X11),X12) = vplus(X10,vplus(X11,X12)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(33, 0), 0)') ).
fof('ass(cond(241, 0), 0)',axiom,
! [X3,X4] :
( less(X3,vplus(X4,v1))
=> leq(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(241, 0), 0)') ).
fof('holds(284, 438, 1)',axiom,
vmul(vd436,vsucc(vd437)) = vplus(vmul(vd436,vd437),vd436),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(284, 438, 1)') ).
fof('ass(cond(61, 0), 0)',axiom,
! [X5,X6] : vplus(X6,X5) = vplus(X5,X6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
fof('holds(286, 441, 3)',axiom,
vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436) = vplus(vmul(vd436,vd437),vplus(vmul(vd436,vd439),vd436)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(286, 441, 3)') ).
fof('holds(286, 441, 2)',axiom,
vplus(vmul(vd436,vplus(vd437,vd439)),vd436) = vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(286, 441, 2)') ).
fof('holds(284, 438, 2)',axiom,
vplus(vmul(vd436,vd437),vd436) = vplus(vmul(vd436,vd437),vmul(vd436,v1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(284, 438, 2)') ).
fof('holds(285, 440, 0)',axiom,
vmul(vd436,vplus(vd437,vd439)) = vplus(vmul(vd436,vd437),vmul(vd436,vd439)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','holds(285, 440, 0)') ).
fof(i_0_16,negated_conjecture,
vplus(vmul(vd436,vd437),vplus(vmul(vd436,vd439),vd436)) != vplus(vmul(vd436,vd437),vmul(vd436,vsucc(vd439))),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],['holds(286, 441, 4)'])]) ).
fof(i_0_17,plain,
! [X43,X44] :
( vplus(X43,vsucc(X44)) = vsucc(vplus(X43,X44))
& vplus(X43,v1) = vsucc(X43) ),
inference(variable_rename,[status(thm)],['qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))']) ).
fof(i_0_18,plain,
! [X31,X32] :
( vmul(X31,vsucc(X32)) = vplus(vmul(X31,X32),X31)
& vmul(X31,v1) = X31 ),
inference(variable_rename,[status(thm)],['qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))']) ).
fof(i_0_19,plain,
! [X37,X38] : vplus(vsucc(X37),X38) = vsucc(vplus(X37,X38)),
inference(variable_rename,[status(thm)],['ass(cond(52, 0), 0)']) ).
fof(i_0_20,plain,
! [X39] : vplus(v1,X39) = vsucc(X39),
inference(variable_rename,[status(thm)],['ass(cond(43, 0), 0)']) ).
fof(i_0_21,plain,
! [X45] :
( X45 = v1
| X45 = vsucc(vskolem2(X45)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(20, 0), 0)'])]) ).
cnf(i_0_22,negated_conjecture,
vplus(vmul(vd436,vd437),vplus(vmul(vd436,vd439),vd436)) != vplus(vmul(vd436,vd437),vmul(vd436,vsucc(vd439))),
inference(split_conjunct,[status(thm)],[i_0_16]) ).
cnf(i_0_23,plain,
vplus(X1,v1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_17]) ).
cnf(i_0_24,plain,
vmul(vd436,vsucc(vplus(vd437,vd439))) = vplus(vmul(vd436,vplus(vd437,vd439)),vd436),
inference(split_conjunct,[status(thm)],['holds(286, 441, 1)']) ).
cnf(i_0_25,plain,
vmul(vd436,vplus(vd437,vsucc(vd439))) = vmul(vd436,vsucc(vplus(vd437,vd439))),
inference(split_conjunct,[status(thm)],['holds(286, 441, 0)']) ).
fof(i_0_26,plain,
! [X40,X41,X42] : vplus(vplus(X40,X41),X42) = vplus(X40,vplus(X41,X42)),
inference(variable_rename,[status(thm)],['ass(cond(33, 0), 0)']) ).
cnf(i_0_27,plain,
vmul(X1,vsucc(X2)) = vplus(vmul(X1,X2),X1),
inference(split_conjunct,[status(thm)],[i_0_18]) ).
cnf(i_0_28,plain,
vplus(vsucc(X1),X2) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_19]) ).
cnf(i_0_29,plain,
vplus(X1,vsucc(X2)) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_17]) ).
fof(i_0_30,plain,
! [X33,X34] :
( ~ less(X33,vplus(X34,v1))
| leq(X33,X34) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(241, 0), 0)'])]) ).
cnf(i_0_31,plain,
vmul(vd436,vsucc(vd437)) = vplus(vmul(vd436,vd437),vd436),
inference(split_conjunct,[status(thm)],['holds(284, 438, 1)']) ).
fof(i_0_32,plain,
! [X35,X36] : vplus(X36,X35) = vplus(X35,X36),
inference(variable_rename,[status(thm)],['ass(cond(61, 0), 0)']) ).
cnf(i_0_33,plain,
vplus(v1,X1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_20]) ).
cnf(i_0_34,plain,
( X1 = v1
| X1 = vsucc(vskolem2(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_21]) ).
cnf(i_0_35,negated_conjecture,
vplus(vmul(vd436,vd437),vplus(vmul(vd436,vd439),vd436)) != vplus(vmul(vd436,vd437),vmul(vd436,vplus(vd439,v1))),
inference(rw,[status(thm)],[i_0_22,c_0_23]),
[final] ).
cnf(i_0_36,plain,
vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436) = vplus(vmul(vd436,vd437),vplus(vmul(vd436,vd439),vd436)),
inference(split_conjunct,[status(thm)],['holds(286, 441, 3)']),
[final] ).
cnf(i_0_37,plain,
vplus(vmul(vd436,vplus(vd437,vd439)),vd436) = vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),
inference(split_conjunct,[status(thm)],['holds(286, 441, 2)']),
[final] ).
cnf(i_0_38,plain,
vmul(vd436,vplus(vplus(vd437,vd439),v1)) = vplus(vmul(vd436,vplus(vd437,vd439)),vd436),
inference(rw,[status(thm)],[i_0_24,c_0_23]),
[final] ).
cnf(i_0_39,plain,
vmul(vd436,vplus(vd437,vplus(vd439,v1))) = vmul(vd436,vplus(vplus(vd437,vd439),v1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_25,c_0_23]),c_0_23]),
[final] ).
cnf(i_0_40,plain,
vplus(vmul(vd436,vd437),vd436) = vplus(vmul(vd436,vd437),vmul(vd436,v1)),
inference(split_conjunct,[status(thm)],['holds(284, 438, 2)']),
[final] ).
cnf(i_0_41,plain,
vmul(vd436,vplus(vd437,vd439)) = vplus(vmul(vd436,vd437),vmul(vd436,vd439)),
inference(split_conjunct,[status(thm)],['holds(285, 440, 0)']),
[final] ).
cnf(i_0_42,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_43,plain,
vmul(X1,vplus(X2,v1)) = vplus(vmul(X1,X2),X1),
inference(rw,[status(thm)],[i_0_27,c_0_23]),
[final] ).
cnf(i_0_44,plain,
vplus(vplus(X1,v1),X2) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_28,c_0_23]),c_0_23]),
[final] ).
cnf(i_0_45,plain,
vplus(X1,vplus(X2,v1)) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_29,c_0_23]),c_0_23]),
[final] ).
cnf(i_0_46,plain,
( leq(X1,X2)
| ~ less(X1,vplus(X2,v1)) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_47,plain,
vmul(vd436,vplus(vd437,v1)) = vplus(vmul(vd436,vd437),vd436),
inference(rw,[status(thm)],[i_0_31,c_0_23]),
[final] ).
cnf(i_0_48,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_49,plain,
vplus(v1,X1) = vplus(X1,v1),
inference(rw,[status(thm)],[i_0_33,c_0_23]),
[final] ).
cnf(i_0_50,plain,
( X1 = v1
| X1 = vplus(vskolem2(X1),v1) ),
inference(rw,[status(thm)],[i_0_34,c_0_23]),
[final] ).
cnf(i_0_51,plain,
vmul(X1,v1) = X1,
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_52,axiom,
X1 = X1 ).
cnf(i_0_53,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_54,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_55,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_56,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_57,axiom,
( X1 != X2
| vmul(X1,X3) = vmul(X2,X3) ) ).
cnf(i_0_58,axiom,
( X1 != X2
| vmul(X3,X1) = vmul(X3,X2) ) ).
cnf(i_0_59,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_60,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_61,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_62,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_52_001,axiom,
X1 = X1 ).
cnf(i_0_53_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_54_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_55_004,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_56_005,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_57_006,axiom,
( X1 != X2
| vmul(X1,X3) = vmul(X2,X3) ) ).
cnf(i_0_58_007,axiom,
( X1 != X2
| vmul(X3,X1) = vmul(X3,X2) ) ).
cnf(i_0_59_008,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_60_009,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_61_010,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_62_011,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_63,plain,
vplus(vmul(vd436,vd439),vd436) != vmul(vd436,vplus(vd439,v1)),
inference(scs_inference,[],[i_0_35,i_0_56]) ).
cnf(i_0_64,plain,
X1 = vmul(X1,v1),
inference(scs_inference,[],[i_0_35,i_0_51,i_0_56,i_0_53]) ).
cnf(i_0_65,plain,
vplus(vmul(vd436,vd437),vplus(vmul(vd436,vd439),vd436)) != vplus(vmul(vd436,vplus(vd439,v1)),vmul(vd436,vd437)),
inference(scs_inference,[],[i_0_35,i_0_48,i_0_51,i_0_56,i_0_53,i_0_54]) ).
cnf(i_0_66,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_67,plain,
vplus(X1,vplus(X2,X3)) = vplus(vplus(X1,X2),X3),
inference(scs_inference,[],[i_0_42,i_0_53]) ).
cnf(i_0_68,plain,
vplus(vplus(X1,X2),X3) = vmul(vplus(X1,vplus(X2,X3)),v1),
inference(scs_inference,[],[i_0_64,i_0_42,i_0_53,i_0_54]) ).
cnf(i_0_69,plain,
X1 = vmul(X1,v1),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_70,plain,
vmul(vplus(X1,vplus(X2,X3)),v1) = vplus(vplus(X1,X2),X3),
inference(scs_inference,[],[i_0_68,i_0_53]) ).
cnf(i_0_71,plain,
vmul(vplus(X1,X2),vplus(X3,v1)) = vplus(vplus(vmul(vplus(X1,X2),X3),X1),X2),
inference(scs_inference,[],[i_0_67,i_0_68,i_0_43,i_0_53,i_0_54]) ).
cnf(i_0_72,plain,
vplus(X1,vplus(X2,X3)) = vplus(vplus(X1,X2),X3),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_73,plain,
vmul(X1,vplus(X2,v1)) = vplus(vmul(X1,X2),X1),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_74,plain,
vplus(vplus(vmul(vplus(X1,X2),X3),X1),X2) = vmul(vplus(X1,X2),vplus(X3,v1)),
inference(scs_inference,[],[i_0_71,i_0_53]) ).
cnf(i_0_75,plain,
vmul(vplus(X1,X2),vplus(X3,v1)) = vmul(vplus(vmul(vplus(X1,X2),X3),vplus(X1,X2)),v1),
inference(scs_inference,[],[i_0_71,i_0_68,i_0_53,i_0_54]) ).
cnf(i_0_76,plain,
vplus(vplus(X1,X2),X3) = vmul(vplus(X1,vplus(X2,X3)),v1),
inference(rename_variables,[],[i_0_68]) ).
cnf(i_0_77,plain,
vmul(vplus(vmul(vplus(X1,X2),X3),vplus(X1,X2)),v1) = vmul(vplus(X1,X2),vplus(X3,v1)),
inference(scs_inference,[],[i_0_75,i_0_53]) ).
cnf(i_0_78,plain,
vmul(vmul(vd436,vplus(vd437,vd439)),v1) = vplus(vmul(vd436,vd437),vmul(vd436,vd439)),
inference(scs_inference,[],[i_0_75,i_0_41,i_0_51,i_0_53,i_0_54]) ).
cnf(i_0_79,plain,
vmul(X1,v1) = X1,
inference(rename_variables,[],[i_0_51]) ).
cnf(i_0_80,plain,
vplus(vmul(vd436,vd437),vmul(vd436,vd439)) = vmul(vmul(vd436,vplus(vd437,vd439)),v1),
inference(scs_inference,[],[i_0_78,i_0_53]) ).
cnf(i_0_81,plain,
vplus(vmul(vplus(X1,X2),X3),vplus(X1,X2)) = vmul(vplus(X1,X2),vplus(X3,v1)),
inference(scs_inference,[],[i_0_78,i_0_77,i_0_64,i_0_53,i_0_54]) ).
cnf(i_0_82,plain,
X1 = vmul(X1,v1),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_83,plain,
vplus(vplus(X1,X2),v1) = vplus(vplus(X1,v1),X2),
inference(scs_inference,[],[i_0_44,i_0_53]) ).
cnf(i_0_84,plain,
vplus(vplus(X1,X2),vmul(vplus(X1,X2),X3)) = vmul(vplus(X1,X2),vplus(X3,v1)),
inference(scs_inference,[],[i_0_81,i_0_44,i_0_48,i_0_53,i_0_54]) ).
cnf(i_0_85,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_86,plain,
vmul(vplus(X1,X2),vplus(X3,v1)) = vplus(vplus(X1,X2),vmul(vplus(X1,X2),X3)),
inference(scs_inference,[],[i_0_84,i_0_53]) ).
cnf(i_0_87,plain,
vmul(vd436,vplus(vd437,v1)) = vplus(vmul(vd436,vd437),vmul(vd436,v1)),
inference(scs_inference,[],[i_0_84,i_0_40,i_0_43,i_0_53,i_0_54]) ).
cnf(i_0_88,plain,
vmul(X1,vplus(X2,v1)) = vplus(vmul(X1,X2),X1),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_89,plain,
vplus(vmul(vd436,vd437),vmul(vd436,v1)) = vmul(vd436,vplus(vd437,v1)),
inference(scs_inference,[],[i_0_87,i_0_53]) ).
cnf(i_0_90,plain,
vmul(vmul(vd436,vplus(vd437,v1)),v1) = vplus(vmul(vd436,vd437),vmul(vd436,v1)),
inference(scs_inference,[],[i_0_87,i_0_51,i_0_53,i_0_54]) ).
cnf(i_0_91,plain,
vmul(X1,v1) = X1,
inference(rename_variables,[],[i_0_51]) ).
cnf(i_0_92,plain,
vplus(vmul(vd436,vd437),vmul(vd436,v1)) = vmul(vmul(vd436,vplus(vd437,v1)),v1),
inference(scs_inference,[],[i_0_90,i_0_53]) ).
cnf(i_0_93,plain,
vplus(vd436,vmul(vd436,vplus(vd437,vd439))) = vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),
inference(scs_inference,[],[i_0_90,i_0_37,i_0_48,i_0_53,i_0_54]) ).
cnf(i_0_94,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_95,plain,
vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436) = vplus(vd436,vmul(vd436,vplus(vd437,vd439))),
inference(scs_inference,[],[i_0_93,i_0_53]) ).
cnf(i_0_96,plain,
vmul(vd436,vplus(vplus(vd437,vd439),v1)) = vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),
inference(scs_inference,[],[i_0_93,i_0_37,i_0_43,i_0_53,i_0_54]) ).
cnf(i_0_97,plain,
vmul(X1,vplus(X2,v1)) = vplus(vmul(X1,X2),X1),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_98,plain,
vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436) = vmul(vd436,vplus(vplus(vd437,vd439),v1)),
inference(scs_inference,[],[i_0_96,i_0_53]) ).
cnf(i_0_99,plain,
vmul(vd436,vplus(vd437,vplus(vd439,v1))) = vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),
inference(scs_inference,[],[i_0_96,i_0_39,i_0_53,i_0_54]) ).
cnf(i_0_100,plain,
vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436) = vmul(vd436,vplus(vd437,vplus(vd439,v1))),
inference(scs_inference,[],[i_0_99,i_0_53]) ).
cnf(i_0_101,plain,
vmul(vd436,vplus(vd437,vplus(vd439,v1))) = vplus(vd436,vmul(vd436,vplus(vd437,vd439))),
inference(scs_inference,[],[i_0_99,i_0_95,i_0_53,i_0_54]) ).
cnf(i_0_102,plain,
vplus(vd436,vmul(vd436,vplus(vd437,vd439))) = vmul(vd436,vplus(vd437,vplus(vd439,v1))),
inference(scs_inference,[],[i_0_101,i_0_53]) ).
cnf(i_0_103,plain,
vplus(vd436,vmul(vd436,vd437)) = vplus(vmul(vd436,vd437),vmul(vd436,v1)),
inference(scs_inference,[],[i_0_101,i_0_40,i_0_48,i_0_53,i_0_54]) ).
cnf(i_0_104,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(rename_variables,[],[i_0_48]) ).
cnf(i_0_105,plain,
vplus(vmul(vd436,vd437),vmul(vd436,v1)) = vplus(vd436,vmul(vd436,vd437)),
inference(scs_inference,[],[i_0_103,i_0_53]) ).
cnf(i_0_106,plain,
vmul(vplus(vd436,vmul(vd436,vd437)),v1) = vplus(vmul(vd436,vd437),vmul(vd436,v1)),
inference(scs_inference,[],[i_0_103,i_0_51,i_0_53,i_0_54]) ).
cnf(i_0_107,plain,
vmul(X1,v1) = X1,
inference(rename_variables,[],[i_0_51]) ).
cnf(i_0_108,plain,
vplus(vmul(vd436,vd437),vmul(vd436,v1)) = vmul(vplus(vd436,vmul(vd436,vd437)),v1),
inference(scs_inference,[],[i_0_106,i_0_53]) ).
cnf(i_0_109,plain,
vmul(vplus(vd436,vmul(vd436,vd437)),v1) = vmul(vd436,vplus(vd437,v1)),
inference(scs_inference,[],[i_0_106,i_0_89,i_0_53,i_0_54]) ).
cnf(i_0_110,plain,
vmul(vd436,vplus(vd437,v1)) = vmul(vplus(vd436,vmul(vd436,vd437)),v1),
inference(scs_inference,[],[i_0_109,i_0_53]) ).
cnf(i_0_111,plain,
vmul(vmul(vd436,vplus(vd437,v1)),v1) = vplus(vd436,vmul(vd436,vd437)),
inference(scs_inference,[],[i_0_109,i_0_105,i_0_90,i_0_53,i_0_54]) ).
cnf(i_0_112,plain,
vplus(vd436,vmul(vd436,vd437)) = vmul(vmul(vd436,vplus(vd437,v1)),v1),
inference(scs_inference,[],[i_0_111,i_0_53]) ).
cnf(i_0_113,plain,
vmul(vd436,vplus(vd437,v1)) = vplus(vd436,vmul(vd436,vd437)),
inference(scs_inference,[],[i_0_111,i_0_105,i_0_87,i_0_53,i_0_54]) ).
cnf(i_0_114,plain,
vplus(vd436,vmul(vd436,vd437)) = vmul(vd436,vplus(vd437,v1)),
inference(scs_inference,[],[i_0_113,i_0_53]) ).
cnf(i_0_115,plain,
vmul(vplus(X1,X2),vplus(X3,v1)) = vplus(X1,vplus(X2,vmul(vplus(X1,X2),X3))),
inference(scs_inference,[],[i_0_86,i_0_113,i_0_42,i_0_53,i_0_54]) ).
cnf(i_0_116,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_117,plain,
vplus(X1,vplus(X2,vmul(vplus(X1,X2),X3))) = vmul(vplus(X1,X2),vplus(X3,v1)),
inference(scs_inference,[],[i_0_115,i_0_53]) ).
cnf(i_0_118,plain,
vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436) = vplus(vmul(vd436,vplus(vd437,vd439)),vd436),
inference(scs_inference,[],[i_0_98,i_0_115,i_0_43,i_0_53,i_0_54]) ).
cnf(i_0_119,plain,
vmul(X1,vplus(X2,v1)) = vplus(vmul(X1,X2),X1),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_120,plain,
vplus(vmul(vd436,vd437),vmul(vd436,vd439)) = vmul(vd436,vplus(vd437,vd439)),
inference(scs_inference,[],[i_0_41,i_0_53]) ).
cnf(i_0_121,plain,
vmul(vd436,vplus(vplus(vd437,vd439),v1)) = vmul(vd436,vplus(vd437,vplus(vd439,v1))),
inference(scs_inference,[],[i_0_39,i_0_53]) ).
cnf(i_0_122,plain,
vplus(vd436,vmul(vd436,vd437)) = vmul(vmul(vmul(vd436,vplus(vd437,v1)),v1),v1),
inference(scs_inference,[],[i_0_112,i_0_64,i_0_39,i_0_53,i_0_54]) ).
cnf(i_0_123,plain,
X1 = vmul(X1,v1),
inference(rename_variables,[],[i_0_64]) ).
cnf(i_0_124,plain,
vmul(vmul(vmul(vd436,vplus(vd437,v1)),v1),v1) = vplus(vd436,vmul(vd436,vd437)),
inference(scs_inference,[],[i_0_122,i_0_53]) ).
cnf(i_0_125,plain,
vmul(vd436,vplus(vd437,v1)) = vmul(vmul(vmul(vd436,vplus(vd437,v1)),v1),v1),
inference(scs_inference,[],[i_0_122,i_0_113,i_0_53,i_0_54]) ).
cnf(i_0_126,plain,
vmul(vmul(vmul(vd436,vplus(vd437,v1)),v1),v1) = vmul(vd436,vplus(vd437,v1)),
inference(scs_inference,[],[i_0_125,i_0_53]) ).
cnf(i_0_127,plain,
vmul(vmul(vmul(vd436,vplus(vd437,v1)),v1),v1) = vplus(vmul(vd436,vd437),vmul(vd436,v1)),
inference(scs_inference,[],[i_0_125,i_0_124,i_0_103,i_0_53,i_0_54]) ).
cnf(i_0_128,plain,
vplus(vmul(vd436,vd437),vmul(vd436,v1)) = vmul(vmul(vmul(vd436,vplus(vd437,v1)),v1),v1),
inference(scs_inference,[],[i_0_127,i_0_53]) ).
cnf(i_0_129,plain,
vplus(vmul(vd436,vd437),vmul(vd436,v1)) = vplus(vmul(vd436,vd437),vd436),
inference(scs_inference,[],[i_0_40,i_0_53]) ).
cnf(i_0_130,plain,
vmul(vmul(vmul(vd436,vplus(vd437,v1)),v1),v1) = vplus(vmul(vd436,vd437),vd436),
inference(scs_inference,[],[i_0_127,i_0_40,i_0_53,i_0_54]) ).
cnf(i_0_131,plain,
vplus(vmul(vd436,vd437),vd436) = vmul(vmul(vmul(vd436,vplus(vd437,v1)),v1),v1),
inference(scs_inference,[],[i_0_130,i_0_53]) ).
cnf(i_0_132,plain,
vmul(vmul(vd436,vplus(vd437,v1)),v1) = vmul(vplus(vd436,vmul(vd436,vd437)),v1),
inference(scs_inference,[],[i_0_108,i_0_130,i_0_90,i_0_53,i_0_54]) ).
cnf(i_0_133,plain,
vmul(vplus(vd436,vmul(vd436,vd437)),v1) = vmul(vmul(vd436,vplus(vd437,v1)),v1),
inference(scs_inference,[],[i_0_132,i_0_53]) ).
cnf(i_0_134,plain,
vmul(vplus(vd436,vmul(vd436,vd437)),v1) = vplus(vmul(vd436,vd437),vd436),
inference(scs_inference,[],[i_0_132,i_0_129,i_0_106,i_0_53,i_0_54]) ).
cnf(i_0_135,plain,
vplus(vmul(vd436,vd437),vd436) = vmul(vplus(vd436,vmul(vd436,vd437)),v1),
inference(scs_inference,[],[i_0_134,i_0_53]) ).
cnf(i_0_136,plain,
$false,
inference(scs_inference,[],[i_0_63,i_0_43,i_0_53]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : NUM848+2 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.06 % 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.06/0.24 % Computer : n024.cluster.edu
% 0.06/0.24 % Model : x86_64 x86_64
% 0.06/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.24 % Memory : 8042.1875MB
% 0.06/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.24 % CPULimit : 300
% 0.06/0.24 % WCLimit : 300
% 0.06/0.24 % DateTime : Mon May 4 20:15:42 EDT 2026
% 0.06/0.24 % CPUTime :
% 0.06/0.24 % start to proof: theBenchmark
% 0.17/1.51 % Version : CSE_E---1.7
% 0.17/1.51 % Problem : theBenchmark.p
% 0.17/1.51 % SZS status Theorem for theBenchmark.p
% 0.17/1.51 % SZS output start CNFRefutation
% See solution above
% 0.17/1.57 % Total time : 1.261s
%------------------------------------------------------------------------------