%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n003.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 08:43:24 EDT 2022 % Result : Theorem 6.23s 2.05s % Output : Proof 11.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n003.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 14 12:04:25 EDT 2022 % 0.13/0.35 % CPUTime : % 0.20/0.60 ____ _ % 0.20/0.60 ___ / __ \_____(_)___ ________ __________ % 0.20/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.20/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.20/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.20/0.60 % 0.20/0.60 A Theorem Prover for First-Order Logic % 0.20/0.61 (ePrincess v.1.0) % 0.20/0.61 % 0.20/0.61 (c) Philipp Rümmer, 2009-2015 % 0.20/0.61 (c) Peter Backeman, 2014-2015 % 0.20/0.61 (contributions by Angelo Brillout, Peter Baumgartner) % 0.20/0.61 Free software under GNU Lesser General Public License (LGPL). % 0.20/0.61 Bug reports to peter@backeman.se % 0.20/0.61 % 0.20/0.61 For more information, visit http://user.uu.se/~petba168/breu/ % 0.20/0.61 % 0.20/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.70/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.06/1.04 Prover 0: Preprocessing ... % 3.37/1.42 Prover 0: Warning: ignoring some quantifiers % 3.67/1.46 Prover 0: Constructing countermodel ... % 6.23/2.05 Prover 0: proved (1396ms) % 6.23/2.05 % 6.23/2.05 No countermodel exists, formula is valid % 6.23/2.05 % SZS status Theorem for theBenchmark % 6.23/2.05 % 6.23/2.05 Generating proof ... Warning: ignoring some quantifiers % 10.15/2.96 found it (size 290) % 10.15/2.96 % 10.15/2.96 % SZS output start Proof for theBenchmark % 10.15/2.96 Assumed formulas after preprocessing and simplification: % 10.15/2.96 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : (k3_latsubgr(v0, v3, v6) = v7 & k11_group_4(v3) = v5 & k11_group_4(v0) = v2 & u1_struct_0(v3) = v4 & u1_struct_0(v0) = v1 & l2_lattices(v13) & l1_lattices(v15) & l1_struct_0(v14) & l1_struct_0(v8) & v1_xboole_0(v11) & v1_xboole_0(v10) & v1_xboole_0(k1_xboole_0) & v1_relat_1(v11) & l3_lattices(v12) & v2_funct_1(v11) & v2_funct_1(v6) & m2_relset_1(v6, v1, v4) & v1_group_6(v6, v0, v3) & v1_funct_2(v6, v1, v4) & v1_funct_1(v11) & v1_funct_1(v6) & l1_group_1(v16) & l1_group_1(v3) & l1_group_1(v0) & v4_group_1(v3) & v4_group_1(v0) & v3_group_1(v3) & v3_group_1(v0) & ~ v1_xboole_0(v9) & ~ m1_lattice4(v7, v2, v5) & ~ v3_struct_0(v8) & ~ v3_struct_0(v3) & ~ v3_struct_0(v0) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v23 = v19 | ~ (g3_lattices(v21, v22, v23) = v20) | ~ (g3_lattices(v17, v18, v19) = v20) | ~ v1_funct_1(v19) | ~ v1_funct_1(v18) | ? [v24] : (k2_zfmisc_1(v17, v17) = v24 & ( ~ m1_relset_1(v19, v24, v17) | ~ m1_relset_1(v18, v24, v17) | ~ v1_funct_2(v19, v24, v17) | ~ v1_funct_2(v18, v24, v17)))) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v22 = v18 | ~ (g3_lattices(v21, v22, v23) = v20) | ~ (g3_lattices(v17, v18, v19) = v20) | ~ v1_funct_1(v19) | ~ v1_funct_1(v18) | ? [v24] : (k2_zfmisc_1(v17, v17) = v24 & ( ~ m1_relset_1(v19, v24, v17) | ~ m1_relset_1(v18, v24, v17) | ~ v1_funct_2(v19, v24, v17) | ~ v1_funct_2(v18, v24, v17)))) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ! [v22] : ! [v23] : (v21 = v17 | ~ (g3_lattices(v21, v22, v23) = v20) | ~ (g3_lattices(v17, v18, v19) = v20) | ~ v1_funct_1(v19) | ~ v1_funct_1(v18) | ? [v24] : (k2_zfmisc_1(v17, v17) = v24 & ( ~ m1_relset_1(v19, v24, v17) | ~ m1_relset_1(v18, v24, v17) | ~ v1_funct_2(v19, v24, v17) | ~ v1_funct_2(v18, v24, v17)))) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : (v21 = v17 | ~ (u1_struct_0(v17) = v18) | ~ (u2_lattices(v17) = v19) | ~ (u1_lattices(v17) = v20) | ~ (g3_lattices(v18, v19, v20) = v21) | ~ v3_lattices(v17) | ~ l3_lattices(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : (v18 = v17 | ~ (k3_latsubgr(v21, v20, v19) = v18) | ~ (k3_latsubgr(v21, v20, v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : (v18 = v17 | ~ (g3_lattices(v21, v20, v19) = v18) | ~ (g3_lattices(v21, v20, v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v19) = v20) | ~ (u1_struct_0(v17) = v18) | ~ m4_vectsp_8(v21, v17, v19) | ~ m3_vectsp_8(v21, v17, v19) | ~ v10_lattices(v19) | ~ v10_lattices(v17) | ~ l3_lattices(v19) | ~ l3_lattices(v17) | ~ m2_relset_1(v21, v18, v20) | ~ v1_funct_2(v21, v18, v20) | ~ v1_funct_1(v21) | m1_lattice4(v21, v17, v19) | v3_struct_0(v19) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v19) = v20) | ~ (u1_struct_0(v17) = v18) | ~ v10_lattices(v19) | ~ v10_lattices(v17) | ~ l3_lattices(v19) | ~ l3_lattices(v17) | ~ m1_lattice4(v21, v17, v19) | ~ m2_relset_1(v21, v18, v20) | ~ v1_funct_2(v21, v18, v20) | ~ v1_funct_1(v21) | m4_vectsp_8(v21, v17, v19) | v3_struct_0(v19) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v19) = v20) | ~ (u1_struct_0(v17) = v18) | ~ v10_lattices(v19) | ~ v10_lattices(v17) | ~ l3_lattices(v19) | ~ l3_lattices(v17) | ~ m1_lattice4(v21, v17, v19) | ~ m2_relset_1(v21, v18, v20) | ~ v1_funct_2(v21, v18, v20) | ~ v1_funct_1(v21) | m3_vectsp_8(v21, v17, v19) | v3_struct_0(v19) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ m4_vectsp_8(v21, v17, v18) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | m2_relset_1(v21, v19, v20) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ m4_vectsp_8(v21, v17, v18) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | v1_funct_2(v21, v19, v20) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ m4_vectsp_8(v21, v17, v18) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | v1_funct_1(v21) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ m3_vectsp_8(v21, v17, v18) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | m2_relset_1(v21, v19, v20) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ m3_vectsp_8(v21, v17, v18) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | v1_funct_2(v21, v19, v20) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ m3_vectsp_8(v21, v17, v18) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | v1_funct_1(v21) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | ~ m1_lattice4(v21, v17, v18) | m2_relset_1(v21, v19, v20) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | ~ m1_lattice4(v21, v17, v18) | v1_funct_2(v21, v19, v20) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (u1_struct_0(v18) = v20) | ~ (u1_struct_0(v17) = v19) | ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | ~ m1_lattice4(v21, v17, v18) | v1_funct_1(v21) | v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v18 = v17 | ~ (k2_zfmisc_1(v20, v19) = v18) | ~ (k2_zfmisc_1(v20, v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (k3_latsubgr(v17, v18, v19) = v20) | ~ v1_funct_1(v19) | ~ l1_group_1(v18) | ~ l1_group_1(v17) | ~ v4_group_1(v18) | ~ v4_group_1(v17) | ~ v3_group_1(v18) | ~ v3_group_1(v17) | v3_struct_0(v18) | v3_struct_0(v17) | ? [v21] : ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : (k11_group_4(v18) = v25 & k11_group_4(v17) = v23 & u1_struct_0(v25) = v26 & u1_struct_0(v23) = v24 & u1_struct_0(v18) = v22 & u1_struct_0(v17) = v21 & ( ~ m1_relset_1(v19, v21, v22) | ~ v1_funct_2(v19, v21, v22) | (m2_relset_1(v20, v24, v26) & v1_funct_2(v20, v24, v26) & v1_funct_1(v20))))) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (k2_zfmisc_1(v17, v18) = v20) | ~ m2_relset_1(v19, v17, v18) | ? [v21] : (k1_zfmisc_1(v20) = v21 & m1_subset_1(v19, v21))) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (k1_zfmisc_1(v19) = v20) | ~ v1_xboole_0(v19) | ~ m1_subset_1(v18, v20) | ~ r2_hidden(v17, v18)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (k1_zfmisc_1(v19) = v20) | ~ m1_subset_1(v18, v20) | ~ r2_hidden(v17, v18) | m1_subset_1(v17, v19)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (g3_lattices(v17, v18, v19) = v20) | ~ v1_funct_1(v19) | ~ v1_funct_1(v18) | v3_lattices(v20) | ? [v21] : (k2_zfmisc_1(v17, v17) = v21 & ( ~ m1_relset_1(v19, v21, v17) | ~ m1_relset_1(v18, v21, v17) | ~ v1_funct_2(v19, v21, v17) | ~ v1_funct_2(v18, v21, v17)))) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (g3_lattices(v17, v18, v19) = v20) | ~ v1_funct_1(v19) | ~ v1_funct_1(v18) | l3_lattices(v20) | ? [v21] : (k2_zfmisc_1(v17, v17) = v21 & ( ~ m1_relset_1(v19, v21, v17) | ~ m1_relset_1(v18, v21, v17) | ~ v1_funct_2(v19, v21, v17) | ~ v1_funct_2(v18, v21, v17)))) & ? [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (k2_zfmisc_1(v18, v19) = v20) | v1_relat_1(v17) | ? [v21] : (k1_zfmisc_1(v20) = v21 & ~ m1_subset_1(v17, v21))) & ! [v17] : ! [v18] : ! [v19] : (v18 = v17 | ~ (k11_group_4(v19) = v18) | ~ (k11_group_4(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : (v18 = v17 | ~ (k1_zfmisc_1(v19) = v18) | ~ (k1_zfmisc_1(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : (v18 = v17 | ~ (u1_struct_0(v19) = v18) | ~ (u1_struct_0(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : (v18 = v17 | ~ (u2_lattices(v19) = v18) | ~ (u2_lattices(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : (v18 = v17 | ~ (u1_lattices(v19) = v18) | ~ (u1_lattices(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k2_zfmisc_1(v18, v18) = v19) | ~ (u1_struct_0(v17) = v18) | ~ l2_lattices(v17) | ? [v20] : (u2_lattices(v17) = v20 & m2_relset_1(v20, v19, v18) & v1_funct_2(v20, v19, v18) & v1_funct_1(v20))) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k2_zfmisc_1(v18, v18) = v19) | ~ (u1_struct_0(v17) = v18) | ~ l1_lattices(v17) | ? [v20] : (u1_lattices(v17) = v20 & m2_relset_1(v20, v19, v18) & v1_funct_2(v20, v19, v18) & v1_funct_1(v20))) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k2_zfmisc_1(v17, v18) = v19) | ~ v1_xboole_0(v19) | v1_xboole_0(v18) | v1_xboole_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k1_zfmisc_1(v18) = v19) | ~ r1_tarski(v17, v18) | m1_subset_1(v17, v19)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k1_zfmisc_1(v18) = v19) | ~ m1_subset_1(v17, v19) | r1_tarski(v17, v18)) & ! [v17] : ! [v18] : ! [v19] : ( ~ v1_xboole_0(v19) | ~ m1_relset_1(v19, v17, v18) | ~ v1_funct_2(v19, v17, v18) | ~ v1_funct_1(v19) | v1_xboole_0(v18) | v1_xboole_0(v17)) & ! [v17] : ! [v18] : ! [v19] : ( ~ v1_partfun1(v19, v17, v18) | ~ m1_relset_1(v19, v17, v18) | ~ v1_funct_1(v19) | v1_funct_2(v19, v17, v18)) & ! [v17] : ! [v18] : ! [v19] : ( ~ m1_relset_1(v19, v17, v18) | ~ v1_funct_2(v19, v17, v18) | ~ v1_funct_1(v19) | v1_xboole_0(v18) | v1_xboole_0(v17) | v1_partfun1(v19, v17, v18)) & ! [v17] : ! [v18] : ! [v19] : ( ~ m1_relset_1(v19, v17, v18) | ~ v1_funct_2(v19, v17, v18) | ~ v1_funct_1(v19) | v1_xboole_0(v18) | v1_partfun1(v19, v17, v18)) & ! [v17] : ! [v18] : ! [v19] : ( ~ m1_relset_1(v19, v17, v18) | m2_relset_1(v19, v17, v18)) & ! [v17] : ! [v18] : ! [v19] : ( ~ m2_relset_1(v19, v17, v18) | m1_relset_1(v19, v17, v18)) & ! [v17] : ! [v18] : (v18 = v17 | ~ v1_xboole_0(v18) | ~ v1_xboole_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | ~ v3_struct_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v15_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v14_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v13_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v9_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v8_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v7_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v6_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v5_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v4_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v10_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v3_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | l3_lattices(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v3_struct_0(v17) | ? [v19] : (u1_struct_0(v17) = v19 & ! [v20] : ! [v21] : ( ~ (k11_group_4(v20) = v21) | ~ l1_group_1(v20) | ~ v4_group_1(v20) | ~ v3_group_1(v20) | v3_struct_0(v20) | ? [v22] : (u1_struct_0(v20) = v22 & ! [v23] : ! [v24] : ( ~ (k3_latsubgr(v17, v20, v23) = v24) | ~ v2_funct_1(v23) | ~ m2_relset_1(v23, v19, v22) | ~ v1_group_6(v23, v17, v20) | ~ v1_funct_2(v23, v19, v22) | ~ v1_funct_1(v23) | m3_vectsp_8(v24, v18, v21)))) & ! [v20] : ! [v21] : ( ~ (u1_struct_0(v20) = v21) | ~ l1_group_1(v20) | ~ v4_group_1(v20) | ~ v3_group_1(v20) | v3_struct_0(v20) | ? [v22] : (k11_group_4(v20) = v22 & ! [v23] : ! [v24] : ( ~ (k3_latsubgr(v17, v20, v23) = v24) | ~ v2_funct_1(v23) | ~ m2_relset_1(v23, v19, v21) | ~ v1_group_6(v23, v17, v20) | ~ v1_funct_2(v23, v19, v21) | ~ v1_funct_1(v23) | m3_vectsp_8(v24, v18, v22)))))) & ! [v17] : ! [v18] : ( ~ (k11_group_4(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v3_struct_0(v17) | ? [v19] : (u1_struct_0(v17) = v19 & ! [v20] : ! [v21] : ( ~ (k11_group_4(v20) = v21) | ~ l1_group_1(v20) | ~ v4_group_1(v20) | ~ v3_group_1(v20) | v3_struct_0(v20) | ? [v22] : (u1_struct_0(v20) = v22 & ! [v23] : ! [v24] : ( ~ (k3_latsubgr(v17, v20, v23) = v24) | ~ m2_relset_1(v23, v19, v22) | ~ v1_group_6(v23, v17, v20) | ~ v1_funct_2(v23, v19, v22) | ~ v1_funct_1(v23) | m4_vectsp_8(v24, v18, v21)))) & ! [v20] : ! [v21] : ( ~ (u1_struct_0(v20) = v21) | ~ l1_group_1(v20) | ~ v4_group_1(v20) | ~ v3_group_1(v20) | v3_struct_0(v20) | ? [v22] : (k11_group_4(v20) = v22 & ! [v23] : ! [v24] : ( ~ (k3_latsubgr(v17, v20, v23) = v24) | ~ m2_relset_1(v23, v19, v21) | ~ v1_group_6(v23, v17, v20) | ~ v1_funct_2(v23, v19, v21) | ~ v1_funct_1(v23) | m4_vectsp_8(v24, v18, v22)))))) & ! [v17] : ! [v18] : ( ~ (k1_zfmisc_1(v17) = v18) | ~ v1_xboole_0(v18)) & ! [v17] : ! [v18] : ( ~ (k1_zfmisc_1(v17) = v18) | v1_xboole_0(v17) | ? [v19] : (m1_subset_1(v19, v18) & ~ v1_xboole_0(v19))) & ! [v17] : ! [v18] : ( ~ (k1_zfmisc_1(v17) = v18) | ? [v19] : (v1_xboole_0(v19) & m1_subset_1(v19, v18))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l2_lattices(v17) | ? [v19] : ? [v20] : (k2_zfmisc_1(v18, v18) = v20 & u2_lattices(v17) = v19 & m2_relset_1(v19, v20, v18) & v1_funct_2(v19, v20, v18) & v1_funct_1(v19))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l1_lattices(v17) | ? [v19] : ? [v20] : (k2_zfmisc_1(v18, v18) = v20 & u1_lattices(v17) = v19 & m2_relset_1(v19, v20, v18) & v1_funct_2(v19, v20, v18) & v1_funct_1(v19))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l1_struct_0(v17) | ~ v1_xboole_0(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l1_struct_0(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (k1_zfmisc_1(v18) = v19 & m1_subset_1(v20, v19) & ~ v1_xboole_0(v20))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v3_struct_0(v17) | ? [v19] : (k11_group_4(v17) = v19 & ! [v20] : ! [v21] : ( ~ (k11_group_4(v20) = v21) | ~ l1_group_1(v20) | ~ v4_group_1(v20) | ~ v3_group_1(v20) | v3_struct_0(v20) | ? [v22] : (u1_struct_0(v20) = v22 & ! [v23] : ! [v24] : ( ~ (k3_latsubgr(v17, v20, v23) = v24) | ~ v2_funct_1(v23) | ~ m2_relset_1(v23, v18, v22) | ~ v1_group_6(v23, v17, v20) | ~ v1_funct_2(v23, v18, v22) | ~ v1_funct_1(v23) | m3_vectsp_8(v24, v19, v21)))) & ! [v20] : ! [v21] : ( ~ (u1_struct_0(v20) = v21) | ~ l1_group_1(v20) | ~ v4_group_1(v20) | ~ v3_group_1(v20) | v3_struct_0(v20) | ? [v22] : (k11_group_4(v20) = v22 & ! [v23] : ! [v24] : ( ~ (k3_latsubgr(v17, v20, v23) = v24) | ~ v2_funct_1(v23) | ~ m2_relset_1(v23, v18, v21) | ~ v1_group_6(v23, v17, v20) | ~ v1_funct_2(v23, v18, v21) | ~ v1_funct_1(v23) | m3_vectsp_8(v24, v19, v22)))))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l1_group_1(v17) | ~ v4_group_1(v17) | ~ v3_group_1(v17) | v3_struct_0(v17) | ? [v19] : (k11_group_4(v17) = v19 & ! [v20] : ! [v21] : ( ~ (k11_group_4(v20) = v21) | ~ l1_group_1(v20) | ~ v4_group_1(v20) | ~ v3_group_1(v20) | v3_struct_0(v20) | ? [v22] : (u1_struct_0(v20) = v22 & ! [v23] : ! [v24] : ( ~ (k3_latsubgr(v17, v20, v23) = v24) | ~ m2_relset_1(v23, v18, v22) | ~ v1_group_6(v23, v17, v20) | ~ v1_funct_2(v23, v18, v22) | ~ v1_funct_1(v23) | m4_vectsp_8(v24, v19, v21)))) & ! [v20] : ! [v21] : ( ~ (u1_struct_0(v20) = v21) | ~ l1_group_1(v20) | ~ v4_group_1(v20) | ~ v3_group_1(v20) | v3_struct_0(v20) | ? [v22] : (k11_group_4(v20) = v22 & ! [v23] : ! [v24] : ( ~ (k3_latsubgr(v17, v20, v23) = v24) | ~ m2_relset_1(v23, v18, v21) | ~ v1_group_6(v23, v17, v20) | ~ v1_funct_2(v23, v18, v21) | ~ v1_funct_1(v23) | m4_vectsp_8(v24, v19, v22)))))) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | v1_funct_1(v18)) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | ? [v19] : ? [v20] : (k2_zfmisc_1(v19, v19) = v20 & u1_struct_0(v17) = v19 & m2_relset_1(v18, v20, v19) & v1_funct_2(v18, v20, v19))) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l1_lattices(v17) | v1_funct_1(v18)) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l1_lattices(v17) | ? [v19] : ? [v20] : (k2_zfmisc_1(v19, v19) = v20 & u1_struct_0(v17) = v19 & m2_relset_1(v18, v20, v19) & v1_funct_2(v18, v20, v19))) & ! [v17] : ! [v18] : ( ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | v3_struct_0(v18) | v3_struct_0(v17) | ? [v19] : m4_vectsp_8(v19, v17, v18)) & ! [v17] : ! [v18] : ( ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | v3_struct_0(v18) | v3_struct_0(v17) | ? [v19] : m3_vectsp_8(v19, v17, v18)) & ! [v17] : ! [v18] : ( ~ v10_lattices(v18) | ~ v10_lattices(v17) | ~ l3_lattices(v18) | ~ l3_lattices(v17) | v3_struct_0(v18) | v3_struct_0(v17) | ? [v19] : m1_lattice4(v19, v17, v18)) & ! [v17] : ! [v18] : ( ~ v1_xboole_0(v18) | ~ r2_hidden(v17, v18)) & ! [v17] : ! [v18] : ( ~ m1_subset_1(v17, v18) | v1_xboole_0(v18) | r2_hidden(v17, v18)) & ! [v17] : ! [v18] : ( ~ r2_hidden(v18, v17) | ~ r2_hidden(v17, v18)) & ! [v17] : ! [v18] : ( ~ r2_hidden(v17, v18) | m1_subset_1(v17, v18)) & ! [v17] : (v17 = k1_xboole_0 | ~ v1_xboole_0(v17)) & ! [v17] : ( ~ l2_lattices(v17) | l1_struct_0(v17)) & ! [v17] : ( ~ l1_lattices(v17) | l1_struct_0(v17)) & ! [v17] : ( ~ l3_lattices(v17) | l2_lattices(v17)) & ! [v17] : ( ~ l3_lattices(v17) | l1_lattices(v17)) & ! [v17] : ( ~ l1_group_1(v17) | l1_struct_0(v17)) & ? [v17] : ? [v18] : ? [v19] : m1_relset_1(v19, v17, v18) & ? [v17] : ? [v18] : ? [v19] : m2_relset_1(v19, v17, v18) & ? [v17] : ? [v18] : ? [v19] : (v1_relat_1(v19) & m1_relset_1(v19, v17, v18) & v1_funct_2(v19, v17, v18) & v1_funct_1(v19)) & ? [v17] : ? [v18] : ? [v19] : (v1_relat_1(v19) & m1_relset_1(v19, v17, v18) & v1_funct_1(v19)) & ? [v17] : ? [v18] : m1_subset_1(v18, v17) & ? [v17] : r1_tarski(v17, v17)) % 10.43/3.02 | 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, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13, all_0_14_14, all_0_15_15, all_0_16_16 yields: % 10.43/3.02 | (1) k3_latsubgr(all_0_16_16, all_0_13_13, all_0_10_10) = all_0_9_9 & k11_group_4(all_0_13_13) = all_0_11_11 & k11_group_4(all_0_16_16) = all_0_14_14 & u1_struct_0(all_0_13_13) = all_0_12_12 & u1_struct_0(all_0_16_16) = all_0_15_15 & l2_lattices(all_0_3_3) & l1_lattices(all_0_1_1) & l1_struct_0(all_0_2_2) & l1_struct_0(all_0_8_8) & v1_xboole_0(all_0_5_5) & v1_xboole_0(all_0_6_6) & v1_xboole_0(k1_xboole_0) & v1_relat_1(all_0_5_5) & l3_lattices(all_0_4_4) & v2_funct_1(all_0_5_5) & v2_funct_1(all_0_10_10) & m2_relset_1(all_0_10_10, all_0_15_15, all_0_12_12) & v1_group_6(all_0_10_10, all_0_16_16, all_0_13_13) & v1_funct_2(all_0_10_10, all_0_15_15, all_0_12_12) & v1_funct_1(all_0_5_5) & v1_funct_1(all_0_10_10) & l1_group_1(all_0_0_0) & l1_group_1(all_0_13_13) & l1_group_1(all_0_16_16) & v4_group_1(all_0_13_13) & v4_group_1(all_0_16_16) & v3_group_1(all_0_13_13) & v3_group_1(all_0_16_16) & ~ v1_xboole_0(all_0_7_7) & ~ m1_lattice4(all_0_9_9, all_0_14_14, all_0_11_11) & ~ v3_struct_0(all_0_8_8) & ~ v3_struct_0(all_0_13_13) & ~ v3_struct_0(all_0_16_16) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v2 | ~ (g3_lattices(v4, v5, v6) = v3) | ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | ? [v7] : (k2_zfmisc_1(v0, v0) = v7 & ( ~ m1_relset_1(v2, v7, v0) | ~ m1_relset_1(v1, v7, v0) | ~ v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, v7, v0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v5 = v1 | ~ (g3_lattices(v4, v5, v6) = v3) | ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | ? [v7] : (k2_zfmisc_1(v0, v0) = v7 & ( ~ m1_relset_1(v2, v7, v0) | ~ m1_relset_1(v1, v7, v0) | ~ v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, v7, v0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v0 | ~ (g3_lattices(v4, v5, v6) = v3) | ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | ? [v7] : (k2_zfmisc_1(v0, v0) = v7 & ( ~ m1_relset_1(v2, v7, v0) | ~ m1_relset_1(v1, v7, v0) | ~ v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, v7, v0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v0 | ~ (u1_struct_0(v0) = v1) | ~ (u2_lattices(v0) = v2) | ~ (u1_lattices(v0) = v3) | ~ (g3_lattices(v1, v2, v3) = v4) | ~ v3_lattices(v0) | ~ l3_lattices(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (k3_latsubgr(v4, v3, v2) = v1) | ~ (k3_latsubgr(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (g3_lattices(v4, v3, v2) = v1) | ~ (g3_lattices(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v2) = v3) | ~ (u1_struct_0(v0) = v1) | ~ m4_vectsp_8(v4, v0, v2) | ~ m3_vectsp_8(v4, v0, v2) | ~ v10_lattices(v2) | ~ v10_lattices(v0) | ~ l3_lattices(v2) | ~ l3_lattices(v0) | ~ m2_relset_1(v4, v1, v3) | ~ v1_funct_2(v4, v1, v3) | ~ v1_funct_1(v4) | m1_lattice4(v4, v0, v2) | v3_struct_0(v2) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v2) = v3) | ~ (u1_struct_0(v0) = v1) | ~ v10_lattices(v2) | ~ v10_lattices(v0) | ~ l3_lattices(v2) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v2) | ~ m2_relset_1(v4, v1, v3) | ~ v1_funct_2(v4, v1, v3) | ~ v1_funct_1(v4) | m4_vectsp_8(v4, v0, v2) | v3_struct_0(v2) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v2) = v3) | ~ (u1_struct_0(v0) = v1) | ~ v10_lattices(v2) | ~ v10_lattices(v0) | ~ l3_lattices(v2) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v2) | ~ m2_relset_1(v4, v1, v3) | ~ v1_funct_2(v4, v1, v3) | ~ v1_funct_1(v4) | m3_vectsp_8(v4, v0, v2) | v3_struct_0(v2) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m4_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | m2_relset_1(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m4_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v1_funct_2(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m4_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v1_funct_1(v4) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m3_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | m2_relset_1(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m3_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v1_funct_2(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m3_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v1_funct_1(v4) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v1) | m2_relset_1(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v1) | v1_funct_2(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v1) | v1_funct_1(v4) | v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k2_zfmisc_1(v3, v2) = v1) | ~ (k2_zfmisc_1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k3_latsubgr(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ l1_group_1(v1) | ~ l1_group_1(v0) | ~ v4_group_1(v1) | ~ v4_group_1(v0) | ~ v3_group_1(v1) | ~ v3_group_1(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (k11_group_4(v1) = v8 & k11_group_4(v0) = v6 & u1_struct_0(v8) = v9 & u1_struct_0(v6) = v7 & u1_struct_0(v1) = v5 & u1_struct_0(v0) = v4 & ( ~ m1_relset_1(v2, v4, v5) | ~ v1_funct_2(v2, v4, v5) | (m2_relset_1(v3, v7, v9) & v1_funct_2(v3, v7, v9) & v1_funct_1(v3))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k2_zfmisc_1(v0, v1) = v3) | ~ m2_relset_1(v2, v0, v1) | ? [v4] : (k1_zfmisc_1(v3) = v4 & m1_subset_1(v2, v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_zfmisc_1(v2) = v3) | ~ v1_xboole_0(v2) | ~ m1_subset_1(v1, v3) | ~ r2_hidden(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_zfmisc_1(v2) = v3) | ~ m1_subset_1(v1, v3) | ~ r2_hidden(v0, v1) | m1_subset_1(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | v3_lattices(v3) | ? [v4] : (k2_zfmisc_1(v0, v0) = v4 & ( ~ m1_relset_1(v2, v4, v0) | ~ m1_relset_1(v1, v4, v0) | ~ v1_funct_2(v2, v4, v0) | ~ v1_funct_2(v1, v4, v0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | l3_lattices(v3) | ? [v4] : (k2_zfmisc_1(v0, v0) = v4 & ( ~ m1_relset_1(v2, v4, v0) | ~ m1_relset_1(v1, v4, v0) | ~ v1_funct_2(v2, v4, v0) | ~ v1_funct_2(v1, v4, v0)))) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k2_zfmisc_1(v1, v2) = v3) | v1_relat_1(v0) | ? [v4] : (k1_zfmisc_1(v3) = v4 & ~ m1_subset_1(v0, v4))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (k11_group_4(v2) = v1) | ~ (k11_group_4(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u2_lattices(v2) = v1) | ~ (u2_lattices(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u1_lattices(v2) = v1) | ~ (u1_lattices(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k2_zfmisc_1(v1, v1) = v2) | ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ? [v3] : (u2_lattices(v0) = v3 & m2_relset_1(v3, v2, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k2_zfmisc_1(v1, v1) = v2) | ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ? [v3] : (u1_lattices(v0) = v3 & m2_relset_1(v3, v2, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k2_zfmisc_1(v0, v1) = v2) | ~ v1_xboole_0(v2) | v1_xboole_0(v1) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_zfmisc_1(v1) = v2) | ~ r1_tarski(v0, v1) | m1_subset_1(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_zfmisc_1(v1) = v2) | ~ m1_subset_1(v0, v2) | r1_tarski(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ v1_xboole_0(v2) | ~ m1_relset_1(v2, v0, v1) | ~ v1_funct_2(v2, v0, v1) | ~ v1_funct_1(v2) | v1_xboole_0(v1) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ v1_partfun1(v2, v0, v1) | ~ m1_relset_1(v2, v0, v1) | ~ v1_funct_1(v2) | v1_funct_2(v2, v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ m1_relset_1(v2, v0, v1) | ~ v1_funct_2(v2, v0, v1) | ~ v1_funct_1(v2) | v1_xboole_0(v1) | v1_xboole_0(v0) | v1_partfun1(v2, v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ m1_relset_1(v2, v0, v1) | ~ v1_funct_2(v2, v0, v1) | ~ v1_funct_1(v2) | v1_xboole_0(v1) | v1_partfun1(v2, v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ m1_relset_1(v2, v0, v1) | m2_relset_1(v2, v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ m2_relset_1(v2, v0, v1) | m1_relset_1(v2, v0, v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ v1_xboole_0(v1) | ~ v1_xboole_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | ~ v3_struct_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v15_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v14_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v13_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v9_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v8_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v7_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v6_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v5_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v4_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v10_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | l3_lattices(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k11_group_4(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (u1_struct_0(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ v2_funct_1(v6) | ~ m2_relset_1(v6, v2, v5) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v2, v5) | ~ v1_funct_1(v6) | m3_vectsp_8(v7, v1, v4)))) & ! [v3] : ! [v4] : ( ~ (u1_struct_0(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (k11_group_4(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ v2_funct_1(v6) | ~ m2_relset_1(v6, v2, v4) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v2, v4) | ~ v1_funct_1(v6) | m3_vectsp_8(v7, v1, v5)))))) & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k11_group_4(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (u1_struct_0(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ m2_relset_1(v6, v2, v5) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v2, v5) | ~ v1_funct_1(v6) | m4_vectsp_8(v7, v1, v4)))) & ! [v3] : ! [v4] : ( ~ (u1_struct_0(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (k11_group_4(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ m2_relset_1(v6, v2, v4) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v2, v4) | ~ v1_funct_1(v6) | m4_vectsp_8(v7, v1, v5)))))) & ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ v1_xboole_0(v1)) & ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | v1_xboole_0(v0) | ? [v2] : (m1_subset_1(v2, v1) & ~ v1_xboole_0(v2))) & ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | ? [v2] : (v1_xboole_0(v2) & m1_subset_1(v2, v1))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ? [v2] : ? [v3] : (k2_zfmisc_1(v1, v1) = v3 & u2_lattices(v0) = v2 & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ? [v2] : ? [v3] : (k2_zfmisc_1(v1, v1) = v3 & u1_lattices(v0) = v2 & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_struct_0(v0) | ~ v1_xboole_0(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_struct_0(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (k1_zfmisc_1(v1) = v2 & m1_subset_1(v3, v2) & ~ v1_xboole_0(v3))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k11_group_4(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (u1_struct_0(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ v2_funct_1(v6) | ~ m2_relset_1(v6, v1, v5) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v1, v5) | ~ v1_funct_1(v6) | m3_vectsp_8(v7, v2, v4)))) & ! [v3] : ! [v4] : ( ~ (u1_struct_0(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (k11_group_4(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ v2_funct_1(v6) | ~ m2_relset_1(v6, v1, v4) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v1, v4) | ~ v1_funct_1(v6) | m3_vectsp_8(v7, v2, v5)))))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k11_group_4(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (u1_struct_0(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ m2_relset_1(v6, v1, v5) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v1, v5) | ~ v1_funct_1(v6) | m4_vectsp_8(v7, v2, v4)))) & ! [v3] : ! [v4] : ( ~ (u1_struct_0(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (k11_group_4(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ m2_relset_1(v6, v1, v4) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v1, v4) | ~ v1_funct_1(v6) | m4_vectsp_8(v7, v2, v5)))))) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | v1_funct_1(v1)) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ? [v2] : ? [v3] : (k2_zfmisc_1(v2, v2) = v3 & u1_struct_0(v0) = v2 & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | v1_funct_1(v1)) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ? [v2] : ? [v3] : (k2_zfmisc_1(v2, v2) = v3 & u1_struct_0(v0) = v2 & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) & ! [v0] : ! [v1] : ( ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v2] : m4_vectsp_8(v2, v0, v1)) & ! [v0] : ! [v1] : ( ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v2] : m3_vectsp_8(v2, v0, v1)) & ! [v0] : ! [v1] : ( ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v2] : m1_lattice4(v2, v0, v1)) & ! [v0] : ! [v1] : ( ~ v1_xboole_0(v1) | ~ r2_hidden(v0, v1)) & ! [v0] : ! [v1] : ( ~ m1_subset_1(v0, v1) | v1_xboole_0(v1) | r2_hidden(v0, v1)) & ! [v0] : ! [v1] : ( ~ r2_hidden(v1, v0) | ~ r2_hidden(v0, v1)) & ! [v0] : ! [v1] : ( ~ r2_hidden(v0, v1) | m1_subset_1(v0, v1)) & ! [v0] : (v0 = k1_xboole_0 | ~ v1_xboole_0(v0)) & ! [v0] : ( ~ l2_lattices(v0) | l1_struct_0(v0)) & ! [v0] : ( ~ l1_lattices(v0) | l1_struct_0(v0)) & ! [v0] : ( ~ l3_lattices(v0) | l2_lattices(v0)) & ! [v0] : ( ~ l3_lattices(v0) | l1_lattices(v0)) & ! [v0] : ( ~ l1_group_1(v0) | l1_struct_0(v0)) & ? [v0] : ? [v1] : ? [v2] : m1_relset_1(v2, v0, v1) & ? [v0] : ? [v1] : ? [v2] : m2_relset_1(v2, v0, v1) & ? [v0] : ? [v1] : ? [v2] : (v1_relat_1(v2) & m1_relset_1(v2, v0, v1) & v1_funct_2(v2, v0, v1) & v1_funct_1(v2)) & ? [v0] : ? [v1] : ? [v2] : (v1_relat_1(v2) & m1_relset_1(v2, v0, v1) & v1_funct_1(v2)) & ? [v0] : ? [v1] : m1_subset_1(v1, v0) & ? [v0] : r1_tarski(v0, v0) % 10.43/3.05 | % 10.43/3.05 | Applying alpha-rule on (1) yields: % 10.43/3.05 | (2) ! [v0] : (v0 = k1_xboole_0 | ~ v1_xboole_0(v0)) % 10.43/3.05 | (3) v1_funct_1(all_0_10_10) % 10.43/3.05 | (4) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v10_lattices(v1) | v3_struct_0(v0)) % 10.43/3.05 | (5) ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ v1_xboole_0(v1)) % 10.43/3.05 | (6) l1_group_1(all_0_13_13) % 10.43/3.05 | (7) m2_relset_1(all_0_10_10, all_0_15_15, all_0_12_12) % 10.43/3.05 | (8) v1_xboole_0(all_0_6_6) % 10.43/3.05 | (9) l1_struct_0(all_0_2_2) % 10.43/3.05 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | v3_lattices(v3) | ? [v4] : (k2_zfmisc_1(v0, v0) = v4 & ( ~ m1_relset_1(v2, v4, v0) | ~ m1_relset_1(v1, v4, v0) | ~ v1_funct_2(v2, v4, v0) | ~ v1_funct_2(v1, v4, v0)))) % 10.43/3.05 | (11) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) % 10.43/3.05 | (12) v1_relat_1(all_0_5_5) % 10.43/3.05 | (13) ! [v0] : ( ~ l1_group_1(v0) | l1_struct_0(v0)) % 10.43/3.05 | (14) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k11_group_4(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (u1_struct_0(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ m2_relset_1(v6, v2, v5) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v2, v5) | ~ v1_funct_1(v6) | m4_vectsp_8(v7, v1, v4)))) & ! [v3] : ! [v4] : ( ~ (u1_struct_0(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (k11_group_4(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ m2_relset_1(v6, v2, v4) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v2, v4) | ~ v1_funct_1(v6) | m4_vectsp_8(v7, v1, v5)))))) % 10.43/3.05 | (15) ! [v0] : ! [v1] : ( ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v2] : m4_vectsp_8(v2, v0, v1)) % 10.43/3.05 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v2) = v3) | ~ (u1_struct_0(v0) = v1) | ~ m4_vectsp_8(v4, v0, v2) | ~ m3_vectsp_8(v4, v0, v2) | ~ v10_lattices(v2) | ~ v10_lattices(v0) | ~ l3_lattices(v2) | ~ l3_lattices(v0) | ~ m2_relset_1(v4, v1, v3) | ~ v1_funct_2(v4, v1, v3) | ~ v1_funct_1(v4) | m1_lattice4(v4, v0, v2) | v3_struct_0(v2) | v3_struct_0(v0)) % 10.43/3.05 | (17) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v4_lattices(v1) | v3_struct_0(v0)) % 10.43/3.05 | (18) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v9_lattices(v1) | v3_struct_0(v0)) % 10.43/3.05 | (19) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ? [v2] : ? [v3] : (k2_zfmisc_1(v1, v1) = v3 & u1_lattices(v0) = v2 & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 10.43/3.05 | (20) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_struct_0(v0) | ~ v1_xboole_0(v1) | v3_struct_0(v0)) % 10.43/3.05 | (21) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ? [v2] : ? [v3] : (k2_zfmisc_1(v1, v1) = v3 & u2_lattices(v0) = v2 & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 10.43/3.06 | (22) k3_latsubgr(all_0_16_16, all_0_13_13, all_0_10_10) = all_0_9_9 % 10.43/3.06 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u1_lattices(v2) = v1) | ~ (u1_lattices(v2) = v0)) % 10.43/3.06 | (24) ~ m1_lattice4(all_0_9_9, all_0_14_14, all_0_11_11) % 10.43/3.06 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = v2 | ~ (g3_lattices(v4, v5, v6) = v3) | ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | ? [v7] : (k2_zfmisc_1(v0, v0) = v7 & ( ~ m1_relset_1(v2, v7, v0) | ~ m1_relset_1(v1, v7, v0) | ~ v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, v7, v0)))) % 10.43/3.06 | (26) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v13_lattices(v1) | v3_struct_0(v0)) % 10.43/3.06 | (27) ! [v0] : ! [v1] : ( ~ v1_xboole_0(v1) | ~ r2_hidden(v0, v1)) % 10.43/3.06 | (28) ? [v0] : ? [v1] : ? [v2] : m1_relset_1(v2, v0, v1) % 10.43/3.06 | (29) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v14_lattices(v1) | v3_struct_0(v0)) % 10.43/3.06 | (30) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m4_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v1_funct_2(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.06 | (31) u1_struct_0(all_0_16_16) = all_0_15_15 % 10.43/3.06 | (32) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (k11_group_4(v2) = v1) | ~ (k11_group_4(v2) = v0)) % 10.43/3.06 | (33) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k11_group_4(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (u1_struct_0(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ v2_funct_1(v6) | ~ m2_relset_1(v6, v2, v5) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v2, v5) | ~ v1_funct_1(v6) | m3_vectsp_8(v7, v1, v4)))) & ! [v3] : ! [v4] : ( ~ (u1_struct_0(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (k11_group_4(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ v2_funct_1(v6) | ~ m2_relset_1(v6, v2, v4) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v2, v4) | ~ v1_funct_1(v6) | m3_vectsp_8(v7, v1, v5)))))) % 10.43/3.06 | (34) ~ v3_struct_0(all_0_16_16) % 10.43/3.06 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ (k2_zfmisc_1(v1, v1) = v2) | ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ? [v3] : (u2_lattices(v0) = v3 & m2_relset_1(v3, v2, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) % 10.43/3.06 | (36) l2_lattices(all_0_3_3) % 10.43/3.06 | (37) ! [v0] : ! [v1] : ! [v2] : ( ~ (k2_zfmisc_1(v1, v1) = v2) | ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ? [v3] : (u1_lattices(v0) = v3 & m2_relset_1(v3, v2, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) % 10.43/3.06 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v0 | ~ (g3_lattices(v4, v5, v6) = v3) | ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | ? [v7] : (k2_zfmisc_1(v0, v0) = v7 & ( ~ m1_relset_1(v2, v7, v0) | ~ m1_relset_1(v1, v7, v0) | ~ v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, v7, v0)))) % 10.43/3.06 | (39) k11_group_4(all_0_13_13) = all_0_11_11 % 10.43/3.06 | (40) v2_funct_1(all_0_10_10) % 10.43/3.06 | (41) ? [v0] : ? [v1] : ? [v2] : m2_relset_1(v2, v0, v1) % 10.43/3.06 | (42) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | ~ v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.06 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (g3_lattices(v4, v3, v2) = v1) | ~ (g3_lattices(v4, v3, v2) = v0)) % 10.43/3.06 | (44) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k11_group_4(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (u1_struct_0(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ m2_relset_1(v6, v1, v5) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v1, v5) | ~ v1_funct_1(v6) | m4_vectsp_8(v7, v2, v4)))) & ! [v3] : ! [v4] : ( ~ (u1_struct_0(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (k11_group_4(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ m2_relset_1(v6, v1, v4) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v1, v4) | ~ v1_funct_1(v6) | m4_vectsp_8(v7, v2, v5)))))) % 10.43/3.06 | (45) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v15_lattices(v1) | v3_struct_0(v0)) % 10.43/3.06 | (46) ! [v0] : ! [v1] : ( ~ r2_hidden(v1, v0) | ~ r2_hidden(v0, v1)) % 10.43/3.06 | (47) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ? [v2] : ? [v3] : (k2_zfmisc_1(v2, v2) = v3 & u1_struct_0(v0) = v2 & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) % 10.43/3.06 | (48) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | v1_funct_1(v1)) % 10.43/3.06 | (49) ~ v1_xboole_0(all_0_7_7) % 10.43/3.06 | (50) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ? [v2] : ? [v3] : (k2_zfmisc_1(v2, v2) = v3 & u1_struct_0(v0) = v2 & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) % 10.43/3.06 | (51) v1_group_6(all_0_10_10, all_0_16_16, all_0_13_13) % 10.43/3.06 | (52) ! [v0] : ! [v1] : ! [v2] : ( ~ (k2_zfmisc_1(v0, v1) = v2) | ~ v1_xboole_0(v2) | v1_xboole_0(v1) | v1_xboole_0(v0)) % 10.43/3.06 | (53) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) % 10.43/3.06 | (54) k11_group_4(all_0_16_16) = all_0_14_14 % 10.43/3.06 | (55) ! [v0] : ! [v1] : ! [v2] : ( ~ m1_relset_1(v2, v0, v1) | ~ v1_funct_2(v2, v0, v1) | ~ v1_funct_1(v2) | v1_xboole_0(v1) | v1_partfun1(v2, v0, v1)) % 10.43/3.06 | (56) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k2_zfmisc_1(v0, v1) = v3) | ~ m2_relset_1(v2, v0, v1) | ? [v4] : (k1_zfmisc_1(v3) = v4 & m1_subset_1(v2, v4))) % 10.43/3.06 | (57) ? [v0] : ? [v1] : m1_subset_1(v1, v0) % 10.43/3.06 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m4_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | m2_relset_1(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.06 | (59) v4_group_1(all_0_16_16) % 10.43/3.06 | (60) u1_struct_0(all_0_13_13) = all_0_12_12 % 10.43/3.07 | (61) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v5_lattices(v1) | v3_struct_0(v0)) % 10.43/3.07 | (62) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v2) = v3) | ~ (u1_struct_0(v0) = v1) | ~ v10_lattices(v2) | ~ v10_lattices(v0) | ~ l3_lattices(v2) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v2) | ~ m2_relset_1(v4, v1, v3) | ~ v1_funct_2(v4, v1, v3) | ~ v1_funct_1(v4) | m4_vectsp_8(v4, v0, v2) | v3_struct_0(v2) | v3_struct_0(v0)) % 10.43/3.07 | (63) l3_lattices(all_0_4_4) % 10.43/3.07 | (64) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k2_zfmisc_1(v1, v2) = v3) | v1_relat_1(v0) | ? [v4] : (k1_zfmisc_1(v3) = v4 & ~ m1_subset_1(v0, v4))) % 10.43/3.07 | (65) v1_funct_1(all_0_5_5) % 10.43/3.07 | (66) ! [v0] : ! [v1] : ( ~ r2_hidden(v0, v1) | m1_subset_1(v0, v1)) % 10.43/3.07 | (67) ! [v0] : ! [v1] : (v1 = v0 | ~ v1_xboole_0(v1) | ~ v1_xboole_0(v0)) % 10.43/3.07 | (68) l1_struct_0(all_0_8_8) % 10.43/3.07 | (69) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m3_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v1_funct_2(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.07 | (70) v1_xboole_0(k1_xboole_0) % 10.43/3.07 | (71) l1_group_1(all_0_16_16) % 10.43/3.07 | (72) ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_zfmisc_1(v1) = v2) | ~ m1_subset_1(v0, v2) | r1_tarski(v0, v1)) % 10.43/3.07 | (73) ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_zfmisc_1(v1) = v2) | ~ r1_tarski(v0, v1) | m1_subset_1(v0, v2)) % 10.43/3.07 | (74) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v7_lattices(v1) | v3_struct_0(v0)) % 10.43/3.07 | (75) ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | v1_xboole_0(v0) | ? [v2] : (m1_subset_1(v2, v1) & ~ v1_xboole_0(v2))) % 10.43/3.07 | (76) v3_group_1(all_0_16_16) % 10.43/3.07 | (77) ! [v0] : ( ~ l1_lattices(v0) | l1_struct_0(v0)) % 10.43/3.07 | (78) ? [v0] : r1_tarski(v0, v0) % 10.43/3.07 | (79) ~ v3_struct_0(all_0_8_8) % 10.43/3.07 | (80) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m3_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | m2_relset_1(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.07 | (81) v1_xboole_0(all_0_5_5) % 10.43/3.07 | (82) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k11_group_4(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (u1_struct_0(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ v2_funct_1(v6) | ~ m2_relset_1(v6, v1, v5) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v1, v5) | ~ v1_funct_1(v6) | m3_vectsp_8(v7, v2, v4)))) & ! [v3] : ! [v4] : ( ~ (u1_struct_0(v3) = v4) | ~ l1_group_1(v3) | ~ v4_group_1(v3) | ~ v3_group_1(v3) | v3_struct_0(v3) | ? [v5] : (k11_group_4(v3) = v5 & ! [v6] : ! [v7] : ( ~ (k3_latsubgr(v0, v3, v6) = v7) | ~ v2_funct_1(v6) | ~ m2_relset_1(v6, v1, v4) | ~ v1_group_6(v6, v0, v3) | ~ v1_funct_2(v6, v1, v4) | ~ v1_funct_1(v6) | m3_vectsp_8(v7, v2, v5)))))) % 10.43/3.07 | (83) ! [v0] : ! [v1] : ! [v2] : ( ~ m1_relset_1(v2, v0, v1) | ~ v1_funct_2(v2, v0, v1) | ~ v1_funct_1(v2) | v1_xboole_0(v1) | v1_xboole_0(v0) | v1_partfun1(v2, v0, v1)) % 10.43/3.07 | (84) l1_group_1(all_0_0_0) % 10.43/3.07 | (85) v1_funct_2(all_0_10_10, all_0_15_15, all_0_12_12) % 10.43/3.07 | (86) ! [v0] : ( ~ l2_lattices(v0) | l1_struct_0(v0)) % 10.43/3.07 | (87) ? [v0] : ? [v1] : ? [v2] : (v1_relat_1(v2) & m1_relset_1(v2, v0, v1) & v1_funct_1(v2)) % 10.43/3.07 | (88) ! [v0] : ! [v1] : ! [v2] : ( ~ m2_relset_1(v2, v0, v1) | m1_relset_1(v2, v0, v1)) % 10.43/3.07 | (89) ! [v0] : ! [v1] : ! [v2] : ( ~ m1_relset_1(v2, v0, v1) | m2_relset_1(v2, v0, v1)) % 10.43/3.07 | (90) v3_group_1(all_0_13_13) % 10.43/3.07 | (91) ? [v0] : ? [v1] : ? [v2] : (v1_relat_1(v2) & m1_relset_1(v2, v0, v1) & v1_funct_2(v2, v0, v1) & v1_funct_1(v2)) % 10.43/3.07 | (92) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = v0 | ~ (u1_struct_0(v0) = v1) | ~ (u2_lattices(v0) = v2) | ~ (u1_lattices(v0) = v3) | ~ (g3_lattices(v1, v2, v3) = v4) | ~ v3_lattices(v0) | ~ l3_lattices(v0)) % 10.43/3.07 | (93) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (k3_latsubgr(v4, v3, v2) = v1) | ~ (k3_latsubgr(v4, v3, v2) = v0)) % 10.43/3.07 | (94) l1_lattices(all_0_1_1) % 10.43/3.07 | (95) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m3_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v1_funct_1(v4) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.07 | (96) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_struct_0(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (k1_zfmisc_1(v1) = v2 & m1_subset_1(v3, v2) & ~ v1_xboole_0(v3))) % 10.43/3.07 | (97) v4_group_1(all_0_13_13) % 10.43/3.07 | (98) v2_funct_1(all_0_5_5) % 10.43/3.07 | (99) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v1) | m2_relset_1(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.07 | (100) ~ v3_struct_0(all_0_13_13) % 10.43/3.07 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v5 = v1 | ~ (g3_lattices(v4, v5, v6) = v3) | ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | ? [v7] : (k2_zfmisc_1(v0, v0) = v7 & ( ~ m1_relset_1(v2, v7, v0) | ~ m1_relset_1(v1, v7, v0) | ~ v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, v7, v0)))) % 10.43/3.07 | (102) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_lattices(v1) | v3_struct_0(v0)) % 10.43/3.07 | (103) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v1) | v1_funct_2(v4, v2, v3) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.07 | (104) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k3_latsubgr(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ l1_group_1(v1) | ~ l1_group_1(v0) | ~ v4_group_1(v1) | ~ v4_group_1(v0) | ~ v3_group_1(v1) | ~ v3_group_1(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (k11_group_4(v1) = v8 & k11_group_4(v0) = v6 & u1_struct_0(v8) = v9 & u1_struct_0(v6) = v7 & u1_struct_0(v1) = v5 & u1_struct_0(v0) = v4 & ( ~ m1_relset_1(v2, v4, v5) | ~ v1_funct_2(v2, v4, v5) | (m2_relset_1(v3, v7, v9) & v1_funct_2(v3, v7, v9) & v1_funct_1(v3))))) % 10.43/3.07 | (105) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ m4_vectsp_8(v4, v0, v1) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v1_funct_1(v4) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.08 | (106) ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | ? [v2] : (v1_xboole_0(v2) & m1_subset_1(v2, v1))) % 10.43/3.08 | (107) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u2_lattices(v2) = v1) | ~ (u2_lattices(v2) = v0)) % 10.43/3.08 | (108) ! [v0] : ( ~ l3_lattices(v0) | l2_lattices(v0)) % 10.43/3.08 | (109) ! [v0] : ! [v1] : ! [v2] : ( ~ v1_xboole_0(v2) | ~ m1_relset_1(v2, v0, v1) | ~ v1_funct_2(v2, v0, v1) | ~ v1_funct_1(v2) | v1_xboole_0(v1) | v1_xboole_0(v0)) % 10.43/3.08 | (110) ! [v0] : ( ~ l3_lattices(v0) | l1_lattices(v0)) % 10.43/3.08 | (111) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v1) = v3) | ~ (u1_struct_0(v0) = v2) | ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v1) | v1_funct_1(v4) | v3_struct_0(v1) | v3_struct_0(v0)) % 10.43/3.08 | (112) ! [v0] : ! [v1] : ( ~ m1_subset_1(v0, v1) | v1_xboole_0(v1) | r2_hidden(v0, v1)) % 10.43/3.08 | (113) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | l3_lattices(v1) | v3_struct_0(v0)) % 10.43/3.08 | (114) ! [v0] : ! [v1] : ! [v2] : ( ~ v1_partfun1(v2, v0, v1) | ~ m1_relset_1(v2, v0, v1) | ~ v1_funct_1(v2) | v1_funct_2(v2, v0, v1)) % 10.91/3.08 | (115) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v8_lattices(v1) | v3_struct_0(v0)) % 10.91/3.08 | (116) ! [v0] : ! [v1] : ( ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v2] : m3_vectsp_8(v2, v0, v1)) % 10.91/3.08 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_zfmisc_1(v2) = v3) | ~ m1_subset_1(v1, v3) | ~ r2_hidden(v0, v1) | m1_subset_1(v0, v2)) % 10.91/3.08 | (118) ! [v0] : ! [v1] : ( ~ v10_lattices(v1) | ~ v10_lattices(v0) | ~ l3_lattices(v1) | ~ l3_lattices(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v2] : m1_lattice4(v2, v0, v1)) % 10.91/3.08 | (119) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v6_lattices(v1) | v3_struct_0(v0)) % 10.91/3.08 | (120) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_zfmisc_1(v2) = v3) | ~ v1_xboole_0(v2) | ~ m1_subset_1(v1, v3) | ~ r2_hidden(v0, v1)) % 10.91/3.08 | (121) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k2_zfmisc_1(v3, v2) = v1) | ~ (k2_zfmisc_1(v3, v2) = v0)) % 10.91/3.08 | (122) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | v1_funct_1(v1)) % 10.91/3.08 | (123) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (u1_struct_0(v2) = v3) | ~ (u1_struct_0(v0) = v1) | ~ v10_lattices(v2) | ~ v10_lattices(v0) | ~ l3_lattices(v2) | ~ l3_lattices(v0) | ~ m1_lattice4(v4, v0, v2) | ~ m2_relset_1(v4, v1, v3) | ~ v1_funct_2(v4, v1, v3) | ~ v1_funct_1(v4) | m3_vectsp_8(v4, v0, v2) | v3_struct_0(v2) | v3_struct_0(v0)) % 10.91/3.08 | (124) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (g3_lattices(v0, v1, v2) = v3) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | l3_lattices(v3) | ? [v4] : (k2_zfmisc_1(v0, v0) = v4 & ( ~ m1_relset_1(v2, v4, v0) | ~ m1_relset_1(v1, v4, v0) | ~ v1_funct_2(v2, v4, v0) | ~ v1_funct_2(v1, v4, v0)))) % 10.91/3.08 | % 10.91/3.08 | Instantiating formula (88) with all_0_10_10, all_0_12_12, all_0_15_15 and discharging atoms m2_relset_1(all_0_10_10, all_0_15_15, all_0_12_12), yields: % 10.91/3.08 | (125) m1_relset_1(all_0_10_10, all_0_15_15, all_0_12_12) % 10.91/3.08 | % 10.91/3.08 | Instantiating formula (4) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.91/3.08 | (126) v10_lattices(all_0_11_11) % 10.91/3.08 | % 10.91/3.08 | Instantiating formula (113) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.91/3.08 | (127) l3_lattices(all_0_11_11) % 10.91/3.08 | % 10.91/3.08 | Instantiating formula (33) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.91/3.08 | (128) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k11_group_4(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (u1_struct_0(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_13_13, v1, v4) = v5) | ~ v2_funct_1(v4) | ~ m2_relset_1(v4, v0, v3) | ~ v1_group_6(v4, all_0_13_13, v1) | ~ v1_funct_2(v4, v0, v3) | ~ v1_funct_1(v4) | m3_vectsp_8(v5, all_0_11_11, v2)))) & ! [v1] : ! [v2] : ( ~ (u1_struct_0(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (k11_group_4(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_13_13, v1, v4) = v5) | ~ v2_funct_1(v4) | ~ m2_relset_1(v4, v0, v2) | ~ v1_group_6(v4, all_0_13_13, v1) | ~ v1_funct_2(v4, v0, v2) | ~ v1_funct_1(v4) | m3_vectsp_8(v5, all_0_11_11, v3))))) % 10.91/3.08 | % 10.91/3.08 | Instantiating formula (14) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.91/3.08 | (129) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k11_group_4(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (u1_struct_0(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_13_13, v1, v4) = v5) | ~ m2_relset_1(v4, v0, v3) | ~ v1_group_6(v4, all_0_13_13, v1) | ~ v1_funct_2(v4, v0, v3) | ~ v1_funct_1(v4) | m4_vectsp_8(v5, all_0_11_11, v2)))) & ! [v1] : ! [v2] : ( ~ (u1_struct_0(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (k11_group_4(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_13_13, v1, v4) = v5) | ~ m2_relset_1(v4, v0, v2) | ~ v1_group_6(v4, all_0_13_13, v1) | ~ v1_funct_2(v4, v0, v2) | ~ v1_funct_1(v4) | m4_vectsp_8(v5, all_0_11_11, v3))))) % 10.91/3.08 | % 10.91/3.08 | Instantiating formula (82) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.91/3.08 | (130) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k11_group_4(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (u1_struct_0(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_13_13, v1, v4) = v5) | ~ v2_funct_1(v4) | ~ m2_relset_1(v4, all_0_12_12, v3) | ~ v1_group_6(v4, all_0_13_13, v1) | ~ v1_funct_2(v4, all_0_12_12, v3) | ~ v1_funct_1(v4) | m3_vectsp_8(v5, v0, v2)))) & ! [v1] : ! [v2] : ( ~ (u1_struct_0(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (k11_group_4(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_13_13, v1, v4) = v5) | ~ v2_funct_1(v4) | ~ m2_relset_1(v4, all_0_12_12, v2) | ~ v1_group_6(v4, all_0_13_13, v1) | ~ v1_funct_2(v4, all_0_12_12, v2) | ~ v1_funct_1(v4) | m3_vectsp_8(v5, v0, v3))))) % 10.91/3.08 | % 10.91/3.08 | Instantiating formula (44) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.91/3.08 | (131) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k11_group_4(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (u1_struct_0(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_13_13, v1, v4) = v5) | ~ m2_relset_1(v4, all_0_12_12, v3) | ~ v1_group_6(v4, all_0_13_13, v1) | ~ v1_funct_2(v4, all_0_12_12, v3) | ~ v1_funct_1(v4) | m4_vectsp_8(v5, v0, v2)))) & ! [v1] : ! [v2] : ( ~ (u1_struct_0(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (k11_group_4(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_13_13, v1, v4) = v5) | ~ m2_relset_1(v4, all_0_12_12, v2) | ~ v1_group_6(v4, all_0_13_13, v1) | ~ v1_funct_2(v4, all_0_12_12, v2) | ~ v1_funct_1(v4) | m4_vectsp_8(v5, v0, v3))))) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (104) with all_0_9_9, all_0_10_10, all_0_13_13, all_0_16_16 and discharging atoms k3_latsubgr(all_0_16_16, all_0_13_13, all_0_10_10) = all_0_9_9, v1_funct_1(all_0_10_10), l1_group_1(all_0_13_13), l1_group_1(all_0_16_16), v4_group_1(all_0_13_13), v4_group_1(all_0_16_16), v3_group_1(all_0_13_13), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_13_13), ~ v3_struct_0(all_0_16_16), yields: % 10.91/3.09 | (132) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (k11_group_4(all_0_13_13) = v4 & k11_group_4(all_0_16_16) = v2 & u1_struct_0(v4) = v5 & u1_struct_0(v2) = v3 & u1_struct_0(all_0_13_13) = v1 & u1_struct_0(all_0_16_16) = v0 & ( ~ m1_relset_1(all_0_10_10, v0, v1) | ~ v1_funct_2(all_0_10_10, v0, v1) | (m2_relset_1(all_0_9_9, v3, v5) & v1_funct_2(all_0_9_9, v3, v5) & v1_funct_1(all_0_9_9)))) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (4) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.91/3.09 | (133) v10_lattices(all_0_14_14) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (113) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.91/3.09 | (134) l3_lattices(all_0_14_14) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (33) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.91/3.09 | (135) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k11_group_4(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (u1_struct_0(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_16_16, v1, v4) = v5) | ~ v2_funct_1(v4) | ~ m2_relset_1(v4, v0, v3) | ~ v1_group_6(v4, all_0_16_16, v1) | ~ v1_funct_2(v4, v0, v3) | ~ v1_funct_1(v4) | m3_vectsp_8(v5, all_0_14_14, v2)))) & ! [v1] : ! [v2] : ( ~ (u1_struct_0(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (k11_group_4(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_16_16, v1, v4) = v5) | ~ v2_funct_1(v4) | ~ m2_relset_1(v4, v0, v2) | ~ v1_group_6(v4, all_0_16_16, v1) | ~ v1_funct_2(v4, v0, v2) | ~ v1_funct_1(v4) | m3_vectsp_8(v5, all_0_14_14, v3))))) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (14) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.91/3.09 | (136) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k11_group_4(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (u1_struct_0(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_16_16, v1, v4) = v5) | ~ m2_relset_1(v4, v0, v3) | ~ v1_group_6(v4, all_0_16_16, v1) | ~ v1_funct_2(v4, v0, v3) | ~ v1_funct_1(v4) | m4_vectsp_8(v5, all_0_14_14, v2)))) & ! [v1] : ! [v2] : ( ~ (u1_struct_0(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (k11_group_4(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_16_16, v1, v4) = v5) | ~ m2_relset_1(v4, v0, v2) | ~ v1_group_6(v4, all_0_16_16, v1) | ~ v1_funct_2(v4, v0, v2) | ~ v1_funct_1(v4) | m4_vectsp_8(v5, all_0_14_14, v3))))) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (82) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.91/3.09 | (137) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k11_group_4(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (u1_struct_0(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_16_16, v1, v4) = v5) | ~ v2_funct_1(v4) | ~ m2_relset_1(v4, all_0_15_15, v3) | ~ v1_group_6(v4, all_0_16_16, v1) | ~ v1_funct_2(v4, all_0_15_15, v3) | ~ v1_funct_1(v4) | m3_vectsp_8(v5, v0, v2)))) & ! [v1] : ! [v2] : ( ~ (u1_struct_0(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (k11_group_4(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_16_16, v1, v4) = v5) | ~ v2_funct_1(v4) | ~ m2_relset_1(v4, all_0_15_15, v2) | ~ v1_group_6(v4, all_0_16_16, v1) | ~ v1_funct_2(v4, all_0_15_15, v2) | ~ v1_funct_1(v4) | m3_vectsp_8(v5, v0, v3))))) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (44) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.91/3.09 | (138) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k11_group_4(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (u1_struct_0(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_16_16, v1, v4) = v5) | ~ m2_relset_1(v4, all_0_15_15, v3) | ~ v1_group_6(v4, all_0_16_16, v1) | ~ v1_funct_2(v4, all_0_15_15, v3) | ~ v1_funct_1(v4) | m4_vectsp_8(v5, v0, v2)))) & ! [v1] : ! [v2] : ( ~ (u1_struct_0(v1) = v2) | ~ l1_group_1(v1) | ~ v4_group_1(v1) | ~ v3_group_1(v1) | v3_struct_0(v1) | ? [v3] : (k11_group_4(v1) = v3 & ! [v4] : ! [v5] : ( ~ (k3_latsubgr(all_0_16_16, v1, v4) = v5) | ~ m2_relset_1(v4, all_0_15_15, v2) | ~ v1_group_6(v4, all_0_16_16, v1) | ~ v1_funct_2(v4, all_0_15_15, v2) | ~ v1_funct_1(v4) | m4_vectsp_8(v5, v0, v3))))) % 10.91/3.09 | % 10.91/3.09 | Instantiating (132) with all_27_0_33, all_27_1_34, all_27_2_35, all_27_3_36, all_27_4_37, all_27_5_38 yields: % 10.91/3.09 | (139) k11_group_4(all_0_13_13) = all_27_1_34 & k11_group_4(all_0_16_16) = all_27_3_36 & u1_struct_0(all_27_1_34) = all_27_0_33 & u1_struct_0(all_27_3_36) = all_27_2_35 & u1_struct_0(all_0_13_13) = all_27_4_37 & u1_struct_0(all_0_16_16) = all_27_5_38 & ( ~ m1_relset_1(all_0_10_10, all_27_5_38, all_27_4_37) | ~ v1_funct_2(all_0_10_10, all_27_5_38, all_27_4_37) | (m2_relset_1(all_0_9_9, all_27_2_35, all_27_0_33) & v1_funct_2(all_0_9_9, all_27_2_35, all_27_0_33) & v1_funct_1(all_0_9_9))) % 10.91/3.09 | % 10.91/3.09 | Applying alpha-rule on (139) yields: % 10.91/3.09 | (140) u1_struct_0(all_27_1_34) = all_27_0_33 % 10.91/3.09 | (141) ~ m1_relset_1(all_0_10_10, all_27_5_38, all_27_4_37) | ~ v1_funct_2(all_0_10_10, all_27_5_38, all_27_4_37) | (m2_relset_1(all_0_9_9, all_27_2_35, all_27_0_33) & v1_funct_2(all_0_9_9, all_27_2_35, all_27_0_33) & v1_funct_1(all_0_9_9)) % 10.91/3.09 | (142) k11_group_4(all_0_16_16) = all_27_3_36 % 10.91/3.09 | (143) u1_struct_0(all_0_13_13) = all_27_4_37 % 10.91/3.09 | (144) k11_group_4(all_0_13_13) = all_27_1_34 % 10.91/3.09 | (145) u1_struct_0(all_0_16_16) = all_27_5_38 % 10.91/3.09 | (146) u1_struct_0(all_27_3_36) = all_27_2_35 % 10.91/3.09 | % 10.91/3.09 | Instantiating (131) with all_29_0_39 yields: % 10.91/3.09 | (147) k11_group_4(all_0_13_13) = all_29_0_39 & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ m2_relset_1(v3, all_0_12_12, v2) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_0_12_12, v2) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_29_0_39, v1)))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ m2_relset_1(v3, all_0_12_12, v1) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_0_12_12, v1) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_29_0_39, v2)))) % 10.91/3.09 | % 10.91/3.09 | Applying alpha-rule on (147) yields: % 10.91/3.09 | (148) k11_group_4(all_0_13_13) = all_29_0_39 % 10.91/3.09 | (149) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ m2_relset_1(v3, all_0_12_12, v2) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_0_12_12, v2) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_29_0_39, v1)))) % 10.91/3.09 | (150) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ m2_relset_1(v3, all_0_12_12, v1) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_0_12_12, v1) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_29_0_39, v2)))) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (149) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.91/3.09 | (151) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v1) = v2) | ~ m2_relset_1(v1, all_0_12_12, v0) | ~ v1_group_6(v1, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v1, all_0_12_12, v0) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_29_0_39, all_0_11_11))) % 10.91/3.09 | % 10.91/3.09 | Instantiating formula (150) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.10 | (152) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v1) = v2) | ~ m2_relset_1(v1, all_0_12_12, all_0_12_12) | ~ v1_group_6(v1, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v1, all_0_12_12, all_0_12_12) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_29_0_39, v0))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (149) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.10 | (153) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v1) = v2) | ~ m2_relset_1(v1, all_0_12_12, v0) | ~ v1_group_6(v1, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v1, all_0_12_12, v0) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_29_0_39, all_0_14_14))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (150) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.10 | (154) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v1) = v2) | ~ m2_relset_1(v1, all_0_12_12, all_0_15_15) | ~ v1_group_6(v1, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v1, all_0_12_12, all_0_15_15) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_29_0_39, v0))) % 10.99/3.10 | % 10.99/3.10 | Instantiating (128) with all_32_0_40 yields: % 10.99/3.10 | (155) u1_struct_0(all_0_13_13) = all_32_0_40 & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_32_0_40, v2) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_32_0_40, v2) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_0_11_11, v1)))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_32_0_40, v1) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_32_0_40, v1) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_0_11_11, v2)))) % 10.99/3.10 | % 10.99/3.10 | Applying alpha-rule on (155) yields: % 10.99/3.10 | (156) u1_struct_0(all_0_13_13) = all_32_0_40 % 10.99/3.10 | (157) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_32_0_40, v2) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_32_0_40, v2) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_0_11_11, v1)))) % 10.99/3.10 | (158) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_32_0_40, v1) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_32_0_40, v1) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_0_11_11, v2)))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (157) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.10 | (159) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_32_0_40, v0) | ~ v1_group_6(v1, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v1, all_32_0_40, v0) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_0_11_11, all_0_11_11))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (158) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.10 | (160) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_32_0_40, all_0_12_12) | ~ v1_group_6(v1, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v1, all_32_0_40, all_0_12_12) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_0_11_11, v0))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (157) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.10 | (161) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_32_0_40, v0) | ~ v1_group_6(v1, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v1, all_32_0_40, v0) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_0_11_11, all_0_14_14))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (158) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.10 | (162) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_32_0_40, all_0_15_15) | ~ v1_group_6(v1, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v1, all_32_0_40, all_0_15_15) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_0_11_11, v0))) % 10.99/3.10 | % 10.99/3.10 | Instantiating (130) with all_35_0_41 yields: % 10.99/3.10 | (163) k11_group_4(all_0_13_13) = all_35_0_41 & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_0_12_12, v2) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_0_12_12, v2) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_35_0_41, v1)))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_0_12_12, v1) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_0_12_12, v1) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_35_0_41, v2)))) % 10.99/3.10 | % 10.99/3.10 | Applying alpha-rule on (163) yields: % 10.99/3.10 | (164) k11_group_4(all_0_13_13) = all_35_0_41 % 10.99/3.10 | (165) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_0_12_12, v2) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_0_12_12, v2) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_35_0_41, v1)))) % 10.99/3.10 | (166) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_0_12_12, v1) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_0_12_12, v1) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_35_0_41, v2)))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (165) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.10 | (167) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_0_12_12, v0) | ~ v1_group_6(v1, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v1, all_0_12_12, v0) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_35_0_41, all_0_11_11))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (166) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.10 | (168) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_0_12_12, all_0_12_12) | ~ v1_group_6(v1, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v1, all_0_12_12, all_0_12_12) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_35_0_41, v0))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (165) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.10 | (169) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_0_12_12, v0) | ~ v1_group_6(v1, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v1, all_0_12_12, v0) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_35_0_41, all_0_14_14))) % 10.99/3.10 | % 10.99/3.10 | Instantiating formula (166) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.10 | (170) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_0_12_12, all_0_15_15) | ~ v1_group_6(v1, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v1, all_0_12_12, all_0_15_15) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_35_0_41, v0))) % 10.99/3.10 | % 10.99/3.10 | Instantiating (129) with all_38_0_42 yields: % 10.99/3.10 | (171) u1_struct_0(all_0_13_13) = all_38_0_42 & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ m2_relset_1(v3, all_38_0_42, v2) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_38_0_42, v2) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_0_11_11, v1)))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ m2_relset_1(v3, all_38_0_42, v1) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_38_0_42, v1) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_0_11_11, v2)))) % 10.99/3.11 | % 10.99/3.11 | Applying alpha-rule on (171) yields: % 10.99/3.11 | (172) u1_struct_0(all_0_13_13) = all_38_0_42 % 10.99/3.11 | (173) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ m2_relset_1(v3, all_38_0_42, v2) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_38_0_42, v2) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_0_11_11, v1)))) % 10.99/3.11 | (174) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_13_13, v0, v3) = v4) | ~ m2_relset_1(v3, all_38_0_42, v1) | ~ v1_group_6(v3, all_0_13_13, v0) | ~ v1_funct_2(v3, all_38_0_42, v1) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_0_11_11, v2)))) % 10.99/3.11 | % 10.99/3.11 | Instantiating formula (173) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.11 | (175) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v1) = v2) | ~ m2_relset_1(v1, all_38_0_42, v0) | ~ v1_group_6(v1, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v1, all_38_0_42, v0) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_0_11_11, all_0_11_11))) % 10.99/3.11 | % 10.99/3.11 | Instantiating formula (174) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.11 | (176) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v1) = v2) | ~ m2_relset_1(v1, all_38_0_42, all_0_12_12) | ~ v1_group_6(v1, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v1, all_38_0_42, all_0_12_12) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_0_11_11, v0))) % 10.99/3.11 | % 10.99/3.11 | Instantiating formula (173) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.11 | (177) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v1) = v2) | ~ m2_relset_1(v1, all_38_0_42, v0) | ~ v1_group_6(v1, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v1, all_38_0_42, v0) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_0_11_11, all_0_14_14))) % 10.99/3.11 | % 10.99/3.11 | Instantiating formula (174) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.11 | (178) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v1) = v2) | ~ m2_relset_1(v1, all_38_0_42, all_0_15_15) | ~ v1_group_6(v1, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v1, all_38_0_42, all_0_15_15) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_0_11_11, v0))) % 10.99/3.11 | % 10.99/3.11 | Instantiating (138) with all_41_0_43 yields: % 10.99/3.11 | (179) k11_group_4(all_0_16_16) = all_41_0_43 & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ m2_relset_1(v3, all_0_15_15, v2) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_0_15_15, v2) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_41_0_43, v1)))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ m2_relset_1(v3, all_0_15_15, v1) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_0_15_15, v1) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_41_0_43, v2)))) % 10.99/3.11 | % 10.99/3.11 | Applying alpha-rule on (179) yields: % 10.99/3.11 | (180) k11_group_4(all_0_16_16) = all_41_0_43 % 10.99/3.11 | (181) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ m2_relset_1(v3, all_0_15_15, v2) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_0_15_15, v2) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_41_0_43, v1)))) % 10.99/3.11 | (182) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ m2_relset_1(v3, all_0_15_15, v1) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_0_15_15, v1) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_41_0_43, v2)))) % 10.99/3.11 | % 10.99/3.11 | Instantiating formula (181) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.11 | (183) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v1) = v2) | ~ m2_relset_1(v1, all_0_15_15, v0) | ~ v1_group_6(v1, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v1, all_0_15_15, v0) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_41_0_43, all_0_11_11))) % 10.99/3.11 | % 10.99/3.11 | Instantiating formula (182) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 10.99/3.11 | (184) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v1) = v2) | ~ m2_relset_1(v1, all_0_15_15, all_0_12_12) | ~ v1_group_6(v1, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v1, all_0_15_15, all_0_12_12) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_41_0_43, v0))) % 10.99/3.11 | % 10.99/3.11 | Instantiating formula (181) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.11 | (185) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v1) = v2) | ~ m2_relset_1(v1, all_0_15_15, v0) | ~ v1_group_6(v1, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v1, all_0_15_15, v0) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_41_0_43, all_0_14_14))) % 10.99/3.11 | % 10.99/3.11 | Instantiating formula (182) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 10.99/3.11 | (186) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v1) = v2) | ~ m2_relset_1(v1, all_0_15_15, all_0_15_15) | ~ v1_group_6(v1, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v1, all_0_15_15, all_0_15_15) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_41_0_43, v0))) % 10.99/3.11 | % 10.99/3.11 | Instantiating (137) with all_44_0_44 yields: % 10.99/3.11 | (187) k11_group_4(all_0_16_16) = all_44_0_44 & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_0_15_15, v2) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_0_15_15, v2) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_44_0_44, v1)))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_0_15_15, v1) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_0_15_15, v1) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_44_0_44, v2)))) % 10.99/3.11 | % 10.99/3.11 | Applying alpha-rule on (187) yields: % 10.99/3.11 | (188) k11_group_4(all_0_16_16) = all_44_0_44 % 10.99/3.11 | (189) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_0_15_15, v2) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_0_15_15, v2) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_44_0_44, v1)))) % 10.99/3.11 | (190) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_0_15_15, v1) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_0_15_15, v1) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_44_0_44, v2)))) % 11.07/3.11 | % 11.07/3.11 | Instantiating formula (189) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 11.07/3.11 | (191) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_0_15_15, v0) | ~ v1_group_6(v1, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v1, all_0_15_15, v0) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_44_0_44, all_0_11_11))) % 11.07/3.11 | % 11.07/3.12 | Instantiating formula (190) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 11.07/3.12 | (192) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_0_15_15, all_0_12_12) | ~ v1_group_6(v1, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v1, all_0_15_15, all_0_12_12) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_44_0_44, v0))) % 11.07/3.12 | % 11.07/3.12 | Instantiating formula (189) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 11.07/3.12 | (193) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_0_15_15, v0) | ~ v1_group_6(v1, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v1, all_0_15_15, v0) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_44_0_44, all_0_14_14))) % 11.07/3.12 | % 11.07/3.12 | Instantiating formula (190) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 11.08/3.12 | (194) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_0_15_15, all_0_15_15) | ~ v1_group_6(v1, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v1, all_0_15_15, all_0_15_15) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_44_0_44, v0))) % 11.08/3.12 | % 11.08/3.12 | Instantiating (136) with all_47_0_45 yields: % 11.08/3.12 | (195) u1_struct_0(all_0_16_16) = all_47_0_45 & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ m2_relset_1(v3, all_47_0_45, v2) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_47_0_45, v2) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_0_14_14, v1)))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ m2_relset_1(v3, all_47_0_45, v1) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_47_0_45, v1) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_0_14_14, v2)))) % 11.08/3.12 | % 11.08/3.12 | Applying alpha-rule on (195) yields: % 11.08/3.12 | (196) u1_struct_0(all_0_16_16) = all_47_0_45 % 11.08/3.12 | (197) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ m2_relset_1(v3, all_47_0_45, v2) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_47_0_45, v2) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_0_14_14, v1)))) % 11.08/3.12 | (198) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ m2_relset_1(v3, all_47_0_45, v1) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_47_0_45, v1) | ~ v1_funct_1(v3) | m4_vectsp_8(v4, all_0_14_14, v2)))) % 11.08/3.12 | % 11.08/3.12 | Instantiating formula (197) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 11.08/3.12 | (199) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v1) = v2) | ~ m2_relset_1(v1, all_47_0_45, v0) | ~ v1_group_6(v1, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v1, all_47_0_45, v0) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_0_14_14, all_0_11_11))) % 11.08/3.12 | % 11.08/3.12 | Instantiating formula (198) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 11.08/3.12 | (200) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v1) = v2) | ~ m2_relset_1(v1, all_47_0_45, all_0_12_12) | ~ v1_group_6(v1, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v1, all_47_0_45, all_0_12_12) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_0_14_14, v0))) % 11.08/3.12 | % 11.08/3.12 | Instantiating formula (197) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 11.08/3.12 | (201) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v1) = v2) | ~ m2_relset_1(v1, all_47_0_45, v0) | ~ v1_group_6(v1, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v1, all_47_0_45, v0) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_0_14_14, all_0_14_14))) % 11.08/3.12 | % 11.08/3.12 | Instantiating formula (198) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 11.08/3.12 | (202) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v1) = v2) | ~ m2_relset_1(v1, all_47_0_45, all_0_15_15) | ~ v1_group_6(v1, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v1, all_47_0_45, all_0_15_15) | ~ v1_funct_1(v1) | m4_vectsp_8(v2, all_0_14_14, v0))) % 11.08/3.12 | % 11.08/3.12 | Instantiating (135) with all_50_0_46 yields: % 11.08/3.12 | (203) u1_struct_0(all_0_16_16) = all_50_0_46 & ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_50_0_46, v2) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_50_0_46, v2) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_0_14_14, v1)))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_50_0_46, v1) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_50_0_46, v1) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_0_14_14, v2)))) % 11.08/3.12 | % 11.08/3.12 | Applying alpha-rule on (203) yields: % 11.08/3.12 | (204) u1_struct_0(all_0_16_16) = all_50_0_46 % 11.08/3.12 | (205) ! [v0] : ! [v1] : ( ~ (k11_group_4(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (u1_struct_0(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_50_0_46, v2) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_50_0_46, v2) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_0_14_14, v1)))) % 11.08/3.12 | (206) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_group_1(v0) | ~ v4_group_1(v0) | ~ v3_group_1(v0) | v3_struct_0(v0) | ? [v2] : (k11_group_4(v0) = v2 & ! [v3] : ! [v4] : ( ~ (k3_latsubgr(all_0_16_16, v0, v3) = v4) | ~ v2_funct_1(v3) | ~ m2_relset_1(v3, all_50_0_46, v1) | ~ v1_group_6(v3, all_0_16_16, v0) | ~ v1_funct_2(v3, all_50_0_46, v1) | ~ v1_funct_1(v3) | m3_vectsp_8(v4, all_0_14_14, v2)))) % 11.08/3.12 | % 11.08/3.12 | Instantiating formula (205) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 11.08/3.12 | (207) ? [v0] : (u1_struct_0(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_50_0_46, v0) | ~ v1_group_6(v1, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v1, all_50_0_46, v0) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_0_14_14, all_0_11_11))) % 11.08/3.12 | % 11.08/3.12 | Instantiating formula (206) with all_0_12_12, all_0_13_13 and discharging atoms u1_struct_0(all_0_13_13) = all_0_12_12, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), ~ v3_struct_0(all_0_13_13), yields: % 11.08/3.12 | (208) ? [v0] : (k11_group_4(all_0_13_13) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_50_0_46, all_0_12_12) | ~ v1_group_6(v1, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v1, all_50_0_46, all_0_12_12) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_0_14_14, v0))) % 11.08/3.12 | % 11.08/3.12 | Instantiating formula (205) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 11.08/3.12 | (209) ? [v0] : (u1_struct_0(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_50_0_46, v0) | ~ v1_group_6(v1, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v1, all_50_0_46, v0) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_0_14_14, all_0_14_14))) % 11.08/3.12 | % 11.08/3.12 | Instantiating formula (206) with all_0_15_15, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_0_15_15, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 11.08/3.12 | (210) ? [v0] : (k11_group_4(all_0_16_16) = v0 & ! [v1] : ! [v2] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v1) = v2) | ~ v2_funct_1(v1) | ~ m2_relset_1(v1, all_50_0_46, all_0_15_15) | ~ v1_group_6(v1, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v1, all_50_0_46, all_0_15_15) | ~ v1_funct_1(v1) | m3_vectsp_8(v2, all_0_14_14, v0))) % 11.08/3.13 | % 11.08/3.13 | Instantiating (154) with all_53_0_47 yields: % 11.08/3.13 | (211) k11_group_4(all_0_16_16) = all_53_0_47 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_0_12_12, all_0_15_15) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_0_12_12, all_0_15_15) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_29_0_39, all_53_0_47)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (211) yields: % 11.08/3.13 | (212) k11_group_4(all_0_16_16) = all_53_0_47 % 11.08/3.13 | (213) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_0_12_12, all_0_15_15) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_0_12_12, all_0_15_15) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_29_0_39, all_53_0_47)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (153) with all_56_0_48 yields: % 11.08/3.13 | (214) u1_struct_0(all_0_16_16) = all_56_0_48 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_0_12_12, all_56_0_48) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_0_12_12, all_56_0_48) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_29_0_39, all_0_14_14)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (214) yields: % 11.08/3.13 | (215) u1_struct_0(all_0_16_16) = all_56_0_48 % 11.08/3.13 | (216) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_0_12_12, all_56_0_48) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_0_12_12, all_56_0_48) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_29_0_39, all_0_14_14)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (152) with all_59_0_49 yields: % 11.08/3.13 | (217) k11_group_4(all_0_13_13) = all_59_0_49 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_0_12_12, all_0_12_12) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_0_12_12, all_0_12_12) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_29_0_39, all_59_0_49)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (217) yields: % 11.08/3.13 | (218) k11_group_4(all_0_13_13) = all_59_0_49 % 11.08/3.13 | (219) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_0_12_12, all_0_12_12) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_0_12_12, all_0_12_12) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_29_0_39, all_59_0_49)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (151) with all_62_0_50 yields: % 11.08/3.13 | (220) u1_struct_0(all_0_13_13) = all_62_0_50 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_0_12_12, all_62_0_50) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_0_12_12, all_62_0_50) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_29_0_39, all_0_11_11)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (220) yields: % 11.08/3.13 | (221) u1_struct_0(all_0_13_13) = all_62_0_50 % 11.08/3.13 | (222) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_0_12_12, all_62_0_50) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_0_12_12, all_62_0_50) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_29_0_39, all_0_11_11)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (162) with all_65_0_51 yields: % 11.08/3.13 | (223) k11_group_4(all_0_16_16) = all_65_0_51 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_32_0_40, all_0_15_15) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_32_0_40, all_0_15_15) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_11_11, all_65_0_51)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (223) yields: % 11.08/3.13 | (224) k11_group_4(all_0_16_16) = all_65_0_51 % 11.08/3.13 | (225) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_32_0_40, all_0_15_15) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_32_0_40, all_0_15_15) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_11_11, all_65_0_51)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (160) with all_68_0_52 yields: % 11.08/3.13 | (226) k11_group_4(all_0_13_13) = all_68_0_52 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_32_0_40, all_0_12_12) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_32_0_40, all_0_12_12) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_11_11, all_68_0_52)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (226) yields: % 11.08/3.13 | (227) k11_group_4(all_0_13_13) = all_68_0_52 % 11.08/3.13 | (228) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_32_0_40, all_0_12_12) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_32_0_40, all_0_12_12) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_11_11, all_68_0_52)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (159) with all_71_0_53 yields: % 11.08/3.13 | (229) u1_struct_0(all_0_13_13) = all_71_0_53 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_32_0_40, all_71_0_53) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_32_0_40, all_71_0_53) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_11_11, all_0_11_11)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (229) yields: % 11.08/3.13 | (230) u1_struct_0(all_0_13_13) = all_71_0_53 % 11.08/3.13 | (231) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_32_0_40, all_71_0_53) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_32_0_40, all_71_0_53) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_11_11, all_0_11_11)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (161) with all_74_0_54 yields: % 11.08/3.13 | (232) u1_struct_0(all_0_16_16) = all_74_0_54 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_32_0_40, all_74_0_54) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_32_0_40, all_74_0_54) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_11_11, all_0_14_14)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (232) yields: % 11.08/3.13 | (233) u1_struct_0(all_0_16_16) = all_74_0_54 % 11.08/3.13 | (234) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_32_0_40, all_74_0_54) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_32_0_40, all_74_0_54) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_11_11, all_0_14_14)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (170) with all_77_0_55 yields: % 11.08/3.13 | (235) k11_group_4(all_0_16_16) = all_77_0_55 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_12_12, all_0_15_15) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_0_12_12, all_0_15_15) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_35_0_41, all_77_0_55)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (235) yields: % 11.08/3.13 | (236) k11_group_4(all_0_16_16) = all_77_0_55 % 11.08/3.13 | (237) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_12_12, all_0_15_15) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_0_12_12, all_0_15_15) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_35_0_41, all_77_0_55)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (168) with all_80_0_56 yields: % 11.08/3.13 | (238) k11_group_4(all_0_13_13) = all_80_0_56 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_12_12, all_0_12_12) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_0_12_12, all_0_12_12) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_35_0_41, all_80_0_56)) % 11.08/3.13 | % 11.08/3.13 | Applying alpha-rule on (238) yields: % 11.08/3.13 | (239) k11_group_4(all_0_13_13) = all_80_0_56 % 11.08/3.13 | (240) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_12_12, all_0_12_12) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_0_12_12, all_0_12_12) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_35_0_41, all_80_0_56)) % 11.08/3.13 | % 11.08/3.13 | Instantiating (167) with all_83_0_57 yields: % 11.08/3.13 | (241) u1_struct_0(all_0_13_13) = all_83_0_57 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_12_12, all_83_0_57) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_0_12_12, all_83_0_57) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_35_0_41, all_0_11_11)) % 11.08/3.15 | % 11.08/3.15 | Applying alpha-rule on (241) yields: % 11.08/3.15 | (242) u1_struct_0(all_0_13_13) = all_83_0_57 % 11.08/3.15 | (243) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_12_12, all_83_0_57) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_0_12_12, all_83_0_57) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_35_0_41, all_0_11_11)) % 11.08/3.15 | % 11.08/3.15 | Instantiating (169) with all_86_0_58 yields: % 11.08/3.15 | (244) u1_struct_0(all_0_16_16) = all_86_0_58 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_12_12, all_86_0_58) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_0_12_12, all_86_0_58) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_35_0_41, all_0_14_14)) % 11.08/3.15 | % 11.08/3.15 | Applying alpha-rule on (244) yields: % 11.08/3.15 | (245) u1_struct_0(all_0_16_16) = all_86_0_58 % 11.08/3.15 | (246) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_12_12, all_86_0_58) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_0_12_12, all_86_0_58) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_35_0_41, all_0_14_14)) % 11.08/3.15 | % 11.08/3.15 | Instantiating (178) with all_89_0_59 yields: % 11.08/3.15 | (247) k11_group_4(all_0_16_16) = all_89_0_59 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_38_0_42, all_0_15_15) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_38_0_42, all_0_15_15) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_11_11, all_89_0_59)) % 11.08/3.15 | % 11.08/3.15 | Applying alpha-rule on (247) yields: % 11.08/3.15 | (248) k11_group_4(all_0_16_16) = all_89_0_59 % 11.08/3.15 | (249) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_38_0_42, all_0_15_15) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_38_0_42, all_0_15_15) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_11_11, all_89_0_59)) % 11.08/3.15 | % 11.08/3.15 | Instantiating (176) with all_92_0_60 yields: % 11.08/3.15 | (250) k11_group_4(all_0_13_13) = all_92_0_60 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_38_0_42, all_0_12_12) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_38_0_42, all_0_12_12) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_11_11, all_92_0_60)) % 11.08/3.15 | % 11.08/3.15 | Applying alpha-rule on (250) yields: % 11.08/3.15 | (251) k11_group_4(all_0_13_13) = all_92_0_60 % 11.08/3.15 | (252) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_38_0_42, all_0_12_12) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_38_0_42, all_0_12_12) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_11_11, all_92_0_60)) % 11.08/3.15 | % 11.08/3.15 | Instantiating (177) with all_95_0_61 yields: % 11.08/3.15 | (253) u1_struct_0(all_0_16_16) = all_95_0_61 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_38_0_42, all_95_0_61) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_38_0_42, all_95_0_61) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_11_11, all_0_14_14)) % 11.08/3.15 | % 11.08/3.15 | Applying alpha-rule on (253) yields: % 11.08/3.15 | (254) u1_struct_0(all_0_16_16) = all_95_0_61 % 11.08/3.15 | (255) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_38_0_42, all_95_0_61) | ~ v1_group_6(v0, all_0_13_13, all_0_16_16) | ~ v1_funct_2(v0, all_38_0_42, all_95_0_61) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_11_11, all_0_14_14)) % 11.08/3.15 | % 11.08/3.15 | Instantiating (175) with all_98_0_62 yields: % 11.08/3.15 | (256) u1_struct_0(all_0_13_13) = all_98_0_62 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_38_0_42, all_98_0_62) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_38_0_42, all_98_0_62) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_11_11, all_0_11_11)) % 11.08/3.15 | % 11.08/3.15 | Applying alpha-rule on (256) yields: % 11.08/3.15 | (257) u1_struct_0(all_0_13_13) = all_98_0_62 % 11.08/3.15 | (258) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_13_13, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_38_0_42, all_98_0_62) | ~ v1_group_6(v0, all_0_13_13, all_0_13_13) | ~ v1_funct_2(v0, all_38_0_42, all_98_0_62) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_11_11, all_0_11_11)) % 11.08/3.15 | % 11.08/3.15 | Instantiating (186) with all_101_0_63 yields: % 11.08/3.15 | (259) k11_group_4(all_0_16_16) = all_101_0_63 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_0_15_15, all_0_15_15) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_0_15_15, all_0_15_15) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_41_0_43, all_101_0_63)) % 11.08/3.15 | % 11.08/3.15 | Applying alpha-rule on (259) yields: % 11.08/3.15 | (260) k11_group_4(all_0_16_16) = all_101_0_63 % 11.08/3.15 | (261) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_0_15_15, all_0_15_15) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_0_15_15, all_0_15_15) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_41_0_43, all_101_0_63)) % 11.08/3.15 | % 11.08/3.15 | Instantiating (185) with all_104_0_64 yields: % 11.08/3.15 | (262) u1_struct_0(all_0_16_16) = all_104_0_64 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_0_15_15, all_104_0_64) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_0_15_15, all_104_0_64) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_41_0_43, all_0_14_14)) % 11.08/3.16 | % 11.08/3.16 | Applying alpha-rule on (262) yields: % 11.08/3.16 | (263) u1_struct_0(all_0_16_16) = all_104_0_64 % 11.08/3.16 | (264) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_0_15_15, all_104_0_64) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_0_15_15, all_104_0_64) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_41_0_43, all_0_14_14)) % 11.08/3.16 | % 11.08/3.16 | Instantiating (184) with all_107_0_65 yields: % 11.08/3.16 | (265) k11_group_4(all_0_13_13) = all_107_0_65 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_0_15_15, all_0_12_12) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_0_15_15, all_0_12_12) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_41_0_43, all_107_0_65)) % 11.08/3.16 | % 11.08/3.16 | Applying alpha-rule on (265) yields: % 11.08/3.16 | (266) k11_group_4(all_0_13_13) = all_107_0_65 % 11.08/3.16 | (267) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_0_15_15, all_0_12_12) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_0_15_15, all_0_12_12) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_41_0_43, all_107_0_65)) % 11.08/3.16 | % 11.08/3.16 | Instantiating formula (267) with all_0_9_9, all_0_10_10 and discharging atoms k3_latsubgr(all_0_16_16, all_0_13_13, all_0_10_10) = all_0_9_9, m2_relset_1(all_0_10_10, all_0_15_15, all_0_12_12), v1_group_6(all_0_10_10, all_0_16_16, all_0_13_13), v1_funct_2(all_0_10_10, all_0_15_15, all_0_12_12), v1_funct_1(all_0_10_10), yields: % 11.08/3.16 | (268) m4_vectsp_8(all_0_9_9, all_41_0_43, all_107_0_65) % 11.08/3.16 | % 11.08/3.16 | Instantiating (183) with all_111_0_66 yields: % 11.08/3.16 | (269) u1_struct_0(all_0_13_13) = all_111_0_66 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_0_15_15, all_111_0_66) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_0_15_15, all_111_0_66) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_41_0_43, all_0_11_11)) % 11.08/3.16 | % 11.08/3.16 | Applying alpha-rule on (269) yields: % 11.08/3.16 | (270) u1_struct_0(all_0_13_13) = all_111_0_66 % 11.08/3.16 | (271) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_0_15_15, all_111_0_66) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_0_15_15, all_111_0_66) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_41_0_43, all_0_11_11)) % 11.08/3.16 | % 11.08/3.16 | Instantiating (194) with all_114_0_67 yields: % 11.08/3.16 | (272) k11_group_4(all_0_16_16) = all_114_0_67 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_15_15, all_0_15_15) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_0_15_15, all_0_15_15) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_44_0_44, all_114_0_67)) % 11.08/3.16 | % 11.08/3.16 | Applying alpha-rule on (272) yields: % 11.08/3.16 | (273) k11_group_4(all_0_16_16) = all_114_0_67 % 11.08/3.16 | (274) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_15_15, all_0_15_15) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_0_15_15, all_0_15_15) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_44_0_44, all_114_0_67)) % 11.08/3.16 | % 11.08/3.16 | Instantiating (192) with all_117_0_68 yields: % 11.08/3.16 | (275) k11_group_4(all_0_13_13) = all_117_0_68 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_15_15, all_0_12_12) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_0_15_15, all_0_12_12) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_44_0_44, all_117_0_68)) % 11.08/3.16 | % 11.08/3.16 | Applying alpha-rule on (275) yields: % 11.08/3.16 | (276) k11_group_4(all_0_13_13) = all_117_0_68 % 11.08/3.16 | (277) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_15_15, all_0_12_12) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_0_15_15, all_0_12_12) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_44_0_44, all_117_0_68)) % 11.08/3.16 | % 11.08/3.16 | Instantiating formula (277) with all_0_9_9, all_0_10_10 and discharging atoms k3_latsubgr(all_0_16_16, all_0_13_13, all_0_10_10) = all_0_9_9, v2_funct_1(all_0_10_10), m2_relset_1(all_0_10_10, all_0_15_15, all_0_12_12), v1_group_6(all_0_10_10, all_0_16_16, all_0_13_13), v1_funct_2(all_0_10_10, all_0_15_15, all_0_12_12), v1_funct_1(all_0_10_10), yields: % 11.08/3.16 | (278) m3_vectsp_8(all_0_9_9, all_44_0_44, all_117_0_68) % 11.08/3.16 | % 11.08/3.16 | Instantiating (191) with all_121_0_69 yields: % 11.08/3.16 | (279) u1_struct_0(all_0_13_13) = all_121_0_69 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_15_15, all_121_0_69) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_0_15_15, all_121_0_69) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_44_0_44, all_0_11_11)) % 11.08/3.16 | % 11.08/3.16 | Applying alpha-rule on (279) yields: % 11.08/3.16 | (280) u1_struct_0(all_0_13_13) = all_121_0_69 % 11.08/3.16 | (281) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_15_15, all_121_0_69) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_0_15_15, all_121_0_69) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_44_0_44, all_0_11_11)) % 11.08/3.16 | % 11.08/3.16 | Instantiating (193) with all_124_0_70 yields: % 11.08/3.16 | (282) u1_struct_0(all_0_16_16) = all_124_0_70 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_15_15, all_124_0_70) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_0_15_15, all_124_0_70) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_44_0_44, all_0_14_14)) % 11.08/3.17 | % 11.08/3.17 | Applying alpha-rule on (282) yields: % 11.08/3.17 | (283) u1_struct_0(all_0_16_16) = all_124_0_70 % 11.08/3.17 | (284) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_0_15_15, all_124_0_70) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_0_15_15, all_124_0_70) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_44_0_44, all_0_14_14)) % 11.08/3.17 | % 11.08/3.17 | Instantiating (202) with all_127_0_71 yields: % 11.08/3.17 | (285) k11_group_4(all_0_16_16) = all_127_0_71 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_47_0_45, all_0_15_15) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_47_0_45, all_0_15_15) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_14_14, all_127_0_71)) % 11.08/3.17 | % 11.08/3.17 | Applying alpha-rule on (285) yields: % 11.08/3.17 | (286) k11_group_4(all_0_16_16) = all_127_0_71 % 11.08/3.17 | (287) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_47_0_45, all_0_15_15) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_47_0_45, all_0_15_15) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_14_14, all_127_0_71)) % 11.08/3.17 | % 11.08/3.17 | Instantiating (201) with all_130_0_72 yields: % 11.08/3.17 | (288) u1_struct_0(all_0_16_16) = all_130_0_72 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_47_0_45, all_130_0_72) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_47_0_45, all_130_0_72) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_14_14, all_0_14_14)) % 11.08/3.17 | % 11.08/3.17 | Applying alpha-rule on (288) yields: % 11.08/3.17 | (289) u1_struct_0(all_0_16_16) = all_130_0_72 % 11.08/3.17 | (290) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ m2_relset_1(v0, all_47_0_45, all_130_0_72) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_47_0_45, all_130_0_72) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_14_14, all_0_14_14)) % 11.08/3.17 | % 11.08/3.17 | Instantiating (200) with all_133_0_73 yields: % 11.08/3.17 | (291) k11_group_4(all_0_13_13) = all_133_0_73 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_47_0_45, all_0_12_12) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_47_0_45, all_0_12_12) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_14_14, all_133_0_73)) % 11.08/3.17 | % 11.08/3.17 | Applying alpha-rule on (291) yields: % 11.08/3.17 | (292) k11_group_4(all_0_13_13) = all_133_0_73 % 11.08/3.17 | (293) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_47_0_45, all_0_12_12) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_47_0_45, all_0_12_12) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_14_14, all_133_0_73)) % 11.08/3.17 | % 11.08/3.17 | Instantiating (199) with all_136_0_74 yields: % 11.08/3.17 | (294) u1_struct_0(all_0_13_13) = all_136_0_74 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_47_0_45, all_136_0_74) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_47_0_45, all_136_0_74) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_14_14, all_0_11_11)) % 11.08/3.17 | % 11.08/3.17 | Applying alpha-rule on (294) yields: % 11.08/3.17 | (295) u1_struct_0(all_0_13_13) = all_136_0_74 % 11.08/3.17 | (296) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ m2_relset_1(v0, all_47_0_45, all_136_0_74) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_47_0_45, all_136_0_74) | ~ v1_funct_1(v0) | m4_vectsp_8(v1, all_0_14_14, all_0_11_11)) % 11.08/3.17 | % 11.08/3.17 | Instantiating (210) with all_139_0_75 yields: % 11.08/3.17 | (297) k11_group_4(all_0_16_16) = all_139_0_75 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_50_0_46, all_0_15_15) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_50_0_46, all_0_15_15) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_14_14, all_139_0_75)) % 11.08/3.17 | % 11.08/3.17 | Applying alpha-rule on (297) yields: % 11.08/3.17 | (298) k11_group_4(all_0_16_16) = all_139_0_75 % 11.08/3.17 | (299) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_50_0_46, all_0_15_15) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_50_0_46, all_0_15_15) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_14_14, all_139_0_75)) % 11.08/3.17 | % 11.08/3.17 | Instantiating (209) with all_142_0_76 yields: % 11.08/3.17 | (300) u1_struct_0(all_0_16_16) = all_142_0_76 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_50_0_46, all_142_0_76) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_50_0_46, all_142_0_76) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_14_14, all_0_14_14)) % 11.08/3.17 | % 11.08/3.17 | Applying alpha-rule on (300) yields: % 11.08/3.17 | (301) u1_struct_0(all_0_16_16) = all_142_0_76 % 11.08/3.17 | (302) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_16_16, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_50_0_46, all_142_0_76) | ~ v1_group_6(v0, all_0_16_16, all_0_16_16) | ~ v1_funct_2(v0, all_50_0_46, all_142_0_76) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_14_14, all_0_14_14)) % 11.08/3.17 | % 11.08/3.17 | Instantiating (208) with all_145_0_77 yields: % 11.08/3.17 | (303) k11_group_4(all_0_13_13) = all_145_0_77 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_50_0_46, all_0_12_12) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_50_0_46, all_0_12_12) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_14_14, all_145_0_77)) % 11.08/3.18 | % 11.08/3.18 | Applying alpha-rule on (303) yields: % 11.08/3.18 | (304) k11_group_4(all_0_13_13) = all_145_0_77 % 11.08/3.18 | (305) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_50_0_46, all_0_12_12) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_50_0_46, all_0_12_12) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_14_14, all_145_0_77)) % 11.08/3.18 | % 11.08/3.18 | Instantiating (207) with all_148_0_78 yields: % 11.08/3.18 | (306) u1_struct_0(all_0_13_13) = all_148_0_78 & ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_50_0_46, all_148_0_78) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_50_0_46, all_148_0_78) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_14_14, all_0_11_11)) % 11.08/3.18 | % 11.08/3.18 | Applying alpha-rule on (306) yields: % 11.08/3.18 | (307) u1_struct_0(all_0_13_13) = all_148_0_78 % 11.08/3.18 | (308) ! [v0] : ! [v1] : ( ~ (k3_latsubgr(all_0_16_16, all_0_13_13, v0) = v1) | ~ v2_funct_1(v0) | ~ m2_relset_1(v0, all_50_0_46, all_148_0_78) | ~ v1_group_6(v0, all_0_16_16, all_0_13_13) | ~ v1_funct_2(v0, all_50_0_46, all_148_0_78) | ~ v1_funct_1(v0) | m3_vectsp_8(v1, all_0_14_14, all_0_11_11)) % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_133_0_73, all_145_0_77 and discharging atoms k11_group_4(all_0_13_13) = all_145_0_77, k11_group_4(all_0_13_13) = all_133_0_73, yields: % 11.08/3.18 | (309) all_145_0_77 = all_133_0_73 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_117_0_68, all_133_0_73 and discharging atoms k11_group_4(all_0_13_13) = all_133_0_73, k11_group_4(all_0_13_13) = all_117_0_68, yields: % 11.08/3.18 | (310) all_133_0_73 = all_117_0_68 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_107_0_65, all_117_0_68 and discharging atoms k11_group_4(all_0_13_13) = all_117_0_68, k11_group_4(all_0_13_13) = all_107_0_65, yields: % 11.08/3.18 | (311) all_117_0_68 = all_107_0_65 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_92_0_60, all_0_11_11 and discharging atoms k11_group_4(all_0_13_13) = all_92_0_60, k11_group_4(all_0_13_13) = all_0_11_11, yields: % 11.08/3.18 | (312) all_92_0_60 = all_0_11_11 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_80_0_56, all_107_0_65 and discharging atoms k11_group_4(all_0_13_13) = all_107_0_65, k11_group_4(all_0_13_13) = all_80_0_56, yields: % 11.08/3.18 | (313) all_107_0_65 = all_80_0_56 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_68_0_52, all_80_0_56 and discharging atoms k11_group_4(all_0_13_13) = all_80_0_56, k11_group_4(all_0_13_13) = all_68_0_52, yields: % 11.08/3.18 | (314) all_80_0_56 = all_68_0_52 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_59_0_49, all_92_0_60 and discharging atoms k11_group_4(all_0_13_13) = all_92_0_60, k11_group_4(all_0_13_13) = all_59_0_49, yields: % 11.08/3.18 | (315) all_92_0_60 = all_59_0_49 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_59_0_49, all_68_0_52 and discharging atoms k11_group_4(all_0_13_13) = all_68_0_52, k11_group_4(all_0_13_13) = all_59_0_49, yields: % 11.08/3.18 | (316) all_68_0_52 = all_59_0_49 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_35_0_41, all_145_0_77 and discharging atoms k11_group_4(all_0_13_13) = all_145_0_77, k11_group_4(all_0_13_13) = all_35_0_41, yields: % 11.08/3.18 | (317) all_145_0_77 = all_35_0_41 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_29_0_39, all_92_0_60 and discharging atoms k11_group_4(all_0_13_13) = all_92_0_60, k11_group_4(all_0_13_13) = all_29_0_39, yields: % 11.08/3.18 | (318) all_92_0_60 = all_29_0_39 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_13_13, all_27_1_34, all_59_0_49 and discharging atoms k11_group_4(all_0_13_13) = all_59_0_49, k11_group_4(all_0_13_13) = all_27_1_34, yields: % 11.08/3.18 | (319) all_59_0_49 = all_27_1_34 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_127_0_71, all_139_0_75 and discharging atoms k11_group_4(all_0_16_16) = all_139_0_75, k11_group_4(all_0_16_16) = all_127_0_71, yields: % 11.08/3.18 | (320) all_139_0_75 = all_127_0_71 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_114_0_67, all_127_0_71 and discharging atoms k11_group_4(all_0_16_16) = all_127_0_71, k11_group_4(all_0_16_16) = all_114_0_67, yields: % 11.08/3.18 | (321) all_127_0_71 = all_114_0_67 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_101_0_63, all_114_0_67 and discharging atoms k11_group_4(all_0_16_16) = all_114_0_67, k11_group_4(all_0_16_16) = all_101_0_63, yields: % 11.08/3.18 | (322) all_114_0_67 = all_101_0_63 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_89_0_59, all_101_0_63 and discharging atoms k11_group_4(all_0_16_16) = all_101_0_63, k11_group_4(all_0_16_16) = all_89_0_59, yields: % 11.08/3.18 | (323) all_101_0_63 = all_89_0_59 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_77_0_55, all_89_0_59 and discharging atoms k11_group_4(all_0_16_16) = all_89_0_59, k11_group_4(all_0_16_16) = all_77_0_55, yields: % 11.08/3.18 | (324) all_89_0_59 = all_77_0_55 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_65_0_51, all_77_0_55 and discharging atoms k11_group_4(all_0_16_16) = all_77_0_55, k11_group_4(all_0_16_16) = all_65_0_51, yields: % 11.08/3.18 | (325) all_77_0_55 = all_65_0_51 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_53_0_47, all_65_0_51 and discharging atoms k11_group_4(all_0_16_16) = all_65_0_51, k11_group_4(all_0_16_16) = all_53_0_47, yields: % 11.08/3.18 | (326) all_65_0_51 = all_53_0_47 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_44_0_44, all_53_0_47 and discharging atoms k11_group_4(all_0_16_16) = all_53_0_47, k11_group_4(all_0_16_16) = all_44_0_44, yields: % 11.08/3.18 | (327) all_53_0_47 = all_44_0_44 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_41_0_43, all_0_14_14 and discharging atoms k11_group_4(all_0_16_16) = all_41_0_43, k11_group_4(all_0_16_16) = all_0_14_14, yields: % 11.08/3.18 | (328) all_41_0_43 = all_0_14_14 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_41_0_43, all_44_0_44 and discharging atoms k11_group_4(all_0_16_16) = all_44_0_44, k11_group_4(all_0_16_16) = all_41_0_43, yields: % 11.08/3.18 | (329) all_44_0_44 = all_41_0_43 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (32) with all_0_16_16, all_27_3_36, all_139_0_75 and discharging atoms k11_group_4(all_0_16_16) = all_139_0_75, k11_group_4(all_0_16_16) = all_27_3_36, yields: % 11.08/3.18 | (330) all_139_0_75 = all_27_3_36 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (11) with all_0_13_13, all_136_0_74, all_148_0_78 and discharging atoms u1_struct_0(all_0_13_13) = all_148_0_78, u1_struct_0(all_0_13_13) = all_136_0_74, yields: % 11.08/3.18 | (331) all_148_0_78 = all_136_0_74 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (11) with all_0_13_13, all_111_0_66, all_148_0_78 and discharging atoms u1_struct_0(all_0_13_13) = all_148_0_78, u1_struct_0(all_0_13_13) = all_111_0_66, yields: % 11.08/3.18 | (332) all_148_0_78 = all_111_0_66 % 11.08/3.18 | % 11.08/3.18 | Instantiating formula (11) with all_0_13_13, all_83_0_57, all_148_0_78 and discharging atoms u1_struct_0(all_0_13_13) = all_148_0_78, u1_struct_0(all_0_13_13) = all_83_0_57, yields: % 11.08/3.18 | (333) all_148_0_78 = all_83_0_57 % 11.08/3.18 | % 11.08/3.19 | Instantiating formula (11) with all_0_13_13, all_83_0_57, all_98_0_62 and discharging atoms u1_struct_0(all_0_13_13) = all_98_0_62, u1_struct_0(all_0_13_13) = all_83_0_57, yields: % 11.08/3.19 | (334) all_98_0_62 = all_83_0_57 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_13_13, all_71_0_53, all_121_0_69 and discharging atoms u1_struct_0(all_0_13_13) = all_121_0_69, u1_struct_0(all_0_13_13) = all_71_0_53, yields: % 11.08/3.19 | (335) all_121_0_69 = all_71_0_53 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_13_13, all_71_0_53, all_83_0_57 and discharging atoms u1_struct_0(all_0_13_13) = all_83_0_57, u1_struct_0(all_0_13_13) = all_71_0_53, yields: % 11.08/3.19 | (336) all_83_0_57 = all_71_0_53 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_13_13, all_62_0_50, all_98_0_62 and discharging atoms u1_struct_0(all_0_13_13) = all_98_0_62, u1_struct_0(all_0_13_13) = all_62_0_50, yields: % 11.08/3.19 | (337) all_98_0_62 = all_62_0_50 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_13_13, all_38_0_42, all_148_0_78 and discharging atoms u1_struct_0(all_0_13_13) = all_148_0_78, u1_struct_0(all_0_13_13) = all_38_0_42, yields: % 11.08/3.19 | (338) all_148_0_78 = all_38_0_42 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_13_13, all_32_0_40, all_0_12_12 and discharging atoms u1_struct_0(all_0_13_13) = all_32_0_40, u1_struct_0(all_0_13_13) = all_0_12_12, yields: % 11.08/3.19 | (339) all_32_0_40 = all_0_12_12 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_13_13, all_32_0_40, all_83_0_57 and discharging atoms u1_struct_0(all_0_13_13) = all_83_0_57, u1_struct_0(all_0_13_13) = all_32_0_40, yields: % 11.08/3.19 | (340) all_83_0_57 = all_32_0_40 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_13_13, all_27_4_37, all_121_0_69 and discharging atoms u1_struct_0(all_0_13_13) = all_121_0_69, u1_struct_0(all_0_13_13) = all_27_4_37, yields: % 11.08/3.19 | (341) all_121_0_69 = all_27_4_37 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_124_0_70, all_130_0_72 and discharging atoms u1_struct_0(all_0_16_16) = all_130_0_72, u1_struct_0(all_0_16_16) = all_124_0_70, yields: % 11.08/3.19 | (342) all_130_0_72 = all_124_0_70 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_104_0_64, all_142_0_76 and discharging atoms u1_struct_0(all_0_16_16) = all_142_0_76, u1_struct_0(all_0_16_16) = all_104_0_64, yields: % 11.08/3.19 | (343) all_142_0_76 = all_104_0_64 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_104_0_64, all_124_0_70 and discharging atoms u1_struct_0(all_0_16_16) = all_124_0_70, u1_struct_0(all_0_16_16) = all_104_0_64, yields: % 11.08/3.19 | (344) all_124_0_70 = all_104_0_64 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_95_0_61, all_124_0_70 and discharging atoms u1_struct_0(all_0_16_16) = all_124_0_70, u1_struct_0(all_0_16_16) = all_95_0_61, yields: % 11.08/3.19 | (345) all_124_0_70 = all_95_0_61 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_86_0_58, all_124_0_70 and discharging atoms u1_struct_0(all_0_16_16) = all_124_0_70, u1_struct_0(all_0_16_16) = all_86_0_58, yields: % 11.08/3.19 | (346) all_124_0_70 = all_86_0_58 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_74_0_54, all_124_0_70 and discharging atoms u1_struct_0(all_0_16_16) = all_124_0_70, u1_struct_0(all_0_16_16) = all_74_0_54, yields: % 11.08/3.19 | (347) all_124_0_70 = all_74_0_54 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_56_0_48, all_142_0_76 and discharging atoms u1_struct_0(all_0_16_16) = all_142_0_76, u1_struct_0(all_0_16_16) = all_56_0_48, yields: % 11.08/3.19 | (348) all_142_0_76 = all_56_0_48 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_50_0_46, all_0_15_15 and discharging atoms u1_struct_0(all_0_16_16) = all_50_0_46, u1_struct_0(all_0_16_16) = all_0_15_15, yields: % 11.08/3.19 | (349) all_50_0_46 = all_0_15_15 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_50_0_46, all_124_0_70 and discharging atoms u1_struct_0(all_0_16_16) = all_124_0_70, u1_struct_0(all_0_16_16) = all_50_0_46, yields: % 11.08/3.19 | (350) all_124_0_70 = all_50_0_46 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_47_0_45, all_130_0_72 and discharging atoms u1_struct_0(all_0_16_16) = all_130_0_72, u1_struct_0(all_0_16_16) = all_47_0_45, yields: % 11.08/3.19 | (351) all_130_0_72 = all_47_0_45 % 11.08/3.19 | % 11.08/3.19 | Instantiating formula (11) with all_0_16_16, all_27_5_38, all_50_0_46 and discharging atoms u1_struct_0(all_0_16_16) = all_50_0_46, u1_struct_0(all_0_16_16) = all_27_5_38, yields: % 11.08/3.19 | (352) all_50_0_46 = all_27_5_38 % 11.08/3.19 | % 11.08/3.19 | Combining equations (333,331) yields a new equation: % 11.08/3.19 | (353) all_136_0_74 = all_83_0_57 % 11.08/3.19 | % 11.08/3.19 | Combining equations (338,331) yields a new equation: % 11.08/3.19 | (354) all_136_0_74 = all_38_0_42 % 11.08/3.19 | % 11.08/3.19 | Combining equations (332,331) yields a new equation: % 11.08/3.19 | (355) all_136_0_74 = all_111_0_66 % 11.08/3.19 | % 11.08/3.19 | Combining equations (309,317) yields a new equation: % 11.08/3.19 | (356) all_133_0_73 = all_35_0_41 % 11.08/3.19 | % 11.08/3.19 | Simplifying 356 yields: % 11.08/3.19 | (357) all_133_0_73 = all_35_0_41 % 11.08/3.19 | % 11.08/3.19 | Combining equations (343,348) yields a new equation: % 11.08/3.19 | (358) all_104_0_64 = all_56_0_48 % 11.08/3.19 | % 11.08/3.19 | Simplifying 358 yields: % 11.08/3.19 | (359) all_104_0_64 = all_56_0_48 % 11.08/3.19 | % 11.08/3.19 | Combining equations (320,330) yields a new equation: % 11.08/3.19 | (360) all_127_0_71 = all_27_3_36 % 11.08/3.19 | % 11.08/3.19 | Simplifying 360 yields: % 11.08/3.19 | (361) all_127_0_71 = all_27_3_36 % 11.08/3.19 | % 11.08/3.19 | Combining equations (354,355) yields a new equation: % 11.08/3.19 | (362) all_111_0_66 = all_38_0_42 % 11.08/3.19 | % 11.08/3.19 | Combining equations (353,355) yields a new equation: % 11.08/3.19 | (363) all_111_0_66 = all_83_0_57 % 11.08/3.19 | % 11.08/3.19 | Combining equations (310,357) yields a new equation: % 11.08/3.19 | (364) all_117_0_68 = all_35_0_41 % 11.08/3.19 | % 11.08/3.19 | Simplifying 364 yields: % 11.08/3.19 | (365) all_117_0_68 = all_35_0_41 % 11.08/3.19 | % 11.08/3.19 | Combining equations (342,351) yields a new equation: % 11.08/3.19 | (366) all_124_0_70 = all_47_0_45 % 11.08/3.19 | % 11.08/3.19 | Simplifying 366 yields: % 11.08/3.19 | (367) all_124_0_70 = all_47_0_45 % 11.08/3.19 | % 11.08/3.19 | Combining equations (321,361) yields a new equation: % 11.08/3.19 | (368) all_114_0_67 = all_27_3_36 % 11.08/3.19 | % 11.08/3.19 | Simplifying 368 yields: % 11.08/3.19 | (369) all_114_0_67 = all_27_3_36 % 11.08/3.19 | % 11.08/3.19 | Combining equations (350,345) yields a new equation: % 11.08/3.19 | (370) all_95_0_61 = all_50_0_46 % 11.08/3.19 | % 11.08/3.19 | Combining equations (344,345) yields a new equation: % 11.08/3.19 | (371) all_104_0_64 = all_95_0_61 % 11.08/3.19 | % 11.08/3.19 | Simplifying 371 yields: % 11.08/3.19 | (372) all_104_0_64 = all_95_0_61 % 11.08/3.19 | % 11.08/3.19 | Combining equations (347,345) yields a new equation: % 11.08/3.19 | (373) all_95_0_61 = all_74_0_54 % 11.08/3.19 | % 11.08/3.19 | Combining equations (346,345) yields a new equation: % 11.08/3.19 | (374) all_95_0_61 = all_86_0_58 % 11.08/3.19 | % 11.08/3.19 | Combining equations (367,345) yields a new equation: % 11.08/3.19 | (375) all_95_0_61 = all_47_0_45 % 11.08/3.19 | % 11.08/3.19 | Combining equations (335,341) yields a new equation: % 11.08/3.19 | (376) all_71_0_53 = all_27_4_37 % 11.08/3.19 | % 11.08/3.19 | Simplifying 376 yields: % 11.08/3.19 | (377) all_71_0_53 = all_27_4_37 % 11.08/3.19 | % 11.08/3.19 | Combining equations (311,365) yields a new equation: % 11.08/3.19 | (378) all_107_0_65 = all_35_0_41 % 11.08/3.19 | % 11.08/3.19 | Simplifying 378 yields: % 11.08/3.19 | (379) all_107_0_65 = all_35_0_41 % 11.08/3.19 | % 11.08/3.20 | Combining equations (322,369) yields a new equation: % 11.08/3.20 | (380) all_101_0_63 = all_27_3_36 % 11.08/3.20 | % 11.08/3.20 | Simplifying 380 yields: % 11.08/3.20 | (381) all_101_0_63 = all_27_3_36 % 11.08/3.20 | % 11.08/3.20 | Combining equations (363,362) yields a new equation: % 11.08/3.20 | (382) all_83_0_57 = all_38_0_42 % 11.08/3.20 | % 11.08/3.20 | Simplifying 382 yields: % 11.08/3.20 | (383) all_83_0_57 = all_38_0_42 % 11.08/3.20 | % 11.08/3.20 | Combining equations (313,379) yields a new equation: % 11.08/3.20 | (384) all_80_0_56 = all_35_0_41 % 11.08/3.20 | % 11.08/3.20 | Simplifying 384 yields: % 11.08/3.20 | (385) all_80_0_56 = all_35_0_41 % 11.08/3.20 | % 11.08/3.20 | Combining equations (372,359) yields a new equation: % 11.08/3.20 | (386) all_95_0_61 = all_56_0_48 % 11.08/3.20 | % 11.08/3.20 | Simplifying 386 yields: % 11.08/3.20 | (387) all_95_0_61 = all_56_0_48 % 11.08/3.20 | % 11.08/3.20 | Combining equations (323,381) yields a new equation: % 11.08/3.20 | (388) all_89_0_59 = all_27_3_36 % 11.08/3.20 | % 11.08/3.20 | Simplifying 388 yields: % 11.08/3.20 | (389) all_89_0_59 = all_27_3_36 % 11.08/3.20 | % 11.08/3.20 | Combining equations (334,337) yields a new equation: % 11.08/3.20 | (390) all_83_0_57 = all_62_0_50 % 11.08/3.20 | % 11.08/3.20 | Simplifying 390 yields: % 11.08/3.20 | (391) all_83_0_57 = all_62_0_50 % 11.08/3.20 | % 11.08/3.20 | Combining equations (373,374) yields a new equation: % 11.08/3.20 | (392) all_86_0_58 = all_74_0_54 % 11.08/3.20 | % 11.08/3.20 | Combining equations (370,374) yields a new equation: % 11.08/3.20 | (393) all_86_0_58 = all_50_0_46 % 11.08/3.20 | % 11.08/3.20 | Combining equations (387,374) yields a new equation: % 11.08/3.20 | (394) all_86_0_58 = all_56_0_48 % 11.08/3.20 | % 11.08/3.20 | Combining equations (375,374) yields a new equation: % 11.08/3.20 | (395) all_86_0_58 = all_47_0_45 % 11.08/3.20 | % 11.08/3.20 | Combining equations (315,318) yields a new equation: % 11.08/3.20 | (396) all_59_0_49 = all_29_0_39 % 11.08/3.20 | % 11.08/3.20 | Simplifying 396 yields: % 11.08/3.20 | (397) all_59_0_49 = all_29_0_39 % 11.08/3.20 | % 11.08/3.20 | Combining equations (312,318) yields a new equation: % 11.08/3.20 | (398) all_29_0_39 = all_0_11_11 % 11.08/3.20 | % 11.43/3.20 | Combining equations (324,389) yields a new equation: % 11.43/3.20 | (399) all_77_0_55 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Simplifying 399 yields: % 11.43/3.20 | (400) all_77_0_55 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Combining equations (393,392) yields a new equation: % 11.43/3.20 | (401) all_74_0_54 = all_50_0_46 % 11.43/3.20 | % 11.43/3.20 | Combining equations (395,392) yields a new equation: % 11.43/3.20 | (402) all_74_0_54 = all_47_0_45 % 11.43/3.20 | % 11.43/3.20 | Combining equations (394,392) yields a new equation: % 11.43/3.20 | (403) all_74_0_54 = all_56_0_48 % 11.43/3.20 | % 11.43/3.20 | Combining equations (336,391) yields a new equation: % 11.43/3.20 | (404) all_71_0_53 = all_62_0_50 % 11.43/3.20 | % 11.43/3.20 | Simplifying 404 yields: % 11.43/3.20 | (405) all_71_0_53 = all_62_0_50 % 11.43/3.20 | % 11.43/3.20 | Combining equations (340,391) yields a new equation: % 11.43/3.20 | (406) all_62_0_50 = all_32_0_40 % 11.43/3.20 | % 11.43/3.20 | Combining equations (383,391) yields a new equation: % 11.43/3.20 | (407) all_62_0_50 = all_38_0_42 % 11.43/3.20 | % 11.43/3.20 | Combining equations (314,385) yields a new equation: % 11.43/3.20 | (408) all_68_0_52 = all_35_0_41 % 11.43/3.20 | % 11.43/3.20 | Simplifying 408 yields: % 11.43/3.20 | (409) all_68_0_52 = all_35_0_41 % 11.43/3.20 | % 11.43/3.20 | Combining equations (325,400) yields a new equation: % 11.43/3.20 | (410) all_65_0_51 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Simplifying 410 yields: % 11.43/3.20 | (411) all_65_0_51 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Combining equations (401,403) yields a new equation: % 11.43/3.20 | (412) all_56_0_48 = all_50_0_46 % 11.43/3.20 | % 11.43/3.20 | Combining equations (402,403) yields a new equation: % 11.43/3.20 | (413) all_56_0_48 = all_47_0_45 % 11.43/3.20 | % 11.43/3.20 | Combining equations (405,377) yields a new equation: % 11.43/3.20 | (414) all_62_0_50 = all_27_4_37 % 11.43/3.20 | % 11.43/3.20 | Simplifying 414 yields: % 11.43/3.20 | (415) all_62_0_50 = all_27_4_37 % 11.43/3.20 | % 11.43/3.20 | Combining equations (316,409) yields a new equation: % 11.43/3.20 | (416) all_59_0_49 = all_35_0_41 % 11.43/3.20 | % 11.43/3.20 | Simplifying 416 yields: % 11.43/3.20 | (417) all_59_0_49 = all_35_0_41 % 11.43/3.20 | % 11.43/3.20 | Combining equations (326,411) yields a new equation: % 11.43/3.20 | (418) all_53_0_47 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Simplifying 418 yields: % 11.43/3.20 | (419) all_53_0_47 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Combining equations (406,407) yields a new equation: % 11.43/3.20 | (420) all_38_0_42 = all_32_0_40 % 11.43/3.20 | % 11.43/3.20 | Combining equations (415,407) yields a new equation: % 11.43/3.20 | (421) all_38_0_42 = all_27_4_37 % 11.43/3.20 | % 11.43/3.20 | Combining equations (319,417) yields a new equation: % 11.43/3.20 | (422) all_35_0_41 = all_27_1_34 % 11.43/3.20 | % 11.43/3.20 | Combining equations (397,417) yields a new equation: % 11.43/3.20 | (423) all_35_0_41 = all_29_0_39 % 11.43/3.20 | % 11.43/3.20 | Combining equations (412,413) yields a new equation: % 11.43/3.20 | (424) all_50_0_46 = all_47_0_45 % 11.43/3.20 | % 11.43/3.20 | Simplifying 424 yields: % 11.43/3.20 | (425) all_50_0_46 = all_47_0_45 % 11.43/3.20 | % 11.43/3.20 | Combining equations (327,419) yields a new equation: % 11.43/3.20 | (426) all_44_0_44 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Simplifying 426 yields: % 11.43/3.20 | (427) all_44_0_44 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Combining equations (349,425) yields a new equation: % 11.43/3.20 | (428) all_47_0_45 = all_0_15_15 % 11.43/3.20 | % 11.43/3.20 | Combining equations (352,425) yields a new equation: % 11.43/3.20 | (429) all_47_0_45 = all_27_5_38 % 11.43/3.20 | % 11.43/3.20 | Combining equations (429,428) yields a new equation: % 11.43/3.20 | (430) all_27_5_38 = all_0_15_15 % 11.43/3.20 | % 11.43/3.20 | Simplifying 430 yields: % 11.43/3.20 | (431) all_27_5_38 = all_0_15_15 % 11.43/3.20 | % 11.43/3.20 | Combining equations (329,427) yields a new equation: % 11.43/3.20 | (432) all_41_0_43 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Simplifying 432 yields: % 11.43/3.20 | (433) all_41_0_43 = all_27_3_36 % 11.43/3.20 | % 11.43/3.20 | Combining equations (328,433) yields a new equation: % 11.43/3.20 | (434) all_27_3_36 = all_0_14_14 % 11.43/3.20 | % 11.43/3.20 | Combining equations (420,421) yields a new equation: % 11.43/3.20 | (435) all_32_0_40 = all_27_4_37 % 11.43/3.20 | % 11.43/3.20 | Simplifying 435 yields: % 11.43/3.20 | (436) all_32_0_40 = all_27_4_37 % 11.43/3.20 | % 11.43/3.20 | Combining equations (423,422) yields a new equation: % 11.43/3.20 | (437) all_29_0_39 = all_27_1_34 % 11.43/3.20 | % 11.43/3.20 | Simplifying 437 yields: % 11.43/3.20 | (438) all_29_0_39 = all_27_1_34 % 11.43/3.20 | % 11.43/3.20 | Combining equations (339,436) yields a new equation: % 11.43/3.20 | (439) all_27_4_37 = all_0_12_12 % 11.43/3.20 | % 11.43/3.20 | Combining equations (398,438) yields a new equation: % 11.43/3.20 | (440) all_27_1_34 = all_0_11_11 % 11.43/3.20 | % 11.43/3.20 | Combining equations (440,422) yields a new equation: % 11.43/3.20 | (441) all_35_0_41 = all_0_11_11 % 11.43/3.20 | % 11.43/3.20 | Combining equations (434,433) yields a new equation: % 11.43/3.20 | (328) all_41_0_43 = all_0_14_14 % 11.43/3.20 | % 11.43/3.20 | Combining equations (434,427) yields a new equation: % 11.43/3.20 | (443) all_44_0_44 = all_0_14_14 % 11.43/3.20 | % 11.43/3.20 | Combining equations (441,379) yields a new equation: % 11.43/3.20 | (444) all_107_0_65 = all_0_11_11 % 11.43/3.21 | % 11.43/3.21 | Combining equations (441,365) yields a new equation: % 11.43/3.21 | (445) all_117_0_68 = all_0_11_11 % 11.43/3.21 | % 11.43/3.21 | From (440) and (144) follows: % 11.43/3.21 | (39) k11_group_4(all_0_13_13) = all_0_11_11 % 11.43/3.21 | % 11.43/3.21 | From (434) and (142) follows: % 11.43/3.21 | (54) k11_group_4(all_0_16_16) = all_0_14_14 % 11.43/3.21 | % 11.43/3.21 | From (440) and (140) follows: % 11.43/3.21 | (448) u1_struct_0(all_0_11_11) = all_27_0_33 % 11.43/3.21 | % 11.43/3.21 | From (434) and (146) follows: % 11.43/3.21 | (449) u1_struct_0(all_0_14_14) = all_27_2_35 % 11.43/3.21 | % 11.43/3.21 | From (328)(444) and (268) follows: % 11.43/3.21 | (450) m4_vectsp_8(all_0_9_9, all_0_14_14, all_0_11_11) % 11.43/3.21 | % 11.43/3.21 | From (443)(445) and (278) follows: % 11.43/3.21 | (451) m3_vectsp_8(all_0_9_9, all_0_14_14, all_0_11_11) % 11.43/3.21 | % 11.43/3.21 +-Applying beta-rule and splitting (141), into two cases. % 11.43/3.21 |-Branch one: % 11.43/3.21 | (452) ~ v1_funct_2(all_0_10_10, all_27_5_38, all_27_4_37) % 11.43/3.21 | % 11.43/3.21 | From (431)(439) and (452) follows: % 11.43/3.21 | (453) ~ v1_funct_2(all_0_10_10, all_0_15_15, all_0_12_12) % 11.43/3.21 | % 11.43/3.21 | Using (85) and (453) yields: % 11.43/3.21 | (454) $false % 11.43/3.21 | % 11.43/3.21 |-The branch is then unsatisfiable % 11.43/3.21 |-Branch two: % 11.43/3.21 | (455) v1_funct_2(all_0_10_10, all_27_5_38, all_27_4_37) % 11.43/3.21 | (456) ~ m1_relset_1(all_0_10_10, all_27_5_38, all_27_4_37) | (m2_relset_1(all_0_9_9, all_27_2_35, all_27_0_33) & v1_funct_2(all_0_9_9, all_27_2_35, all_27_0_33) & v1_funct_1(all_0_9_9)) % 11.43/3.21 | % 11.43/3.21 +-Applying beta-rule and splitting (456), into two cases. % 11.43/3.21 |-Branch one: % 11.43/3.21 | (457) ~ m1_relset_1(all_0_10_10, all_27_5_38, all_27_4_37) % 11.43/3.21 | % 11.43/3.21 | From (431)(439) and (457) follows: % 11.43/3.21 | (458) ~ m1_relset_1(all_0_10_10, all_0_15_15, all_0_12_12) % 11.43/3.21 | % 11.43/3.21 | Using (125) and (458) yields: % 11.43/3.21 | (454) $false % 11.43/3.21 | % 11.43/3.21 |-The branch is then unsatisfiable % 11.43/3.21 |-Branch two: % 11.43/3.21 | (460) m1_relset_1(all_0_10_10, all_27_5_38, all_27_4_37) % 11.43/3.21 | (461) m2_relset_1(all_0_9_9, all_27_2_35, all_27_0_33) & v1_funct_2(all_0_9_9, all_27_2_35, all_27_0_33) & v1_funct_1(all_0_9_9) % 11.43/3.21 | % 11.43/3.21 | Applying alpha-rule on (461) yields: % 11.43/3.21 | (462) m2_relset_1(all_0_9_9, all_27_2_35, all_27_0_33) % 11.43/3.21 | (463) v1_funct_2(all_0_9_9, all_27_2_35, all_27_0_33) % 11.43/3.21 | (464) v1_funct_1(all_0_9_9) % 11.43/3.21 | % 11.43/3.21 | Instantiating formula (16) with all_0_9_9, all_27_0_33, all_0_11_11, all_27_2_35, all_0_14_14 and discharging atoms u1_struct_0(all_0_11_11) = all_27_0_33, u1_struct_0(all_0_14_14) = all_27_2_35, m4_vectsp_8(all_0_9_9, all_0_14_14, all_0_11_11), m3_vectsp_8(all_0_9_9, all_0_14_14, all_0_11_11), v10_lattices(all_0_11_11), v10_lattices(all_0_14_14), l3_lattices(all_0_11_11), l3_lattices(all_0_14_14), m2_relset_1(all_0_9_9, all_27_2_35, all_27_0_33), v1_funct_2(all_0_9_9, all_27_2_35, all_27_0_33), v1_funct_1(all_0_9_9), ~ m1_lattice4(all_0_9_9, all_0_14_14, all_0_11_11), yields: % 11.43/3.21 | (465) v3_struct_0(all_0_11_11) | v3_struct_0(all_0_14_14) % 11.43/3.21 | % 11.43/3.21 +-Applying beta-rule and splitting (465), into two cases. % 11.43/3.21 |-Branch one: % 11.43/3.21 | (466) v3_struct_0(all_0_11_11) % 11.43/3.21 | % 11.43/3.21 | Instantiating formula (42) with all_0_11_11, all_0_13_13 and discharging atoms k11_group_4(all_0_13_13) = all_0_11_11, l1_group_1(all_0_13_13), v4_group_1(all_0_13_13), v3_group_1(all_0_13_13), v3_struct_0(all_0_11_11), ~ v3_struct_0(all_0_13_13), yields: % 11.43/3.21 | (454) $false % 11.43/3.21 | % 11.43/3.21 |-The branch is then unsatisfiable % 11.43/3.21 |-Branch two: % 11.43/3.21 | (468) ~ v3_struct_0(all_0_11_11) % 11.43/3.21 | (469) v3_struct_0(all_0_14_14) % 11.43/3.21 | % 11.43/3.21 | Instantiating formula (42) with all_0_14_14, all_0_16_16 and discharging atoms k11_group_4(all_0_16_16) = all_0_14_14, l1_group_1(all_0_16_16), v4_group_1(all_0_16_16), v3_group_1(all_0_16_16), v3_struct_0(all_0_14_14), ~ v3_struct_0(all_0_16_16), yields: % 11.43/3.21 | (454) $false % 11.43/3.21 | % 11.43/3.21 |-The branch is then unsatisfiable % 11.43/3.21 % SZS output end Proof for theBenchmark % 11.43/3.21 % 11.43/3.21 2594ms %------------------------------------------------------------------------------