%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO253+1 : TPTP v9.2.1. Bugfixed v6.4.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 : n018.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.62s
% Output : CNFRefutation 0.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO253+1 : TPTP v9.2.1. Bugfixed v6.4.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.16/0.33 % Computer : n018.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 17:50:47 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.29/1.62 % Version : CSE_E---1.7
% 0.29/1.62 % Problem : theBenchmark.p
% 0.29/1.62 % SZS status Theorem for theBenchmark.p
% 0.29/1.62 % SZS output start CNFRefutation
% 0.29/1.62 fof(bf_def, axiom, ![X2, X1, X4]:(before_on_line(X2,X1,X4)<=>(((distinct_points(X1,X4)&~((left_apart_point(X1,X2)|left_apart_point(X1,reverse_line(X2)))))&~((left_apart_point(X4,X2)|left_apart_point(X4,reverse_line(X2)))))&~(unequally_directed_lines(X2,line_connecting(X1,X4))))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', bf_def)).
% 0.29/1.62 fof(oagco9, axiom, ![X1, X4]:~(unequally_directed_lines(line_connecting(X1,X4),reverse_line(line_connecting(X4,X1)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco9)).
% 0.29/1.62 fof(oagco6, axiom, ![X2, X3]:((unequally_directed_lines(X2,X3)&unequally_directed_lines(X2,reverse_line(X3)))=>(~(apart_point_and_line(intersection_point(X2,X3),X2))&~(apart_point_and_line(intersection_point(X2,X3),X3)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco6)).
% 0.29/1.62 fof(oagco5, axiom, ![X1, X4]:(distinct_points(X1,X4)=>(~(apart_point_and_line(X1,line_connecting(X1,X4)))&~(apart_point_and_line(X4,line_connecting(X1,X4))))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco5)).
% 0.29/1.62 fof(oagco10, axiom, ![X1, X2]:~(unequally_directed_lines(parallel_through_point(X2,X1),X2)), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco10)).
% 0.29/1.62 fof(oagco7, axiom, ![X1, X2]:~(apart_point_and_line(X1,parallel_through_point(X2,X1))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco7)).
% 0.29/1.62 fof(con, conjecture, ![X1, X4, X2]:((apart_point_and_line(X1,X2)&~(apart_point_and_line(X4,parallel_through_point(X2,X1))))=>apart_point_and_line(X4,X2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 0.29/1.62 fof(oagco8, axiom, ![X2]:~(distinct_lines(X2,reverse_line(X2))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco8)).
% 0.29/1.62 fof(oag3, axiom, ![X2]:~(distinct_lines(X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag3)).
% 0.29/1.62 fof(oag1, axiom, ![X1]:~(distinct_points(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag1)).
% 0.29/1.62 fof(oag5, axiom, ![X2]:~(unequally_directed_lines(X2,X2)), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag5)).
% 0.29/1.62 fof(bet_def, axiom, ![X2, X1, X4, X5]:(between_on_line(X2,X1,X4,X5)<=>((before_on_line(X2,X1,X4)&before_on_line(X2,X4,X5))|(before_on_line(X2,X5,X4)&before_on_line(X2,X4,X1)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', bet_def)).
% 0.29/1.62 fof(oaguc1, axiom, ![X1, X4, X2, X3]:((distinct_points(X1,X4)&distinct_lines(X2,X3))=>(left_apart_point(X1,X2)|left_apart_point(X4,X2)|left_apart_point(X1,X3)|left_apart_point(X4,X3)|left_apart_point(X1,reverse_line(X2))|left_apart_point(X4,reverse_line(X2))|left_apart_point(X1,reverse_line(X3))|left_apart_point(X4,reverse_line(X3)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oaguc1)).
% 0.29/1.62 fof(div_def, axiom, ![X1, X4, X2]:(divides_points(X2,X1,X4)<=>((left_apart_point(X1,X2)&left_apart_point(X4,reverse_line(X2)))|(left_apart_point(X1,reverse_line(X2))&left_apart_point(X4,X2)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', div_def)).
% 0.29/1.62 fof(oaguc2, axiom, ![X1, X4, X2]:((distinct_points(X1,X4)&left_apart_point(X1,X2))=>(left_apart_point(X4,X2)|left_convergent_lines(line_connecting(X1,X4),X2))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oaguc2)).
% 0.29/1.62 fof(oagco2, axiom, ![X2, X3]:((((line(X2)&line(X3))&unequally_directed_lines(X2,X3))&unequally_directed_lines(X2,reverse_line(X3)))=>point(intersection_point(X2,X3))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco2)).
% 0.29/1.62 fof(oag7, axiom, ![X2, X3, X6]:((unequally_directed_lines(X2,X3)&unequally_directed_lines(X2,reverse_line(X3)))=>((unequally_directed_lines(X2,X6)&unequally_directed_lines(X2,reverse_line(X6)))|(unequally_directed_lines(X3,X6)&unequally_directed_lines(X3,reverse_line(X6))))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag7)).
% 0.29/1.62 fof(oag9, axiom, ![X2, X3]:((unequally_directed_lines(X2,X3)&unequally_directed_lines(X2,reverse_line(X3)))=>(left_convergent_lines(X2,X3)|left_convergent_lines(X2,reverse_line(X3)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag9)).
% 0.29/1.62 fof(oagsub2, axiom, ![X1, X2, X3]:((left_apart_point(X1,X2)&unequally_directed_lines(X2,X3))=>(distinct_lines(X2,X3)|left_apart_point(X1,reverse_line(X3)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagsub2)).
% 0.29/1.62 fof(con_def, axiom, ![X2, X3]:(convergent_lines(X2,X3)<=>(unequally_directed_lines(X2,X3)&unequally_directed_lines(X2,reverse_line(X3)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', con_def)).
% 0.29/1.62 fof(oagco1, axiom, ![X1, X4]:(((point(X1)&point(X4))&distinct_points(X1,X4))=>line(line_connecting(X1,X4))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco1)).
% 0.29/1.62 fof(apt_def, axiom, ![X1, X2]:(apart_point_and_line(X1,X2)<=>(left_apart_point(X1,X2)|left_apart_point(X1,reverse_line(X2)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', apt_def)).
% 0.29/1.62 fof(oag4, axiom, ![X2, X3, X6]:(distinct_lines(X2,X3)=>(distinct_lines(X2,X6)|distinct_lines(X3,X6))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag4)).
% 0.29/1.62 fof(oag2, axiom, ![X1, X4, X5]:(distinct_points(X1,X4)=>(distinct_points(X1,X5)|distinct_points(X4,X5))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag2)).
% 0.29/1.62 fof(oagsub3, axiom, ![X2, X3, X6]:(left_convergent_lines(X2,X3)=>(unequally_directed_lines(X3,X6)|left_convergent_lines(X2,X6))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagsub3)).
% 0.29/1.62 fof(oag6, axiom, ![X2, X3, X6]:(unequally_directed_lines(X2,X3)=>(unequally_directed_lines(X2,X6)|unequally_directed_lines(X3,X6))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag6)).
% 0.29/1.62 fof(oagsub1, axiom, ![X1, X4, X2]:(left_apart_point(X1,X2)=>(distinct_points(X1,X4)|left_apart_point(X4,X2))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagsub1)).
% 0.29/1.62 fof(oag8, axiom, ![X2, X3]:((line(X2)&line(X3))=>(unequally_directed_lines(X2,X3)|unequally_directed_lines(X2,reverse_line(X3)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag8)).
% 0.29/1.62 fof(oagco3, axiom, ![X2, X1]:((point(X1)&line(X2))=>line(parallel_through_point(X2,X1))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco3)).
% 0.29/1.62 fof(oag11, axiom, ![X2, X3]:~((left_convergent_lines(X2,X3)|left_convergent_lines(X2,reverse_line(X3)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag11)).
% 0.29/1.62 fof(oag10, axiom, ![X1, X2]:~((left_apart_point(X1,X2)|left_apart_point(X1,reverse_line(X2)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oag10)).
% 0.29/1.62 fof(oagco4, axiom, ![X2]:(line(X2)=>line(reverse_line(X2))), file('/export/starexec/sandbox/benchmark/Axioms/GEO007+0.ax', oagco4)).
% 0.29/1.62 fof(i_0_32, plain, ![X2, X1, X4]:(before_on_line(X2,X1,X4)<=>(((distinct_points(X1,X4)&~((left_apart_point(X1,X2)|left_apart_point(X1,reverse_line(X2)))))&~((left_apart_point(X4,X2)|left_apart_point(X4,reverse_line(X2)))))&~unequally_directed_lines(X2,line_connecting(X1,X4)))), inference(fof_simplification,[status(thm)],[bf_def])).
% 0.29/1.62 fof(i_0_33, plain, ![X1, X4]:~unequally_directed_lines(line_connecting(X1,X4),reverse_line(line_connecting(X4,X1))), inference(fof_simplification,[status(thm)],[oagco9])).
% 0.29/1.62 fof(i_0_34, plain, ![X2, X3]:((unequally_directed_lines(X2,X3)&unequally_directed_lines(X2,reverse_line(X3)))=>(~apart_point_and_line(intersection_point(X2,X3),X2)&~apart_point_and_line(intersection_point(X2,X3),X3))), inference(fof_simplification,[status(thm)],[oagco6])).
% 0.29/1.62 fof(i_0_35, plain, ![X1, X4]:(distinct_points(X1,X4)=>(~apart_point_and_line(X1,line_connecting(X1,X4))&~apart_point_and_line(X4,line_connecting(X1,X4)))), inference(fof_simplification,[status(thm)],[oagco5])).
% 0.29/1.62 fof(i_0_36, plain, ![X1, X2]:~unequally_directed_lines(parallel_through_point(X2,X1),X2), inference(fof_simplification,[status(thm)],[oagco10])).
% 0.29/1.62 fof(i_0_37, plain, ![X1, X2]:~apart_point_and_line(X1,parallel_through_point(X2,X1)), inference(fof_simplification,[status(thm)],[oagco7])).
% 0.29/1.62 fof(i_0_38, negated_conjecture, ~(![X1, X4, X2]:((apart_point_and_line(X1,X2)&~apart_point_and_line(X4,parallel_through_point(X2,X1)))=>apart_point_and_line(X4,X2))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[con])])).
% 0.29/1.62 fof(i_0_39, plain, ![X2]:~distinct_lines(X2,reverse_line(X2)), inference(fof_simplification,[status(thm)],[oagco8])).
% 0.29/1.62 fof(i_0_40, plain, ![X2]:~distinct_lines(X2,X2), inference(fof_simplification,[status(thm)],[oag3])).
% 0.29/1.62 fof(i_0_41, plain, ![X1]:~distinct_points(X1,X1), inference(fof_simplification,[status(thm)],[oag1])).
% 0.29/1.62 fof(i_0_42, plain, ![X2]:~unequally_directed_lines(X2,X2), inference(fof_simplification,[status(thm)],[oag5])).
% 0.29/1.62 fof(i_0_43, plain, ![X91, X92, X93, X94]:((((before_on_line(X91,X94,X93)|before_on_line(X91,X92,X93)|~between_on_line(X91,X92,X93,X94))&(before_on_line(X91,X93,X92)|before_on_line(X91,X92,X93)|~between_on_line(X91,X92,X93,X94)))&((before_on_line(X91,X94,X93)|before_on_line(X91,X93,X94)|~between_on_line(X91,X92,X93,X94))&(before_on_line(X91,X93,X92)|before_on_line(X91,X93,X94)|~between_on_line(X91,X92,X93,X94))))&((~before_on_line(X91,X92,X93)|~before_on_line(X91,X93,X94)|between_on_line(X91,X92,X93,X94))&(~before_on_line(X91,X94,X93)|~before_on_line(X91,X93,X92)|between_on_line(X91,X92,X93,X94)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[bet_def])])])).
% 0.29/1.62 fof(i_0_44, plain, ![X88, X89, X90]:(((((distinct_points(X89,X90)|~before_on_line(X88,X89,X90))&((~left_apart_point(X89,X88)|~before_on_line(X88,X89,X90))&(~left_apart_point(X89,reverse_line(X88))|~before_on_line(X88,X89,X90))))&((~left_apart_point(X90,X88)|~before_on_line(X88,X89,X90))&(~left_apart_point(X90,reverse_line(X88))|~before_on_line(X88,X89,X90))))&(~unequally_directed_lines(X88,line_connecting(X89,X90))|~before_on_line(X88,X89,X90)))&(~distinct_points(X89,X90)|(left_apart_point(X89,X88)|left_apart_point(X89,reverse_line(X88)))|(left_apart_point(X90,X88)|left_apart_point(X90,reverse_line(X88)))|unequally_directed_lines(X88,line_connecting(X89,X90))|before_on_line(X88,X89,X90))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_32])])])).
% 0.29/1.62 fof(i_0_45, plain, ![X136, X137, X138, X139]:(~distinct_points(X136,X137)|~distinct_lines(X138,X139)|(left_apart_point(X136,X138)|left_apart_point(X137,X138)|left_apart_point(X136,X139)|left_apart_point(X137,X139)|left_apart_point(X136,reverse_line(X138))|left_apart_point(X137,reverse_line(X138))|left_apart_point(X136,reverse_line(X139))|left_apart_point(X137,reverse_line(X139)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oaguc1])])).
% 0.29/1.62 fof(i_0_46, plain, ![X132, X133]:~unequally_directed_lines(line_connecting(X132,X133),reverse_line(line_connecting(X133,X132))), inference(variable_rename,[status(thm)],[i_0_33])).
% 0.29/1.62 fof(i_0_47, plain, ![X85, X86, X87]:((((left_apart_point(X85,reverse_line(X87))|left_apart_point(X85,X87)|~divides_points(X87,X85,X86))&(left_apart_point(X86,X87)|left_apart_point(X85,X87)|~divides_points(X87,X85,X86)))&((left_apart_point(X85,reverse_line(X87))|left_apart_point(X86,reverse_line(X87))|~divides_points(X87,X85,X86))&(left_apart_point(X86,X87)|left_apart_point(X86,reverse_line(X87))|~divides_points(X87,X85,X86))))&((~left_apart_point(X85,X87)|~left_apart_point(X86,reverse_line(X87))|divides_points(X87,X85,X86))&(~left_apart_point(X85,reverse_line(X87))|~left_apart_point(X86,X87)|divides_points(X87,X85,X86)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[div_def])])])).
% 0.29/1.62 fof(i_0_48, plain, ![X127, X128]:((~apart_point_and_line(intersection_point(X127,X128),X127)|(~unequally_directed_lines(X127,X128)|~unequally_directed_lines(X127,reverse_line(X128))))&(~apart_point_and_line(intersection_point(X127,X128),X128)|(~unequally_directed_lines(X127,X128)|~unequally_directed_lines(X127,reverse_line(X128))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_34])])])).
% 0.29/1.62 fof(i_0_49, plain, ![X140, X141, X142]:(~distinct_points(X140,X141)|~left_apart_point(X140,X142)|(left_apart_point(X141,X142)|left_convergent_lines(line_connecting(X140,X141),X142))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oaguc2])])).
% 0.29/1.62 fof(i_0_50, plain, ![X120, X121]:(~line(X120)|~line(X121)|~unequally_directed_lines(X120,X121)|~unequally_directed_lines(X120,reverse_line(X121))|point(intersection_point(X120,X121))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagco2])])).
% 0.29/1.62 fof(i_0_51, plain, ![X107, X108, X109]:(((unequally_directed_lines(X108,X109)|unequally_directed_lines(X107,X109)|(~unequally_directed_lines(X107,X108)|~unequally_directed_lines(X107,reverse_line(X108))))&(unequally_directed_lines(X108,reverse_line(X109))|unequally_directed_lines(X107,X109)|(~unequally_directed_lines(X107,X108)|~unequally_directed_lines(X107,reverse_line(X108)))))&((unequally_directed_lines(X108,X109)|unequally_directed_lines(X107,reverse_line(X109))|(~unequally_directed_lines(X107,X108)|~unequally_directed_lines(X107,reverse_line(X108))))&(unequally_directed_lines(X108,reverse_line(X109))|unequally_directed_lines(X107,reverse_line(X109))|(~unequally_directed_lines(X107,X108)|~unequally_directed_lines(X107,reverse_line(X108)))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag7])])])).
% 0.29/1.62 fof(i_0_52, plain, ![X112, X113]:(~unequally_directed_lines(X112,X113)|~unequally_directed_lines(X112,reverse_line(X113))|(left_convergent_lines(X112,X113)|left_convergent_lines(X112,reverse_line(X113)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag9])])).
% 0.29/1.62 fof(i_0_53, plain, ![X125, X126]:((~apart_point_and_line(X125,line_connecting(X125,X126))|~distinct_points(X125,X126))&(~apart_point_and_line(X126,line_connecting(X125,X126))|~distinct_points(X125,X126))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_35])])])).
% 0.29/1.62 fof(i_0_54, plain, ![X146, X147, X148]:(~left_apart_point(X146,X147)|~unequally_directed_lines(X147,X148)|(distinct_lines(X147,X148)|left_apart_point(X146,reverse_line(X148)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagsub2])])).
% 0.29/1.62 fof(i_0_55, plain, ![X83, X84]:(((unequally_directed_lines(X83,X84)|~convergent_lines(X83,X84))&(unequally_directed_lines(X83,reverse_line(X84))|~convergent_lines(X83,X84)))&(~unequally_directed_lines(X83,X84)|~unequally_directed_lines(X83,reverse_line(X84))|convergent_lines(X83,X84))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[con_def])])])).
% 0.29/1.62 fof(i_0_56, plain, ![X118, X119]:(~point(X118)|~point(X119)|~distinct_points(X118,X119)|line(line_connecting(X118,X119))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagco1])])).
% 0.29/1.62 fof(i_0_57, plain, ![X134, X135]:~unequally_directed_lines(parallel_through_point(X135,X134),X135), inference(variable_rename,[status(thm)],[i_0_36])).
% 0.29/1.62 fof(i_0_58, plain, ![X129, X130]:~apart_point_and_line(X129,parallel_through_point(X130,X129)), inference(variable_rename,[status(thm)],[i_0_37])).
% 0.29/1.62 fof(i_0_59, plain, ![X81, X82]:((~apart_point_and_line(X81,X82)|(left_apart_point(X81,X82)|left_apart_point(X81,reverse_line(X82))))&((~left_apart_point(X81,X82)|apart_point_and_line(X81,X82))&(~left_apart_point(X81,reverse_line(X82))|apart_point_and_line(X81,X82)))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[apt_def])])])).
% 0.29/1.62 fof(i_0_60, plain, ![X100, X101, X102]:(~distinct_lines(X100,X101)|(distinct_lines(X100,X102)|distinct_lines(X101,X102))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag4])])).
% 0.29/1.62 fof(i_0_61, plain, ![X96, X97, X98]:(~distinct_points(X96,X97)|(distinct_points(X96,X98)|distinct_points(X97,X98))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag2])])).
% 0.29/1.62 fof(i_0_62, plain, ![X149, X150, X151]:(~left_convergent_lines(X149,X150)|(unequally_directed_lines(X150,X151)|left_convergent_lines(X149,X151))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagsub3])])).
% 0.29/1.62 fof(i_0_63, plain, ![X104, X105, X106]:(~unequally_directed_lines(X104,X105)|(unequally_directed_lines(X104,X106)|unequally_directed_lines(X105,X106))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag6])])).
% 0.29/1.62 fof(i_0_64, plain, ![X143, X144, X145]:(~left_apart_point(X143,X145)|(distinct_points(X143,X144)|left_apart_point(X144,X145))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagsub1])])).
% 0.29/1.62 fof(i_0_65, negated_conjecture, ((apart_point_and_line(esk1_0,esk3_0)&~apart_point_and_line(esk2_0,parallel_through_point(esk3_0,esk1_0)))&~apart_point_and_line(esk2_0,esk3_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_38])])])).
% 0.29/1.62 fof(i_0_66, plain, ![X110, X111]:(~line(X110)|~line(X111)|(unequally_directed_lines(X110,X111)|unequally_directed_lines(X110,reverse_line(X111)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag8])])).
% 0.29/1.62 fof(i_0_67, plain, ![X122, X123]:(~point(X123)|~line(X122)|line(parallel_through_point(X122,X123))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagco3])])).
% 0.29/1.62 fof(i_0_68, plain, ![X116, X117]:(~left_convergent_lines(X116,X117)&~left_convergent_lines(X116,reverse_line(X117))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag11])])).
% 0.29/1.62 fof(i_0_69, plain, ![X131]:~distinct_lines(X131,reverse_line(X131)), inference(variable_rename,[status(thm)],[i_0_39])).
% 0.29/1.62 fof(i_0_70, plain, ![X114, X115]:(~left_apart_point(X114,X115)&~left_apart_point(X114,reverse_line(X115))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag10])])).
% 0.29/1.62 fof(i_0_71, plain, ![X99]:~distinct_lines(X99,X99), inference(variable_rename,[status(thm)],[i_0_40])).
% 0.29/1.62 fof(i_0_72, plain, ![X95]:~distinct_points(X95,X95), inference(variable_rename,[status(thm)],[i_0_41])).
% 0.29/1.62 fof(i_0_73, plain, ![X103]:~unequally_directed_lines(X103,X103), inference(variable_rename,[status(thm)],[i_0_42])).
% 0.29/1.62 fof(i_0_74, plain, ![X124]:(~line(X124)|line(reverse_line(X124))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagco4])])).
% 0.29/1.62 cnf(i_0_75, 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_43]), ['final']).
% 0.29/1.62 cnf(i_0_76, 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_43]), ['final']).
% 0.29/1.62 cnf(i_0_77, 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_43]), ['final']).
% 0.29/1.62 cnf(i_0_78, 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_43]), ['final']).
% 0.29/1.62 cnf(i_0_79, 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_43]), ['final']).
% 0.29/1.62 cnf(i_0_80, 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_43]), ['final']).
% 0.29/1.62 cnf(i_0_81, plain, (left_apart_point(X1,X3)|left_apart_point(X1,reverse_line(X3))|left_apart_point(X2,X3)|left_apart_point(X2,reverse_line(X3))|unequally_directed_lines(X3,line_connecting(X1,X2))|before_on_line(X3,X1,X2)|~distinct_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.29/1.62 cnf(i_0_82, 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_45]), ['final']).
% 0.29/1.62 cnf(i_0_83, plain, (~unequally_directed_lines(line_connecting(X1,X2),reverse_line(line_connecting(X2,X1)))), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.29/1.62 cnf(i_0_84, plain, (~unequally_directed_lines(X1,line_connecting(X2,X3))|~before_on_line(X1,X2,X3)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.29/1.62 cnf(i_0_85, plain, (left_apart_point(X1,reverse_line(X2))|left_apart_point(X3,reverse_line(X2))|~divides_points(X2,X1,X3)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.29/1.62 cnf(i_0_86, plain, (left_apart_point(X1,reverse_line(X2))|left_apart_point(X1,X2)|~divides_points(X2,X1,X3)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.29/1.62 cnf(i_0_87, plain, (left_apart_point(X1,X2)|left_apart_point(X1,reverse_line(X2))|~divides_points(X2,X3,X1)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.29/1.62 cnf(i_0_88, 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_48]), ['final']).
% 0.29/1.62 cnf(i_0_89, 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_48]), ['final']).
% 0.29/1.62 cnf(i_0_90, plain, (~left_apart_point(X1,reverse_line(X2))|~before_on_line(X2,X1,X3)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.29/1.62 cnf(i_0_91, plain, (~left_apart_point(X1,reverse_line(X2))|~before_on_line(X2,X3,X1)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.29/1.62 cnf(i_0_92, plain, (left_apart_point(X1,X2)|left_apart_point(X3,X2)|~divides_points(X2,X3,X1)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.29/1.62 cnf(i_0_93, plain, (divides_points(X2,X1,X3)|~left_apart_point(X1,X2)|~left_apart_point(X3,reverse_line(X2))), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.29/1.62 cnf(i_0_94, plain, (divides_points(X2,X1,X3)|~left_apart_point(X1,reverse_line(X2))|~left_apart_point(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.29/1.62 cnf(i_0_95, plain, (~left_apart_point(X1,X2)|~before_on_line(X2,X1,X3)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.29/1.62 cnf(i_0_96, plain, (~left_apart_point(X1,X2)|~before_on_line(X2,X3,X1)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.29/1.62 cnf(i_0_97, plain, (distinct_points(X1,X2)|~before_on_line(X3,X1,X2)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.29/1.62 cnf(i_0_98, 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_49]), ['final']).
% 0.29/1.62 cnf(i_0_99, 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_50]), ['final']).
% 0.29/1.62 cnf(i_0_100, 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_51]), ['final']).
% 0.29/1.62 cnf(i_0_101, 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_52]), ['final']).
% 0.29/1.62 cnf(i_0_102, 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_51]), ['final']).
% 0.29/1.62 cnf(i_0_103, 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_51]), ['final']).
% 0.29/1.62 cnf(i_0_104, plain, (~apart_point_and_line(X1,line_connecting(X1,X2))|~distinct_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.29/1.62 cnf(i_0_105, plain, (~apart_point_and_line(X1,line_connecting(X2,X1))|~distinct_points(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.29/1.62 cnf(i_0_106, 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_51]), ['final']).
% 0.29/1.62 cnf(i_0_107, 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_54]), ['final']).
% 0.29/1.62 cnf(i_0_108, plain, (convergent_lines(X1,X2)|~unequally_directed_lines(X1,X2)|~unequally_directed_lines(X1,reverse_line(X2))), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.29/1.62 cnf(i_0_109, plain, (line(line_connecting(X1,X2))|~point(X1)|~point(X2)|~distinct_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.29/1.62 cnf(i_0_110, plain, (~unequally_directed_lines(parallel_through_point(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.29/1.62 cnf(i_0_111, plain, (~apart_point_and_line(X1,parallel_through_point(X2,X1))), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.29/1.62 cnf(i_0_112, plain, (left_apart_point(X1,X2)|left_apart_point(X1,reverse_line(X2))|~apart_point_and_line(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.29/1.62 cnf(i_0_113, plain, (distinct_lines(X1,X3)|distinct_lines(X2,X3)|~distinct_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.29/1.62 cnf(i_0_114, plain, (distinct_points(X1,X3)|distinct_points(X2,X3)|~distinct_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.29/1.62 cnf(i_0_115, plain, (unequally_directed_lines(X2,X3)|left_convergent_lines(X1,X3)|~left_convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.29/1.62 cnf(i_0_116, plain, (unequally_directed_lines(X1,X3)|unequally_directed_lines(X2,X3)|~unequally_directed_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.29/1.62 cnf(i_0_117, plain, (distinct_points(X1,X3)|left_apart_point(X3,X2)|~left_apart_point(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.29/1.62 cnf(i_0_118, negated_conjecture, (~apart_point_and_line(esk2_0,parallel_through_point(esk3_0,esk1_0))), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.29/1.62 cnf(i_0_119, plain, (unequally_directed_lines(X1,X2)|unequally_directed_lines(X1,reverse_line(X2))|~line(X1)|~line(X2)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 0.29/1.62 cnf(i_0_120, plain, (apart_point_and_line(X1,X2)|~left_apart_point(X1,reverse_line(X2))), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.29/1.62 cnf(i_0_121, plain, (line(parallel_through_point(X2,X1))|~point(X1)|~line(X2)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.29/1.62 cnf(i_0_122, plain, (unequally_directed_lines(X1,reverse_line(X2))|~convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.29/1.62 cnf(i_0_123, plain, (unequally_directed_lines(X1,X2)|~convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.29/1.62 cnf(i_0_124, plain, (apart_point_and_line(X1,X2)|~left_apart_point(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.29/1.62 cnf(i_0_125, plain, (~left_convergent_lines(X1,reverse_line(X2))), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.29/1.62 cnf(i_0_126, plain, (~distinct_lines(X1,reverse_line(X1))), inference(split_conjunct,[status(thm)],[i_0_69]), ['final']).
% 0.29/1.62 cnf(i_0_127, plain, (~left_apart_point(X1,reverse_line(X2))), inference(split_conjunct,[status(thm)],[i_0_70]), ['final']).
% 0.29/1.62 cnf(i_0_128, plain, (~left_convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.29/1.62 cnf(i_0_129, plain, (~distinct_lines(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_71]), ['final']).
% 0.29/1.62 cnf(i_0_130, plain, (~distinct_points(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.29/1.62 cnf(i_0_131, plain, (~unequally_directed_lines(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.29/1.62 cnf(i_0_132, plain, (~left_apart_point(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_70]), ['final']).
% 0.29/1.62 cnf(i_0_133, negated_conjecture, (~apart_point_and_line(esk2_0,esk3_0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.29/1.62 cnf(i_0_134, plain, (line(reverse_line(X1))|~line(X1)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.29/1.62 cnf(i_0_135, negated_conjecture, (apart_point_and_line(esk1_0,esk3_0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.29/1.67 cnf(i_0_136, plain, (~before_on_line(X1,X2,X2)), inference(scs_inference,[],[i_0_130,i_0_97])).
% 0.29/1.67 cnf(i_0_137, plain, (distinct_points(X1,X2)|~before_on_line(X3,X1,X2)), inference(rename_variables,[],[i_0_97])).
% 0.29/1.67 cnf(i_0_138, plain, (~convergent_lines(reverse_line(X1),X1)), inference(scs_inference,[],[i_0_131,i_0_130,i_0_97,i_0_122])).
% 0.29/1.67 cnf(i_0_139, plain, (~unequally_directed_lines(X1,X1)), inference(rename_variables,[],[i_0_131])).
% 0.29/1.67 cnf(i_0_140, plain, (unequally_directed_lines(X1,reverse_line(X2))|~convergent_lines(X1,X2)), inference(rename_variables,[],[i_0_122])).
% 0.29/1.67 cnf(i_0_141, plain, (left_apart_point(esk1_0,esk3_0)), inference(scs_inference,[],[i_0_135,i_0_132,i_0_131,i_0_130,i_0_97,i_0_122,i_0_112])).
% 0.29/1.67 cnf(i_0_142, plain, (~left_apart_point(X1,X2)), inference(rename_variables,[],[i_0_132])).
% 0.29/1.67 cnf(i_0_143, plain, (left_apart_point(X1,reverse_line(X2))|~apart_point_and_line(X1,X2)|left_apart_point(X1,X2)), inference(rename_variables,[],[i_0_112])).
% 0.29/1.67 cnf(i_0_144, plain, (~between_on_line(X1,X2,X2,X3)), inference(scs_inference,[],[i_0_135,i_0_132,i_0_131,i_0_130,i_0_97,i_0_122,i_0_112,i_0_76])).
% 0.29/1.67 cnf(i_0_145, plain, (before_on_line(X1,X2,X3)|before_on_line(X1,X3,X2)|~between_on_line(X1,X2,X3,X4)), inference(rename_variables,[],[i_0_76])).
% 0.29/1.67 cnf(i_0_146, plain, (~between_on_line(X1,X2,X3,X3)), inference(scs_inference,[],[i_0_135,i_0_132,i_0_131,i_0_130,i_0_97,i_0_122,i_0_112,i_0_76,i_0_77])).
% 0.29/1.67 cnf(i_0_147, plain, (before_on_line(X1,X2,X3)|before_on_line(X1,X3,X2)|~between_on_line(X1,X4,X2,X3)), inference(rename_variables,[],[i_0_77])).
% 0.29/1.67 cnf(i_0_148, plain, (~line(line_connecting(X1,X1))), inference(scs_inference,[],[i_0_135,i_0_132,i_0_131,i_0_139,i_0_130,i_0_83,i_0_97,i_0_122,i_0_112,i_0_76,i_0_77,i_0_119])).
% 0.29/1.67 cnf(i_0_149, plain, (~unequally_directed_lines(line_connecting(X1,X2),reverse_line(line_connecting(X2,X1)))), inference(rename_variables,[],[i_0_83])).
% 0.29/1.67 cnf(i_0_150, plain, (~unequally_directed_lines(X1,X1)), inference(rename_variables,[],[i_0_131])).
% 0.29/1.67 cnf(i_0_151, plain, (unequally_directed_lines(X1,reverse_line(X2))|~line(X1)|~line(X2)|unequally_directed_lines(X1,X2)), inference(rename_variables,[],[i_0_119])).
% 0.29/1.67 cnf(i_0_152, plain, (~left_convergent_lines(X1,X2)), inference(rename_variables,[],[i_0_128])).
% 0.29/1.67 cnf(i_0_153, plain, (~left_apart_point(X1,X2)), inference(rename_variables,[],[i_0_132])).
% 0.29/1.67 cnf(i_0_154, plain, (~left_apart_point(X1,X2)), inference(rename_variables,[],[i_0_132])).
% 0.29/1.67 cnf(i_0_155, plain, (~unequally_directed_lines(X1,X1)), inference(rename_variables,[],[i_0_131])).
% 0.29/1.67 cnf(i_0_156, plain, (~left_apart_point(X1,X2)), inference(rename_variables,[],[i_0_132])).
% 0.29/1.67 cnf(i_0_157, plain, (~left_apart_point(X1,X2)), inference(rename_variables,[],[i_0_132])).
% 0.29/1.67 cnf(i_0_158, plain, (~left_apart_point(X1,X2)), inference(rename_variables,[],[i_0_132])).
% 0.29/1.67 cnf(i_0_160,plain, ($false), inference(scs_inference,[],[i_0+141, i_0_132]), ['proof']).
% 0.29/1.67 % SZS output end CNFRefutation
% 0.29/1.67 % Total time : 1.273s
%------------------------------------------------------------------------------