%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO196+3 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n002.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:19:50 PM UTC 2026
% Result : Theorem 49.49s 25.66s
% Output : CNFRefutation 50.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO196+3 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.32 % Computer : n002.cluster.edu
% 0.16/0.32 % Model : x86_64 x86_64
% 0.16/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.32 % Memory : 8042.1875MB
% 0.16/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.32 % CPULimit : 300
% 0.16/0.32 % WCLimit : 300
% 0.16/0.32 % DateTime : Mon May 4 17:47:16 EDT 2026
% 0.16/0.32 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 49.49/25.66 % Version : CSE_E---1.7
% 49.49/25.66 % Problem : theBenchmark.p
% 49.49/25.66 % SZS status Theorem for theBenchmark.p
% 49.49/25.66 % SZS output start CNFRefutation
% 49.49/25.66 fof(con, conjecture, ![X1, X2, X4, X5]:((((convergent_lines(X1,X2)&convergent_lines(X4,X5))&incident_point_and_line(intersection_point(X1,X2),X4))&incident_point_and_line(intersection_point(X1,X2),X5))=>(incident_point_and_line(intersection_point(X4,X5),X1)&incident_point_and_line(intersection_point(X4,X5),X2))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', con)).
% 49.49/25.66 fof(ci3, axiom, ![X1, X2]:(convergent_lines(X1,X2)=>~(apart_point_and_line(intersection_point(X1,X2),X1))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ci3)).
% 49.49/25.66 fof(ci4, axiom, ![X1, X2]:(convergent_lines(X1,X2)=>~(apart_point_and_line(intersection_point(X1,X2),X2))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ci4)).
% 49.49/25.66 fof(ci1, axiom, ![X1, X2]:(distinct_points(X1,X2)=>~(apart_point_and_line(X1,line_connecting(X1,X2)))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ci1)).
% 49.49/25.66 fof(ci2, axiom, ![X1, X2]:(distinct_points(X1,X2)=>~(apart_point_and_line(X2,line_connecting(X1,X2)))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ci2)).
% 49.49/25.66 fof(cotno1, axiom, ![X6, X7, X8]:(((~(convergent_lines(X6,X7))|~(unorthogonal_lines(X6,X7)))&(~(convergent_lines(X6,X8))|~(unorthogonal_lines(X6,X8))))=>(~(convergent_lines(X7,X8))|~(unorthogonal_lines(X7,X8)))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax', cotno1)).
% 49.49/25.66 fof(ooc1, axiom, ![X9, X6]:~(unorthogonal_lines(orthogonal_through_point(X6,X9),X6)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ooc1)).
% 49.49/25.66 fof(cp1, axiom, ![X1, X2]:~(convergent_lines(parallel_through_point(X2,X1),X2)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+2.ax', cp1)).
% 49.49/25.66 fof(ooc2, axiom, ![X9, X6]:~(apart_point_and_line(X9,orthogonal_through_point(X6,X9))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ooc2)).
% 49.49/25.66 fof(cp2, axiom, ![X1, X2]:~(apart_point_and_line(X1,parallel_through_point(X2,X1))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+2.ax', cp2)).
% 49.49/25.66 fof(couo1, axiom, ![X6, X7, X8]:((~(unorthogonal_lines(X6,X7))&~(unorthogonal_lines(X6,X8)))=>~(convergent_lines(X7,X8))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax', couo1)).
% 49.49/25.66 fof(a5, axiom, ![X1, X2]:(orthogonal_lines(X1,X2)<=>~(unorthogonal_lines(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a5)).
% 49.49/25.66 fof(a4, axiom, ![X1, X2]:(incident_point_and_line(X1,X2)<=>~(apart_point_and_line(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a4)).
% 49.49/25.66 fof(a3, axiom, ![X1, X2]:(parallel_lines(X1,X2)<=>~(convergent_lines(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', a3)).
% 49.49/25.66 fof(ax2, axiom, ![X1, X2]:(equal_lines(X1,X2)<=>~(distinct_lines(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', ax2)).
% 49.49/25.66 fof(ax1, axiom, ![X1, X2]:(equal_points(X1,X2)<=>~(distinct_points(X1,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+6.ax', ax1)).
% 49.49/25.66 fof(coipo1, axiom, ![X6, X7]:~((~(convergent_lines(X6,X7))&~(unorthogonal_lines(X6,X7)))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+4.ax', coipo1)).
% 49.49/25.66 fof(apart3, axiom, ![X1]:~(convergent_lines(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart3)).
% 49.49/25.66 fof(apart2, axiom, ![X1]:~(distinct_lines(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart2)).
% 49.49/25.66 fof(apart1, axiom, ![X1]:~(distinct_points(X1,X1)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart1)).
% 49.49/25.66 fof(cu1, axiom, ![X1, X2, X4, X5]:((distinct_points(X1,X2)&distinct_lines(X4,X5))=>(apart_point_and_line(X1,X4)|apart_point_and_line(X1,X5)|apart_point_and_line(X2,X4)|apart_point_and_line(X2,X5))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', cu1)).
% 49.49/25.66 fof(ouo1, axiom, ![X9, X6, X7, X8]:(distinct_lines(X6,X7)=>(apart_point_and_line(X9,X6)|apart_point_and_line(X9,X7)|unorthogonal_lines(X6,X8)|unorthogonal_lines(X7,X8))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', ouo1)).
% 49.49/25.66 fof(oac1, axiom, ![X6, X7, X8]:((convergent_lines(X6,X7)&unorthogonal_lines(X6,X7))=>((convergent_lines(X6,X8)&unorthogonal_lines(X6,X8))|(convergent_lines(X7,X8)&unorthogonal_lines(X7,X8)))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', oac1)).
% 49.49/25.66 fof(con1, axiom, ![X9, X10]:(((point(X9)&point(X10))&distinct_points(X9,X10))=>line(line_connecting(X9,X10))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+5.ax', con1)).
% 49.49/25.66 fof(int1, axiom, ![X6, X7]:(((line(X6)&line(X7))&convergent_lines(X6,X7))=>point(intersection_point(X6,X7))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+5.ax', int1)).
% 49.49/25.66 fof(cup1, axiom, ![X1, X2, X3]:(distinct_lines(X2,X3)=>(apart_point_and_line(X1,X2)|apart_point_and_line(X1,X3)|convergent_lines(X2,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+2.ax', cup1)).
% 49.49/25.66 fof(ax6, axiom, ![X1, X2, X3]:(convergent_lines(X1,X2)=>(convergent_lines(X1,X3)|convergent_lines(X2,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ax6)).
% 49.49/25.66 fof(ceq2, axiom, ![X1, X2, X3]:(apart_point_and_line(X1,X2)=>(distinct_lines(X2,X3)|apart_point_and_line(X1,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ceq2)).
% 49.49/25.66 fof(ceq3, axiom, ![X1, X2, X3]:(convergent_lines(X1,X2)=>(distinct_lines(X2,X3)|convergent_lines(X1,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ceq3)).
% 49.49/25.66 fof(apart5, axiom, ![X1, X2, X3]:(distinct_lines(X1,X2)=>(distinct_lines(X1,X3)|distinct_lines(X2,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart5)).
% 49.49/25.66 fof(ceq1, axiom, ![X1, X2, X3]:(apart_point_and_line(X1,X2)=>(distinct_points(X1,X3)|apart_point_and_line(X3,X2))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', ceq1)).
% 49.49/25.66 fof(apart4, axiom, ![X1, X2, X3]:(distinct_points(X1,X2)=>(distinct_points(X1,X3)|distinct_points(X2,X3))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+0.ax', apart4)).
% 49.49/25.66 fof(orth1, axiom, ![X6, X9]:((line(X6)&point(X9))=>line(orthogonal_through_point(X6,X9))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+5.ax', orth1)).
% 49.49/25.66 fof(par1, axiom, ![X6, X9]:((line(X6)&point(X9))=>line(parallel_through_point(X6,X9))), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+5.ax', par1)).
% 49.49/25.66 fof(p1, axiom, ![X1, X2]:(distinct_lines(X1,X2)=>convergent_lines(X1,X2)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+1.ax', p1)).
% 49.49/25.66 fof(occu1, axiom, ![X6, X7]:(convergent_lines(X6,X7)|unorthogonal_lines(X6,X7)), file('/export/starexec/sandbox2/benchmark/Axioms/GEO006+3.ax', occu1)).
% 49.49/25.66 fof(i_0_36, negated_conjecture, ~(![X1, X2, X4, X5]:((((convergent_lines(X1,X2)&convergent_lines(X4,X5))&incident_point_and_line(intersection_point(X1,X2),X4))&incident_point_and_line(intersection_point(X1,X2),X5))=>(incident_point_and_line(intersection_point(X4,X5),X1)&incident_point_and_line(intersection_point(X4,X5),X2)))), inference(assume_negation,[status(cth)],[con])).
% 49.49/25.66 fof(i_0_37, plain, ![X1, X2]:(convergent_lines(X1,X2)=>~apart_point_and_line(intersection_point(X1,X2),X1)), inference(fof_simplification,[status(thm)],[ci3])).
% 49.49/25.66 fof(i_0_38, plain, ![X1, X2]:(convergent_lines(X1,X2)=>~apart_point_and_line(intersection_point(X1,X2),X2)), inference(fof_simplification,[status(thm)],[ci4])).
% 49.49/25.66 fof(i_0_39, plain, ![X1, X2]:(distinct_points(X1,X2)=>~apart_point_and_line(X1,line_connecting(X1,X2))), inference(fof_simplification,[status(thm)],[ci1])).
% 49.49/25.66 fof(i_0_40, plain, ![X1, X2]:(distinct_points(X1,X2)=>~apart_point_and_line(X2,line_connecting(X1,X2))), inference(fof_simplification,[status(thm)],[ci2])).
% 49.49/25.66 fof(i_0_41, plain, ![X6, X7, X8]:(((~convergent_lines(X6,X7)|~unorthogonal_lines(X6,X7))&(~convergent_lines(X6,X8)|~unorthogonal_lines(X6,X8)))=>(~convergent_lines(X7,X8)|~unorthogonal_lines(X7,X8))), inference(fof_simplification,[status(thm)],[cotno1])).
% 49.49/25.66 fof(i_0_42, plain, ![X9, X6]:~unorthogonal_lines(orthogonal_through_point(X6,X9),X6), inference(fof_simplification,[status(thm)],[ooc1])).
% 49.49/25.66 fof(i_0_43, plain, ![X1, X2]:~convergent_lines(parallel_through_point(X2,X1),X2), inference(fof_simplification,[status(thm)],[cp1])).
% 49.49/25.66 fof(i_0_44, plain, ![X9, X6]:~apart_point_and_line(X9,orthogonal_through_point(X6,X9)), inference(fof_simplification,[status(thm)],[ooc2])).
% 49.49/25.66 fof(i_0_45, plain, ![X1, X2]:~apart_point_and_line(X1,parallel_through_point(X2,X1)), inference(fof_simplification,[status(thm)],[cp2])).
% 49.49/25.66 fof(i_0_46, plain, ![X6, X7, X8]:((~unorthogonal_lines(X6,X7)&~unorthogonal_lines(X6,X8))=>~convergent_lines(X7,X8)), inference(fof_simplification,[status(thm)],[couo1])).
% 49.49/25.66 fof(i_0_47, plain, ![X1, X2]:(orthogonal_lines(X1,X2)<=>~unorthogonal_lines(X1,X2)), inference(fof_simplification,[status(thm)],[a5])).
% 49.49/25.66 fof(i_0_48, plain, ![X1, X2]:(incident_point_and_line(X1,X2)<=>~apart_point_and_line(X1,X2)), inference(fof_simplification,[status(thm)],[a4])).
% 49.49/25.66 fof(i_0_49, plain, ![X1, X2]:(parallel_lines(X1,X2)<=>~convergent_lines(X1,X2)), inference(fof_simplification,[status(thm)],[a3])).
% 49.49/25.66 fof(i_0_50, plain, ![X1, X2]:(equal_lines(X1,X2)<=>~distinct_lines(X1,X2)), inference(fof_simplification,[status(thm)],[ax2])).
% 49.49/25.66 fof(i_0_51, plain, ![X1, X2]:(equal_points(X1,X2)<=>~distinct_points(X1,X2)), inference(fof_simplification,[status(thm)],[ax1])).
% 49.49/25.66 fof(i_0_52, plain, ![X6, X7]:~((~convergent_lines(X6,X7)&~unorthogonal_lines(X6,X7))), inference(fof_simplification,[status(thm)],[coipo1])).
% 49.49/25.66 fof(i_0_53, plain, ![X1]:~convergent_lines(X1,X1), inference(fof_simplification,[status(thm)],[apart3])).
% 49.49/25.66 fof(i_0_54, plain, ![X1]:~distinct_lines(X1,X1), inference(fof_simplification,[status(thm)],[apart2])).
% 49.49/25.66 fof(i_0_55, plain, ![X1]:~distinct_points(X1,X1), inference(fof_simplification,[status(thm)],[apart1])).
% 49.49/25.66 fof(i_0_56, plain, ![X116, X117, X118, X119]:(~distinct_points(X116,X117)|~distinct_lines(X118,X119)|(apart_point_and_line(X116,X118)|apart_point_and_line(X116,X119)|apart_point_and_line(X117,X118)|apart_point_and_line(X117,X119))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cu1])])).
% 49.49/25.66 fof(i_0_57, negated_conjecture, ((((convergent_lines(esk1_0,esk2_0)&convergent_lines(esk3_0,esk4_0))&incident_point_and_line(intersection_point(esk1_0,esk2_0),esk3_0))&incident_point_and_line(intersection_point(esk1_0,esk2_0),esk4_0))&(~incident_point_and_line(intersection_point(esk3_0,esk4_0),esk1_0)|~incident_point_and_line(intersection_point(esk3_0,esk4_0),esk2_0))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_36])])])).
% 49.49/25.66 fof(i_0_58, plain, ![X112, X113]:(~convergent_lines(X112,X113)|~apart_point_and_line(intersection_point(X112,X113),X112)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_37])])).
% 49.49/25.66 fof(i_0_59, plain, ![X114, X115]:(~convergent_lines(X114,X115)|~apart_point_and_line(intersection_point(X114,X115),X115)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_38])])).
% 49.49/25.66 fof(i_0_60, plain, ![X108, X109]:(~distinct_points(X108,X109)|~apart_point_and_line(X108,line_connecting(X108,X109))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_39])])).
% 49.49/25.66 fof(i_0_61, plain, ![X110, X111]:(~distinct_points(X110,X111)|~apart_point_and_line(X111,line_connecting(X110,X111))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_40])])).
% 49.49/25.66 fof(i_0_62, plain, ![X147, X148, X149, X150]:(~distinct_lines(X148,X149)|(apart_point_and_line(X147,X148)|apart_point_and_line(X147,X149)|unorthogonal_lines(X148,X150)|unorthogonal_lines(X149,X150))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ouo1])])).
% 49.49/25.66 fof(i_0_63, plain, ![X153, X154, X155]:(((convergent_lines(X153,X155)|convergent_lines(X153,X154)|(~convergent_lines(X154,X155)|~unorthogonal_lines(X154,X155)))&(unorthogonal_lines(X153,X155)|convergent_lines(X153,X154)|(~convergent_lines(X154,X155)|~unorthogonal_lines(X154,X155))))&((convergent_lines(X153,X155)|unorthogonal_lines(X153,X154)|(~convergent_lines(X154,X155)|~unorthogonal_lines(X154,X155)))&(unorthogonal_lines(X153,X155)|unorthogonal_lines(X153,X154)|(~convergent_lines(X154,X155)|~unorthogonal_lines(X154,X155))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_41])])])).
% 49.49/25.66 fof(i_0_64, plain, ![X140, X141, X142]:(((convergent_lines(X141,X142)|convergent_lines(X140,X142)|(~convergent_lines(X140,X141)|~unorthogonal_lines(X140,X141)))&(unorthogonal_lines(X141,X142)|convergent_lines(X140,X142)|(~convergent_lines(X140,X141)|~unorthogonal_lines(X140,X141))))&((convergent_lines(X141,X142)|unorthogonal_lines(X140,X142)|(~convergent_lines(X140,X141)|~unorthogonal_lines(X140,X141)))&(unorthogonal_lines(X141,X142)|unorthogonal_lines(X140,X142)|(~convergent_lines(X140,X141)|~unorthogonal_lines(X140,X141))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oac1])])])).
% 49.49/25.66 fof(i_0_65, plain, ![X159, X160]:(~point(X159)|~point(X160)|~distinct_points(X159,X160)|line(line_connecting(X159,X160))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[con1])])).
% 49.49/25.66 fof(i_0_66, plain, ![X161, X162]:(~line(X161)|~line(X162)|~convergent_lines(X161,X162)|point(intersection_point(X161,X162))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[int1])])).
% 49.49/25.66 fof(i_0_67, plain, ![X135, X136, X137]:(~distinct_lines(X136,X137)|(apart_point_and_line(X135,X136)|apart_point_and_line(X135,X137)|convergent_lines(X136,X137))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cup1])])).
% 49.49/25.66 fof(i_0_68, plain, ![X143, X144]:~unorthogonal_lines(orthogonal_through_point(X144,X143),X144), inference(variable_rename,[status(thm)],[i_0_42])).
% 49.49/25.66 fof(i_0_69, plain, ![X131, X132]:~convergent_lines(parallel_through_point(X132,X131),X132), inference(variable_rename,[status(thm)],[i_0_43])).
% 49.49/25.66 fof(i_0_70, plain, ![X145, X146]:~apart_point_and_line(X145,orthogonal_through_point(X146,X145)), inference(variable_rename,[status(thm)],[i_0_44])).
% 49.49/25.66 fof(i_0_71, plain, ![X133, X134]:~apart_point_and_line(X133,parallel_through_point(X134,X133)), inference(variable_rename,[status(thm)],[i_0_45])).
% 49.49/25.66 fof(i_0_72, plain, ![X156, X157, X158]:(unorthogonal_lines(X156,X157)|unorthogonal_lines(X156,X158)|~convergent_lines(X157,X158)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_46])])).
% 49.49/25.66 fof(i_0_73, plain, ![X105, X106, X107]:(~convergent_lines(X105,X106)|(convergent_lines(X105,X107)|convergent_lines(X106,X107))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax6])])).
% 49.49/25.66 fof(i_0_74, plain, ![X123, X124, X125]:(~apart_point_and_line(X123,X124)|(distinct_lines(X124,X125)|apart_point_and_line(X123,X125))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ceq2])])).
% 49.49/25.66 fof(i_0_75, plain, ![X126, X127, X128]:(~convergent_lines(X126,X127)|(distinct_lines(X127,X128)|convergent_lines(X126,X128))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ceq3])])).
% 49.49/25.66 fof(i_0_76, plain, ![X102, X103, X104]:(~distinct_lines(X102,X103)|(distinct_lines(X102,X104)|distinct_lines(X103,X104))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[apart5])])).
% 49.49/25.66 fof(i_0_77, plain, ![X120, X121, X122]:(~apart_point_and_line(X120,X121)|(distinct_points(X120,X122)|apart_point_and_line(X122,X121))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ceq1])])).
% 49.49/25.66 fof(i_0_78, plain, ![X99, X100, X101]:(~distinct_points(X99,X100)|(distinct_points(X99,X101)|distinct_points(X100,X101))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[apart4])])).
% 49.49/25.66 fof(i_0_79, plain, ![X175, X176]:((~orthogonal_lines(X175,X176)|~unorthogonal_lines(X175,X176))&(unorthogonal_lines(X175,X176)|orthogonal_lines(X175,X176))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_47])])).
% 49.49/25.66 fof(i_0_80, plain, ![X173, X174]:((~incident_point_and_line(X173,X174)|~apart_point_and_line(X173,X174))&(apart_point_and_line(X173,X174)|incident_point_and_line(X173,X174))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_48])])).
% 49.49/25.66 fof(i_0_81, plain, ![X171, X172]:((~parallel_lines(X171,X172)|~convergent_lines(X171,X172))&(convergent_lines(X171,X172)|parallel_lines(X171,X172))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_49])])).
% 49.49/25.66 fof(i_0_82, plain, ![X169, X170]:((~equal_lines(X169,X170)|~distinct_lines(X169,X170))&(distinct_lines(X169,X170)|equal_lines(X169,X170))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_50])])).
% 49.49/25.66 fof(i_0_83, plain, ![X167, X168]:((~equal_points(X167,X168)|~distinct_points(X167,X168))&(distinct_points(X167,X168)|equal_points(X167,X168))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_51])])).
% 49.49/25.66 fof(i_0_84, plain, ![X165, X166]:(~line(X165)|~point(X166)|line(orthogonal_through_point(X165,X166))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[orth1])])).
% 49.49/25.66 fof(i_0_85, plain, ![X163, X164]:(~line(X163)|~point(X164)|line(parallel_through_point(X163,X164))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[par1])])).
% 49.49/25.66 fof(i_0_86, plain, ![X129, X130]:(~distinct_lines(X129,X130)|convergent_lines(X129,X130)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p1])])).
% 49.49/25.66 fof(i_0_87, plain, ![X151, X152]:(convergent_lines(X151,X152)|unorthogonal_lines(X151,X152)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_52])])).
% 49.49/25.66 fof(i_0_88, plain, ![X138, X139]:(convergent_lines(X138,X139)|unorthogonal_lines(X138,X139)), inference(variable_rename,[status(thm)],[occu1])).
% 49.49/25.66 fof(i_0_89, plain, ![X98]:~convergent_lines(X98,X98), inference(variable_rename,[status(thm)],[i_0_53])).
% 49.49/25.66 fof(i_0_90, plain, ![X97]:~distinct_lines(X97,X97), inference(variable_rename,[status(thm)],[i_0_54])).
% 49.49/25.66 fof(i_0_91, plain, ![X96]:~distinct_points(X96,X96), inference(variable_rename,[status(thm)],[i_0_55])).
% 49.49/25.66 cnf(i_0_92, plain, (apart_point_and_line(X1,X3)|apart_point_and_line(X1,X4)|apart_point_and_line(X2,X3)|apart_point_and_line(X2,X4)|~distinct_points(X1,X2)|~distinct_lines(X3,X4)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 49.49/25.66 cnf(i_0_93, negated_conjecture, (~incident_point_and_line(intersection_point(esk3_0,esk4_0),esk1_0)|~incident_point_and_line(intersection_point(esk3_0,esk4_0),esk2_0)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 49.49/25.66 cnf(i_0_94, plain, (~convergent_lines(X1,X2)|~apart_point_and_line(intersection_point(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 49.49/25.66 cnf(i_0_95, plain, (~convergent_lines(X1,X2)|~apart_point_and_line(intersection_point(X1,X2),X2)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 49.49/25.66 cnf(i_0_96, plain, (~distinct_points(X1,X2)|~apart_point_and_line(X1,line_connecting(X1,X2))), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 49.49/25.66 cnf(i_0_97, plain, (~distinct_points(X1,X2)|~apart_point_and_line(X2,line_connecting(X1,X2))), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 49.49/25.66 cnf(i_0_98, plain, (apart_point_and_line(X3,X1)|apart_point_and_line(X3,X2)|unorthogonal_lines(X1,X4)|unorthogonal_lines(X2,X4)|~distinct_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 49.49/25.66 cnf(i_0_99, plain, (unorthogonal_lines(X1,X2)|unorthogonal_lines(X1,X3)|~convergent_lines(X3,X2)|~unorthogonal_lines(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 49.49/25.66 cnf(i_0_100, plain, (unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|~convergent_lines(X3,X1)|~unorthogonal_lines(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 49.49/25.66 cnf(i_0_101, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X1,X3)|~convergent_lines(X3,X2)|~unorthogonal_lines(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 49.49/25.66 cnf(i_0_102, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X3,X2)|~convergent_lines(X3,X1)|~unorthogonal_lines(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 49.49/25.66 cnf(i_0_103, plain, (unorthogonal_lines(X1,X2)|convergent_lines(X1,X3)|~convergent_lines(X3,X2)|~unorthogonal_lines(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 49.49/25.66 cnf(i_0_104, plain, (convergent_lines(X1,X2)|convergent_lines(X1,X3)|~convergent_lines(X3,X2)|~unorthogonal_lines(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 49.49/25.66 cnf(i_0_105, plain, (unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|~convergent_lines(X3,X1)|~unorthogonal_lines(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 49.49/25.66 cnf(i_0_106, plain, (convergent_lines(X1,X2)|convergent_lines(X3,X2)|~convergent_lines(X3,X1)|~unorthogonal_lines(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 49.49/25.66 cnf(i_0_107, plain, (line(line_connecting(X1,X2))|~point(X1)|~point(X2)|~distinct_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 49.49/25.66 cnf(i_0_108, plain, (point(intersection_point(X1,X2))|~line(X1)|~line(X2)|~convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 49.49/25.66 cnf(i_0_109, plain, (apart_point_and_line(X3,X1)|apart_point_and_line(X3,X2)|convergent_lines(X1,X2)|~distinct_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 49.49/25.66 cnf(i_0_110, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 49.49/25.66 cnf(i_0_111, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_69]), ['final']).
% 49.49/25.66 cnf(i_0_112, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(split_conjunct,[status(thm)],[i_0_70]), ['final']).
% 49.49/25.66 cnf(i_0_113, plain, (~apart_point_and_line(X1,parallel_through_point(X2,X1))), inference(split_conjunct,[status(thm)],[i_0_71]), ['final']).
% 49.49/25.66 cnf(i_0_114, plain, (unorthogonal_lines(X1,X2)|unorthogonal_lines(X1,X3)|~convergent_lines(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 49.49/25.66 cnf(i_0_115, plain, (convergent_lines(X1,X3)|convergent_lines(X2,X3)|~convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 49.49/25.66 cnf(i_0_116, plain, (distinct_lines(X2,X3)|apart_point_and_line(X1,X3)|~apart_point_and_line(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 49.49/25.66 cnf(i_0_117, plain, (distinct_lines(X2,X3)|convergent_lines(X1,X3)|~convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_75]), ['final']).
% 49.49/25.66 cnf(i_0_118, plain, (distinct_lines(X1,X3)|distinct_lines(X2,X3)|~distinct_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_76]), ['final']).
% 49.49/25.66 cnf(i_0_119, plain, (distinct_points(X1,X3)|apart_point_and_line(X3,X2)|~apart_point_and_line(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_77]), ['final']).
% 49.49/25.66 cnf(i_0_120, plain, (distinct_points(X1,X3)|distinct_points(X2,X3)|~distinct_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_78]), ['final']).
% 49.49/25.66 cnf(i_0_121, plain, (~orthogonal_lines(X1,X2)|~unorthogonal_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 49.49/25.66 cnf(i_0_122, plain, (~incident_point_and_line(X1,X2)|~apart_point_and_line(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_80]), ['final']).
% 49.49/25.66 cnf(i_0_123, plain, (~parallel_lines(X1,X2)|~convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_81]), ['final']).
% 49.49/25.66 cnf(i_0_124, plain, (~equal_lines(X1,X2)|~distinct_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_82]), ['final']).
% 49.49/25.66 cnf(i_0_125, plain, (~equal_points(X1,X2)|~distinct_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_83]), ['final']).
% 49.49/25.66 cnf(i_0_126, plain, (line(orthogonal_through_point(X1,X2))|~line(X1)|~point(X2)), inference(split_conjunct,[status(thm)],[i_0_84]), ['final']).
% 49.49/25.66 cnf(i_0_127, plain, (line(parallel_through_point(X1,X2))|~line(X1)|~point(X2)), inference(split_conjunct,[status(thm)],[i_0_85]), ['final']).
% 49.49/25.66 cnf(i_0_128, plain, (convergent_lines(X1,X2)|~distinct_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_86]), ['final']).
% 49.49/25.66 cnf(i_0_129, negated_conjecture, (incident_point_and_line(intersection_point(esk1_0,esk2_0),esk4_0)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 49.49/25.66 cnf(i_0_130, negated_conjecture, (incident_point_and_line(intersection_point(esk1_0,esk2_0),esk3_0)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 49.49/25.66 cnf(i_0_131, plain, (unorthogonal_lines(X1,X2)|orthogonal_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 49.49/25.66 cnf(i_0_132, plain, (apart_point_and_line(X1,X2)|incident_point_and_line(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_80]), ['final']).
% 49.49/25.66 cnf(i_0_133, plain, (convergent_lines(X1,X2)|parallel_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_81]), ['final']).
% 49.49/25.66 cnf(i_0_134, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_87]), ['final']).
% 49.49/25.66 cnf(i_0_135, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_88]), ['final']).
% 49.49/25.66 cnf(i_0_136, plain, (distinct_lines(X1,X2)|equal_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_82]), ['final']).
% 49.49/25.66 cnf(i_0_137, plain, (distinct_points(X1,X2)|equal_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_83]), ['final']).
% 49.49/25.66 cnf(i_0_138, plain, (~convergent_lines(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_89]), ['final']).
% 49.49/25.66 cnf(i_0_139, plain, (~distinct_lines(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_90]), ['final']).
% 49.49/25.66 cnf(i_0_140, plain, (~distinct_points(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_91]), ['final']).
% 49.49/25.66 cnf(i_0_141, negated_conjecture, (convergent_lines(esk3_0,esk4_0)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 49.49/25.66 cnf(i_0_142, negated_conjecture, (convergent_lines(esk1_0,esk2_0)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 50.29/26.07 cnf(i_0_143, plain, (~parallel_lines(esk3_0,esk4_0)), inference(scs_inference,[],[i_0_141,i_0_123])).
% 50.29/26.07 cnf(i_0_144, plain, (~convergent_lines(X1,X2)|~parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_123])).
% 50.29/26.07 cnf(i_0_145, plain, (convergent_lines(orthogonal_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_141,i_0_110,i_0_123,i_0_135])).
% 50.29/26.07 cnf(i_0_146, plain, (unorthogonal_lines(X1,X2)|convergent_lines(X1,X2)), inference(rename_variables,[],[i_0_135])).
% 50.29/26.07 cnf(i_0_147, plain, (unorthogonal_lines(orthogonal_through_point(esk3_0,X1),esk4_0)), inference(scs_inference,[],[i_0_141,i_0_110,i_0_123,i_0_135,i_0_114])).
% 50.29/26.07 cnf(i_0_148, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_149, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_150, plain, (convergent_lines(esk4_0,esk3_0)), inference(scs_inference,[],[i_0_141,i_0_138,i_0_110,i_0_123,i_0_135,i_0_114,i_0_115])).
% 50.29/26.07 cnf(i_0_151, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_152, plain, (~convergent_lines(X1,X2)|convergent_lines(X1,X3)|convergent_lines(X2,X3)), inference(rename_variables,[],[i_0_115])).
% 50.29/26.07 cnf(i_0_153, plain, (~orthogonal_lines(orthogonal_through_point(esk3_0,X1),esk4_0)), inference(scs_inference,[],[i_0_141,i_0_138,i_0_110,i_0_123,i_0_135,i_0_114,i_0_115,i_0_121])).
% 50.29/26.07 cnf(i_0_154, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_155, plain, (~unorthogonal_lines(esk3_0,esk4_0)|unorthogonal_lines(esk4_0,esk3_0)), inference(scs_inference,[],[i_0_141,i_0_138,i_0_151,i_0_110,i_0_123,i_0_135,i_0_114,i_0_115,i_0_121,i_0_101])).
% 50.29/26.07 cnf(i_0_156, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_157, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_158, plain, (~unorthogonal_lines(esk4_0,esk3_0)|unorthogonal_lines(esk4_0,esk3_0)), inference(scs_inference,[],[i_0_141,i_0_138,i_0_151,i_0_156,i_0_110,i_0_123,i_0_135,i_0_114,i_0_115,i_0_121,i_0_101,i_0_105])).
% 50.29/26.07 cnf(i_0_159, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_160, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_105])).
% 50.29/26.07 cnf(i_0_161, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_162, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_163, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_164, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_165, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_167, plain, (~parallel_lines(esk1_0,esk2_0)), inference(scs_inference,[],[i_0_142,i_0_123])).
% 50.29/26.07 cnf(i_0_168, plain, (~convergent_lines(X1,X2)|~parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_123])).
% 50.29/26.07 cnf(i_0_169, plain, (unorthogonal_lines(orthogonal_through_point(esk1_0,X1),esk2_0)), inference(scs_inference,[],[i_0_142,i_0_110,i_0_123,i_0_114])).
% 50.29/26.07 cnf(i_0_170, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_171, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_172, plain, (convergent_lines(esk2_0,esk1_0)), inference(scs_inference,[],[i_0_142,i_0_138,i_0_110,i_0_123,i_0_114,i_0_115])).
% 50.29/26.07 cnf(i_0_173, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_174, plain, (~convergent_lines(X1,X2)|convergent_lines(X1,X3)|convergent_lines(X2,X3)), inference(rename_variables,[],[i_0_115])).
% 50.29/26.07 cnf(i_0_175, plain, (~orthogonal_lines(orthogonal_through_point(esk1_0,X1),esk2_0)), inference(scs_inference,[],[i_0_142,i_0_138,i_0_110,i_0_123,i_0_114,i_0_115,i_0_121])).
% 50.29/26.07 cnf(i_0_176, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_177, plain, (~unorthogonal_lines(esk3_0,esk4_0)|unorthogonal_lines(parallel_through_point(esk4_0,X1),esk3_0)), inference(scs_inference,[],[i_0_141,i_0_142,i_0_111,i_0_138,i_0_110,i_0_123,i_0_114,i_0_115,i_0_121,i_0_101])).
% 50.29/26.07 cnf(i_0_178, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_179, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_180, plain, (~unorthogonal_lines(esk4_0,esk3_0)|unorthogonal_lines(parallel_through_point(esk4_0,X1),esk3_0)), inference(scs_inference,[],[i_0_141,i_0_142,i_0_150,i_0_111,i_0_138,i_0_173,i_0_110,i_0_123,i_0_114,i_0_115,i_0_121,i_0_101,i_0_105])).
% 50.29/26.07 cnf(i_0_181, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_182, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_105])).
% 50.29/26.07 cnf(i_0_183, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_184, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_185, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_186, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_187, plain, (~apart_point_and_line(X1,parallel_through_point(X2,X1))), inference(rename_variables,[],[i_0_113])).
% 50.29/26.07 cnf(i_0_189, plain, (~parallel_lines(esk4_0,esk3_0)), inference(scs_inference,[],[i_0_150,i_0_123])).
% 50.29/26.07 cnf(i_0_190, plain, (~convergent_lines(X1,X2)|~parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_123])).
% 50.29/26.07 cnf(i_0_191, plain, (unorthogonal_lines(orthogonal_through_point(esk4_0,X1),esk3_0)), inference(scs_inference,[],[i_0_150,i_0_110,i_0_123,i_0_114])).
% 50.29/26.07 cnf(i_0_192, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_193, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_194, plain, (convergent_lines(X1,orthogonal_through_point(X1,X2))), inference(scs_inference,[],[i_0_150,i_0_145,i_0_138,i_0_110,i_0_123,i_0_114,i_0_115])).
% 50.29/26.07 cnf(i_0_195, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_196, plain, (~convergent_lines(X1,X2)|convergent_lines(X1,X3)|convergent_lines(X2,X3)), inference(rename_variables,[],[i_0_115])).
% 50.29/26.07 cnf(i_0_197, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(scs_inference,[],[i_0_150,i_0_145,i_0_138,i_0_195,i_0_110,i_0_192,i_0_123,i_0_114,i_0_115,i_0_105])).
% 50.29/26.07 cnf(i_0_198, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_199, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_105])).
% 50.29/26.07 cnf(i_0_200, plain, (~orthogonal_lines(orthogonal_through_point(esk4_0,X1),esk3_0)), inference(scs_inference,[],[i_0_150,i_0_145,i_0_138,i_0_195,i_0_110,i_0_192,i_0_123,i_0_114,i_0_115,i_0_105,i_0_121])).
% 50.29/26.07 cnf(i_0_201, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_202, plain, (~unorthogonal_lines(esk3_0,esk4_0)|unorthogonal_lines(esk3_0,orthogonal_through_point(esk4_0,X1))), inference(scs_inference,[],[i_0_141,i_0_150,i_0_145,i_0_138,i_0_195,i_0_110,i_0_192,i_0_123,i_0_114,i_0_115,i_0_105,i_0_121,i_0_100])).
% 50.29/26.07 cnf(i_0_203, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_100])).
% 50.29/26.07 cnf(i_0_204, plain, (~unorthogonal_lines(esk3_0,esk4_0)|convergent_lines(parallel_through_point(esk4_0,X1),esk3_0)), inference(scs_inference,[],[i_0_141,i_0_150,i_0_145,i_0_111,i_0_138,i_0_195,i_0_110,i_0_192,i_0_123,i_0_114,i_0_115,i_0_105,i_0_121,i_0_100,i_0_104])).
% 50.29/26.07 cnf(i_0_205, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_206, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_104])).
% 50.29/26.07 cnf(i_0_207, plain, (~unorthogonal_lines(esk1_0,esk2_0)|unorthogonal_lines(parallel_through_point(esk2_0,X1),esk1_0)), inference(scs_inference,[],[i_0_141,i_0_142,i_0_150,i_0_145,i_0_111,i_0_205,i_0_138,i_0_195,i_0_110,i_0_192,i_0_123,i_0_114,i_0_115,i_0_105,i_0_121,i_0_100,i_0_104,i_0_101])).
% 50.29/26.07 cnf(i_0_208, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_209, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_210, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_211, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_212, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_213, plain, (~apart_point_and_line(X1,parallel_through_point(X2,X1))), inference(rename_variables,[],[i_0_113])).
% 50.29/26.07 cnf(i_0_215, plain, (~parallel_lines(X1,orthogonal_through_point(X1,X2))), inference(scs_inference,[],[i_0_194,i_0_123])).
% 50.29/26.07 cnf(i_0_216, plain, (~convergent_lines(X1,X2)|~parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_123])).
% 50.29/26.07 cnf(i_0_217, plain, (unorthogonal_lines(X1,orthogonal_through_point(orthogonal_through_point(X1,X2),X3))), inference(scs_inference,[],[i_0_194,i_0_197,i_0_123,i_0_114])).
% 50.29/26.07 cnf(i_0_218, plain, (convergent_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_194])).
% 50.29/26.07 cnf(i_0_219, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_220, plain, (convergent_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(scs_inference,[],[i_0_194,i_0_218,i_0_197,i_0_111,i_0_123,i_0_114,i_0_115])).
% 50.29/26.07 cnf(i_0_221, plain, (convergent_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_194])).
% 50.29/26.07 cnf(i_0_222, plain, (~convergent_lines(X1,X2)|convergent_lines(X1,X3)|convergent_lines(X2,X3)), inference(rename_variables,[],[i_0_115])).
% 50.29/26.07 cnf(i_0_223, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(scs_inference,[],[i_0_194,i_0_218,i_0_197,i_0_111,i_0_123,i_0_114,i_0_115,i_0_101])).
% 50.29/26.07 cnf(i_0_224, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_225, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_226, plain, (~unorthogonal_lines(esk1_0,esk2_0)|convergent_lines(parallel_through_point(esk2_0,X1),esk1_0)), inference(scs_inference,[],[i_0_142,i_0_194,i_0_218,i_0_197,i_0_111,i_0_123,i_0_114,i_0_115,i_0_101,i_0_104])).
% 50.29/26.07 cnf(i_0_227, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_228, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_104])).
% 50.29/26.07 cnf(i_0_229, plain, (~unorthogonal_lines(esk1_0,esk2_0)|unorthogonal_lines(esk1_0,orthogonal_through_point(esk2_0,X1))), inference(scs_inference,[],[i_0_142,i_0_194,i_0_218,i_0_197,i_0_224,i_0_111,i_0_123,i_0_114,i_0_115,i_0_101,i_0_104,i_0_100])).
% 50.29/26.07 cnf(i_0_230, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_231, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_100])).
% 50.29/26.07 cnf(i_0_232, plain, (~unorthogonal_lines(esk3_0,esk4_0)|unorthogonal_lines(esk3_0,esk4_0)), inference(scs_inference,[],[i_0_141,i_0_142,i_0_194,i_0_218,i_0_197,i_0_224,i_0_111,i_0_138,i_0_123,i_0_114,i_0_115,i_0_101,i_0_104,i_0_100,i_0_102])).
% 50.29/26.07 cnf(i_0_233, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_234, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_102])).
% 50.29/26.07 cnf(i_0_235, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_236, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_237, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_239, plain, (~orthogonal_lines(X1,orthogonal_through_point(orthogonal_through_point(X1,X2),X3))), inference(scs_inference,[],[i_0_217,i_0_121])).
% 50.29/26.07 cnf(i_0_240, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_241, plain, (~parallel_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(scs_inference,[],[i_0_217,i_0_220,i_0_121,i_0_123])).
% 50.29/26.07 cnf(i_0_242, plain, (~convergent_lines(X1,X2)|~parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_123])).
% 50.29/26.07 cnf(i_0_243, plain, (unorthogonal_lines(orthogonal_through_point(parallel_through_point(esk3_0,X1),X2),esk4_0)), inference(scs_inference,[],[i_0_141,i_0_217,i_0_220,i_0_223,i_0_121,i_0_123,i_0_114])).
% 50.29/26.07 cnf(i_0_244, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_245, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_246, plain, (~unorthogonal_lines(esk4_0,esk3_0)|unorthogonal_lines(esk4_0,orthogonal_through_point(esk3_0,X1))), inference(scs_inference,[],[i_0_141,i_0_150,i_0_217,i_0_220,i_0_223,i_0_197,i_0_121,i_0_123,i_0_114,i_0_100])).
% 50.29/26.07 cnf(i_0_247, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_248, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_100])).
% 50.29/26.07 cnf(i_0_249, plain, (~unorthogonal_lines(esk3_0,esk4_0)|unorthogonal_lines(esk4_0,orthogonal_through_point(esk3_0,X1))), inference(scs_inference,[],[i_0_141,i_0_150,i_0_217,i_0_220,i_0_223,i_0_197,i_0_138,i_0_121,i_0_123,i_0_114,i_0_100,i_0_101])).
% 50.29/26.07 cnf(i_0_250, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_251, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_252, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_253, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_254, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_255, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_256, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_257, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_258, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_259, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_261, plain, (~orthogonal_lines(orthogonal_through_point(parallel_through_point(esk3_0,X1),X2),esk4_0)), inference(scs_inference,[],[i_0_243,i_0_121])).
% 50.29/26.07 cnf(i_0_262, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_263, plain, (~parallel_lines(esk2_0,esk1_0)), inference(scs_inference,[],[i_0_172,i_0_243,i_0_121,i_0_123])).
% 50.29/26.07 cnf(i_0_264, plain, (~convergent_lines(X1,X2)|~parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_123])).
% 50.29/26.07 cnf(i_0_265, plain, (unorthogonal_lines(orthogonal_through_point(parallel_through_point(esk1_0,X1),X2),esk2_0)), inference(scs_inference,[],[i_0_142,i_0_172,i_0_243,i_0_223,i_0_121,i_0_123,i_0_114])).
% 50.29/26.07 cnf(i_0_266, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_267, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_268, plain, (~unorthogonal_lines(esk2_0,esk1_0)|unorthogonal_lines(esk2_0,orthogonal_through_point(esk1_0,X1))), inference(scs_inference,[],[i_0_142,i_0_172,i_0_243,i_0_223,i_0_197,i_0_121,i_0_123,i_0_114,i_0_100])).
% 50.29/26.07 cnf(i_0_269, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_270, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_100])).
% 50.29/26.07 cnf(i_0_271, plain, (~unorthogonal_lines(esk1_0,esk2_0)|unorthogonal_lines(esk2_0,orthogonal_through_point(esk1_0,X1))), inference(scs_inference,[],[i_0_142,i_0_172,i_0_243,i_0_223,i_0_197,i_0_138,i_0_121,i_0_123,i_0_114,i_0_100,i_0_101])).
% 50.29/26.07 cnf(i_0_272, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_273, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_274, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_275, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_276, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_277, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_278, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_279, plain, (~apart_point_and_line(X1,parallel_through_point(X2,X1))), inference(rename_variables,[],[i_0_113])).
% 50.29/26.07 cnf(i_0_280, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_281, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_283, plain, (~orthogonal_lines(orthogonal_through_point(parallel_through_point(esk1_0,X1),X2),esk2_0)), inference(scs_inference,[],[i_0_265,i_0_121])).
% 50.29/26.07 cnf(i_0_284, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_285, plain, (~parallel_lines(orthogonal_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_265,i_0_145,i_0_121,i_0_123])).
% 50.29/26.07 cnf(i_0_286, plain, (~convergent_lines(X1,X2)|~parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_123])).
% 50.29/26.07 cnf(i_0_287, plain, (unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),orthogonal_through_point(X1,X4))), inference(scs_inference,[],[i_0_194,i_0_265,i_0_223,i_0_145,i_0_121,i_0_123,i_0_114])).
% 50.29/26.07 cnf(i_0_288, plain, (convergent_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_194])).
% 50.29/26.07 cnf(i_0_289, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_290, plain, (~unorthogonal_lines(esk4_0,esk3_0)|convergent_lines(parallel_through_point(esk3_0,X1),esk4_0)), inference(scs_inference,[],[i_0_194,i_0_150,i_0_265,i_0_223,i_0_145,i_0_111,i_0_121,i_0_123,i_0_114,i_0_104])).
% 50.29/26.07 cnf(i_0_291, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_292, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_104])).
% 50.29/26.07 cnf(i_0_293, plain, (convergent_lines(parallel_through_point(esk3_0,X1),esk4_0)|~unorthogonal_lines(esk3_0,esk4_0)), inference(scs_inference,[],[i_0_194,i_0_150,i_0_265,i_0_223,i_0_145,i_0_111,i_0_121,i_0_123,i_0_114,i_0_104,i_0_155])).
% 50.29/26.07 cnf(i_0_294, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_295, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_296, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_297, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_298, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_299, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_300, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_301, plain, (~apart_point_and_line(X1,parallel_through_point(X2,X1))), inference(rename_variables,[],[i_0_113])).
% 50.29/26.07 cnf(i_0_302, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_303, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_305, plain, (~orthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),orthogonal_through_point(X1,X4))), inference(scs_inference,[],[i_0_287,i_0_121])).
% 50.29/26.07 cnf(i_0_306, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_307, plain, (unorthogonal_lines(orthogonal_through_point(parallel_through_point(esk4_0,X1),X2),esk3_0)), inference(scs_inference,[],[i_0_150,i_0_223,i_0_287,i_0_121,i_0_114])).
% 50.29/26.07 cnf(i_0_308, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_309, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_310, plain, (~unorthogonal_lines(esk2_0,esk1_0)|convergent_lines(parallel_through_point(esk1_0,X1),esk2_0)), inference(scs_inference,[],[i_0_150,i_0_172,i_0_223,i_0_287,i_0_111,i_0_121,i_0_114,i_0_104])).
% 50.29/26.07 cnf(i_0_311, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_312, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_104])).
% 50.29/26.07 cnf(i_0_313, plain, (~unorthogonal_lines(esk3_0,esk4_0)|convergent_lines(orthogonal_through_point(parallel_through_point(esk4_0,X1),X2),esk3_0)), inference(scs_inference,[],[i_0_141,i_0_150,i_0_172,i_0_223,i_0_308,i_0_287,i_0_111,i_0_121,i_0_114,i_0_104,i_0_103])).
% 50.29/26.07 cnf(i_0_314, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_315, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_316, plain, (~unorthogonal_lines(esk3_0,esk4_0)|convergent_lines(esk3_0,orthogonal_through_point(esk4_0,X1))), inference(scs_inference,[],[i_0_141,i_0_150,i_0_172,i_0_197,i_0_223,i_0_308,i_0_287,i_0_111,i_0_121,i_0_114,i_0_104,i_0_103,i_0_105])).
% 50.29/26.07 cnf(i_0_317, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_318, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_105])).
% 50.29/26.07 cnf(i_0_319, plain, (~unorthogonal_lines(esk4_0,esk3_0)|unorthogonal_lines(parallel_through_point(esk3_0,X1),esk4_0)), inference(scs_inference,[],[i_0_141,i_0_150,i_0_172,i_0_197,i_0_223,i_0_308,i_0_287,i_0_111,i_0_311,i_0_121,i_0_114,i_0_104,i_0_103,i_0_105,i_0_101])).
% 50.29/26.07 cnf(i_0_320, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_321, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_322, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_323, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_325, plain, (~orthogonal_lines(orthogonal_through_point(parallel_through_point(esk4_0,X1),X2),esk3_0)), inference(scs_inference,[],[i_0_307,i_0_121])).
% 50.29/26.07 cnf(i_0_326, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_327, plain, (unorthogonal_lines(orthogonal_through_point(parallel_through_point(esk2_0,X1),X2),esk1_0)), inference(scs_inference,[],[i_0_172,i_0_223,i_0_307,i_0_121,i_0_114])).
% 50.29/26.07 cnf(i_0_328, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_329, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_330, plain, (~unorthogonal_lines(esk1_0,esk2_0)|convergent_lines(orthogonal_through_point(parallel_through_point(esk2_0,X1),X2),esk1_0)), inference(scs_inference,[],[i_0_142,i_0_172,i_0_223,i_0_328,i_0_307,i_0_121,i_0_114,i_0_103])).
% 50.29/26.07 cnf(i_0_331, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_332, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_333, plain, (~unorthogonal_lines(esk1_0,esk2_0)|convergent_lines(esk1_0,orthogonal_through_point(esk2_0,X1))), inference(scs_inference,[],[i_0_142,i_0_172,i_0_197,i_0_223,i_0_328,i_0_307,i_0_121,i_0_114,i_0_103,i_0_105])).
% 50.29/26.07 cnf(i_0_334, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_335, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_105])).
% 50.29/26.07 cnf(i_0_336, plain, (~unorthogonal_lines(esk2_0,esk1_0)|unorthogonal_lines(parallel_through_point(esk1_0,X1),esk2_0)), inference(scs_inference,[],[i_0_142,i_0_172,i_0_197,i_0_223,i_0_328,i_0_307,i_0_111,i_0_121,i_0_114,i_0_103,i_0_105,i_0_101])).
% 50.29/26.07 cnf(i_0_337, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_338, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_339, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_340, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_342, plain, (~orthogonal_lines(orthogonal_through_point(parallel_through_point(esk2_0,X1),X2),esk1_0)), inference(scs_inference,[],[i_0_327,i_0_121])).
% 50.29/26.07 cnf(i_0_343, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_344, plain, (unorthogonal_lines(parallel_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_220,i_0_197,i_0_327,i_0_121,i_0_114])).
% 50.29/26.07 cnf(i_0_345, plain, (convergent_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_220])).
% 50.29/26.07 cnf(i_0_346, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_347, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_348, plain, (~unorthogonal_lines(esk4_0,esk3_0)|convergent_lines(orthogonal_through_point(parallel_through_point(esk3_0,X1),X2),esk4_0)), inference(scs_inference,[],[i_0_150,i_0_220,i_0_197,i_0_223,i_0_327,i_0_121,i_0_114,i_0_103])).
% 50.29/26.07 cnf(i_0_349, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_350, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_351, plain, (convergent_lines(orthogonal_through_point(parallel_through_point(esk3_0,X1),X2),esk4_0)|~unorthogonal_lines(esk3_0,esk4_0)), inference(scs_inference,[],[i_0_150,i_0_220,i_0_197,i_0_223,i_0_327,i_0_121,i_0_114,i_0_103,i_0_155])).
% 50.29/26.07 cnf(i_0_352, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_353, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_100])).
% 50.29/26.07 cnf(i_0_354, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_355, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_356, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_357, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_358, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_360, plain, (~orthogonal_lines(parallel_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_344,i_0_121])).
% 50.29/26.07 cnf(i_0_361, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_362, plain, (unorthogonal_lines(X1,X1)), inference(scs_inference,[],[i_0_197,i_0_344,i_0_145,i_0_121,i_0_114])).
% 50.29/26.07 cnf(i_0_363, plain, (convergent_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_145])).
% 50.29/26.07 cnf(i_0_364, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_365, plain, (~unorthogonal_lines(esk2_0,esk1_0)|convergent_lines(orthogonal_through_point(parallel_through_point(esk1_0,X1),X2),esk2_0)), inference(scs_inference,[],[i_0_172,i_0_197,i_0_223,i_0_344,i_0_145,i_0_121,i_0_114,i_0_103])).
% 50.29/26.07 cnf(i_0_366, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_367, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_368, plain, (~unorthogonal_lines(esk4_0,esk3_0)|convergent_lines(esk4_0,orthogonal_through_point(esk3_0,X1))), inference(scs_inference,[],[i_0_150,i_0_172,i_0_197,i_0_223,i_0_344,i_0_145,i_0_121,i_0_114,i_0_103,i_0_105])).
% 50.29/26.07 cnf(i_0_369, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_370, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_105])).
% 50.29/26.07 cnf(i_0_371, plain, (~unorthogonal_lines(esk1_0,esk2_0)|unorthogonal_lines(esk1_0,esk2_0)), inference(scs_inference,[],[i_0_142,i_0_150,i_0_172,i_0_197,i_0_223,i_0_344,i_0_145,i_0_138,i_0_121,i_0_114,i_0_103,i_0_105,i_0_102])).
% 50.29/26.07 cnf(i_0_372, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_373, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_102])).
% 50.29/26.07 cnf(i_0_374, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_375, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_377, plain, (~orthogonal_lines(X1,X1)), inference(scs_inference,[],[i_0_362,i_0_121])).
% 50.29/26.07 cnf(i_0_378, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_379, plain, (~unorthogonal_lines(esk2_0,esk1_0)|convergent_lines(esk2_0,orthogonal_through_point(esk1_0,X1))), inference(scs_inference,[],[i_0_172,i_0_197,i_0_362,i_0_121,i_0_105])).
% 50.29/26.07 cnf(i_0_380, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_381, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_105])).
% 50.29/26.07 cnf(i_0_382, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_383, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_385, plain, (~unorthogonal_lines(esk2_0,esk1_0)|unorthogonal_lines(esk2_0,esk1_0)), inference(scs_inference,[],[i_0_172,i_0_138,i_0_102])).
% 50.29/26.07 cnf(i_0_386, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_387, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_102])).
% 50.29/26.07 cnf(i_0_388, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_389, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_390, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_391, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_392, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_197])).
% 50.29/26.07 cnf(i_0_394, plain, (unorthogonal_lines(orthogonal_through_point(esk2_0,X1),esk1_0)), inference(scs_inference,[],[i_0_110,i_0_172,i_0_114])).
% 50.29/26.07 cnf(i_0_395, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_396, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_397, plain, (~orthogonal_lines(orthogonal_through_point(esk2_0,X1),esk1_0)), inference(scs_inference,[],[i_0_110,i_0_172,i_0_114,i_0_121])).
% 50.29/26.07 cnf(i_0_398, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_399, plain, (~unorthogonal_lines(esk3_0,esk4_0)|convergent_lines(orthogonal_through_point(esk4_0,X1),esk3_0)), inference(scs_inference,[],[i_0_110,i_0_395,i_0_141,i_0_172,i_0_114,i_0_121,i_0_103])).
% 50.29/26.07 cnf(i_0_400, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_401, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_402, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_403, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_405, plain, (unorthogonal_lines(orthogonal_through_point(X1,X2),orthogonal_through_point(X1,X3))), inference(scs_inference,[],[i_0_110,i_0_194,i_0_114])).
% 50.29/26.07 cnf(i_0_406, plain, (convergent_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_194])).
% 50.29/26.07 cnf(i_0_407, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_408, plain, (~orthogonal_lines(orthogonal_through_point(X1,X2),orthogonal_through_point(X1,X3))), inference(scs_inference,[],[i_0_110,i_0_194,i_0_114,i_0_121])).
% 50.29/26.07 cnf(i_0_409, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_410, plain, (~unorthogonal_lines(esk1_0,esk2_0)|convergent_lines(orthogonal_through_point(esk2_0,X1),esk1_0)), inference(scs_inference,[],[i_0_110,i_0_142,i_0_194,i_0_114,i_0_121,i_0_103])).
% 50.29/26.07 cnf(i_0_411, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_412, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_413, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_414, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_416, plain, (unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(X1,X2),X3),X1)), inference(scs_inference,[],[i_0_110,i_0_145,i_0_114])).
% 50.29/26.07 cnf(i_0_417, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_418, plain, (~convergent_lines(X1,X2)|unorthogonal_lines(X3,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_114])).
% 50.29/26.07 cnf(i_0_419, plain, (~orthogonal_lines(orthogonal_through_point(orthogonal_through_point(X1,X2),X3),X1)), inference(scs_inference,[],[i_0_110,i_0_145,i_0_114,i_0_121])).
% 50.29/26.07 cnf(i_0_420, plain, (~unorthogonal_lines(X1,X2)|~orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_121])).
% 50.29/26.07 cnf(i_0_421, plain, (~unorthogonal_lines(esk4_0,esk3_0)|convergent_lines(orthogonal_through_point(esk3_0,X1),esk4_0)), inference(scs_inference,[],[i_0_110,i_0_417,i_0_150,i_0_145,i_0_114,i_0_121,i_0_103])).
% 50.29/26.07 cnf(i_0_422, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_423, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_425, plain, (~unorthogonal_lines(esk2_0,esk1_0)|convergent_lines(orthogonal_through_point(esk1_0,X1),esk2_0)), inference(scs_inference,[],[i_0_110,i_0_172,i_0_103])).
% 50.29/26.07 cnf(i_0_426, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_427, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_428, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_429, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_431, plain, (~unorthogonal_lines(esk1_0,esk2_0)|unorthogonal_lines(esk2_0,esk1_0)), inference(scs_inference,[],[i_0_138,i_0_142,i_0_101])).
% 50.29/26.07 cnf(i_0_432, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_433, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_434, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_435, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_437, plain, (~unorthogonal_lines(esk4_0,esk3_0)|unorthogonal_lines(esk3_0,esk4_0)), inference(scs_inference,[],[i_0_138,i_0_150,i_0_101])).
% 50.29/26.07 cnf(i_0_438, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_439, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_440, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_441, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_443, plain, (~unorthogonal_lines(esk2_0,esk1_0)|unorthogonal_lines(esk1_0,esk2_0)), inference(scs_inference,[],[i_0_138,i_0_172,i_0_101])).
% 50.29/26.07 cnf(i_0_444, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_445, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_446, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_112])).
% 50.29/26.07 cnf(i_0_447, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_223])).
% 50.29/26.07 cnf(i_0_449, plain, (~apart_point_and_line(intersection_point(esk1_0,esk2_0),esk4_0)), inference(scs_inference,[],[i_0_129,i_0_122])).
% 50.29/26.07 cnf(i_0_450, plain, (~incident_point_and_line(X1,X2)|~apart_point_and_line(X1,X2)), inference(rename_variables,[],[i_0_122])).
% 50.29/26.07 cnf(i_0_451, plain, (~distinct_lines(parallel_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_129,i_0_111,i_0_122,i_0_128])).
% 50.29/26.07 cnf(i_0_452, plain, (convergent_lines(X1,X2)|~distinct_lines(X1,X2)), inference(rename_variables,[],[i_0_128])).
% 50.29/26.07 cnf(i_0_453, plain, (incident_point_and_line(X1,parallel_through_point(X2,X1))), inference(scs_inference,[],[i_0_129,i_0_111,i_0_113,i_0_122,i_0_128,i_0_132])).
% 50.29/26.07 cnf(i_0_454, plain, (apart_point_and_line(X1,X2)|incident_point_and_line(X1,X2)), inference(rename_variables,[],[i_0_132])).
% 50.29/26.07 cnf(i_0_455, plain, (equal_lines(X1,X1)), inference(scs_inference,[],[i_0_129,i_0_139,i_0_111,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136])).
% 50.29/26.07 cnf(i_0_456, plain, (distinct_lines(X1,X2)|equal_lines(X1,X2)), inference(rename_variables,[],[i_0_136])).
% 50.29/26.07 cnf(i_0_457, plain, (equal_points(X1,X1)), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137])).
% 50.29/26.07 cnf(i_0_458, plain, (distinct_points(X1,X2)|equal_points(X1,X2)), inference(rename_variables,[],[i_0_137])).
% 50.29/26.07 cnf(i_0_459, plain, (~apart_point_and_line(intersection_point(esk2_0,esk1_0),esk2_0)), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_172,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94])).
% 50.29/26.07 cnf(i_0_460, plain, (~convergent_lines(X1,X2)|~apart_point_and_line(intersection_point(X1,X2),X1)), inference(rename_variables,[],[i_0_94])).
% 50.29/26.07 cnf(i_0_461, plain, (~apart_point_and_line(intersection_point(esk2_0,esk1_0),esk1_0)), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_172,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95])).
% 50.29/26.07 cnf(i_0_462, plain, (~convergent_lines(X1,X2)|~apart_point_and_line(intersection_point(X1,X2),X2)), inference(rename_variables,[],[i_0_95])).
% 50.29/26.07 cnf(i_0_463, plain, (parallel_lines(parallel_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_172,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95,i_0_133])).
% 50.29/26.07 cnf(i_0_464, plain, (convergent_lines(X1,X2)|parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_133])).
% 50.29/26.07 cnf(i_0_465, plain, (orthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_110,i_0_172,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95,i_0_133,i_0_131])).
% 50.29/26.07 cnf(i_0_466, plain, (unorthogonal_lines(X1,X2)|orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_131])).
% 50.29/26.07 cnf(i_0_467, plain, (~convergent_lines(X1,parallel_through_point(X1,X2))), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_110,i_0_172,i_0_138,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95,i_0_133,i_0_131,i_0_115])).
% 50.29/26.07 cnf(i_0_468, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_138])).
% 50.29/26.07 cnf(i_0_469, plain, (convergent_lines(X1,X2)|convergent_lines(X3,X2)|~convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_115])).
% 50.29/26.07 cnf(i_0_470, plain, (unorthogonal_lines(X1,parallel_through_point(X1,X2))), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_110,i_0_172,i_0_138,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95,i_0_133,i_0_131,i_0_115,i_0_135])).
% 50.29/26.07 cnf(i_0_471, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_135])).
% 50.29/26.07 cnf(i_0_472, plain, (~distinct_lines(X1,parallel_through_point(X1,X2))), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_110,i_0_172,i_0_138,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95,i_0_133,i_0_131,i_0_115,i_0_135,i_0_118])).
% 50.29/26.07 cnf(i_0_473, plain, (distinct_lines(X1,X2)|distinct_lines(X3,X2)|~distinct_lines(X3,X1)), inference(rename_variables,[],[i_0_118])).
% 50.29/26.07 cnf(i_0_474, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),parallel_through_point(X1,X3))|~convergent_lines(orthogonal_through_point(X1,X2),parallel_through_point(X1,X3))), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_110,i_0_172,i_0_138,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95,i_0_133,i_0_131,i_0_115,i_0_135,i_0_118,i_0_102])).
% 50.29/26.07 cnf(i_0_475, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_476, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X3,X2)|~unorthogonal_lines(X3,X1)|~convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_102])).
% 50.29/26.07 cnf(i_0_477, plain, (~apart_point_and_line(X1,X2)), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_110,i_0_172,i_0_138,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95,i_0_133,i_0_131,i_0_115,i_0_135,i_0_118,i_0_102,i_0_116])).
% 50.29/26.07 cnf(i_0_478, plain, (distinct_lines(X1,X2)|apart_point_and_line(X3,X2)|~apart_point_and_line(X3,X1)), inference(rename_variables,[],[i_0_116])).
% 50.29/26.07 cnf(i_0_479, plain, (~convergent_lines(parallel_through_point(X1,X2),parallel_through_point(X1,X3))), inference(scs_inference,[],[i_0_129,i_0_139,i_0_140,i_0_111,i_0_475,i_0_110,i_0_172,i_0_138,i_0_113,i_0_122,i_0_128,i_0_132,i_0_136,i_0_137,i_0_94,i_0_95,i_0_133,i_0_131,i_0_115,i_0_135,i_0_118,i_0_102,i_0_116,i_0_117])).
% 50.29/26.07 cnf(i_0_480, plain, (distinct_lines(X1,X2)|convergent_lines(X3,X2)|~convergent_lines(X3,X1)), inference(rename_variables,[],[i_0_117])).
% 50.29/26.07 cnf(i_0_481, plain, (unorthogonal_lines(X1,X1)), inference(rename_variables,[],[i_0_362])).
% 50.29/26.07 cnf(i_0_483, plain, (~distinct_lines(parallel_through_point(X1,X2),parallel_through_point(X1,X3))), inference(scs_inference,[],[i_0_479,i_0_128])).
% 50.29/26.07 cnf(i_0_484, plain, (convergent_lines(X1,X2)|~distinct_lines(X1,X2)), inference(rename_variables,[],[i_0_128])).
% 50.29/26.07 cnf(i_0_485, plain, (incident_point_and_line(X1,X2)), inference(scs_inference,[],[i_0_477,i_0_479,i_0_128,i_0_132])).
% 50.29/26.07 cnf(i_0_486, plain, (apart_point_and_line(X1,X2)|incident_point_and_line(X1,X2)), inference(rename_variables,[],[i_0_132])).
% 50.29/26.07 cnf(i_0_487, plain, (equal_lines(parallel_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_477,i_0_451,i_0_479,i_0_128,i_0_132,i_0_136])).
% 50.29/26.07 cnf(i_0_488, plain, (distinct_lines(X1,X2)|equal_lines(X1,X2)), inference(rename_variables,[],[i_0_136])).
% 50.29/26.07 cnf(i_0_489, plain, (parallel_lines(X1,parallel_through_point(X1,X2))), inference(scs_inference,[],[i_0_477,i_0_451,i_0_467,i_0_479,i_0_128,i_0_132,i_0_136,i_0_133])).
% 50.29/26.07 cnf(i_0_490, plain, (convergent_lines(X1,X2)|parallel_lines(X1,X2)), inference(rename_variables,[],[i_0_133])).
% 50.29/26.07 cnf(i_0_491, plain, (orthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(scs_inference,[],[i_0_477,i_0_451,i_0_467,i_0_479,i_0_197,i_0_128,i_0_132,i_0_136,i_0_133,i_0_131])).
% 50.29/26.07 cnf(i_0_492, plain, (unorthogonal_lines(X1,X2)|orthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_131])).
% 50.29/26.07 cnf(i_0_493, plain, (unorthogonal_lines(parallel_through_point(X1,X2),parallel_through_point(X1,X3))), inference(scs_inference,[],[i_0_477,i_0_451,i_0_467,i_0_479,i_0_197,i_0_128,i_0_132,i_0_136,i_0_133,i_0_131,i_0_135])).
% 50.29/26.07 cnf(i_0_494, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X1,X2)), inference(rename_variables,[],[i_0_135])).
% 50.29/26.07 cnf(i_0_495, plain, (~incident_point_and_line(intersection_point(esk3_0,esk4_0),esk1_0)), inference(scs_inference,[],[i_0_477,i_0_451,i_0_467,i_0_479,i_0_197,i_0_128,i_0_132,i_0_136,i_0_133,i_0_131,i_0_135,i_0_93])).
% 50.29/26.07 cnf(i_0_496, plain, (~convergent_lines(orthogonal_through_point(esk2_0,X1),esk1_0)|convergent_lines(orthogonal_through_point(esk1_0,X2),orthogonal_through_point(esk2_0,X1))), inference(scs_inference,[],[i_0_477,i_0_451,i_0_467,i_0_479,i_0_394,i_0_110,i_0_197,i_0_128,i_0_132,i_0_136,i_0_133,i_0_131,i_0_135,i_0_93,i_0_103])).
% 50.29/26.07 cnf(i_0_497, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_110])).
% 50.29/26.07 cnf(i_0_498, plain, (~unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|convergent_lines(X3,X1)|~convergent_lines(X1,X2)), inference(rename_variables,[],[i_0_103])).
% 50.29/26.07 cnf(i_0_499, plain, (~convergent_lines(orthogonal_through_point(esk2_0,X1),esk1_0)|unorthogonal_lines(parallel_through_point(esk1_0,X2),orthogonal_through_point(esk2_0,X1))), inference(scs_inference,[],[i_0_477,i_0_451,i_0_467,i_0_479,i_0_394,i_0_110,i_0_197,i_0_111,i_0_128,i_0_132,i_0_136,i_0_133,i_0_131,i_0_135,i_0_93,i_0_103,i_0_101])).
% 50.29/26.07 cnf(i_0_500, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_111])).
% 50.29/26.07 cnf(i_0_501, plain, (~unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|unorthogonal_lines(X3,X1)|~convergent_lines(X1,X2)), inference(rename_variables,[],[i_0_101])).
% 50.29/26.07 cnf(i_0_502,plain, ($false), inference(scs_inference,[],[i_0+485, i_0_495]), ['proof']).
% 50.29/26.07 % SZS output end CNFRefutation
% 50.29/26.07 % Total time : 25.324s
%------------------------------------------------------------------------------