%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : TOP022+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n028.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 : Thu Jul 21 21:24:38 EDT 2022 % Result : Theorem 3.39s 1.51s % Output : Proof 4.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : TOP022+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n028.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 : Sun May 29 08:41:03 EDT 2022 % 0.12/0.33 % CPUTime : % 0.56/0.57 ____ _ % 0.56/0.57 ___ / __ \_____(_)___ ________ __________ % 0.56/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.56/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.56/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.56/0.57 % 0.56/0.57 A Theorem Prover for First-Order Logic % 0.56/0.57 (ePrincess v.1.0) % 0.56/0.57 % 0.56/0.57 (c) Philipp Rümmer, 2009-2015 % 0.56/0.57 (c) Peter Backeman, 2014-2015 % 0.56/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.56/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.56/0.57 Bug reports to peter@backeman.se % 0.56/0.57 % 0.56/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.56/0.57 % 0.56/0.57 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.56/0.62 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.31/0.89 Prover 0: Preprocessing ... % 1.53/1.00 Prover 0: Warning: ignoring some quantifiers % 1.53/1.02 Prover 0: Constructing countermodel ... % 2.14/1.18 Prover 0: gave up % 2.14/1.18 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.24/1.19 Prover 1: Preprocessing ... % 2.46/1.27 Prover 1: Constructing countermodel ... % 2.94/1.38 Prover 1: gave up % 2.94/1.38 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.94/1.39 Prover 2: Preprocessing ... % 2.94/1.44 Prover 2: Warning: ignoring some quantifiers % 2.94/1.44 Prover 2: Constructing countermodel ... % 3.39/1.50 Prover 2: proved (128ms) % 3.39/1.51 % 3.39/1.51 No countermodel exists, formula is valid % 3.39/1.51 % SZS status Theorem for theBenchmark % 3.39/1.51 % 3.39/1.51 Generating proof ... Warning: ignoring some quantifiers % 4.65/1.77 found it (size 65) % 4.65/1.77 % 4.65/1.77 % SZS output start Proof for theBenchmark % 4.65/1.77 Assumed formulas after preprocessing and simplification: % 4.65/1.77 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = 0) & first_homotop_grp(v0, v2) = v4 & first_homotop_grp(v0, v1) = v3 & a_member_of(v2, v0) = 0 & a_member_of(v1, v0) = 0 & path_connected(v0) = 0 & isomorphic_groups(v3, v4) = v5 & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v13 = 0 | ~ (alpha_hat(v6) = v10) | ~ (first_homotop_grp(v9, v8) = v12) | ~ (first_homotop_grp(v9, v7) = v11) | ~ (a_group_isomorphism_from_to(v10, v11, v12) = v13) | ? [v14] : ( ~ (v14 = 0) & a_path_from_to_in(v6, v7, v8, v9) = v14)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v7 = v6 | ~ (a_path_from_to_in(v11, v10, v9, v8) = v7) | ~ (a_path_from_to_in(v11, v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (a_member_of(v8, v6) = v10) | ~ (a_member_of(v7, v6) = v9) | ~ (a_path_from_to_in(v11, v7, v8, v6) = 0) | path_connected(v6) = 0) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (a_member_of(v8, v6) = v10) | ~ (a_member_of(v7, v6) = v9) | path_connected(v6) = 0) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v9 = 0 | ~ (a_member_of(v8, v6) = v10) | ~ (a_member_of(v7, v6) = v9) | path_connected(v6) = 0) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ! [v10] : (v7 = v6 | ~ (a_group_isomorphism_from_to(v10, v9, v8) = v7) | ~ (a_group_isomorphism_from_to(v10, v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v8 = 0 | ~ (isomorphic_groups(v6, v7) = v8) | ~ (a_group_isomorphism_from_to(v9, v6, v7) = 0)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (first_homotop_grp(v9, v8) = v7) | ~ (first_homotop_grp(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (a_member_of(v9, v8) = v7) | ~ (a_member_of(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : (v7 = v6 | ~ (isomorphic_groups(v9, v8) = v7) | ~ (isomorphic_groups(v9, v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ! [v9] : ( ~ (a_path_from_to_in(v6, v7, v8, v9) = 0) | ? [v10] : ? [v11] : ? [v12] : (alpha_hat(v6) = v10 & first_homotop_grp(v9, v8) = v12 & first_homotop_grp(v9, v7) = v11 & a_group_isomorphism_from_to(v10, v11, v12) = 0)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (alpha_hat(v8) = v7) | ~ (alpha_hat(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : (v7 = v6 | ~ (path_connected(v8) = v7) | ~ (path_connected(v8) = v6)) & ! [v6] : ! [v7] : ! [v8] : ( ~ (a_member_of(v8, v6) = 0) | ~ (a_member_of(v7, v6) = 0) | ? [v9] : ? [v10] : ((v10 = 0 & a_path_from_to_in(v9, v7, v8, v6) = 0) | ( ~ (v9 = 0) & path_connected(v6) = v9))) & ! [v6] : ! [v7] : ( ~ (isomorphic_groups(v6, v7) = 0) | ? [v8] : a_group_isomorphism_from_to(v8, v6, v7) = 0) & ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : a_path_from_to_in(v9, v8, v7, v6) = v10 & ? [v6] : ? [v7] : ? [v8] : ? [v9] : a_group_isomorphism_from_to(v8, v7, v6) = v9 & ? [v6] : ? [v7] : ? [v8] : first_homotop_grp(v7, v6) = v8 & ? [v6] : ? [v7] : ? [v8] : a_member_of(v7, v6) = v8 & ? [v6] : ? [v7] : ? [v8] : isomorphic_groups(v7, v6) = v8 & ? [v6] : ? [v7] : alpha_hat(v6) = v7 & ? [v6] : ? [v7] : path_connected(v6) = v7) % 4.75/1.81 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5 yields: % 4.75/1.81 | (1) ~ (all_0_0_0 = 0) & first_homotop_grp(all_0_5_5, all_0_3_3) = all_0_1_1 & first_homotop_grp(all_0_5_5, all_0_4_4) = all_0_2_2 & a_member_of(all_0_3_3, all_0_5_5) = 0 & a_member_of(all_0_4_4, all_0_5_5) = 0 & path_connected(all_0_5_5) = 0 & isomorphic_groups(all_0_2_2, all_0_1_1) = all_0_0_0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (alpha_hat(v0) = v4) | ~ (first_homotop_grp(v3, v2) = v6) | ~ (first_homotop_grp(v3, v1) = v5) | ~ (a_group_isomorphism_from_to(v4, v5, v6) = v7) | ? [v8] : ( ~ (v8 = 0) & a_path_from_to_in(v0, v1, v2, v3) = v8)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = v0 | ~ (a_path_from_to_in(v5, v4, v3, v2) = v1) | ~ (a_path_from_to_in(v5, v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (a_member_of(v2, v0) = v4) | ~ (a_member_of(v1, v0) = v3) | ~ (a_path_from_to_in(v5, v1, v2, v0) = 0) | path_connected(v0) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (a_member_of(v2, v0) = v4) | ~ (a_member_of(v1, v0) = v3) | path_connected(v0) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = 0 | ~ (a_member_of(v2, v0) = v4) | ~ (a_member_of(v1, v0) = v3) | path_connected(v0) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (a_group_isomorphism_from_to(v4, v3, v2) = v1) | ~ (a_group_isomorphism_from_to(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (isomorphic_groups(v0, v1) = v2) | ~ (a_group_isomorphism_from_to(v3, v0, v1) = 0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (first_homotop_grp(v3, v2) = v1) | ~ (first_homotop_grp(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a_member_of(v3, v2) = v1) | ~ (a_member_of(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (isomorphic_groups(v3, v2) = v1) | ~ (isomorphic_groups(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (a_path_from_to_in(v0, v1, v2, v3) = 0) | ? [v4] : ? [v5] : ? [v6] : (alpha_hat(v0) = v4 & first_homotop_grp(v3, v2) = v6 & first_homotop_grp(v3, v1) = v5 & a_group_isomorphism_from_to(v4, v5, v6) = 0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (alpha_hat(v2) = v1) | ~ (alpha_hat(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (path_connected(v2) = v1) | ~ (path_connected(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (a_member_of(v2, v0) = 0) | ~ (a_member_of(v1, v0) = 0) | ? [v3] : ? [v4] : ((v4 = 0 & a_path_from_to_in(v3, v1, v2, v0) = 0) | ( ~ (v3 = 0) & path_connected(v0) = v3))) & ! [v0] : ! [v1] : ( ~ (isomorphic_groups(v0, v1) = 0) | ? [v2] : a_group_isomorphism_from_to(v2, v0, v1) = 0) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : a_path_from_to_in(v3, v2, v1, v0) = v4 & ? [v0] : ? [v1] : ? [v2] : ? [v3] : a_group_isomorphism_from_to(v2, v1, v0) = v3 & ? [v0] : ? [v1] : ? [v2] : first_homotop_grp(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : a_member_of(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : isomorphic_groups(v1, v0) = v2 & ? [v0] : ? [v1] : alpha_hat(v0) = v1 & ? [v0] : ? [v1] : path_connected(v0) = v1 % 4.75/1.81 | % 4.75/1.81 | Applying alpha-rule on (1) yields: % 4.75/1.81 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = 0 | ~ (isomorphic_groups(v0, v1) = v2) | ~ (a_group_isomorphism_from_to(v3, v0, v1) = 0)) % 4.75/1.81 | (3) ? [v0] : ? [v1] : path_connected(v0) = v1 % 4.75/1.81 | (4) ~ (all_0_0_0 = 0) % 4.75/1.81 | (5) first_homotop_grp(all_0_5_5, all_0_4_4) = all_0_2_2 % 4.75/1.82 | (6) ? [v0] : ? [v1] : ? [v2] : a_member_of(v1, v0) = v2 % 4.75/1.82 | (7) ? [v0] : ? [v1] : ? [v2] : ? [v3] : a_group_isomorphism_from_to(v2, v1, v0) = v3 % 4.75/1.82 | (8) isomorphic_groups(all_0_2_2, all_0_1_1) = all_0_0_0 % 4.75/1.82 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (a_member_of(v2, v0) = v4) | ~ (a_member_of(v1, v0) = v3) | path_connected(v0) = 0) % 4.75/1.82 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (path_connected(v2) = v1) | ~ (path_connected(v2) = v0)) % 4.75/1.82 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v3 = 0 | ~ (a_member_of(v2, v0) = v4) | ~ (a_member_of(v1, v0) = v3) | path_connected(v0) = 0) % 4.75/1.82 | (12) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : a_path_from_to_in(v3, v2, v1, v0) = v4 % 4.75/1.82 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (a_group_isomorphism_from_to(v4, v3, v2) = v1) | ~ (a_group_isomorphism_from_to(v4, v3, v2) = v0)) % 4.91/1.82 | (14) ! [v0] : ! [v1] : ! [v2] : ( ~ (a_member_of(v2, v0) = 0) | ~ (a_member_of(v1, v0) = 0) | ? [v3] : ? [v4] : ((v4 = 0 & a_path_from_to_in(v3, v1, v2, v0) = 0) | ( ~ (v3 = 0) & path_connected(v0) = v3))) % 4.91/1.82 | (15) ! [v0] : ! [v1] : ( ~ (isomorphic_groups(v0, v1) = 0) | ? [v2] : a_group_isomorphism_from_to(v2, v0, v1) = 0) % 4.91/1.82 | (16) ? [v0] : ? [v1] : ? [v2] : first_homotop_grp(v1, v0) = v2 % 4.91/1.82 | (17) a_member_of(all_0_3_3, all_0_5_5) = 0 % 4.91/1.82 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (alpha_hat(v0) = v4) | ~ (first_homotop_grp(v3, v2) = v6) | ~ (first_homotop_grp(v3, v1) = v5) | ~ (a_group_isomorphism_from_to(v4, v5, v6) = v7) | ? [v8] : ( ~ (v8 = 0) & a_path_from_to_in(v0, v1, v2, v3) = v8)) % 4.91/1.82 | (19) a_member_of(all_0_4_4, all_0_5_5) = 0 % 4.91/1.82 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (a_member_of(v3, v2) = v1) | ~ (a_member_of(v3, v2) = v0)) % 4.91/1.82 | (21) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (a_member_of(v2, v0) = v4) | ~ (a_member_of(v1, v0) = v3) | ~ (a_path_from_to_in(v5, v1, v2, v0) = 0) | path_connected(v0) = 0) % 4.91/1.82 | (22) ? [v0] : ? [v1] : ? [v2] : isomorphic_groups(v1, v0) = v2 % 4.91/1.82 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = v0 | ~ (a_path_from_to_in(v5, v4, v3, v2) = v1) | ~ (a_path_from_to_in(v5, v4, v3, v2) = v0)) % 4.91/1.82 | (24) ? [v0] : ? [v1] : alpha_hat(v0) = v1 % 4.91/1.82 | (25) first_homotop_grp(all_0_5_5, all_0_3_3) = all_0_1_1 % 4.91/1.82 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (a_path_from_to_in(v0, v1, v2, v3) = 0) | ? [v4] : ? [v5] : ? [v6] : (alpha_hat(v0) = v4 & first_homotop_grp(v3, v2) = v6 & first_homotop_grp(v3, v1) = v5 & a_group_isomorphism_from_to(v4, v5, v6) = 0)) % 4.91/1.82 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (first_homotop_grp(v3, v2) = v1) | ~ (first_homotop_grp(v3, v2) = v0)) % 4.91/1.82 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (isomorphic_groups(v3, v2) = v1) | ~ (isomorphic_groups(v3, v2) = v0)) % 4.91/1.82 | (29) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (alpha_hat(v2) = v1) | ~ (alpha_hat(v2) = v0)) % 4.91/1.82 | (30) path_connected(all_0_5_5) = 0 % 4.91/1.82 | % 4.91/1.82 | Instantiating formula (14) with all_0_3_3, all_0_3_3, all_0_5_5 and discharging atoms a_member_of(all_0_3_3, all_0_5_5) = 0, yields: % 4.91/1.83 | (31) ? [v0] : ? [v1] : ((v1 = 0 & a_path_from_to_in(v0, all_0_3_3, all_0_3_3, all_0_5_5) = 0) | ( ~ (v0 = 0) & path_connected(all_0_5_5) = v0)) % 4.91/1.83 | % 4.91/1.83 | Instantiating formula (14) with all_0_4_4, all_0_3_3, all_0_5_5 and discharging atoms a_member_of(all_0_3_3, all_0_5_5) = 0, a_member_of(all_0_4_4, all_0_5_5) = 0, yields: % 4.91/1.83 | (32) ? [v0] : ? [v1] : ((v1 = 0 & a_path_from_to_in(v0, all_0_3_3, all_0_4_4, all_0_5_5) = 0) | ( ~ (v0 = 0) & path_connected(all_0_5_5) = v0)) % 4.91/1.83 | % 4.91/1.83 | Instantiating formula (14) with all_0_3_3, all_0_4_4, all_0_5_5 and discharging atoms a_member_of(all_0_3_3, all_0_5_5) = 0, a_member_of(all_0_4_4, all_0_5_5) = 0, yields: % 4.91/1.83 | (33) ? [v0] : ? [v1] : ((v1 = 0 & a_path_from_to_in(v0, all_0_4_4, all_0_3_3, all_0_5_5) = 0) | ( ~ (v0 = 0) & path_connected(all_0_5_5) = v0)) % 4.91/1.83 | % 4.91/1.83 | Instantiating formula (14) with all_0_4_4, all_0_4_4, all_0_5_5 and discharging atoms a_member_of(all_0_4_4, all_0_5_5) = 0, yields: % 4.91/1.83 | (34) ? [v0] : ? [v1] : ((v1 = 0 & a_path_from_to_in(v0, all_0_4_4, all_0_4_4, all_0_5_5) = 0) | ( ~ (v0 = 0) & path_connected(all_0_5_5) = v0)) % 4.91/1.83 | % 4.91/1.83 | Instantiating (34) with all_22_0_28, all_22_1_29 yields: % 4.91/1.83 | (35) (all_22_0_28 = 0 & a_path_from_to_in(all_22_1_29, all_0_4_4, all_0_4_4, all_0_5_5) = 0) | ( ~ (all_22_1_29 = 0) & path_connected(all_0_5_5) = all_22_1_29) % 4.91/1.83 | % 4.91/1.83 | Instantiating (32) with all_23_0_30, all_23_1_31 yields: % 4.91/1.83 | (36) (all_23_0_30 = 0 & a_path_from_to_in(all_23_1_31, all_0_3_3, all_0_4_4, all_0_5_5) = 0) | ( ~ (all_23_1_31 = 0) & path_connected(all_0_5_5) = all_23_1_31) % 4.91/1.83 | % 4.91/1.83 | Instantiating (31) with all_24_0_32, all_24_1_33 yields: % 4.91/1.83 | (37) (all_24_0_32 = 0 & a_path_from_to_in(all_24_1_33, all_0_3_3, all_0_3_3, all_0_5_5) = 0) | ( ~ (all_24_1_33 = 0) & path_connected(all_0_5_5) = all_24_1_33) % 4.91/1.83 | % 4.91/1.83 | Instantiating (33) with all_25_0_34, all_25_1_35 yields: % 4.91/1.83 | (38) (all_25_0_34 = 0 & a_path_from_to_in(all_25_1_35, all_0_4_4, all_0_3_3, all_0_5_5) = 0) | ( ~ (all_25_1_35 = 0) & path_connected(all_0_5_5) = all_25_1_35) % 4.91/1.83 | % 4.91/1.83 +-Applying beta-rule and splitting (35), into two cases. % 4.91/1.83 |-Branch one: % 4.91/1.83 | (39) all_22_0_28 = 0 & a_path_from_to_in(all_22_1_29, all_0_4_4, all_0_4_4, all_0_5_5) = 0 % 4.91/1.83 | % 4.91/1.83 | Applying alpha-rule on (39) yields: % 4.91/1.83 | (40) all_22_0_28 = 0 % 4.91/1.83 | (41) a_path_from_to_in(all_22_1_29, all_0_4_4, all_0_4_4, all_0_5_5) = 0 % 4.91/1.83 | % 4.91/1.83 +-Applying beta-rule and splitting (36), into two cases. % 4.91/1.83 |-Branch one: % 4.91/1.83 | (42) all_23_0_30 = 0 & a_path_from_to_in(all_23_1_31, all_0_3_3, all_0_4_4, all_0_5_5) = 0 % 4.97/1.83 | % 4.97/1.83 | Applying alpha-rule on (42) yields: % 4.97/1.83 | (43) all_23_0_30 = 0 % 4.97/1.83 | (44) a_path_from_to_in(all_23_1_31, all_0_3_3, all_0_4_4, all_0_5_5) = 0 % 4.97/1.83 | % 4.97/1.83 +-Applying beta-rule and splitting (37), into two cases. % 4.97/1.83 |-Branch one: % 4.97/1.83 | (45) all_24_0_32 = 0 & a_path_from_to_in(all_24_1_33, all_0_3_3, all_0_3_3, all_0_5_5) = 0 % 4.97/1.83 | % 4.97/1.83 | Applying alpha-rule on (45) yields: % 4.97/1.83 | (46) all_24_0_32 = 0 % 4.97/1.83 | (47) a_path_from_to_in(all_24_1_33, all_0_3_3, all_0_3_3, all_0_5_5) = 0 % 4.97/1.83 | % 4.97/1.83 +-Applying beta-rule and splitting (38), into two cases. % 4.97/1.83 |-Branch one: % 4.97/1.83 | (48) all_25_0_34 = 0 & a_path_from_to_in(all_25_1_35, all_0_4_4, all_0_3_3, all_0_5_5) = 0 % 4.97/1.83 | % 4.97/1.83 | Applying alpha-rule on (48) yields: % 4.97/1.83 | (49) all_25_0_34 = 0 % 4.97/1.83 | (50) a_path_from_to_in(all_25_1_35, all_0_4_4, all_0_3_3, all_0_5_5) = 0 % 4.97/1.83 | % 4.97/1.83 | Instantiating formula (26) with all_0_5_5, all_0_3_3, all_0_4_4, all_25_1_35 and discharging atoms a_path_from_to_in(all_25_1_35, all_0_4_4, all_0_3_3, all_0_5_5) = 0, yields: % 4.97/1.83 | (51) ? [v0] : ? [v1] : ? [v2] : (alpha_hat(all_25_1_35) = v0 & first_homotop_grp(all_0_5_5, all_0_3_3) = v2 & first_homotop_grp(all_0_5_5, all_0_4_4) = v1 & a_group_isomorphism_from_to(v0, v1, v2) = 0) % 4.97/1.83 | % 4.97/1.83 | Instantiating formula (26) with all_0_5_5, all_0_3_3, all_0_3_3, all_24_1_33 and discharging atoms a_path_from_to_in(all_24_1_33, all_0_3_3, all_0_3_3, all_0_5_5) = 0, yields: % 4.97/1.83 | (52) ? [v0] : ? [v1] : ? [v2] : (alpha_hat(all_24_1_33) = v0 & first_homotop_grp(all_0_5_5, all_0_3_3) = v2 & first_homotop_grp(all_0_5_5, all_0_3_3) = v1 & a_group_isomorphism_from_to(v0, v1, v2) = 0) % 4.97/1.83 | % 4.97/1.83 | Instantiating formula (26) with all_0_5_5, all_0_4_4, all_0_3_3, all_23_1_31 and discharging atoms a_path_from_to_in(all_23_1_31, all_0_3_3, all_0_4_4, all_0_5_5) = 0, yields: % 4.97/1.84 | (53) ? [v0] : ? [v1] : ? [v2] : (alpha_hat(all_23_1_31) = v0 & first_homotop_grp(all_0_5_5, all_0_3_3) = v1 & first_homotop_grp(all_0_5_5, all_0_4_4) = v2 & a_group_isomorphism_from_to(v0, v1, v2) = 0) % 4.97/1.84 | % 4.97/1.84 | Instantiating formula (26) with all_0_5_5, all_0_4_4, all_0_4_4, all_22_1_29 and discharging atoms a_path_from_to_in(all_22_1_29, all_0_4_4, all_0_4_4, all_0_5_5) = 0, yields: % 4.97/1.84 | (54) ? [v0] : ? [v1] : ? [v2] : (alpha_hat(all_22_1_29) = v0 & first_homotop_grp(all_0_5_5, all_0_4_4) = v2 & first_homotop_grp(all_0_5_5, all_0_4_4) = v1 & a_group_isomorphism_from_to(v0, v1, v2) = 0) % 4.97/1.84 | % 4.97/1.84 | Instantiating (54) with all_45_0_36, all_45_1_37, all_45_2_38 yields: % 4.97/1.84 | (55) alpha_hat(all_22_1_29) = all_45_2_38 & first_homotop_grp(all_0_5_5, all_0_4_4) = all_45_0_36 & first_homotop_grp(all_0_5_5, all_0_4_4) = all_45_1_37 & a_group_isomorphism_from_to(all_45_2_38, all_45_1_37, all_45_0_36) = 0 % 4.97/1.84 | % 4.97/1.84 | Applying alpha-rule on (55) yields: % 4.97/1.84 | (56) alpha_hat(all_22_1_29) = all_45_2_38 % 4.97/1.84 | (57) first_homotop_grp(all_0_5_5, all_0_4_4) = all_45_0_36 % 4.97/1.84 | (58) first_homotop_grp(all_0_5_5, all_0_4_4) = all_45_1_37 % 4.97/1.84 | (59) a_group_isomorphism_from_to(all_45_2_38, all_45_1_37, all_45_0_36) = 0 % 4.97/1.84 | % 4.97/1.84 | Instantiating (52) with all_47_0_39, all_47_1_40, all_47_2_41 yields: % 4.97/1.84 | (60) alpha_hat(all_24_1_33) = all_47_2_41 & first_homotop_grp(all_0_5_5, all_0_3_3) = all_47_0_39 & first_homotop_grp(all_0_5_5, all_0_3_3) = all_47_1_40 & a_group_isomorphism_from_to(all_47_2_41, all_47_1_40, all_47_0_39) = 0 % 4.97/1.84 | % 4.97/1.84 | Applying alpha-rule on (60) yields: % 4.97/1.84 | (61) alpha_hat(all_24_1_33) = all_47_2_41 % 4.97/1.84 | (62) first_homotop_grp(all_0_5_5, all_0_3_3) = all_47_0_39 % 4.97/1.84 | (63) first_homotop_grp(all_0_5_5, all_0_3_3) = all_47_1_40 % 4.97/1.84 | (64) a_group_isomorphism_from_to(all_47_2_41, all_47_1_40, all_47_0_39) = 0 % 4.97/1.84 | % 4.97/1.84 | Instantiating (51) with all_49_0_42, all_49_1_43, all_49_2_44 yields: % 4.97/1.84 | (65) alpha_hat(all_25_1_35) = all_49_2_44 & first_homotop_grp(all_0_5_5, all_0_3_3) = all_49_0_42 & first_homotop_grp(all_0_5_5, all_0_4_4) = all_49_1_43 & a_group_isomorphism_from_to(all_49_2_44, all_49_1_43, all_49_0_42) = 0 % 4.97/1.84 | % 4.97/1.84 | Applying alpha-rule on (65) yields: % 4.97/1.84 | (66) alpha_hat(all_25_1_35) = all_49_2_44 % 4.97/1.84 | (67) first_homotop_grp(all_0_5_5, all_0_3_3) = all_49_0_42 % 4.97/1.84 | (68) first_homotop_grp(all_0_5_5, all_0_4_4) = all_49_1_43 % 4.97/1.84 | (69) a_group_isomorphism_from_to(all_49_2_44, all_49_1_43, all_49_0_42) = 0 % 4.97/1.84 | % 4.97/1.84 | Instantiating (53) with all_51_0_45, all_51_1_46, all_51_2_47 yields: % 4.97/1.84 | (70) alpha_hat(all_23_1_31) = all_51_2_47 & first_homotop_grp(all_0_5_5, all_0_3_3) = all_51_1_46 & first_homotop_grp(all_0_5_5, all_0_4_4) = all_51_0_45 & a_group_isomorphism_from_to(all_51_2_47, all_51_1_46, all_51_0_45) = 0 % 4.97/1.84 | % 4.97/1.84 | Applying alpha-rule on (70) yields: % 4.97/1.84 | (71) alpha_hat(all_23_1_31) = all_51_2_47 % 4.97/1.84 | (72) first_homotop_grp(all_0_5_5, all_0_3_3) = all_51_1_46 % 4.97/1.84 | (73) first_homotop_grp(all_0_5_5, all_0_4_4) = all_51_0_45 % 4.97/1.84 | (74) a_group_isomorphism_from_to(all_51_2_47, all_51_1_46, all_51_0_45) = 0 % 4.97/1.84 | % 4.97/1.84 | Instantiating formula (27) with all_0_5_5, all_0_3_3, all_49_0_42, all_0_1_1 and discharging atoms first_homotop_grp(all_0_5_5, all_0_3_3) = all_49_0_42, first_homotop_grp(all_0_5_5, all_0_3_3) = all_0_1_1, yields: % 4.97/1.84 | (75) all_49_0_42 = all_0_1_1 % 4.97/1.84 | % 4.97/1.84 | Instantiating formula (27) with all_0_5_5, all_0_3_3, all_47_0_39, all_49_0_42 and discharging atoms first_homotop_grp(all_0_5_5, all_0_3_3) = all_49_0_42, first_homotop_grp(all_0_5_5, all_0_3_3) = all_47_0_39, yields: % 4.97/1.84 | (76) all_49_0_42 = all_47_0_39 % 4.97/1.84 | % 4.97/1.84 | Instantiating formula (27) with all_0_5_5, all_0_4_4, all_49_1_43, all_0_2_2 and discharging atoms first_homotop_grp(all_0_5_5, all_0_4_4) = all_49_1_43, first_homotop_grp(all_0_5_5, all_0_4_4) = all_0_2_2, yields: % 4.97/1.84 | (77) all_49_1_43 = all_0_2_2 % 4.97/1.84 | % 4.97/1.84 | Instantiating formula (27) with all_0_5_5, all_0_4_4, all_49_1_43, all_51_0_45 and discharging atoms first_homotop_grp(all_0_5_5, all_0_4_4) = all_51_0_45, first_homotop_grp(all_0_5_5, all_0_4_4) = all_49_1_43, yields: % 4.97/1.84 | (78) all_51_0_45 = all_49_1_43 % 4.97/1.84 | % 4.97/1.84 | Instantiating formula (27) with all_0_5_5, all_0_4_4, all_45_0_36, all_51_0_45 and discharging atoms first_homotop_grp(all_0_5_5, all_0_4_4) = all_51_0_45, first_homotop_grp(all_0_5_5, all_0_4_4) = all_45_0_36, yields: % 4.97/1.84 | (79) all_51_0_45 = all_45_0_36 % 4.97/1.84 | % 4.97/1.84 | Instantiating formula (27) with all_0_5_5, all_0_4_4, all_45_1_37, all_49_1_43 and discharging atoms first_homotop_grp(all_0_5_5, all_0_4_4) = all_49_1_43, first_homotop_grp(all_0_5_5, all_0_4_4) = all_45_1_37, yields: % 4.97/1.84 | (80) all_49_1_43 = all_45_1_37 % 4.97/1.84 | % 4.97/1.85 | Combining equations (78,79) yields a new equation: % 4.97/1.85 | (81) all_49_1_43 = all_45_0_36 % 4.97/1.85 | % 4.97/1.85 | Simplifying 81 yields: % 4.97/1.85 | (82) all_49_1_43 = all_45_0_36 % 4.97/1.85 | % 4.97/1.85 | Combining equations (75,76) yields a new equation: % 4.97/1.85 | (83) all_47_0_39 = all_0_1_1 % 4.97/1.85 | % 4.97/1.85 | Combining equations (77,82) yields a new equation: % 4.97/1.85 | (84) all_45_0_36 = all_0_2_2 % 4.97/1.85 | % 4.97/1.85 | Combining equations (80,82) yields a new equation: % 4.97/1.85 | (85) all_45_0_36 = all_45_1_37 % 4.97/1.85 | % 4.97/1.85 | Combining equations (84,85) yields a new equation: % 4.97/1.85 | (86) all_45_1_37 = all_0_2_2 % 4.97/1.85 | % 4.97/1.85 | Combining equations (86,85) yields a new equation: % 4.97/1.85 | (84) all_45_0_36 = all_0_2_2 % 4.97/1.85 | % 4.97/1.85 | Combining equations (84,82) yields a new equation: % 4.97/1.85 | (77) all_49_1_43 = all_0_2_2 % 4.97/1.85 | % 4.97/1.85 | Combining equations (83,76) yields a new equation: % 4.97/1.85 | (75) all_49_0_42 = all_0_1_1 % 4.97/1.85 | % 4.97/1.85 | From (77)(75) and (69) follows: % 4.97/1.85 | (90) a_group_isomorphism_from_to(all_49_2_44, all_0_2_2, all_0_1_1) = 0 % 4.97/1.85 | % 4.97/1.85 | Instantiating formula (2) with all_49_2_44, all_0_0_0, all_0_1_1, all_0_2_2 and discharging atoms isomorphic_groups(all_0_2_2, all_0_1_1) = all_0_0_0, a_group_isomorphism_from_to(all_49_2_44, all_0_2_2, all_0_1_1) = 0, yields: % 4.97/1.85 | (91) all_0_0_0 = 0 % 4.97/1.85 | % 4.97/1.85 | Equations (91) can reduce 4 to: % 4.97/1.85 | (92) $false % 4.97/1.85 | % 4.97/1.85 |-The branch is then unsatisfiable % 4.97/1.85 |-Branch two: % 4.97/1.85 | (93) ~ (all_25_1_35 = 0) & path_connected(all_0_5_5) = all_25_1_35 % 4.97/1.85 | % 4.97/1.85 | Applying alpha-rule on (93) yields: % 4.97/1.85 | (94) ~ (all_25_1_35 = 0) % 4.97/1.85 | (95) path_connected(all_0_5_5) = all_25_1_35 % 4.97/1.85 | % 4.97/1.85 | Instantiating formula (10) with all_0_5_5, all_25_1_35, 0 and discharging atoms path_connected(all_0_5_5) = all_25_1_35, path_connected(all_0_5_5) = 0, yields: % 4.97/1.85 | (96) all_25_1_35 = 0 % 4.97/1.85 | % 4.97/1.85 | Equations (96) can reduce 94 to: % 4.97/1.85 | (92) $false % 4.97/1.85 | % 4.97/1.85 |-The branch is then unsatisfiable % 4.97/1.85 |-Branch two: % 4.97/1.85 | (98) ~ (all_24_1_33 = 0) & path_connected(all_0_5_5) = all_24_1_33 % 4.97/1.85 | % 4.97/1.85 | Applying alpha-rule on (98) yields: % 4.97/1.85 | (99) ~ (all_24_1_33 = 0) % 4.97/1.85 | (100) path_connected(all_0_5_5) = all_24_1_33 % 4.97/1.85 | % 4.97/1.85 | Instantiating formula (10) with all_0_5_5, all_24_1_33, 0 and discharging atoms path_connected(all_0_5_5) = all_24_1_33, path_connected(all_0_5_5) = 0, yields: % 4.97/1.85 | (101) all_24_1_33 = 0 % 4.97/1.85 | % 4.97/1.85 | Equations (101) can reduce 99 to: % 4.97/1.85 | (92) $false % 4.97/1.85 | % 4.97/1.85 |-The branch is then unsatisfiable % 4.97/1.85 |-Branch two: % 4.97/1.85 | (103) ~ (all_23_1_31 = 0) & path_connected(all_0_5_5) = all_23_1_31 % 4.97/1.85 | % 4.97/1.85 | Applying alpha-rule on (103) yields: % 4.97/1.85 | (104) ~ (all_23_1_31 = 0) % 4.97/1.85 | (105) path_connected(all_0_5_5) = all_23_1_31 % 4.97/1.85 | % 4.97/1.85 | Instantiating formula (10) with all_0_5_5, all_23_1_31, 0 and discharging atoms path_connected(all_0_5_5) = all_23_1_31, path_connected(all_0_5_5) = 0, yields: % 4.97/1.85 | (106) all_23_1_31 = 0 % 4.97/1.85 | % 4.97/1.85 | Equations (106) can reduce 104 to: % 4.97/1.85 | (92) $false % 4.97/1.85 | % 4.97/1.85 |-The branch is then unsatisfiable % 4.97/1.85 |-Branch two: % 4.97/1.85 | (108) ~ (all_22_1_29 = 0) & path_connected(all_0_5_5) = all_22_1_29 % 4.97/1.85 | % 4.97/1.85 | Applying alpha-rule on (108) yields: % 4.97/1.85 | (109) ~ (all_22_1_29 = 0) % 4.97/1.86 | (110) path_connected(all_0_5_5) = all_22_1_29 % 4.97/1.86 | % 4.97/1.86 | Instantiating formula (10) with all_0_5_5, all_22_1_29, 0 and discharging atoms path_connected(all_0_5_5) = all_22_1_29, path_connected(all_0_5_5) = 0, yields: % 4.97/1.86 | (111) all_22_1_29 = 0 % 4.97/1.86 | % 4.97/1.86 | Equations (111) can reduce 109 to: % 4.97/1.86 | (92) $false % 4.97/1.86 | % 4.97/1.86 |-The branch is then unsatisfiable % 4.97/1.86 % SZS output end Proof for theBenchmark % 4.97/1.86 % 4.97/1.86 1273ms %------------------------------------------------------------------------------