%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GEO199+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n012.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:35 EDT 2022 % Result : Theorem 23.47s 7.20s % Output : Proof 32.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GEO199+2 : TPTP v8.1.0. Released v3.3.0. % 0.12/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n012.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sat Jun 18 01:40:38 EDT 2022 % 0.12/0.34 % CPUTime : % 0.65/0.63 ____ _ % 0.65/0.63 ___ / __ \_____(_)___ ________ __________ % 0.65/0.63 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.65/0.63 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.65/0.63 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.65/0.63 % 0.65/0.63 A Theorem Prover for First-Order Logic % 0.65/0.63 (ePrincess v.1.0) % 0.65/0.63 % 0.65/0.63 (c) Philipp Rümmer, 2009-2015 % 0.65/0.63 (c) Peter Backeman, 2014-2015 % 0.65/0.63 (contributions by Angelo Brillout, Peter Baumgartner) % 0.65/0.63 Free software under GNU Lesser General Public License (LGPL). % 0.65/0.63 Bug reports to peter@backeman.se % 0.65/0.63 % 0.65/0.63 For more information, visit http://user.uu.se/~petba168/breu/ % 0.65/0.63 % 0.65/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.70/0.70 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.58/1.00 Prover 0: Preprocessing ... % 1.90/1.13 Prover 0: Warning: ignoring some quantifiers % 1.90/1.15 Prover 0: Constructing countermodel ... % 2.87/1.44 Prover 0: gave up % 2.87/1.44 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 3.29/1.46 Prover 1: Preprocessing ... % 3.59/1.54 Prover 1: Constructing countermodel ... % 3.59/1.57 Prover 1: gave up % 3.59/1.57 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.59/1.59 Prover 2: Preprocessing ... % 4.27/1.69 Prover 2: Warning: ignoring some quantifiers % 4.27/1.70 Prover 2: Constructing countermodel ... % 4.89/1.86 Prover 2: gave up % 4.89/1.86 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 4.89/1.88 Prover 3: Preprocessing ... % 4.89/1.89 Prover 3: Warning: ignoring some quantifiers % 4.89/1.89 Prover 3: Constructing countermodel ... % 5.28/1.97 Prover 3: gave up % 5.28/1.97 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 5.65/1.99 Prover 4: Preprocessing ... % 5.65/2.05 Prover 4: Warning: ignoring some quantifiers % 5.65/2.05 Prover 4: Constructing countermodel ... % 10.47/3.18 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 10.47/3.20 Prover 5: Preprocessing ... % 10.99/3.28 Prover 5: Constructing countermodel ... % 23.47/7.20 Prover 5: proved (4016ms) % 23.47/7.20 Prover 4: stopped % 23.47/7.20 % 23.47/7.20 No countermodel exists, formula is valid % 23.47/7.20 % SZS status Theorem for theBenchmark % 23.47/7.20 % 23.47/7.20 Generating proof ... found it (size 298) % 31.86/9.87 % 31.86/9.87 % SZS output start Proof for theBenchmark % 31.86/9.87 Assumed formulas after preprocessing and simplification: % 31.86/9.87 | (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] : ( ~ (v4 = 0) & intersection_point(v1, v0) = v5 & intersection_point(v0, v1) = v3 & apart_point_and_line(v5, v2) = 0 & apart_point_and_line(v3, v2) = v4 & convergent_lines(v2, v1) = 0 & convergent_lines(v0, v2) = 0 & convergent_lines(v0, v1) = 0) % 32.27/9.93 | Applying alpha-rule on (0) yields: % 32.27/9.93 | (1) ! [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))))) % 32.43/9.93 | (2) ! [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))) % 32.43/9.93 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) % 32.43/9.93 | (4) ! [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)) % 32.43/9.93 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) % 32.43/9.93 | (6) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (distinct_lines(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3)) % 32.43/9.93 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) % 32.43/9.94 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) % 32.43/9.94 | (9) ! [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) % 32.43/9.94 | (10) ! [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)))) % 32.43/9.94 | (11) ! [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)) % 32.43/9.94 | (12) ! [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)))) % 32.43/9.94 | (13) ! [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)))) % 32.43/9.94 | (14) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v4 = 0) & intersection_point(v1, v0) = v5 & intersection_point(v0, v1) = v3 & apart_point_and_line(v5, v2) = 0 & apart_point_and_line(v3, v2) = v4 & convergent_lines(v2, v1) = 0 & convergent_lines(v0, v2) = 0 & convergent_lines(v0, v1) = 0) % 32.43/9.94 | (15) ! [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))) % 32.43/9.94 | (16) ! [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))) % 32.43/9.94 | (17) ! [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) % 32.43/9.94 | (18) ! [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))))) % 32.43/9.94 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 32.43/9.95 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 32.51/9.95 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) % 32.51/9.95 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) % 32.51/9.95 | (23) ! [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))))) % 32.51/9.95 | (24) ! [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))) % 32.51/9.95 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) % 32.51/9.95 | (26) ! [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)) % 32.51/9.95 | (27) ! [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))) % 32.51/9.95 | (28) ! [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) % 32.51/9.95 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) % 32.51/9.95 | (30) ! [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)) % 32.51/9.95 | (31) ! [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) % 32.51/9.95 | (32) ! [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))))) % 32.51/9.95 | (33) ! [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))))) % 32.51/9.95 | (34) ! [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)) % 32.51/9.95 | (35) ! [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))) % 32.51/9.95 | (36) ! [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)))) % 32.51/9.95 | (37) ! [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)))) % 32.51/9.96 | (38) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v0, v1) = 0) % 32.51/9.96 | (39) ! [v0] : ~ (distinct_points(v0, v0) = 0) % 32.51/9.96 | (40) ! [v0] : ~ (convergent_lines(v0, v0) = 0) % 32.51/9.96 | (41) ! [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)) % 32.51/9.96 | (42) ! [v0] : ~ (distinct_lines(v0, v0) = 0) % 32.51/9.96 | (43) ! [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))) % 32.51/9.96 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) % 32.51/9.96 | (45) ! [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))) % 32.51/9.96 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) % 32.51/9.96 | % 32.51/9.96 | Instantiating (14) 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: % 32.51/9.96 | (47) ~ (all_1_1_1 = 0) & intersection_point(all_1_4_4, all_1_5_5) = all_1_0_0 & intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2 & apart_point_and_line(all_1_0_0, all_1_3_3) = 0 & apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1 & 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 % 32.51/9.96 | % 32.51/9.96 | Applying alpha-rule on (47) yields: % 32.51/9.96 | (48) ~ (all_1_1_1 = 0) % 32.51/9.96 | (49) apart_point_and_line(all_1_0_0, all_1_3_3) = 0 % 32.51/9.96 | (50) convergent_lines(all_1_3_3, all_1_4_4) = 0 % 32.51/9.96 | (51) convergent_lines(all_1_5_5, all_1_4_4) = 0 % 32.51/9.96 | (52) apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1 % 32.51/9.96 | (53) intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2 % 32.51/9.96 | (54) intersection_point(all_1_4_4, all_1_5_5) = all_1_0_0 % 32.51/9.96 | (55) convergent_lines(all_1_5_5, all_1_3_3) = 0 % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (40) with all_1_5_5 yields: % 32.51/9.96 | (56) ~ (convergent_lines(all_1_5_5, all_1_5_5) = 0) % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (35) with 0, 0, all_1_0_0, all_1_3_3, all_1_3_3 and discharging atoms apart_point_and_line(all_1_0_0, all_1_3_3) = 0, yields: % 32.51/9.96 | (57) ? [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_0_0, v1) = v2 & ( ~ (v0 = 0) | v2 = 0)) % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (28) with all_1_1_1, all_1_2_2, all_1_3_3, all_1_0_0 and discharging atoms apart_point_and_line(all_1_0_0, all_1_3_3) = 0, apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1, yields: % 32.51/9.96 | (58) all_1_1_1 = 0 | distinct_points(all_1_0_0, all_1_2_2) = 0 % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (43) with all_1_1_1, all_1_1_1, all_1_3_3, all_1_3_3, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1, yields: % 32.51/9.96 | (59) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (23) with 0, all_1_0_0, all_1_4_4, all_1_3_3 and discharging atoms apart_point_and_line(all_1_0_0, all_1_3_3) = 0, convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 32.51/9.96 | (60) ? [v0] : ? [v1] : (intersection_point(all_1_3_3, all_1_4_4) = v1 & apart_point_and_line(all_1_0_0, all_1_4_4) = v0 & distinct_points(all_1_0_0, v1) = 0) % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (23) with all_1_1_1, 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) = all_1_1_1, convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 32.51/9.96 | (61) ? [v0] : ? [v1] : ? [v2] : (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) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_1_1_1 = 0)))) % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (38) with all_1_4_4, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 32.51/9.96 | (62) distinct_lines(all_1_3_3, all_1_4_4) = 0 % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (18) with 0, all_1_0_0, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_0_0, all_1_3_3) = 0, convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 32.51/9.96 | (63) ? [v0] : ? [v1] : (intersection_point(all_1_5_5, all_1_3_3) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v0 & distinct_points(all_1_0_0, v1) = 0) % 32.51/9.96 | % 32.51/9.96 | Instantiating formula (18) with all_1_1_1, 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) = all_1_1_1, convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 32.51/9.97 | (64) ? [v0] : ? [v1] : ? [v2] : (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) = v2 & (v2 = 0 | ( ~ (v0 = 0) & ~ (all_1_1_1 = 0)))) % 32.51/9.97 | % 32.51/9.97 | Instantiating formula (38) with all_1_3_3, all_1_5_5 and discharging atoms convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 32.51/9.97 | (65) distinct_lines(all_1_5_5, all_1_3_3) = 0 % 32.51/9.97 | % 32.51/9.97 | Instantiating formula (38) with all_1_4_4, all_1_5_5 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 32.51/9.97 | (66) distinct_lines(all_1_5_5, all_1_4_4) = 0 % 32.51/9.97 | % 32.51/9.97 | Instantiating (61) with all_17_0_6, all_17_1_7, all_17_2_8 yields: % 32.51/9.97 | (67) intersection_point(all_1_3_3, all_1_4_4) = all_17_1_7 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_2_8 & distinct_points(all_1_2_2, all_17_1_7) = all_17_0_6 & (all_17_0_6 = 0 | ( ~ (all_17_2_8 = 0) & ~ (all_1_1_1 = 0))) % 32.51/9.97 | % 32.51/9.97 | Applying alpha-rule on (67) yields: % 32.51/9.97 | (68) intersection_point(all_1_3_3, all_1_4_4) = all_17_1_7 % 32.51/9.97 | (69) apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_2_8 % 32.51/9.97 | (70) distinct_points(all_1_2_2, all_17_1_7) = all_17_0_6 % 32.51/9.97 | (71) all_17_0_6 = 0 | ( ~ (all_17_2_8 = 0) & ~ (all_1_1_1 = 0)) % 32.51/9.97 | % 32.51/9.97 | Instantiating (64) with all_19_0_9, all_19_1_10, all_19_2_11 yields: % 32.51/9.97 | (72) intersection_point(all_1_5_5, all_1_3_3) = all_19_1_10 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_2_11 & distinct_points(all_1_2_2, all_19_1_10) = all_19_0_9 & (all_19_0_9 = 0 | ( ~ (all_19_2_11 = 0) & ~ (all_1_1_1 = 0))) % 32.51/9.97 | % 32.51/9.97 | Applying alpha-rule on (72) yields: % 32.51/9.97 | (73) intersection_point(all_1_5_5, all_1_3_3) = all_19_1_10 % 32.51/9.97 | (74) apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_2_11 % 32.51/9.97 | (75) distinct_points(all_1_2_2, all_19_1_10) = all_19_0_9 % 32.51/9.97 | (76) all_19_0_9 = 0 | ( ~ (all_19_2_11 = 0) & ~ (all_1_1_1 = 0)) % 32.51/9.97 | % 32.51/9.97 | Instantiating (60) with all_21_0_12, all_21_1_13 yields: % 32.51/9.97 | (77) intersection_point(all_1_3_3, all_1_4_4) = all_21_0_12 & apart_point_and_line(all_1_0_0, all_1_4_4) = all_21_1_13 & distinct_points(all_1_0_0, all_21_0_12) = 0 % 32.51/9.97 | % 32.51/9.97 | Applying alpha-rule on (77) yields: % 32.51/9.97 | (78) intersection_point(all_1_3_3, all_1_4_4) = all_21_0_12 % 32.51/9.97 | (79) apart_point_and_line(all_1_0_0, all_1_4_4) = all_21_1_13 % 32.51/9.97 | (80) distinct_points(all_1_0_0, all_21_0_12) = 0 % 32.51/9.97 | % 32.51/9.97 | Instantiating (57) with all_23_0_14, all_23_1_15, all_23_2_16 yields: % 32.51/9.97 | (81) intersection_point(all_1_3_3, all_1_3_3) = all_23_1_15 & convergent_lines(all_1_3_3, all_1_3_3) = all_23_2_16 & distinct_points(all_1_0_0, all_23_1_15) = all_23_0_14 & ( ~ (all_23_2_16 = 0) | all_23_0_14 = 0) % 32.51/9.97 | % 32.51/9.97 | Applying alpha-rule on (81) yields: % 32.51/9.97 | (82) intersection_point(all_1_3_3, all_1_3_3) = all_23_1_15 % 32.51/9.97 | (83) convergent_lines(all_1_3_3, all_1_3_3) = all_23_2_16 % 32.51/9.97 | (84) distinct_points(all_1_0_0, all_23_1_15) = all_23_0_14 % 32.51/9.97 | (85) ~ (all_23_2_16 = 0) | all_23_0_14 = 0 % 32.51/9.97 | % 32.51/9.97 | Instantiating (63) with all_25_0_17, all_25_1_18 yields: % 32.51/9.97 | (86) intersection_point(all_1_5_5, all_1_3_3) = all_25_0_17 & apart_point_and_line(all_1_0_0, all_1_5_5) = all_25_1_18 & distinct_points(all_1_0_0, all_25_0_17) = 0 % 32.51/9.97 | % 32.51/9.97 | Applying alpha-rule on (86) yields: % 32.51/9.97 | (87) intersection_point(all_1_5_5, all_1_3_3) = all_25_0_17 % 32.51/9.97 | (88) apart_point_and_line(all_1_0_0, all_1_5_5) = all_25_1_18 % 32.51/9.97 | (89) distinct_points(all_1_0_0, all_25_0_17) = 0 % 32.51/9.97 | % 32.51/9.97 +-Applying beta-rule and splitting (58), into two cases. % 32.51/9.97 |-Branch one: % 32.51/9.97 | (90) distinct_points(all_1_0_0, all_1_2_2) = 0 % 32.51/9.97 | % 32.51/9.97 +-Applying beta-rule and splitting (59), into two cases. % 32.51/9.97 |-Branch one: % 32.51/9.97 | (91) all_1_1_1 = 0 % 32.51/9.97 | % 32.51/9.97 | Equations (91) can reduce 48 to: % 32.51/9.97 | (92) $false % 32.51/9.97 | % 32.51/9.97 |-The branch is then unsatisfiable % 32.51/9.97 |-Branch two: % 32.51/9.97 | (48) ~ (all_1_1_1 = 0) % 32.51/9.97 | (94) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 32.51/9.97 | % 32.51/9.97 | Instantiating (94) with all_35_0_19, all_35_1_20, all_35_2_21, all_35_3_22 yields: % 32.51/9.97 | (95) apart_point_and_line(all_1_2_2, all_1_3_3) = all_35_0_19 & apart_point_and_line(all_1_2_2, 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_2_2, all_1_2_2) = all_35_3_22 & ( ~ (all_35_2_21 = 0) | ~ (all_35_3_22 = 0) | all_35_0_19 = 0 | all_35_1_20 = 0) % 32.51/9.97 | % 32.51/9.97 | Applying alpha-rule on (95) yields: % 32.51/9.97 | (96) distinct_lines(all_1_3_3, all_1_3_3) = all_35_2_21 % 32.51/9.97 | (97) ~ (all_35_2_21 = 0) | ~ (all_35_3_22 = 0) | all_35_0_19 = 0 | all_35_1_20 = 0 % 32.51/9.97 | (98) apart_point_and_line(all_1_2_2, all_1_3_3) = all_35_0_19 % 32.51/9.97 | (99) apart_point_and_line(all_1_2_2, all_1_3_3) = all_35_1_20 % 32.51/9.97 | (100) distinct_points(all_1_2_2, all_1_2_2) = all_35_3_22 % 32.51/9.97 | % 32.51/9.97 | Instantiating formula (3) with all_1_3_3, all_1_4_4, all_17_1_7, all_21_0_12 and discharging atoms intersection_point(all_1_3_3, all_1_4_4) = all_21_0_12, intersection_point(all_1_3_3, all_1_4_4) = all_17_1_7, yields: % 32.51/9.97 | (101) all_21_0_12 = all_17_1_7 % 32.51/9.97 | % 32.51/9.97 | Instantiating formula (3) with all_1_5_5, all_1_3_3, all_19_1_10, all_25_0_17 and discharging atoms intersection_point(all_1_5_5, all_1_3_3) = all_25_0_17, intersection_point(all_1_5_5, all_1_3_3) = all_19_1_10, yields: % 32.51/9.97 | (102) all_25_0_17 = all_19_1_10 % 32.51/9.97 | % 32.51/9.97 | Instantiating formula (21) with all_1_2_2, all_1_3_3, all_35_0_19, all_1_1_1 and discharging atoms apart_point_and_line(all_1_2_2, all_1_3_3) = all_35_0_19, apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1, yields: % 32.51/9.97 | (103) all_35_0_19 = all_1_1_1 % 32.51/9.97 | % 32.51/9.97 | Instantiating formula (21) with all_1_2_2, all_1_3_3, all_35_1_20, all_35_0_19 and discharging atoms apart_point_and_line(all_1_2_2, all_1_3_3) = all_35_0_19, apart_point_and_line(all_1_2_2, all_1_3_3) = all_35_1_20, yields: % 32.51/9.97 | (104) all_35_0_19 = all_35_1_20 % 32.51/9.97 | % 32.51/9.97 | Instantiating formula (40) with all_1_3_3 yields: % 32.51/9.97 | (105) ~ (convergent_lines(all_1_3_3, all_1_3_3) = 0) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (39) with all_1_0_0 yields: % 32.51/9.98 | (106) ~ (distinct_points(all_1_0_0, all_1_0_0) = 0) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (39) with all_1_2_2 yields: % 32.51/9.98 | (107) ~ (distinct_points(all_1_2_2, all_1_2_2) = 0) % 32.51/9.98 | % 32.51/9.98 | Combining equations (103,104) yields a new equation: % 32.51/9.98 | (108) all_35_1_20 = all_1_1_1 % 32.51/9.98 | % 32.51/9.98 | From (101) and (78) follows: % 32.51/9.98 | (68) intersection_point(all_1_3_3, all_1_4_4) = all_17_1_7 % 32.51/9.98 | % 32.51/9.98 | From (102) and (87) follows: % 32.51/9.98 | (73) intersection_point(all_1_5_5, all_1_3_3) = all_19_1_10 % 32.51/9.98 | % 32.51/9.98 | From (108) and (99) follows: % 32.51/9.98 | (52) apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1 % 32.51/9.98 | % 32.51/9.98 | From (102) and (89) follows: % 32.51/9.98 | (112) distinct_points(all_1_0_0, all_19_1_10) = 0 % 32.51/9.98 | % 32.51/9.98 | From (101) and (80) follows: % 32.51/9.98 | (113) distinct_points(all_1_0_0, all_17_1_7) = 0 % 32.51/9.98 | % 32.51/9.98 | Using (83) and (105) yields: % 32.51/9.98 | (114) ~ (all_23_2_16 = 0) % 32.51/9.98 | % 32.51/9.98 | Using (100) and (107) yields: % 32.51/9.98 | (115) ~ (all_35_3_22 = 0) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (33) with all_17_1_7, all_1_1_1, all_1_2_2, all_1_4_4, all_1_3_3 and discharging atoms intersection_point(all_1_3_3, all_1_4_4) = all_17_1_7, apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1, yields: % 32.51/9.98 | (116) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & convergent_lines(all_1_3_3, all_1_4_4) = v0 & distinct_points(all_1_2_2, all_17_1_7) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_1_1 = 0)))) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (32) with all_19_1_10, all_1_1_1, all_1_2_2, all_1_3_3, all_1_5_5 and discharging atoms intersection_point(all_1_5_5, all_1_3_3) = all_19_1_10, apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1, yields: % 32.51/9.98 | (117) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_5_5) = v1 & convergent_lines(all_1_5_5, all_1_3_3) = v0 & distinct_points(all_1_2_2, all_19_1_10) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_1_1 = 0)))) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (35) with 0, all_21_1_13, all_1_0_0, all_1_3_3, all_1_4_4 and discharging atoms apart_point_and_line(all_1_0_0, all_1_3_3) = 0, apart_point_and_line(all_1_0_0, all_1_4_4) = all_21_1_13, yields: % 32.51/9.98 | (118) ? [v0] : ? [v1] : ? [v2] : (intersection_point(all_1_4_4, all_1_3_3) = v1 & convergent_lines(all_1_4_4, all_1_3_3) = v0 & distinct_points(all_1_0_0, v1) = v2 & ( ~ (v0 = 0) | v2 = 0)) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (33) with all_1_0_0, all_21_1_13, all_1_0_0, all_1_5_5, all_1_4_4 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_1_0_0, apart_point_and_line(all_1_0_0, all_1_4_4) = all_21_1_13, yields: % 32.51/9.98 | (119) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_1_5_5) = v1 & convergent_lines(all_1_4_4, all_1_5_5) = v0 & distinct_points(all_1_0_0, all_1_0_0) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_21_1_13 = 0)))) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (32) with all_1_0_0, all_25_1_18, all_1_0_0, all_1_5_5, all_1_4_4 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_1_0_0, apart_point_and_line(all_1_0_0, all_1_5_5) = all_25_1_18, yields: % 32.51/9.98 | (120) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_1_4_4) = v1 & convergent_lines(all_1_4_4, all_1_5_5) = v0 & distinct_points(all_1_0_0, all_1_0_0) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_25_1_18 = 0)))) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (43) with all_17_2_8, all_17_2_8, 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_2_8, yields: % 32.51/9.98 | (121) all_17_2_8 = 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)) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (33) with all_1_0_0, all_17_2_8, 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_0_0, apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_2_8, yields: % 32.51/9.98 | (122) ? [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_0_0) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_17_2_8 = 0)))) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (32) with all_1_2_2, all_17_2_8, 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_2_8, yields: % 32.51/9.98 | (123) ? [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_2_8 = 0)))) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (18) with all_17_2_8, 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_2_8, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 32.51/9.98 | (124) ? [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_2_8 = 0)))) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (43) with all_19_2_11, all_1_1_1, all_1_5_5, all_1_3_3, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_3_3) = all_1_1_1, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_2_11, yields: % 32.51/9.98 | (125) all_19_2_11 = 0 | all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & apart_point_and_line(all_1_2_2, all_1_5_5) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 32.51/9.98 | % 32.51/9.98 | Instantiating formula (43) with all_19_2_11, all_17_2_8, 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_2_8, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_2_11, yields: % 32.51/9.99 | (126) all_19_2_11 = 0 | all_17_2_8 = 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)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (32) with all_1_0_0, all_19_2_11, 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_0_0, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_2_11, yields: % 32.51/9.99 | (127) ? [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_0_0) = v2 & ( ~ (v0 = 0) | v2 = 0 | ( ~ (v1 = 0) & ~ (all_19_2_11 = 0)))) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (33) with all_1_2_2, all_19_2_11, 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_2_11, yields: % 32.51/9.99 | (128) ? [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_2_11 = 0)))) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (23) with all_19_2_11, 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_2_11, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 32.51/9.99 | (129) ? [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_2_11 = 0)))) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (25) with all_23_2_16, all_1_3_3, all_1_4_4, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_3_3) = all_23_2_16, convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 32.51/9.99 | (130) all_23_2_16 = 0 | convergent_lines(all_1_4_4, all_1_3_3) = 0 % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (36) with 0, all_1_0_0, all_19_1_10, all_1_0_0 and discharging atoms distinct_points(all_1_0_0, all_19_1_10) = 0, yields: % 32.51/9.99 | (131) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_0_0, all_19_1_10) = v0 & apart_point_and_line(all_1_0_0, v0) = v1 & distinct_points(all_1_0_0, all_1_0_0) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (15) with all_1_3_3, all_1_5_5, all_19_1_10, all_1_0_0 and discharging atoms distinct_lines(all_1_5_5, all_1_3_3) = 0, distinct_points(all_1_0_0, all_19_1_10) = 0, yields: % 32.51/9.99 | (132) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_19_1_10, all_1_3_3) = v3 & apart_point_and_line(all_19_1_10, all_1_5_5) = v2 & apart_point_and_line(all_1_0_0, all_1_3_3) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (15) with all_1_4_4, all_1_5_5, all_19_1_10, all_1_0_0 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = 0, distinct_points(all_1_0_0, all_19_1_10) = 0, yields: % 32.51/9.99 | (133) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_19_1_10, all_1_4_4) = v3 & apart_point_and_line(all_19_1_10, all_1_5_5) = v2 & apart_point_and_line(all_1_0_0, all_1_4_4) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (36) with 0, all_1_0_0, all_17_1_7, all_1_0_0 and discharging atoms distinct_points(all_1_0_0, all_17_1_7) = 0, yields: % 32.51/9.99 | (134) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_0_0, all_17_1_7) = v0 & apart_point_and_line(all_1_0_0, v0) = v1 & distinct_points(all_1_0_0, all_1_0_0) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (15) with all_1_4_4, all_1_3_3, all_17_1_7, all_1_0_0 and discharging atoms distinct_lines(all_1_3_3, all_1_4_4) = 0, distinct_points(all_1_0_0, all_17_1_7) = 0, yields: % 32.51/9.99 | (135) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_17_1_7, all_1_3_3) = v2 & apart_point_and_line(all_17_1_7, all_1_4_4) = v3 & apart_point_and_line(all_1_0_0, all_1_3_3) = v0 & apart_point_and_line(all_1_0_0, all_1_4_4) = v1 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (15) with all_1_3_3, all_1_5_5, all_17_1_7, all_1_0_0 and discharging atoms distinct_lines(all_1_5_5, all_1_3_3) = 0, distinct_points(all_1_0_0, all_17_1_7) = 0, yields: % 32.51/9.99 | (136) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_17_1_7, all_1_3_3) = v3 & apart_point_and_line(all_17_1_7, all_1_5_5) = v2 & apart_point_and_line(all_1_0_0, all_1_3_3) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (15) with all_1_4_4, all_1_5_5, all_17_1_7, all_1_0_0 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = 0, distinct_points(all_1_0_0, all_17_1_7) = 0, yields: % 32.51/9.99 | (137) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_17_1_7, all_1_4_4) = v3 & apart_point_and_line(all_17_1_7, all_1_5_5) = v2 & apart_point_and_line(all_1_0_0, all_1_4_4) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v0 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (36) with 0, all_1_0_0, all_1_2_2, all_1_0_0 and discharging atoms distinct_points(all_1_0_0, all_1_2_2) = 0, yields: % 32.51/9.99 | (138) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_0_0, all_1_2_2) = v0 & apart_point_and_line(all_1_0_0, v0) = v1 & distinct_points(all_1_0_0, all_1_0_0) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (16) with all_19_2_11, all_17_2_8, all_1_5_5, all_1_4_4, all_1_2_2, all_1_0_0 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_2_8, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_2_11, distinct_points(all_1_0_0, all_1_2_2) = 0, yields: % 32.51/9.99 | (139) all_19_2_11 = 0 | all_17_2_8 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_1_4_4) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (16) with all_19_2_11, all_19_2_11, all_1_5_5, all_1_5_5, all_1_2_2, all_1_0_0 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_2_11, distinct_points(all_1_0_0, all_1_2_2) = 0, yields: % 32.51/9.99 | (140) all_19_2_11 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_1_5_5) = v2 & apart_point_and_line(all_1_0_0, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (15) with all_1_4_4, all_1_5_5, all_1_2_2, all_1_0_0 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = 0, distinct_points(all_1_0_0, all_1_2_2) = 0, yields: % 32.51/9.99 | (141) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_0_0, all_1_4_4) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v0 & 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 & (v3 = 0 | v2 = 0 | v1 = 0 | v0 = 0)) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (41) with all_35_3_22, all_35_3_22, all_1_2_2, all_1_2_2, all_1_2_2 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_35_3_22, yields: % 32.51/9.99 | (142) all_35_3_22 = 0 | ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_1_2_2) = v1 & apart_point_and_line(all_1_2_2, v1) = v2 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 32.51/9.99 | % 32.51/9.99 | Instantiating formula (1) with all_35_3_22, all_1_2_2, 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, distinct_points(all_1_2_2, all_1_2_2) = all_35_3_22, yields: % 32.51/9.99 | (143) all_35_3_22 = 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_5_5) = v1 & convergent_lines(all_1_5_5, all_1_4_4) = v0 & ( ~ (v0 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) % 32.51/9.99 | % 32.51/9.99 | Instantiating (132) with all_52_0_26, all_52_1_27, all_52_2_28, all_52_3_29 yields: % 32.51/9.99 | (144) apart_point_and_line(all_19_1_10, all_1_3_3) = all_52_0_26 & apart_point_and_line(all_19_1_10, all_1_5_5) = all_52_1_27 & apart_point_and_line(all_1_0_0, all_1_3_3) = all_52_2_28 & apart_point_and_line(all_1_0_0, all_1_5_5) = all_52_3_29 & (all_52_0_26 = 0 | all_52_1_27 = 0 | all_52_2_28 = 0 | all_52_3_29 = 0) % 32.51/9.99 | % 32.51/10.00 | Applying alpha-rule on (144) yields: % 32.51/10.00 | (145) all_52_0_26 = 0 | all_52_1_27 = 0 | all_52_2_28 = 0 | all_52_3_29 = 0 % 32.51/10.00 | (146) apart_point_and_line(all_1_0_0, all_1_5_5) = all_52_3_29 % 32.51/10.00 | (147) apart_point_and_line(all_19_1_10, all_1_3_3) = all_52_0_26 % 32.51/10.00 | (148) apart_point_and_line(all_1_0_0, all_1_3_3) = all_52_2_28 % 32.51/10.00 | (149) apart_point_and_line(all_19_1_10, all_1_5_5) = all_52_1_27 % 32.51/10.00 | % 32.51/10.00 | Instantiating (141) with all_60_0_40, all_60_1_41, all_60_2_42, all_60_3_43 yields: % 32.51/10.00 | (150) apart_point_and_line(all_1_0_0, all_1_4_4) = all_60_2_42 & apart_point_and_line(all_1_0_0, all_1_5_5) = all_60_3_43 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_60_0_40 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_60_1_41 & (all_60_0_40 = 0 | all_60_1_41 = 0 | all_60_2_42 = 0 | all_60_3_43 = 0) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (150) yields: % 32.51/10.00 | (151) all_60_0_40 = 0 | all_60_1_41 = 0 | all_60_2_42 = 0 | all_60_3_43 = 0 % 32.51/10.00 | (152) apart_point_and_line(all_1_0_0, all_1_5_5) = all_60_3_43 % 32.51/10.00 | (153) apart_point_and_line(all_1_0_0, all_1_4_4) = all_60_2_42 % 32.51/10.00 | (154) apart_point_and_line(all_1_2_2, all_1_5_5) = all_60_1_41 % 32.51/10.00 | (155) apart_point_and_line(all_1_2_2, all_1_4_4) = all_60_0_40 % 32.51/10.00 | % 32.51/10.00 | Instantiating (138) with all_62_0_44, all_62_1_45, all_62_2_46 yields: % 32.51/10.00 | (156) line_connecting(all_1_0_0, all_1_2_2) = all_62_2_46 & apart_point_and_line(all_1_0_0, all_62_2_46) = all_62_1_45 & distinct_points(all_1_0_0, all_1_0_0) = all_62_0_44 & ( ~ (all_62_1_45 = 0) | all_62_0_44 = 0) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (156) yields: % 32.51/10.00 | (157) line_connecting(all_1_0_0, all_1_2_2) = all_62_2_46 % 32.51/10.00 | (158) apart_point_and_line(all_1_0_0, all_62_2_46) = all_62_1_45 % 32.51/10.00 | (159) distinct_points(all_1_0_0, all_1_0_0) = all_62_0_44 % 32.51/10.00 | (160) ~ (all_62_1_45 = 0) | all_62_0_44 = 0 % 32.51/10.00 | % 32.51/10.00 | Instantiating (137) with all_64_0_47, all_64_1_48, all_64_2_49, all_64_3_50 yields: % 32.51/10.00 | (161) apart_point_and_line(all_17_1_7, all_1_4_4) = all_64_0_47 & apart_point_and_line(all_17_1_7, all_1_5_5) = all_64_1_48 & apart_point_and_line(all_1_0_0, all_1_4_4) = all_64_2_49 & apart_point_and_line(all_1_0_0, all_1_5_5) = all_64_3_50 & (all_64_0_47 = 0 | all_64_1_48 = 0 | all_64_2_49 = 0 | all_64_3_50 = 0) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (161) yields: % 32.51/10.00 | (162) apart_point_and_line(all_1_0_0, all_1_4_4) = all_64_2_49 % 32.51/10.00 | (163) apart_point_and_line(all_17_1_7, all_1_4_4) = all_64_0_47 % 32.51/10.00 | (164) apart_point_and_line(all_1_0_0, all_1_5_5) = all_64_3_50 % 32.51/10.00 | (165) apart_point_and_line(all_17_1_7, all_1_5_5) = all_64_1_48 % 32.51/10.00 | (166) all_64_0_47 = 0 | all_64_1_48 = 0 | all_64_2_49 = 0 | all_64_3_50 = 0 % 32.51/10.00 | % 32.51/10.00 | Instantiating (136) with all_66_0_51, all_66_1_52, all_66_2_53, all_66_3_54 yields: % 32.51/10.00 | (167) apart_point_and_line(all_17_1_7, all_1_3_3) = all_66_0_51 & apart_point_and_line(all_17_1_7, all_1_5_5) = all_66_1_52 & apart_point_and_line(all_1_0_0, all_1_3_3) = all_66_2_53 & apart_point_and_line(all_1_0_0, all_1_5_5) = all_66_3_54 & (all_66_0_51 = 0 | all_66_1_52 = 0 | all_66_2_53 = 0 | all_66_3_54 = 0) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (167) yields: % 32.51/10.00 | (168) apart_point_and_line(all_17_1_7, all_1_3_3) = all_66_0_51 % 32.51/10.00 | (169) apart_point_and_line(all_1_0_0, all_1_5_5) = all_66_3_54 % 32.51/10.00 | (170) apart_point_and_line(all_1_0_0, all_1_3_3) = all_66_2_53 % 32.51/10.00 | (171) apart_point_and_line(all_17_1_7, all_1_5_5) = all_66_1_52 % 32.51/10.00 | (172) all_66_0_51 = 0 | all_66_1_52 = 0 | all_66_2_53 = 0 | all_66_3_54 = 0 % 32.51/10.00 | % 32.51/10.00 | Instantiating (123) with all_68_0_55, all_68_1_56, all_68_2_57 yields: % 32.51/10.00 | (173) apart_point_and_line(all_1_2_2, all_1_5_5) = all_68_1_56 & convergent_lines(all_1_5_5, all_1_4_4) = all_68_2_57 & distinct_points(all_1_2_2, all_1_2_2) = all_68_0_55 & ( ~ (all_68_2_57 = 0) | all_68_0_55 = 0 | ( ~ (all_68_1_56 = 0) & ~ (all_17_2_8 = 0))) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (173) yields: % 32.51/10.00 | (174) apart_point_and_line(all_1_2_2, all_1_5_5) = all_68_1_56 % 32.51/10.00 | (175) convergent_lines(all_1_5_5, all_1_4_4) = all_68_2_57 % 32.51/10.00 | (176) distinct_points(all_1_2_2, all_1_2_2) = all_68_0_55 % 32.51/10.00 | (177) ~ (all_68_2_57 = 0) | all_68_0_55 = 0 | ( ~ (all_68_1_56 = 0) & ~ (all_17_2_8 = 0)) % 32.51/10.00 | % 32.51/10.00 | Instantiating (120) with all_70_0_58, all_70_1_59, all_70_2_60 yields: % 32.51/10.00 | (178) apart_point_and_line(all_1_0_0, all_1_4_4) = all_70_1_59 & convergent_lines(all_1_4_4, all_1_5_5) = all_70_2_60 & distinct_points(all_1_0_0, all_1_0_0) = all_70_0_58 & ( ~ (all_70_2_60 = 0) | all_70_0_58 = 0 | ( ~ (all_70_1_59 = 0) & ~ (all_25_1_18 = 0))) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (178) yields: % 32.51/10.00 | (179) apart_point_and_line(all_1_0_0, all_1_4_4) = all_70_1_59 % 32.51/10.00 | (180) convergent_lines(all_1_4_4, all_1_5_5) = all_70_2_60 % 32.51/10.00 | (181) distinct_points(all_1_0_0, all_1_0_0) = all_70_0_58 % 32.51/10.00 | (182) ~ (all_70_2_60 = 0) | all_70_0_58 = 0 | ( ~ (all_70_1_59 = 0) & ~ (all_25_1_18 = 0)) % 32.51/10.00 | % 32.51/10.00 | Instantiating (131) with all_72_0_61, all_72_1_62, all_72_2_63 yields: % 32.51/10.00 | (183) line_connecting(all_1_0_0, all_19_1_10) = all_72_2_63 & apart_point_and_line(all_1_0_0, all_72_2_63) = all_72_1_62 & distinct_points(all_1_0_0, all_1_0_0) = all_72_0_61 & ( ~ (all_72_1_62 = 0) | all_72_0_61 = 0) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (183) yields: % 32.51/10.00 | (184) line_connecting(all_1_0_0, all_19_1_10) = all_72_2_63 % 32.51/10.00 | (185) apart_point_and_line(all_1_0_0, all_72_2_63) = all_72_1_62 % 32.51/10.00 | (186) distinct_points(all_1_0_0, all_1_0_0) = all_72_0_61 % 32.51/10.00 | (187) ~ (all_72_1_62 = 0) | all_72_0_61 = 0 % 32.51/10.00 | % 32.51/10.00 | Instantiating (122) with all_74_0_64, all_74_1_65, all_74_2_66 yields: % 32.51/10.00 | (188) apart_point_and_line(all_1_2_2, all_1_5_5) = all_74_1_65 & convergent_lines(all_1_4_4, all_1_5_5) = all_74_2_66 & distinct_points(all_1_2_2, all_1_0_0) = all_74_0_64 & ( ~ (all_74_2_66 = 0) | all_74_0_64 = 0 | ( ~ (all_74_1_65 = 0) & ~ (all_17_2_8 = 0))) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (188) yields: % 32.51/10.00 | (189) apart_point_and_line(all_1_2_2, all_1_5_5) = all_74_1_65 % 32.51/10.00 | (190) convergent_lines(all_1_4_4, all_1_5_5) = all_74_2_66 % 32.51/10.00 | (191) distinct_points(all_1_2_2, all_1_0_0) = all_74_0_64 % 32.51/10.00 | (192) ~ (all_74_2_66 = 0) | all_74_0_64 = 0 | ( ~ (all_74_1_65 = 0) & ~ (all_17_2_8 = 0)) % 32.51/10.00 | % 32.51/10.00 | Instantiating (129) with all_78_0_70, all_78_1_71, all_78_2_72 yields: % 32.51/10.00 | (193) intersection_point(all_1_5_5, all_1_4_4) = all_78_1_71 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_78_2_72 & distinct_points(all_1_2_2, all_78_1_71) = all_78_0_70 & (all_78_0_70 = 0 | ( ~ (all_78_2_72 = 0) & ~ (all_19_2_11 = 0))) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (193) yields: % 32.51/10.00 | (194) intersection_point(all_1_5_5, all_1_4_4) = all_78_1_71 % 32.51/10.00 | (195) apart_point_and_line(all_1_2_2, all_1_4_4) = all_78_2_72 % 32.51/10.00 | (196) distinct_points(all_1_2_2, all_78_1_71) = all_78_0_70 % 32.51/10.00 | (197) all_78_0_70 = 0 | ( ~ (all_78_2_72 = 0) & ~ (all_19_2_11 = 0)) % 32.51/10.00 | % 32.51/10.00 | Instantiating (124) with all_82_0_76, all_82_1_77, all_82_2_78 yields: % 32.51/10.00 | (198) intersection_point(all_1_5_5, all_1_4_4) = all_82_1_77 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_82_2_78 & distinct_points(all_1_2_2, all_82_1_77) = all_82_0_76 & (all_82_0_76 = 0 | ( ~ (all_82_2_78 = 0) & ~ (all_17_2_8 = 0))) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (198) yields: % 32.51/10.00 | (199) intersection_point(all_1_5_5, all_1_4_4) = all_82_1_77 % 32.51/10.00 | (200) apart_point_and_line(all_1_2_2, all_1_5_5) = all_82_2_78 % 32.51/10.00 | (201) distinct_points(all_1_2_2, all_82_1_77) = all_82_0_76 % 32.51/10.00 | (202) all_82_0_76 = 0 | ( ~ (all_82_2_78 = 0) & ~ (all_17_2_8 = 0)) % 32.51/10.00 | % 32.51/10.00 | Instantiating (128) with all_90_0_88, all_90_1_89, all_90_2_90 yields: % 32.51/10.00 | (203) apart_point_and_line(all_1_2_2, all_1_4_4) = all_90_1_89 & convergent_lines(all_1_5_5, all_1_4_4) = all_90_2_90 & distinct_points(all_1_2_2, all_1_2_2) = all_90_0_88 & ( ~ (all_90_2_90 = 0) | all_90_0_88 = 0 | ( ~ (all_90_1_89 = 0) & ~ (all_19_2_11 = 0))) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (203) yields: % 32.51/10.00 | (204) apart_point_and_line(all_1_2_2, all_1_4_4) = all_90_1_89 % 32.51/10.00 | (205) convergent_lines(all_1_5_5, all_1_4_4) = all_90_2_90 % 32.51/10.00 | (206) distinct_points(all_1_2_2, all_1_2_2) = all_90_0_88 % 32.51/10.00 | (207) ~ (all_90_2_90 = 0) | all_90_0_88 = 0 | ( ~ (all_90_1_89 = 0) & ~ (all_19_2_11 = 0)) % 32.51/10.00 | % 32.51/10.00 | Instantiating (135) with all_92_0_91, all_92_1_92, all_92_2_93, all_92_3_94 yields: % 32.51/10.00 | (208) apart_point_and_line(all_17_1_7, all_1_3_3) = all_92_1_92 & apart_point_and_line(all_17_1_7, all_1_4_4) = all_92_0_91 & apart_point_and_line(all_1_0_0, all_1_3_3) = all_92_3_94 & apart_point_and_line(all_1_0_0, all_1_4_4) = all_92_2_93 & (all_92_0_91 = 0 | all_92_1_92 = 0 | all_92_2_93 = 0 | all_92_3_94 = 0) % 32.51/10.00 | % 32.51/10.00 | Applying alpha-rule on (208) yields: % 32.51/10.00 | (209) all_92_0_91 = 0 | all_92_1_92 = 0 | all_92_2_93 = 0 | all_92_3_94 = 0 % 32.51/10.00 | (210) apart_point_and_line(all_17_1_7, all_1_4_4) = all_92_0_91 % 32.51/10.00 | (211) apart_point_and_line(all_1_0_0, all_1_3_3) = all_92_3_94 % 32.51/10.00 | (212) apart_point_and_line(all_1_0_0, all_1_4_4) = all_92_2_93 % 32.51/10.00 | (213) apart_point_and_line(all_17_1_7, all_1_3_3) = all_92_1_92 % 32.51/10.00 | % 32.51/10.00 | Instantiating (134) with all_94_0_95, all_94_1_96, all_94_2_97 yields: % 32.51/10.00 | (214) line_connecting(all_1_0_0, all_17_1_7) = all_94_2_97 & apart_point_and_line(all_1_0_0, all_94_2_97) = all_94_1_96 & distinct_points(all_1_0_0, all_1_0_0) = all_94_0_95 & ( ~ (all_94_1_96 = 0) | all_94_0_95 = 0) % 32.51/10.01 | % 32.51/10.01 | Applying alpha-rule on (214) yields: % 32.51/10.01 | (215) line_connecting(all_1_0_0, all_17_1_7) = all_94_2_97 % 32.51/10.01 | (216) apart_point_and_line(all_1_0_0, all_94_2_97) = all_94_1_96 % 32.51/10.01 | (217) distinct_points(all_1_0_0, all_1_0_0) = all_94_0_95 % 32.51/10.01 | (218) ~ (all_94_1_96 = 0) | all_94_0_95 = 0 % 32.51/10.01 | % 32.51/10.01 | Instantiating (133) with all_96_0_98, all_96_1_99, all_96_2_100, all_96_3_101 yields: % 32.51/10.01 | (219) apart_point_and_line(all_19_1_10, all_1_4_4) = all_96_0_98 & apart_point_and_line(all_19_1_10, all_1_5_5) = all_96_1_99 & apart_point_and_line(all_1_0_0, all_1_4_4) = all_96_2_100 & apart_point_and_line(all_1_0_0, all_1_5_5) = all_96_3_101 & (all_96_0_98 = 0 | all_96_1_99 = 0 | all_96_2_100 = 0 | all_96_3_101 = 0) % 32.51/10.01 | % 32.51/10.01 | Applying alpha-rule on (219) yields: % 32.51/10.01 | (220) all_96_0_98 = 0 | all_96_1_99 = 0 | all_96_2_100 = 0 | all_96_3_101 = 0 % 32.51/10.01 | (221) apart_point_and_line(all_1_0_0, all_1_5_5) = all_96_3_101 % 32.51/10.01 | (222) apart_point_and_line(all_19_1_10, all_1_4_4) = all_96_0_98 % 32.51/10.01 | (223) apart_point_and_line(all_19_1_10, all_1_5_5) = all_96_1_99 % 32.51/10.01 | (224) apart_point_and_line(all_1_0_0, all_1_4_4) = all_96_2_100 % 32.51/10.01 | % 32.51/10.01 | Instantiating (127) with all_98_0_102, all_98_1_103, all_98_2_104 yields: % 32.51/10.01 | (225) apart_point_and_line(all_1_2_2, all_1_4_4) = all_98_1_103 & convergent_lines(all_1_4_4, all_1_5_5) = all_98_2_104 & distinct_points(all_1_2_2, all_1_0_0) = all_98_0_102 & ( ~ (all_98_2_104 = 0) | all_98_0_102 = 0 | ( ~ (all_98_1_103 = 0) & ~ (all_19_2_11 = 0))) % 32.51/10.01 | % 32.51/10.01 | Applying alpha-rule on (225) yields: % 32.51/10.01 | (226) apart_point_and_line(all_1_2_2, all_1_4_4) = all_98_1_103 % 32.51/10.01 | (227) convergent_lines(all_1_4_4, all_1_5_5) = all_98_2_104 % 32.51/10.01 | (228) distinct_points(all_1_2_2, all_1_0_0) = all_98_0_102 % 32.51/10.01 | (229) ~ (all_98_2_104 = 0) | all_98_0_102 = 0 | ( ~ (all_98_1_103 = 0) & ~ (all_19_2_11 = 0)) % 32.51/10.01 | % 32.51/10.01 | Instantiating (119) with all_100_0_105, all_100_1_106, all_100_2_107 yields: % 32.51/10.01 | (230) apart_point_and_line(all_1_0_0, all_1_5_5) = all_100_1_106 & convergent_lines(all_1_4_4, all_1_5_5) = all_100_2_107 & distinct_points(all_1_0_0, all_1_0_0) = all_100_0_105 & ( ~ (all_100_2_107 = 0) | all_100_0_105 = 0 | ( ~ (all_100_1_106 = 0) & ~ (all_21_1_13 = 0))) % 32.51/10.01 | % 32.51/10.01 | Applying alpha-rule on (230) yields: % 32.51/10.01 | (231) apart_point_and_line(all_1_0_0, all_1_5_5) = all_100_1_106 % 32.51/10.01 | (232) convergent_lines(all_1_4_4, all_1_5_5) = all_100_2_107 % 32.51/10.01 | (233) distinct_points(all_1_0_0, all_1_0_0) = all_100_0_105 % 32.51/10.01 | (234) ~ (all_100_2_107 = 0) | all_100_0_105 = 0 | ( ~ (all_100_1_106 = 0) & ~ (all_21_1_13 = 0)) % 32.51/10.01 | % 32.51/10.01 | Instantiating (118) with all_102_0_108, all_102_1_109, all_102_2_110 yields: % 32.51/10.01 | (235) intersection_point(all_1_4_4, all_1_3_3) = all_102_1_109 & convergent_lines(all_1_4_4, all_1_3_3) = all_102_2_110 & distinct_points(all_1_0_0, all_102_1_109) = all_102_0_108 & ( ~ (all_102_2_110 = 0) | all_102_0_108 = 0) % 32.51/10.01 | % 32.51/10.01 | Applying alpha-rule on (235) yields: % 32.51/10.01 | (236) intersection_point(all_1_4_4, all_1_3_3) = all_102_1_109 % 32.51/10.01 | (237) convergent_lines(all_1_4_4, all_1_3_3) = all_102_2_110 % 32.51/10.01 | (238) distinct_points(all_1_0_0, all_102_1_109) = all_102_0_108 % 32.51/10.01 | (239) ~ (all_102_2_110 = 0) | all_102_0_108 = 0 % 32.51/10.01 | % 32.51/10.01 | Instantiating (116) with all_104_0_111, all_104_1_112, all_104_2_113 yields: % 32.51/10.01 | (240) apart_point_and_line(all_1_2_2, all_1_4_4) = all_104_1_112 & convergent_lines(all_1_3_3, all_1_4_4) = all_104_2_113 & distinct_points(all_1_2_2, all_17_1_7) = all_104_0_111 & ( ~ (all_104_2_113 = 0) | all_104_0_111 = 0 | ( ~ (all_104_1_112 = 0) & ~ (all_1_1_1 = 0))) % 32.51/10.01 | % 32.51/10.01 | Applying alpha-rule on (240) yields: % 32.51/10.01 | (241) apart_point_and_line(all_1_2_2, all_1_4_4) = all_104_1_112 % 32.51/10.01 | (242) convergent_lines(all_1_3_3, all_1_4_4) = all_104_2_113 % 32.51/10.01 | (243) distinct_points(all_1_2_2, all_17_1_7) = all_104_0_111 % 32.51/10.01 | (244) ~ (all_104_2_113 = 0) | all_104_0_111 = 0 | ( ~ (all_104_1_112 = 0) & ~ (all_1_1_1 = 0)) % 32.51/10.01 | % 32.51/10.01 | Instantiating (117) with all_108_0_117, all_108_1_118, all_108_2_119 yields: % 32.51/10.01 | (245) apart_point_and_line(all_1_2_2, all_1_5_5) = all_108_1_118 & convergent_lines(all_1_5_5, all_1_3_3) = all_108_2_119 & distinct_points(all_1_2_2, all_19_1_10) = all_108_0_117 & ( ~ (all_108_2_119 = 0) | all_108_0_117 = 0 | ( ~ (all_108_1_118 = 0) & ~ (all_1_1_1 = 0))) % 32.51/10.01 | % 32.51/10.01 | Applying alpha-rule on (245) yields: % 32.51/10.01 | (246) apart_point_and_line(all_1_2_2, all_1_5_5) = all_108_1_118 % 32.51/10.01 | (247) convergent_lines(all_1_5_5, all_1_3_3) = all_108_2_119 % 32.51/10.01 | (248) distinct_points(all_1_2_2, all_19_1_10) = all_108_0_117 % 32.51/10.01 | (249) ~ (all_108_2_119 = 0) | all_108_0_117 = 0 | ( ~ (all_108_1_118 = 0) & ~ (all_1_1_1 = 0)) % 32.51/10.01 | % 32.51/10.01 +-Applying beta-rule and splitting (142), into two cases. % 32.51/10.01 |-Branch one: % 32.51/10.01 | (250) all_35_3_22 = 0 % 32.51/10.01 | % 32.51/10.01 | Equations (250) can reduce 115 to: % 32.51/10.01 | (92) $false % 32.51/10.01 | % 32.51/10.01 |-The branch is then unsatisfiable % 32.51/10.01 |-Branch two: % 32.51/10.01 | (115) ~ (all_35_3_22 = 0) % 32.51/10.01 | (253) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_1_2_2) = v1 & apart_point_and_line(all_1_2_2, v1) = v2 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 32.51/10.01 | % 32.51/10.01 | Instantiating (253) with all_121_0_123, all_121_1_124, all_121_2_125 yields: % 32.51/10.01 | (254) line_connecting(all_1_2_2, all_1_2_2) = all_121_1_124 & apart_point_and_line(all_1_2_2, all_121_1_124) = all_121_0_123 & distinct_points(all_1_2_2, all_1_2_2) = all_121_2_125 & ( ~ (all_121_0_123 = 0) | ~ (all_121_2_125 = 0)) % 32.51/10.01 | % 32.51/10.01 | Applying alpha-rule on (254) yields: % 32.51/10.01 | (255) line_connecting(all_1_2_2, all_1_2_2) = all_121_1_124 % 32.51/10.01 | (256) apart_point_and_line(all_1_2_2, all_121_1_124) = all_121_0_123 % 32.51/10.01 | (257) distinct_points(all_1_2_2, all_1_2_2) = all_121_2_125 % 32.51/10.01 | (258) ~ (all_121_0_123 = 0) | ~ (all_121_2_125 = 0) % 32.51/10.01 | % 32.51/10.01 +-Applying beta-rule and splitting (130), into two cases. % 32.51/10.01 |-Branch one: % 32.51/10.01 | (259) convergent_lines(all_1_4_4, all_1_3_3) = 0 % 32.51/10.01 | % 32.51/10.01 | Instantiating formula (3) with all_1_5_5, all_1_4_4, all_82_1_77, all_1_2_2 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_82_1_77, intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2, yields: % 32.51/10.01 | (260) all_82_1_77 = all_1_2_2 % 32.51/10.01 | % 32.51/10.01 | Instantiating formula (3) with all_1_5_5, all_1_4_4, all_78_1_71, all_82_1_77 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_82_1_77, intersection_point(all_1_5_5, all_1_4_4) = all_78_1_71, yields: % 32.51/10.01 | (261) all_82_1_77 = all_78_1_71 % 32.51/10.01 | % 32.51/10.01 | Instantiating formula (21) with all_1_0_0, all_1_4_4, all_92_2_93, all_96_2_100 and discharging atoms apart_point_and_line(all_1_0_0, all_1_4_4) = all_96_2_100, apart_point_and_line(all_1_0_0, all_1_4_4) = all_92_2_93, yields: % 32.51/10.01 | (262) all_96_2_100 = all_92_2_93 % 32.51/10.01 | % 32.51/10.01 | Instantiating formula (21) with all_1_0_0, all_1_4_4, all_70_1_59, all_92_2_93 and discharging atoms apart_point_and_line(all_1_0_0, all_1_4_4) = all_92_2_93, apart_point_and_line(all_1_0_0, all_1_4_4) = all_70_1_59, yields: % 32.51/10.01 | (263) all_92_2_93 = all_70_1_59 % 32.51/10.01 | % 32.51/10.01 | Instantiating formula (21) with all_1_0_0, all_1_4_4, all_64_2_49, all_21_1_13 and discharging atoms apart_point_and_line(all_1_0_0, all_1_4_4) = all_64_2_49, apart_point_and_line(all_1_0_0, all_1_4_4) = all_21_1_13, yields: % 32.51/10.01 | (264) all_64_2_49 = all_21_1_13 % 32.51/10.01 | % 32.51/10.01 | Instantiating formula (21) with all_1_0_0, all_1_4_4, all_64_2_49, all_70_1_59 and discharging atoms apart_point_and_line(all_1_0_0, all_1_4_4) = all_70_1_59, apart_point_and_line(all_1_0_0, all_1_4_4) = all_64_2_49, yields: % 32.51/10.01 | (265) all_70_1_59 = all_64_2_49 % 32.51/10.01 | % 32.51/10.01 | Instantiating formula (21) with all_1_0_0, all_1_4_4, all_60_2_42, all_96_2_100 and discharging atoms apart_point_and_line(all_1_0_0, all_1_4_4) = all_96_2_100, apart_point_and_line(all_1_0_0, all_1_4_4) = all_60_2_42, yields: % 32.51/10.01 | (266) all_96_2_100 = all_60_2_42 % 32.51/10.01 | % 32.51/10.01 | Instantiating formula (21) with all_1_0_0, all_1_5_5, all_96_3_101, all_100_1_106 and discharging atoms apart_point_and_line(all_1_0_0, all_1_5_5) = all_100_1_106, apart_point_and_line(all_1_0_0, all_1_5_5) = all_96_3_101, yields: % 32.85/10.01 | (267) all_100_1_106 = all_96_3_101 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_0_0, all_1_5_5, all_66_3_54, all_100_1_106 and discharging atoms apart_point_and_line(all_1_0_0, all_1_5_5) = all_100_1_106, apart_point_and_line(all_1_0_0, all_1_5_5) = all_66_3_54, yields: % 32.85/10.01 | (268) all_100_1_106 = all_66_3_54 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_0_0, all_1_5_5, all_64_3_50, all_25_1_18 and discharging atoms apart_point_and_line(all_1_0_0, all_1_5_5) = all_64_3_50, apart_point_and_line(all_1_0_0, all_1_5_5) = all_25_1_18, yields: % 32.85/10.01 | (269) all_64_3_50 = all_25_1_18 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_0_0, all_1_5_5, all_64_3_50, all_66_3_54 and discharging atoms apart_point_and_line(all_1_0_0, all_1_5_5) = all_66_3_54, apart_point_and_line(all_1_0_0, all_1_5_5) = all_64_3_50, yields: % 32.85/10.01 | (270) all_66_3_54 = all_64_3_50 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_0_0, all_1_5_5, all_60_3_43, all_100_1_106 and discharging atoms apart_point_and_line(all_1_0_0, all_1_5_5) = all_100_1_106, apart_point_and_line(all_1_0_0, all_1_5_5) = all_60_3_43, yields: % 32.85/10.01 | (271) all_100_1_106 = all_60_3_43 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_0_0, all_1_5_5, all_52_3_29, all_64_3_50 and discharging atoms apart_point_and_line(all_1_0_0, all_1_5_5) = all_64_3_50, apart_point_and_line(all_1_0_0, all_1_5_5) = all_52_3_29, yields: % 32.85/10.01 | (272) all_64_3_50 = all_52_3_29 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_2_2, all_1_4_4, all_104_1_112, all_17_2_8 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_104_1_112, apart_point_and_line(all_1_2_2, all_1_4_4) = all_17_2_8, yields: % 32.85/10.01 | (273) all_104_1_112 = all_17_2_8 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_2_2, all_1_4_4, all_98_1_103, all_104_1_112 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_104_1_112, apart_point_and_line(all_1_2_2, all_1_4_4) = all_98_1_103, yields: % 32.85/10.01 | (274) all_104_1_112 = all_98_1_103 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_2_2, all_1_4_4, all_90_1_89, all_98_1_103 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_98_1_103, apart_point_and_line(all_1_2_2, all_1_4_4) = all_90_1_89, yields: % 32.85/10.01 | (275) all_98_1_103 = all_90_1_89 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_2_2, all_1_4_4, all_78_2_72, all_90_1_89 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_90_1_89, apart_point_and_line(all_1_2_2, all_1_4_4) = all_78_2_72, yields: % 32.85/10.01 | (276) all_90_1_89 = all_78_2_72 % 32.85/10.01 | % 32.85/10.01 | Instantiating formula (21) with all_1_2_2, all_1_4_4, all_60_0_40, all_78_2_72 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_78_2_72, apart_point_and_line(all_1_2_2, all_1_4_4) = all_60_0_40, yields: % 32.85/10.02 | (277) all_78_2_72 = all_60_0_40 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (21) with all_1_2_2, all_1_5_5, all_82_2_78, all_108_1_118 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_108_1_118, apart_point_and_line(all_1_2_2, all_1_5_5) = all_82_2_78, yields: % 32.85/10.02 | (278) all_108_1_118 = all_82_2_78 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (21) with all_1_2_2, all_1_5_5, all_74_1_65, all_19_2_11 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_74_1_65, apart_point_and_line(all_1_2_2, all_1_5_5) = all_19_2_11, yields: % 32.85/10.02 | (279) all_74_1_65 = all_19_2_11 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (21) with all_1_2_2, all_1_5_5, all_74_1_65, all_82_2_78 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_82_2_78, apart_point_and_line(all_1_2_2, all_1_5_5) = all_74_1_65, yields: % 32.85/10.02 | (280) all_82_2_78 = all_74_1_65 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (21) with all_1_2_2, all_1_5_5, all_68_1_56, all_108_1_118 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_108_1_118, apart_point_and_line(all_1_2_2, all_1_5_5) = all_68_1_56, yields: % 32.85/10.02 | (281) all_108_1_118 = all_68_1_56 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (21) with all_1_2_2, all_1_5_5, all_60_1_41, all_74_1_65 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_74_1_65, apart_point_and_line(all_1_2_2, all_1_5_5) = all_60_1_41, yields: % 32.85/10.02 | (282) all_74_1_65 = all_60_1_41 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (22) with all_1_4_4, all_1_3_3, 0, all_102_2_110 and discharging atoms convergent_lines(all_1_4_4, all_1_3_3) = all_102_2_110, convergent_lines(all_1_4_4, all_1_3_3) = 0, yields: % 32.85/10.02 | (283) all_102_2_110 = 0 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (22) with all_1_4_4, all_1_5_5, all_98_2_104, all_100_2_107 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = all_100_2_107, convergent_lines(all_1_4_4, all_1_5_5) = all_98_2_104, yields: % 32.85/10.02 | (284) all_100_2_107 = all_98_2_104 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (22) with all_1_4_4, all_1_5_5, all_74_2_66, all_100_2_107 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = all_100_2_107, convergent_lines(all_1_4_4, all_1_5_5) = all_74_2_66, yields: % 32.85/10.02 | (285) all_100_2_107 = all_74_2_66 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (22) with all_1_4_4, all_1_5_5, all_70_2_60, all_98_2_104 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = all_98_2_104, convergent_lines(all_1_4_4, all_1_5_5) = all_70_2_60, yields: % 32.85/10.02 | (286) all_98_2_104 = all_70_2_60 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (22) with all_1_5_5, all_1_4_4, all_90_2_90, 0 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_90_2_90, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 32.85/10.02 | (287) all_90_2_90 = 0 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (22) with all_1_5_5, all_1_4_4, all_68_2_57, all_90_2_90 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_90_2_90, convergent_lines(all_1_5_5, all_1_4_4) = all_68_2_57, yields: % 32.85/10.02 | (288) all_90_2_90 = all_68_2_57 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (46) with all_1_0_0, all_1_0_0, all_94_0_95, all_100_0_105 and discharging atoms distinct_points(all_1_0_0, all_1_0_0) = all_100_0_105, distinct_points(all_1_0_0, all_1_0_0) = all_94_0_95, yields: % 32.85/10.02 | (289) all_100_0_105 = all_94_0_95 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (46) with all_1_0_0, all_1_0_0, all_72_0_61, all_100_0_105 and discharging atoms distinct_points(all_1_0_0, all_1_0_0) = all_100_0_105, distinct_points(all_1_0_0, all_1_0_0) = all_72_0_61, yields: % 32.85/10.02 | (290) all_100_0_105 = all_72_0_61 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (46) with all_1_0_0, all_1_0_0, all_70_0_58, all_100_0_105 and discharging atoms distinct_points(all_1_0_0, all_1_0_0) = all_100_0_105, distinct_points(all_1_0_0, all_1_0_0) = all_70_0_58, yields: % 32.85/10.02 | (291) all_100_0_105 = all_70_0_58 % 32.85/10.02 | % 32.85/10.02 | Using (181) and (106) yields: % 32.85/10.02 | (292) ~ (all_70_0_58 = 0) % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (46) with all_1_0_0, all_1_0_0, all_62_0_44, all_72_0_61 and discharging atoms distinct_points(all_1_0_0, all_1_0_0) = all_72_0_61, distinct_points(all_1_0_0, all_1_0_0) = all_62_0_44, yields: % 32.85/10.02 | (293) all_72_0_61 = all_62_0_44 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (46) with all_1_2_2, all_1_2_2, all_121_2_125, all_78_0_70 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_121_2_125, yields: % 32.85/10.02 | (294) all_121_2_125 = all_78_0_70 | ~ (distinct_points(all_1_2_2, all_1_2_2) = all_78_0_70) % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (46) with all_1_2_2, all_1_2_2, all_90_0_88, all_35_3_22 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_90_0_88, distinct_points(all_1_2_2, all_1_2_2) = all_35_3_22, yields: % 32.85/10.02 | (295) all_90_0_88 = all_35_3_22 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (46) with all_1_2_2, all_1_2_2, all_90_0_88, all_121_2_125 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_121_2_125, distinct_points(all_1_2_2, all_1_2_2) = all_90_0_88, yields: % 32.85/10.02 | (296) all_121_2_125 = all_90_0_88 % 32.85/10.02 | % 32.85/10.02 | Instantiating formula (46) with all_1_2_2, all_1_2_2, all_68_0_55, all_121_2_125 and discharging atoms distinct_points(all_1_2_2, all_1_2_2) = all_121_2_125, distinct_points(all_1_2_2, all_1_2_2) = all_68_0_55, yields: % 32.85/10.02 | (297) all_121_2_125 = all_68_0_55 % 32.85/10.02 | % 32.85/10.02 | Using (176) and (107) yields: % 32.85/10.02 | (298) ~ (all_68_0_55 = 0) % 32.85/10.02 | % 32.85/10.02 | Combining equations (296,297) yields a new equation: % 32.85/10.02 | (299) all_90_0_88 = all_68_0_55 % 32.85/10.02 | % 32.85/10.02 | Simplifying 299 yields: % 32.85/10.02 | (300) all_90_0_88 = all_68_0_55 % 32.85/10.02 | % 32.85/10.02 | Combining equations (278,281) yields a new equation: % 32.85/10.02 | (301) all_82_2_78 = all_68_1_56 % 32.85/10.02 | % 32.85/10.02 | Simplifying 301 yields: % 32.85/10.02 | (302) all_82_2_78 = all_68_1_56 % 32.85/10.02 | % 32.85/10.02 | Combining equations (274,273) yields a new equation: % 32.85/10.02 | (303) all_98_1_103 = all_17_2_8 % 32.85/10.02 | % 32.85/10.02 | Simplifying 303 yields: % 32.85/10.02 | (304) all_98_1_103 = all_17_2_8 % 32.85/10.02 | % 32.85/10.02 | Combining equations (291,289) yields a new equation: % 32.85/10.02 | (305) all_94_0_95 = all_70_0_58 % 32.85/10.02 | % 32.85/10.02 | Combining equations (290,289) yields a new equation: % 32.85/10.02 | (306) all_94_0_95 = all_72_0_61 % 32.85/10.02 | % 32.85/10.02 | Combining equations (271,267) yields a new equation: % 32.85/10.02 | (307) all_96_3_101 = all_60_3_43 % 32.85/10.02 | % 32.85/10.02 | Combining equations (268,267) yields a new equation: % 32.85/10.02 | (308) all_96_3_101 = all_66_3_54 % 32.85/10.02 | % 32.85/10.02 | Combining equations (284,285) yields a new equation: % 32.85/10.02 | (309) all_98_2_104 = all_74_2_66 % 32.85/10.02 | % 32.85/10.02 | Simplifying 309 yields: % 32.85/10.02 | (310) all_98_2_104 = all_74_2_66 % 32.85/10.02 | % 32.85/10.02 | Combining equations (275,304) yields a new equation: % 32.85/10.02 | (311) all_90_1_89 = all_17_2_8 % 32.85/10.02 | % 32.85/10.02 | Simplifying 311 yields: % 32.85/10.02 | (312) all_90_1_89 = all_17_2_8 % 32.85/10.02 | % 32.85/10.02 | Combining equations (310,286) yields a new equation: % 32.85/10.02 | (313) all_74_2_66 = all_70_2_60 % 32.85/10.02 | % 32.85/10.02 | Simplifying 313 yields: % 32.85/10.02 | (314) all_74_2_66 = all_70_2_60 % 32.85/10.02 | % 32.85/10.02 | Combining equations (262,266) yields a new equation: % 32.85/10.02 | (315) all_92_2_93 = all_60_2_42 % 32.85/10.02 | % 32.85/10.02 | Simplifying 315 yields: % 32.85/10.02 | (316) all_92_2_93 = all_60_2_42 % 32.85/10.02 | % 32.85/10.02 | Combining equations (308,307) yields a new equation: % 32.85/10.02 | (317) all_66_3_54 = all_60_3_43 % 32.85/10.02 | % 32.85/10.02 | Simplifying 317 yields: % 32.85/10.02 | (318) all_66_3_54 = all_60_3_43 % 32.85/10.02 | % 32.85/10.02 | Combining equations (306,305) yields a new equation: % 32.85/10.02 | (319) all_72_0_61 = all_70_0_58 % 32.85/10.02 | % 32.85/10.02 | Simplifying 319 yields: % 32.85/10.02 | (320) all_72_0_61 = all_70_0_58 % 32.85/10.02 | % 32.85/10.02 | Combining equations (263,316) yields a new equation: % 32.85/10.02 | (321) all_70_1_59 = all_60_2_42 % 32.85/10.02 | % 32.85/10.02 | Simplifying 321 yields: % 32.85/10.02 | (322) all_70_1_59 = all_60_2_42 % 32.85/10.02 | % 32.85/10.02 | Combining equations (295,300) yields a new equation: % 32.85/10.02 | (323) all_68_0_55 = all_35_3_22 % 32.85/10.02 | % 32.85/10.02 | Combining equations (276,312) yields a new equation: % 32.85/10.02 | (324) all_78_2_72 = all_17_2_8 % 32.85/10.02 | % 32.85/10.02 | Simplifying 324 yields: % 32.85/10.02 | (325) all_78_2_72 = all_17_2_8 % 32.85/10.02 | % 32.85/10.02 | Combining equations (288,287) yields a new equation: % 32.85/10.02 | (326) all_68_2_57 = 0 % 32.85/10.02 | % 32.85/10.02 | Simplifying 326 yields: % 32.85/10.02 | (327) all_68_2_57 = 0 % 32.85/10.02 | % 32.85/10.02 | Combining equations (260,261) yields a new equation: % 32.85/10.02 | (328) all_78_1_71 = all_1_2_2 % 32.85/10.02 | % 32.85/10.02 | Combining equations (280,302) yields a new equation: % 32.85/10.02 | (329) all_74_1_65 = all_68_1_56 % 32.85/10.02 | % 32.85/10.02 | Simplifying 329 yields: % 32.85/10.02 | (330) all_74_1_65 = all_68_1_56 % 32.85/10.02 | % 32.85/10.02 | Combining equations (277,325) yields a new equation: % 32.85/10.02 | (331) all_60_0_40 = all_17_2_8 % 32.85/10.02 | % 32.85/10.02 | Simplifying 331 yields: % 32.85/10.02 | (332) all_60_0_40 = all_17_2_8 % 32.85/10.02 | % 32.85/10.02 | Combining equations (282,330) yields a new equation: % 32.85/10.02 | (333) all_68_1_56 = all_60_1_41 % 32.85/10.02 | % 32.85/10.02 | Combining equations (279,330) yields a new equation: % 32.85/10.02 | (334) all_68_1_56 = all_19_2_11 % 32.85/10.02 | % 32.85/10.02 | Combining equations (293,320) yields a new equation: % 32.85/10.02 | (335) all_70_0_58 = all_62_0_44 % 32.85/10.02 | % 32.85/10.02 | Combining equations (265,322) yields a new equation: % 32.85/10.02 | (336) all_64_2_49 = all_60_2_42 % 32.85/10.02 | % 32.85/10.02 | Simplifying 336 yields: % 32.85/10.02 | (337) all_64_2_49 = all_60_2_42 % 32.85/10.02 | % 32.85/10.02 | Combining equations (334,333) yields a new equation: % 32.85/10.02 | (338) all_60_1_41 = all_19_2_11 % 32.85/10.02 | % 32.85/10.02 | Combining equations (270,318) yields a new equation: % 32.85/10.02 | (339) all_64_3_50 = all_60_3_43 % 32.85/10.02 | % 32.85/10.02 | Simplifying 339 yields: % 32.85/10.02 | (340) all_64_3_50 = all_60_3_43 % 32.85/10.02 | % 32.85/10.02 | Combining equations (264,337) yields a new equation: % 32.85/10.02 | (341) all_60_2_42 = all_21_1_13 % 32.85/10.02 | % 32.85/10.02 | Combining equations (272,340) yields a new equation: % 32.85/10.02 | (342) all_60_3_43 = all_52_3_29 % 32.85/10.02 | % 32.85/10.02 | Combining equations (269,340) yields a new equation: % 32.85/10.02 | (343) all_60_3_43 = all_25_1_18 % 32.85/10.02 | % 32.85/10.02 | Combining equations (343,342) yields a new equation: % 32.85/10.02 | (344) all_52_3_29 = all_25_1_18 % 32.85/10.02 | % 32.85/10.02 | Combining equations (344,342) yields a new equation: % 32.85/10.02 | (343) all_60_3_43 = all_25_1_18 % 32.85/10.02 | % 32.85/10.03 | Combining equations (341,322) yields a new equation: % 32.85/10.03 | (346) all_70_1_59 = all_21_1_13 % 32.85/10.03 | % 32.85/10.03 | Combining equations (323,297) yields a new equation: % 32.85/10.03 | (347) all_121_2_125 = all_35_3_22 % 32.85/10.03 | % 32.85/10.03 | Equations (335) can reduce 292 to: % 32.85/10.03 | (348) ~ (all_62_0_44 = 0) % 32.85/10.03 | % 32.85/10.03 | Equations (323) can reduce 298 to: % 32.85/10.03 | (115) ~ (all_35_3_22 = 0) % 32.85/10.03 | % 32.85/10.03 | From (314) and (190) follows: % 32.85/10.03 | (180) convergent_lines(all_1_4_4, all_1_5_5) = all_70_2_60 % 32.85/10.03 | % 32.85/10.03 | From (327) and (175) follows: % 32.85/10.03 | (51) convergent_lines(all_1_5_5, all_1_4_4) = 0 % 32.85/10.03 | % 32.85/10.03 | From (335) and (181) follows: % 32.85/10.03 | (159) distinct_points(all_1_0_0, all_1_0_0) = all_62_0_44 % 32.85/10.03 | % 32.85/10.03 | From (328) and (196) follows: % 32.85/10.03 | (353) distinct_points(all_1_2_2, all_1_2_2) = all_78_0_70 % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (143), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (250) all_35_3_22 = 0 % 32.85/10.03 | % 32.85/10.03 | Equations (250) can reduce 115 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (115) ~ (all_35_3_22 = 0) % 32.85/10.03 | (357) ? [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_5_5) = v1 & convergent_lines(all_1_5_5, all_1_4_4) = v0 & ( ~ (v0 = 0) | ( ~ (v2 = 0) & ~ (v1 = 0)))) % 32.85/10.03 | % 32.85/10.03 | Instantiating (357) with all_152_0_135, all_152_1_136, all_152_2_137 yields: % 32.85/10.03 | (358) apart_point_and_line(all_1_2_2, all_1_4_4) = all_152_0_135 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_152_1_136 & convergent_lines(all_1_5_5, all_1_4_4) = all_152_2_137 & ( ~ (all_152_2_137 = 0) | ( ~ (all_152_0_135 = 0) & ~ (all_152_1_136 = 0))) % 32.85/10.03 | % 32.85/10.03 | Applying alpha-rule on (358) yields: % 32.85/10.03 | (359) apart_point_and_line(all_1_2_2, all_1_4_4) = all_152_0_135 % 32.85/10.03 | (360) apart_point_and_line(all_1_2_2, all_1_5_5) = all_152_1_136 % 32.85/10.03 | (361) convergent_lines(all_1_5_5, all_1_4_4) = all_152_2_137 % 32.85/10.03 | (362) ~ (all_152_2_137 = 0) | ( ~ (all_152_0_135 = 0) & ~ (all_152_1_136 = 0)) % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (239), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (363) ~ (all_102_2_110 = 0) % 32.85/10.03 | % 32.85/10.03 | Equations (283) can reduce 363 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (283) all_102_2_110 = 0 % 32.85/10.03 | (366) all_102_0_108 = 0 % 32.85/10.03 | % 32.85/10.03 | From (366) and (238) follows: % 32.85/10.03 | (367) distinct_points(all_1_0_0, all_102_1_109) = 0 % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (294), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (368) ~ (distinct_points(all_1_2_2, all_1_2_2) = all_78_0_70) % 32.85/10.03 | % 32.85/10.03 | Using (353) and (368) yields: % 32.85/10.03 | (369) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (353) distinct_points(all_1_2_2, all_1_2_2) = all_78_0_70 % 32.85/10.03 | (371) all_121_2_125 = all_78_0_70 % 32.85/10.03 | % 32.85/10.03 | Combining equations (371,347) yields a new equation: % 32.85/10.03 | (372) all_78_0_70 = all_35_3_22 % 32.85/10.03 | % 32.85/10.03 | Simplifying 372 yields: % 32.85/10.03 | (373) all_78_0_70 = all_35_3_22 % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (197), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (374) all_78_0_70 = 0 % 32.85/10.03 | % 32.85/10.03 | Combining equations (373,374) yields a new equation: % 32.85/10.03 | (375) all_35_3_22 = 0 % 32.85/10.03 | % 32.85/10.03 | Simplifying 375 yields: % 32.85/10.03 | (250) all_35_3_22 = 0 % 32.85/10.03 | % 32.85/10.03 | Equations (250) can reduce 115 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (378) ~ (all_78_0_70 = 0) % 32.85/10.03 | (379) ~ (all_78_2_72 = 0) & ~ (all_19_2_11 = 0) % 32.85/10.03 | % 32.85/10.03 | Applying alpha-rule on (379) yields: % 32.85/10.03 | (380) ~ (all_78_2_72 = 0) % 32.85/10.03 | (381) ~ (all_19_2_11 = 0) % 32.85/10.03 | % 32.85/10.03 | Equations (325) can reduce 380 to: % 32.85/10.03 | (382) ~ (all_17_2_8 = 0) % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (121), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (383) all_17_2_8 = 0 % 32.85/10.03 | % 32.85/10.03 | Equations (383) can reduce 382 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (382) ~ (all_17_2_8 = 0) % 32.85/10.03 | (386) ? [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)) % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (140), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (387) all_19_2_11 = 0 % 32.85/10.03 | % 32.85/10.03 | Equations (387) can reduce 381 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (381) ~ (all_19_2_11 = 0) % 32.85/10.03 | (390) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_1_5_5) = v2 & apart_point_and_line(all_1_0_0, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (125), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (387) all_19_2_11 = 0 % 32.85/10.03 | % 32.85/10.03 | Equations (387) can reduce 381 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (381) ~ (all_19_2_11 = 0) % 32.85/10.03 | (394) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & apart_point_and_line(all_1_2_2, all_1_5_5) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (139), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (387) all_19_2_11 = 0 % 32.85/10.03 | % 32.85/10.03 | Equations (387) can reduce 381 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (381) ~ (all_19_2_11 = 0) % 32.85/10.03 | (398) all_17_2_8 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_1_4_4) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (126), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (387) all_19_2_11 = 0 % 32.85/10.03 | % 32.85/10.03 | Equations (387) can reduce 381 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (381) ~ (all_19_2_11 = 0) % 32.85/10.03 | (402) all_17_2_8 = 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)) % 32.85/10.03 | % 32.85/10.03 +-Applying beta-rule and splitting (398), into two cases. % 32.85/10.03 |-Branch one: % 32.85/10.03 | (383) all_17_2_8 = 0 % 32.85/10.03 | % 32.85/10.03 | Equations (383) can reduce 382 to: % 32.85/10.03 | (92) $false % 32.85/10.03 | % 32.85/10.03 |-The branch is then unsatisfiable % 32.85/10.03 |-Branch two: % 32.85/10.03 | (382) ~ (all_17_2_8 = 0) % 32.85/10.03 | (406) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_1_4_4) = v1 & apart_point_and_line(all_1_0_0, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 32.85/10.03 | % 32.85/10.03 | Instantiating formula (22) with all_1_5_5, all_1_4_4, all_152_2_137, 0 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_152_2_137, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 32.85/10.03 | (407) all_152_2_137 = 0 % 32.85/10.03 | % 32.85/10.03 | From (407) and (361) follows: % 32.85/10.03 | (51) convergent_lines(all_1_5_5, all_1_4_4) = 0 % 32.85/10.03 | % 32.85/10.03 | Instantiating formula (29) with all_70_2_60, 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_70_2_60, convergent_lines(all_1_5_5, all_1_4_4) = 0, ~ (convergent_lines(all_1_5_5, all_1_5_5) = 0), yields: % 32.85/10.03 | (409) all_70_2_60 = 0 % 32.85/10.03 | % 32.85/10.03 | Instantiating formula (41) with all_62_0_44, 0, all_1_0_0, all_1_0_0, all_17_1_7 and discharging atoms distinct_points(all_1_0_0, all_17_1_7) = 0, distinct_points(all_1_0_0, all_1_0_0) = all_62_0_44, yields: % 32.85/10.03 | (410) all_62_0_44 = 0 | ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_17_1_7, all_1_0_0) = v1 & apart_point_and_line(all_1_0_0, v1) = v2 & distinct_points(all_17_1_7, all_1_0_0) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 32.85/10.03 | % 32.85/10.03 | Instantiating formula (41) with all_62_0_44, 0, all_1_0_0, all_1_0_0, all_1_2_2 and discharging atoms distinct_points(all_1_0_0, all_1_0_0) = all_62_0_44, distinct_points(all_1_0_0, all_1_2_2) = 0, yields: % 32.85/10.03 | (411) all_62_0_44 = 0 | ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_1_0_0) = v1 & apart_point_and_line(all_1_0_0, v1) = v2 & distinct_points(all_1_2_2, all_1_0_0) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 32.85/10.03 | % 32.85/10.03 | Instantiating formula (41) with all_62_0_44, 0, all_1_0_0, all_1_0_0, all_102_1_109 and discharging atoms distinct_points(all_1_0_0, all_102_1_109) = 0, distinct_points(all_1_0_0, all_1_0_0) = all_62_0_44, yields: % 32.85/10.03 | (412) all_62_0_44 = 0 | ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_102_1_109, all_1_0_0) = v1 & apart_point_and_line(all_1_0_0, v1) = v2 & distinct_points(all_102_1_109, all_1_0_0) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 32.85/10.03 | % 32.85/10.04 +-Applying beta-rule and splitting (410), into two cases. % 32.85/10.04 |-Branch one: % 32.85/10.04 | (413) all_62_0_44 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (413) can reduce 348 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (348) ~ (all_62_0_44 = 0) % 32.85/10.04 | (416) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_17_1_7, all_1_0_0) = v1 & apart_point_and_line(all_1_0_0, v1) = v2 & distinct_points(all_17_1_7, all_1_0_0) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 32.85/10.04 | % 32.85/10.04 +-Applying beta-rule and splitting (411), into two cases. % 32.85/10.04 |-Branch one: % 32.85/10.04 | (413) all_62_0_44 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (413) can reduce 348 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (348) ~ (all_62_0_44 = 0) % 32.85/10.04 | (420) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_2_2, all_1_0_0) = v1 & apart_point_and_line(all_1_0_0, v1) = v2 & distinct_points(all_1_2_2, all_1_0_0) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 32.85/10.04 | % 32.85/10.04 +-Applying beta-rule and splitting (412), into two cases. % 32.85/10.04 |-Branch one: % 32.85/10.04 | (413) all_62_0_44 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (413) can reduce 348 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (348) ~ (all_62_0_44 = 0) % 32.85/10.04 | (424) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_102_1_109, all_1_0_0) = v1 & apart_point_and_line(all_1_0_0, v1) = v2 & distinct_points(all_102_1_109, all_1_0_0) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 32.85/10.04 | % 32.85/10.04 +-Applying beta-rule and splitting (182), into two cases. % 32.85/10.04 |-Branch one: % 32.85/10.04 | (425) ~ (all_70_2_60 = 0) % 32.85/10.04 | % 32.85/10.04 | Equations (409) can reduce 425 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (409) all_70_2_60 = 0 % 32.85/10.04 | (428) all_70_0_58 = 0 | ( ~ (all_70_1_59 = 0) & ~ (all_25_1_18 = 0)) % 32.85/10.04 | % 32.85/10.04 +-Applying beta-rule and splitting (428), into two cases. % 32.85/10.04 |-Branch one: % 32.85/10.04 | (429) all_70_0_58 = 0 % 32.85/10.04 | % 32.85/10.04 | Combining equations (335,429) yields a new equation: % 32.85/10.04 | (430) all_62_0_44 = 0 % 32.85/10.04 | % 32.85/10.04 | Simplifying 430 yields: % 32.85/10.04 | (413) all_62_0_44 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (413) can reduce 348 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (292) ~ (all_70_0_58 = 0) % 32.85/10.04 | (434) ~ (all_70_1_59 = 0) & ~ (all_25_1_18 = 0) % 32.85/10.04 | % 32.85/10.04 | Applying alpha-rule on (434) yields: % 32.85/10.04 | (435) ~ (all_70_1_59 = 0) % 32.85/10.04 | (436) ~ (all_25_1_18 = 0) % 32.85/10.04 | % 32.85/10.04 | Equations (346) can reduce 435 to: % 32.85/10.04 | (437) ~ (all_21_1_13 = 0) % 32.85/10.04 | % 32.85/10.04 +-Applying beta-rule and splitting (151), into two cases. % 32.85/10.04 |-Branch one: % 32.85/10.04 | (438) all_60_0_40 = 0 % 32.85/10.04 | % 32.85/10.04 | Combining equations (332,438) yields a new equation: % 32.85/10.04 | (439) all_17_2_8 = 0 % 32.85/10.04 | % 32.85/10.04 | Simplifying 439 yields: % 32.85/10.04 | (383) all_17_2_8 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (383) can reduce 382 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (442) ~ (all_60_0_40 = 0) % 32.85/10.04 | (443) all_60_1_41 = 0 | all_60_2_42 = 0 | all_60_3_43 = 0 % 32.85/10.04 | % 32.85/10.04 +-Applying beta-rule and splitting (443), into two cases. % 32.85/10.04 |-Branch one: % 32.85/10.04 | (444) all_60_1_41 = 0 % 32.85/10.04 | % 32.85/10.04 | Combining equations (444,338) yields a new equation: % 32.85/10.04 | (387) all_19_2_11 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (387) can reduce 381 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (447) ~ (all_60_1_41 = 0) % 32.85/10.04 | (448) all_60_2_42 = 0 | all_60_3_43 = 0 % 32.85/10.04 | % 32.85/10.04 +-Applying beta-rule and splitting (448), into two cases. % 32.85/10.04 |-Branch one: % 32.85/10.04 | (449) all_60_2_42 = 0 % 32.85/10.04 | % 32.85/10.04 | Combining equations (449,341) yields a new equation: % 32.85/10.04 | (450) all_21_1_13 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (450) can reduce 437 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (452) ~ (all_60_2_42 = 0) % 32.85/10.04 | (453) all_60_3_43 = 0 % 32.85/10.04 | % 32.85/10.04 | Combining equations (343,453) yields a new equation: % 32.85/10.04 | (454) all_25_1_18 = 0 % 32.85/10.04 | % 32.85/10.04 | Simplifying 454 yields: % 32.85/10.04 | (455) all_25_1_18 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (455) can reduce 436 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (457) ~ (convergent_lines(all_1_4_4, all_1_3_3) = 0) % 32.85/10.04 | (458) all_23_2_16 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (458) can reduce 114 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 |-Branch two: % 32.85/10.04 | (460) ~ (distinct_points(all_1_0_0, all_1_2_2) = 0) % 32.85/10.04 | (91) all_1_1_1 = 0 % 32.85/10.04 | % 32.85/10.04 | Equations (91) can reduce 48 to: % 32.85/10.04 | (92) $false % 32.85/10.04 | % 32.85/10.04 |-The branch is then unsatisfiable % 32.85/10.04 % SZS output end Proof for theBenchmark % 32.85/10.04 % 32.85/10.04 9395ms %------------------------------------------------------------------------------