%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GEO189+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n029.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:26 EDT 2022 % Result : Theorem 12.64s 3.64s % Output : Proof 19.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GEO189+2 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sat Jun 18 08:35:29 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.58 ____ _ % 0.19/0.58 ___ / __ \_____(_)___ ________ __________ % 0.19/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.19/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.19/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.19/0.58 % 0.19/0.58 A Theorem Prover for First-Order Logic % 0.19/0.58 (ePrincess v.1.0) % 0.19/0.58 % 0.19/0.58 (c) Philipp Rümmer, 2009-2015 % 0.19/0.58 (c) Peter Backeman, 2014-2015 % 0.19/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.19/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.19/0.58 Bug reports to peter@backeman.se % 0.19/0.58 % 0.19/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.19/0.58 % 0.19/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.66/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.60/0.93 Prover 0: Preprocessing ... % 1.84/1.06 Prover 0: Warning: ignoring some quantifiers % 1.99/1.08 Prover 0: Constructing countermodel ... % 2.66/1.26 Prover 0: gave up % 2.66/1.26 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.66/1.29 Prover 1: Preprocessing ... % 2.94/1.38 Prover 1: Constructing countermodel ... % 3.28/1.44 Prover 1: gave up % 3.28/1.44 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.35/1.46 Prover 2: Preprocessing ... % 3.80/1.58 Prover 2: Warning: ignoring some quantifiers % 3.80/1.58 Prover 2: Constructing countermodel ... % 4.41/1.73 Prover 2: gave up % 4.41/1.73 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 4.41/1.75 Prover 3: Preprocessing ... % 4.76/1.76 Prover 3: Warning: ignoring some quantifiers % 4.76/1.77 Prover 3: Constructing countermodel ... % 4.86/1.81 Prover 3: gave up % 4.86/1.81 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 4.86/1.82 Prover 4: Preprocessing ... % 5.20/1.89 Prover 4: Warning: ignoring some quantifiers % 5.20/1.89 Prover 4: Constructing countermodel ... % 10.09/3.03 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 10.09/3.05 Prover 5: Preprocessing ... % 10.40/3.13 Prover 5: Constructing countermodel ... % 12.64/3.63 Prover 5: proved (605ms) % 12.64/3.63 Prover 4: stopped % 12.64/3.64 % 12.64/3.64 No countermodel exists, formula is valid % 12.64/3.64 % SZS status Theorem for theBenchmark % 12.64/3.64 % 12.64/3.64 Generating proof ... found it (size 456) % 18.83/5.10 % 18.83/5.10 % SZS output start Proof for theBenchmark % 18.83/5.10 Assumed formulas after preprocessing and simplification: % 18.83/5.10 | (0) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v1, v2) = v4) | ~ (distinct_points(v0, v1) = 0) | ? [v6] : ? [v7] : ? [v8] : (apart_point_and_line(v0, v3) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_lines(v2, v3) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v0, v3) = v4) | ~ (distinct_lines(v2, v3) = 0) | ? [v6] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v2) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (apart_point_and_line(v1, v2) = v9 & apart_point_and_line(v0, v3) = v8 & distinct_lines(v2, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0 | v8 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v2) = v5) | ~ (apart_point_and_line(v0, v3) = v4) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (apart_point_and_line(v1, v3) = v9 & apart_point_and_line(v0, v2) = v8 & distinct_lines(v2, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0 | v8 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v2) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v2, v3) = 0) | ? [v6] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v3) = v8 & apart_point_and_line(v0, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v0, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_points(v0, v1) = 0) | ? [v6] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v3) = v8 & apart_point_and_line(v1, v2) = v7 & distinct_lines(v2, v3) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v2, v1) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_lines(v1, v2) = v4) | ~ (distinct_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_lines(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_points(v1, v2) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_points(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (intersection_point(v0, v1) = v3) | ~ (distinct_points(v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v1) = v7 & apart_point_and_line(v2, v0) = v6 & convergent_lines(v0, v1) = v5 & ( ~ (v5 = 0) | ( ~ (v7 = 0) & ~ (v6 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (intersection_point(v0, v1) = v4) | ~ (apart_point_and_line(v2, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v0) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v4) = v7 & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (intersection_point(v0, v1) = v4) | ~ (apart_point_and_line(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v1) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v4) = v7 & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (line_connecting(v0, v1) = v3) | ~ (distinct_points(v2, v1) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v3) = v6 & distinct_points(v2, v0) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (line_connecting(v0, v1) = v3) | ~ (distinct_points(v2, v0) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v3) = v6 & distinct_points(v2, v1) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & v4 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (apart_point_and_line(v2, v1) = v4) | ~ (apart_point_and_line(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (intersection_point(v0, v1) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v6) = v7 & ( ~ (v5 = 0) | v7 = 0)) | ( ~ (v4 = 0) & ~ (v3 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (distinct_points(v2, v1) = v4) | ~ (distinct_points(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (line_connecting(v0, v1) = v6 & apart_point_and_line(v2, v6) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v7 = 0) | ~ (v5 = 0))) | (v4 = 0 & v3 = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v2, v1) = v3) | ~ (apart_point_and_line(v0, v1) = 0) | distinct_points(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (apart_point_and_line(v0, v1) = 0) | distinct_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | apart_point_and_line(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = 0) | ~ (distinct_points(v0, v2) = v3) | apart_point_and_line(v2, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (line_connecting(v0, v1) = v3) | ~ (apart_point_and_line(v2, v3) = 0) | ? [v4] : ? [v5] : ? [v6] : (distinct_points(v2, v1) = v6 & distinct_points(v2, v0) = v5 & distinct_points(v0, v1) = v4 & ( ~ (v4 = 0) | (v6 = 0 & v5 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (apart_point_and_line(v2, v1) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (intersection_point(v0, v1) = v5 & apart_point_and_line(v2, v0) = v4 & distinct_points(v2, v5) = v6 & (v6 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (apart_point_and_line(v2, v0) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (intersection_point(v0, v1) = v5 & apart_point_and_line(v2, v1) = v4 & distinct_points(v2, v5) = v6 & (v6 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_lines(v2, v3) = 0) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v1, v3) = v7 & apart_point_and_line(v1, v2) = v6 & apart_point_and_line(v0, v3) = v5 & apart_point_and_line(v0, v2) = v4 & (v7 = 0 | v6 = 0 | v5 = 0 | v4 = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_points(v2, v1) = v3) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (line_connecting(v0, v1) = v4 & apart_point_and_line(v2, v4) = v5 & distinct_points(v2, v0) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_points(v2, v0) = v3) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (line_connecting(v0, v1) = v4 & apart_point_and_line(v2, v4) = v5 & distinct_points(v2, v1) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v3 = 0)))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (distinct_lines(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3)) & ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v0, v1) = 0) & ! [v0] : ~ (convergent_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_points(v0, v0) = 0) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v4 = 0) & line_connecting(v0, v2) = v5 & line_connecting(v0, v1) = v3 & apart_point_and_line(v2, v3) = v4 & apart_point_and_line(v1, v5) = 0 & distinct_points(v1, v2) = 0 & distinct_points(v0, v2) = 0 & distinct_points(v0, v1) = 0) % 19.16/5.16 | Applying alpha-rule on (0) yields: % 19.16/5.16 | (1) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (intersection_point(v0, v1) = v3) | ~ (distinct_points(v2, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v1) = v7 & apart_point_and_line(v2, v0) = v6 & convergent_lines(v0, v1) = v5 & ( ~ (v5 = 0) | ( ~ (v7 = 0) & ~ (v6 = 0))))) % 19.16/5.17 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v0, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_points(v0, v1) = 0) | ? [v6] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v3) = v8 & apart_point_and_line(v1, v2) = v7 & distinct_lines(v2, v3) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 19.16/5.17 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) % 19.16/5.17 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_lines(v1, v2) = v4) | ~ (distinct_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_lines(v0, v1) = v5)) % 19.16/5.17 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) % 19.27/5.17 | (6) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (distinct_lines(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3)) % 19.27/5.17 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) % 19.27/5.17 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) % 19.27/5.17 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = 0) | ~ (distinct_points(v0, v2) = v3) | apart_point_and_line(v2, v1) = 0) % 19.27/5.17 | (10) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v4 = 0) & line_connecting(v0, v2) = v5 & line_connecting(v0, v1) = v3 & apart_point_and_line(v2, v3) = v4 & apart_point_and_line(v1, v5) = 0 & distinct_points(v1, v2) = 0 & distinct_points(v0, v2) = 0 & distinct_points(v0, v1) = 0) % 19.27/5.17 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (line_connecting(v0, v1) = v3) | ~ (distinct_points(v2, v1) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v3) = v6 & distinct_points(v2, v0) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & v4 = 0)))) % 19.27/5.17 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v1, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) % 19.27/5.17 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (line_connecting(v0, v1) = v3) | ~ (distinct_points(v2, v0) = v4) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v3) = v6 & distinct_points(v2, v1) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v7 = 0 & v4 = 0)))) % 19.27/5.17 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (line_connecting(v0, v1) = v3) | ~ (apart_point_and_line(v2, v3) = 0) | ? [v4] : ? [v5] : ? [v6] : (distinct_points(v2, v1) = v6 & distinct_points(v2, v0) = v5 & distinct_points(v0, v1) = v4 & ( ~ (v4 = 0) | (v6 = 0 & v5 = 0)))) % 19.27/5.18 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_lines(v2, v3) = 0) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v1, v3) = v7 & apart_point_and_line(v1, v2) = v6 & apart_point_and_line(v0, v3) = v5 & apart_point_and_line(v0, v2) = v4 & (v7 = 0 | v6 = 0 | v5 = 0 | v4 = 0))) % 19.27/5.18 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v1, v2) = v4) | ~ (distinct_points(v0, v1) = 0) | ? [v6] : ? [v7] : ? [v8] : (apart_point_and_line(v0, v3) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_lines(v2, v3) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 19.27/5.18 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v1) = 0) | ~ (distinct_lines(v1, v2) = v3) | apart_point_and_line(v0, v2) = 0) % 19.27/5.18 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (apart_point_and_line(v2, v1) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (intersection_point(v0, v1) = v5 & apart_point_and_line(v2, v0) = v4 & distinct_points(v2, v5) = v6 & (v6 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))))) % 19.27/5.18 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 19.27/5.18 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 19.27/5.18 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) % 19.27/5.18 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) % 19.27/5.18 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (apart_point_and_line(v2, v0) = v3) | ~ (convergent_lines(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (intersection_point(v0, v1) = v5 & apart_point_and_line(v2, v1) = v4 & distinct_points(v2, v5) = v6 & (v6 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))))) % 19.27/5.18 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v2) = v5) | ~ (apart_point_and_line(v0, v3) = v4) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (apart_point_and_line(v1, v3) = v9 & apart_point_and_line(v0, v2) = v8 & distinct_lines(v2, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0 | v8 = 0))) % 19.27/5.18 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) % 19.27/5.18 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (apart_point_and_line(v2, v1) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & apart_point_and_line(v0, v1) = v5)) % 19.27/5.18 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v2) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ~ (distinct_lines(v2, v3) = 0) | ? [v6] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v3) = v8 & apart_point_and_line(v0, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 19.27/5.18 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v2, v1) = v3) | ~ (apart_point_and_line(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 19.27/5.18 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) % 19.27/5.18 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (convergent_lines(v1, v2) = v4) | ~ (convergent_lines(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & convergent_lines(v0, v1) = v5)) % 19.27/5.19 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | ~ (apart_point_and_line(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 19.27/5.19 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (intersection_point(v0, v1) = v4) | ~ (apart_point_and_line(v2, v1) = v3) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v0) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v4) = v7 & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v3 = 0))))) % 19.27/5.19 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (intersection_point(v0, v1) = v4) | ~ (apart_point_and_line(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (apart_point_and_line(v2, v1) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v4) = v7 & ( ~ (v5 = 0) | v7 = 0 | ( ~ (v6 = 0) & ~ (v3 = 0))))) % 19.27/5.19 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | v3 = 0 | ~ (distinct_points(v1, v2) = v4) | ~ (distinct_points(v0, v2) = v3) | ? [v5] : ( ~ (v5 = 0) & distinct_points(v0, v1) = v5)) % 19.27/5.19 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (apart_point_and_line(v2, v1) = v4) | ~ (apart_point_and_line(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (intersection_point(v0, v1) = v6 & convergent_lines(v0, v1) = v5 & distinct_points(v2, v6) = v7 & ( ~ (v5 = 0) | v7 = 0)) | ( ~ (v4 = 0) & ~ (v3 = 0))) % 19.27/5.19 | (36) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_points(v2, v1) = v3) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (line_connecting(v0, v1) = v4 & apart_point_and_line(v2, v4) = v5 & distinct_points(v2, v0) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v3 = 0)))) % 19.27/5.19 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (distinct_points(v2, v0) = v3) | ~ (distinct_points(v0, v1) = 0) | ? [v4] : ? [v5] : ? [v6] : (line_connecting(v0, v1) = v4 & apart_point_and_line(v2, v4) = v5 & distinct_points(v2, v1) = v6 & ( ~ (v5 = 0) | (v6 = 0 & v3 = 0)))) % 19.27/5.19 | (38) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v0, v1) = 0) % 19.27/5.19 | (39) ! [v0] : ~ (distinct_points(v0, v0) = 0) % 19.27/5.19 | (40) ! [v0] : ~ (convergent_lines(v0, v0) = 0) % 19.27/5.19 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (distinct_points(v2, v1) = v4) | ~ (distinct_points(v2, v0) = v3) | ? [v5] : ? [v6] : ? [v7] : (line_connecting(v0, v1) = v6 & apart_point_and_line(v2, v6) = v7 & distinct_points(v0, v1) = v5 & ( ~ (v7 = 0) | ~ (v5 = 0))) | (v4 = 0 & v3 = 0)) % 19.27/5.19 | (42) ! [v0] : ~ (distinct_lines(v0, v0) = 0) % 19.27/5.19 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v0, v2) = v4) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : (apart_point_and_line(v1, v2) = v9 & apart_point_and_line(v0, v3) = v8 & distinct_lines(v2, v3) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0 | v8 = 0))) % 19.27/5.19 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) % 19.27/5.19 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | v4 = 0 | ~ (apart_point_and_line(v1, v3) = v5) | ~ (apart_point_and_line(v0, v3) = v4) | ~ (distinct_lines(v2, v3) = 0) | ? [v6] : ? [v7] : ? [v8] : (apart_point_and_line(v1, v2) = v8 & apart_point_and_line(v0, v2) = v7 & distinct_points(v0, v1) = v6 & ( ~ (v6 = 0) | v8 = 0 | v7 = 0))) % 19.27/5.19 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) % 19.27/5.19 | % 19.27/5.19 | 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: % 19.27/5.19 | (47) ~ (all_1_1_1 = 0) & line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0 & line_connecting(all_1_5_5, all_1_4_4) = all_1_2_2 & apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1 & apart_point_and_line(all_1_4_4, all_1_0_0) = 0 & distinct_points(all_1_4_4, all_1_3_3) = 0 & distinct_points(all_1_5_5, all_1_3_3) = 0 & distinct_points(all_1_5_5, all_1_4_4) = 0 % 19.27/5.19 | % 19.27/5.19 | Applying alpha-rule on (47) yields: % 19.27/5.19 | (48) ~ (all_1_1_1 = 0) % 19.27/5.19 | (49) apart_point_and_line(all_1_4_4, all_1_0_0) = 0 % 19.27/5.20 | (50) line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0 % 19.27/5.20 | (51) distinct_points(all_1_5_5, all_1_3_3) = 0 % 19.27/5.20 | (52) line_connecting(all_1_5_5, all_1_4_4) = all_1_2_2 % 19.27/5.20 | (53) distinct_points(all_1_4_4, all_1_3_3) = 0 % 19.27/5.20 | (54) apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1 % 19.27/5.20 | (55) distinct_points(all_1_5_5, all_1_4_4) = 0 % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (39) with all_1_4_4 yields: % 19.27/5.20 | (56) ~ (distinct_points(all_1_4_4, all_1_4_4) = 0) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (39) with all_1_5_5 yields: % 19.27/5.20 | (57) ~ (distinct_points(all_1_5_5, all_1_5_5) = 0) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (43) with all_1_1_1, all_1_1_1, all_1_2_2, all_1_2_2, all_1_3_3, all_1_3_3 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, yields: % 19.27/5.20 | (58) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_2_2) = v3 & apart_point_and_line(all_1_3_3, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_2_2) = v1 & distinct_points(all_1_3_3, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (14) with all_1_0_0, all_1_4_4, all_1_3_3, all_1_5_5 and discharging atoms line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0, apart_point_and_line(all_1_4_4, all_1_0_0) = 0, yields: % 19.27/5.20 | (59) ? [v0] : ? [v1] : ? [v2] : (distinct_points(all_1_4_4, all_1_3_3) = v2 & distinct_points(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_5_5, all_1_3_3) = v0 & ( ~ (v0 = 0) | (v2 = 0 & v1 = 0))) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (14) with all_1_2_2, all_1_4_4, all_1_4_4, all_1_5_5 and discharging atoms line_connecting(all_1_5_5, all_1_4_4) = all_1_2_2, yields: % 19.27/5.20 | (60) ~ (apart_point_and_line(all_1_4_4, all_1_2_2) = 0) | ? [v0] : ? [v1] : ? [v2] : (distinct_points(all_1_4_4, all_1_4_4) = v2 & distinct_points(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v0 = 0) | (v2 = 0 & v1 = 0))) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (36) with 0, all_1_4_4, all_1_3_3, all_1_4_4 and discharging atoms distinct_points(all_1_4_4, all_1_3_3) = 0, yields: % 19.27/5.20 | (61) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_4_4, all_1_3_3) = v0 & apart_point_and_line(all_1_4_4, v0) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (11) with 0, all_1_0_0, all_1_4_4, all_1_3_3, all_1_5_5 and discharging atoms line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0, distinct_points(all_1_4_4, all_1_3_3) = 0, yields: % 19.27/5.20 | (62) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v2 & distinct_points(all_1_5_5, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (16) with all_1_1_1, all_1_1_1, all_1_2_2, all_1_2_2, all_1_3_3, all_1_4_4 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, distinct_points(all_1_4_4, all_1_3_3) = 0, yields: % 19.27/5.20 | (63) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (36) with 0, all_1_5_5, all_1_3_3, all_1_4_4 and discharging atoms distinct_points(all_1_4_4, all_1_3_3) = 0, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.27/5.20 | (64) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_4_4, all_1_3_3) = v0 & apart_point_and_line(all_1_5_5, v0) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (36) with 0, all_1_5_5, all_1_3_3, all_1_5_5 and discharging atoms distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.27/5.20 | (65) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_5_5, all_1_3_3) = v0 & apart_point_and_line(all_1_5_5, v0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (11) with 0, all_1_0_0, all_1_5_5, all_1_3_3, all_1_5_5 and discharging atoms line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.27/5.20 | (66) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_3_3) = v0 & distinct_points(all_1_5_5, all_1_5_5) = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (16) with all_1_1_1, all_1_1_1, all_1_2_2, all_1_2_2, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.27/5.20 | (67) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (36) with 0, all_1_4_4, all_1_3_3, all_1_5_5 and discharging atoms distinct_points(all_1_4_4, all_1_3_3) = 0, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.27/5.20 | (68) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_5_5, all_1_3_3) = v0 & apart_point_and_line(all_1_4_4, v0) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (37) with 0, all_1_5_5, all_1_3_3, all_1_4_4 and discharging atoms distinct_points(all_1_4_4, all_1_3_3) = 0, distinct_points(all_1_5_5, all_1_4_4) = 0, yields: % 19.27/5.20 | (69) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_4_4, all_1_3_3) = v0 & apart_point_and_line(all_1_5_5, v0) = v1 & distinct_points(all_1_5_5, all_1_3_3) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 19.27/5.20 | % 19.27/5.20 | Instantiating formula (36) with 0, all_1_5_5, all_1_4_4, all_1_5_5 and discharging atoms distinct_points(all_1_5_5, all_1_4_4) = 0, yields: % 19.27/5.20 | (70) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_5_5, all_1_4_4) = v0 & apart_point_and_line(all_1_5_5, v0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 19.27/5.21 | % 19.27/5.21 | Instantiating formula (11) with 0, all_1_2_2, all_1_5_5, all_1_4_4, all_1_5_5 and discharging atoms line_connecting(all_1_5_5, all_1_4_4) = all_1_2_2, distinct_points(all_1_5_5, all_1_4_4) = 0, yields: % 19.27/5.21 | (71) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_1_2_2) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & distinct_points(all_1_5_5, all_1_5_5) = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 19.27/5.21 | % 19.27/5.21 | Instantiating (71) with all_16_0_6, all_16_1_7, all_16_2_8 yields: % 19.27/5.21 | (72) apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7 & distinct_points(all_1_5_5, all_1_4_4) = all_16_2_8 & distinct_points(all_1_5_5, all_1_5_5) = all_16_0_6 & ( ~ (all_16_1_7 = 0) | ~ (all_16_2_8 = 0) | all_16_0_6 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (72) yields: % 19.27/5.21 | (73) apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7 % 19.27/5.21 | (74) distinct_points(all_1_5_5, all_1_4_4) = all_16_2_8 % 19.27/5.21 | (75) distinct_points(all_1_5_5, all_1_5_5) = all_16_0_6 % 19.27/5.21 | (76) ~ (all_16_1_7 = 0) | ~ (all_16_2_8 = 0) | all_16_0_6 = 0 % 19.27/5.21 | % 19.27/5.21 | Instantiating (69) with all_18_0_9, all_18_1_10, all_18_2_11 yields: % 19.27/5.21 | (77) line_connecting(all_1_4_4, all_1_3_3) = all_18_2_11 & apart_point_and_line(all_1_5_5, all_18_2_11) = all_18_1_10 & distinct_points(all_1_5_5, all_1_3_3) = all_18_0_9 & ( ~ (all_18_1_10 = 0) | all_18_0_9 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (77) yields: % 19.27/5.21 | (78) line_connecting(all_1_4_4, all_1_3_3) = all_18_2_11 % 19.27/5.21 | (79) apart_point_and_line(all_1_5_5, all_18_2_11) = all_18_1_10 % 19.27/5.21 | (80) distinct_points(all_1_5_5, all_1_3_3) = all_18_0_9 % 19.27/5.21 | (81) ~ (all_18_1_10 = 0) | all_18_0_9 = 0 % 19.27/5.21 | % 19.27/5.21 | Instantiating (62) with all_20_0_12, all_20_1_13, all_20_2_14 yields: % 19.27/5.21 | (82) apart_point_and_line(all_1_4_4, all_1_0_0) = all_20_1_13 & distinct_points(all_1_4_4, all_1_5_5) = all_20_0_12 & distinct_points(all_1_5_5, all_1_3_3) = all_20_2_14 & ( ~ (all_20_1_13 = 0) | ~ (all_20_2_14 = 0) | all_20_0_12 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (82) yields: % 19.27/5.21 | (83) apart_point_and_line(all_1_4_4, all_1_0_0) = all_20_1_13 % 19.27/5.21 | (84) distinct_points(all_1_4_4, all_1_5_5) = all_20_0_12 % 19.27/5.21 | (85) distinct_points(all_1_5_5, all_1_3_3) = all_20_2_14 % 19.27/5.21 | (86) ~ (all_20_1_13 = 0) | ~ (all_20_2_14 = 0) | all_20_0_12 = 0 % 19.27/5.21 | % 19.27/5.21 | Instantiating (61) with all_22_0_15, all_22_1_16, all_22_2_17 yields: % 19.27/5.21 | (87) line_connecting(all_1_4_4, all_1_3_3) = all_22_2_17 & apart_point_and_line(all_1_4_4, all_22_2_17) = all_22_1_16 & distinct_points(all_1_4_4, all_1_4_4) = all_22_0_15 & ( ~ (all_22_1_16 = 0) | all_22_0_15 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (87) yields: % 19.27/5.21 | (88) line_connecting(all_1_4_4, all_1_3_3) = all_22_2_17 % 19.27/5.21 | (89) apart_point_and_line(all_1_4_4, all_22_2_17) = all_22_1_16 % 19.27/5.21 | (90) distinct_points(all_1_4_4, all_1_4_4) = all_22_0_15 % 19.27/5.21 | (91) ~ (all_22_1_16 = 0) | all_22_0_15 = 0 % 19.27/5.21 | % 19.27/5.21 | Instantiating (59) with all_24_0_18, all_24_1_19, all_24_2_20 yields: % 19.27/5.21 | (92) distinct_points(all_1_4_4, all_1_3_3) = all_24_0_18 & distinct_points(all_1_4_4, all_1_5_5) = all_24_1_19 & distinct_points(all_1_5_5, all_1_3_3) = all_24_2_20 & ( ~ (all_24_2_20 = 0) | (all_24_0_18 = 0 & all_24_1_19 = 0)) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (92) yields: % 19.27/5.21 | (93) distinct_points(all_1_4_4, all_1_3_3) = all_24_0_18 % 19.27/5.21 | (94) distinct_points(all_1_4_4, all_1_5_5) = all_24_1_19 % 19.27/5.21 | (95) distinct_points(all_1_5_5, all_1_3_3) = all_24_2_20 % 19.27/5.21 | (96) ~ (all_24_2_20 = 0) | (all_24_0_18 = 0 & all_24_1_19 = 0) % 19.27/5.21 | % 19.27/5.21 | Instantiating (68) with all_26_0_21, all_26_1_22, all_26_2_23 yields: % 19.27/5.21 | (97) line_connecting(all_1_5_5, all_1_3_3) = all_26_2_23 & apart_point_and_line(all_1_4_4, all_26_2_23) = all_26_1_22 & distinct_points(all_1_4_4, all_1_5_5) = all_26_0_21 & ( ~ (all_26_1_22 = 0) | all_26_0_21 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (97) yields: % 19.27/5.21 | (98) line_connecting(all_1_5_5, all_1_3_3) = all_26_2_23 % 19.27/5.21 | (99) apart_point_and_line(all_1_4_4, all_26_2_23) = all_26_1_22 % 19.27/5.21 | (100) distinct_points(all_1_4_4, all_1_5_5) = all_26_0_21 % 19.27/5.21 | (101) ~ (all_26_1_22 = 0) | all_26_0_21 = 0 % 19.27/5.21 | % 19.27/5.21 | Instantiating (70) with all_28_0_24, all_28_1_25, all_28_2_26 yields: % 19.27/5.21 | (102) line_connecting(all_1_5_5, all_1_4_4) = all_28_2_26 & apart_point_and_line(all_1_5_5, all_28_2_26) = all_28_1_25 & distinct_points(all_1_5_5, all_1_5_5) = all_28_0_24 & ( ~ (all_28_1_25 = 0) | all_28_0_24 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (102) yields: % 19.27/5.21 | (103) line_connecting(all_1_5_5, all_1_4_4) = all_28_2_26 % 19.27/5.21 | (104) apart_point_and_line(all_1_5_5, all_28_2_26) = all_28_1_25 % 19.27/5.21 | (105) distinct_points(all_1_5_5, all_1_5_5) = all_28_0_24 % 19.27/5.21 | (106) ~ (all_28_1_25 = 0) | all_28_0_24 = 0 % 19.27/5.21 | % 19.27/5.21 | Instantiating (66) with all_32_0_30, all_32_1_31, all_32_2_32 yields: % 19.27/5.21 | (107) apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31 & distinct_points(all_1_5_5, all_1_3_3) = all_32_2_32 & distinct_points(all_1_5_5, all_1_5_5) = all_32_0_30 & ( ~ (all_32_1_31 = 0) | ~ (all_32_2_32 = 0) | all_32_0_30 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (107) yields: % 19.27/5.21 | (108) apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31 % 19.27/5.21 | (109) distinct_points(all_1_5_5, all_1_3_3) = all_32_2_32 % 19.27/5.21 | (110) distinct_points(all_1_5_5, all_1_5_5) = all_32_0_30 % 19.27/5.21 | (111) ~ (all_32_1_31 = 0) | ~ (all_32_2_32 = 0) | all_32_0_30 = 0 % 19.27/5.21 | % 19.27/5.21 | Instantiating (65) with all_34_0_33, all_34_1_34, all_34_2_35 yields: % 19.27/5.21 | (112) line_connecting(all_1_5_5, all_1_3_3) = all_34_2_35 & apart_point_and_line(all_1_5_5, all_34_2_35) = all_34_1_34 & distinct_points(all_1_5_5, all_1_5_5) = all_34_0_33 & ( ~ (all_34_1_34 = 0) | all_34_0_33 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (112) yields: % 19.27/5.21 | (113) line_connecting(all_1_5_5, all_1_3_3) = all_34_2_35 % 19.27/5.21 | (114) apart_point_and_line(all_1_5_5, all_34_2_35) = all_34_1_34 % 19.27/5.21 | (115) distinct_points(all_1_5_5, all_1_5_5) = all_34_0_33 % 19.27/5.21 | (116) ~ (all_34_1_34 = 0) | all_34_0_33 = 0 % 19.27/5.21 | % 19.27/5.21 | Instantiating (64) with all_36_0_36, all_36_1_37, all_36_2_38 yields: % 19.27/5.21 | (117) line_connecting(all_1_4_4, all_1_3_3) = all_36_2_38 & apart_point_and_line(all_1_5_5, all_36_2_38) = all_36_1_37 & distinct_points(all_1_5_5, all_1_4_4) = all_36_0_36 & ( ~ (all_36_1_37 = 0) | all_36_0_36 = 0) % 19.27/5.21 | % 19.27/5.21 | Applying alpha-rule on (117) yields: % 19.27/5.21 | (118) line_connecting(all_1_4_4, all_1_3_3) = all_36_2_38 % 19.27/5.22 | (119) apart_point_and_line(all_1_5_5, all_36_2_38) = all_36_1_37 % 19.27/5.22 | (120) distinct_points(all_1_5_5, all_1_4_4) = all_36_0_36 % 19.27/5.22 | (121) ~ (all_36_1_37 = 0) | all_36_0_36 = 0 % 19.27/5.22 | % 19.27/5.22 +-Applying beta-rule and splitting (67), into two cases. % 19.27/5.22 |-Branch one: % 19.27/5.22 | (122) all_1_1_1 = 0 % 19.27/5.22 | % 19.27/5.22 | Equations (122) can reduce 48 to: % 19.27/5.22 | (123) $false % 19.27/5.22 | % 19.27/5.22 |-The branch is then unsatisfiable % 19.27/5.22 |-Branch two: % 19.27/5.22 | (48) ~ (all_1_1_1 = 0) % 19.27/5.22 | (125) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.27/5.22 | % 19.27/5.22 | Instantiating (125) with all_42_0_39, all_42_1_40, all_42_2_41 yields: % 19.27/5.22 | (126) apart_point_and_line(all_1_5_5, all_1_2_2) = all_42_0_39 & apart_point_and_line(all_1_5_5, all_1_2_2) = all_42_1_40 & distinct_lines(all_1_2_2, all_1_2_2) = all_42_2_41 & ( ~ (all_42_2_41 = 0) | all_42_0_39 = 0 | all_42_1_40 = 0) % 19.27/5.22 | % 19.27/5.22 | Applying alpha-rule on (126) yields: % 19.27/5.22 | (127) apart_point_and_line(all_1_5_5, all_1_2_2) = all_42_0_39 % 19.27/5.22 | (128) apart_point_and_line(all_1_5_5, all_1_2_2) = all_42_1_40 % 19.27/5.22 | (129) distinct_lines(all_1_2_2, all_1_2_2) = all_42_2_41 % 19.27/5.22 | (130) ~ (all_42_2_41 = 0) | all_42_0_39 = 0 | all_42_1_40 = 0 % 19.27/5.22 | % 19.27/5.22 +-Applying beta-rule and splitting (63), into two cases. % 19.27/5.22 |-Branch one: % 19.27/5.22 | (122) all_1_1_1 = 0 % 19.27/5.22 | % 19.27/5.22 | Equations (122) can reduce 48 to: % 19.27/5.22 | (123) $false % 19.27/5.22 | % 19.27/5.22 |-The branch is then unsatisfiable % 19.27/5.22 |-Branch two: % 19.27/5.22 | (48) ~ (all_1_1_1 = 0) % 19.27/5.22 | (134) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.27/5.22 | % 19.27/5.22 | Instantiating (134) with all_47_0_42, all_47_1_43, all_47_2_44 yields: % 19.27/5.22 | (135) apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_0_42 & apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43 & distinct_lines(all_1_2_2, all_1_2_2) = all_47_2_44 & ( ~ (all_47_2_44 = 0) | all_47_0_42 = 0 | all_47_1_43 = 0) % 19.27/5.22 | % 19.27/5.22 | Applying alpha-rule on (135) yields: % 19.27/5.22 | (136) apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_0_42 % 19.27/5.22 | (137) apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43 % 19.27/5.22 | (138) distinct_lines(all_1_2_2, all_1_2_2) = all_47_2_44 % 19.27/5.22 | (139) ~ (all_47_2_44 = 0) | all_47_0_42 = 0 | all_47_1_43 = 0 % 19.27/5.22 | % 19.27/5.22 +-Applying beta-rule and splitting (58), into two cases. % 19.27/5.22 |-Branch one: % 19.27/5.22 | (122) all_1_1_1 = 0 % 19.27/5.22 | % 19.27/5.22 | Equations (122) can reduce 48 to: % 19.27/5.22 | (123) $false % 19.27/5.22 | % 19.27/5.22 |-The branch is then unsatisfiable % 19.27/5.22 |-Branch two: % 19.27/5.22 | (48) ~ (all_1_1_1 = 0) % 19.27/5.22 | (143) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_2_2) = v3 & apart_point_and_line(all_1_3_3, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_2_2) = v1 & distinct_points(all_1_3_3, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.22 | % 19.54/5.22 | Instantiating (143) with all_52_0_45, all_52_1_46, all_52_2_47, all_52_3_48 yields: % 19.54/5.22 | (144) apart_point_and_line(all_1_3_3, all_1_2_2) = all_52_0_45 & apart_point_and_line(all_1_3_3, all_1_2_2) = all_52_1_46 & distinct_lines(all_1_2_2, all_1_2_2) = all_52_2_47 & distinct_points(all_1_3_3, all_1_3_3) = all_52_3_48 & ( ~ (all_52_2_47 = 0) | ~ (all_52_3_48 = 0) | all_52_0_45 = 0 | all_52_1_46 = 0) % 19.54/5.22 | % 19.54/5.22 | Applying alpha-rule on (144) yields: % 19.54/5.22 | (145) apart_point_and_line(all_1_3_3, all_1_2_2) = all_52_1_46 % 19.54/5.22 | (146) ~ (all_52_2_47 = 0) | ~ (all_52_3_48 = 0) | all_52_0_45 = 0 | all_52_1_46 = 0 % 19.54/5.22 | (147) apart_point_and_line(all_1_3_3, all_1_2_2) = all_52_0_45 % 19.54/5.22 | (148) distinct_points(all_1_3_3, all_1_3_3) = all_52_3_48 % 19.54/5.22 | (149) distinct_lines(all_1_2_2, all_1_2_2) = all_52_2_47 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (8) with all_1_4_4, all_1_3_3, all_22_2_17, all_36_2_38 and discharging atoms line_connecting(all_1_4_4, all_1_3_3) = all_36_2_38, line_connecting(all_1_4_4, all_1_3_3) = all_22_2_17, yields: % 19.54/5.22 | (150) all_36_2_38 = all_22_2_17 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (8) with all_1_4_4, all_1_3_3, all_18_2_11, all_36_2_38 and discharging atoms line_connecting(all_1_4_4, all_1_3_3) = all_36_2_38, line_connecting(all_1_4_4, all_1_3_3) = all_18_2_11, yields: % 19.54/5.22 | (151) all_36_2_38 = all_18_2_11 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (8) with all_1_5_5, all_1_3_3, all_34_2_35, all_1_0_0 and discharging atoms line_connecting(all_1_5_5, all_1_3_3) = all_34_2_35, line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0, yields: % 19.54/5.22 | (152) all_34_2_35 = all_1_0_0 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (8) with all_1_5_5, all_1_3_3, all_26_2_23, all_34_2_35 and discharging atoms line_connecting(all_1_5_5, all_1_3_3) = all_34_2_35, line_connecting(all_1_5_5, all_1_3_3) = all_26_2_23, yields: % 19.54/5.22 | (153) all_34_2_35 = all_26_2_23 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (8) with all_1_5_5, all_1_4_4, all_28_2_26, all_1_2_2 and discharging atoms line_connecting(all_1_5_5, all_1_4_4) = all_28_2_26, line_connecting(all_1_5_5, all_1_4_4) = all_1_2_2, yields: % 19.54/5.22 | (154) all_28_2_26 = all_1_2_2 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (21) with all_1_3_3, all_1_2_2, all_52_0_45, all_1_1_1 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_52_0_45, apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, yields: % 19.54/5.22 | (155) all_52_0_45 = all_1_1_1 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (21) with all_1_3_3, all_1_2_2, all_52_1_46, all_52_0_45 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_52_0_45, apart_point_and_line(all_1_3_3, all_1_2_2) = all_52_1_46, yields: % 19.54/5.22 | (156) all_52_0_45 = all_52_1_46 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_26_1_22, 0 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = 0, yields: % 19.54/5.22 | (157) all_26_1_22 = 0 | ~ (apart_point_and_line(all_1_4_4, all_1_0_0) = all_26_1_22) % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_22_1_16, 0 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = 0, yields: % 19.54/5.22 | (158) all_22_1_16 = 0 | ~ (apart_point_and_line(all_1_4_4, all_1_0_0) = all_22_1_16) % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_20_1_13, 0 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = all_20_1_13, apart_point_and_line(all_1_4_4, all_1_0_0) = 0, yields: % 19.54/5.22 | (159) all_20_1_13 = 0 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (21) with all_1_4_4, all_1_2_2, all_47_1_43, all_47_0_42 and discharging atoms apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_0_42, apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, yields: % 19.54/5.22 | (160) all_47_0_42 = all_47_1_43 % 19.54/5.22 | % 19.54/5.22 | Instantiating formula (21) with all_1_5_5, all_1_0_0, all_32_1_31, all_34_1_34 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.54/5.23 | (161) all_34_1_34 = all_32_1_31 | ~ (apart_point_and_line(all_1_5_5, all_1_0_0) = all_34_1_34) % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (21) with all_1_5_5, all_1_2_2, all_42_0_39, all_28_1_25 and discharging atoms apart_point_and_line(all_1_5_5, all_1_2_2) = all_42_0_39, yields: % 19.54/5.23 | (162) all_42_0_39 = all_28_1_25 | ~ (apart_point_and_line(all_1_5_5, all_1_2_2) = all_28_1_25) % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (21) with all_1_5_5, all_1_2_2, all_16_1_7, all_42_0_39 and discharging atoms apart_point_and_line(all_1_5_5, all_1_2_2) = all_42_0_39, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.54/5.23 | (163) all_42_0_39 = all_16_1_7 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (39) with all_1_3_3 yields: % 19.54/5.23 | (164) ~ (distinct_points(all_1_3_3, all_1_3_3) = 0) % 19.54/5.23 | % 19.54/5.23 | Using (90) and (56) yields: % 19.54/5.23 | (165) ~ (all_22_0_15 = 0) % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_4_4, all_1_5_5, all_24_1_19, all_26_0_21 and discharging atoms distinct_points(all_1_4_4, all_1_5_5) = all_26_0_21, distinct_points(all_1_4_4, all_1_5_5) = all_24_1_19, yields: % 19.54/5.23 | (166) all_26_0_21 = all_24_1_19 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_4_4, all_1_5_5, all_20_0_12, all_26_0_21 and discharging atoms distinct_points(all_1_4_4, all_1_5_5) = all_26_0_21, distinct_points(all_1_4_4, all_1_5_5) = all_20_0_12, yields: % 19.54/5.23 | (167) all_26_0_21 = all_20_0_12 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_3_3, all_24_2_20, 0 and discharging atoms distinct_points(all_1_5_5, all_1_3_3) = all_24_2_20, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.54/5.23 | (168) all_24_2_20 = 0 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_3_3, all_24_2_20, all_32_2_32 and discharging atoms distinct_points(all_1_5_5, all_1_3_3) = all_32_2_32, distinct_points(all_1_5_5, all_1_3_3) = all_24_2_20, yields: % 19.54/5.23 | (169) all_32_2_32 = all_24_2_20 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_3_3, all_20_2_14, all_32_2_32 and discharging atoms distinct_points(all_1_5_5, all_1_3_3) = all_32_2_32, distinct_points(all_1_5_5, all_1_3_3) = all_20_2_14, yields: % 19.54/5.23 | (170) all_32_2_32 = all_20_2_14 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_3_3, all_18_0_9, all_24_2_20 and discharging atoms distinct_points(all_1_5_5, all_1_3_3) = all_24_2_20, distinct_points(all_1_5_5, all_1_3_3) = all_18_0_9, yields: % 19.54/5.23 | (171) all_24_2_20 = all_18_0_9 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_4_4, all_36_0_36, 0 and discharging atoms distinct_points(all_1_5_5, all_1_4_4) = all_36_0_36, distinct_points(all_1_5_5, all_1_4_4) = 0, yields: % 19.54/5.23 | (172) all_36_0_36 = 0 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_4_4, all_16_2_8, all_36_0_36 and discharging atoms distinct_points(all_1_5_5, all_1_4_4) = all_36_0_36, distinct_points(all_1_5_5, all_1_4_4) = all_16_2_8, yields: % 19.54/5.23 | (173) all_36_0_36 = all_16_2_8 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_5_5, all_32_0_30, all_34_0_33 and discharging atoms distinct_points(all_1_5_5, all_1_5_5) = all_34_0_33, distinct_points(all_1_5_5, all_1_5_5) = all_32_0_30, yields: % 19.54/5.23 | (174) all_34_0_33 = all_32_0_30 % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_5_5, all_28_0_24, all_32_0_30 and discharging atoms distinct_points(all_1_5_5, all_1_5_5) = all_32_0_30, distinct_points(all_1_5_5, all_1_5_5) = all_28_0_24, yields: % 19.54/5.23 | (175) all_32_0_30 = all_28_0_24 % 19.54/5.23 | % 19.54/5.23 | Using (105) and (57) yields: % 19.54/5.23 | (176) ~ (all_28_0_24 = 0) % 19.54/5.23 | % 19.54/5.23 | Instantiating formula (46) with all_1_5_5, all_1_5_5, all_16_0_6, all_34_0_33 and discharging atoms distinct_points(all_1_5_5, all_1_5_5) = all_34_0_33, distinct_points(all_1_5_5, all_1_5_5) = all_16_0_6, yields: % 19.54/5.23 | (177) all_34_0_33 = all_16_0_6 % 19.54/5.23 | % 19.54/5.23 | Combining equations (155,156) yields a new equation: % 19.54/5.23 | (178) all_52_1_46 = all_1_1_1 % 19.54/5.23 | % 19.54/5.23 | Combining equations (173,172) yields a new equation: % 19.54/5.23 | (179) all_16_2_8 = 0 % 19.54/5.23 | % 19.54/5.23 | Simplifying 179 yields: % 19.54/5.23 | (180) all_16_2_8 = 0 % 19.54/5.23 | % 19.54/5.23 | Combining equations (150,151) yields a new equation: % 19.54/5.23 | (181) all_22_2_17 = all_18_2_11 % 19.54/5.23 | % 19.54/5.23 | Simplifying 181 yields: % 19.54/5.23 | (182) all_22_2_17 = all_18_2_11 % 19.54/5.23 | % 19.54/5.23 | Combining equations (174,177) yields a new equation: % 19.54/5.23 | (183) all_32_0_30 = all_16_0_6 % 19.54/5.23 | % 19.54/5.23 | Simplifying 183 yields: % 19.54/5.23 | (184) all_32_0_30 = all_16_0_6 % 19.54/5.23 | % 19.54/5.23 | Combining equations (152,153) yields a new equation: % 19.54/5.23 | (185) all_26_2_23 = all_1_0_0 % 19.54/5.23 | % 19.54/5.23 | Combining equations (184,175) yields a new equation: % 19.54/5.23 | (186) all_28_0_24 = all_16_0_6 % 19.54/5.23 | % 19.54/5.23 | Combining equations (169,170) yields a new equation: % 19.54/5.23 | (187) all_24_2_20 = all_20_2_14 % 19.54/5.23 | % 19.54/5.23 | Simplifying 187 yields: % 19.54/5.23 | (188) all_24_2_20 = all_20_2_14 % 19.54/5.23 | % 19.54/5.23 | Combining equations (167,166) yields a new equation: % 19.54/5.23 | (189) all_24_1_19 = all_20_0_12 % 19.54/5.23 | % 19.54/5.23 | Combining equations (168,188) yields a new equation: % 19.54/5.23 | (190) all_20_2_14 = 0 % 19.54/5.23 | % 19.54/5.23 | Combining equations (171,188) yields a new equation: % 19.54/5.23 | (191) all_20_2_14 = all_18_0_9 % 19.54/5.23 | % 19.54/5.23 | Combining equations (191,190) yields a new equation: % 19.54/5.23 | (192) all_18_0_9 = 0 % 19.54/5.23 | % 19.54/5.23 | Simplifying 192 yields: % 19.54/5.23 | (193) all_18_0_9 = 0 % 19.54/5.23 | % 19.54/5.23 | Combining equations (185,153) yields a new equation: % 19.54/5.23 | (152) all_34_2_35 = all_1_0_0 % 19.54/5.23 | % 19.54/5.23 | Equations (186) can reduce 176 to: % 19.54/5.23 | (195) ~ (all_16_0_6 = 0) % 19.54/5.23 | % 19.54/5.23 | From (185) and (98) follows: % 19.54/5.23 | (50) line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0 % 19.54/5.23 | % 19.54/5.23 | From (178) and (145) follows: % 19.54/5.23 | (54) apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1 % 19.54/5.23 | % 19.54/5.23 | From (185) and (99) follows: % 19.54/5.23 | (198) apart_point_and_line(all_1_4_4, all_1_0_0) = all_26_1_22 % 19.54/5.23 | % 19.54/5.23 | From (182) and (89) follows: % 19.54/5.23 | (199) apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16 % 19.54/5.23 | % 19.54/5.23 | From (160) and (136) follows: % 19.54/5.24 | (137) apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43 % 19.54/5.24 | % 19.54/5.24 | From (152) and (114) follows: % 19.54/5.24 | (201) apart_point_and_line(all_1_5_5, all_1_0_0) = all_34_1_34 % 19.54/5.24 | % 19.54/5.24 | From (154) and (104) follows: % 19.54/5.24 | (202) apart_point_and_line(all_1_5_5, all_1_2_2) = all_28_1_25 % 19.54/5.24 | % 19.54/5.24 | From (189) and (94) follows: % 19.54/5.24 | (84) distinct_points(all_1_4_4, all_1_5_5) = all_20_0_12 % 19.54/5.24 | % 19.54/5.24 | From (193) and (80) follows: % 19.54/5.24 | (51) distinct_points(all_1_5_5, all_1_3_3) = 0 % 19.54/5.24 | % 19.54/5.24 | From (180) and (74) follows: % 19.54/5.24 | (55) distinct_points(all_1_5_5, all_1_4_4) = 0 % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (91), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (206) ~ (all_22_1_16 = 0) % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (86), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (207) ~ (all_20_1_13 = 0) % 19.54/5.24 | % 19.54/5.24 | Equations (159) can reduce 207 to: % 19.54/5.24 | (123) $false % 19.54/5.24 | % 19.54/5.24 |-The branch is then unsatisfiable % 19.54/5.24 |-Branch two: % 19.54/5.24 | (159) all_20_1_13 = 0 % 19.54/5.24 | (210) ~ (all_20_2_14 = 0) | all_20_0_12 = 0 % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (210), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (211) ~ (all_20_2_14 = 0) % 19.54/5.24 | % 19.54/5.24 | Equations (190) can reduce 211 to: % 19.54/5.24 | (123) $false % 19.54/5.24 | % 19.54/5.24 |-The branch is then unsatisfiable % 19.54/5.24 |-Branch two: % 19.54/5.24 | (190) all_20_2_14 = 0 % 19.54/5.24 | (214) all_20_0_12 = 0 % 19.54/5.24 | % 19.54/5.24 | From (214) and (84) follows: % 19.54/5.24 | (215) distinct_points(all_1_4_4, all_1_5_5) = 0 % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (106), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (216) ~ (all_28_1_25 = 0) % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (116), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (217) ~ (all_34_1_34 = 0) % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (60), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (218) ~ (apart_point_and_line(all_1_4_4, all_1_2_2) = 0) % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (158), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (219) ~ (apart_point_and_line(all_1_4_4, all_1_0_0) = all_22_1_16) % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (162), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (220) ~ (apart_point_and_line(all_1_5_5, all_1_2_2) = all_28_1_25) % 19.54/5.24 | % 19.54/5.24 | Using (202) and (220) yields: % 19.54/5.24 | (221) $false % 19.54/5.24 | % 19.54/5.24 |-The branch is then unsatisfiable % 19.54/5.24 |-Branch two: % 19.54/5.24 | (202) apart_point_and_line(all_1_5_5, all_1_2_2) = all_28_1_25 % 19.54/5.24 | (223) all_42_0_39 = all_28_1_25 % 19.54/5.24 | % 19.54/5.24 | Combining equations (223,163) yields a new equation: % 19.54/5.24 | (224) all_28_1_25 = all_16_1_7 % 19.54/5.24 | % 19.54/5.24 | Simplifying 224 yields: % 19.54/5.24 | (225) all_28_1_25 = all_16_1_7 % 19.54/5.24 | % 19.54/5.24 | Equations (225) can reduce 216 to: % 19.54/5.24 | (226) ~ (all_16_1_7 = 0) % 19.54/5.24 | % 19.54/5.24 | From (225) and (202) follows: % 19.54/5.24 | (73) apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7 % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (157), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (228) ~ (apart_point_and_line(all_1_4_4, all_1_0_0) = all_26_1_22) % 19.54/5.24 | % 19.54/5.24 | Using (198) and (228) yields: % 19.54/5.24 | (221) $false % 19.54/5.24 | % 19.54/5.24 |-The branch is then unsatisfiable % 19.54/5.24 |-Branch two: % 19.54/5.24 | (198) apart_point_and_line(all_1_4_4, all_1_0_0) = all_26_1_22 % 19.54/5.24 | (231) all_26_1_22 = 0 % 19.54/5.24 | % 19.54/5.24 | From (231) and (198) follows: % 19.54/5.24 | (49) apart_point_and_line(all_1_4_4, all_1_0_0) = 0 % 19.54/5.24 | % 19.54/5.24 +-Applying beta-rule and splitting (161), into two cases. % 19.54/5.24 |-Branch one: % 19.54/5.24 | (233) ~ (apart_point_and_line(all_1_5_5, all_1_0_0) = all_34_1_34) % 19.54/5.24 | % 19.54/5.24 | Using (201) and (233) yields: % 19.54/5.24 | (221) $false % 19.54/5.24 | % 19.54/5.24 |-The branch is then unsatisfiable % 19.54/5.24 |-Branch two: % 19.54/5.24 | (201) apart_point_and_line(all_1_5_5, all_1_0_0) = all_34_1_34 % 19.54/5.24 | (236) all_34_1_34 = all_32_1_31 % 19.54/5.24 | % 19.54/5.24 | Equations (236) can reduce 217 to: % 19.54/5.24 | (237) ~ (all_32_1_31 = 0) % 19.54/5.24 | % 19.54/5.24 | From (236) and (201) follows: % 19.54/5.24 | (108) apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31 % 19.54/5.24 | % 19.54/5.24 | Using (137) and (218) yields: % 19.54/5.24 | (239) ~ (all_47_1_43 = 0) % 19.54/5.24 | % 19.54/5.24 | Using (148) and (164) yields: % 19.54/5.24 | (240) ~ (all_52_3_48 = 0) % 19.54/5.24 | % 19.54/5.24 | Instantiating formula (43) with all_22_1_16, all_1_1_1, all_18_2_11, all_1_2_2, all_1_4_4, all_1_3_3 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, yields: % 19.54/5.24 | (241) all_22_1_16 = 0 | all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_3_3, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.24 | % 19.54/5.24 | Instantiating formula (24) with all_1_1_1, all_22_1_16, all_18_2_11, all_1_2_2, all_1_3_3, all_1_4_4 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, yields: % 19.54/5.24 | (242) all_22_1_16 = 0 | all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.24 | % 19.54/5.24 | Instantiating formula (43) with all_22_1_16, all_22_1_16, all_18_2_11, all_18_2_11, all_1_4_4, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, yields: % 19.54/5.24 | (243) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_18_2_11) = v2 & distinct_lines(all_18_2_11, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.24 | % 19.54/5.24 | Instantiating formula (31) with all_47_1_43, all_1_2_2, all_1_0_0, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = 0, apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, yields: % 19.54/5.25 | (244) all_47_1_43 = 0 | distinct_lines(all_1_0_0, all_1_2_2) = 0 % 19.54/5.25 | % 19.54/5.25 | Instantiating formula (43) with all_47_1_43, all_22_1_16, all_1_2_2, all_18_2_11, all_1_4_4, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, yields: % 19.54/5.25 | (245) all_47_1_43 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.25 | % 19.54/5.25 | Instantiating formula (43) with all_22_1_16, all_47_1_43, all_18_2_11, all_1_2_2, all_1_4_4, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, yields: % 19.54/5.25 | (246) all_47_1_43 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.25 | % 19.54/5.25 | Instantiating formula (24) with all_47_1_43, all_22_1_16, all_18_2_11, all_1_2_2, all_1_4_4, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, yields: % 19.54/5.25 | (247) all_47_1_43 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.25 | % 19.54/5.25 | Instantiating formula (24) with all_22_1_16, all_47_1_43, all_1_2_2, all_18_2_11, all_1_4_4, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, yields: % 19.54/5.25 | (248) all_47_1_43 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.25 | % 19.54/5.25 | Instantiating formula (43) with all_32_1_31, all_1_1_1, all_1_0_0, all_1_2_2, all_1_5_5, all_1_3_3 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.54/5.25 | (249) all_32_1_31 = 0 | all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_3_3, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.54/5.25 | % 19.68/5.25 | Instantiating formula (24) with all_32_1_31, all_1_1_1, all_1_2_2, all_1_0_0, all_1_5_5, all_1_3_3 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (250) all_32_1_31 = 0 | all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_0_0, all_1_2_2) = v1 & distinct_points(all_1_3_3, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (24) with all_1_1_1, all_32_1_31, all_1_0_0, all_1_2_2, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (251) all_32_1_31 = 0 | all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (43) with all_32_1_31, all_22_1_16, all_1_0_0, all_18_2_11, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (252) all_32_1_31 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_18_2_11, all_1_0_0) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (43) with all_22_1_16, all_32_1_31, all_18_2_11, all_1_0_0, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (253) all_32_1_31 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_1_0_0, all_18_2_11) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (24) with all_32_1_31, all_22_1_16, all_18_2_11, all_1_0_0, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (254) all_32_1_31 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_1_0_0, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (24) with all_22_1_16, all_32_1_31, all_1_0_0, all_18_2_11, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (255) all_32_1_31 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_18_2_11, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (43) with all_32_1_31, all_47_1_43, all_1_0_0, all_1_2_2, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (256) all_47_1_43 = 0 | all_32_1_31 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (24) with all_47_1_43, all_32_1_31, all_1_0_0, all_1_2_2, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (257) all_47_1_43 = 0 | all_32_1_31 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (2) with all_32_1_31, all_32_1_31, all_1_0_0, all_1_0_0, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.68/5.25 | (258) all_32_1_31 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_3_3, all_1_0_0) = v1 & distinct_lines(all_1_0_0, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.25 | % 19.68/5.25 | Instantiating formula (43) with all_32_1_31, all_32_1_31, all_1_0_0, all_1_0_0, all_1_5_5, all_1_5_5 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, yields: % 19.68/5.25 | (259) all_32_1_31 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_0_0) = v2 & distinct_lines(all_1_0_0, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.25 | % 19.68/5.26 | Instantiating formula (43) with all_16_1_7, all_22_1_16, all_1_2_2, all_18_2_11, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.68/5.26 | (260) all_22_1_16 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (43) with all_22_1_16, all_16_1_7, all_18_2_11, all_1_2_2, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.68/5.26 | (261) all_22_1_16 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (24) with all_16_1_7, all_22_1_16, all_18_2_11, all_1_2_2, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.68/5.26 | (262) all_22_1_16 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (24) with all_22_1_16, all_16_1_7, all_1_2_2, all_18_2_11, all_1_4_4, all_1_5_5 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.68/5.26 | (263) all_22_1_16 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (2) with all_16_1_7, all_32_1_31, all_1_2_2, all_1_0_0, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.68/5.26 | (264) all_32_1_31 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v1 & apart_point_and_line(all_1_3_3, all_1_2_2) = v2 & distinct_lines(all_1_0_0, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (2) with all_32_1_31, all_16_1_7, all_1_0_0, all_1_2_2, all_1_3_3, all_1_5_5 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.68/5.26 | (265) all_32_1_31 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_3_3, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (43) with all_16_1_7, all_32_1_31, all_1_2_2, all_1_0_0, all_1_5_5, all_1_5_5 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.68/5.26 | (266) all_32_1_31 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_0_0, all_1_2_2) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (43) with all_32_1_31, all_16_1_7, all_1_0_0, all_1_2_2, all_1_5_5, all_1_5_5 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.68/5.26 | (267) all_32_1_31 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (24) with all_16_1_7, all_32_1_31, all_1_0_0, all_1_2_2, all_1_5_5, all_1_5_5 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.68/5.26 | (268) all_32_1_31 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (24) with all_32_1_31, all_16_1_7, all_1_2_2, all_1_0_0, all_1_5_5, all_1_5_5 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, yields: % 19.68/5.26 | (269) all_32_1_31 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_0_0, all_1_2_2) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (36) with all_52_3_48, all_1_3_3, all_1_3_3, all_1_5_5 and discharging atoms distinct_points(all_1_3_3, all_1_3_3) = all_52_3_48, distinct_points(all_1_5_5, all_1_3_3) = 0, yields: % 19.68/5.26 | (270) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_5_5, all_1_3_3) = v0 & apart_point_and_line(all_1_3_3, v0) = v1 & distinct_points(all_1_3_3, all_1_5_5) = v2 & ( ~ (v1 = 0) | (v2 = 0 & all_52_3_48 = 0))) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (41) with all_52_3_48, all_52_3_48, all_1_3_3, all_1_3_3, all_1_3_3 and discharging atoms distinct_points(all_1_3_3, all_1_3_3) = all_52_3_48, yields: % 19.68/5.26 | (271) all_52_3_48 = 0 | ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_3_3, all_1_3_3) = v1 & apart_point_and_line(all_1_3_3, v1) = v2 & distinct_points(all_1_3_3, all_1_3_3) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (11) with all_52_3_48, all_1_0_0, all_1_3_3, all_1_3_3, all_1_5_5 and discharging atoms line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0, distinct_points(all_1_3_3, all_1_3_3) = all_52_3_48, yields: % 19.68/5.26 | (272) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v1 & distinct_points(all_1_3_3, all_1_5_5) = v2 & distinct_points(all_1_5_5, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v2 = 0 & all_52_3_48 = 0))) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (2) with all_22_1_16, all_22_1_16, all_18_2_11, all_18_2_11, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, distinct_points(all_1_4_4, all_1_5_5) = 0, yields: % 19.68/5.26 | (273) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v1 & distinct_lines(all_18_2_11, all_18_2_11) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (2) with all_22_1_16, all_47_1_43, all_18_2_11, all_1_2_2, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, distinct_points(all_1_4_4, all_1_5_5) = 0, yields: % 19.68/5.26 | (274) all_47_1_43 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_18_2_11) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (2) with all_47_1_43, all_22_1_16, all_1_2_2, all_18_2_11, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_4_4, all_18_2_11) = all_22_1_16, apart_point_and_line(all_1_4_4, all_1_2_2) = all_47_1_43, distinct_points(all_1_4_4, all_1_5_5) = 0, yields: % 19.68/5.26 | (275) all_47_1_43 = 0 | all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_18_2_11) = v1 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_18_2_11, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (16) with all_32_1_31, all_32_1_31, all_1_0_0, all_1_0_0, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, distinct_points(all_1_4_4, all_1_5_5) = 0, yields: % 19.68/5.26 | (276) all_32_1_31 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_4_4, all_1_0_0) = v1 & distinct_lines(all_1_0_0, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (16) with all_32_1_31, all_16_1_7, all_1_0_0, all_1_2_2, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, distinct_points(all_1_4_4, all_1_5_5) = 0, yields: % 19.68/5.26 | (277) all_32_1_31 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating formula (16) with all_16_1_7, all_32_1_31, all_1_2_2, all_1_0_0, all_1_5_5, all_1_4_4 and discharging atoms apart_point_and_line(all_1_5_5, all_1_0_0) = all_32_1_31, apart_point_and_line(all_1_5_5, all_1_2_2) = all_16_1_7, distinct_points(all_1_4_4, all_1_5_5) = 0, yields: % 19.68/5.26 | (278) all_32_1_31 = 0 | all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v1 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_1_0_0, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.26 | % 19.68/5.26 | Instantiating (272) with all_143_0_79, all_143_1_80, all_143_2_81 yields: % 19.68/5.26 | (279) apart_point_and_line(all_1_3_3, all_1_0_0) = all_143_1_80 & distinct_points(all_1_3_3, all_1_5_5) = all_143_0_79 & distinct_points(all_1_5_5, all_1_3_3) = all_143_2_81 & ( ~ (all_143_1_80 = 0) | ~ (all_143_2_81 = 0) | (all_143_0_79 = 0 & all_52_3_48 = 0)) % 19.68/5.26 | % 19.68/5.26 | Applying alpha-rule on (279) yields: % 19.68/5.26 | (280) apart_point_and_line(all_1_3_3, all_1_0_0) = all_143_1_80 % 19.68/5.26 | (281) distinct_points(all_1_3_3, all_1_5_5) = all_143_0_79 % 19.68/5.26 | (282) distinct_points(all_1_5_5, all_1_3_3) = all_143_2_81 % 19.68/5.26 | (283) ~ (all_143_1_80 = 0) | ~ (all_143_2_81 = 0) | (all_143_0_79 = 0 & all_52_3_48 = 0) % 19.68/5.26 | % 19.68/5.26 | Instantiating (270) with all_147_0_85, all_147_1_86, all_147_2_87 yields: % 19.68/5.26 | (284) line_connecting(all_1_5_5, all_1_3_3) = all_147_2_87 & apart_point_and_line(all_1_3_3, all_147_2_87) = all_147_1_86 & distinct_points(all_1_3_3, all_1_5_5) = all_147_0_85 & ( ~ (all_147_1_86 = 0) | (all_147_0_85 = 0 & all_52_3_48 = 0)) % 19.68/5.26 | % 19.68/5.26 | Applying alpha-rule on (284) yields: % 19.68/5.26 | (285) line_connecting(all_1_5_5, all_1_3_3) = all_147_2_87 % 19.68/5.26 | (286) apart_point_and_line(all_1_3_3, all_147_2_87) = all_147_1_86 % 19.68/5.26 | (287) distinct_points(all_1_3_3, all_1_5_5) = all_147_0_85 % 19.68/5.26 | (288) ~ (all_147_1_86 = 0) | (all_147_0_85 = 0 & all_52_3_48 = 0) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (271), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (289) all_52_3_48 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (289) can reduce 240 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (240) ~ (all_52_3_48 = 0) % 19.68/5.27 | (292) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_3_3, all_1_3_3) = v1 & apart_point_and_line(all_1_3_3, v1) = v2 & distinct_points(all_1_3_3, all_1_3_3) = v0 & ( ~ (v2 = 0) | ~ (v0 = 0))) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (263), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (293) all_22_1_16 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (293) can reduce 206 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (206) ~ (all_22_1_16 = 0) % 19.68/5.27 | (296) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (278), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (300) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v1 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_1_0_0, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (277), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (304) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (264), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (308) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v1 & apart_point_and_line(all_1_3_3, all_1_2_2) = v2 & distinct_lines(all_1_0_0, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (265), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (312) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_3_3, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (266), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (316) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_0_0, all_1_2_2) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (267), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (320) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (288), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (321) ~ (all_147_1_86 = 0) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (268), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (325) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (269), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (329) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_0_0, all_1_2_2) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (329), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (330) all_16_1_7 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (330) can reduce 226 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (226) ~ (all_16_1_7 = 0) % 19.68/5.27 | (333) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_0_0, all_1_2_2) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.27 | % 19.68/5.27 | Instantiating (333) with all_196_0_91, all_196_1_92, all_196_2_93, all_196_3_94 yields: % 19.68/5.27 | (334) apart_point_and_line(all_1_5_5, all_1_0_0) = all_196_1_92 & apart_point_and_line(all_1_5_5, all_1_2_2) = all_196_0_91 & distinct_lines(all_1_0_0, all_1_2_2) = all_196_2_93 & distinct_points(all_1_5_5, all_1_5_5) = all_196_3_94 & ( ~ (all_196_2_93 = 0) | ~ (all_196_3_94 = 0) | all_196_0_91 = 0 | all_196_1_92 = 0) % 19.68/5.27 | % 19.68/5.27 | Applying alpha-rule on (334) yields: % 19.68/5.27 | (335) apart_point_and_line(all_1_5_5, all_1_2_2) = all_196_0_91 % 19.68/5.27 | (336) ~ (all_196_2_93 = 0) | ~ (all_196_3_94 = 0) | all_196_0_91 = 0 | all_196_1_92 = 0 % 19.68/5.27 | (337) distinct_points(all_1_5_5, all_1_5_5) = all_196_3_94 % 19.68/5.27 | (338) distinct_lines(all_1_0_0, all_1_2_2) = all_196_2_93 % 19.68/5.27 | (339) apart_point_and_line(all_1_5_5, all_1_0_0) = all_196_1_92 % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (273), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (293) all_22_1_16 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (293) can reduce 206 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (206) ~ (all_22_1_16 = 0) % 19.68/5.27 | (343) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v1 & distinct_lines(all_18_2_11, all_18_2_11) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (243), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (293) all_22_1_16 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (293) can reduce 206 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (206) ~ (all_22_1_16 = 0) % 19.68/5.27 | (347) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_18_2_11) = v2 & distinct_lines(all_18_2_11, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (244), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (348) distinct_lines(all_1_0_0, all_1_2_2) = 0 % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (258), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (352) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_3_3, all_1_0_0) = v1 & distinct_lines(all_1_0_0, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (276), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (356) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_4_4, all_1_0_0) = v1 & distinct_lines(all_1_0_0, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.27 | % 19.68/5.27 | Instantiating (356) with all_237_0_108, all_237_1_109, all_237_2_110 yields: % 19.68/5.27 | (357) apart_point_and_line(all_1_4_4, all_1_0_0) = all_237_0_108 & apart_point_and_line(all_1_4_4, all_1_0_0) = all_237_1_109 & distinct_lines(all_1_0_0, all_1_0_0) = all_237_2_110 & ( ~ (all_237_2_110 = 0) | all_237_0_108 = 0 | all_237_1_109 = 0) % 19.68/5.27 | % 19.68/5.27 | Applying alpha-rule on (357) yields: % 19.68/5.27 | (358) apart_point_and_line(all_1_4_4, all_1_0_0) = all_237_0_108 % 19.68/5.27 | (359) apart_point_and_line(all_1_4_4, all_1_0_0) = all_237_1_109 % 19.68/5.27 | (360) distinct_lines(all_1_0_0, all_1_0_0) = all_237_2_110 % 19.68/5.27 | (361) ~ (all_237_2_110 = 0) | all_237_0_108 = 0 | all_237_1_109 = 0 % 19.68/5.27 | % 19.68/5.27 +-Applying beta-rule and splitting (259), into two cases. % 19.68/5.27 |-Branch one: % 19.68/5.27 | (297) all_32_1_31 = 0 % 19.68/5.27 | % 19.68/5.27 | Equations (297) can reduce 237 to: % 19.68/5.27 | (123) $false % 19.68/5.27 | % 19.68/5.27 |-The branch is then unsatisfiable % 19.68/5.27 |-Branch two: % 19.68/5.27 | (237) ~ (all_32_1_31 = 0) % 19.68/5.27 | (365) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_0_0) = v2 & distinct_lines(all_1_0_0, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (253), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (297) all_32_1_31 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (297) can reduce 237 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (237) ~ (all_32_1_31 = 0) % 19.68/5.28 | (369) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_1_0_0, all_18_2_11) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (246), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (370) all_47_1_43 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (370) can reduce 239 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (239) ~ (all_47_1_43 = 0) % 19.68/5.28 | (373) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (275), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (370) all_47_1_43 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (370) can reduce 239 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (239) ~ (all_47_1_43 = 0) % 19.68/5.28 | (377) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_18_2_11) = v1 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_18_2_11, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (254), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (297) all_32_1_31 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (297) can reduce 237 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (237) ~ (all_32_1_31 = 0) % 19.68/5.28 | (381) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_1_0_0, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (255), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (297) all_32_1_31 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (297) can reduce 237 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (237) ~ (all_32_1_31 = 0) % 19.68/5.28 | (385) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_18_2_11, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (256), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (370) all_47_1_43 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (370) can reduce 239 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (239) ~ (all_47_1_43 = 0) % 19.68/5.28 | (389) all_32_1_31 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (257), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (370) all_47_1_43 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (370) can reduce 239 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (239) ~ (all_47_1_43 = 0) % 19.68/5.28 | (393) all_32_1_31 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (274), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (370) all_47_1_43 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (370) can reduce 239 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (239) ~ (all_47_1_43 = 0) % 19.68/5.28 | (397) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_18_2_11) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (245), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (370) all_47_1_43 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (370) can reduce 239 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (239) ~ (all_47_1_43 = 0) % 19.68/5.28 | (401) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (247), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (370) all_47_1_43 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (370) can reduce 239 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (239) ~ (all_47_1_43 = 0) % 19.68/5.28 | (405) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (248), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (370) all_47_1_43 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (370) can reduce 239 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (239) ~ (all_47_1_43 = 0) % 19.68/5.28 | (409) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (249), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (297) all_32_1_31 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (297) can reduce 237 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (237) ~ (all_32_1_31 = 0) % 19.68/5.28 | (413) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_3_3, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (251), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (297) all_32_1_31 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (297) can reduce 237 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (237) ~ (all_32_1_31 = 0) % 19.68/5.28 | (417) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (252), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (297) all_32_1_31 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (297) can reduce 237 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (237) ~ (all_32_1_31 = 0) % 19.68/5.28 | (421) all_22_1_16 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_18_2_11, all_1_0_0) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (260), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (293) all_22_1_16 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (293) can reduce 206 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (206) ~ (all_22_1_16 = 0) % 19.68/5.28 | (425) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (261), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (293) all_22_1_16 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (293) can reduce 206 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (206) ~ (all_22_1_16 = 0) % 19.68/5.28 | (429) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (262), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (293) all_22_1_16 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (293) can reduce 206 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (206) ~ (all_22_1_16 = 0) % 19.68/5.28 | (433) all_16_1_7 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (304), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (330) all_16_1_7 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (330) can reduce 226 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (226) ~ (all_16_1_7 = 0) % 19.68/5.28 | (437) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.28 | % 19.68/5.28 | Instantiating (437) with all_313_0_124, all_313_1_125, all_313_2_126 yields: % 19.68/5.28 | (438) apart_point_and_line(all_1_4_4, all_1_0_0) = all_313_0_124 & apart_point_and_line(all_1_4_4, all_1_2_2) = all_313_1_125 & distinct_lines(all_1_2_2, all_1_0_0) = all_313_2_126 & ( ~ (all_313_2_126 = 0) | all_313_0_124 = 0 | all_313_1_125 = 0) % 19.68/5.28 | % 19.68/5.28 | Applying alpha-rule on (438) yields: % 19.68/5.28 | (439) apart_point_and_line(all_1_4_4, all_1_0_0) = all_313_0_124 % 19.68/5.28 | (440) apart_point_and_line(all_1_4_4, all_1_2_2) = all_313_1_125 % 19.68/5.28 | (441) distinct_lines(all_1_2_2, all_1_0_0) = all_313_2_126 % 19.68/5.28 | (442) ~ (all_313_2_126 = 0) | all_313_0_124 = 0 | all_313_1_125 = 0 % 19.68/5.28 | % 19.68/5.28 +-Applying beta-rule and splitting (312), into two cases. % 19.68/5.28 |-Branch one: % 19.68/5.28 | (330) all_16_1_7 = 0 % 19.68/5.28 | % 19.68/5.28 | Equations (330) can reduce 226 to: % 19.68/5.28 | (123) $false % 19.68/5.28 | % 19.68/5.28 |-The branch is then unsatisfiable % 19.68/5.28 |-Branch two: % 19.68/5.28 | (226) ~ (all_16_1_7 = 0) % 19.68/5.28 | (446) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_3_3, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.28 | % 19.68/5.28 | Instantiating (446) with all_318_0_127, all_318_1_128, all_318_2_129 yields: % 19.68/5.28 | (447) apart_point_and_line(all_1_3_3, all_1_0_0) = all_318_0_127 & apart_point_and_line(all_1_3_3, all_1_2_2) = all_318_1_128 & distinct_lines(all_1_2_2, all_1_0_0) = all_318_2_129 & ( ~ (all_318_2_129 = 0) | all_318_0_127 = 0 | all_318_1_128 = 0) % 19.68/5.28 | % 19.68/5.28 | Applying alpha-rule on (447) yields: % 19.68/5.28 | (448) apart_point_and_line(all_1_3_3, all_1_0_0) = all_318_0_127 % 19.68/5.29 | (449) apart_point_and_line(all_1_3_3, all_1_2_2) = all_318_1_128 % 19.68/5.29 | (450) distinct_lines(all_1_2_2, all_1_0_0) = all_318_2_129 % 19.68/5.29 | (451) ~ (all_318_2_129 = 0) | all_318_0_127 = 0 | all_318_1_128 = 0 % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (320), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (330) all_16_1_7 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (330) can reduce 226 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (226) ~ (all_16_1_7 = 0) % 19.68/5.29 | (455) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (325), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (330) all_16_1_7 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (330) can reduce 226 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (226) ~ (all_16_1_7 = 0) % 19.68/5.29 | (459) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_5_5, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (369), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (463) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_1_0_0, all_18_2_11) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 | Instantiating (463) with all_343_0_138, all_343_1_139, all_343_2_140, all_343_3_141 yields: % 19.68/5.29 | (464) apart_point_and_line(all_1_4_4, all_1_0_0) = all_343_0_138 & apart_point_and_line(all_1_5_5, all_18_2_11) = all_343_1_139 & distinct_lines(all_1_0_0, all_18_2_11) = all_343_2_140 & distinct_points(all_1_5_5, all_1_4_4) = all_343_3_141 & ( ~ (all_343_2_140 = 0) | ~ (all_343_3_141 = 0) | all_343_0_138 = 0 | all_343_1_139 = 0) % 19.68/5.29 | % 19.68/5.29 | Applying alpha-rule on (464) yields: % 19.68/5.29 | (465) apart_point_and_line(all_1_4_4, all_1_0_0) = all_343_0_138 % 19.68/5.29 | (466) distinct_points(all_1_5_5, all_1_4_4) = all_343_3_141 % 19.68/5.29 | (467) ~ (all_343_2_140 = 0) | ~ (all_343_3_141 = 0) | all_343_0_138 = 0 | all_343_1_139 = 0 % 19.68/5.29 | (468) apart_point_and_line(all_1_5_5, all_18_2_11) = all_343_1_139 % 19.68/5.29 | (469) distinct_lines(all_1_0_0, all_18_2_11) = all_343_2_140 % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (373), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (473) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (377), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (477) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_18_2_11) = v1 & apart_point_and_line(all_1_5_5, all_1_2_2) = v2 & distinct_lines(all_18_2_11, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (381), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (481) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_1_0_0, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 | Instantiating (481) with all_358_0_149, all_358_1_150, all_358_2_151, all_358_3_152 yields: % 19.68/5.29 | (482) apart_point_and_line(all_1_4_4, all_1_0_0) = all_358_1_150 & apart_point_and_line(all_1_5_5, all_18_2_11) = all_358_0_149 & distinct_lines(all_1_0_0, all_18_2_11) = all_358_2_151 & distinct_points(all_1_4_4, all_1_5_5) = all_358_3_152 & ( ~ (all_358_2_151 = 0) | ~ (all_358_3_152 = 0) | all_358_0_149 = 0 | all_358_1_150 = 0) % 19.68/5.29 | % 19.68/5.29 | Applying alpha-rule on (482) yields: % 19.68/5.29 | (483) apart_point_and_line(all_1_4_4, all_1_0_0) = all_358_1_150 % 19.68/5.29 | (484) ~ (all_358_2_151 = 0) | ~ (all_358_3_152 = 0) | all_358_0_149 = 0 | all_358_1_150 = 0 % 19.68/5.29 | (485) apart_point_and_line(all_1_5_5, all_18_2_11) = all_358_0_149 % 19.68/5.29 | (486) distinct_points(all_1_4_4, all_1_5_5) = all_358_3_152 % 19.68/5.29 | (487) distinct_lines(all_1_0_0, all_18_2_11) = all_358_2_151 % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (385), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (491) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_18_2_11, all_1_0_0) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 | Instantiating (491) with all_363_0_153, all_363_1_154, all_363_2_155, all_363_3_156 yields: % 19.68/5.29 | (492) apart_point_and_line(all_1_4_4, all_1_0_0) = all_363_0_153 & apart_point_and_line(all_1_5_5, all_18_2_11) = all_363_1_154 & distinct_lines(all_18_2_11, all_1_0_0) = all_363_2_155 & distinct_points(all_1_5_5, all_1_4_4) = all_363_3_156 & ( ~ (all_363_2_155 = 0) | ~ (all_363_3_156 = 0) | all_363_0_153 = 0 | all_363_1_154 = 0) % 19.68/5.29 | % 19.68/5.29 | Applying alpha-rule on (492) yields: % 19.68/5.29 | (493) distinct_points(all_1_5_5, all_1_4_4) = all_363_3_156 % 19.68/5.29 | (494) apart_point_and_line(all_1_5_5, all_18_2_11) = all_363_1_154 % 19.68/5.29 | (495) distinct_lines(all_18_2_11, all_1_0_0) = all_363_2_155 % 19.68/5.29 | (496) apart_point_and_line(all_1_4_4, all_1_0_0) = all_363_0_153 % 19.68/5.29 | (497) ~ (all_363_2_155 = 0) | ~ (all_363_3_156 = 0) | all_363_0_153 = 0 | all_363_1_154 = 0 % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (397), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (501) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v1 & distinct_lines(all_1_2_2, all_18_2_11) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (401), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (505) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (405), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (509) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (409), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (513) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (421), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (293) all_22_1_16 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (293) can reduce 206 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (206) ~ (all_22_1_16 = 0) % 19.68/5.29 | (517) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_18_2_11, all_1_0_0) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 | Instantiating (517) with all_388_0_172, all_388_1_173, all_388_2_174, all_388_3_175 yields: % 19.68/5.29 | (518) apart_point_and_line(all_1_4_4, all_1_0_0) = all_388_1_173 & apart_point_and_line(all_1_5_5, all_18_2_11) = all_388_0_172 & distinct_lines(all_18_2_11, all_1_0_0) = all_388_2_174 & distinct_points(all_1_4_4, all_1_5_5) = all_388_3_175 & ( ~ (all_388_2_174 = 0) | ~ (all_388_3_175 = 0) | all_388_0_172 = 0 | all_388_1_173 = 0) % 19.68/5.29 | % 19.68/5.29 | Applying alpha-rule on (518) yields: % 19.68/5.29 | (519) distinct_points(all_1_4_4, all_1_5_5) = all_388_3_175 % 19.68/5.29 | (520) distinct_lines(all_18_2_11, all_1_0_0) = all_388_2_174 % 19.68/5.29 | (521) apart_point_and_line(all_1_5_5, all_18_2_11) = all_388_0_172 % 19.68/5.29 | (522) ~ (all_388_2_174 = 0) | ~ (all_388_3_175 = 0) | all_388_0_172 = 0 | all_388_1_173 = 0 % 19.68/5.29 | (523) apart_point_and_line(all_1_4_4, all_1_0_0) = all_388_1_173 % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (425), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (330) all_16_1_7 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (330) can reduce 226 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (226) ~ (all_16_1_7 = 0) % 19.68/5.29 | (527) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_18_2_11, all_1_2_2) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (429), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.29 | (330) all_16_1_7 = 0 % 19.68/5.29 | % 19.68/5.29 | Equations (330) can reduce 226 to: % 19.68/5.29 | (123) $false % 19.68/5.29 | % 19.68/5.29 |-The branch is then unsatisfiable % 19.68/5.29 |-Branch two: % 19.68/5.29 | (226) ~ (all_16_1_7 = 0) % 19.68/5.29 | (531) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & apart_point_and_line(all_1_5_5, all_18_2_11) = v2 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.29 | % 19.68/5.29 +-Applying beta-rule and splitting (433), into two cases. % 19.68/5.29 |-Branch one: % 19.68/5.30 | (330) all_16_1_7 = 0 % 19.68/5.30 | % 19.68/5.30 | Equations (330) can reduce 226 to: % 19.68/5.30 | (123) $false % 19.68/5.30 | % 19.68/5.30 |-The branch is then unsatisfiable % 19.68/5.30 |-Branch two: % 19.68/5.30 | (226) ~ (all_16_1_7 = 0) % 19.68/5.30 | (535) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & apart_point_and_line(all_1_5_5, all_18_2_11) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (8) with all_1_5_5, all_1_3_3, all_147_2_87, all_1_0_0 and discharging atoms line_connecting(all_1_5_5, all_1_3_3) = all_147_2_87, line_connecting(all_1_5_5, all_1_3_3) = all_1_0_0, yields: % 19.68/5.30 | (536) all_147_2_87 = all_1_0_0 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_3_3, all_1_0_0, all_318_0_127, all_147_1_86 and discharging atoms apart_point_and_line(all_1_3_3, all_1_0_0) = all_318_0_127, yields: % 19.68/5.30 | (537) all_318_0_127 = all_147_1_86 | ~ (apart_point_and_line(all_1_3_3, all_1_0_0) = all_147_1_86) % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_3_3, all_1_0_0, all_143_1_80, all_318_0_127 and discharging atoms apart_point_and_line(all_1_3_3, all_1_0_0) = all_318_0_127, apart_point_and_line(all_1_3_3, all_1_0_0) = all_143_1_80, yields: % 19.68/5.30 | (538) all_318_0_127 = all_143_1_80 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_3_3, all_1_2_2, all_318_1_128, all_1_1_1 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_318_1_128, apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, yields: % 19.68/5.30 | (539) all_318_1_128 = all_1_1_1 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_363_0_153, 0 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = all_363_0_153, apart_point_and_line(all_1_4_4, all_1_0_0) = 0, yields: % 19.68/5.30 | (540) all_363_0_153 = 0 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_343_0_138, all_388_1_173 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = all_388_1_173, apart_point_and_line(all_1_4_4, all_1_0_0) = all_343_0_138, yields: % 19.68/5.30 | (541) all_388_1_173 = all_343_0_138 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_343_0_138, all_358_1_150 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = all_358_1_150, apart_point_and_line(all_1_4_4, all_1_0_0) = all_343_0_138, yields: % 19.68/5.30 | (542) all_358_1_150 = all_343_0_138 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_313_0_124, all_363_0_153 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = all_363_0_153, apart_point_and_line(all_1_4_4, all_1_0_0) = all_313_0_124, yields: % 19.68/5.30 | (543) all_363_0_153 = all_313_0_124 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_313_0_124, all_343_0_138 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = all_343_0_138, apart_point_and_line(all_1_4_4, all_1_0_0) = all_313_0_124, yields: % 19.68/5.30 | (544) all_343_0_138 = all_313_0_124 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_237_0_108, all_358_1_150 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = all_358_1_150, apart_point_and_line(all_1_4_4, all_1_0_0) = all_237_0_108, yields: % 19.68/5.30 | (545) all_358_1_150 = all_237_0_108 % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (21) with all_1_4_4, all_1_0_0, all_237_1_109, all_388_1_173 and discharging atoms apart_point_and_line(all_1_4_4, all_1_0_0) = all_388_1_173, apart_point_and_line(all_1_4_4, all_1_0_0) = all_237_1_109, yields: % 19.68/5.30 | (546) all_388_1_173 = all_237_1_109 % 19.68/5.30 | % 19.68/5.30 | Using (359) and (219) yields: % 19.68/5.30 | (547) ~ (all_237_1_109 = all_22_1_16) % 19.68/5.30 | % 19.68/5.30 | Instantiating formula (5) with all_1_0_0, all_1_2_2, all_196_2_93, 0 and discharging atoms distinct_lines(all_1_0_0, all_1_2_2) = all_196_2_93, distinct_lines(all_1_0_0, all_1_2_2) = 0, yields: % 19.68/5.30 | (548) all_196_2_93 = 0 % 19.68/5.30 | % 19.68/5.30 | Combining equations (541,546) yields a new equation: % 19.68/5.30 | (549) all_343_0_138 = all_237_1_109 % 19.68/5.30 | % 19.68/5.30 | Simplifying 549 yields: % 19.68/5.30 | (550) all_343_0_138 = all_237_1_109 % 19.68/5.30 | % 19.68/5.30 | Combining equations (543,540) yields a new equation: % 19.68/5.30 | (551) all_313_0_124 = 0 % 19.68/5.30 | % 19.68/5.30 | Simplifying 551 yields: % 19.68/5.30 | (552) all_313_0_124 = 0 % 19.68/5.30 | % 19.68/5.30 | Combining equations (542,545) yields a new equation: % 19.68/5.30 | (553) all_343_0_138 = all_237_0_108 % 19.68/5.30 | % 19.68/5.30 | Simplifying 553 yields: % 19.68/5.30 | (554) all_343_0_138 = all_237_0_108 % 19.68/5.30 | % 19.68/5.30 | Combining equations (544,554) yields a new equation: % 19.68/5.30 | (555) all_313_0_124 = all_237_0_108 % 19.68/5.30 | % 19.68/5.30 | Simplifying 555 yields: % 19.68/5.30 | (556) all_313_0_124 = all_237_0_108 % 19.68/5.30 | % 19.68/5.30 | Combining equations (550,554) yields a new equation: % 19.68/5.30 | (557) all_237_0_108 = all_237_1_109 % 19.68/5.30 | % 19.68/5.30 | Combining equations (556,552) yields a new equation: % 19.68/5.30 | (558) all_237_0_108 = 0 % 19.68/5.30 | % 19.68/5.30 | Simplifying 558 yields: % 19.68/5.30 | (559) all_237_0_108 = 0 % 19.68/5.30 | % 19.68/5.30 | Combining equations (559,557) yields a new equation: % 19.68/5.30 | (560) all_237_1_109 = 0 % 19.68/5.30 | % 19.68/5.30 | Equations (560) can reduce 547 to: % 19.68/5.30 | (561) ~ (all_22_1_16 = 0) % 19.68/5.30 | % 19.68/5.30 | Simplifying 561 yields: % 19.68/5.30 | (206) ~ (all_22_1_16 = 0) % 19.68/5.30 | % 19.68/5.30 | From (536) and (286) follows: % 19.68/5.30 | (563) apart_point_and_line(all_1_3_3, all_1_0_0) = all_147_1_86 % 19.68/5.30 | % 19.68/5.30 | From (539) and (449) follows: % 19.68/5.30 | (54) apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1 % 19.68/5.30 | % 19.68/5.30 | From (548) and (338) follows: % 19.68/5.30 | (348) distinct_lines(all_1_0_0, all_1_2_2) = 0 % 19.68/5.30 | % 19.68/5.30 +-Applying beta-rule and splitting (413), into two cases. % 19.68/5.30 |-Branch one: % 19.68/5.30 | (122) all_1_1_1 = 0 % 19.68/5.30 | % 19.68/5.30 | Equations (122) can reduce 48 to: % 19.68/5.30 | (123) $false % 19.68/5.30 | % 19.68/5.30 |-The branch is then unsatisfiable % 19.68/5.30 |-Branch two: % 19.68/5.30 | (48) ~ (all_1_1_1 = 0) % 19.68/5.30 | (569) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_1_0_0) = v1 & distinct_points(all_1_3_3, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.30 | % 19.68/5.30 | Instantiating (569) with all_453_0_201, all_453_1_202, all_453_2_203, all_453_3_204 yields: % 19.68/5.30 | (570) apart_point_and_line(all_1_3_3, all_1_0_0) = all_453_1_202 & apart_point_and_line(all_1_5_5, all_1_2_2) = all_453_0_201 & distinct_lines(all_1_2_2, all_1_0_0) = all_453_2_203 & distinct_points(all_1_3_3, all_1_5_5) = all_453_3_204 & ( ~ (all_453_2_203 = 0) | ~ (all_453_3_204 = 0) | all_453_0_201 = 0 | all_453_1_202 = 0) % 19.68/5.30 | % 19.68/5.30 | Applying alpha-rule on (570) yields: % 19.68/5.30 | (571) apart_point_and_line(all_1_3_3, all_1_0_0) = all_453_1_202 % 19.68/5.30 | (572) apart_point_and_line(all_1_5_5, all_1_2_2) = all_453_0_201 % 19.68/5.30 | (573) distinct_points(all_1_3_3, all_1_5_5) = all_453_3_204 % 19.68/5.30 | (574) distinct_lines(all_1_2_2, all_1_0_0) = all_453_2_203 % 19.68/5.30 | (575) ~ (all_453_2_203 = 0) | ~ (all_453_3_204 = 0) | all_453_0_201 = 0 | all_453_1_202 = 0 % 19.68/5.30 | % 19.68/5.30 +-Applying beta-rule and splitting (242), into two cases. % 19.68/5.30 |-Branch one: % 19.68/5.30 | (293) all_22_1_16 = 0 % 19.68/5.30 | % 19.68/5.30 | Equations (293) can reduce 206 to: % 19.68/5.30 | (123) $false % 19.68/5.30 | % 19.68/5.30 |-The branch is then unsatisfiable % 19.68/5.30 |-Branch two: % 19.68/5.30 | (206) ~ (all_22_1_16 = 0) % 19.68/5.30 | (579) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_18_2_11) = v3 & apart_point_and_line(all_1_4_4, all_1_2_2) = v2 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_4_4, all_1_3_3) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.30 | % 19.68/5.30 +-Applying beta-rule and splitting (241), into two cases. % 19.68/5.30 |-Branch one: % 19.68/5.30 | (293) all_22_1_16 = 0 % 19.68/5.30 | % 19.68/5.30 | Equations (293) can reduce 206 to: % 19.68/5.30 | (123) $false % 19.68/5.30 | % 19.68/5.30 |-The branch is then unsatisfiable % 19.68/5.30 |-Branch two: % 19.68/5.30 | (206) ~ (all_22_1_16 = 0) % 19.68/5.30 | (583) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_3_3, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.30 | % 19.68/5.30 +-Applying beta-rule and splitting (583), into two cases. % 19.68/5.30 |-Branch one: % 19.68/5.30 | (122) all_1_1_1 = 0 % 19.68/5.30 | % 19.68/5.30 | Equations (122) can reduce 48 to: % 19.68/5.30 | (123) $false % 19.68/5.30 | % 19.68/5.30 |-The branch is then unsatisfiable % 19.68/5.30 |-Branch two: % 19.68/5.30 | (48) ~ (all_1_1_1 = 0) % 19.68/5.30 | (587) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_18_2_11) = v2 & apart_point_and_line(all_1_4_4, all_1_2_2) = v3 & distinct_lines(all_1_2_2, all_18_2_11) = v1 & distinct_points(all_1_3_3, all_1_4_4) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.30 | % 19.68/5.30 +-Applying beta-rule and splitting (308), into two cases. % 19.68/5.30 |-Branch one: % 19.68/5.30 | (330) all_16_1_7 = 0 % 19.68/5.30 | % 19.68/5.30 | Equations (330) can reduce 226 to: % 19.68/5.30 | (123) $false % 19.68/5.30 | % 19.68/5.30 |-The branch is then unsatisfiable % 19.68/5.30 |-Branch two: % 19.68/5.30 | (226) ~ (all_16_1_7 = 0) % 19.68/5.30 | (591) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v1 & apart_point_and_line(all_1_3_3, all_1_2_2) = v2 & distinct_lines(all_1_0_0, all_1_2_2) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 19.68/5.30 | % 19.68/5.30 | Instantiating (591) with all_493_0_209, all_493_1_210, all_493_2_211 yields: % 19.68/5.30 | (592) apart_point_and_line(all_1_3_3, all_1_0_0) = all_493_1_210 & apart_point_and_line(all_1_3_3, all_1_2_2) = all_493_0_209 & distinct_lines(all_1_0_0, all_1_2_2) = all_493_2_211 & ( ~ (all_493_2_211 = 0) | all_493_0_209 = 0 | all_493_1_210 = 0) % 19.68/5.30 | % 19.68/5.30 | Applying alpha-rule on (592) yields: % 19.68/5.30 | (593) apart_point_and_line(all_1_3_3, all_1_0_0) = all_493_1_210 % 19.68/5.30 | (594) apart_point_and_line(all_1_3_3, all_1_2_2) = all_493_0_209 % 19.68/5.30 | (595) distinct_lines(all_1_0_0, all_1_2_2) = all_493_2_211 % 19.68/5.30 | (596) ~ (all_493_2_211 = 0) | all_493_0_209 = 0 | all_493_1_210 = 0 % 19.68/5.30 | % 19.68/5.30 +-Applying beta-rule and splitting (537), into two cases. % 19.68/5.30 |-Branch one: % 19.68/5.30 | (597) ~ (apart_point_and_line(all_1_3_3, all_1_0_0) = all_147_1_86) % 19.68/5.30 | % 19.68/5.30 | Using (563) and (597) yields: % 19.68/5.30 | (221) $false % 19.68/5.30 | % 19.68/5.30 |-The branch is then unsatisfiable % 19.68/5.30 |-Branch two: % 19.68/5.31 | (563) apart_point_and_line(all_1_3_3, all_1_0_0) = all_147_1_86 % 19.68/5.31 | (600) all_318_0_127 = all_147_1_86 % 19.68/5.31 | % 19.68/5.31 | Combining equations (538,600) yields a new equation: % 19.68/5.31 | (601) all_147_1_86 = all_143_1_80 % 19.68/5.31 | % 19.68/5.31 | Equations (601) can reduce 321 to: % 19.68/5.31 | (602) ~ (all_143_1_80 = 0) % 19.68/5.31 | % 19.68/5.31 | From (601) and (563) follows: % 19.68/5.31 | (280) apart_point_and_line(all_1_3_3, all_1_0_0) = all_143_1_80 % 19.68/5.31 | % 19.68/5.31 | Instantiating formula (21) with all_1_3_3, all_1_0_0, all_493_1_210, all_143_1_80 and discharging atoms apart_point_and_line(all_1_3_3, all_1_0_0) = all_493_1_210, apart_point_and_line(all_1_3_3, all_1_0_0) = all_143_1_80, yields: % 19.68/5.31 | (604) all_493_1_210 = all_143_1_80 % 19.68/5.31 | % 19.68/5.31 | Instantiating formula (21) with all_1_3_3, all_1_0_0, all_453_1_202, all_493_1_210 and discharging atoms apart_point_and_line(all_1_3_3, all_1_0_0) = all_493_1_210, apart_point_and_line(all_1_3_3, all_1_0_0) = all_453_1_202, yields: % 19.68/5.31 | (605) all_493_1_210 = all_453_1_202 % 19.68/5.31 | % 19.68/5.31 | Instantiating formula (21) with all_1_3_3, all_1_2_2, all_493_0_209, all_1_1_1 and discharging atoms apart_point_and_line(all_1_3_3, all_1_2_2) = all_493_0_209, apart_point_and_line(all_1_3_3, all_1_2_2) = all_1_1_1, yields: % 19.68/5.31 | (606) all_493_0_209 = all_1_1_1 % 19.68/5.31 | % 19.68/5.31 | Instantiating formula (5) with all_1_0_0, all_1_2_2, all_493_2_211, 0 and discharging atoms distinct_lines(all_1_0_0, all_1_2_2) = all_493_2_211, distinct_lines(all_1_0_0, all_1_2_2) = 0, yields: % 19.68/5.31 | (607) all_493_2_211 = 0 % 19.68/5.31 | % 19.68/5.31 | Combining equations (604,605) yields a new equation: % 19.68/5.31 | (608) all_453_1_202 = all_143_1_80 % 19.68/5.31 | % 19.68/5.31 | Combining equations (608,605) yields a new equation: % 19.68/5.31 | (604) all_493_1_210 = all_143_1_80 % 19.68/5.31 | % 19.68/5.31 +-Applying beta-rule and splitting (250), into two cases. % 19.68/5.31 |-Branch one: % 19.68/5.31 | (297) all_32_1_31 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (297) can reduce 237 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (237) ~ (all_32_1_31 = 0) % 19.68/5.31 | (613) all_1_1_1 = 0 | ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_0_0, all_1_2_2) = v1 & distinct_points(all_1_3_3, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.31 | % 19.68/5.31 +-Applying beta-rule and splitting (613), into two cases. % 19.68/5.31 |-Branch one: % 19.68/5.31 | (122) all_1_1_1 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (122) can reduce 48 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (48) ~ (all_1_1_1 = 0) % 19.68/5.31 | (617) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (apart_point_and_line(all_1_3_3, all_1_0_0) = v2 & apart_point_and_line(all_1_5_5, all_1_2_2) = v3 & distinct_lines(all_1_0_0, all_1_2_2) = v1 & distinct_points(all_1_3_3, all_1_5_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 19.68/5.31 | % 19.68/5.31 +-Applying beta-rule and splitting (596), into two cases. % 19.68/5.31 |-Branch one: % 19.68/5.31 | (618) ~ (all_493_2_211 = 0) % 19.68/5.31 | % 19.68/5.31 | Equations (607) can reduce 618 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (607) all_493_2_211 = 0 % 19.68/5.31 | (621) all_493_0_209 = 0 | all_493_1_210 = 0 % 19.68/5.31 | % 19.68/5.31 +-Applying beta-rule and splitting (621), into two cases. % 19.68/5.31 |-Branch one: % 19.68/5.31 | (622) all_493_0_209 = 0 % 19.68/5.31 | % 19.68/5.31 | Combining equations (622,606) yields a new equation: % 19.68/5.31 | (122) all_1_1_1 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (122) can reduce 48 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (625) ~ (all_493_0_209 = 0) % 19.68/5.31 | (626) all_493_1_210 = 0 % 19.68/5.31 | % 19.68/5.31 | Combining equations (626,604) yields a new equation: % 19.68/5.31 | (627) all_143_1_80 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (627) can reduce 602 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (629) ~ (distinct_lines(all_1_0_0, all_1_2_2) = 0) % 19.68/5.31 | (370) all_47_1_43 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (370) can reduce 239 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (632) all_147_1_86 = 0 % 19.68/5.31 | (633) all_147_0_85 = 0 & all_52_3_48 = 0 % 19.68/5.31 | % 19.68/5.31 | Applying alpha-rule on (633) yields: % 19.68/5.31 | (634) all_147_0_85 = 0 % 19.68/5.31 | (289) all_52_3_48 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (289) can reduce 240 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (637) apart_point_and_line(all_1_4_4, all_1_0_0) = all_22_1_16 % 19.68/5.31 | (293) all_22_1_16 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (293) can reduce 206 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (640) apart_point_and_line(all_1_4_4, all_1_2_2) = 0 % 19.68/5.31 | (641) ? [v0] : ? [v1] : ? [v2] : (distinct_points(all_1_4_4, all_1_4_4) = v2 & distinct_points(all_1_4_4, all_1_5_5) = v1 & distinct_points(all_1_5_5, all_1_4_4) = v0 & ( ~ (v0 = 0) | (v2 = 0 & v1 = 0))) % 19.68/5.31 | % 19.68/5.31 | Instantiating (641) with all_82_0_219, all_82_1_220, all_82_2_221 yields: % 19.68/5.31 | (642) distinct_points(all_1_4_4, all_1_4_4) = all_82_0_219 & distinct_points(all_1_4_4, all_1_5_5) = all_82_1_220 & distinct_points(all_1_5_5, all_1_4_4) = all_82_2_221 & ( ~ (all_82_2_221 = 0) | (all_82_0_219 = 0 & all_82_1_220 = 0)) % 19.68/5.31 | % 19.68/5.31 | Applying alpha-rule on (642) yields: % 19.68/5.31 | (643) distinct_points(all_1_4_4, all_1_4_4) = all_82_0_219 % 19.68/5.31 | (644) distinct_points(all_1_4_4, all_1_5_5) = all_82_1_220 % 19.68/5.31 | (645) distinct_points(all_1_5_5, all_1_4_4) = all_82_2_221 % 19.68/5.31 | (646) ~ (all_82_2_221 = 0) | (all_82_0_219 = 0 & all_82_1_220 = 0) % 19.68/5.31 | % 19.68/5.31 | Instantiating formula (46) with all_1_4_4, all_1_4_4, all_82_0_219, all_22_0_15 and discharging atoms distinct_points(all_1_4_4, all_1_4_4) = all_82_0_219, distinct_points(all_1_4_4, all_1_4_4) = all_22_0_15, yields: % 19.68/5.31 | (647) all_82_0_219 = all_22_0_15 % 19.68/5.31 | % 19.68/5.31 | Using (643) and (56) yields: % 19.68/5.31 | (648) ~ (all_82_0_219 = 0) % 19.68/5.31 | % 19.68/5.31 | Instantiating formula (46) with all_1_5_5, all_1_4_4, all_82_2_221, 0 and discharging atoms distinct_points(all_1_5_5, all_1_4_4) = all_82_2_221, distinct_points(all_1_5_5, all_1_4_4) = 0, yields: % 19.68/5.31 | (649) all_82_2_221 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (647) can reduce 648 to: % 19.68/5.31 | (165) ~ (all_22_0_15 = 0) % 19.68/5.31 | % 19.68/5.31 +-Applying beta-rule and splitting (646), into two cases. % 19.68/5.31 |-Branch one: % 19.68/5.31 | (651) ~ (all_82_2_221 = 0) % 19.68/5.31 | % 19.68/5.31 | Equations (649) can reduce 651 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (649) all_82_2_221 = 0 % 19.68/5.31 | (654) all_82_0_219 = 0 & all_82_1_220 = 0 % 19.68/5.31 | % 19.68/5.31 | Applying alpha-rule on (654) yields: % 19.68/5.31 | (655) all_82_0_219 = 0 % 19.68/5.31 | (656) all_82_1_220 = 0 % 19.68/5.31 | % 19.68/5.31 | Combining equations (655,647) yields a new equation: % 19.68/5.31 | (657) all_22_0_15 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (657) can reduce 165 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (659) all_34_1_34 = 0 % 19.68/5.31 | (660) all_34_0_33 = 0 % 19.68/5.31 | % 19.68/5.31 | Combining equations (660,177) yields a new equation: % 19.68/5.31 | (661) all_16_0_6 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (661) can reduce 195 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (663) all_28_1_25 = 0 % 19.68/5.31 | (664) all_28_0_24 = 0 % 19.68/5.31 | % 19.68/5.31 | Combining equations (186,664) yields a new equation: % 19.68/5.31 | (665) all_16_0_6 = 0 % 19.68/5.31 | % 19.68/5.31 | Simplifying 665 yields: % 19.68/5.31 | (661) all_16_0_6 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (661) can reduce 195 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 |-Branch two: % 19.68/5.31 | (293) all_22_1_16 = 0 % 19.68/5.31 | (657) all_22_0_15 = 0 % 19.68/5.31 | % 19.68/5.31 | Equations (657) can reduce 165 to: % 19.68/5.31 | (123) $false % 19.68/5.31 | % 19.68/5.31 |-The branch is then unsatisfiable % 19.68/5.31 % SZS output end Proof for theBenchmark % 19.68/5.31 % 19.68/5.31 4722ms %------------------------------------------------------------------------------