%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM846+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 : n004.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.27s 1.61s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_29)
% Comments :
%------------------------------------------------------------------------------
fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
! [X19,X20] :
( vplus(X19,vsucc(X20)) = vsucc(vplus(X19,X20))
& vplus(X19,v1) = vsucc(X19) ),
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,
! [X4,X5] :
( vmul(X4,vsucc(X5)) = vplus(vmul(X4,X5),X4)
& vmul(X4,v1) = X4 ),
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,
! [X13,X14] : vplus(vsucc(X13),X14) = vsucc(vplus(X13,X14)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(52, 0), 0)') ).
fof('ass(cond(6, 0), 0)',axiom,
! [X23,X24] :
( X23 != X24
=> vsucc(X23) != vsucc(X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(6, 0), 0)') ).
fof('ass(cond(43, 0), 0)',axiom,
! [X15] : vplus(v1,X15) = vsucc(X15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(43, 0), 0)') ).
fof('ass(cond(12, 0), 0)',axiom,
! [X22] : vsucc(X22) != X22,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(12, 0), 0)') ).
fof('ass(cond(20, 0), 0)',axiom,
! [X21] :
( X21 != v1
=> X21 = vsucc(vskolem2(X21)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(20, 0), 0)') ).
fof('holds(286, 441, 2)',conjecture,
vplus(vmul(vd436,vplus(vd437,vd439)),vd436) = vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','holds(286, 441, 2)') ).
fof('holds(286, 441, 1)',axiom,
vmul(vd436,vsucc(vplus(vd437,vd439))) = vplus(vmul(vd436,vplus(vd437,vd439)),vd436),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p','holds(286, 441, 0)') ).
fof('ass(cond(33, 0), 0)',axiom,
! [X16,X17,X18] : vplus(vplus(X16,X17),X18) = vplus(X16,vplus(X17,X18)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(33, 0), 0)') ).
fof('ass(cond(241, 0), 0)',axiom,
! [X6,X7] :
( less(X6,vplus(X7,v1))
=> leq(X6,X7) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p','holds(284, 438, 1)') ).
fof('ass(cond(234, 0), 0)',axiom,
! [X8,X9] :
( greater(X8,X9)
=> geq(X8,vplus(X9,v1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(234, 0), 0)') ).
fof('ass(cond(270, 0), 0)',axiom,
! [X1,X2] : vmul(X1,X2) = vmul(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(270, 0), 0)') ).
fof('ass(cond(61, 0), 0)',axiom,
! [X11,X12] : vplus(X12,X11) = vplus(X11,X12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(61, 0), 0)') ).
fof('ass(cond(253, 0), 0)',axiom,
! [X3] : vmul(v1,X3) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(253, 0), 0)') ).
fof('ass(cond(228, 0), 0)',axiom,
! [X10] : geq(X10,v1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ass(cond(228, 0), 0)') ).
fof('holds(284, 438, 2)',axiom,
vplus(vmul(vd436,vd437),vd436) = vplus(vmul(vd436,vd437),vmul(vd436,v1)),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p','holds(285, 440, 0)') ).
fof(i_0_20,plain,
! [X67,X68] :
( vplus(X67,vsucc(X68)) = vsucc(vplus(X67,X68))
& vplus(X67,v1) = vsucc(X67) ),
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,
! [X52,X53] :
( vmul(X52,vsucc(X53)) = vplus(vmul(X52,X53),X52)
& vmul(X52,v1) = X52 ),
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,
! [X61,X62] : vplus(vsucc(X61),X62) = vsucc(vplus(X61,X62)),
inference(variable_rename,[status(thm)],['ass(cond(52, 0), 0)']) ).
fof(i_0_23,plain,
! [X71,X72] :
( X71 = X72
| vsucc(X71) != vsucc(X72) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(6, 0), 0)'])]) ).
fof(i_0_24,plain,
! [X63] : vplus(v1,X63) = vsucc(X63),
inference(variable_rename,[status(thm)],['ass(cond(43, 0), 0)']) ).
fof(i_0_25,plain,
! [X70] : vsucc(X70) != X70,
inference(variable_rename,[status(thm)],['ass(cond(12, 0), 0)']) ).
fof(i_0_26,plain,
! [X69] :
( X69 = v1
| X69 = vsucc(vskolem2(X69)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(20, 0), 0)'])]) ).
fof(i_0_27,negated_conjecture,
vplus(vmul(vd436,vplus(vd437,vd439)),vd436) != vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],['holds(286, 441, 2)'])]) ).
cnf(i_0_28,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_29,plain,
vplus(X1,v1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_20]) ).
cnf(i_0_30,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_31,plain,
! [X64,X65,X66] : vplus(vplus(X64,X65),X66) = vplus(X64,vplus(X65,X66)),
inference(variable_rename,[status(thm)],['ass(cond(33, 0), 0)']) ).
cnf(i_0_32,plain,
vmul(X1,vsucc(X2)) = vplus(vmul(X1,X2),X1),
inference(split_conjunct,[status(thm)],[i_0_21]) ).
cnf(i_0_33,plain,
vplus(vsucc(X1),X2) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_22]) ).
cnf(i_0_34,plain,
vplus(X1,vsucc(X2)) = vsucc(vplus(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_20]) ).
fof(i_0_35,plain,
! [X54,X55] :
( ~ less(X54,vplus(X55,v1))
| leq(X54,X55) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(241, 0), 0)'])]) ).
cnf(i_0_36,plain,
vmul(vd436,vsucc(vd437)) = vplus(vmul(vd436,vd437),vd436),
inference(split_conjunct,[status(thm)],['holds(284, 438, 1)']) ).
fof(i_0_37,plain,
! [X56,X57] :
( ~ greater(X56,X57)
| geq(X56,vplus(X57,v1)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['ass(cond(234, 0), 0)'])]) ).
cnf(i_0_38,plain,
( X1 = X2
| vsucc(X1) != vsucc(X2) ),
inference(split_conjunct,[status(thm)],[i_0_23]) ).
fof(i_0_39,plain,
! [X49,X50] : vmul(X49,X50) = vmul(X50,X49),
inference(variable_rename,[status(thm)],['ass(cond(270, 0), 0)']) ).
fof(i_0_40,plain,
! [X59,X60] : vplus(X60,X59) = vplus(X59,X60),
inference(variable_rename,[status(thm)],['ass(cond(61, 0), 0)']) ).
cnf(i_0_41,plain,
vplus(v1,X1) = vsucc(X1),
inference(split_conjunct,[status(thm)],[i_0_24]) ).
cnf(i_0_42,plain,
vsucc(X1) != X1,
inference(split_conjunct,[status(thm)],[i_0_25]) ).
cnf(i_0_43,plain,
( X1 = v1
| X1 = vsucc(vskolem2(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_26]) ).
fof(i_0_44,plain,
! [X51] : vmul(v1,X51) = X51,
inference(variable_rename,[status(thm)],['ass(cond(253, 0), 0)']) ).
fof(i_0_45,plain,
! [X58] : geq(X58,v1),
inference(variable_rename,[status(thm)],['ass(cond(228, 0), 0)']) ).
cnf(i_0_46,negated_conjecture,
vplus(vmul(vd436,vplus(vd437,vd439)),vd436) != vplus(vplus(vmul(vd436,vd437),vmul(vd436,vd439)),vd436),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_47,plain,
vmul(vd436,vplus(vplus(vd437,vd439),v1)) = vplus(vmul(vd436,vplus(vd437,vd439)),vd436),
inference(rw,[status(thm)],[i_0_28,c_0_29]),
[final] ).
cnf(i_0_48,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_30,c_0_29]),c_0_29]),
[final] ).
cnf(i_0_49,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_50,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_51,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_52,plain,
vmul(X1,vplus(X2,v1)) = vplus(vmul(X1,X2),X1),
inference(rw,[status(thm)],[i_0_32,c_0_29]),
[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_33,c_0_29]),c_0_29]),
[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_34,c_0_29]),c_0_29]),
[final] ).
cnf(i_0_55,plain,
( leq(X1,X2)
| ~ less(X1,vplus(X2,v1)) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_56,plain,
vmul(vd436,vplus(vd437,v1)) = vplus(vmul(vd436,vd437),vd436),
inference(rw,[status(thm)],[i_0_36,c_0_29]),
[final] ).
cnf(i_0_57,plain,
( geq(X1,vplus(X2,v1))
| ~ greater(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_58,plain,
( X1 = X2
| vplus(X1,v1) != vplus(X2,v1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_38,c_0_29]),c_0_29]),
[final] ).
cnf(i_0_59,plain,
vmul(X1,X2) = vmul(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_60,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_61,plain,
vplus(v1,X1) = vplus(X1,v1),
inference(rw,[status(thm)],[i_0_41,c_0_29]),
[final] ).
cnf(i_0_62,plain,
vplus(X1,v1) != X1,
inference(rw,[status(thm)],[i_0_42,c_0_29]),
[final] ).
cnf(i_0_63,plain,
( X1 = v1
| X1 = vplus(vskolem2(X1),v1) ),
inference(rw,[status(thm)],[i_0_43,c_0_29]),
[final] ).
cnf(i_0_64,plain,
vmul(v1,X1) = X1,
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_65,plain,
vmul(X1,v1) = X1,
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_66,plain,
geq(X1,v1),
inference(split_conjunct,[status(thm)],[i_0_45]),
[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,[],[58]) ).
cnf(i_0_83,plain,
X1 = vmul(v1,X1),
inference(scs_inference,[],[i_0_64,i_0_68]) ).
cnf(i_0_84,plain,
$false,
inference(scs_inference,[],[i_0_46,i_0_64,i_0_50,i_0_68,i_0_70]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NUM846+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.16/0.33 % Computer : n004.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 01:15:17 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.27/1.61 % Version : CSE_E---1.7
% 0.27/1.61 % Problem : theBenchmark.p
% 0.27/1.61 % SZS status Theorem for theBenchmark.p
% 0.27/1.61 % SZS output start CNFRefutation
% See solution above
% 0.27/1.63 % Total time : 1.273s
%------------------------------------------------------------------------------