%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO251+3 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n017.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 : Tue May 5 04:20:08 PM UTC 2026
% Result : Theorem 0.29s 1.63s
% Output : CNFRefutation 0.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 37
% Syntax : Number of formulae : 152 ( 29 unt; 0 def)
% Number of atoms : 481 ( 0 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 536 ( 207 ~; 238 |; 58 &)
% ( 12 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-4 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 344 ( 17 sgn 181 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax6_cons_objs,axiom,
! [X4,X5] :
( ( unequally_directed_lines(X4,X5)
& unequally_directed_lines(X4,reverse_line(X5)) )
=> ( ~ apart_point_and_line(intersection_point(X4,X5),X4)
& ~ apart_point_and_line(intersection_point(X4,X5),X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax6_cons_objs) ).
fof(ax5_cons_objs,axiom,
! [X3,X6] :
( distinct_points(X3,X6)
=> ( ~ apart_point_and_line(X3,line_connecting(X3,X6))
& ~ apart_point_and_line(X6,line_connecting(X3,X6)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax5_cons_objs) ).
fof(ax7_cons_objs,axiom,
! [X3,X4] : ~ apart_point_and_line(X3,parallel_through_point(X4,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax7_cons_objs) ).
fof(con,conjecture,
! [X3,X6,X4] :
( right_apart_point(X6,parallel_through_point(X4,X3))
=> left_apart_point(X3,parallel_through_point(X4,X6)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',con) ).
fof(a4_defns,axiom,
! [X1,X2] :
( equally_directed_lines(X1,X2)
<=> ~ unequally_directed_lines(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a4_defns) ).
fof(a5_defns,axiom,
! [X1,X2] :
( equally_directed_opposite_lines(X1,X2)
<=> ~ unequally_directed_opposite_lines(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a5_defns) ).
fof(ax8_cons_objs,axiom,
! [X4] : ~ distinct_lines(X4,reverse_line(X4)),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax8_cons_objs) ).
fof(ax3_basics,axiom,
! [X4] : ~ distinct_lines(X4,X4),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax3_basics) ).
fof(ax1_basics,axiom,
! [X3] : ~ distinct_points(X3,X3),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax1_basics) ).
fof(a9_defns,axiom,
! [X4,X3,X6,X7] :
( between_on_line(X4,X3,X6,X7)
<=> ( ( before_on_line(X4,X3,X6)
& before_on_line(X4,X6,X7) )
| ( before_on_line(X4,X7,X6)
& before_on_line(X4,X6,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a9_defns) ).
fof(ax4_defns,axiom,
! [X4,X3,X6] :
( before_on_line(X4,X3,X6)
<=> ( distinct_points(X3,X6)
& incident_point_and_line(X3,X4)
& incident_point_and_line(X6,X4)
& equally_directed_lines(X4,line_connecting(X3,X6)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax4_defns) ).
fof(ax1_uniq_cons,axiom,
! [X3,X6,X4,X5] :
( ( distinct_points(X3,X6)
& distinct_lines(X4,X5) )
=> ( left_apart_point(X3,X4)
| left_apart_point(X6,X4)
| left_apart_point(X3,X5)
| left_apart_point(X6,X5)
| left_apart_point(X3,reverse_line(X4))
| left_apart_point(X6,reverse_line(X4))
| left_apart_point(X3,reverse_line(X5))
| left_apart_point(X6,reverse_line(X5)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax1_uniq_cons) ).
fof(ax9_cons_objs,axiom,
! [X3,X6] :
( distinct_points(X3,X6)
=> equally_directed_lines(line_connecting(X3,X6),reverse_line(line_connecting(X6,X3))) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax9_cons_objs) ).
fof(a8_defns,axiom,
! [X3,X6,X4] :
( divides_points(X4,X3,X6)
<=> ( ( left_apart_point(X3,X4)
& right_apart_point(X6,X4) )
| ( right_apart_point(X3,X4)
& left_apart_point(X6,X4) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a8_defns) ).
fof(ax2_uniq_cons,axiom,
! [X3,X6,X4] :
( ( distinct_points(X3,X6)
& left_apart_point(X3,X4) )
=> ( left_apart_point(X6,X4)
| left_convergent_lines(line_connecting(X3,X6),X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax2_uniq_cons) ).
fof(ax2_cons_objs,axiom,
! [X4,X5] :
( ( line(X4)
& line(X5)
& unequally_directed_lines(X4,X5)
& unequally_directed_lines(X4,reverse_line(X5)) )
=> point(intersection_point(X4,X5)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax2_cons_objs) ).
fof(ax7_basics,axiom,
! [X4,X5,X8] :
( ( unequally_directed_lines(X4,X5)
& unequally_directed_lines(X4,reverse_line(X5)) )
=> ( ( unequally_directed_lines(X4,X8)
& unequally_directed_lines(X4,reverse_line(X8)) )
| ( unequally_directed_lines(X5,X8)
& unequally_directed_lines(X5,reverse_line(X8)) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax7_basics) ).
fof(ax9_basics,axiom,
! [X4,X5] :
( ( unequally_directed_lines(X4,X5)
& unequally_directed_lines(X4,reverse_line(X5)) )
=> ( left_convergent_lines(X4,X5)
| left_convergent_lines(X4,reverse_line(X5)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax9_basics) ).
fof(ax2_subs,axiom,
! [X3,X4,X5] :
( ( left_apart_point(X3,X4)
& unequally_directed_lines(X4,X5) )
=> ( distinct_lines(X4,X5)
| left_apart_point(X3,reverse_line(X5)) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax2_subs) ).
fof(ax1_cons_objs,axiom,
! [X3,X6] :
( ( point(X3)
& point(X6)
& distinct_points(X3,X6) )
=> line(line_connecting(X3,X6)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax1_cons_objs) ).
fof(a7_defns,axiom,
! [X4,X5] :
( convergent_lines(X4,X5)
<=> ( unequally_directed_lines(X4,X5)
& unequally_directed_opposite_lines(X4,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a7_defns) ).
fof(ax4_basics,axiom,
! [X4,X5,X8] :
( distinct_lines(X4,X5)
=> ( distinct_lines(X4,X8)
| distinct_lines(X5,X8) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax4_basics) ).
fof(ax2_basics,axiom,
! [X3,X6,X7] :
( distinct_points(X3,X6)
=> ( distinct_points(X3,X7)
| distinct_points(X6,X7) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax2_basics) ).
fof(ax1_subs,axiom,
! [X3,X6,X4] :
( left_apart_point(X3,X4)
=> ( distinct_points(X3,X6)
| left_apart_point(X6,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax1_subs) ).
fof(a6_defns,axiom,
! [X3,X4] :
( apart_point_and_line(X3,X4)
<=> ( left_apart_point(X3,X4)
| right_apart_point(X3,X4) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a6_defns) ).
fof(ax3_subs,axiom,
! [X4,X5,X8] :
( left_convergent_lines(X4,X5)
=> ( unequally_directed_lines(X5,X8)
| left_convergent_lines(X4,X8) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax3_subs) ).
fof(ax6_basics,axiom,
! [X4,X5,X8] :
( unequally_directed_lines(X4,X5)
=> ( unequally_directed_lines(X4,X8)
| unequally_directed_lines(X5,X8) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax6_basics) ).
fof(a3_defns,axiom,
! [X1,X2] :
( right_convergent_lines(X1,X2)
<=> left_convergent_lines(X1,reverse_line(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a3_defns) ).
fof(a2_defns,axiom,
! [X1,X2] :
( right_apart_point(X1,X2)
<=> left_apart_point(X1,reverse_line(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a2_defns) ).
fof(a1_defns,axiom,
! [X1,X2] :
( unequally_directed_opposite_lines(X1,X2)
<=> unequally_directed_lines(X1,reverse_line(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',a1_defns) ).
fof(ax3_cons_objs,axiom,
! [X4,X3] :
( ( point(X3)
& line(X4) )
=> line(parallel_through_point(X4,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax3_cons_objs) ).
fof(ax10_cons_objs,axiom,
! [X3,X4] : equally_directed_lines(parallel_through_point(X4,X3),X4),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax10_cons_objs) ).
fof(ax8_basics,axiom,
! [X4,X5] :
( unequally_directed_lines(X4,X5)
| unequally_directed_lines(X4,reverse_line(X5)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax8_basics) ).
fof(ax11_basics,axiom,
! [X4,X5] :
~ ( left_convergent_lines(X4,X5)
| left_convergent_lines(X4,reverse_line(X5)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax11_basics) ).
fof(ax10_basics,axiom,
! [X3,X4] :
~ ( left_apart_point(X3,X4)
| left_apart_point(X3,reverse_line(X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax10_basics) ).
fof(ax4_cons_objs,axiom,
! [X4] :
( line(X4)
=> line(reverse_line(X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax4_cons_objs) ).
fof(ax5_basics,axiom,
! [X4] : equally_directed_lines(X4,X4),
file('/export/starexec/sandbox/benchmark/Axioms/GEO009+0.ax',ax5_basics) ).
fof(i_0_37,plain,
! [X4,X5] :
( ( unequally_directed_lines(X4,X5)
& unequally_directed_lines(X4,reverse_line(X5)) )
=> ( ~ apart_point_and_line(intersection_point(X4,X5),X4)
& ~ apart_point_and_line(intersection_point(X4,X5),X5) ) ),
inference(fof_simplification,[status(thm)],[ax6_cons_objs]) ).
fof(i_0_38,plain,
! [X3,X6] :
( distinct_points(X3,X6)
=> ( ~ apart_point_and_line(X3,line_connecting(X3,X6))
& ~ apart_point_and_line(X6,line_connecting(X3,X6)) ) ),
inference(fof_simplification,[status(thm)],[ax5_cons_objs]) ).
fof(i_0_39,plain,
! [X3,X4] : ~ apart_point_and_line(X3,parallel_through_point(X4,X3)),
inference(fof_simplification,[status(thm)],[ax7_cons_objs]) ).
fof(i_0_40,negated_conjecture,
~ ! [X3,X6,X4] :
( right_apart_point(X6,parallel_through_point(X4,X3))
=> left_apart_point(X3,parallel_through_point(X4,X6)) ),
inference(assume_negation,[status(cth)],[con]) ).
fof(i_0_41,plain,
! [X1,X2] :
( equally_directed_lines(X1,X2)
<=> ~ unequally_directed_lines(X1,X2) ),
inference(fof_simplification,[status(thm)],[a4_defns]) ).
fof(i_0_42,plain,
! [X1,X2] :
( equally_directed_opposite_lines(X1,X2)
<=> ~ unequally_directed_opposite_lines(X1,X2) ),
inference(fof_simplification,[status(thm)],[a5_defns]) ).
fof(i_0_43,plain,
! [X4] : ~ distinct_lines(X4,reverse_line(X4)),
inference(fof_simplification,[status(thm)],[ax8_cons_objs]) ).
fof(i_0_44,plain,
! [X4] : ~ distinct_lines(X4,X4),
inference(fof_simplification,[status(thm)],[ax3_basics]) ).
fof(i_0_45,plain,
! [X3] : ~ distinct_points(X3,X3),
inference(fof_simplification,[status(thm)],[ax1_basics]) ).
fof(i_0_46,plain,
! [X113,X114,X115,X116] :
( ( before_on_line(X113,X116,X115)
| before_on_line(X113,X114,X115)
| ~ between_on_line(X113,X114,X115,X116) )
& ( before_on_line(X113,X115,X114)
| before_on_line(X113,X114,X115)
| ~ between_on_line(X113,X114,X115,X116) )
& ( before_on_line(X113,X116,X115)
| before_on_line(X113,X115,X116)
| ~ between_on_line(X113,X114,X115,X116) )
& ( before_on_line(X113,X115,X114)
| before_on_line(X113,X115,X116)
| ~ between_on_line(X113,X114,X115,X116) )
& ( ~ before_on_line(X113,X114,X115)
| ~ before_on_line(X113,X115,X116)
| between_on_line(X113,X114,X115,X116) )
& ( ~ before_on_line(X113,X116,X115)
| ~ before_on_line(X113,X115,X114)
| between_on_line(X113,X114,X115,X116) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a9_defns])])]) ).
fof(i_0_47,plain,
! [X110,X111,X112] :
( ( distinct_points(X111,X112)
| ~ before_on_line(X110,X111,X112) )
& ( incident_point_and_line(X111,X110)
| ~ before_on_line(X110,X111,X112) )
& ( incident_point_and_line(X112,X110)
| ~ before_on_line(X110,X111,X112) )
& ( equally_directed_lines(X110,line_connecting(X111,X112))
| ~ before_on_line(X110,X111,X112) )
& ( ~ distinct_points(X111,X112)
| ~ incident_point_and_line(X111,X110)
| ~ incident_point_and_line(X112,X110)
| ~ equally_directed_lines(X110,line_connecting(X111,X112))
| before_on_line(X110,X111,X112) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax4_defns])])]) ).
fof(i_0_48,plain,
! [X158,X159,X160,X161] :
( ~ distinct_points(X158,X159)
| ~ distinct_lines(X160,X161)
| left_apart_point(X158,X160)
| left_apart_point(X159,X160)
| left_apart_point(X158,X161)
| left_apart_point(X159,X161)
| left_apart_point(X158,reverse_line(X160))
| left_apart_point(X159,reverse_line(X160))
| left_apart_point(X158,reverse_line(X161))
| left_apart_point(X159,reverse_line(X161)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax1_uniq_cons])]) ).
fof(i_0_49,plain,
! [X154,X155] :
( ~ distinct_points(X154,X155)
| equally_directed_lines(line_connecting(X154,X155),reverse_line(line_connecting(X155,X154))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax9_cons_objs])]) ).
fof(i_0_50,plain,
! [X149,X150] :
( ( ~ apart_point_and_line(intersection_point(X149,X150),X149)
| ~ unequally_directed_lines(X149,X150)
| ~ unequally_directed_lines(X149,reverse_line(X150)) )
& ( ~ apart_point_and_line(intersection_point(X149,X150),X150)
| ~ unequally_directed_lines(X149,X150)
| ~ unequally_directed_lines(X149,reverse_line(X150)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_37])])]) ).
fof(i_0_51,plain,
! [X107,X108,X109] :
( ( right_apart_point(X107,X109)
| left_apart_point(X107,X109)
| ~ divides_points(X109,X107,X108) )
& ( left_apart_point(X108,X109)
| left_apart_point(X107,X109)
| ~ divides_points(X109,X107,X108) )
& ( right_apart_point(X107,X109)
| right_apart_point(X108,X109)
| ~ divides_points(X109,X107,X108) )
& ( left_apart_point(X108,X109)
| right_apart_point(X108,X109)
| ~ divides_points(X109,X107,X108) )
& ( ~ left_apart_point(X107,X109)
| ~ right_apart_point(X108,X109)
| divides_points(X109,X107,X108) )
& ( ~ right_apart_point(X107,X109)
| ~ left_apart_point(X108,X109)
| divides_points(X109,X107,X108) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a8_defns])])]) ).
fof(i_0_52,plain,
! [X162,X163,X164] :
( ~ distinct_points(X162,X163)
| ~ left_apart_point(X162,X164)
| left_apart_point(X163,X164)
| left_convergent_lines(line_connecting(X162,X163),X164) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax2_uniq_cons])]) ).
fof(i_0_53,plain,
! [X142,X143] :
( ~ line(X142)
| ~ line(X143)
| ~ unequally_directed_lines(X142,X143)
| ~ unequally_directed_lines(X142,reverse_line(X143))
| point(intersection_point(X142,X143)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax2_cons_objs])]) ).
fof(i_0_54,plain,
! [X129,X130,X131] :
( ( unequally_directed_lines(X130,X131)
| unequally_directed_lines(X129,X131)
| ~ unequally_directed_lines(X129,X130)
| ~ unequally_directed_lines(X129,reverse_line(X130)) )
& ( unequally_directed_lines(X130,reverse_line(X131))
| unequally_directed_lines(X129,X131)
| ~ unequally_directed_lines(X129,X130)
| ~ unequally_directed_lines(X129,reverse_line(X130)) )
& ( unequally_directed_lines(X130,X131)
| unequally_directed_lines(X129,reverse_line(X131))
| ~ unequally_directed_lines(X129,X130)
| ~ unequally_directed_lines(X129,reverse_line(X130)) )
& ( unequally_directed_lines(X130,reverse_line(X131))
| unequally_directed_lines(X129,reverse_line(X131))
| ~ unequally_directed_lines(X129,X130)
| ~ unequally_directed_lines(X129,reverse_line(X130)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax7_basics])])]) ).
fof(i_0_55,plain,
! [X134,X135] :
( ~ unequally_directed_lines(X134,X135)
| ~ unequally_directed_lines(X134,reverse_line(X135))
| left_convergent_lines(X134,X135)
| left_convergent_lines(X134,reverse_line(X135)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax9_basics])]) ).
fof(i_0_56,plain,
! [X147,X148] :
( ( ~ apart_point_and_line(X147,line_connecting(X147,X148))
| ~ distinct_points(X147,X148) )
& ( ~ apart_point_and_line(X148,line_connecting(X147,X148))
| ~ distinct_points(X147,X148) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_38])])]) ).
fof(i_0_57,plain,
! [X168,X169,X170] :
( ~ left_apart_point(X168,X169)
| ~ unequally_directed_lines(X169,X170)
| distinct_lines(X169,X170)
| left_apart_point(X168,reverse_line(X170)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax2_subs])]) ).
fof(i_0_58,plain,
! [X140,X141] :
( ~ point(X140)
| ~ point(X141)
| ~ distinct_points(X140,X141)
| line(line_connecting(X140,X141)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax1_cons_objs])]) ).
fof(i_0_59,plain,
! [X151,X152] : ~ apart_point_and_line(X151,parallel_through_point(X152,X151)),
inference(variable_rename,[status(thm)],[i_0_39]) ).
fof(i_0_60,plain,
! [X105,X106] :
( ( unequally_directed_lines(X105,X106)
| ~ convergent_lines(X105,X106) )
& ( unequally_directed_opposite_lines(X105,X106)
| ~ convergent_lines(X105,X106) )
& ( ~ unequally_directed_lines(X105,X106)
| ~ unequally_directed_opposite_lines(X105,X106)
| convergent_lines(X105,X106) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a7_defns])])]) ).
fof(i_0_61,plain,
! [X122,X123,X124] :
( ~ distinct_lines(X122,X123)
| distinct_lines(X122,X124)
| distinct_lines(X123,X124) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax4_basics])]) ).
fof(i_0_62,plain,
! [X118,X119,X120] :
( ~ distinct_points(X118,X119)
| distinct_points(X118,X120)
| distinct_points(X119,X120) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax2_basics])]) ).
fof(i_0_63,plain,
! [X165,X166,X167] :
( ~ left_apart_point(X165,X167)
| distinct_points(X165,X166)
| left_apart_point(X166,X167) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax1_subs])]) ).
fof(i_0_64,plain,
! [X103,X104] :
( ( ~ apart_point_and_line(X103,X104)
| left_apart_point(X103,X104)
| right_apart_point(X103,X104) )
& ( ~ left_apart_point(X103,X104)
| apart_point_and_line(X103,X104) )
& ( ~ right_apart_point(X103,X104)
| apart_point_and_line(X103,X104) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a6_defns])])]) ).
fof(i_0_65,plain,
! [X171,X172,X173] :
( ~ left_convergent_lines(X171,X172)
| unequally_directed_lines(X172,X173)
| left_convergent_lines(X171,X173) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3_subs])]) ).
fof(i_0_66,plain,
! [X126,X127,X128] :
( ~ unequally_directed_lines(X126,X127)
| unequally_directed_lines(X126,X128)
| unequally_directed_lines(X127,X128) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax6_basics])]) ).
fof(i_0_67,negated_conjecture,
( right_apart_point(esk2_0,parallel_through_point(esk3_0,esk1_0))
& ~ left_apart_point(esk1_0,parallel_through_point(esk3_0,esk2_0)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_40])])]) ).
fof(i_0_68,plain,
! [X97,X98] :
( ( ~ right_convergent_lines(X97,X98)
| left_convergent_lines(X97,reverse_line(X98)) )
& ( ~ left_convergent_lines(X97,reverse_line(X98))
| right_convergent_lines(X97,X98) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a3_defns])]) ).
fof(i_0_69,plain,
! [X95,X96] :
( ( ~ right_apart_point(X95,X96)
| left_apart_point(X95,reverse_line(X96)) )
& ( ~ left_apart_point(X95,reverse_line(X96))
| right_apart_point(X95,X96) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a2_defns])]) ).
fof(i_0_70,plain,
! [X93,X94] :
( ( ~ unequally_directed_opposite_lines(X93,X94)
| unequally_directed_lines(X93,reverse_line(X94)) )
& ( ~ unequally_directed_lines(X93,reverse_line(X94))
| unequally_directed_opposite_lines(X93,X94) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[a1_defns])]) ).
fof(i_0_71,plain,
! [X99,X100] :
( ( ~ equally_directed_lines(X99,X100)
| ~ unequally_directed_lines(X99,X100) )
& ( unequally_directed_lines(X99,X100)
| equally_directed_lines(X99,X100) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_41])]) ).
fof(i_0_72,plain,
! [X101,X102] :
( ( ~ equally_directed_opposite_lines(X101,X102)
| ~ unequally_directed_opposite_lines(X101,X102) )
& ( unequally_directed_opposite_lines(X101,X102)
| equally_directed_opposite_lines(X101,X102) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_42])]) ).
fof(i_0_73,plain,
! [X144,X145] :
( ~ point(X145)
| ~ line(X144)
| line(parallel_through_point(X144,X145)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax3_cons_objs])]) ).
fof(i_0_74,plain,
! [X156,X157] : equally_directed_lines(parallel_through_point(X157,X156),X157),
inference(variable_rename,[status(thm)],[ax10_cons_objs]) ).
fof(i_0_75,plain,
! [X132,X133] :
( unequally_directed_lines(X132,X133)
| unequally_directed_lines(X132,reverse_line(X133)) ),
inference(variable_rename,[status(thm)],[ax8_basics]) ).
fof(i_0_76,plain,
! [X153] : ~ distinct_lines(X153,reverse_line(X153)),
inference(variable_rename,[status(thm)],[i_0_43]) ).
fof(i_0_77,plain,
! [X138,X139] :
( ~ left_convergent_lines(X138,X139)
& ~ left_convergent_lines(X138,reverse_line(X139)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax11_basics])]) ).
fof(i_0_78,plain,
! [X136,X137] :
( ~ left_apart_point(X136,X137)
& ~ left_apart_point(X136,reverse_line(X137)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax10_basics])]) ).
fof(i_0_79,plain,
! [X121] : ~ distinct_lines(X121,X121),
inference(variable_rename,[status(thm)],[i_0_44]) ).
fof(i_0_80,plain,
! [X117] : ~ distinct_points(X117,X117),
inference(variable_rename,[status(thm)],[i_0_45]) ).
fof(i_0_81,plain,
! [X146] :
( ~ line(X146)
| line(reverse_line(X146)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax4_cons_objs])]) ).
fof(i_0_82,plain,
! [X125] : equally_directed_lines(X125,X125),
inference(variable_rename,[status(thm)],[ax5_basics]) ).
cnf(i_0_83,plain,
( before_on_line(X1,X2,X3)
| before_on_line(X1,X2,X4)
| ~ between_on_line(X1,X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_84,plain,
( before_on_line(X1,X2,X3)
| before_on_line(X1,X3,X2)
| ~ between_on_line(X1,X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_85,plain,
( before_on_line(X1,X2,X3)
| before_on_line(X1,X3,X2)
| ~ between_on_line(X1,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_86,plain,
( before_on_line(X1,X2,X3)
| before_on_line(X1,X4,X3)
| ~ between_on_line(X1,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_87,plain,
( between_on_line(X1,X2,X3,X4)
| ~ before_on_line(X1,X2,X3)
| ~ before_on_line(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_88,plain,
( between_on_line(X1,X4,X3,X2)
| ~ before_on_line(X1,X2,X3)
| ~ before_on_line(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_46]),
[final] ).
cnf(i_0_89,plain,
( before_on_line(X3,X1,X2)
| ~ distinct_points(X1,X2)
| ~ incident_point_and_line(X1,X3)
| ~ incident_point_and_line(X2,X3)
| ~ equally_directed_lines(X3,line_connecting(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_90,plain,
( left_apart_point(X1,X3)
| left_apart_point(X2,X3)
| left_apart_point(X1,X4)
| left_apart_point(X2,X4)
| left_apart_point(X1,reverse_line(X3))
| left_apart_point(X2,reverse_line(X3))
| left_apart_point(X1,reverse_line(X4))
| left_apart_point(X2,reverse_line(X4))
| ~ distinct_points(X1,X2)
| ~ distinct_lines(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_91,plain,
( equally_directed_lines(X1,line_connecting(X2,X3))
| ~ before_on_line(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_92,plain,
( equally_directed_lines(line_connecting(X1,X2),reverse_line(line_connecting(X2,X1)))
| ~ distinct_points(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_93,plain,
( ~ apart_point_and_line(intersection_point(X1,X2),X1)
| ~ unequally_directed_lines(X1,X2)
| ~ unequally_directed_lines(X1,reverse_line(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_94,plain,
( ~ apart_point_and_line(intersection_point(X1,X2),X2)
| ~ unequally_directed_lines(X1,X2)
| ~ unequally_directed_lines(X1,reverse_line(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_95,plain,
( left_apart_point(X1,X2)
| left_apart_point(X3,X2)
| ~ divides_points(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_96,plain,
( right_apart_point(X1,X2)
| left_apart_point(X1,X2)
| ~ divides_points(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_97,plain,
( left_apart_point(X1,X2)
| right_apart_point(X1,X2)
| ~ divides_points(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_98,plain,
( right_apart_point(X1,X2)
| right_apart_point(X3,X2)
| ~ divides_points(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_99,plain,
( incident_point_and_line(X1,X2)
| ~ before_on_line(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_100,plain,
( incident_point_and_line(X1,X2)
| ~ before_on_line(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_101,plain,
( distinct_points(X1,X2)
| ~ before_on_line(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_102,plain,
( left_apart_point(X2,X3)
| left_convergent_lines(line_connecting(X1,X2),X3)
| ~ distinct_points(X1,X2)
| ~ left_apart_point(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_103,plain,
( divides_points(X2,X1,X3)
| ~ right_apart_point(X1,X2)
| ~ left_apart_point(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_104,plain,
( divides_points(X2,X1,X3)
| ~ left_apart_point(X1,X2)
| ~ right_apart_point(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_105,plain,
( point(intersection_point(X1,X2))
| ~ line(X1)
| ~ line(X2)
| ~ unequally_directed_lines(X1,X2)
| ~ unequally_directed_lines(X1,reverse_line(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_106,plain,
( unequally_directed_lines(X1,reverse_line(X2))
| unequally_directed_lines(X3,reverse_line(X2))
| ~ unequally_directed_lines(X3,X1)
| ~ unequally_directed_lines(X3,reverse_line(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_107,plain,
( left_convergent_lines(X1,X2)
| left_convergent_lines(X1,reverse_line(X2))
| ~ unequally_directed_lines(X1,X2)
| ~ unequally_directed_lines(X1,reverse_line(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_108,plain,
( unequally_directed_lines(X1,X2)
| unequally_directed_lines(X3,reverse_line(X2))
| ~ unequally_directed_lines(X3,X1)
| ~ unequally_directed_lines(X3,reverse_line(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_109,plain,
( unequally_directed_lines(X1,reverse_line(X2))
| unequally_directed_lines(X3,X2)
| ~ unequally_directed_lines(X3,X1)
| ~ unequally_directed_lines(X3,reverse_line(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_110,plain,
( ~ apart_point_and_line(X1,line_connecting(X1,X2))
| ~ distinct_points(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_111,plain,
( ~ apart_point_and_line(X1,line_connecting(X2,X1))
| ~ distinct_points(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_112,plain,
( unequally_directed_lines(X1,X2)
| unequally_directed_lines(X3,X2)
| ~ unequally_directed_lines(X3,X1)
| ~ unequally_directed_lines(X3,reverse_line(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_113,plain,
( distinct_lines(X2,X3)
| left_apart_point(X1,reverse_line(X3))
| ~ left_apart_point(X1,X2)
| ~ unequally_directed_lines(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_114,plain,
( line(line_connecting(X1,X2))
| ~ point(X1)
| ~ point(X2)
| ~ distinct_points(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_115,plain,
~ apart_point_and_line(X1,parallel_through_point(X2,X1)),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_116,plain,
( convergent_lines(X1,X2)
| ~ unequally_directed_lines(X1,X2)
| ~ unequally_directed_opposite_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_117,plain,
( distinct_lines(X1,X3)
| distinct_lines(X2,X3)
| ~ distinct_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_118,plain,
( distinct_points(X1,X3)
| distinct_points(X2,X3)
| ~ distinct_points(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_119,plain,
( distinct_points(X1,X3)
| left_apart_point(X3,X2)
| ~ left_apart_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_120,plain,
( left_apart_point(X1,X2)
| right_apart_point(X1,X2)
| ~ apart_point_and_line(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_121,plain,
( unequally_directed_lines(X2,X3)
| left_convergent_lines(X1,X3)
| ~ left_convergent_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_122,plain,
( unequally_directed_lines(X1,X3)
| unequally_directed_lines(X2,X3)
| ~ unequally_directed_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_123,negated_conjecture,
~ left_apart_point(esk1_0,parallel_through_point(esk3_0,esk2_0)),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_124,plain,
( right_convergent_lines(X1,X2)
| ~ left_convergent_lines(X1,reverse_line(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_125,plain,
( right_apart_point(X1,X2)
| ~ left_apart_point(X1,reverse_line(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_126,plain,
( unequally_directed_opposite_lines(X1,X2)
| ~ unequally_directed_lines(X1,reverse_line(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_127,plain,
( ~ equally_directed_lines(X1,X2)
| ~ unequally_directed_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_128,plain,
( ~ equally_directed_opposite_lines(X1,X2)
| ~ unequally_directed_opposite_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_129,plain,
( line(parallel_through_point(X2,X1))
| ~ point(X1)
| ~ line(X2) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_130,plain,
( left_convergent_lines(X1,reverse_line(X2))
| ~ right_convergent_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_131,plain,
( left_apart_point(X1,reverse_line(X2))
| ~ right_apart_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_132,plain,
( unequally_directed_lines(X1,reverse_line(X2))
| ~ unequally_directed_opposite_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_133,plain,
equally_directed_lines(parallel_through_point(X1,X2),X1),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_134,plain,
( apart_point_and_line(X1,X2)
| ~ left_apart_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_135,plain,
( apart_point_and_line(X1,X2)
| ~ right_apart_point(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_136,plain,
( unequally_directed_lines(X1,X2)
| ~ convergent_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_137,plain,
( unequally_directed_opposite_lines(X1,X2)
| ~ convergent_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_138,plain,
( unequally_directed_lines(X1,X2)
| unequally_directed_lines(X1,reverse_line(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_139,negated_conjecture,
right_apart_point(esk2_0,parallel_through_point(esk3_0,esk1_0)),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_140,plain,
~ distinct_lines(X1,reverse_line(X1)),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_141,plain,
~ left_convergent_lines(X1,reverse_line(X2)),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_142,plain,
~ left_apart_point(X1,reverse_line(X2)),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_143,plain,
( unequally_directed_lines(X1,X2)
| equally_directed_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_144,plain,
( unequally_directed_opposite_lines(X1,X2)
| equally_directed_opposite_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_145,plain,
~ distinct_lines(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_146,plain,
~ distinct_points(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_147,plain,
~ left_convergent_lines(X1,X2),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_148,plain,
~ left_apart_point(X1,X2),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_149,plain,
( line(reverse_line(X1))
| ~ line(X1) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_150,plain,
equally_directed_lines(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_151,plain,
$false,
inference(scs_inference,[],[i_0_148,i_0_139,i_0_131]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO251+3 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.18/0.34 % Computer : n017.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Mon May 4 17:49:27 EDT 2026
% 0.18/0.34 % CPUTime :
% 0.18/0.35 % start to proof: theBenchmark
% 0.29/1.63 % Version : CSE_E---1.7
% 0.29/1.63 % Problem : theBenchmark.p
% 0.29/1.63 % SZS status Theorem for theBenchmark.p
% 0.29/1.63 % SZS output start CNFRefutation
% See solution above
% 0.29/1.64 % Total time : 1.274s
%------------------------------------------------------------------------------