%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GEO195+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 03:48:31 EDT 2022 % Result : Theorem 22.47s 6.03s % Output : Proof 30.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GEO195+1 : TPTP v8.1.0. Released v3.3.0. % 0.12/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sat Jun 18 06:06:19 EDT 2022 % 0.19/0.33 % CPUTime : % 0.57/0.59 ____ _ % 0.57/0.59 ___ / __ \_____(_)___ ________ __________ % 0.57/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.57/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.57/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.57/0.59 % 0.57/0.59 A Theorem Prover for First-Order Logic % 0.57/0.59 (ePrincess v.1.0) % 0.57/0.59 % 0.57/0.59 (c) Philipp Rümmer, 2009-2015 % 0.57/0.59 (c) Peter Backeman, 2014-2015 % 0.57/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.57/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.57/0.59 Bug reports to peter@backeman.se % 0.57/0.59 % 0.57/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.57/0.59 % 0.57/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.76/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.77/0.94 Prover 0: Preprocessing ... % 1.93/1.07 Prover 0: Warning: ignoring some quantifiers % 2.11/1.09 Prover 0: Constructing countermodel ... % 3.18/1.40 Prover 0: gave up % 3.18/1.40 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 3.18/1.42 Prover 1: Preprocessing ... % 3.52/1.51 Prover 1: Constructing countermodel ... % 3.70/1.54 Prover 1: gave up % 3.70/1.54 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.70/1.56 Prover 2: Preprocessing ... % 4.09/1.67 Prover 2: Warning: ignoring some quantifiers % 4.09/1.68 Prover 2: Constructing countermodel ... % 13.25/3.83 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 13.25/3.84 Prover 3: Preprocessing ... % 13.25/3.85 Prover 3: Warning: ignoring some quantifiers % 13.25/3.86 Prover 3: Constructing countermodel ... % 13.61/3.89 Prover 3: gave up % 13.61/3.90 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 13.61/3.91 Prover 4: Preprocessing ... % 13.61/3.97 Prover 4: Warning: ignoring some quantifiers % 13.61/3.97 Prover 4: Constructing countermodel ... % 17.91/4.94 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 17.91/4.97 Prover 5: Preprocessing ... % 18.31/5.03 Prover 5: Constructing countermodel ... % 22.47/6.03 Prover 5: proved (1088ms) % 22.47/6.03 Prover 4: stopped % 22.47/6.03 Prover 2: stopped % 22.47/6.03 % 22.47/6.03 No countermodel exists, formula is valid % 22.47/6.03 % SZS status Theorem for theBenchmark % 22.47/6.03 % 22.47/6.03 Generating proof ... found it (size 446) % 29.41/7.75 % 29.41/7.75 % SZS output start Proof for theBenchmark % 29.41/7.75 Assumed formulas after preprocessing and simplification: % 29.41/7.76 | (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 | ~ (convergent_lines(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_lines(v1, v2) = v4) | ~ (distinct_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_lines(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_points(v1, v2) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_points(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (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 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | convergent_lines(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (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] : ( ~ (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] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v2, v1) = v4 & convergent_lines(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v2, v0) = v4 & convergent_lines(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v1, v2) = v4 & distinct_points(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v0, v2) = v4 & distinct_points(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) & ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v1) = v3)) & ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v0) = v3)) & ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v1, v2) = v3)) & ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v0, v2) = v3)) & ! [v0] : ~ (convergent_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_points(v0, v0) = 0) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = 0) & intersection_point(v1, v0) = v4 & intersection_point(v0, v1) = v3 & apart_point_and_line(v4, v2) = v5 & apart_point_and_line(v3, v2) = 0 & convergent_lines(v2, v1) = 0 & convergent_lines(v0, v2) = 0 & convergent_lines(v0, v1) = 0) % 29.78/7.82 | Applying alpha-rule on (0) yields: % 29.78/7.82 | (1) ! [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))) % 29.78/7.82 | (2) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v1) = v3)) % 29.78/7.82 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) % 29.78/7.82 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 29.78/7.82 | (5) ! [v0] : ~ (distinct_lines(v0, v0) = 0) % 29.78/7.82 | (6) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & intersection_point(v0, v1) = v2 & apart_point_and_line(v2, v0) = v3)) % 29.78/7.82 | (7) ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v0, v2) = v3)) % 29.78/7.82 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) % 29.78/7.82 | (9) ! [v0] : ~ (convergent_lines(v0, v0) = 0) % 29.78/7.82 | (10) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = 0) & intersection_point(v1, v0) = v4 & intersection_point(v0, v1) = v3 & apart_point_and_line(v4, v2) = v5 & apart_point_and_line(v3, v2) = 0 & convergent_lines(v2, v1) = 0 & convergent_lines(v0, v2) = 0 & convergent_lines(v0, v1) = 0) % 29.78/7.82 | (11) ! [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) % 29.78/7.82 | (12) ! [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))) % 29.78/7.83 | (13) ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v1, v2) = v4 & distinct_points(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 29.78/7.83 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) % 29.78/7.83 | (15) ! [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) % 29.78/7.83 | (16) ! [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)) % 29.78/7.83 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 29.78/7.83 | (18) ! [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) % 29.78/7.83 | (19) ! [v0] : ~ (distinct_points(v0, v0) = 0) % 29.78/7.83 | (20) ! [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))) % 29.78/7.83 | (21) ! [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))) % 29.78/7.83 | (22) ! [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)) % 29.78/7.83 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (convergent_lines(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) % 29.78/7.83 | (24) ! [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) % 29.78/7.83 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) % 29.78/7.83 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 29.78/7.83 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) % 29.78/7.83 | (28) ! [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))) % 29.78/7.83 | (29) ! [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))) % 29.78/7.84 | (30) ! [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)) % 29.78/7.84 | (31) ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ( ~ (v3 = 0) & line_connecting(v0, v1) = v2 & apart_point_and_line(v1, v2) = v3)) % 29.78/7.84 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) % 29.78/7.84 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | convergent_lines(v0, v2) = 0) % 29.78/7.84 | (34) ! [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))) % 29.78/7.84 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) % 29.78/7.84 | (36) ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v2, v0) = v4 & convergent_lines(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 29.78/7.84 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) % 29.78/7.84 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v2, v1) = v4 & convergent_lines(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 29.78/7.84 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) % 29.78/7.84 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) % 29.78/7.84 | (41) ! [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)) % 29.78/7.84 | (42) ! [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)) % 29.78/7.84 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : (apart_point_and_line(v0, v2) = v4 & distinct_points(v0, v1) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0)))) % 29.78/7.84 | % 29.78/7.84 | Instantiating (10) 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: % 29.78/7.84 | (44) ~ (all_1_0_0 = 0) & intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1 & intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2 & apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0 & apart_point_and_line(all_1_2_2, all_1_3_3) = 0 & convergent_lines(all_1_3_3, all_1_4_4) = 0 & convergent_lines(all_1_5_5, all_1_3_3) = 0 & convergent_lines(all_1_5_5, all_1_4_4) = 0 % 29.78/7.84 | % 29.78/7.84 | Applying alpha-rule on (44) yields: % 29.78/7.84 | (45) convergent_lines(all_1_5_5, all_1_3_3) = 0 % 29.78/7.84 | (46) apart_point_and_line(all_1_2_2, all_1_3_3) = 0 % 29.78/7.84 | (47) convergent_lines(all_1_5_5, all_1_4_4) = 0 % 29.78/7.84 | (48) convergent_lines(all_1_3_3, all_1_4_4) = 0 % 29.78/7.84 | (49) apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0 % 29.78/7.84 | (50) intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2 % 29.78/7.84 | (51) intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1 % 29.78/7.84 | (52) ~ (all_1_0_0 = 0) % 29.78/7.84 | % 29.78/7.85 | Instantiating formula (9) with all_1_4_4 yields: % 29.78/7.85 | (53) ~ (convergent_lines(all_1_4_4, all_1_4_4) = 0) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (9) with all_1_5_5 yields: % 29.78/7.85 | (54) ~ (convergent_lines(all_1_5_5, all_1_5_5) = 0) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (38) with all_1_1_1, all_1_5_5, all_1_4_4 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1, yields: % 29.78/7.85 | (55) ? [v0] : ? [v1] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & convergent_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (36) with all_1_1_1, all_1_5_5, all_1_4_4 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1, yields: % 29.78/7.85 | (56) ? [v0] : ? [v1] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & convergent_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (38) with 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, yields: % 29.78/7.85 | (57) ? [v0] : ? [v1] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & convergent_lines(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (36) with 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, yields: % 29.78/7.85 | (58) ? [v0] : ? [v1] : (apart_point_and_line(all_1_2_2, all_1_5_5) = v1 & convergent_lines(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (12) with all_1_0_0, all_1_0_0, all_1_3_3, all_1_3_3, all_1_1_1, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 29.78/7.85 | (59) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (15) with all_1_0_0, all_1_1_1, all_1_3_3, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_1_3_3) = 0, yields: % 29.78/7.85 | (60) all_1_0_0 = 0 | distinct_points(all_1_2_2, all_1_1_1) = 0 % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (2) with all_1_4_4, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 29.78/7.85 | (61) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_1_3_3, all_1_4_4) = v0 & apart_point_and_line(v0, all_1_4_4) = v1) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (6) with all_1_4_4, all_1_3_3 and discharging atoms convergent_lines(all_1_3_3, all_1_4_4) = 0, yields: % 29.78/7.85 | (62) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_1_3_3, all_1_4_4) = v0 & apart_point_and_line(v0, all_1_3_3) = v1) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (2) with all_1_3_3, all_1_5_5 and discharging atoms convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 29.78/7.85 | (63) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_1_5_5, all_1_3_3) = v0 & apart_point_and_line(v0, all_1_3_3) = v1) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (6) with all_1_3_3, all_1_5_5 and discharging atoms convergent_lines(all_1_5_5, all_1_3_3) = 0, yields: % 29.78/7.85 | (64) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_1_5_5, all_1_3_3) = v0 & apart_point_and_line(v0, all_1_5_5) = v1) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (2) with all_1_4_4, all_1_5_5 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 29.78/7.85 | (65) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_1_5_5, all_1_4_4) = v0 & apart_point_and_line(v0, all_1_4_4) = v1) % 29.78/7.85 | % 29.78/7.85 | Instantiating formula (6) with all_1_4_4, all_1_5_5 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 29.78/7.85 | (66) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_1_5_5, all_1_4_4) = v0 & apart_point_and_line(v0, all_1_5_5) = v1) % 29.78/7.85 | % 29.78/7.85 | Instantiating (66) with all_16_0_6, all_16_1_7 yields: % 29.78/7.85 | (67) ~ (all_16_0_6 = 0) & intersection_point(all_1_5_5, all_1_4_4) = all_16_1_7 & apart_point_and_line(all_16_1_7, all_1_5_5) = all_16_0_6 % 29.78/7.85 | % 29.78/7.85 | Applying alpha-rule on (67) yields: % 29.78/7.85 | (68) ~ (all_16_0_6 = 0) % 29.78/7.85 | (69) intersection_point(all_1_5_5, all_1_4_4) = all_16_1_7 % 29.78/7.85 | (70) apart_point_and_line(all_16_1_7, all_1_5_5) = all_16_0_6 % 29.78/7.85 | % 29.78/7.85 | Instantiating (64) with all_18_0_8, all_18_1_9 yields: % 29.78/7.85 | (71) ~ (all_18_0_8 = 0) & intersection_point(all_1_5_5, all_1_3_3) = all_18_1_9 & apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8 % 29.78/7.85 | % 29.78/7.85 | Applying alpha-rule on (71) yields: % 29.78/7.85 | (72) ~ (all_18_0_8 = 0) % 29.78/7.85 | (73) intersection_point(all_1_5_5, all_1_3_3) = all_18_1_9 % 29.78/7.85 | (74) apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8 % 29.78/7.85 | % 29.78/7.85 | Instantiating (62) with all_20_0_10, all_20_1_11 yields: % 29.78/7.85 | (75) ~ (all_20_0_10 = 0) & intersection_point(all_1_3_3, all_1_4_4) = all_20_1_11 & apart_point_and_line(all_20_1_11, all_1_3_3) = all_20_0_10 % 29.78/7.85 | % 29.78/7.85 | Applying alpha-rule on (75) yields: % 29.78/7.85 | (76) ~ (all_20_0_10 = 0) % 29.78/7.85 | (77) intersection_point(all_1_3_3, all_1_4_4) = all_20_1_11 % 29.78/7.85 | (78) apart_point_and_line(all_20_1_11, all_1_3_3) = all_20_0_10 % 29.78/7.85 | % 29.78/7.85 | Instantiating (61) with all_22_0_12, all_22_1_13 yields: % 29.78/7.85 | (79) ~ (all_22_0_12 = 0) & intersection_point(all_1_3_3, all_1_4_4) = all_22_1_13 & apart_point_and_line(all_22_1_13, all_1_4_4) = all_22_0_12 % 29.78/7.86 | % 29.78/7.86 | Applying alpha-rule on (79) yields: % 29.78/7.86 | (80) ~ (all_22_0_12 = 0) % 29.78/7.86 | (81) intersection_point(all_1_3_3, all_1_4_4) = all_22_1_13 % 29.78/7.86 | (82) apart_point_and_line(all_22_1_13, all_1_4_4) = all_22_0_12 % 29.78/7.86 | % 29.78/7.86 | Instantiating (63) with all_24_0_14, all_24_1_15 yields: % 29.78/7.86 | (83) ~ (all_24_0_14 = 0) & intersection_point(all_1_5_5, all_1_3_3) = all_24_1_15 & apart_point_and_line(all_24_1_15, all_1_3_3) = all_24_0_14 % 29.78/7.86 | % 29.78/7.86 | Applying alpha-rule on (83) yields: % 29.78/7.86 | (84) ~ (all_24_0_14 = 0) % 29.78/7.86 | (85) intersection_point(all_1_5_5, all_1_3_3) = all_24_1_15 % 29.78/7.86 | (86) apart_point_and_line(all_24_1_15, all_1_3_3) = all_24_0_14 % 29.78/7.86 | % 29.78/7.86 | Instantiating (65) with all_26_0_16, all_26_1_17 yields: % 29.78/7.86 | (87) ~ (all_26_0_16 = 0) & intersection_point(all_1_5_5, all_1_4_4) = all_26_1_17 & apart_point_and_line(all_26_1_17, all_1_4_4) = all_26_0_16 % 29.78/7.86 | % 29.78/7.86 | Applying alpha-rule on (87) yields: % 29.78/7.86 | (88) ~ (all_26_0_16 = 0) % 29.78/7.86 | (89) intersection_point(all_1_5_5, all_1_4_4) = all_26_1_17 % 29.78/7.86 | (90) apart_point_and_line(all_26_1_17, all_1_4_4) = all_26_0_16 % 29.78/7.86 | % 29.78/7.86 | Instantiating (58) with all_28_0_18, all_28_1_19 yields: % 29.78/7.86 | (91) apart_point_and_line(all_1_2_2, all_1_5_5) = all_28_0_18 & convergent_lines(all_1_5_5, all_1_4_4) = all_28_1_19 & ( ~ (all_28_0_18 = 0) | ~ (all_28_1_19 = 0)) % 29.78/7.86 | % 29.78/7.86 | Applying alpha-rule on (91) yields: % 29.78/7.86 | (92) apart_point_and_line(all_1_2_2, all_1_5_5) = all_28_0_18 % 29.78/7.86 | (93) convergent_lines(all_1_5_5, all_1_4_4) = all_28_1_19 % 29.78/7.86 | (94) ~ (all_28_0_18 = 0) | ~ (all_28_1_19 = 0) % 29.78/7.86 | % 29.78/7.86 | Instantiating (57) with all_30_0_20, all_30_1_21 yields: % 29.78/7.86 | (95) apart_point_and_line(all_1_2_2, all_1_4_4) = all_30_0_20 & convergent_lines(all_1_5_5, all_1_4_4) = all_30_1_21 & ( ~ (all_30_0_20 = 0) | ~ (all_30_1_21 = 0)) % 29.78/7.86 | % 29.78/7.86 | Applying alpha-rule on (95) yields: % 29.78/7.86 | (96) apart_point_and_line(all_1_2_2, all_1_4_4) = all_30_0_20 % 29.78/7.86 | (97) convergent_lines(all_1_5_5, all_1_4_4) = all_30_1_21 % 29.78/7.86 | (98) ~ (all_30_0_20 = 0) | ~ (all_30_1_21 = 0) % 29.78/7.86 | % 29.78/7.86 | Instantiating (56) with all_32_0_22, all_32_1_23 yields: % 29.78/7.86 | (99) apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22 & convergent_lines(all_1_4_4, all_1_5_5) = all_32_1_23 & ( ~ (all_32_0_22 = 0) | ~ (all_32_1_23 = 0)) % 29.78/7.86 | % 29.78/7.86 | Applying alpha-rule on (99) yields: % 29.78/7.86 | (100) apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22 % 29.78/7.86 | (101) convergent_lines(all_1_4_4, all_1_5_5) = all_32_1_23 % 29.78/7.86 | (102) ~ (all_32_0_22 = 0) | ~ (all_32_1_23 = 0) % 29.78/7.86 | % 29.78/7.86 | Instantiating (55) with all_34_0_24, all_34_1_25 yields: % 29.78/7.86 | (103) apart_point_and_line(all_1_1_1, all_1_5_5) = all_34_0_24 & convergent_lines(all_1_4_4, all_1_5_5) = all_34_1_25 & ( ~ (all_34_0_24 = 0) | ~ (all_34_1_25 = 0)) % 29.78/7.86 | % 29.78/7.86 | Applying alpha-rule on (103) yields: % 29.78/7.86 | (104) apart_point_and_line(all_1_1_1, all_1_5_5) = all_34_0_24 % 29.78/7.86 | (105) convergent_lines(all_1_4_4, all_1_5_5) = all_34_1_25 % 29.78/7.86 | (106) ~ (all_34_0_24 = 0) | ~ (all_34_1_25 = 0) % 29.78/7.86 | % 29.78/7.86 +-Applying beta-rule and splitting (60), into two cases. % 29.78/7.86 |-Branch one: % 29.78/7.86 | (107) distinct_points(all_1_2_2, all_1_1_1) = 0 % 29.78/7.86 | % 29.78/7.86 +-Applying beta-rule and splitting (59), into two cases. % 29.78/7.86 |-Branch one: % 29.78/7.86 | (108) all_1_0_0 = 0 % 29.78/7.86 | % 29.78/7.86 | Equations (108) can reduce 52 to: % 29.78/7.86 | (109) $false % 29.78/7.86 | % 29.78/7.86 |-The branch is then unsatisfiable % 29.78/7.86 |-Branch two: % 29.78/7.86 | (52) ~ (all_1_0_0 = 0) % 29.78/7.86 | (111) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.86 | % 29.78/7.86 | Instantiating (111) with all_44_0_26, all_44_1_27, all_44_2_28, all_44_3_29 yields: % 29.78/7.86 | (112) apart_point_and_line(all_1_1_1, all_1_3_3) = all_44_0_26 & apart_point_and_line(all_1_1_1, all_1_3_3) = all_44_1_27 & distinct_lines(all_1_3_3, all_1_3_3) = all_44_2_28 & distinct_points(all_1_1_1, all_1_1_1) = all_44_3_29 & ( ~ (all_44_2_28 = 0) | ~ (all_44_3_29 = 0) | all_44_0_26 = 0 | all_44_1_27 = 0) % 29.78/7.86 | % 29.78/7.86 | Applying alpha-rule on (112) yields: % 29.78/7.86 | (113) apart_point_and_line(all_1_1_1, all_1_3_3) = all_44_0_26 % 29.78/7.86 | (114) distinct_points(all_1_1_1, all_1_1_1) = all_44_3_29 % 29.78/7.86 | (115) apart_point_and_line(all_1_1_1, all_1_3_3) = all_44_1_27 % 29.78/7.86 | (116) ~ (all_44_2_28 = 0) | ~ (all_44_3_29 = 0) | all_44_0_26 = 0 | all_44_1_27 = 0 % 29.78/7.86 | (117) distinct_lines(all_1_3_3, all_1_3_3) = all_44_2_28 % 29.78/7.86 | % 29.78/7.86 | Instantiating formula (27) with all_1_3_3, all_1_4_4, all_20_1_11, all_22_1_13 and discharging atoms intersection_point(all_1_3_3, all_1_4_4) = all_22_1_13, intersection_point(all_1_3_3, all_1_4_4) = all_20_1_11, yields: % 29.78/7.86 | (118) all_22_1_13 = all_20_1_11 % 29.78/7.86 | % 29.78/7.86 | Instantiating formula (27) with all_1_5_5, all_1_3_3, all_18_1_9, all_24_1_15 and discharging atoms intersection_point(all_1_5_5, all_1_3_3) = all_24_1_15, intersection_point(all_1_5_5, all_1_3_3) = all_18_1_9, yields: % 29.78/7.87 | (119) all_24_1_15 = all_18_1_9 % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (27) with all_1_5_5, all_1_4_4, all_26_1_17, all_1_2_2 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_26_1_17, intersection_point(all_1_5_5, all_1_4_4) = all_1_2_2, yields: % 29.78/7.87 | (120) all_26_1_17 = all_1_2_2 % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (27) with all_1_5_5, all_1_4_4, all_16_1_7, all_26_1_17 and discharging atoms intersection_point(all_1_5_5, all_1_4_4) = all_26_1_17, intersection_point(all_1_5_5, all_1_4_4) = all_16_1_7, yields: % 29.78/7.87 | (121) all_26_1_17 = all_16_1_7 % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (8) with all_1_1_1, all_1_3_3, all_44_0_26, all_1_0_0 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_44_0_26, apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 29.78/7.87 | (122) all_44_0_26 = all_1_0_0 % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (8) with all_1_1_1, all_1_3_3, all_44_1_27, all_44_0_26 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_44_0_26, apart_point_and_line(all_1_1_1, all_1_3_3) = all_44_1_27, yields: % 29.78/7.87 | (123) all_44_0_26 = all_44_1_27 % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_30_0_20, all_26_0_16 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_30_0_20, yields: % 29.78/7.87 | (124) all_30_0_20 = all_26_0_16 | ~ (apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16) % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (8) with all_1_2_2, all_1_5_5, all_28_0_18, all_16_0_6 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_28_0_18, yields: % 29.78/7.87 | (125) all_28_0_18 = all_16_0_6 | ~ (apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6) % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (35) with all_1_4_4, all_1_5_5, all_32_1_23, all_34_1_25 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = all_34_1_25, convergent_lines(all_1_4_4, all_1_5_5) = all_32_1_23, yields: % 29.78/7.87 | (126) all_34_1_25 = all_32_1_23 % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (35) with all_1_5_5, all_1_4_4, all_30_1_21, 0 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_30_1_21, convergent_lines(all_1_5_5, all_1_4_4) = 0, yields: % 29.78/7.87 | (127) all_30_1_21 = 0 % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (35) with all_1_5_5, all_1_4_4, all_28_1_19, all_30_1_21 and discharging atoms convergent_lines(all_1_5_5, all_1_4_4) = all_30_1_21, convergent_lines(all_1_5_5, all_1_4_4) = all_28_1_19, yields: % 29.78/7.87 | (128) all_30_1_21 = all_28_1_19 % 29.78/7.87 | % 29.78/7.87 | Combining equations (122,123) yields a new equation: % 29.78/7.87 | (129) all_44_1_27 = all_1_0_0 % 29.78/7.87 | % 29.78/7.87 | Combining equations (128,127) yields a new equation: % 29.78/7.87 | (130) all_28_1_19 = 0 % 29.78/7.87 | % 29.78/7.87 | Simplifying 130 yields: % 29.78/7.87 | (131) all_28_1_19 = 0 % 29.78/7.87 | % 29.78/7.87 | Combining equations (120,121) yields a new equation: % 29.78/7.87 | (132) all_16_1_7 = all_1_2_2 % 29.78/7.87 | % 29.78/7.87 | Combining equations (132,121) yields a new equation: % 29.78/7.87 | (120) all_26_1_17 = all_1_2_2 % 29.78/7.87 | % 29.78/7.87 | From (120) and (90) follows: % 29.78/7.87 | (134) apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16 % 29.78/7.87 | % 29.78/7.87 | From (119) and (86) follows: % 29.78/7.87 | (135) apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14 % 29.78/7.87 | % 29.78/7.87 | From (118) and (82) follows: % 29.78/7.87 | (136) apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12 % 29.78/7.87 | % 29.78/7.87 | From (132) and (70) follows: % 29.78/7.87 | (137) apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6 % 29.78/7.87 | % 29.78/7.87 | From (129) and (115) follows: % 29.78/7.87 | (49) apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0 % 29.78/7.87 | % 29.78/7.87 | From (126) and (105) follows: % 29.78/7.87 | (101) convergent_lines(all_1_4_4, all_1_5_5) = all_32_1_23 % 29.78/7.87 | % 29.78/7.87 | From (131) and (93) follows: % 29.78/7.87 | (47) convergent_lines(all_1_5_5, all_1_4_4) = 0 % 29.78/7.87 | % 29.78/7.87 +-Applying beta-rule and splitting (98), into two cases. % 29.78/7.87 |-Branch one: % 29.78/7.87 | (141) ~ (all_30_0_20 = 0) % 29.78/7.87 | % 29.78/7.87 +-Applying beta-rule and splitting (94), into two cases. % 29.78/7.87 |-Branch one: % 29.78/7.87 | (142) ~ (all_28_0_18 = 0) % 29.78/7.87 | % 29.78/7.87 +-Applying beta-rule and splitting (125), into two cases. % 29.78/7.87 |-Branch one: % 29.78/7.87 | (143) ~ (apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6) % 29.78/7.87 | % 29.78/7.87 | Using (137) and (143) yields: % 29.78/7.87 | (144) $false % 29.78/7.87 | % 29.78/7.87 |-The branch is then unsatisfiable % 29.78/7.87 |-Branch two: % 29.78/7.87 | (137) apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6 % 29.78/7.87 | (146) all_28_0_18 = all_16_0_6 % 29.78/7.87 | % 29.78/7.87 | Equations (146) can reduce 142 to: % 29.78/7.87 | (68) ~ (all_16_0_6 = 0) % 29.78/7.87 | % 29.78/7.87 | From (146) and (92) follows: % 29.78/7.87 | (137) apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6 % 29.78/7.87 | % 29.78/7.87 +-Applying beta-rule and splitting (124), into two cases. % 29.78/7.87 |-Branch one: % 29.78/7.87 | (149) ~ (apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16) % 29.78/7.87 | % 29.78/7.87 | Using (134) and (149) yields: % 29.78/7.87 | (144) $false % 29.78/7.87 | % 29.78/7.87 |-The branch is then unsatisfiable % 29.78/7.87 |-Branch two: % 29.78/7.87 | (134) apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16 % 29.78/7.87 | (152) all_30_0_20 = all_26_0_16 % 29.78/7.87 | % 29.78/7.87 | Equations (152) can reduce 141 to: % 29.78/7.87 | (88) ~ (all_26_0_16 = 0) % 29.78/7.87 | % 29.78/7.87 | From (152) and (96) follows: % 29.78/7.87 | (134) apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16 % 29.78/7.87 | % 29.78/7.87 | Instantiating formula (12) with all_18_0_8, all_1_0_0, all_1_5_5, all_1_3_3, all_18_1_9, all_1_1_1 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 29.78/7.87 | (155) all_18_0_8 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (12) with all_1_0_0, all_18_0_8, all_1_3_3, all_1_5_5, all_1_1_1, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, yields: % 29.78/7.88 | (156) all_18_0_8 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_3_3) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_3_3) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (12) with all_18_0_8, all_22_0_12, all_1_5_5, all_1_4_4, all_18_1_9, all_20_1_11 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, yields: % 29.78/7.88 | (157) all_22_0_12 = 0 | all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_20_1_11, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (12) with all_22_0_12, all_18_0_8, all_1_4_4, all_1_5_5, all_20_1_11, all_18_1_9 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, yields: % 29.78/7.88 | (158) all_22_0_12 = 0 | all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_18_1_9, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (29) with all_18_0_8, all_22_0_12, all_1_4_4, all_1_5_5, all_18_1_9, all_20_1_11 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, yields: % 29.78/7.88 | (159) all_22_0_12 = 0 | all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (29) with all_22_0_12, all_18_0_8, all_1_5_5, all_1_4_4, all_20_1_11, all_18_1_9 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, yields: % 29.78/7.88 | (160) all_22_0_12 = 0 | all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (12) with all_18_0_8, all_18_0_8, all_1_5_5, all_1_5_5, all_18_1_9, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, yields: % 29.78/7.88 | (161) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & distinct_lines(all_1_5_5, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (12) with all_32_0_22, all_1_0_0, all_1_4_4, all_1_3_3, all_1_1_1, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.88 | (162) all_32_0_22 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (12) with all_1_0_0, all_32_0_22, all_1_3_3, all_1_4_4, all_1_1_1, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.88 | (163) all_32_0_22 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (29) with all_32_0_22, all_1_0_0, all_1_3_3, all_1_4_4, all_1_1_1, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.88 | (164) all_32_0_22 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (29) with all_1_0_0, all_32_0_22, all_1_4_4, all_1_3_3, all_1_1_1, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.88 | (165) all_32_0_22 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.88 | % 29.78/7.88 | Instantiating formula (12) with all_32_0_22, all_20_0_10, all_1_4_4, all_1_3_3, all_1_1_1, all_20_1_11 and discharging atoms apart_point_and_line(all_20_1_11, all_1_3_3) = all_20_0_10, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.88 | (166) all_32_0_22 = 0 | all_20_0_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.89 | % 29.78/7.89 | Instantiating formula (12) with all_20_0_10, all_32_0_22, all_1_3_3, all_1_4_4, all_20_1_11, all_1_1_1 and discharging atoms apart_point_and_line(all_20_1_11, all_1_3_3) = all_20_0_10, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.89 | (167) all_32_0_22 = 0 | all_20_0_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.89 | % 29.78/7.89 | Instantiating formula (29) with all_32_0_22, all_20_0_10, all_1_3_3, all_1_4_4, all_1_1_1, all_20_1_11 and discharging atoms apart_point_and_line(all_20_1_11, all_1_3_3) = all_20_0_10, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.89 | (168) all_32_0_22 = 0 | all_20_0_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_20_1_11, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.89 | % 29.78/7.89 | Instantiating formula (29) with all_20_0_10, all_32_0_22, all_1_4_4, all_1_3_3, all_20_1_11, all_1_1_1 and discharging atoms apart_point_and_line(all_20_1_11, all_1_3_3) = all_20_0_10, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.89 | (169) all_32_0_22 = 0 | all_20_0_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.89 | % 29.78/7.89 | Instantiating formula (12) with all_32_0_22, all_22_0_12, all_1_4_4, all_1_4_4, all_1_1_1, all_20_1_11 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.89 | (170) all_32_0_22 = 0 | all_22_0_12 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 29.78/7.89 | % 29.78/7.89 | Instantiating formula (12) with all_22_0_12, all_32_0_22, all_1_4_4, all_1_4_4, all_20_1_11, all_1_1_1 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 29.78/7.89 | (171) all_32_0_22 = 0 | all_22_0_12 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.89 | % 30.18/7.89 | Instantiating formula (12) with all_32_0_22, all_24_0_14, all_1_4_4, all_1_3_3, all_1_1_1, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.89 | (172) all_32_0_22 = 0 | all_24_0_14 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.89 | % 30.18/7.89 | Instantiating formula (12) with all_24_0_14, all_32_0_22, all_1_3_3, all_1_4_4, all_18_1_9, all_1_1_1 and discharging atoms apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.89 | (173) all_32_0_22 = 0 | all_24_0_14 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.89 | % 30.18/7.89 | Instantiating formula (29) with all_32_0_22, all_24_0_14, all_1_3_3, all_1_4_4, all_1_1_1, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.89 | (174) all_32_0_22 = 0 | all_24_0_14 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.89 | % 30.18/7.89 | Instantiating formula (29) with all_24_0_14, all_32_0_22, all_1_4_4, all_1_3_3, all_18_1_9, all_1_1_1 and discharging atoms apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.89 | (175) all_32_0_22 = 0 | all_24_0_14 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.89 | % 30.18/7.89 | Instantiating formula (12) with all_32_0_22, all_18_0_8, all_1_4_4, all_1_5_5, all_1_1_1, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.89 | (176) all_32_0_22 = 0 | all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.89 | % 30.18/7.89 | Instantiating formula (12) with all_18_0_8, all_32_0_22, all_1_5_5, all_1_4_4, all_18_1_9, all_1_1_1 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.89 | (177) all_32_0_22 = 0 | all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.89 | % 30.18/7.89 | Instantiating formula (29) with all_32_0_22, all_18_0_8, all_1_5_5, all_1_4_4, all_1_1_1, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.90 | (178) all_32_0_22 = 0 | all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (29) with all_18_0_8, all_32_0_22, all_1_4_4, all_1_5_5, all_18_1_9, all_1_1_1 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.90 | (179) all_32_0_22 = 0 | all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (12) with all_32_0_22, all_32_0_22, all_1_4_4, all_1_4_4, all_1_1_1, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, yields: % 30.18/7.90 | (180) all_32_0_22 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (12) with all_26_0_16, all_1_0_0, all_1_4_4, all_1_3_3, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, yields: % 30.18/7.90 | (181) all_26_0_16 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (12) with all_1_0_0, all_26_0_16, all_1_3_3, all_1_4_4, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, yields: % 30.18/7.90 | (182) all_26_0_16 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (29) with all_26_0_16, all_1_0_0, all_1_3_3, all_1_4_4, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, yields: % 30.18/7.90 | (183) all_26_0_16 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (29) with all_1_0_0, all_26_0_16, all_1_4_4, all_1_3_3, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, yields: % 30.18/7.90 | (184) all_26_0_16 = 0 | all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (12) with all_16_0_6, all_22_0_12, all_1_5_5, all_1_4_4, all_1_2_2, all_20_1_11 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.90 | (185) all_22_0_12 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_20_1_11, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (12) with all_22_0_12, all_16_0_6, all_1_4_4, all_1_5_5, all_20_1_11, all_1_2_2 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.90 | (186) all_22_0_12 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (29) with all_16_0_6, all_22_0_12, all_1_4_4, all_1_5_5, all_1_2_2, all_20_1_11 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.90 | (187) all_22_0_12 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (29) with all_22_0_12, all_16_0_6, all_1_5_5, all_1_4_4, all_20_1_11, all_1_2_2 and discharging atoms apart_point_and_line(all_20_1_11, all_1_4_4) = all_22_0_12, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.90 | (188) all_22_0_12 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.90 | % 30.18/7.90 | Instantiating formula (12) with all_16_0_6, all_24_0_14, all_1_5_5, all_1_3_3, all_1_2_2, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.90 | (189) all_24_0_14 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (12) with all_24_0_14, all_16_0_6, all_1_3_3, all_1_5_5, all_18_1_9, all_1_2_2 and discharging atoms apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (190) all_24_0_14 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_5_5, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (29) with all_16_0_6, all_24_0_14, all_1_3_3, all_1_5_5, all_1_2_2, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (191) all_24_0_14 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_5_5, all_1_3_3) = v1 & distinct_points(all_18_1_9, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (29) with all_24_0_14, all_16_0_6, all_1_5_5, all_1_3_3, all_18_1_9, all_1_2_2 and discharging atoms apart_point_and_line(all_18_1_9, all_1_3_3) = all_24_0_14, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (192) all_24_0_14 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (12) with all_16_0_6, all_18_0_8, all_1_5_5, all_1_5_5, all_1_2_2, all_18_1_9 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (193) all_18_0_8 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (12) with all_18_0_8, all_16_0_6, all_1_5_5, all_1_5_5, all_18_1_9, all_1_2_2 and discharging atoms apart_point_and_line(all_18_1_9, all_1_5_5) = all_18_0_8, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (194) all_18_0_8 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_5_5) = v2 & distinct_lines(all_1_5_5, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (12) with all_16_0_6, all_32_0_22, all_1_5_5, all_1_4_4, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (195) all_32_0_22 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (12) with all_32_0_22, all_16_0_6, all_1_4_4, all_1_5_5, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (196) all_32_0_22 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (29) with all_16_0_6, all_32_0_22, all_1_4_4, all_1_5_5, all_1_2_2, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (197) all_32_0_22 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (29) with all_32_0_22, all_16_0_6, all_1_5_5, all_1_4_4, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (198) all_32_0_22 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (12) with all_16_0_6, all_26_0_16, 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_26_0_16, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (199) all_26_0_16 = 0 | all_16_0_6 = 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)) % 30.18/7.91 | % 30.18/7.91 | Instantiating formula (12) with all_26_0_16, all_16_0_6, all_1_4_4, all_1_5_5, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.91 | (200) all_26_0_16 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.92 | % 30.18/7.92 | Instantiating formula (29) with all_16_0_6, all_26_0_16, all_1_4_4, all_1_5_5, all_1_2_2, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.92 | (201) all_26_0_16 = 0 | all_16_0_6 = 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_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.92 | % 30.18/7.92 | Instantiating formula (25) with all_32_1_23, 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_32_1_23, convergent_lines(all_1_5_5, all_1_4_4) = 0, ~ (convergent_lines(all_1_5_5, all_1_5_5) = 0), yields: % 30.18/7.92 | (202) all_32_1_23 = 0 % 30.18/7.92 | % 30.18/7.92 | Instantiating formula (2) with all_1_5_5, all_1_4_4 yields: % 30.18/7.92 | (203) ~ (convergent_lines(all_1_4_4, all_1_5_5) = 0) | ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_1_4_4, all_1_5_5) = v0 & apart_point_and_line(v0, all_1_5_5) = v1) % 30.18/7.92 | % 30.18/7.92 | Instantiating formula (34) with all_32_0_22, all_32_0_22, all_1_4_4, all_1_4_4, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 30.18/7.92 | (204) all_32_0_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_4_4) = v1 & distinct_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.92 | % 30.18/7.92 | Instantiating formula (34) with all_32_0_22, all_34_0_24, all_1_4_4, all_1_5_5, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_1_1, all_1_4_4) = all_32_0_22, apart_point_and_line(all_1_1_1, all_1_5_5) = all_34_0_24, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 30.18/7.92 | (205) all_34_0_24 = 0 | all_32_0_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 & distinct_lines(all_1_5_5, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.92 | % 30.18/7.92 | Instantiating formula (28) with all_26_0_16, all_26_0_16, all_1_4_4, all_1_4_4, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 30.18/7.92 | (206) all_26_0_16 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.92 | % 30.18/7.92 | Instantiating formula (28) with all_16_0_6, all_26_0_16, all_1_5_5, all_1_4_4, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 30.18/7.92 | (207) all_26_0_16 = 0 | all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.92 | % 30.18/7.92 | Instantiating formula (28) with all_16_0_6, all_16_0_6, all_1_5_5, all_1_5_5, all_1_1_1, all_1_2_2 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, distinct_points(all_1_2_2, all_1_1_1) = 0, yields: % 30.18/7.92 | (208) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.92 | % 30.18/7.92 | From (202) and (101) follows: % 30.18/7.92 | (209) convergent_lines(all_1_4_4, all_1_5_5) = 0 % 30.18/7.92 | % 30.18/7.92 +-Applying beta-rule and splitting (102), into two cases. % 30.18/7.92 |-Branch one: % 30.18/7.92 | (210) ~ (all_32_0_22 = 0) % 30.18/7.92 | % 30.18/7.92 +-Applying beta-rule and splitting (208), into two cases. % 30.18/7.92 |-Branch one: % 30.18/7.92 | (211) all_16_0_6 = 0 % 30.18/7.92 | % 30.18/7.92 | Equations (211) can reduce 68 to: % 30.18/7.92 | (109) $false % 30.18/7.92 | % 30.18/7.92 |-The branch is then unsatisfiable % 30.18/7.92 |-Branch two: % 30.18/7.92 | (68) ~ (all_16_0_6 = 0) % 30.18/7.92 | (214) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v1 & distinct_lines(all_1_5_5, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.92 | % 30.18/7.92 | Instantiating (214) with all_87_0_34, all_87_1_35, all_87_2_36 yields: % 30.18/7.92 | (215) apart_point_and_line(all_1_1_1, all_1_5_5) = all_87_0_34 & apart_point_and_line(all_1_1_1, all_1_5_5) = all_87_1_35 & distinct_lines(all_1_5_5, all_1_5_5) = all_87_2_36 & ( ~ (all_87_2_36 = 0) | all_87_0_34 = 0 | all_87_1_35 = 0) % 30.18/7.92 | % 30.18/7.92 | Applying alpha-rule on (215) yields: % 30.18/7.92 | (216) apart_point_and_line(all_1_1_1, all_1_5_5) = all_87_0_34 % 30.18/7.92 | (217) apart_point_and_line(all_1_1_1, all_1_5_5) = all_87_1_35 % 30.18/7.92 | (218) distinct_lines(all_1_5_5, all_1_5_5) = all_87_2_36 % 30.18/7.92 | (219) ~ (all_87_2_36 = 0) | all_87_0_34 = 0 | all_87_1_35 = 0 % 30.18/7.92 | % 30.18/7.92 +-Applying beta-rule and splitting (185), into two cases. % 30.18/7.92 |-Branch one: % 30.18/7.92 | (220) all_22_0_12 = 0 % 30.18/7.92 | % 30.18/7.92 | Equations (220) can reduce 80 to: % 30.18/7.92 | (109) $false % 30.18/7.92 | % 30.18/7.92 |-The branch is then unsatisfiable % 30.18/7.92 |-Branch two: % 30.18/7.92 | (80) ~ (all_22_0_12 = 0) % 30.18/7.92 | (223) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_20_1_11, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.92 | % 30.18/7.92 +-Applying beta-rule and splitting (186), into two cases. % 30.18/7.92 |-Branch one: % 30.18/7.92 | (220) all_22_0_12 = 0 % 30.18/7.92 | % 30.18/7.92 | Equations (220) can reduce 80 to: % 30.18/7.92 | (109) $false % 30.18/7.92 | % 30.18/7.92 |-The branch is then unsatisfiable % 30.18/7.92 |-Branch two: % 30.18/7.92 | (80) ~ (all_22_0_12 = 0) % 30.18/7.92 | (227) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.92 | % 30.18/7.92 +-Applying beta-rule and splitting (187), into two cases. % 30.18/7.92 |-Branch one: % 30.18/7.92 | (220) all_22_0_12 = 0 % 30.18/7.92 | % 30.18/7.93 | Equations (220) can reduce 80 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (80) ~ (all_22_0_12 = 0) % 30.18/7.93 | (231) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (199), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (232) all_26_0_16 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (232) can reduce 88 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (88) ~ (all_26_0_16 = 0) % 30.18/7.93 | (235) all_16_0_6 = 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)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (200), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (232) all_26_0_16 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (232) can reduce 88 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (88) ~ (all_26_0_16 = 0) % 30.18/7.93 | (239) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (201), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (232) all_26_0_16 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (232) can reduce 88 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (88) ~ (all_26_0_16 = 0) % 30.18/7.93 | (243) all_16_0_6 = 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_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (193), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (244) all_18_0_8 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (244) can reduce 72 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (72) ~ (all_18_0_8 = 0) % 30.18/7.93 | (247) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (194), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (244) all_18_0_8 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (244) can reduce 72 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (72) ~ (all_18_0_8 = 0) % 30.18/7.93 | (251) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_5_5) = v2 & distinct_lines(all_1_5_5, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (188), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (220) all_22_0_12 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (220) can reduce 80 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (80) ~ (all_22_0_12 = 0) % 30.18/7.93 | (255) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (191), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (256) all_24_0_14 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (256) can reduce 84 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (84) ~ (all_24_0_14 = 0) % 30.18/7.93 | (259) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_5_5, all_1_3_3) = v1 & distinct_points(all_18_1_9, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (189), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (256) all_24_0_14 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (256) can reduce 84 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (84) ~ (all_24_0_14 = 0) % 30.18/7.93 | (263) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (190), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (256) all_24_0_14 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (256) can reduce 84 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (84) ~ (all_24_0_14 = 0) % 30.18/7.93 | (267) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_5_5, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (192), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (256) all_24_0_14 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (256) can reduce 84 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (84) ~ (all_24_0_14 = 0) % 30.18/7.93 | (271) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (203), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (272) ~ (convergent_lines(all_1_4_4, all_1_5_5) = 0) % 30.18/7.93 | % 30.18/7.93 | Using (209) and (272) yields: % 30.18/7.93 | (144) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (209) convergent_lines(all_1_4_4, all_1_5_5) = 0 % 30.18/7.93 | (275) ? [v0] : ? [v1] : ( ~ (v1 = 0) & intersection_point(all_1_4_4, all_1_5_5) = v0 & apart_point_and_line(v0, all_1_5_5) = v1) % 30.18/7.93 | % 30.18/7.93 | Instantiating (275) with all_132_0_37, all_132_1_38 yields: % 30.18/7.93 | (276) ~ (all_132_0_37 = 0) & intersection_point(all_1_4_4, all_1_5_5) = all_132_1_38 & apart_point_and_line(all_132_1_38, all_1_5_5) = all_132_0_37 % 30.18/7.93 | % 30.18/7.93 | Applying alpha-rule on (276) yields: % 30.18/7.93 | (277) ~ (all_132_0_37 = 0) % 30.18/7.93 | (278) intersection_point(all_1_4_4, all_1_5_5) = all_132_1_38 % 30.18/7.93 | (279) apart_point_and_line(all_132_1_38, all_1_5_5) = all_132_0_37 % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (196), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (280) all_32_0_22 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (280) can reduce 210 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (210) ~ (all_32_0_22 = 0) % 30.18/7.93 | (283) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.93 | % 30.18/7.93 +-Applying beta-rule and splitting (198), into two cases. % 30.18/7.93 |-Branch one: % 30.18/7.93 | (280) all_32_0_22 = 0 % 30.18/7.93 | % 30.18/7.93 | Equations (280) can reduce 210 to: % 30.18/7.93 | (109) $false % 30.18/7.93 | % 30.18/7.93 |-The branch is then unsatisfiable % 30.18/7.93 |-Branch two: % 30.18/7.93 | (210) ~ (all_32_0_22 = 0) % 30.18/7.93 | (287) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (227), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (211) all_16_0_6 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (211) can reduce 68 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (68) ~ (all_16_0_6 = 0) % 30.18/7.94 | (291) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 | Instantiating (291) with all_143_0_39, all_143_1_40, all_143_2_41, all_143_3_42 yields: % 30.18/7.94 | (292) apart_point_and_line(all_20_1_11, all_1_5_5) = all_143_0_39 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_143_1_40 & distinct_lines(all_1_5_5, all_1_4_4) = all_143_2_41 & distinct_points(all_1_2_2, all_20_1_11) = all_143_3_42 & ( ~ (all_143_2_41 = 0) | ~ (all_143_3_42 = 0) | all_143_0_39 = 0 | all_143_1_40 = 0) % 30.18/7.94 | % 30.18/7.94 | Applying alpha-rule on (292) yields: % 30.18/7.94 | (293) apart_point_and_line(all_1_2_2, all_1_4_4) = all_143_1_40 % 30.18/7.94 | (294) distinct_points(all_1_2_2, all_20_1_11) = all_143_3_42 % 30.18/7.94 | (295) apart_point_and_line(all_20_1_11, all_1_5_5) = all_143_0_39 % 30.18/7.94 | (296) distinct_lines(all_1_5_5, all_1_4_4) = all_143_2_41 % 30.18/7.94 | (297) ~ (all_143_2_41 = 0) | ~ (all_143_3_42 = 0) | all_143_0_39 = 0 | all_143_1_40 = 0 % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (239), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (211) all_16_0_6 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (211) can reduce 68 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (68) ~ (all_16_0_6 = 0) % 30.18/7.94 | (301) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 | Instantiating (301) with all_148_0_43, all_148_1_44, all_148_2_45, all_148_3_46 yields: % 30.18/7.94 | (302) apart_point_and_line(all_1_2_2, all_1_4_4) = all_148_1_44 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_148_0_43 & distinct_lines(all_1_5_5, all_1_4_4) = all_148_2_45 & distinct_points(all_1_2_2, all_1_2_2) = all_148_3_46 & ( ~ (all_148_2_45 = 0) | ~ (all_148_3_46 = 0) | all_148_0_43 = 0 | all_148_1_44 = 0) % 30.18/7.94 | % 30.18/7.94 | Applying alpha-rule on (302) yields: % 30.18/7.94 | (303) apart_point_and_line(all_1_2_2, all_1_4_4) = all_148_1_44 % 30.18/7.94 | (304) apart_point_and_line(all_1_2_2, all_1_5_5) = all_148_0_43 % 30.18/7.94 | (305) distinct_points(all_1_2_2, all_1_2_2) = all_148_3_46 % 30.18/7.94 | (306) distinct_lines(all_1_5_5, all_1_4_4) = all_148_2_45 % 30.18/7.94 | (307) ~ (all_148_2_45 = 0) | ~ (all_148_3_46 = 0) | all_148_0_43 = 0 | all_148_1_44 = 0 % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (247), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (211) all_16_0_6 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (211) can reduce 68 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (68) ~ (all_16_0_6 = 0) % 30.18/7.94 | (311) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 | Instantiating (311) with all_153_0_47, all_153_1_48, all_153_2_49, all_153_3_50 yields: % 30.18/7.94 | (312) apart_point_and_line(all_18_1_9, all_1_5_5) = all_153_1_48 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_153_0_47 & distinct_lines(all_1_5_5, all_1_5_5) = all_153_2_49 & distinct_points(all_18_1_9, all_1_2_2) = all_153_3_50 & ( ~ (all_153_2_49 = 0) | ~ (all_153_3_50 = 0) | all_153_0_47 = 0 | all_153_1_48 = 0) % 30.18/7.94 | % 30.18/7.94 | Applying alpha-rule on (312) yields: % 30.18/7.94 | (313) apart_point_and_line(all_18_1_9, all_1_5_5) = all_153_1_48 % 30.18/7.94 | (314) distinct_lines(all_1_5_5, all_1_5_5) = all_153_2_49 % 30.18/7.94 | (315) apart_point_and_line(all_1_2_2, all_1_5_5) = all_153_0_47 % 30.18/7.94 | (316) distinct_points(all_18_1_9, all_1_2_2) = all_153_3_50 % 30.18/7.94 | (317) ~ (all_153_2_49 = 0) | ~ (all_153_3_50 = 0) | all_153_0_47 = 0 | all_153_1_48 = 0 % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (255), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (211) all_16_0_6 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (211) can reduce 68 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (68) ~ (all_16_0_6 = 0) % 30.18/7.94 | (321) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 | Instantiating (321) with all_158_0_51, all_158_1_52, all_158_2_53, all_158_3_54 yields: % 30.18/7.94 | (322) apart_point_and_line(all_20_1_11, all_1_5_5) = all_158_0_51 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_158_1_52 & distinct_lines(all_1_4_4, all_1_5_5) = all_158_2_53 & distinct_points(all_1_2_2, all_20_1_11) = all_158_3_54 & ( ~ (all_158_2_53 = 0) | ~ (all_158_3_54 = 0) | all_158_0_51 = 0 | all_158_1_52 = 0) % 30.18/7.94 | % 30.18/7.94 | Applying alpha-rule on (322) yields: % 30.18/7.94 | (323) distinct_lines(all_1_4_4, all_1_5_5) = all_158_2_53 % 30.18/7.94 | (324) ~ (all_158_2_53 = 0) | ~ (all_158_3_54 = 0) | all_158_0_51 = 0 | all_158_1_52 = 0 % 30.18/7.94 | (325) apart_point_and_line(all_1_2_2, all_1_4_4) = all_158_1_52 % 30.18/7.94 | (326) distinct_points(all_1_2_2, all_20_1_11) = all_158_3_54 % 30.18/7.94 | (327) apart_point_and_line(all_20_1_11, all_1_5_5) = all_158_0_51 % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (267), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (211) all_16_0_6 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (211) can reduce 68 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (68) ~ (all_16_0_6 = 0) % 30.18/7.94 | (331) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_5_5, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (271), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (211) all_16_0_6 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (211) can reduce 68 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (68) ~ (all_16_0_6 = 0) % 30.18/7.94 | (335) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_2_2, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (161), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (244) all_18_0_8 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (244) can reduce 72 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (72) ~ (all_18_0_8 = 0) % 30.18/7.94 | (339) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_5_5) = v3 & apart_point_and_line(all_18_1_9, all_1_5_5) = v2 & distinct_lines(all_1_5_5, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (180), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (280) all_32_0_22 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (280) can reduce 210 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (210) ~ (all_32_0_22 = 0) % 30.18/7.94 | (343) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.94 | % 30.18/7.94 +-Applying beta-rule and splitting (204), into two cases. % 30.18/7.94 |-Branch one: % 30.18/7.94 | (280) all_32_0_22 = 0 % 30.18/7.94 | % 30.18/7.94 | Equations (280) can reduce 210 to: % 30.18/7.94 | (109) $false % 30.18/7.94 | % 30.18/7.94 |-The branch is then unsatisfiable % 30.18/7.94 |-Branch two: % 30.18/7.94 | (210) ~ (all_32_0_22 = 0) % 30.18/7.94 | (347) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_2_2, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.94 | % 30.18/7.94 | Instantiating (347) with all_191_0_71, all_191_1_72, all_191_2_73 yields: % 30.18/7.94 | (348) apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_0_71 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_1_72 & distinct_lines(all_1_4_4, all_1_4_4) = all_191_2_73 & ( ~ (all_191_2_73 = 0) | all_191_0_71 = 0 | all_191_1_72 = 0) % 30.18/7.94 | % 30.18/7.94 | Applying alpha-rule on (348) yields: % 30.18/7.94 | (349) apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_0_71 % 30.18/7.94 | (350) apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_1_72 % 30.18/7.94 | (351) distinct_lines(all_1_4_4, all_1_4_4) = all_191_2_73 % 30.18/7.94 | (352) ~ (all_191_2_73 = 0) | all_191_0_71 = 0 | all_191_1_72 = 0 % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (206), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (232) all_26_0_16 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (232) can reduce 88 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (88) ~ (all_26_0_16 = 0) % 30.18/7.95 | (356) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & distinct_lines(all_1_4_4, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (166), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (360) all_20_0_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (167), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (364) all_20_0_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (181), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (232) all_26_0_16 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (232) can reduce 88 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (88) ~ (all_26_0_16 = 0) % 30.18/7.95 | (368) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (168), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (372) all_20_0_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_20_1_11, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (169), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (376) all_20_0_10 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (172), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (380) all_24_0_14 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (170), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (384) all_22_0_12 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (182), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (232) all_26_0_16 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (232) can reduce 88 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (88) ~ (all_26_0_16 = 0) % 30.18/7.95 | (388) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (183), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (232) all_26_0_16 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (232) can reduce 88 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (88) ~ (all_26_0_16 = 0) % 30.18/7.95 | (392) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & apart_point_and_line(all_1_2_2, all_1_3_3) = v3 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (174), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (396) all_24_0_14 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (175), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (400) all_24_0_14 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (184), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (232) all_26_0_16 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (232) can reduce 88 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (88) ~ (all_26_0_16 = 0) % 30.18/7.95 | (404) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & apart_point_and_line(all_1_2_2, all_1_3_3) = v2 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_2_2, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (157), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (220) all_22_0_12 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (220) can reduce 80 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (80) ~ (all_22_0_12 = 0) % 30.18/7.95 | (408) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_20_1_11, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (176), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (412) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (177), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (416) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (171), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (420) all_22_0_12 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (173), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (424) all_24_0_14 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.95 | % 30.18/7.95 +-Applying beta-rule and splitting (178), into two cases. % 30.18/7.95 |-Branch one: % 30.18/7.95 | (280) all_32_0_22 = 0 % 30.18/7.95 | % 30.18/7.95 | Equations (280) can reduce 210 to: % 30.18/7.95 | (109) $false % 30.18/7.95 | % 30.18/7.95 |-The branch is then unsatisfiable % 30.18/7.95 |-Branch two: % 30.18/7.95 | (210) ~ (all_32_0_22 = 0) % 30.18/7.95 | (428) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (179), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (280) all_32_0_22 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (280) can reduce 210 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (210) ~ (all_32_0_22 = 0) % 30.18/7.96 | (432) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (160), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (220) all_22_0_12 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (220) can reduce 80 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (80) ~ (all_22_0_12 = 0) % 30.18/7.96 | (436) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_18_1_9, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (158), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (220) all_22_0_12 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (220) can reduce 80 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (80) ~ (all_22_0_12 = 0) % 30.18/7.96 | (440) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_18_1_9, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (159), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (220) all_22_0_12 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (220) can reduce 80 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (80) ~ (all_22_0_12 = 0) % 30.18/7.96 | (444) all_18_0_8 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (164), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (280) all_32_0_22 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (280) can reduce 210 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (210) ~ (all_32_0_22 = 0) % 30.18/7.96 | (448) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (162), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (280) all_32_0_22 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (280) can reduce 210 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (210) ~ (all_32_0_22 = 0) % 30.18/7.96 | (452) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_4_4) = v2 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (163), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (280) all_32_0_22 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (280) can reduce 210 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (210) ~ (all_32_0_22 = 0) % 30.18/7.96 | (456) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_3_3) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (165), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (280) all_32_0_22 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (280) can reduce 210 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (210) ~ (all_32_0_22 = 0) % 30.18/7.96 | (460) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_3_3) = v2 & apart_point_and_line(all_1_1_1, all_1_4_4) = v3 & distinct_lines(all_1_3_3, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (155), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (244) all_18_0_8 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (244) can reduce 72 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (72) ~ (all_18_0_8 = 0) % 30.18/7.96 | (464) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_3_3) = v3 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_3_3, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (156), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (244) all_18_0_8 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (244) can reduce 72 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (72) ~ (all_18_0_8 = 0) % 30.18/7.96 | (468) all_1_0_0 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_3_3) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_3_3) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (197), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (280) all_32_0_22 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (280) can reduce 210 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (210) ~ (all_32_0_22 = 0) % 30.18/7.96 | (472) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (195), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (280) all_32_0_22 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (280) can reduce 210 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (210) ~ (all_32_0_22 = 0) % 30.18/7.96 | (476) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (223), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (211) all_16_0_6 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (211) can reduce 68 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (68) ~ (all_16_0_6 = 0) % 30.18/7.96 | (480) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_20_1_11, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 | Instantiating (480) with all_369_0_81, all_369_1_82, all_369_2_83, all_369_3_84 yields: % 30.18/7.96 | (481) apart_point_and_line(all_20_1_11, all_1_5_5) = all_369_1_82 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_369_0_81 & distinct_lines(all_1_4_4, all_1_5_5) = all_369_2_83 & distinct_points(all_20_1_11, all_1_2_2) = all_369_3_84 & ( ~ (all_369_2_83 = 0) | ~ (all_369_3_84 = 0) | all_369_0_81 = 0 | all_369_1_82 = 0) % 30.18/7.96 | % 30.18/7.96 | Applying alpha-rule on (481) yields: % 30.18/7.96 | (482) apart_point_and_line(all_20_1_11, all_1_5_5) = all_369_1_82 % 30.18/7.96 | (483) ~ (all_369_2_83 = 0) | ~ (all_369_3_84 = 0) | all_369_0_81 = 0 | all_369_1_82 = 0 % 30.18/7.96 | (484) apart_point_and_line(all_1_2_2, all_1_4_4) = all_369_0_81 % 30.18/7.96 | (485) distinct_lines(all_1_4_4, all_1_5_5) = all_369_2_83 % 30.18/7.96 | (486) distinct_points(all_20_1_11, all_1_2_2) = all_369_3_84 % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (231), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (211) all_16_0_6 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (211) can reduce 68 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (68) ~ (all_16_0_6 = 0) % 30.18/7.96 | (490) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_1_2_2, all_1_4_4) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_1_2_2) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 | Instantiating (490) with all_374_0_85, all_374_1_86, all_374_2_87, all_374_3_88 yields: % 30.18/7.96 | (491) apart_point_and_line(all_20_1_11, all_1_5_5) = all_374_1_86 & apart_point_and_line(all_1_2_2, all_1_4_4) = all_374_0_85 & distinct_lines(all_1_5_5, all_1_4_4) = all_374_2_87 & distinct_points(all_20_1_11, all_1_2_2) = all_374_3_88 & ( ~ (all_374_2_87 = 0) | ~ (all_374_3_88 = 0) | all_374_0_85 = 0 | all_374_1_86 = 0) % 30.18/7.96 | % 30.18/7.96 | Applying alpha-rule on (491) yields: % 30.18/7.96 | (492) ~ (all_374_2_87 = 0) | ~ (all_374_3_88 = 0) | all_374_0_85 = 0 | all_374_1_86 = 0 % 30.18/7.96 | (493) apart_point_and_line(all_1_2_2, all_1_4_4) = all_374_0_85 % 30.18/7.96 | (494) distinct_lines(all_1_5_5, all_1_4_4) = all_374_2_87 % 30.18/7.96 | (495) distinct_points(all_20_1_11, all_1_2_2) = all_374_3_88 % 30.18/7.96 | (496) apart_point_and_line(all_20_1_11, all_1_5_5) = all_374_1_86 % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (408), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (244) all_18_0_8 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (244) can reduce 72 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (72) ~ (all_18_0_8 = 0) % 30.18/7.96 | (500) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_20_1_11, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.96 | % 30.18/7.96 +-Applying beta-rule and splitting (412), into two cases. % 30.18/7.96 |-Branch one: % 30.18/7.96 | (244) all_18_0_8 = 0 % 30.18/7.96 | % 30.18/7.96 | Equations (244) can reduce 72 to: % 30.18/7.96 | (109) $false % 30.18/7.96 | % 30.18/7.96 |-The branch is then unsatisfiable % 30.18/7.96 |-Branch two: % 30.18/7.96 | (72) ~ (all_18_0_8 = 0) % 30.18/7.96 | (504) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & apart_point_and_line(all_1_1_1, all_1_5_5) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_18_1_9, all_1_1_1) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.97 | % 30.18/7.97 | Instantiating (504) with all_414_0_117, all_414_1_118, all_414_2_119, all_414_3_120 yields: % 30.18/7.97 | (505) apart_point_and_line(all_18_1_9, all_1_4_4) = all_414_1_118 & apart_point_and_line(all_1_1_1, all_1_5_5) = all_414_0_117 & distinct_lines(all_1_5_5, all_1_4_4) = all_414_2_119 & distinct_points(all_18_1_9, all_1_1_1) = all_414_3_120 & ( ~ (all_414_2_119 = 0) | ~ (all_414_3_120 = 0) | all_414_0_117 = 0 | all_414_1_118 = 0) % 30.18/7.97 | % 30.18/7.97 | Applying alpha-rule on (505) yields: % 30.18/7.97 | (506) apart_point_and_line(all_18_1_9, all_1_4_4) = all_414_1_118 % 30.18/7.97 | (507) apart_point_and_line(all_1_1_1, all_1_5_5) = all_414_0_117 % 30.18/7.97 | (508) ~ (all_414_2_119 = 0) | ~ (all_414_3_120 = 0) | all_414_0_117 = 0 | all_414_1_118 = 0 % 30.18/7.97 | (509) distinct_lines(all_1_5_5, all_1_4_4) = all_414_2_119 % 30.18/7.97 | (510) distinct_points(all_18_1_9, all_1_1_1) = all_414_3_120 % 30.18/7.97 | % 30.18/7.97 +-Applying beta-rule and splitting (416), into two cases. % 30.18/7.97 |-Branch one: % 30.18/7.97 | (244) all_18_0_8 = 0 % 30.18/7.97 | % 30.18/7.97 | Equations (244) can reduce 72 to: % 30.18/7.97 | (109) $false % 30.18/7.97 | % 30.18/7.97 |-The branch is then unsatisfiable % 30.18/7.97 |-Branch two: % 30.18/7.97 | (72) ~ (all_18_0_8 = 0) % 30.18/7.97 | (514) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_1_1, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.97 | % 30.18/7.97 | Instantiating (514) with all_419_0_121, all_419_1_122, all_419_2_123, all_419_3_124 yields: % 30.18/7.97 | (515) apart_point_and_line(all_18_1_9, all_1_4_4) = all_419_0_121 & apart_point_and_line(all_1_1_1, all_1_5_5) = all_419_1_122 & distinct_lines(all_1_4_4, all_1_5_5) = all_419_2_123 & distinct_points(all_1_1_1, all_18_1_9) = all_419_3_124 & ( ~ (all_419_2_123 = 0) | ~ (all_419_3_124 = 0) | all_419_0_121 = 0 | all_419_1_122 = 0) % 30.18/7.97 | % 30.18/7.97 | Applying alpha-rule on (515) yields: % 30.18/7.97 | (516) distinct_points(all_1_1_1, all_18_1_9) = all_419_3_124 % 30.18/7.97 | (517) apart_point_and_line(all_18_1_9, all_1_4_4) = all_419_0_121 % 30.18/7.97 | (518) ~ (all_419_2_123 = 0) | ~ (all_419_3_124 = 0) | all_419_0_121 = 0 | all_419_1_122 = 0 % 30.18/7.97 | (519) apart_point_and_line(all_1_1_1, all_1_5_5) = all_419_1_122 % 30.18/7.97 | (520) distinct_lines(all_1_4_4, all_1_5_5) = all_419_2_123 % 30.18/7.97 | % 30.18/7.97 +-Applying beta-rule and splitting (440), into two cases. % 30.18/7.97 |-Branch one: % 30.18/7.97 | (244) all_18_0_8 = 0 % 30.18/7.97 | % 30.18/7.97 | Equations (244) can reduce 72 to: % 30.18/7.97 | (109) $false % 30.18/7.97 | % 30.18/7.97 |-The branch is then unsatisfiable % 30.18/7.97 |-Branch two: % 30.18/7.97 | (72) ~ (all_18_0_8 = 0) % 30.18/7.97 | (524) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v3 & apart_point_and_line(all_18_1_9, all_1_4_4) = v2 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_18_1_9, all_20_1_11) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.97 | % 30.18/7.97 | Instantiating (524) with all_429_0_129, all_429_1_130, all_429_2_131, all_429_3_132 yields: % 30.18/7.97 | (525) apart_point_and_line(all_20_1_11, all_1_5_5) = all_429_0_129 & apart_point_and_line(all_18_1_9, all_1_4_4) = all_429_1_130 & distinct_lines(all_1_5_5, all_1_4_4) = all_429_2_131 & distinct_points(all_18_1_9, all_20_1_11) = all_429_3_132 & ( ~ (all_429_2_131 = 0) | ~ (all_429_3_132 = 0) | all_429_0_129 = 0 | all_429_1_130 = 0) % 30.18/7.97 | % 30.18/7.97 | Applying alpha-rule on (525) yields: % 30.18/7.97 | (526) distinct_points(all_18_1_9, all_20_1_11) = all_429_3_132 % 30.18/7.97 | (527) ~ (all_429_2_131 = 0) | ~ (all_429_3_132 = 0) | all_429_0_129 = 0 | all_429_1_130 = 0 % 30.18/7.97 | (528) apart_point_and_line(all_18_1_9, all_1_4_4) = all_429_1_130 % 30.18/7.97 | (529) distinct_lines(all_1_5_5, all_1_4_4) = all_429_2_131 % 30.18/7.97 | (530) apart_point_and_line(all_20_1_11, all_1_5_5) = all_429_0_129 % 30.18/7.97 | % 30.18/7.97 +-Applying beta-rule and splitting (444), into two cases. % 30.18/7.97 |-Branch one: % 30.18/7.97 | (244) all_18_0_8 = 0 % 30.18/7.97 | % 30.18/7.97 | Equations (244) can reduce 72 to: % 30.18/7.97 | (109) $false % 30.18/7.97 | % 30.18/7.97 |-The branch is then unsatisfiable % 30.18/7.97 |-Branch two: % 30.18/7.97 | (72) ~ (all_18_0_8 = 0) % 30.18/7.97 | (534) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_20_1_11, all_1_5_5) = v2 & apart_point_and_line(all_18_1_9, all_1_4_4) = v3 & distinct_lines(all_1_5_5, all_1_4_4) = v1 & distinct_points(all_20_1_11, all_18_1_9) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 30.18/7.97 | % 30.18/7.97 | Instantiating (534) with all_434_0_133, all_434_1_134, all_434_2_135, all_434_3_136 yields: % 30.18/7.97 | (535) apart_point_and_line(all_20_1_11, all_1_5_5) = all_434_1_134 & apart_point_and_line(all_18_1_9, all_1_4_4) = all_434_0_133 & distinct_lines(all_1_5_5, all_1_4_4) = all_434_2_135 & distinct_points(all_20_1_11, all_18_1_9) = all_434_3_136 & ( ~ (all_434_2_135 = 0) | ~ (all_434_3_136 = 0) | all_434_0_133 = 0 | all_434_1_134 = 0) % 30.18/7.97 | % 30.18/7.97 | Applying alpha-rule on (535) yields: % 30.18/7.97 | (536) ~ (all_434_2_135 = 0) | ~ (all_434_3_136 = 0) | all_434_0_133 = 0 | all_434_1_134 = 0 % 30.18/7.97 | (537) apart_point_and_line(all_18_1_9, all_1_4_4) = all_434_0_133 % 30.18/7.97 | (538) distinct_lines(all_1_5_5, all_1_4_4) = all_434_2_135 % 30.18/7.97 | (539) apart_point_and_line(all_20_1_11, all_1_5_5) = all_434_1_134 % 30.18/7.97 | (540) distinct_points(all_20_1_11, all_18_1_9) = all_434_3_136 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (27) with all_1_4_4, all_1_5_5, all_132_1_38, all_1_1_1 and discharging atoms intersection_point(all_1_4_4, all_1_5_5) = all_132_1_38, intersection_point(all_1_4_4, all_1_5_5) = all_1_1_1, yields: % 30.18/7.97 | (541) all_132_1_38 = all_1_1_1 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_1_1, all_1_5_5, all_419_1_122, all_34_0_24 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_419_1_122, apart_point_and_line(all_1_1_1, all_1_5_5) = all_34_0_24, yields: % 30.18/7.97 | (542) all_419_1_122 = all_34_0_24 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_1_1, all_1_5_5, all_414_0_117, all_419_1_122 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_419_1_122, apart_point_and_line(all_1_1_1, all_1_5_5) = all_414_0_117, yields: % 30.18/7.97 | (543) all_419_1_122 = all_414_0_117 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_1_1, all_1_5_5, all_87_0_34, all_419_1_122 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_419_1_122, apart_point_and_line(all_1_1_1, all_1_5_5) = all_87_0_34, yields: % 30.18/7.97 | (544) all_419_1_122 = all_87_0_34 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_1_1, all_1_5_5, all_87_1_35, all_132_0_37 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_87_1_35, yields: % 30.18/7.97 | (545) all_132_0_37 = all_87_1_35 | ~ (apart_point_and_line(all_1_1_1, all_1_5_5) = all_132_0_37) % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_1_1, all_1_5_5, all_87_1_35, all_419_1_122 and discharging atoms apart_point_and_line(all_1_1_1, all_1_5_5) = all_419_1_122, apart_point_and_line(all_1_1_1, all_1_5_5) = all_87_1_35, yields: % 30.18/7.97 | (546) all_419_1_122 = all_87_1_35 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_374_0_85, all_26_0_16 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_374_0_85, apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, yields: % 30.18/7.97 | (547) all_374_0_85 = all_26_0_16 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_191_0_71, all_369_0_81 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_369_0_81, apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_0_71, yields: % 30.18/7.97 | (548) all_369_0_81 = all_191_0_71 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_191_1_72, all_374_0_85 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_374_0_85, apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_1_72, yields: % 30.18/7.97 | (549) all_374_0_85 = all_191_1_72 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_191_1_72, all_191_0_71 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_0_71, apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_1_72, yields: % 30.18/7.97 | (550) all_191_0_71 = all_191_1_72 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_158_1_52, all_369_0_81 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_369_0_81, apart_point_and_line(all_1_2_2, all_1_4_4) = all_158_1_52, yields: % 30.18/7.97 | (551) all_369_0_81 = all_158_1_52 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_148_1_44, all_374_0_85 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_374_0_85, apart_point_and_line(all_1_2_2, all_1_4_4) = all_148_1_44, yields: % 30.18/7.97 | (552) all_374_0_85 = all_148_1_44 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_143_1_40, all_191_1_72 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_191_1_72, apart_point_and_line(all_1_2_2, all_1_4_4) = all_143_1_40, yields: % 30.18/7.97 | (553) all_191_1_72 = all_143_1_40 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_5_5, all_153_0_47, all_16_0_6 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_153_0_47, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.97 | (554) all_153_0_47 = all_16_0_6 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (8) with all_1_2_2, all_1_5_5, all_148_0_43, all_153_0_47 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_153_0_47, apart_point_and_line(all_1_2_2, all_1_5_5) = all_148_0_43, yields: % 30.18/7.97 | (555) all_153_0_47 = all_148_0_43 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (14) with all_1_5_5, all_1_4_4, all_414_2_119, all_429_2_131 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = all_429_2_131, distinct_lines(all_1_5_5, all_1_4_4) = all_414_2_119, yields: % 30.18/7.97 | (556) all_429_2_131 = all_414_2_119 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (14) with all_1_5_5, all_1_4_4, all_374_2_87, all_434_2_135 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = all_434_2_135, distinct_lines(all_1_5_5, all_1_4_4) = all_374_2_87, yields: % 30.18/7.97 | (557) all_434_2_135 = all_374_2_87 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (14) with all_1_5_5, all_1_4_4, all_374_2_87, all_414_2_119 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = all_414_2_119, distinct_lines(all_1_5_5, all_1_4_4) = all_374_2_87, yields: % 30.18/7.97 | (558) all_414_2_119 = all_374_2_87 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (14) with all_1_5_5, all_1_4_4, all_148_2_45, all_429_2_131 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = all_429_2_131, distinct_lines(all_1_5_5, all_1_4_4) = all_148_2_45, yields: % 30.18/7.97 | (559) all_429_2_131 = all_148_2_45 % 30.18/7.97 | % 30.18/7.97 | Instantiating formula (14) with all_1_5_5, all_1_4_4, all_143_2_41, all_434_2_135 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = all_434_2_135, distinct_lines(all_1_5_5, all_1_4_4) = all_143_2_41, yields: % 30.18/7.97 | (560) all_434_2_135 = all_143_2_41 % 30.18/7.97 | % 30.18/7.97 | Combining equations (557,560) yields a new equation: % 30.18/7.97 | (561) all_374_2_87 = all_143_2_41 % 30.18/7.97 | % 30.18/7.97 | Simplifying 561 yields: % 30.18/7.97 | (562) all_374_2_87 = all_143_2_41 % 30.18/7.97 | % 30.18/7.97 | Combining equations (556,559) yields a new equation: % 30.18/7.97 | (563) all_414_2_119 = all_148_2_45 % 30.18/7.97 | % 30.18/7.97 | Simplifying 563 yields: % 30.18/7.97 | (564) all_414_2_119 = all_148_2_45 % 30.18/7.97 | % 30.18/7.97 | Combining equations (544,543) yields a new equation: % 30.18/7.97 | (565) all_414_0_117 = all_87_0_34 % 30.18/7.97 | % 30.18/7.97 | Combining equations (542,543) yields a new equation: % 30.18/7.97 | (566) all_414_0_117 = all_34_0_24 % 30.18/7.97 | % 30.18/7.97 | Combining equations (546,543) yields a new equation: % 30.18/7.97 | (567) all_414_0_117 = all_87_1_35 % 30.18/7.97 | % 30.18/7.97 | Combining equations (566,565) yields a new equation: % 30.18/7.97 | (568) all_87_0_34 = all_34_0_24 % 30.18/7.97 | % 30.18/7.97 | Combining equations (567,565) yields a new equation: % 30.18/7.97 | (569) all_87_0_34 = all_87_1_35 % 30.18/7.97 | % 30.18/7.97 | Combining equations (558,564) yields a new equation: % 30.18/7.97 | (570) all_374_2_87 = all_148_2_45 % 30.18/7.97 | % 30.18/7.97 | Simplifying 570 yields: % 30.18/7.97 | (571) all_374_2_87 = all_148_2_45 % 30.18/7.97 | % 30.18/7.97 | Combining equations (547,552) yields a new equation: % 30.18/7.97 | (572) all_148_1_44 = all_26_0_16 % 30.18/7.97 | % 30.18/7.97 | Combining equations (549,552) yields a new equation: % 30.18/7.97 | (573) all_191_1_72 = all_148_1_44 % 30.18/7.97 | % 30.18/7.97 | Simplifying 573 yields: % 30.18/7.97 | (574) all_191_1_72 = all_148_1_44 % 30.18/7.98 | % 30.18/7.98 | Combining equations (562,571) yields a new equation: % 30.18/7.98 | (575) all_148_2_45 = all_143_2_41 % 30.18/7.98 | % 30.18/7.98 | Combining equations (548,551) yields a new equation: % 30.18/7.98 | (576) all_191_0_71 = all_158_1_52 % 30.18/7.98 | % 30.18/7.98 | Simplifying 576 yields: % 30.18/7.98 | (577) all_191_0_71 = all_158_1_52 % 30.18/7.98 | % 30.18/7.98 | Combining equations (550,577) yields a new equation: % 30.18/7.98 | (578) all_191_1_72 = all_158_1_52 % 30.18/7.98 | % 30.18/7.98 | Simplifying 578 yields: % 30.18/7.98 | (579) all_191_1_72 = all_158_1_52 % 30.18/7.98 | % 30.18/7.98 | Combining equations (553,579) yields a new equation: % 30.18/7.98 | (580) all_158_1_52 = all_143_1_40 % 30.18/7.98 | % 30.18/7.98 | Combining equations (574,579) yields a new equation: % 30.18/7.98 | (581) all_158_1_52 = all_148_1_44 % 30.18/7.98 | % 30.18/7.98 | Combining equations (581,580) yields a new equation: % 30.18/7.98 | (582) all_148_1_44 = all_143_1_40 % 30.18/7.98 | % 30.18/7.98 | Simplifying 582 yields: % 30.18/7.98 | (583) all_148_1_44 = all_143_1_40 % 30.18/7.98 | % 30.18/7.98 | Combining equations (554,555) yields a new equation: % 30.18/7.98 | (584) all_148_0_43 = all_16_0_6 % 30.18/7.98 | % 30.18/7.98 | Combining equations (572,583) yields a new equation: % 30.18/7.98 | (585) all_143_1_40 = all_26_0_16 % 30.18/7.98 | % 30.18/7.98 | Combining equations (569,568) yields a new equation: % 30.18/7.98 | (586) all_87_1_35 = all_34_0_24 % 30.18/7.98 | % 30.18/7.98 | Simplifying 586 yields: % 30.18/7.98 | (587) all_87_1_35 = all_34_0_24 % 30.18/7.98 | % 30.18/7.98 | From (541) and (279) follows: % 30.18/7.98 | (588) apart_point_and_line(all_1_1_1, all_1_5_5) = all_132_0_37 % 30.18/7.98 | % 30.18/7.98 | From (585) and (293) follows: % 30.18/7.98 | (134) apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16 % 30.18/7.98 | % 30.18/7.98 | From (584) and (304) follows: % 30.18/7.98 | (137) apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6 % 30.18/7.98 | % 30.18/7.98 | From (575) and (306) follows: % 30.18/7.98 | (296) distinct_lines(all_1_5_5, all_1_4_4) = all_143_2_41 % 30.18/7.98 | % 30.18/7.98 +-Applying beta-rule and splitting (545), into two cases. % 30.18/7.98 |-Branch one: % 30.18/7.98 | (592) ~ (apart_point_and_line(all_1_1_1, all_1_5_5) = all_132_0_37) % 30.18/7.98 | % 30.18/7.98 | Using (588) and (592) yields: % 30.18/7.98 | (144) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (588) apart_point_and_line(all_1_1_1, all_1_5_5) = all_132_0_37 % 30.18/7.98 | (595) all_132_0_37 = all_87_1_35 % 30.18/7.98 | % 30.18/7.98 | Combining equations (587,595) yields a new equation: % 30.18/7.98 | (596) all_132_0_37 = all_34_0_24 % 30.18/7.98 | % 30.18/7.98 | Equations (596) can reduce 277 to: % 30.18/7.98 | (597) ~ (all_34_0_24 = 0) % 30.18/7.98 | % 30.18/7.98 +-Applying beta-rule and splitting (205), into two cases. % 30.18/7.98 |-Branch one: % 30.18/7.98 | (598) all_34_0_24 = 0 % 30.18/7.98 | % 30.18/7.98 | Equations (598) can reduce 597 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (597) ~ (all_34_0_24 = 0) % 30.18/7.98 | (601) all_32_0_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 & distinct_lines(all_1_5_5, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.98 | % 30.18/7.98 +-Applying beta-rule and splitting (601), into two cases. % 30.18/7.98 |-Branch one: % 30.18/7.98 | (280) all_32_0_22 = 0 % 30.18/7.98 | % 30.18/7.98 | Equations (280) can reduce 210 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (210) ~ (all_32_0_22 = 0) % 30.18/7.98 | (605) ? [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 & distinct_lines(all_1_5_5, all_1_4_4) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.98 | % 30.18/7.98 | Instantiating (605) with all_490_0_157, all_490_1_158, all_490_2_159 yields: % 30.18/7.98 | (606) apart_point_and_line(all_1_2_2, all_1_4_4) = all_490_0_157 & apart_point_and_line(all_1_2_2, all_1_5_5) = all_490_1_158 & distinct_lines(all_1_5_5, all_1_4_4) = all_490_2_159 & ( ~ (all_490_2_159 = 0) | all_490_0_157 = 0 | all_490_1_158 = 0) % 30.18/7.98 | % 30.18/7.98 | Applying alpha-rule on (606) yields: % 30.18/7.98 | (607) apart_point_and_line(all_1_2_2, all_1_4_4) = all_490_0_157 % 30.18/7.98 | (608) apart_point_and_line(all_1_2_2, all_1_5_5) = all_490_1_158 % 30.18/7.98 | (609) distinct_lines(all_1_5_5, all_1_4_4) = all_490_2_159 % 30.18/7.98 | (610) ~ (all_490_2_159 = 0) | all_490_0_157 = 0 | all_490_1_158 = 0 % 30.18/7.98 | % 30.18/7.98 | Instantiating formula (8) with all_1_2_2, all_1_4_4, all_490_0_157, all_26_0_16 and discharging atoms apart_point_and_line(all_1_2_2, all_1_4_4) = all_490_0_157, apart_point_and_line(all_1_2_2, all_1_4_4) = all_26_0_16, yields: % 30.18/7.98 | (611) all_490_0_157 = all_26_0_16 % 30.18/7.98 | % 30.18/7.98 | Instantiating formula (8) with all_1_2_2, all_1_5_5, all_490_1_158, all_16_0_6 and discharging atoms apart_point_and_line(all_1_2_2, all_1_5_5) = all_490_1_158, apart_point_and_line(all_1_2_2, all_1_5_5) = all_16_0_6, yields: % 30.18/7.98 | (612) all_490_1_158 = all_16_0_6 % 30.18/7.98 | % 30.18/7.98 | Instantiating formula (14) with all_1_5_5, all_1_4_4, all_490_2_159, all_143_2_41 and discharging atoms distinct_lines(all_1_5_5, all_1_4_4) = all_490_2_159, distinct_lines(all_1_5_5, all_1_4_4) = all_143_2_41, yields: % 30.18/7.98 | (613) all_490_2_159 = all_143_2_41 % 30.18/7.98 | % 30.18/7.98 | From (613) and (609) follows: % 30.18/7.98 | (296) distinct_lines(all_1_5_5, all_1_4_4) = all_143_2_41 % 30.18/7.98 | % 30.18/7.98 +-Applying beta-rule and splitting (207), into two cases. % 30.18/7.98 |-Branch one: % 30.18/7.98 | (232) all_26_0_16 = 0 % 30.18/7.98 | % 30.18/7.98 | Equations (232) can reduce 88 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (88) ~ (all_26_0_16 = 0) % 30.18/7.98 | (618) all_16_0_6 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.98 | % 30.18/7.98 +-Applying beta-rule and splitting (618), into two cases. % 30.18/7.98 |-Branch one: % 30.18/7.98 | (211) all_16_0_6 = 0 % 30.18/7.98 | % 30.18/7.98 | Equations (211) can reduce 68 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (68) ~ (all_16_0_6 = 0) % 30.18/7.98 | (622) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_1_1, all_1_4_4) = v1 & apart_point_and_line(all_1_1_1, all_1_5_5) = v2 & distinct_lines(all_1_4_4, all_1_5_5) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 30.18/7.98 | % 30.18/7.98 +-Applying beta-rule and splitting (610), into two cases. % 30.18/7.98 |-Branch one: % 30.18/7.98 | (623) ~ (all_490_2_159 = 0) % 30.18/7.98 | % 30.18/7.98 | Equations (613) can reduce 623 to: % 30.18/7.98 | (624) ~ (all_143_2_41 = 0) % 30.18/7.98 | % 30.18/7.98 | Instantiating formula (33) with all_143_2_41, all_1_4_4, all_1_5_5, all_1_4_4 and discharging atoms convergent_lines(all_1_4_4, all_1_5_5) = 0, distinct_lines(all_1_5_5, all_1_4_4) = all_143_2_41, ~ (convergent_lines(all_1_4_4, all_1_4_4) = 0), yields: % 30.18/7.98 | (625) all_143_2_41 = 0 % 30.18/7.98 | % 30.18/7.98 | Equations (625) can reduce 624 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (627) all_490_2_159 = 0 % 30.18/7.98 | (628) all_490_0_157 = 0 | all_490_1_158 = 0 % 30.18/7.98 | % 30.18/7.98 +-Applying beta-rule and splitting (628), into two cases. % 30.18/7.98 |-Branch one: % 30.18/7.98 | (629) all_490_0_157 = 0 % 30.18/7.98 | % 30.18/7.98 | Combining equations (629,611) yields a new equation: % 30.18/7.98 | (232) all_26_0_16 = 0 % 30.18/7.98 | % 30.18/7.98 | Equations (232) can reduce 88 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (632) ~ (all_490_0_157 = 0) % 30.18/7.98 | (633) all_490_1_158 = 0 % 30.18/7.98 | % 30.18/7.98 | Combining equations (633,612) yields a new equation: % 30.18/7.98 | (211) all_16_0_6 = 0 % 30.18/7.98 | % 30.18/7.98 | Equations (211) can reduce 68 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (280) all_32_0_22 = 0 % 30.18/7.98 | (637) ~ (all_32_1_23 = 0) % 30.18/7.98 | % 30.18/7.98 | Equations (202) can reduce 637 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (639) all_28_0_18 = 0 % 30.18/7.98 | (640) ~ (all_28_1_19 = 0) % 30.18/7.98 | % 30.18/7.98 | Equations (131) can reduce 640 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (642) all_30_0_20 = 0 % 30.18/7.98 | (643) ~ (all_30_1_21 = 0) % 30.18/7.98 | % 30.18/7.98 | Equations (127) can reduce 643 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 |-Branch two: % 30.18/7.98 | (645) ~ (distinct_points(all_1_2_2, all_1_1_1) = 0) % 30.18/7.98 | (108) all_1_0_0 = 0 % 30.18/7.98 | % 30.18/7.98 | Equations (108) can reduce 52 to: % 30.18/7.98 | (109) $false % 30.18/7.98 | % 30.18/7.98 |-The branch is then unsatisfiable % 30.18/7.98 % SZS output end Proof for theBenchmark % 30.18/7.98 % 30.18/7.98 7382ms %------------------------------------------------------------------------------