%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO354+1 : TPTP v8.1.2. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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 May 9 17:21:58 EDT 2024
% Result : Satisfiable 0.48s 0.68s
% Output : Saturation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : GEO354+1 : TPTP v8.1.2. Released v6.4.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n003.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 08:33:23 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.48/0.68 % Version: 1.5
% 0.48/0.68 % SZS status Satisfiable
% 0.48/0.68 % SZS output start Saturation
% 0.48/0.68 fof(bf_def,axiom,(![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('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', bf_def)).
% 0.48/0.68 fof(c151,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))))))),inference(fof_simplification,[status(thm)],[bf_def])).
% 0.48/0.68 fof(c152,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))))&((((~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)))|before_on_line(L,A,B)))))),inference(fof_nnf,[status(thm)],[c151])).
% 0.48/0.68 fof(c153,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)))))))&(![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)))|before_on_line(L,A,B)))))),inference(shift_quantors,[status(thm)],[c152])).
% 0.48/0.68 fof(c155,plain,(![X89]:(![X90]:(![X91]:(![X92]:(![X93]:(![X94]:((~before_on_line(X89,X90,X91)|(((distinct_points(X90,X91)&(~left_apart_point(X90,X89)&~left_apart_point(X90,reverse_line(X89))))&(~left_apart_point(X91,X89)&~left_apart_point(X91,reverse_line(X89))))&~unequally_directed_lines(X89,line_connecting(X90,X91))))&((((~distinct_points(X93,X94)|(left_apart_point(X93,X92)|left_apart_point(X93,reverse_line(X92))))|(left_apart_point(X94,X92)|left_apart_point(X94,reverse_line(X92))))|unequally_directed_lines(X92,line_connecting(X93,X94)))|before_on_line(X92,X93,X94))))))))),inference(shift_quantors,[status(thm)],[fof(c154,plain,((![X89]:(![X90]:(![X91]:(~before_on_line(X89,X90,X91)|(((distinct_points(X90,X91)&(~left_apart_point(X90,X89)&~left_apart_point(X90,reverse_line(X89))))&(~left_apart_point(X91,X89)&~left_apart_point(X91,reverse_line(X89))))&~unequally_directed_lines(X89,line_connecting(X90,X91)))))))&(![X92]:(![X93]:(![X94]:((((~distinct_points(X93,X94)|(left_apart_point(X93,X92)|left_apart_point(X93,reverse_line(X92))))|(left_apart_point(X94,X92)|left_apart_point(X94,reverse_line(X92))))|unequally_directed_lines(X92,line_connecting(X93,X94)))|before_on_line(X92,X93,X94)))))),inference(variable_rename,[status(thm)],[c153])).])).
% 0.48/0.68 fof(c156,plain,(![X89]:(![X90]:(![X91]:(![X92]:(![X93]:(![X94]:(((((~before_on_line(X89,X90,X91)|distinct_points(X90,X91))&((~before_on_line(X89,X90,X91)|~left_apart_point(X90,X89))&(~before_on_line(X89,X90,X91)|~left_apart_point(X90,reverse_line(X89)))))&((~before_on_line(X89,X90,X91)|~left_apart_point(X91,X89))&(~before_on_line(X89,X90,X91)|~left_apart_point(X91,reverse_line(X89)))))&(~before_on_line(X89,X90,X91)|~unequally_directed_lines(X89,line_connecting(X90,X91))))&((((~distinct_points(X93,X94)|(left_apart_point(X93,X92)|left_apart_point(X93,reverse_line(X92))))|(left_apart_point(X94,X92)|left_apart_point(X94,reverse_line(X92))))|unequally_directed_lines(X92,line_connecting(X93,X94)))|before_on_line(X92,X93,X94))))))))),inference(distribute,[status(thm)],[c155])).
% 0.48/0.68 cnf(c163,plain,~distinct_points(X293,X291)|left_apart_point(X293,X292)|left_apart_point(X293,reverse_line(X292))|left_apart_point(X291,X292)|left_apart_point(X291,reverse_line(X292))|unequally_directed_lines(X292,line_connecting(X293,X291))|before_on_line(X292,X293,X291),inference(split_conjunct,[status(thm)],[c156])).
% 0.48/0.68 fof(div_def,axiom,(![A]:(![B]:(![L]:(divides_points(L,A,B)<=>((left_apart_point(A,L)&left_apart_point(B,reverse_line(L)))|(left_apart_point(A,reverse_line(L))&left_apart_point(B,L))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', div_def)).
% 0.48/0.68 fof(c164,plain,(![A]:(![B]:(![L]:((~divides_points(L,A,B)|((left_apart_point(A,L)&left_apart_point(B,reverse_line(L)))|(left_apart_point(A,reverse_line(L))&left_apart_point(B,L))))&(((~left_apart_point(A,L)|~left_apart_point(B,reverse_line(L)))&(~left_apart_point(A,reverse_line(L))|~left_apart_point(B,L)))|divides_points(L,A,B)))))),inference(fof_nnf,[status(thm)],[div_def])).
% 0.48/0.68 fof(c165,plain,((![A]:(![B]:(![L]:(~divides_points(L,A,B)|((left_apart_point(A,L)&left_apart_point(B,reverse_line(L)))|(left_apart_point(A,reverse_line(L))&left_apart_point(B,L)))))))&(![A]:(![B]:(![L]:(((~left_apart_point(A,L)|~left_apart_point(B,reverse_line(L)))&(~left_apart_point(A,reverse_line(L))|~left_apart_point(B,L)))|divides_points(L,A,B)))))),inference(shift_quantors,[status(thm)],[c164])).
% 0.48/0.68 fof(c167,plain,(![X95]:(![X96]:(![X97]:(![X98]:(![X99]:(![X100]:((~divides_points(X97,X95,X96)|((left_apart_point(X95,X97)&left_apart_point(X96,reverse_line(X97)))|(left_apart_point(X95,reverse_line(X97))&left_apart_point(X96,X97))))&(((~left_apart_point(X98,X100)|~left_apart_point(X99,reverse_line(X100)))&(~left_apart_point(X98,reverse_line(X100))|~left_apart_point(X99,X100)))|divides_points(X100,X98,X99))))))))),inference(shift_quantors,[status(thm)],[fof(c166,plain,((![X95]:(![X96]:(![X97]:(~divides_points(X97,X95,X96)|((left_apart_point(X95,X97)&left_apart_point(X96,reverse_line(X97)))|(left_apart_point(X95,reverse_line(X97))&left_apart_point(X96,X97)))))))&(![X98]:(![X99]:(![X100]:(((~left_apart_point(X98,X100)|~left_apart_point(X99,reverse_line(X100)))&(~left_apart_point(X98,reverse_line(X100))|~left_apart_point(X99,X100)))|divides_points(X100,X98,X99)))))),inference(variable_rename,[status(thm)],[c165])).])).
% 0.48/0.68 fof(c168,plain,(![X95]:(![X96]:(![X97]:(![X98]:(![X99]:(![X100]:((((~divides_points(X97,X95,X96)|(left_apart_point(X95,X97)|left_apart_point(X95,reverse_line(X97))))&(~divides_points(X97,X95,X96)|(left_apart_point(X95,X97)|left_apart_point(X96,X97))))&((~divides_points(X97,X95,X96)|(left_apart_point(X96,reverse_line(X97))|left_apart_point(X95,reverse_line(X97))))&(~divides_points(X97,X95,X96)|(left_apart_point(X96,reverse_line(X97))|left_apart_point(X96,X97)))))&(((~left_apart_point(X98,X100)|~left_apart_point(X99,reverse_line(X100)))|divides_points(X100,X98,X99))&((~left_apart_point(X98,reverse_line(X100))|~left_apart_point(X99,X100))|divides_points(X100,X98,X99)))))))))),inference(distribute,[status(thm)],[c167])).
% 0.48/0.68 cnf(c171,plain,~divides_points(X273,X272,X274)|left_apart_point(X274,reverse_line(X273))|left_apart_point(X272,reverse_line(X273)),inference(split_conjunct,[status(thm)],[c168])).
% 0.48/0.68 fof(oaguc1,axiom,(![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('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oaguc1)).
% 0.48/0.68 fof(c50,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)))))))),inference(fof_nnf,[status(thm)],[oaguc1])).
% 0.48/0.68 fof(c51,plain,(![X32]:(![X33]:(![X34]:(![X35]:((~distinct_points(X32,X33)|~distinct_lines(X34,X35))|(((((((left_apart_point(X32,X34)|left_apart_point(X33,X34))|left_apart_point(X32,X35))|left_apart_point(X33,X35))|left_apart_point(X32,reverse_line(X34)))|left_apart_point(X33,reverse_line(X34)))|left_apart_point(X32,reverse_line(X35)))|left_apart_point(X33,reverse_line(X35)))))))),inference(variable_rename,[status(thm)],[c50])).
% 0.48/0.68 cnf(c52,plain,~distinct_points(X268,X270)|~distinct_lines(X269,X271)|left_apart_point(X268,X269)|left_apart_point(X270,X269)|left_apart_point(X268,X271)|left_apart_point(X270,X271)|left_apart_point(X268,reverse_line(X269))|left_apart_point(X270,reverse_line(X269))|left_apart_point(X268,reverse_line(X271))|left_apart_point(X270,reverse_line(X271)),inference(split_conjunct,[status(thm)],[c51])).
% 0.48/0.68 fof(bet_def,axiom,(![L]:(![A]:(![B]:(![C]:(between_on_line(L,A,B,C)<=>((before_on_line(L,A,B)&before_on_line(L,B,C))|(before_on_line(L,C,B)&before_on_line(L,B,A)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', bet_def)).
% 0.48/0.68 fof(c140,plain,(![L]:(![A]:(![B]:(![C]:((~between_on_line(L,A,B,C)|((before_on_line(L,A,B)&before_on_line(L,B,C))|(before_on_line(L,C,B)&before_on_line(L,B,A))))&(((~before_on_line(L,A,B)|~before_on_line(L,B,C))&(~before_on_line(L,C,B)|~before_on_line(L,B,A)))|between_on_line(L,A,B,C))))))),inference(fof_nnf,[status(thm)],[bet_def])).
% 0.48/0.68 fof(c141,plain,((![L]:(![A]:(![B]:(![C]:(~between_on_line(L,A,B,C)|((before_on_line(L,A,B)&before_on_line(L,B,C))|(before_on_line(L,C,B)&before_on_line(L,B,A))))))))&(![L]:(![A]:(![B]:(![C]:(((~before_on_line(L,A,B)|~before_on_line(L,B,C))&(~before_on_line(L,C,B)|~before_on_line(L,B,A)))|between_on_line(L,A,B,C))))))),inference(shift_quantors,[status(thm)],[c140])).
% 0.48/0.68 fof(c143,plain,(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(![X88]:((~between_on_line(X81,X82,X83,X84)|((before_on_line(X81,X82,X83)&before_on_line(X81,X83,X84))|(before_on_line(X81,X84,X83)&before_on_line(X81,X83,X82))))&(((~before_on_line(X85,X86,X87)|~before_on_line(X85,X87,X88))&(~before_on_line(X85,X88,X87)|~before_on_line(X85,X87,X86)))|between_on_line(X85,X86,X87,X88))))))))))),inference(shift_quantors,[status(thm)],[fof(c142,plain,((![X81]:(![X82]:(![X83]:(![X84]:(~between_on_line(X81,X82,X83,X84)|((before_on_line(X81,X82,X83)&before_on_line(X81,X83,X84))|(before_on_line(X81,X84,X83)&before_on_line(X81,X83,X82))))))))&(![X85]:(![X86]:(![X87]:(![X88]:(((~before_on_line(X85,X86,X87)|~before_on_line(X85,X87,X88))&(~before_on_line(X85,X88,X87)|~before_on_line(X85,X87,X86)))|between_on_line(X85,X86,X87,X88))))))),inference(variable_rename,[status(thm)],[c141])).])).
% 0.48/0.68 fof(c144,plain,(![X81]:(![X82]:(![X83]:(![X84]:(![X85]:(![X86]:(![X87]:(![X88]:((((~between_on_line(X81,X82,X83,X84)|(before_on_line(X81,X82,X83)|before_on_line(X81,X84,X83)))&(~between_on_line(X81,X82,X83,X84)|(before_on_line(X81,X82,X83)|before_on_line(X81,X83,X82))))&((~between_on_line(X81,X82,X83,X84)|(before_on_line(X81,X83,X84)|before_on_line(X81,X84,X83)))&(~between_on_line(X81,X82,X83,X84)|(before_on_line(X81,X83,X84)|before_on_line(X81,X83,X82)))))&(((~before_on_line(X85,X86,X87)|~before_on_line(X85,X87,X88))|between_on_line(X85,X86,X87,X88))&((~before_on_line(X85,X88,X87)|~before_on_line(X85,X87,X86))|between_on_line(X85,X86,X87,X88)))))))))))),inference(distribute,[status(thm)],[c143])).
% 0.48/0.68 cnf(c150,plain,~before_on_line(X258,X259,X261)|~before_on_line(X258,X261,X260)|between_on_line(X258,X260,X261,X259),inference(split_conjunct,[status(thm)],[c144])).
% 0.48/0.68 cnf(c149,plain,~before_on_line(X249,X251,X250)|~before_on_line(X249,X250,X252)|between_on_line(X249,X251,X250,X252),inference(split_conjunct,[status(thm)],[c144])).
% 0.48/0.68 cnf(c192,plain,~before_on_line(X257,X256,X256)|between_on_line(X257,X256,X256,X256),inference(factor,[status(thm)],[c149])).
% 0.48/0.68 cnf(c148,plain,~between_on_line(X248,X246,X245,X247)|before_on_line(X248,X245,X247)|before_on_line(X248,X245,X246),inference(split_conjunct,[status(thm)],[c144])).
% 0.48/0.68 cnf(c147,plain,~between_on_line(X244,X242,X241,X243)|before_on_line(X244,X241,X243)|before_on_line(X244,X243,X241),inference(split_conjunct,[status(thm)],[c144])).
% 0.48/0.68 cnf(c146,plain,~between_on_line(X240,X238,X237,X239)|before_on_line(X240,X238,X237)|before_on_line(X240,X237,X238),inference(split_conjunct,[status(thm)],[c144])).
% 0.48/0.68 cnf(c145,plain,~between_on_line(X236,X234,X233,X235)|before_on_line(X236,X234,X233)|before_on_line(X236,X235,X233),inference(split_conjunct,[status(thm)],[c144])).
% 0.48/0.68 fof(oagco1,axiom,(![A]:(![B]:(((point(A)&point(B))&distinct_points(A,B))=>line(line_connecting(A,B))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oagco1)).
% 0.48/0.68 fof(c86,plain,(![A]:(![B]:(((~point(A)|~point(B))|~distinct_points(A,B))|line(line_connecting(A,B))))),inference(fof_nnf,[status(thm)],[oagco1])).
% 0.48/0.68 fof(c87,plain,(![X52]:(![X53]:(((~point(X52)|~point(X53))|~distinct_points(X52,X53))|line(line_connecting(X52,X53))))),inference(variable_rename,[status(thm)],[c86])).
% 0.48/0.68 cnf(c88,plain,~point(X227)|~point(X226)|~distinct_points(X227,X226)|line(line_connecting(X227,X226)),inference(split_conjunct,[status(thm)],[c87])).
% 0.48/0.68 cnf(c172,plain,~divides_points(X214,X213,X215)|left_apart_point(X215,reverse_line(X214))|left_apart_point(X215,X214),inference(split_conjunct,[status(thm)],[c168])).
% 0.48/0.68 cnf(c169,plain,~divides_points(X211,X210,X212)|left_apart_point(X210,X211)|left_apart_point(X210,reverse_line(X211)),inference(split_conjunct,[status(thm)],[c168])).
% 0.48/0.68 fof(apt_def,axiom,(![A]:(![L]:(apart_point_and_line(A,L)<=>(left_apart_point(A,L)|left_apart_point(A,reverse_line(L)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', apt_def)).
% 0.48/0.68 fof(c183,plain,(![A]:(![L]:((~apart_point_and_line(A,L)|(left_apart_point(A,L)|left_apart_point(A,reverse_line(L))))&((~left_apart_point(A,L)&~left_apart_point(A,reverse_line(L)))|apart_point_and_line(A,L))))),inference(fof_nnf,[status(thm)],[apt_def])).
% 0.48/0.68 fof(c184,plain,((![A]:(![L]:(~apart_point_and_line(A,L)|(left_apart_point(A,L)|left_apart_point(A,reverse_line(L))))))&(![A]:(![L]:((~left_apart_point(A,L)&~left_apart_point(A,reverse_line(L)))|apart_point_and_line(A,L))))),inference(shift_quantors,[status(thm)],[c183])).
% 0.48/0.68 fof(c186,plain,(![X105]:(![X106]:(![X107]:(![X108]:((~apart_point_and_line(X105,X106)|(left_apart_point(X105,X106)|left_apart_point(X105,reverse_line(X106))))&((~left_apart_point(X107,X108)&~left_apart_point(X107,reverse_line(X108)))|apart_point_and_line(X107,X108))))))),inference(shift_quantors,[status(thm)],[fof(c185,plain,((![X105]:(![X106]:(~apart_point_and_line(X105,X106)|(left_apart_point(X105,X106)|left_apart_point(X105,reverse_line(X106))))))&(![X107]:(![X108]:((~left_apart_point(X107,X108)&~left_apart_point(X107,reverse_line(X108)))|apart_point_and_line(X107,X108))))),inference(variable_rename,[status(thm)],[c184])).])).
% 0.48/0.68 fof(c187,plain,(![X105]:(![X106]:(![X107]:(![X108]:((~apart_point_and_line(X105,X106)|(left_apart_point(X105,X106)|left_apart_point(X105,reverse_line(X106))))&((~left_apart_point(X107,X108)|apart_point_and_line(X107,X108))&(~left_apart_point(X107,reverse_line(X108))|apart_point_and_line(X107,X108)))))))),inference(distribute,[status(thm)],[c186])).
% 0.48/0.68 cnf(c188,plain,~apart_point_and_line(X208,X209)|left_apart_point(X208,X209)|left_apart_point(X208,reverse_line(X209)),inference(split_conjunct,[status(thm)],[c187])).
% 0.48/0.68 fof(cld4,axiom,(![L]:(![M]:((line(L)&line(M))=>(~((~unequally_directed_lines(L,M))&(~unequally_directed_lines(L,reverse_line(M)))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+1.ax', cld4)).
% 0.48/0.68 fof(c7,plain,(![L]:(![M]:((line(L)&line(M))=>(~(~unequally_directed_lines(L,M)&~unequally_directed_lines(L,reverse_line(M))))))),inference(fof_simplification,[status(thm)],[cld4])).
% 0.48/0.68 fof(c8,plain,(![L]:(![M]:((~line(L)|~line(M))|(unequally_directed_lines(L,M)|unequally_directed_lines(L,reverse_line(M)))))),inference(fof_nnf,[status(thm)],[c7])).
% 0.48/0.68 fof(c9,plain,(![X7]:(![X8]:((~line(X7)|~line(X8))|(unequally_directed_lines(X7,X8)|unequally_directed_lines(X7,reverse_line(X8)))))),inference(variable_rename,[status(thm)],[c8])).
% 0.48/0.68 cnf(c10,plain,~line(X139)|~line(X140)|unequally_directed_lines(X139,X140)|unequally_directed_lines(X139,reverse_line(X140)),inference(split_conjunct,[status(thm)],[c9])).
% 0.48/0.68 cnf(c191,plain,~line(X198)|unequally_directed_lines(X198,X198)|unequally_directed_lines(X198,reverse_line(X198)),inference(factor,[status(thm)],[c10])).
% 0.48/0.68 cnf(c170,plain,~divides_points(X196,X195,X197)|left_apart_point(X195,X196)|left_apart_point(X197,X196),inference(split_conjunct,[status(thm)],[c168])).
% 0.48/0.68 cnf(c162,plain,~before_on_line(X192,X194,X193)|~unequally_directed_lines(X192,line_connecting(X194,X193)),inference(split_conjunct,[status(thm)],[c156])).
% 0.48/0.68 fof(oag2,axiom,(![A]:(![B]:(![C]:(distinct_points(A,B)=>(distinct_points(A,C)|distinct_points(B,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oag2)).
% 0.48/0.68 fof(c132,plain,(![A]:(![B]:(![C]:(~distinct_points(A,B)|(distinct_points(A,C)|distinct_points(B,C)))))),inference(fof_nnf,[status(thm)],[oag2])).
% 0.48/0.68 fof(c133,plain,(![A]:(![B]:(~distinct_points(A,B)|(![C]:(distinct_points(A,C)|distinct_points(B,C)))))),inference(shift_quantors,[status(thm)],[c132])).
% 0.48/0.68 fof(c135,plain,(![X77]:(![X78]:(![X79]:(~distinct_points(X77,X78)|(distinct_points(X77,X79)|distinct_points(X78,X79)))))),inference(shift_quantors,[status(thm)],[fof(c134,plain,(![X77]:(![X78]:(~distinct_points(X77,X78)|(![X79]:(distinct_points(X77,X79)|distinct_points(X78,X79)))))),inference(variable_rename,[status(thm)],[c133])).])).
% 0.48/0.68 cnf(c136,plain,~distinct_points(X189,X190)|distinct_points(X189,X191)|distinct_points(X190,X191),inference(split_conjunct,[status(thm)],[c135])).
% 0.48/0.68 fof(oag4,axiom,(![L]:(![M]:(![N]:(distinct_lines(L,M)=>(distinct_lines(L,N)|distinct_lines(M,N)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oag4)).
% 0.48/0.68 fof(c124,plain,(![L]:(![M]:(![N]:(~distinct_lines(L,M)|(distinct_lines(L,N)|distinct_lines(M,N)))))),inference(fof_nnf,[status(thm)],[oag4])).
% 0.48/0.68 fof(c125,plain,(![L]:(![M]:(~distinct_lines(L,M)|(![N]:(distinct_lines(L,N)|distinct_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c124])).
% 0.48/0.68 fof(c127,plain,(![X73]:(![X74]:(![X75]:(~distinct_lines(X73,X74)|(distinct_lines(X73,X75)|distinct_lines(X74,X75)))))),inference(shift_quantors,[status(thm)],[fof(c126,plain,(![X73]:(![X74]:(~distinct_lines(X73,X74)|(![X75]:(distinct_lines(X73,X75)|distinct_lines(X74,X75)))))),inference(variable_rename,[status(thm)],[c125])).])).
% 0.48/0.68 cnf(c128,plain,~distinct_lines(X184,X183)|distinct_lines(X184,X185)|distinct_lines(X183,X185),inference(split_conjunct,[status(thm)],[c127])).
% 0.48/0.68 fof(oag6,axiom,(![L]:(![M]:(![N]:(unequally_directed_lines(L,M)=>(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oag6)).
% 0.48/0.68 fof(c116,plain,(![L]:(![M]:(![N]:(~unequally_directed_lines(L,M)|(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(fof_nnf,[status(thm)],[oag6])).
% 0.48/0.68 fof(c117,plain,(![L]:(![M]:(~unequally_directed_lines(L,M)|(![N]:(unequally_directed_lines(L,N)|unequally_directed_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c116])).
% 0.48/0.68 fof(c119,plain,(![X69]:(![X70]:(![X71]:(~unequally_directed_lines(X69,X70)|(unequally_directed_lines(X69,X71)|unequally_directed_lines(X70,X71)))))),inference(shift_quantors,[status(thm)],[fof(c118,plain,(![X69]:(![X70]:(~unequally_directed_lines(X69,X70)|(![X71]:(unequally_directed_lines(X69,X71)|unequally_directed_lines(X70,X71)))))),inference(variable_rename,[status(thm)],[c117])).])).
% 0.48/0.68 cnf(c120,plain,~unequally_directed_lines(X181,X180)|unequally_directed_lines(X181,X182)|unequally_directed_lines(X180,X182),inference(split_conjunct,[status(thm)],[c119])).
% 0.48/0.68 fof(oagco3,axiom,(![L]:(![A]:((point(A)&line(L))=>line(parallel_through_point(L,A))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oagco3)).
% 0.48/0.68 fof(c80,plain,(![L]:(![A]:((~point(A)|~line(L))|line(parallel_through_point(L,A))))),inference(fof_nnf,[status(thm)],[oagco3])).
% 0.48/0.68 fof(c81,plain,(![X48]:(![X49]:((~point(X49)|~line(X48))|line(parallel_through_point(X48,X49))))),inference(variable_rename,[status(thm)],[c80])).
% 0.48/0.68 cnf(c82,plain,~point(X179)|~line(X178)|line(parallel_through_point(X178,X179)),inference(split_conjunct,[status(thm)],[c81])).
% 0.48/0.68 fof(cld2,axiom,(![L]:(![M]:(![N]:(((~unequally_directed_lines(L,M))&(~unequally_directed_lines(L,N)))=>(~unequally_directed_lines(M,N)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+1.ax', cld2)).
% 0.48/0.68 fof(c29,plain,(![L]:(![M]:(![N]:((~unequally_directed_lines(L,M)&~unequally_directed_lines(L,N))=>~unequally_directed_lines(M,N))))),inference(fof_simplification,[status(thm)],[cld2])).
% 0.48/0.68 fof(c30,plain,(![L]:(![M]:(![N]:((unequally_directed_lines(L,M)|unequally_directed_lines(L,N))|~unequally_directed_lines(M,N))))),inference(fof_nnf,[status(thm)],[c29])).
% 0.48/0.68 fof(c31,plain,(![X16]:(![X17]:(![X18]:((unequally_directed_lines(X16,X17)|unequally_directed_lines(X16,X18))|~unequally_directed_lines(X17,X18))))),inference(variable_rename,[status(thm)],[c30])).
% 0.48/0.68 cnf(c32,plain,unequally_directed_lines(X164,X165)|unequally_directed_lines(X164,X166)|~unequally_directed_lines(X165,X166),inference(split_conjunct,[status(thm)],[c31])).
% 0.48/0.68 fof(oagco5,axiom,(![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('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oagco5)).
% 0.48/0.68 fof(c71,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)))))),inference(fof_simplification,[status(thm)],[oagco5])).
% 0.48/0.68 fof(c72,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)))))),inference(fof_nnf,[status(thm)],[c71])).
% 0.48/0.68 fof(c73,plain,(![X45]:(![X46]:(~distinct_points(X45,X46)|(~apart_point_and_line(X45,line_connecting(X45,X46))&~apart_point_and_line(X46,line_connecting(X45,X46)))))),inference(variable_rename,[status(thm)],[c72])).
% 0.48/0.68 fof(c74,plain,(![X45]:(![X46]:((~distinct_points(X45,X46)|~apart_point_and_line(X45,line_connecting(X45,X46)))&(~distinct_points(X45,X46)|~apart_point_and_line(X46,line_connecting(X45,X46)))))),inference(distribute,[status(thm)],[c73])).
% 0.48/0.68 cnf(c76,plain,~distinct_points(X157,X156)|~apart_point_and_line(X156,line_connecting(X157,X156)),inference(split_conjunct,[status(thm)],[c74])).
% 0.48/0.68 cnf(c75,plain,~distinct_points(X152,X151)|~apart_point_and_line(X152,line_connecting(X152,X151)),inference(split_conjunct,[status(thm)],[c74])).
% 0.48/0.68 fof(con_def,axiom,(![L]:(![M]:(convergent_lines(L,M)<=>(unequally_directed_lines(L,M)&unequally_directed_lines(L,reverse_line(M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', con_def)).
% 0.48/0.68 fof(c175,plain,(![L]:(![M]:((~convergent_lines(L,M)|(unequally_directed_lines(L,M)&unequally_directed_lines(L,reverse_line(M))))&((~unequally_directed_lines(L,M)|~unequally_directed_lines(L,reverse_line(M)))|convergent_lines(L,M))))),inference(fof_nnf,[status(thm)],[con_def])).
% 0.48/0.68 fof(c176,plain,((![L]:(![M]:(~convergent_lines(L,M)|(unequally_directed_lines(L,M)&unequally_directed_lines(L,reverse_line(M))))))&(![L]:(![M]:((~unequally_directed_lines(L,M)|~unequally_directed_lines(L,reverse_line(M)))|convergent_lines(L,M))))),inference(shift_quantors,[status(thm)],[c175])).
% 0.48/0.68 fof(c178,plain,(![X101]:(![X102]:(![X103]:(![X104]:((~convergent_lines(X101,X102)|(unequally_directed_lines(X101,X102)&unequally_directed_lines(X101,reverse_line(X102))))&((~unequally_directed_lines(X103,X104)|~unequally_directed_lines(X103,reverse_line(X104)))|convergent_lines(X103,X104))))))),inference(shift_quantors,[status(thm)],[fof(c177,plain,((![X101]:(![X102]:(~convergent_lines(X101,X102)|(unequally_directed_lines(X101,X102)&unequally_directed_lines(X101,reverse_line(X102))))))&(![X103]:(![X104]:((~unequally_directed_lines(X103,X104)|~unequally_directed_lines(X103,reverse_line(X104)))|convergent_lines(X103,X104))))),inference(variable_rename,[status(thm)],[c176])).])).
% 0.48/0.68 fof(c179,plain,(![X101]:(![X102]:(![X103]:(![X104]:(((~convergent_lines(X101,X102)|unequally_directed_lines(X101,X102))&(~convergent_lines(X101,X102)|unequally_directed_lines(X101,reverse_line(X102))))&((~unequally_directed_lines(X103,X104)|~unequally_directed_lines(X103,reverse_line(X104)))|convergent_lines(X103,X104))))))),inference(distribute,[status(thm)],[c178])).
% 0.48/0.68 cnf(c181,plain,~convergent_lines(X148,X147)|unequally_directed_lines(X148,reverse_line(X147)),inference(split_conjunct,[status(thm)],[c179])).
% 0.48/0.68 cnf(c157,plain,~before_on_line(X136,X138,X137)|distinct_points(X138,X137),inference(split_conjunct,[status(thm)],[c156])).
% 0.48/0.68 cnf(c180,plain,~convergent_lines(X133,X132)|unequally_directed_lines(X133,X132),inference(split_conjunct,[status(thm)],[c179])).
% 0.48/0.68 fof(oagco4,axiom,(![L]:(line(L)=>line(reverse_line(L)))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oagco4)).
% 0.48/0.68 fof(c77,plain,(![L]:(~line(L)|line(reverse_line(L)))),inference(fof_nnf,[status(thm)],[oagco4])).
% 0.48/0.68 fof(c78,plain,(![X47]:(~line(X47)|line(reverse_line(X47)))),inference(variable_rename,[status(thm)],[c77])).
% 0.48/0.68 cnf(c79,plain,~line(X131)|line(reverse_line(X131)),inference(split_conjunct,[status(thm)],[c78])).
% 0.48/0.68 fof(oagco7,axiom,(![A]:(![L]:(~apart_point_and_line(A,parallel_through_point(L,A))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oagco7)).
% 0.48/0.68 fof(c62,plain,(![A]:(![L]:~apart_point_and_line(A,parallel_through_point(L,A)))),inference(fof_simplification,[status(thm)],[oagco7])).
% 0.48/0.68 fof(c63,plain,(![X41]:(![X42]:~apart_point_and_line(X41,parallel_through_point(X42,X41)))),inference(variable_rename,[status(thm)],[c62])).
% 0.48/0.68 cnf(c64,plain,~apart_point_and_line(X129,parallel_through_point(X130,X129)),inference(split_conjunct,[status(thm)],[c63])).
% 0.48/0.68 fof(cld5,axiom,(![L]:(![M]:(![N]:((~unequally_directed_lines(L,reverse_line(M)))&((~unequally_directed_lines(L,reverse_line(N)))=>(~unequally_directed_lines(M,N))))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+1.ax', cld5)).
% 0.48/0.68 fof(c0,plain,(![L]:(![M]:(![N]:(~unequally_directed_lines(L,reverse_line(M))&(~unequally_directed_lines(L,reverse_line(N))=>~unequally_directed_lines(M,N)))))),inference(fof_simplification,[status(thm)],[cld5])).
% 0.48/0.68 fof(c1,plain,(![L]:(![M]:(![N]:(~unequally_directed_lines(L,reverse_line(M))&(unequally_directed_lines(L,reverse_line(N))|~unequally_directed_lines(M,N)))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.48/0.68 fof(c2,plain,((![L]:(![M]:~unequally_directed_lines(L,reverse_line(M))))&(![L]:(![M]:(![N]:(unequally_directed_lines(L,reverse_line(N))|~unequally_directed_lines(M,N)))))),inference(shift_quantors,[status(thm)],[c1])).
% 0.48/0.68 fof(c4,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(~unequally_directed_lines(X2,reverse_line(X3))&(unequally_directed_lines(X4,reverse_line(X6))|~unequally_directed_lines(X5,X6)))))))),inference(shift_quantors,[status(thm)],[fof(c3,plain,((![X2]:(![X3]:~unequally_directed_lines(X2,reverse_line(X3))))&(![X4]:(![X5]:(![X6]:(unequally_directed_lines(X4,reverse_line(X6))|~unequally_directed_lines(X5,X6)))))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.48/0.68 cnf(c6,plain,unequally_directed_lines(X128,reverse_line(X126))|~unequally_directed_lines(X127,X126),inference(split_conjunct,[status(thm)],[c4])).
% 0.48/0.68 fof(oagco10,axiom,(![A]:(![L]:(~unequally_directed_lines(parallel_through_point(L,A),L)))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oagco10)).
% 0.48/0.68 fof(c53,plain,(![A]:(![L]:~unequally_directed_lines(parallel_through_point(L,A),L))),inference(fof_simplification,[status(thm)],[oagco10])).
% 0.48/0.68 fof(c54,plain,(![X36]:(![X37]:~unequally_directed_lines(parallel_through_point(X37,X36),X37))),inference(variable_rename,[status(thm)],[c53])).
% 0.48/0.68 cnf(c55,plain,~unequally_directed_lines(parallel_through_point(X124,X125),X124),inference(split_conjunct,[status(thm)],[c54])).
% 0.48/0.68 fof(oagco8,axiom,(![L]:(~distinct_lines(L,reverse_line(L)))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oagco8)).
% 0.48/0.68 fof(c59,plain,(![L]:~distinct_lines(L,reverse_line(L))),inference(fof_simplification,[status(thm)],[oagco8])).
% 0.48/0.68 fof(c60,plain,(![X40]:~distinct_lines(X40,reverse_line(X40))),inference(variable_rename,[status(thm)],[c59])).
% 0.48/0.68 cnf(c61,plain,~distinct_lines(X119,reverse_line(X119)),inference(split_conjunct,[status(thm)],[c60])).
% 0.48/0.68 fof(oag1,axiom,(![A]:(~distinct_points(A,A))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oag1)).
% 0.48/0.68 fof(c137,plain,(![A]:~distinct_points(A,A)),inference(fof_simplification,[status(thm)],[oag1])).
% 0.48/0.68 fof(c138,plain,(![X80]:~distinct_points(X80,X80)),inference(variable_rename,[status(thm)],[c137])).
% 0.48/0.68 cnf(c139,plain,~distinct_points(X118,X118),inference(split_conjunct,[status(thm)],[c138])).
% 0.48/0.68 cnf(c5,plain,~unequally_directed_lines(X116,reverse_line(X117)),inference(split_conjunct,[status(thm)],[c4])).
% 0.48/0.68 fof(oag3,axiom,(![L]:(~distinct_lines(L,L))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oag3)).
% 0.48/0.68 fof(c129,plain,(![L]:~distinct_lines(L,L)),inference(fof_simplification,[status(thm)],[oag3])).
% 0.48/0.68 fof(c130,plain,(![X76]:~distinct_lines(X76,X76)),inference(variable_rename,[status(thm)],[c129])).
% 0.48/0.68 cnf(c131,plain,~distinct_lines(X115,X115),inference(split_conjunct,[status(thm)],[c130])).
% 0.48/0.68 fof(oag10,axiom,(![A]:(![L]:(~(left_apart_point(A,L)|left_apart_point(A,reverse_line(L)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oag10)).
% 0.48/0.68 fof(c95,plain,(![A]:(![L]:(~left_apart_point(A,L)&~left_apart_point(A,reverse_line(L))))),inference(fof_nnf,[status(thm)],[oag10])).
% 0.48/0.68 fof(c96,plain,((![A]:(![L]:~left_apart_point(A,L)))&(![A]:(![L]:~left_apart_point(A,reverse_line(L))))),inference(shift_quantors,[status(thm)],[c95])).
% 0.48/0.68 fof(c98,plain,(![X58]:(![X59]:(![X60]:(![X61]:(~left_apart_point(X58,X59)&~left_apart_point(X60,reverse_line(X61))))))),inference(shift_quantors,[status(thm)],[fof(c97,plain,((![X58]:(![X59]:~left_apart_point(X58,X59)))&(![X60]:(![X61]:~left_apart_point(X60,reverse_line(X61))))),inference(variable_rename,[status(thm)],[c96])).])).
% 0.48/0.68 cnf(c99,plain,~left_apart_point(X112,X113),inference(split_conjunct,[status(thm)],[c98])).
% 0.48/0.68 fof(oag11,axiom,(![L]:(![M]:(~(left_convergent_lines(L,M)|left_convergent_lines(L,reverse_line(M)))))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax', oag11)).
% 0.48/0.68 fof(c89,plain,(![L]:(![M]:(~left_convergent_lines(L,M)&~left_convergent_lines(L,reverse_line(M))))),inference(fof_nnf,[status(thm)],[oag11])).
% 0.48/0.68 fof(c90,plain,((![L]:(![M]:~left_convergent_lines(L,M)))&(![L]:(![M]:~left_convergent_lines(L,reverse_line(M))))),inference(shift_quantors,[status(thm)],[c89])).
% 0.48/0.68 fof(c92,plain,(![X54]:(![X55]:(![X56]:(![X57]:(~left_convergent_lines(X54,X55)&~left_convergent_lines(X56,reverse_line(X57))))))),inference(shift_quantors,[status(thm)],[fof(c91,plain,((![X54]:(![X55]:~left_convergent_lines(X54,X55)))&(![X56]:(![X57]:~left_convergent_lines(X56,reverse_line(X57))))),inference(variable_rename,[status(thm)],[c90])).])).
% 0.48/0.68 cnf(c93,plain,~left_convergent_lines(X111,X110),inference(split_conjunct,[status(thm)],[c92])).
% 0.48/0.68 fof(cld1,axiom,(![L]:(~unequally_directed_lines(L,L))),file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+1.ax', cld1)).
% 0.48/0.68 fof(c33,plain,(![L]:~unequally_directed_lines(L,L)),inference(fof_simplification,[status(thm)],[cld1])).
% 0.48/0.68 fof(c34,plain,(![X19]:~unequally_directed_lines(X19,X19)),inference(variable_rename,[status(thm)],[c33])).
% 0.48/0.68 cnf(c35,plain,~unequally_directed_lines(X109,X109),inference(split_conjunct,[status(thm)],[c34])).
% 0.48/0.68 % SZS output end Saturation
% 0.48/0.68
% 0.48/0.68 % Initial clauses : 71
% 0.48/0.68 % Processed clauses : 39
% 0.48/0.68 % Factors computed : 3
% 0.48/0.68 % Resolvents computed: 0
% 0.48/0.68 % Tautologies deleted: 4
% 0.48/0.68 % Forward subsumed : 31
% 0.48/0.68 % Backward subsumed : 0
% 0.48/0.68 % -------- CPU Time ---------
% 0.48/0.68 % User time : 0.309 s
% 0.48/0.68 % System time : 0.016 s
% 0.48/0.68 % Total time : 0.325 s
%------------------------------------------------------------------------------