%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO009-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:23:44 PM UTC 2026
% Result : Unsatisfiable 72.99s 9.70s
% Output : CNFRefutation 23.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 32
% Syntax : Number of formulae : 123 ( 25 unt; 18 def)
% Number of atoms : 290 ( 39 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 287 ( 120 ~; 149 |; 0 &)
% ( 18 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 19 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 96 ( 96 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f32,axiom,
! [U,V] : between(U,V,reflection(U,V)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [U] : U = reflection(U,U),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [U,V] : U = reflection(reflection(U,V),V),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [U,V,W] :
( between(W,V,U)
| ~ between(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
! [U,V] : between(U,U,V),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [U,V,W] :
( U = V
| ~ between(V,U,W)
| ~ between(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [U,V,W,X] :
( between(V,W,X)
| ~ between(U,W,X)
| ~ between(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [U,V,W,X] :
( V = W
| between(U,W,X)
| ~ between(V,W,X)
| ~ between(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [U,V,W,X] :
( V = W
| between(U,V,X)
| ~ between(V,W,X)
| ~ between(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
! [U,W,X,V] :
( between(V,U,W)
| between(U,V,W)
| W = X
| ~ between(V,W,X)
| ~ between(U,W,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,hypothesis,
between(a,c,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,hypothesis,
between(a,d,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,hypothesis,
~ between(a,c,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,negated_conjecture,
~ between(a,d,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,plain,
! [X0,X1] : between(X0,X1,reflection(X0,X1)),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f124,plain,
! [X0] : reflection(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f136,plain,
! [X0,X1] : X0 = reflection(reflection(X0,X1),X1),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f140,plain,
! [X0,X1,X2] :
( ~ between(X2,X1,X0)
| between(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f141,plain,
! [X0,X1] : between(X0,X0,X1),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f142,plain,
! [U,V] :
( U = V
| ! [W] :
( ~ between(V,U,W)
| ~ between(U,V,W) ) ),
inference(miniscoping,[status(thm)],[f49]) ).
fof(f143,plain,
! [X0,X1,X2] :
( ~ between(X1,X0,X2)
| X1 = X0
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f152,plain,
! [V,W,X] :
( between(V,W,X)
| ! [U] :
( ~ between(U,W,X)
| ~ between(U,V,W) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( between(X3,X1,X2)
| ~ between(X0,X3,X1)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f154,plain,
! [V,W] :
( V = W
| ! [U,X] :
( between(U,W,X)
| ~ between(V,W,X)
| ~ between(U,V,W) ) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f155,plain,
! [X0,X1,X2,X3] :
( X2 = X1
| between(X0,X2,X3)
| ~ between(X1,X2,X3)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [V,W] :
( V = W
| ! [U,X] :
( between(U,V,X)
| ~ between(V,W,X)
| ~ between(U,V,W) ) ),
inference(miniscoping,[status(thm)],[f56]) ).
fof(f157,plain,
! [X0,X1,X2,X3] :
( between(X0,X1,X3)
| ~ between(X1,X2,X3)
| X2 = X1
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f192,plain,
! [U,W,V] :
( between(V,U,W)
| between(U,V,W)
| ! [X] :
( W = X
| ~ between(V,W,X)
| ~ between(U,W,X) ) ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f193,plain,
! [X0,X1,X2,X3] :
( ~ between(X3,X1,X0)
| ~ between(X2,X1,X0)
| between(X3,X2,X1)
| between(X2,X3,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f192]) ).
fof(f194,plain,
between(a,c,e),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f195,plain,
between(a,d,e),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f196,plain,
~ between(a,c,d),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f197,plain,
~ between(a,d,c),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f282,plain,
! [X0,X1,X2] :
( ~ between(X0,X2,reflection(X1,X2))
| reflection(X1,X2) = X2
| between(X1,X0,X2)
| between(X0,X1,X2) ),
inference(resolution,[status(thm)],[f193,f121]) ).
fof(f305,plain,
! [X0] :
( ~ between(X0,d,e)
| between(a,X0,d)
| between(X0,a,d)
| e = d ),
inference(resolution,[status(thm)],[f195,f193]) ).
fof(f306,plain,
( a = d
| ~ between(d,a,e) ),
inference(resolution,[status(thm)],[f195,f143]) ).
fof(f309,plain,
between(e,d,a),
inference(resolution,[status(thm)],[f195,f140]) ).
fof(f314,definition,
( sQ1_spl
<=> e = d ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f315,plain,
( ~ sQ1_spl
| d = e ),
inference(component_clause,[status(thm)],[f314]) ).
fof(f316,plain,
( sQ1_spl
| d != e ),
inference(component_clause,[status(thm)],[f314]) ).
fof(f318,definition,
! [X0] :
( sQ2_spl
<=> ( ~ between(X0,d,e)
| between(a,X0,d)
| between(X0,a,d) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f319,plain,
! [X0] :
( ~ sQ2_spl
| between(a,X0,d)
| ~ between(X0,d,e)
| between(X0,a,d) ),
inference(component_clause,[status(thm)],[f318]) ).
fof(f321,plain,
( sQ2_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f305,f314,f318]) ).
fof(f322,definition,
( sQ3_spl
<=> d = a ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f323,plain,
( ~ sQ3_spl
| d = a ),
inference(component_clause,[status(thm)],[f322]) ).
fof(f329,definition,
( sQ5_spl
<=> between(d,a,e) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f331,plain,
( sQ5_spl
| ~ between(d,a,e) ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f332,plain,
( sQ3_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f306,f329,f322]) ).
fof(f341,plain,
( ~ sQ3_spl
| ~ between(d,d,c) ),
inference(backward_demodulation,[status(thm)],[f323,f197]) ).
fof(f342,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f341,f141]) ).
fof(f343,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f342]) ).
fof(f356,definition,
( sQ6_spl
<=> between(c,a,d) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f357,plain,
( ~ sQ6_spl
| between(c,a,d) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,definition,
( sQ7_spl
<=> a = c ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f360,plain,
( ~ sQ7_spl
| c = a ),
inference(component_clause,[status(thm)],[f359]) ).
fof(f363,definition,
( sQ8_spl
<=> between(a,d,c) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f364,plain,
( ~ sQ8_spl
| between(a,d,c) ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f396,plain,
between(a,d,e),
inference(resolution,[status(thm)],[f309,f140]) ).
fof(f446,plain,
( ~ sQ7_spl
| ~ between(a,a,d) ),
inference(forward_demodulation,[status(thm)],[f360,f196]) ).
fof(f447,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f446,f141]) ).
fof(f448,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f447]) ).
fof(f463,plain,
( ~ sQ1_spl
| between(a,c,d) ),
inference(forward_demodulation,[status(thm)],[f315,f194]) ).
fof(f503,plain,
! [X0,X1,X2] :
( X2 = X1
| between(X0,X2,reflection(X1,X2))
| ~ between(X0,X1,X2) ),
inference(resolution,[status(thm)],[f155,f121]) ).
fof(f524,plain,
! [X0] :
( between(c,e,X0)
| ~ between(a,e,X0) ),
inference(resolution,[status(thm)],[f194,f153]) ).
fof(f527,plain,
! [X0] :
( between(X0,a,e)
| c = a
| ~ between(X0,a,c) ),
inference(resolution,[status(thm)],[f194,f157]) ).
fof(f532,plain,
! [X0] :
( ~ between(X0,c,e)
| between(a,X0,c)
| between(X0,a,c)
| e = c ),
inference(resolution,[status(thm)],[f194,f193]) ).
fof(f533,plain,
( a = c
| ~ between(c,a,e) ),
inference(resolution,[status(thm)],[f194,f143]) ).
fof(f538,definition,
! [X0] :
( sQ19_spl
<=> ( between(X0,a,e)
| ~ between(X0,a,c) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f539,plain,
! [X0] :
( ~ sQ19_spl
| ~ between(X0,a,c)
| between(X0,a,e) ),
inference(component_clause,[status(thm)],[f538]) ).
fof(f541,plain,
( sQ7_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f527,f538,f359]) ).
fof(f549,definition,
( sQ22_spl
<=> e = c ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f550,plain,
( ~ sQ22_spl
| e = c ),
inference(component_clause,[status(thm)],[f549]) ).
fof(f557,definition,
! [X0] :
( sQ24_spl
<=> ( ~ between(X0,c,e)
| between(a,X0,c)
| between(X0,a,c) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f558,plain,
! [X0] :
( ~ sQ24_spl
| ~ between(X0,c,e)
| between(a,X0,c)
| between(X0,a,c) ),
inference(component_clause,[status(thm)],[f557]) ).
fof(f560,plain,
( sQ24_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f532,f549,f557]) ).
fof(f561,definition,
( sQ25_spl
<=> between(c,a,e) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f563,plain,
( sQ25_spl
| ~ between(c,a,e) ),
inference(component_clause,[status(thm)],[f561]) ).
fof(f564,plain,
( sQ7_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f533,f561,f359]) ).
fof(f588,plain,
( ~ sQ22_spl
| ~ between(a,d,e) ),
inference(backward_demodulation,[status(thm)],[f550,f197]) ).
fof(f602,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f396,f588]) ).
fof(f603,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f602]) ).
fof(f700,plain,
! [X0] :
( between(X0,a,e)
| d = a
| ~ between(X0,a,d) ),
inference(resolution,[status(thm)],[f195,f157]) ).
fof(f726,definition,
! [X0] :
( sQ43_spl
<=> ( between(X0,a,e)
| ~ between(X0,a,d) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f727,plain,
! [X0] :
( ~ sQ43_spl
| ~ between(X0,a,d)
| between(X0,a,e) ),
inference(component_clause,[status(thm)],[f726]) ).
fof(f729,plain,
( sQ3_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f700,f726,f322]) ).
fof(f876,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f196]) ).
fof(f877,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f876]) ).
fof(f2352,plain,
( e = d
| between(a,e,reflection(d,e)) ),
inference(resolution,[status(thm)],[f503,f195]) ).
fof(f2375,definition,
( sQ138_spl
<=> between(a,e,reflection(d,e)) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f2376,plain,
( ~ sQ138_spl
| between(a,e,reflection(d,e)) ),
inference(component_clause,[status(thm)],[f2375]) ).
fof(f2378,plain,
( sQ1_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f2352,f2375,f314]) ).
fof(f4979,definition,
( sQ427_spl
<=> reflection(d,e) = e ),
introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition]) ).
fof(f4980,plain,
( ~ sQ427_spl
| reflection(d,e) = e ),
inference(component_clause,[status(thm)],[f4979]) ).
fof(f5184,plain,
( ~ sQ138_spl
| between(c,e,reflection(d,e)) ),
inference(resolution,[status(thm)],[f2376,f524]) ).
fof(f5331,plain,
( ~ sQ427_spl
| d = reflection(e,e) ),
inference(paramodulation,[status(thm)],[f4980,f136]) ).
fof(f5348,plain,
( ~ sQ427_spl
| d = e ),
inference(forward_demodulation,[status(thm)],[f124,f5331]) ).
fof(f5349,plain,
( ~ sQ427_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5348,f316]) ).
fof(f5350,plain,
( ~ sQ427_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f5349]) ).
fof(f10874,plain,
( ~ sQ138_spl
| reflection(d,e) = e
| between(d,c,e)
| between(c,d,e) ),
inference(resolution,[status(thm)],[f5184,f282]) ).
fof(f10924,definition,
( sQ1167_spl
<=> between(c,d,e) ),
introduced(definition,[new_symbols(definition,[sQ1167_spl])],[split_symbol_definition]) ).
fof(f10925,plain,
( ~ sQ1167_spl
| between(c,d,e) ),
inference(component_clause,[status(thm)],[f10924]) ).
fof(f10927,definition,
( sQ1168_spl
<=> between(d,c,e) ),
introduced(definition,[new_symbols(definition,[sQ1168_spl])],[split_symbol_definition]) ).
fof(f10928,plain,
( ~ sQ1168_spl
| between(d,c,e) ),
inference(component_clause,[status(thm)],[f10927]) ).
fof(f10930,plain,
( ~ sQ138_spl
| sQ427_spl
| sQ1168_spl
| sQ1167_spl ),
inference(split_clause,[status(thm)],[f10874,f10924,f10927,f4979,f2375]) ).
fof(f11033,plain,
( ~ sQ2_spl
| ~ sQ1167_spl
| between(a,c,d)
| between(c,a,d) ),
inference(resolution,[status(thm)],[f10925,f319]) ).
fof(f11190,definition,
( sQ1222_spl
<=> between(a,c,d) ),
introduced(definition,[new_symbols(definition,[sQ1222_spl])],[split_symbol_definition]) ).
fof(f11191,plain,
( ~ sQ1222_spl
| between(a,c,d) ),
inference(component_clause,[status(thm)],[f11190]) ).
fof(f11193,plain,
( ~ sQ2_spl
| ~ sQ1167_spl
| sQ1222_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f11033,f356,f11190,f10924,f318]) ).
fof(f11198,plain,
( ~ sQ1222_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11191,f196]) ).
fof(f11199,plain,
~ sQ1222_spl,
inference(contradiction_clause,[status(thm)],[f11198]) ).
fof(f11366,plain,
( ~ sQ43_spl
| ~ sQ6_spl
| between(c,a,e) ),
inference(resolution,[status(thm)],[f357,f727]) ).
fof(f11499,plain,
( ~ sQ43_spl
| ~ sQ6_spl
| sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11366,f563]) ).
fof(f11500,plain,
( ~ sQ43_spl
| ~ sQ6_spl
| sQ25_spl ),
inference(contradiction_clause,[status(thm)],[f11499]) ).
fof(f11501,plain,
( ~ sQ24_spl
| ~ sQ1168_spl
| between(a,d,c)
| between(d,a,c) ),
inference(resolution,[status(thm)],[f10928,f558]) ).
fof(f11615,definition,
( sQ1292_spl
<=> between(d,a,c) ),
introduced(definition,[new_symbols(definition,[sQ1292_spl])],[split_symbol_definition]) ).
fof(f11616,plain,
( ~ sQ1292_spl
| between(d,a,c) ),
inference(component_clause,[status(thm)],[f11615]) ).
fof(f11618,plain,
( ~ sQ24_spl
| ~ sQ1168_spl
| sQ8_spl
| sQ1292_spl ),
inference(split_clause,[status(thm)],[f11501,f11615,f363,f10927,f557]) ).
fof(f11828,plain,
( ~ sQ19_spl
| ~ sQ1292_spl
| between(d,a,e) ),
inference(resolution,[status(thm)],[f11616,f539]) ).
fof(f11889,plain,
( ~ sQ19_spl
| ~ sQ1292_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11828,f331]) ).
fof(f11890,plain,
( ~ sQ19_spl
| ~ sQ1292_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f11889]) ).
fof(f11891,plain,
( ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f364,f197]) ).
fof(f11892,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f11891]) ).
fof(f11893,plain,
$false,
inference(sat_refutation,[status(thm)],[f321,f332,f343,f448,f541,f560,f564,f603,f729,f877,f2378,f5350,f10930,f11193,f11199,f11500,f11618,f11890,f11892]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO009-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 08:10:11 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 72.99/9.70 % Refutation found
% 72.99/9.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 72.99/9.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 23.21/9.73 % Elapsed time: 9.351189 seconds
% 23.21/9.73 % CPU time: 73.898201 seconds
% 23.21/9.73 % Total memory used: 257.262 MB
% 23.21/9.73 % Net memory used: 226.742 MB
%------------------------------------------------------------------------------