%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GEO213+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n028.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:47 EDT 2022 % Result : Theorem 21.07s 5.61s % Output : Proof 28.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : GEO213+1 : TPTP v8.1.0. Released v3.3.0. % 0.13/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.14/0.34 % Computer : n028.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sat Jun 18 00:25:58 EDT 2022 % 0.14/0.34 % CPUTime : % 0.57/0.60 ____ _ % 0.57/0.60 ___ / __ \_____(_)___ ________ __________ % 0.57/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.57/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.57/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.57/0.60 % 0.57/0.60 A Theorem Prover for First-Order Logic % 0.57/0.60 (ePrincess v.1.0) % 0.57/0.60 % 0.57/0.60 (c) Philipp Rümmer, 2009-2015 % 0.57/0.60 (c) Peter Backeman, 2014-2015 % 0.57/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.57/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.57/0.60 Bug reports to peter@backeman.se % 0.57/0.60 % 0.57/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.57/0.60 % 0.57/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.76/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.74/0.98 Prover 0: Preprocessing ... % 2.10/1.14 Prover 0: Warning: ignoring some quantifiers % 2.10/1.16 Prover 0: Constructing countermodel ... % 3.89/1.55 Prover 0: gave up % 3.89/1.56 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 3.89/1.58 Prover 1: Preprocessing ... % 4.34/1.67 Prover 1: Constructing countermodel ... % 4.71/1.74 Prover 1: gave up % 4.71/1.74 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 4.71/1.76 Prover 2: Preprocessing ... % 5.21/1.90 Prover 2: Warning: ignoring some quantifiers % 5.21/1.91 Prover 2: Constructing countermodel ... % 14.14/3.98 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 14.14/4.01 Prover 3: Preprocessing ... % 14.35/4.04 Prover 3: Warning: ignoring some quantifiers % 14.35/4.04 Prover 3: Constructing countermodel ... % 14.88/4.17 Prover 3: gave up % 14.88/4.17 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 15.09/4.19 Prover 4: Preprocessing ... % 15.48/4.28 Prover 4: Warning: ignoring some quantifiers % 15.58/4.29 Prover 4: Constructing countermodel ... % 19.34/5.21 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 19.48/5.24 Prover 5: Preprocessing ... % 19.48/5.32 Prover 5: Constructing countermodel ... % 21.07/5.61 Prover 5: proved (405ms) % 21.07/5.61 Prover 4: stopped % 21.07/5.61 Prover 2: stopped % 21.07/5.61 % 21.07/5.61 No countermodel exists, formula is valid % 21.07/5.61 % SZS status Theorem for theBenchmark % 21.07/5.61 % 21.07/5.61 Generating proof ... found it (size 205) % 27.27/7.12 % 27.27/7.12 % SZS output start Proof for theBenchmark % 27.27/7.12 Assumed formulas after preprocessing and simplification: % 27.27/7.12 | (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] : ? [v7] : (unorthogonal_lines(v1, v3) = v7 & apart_point_and_line(v0, v1) = v6 & (v7 = 0 | v6 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v2, v3) = v5) | ~ (apart_point_and_line(v0, v1) = v4) | ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v1, v3) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_lines(v1, v2) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v1, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v2, v3) = v8 & apart_point_and_line(v0, v1) = v7 & distinct_lines(v1, v2) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [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] : ? [v7] : (unorthogonal_lines(v2, v3) = v7 & apart_point_and_line(v0, v2) = v6 & (v7 = 0 | v6 = 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] : ? [v7] : ? [v8] : (apart_point_and_line(v0, v3) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_lines(v2, v3) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [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] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v2) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [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] : ? [v7] : ? [v8] : ? [v9] : (apart_point_and_line(v1, v2) = v9 & apart_point_and_line(v0, v3) = v8 & distinct_lines(v2, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0 | v8 = 0))) & ! [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] : ? [v7] : ? [v8] : ? [v9] : (apart_point_and_line(v1, v3) = v9 & apart_point_and_line(v0, v2) = v8 & distinct_lines(v2, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0 | v8 = 0))) & ! [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] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v3) = v8 & apart_point_and_line(v0, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [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] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v3) = v8 & apart_point_and_line(v1, v2) = v7 & distinct_lines(v2, v3) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [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] : ? [v6] : (convergent_lines(v1, v2) = v6 & distinct_lines(v1, v2) = v5 & ( ~ (v5 = 0) | v6 = 0))) & ! [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] : ? [v6] : (apart_point_and_line(v0, v1) = v6 & distinct_lines(v1, v2) = v5 & ( ~ (v5 = 0) | v6 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v1) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ? [v6] : (apart_point_and_line(v0, v2) = v6 & distinct_lines(v1, v2) = v5 & ( ~ (v5 = 0) | v6 = 0))) & ! [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] : ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v0, v1) = v6 & convergent_lines(v1, v2) = v8 & convergent_lines(v0, v2) = v7 & convergent_lines(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v8 = 0 & v4 = 0) | (v7 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v0, v2) = v7 & unorthogonal_lines(v0, v1) = v6 & convergent_lines(v1, v2) = v8 & convergent_lines(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v8 = 0 & v4 = 0) | (v7 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v1, v2) = v8 & unorthogonal_lines(v0, v1) = v6 & convergent_lines(v0, v2) = v7 & convergent_lines(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v8 = 0 & v4 = 0) | (v7 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v1, v2) = v8 & unorthogonal_lines(v0, v2) = v7 & unorthogonal_lines(v0, v1) = v6 & convergent_lines(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v8 = 0 & v4 = 0) | (v7 = 0 & v3 = 0)))) & ! [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] : ? [v5] : (apart_point_and_line(v0, v1) = v4 & convergent_lines(v1, v2) = v5 & (v5 = 0 | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = v3) | ~ (distinct_lines(v1, v2) = 0) | ? [v4] : ? [v5] : (apart_point_and_line(v0, v2) = v4 & convergent_lines(v1, v2) = v5 & (v5 = 0 | v4 = 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] : ? [v6] : ? [v7] : (unorthogonal_lines(v0, v2) = v6 & convergent_lines(v1, v2) = v7 & convergent_lines(v0, v2) = v5 & convergent_lines(v0, v1) = v4 & ( ~ (v4 = 0) | (v7 = 0 & v3 = 0) | (v6 = 0 & v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v0, v2) = v6 & unorthogonal_lines(v0, v1) = v4 & convergent_lines(v1, v2) = v7 & convergent_lines(v0, v2) = v5 & ( ~ (v4 = 0) | (v7 = 0 & v3 = 0) | (v6 = 0 & v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (unorthogonal_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & convergent_lines(v1, v2) = v6 & convergent_lines(v0, v2) = v5 & convergent_lines(v0, v1) = v4 & ( ~ (v4 = 0) | (v7 = 0 & v6 = 0) | (v5 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v1) = v4 & convergent_lines(v1, v2) = v6 & convergent_lines(v0, v2) = v5 & ( ~ (v4 = 0) | (v7 = 0 & v6 = 0) | (v5 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v1) = 0) | ~ (convergent_lines(v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v2) = v6 & convergent_lines(v0, v2) = v5 & convergent_lines(v0, v1) = v4 & ( ~ (v4 = 0) | (v7 = 0 & v3 = 0) | (v6 = 0 & v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v1) = 0) | ~ (convergent_lines(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v2) = v5 & convergent_lines(v1, v2) = v6 & convergent_lines(v0, v1) = v4 & ( ~ (v4 = 0) | (v7 = 0 & v6 = 0) | (v5 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v2) = v6 & unorthogonal_lines(v0, v1) = v4 & convergent_lines(v0, v2) = v5 & ( ~ (v4 = 0) | (v7 = 0 & v3 = 0) | (v6 = 0 & v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v2) = v5 & unorthogonal_lines(v0, v1) = v4 & convergent_lines(v1, v2) = v6 & ( ~ (v4 = 0) | (v7 = 0 & v6 = 0) | (v5 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_lines(v2, v3) = 0) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v1, v3) = v7 & apart_point_and_line(v1, v2) = v6 & apart_point_and_line(v0, v3) = v5 & apart_point_and_line(v0, v2) = v4 & (v7 = 0 | v6 = 0 | v5 = 0 | v4 = 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] : ? [v4] : (apart_point_and_line(v2, v1) = v4 & convergent_lines(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v2, v0) = v4 & convergent_lines(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v1, v2) = v4 & distinct_points(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v0, v2) = v4 & distinct_points(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [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] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & ~ (v3 = 0) & unorthogonal_lines(v1, v2) = v4 & unorthogonal_lines(v0, v1) = 0 & distinct_lines(v0, v2) = v3) % 27.27/7.17 | Applying alpha-rule on (0) yields: % 27.27/7.17 | (1) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (unorthogonal_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & convergent_lines(v1, v2) = v6 & convergent_lines(v0, v2) = v5 & convergent_lines(v0, v1) = v4 & ( ~ (v4 = 0) | (v7 = 0 & v6 = 0) | (v5 = 0 & v3 = 0)))) % 27.27/7.17 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ (parallel_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & apart_point_and_line(v0, v2) = v3)) % 27.27/7.17 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) % 27.27/7.17 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v1) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ? [v6] : (apart_point_and_line(v0, v2) = v6 & distinct_lines(v1, v2) = v5 & ( ~ (v5 = 0) | v6 = 0))) % 27.27/7.17 | (5) ! [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] : ? [v7] : ? [v8] : ? [v9] : (apart_point_and_line(v1, v2) = v9 & apart_point_and_line(v0, v3) = v8 & distinct_lines(v2, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0 | v8 = 0))) % 27.27/7.17 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v1) = 0) | ~ (convergent_lines(v0, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v2) = v5 & convergent_lines(v1, v2) = v6 & convergent_lines(v0, v1) = v4 & ( ~ (v4 = 0) | (v7 = 0 & v6 = 0) | (v5 = 0 & v3 = 0)))) % 27.27/7.17 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v1, v2) = v4) | ~ (unorthogonal_lines(v0, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v0, v1) = v6 & convergent_lines(v1, v2) = v8 & convergent_lines(v0, v2) = v7 & convergent_lines(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v8 = 0 & v4 = 0) | (v7 = 0 & v3 = 0)))) % 27.27/7.17 | (8) ! [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] : ? [v7] : (unorthogonal_lines(v1, v3) = v7 & apart_point_and_line(v0, v1) = v6 & (v7 = 0 | v6 = 0))) % 27.27/7.17 | (9) ! [v0] : ! [v1] : ! [v2] : ( ~ (orthogonal_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & unorthogonal_lines(v2, v1) = v3)) % 27.27/7.17 | (10) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v0) = v3)) % 27.27/7.17 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v0, v2) = v4 & distinct_points(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 27.27/7.17 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_lines(v2, v3) = 0) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v1, v3) = v7 & apart_point_and_line(v1, v2) = v6 & apart_point_and_line(v0, v3) = v5 & apart_point_and_line(v0, v2) = v4 & (v7 = 0 | v6 = 0 | v5 = 0 | v4 = 0))) % 27.27/7.17 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) % 27.27/7.17 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) % 27.27/7.17 | (15) ! [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] : ? [v7] : ? [v8] : (apart_point_and_line(v0, v3) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_lines(v2, v3) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 27.27/7.17 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v2, v1) = v4 & convergent_lines(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 27.27/7.17 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v0, v2) = v7 & unorthogonal_lines(v0, v1) = v6 & convergent_lines(v1, v2) = v8 & convergent_lines(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v8 = 0 & v4 = 0) | (v7 = 0 & v3 = 0)))) % 27.27/7.17 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | convergent_lines(v0, v2) = 0) % 27.27/7.17 | (19) ! [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)) % 27.27/7.18 | (20) ! [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) % 27.27/7.18 | (21) ! [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) % 27.27/7.18 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (distinct_lines(v1, v2) = 0) | ? [v4] : ? [v5] : (apart_point_and_line(v0, v1) = v4 & convergent_lines(v1, v2) = v5 & (v5 = 0 | v4 = 0))) % 27.27/7.18 | (23) ! [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] : ? [v7] : (unorthogonal_lines(v2, v3) = v7 & apart_point_and_line(v0, v2) = v6 & (v7 = 0 | v6 = 0))) % 27.27/7.18 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v2) = v6 & unorthogonal_lines(v0, v1) = v4 & convergent_lines(v0, v2) = v5 & ( ~ (v4 = 0) | (v7 = 0 & v3 = 0) | (v6 = 0 & v5 = 0)))) % 27.27/7.18 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v1, v2) = v3) | ~ (unorthogonal_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v0, v2) = v6 & convergent_lines(v1, v2) = v7 & convergent_lines(v0, v2) = v5 & convergent_lines(v0, v1) = v4 & ( ~ (v4 = 0) | (v7 = 0 & v3 = 0) | (v6 = 0 & v5 = 0)))) % 27.27/7.18 | (26) ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v1, v2) = v3)) % 27.27/7.18 | (27) ! [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) % 27.27/7.18 | (28) ! [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] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v2) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 27.27/7.18 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v0, v2) = v6 & unorthogonal_lines(v0, v1) = v4 & convergent_lines(v1, v2) = v7 & convergent_lines(v0, v2) = v5 & ( ~ (v4 = 0) | (v7 = 0 & v3 = 0) | (v6 = 0 & v5 = 0)))) % 27.27/7.18 | (30) ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v1, v2) = v4 & distinct_points(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 27.27/7.18 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) % 27.27/7.18 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (unorthogonal_lines(v3, v2) = v1) | ~ (unorthogonal_lines(v3, v2) = v0)) % 27.27/7.18 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 27.27/7.18 | (34) ! [v0] : ! [v1] : ! [v2] : ( ~ (parallel_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v2, v1) = v3)) % 27.27/7.18 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v1) = v4 & convergent_lines(v1, v2) = v6 & convergent_lines(v0, v2) = v5 & ( ~ (v4 = 0) | (v7 = 0 & v6 = 0) | (v5 = 0 & v3 = 0)))) % 27.27/7.18 | (36) ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v0, v2) = v3)) % 27.79/7.18 | (37) ! [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)) % 27.79/7.18 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v2, v3) = v5) | ~ (apart_point_and_line(v0, v1) = v4) | ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v1, v3) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_lines(v1, v2) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 27.79/7.18 | (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] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v3) = v8 & apart_point_and_line(v0, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 27.79/7.18 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 27.79/7.18 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (orthogonal_through_point(v3, v2) = v1) | ~ (orthogonal_through_point(v3, v2) = v0)) % 27.79/7.18 | (42) ! [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] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v3) = v8 & apart_point_and_line(v1, v2) = v7 & distinct_lines(v2, v3) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 27.79/7.19 | (43) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v1) = v3)) % 27.79/7.19 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) % 27.79/7.19 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) % 27.79/7.19 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (unorthogonal_lines(v0, v1) = 0) | ~ (convergent_lines(v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v2) = v6 & convergent_lines(v0, v2) = v5 & convergent_lines(v0, v1) = v4 & ( ~ (v4 = 0) | (v7 = 0 & v3 = 0) | (v6 = 0 & v5 = 0)))) % 27.79/7.19 | (47) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (unorthogonal_lines(v1, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v2, v3) = v8 & apart_point_and_line(v0, v1) = v7 & distinct_lines(v1, v2) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 27.79/7.19 | (48) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (convergent_lines(v0, v1) = v2) | unorthogonal_lines(v0, v1) = 0) % 27.79/7.19 | (49) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (unorthogonal_lines(v0, v1) = v2) | convergent_lines(v0, v1) = 0) % 27.79/7.19 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) % 27.79/7.19 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v4) | ~ (apart_point_and_line(v0, v1) = v3) | ? [v5] : ? [v6] : (convergent_lines(v1, v2) = v6 & distinct_lines(v1, v2) = v5 & ( ~ (v5 = 0) | v6 = 0))) % 27.79/7.19 | (52) ! [v0] : ~ (distinct_lines(v0, v0) = 0) % 27.79/7.19 | (53) ! [v0] : ~ (distinct_points(v0, v0) = 0) % 27.79/7.19 | (54) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (unorthogonal_lines(v1, v2) = v7 & unorthogonal_lines(v0, v2) = v5 & unorthogonal_lines(v0, v1) = v4 & convergent_lines(v1, v2) = v6 & ( ~ (v4 = 0) | (v7 = 0 & v6 = 0) | (v5 = 0 & v3 = 0)))) % 27.79/7.19 | (55) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ? [v6] : (apart_point_and_line(v0, v1) = v6 & distinct_lines(v1, v2) = v5 & ( ~ (v5 = 0) | v6 = 0))) % 27.79/7.19 | (56) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = v3) | ~ (distinct_lines(v1, v2) = 0) | ? [v4] : ? [v5] : (apart_point_and_line(v0, v2) = v4 & convergent_lines(v1, v2) = v5 & (v5 = 0 | v4 = 0))) % 27.79/7.19 | (57) ! [v0] : ! [v1] : ! [v2] : ( ~ (orthogonal_through_point(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & apart_point_and_line(v0, v2) = v3)) % 27.79/7.19 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) % 27.79/7.19 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v1, v2) = v8 & unorthogonal_lines(v0, v2) = v7 & unorthogonal_lines(v0, v1) = v6 & convergent_lines(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v8 = 0 & v4 = 0) | (v7 = 0 & v3 = 0)))) % 27.79/7.19 | (60) ! [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)) % 27.79/7.19 | (61) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = 0) & ~ (v3 = 0) & unorthogonal_lines(v1, v2) = v4 & unorthogonal_lines(v0, v1) = 0 & distinct_lines(v0, v2) = v3) % 27.79/7.19 | (62) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (parallel_through_point(v3, v2) = v1) | ~ (parallel_through_point(v3, v2) = v0)) % 27.79/7.19 | (63) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) % 27.79/7.19 | (64) ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v2, v0) = v4 & convergent_lines(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 27.79/7.19 | (65) ! [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)) % 27.79/7.19 | (66) ! [v0] : ~ (convergent_lines(v0, v0) = 0) % 27.79/7.19 | (67) ! [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] : ? [v7] : ? [v8] : ? [v9] : (apart_point_and_line(v1, v3) = v9 & apart_point_and_line(v0, v2) = v8 & distinct_lines(v2, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0 | v8 = 0))) % 27.79/7.19 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) % 27.79/7.20 | (69) ! [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) % 27.79/7.20 | (70) ! [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)) % 27.79/7.20 | (71) ! [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)) % 27.79/7.20 | (72) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 27.79/7.20 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (unorthogonal_lines(v0, v2) = v3) | ~ (convergent_lines(v1, v2) = v4) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (unorthogonal_lines(v1, v2) = v8 & unorthogonal_lines(v0, v1) = v6 & convergent_lines(v0, v2) = v7 & convergent_lines(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v8 = 0 & v4 = 0) | (v7 = 0 & v3 = 0)))) % 27.79/7.20 | % 27.79/7.20 | Instantiating (61) with all_1_0_0, all_1_1_1, all_1_2_2, all_1_3_3, all_1_4_4 yields: % 27.79/7.20 | (74) ~ (all_1_0_0 = 0) & ~ (all_1_1_1 = 0) & unorthogonal_lines(all_1_3_3, all_1_2_2) = all_1_0_0 & unorthogonal_lines(all_1_4_4, all_1_3_3) = 0 & distinct_lines(all_1_4_4, all_1_2_2) = all_1_1_1 % 27.79/7.20 | % 27.79/7.20 | Applying alpha-rule on (74) yields: % 27.79/7.20 | (75) distinct_lines(all_1_4_4, all_1_2_2) = all_1_1_1 % 27.79/7.20 | (76) unorthogonal_lines(all_1_4_4, all_1_3_3) = 0 % 27.79/7.20 | (77) ~ (all_1_0_0 = 0) % 27.79/7.20 | (78) ~ (all_1_1_1 = 0) % 27.79/7.20 | (79) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_1_0_0 % 27.79/7.20 | % 27.79/7.20 | Instantiating formula (7) with all_1_0_0, all_1_0_0, all_1_2_2, all_1_3_3, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_2_2) = all_1_0_0, yields: % 27.79/7.20 | (80) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_3_3) = v1 & convergent_lines(all_1_3_3, all_1_2_2) = v3 & convergent_lines(all_1_3_3, all_1_2_2) = v2 & convergent_lines(all_1_3_3, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & all_1_0_0 = 0) | (v2 = 0 & all_1_0_0 = 0))) % 27.79/7.20 | % 27.79/7.20 | Instantiating formula (49) with all_1_0_0, all_1_2_2, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_2_2) = all_1_0_0, yields: % 27.79/7.20 | (81) all_1_0_0 = 0 | convergent_lines(all_1_3_3, all_1_2_2) = 0 % 27.79/7.20 | % 27.79/7.20 | Instantiating formula (7) with 0, 0, all_1_3_3, all_1_4_4, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, yields: % 27.79/7.20 | (82) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_4_4, all_1_4_4) = v1 & convergent_lines(all_1_4_4, all_1_3_3) = v3 & convergent_lines(all_1_4_4, all_1_3_3) = v2 & convergent_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 27.79/7.20 | % 27.79/7.20 | Instantiating formula (1) with 0, all_1_3_3, all_1_3_3, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, yields: % 27.79/7.20 | (83) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_3_3) = v3 & convergent_lines(all_1_3_3, all_1_3_3) = v2 & convergent_lines(all_1_4_4, all_1_3_3) = v1 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & ( ~ (v0 = 0) | v1 = 0 | (v3 = 0 & v2 = 0))) % 27.79/7.20 | % 27.79/7.20 | Instantiating formula (25) with all_1_0_0, all_1_2_2, all_1_3_3, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_2_2) = all_1_0_0, unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, yields: % 27.79/7.20 | (84) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_4_4, all_1_2_2) = v2 & convergent_lines(all_1_3_3, all_1_2_2) = v3 & convergent_lines(all_1_4_4, all_1_2_2) = v1 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & ( ~ (v0 = 0) | (v3 = 0 & all_1_0_0 = 0) | (v2 = 0 & v1 = 0))) % 27.79/7.20 | % 27.79/7.20 | Instantiating formula (60) with all_1_1_1, all_1_1_1, all_1_2_2, all_1_4_4, all_1_4_4 and discharging atoms distinct_lines(all_1_4_4, all_1_2_2) = all_1_1_1, yields: % 27.79/7.20 | (85) all_1_1_1 = 0 | ? [v0] : ( ~ (v0 = 0) & distinct_lines(all_1_4_4, all_1_4_4) = v0) % 27.79/7.20 | % 27.79/7.20 | Instantiating (84) with all_8_0_5, all_8_1_6, all_8_2_7, all_8_3_8 yields: % 27.79/7.20 | (86) unorthogonal_lines(all_1_4_4, all_1_2_2) = all_8_1_6 & convergent_lines(all_1_3_3, all_1_2_2) = all_8_0_5 & convergent_lines(all_1_4_4, all_1_2_2) = all_8_2_7 & convergent_lines(all_1_4_4, all_1_3_3) = all_8_3_8 & ( ~ (all_8_3_8 = 0) | (all_8_0_5 = 0 & all_1_0_0 = 0) | (all_8_1_6 = 0 & all_8_2_7 = 0)) % 27.79/7.20 | % 27.79/7.20 | Applying alpha-rule on (86) yields: % 27.79/7.20 | (87) convergent_lines(all_1_4_4, all_1_3_3) = all_8_3_8 % 27.79/7.20 | (88) convergent_lines(all_1_4_4, all_1_2_2) = all_8_2_7 % 27.79/7.20 | (89) ~ (all_8_3_8 = 0) | (all_8_0_5 = 0 & all_1_0_0 = 0) | (all_8_1_6 = 0 & all_8_2_7 = 0) % 27.79/7.20 | (90) unorthogonal_lines(all_1_4_4, all_1_2_2) = all_8_1_6 % 27.79/7.20 | (91) convergent_lines(all_1_3_3, all_1_2_2) = all_8_0_5 % 27.79/7.20 | % 27.79/7.20 | Instantiating (82) with all_10_0_9, all_10_1_10, all_10_2_11, all_10_3_12 yields: % 27.79/7.20 | (92) unorthogonal_lines(all_1_4_4, all_1_4_4) = all_10_2_11 & convergent_lines(all_1_4_4, all_1_3_3) = all_10_0_9 & convergent_lines(all_1_4_4, all_1_3_3) = all_10_1_10 & convergent_lines(all_1_4_4, all_1_4_4) = all_10_3_12 & ( ~ (all_10_2_11 = 0) | ~ (all_10_3_12 = 0) | all_10_0_9 = 0 | all_10_1_10 = 0) % 27.79/7.20 | % 27.79/7.20 | Applying alpha-rule on (92) yields: % 27.79/7.20 | (93) convergent_lines(all_1_4_4, all_1_3_3) = all_10_0_9 % 27.79/7.20 | (94) convergent_lines(all_1_4_4, all_1_3_3) = all_10_1_10 % 27.79/7.20 | (95) unorthogonal_lines(all_1_4_4, all_1_4_4) = all_10_2_11 % 27.79/7.20 | (96) ~ (all_10_2_11 = 0) | ~ (all_10_3_12 = 0) | all_10_0_9 = 0 | all_10_1_10 = 0 % 27.79/7.20 | (97) convergent_lines(all_1_4_4, all_1_4_4) = all_10_3_12 % 27.79/7.20 | % 27.79/7.20 | Instantiating (83) with all_12_0_13, all_12_1_14, all_12_2_15, all_12_3_16 yields: % 27.79/7.20 | (98) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13 & convergent_lines(all_1_3_3, all_1_3_3) = all_12_1_14 & convergent_lines(all_1_4_4, all_1_3_3) = all_12_2_15 & convergent_lines(all_1_4_4, all_1_3_3) = all_12_3_16 & ( ~ (all_12_3_16 = 0) | all_12_2_15 = 0 | (all_12_0_13 = 0 & all_12_1_14 = 0)) % 27.79/7.20 | % 27.79/7.20 | Applying alpha-rule on (98) yields: % 27.79/7.20 | (99) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13 % 27.79/7.20 | (100) convergent_lines(all_1_4_4, all_1_3_3) = all_12_3_16 % 27.79/7.20 | (101) convergent_lines(all_1_3_3, all_1_3_3) = all_12_1_14 % 27.79/7.21 | (102) convergent_lines(all_1_4_4, all_1_3_3) = all_12_2_15 % 27.79/7.21 | (103) ~ (all_12_3_16 = 0) | all_12_2_15 = 0 | (all_12_0_13 = 0 & all_12_1_14 = 0) % 27.79/7.21 | % 27.79/7.21 | Instantiating (80) with all_14_0_17, all_14_1_18, all_14_2_19, all_14_3_20 yields: % 27.79/7.21 | (104) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_14_2_19 & convergent_lines(all_1_3_3, all_1_2_2) = all_14_0_17 & convergent_lines(all_1_3_3, all_1_2_2) = all_14_1_18 & convergent_lines(all_1_3_3, all_1_3_3) = all_14_3_20 & ( ~ (all_14_2_19 = 0) | ~ (all_14_3_20 = 0) | (all_14_0_17 = 0 & all_1_0_0 = 0) | (all_14_1_18 = 0 & all_1_0_0 = 0)) % 27.79/7.21 | % 27.79/7.21 | Applying alpha-rule on (104) yields: % 27.79/7.21 | (105) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_14_2_19 % 27.79/7.21 | (106) convergent_lines(all_1_3_3, all_1_2_2) = all_14_0_17 % 27.79/7.21 | (107) convergent_lines(all_1_3_3, all_1_2_2) = all_14_1_18 % 27.79/7.21 | (108) ~ (all_14_2_19 = 0) | ~ (all_14_3_20 = 0) | (all_14_0_17 = 0 & all_1_0_0 = 0) | (all_14_1_18 = 0 & all_1_0_0 = 0) % 27.79/7.21 | (109) convergent_lines(all_1_3_3, all_1_3_3) = all_14_3_20 % 27.79/7.21 | % 27.79/7.21 +-Applying beta-rule and splitting (81), into two cases. % 27.79/7.21 |-Branch one: % 27.79/7.21 | (110) convergent_lines(all_1_3_3, all_1_2_2) = 0 % 27.79/7.21 | % 27.79/7.21 +-Applying beta-rule and splitting (85), into two cases. % 27.79/7.21 |-Branch one: % 27.79/7.21 | (111) all_1_1_1 = 0 % 27.79/7.21 | % 27.79/7.21 | Equations (111) can reduce 78 to: % 27.79/7.21 | (112) $false % 27.79/7.21 | % 27.79/7.21 |-The branch is then unsatisfiable % 27.79/7.21 |-Branch two: % 27.79/7.21 | (78) ~ (all_1_1_1 = 0) % 27.79/7.21 | (114) ? [v0] : ( ~ (v0 = 0) & distinct_lines(all_1_4_4, all_1_4_4) = v0) % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (32) with all_1_3_3, all_1_3_3, all_12_0_13, all_1_0_0 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13, yields: % 27.79/7.21 | (115) all_12_0_13 = all_1_0_0 | ~ (unorthogonal_lines(all_1_3_3, all_1_3_3) = all_1_0_0) % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (32) with all_1_3_3, all_1_3_3, all_12_0_13, all_14_2_19 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_14_2_19, unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13, yields: % 27.79/7.21 | (116) all_14_2_19 = all_12_0_13 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (44) with all_1_3_3, all_1_2_2, all_14_1_18, all_14_0_17 and discharging atoms convergent_lines(all_1_3_3, all_1_2_2) = all_14_0_17, convergent_lines(all_1_3_3, all_1_2_2) = all_14_1_18, yields: % 27.79/7.21 | (117) all_14_0_17 = all_14_1_18 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (44) with all_1_3_3, all_1_2_2, all_8_0_5, all_14_1_18 and discharging atoms convergent_lines(all_1_3_3, all_1_2_2) = all_14_1_18, convergent_lines(all_1_3_3, all_1_2_2) = all_8_0_5, yields: % 27.79/7.21 | (118) all_14_1_18 = all_8_0_5 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (44) with all_1_3_3, all_1_2_2, 0, all_14_0_17 and discharging atoms convergent_lines(all_1_3_3, all_1_2_2) = all_14_0_17, convergent_lines(all_1_3_3, all_1_2_2) = 0, yields: % 27.79/7.21 | (119) all_14_0_17 = 0 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (66) with all_1_3_3 yields: % 27.79/7.21 | (120) ~ (convergent_lines(all_1_3_3, all_1_3_3) = 0) % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (44) with all_1_3_3, all_1_3_3, all_12_1_14, all_14_3_20 and discharging atoms convergent_lines(all_1_3_3, all_1_3_3) = all_14_3_20, convergent_lines(all_1_3_3, all_1_3_3) = all_12_1_14, yields: % 27.79/7.21 | (121) all_14_3_20 = all_12_1_14 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (44) with all_1_4_4, all_1_3_3, all_10_0_9, all_12_2_15 and discharging atoms convergent_lines(all_1_4_4, all_1_3_3) = all_12_2_15, convergent_lines(all_1_4_4, all_1_3_3) = all_10_0_9, yields: % 27.79/7.21 | (122) all_12_2_15 = all_10_0_9 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (44) with all_1_4_4, all_1_3_3, all_10_0_9, all_12_3_16 and discharging atoms convergent_lines(all_1_4_4, all_1_3_3) = all_12_3_16, convergent_lines(all_1_4_4, all_1_3_3) = all_10_0_9, yields: % 27.79/7.21 | (123) all_12_3_16 = all_10_0_9 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (44) with all_1_4_4, all_1_3_3, all_10_1_10, all_12_3_16 and discharging atoms convergent_lines(all_1_4_4, all_1_3_3) = all_12_3_16, convergent_lines(all_1_4_4, all_1_3_3) = all_10_1_10, yields: % 27.79/7.21 | (124) all_12_3_16 = all_10_1_10 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (44) with all_1_4_4, all_1_3_3, all_8_3_8, all_12_2_15 and discharging atoms convergent_lines(all_1_4_4, all_1_3_3) = all_12_2_15, convergent_lines(all_1_4_4, all_1_3_3) = all_8_3_8, yields: % 27.79/7.21 | (125) all_12_2_15 = all_8_3_8 % 27.79/7.21 | % 27.79/7.21 | Instantiating formula (66) with all_1_4_4 yields: % 27.79/7.21 | (126) ~ (convergent_lines(all_1_4_4, all_1_4_4) = 0) % 27.79/7.21 | % 27.79/7.21 | Combining equations (117,119) yields a new equation: % 27.79/7.21 | (127) all_14_1_18 = 0 % 27.79/7.21 | % 27.79/7.21 | Simplifying 127 yields: % 27.79/7.21 | (128) all_14_1_18 = 0 % 27.79/7.21 | % 27.79/7.21 | Combining equations (128,118) yields a new equation: % 27.79/7.21 | (129) all_8_0_5 = 0 % 27.79/7.21 | % 27.79/7.21 | Combining equations (122,125) yields a new equation: % 27.79/7.21 | (130) all_10_0_9 = all_8_3_8 % 27.79/7.21 | % 27.79/7.21 | Simplifying 130 yields: % 27.79/7.21 | (131) all_10_0_9 = all_8_3_8 % 27.79/7.21 | % 27.79/7.21 | Combining equations (123,124) yields a new equation: % 27.79/7.21 | (132) all_10_0_9 = all_10_1_10 % 27.79/7.21 | % 27.79/7.21 | Simplifying 132 yields: % 27.79/7.21 | (133) all_10_0_9 = all_10_1_10 % 27.79/7.21 | % 27.79/7.21 | Combining equations (131,133) yields a new equation: % 27.79/7.21 | (134) all_10_1_10 = all_8_3_8 % 27.79/7.21 | % 27.79/7.21 | From (116) and (105) follows: % 27.79/7.21 | (99) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13 % 27.79/7.21 | % 27.79/7.21 | From (129) and (91) follows: % 27.79/7.21 | (110) convergent_lines(all_1_3_3, all_1_2_2) = 0 % 27.79/7.21 | % 27.79/7.21 | From (121) and (109) follows: % 27.79/7.21 | (101) convergent_lines(all_1_3_3, all_1_3_3) = all_12_1_14 % 27.79/7.21 | % 27.79/7.21 | From (134) and (94) follows: % 27.79/7.21 | (87) convergent_lines(all_1_4_4, all_1_3_3) = all_8_3_8 % 27.79/7.21 | % 27.79/7.21 | Using (101) and (120) yields: % 27.96/7.21 | (139) ~ (all_12_1_14 = 0) % 27.96/7.21 | % 27.96/7.21 | Instantiating formula (7) with 0, all_12_0_13, all_1_3_3, all_1_4_4, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13, unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, yields: % 27.96/7.21 | (140) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_4_4) = v1 & convergent_lines(all_1_3_3, all_1_3_3) = v2 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & convergent_lines(all_1_4_4, all_1_3_3) = v3 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | (v2 = 0 & all_12_0_13 = 0))) % 27.96/7.21 | % 27.96/7.21 | Instantiating formula (49) with all_12_0_13, all_1_3_3, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13, ~ (convergent_lines(all_1_3_3, all_1_3_3) = 0), yields: % 27.96/7.22 | (141) all_12_0_13 = 0 % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (7) with all_8_1_6, all_1_0_0, all_1_2_2, all_1_4_4, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_2_2) = all_1_0_0, unorthogonal_lines(all_1_4_4, all_1_2_2) = all_8_1_6, yields: % 27.96/7.22 | (142) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_4_4) = v1 & convergent_lines(all_1_3_3, all_1_2_2) = v2 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & convergent_lines(all_1_4_4, all_1_2_2) = v3 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & all_8_1_6 = 0) | (v2 = 0 & all_1_0_0 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (7) with all_1_0_0, all_8_1_6, all_1_2_2, all_1_3_3, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_2_2) = all_1_0_0, unorthogonal_lines(all_1_4_4, all_1_2_2) = all_8_1_6, yields: % 27.96/7.22 | (143) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_4_4, all_1_3_3) = v1 & convergent_lines(all_1_3_3, all_1_2_2) = v3 & convergent_lines(all_1_4_4, all_1_2_2) = v2 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & all_1_0_0 = 0) | (v2 = 0 & all_8_1_6 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (1) with all_8_1_6, all_1_2_2, all_1_3_3, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_2_2) = all_8_1_6, unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, yields: % 27.96/7.22 | (144) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_2_2) = v3 & convergent_lines(all_1_3_3, all_1_2_2) = v2 & convergent_lines(all_1_4_4, all_1_2_2) = v1 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & ( ~ (v0 = 0) | (v3 = 0 & v2 = 0) | (v1 = 0 & all_8_1_6 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (49) with all_8_1_6, all_1_2_2, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_2_2) = all_8_1_6, yields: % 27.96/7.22 | (145) all_8_1_6 = 0 | convergent_lines(all_1_4_4, all_1_2_2) = 0 % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (1) with all_10_2_11, all_1_4_4, all_1_3_3, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, unorthogonal_lines(all_1_4_4, all_1_4_4) = all_10_2_11, yields: % 27.96/7.22 | (146) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_4_4) = v3 & convergent_lines(all_1_3_3, all_1_4_4) = v2 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & convergent_lines(all_1_4_4, all_1_4_4) = v1 & ( ~ (v0 = 0) | (v3 = 0 & v2 = 0) | (v1 = 0 & all_10_2_11 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (46) with 0, all_1_2_2, all_1_3_3, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, convergent_lines(all_1_3_3, all_1_2_2) = 0, yields: % 27.96/7.22 | (147) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_2_2) = v3 & unorthogonal_lines(all_1_4_4, all_1_2_2) = v2 & convergent_lines(all_1_4_4, all_1_2_2) = v1 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & ( ~ (v0 = 0) | v3 = 0 | (v2 = 0 & v1 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (17) with all_8_1_6, 0, all_1_2_2, all_1_4_4, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_2_2) = all_8_1_6, convergent_lines(all_1_3_3, all_1_2_2) = 0, yields: % 27.96/7.22 | (148) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_2_2) = v2 & unorthogonal_lines(all_1_3_3, all_1_4_4) = v1 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & convergent_lines(all_1_4_4, all_1_2_2) = v3 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0 | (v3 = 0 & all_8_1_6 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (73) with 0, all_8_1_6, all_1_2_2, all_1_3_3, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_2_2) = all_8_1_6, convergent_lines(all_1_3_3, all_1_2_2) = 0, yields: % 27.96/7.22 | (149) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_2_2) = v3 & unorthogonal_lines(all_1_4_4, all_1_3_3) = v1 & convergent_lines(all_1_4_4, all_1_2_2) = v2 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | (v2 = 0 & all_8_1_6 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (35) with all_12_0_13, all_1_3_3, all_1_2_2, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13, convergent_lines(all_1_3_3, all_1_2_2) = 0, yields: % 27.96/7.22 | (150) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_2_2, all_1_3_3) = v3 & unorthogonal_lines(all_1_3_3, all_1_2_2) = v0 & convergent_lines(all_1_2_2, all_1_3_3) = v2 & convergent_lines(all_1_3_3, all_1_3_3) = v1 & ( ~ (v0 = 0) | (v3 = 0 & v2 = 0) | (v1 = 0 & all_12_0_13 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (58) with all_12_1_14, all_1_3_3, all_1_2_2, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_2_2) = 0, convergent_lines(all_1_3_3, all_1_3_3) = all_12_1_14, yields: % 27.96/7.22 | (151) all_12_1_14 = 0 | convergent_lines(all_1_2_2, all_1_3_3) = 0 % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (54) with all_12_1_14, all_1_3_3, all_1_2_2, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_2_2) = 0, convergent_lines(all_1_3_3, all_1_3_3) = all_12_1_14, yields: % 27.96/7.22 | (152) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_2_2, all_1_3_3) = v3 & unorthogonal_lines(all_1_3_3, all_1_2_2) = v0 & unorthogonal_lines(all_1_3_3, all_1_3_3) = v1 & convergent_lines(all_1_2_2, all_1_3_3) = v2 & ( ~ (v0 = 0) | (v3 = 0 & v2 = 0) | (v1 = 0 & all_12_1_14 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (17) with 0, all_12_1_14, all_1_3_3, all_1_4_4, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, convergent_lines(all_1_3_3, all_1_3_3) = all_12_1_14, yields: % 27.96/7.22 | (153) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_3_3) = v2 & unorthogonal_lines(all_1_3_3, all_1_4_4) = v1 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & convergent_lines(all_1_4_4, all_1_3_3) = v3 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | (v2 = 0 & all_12_1_14 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (59) with all_8_2_7, 0, all_1_2_2, all_1_4_4, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_2_2) = 0, convergent_lines(all_1_4_4, all_1_2_2) = all_8_2_7, yields: % 27.96/7.22 | (154) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_2_2) = v2 & unorthogonal_lines(all_1_3_3, all_1_4_4) = v1 & unorthogonal_lines(all_1_4_4, all_1_2_2) = v3 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0 | (v3 = 0 & all_8_2_7 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (73) with all_8_2_7, all_1_0_0, all_1_2_2, all_1_4_4, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_2_2) = all_1_0_0, convergent_lines(all_1_4_4, all_1_2_2) = all_8_2_7, yields: % 27.96/7.22 | (155) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_4_4) = v1 & unorthogonal_lines(all_1_4_4, all_1_2_2) = v3 & convergent_lines(all_1_3_3, all_1_2_2) = v2 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & all_8_2_7 = 0) | (v2 = 0 & all_1_0_0 = 0))) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (63) with all_8_3_8, all_1_3_3, all_1_4_4, all_1_3_3 and discharging atoms convergent_lines(all_1_4_4, all_1_3_3) = all_8_3_8, ~ (convergent_lines(all_1_3_3, all_1_3_3) = 0), yields: % 27.96/7.22 | (156) all_8_3_8 = 0 | ~ (convergent_lines(all_1_3_3, all_1_4_4) = 0) % 27.96/7.22 | % 27.96/7.22 | Instantiating formula (59) with all_8_3_8, all_12_1_14, all_1_3_3, all_1_4_4, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_3_3) = all_12_1_14, convergent_lines(all_1_4_4, all_1_3_3) = all_8_3_8, yields: % 27.96/7.23 | (157) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_3_3) = v2 & unorthogonal_lines(all_1_3_3, all_1_4_4) = v1 & unorthogonal_lines(all_1_4_4, all_1_3_3) = v3 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & all_8_3_8 = 0) | (v2 = 0 & all_12_1_14 = 0))) % 27.96/7.23 | % 27.96/7.23 | Instantiating formula (73) with all_8_3_8, all_12_0_13, all_1_3_3, all_1_4_4, all_1_3_3 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_12_0_13, convergent_lines(all_1_4_4, all_1_3_3) = all_8_3_8, yields: % 27.96/7.23 | (158) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_4_4) = v1 & unorthogonal_lines(all_1_4_4, all_1_3_3) = v3 & convergent_lines(all_1_3_3, all_1_3_3) = v2 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & all_8_3_8 = 0) | (v2 = 0 & all_12_0_13 = 0))) % 27.96/7.23 | % 27.96/7.23 | Instantiating formula (58) with all_10_3_12, all_1_4_4, all_1_2_2, all_1_4_4 and discharging atoms convergent_lines(all_1_4_4, all_1_4_4) = all_10_3_12, yields: % 27.96/7.23 | (159) all_10_3_12 = 0 | ~ (convergent_lines(all_1_4_4, all_1_2_2) = 0) | convergent_lines(all_1_2_2, all_1_4_4) = 0 % 27.96/7.23 | % 27.96/7.23 | Instantiating formula (6) with all_10_3_12, all_1_4_4, all_1_3_3, all_1_4_4 and discharging atoms unorthogonal_lines(all_1_4_4, all_1_3_3) = 0, convergent_lines(all_1_4_4, all_1_4_4) = all_10_3_12, yields: % 27.96/7.23 | (160) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (unorthogonal_lines(all_1_3_3, all_1_4_4) = v3 & unorthogonal_lines(all_1_4_4, all_1_4_4) = v1 & convergent_lines(all_1_3_3, all_1_4_4) = v2 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & ( ~ (v0 = 0) | (v3 = 0 & v2 = 0) | (v1 = 0 & all_10_3_12 = 0))) % 27.96/7.23 | % 27.96/7.23 | Instantiating (158) with all_40_0_22, all_40_1_23, all_40_2_24, all_40_3_25 yields: % 27.96/7.23 | (161) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_40_2_24 & unorthogonal_lines(all_1_4_4, all_1_3_3) = all_40_0_22 & convergent_lines(all_1_3_3, all_1_3_3) = all_40_1_23 & convergent_lines(all_1_3_3, all_1_4_4) = all_40_3_25 & ( ~ (all_40_2_24 = 0) | ~ (all_40_3_25 = 0) | (all_40_0_22 = 0 & all_8_3_8 = 0) | (all_40_1_23 = 0 & all_12_0_13 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (161) yields: % 27.96/7.23 | (162) convergent_lines(all_1_3_3, all_1_3_3) = all_40_1_23 % 27.96/7.23 | (163) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_40_2_24 % 27.96/7.23 | (164) unorthogonal_lines(all_1_4_4, all_1_3_3) = all_40_0_22 % 27.96/7.23 | (165) ~ (all_40_2_24 = 0) | ~ (all_40_3_25 = 0) | (all_40_0_22 = 0 & all_8_3_8 = 0) | (all_40_1_23 = 0 & all_12_0_13 = 0) % 27.96/7.23 | (166) convergent_lines(all_1_3_3, all_1_4_4) = all_40_3_25 % 27.96/7.23 | % 27.96/7.23 | Instantiating (160) with all_46_0_34, all_46_1_35, all_46_2_36, all_46_3_37 yields: % 27.96/7.23 | (167) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_46_0_34 & unorthogonal_lines(all_1_4_4, all_1_4_4) = all_46_2_36 & convergent_lines(all_1_3_3, all_1_4_4) = all_46_1_35 & convergent_lines(all_1_4_4, all_1_3_3) = all_46_3_37 & ( ~ (all_46_3_37 = 0) | (all_46_0_34 = 0 & all_46_1_35 = 0) | (all_46_2_36 = 0 & all_10_3_12 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (167) yields: % 27.96/7.23 | (168) unorthogonal_lines(all_1_4_4, all_1_4_4) = all_46_2_36 % 27.96/7.23 | (169) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_46_0_34 % 27.96/7.23 | (170) convergent_lines(all_1_3_3, all_1_4_4) = all_46_1_35 % 27.96/7.23 | (171) convergent_lines(all_1_4_4, all_1_3_3) = all_46_3_37 % 27.96/7.23 | (172) ~ (all_46_3_37 = 0) | (all_46_0_34 = 0 & all_46_1_35 = 0) | (all_46_2_36 = 0 & all_10_3_12 = 0) % 27.96/7.23 | % 27.96/7.23 | Instantiating (154) with all_50_0_42, all_50_1_43, all_50_2_44, all_50_3_45 yields: % 27.96/7.23 | (173) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_50_1_43 & unorthogonal_lines(all_1_3_3, all_1_4_4) = all_50_2_44 & unorthogonal_lines(all_1_4_4, all_1_2_2) = all_50_0_42 & convergent_lines(all_1_3_3, all_1_4_4) = all_50_3_45 & ( ~ (all_50_2_44 = 0) | ~ (all_50_3_45 = 0) | all_50_1_43 = 0 | (all_50_0_42 = 0 & all_8_2_7 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (173) yields: % 27.96/7.23 | (174) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_50_1_43 % 27.96/7.23 | (175) unorthogonal_lines(all_1_4_4, all_1_2_2) = all_50_0_42 % 27.96/7.23 | (176) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_50_2_44 % 27.96/7.23 | (177) convergent_lines(all_1_3_3, all_1_4_4) = all_50_3_45 % 27.96/7.23 | (178) ~ (all_50_2_44 = 0) | ~ (all_50_3_45 = 0) | all_50_1_43 = 0 | (all_50_0_42 = 0 & all_8_2_7 = 0) % 27.96/7.23 | % 27.96/7.23 | Instantiating (153) with all_52_0_46, all_52_1_47, all_52_2_48, all_52_3_49 yields: % 27.96/7.23 | (179) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_52_1_47 & unorthogonal_lines(all_1_3_3, all_1_4_4) = all_52_2_48 & convergent_lines(all_1_3_3, all_1_4_4) = all_52_3_49 & convergent_lines(all_1_4_4, all_1_3_3) = all_52_0_46 & ( ~ (all_52_2_48 = 0) | ~ (all_52_3_49 = 0) | all_52_0_46 = 0 | (all_52_1_47 = 0 & all_12_1_14 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (179) yields: % 27.96/7.23 | (180) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_52_1_47 % 27.96/7.23 | (181) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_52_2_48 % 27.96/7.23 | (182) ~ (all_52_2_48 = 0) | ~ (all_52_3_49 = 0) | all_52_0_46 = 0 | (all_52_1_47 = 0 & all_12_1_14 = 0) % 27.96/7.23 | (183) convergent_lines(all_1_3_3, all_1_4_4) = all_52_3_49 % 27.96/7.23 | (184) convergent_lines(all_1_4_4, all_1_3_3) = all_52_0_46 % 27.96/7.23 | % 27.96/7.23 | Instantiating (148) with all_54_0_50, all_54_1_51, all_54_2_52, all_54_3_53 yields: % 27.96/7.23 | (185) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_54_1_51 & unorthogonal_lines(all_1_3_3, all_1_4_4) = all_54_2_52 & convergent_lines(all_1_3_3, all_1_4_4) = all_54_3_53 & convergent_lines(all_1_4_4, all_1_2_2) = all_54_0_50 & ( ~ (all_54_2_52 = 0) | ~ (all_54_3_53 = 0) | all_54_1_51 = 0 | (all_54_0_50 = 0 & all_8_1_6 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (185) yields: % 27.96/7.23 | (186) ~ (all_54_2_52 = 0) | ~ (all_54_3_53 = 0) | all_54_1_51 = 0 | (all_54_0_50 = 0 & all_8_1_6 = 0) % 27.96/7.23 | (187) convergent_lines(all_1_4_4, all_1_2_2) = all_54_0_50 % 27.96/7.23 | (188) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_54_1_51 % 27.96/7.23 | (189) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_54_2_52 % 27.96/7.23 | (190) convergent_lines(all_1_3_3, all_1_4_4) = all_54_3_53 % 27.96/7.23 | % 27.96/7.23 | Instantiating (147) with all_56_0_54, all_56_1_55, all_56_2_56, all_56_3_57 yields: % 27.96/7.23 | (191) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_56_0_54 & unorthogonal_lines(all_1_4_4, all_1_2_2) = all_56_1_55 & convergent_lines(all_1_4_4, all_1_2_2) = all_56_2_56 & convergent_lines(all_1_4_4, all_1_3_3) = all_56_3_57 & ( ~ (all_56_3_57 = 0) | all_56_0_54 = 0 | (all_56_1_55 = 0 & all_56_2_56 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (191) yields: % 27.96/7.23 | (192) unorthogonal_lines(all_1_4_4, all_1_2_2) = all_56_1_55 % 27.96/7.23 | (193) ~ (all_56_3_57 = 0) | all_56_0_54 = 0 | (all_56_1_55 = 0 & all_56_2_56 = 0) % 27.96/7.23 | (194) convergent_lines(all_1_4_4, all_1_3_3) = all_56_3_57 % 27.96/7.23 | (195) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_56_0_54 % 27.96/7.23 | (196) convergent_lines(all_1_4_4, all_1_2_2) = all_56_2_56 % 27.96/7.23 | % 27.96/7.23 | Instantiating (143) with all_58_0_58, all_58_1_59, all_58_2_60, all_58_3_61 yields: % 27.96/7.23 | (197) unorthogonal_lines(all_1_4_4, all_1_3_3) = all_58_2_60 & convergent_lines(all_1_3_3, all_1_2_2) = all_58_0_58 & convergent_lines(all_1_4_4, all_1_2_2) = all_58_1_59 & convergent_lines(all_1_4_4, all_1_3_3) = all_58_3_61 & ( ~ (all_58_2_60 = 0) | ~ (all_58_3_61 = 0) | (all_58_0_58 = 0 & all_1_0_0 = 0) | (all_58_1_59 = 0 & all_8_1_6 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (197) yields: % 27.96/7.23 | (198) ~ (all_58_2_60 = 0) | ~ (all_58_3_61 = 0) | (all_58_0_58 = 0 & all_1_0_0 = 0) | (all_58_1_59 = 0 & all_8_1_6 = 0) % 27.96/7.23 | (199) convergent_lines(all_1_3_3, all_1_2_2) = all_58_0_58 % 27.96/7.23 | (200) unorthogonal_lines(all_1_4_4, all_1_3_3) = all_58_2_60 % 27.96/7.23 | (201) convergent_lines(all_1_4_4, all_1_3_3) = all_58_3_61 % 27.96/7.23 | (202) convergent_lines(all_1_4_4, all_1_2_2) = all_58_1_59 % 27.96/7.23 | % 27.96/7.23 | Instantiating (152) with all_60_0_62, all_60_1_63, all_60_2_64, all_60_3_65 yields: % 27.96/7.23 | (203) unorthogonal_lines(all_1_2_2, all_1_3_3) = all_60_0_62 & unorthogonal_lines(all_1_3_3, all_1_2_2) = all_60_3_65 & unorthogonal_lines(all_1_3_3, all_1_3_3) = all_60_2_64 & convergent_lines(all_1_2_2, all_1_3_3) = all_60_1_63 & ( ~ (all_60_3_65 = 0) | (all_60_0_62 = 0 & all_60_1_63 = 0) | (all_60_2_64 = 0 & all_12_1_14 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (203) yields: % 27.96/7.23 | (204) ~ (all_60_3_65 = 0) | (all_60_0_62 = 0 & all_60_1_63 = 0) | (all_60_2_64 = 0 & all_12_1_14 = 0) % 27.96/7.23 | (205) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_60_2_64 % 27.96/7.23 | (206) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_60_3_65 % 27.96/7.23 | (207) unorthogonal_lines(all_1_2_2, all_1_3_3) = all_60_0_62 % 27.96/7.23 | (208) convergent_lines(all_1_2_2, all_1_3_3) = all_60_1_63 % 27.96/7.23 | % 27.96/7.23 | Instantiating (146) with all_66_0_72, all_66_1_73, all_66_2_74, all_66_3_75 yields: % 27.96/7.23 | (209) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_66_0_72 & convergent_lines(all_1_3_3, all_1_4_4) = all_66_1_73 & convergent_lines(all_1_4_4, all_1_3_3) = all_66_3_75 & convergent_lines(all_1_4_4, all_1_4_4) = all_66_2_74 & ( ~ (all_66_3_75 = 0) | (all_66_0_72 = 0 & all_66_1_73 = 0) | (all_66_2_74 = 0 & all_10_2_11 = 0)) % 27.96/7.23 | % 27.96/7.23 | Applying alpha-rule on (209) yields: % 27.96/7.23 | (210) convergent_lines(all_1_4_4, all_1_4_4) = all_66_2_74 % 27.96/7.24 | (211) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_66_0_72 % 27.96/7.24 | (212) convergent_lines(all_1_4_4, all_1_3_3) = all_66_3_75 % 27.96/7.24 | (213) ~ (all_66_3_75 = 0) | (all_66_0_72 = 0 & all_66_1_73 = 0) | (all_66_2_74 = 0 & all_10_2_11 = 0) % 27.96/7.24 | (214) convergent_lines(all_1_3_3, all_1_4_4) = all_66_1_73 % 27.96/7.24 | % 27.96/7.24 | Instantiating (150) with all_70_0_78, all_70_1_79, all_70_2_80, all_70_3_81 yields: % 27.96/7.24 | (215) unorthogonal_lines(all_1_2_2, all_1_3_3) = all_70_0_78 & unorthogonal_lines(all_1_3_3, all_1_2_2) = all_70_3_81 & convergent_lines(all_1_2_2, all_1_3_3) = all_70_1_79 & convergent_lines(all_1_3_3, all_1_3_3) = all_70_2_80 & ( ~ (all_70_3_81 = 0) | (all_70_0_78 = 0 & all_70_1_79 = 0) | (all_70_2_80 = 0 & all_12_0_13 = 0)) % 27.96/7.24 | % 27.96/7.24 | Applying alpha-rule on (215) yields: % 27.96/7.24 | (216) ~ (all_70_3_81 = 0) | (all_70_0_78 = 0 & all_70_1_79 = 0) | (all_70_2_80 = 0 & all_12_0_13 = 0) % 27.96/7.24 | (217) unorthogonal_lines(all_1_2_2, all_1_3_3) = all_70_0_78 % 27.96/7.24 | (218) convergent_lines(all_1_2_2, all_1_3_3) = all_70_1_79 % 27.96/7.24 | (219) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_70_3_81 % 27.96/7.24 | (220) convergent_lines(all_1_3_3, all_1_3_3) = all_70_2_80 % 27.96/7.24 | % 27.96/7.24 | Instantiating (142) with all_72_0_82, all_72_1_83, all_72_2_84, all_72_3_85 yields: % 27.96/7.24 | (221) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_72_2_84 & convergent_lines(all_1_3_3, all_1_2_2) = all_72_1_83 & convergent_lines(all_1_3_3, all_1_4_4) = all_72_3_85 & convergent_lines(all_1_4_4, all_1_2_2) = all_72_0_82 & ( ~ (all_72_2_84 = 0) | ~ (all_72_3_85 = 0) | (all_72_0_82 = 0 & all_8_1_6 = 0) | (all_72_1_83 = 0 & all_1_0_0 = 0)) % 27.96/7.24 | % 27.96/7.24 | Applying alpha-rule on (221) yields: % 27.96/7.24 | (222) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_72_2_84 % 27.96/7.24 | (223) ~ (all_72_2_84 = 0) | ~ (all_72_3_85 = 0) | (all_72_0_82 = 0 & all_8_1_6 = 0) | (all_72_1_83 = 0 & all_1_0_0 = 0) % 27.96/7.24 | (224) convergent_lines(all_1_3_3, all_1_4_4) = all_72_3_85 % 27.96/7.24 | (225) convergent_lines(all_1_3_3, all_1_2_2) = all_72_1_83 % 27.96/7.24 | (226) convergent_lines(all_1_4_4, all_1_2_2) = all_72_0_82 % 27.96/7.24 | % 27.96/7.24 | Instantiating (155) with all_74_0_86, all_74_1_87, all_74_2_88, all_74_3_89 yields: % 27.96/7.24 | (227) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_74_2_88 & unorthogonal_lines(all_1_4_4, all_1_2_2) = all_74_0_86 & convergent_lines(all_1_3_3, all_1_2_2) = all_74_1_87 & convergent_lines(all_1_3_3, all_1_4_4) = all_74_3_89 & ( ~ (all_74_2_88 = 0) | ~ (all_74_3_89 = 0) | (all_74_0_86 = 0 & all_8_2_7 = 0) | (all_74_1_87 = 0 & all_1_0_0 = 0)) % 27.96/7.24 | % 27.96/7.24 | Applying alpha-rule on (227) yields: % 27.96/7.24 | (228) unorthogonal_lines(all_1_4_4, all_1_2_2) = all_74_0_86 % 27.96/7.24 | (229) convergent_lines(all_1_3_3, all_1_2_2) = all_74_1_87 % 27.96/7.24 | (230) ~ (all_74_2_88 = 0) | ~ (all_74_3_89 = 0) | (all_74_0_86 = 0 & all_8_2_7 = 0) | (all_74_1_87 = 0 & all_1_0_0 = 0) % 27.96/7.24 | (231) convergent_lines(all_1_3_3, all_1_4_4) = all_74_3_89 % 27.96/7.24 | (232) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_74_2_88 % 27.96/7.24 | % 27.96/7.24 | Instantiating (149) with all_78_0_94, all_78_1_95, all_78_2_96, all_78_3_97 yields: % 27.96/7.24 | (233) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_78_0_94 & unorthogonal_lines(all_1_4_4, all_1_3_3) = all_78_2_96 & convergent_lines(all_1_4_4, all_1_2_2) = all_78_1_95 & convergent_lines(all_1_4_4, all_1_3_3) = all_78_3_97 & ( ~ (all_78_2_96 = 0) | ~ (all_78_3_97 = 0) | all_78_0_94 = 0 | (all_78_1_95 = 0 & all_8_1_6 = 0)) % 27.96/7.24 | % 27.96/7.24 | Applying alpha-rule on (233) yields: % 27.96/7.24 | (234) unorthogonal_lines(all_1_4_4, all_1_3_3) = all_78_2_96 % 27.96/7.24 | (235) convergent_lines(all_1_4_4, all_1_2_2) = all_78_1_95 % 27.96/7.24 | (236) ~ (all_78_2_96 = 0) | ~ (all_78_3_97 = 0) | all_78_0_94 = 0 | (all_78_1_95 = 0 & all_8_1_6 = 0) % 27.96/7.24 | (237) convergent_lines(all_1_4_4, all_1_3_3) = all_78_3_97 % 27.96/7.24 | (238) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_78_0_94 % 27.96/7.24 | % 27.96/7.24 | Instantiating (157) with all_80_0_98, all_80_1_99, all_80_2_100, all_80_3_101 yields: % 27.96/7.24 | (239) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_80_1_99 & unorthogonal_lines(all_1_3_3, all_1_4_4) = all_80_2_100 & unorthogonal_lines(all_1_4_4, all_1_3_3) = all_80_0_98 & convergent_lines(all_1_3_3, all_1_4_4) = all_80_3_101 & ( ~ (all_80_2_100 = 0) | ~ (all_80_3_101 = 0) | (all_80_0_98 = 0 & all_8_3_8 = 0) | (all_80_1_99 = 0 & all_12_1_14 = 0)) % 27.96/7.24 | % 27.96/7.24 | Applying alpha-rule on (239) yields: % 27.96/7.24 | (240) convergent_lines(all_1_3_3, all_1_4_4) = all_80_3_101 % 27.96/7.24 | (241) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_80_1_99 % 27.96/7.24 | (242) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_80_2_100 % 27.96/7.24 | (243) ~ (all_80_2_100 = 0) | ~ (all_80_3_101 = 0) | (all_80_0_98 = 0 & all_8_3_8 = 0) | (all_80_1_99 = 0 & all_12_1_14 = 0) % 27.96/7.24 | (244) unorthogonal_lines(all_1_4_4, all_1_3_3) = all_80_0_98 % 27.96/7.24 | % 27.96/7.24 | Instantiating (144) with all_82_0_102, all_82_1_103, all_82_2_104, all_82_3_105 yields: % 27.96/7.24 | (245) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_82_0_102 & convergent_lines(all_1_3_3, all_1_2_2) = all_82_1_103 & convergent_lines(all_1_4_4, all_1_2_2) = all_82_2_104 & convergent_lines(all_1_4_4, all_1_3_3) = all_82_3_105 & ( ~ (all_82_3_105 = 0) | (all_82_0_102 = 0 & all_82_1_103 = 0) | (all_82_2_104 = 0 & all_8_1_6 = 0)) % 27.96/7.24 | % 27.96/7.24 | Applying alpha-rule on (245) yields: % 27.96/7.24 | (246) convergent_lines(all_1_3_3, all_1_2_2) = all_82_1_103 % 27.96/7.24 | (247) convergent_lines(all_1_4_4, all_1_3_3) = all_82_3_105 % 27.96/7.24 | (248) unorthogonal_lines(all_1_3_3, all_1_2_2) = all_82_0_102 % 27.96/7.24 | (249) convergent_lines(all_1_4_4, all_1_2_2) = all_82_2_104 % 27.96/7.24 | (250) ~ (all_82_3_105 = 0) | (all_82_0_102 = 0 & all_82_1_103 = 0) | (all_82_2_104 = 0 & all_8_1_6 = 0) % 27.96/7.24 | % 27.96/7.24 | Instantiating (140) with all_84_0_106, all_84_1_107, all_84_2_108, all_84_3_109 yields: % 27.96/7.24 | (251) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_84_2_108 & convergent_lines(all_1_3_3, all_1_3_3) = all_84_1_107 & convergent_lines(all_1_3_3, all_1_4_4) = all_84_3_109 & convergent_lines(all_1_4_4, all_1_3_3) = all_84_0_106 & ( ~ (all_84_2_108 = 0) | ~ (all_84_3_109 = 0) | all_84_0_106 = 0 | (all_84_1_107 = 0 & all_12_0_13 = 0)) % 27.96/7.24 | % 27.96/7.24 | Applying alpha-rule on (251) yields: % 27.96/7.24 | (252) convergent_lines(all_1_3_3, all_1_4_4) = all_84_3_109 % 27.96/7.24 | (253) convergent_lines(all_1_3_3, all_1_3_3) = all_84_1_107 % 27.96/7.24 | (254) ~ (all_84_2_108 = 0) | ~ (all_84_3_109 = 0) | all_84_0_106 = 0 | (all_84_1_107 = 0 & all_12_0_13 = 0) % 27.96/7.24 | (255) unorthogonal_lines(all_1_3_3, all_1_4_4) = all_84_2_108 % 27.96/7.24 | (256) convergent_lines(all_1_4_4, all_1_3_3) = all_84_0_106 % 27.96/7.24 | % 27.96/7.24 | From (141) and (99) follows: % 27.96/7.24 | (257) unorthogonal_lines(all_1_3_3, all_1_3_3) = 0 % 27.96/7.24 | % 27.96/7.24 +-Applying beta-rule and splitting (115), into two cases. % 27.96/7.24 |-Branch one: % 27.96/7.24 | (258) ~ (unorthogonal_lines(all_1_3_3, all_1_3_3) = all_1_0_0) % 27.96/7.24 | % 27.96/7.24 +-Applying beta-rule and splitting (151), into two cases. % 27.96/7.24 |-Branch one: % 27.96/7.24 | (259) convergent_lines(all_1_2_2, all_1_3_3) = 0 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (32) with all_1_3_3, all_1_3_3, all_60_2_64, all_80_1_99 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_80_1_99, unorthogonal_lines(all_1_3_3, all_1_3_3) = all_60_2_64, yields: % 27.96/7.24 | (260) all_80_1_99 = all_60_2_64 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (32) with all_1_3_3, all_1_3_3, all_52_1_47, all_80_1_99 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_80_1_99, unorthogonal_lines(all_1_3_3, all_1_3_3) = all_52_1_47, yields: % 27.96/7.24 | (261) all_80_1_99 = all_52_1_47 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (32) with all_1_3_3, all_1_3_3, 0, all_80_1_99 and discharging atoms unorthogonal_lines(all_1_3_3, all_1_3_3) = all_80_1_99, unorthogonal_lines(all_1_3_3, all_1_3_3) = 0, yields: % 27.96/7.24 | (262) all_80_1_99 = 0 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (66) with all_1_2_2 yields: % 27.96/7.24 | (263) ~ (convergent_lines(all_1_2_2, all_1_2_2) = 0) % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_2_2, all_1_3_3, all_60_1_63, all_70_1_79 and discharging atoms convergent_lines(all_1_2_2, all_1_3_3) = all_70_1_79, convergent_lines(all_1_2_2, all_1_3_3) = all_60_1_63, yields: % 27.96/7.24 | (264) all_70_1_79 = all_60_1_63 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_2_2, all_1_3_3, 0, all_70_1_79 and discharging atoms convergent_lines(all_1_2_2, all_1_3_3) = all_70_1_79, convergent_lines(all_1_2_2, all_1_3_3) = 0, yields: % 27.96/7.24 | (265) all_70_1_79 = 0 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_72_3_85, all_84_3_109 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_84_3_109, convergent_lines(all_1_3_3, all_1_4_4) = all_72_3_85, yields: % 27.96/7.24 | (266) all_84_3_109 = all_72_3_85 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_66_1_73, all_74_3_89 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_74_3_89, convergent_lines(all_1_3_3, all_1_4_4) = all_66_1_73, yields: % 27.96/7.24 | (267) all_74_3_89 = all_66_1_73 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_54_3_53, all_84_3_109 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_84_3_109, convergent_lines(all_1_3_3, all_1_4_4) = all_54_3_53, yields: % 27.96/7.24 | (268) all_84_3_109 = all_54_3_53 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_54_3_53, all_80_3_101 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_80_3_101, convergent_lines(all_1_3_3, all_1_4_4) = all_54_3_53, yields: % 27.96/7.24 | (269) all_80_3_101 = all_54_3_53 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_54_3_53, all_74_3_89 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_74_3_89, convergent_lines(all_1_3_3, all_1_4_4) = all_54_3_53, yields: % 27.96/7.24 | (270) all_74_3_89 = all_54_3_53 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_52_3_49, all_74_3_89 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_74_3_89, convergent_lines(all_1_3_3, all_1_4_4) = all_52_3_49, yields: % 27.96/7.24 | (271) all_74_3_89 = all_52_3_49 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_50_3_45, all_80_3_101 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_80_3_101, convergent_lines(all_1_3_3, all_1_4_4) = all_50_3_45, yields: % 27.96/7.24 | (272) all_80_3_101 = all_50_3_45 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_46_1_35, all_84_3_109 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_84_3_109, convergent_lines(all_1_3_3, all_1_4_4) = all_46_1_35, yields: % 27.96/7.24 | (273) all_84_3_109 = all_46_1_35 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_3_3, all_1_4_4, all_40_3_25, all_80_3_101 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = all_80_3_101, convergent_lines(all_1_3_3, all_1_4_4) = all_40_3_25, yields: % 27.96/7.24 | (274) all_80_3_101 = all_40_3_25 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_4_4, all_1_2_2, all_72_0_82, all_8_2_7 and discharging atoms convergent_lines(all_1_4_4, all_1_2_2) = all_72_0_82, convergent_lines(all_1_4_4, all_1_2_2) = all_8_2_7, yields: % 27.96/7.24 | (275) all_72_0_82 = all_8_2_7 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_4_4, all_1_2_2, all_72_0_82, all_82_2_104 and discharging atoms convergent_lines(all_1_4_4, all_1_2_2) = all_82_2_104, convergent_lines(all_1_4_4, all_1_2_2) = all_72_0_82, yields: % 27.96/7.24 | (276) all_82_2_104 = all_72_0_82 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_4_4, all_1_2_2, all_72_0_82, all_78_1_95 and discharging atoms convergent_lines(all_1_4_4, all_1_2_2) = all_78_1_95, convergent_lines(all_1_4_4, all_1_2_2) = all_72_0_82, yields: % 27.96/7.24 | (277) all_78_1_95 = all_72_0_82 % 27.96/7.24 | % 27.96/7.24 | Instantiating formula (44) with all_1_4_4, all_1_2_2, all_58_1_59, all_78_1_95 and discharging atoms convergent_lines(all_1_4_4, all_1_2_2) = all_78_1_95, convergent_lines(all_1_4_4, all_1_2_2) = all_58_1_59, yields: % 27.96/7.25 | (278) all_78_1_95 = all_58_1_59 % 27.96/7.25 | % 27.96/7.25 | Instantiating formula (44) with all_1_4_4, all_1_2_2, all_56_2_56, all_82_2_104 and discharging atoms convergent_lines(all_1_4_4, all_1_2_2) = all_82_2_104, convergent_lines(all_1_4_4, all_1_2_2) = all_56_2_56, yields: % 27.96/7.25 | (279) all_82_2_104 = all_56_2_56 % 27.96/7.25 | % 27.96/7.25 | Instantiating formula (44) with all_1_4_4, all_1_2_2, all_54_0_50, all_72_0_82 and discharging atoms convergent_lines(all_1_4_4, all_1_2_2) = all_72_0_82, convergent_lines(all_1_4_4, all_1_2_2) = all_54_0_50, yields: % 27.96/7.25 | (280) all_72_0_82 = all_54_0_50 % 27.96/7.25 | % 27.96/7.25 | Instantiating formula (44) with all_1_4_4, all_1_4_4, all_66_2_74, all_10_3_12 and discharging atoms convergent_lines(all_1_4_4, all_1_4_4) = all_66_2_74, convergent_lines(all_1_4_4, all_1_4_4) = all_10_3_12, yields: % 27.96/7.25 | (281) all_66_2_74 = all_10_3_12 % 27.96/7.25 | % 27.96/7.25 | Using (210) and (126) yields: % 27.96/7.25 | (282) ~ (all_66_2_74 = 0) % 27.96/7.25 | % 27.96/7.25 | Using (180) and (258) yields: % 27.96/7.25 | (283) ~ (all_52_1_47 = all_1_0_0) % 27.96/7.25 | % 27.96/7.25 | Combining equations (273,266) yields a new equation: % 27.96/7.25 | (284) all_72_3_85 = all_46_1_35 % 27.96/7.25 | % 27.96/7.25 | Combining equations (268,266) yields a new equation: % 27.96/7.25 | (285) all_72_3_85 = all_54_3_53 % 27.96/7.25 | % 27.96/7.25 | Combining equations (276,279) yields a new equation: % 27.96/7.25 | (286) all_72_0_82 = all_56_2_56 % 27.96/7.25 | % 27.96/7.25 | Simplifying 286 yields: % 27.96/7.25 | (287) all_72_0_82 = all_56_2_56 % 27.96/7.25 | % 27.96/7.25 | Combining equations (262,260) yields a new equation: % 27.96/7.25 | (288) all_60_2_64 = 0 % 27.96/7.25 | % 27.96/7.25 | Combining equations (261,260) yields a new equation: % 27.96/7.25 | (289) all_60_2_64 = all_52_1_47 % 27.96/7.25 | % 27.96/7.25 | Combining equations (274,272) yields a new equation: % 27.96/7.25 | (290) all_50_3_45 = all_40_3_25 % 27.96/7.25 | % 27.96/7.25 | Combining equations (269,272) yields a new equation: % 27.96/7.25 | (291) all_54_3_53 = all_50_3_45 % 27.96/7.25 | % 27.96/7.25 | Simplifying 291 yields: % 27.96/7.25 | (292) all_54_3_53 = all_50_3_45 % 27.96/7.25 | % 28.13/7.25 | Combining equations (277,278) yields a new equation: % 28.13/7.25 | (293) all_72_0_82 = all_58_1_59 % 28.13/7.25 | % 28.13/7.25 | Simplifying 293 yields: % 28.13/7.25 | (294) all_72_0_82 = all_58_1_59 % 28.13/7.25 | % 28.13/7.25 | Combining equations (270,267) yields a new equation: % 28.13/7.25 | (295) all_66_1_73 = all_54_3_53 % 28.13/7.25 | % 28.13/7.25 | Combining equations (271,267) yields a new equation: % 28.13/7.25 | (296) all_66_1_73 = all_52_3_49 % 28.13/7.25 | % 28.13/7.25 | Combining equations (280,294) yields a new equation: % 28.13/7.25 | (297) all_58_1_59 = all_54_0_50 % 28.13/7.25 | % 28.13/7.25 | Combining equations (275,294) yields a new equation: % 28.13/7.25 | (298) all_58_1_59 = all_8_2_7 % 28.13/7.25 | % 28.13/7.25 | Combining equations (287,294) yields a new equation: % 28.13/7.25 | (299) all_58_1_59 = all_56_2_56 % 28.13/7.25 | % 28.13/7.25 | Combining equations (285,284) yields a new equation: % 28.13/7.25 | (300) all_54_3_53 = all_46_1_35 % 28.13/7.25 | % 28.13/7.25 | Simplifying 300 yields: % 28.13/7.25 | (301) all_54_3_53 = all_46_1_35 % 28.13/7.25 | % 28.13/7.25 | Combining equations (265,264) yields a new equation: % 28.13/7.25 | (302) all_60_1_63 = 0 % 28.13/7.25 | % 28.13/7.25 | Combining equations (295,296) yields a new equation: % 28.13/7.25 | (303) all_54_3_53 = all_52_3_49 % 28.13/7.25 | % 28.13/7.25 | Simplifying 303 yields: % 28.13/7.25 | (304) all_54_3_53 = all_52_3_49 % 28.13/7.25 | % 28.13/7.25 | Combining equations (288,289) yields a new equation: % 28.13/7.25 | (305) all_52_1_47 = 0 % 28.13/7.25 | % 28.13/7.25 | Combining equations (298,299) yields a new equation: % 28.13/7.25 | (306) all_56_2_56 = all_8_2_7 % 28.13/7.25 | % 28.13/7.25 | Combining equations (297,299) yields a new equation: % 28.13/7.25 | (307) all_56_2_56 = all_54_0_50 % 28.13/7.25 | % 28.13/7.25 | Combining equations (306,307) yields a new equation: % 28.13/7.25 | (308) all_54_0_50 = all_8_2_7 % 28.13/7.25 | % 28.13/7.25 | Combining equations (292,304) yields a new equation: % 28.13/7.25 | (309) all_52_3_49 = all_50_3_45 % 28.13/7.25 | % 28.13/7.25 | Combining equations (301,304) yields a new equation: % 28.13/7.25 | (310) all_52_3_49 = all_46_1_35 % 28.13/7.25 | % 28.13/7.25 | Combining equations (309,310) yields a new equation: % 28.13/7.25 | (311) all_50_3_45 = all_46_1_35 % 28.13/7.25 | % 28.13/7.25 | Simplifying 311 yields: % 28.13/7.25 | (312) all_50_3_45 = all_46_1_35 % 28.13/7.25 | % 28.13/7.25 | Combining equations (290,312) yields a new equation: % 28.13/7.25 | (313) all_46_1_35 = all_40_3_25 % 28.13/7.25 | % 28.13/7.25 | Equations (281) can reduce 282 to: % 28.13/7.25 | (314) ~ (all_10_3_12 = 0) % 28.13/7.25 | % 28.13/7.25 | Equations (305) can reduce 283 to: % 28.13/7.25 | (315) ~ (all_1_0_0 = 0) % 28.13/7.25 | % 28.13/7.25 | Simplifying 315 yields: % 28.13/7.25 | (77) ~ (all_1_0_0 = 0) % 28.13/7.25 | % 28.13/7.25 | From (302) and (208) follows: % 28.13/7.25 | (259) convergent_lines(all_1_2_2, all_1_3_3) = 0 % 28.13/7.25 | % 28.13/7.25 | From (313) and (170) follows: % 28.13/7.25 | (166) convergent_lines(all_1_3_3, all_1_4_4) = all_40_3_25 % 28.13/7.25 | % 28.13/7.25 | From (308) and (187) follows: % 28.13/7.25 | (88) convergent_lines(all_1_4_4, all_1_2_2) = all_8_2_7 % 28.13/7.25 | % 28.13/7.25 | Instantiating formula (18) with all_1_1_1, all_1_2_2, all_1_4_4, all_1_2_2 and discharging atoms distinct_lines(all_1_4_4, all_1_2_2) = all_1_1_1, ~ (convergent_lines(all_1_2_2, all_1_2_2) = 0), yields: % 28.13/7.25 | (320) all_1_1_1 = 0 | ~ (convergent_lines(all_1_2_2, all_1_4_4) = 0) % 28.13/7.25 | % 28.13/7.25 | Instantiating formula (63) with all_40_3_25, all_1_4_4, all_1_3_3, all_1_2_2 and discharging atoms convergent_lines(all_1_2_2, all_1_3_3) = 0, convergent_lines(all_1_3_3, all_1_4_4) = all_40_3_25, yields: % 28.13/7.25 | (321) all_40_3_25 = 0 | convergent_lines(all_1_2_2, all_1_4_4) = 0 % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (320), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (322) ~ (convergent_lines(all_1_2_2, all_1_4_4) = 0) % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (159), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (323) ~ (convergent_lines(all_1_4_4, all_1_2_2) = 0) % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (145), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (324) convergent_lines(all_1_4_4, all_1_2_2) = 0 % 28.13/7.25 | % 28.13/7.25 | Using (324) and (323) yields: % 28.13/7.25 | (325) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (323) ~ (convergent_lines(all_1_4_4, all_1_2_2) = 0) % 28.13/7.25 | (327) all_8_1_6 = 0 % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (321), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (328) convergent_lines(all_1_2_2, all_1_4_4) = 0 % 28.13/7.25 | % 28.13/7.25 | Using (328) and (322) yields: % 28.13/7.25 | (325) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (322) ~ (convergent_lines(all_1_2_2, all_1_4_4) = 0) % 28.13/7.25 | (331) all_40_3_25 = 0 % 28.13/7.25 | % 28.13/7.25 | From (331) and (166) follows: % 28.13/7.25 | (332) convergent_lines(all_1_3_3, all_1_4_4) = 0 % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (156), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (333) ~ (convergent_lines(all_1_3_3, all_1_4_4) = 0) % 28.13/7.25 | % 28.13/7.25 | Using (332) and (333) yields: % 28.13/7.25 | (325) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (332) convergent_lines(all_1_3_3, all_1_4_4) = 0 % 28.13/7.25 | (336) all_8_3_8 = 0 % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (89), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (337) ~ (all_8_3_8 = 0) % 28.13/7.25 | % 28.13/7.25 | Equations (336) can reduce 337 to: % 28.13/7.25 | (112) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (336) all_8_3_8 = 0 % 28.13/7.25 | (340) (all_8_0_5 = 0 & all_1_0_0 = 0) | (all_8_1_6 = 0 & all_8_2_7 = 0) % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (340), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (341) all_8_0_5 = 0 & all_1_0_0 = 0 % 28.13/7.25 | % 28.13/7.25 | Applying alpha-rule on (341) yields: % 28.13/7.25 | (129) all_8_0_5 = 0 % 28.13/7.25 | (343) all_1_0_0 = 0 % 28.13/7.25 | % 28.13/7.25 | Equations (343) can reduce 77 to: % 28.13/7.25 | (112) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (345) all_8_1_6 = 0 & all_8_2_7 = 0 % 28.13/7.25 | % 28.13/7.25 | Applying alpha-rule on (345) yields: % 28.13/7.25 | (327) all_8_1_6 = 0 % 28.13/7.25 | (347) all_8_2_7 = 0 % 28.13/7.25 | % 28.13/7.25 | From (347) and (88) follows: % 28.13/7.25 | (324) convergent_lines(all_1_4_4, all_1_2_2) = 0 % 28.13/7.25 | % 28.13/7.25 | Using (324) and (323) yields: % 28.13/7.25 | (325) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (324) convergent_lines(all_1_4_4, all_1_2_2) = 0 % 28.13/7.25 | (351) all_10_3_12 = 0 | convergent_lines(all_1_2_2, all_1_4_4) = 0 % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (321), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (328) convergent_lines(all_1_2_2, all_1_4_4) = 0 % 28.13/7.25 | % 28.13/7.25 | Using (328) and (322) yields: % 28.13/7.25 | (325) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (322) ~ (convergent_lines(all_1_2_2, all_1_4_4) = 0) % 28.13/7.25 | (331) all_40_3_25 = 0 % 28.13/7.25 | % 28.13/7.25 +-Applying beta-rule and splitting (351), into two cases. % 28.13/7.25 |-Branch one: % 28.13/7.25 | (328) convergent_lines(all_1_2_2, all_1_4_4) = 0 % 28.13/7.25 | % 28.13/7.25 | Using (328) and (322) yields: % 28.13/7.25 | (325) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (322) ~ (convergent_lines(all_1_2_2, all_1_4_4) = 0) % 28.13/7.25 | (359) all_10_3_12 = 0 % 28.13/7.25 | % 28.13/7.25 | Equations (359) can reduce 314 to: % 28.13/7.25 | (112) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (328) convergent_lines(all_1_2_2, all_1_4_4) = 0 % 28.13/7.25 | (111) all_1_1_1 = 0 % 28.13/7.25 | % 28.13/7.25 | Equations (111) can reduce 78 to: % 28.13/7.25 | (112) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.25 | (364) ~ (convergent_lines(all_1_2_2, all_1_3_3) = 0) % 28.13/7.25 | (365) all_12_1_14 = 0 % 28.13/7.25 | % 28.13/7.25 | Equations (365) can reduce 139 to: % 28.13/7.25 | (112) $false % 28.13/7.25 | % 28.13/7.25 |-The branch is then unsatisfiable % 28.13/7.25 |-Branch two: % 28.13/7.26 | (367) unorthogonal_lines(all_1_3_3, all_1_3_3) = all_1_0_0 % 28.13/7.26 | (368) all_12_0_13 = all_1_0_0 % 28.13/7.26 | % 28.13/7.26 | Combining equations (368,141) yields a new equation: % 28.13/7.26 | (369) all_1_0_0 = 0 % 28.13/7.26 | % 28.13/7.26 | Simplifying 369 yields: % 28.13/7.26 | (343) all_1_0_0 = 0 % 28.13/7.26 | % 28.13/7.26 | Equations (343) can reduce 77 to: % 28.13/7.26 | (112) $false % 28.13/7.26 | % 28.13/7.26 |-The branch is then unsatisfiable % 28.13/7.26 |-Branch two: % 28.13/7.26 | (372) ~ (convergent_lines(all_1_3_3, all_1_2_2) = 0) % 28.13/7.26 | (343) all_1_0_0 = 0 % 28.13/7.26 | % 28.13/7.26 | Equations (343) can reduce 77 to: % 28.13/7.26 | (112) $false % 28.13/7.26 | % 28.13/7.26 |-The branch is then unsatisfiable % 28.13/7.26 % SZS output end Proof for theBenchmark % 28.13/7.26 % 28.13/7.26 6641ms %------------------------------------------------------------------------------