%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO068-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Sun Sep 27 07:16:58 AM UTC 2026
% Result : Unsatisfiable 12.60s 2.21s
% Output : CNFRefutation 12.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 44 ( 17 unt; 0 def)
% Number of atoms : 93 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 87 ( 38 ~; 49 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 50 ( 0 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(colinearity1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( colinear(VAR_0,VAR_1,VAR_2)
| ~ between(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',colinearity1) ).
cnf(c_19,plain,
( colinear(A,B,C)
| ~ between(A,B,C) ),
inference(clausify,[status(thm)],[colinearity1]) ).
fof(colinearity2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( colinear(VAR_2,VAR_0,VAR_1)
| ~ between(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',colinearity2) ).
cnf(c_20,plain,
( colinear(C,A,B)
| ~ between(A,B,C) ),
inference(clausify,[status(thm)],[colinearity2]) ).
fof(colinearity3,axiom,
! [VAR_0,VAR_1,VAR_2] :
( colinear(VAR_1,VAR_2,VAR_0)
| ~ between(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',colinearity3) ).
cnf(c_21,plain,
( colinear(B,C,A)
| ~ between(A,B,C) ),
inference(clausify,[status(thm)],[colinearity3]) ).
fof(colinearity4,axiom,
! [VAR_0,VAR_1,VAR_2] :
( between(VAR_2,VAR_0,VAR_1)
| between(VAR_1,VAR_2,VAR_0)
| between(VAR_0,VAR_1,VAR_2)
| ~ colinear(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',colinearity4) ).
cnf(c_22,plain,
( between(C,A,B)
| between(B,C,A)
| between(A,B,C)
| ~ colinear(A,B,C) ),
inference(clausify,[status(thm)],[colinearity4]) ).
fof(d4_2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( equidistant(VAR_1,VAR_0,VAR_3,VAR_2)
| ~ equidistant(VAR_0,VAR_1,VAR_2,VAR_3) ),
file('theBenchmark.p',d4_2) ).
cnf(c_29,plain,
( equidistant(B,A,D,C)
| ~ equidistant(A,B,C,D) ),
inference(clausify,[status(thm)],[d4_2]) ).
fof(b11,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( between(VAR_2,VAR_3,VAR_5)
| ~ between(VAR_0,VAR_1,VAR_4)
| ~ equidistant(VAR_0,VAR_4,VAR_2,VAR_5)
| ~ equidistant(VAR_1,VAR_4,VAR_3,VAR_5)
| ~ equidistant(VAR_0,VAR_1,VAR_2,VAR_3) ),
file('theBenchmark.p',b11) ).
cnf(c_93,plain,
( between(C,D,F)
| ~ between(A,B,E)
| ~ equidistant(A,E,C,F)
| ~ equidistant(B,E,D,F)
| ~ equidistant(A,B,C,D) ),
inference(clausify,[status(thm)],[b11]) ).
fof(u_to_v_equals_u1_to_v1,axiom,
equidistant(u,v,u1,v1),
file('theBenchmark.p',u_to_v_equals_u1_to_v1) ).
cnf(c_114,plain,
equidistant(u,v,u1,v1),
inference(clausify,[status(thm)],[u_to_v_equals_u1_to_v1]) ).
fof(v_to_w_equals_v1_to_w1,axiom,
equidistant(v,w,v1,w1),
file('theBenchmark.p',v_to_w_equals_v1_to_w1) ).
cnf(c_115,plain,
equidistant(v,w,v1,w1),
inference(clausify,[status(thm)],[v_to_w_equals_v1_to_w1]) ).
fof(u_to_w_equals_u1_to_w1,axiom,
equidistant(u,w,u1,w1),
file('theBenchmark.p',u_to_w_equals_u1_to_w1) ).
cnf(c_116,plain,
equidistant(u,w,u1,w1),
inference(clausify,[status(thm)],[u_to_w_equals_u1_to_w1]) ).
fof(uvw_colinear,axiom,
colinear(u,v,w),
file('theBenchmark.p',uvw_colinear) ).
cnf(c_117,plain,
colinear(u,v,w),
inference(clausify,[status(thm)],[uvw_colinear]) ).
fof(prove_u1v1w1_colinear,axiom,
~ colinear(u1,v1,w1),
file('theBenchmark.p',prove_u1v1w1_colinear) ).
cnf(c_118,plain,
~ colinear(u1,v1,w1),
inference(clausify,[status(thm)],[prove_u1v1w1_colinear]) ).
cnf(c_570,plain,
equidistant(v,u,v1,u1),
inference(resolve,[status(thm)],[c_114,c_29]) ).
cnf(c_611,plain,
equidistant(w,v,w1,v1),
inference(resolve,[status(thm)],[c_115,c_29]) ).
cnf(c_652,plain,
equidistant(w,u,w1,u1),
inference(resolve,[status(thm)],[c_116,c_29]) ).
cnf(c_676,plain,
( between(w,u,v)
| between(v,w,u)
| between(u,v,w) ),
inference(resolve,[status(thm)],[c_117,c_22]) ).
cnf(c_3476,plain,
( between(w1,u1,B)
| ~ between(w,u,A)
| ~ equidistant(w,A,w1,B)
| ~ equidistant(u,A,u1,B) ),
inference(resolve,[status(thm)],[c_93,c_652]) ).
cnf(c_3477,plain,
( between(w1,u1,v1)
| ~ between(w,u,v)
| ~ equidistant(w,v,w1,v1) ),
inference(resolve,[status(thm)],[c_3476,c_114]) ).
cnf(c_3478,plain,
( between(w1,u1,v1)
| ~ between(w,u,v) ),
inference(resolve,[status(thm)],[c_3477,c_611]) ).
cnf(c_2320,plain,
( between(v,w,u)
| between(u,v,w)
| between(w1,u1,v1) ),
inference(resolve,[status(thm)],[c_3478,c_676]) ).
cnf(c_3479,plain,
( colinear(u1,v1,w1)
| between(v,w,u)
| between(u,v,w) ),
inference(resolve,[status(thm)],[c_2320,c_21]) ).
cnf(c_2754,plain,
( between(v,w,u)
| between(u,v,w) ),
inference(resolve,[status(thm)],[c_118,c_3479]) ).
cnf(c_3480,plain,
( between(v1,w1,B)
| ~ between(v,w,A)
| ~ equidistant(v,A,v1,B)
| ~ equidistant(w,A,w1,B) ),
inference(resolve,[status(thm)],[c_93,c_115]) ).
cnf(c_3481,plain,
( between(v1,w1,u1)
| ~ between(v,w,u)
| ~ equidistant(v,u,v1,u1) ),
inference(resolve,[status(thm)],[c_3480,c_652]) ).
cnf(c_3482,plain,
( between(v1,w1,u1)
| ~ between(v,w,u) ),
inference(resolve,[status(thm)],[c_3481,c_570]) ).
cnf(c_2829,plain,
( between(u,v,w)
| between(v1,w1,u1) ),
inference(resolve,[status(thm)],[c_3482,c_2754]) ).
cnf(c_3483,plain,
( colinear(u1,v1,w1)
| between(u,v,w) ),
inference(resolve,[status(thm)],[c_2829,c_20]) ).
cnf(c_3108,plain,
between(u,v,w),
inference(resolve,[status(thm)],[c_118,c_3483]) ).
cnf(c_3484,plain,
( between(u1,v1,B)
| ~ between(u,v,A)
| ~ equidistant(u,A,u1,B)
| ~ equidistant(v,A,v1,B) ),
inference(resolve,[status(thm)],[c_93,c_114]) ).
cnf(c_3485,plain,
( between(u1,v1,w1)
| ~ between(u,v,w)
| ~ equidistant(u,w,u1,w1) ),
inference(resolve,[status(thm)],[c_3484,c_115]) ).
cnf(c_3486,plain,
( between(u1,v1,w1)
| ~ between(u,v,w) ),
inference(resolve,[status(thm)],[c_3485,c_116]) ).
cnf(c_3184,plain,
between(u1,v1,w1),
inference(resolve,[status(thm)],[c_3486,c_3108]) ).
cnf(c_3487,plain,
colinear(u1,v1,w1),
inference(resolve,[status(thm)],[c_3184,c_19]) ).
cnf(c_3475,plain,
$false,
inference(resolve,[status(thm)],[c_118,c_3487]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO068-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.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 : Fri Sep 25 12:41:57 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 1364816 was started by sandbox on n015,
% 0.09/0.37 % Fri Sep 25 12:41:57 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 12.60/2.21
% 12.60/2.21 % SZS status Unsatisfiable for theBenchmark
% 12.60/2.21
% 12.60/2.21 % Proof 1 at 1.47 (+ 0.27) seconds.
% 12.60/2.21 % Length of proof is 21.
% 12.60/2.21 % Level of proof is 7.
% 12.60/2.21 % Maximum clause weight is 28.000.
% 12.60/2.21 % Given clauses 254.
% 12.60/2.21
% 12.60/2.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------