%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GEO069-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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 0.07s 0.38s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 7
% Syntax : Number of formulae : 27 ( 15 unt; 0 def)
% Number of atoms : 49 ( 9 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 44 ( 22 ~; 22 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 26 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t10_2,axiom,
! [VAR_0,VAR_1,VAR_2] :
( colinear(VAR_1,VAR_2,VAR_0)
| ~ colinear(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',t10_2) ).
cnf(c_105,plain,
( colinear(B,C,A)
| ~ colinear(A,B,C) ),
inference(clausify,[status(thm)],[t10_2]) ).
fof(t12_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_0 = VAR_1
| colinear(VAR_0,VAR_2,VAR_3)
| ~ colinear(VAR_0,VAR_1,VAR_3)
| ~ colinear(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',t12_1) ).
cnf(c_115,plain,
( A = B
| colinear(A,C,D)
| ~ colinear(A,B,D)
| ~ colinear(A,B,C) ),
inference(clausify,[status(thm)],[t12_1]) ).
fof(t12_2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_0 = VAR_1
| colinear(VAR_1,VAR_2,VAR_3)
| ~ colinear(VAR_0,VAR_1,VAR_3)
| ~ colinear(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',t12_2) ).
cnf(c_116,plain,
( A = B
| colinear(B,C,D)
| ~ colinear(A,B,D)
| ~ colinear(A,B,C) ),
inference(clausify,[status(thm)],[t12_2]) ).
fof(u_not_v,axiom,
u != v,
file('theBenchmark.p',u_not_v) ).
cnf(c_117,plain,
u != v,
inference(clausify,[status(thm)],[u_not_v]) ).
cnf(c_118,plain,
v != u,
inference(copy,[status(thm)],[c_117]) ).
fof(wvu_colinear,axiom,
colinear(w,v,u),
file('theBenchmark.p',wvu_colinear) ).
cnf(c_119,plain,
colinear(w,v,u),
inference(clausify,[status(thm)],[wvu_colinear]) ).
fof(xvu_colinear,axiom,
colinear(x,v,u),
file('theBenchmark.p',xvu_colinear) ).
cnf(c_120,plain,
colinear(x,v,u),
inference(clausify,[status(thm)],[xvu_colinear]) ).
fof(prove_xwu_and_xwv_colinear,axiom,
( ~ colinear(x,w,v)
| ~ colinear(x,w,u) ),
file('theBenchmark.p',prove_xwu_and_xwv_colinear) ).
cnf(c_121,plain,
( ~ colinear(x,w,v)
| ~ colinear(x,w,u) ),
inference(clausify,[status(thm)],[prove_xwu_and_xwv_colinear]) ).
cnf(c_416,plain,
colinear(v,u,w),
inference(resolve,[status(thm)],[c_119,c_105]) ).
cnf(c_426,plain,
colinear(v,u,x),
inference(resolve,[status(thm)],[c_120,c_105]) ).
cnf(c_671,plain,
( v = u
| colinear(u,A,w)
| ~ colinear(v,u,A) ),
inference(resolve,[status(thm)],[c_416,c_116]) ).
cnf(c_478,plain,
( colinear(u,A,w)
| ~ colinear(v,u,A) ),
inference(resolve,[status(thm)],[c_118,c_671]) ).
cnf(c_672,plain,
( v = u
| colinear(v,A,w)
| ~ colinear(v,u,A) ),
inference(resolve,[status(thm)],[c_416,c_115]) ).
cnf(c_480,plain,
( colinear(v,A,w)
| ~ colinear(v,u,A) ),
inference(resolve,[status(thm)],[c_118,c_672]) ).
cnf(c_608,plain,
colinear(u,x,w),
inference(resolve,[status(thm)],[c_478,c_426]) ).
cnf(c_618,plain,
colinear(x,w,u),
inference(resolve,[status(thm)],[c_608,c_105]) ).
cnf(c_621,plain,
~ colinear(x,w,v),
inference(resolve,[status(thm)],[c_618,c_121]) ).
cnf(c_660,plain,
colinear(v,x,w),
inference(resolve,[status(thm)],[c_480,c_426]) ).
cnf(c_673,plain,
colinear(x,w,v),
inference(resolve,[status(thm)],[c_660,c_105]) ).
cnf(c_670,plain,
$false,
inference(resolve,[status(thm)],[c_621,c_673]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO069-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Fri Sep 25 12:38:20 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/0.31 % Process 2100945 was started by sandbox2 on n012,
% 0.03/0.31 % Fri Sep 25 12:38:20 2026
% 0.03/0.31 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.03/0.32
% 0.03/0.32 % From the command line: assign(max_seconds, 300).
% 0.07/0.38
% 0.07/0.38 % SZS status Unsatisfiable for theBenchmark
% 0.07/0.38
% 0.07/0.38 % Proof 1 at 0.04 (+ 0.01) seconds.
% 0.07/0.38 % Length of proof is 17.
% 0.07/0.38 % Level of proof is 6.
% 0.07/0.38 % Maximum clause weight is 15.000.
% 0.07/0.38 % Given clauses 159.
% 0.07/0.38
% 0.07/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------