%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : LAT326+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n006.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 : Sun Jul 17 04:33:05 EDT 2022 % Result : Theorem 7.79s 2.46s % Output : Proof 15.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : LAT326+1 : TPTP v8.1.0. Released v3.4.0. % 0.00/0.10 % Command : ePrincess-casc -timeout=%d %s % 0.11/0.31 % Computer : n006.cluster.edu % 0.11/0.31 % Model : x86_64 x86_64 % 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.31 % Memory : 8042.1875MB % 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 600 % 0.11/0.31 % DateTime : Wed Jun 29 10:27:08 EDT 2022 % 0.11/0.31 % CPUTime : % 0.16/0.56 ____ _ % 0.16/0.56 ___ / __ \_____(_)___ ________ __________ % 0.16/0.56 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.16/0.56 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.16/0.56 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.16/0.56 % 0.16/0.56 A Theorem Prover for First-Order Logic % 0.16/0.56 (ePrincess v.1.0) % 0.16/0.56 % 0.16/0.56 (c) Philipp Rümmer, 2009-2015 % 0.16/0.56 (c) Peter Backeman, 2014-2015 % 0.16/0.56 (contributions by Angelo Brillout, Peter Baumgartner) % 0.16/0.56 Free software under GNU Lesser General Public License (LGPL). % 0.16/0.56 Bug reports to peter@backeman.se % 0.16/0.56 % 0.16/0.56 For more information, visit http://user.uu.se/~petba168/breu/ % 0.16/0.56 % 0.16/0.57 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.71/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.96/1.02 Prover 0: Preprocessing ... % 3.45/1.43 Prover 0: Warning: ignoring some quantifiers % 3.45/1.46 Prover 0: Constructing countermodel ... % 7.79/2.46 Prover 0: proved (1814ms) % 7.79/2.46 % 7.79/2.46 No countermodel exists, formula is valid % 7.79/2.46 % SZS status Theorem for theBenchmark % 7.79/2.46 % 7.79/2.46 Generating proof ... Warning: ignoring some quantifiers % 14.37/3.95 found it (size 277) % 14.37/3.95 % 14.37/3.95 % SZS output start Proof for theBenchmark % 14.37/3.96 Assumed formulas after preprocessing and simplification: % 14.37/3.96 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : (u2_lattices(v0) = v1 & u1_lattices(v0) = v2 & k1_realset1(v2, v3) = v6 & k1_realset1(v1, v3) = v5 & k2_zfmisc_1(v3, v3) = v4 & l2_lattices(v14) & l1_struct_0(v15) & l1_struct_0(v7) & l1_lattices(v16) & v2_funct_1(v8) & v1_relat_1(v12) & v1_relat_1(v10) & v1_relat_1(v8) & m2_relset_1(v6, v4, v3) & m2_relset_1(v5, v4, v3) & v1_funct_2(v6, v4, v3) & v1_funct_2(v5, v4, v3) & v1_funct_1(v12) & v1_funct_1(v10) & v1_funct_1(v8) & v1_funct_1(v6) & v1_funct_1(v5) & m2_lattice4(v3, v0) & v1_xboole_0(v11) & v1_xboole_0(v10) & v1_xboole_0(k1_xboole_0) & l3_lattices(v13) & l3_lattices(v0) & v10_lattices(v0) & ~ v1_xboole_0(v9) & ~ v1_xboole_0(v3) & ~ v3_struct_0(v7) & ~ v3_struct_0(v0) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v18 = v17 | ~ (k7_relat_1(v20, v19) = v18) | ~ (k7_relat_1(v20, v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v18 = v17 | ~ (k1_realset1(v20, v19) = v18) | ~ (k1_realset1(v20, v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v18 = v17 | ~ (k2_zfmisc_1(v20, v19) = v18) | ~ (k2_zfmisc_1(v20, v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (k7_relat_1(v17, v19) = v20) | ~ (k2_zfmisc_1(v18, v18) = v19) | ~ v1_relat_1(v17) | k1_realset1(v17, v18) = 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) | ~ m1_subset_1(v18, v20) | ~ r2_hidden(v17, v18) | ~ v1_xboole_0(v19)) & ! [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] : ( ~ (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 | ~ (u2_lattices(v19) = v18) | ~ (u2_lattices(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : (v18 = v17 | ~ (u1_lattices(v19) = v18) | ~ (u1_lattices(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : (v18 = v17 | ~ (u1_struct_0(v19) = v18) | ~ (u1_struct_0(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : (v18 = v17 | ~ (k1_zfmisc_1(v19) = v18) | ~ (k1_zfmisc_1(v19) = v17)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (u1_struct_0(v17) = v18) | ~ (k2_zfmisc_1(v18, v18) = v19) | ~ l2_lattices(v17) | ~ v5_lattices(v17) | v3_struct_0(v17) | ? [v20] : (u2_lattices(v17) = v20 & v1_partfun1(v20, v19, v18) & v1_relat_1(v20) & v2_binop_1(v20, v18) & v1_funct_2(v20, v19, v18) & v1_funct_1(v20))) & ! [v17] : ! [v18] : ! [v19] : ( ~ (u1_struct_0(v17) = v18) | ~ (k2_zfmisc_1(v18, v18) = v19) | ~ l2_lattices(v17) | ~ v4_lattices(v17) | v3_struct_0(v17) | ? [v20] : (u2_lattices(v17) = v20 & v1_partfun1(v20, v19, v18) & v1_relat_1(v20) & v1_binop_1(v20, v18) & v1_funct_2(v20, v19, v18) & v1_funct_1(v20))) & ! [v17] : ! [v18] : ! [v19] : ( ~ (u1_struct_0(v17) = v18) | ~ (k2_zfmisc_1(v18, v18) = v19) | ~ 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] : ( ~ (u1_struct_0(v17) = v18) | ~ (k2_zfmisc_1(v18, v18) = v19) | ~ l1_lattices(v17) | ~ v7_lattices(v17) | v3_struct_0(v17) | ? [v20] : (u1_lattices(v17) = v20 & v1_partfun1(v20, v19, v18) & v1_relat_1(v20) & v2_binop_1(v20, v18) & v1_funct_2(v20, v19, v18) & v1_funct_1(v20))) & ! [v17] : ! [v18] : ! [v19] : ( ~ (u1_struct_0(v17) = v18) | ~ (k2_zfmisc_1(v18, v18) = v19) | ~ l1_lattices(v17) | ~ v6_lattices(v17) | v3_struct_0(v17) | ? [v20] : (u1_lattices(v17) = v20 & v1_partfun1(v20, v19, v18) & v1_relat_1(v20) & v1_binop_1(v20, v18) & v1_funct_2(v20, v19, v18) & v1_funct_1(v20))) & ! [v17] : ! [v18] : ! [v19] : ( ~ (u1_struct_0(v17) = v18) | ~ (k2_zfmisc_1(v18, v18) = v19) | ~ 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] : ( ~ (k7_relat_1(v17, v18) = v19) | ~ v1_relat_1(v17) | ~ v1_funct_1(v17) | v1_relat_1(v19)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k7_relat_1(v17, v18) = v19) | ~ v1_relat_1(v17) | ~ v1_funct_1(v17) | v1_funct_1(v19)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k7_relat_1(v17, v18) = v19) | ~ v1_relat_1(v17) | v1_relat_1(v19)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k1_realset1(v17, v18) = v19) | ~ v1_relat_1(v17) | ~ v1_funct_1(v17) | v1_relat_1(v19)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k1_realset1(v17, v18) = v19) | ~ v1_relat_1(v17) | ~ v1_funct_1(v17) | v1_funct_1(v19)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k1_realset1(v17, v18) = v19) | ~ v1_relat_1(v17) | v1_relat_1(v19)) & ! [v17] : ! [v18] : ! [v19] : ( ~ (k1_realset1(v17, v18) = v19) | ~ v1_relat_1(v17) | ? [v20] : (k7_relat_1(v17, v20) = v19 & k2_zfmisc_1(v18, v18) = 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] : ( ~ 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] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | ~ v5_lattices(v17) | v1_relat_1(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | ~ v5_lattices(v17) | v1_funct_1(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | ~ v5_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u1_struct_0(v17) = v19 & k2_zfmisc_1(v19, v19) = v20 & v1_partfun1(v18, v20, v19) & v2_binop_1(v18, v19) & v1_funct_2(v18, v20, v19))) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | ~ v4_lattices(v17) | v1_relat_1(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | ~ v4_lattices(v17) | v1_funct_1(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | ~ v4_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u1_struct_0(v17) = v19 & k2_zfmisc_1(v19, v19) = v20 & v1_partfun1(v18, v20, v19) & v1_binop_1(v18, v19) & v1_funct_2(v18, v20, v19))) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | v1_funct_1(v18)) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l2_lattices(v17) | ? [v19] : ? [v20] : (u1_struct_0(v17) = v19 & k2_zfmisc_1(v19, v19) = v20 & m2_relset_1(v18, v20, v19) & v1_funct_2(v18, v20, v19))) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u1_lattices(v17) = v20 & u1_struct_0(v17) = v19 & r1_lattice2(v19, v20, v18))) & ! [v17] : ! [v18] : ( ~ (u2_lattices(v17) = v18) | ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u1_lattices(v17) = v20 & u1_struct_0(v17) = v19 & r1_lattice2(v19, v18, v20))) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l1_lattices(v17) | ~ v7_lattices(v17) | v1_relat_1(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l1_lattices(v17) | ~ v7_lattices(v17) | v1_funct_1(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l1_lattices(v17) | ~ v7_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u1_struct_0(v17) = v19 & k2_zfmisc_1(v19, v19) = v20 & v1_partfun1(v18, v20, v19) & v2_binop_1(v18, v19) & v1_funct_2(v18, v20, v19))) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l1_lattices(v17) | ~ v6_lattices(v17) | v1_relat_1(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l1_lattices(v17) | ~ v6_lattices(v17) | v1_funct_1(v18) | v3_struct_0(v17)) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l1_lattices(v17) | ~ v6_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u1_struct_0(v17) = v19 & k2_zfmisc_1(v19, v19) = v20 & v1_partfun1(v18, v20, v19) & v1_binop_1(v18, 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] : (u1_struct_0(v17) = v19 & k2_zfmisc_1(v19, v19) = v20 & m2_relset_1(v18, v20, v19) & v1_funct_2(v18, v20, v19))) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u2_lattices(v17) = v20 & u1_struct_0(v17) = v19 & r1_lattice2(v19, v20, v18))) & ! [v17] : ! [v18] : ( ~ (u1_lattices(v17) = v18) | ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u2_lattices(v17) = v20 & u1_struct_0(v17) = v19 & r1_lattice2(v19, v18, v20))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l2_lattices(v17) | ~ v5_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u2_lattices(v17) = v19 & k2_zfmisc_1(v18, v18) = v20 & v1_partfun1(v19, v20, v18) & v1_relat_1(v19) & v2_binop_1(v19, v18) & v1_funct_2(v19, v20, v18) & v1_funct_1(v19))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l2_lattices(v17) | ~ v4_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u2_lattices(v17) = v19 & k2_zfmisc_1(v18, v18) = v20 & v1_partfun1(v19, v20, v18) & v1_relat_1(v19) & v1_binop_1(v19, v18) & v1_funct_2(v19, v20, v18) & v1_funct_1(v19))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l2_lattices(v17) | ? [v19] : ? [v20] : (u2_lattices(v17) = v19 & k2_zfmisc_1(v18, v18) = v20 & 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_lattices(v17) | ~ v7_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u1_lattices(v17) = v19 & k2_zfmisc_1(v18, v18) = v20 & v1_partfun1(v19, v20, v18) & v1_relat_1(v19) & v2_binop_1(v19, v18) & v1_funct_2(v19, v20, v18) & v1_funct_1(v19))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l1_lattices(v17) | ~ v6_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u1_lattices(v17) = v19 & k2_zfmisc_1(v18, v18) = v20 & v1_partfun1(v19, v20, v18) & v1_relat_1(v19) & v1_binop_1(v19, v18) & v1_funct_2(v19, v20, v18) & v1_funct_1(v19))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l1_lattices(v17) | ? [v19] : ? [v20] : (u1_lattices(v17) = v19 & k2_zfmisc_1(v18, v18) = v20 & m2_relset_1(v19, v20, v18) & v1_funct_2(v19, v20, v18) & v1_funct_1(v19))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u2_lattices(v17) = v20 & u1_lattices(v17) = v19 & r1_lattice2(v18, v19, v20))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v19] : ? [v20] : (u2_lattices(v17) = v19 & u1_lattices(v17) = v20 & r1_lattice2(v18, v19, v20))) & ! [v17] : ! [v18] : ( ~ (u1_struct_0(v17) = v18) | ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v19] : (k1_zfmisc_1(v18) = v19 & ! [v20] : ( ~ m2_lattice4(v20, v17) | m1_subset_1(v20, v19)))) & ! [v17] : ! [v18] : ( ~ (k2_zfmisc_1(v17, v17) = v18) | v1_xboole_0(v17) | ? [v19] : (k1_zfmisc_1(v17) = v19 & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ! [v25] : ( ~ (k1_realset1(v24, v20) = v25) | ~ (k1_realset1(v22, v20) = v23) | ~ (k2_zfmisc_1(v20, v20) = v21) | ~ m1_subset_1(v20, v19) | ~ r1_lattice2(v17, v22, v24) | ~ m2_relset_1(v25, v21, v20) | ~ m2_relset_1(v24, v18, v17) | ~ m2_relset_1(v23, v21, v20) | ~ m2_relset_1(v22, v18, v17) | ~ v1_funct_2(v25, v21, v20) | ~ v1_funct_2(v24, v18, v17) | ~ v1_funct_2(v23, v21, v20) | ~ v1_funct_2(v22, v18, v17) | ~ v1_funct_1(v25) | ~ v1_funct_1(v24) | ~ v1_funct_1(v23) | ~ v1_funct_1(v22) | r1_lattice2(v20, v23, v25) | v1_xboole_0(v20)))) & ! [v17] : ! [v18] : ( ~ (k2_zfmisc_1(v17, v17) = v18) | v1_xboole_0(v17) | ? [v19] : (k1_zfmisc_1(v17) = v19 & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (k1_realset1(v22, v20) = v23) | ~ (k2_zfmisc_1(v20, v20) = v21) | ~ v3_binop_1(v22, v17) | ~ m1_subset_1(v20, v19) | ~ m2_relset_1(v23, v21, v20) | ~ m2_relset_1(v22, v18, v17) | ~ v1_funct_2(v23, v21, v20) | ~ v1_funct_2(v22, v18, v17) | ~ v1_funct_1(v23) | ~ v1_funct_1(v22) | v3_binop_1(v23, v20) | v1_xboole_0(v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (k1_realset1(v22, v20) = v23) | ~ (k2_zfmisc_1(v20, v20) = v21) | ~ m1_subset_1(v20, v19) | ~ v2_binop_1(v22, v17) | ~ m2_relset_1(v23, v21, v20) | ~ m2_relset_1(v22, v18, v17) | ~ v1_funct_2(v23, v21, v20) | ~ v1_funct_2(v22, v18, v17) | ~ v1_funct_1(v23) | ~ v1_funct_1(v22) | v2_binop_1(v23, v20) | v1_xboole_0(v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (k1_realset1(v22, v20) = v23) | ~ (k2_zfmisc_1(v20, v20) = v21) | ~ m1_subset_1(v20, v19) | ~ v1_binop_1(v22, v17) | ~ m2_relset_1(v23, v21, v20) | ~ m2_relset_1(v22, v18, v17) | ~ v1_funct_2(v23, v21, v20) | ~ v1_funct_2(v22, v18, v17) | ~ v1_funct_1(v23) | ~ v1_funct_1(v22) | v1_binop_1(v23, v20) | v1_xboole_0(v20)))) & ! [v17] : ! [v18] : ( ~ (k1_zfmisc_1(v17) = v18) | ~ v1_xboole_0(v18)) & ! [v17] : ! [v18] : ( ~ (k1_zfmisc_1(v17) = v18) | v1_xboole_0(v17) | ? [v19] : (k2_zfmisc_1(v17, v17) = v19 & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ! [v24] : ! [v25] : ( ~ (k1_realset1(v24, v20) = v25) | ~ (k1_realset1(v22, v20) = v23) | ~ (k2_zfmisc_1(v20, v20) = v21) | ~ m1_subset_1(v20, v18) | ~ r1_lattice2(v17, v22, v24) | ~ m2_relset_1(v25, v21, v20) | ~ m2_relset_1(v24, v19, v17) | ~ m2_relset_1(v23, v21, v20) | ~ m2_relset_1(v22, v19, v17) | ~ v1_funct_2(v25, v21, v20) | ~ v1_funct_2(v24, v19, v17) | ~ v1_funct_2(v23, v21, v20) | ~ v1_funct_2(v22, v19, v17) | ~ v1_funct_1(v25) | ~ v1_funct_1(v24) | ~ v1_funct_1(v23) | ~ v1_funct_1(v22) | r1_lattice2(v20, v23, v25) | v1_xboole_0(v20)))) & ! [v17] : ! [v18] : ( ~ (k1_zfmisc_1(v17) = v18) | v1_xboole_0(v17) | ? [v19] : (k2_zfmisc_1(v17, v17) = v19 & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (k1_realset1(v22, v20) = v23) | ~ (k2_zfmisc_1(v20, v20) = v21) | ~ v3_binop_1(v22, v17) | ~ m1_subset_1(v20, v18) | ~ m2_relset_1(v23, v21, v20) | ~ m2_relset_1(v22, v19, v17) | ~ v1_funct_2(v23, v21, v20) | ~ v1_funct_2(v22, v19, v17) | ~ v1_funct_1(v23) | ~ v1_funct_1(v22) | v3_binop_1(v23, v20) | v1_xboole_0(v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (k1_realset1(v22, v20) = v23) | ~ (k2_zfmisc_1(v20, v20) = v21) | ~ m1_subset_1(v20, v18) | ~ v2_binop_1(v22, v17) | ~ m2_relset_1(v23, v21, v20) | ~ m2_relset_1(v22, v19, v17) | ~ v1_funct_2(v23, v21, v20) | ~ v1_funct_2(v22, v19, v17) | ~ v1_funct_1(v23) | ~ v1_funct_1(v22) | v2_binop_1(v23, v20) | v1_xboole_0(v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ (k1_realset1(v22, v20) = v23) | ~ (k2_zfmisc_1(v20, v20) = v21) | ~ m1_subset_1(v20, v18) | ~ v1_binop_1(v22, v17) | ~ m2_relset_1(v23, v21, v20) | ~ m2_relset_1(v22, v19, v17) | ~ v1_funct_2(v23, v21, v20) | ~ v1_funct_2(v22, v19, v17) | ~ v1_funct_1(v23) | ~ v1_funct_1(v22) | v1_binop_1(v23, v20) | v1_xboole_0(v20)))) & ! [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] : (m1_subset_1(v19, v18) & v1_xboole_0(v19))) & ! [v17] : ! [v18] : ( ~ m1_subset_1(v17, v18) | r2_hidden(v17, v18) | v1_xboole_0(v18)) & ! [v17] : ! [v18] : ( ~ r2_hidden(v18, v17) | ~ r2_hidden(v17, v18)) & ! [v17] : ! [v18] : ( ~ r2_hidden(v17, v18) | ~ v1_xboole_0(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] : ( ~ v1_relat_1(v17) | ~ v1_funct_1(v17) | ~ v1_xboole_0(v17) | v2_funct_1(v17)) & ! [v17] : ( ~ v9_lattices(v17) | ~ v8_lattices(v17) | ~ v7_lattices(v17) | ~ v6_lattices(v17) | ~ v5_lattices(v17) | ~ v4_lattices(v17) | ~ l3_lattices(v17) | v10_lattices(v17) | v3_struct_0(v17)) & ! [v17] : ( ~ v1_xboole_0(v17) | v1_funct_1(v17)) & ! [v17] : ( ~ l3_lattices(v17) | ~ v10_lattices(v17) | v9_lattices(v17) | v3_struct_0(v17)) & ! [v17] : ( ~ l3_lattices(v17) | ~ v10_lattices(v17) | v8_lattices(v17) | v3_struct_0(v17)) & ! [v17] : ( ~ l3_lattices(v17) | ~ v10_lattices(v17) | v7_lattices(v17) | v3_struct_0(v17)) & ! [v17] : ( ~ l3_lattices(v17) | ~ v10_lattices(v17) | v6_lattices(v17) | v3_struct_0(v17)) & ! [v17] : ( ~ l3_lattices(v17) | ~ v10_lattices(v17) | v5_lattices(v17) | v3_struct_0(v17)) & ! [v17] : ( ~ l3_lattices(v17) | ~ v10_lattices(v17) | v4_lattices(v17) | v3_struct_0(v17)) & ! [v17] : ( ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v18] : (m2_lattice4(v18, v17) & ~ v1_xboole_0(v18))) & ! [v17] : ( ~ l3_lattices(v17) | ~ v10_lattices(v17) | v3_struct_0(v17) | ? [v18] : m2_lattice4(v18, v17)) & ! [v17] : ( ~ l3_lattices(v17) | l2_lattices(v17)) & ! [v17] : ( ~ l3_lattices(v17) | l1_lattices(v17)) & ? [v17] : ? [v18] : ? [v19] : m1_relset_1(v19, v17, v18) & ? [v17] : ? [v18] : ? [v19] : m2_relset_1(v19, v17, v18) & ? [v17] : ? [v18] : m1_subset_1(v18, v17) & ? [v17] : r1_tarski(v17, v17) & ( ~ r1_lattice2(v3, v6, v5) | ~ r1_lattice2(v3, v5, v6) | ~ v2_binop_1(v6, v3) | ~ v2_binop_1(v5, v3) | ~ v1_binop_1(v6, v3) | ~ v1_binop_1(v5, v3))) % 14.79/4.06 | 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: % 14.79/4.06 | (1) u2_lattices(all_0_16_16) = all_0_15_15 & u1_lattices(all_0_16_16) = all_0_14_14 & k1_realset1(all_0_14_14, all_0_13_13) = all_0_10_10 & k1_realset1(all_0_15_15, all_0_13_13) = all_0_11_11 & k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12 & l2_lattices(all_0_2_2) & l1_struct_0(all_0_1_1) & l1_struct_0(all_0_9_9) & l1_lattices(all_0_0_0) & v2_funct_1(all_0_8_8) & v1_relat_1(all_0_4_4) & v1_relat_1(all_0_6_6) & v1_relat_1(all_0_8_8) & m2_relset_1(all_0_10_10, all_0_12_12, all_0_13_13) & m2_relset_1(all_0_11_11, all_0_12_12, all_0_13_13) & v1_funct_2(all_0_10_10, all_0_12_12, all_0_13_13) & v1_funct_2(all_0_11_11, all_0_12_12, all_0_13_13) & v1_funct_1(all_0_4_4) & v1_funct_1(all_0_6_6) & v1_funct_1(all_0_8_8) & v1_funct_1(all_0_10_10) & v1_funct_1(all_0_11_11) & m2_lattice4(all_0_13_13, all_0_16_16) & v1_xboole_0(all_0_5_5) & v1_xboole_0(all_0_6_6) & v1_xboole_0(k1_xboole_0) & l3_lattices(all_0_3_3) & l3_lattices(all_0_16_16) & v10_lattices(all_0_16_16) & ~ v1_xboole_0(all_0_7_7) & ~ v1_xboole_0(all_0_13_13) & ~ v3_struct_0(all_0_9_9) & ~ v3_struct_0(all_0_16_16) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k7_relat_1(v3, v2) = v1) | ~ (k7_relat_1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k1_realset1(v3, v2) = v1) | ~ (k1_realset1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k2_zfmisc_1(v3, v2) = v1) | ~ (k2_zfmisc_1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k7_relat_1(v0, v2) = v3) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v1_relat_1(v0) | k1_realset1(v0, v1) = 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) | ~ m1_subset_1(v1, v3) | ~ r2_hidden(v0, v1) | ~ v1_xboole_0(v2)) & ! [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] : ( ~ (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 | ~ (u2_lattices(v2) = v1) | ~ (u2_lattices(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u1_lattices(v2) = v1) | ~ (u1_lattices(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v3_struct_0(v0) | ? [v3] : (u2_lattices(v0) = v3 & v1_partfun1(v3, v2, v1) & v1_relat_1(v3) & v2_binop_1(v3, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v3_struct_0(v0) | ? [v3] : (u2_lattices(v0) = v3 & v1_partfun1(v3, v2, v1) & v1_relat_1(v3) & v1_binop_1(v3, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ 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] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v3_struct_0(v0) | ? [v3] : (u1_lattices(v0) = v3 & v1_partfun1(v3, v2, v1) & v1_relat_1(v3) & v2_binop_1(v3, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v3_struct_0(v0) | ? [v3] : (u1_lattices(v0) = v3 & v1_partfun1(v3, v2, v1) & v1_relat_1(v3) & v1_binop_1(v3, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ 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] : ( ~ (k7_relat_1(v0, v1) = v2) | ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | v1_relat_1(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k7_relat_1(v0, v1) = v2) | ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | v1_funct_1(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k7_relat_1(v0, v1) = v2) | ~ v1_relat_1(v0) | v1_relat_1(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_realset1(v0, v1) = v2) | ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | v1_relat_1(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_realset1(v0, v1) = v2) | ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | v1_funct_1(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_realset1(v0, v1) = v2) | ~ v1_relat_1(v0) | v1_relat_1(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_realset1(v0, v1) = v2) | ~ v1_relat_1(v0) | ? [v3] : (k7_relat_1(v0, v3) = v2 & k2_zfmisc_1(v1, v1) = 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] : ( ~ 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] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v1_relat_1(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v1_funct_1(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & v1_partfun1(v1, v3, v2) & v2_binop_1(v1, v2) & v1_funct_2(v1, v3, v2))) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v1_relat_1(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v1_funct_1(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & v1_partfun1(v1, v3, v2) & v1_binop_1(v1, v2) & v1_funct_2(v1, v3, v2))) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | v1_funct_1(v1)) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v3 & u1_struct_0(v0) = v2 & r1_lattice2(v2, v3, v1))) & ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v3 & u1_struct_0(v0) = v2 & r1_lattice2(v2, v1, v3))) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v1_relat_1(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v1_funct_1(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & v1_partfun1(v1, v3, v2) & v2_binop_1(v1, v2) & v1_funct_2(v1, v3, v2))) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v1_relat_1(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v1_funct_1(v1) | v3_struct_0(v0)) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & v1_partfun1(v1, v3, v2) & v1_binop_1(v1, 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] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v3 & u1_struct_0(v0) = v2 & r1_lattice2(v2, v3, v1))) & ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v3 & u1_struct_0(v0) = v2 & r1_lattice2(v2, v1, v3))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & v1_partfun1(v2, v3, v1) & v1_relat_1(v2) & v2_binop_1(v2, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & v1_partfun1(v2, v3, v1) & v1_relat_1(v2) & v1_binop_1(v2, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & 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_lattices(v0) | ~ v7_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & v1_partfun1(v2, v3, v1) & v1_relat_1(v2) & v2_binop_1(v2, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & v1_partfun1(v2, v3, v1) & v1_relat_1(v2) & v1_binop_1(v2, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v3 & u1_lattices(v0) = v2 & r1_lattice2(v1, v2, v3))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v2 & u1_lattices(v0) = v3 & r1_lattice2(v1, v2, v3))) & ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : (k1_zfmisc_1(v1) = v2 & ! [v3] : ( ~ m2_lattice4(v3, v0) | m1_subset_1(v3, v2)))) & ! [v0] : ! [v1] : ( ~ (k2_zfmisc_1(v0, v0) = v1) | v1_xboole_0(v0) | ? [v2] : (k1_zfmisc_1(v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (k1_realset1(v7, v3) = v8) | ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v2) | ~ r1_lattice2(v0, v5, v7) | ~ m2_relset_1(v8, v4, v3) | ~ m2_relset_1(v7, v1, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v1, v0) | ~ v1_funct_2(v8, v4, v3) | ~ v1_funct_2(v7, v1, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_1(v8) | ~ v1_funct_1(v7) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | r1_lattice2(v3, v6, v8) | v1_xboole_0(v3)))) & ! [v0] : ! [v1] : ( ~ (k2_zfmisc_1(v0, v0) = v1) | v1_xboole_0(v0) | ? [v2] : (k1_zfmisc_1(v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ v3_binop_1(v5, v0) | ~ m1_subset_1(v3, v2) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v1, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v3_binop_1(v6, v3) | v1_xboole_0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v2) | ~ v2_binop_1(v5, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v1, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v2_binop_1(v6, v3) | v1_xboole_0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v2) | ~ v1_binop_1(v5, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v1, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v1_binop_1(v6, v3) | v1_xboole_0(v3)))) & ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ v1_xboole_0(v1)) & ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | v1_xboole_0(v0) | ? [v2] : (k2_zfmisc_1(v0, v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (k1_realset1(v7, v3) = v8) | ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v1) | ~ r1_lattice2(v0, v5, v7) | ~ m2_relset_1(v8, v4, v3) | ~ m2_relset_1(v7, v2, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v2, v0) | ~ v1_funct_2(v8, v4, v3) | ~ v1_funct_2(v7, v2, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v2, v0) | ~ v1_funct_1(v8) | ~ v1_funct_1(v7) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | r1_lattice2(v3, v6, v8) | v1_xboole_0(v3)))) & ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | v1_xboole_0(v0) | ? [v2] : (k2_zfmisc_1(v0, v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ v3_binop_1(v5, v0) | ~ m1_subset_1(v3, v1) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v2, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v2, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v3_binop_1(v6, v3) | v1_xboole_0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v1) | ~ v2_binop_1(v5, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v2, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v2, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v2_binop_1(v6, v3) | v1_xboole_0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v1) | ~ v1_binop_1(v5, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v2, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v2, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v1_binop_1(v6, v3) | v1_xboole_0(v3)))) & ! [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] : (m1_subset_1(v2, v1) & v1_xboole_0(v2))) & ! [v0] : ! [v1] : ( ~ m1_subset_1(v0, v1) | r2_hidden(v0, v1) | v1_xboole_0(v1)) & ! [v0] : ! [v1] : ( ~ r2_hidden(v1, v0) | ~ r2_hidden(v0, v1)) & ! [v0] : ! [v1] : ( ~ r2_hidden(v0, v1) | ~ v1_xboole_0(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] : ( ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | ~ v1_xboole_0(v0) | v2_funct_1(v0)) & ! [v0] : ( ~ v9_lattices(v0) | ~ v8_lattices(v0) | ~ v7_lattices(v0) | ~ v6_lattices(v0) | ~ v5_lattices(v0) | ~ v4_lattices(v0) | ~ l3_lattices(v0) | v10_lattices(v0) | v3_struct_0(v0)) & ! [v0] : ( ~ v1_xboole_0(v0) | v1_funct_1(v0)) & ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v9_lattices(v0) | v3_struct_0(v0)) & ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v8_lattices(v0) | v3_struct_0(v0)) & ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v7_lattices(v0) | v3_struct_0(v0)) & ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v6_lattices(v0) | v3_struct_0(v0)) & ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v5_lattices(v0) | v3_struct_0(v0)) & ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v4_lattices(v0) | v3_struct_0(v0)) & ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v1] : (m2_lattice4(v1, v0) & ~ v1_xboole_0(v1))) & ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v1] : m2_lattice4(v1, v0)) & ! [v0] : ( ~ l3_lattices(v0) | l2_lattices(v0)) & ! [v0] : ( ~ l3_lattices(v0) | l1_lattices(v0)) & ? [v0] : ? [v1] : ? [v2] : m1_relset_1(v2, v0, v1) & ? [v0] : ? [v1] : ? [v2] : m2_relset_1(v2, v0, v1) & ? [v0] : ? [v1] : m1_subset_1(v1, v0) & ? [v0] : r1_tarski(v0, v0) & ( ~ r1_lattice2(all_0_13_13, all_0_10_10, all_0_11_11) | ~ r1_lattice2(all_0_13_13, all_0_11_11, all_0_10_10) | ~ v2_binop_1(all_0_10_10, all_0_13_13) | ~ v2_binop_1(all_0_11_11, all_0_13_13) | ~ v1_binop_1(all_0_10_10, all_0_13_13) | ~ v1_binop_1(all_0_11_11, all_0_13_13)) % 14.79/4.08 | % 14.79/4.08 | Applying alpha-rule on (1) yields: % 14.79/4.08 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ m2_relset_1(v2, v0, v1) | m1_relset_1(v2, v0, v1)) % 14.79/4.08 | (3) ! [v0] : ! [v1] : ! [v2] : ( ~ m1_relset_1(v2, v0, v1) | m2_relset_1(v2, v0, v1)) % 14.79/4.08 | (4) ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v1] : (m2_lattice4(v1, v0) & ~ v1_xboole_0(v1))) % 14.79/4.08 | (5) ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ v1_xboole_0(v1)) % 14.79/4.08 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k2_zfmisc_1(v3, v2) = v1) | ~ (k2_zfmisc_1(v3, v2) = v0)) % 14.79/4.08 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l2_lattices(v0) | ? [v3] : (u2_lattices(v0) = v3 & m2_relset_1(v3, v2, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) % 14.79/4.08 | (8) ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | v1_xboole_0(v0) | ? [v2] : (m1_subset_1(v2, v1) & ~ v1_xboole_0(v2))) % 14.79/4.08 | (9) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & v1_partfun1(v2, v3, v1) & v1_relat_1(v2) & v2_binop_1(v2, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 14.79/4.08 | (10) v1_relat_1(all_0_8_8) % 14.79/4.08 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_realset1(v0, v1) = v2) | ~ v1_relat_1(v0) | v1_relat_1(v2)) % 14.79/4.08 | (12) ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | ? [v2] : (m1_subset_1(v2, v1) & v1_xboole_0(v2))) % 14.79/4.08 | (13) ! [v0] : ! [v1] : ( ~ r2_hidden(v0, v1) | m1_subset_1(v0, v1)) % 14.79/4.08 | (14) ! [v0] : ! [v1] : ( ~ (k2_zfmisc_1(v0, v0) = v1) | v1_xboole_0(v0) | ? [v2] : (k1_zfmisc_1(v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (k1_realset1(v7, v3) = v8) | ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v2) | ~ r1_lattice2(v0, v5, v7) | ~ m2_relset_1(v8, v4, v3) | ~ m2_relset_1(v7, v1, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v1, v0) | ~ v1_funct_2(v8, v4, v3) | ~ v1_funct_2(v7, v1, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_1(v8) | ~ v1_funct_1(v7) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | r1_lattice2(v3, v6, v8) | v1_xboole_0(v3)))) % 14.79/4.08 | (15) ! [v0] : ( ~ l1_lattices(v0) | l1_struct_0(v0)) % 14.79/4.08 | (16) ? [v0] : r1_tarski(v0, v0) % 14.79/4.08 | (17) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v2 & u1_lattices(v0) = v3 & r1_lattice2(v1, v2, v3))) % 14.79/4.08 | (18) ~ v1_xboole_0(all_0_13_13) % 14.79/4.08 | (19) l1_lattices(all_0_0_0) % 14.79/4.08 | (20) ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | v1_xboole_0(v0) | ? [v2] : (k2_zfmisc_1(v0, v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (k1_realset1(v7, v3) = v8) | ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v1) | ~ r1_lattice2(v0, v5, v7) | ~ m2_relset_1(v8, v4, v3) | ~ m2_relset_1(v7, v2, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v2, v0) | ~ v1_funct_2(v8, v4, v3) | ~ v1_funct_2(v7, v2, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v2, v0) | ~ v1_funct_1(v8) | ~ v1_funct_1(v7) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | r1_lattice2(v3, v6, v8) | v1_xboole_0(v3)))) % 15.15/4.09 | (21) ? [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))) % 15.15/4.09 | (22) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | v1_funct_1(v1)) % 15.15/4.09 | (23) v1_funct_1(all_0_11_11) % 15.15/4.09 | (24) v1_relat_1(all_0_6_6) % 15.15/4.09 | (25) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) % 15.15/4.09 | (26) ~ r1_lattice2(all_0_13_13, all_0_10_10, all_0_11_11) | ~ r1_lattice2(all_0_13_13, all_0_11_11, all_0_10_10) | ~ v2_binop_1(all_0_10_10, all_0_13_13) | ~ v2_binop_1(all_0_11_11, all_0_13_13) | ~ v1_binop_1(all_0_10_10, all_0_13_13) | ~ v1_binop_1(all_0_11_11, all_0_13_13) % 15.15/4.09 | (27) ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v7_lattices(v0) | v3_struct_0(v0)) % 15.15/4.09 | (28) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v1_relat_1(v1) | v3_struct_0(v0)) % 15.15/4.09 | (29) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & v1_partfun1(v1, v3, v2) & v2_binop_1(v1, v2) & v1_funct_2(v1, v3, v2))) % 15.15/4.09 | (30) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & v1_partfun1(v2, v3, v1) & v1_relat_1(v2) & v1_binop_1(v2, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 15.15/4.09 | (31) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_struct_0(v0) | ~ v1_xboole_0(v1) | v3_struct_0(v0)) % 15.15/4.09 | (32) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | v1_funct_1(v1)) % 15.15/4.09 | (33) u2_lattices(all_0_16_16) = all_0_15_15 % 15.15/4.09 | (34) ? [v0] : ? [v1] : ? [v2] : m2_relset_1(v2, v0, v1) % 15.15/4.09 | (35) ! [v0] : ( ~ v1_xboole_0(v0) | v1_funct_1(v0)) % 15.15/4.09 | (36) ! [v0] : ( ~ l3_lattices(v0) | l1_lattices(v0)) % 15.15/4.09 | (37) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u1_lattices(v2) = v1) | ~ (u1_lattices(v2) = v0)) % 15.15/4.09 | (38) ! [v0] : ! [v1] : ( ~ (k2_zfmisc_1(v0, v0) = v1) | v1_xboole_0(v0) | ? [v2] : (k1_zfmisc_1(v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ v3_binop_1(v5, v0) | ~ m1_subset_1(v3, v2) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v1, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v3_binop_1(v6, v3) | v1_xboole_0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v2) | ~ v2_binop_1(v5, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v1, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v2_binop_1(v6, v3) | v1_xboole_0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v2) | ~ v1_binop_1(v5, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v1, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v1_binop_1(v6, v3) | v1_xboole_0(v3)))) % 15.15/4.09 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k1_realset1(v3, v2) = v1) | ~ (k1_realset1(v3, v2) = v0)) % 15.15/4.09 | (40) ! [v0] : ! [v1] : ( ~ r2_hidden(v1, v0) | ~ r2_hidden(v0, v1)) % 15.15/4.09 | (41) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) % 15.15/4.09 | (42) ~ v1_xboole_0(all_0_7_7) % 15.15/4.09 | (43) v1_funct_2(all_0_11_11, all_0_12_12, all_0_13_13) % 15.15/4.09 | (44) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & v1_partfun1(v1, v3, v2) & v2_binop_1(v1, v2) & v1_funct_2(v1, v3, v2))) % 15.15/4.09 | (45) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & v1_partfun1(v2, v3, v1) & v1_relat_1(v2) & v1_binop_1(v2, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 15.15/4.09 | (46) ! [v0] : (v0 = k1_xboole_0 | ~ v1_xboole_0(v0)) % 15.15/4.09 | (47) ! [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))) % 15.15/4.09 | (48) l2_lattices(all_0_2_2) % 15.15/4.09 | (49) ? [v0] : ? [v1] : m1_subset_1(v1, v0) % 15.15/4.09 | (50) ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_realset1(v0, v1) = v2) | ~ v1_relat_1(v0) | ? [v3] : (k7_relat_1(v0, v3) = v2 & k2_zfmisc_1(v1, v1) = v3)) % 15.15/4.09 | (51) ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v1] : m2_lattice4(v1, v0)) % 15.15/4.09 | (52) v1_xboole_0(all_0_6_6) % 15.15/4.09 | (53) ! [v0] : ! [v1] : ! [v2] : ( ~ (k7_relat_1(v0, v1) = v2) | ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | v1_relat_1(v2)) % 15.15/4.09 | (54) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_zfmisc_1(v2) = v3) | ~ m1_subset_1(v1, v3) | ~ r2_hidden(v0, v1) | m1_subset_1(v0, v2)) % 15.15/4.09 | (55) ! [v0] : ! [v1] : ( ~ m1_subset_1(v0, v1) | r2_hidden(v0, v1) | v1_xboole_0(v1)) % 15.15/4.09 | (56) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v3 & u1_lattices(v0) = v2 & r1_lattice2(v1, v2, v3))) % 15.15/4.09 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k7_relat_1(v0, v2) = v3) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v1_relat_1(v0) | k1_realset1(v0, v1) = v3) % 15.15/4.09 | (58) ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v3_struct_0(v0) | ? [v3] : (u1_lattices(v0) = v3 & v1_partfun1(v3, v2, v1) & v1_relat_1(v3) & v1_binop_1(v3, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) % 15.15/4.09 | (59) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v1_funct_1(v1) | v3_struct_0(v0)) % 15.15/4.09 | (60) ! [v0] : ! [v1] : ( ~ r2_hidden(v0, v1) | ~ v1_xboole_0(v1)) % 15.15/4.09 | (61) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v1_relat_1(v1) | v3_struct_0(v0)) % 15.15/4.10 | (62) ! [v0] : ( ~ v9_lattices(v0) | ~ v8_lattices(v0) | ~ v7_lattices(v0) | ~ v6_lattices(v0) | ~ v5_lattices(v0) | ~ v4_lattices(v0) | ~ l3_lattices(v0) | v10_lattices(v0) | v3_struct_0(v0)) % 15.15/4.10 | (63) ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v3_struct_0(v0) | ? [v3] : (u2_lattices(v0) = v3 & v1_partfun1(v3, v2, v1) & v1_relat_1(v3) & v2_binop_1(v3, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) % 15.15/4.10 | (64) v1_funct_1(all_0_6_6) % 15.15/4.10 | (65) ! [v0] : ! [v1] : ! [v2] : ( ~ (k2_zfmisc_1(v0, v1) = v2) | ~ v1_xboole_0(v2) | v1_xboole_0(v1) | v1_xboole_0(v0)) % 15.15/4.10 | (66) ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_zfmisc_1(v1) = v2) | ~ m1_subset_1(v0, v2) | r1_tarski(v0, v1)) % 15.15/4.10 | (67) ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_zfmisc_1(v1) = v2) | ~ r1_tarski(v0, v1) | m1_subset_1(v0, v2)) % 15.15/4.10 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_zfmisc_1(v2) = v3) | ~ m1_subset_1(v1, v3) | ~ r2_hidden(v0, v1) | ~ v1_xboole_0(v2)) % 15.15/4.10 | (69) ! [v0] : ! [v1] : ( ~ (k1_zfmisc_1(v0) = v1) | v1_xboole_0(v0) | ? [v2] : (k2_zfmisc_1(v0, v0) = v2 & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ v3_binop_1(v5, v0) | ~ m1_subset_1(v3, v1) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v2, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v2, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v3_binop_1(v6, v3) | v1_xboole_0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v1) | ~ v2_binop_1(v5, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v2, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v2, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v2_binop_1(v6, v3) | v1_xboole_0(v3)) & ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v3) = v6) | ~ (k2_zfmisc_1(v3, v3) = v4) | ~ m1_subset_1(v3, v1) | ~ v1_binop_1(v5, v0) | ~ m2_relset_1(v6, v4, v3) | ~ m2_relset_1(v5, v2, v0) | ~ v1_funct_2(v6, v4, v3) | ~ v1_funct_2(v5, v2, v0) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | v1_binop_1(v6, v3) | v1_xboole_0(v3)))) % 15.15/4.10 | (70) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v1_relat_1(v1) | v3_struct_0(v0)) % 15.15/4.10 | (71) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 15.15/4.10 | (72) v2_funct_1(all_0_8_8) % 15.15/4.10 | (73) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v1_relat_1(v1) | v3_struct_0(v0)) % 15.15/4.10 | (74) k1_realset1(all_0_15_15, all_0_13_13) = all_0_11_11 % 15.15/4.10 | (75) k1_realset1(all_0_14_14, all_0_13_13) = all_0_10_10 % 15.15/4.10 | (76) ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_realset1(v0, v1) = v2) | ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | v1_relat_1(v2)) % 15.15/4.10 | (77) ~ v3_struct_0(all_0_16_16) % 15.15/4.10 | (78) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) % 15.15/4.10 | (79) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v5_lattices(v0) | v1_funct_1(v1) | v3_struct_0(v0)) % 15.15/4.10 | (80) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (k7_relat_1(v3, v2) = v1) | ~ (k7_relat_1(v3, v2) = v0)) % 15.15/4.10 | (81) m2_relset_1(all_0_10_10, all_0_12_12, all_0_13_13) % 15.15/4.10 | (82) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & v1_partfun1(v1, v3, v2) & v1_binop_1(v1, v2) & v1_funct_2(v1, v3, v2))) % 15.15/4.10 | (83) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u2_lattices(v2) = v1) | ~ (u2_lattices(v2) = v0)) % 15.15/4.10 | (84) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & v1_partfun1(v2, v3, v1) & v1_relat_1(v2) & v2_binop_1(v2, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 15.15/4.10 | (85) v1_relat_1(all_0_4_4) % 15.15/4.10 | (86) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v3 & u1_struct_0(v0) = v2 & r1_lattice2(v2, v3, v1))) % 15.15/4.10 | (87) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v3 & u1_struct_0(v0) = v2 & r1_lattice2(v2, v3, v1))) % 15.15/4.10 | (88) ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v5_lattices(v0) | v3_struct_0(v0)) % 15.15/4.10 | (89) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & v1_partfun1(v1, v3, v2) & v1_binop_1(v1, v2) & v1_funct_2(v1, v3, v2))) % 15.15/4.10 | (90) ! [v0] : ( ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | ~ v1_xboole_0(v0) | v2_funct_1(v0)) % 15.15/4.10 | (91) v1_funct_1(all_0_4_4) % 15.15/4.10 | (92) ! [v0] : ! [v1] : ! [v2] : ( ~ (k1_realset1(v0, v1) = v2) | ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | v1_funct_1(v2)) % 15.15/4.10 | (93) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : (k1_zfmisc_1(v1) = v2 & ! [v3] : ( ~ m2_lattice4(v3, v0) | m1_subset_1(v3, v2)))) % 15.15/4.10 | (94) ! [v0] : ( ~ l3_lattices(v0) | l2_lattices(v0)) % 15.15/4.10 | (95) v1_xboole_0(k1_xboole_0) % 15.15/4.10 | (96) v1_xboole_0(all_0_5_5) % 15.15/4.10 | (97) ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l1_lattices(v0) | ~ v7_lattices(v0) | v3_struct_0(v0) | ? [v3] : (u1_lattices(v0) = v3 & v1_partfun1(v3, v2, v1) & v1_relat_1(v3) & v2_binop_1(v3, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) % 15.15/4.10 | (98) m2_lattice4(all_0_13_13, all_0_16_16) % 15.15/4.10 | (99) ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v6_lattices(v0) | v3_struct_0(v0)) % 15.15/4.11 | (100) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12 % 15.15/4.11 | (101) v1_funct_1(all_0_8_8) % 15.15/4.11 | (102) ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v9_lattices(v0) | v3_struct_0(v0)) % 15.15/4.11 | (103) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l1_lattices(v0) | ~ v6_lattices(v0) | v1_funct_1(v1) | v3_struct_0(v0)) % 15.15/4.11 | (104) v1_funct_1(all_0_10_10) % 15.15/4.11 | (105) ! [v0] : ! [v1] : (v1 = v0 | ~ v1_xboole_0(v1) | ~ v1_xboole_0(v0)) % 15.15/4.11 | (106) ! [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))) % 15.15/4.11 | (107) ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v3_struct_0(v0) | ? [v3] : (u2_lattices(v0) = v3 & v1_partfun1(v3, v2, v1) & v1_relat_1(v3) & v1_binop_1(v3, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) % 15.15/4.11 | (108) u1_lattices(all_0_16_16) = all_0_14_14 % 15.15/4.11 | (109) ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v4_lattices(v0) | v3_struct_0(v0)) % 15.15/4.11 | (110) v10_lattices(all_0_16_16) % 15.15/4.11 | (111) v1_funct_2(all_0_10_10, all_0_12_12, all_0_13_13) % 15.15/4.11 | (112) ! [v0] : ! [v1] : ! [v2] : ( ~ (k7_relat_1(v0, v1) = v2) | ~ v1_relat_1(v0) | ~ v1_funct_1(v0) | v1_funct_1(v2)) % 15.15/4.11 | (113) ! [v0] : ! [v1] : ! [v2] : ( ~ (u1_struct_0(v0) = v1) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ l1_lattices(v0) | ? [v3] : (u1_lattices(v0) = v3 & m2_relset_1(v3, v2, v1) & v1_funct_2(v3, v2, v1) & v1_funct_1(v3))) % 15.15/4.11 | (114) ! [v0] : ! [v1] : ! [v2] : ( ~ (k7_relat_1(v0, v1) = v2) | ~ v1_relat_1(v0) | v1_relat_1(v2)) % 15.15/4.11 | (115) ~ v3_struct_0(all_0_9_9) % 15.15/4.11 | (116) m2_relset_1(all_0_11_11, all_0_12_12, all_0_13_13) % 15.15/4.11 | (117) ! [v0] : ! [v1] : ( ~ (u1_lattices(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v3 & u1_struct_0(v0) = v2 & r1_lattice2(v2, v1, v3))) % 15.15/4.11 | (118) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l3_lattices(v0) | ~ v10_lattices(v0) | v3_struct_0(v0) | ? [v2] : ? [v3] : (u1_lattices(v0) = v3 & u1_struct_0(v0) = v2 & r1_lattice2(v2, v1, v3))) % 15.15/4.11 | (119) ! [v0] : ( ~ l2_lattices(v0) | l1_struct_0(v0)) % 15.15/4.11 | (120) ! [v0] : ! [v1] : ( ~ (u1_struct_0(v0) = v1) | ~ l2_lattices(v0) | ? [v2] : ? [v3] : (u2_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 15.15/4.11 | (121) l3_lattices(all_0_3_3) % 15.15/4.11 | (122) ! [v0] : ( ~ l3_lattices(v0) | ~ v10_lattices(v0) | v8_lattices(v0) | v3_struct_0(v0)) % 15.15/4.11 | (123) l1_struct_0(all_0_1_1) % 15.15/4.11 | (124) l3_lattices(all_0_16_16) % 15.15/4.11 | (125) ! [v0] : ! [v1] : ( ~ (u2_lattices(v0) = v1) | ~ l2_lattices(v0) | ~ v4_lattices(v0) | v1_funct_1(v1) | v3_struct_0(v0)) % 15.15/4.11 | (126) ? [v0] : ? [v1] : ? [v2] : m1_relset_1(v2, v0, v1) % 15.15/4.11 | (127) l1_struct_0(all_0_9_9) % 15.15/4.11 | (128) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) % 15.15/4.11 | % 15.15/4.11 | Instantiating formula (14) with all_0_12_12, all_0_13_13 and discharging atoms k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, ~ v1_xboole_0(all_0_13_13), yields: % 15.15/4.11 | (129) ? [v0] : (k1_zfmisc_1(all_0_13_13) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v1) = v6) | ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ r1_lattice2(all_0_13_13, v3, v5) | ~ m2_relset_1(v6, v2, v1) | ~ m2_relset_1(v5, all_0_12_12, all_0_13_13) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v6, v2, v1) | ~ v1_funct_2(v5, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | r1_lattice2(v1, v4, v6) | v1_xboole_0(v1))) % 15.15/4.11 | % 15.15/4.11 | Instantiating formula (38) with all_0_12_12, all_0_13_13 and discharging atoms k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, ~ v1_xboole_0(all_0_13_13), yields: % 15.15/4.11 | (130) ? [v0] : (k1_zfmisc_1(all_0_13_13) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v3_binop_1(v3, all_0_13_13) | ~ m1_subset_1(v1, v0) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v3_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ v2_binop_1(v3, all_0_13_13) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v2_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ v1_binop_1(v3, all_0_13_13) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v1_binop_1(v4, v1) | v1_xboole_0(v1))) % 15.15/4.11 | % 15.15/4.11 | Instantiating formula (94) with all_0_16_16 and discharging atoms l3_lattices(all_0_16_16), yields: % 15.15/4.11 | (131) l2_lattices(all_0_16_16) % 15.15/4.11 | % 15.15/4.11 | Instantiating formula (36) with all_0_16_16 and discharging atoms l3_lattices(all_0_16_16), yields: % 15.15/4.11 | (132) l1_lattices(all_0_16_16) % 15.15/4.12 | % 15.15/4.12 | Instantiating formula (87) with all_0_15_15, all_0_16_16 and discharging atoms u2_lattices(all_0_16_16) = all_0_15_15, l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.12 | (133) ? [v0] : ? [v1] : (u1_lattices(all_0_16_16) = v1 & u1_struct_0(all_0_16_16) = v0 & r1_lattice2(v0, v1, all_0_15_15)) % 15.15/4.12 | % 15.15/4.12 | Instantiating formula (118) with all_0_15_15, all_0_16_16 and discharging atoms u2_lattices(all_0_16_16) = all_0_15_15, l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.12 | (134) ? [v0] : ? [v1] : (u1_lattices(all_0_16_16) = v1 & u1_struct_0(all_0_16_16) = v0 & r1_lattice2(v0, all_0_15_15, v1)) % 15.15/4.12 | % 15.15/4.12 | Instantiating formula (86) with all_0_14_14, all_0_16_16 and discharging atoms u1_lattices(all_0_16_16) = all_0_14_14, l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.12 | (135) ? [v0] : ? [v1] : (u2_lattices(all_0_16_16) = v1 & u1_struct_0(all_0_16_16) = v0 & r1_lattice2(v0, v1, all_0_14_14)) % 15.15/4.12 | % 15.15/4.12 | Instantiating formula (117) with all_0_14_14, all_0_16_16 and discharging atoms u1_lattices(all_0_16_16) = all_0_14_14, l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.12 | (136) ? [v0] : ? [v1] : (u2_lattices(all_0_16_16) = v1 & u1_struct_0(all_0_16_16) = v0 & r1_lattice2(v0, all_0_14_14, v1)) % 15.15/4.12 | % 15.15/4.12 | Instantiating formula (27) with all_0_16_16 and discharging atoms l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.12 | (137) v7_lattices(all_0_16_16) % 15.15/4.12 | % 15.15/4.12 | Instantiating formula (99) with all_0_16_16 and discharging atoms l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.12 | (138) v6_lattices(all_0_16_16) % 15.15/4.12 | % 15.15/4.12 | Instantiating formula (88) with all_0_16_16 and discharging atoms l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.12 | (139) v5_lattices(all_0_16_16) % 15.15/4.12 | % 15.15/4.12 | Instantiating formula (109) with all_0_16_16 and discharging atoms l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.12 | (140) v4_lattices(all_0_16_16) % 15.15/4.12 | % 15.15/4.12 | Instantiating (136) with all_23_0_27, all_23_1_28 yields: % 15.15/4.12 | (141) u2_lattices(all_0_16_16) = all_23_0_27 & u1_struct_0(all_0_16_16) = all_23_1_28 & r1_lattice2(all_23_1_28, all_0_14_14, all_23_0_27) % 15.15/4.12 | % 15.15/4.12 | Applying alpha-rule on (141) yields: % 15.15/4.12 | (142) u2_lattices(all_0_16_16) = all_23_0_27 % 15.15/4.12 | (143) u1_struct_0(all_0_16_16) = all_23_1_28 % 15.15/4.12 | (144) r1_lattice2(all_23_1_28, all_0_14_14, all_23_0_27) % 15.15/4.12 | % 15.15/4.12 | Instantiating (135) with all_25_0_29, all_25_1_30 yields: % 15.15/4.12 | (145) u2_lattices(all_0_16_16) = all_25_0_29 & u1_struct_0(all_0_16_16) = all_25_1_30 & r1_lattice2(all_25_1_30, all_25_0_29, all_0_14_14) % 15.15/4.12 | % 15.15/4.12 | Applying alpha-rule on (145) yields: % 15.15/4.12 | (146) u2_lattices(all_0_16_16) = all_25_0_29 % 15.15/4.12 | (147) u1_struct_0(all_0_16_16) = all_25_1_30 % 15.15/4.12 | (148) r1_lattice2(all_25_1_30, all_25_0_29, all_0_14_14) % 15.15/4.12 | % 15.15/4.12 | Instantiating (134) with all_29_0_32, all_29_1_33 yields: % 15.15/4.12 | (149) u1_lattices(all_0_16_16) = all_29_0_32 & u1_struct_0(all_0_16_16) = all_29_1_33 & r1_lattice2(all_29_1_33, all_0_15_15, all_29_0_32) % 15.15/4.12 | % 15.15/4.12 | Applying alpha-rule on (149) yields: % 15.15/4.12 | (150) u1_lattices(all_0_16_16) = all_29_0_32 % 15.15/4.12 | (151) u1_struct_0(all_0_16_16) = all_29_1_33 % 15.15/4.12 | (152) r1_lattice2(all_29_1_33, all_0_15_15, all_29_0_32) % 15.15/4.12 | % 15.15/4.12 | Instantiating (130) with all_31_0_34 yields: % 15.15/4.12 | (153) k1_zfmisc_1(all_0_13_13) = all_31_0_34 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ v3_binop_1(v2, all_0_13_13) | ~ m1_subset_1(v0, all_31_0_34) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v3_binop_1(v3, v0) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ v2_binop_1(v2, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v2_binop_1(v3, v0) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ v1_binop_1(v2, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v1_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.15/4.12 | % 15.15/4.12 | Applying alpha-rule on (153) yields: % 15.15/4.12 | (154) k1_zfmisc_1(all_0_13_13) = all_31_0_34 % 15.15/4.12 | (155) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ v3_binop_1(v2, all_0_13_13) | ~ m1_subset_1(v0, all_31_0_34) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v3_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.15/4.12 | (156) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ v2_binop_1(v2, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v2_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.15/4.12 | (157) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ v1_binop_1(v2, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v1_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.15/4.12 | % 15.15/4.12 | Instantiating (129) with all_34_0_35 yields: % 15.15/4.12 | (158) k1_zfmisc_1(all_0_13_13) = all_34_0_35 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (k1_realset1(v4, v0) = v5) | ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_34_0_35) | ~ r1_lattice2(all_0_13_13, v2, v4) | ~ m2_relset_1(v5, v1, v0) | ~ m2_relset_1(v4, all_0_12_12, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_2(v4, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | r1_lattice2(v0, v3, v5) | v1_xboole_0(v0)) % 15.15/4.13 | % 15.15/4.13 | Applying alpha-rule on (158) yields: % 15.15/4.13 | (159) k1_zfmisc_1(all_0_13_13) = all_34_0_35 % 15.15/4.13 | (160) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (k1_realset1(v4, v0) = v5) | ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_34_0_35) | ~ r1_lattice2(all_0_13_13, v2, v4) | ~ m2_relset_1(v5, v1, v0) | ~ m2_relset_1(v4, all_0_12_12, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_2(v4, all_0_12_12, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_0_12_12, all_0_13_13) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | r1_lattice2(v0, v3, v5) | v1_xboole_0(v0)) % 15.15/4.13 | % 15.15/4.13 | Instantiating (133) with all_37_0_36, all_37_1_37 yields: % 15.15/4.13 | (161) u1_lattices(all_0_16_16) = all_37_0_36 & u1_struct_0(all_0_16_16) = all_37_1_37 & r1_lattice2(all_37_1_37, all_37_0_36, all_0_15_15) % 15.15/4.13 | % 15.15/4.13 | Applying alpha-rule on (161) yields: % 15.15/4.13 | (162) u1_lattices(all_0_16_16) = all_37_0_36 % 15.15/4.13 | (163) u1_struct_0(all_0_16_16) = all_37_1_37 % 15.15/4.13 | (164) r1_lattice2(all_37_1_37, all_37_0_36, all_0_15_15) % 15.15/4.13 | % 15.15/4.13 | Instantiating formula (83) with all_0_16_16, all_25_0_29, all_0_15_15 and discharging atoms u2_lattices(all_0_16_16) = all_25_0_29, u2_lattices(all_0_16_16) = all_0_15_15, yields: % 15.15/4.13 | (165) all_25_0_29 = all_0_15_15 % 15.15/4.13 | % 15.15/4.13 | Instantiating formula (83) with all_0_16_16, all_23_0_27, all_25_0_29 and discharging atoms u2_lattices(all_0_16_16) = all_25_0_29, u2_lattices(all_0_16_16) = all_23_0_27, yields: % 15.15/4.13 | (166) all_25_0_29 = all_23_0_27 % 15.15/4.13 | % 15.15/4.13 | Instantiating formula (37) with all_0_16_16, all_37_0_36, all_0_14_14 and discharging atoms u1_lattices(all_0_16_16) = all_37_0_36, u1_lattices(all_0_16_16) = all_0_14_14, yields: % 15.15/4.13 | (167) all_37_0_36 = all_0_14_14 % 15.15/4.13 | % 15.15/4.13 | Instantiating formula (37) with all_0_16_16, all_29_0_32, all_37_0_36 and discharging atoms u1_lattices(all_0_16_16) = all_37_0_36, u1_lattices(all_0_16_16) = all_29_0_32, yields: % 15.15/4.13 | (168) all_37_0_36 = all_29_0_32 % 15.15/4.13 | % 15.15/4.13 | Instantiating formula (128) with all_0_16_16, all_29_1_33, all_37_1_37 and discharging atoms u1_struct_0(all_0_16_16) = all_37_1_37, u1_struct_0(all_0_16_16) = all_29_1_33, yields: % 15.15/4.13 | (169) all_37_1_37 = all_29_1_33 % 15.15/4.13 | % 15.15/4.13 | Instantiating formula (128) with all_0_16_16, all_25_1_30, all_29_1_33 and discharging atoms u1_struct_0(all_0_16_16) = all_29_1_33, u1_struct_0(all_0_16_16) = all_25_1_30, yields: % 15.15/4.13 | (170) all_29_1_33 = all_25_1_30 % 15.15/4.13 | % 15.15/4.13 | Instantiating formula (128) with all_0_16_16, all_23_1_28, all_37_1_37 and discharging atoms u1_struct_0(all_0_16_16) = all_37_1_37, u1_struct_0(all_0_16_16) = all_23_1_28, yields: % 15.15/4.13 | (171) all_37_1_37 = all_23_1_28 % 15.15/4.13 | % 15.15/4.13 | Instantiating formula (41) with all_0_13_13, all_31_0_34, all_34_0_35 and discharging atoms k1_zfmisc_1(all_0_13_13) = all_34_0_35, k1_zfmisc_1(all_0_13_13) = all_31_0_34, yields: % 15.15/4.13 | (172) all_34_0_35 = all_31_0_34 % 15.15/4.13 | % 15.15/4.13 | Combining equations (168,167) yields a new equation: % 15.15/4.13 | (173) all_29_0_32 = all_0_14_14 % 15.15/4.13 | % 15.15/4.13 | Simplifying 173 yields: % 15.15/4.13 | (174) all_29_0_32 = all_0_14_14 % 15.15/4.13 | % 15.15/4.13 | Combining equations (169,171) yields a new equation: % 15.15/4.13 | (175) all_29_1_33 = all_23_1_28 % 15.15/4.13 | % 15.15/4.13 | Simplifying 175 yields: % 15.15/4.13 | (176) all_29_1_33 = all_23_1_28 % 15.15/4.13 | % 15.15/4.13 | Combining equations (170,176) yields a new equation: % 15.15/4.13 | (177) all_25_1_30 = all_23_1_28 % 15.15/4.13 | % 15.15/4.13 | Simplifying 177 yields: % 15.15/4.13 | (178) all_25_1_30 = all_23_1_28 % 15.15/4.13 | % 15.15/4.13 | Combining equations (166,165) yields a new equation: % 15.15/4.14 | (179) all_23_0_27 = all_0_15_15 % 15.15/4.14 | % 15.15/4.14 | Simplifying 179 yields: % 15.15/4.14 | (180) all_23_0_27 = all_0_15_15 % 15.15/4.14 | % 15.15/4.14 | From (180) and (142) follows: % 15.15/4.14 | (33) u2_lattices(all_0_16_16) = all_0_15_15 % 15.15/4.14 | % 15.15/4.14 | From (174) and (150) follows: % 15.15/4.14 | (108) u1_lattices(all_0_16_16) = all_0_14_14 % 15.15/4.14 | % 15.15/4.14 | From (178) and (147) follows: % 15.15/4.14 | (143) u1_struct_0(all_0_16_16) = all_23_1_28 % 15.15/4.14 | % 15.15/4.14 | From (172) and (159) follows: % 15.15/4.14 | (154) k1_zfmisc_1(all_0_13_13) = all_31_0_34 % 15.15/4.14 | % 15.15/4.14 | From (178)(165) and (148) follows: % 15.15/4.14 | (185) r1_lattice2(all_23_1_28, all_0_15_15, all_0_14_14) % 15.15/4.14 | % 15.15/4.14 | From (180) and (144) follows: % 15.15/4.14 | (186) r1_lattice2(all_23_1_28, all_0_14_14, all_0_15_15) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (93) with all_23_1_28, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_23_1_28, l3_lattices(all_0_16_16), v10_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.14 | (187) ? [v0] : (k1_zfmisc_1(all_23_1_28) = v0 & ! [v1] : ( ~ m2_lattice4(v1, all_0_16_16) | m1_subset_1(v1, v0))) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (20) with all_31_0_34, all_0_13_13 and discharging atoms k1_zfmisc_1(all_0_13_13) = all_31_0_34, ~ v1_xboole_0(all_0_13_13), yields: % 15.15/4.14 | (188) ? [v0] : (k2_zfmisc_1(all_0_13_13, all_0_13_13) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v1) = v6) | ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_31_0_34) | ~ r1_lattice2(all_0_13_13, v3, v5) | ~ m2_relset_1(v6, v2, v1) | ~ m2_relset_1(v5, v0, all_0_13_13) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_0_13_13) | ~ v1_funct_2(v6, v2, v1) | ~ v1_funct_2(v5, v0, all_0_13_13) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_0_13_13) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | r1_lattice2(v1, v4, v6) | v1_xboole_0(v1))) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (69) with all_31_0_34, all_0_13_13 and discharging atoms k1_zfmisc_1(all_0_13_13) = all_31_0_34, ~ v1_xboole_0(all_0_13_13), yields: % 15.15/4.14 | (189) ? [v0] : (k2_zfmisc_1(all_0_13_13, all_0_13_13) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v3_binop_1(v3, all_0_13_13) | ~ m1_subset_1(v1, all_31_0_34) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_0_13_13) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_0_13_13) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v3_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_31_0_34) | ~ v2_binop_1(v3, all_0_13_13) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_0_13_13) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_0_13_13) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v2_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_31_0_34) | ~ v1_binop_1(v3, all_0_13_13) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_0_13_13) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_0_13_13) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v1_binop_1(v4, v1) | v1_xboole_0(v1))) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (120) with all_23_1_28, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_23_1_28, l2_lattices(all_0_16_16), yields: % 15.15/4.14 | (190) ? [v0] : ? [v1] : (u2_lattices(all_0_16_16) = v0 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = v1 & m2_relset_1(v0, v1, all_23_1_28) & v1_funct_2(v0, v1, all_23_1_28) & v1_funct_1(v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (25) with all_0_15_15, all_0_16_16 and discharging atoms u2_lattices(all_0_16_16) = all_0_15_15, l2_lattices(all_0_16_16), yields: % 15.15/4.14 | (191) ? [v0] : ? [v1] : (u1_struct_0(all_0_16_16) = v0 & k2_zfmisc_1(v0, v0) = v1 & m2_relset_1(all_0_15_15, v1, v0) & v1_funct_2(all_0_15_15, v1, v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (71) with all_23_1_28, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_23_1_28, l1_lattices(all_0_16_16), yields: % 15.15/4.14 | (192) ? [v0] : ? [v1] : (u1_lattices(all_0_16_16) = v0 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = v1 & m2_relset_1(v0, v1, all_23_1_28) & v1_funct_2(v0, v1, all_23_1_28) & v1_funct_1(v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (78) with all_0_14_14, all_0_16_16 and discharging atoms u1_lattices(all_0_16_16) = all_0_14_14, l1_lattices(all_0_16_16), yields: % 15.15/4.14 | (193) ? [v0] : ? [v1] : (u1_struct_0(all_0_16_16) = v0 & k2_zfmisc_1(v0, v0) = v1 & m2_relset_1(all_0_14_14, v1, v0) & v1_funct_2(all_0_14_14, v1, v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (15) with all_0_16_16 and discharging atoms l1_lattices(all_0_16_16), yields: % 15.15/4.14 | (194) l1_struct_0(all_0_16_16) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (84) with all_23_1_28, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_23_1_28, l1_lattices(all_0_16_16), v7_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.14 | (195) ? [v0] : ? [v1] : (u1_lattices(all_0_16_16) = v0 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = v1 & v1_partfun1(v0, v1, all_23_1_28) & v1_relat_1(v0) & v2_binop_1(v0, all_23_1_28) & v1_funct_2(v0, v1, all_23_1_28) & v1_funct_1(v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (44) with all_0_14_14, all_0_16_16 and discharging atoms u1_lattices(all_0_16_16) = all_0_14_14, l1_lattices(all_0_16_16), v7_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.14 | (196) ? [v0] : ? [v1] : (u1_struct_0(all_0_16_16) = v0 & k2_zfmisc_1(v0, v0) = v1 & v1_partfun1(all_0_14_14, v1, v0) & v2_binop_1(all_0_14_14, v0) & v1_funct_2(all_0_14_14, v1, v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (45) with all_23_1_28, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_23_1_28, l1_lattices(all_0_16_16), v6_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.14 | (197) ? [v0] : ? [v1] : (u1_lattices(all_0_16_16) = v0 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = v1 & v1_partfun1(v0, v1, all_23_1_28) & v1_relat_1(v0) & v1_binop_1(v0, all_23_1_28) & v1_funct_2(v0, v1, all_23_1_28) & v1_funct_1(v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (89) with all_0_14_14, all_0_16_16 and discharging atoms u1_lattices(all_0_16_16) = all_0_14_14, l1_lattices(all_0_16_16), v6_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.14 | (198) ? [v0] : ? [v1] : (u1_struct_0(all_0_16_16) = v0 & k2_zfmisc_1(v0, v0) = v1 & v1_partfun1(all_0_14_14, v1, v0) & v1_binop_1(all_0_14_14, v0) & v1_funct_2(all_0_14_14, v1, v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (9) with all_23_1_28, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_23_1_28, l2_lattices(all_0_16_16), v5_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.14 | (199) ? [v0] : ? [v1] : (u2_lattices(all_0_16_16) = v0 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = v1 & v1_partfun1(v0, v1, all_23_1_28) & v1_relat_1(v0) & v2_binop_1(v0, all_23_1_28) & v1_funct_2(v0, v1, all_23_1_28) & v1_funct_1(v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (29) with all_0_15_15, all_0_16_16 and discharging atoms u2_lattices(all_0_16_16) = all_0_15_15, l2_lattices(all_0_16_16), v5_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.14 | (200) ? [v0] : ? [v1] : (u1_struct_0(all_0_16_16) = v0 & k2_zfmisc_1(v0, v0) = v1 & v1_partfun1(all_0_15_15, v1, v0) & v2_binop_1(all_0_15_15, v0) & v1_funct_2(all_0_15_15, v1, v0)) % 15.15/4.14 | % 15.15/4.14 | Instantiating formula (30) with all_23_1_28, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_23_1_28, l2_lattices(all_0_16_16), v4_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.14 | (201) ? [v0] : ? [v1] : (u2_lattices(all_0_16_16) = v0 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = v1 & v1_partfun1(v0, v1, all_23_1_28) & v1_relat_1(v0) & v1_binop_1(v0, all_23_1_28) & v1_funct_2(v0, v1, all_23_1_28) & v1_funct_1(v0)) % 15.15/4.15 | % 15.15/4.15 | Instantiating formula (82) with all_0_15_15, all_0_16_16 and discharging atoms u2_lattices(all_0_16_16) = all_0_15_15, l2_lattices(all_0_16_16), v4_lattices(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.15 | (202) ? [v0] : ? [v1] : (u1_struct_0(all_0_16_16) = v0 & k2_zfmisc_1(v0, v0) = v1 & v1_partfun1(all_0_15_15, v1, v0) & v1_binop_1(all_0_15_15, v0) & v1_funct_2(all_0_15_15, v1, v0)) % 15.15/4.15 | % 15.15/4.15 | Instantiating (195) with all_51_0_39, all_51_1_40 yields: % 15.15/4.15 | (203) u1_lattices(all_0_16_16) = all_51_1_40 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_51_0_39 & v1_partfun1(all_51_1_40, all_51_0_39, all_23_1_28) & v1_relat_1(all_51_1_40) & v2_binop_1(all_51_1_40, all_23_1_28) & v1_funct_2(all_51_1_40, all_51_0_39, all_23_1_28) & v1_funct_1(all_51_1_40) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (203) yields: % 15.15/4.15 | (204) v2_binop_1(all_51_1_40, all_23_1_28) % 15.15/4.15 | (205) u1_lattices(all_0_16_16) = all_51_1_40 % 15.15/4.15 | (206) v1_funct_2(all_51_1_40, all_51_0_39, all_23_1_28) % 15.15/4.15 | (207) v1_partfun1(all_51_1_40, all_51_0_39, all_23_1_28) % 15.15/4.15 | (208) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_51_0_39 % 15.15/4.15 | (209) v1_funct_1(all_51_1_40) % 15.15/4.15 | (210) v1_relat_1(all_51_1_40) % 15.15/4.15 | % 15.15/4.15 | Instantiating (193) with all_53_0_41, all_53_1_42 yields: % 15.15/4.15 | (211) u1_struct_0(all_0_16_16) = all_53_1_42 & k2_zfmisc_1(all_53_1_42, all_53_1_42) = all_53_0_41 & m2_relset_1(all_0_14_14, all_53_0_41, all_53_1_42) & v1_funct_2(all_0_14_14, all_53_0_41, all_53_1_42) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (211) yields: % 15.15/4.15 | (212) u1_struct_0(all_0_16_16) = all_53_1_42 % 15.15/4.15 | (213) k2_zfmisc_1(all_53_1_42, all_53_1_42) = all_53_0_41 % 15.15/4.15 | (214) m2_relset_1(all_0_14_14, all_53_0_41, all_53_1_42) % 15.15/4.15 | (215) v1_funct_2(all_0_14_14, all_53_0_41, all_53_1_42) % 15.15/4.15 | % 15.15/4.15 | Instantiating (189) with all_59_0_45 yields: % 15.15/4.15 | (216) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_59_0_45 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ v3_binop_1(v2, all_0_13_13) | ~ m1_subset_1(v0, all_31_0_34) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v3_binop_1(v3, v0) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ v2_binop_1(v2, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v2_binop_1(v3, v0) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ v1_binop_1(v2, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v1_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (216) yields: % 15.15/4.15 | (217) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_59_0_45 % 15.15/4.15 | (218) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ v3_binop_1(v2, all_0_13_13) | ~ m1_subset_1(v0, all_31_0_34) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v3_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.15/4.15 | (219) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ v2_binop_1(v2, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v2_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.15/4.15 | (220) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ v1_binop_1(v2, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_59_0_45, all_0_13_13) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v1_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.15/4.15 | % 15.15/4.15 | Instantiating (188) with all_62_0_46 yields: % 15.15/4.15 | (221) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_62_0_46 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (k1_realset1(v4, v0) = v5) | ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ r1_lattice2(all_0_13_13, v2, v4) | ~ m2_relset_1(v5, v1, v0) | ~ m2_relset_1(v4, all_62_0_46, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_62_0_46, all_0_13_13) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_2(v4, all_62_0_46, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_62_0_46, all_0_13_13) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | r1_lattice2(v0, v3, v5) | v1_xboole_0(v0)) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (221) yields: % 15.15/4.15 | (222) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_62_0_46 % 15.15/4.15 | (223) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (k1_realset1(v4, v0) = v5) | ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_31_0_34) | ~ r1_lattice2(all_0_13_13, v2, v4) | ~ m2_relset_1(v5, v1, v0) | ~ m2_relset_1(v4, all_62_0_46, all_0_13_13) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_62_0_46, all_0_13_13) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_2(v4, all_62_0_46, all_0_13_13) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_62_0_46, all_0_13_13) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | r1_lattice2(v0, v3, v5) | v1_xboole_0(v0)) % 15.15/4.15 | % 15.15/4.15 | Instantiating (191) with all_65_0_47, all_65_1_48 yields: % 15.15/4.15 | (224) u1_struct_0(all_0_16_16) = all_65_1_48 & k2_zfmisc_1(all_65_1_48, all_65_1_48) = all_65_0_47 & m2_relset_1(all_0_15_15, all_65_0_47, all_65_1_48) & v1_funct_2(all_0_15_15, all_65_0_47, all_65_1_48) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (224) yields: % 15.15/4.15 | (225) u1_struct_0(all_0_16_16) = all_65_1_48 % 15.15/4.15 | (226) k2_zfmisc_1(all_65_1_48, all_65_1_48) = all_65_0_47 % 15.15/4.15 | (227) m2_relset_1(all_0_15_15, all_65_0_47, all_65_1_48) % 15.15/4.15 | (228) v1_funct_2(all_0_15_15, all_65_0_47, all_65_1_48) % 15.15/4.15 | % 15.15/4.15 | Instantiating (199) with all_67_0_49, all_67_1_50 yields: % 15.15/4.15 | (229) u2_lattices(all_0_16_16) = all_67_1_50 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_67_0_49 & v1_partfun1(all_67_1_50, all_67_0_49, all_23_1_28) & v1_relat_1(all_67_1_50) & v2_binop_1(all_67_1_50, all_23_1_28) & v1_funct_2(all_67_1_50, all_67_0_49, all_23_1_28) & v1_funct_1(all_67_1_50) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (229) yields: % 15.15/4.15 | (230) v2_binop_1(all_67_1_50, all_23_1_28) % 15.15/4.15 | (231) v1_partfun1(all_67_1_50, all_67_0_49, all_23_1_28) % 15.15/4.15 | (232) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_67_0_49 % 15.15/4.15 | (233) v1_funct_1(all_67_1_50) % 15.15/4.15 | (234) v1_relat_1(all_67_1_50) % 15.15/4.15 | (235) u2_lattices(all_0_16_16) = all_67_1_50 % 15.15/4.15 | (236) v1_funct_2(all_67_1_50, all_67_0_49, all_23_1_28) % 15.15/4.15 | % 15.15/4.15 | Instantiating (196) with all_69_0_51, all_69_1_52 yields: % 15.15/4.15 | (237) u1_struct_0(all_0_16_16) = all_69_1_52 & k2_zfmisc_1(all_69_1_52, all_69_1_52) = all_69_0_51 & v1_partfun1(all_0_14_14, all_69_0_51, all_69_1_52) & v2_binop_1(all_0_14_14, all_69_1_52) & v1_funct_2(all_0_14_14, all_69_0_51, all_69_1_52) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (237) yields: % 15.15/4.15 | (238) v1_funct_2(all_0_14_14, all_69_0_51, all_69_1_52) % 15.15/4.15 | (239) u1_struct_0(all_0_16_16) = all_69_1_52 % 15.15/4.15 | (240) v1_partfun1(all_0_14_14, all_69_0_51, all_69_1_52) % 15.15/4.15 | (241) k2_zfmisc_1(all_69_1_52, all_69_1_52) = all_69_0_51 % 15.15/4.15 | (242) v2_binop_1(all_0_14_14, all_69_1_52) % 15.15/4.15 | % 15.15/4.15 | Instantiating (187) with all_71_0_53 yields: % 15.15/4.15 | (243) k1_zfmisc_1(all_23_1_28) = all_71_0_53 & ! [v0] : ( ~ m2_lattice4(v0, all_0_16_16) | m1_subset_1(v0, all_71_0_53)) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (243) yields: % 15.15/4.15 | (244) k1_zfmisc_1(all_23_1_28) = all_71_0_53 % 15.15/4.15 | (245) ! [v0] : ( ~ m2_lattice4(v0, all_0_16_16) | m1_subset_1(v0, all_71_0_53)) % 15.15/4.15 | % 15.15/4.15 | Instantiating formula (245) with all_0_13_13 and discharging atoms m2_lattice4(all_0_13_13, all_0_16_16), yields: % 15.15/4.15 | (246) m1_subset_1(all_0_13_13, all_71_0_53) % 15.15/4.15 | % 15.15/4.15 | Instantiating (192) with all_75_0_54, all_75_1_55 yields: % 15.15/4.15 | (247) u1_lattices(all_0_16_16) = all_75_1_55 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_75_0_54 & m2_relset_1(all_75_1_55, all_75_0_54, all_23_1_28) & v1_funct_2(all_75_1_55, all_75_0_54, all_23_1_28) & v1_funct_1(all_75_1_55) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (247) yields: % 15.15/4.15 | (248) v1_funct_2(all_75_1_55, all_75_0_54, all_23_1_28) % 15.15/4.15 | (249) m2_relset_1(all_75_1_55, all_75_0_54, all_23_1_28) % 15.15/4.15 | (250) v1_funct_1(all_75_1_55) % 15.15/4.15 | (251) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_75_0_54 % 15.15/4.15 | (252) u1_lattices(all_0_16_16) = all_75_1_55 % 15.15/4.15 | % 15.15/4.15 | Instantiating (202) with all_77_0_56, all_77_1_57 yields: % 15.15/4.15 | (253) u1_struct_0(all_0_16_16) = all_77_1_57 & k2_zfmisc_1(all_77_1_57, all_77_1_57) = all_77_0_56 & v1_partfun1(all_0_15_15, all_77_0_56, all_77_1_57) & v1_binop_1(all_0_15_15, all_77_1_57) & v1_funct_2(all_0_15_15, all_77_0_56, all_77_1_57) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (253) yields: % 15.15/4.15 | (254) v1_funct_2(all_0_15_15, all_77_0_56, all_77_1_57) % 15.15/4.15 | (255) v1_partfun1(all_0_15_15, all_77_0_56, all_77_1_57) % 15.15/4.15 | (256) v1_binop_1(all_0_15_15, all_77_1_57) % 15.15/4.15 | (257) k2_zfmisc_1(all_77_1_57, all_77_1_57) = all_77_0_56 % 15.15/4.15 | (258) u1_struct_0(all_0_16_16) = all_77_1_57 % 15.15/4.15 | % 15.15/4.15 | Instantiating (198) with all_79_0_58, all_79_1_59 yields: % 15.15/4.15 | (259) u1_struct_0(all_0_16_16) = all_79_1_59 & k2_zfmisc_1(all_79_1_59, all_79_1_59) = all_79_0_58 & v1_partfun1(all_0_14_14, all_79_0_58, all_79_1_59) & v1_binop_1(all_0_14_14, all_79_1_59) & v1_funct_2(all_0_14_14, all_79_0_58, all_79_1_59) % 15.15/4.15 | % 15.15/4.15 | Applying alpha-rule on (259) yields: % 15.15/4.15 | (260) u1_struct_0(all_0_16_16) = all_79_1_59 % 15.15/4.15 | (261) v1_partfun1(all_0_14_14, all_79_0_58, all_79_1_59) % 15.15/4.15 | (262) v1_funct_2(all_0_14_14, all_79_0_58, all_79_1_59) % 15.15/4.15 | (263) k2_zfmisc_1(all_79_1_59, all_79_1_59) = all_79_0_58 % 15.15/4.16 | (264) v1_binop_1(all_0_14_14, all_79_1_59) % 15.15/4.16 | % 15.15/4.16 | Instantiating (197) with all_81_0_60, all_81_1_61 yields: % 15.15/4.16 | (265) u1_lattices(all_0_16_16) = all_81_1_61 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_81_0_60 & v1_partfun1(all_81_1_61, all_81_0_60, all_23_1_28) & v1_relat_1(all_81_1_61) & v1_binop_1(all_81_1_61, all_23_1_28) & v1_funct_2(all_81_1_61, all_81_0_60, all_23_1_28) & v1_funct_1(all_81_1_61) % 15.15/4.16 | % 15.15/4.16 | Applying alpha-rule on (265) yields: % 15.15/4.16 | (266) u1_lattices(all_0_16_16) = all_81_1_61 % 15.15/4.16 | (267) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_81_0_60 % 15.15/4.16 | (268) v1_partfun1(all_81_1_61, all_81_0_60, all_23_1_28) % 15.15/4.16 | (269) v1_binop_1(all_81_1_61, all_23_1_28) % 15.15/4.16 | (270) v1_relat_1(all_81_1_61) % 15.15/4.16 | (271) v1_funct_2(all_81_1_61, all_81_0_60, all_23_1_28) % 15.15/4.16 | (272) v1_funct_1(all_81_1_61) % 15.15/4.16 | % 15.15/4.16 | Instantiating (201) with all_83_0_62, all_83_1_63 yields: % 15.15/4.16 | (273) u2_lattices(all_0_16_16) = all_83_1_63 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_83_0_62 & v1_partfun1(all_83_1_63, all_83_0_62, all_23_1_28) & v1_relat_1(all_83_1_63) & v1_binop_1(all_83_1_63, all_23_1_28) & v1_funct_2(all_83_1_63, all_83_0_62, all_23_1_28) & v1_funct_1(all_83_1_63) % 15.15/4.16 | % 15.15/4.16 | Applying alpha-rule on (273) yields: % 15.15/4.16 | (274) v1_partfun1(all_83_1_63, all_83_0_62, all_23_1_28) % 15.15/4.16 | (275) v1_relat_1(all_83_1_63) % 15.15/4.16 | (276) v1_funct_1(all_83_1_63) % 15.15/4.16 | (277) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_83_0_62 % 15.15/4.16 | (278) u2_lattices(all_0_16_16) = all_83_1_63 % 15.15/4.16 | (279) v1_funct_2(all_83_1_63, all_83_0_62, all_23_1_28) % 15.15/4.16 | (280) v1_binop_1(all_83_1_63, all_23_1_28) % 15.15/4.16 | % 15.15/4.16 | Instantiating (200) with all_85_0_64, all_85_1_65 yields: % 15.15/4.16 | (281) u1_struct_0(all_0_16_16) = all_85_1_65 & k2_zfmisc_1(all_85_1_65, all_85_1_65) = all_85_0_64 & v1_partfun1(all_0_15_15, all_85_0_64, all_85_1_65) & v2_binop_1(all_0_15_15, all_85_1_65) & v1_funct_2(all_0_15_15, all_85_0_64, all_85_1_65) % 15.15/4.16 | % 15.15/4.16 | Applying alpha-rule on (281) yields: % 15.15/4.16 | (282) v2_binop_1(all_0_15_15, all_85_1_65) % 15.15/4.16 | (283) v1_funct_2(all_0_15_15, all_85_0_64, all_85_1_65) % 15.15/4.16 | (284) v1_partfun1(all_0_15_15, all_85_0_64, all_85_1_65) % 15.15/4.16 | (285) k2_zfmisc_1(all_85_1_65, all_85_1_65) = all_85_0_64 % 15.15/4.16 | (286) u1_struct_0(all_0_16_16) = all_85_1_65 % 15.15/4.16 | % 15.15/4.16 | Instantiating (190) with all_87_0_66, all_87_1_67 yields: % 15.15/4.16 | (287) u2_lattices(all_0_16_16) = all_87_1_67 & k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_87_0_66 & m2_relset_1(all_87_1_67, all_87_0_66, all_23_1_28) & v1_funct_2(all_87_1_67, all_87_0_66, all_23_1_28) & v1_funct_1(all_87_1_67) % 15.15/4.16 | % 15.15/4.16 | Applying alpha-rule on (287) yields: % 15.15/4.16 | (288) v1_funct_2(all_87_1_67, all_87_0_66, all_23_1_28) % 15.15/4.16 | (289) v1_funct_1(all_87_1_67) % 15.15/4.16 | (290) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_87_0_66 % 15.15/4.16 | (291) m2_relset_1(all_87_1_67, all_87_0_66, all_23_1_28) % 15.15/4.16 | (292) u2_lattices(all_0_16_16) = all_87_1_67 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (83) with all_0_16_16, all_87_1_67, all_0_15_15 and discharging atoms u2_lattices(all_0_16_16) = all_87_1_67, u2_lattices(all_0_16_16) = all_0_15_15, yields: % 15.15/4.16 | (293) all_87_1_67 = all_0_15_15 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (83) with all_0_16_16, all_83_1_63, all_87_1_67 and discharging atoms u2_lattices(all_0_16_16) = all_87_1_67, u2_lattices(all_0_16_16) = all_83_1_63, yields: % 15.15/4.16 | (294) all_87_1_67 = all_83_1_63 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (83) with all_0_16_16, all_67_1_50, all_83_1_63 and discharging atoms u2_lattices(all_0_16_16) = all_83_1_63, u2_lattices(all_0_16_16) = all_67_1_50, yields: % 15.15/4.16 | (295) all_83_1_63 = all_67_1_50 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (37) with all_0_16_16, all_75_1_55, all_0_14_14 and discharging atoms u1_lattices(all_0_16_16) = all_75_1_55, u1_lattices(all_0_16_16) = all_0_14_14, yields: % 15.15/4.16 | (296) all_75_1_55 = all_0_14_14 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (37) with all_0_16_16, all_75_1_55, all_81_1_61 and discharging atoms u1_lattices(all_0_16_16) = all_81_1_61, u1_lattices(all_0_16_16) = all_75_1_55, yields: % 15.15/4.16 | (297) all_81_1_61 = all_75_1_55 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (37) with all_0_16_16, all_51_1_40, all_81_1_61 and discharging atoms u1_lattices(all_0_16_16) = all_81_1_61, u1_lattices(all_0_16_16) = all_51_1_40, yields: % 15.15/4.16 | (298) all_81_1_61 = all_51_1_40 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (128) with all_0_16_16, all_79_1_59, all_85_1_65 and discharging atoms u1_struct_0(all_0_16_16) = all_85_1_65, u1_struct_0(all_0_16_16) = all_79_1_59, yields: % 15.15/4.16 | (299) all_85_1_65 = all_79_1_59 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (128) with all_0_16_16, all_77_1_57, all_79_1_59 and discharging atoms u1_struct_0(all_0_16_16) = all_79_1_59, u1_struct_0(all_0_16_16) = all_77_1_57, yields: % 15.15/4.16 | (300) all_79_1_59 = all_77_1_57 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (128) with all_0_16_16, all_69_1_52, all_77_1_57 and discharging atoms u1_struct_0(all_0_16_16) = all_77_1_57, u1_struct_0(all_0_16_16) = all_69_1_52, yields: % 15.15/4.16 | (301) all_77_1_57 = all_69_1_52 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (128) with all_0_16_16, all_65_1_48, all_23_1_28 and discharging atoms u1_struct_0(all_0_16_16) = all_65_1_48, u1_struct_0(all_0_16_16) = all_23_1_28, yields: % 15.15/4.16 | (302) all_65_1_48 = all_23_1_28 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (128) with all_0_16_16, all_65_1_48, all_69_1_52 and discharging atoms u1_struct_0(all_0_16_16) = all_69_1_52, u1_struct_0(all_0_16_16) = all_65_1_48, yields: % 15.15/4.16 | (303) all_69_1_52 = all_65_1_48 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (128) with all_0_16_16, all_53_1_42, all_85_1_65 and discharging atoms u1_struct_0(all_0_16_16) = all_85_1_65, u1_struct_0(all_0_16_16) = all_53_1_42, yields: % 15.15/4.16 | (304) all_85_1_65 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_83_0_62, all_87_0_66 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_87_0_66, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_83_0_62, yields: % 15.15/4.16 | (305) all_87_0_66 = all_83_0_62 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_81_0_60, all_83_0_62 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_83_0_62, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_81_0_60, yields: % 15.15/4.16 | (306) all_83_0_62 = all_81_0_60 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_75_0_54, all_83_0_62 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_83_0_62, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_75_0_54, yields: % 15.15/4.16 | (307) all_83_0_62 = all_75_0_54 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_67_0_49, all_75_0_54 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_75_0_54, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_67_0_49, yields: % 15.15/4.16 | (308) all_75_0_54 = all_67_0_49 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_51_0_39, all_87_0_66 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_87_0_66, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_51_0_39, yields: % 15.15/4.16 | (309) all_87_0_66 = all_51_0_39 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (6) with all_0_13_13, all_0_13_13, all_62_0_46, all_0_12_12 and discharging atoms k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_62_0_46, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, yields: % 15.15/4.16 | (310) all_62_0_46 = all_0_12_12 % 15.15/4.16 | % 15.15/4.16 | Instantiating formula (6) with all_0_13_13, all_0_13_13, all_59_0_45, all_62_0_46 and discharging atoms k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_62_0_46, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_59_0_45, yields: % 15.15/4.16 | (311) all_62_0_46 = all_59_0_45 % 15.15/4.16 | % 15.15/4.16 | Combining equations (305,309) yields a new equation: % 15.15/4.16 | (312) all_83_0_62 = all_51_0_39 % 15.15/4.16 | % 15.15/4.16 | Simplifying 312 yields: % 15.15/4.16 | (313) all_83_0_62 = all_51_0_39 % 15.15/4.16 | % 15.15/4.16 | Combining equations (294,293) yields a new equation: % 15.15/4.16 | (314) all_83_1_63 = all_0_15_15 % 15.15/4.16 | % 15.15/4.16 | Simplifying 314 yields: % 15.15/4.16 | (315) all_83_1_63 = all_0_15_15 % 15.15/4.16 | % 15.15/4.16 | Combining equations (299,304) yields a new equation: % 15.15/4.16 | (316) all_79_1_59 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Simplifying 316 yields: % 15.15/4.16 | (317) all_79_1_59 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Combining equations (307,306) yields a new equation: % 15.15/4.16 | (318) all_81_0_60 = all_75_0_54 % 15.15/4.16 | % 15.15/4.16 | Combining equations (313,306) yields a new equation: % 15.15/4.16 | (319) all_81_0_60 = all_51_0_39 % 15.15/4.16 | % 15.15/4.16 | Combining equations (295,315) yields a new equation: % 15.15/4.16 | (320) all_67_1_50 = all_0_15_15 % 15.15/4.16 | % 15.15/4.16 | Simplifying 320 yields: % 15.15/4.16 | (321) all_67_1_50 = all_0_15_15 % 15.15/4.16 | % 15.15/4.16 | Combining equations (318,319) yields a new equation: % 15.15/4.16 | (322) all_75_0_54 = all_51_0_39 % 15.15/4.16 | % 15.15/4.16 | Simplifying 322 yields: % 15.15/4.16 | (323) all_75_0_54 = all_51_0_39 % 15.15/4.16 | % 15.15/4.16 | Combining equations (297,298) yields a new equation: % 15.15/4.16 | (324) all_75_1_55 = all_51_1_40 % 15.15/4.16 | % 15.15/4.16 | Simplifying 324 yields: % 15.15/4.16 | (325) all_75_1_55 = all_51_1_40 % 15.15/4.16 | % 15.15/4.16 | Combining equations (300,317) yields a new equation: % 15.15/4.16 | (326) all_77_1_57 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Simplifying 326 yields: % 15.15/4.16 | (327) all_77_1_57 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Combining equations (301,327) yields a new equation: % 15.15/4.16 | (328) all_69_1_52 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Simplifying 328 yields: % 15.15/4.16 | (329) all_69_1_52 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Combining equations (308,323) yields a new equation: % 15.15/4.16 | (330) all_67_0_49 = all_51_0_39 % 15.15/4.16 | % 15.15/4.16 | Simplifying 330 yields: % 15.15/4.16 | (331) all_67_0_49 = all_51_0_39 % 15.15/4.16 | % 15.15/4.16 | Combining equations (296,325) yields a new equation: % 15.15/4.16 | (332) all_51_1_40 = all_0_14_14 % 15.15/4.16 | % 15.15/4.16 | Combining equations (303,329) yields a new equation: % 15.15/4.16 | (333) all_65_1_48 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Simplifying 333 yields: % 15.15/4.16 | (334) all_65_1_48 = all_53_1_42 % 15.15/4.16 | % 15.15/4.16 | Combining equations (302,334) yields a new equation: % 15.15/4.16 | (335) all_53_1_42 = all_23_1_28 % 15.15/4.16 | % 15.15/4.16 | Combining equations (310,311) yields a new equation: % 15.15/4.16 | (336) all_59_0_45 = all_0_12_12 % 15.15/4.16 | % 15.15/4.16 | Combining equations (335,334) yields a new equation: % 15.15/4.16 | (302) all_65_1_48 = all_23_1_28 % 15.15/4.16 | % 15.15/4.16 | Combining equations (335,329) yields a new equation: % 15.15/4.16 | (338) all_69_1_52 = all_23_1_28 % 15.15/4.16 | % 15.15/4.16 | Combining equations (335,327) yields a new equation: % 15.15/4.16 | (339) all_77_1_57 = all_23_1_28 % 15.15/4.16 | % 15.15/4.16 | Combining equations (335,317) yields a new equation: % 15.15/4.16 | (340) all_79_1_59 = all_23_1_28 % 15.15/4.16 | % 15.15/4.16 | Combining equations (335,304) yields a new equation: % 15.15/4.16 | (341) all_85_1_65 = all_23_1_28 % 15.15/4.16 | % 15.15/4.16 | From (335) and (212) follows: % 15.15/4.16 | (143) u1_struct_0(all_0_16_16) = all_23_1_28 % 15.15/4.16 | % 15.15/4.16 | From (341)(341) and (285) follows: % 15.15/4.16 | (343) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_85_0_64 % 15.15/4.17 | % 15.15/4.17 | From (340)(340) and (263) follows: % 15.15/4.17 | (344) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_79_0_58 % 15.15/4.17 | % 15.15/4.17 | From (339)(339) and (257) follows: % 15.15/4.17 | (345) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_77_0_56 % 15.15/4.17 | % 15.15/4.17 | From (338)(338) and (241) follows: % 15.15/4.17 | (346) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_69_0_51 % 15.15/4.17 | % 15.15/4.17 | From (302)(302) and (226) follows: % 15.15/4.17 | (347) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_65_0_47 % 15.15/4.17 | % 15.15/4.17 | From (335)(335) and (213) follows: % 15.15/4.17 | (348) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_53_0_41 % 15.15/4.17 | % 15.15/4.17 | From (331) and (232) follows: % 15.15/4.17 | (208) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | From (336) and (217) follows: % 15.15/4.17 | (100) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12 % 15.15/4.17 | % 15.15/4.17 | From (321) and (234) follows: % 15.15/4.17 | (351) v1_relat_1(all_0_15_15) % 15.15/4.17 | % 15.15/4.17 | From (332) and (210) follows: % 15.15/4.17 | (352) v1_relat_1(all_0_14_14) % 15.15/4.17 | % 15.15/4.17 | From (338) and (242) follows: % 15.15/4.17 | (353) v2_binop_1(all_0_14_14, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (341) and (282) follows: % 15.15/4.17 | (354) v2_binop_1(all_0_15_15, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (340) and (264) follows: % 15.15/4.17 | (355) v1_binop_1(all_0_14_14, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (339) and (256) follows: % 15.15/4.17 | (356) v1_binop_1(all_0_15_15, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (335) and (214) follows: % 15.15/4.17 | (357) m2_relset_1(all_0_14_14, all_53_0_41, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (302) and (227) follows: % 15.15/4.17 | (358) m2_relset_1(all_0_15_15, all_65_0_47, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (335) and (215) follows: % 15.15/4.17 | (359) v1_funct_2(all_0_14_14, all_53_0_41, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (302) and (228) follows: % 15.15/4.17 | (360) v1_funct_2(all_0_15_15, all_65_0_47, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (321) and (233) follows: % 15.15/4.17 | (361) v1_funct_1(all_0_15_15) % 15.15/4.17 | % 15.15/4.17 | From (332) and (209) follows: % 15.15/4.17 | (362) v1_funct_1(all_0_14_14) % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_85_0_64, all_51_0_39 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_85_0_64, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_51_0_39, yields: % 15.15/4.17 | (363) all_85_0_64 = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_79_0_58, all_85_0_64 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_85_0_64, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_79_0_58, yields: % 15.15/4.17 | (364) all_85_0_64 = all_79_0_58 % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_69_0_51, all_79_0_58 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_79_0_58, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_69_0_51, yields: % 15.15/4.17 | (365) all_79_0_58 = all_69_0_51 % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_69_0_51, all_77_0_56 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_77_0_56, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_69_0_51, yields: % 15.15/4.17 | (366) all_77_0_56 = all_69_0_51 % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_65_0_47, all_77_0_56 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_77_0_56, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_65_0_47, yields: % 15.15/4.17 | (367) all_77_0_56 = all_65_0_47 % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (6) with all_23_1_28, all_23_1_28, all_53_0_41, all_69_0_51 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_69_0_51, k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_53_0_41, yields: % 15.15/4.17 | (368) all_69_0_51 = all_53_0_41 % 15.15/4.17 | % 15.15/4.17 | Combining equations (364,363) yields a new equation: % 15.15/4.17 | (369) all_79_0_58 = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | Simplifying 369 yields: % 15.15/4.17 | (370) all_79_0_58 = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | Combining equations (365,370) yields a new equation: % 15.15/4.17 | (371) all_69_0_51 = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | Simplifying 371 yields: % 15.15/4.17 | (372) all_69_0_51 = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | Combining equations (366,367) yields a new equation: % 15.15/4.17 | (373) all_69_0_51 = all_65_0_47 % 15.15/4.17 | % 15.15/4.17 | Simplifying 373 yields: % 15.15/4.17 | (374) all_69_0_51 = all_65_0_47 % 15.15/4.17 | % 15.15/4.17 | Combining equations (368,374) yields a new equation: % 15.15/4.17 | (375) all_65_0_47 = all_53_0_41 % 15.15/4.17 | % 15.15/4.17 | Combining equations (372,374) yields a new equation: % 15.15/4.17 | (376) all_65_0_47 = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | Combining equations (376,375) yields a new equation: % 15.15/4.17 | (377) all_53_0_41 = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | Combining equations (377,375) yields a new equation: % 15.15/4.17 | (376) all_65_0_47 = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | From (377) and (348) follows: % 15.15/4.17 | (208) k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_51_0_39 % 15.15/4.17 | % 15.15/4.17 | From (377) and (357) follows: % 15.15/4.17 | (380) m2_relset_1(all_0_14_14, all_51_0_39, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (376) and (358) follows: % 15.15/4.17 | (381) m2_relset_1(all_0_15_15, all_51_0_39, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (377) and (359) follows: % 15.15/4.17 | (382) v1_funct_2(all_0_14_14, all_51_0_39, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | From (376) and (360) follows: % 15.15/4.17 | (383) v1_funct_2(all_0_15_15, all_51_0_39, all_23_1_28) % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (14) with all_51_0_39, all_23_1_28 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_51_0_39, yields: % 15.15/4.17 | (384) v1_xboole_0(all_23_1_28) | ? [v0] : (k1_zfmisc_1(all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v1) = v6) | ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ r1_lattice2(all_23_1_28, v3, v5) | ~ m2_relset_1(v6, v2, v1) | ~ m2_relset_1(v5, all_51_0_39, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v6, v2, v1) | ~ v1_funct_2(v5, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | r1_lattice2(v1, v4, v6) | v1_xboole_0(v1))) % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (38) with all_51_0_39, all_23_1_28 and discharging atoms k2_zfmisc_1(all_23_1_28, all_23_1_28) = all_51_0_39, yields: % 15.15/4.17 | (385) v1_xboole_0(all_23_1_28) | ? [v0] : (k1_zfmisc_1(all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v3_binop_1(v3, all_23_1_28) | ~ m1_subset_1(v1, v0) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v3_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ v2_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v2_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ v1_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v1_binop_1(v4, v1) | v1_xboole_0(v1))) % 15.15/4.17 | % 15.15/4.17 | Instantiating formula (20) with all_71_0_53, all_23_1_28 and discharging atoms k1_zfmisc_1(all_23_1_28) = all_71_0_53, yields: % 15.15/4.17 | (386) v1_xboole_0(all_23_1_28) | ? [v0] : (k2_zfmisc_1(all_23_1_28, all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v1) = v6) | ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_71_0_53) | ~ r1_lattice2(all_23_1_28, v3, v5) | ~ m2_relset_1(v6, v2, v1) | ~ m2_relset_1(v5, v0, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v6, v2, v1) | ~ v1_funct_2(v5, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | r1_lattice2(v1, v4, v6) | v1_xboole_0(v1))) % 15.15/4.18 | % 15.15/4.18 | Instantiating formula (69) with all_71_0_53, all_23_1_28 and discharging atoms k1_zfmisc_1(all_23_1_28) = all_71_0_53, yields: % 15.15/4.18 | (387) v1_xboole_0(all_23_1_28) | ? [v0] : (k2_zfmisc_1(all_23_1_28, all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v3_binop_1(v3, all_23_1_28) | ~ m1_subset_1(v1, all_71_0_53) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v3_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_71_0_53) | ~ v2_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v2_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_71_0_53) | ~ v1_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v1_binop_1(v4, v1) | v1_xboole_0(v1))) % 15.15/4.18 | % 15.15/4.18 | Instantiating formula (106) with all_23_1_28, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = all_23_1_28, l1_struct_0(all_0_16_16), ~ v3_struct_0(all_0_16_16), yields: % 15.15/4.18 | (388) ? [v0] : ? [v1] : (k1_zfmisc_1(all_23_1_28) = v0 & m1_subset_1(v1, v0) & ~ v1_xboole_0(v1)) % 15.15/4.18 | % 15.15/4.18 | Instantiating formula (50) with all_0_10_10, all_0_13_13, all_0_14_14 and discharging atoms k1_realset1(all_0_14_14, all_0_13_13) = all_0_10_10, v1_relat_1(all_0_14_14), yields: % 15.15/4.18 | (389) ? [v0] : (k7_relat_1(all_0_14_14, v0) = all_0_10_10 & k2_zfmisc_1(all_0_13_13, all_0_13_13) = v0) % 15.15/4.18 | % 15.15/4.18 | Instantiating formula (50) with all_0_11_11, all_0_13_13, all_0_15_15 and discharging atoms k1_realset1(all_0_15_15, all_0_13_13) = all_0_11_11, v1_relat_1(all_0_15_15), yields: % 15.15/4.18 | (390) ? [v0] : (k7_relat_1(all_0_15_15, v0) = all_0_11_11 & k2_zfmisc_1(all_0_13_13, all_0_13_13) = v0) % 15.15/4.18 | % 15.15/4.18 | Instantiating (390) with all_103_0_68 yields: % 15.15/4.18 | (391) k7_relat_1(all_0_15_15, all_103_0_68) = all_0_11_11 & k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_103_0_68 % 15.15/4.18 | % 15.15/4.18 | Applying alpha-rule on (391) yields: % 15.15/4.18 | (392) k7_relat_1(all_0_15_15, all_103_0_68) = all_0_11_11 % 15.15/4.18 | (393) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_103_0_68 % 15.15/4.18 | % 15.15/4.18 | Instantiating (388) with all_105_0_69, all_105_1_70 yields: % 15.15/4.18 | (394) k1_zfmisc_1(all_23_1_28) = all_105_1_70 & m1_subset_1(all_105_0_69, all_105_1_70) & ~ v1_xboole_0(all_105_0_69) % 15.15/4.18 | % 15.15/4.18 | Applying alpha-rule on (394) yields: % 15.15/4.18 | (395) k1_zfmisc_1(all_23_1_28) = all_105_1_70 % 15.15/4.18 | (396) m1_subset_1(all_105_0_69, all_105_1_70) % 15.15/4.18 | (397) ~ v1_xboole_0(all_105_0_69) % 15.15/4.18 | % 15.15/4.18 | Instantiating (389) with all_109_0_72 yields: % 15.15/4.18 | (398) k7_relat_1(all_0_14_14, all_109_0_72) = all_0_10_10 & k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_109_0_72 % 15.15/4.18 | % 15.15/4.18 | Applying alpha-rule on (398) yields: % 15.15/4.18 | (399) k7_relat_1(all_0_14_14, all_109_0_72) = all_0_10_10 % 15.15/4.18 | (400) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_109_0_72 % 15.15/4.18 | % 15.15/4.18 | Instantiating formula (6) with all_0_13_13, all_0_13_13, all_109_0_72, all_0_12_12 and discharging atoms k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_109_0_72, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, yields: % 15.15/4.18 | (401) all_109_0_72 = all_0_12_12 % 15.15/4.18 | % 15.15/4.18 | Instantiating formula (6) with all_0_13_13, all_0_13_13, all_103_0_68, all_109_0_72 and discharging atoms k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_109_0_72, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_103_0_68, yields: % 15.15/4.18 | (402) all_109_0_72 = all_103_0_68 % 15.15/4.18 | % 15.15/4.18 | Instantiating formula (41) with all_23_1_28, all_105_1_70, all_71_0_53 and discharging atoms k1_zfmisc_1(all_23_1_28) = all_105_1_70, k1_zfmisc_1(all_23_1_28) = all_71_0_53, yields: % 15.15/4.18 | (403) all_105_1_70 = all_71_0_53 % 15.15/4.18 | % 15.15/4.18 | Combining equations (401,402) yields a new equation: % 15.15/4.18 | (404) all_103_0_68 = all_0_12_12 % 15.15/4.18 | % 15.15/4.18 | From (404) and (393) follows: % 15.15/4.18 | (100) k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12 % 15.15/4.18 | % 15.15/4.18 | From (403) and (395) follows: % 15.15/4.18 | (244) k1_zfmisc_1(all_23_1_28) = all_71_0_53 % 15.15/4.18 | % 15.15/4.18 +-Applying beta-rule and splitting (26), into two cases. % 15.15/4.18 |-Branch one: % 15.15/4.18 | (407) ~ r1_lattice2(all_0_13_13, all_0_10_10, all_0_11_11) % 15.15/4.18 | % 15.15/4.18 +-Applying beta-rule and splitting (387), into two cases. % 15.15/4.18 |-Branch one: % 15.15/4.18 | (408) v1_xboole_0(all_23_1_28) % 15.15/4.18 | % 15.15/4.18 | Instantiating formula (46) with all_23_1_28 and discharging atoms v1_xboole_0(all_23_1_28), yields: % 15.58/4.18 | (409) all_23_1_28 = k1_xboole_0 % 15.58/4.18 | % 15.58/4.18 | From (409) and (143) follows: % 15.58/4.18 | (410) u1_struct_0(all_0_16_16) = k1_xboole_0 % 15.58/4.18 | % 15.58/4.18 | From (409) and (408) follows: % 15.58/4.18 | (95) v1_xboole_0(k1_xboole_0) % 15.58/4.18 | % 15.58/4.18 | Instantiating formula (31) with k1_xboole_0, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = k1_xboole_0, l1_struct_0(all_0_16_16), v1_xboole_0(k1_xboole_0), ~ v3_struct_0(all_0_16_16), yields: % 15.58/4.18 | (412) $false % 15.58/4.18 | % 15.58/4.18 |-The branch is then unsatisfiable % 15.58/4.18 |-Branch two: % 15.58/4.18 | (413) ~ v1_xboole_0(all_23_1_28) % 15.58/4.18 | (414) ? [v0] : (k2_zfmisc_1(all_23_1_28, all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v3_binop_1(v3, all_23_1_28) | ~ m1_subset_1(v1, all_71_0_53) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v3_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_71_0_53) | ~ v2_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v2_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_71_0_53) | ~ v1_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v1_binop_1(v4, v1) | v1_xboole_0(v1))) % 15.58/4.18 | % 15.58/4.18 +-Applying beta-rule and splitting (385), into two cases. % 15.58/4.18 |-Branch one: % 15.58/4.18 | (408) v1_xboole_0(all_23_1_28) % 15.58/4.18 | % 15.58/4.18 | Using (408) and (413) yields: % 15.58/4.18 | (412) $false % 15.58/4.18 | % 15.58/4.18 |-The branch is then unsatisfiable % 15.58/4.18 |-Branch two: % 15.58/4.18 | (413) ~ v1_xboole_0(all_23_1_28) % 15.58/4.18 | (418) ? [v0] : (k1_zfmisc_1(all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v3_binop_1(v3, all_23_1_28) | ~ m1_subset_1(v1, v0) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v3_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ v2_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v2_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ v1_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v1_binop_1(v4, v1) | v1_xboole_0(v1))) % 15.58/4.18 | % 15.58/4.18 +-Applying beta-rule and splitting (386), into two cases. % 15.58/4.18 |-Branch one: % 15.58/4.18 | (408) v1_xboole_0(all_23_1_28) % 15.58/4.18 | % 15.58/4.18 | Using (408) and (413) yields: % 15.58/4.18 | (412) $false % 15.58/4.18 | % 15.58/4.18 |-The branch is then unsatisfiable % 15.58/4.18 |-Branch two: % 15.58/4.18 | (413) ~ v1_xboole_0(all_23_1_28) % 15.58/4.18 | (422) ? [v0] : (k2_zfmisc_1(all_23_1_28, all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v1) = v6) | ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_71_0_53) | ~ r1_lattice2(all_23_1_28, v3, v5) | ~ m2_relset_1(v6, v2, v1) | ~ m2_relset_1(v5, v0, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v6, v2, v1) | ~ v1_funct_2(v5, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | r1_lattice2(v1, v4, v6) | v1_xboole_0(v1))) % 15.58/4.19 | % 15.58/4.19 +-Applying beta-rule and splitting (384), into two cases. % 15.58/4.19 |-Branch one: % 15.58/4.19 | (408) v1_xboole_0(all_23_1_28) % 15.58/4.19 | % 15.58/4.19 | Using (408) and (413) yields: % 15.58/4.19 | (412) $false % 15.58/4.19 | % 15.58/4.19 |-The branch is then unsatisfiable % 15.58/4.19 |-Branch two: % 15.58/4.19 | (413) ~ v1_xboole_0(all_23_1_28) % 15.58/4.19 | (426) ? [v0] : (k1_zfmisc_1(all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v1) = v6) | ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ r1_lattice2(all_23_1_28, v3, v5) | ~ m2_relset_1(v6, v2, v1) | ~ m2_relset_1(v5, all_51_0_39, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v6, v2, v1) | ~ v1_funct_2(v5, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | r1_lattice2(v1, v4, v6) | v1_xboole_0(v1))) % 15.58/4.19 | % 15.58/4.19 | Instantiating (418) with all_170_0_74 yields: % 15.58/4.19 | (427) k1_zfmisc_1(all_23_1_28) = all_170_0_74 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ v3_binop_1(v2, all_23_1_28) | ~ m1_subset_1(v0, all_170_0_74) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v3_binop_1(v3, v0) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_170_0_74) | ~ v2_binop_1(v2, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v2_binop_1(v3, v0) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_170_0_74) | ~ v1_binop_1(v2, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v1_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.58/4.19 | % 15.58/4.19 | Applying alpha-rule on (427) yields: % 15.58/4.19 | (428) k1_zfmisc_1(all_23_1_28) = all_170_0_74 % 15.58/4.19 | (429) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ v3_binop_1(v2, all_23_1_28) | ~ m1_subset_1(v0, all_170_0_74) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v3_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.58/4.19 | (430) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_170_0_74) | ~ v2_binop_1(v2, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v2_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.58/4.19 | (431) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_170_0_74) | ~ v1_binop_1(v2, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v1_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.58/4.19 | % 15.58/4.19 | Instantiating (426) with all_176_0_76 yields: % 15.58/4.19 | (432) k1_zfmisc_1(all_23_1_28) = all_176_0_76 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (k1_realset1(v4, v0) = v5) | ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_176_0_76) | ~ r1_lattice2(all_23_1_28, v2, v4) | ~ m2_relset_1(v5, v1, v0) | ~ m2_relset_1(v4, all_51_0_39, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_2(v4, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | r1_lattice2(v0, v3, v5) | v1_xboole_0(v0)) % 15.58/4.19 | % 15.58/4.19 | Applying alpha-rule on (432) yields: % 15.58/4.19 | (433) k1_zfmisc_1(all_23_1_28) = all_176_0_76 % 15.58/4.19 | (434) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (k1_realset1(v4, v0) = v5) | ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_176_0_76) | ~ r1_lattice2(all_23_1_28, v2, v4) | ~ m2_relset_1(v5, v1, v0) | ~ m2_relset_1(v4, all_51_0_39, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_2(v4, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | r1_lattice2(v0, v3, v5) | v1_xboole_0(v0)) % 15.58/4.19 | % 15.58/4.19 | Instantiating formula (41) with all_23_1_28, all_176_0_76, all_71_0_53 and discharging atoms k1_zfmisc_1(all_23_1_28) = all_176_0_76, k1_zfmisc_1(all_23_1_28) = all_71_0_53, yields: % 15.58/4.19 | (435) all_176_0_76 = all_71_0_53 % 15.58/4.19 | % 15.58/4.19 | Instantiating formula (41) with all_23_1_28, all_170_0_74, all_176_0_76 and discharging atoms k1_zfmisc_1(all_23_1_28) = all_176_0_76, k1_zfmisc_1(all_23_1_28) = all_170_0_74, yields: % 15.58/4.19 | (436) all_176_0_76 = all_170_0_74 % 15.58/4.19 | % 15.58/4.19 | Combining equations (435,436) yields a new equation: % 15.58/4.19 | (437) all_170_0_74 = all_71_0_53 % 15.58/4.19 | % 15.58/4.19 | Combining equations (437,436) yields a new equation: % 15.58/4.19 | (435) all_176_0_76 = all_71_0_53 % 15.58/4.19 | % 15.58/4.19 | Instantiating formula (434) with all_0_11_11, all_0_15_15, all_0_10_10, all_0_14_14, all_0_12_12, all_0_13_13 and discharging atoms k1_realset1(all_0_14_14, all_0_13_13) = all_0_10_10, k1_realset1(all_0_15_15, all_0_13_13) = all_0_11_11, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, r1_lattice2(all_23_1_28, all_0_14_14, all_0_15_15), m2_relset_1(all_0_10_10, all_0_12_12, all_0_13_13), m2_relset_1(all_0_11_11, all_0_12_12, all_0_13_13), m2_relset_1(all_0_14_14, all_51_0_39, all_23_1_28), m2_relset_1(all_0_15_15, all_51_0_39, all_23_1_28), v1_funct_2(all_0_10_10, all_0_12_12, all_0_13_13), v1_funct_2(all_0_11_11, all_0_12_12, all_0_13_13), v1_funct_2(all_0_14_14, all_51_0_39, all_23_1_28), v1_funct_2(all_0_15_15, all_51_0_39, all_23_1_28), v1_funct_1(all_0_10_10), v1_funct_1(all_0_11_11), v1_funct_1(all_0_14_14), v1_funct_1(all_0_15_15), ~ r1_lattice2(all_0_13_13, all_0_10_10, all_0_11_11), ~ v1_xboole_0(all_0_13_13), yields: % 15.66/4.19 | (439) ~ m1_subset_1(all_0_13_13, all_176_0_76) % 15.66/4.19 | % 15.66/4.19 | From (435) and (439) follows: % 15.66/4.19 | (440) ~ m1_subset_1(all_0_13_13, all_71_0_53) % 15.66/4.19 | % 15.66/4.19 | Using (246) and (440) yields: % 15.66/4.19 | (412) $false % 15.66/4.19 | % 15.66/4.19 |-The branch is then unsatisfiable % 15.66/4.19 |-Branch two: % 15.66/4.19 | (442) r1_lattice2(all_0_13_13, all_0_10_10, all_0_11_11) % 15.66/4.19 | (443) ~ r1_lattice2(all_0_13_13, all_0_11_11, all_0_10_10) | ~ v2_binop_1(all_0_10_10, all_0_13_13) | ~ v2_binop_1(all_0_11_11, all_0_13_13) | ~ v1_binop_1(all_0_10_10, all_0_13_13) | ~ v1_binop_1(all_0_11_11, all_0_13_13) % 15.66/4.19 | % 15.66/4.19 +-Applying beta-rule and splitting (386), into two cases. % 15.66/4.19 |-Branch one: % 15.66/4.19 | (408) v1_xboole_0(all_23_1_28) % 15.66/4.19 | % 15.66/4.19 | Instantiating formula (46) with all_23_1_28 and discharging atoms v1_xboole_0(all_23_1_28), yields: % 15.66/4.19 | (409) all_23_1_28 = k1_xboole_0 % 15.66/4.19 | % 15.66/4.19 | From (409) and (143) follows: % 15.66/4.19 | (410) u1_struct_0(all_0_16_16) = k1_xboole_0 % 15.66/4.19 | % 15.66/4.19 | From (409) and (408) follows: % 15.66/4.19 | (95) v1_xboole_0(k1_xboole_0) % 15.66/4.19 | % 15.66/4.19 | Instantiating formula (31) with k1_xboole_0, all_0_16_16 and discharging atoms u1_struct_0(all_0_16_16) = k1_xboole_0, l1_struct_0(all_0_16_16), v1_xboole_0(k1_xboole_0), ~ v3_struct_0(all_0_16_16), yields: % 15.66/4.19 | (412) $false % 15.66/4.19 | % 15.66/4.19 |-The branch is then unsatisfiable % 15.66/4.19 |-Branch two: % 15.66/4.19 | (413) ~ v1_xboole_0(all_23_1_28) % 15.66/4.19 | (422) ? [v0] : (k2_zfmisc_1(all_23_1_28, all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v1) = v6) | ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, all_71_0_53) | ~ r1_lattice2(all_23_1_28, v3, v5) | ~ m2_relset_1(v6, v2, v1) | ~ m2_relset_1(v5, v0, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, v0, all_23_1_28) | ~ v1_funct_2(v6, v2, v1) | ~ v1_funct_2(v5, v0, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, v0, all_23_1_28) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | r1_lattice2(v1, v4, v6) | v1_xboole_0(v1))) % 15.66/4.19 | % 15.66/4.19 +-Applying beta-rule and splitting (385), into two cases. % 15.66/4.19 |-Branch one: % 15.66/4.19 | (408) v1_xboole_0(all_23_1_28) % 15.66/4.19 | % 15.66/4.19 | Using (408) and (413) yields: % 15.66/4.19 | (412) $false % 15.66/4.19 | % 15.66/4.19 |-The branch is then unsatisfiable % 15.66/4.19 |-Branch two: % 15.66/4.19 | (413) ~ v1_xboole_0(all_23_1_28) % 15.66/4.19 | (418) ? [v0] : (k1_zfmisc_1(all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ v3_binop_1(v3, all_23_1_28) | ~ m1_subset_1(v1, v0) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v3_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ v2_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v2_binop_1(v4, v1) | v1_xboole_0(v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ v1_binop_1(v3, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | v1_binop_1(v4, v1) | v1_xboole_0(v1))) % 15.66/4.20 | % 15.66/4.20 +-Applying beta-rule and splitting (384), into two cases. % 15.66/4.20 |-Branch one: % 15.66/4.20 | (408) v1_xboole_0(all_23_1_28) % 15.66/4.20 | % 15.66/4.20 | Using (408) and (413) yields: % 15.66/4.20 | (412) $false % 15.66/4.20 | % 15.66/4.20 |-The branch is then unsatisfiable % 15.66/4.20 |-Branch two: % 15.66/4.20 | (413) ~ v1_xboole_0(all_23_1_28) % 15.66/4.20 | (426) ? [v0] : (k1_zfmisc_1(all_23_1_28) = v0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (k1_realset1(v5, v1) = v6) | ~ (k1_realset1(v3, v1) = v4) | ~ (k2_zfmisc_1(v1, v1) = v2) | ~ m1_subset_1(v1, v0) | ~ r1_lattice2(all_23_1_28, v3, v5) | ~ m2_relset_1(v6, v2, v1) | ~ m2_relset_1(v5, all_51_0_39, all_23_1_28) | ~ m2_relset_1(v4, v2, v1) | ~ m2_relset_1(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v6, v2, v1) | ~ v1_funct_2(v5, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v4, v2, v1) | ~ v1_funct_2(v3, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v6) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | r1_lattice2(v1, v4, v6) | v1_xboole_0(v1))) % 15.66/4.20 | % 15.66/4.20 | Instantiating (418) with all_170_0_79 yields: % 15.66/4.20 | (459) k1_zfmisc_1(all_23_1_28) = all_170_0_79 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ v3_binop_1(v2, all_23_1_28) | ~ m1_subset_1(v0, all_170_0_79) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v3_binop_1(v3, v0) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_170_0_79) | ~ v2_binop_1(v2, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v2_binop_1(v3, v0) | v1_xboole_0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_170_0_79) | ~ v1_binop_1(v2, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v1_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.66/4.20 | % 15.66/4.20 | Applying alpha-rule on (459) yields: % 15.66/4.20 | (460) k1_zfmisc_1(all_23_1_28) = all_170_0_79 % 15.66/4.20 | (461) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ v3_binop_1(v2, all_23_1_28) | ~ m1_subset_1(v0, all_170_0_79) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v3_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.66/4.20 | (462) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_170_0_79) | ~ v2_binop_1(v2, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v2_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.66/4.20 | (463) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_170_0_79) | ~ v1_binop_1(v2, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | v1_binop_1(v3, v0) | v1_xboole_0(v0)) % 15.66/4.20 | % 15.66/4.20 | Instantiating (426) with all_173_0_80 yields: % 15.66/4.20 | (464) k1_zfmisc_1(all_23_1_28) = all_173_0_80 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (k1_realset1(v4, v0) = v5) | ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_173_0_80) | ~ r1_lattice2(all_23_1_28, v2, v4) | ~ m2_relset_1(v5, v1, v0) | ~ m2_relset_1(v4, all_51_0_39, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_2(v4, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | r1_lattice2(v0, v3, v5) | v1_xboole_0(v0)) % 15.66/4.20 | % 15.66/4.20 | Applying alpha-rule on (464) yields: % 15.66/4.20 | (465) k1_zfmisc_1(all_23_1_28) = all_173_0_80 % 15.66/4.20 | (466) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (k1_realset1(v4, v0) = v5) | ~ (k1_realset1(v2, v0) = v3) | ~ (k2_zfmisc_1(v0, v0) = v1) | ~ m1_subset_1(v0, all_173_0_80) | ~ r1_lattice2(all_23_1_28, v2, v4) | ~ m2_relset_1(v5, v1, v0) | ~ m2_relset_1(v4, all_51_0_39, all_23_1_28) | ~ m2_relset_1(v3, v1, v0) | ~ m2_relset_1(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v5, v1, v0) | ~ v1_funct_2(v4, all_51_0_39, all_23_1_28) | ~ v1_funct_2(v3, v1, v0) | ~ v1_funct_2(v2, all_51_0_39, all_23_1_28) | ~ v1_funct_1(v5) | ~ v1_funct_1(v4) | ~ v1_funct_1(v3) | ~ v1_funct_1(v2) | r1_lattice2(v0, v3, v5) | v1_xboole_0(v0)) % 15.66/4.20 | % 15.66/4.20 | Instantiating formula (41) with all_23_1_28, all_173_0_80, all_71_0_53 and discharging atoms k1_zfmisc_1(all_23_1_28) = all_173_0_80, k1_zfmisc_1(all_23_1_28) = all_71_0_53, yields: % 15.66/4.20 | (467) all_173_0_80 = all_71_0_53 % 15.66/4.20 | % 15.66/4.20 | Instantiating formula (41) with all_23_1_28, all_170_0_79, all_173_0_80 and discharging atoms k1_zfmisc_1(all_23_1_28) = all_173_0_80, k1_zfmisc_1(all_23_1_28) = all_170_0_79, yields: % 15.66/4.20 | (468) all_173_0_80 = all_170_0_79 % 15.66/4.20 | % 15.66/4.20 | Combining equations (468,467) yields a new equation: % 15.66/4.20 | (469) all_170_0_79 = all_71_0_53 % 15.66/4.20 | % 15.66/4.20 | Simplifying 469 yields: % 15.66/4.20 | (470) all_170_0_79 = all_71_0_53 % 15.66/4.20 | % 15.66/4.20 +-Applying beta-rule and splitting (443), into two cases. % 15.66/4.20 |-Branch one: % 15.66/4.20 | (471) ~ r1_lattice2(all_0_13_13, all_0_11_11, all_0_10_10) % 15.66/4.20 | % 15.66/4.20 | Instantiating formula (466) with all_0_10_10, all_0_14_14, all_0_11_11, all_0_15_15, all_0_12_12, all_0_13_13 and discharging atoms k1_realset1(all_0_14_14, all_0_13_13) = all_0_10_10, k1_realset1(all_0_15_15, all_0_13_13) = all_0_11_11, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, r1_lattice2(all_23_1_28, all_0_15_15, all_0_14_14), m2_relset_1(all_0_10_10, all_0_12_12, all_0_13_13), m2_relset_1(all_0_11_11, all_0_12_12, all_0_13_13), m2_relset_1(all_0_14_14, all_51_0_39, all_23_1_28), m2_relset_1(all_0_15_15, all_51_0_39, all_23_1_28), v1_funct_2(all_0_10_10, all_0_12_12, all_0_13_13), v1_funct_2(all_0_11_11, all_0_12_12, all_0_13_13), v1_funct_2(all_0_14_14, all_51_0_39, all_23_1_28), v1_funct_2(all_0_15_15, all_51_0_39, all_23_1_28), v1_funct_1(all_0_10_10), v1_funct_1(all_0_11_11), v1_funct_1(all_0_14_14), v1_funct_1(all_0_15_15), ~ r1_lattice2(all_0_13_13, all_0_11_11, all_0_10_10), ~ v1_xboole_0(all_0_13_13), yields: % 15.66/4.20 | (472) ~ m1_subset_1(all_0_13_13, all_173_0_80) % 15.66/4.20 | % 15.66/4.20 | From (467) and (472) follows: % 15.66/4.20 | (440) ~ m1_subset_1(all_0_13_13, all_71_0_53) % 15.66/4.20 | % 15.66/4.20 | Using (246) and (440) yields: % 15.66/4.20 | (412) $false % 15.66/4.20 | % 15.66/4.20 |-The branch is then unsatisfiable % 15.66/4.20 |-Branch two: % 15.66/4.20 | (475) r1_lattice2(all_0_13_13, all_0_11_11, all_0_10_10) % 15.66/4.20 | (476) ~ v2_binop_1(all_0_10_10, all_0_13_13) | ~ v2_binop_1(all_0_11_11, all_0_13_13) | ~ v1_binop_1(all_0_10_10, all_0_13_13) | ~ v1_binop_1(all_0_11_11, all_0_13_13) % 15.66/4.20 | % 15.66/4.20 +-Applying beta-rule and splitting (476), into two cases. % 15.66/4.20 |-Branch one: % 15.66/4.20 | (477) ~ v2_binop_1(all_0_10_10, all_0_13_13) % 15.66/4.20 | % 15.66/4.20 | Instantiating formula (462) with all_0_10_10, all_0_14_14, all_0_12_12, all_0_13_13 and discharging atoms k1_realset1(all_0_14_14, all_0_13_13) = all_0_10_10, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, v2_binop_1(all_0_14_14, all_23_1_28), m2_relset_1(all_0_10_10, all_0_12_12, all_0_13_13), m2_relset_1(all_0_14_14, all_51_0_39, all_23_1_28), v1_funct_2(all_0_10_10, all_0_12_12, all_0_13_13), v1_funct_2(all_0_14_14, all_51_0_39, all_23_1_28), v1_funct_1(all_0_10_10), v1_funct_1(all_0_14_14), ~ v2_binop_1(all_0_10_10, all_0_13_13), ~ v1_xboole_0(all_0_13_13), yields: % 15.66/4.20 | (478) ~ m1_subset_1(all_0_13_13, all_170_0_79) % 15.66/4.20 | % 15.66/4.20 | From (470) and (478) follows: % 15.66/4.20 | (440) ~ m1_subset_1(all_0_13_13, all_71_0_53) % 15.66/4.20 | % 15.66/4.20 | Using (246) and (440) yields: % 15.66/4.20 | (412) $false % 15.66/4.20 | % 15.66/4.20 |-The branch is then unsatisfiable % 15.66/4.20 |-Branch two: % 15.66/4.20 | (481) v2_binop_1(all_0_10_10, all_0_13_13) % 15.66/4.20 | (482) ~ v2_binop_1(all_0_11_11, all_0_13_13) | ~ v1_binop_1(all_0_10_10, all_0_13_13) | ~ v1_binop_1(all_0_11_11, all_0_13_13) % 15.66/4.20 | % 15.66/4.20 +-Applying beta-rule and splitting (482), into two cases. % 15.66/4.20 |-Branch one: % 15.66/4.20 | (483) ~ v2_binop_1(all_0_11_11, all_0_13_13) % 15.66/4.20 | % 15.66/4.20 | Instantiating formula (462) with all_0_11_11, all_0_15_15, all_0_12_12, all_0_13_13 and discharging atoms k1_realset1(all_0_15_15, all_0_13_13) = all_0_11_11, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, v2_binop_1(all_0_15_15, all_23_1_28), m2_relset_1(all_0_11_11, all_0_12_12, all_0_13_13), m2_relset_1(all_0_15_15, all_51_0_39, all_23_1_28), v1_funct_2(all_0_11_11, all_0_12_12, all_0_13_13), v1_funct_2(all_0_15_15, all_51_0_39, all_23_1_28), v1_funct_1(all_0_11_11), v1_funct_1(all_0_15_15), ~ v2_binop_1(all_0_11_11, all_0_13_13), ~ v1_xboole_0(all_0_13_13), yields: % 15.66/4.20 | (478) ~ m1_subset_1(all_0_13_13, all_170_0_79) % 15.66/4.20 | % 15.66/4.20 | From (470) and (478) follows: % 15.66/4.21 | (440) ~ m1_subset_1(all_0_13_13, all_71_0_53) % 15.66/4.21 | % 15.66/4.21 | Using (246) and (440) yields: % 15.66/4.21 | (412) $false % 15.66/4.21 | % 15.66/4.21 |-The branch is then unsatisfiable % 15.66/4.21 |-Branch two: % 15.66/4.21 | (487) v2_binop_1(all_0_11_11, all_0_13_13) % 15.66/4.21 | (488) ~ v1_binop_1(all_0_10_10, all_0_13_13) | ~ v1_binop_1(all_0_11_11, all_0_13_13) % 15.66/4.21 | % 15.66/4.21 +-Applying beta-rule and splitting (488), into two cases. % 15.66/4.21 |-Branch one: % 15.66/4.21 | (489) ~ v1_binop_1(all_0_10_10, all_0_13_13) % 15.66/4.21 | % 15.66/4.21 | Instantiating formula (463) with all_0_10_10, all_0_14_14, all_0_12_12, all_0_13_13 and discharging atoms k1_realset1(all_0_14_14, all_0_13_13) = all_0_10_10, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, v1_binop_1(all_0_14_14, all_23_1_28), m2_relset_1(all_0_10_10, all_0_12_12, all_0_13_13), m2_relset_1(all_0_14_14, all_51_0_39, all_23_1_28), v1_funct_2(all_0_10_10, all_0_12_12, all_0_13_13), v1_funct_2(all_0_14_14, all_51_0_39, all_23_1_28), v1_funct_1(all_0_10_10), v1_funct_1(all_0_14_14), ~ v1_binop_1(all_0_10_10, all_0_13_13), ~ v1_xboole_0(all_0_13_13), yields: % 15.66/4.21 | (478) ~ m1_subset_1(all_0_13_13, all_170_0_79) % 15.66/4.21 | % 15.66/4.21 | From (470) and (478) follows: % 15.66/4.21 | (440) ~ m1_subset_1(all_0_13_13, all_71_0_53) % 15.66/4.21 | % 15.66/4.21 | Using (246) and (440) yields: % 15.66/4.21 | (412) $false % 15.66/4.21 | % 15.66/4.21 |-The branch is then unsatisfiable % 15.66/4.21 |-Branch two: % 15.66/4.21 | (493) v1_binop_1(all_0_10_10, all_0_13_13) % 15.66/4.21 | (494) ~ v1_binop_1(all_0_11_11, all_0_13_13) % 15.66/4.21 | % 15.66/4.21 | Instantiating formula (463) with all_0_11_11, all_0_15_15, all_0_12_12, all_0_13_13 and discharging atoms k1_realset1(all_0_15_15, all_0_13_13) = all_0_11_11, k2_zfmisc_1(all_0_13_13, all_0_13_13) = all_0_12_12, v1_binop_1(all_0_15_15, all_23_1_28), m2_relset_1(all_0_11_11, all_0_12_12, all_0_13_13), m2_relset_1(all_0_15_15, all_51_0_39, all_23_1_28), v1_funct_2(all_0_11_11, all_0_12_12, all_0_13_13), v1_funct_2(all_0_15_15, all_51_0_39, all_23_1_28), v1_funct_1(all_0_11_11), v1_funct_1(all_0_15_15), ~ v1_binop_1(all_0_11_11, all_0_13_13), ~ v1_xboole_0(all_0_13_13), yields: % 15.66/4.21 | (478) ~ m1_subset_1(all_0_13_13, all_170_0_79) % 15.66/4.21 | % 15.66/4.21 | From (470) and (478) follows: % 15.66/4.21 | (440) ~ m1_subset_1(all_0_13_13, all_71_0_53) % 15.66/4.21 | % 15.66/4.21 | Using (246) and (440) yields: % 15.66/4.21 | (412) $false % 15.66/4.21 | % 15.66/4.21 |-The branch is then unsatisfiable % 15.66/4.21 % SZS output end Proof for theBenchmark % 15.66/4.21 % 15.66/4.21 3628ms %------------------------------------------------------------------------------