%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM013+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 3.86s 1.17s
% Output : Proof 3.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 8
% Syntax : Number of formulae : 98 ( 7 unt; 4 def)
% Number of atoms : 408 ( 7 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 501 ( 191 ~; 240 |; 48 &)
% ( 4 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-3 aty)
% Number of variables : 153 ( 6 sgn 68 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,definition,
! [W0,W1] :
( ( aRewritingSystem0(W1)
& aElement0(W0) )
=> ! [W2] :
( aNormalFormOfIn0(W2,W0,W1)
<=> ( ~ ? [W3] : aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mNFRDef) ).
fof(f12_nnf,plain,
! [W0,W1] :
( ! [W2] :
( ( ? [W3] : aReductOfIn0(W3,W2,W1)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W2)
| aNormalFormOfIn0(W2,W0,W1) )
& ( ( ! [W3] : ~ aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) )
| ~ aNormalFormOfIn0(W2,W0,W1) ) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [W0,W1,W2,W3] :
( ( ( aReductOfIn0(sk11(W0,W1,W2),W2,W1)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W2)
| aNormalFormOfIn0(W2,W0,W1) )
& ( ( ~ aReductOfIn0(W3,W2,W1)
& sdtmndtasgtdt0(W0,W1,W2)
& aElement0(W2) )
| ~ aNormalFormOfIn0(W2,W0,W1) ) )
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11])],[f12_nnf]) ).
cnf(c41,plain,
( aReductOfIn0(sk11(X0,X1,X2),X2,X1)
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f14,conjecture,
! [W0] :
( aElement0(W0)
=> ( ! [W1] :
( aElement0(W1)
=> ( iLess0(W1,W0)
=> ? [W2] : aNormalFormOfIn0(W2,W1,xR) ) )
=> ? [W1] : aNormalFormOfIn0(W1,W0,xR) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f14_neg,negated_conjecture,
~ ! [W0] :
( aElement0(W0)
=> ( ! [W1] :
( aElement0(W1)
=> ( iLess0(W1,W0)
=> ? [W2] : aNormalFormOfIn0(W2,W1,xR) ) )
=> ? [W1] : aNormalFormOfIn0(W1,W0,xR) ) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
fof(f14_nnf,plain,
? [W0] :
( ! [W1] : ~ aNormalFormOfIn0(W1,W0,xR)
& ! [W1] :
( ? [W2] : aNormalFormOfIn0(W2,W1,xR)
| ~ iLess0(W1,W0)
| ~ aElement0(W1) )
& aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f14_neg]) ).
fof(f14_sk,plain,
! [W1] :
( ~ aNormalFormOfIn0(W1,sk12,xR)
& ( aNormalFormOfIn0(sk13(W1),W1,xR)
| ~ iLess0(W1,sk12)
| ~ aElement0(W1) )
& aElement0(sk12) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk12,sk13])],[f14_nnf]) ).
cnf(c44,plain,
aElement0(sk12),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p791,plain,
( aReductOfIn0(sk11(sk12,X0,X1),X1,X0)
| ~ sdtmndtasgtdt0(sk12,X0,X1)
| ~ aElement0(X1)
| aNormalFormOfIn0(X1,sk12,X0)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c41,c44]) ).
fof(f13,hypothesis,
( isTerminating0(xR)
& aRewritingSystem0(xR) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__587) ).
fof(f13_nnf,plain,
( isTerminating0(xR)
& aRewritingSystem0(xR) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
( isTerminating0(xR)
& aRewritingSystem0(xR) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c42,plain,
aRewritingSystem0(xR),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p798,plain,
( aReductOfIn0(sk11(sk12,xR,X0),X0,xR)
| ~ sdtmndtasgtdt0(sk12,xR,X0)
| ~ aElement0(X0)
| aNormalFormOfIn0(X0,sk12,xR) ),
inference(resolution,[status(thm)],[p791,c42]) ).
cnf(p799,plain,
( aReductOfIn0(sk11(sk12,xR,sk12),sk12,xR)
| ~ sdtmndtasgtdt0(sk12,xR,sk12)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p798,c44]) ).
fof(f7,definition,
! [W0,W1,W2] :
( ( aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( sdtmndtasgtdt0(W0,W1,W2)
<=> ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTCRDef) ).
fof(f7_nnf,plain,
! [W0,W1,W2] :
( ( ( ( ~ sdtmndtplgtdt0(W0,W1,W2)
& W0 != W2 )
| sdtmndtasgtdt0(W0,W1,W2) )
& ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2
| ~ sdtmndtasgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [W0,W1,W2] :
( ( ( ( ~ sdtmndtplgtdt0(W0,W1,W2)
& W0 != W2 )
| sdtmndtasgtdt0(W0,W1,W2) )
& ( sdtmndtplgtdt0(W0,W1,W2)
| W0 = W2
| ~ sdtmndtasgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c12,plain,
( X0 != X2
| sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p114,plain,
( sk12 != X1
| sdtmndtasgtdt0(sk12,X0,X1)
| ~ aElement0(X1)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c12,c44]) ).
cnf(p121,plain,
( sdtmndtasgtdt0(sk12,X0,sk12)
| ~ aElement0(sk12)
| ~ aRewritingSystem0(X0) ),
inference(equality_resolution,[status(thm)],[p114]) ).
cnf(p123,plain,
( sdtmndtasgtdt0(sk12,xR,sk12)
| ~ aElement0(sk12) ),
inference(resolution,[status(thm)],[p121,c42]) ).
cnf(p124,plain,
sdtmndtasgtdt0(sk12,xR,sk12),
inference(resolution,[status(thm)],[p123,c44]) ).
cnf(p806,plain,
( aReductOfIn0(sk11(sk12,xR,sk12),sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p799,p124]) ).
fof(f2,axiom,
! [W0,W1] :
( ( aRewritingSystem0(W1)
& aElement0(W0) )
=> ! [W2] :
( aReductOfIn0(W2,W0,W1)
=> aElement0(W2) ) ),
file('/export/starexec/sandbox/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(p65,plain,
( aElement0(X1)
| ~ aReductOfIn0(X1,sk12,X0)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c2,c44]) ).
cnf(p72,plain,
( aElement0(X0)
| ~ aReductOfIn0(X0,sk12,xR) ),
inference(resolution,[status(thm)],[p65,c42]) ).
cnf(p807,plain,
( aElement0(sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p806,p72]) ).
fof(f8,axiom,
! [W0,W1,W2,W3] :
( ( aElement0(W3)
& aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( ( sdtmndtasgtdt0(W2,W1,W3)
& sdtmndtasgtdt0(W0,W1,W2) )
=> sdtmndtasgtdt0(W0,W1,W3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTCRTrans) ).
fof(f8_nnf,plain,
! [W0,W1,W2,W3] :
( sdtmndtasgtdt0(W0,W1,W3)
| ~ sdtmndtasgtdt0(W2,W1,W3)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W3)
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [W0,W1,W2,W3] :
( sdtmndtasgtdt0(W0,W1,W3)
| ~ sdtmndtasgtdt0(W2,W1,W3)
| ~ sdtmndtasgtdt0(W0,W1,W2)
| ~ aElement0(W3)
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c14,plain,
( sdtmndtasgtdt0(X0,X1,X3)
| ~ sdtmndtasgtdt0(X2,X1,X3)
| ~ sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X3)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p738,plain,
( sdtmndtasgtdt0(sk12,X0,X2)
| ~ sdtmndtasgtdt0(X1,X0,X2)
| ~ sdtmndtasgtdt0(sk12,X0,X1)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c14,c44]) ).
cnf(p745,plain,
( sdtmndtasgtdt0(sk12,xR,X1)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ sdtmndtasgtdt0(sk12,xR,X0)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[p738,c42]) ).
cnf(p885,plain,
( sdtmndtasgtdt0(sk12,xR,X0)
| ~ sdtmndtasgtdt0(sk11(sk12,xR,sk12),xR,X0)
| ~ sdtmndtasgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| ~ aElement0(X0)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p807,p745]) ).
cnf(c45,plain,
( aNormalFormOfIn0(sk13(X1),X1,xR)
| ~ iLess0(X1,sk12)
| ~ aElement0(X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p808,plain,
( aNormalFormOfIn0(sk13(sk11(sk12,xR,sk12)),sk11(sk12,xR,sk12),xR)
| ~ iLess0(sk11(sk12,xR,sk12),sk12)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p807,c45]) ).
fof(f5,definition,
! [W0,W1,W2] :
( ( aElement0(W2)
& aRewritingSystem0(W1)
& aElement0(W0) )
=> ( sdtmndtplgtdt0(W0,W1,W2)
<=> ( ? [W3] :
( sdtmndtplgtdt0(W3,W1,W2)
& aReductOfIn0(W3,W0,W1)
& aElement0(W3) )
| aReductOfIn0(W2,W0,W1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTCDef) ).
fof(f5_nnf,plain,
! [W0,W1,W2] :
( ( ( ( ! [W3] :
( ~ sdtmndtplgtdt0(W3,W1,W2)
| ~ aReductOfIn0(W3,W0,W1)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W2,W0,W1) )
| sdtmndtplgtdt0(W0,W1,W2) )
& ( ? [W3] :
( sdtmndtplgtdt0(W3,W1,W2)
& aReductOfIn0(W3,W0,W1)
& aElement0(W3) )
| aReductOfIn0(W2,W0,W1)
| ~ sdtmndtplgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [W0,W1,W2,W3] :
( ( ( ( ( ~ sdtmndtplgtdt0(W3,W1,W2)
| ~ aReductOfIn0(W3,W0,W1)
| ~ aElement0(W3) )
& ~ aReductOfIn0(W2,W0,W1) )
| sdtmndtplgtdt0(W0,W1,W2) )
& ( ( sdtmndtplgtdt0(sk0(W0,W1,W2),W1,W2)
& aReductOfIn0(sk0(W0,W1,W2),W0,W1)
& aElement0(sk0(W0,W1,W2)) )
| aReductOfIn0(W2,W0,W1)
| ~ sdtmndtplgtdt0(W0,W1,W2) ) )
| ~ aElement0(W2)
| ~ aRewritingSystem0(W1)
| ~ aElement0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f5_nnf]) ).
cnf(c8,plain,
( ~ aReductOfIn0(X2,X0,X1)
| sdtmndtplgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p152,plain,
( ~ aReductOfIn0(X1,sk12,X0)
| sdtmndtplgtdt0(sk12,X0,X1)
| ~ aElement0(X1)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c8,c44]) ).
cnf(p159,plain,
( ~ aReductOfIn0(X0,sk12,xR)
| sdtmndtplgtdt0(sk12,xR,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[p152,c42]) ).
cnf(p817,plain,
( ~ aReductOfIn0(sk11(sk12,xR,sk12),sk12,xR)
| sdtmndtplgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p807,p159]) ).
cnf(p898,plain,
( aNormalFormOfIn0(sk12,sk12,xR)
| sdtmndtplgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p817,p806]) ).
cnf(p899,plain,
( sdtmndtplgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p898]) ).
fof(f11,definition,
! [W0] :
( aRewritingSystem0(W0)
=> ( isTerminating0(W0)
<=> ! [W1,W2] :
( ( aElement0(W2)
& aElement0(W1) )
=> ( sdtmndtplgtdt0(W1,W0,W2)
=> iLess0(W2,W1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mTermin) ).
fof(f11_nnf,plain,
! [W0] :
( ( ( ? [W1,W2] :
( ~ iLess0(W2,W1)
& sdtmndtplgtdt0(W1,W0,W2)
& aElement0(W2)
& aElement0(W1) )
| isTerminating0(W0) )
& ( ! [W1,W2] :
( iLess0(W2,W1)
| ~ sdtmndtplgtdt0(W1,W0,W2)
| ~ aElement0(W2)
| ~ aElement0(W1) )
| ~ isTerminating0(W0) ) )
| ~ aRewritingSystem0(W0) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [W0,W1,W2] :
( ( ( ( ~ iLess0(sk10(W0),sk9(W0))
& sdtmndtplgtdt0(sk9(W0),W0,sk10(W0))
& aElement0(sk10(W0))
& aElement0(sk9(W0)) )
| isTerminating0(W0) )
& ( iLess0(W2,W1)
| ~ sdtmndtplgtdt0(W1,W0,W2)
| ~ aElement0(W2)
| ~ aElement0(W1)
| ~ isTerminating0(W0) ) )
| ~ aRewritingSystem0(W0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9,sk10])],[f11_nnf]) ).
cnf(c33,plain,
( iLess0(X2,X1)
| ~ sdtmndtplgtdt0(X1,X0,X2)
| ~ aElement0(X2)
| ~ aElement0(X1)
| ~ isTerminating0(X0)
| ~ aRewritingSystem0(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p271,plain,
( iLess0(X1,X0)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| ~ aElement0(X1)
| ~ aElement0(X0)
| ~ isTerminating0(xR) ),
inference(resolution,[status(thm)],[c33,c42]) ).
cnf(c43,plain,
isTerminating0(xR),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p281,plain,
( iLess0(X1,X0)
| ~ sdtmndtplgtdt0(X0,xR,X1)
| ~ aElement0(X1)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[p271,c43]) ).
cnf(p282,plain,
( iLess0(X0,sk12)
| ~ sdtmndtplgtdt0(sk12,xR,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[p281,c44]) ).
cnf(p831,plain,
( iLess0(sk11(sk12,xR,sk12),sk12)
| ~ sdtmndtplgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p807,p282]) ).
cnf(p900,plain,
( iLess0(sk11(sk12,xR,sk12),sk12)
| aNormalFormOfIn0(sk12,sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p899,p831]) ).
cnf(p901,plain,
( iLess0(sk11(sk12,xR,sk12),sk12)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p900]) ).
cnf(p911,plain,
( aNormalFormOfIn0(sk12,sk12,xR)
| aNormalFormOfIn0(sk13(sk11(sk12,xR,sk12)),sk11(sk12,xR,sk12),xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p808,p901]) ).
cnf(p912,plain,
( aNormalFormOfIn0(sk13(sk11(sk12,xR,sk12)),sk11(sk12,xR,sk12),xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p911]) ).
cnf(c38,plain,
( aElement0(X2)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p810,plain,
( aElement0(X1)
| ~ aNormalFormOfIn0(X1,sk11(sk12,xR,sk12),X0)
| ~ aRewritingSystem0(X0)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p807,c38]) ).
cnf(p895,plain,
( aElement0(X0)
| ~ aNormalFormOfIn0(X0,sk11(sk12,xR,sk12),xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p810,c42]) ).
cnf(p913,plain,
( aElement0(sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk12,sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p912,p895]) ).
cnf(p915,plain,
( aElement0(sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p913]) ).
cnf(p1072,plain,
( aNormalFormOfIn0(sk12,sk12,xR)
| sdtmndtasgtdt0(sk12,xR,sk13(sk11(sk12,xR,sk12)))
| ~ sdtmndtasgtdt0(sk11(sk12,xR,sk12),xR,sk13(sk11(sk12,xR,sk12)))
| ~ sdtmndtasgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p885,p915]) ).
cnf(p1724,plain,
( sdtmndtasgtdt0(sk12,xR,sk13(sk11(sk12,xR,sk12)))
| ~ sdtmndtasgtdt0(sk11(sk12,xR,sk12),xR,sk13(sk11(sk12,xR,sk12)))
| ~ sdtmndtasgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p1072]) ).
cnf(c13,plain,
( ~ sdtmndtplgtdt0(X0,X1,X2)
| sdtmndtasgtdt0(X0,X1,X2)
| ~ aElement0(X2)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p174,plain,
( ~ sdtmndtplgtdt0(sk12,X0,X1)
| sdtmndtasgtdt0(sk12,X0,X1)
| ~ aElement0(X1)
| ~ aRewritingSystem0(X0) ),
inference(resolution,[status(thm)],[c13,c44]) ).
cnf(p181,plain,
( ~ sdtmndtplgtdt0(sk12,xR,X0)
| sdtmndtasgtdt0(sk12,xR,X0)
| ~ aElement0(X0) ),
inference(resolution,[status(thm)],[p174,c42]) ).
cnf(p820,plain,
( ~ sdtmndtplgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| sdtmndtasgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p807,p181]) ).
cnf(p902,plain,
( aNormalFormOfIn0(sk12,sk12,xR)
| sdtmndtasgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p820,p899]) ).
cnf(p903,plain,
( sdtmndtasgtdt0(sk12,xR,sk11(sk12,xR,sk12))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p902]) ).
cnf(p1725,plain,
( aNormalFormOfIn0(sk12,sk12,xR)
| sdtmndtasgtdt0(sk12,xR,sk13(sk11(sk12,xR,sk12)))
| ~ sdtmndtasgtdt0(sk11(sk12,xR,sk12),xR,sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p1724,p903]) ).
cnf(p1726,plain,
( sdtmndtasgtdt0(sk12,xR,sk13(sk11(sk12,xR,sk12)))
| ~ sdtmndtasgtdt0(sk11(sk12,xR,sk12),xR,sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p1725]) ).
cnf(c39,plain,
( sdtmndtasgtdt0(X0,X1,X2)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p811,plain,
( sdtmndtasgtdt0(sk11(sk12,xR,sk12),X0,X1)
| ~ aNormalFormOfIn0(X1,sk11(sk12,xR,sk12),X0)
| ~ aRewritingSystem0(X0)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p807,c39]) ).
cnf(p1010,plain,
( sdtmndtasgtdt0(sk11(sk12,xR,sk12),xR,X0)
| ~ aNormalFormOfIn0(X0,sk11(sk12,xR,sk12),xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p811,c42]) ).
cnf(p1011,plain,
( aNormalFormOfIn0(sk12,sk12,xR)
| sdtmndtasgtdt0(sk11(sk12,xR,sk12),xR,sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p1010,p912]) ).
cnf(p1012,plain,
( sdtmndtasgtdt0(sk11(sk12,xR,sk12),xR,sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p1011]) ).
cnf(p1727,plain,
( aNormalFormOfIn0(sk12,sk12,xR)
| sdtmndtasgtdt0(sk12,xR,sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p1726,p1012]) ).
cnf(p1728,plain,
( sdtmndtasgtdt0(sk12,xR,sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p1727]) ).
cnf(p1004,plain,
( aReductOfIn0(sk11(sk12,xR,sk13(sk11(sk12,xR,sk12))),sk13(sk11(sk12,xR,sk12)),xR)
| ~ sdtmndtasgtdt0(sk12,xR,sk13(sk11(sk12,xR,sk12)))
| aNormalFormOfIn0(sk13(sk11(sk12,xR,sk12)),sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p915,p798]) ).
cnf(p1736,plain,
( aReductOfIn0(sk11(sk12,xR,sk13(sk11(sk12,xR,sk12))),sk13(sk11(sk12,xR,sk12)),xR)
| aNormalFormOfIn0(sk13(sk11(sk12,xR,sk12)),sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p1728,p1004]) ).
cnf(p1908,plain,
( aReductOfIn0(sk11(sk12,xR,sk13(sk11(sk12,xR,sk12))),sk13(sk11(sk12,xR,sk12)),xR)
| aNormalFormOfIn0(sk13(sk11(sk12,xR,sk12)),sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p1736]) ).
cnf(c40,plain,
( ~ aReductOfIn0(X3,X2,X1)
| ~ aNormalFormOfIn0(X2,X0,X1)
| ~ aRewritingSystem0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p812,plain,
( ~ aReductOfIn0(X2,X1,X0)
| ~ aNormalFormOfIn0(X1,sk11(sk12,xR,sk12),X0)
| ~ aRewritingSystem0(X0)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p807,c40]) ).
cnf(p897,plain,
( ~ aReductOfIn0(X1,X0,xR)
| ~ aNormalFormOfIn0(X0,sk11(sk12,xR,sk12),xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p812,c42]) ).
cnf(p914,plain,
( ~ aReductOfIn0(X0,sk13(sk11(sk12,xR,sk12)),xR)
| aNormalFormOfIn0(sk12,sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p912,p897]) ).
cnf(p1006,plain,
( ~ aReductOfIn0(X0,sk13(sk11(sk12,xR,sk12)),xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p914]) ).
cnf(p1909,plain,
( aNormalFormOfIn0(sk12,sk12,xR)
| aNormalFormOfIn0(sk13(sk11(sk12,xR,sk12)),sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(resolution,[status(thm)],[p1908,p1006]) ).
cnf(p1910,plain,
( aNormalFormOfIn0(sk13(sk11(sk12,xR,sk12)),sk12,xR)
| aNormalFormOfIn0(sk12,sk12,xR) ),
inference(factoring,[status(thm)],[p1909]) ).
cnf(c46,plain,
~ aNormalFormOfIn0(X1,sk12,xR),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p1911,plain,
aNormalFormOfIn0(sk12,sk12,xR),
inference(resolution,[status(thm)],[p1910,c46]) ).
cnf(p1912,plain,
$false,
inference(resolution,[status(thm)],[p1911,c46]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM013+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 07:46:16 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.86/1.17 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.86/1.17 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------