%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM844+2 : TPTP v9.2.1. Released v4.1.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 : n026.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:42 PM UTC 2026
% Result : Theorem 0.26s 1.62s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_28)
% Comments :
%------------------------------------------------------------------------------
fof('holds(266, 415, 3)',conjecture,
vplus(vmul(vd411,vd413),vplus(vd413,vsucc(vd411))) = vplus(vmul(vd411,vd413),vplus(vsucc(vd411),vd413)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(266, 415, 3)') ).
fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
! [X16,X17] :
( vplus(X16,vsucc(X17)) = vsucc(vplus(X16,X17))
& vplus(X16,v1) = vsucc(X16) ),
file('/export/starexec/sandbox2/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,
! [X2,X3] :
( vmul(X2,vsucc(X3)) = vplus(vmul(X2,X3),X2)
& vmul(X2,v1) = X2 ),
file('/export/starexec/sandbox2/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,
! [X10,X11] : vplus(vsucc(X10),X11) = vsucc(vplus(X10,X11)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(52, 0), 0)') ).
fof('ass(cond(6, 0), 0)',axiom,
! [X20,X21] :
( X20 != X21
=> vsucc(X20) != vsucc(X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(6, 0), 0)') ).
fof('ass(cond(43, 0), 0)',axiom,
! [X12] : vplus(v1,X12) = vsucc(X12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(43, 0), 0)') ).
fof('ass(cond(12, 0), 0)',axiom,
! [X19] : vsucc(X19) != X19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(12, 0), 0)') ).
fof('ass(cond(20, 0), 0)',axiom,
! [X18] :
( X18 != v1
=> X18 = vsucc(vskolem2(X18)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(20, 0), 0)') ).
fof('holds(266, 415, 1)',axiom,
vplus(vmul(vsucc(vd411),vd413),vsucc(vd411)) = vplus(vplus(vmul(vd411,vd413),vd413),vsucc(vd411)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(266, 415, 1)') ).
fof('holds(266, 415, 2)',axiom,
vplus(vplus(vmul(vd411,vd413),vd413),vsucc(vd411)) = vplus(vmul(vd411,vd413),vplus(vd413,vsucc(vd411))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(266, 415, 2)') ).
fof('holds(266, 415, 0)',axiom,
vmul(vsucc(vd411),vsucc(vd413)) = vplus(vmul(vsucc(vd411),vd413),vsucc(vd411)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(266, 415, 0)') ).
fof('ass(cond(33, 0), 0)',axiom,
! [X13,X14,X15] : vplus(vplus(X13,X14),X15) = vplus(X13,vplus(X14,X15)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(33, 0), 0)') ).
fof('ass(cond(241, 0), 0)',axiom,
! [X4,X5] :
( less(X4,vplus(X5,v1))
=> leq(X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(241, 0), 0)') ).
fof('holds(265, 414, 0)',axiom,
vmul(vsucc(vd411),vd413) = vplus(vmul(vd411,vd413),vd413),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(265, 414, 0)') ).
fof('ass(cond(234, 0), 0)',axiom,
! [X6,X7] :
( greater(X6,X7)
=> geq(X6,vplus(X7,v1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(234, 0), 0)') ).
fof('holds(264, 412, 0)',axiom,
vmul(vsucc(vd411),v1) = vsucc(vd411),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(264, 412, 0)') ).
fof('holds(264, 412, 1)',axiom,
vsucc(vd411) = vsucc(vmul(vd411,v1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(264, 412, 1)') ).
fof('ass(cond(61, 0), 0)',axiom,
! [X8,X9] : vplus(X9,X8) = vplus(X8,X9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
fof('ass(cond(253, 0), 0)',axiom,
! [X1] : vmul(v1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(253, 0), 0)') ).
fof(i_0_19,negated_conjecture,
vplus(vmul(vd411,vd413),vplus(vd413,vsucc(vd411))) != vplus(vmul(vd411,vd413),vplus(vsucc(vd411),vd413)),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],['holds(266, 415, 3)'])]) ).
fof(i_0_20,plain,
! [X58,X59] :
( vplus(X58,vsucc(X59)) = vsucc(vplus(X58,X59))
& vplus(X58,v1) = vsucc(X58) ),
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_21,plain,
! [X44,X45] :
( vmul(X44,vsucc(X45)) = vplus(vmul(X44,X45),X44)
& vmul(X44,v1) = X44 ),
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_22,plain,
! [X52,X53] : vplus(vsucc(X52),X53) = vsucc(vplus(X52,X53)),
inference(variable_rename,[status(thm)],['ass(cond(52, 0), 0)']) ).
fof(i_0_23,plain,
! [X62,X63] :
( X62 = X63
| vsucc(X62) != vsucc(X63) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(6, 0), 0)'])]) ).
fof(i_0_24,plain,
! [X54] : vplus(v1,X54) = vsucc(X54),
inference(variable_rename,[status(thm)],['ass(cond(43, 0), 0)']) ).
fof(i_0_25,plain,
! [X61] : vsucc(X61) != X61,
inference(variable_rename,[status(thm)],['ass(cond(12, 0), 0)']) ).
fof(i_0_26,plain,
! [X60] :
( X60 = v1
| X60 = vsucc(vskolem2(X60)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(20, 0), 0)'])]) ).
cnf(i_0_27,negated_conjecture,
vplus(vmul(vd411,vd413),vplus(vd413,vsucc(vd411))) != vplus(vmul(vd411,vd413),vplus(vsucc(vd411),vd413)),
inference(split_conjunct,[status(thm)],[i_0_19]) ).
cnf(i_0_28,plain,
vplus(X1,v1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_20]) ).
cnf(i_0_29,plain,
vplus(vmul(vsucc(vd411),vd413),vsucc(vd411)) = vplus(vplus(vmul(vd411,vd413),vd413),vsucc(vd411)),
inference(split_conjunct,[status(thm)],['holds(266, 415, 1)']) ).
cnf(i_0_30,plain,
vplus(vplus(vmul(vd411,vd413),vd413),vsucc(vd411)) = vplus(vmul(vd411,vd413),vplus(vd413,vsucc(vd411))),
inference(split_conjunct,[status(thm)],['holds(266, 415, 2)']) ).
cnf(i_0_31,plain,
vmul(vsucc(vd411),vsucc(vd413)) = vplus(vmul(vsucc(vd411),vd413),vsucc(vd411)),
inference(split_conjunct,[status(thm)],['holds(266, 415, 0)']) ).
fof(i_0_32,plain,
! [X55,X56,X57] : vplus(vplus(X55,X56),X57) = vplus(X55,vplus(X56,X57)),
inference(variable_rename,[status(thm)],['ass(cond(33, 0), 0)']) ).
cnf(i_0_33,plain,
vmul(X1,vsucc(X2)) = vplus(vmul(X1,X2),X1),
inference(split_conjunct,[status(thm)],[i_0_21]) ).
cnf(i_0_34,plain,
vplus(vsucc(X1),X2) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_22]) ).
cnf(i_0_35,plain,
vplus(X1,vsucc(X2)) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_20]) ).
fof(i_0_36,plain,
! [X46,X47] :
( ~ less(X46,vplus(X47,v1))
| leq(X46,X47) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(241, 0), 0)'])]) ).
cnf(i_0_37,plain,
vmul(vsucc(vd411),vd413) = vplus(vmul(vd411,vd413),vd413),
inference(split_conjunct,[status(thm)],['holds(265, 414, 0)']) ).
fof(i_0_38,plain,
! [X48,X49] :
( ~ greater(X48,X49)
| geq(X48,vplus(X49,v1)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(234, 0), 0)'])]) ).
cnf(i_0_39,plain,
vmul(vsucc(vd411),v1) = vsucc(vd411),
inference(split_conjunct,[status(thm)],['holds(264, 412, 0)']) ).
cnf(i_0_40,plain,
vsucc(vd411) = vsucc(vmul(vd411,v1)),
inference(split_conjunct,[status(thm)],['holds(264, 412, 1)']) ).
cnf(i_0_41,plain,
( X1 = X2
| vsucc(X1) != vsucc(X2) ),
inference(split_conjunct,[status(thm)],[i_0_23]) ).
fof(i_0_42,plain,
! [X50,X51] : vplus(X51,X50) = vplus(X50,X51),
inference(variable_rename,[status(thm)],['ass(cond(61, 0), 0)']) ).
cnf(i_0_43,plain,
vplus(v1,X1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_24]) ).
cnf(i_0_44,plain,
vsucc(X1) != X1,
inference(split_conjunct,[status(thm)],[i_0_25]) ).
cnf(i_0_45,plain,
( X1 = v1
| X1 = vsucc(vskolem2(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_26]) ).
fof(i_0_46,plain,
! [X43] : vmul(v1,X43) = X43,
inference(variable_rename,[status(thm)],['ass(cond(253, 0), 0)']) ).
cnf(i_0_47,negated_conjecture,
vplus(vmul(vd411,vd413),vplus(vd413,vplus(vd411,v1))) != vplus(vmul(vd411,vd413),vplus(vplus(vd411,v1),vd413)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_27,c_0_28]),c_0_28]),
[final] ).
cnf(i_0_48,plain,
vplus(vplus(vmul(vd411,vd413),vd413),vplus(vd411,v1)) = vplus(vmul(vplus(vd411,v1),vd413),vplus(vd411,v1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_29,c_0_28]),c_0_28]),c_0_28]),
[final] ).
cnf(i_0_49,plain,
vplus(vplus(vmul(vd411,vd413),vd413),vplus(vd411,v1)) = vplus(vmul(vd411,vd413),vplus(vd413,vplus(vd411,v1))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_30,c_0_28]),c_0_28]),
[final] ).
cnf(i_0_50,plain,
vmul(vplus(vd411,v1),vplus(vd413,v1)) = vplus(vmul(vplus(vd411,v1),vd413),vplus(vd411,v1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_31,c_0_28]),c_0_28]),c_0_28]),c_0_28]),
[final] ).
cnf(i_0_51,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_52,plain,
vmul(X1,vplus(X2,v1)) = vplus(vmul(X1,X2),X1),
inference(rw,[status(thm)],[i_0_33,c_0_28]),
[final] ).
cnf(i_0_53,plain,
vplus(vplus(X1,v1),X2) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_34,c_0_28]),c_0_28]),
[final] ).
cnf(i_0_54,plain,
vplus(X1,vplus(X2,v1)) = vplus(vplus(X1,X2),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_35,c_0_28]),c_0_28]),
[final] ).
cnf(i_0_55,plain,
( leq(X1,X2)
| ~ less(X1,vplus(X2,v1)) ),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_56,plain,
vplus(vmul(vd411,vd413),vd413) = vmul(vplus(vd411,v1),vd413),
inference(rw,[status(thm)],[i_0_37,c_0_28]),
[final] ).
cnf(i_0_57,plain,
( geq(X1,vplus(X2,v1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_58,plain,
vmul(vplus(vd411,v1),v1) = vplus(vd411,v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_39,c_0_28]),c_0_28]),
[final] ).
cnf(i_0_59,plain,
vplus(vd411,v1) = vplus(vmul(vd411,v1),v1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_40,c_0_28]),c_0_28]),
[final] ).
cnf(i_0_60,plain,
( X1 = X2
| vplus(X1,v1) != vplus(X2,v1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_41,c_0_28]),c_0_28]),
[final] ).
cnf(i_0_61,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_62,plain,
vplus(v1,X1) = vplus(X1,v1),
inference(rw,[status(thm)],[i_0_43,c_0_28]),
[final] ).
cnf(i_0_63,plain,
vplus(X1,v1) != X1,
inference(rw,[status(thm)],[i_0_44,c_0_28]),
[final] ).
cnf(i_0_64,plain,
( X1 = v1
| X1 = vplus(vskolem2(X1),v1) ),
inference(rw,[status(thm)],[i_0_45,c_0_28]),
[final] ).
cnf(i_0_65,plain,
vmul(v1,X1) = X1,
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_66,plain,
vmul(X1,v1) = X1,
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_67,axiom,
X1 = X1 ).
cnf(i_0_68,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_69,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_70,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_71,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_72,axiom,
( X1 != X2
| vmul(X1,X3) = vmul(X2,X3) ) ).
cnf(i_0_73,axiom,
( X1 != X2
| vmul(X3,X1) = vmul(X3,X2) ) ).
cnf(i_0_74,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_75,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_76,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_77,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_78,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_79,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_80,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_81,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_67_001,axiom,
X1 = X1 ).
cnf(i_0_68_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_69_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_70_004,axiom,
( X1 != X2
| vplus(X1,X3) = vplus(X2,X3) ) ).
cnf(i_0_71_005,axiom,
( X1 != X2
| vplus(X3,X1) = vplus(X3,X2) ) ).
cnf(i_0_72_006,axiom,
( X1 != X2
| vmul(X1,X3) = vmul(X2,X3) ) ).
cnf(i_0_73_007,axiom,
( X1 != X2
| vmul(X3,X1) = vmul(X3,X2) ) ).
cnf(i_0_74_008,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_75_009,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_76_010,axiom,
( X1 != X2
| ~ less(X1,X3)
| less(X2,X3) ) ).
cnf(i_0_77_011,axiom,
( X1 != X2
| ~ less(X3,X1)
| less(X3,X2) ) ).
cnf(i_0_78_012,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_79_013,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_80_014,axiom,
( X1 != X2
| ~ greater(X1,X3)
| greater(X2,X3) ) ).
cnf(i_0_81_015,axiom,
( X1 != X2
| ~ greater(X3,X1)
| greater(X3,X2) ) ).
cnf(i_0_82,plain,
X1 = X1,
inference(equality_inference,[],[60]) ).
cnf(i_0_83,plain,
$false,
inference(scs_inference,[],[i_0_47,i_0_61,i_0_71]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM844+2 : TPTP v9.2.1. Released v4.1.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.14/0.33 % Computer : n026.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Tue May 5 01:15:53 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 0.26/1.62 % Version : CSE_E---1.7
% 0.26/1.62 % Problem : theBenchmark.p
% 0.26/1.62 % SZS status Theorem for theBenchmark.p
% 0.26/1.62 % SZS output start CNFRefutation
% See solution above
% 0.26/1.63 % Total time : 1.272s
%------------------------------------------------------------------------------