%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GEO222+2 : TPTP v9.2.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:20:00 PM UTC 2026
% Result : Theorem 0.46s 1.62s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO222+2 : TPTP v9.2.1. Released v3.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n025.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 17:48:43 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.35 % start to proof: theBenchmark
% 0.46/1.62 % Version : CSE_E---1.7
% 0.46/1.62 % Problem : theBenchmark.p
% 0.46/1.62 % SZS status Theorem for theBenchmark.p
% 0.46/1.62 % SZS output start CNFRefutation
% 0.46/1.62 fof(con, conjecture, ![X9, X6]:~(convergent_lines(X6,orthogonal_through_point(orthogonal_through_point(X6,X9),X9))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', con)).
% 0.46/1.62 fof(ooc1, axiom, ![X9, X6]:~(unorthogonal_lines(orthogonal_through_point(X6,X9),X6)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', ooc1)).
% 0.46/1.62 fof(cp1, axiom, ![X1, X2]:~(convergent_lines(parallel_through_point(X2,X1),X2)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+2.ax', cp1)).
% 0.46/1.62 fof(ooc2, axiom, ![X9, X6]:~(apart_point_and_line(X9,orthogonal_through_point(X6,X9))), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', ooc2)).
% 0.46/1.62 fof(cp2, axiom, ![X1, X2]:~(apart_point_and_line(X1,parallel_through_point(X2,X1))), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+2.ax', cp2)).
% 0.46/1.62 fof(apart3, axiom, ![X1]:~(convergent_lines(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', apart3)).
% 0.46/1.62 fof(apart2, axiom, ![X1]:~(distinct_lines(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', apart2)).
% 0.46/1.62 fof(apart1, axiom, ![X1]:~(distinct_points(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', apart1)).
% 0.46/1.62 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/sandbox/benchmark/Axioms/GEO008+0.ax', cu1)).
% 0.46/1.62 fof(con1, axiom, ![X1, X2, X3]:(distinct_points(X1,X2)=>(apart_point_and_line(X3,line_connecting(X1,X2))=>(distinct_points(X3,X1)&distinct_points(X3,X2)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', con1)).
% 0.46/1.62 fof(con2, axiom, ![X1, X2, X3]:(convergent_lines(X1,X2)=>((apart_point_and_line(X3,X1)|apart_point_and_line(X3,X2))=>distinct_points(X3,intersection_point(X1,X2)))), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', con2)).
% 0.46/1.62 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/sandbox/benchmark/Axioms/GEO006+3.ax', ouo1)).
% 0.46/1.62 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/sandbox/benchmark/Axioms/GEO006+3.ax', oac1)).
% 0.46/1.62 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/sandbox/benchmark/Axioms/GEO006+2.ax', cup1)).
% 0.46/1.62 fof(apart6, axiom, ![X1, X2, X3]:(convergent_lines(X1,X2)=>(convergent_lines(X1,X3)|convergent_lines(X2,X3))), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', apart6)).
% 0.46/1.62 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/sandbox/benchmark/Axioms/GEO008+0.ax', ceq2)).
% 0.46/1.62 fof(apart5, axiom, ![X1, X2, X3]:(distinct_lines(X1,X2)=>(distinct_lines(X1,X3)|distinct_lines(X2,X3))), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', apart5)).
% 0.46/1.62 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/sandbox/benchmark/Axioms/GEO008+0.ax', ceq1)).
% 0.46/1.62 fof(apart4, axiom, ![X1, X2, X3]:(distinct_points(X1,X2)=>(distinct_points(X1,X3)|distinct_points(X2,X3))), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', apart4)).
% 0.46/1.62 fof(ceq3, axiom, ![X1, X2]:(convergent_lines(X1,X2)=>distinct_lines(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/GEO008+0.ax', ceq3)).
% 0.46/1.62 fof(occu1, axiom, ![X6, X7]:(convergent_lines(X6,X7)|unorthogonal_lines(X6,X7)), file('/export/starexec/sandbox/benchmark/Axioms/GEO006+3.ax', occu1)).
% 0.46/1.62 fof(i_0_21, negated_conjecture, ~(![X9, X6]:~convergent_lines(X6,orthogonal_through_point(orthogonal_through_point(X6,X9),X9))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[con])])).
% 0.46/1.62 fof(i_0_22, plain, ![X9, X6]:~unorthogonal_lines(orthogonal_through_point(X6,X9),X6), inference(fof_simplification,[status(thm)],[ooc1])).
% 0.46/1.62 fof(i_0_23, plain, ![X1, X2]:~convergent_lines(parallel_through_point(X2,X1),X2), inference(fof_simplification,[status(thm)],[cp1])).
% 0.46/1.62 fof(i_0_24, plain, ![X9, X6]:~apart_point_and_line(X9,orthogonal_through_point(X6,X9)), inference(fof_simplification,[status(thm)],[ooc2])).
% 0.46/1.62 fof(i_0_25, plain, ![X1, X2]:~apart_point_and_line(X1,parallel_through_point(X2,X1)), inference(fof_simplification,[status(thm)],[cp2])).
% 0.46/1.62 fof(i_0_26, plain, ![X1]:~convergent_lines(X1,X1), inference(fof_simplification,[status(thm)],[apart3])).
% 0.46/1.62 fof(i_0_27, plain, ![X1]:~distinct_lines(X1,X1), inference(fof_simplification,[status(thm)],[apart2])).
% 0.46/1.62 fof(i_0_28, plain, ![X1]:~distinct_points(X1,X1), inference(fof_simplification,[status(thm)],[apart1])).
% 0.46/1.62 fof(i_0_29, plain, ![X80, X81, X82, X83]:(~distinct_points(X80,X81)|~distinct_lines(X82,X83)|(apart_point_and_line(X80,X82)|apart_point_and_line(X80,X83)|apart_point_and_line(X81,X82)|apart_point_and_line(X81,X83))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cu1])])).
% 0.46/1.62 fof(i_0_30, plain, ![X74, X75, X76]:((distinct_points(X76,X74)|~apart_point_and_line(X76,line_connecting(X74,X75))|~distinct_points(X74,X75))&(distinct_points(X76,X75)|~apart_point_and_line(X76,line_connecting(X74,X75))|~distinct_points(X74,X75))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[con1])])])).
% 0.46/1.62 fof(i_0_31, plain, ![X77, X78, X79]:((~apart_point_and_line(X79,X77)|distinct_points(X79,intersection_point(X77,X78))|~convergent_lines(X77,X78))&(~apart_point_and_line(X79,X78)|distinct_points(X79,intersection_point(X77,X78))|~convergent_lines(X77,X78))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[con2])])])).
% 0.46/1.62 fof(i_0_32, plain, ![X108, X109, X110, X111]:(~distinct_lines(X109,X110)|(apart_point_and_line(X108,X109)|apart_point_and_line(X108,X110)|unorthogonal_lines(X109,X111)|unorthogonal_lines(X110,X111))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ouo1])])).
% 0.46/1.62 fof(i_0_33, negated_conjecture, convergent_lines(esk2_0,orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_21])])])).
% 0.46/1.62 fof(i_0_34, plain, ![X101, X102, X103]:(((convergent_lines(X102,X103)|convergent_lines(X101,X103)|(~convergent_lines(X101,X102)|~unorthogonal_lines(X101,X102)))&(unorthogonal_lines(X102,X103)|convergent_lines(X101,X103)|(~convergent_lines(X101,X102)|~unorthogonal_lines(X101,X102))))&((convergent_lines(X102,X103)|unorthogonal_lines(X101,X103)|(~convergent_lines(X101,X102)|~unorthogonal_lines(X101,X102)))&(unorthogonal_lines(X102,X103)|unorthogonal_lines(X101,X103)|(~convergent_lines(X101,X102)|~unorthogonal_lines(X101,X102))))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oac1])])])).
% 0.46/1.62 fof(i_0_35, plain, ![X96, X97, X98]:(~distinct_lines(X97,X98)|(apart_point_and_line(X96,X97)|apart_point_and_line(X96,X98)|convergent_lines(X97,X98))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cup1])])).
% 0.46/1.62 fof(i_0_36, plain, ![X104, X105]:~unorthogonal_lines(orthogonal_through_point(X105,X104),X105), inference(variable_rename,[status(thm)],[i_0_22])).
% 0.46/1.62 fof(i_0_37, plain, ![X92, X93]:~convergent_lines(parallel_through_point(X93,X92),X93), inference(variable_rename,[status(thm)],[i_0_23])).
% 0.46/1.62 fof(i_0_38, plain, ![X106, X107]:~apart_point_and_line(X106,orthogonal_through_point(X107,X106)), inference(variable_rename,[status(thm)],[i_0_24])).
% 0.46/1.62 fof(i_0_39, plain, ![X94, X95]:~apart_point_and_line(X94,parallel_through_point(X95,X94)), inference(variable_rename,[status(thm)],[i_0_25])).
% 0.46/1.62 fof(i_0_40, plain, ![X71, X72, X73]:(~convergent_lines(X71,X72)|(convergent_lines(X71,X73)|convergent_lines(X72,X73))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[apart6])])).
% 0.46/1.62 fof(i_0_41, plain, ![X87, X88, X89]:(~apart_point_and_line(X87,X88)|(distinct_lines(X88,X89)|apart_point_and_line(X87,X89))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ceq2])])).
% 0.46/1.62 fof(i_0_42, plain, ![X68, X69, X70]:(~distinct_lines(X68,X69)|(distinct_lines(X68,X70)|distinct_lines(X69,X70))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[apart5])])).
% 0.46/1.62 fof(i_0_43, plain, ![X84, X85, X86]:(~apart_point_and_line(X84,X85)|(distinct_points(X84,X86)|apart_point_and_line(X86,X85))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ceq1])])).
% 0.46/1.62 fof(i_0_44, plain, ![X65, X66, X67]:(~distinct_points(X65,X66)|(distinct_points(X65,X67)|distinct_points(X66,X67))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[apart4])])).
% 0.46/1.62 fof(i_0_45, plain, ![X90, X91]:(~convergent_lines(X90,X91)|distinct_lines(X90,X91)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ceq3])])).
% 0.46/1.62 fof(i_0_46, plain, ![X99, X100]:(convergent_lines(X99,X100)|unorthogonal_lines(X99,X100)), inference(variable_rename,[status(thm)],[occu1])).
% 0.46/1.62 fof(i_0_47, plain, ![X64]:~convergent_lines(X64,X64), inference(variable_rename,[status(thm)],[i_0_26])).
% 0.46/1.62 fof(i_0_48, plain, ![X63]:~distinct_lines(X63,X63), inference(variable_rename,[status(thm)],[i_0_27])).
% 0.46/1.62 fof(i_0_49, plain, ![X62]:~distinct_points(X62,X62), inference(variable_rename,[status(thm)],[i_0_28])).
% 0.46/1.62 cnf(i_0_50, 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_29]), ['final']).
% 0.46/1.62 cnf(i_0_51, plain, (distinct_points(X1,X2)|~apart_point_and_line(X1,line_connecting(X2,X3))|~distinct_points(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_30]), ['final']).
% 0.46/1.62 cnf(i_0_52, plain, (distinct_points(X1,X2)|~apart_point_and_line(X1,line_connecting(X3,X2))|~distinct_points(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_30]), ['final']).
% 0.46/1.62 cnf(i_0_53, plain, (distinct_points(X1,intersection_point(X2,X3))|~apart_point_and_line(X1,X2)|~convergent_lines(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_31]), ['final']).
% 0.46/1.62 cnf(i_0_54, plain, (distinct_points(X1,intersection_point(X3,X2))|~apart_point_and_line(X1,X2)|~convergent_lines(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_31]), ['final']).
% 0.46/1.62 cnf(i_0_55, 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_32]), ['final']).
% 0.46/1.62 cnf(i_0_56, negated_conjecture, (convergent_lines(esk2_0,orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0))), inference(split_conjunct,[status(thm)],[i_0_33]), ['final']).
% 0.46/1.62 cnf(i_0_57, plain, (unorthogonal_lines(X1,X2)|unorthogonal_lines(X3,X2)|~convergent_lines(X3,X1)|~unorthogonal_lines(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_34]), ['final']).
% 0.46/1.62 cnf(i_0_58, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X3,X2)|~convergent_lines(X3,X1)|~unorthogonal_lines(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_34]), ['final']).
% 0.46/1.62 cnf(i_0_59, plain, (unorthogonal_lines(X1,X2)|convergent_lines(X3,X2)|~convergent_lines(X3,X1)|~unorthogonal_lines(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_34]), ['final']).
% 0.46/1.62 cnf(i_0_60, plain, (convergent_lines(X1,X2)|convergent_lines(X3,X2)|~convergent_lines(X3,X1)|~unorthogonal_lines(X3,X1)), inference(split_conjunct,[status(thm)],[i_0_34]), ['final']).
% 0.46/1.62 cnf(i_0_61, 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_35]), ['final']).
% 0.46/1.62 cnf(i_0_62, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_36]), ['final']).
% 0.46/1.62 cnf(i_0_63, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_37]), ['final']).
% 0.46/1.62 cnf(i_0_64, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(split_conjunct,[status(thm)],[i_0_38]), ['final']).
% 0.46/1.62 cnf(i_0_65, plain, (~apart_point_and_line(X1,parallel_through_point(X2,X1))), inference(split_conjunct,[status(thm)],[i_0_39]), ['final']).
% 0.46/1.62 cnf(i_0_66, plain, (convergent_lines(X1,X3)|convergent_lines(X2,X3)|~convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_40]), ['final']).
% 0.46/1.62 cnf(i_0_67, plain, (distinct_lines(X2,X3)|apart_point_and_line(X1,X3)|~apart_point_and_line(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_41]), ['final']).
% 0.46/1.62 cnf(i_0_68, plain, (distinct_lines(X1,X3)|distinct_lines(X2,X3)|~distinct_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_42]), ['final']).
% 0.46/1.62 cnf(i_0_69, plain, (distinct_points(X1,X3)|apart_point_and_line(X3,X2)|~apart_point_and_line(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.46/1.62 cnf(i_0_70, plain, (distinct_points(X1,X3)|distinct_points(X2,X3)|~distinct_points(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.46/1.62 cnf(i_0_71, plain, (distinct_lines(X1,X2)|~convergent_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_45]), ['final']).
% 0.46/1.62 cnf(i_0_72, plain, (convergent_lines(X1,X2)|unorthogonal_lines(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_46]), ['final']).
% 0.46/1.62 cnf(i_0_73, plain, (~convergent_lines(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_47]), ['final']).
% 0.46/1.62 cnf(i_0_74, plain, (~distinct_lines(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_48]), ['final']).
% 0.46/1.62 cnf(i_0_75, plain, (~distinct_points(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_49]), ['final']).
% 0.56/1.77 cnf(i_0_76, plain, (distinct_lines(esk2_0,orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0))), inference(scs_inference,[],[i_0_56,i_0_71])).
% 0.56/1.77 cnf(i_0_77, plain, (~convergent_lines(X1,X2)|distinct_lines(X1,X2)), inference(rename_variables,[],[i_0_71])).
% 0.56/1.77 cnf(i_0_78, plain, (convergent_lines(orthogonal_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_56,i_0_62,i_0_71,i_0_72])).
% 0.56/1.77 cnf(i_0_79, plain, (unorthogonal_lines(X1,X2)|convergent_lines(X1,X2)), inference(rename_variables,[],[i_0_72])).
% 0.56/1.77 cnf(i_0_80, plain, (convergent_lines(orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0),esk2_0)), inference(scs_inference,[],[i_0_56,i_0_73,i_0_62,i_0_71,i_0_72,i_0_66])).
% 0.56/1.77 cnf(i_0_81, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_73])).
% 0.56/1.77 cnf(i_0_82, plain, (~convergent_lines(X1,X2)|convergent_lines(X1,X3)|convergent_lines(X2,X3)), inference(rename_variables,[],[i_0_66])).
% 0.56/1.77 cnf(i_0_83, plain, (distinct_lines(orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0),esk2_0)), inference(scs_inference,[],[i_0_56,i_0_73,i_0_74,i_0_62,i_0_71,i_0_72,i_0_66,i_0_68])).
% 0.56/1.77 cnf(i_0_84, plain, (~distinct_lines(X1,X1)), inference(rename_variables,[],[i_0_74])).
% 0.56/1.77 cnf(i_0_85, plain, (~distinct_lines(X1,X2)|distinct_lines(X1,X3)|distinct_lines(X2,X3)), inference(rename_variables,[],[i_0_68])).
% 0.56/1.77 cnf(i_0_86, plain, (~distinct_lines(parallel_through_point(orthogonal_through_point(X1,X2),X2),orthogonal_through_point(X1,X2))), inference(scs_inference,[],[i_0_56,i_0_73,i_0_74,i_0_62,i_0_63,i_0_64,i_0_65,i_0_71,i_0_72,i_0_66,i_0_68,i_0_61])).
% 0.56/1.77 cnf(i_0_87, plain, (~convergent_lines(parallel_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_63])).
% 0.56/1.77 cnf(i_0_88, plain, (~apart_point_and_line(X1,parallel_through_point(X2,X1))), inference(rename_variables,[],[i_0_65])).
% 0.56/1.77 cnf(i_0_89, plain, (convergent_lines(X1,X2)|~distinct_lines(X1,X2)|apart_point_and_line(X3,X1)|apart_point_and_line(X3,X2)), inference(rename_variables,[],[i_0_61])).
% 0.56/1.77 cnf(i_0_90, plain, (~unorthogonal_lines(esk2_0,orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0))|unorthogonal_lines(esk2_0,orthogonal_through_point(esk2_0,esk1_0))), inference(scs_inference,[],[i_0_56,i_0_73,i_0_74,i_0_62,i_0_63,i_0_64,i_0_65,i_0_71,i_0_72,i_0_66,i_0_68,i_0_61,i_0_57])).
% 0.56/1.77 cnf(i_0_91, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_62])).
% 0.56/1.77 cnf(i_0_92, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_57])).
% 0.56/1.77 cnf(i_0_93, plain, (~unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0),esk2_0)|unorthogonal_lines(esk2_0,orthogonal_through_point(esk2_0,esk1_0))), inference(scs_inference,[],[i_0_56,i_0_73,i_0_81,i_0_74,i_0_62,i_0_63,i_0_64,i_0_65,i_0_71,i_0_72,i_0_66,i_0_68,i_0_61,i_0_57,i_0_59])).
% 0.56/1.77 cnf(i_0_94, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_73])).
% 0.56/1.77 cnf(i_0_95, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_59])).
% 0.56/1.77 cnf(i_0_96, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_62])).
% 0.56/1.77 cnf(i_0_97, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_62])).
% 0.56/1.77 cnf(i_0_98, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_64])).
% 0.56/1.77 cnf(i_0_99, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_64])).
% 0.56/1.77 cnf(i_0_101, plain, (distinct_lines(orthogonal_through_point(X1,X2),X1)), inference(scs_inference,[],[i_0_78,i_0_71])).
% 0.56/1.77 cnf(i_0_102, plain, (~convergent_lines(X1,X2)|distinct_lines(X1,X2)), inference(rename_variables,[],[i_0_71])).
% 0.56/1.77 cnf(i_0_103, plain, (distinct_lines(X1,orthogonal_through_point(X1,X2))), inference(scs_inference,[],[i_0_78,i_0_74,i_0_71,i_0_68])).
% 0.56/1.77 cnf(i_0_104, plain, (~distinct_lines(X1,X1)), inference(rename_variables,[],[i_0_74])).
% 0.56/1.77 cnf(i_0_105, plain, (~distinct_lines(X1,X2)|distinct_lines(X1,X3)|distinct_lines(X2,X3)), inference(rename_variables,[],[i_0_68])).
% 0.56/1.77 cnf(i_0_106, plain, (convergent_lines(X1,orthogonal_through_point(X1,X2))), inference(scs_inference,[],[i_0_78,i_0_73,i_0_74,i_0_71,i_0_68,i_0_66])).
% 0.56/1.77 cnf(i_0_107, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_73])).
% 0.56/1.77 cnf(i_0_108, plain, (~convergent_lines(X1,X2)|convergent_lines(X1,X3)|convergent_lines(X2,X3)), inference(rename_variables,[],[i_0_66])).
% 0.56/1.77 cnf(i_0_109, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(scs_inference,[],[i_0_78,i_0_73,i_0_107,i_0_74,i_0_62,i_0_71,i_0_68,i_0_66,i_0_59])).
% 0.56/1.77 cnf(i_0_110, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_62])).
% 0.56/1.77 cnf(i_0_111, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_59])).
% 0.56/1.77 cnf(i_0_112, plain, (apart_point_and_line(esk1_0,esk2_0)), inference(scs_inference,[],[i_0_76,i_0_78,i_0_73,i_0_107,i_0_74,i_0_62,i_0_110,i_0_64,i_0_71,i_0_68,i_0_66,i_0_59,i_0_55])).
% 0.56/1.77 cnf(i_0_113, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_62])).
% 0.56/1.77 cnf(i_0_114, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_64])).
% 0.56/1.77 cnf(i_0_115, plain, (unorthogonal_lines(X1,X2)|~distinct_lines(X3,X1)|apart_point_and_line(X4,X3)|apart_point_and_line(X4,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_55])).
% 0.56/1.77 cnf(i_0_116, plain, (~unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0),esk2_0)|unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0),esk2_0)), inference(scs_inference,[],[i_0_76,i_0_80,i_0_78,i_0_73,i_0_107,i_0_74,i_0_62,i_0_110,i_0_64,i_0_71,i_0_68,i_0_66,i_0_59,i_0_55,i_0_58])).
% 0.56/1.77 cnf(i_0_117, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_73])).
% 0.56/1.77 cnf(i_0_118, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_58])).
% 0.56/1.77 cnf(i_0_119, plain, (~unorthogonal_lines(esk2_0,orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0))|unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0),esk2_0)), inference(scs_inference,[],[i_0_56,i_0_76,i_0_80,i_0_78,i_0_73,i_0_107,i_0_74,i_0_62,i_0_110,i_0_113,i_0_64,i_0_71,i_0_68,i_0_66,i_0_59,i_0_55,i_0_58,i_0_57])).
% 0.56/1.77 cnf(i_0_120, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_62])).
% 0.56/1.77 cnf(i_0_121, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_57])).
% 0.56/1.77 cnf(i_0_123, plain, (~unorthogonal_lines(esk2_0,orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0))), inference(scs_inference,[],[i_0_109,i_0_90])).
% 0.56/1.77 cnf(i_0_124, plain, (~unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0),esk2_0)), inference(scs_inference,[],[i_0_109,i_0_93])).
% 0.56/1.77 cnf(i_0_125, plain, (convergent_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(scs_inference,[],[i_0_106,i_0_63,i_0_66])).
% 0.56/1.77 cnf(i_0_126, plain, (convergent_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_106])).
% 0.56/1.77 cnf(i_0_127, plain, (~convergent_lines(X1,X2)|convergent_lines(X1,X3)|convergent_lines(X2,X3)), inference(rename_variables,[],[i_0_66])).
% 0.56/1.77 cnf(i_0_128, plain, (unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X2),orthogonal_through_point(parallel_through_point(X1,X2),X3))), inference(scs_inference,[],[i_0_101,i_0_106,i_0_109,i_0_63,i_0_64,i_0_65,i_0_66,i_0_55])).
% 0.56/1.77 cnf(i_0_129, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_109])).
% 0.56/1.77 cnf(i_0_130, plain, (distinct_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_101])).
% 0.56/1.77 cnf(i_0_131, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_64])).
% 0.56/1.77 cnf(i_0_132, plain, (unorthogonal_lines(X1,X2)|~distinct_lines(X3,X1)|apart_point_and_line(X4,X3)|apart_point_and_line(X4,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_55])).
% 0.56/1.77 cnf(i_0_133, plain, (distinct_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(scs_inference,[],[i_0_101,i_0_106,i_0_109,i_0_63,i_0_64,i_0_65,i_0_66,i_0_55,i_0_71])).
% 0.56/1.77 cnf(i_0_134, plain, (~convergent_lines(X1,X2)|distinct_lines(X1,X2)), inference(rename_variables,[],[i_0_71])).
% 0.56/1.77 cnf(i_0_135, plain, (distinct_lines(X1,orthogonal_through_point(parallel_through_point(X1,X2),X3))), inference(scs_inference,[],[i_0_101,i_0_106,i_0_109,i_0_63,i_0_74,i_0_64,i_0_65,i_0_66,i_0_55,i_0_71,i_0_68])).
% 0.56/1.77 cnf(i_0_136, plain, (~distinct_lines(X1,X1)), inference(rename_variables,[],[i_0_74])).
% 0.56/1.77 cnf(i_0_137, plain, (~distinct_lines(X1,X2)|distinct_lines(X1,X3)|distinct_lines(X2,X3)), inference(rename_variables,[],[i_0_68])).
% 0.56/1.77 cnf(i_0_138, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)|unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(scs_inference,[],[i_0_101,i_0_106,i_0_109,i_0_63,i_0_73,i_0_74,i_0_64,i_0_65,i_0_66,i_0_55,i_0_71,i_0_68,i_0_58])).
% 0.56/1.77 cnf(i_0_139, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_58])).
% 0.56/1.77 cnf(i_0_140, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_109])).
% 0.56/1.77 cnf(i_0_141, plain, (~unorthogonal_lines(X1,orthogonal_through_point(X1,X2))), inference(rename_variables,[],[i_0_109])).
% 0.56/1.77 cnf(i_0_142, plain, (distinct_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_101])).
% 0.56/1.77 cnf(i_0_144, plain, (~unorthogonal_lines(orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0),esk2_0)), inference(scs_inference,[],[i_0_124,i_0_116])).
% 0.56/1.77 cnf(i_0_145, plain, (~unorthogonal_lines(esk2_0,orthogonal_through_point(orthogonal_through_point(esk2_0,esk1_0),esk1_0))), inference(scs_inference,[],[i_0_124,i_0_119])).
% 0.56/1.77 cnf(i_0_146, plain, (convergent_lines(X1,orthogonal_through_point(parallel_through_point(X1,X2),X3))), inference(scs_inference,[],[i_0_125,i_0_73,i_0_66])).
% 0.56/1.77 cnf(i_0_147, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_73])).
% 0.56/1.77 cnf(i_0_148, plain, (~convergent_lines(X1,X2)|convergent_lines(X1,X3)|convergent_lines(X2,X3)), inference(rename_variables,[],[i_0_66])).
% 0.56/1.77 cnf(i_0_149, plain, (~unorthogonal_lines(X1,orthogonal_through_point(parallel_through_point(X1,X2),X3))|unorthogonal_lines(X1,orthogonal_through_point(parallel_through_point(X1,X2),X3))), inference(scs_inference,[],[i_0_125,i_0_73,i_0_147,i_0_66,i_0_58])).
% 0.56/1.77 cnf(i_0_150, plain, (~convergent_lines(X1,X1)), inference(rename_variables,[],[i_0_73])).
% 0.56/1.77 cnf(i_0_151, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|convergent_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_58])).
% 0.56/1.77 cnf(i_0_152, plain, (convergent_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_125])).
% 0.56/1.77 cnf(i_0_153, plain, (distinct_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_133])).
% 0.56/1.77 cnf(i_0_154, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_64])).
% 0.56/1.77 cnf(i_0_155, plain, (distinct_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_133])).
% 0.56/1.77 cnf(i_0_156, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_64])).
% 0.56/1.77 cnf(i_0_157, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_64])).
% 0.56/1.77 cnf(i_0_159, plain, (apart_point_and_line(esk1_0,orthogonal_through_point(esk2_0,esk1_0))), inference(scs_inference,[],[i_0_101,i_0_124,i_0_62,i_0_64,i_0_55])).
% 0.56/1.77 cnf(i_0_160, plain, (~unorthogonal_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_62])).
% 0.56/1.77 cnf(i_0_161, plain, (distinct_lines(orthogonal_through_point(X1,X2),X1)), inference(rename_variables,[],[i_0_101])).
% 0.56/1.77 cnf(i_0_162, plain, (~apart_point_and_line(X1,orthogonal_through_point(X2,X1))), inference(rename_variables,[],[i_0_64])).
% 0.56/1.77 cnf(i_0_163, plain, (unorthogonal_lines(X1,X2)|~distinct_lines(X3,X1)|apart_point_and_line(X4,X3)|apart_point_and_line(X4,X1)|unorthogonal_lines(X3,X2)), inference(rename_variables,[],[i_0_55])).
% 0.56/1.77 cnf(i_0_164, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)|convergent_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),orthogonal_through_point(X1,X4))), inference(scs_inference,[],[i_0_101,i_0_109,i_0_124,i_0_125,i_0_62,i_0_64,i_0_55,i_0_59])).
% 0.56/1.77 cnf(i_0_165, plain, (convergent_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_125])).
% 0.56/1.77 cnf(i_0_166, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|convergent_lines(X1,X3)), inference(rename_variables,[],[i_0_59])).
% 0.56/1.77 cnf(i_0_167, plain, (~unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)|unorthogonal_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),orthogonal_through_point(X1,X4))), inference(scs_inference,[],[i_0_101,i_0_109,i_0_124,i_0_125,i_0_165,i_0_62,i_0_64,i_0_55,i_0_59,i_0_57])).
% 0.56/1.77 cnf(i_0_168, plain, (convergent_lines(orthogonal_through_point(parallel_through_point(X1,X2),X3),X1)), inference(rename_variables,[],[i_0_125])).
% 0.56/1.77 cnf(i_0_169, plain, (~convergent_lines(X1,X2)|~unorthogonal_lines(X1,X2)|unorthogonal_lines(X2,X3)|unorthogonal_lines(X1,X3)), inference(rename_variables,[],[i_0_57])).
% 0.56/1.77 cnf(i_0_170,plain, ($false), inference(scs_inference,[],[i_0+159, i_0_64]), ['proof']).
% 0.56/1.77 % SZS output end CNFRefutation
% 0.56/1.77 % Total time : 1.272s
%------------------------------------------------------------------------------