%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS098+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:53:03 PM UTC 2026
% Result : Unsatisfiable 3.97s 1.12s
% Output : Proof 3.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 7
% Syntax : Number of formulae : 54 ( 19 unt; 0 def)
% Number of atoms : 199 ( 28 equ)
% Maximal formula atoms : 44 ( 3 avg)
% Number of connectives : 229 ( 84 ~; 77 |; 60 &)
% ( 1 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-2 aty)
% Number of variables : 105 ( 0 sgn 56 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f27,axiom,
! [X] :
( cUnsatisfiable(X)
<=> ( ? [Y] :
( ? [Z] :
( cc(Z)
& rt1(Y,Z) )
& ! [Z0,Z1] :
( ( rtt(Y,Z1)
& rtt(Y,Z0) )
=> Z0 = Z1 )
& rr1(X,Y) )
& ~ ? [Y0,Y1] :
( Y0 != Y1
& rr(X,Y1)
& rr(X,Y0) )
& ? [Y] :
( ? [Z] :
( cd(Z)
& rt2(Y,Z) )
& ! [Z0,Z1] :
( ( rtt(Y,Z1)
& rtt(Y,Z0) )
=> Z0 = Z1 )
& rr2(X,Y) )
& ? [Y] :
( ! [Z0,Z1] :
( ( rtt(Y,Z1)
& rtt(Y,Z0) )
=> Z0 = Z1 )
& ? [Z] :
( ce(Z)
& rt3(Y,Z) )
& rr3(X,Y) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(f27_nnf,plain,
! [X] :
( ( ! [Y] :
( ! [Z] :
( ~ cc(Z)
| ~ rt1(Y,Z) )
| ? [Z0,Z1] :
( Z0 != Z1
& rtt(Y,Z1)
& rtt(Y,Z0) )
| ~ rr1(X,Y) )
| ? [Y0,Y1] :
( Y0 != Y1
& rr(X,Y1)
& rr(X,Y0) )
| ! [Y] :
( ! [Z] :
( ~ cd(Z)
| ~ rt2(Y,Z) )
| ? [Z0,Z1] :
( Z0 != Z1
& rtt(Y,Z1)
& rtt(Y,Z0) )
| ~ rr2(X,Y) )
| ! [Y] :
( ? [Z0,Z1] :
( Z0 != Z1
& rtt(Y,Z1)
& rtt(Y,Z0) )
| ! [Z] :
( ~ ce(Z)
| ~ rt3(Y,Z) )
| ~ rr3(X,Y) )
| cUnsatisfiable(X) )
& ( ( ? [Y] :
( ? [Z] :
( cc(Z)
& rt1(Y,Z) )
& ! [Z0,Z1] :
( Z0 = Z1
| ~ rtt(Y,Z1)
| ~ rtt(Y,Z0) )
& rr1(X,Y) )
& ! [Y0,Y1] :
( Y0 = Y1
| ~ rr(X,Y1)
| ~ rr(X,Y0) )
& ? [Y] :
( ? [Z] :
( cd(Z)
& rt2(Y,Z) )
& ! [Z0,Z1] :
( Z0 = Z1
| ~ rtt(Y,Z1)
| ~ rtt(Y,Z0) )
& rr2(X,Y) )
& ? [Y] :
( ! [Z0,Z1] :
( Z0 = Z1
| ~ rtt(Y,Z1)
| ~ rtt(Y,Z0) )
& ? [Z] :
( ce(Z)
& rt3(Y,Z) )
& rr3(X,Y) ) )
| ~ cUnsatisfiable(X) ) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [X,Z0,Z1,Y0,Y1,Y,Z] :
( ( ~ cc(Z)
| ~ rt1(Y,Z)
| ( sk12(X,Y) != sk13(X,Y)
& rtt(Y,sk13(X,Y))
& rtt(Y,sk12(X,Y)) )
| ~ rr1(X,Y)
| ( sk10(X) != sk11(X)
& rr(X,sk11(X))
& rr(X,sk10(X)) )
| ~ cd(Z)
| ~ rt2(Y,Z)
| ( sk8(X,Y) != sk9(X,Y)
& rtt(Y,sk9(X,Y))
& rtt(Y,sk8(X,Y)) )
| ~ rr2(X,Y)
| ( sk6(X,Y) != sk7(X,Y)
& rtt(Y,sk7(X,Y))
& rtt(Y,sk6(X,Y)) )
| ~ ce(Z)
| ~ rt3(Y,Z)
| ~ rr3(X,Y)
| cUnsatisfiable(X) )
& ( ( cc(sk5(X))
& rt1(sk4(X),sk5(X))
& ( Z0 = Z1
| ~ rtt(sk4(X),Z1)
| ~ rtt(sk4(X),Z0) )
& rr1(X,sk4(X))
& ( Y0 = Y1
| ~ rr(X,Y1)
| ~ rr(X,Y0) )
& cd(sk3(X))
& rt2(sk2(X),sk3(X))
& ( Z0 = Z1
| ~ rtt(sk2(X),Z1)
| ~ rtt(sk2(X),Z0) )
& rr2(X,sk2(X))
& ( Z0 = Z1
| ~ rtt(sk0(X),Z1)
| ~ rtt(sk0(X),Z0) )
& ce(sk1(X))
& rt3(sk0(X),sk1(X))
& rr3(X,sk0(X)) )
| ~ cUnsatisfiable(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10,sk11,sk12,sk13])],[f27_nnf]) ).
cnf(c32,plain,
( X3 = X4
| ~ rtt(sk0(X0),X4)
| ~ rtt(sk0(X0),X3)
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
fof(f29,axiom,
cUnsatisfiable(i2003_11_14_17_20_25524),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
fof(f29_nnf,plain,
cUnsatisfiable(i2003_11_14_17_20_25524),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c126,plain,
cUnsatisfiable(i2003_11_14_17_20_25524),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(p172,plain,
( X0 = X1
| ~ rtt(sk0(i2003_11_14_17_20_25524),X1)
| ~ rtt(sk0(i2003_11_14_17_20_25524),X0) ),
inference(resolution,[status(thm)],[c32,c126]) ).
cnf(c30,plain,
( rt3(sk0(X0),sk1(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p150,plain,
rt3(sk0(i2003_11_14_17_20_25524),sk1(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[c30,c126]) ).
fof(f38,axiom,
! [X,Y] :
( rt3(X,Y)
=> rtt(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_13) ).
fof(f38_nnf,plain,
! [X,Y] :
( rtt(X,Y)
| ~ rt3(X,Y) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X,Y] :
( rtt(X,Y)
| ~ rt3(X,Y) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c135,plain,
( rtt(X0,X1)
| ~ rt3(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p151,plain,
rtt(sk0(i2003_11_14_17_20_25524),sk1(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[p150,c135]) ).
cnf(p173,plain,
( sk1(i2003_11_14_17_20_25524) = X0
| ~ rtt(sk0(i2003_11_14_17_20_25524),X0) ),
inference(resolution,[status(thm)],[p172,p151]) ).
cnf(c37,plain,
( X5 = X6
| ~ rr(X0,X6)
| ~ rr(X0,X5)
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p156,plain,
( X0 = X1
| ~ rr(i2003_11_14_17_20_25524,X1)
| ~ rr(i2003_11_14_17_20_25524,X0) ),
inference(resolution,[status(thm)],[c37,c126]) ).
fof(f34,axiom,
! [X,Y] :
( rr2(X,Y)
=> rr(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
fof(f34_nnf,plain,
! [X,Y] :
( rr(X,Y)
| ~ rr2(X,Y) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [X,Y] :
( rr(X,Y)
| ~ rr2(X,Y) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c131,plain,
( rr(X0,X1)
| ~ rr2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(c33,plain,
( rr2(X0,sk2(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p145,plain,
rr2(i2003_11_14_17_20_25524,sk2(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[c33,c126]) ).
cnf(p148,plain,
rr(i2003_11_14_17_20_25524,sk2(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[c131,p145]) ).
cnf(p158,plain,
( sk2(i2003_11_14_17_20_25524) = X0
| ~ rr(i2003_11_14_17_20_25524,X0) ),
inference(resolution,[status(thm)],[p156,p148]) ).
fof(f37,axiom,
! [X,Y] :
( rr3(X,Y)
=> rr(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_12) ).
fof(f37_nnf,plain,
! [X,Y] :
( rr(X,Y)
| ~ rr3(X,Y) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [X,Y] :
( rr(X,Y)
| ~ rr3(X,Y) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c134,plain,
( rr(X0,X1)
| ~ rr3(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(c29,plain,
( rr3(X0,sk0(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p144,plain,
rr3(i2003_11_14_17_20_25524,sk0(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[c29,c126]) ).
cnf(p149,plain,
rr(i2003_11_14_17_20_25524,sk0(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[c134,p144]) ).
cnf(p164,plain,
sk2(i2003_11_14_17_20_25524) = sk0(i2003_11_14_17_20_25524),
inference(resolution,[status(thm)],[p158,p149]) ).
cnf(c35,plain,
( rt2(sk2(X0),sk3(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p152,plain,
rt2(sk2(i2003_11_14_17_20_25524),sk3(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[c35,c126]) ).
fof(f36,axiom,
! [X,Y] :
( rt2(X,Y)
=> rtt(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_11) ).
fof(f36_nnf,plain,
! [X,Y] :
( rtt(X,Y)
| ~ rt2(X,Y) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X,Y] :
( rtt(X,Y)
| ~ rt2(X,Y) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c133,plain,
( rtt(X0,X1)
| ~ rt2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p153,plain,
rtt(sk2(i2003_11_14_17_20_25524),sk3(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[p152,c133]) ).
cnf(p167,plain,
rtt(sk0(i2003_11_14_17_20_25524),sk3(i2003_11_14_17_20_25524)),
inference(demodulation,[status(thm)],[p164,p153]) ).
cnf(p176,plain,
sk1(i2003_11_14_17_20_25524) = sk3(i2003_11_14_17_20_25524),
inference(resolution,[status(thm)],[p173,p167]) ).
cnf(c36,plain,
( cd(sk3(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p139,plain,
cd(sk3(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[c36,c126]) ).
cnf(p178,plain,
cd(sk1(i2003_11_14_17_20_25524)),
inference(superposition,[status(thm)],[p176,p139]) ).
cnf(c31,plain,
( ce(sk1(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(p136,plain,
ce(sk1(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[c31,c126]) ).
fof(f32,axiom,
! [X] :
~ ( cd(X)
& ce(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
fof(f32_nnf,plain,
! [X] :
( ~ cd(X)
| ~ ce(X) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [X] :
( ~ cd(X)
| ~ ce(X) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c129,plain,
( ~ cd(X0)
| ~ ce(X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p138,plain,
~ cd(sk1(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[p136,c129]) ).
cnf(p201,plain,
$false,
inference(resolution,[status(thm)],[p178,p138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS098+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 19:23:58 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.97/1.12 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.97/1.12 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------