%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM013+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 01:03:29 PM UTC 2026
% Result : Theorem 4.80s 6.13s
% Output : Proof 4.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 3
% Syntax : Number of formulae : 43 ( 11 unt; 0 def)
% Number of atoms : 208 ( 14 equ)
% Maximal formula atoms : 23 ( 4 avg)
% Number of connectives : 255 ( 90 ~; 89 |; 64 &)
% ( 0 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 66 ( 4 sgn 28 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f13,hypothesis,
( isTerminating0(xR)
& ! [W0,W1] :
( ( aElement0(W1)
& aElement0(W0) )
=> ( ( sdtmndtplgtdt0(W0,xR,W1)
| ? [W2] :
( sdtmndtplgtdt0(W2,xR,W1)
& aReductOfIn0(W2,W0,xR)
& aElement0(W2) )
| aReductOfIn0(W1,W0,xR) )
=> iLess0(W1,W0) ) )
& aRewritingSystem0(xR) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__587) ).
fof(f13_nnf,plain,
( isTerminating0(xR)
& ! [W0,W1] :
( iLess0(W1,W0)
| ( ~ sdtmndtplgtdt0(W0,xR,W1)
& ! [W2] :
( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,W0,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,W0,xR) )
| ~ aElement0(W1)
| ~ aElement0(W0) )
& aRewritingSystem0(xR) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [W0,W1,W2] :
( isTerminating0(xR)
& ( iLess0(W1,W0)
| ( ~ sdtmndtplgtdt0(W0,xR,W1)
& ( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,W0,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,W0,xR) )
| ~ aElement0(W1)
| ~ aElement0(W0) )
& aRewritingSystem0(xR) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c43,plain,
( iLess0(X1,X0)
| ~ aReductOfIn0(X1,X0,xR)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
fof(f14,conjecture,
! [W0] :
( aElement0(W0)
=> ( ! [W1] :
( aElement0(W1)
=> ( iLess0(W1,W0)
=> ? [W2] :
( aNormalFormOfIn0(W2,W1,xR)
& ~ ? [W3] : aReductOfIn0(W3,W2,xR)
& sdtmndtasgtdt0(W1,xR,W2)
& ( ( sdtmndtplgtdt0(W1,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W1,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W1,xR) ) )
| W1 = W2 )
& aElement0(W2) ) ) )
=> ? [W1] :
( aNormalFormOfIn0(W1,W0,xR)
| ( ~ ? [W2] : aReductOfIn0(W2,W1,xR)
& ( sdtmndtasgtdt0(W0,xR,W1)
| sdtmndtplgtdt0(W0,xR,W1)
| ? [W2] :
( sdtmndtplgtdt0(W2,xR,W1)
& aReductOfIn0(W2,W0,xR)
& aElement0(W2) )
| aReductOfIn0(W1,W0,xR)
| W0 = W1 )
& aElement0(W1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f14_neg,negated_conjecture,
~ ! [W0] :
( aElement0(W0)
=> ( ! [W1] :
( aElement0(W1)
=> ( iLess0(W1,W0)
=> ? [W2] :
( aNormalFormOfIn0(W2,W1,xR)
& ~ ? [W3] : aReductOfIn0(W3,W2,xR)
& sdtmndtasgtdt0(W1,xR,W2)
& ( ( sdtmndtplgtdt0(W1,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W1,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W1,xR) ) )
| W1 = W2 )
& aElement0(W2) ) ) )
=> ? [W1] :
( aNormalFormOfIn0(W1,W0,xR)
| ( ~ ? [W2] : aReductOfIn0(W2,W1,xR)
& ( sdtmndtasgtdt0(W0,xR,W1)
| sdtmndtplgtdt0(W0,xR,W1)
| ? [W2] :
( sdtmndtplgtdt0(W2,xR,W1)
& aReductOfIn0(W2,W0,xR)
& aElement0(W2) )
| aReductOfIn0(W1,W0,xR)
| W0 = W1 )
& aElement0(W1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f14_nnf,plain,
? [W0] :
( ! [W1] :
( ~ aNormalFormOfIn0(W1,W0,xR)
& ( ? [W2] : aReductOfIn0(W2,W1,xR)
| ( ~ sdtmndtasgtdt0(W0,xR,W1)
& ~ sdtmndtplgtdt0(W0,xR,W1)
& ! [W2] :
( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,W0,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,W0,xR)
& W0 != W1 )
| ~ aElement0(W1) ) )
& ! [W1] :
( ? [W2] :
( aNormalFormOfIn0(W2,W1,xR)
& ! [W3] : ~ aReductOfIn0(W3,W2,xR)
& sdtmndtasgtdt0(W1,xR,W2)
& ( ( sdtmndtplgtdt0(W1,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W1,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W1,xR) ) )
| W1 = W2 )
& aElement0(W2) )
| ~ iLess0(W1,W0)
| ~ aElement0(W1) )
& aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f14_neg]) ).
fof(f14_sk,plain,
! [W1,W3,W2] :
( ~ aNormalFormOfIn0(W1,sk12,xR)
& ( aReductOfIn0(sk15(W1),W1,xR)
| ( ~ sdtmndtasgtdt0(sk12,xR,W1)
& ~ sdtmndtplgtdt0(sk12,xR,W1)
& ( ~ sdtmndtplgtdt0(W2,xR,W1)
| ~ aReductOfIn0(W2,sk12,xR)
| ~ aElement0(W2) )
& ~ aReductOfIn0(W1,sk12,xR)
& sk12 != W1 )
| ~ aElement0(W1) )
& ( ( aNormalFormOfIn0(sk13(W1),W1,xR)
& ~ aReductOfIn0(W3,sk13(W1),xR)
& sdtmndtasgtdt0(W1,xR,sk13(W1))
& ( ( sdtmndtplgtdt0(W1,xR,sk13(W1))
& ( ( sdtmndtplgtdt0(sk14(W1),xR,sk13(W1))
& aReductOfIn0(sk14(W1),W1,xR)
& aElement0(sk14(W1)) )
| aReductOfIn0(sk13(W1),W1,xR) ) )
| W1 = sk13(W1) )
& aElement0(sk13(W1)) )
| ~ iLess0(W1,sk12)
| ~ aElement0(W1) )
& aElement0(sk12) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk12,sk13,sk14,sk15])],[f14_nnf]) ).
cnf(c47,plain,
aElement0(sk12),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p287,plain,
( iLess0(X0,sk12)
| ~ aReductOfIn0(X0,sk12,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[c43,c47]) ).
fof(f2,axiom,
! [W0,W1] :
( ( aRewritingSystem0(W1)
& aElement0(W0) )
=> ! [W2] :
( aReductOfIn0(W2,W0,W1)
=> aElement0(W2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mReduct) ).
fof(f2_nnf,plain,
! [W0,W1] :
( ! [W2] :
( aElement0(W2)
| ~ aReductOfIn0(W2,W0,W1) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [W0,W1,W2] :
( aElement0(W2)
| ~ aReductOfIn0(W2,W0,W1)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( aElement0(X2)
| ~ aReductOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p208,plain,
( aElement0(X1)
| ~ aReductOfIn0(X1,sk12,X0)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c2,c47]) ).
cnf(c42,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p215,plain,
( aElement0(X0)
| ~ aReductOfIn0(X0,sk12,xR) ),
inference(resolution,[status(thm)],[p208,c42]) ).
cnf(c56,plain,
( aReductOfIn0(sk15(X1),X1,xR)
| sk12 != X1
| ~ aElement0(X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p69,plain,
( aReductOfIn0(sk15(sk12),sk12,xR)
| ~ aElement0(sk12) ),
inference(equality_resolution,[status(thm)],[c56]) ).
cnf(p71,plain,
aReductOfIn0(sk15(sk12),sk12,xR),
inference(resolution,[status(thm)],[p69,c47]) ).
cnf(p216,plain,
aElement0(sk15(sk12)),
inference(resolution,[status(thm)],[p215,p71]) ).
cnf(p303,plain,
( iLess0(sk15(sk12),sk12)
| ~ aReductOfIn0(sk15(sk12),sk12,xR) ),
inference(resolution,[status(thm)],[p287,p216]) ).
cnf(p305,plain,
iLess0(sk15(sk12),sk12),
inference(resolution,[status(thm)],[p303,p71]) ).
cnf(c48,plain,
( aElement0(sk13(X1))
| ~ iLess0(X1,sk12)
| ~ aElement0(X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p229,plain,
( aElement0(sk13(sk15(sk12)))
| ~ iLess0(sk15(sk12),sk12) ),
inference(resolution,[status(thm)],[p216,c48]) ).
cnf(p306,plain,
aElement0(sk13(sk15(sk12))),
inference(resolution,[status(thm)],[p305,p229]) ).
cnf(c58,plain,
( aReductOfIn0(sk15(X1),X1,xR)
| ~ sdtmndtplgtdt0(X2,xR,X1)
| ~ aReductOfIn0(X2,sk12,xR)
| ~ aElement0(X2)
| ~ aElement0(X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p318,plain,
( aReductOfIn0(sk15(sk13(sk15(sk12))),sk13(sk15(sk12)),xR)
| ~ sdtmndtplgtdt0(X0,xR,sk13(sk15(sk12)))
| ~ aReductOfIn0(X0,sk12,xR)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[p306,c58]) ).
cnf(p366,plain,
( aReductOfIn0(sk15(sk13(sk15(sk12))),sk13(sk15(sk12)),xR)
| ~ sdtmndtplgtdt0(sk15(sk12),xR,sk13(sk15(sk12)))
| ~ aReductOfIn0(sk15(sk12),sk12,xR) ),
inference(resolution,[status(thm)],[p318,p216]) ).
cnf(p368,plain,
( aReductOfIn0(sk15(sk13(sk15(sk12))),sk13(sk15(sk12)),xR)
| ~ sdtmndtplgtdt0(sk15(sk12),xR,sk13(sk15(sk12))) ),
inference(resolution,[status(thm)],[p366,p71]) ).
cnf(c52,plain,
( sdtmndtplgtdt0(X1,xR,sk13(X1))
| X1 = sk13(X1)
| ~ iLess0(X1,sk12)
| ~ aElement0(X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p226,plain,
( sdtmndtplgtdt0(sk15(sk12),xR,sk13(sk15(sk12)))
| sk15(sk12) = sk13(sk15(sk12))
| ~ iLess0(sk15(sk12),sk12) ),
inference(resolution,[status(thm)],[p216,c52]) ).
cnf(p310,plain,
( sdtmndtplgtdt0(sk15(sk12),xR,sk13(sk15(sk12)))
| sk15(sk12) = sk13(sk15(sk12)) ),
inference(resolution,[status(thm)],[p305,p226]) ).
cnf(p369,plain,
( sk15(sk12) = sk13(sk15(sk12))
| aReductOfIn0(sk15(sk13(sk15(sk12))),sk13(sk15(sk12)),xR) ),
inference(resolution,[status(thm)],[p368,p310]) ).
cnf(c54,plain,
( ~ aReductOfIn0(X3,sk13(X1),xR)
| ~ iLess0(X1,sk12)
| ~ aElement0(X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p218,plain,
( ~ aReductOfIn0(X0,sk13(sk15(sk12)),xR)
| ~ iLess0(sk15(sk12),sk12) ),
inference(resolution,[status(thm)],[p216,c54]) ).
cnf(p307,plain,
~ aReductOfIn0(X0,sk13(sk15(sk12)),xR),
inference(resolution,[status(thm)],[p305,p218]) ).
cnf(p370,plain,
sk15(sk12) = sk13(sk15(sk12)),
inference(resolution,[status(thm)],[p369,p307]) ).
cnf(p371,plain,
~ aReductOfIn0(X0,sk15(sk12),xR),
inference(superposition,[status(thm)],[p370,p307]) ).
cnf(c57,plain,
( aReductOfIn0(sk15(X1),X1,xR)
| ~ aReductOfIn0(X1,sk12,xR)
| ~ aElement0(X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p223,plain,
( aReductOfIn0(sk15(sk15(sk12)),sk15(sk12),xR)
| ~ aReductOfIn0(sk15(sk12),sk12,xR) ),
inference(resolution,[status(thm)],[p216,c57]) ).
cnf(p238,plain,
aReductOfIn0(sk15(sk15(sk12)),sk15(sk12),xR),
inference(resolution,[status(thm)],[p223,p71]) ).
cnf(p385,plain,
$false,
inference(resolution,[status(thm)],[p371,p238]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM013+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/5.36 % Computer : n018.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Fri Sep 25 07:48:26 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.80/6.13 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.80/6.13 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------