%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GEO013-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 : n011.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:46 PM UTC 2026
% Result : Unsatisfiable 3.49s 26.50s
% Output : CNFRefutation 1.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of formulae : 40 ( 21 unt; 0 def)
% Number of atoms : 74 ( 14 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 70 ( 36 ~; 34 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 47 ( 47 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f91,axiom,
! [U,V,W] :
( colinear(W,V,U)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [U,V,W] :
( colinear(V,W,U)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [U,V,W] :
( colinear(U,W,V)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,axiom,
! [U,V,W,X] :
( U = V
| colinear(U,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,axiom,
! [U,V,W,X] :
( U = V
| colinear(V,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,hypothesis,
a != b,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,hypothesis,
colinear(a,b,d1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,hypothesis,
colinear(a,b,d2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,hypothesis,
colinear(a,b,d3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,negated_conjecture,
~ colinear(d1,d2,d3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f236,plain,
! [X0,X1,X2] :
( colinear(X2,X1,X0)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f237,plain,
! [X0,X1,X2] :
( colinear(X1,X2,X0)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f238,plain,
! [X0,X1,X2] :
( colinear(X0,X2,X1)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f249,plain,
! [U,V] :
( U = V
| ! [W,X] :
( colinear(U,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ) ),
inference(miniscoping,[status(thm)],[f102]) ).
fof(f250,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| colinear(X0,X2,X3)
| ~ colinear(X0,X1,X3)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f251,plain,
! [U,V] :
( U = V
| ! [W,X] :
( colinear(V,W,X)
| ~ colinear(U,V,X)
| ~ colinear(U,V,W) ) ),
inference(miniscoping,[status(thm)],[f103]) ).
fof(f252,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| colinear(X1,X2,X3)
| ~ colinear(X0,X1,X3)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f251]) ).
fof(f257,plain,
a != b,
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f258,plain,
colinear(a,b,d1),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f259,plain,
colinear(a,b,d2),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f260,plain,
colinear(a,b,d3),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f261,plain,
~ colinear(d1,d2,d3),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f277,plain,
~ colinear(d3,d2,d1),
inference(resolution,[status(thm)],[f236,f261]) ).
fof(f298,plain,
~ colinear(d1,d3,d2),
inference(resolution,[status(thm)],[f237,f277]) ).
fof(f299,plain,
~ colinear(d3,d1,d2),
inference(resolution,[status(thm)],[f237,f261]) ).
fof(f355,plain,
~ colinear(d2,d1,d3),
inference(resolution,[status(thm)],[f298,f237]) ).
fof(f363,plain,
~ colinear(d2,d3,d1),
inference(resolution,[status(thm)],[f299,f237]) ).
fof(f408,plain,
! [X0] :
( a = b
| colinear(a,X0,d3)
| ~ colinear(a,b,X0) ),
inference(resolution,[status(thm)],[f250,f260]) ).
fof(f409,plain,
! [X0] :
( a = b
| colinear(a,X0,d2)
| ~ colinear(a,b,X0) ),
inference(resolution,[status(thm)],[f250,f259]) ).
fof(f434,plain,
! [X0] :
( colinear(a,X0,d3)
| ~ colinear(a,b,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f257]) ).
fof(f435,plain,
! [X0] :
( colinear(a,X0,d2)
| ~ colinear(a,b,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f409,f257]) ).
fof(f476,plain,
! [X0] :
( X0 = d2
| ~ colinear(X0,d2,d1)
| ~ colinear(X0,d2,d3) ),
inference(resolution,[status(thm)],[f252,f363]) ).
fof(f855,plain,
colinear(a,d2,d3),
inference(resolution,[status(thm)],[f434,f259]) ).
fof(f856,plain,
colinear(a,d1,d3),
inference(resolution,[status(thm)],[f434,f258]) ).
fof(f874,plain,
( a = d2
| ~ colinear(a,d2,d1) ),
inference(resolution,[status(thm)],[f855,f476]) ).
fof(f892,plain,
( ~ colinear(a,d1,d2)
| a = d2 ),
inference(resolution,[status(thm)],[f874,f238]) ).
fof(f1712,plain,
colinear(a,d1,d2),
inference(resolution,[status(thm)],[f435,f258]) ).
fof(f1737,plain,
a = d2,
inference(backward_subsumption_resolution,[status(thm)],[f892,f1712]) ).
fof(f1786,plain,
~ colinear(a,d1,d3),
inference(backward_demodulation,[status(thm)],[f1737,f355]) ).
fof(f1815,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1786,f856]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO013-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/25.92 % CPULimit : 300
% 0.09/25.92 % WCLimit : 300
% 0.09/25.92 % DateTime : Sun Sep 20 08:16:17 UTC 2026
% 0.09/25.92 % CPUTime :
% 0.09/25.94 % Drodi V4.1.1
% 3.49/26.50 % Refutation found
% 3.49/26.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.49/26.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.86/26.51 % Elapsed time: 0.583396 seconds
% 1.86/26.51 % CPU time: 4.314521 seconds
% 1.86/26.51 % Total memory used: 132.223 MB
% 1.86/26.51 % Net memory used: 128.406 MB
%------------------------------------------------------------------------------