%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GEO195+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 03:48:31 EDT 2022 % Result : Theorem 24.26s 7.87s % Output : Proof 36.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : GEO195+2 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n003.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 17 18:50:12 EDT 2022 % 0.12/0.33 % CPUTime : % 0.64/0.63 ____ _ % 0.64/0.63 ___ / __ \_____(_)___ ________ __________ % 0.64/0.63 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.64/0.63 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.64/0.63 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.64/0.63 % 0.64/0.63 A Theorem Prover for First-Order Logic % 0.64/0.63 (ePrincess v.1.0) % 0.64/0.63 % 0.64/0.63 (c) Philipp Rümmer, 2009-2015 % 0.64/0.63 (c) Peter Backeman, 2014-2015 % 0.64/0.63 (contributions by Angelo Brillout, Peter Baumgartner) % 0.64/0.63 Free software under GNU Lesser General Public License (LGPL). % 0.64/0.63 Bug reports to peter@backeman.se % 0.64/0.63 % 0.64/0.63 For more information, visit http://user.uu.se/~petba168/breu/ % 0.64/0.63 % 0.64/0.63 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.64/0.68 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.60/0.96 Prover 0: Preprocessing ... % 1.93/1.10 Prover 0: Warning: ignoring some quantifiers % 2.01/1.12 Prover 0: Constructing countermodel ... % 2.66/1.35 Prover 0: gave up % 2.66/1.35 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.92/1.38 Prover 1: Preprocessing ... % 3.18/1.46 Prover 1: Constructing countermodel ... % 3.18/1.50 Prover 1: gave up % 3.18/1.50 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.18/1.52 Prover 2: Preprocessing ... % 3.78/1.63 Prover 2: Warning: ignoring some quantifiers % 3.78/1.63 Prover 2: Constructing countermodel ... % 4.90/1.83 Prover 2: gave up % 4.90/1.83 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 4.90/1.85 Prover 3: Preprocessing ... % 4.90/1.86 Prover 3: Warning: ignoring some quantifiers % 4.90/1.86 Prover 3: Constructing countermodel ... % 5.17/1.93 Prover 3: gave up % 5.17/1.93 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 5.17/1.94 Prover 4: Preprocessing ... % 5.69/2.01 Prover 4: Warning: ignoring some quantifiers % 5.69/2.01 Prover 4: Constructing countermodel ... % 10.35/3.14 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 10.35/3.16 Prover 5: Preprocessing ... % 10.76/3.25 Prover 5: Constructing countermodel ... % 24.26/7.87 Prover 5: proved (4731ms) % 24.26/7.87 Prover 4: stopped % 24.26/7.87 % 24.26/7.87 No countermodel exists, formula is valid % 24.26/7.87 % SZS status Theorem for theBenchmark % 24.26/7.87 % 24.26/7.87 Generating proof ... found it (size 570) % 35.77/11.23 % 35.77/11.23 % SZS output start Proof for theBenchmark % 35.77/11.23 Assumed formulas after preprocessing and simplification: % 35.77/11.23 | (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) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (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] : (v4 = 0 | ~ (intersection_point(v0, v1) = v3) | ~ (distinct_points(v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v1) = v7 & apart_point_and_line(v2, v0) = v6 & convergent_lines(v0, v1) = v5 & ( ~ (v5 = 0) | ( ~ (v7 = 0) & ~ (v6 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (intersection_point(v0, v1) = v4) | ~ (apart_point_and_line(v2, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v0) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v4) = v7 & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (intersection_point(v0, v1) = v4) | ~ (apart_point_and_line(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v1) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v4) = v7 & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (line_connecting(v0, v1) = v3) | ~ (distinct_points(v2, v1) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v3) = v6 & distinct_points(v2, v0) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (line_connecting(v0, v1) = v3) | ~ (distinct_points(v2, v0) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v3) = v6 & distinct_points(v2, v1) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (apart_point_and_line(v2, v1) = v4) | ~ (apart_point_and_line(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (intersection_point(v0, v1) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v6) = v7 & ( ~ (v5 = 0) | v7 = 0)) | ( ~ (v4 = 0) & ~ (v3 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (distinct_points(v2, v1) = v4) | ~ (distinct_points(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (line_connecting(v0, v1) = v6 & apart_point_and_line(v2, v6) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v7 = 0) | ~ (v5 = 0))) | (v4 = 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, 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 | ~ (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 | ~ (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] : ( ~ (line_connecting(v0, v1) = v3) | ~ (apart_point_and_line(v2, v3) = 0) | ? [v4] : ? [v5] : ? [v6] : (distinct_points(v2, v1) = v6 & distinct_points(v2, v0) = v5 & distinct_points(v0, v1) = v4 & ( ~ (v4 = 0) | (v6 = 0 & v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (apart_point_and_line(v2, v1) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (intersection_point(v0, v1) = v5 & apart_point_and_line(v2, v0) = v4 & distinct_points(v2, v5) = v6 & (v6 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (apart_point_and_line(v2, v0) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (intersection_point(v0, v1) = v5 & apart_point_and_line(v2, v1) = v4 & distinct_points(v2, v5) = v6 & (v6 = 0 | ( ~ (v4 = 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] : ! [v3] : ( ~ (distinct_points(v2, v1) = v3) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (line_connecting(v0, v1) = v4 & apart_point_and_line(v2, v4) = v5 & distinct_points(v2, v0) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_points(v2, v0) = v3) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (line_connecting(v0, v1) = v4 & apart_point_and_line(v2, v4) = v5 & distinct_points(v2, v1) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (distinct_lines(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3)) & ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v0, v1) = 0) & ! [v0] : ~ (convergent_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_points(v0, v0) = 0) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = 0) & intersection_point(v1, v0) = v4 & intersection_point(v0, v1) = v3 & apart_point_and_line(v4, v2) = v5 & apart_point_and_line(v3, v2) = 0 & convergent_lines(v2, v1) = 0 & convergent_lines(v0, v2) = 0 & convergent_lines(v0, v1) = 0) % 36.13/11.29 | Applying alpha-rule on (0) yields: % 36.13/11.29 | (1) ! [v0] : ~ (distinct_points(v0, v0) = 0) % 36.13/11.29 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (apart_point_and_line(v2, v0) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (intersection_point(v0, v1) = v5 & apart_point_and_line(v2, v1) = v4 & distinct_points(v2, v5) = v6 & (v6 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))))) % 36.13/11.29 | (3) ! [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)) % 36.13/11.29 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) % 36.13/11.29 | (5) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = 0) & intersection_point(v1, v0) = v4 & intersection_point(v0, v1) = v3 & apart_point_and_line(v4, v2) = v5 & apart_point_and_line(v3, v2) = 0 & convergent_lines(v2, v1) = 0 & convergent_lines(v0, v2) = 0 & convergent_lines(v0, v1) = 0) % 36.13/11.30 | (6) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v0, v1) = 0) % 36.13/11.30 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) % 36.13/11.30 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) % 36.13/11.30 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) % 36.13/11.30 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (distinct_points(v2, v1) = v4) | ~ (distinct_points(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (line_connecting(v0, v1) = v6 & apart_point_and_line(v2, v6) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v7 = 0) | ~ (v5 = 0))) | (v4 = 0 & v3 = 0)) % 36.13/11.30 | (11) ! [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) % 36.13/11.30 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 36.13/11.30 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_points(v2, v1) = v3) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (line_connecting(v0, v1) = v4 & apart_point_and_line(v2, v4) = v5 & distinct_points(v2, v0) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v3 = 0)))) % 36.13/11.30 | (14) ! [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) % 36.13/11.30 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (apart_point_and_line(v2, v1) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (intersection_point(v0, v1) = v5 & apart_point_and_line(v2, v0) = v4 & distinct_points(v2, v5) = v6 & (v6 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))))) % 36.13/11.30 | (16) ! [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))) % 36.13/11.30 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) % 36.13/11.30 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) % 36.13/11.30 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (line_connecting(v0, v1) = v3) | ~ (distinct_points(v2, v1) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v3) = v6 & distinct_points(v2, v0) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & v4 = 0)))) % 36.13/11.30 | (20) ! [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))) % 36.13/11.31 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) % 36.13/11.31 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) % 36.13/11.31 | (23) ! [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))) % 36.13/11.31 | (24) ! [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) % 36.13/11.31 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_points(v2, v0) = v3) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (line_connecting(v0, v1) = v4 & apart_point_and_line(v2, v4) = v5 & distinct_points(v2, v1) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v3 = 0)))) % 36.13/11.31 | (26) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (distinct_lines(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3)) % 36.13/11.31 | (27) ! [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))) % 36.13/11.31 | (28) ! [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))) % 36.13/11.31 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (intersection_point(v0, v1) = v4) | ~ (apart_point_and_line(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v1) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v4) = v7 & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v3 = 0))))) % 36.13/11.31 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (intersection_point(v0, v1) = v3) | ~ (distinct_points(v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v1) = v7 & apart_point_and_line(v2, v0) = v6 & convergent_lines(v0, v1) = v5 & ( ~ (v5 = 0) | ( ~ (v7 = 0) & ~ (v6 = 0))))) % 36.13/11.31 | (31) ! [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)) % 36.13/11.31 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (line_connecting(v0, v1) = v3) | ~ (apart_point_and_line(v2, v3) = 0) | ? [v4] : ? [v5] : ? [v6] : (distinct_points(v2, v1) = v6 & distinct_points(v2, v0) = v5 & distinct_points(v0, v1) = v4 & ( ~ (v4 = 0) | (v6 = 0 & v5 = 0)))) % 36.13/11.31 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (apart_point_and_line(v2, v1) = v4) | ~ (apart_point_and_line(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (intersection_point(v0, v1) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v6) = v7 & ( ~ (v5 = 0) | v7 = 0)) | ( ~ (v4 = 0) & ~ (v3 = 0))) % 36.13/11.32 | (34) ! [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)) % 36.13/11.32 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (line_connecting(v0, v1) = v3) | ~ (distinct_points(v2, v0) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v3) = v6 & distinct_points(v2, v1) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & v4 = 0)))) % 36.13/11.32 | (36) ! [v0] : ~ (distinct_lines(v0, v0) = 0) % 36.13/11.32 | (37) ! [v0] : ~ (convergent_lines(v0, v0) = 0) % 36.13/11.32 | (38) ! [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))) % 36.13/11.32 | (39) ! [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)) % 36.13/11.32 | (40) ! [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) % 36.13/11.32 | (41) ! [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)) % 36.13/11.32 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 36.13/11.32 | (43) ! [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))) % 36.13/11.32 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) % 36.13/11.32 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (intersection_point(v0, v1) = v4) | ~ (apart_point_and_line(v2, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v0) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v4) = v7 & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v3 = 0))))) % 36.13/11.32 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) % 36.13/11.32 | % 36.13/11.32 | Instantiating (5) with all_1_0_0, all_1_1_1, all_1_2_2, all_1_3_3, all_1_4_4, all_1_5_5 yields: % 36.13/11.32 | (47) ~ (all_1_0_0 = 0) & intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1 & intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2 & apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0 & apart_point_and_line(all_1_2_2, all_1_3_3) = 0 & convergent_lines(all_1_3_3, all_1_4_4) = 0 & convergent_lines(all_1_5_5, all_1_3_3) = 0 & convergent_lines(all_1_5_5, all_1_4_4) = 0 % 36.13/11.32 | % 36.13/11.32 | Applying alpha-rule on (47) yields: % 36.13/11.32 | (48) ~ (all_1_0_0 = 0) % 36.13/11.32 | (49) convergent_lines(all_1_5_5, all_1_3_3) = 0 % 36.13/11.32 | (50) intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1 % 36.13/11.32 | (51) apart_point_and_line(all_1_2_2, all_1_3_3) = 0 % 36.13/11.32 | (52) convergent_lines(all_1_3_3, all_1_4_4) = 0 % 36.13/11.32 | (53) apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0 % 36.13/11.32 | (54) intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2 % 36.13/11.32 | (55) convergent_lines(all_1_5_5, all_1_4_4) = 0 % 36.13/11.32 | % 36.13/11.32 | Instantiating formula (37) with all_1_5_5 yields: % 36.13/11.32 | (56) ~ (convergent_lines(all_1_5_5, all_1_5_5) = 0) % 36.13/11.32 | % 36.13/11.32 | Instantiating formula (23) with all_1_0_0, all_1_0_0, all_1_3_3, all_1_3_3, all_1_1_1, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 36.13/11.32 | (57) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (33) with 0, 0, all_1_2_2, all_1_3_3, all_1_3_3 and discharging atoms apart_point_and_line(all_1_2_2, all_1_3_3) = 0, yields: % 36.13/11.33 | (58) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_3_3, all_1_3_3) = v1 & convergent_lines(all_1_3_3, all_1_3_3) = v0 & distinct_points(all_1_2_2, v1) = v2 & ( ~ (v0 = 0) | v2 = 0)) % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (40) with all_1_0_0, all_1_1_1, all_1_3_3, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_1_3_3) = 0, yields: % 36.13/11.33 | (59) all_1_0_0 = 0 | distinct_points(all_1_2_2, all_1_1_1) = 0 % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (2) with all_1_0_0, all_1_1_1, all_1_4_4, all_1_3_3 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 36.13/11.33 | (60) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_3_3, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_4_4) = v0 & distinct_points(all_1_1_1, v1) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_1_0_0 = 0)))) % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (2) with 0, all_1_2_2, all_1_4_4, all_1_3_3 and discharging atoms apart_point_and_line(all_1_2_2, all_1_3_3) = 0, convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 36.13/11.33 | (61) ? [v0] : ? [v1] : (intersection_point(all_1_3_3, all_1_4_4) = v1 & apart_point_and_line(all_1_2_2, all_1_4_4) = v0 & distinct_points(all_1_2_2, v1) = 0) % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (6) with all_1_4_4, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 36.13/11.33 | (62) distinct_lines(all_1_3_3, all_1_4_4) = 0 % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (15) with all_1_0_0, all_1_1_1, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 36.13/11.33 | (63) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_5_5, all_1_3_3) = v1 & apart_point_and_line(all_1_1_1, all_1_5_5) = v0 & distinct_points(all_1_1_1, v1) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_1_0_0 = 0)))) % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (15) with 0, all_1_2_2, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_2_2, all_1_3_3) = 0, convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 36.13/11.33 | (64) ? [v0] : ? [v1] : (intersection_point(all_1_5_5, all_1_3_3) = v1 & apart_point_and_line(all_1_2_2, all_1_5_5) = v0 & distinct_points(all_1_2_2, v1) = 0) % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (6) with all_1_3_3, all_1_5_5 and discharging atoms convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 36.13/11.33 | (65) distinct_lines(all_1_5_5, all_1_3_3) = 0 % 36.13/11.33 | % 36.13/11.33 | Instantiating formula (6) with all_1_4_4, all_1_5_5 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 36.13/11.33 | (66) distinct_lines(all_1_5_5, all_1_4_4) = 0 % 36.13/11.33 | % 36.13/11.33 | Instantiating (61) with all_17_0_6, all_17_1_7 yields: % 36.13/11.33 | (67) intersection_point(all_1_3_3, all_1_4_4) = all_17_0_6 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7 & distinct_points(all_1_2_2, all_17_0_6) = 0 % 36.13/11.33 | % 36.13/11.33 | Applying alpha-rule on (67) yields: % 36.13/11.33 | (68) intersection_point(all_1_3_3, all_1_4_4) = all_17_0_6 % 36.13/11.33 | (69) apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7 % 36.13/11.33 | (70) distinct_points(all_1_2_2, all_17_0_6) = 0 % 36.13/11.33 | % 36.13/11.33 | Instantiating (64) with all_19_0_8, all_19_1_9 yields: % 36.13/11.33 | (71) intersection_point(all_1_5_5, all_1_3_3) = all_19_0_8 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9 & distinct_points(all_1_2_2, all_19_0_8) = 0 % 36.13/11.33 | % 36.13/11.33 | Applying alpha-rule on (71) yields: % 36.13/11.33 | (72) intersection_point(all_1_5_5, all_1_3_3) = all_19_0_8 % 36.13/11.33 | (73) apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9 % 36.13/11.33 | (74) distinct_points(all_1_2_2, all_19_0_8) = 0 % 36.13/11.33 | % 36.13/11.33 | Instantiating (60) with all_21_0_10, all_21_1_11, all_21_2_12 yields: % 36.13/11.33 | (75) intersection_point(all_1_3_3, all_1_4_4) = all_21_1_11 & apart_point_and_line(all_1_1_1, all_1_4_4) = all_21_2_12 & distinct_points(all_1_1_1, all_21_1_11) = all_21_0_10 & (all_21_0_10 = 0 | ( ~ (all_21_2_12 = 0) & ~ (all_1_0_0 = 0))) % 36.13/11.33 | % 36.13/11.33 | Applying alpha-rule on (75) yields: % 36.13/11.33 | (76) intersection_point(all_1_3_3, all_1_4_4) = all_21_1_11 % 36.13/11.33 | (77) apart_point_and_line(all_1_1_1, all_1_4_4) = all_21_2_12 % 36.13/11.33 | (78) distinct_points(all_1_1_1, all_21_1_11) = all_21_0_10 % 36.13/11.33 | (79) all_21_0_10 = 0 | ( ~ (all_21_2_12 = 0) & ~ (all_1_0_0 = 0)) % 36.13/11.33 | % 36.13/11.33 | Instantiating (63) with all_23_0_13, all_23_1_14, all_23_2_15 yields: % 36.13/11.33 | (80) intersection_point(all_1_5_5, all_1_3_3) = all_23_1_14 & apart_point_and_line(all_1_1_1, all_1_5_5) = all_23_2_15 & distinct_points(all_1_1_1, all_23_1_14) = all_23_0_13 & (all_23_0_13 = 0 | ( ~ (all_23_2_15 = 0) & ~ (all_1_0_0 = 0))) % 36.13/11.33 | % 36.13/11.33 | Applying alpha-rule on (80) yields: % 36.13/11.33 | (81) intersection_point(all_1_5_5, all_1_3_3) = all_23_1_14 % 36.13/11.33 | (82) apart_point_and_line(all_1_1_1, all_1_5_5) = all_23_2_15 % 36.13/11.33 | (83) distinct_points(all_1_1_1, all_23_1_14) = all_23_0_13 % 36.13/11.33 | (84) all_23_0_13 = 0 | ( ~ (all_23_2_15 = 0) & ~ (all_1_0_0 = 0)) % 36.13/11.33 | % 36.13/11.33 | Instantiating (58) with all_25_0_16, all_25_1_17, all_25_2_18 yields: % 36.13/11.33 | (85) intersection_point(all_1_3_3, all_1_3_3) = all_25_1_17 & convergent_lines(all_1_3_3, all_1_3_3) = all_25_2_18 & distinct_points(all_1_2_2, all_25_1_17) = all_25_0_16 & ( ~ (all_25_2_18 = 0) | all_25_0_16 = 0) % 36.13/11.33 | % 36.13/11.33 | Applying alpha-rule on (85) yields: % 36.13/11.33 | (86) intersection_point(all_1_3_3, all_1_3_3) = all_25_1_17 % 36.13/11.33 | (87) convergent_lines(all_1_3_3, all_1_3_3) = all_25_2_18 % 36.13/11.33 | (88) distinct_points(all_1_2_2, all_25_1_17) = all_25_0_16 % 36.13/11.33 | (89) ~ (all_25_2_18 = 0) | all_25_0_16 = 0 % 36.13/11.33 | % 36.13/11.33 +-Applying beta-rule and splitting (59), into two cases. % 36.13/11.33 |-Branch one: % 36.13/11.33 | (90) distinct_points(all_1_2_2, all_1_1_1) = 0 % 36.13/11.33 | % 36.13/11.33 +-Applying beta-rule and splitting (57), into two cases. % 36.13/11.33 |-Branch one: % 36.13/11.33 | (91) all_1_0_0 = 0 % 36.13/11.33 | % 36.13/11.33 | Equations (91) can reduce 48 to: % 36.13/11.33 | (92) $false % 36.13/11.33 | % 36.13/11.33 |-The branch is then unsatisfiable % 36.13/11.33 |-Branch two: % 36.13/11.33 | (48) ~ (all_1_0_0 = 0) % 36.13/11.34 | (94) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.13/11.34 | % 36.13/11.34 | Instantiating (94) with all_35_0_19, all_35_1_20, all_35_2_21, all_35_3_22 yields: % 36.13/11.34 | (95) apart_point_and_line(all_1_1_1, all_1_3_3) = all_35_0_19 & apart_point_and_line(all_1_1_1, all_1_3_3) = all_35_1_20 & distinct_lines(all_1_3_3, all_1_3_3) = all_35_2_21 & distinct_points(all_1_1_1, all_1_1_1) = all_35_3_22 & ( ~ (all_35_2_21 = 0) | ~ (all_35_3_22 = 0) | all_35_0_19 = 0 | all_35_1_20 = 0) % 36.13/11.34 | % 36.13/11.34 | Applying alpha-rule on (95) yields: % 36.13/11.34 | (96) apart_point_and_line(all_1_1_1, all_1_3_3) = all_35_1_20 % 36.13/11.34 | (97) apart_point_and_line(all_1_1_1, all_1_3_3) = all_35_0_19 % 36.13/11.34 | (98) distinct_lines(all_1_3_3, all_1_3_3) = all_35_2_21 % 36.13/11.34 | (99) distinct_points(all_1_1_1, all_1_1_1) = all_35_3_22 % 36.13/11.34 | (100) ~ (all_35_2_21 = 0) | ~ (all_35_3_22 = 0) | all_35_0_19 = 0 | all_35_1_20 = 0 % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (9) with all_1_3_3, all_1_4_4, all_17_0_6, all_21_1_11 and discharging atoms intersection_point(all_1_3_3, all_1_4_4) = all_21_1_11, intersection_point(all_1_3_3, all_1_4_4) = all_17_0_6, yields: % 36.13/11.34 | (101) all_21_1_11 = all_17_0_6 % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (9) with all_1_5_5, all_1_3_3, all_19_0_8, all_23_1_14 and discharging atoms intersection_point(all_1_5_5, all_1_3_3) = all_23_1_14, intersection_point(all_1_5_5, all_1_3_3) = all_19_0_8, yields: % 36.13/11.34 | (102) all_23_1_14 = all_19_0_8 % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (22) with all_1_1_1, all_1_3_3, all_35_0_19, all_1_0_0 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_35_0_19, apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 36.13/11.34 | (103) all_35_0_19 = all_1_0_0 % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (22) with all_1_1_1, all_1_3_3, all_35_1_20, all_35_0_19 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_35_0_19, apart_point_and_line(all_1_1_1, all_1_3_3) = all_35_1_20, yields: % 36.13/11.34 | (104) all_35_0_19 = all_35_1_20 % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (1) with all_1_1_1 yields: % 36.13/11.34 | (105) ~ (distinct_points(all_1_1_1, all_1_1_1) = 0) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (1) with all_1_2_2 yields: % 36.13/11.34 | (106) ~ (distinct_points(all_1_2_2, all_1_2_2) = 0) % 36.13/11.34 | % 36.13/11.34 | Combining equations (103,104) yields a new equation: % 36.13/11.34 | (107) all_35_1_20 = all_1_0_0 % 36.13/11.34 | % 36.13/11.34 | From (101) and (76) follows: % 36.13/11.34 | (68) intersection_point(all_1_3_3, all_1_4_4) = all_17_0_6 % 36.13/11.34 | % 36.13/11.34 | From (102) and (81) follows: % 36.13/11.34 | (72) intersection_point(all_1_5_5, all_1_3_3) = all_19_0_8 % 36.13/11.34 | % 36.13/11.34 | From (107) and (96) follows: % 36.13/11.34 | (53) apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0 % 36.13/11.34 | % 36.13/11.34 | From (102) and (83) follows: % 36.13/11.34 | (111) distinct_points(all_1_1_1, all_19_0_8) = all_23_0_13 % 36.13/11.34 | % 36.13/11.34 | From (101) and (78) follows: % 36.13/11.34 | (112) distinct_points(all_1_1_1, all_17_0_6) = all_21_0_10 % 36.13/11.34 | % 36.13/11.34 | Using (99) and (105) yields: % 36.13/11.34 | (113) ~ (all_35_3_22 = 0) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (45) with all_25_1_17, all_1_0_0, all_1_1_1, all_1_3_3, all_1_3_3 and discharging atoms intersection_point(all_1_3_3, all_1_3_3) = all_25_1_17, apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 36.13/11.34 | (114) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v1 & convergent_lines(all_1_3_3, all_1_3_3) = v0 & distinct_points(all_1_1_1, all_25_1_17) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_0_0 = 0)))) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (29) with all_17_0_6, all_1_0_0, all_1_1_1, all_1_4_4, all_1_3_3 and discharging atoms intersection_point(all_1_3_3, all_1_4_4) = all_17_0_6, apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 36.13/11.34 | (115) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & distinct_points(all_1_1_1, all_17_0_6) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_0_0 = 0)))) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (45) with all_19_0_8, all_1_0_0, all_1_1_1, all_1_3_3, all_1_5_5 and discharging atoms intersection_point(all_1_5_5, all_1_3_3) = all_19_0_8, apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 36.13/11.34 | (116) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & convergent_lines(all_1_5_5, all_1_3_3) = v0 & distinct_points(all_1_1_1, all_19_0_8) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_0_0 = 0)))) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (29) with all_1_1_1, all_21_2_12, all_1_1_1, all_1_5_5, all_1_4_4 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1, apart_point_and_line(all_1_1_1, all_1_4_4) = all_21_2_12, yields: % 36.13/11.34 | (117) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & convergent_lines(all_1_4_4, all_1_5_5) = v0 & distinct_points(all_1_1_1, all_1_1_1) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_21_2_12 = 0)))) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (45) with all_1_2_2, all_21_2_12, all_1_1_1, all_1_4_4, all_1_5_5 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2, apart_point_and_line(all_1_1_1, all_1_4_4) = all_21_2_12, yields: % 36.13/11.34 | (118) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & convergent_lines(all_1_5_5, all_1_4_4) = v0 & distinct_points(all_1_1_1, all_1_2_2) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_21_2_12 = 0)))) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (45) with all_17_0_6, all_21_2_12, all_1_1_1, all_1_4_4, all_1_3_3 and discharging atoms intersection_point(all_1_3_3, all_1_4_4) = all_17_0_6, apart_point_and_line(all_1_1_1, all_1_4_4) = all_21_2_12, yields: % 36.13/11.34 | (119) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v1 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & distinct_points(all_1_1_1, all_17_0_6) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_21_2_12 = 0)))) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (15) with all_21_2_12, all_1_1_1, all_1_4_4, all_1_3_3 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_21_2_12, convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 36.13/11.34 | (120) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_3_3, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_3_3) = v0 & distinct_points(all_1_1_1, v1) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_21_2_12 = 0)))) % 36.13/11.34 | % 36.13/11.34 | Instantiating formula (15) with all_21_2_12, all_1_1_1, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_21_2_12, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 36.13/11.35 | (121) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_5_5, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_5_5) = v0 & distinct_points(all_1_1_1, v1) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_21_2_12 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (45) with all_1_1_1, all_23_2_15, all_1_1_1, all_1_5_5, all_1_4_4 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1, apart_point_and_line(all_1_1_1, all_1_5_5) = all_23_2_15, yields: % 36.13/11.35 | (122) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & convergent_lines(all_1_4_4, all_1_5_5) = v0 & distinct_points(all_1_1_1, all_1_1_1) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_23_2_15 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (29) with all_1_2_2, all_23_2_15, all_1_1_1, all_1_4_4, all_1_5_5 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2, apart_point_and_line(all_1_1_1, all_1_5_5) = all_23_2_15, yields: % 36.13/11.35 | (123) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & convergent_lines(all_1_5_5, all_1_4_4) = v0 & distinct_points(all_1_1_1, all_1_2_2) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_23_2_15 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (29) with all_19_0_8, all_23_2_15, all_1_1_1, all_1_3_3, all_1_5_5 and discharging atoms intersection_point(all_1_5_5, all_1_3_3) = all_19_0_8, apart_point_and_line(all_1_1_1, all_1_5_5) = all_23_2_15, yields: % 36.13/11.35 | (124) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v1 & convergent_lines(all_1_5_5, all_1_3_3) = v0 & distinct_points(all_1_1_1, all_19_0_8) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_23_2_15 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (2) with all_23_2_15, all_1_1_1, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_23_2_15, convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 36.13/11.35 | (125) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_5_5, all_1_3_3) = v1 & apart_point_and_line(all_1_1_1, all_1_3_3) = v0 & distinct_points(all_1_1_1, v1) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_23_2_15 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (2) with all_23_2_15, all_1_1_1, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_23_2_15, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 36.13/11.35 | (126) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_5_5, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_4_4) = v0 & distinct_points(all_1_1_1, v1) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_23_2_15 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (23) with all_17_1_7, all_17_1_7, all_1_4_4, all_1_4_4, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, yields: % 36.13/11.35 | (127) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (29) with all_1_1_1, all_17_1_7, all_1_2_2, all_1_5_5, all_1_4_4 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1, apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, yields: % 36.13/11.35 | (128) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_5_5) = v1 & convergent_lines(all_1_4_4, all_1_5_5) = v0 & distinct_points(all_1_2_2, all_1_1_1) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_17_1_7 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (45) with all_1_2_2, all_17_1_7, all_1_2_2, all_1_4_4, all_1_5_5 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2, apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, yields: % 36.13/11.35 | (129) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_5_5) = v1 & convergent_lines(all_1_5_5, all_1_4_4) = v0 & distinct_points(all_1_2_2, all_1_2_2) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_17_1_7 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (15) with all_17_1_7, all_1_2_2, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 36.13/11.35 | (130) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_5_5, all_1_4_4) = v1 & apart_point_and_line(all_1_2_2, all_1_5_5) = v0 & distinct_points(all_1_2_2, v1) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_17_1_7 = 0)))) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (23) with all_19_1_9, all_1_0_0, all_1_5_5, all_1_3_3, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.13/11.35 | (131) all_19_1_9 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (28) with all_1_0_0, all_19_1_9, all_1_5_5, all_1_3_3, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.13/11.35 | (132) all_19_1_9 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (33) with all_19_1_9, 0, all_1_2_2, all_1_5_5, all_1_3_3 and discharging atoms apart_point_and_line(all_1_2_2, all_1_3_3) = 0, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.13/11.35 | (133) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_3_3, all_1_5_5) = v1 & convergent_lines(all_1_3_3, all_1_5_5) = v0 & distinct_points(all_1_2_2, v1) = v2 & ( ~ (v0 = 0) | v2 = 0)) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (23) with all_19_1_9, all_17_1_7, all_1_5_5, all_1_4_4, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.13/11.35 | (134) all_19_1_9 = 0 | all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (28) with all_17_1_7, all_19_1_9, all_1_5_5, all_1_4_4, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.13/11.35 | (135) all_19_1_9 = 0 | all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.13/11.35 | % 36.13/11.35 | Instantiating formula (45) with all_1_1_1, all_19_1_9, all_1_2_2, all_1_5_5, all_1_4_4 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.13/11.35 | (136) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & convergent_lines(all_1_4_4, all_1_5_5) = v0 & distinct_points(all_1_2_2, all_1_1_1) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_19_1_9 = 0)))) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (29) with all_1_2_2, all_19_1_9, all_1_2_2, all_1_4_4, all_1_5_5 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.13/11.36 | (137) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & convergent_lines(all_1_5_5, all_1_4_4) = v0 & distinct_points(all_1_2_2, all_1_2_2) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_19_1_9 = 0)))) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (2) with all_19_1_9, all_1_2_2, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 36.13/11.36 | (138) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_5_5, all_1_4_4) = v1 & apart_point_and_line(all_1_2_2, all_1_4_4) = v0 & distinct_points(all_1_2_2, v1) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_19_1_9 = 0)))) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (20) with all_17_1_7, all_17_1_7, all_1_4_4, all_1_5_5, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, distinct_lines(all_1_5_5, all_1_4_4) = 0, yields: % 36.13/11.36 | (139) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (38) with all_19_1_9, all_19_1_9, all_1_4_4, all_1_5_5, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, distinct_lines(all_1_5_5, all_1_4_4) = 0, yields: % 36.13/11.36 | (140) all_19_1_9 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (10) with all_35_3_22, all_35_3_22, all_1_1_1, all_1_1_1, all_1_1_1 and discharging atoms distinct_points(all_1_1_1, all_1_1_1) = all_35_3_22, yields: % 36.13/11.36 | (141) all_35_3_22 = 0 | ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_1_1, all_1_1_1) = v1 & apart_point_and_line(all_1_1_1, v1) = v2 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (13) with 0, all_1_2_2, all_19_0_8, all_1_2_2 and discharging atoms distinct_points(all_1_2_2, all_19_0_8) = 0, yields: % 36.13/11.36 | (142) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_19_0_8) = v0 & apart_point_and_line(all_1_2_2, v0) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (16) with all_17_1_7, all_17_1_7, all_1_4_4, all_1_4_4, all_19_0_8, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, distinct_points(all_1_2_2, all_19_0_8) = 0, yields: % 36.13/11.36 | (143) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_19_0_8, all_1_4_4) = v2 & apart_point_and_line(all_19_0_8, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (16) with all_19_1_9, all_19_1_9, all_1_5_5, all_1_5_5, all_19_0_8, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, distinct_points(all_1_2_2, all_19_0_8) = 0, yields: % 36.13/11.36 | (144) all_19_1_9 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_19_0_8, all_1_5_5) = v2 & apart_point_and_line(all_19_0_8, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (13) with all_23_0_13, all_1_1_1, all_19_0_8, all_1_2_2 and discharging atoms distinct_points(all_1_1_1, all_19_0_8) = all_23_0_13, distinct_points(all_1_2_2, all_19_0_8) = 0, yields: % 36.13/11.36 | (145) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_19_0_8) = v0 & apart_point_and_line(all_1_1_1, v0) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v2 & ( ~ (v1 = 0) | (v2 = 0 & all_23_0_13 = 0))) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (13) with all_21_0_10, all_1_1_1, all_17_0_6, all_1_2_2 and discharging atoms distinct_points(all_1_1_1, all_17_0_6) = all_21_0_10, distinct_points(all_1_2_2, all_17_0_6) = 0, yields: % 36.13/11.36 | (146) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_17_0_6) = v0 & apart_point_and_line(all_1_1_1, v0) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v2 & ( ~ (v1 = 0) | (v2 = 0 & all_21_0_10 = 0))) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (13) with all_35_3_22, all_1_1_1, all_1_1_1, all_1_2_2 and discharging atoms distinct_points(all_1_1_1, all_1_1_1) = all_35_3_22, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 36.13/11.36 | (147) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_1_1_1) = v0 & apart_point_and_line(all_1_1_1, v0) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v2 & ( ~ (v1 = 0) | (v2 = 0 & all_35_3_22 = 0))) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (43) with all_1_4_4, all_1_3_3, all_19_0_8, all_1_2_2 and discharging atoms distinct_lines(all_1_3_3, all_1_4_4) = 0, distinct_points(all_1_2_2, all_19_0_8) = 0, yields: % 36.13/11.36 | (148) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_19_0_8, all_1_3_3) = v2 & apart_point_and_line(all_19_0_8, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v0 & apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (43) with all_1_3_3, all_1_5_5, all_19_0_8, all_1_2_2 and discharging atoms distinct_lines(all_1_5_5, all_1_3_3) = 0, distinct_points(all_1_2_2, all_19_0_8) = 0, yields: % 36.13/11.36 | (149) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_19_0_8, all_1_3_3) = v3 & apart_point_and_line(all_19_0_8, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v1 & apart_point_and_line(all_1_2_2, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (43) with all_1_4_4, all_1_5_5, all_19_0_8, all_1_2_2 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = 0, distinct_points(all_1_2_2, all_19_0_8) = 0, yields: % 36.13/11.36 | (150) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_19_0_8, all_1_4_4) = v3 & apart_point_and_line(all_19_0_8, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & apart_point_and_line(all_1_2_2, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (13) with 0, all_1_2_2, all_17_0_6, all_1_2_2 and discharging atoms distinct_points(all_1_2_2, all_17_0_6) = 0, yields: % 36.13/11.36 | (151) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_17_0_6) = v0 & apart_point_and_line(all_1_2_2, v0) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (16) with all_17_1_7, all_17_1_7, all_1_4_4, all_1_4_4, all_17_0_6, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, distinct_points(all_1_2_2, all_17_0_6) = 0, yields: % 36.13/11.36 | (152) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_17_0_6, all_1_4_4) = v2 & apart_point_and_line(all_17_0_6, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.13/11.36 | % 36.13/11.36 | Instantiating formula (16) with all_19_1_9, all_17_1_7, all_1_5_5, all_1_4_4, all_17_0_6, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, distinct_points(all_1_2_2, all_17_0_6) = 0, yields: % 36.13/11.37 | (153) all_19_1_9 = 0 | all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_17_0_6, all_1_4_4) = v1 & apart_point_and_line(all_17_0_6, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.13/11.37 | % 36.13/11.37 | Instantiating formula (43) with all_1_4_4, all_1_3_3, all_17_0_6, all_1_2_2 and discharging atoms distinct_lines(all_1_3_3, all_1_4_4) = 0, distinct_points(all_1_2_2, all_17_0_6) = 0, yields: % 36.13/11.37 | (154) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_17_0_6, all_1_3_3) = v2 & apart_point_and_line(all_17_0_6, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v0 & apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 36.13/11.37 | % 36.13/11.37 | Instantiating formula (43) with all_1_3_3, all_1_5_5, all_17_0_6, all_1_2_2 and discharging atoms distinct_lines(all_1_5_5, all_1_3_3) = 0, distinct_points(all_1_2_2, all_17_0_6) = 0, yields: % 36.13/11.37 | (155) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_17_0_6, all_1_3_3) = v3 & apart_point_and_line(all_17_0_6, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v1 & apart_point_and_line(all_1_2_2, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 36.13/11.37 | % 36.13/11.37 | Instantiating formula (43) with all_1_4_4, all_1_5_5, all_17_0_6, all_1_2_2 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = 0, distinct_points(all_1_2_2, all_17_0_6) = 0, yields: % 36.13/11.37 | (156) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_17_0_6, all_1_4_4) = v3 & apart_point_and_line(all_17_0_6, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & apart_point_and_line(all_1_2_2, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 36.13/11.37 | % 36.13/11.37 | Instantiating formula (13) with 0, all_1_2_2, all_1_1_1, all_1_2_2 and discharging atoms distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 36.13/11.37 | (157) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_1_1_1) = v0 & apart_point_and_line(all_1_2_2, v0) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 36.13/11.37 | % 36.13/11.37 | Instantiating formula (16) with all_19_1_9, all_17_1_7, all_1_5_5, all_1_4_4, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 36.13/11.37 | (158) all_19_1_9 = 0 | all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.13/11.37 | % 36.13/11.37 | Instantiating formula (16) with all_19_1_9, all_19_1_9, all_1_5_5, all_1_5_5, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 36.13/11.37 | (159) all_19_1_9 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.13/11.37 | % 36.13/11.37 | Instantiating formula (43) with all_1_4_4, all_1_5_5, all_1_1_1, all_1_2_2 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = 0, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 36.13/11.37 | (160) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & apart_point_and_line(all_1_2_2, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 36.13/11.37 | % 36.13/11.37 | Instantiating (160) with all_50_0_23, all_50_1_24, all_50_2_25, all_50_3_26 yields: % 36.13/11.37 | (161) apart_point_and_line(all_1_1_1, all_1_4_4) = all_50_0_23 & apart_point_and_line(all_1_1_1, all_1_5_5) = all_50_1_24 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_50_2_25 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_50_3_26 & (all_50_0_23 = 0 | all_50_1_24 = 0 | all_50_2_25 = 0 | all_50_3_26 = 0) % 36.13/11.37 | % 36.13/11.37 | Applying alpha-rule on (161) yields: % 36.13/11.37 | (162) apart_point_and_line(all_1_1_1, all_1_5_5) = all_50_1_24 % 36.13/11.37 | (163) apart_point_and_line(all_1_2_2, all_1_5_5) = all_50_3_26 % 36.13/11.37 | (164) apart_point_and_line(all_1_1_1, all_1_4_4) = all_50_0_23 % 36.13/11.37 | (165) apart_point_and_line(all_1_2_2, all_1_4_4) = all_50_2_25 % 36.13/11.37 | (166) all_50_0_23 = 0 | all_50_1_24 = 0 | all_50_2_25 = 0 | all_50_3_26 = 0 % 36.13/11.37 | % 36.13/11.37 | Instantiating (156) with all_52_0_27, all_52_1_28, all_52_2_29, all_52_3_30 yields: % 36.13/11.37 | (167) apart_point_and_line(all_17_0_6, all_1_4_4) = all_52_0_27 & apart_point_and_line(all_17_0_6, all_1_5_5) = all_52_1_28 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_52_2_29 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_52_3_30 & (all_52_0_27 = 0 | all_52_1_28 = 0 | all_52_2_29 = 0 | all_52_3_30 = 0) % 36.13/11.37 | % 36.13/11.37 | Applying alpha-rule on (167) yields: % 36.13/11.37 | (168) apart_point_and_line(all_1_2_2, all_1_5_5) = all_52_3_30 % 36.58/11.37 | (169) apart_point_and_line(all_17_0_6, all_1_5_5) = all_52_1_28 % 36.58/11.37 | (170) apart_point_and_line(all_1_2_2, all_1_4_4) = all_52_2_29 % 36.58/11.37 | (171) apart_point_and_line(all_17_0_6, all_1_4_4) = all_52_0_27 % 36.58/11.37 | (172) all_52_0_27 = 0 | all_52_1_28 = 0 | all_52_2_29 = 0 | all_52_3_30 = 0 % 36.58/11.37 | % 36.58/11.37 | Instantiating (155) with all_54_0_31, all_54_1_32, all_54_2_33, all_54_3_34 yields: % 36.58/11.37 | (173) apart_point_and_line(all_17_0_6, all_1_3_3) = all_54_0_31 & apart_point_and_line(all_17_0_6, all_1_5_5) = all_54_1_32 & apart_point_and_line(all_1_2_2, all_1_3_3) = all_54_2_33 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_54_3_34 & (all_54_0_31 = 0 | all_54_1_32 = 0 | all_54_2_33 = 0 | all_54_3_34 = 0) % 36.58/11.37 | % 36.58/11.37 | Applying alpha-rule on (173) yields: % 36.58/11.37 | (174) apart_point_and_line(all_17_0_6, all_1_3_3) = all_54_0_31 % 36.58/11.37 | (175) all_54_0_31 = 0 | all_54_1_32 = 0 | all_54_2_33 = 0 | all_54_3_34 = 0 % 36.58/11.37 | (176) apart_point_and_line(all_1_2_2, all_1_5_5) = all_54_3_34 % 36.58/11.37 | (177) apart_point_and_line(all_17_0_6, all_1_5_5) = all_54_1_32 % 36.58/11.37 | (178) apart_point_and_line(all_1_2_2, all_1_3_3) = all_54_2_33 % 36.58/11.37 | % 36.58/11.37 | Instantiating (154) with all_56_0_35, all_56_1_36, all_56_2_37, all_56_3_38 yields: % 36.58/11.37 | (179) apart_point_and_line(all_17_0_6, all_1_3_3) = all_56_1_36 & apart_point_and_line(all_17_0_6, all_1_4_4) = all_56_0_35 & apart_point_and_line(all_1_2_2, all_1_3_3) = all_56_3_38 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_56_2_37 & (all_56_0_35 = 0 | all_56_1_36 = 0 | all_56_2_37 = 0 | all_56_3_38 = 0) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (179) yields: % 36.58/11.38 | (180) apart_point_and_line(all_17_0_6, all_1_3_3) = all_56_1_36 % 36.58/11.38 | (181) all_56_0_35 = 0 | all_56_1_36 = 0 | all_56_2_37 = 0 | all_56_3_38 = 0 % 36.58/11.38 | (182) apart_point_and_line(all_1_2_2, all_1_3_3) = all_56_3_38 % 36.58/11.38 | (183) apart_point_and_line(all_1_2_2, all_1_4_4) = all_56_2_37 % 36.58/11.38 | (184) apart_point_and_line(all_17_0_6, all_1_4_4) = all_56_0_35 % 36.58/11.38 | % 36.58/11.38 | Instantiating (150) with all_58_0_39, all_58_1_40, all_58_2_41, all_58_3_42 yields: % 36.58/11.38 | (185) apart_point_and_line(all_19_0_8, all_1_4_4) = all_58_0_39 & apart_point_and_line(all_19_0_8, all_1_5_5) = all_58_1_40 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_58_2_41 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_58_3_42 & (all_58_0_39 = 0 | all_58_1_40 = 0 | all_58_2_41 = 0 | all_58_3_42 = 0) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (185) yields: % 36.58/11.38 | (186) apart_point_and_line(all_19_0_8, all_1_4_4) = all_58_0_39 % 36.58/11.38 | (187) apart_point_and_line(all_1_2_2, all_1_4_4) = all_58_2_41 % 36.58/11.38 | (188) apart_point_and_line(all_1_2_2, all_1_5_5) = all_58_3_42 % 36.58/11.38 | (189) all_58_0_39 = 0 | all_58_1_40 = 0 | all_58_2_41 = 0 | all_58_3_42 = 0 % 36.58/11.38 | (190) apart_point_and_line(all_19_0_8, all_1_5_5) = all_58_1_40 % 36.58/11.38 | % 36.58/11.38 | Instantiating (149) with all_60_0_43, all_60_1_44, all_60_2_45, all_60_3_46 yields: % 36.58/11.38 | (191) apart_point_and_line(all_19_0_8, all_1_3_3) = all_60_0_43 & apart_point_and_line(all_19_0_8, all_1_5_5) = all_60_1_44 & apart_point_and_line(all_1_2_2, all_1_3_3) = all_60_2_45 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_60_3_46 & (all_60_0_43 = 0 | all_60_1_44 = 0 | all_60_2_45 = 0 | all_60_3_46 = 0) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (191) yields: % 36.58/11.38 | (192) apart_point_and_line(all_19_0_8, all_1_3_3) = all_60_0_43 % 36.58/11.38 | (193) apart_point_and_line(all_1_2_2, all_1_5_5) = all_60_3_46 % 36.58/11.38 | (194) apart_point_and_line(all_1_2_2, all_1_3_3) = all_60_2_45 % 36.58/11.38 | (195) apart_point_and_line(all_19_0_8, all_1_5_5) = all_60_1_44 % 36.58/11.38 | (196) all_60_0_43 = 0 | all_60_1_44 = 0 | all_60_2_45 = 0 | all_60_3_46 = 0 % 36.58/11.38 | % 36.58/11.38 | Instantiating (148) with all_62_0_47, all_62_1_48, all_62_2_49, all_62_3_50 yields: % 36.58/11.38 | (197) apart_point_and_line(all_19_0_8, all_1_3_3) = all_62_1_48 & apart_point_and_line(all_19_0_8, all_1_4_4) = all_62_0_47 & apart_point_and_line(all_1_2_2, all_1_3_3) = all_62_3_50 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_62_2_49 & (all_62_0_47 = 0 | all_62_1_48 = 0 | all_62_2_49 = 0 | all_62_3_50 = 0) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (197) yields: % 36.58/11.38 | (198) apart_point_and_line(all_1_2_2, all_1_3_3) = all_62_3_50 % 36.58/11.38 | (199) all_62_0_47 = 0 | all_62_1_48 = 0 | all_62_2_49 = 0 | all_62_3_50 = 0 % 36.58/11.38 | (200) apart_point_and_line(all_1_2_2, all_1_4_4) = all_62_2_49 % 36.58/11.38 | (201) apart_point_and_line(all_19_0_8, all_1_3_3) = all_62_1_48 % 36.58/11.38 | (202) apart_point_and_line(all_19_0_8, all_1_4_4) = all_62_0_47 % 36.58/11.38 | % 36.58/11.38 | Instantiating (146) with all_64_0_51, all_64_1_52, all_64_2_53 yields: % 36.58/11.38 | (203) line_connecting(all_1_2_2, all_17_0_6) = all_64_2_53 & apart_point_and_line(all_1_1_1, all_64_2_53) = all_64_1_52 & distinct_points(all_1_1_1, all_1_2_2) = all_64_0_51 & ( ~ (all_64_1_52 = 0) | (all_64_0_51 = 0 & all_21_0_10 = 0)) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (203) yields: % 36.58/11.38 | (204) line_connecting(all_1_2_2, all_17_0_6) = all_64_2_53 % 36.58/11.38 | (205) apart_point_and_line(all_1_1_1, all_64_2_53) = all_64_1_52 % 36.58/11.38 | (206) distinct_points(all_1_1_1, all_1_2_2) = all_64_0_51 % 36.58/11.38 | (207) ~ (all_64_1_52 = 0) | (all_64_0_51 = 0 & all_21_0_10 = 0) % 36.58/11.38 | % 36.58/11.38 | Instantiating (147) with all_66_0_54, all_66_1_55, all_66_2_56 yields: % 36.58/11.38 | (208) line_connecting(all_1_2_2, all_1_1_1) = all_66_2_56 & apart_point_and_line(all_1_1_1, all_66_2_56) = all_66_1_55 & distinct_points(all_1_1_1, all_1_2_2) = all_66_0_54 & ( ~ (all_66_1_55 = 0) | (all_66_0_54 = 0 & all_35_3_22 = 0)) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (208) yields: % 36.58/11.38 | (209) line_connecting(all_1_2_2, all_1_1_1) = all_66_2_56 % 36.58/11.38 | (210) apart_point_and_line(all_1_1_1, all_66_2_56) = all_66_1_55 % 36.58/11.38 | (211) distinct_points(all_1_1_1, all_1_2_2) = all_66_0_54 % 36.58/11.38 | (212) ~ (all_66_1_55 = 0) | (all_66_0_54 = 0 & all_35_3_22 = 0) % 36.58/11.38 | % 36.58/11.38 | Instantiating (151) with all_68_0_57, all_68_1_58, all_68_2_59 yields: % 36.58/11.38 | (213) line_connecting(all_1_2_2, all_17_0_6) = all_68_2_59 & apart_point_and_line(all_1_2_2, all_68_2_59) = all_68_1_58 & distinct_points(all_1_2_2, all_1_2_2) = all_68_0_57 & ( ~ (all_68_1_58 = 0) | all_68_0_57 = 0) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (213) yields: % 36.58/11.38 | (214) line_connecting(all_1_2_2, all_17_0_6) = all_68_2_59 % 36.58/11.38 | (215) apart_point_and_line(all_1_2_2, all_68_2_59) = all_68_1_58 % 36.58/11.38 | (216) distinct_points(all_1_2_2, all_1_2_2) = all_68_0_57 % 36.58/11.38 | (217) ~ (all_68_1_58 = 0) | all_68_0_57 = 0 % 36.58/11.38 | % 36.58/11.38 | Instantiating (145) with all_70_0_60, all_70_1_61, all_70_2_62 yields: % 36.58/11.38 | (218) line_connecting(all_1_2_2, all_19_0_8) = all_70_2_62 & apart_point_and_line(all_1_1_1, all_70_2_62) = all_70_1_61 & distinct_points(all_1_1_1, all_1_2_2) = all_70_0_60 & ( ~ (all_70_1_61 = 0) | (all_70_0_60 = 0 & all_23_0_13 = 0)) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (218) yields: % 36.58/11.38 | (219) line_connecting(all_1_2_2, all_19_0_8) = all_70_2_62 % 36.58/11.38 | (220) apart_point_and_line(all_1_1_1, all_70_2_62) = all_70_1_61 % 36.58/11.38 | (221) distinct_points(all_1_1_1, all_1_2_2) = all_70_0_60 % 36.58/11.38 | (222) ~ (all_70_1_61 = 0) | (all_70_0_60 = 0 & all_23_0_13 = 0) % 36.58/11.38 | % 36.58/11.38 | Instantiating (142) with all_72_0_63, all_72_1_64, all_72_2_65 yields: % 36.58/11.38 | (223) line_connecting(all_1_2_2, all_19_0_8) = all_72_2_65 & apart_point_and_line(all_1_2_2, all_72_2_65) = all_72_1_64 & distinct_points(all_1_2_2, all_1_2_2) = all_72_0_63 & ( ~ (all_72_1_64 = 0) | all_72_0_63 = 0) % 36.58/11.38 | % 36.58/11.38 | Applying alpha-rule on (223) yields: % 36.58/11.38 | (224) line_connecting(all_1_2_2, all_19_0_8) = all_72_2_65 % 36.58/11.38 | (225) apart_point_and_line(all_1_2_2, all_72_2_65) = all_72_1_64 % 36.58/11.38 | (226) distinct_points(all_1_2_2, all_1_2_2) = all_72_0_63 % 36.58/11.39 | (227) ~ (all_72_1_64 = 0) | all_72_0_63 = 0 % 36.58/11.39 | % 36.58/11.39 | Instantiating (157) with all_74_0_66, all_74_1_67, all_74_2_68 yields: % 36.58/11.39 | (228) line_connecting(all_1_2_2, all_1_1_1) = all_74_2_68 & apart_point_and_line(all_1_2_2, all_74_2_68) = all_74_1_67 & distinct_points(all_1_2_2, all_1_2_2) = all_74_0_66 & ( ~ (all_74_1_67 = 0) | all_74_0_66 = 0) % 36.58/11.39 | % 36.58/11.39 | Applying alpha-rule on (228) yields: % 36.58/11.39 | (229) line_connecting(all_1_2_2, all_1_1_1) = all_74_2_68 % 36.58/11.39 | (230) apart_point_and_line(all_1_2_2, all_74_2_68) = all_74_1_67 % 36.58/11.39 | (231) distinct_points(all_1_2_2, all_1_2_2) = all_74_0_66 % 36.58/11.39 | (232) ~ (all_74_1_67 = 0) | all_74_0_66 = 0 % 36.58/11.39 | % 36.58/11.39 | Instantiating (138) with all_76_0_69, all_76_1_70, all_76_2_71 yields: % 36.58/11.39 | (233) intersection_point(all_1_5_5, all_1_4_4) = all_76_1_70 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_76_2_71 & distinct_points(all_1_2_2, all_76_1_70) = all_76_0_69 & (all_76_0_69 = 0 | ( ~ (all_76_2_71 = 0) & ~ (all_19_1_9 = 0))) % 36.58/11.39 | % 36.58/11.39 | Applying alpha-rule on (233) yields: % 36.58/11.39 | (234) intersection_point(all_1_5_5, all_1_4_4) = all_76_1_70 % 36.58/11.39 | (235) apart_point_and_line(all_1_2_2, all_1_4_4) = all_76_2_71 % 36.58/11.39 | (236) distinct_points(all_1_2_2, all_76_1_70) = all_76_0_69 % 36.58/11.39 | (237) all_76_0_69 = 0 | ( ~ (all_76_2_71 = 0) & ~ (all_19_1_9 = 0)) % 36.58/11.39 | % 36.58/11.39 | Instantiating (137) with all_78_0_72, all_78_1_73, all_78_2_74 yields: % 36.58/11.39 | (238) apart_point_and_line(all_1_2_2, all_1_4_4) = all_78_1_73 & convergent_lines(all_1_5_5, all_1_4_4) = all_78_2_74 & distinct_points(all_1_2_2, all_1_2_2) = all_78_0_72 & ( ~ (all_78_2_74 = 0) | all_78_0_72 = 0 | ( ~ (all_78_1_73 = 0) & ~ (all_19_1_9 = 0))) % 36.58/11.39 | % 36.58/11.39 | Applying alpha-rule on (238) yields: % 36.58/11.39 | (239) apart_point_and_line(all_1_2_2, all_1_4_4) = all_78_1_73 % 36.58/11.39 | (240) convergent_lines(all_1_5_5, all_1_4_4) = all_78_2_74 % 36.58/11.39 | (241) distinct_points(all_1_2_2, all_1_2_2) = all_78_0_72 % 36.58/11.39 | (242) ~ (all_78_2_74 = 0) | all_78_0_72 = 0 | ( ~ (all_78_1_73 = 0) & ~ (all_19_1_9 = 0)) % 36.58/11.39 | % 36.58/11.39 | Instantiating (136) with all_80_0_75, all_80_1_76, all_80_2_77 yields: % 36.58/11.39 | (243) apart_point_and_line(all_1_2_2, all_1_4_4) = all_80_1_76 & convergent_lines(all_1_4_4, all_1_5_5) = all_80_2_77 & distinct_points(all_1_2_2, all_1_1_1) = all_80_0_75 & ( ~ (all_80_2_77 = 0) | all_80_0_75 = 0 | ( ~ (all_80_1_76 = 0) & ~ (all_19_1_9 = 0))) % 36.58/11.39 | % 36.58/11.39 | Applying alpha-rule on (243) yields: % 36.58/11.39 | (244) apart_point_and_line(all_1_2_2, all_1_4_4) = all_80_1_76 % 36.58/11.39 | (245) convergent_lines(all_1_4_4, all_1_5_5) = all_80_2_77 % 36.58/11.39 | (246) distinct_points(all_1_2_2, all_1_1_1) = all_80_0_75 % 36.58/11.39 | (247) ~ (all_80_2_77 = 0) | all_80_0_75 = 0 | ( ~ (all_80_1_76 = 0) & ~ (all_19_1_9 = 0)) % 36.58/11.39 | % 36.58/11.39 | Instantiating (133) with all_82_0_78, all_82_1_79, all_82_2_80 yields: % 36.58/11.39 | (248) intersection_point(all_1_3_3, all_1_5_5) = all_82_1_79 & convergent_lines(all_1_3_3, all_1_5_5) = all_82_2_80 & distinct_points(all_1_2_2, all_82_1_79) = all_82_0_78 & ( ~ (all_82_2_80 = 0) | all_82_0_78 = 0) % 36.58/11.39 | % 36.58/11.39 | Applying alpha-rule on (248) yields: % 36.58/11.39 | (249) intersection_point(all_1_3_3, all_1_5_5) = all_82_1_79 % 36.58/11.39 | (250) convergent_lines(all_1_3_3, all_1_5_5) = all_82_2_80 % 36.58/11.39 | (251) distinct_points(all_1_2_2, all_82_1_79) = all_82_0_78 % 36.58/11.39 | (252) ~ (all_82_2_80 = 0) | all_82_0_78 = 0 % 36.58/11.39 | % 36.58/11.39 | Instantiating (130) with all_86_0_84, all_86_1_85, all_86_2_86 yields: % 36.58/11.39 | (253) intersection_point(all_1_5_5, all_1_4_4) = all_86_1_85 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_86_2_86 & distinct_points(all_1_2_2, all_86_1_85) = all_86_0_84 & (all_86_0_84 = 0 | ( ~ (all_86_2_86 = 0) & ~ (all_17_1_7 = 0))) % 36.58/11.39 | % 36.58/11.39 | Applying alpha-rule on (253) yields: % 36.58/11.39 | (254) intersection_point(all_1_5_5, all_1_4_4) = all_86_1_85 % 36.58/11.39 | (255) apart_point_and_line(all_1_2_2, all_1_5_5) = all_86_2_86 % 36.58/11.39 | (256) distinct_points(all_1_2_2, all_86_1_85) = all_86_0_84 % 36.58/11.39 | (257) all_86_0_84 = 0 | ( ~ (all_86_2_86 = 0) & ~ (all_17_1_7 = 0)) % 36.58/11.39 | % 36.58/11.39 | Instantiating (129) with all_88_0_87, all_88_1_88, all_88_2_89 yields: % 36.58/11.39 | (258) apart_point_and_line(all_1_2_2, all_1_5_5) = all_88_1_88 & convergent_lines(all_1_5_5, all_1_4_4) = all_88_2_89 & distinct_points(all_1_2_2, all_1_2_2) = all_88_0_87 & ( ~ (all_88_2_89 = 0) | all_88_0_87 = 0 | ( ~ (all_88_1_88 = 0) & ~ (all_17_1_7 = 0))) % 36.58/11.39 | % 36.58/11.39 | Applying alpha-rule on (258) yields: % 36.58/11.39 | (259) apart_point_and_line(all_1_2_2, all_1_5_5) = all_88_1_88 % 36.58/11.39 | (260) convergent_lines(all_1_5_5, all_1_4_4) = all_88_2_89 % 36.68/11.39 | (261) distinct_points(all_1_2_2, all_1_2_2) = all_88_0_87 % 36.68/11.39 | (262) ~ (all_88_2_89 = 0) | all_88_0_87 = 0 | ( ~ (all_88_1_88 = 0) & ~ (all_17_1_7 = 0)) % 36.68/11.39 | % 36.68/11.39 | Instantiating (128) with all_90_0_90, all_90_1_91, all_90_2_92 yields: % 36.68/11.39 | (263) apart_point_and_line(all_1_2_2, all_1_5_5) = all_90_1_91 & convergent_lines(all_1_4_4, all_1_5_5) = all_90_2_92 & distinct_points(all_1_2_2, all_1_1_1) = all_90_0_90 & ( ~ (all_90_2_92 = 0) | all_90_0_90 = 0 | ( ~ (all_90_1_91 = 0) & ~ (all_17_1_7 = 0))) % 36.68/11.39 | % 36.68/11.39 | Applying alpha-rule on (263) yields: % 36.68/11.39 | (264) apart_point_and_line(all_1_2_2, all_1_5_5) = all_90_1_91 % 36.68/11.39 | (265) convergent_lines(all_1_4_4, all_1_5_5) = all_90_2_92 % 36.68/11.39 | (266) distinct_points(all_1_2_2, all_1_1_1) = all_90_0_90 % 36.68/11.39 | (267) ~ (all_90_2_92 = 0) | all_90_0_90 = 0 | ( ~ (all_90_1_91 = 0) & ~ (all_17_1_7 = 0)) % 36.68/11.39 | % 36.68/11.39 | Instantiating (126) with all_92_0_93, all_92_1_94, all_92_2_95 yields: % 36.68/11.39 | (268) intersection_point(all_1_5_5, all_1_4_4) = all_92_1_94 & apart_point_and_line(all_1_1_1, all_1_4_4) = all_92_2_95 & distinct_points(all_1_1_1, all_92_1_94) = all_92_0_93 & (all_92_0_93 = 0 | ( ~ (all_92_2_95 = 0) & ~ (all_23_2_15 = 0))) % 36.68/11.39 | % 36.68/11.39 | Applying alpha-rule on (268) yields: % 36.68/11.39 | (269) intersection_point(all_1_5_5, all_1_4_4) = all_92_1_94 % 36.68/11.40 | (270) apart_point_and_line(all_1_1_1, all_1_4_4) = all_92_2_95 % 36.68/11.40 | (271) distinct_points(all_1_1_1, all_92_1_94) = all_92_0_93 % 36.68/11.40 | (272) all_92_0_93 = 0 | ( ~ (all_92_2_95 = 0) & ~ (all_23_2_15 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (123) with all_94_0_96, all_94_1_97, all_94_2_98 yields: % 36.68/11.40 | (273) apart_point_and_line(all_1_1_1, all_1_4_4) = all_94_1_97 & convergent_lines(all_1_5_5, all_1_4_4) = all_94_2_98 & distinct_points(all_1_1_1, all_1_2_2) = all_94_0_96 & ( ~ (all_94_2_98 = 0) | all_94_0_96 = 0 | ( ~ (all_94_1_97 = 0) & ~ (all_23_2_15 = 0))) % 36.68/11.40 | % 36.68/11.40 | Applying alpha-rule on (273) yields: % 36.68/11.40 | (274) apart_point_and_line(all_1_1_1, all_1_4_4) = all_94_1_97 % 36.68/11.40 | (275) convergent_lines(all_1_5_5, all_1_4_4) = all_94_2_98 % 36.68/11.40 | (276) distinct_points(all_1_1_1, all_1_2_2) = all_94_0_96 % 36.68/11.40 | (277) ~ (all_94_2_98 = 0) | all_94_0_96 = 0 | ( ~ (all_94_1_97 = 0) & ~ (all_23_2_15 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (122) with all_96_0_99, all_96_1_100, all_96_2_101 yields: % 36.68/11.40 | (278) apart_point_and_line(all_1_1_1, all_1_4_4) = all_96_1_100 & convergent_lines(all_1_4_4, all_1_5_5) = all_96_2_101 & distinct_points(all_1_1_1, all_1_1_1) = all_96_0_99 & ( ~ (all_96_2_101 = 0) | all_96_0_99 = 0 | ( ~ (all_96_1_100 = 0) & ~ (all_23_2_15 = 0))) % 36.68/11.40 | % 36.68/11.40 | Applying alpha-rule on (278) yields: % 36.68/11.40 | (279) apart_point_and_line(all_1_1_1, all_1_4_4) = all_96_1_100 % 36.68/11.40 | (280) convergent_lines(all_1_4_4, all_1_5_5) = all_96_2_101 % 36.68/11.40 | (281) distinct_points(all_1_1_1, all_1_1_1) = all_96_0_99 % 36.68/11.40 | (282) ~ (all_96_2_101 = 0) | all_96_0_99 = 0 | ( ~ (all_96_1_100 = 0) & ~ (all_23_2_15 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (125) with all_98_0_102, all_98_1_103, all_98_2_104 yields: % 36.68/11.40 | (283) intersection_point(all_1_5_5, all_1_3_3) = all_98_1_103 & apart_point_and_line(all_1_1_1, all_1_3_3) = all_98_2_104 & distinct_points(all_1_1_1, all_98_1_103) = all_98_0_102 & (all_98_0_102 = 0 | ( ~ (all_98_2_104 = 0) & ~ (all_23_2_15 = 0))) % 36.68/11.40 | % 36.68/11.40 | Applying alpha-rule on (283) yields: % 36.68/11.40 | (284) intersection_point(all_1_5_5, all_1_3_3) = all_98_1_103 % 36.68/11.40 | (285) apart_point_and_line(all_1_1_1, all_1_3_3) = all_98_2_104 % 36.68/11.40 | (286) distinct_points(all_1_1_1, all_98_1_103) = all_98_0_102 % 36.68/11.40 | (287) all_98_0_102 = 0 | ( ~ (all_98_2_104 = 0) & ~ (all_23_2_15 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (121) with all_100_0_105, all_100_1_106, all_100_2_107 yields: % 36.68/11.40 | (288) intersection_point(all_1_5_5, all_1_4_4) = all_100_1_106 & apart_point_and_line(all_1_1_1, all_1_5_5) = all_100_2_107 & distinct_points(all_1_1_1, all_100_1_106) = all_100_0_105 & (all_100_0_105 = 0 | ( ~ (all_100_2_107 = 0) & ~ (all_21_2_12 = 0))) % 36.68/11.40 | % 36.68/11.40 | Applying alpha-rule on (288) yields: % 36.68/11.40 | (289) intersection_point(all_1_5_5, all_1_4_4) = all_100_1_106 % 36.68/11.40 | (290) apart_point_and_line(all_1_1_1, all_1_5_5) = all_100_2_107 % 36.68/11.40 | (291) distinct_points(all_1_1_1, all_100_1_106) = all_100_0_105 % 36.68/11.40 | (292) all_100_0_105 = 0 | ( ~ (all_100_2_107 = 0) & ~ (all_21_2_12 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (124) with all_102_0_108, all_102_1_109, all_102_2_110 yields: % 36.68/11.40 | (293) apart_point_and_line(all_1_1_1, all_1_3_3) = all_102_1_109 & convergent_lines(all_1_5_5, all_1_3_3) = all_102_2_110 & distinct_points(all_1_1_1, all_19_0_8) = all_102_0_108 & ( ~ (all_102_2_110 = 0) | all_102_0_108 = 0 | ( ~ (all_102_1_109 = 0) & ~ (all_23_2_15 = 0))) % 36.68/11.40 | % 36.68/11.40 | Applying alpha-rule on (293) yields: % 36.68/11.40 | (294) apart_point_and_line(all_1_1_1, all_1_3_3) = all_102_1_109 % 36.68/11.40 | (295) convergent_lines(all_1_5_5, all_1_3_3) = all_102_2_110 % 36.68/11.40 | (296) distinct_points(all_1_1_1, all_19_0_8) = all_102_0_108 % 36.68/11.40 | (297) ~ (all_102_2_110 = 0) | all_102_0_108 = 0 | ( ~ (all_102_1_109 = 0) & ~ (all_23_2_15 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (120) with all_104_0_111, all_104_1_112, all_104_2_113 yields: % 36.68/11.40 | (298) intersection_point(all_1_3_3, all_1_4_4) = all_104_1_112 & apart_point_and_line(all_1_1_1, all_1_3_3) = all_104_2_113 & distinct_points(all_1_1_1, all_104_1_112) = all_104_0_111 & (all_104_0_111 = 0 | ( ~ (all_104_2_113 = 0) & ~ (all_21_2_12 = 0))) % 36.68/11.40 | % 36.68/11.40 | Applying alpha-rule on (298) yields: % 36.68/11.40 | (299) intersection_point(all_1_3_3, all_1_4_4) = all_104_1_112 % 36.68/11.40 | (300) apart_point_and_line(all_1_1_1, all_1_3_3) = all_104_2_113 % 36.68/11.40 | (301) distinct_points(all_1_1_1, all_104_1_112) = all_104_0_111 % 36.68/11.40 | (302) all_104_0_111 = 0 | ( ~ (all_104_2_113 = 0) & ~ (all_21_2_12 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (118) with all_106_0_114, all_106_1_115, all_106_2_116 yields: % 36.68/11.40 | (303) apart_point_and_line(all_1_1_1, all_1_5_5) = all_106_1_115 & convergent_lines(all_1_5_5, all_1_4_4) = all_106_2_116 & distinct_points(all_1_1_1, all_1_2_2) = all_106_0_114 & ( ~ (all_106_2_116 = 0) | all_106_0_114 = 0 | ( ~ (all_106_1_115 = 0) & ~ (all_21_2_12 = 0))) % 36.68/11.40 | % 36.68/11.40 | Applying alpha-rule on (303) yields: % 36.68/11.40 | (304) apart_point_and_line(all_1_1_1, all_1_5_5) = all_106_1_115 % 36.68/11.40 | (305) convergent_lines(all_1_5_5, all_1_4_4) = all_106_2_116 % 36.68/11.40 | (306) distinct_points(all_1_1_1, all_1_2_2) = all_106_0_114 % 36.68/11.40 | (307) ~ (all_106_2_116 = 0) | all_106_0_114 = 0 | ( ~ (all_106_1_115 = 0) & ~ (all_21_2_12 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (117) with all_108_0_117, all_108_1_118, all_108_2_119 yields: % 36.68/11.40 | (308) apart_point_and_line(all_1_1_1, all_1_5_5) = all_108_1_118 & convergent_lines(all_1_4_4, all_1_5_5) = all_108_2_119 & distinct_points(all_1_1_1, all_1_1_1) = all_108_0_117 & ( ~ (all_108_2_119 = 0) | all_108_0_117 = 0 | ( ~ (all_108_1_118 = 0) & ~ (all_21_2_12 = 0))) % 36.68/11.40 | % 36.68/11.40 | Applying alpha-rule on (308) yields: % 36.68/11.40 | (309) apart_point_and_line(all_1_1_1, all_1_5_5) = all_108_1_118 % 36.68/11.40 | (310) convergent_lines(all_1_4_4, all_1_5_5) = all_108_2_119 % 36.68/11.40 | (311) distinct_points(all_1_1_1, all_1_1_1) = all_108_0_117 % 36.68/11.40 | (312) ~ (all_108_2_119 = 0) | all_108_0_117 = 0 | ( ~ (all_108_1_118 = 0) & ~ (all_21_2_12 = 0)) % 36.68/11.40 | % 36.68/11.40 | Instantiating (116) with all_110_0_120, all_110_1_121, all_110_2_122 yields: % 36.68/11.41 | (313) apart_point_and_line(all_1_1_1, all_1_5_5) = all_110_1_121 & convergent_lines(all_1_5_5, all_1_3_3) = all_110_2_122 & distinct_points(all_1_1_1, all_19_0_8) = all_110_0_120 & ( ~ (all_110_2_122 = 0) | all_110_0_120 = 0 | ( ~ (all_110_1_121 = 0) & ~ (all_1_0_0 = 0))) % 36.68/11.41 | % 36.68/11.41 | Applying alpha-rule on (313) yields: % 36.68/11.41 | (314) apart_point_and_line(all_1_1_1, all_1_5_5) = all_110_1_121 % 36.68/11.41 | (315) convergent_lines(all_1_5_5, all_1_3_3) = all_110_2_122 % 36.68/11.41 | (316) distinct_points(all_1_1_1, all_19_0_8) = all_110_0_120 % 36.68/11.41 | (317) ~ (all_110_2_122 = 0) | all_110_0_120 = 0 | ( ~ (all_110_1_121 = 0) & ~ (all_1_0_0 = 0)) % 36.68/11.41 | % 36.68/11.41 | Instantiating (119) with all_112_0_123, all_112_1_124, all_112_2_125 yields: % 36.68/11.41 | (318) apart_point_and_line(all_1_1_1, all_1_3_3) = all_112_1_124 & convergent_lines(all_1_3_3, all_1_4_4) = all_112_2_125 & distinct_points(all_1_1_1, all_17_0_6) = all_112_0_123 & ( ~ (all_112_2_125 = 0) | all_112_0_123 = 0 | ( ~ (all_112_1_124 = 0) & ~ (all_21_2_12 = 0))) % 36.68/11.41 | % 36.68/11.41 | Applying alpha-rule on (318) yields: % 36.68/11.41 | (319) apart_point_and_line(all_1_1_1, all_1_3_3) = all_112_1_124 % 36.68/11.41 | (320) convergent_lines(all_1_3_3, all_1_4_4) = all_112_2_125 % 36.68/11.41 | (321) distinct_points(all_1_1_1, all_17_0_6) = all_112_0_123 % 36.68/11.41 | (322) ~ (all_112_2_125 = 0) | all_112_0_123 = 0 | ( ~ (all_112_1_124 = 0) & ~ (all_21_2_12 = 0)) % 36.68/11.41 | % 36.68/11.41 | Instantiating (115) with all_114_0_126, all_114_1_127, all_114_2_128 yields: % 36.68/11.41 | (323) apart_point_and_line(all_1_1_1, all_1_4_4) = all_114_1_127 & convergent_lines(all_1_3_3, all_1_4_4) = all_114_2_128 & distinct_points(all_1_1_1, all_17_0_6) = all_114_0_126 & ( ~ (all_114_2_128 = 0) | all_114_0_126 = 0 | ( ~ (all_114_1_127 = 0) & ~ (all_1_0_0 = 0))) % 36.68/11.41 | % 36.68/11.41 | Applying alpha-rule on (323) yields: % 36.68/11.41 | (324) apart_point_and_line(all_1_1_1, all_1_4_4) = all_114_1_127 % 36.68/11.41 | (325) convergent_lines(all_1_3_3, all_1_4_4) = all_114_2_128 % 36.68/11.41 | (326) distinct_points(all_1_1_1, all_17_0_6) = all_114_0_126 % 36.68/11.41 | (327) ~ (all_114_2_128 = 0) | all_114_0_126 = 0 | ( ~ (all_114_1_127 = 0) & ~ (all_1_0_0 = 0)) % 36.68/11.41 | % 36.68/11.41 | Instantiating (114) with all_116_0_129, all_116_1_130, all_116_2_131 yields: % 36.68/11.41 | (328) apart_point_and_line(all_1_1_1, all_1_3_3) = all_116_1_130 & convergent_lines(all_1_3_3, all_1_3_3) = all_116_2_131 & distinct_points(all_1_1_1, all_25_1_17) = all_116_0_129 & ( ~ (all_116_2_131 = 0) | all_116_0_129 = 0 | ( ~ (all_116_1_130 = 0) & ~ (all_1_0_0 = 0))) % 36.68/11.41 | % 36.68/11.41 | Applying alpha-rule on (328) yields: % 36.68/11.41 | (329) apart_point_and_line(all_1_1_1, all_1_3_3) = all_116_1_130 % 36.68/11.41 | (330) convergent_lines(all_1_3_3, all_1_3_3) = all_116_2_131 % 36.68/11.41 | (331) distinct_points(all_1_1_1, all_25_1_17) = all_116_0_129 % 36.68/11.41 | (332) ~ (all_116_2_131 = 0) | all_116_0_129 = 0 | ( ~ (all_116_1_130 = 0) & ~ (all_1_0_0 = 0)) % 36.68/11.41 | % 36.68/11.41 +-Applying beta-rule and splitting (141), into two cases. % 36.68/11.41 |-Branch one: % 36.68/11.41 | (333) all_35_3_22 = 0 % 36.68/11.41 | % 36.68/11.41 | Equations (333) can reduce 113 to: % 36.68/11.41 | (92) $false % 36.68/11.41 | % 36.68/11.41 |-The branch is then unsatisfiable % 36.68/11.41 |-Branch two: % 36.68/11.41 | (113) ~ (all_35_3_22 = 0) % 36.68/11.41 | (336) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_1_1, all_1_1_1) = v1 & apart_point_and_line(all_1_1_1, v1) = v2 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 36.68/11.41 | % 36.68/11.41 | Instantiating (336) with all_137_0_135, all_137_1_136, all_137_2_137 yields: % 36.68/11.41 | (337) line_connecting(all_1_1_1, all_1_1_1) = all_137_1_136 & apart_point_and_line(all_1_1_1, all_137_1_136) = all_137_0_135 & distinct_points(all_1_1_1, all_1_1_1) = all_137_2_137 & ( ~ (all_137_0_135 = 0) | ~ (all_137_2_137 = 0)) % 36.68/11.41 | % 36.68/11.41 | Applying alpha-rule on (337) yields: % 36.68/11.41 | (338) line_connecting(all_1_1_1, all_1_1_1) = all_137_1_136 % 36.68/11.41 | (339) apart_point_and_line(all_1_1_1, all_137_1_136) = all_137_0_135 % 36.68/11.41 | (340) distinct_points(all_1_1_1, all_1_1_1) = all_137_2_137 % 36.68/11.41 | (341) ~ (all_137_0_135 = 0) | ~ (all_137_2_137 = 0) % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (9) with all_1_5_5, all_1_4_4, all_92_1_94, all_1_2_2 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_92_1_94, intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2, yields: % 36.68/11.41 | (342) all_92_1_94 = all_1_2_2 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (9) with all_1_5_5, all_1_4_4, all_92_1_94, all_100_1_106 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_100_1_106, intersection_point(all_1_5_5, all_1_4_4) = all_92_1_94, yields: % 36.68/11.41 | (343) all_100_1_106 = all_92_1_94 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (9) with all_1_5_5, all_1_4_4, all_86_1_85, all_92_1_94 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_92_1_94, intersection_point(all_1_5_5, all_1_4_4) = all_86_1_85, yields: % 36.68/11.41 | (344) all_92_1_94 = all_86_1_85 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (9) with all_1_5_5, all_1_4_4, all_76_1_70, all_100_1_106 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_100_1_106, intersection_point(all_1_5_5, all_1_4_4) = all_76_1_70, yields: % 36.68/11.41 | (345) all_100_1_106 = all_76_1_70 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (21) with all_1_2_2, all_19_0_8, all_70_2_62, all_72_2_65 and discharging atoms line_connecting(all_1_2_2, all_19_0_8) = all_72_2_65, line_connecting(all_1_2_2, all_19_0_8) = all_70_2_62, yields: % 36.68/11.41 | (346) all_72_2_65 = all_70_2_62 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (21) with all_1_2_2, all_17_0_6, all_64_2_53, all_68_2_59 and discharging atoms line_connecting(all_1_2_2, all_17_0_6) = all_68_2_59, line_connecting(all_1_2_2, all_17_0_6) = all_64_2_53, yields: % 36.68/11.41 | (347) all_68_2_59 = all_64_2_53 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (21) with all_1_2_2, all_1_1_1, all_66_2_56, all_74_2_68 and discharging atoms line_connecting(all_1_2_2, all_1_1_1) = all_74_2_68, line_connecting(all_1_2_2, all_1_1_1) = all_66_2_56, yields: % 36.68/11.41 | (348) all_74_2_68 = all_66_2_56 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (22) with all_1_1_1, all_1_3_3, all_112_1_124, all_116_1_130 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_116_1_130, apart_point_and_line(all_1_1_1, all_1_3_3) = all_112_1_124, yields: % 36.68/11.41 | (349) all_116_1_130 = all_112_1_124 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (22) with all_1_1_1, all_1_3_3, all_104_2_113, all_1_0_0 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_104_2_113, apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 36.68/11.41 | (350) all_104_2_113 = all_1_0_0 % 36.68/11.41 | % 36.68/11.41 | Instantiating formula (22) with all_1_1_1, all_1_3_3, all_104_2_113, all_112_1_124 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_112_1_124, apart_point_and_line(all_1_1_1, all_1_3_3) = all_104_2_113, yields: % 36.68/11.42 | (351) all_112_1_124 = all_104_2_113 % 36.68/11.42 | % 36.68/11.42 | Instantiating formula (22) with all_1_1_1, all_1_3_3, all_102_1_109, all_104_2_113 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_104_2_113, apart_point_and_line(all_1_1_1, all_1_3_3) = all_102_1_109, yields: % 36.68/11.42 | (352) all_104_2_113 = all_102_1_109 % 36.68/11.42 | % 36.68/11.42 | Instantiating formula (22) with all_1_1_1, all_1_3_3, all_98_2_104, all_116_1_130 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_116_1_130, apart_point_and_line(all_1_1_1, all_1_3_3) = all_98_2_104, yields: % 36.68/11.42 | (353) all_116_1_130 = all_98_2_104 % 36.68/11.42 | % 36.68/11.42 | Instantiating formula (22) with all_1_1_1, all_1_4_4, all_114_1_127, all_21_2_12 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_114_1_127, apart_point_and_line(all_1_1_1, all_1_4_4) = all_21_2_12, yields: % 36.68/11.42 | (354) all_114_1_127 = all_21_2_12 % 36.68/11.42 | % 36.68/11.42 | Instantiating formula (22) with all_1_1_1, all_1_4_4, all_96_1_100, all_114_1_127 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_114_1_127, apart_point_and_line(all_1_1_1, all_1_4_4) = all_96_1_100, yields: % 36.68/11.42 | (355) all_114_1_127 = all_96_1_100 % 36.68/11.42 | % 36.68/11.42 | Instantiating formula (22) with all_1_1_1, all_1_4_4, all_94_1_97, all_114_1_127 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_114_1_127, apart_point_and_line(all_1_1_1, all_1_4_4) = all_94_1_97, yields: % 36.68/11.42 | (356) all_114_1_127 = all_94_1_97 % 36.68/11.42 | % 36.68/11.42 | Instantiating formula (22) with all_1_1_1, all_1_4_4, all_92_2_95, all_96_1_100 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_96_1_100, apart_point_and_line(all_1_1_1, all_1_4_4) = all_92_2_95, yields: % 36.68/11.42 | (357) all_96_1_100 = all_92_2_95 % 36.68/11.42 | % 36.68/11.42 | Instantiating formula (22) with all_1_1_1, all_1_4_4, all_50_0_23, all_114_1_127 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_114_1_127, apart_point_and_line(all_1_1_1, all_1_4_4) = all_50_0_23, yields: % 36.68/11.42 | (358) all_114_1_127 = all_50_0_23 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_1_1, all_1_5_5, all_110_1_121, all_23_2_15 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_110_1_121, apart_point_and_line(all_1_1_1, all_1_5_5) = all_23_2_15, yields: % 36.80/11.42 | (359) all_110_1_121 = all_23_2_15 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_1_1, all_1_5_5, all_108_1_118, all_110_1_121 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_110_1_121, apart_point_and_line(all_1_1_1, all_1_5_5) = all_108_1_118, yields: % 36.80/11.42 | (360) all_110_1_121 = all_108_1_118 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_1_1, all_1_5_5, all_106_1_115, all_110_1_121 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_110_1_121, apart_point_and_line(all_1_1_1, all_1_5_5) = all_106_1_115, yields: % 36.80/11.42 | (361) all_110_1_121 = all_106_1_115 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_1_1, all_1_5_5, all_100_2_107, all_110_1_121 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_110_1_121, apart_point_and_line(all_1_1_1, all_1_5_5) = all_100_2_107, yields: % 36.80/11.42 | (362) all_110_1_121 = all_100_2_107 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_1_1, all_1_5_5, all_50_1_24, all_100_2_107 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_100_2_107, apart_point_and_line(all_1_1_1, all_1_5_5) = all_50_1_24, yields: % 36.80/11.42 | (363) all_100_2_107 = all_50_1_24 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_78_1_73, all_80_1_76 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_80_1_76, apart_point_and_line(all_1_2_2, all_1_4_4) = all_78_1_73, yields: % 36.80/11.42 | (364) all_80_1_76 = all_78_1_73 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_76_2_71, all_17_1_7 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_76_2_71, apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, yields: % 36.80/11.42 | (365) all_76_2_71 = all_17_1_7 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_76_2_71, all_80_1_76 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_80_1_76, apart_point_and_line(all_1_2_2, all_1_4_4) = all_76_2_71, yields: % 36.80/11.42 | (366) all_80_1_76 = all_76_2_71 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_62_2_49, all_80_1_76 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_80_1_76, apart_point_and_line(all_1_2_2, all_1_4_4) = all_62_2_49, yields: % 36.80/11.42 | (367) all_80_1_76 = all_62_2_49 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_56_2_37, all_58_2_41 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_58_2_41, apart_point_and_line(all_1_2_2, all_1_4_4) = all_56_2_37, yields: % 36.80/11.42 | (368) all_58_2_41 = all_56_2_37 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_52_2_29, all_80_1_76 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_80_1_76, apart_point_and_line(all_1_2_2, all_1_4_4) = all_52_2_29, yields: % 36.80/11.42 | (369) all_80_1_76 = all_52_2_29 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_52_2_29, all_58_2_41 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_58_2_41, apart_point_and_line(all_1_2_2, all_1_4_4) = all_52_2_29, yields: % 36.80/11.42 | (370) all_58_2_41 = all_52_2_29 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_50_2_25, all_58_2_41 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_58_2_41, apart_point_and_line(all_1_2_2, all_1_4_4) = all_50_2_25, yields: % 36.80/11.42 | (371) all_58_2_41 = all_50_2_25 % 36.80/11.42 | % 36.80/11.42 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_86_2_86, all_90_1_91 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_90_1_91, apart_point_and_line(all_1_2_2, all_1_5_5) = all_86_2_86, yields: % 36.81/11.42 | (372) all_90_1_91 = all_86_2_86 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_60_3_46, all_86_2_86 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_86_2_86, apart_point_and_line(all_1_2_2, all_1_5_5) = all_60_3_46, yields: % 36.81/11.42 | (373) all_86_2_86 = all_60_3_46 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_58_3_42, all_19_1_9 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_58_3_42, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.81/11.42 | (374) all_58_3_42 = all_19_1_9 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_58_3_42, all_88_1_88 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_88_1_88, apart_point_and_line(all_1_2_2, all_1_5_5) = all_58_3_42, yields: % 36.81/11.42 | (375) all_88_1_88 = all_58_3_42 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_58_3_42, all_60_3_46 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_60_3_46, apart_point_and_line(all_1_2_2, all_1_5_5) = all_58_3_42, yields: % 36.81/11.42 | (376) all_60_3_46 = all_58_3_42 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_54_3_34, all_90_1_91 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_90_1_91, apart_point_and_line(all_1_2_2, all_1_5_5) = all_54_3_34, yields: % 36.81/11.42 | (377) all_90_1_91 = all_54_3_34 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_52_3_30, all_88_1_88 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_88_1_88, apart_point_and_line(all_1_2_2, all_1_5_5) = all_52_3_30, yields: % 36.81/11.42 | (378) all_88_1_88 = all_52_3_30 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_50_3_26, all_88_1_88 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_88_1_88, apart_point_and_line(all_1_2_2, all_1_5_5) = all_50_3_26, yields: % 36.81/11.42 | (379) all_88_1_88 = all_50_3_26 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_4_4, all_1_5_5, all_96_2_101, all_108_2_119 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = all_108_2_119, convergent_lines(all_1_4_4, all_1_5_5) = all_96_2_101, yields: % 36.81/11.42 | (380) all_108_2_119 = all_96_2_101 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_4_4, all_1_5_5, all_90_2_92, all_108_2_119 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = all_108_2_119, convergent_lines(all_1_4_4, all_1_5_5) = all_90_2_92, yields: % 36.81/11.42 | (381) all_108_2_119 = all_90_2_92 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_4_4, all_1_5_5, all_80_2_77, all_96_2_101 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = all_96_2_101, convergent_lines(all_1_4_4, all_1_5_5) = all_80_2_77, yields: % 36.81/11.42 | (382) all_96_2_101 = all_80_2_77 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_5_5, all_1_3_3, all_110_2_122, 0 and discharging atoms convergent_lines(all_1_5_5, all_1_3_3) = all_110_2_122, convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 36.81/11.42 | (383) all_110_2_122 = 0 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_5_5, all_1_3_3, all_102_2_110, all_110_2_122 and discharging atoms convergent_lines(all_1_5_5, all_1_3_3) = all_110_2_122, convergent_lines(all_1_5_5, all_1_3_3) = all_102_2_110, yields: % 36.81/11.42 | (384) all_110_2_122 = all_102_2_110 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_5_5, all_1_4_4, all_94_2_98, all_106_2_116 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_106_2_116, convergent_lines(all_1_5_5, all_1_4_4) = all_94_2_98, yields: % 36.81/11.42 | (385) all_106_2_116 = all_94_2_98 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_5_5, all_1_4_4, all_88_2_89, 0 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_88_2_89, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 36.81/11.42 | (386) all_88_2_89 = 0 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_5_5, all_1_4_4, all_88_2_89, all_106_2_116 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_106_2_116, convergent_lines(all_1_5_5, all_1_4_4) = all_88_2_89, yields: % 36.81/11.42 | (387) all_106_2_116 = all_88_2_89 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (4) with all_1_5_5, all_1_4_4, all_78_2_74, all_106_2_116 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_106_2_116, convergent_lines(all_1_5_5, all_1_4_4) = all_78_2_74, yields: % 36.81/11.42 | (388) all_106_2_116 = all_78_2_74 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_1_1, all_1_1_1, all_108_0_117, all_35_3_22 and discharging atoms distinct_points(all_1_1_1, all_1_1_1) = all_108_0_117, distinct_points(all_1_1_1, all_1_1_1) = all_35_3_22, yields: % 36.81/11.42 | (389) all_108_0_117 = all_35_3_22 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_1_1, all_1_1_1, all_108_0_117, all_137_2_137 and discharging atoms distinct_points(all_1_1_1, all_1_1_1) = all_137_2_137, distinct_points(all_1_1_1, all_1_1_1) = all_108_0_117, yields: % 36.81/11.42 | (390) all_137_2_137 = all_108_0_117 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_1_1, all_1_1_1, all_96_0_99, all_137_2_137 and discharging atoms distinct_points(all_1_1_1, all_1_1_1) = all_137_2_137, distinct_points(all_1_1_1, all_1_1_1) = all_96_0_99, yields: % 36.81/11.42 | (391) all_137_2_137 = all_96_0_99 % 36.81/11.42 | % 36.81/11.42 | Using (281) and (105) yields: % 36.81/11.42 | (392) ~ (all_96_0_99 = 0) % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_1_1, all_1_2_2, all_106_0_114, all_92_0_93 and discharging atoms distinct_points(all_1_1_1, all_1_2_2) = all_106_0_114, yields: % 36.81/11.42 | (393) all_106_0_114 = all_92_0_93 | ~ (distinct_points(all_1_1_1, all_1_2_2) = all_92_0_93) % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_1_1, all_1_2_2, all_94_0_96, all_106_0_114 and discharging atoms distinct_points(all_1_1_1, all_1_2_2) = all_106_0_114, distinct_points(all_1_1_1, all_1_2_2) = all_94_0_96, yields: % 36.81/11.42 | (394) all_106_0_114 = all_94_0_96 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_1_1, all_1_2_2, all_70_0_60, all_106_0_114 and discharging atoms distinct_points(all_1_1_1, all_1_2_2) = all_106_0_114, distinct_points(all_1_1_1, all_1_2_2) = all_70_0_60, yields: % 36.81/11.42 | (395) all_106_0_114 = all_70_0_60 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_1_1, all_1_2_2, all_66_0_54, all_94_0_96 and discharging atoms distinct_points(all_1_1_1, all_1_2_2) = all_94_0_96, distinct_points(all_1_1_1, all_1_2_2) = all_66_0_54, yields: % 36.81/11.42 | (396) all_94_0_96 = all_66_0_54 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_1_1, all_1_2_2, all_64_0_51, all_94_0_96 and discharging atoms distinct_points(all_1_1_1, all_1_2_2) = all_94_0_96, distinct_points(all_1_1_1, all_1_2_2) = all_64_0_51, yields: % 36.81/11.42 | (397) all_94_0_96 = all_64_0_51 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_2_2, all_1_1_1, all_90_0_90, 0 and discharging atoms distinct_points(all_1_2_2, all_1_1_1) = all_90_0_90, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 36.81/11.42 | (398) all_90_0_90 = 0 % 36.81/11.42 | % 36.81/11.42 | Instantiating formula (8) with all_1_2_2, all_1_1_1, all_80_0_75, all_90_0_90 and discharging atoms distinct_points(all_1_2_2, all_1_1_1) = all_90_0_90, distinct_points(all_1_2_2, all_1_1_1) = all_80_0_75, yields: % 36.81/11.42 | (399) all_90_0_90 = all_80_0_75 % 36.81/11.42 | % 36.81/11.43 | Instantiating formula (8) with all_1_2_2, all_1_2_2, all_78_0_72, all_88_0_87 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_88_0_87, distinct_points(all_1_2_2, all_1_2_2) = all_78_0_72, yields: % 36.81/11.43 | (400) all_88_0_87 = all_78_0_72 % 36.81/11.43 | % 36.81/11.43 | Instantiating formula (8) with all_1_2_2, all_1_2_2, all_74_0_66, all_88_0_87 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_88_0_87, distinct_points(all_1_2_2, all_1_2_2) = all_74_0_66, yields: % 36.81/11.43 | (401) all_88_0_87 = all_74_0_66 % 36.81/11.43 | % 36.81/11.43 | Instantiating formula (8) with all_1_2_2, all_1_2_2, all_72_0_63, all_78_0_72 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_78_0_72, distinct_points(all_1_2_2, all_1_2_2) = all_72_0_63, yields: % 36.81/11.43 | (402) all_78_0_72 = all_72_0_63 % 36.81/11.43 | % 36.81/11.43 | Using (226) and (106) yields: % 36.81/11.43 | (403) ~ (all_72_0_63 = 0) % 36.81/11.43 | % 36.81/11.43 | Instantiating formula (8) with all_1_2_2, all_1_2_2, all_68_0_57, all_78_0_72 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_78_0_72, distinct_points(all_1_2_2, all_1_2_2) = all_68_0_57, yields: % 36.81/11.43 | (404) all_78_0_72 = all_68_0_57 % 36.81/11.43 | % 36.81/11.43 | Combining equations (390,391) yields a new equation: % 36.81/11.43 | (405) all_108_0_117 = all_96_0_99 % 36.81/11.43 | % 36.81/11.43 | Simplifying 405 yields: % 36.81/11.43 | (406) all_108_0_117 = all_96_0_99 % 36.81/11.43 | % 36.81/11.43 | Combining equations (349,353) yields a new equation: % 36.81/11.43 | (407) all_112_1_124 = all_98_2_104 % 36.81/11.43 | % 36.81/11.43 | Simplifying 407 yields: % 36.81/11.43 | (408) all_112_1_124 = all_98_2_104 % 36.81/11.43 | % 36.81/11.43 | Combining equations (355,356) yields a new equation: % 36.81/11.43 | (409) all_96_1_100 = all_94_1_97 % 36.81/11.43 | % 36.81/11.43 | Simplifying 409 yields: % 36.81/11.43 | (410) all_96_1_100 = all_94_1_97 % 36.81/11.43 | % 36.81/11.43 | Combining equations (354,356) yields a new equation: % 36.81/11.43 | (411) all_94_1_97 = all_21_2_12 % 36.81/11.43 | % 36.81/11.43 | Combining equations (358,356) yields a new equation: % 36.81/11.43 | (412) all_94_1_97 = all_50_0_23 % 36.81/11.43 | % 36.81/11.43 | Combining equations (351,408) yields a new equation: % 36.81/11.43 | (413) all_104_2_113 = all_98_2_104 % 36.81/11.43 | % 36.81/11.43 | Simplifying 413 yields: % 36.81/11.43 | (414) all_104_2_113 = all_98_2_104 % 36.81/11.43 | % 36.81/11.43 | Combining equations (361,360) yields a new equation: % 36.81/11.43 | (415) all_108_1_118 = all_106_1_115 % 36.81/11.43 | % 36.81/11.43 | Combining equations (362,360) yields a new equation: % 36.81/11.43 | (416) all_108_1_118 = all_100_2_107 % 36.81/11.43 | % 36.81/11.43 | Combining equations (359,360) yields a new equation: % 36.81/11.43 | (417) all_108_1_118 = all_23_2_15 % 36.81/11.43 | % 36.81/11.43 | Combining equations (384,383) yields a new equation: % 36.81/11.43 | (418) all_102_2_110 = 0 % 36.81/11.43 | % 36.81/11.43 | Simplifying 418 yields: % 36.81/11.43 | (419) all_102_2_110 = 0 % 36.81/11.43 | % 36.81/11.43 | Combining equations (389,406) yields a new equation: % 36.81/11.43 | (420) all_96_0_99 = all_35_3_22 % 36.81/11.43 | % 36.81/11.43 | Combining equations (416,415) yields a new equation: % 36.81/11.43 | (421) all_106_1_115 = all_100_2_107 % 36.81/11.43 | % 36.81/11.43 | Combining equations (417,415) yields a new equation: % 36.81/11.43 | (422) all_106_1_115 = all_23_2_15 % 36.81/11.43 | % 36.81/11.43 | Combining equations (380,381) yields a new equation: % 36.81/11.43 | (423) all_96_2_101 = all_90_2_92 % 36.81/11.43 | % 36.81/11.43 | Simplifying 423 yields: % 36.81/11.43 | (424) all_96_2_101 = all_90_2_92 % 36.81/11.43 | % 36.81/11.43 | Combining equations (394,395) yields a new equation: % 36.81/11.43 | (425) all_94_0_96 = all_70_0_60 % 36.81/11.43 | % 36.81/11.43 | Simplifying 425 yields: % 36.81/11.43 | (426) all_94_0_96 = all_70_0_60 % 36.81/11.43 | % 36.81/11.43 | Combining equations (421,422) yields a new equation: % 36.81/11.43 | (427) all_100_2_107 = all_23_2_15 % 36.81/11.43 | % 36.81/11.43 | Simplifying 427 yields: % 36.81/11.43 | (428) all_100_2_107 = all_23_2_15 % 36.81/11.43 | % 36.81/11.43 | Combining equations (387,385) yields a new equation: % 36.81/11.43 | (429) all_94_2_98 = all_88_2_89 % 36.81/11.43 | % 36.81/11.43 | Combining equations (388,385) yields a new equation: % 36.81/11.43 | (430) all_94_2_98 = all_78_2_74 % 36.81/11.43 | % 36.81/11.43 | Combining equations (350,352) yields a new equation: % 36.81/11.43 | (431) all_102_1_109 = all_1_0_0 % 36.81/11.43 | % 36.81/11.43 | Combining equations (414,352) yields a new equation: % 36.81/11.43 | (432) all_102_1_109 = all_98_2_104 % 36.81/11.43 | % 36.81/11.43 | Combining equations (431,432) yields a new equation: % 36.81/11.43 | (433) all_98_2_104 = all_1_0_0 % 36.81/11.43 | % 36.81/11.43 | Combining equations (343,345) yields a new equation: % 36.81/11.43 | (434) all_92_1_94 = all_76_1_70 % 36.81/11.43 | % 36.81/11.43 | Simplifying 434 yields: % 36.81/11.43 | (435) all_92_1_94 = all_76_1_70 % 36.81/11.43 | % 36.81/11.43 | Combining equations (363,428) yields a new equation: % 36.81/11.43 | (436) all_50_1_24 = all_23_2_15 % 36.81/11.43 | % 36.81/11.43 | Simplifying 436 yields: % 36.81/11.43 | (437) all_50_1_24 = all_23_2_15 % 36.81/11.43 | % 36.81/11.43 | Combining equations (410,357) yields a new equation: % 36.81/11.43 | (438) all_94_1_97 = all_92_2_95 % 36.81/11.43 | % 36.81/11.43 | Simplifying 438 yields: % 36.81/11.43 | (439) all_94_1_97 = all_92_2_95 % 36.81/11.43 | % 36.81/11.43 | Combining equations (424,382) yields a new equation: % 36.81/11.43 | (440) all_90_2_92 = all_80_2_77 % 36.81/11.43 | % 36.81/11.43 | Simplifying 440 yields: % 36.81/11.43 | (441) all_90_2_92 = all_80_2_77 % 36.81/11.43 | % 36.81/11.43 | Combining equations (396,426) yields a new equation: % 36.81/11.43 | (442) all_70_0_60 = all_66_0_54 % 36.81/11.43 | % 36.81/11.43 | Combining equations (397,426) yields a new equation: % 36.81/11.43 | (443) all_70_0_60 = all_64_0_51 % 36.81/11.43 | % 36.81/11.43 | Combining equations (411,439) yields a new equation: % 36.81/11.43 | (444) all_92_2_95 = all_21_2_12 % 36.81/11.43 | % 36.81/11.43 | Combining equations (412,439) yields a new equation: % 36.81/11.43 | (445) all_92_2_95 = all_50_0_23 % 36.81/11.43 | % 36.81/11.43 | Combining equations (429,430) yields a new equation: % 36.81/11.43 | (446) all_88_2_89 = all_78_2_74 % 36.81/11.43 | % 36.81/11.43 | Simplifying 446 yields: % 36.81/11.43 | (447) all_88_2_89 = all_78_2_74 % 36.81/11.43 | % 36.81/11.43 | Combining equations (435,344) yields a new equation: % 36.81/11.43 | (448) all_86_1_85 = all_76_1_70 % 36.81/11.43 | % 36.81/11.43 | Combining equations (342,344) yields a new equation: % 36.81/11.43 | (449) all_86_1_85 = all_1_2_2 % 36.81/11.43 | % 36.81/11.43 | Combining equations (444,445) yields a new equation: % 36.81/11.43 | (450) all_50_0_23 = all_21_2_12 % 36.81/11.43 | % 36.81/11.43 | Combining equations (399,398) yields a new equation: % 36.81/11.43 | (451) all_80_0_75 = 0 % 36.81/11.43 | % 36.81/11.43 | Simplifying 451 yields: % 36.81/11.43 | (452) all_80_0_75 = 0 % 36.81/11.43 | % 36.81/11.43 | Combining equations (372,377) yields a new equation: % 36.81/11.43 | (453) all_86_2_86 = all_54_3_34 % 36.81/11.43 | % 36.81/11.43 | Simplifying 453 yields: % 36.81/11.43 | (454) all_86_2_86 = all_54_3_34 % 36.81/11.43 | % 36.81/11.43 | Combining equations (400,401) yields a new equation: % 36.81/11.43 | (455) all_78_0_72 = all_74_0_66 % 36.81/11.43 | % 36.81/11.43 | Simplifying 455 yields: % 36.81/11.43 | (456) all_78_0_72 = all_74_0_66 % 36.81/11.43 | % 36.81/11.43 | Combining equations (379,378) yields a new equation: % 36.81/11.43 | (457) all_52_3_30 = all_50_3_26 % 36.81/11.43 | % 36.81/11.43 | Combining equations (375,378) yields a new equation: % 36.81/11.43 | (458) all_58_3_42 = all_52_3_30 % 36.81/11.43 | % 36.81/11.43 | Simplifying 458 yields: % 36.81/11.43 | (459) all_58_3_42 = all_52_3_30 % 36.81/11.43 | % 36.81/11.43 | Combining equations (386,447) yields a new equation: % 36.81/11.43 | (460) all_78_2_74 = 0 % 36.81/11.43 | % 36.81/11.43 | Combining equations (449,448) yields a new equation: % 36.81/11.43 | (461) all_76_1_70 = all_1_2_2 % 36.81/11.43 | % 36.81/11.43 | Combining equations (373,454) yields a new equation: % 36.81/11.43 | (462) all_60_3_46 = all_54_3_34 % 36.81/11.43 | % 36.81/11.43 | Simplifying 462 yields: % 36.81/11.43 | (463) all_60_3_46 = all_54_3_34 % 36.81/11.43 | % 36.81/11.43 | Combining equations (369,364) yields a new equation: % 36.81/11.43 | (464) all_78_1_73 = all_52_2_29 % 36.81/11.43 | % 36.81/11.43 | Combining equations (366,364) yields a new equation: % 36.81/11.43 | (465) all_78_1_73 = all_76_2_71 % 36.81/11.43 | % 36.81/11.43 | Combining equations (367,364) yields a new equation: % 36.81/11.43 | (466) all_78_1_73 = all_62_2_49 % 36.81/11.43 | % 36.81/11.43 | Combining equations (402,456) yields a new equation: % 36.81/11.43 | (467) all_74_0_66 = all_72_0_63 % 36.81/11.43 | % 36.81/11.43 | Combining equations (404,456) yields a new equation: % 36.81/11.43 | (468) all_74_0_66 = all_68_0_57 % 36.81/11.43 | % 36.81/11.43 | Combining equations (464,466) yields a new equation: % 36.81/11.43 | (469) all_62_2_49 = all_52_2_29 % 36.81/11.43 | % 36.81/11.43 | Combining equations (465,466) yields a new equation: % 36.81/11.43 | (470) all_76_2_71 = all_62_2_49 % 36.81/11.43 | % 36.81/11.43 | Simplifying 470 yields: % 36.81/11.43 | (471) all_76_2_71 = all_62_2_49 % 36.81/11.43 | % 36.81/11.43 | Combining equations (471,365) yields a new equation: % 36.81/11.43 | (472) all_62_2_49 = all_17_1_7 % 36.81/11.43 | % 36.81/11.43 | Simplifying 472 yields: % 36.81/11.43 | (473) all_62_2_49 = all_17_1_7 % 36.81/11.43 | % 36.81/11.43 | Combining equations (467,468) yields a new equation: % 36.81/11.43 | (474) all_72_0_63 = all_68_0_57 % 36.81/11.43 | % 36.81/11.43 | Simplifying 474 yields: % 36.81/11.43 | (475) all_72_0_63 = all_68_0_57 % 36.81/11.43 | % 36.81/11.43 | Combining equations (443,442) yields a new equation: % 36.81/11.43 | (476) all_66_0_54 = all_64_0_51 % 36.81/11.43 | % 36.81/11.43 | Combining equations (469,473) yields a new equation: % 36.81/11.43 | (477) all_52_2_29 = all_17_1_7 % 36.81/11.43 | % 36.81/11.43 | Simplifying 477 yields: % 36.81/11.43 | (478) all_52_2_29 = all_17_1_7 % 36.81/11.43 | % 36.81/11.43 | Combining equations (376,463) yields a new equation: % 36.81/11.43 | (479) all_58_3_42 = all_54_3_34 % 36.81/11.43 | % 36.81/11.43 | Simplifying 479 yields: % 36.81/11.43 | (480) all_58_3_42 = all_54_3_34 % 36.81/11.43 | % 36.81/11.43 | Combining equations (371,368) yields a new equation: % 36.81/11.43 | (481) all_56_2_37 = all_50_2_25 % 36.81/11.43 | % 36.81/11.43 | Combining equations (370,368) yields a new equation: % 36.81/11.43 | (482) all_56_2_37 = all_52_2_29 % 36.81/11.43 | % 36.81/11.43 | Combining equations (459,480) yields a new equation: % 36.81/11.43 | (483) all_54_3_34 = all_52_3_30 % 36.81/11.43 | % 36.81/11.43 | Combining equations (374,480) yields a new equation: % 36.81/11.43 | (484) all_54_3_34 = all_19_1_9 % 36.81/11.43 | % 36.81/11.43 | Combining equations (482,481) yields a new equation: % 36.81/11.43 | (485) all_52_2_29 = all_50_2_25 % 36.81/11.43 | % 36.81/11.43 | Simplifying 485 yields: % 36.81/11.43 | (486) all_52_2_29 = all_50_2_25 % 36.81/11.43 | % 36.81/11.43 | Combining equations (483,484) yields a new equation: % 36.81/11.43 | (487) all_52_3_30 = all_19_1_9 % 36.81/11.43 | % 36.81/11.43 | Simplifying 487 yields: % 36.81/11.43 | (488) all_52_3_30 = all_19_1_9 % 36.81/11.43 | % 36.81/11.43 | Combining equations (486,478) yields a new equation: % 36.81/11.43 | (489) all_50_2_25 = all_17_1_7 % 36.81/11.43 | % 36.81/11.43 | Simplifying 489 yields: % 36.81/11.43 | (490) all_50_2_25 = all_17_1_7 % 36.81/11.43 | % 36.81/11.43 | Combining equations (488,457) yields a new equation: % 36.81/11.43 | (491) all_50_3_26 = all_19_1_9 % 36.81/11.43 | % 36.81/11.43 | Combining equations (491,457) yields a new equation: % 36.81/11.43 | (488) all_52_3_30 = all_19_1_9 % 36.81/11.43 | % 36.81/11.43 | Combining equations (476,442) yields a new equation: % 36.81/11.43 | (443) all_70_0_60 = all_64_0_51 % 36.81/11.43 | % 36.81/11.43 | Combining equations (461,448) yields a new equation: % 36.81/11.43 | (449) all_86_1_85 = all_1_2_2 % 36.81/11.43 | % 36.81/11.43 | Combining equations (460,447) yields a new equation: % 36.81/11.43 | (386) all_88_2_89 = 0 % 36.81/11.43 | % 36.81/11.43 | Combining equations (488,378) yields a new equation: % 36.81/11.43 | (496) all_88_1_88 = all_19_1_9 % 36.81/11.43 | % 36.81/11.43 | Combining equations (468,401) yields a new equation: % 36.81/11.43 | (497) all_88_0_87 = all_68_0_57 % 36.81/11.43 | % 36.81/11.43 | Combining equations (450,445) yields a new equation: % 36.81/11.43 | (444) all_92_2_95 = all_21_2_12 % 36.81/11.43 | % 36.81/11.43 | Combining equations (449,344) yields a new equation: % 36.81/11.43 | (342) all_92_1_94 = all_1_2_2 % 36.81/11.43 | % 36.81/11.43 | Combining equations (444,357) yields a new equation: % 36.81/11.43 | (500) all_96_1_100 = all_21_2_12 % 36.81/11.43 | % 36.81/11.43 | Combining equations (443,395) yields a new equation: % 36.81/11.43 | (501) all_106_0_114 = all_64_0_51 % 36.81/11.43 | % 36.81/11.43 | Equations (420) can reduce 392 to: % 36.81/11.43 | (113) ~ (all_35_3_22 = 0) % 36.81/11.43 | % 36.81/11.43 | Equations (475) can reduce 403 to: % 36.81/11.43 | (503) ~ (all_68_0_57 = 0) % 36.81/11.43 | % 36.81/11.43 | From (433) and (285) follows: % 36.81/11.43 | (53) apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0 % 36.81/11.43 | % 36.81/11.43 | From (348) and (230) follows: % 36.81/11.43 | (505) apart_point_and_line(all_1_2_2, all_66_2_56) = all_74_1_67 % 36.81/11.43 | % 36.81/11.43 | From (346) and (225) follows: % 36.81/11.43 | (506) apart_point_and_line(all_1_2_2, all_70_2_62) = all_72_1_64 % 36.81/11.43 | % 36.81/11.43 | From (347) and (215) follows: % 36.81/11.43 | (507) apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58 % 36.81/11.43 | % 36.81/11.43 | From (490) and (165) follows: % 36.81/11.43 | (69) apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7 % 36.81/11.43 | % 36.81/11.43 | From (491) and (163) follows: % 36.81/11.43 | (73) apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9 % 36.81/11.43 | % 36.81/11.43 | From (441) and (265) follows: % 36.81/11.43 | (245) convergent_lines(all_1_4_4, all_1_5_5) = all_80_2_77 % 36.81/11.43 | % 36.81/11.43 | From (419) and (295) follows: % 36.81/11.43 | (49) convergent_lines(all_1_5_5, all_1_3_3) = 0 % 36.81/11.43 | % 36.81/11.43 | From (460) and (240) follows: % 36.81/11.43 | (55) convergent_lines(all_1_5_5, all_1_4_4) = 0 % 36.81/11.43 | % 36.81/11.43 | From (342) and (271) follows: % 36.81/11.43 | (513) distinct_points(all_1_1_1, all_1_2_2) = all_92_0_93 % 36.81/11.43 | % 36.81/11.43 | From (420) and (281) follows: % 36.81/11.43 | (99) distinct_points(all_1_1_1, all_1_1_1) = all_35_3_22 % 36.81/11.43 | % 36.81/11.43 | From (452) and (246) follows: % 36.81/11.43 | (90) distinct_points(all_1_2_2, all_1_1_1) = 0 % 36.81/11.43 | % 36.81/11.43 +-Applying beta-rule and splitting (227), into two cases. % 36.81/11.43 |-Branch one: % 36.81/11.43 | (516) ~ (all_72_1_64 = 0) % 36.81/11.43 | % 36.81/11.43 +-Applying beta-rule and splitting (393), into two cases. % 36.81/11.43 |-Branch one: % 36.81/11.43 | (517) ~ (distinct_points(all_1_1_1, all_1_2_2) = all_92_0_93) % 36.81/11.43 | % 36.81/11.43 | Using (513) and (517) yields: % 36.81/11.43 | (518) $false % 36.81/11.43 | % 36.81/11.43 |-The branch is then unsatisfiable % 36.81/11.43 |-Branch two: % 36.81/11.43 | (513) distinct_points(all_1_1_1, all_1_2_2) = all_92_0_93 % 36.81/11.43 | (520) all_106_0_114 = all_92_0_93 % 36.81/11.43 | % 36.81/11.43 | Combining equations (520,501) yields a new equation: % 36.81/11.43 | (521) all_92_0_93 = all_64_0_51 % 36.81/11.43 | % 36.81/11.43 | Simplifying 521 yields: % 36.81/11.43 | (522) all_92_0_93 = all_64_0_51 % 36.81/11.43 | % 36.81/11.43 | From (522) and (513) follows: % 36.81/11.43 | (206) distinct_points(all_1_1_1, all_1_2_2) = all_64_0_51 % 36.81/11.43 | % 36.81/11.43 +-Applying beta-rule and splitting (232), into two cases. % 36.81/11.43 |-Branch one: % 36.81/11.43 | (524) ~ (all_74_1_67 = 0) % 36.81/11.43 | % 36.81/11.43 +-Applying beta-rule and splitting (262), into two cases. % 36.81/11.43 |-Branch one: % 36.81/11.43 | (525) ~ (all_88_2_89 = 0) % 36.81/11.43 | % 36.81/11.43 | Equations (386) can reduce 525 to: % 36.81/11.43 | (92) $false % 36.81/11.43 | % 36.81/11.43 |-The branch is then unsatisfiable % 36.81/11.43 |-Branch two: % 36.81/11.43 | (386) all_88_2_89 = 0 % 36.81/11.43 | (528) all_88_0_87 = 0 | ( ~ (all_88_1_88 = 0) & ~ (all_17_1_7 = 0)) % 36.81/11.43 | % 36.81/11.43 +-Applying beta-rule and splitting (528), into two cases. % 36.81/11.43 |-Branch one: % 36.81/11.43 | (529) all_88_0_87 = 0 % 36.81/11.43 | % 36.81/11.43 | Combining equations (529,497) yields a new equation: % 36.81/11.43 | (530) all_68_0_57 = 0 % 36.81/11.43 | % 36.81/11.43 | Equations (530) can reduce 503 to: % 36.81/11.43 | (92) $false % 36.81/11.43 | % 36.81/11.43 |-The branch is then unsatisfiable % 36.81/11.43 |-Branch two: % 36.81/11.43 | (532) ~ (all_88_0_87 = 0) % 36.81/11.43 | (533) ~ (all_88_1_88 = 0) & ~ (all_17_1_7 = 0) % 36.81/11.43 | % 36.81/11.43 | Applying alpha-rule on (533) yields: % 36.81/11.43 | (534) ~ (all_88_1_88 = 0) % 36.81/11.43 | (535) ~ (all_17_1_7 = 0) % 36.81/11.43 | % 36.81/11.43 | Equations (497) can reduce 532 to: % 36.81/11.43 | (503) ~ (all_68_0_57 = 0) % 36.81/11.43 | % 36.81/11.43 | Equations (496) can reduce 534 to: % 36.81/11.43 | (537) ~ (all_19_1_9 = 0) % 36.81/11.43 | % 36.81/11.43 +-Applying beta-rule and splitting (139), into two cases. % 36.81/11.43 |-Branch one: % 36.81/11.43 | (538) all_17_1_7 = 0 % 36.81/11.43 | % 36.81/11.43 | Equations (538) can reduce 535 to: % 36.81/11.43 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (535) ~ (all_17_1_7 = 0) % 36.81/11.44 | (541) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 | Instantiating (541) with all_203_0_147, all_203_1_148, all_203_2_149 yields: % 36.81/11.44 | (542) apart_point_and_line(all_1_2_2, all_1_5_5) = all_203_0_147 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_203_1_148 & distinct_points(all_1_2_2, all_1_2_2) = all_203_2_149 & ( ~ (all_203_2_149 = 0) | all_203_0_147 = 0 | all_203_1_148 = 0) % 36.81/11.44 | % 36.81/11.44 | Applying alpha-rule on (542) yields: % 36.81/11.44 | (543) apart_point_and_line(all_1_2_2, all_1_5_5) = all_203_0_147 % 36.81/11.44 | (544) apart_point_and_line(all_1_2_2, all_1_5_5) = all_203_1_148 % 36.81/11.44 | (545) distinct_points(all_1_2_2, all_1_2_2) = all_203_2_149 % 36.81/11.44 | (546) ~ (all_203_2_149 = 0) | all_203_0_147 = 0 | all_203_1_148 = 0 % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (159), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (550) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (144), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (554) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_19_0_8, all_1_5_5) = v2 & apart_point_and_line(all_19_0_8, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (140), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (558) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 | Instantiating (558) with all_219_0_156, all_219_1_157, all_219_2_158 yields: % 36.81/11.44 | (559) apart_point_and_line(all_1_2_2, all_1_4_4) = all_219_0_156 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_219_1_157 & distinct_points(all_1_2_2, all_1_2_2) = all_219_2_158 & ( ~ (all_219_2_158 = 0) | all_219_0_156 = 0 | all_219_1_157 = 0) % 36.81/11.44 | % 36.81/11.44 | Applying alpha-rule on (559) yields: % 36.81/11.44 | (560) apart_point_and_line(all_1_2_2, all_1_4_4) = all_219_0_156 % 36.81/11.44 | (561) apart_point_and_line(all_1_2_2, all_1_4_4) = all_219_1_157 % 36.81/11.44 | (562) distinct_points(all_1_2_2, all_1_2_2) = all_219_2_158 % 36.81/11.44 | (563) ~ (all_219_2_158 = 0) | all_219_0_156 = 0 | all_219_1_157 = 0 % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (127), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (538) all_17_1_7 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (538) can reduce 535 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (535) ~ (all_17_1_7 = 0) % 36.81/11.44 | (567) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.44 | % 36.81/11.44 | Instantiating (567) with all_224_0_159, all_224_1_160, all_224_2_161, all_224_3_162 yields: % 36.81/11.44 | (568) apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_0_159 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_1_160 & distinct_lines(all_1_4_4, all_1_4_4) = all_224_2_161 & distinct_points(all_1_2_2, all_1_2_2) = all_224_3_162 & ( ~ (all_224_2_161 = 0) | ~ (all_224_3_162 = 0) | all_224_0_159 = 0 | all_224_1_160 = 0) % 36.81/11.44 | % 36.81/11.44 | Applying alpha-rule on (568) yields: % 36.81/11.44 | (569) ~ (all_224_2_161 = 0) | ~ (all_224_3_162 = 0) | all_224_0_159 = 0 | all_224_1_160 = 0 % 36.81/11.44 | (570) distinct_lines(all_1_4_4, all_1_4_4) = all_224_2_161 % 36.81/11.44 | (571) apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_0_159 % 36.81/11.44 | (572) distinct_points(all_1_2_2, all_1_2_2) = all_224_3_162 % 36.81/11.44 | (573) apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_1_160 % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (152), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (538) all_17_1_7 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (538) can reduce 535 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (535) ~ (all_17_1_7 = 0) % 36.81/11.44 | (577) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_17_0_6, all_1_4_4) = v2 & apart_point_and_line(all_17_0_6, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (143), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (538) all_17_1_7 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (538) can reduce 535 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (535) ~ (all_17_1_7 = 0) % 36.81/11.44 | (581) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_19_0_8, all_1_4_4) = v2 & apart_point_and_line(all_19_0_8, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (131), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (585) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (153), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (589) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_17_0_6, all_1_4_4) = v1 & apart_point_and_line(all_17_0_6, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (135), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (593) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (132), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (597) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (158), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (601) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (217), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (602) ~ (all_68_1_58 = 0) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (134), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (547) all_19_1_9 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (547) can reduce 537 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (537) ~ (all_19_1_9 = 0) % 36.81/11.44 | (606) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (589), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (538) all_17_1_7 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (538) can reduce 535 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (535) ~ (all_17_1_7 = 0) % 36.81/11.44 | (610) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_17_0_6, all_1_4_4) = v1 & apart_point_and_line(all_17_0_6, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.44 | % 36.81/11.44 +-Applying beta-rule and splitting (593), into two cases. % 36.81/11.44 |-Branch one: % 36.81/11.44 | (538) all_17_1_7 = 0 % 36.81/11.44 | % 36.81/11.44 | Equations (538) can reduce 535 to: % 36.81/11.44 | (92) $false % 36.81/11.44 | % 36.81/11.44 |-The branch is then unsatisfiable % 36.81/11.44 |-Branch two: % 36.81/11.44 | (535) ~ (all_17_1_7 = 0) % 36.81/11.44 | (614) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.44 | % 36.81/11.44 | Instantiating (614) with all_270_0_172, all_270_1_173, all_270_2_174, all_270_3_175 yields: % 36.81/11.44 | (615) apart_point_and_line(all_1_2_2, all_1_4_4) = all_270_1_173 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_270_0_172 & distinct_lines(all_1_4_4, all_1_5_5) = all_270_2_174 & distinct_points(all_1_2_2, all_1_2_2) = all_270_3_175 & ( ~ (all_270_2_174 = 0) | ~ (all_270_3_175 = 0) | all_270_0_172 = 0 | all_270_1_173 = 0) % 36.81/11.44 | % 36.81/11.44 | Applying alpha-rule on (615) yields: % 36.81/11.44 | (616) apart_point_and_line(all_1_2_2, all_1_4_4) = all_270_1_173 % 36.81/11.44 | (617) apart_point_and_line(all_1_2_2, all_1_5_5) = all_270_0_172 % 36.81/11.44 | (618) distinct_points(all_1_2_2, all_1_2_2) = all_270_3_175 % 36.81/11.44 | (619) distinct_lines(all_1_4_4, all_1_5_5) = all_270_2_174 % 36.81/11.44 | (620) ~ (all_270_2_174 = 0) | ~ (all_270_3_175 = 0) | all_270_0_172 = 0 | all_270_1_173 = 0 % 36.81/11.44 | % 36.81/11.44 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_224_0_159, all_270_1_173 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_270_1_173, apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_0_159, yields: % 36.81/11.44 | (621) all_270_1_173 = all_224_0_159 % 36.81/11.44 | % 36.81/11.44 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_224_1_160, all_17_1_7 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_1_160, apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, yields: % 36.81/11.44 | (622) all_224_1_160 = all_17_1_7 % 36.81/11.44 | % 36.81/11.44 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_224_1_160, all_224_0_159 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_0_159, apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_1_160, yields: % 36.81/11.44 | (623) all_224_0_159 = all_224_1_160 % 36.81/11.44 | % 36.81/11.44 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_219_0_156, all_270_1_173 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_270_1_173, apart_point_and_line(all_1_2_2, all_1_4_4) = all_219_0_156, yields: % 36.81/11.44 | (624) all_270_1_173 = all_219_0_156 % 36.81/11.44 | % 36.81/11.44 | Instantiating formula (22) with all_1_2_2, all_1_4_4, all_219_1_157, all_224_1_160 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_224_1_160, apart_point_and_line(all_1_2_2, all_1_4_4) = all_219_1_157, yields: % 36.81/11.44 | (625) all_224_1_160 = all_219_1_157 % 36.81/11.44 | % 36.81/11.44 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_270_0_172, all_19_1_9 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_270_0_172, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.81/11.44 | (626) all_270_0_172 = all_19_1_9 % 36.81/11.44 | % 36.81/11.44 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_203_0_147, all_270_0_172 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_270_0_172, apart_point_and_line(all_1_2_2, all_1_5_5) = all_203_0_147, yields: % 36.81/11.44 | (627) all_270_0_172 = all_203_0_147 % 36.81/11.44 | % 36.81/11.44 | Instantiating formula (22) with all_1_2_2, all_1_5_5, all_203_1_148, all_203_0_147 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_203_0_147, apart_point_and_line(all_1_2_2, all_1_5_5) = all_203_1_148, yields: % 36.81/11.44 | (628) all_203_0_147 = all_203_1_148 % 36.81/11.44 | % 36.81/11.44 | Combining equations (627,626) yields a new equation: % 36.81/11.44 | (629) all_203_0_147 = all_19_1_9 % 36.81/11.44 | % 36.81/11.44 | Simplifying 629 yields: % 36.81/11.44 | (630) all_203_0_147 = all_19_1_9 % 36.81/11.44 | % 36.81/11.44 | Combining equations (621,624) yields a new equation: % 36.81/11.44 | (631) all_224_0_159 = all_219_0_156 % 36.81/11.44 | % 36.81/11.44 | Simplifying 631 yields: % 36.81/11.44 | (632) all_224_0_159 = all_219_0_156 % 36.81/11.44 | % 36.81/11.44 | Combining equations (623,632) yields a new equation: % 36.81/11.44 | (633) all_224_1_160 = all_219_0_156 % 36.81/11.44 | % 36.81/11.44 | Simplifying 633 yields: % 36.81/11.44 | (634) all_224_1_160 = all_219_0_156 % 36.81/11.44 | % 36.81/11.44 | Combining equations (622,634) yields a new equation: % 36.81/11.44 | (635) all_219_0_156 = all_17_1_7 % 36.81/11.44 | % 36.81/11.44 | Combining equations (625,634) yields a new equation: % 36.81/11.44 | (636) all_219_0_156 = all_219_1_157 % 36.81/11.44 | % 36.81/11.44 | Combining equations (636,635) yields a new equation: % 36.81/11.44 | (637) all_219_1_157 = all_17_1_7 % 36.81/11.45 | % 36.81/11.45 | Simplifying 637 yields: % 36.81/11.45 | (638) all_219_1_157 = all_17_1_7 % 36.81/11.45 | % 36.81/11.45 | Combining equations (628,630) yields a new equation: % 36.81/11.45 | (639) all_203_1_148 = all_19_1_9 % 36.81/11.45 | % 36.81/11.45 | Simplifying 639 yields: % 36.81/11.45 | (640) all_203_1_148 = all_19_1_9 % 36.81/11.45 | % 36.81/11.45 | From (638) and (561) follows: % 36.81/11.45 | (69) apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7 % 36.81/11.45 | % 36.81/11.45 | From (640) and (544) follows: % 36.81/11.45 | (73) apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9 % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (23) with all_72_1_64, all_1_0_0, all_70_2_62, all_1_3_3, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_70_2_62) = all_72_1_64, yields: % 36.81/11.45 | (643) all_72_1_64 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_70_2_62) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (23) with all_1_0_0, all_72_1_64, all_1_3_3, all_70_2_62, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_70_2_62) = all_72_1_64, yields: % 36.81/11.45 | (644) all_72_1_64 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_70_2_62, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (28) with all_72_1_64, all_1_0_0, all_1_3_3, all_70_2_62, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_70_2_62) = all_72_1_64, yields: % 36.81/11.45 | (645) all_72_1_64 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_70_2_62, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (28) with all_1_0_0, all_72_1_64, all_70_2_62, all_1_3_3, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_70_2_62) = all_72_1_64, yields: % 36.81/11.45 | (646) all_72_1_64 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_70_2_62) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (16) with all_68_1_58, all_68_1_58, all_64_2_53, all_64_2_53, all_19_0_8, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, distinct_points(all_1_2_2, all_19_0_8) = 0, yields: % 36.81/11.45 | (647) all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_19_0_8, all_64_2_53) = v2 & apart_point_and_line(all_19_0_8, all_64_2_53) = v1 & distinct_lines(all_64_2_53, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (16) with all_68_1_58, all_68_1_58, all_64_2_53, all_64_2_53, all_17_0_6, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, distinct_points(all_1_2_2, all_17_0_6) = 0, yields: % 36.81/11.45 | (648) all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_17_0_6, all_64_2_53) = v2 & apart_point_and_line(all_17_0_6, all_64_2_53) = v1 & distinct_lines(all_64_2_53, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (16) with all_68_1_58, all_68_1_58, all_64_2_53, all_64_2_53, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 36.81/11.45 | (649) all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_64_2_53) = v1 & distinct_lines(all_64_2_53, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (23) with all_68_1_58, all_68_1_58, all_64_2_53, all_64_2_53, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, yields: % 36.81/11.45 | (650) all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_64_2_53) = v3 & apart_point_and_line(all_1_2_2, all_64_2_53) = v2 & distinct_lines(all_64_2_53, all_64_2_53) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (7) with all_82_2_80, all_1_5_5, all_1_3_3, all_1_5_5 and discharging atoms convergent_lines(all_1_3_3, all_1_5_5) = all_82_2_80, convergent_lines(all_1_5_5, all_1_3_3) = 0, ~ (convergent_lines(all_1_5_5, all_1_5_5) = 0), yields: % 36.81/11.45 | (651) all_82_2_80 = 0 % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (7) with all_80_2_77, all_1_5_5, all_1_4_4, all_1_5_5 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = all_80_2_77, convergent_lines(all_1_5_5, all_1_4_4) = 0, ~ (convergent_lines(all_1_5_5, all_1_5_5) = 0), yields: % 36.81/11.45 | (652) all_80_2_77 = 0 % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (12) with all_64_0_51, all_1_2_2, all_1_1_1, all_1_2_2 and discharging atoms distinct_points(all_1_1_1, all_1_2_2) = all_64_0_51, distinct_points(all_1_2_2, all_1_1_1) = 0, ~ (distinct_points(all_1_2_2, all_1_2_2) = 0), yields: % 36.81/11.45 | (653) all_64_0_51 = 0 % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (27) with all_68_1_58, all_17_1_7, all_64_2_53, all_1_4_4, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, yields: % 36.81/11.45 | (654) all_68_1_58 = 0 | all_17_1_7 = 0 | ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (27) with all_68_1_58, all_19_1_9, all_64_2_53, all_1_5_5, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_1_9, yields: % 36.81/11.45 | (655) all_68_1_58 = 0 | all_19_1_9 = 0 | ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (27) with all_68_1_58, all_72_1_64, all_64_2_53, all_70_2_62, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_2_2, all_70_2_62) = all_72_1_64, apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, yields: % 36.81/11.45 | (656) all_72_1_64 = 0 | all_68_1_58 = 0 | ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v1 & apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & distinct_lines(all_70_2_62, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (27) with all_68_1_58, all_74_1_67, all_64_2_53, all_66_2_56, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_2_2, all_66_2_56) = all_74_1_67, apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, yields: % 36.81/11.45 | (657) all_74_1_67 = 0 | all_68_1_58 = 0 | ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_66_2_56) = v1 & apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & distinct_lines(all_66_2_56, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (27) with all_68_1_58, all_68_1_58, all_64_2_53, all_64_2_53, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, yields: % 36.81/11.45 | (658) all_68_1_58 = 0 | ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_64_2_53) = v1 & distinct_lines(all_64_2_53, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (25) with all_35_3_22, all_1_1_1, all_1_2_2, all_1_1_1 and discharging atoms distinct_points(all_1_1_1, all_1_1_1) = all_35_3_22, yields: % 36.81/11.45 | (659) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) | ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_1_1, all_1_2_2) = v0 & apart_point_and_line(all_1_1_1, v0) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v2 & ( ~ (v1 = 0) | (v2 = 0 & all_35_3_22 = 0))) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (25) with 0, all_1_2_2, all_1_2_2, all_1_1_1 and discharging atoms distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 36.81/11.45 | (660) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) | ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_1_1, all_1_2_2) = v0 & apart_point_and_line(all_1_2_2, v0) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 36.81/11.45 | % 36.81/11.45 | Instantiating formula (16) with all_17_1_7, all_68_1_58, all_1_4_4, all_64_2_53, all_82_1_79, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_64_2_53) = all_68_1_58, apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_1_7, yields: % 36.81/11.45 | (661) all_68_1_58 = 0 | all_17_1_7 = 0 | ~ (distinct_points(all_1_2_2, all_82_1_79) = 0) | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_82_1_79, all_64_2_53) = v1 & apart_point_and_line(all_82_1_79, all_1_4_4) = v2 & distinct_lines(all_64_2_53, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 | Combining equations (652,382) yields a new equation: % 36.81/11.45 | (662) all_96_2_101 = 0 % 36.81/11.45 | % 36.81/11.45 | From (653) and (206) follows: % 36.81/11.45 | (663) distinct_points(all_1_1_1, all_1_2_2) = 0 % 36.81/11.45 | % 36.81/11.45 +-Applying beta-rule and splitting (659), into two cases. % 36.81/11.45 |-Branch one: % 36.81/11.45 | (664) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) % 36.81/11.45 | % 36.81/11.45 | Using (663) and (664) yields: % 36.81/11.45 | (518) $false % 36.81/11.45 | % 36.81/11.45 |-The branch is then unsatisfiable % 36.81/11.45 |-Branch two: % 36.81/11.45 | (663) distinct_points(all_1_1_1, all_1_2_2) = 0 % 36.81/11.45 | (667) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_1_1, all_1_2_2) = v0 & apart_point_and_line(all_1_1_1, v0) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v2 & ( ~ (v1 = 0) | (v2 = 0 & all_35_3_22 = 0))) % 36.81/11.45 | % 36.81/11.45 +-Applying beta-rule and splitting (660), into two cases. % 36.81/11.45 |-Branch one: % 36.81/11.45 | (664) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) % 36.81/11.45 | % 36.81/11.45 | Using (663) and (664) yields: % 36.81/11.45 | (518) $false % 36.81/11.45 | % 36.81/11.45 |-The branch is then unsatisfiable % 36.81/11.45 |-Branch two: % 36.81/11.45 | (663) distinct_points(all_1_1_1, all_1_2_2) = 0 % 36.81/11.45 | (671) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_1_1, all_1_2_2) = v0 & apart_point_and_line(all_1_2_2, v0) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 36.81/11.45 | % 36.81/11.45 +-Applying beta-rule and splitting (648), into two cases. % 36.81/11.45 |-Branch one: % 36.81/11.45 | (672) all_68_1_58 = 0 % 36.81/11.45 | % 36.81/11.45 | Equations (672) can reduce 602 to: % 36.81/11.45 | (92) $false % 36.81/11.45 | % 36.81/11.45 |-The branch is then unsatisfiable % 36.81/11.45 |-Branch two: % 36.81/11.45 | (602) ~ (all_68_1_58 = 0) % 36.81/11.45 | (675) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_17_0_6, all_64_2_53) = v2 & apart_point_and_line(all_17_0_6, all_64_2_53) = v1 & distinct_lines(all_64_2_53, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 +-Applying beta-rule and splitting (649), into two cases. % 36.81/11.45 |-Branch one: % 36.81/11.45 | (672) all_68_1_58 = 0 % 36.81/11.45 | % 36.81/11.45 | Equations (672) can reduce 602 to: % 36.81/11.45 | (92) $false % 36.81/11.45 | % 36.81/11.45 |-The branch is then unsatisfiable % 36.81/11.45 |-Branch two: % 36.81/11.45 | (602) ~ (all_68_1_58 = 0) % 36.81/11.45 | (679) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_64_2_53) = v1 & distinct_lines(all_64_2_53, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.45 | % 36.81/11.45 +-Applying beta-rule and splitting (650), into two cases. % 36.81/11.45 |-Branch one: % 36.81/11.45 | (672) all_68_1_58 = 0 % 36.81/11.45 | % 36.81/11.45 | Equations (672) can reduce 602 to: % 36.81/11.45 | (92) $false % 36.81/11.45 | % 36.81/11.45 |-The branch is then unsatisfiable % 36.81/11.45 |-Branch two: % 36.81/11.45 | (602) ~ (all_68_1_58 = 0) % 36.81/11.45 | (683) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_64_2_53) = v3 & apart_point_and_line(all_1_2_2, all_64_2_53) = v2 & distinct_lines(all_64_2_53, all_64_2_53) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.45 | % 36.81/11.45 +-Applying beta-rule and splitting (658), into two cases. % 36.81/11.45 |-Branch one: % 36.81/11.45 | (664) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) % 36.81/11.45 | % 36.81/11.45 | Using (663) and (664) yields: % 36.81/11.45 | (518) $false % 36.81/11.45 | % 36.81/11.45 |-The branch is then unsatisfiable % 36.81/11.45 |-Branch two: % 36.81/11.45 | (663) distinct_points(all_1_1_1, all_1_2_2) = 0 % 36.81/11.45 | (649) all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_64_2_53) = v1 & distinct_lines(all_64_2_53, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (643), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (688) all_72_1_64 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (688) can reduce 516 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (516) ~ (all_72_1_64 = 0) % 36.81/11.46 | (691) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_70_2_62) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (644), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (688) all_72_1_64 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (688) can reduce 516 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (516) ~ (all_72_1_64 = 0) % 36.81/11.46 | (695) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_70_2_62, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (645), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (688) all_72_1_64 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (688) can reduce 516 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (516) ~ (all_72_1_64 = 0) % 36.81/11.46 | (699) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_70_2_62, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (646), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (688) all_72_1_64 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (688) can reduce 516 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (516) ~ (all_72_1_64 = 0) % 36.81/11.46 | (703) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_70_2_62) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (654), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (664) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) % 36.81/11.46 | % 36.81/11.46 | Using (663) and (664) yields: % 36.81/11.46 | (518) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (663) distinct_points(all_1_1_1, all_1_2_2) = 0 % 36.81/11.46 | (707) all_68_1_58 = 0 | all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (655), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (664) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) % 36.81/11.46 | % 36.81/11.46 | Using (663) and (664) yields: % 36.81/11.46 | (518) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (663) distinct_points(all_1_1_1, all_1_2_2) = 0 % 36.81/11.46 | (711) all_68_1_58 = 0 | all_19_1_9 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (656), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (664) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) % 36.81/11.46 | % 36.81/11.46 | Using (663) and (664) yields: % 36.81/11.46 | (518) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (663) distinct_points(all_1_1_1, all_1_2_2) = 0 % 36.81/11.46 | (715) all_72_1_64 = 0 | all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v1 & apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & distinct_lines(all_70_2_62, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (657), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (664) ~ (distinct_points(all_1_1_1, all_1_2_2) = 0) % 36.81/11.46 | % 36.81/11.46 | Using (663) and (664) yields: % 36.81/11.46 | (518) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (663) distinct_points(all_1_1_1, all_1_2_2) = 0 % 36.81/11.46 | (719) all_74_1_67 = 0 | all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_66_2_56) = v1 & apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & distinct_lines(all_66_2_56, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (707), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (672) all_68_1_58 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (672) can reduce 602 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (602) ~ (all_68_1_58 = 0) % 36.81/11.46 | (723) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (711), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (672) all_68_1_58 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (672) can reduce 602 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (602) ~ (all_68_1_58 = 0) % 36.81/11.46 | (727) all_19_1_9 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (282), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (728) ~ (all_96_2_101 = 0) % 36.81/11.46 | % 36.81/11.46 | Equations (662) can reduce 728 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (662) all_96_2_101 = 0 % 36.81/11.46 | (731) all_96_0_99 = 0 | ( ~ (all_96_1_100 = 0) & ~ (all_23_2_15 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (715), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (688) all_72_1_64 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (688) can reduce 516 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (516) ~ (all_72_1_64 = 0) % 36.81/11.46 | (735) all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v1 & apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & distinct_lines(all_70_2_62, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (719), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (736) all_74_1_67 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (736) can reduce 524 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (524) ~ (all_74_1_67 = 0) % 36.81/11.46 | (739) all_68_1_58 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_66_2_56) = v1 & apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & distinct_lines(all_66_2_56, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (723), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (538) all_17_1_7 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (538) can reduce 535 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (535) ~ (all_17_1_7 = 0) % 36.81/11.46 | (743) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (727), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (547) all_19_1_9 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (547) can reduce 537 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (537) ~ (all_19_1_9 = 0) % 36.81/11.46 | (747) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (252), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (748) ~ (all_82_2_80 = 0) % 36.81/11.46 | % 36.81/11.46 | Equations (651) can reduce 748 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (651) all_82_2_80 = 0 % 36.81/11.46 | (751) all_82_0_78 = 0 % 36.81/11.46 | % 36.81/11.46 | From (751) and (251) follows: % 36.81/11.46 | (752) distinct_points(all_1_2_2, all_82_1_79) = 0 % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (731), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (753) all_96_0_99 = 0 % 36.81/11.46 | % 36.81/11.46 | Combining equations (753,420) yields a new equation: % 36.81/11.46 | (333) all_35_3_22 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (333) can reduce 113 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (392) ~ (all_96_0_99 = 0) % 36.81/11.46 | (757) ~ (all_96_1_100 = 0) & ~ (all_23_2_15 = 0) % 36.81/11.46 | % 36.81/11.46 | Applying alpha-rule on (757) yields: % 36.81/11.46 | (758) ~ (all_96_1_100 = 0) % 36.81/11.46 | (759) ~ (all_23_2_15 = 0) % 36.81/11.46 | % 36.81/11.46 | Equations (500) can reduce 758 to: % 36.81/11.46 | (760) ~ (all_21_2_12 = 0) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (661), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (761) ~ (distinct_points(all_1_2_2, all_82_1_79) = 0) % 36.81/11.46 | % 36.81/11.46 | Using (752) and (761) yields: % 36.81/11.46 | (518) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (752) distinct_points(all_1_2_2, all_82_1_79) = 0 % 36.81/11.46 | (764) all_68_1_58 = 0 | all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_82_1_79, all_64_2_53) = v1 & apart_point_and_line(all_82_1_79, all_1_4_4) = v2 & distinct_lines(all_64_2_53, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.46 | % 36.81/11.46 +-Applying beta-rule and splitting (735), into two cases. % 36.81/11.46 |-Branch one: % 36.81/11.46 | (672) all_68_1_58 = 0 % 36.81/11.46 | % 36.81/11.46 | Equations (672) can reduce 602 to: % 36.81/11.46 | (92) $false % 36.81/11.46 | % 36.81/11.46 |-The branch is then unsatisfiable % 36.81/11.46 |-Branch two: % 36.81/11.46 | (602) ~ (all_68_1_58 = 0) % 36.81/11.47 | (768) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_70_2_62) = v1 & apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & distinct_lines(all_70_2_62, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.47 | % 36.81/11.47 +-Applying beta-rule and splitting (739), into two cases. % 36.81/11.47 |-Branch one: % 36.81/11.47 | (672) all_68_1_58 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (672) can reduce 602 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (602) ~ (all_68_1_58 = 0) % 36.81/11.47 | (772) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_66_2_56) = v1 & apart_point_and_line(all_1_1_1, all_64_2_53) = v2 & distinct_lines(all_66_2_56, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.47 | % 36.81/11.47 +-Applying beta-rule and splitting (647), into two cases. % 36.81/11.47 |-Branch one: % 36.81/11.47 | (672) all_68_1_58 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (672) can reduce 602 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (602) ~ (all_68_1_58 = 0) % 36.81/11.47 | (776) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_19_0_8, all_64_2_53) = v2 & apart_point_and_line(all_19_0_8, all_64_2_53) = v1 & distinct_lines(all_64_2_53, all_64_2_53) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.47 | % 36.81/11.47 +-Applying beta-rule and splitting (764), into two cases. % 36.81/11.47 |-Branch one: % 36.81/11.47 | (672) all_68_1_58 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (672) can reduce 602 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (602) ~ (all_68_1_58 = 0) % 36.81/11.47 | (780) all_17_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_82_1_79, all_64_2_53) = v1 & apart_point_and_line(all_82_1_79, all_1_4_4) = v2 & distinct_lines(all_64_2_53, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.47 | % 36.81/11.47 +-Applying beta-rule and splitting (780), into two cases. % 36.81/11.47 |-Branch one: % 36.81/11.47 | (538) all_17_1_7 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (538) can reduce 535 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (535) ~ (all_17_1_7 = 0) % 36.81/11.47 | (784) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_82_1_79, all_64_2_53) = v1 & apart_point_and_line(all_82_1_79, all_1_4_4) = v2 & distinct_lines(all_64_2_53, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 36.81/11.47 | % 36.81/11.47 +-Applying beta-rule and splitting (166), into two cases. % 36.81/11.47 |-Branch one: % 36.81/11.47 | (785) all_50_0_23 = 0 % 36.81/11.47 | % 36.81/11.47 | Combining equations (450,785) yields a new equation: % 36.81/11.47 | (786) all_21_2_12 = 0 % 36.81/11.47 | % 36.81/11.47 | Simplifying 786 yields: % 36.81/11.47 | (787) all_21_2_12 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (787) can reduce 760 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (789) ~ (all_50_0_23 = 0) % 36.81/11.47 | (790) all_50_1_24 = 0 | all_50_2_25 = 0 | all_50_3_26 = 0 % 36.81/11.47 | % 36.81/11.47 +-Applying beta-rule and splitting (790), into two cases. % 36.81/11.47 |-Branch one: % 36.81/11.47 | (791) all_50_1_24 = 0 % 36.81/11.47 | % 36.81/11.47 | Combining equations (791,437) yields a new equation: % 36.81/11.47 | (792) all_23_2_15 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (792) can reduce 759 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (794) ~ (all_50_1_24 = 0) % 36.81/11.47 | (795) all_50_2_25 = 0 | all_50_3_26 = 0 % 36.81/11.47 | % 36.81/11.47 +-Applying beta-rule and splitting (795), into two cases. % 36.81/11.47 |-Branch one: % 36.81/11.47 | (796) all_50_2_25 = 0 % 36.81/11.47 | % 36.81/11.47 | Combining equations (490,796) yields a new equation: % 36.81/11.47 | (797) all_17_1_7 = 0 % 36.81/11.47 | % 36.81/11.47 | Simplifying 797 yields: % 36.81/11.47 | (538) all_17_1_7 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (538) can reduce 535 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (800) ~ (all_50_2_25 = 0) % 36.81/11.47 | (801) all_50_3_26 = 0 % 36.81/11.47 | % 36.81/11.47 | Combining equations (801,491) yields a new equation: % 36.81/11.47 | (547) all_19_1_9 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (547) can reduce 537 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (672) all_68_1_58 = 0 % 36.81/11.47 | (530) all_68_0_57 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (530) can reduce 503 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (736) all_74_1_67 = 0 % 36.81/11.47 | (808) all_74_0_66 = 0 % 36.81/11.47 | % 36.81/11.47 | Combining equations (468,808) yields a new equation: % 36.81/11.47 | (809) all_68_0_57 = 0 % 36.81/11.47 | % 36.81/11.47 | Simplifying 809 yields: % 36.81/11.47 | (530) all_68_0_57 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (530) can reduce 503 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (688) all_72_1_64 = 0 % 36.81/11.47 | (813) all_72_0_63 = 0 % 36.81/11.47 | % 36.81/11.47 | Combining equations (475,813) yields a new equation: % 36.81/11.47 | (809) all_68_0_57 = 0 % 36.81/11.47 | % 36.81/11.47 | Simplifying 809 yields: % 36.81/11.47 | (530) all_68_0_57 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (530) can reduce 503 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 |-Branch two: % 36.81/11.47 | (817) ~ (distinct_points(all_1_2_2, all_1_1_1) = 0) % 36.81/11.47 | (91) all_1_0_0 = 0 % 36.81/11.47 | % 36.81/11.47 | Equations (91) can reduce 48 to: % 36.81/11.47 | (92) $false % 36.81/11.47 | % 36.81/11.47 |-The branch is then unsatisfiable % 36.81/11.47 % SZS output end Proof for theBenchmark % 36.81/11.47 % 36.81/11.47 10832ms %------------------------------------------------------------------------------