%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GEO225+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:57 EDT 2022 % Result : Theorem 8.61s 2.57s % Output : Proof 11.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GEO225+2 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 17 21:15:58 EDT 2022 % 0.12/0.33 % CPUTime : % 0.50/0.58 ____ _ % 0.50/0.58 ___ / __ \_____(_)___ ________ __________ % 0.50/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.50/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.50/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.50/0.58 % 0.50/0.58 A Theorem Prover for First-Order Logic % 0.50/0.58 (ePrincess v.1.0) % 0.50/0.58 % 0.50/0.58 (c) Philipp Rümmer, 2009-2015 % 0.50/0.58 (c) Peter Backeman, 2014-2015 % 0.50/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.50/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.50/0.58 Bug reports to peter@backeman.se % 0.50/0.58 % 0.50/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.50/0.58 % 0.50/0.58 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.50/0.62 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.54/0.90 Prover 0: Preprocessing ... % 2.18/1.06 Prover 0: Warning: ignoring some quantifiers % 2.24/1.08 Prover 0: Constructing countermodel ... % 2.80/1.24 Prover 0: gave up % 2.80/1.24 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.80/1.27 Prover 1: Preprocessing ... % 3.29/1.38 Prover 1: Constructing countermodel ... % 3.29/1.41 Prover 1: gave up % 3.29/1.41 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.57/1.44 Prover 2: Preprocessing ... % 4.16/1.57 Prover 2: Warning: ignoring some quantifiers % 4.33/1.58 Prover 2: Constructing countermodel ... % 4.62/1.65 Prover 2: gave up % 4.62/1.65 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 4.68/1.67 Prover 3: Preprocessing ... % 4.68/1.69 Prover 3: Warning: ignoring some quantifiers % 4.68/1.69 Prover 3: Constructing countermodel ... % 4.68/1.73 Prover 3: gave up % 4.68/1.73 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 5.00/1.75 Prover 4: Preprocessing ... % 5.41/1.84 Prover 4: Warning: ignoring some quantifiers % 5.41/1.84 Prover 4: Constructing countermodel ... % 7.95/2.42 Prover 4: gave up % 7.95/2.42 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 7.95/2.44 Prover 5: Preprocessing ... % 8.21/2.49 Prover 5: Constructing countermodel ... % 8.61/2.57 Prover 5: proved (145ms) % 8.61/2.57 % 8.61/2.57 No countermodel exists, formula is valid % 8.61/2.57 % SZS status Theorem for theBenchmark % 8.61/2.57 % 8.61/2.57 Generating proof ... found it (size 59) % 11.41/3.19 % 11.41/3.19 % SZS output start Proof for theBenchmark % 11.41/3.19 Assumed formulas after preprocessing and simplification: % 11.41/3.19 | (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 | ~ (orthogonal_through_point(v3, v2) = v1) | ~ (orthogonal_through_point(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (parallel_through_point(v3, v2) = v1) | ~ (parallel_through_point(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (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] : ! [v2] : (v1 = v0 | ~ (point(v2) = v1) | ~ (point(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (line(v2) = v1) | ~ (line(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (orthogonal_through_point(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (point(v1) = v4 & line(v2) = v5 & line(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (parallel_through_point(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (point(v1) = v4 & line(v2) = v5 & line(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (point(v2) = v6 & line(v1) = v4 & line(v0) = v3 & convergent_lines(v0, v1) = v5 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | v6 = 0))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (point(v1) = v4 & point(v0) = v3 & line(v2) = v6 & distinct_points(v0, v1) = v5 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | v6 = 0))) & ! [v0] : ! [v1] : ( ~ (point(v1) = 0) | ~ (point(v0) = 0) | ? [v2] : ? [v3] : ? [v4] : (line(v3) = v4 & line_connecting(v0, v1) = v3 & distinct_points(v0, v1) = v2 & ( ~ (v2 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ( ~ (point(v1) = 0) | ~ (line(v0) = 0) | ? [v2] : (orthogonal_through_point(v0, v1) = v2 & line(v2) = 0)) & ! [v0] : ! [v1] : ( ~ (point(v1) = 0) | ~ (line(v0) = 0) | ? [v2] : (parallel_through_point(v0, v1) = v2 & line(v2) = 0)) & ! [v0] : ! [v1] : ( ~ (line(v1) = 0) | ~ (line(v0) = 0) | ? [v2] : ? [v3] : ? [v4] : (point(v3) = v4 & intersection_point(v0, v1) = v3 & convergent_lines(v0, v1) = v2 & ( ~ (v2 = 0) | v4 = 0))) & ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v0, v1) = 0) & ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (point(v4) = v5 & line(v1) = v3 & line(v0) = v2 & intersection_point(v0, v1) = v4 & ( ~ (v3 = 0) | ~ (v2 = 0) | v5 = 0))) & ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (point(v1) = v3 & point(v0) = v2 & line(v4) = v5 & line_connecting(v0, v1) = v4 & ( ~ (v3 = 0) | ~ (v2 = 0) | v5 = 0))) & ! [v0] : ~ (convergent_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_lines(v0, v0) = 0) & ! [v0] : ~ (distinct_points(v0, v0) = 0) & ? [v0] : ? [v1] : (point(v1) = 0 & point(v0) = 0 & distinct_points(v0, v1) = 0 & ! [v2] : ! [v3] : (v3 = 0 | ~ (line(v2) = v3)) & ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v1, v2) = v3) | apart_point_and_line(v0, v2) = 0) & ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | apart_point_and_line(v1, v2) = 0)) % 11.58/3.25 | Applying alpha-rule on (0) yields: % 11.58/3.25 | (1) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_lines(v3, v2) = v1) | ~ (distinct_lines(v3, v2) = v0)) % 11.58/3.25 | (2) ! [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)))) % 11.58/3.25 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (line_connecting(v3, v2) = v1) | ~ (line_connecting(v3, v2) = v0)) % 11.58/3.25 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (convergent_lines(v3, v2) = v1) | ~ (convergent_lines(v3, v2) = v0)) % 11.70/3.25 | (5) ! [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))))) % 11.70/3.25 | (6) ! [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)) % 11.70/3.25 | (7) ! [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))) % 11.70/3.25 | (8) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | distinct_lines(v0, v1) = 0) % 11.70/3.25 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v0, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v1, v2) = 0) % 11.70/3.25 | (10) ! [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))) % 11.70/3.25 | (11) ! [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))) % 11.70/3.25 | (12) ! [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))) % 11.70/3.25 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v0, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v1, v2) = 0) % 11.70/3.25 | (14) ! [v0] : ! [v1] : ( ~ (point(v1) = 0) | ~ (line(v0) = 0) | ? [v2] : (parallel_through_point(v0, v1) = v2 & line(v2) = 0)) % 11.70/3.25 | (15) ! [v0] : ~ (distinct_lines(v0, v0) = 0) % 11.70/3.25 | (16) ! [v0] : ! [v1] : ( ~ (point(v1) = 0) | ~ (point(v0) = 0) | ? [v2] : ? [v3] : ? [v4] : (line(v3) = v4 & line_connecting(v0, v1) = v3 & distinct_points(v0, v1) = v2 & ( ~ (v2 = 0) | v4 = 0))) % 11.70/3.26 | (17) ! [v0] : ! [v1] : ( ~ (point(v1) = 0) | ~ (line(v0) = 0) | ? [v2] : (orthogonal_through_point(v0, v1) = v2 & line(v2) = 0)) % 11.70/3.26 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_lines(v1, v2) = v3) | ~ (distinct_lines(v0, v1) = 0) | distinct_lines(v0, v2) = 0) % 11.70/3.26 | (19) ! [v0] : ! [v1] : ( ~ (distinct_points(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (point(v1) = v3 & point(v0) = v2 & line(v4) = v5 & line_connecting(v0, v1) = v4 & ( ~ (v3 = 0) | ~ (v2 = 0) | v5 = 0))) % 11.70/3.26 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (orthogonal_through_point(v3, v2) = v1) | ~ (orthogonal_through_point(v3, v2) = v0)) % 11.70/3.26 | (21) ! [v0] : ! [v1] : ! [v2] : ( ~ (parallel_through_point(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (point(v1) = v4 & line(v2) = v5 & line(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 11.70/3.26 | (22) ! [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)) % 11.70/3.26 | (23) ! [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))))) % 11.70/3.26 | (24) ! [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))) % 11.70/3.26 | (25) ! [v0] : ~ (convergent_lines(v0, v0) = 0) % 11.70/3.26 | (26) ! [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) % 11.70/3.26 | (27) ! [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)))) % 11.70/3.26 | (28) ! [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))) % 11.70/3.26 | (29) ! [v0] : ! [v1] : ( ~ (line(v1) = 0) | ~ (line(v0) = 0) | ? [v2] : ? [v3] : ? [v4] : (point(v3) = v4 & intersection_point(v0, v1) = v3 & convergent_lines(v0, v1) = v2 & ( ~ (v2 = 0) | v4 = 0))) % 11.70/3.26 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (distinct_points(v3, v2) = v1) | ~ (distinct_points(v3, v2) = v0)) % 11.70/3.26 | (31) ! [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))))) % 11.70/3.26 | (32) ! [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)) % 11.70/3.26 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (apart_point_and_line(v3, v2) = v1) | ~ (apart_point_and_line(v3, v2) = v0)) % 11.70/3.26 | (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)) % 11.70/3.26 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v0, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v1, v2) = 0) % 11.70/3.26 | (36) ! [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))))) % 11.70/3.26 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (distinct_points(v1, v2) = v3) | ~ (distinct_points(v0, v1) = 0) | distinct_points(v0, v2) = 0) % 11.70/3.27 | (38) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (point(v2) = v1) | ~ (point(v2) = v0)) % 11.70/3.27 | (39) ! [v0] : ! [v1] : ( ~ (convergent_lines(v0, v1) = 0) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (point(v4) = v5 & line(v1) = v3 & line(v0) = v2 & intersection_point(v0, v1) = v4 & ( ~ (v3 = 0) | ~ (v2 = 0) | v5 = 0))) % 11.70/3.27 | (40) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (line(v2) = v1) | ~ (line(v2) = v0)) % 11.70/3.27 | (41) ! [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)))) % 11.70/3.27 | (42) ! [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)) % 11.70/3.27 | (43) ! [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))))) % 11.70/3.27 | (44) ! [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)) % 11.70/3.27 | (45) ! [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) % 11.70/3.27 | (46) ! [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) % 11.70/3.27 | (47) ! [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) % 11.70/3.27 | (48) ! [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))) % 11.70/3.27 | (49) ! [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))) % 11.70/3.27 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (intersection_point(v3, v2) = v1) | ~ (intersection_point(v3, v2) = v0)) % 11.70/3.27 | (51) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (parallel_through_point(v3, v2) = v1) | ~ (parallel_through_point(v3, v2) = v0)) % 11.70/3.27 | (52) ! [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)))) % 11.70/3.27 | (53) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (convergent_lines(v1, v2) = v3) | ~ (convergent_lines(v0, v1) = 0) | convergent_lines(v0, v2) = 0) % 11.70/3.27 | (54) ? [v0] : ? [v1] : (point(v1) = 0 & point(v0) = 0 & distinct_points(v0, v1) = 0 & ! [v2] : ! [v3] : (v3 = 0 | ~ (line(v2) = v3)) & ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v1, v2) = v3) | apart_point_and_line(v0, v2) = 0) & ! [v2] : ! [v3] : (v3 = 0 | ~ (apart_point_and_line(v0, v2) = v3) | apart_point_and_line(v1, v2) = 0)) % 11.70/3.27 | (55) ! [v0] : ! [v1] : ! [v2] : ( ~ (intersection_point(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (point(v2) = v6 & line(v1) = v4 & line(v0) = v3 & convergent_lines(v0, v1) = v5 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | v6 = 0))) % 11.70/3.27 | (56) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (distinct_lines(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & convergent_lines(v0, v1) = v3)) % 11.70/3.27 | (57) ! [v0] : ~ (distinct_points(v0, v0) = 0) % 11.70/3.27 | (58) ! [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)))) % 11.70/3.28 | (59) ! [v0] : ! [v1] : ! [v2] : ( ~ (line_connecting(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (point(v1) = v4 & point(v0) = v3 & line(v2) = v6 & distinct_points(v0, v1) = v5 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v3 = 0) | v6 = 0))) % 11.70/3.28 | (60) ! [v0] : ! [v1] : ! [v2] : ( ~ (orthogonal_through_point(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (point(v1) = v4 & line(v2) = v5 & line(v0) = v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 11.70/3.28 | % 11.70/3.28 | Instantiating (54) with all_1_0_0, all_1_1_1 yields: % 11.70/3.28 | (61) point(all_1_0_0) = 0 & point(all_1_1_1) = 0 & distinct_points(all_1_1_1, all_1_0_0) = 0 & ! [v0] : ! [v1] : (v1 = 0 | ~ (line(v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (apart_point_and_line(all_1_0_0, v0) = v1) | apart_point_and_line(all_1_1_1, v0) = 0) & ! [v0] : ! [v1] : (v1 = 0 | ~ (apart_point_and_line(all_1_1_1, v0) = v1) | apart_point_and_line(all_1_0_0, v0) = 0) % 11.70/3.28 | % 11.70/3.28 | Applying alpha-rule on (61) yields: % 11.70/3.28 | (62) distinct_points(all_1_1_1, all_1_0_0) = 0 % 11.70/3.28 | (63) ! [v0] : ! [v1] : (v1 = 0 | ~ (apart_point_and_line(all_1_1_1, v0) = v1) | apart_point_and_line(all_1_0_0, v0) = 0) % 11.70/3.28 | (64) ! [v0] : ! [v1] : (v1 = 0 | ~ (apart_point_and_line(all_1_0_0, v0) = v1) | apart_point_and_line(all_1_1_1, v0) = 0) % 11.70/3.28 | (65) point(all_1_0_0) = 0 % 11.70/3.28 | (66) ! [v0] : ! [v1] : (v1 = 0 | ~ (line(v0) = v1)) % 11.70/3.28 | (67) point(all_1_1_1) = 0 % 11.70/3.28 | % 11.70/3.28 | Instantiating formula (57) with all_1_1_1 yields: % 11.70/3.28 | (68) ~ (distinct_points(all_1_1_1, all_1_1_1) = 0) % 11.70/3.28 | % 11.70/3.28 | Instantiating formula (16) with all_1_0_0, all_1_0_0 and discharging atoms point(all_1_0_0) = 0, yields: % 11.70/3.28 | (69) ? [v0] : ? [v1] : ? [v2] : (line(v1) = v2 & line_connecting(all_1_0_0, all_1_0_0) = v1 & distinct_points(all_1_0_0, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0)) % 11.70/3.28 | % 11.70/3.28 | Instantiating formula (16) with all_1_0_0, all_1_1_1 and discharging atoms point(all_1_0_0) = 0, point(all_1_1_1) = 0, yields: % 11.70/3.28 | (70) ? [v0] : ? [v1] : ? [v2] : (line(v1) = v2 & line_connecting(all_1_1_1, all_1_0_0) = v1 & distinct_points(all_1_1_1, all_1_0_0) = v0 & ( ~ (v0 = 0) | v2 = 0)) % 11.70/3.28 | % 11.70/3.28 | Instantiating formula (16) with all_1_1_1, all_1_1_1 and discharging atoms point(all_1_1_1) = 0, yields: % 11.70/3.28 | (71) ? [v0] : ? [v1] : ? [v2] : (line(v1) = v2 & line_connecting(all_1_1_1, all_1_1_1) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v0 & ( ~ (v0 = 0) | v2 = 0)) % 11.70/3.28 | % 11.70/3.28 | Instantiating formula (2) with 0, all_1_1_1, all_1_0_0, all_1_1_1 and discharging atoms distinct_points(all_1_1_1, all_1_0_0) = 0, yields: % 11.70/3.28 | (72) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_1_1, all_1_0_0) = v0 & apart_point_and_line(all_1_1_1, v0) = v1 & distinct_points(all_1_1_1, all_1_1_1) = v2 & ( ~ (v1 = 0) | v2 = 0)) % 11.70/3.28 | % 11.70/3.28 | Instantiating formula (19) with all_1_0_0, all_1_1_1 and discharging atoms distinct_points(all_1_1_1, all_1_0_0) = 0, yields: % 11.70/3.28 | (73) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (point(all_1_0_0) = v1 & point(all_1_1_1) = v0 & line(v2) = v3 & line_connecting(all_1_1_1, all_1_0_0) = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 11.70/3.28 | % 11.70/3.28 | Instantiating (73) with all_17_0_2, all_17_1_3, all_17_2_4, all_17_3_5 yields: % 11.70/3.28 | (74) point(all_1_0_0) = all_17_2_4 & point(all_1_1_1) = all_17_3_5 & line(all_17_1_3) = all_17_0_2 & line_connecting(all_1_1_1, all_1_0_0) = all_17_1_3 & ( ~ (all_17_2_4 = 0) | ~ (all_17_3_5 = 0) | all_17_0_2 = 0) % 11.70/3.28 | % 11.70/3.28 | Applying alpha-rule on (74) yields: % 11.70/3.28 | (75) line(all_17_1_3) = all_17_0_2 % 11.70/3.28 | (76) line_connecting(all_1_1_1, all_1_0_0) = all_17_1_3 % 11.70/3.28 | (77) point(all_1_1_1) = all_17_3_5 % 11.70/3.28 | (78) ~ (all_17_2_4 = 0) | ~ (all_17_3_5 = 0) | all_17_0_2 = 0 % 11.70/3.28 | (79) point(all_1_0_0) = all_17_2_4 % 11.70/3.28 | % 11.70/3.28 | Instantiating (71) with all_19_0_6, all_19_1_7, all_19_2_8 yields: % 11.70/3.28 | (80) line(all_19_1_7) = all_19_0_6 & line_connecting(all_1_1_1, all_1_1_1) = all_19_1_7 & distinct_points(all_1_1_1, all_1_1_1) = all_19_2_8 & ( ~ (all_19_2_8 = 0) | all_19_0_6 = 0) % 11.70/3.28 | % 11.70/3.28 | Applying alpha-rule on (80) yields: % 11.70/3.28 | (81) line(all_19_1_7) = all_19_0_6 % 11.70/3.28 | (82) line_connecting(all_1_1_1, all_1_1_1) = all_19_1_7 % 11.70/3.28 | (83) distinct_points(all_1_1_1, all_1_1_1) = all_19_2_8 % 11.70/3.28 | (84) ~ (all_19_2_8 = 0) | all_19_0_6 = 0 % 11.70/3.28 | % 11.70/3.29 | Instantiating (70) with all_21_0_9, all_21_1_10, all_21_2_11 yields: % 11.70/3.29 | (85) line(all_21_1_10) = all_21_0_9 & line_connecting(all_1_1_1, all_1_0_0) = all_21_1_10 & distinct_points(all_1_1_1, all_1_0_0) = all_21_2_11 & ( ~ (all_21_2_11 = 0) | all_21_0_9 = 0) % 11.70/3.29 | % 11.70/3.29 | Applying alpha-rule on (85) yields: % 11.70/3.29 | (86) line(all_21_1_10) = all_21_0_9 % 11.70/3.29 | (87) line_connecting(all_1_1_1, all_1_0_0) = all_21_1_10 % 11.70/3.29 | (88) distinct_points(all_1_1_1, all_1_0_0) = all_21_2_11 % 11.70/3.29 | (89) ~ (all_21_2_11 = 0) | all_21_0_9 = 0 % 11.70/3.29 | % 11.70/3.29 | Instantiating (72) with all_23_0_12, all_23_1_13, all_23_2_14 yields: % 11.70/3.29 | (90) line_connecting(all_1_1_1, all_1_0_0) = all_23_2_14 & apart_point_and_line(all_1_1_1, all_23_2_14) = all_23_1_13 & distinct_points(all_1_1_1, all_1_1_1) = all_23_0_12 & ( ~ (all_23_1_13 = 0) | all_23_0_12 = 0) % 11.70/3.29 | % 11.70/3.29 | Applying alpha-rule on (90) yields: % 11.70/3.29 | (91) line_connecting(all_1_1_1, all_1_0_0) = all_23_2_14 % 11.70/3.29 | (92) apart_point_and_line(all_1_1_1, all_23_2_14) = all_23_1_13 % 11.70/3.29 | (93) distinct_points(all_1_1_1, all_1_1_1) = all_23_0_12 % 11.70/3.29 | (94) ~ (all_23_1_13 = 0) | all_23_0_12 = 0 % 11.70/3.29 | % 11.70/3.29 | Instantiating (69) with all_27_0_18, all_27_1_19, all_27_2_20 yields: % 11.70/3.29 | (95) line(all_27_1_19) = all_27_0_18 & line_connecting(all_1_0_0, all_1_0_0) = all_27_1_19 & distinct_points(all_1_0_0, all_1_0_0) = all_27_2_20 & ( ~ (all_27_2_20 = 0) | all_27_0_18 = 0) % 11.70/3.29 | % 11.70/3.29 | Applying alpha-rule on (95) yields: % 11.70/3.29 | (96) line(all_27_1_19) = all_27_0_18 % 11.70/3.29 | (97) line_connecting(all_1_0_0, all_1_0_0) = all_27_1_19 % 11.70/3.29 | (98) distinct_points(all_1_0_0, all_1_0_0) = all_27_2_20 % 11.70/3.29 | (99) ~ (all_27_2_20 = 0) | all_27_0_18 = 0 % 11.70/3.29 | % 11.70/3.29 | Instantiating formula (3) with all_1_1_1, all_1_0_0, all_21_1_10, all_23_2_14 and discharging atoms line_connecting(all_1_1_1, all_1_0_0) = all_23_2_14, line_connecting(all_1_1_1, all_1_0_0) = all_21_1_10, yields: % 11.70/3.29 | (100) all_23_2_14 = all_21_1_10 % 11.70/3.29 | % 11.70/3.29 | Instantiating formula (3) with all_1_1_1, all_1_0_0, all_17_1_3, all_23_2_14 and discharging atoms line_connecting(all_1_1_1, all_1_0_0) = all_23_2_14, line_connecting(all_1_1_1, all_1_0_0) = all_17_1_3, yields: % 11.70/3.29 | (101) all_23_2_14 = all_17_1_3 % 11.70/3.29 | % 11.70/3.29 | Instantiating formula (57) with all_1_0_0 yields: % 11.70/3.29 | (102) ~ (distinct_points(all_1_0_0, all_1_0_0) = 0) % 11.70/3.29 | % 11.70/3.29 | Instantiating formula (30) with all_1_1_1, all_1_0_0, all_21_2_11, 0 and discharging atoms distinct_points(all_1_1_1, all_1_0_0) = all_21_2_11, distinct_points(all_1_1_1, all_1_0_0) = 0, yields: % 11.70/3.29 | (103) all_21_2_11 = 0 % 11.70/3.29 | % 11.70/3.29 | Using (93) and (68) yields: % 11.70/3.29 | (104) ~ (all_23_0_12 = 0) % 11.70/3.29 | % 11.70/3.29 | Instantiating formula (30) with all_1_1_1, all_1_1_1, all_19_2_8, all_23_0_12 and discharging atoms distinct_points(all_1_1_1, all_1_1_1) = all_23_0_12, distinct_points(all_1_1_1, all_1_1_1) = all_19_2_8, yields: % 11.70/3.29 | (105) all_23_0_12 = all_19_2_8 % 11.70/3.29 | % 11.70/3.29 | Combining equations (100,101) yields a new equation: % 11.70/3.29 | (106) all_21_1_10 = all_17_1_3 % 11.70/3.29 | % 11.70/3.29 | Simplifying 106 yields: % 11.70/3.29 | (107) all_21_1_10 = all_17_1_3 % 11.70/3.29 | % 11.70/3.29 | Equations (105) can reduce 104 to: % 11.70/3.29 | (108) ~ (all_19_2_8 = 0) % 11.70/3.29 | % 11.70/3.29 | From (107) and (87) follows: % 11.70/3.29 | (76) line_connecting(all_1_1_1, all_1_0_0) = all_17_1_3 % 11.70/3.29 | % 11.70/3.29 | From (101) and (92) follows: % 11.70/3.29 | (110) apart_point_and_line(all_1_1_1, all_17_1_3) = all_23_1_13 % 11.70/3.29 | % 11.70/3.29 | From (103) and (88) follows: % 11.70/3.29 | (62) distinct_points(all_1_1_1, all_1_0_0) = 0 % 11.70/3.29 | % 11.70/3.29 +-Applying beta-rule and splitting (94), into two cases. % 11.70/3.29 |-Branch one: % 11.70/3.29 | (112) ~ (all_23_1_13 = 0) % 11.70/3.29 | % 11.70/3.29 | Using (98) and (102) yields: % 11.70/3.29 | (113) ~ (all_27_2_20 = 0) % 11.70/3.29 | % 11.70/3.29 | Instantiating formula (12) with all_23_1_13, all_23_1_13, all_17_1_3, all_17_1_3, all_1_0_0, all_1_1_1 and discharging atoms apart_point_and_line(all_1_1_1, all_17_1_3) = all_23_1_13, distinct_points(all_1_1_1, all_1_0_0) = 0, yields: % 11.70/3.29 | (114) all_23_1_13 = 0 | ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_17_1_3) = v2 & apart_point_and_line(all_1_0_0, all_17_1_3) = v1 & distinct_lines(all_17_1_3, all_17_1_3) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 11.70/3.29 | % 11.70/3.29 | Instantiating formula (63) with all_23_1_13, all_17_1_3 and discharging atoms apart_point_and_line(all_1_1_1, all_17_1_3) = all_23_1_13, yields: % 11.70/3.29 | (115) all_23_1_13 = 0 | apart_point_and_line(all_1_0_0, all_17_1_3) = 0 % 11.70/3.29 | % 11.70/3.29 | Instantiating formula (2) with all_27_2_20, all_1_0_0, all_1_0_0, all_1_1_1 and discharging atoms distinct_points(all_1_0_0, all_1_0_0) = all_27_2_20, distinct_points(all_1_1_1, all_1_0_0) = 0, yields: % 11.70/3.29 | (116) ? [v0] : ? [v1] : ? [v2] : (line_connecting(all_1_1_1, all_1_0_0) = v0 & apart_point_and_line(all_1_0_0, v0) = v1 & distinct_points(all_1_0_0, all_1_1_1) = v2 & ( ~ (v1 = 0) | (v2 = 0 & all_27_2_20 = 0))) % 11.70/3.29 | % 11.70/3.29 | Instantiating (116) with all_48_0_24, all_48_1_25, all_48_2_26 yields: % 11.70/3.29 | (117) line_connecting(all_1_1_1, all_1_0_0) = all_48_2_26 & apart_point_and_line(all_1_0_0, all_48_2_26) = all_48_1_25 & distinct_points(all_1_0_0, all_1_1_1) = all_48_0_24 & ( ~ (all_48_1_25 = 0) | (all_48_0_24 = 0 & all_27_2_20 = 0)) % 11.70/3.29 | % 11.70/3.29 | Applying alpha-rule on (117) yields: % 11.70/3.29 | (118) line_connecting(all_1_1_1, all_1_0_0) = all_48_2_26 % 11.70/3.30 | (119) apart_point_and_line(all_1_0_0, all_48_2_26) = all_48_1_25 % 11.70/3.30 | (120) distinct_points(all_1_0_0, all_1_1_1) = all_48_0_24 % 11.70/3.30 | (121) ~ (all_48_1_25 = 0) | (all_48_0_24 = 0 & all_27_2_20 = 0) % 11.70/3.30 | % 11.70/3.30 +-Applying beta-rule and splitting (121), into two cases. % 11.70/3.30 |-Branch one: % 11.70/3.30 | (122) ~ (all_48_1_25 = 0) % 11.70/3.30 | % 11.70/3.30 +-Applying beta-rule and splitting (114), into two cases. % 11.70/3.30 |-Branch one: % 11.70/3.30 | (123) all_23_1_13 = 0 % 11.70/3.30 | % 11.70/3.31 | Equations (123) can reduce 112 to: % 11.70/3.31 | (124) $false % 11.70/3.31 | % 11.70/3.31 |-The branch is then unsatisfiable % 11.70/3.31 |-Branch two: % 11.70/3.31 | (112) ~ (all_23_1_13 = 0) % 11.70/3.31 | (126) ? [v0] : ? [v1] : ? [v2] : (apart_point_and_line(all_1_0_0, all_17_1_3) = v2 & apart_point_and_line(all_1_0_0, all_17_1_3) = v1 & distinct_lines(all_17_1_3, all_17_1_3) = v0 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 11.70/3.31 | % 11.70/3.31 +-Applying beta-rule and splitting (115), into two cases. % 11.70/3.31 |-Branch one: % 11.70/3.31 | (127) apart_point_and_line(all_1_0_0, all_17_1_3) = 0 % 11.70/3.31 | % 11.70/3.31 | Instantiating formula (3) with all_1_1_1, all_1_0_0, all_48_2_26, all_17_1_3 and discharging atoms line_connecting(all_1_1_1, all_1_0_0) = all_48_2_26, line_connecting(all_1_1_1, all_1_0_0) = all_17_1_3, yields: % 11.70/3.31 | (128) all_48_2_26 = all_17_1_3 % 11.70/3.31 | % 11.70/3.31 | Instantiating formula (33) with all_1_0_0, all_17_1_3, 0, all_48_1_25 and discharging atoms apart_point_and_line(all_1_0_0, all_17_1_3) = 0, yields: % 11.70/3.31 | (129) all_48_1_25 = 0 | ~ (apart_point_and_line(all_1_0_0, all_17_1_3) = all_48_1_25) % 11.70/3.31 | % 11.70/3.31 | From (128) and (119) follows: % 11.70/3.31 | (130) apart_point_and_line(all_1_0_0, all_17_1_3) = all_48_1_25 % 11.70/3.31 | % 11.70/3.31 +-Applying beta-rule and splitting (129), into two cases. % 11.70/3.31 |-Branch one: % 11.70/3.31 | (131) ~ (apart_point_and_line(all_1_0_0, all_17_1_3) = all_48_1_25) % 11.70/3.31 | % 11.70/3.31 | Using (130) and (131) yields: % 11.70/3.31 | (132) $false % 11.70/3.31 | % 11.70/3.31 |-The branch is then unsatisfiable % 11.70/3.31 |-Branch two: % 11.70/3.31 | (130) apart_point_and_line(all_1_0_0, all_17_1_3) = all_48_1_25 % 11.70/3.31 | (134) all_48_1_25 = 0 % 11.70/3.31 | % 11.70/3.31 | Equations (134) can reduce 122 to: % 11.70/3.31 | (124) $false % 11.70/3.31 | % 11.70/3.31 |-The branch is then unsatisfiable % 11.70/3.31 |-Branch two: % 11.70/3.31 | (136) ~ (apart_point_and_line(all_1_0_0, all_17_1_3) = 0) % 11.70/3.31 | (123) all_23_1_13 = 0 % 11.70/3.31 | % 11.70/3.31 | Equations (123) can reduce 112 to: % 11.70/3.31 | (124) $false % 11.70/3.31 | % 11.70/3.31 |-The branch is then unsatisfiable % 11.70/3.31 |-Branch two: % 11.70/3.31 | (134) all_48_1_25 = 0 % 11.70/3.31 | (140) all_48_0_24 = 0 & all_27_2_20 = 0 % 11.70/3.31 | % 11.70/3.31 | Applying alpha-rule on (140) yields: % 11.70/3.31 | (141) all_48_0_24 = 0 % 11.70/3.31 | (142) all_27_2_20 = 0 % 11.70/3.31 | % 11.70/3.31 | Equations (142) can reduce 113 to: % 11.70/3.31 | (124) $false % 11.70/3.31 | % 11.70/3.31 |-The branch is then unsatisfiable % 11.70/3.31 |-Branch two: % 11.70/3.31 | (123) all_23_1_13 = 0 % 11.70/3.31 | (145) all_23_0_12 = 0 % 11.70/3.31 | % 11.70/3.31 | Combining equations (145,105) yields a new equation: % 11.70/3.31 | (146) all_19_2_8 = 0 % 11.70/3.31 | % 11.70/3.31 | Equations (146) can reduce 108 to: % 11.70/3.31 | (124) $false % 11.70/3.31 | % 11.70/3.31 |-The branch is then unsatisfiable % 11.70/3.31 % SZS output end Proof for theBenchmark % 11.70/3.31 % 11.70/3.31 2725ms %------------------------------------------------------------------------------