%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM856+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:18:14 AM UTC 2026
% Result : Theorem 166.43s 38.90s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 13
% Syntax : Number of formulae : 74 ( 29 unt; 0 def)
% Number of atoms : 134 ( 16 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 100 ( 40 ~; 48 |; 5 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 91 ( 0 sgn 25 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof('dis(antec(scope(318)))',axiom,
( ( greater(vd517,vd518)
& geq(vd519,vd520) )
| ( geq(vd517,vd518)
& greater(vd519,vd520) ) ),
file('theBenchmark.p','dis(antec(scope(318)))') ).
fof('ass(cond(conjunct2(conjunct2(307)), 0), 0)',axiom,
! [Vd496,Vd497,Vd498] :
( less(vmul(Vd496,Vd497),vmul(Vd498,Vd497))
=> less(Vd496,Vd498) ),
file('theBenchmark.p','ass(cond(conjunct2(conjunct2(307)), 0), 0)') ).
fof('ass(cond(299, 0), 0)',axiom,
! [Vd456,Vd465,Vd466] :
( less(Vd465,Vd466)
=> less(vmul(Vd465,Vd456),vmul(Vd466,Vd456)) ),
file('theBenchmark.p','ass(cond(299, 0), 0)') ).
fof('ass(cond(270, 0), 0)',axiom,
! [Vd418,Vd419] : vmul(Vd418,Vd419) = vmul(Vd419,Vd418),
file('theBenchmark.p','ass(cond(270, 0), 0)') ).
fof('qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))',axiom,
! [Vd396,Vd397] :
( vmul(Vd396,v1) = Vd396
& vmul(Vd396,vsucc(Vd397)) = vplus(vmul(Vd396,Vd397),Vd396) ),
file('theBenchmark.p','qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))') ).
fof('ass(cond(goal(177), 0), 0)',axiom,
! [Vd281,Vd282,Vd283] :
( ( ( less(Vd281,Vd282)
& leq(Vd282,Vd283) )
| ( leq(Vd281,Vd282)
& less(Vd282,Vd283) ) )
=> less(Vd281,Vd283) ),
file('theBenchmark.p','ass(cond(goal(177), 0), 0)') ).
fof('ass(cond(158, 0), 0)',axiom,
! [Vd254,Vd255] :
( geq(Vd254,Vd255)
=> leq(Vd255,Vd254) ),
file('theBenchmark.p','ass(cond(158, 0), 0)') ).
fof('def(cond(conseq(axiom(3)), 17), 1)',axiom,
! [Vd249,Vd250] :
( leq(Vd250,Vd249)
<=> ( Vd250 = Vd249
| less(Vd250,Vd249) ) ),
file('theBenchmark.p','def(cond(conseq(axiom(3)), 17), 1)') ).
fof('def(cond(conseq(axiom(3)), 16), 1)',axiom,
! [Vd244,Vd245] :
( geq(Vd245,Vd244)
<=> ( Vd245 = Vd244
| greater(Vd245,Vd244) ) ),
file('theBenchmark.p','def(cond(conseq(axiom(3)), 16), 1)') ).
fof('ass(cond(140, 0), 0)',axiom,
! [Vd208,Vd209] :
( greater(Vd208,Vd209)
=> less(Vd209,Vd208) ),
file('theBenchmark.p','ass(cond(140, 0), 0)') ).
fof('ass(cond(goal(130), 0), 0)',axiom,
! [Vd203,Vd204] :
( less(Vd203,Vd204)
| greater(Vd203,Vd204)
| Vd203 = Vd204 ),
file('theBenchmark.p','ass(cond(goal(130), 0), 0)') ).
fof('ass(cond(goal(130), 0), 1)',axiom,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| Vd203 != Vd204 ),
file('theBenchmark.p','ass(cond(goal(130), 0), 1)') ).
fof('holds(conseq(scope(318)), 525, 0)',conjecture,
greater(vmul(vd517,vd519),vmul(vd518,vd520)),
file('theBenchmark.p','holds(conseq(scope(318)), 525, 0)') ).
fof('holds(conseq(scope(318)), 525, 0)_neg',negated_conjecture,
~ greater(vmul(vd517,vd519),vmul(vd518,vd520)),
inference(assume_negation,[status(cth)],['holds(conseq(scope(318)), 525, 0)']) ).
cnf(c_60,plain,
( geq(vd519,vd520)
| greater(vd519,vd520) ),
inference(clausify,[status(thm)],['dis(antec(scope(318)))']) ).
cnf(c_61,plain,
( greater(vd517,vd518)
| greater(vd519,vd520) ),
inference(clausify,[status(thm)],['dis(antec(scope(318)))']) ).
cnf(c_63,plain,
( greater(vd517,vd518)
| geq(vd517,vd518) ),
inference(clausify,[status(thm)],['dis(antec(scope(318)))']) ).
cnf(c_65,plain,
( less(A,C)
| ~ less(vmul(A,B),vmul(C,B)) ),
inference(clausify,[status(thm)],['ass(cond(conjunct2(conjunct2(307)), 0), 0)']) ).
cnf(c_68,plain,
( less(vmul(A,C),vmul(B,C))
| ~ less(A,B) ),
inference(clausify,[status(thm)],['ass(cond(299, 0), 0)']) ).
cnf(c_74,plain,
vmul(A,B) = vmul(B,A),
inference(clausify,[status(thm)],['ass(cond(270, 0), 0)']) ).
cnf(c_80,plain,
vmul(A,v1) = A,
inference(clausify,[status(thm)],['qu(cond(conseq(axiom(3)), 32), and(holds(definiens(249), 399, 0), holds(definiens(249), 398, 0)))']) ).
cnf(c_96,plain,
( less(C,B)
| ~ leq(C,A)
| ~ less(A,B) ),
inference(clausify,[status(thm)],['ass(cond(goal(177), 0), 0)']) ).
cnf(c_97,plain,
( less(C,B)
| ~ less(C,A)
| ~ leq(A,B) ),
inference(clausify,[status(thm)],['ass(cond(goal(177), 0), 0)']) ).
cnf(c_100,plain,
( leq(B,A)
| ~ geq(A,B) ),
inference(clausify,[status(thm)],['ass(cond(158, 0), 0)']) ).
cnf(c_102,plain,
( ~ less(A,B)
| leq(A,B) ),
inference(clausify,[status(thm)],['def(cond(conseq(axiom(3)), 17), 1)']) ).
cnf(c_103,plain,
( B != A
| leq(A,B) ),
inference(clausify,[status(thm)],['def(cond(conseq(axiom(3)), 17), 1)']) ).
cnf(c_105,plain,
( ~ greater(A,B)
| geq(A,B) ),
inference(clausify,[status(thm)],['def(cond(conseq(axiom(3)), 16), 1)']) ).
cnf(c_108,plain,
( less(B,A)
| ~ greater(A,B) ),
inference(clausify,[status(thm)],['ass(cond(140, 0), 0)']) ).
cnf(c_109,plain,
( less(B,A)
| greater(B,A)
| A = B ),
inference(clausify,[status(thm)],['ass(cond(goal(130), 0), 0)']) ).
cnf(c_110,plain,
( ~ less(B,A)
| A != B ),
inference(clausify,[status(thm)],['ass(cond(goal(130), 0), 1)']) ).
cnf(c_137,negated_conjecture,
~ greater(vmul(vd517,vd519),vmul(vd518,vd520)),
inference(clausify,[status(thm)],['holds(conseq(scope(318)), 525, 0)_neg']) ).
cnf(c_223,plain,
leq(vmul(A,B),vmul(B,A)),
inference(resolve,[status(thm)],[c_103,c_74]) ).
cnf(c_13544,plain,
( geq(vd517,vd518)
| geq(vd517,vd518) ),
inference(resolve,[status(thm)],[c_105,c_63]) ).
cnf(c_231,plain,
geq(vd517,vd518),
inference(copy,[status(thm)],[c_13544]) ).
cnf(c_13545,plain,
( geq(vd519,vd520)
| geq(vd519,vd520) ),
inference(resolve,[status(thm)],[c_105,c_60]) ).
cnf(c_233,plain,
geq(vd519,vd520),
inference(copy,[status(thm)],[c_13545]) ).
cnf(c_239,plain,
( greater(vd519,vd520)
| less(vd518,vd517) ),
inference(resolve,[status(thm)],[c_108,c_61]) ).
cnf(c_242,plain,
( leq(A,B)
| less(A,B)
| greater(A,B) ),
inference(resolve,[status(thm)],[c_109,c_103]) ).
cnf(c_271,plain,
( less(vmul(B,C),vmul(A,C))
| greater(B,A)
| A = B ),
inference(resolve,[status(thm)],[c_109,c_68]) ).
cnf(c_13546,plain,
~ less(A,vmul(A,v1)),
inference(resolve,[status(thm)],[c_110,c_80]) ).
cnf(c_273,plain,
~ less(A,A),
inference(paramod,[status(thm)],[c_80,c_13546]) ).
cnf(c_461,plain,
~ greater(vmul(vd519,vd517),vmul(vd518,vd520)),
inference(paramod,[status(thm)],[c_74,c_137]) ).
cnf(c_462,plain,
~ greater(vmul(vd517,vd519),vmul(vd520,vd518)),
inference(paramod,[status(thm)],[c_74,c_137]) ).
cnf(c_502,plain,
leq(vd518,vd517),
inference(resolve,[status(thm)],[c_231,c_100]) ).
cnf(c_508,plain,
leq(vd520,vd519),
inference(resolve,[status(thm)],[c_233,c_100]) ).
cnf(c_13547,plain,
( less(A,vd517)
| ~ less(A,vd518) ),
inference(resolve,[status(thm)],[c_97,c_502]) ).
cnf(c_598,plain,
~ less(vd517,vd518),
inference(resolve,[status(thm)],[c_13547,c_273]) ).
cnf(c_13548,plain,
( less(A,vd519)
| ~ less(A,vd520) ),
inference(resolve,[status(thm)],[c_97,c_508]) ).
cnf(c_607,plain,
~ less(vd519,vd520),
inference(resolve,[status(thm)],[c_13548,c_273]) ).
cnf(c_643,plain,
~ less(vmul(vd517,A),vmul(vd518,A)),
inference(resolve,[status(thm)],[c_65,c_598]) ).
cnf(c_645,plain,
~ greater(vd520,vd519),
inference(resolve,[status(thm)],[c_108,c_607]) ).
cnf(c_647,plain,
~ less(vmul(vd519,A),vmul(vd520,A)),
inference(resolve,[status(thm)],[c_65,c_607]) ).
cnf(c_837,plain,
( less(vd520,vd519)
| less(vd518,vd517) ),
inference(resolve,[status(thm)],[c_239,c_108]) ).
cnf(c_1787,plain,
( less(vmul(vd518,A),vmul(vd517,A))
| less(vd520,vd519) ),
inference(resolve,[status(thm)],[c_837,c_68]) ).
cnf(c_13549,plain,
( leq(A,B)
| leq(A,B)
| greater(A,B) ),
inference(resolve,[status(thm)],[c_242,c_102]) ).
cnf(c_2700,plain,
( leq(A,B)
| greater(A,B) ),
inference(copy,[status(thm)],[c_13549]) ).
cnf(c_2720,plain,
~ greater(vmul(vd519,vd517),vmul(vd520,vd518)),
inference(paramod,[status(thm)],[c_74,c_461]) ).
cnf(c_13550,plain,
( less(A,vmul(C,B))
| ~ less(A,vmul(B,C)) ),
inference(resolve,[status(thm)],[c_97,c_223]) ).
cnf(c_3025,plain,
~ less(vmul(vd517,A),vmul(A,vd518)),
inference(resolve,[status(thm)],[c_13550,c_643]) ).
cnf(c_13551,plain,
( less(vmul(B,A),C)
| ~ less(vmul(A,B),C) ),
inference(resolve,[status(thm)],[c_96,c_223]) ).
cnf(c_3323,plain,
~ less(vmul(A,vd519),vmul(vd520,A)),
inference(resolve,[status(thm)],[c_13551,c_647]) ).
cnf(c_3831,plain,
( less(C,B)
| ~ less(C,A)
| greater(A,B) ),
inference(resolve,[status(thm)],[c_2700,c_97]) ).
cnf(c_13552,plain,
( less(vmul(B,A),C)
| ~ less(vmul(A,B),C) ),
inference(resolve,[status(thm)],[c_96,c_223]) ).
cnf(c_4563,plain,
~ less(vmul(A,vd517),vmul(A,vd518)),
inference(resolve,[status(thm)],[c_13552,c_3025]) ).
cnf(c_13553,plain,
( less(A,vmul(vd520,vd518))
| ~ less(A,vmul(vd519,vd517)) ),
inference(resolve,[status(thm)],[c_3831,c_2720]) ).
cnf(c_12314,plain,
~ less(vmul(vd520,vd517),vmul(vd519,vd517)),
inference(resolve,[status(thm)],[c_13553,c_4563]) ).
cnf(c_13554,plain,
( less(A,vmul(vd520,vd518))
| ~ less(A,vmul(vd517,vd519)) ),
inference(resolve,[status(thm)],[c_3831,c_462]) ).
cnf(c_12338,plain,
~ less(vmul(vd518,vd519),vmul(vd517,vd519)),
inference(resolve,[status(thm)],[c_13554,c_3323]) ).
cnf(c_13555,plain,
( greater(vd520,vd519)
| vd519 = vd520 ),
inference(resolve,[status(thm)],[c_12314,c_271]) ).
cnf(c_13556,plain,
( greater(vd520,vd519)
| vd520 = vd519 ),
inference(copy,[status(thm)],[c_13555]) ).
cnf(c_13188,plain,
vd520 = vd519,
inference(resolve,[status(thm)],[c_645,c_13556]) ).
cnf(c_13557,plain,
( less(vmul(vd518,A),vmul(vd517,A))
| less(vd519,vd519) ),
inference(paramod,[status(thm)],[c_13188,c_1787]) ).
cnf(c_13542,plain,
less(vmul(vd518,A),vmul(vd517,A)),
inference(resolve,[status(thm)],[c_273,c_13557]) ).
cnf(c_13543,plain,
$false,
inference(resolve,[status(thm)],[c_13542,c_12338]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM856+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.08/15.80 % CPULimit : 300
% 0.08/15.80 % WCLimit : 300
% 0.08/15.80 % DateTime : Sat Sep 26 04:14:21 UTC 2026
% 0.08/15.81 % CPUTime :
% 0.08/15.81 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/15.81 % Process 379373 was started by sandbox on n019,
% 0.08/15.81 % Sat Sep 26 04:14:21 2026
% 0.08/15.81 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/15.83
% 0.08/15.83 % From the command line: assign(max_seconds, 300).
% 166.43/38.90
% 166.43/38.90 % given #500 (A,wt=28): 320 A = B | vplus(A,f3(B,A)) = B | less(B,A). [resolve(117,c,114,b)].
% 166.43/38.90
% 166.43/38.90 % SZS status Theorem for theBenchmark
% 166.43/38.90
% 166.43/38.90 % Proof 1 at 5.42 (+ 1.40) seconds.
% 166.43/38.90 % Length of proof is 59.
% 166.43/38.90 % Level of proof is 11.
% 166.43/38.90 % Maximum clause weight is 23.000.
% 166.43/38.90 % Given clauses 683.
% 166.43/38.90
% 166.43/38.90 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------