%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : KRS098+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 : Thu Sep 24 12:59:41 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.37s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 9
% Syntax : Number of formulae : 53 ( 18 unt; 2 def)
% Number of atoms : 256 ( 32 equ)
% Maximal formula atoms : 36 ( 4 avg)
% Number of connectives : 307 ( 104 ~; 98 |; 93 &)
% ( 5 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-2 aty)
% Number of variables : 169 ( 121 !; 48 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,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/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
cUnsatisfiable(i2003_11_14_17_20_25524),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [X] :
~ ( cc(X)
& ce(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,axiom,
! [X,Y] :
( rr1(X,Y)
=> rr(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [X,Y] :
( rt1(X,Y)
=> rtt(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [X,Y] :
( rr3(X,Y)
=> rr(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [X,Y] :
( rt3(X,Y)
=> rtt(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,plain,
! [X] :
( 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) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f123,definition,
! [Y,Z0,Z1] :
( sP0_prd(Z1,Z0,Y)
<=> ( Z0 = Z1
| ~ rtt(Y,Z1)
| ~ rtt(Y,Z0) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f124,definition,
! [Y,Z0,Z1] :
( sP1_prd(Z1,Z0,Y)
<=> ( Z0 = Z1
| ~ rtt(Y,Z1)
| ~ rtt(Y,Z0) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f125,plain,
! [X] :
( 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] : sP1_prd(Z1,Z0,Y)
& rr2(X,Y) )
& ? [Y] :
( ! [Z0,Z1] : sP0_prd(Z1,Z0,Y)
& ? [Z] :
( ce(Z)
& rt3(Y,Z) )
& rr3(X,Y) ) ) ),
inference(formula_renaming,[status(thm)],[f122,f124,f123]) ).
fof(f126,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] : ~ sP1_prd(Z1,Z0,Y)
| ~ rr2(X,Y) )
| ! [Y] :
( ? [Z0,Z1] : ~ sP0_prd(Z1,Z0,Y)
| ! [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] : sP1_prd(Z1,Z0,Y)
& rr2(X,Y) )
& ? [Y] :
( ! [Z0,Z1] : sP0_prd(Z1,Z0,Y)
& ? [Z] :
( ce(Z)
& rt3(Y,Z) )
& rr3(X,Y) ) )
| ~ cUnsatisfiable(X) ) ),
inference(NNF_transformation,[status(thm)],[f125]) ).
fof(f127,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] : ~ sP1_prd(Z1,Z0,Y)
| ~ rr2(X,Y) )
| ! [Y] :
( ? [Z0,Z1] : ~ sP0_prd(Z1,Z0,Y)
| ! [Z] :
( ~ ce(Z)
| ~ rt3(Y,Z) )
| ~ rr3(X,Y) )
| cUnsatisfiable(X) )
& ! [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] : sP1_prd(Z1,Z0,Y)
& rr2(X,Y) )
& ? [Y] :
( ! [Z0,Z1] : sP0_prd(Z1,Z0,Y)
& ? [Z] :
( ce(Z)
& rt3(Y,Z) )
& rr3(X,Y) ) )
| ~ cUnsatisfiable(X) ) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,plain,
( ! [X] :
( ! [Y] :
( ! [Z] :
( ~ cc(Z)
| ~ rt1(Y,Z) )
| ( sK12_skl(Y,X) != sK13_skl(Y,X)
& rtt(Y,sK13_skl(Y,X))
& rtt(Y,sK12_skl(Y,X)) )
| ~ rr1(X,Y) )
| ( sK10_skl(X) != sK11_skl(X)
& rr(X,sK11_skl(X))
& rr(X,sK10_skl(X)) )
| ! [Y] :
( ! [Z] :
( ~ cd(Z)
| ~ rt2(Y,Z) )
| ~ sP1_prd(sK9_skl(Y,X),sK8_skl(Y,X),Y)
| ~ rr2(X,Y) )
| ! [Y] :
( ~ sP0_prd(sK7_skl(Y,X),sK6_skl(Y,X),Y)
| ! [Z] :
( ~ ce(Z)
| ~ rt3(Y,Z) )
| ~ rr3(X,Y) )
| cUnsatisfiable(X) )
& ! [X] :
( ( cc(sK5_skl(X))
& rt1(sK4_skl(X),sK5_skl(X))
& ! [Z0,Z1] :
( Z0 = Z1
| ~ rtt(sK4_skl(X),Z1)
| ~ rtt(sK4_skl(X),Z0) )
& rr1(X,sK4_skl(X))
& ! [Y0,Y1] :
( Y0 = Y1
| ~ rr(X,Y1)
| ~ rr(X,Y0) )
& cd(sK3_skl(X))
& rt2(sK2_skl(X),sK3_skl(X))
& ! [Z0,Z1] : sP1_prd(Z1,Z0,sK2_skl(X))
& rr2(X,sK2_skl(X))
& ! [Z0,Z1] : sP0_prd(Z1,Z0,sK0_skl(X))
& ce(sK1_skl(X))
& rt3(sK0_skl(X),sK1_skl(X))
& rr3(X,sK0_skl(X)) )
| ~ cUnsatisfiable(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(Y,sK0_skl(X)),skolemize(Z,sK1_skl(X)),skolemize(Y,sK2_skl(X)),skolemize(Z,sK3_skl(X)),skolemize(Y,sK4_skl(X)),skolemize(Z,sK5_skl(X)),skolemize(Z0,sK6_skl(Y,X)),skolemize(Z1,sK7_skl(Y,X)),skolemize(Z0,sK8_skl(Y,X)),skolemize(Z1,sK9_skl(Y,X)),skolemize(Y0,sK10_skl(X)),skolemize(Y1,sK11_skl(X)),skolemize(Z0,sK12_skl(Y,X)),skolemize(Z1,sK13_skl(Y,X))],[f127]) ).
fof(f129,plain,
! [X0] :
( rr3(X0,sK0_skl(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f130,plain,
! [X0] :
( rt3(sK0_skl(X0),sK1_skl(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,plain,
! [X0] :
( ce(sK1_skl(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f137,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ rr(X0,X2)
| ~ rr(X0,X1)
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f138,plain,
! [X0] :
( rr1(X0,sK4_skl(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f139,plain,
! [X0,X1,X2] :
( X1 = X2
| ~ rtt(sK4_skl(X0),X2)
| ~ rtt(sK4_skl(X0),X1)
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f140,plain,
! [X0] :
( rt1(sK4_skl(X0),sK5_skl(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f141,plain,
! [X0] :
( cc(sK5_skl(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f156,plain,
cUnsatisfiable(i2003_11_14_17_20_25524),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f159,plain,
! [X] :
( ~ cc(X)
| ~ ce(X) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f160,plain,
! [X0] :
( ~ cc(X0)
| ~ ce(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f163,plain,
! [X,Y] :
( rr(X,Y)
| ~ rr1(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f164,plain,
! [X0,X1] :
( rr(X0,X1)
| ~ rr1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f167,plain,
! [X,Y] :
( rtt(X,Y)
| ~ rt1(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f168,plain,
! [X0,X1] :
( rtt(X0,X1)
| ~ rt1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f171,plain,
! [X,Y] :
( rr(X,Y)
| ~ rr3(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f172,plain,
! [X0,X1] :
( rr(X0,X1)
| ~ rr3(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,plain,
! [X,Y] :
( rtt(X,Y)
| ~ rt3(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f39]) ).
fof(f174,plain,
! [X0,X1] :
( rtt(X0,X1)
| ~ rt3(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f190,plain,
ce(sK1_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f131,f156]) ).
fof(f191,plain,
rr3(i2003_11_14_17_20_25524,sK0_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f129,f156]) ).
fof(f195,plain,
cc(sK5_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f141,f156]) ).
fof(f196,plain,
rt3(sK0_skl(i2003_11_14_17_20_25524),sK1_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f130,f156]) ).
fof(f197,plain,
~ ce(sK5_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f195,f160]) ).
fof(f201,plain,
rr(i2003_11_14_17_20_25524,sK0_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f191,f172]) ).
fof(f204,plain,
rr1(i2003_11_14_17_20_25524,sK4_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f138,f156]) ).
fof(f205,plain,
rr(i2003_11_14_17_20_25524,sK4_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f204,f164]) ).
fof(f210,plain,
rtt(sK0_skl(i2003_11_14_17_20_25524),sK1_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f196,f174]) ).
fof(f212,plain,
rt1(sK4_skl(i2003_11_14_17_20_25524),sK5_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f140,f156]) ).
fof(f213,plain,
rtt(sK4_skl(i2003_11_14_17_20_25524),sK5_skl(i2003_11_14_17_20_25524)),
inference(resolution,[status(thm)],[f212,f168]) ).
fof(f214,plain,
! [X0] :
( sK4_skl(i2003_11_14_17_20_25524) = X0
| ~ rr(i2003_11_14_17_20_25524,X0)
| ~ cUnsatisfiable(i2003_11_14_17_20_25524) ),
inference(resolution,[status(thm)],[f137,f205]) ).
fof(f217,plain,
! [X0] :
( sK4_skl(i2003_11_14_17_20_25524) = X0
| ~ rr(i2003_11_14_17_20_25524,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f214,f156]) ).
fof(f222,plain,
sK4_skl(i2003_11_14_17_20_25524) = sK0_skl(i2003_11_14_17_20_25524),
inference(resolution,[status(thm)],[f217,f201]) ).
fof(f228,plain,
rtt(sK4_skl(i2003_11_14_17_20_25524),sK1_skl(i2003_11_14_17_20_25524)),
inference(backward_demodulation,[status(thm)],[f222,f210]) ).
fof(f234,plain,
! [X0] :
( sK5_skl(i2003_11_14_17_20_25524) = X0
| ~ rtt(sK4_skl(i2003_11_14_17_20_25524),X0)
| ~ cUnsatisfiable(i2003_11_14_17_20_25524) ),
inference(resolution,[status(thm)],[f139,f213]) ).
fof(f235,plain,
! [X0] :
( sK5_skl(i2003_11_14_17_20_25524) = X0
| ~ rtt(sK4_skl(i2003_11_14_17_20_25524),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f234,f156]) ).
fof(f247,plain,
sK5_skl(i2003_11_14_17_20_25524) = sK1_skl(i2003_11_14_17_20_25524),
inference(resolution,[status(thm)],[f235,f228]) ).
fof(f252,plain,
ce(sK5_skl(i2003_11_14_17_20_25524)),
inference(backward_demodulation,[status(thm)],[f247,f190]) ).
fof(f253,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f252,f197]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS098+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n006.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 : Sun Sep 20 22:53:33 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.37 % Refutation found
% 0.12/0.37 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.38 % Elapsed time: 0.029717 seconds
% 0.12/0.38 % CPU time: 0.093282 seconds
% 0.12/0.38 % Total memory used: 4.665 MB
% 0.12/0.38 % Net memory used: 4.481 MB
%------------------------------------------------------------------------------