%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GEO230+1 : TPTP v9.0.0. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 01:38:40 PM UTC 2025
% Result : Theorem 25.65s 3.58s
% Output : CNFRefutation 25.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 14
% Syntax : Number of formulae : 108 ( 55 unt; 0 def)
% Number of atoms : 248 ( 0 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 252 ( 112 ~; 123 |; 6 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 115 ( 22 sgn 36 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(con,plain,
! [A,B] :
( distinct_points(A,B)
=> ( ~ distinct_lines(line_connecting(A,B),line_connecting(B,A))
& ~ unequally_directed_lines(line_connecting(B,A),line_connecting(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',con) ).
fof(con_negated,plain,
~ ! [A,B] :
( distinct_points(A,B)
=> ( ~ distinct_lines(line_connecting(A,B),line_connecting(B,A))
& ~ unequally_directed_lines(line_connecting(B,A),line_connecting(A,B)) ) ),
inference(negate_conjecture,[status(cth)],[con]) ).
cnf(59,plain,
( unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(sK1,sK2))
| distinct_lines(line_connecting(sK1,sK2),line_connecting(sK2,sK1)) ),
inference(cnf,[status(esa)],[con_negated]) ).
cnf(l0,plain,
( unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(sK1,sK2))
| distinct_lines(line_connecting(sK1,sK2),line_connecting(sK2,sK1)) ),
inference(instantiation,[status(thm)],[59]) ).
fof(oaguc1,plain,
! [A,B,L,M] :
( ( distinct_points(A,B)
& distinct_lines(L,M) )
=> ( left_apart_point(A,L)
| left_apart_point(B,L)
| left_apart_point(A,M)
| left_apart_point(B,M)
| left_apart_point(A,reverse_line(L))
| left_apart_point(B,reverse_line(L))
| left_apart_point(A,reverse_line(M))
| left_apart_point(B,reverse_line(M)) ) ),
file('Axioms/GEO007+0.ax',oaguc1) ).
cnf(53,plain,
( ~ distinct_points(X0,X1)
| ~ distinct_lines(X2,X3)
| left_apart_point(X0,X2)
| left_apart_point(X0,X3)
| left_apart_point(X0,reverse_line(X2))
| left_apart_point(X0,reverse_line(X3))
| left_apart_point(X1,X2)
| left_apart_point(X1,X3)
| left_apart_point(X1,reverse_line(X2))
| left_apart_point(X1,reverse_line(X3)) ),
inference(cnf,[status(esa)],[oaguc1]) ).
cnf(l482,plain,
( ~ distinct_points(sK2,X0_812)
| ~ distinct_lines(line_connecting(sK1,sK2),line_connecting(sK2,sK1))
| left_apart_point(sK2,line_connecting(sK1,sK2))
| left_apart_point(sK2,line_connecting(sK2,sK1))
| left_apart_point(sK2,reverse_line(line_connecting(sK1,sK2)))
| left_apart_point(sK2,reverse_line(line_connecting(sK2,sK1)))
| left_apart_point(X0_812,line_connecting(sK1,sK2))
| left_apart_point(X0_812,line_connecting(sK2,sK1))
| left_apart_point(X0_812,reverse_line(line_connecting(sK1,sK2)))
| left_apart_point(X0_812,reverse_line(line_connecting(sK2,sK1))) ),
inference(instantiation,[status(thm)],[53]) ).
fof(oagsub1,plain,
! [A,B,L] :
( left_apart_point(A,L)
=> ( distinct_points(A,B)
| left_apart_point(B,L) ) ),
file('Axioms/GEO007+0.ax',oagsub1) ).
cnf(55,plain,
( ~ left_apart_point(X0,X1)
| left_apart_point(X2,X1)
| distinct_points(X0,X2) ),
inference(cnf,[status(esa)],[oagsub1]) ).
cnf(l510,plain,
( ~ left_apart_point(sK2,line_connecting(sK2,sK1))
| left_apart_point(sK1,line_connecting(sK2,sK1))
| distinct_points(sK2,sK1) ),
inference(instantiation,[status(thm)],[55]) ).
fof(oag6,plain,
! [L,M,N] :
( unequally_directed_lines(L,M)
=> ( unequally_directed_lines(L,N)
| unequally_directed_lines(M,N) ) ),
file('Axioms/GEO007+0.ax',oag6) ).
cnf(30,plain,
( ~ unequally_directed_lines(X0,X1)
| unequally_directed_lines(X0,X2)
| unequally_directed_lines(X1,X2) ),
inference(cnf,[status(esa)],[oag6]) ).
cnf(l1,plain,
( ~ unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(sK1,sK2))
| unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(X0_71,X0_71))
| unequally_directed_lines(line_connecting(sK1,sK2),line_connecting(X0_71,X0_71)) ),
inference(instantiation,[status(thm)],[30]) ).
fof(oaguc2,plain,
! [A,B,L] :
( ( distinct_points(A,B)
& left_apart_point(A,L) )
=> ( left_apart_point(B,L)
| left_convergent_lines(line_connecting(A,B),L) ) ),
file('Axioms/GEO007+0.ax',oaguc2) ).
cnf(54,plain,
( ~ left_apart_point(X0,X1)
| ~ distinct_points(X0,X2)
| left_apart_point(X2,X1)
| left_convergent_lines(line_connecting(X0,X2),X1) ),
inference(cnf,[status(esa)],[oaguc2]) ).
cnf(l506,plain,
( ~ left_apart_point(X0_812,reverse_line(line_connecting(sK1,sK2)))
| ~ distinct_points(X0_812,sK1)
| left_apart_point(sK1,reverse_line(line_connecting(sK1,sK2)))
| left_convergent_lines(line_connecting(X0_812,sK1),reverse_line(line_connecting(sK1,sK2))) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l485,plain,
( ~ left_apart_point(X0_812,line_connecting(sK2,sK1))
| left_apart_point(X0_500,line_connecting(sK2,sK1))
| distinct_points(X0_812,X0_500) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l522,plain,
( ~ left_apart_point(sK1,reverse_line(line_connecting(sK1,sK2)))
| ~ distinct_points(sK1,sK2)
| left_apart_point(sK2,reverse_line(line_connecting(sK1,sK2)))
| left_convergent_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(sK1,sK2))) ),
inference(instantiation,[status(thm)],[54]) ).
fof(oag10,plain,
! [A,L] :
~ ( left_apart_point(A,L)
| left_apart_point(A,reverse_line(L)) ),
file('Axioms/GEO007+0.ax',oag10) ).
cnf(37,plain,
~ left_apart_point(X0,X1),
inference(cnf,[status(esa)],[oag10]) ).
cnf(l525,plain,
~ left_apart_point(sK2,reverse_line(line_connecting(sK1,sK2))),
inference(instantiation,[status(thm)],[37]) ).
fof(oag11,plain,
! [L,M] :
~ ( left_convergent_lines(L,M)
| left_convergent_lines(L,reverse_line(M)) ),
file('Axioms/GEO007+0.ax',oag11) ).
cnf(39,plain,
~ left_convergent_lines(X0,X1),
inference(cnf,[status(esa)],[oag11]) ).
cnf(l698,plain,
~ left_convergent_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(sK1,sK2))),
inference(instantiation,[status(thm)],[39]) ).
cnf(58,plain,
distinct_points(sK1,sK2),
inference(cnf,[status(esa)],[con_negated]) ).
cnf(l531,plain,
distinct_points(sK1,sK2),
inference(instantiation,[status(thm)],[58]) ).
cnf(l487,plain,
~ left_apart_point(X0_500,line_connecting(sK2,sK1)),
inference(instantiation,[status(thm)],[37]) ).
cnf(40,plain,
~ left_convergent_lines(X0,reverse_line(X1)),
inference(cnf,[status(esa)],[oag11]) ).
cnf(l564,plain,
~ left_convergent_lines(line_connecting(X0_812,sK1),reverse_line(line_connecting(sK1,sK2))),
inference(instantiation,[status(thm)],[40]) ).
cnf(l488,plain,
( ~ left_apart_point(sK2,reverse_line(line_connecting(sK1,sK2)))
| ~ distinct_points(sK2,sK1)
| left_apart_point(sK1,reverse_line(line_connecting(sK1,sK2)))
| left_convergent_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(sK1,sK2))) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l495,plain,
( ~ left_apart_point(sK2,reverse_line(line_connecting(sK2,sK1)))
| left_apart_point(X0_626,reverse_line(line_connecting(sK2,sK1)))
| distinct_points(sK2,X0_626) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l556,plain,
~ left_convergent_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(sK1,sK2))),
inference(instantiation,[status(thm)],[40]) ).
fof(oag2,plain,
! [A,B,C] :
( distinct_points(A,B)
=> ( distinct_points(A,C)
| distinct_points(B,C) ) ),
file('Axioms/GEO007+0.ax',oag2) ).
cnf(26,plain,
( ~ distinct_points(X0,X1)
| distinct_points(X0,X2)
| distinct_points(X1,X2) ),
inference(cnf,[status(esa)],[oag2]) ).
cnf(l489,plain,
( ~ distinct_points(sK1,sK2)
| distinct_points(sK1,sK1)
| distinct_points(sK2,sK1) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l572,plain,
~ left_apart_point(X0_626,reverse_line(line_connecting(sK2,sK1))),
inference(instantiation,[status(thm)],[37]) ).
cnf(l623,plain,
( ~ left_apart_point(sK2,reverse_line(line_connecting(sK2,sK1)))
| ~ distinct_points(sK2,X0_626)
| left_apart_point(X0_626,reverse_line(line_connecting(sK2,sK1)))
| left_convergent_lines(line_connecting(sK2,X0_626),reverse_line(line_connecting(sK2,sK1))) ),
inference(instantiation,[status(thm)],[54]) ).
fof(oag1,plain,
! [A] : ~ distinct_points(A,A),
file('Axioms/GEO007+0.ax',oag1) ).
cnf(25,plain,
~ distinct_points(X0,X0),
inference(cnf,[status(esa)],[oag1]) ).
cnf(l490,plain,
~ distinct_points(sK1,sK1),
inference(instantiation,[status(thm)],[25]) ).
cnf(l515,plain,
~ left_apart_point(sK1,reverse_line(line_connecting(sK1,sK2))),
inference(instantiation,[status(thm)],[37]) ).
cnf(l501,plain,
( ~ distinct_points(sK2,sK1)
| distinct_points(sK2,X0_812)
| distinct_points(sK1,X0_812) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l782,plain,
( ~ distinct_points(sK1,X0_812)
| ~ distinct_lines(line_connecting(sK1,sK2),line_connecting(sK2,sK1))
| left_apart_point(sK1,line_connecting(sK1,sK2))
| left_apart_point(sK1,line_connecting(sK2,sK1))
| left_apart_point(sK1,reverse_line(line_connecting(sK1,sK2)))
| left_apart_point(sK1,reverse_line(line_connecting(sK2,sK1)))
| left_apart_point(X0_812,line_connecting(sK1,sK2))
| left_apart_point(X0_812,line_connecting(sK2,sK1))
| left_apart_point(X0_812,reverse_line(line_connecting(sK1,sK2)))
| left_apart_point(X0_812,reverse_line(line_connecting(sK2,sK1))) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(38,plain,
~ left_apart_point(X0,reverse_line(X1)),
inference(cnf,[status(esa)],[oag10]) ).
cnf(l793,plain,
~ left_apart_point(sK1,reverse_line(line_connecting(sK1,sK2))),
inference(instantiation,[status(thm)],[38]) ).
cnf(l813,plain,
~ left_apart_point(X0_812,reverse_line(line_connecting(sK1,sK2))),
inference(instantiation,[status(thm)],[37]) ).
cnf(l543,plain,
( ~ left_apart_point(X0_812,reverse_line(line_connecting(sK1,sK2)))
| left_apart_point(sK1,reverse_line(line_connecting(sK1,sK2)))
| distinct_points(X0_812,sK1) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l496,plain,
( ~ left_apart_point(X0_812,line_connecting(sK1,sK2))
| ~ distinct_points(X0_812,sK1)
| left_apart_point(sK1,line_connecting(sK1,sK2))
| left_convergent_lines(line_connecting(X0_812,sK1),line_connecting(sK1,sK2)) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l497,plain,
( ~ left_apart_point(sK1,line_connecting(sK1,sK2))
| ~ distinct_points(sK1,sK2)
| left_apart_point(sK2,line_connecting(sK1,sK2))
| left_convergent_lines(line_connecting(sK1,sK2),line_connecting(sK1,sK2)) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l560,plain,
distinct_points(sK1,sK2),
inference(instantiation,[status(thm)],[58]) ).
cnf(l491,plain,
distinct_points(sK1,sK2),
inference(instantiation,[status(thm)],[58]) ).
cnf(l566,plain,
~ left_apart_point(sK2,line_connecting(sK1,sK2)),
inference(instantiation,[status(thm)],[37]) ).
cnf(l728,plain,
~ left_convergent_lines(line_connecting(sK1,sK2),line_connecting(sK1,sK2)),
inference(instantiation,[status(thm)],[39]) ).
cnf(l486,plain,
~ left_apart_point(X0_812,reverse_line(line_connecting(sK2,sK1))),
inference(instantiation,[status(thm)],[37]) ).
cnf(l539,plain,
~ left_apart_point(sK1,line_connecting(sK2,sK1)),
inference(instantiation,[status(thm)],[37]) ).
cnf(l799,plain,
~ left_apart_point(sK1,line_connecting(sK2,sK1)),
inference(instantiation,[status(thm)],[37]) ).
cnf(l800,plain,
~ left_apart_point(sK1,line_connecting(sK1,sK2)),
inference(instantiation,[status(thm)],[37]) ).
cnf(l503,plain,
( ~ distinct_points(sK1,sK2)
| distinct_points(sK1,sK1)
| distinct_points(sK2,sK1) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l702,plain,
~ left_convergent_lines(line_connecting(sK2,X0_626),reverse_line(line_connecting(sK2,sK1))),
inference(instantiation,[status(thm)],[39]) ).
fof(oagsub3,plain,
! [L,M,N] :
( left_convergent_lines(L,M)
=> ( unequally_directed_lines(M,N)
| left_convergent_lines(L,N) ) ),
file('Axioms/GEO007+0.ax',oagsub3) ).
cnf(57,plain,
( ~ left_convergent_lines(X0,X1)
| unequally_directed_lines(X1,X2)
| left_convergent_lines(X0,X2) ),
inference(cnf,[status(esa)],[oagsub3]) ).
cnf(l511,plain,
( ~ left_convergent_lines(line_connecting(X0_812,sK1),line_connecting(sK1,sK2))
| unequally_directed_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(sK2,sK1)))
| left_convergent_lines(line_connecting(X0_812,sK1),reverse_line(line_connecting(sK2,sK1))) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l794,plain,
~ left_apart_point(X0_812,line_connecting(sK1,sK2)),
inference(instantiation,[status(thm)],[37]) ).
cnf(l620,plain,
~ left_convergent_lines(line_connecting(X0_812,sK1),reverse_line(line_connecting(sK2,sK1))),
inference(instantiation,[status(thm)],[40]) ).
cnf(l542,plain,
distinct_points(sK1,sK2),
inference(instantiation,[status(thm)],[58]) ).
cnf(l546,plain,
( ~ left_apart_point(X0_812,line_connecting(sK1,sK2))
| left_apart_point(sK1,line_connecting(sK1,sK2))
| distinct_points(X0_812,sK1) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l626,plain,
~ left_apart_point(X0_626,reverse_line(line_connecting(sK2,sK1))),
inference(instantiation,[status(thm)],[37]) ).
fof(oagco9,plain,
! [A,B] : ~ unequally_directed_lines(line_connecting(A,B),reverse_line(line_connecting(B,A))),
file('Axioms/GEO007+0.ax',oagco9) ).
cnf(51,plain,
~ unequally_directed_lines(line_connecting(X0,X1),reverse_line(line_connecting(X1,X0))),
inference(cnf,[status(esa)],[oagco9]) ).
cnf(l622,plain,
~ unequally_directed_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(sK2,sK1))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l811,plain,
~ left_apart_point(X0_812,line_connecting(sK2,sK1)),
inference(instantiation,[status(thm)],[37]) ).
cnf(l581,plain,
~ distinct_points(sK1,sK1),
inference(instantiation,[status(thm)],[25]) ).
cnf(l499,plain,
( ~ left_apart_point(X0_812,line_connecting(sK2,sK1))
| ~ distinct_points(X0_812,X0_500)
| left_apart_point(X0_500,line_connecting(sK2,sK1))
| left_convergent_lines(line_connecting(X0_812,X0_500),line_connecting(sK2,sK1)) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l611,plain,
~ left_convergent_lines(line_connecting(X0_812,X0_500),line_connecting(sK2,sK1)),
inference(instantiation,[status(thm)],[39]) ).
cnf(l801,plain,
~ left_apart_point(sK1,reverse_line(line_connecting(sK2,sK1))),
inference(instantiation,[status(thm)],[38]) ).
fof(oagco5,plain,
! [A,B] :
( distinct_points(A,B)
=> ( ~ apart_point_and_line(A,line_connecting(A,B))
& ~ apart_point_and_line(B,line_connecting(A,B)) ) ),
file('Axioms/GEO007+0.ax',oagco5) ).
cnf(45,plain,
( ~ apart_point_and_line(X0,line_connecting(X0,X1))
| ~ distinct_points(X0,X1) ),
inference(cnf,[status(esa)],[oagco5]) ).
cnf(l694,plain,
( ~ apart_point_and_line(sK2,line_connecting(sK2,sK1))
| ~ distinct_points(sK2,sK1) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l500,plain,
~ left_apart_point(X0_500,line_connecting(sK2,sK1)),
inference(instantiation,[status(thm)],[37]) ).
cnf(l812,plain,
~ left_apart_point(X0_812,reverse_line(line_connecting(sK2,sK1))),
inference(instantiation,[status(thm)],[38]) ).
cnf(l483,plain,
( ~ left_apart_point(sK2,line_connecting(sK1,sK2))
| ~ distinct_points(sK2,sK1)
| left_apart_point(sK1,line_connecting(sK1,sK2))
| left_convergent_lines(line_connecting(sK2,sK1),line_connecting(sK1,sK2)) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l602,plain,
( ~ distinct_points(sK1,sK2)
| distinct_points(sK1,sK1)
| distinct_points(sK2,sK1) ),
inference(instantiation,[status(thm)],[26]) ).
fof(apt_def,plain,
! [A,L] :
( apart_point_and_line(A,L)
<=> ( left_apart_point(A,L)
| left_apart_point(A,reverse_line(L)) ) ),
file('Axioms/GEO007+0.ax',apt_def) ).
cnf(1,plain,
( ~ left_apart_point(X0,X1)
| apart_point_and_line(X0,X1) ),
inference(cnf,[status(esa)],[apt_def]) ).
cnf(l710,plain,
( ~ left_apart_point(sK2,line_connecting(sK2,sK1))
| apart_point_and_line(sK2,line_connecting(sK2,sK1)) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l584,plain,
~ left_convergent_lines(line_connecting(sK2,sK1),line_connecting(sK1,sK2)),
inference(instantiation,[status(thm)],[39]) ).
cnf(l589,plain,
~ left_apart_point(sK1,line_connecting(sK1,sK2)),
inference(instantiation,[status(thm)],[37]) ).
fof(oag9,plain,
! [L,M] :
( ( unequally_directed_lines(L,M)
& unequally_directed_lines(L,reverse_line(M)) )
=> ( left_convergent_lines(L,M)
| left_convergent_lines(L,reverse_line(M)) ) ),
file('Axioms/GEO007+0.ax',oag9) ).
cnf(36,plain,
( ~ unequally_directed_lines(X0,X1)
| ~ unequally_directed_lines(X0,reverse_line(X1))
| left_convergent_lines(X0,X1)
| left_convergent_lines(X0,reverse_line(X1)) ),
inference(cnf,[status(esa)],[oag9]) ).
cnf(l18,plain,
( ~ unequally_directed_lines(line_connecting(sK1,sK2),line_connecting(X0_71,X0_71))
| ~ unequally_directed_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_71,X0_71)))
| left_convergent_lines(line_connecting(sK1,sK2),line_connecting(X0_71,X0_71))
| left_convergent_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_71,X0_71))) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l32,plain,
( ~ unequally_directed_lines(line_connecting(sK1,sK2),line_connecting(X0_71,X0_71))
| unequally_directed_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_71,X0_71)))
| unequally_directed_lines(line_connecting(X0_71,X0_71),reverse_line(line_connecting(X0_71,X0_71))) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l618,plain,
distinct_points(sK1,sK2),
inference(instantiation,[status(thm)],[58]) ).
cnf(l15,plain,
( ~ unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(X0_71,X0_71))
| ~ unequally_directed_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X0_71,X0_71)))
| left_convergent_lines(line_connecting(sK2,sK1),line_connecting(X0_71,X0_71))
| left_convergent_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X0_71,X0_71))) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l675,plain,
~ left_apart_point(sK1,line_connecting(sK1,sK2)),
inference(instantiation,[status(thm)],[37]) ).
cnf(l544,plain,
~ left_apart_point(sK1,reverse_line(line_connecting(sK1,sK2))),
inference(instantiation,[status(thm)],[38]) ).
cnf(l608,plain,
~ distinct_points(sK1,sK1),
inference(instantiation,[status(thm)],[25]) ).
cnf(l27,plain,
( ~ unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(X0_71,X0_71))
| unequally_directed_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X0_71,X0_71)))
| unequally_directed_lines(line_connecting(X0_71,X0_71),reverse_line(line_connecting(X0_71,X0_71))) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l40,plain,
~ left_convergent_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_71,X0_71))),
inference(instantiation,[status(thm)],[40]) ).
cnf(l17,plain,
~ left_convergent_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X0_71,X0_71))),
inference(instantiation,[status(thm)],[39]) ).
cnf(l84,plain,
~ unequally_directed_lines(line_connecting(X0_71,X0_71),reverse_line(line_connecting(X0_71,X0_71))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l95,plain,
~ unequally_directed_lines(line_connecting(X0_71,X0_71),reverse_line(line_connecting(X0_71,X0_71))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l29,plain,
( ~ left_convergent_lines(line_connecting(sK1,sK2),line_connecting(X0_71,X0_71))
| unequally_directed_lines(line_connecting(X0_71,X0_71),reverse_line(line_connecting(X0_71,X0_71)))
| left_convergent_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_71,X0_71))) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l89,plain,
~ unequally_directed_lines(line_connecting(X0_71,X0_71),reverse_line(line_connecting(X0_71,X0_71))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l91,plain,
~ left_convergent_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_71,X0_71))),
inference(instantiation,[status(thm)],[39]) ).
cnf(l31,plain,
( ~ left_convergent_lines(line_connecting(sK2,sK1),line_connecting(X0_71,X0_71))
| unequally_directed_lines(line_connecting(X0_71,X0_71),reverse_line(line_connecting(X0_71,X0_71)))
| left_convergent_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X0_71,X0_71))) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l71,plain,
~ unequally_directed_lines(line_connecting(X0_71,X0_71),reverse_line(line_connecting(X0_71,X0_71))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l37,plain,
~ left_convergent_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X0_71,X0_71))),
inference(instantiation,[status(thm)],[39]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l482,l510,l1,l506,l485,l522,l525,l698,l531,l487,l564,l488,l495,l556,l489,l572,l623,l490,l515,l501,l782,l793,l813,l543,l496,l497,l560,l491,l566,l728,l486,l539,l799,l800,l503,l702,l511,l794,l620,l542,l546,l626,l622,l811,l581,l499,l611,l801,l694,l500,l812,l483,l602,l710,l584,l589,l18,l32,l618,l15,l675,l544,l608,l27,l40,l17,l84,l95,l29,l89,l91,l31,l71,l37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO230+1 : TPTP v9.0.0. Bugfixed v6.4.0.
% 0.03/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Sun Jul 20 11:46:49 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.35 % launching worker at depth: 1
% 0.13/0.35 % launching worker at depth: 7
% 0.13/0.35 % launching worker at depth: 4
% 0.13/0.35 % launching worker at depth: 5
% 0.13/0.35 % launching worker at depth: 3
% 0.13/0.35 % launching worker at depth: 6
% 0.13/0.35 % launching worker at depth: 2
% 0.13/0.35 % launching worker at depth: 8
% 0.13/0.35 % launching worker at depth: 9
% 0.20/0.36 % launching worker at depth: 10
% 0.20/0.50 % launching worker at depth: 11
% 25.65/3.58 % SZS status Theorem for theBenchmark
% 25.65/3.58 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------