%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GEO222+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 03:48:55 EDT 2022 % Result : Theorem 8.00s 2.54s % Output : Proof 23.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GEO222+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jun 17 20:22:12 EDT 2022 % 0.13/0.34 % CPUTime : % 0.57/0.59 ____ _ % 0.57/0.59 ___ / __ \_____(_)___ ________ __________ % 0.57/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.57/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.57/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.57/0.59 % 0.57/0.59 A Theorem Prover for First-Order Logic % 0.57/0.59 (ePrincess v.1.0) % 0.57/0.59 % 0.57/0.59 (c) Philipp Rümmer, 2009-2015 % 0.57/0.59 (c) Peter Backeman, 2014-2015 % 0.57/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.57/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.57/0.59 Bug reports to peter@backeman.se % 0.57/0.59 % 0.57/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.57/0.59 % 0.57/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.74/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.79/0.97 Prover 0: Preprocessing ... % 2.29/1.19 Prover 0: Warning: ignoring some quantifiers % 2.38/1.22 Prover 0: Constructing countermodel ... % 3.50/1.50 Prover 0: gave up % 3.50/1.50 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 3.64/1.54 Prover 1: Preprocessing ... % 3.99/1.65 Prover 1: Constructing countermodel ... % 3.99/1.67 Prover 1: gave up % 3.99/1.67 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 4.27/1.69 Prover 2: Preprocessing ... % 4.95/1.86 Prover 2: Warning: ignoring some quantifiers % 4.95/1.87 Prover 2: Constructing countermodel ... % 8.00/2.54 Prover 2: proved (873ms) % 8.00/2.54 % 8.00/2.54 No countermodel exists, formula is valid % 8.00/2.54 % SZS status Theorem for theBenchmark % 8.00/2.54 % 8.00/2.54 Generating proof ... Warning: ignoring some quantifiers % 22.56/6.21 found it (size 365) % 22.56/6.21 % 22.56/6.21 % SZS output start Proof for theBenchmark % 22.56/6.21 Assumed formulas after preprocessing and simplification: % 22.56/6.21 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (orthogonal_through_point(v2, v0) = v3 & orthogonal_through_point(v1, v0) = v2 & convergent_lines(v1, v3) = 0 & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (unorthogonal_lines(v6, v7) = v9) | ~ (apart_point_and_line(v4, v6) = v8) | ~ (distinct_lines(v5, v6) = 0) | ? [v10] : ((v10 = 0 & unorthogonal_lines(v5, v7) = 0) | (v10 = 0 & apart_point_and_line(v4, v5) = 0))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (unorthogonal_lines(v6, v7) = v9) | ~ (apart_point_and_line(v4, v5) = v8) | ? [v10] : ((v10 = 0 & unorthogonal_lines(v5, v7) = 0) | (v10 = 0 & apart_point_and_line(v4, v6) = 0) | ( ~ (v10 = 0) & distinct_lines(v5, v6) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (unorthogonal_lines(v5, v7) = v9) | ~ (apart_point_and_line(v4, v6) = v8) | ? [v10] : ((v10 = 0 & unorthogonal_lines(v6, v7) = 0) | (v10 = 0 & apart_point_and_line(v4, v5) = 0) | ( ~ (v10 = 0) & distinct_lines(v5, v6) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (unorthogonal_lines(v5, v7) = v9) | ~ (apart_point_and_line(v4, v5) = v8) | ~ (distinct_lines(v5, v6) = 0) | ? [v10] : ((v10 = 0 & unorthogonal_lines(v6, v7) = 0) | (v10 = 0 & apart_point_and_line(v4, v6) = 0))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (apart_point_and_line(v5, v7) = v9) | ~ (apart_point_and_line(v5, v6) = v8) | ~ (distinct_points(v4, v5) = 0) | ? [v10] : ((v10 = 0 & apart_point_and_line(v4, v7) = 0) | (v10 = 0 & apart_point_and_line(v4, v6) = 0) | ( ~ (v10 = 0) & distinct_lines(v6, v7) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (apart_point_and_line(v5, v7) = v9) | ~ (apart_point_and_line(v4, v7) = v8) | ~ (distinct_lines(v6, v7) = 0) | ? [v10] : ((v10 = 0 & apart_point_and_line(v5, v6) = 0) | (v10 = 0 & apart_point_and_line(v4, v6) = 0) | ( ~ (v10 = 0) & distinct_points(v4, v5) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (apart_point_and_line(v5, v7) = v9) | ~ (apart_point_and_line(v4, v6) = v8) | ? [v10] : ((v10 = 0 & apart_point_and_line(v5, v6) = 0) | (v10 = 0 & apart_point_and_line(v4, v7) = 0) | ( ~ (v10 = 0) & distinct_lines(v6, v7) = v10) | ( ~ (v10 = 0) & distinct_points(v4, v5) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (apart_point_and_line(v5, v6) = v9) | ~ (apart_point_and_line(v4, v7) = v8) | ? [v10] : ((v10 = 0 & apart_point_and_line(v5, v7) = 0) | (v10 = 0 & apart_point_and_line(v4, v6) = 0) | ( ~ (v10 = 0) & distinct_lines(v6, v7) = v10) | ( ~ (v10 = 0) & distinct_points(v4, v5) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (apart_point_and_line(v5, v6) = v9) | ~ (apart_point_and_line(v4, v6) = v8) | ~ (distinct_lines(v6, v7) = 0) | ? [v10] : ((v10 = 0 & apart_point_and_line(v5, v7) = 0) | (v10 = 0 & apart_point_and_line(v4, v7) = 0) | ( ~ (v10 = 0) & distinct_points(v4, v5) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v9 = 0 | v8 = 0 | ~ (apart_point_and_line(v4, v7) = v9) | ~ (apart_point_and_line(v4, v6) = v8) | ~ (distinct_points(v4, v5) = 0) | ? [v10] : ((v10 = 0 & apart_point_and_line(v5, v7) = 0) | (v10 = 0 & apart_point_and_line(v5, v6) = 0) | ( ~ (v10 = 0) & distinct_lines(v6, v7) = v10))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (apart_point_and_line(v6, v5) = v8) | ~ (distinct_points(v4, v6) = v7) | ? [v9] : ( ~ (v9 = 0) & apart_point_and_line(v4, v5) = v9)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (apart_point_and_line(v4, v6) = v8) | ~ (apart_point_and_line(v4, v5) = v7) | ? [v9] : ((v9 = 0 & convergent_lines(v5, v6) = 0) | ( ~ (v9 = 0) & distinct_lines(v5, v6) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (apart_point_and_line(v4, v6) = v8) | ~ (distinct_lines(v5, v6) = v7) | ? [v9] : ( ~ (v9 = 0) & apart_point_and_line(v4, v5) = v9)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (apart_point_and_line(v4, v6) = v7) | ~ (convergent_lines(v5, v6) = v8) | ? [v9] : ((v9 = 0 & apart_point_and_line(v4, v5) = 0) | ( ~ (v9 = 0) & distinct_lines(v5, v6) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (apart_point_and_line(v4, v5) = v7) | ~ (convergent_lines(v5, v6) = v8) | ? [v9] : ((v9 = 0 & apart_point_and_line(v4, v6) = 0) | ( ~ (v9 = 0) & distinct_lines(v5, v6) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (convergent_lines(v5, v6) = v8) | ~ (convergent_lines(v4, v6) = v7) | ? [v9] : ( ~ (v9 = 0) & convergent_lines(v4, v5) = v9)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (convergent_lines(v4, v6) = v8) | ~ (distinct_lines(v5, v6) = v7) | ? [v9] : ( ~ (v9 = 0) & convergent_lines(v4, v5) = v9)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (distinct_lines(v5, v6) = v8) | ~ (distinct_lines(v4, v6) = v7) | ? [v9] : ( ~ (v9 = 0) & distinct_lines(v4, v5) = v9)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : (v8 = 0 | v7 = 0 | ~ (distinct_points(v5, v6) = v8) | ~ (distinct_points(v4, v6) = v7) | ? [v9] : ( ~ (v9 = 0) & distinct_points(v4, v5) = v9)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (unorthogonal_lines(v5, v6) = v8) | ~ (unorthogonal_lines(v4, v6) = v7) | ? [v9] : ((v9 = 0 & v8 = 0 & convergent_lines(v5, v6) = 0) | (v9 = 0 & v7 = 0 & convergent_lines(v4, v6) = 0) | ( ~ (v9 = 0) & unorthogonal_lines(v4, v5) = v9) | ( ~ (v9 = 0) & convergent_lines(v4, v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (unorthogonal_lines(v5, v6) = v8) | ~ (convergent_lines(v4, v6) = v7) | ? [v9] : ((v9 = 0 & v8 = 0 & convergent_lines(v5, v6) = 0) | (v9 = 0 & v7 = 0 & unorthogonal_lines(v4, v6) = 0) | ( ~ (v9 = 0) & unorthogonal_lines(v4, v5) = v9) | ( ~ (v9 = 0) & convergent_lines(v4, v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (unorthogonal_lines(v4, v6) = v7) | ~ (convergent_lines(v5, v6) = v8) | ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v5, v6) = 0) | (v9 = 0 & v7 = 0 & convergent_lines(v4, v6) = 0) | ( ~ (v9 = 0) & unorthogonal_lines(v4, v5) = v9) | ( ~ (v9 = 0) & convergent_lines(v4, v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (convergent_lines(v5, v6) = v8) | ~ (convergent_lines(v4, v6) = v7) | ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v5, v6) = 0) | (v9 = 0 & v7 = 0 & unorthogonal_lines(v4, v6) = 0) | ( ~ (v9 = 0) & unorthogonal_lines(v4, v5) = v9) | ( ~ (v9 = 0) & convergent_lines(v4, v5) = v9))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (apart_point_and_line(v6, v5) = v7) | ~ (apart_point_and_line(v4, v5) = 0) | distinct_points(v4, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (apart_point_and_line(v4, v6) = v7) | ~ (apart_point_and_line(v4, v5) = 0) | distinct_lines(v5, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (apart_point_and_line(v4, v6) = v7) | ~ (distinct_lines(v5, v6) = 0) | ? [v8] : ((v8 = 0 & apart_point_and_line(v4, v5) = 0) | (v8 = 0 & convergent_lines(v5, v6) = 0))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (apart_point_and_line(v4, v5) = v7) | ~ (distinct_lines(v5, v6) = 0) | ? [v8] : ((v8 = 0 & apart_point_and_line(v4, v6) = 0) | (v8 = 0 & convergent_lines(v5, v6) = 0))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (apart_point_and_line(v4, v5) = 0) | ~ (distinct_lines(v5, v6) = v7) | apart_point_and_line(v4, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (apart_point_and_line(v4, v5) = 0) | ~ (distinct_points(v4, v6) = v7) | apart_point_and_line(v6, v5) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (convergent_lines(v5, v6) = v7) | ~ (convergent_lines(v4, v5) = 0) | convergent_lines(v4, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (convergent_lines(v4, v6) = v7) | ~ (convergent_lines(v4, v5) = 0) | convergent_lines(v5, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (convergent_lines(v4, v6) = v7) | ~ (convergent_lines(v4, v5) = 0) | distinct_lines(v5, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (convergent_lines(v4, v5) = 0) | ~ (distinct_lines(v5, v6) = v7) | convergent_lines(v4, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (distinct_lines(v5, v6) = v7) | ~ (distinct_lines(v4, v5) = 0) | distinct_lines(v4, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (distinct_lines(v4, v6) = v7) | ~ (distinct_lines(v4, v5) = 0) | distinct_lines(v5, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (distinct_points(v5, v6) = v7) | ~ (distinct_points(v4, v5) = 0) | distinct_points(v4, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (distinct_points(v4, v6) = v7) | ~ (distinct_points(v4, v5) = 0) | distinct_points(v5, v6) = 0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (orthogonal_through_point(v7, v6) = v5) | ~ (orthogonal_through_point(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (unorthogonal_lines(v7, v6) = v5) | ~ (unorthogonal_lines(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (parallel_through_point(v7, v6) = v5) | ~ (parallel_through_point(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (intersection_point(v7, v6) = v5) | ~ (intersection_point(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (line_connecting(v7, v6) = v5) | ~ (line_connecting(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (apart_point_and_line(v7, v6) = v5) | ~ (apart_point_and_line(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (convergent_lines(v7, v6) = v5) | ~ (convergent_lines(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (distinct_lines(v7, v6) = v5) | ~ (distinct_lines(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (distinct_points(v7, v6) = v5) | ~ (distinct_points(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (unorthogonal_lines(v5, v6) = v7) | ~ (unorthogonal_lines(v4, v5) = 0) | ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v4, v6) = 0 & convergent_lines(v4, v6) = 0) | (v8 = 0 & v7 = 0 & convergent_lines(v5, v6) = 0) | ( ~ (v8 = 0) & convergent_lines(v4, v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (unorthogonal_lines(v5, v6) = v7) | ~ (convergent_lines(v4, v5) = 0) | ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v4, v6) = 0 & convergent_lines(v4, v6) = 0) | (v8 = 0 & v7 = 0 & convergent_lines(v5, v6) = 0) | ( ~ (v8 = 0) & unorthogonal_lines(v4, v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (unorthogonal_lines(v4, v6) = v7) | ~ (unorthogonal_lines(v4, v5) = 0) | ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v5, v6) = 0 & convergent_lines(v5, v6) = 0) | (v8 = 0 & v7 = 0 & convergent_lines(v4, v6) = 0) | ( ~ (v8 = 0) & convergent_lines(v4, v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (unorthogonal_lines(v4, v6) = v7) | ~ (convergent_lines(v4, v5) = 0) | ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v5, v6) = 0 & convergent_lines(v5, v6) = 0) | (v8 = 0 & v7 = 0 & convergent_lines(v4, v6) = 0) | ( ~ (v8 = 0) & unorthogonal_lines(v4, v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (unorthogonal_lines(v4, v5) = 0) | ~ (convergent_lines(v5, v6) = v7) | ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v4, v6) = 0 & convergent_lines(v4, v6) = 0) | (v8 = 0 & v7 = 0 & unorthogonal_lines(v5, v6) = 0) | ( ~ (v8 = 0) & convergent_lines(v4, v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (unorthogonal_lines(v4, v5) = 0) | ~ (convergent_lines(v4, v6) = v7) | ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v5, v6) = 0 & convergent_lines(v5, v6) = 0) | (v8 = 0 & v7 = 0 & unorthogonal_lines(v4, v6) = 0) | ( ~ (v8 = 0) & convergent_lines(v4, v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (convergent_lines(v5, v6) = v7) | ~ (convergent_lines(v4, v5) = 0) | ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v4, v6) = 0 & convergent_lines(v4, v6) = 0) | (v8 = 0 & v7 = 0 & unorthogonal_lines(v5, v6) = 0) | ( ~ (v8 = 0) & unorthogonal_lines(v4, v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (convergent_lines(v4, v6) = v7) | ~ (convergent_lines(v4, v5) = 0) | ? [v8] : ? [v9] : ((v9 = 0 & v8 = 0 & unorthogonal_lines(v5, v6) = 0 & convergent_lines(v5, v6) = 0) | (v8 = 0 & v7 = 0 & unorthogonal_lines(v4, v6) = 0) | ( ~ (v8 = 0) & unorthogonal_lines(v4, v5) = v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (distinct_lines(v6, v7) = 0) | ~ (distinct_points(v4, v5) = 0) | ? [v8] : ((v8 = 0 & apart_point_and_line(v5, v7) = 0) | (v8 = 0 & apart_point_and_line(v5, v6) = 0) | (v8 = 0 & apart_point_and_line(v4, v7) = 0) | (v8 = 0 & apart_point_and_line(v4, v6) = 0))) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (unorthogonal_lines(v4, v5) = v6) | convergent_lines(v4, v5) = 0) & ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (convergent_lines(v4, v5) = v6) | unorthogonal_lines(v4, v5) = 0) & ! [v4] : ! [v5] : ! [v6] : ( ~ (orthogonal_through_point(v5, v4) = v6) | ? [v7] : ( ~ (v7 = 0) & unorthogonal_lines(v6, v5) = v7)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (orthogonal_through_point(v5, v4) = v6) | ? [v7] : ( ~ (v7 = 0) & apart_point_and_line(v4, v6) = v7)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (parallel_through_point(v5, v4) = v6) | ? [v7] : ( ~ (v7 = 0) & apart_point_and_line(v4, v6) = v7)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (parallel_through_point(v5, v4) = v6) | ? [v7] : ( ~ (v7 = 0) & convergent_lines(v6, v5) = v7)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (intersection_point(v4, v5) = v6) | ? [v7] : (( ~ (v7 = 0) & apart_point_and_line(v6, v5) = v7) | ( ~ (v7 = 0) & convergent_lines(v4, v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (intersection_point(v4, v5) = v6) | ? [v7] : (( ~ (v7 = 0) & apart_point_and_line(v6, v4) = v7) | ( ~ (v7 = 0) & convergent_lines(v4, v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (line_connecting(v4, v5) = v6) | ? [v7] : (( ~ (v7 = 0) & apart_point_and_line(v5, v6) = v7) | ( ~ (v7 = 0) & distinct_points(v4, v5) = v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ (line_connecting(v4, v5) = v6) | ? [v7] : (( ~ (v7 = 0) & apart_point_and_line(v4, v6) = v7) | ( ~ (v7 = 0) & distinct_points(v4, v5) = v7))) & ! [v4] : ! [v5] : ( ~ (convergent_lines(v4, v5) = 0) | ? [v6] : ? [v7] : ( ~ (v7 = 0) & intersection_point(v4, v5) = v6 & apart_point_and_line(v6, v5) = v7)) & ! [v4] : ! [v5] : ( ~ (convergent_lines(v4, v5) = 0) | ? [v6] : ? [v7] : ( ~ (v7 = 0) & intersection_point(v4, v5) = v6 & apart_point_and_line(v6, v4) = v7)) & ! [v4] : ! [v5] : ( ~ (distinct_points(v4, v5) = 0) | ? [v6] : ? [v7] : ( ~ (v7 = 0) & line_connecting(v4, v5) = v6 & apart_point_and_line(v5, v6) = v7)) & ! [v4] : ! [v5] : ( ~ (distinct_points(v4, v5) = 0) | ? [v6] : ? [v7] : ( ~ (v7 = 0) & line_connecting(v4, v5) = v6 & apart_point_and_line(v4, v6) = v7)) & ! [v4] : ~ (convergent_lines(v4, v4) = 0) & ! [v4] : ~ (distinct_lines(v4, v4) = 0) & ! [v4] : ~ (distinct_points(v4, v4) = 0) & ? [v4] : ? [v5] : ? [v6] : orthogonal_through_point(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : unorthogonal_lines(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : parallel_through_point(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : intersection_point(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : line_connecting(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : apart_point_and_line(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : convergent_lines(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : distinct_lines(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : distinct_points(v5, v4) = v6) % 22.97/6.28 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 22.97/6.28 | (1) orthogonal_through_point(all_0_1_1, all_0_3_3) = all_0_0_0 & orthogonal_through_point(all_0_2_2, all_0_3_3) = all_0_1_1 & convergent_lines(all_0_2_2, all_0_0_0) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v2, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = 0) | ? [v6] : ((v6 = 0 & unorthogonal_lines(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v1) = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v2, v3) = v5) | ~ (apart_point_and_line(v0, v1) = v4) | ? [v6] : ((v6 = 0 & unorthogonal_lines(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v6 = 0) & distinct_lines(v1, v2) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v1, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ? [v6] : ((v6 = 0 & unorthogonal_lines(v2, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v1) = 0) | ( ~ (v6 = 0) & distinct_lines(v1, v2) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v1, v3) = v5) | ~ (apart_point_and_line(v0, v1) = v4) | ~ (distinct_lines(v1, v2) = 0) | ? [v6] : ((v6 = 0 & unorthogonal_lines(v2, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v1, v2) = v4) | ~ (distinct_points(v0, v1) = 0) | ? [v6] : ((v6 = 0 & apart_point_and_line(v0, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v6 = 0) & distinct_lines(v2, v3) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v0, v3) = v4) | ~ (distinct_lines(v2, v3) = 0) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v2) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v6 = 0) & distinct_points(v0, v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v2) = 0) | (v6 = 0 & apart_point_and_line(v0, v3) = 0) | ( ~ (v6 = 0) & distinct_lines(v2, v3) = v6) | ( ~ (v6 = 0) & distinct_points(v0, v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v2) = v5) | ~ (apart_point_and_line(v0, v3) = v4) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v6 = 0) & distinct_lines(v2, v3) = v6) | ( ~ (v6 = 0) & distinct_points(v0, v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v2) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v2, v3) = 0) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v3) = 0) | ( ~ (v6 = 0) & distinct_points(v0, v1) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v0, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_points(v0, v1) = 0) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v1, v2) = 0) | ( ~ (v6 = 0) & distinct_lines(v2, v3) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v2, v1) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v4) | ~ (apart_point_and_line(v0, v1) = v3) | ? [v5] : ((v5 = 0 & convergent_lines(v1, v2) = 0) | ( ~ (v5 = 0) & distinct_lines(v1, v2) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ((v5 = 0 & apart_point_and_line(v0, v1) = 0) | ( ~ (v5 = 0) & distinct_lines(v1, v2) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v1) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ((v5 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v5 = 0) & distinct_lines(v1, v2) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (convergent_lines(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_lines(v1, v2) = v4) | ~ (distinct_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_lines(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_points(v1, v2) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_points(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v1, v2) = v4) | ~ (unorthogonal_lines(v0, v2) = v3) | ? [v5] : ((v5 = 0 & v4 = 0 & convergent_lines(v1, v2) = 0) | (v5 = 0 & v3 = 0 & convergent_lines(v0, v2) = 0) | ( ~ (v5 = 0) & unorthogonal_lines(v0, v1) = v5) | ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ((v5 = 0 & v4 = 0 & convergent_lines(v1, v2) = 0) | (v5 = 0 & v3 = 0 & unorthogonal_lines(v0, v2) = 0) | ( ~ (v5 = 0) & unorthogonal_lines(v0, v1) = v5) | ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0) | (v5 = 0 & v3 = 0 & convergent_lines(v0, v2) = 0) | ( ~ (v5 = 0) & unorthogonal_lines(v0, v1) = v5) | ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0) | (v5 = 0 & v3 = 0 & unorthogonal_lines(v0, v2) = 0) | ( ~ (v5 = 0) & unorthogonal_lines(v0, v1) = v5) | ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v2, v1) = v3) | ~ (apart_point_and_line(v0, v1) = 0) | distinct_points(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (apart_point_and_line(v0, v1) = 0) | distinct_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (distinct_lines(v1, v2) = 0) | ? [v4] : ((v4 = 0 & apart_point_and_line(v0, v1) = 0) | (v4 = 0 & convergent_lines(v1, v2) = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = v3) | ~ (distinct_lines(v1, v2) = 0) | ? [v4] : ((v4 = 0 & apart_point_and_line(v0, v2) = 0) | (v4 = 0 & convergent_lines(v1, v2) = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | apart_point_and_line(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = 0) | ~ (distinct_points(v0, v2) = v3) | apart_point_and_line(v2, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | convergent_lines(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (orthogonal_through_point(v3, v2) = v1) | ~ (orthogonal_through_point(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unorthogonal_lines(v3, v2) = v1) | ~ (unorthogonal_lines(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (parallel_through_point(v3, v2) = v1) | ~ (parallel_through_point(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v1, v2) = v3) | ~ (unorthogonal_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v0, v2) = 0 & convergent_lines(v0, v2) = 0) | (v4 = 0 & v3 = 0 & convergent_lines(v1, v2) = 0) | ( ~ (v4 = 0) & convergent_lines(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v0, v2) = 0 & convergent_lines(v0, v2) = 0) | (v4 = 0 & v3 = 0 & convergent_lines(v1, v2) = 0) | ( ~ (v4 = 0) & unorthogonal_lines(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (unorthogonal_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0 & convergent_lines(v1, v2) = 0) | (v4 = 0 & v3 = 0 & convergent_lines(v0, v2) = 0) | ( ~ (v4 = 0) & convergent_lines(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0 & convergent_lines(v1, v2) = 0) | (v4 = 0 & v3 = 0 & convergent_lines(v0, v2) = 0) | ( ~ (v4 = 0) & unorthogonal_lines(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v1) = 0) | ~ (convergent_lines(v1, v2) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v0, v2) = 0 & convergent_lines(v0, v2) = 0) | (v4 = 0 & v3 = 0 & unorthogonal_lines(v1, v2) = 0) | ( ~ (v4 = 0) & convergent_lines(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v1) = 0) | ~ (convergent_lines(v0, v2) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0 & convergent_lines(v1, v2) = 0) | (v4 = 0 & v3 = 0 & unorthogonal_lines(v0, v2) = 0) | ( ~ (v4 = 0) & convergent_lines(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v0, v2) = 0 & convergent_lines(v0, v2) = 0) | (v4 = 0 & v3 = 0 & unorthogonal_lines(v1, v2) = 0) | ( ~ (v4 = 0) & unorthogonal_lines(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0 & convergent_lines(v1, v2) = 0) | (v4 = 0 & v3 = 0 & unorthogonal_lines(v0, v2) = 0) | ( ~ (v4 = 0) & unorthogonal_lines(v0, v1) = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_lines(v2, v3) = 0) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ((v4 = 0 & apart_point_and_line(v1, v3) = 0) | (v4 = 0 & apart_point_and_line(v1, v2) = 0) | (v4 = 0 & apart_point_and_line(v0, v3) = 0) | (v4 = 0 & apart_point_and_line(v0, v2) = 0))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (unorthogonal_lines(v0, v1) = v2) | convergent_lines(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (convergent_lines(v0, v1) = v2) | unorthogonal_lines(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (orthogonal_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & unorthogonal_lines(v2, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (orthogonal_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & apart_point_and_line(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (parallel_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & apart_point_and_line(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (parallel_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v2, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & apart_point_and_line(v2, v1) = v3) | ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & apart_point_and_line(v2, v0) = v3) | ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & apart_point_and_line(v1, v2) = v3) | ( ~ (v3 = 0) & distinct_points(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & apart_point_and_line(v0, v2) = v3) | ( ~ (v3 = 0) & distinct_points(v0, v1) = v3))) & ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v1) = v3)) & ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v0) = v3)) & ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v1, v2) = v3)) & ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v0, v2) = v3)) & ! [v0] : ~ (convergent_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_points(v0, v0) = 0) & ? [v0] : ? [v1] : ? [v2] : orthogonal_through_point(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : unorthogonal_lines(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : parallel_through_point(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : intersection_point(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : line_connecting(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : apart_point_and_line(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : convergent_lines(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : distinct_lines(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : distinct_points(v1, v0) = v2 % 22.97/6.31 | % 22.97/6.31 | Applying alpha-rule on (1) yields: % 22.97/6.31 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ((v5 = 0 & v4 = 0 & convergent_lines(v1, v2) = 0) | (v5 = 0 & v3 = 0 & unorthogonal_lines(v0, v2) = 0) | ( ~ (v5 = 0) & unorthogonal_lines(v0, v1) = v5) | ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5))) % 22.97/6.31 | (3) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (convergent_lines(v0, v1) = v2) | unorthogonal_lines(v0, v1) = 0) % 22.97/6.31 | (4) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (unorthogonal_lines(v0, v1) = v2) | convergent_lines(v0, v1) = 0) % 22.97/6.31 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v2, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = 0) | ? [v6] : ((v6 = 0 & unorthogonal_lines(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v1) = 0))) % 22.97/6.31 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v1, v2) = v4) | ~ (distinct_points(v0, v1) = 0) | ? [v6] : ((v6 = 0 & apart_point_and_line(v0, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v6 = 0) & distinct_lines(v2, v3) = v6))) % 22.97/6.31 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v0, v3) = v4) | ~ (distinct_lines(v2, v3) = 0) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v2) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v6 = 0) & distinct_points(v0, v1) = v6))) % 22.97/6.31 | (8) ? [v0] : ? [v1] : ? [v2] : line_connecting(v1, v0) = v2 % 22.97/6.31 | (9) ! [v0] : ~ (distinct_points(v0, v0) = 0) % 22.97/6.31 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v2) = v5) | ~ (apart_point_and_line(v0, v3) = v4) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v6 = 0) & distinct_lines(v2, v3) = v6) | ( ~ (v6 = 0) & distinct_points(v0, v1) = v6))) % 22.97/6.31 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) % 22.97/6.31 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) % 22.97/6.31 | (13) ! [v0] : ~ (distinct_lines(v0, v0) = 0) % 22.97/6.31 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_points(v1, v2) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_points(v0, v1) = v5)) % 22.97/6.31 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0) | (v5 = 0 & v3 = 0 & unorthogonal_lines(v0, v2) = 0) | ( ~ (v5 = 0) & unorthogonal_lines(v0, v1) = v5) | ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5))) % 22.97/6.31 | (16) ? [v0] : ? [v1] : ? [v2] : unorthogonal_lines(v1, v0) = v2 % 22.97/6.31 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v2, v1) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) % 22.97/6.31 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (orthogonal_through_point(v3, v2) = v1) | ~ (orthogonal_through_point(v3, v2) = v0)) % 22.97/6.31 | (19) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v1) = v3)) % 22.97/6.31 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v2) = 0) | (v6 = 0 & apart_point_and_line(v0, v3) = 0) | ( ~ (v6 = 0) & distinct_lines(v2, v3) = v6) | ( ~ (v6 = 0) & distinct_points(v0, v1) = v6))) % 22.97/6.31 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0 & convergent_lines(v1, v2) = 0) | (v4 = 0 & v3 = 0 & convergent_lines(v0, v2) = 0) | ( ~ (v4 = 0) & unorthogonal_lines(v0, v1) = v4))) % 22.97/6.31 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (unorthogonal_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0 & convergent_lines(v1, v2) = 0) | (v4 = 0 & v3 = 0 & convergent_lines(v0, v2) = 0) | ( ~ (v4 = 0) & convergent_lines(v0, v1) = v4))) % 22.97/6.31 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_lines(v1, v2) = v4) | ~ (distinct_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_lines(v0, v1) = v5)) % 22.97/6.31 | (24) ? [v0] : ? [v1] : ? [v2] : apart_point_and_line(v1, v0) = v2 % 22.97/6.31 | (25) ? [v0] : ? [v1] : ? [v2] : convergent_lines(v1, v0) = v2 % 22.97/6.31 | (26) ? [v0] : ? [v1] : ? [v2] : distinct_points(v1, v0) = v2 % 22.97/6.31 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) % 22.97/6.31 | (28) ? [v0] : ? [v1] : ? [v2] : parallel_through_point(v1, v0) = v2 % 22.97/6.31 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v2, v3) = v5) | ~ (apart_point_and_line(v0, v1) = v4) | ? [v6] : ((v6 = 0 & unorthogonal_lines(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v6 = 0) & distinct_lines(v1, v2) = v6))) % 22.97/6.32 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v1, v2) = v4) | ~ (unorthogonal_lines(v0, v2) = v3) | ? [v5] : ((v5 = 0 & v4 = 0 & convergent_lines(v1, v2) = 0) | (v5 = 0 & v3 = 0 & convergent_lines(v0, v2) = 0) | ( ~ (v5 = 0) & unorthogonal_lines(v0, v1) = v5) | ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5))) % 22.97/6.32 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v1, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ? [v6] : ((v6 = 0 & unorthogonal_lines(v2, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v1) = 0) | ( ~ (v6 = 0) & distinct_lines(v1, v2) = v6))) % 23.18/6.32 | (32) orthogonal_through_point(all_0_2_2, all_0_3_3) = all_0_1_1 % 23.18/6.32 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v1) = 0) | ~ (convergent_lines(v1, v2) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v0, v2) = 0 & convergent_lines(v0, v2) = 0) | (v4 = 0 & v3 = 0 & unorthogonal_lines(v1, v2) = 0) | ( ~ (v4 = 0) & convergent_lines(v0, v1) = v4))) % 23.18/6.32 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v1) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ((v5 = 0 & apart_point_and_line(v0, v2) = 0) | ( ~ (v5 = 0) & distinct_lines(v1, v2) = v5))) % 23.18/6.32 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & apart_point_and_line(v1, v2) = v3) | ( ~ (v3 = 0) & distinct_points(v0, v1) = v3))) % 23.18/6.32 | (36) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) % 23.18/6.32 | (37) orthogonal_through_point(all_0_1_1, all_0_3_3) = all_0_0_0 % 23.18/6.32 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) % 23.18/6.32 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v2) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v2, v3) = 0) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v3) = 0) | ( ~ (v6 = 0) & distinct_points(v0, v1) = v6))) % 23.18/6.32 | (40) ! [v0] : ! [v1] : ! [v2] : ( ~ (parallel_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v2, v1) = v3)) % 23.18/6.32 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) % 23.18/6.32 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v0, v2) = 0 & convergent_lines(v0, v2) = 0) | (v4 = 0 & v3 = 0 & convergent_lines(v1, v2) = 0) | ( ~ (v4 = 0) & unorthogonal_lines(v0, v1) = v4))) % 23.18/6.32 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v1, v2) = v3) | ~ (unorthogonal_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v0, v2) = 0 & convergent_lines(v0, v2) = 0) | (v4 = 0 & v3 = 0 & convergent_lines(v1, v2) = 0) | ( ~ (v4 = 0) & convergent_lines(v0, v1) = v4))) % 23.18/6.32 | (44) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v0) = v3)) % 23.18/6.32 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (distinct_lines(v1, v2) = 0) | ? [v4] : ((v4 = 0 & apart_point_and_line(v0, v1) = 0) | (v4 = 0 & convergent_lines(v1, v2) = 0))) % 23.18/6.32 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0 & convergent_lines(v1, v2) = 0) | (v4 = 0 & v3 = 0 & unorthogonal_lines(v0, v2) = 0) | ( ~ (v4 = 0) & unorthogonal_lines(v0, v1) = v4))) % 23.18/6.32 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) % 23.18/6.32 | (48) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = v3) | ~ (distinct_lines(v1, v2) = 0) | ? [v4] : ((v4 = 0 & apart_point_and_line(v0, v2) = 0) | (v4 = 0 & convergent_lines(v1, v2) = 0))) % 23.18/6.32 | (49) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) % 23.18/6.32 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) % 23.18/6.32 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) % 23.18/6.32 | (52) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (apart_point_and_line(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 23.18/6.32 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 23.18/6.32 | (54) ? [v0] : ? [v1] : ? [v2] : orthogonal_through_point(v1, v0) = v2 % 23.18/6.32 | (55) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = 0) | ~ (distinct_points(v0, v2) = v3) | apart_point_and_line(v2, v1) = 0) % 23.18/6.32 | (56) ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & apart_point_and_line(v2, v1) = v3) | ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3))) % 23.18/6.33 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) % 23.18/6.33 | (58) ? [v0] : ? [v1] : ? [v2] : distinct_lines(v1, v0) = v2 % 23.18/6.33 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 23.18/6.33 | (60) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_lines(v2, v3) = 0) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ((v4 = 0 & apart_point_and_line(v1, v3) = 0) | (v4 = 0 & apart_point_and_line(v1, v2) = 0) | (v4 = 0 & apart_point_and_line(v0, v3) = 0) | (v4 = 0 & apart_point_and_line(v0, v2) = 0))) % 23.18/6.33 | (61) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (parallel_through_point(v3, v2) = v1) | ~ (parallel_through_point(v3, v2) = v0)) % 23.18/6.33 | (62) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (convergent_lines(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) % 23.18/6.33 | (63) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v2, v1) = v3) | ~ (apart_point_and_line(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 23.18/6.33 | (64) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 23.18/6.33 | (65) ! [v0] : ! [v1] : ! [v2] : ( ~ (parallel_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & apart_point_and_line(v0, v2) = v3)) % 23.18/6.33 | (66) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) % 23.18/6.33 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | apart_point_and_line(v0, v2) = 0) % 23.18/6.33 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | convergent_lines(v0, v2) = 0) % 23.18/6.33 | (69) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v1, v3) = v5) | ~ (apart_point_and_line(v0, v1) = v4) | ~ (distinct_lines(v1, v2) = 0) | ? [v6] : ((v6 = 0 & unorthogonal_lines(v2, v3) = 0) | (v6 = 0 & apart_point_and_line(v0, v2) = 0))) % 23.18/6.33 | (70) ! [v0] : ! [v1] : ! [v2] : ( ~ (orthogonal_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & unorthogonal_lines(v2, v1) = v3)) % 23.18/6.33 | (71) ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v1, v2) = v3)) % 23.18/6.33 | (72) ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v0, v2) = v3)) % 23.18/6.33 | (73) ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & apart_point_and_line(v2, v0) = v3) | ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3))) % 23.18/6.33 | (74) convergent_lines(all_0_2_2, all_0_0_0) = 0 % 23.18/6.33 | (75) ? [v0] : ? [v1] : ? [v2] : intersection_point(v1, v0) = v2 % 23.18/6.33 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v1) = 0) | ~ (convergent_lines(v0, v2) = v3) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0 & convergent_lines(v1, v2) = 0) | (v4 = 0 & v3 = 0 & unorthogonal_lines(v0, v2) = 0) | ( ~ (v4 = 0) & convergent_lines(v0, v1) = v4))) % 23.18/6.33 | (77) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v1, v2) = 0) | (v5 = 0 & v3 = 0 & convergent_lines(v0, v2) = 0) | ( ~ (v5 = 0) & unorthogonal_lines(v0, v1) = v5) | ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5))) % 23.18/6.33 | (78) ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : (( ~ (v3 = 0) & apart_point_and_line(v0, v2) = v3) | ( ~ (v3 = 0) & distinct_points(v0, v1) = v3))) % 23.18/6.33 | (79) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unorthogonal_lines(v3, v2) = v1) | ~ (unorthogonal_lines(v3, v2) = v0)) % 23.18/6.33 | (80) ! [v0] : ! [v1] : ! [v2] : ( ~ (orthogonal_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & apart_point_and_line(v0, v2) = v3)) % 23.18/6.33 | (81) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & unorthogonal_lines(v0, v2) = 0 & convergent_lines(v0, v2) = 0) | (v4 = 0 & v3 = 0 & unorthogonal_lines(v1, v2) = 0) | ( ~ (v4 = 0) & unorthogonal_lines(v0, v1) = v4))) % 23.18/6.33 | (82) ! [v0] : ~ (convergent_lines(v0, v0) = 0) % 23.18/6.33 | (83) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v4) | ~ (apart_point_and_line(v0, v1) = v3) | ? [v5] : ((v5 = 0 & convergent_lines(v1, v2) = 0) | ( ~ (v5 = 0) & distinct_lines(v1, v2) = v5))) % 23.18/6.33 | (84) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ((v5 = 0 & apart_point_and_line(v0, v1) = 0) | ( ~ (v5 = 0) & distinct_lines(v1, v2) = v5))) % 23.18/6.33 | (85) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v0, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_points(v0, v1) = 0) | ? [v6] : ((v6 = 0 & apart_point_and_line(v1, v3) = 0) | (v6 = 0 & apart_point_and_line(v1, v2) = 0) | ( ~ (v6 = 0) & distinct_lines(v2, v3) = v6))) % 23.18/6.34 | % 23.18/6.34 | Instantiating formula (70) with all_0_0_0, all_0_1_1, all_0_3_3 and discharging atoms orthogonal_through_point(all_0_1_1, all_0_3_3) = all_0_0_0, yields: % 23.18/6.34 | (86) ? [v0] : ( ~ (v0 = 0) & unorthogonal_lines(all_0_0_0, all_0_1_1) = v0) % 23.18/6.34 | % 23.18/6.34 | Instantiating formula (80) with all_0_0_0, all_0_1_1, all_0_3_3 and discharging atoms orthogonal_through_point(all_0_1_1, all_0_3_3) = all_0_0_0, yields: % 23.18/6.34 | (87) ? [v0] : ( ~ (v0 = 0) & apart_point_and_line(all_0_3_3, all_0_0_0) = v0) % 23.18/6.34 | % 23.18/6.34 | Instantiating formula (70) with all_0_1_1, all_0_2_2, all_0_3_3 and discharging atoms orthogonal_through_point(all_0_2_2, all_0_3_3) = all_0_1_1, yields: % 23.18/6.34 | (88) ? [v0] : ( ~ (v0 = 0) & unorthogonal_lines(all_0_1_1, all_0_2_2) = v0) % 23.18/6.34 | % 23.18/6.34 | Instantiating formula (80) with all_0_1_1, all_0_2_2, all_0_3_3 and discharging atoms orthogonal_through_point(all_0_2_2, all_0_3_3) = all_0_1_1, yields: % 23.18/6.34 | (89) ? [v0] : ( ~ (v0 = 0) & apart_point_and_line(all_0_3_3, all_0_1_1) = v0) % 23.18/6.34 | % 23.18/6.34 | Instantiating formula (46) with 0, all_0_0_0, all_0_0_0, all_0_2_2 and discharging atoms convergent_lines(all_0_2_2, all_0_0_0) = 0, yields: % 23.18/6.34 | (90) ? [v0] : ? [v1] : ((v1 = 0 & v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_0_0) = 0 & convergent_lines(all_0_0_0, all_0_0_0) = 0) | (v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & unorthogonal_lines(all_0_2_2, all_0_0_0) = v0)) % 23.18/6.34 | % 23.18/6.34 | Instantiating formula (15) with 0, 0, all_0_0_0, all_0_2_2, all_0_2_2 and discharging atoms convergent_lines(all_0_2_2, all_0_0_0) = 0, yields: % 23.18/6.34 | (91) ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & unorthogonal_lines(all_0_2_2, all_0_2_2) = v0) | ( ~ (v0 = 0) & convergent_lines(all_0_2_2, all_0_2_2) = v0)) % 23.18/6.34 | % 23.18/6.34 | Instantiating formula (19) with all_0_0_0, all_0_2_2 and discharging atoms convergent_lines(all_0_2_2, all_0_0_0) = 0, yields: % 23.18/6.34 | (92) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_0_2_2, all_0_0_0) = v0 & apart_point_and_line(v0, all_0_0_0) = v1) % 23.18/6.34 | % 23.18/6.34 | Instantiating formula (44) with all_0_0_0, all_0_2_2 and discharging atoms convergent_lines(all_0_2_2, all_0_0_0) = 0, yields: % 23.18/6.34 | (93) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_0_2_2, all_0_0_0) = v0 & apart_point_and_line(v0, all_0_2_2) = v1) % 23.18/6.34 | % 23.18/6.34 | Instantiating (93) with all_26_0_31, all_26_1_32 yields: % 23.18/6.34 | (94) ~ (all_26_0_31 = 0) & intersection_point(all_0_2_2, all_0_0_0) = all_26_1_32 & apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31 % 23.18/6.34 | % 23.18/6.34 | Applying alpha-rule on (94) yields: % 23.18/6.34 | (95) ~ (all_26_0_31 = 0) % 23.18/6.34 | (96) intersection_point(all_0_2_2, all_0_0_0) = all_26_1_32 % 23.18/6.34 | (97) apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31 % 23.18/6.34 | % 23.18/6.34 | Instantiating (92) with all_28_0_33, all_28_1_34 yields: % 23.18/6.34 | (98) ~ (all_28_0_33 = 0) & intersection_point(all_0_2_2, all_0_0_0) = all_28_1_34 & apart_point_and_line(all_28_1_34, all_0_0_0) = all_28_0_33 % 23.18/6.34 | % 23.18/6.34 | Applying alpha-rule on (98) yields: % 23.18/6.34 | (99) ~ (all_28_0_33 = 0) % 23.18/6.34 | (100) intersection_point(all_0_2_2, all_0_0_0) = all_28_1_34 % 23.18/6.34 | (101) apart_point_and_line(all_28_1_34, all_0_0_0) = all_28_0_33 % 23.18/6.34 | % 23.18/6.34 | Instantiating (91) with all_30_0_35 yields: % 23.31/6.34 | (102) (all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_30_0_35 = 0) & unorthogonal_lines(all_0_2_2, all_0_2_2) = all_30_0_35) | ( ~ (all_30_0_35 = 0) & convergent_lines(all_0_2_2, all_0_2_2) = all_30_0_35) % 23.31/6.34 | % 23.31/6.34 | Instantiating (90) with all_31_0_36, all_31_1_37 yields: % 23.31/6.34 | (103) (all_31_0_36 = 0 & all_31_1_37 = 0 & unorthogonal_lines(all_0_0_0, all_0_0_0) = 0 & convergent_lines(all_0_0_0, all_0_0_0) = 0) | (all_31_1_37 = 0 & unorthogonal_lines(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_31_1_37 = 0) & unorthogonal_lines(all_0_2_2, all_0_0_0) = all_31_1_37) % 23.31/6.34 | % 23.31/6.34 | Instantiating (89) with all_32_0_38 yields: % 23.31/6.34 | (104) ~ (all_32_0_38 = 0) & apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38 % 23.31/6.34 | % 23.31/6.34 | Applying alpha-rule on (104) yields: % 23.31/6.34 | (105) ~ (all_32_0_38 = 0) % 23.31/6.34 | (106) apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38 % 23.31/6.34 | % 23.31/6.34 | Instantiating (87) with all_34_0_39 yields: % 23.31/6.34 | (107) ~ (all_34_0_39 = 0) & apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39 % 23.31/6.34 | % 23.31/6.34 | Applying alpha-rule on (107) yields: % 23.31/6.34 | (108) ~ (all_34_0_39 = 0) % 23.31/6.34 | (109) apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39 % 23.31/6.34 | % 23.31/6.34 | Instantiating (86) with all_36_0_40 yields: % 23.31/6.34 | (110) ~ (all_36_0_40 = 0) & unorthogonal_lines(all_0_0_0, all_0_1_1) = all_36_0_40 % 23.31/6.34 | % 23.31/6.34 | Applying alpha-rule on (110) yields: % 23.31/6.34 | (111) ~ (all_36_0_40 = 0) % 23.31/6.34 | (112) unorthogonal_lines(all_0_0_0, all_0_1_1) = all_36_0_40 % 23.31/6.34 | % 23.31/6.34 | Instantiating (88) with all_38_0_41 yields: % 23.31/6.34 | (113) ~ (all_38_0_41 = 0) & unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41 % 23.31/6.34 | % 23.31/6.34 | Applying alpha-rule on (113) yields: % 23.31/6.34 | (114) ~ (all_38_0_41 = 0) % 23.31/6.34 | (115) unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41 % 23.31/6.34 | % 23.31/6.34 | Instantiating formula (36) with all_0_2_2, all_0_0_0, all_26_1_32, all_28_1_34 and discharging atoms intersection_point(all_0_2_2, all_0_0_0) = all_28_1_34, intersection_point(all_0_2_2, all_0_0_0) = all_26_1_32, yields: % 23.31/6.34 | (116) all_28_1_34 = all_26_1_32 % 23.31/6.34 | % 23.31/6.34 | From (116) and (101) follows: % 23.31/6.34 | (117) apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33 % 23.31/6.34 | % 23.31/6.34 | Instantiating formula (42) with all_36_0_40, all_0_1_1, all_0_0_0, all_0_2_2 and discharging atoms unorthogonal_lines(all_0_0_0, all_0_1_1) = all_36_0_40, convergent_lines(all_0_2_2, all_0_0_0) = 0, yields: % 23.31/6.34 | (118) ? [v0] : ? [v1] : ((v1 = 0 & v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0 & convergent_lines(all_0_2_2, all_0_1_1) = 0) | (v0 = 0 & all_36_0_40 = 0 & convergent_lines(all_0_0_0, all_0_1_1) = 0) | ( ~ (v0 = 0) & unorthogonal_lines(all_0_2_2, all_0_0_0) = v0)) % 23.31/6.34 | % 23.31/6.34 | Instantiating formula (4) with all_38_0_41, all_0_2_2, all_0_1_1 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, yields: % 23.31/6.34 | (119) all_38_0_41 = 0 | convergent_lines(all_0_1_1, all_0_2_2) = 0 % 23.31/6.34 | % 23.31/6.34 | Instantiating formula (29) with all_36_0_40, all_28_0_33, all_0_1_1, all_0_0_0, all_0_0_0, all_26_1_32 and discharging atoms unorthogonal_lines(all_0_0_0, all_0_1_1) = all_36_0_40, apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, yields: % 23.31/6.34 | (120) all_36_0_40 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (29) with all_38_0_41, all_28_0_33, all_0_2_2, all_0_1_1, all_0_0_0, all_26_1_32 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, yields: % 23.31/6.35 | (121) all_38_0_41 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (31) with all_38_0_41, all_28_0_33, all_0_2_2, all_0_0_0, all_0_1_1, all_26_1_32 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, yields: % 23.31/6.35 | (122) all_38_0_41 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (83) with all_28_0_33, all_28_0_33, all_0_0_0, all_0_0_0, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, yields: % 23.31/6.35 | (123) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & convergent_lines(all_0_0_0, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (20) with all_28_0_33, all_28_0_33, all_0_0_0, all_0_0_0, all_26_1_32, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, yields: % 23.31/6.35 | (124) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (29) with all_36_0_40, all_26_0_31, all_0_1_1, all_0_0_0, all_0_2_2, all_26_1_32 and discharging atoms unorthogonal_lines(all_0_0_0, all_0_1_1) = all_36_0_40, apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (125) all_36_0_40 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (31) with all_36_0_40, all_26_0_31, all_0_1_1, all_0_2_2, all_0_0_0, all_26_1_32 and discharging atoms unorthogonal_lines(all_0_0_0, all_0_1_1) = all_36_0_40, apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (126) all_36_0_40 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (29) with all_38_0_41, all_26_0_31, all_0_2_2, all_0_1_1, all_0_2_2, all_26_1_32 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (127) all_38_0_41 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_1_1) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (31) with all_38_0_41, all_26_0_31, all_0_2_2, all_0_2_2, all_0_1_1, all_26_1_32 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (128) all_38_0_41 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_2_2) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (83) with all_26_0_31, all_28_0_33, all_0_2_2, all_0_0_0, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (129) all_28_0_33 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & convergent_lines(all_0_0_0, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (83) with all_28_0_33, all_26_0_31, all_0_0_0, all_0_2_2, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (130) all_28_0_33 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & convergent_lines(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (20) with all_26_0_31, all_28_0_33, all_0_2_2, all_0_0_0, all_26_1_32, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (131) all_28_0_33 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (20) with all_28_0_33, all_26_0_31, all_0_0_0, all_0_2_2, all_26_1_32, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (132) all_28_0_33 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (83) with all_26_0_31, all_26_0_31, all_0_2_2, all_0_2_2, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (133) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & convergent_lines(all_0_2_2, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_2_2) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (20) with all_26_0_31, all_26_0_31, all_0_2_2, all_0_2_2, all_26_1_32, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, yields: % 23.31/6.35 | (134) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (29) with all_36_0_40, all_34_0_39, all_0_1_1, all_0_0_0, all_0_0_0, all_0_3_3 and discharging atoms unorthogonal_lines(all_0_0_0, all_0_1_1) = all_36_0_40, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.35 | (135) all_36_0_40 = 0 | all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (29) with all_38_0_41, all_34_0_39, all_0_2_2, all_0_1_1, all_0_0_0, all_0_3_3 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.35 | (136) all_38_0_41 = 0 | all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.35 | % 23.31/6.35 | Instantiating formula (31) with all_38_0_41, all_34_0_39, all_0_2_2, all_0_0_0, all_0_1_1, all_0_3_3 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.35 | (137) all_38_0_41 = 0 | all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_34_0_39, all_28_0_33, all_0_0_0, all_0_0_0, all_0_3_3, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.36 | (138) all_34_0_39 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_28_0_33, all_34_0_39, all_0_0_0, all_0_0_0, all_26_1_32, all_0_3_3 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.36 | (139) all_34_0_39 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_34_0_39, all_26_0_31, all_0_0_0, all_0_2_2, all_0_3_3, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.36 | (140) all_34_0_39 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_26_0_31, all_34_0_39, all_0_2_2, all_0_0_0, all_26_1_32, all_0_3_3 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.36 | (141) all_34_0_39 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (10) with all_34_0_39, all_26_0_31, all_0_2_2, all_0_0_0, all_0_3_3, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.36 | (142) all_34_0_39 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (10) with all_26_0_31, all_34_0_39, all_0_0_0, all_0_2_2, all_26_1_32, all_0_3_3 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.36 | (143) all_34_0_39 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (83) with all_34_0_39, all_34_0_39, all_0_0_0, all_0_0_0, all_0_3_3 and discharging atoms apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.36 | (144) all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & convergent_lines(all_0_0_0, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_34_0_39, all_34_0_39, all_0_0_0, all_0_0_0, all_0_3_3, all_0_3_3 and discharging atoms apart_point_and_line(all_0_3_3, all_0_0_0) = all_34_0_39, yields: % 23.31/6.36 | (145) all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (31) with all_36_0_40, all_32_0_38, all_0_1_1, all_0_1_1, all_0_0_0, all_0_3_3 and discharging atoms unorthogonal_lines(all_0_0_0, all_0_1_1) = all_36_0_40, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (146) all_36_0_40 = 0 | all_32_0_38 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_1_1, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (29) with all_38_0_41, all_32_0_38, all_0_2_2, all_0_1_1, all_0_1_1, all_0_3_3 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (147) all_38_0_41 = 0 | all_32_0_38 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_1_1, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_1_1) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_32_0_38, all_28_0_33, all_0_1_1, all_0_0_0, all_0_3_3, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (148) all_32_0_38 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_28_0_33, all_32_0_38, all_0_0_0, all_0_1_1, all_26_1_32, all_0_3_3 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (149) all_32_0_38 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (10) with all_32_0_38, all_28_0_33, all_0_0_0, all_0_1_1, all_0_3_3, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (150) all_32_0_38 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (10) with all_28_0_33, all_32_0_38, all_0_1_1, all_0_0_0, all_26_1_32, all_0_3_3 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (151) all_32_0_38 = 0 | all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_32_0_38, all_26_0_31, all_0_1_1, all_0_2_2, all_0_3_3, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (152) all_32_0_38 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_26_0_31, all_32_0_38, all_0_2_2, all_0_1_1, all_26_1_32, all_0_3_3 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (153) all_32_0_38 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (10) with all_32_0_38, all_26_0_31, all_0_2_2, all_0_1_1, all_0_3_3, all_26_1_32 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (154) all_32_0_38 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (10) with all_26_0_31, all_32_0_38, all_0_1_1, all_0_2_2, all_26_1_32, all_0_3_3 and discharging atoms apart_point_and_line(all_26_1_32, all_0_2_2) = all_26_0_31, apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (155) all_32_0_38 = 0 | all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (83) with all_32_0_38, all_32_0_38, all_0_1_1, all_0_1_1, all_0_3_3 and discharging atoms apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (156) all_32_0_38 = 0 | ? [v0] : ((v0 = 0 & convergent_lines(all_0_1_1, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_1_1) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating formula (20) with all_32_0_38, all_32_0_38, all_0_1_1, all_0_1_1, all_0_3_3, all_0_3_3 and discharging atoms apart_point_and_line(all_0_3_3, all_0_1_1) = all_32_0_38, yields: % 23.31/6.36 | (157) all_32_0_38 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_0_3_3) = v0)) % 23.31/6.36 | % 23.31/6.36 | Instantiating (118) with all_50_0_43, all_50_1_44 yields: % 23.31/6.36 | (158) (all_50_0_43 = 0 & all_50_1_44 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0 & convergent_lines(all_0_2_2, all_0_1_1) = 0) | (all_50_1_44 = 0 & all_36_0_40 = 0 & convergent_lines(all_0_0_0, all_0_1_1) = 0) | ( ~ (all_50_1_44 = 0) & unorthogonal_lines(all_0_2_2, all_0_0_0) = all_50_1_44) % 23.31/6.36 | % 23.31/6.36 +-Applying beta-rule and splitting (102), into two cases. % 23.31/6.36 |-Branch one: % 23.31/6.36 | (159) (all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_30_0_35 = 0) & unorthogonal_lines(all_0_2_2, all_0_2_2) = all_30_0_35) % 23.31/6.36 | % 23.31/6.36 +-Applying beta-rule and splitting (159), into two cases. % 23.31/6.36 |-Branch one: % 23.31/6.36 | (160) all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_0_0) = 0 % 23.31/6.36 | % 23.31/6.36 | Applying alpha-rule on (160) yields: % 23.31/6.36 | (161) all_30_0_35 = 0 % 23.31/6.36 | (162) unorthogonal_lines(all_0_2_2, all_0_0_0) = 0 % 23.31/6.36 | % 23.31/6.37 +-Applying beta-rule and splitting (103), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (163) (all_31_0_36 = 0 & all_31_1_37 = 0 & unorthogonal_lines(all_0_0_0, all_0_0_0) = 0 & convergent_lines(all_0_0_0, all_0_0_0) = 0) | (all_31_1_37 = 0 & unorthogonal_lines(all_0_2_2, all_0_0_0) = 0) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (163), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (164) all_31_0_36 = 0 & all_31_1_37 = 0 & unorthogonal_lines(all_0_0_0, all_0_0_0) = 0 & convergent_lines(all_0_0_0, all_0_0_0) = 0 % 23.31/6.37 | % 23.31/6.37 | Applying alpha-rule on (164) yields: % 23.31/6.37 | (165) all_31_0_36 = 0 % 23.31/6.37 | (166) all_31_1_37 = 0 % 23.31/6.37 | (167) unorthogonal_lines(all_0_0_0, all_0_0_0) = 0 % 23.31/6.37 | (168) convergent_lines(all_0_0_0, all_0_0_0) = 0 % 23.31/6.37 | % 23.31/6.37 | Instantiating formula (82) with all_0_0_0 and discharging atoms convergent_lines(all_0_0_0, all_0_0_0) = 0, yields: % 23.31/6.37 | (169) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (170) all_31_1_37 = 0 & unorthogonal_lines(all_0_2_2, all_0_0_0) = 0 % 23.31/6.37 | % 23.31/6.37 | Applying alpha-rule on (170) yields: % 23.31/6.37 | (166) all_31_1_37 = 0 % 23.31/6.37 | (162) unorthogonal_lines(all_0_2_2, all_0_0_0) = 0 % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (158), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (173) (all_50_0_43 = 0 & all_50_1_44 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0 & convergent_lines(all_0_2_2, all_0_1_1) = 0) | (all_50_1_44 = 0 & all_36_0_40 = 0 & convergent_lines(all_0_0_0, all_0_1_1) = 0) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (173), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (174) all_50_0_43 = 0 & all_50_1_44 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0 & convergent_lines(all_0_2_2, all_0_1_1) = 0 % 23.31/6.37 | % 23.31/6.37 | Applying alpha-rule on (174) yields: % 23.31/6.37 | (175) all_50_0_43 = 0 % 23.31/6.37 | (176) all_50_1_44 = 0 % 23.31/6.37 | (177) unorthogonal_lines(all_0_2_2, all_0_1_1) = 0 % 23.31/6.37 | (178) convergent_lines(all_0_2_2, all_0_1_1) = 0 % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (122), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (179) all_38_0_41 = 0 % 23.31/6.37 | % 23.31/6.37 | Equations (179) can reduce 114 to: % 23.31/6.37 | (180) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (114) ~ (all_38_0_41 = 0) % 23.31/6.37 | (182) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0)) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (127), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (179) all_38_0_41 = 0 % 23.31/6.37 | % 23.31/6.37 | Equations (179) can reduce 114 to: % 23.31/6.37 | (180) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (114) ~ (all_38_0_41 = 0) % 23.31/6.37 | (186) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_1_1) = v0)) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (128), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (179) all_38_0_41 = 0 % 23.31/6.37 | % 23.31/6.37 | Equations (179) can reduce 114 to: % 23.31/6.37 | (180) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (114) ~ (all_38_0_41 = 0) % 23.31/6.37 | (190) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_2_2) = v0)) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (136), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (179) all_38_0_41 = 0 % 23.31/6.37 | % 23.31/6.37 | Equations (179) can reduce 114 to: % 23.31/6.37 | (180) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (114) ~ (all_38_0_41 = 0) % 23.31/6.37 | (194) all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (137), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (179) all_38_0_41 = 0 % 23.31/6.37 | % 23.31/6.37 | Equations (179) can reduce 114 to: % 23.31/6.37 | (180) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (114) ~ (all_38_0_41 = 0) % 23.31/6.37 | (198) all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0)) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (121), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (179) all_38_0_41 = 0 % 23.31/6.37 | % 23.31/6.37 | Equations (179) can reduce 114 to: % 23.31/6.37 | (180) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (114) ~ (all_38_0_41 = 0) % 23.31/6.37 | (202) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (147), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (179) all_38_0_41 = 0 % 23.31/6.37 | % 23.31/6.37 | Equations (179) can reduce 114 to: % 23.31/6.37 | (180) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (114) ~ (all_38_0_41 = 0) % 23.31/6.37 | (206) all_32_0_38 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_1_1, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_1_1) = v0)) % 23.31/6.37 | % 23.31/6.37 | Instantiating formula (42) with all_38_0_41, all_0_2_2, all_0_1_1, all_0_2_2 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, convergent_lines(all_0_2_2, all_0_1_1) = 0, yields: % 23.31/6.37 | (207) ? [v0] : ? [v1] : ((v1 = 0 & v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 & convergent_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0) | ( ~ (v0 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = v0)) % 23.31/6.37 | % 23.31/6.37 | Instantiating (207) with all_381_0_145, all_381_1_146 yields: % 23.31/6.37 | (208) (all_381_0_145 = 0 & all_381_1_146 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 & convergent_lines(all_0_2_2, all_0_2_2) = 0) | (all_381_1_146 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0) | ( ~ (all_381_1_146 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = all_381_1_146) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (208), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (209) (all_381_0_145 = 0 & all_381_1_146 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 & convergent_lines(all_0_2_2, all_0_2_2) = 0) | (all_381_1_146 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0) % 23.31/6.37 | % 23.31/6.37 +-Applying beta-rule and splitting (209), into two cases. % 23.31/6.37 |-Branch one: % 23.31/6.37 | (210) all_381_0_145 = 0 & all_381_1_146 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 & convergent_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.37 | % 23.31/6.37 | Applying alpha-rule on (210) yields: % 23.31/6.37 | (211) all_381_0_145 = 0 % 23.31/6.37 | (212) all_381_1_146 = 0 % 23.31/6.37 | (213) unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.37 | (214) convergent_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.37 | % 23.31/6.37 | Instantiating formula (82) with all_0_2_2 and discharging atoms convergent_lines(all_0_2_2, all_0_2_2) = 0, yields: % 23.31/6.37 | (169) $false % 23.31/6.37 | % 23.31/6.37 |-The branch is then unsatisfiable % 23.31/6.37 |-Branch two: % 23.31/6.37 | (216) all_381_1_146 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0 % 23.31/6.37 | % 23.31/6.37 | Applying alpha-rule on (216) yields: % 23.31/6.37 | (212) all_381_1_146 = 0 % 23.31/6.37 | (179) all_38_0_41 = 0 % 23.31/6.37 | (219) convergent_lines(all_0_1_1, all_0_2_2) = 0 % 23.31/6.37 | % 23.31/6.37 | Equations (179) can reduce 114 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (221) ~ (all_381_1_146 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = all_381_1_146 % 23.31/6.38 | % 23.31/6.38 | Applying alpha-rule on (221) yields: % 23.31/6.38 | (222) ~ (all_381_1_146 = 0) % 23.31/6.38 | (223) unorthogonal_lines(all_0_2_2, all_0_1_1) = all_381_1_146 % 23.31/6.38 | % 23.31/6.38 | Instantiating formula (79) with all_0_2_2, all_0_1_1, all_381_1_146, 0 and discharging atoms unorthogonal_lines(all_0_2_2, all_0_1_1) = all_381_1_146, unorthogonal_lines(all_0_2_2, all_0_1_1) = 0, yields: % 23.31/6.38 | (212) all_381_1_146 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (212) can reduce 222 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (226) all_50_1_44 = 0 & all_36_0_40 = 0 & convergent_lines(all_0_0_0, all_0_1_1) = 0 % 23.31/6.38 | % 23.31/6.38 | Applying alpha-rule on (226) yields: % 23.31/6.38 | (176) all_50_1_44 = 0 % 23.31/6.38 | (228) all_36_0_40 = 0 % 23.31/6.38 | (229) convergent_lines(all_0_0_0, all_0_1_1) = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (228) can reduce 111 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (231) ~ (all_50_1_44 = 0) & unorthogonal_lines(all_0_2_2, all_0_0_0) = all_50_1_44 % 23.31/6.38 | % 23.31/6.38 | Applying alpha-rule on (231) yields: % 23.31/6.38 | (232) ~ (all_50_1_44 = 0) % 23.31/6.38 | (233) unorthogonal_lines(all_0_2_2, all_0_0_0) = all_50_1_44 % 23.31/6.38 | % 23.31/6.38 | Instantiating formula (79) with all_0_2_2, all_0_0_0, 0, all_50_1_44 and discharging atoms unorthogonal_lines(all_0_2_2, all_0_0_0) = all_50_1_44, unorthogonal_lines(all_0_2_2, all_0_0_0) = 0, yields: % 23.31/6.38 | (176) all_50_1_44 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (176) can reduce 232 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (236) ~ (all_31_1_37 = 0) & unorthogonal_lines(all_0_2_2, all_0_0_0) = all_31_1_37 % 23.31/6.38 | % 23.31/6.38 | Applying alpha-rule on (236) yields: % 23.31/6.38 | (237) ~ (all_31_1_37 = 0) % 23.31/6.38 | (238) unorthogonal_lines(all_0_2_2, all_0_0_0) = all_31_1_37 % 23.31/6.38 | % 23.31/6.38 | Instantiating formula (79) with all_0_2_2, all_0_0_0, 0, all_31_1_37 and discharging atoms unorthogonal_lines(all_0_2_2, all_0_0_0) = all_31_1_37, unorthogonal_lines(all_0_2_2, all_0_0_0) = 0, yields: % 23.31/6.38 | (166) all_31_1_37 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (166) can reduce 237 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (241) ~ (all_30_0_35 = 0) & unorthogonal_lines(all_0_2_2, all_0_2_2) = all_30_0_35 % 23.31/6.38 | % 23.31/6.38 | Applying alpha-rule on (241) yields: % 23.31/6.38 | (242) ~ (all_30_0_35 = 0) % 23.31/6.38 | (243) unorthogonal_lines(all_0_2_2, all_0_2_2) = all_30_0_35 % 23.31/6.38 | % 23.31/6.38 | Instantiating formula (4) with all_30_0_35, all_0_2_2, all_0_2_2 and discharging atoms unorthogonal_lines(all_0_2_2, all_0_2_2) = all_30_0_35, yields: % 23.31/6.38 | (244) all_30_0_35 = 0 | convergent_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (244), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (214) convergent_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.38 | % 23.31/6.38 | Instantiating formula (82) with all_0_2_2 and discharging atoms convergent_lines(all_0_2_2, all_0_2_2) = 0, yields: % 23.31/6.38 | (169) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (247) ~ (convergent_lines(all_0_2_2, all_0_2_2) = 0) % 23.31/6.38 | (161) all_30_0_35 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (161) can reduce 242 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (250) ~ (all_30_0_35 = 0) & convergent_lines(all_0_2_2, all_0_2_2) = all_30_0_35 % 23.31/6.38 | % 23.31/6.38 | Applying alpha-rule on (250) yields: % 23.31/6.38 | (242) ~ (all_30_0_35 = 0) % 23.31/6.38 | (252) convergent_lines(all_0_2_2, all_0_2_2) = all_30_0_35 % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (119), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (219) convergent_lines(all_0_1_1, all_0_2_2) = 0 % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (123), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (254) all_28_0_33 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (254) can reduce 99 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (99) ~ (all_28_0_33 = 0) % 23.31/6.38 | (257) ? [v0] : ((v0 = 0 & convergent_lines(all_0_0_0, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (124), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (254) all_28_0_33 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (254) can reduce 99 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (99) ~ (all_28_0_33 = 0) % 23.31/6.38 | (261) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (133), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (262) all_26_0_31 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (262) can reduce 95 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (95) ~ (all_26_0_31 = 0) % 23.31/6.38 | (265) ? [v0] : ((v0 = 0 & convergent_lines(all_0_2_2, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_2_2) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (156), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (266) all_32_0_38 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (266) can reduce 105 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (105) ~ (all_32_0_38 = 0) % 23.31/6.38 | (269) ? [v0] : ((v0 = 0 & convergent_lines(all_0_1_1, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_1_1) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (144), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (270) all_34_0_39 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (270) can reduce 108 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (108) ~ (all_34_0_39 = 0) % 23.31/6.38 | (257) ? [v0] : ((v0 = 0 & convergent_lines(all_0_0_0, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (134), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (262) all_26_0_31 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (262) can reduce 95 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (95) ~ (all_26_0_31 = 0) % 23.31/6.38 | (277) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (145), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (270) all_34_0_39 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (270) can reduce 108 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (108) ~ (all_34_0_39 = 0) % 23.31/6.38 | (281) ? [v0] : ((v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_0_3_3) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (157), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (266) all_32_0_38 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (266) can reduce 105 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (105) ~ (all_32_0_38 = 0) % 23.31/6.38 | (285) ? [v0] : ((v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_0_3_3) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (146), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (228) all_36_0_40 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (228) can reduce 111 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (111) ~ (all_36_0_40 = 0) % 23.31/6.38 | (289) all_32_0_38 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_1_1, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (147), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (179) all_38_0_41 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (179) can reduce 114 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (114) ~ (all_38_0_41 = 0) % 23.31/6.38 | (206) all_32_0_38 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_1_1, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_1_1) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (152), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (266) all_32_0_38 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (266) can reduce 105 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (105) ~ (all_32_0_38 = 0) % 23.31/6.38 | (297) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.38 | % 23.31/6.38 +-Applying beta-rule and splitting (149), into two cases. % 23.31/6.38 |-Branch one: % 23.31/6.38 | (266) all_32_0_38 = 0 % 23.31/6.38 | % 23.31/6.38 | Equations (266) can reduce 105 to: % 23.31/6.38 | (180) $false % 23.31/6.38 | % 23.31/6.38 |-The branch is then unsatisfiable % 23.31/6.38 |-Branch two: % 23.31/6.38 | (105) ~ (all_32_0_38 = 0) % 23.31/6.38 | (301) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (135), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (228) all_36_0_40 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (228) can reduce 111 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (111) ~ (all_36_0_40 = 0) % 23.31/6.39 | (305) all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (131), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (254) all_28_0_33 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (254) can reduce 99 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (99) ~ (all_28_0_33 = 0) % 23.31/6.39 | (309) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (132), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (254) all_28_0_33 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (254) can reduce 99 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (99) ~ (all_28_0_33 = 0) % 23.31/6.39 | (313) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (136), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (179) all_38_0_41 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (179) can reduce 114 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (114) ~ (all_38_0_41 = 0) % 23.31/6.39 | (194) all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (141), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (270) all_34_0_39 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (270) can reduce 108 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (108) ~ (all_34_0_39 = 0) % 23.31/6.39 | (321) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (142), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (270) all_34_0_39 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (270) can reduce 108 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (108) ~ (all_34_0_39 = 0) % 23.31/6.39 | (325) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (140), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (270) all_34_0_39 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (270) can reduce 108 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (108) ~ (all_34_0_39 = 0) % 23.31/6.39 | (329) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (120), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (228) all_36_0_40 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (228) can reduce 111 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (111) ~ (all_36_0_40 = 0) % 23.31/6.39 | (333) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (137), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (179) all_38_0_41 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (179) can reduce 114 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (114) ~ (all_38_0_41 = 0) % 23.31/6.39 | (198) all_34_0_39 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (122), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (179) all_38_0_41 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (179) can reduce 114 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (114) ~ (all_38_0_41 = 0) % 23.31/6.39 | (182) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (125), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (228) all_36_0_40 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (228) can reduce 111 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (111) ~ (all_36_0_40 = 0) % 23.31/6.39 | (345) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (138), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (270) all_34_0_39 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (270) can reduce 108 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (108) ~ (all_34_0_39 = 0) % 23.31/6.39 | (349) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (139), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (270) all_34_0_39 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (270) can reduce 108 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (108) ~ (all_34_0_39 = 0) % 23.31/6.39 | (353) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (143), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (270) all_34_0_39 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (270) can reduce 108 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (108) ~ (all_34_0_39 = 0) % 23.31/6.39 | (357) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (126), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (228) all_36_0_40 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (228) can reduce 111 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (111) ~ (all_36_0_40 = 0) % 23.31/6.39 | (361) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (153), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (266) all_32_0_38 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (266) can reduce 105 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (105) ~ (all_32_0_38 = 0) % 23.31/6.39 | (365) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (154), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (266) all_32_0_38 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (266) can reduce 105 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (105) ~ (all_32_0_38 = 0) % 23.31/6.39 | (369) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (155), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (266) all_32_0_38 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (266) can reduce 105 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (105) ~ (all_32_0_38 = 0) % 23.31/6.39 | (373) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (150), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (266) all_32_0_38 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (266) can reduce 105 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (105) ~ (all_32_0_38 = 0) % 23.31/6.39 | (377) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (127), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (179) all_38_0_41 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (179) can reduce 114 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (114) ~ (all_38_0_41 = 0) % 23.31/6.39 | (186) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_1_1) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (121), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (179) all_38_0_41 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (179) can reduce 114 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (114) ~ (all_38_0_41 = 0) % 23.31/6.39 | (202) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (128), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (179) all_38_0_41 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (179) can reduce 114 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (114) ~ (all_38_0_41 = 0) % 23.31/6.39 | (190) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_2_2) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (148), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (266) all_32_0_38 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (266) can reduce 105 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (105) ~ (all_32_0_38 = 0) % 23.31/6.39 | (393) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.39 | % 23.31/6.39 +-Applying beta-rule and splitting (151), into two cases. % 23.31/6.39 |-Branch one: % 23.31/6.39 | (266) all_32_0_38 = 0 % 23.31/6.39 | % 23.31/6.39 | Equations (266) can reduce 105 to: % 23.31/6.39 | (180) $false % 23.31/6.39 | % 23.31/6.39 |-The branch is then unsatisfiable % 23.31/6.39 |-Branch two: % 23.31/6.39 | (105) ~ (all_32_0_38 = 0) % 23.31/6.39 | (397) all_28_0_33 = 0 | ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (130), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (401) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & convergent_lines(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (129), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (405) all_26_0_31 = 0 | ? [v0] : ((v0 = 0 & convergent_lines(all_0_0_0, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (309), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (409) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (321), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (413) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (329), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (417) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (333), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (421) ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (182), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (425) ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (345), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (429) ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (349), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (433) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (353), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (437) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (377), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (441) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (190), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (445) ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_2_2) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (393), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (449) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (297), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (453) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (301), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (457) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_1_1, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (313), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (461) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_26_1_32) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (325), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (465) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & distinct_points(all_26_1_32, all_0_3_3) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (357), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (469) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_2_2, all_0_0_0) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (361), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (262) all_26_0_31 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (262) can reduce 95 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (95) ~ (all_26_0_31 = 0) % 23.31/6.40 | (473) ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = v0)) % 23.31/6.40 | % 23.31/6.40 | Instantiating (473) with all_316_0_485 yields: % 23.31/6.40 | (474) (all_316_0_485 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0) | (all_316_0_485 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) | ( ~ (all_316_0_485 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = all_316_0_485) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (202), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (478) ? [v0] : ((v0 = 0 & unorthogonal_lines(all_0_0_0, all_0_2_2) = 0) | (v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0)) % 23.31/6.40 | % 23.31/6.40 +-Applying beta-rule and splitting (397), into two cases. % 23.31/6.40 |-Branch one: % 23.31/6.40 | (254) all_28_0_33 = 0 % 23.31/6.40 | % 23.31/6.40 | Equations (254) can reduce 99 to: % 23.31/6.40 | (180) $false % 23.31/6.40 | % 23.31/6.40 |-The branch is then unsatisfiable % 23.31/6.40 |-Branch two: % 23.31/6.40 | (99) ~ (all_28_0_33 = 0) % 23.31/6.40 | (482) ? [v0] : ((v0 = 0 & apart_point_and_line(all_26_1_32, all_0_1_1) = 0) | (v0 = 0 & apart_point_and_line(all_0_3_3, all_0_0_0) = 0) | ( ~ (v0 = 0) & distinct_lines(all_0_0_0, all_0_1_1) = v0) | ( ~ (v0 = 0) & distinct_points(all_0_3_3, all_26_1_32) = v0)) % 23.31/6.40 | % 23.31/6.40 | Instantiating formula (59) with all_30_0_35, all_0_2_2, all_0_0_0, all_0_2_2 and discharging atoms convergent_lines(all_0_2_2, all_0_0_0) = 0, convergent_lines(all_0_2_2, all_0_2_2) = all_30_0_35, yields: % 23.31/6.40 | (483) all_30_0_35 = 0 | distinct_lines(all_0_0_0, all_0_2_2) = 0 % 23.31/6.40 | % 23.31/6.40 | Instantiating formula (15) with 0, all_30_0_35, all_0_2_2, all_0_1_1, all_0_2_2 and discharging atoms convergent_lines(all_0_1_1, all_0_2_2) = 0, convergent_lines(all_0_2_2, all_0_2_2) = all_30_0_35, yields: % 23.31/6.40 | (484) ? [v0] : ((v0 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (v0 = 0 & unorthogonal_lines(all_0_1_1, all_0_2_2) = 0) | ( ~ (v0 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = v0) | ( ~ (v0 = 0) & convergent_lines(all_0_2_2, all_0_1_1) = v0)) % 23.31/6.40 | % 23.31/6.40 | Instantiating formula (2) with all_38_0_41, all_30_0_35, all_0_2_2, all_0_1_1, all_0_2_2 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, convergent_lines(all_0_2_2, all_0_2_2) = all_30_0_35, yields: % 23.31/6.40 | (485) ? [v0] : ((v0 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0) | (v0 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | ( ~ (v0 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = v0) | ( ~ (v0 = 0) & convergent_lines(all_0_2_2, all_0_1_1) = v0)) % 23.31/6.40 | % 23.31/6.40 | Instantiating (485) with all_366_0_495 yields: % 23.31/6.40 | (486) (all_366_0_495 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0) | (all_366_0_495 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | ( ~ (all_366_0_495 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = all_366_0_495) | ( ~ (all_366_0_495 = 0) & convergent_lines(all_0_2_2, all_0_1_1) = all_366_0_495) % 23.31/6.41 | % 23.31/6.41 | Instantiating (484) with all_368_0_497 yields: % 23.31/6.41 | (487) (all_368_0_497 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (all_368_0_497 = 0 & unorthogonal_lines(all_0_1_1, all_0_2_2) = 0) | ( ~ (all_368_0_497 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = all_368_0_497) | ( ~ (all_368_0_497 = 0) & convergent_lines(all_0_2_2, all_0_1_1) = all_368_0_497) % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (483), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (488) distinct_lines(all_0_0_0, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (474), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (489) (all_316_0_485 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0) | (all_316_0_485 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0) % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (489), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (490) all_316_0_485 = 0 & unorthogonal_lines(all_0_2_2, all_0_1_1) = 0 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (490) yields: % 23.31/6.41 | (491) all_316_0_485 = 0 % 23.31/6.41 | (177) unorthogonal_lines(all_0_2_2, all_0_1_1) = 0 % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (486), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (493) (all_366_0_495 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0) | (all_366_0_495 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | ( ~ (all_366_0_495 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = all_366_0_495) % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (493), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (494) (all_366_0_495 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0) | (all_366_0_495 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (494), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (495) all_366_0_495 = 0 & all_38_0_41 = 0 & convergent_lines(all_0_1_1, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (495) yields: % 23.31/6.41 | (496) all_366_0_495 = 0 % 23.31/6.41 | (179) all_38_0_41 = 0 % 23.31/6.41 | (219) convergent_lines(all_0_1_1, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (179) can reduce 114 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (500) all_366_0_495 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (500) yields: % 23.31/6.41 | (496) all_366_0_495 = 0 % 23.31/6.41 | (161) all_30_0_35 = 0 % 23.31/6.41 | (213) unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (161) can reduce 242 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (505) ~ (all_366_0_495 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = all_366_0_495 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (505) yields: % 23.31/6.41 | (506) ~ (all_366_0_495 = 0) % 23.31/6.41 | (507) unorthogonal_lines(all_0_2_2, all_0_1_1) = all_366_0_495 % 23.31/6.41 | % 23.31/6.41 | Instantiating formula (79) with all_0_2_2, all_0_1_1, 0, all_366_0_495 and discharging atoms unorthogonal_lines(all_0_2_2, all_0_1_1) = all_366_0_495, unorthogonal_lines(all_0_2_2, all_0_1_1) = 0, yields: % 23.31/6.41 | (496) all_366_0_495 = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (496) can reduce 506 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (510) ~ (all_366_0_495 = 0) & convergent_lines(all_0_2_2, all_0_1_1) = all_366_0_495 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (510) yields: % 23.31/6.41 | (506) ~ (all_366_0_495 = 0) % 23.31/6.41 | (512) convergent_lines(all_0_2_2, all_0_1_1) = all_366_0_495 % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (487), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (513) (all_368_0_497 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (all_368_0_497 = 0 & unorthogonal_lines(all_0_1_1, all_0_2_2) = 0) | ( ~ (all_368_0_497 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = all_368_0_497) % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (513), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (514) (all_368_0_497 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0) | (all_368_0_497 = 0 & unorthogonal_lines(all_0_1_1, all_0_2_2) = 0) % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (514), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (515) all_368_0_497 = 0 & all_30_0_35 = 0 & unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (515) yields: % 23.31/6.41 | (516) all_368_0_497 = 0 % 23.31/6.41 | (161) all_30_0_35 = 0 % 23.31/6.41 | (213) unorthogonal_lines(all_0_2_2, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (161) can reduce 242 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (520) all_368_0_497 = 0 & unorthogonal_lines(all_0_1_1, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (520) yields: % 23.31/6.41 | (516) all_368_0_497 = 0 % 23.31/6.41 | (522) unorthogonal_lines(all_0_1_1, all_0_2_2) = 0 % 23.31/6.41 | % 23.31/6.41 | Instantiating formula (79) with all_0_1_1, all_0_2_2, 0, all_38_0_41 and discharging atoms unorthogonal_lines(all_0_1_1, all_0_2_2) = all_38_0_41, unorthogonal_lines(all_0_1_1, all_0_2_2) = 0, yields: % 23.31/6.41 | (179) all_38_0_41 = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (179) can reduce 114 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (525) ~ (all_368_0_497 = 0) & unorthogonal_lines(all_0_2_2, all_0_1_1) = all_368_0_497 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (525) yields: % 23.31/6.41 | (526) ~ (all_368_0_497 = 0) % 23.31/6.41 | (527) unorthogonal_lines(all_0_2_2, all_0_1_1) = all_368_0_497 % 23.31/6.41 | % 23.31/6.41 | Instantiating formula (79) with all_0_2_2, all_0_1_1, 0, all_368_0_497 and discharging atoms unorthogonal_lines(all_0_2_2, all_0_1_1) = all_368_0_497, unorthogonal_lines(all_0_2_2, all_0_1_1) = 0, yields: % 23.31/6.41 | (516) all_368_0_497 = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (516) can reduce 526 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (530) ~ (all_368_0_497 = 0) & convergent_lines(all_0_2_2, all_0_1_1) = all_368_0_497 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (530) yields: % 23.31/6.41 | (526) ~ (all_368_0_497 = 0) % 23.31/6.41 | (532) convergent_lines(all_0_2_2, all_0_1_1) = all_368_0_497 % 23.31/6.41 | % 23.31/6.41 | Instantiating formula (27) with all_0_2_2, all_0_1_1, all_366_0_495, all_368_0_497 and discharging atoms convergent_lines(all_0_2_2, all_0_1_1) = all_368_0_497, convergent_lines(all_0_2_2, all_0_1_1) = all_366_0_495, yields: % 23.31/6.41 | (533) all_368_0_497 = all_366_0_495 % 23.31/6.41 | % 23.31/6.41 | Equations (533) can reduce 526 to: % 23.31/6.41 | (506) ~ (all_366_0_495 = 0) % 23.31/6.41 | % 23.31/6.41 | From (533) and (532) follows: % 23.31/6.41 | (512) convergent_lines(all_0_2_2, all_0_1_1) = all_366_0_495 % 23.31/6.41 | % 23.31/6.41 | Instantiating formula (51) with all_366_0_495, all_0_1_1, all_0_2_2, all_0_1_1 and discharging atoms convergent_lines(all_0_1_1, all_0_2_2) = 0, convergent_lines(all_0_2_2, all_0_1_1) = all_366_0_495, yields: % 23.31/6.41 | (536) all_366_0_495 = 0 | convergent_lines(all_0_1_1, all_0_1_1) = 0 % 23.31/6.41 | % 23.31/6.41 +-Applying beta-rule and splitting (536), into two cases. % 23.31/6.41 |-Branch one: % 23.31/6.41 | (537) convergent_lines(all_0_1_1, all_0_1_1) = 0 % 23.31/6.41 | % 23.31/6.41 | Instantiating formula (82) with all_0_1_1 and discharging atoms convergent_lines(all_0_1_1, all_0_1_1) = 0, yields: % 23.31/6.41 | (169) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (539) ~ (convergent_lines(all_0_1_1, all_0_1_1) = 0) % 23.31/6.41 | (496) all_366_0_495 = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (496) can reduce 506 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (542) all_316_0_485 = 0 & apart_point_and_line(all_26_1_32, all_0_0_0) = 0 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (542) yields: % 23.31/6.41 | (491) all_316_0_485 = 0 % 23.31/6.41 | (544) apart_point_and_line(all_26_1_32, all_0_0_0) = 0 % 23.31/6.41 | % 23.31/6.41 | Instantiating formula (11) with all_26_1_32, all_0_0_0, 0, all_28_0_33 and discharging atoms apart_point_and_line(all_26_1_32, all_0_0_0) = all_28_0_33, apart_point_and_line(all_26_1_32, all_0_0_0) = 0, yields: % 23.31/6.41 | (254) all_28_0_33 = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (254) can reduce 99 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (547) ~ (all_316_0_485 = 0) & distinct_lines(all_0_0_0, all_0_2_2) = all_316_0_485 % 23.31/6.41 | % 23.31/6.41 | Applying alpha-rule on (547) yields: % 23.31/6.41 | (548) ~ (all_316_0_485 = 0) % 23.31/6.41 | (549) distinct_lines(all_0_0_0, all_0_2_2) = all_316_0_485 % 23.31/6.41 | % 23.31/6.41 | Instantiating formula (50) with all_0_0_0, all_0_2_2, 0, all_316_0_485 and discharging atoms distinct_lines(all_0_0_0, all_0_2_2) = all_316_0_485, distinct_lines(all_0_0_0, all_0_2_2) = 0, yields: % 23.31/6.41 | (491) all_316_0_485 = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (491) can reduce 548 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.41 |-Branch two: % 23.31/6.41 | (552) ~ (distinct_lines(all_0_0_0, all_0_2_2) = 0) % 23.31/6.41 | (161) all_30_0_35 = 0 % 23.31/6.41 | % 23.31/6.41 | Equations (161) can reduce 242 to: % 23.31/6.41 | (180) $false % 23.31/6.41 | % 23.31/6.41 |-The branch is then unsatisfiable % 23.31/6.42 |-Branch two: % 23.31/6.42 | (555) ~ (convergent_lines(all_0_1_1, all_0_2_2) = 0) % 23.31/6.42 | (179) all_38_0_41 = 0 % 23.31/6.42 | % 23.31/6.42 | Equations (179) can reduce 114 to: % 23.31/6.42 | (180) $false % 23.31/6.42 | % 23.31/6.42 |-The branch is then unsatisfiable % 23.31/6.42 % SZS output end Proof for theBenchmark % 23.31/6.42 % 23.31/6.42 5813ms %------------------------------------------------------------------------------