%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GEO254+1 : TPTP v9.0.0. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n031.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:46 PM UTC 2025
% Result : Theorem 89.41s 11.59s
% Output : CNFRefutation 89.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 15
% Syntax : Number of formulae : 87 ( 44 unt; 0 def)
% Number of atoms : 194 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 197 ( 90 ~; 86 |; 11 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 110 ( 14 sgn 38 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(con,plain,
! [A,B,L] :
( ( distinct_points(A,B)
& ~ apart_point_and_line(A,L)
& ~ apart_point_and_line(B,L) )
=> ( before_on_line(L,A,B)
& before_on_line(L,B,A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con) ).
fof(con_negated,plain,
~ ! [A,B,L] :
( ( distinct_points(A,B)
& ~ apart_point_and_line(A,L)
& ~ apart_point_and_line(B,L) )
=> ( before_on_line(L,A,B)
& before_on_line(L,B,A) ) ),
inference(negate_conjecture,[status(cth)],[con]) ).
cnf(61,plain,
( ~ before_on_line(sK3,sK1,sK2)
| ~ before_on_line(sK3,sK2,sK1) ),
inference(cnf,[status(esa)],[con_negated]) ).
cnf(l0,plain,
( ~ before_on_line(sK3,sK1,sK2)
| ~ before_on_line(sK3,sK2,sK1) ),
inference(instantiation,[status(thm)],[61]) ).
fof(bf_def,plain,
! [L,A,B] :
( before_on_line(L,A,B)
<=> ( distinct_points(A,B)
& ~ ( left_apart_point(A,L)
| left_apart_point(A,reverse_line(L)) )
& ~ ( left_apart_point(B,L)
| left_apart_point(B,reverse_line(L)) )
& ~ unequally_directed_lines(L,line_connecting(A,B)) ) ),
file('Axioms/GEO007+0.ax',bf_def) ).
cnf(18,plain,
( ~ distinct_points(X0,X1)
| before_on_line(X2,X0,X1)
| left_apart_point(X0,X2)
| left_apart_point(X0,reverse_line(X2))
| left_apart_point(X1,X2)
| left_apart_point(X1,reverse_line(X2))
| unequally_directed_lines(X2,line_connecting(X0,X1)) ),
inference(cnf,[status(esa)],[bf_def]) ).
cnf(l2490,plain,
( ~ distinct_points(sK2,sK1)
| before_on_line(sK3,sK2,sK1)
| left_apart_point(sK2,sK3)
| left_apart_point(sK2,reverse_line(sK3))
| left_apart_point(sK1,sK3)
| left_apart_point(sK1,reverse_line(sK3))
| unequally_directed_lines(sK3,line_connecting(sK2,sK1)) ),
inference(instantiation,[status(thm)],[18]) ).
fof(oag10,plain,
! [A,L] :
~ ( left_apart_point(A,L)
| left_apart_point(A,reverse_line(L)) ),
file('Axioms/GEO007+0.ax',oag10) ).
cnf(38,plain,
~ left_apart_point(X0,reverse_line(X1)),
inference(cnf,[status(esa)],[oag10]) ).
cnf(l2586,plain,
~ left_apart_point(sK1,reverse_line(sK3)),
inference(instantiation,[status(thm)],[38]) ).
cnf(l1,plain,
( ~ distinct_points(sK1,sK2)
| before_on_line(sK3,sK1,sK2)
| left_apart_point(sK1,sK3)
| left_apart_point(sK1,reverse_line(sK3))
| left_apart_point(sK2,sK3)
| left_apart_point(sK2,reverse_line(sK3))
| unequally_directed_lines(sK3,line_connecting(sK1,sK2)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(37,plain,
~ left_apart_point(X0,X1),
inference(cnf,[status(esa)],[oag10]) ).
cnf(l90,plain,
~ left_apart_point(sK2,reverse_line(sK3)),
inference(instantiation,[status(thm)],[37]) ).
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(l2588,plain,
( ~ unequally_directed_lines(sK3,line_connecting(sK2,sK1))
| unequally_directed_lines(sK3,line_connecting(X1_3029,X1_3029))
| unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(X1_3029,X1_3029)) ),
inference(instantiation,[status(thm)],[30]) ).
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(l2593,plain,
( ~ unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(X1_3029,X1_3029))
| ~ unequally_directed_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X1_3029,X1_3029)))
| left_convergent_lines(line_connecting(sK2,sK1),line_connecting(X1_3029,X1_3029))
| left_convergent_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X1_3029,X1_3029))) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(58,plain,
distinct_points(sK1,sK2),
inference(cnf,[status(esa)],[con_negated]) ).
cnf(l2,plain,
distinct_points(sK1,sK2),
inference(instantiation,[status(thm)],[58]) ).
cnf(l78,plain,
~ left_apart_point(sK1,reverse_line(sK3)),
inference(instantiation,[status(thm)],[38]) ).
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(l79,plain,
( ~ left_apart_point(sK1,sK3)
| apart_point_and_line(sK1,sK3) ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2491,plain,
~ left_apart_point(sK2,sK3),
inference(instantiation,[status(thm)],[37]) ).
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(l2494,plain,
( ~ distinct_points(sK1,sK2)
| distinct_points(sK1,sK1)
| distinct_points(sK2,sK1) ),
inference(instantiation,[status(thm)],[26]) ).
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(l2633,plain,
~ left_convergent_lines(line_connecting(sK2,sK1),line_connecting(X1_3029,X1_3029)),
inference(instantiation,[status(thm)],[39]) ).
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(l2497,plain,
~ distinct_points(sK1,sK1),
inference(instantiation,[status(thm)],[25]) ).
cnf(l3132,plain,
~ left_convergent_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X1_3029,X1_3029))),
inference(instantiation,[status(thm)],[39]) ).
cnf(l68,plain,
( ~ unequally_directed_lines(sK3,line_connecting(sK1,sK2))
| unequally_directed_lines(sK3,line_connecting(X0_171,X0_171))
| unequally_directed_lines(line_connecting(sK1,sK2),line_connecting(X0_171,X0_171)) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2635,plain,
( ~ unequally_directed_lines(line_connecting(sK2,sK1),line_connecting(X1_3029,X1_3029))
| unequally_directed_lines(line_connecting(sK2,sK1),reverse_line(line_connecting(X1_3029,X1_3029)))
| unequally_directed_lines(line_connecting(X1_3029,X1_3029),reverse_line(line_connecting(X1_3029,X1_3029))) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2584,plain,
~ left_apart_point(sK1,sK3),
inference(instantiation,[status(thm)],[37]) ).
cnf(l69,plain,
( ~ unequally_directed_lines(line_connecting(sK1,sK2),line_connecting(X0_171,X0_171))
| ~ unequally_directed_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_171,X0_171)))
| left_convergent_lines(line_connecting(sK1,sK2),line_connecting(X0_171,X0_171))
| left_convergent_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_171,X0_171))) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l2500,plain,
distinct_points(sK1,sK2),
inference(instantiation,[status(thm)],[58]) ).
cnf(2,plain,
( ~ left_apart_point(X0,reverse_line(X1))
| apart_point_and_line(X0,X1) ),
inference(cnf,[status(esa)],[apt_def]) ).
cnf(l2585,plain,
( ~ left_apart_point(sK2,reverse_line(sK3))
| apart_point_and_line(sK2,sK3) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(40,plain,
~ left_convergent_lines(X0,reverse_line(X1)),
inference(cnf,[status(esa)],[oag11]) ).
cnf(l1417,plain,
~ left_convergent_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_171,X0_171))),
inference(instantiation,[status(thm)],[40]) ).
cnf(59,plain,
~ apart_point_and_line(sK1,sK3),
inference(cnf,[status(esa)],[con_negated]) ).
cnf(l80,plain,
~ apart_point_and_line(sK1,sK3),
inference(instantiation,[status(thm)],[59]) ).
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(l2646,plain,
~ unequally_directed_lines(line_connecting(X1_3029,X1_3029),reverse_line(line_connecting(X1_3029,X1_3029))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l2589,plain,
( ~ unequally_directed_lines(sK3,line_connecting(X1_3029,X1_3029))
| ~ unequally_directed_lines(sK3,reverse_line(line_connecting(X1_3029,X1_3029)))
| left_convergent_lines(sK3,line_connecting(X1_3029,X1_3029))
| left_convergent_lines(sK3,reverse_line(line_connecting(X1_3029,X1_3029))) ),
inference(instantiation,[status(thm)],[36]) ).
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(l2713,plain,
( ~ left_convergent_lines(sK3,line_connecting(X1_3029,X1_3029))
| unequally_directed_lines(line_connecting(X1_3029,X1_3029),reverse_line(line_connecting(X1_3029,X1_3029)))
| left_convergent_lines(sK3,reverse_line(line_connecting(X1_3029,X1_3029))) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(60,plain,
~ apart_point_and_line(sK2,sK3),
inference(cnf,[status(esa)],[con_negated]) ).
cnf(l2622,plain,
~ apart_point_and_line(sK2,sK3),
inference(instantiation,[status(thm)],[60]) ).
cnf(l2762,plain,
( ~ unequally_directed_lines(sK3,line_connecting(X1_3029,X1_3029))
| unequally_directed_lines(sK3,reverse_line(line_connecting(X1_3029,X1_3029)))
| unequally_directed_lines(line_connecting(X1_3029,X1_3029),reverse_line(line_connecting(X1_3029,X1_3029))) ),
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(l85,plain,
( ~ left_apart_point(sK2,sK3)
| ~ distinct_points(sK2,X0_634)
| left_apart_point(X0_634,sK3)
| left_convergent_lines(line_connecting(sK2,X0_634),sK3) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l2728,plain,
~ unequally_directed_lines(line_connecting(X1_3029,X1_3029),reverse_line(line_connecting(X1_3029,X1_3029))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l71,plain,
( ~ unequally_directed_lines(line_connecting(sK1,sK2),line_connecting(X0_171,X0_171))
| unequally_directed_lines(line_connecting(sK1,sK2),reverse_line(line_connecting(X0_171,X0_171)))
| unequally_directed_lines(line_connecting(X0_171,X0_171),reverse_line(line_connecting(X0_171,X0_171))) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l70,plain,
~ left_convergent_lines(line_connecting(sK1,sK2),line_connecting(X0_171,X0_171)),
inference(instantiation,[status(thm)],[39]) ).
cnf(l128,plain,
~ left_apart_point(X0_634,sK3),
inference(instantiation,[status(thm)],[37]) ).
cnf(l88,plain,
~ unequally_directed_lines(line_connecting(X0_171,X0_171),reverse_line(line_connecting(X0_171,X0_171))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l481,plain,
( ~ left_convergent_lines(line_connecting(sK2,X0_634),sK3)
| unequally_directed_lines(sK3,parallel_through_point(sK3,X1_2105))
| left_convergent_lines(line_connecting(sK2,X0_634),parallel_through_point(sK3,X1_2105)) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l642,plain,
( ~ unequally_directed_lines(sK3,parallel_through_point(sK3,X1_2105))
| unequally_directed_lines(sK3,sK3)
| unequally_directed_lines(parallel_through_point(sK3,X1_2105),sK3) ),
inference(instantiation,[status(thm)],[30]) ).
fof(oagco10,plain,
! [A,L] : ~ unequally_directed_lines(parallel_through_point(L,A),L),
file('Axioms/GEO007+0.ax',oagco10) ).
cnf(52,plain,
~ unequally_directed_lines(parallel_through_point(X0,X1),X0),
inference(cnf,[status(esa)],[oagco10]) ).
cnf(l2105,plain,
~ unequally_directed_lines(parallel_through_point(sK3,X1_2105),sK3),
inference(instantiation,[status(thm)],[52]) ).
cnf(l598,plain,
~ left_convergent_lines(line_connecting(sK2,X0_634),parallel_through_point(sK3,X1_2105)),
inference(instantiation,[status(thm)],[39]) ).
cnf(l2950,plain,
~ left_convergent_lines(sK3,reverse_line(line_connecting(X1_3029,X1_3029))),
inference(instantiation,[status(thm)],[39]) ).
fof(oag5,plain,
! [L] : ~ unequally_directed_lines(L,L),
file('Axioms/GEO007+0.ax',oag5) ).
cnf(29,plain,
~ unequally_directed_lines(X0,X0),
inference(cnf,[status(esa)],[oag5]) ).
cnf(l2106,plain,
~ unequally_directed_lines(sK3,sK3),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3029,plain,
~ unequally_directed_lines(line_connecting(X1_3029,X1_3029),reverse_line(line_connecting(X1_3029,X1_3029))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l2734,plain,
~ left_convergent_lines(sK3,reverse_line(line_connecting(X1_3029,X1_3029))),
inference(instantiation,[status(thm)],[40]) ).
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(l134,plain,
( ~ left_apart_point(sK2,sK3)
| left_apart_point(X0_634,sK3)
| distinct_points(sK2,X0_634) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l75,plain,
( ~ unequally_directed_lines(sK3,line_connecting(X0_171,X0_171))
| unequally_directed_lines(sK3,reverse_line(line_connecting(X0_171,X0_171)))
| unequally_directed_lines(line_connecting(X0_171,X0_171),reverse_line(line_connecting(X0_171,X0_171))) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l634,plain,
~ left_apart_point(X0_634,sK3),
inference(instantiation,[status(thm)],[37]) ).
cnf(l171,plain,
~ unequally_directed_lines(line_connecting(X0_171,X0_171),reverse_line(line_connecting(X0_171,X0_171))),
inference(instantiation,[status(thm)],[51]) ).
cnf(l83,plain,
( ~ unequally_directed_lines(sK3,line_connecting(X0_171,X0_171))
| ~ unequally_directed_lines(sK3,reverse_line(line_connecting(X0_171,X0_171)))
| left_convergent_lines(sK3,line_connecting(X0_171,X0_171))
| left_convergent_lines(sK3,reverse_line(line_connecting(X0_171,X0_171))) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l84,plain,
~ left_convergent_lines(sK3,line_connecting(X0_171,X0_171)),
inference(instantiation,[status(thm)],[39]) ).
cnf(l154,plain,
~ left_convergent_lines(sK3,reverse_line(line_connecting(X0_171,X0_171))),
inference(instantiation,[status(thm)],[40]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l2490,l2586,l1,l90,l2588,l2593,l2,l78,l79,l2491,l2494,l2633,l2497,l3132,l68,l2635,l2584,l69,l2500,l2585,l1417,l80,l2646,l2589,l2713,l2622,l2762,l85,l2728,l71,l70,l128,l88,l481,l642,l2105,l598,l2950,l2106,l3029,l2734,l134,l75,l634,l171,l83,l84,l154]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : GEO254+1 : TPTP v9.0.0. Bugfixed v6.4.0.
% 0.07/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n031.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 11:51:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.33 % launching worker at depth: 1
% 0.12/0.33 % launching worker at depth: 3
% 0.12/0.33 % launching worker at depth: 2
% 0.12/0.33 % launching worker at depth: 7
% 0.12/0.33 % launching worker at depth: 4
% 0.12/0.33 % launching worker at depth: 5
% 0.12/0.33 % launching worker at depth: 6
% 0.12/0.33 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.18/0.40 % launching worker at depth: 11
% 4.22/0.91 % launching worker at depth: 12
% 89.41/11.59 % SZS status Theorem for theBenchmark
% 89.41/11.59 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------