%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM022+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 : n002.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:31 PM UTC 2026
% Result : Theorem 8.21s 1.73s
% Output : Proof 8.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 2
% Syntax : Number of formulae : 50 ( 11 unt; 0 def)
% Number of atoms : 487 ( 84 equ)
% Maximal formula atoms : 96 ( 9 avg)
% Number of connectives : 531 ( 94 ~; 171 |; 260 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 35 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 17 con; 0-0 aty)
% Number of variables : 64 ( 0 sgn 9 !; 51 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,conjecture,
( ( ( ( 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) ) )
=> ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& ( ( sdtmndtplgtdt0(xc,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xc,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xc,xR) ) )
| xc = W3 )
& sdtmndtasgtdt0(xb,xR,W3)
& ( ( sdtmndtplgtdt0(xb,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xb,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xb,xR) ) )
| xb = W3 )
& aNormalFormOfIn0(W3,W2,xR)
& ~ ? [W4] : aReductOfIn0(W4,W3,xR)
& sdtmndtasgtdt0(W2,xR,W3)
& ( ( sdtmndtplgtdt0(W2,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W2,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W2,xR) ) )
| W2 = W3 )
& aElement0(W3) )
& 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 )
& sdtmndtasgtdt0(W0,xR,W2)
& ( ( sdtmndtplgtdt0(W0,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W0,xR) ) )
| W0 = W2 )
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& ( ( sdtmndtplgtdt0(W1,xR,xc)
& ( ? [W2] :
( sdtmndtplgtdt0(W2,xR,xc)
& aReductOfIn0(W2,W1,xR)
& aElement0(W2) )
| aReductOfIn0(xc,W1,xR) ) )
| W1 = xc )
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& 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) ) )
=> ( ( sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb ) )
=> ? [W0] :
( ( sdtmndtasgtdt0(xc,xR,W0)
| sdtmndtplgtdt0(xc,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xc,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xc,xR)
| xc = W0 )
& ( sdtmndtasgtdt0(xb,xR,W0)
| sdtmndtplgtdt0(xb,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xb,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xb,xR)
| xb = W0 )
& aElement0(W0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f18_neg,negated_conjecture,
~ ( ( ( ( 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) ) )
=> ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& ( ( sdtmndtplgtdt0(xc,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xc,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xc,xR) ) )
| xc = W3 )
& sdtmndtasgtdt0(xb,xR,W3)
& ( ( sdtmndtplgtdt0(xb,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xb,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xb,xR) ) )
| xb = W3 )
& aNormalFormOfIn0(W3,W2,xR)
& ~ ? [W4] : aReductOfIn0(W4,W3,xR)
& sdtmndtasgtdt0(W2,xR,W3)
& ( ( sdtmndtplgtdt0(W2,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W2,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W2,xR) ) )
| W2 = W3 )
& aElement0(W3) )
& 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 )
& sdtmndtasgtdt0(W0,xR,W2)
& ( ( sdtmndtplgtdt0(W0,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W0,xR) ) )
| W0 = W2 )
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& ( ( sdtmndtplgtdt0(W1,xR,xc)
& ( ? [W2] :
( sdtmndtplgtdt0(W2,xR,xc)
& aReductOfIn0(W2,W1,xR)
& aElement0(W2) )
| aReductOfIn0(xc,W1,xR) ) )
| W1 = xc )
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& 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) ) )
=> ( ( sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb ) )
=> ? [W0] :
( ( sdtmndtasgtdt0(xc,xR,W0)
| sdtmndtplgtdt0(xc,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xc,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xc,xR)
| xc = W0 )
& ( sdtmndtasgtdt0(xb,xR,W0)
| sdtmndtplgtdt0(xb,xR,W0)
| ? [W1] :
( sdtmndtplgtdt0(W1,xR,W0)
& aReductOfIn0(W1,xb,xR)
& aElement0(W1) )
| aReductOfIn0(W0,xb,xR)
| xb = W0 )
& aElement0(W0) ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f18_nnf,plain,
( ! [W0] :
( ( ~ sdtmndtasgtdt0(xc,xR,W0)
& ~ sdtmndtplgtdt0(xc,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xc,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xc,xR)
& xc != W0 )
| ( ~ sdtmndtasgtdt0(xb,xR,W0)
& ~ sdtmndtplgtdt0(xb,xR,W0)
& ! [W1] :
( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xb,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xb,xR)
& xb != W0 )
| ~ aElement0(W0) )
& sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xc)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ? [W0] :
( sdtmndtplgtdt0(W0,xR,xb)
& aReductOfIn0(W0,xa,xR)
& aElement0(W0) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb )
& ( ? [W0] :
( ? [W1] :
( ? [W2] :
( ? [W3] :
( sdtmndtasgtdt0(xc,xR,W3)
& ( ( sdtmndtplgtdt0(xc,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xc,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xc,xR) ) )
| xc = W3 )
& sdtmndtasgtdt0(xb,xR,W3)
& ( ( sdtmndtplgtdt0(xb,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,xb,xR)
& aElement0(W4) )
| aReductOfIn0(W3,xb,xR) ) )
| xb = W3 )
& aNormalFormOfIn0(W3,W2,xR)
& ! [W4] : ~ aReductOfIn0(W4,W3,xR)
& sdtmndtasgtdt0(W2,xR,W3)
& ( ( sdtmndtplgtdt0(W2,xR,W3)
& ( ? [W4] :
( sdtmndtplgtdt0(W4,xR,W3)
& aReductOfIn0(W4,W2,xR)
& aElement0(W4) )
| aReductOfIn0(W3,W2,xR) ) )
| W2 = W3 )
& aElement0(W3) )
& 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 )
& sdtmndtasgtdt0(W0,xR,W2)
& ( ( sdtmndtplgtdt0(W0,xR,W2)
& ( ? [W3] :
( sdtmndtplgtdt0(W3,xR,W2)
& aReductOfIn0(W3,W0,xR)
& aElement0(W3) )
| aReductOfIn0(W2,W0,xR) ) )
| W0 = W2 )
& aElement0(W2) )
& sdtmndtasgtdt0(W1,xR,xc)
& ( ( sdtmndtplgtdt0(W1,xR,xc)
& ( ? [W2] :
( sdtmndtplgtdt0(W2,xR,xc)
& aReductOfIn0(W2,W1,xR)
& aElement0(W2) )
| aReductOfIn0(xc,W1,xR) ) )
| W1 = xc )
& aReductOfIn0(W1,xa,xR)
& aElement0(W1) )
& 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) )
| ( ~ 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) ) ) ),
inference(nnf_transformation,[status(thm)],[f18_neg]) ).
fof(f18_sk,plain,
! [W0,W4,W1] :
( ( ( ~ sdtmndtasgtdt0(xc,xR,W0)
& ~ sdtmndtplgtdt0(xc,xR,W0)
& ( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xc,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xc,xR)
& xc != W0 )
| ( ~ sdtmndtasgtdt0(xb,xR,W0)
& ~ sdtmndtplgtdt0(xb,xR,W0)
& ( ~ sdtmndtplgtdt0(W1,xR,W0)
| ~ aReductOfIn0(W1,xb,xR)
| ~ aElement0(W1) )
& ~ aReductOfIn0(W0,xb,xR)
& xb != W0 )
| ~ aElement0(W0) )
& sdtmndtasgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(xa,xR,xc)
& ( ( sdtmndtplgtdt0(sk31,xR,xc)
& aReductOfIn0(sk31,xa,xR)
& aElement0(sk31) )
| aReductOfIn0(xc,xa,xR) ) )
| xa = xc )
& sdtmndtasgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(xa,xR,xb)
& ( ( sdtmndtplgtdt0(sk30,xR,xb)
& aReductOfIn0(sk30,xa,xR)
& aElement0(sk30) )
| aReductOfIn0(xb,xa,xR) ) )
| xa = xb )
& ( ( sdtmndtasgtdt0(xc,xR,sk26)
& ( ( sdtmndtplgtdt0(xc,xR,sk26)
& ( ( sdtmndtplgtdt0(sk29,xR,sk26)
& aReductOfIn0(sk29,xc,xR)
& aElement0(sk29) )
| aReductOfIn0(sk26,xc,xR) ) )
| xc = sk26 )
& sdtmndtasgtdt0(xb,xR,sk26)
& ( ( sdtmndtplgtdt0(xb,xR,sk26)
& ( ( sdtmndtplgtdt0(sk28,xR,sk26)
& aReductOfIn0(sk28,xb,xR)
& aElement0(sk28) )
| aReductOfIn0(sk26,xb,xR) ) )
| xb = sk26 )
& aNormalFormOfIn0(sk26,sk23,xR)
& ~ aReductOfIn0(W4,sk26,xR)
& sdtmndtasgtdt0(sk23,xR,sk26)
& ( ( sdtmndtplgtdt0(sk23,xR,sk26)
& ( ( sdtmndtplgtdt0(sk27,xR,sk26)
& aReductOfIn0(sk27,sk23,xR)
& aElement0(sk27) )
| aReductOfIn0(sk26,sk23,xR) ) )
| sk23 = sk26 )
& aElement0(sk26)
& sdtmndtasgtdt0(sk21,xR,sk23)
& ( ( sdtmndtplgtdt0(sk21,xR,sk23)
& ( ( sdtmndtplgtdt0(sk25,xR,sk23)
& aReductOfIn0(sk25,sk21,xR)
& aElement0(sk25) )
| aReductOfIn0(sk23,sk21,xR) ) )
| sk21 = sk23 )
& sdtmndtasgtdt0(sk19,xR,sk23)
& ( ( sdtmndtplgtdt0(sk19,xR,sk23)
& ( ( sdtmndtplgtdt0(sk24,xR,sk23)
& aReductOfIn0(sk24,sk19,xR)
& aElement0(sk24) )
| aReductOfIn0(sk23,sk19,xR) ) )
| sk19 = sk23 )
& aElement0(sk23)
& sdtmndtasgtdt0(sk21,xR,xc)
& ( ( sdtmndtplgtdt0(sk21,xR,xc)
& ( ( sdtmndtplgtdt0(sk22,xR,xc)
& aReductOfIn0(sk22,sk21,xR)
& aElement0(sk22) )
| aReductOfIn0(xc,sk21,xR) ) )
| sk21 = xc )
& aReductOfIn0(sk21,xa,xR)
& aElement0(sk21)
& sdtmndtasgtdt0(sk19,xR,xb)
& ( ( sdtmndtplgtdt0(sk19,xR,xb)
& ( ( sdtmndtplgtdt0(sk20,xR,xb)
& aReductOfIn0(sk20,sk19,xR)
& aElement0(sk20) )
| aReductOfIn0(xb,sk19,xR) ) )
| sk19 = xb )
& aReductOfIn0(sk19,xa,xR)
& aElement0(sk19) )
| ( ~ sdtmndtplgtdt0(xa,xR,xc)
& ( ~ sdtmndtplgtdt0(W0,xR,xc)
| ~ aReductOfIn0(W0,xa,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xc,xa,xR) )
| ( ~ sdtmndtplgtdt0(xa,xR,xb)
& ( ~ sdtmndtplgtdt0(W0,xR,xb)
| ~ aReductOfIn0(W0,xa,xR)
| ~ aElement0(W0) )
& ~ aReductOfIn0(xb,xa,xR) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk19,sk20,sk21,sk22,sk23,sk24,sk25,sk26,sk27,sk28,sk29,sk30,sk31])],[f18_nnf]) ).
cnf(c724,plain,
( sdtmndtasgtdt0(xc,xR,sk26)
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(c728,plain,
( sdtmndtplgtdt0(xa,xR,xb)
| xa = xb ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p2052,plain,
( xa = xb
| sdtmndtasgtdt0(xc,xR,sk26)
| ~ sdtmndtplgtdt0(xa,xR,xc) ),
inference(resolution,[status(thm)],[c724,c728]) ).
cnf(c733,plain,
( sdtmndtplgtdt0(xa,xR,xc)
| xa = xc ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p2265,plain,
( xa = xc
| xa = xb
| sdtmndtasgtdt0(xc,xR,sk26) ),
inference(resolution,[status(thm)],[p2052,c733]) ).
cnf(c719,plain,
( sdtmndtasgtdt0(xb,xR,sk26)
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p2051,plain,
( xa = xb
| sdtmndtasgtdt0(xb,xR,sk26)
| ~ sdtmndtplgtdt0(xa,xR,xc) ),
inference(resolution,[status(thm)],[c719,c728]) ).
cnf(p2063,plain,
( xa = xc
| xa = xb
| sdtmndtasgtdt0(xb,xR,sk26) ),
inference(resolution,[status(thm)],[p2051,c733]) ).
cnf(c707,plain,
( aElement0(sk26)
| ~ sdtmndtplgtdt0(xa,xR,xc)
| ~ sdtmndtplgtdt0(xa,xR,xb) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p633,plain,
( xa = xb
| aElement0(sk26)
| ~ sdtmndtplgtdt0(xa,xR,xc) ),
inference(resolution,[status(thm)],[c707,c728]) ).
cnf(p634,plain,
( xa = xc
| xa = xb
| aElement0(sk26) ),
inference(resolution,[status(thm)],[p633,c733]) ).
fof(f16,hypothesis,
( aElement0(xc)
& aElement0(xb)
& aElement0(xa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__731) ).
fof(f16_nnf,plain,
( aElement0(xc)
& aElement0(xb)
& aElement0(xa) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( aElement0(xc)
& aElement0(xb)
& aElement0(xa) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c61,plain,
aElement0(xb),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(c738,plain,
( ~ sdtmndtplgtdt0(xc,xR,X0)
| xb != X0
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p570,plain,
( ~ sdtmndtplgtdt0(xc,xR,xb)
| ~ aElement0(xb) ),
inference(equality_resolution,[status(thm)],[c738]) ).
cnf(p693,plain,
~ sdtmndtplgtdt0(xc,xR,xb),
inference(resolution,[status(thm)],[c61,p570]) ).
cnf(p715,plain,
( ~ sdtmndtplgtdt0(xa,xR,xb)
| xa = xb
| aElement0(sk26) ),
inference(superposition,[status(thm)],[p634,p693]) ).
cnf(p1332,plain,
( xa = xb
| xa = xb
| aElement0(sk26) ),
inference(resolution,[status(thm)],[p715,c728]) ).
cnf(p1333,plain,
( xa = xb
| aElement0(sk26) ),
inference(factoring,[status(thm)],[p1332]) ).
cnf(c62,plain,
aElement0(xc),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(c750,plain,
( xc != X0
| ~ sdtmndtplgtdt0(xb,xR,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p575,plain,
( ~ sdtmndtplgtdt0(xb,xR,xc)
| ~ aElement0(xc) ),
inference(equality_resolution,[status(thm)],[c750]) ).
cnf(p729,plain,
~ sdtmndtplgtdt0(xb,xR,xc),
inference(resolution,[status(thm)],[c62,p575]) ).
cnf(p1360,plain,
( ~ sdtmndtplgtdt0(xa,xR,xc)
| aElement0(sk26) ),
inference(superposition,[status(thm)],[p1333,p729]) ).
cnf(p1429,plain,
( xa = xc
| aElement0(sk26) ),
inference(resolution,[status(thm)],[p1360,c733]) ).
cnf(c735,plain,
( xc != X0
| xb != X0
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p567,plain,
( xb != xc
| ~ aElement0(xc) ),
inference(equality_resolution,[status(thm)],[c735]) ).
cnf(p722,plain,
xb != xc,
inference(resolution,[status(thm)],[c62,p567]) ).
cnf(p1358,plain,
( xa != xc
| aElement0(sk26) ),
inference(superposition,[status(thm)],[p1333,p722]) ).
cnf(p1439,plain,
( aElement0(sk26)
| aElement0(sk26) ),
inference(resolution,[status(thm)],[p1429,p1358]) ).
cnf(p1440,plain,
aElement0(sk26),
inference(factoring,[status(thm)],[p1439]) ).
cnf(c759,plain,
( ~ sdtmndtasgtdt0(xc,xR,X0)
| ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ aElement0(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p1470,plain,
( ~ sdtmndtasgtdt0(xc,xR,sk26)
| ~ sdtmndtasgtdt0(xb,xR,sk26) ),
inference(resolution,[status(thm)],[p1440,c759]) ).
cnf(p2077,plain,
( ~ sdtmndtasgtdt0(xc,xR,sk26)
| xa = xc
| xa = xb ),
inference(resolution,[status(thm)],[p2063,p1470]) ).
cnf(p2266,plain,
( xa = xc
| xa = xb
| xa = xc
| xa = xb ),
inference(resolution,[status(thm)],[p2265,p2077]) ).
cnf(p2462,plain,
( xa = xc
| xa = xc
| xa = xb ),
inference(factoring,[status(thm)],[p2266]) ).
cnf(p2464,plain,
( xa = xc
| xa = xb ),
inference(factoring,[status(thm)],[p2462]) ).
cnf(p2467,plain,
( ~ sdtmndtplgtdt0(xa,xR,xb)
| xa = xb ),
inference(superposition,[status(thm)],[p2464,p693]) ).
cnf(p2525,plain,
( xa = xb
| xa = xb ),
inference(resolution,[status(thm)],[p2467,c728]) ).
cnf(p2535,plain,
xa = xb,
inference(factoring,[status(thm)],[p2525]) ).
cnf(p2548,plain,
~ sdtmndtplgtdt0(xa,xR,xc),
inference(superposition,[status(thm)],[p2535,p729]) ).
cnf(p2654,plain,
xa = xc,
inference(resolution,[status(thm)],[p2548,c733]) ).
cnf(p2546,plain,
xa != xc,
inference(superposition,[status(thm)],[p2535,p722]) ).
cnf(p2684,plain,
$false,
inference(resolution,[status(thm)],[p2654,p2546]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM022+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.58 % Computer : n002.cluster.edu
% 0.12/0.58 % Model : x86_64 x86_64
% 0.12/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.58 % Memory : 8046.5625MB
% 0.12/0.58 % OS : Linux 6.8.0-71-generic
% 0.12/0.58 % CPULimit : 300
% 0.12/0.58 % WCLimit : 300
% 0.12/0.58 % DateTime : Fri Sep 25 07:52:20 UTC 2026
% 0.12/0.59 % CPUTime :
% 0.12/0.59 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.21/1.73 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.21/1.73 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------