%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM016+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 06:59:39 AM UTC 2026
% Result : Theorem 14.81s 2.42s
% Output : CNFRefutation 14.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 3
% Syntax : Number of formulae : 25 ( 6 unt; 0 def)
% Number of atoms : 100 ( 6 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 94 ( 19 ~; 37 |; 38 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 10 ( 0 sgn 0 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__731,axiom,
( aElement0(xc)
& aElement0(xb)
& aElement0(xa) ),
file('theBenchmark.p',m__731) ).
fof(m__731_02,axiom,
( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) )
& sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) ),
file('theBenchmark.p',m__731_02) ).
fof(m__,conjecture,
? [W0] :
( ( sdtmndtasgtdt0(W0,xR,xb)
| sdtmndtplgtdt0(W0,xR,xb)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,xb)
& aReductOfIn0(W1,W0,xR)
& aElement0(W1) )
| aReductOfIn0(xb,W0,xR)
| W0 = xb )
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ? [W0] :
( ( sdtmndtasgtdt0(W0,xR,xb)
| sdtmndtplgtdt0(W0,xR,xb)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,xb)
& aReductOfIn0(W1,W0,xR)
& aElement0(W1) )
| aReductOfIn0(xb,W0,xR)
| W0 = xb )
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_89,negated_conjecture,
( ~ sdtmndtplgtdt0(A,xR,xb)
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_92,negated_conjecture,
( xb != A
| ~ aReductOfIn0(A,xa,xR)
| ~ aElement0(A) ),
inference(clausify,[status(thm)],[m___neg]) ).
fof(nnf_18,plain,
( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) )
& sdtmndtplgtdt0(xa,xR,xb)
& ( ? [X0] :
( sdtmndtplgtdt0(X0,xR,xb)
& aReductOfIn0(X0,xa,xR)
& aElement0(X0) )
| aReductOfIn0(xb,xa,xR) ) ),
inference(fof_nnf,[status(thm)],[m__731_02]) ).
fof(sk_m__731_02_sk,plain,
( sdtmndtplgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(sK1,xR,xc)
& aReductOfIn0(sK1,xa,xR)
& aElement0(sK1) )
| aReductOfIn0(xc,xa,xR) )
& sdtmndtplgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(sK0,xR,xb)
& aReductOfIn0(sK0,xa,xR)
& aElement0(sK0) )
| aReductOfIn0(xb,xa,xR) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(W0,sK1)],[nnf_18]) ).
fof(sk_m__731_02,plain,
( sdtmndtplgtdt0(xa,xR,xc)
& ( sdtmndtplgtdt0(sK1,xR,xc)
| aReductOfIn0(xc,xa,xR) )
& ( aReductOfIn0(sK1,xa,xR)
| aReductOfIn0(xc,xa,xR) )
& ( aElement0(sK1)
| aReductOfIn0(xc,xa,xR) )
& sdtmndtplgtdt0(xa,xR,xb)
& ( sdtmndtplgtdt0(sK0,xR,xb)
| aReductOfIn0(xb,xa,xR) )
& ( aReductOfIn0(sK0,xa,xR)
| aReductOfIn0(xb,xa,xR) )
& ( aElement0(sK0)
| aReductOfIn0(xb,xa,xR) ) ),
inference(cnf_transformation,[status(thm)],[sk_m__731_02_sk]) ).
cnf(c_98,plain,
( sdtmndtplgtdt0(sK0,xR,xb)
| aReductOfIn0(xb,xa,xR) ),
inference(split_conjunct,[status(thm)],[sk_m__731_02]) ).
cnf(c_99,plain,
( aReductOfIn0(sK0,xa,xR)
| aReductOfIn0(xb,xa,xR) ),
inference(split_conjunct,[status(thm)],[sk_m__731_02]) ).
cnf(c_100,plain,
( aElement0(sK0)
| aReductOfIn0(xb,xa,xR) ),
inference(split_conjunct,[status(thm)],[sk_m__731_02]) ).
cnf(c_377,plain,
aElement0(xb),
inference(clausify,[status(thm)],[m__731]) ).
cnf(c_3977,negated_conjecture,
( xb != xb
| ~ aElement0(xb)
| sdtmndtplgtdt0(sK0,xR,xb) ),
inference(resolve,[status(thm)],[c_98,c_92]) ).
cnf(c_3978,negated_conjecture,
( ~ aElement0(xb)
| sdtmndtplgtdt0(sK0,xR,xb) ),
inference(copy,[status(thm)],[c_3977]) ).
cnf(c_1245,negated_conjecture,
sdtmndtplgtdt0(sK0,xR,xb),
inference(resolve,[status(thm)],[c_377,c_3978]) ).
cnf(c_3979,negated_conjecture,
( xb != xb
| ~ aElement0(xb)
| aReductOfIn0(sK0,xa,xR) ),
inference(resolve,[status(thm)],[c_99,c_92]) ).
cnf(c_3980,negated_conjecture,
( ~ aElement0(xb)
| aReductOfIn0(sK0,xa,xR) ),
inference(copy,[status(thm)],[c_3979]) ).
cnf(c_1256,negated_conjecture,
aReductOfIn0(sK0,xa,xR),
inference(resolve,[status(thm)],[c_377,c_3980]) ).
cnf(c_3981,negated_conjecture,
( xb != xb
| ~ aElement0(xb)
| aElement0(sK0) ),
inference(resolve,[status(thm)],[c_100,c_92]) ).
cnf(c_3982,negated_conjecture,
( ~ aElement0(xb)
| aElement0(sK0) ),
inference(copy,[status(thm)],[c_3981]) ).
cnf(c_1261,negated_conjecture,
aElement0(sK0),
inference(resolve,[status(thm)],[c_377,c_3982]) ).
cnf(c_3983,negated_conjecture,
( ~ aReductOfIn0(sK0,xa,xR)
| ~ aElement0(sK0) ),
inference(resolve,[status(thm)],[c_1245,c_89]) ).
cnf(c_3984,negated_conjecture,
~ aReductOfIn0(sK0,xa,xR),
inference(resolve,[status(thm)],[c_1261,c_3983]) ).
cnf(c_3976,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1256,c_3984]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM016+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 23:23:54 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 1705606 was started by sandbox2 on n018,
% 0.09/0.37 % Sat Sep 26 23:23:54 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.25/0.50
% 0.25/0.50 % From the command line: assign(max_seconds, 300).
% 14.81/2.42
% 14.81/2.42 % given #500 (I,wt=47): 1042 -aElement0(A) | -aElement0(B) | -aElement0(C) | -aReductOfIn0(C,A,xR) | -sdtmndtplgtdt0(C,xR,B) | -iLess0(A,xa) | f17(A,A,B) = A | aReductOfIn0(f17(A,A,B),A,xR) | aReductOfIn0(f18(A,A,B),A,xR). [factor(351,a,b),xx(c)].
% 14.81/2.42
% 14.81/2.42 % SZS status Theorem for theBenchmark
% 14.81/2.42
% 14.81/2.42 % Proof 1 at 1.77 (+ 0.12) seconds.
% 14.81/2.42 % Length of proof is 13.
% 14.81/2.42 % Level of proof is 3.
% 14.81/2.42 % Maximum clause weight is 15.000.
% 14.81/2.42 % Given clauses 614.
% 14.81/2.42
% 14.81/2.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------