%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : LAT287+1 : TPTP v8.1.2. Released v3.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n010.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 : 300s % DateTime : Thu Aug 31 06:24:24 EDT 2023 % Result : Theorem 173.17s 24.14s % Output : Proof 173.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : LAT287+1 : TPTP v8.1.2. Released v3.4.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n010.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Aug 24 09:08:51 EDT 2023 % 0.12/0.34 % CPUTime : % 0.20/0.61 ________ _____ % 0.20/0.61 ___ __ \_________(_)________________________________ % 0.20/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.61 % 0.20/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.61 (2023-06-19) % 0.20/0.61 % 0.20/0.61 (c) Philipp Rümmer, 2009-2023 % 0.20/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.61 Amanda Stjerna. % 0.20/0.61 Free software under BSD-3-Clause. % 0.20/0.61 % 0.20/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.61 % 0.20/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.03/1.37 Prover 4: Preprocessing ... % 4.03/1.37 Prover 1: Preprocessing ... % 4.66/1.40 Prover 2: Preprocessing ... % 4.66/1.40 Prover 6: Preprocessing ... % 4.66/1.40 Prover 3: Preprocessing ... % 4.66/1.40 Prover 0: Preprocessing ... % 4.66/1.42 Prover 5: Preprocessing ... % 10.69/2.29 Prover 5: Proving ... % 11.29/2.34 Prover 1: Warning: ignoring some quantifiers % 11.29/2.36 Prover 3: Warning: ignoring some quantifiers % 11.59/2.39 Prover 2: Proving ... % 11.59/2.43 Prover 6: Proving ... % 12.08/2.45 Prover 3: Constructing countermodel ... % 12.35/2.48 Prover 1: Constructing countermodel ... % 14.56/2.78 Prover 4: Warning: ignoring some quantifiers % 14.56/2.89 Prover 4: Constructing countermodel ... % 14.56/2.94 Prover 0: Proving ... % 71.64/10.32 Prover 2: stopped % 71.64/10.34 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 72.48/10.47 Prover 7: Preprocessing ... % 73.61/10.60 Prover 7: Warning: ignoring some quantifiers % 73.95/10.62 Prover 7: Constructing countermodel ... % 99.26/13.98 Prover 5: stopped % 99.26/13.99 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 99.87/14.09 Prover 8: Preprocessing ... % 101.41/14.26 Prover 8: Warning: ignoring some quantifiers % 101.61/14.28 Prover 8: Constructing countermodel ... % 113.95/15.99 Prover 1: stopped % 113.95/16.02 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 115.19/16.13 Prover 9: Preprocessing ... % 118.33/16.52 Prover 9: Warning: ignoring some quantifiers % 118.83/16.57 Prover 9: Constructing countermodel ... % 128.19/17.91 Prover 6: stopped % 128.19/17.92 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 129.53/18.08 Prover 10: Preprocessing ... % 129.53/18.21 Prover 10: Warning: ignoring some quantifiers % 129.53/18.22 Prover 10: Constructing countermodel ... % 134.68/18.73 Prover 10: gave up % 134.68/18.74 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 135.17/18.88 Prover 11: Preprocessing ... % 139.04/19.30 Prover 11: Warning: ignoring some quantifiers % 139.04/19.32 Prover 11: Constructing countermodel ... % 172.63/24.02 Prover 7: Found proof (size 225) % 172.63/24.02 Prover 7: proved (13629ms) % 172.63/24.02 Prover 9: stopped % 172.63/24.02 Prover 0: stopped % 172.63/24.02 Prover 11: stopped % 172.63/24.03 Prover 4: stopped % 172.63/24.03 Prover 8: stopped % 173.17/24.14 Prover 3: stopped % 173.17/24.14 % 173.17/24.14 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 173.17/24.14 % 173.17/24.16 % SZS output start Proof for theBenchmark % 173.17/24.17 Assumptions after simplification: % 173.17/24.17 --------------------------------- % 173.17/24.17 % 173.17/24.17 (abstractness_v3_lattices) % 173.17/24.20 ! [v0: $i] : ! [v1: $i] : ( ~ (u2_lattices(v0) = v1) | ~ $i(v0) | ~ % 173.17/24.20 v3_lattices(v0) | ~ l3_lattices(v0) | ? [v2: $i] : ? [v3: $i] : % 173.17/24.20 (g3_lattices(v2, v1, v3) = v0 & u1_struct_0(v0) = v2 & u1_lattices(v0) = v3 % 173.17/24.20 & $i(v3) & $i(v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = % 173.17/24.20 v1) | ~ $i(v0) | ~ v3_lattices(v0) | ~ l3_lattices(v0) | ? [v2: $i] : % 173.17/24.20 ? [v3: $i] : (g3_lattices(v1, v2, v3) = v0 & u2_lattices(v0) = v2 & % 173.17/24.20 u1_lattices(v0) = v3 & $i(v3) & $i(v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 173.17/24.20 (u1_lattices(v0) = v1) | ~ $i(v0) | ~ v3_lattices(v0) | ~ l3_lattices(v0) % 173.17/24.20 | ? [v2: $i] : ? [v3: $i] : (g3_lattices(v2, v3, v1) = v0 & % 173.17/24.20 u2_lattices(v0) = v3 & u1_struct_0(v0) = v2 & $i(v3) & $i(v2))) % 173.17/24.20 % 173.17/24.20 (d4_lopclset) % 173.33/24.21 ! [v0: $i] : ! [v1: $i] : ( ~ (k6_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.33/24.21 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? % 173.33/24.21 [v3: $i] : ? [v4: $i] : (k5_lopclset(v0) = v4 & k1_lopclset(v0) = v2 & % 173.33/24.21 k4_lopclset(v0) = v3 & g3_lattices(v2, v3, v4) = v1 & $i(v4) & $i(v3) & % 173.33/24.21 $i(v2) & $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k5_lopclset(v0) = v1) % 173.33/24.21 | ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? % 173.33/24.21 [v2: $i] : ? [v3: $i] : ? [v4: $i] : (k6_lopclset(v0) = v2 & % 173.33/24.21 k1_lopclset(v0) = v3 & k4_lopclset(v0) = v4 & g3_lattices(v3, v4, v1) = v2 % 173.33/24.21 & $i(v4) & $i(v3) & $i(v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 173.33/24.21 (k1_lopclset(v0) = v1) | ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) % 173.33/24.21 | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 173.33/24.21 (k6_lopclset(v0) = v2 & k5_lopclset(v0) = v4 & k4_lopclset(v0) = v3 & % 173.33/24.21 g3_lattices(v1, v3, v4) = v2 & $i(v4) & $i(v3) & $i(v2))) & ! [v0: $i] : % 173.33/24.21 ! [v1: $i] : ( ~ (k4_lopclset(v0) = v1) | ~ $i(v0) | ~ l1_pre_topc(v0) | ~ % 173.33/24.21 v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 173.33/24.21 : (k6_lopclset(v0) = v2 & k5_lopclset(v0) = v4 & k1_lopclset(v0) = v3 & % 173.33/24.21 g3_lattices(v3, v1, v4) = v2 & $i(v4) & $i(v3) & $i(v2))) % 173.33/24.21 % 173.33/24.21 (dt_g3_lattices) % 173.33/24.22 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (g3_lattices(v0, % 173.33/24.22 v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ v1_funct_1(v2) | % 173.33/24.22 ~ v1_funct_1(v1) | v3_lattices(v3) | ? [v4: $i] : (k2_zfmisc_1(v0, v0) = v4 % 173.33/24.22 & $i(v4) & ( ~ m1_relset_1(v2, v4, v0) | ~ m1_relset_1(v1, v4, v0) | ~ % 173.33/24.22 v1_funct_2(v2, v4, v0) | ~ v1_funct_2(v1, v4, v0)))) & ! [v0: $i] : ! % 173.33/24.22 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (g3_lattices(v0, v1, v2) = v3) | ~ % 173.33/24.22 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | % 173.33/24.22 l3_lattices(v3) | ? [v4: $i] : (k2_zfmisc_1(v0, v0) = v4 & $i(v4) & ( ~ % 173.33/24.22 m1_relset_1(v2, v4, v0) | ~ m1_relset_1(v1, v4, v0) | ~ v1_funct_2(v2, % 173.33/24.22 v4, v0) | ~ v1_funct_2(v1, v4, v0)))) % 173.33/24.22 % 173.33/24.22 (dt_k1_lopclset) % 173.57/24.22 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.22 l1_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] % 173.57/24.22 : (k1_zfmisc_1(v3) = v4 & k1_zfmisc_1(v2) = v3 & u1_struct_0(v0) = v2 & % 173.57/24.22 $i(v4) & $i(v3) & $i(v2) & m1_subset_1(v1, v4))) & ! [v0: $i] : ! [v1: % 173.57/24.22 $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ l1_pre_topc(v0) | % 173.57/24.22 v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (k1_lopclset(v0) % 173.57/24.22 = v2 & k1_zfmisc_1(v3) = v4 & k1_zfmisc_1(v1) = v3 & $i(v4) & $i(v3) & % 173.57/24.22 $i(v2) & m1_subset_1(v2, v4))) % 173.57/24.22 % 173.57/24.22 (dt_k1_pre_topc) % 173.57/24.22 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.22 l1_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : (k1_zfmisc_1(v2) = v3 & % 173.57/24.22 u1_struct_0(v0) = v2 & $i(v3) & $i(v2) & m1_subset_1(v1, v3))) & ! [v0: % 173.57/24.22 $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.22 l1_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : (k1_pre_topc(v0) = v2 & % 173.57/24.22 k1_zfmisc_1(v1) = v3 & $i(v3) & $i(v2) & m1_subset_1(v2, v3))) % 173.57/24.22 % 173.57/24.22 (dt_k4_lopclset) % 173.57/24.23 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.23 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? % 173.57/24.23 [v3: $i] : (k4_lopclset(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & $i(v3) & % 173.57/24.23 $i(v2) & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & % 173.57/24.23 v1_funct_1(v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k4_lopclset(v0) = v1) % 173.57/24.23 | ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v1_funct_1(v1) | % 173.57/24.23 v3_struct_0(v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (k4_lopclset(v0) = v1) | % 173.57/24.23 ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? % 173.57/24.23 [v2: $i] : ? [v3: $i] : (k1_lopclset(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & % 173.57/24.23 $i(v3) & $i(v2) & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) % 173.57/24.23 % 173.57/24.23 (dt_k5_lopclset) % 173.57/24.23 ! [v0: $i] : ! [v1: $i] : ( ~ (k5_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.23 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v1_funct_1(v1) | v3_struct_0(v0)) & % 173.57/24.23 ! [v0: $i] : ! [v1: $i] : ( ~ (k5_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.23 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? % 173.57/24.23 [v3: $i] : (k1_lopclset(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & $i(v3) & % 173.57/24.23 $i(v2) & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) & ! [v0: $i] % 173.57/24.23 : ! [v1: $i] : ( ~ (k1_lopclset(v0) = v1) | ~ $i(v0) | ~ l1_pre_topc(v0) | % 173.57/24.23 ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : % 173.57/24.23 (k5_lopclset(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 & $i(v3) & $i(v2) & % 173.57/24.23 m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 173.57/24.23 % 173.57/24.23 (dt_k6_lopclset) % 173.57/24.23 ! [v0: $i] : ! [v1: $i] : ( ~ (k6_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.23 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ~ v3_struct_0(v1) | v3_struct_0(v0)) % 173.57/24.23 & ! [v0: $i] : ! [v1: $i] : ( ~ (k6_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.23 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v10_lattices(v1) | v3_struct_0(v0)) & % 173.57/24.23 ! [v0: $i] : ! [v1: $i] : ( ~ (k6_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.23 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | l3_lattices(v1) | v3_struct_0(v0)) % 173.57/24.23 % 173.57/24.23 (dt_l1_pre_topc) % 173.57/24.23 ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | l1_struct_0(v0)) % 173.57/24.23 % 173.57/24.23 (dt_l3_lattices) % 173.57/24.23 ! [v0: $i] : ( ~ $i(v0) | ~ l3_lattices(v0) | l2_lattices(v0)) & ! [v0: $i] % 173.57/24.23 : ( ~ $i(v0) | ~ l3_lattices(v0) | l1_lattices(v0)) % 173.57/24.23 % 173.57/24.23 (dt_u1_lattices) % 173.57/24.24 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.24 l1_lattices(v0) | ? [v2: $i] : ? [v3: $i] : (u1_lattices(v0) = v2 & % 173.57/24.24 k2_zfmisc_1(v1, v1) = v3 & $i(v3) & $i(v2) & m2_relset_1(v2, v3, v1) & % 173.57/24.24 v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0: $i] : ! [v1: $i] : ( % 173.57/24.24 ~ (u1_lattices(v0) = v1) | ~ $i(v0) | ~ l1_lattices(v0) | v1_funct_1(v1)) % 173.57/24.24 & ! [v0: $i] : ! [v1: $i] : ( ~ (u1_lattices(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.24 l1_lattices(v0) | ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v2 & % 173.57/24.24 k2_zfmisc_1(v2, v2) = v3 & $i(v3) & $i(v2) & m2_relset_1(v1, v3, v2) & % 173.57/24.24 v1_funct_2(v1, v3, v2))) % 173.57/24.24 % 173.57/24.24 (dt_u2_lattices) % 173.57/24.24 ! [v0: $i] : ! [v1: $i] : ( ~ (u2_lattices(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.24 l2_lattices(v0) | v1_funct_1(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 173.57/24.24 (u2_lattices(v0) = v1) | ~ $i(v0) | ~ l2_lattices(v0) | ? [v2: $i] : ? % 173.57/24.24 [v3: $i] : (u1_struct_0(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & $i(v3) & % 173.57/24.24 $i(v2) & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, v2))) & ! [v0: $i] % 173.57/24.24 : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ l2_lattices(v0) | % 173.57/24.24 ? [v2: $i] : ? [v3: $i] : (u2_lattices(v0) = v2 & k2_zfmisc_1(v1, v1) = v3 % 173.57/24.24 & $i(v3) & $i(v2) & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, v3, v1) & % 173.57/24.24 v1_funct_1(v2))) % 173.57/24.24 % 173.57/24.24 (fc1_finsub_1) % 173.57/24.24 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.24 v1_xboole_0(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ (k1_zfmisc_1(v0) = v1) | % 173.57/24.24 ~ $i(v0) | v3_finsub_1(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 173.57/24.24 (k1_zfmisc_1(v0) = v1) | ~ $i(v0) | v1_finsub_1(v1)) & ! [v0: $i] : ! % 173.57/24.24 [v1: $i] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ $i(v0) | v4_finsub_1(v1)) % 173.57/24.24 % 173.57/24.24 (fc1_lopclset) % 173.57/24.24 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.24 v1_xboole_0(v1) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0)) % 173.57/24.24 % 173.57/24.24 (fc1_pre_topc) % 173.57/24.24 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.24 l1_struct_0(v0) | v1_xboole_0(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 173.57/24.24 (k1_pre_topc(v0) = v1) | ~ $i(v0) | ~ l1_struct_0(v0) | v5_membered(v1)) & % 173.57/24.24 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.24 l1_struct_0(v0) | v4_membered(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 173.57/24.24 (k1_pre_topc(v0) = v1) | ~ $i(v0) | ~ l1_struct_0(v0) | v3_membered(v1)) & % 173.57/24.24 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.24 l1_struct_0(v0) | v2_membered(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 173.57/24.24 (k1_pre_topc(v0) = v1) | ~ $i(v0) | ~ l1_struct_0(v0) | v1_membered(v1)) % 173.57/24.24 % 173.57/24.24 (free_g3_lattices) % 173.57/24.25 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 173.57/24.25 $i] : ! [v6: $i] : (v6 = v2 | ~ (g3_lattices(v4, v5, v6) = v3) | ~ % 173.57/24.25 (g3_lattices(v0, v1, v2) = v3) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ % 173.57/24.25 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | ? % 173.57/24.25 [v7: $i] : (k2_zfmisc_1(v0, v0) = v7 & $i(v7) & ( ~ m1_relset_1(v2, v7, v0) % 173.57/24.25 | ~ m1_relset_1(v1, v7, v0) | ~ v1_funct_2(v2, v7, v0) | ~ % 173.57/24.25 v1_funct_2(v1, v7, v0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 173.57/24.25 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v5 = v1 | ~ % 173.57/24.25 (g3_lattices(v4, v5, v6) = v3) | ~ (g3_lattices(v0, v1, v2) = v3) | ~ % 173.57/24.25 $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 173.57/24.25 v1_funct_1(v2) | ~ v1_funct_1(v1) | ? [v7: $i] : (k2_zfmisc_1(v0, v0) = v7 % 173.57/24.25 & $i(v7) & ( ~ m1_relset_1(v2, v7, v0) | ~ m1_relset_1(v1, v7, v0) | ~ % 173.57/24.25 v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, v7, v0)))) & ! [v0: $i] : ! % 173.57/24.25 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] % 173.57/24.25 : (v4 = v0 | ~ (g3_lattices(v4, v5, v6) = v3) | ~ (g3_lattices(v0, v1, v2) = % 173.57/24.25 v3) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v2) | ~ $i(v1) | ~ % 173.57/24.25 $i(v0) | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | ? [v7: $i] : % 173.57/24.25 (k2_zfmisc_1(v0, v0) = v7 & $i(v7) & ( ~ m1_relset_1(v2, v7, v0) | ~ % 173.57/24.25 m1_relset_1(v1, v7, v0) | ~ v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, % 173.57/24.25 v7, v0)))) % 173.57/24.25 % 173.57/24.25 (redefinition_m2_relset_1) % 173.57/24.25 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 173.57/24.25 ~ m1_relset_1(v2, v0, v1) | m2_relset_1(v2, v0, v1)) & ! [v0: $i] : ! % 173.57/24.25 [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 173.57/24.25 m2_relset_1(v2, v0, v1) | m1_relset_1(v2, v0, v1)) % 173.57/24.25 % 173.57/24.25 (redefinition_m2_subset_1) % 173.57/24.25 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (k1_zfmisc_1(v0) = % 173.57/24.25 v2) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ~ m2_subset_1(v3, v0, v1) | ~ % 173.57/24.25 m1_subset_1(v1, v2) | v1_xboole_0(v1) | v1_xboole_0(v0) | m1_subset_1(v3, % 173.57/24.25 v1)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 173.57/24.25 (k1_zfmisc_1(v0) = v2) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ~ % 173.57/24.25 m1_subset_1(v3, v1) | ~ m1_subset_1(v1, v2) | m2_subset_1(v3, v0, v1) | % 173.57/24.25 v1_xboole_0(v1) | v1_xboole_0(v0)) % 173.57/24.25 % 173.57/24.25 (t16_lopclset) % 173.57/24.25 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (k6_lopclset(v0) = v2 % 173.57/24.25 & k1_pre_topc(v0) = v1 & u1_struct_0(v2) = v3 & $i(v3) & $i(v2) & $i(v1) & % 173.57/24.25 $i(v0) & l1_pre_topc(v0) & v2_pre_topc(v0) & ~ m1_subset_1(v1, v3) & ~ % 173.57/24.25 v3_struct_0(v0)) % 173.57/24.25 % 173.57/24.25 (t2_subset) % 173.57/24.25 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ m1_subset_1(v0, v1) | % 173.57/24.25 v1_xboole_0(v1) | r2_hidden(v0, v1)) % 173.57/24.25 % 173.57/24.25 (t6_boole) % 173.57/24.25 $i(k1_xboole_0) & ! [v0: $i] : (v0 = k1_xboole_0 | ~ $i(v0) | ~ % 173.57/24.25 v1_xboole_0(v0)) % 173.57/24.25 % 173.57/24.25 (t7_lopclset) % 173.57/24.26 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.26 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? % 173.57/24.26 [v3: $i] : ? [v4: $i] : (k1_lopclset(v0) = v4 & k1_zfmisc_1(v2) = v3 & % 173.57/24.26 u1_struct_0(v0) = v2 & $i(v4) & $i(v3) & $i(v2) & m2_subset_1(v1, v3, % 173.57/24.26 v4))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k1_lopclset(v0) = v1) | ~ % 173.57/24.26 $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 173.57/24.26 $i] : ? [v3: $i] : ? [v4: $i] : (k1_pre_topc(v0) = v2 & k1_zfmisc_1(v3) % 173.57/24.26 = v4 & u1_struct_0(v0) = v3 & $i(v4) & $i(v3) & $i(v2) & m2_subset_1(v2, % 173.57/24.26 v4, v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ % 173.57/24.26 $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 173.57/24.26 $i] : ? [v3: $i] : ? [v4: $i] : (k1_pre_topc(v0) = v2 & k1_lopclset(v0) % 173.57/24.26 = v4 & k1_zfmisc_1(v1) = v3 & $i(v4) & $i(v3) & $i(v2) & m2_subset_1(v2, % 173.57/24.26 v3, v4))) % 173.57/24.26 % 173.57/24.26 (function-axioms) % 173.57/24.26 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 % 173.57/24.26 | ~ (g3_lattices(v4, v3, v2) = v1) | ~ (g3_lattices(v4, v3, v2) = v0)) & % 173.57/24.26 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 173.57/24.26 (k2_zfmisc_1(v3, v2) = v1) | ~ (k2_zfmisc_1(v3, v2) = v0)) & ! [v0: $i] : % 173.57/24.26 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k6_lopclset(v2) = v1) | ~ % 173.57/24.26 (k6_lopclset(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 173.57/24.26 | ~ (a_1_0_lopclset(v2) = v1) | ~ (a_1_0_lopclset(v2) = v0)) & ! [v0: $i] % 173.57/24.26 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k1_pre_topc(v2) = v1) | ~ % 173.57/24.26 (k1_pre_topc(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 173.57/24.26 | ~ (k5_lopclset(v2) = v1) | ~ (k5_lopclset(v2) = v0)) & ! [v0: $i] : ! % 173.57/24.26 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k1_lopclset(v2) = v1) | ~ % 173.57/24.26 (k1_lopclset(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 173.57/24.26 | ~ (k4_lopclset(v2) = v1) | ~ (k4_lopclset(v2) = v0)) & ! [v0: $i] : ! % 173.57/24.26 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k1_zfmisc_1(v2) = v1) | ~ % 173.57/24.26 (k1_zfmisc_1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 173.57/24.26 | ~ (u2_lattices(v2) = v1) | ~ (u2_lattices(v2) = v0)) & ! [v0: $i] : ! % 173.57/24.26 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (u1_struct_0(v2) = v1) | ~ % 173.57/24.26 (u1_struct_0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 173.57/24.26 | ~ (u1_lattices(v2) = v1) | ~ (u1_lattices(v2) = v0)) % 173.57/24.26 % 173.57/24.26 Further assumptions not needed in the proof: % 173.57/24.26 -------------------------------------------- % 173.57/24.26 antisymmetry_r2_hidden, cc10_membered, cc11_membered, cc12_membered, % 173.57/24.26 cc13_membered, cc14_membered, cc15_membered, cc16_membered, cc17_membered, % 173.57/24.26 cc18_membered, cc19_membered, cc1_finset_1, cc1_finsub_1, cc1_funct_2, % 173.57/24.26 cc1_lattices, cc1_membered, cc1_relset_1, cc20_membered, cc2_finset_1, % 173.57/24.26 cc2_finsub_1, cc2_lattices, cc2_membered, cc3_membered, cc4_membered, % 173.57/24.26 cc5_funct_2, cc6_funct_2, d1_lopclset, dt_k1_xboole_0, dt_k1_zfmisc_1, % 173.57/24.26 dt_k2_zfmisc_1, dt_l1_lattices, dt_l1_struct_0, dt_l2_lattices, dt_m1_relset_1, % 173.57/24.26 dt_m1_subset_1, dt_m2_relset_1, dt_m2_subset_1, dt_u1_struct_0, % 173.57/24.26 existence_l1_lattices, existence_l1_pre_topc, existence_l1_struct_0, % 173.57/24.26 existence_l2_lattices, existence_l3_lattices, existence_m1_relset_1, % 173.57/24.26 existence_m1_subset_1, existence_m2_relset_1, existence_m2_subset_1, % 173.57/24.26 fc14_finset_1, fc1_struct_0, fc3_lattices, fc6_membered, % 173.57/24.26 fraenkel_a_1_0_lopclset, rc1_finset_1, rc1_funct_2, rc1_membered, rc2_partfun1, % 173.57/24.26 rc3_finset_1, rc3_lattices, rc3_struct_0, rc4_finset_1, rc5_struct_0, % 173.57/24.26 rc6_lattices, rc6_pre_topc, rc7_pre_topc, rc9_lattices, reflexivity_r1_tarski, % 173.57/24.26 t1_subset, t2_tarski, t3_subset, t4_subset, t5_subset, t7_boole, t8_boole % 173.57/24.26 % 173.57/24.26 Those formulas are unsatisfiable: % 173.57/24.26 --------------------------------- % 173.57/24.26 % 173.57/24.26 Begin of proof % 173.57/24.26 | % 173.57/24.26 | ALPHA: (dt_u1_lattices) implies: % 173.57/24.27 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.27 | l1_lattices(v0) | ? [v2: $i] : ? [v3: $i] : (u1_lattices(v0) = v2 & % 173.57/24.27 | k2_zfmisc_1(v1, v1) = v3 & $i(v3) & $i(v2) & m2_relset_1(v2, v3, % 173.57/24.27 | v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 173.57/24.27 | % 173.57/24.27 | ALPHA: (dt_u2_lattices) implies: % 173.57/24.27 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.27 | l2_lattices(v0) | ? [v2: $i] : ? [v3: $i] : (u2_lattices(v0) = v2 & % 173.57/24.27 | k2_zfmisc_1(v1, v1) = v3 & $i(v3) & $i(v2) & m2_relset_1(v2, v3, % 173.57/24.27 | v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 173.57/24.27 | % 173.57/24.27 | ALPHA: (abstractness_v3_lattices) implies: % 173.57/24.27 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_lattices(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.27 | v3_lattices(v0) | ~ l3_lattices(v0) | ? [v2: $i] : ? [v3: $i] : % 173.57/24.27 | (g3_lattices(v2, v3, v1) = v0 & u2_lattices(v0) = v3 & % 173.57/24.27 | u1_struct_0(v0) = v2 & $i(v3) & $i(v2))) % 173.57/24.27 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.27 | v3_lattices(v0) | ~ l3_lattices(v0) | ? [v2: $i] : ? [v3: $i] : % 173.57/24.27 | (g3_lattices(v1, v2, v3) = v0 & u2_lattices(v0) = v2 & % 173.57/24.27 | u1_lattices(v0) = v3 & $i(v3) & $i(v2))) % 173.57/24.27 | (5) ! [v0: $i] : ! [v1: $i] : ( ~ (u2_lattices(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.27 | v3_lattices(v0) | ~ l3_lattices(v0) | ? [v2: $i] : ? [v3: $i] : % 173.57/24.27 | (g3_lattices(v2, v1, v3) = v0 & u1_struct_0(v0) = v2 & % 173.57/24.27 | u1_lattices(v0) = v3 & $i(v3) & $i(v2))) % 173.57/24.27 | % 173.57/24.27 | ALPHA: (redefinition_m2_relset_1) implies: % 173.57/24.27 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 173.57/24.27 | $i(v0) | ~ m2_relset_1(v2, v0, v1) | m1_relset_1(v2, v0, v1)) % 173.57/24.27 | % 173.57/24.27 | ALPHA: (free_g3_lattices) implies: % 173.57/24.27 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 173.57/24.27 | ! [v5: $i] : ! [v6: $i] : (v4 = v0 | ~ (g3_lattices(v4, v5, v6) = v3) % 173.57/24.27 | | ~ (g3_lattices(v0, v1, v2) = v3) | ~ $i(v6) | ~ $i(v5) | ~ % 173.57/24.27 | $i(v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ v1_funct_1(v2) | ~ % 173.57/24.27 | v1_funct_1(v1) | ? [v7: $i] : (k2_zfmisc_1(v0, v0) = v7 & $i(v7) & ( % 173.57/24.27 | ~ m1_relset_1(v2, v7, v0) | ~ m1_relset_1(v1, v7, v0) | ~ % 173.57/24.27 | v1_funct_2(v2, v7, v0) | ~ v1_funct_2(v1, v7, v0)))) % 173.57/24.27 | % 173.57/24.27 | ALPHA: (dt_g3_lattices) implies: % 173.57/24.27 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 173.57/24.27 | (g3_lattices(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 173.57/24.27 | ~ v1_funct_1(v2) | ~ v1_funct_1(v1) | v3_lattices(v3) | ? [v4: $i] % 173.57/24.27 | : (k2_zfmisc_1(v0, v0) = v4 & $i(v4) & ( ~ m1_relset_1(v2, v4, v0) | % 173.57/24.27 | ~ m1_relset_1(v1, v4, v0) | ~ v1_funct_2(v2, v4, v0) | ~ % 173.57/24.27 | v1_funct_2(v1, v4, v0)))) % 173.57/24.27 | % 173.57/24.27 | ALPHA: (dt_k4_lopclset) implies: % 173.57/24.28 | (9) ! [v0: $i] : ! [v1: $i] : ( ~ (k4_lopclset(v0) = v1) | ~ $i(v0) | ~ % 173.57/24.28 | l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] % 173.57/24.28 | : ? [v3: $i] : (k1_lopclset(v0) = v2 & k2_zfmisc_1(v2, v2) = v3 & % 173.57/24.28 | $i(v3) & $i(v2) & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, v3, % 173.57/24.28 | v2))) % 173.57/24.28 | (10) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_lopclset(v0) = v1) | ~ $i(v0) | % 173.57/24.28 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 173.57/24.28 | $i] : ? [v3: $i] : (k4_lopclset(v0) = v2 & k2_zfmisc_1(v1, v1) = % 173.57/24.28 | v3 & $i(v3) & $i(v2) & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, % 173.57/24.28 | v3, v1) & v1_funct_1(v2))) % 173.57/24.28 | % 173.57/24.28 | ALPHA: (dt_k5_lopclset) implies: % 173.57/24.28 | (11) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_lopclset(v0) = v1) | ~ $i(v0) | % 173.57/24.28 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 173.57/24.28 | $i] : ? [v3: $i] : (k5_lopclset(v0) = v2 & k2_zfmisc_1(v1, v1) = % 173.57/24.28 | v3 & $i(v3) & $i(v2) & m2_relset_1(v2, v3, v1) & v1_funct_2(v2, % 173.57/24.28 | v3, v1) & v1_funct_1(v2))) % 173.57/24.28 | (12) ! [v0: $i] : ! [v1: $i] : ( ~ (k5_lopclset(v0) = v1) | ~ $i(v0) | % 173.57/24.28 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 173.57/24.28 | $i] : ? [v3: $i] : (k1_lopclset(v0) = v2 & k2_zfmisc_1(v2, v2) = % 173.57/24.28 | v3 & $i(v3) & $i(v2) & m2_relset_1(v1, v3, v2) & v1_funct_2(v1, % 173.57/24.28 | v3, v2))) % 173.57/24.28 | % 173.57/24.28 | ALPHA: (dt_l3_lattices) implies: % 173.57/24.28 | (13) ! [v0: $i] : ( ~ $i(v0) | ~ l3_lattices(v0) | l1_lattices(v0)) % 173.57/24.28 | (14) ! [v0: $i] : ( ~ $i(v0) | ~ l3_lattices(v0) | l2_lattices(v0)) % 173.57/24.28 | % 173.57/24.28 | ALPHA: (fc1_pre_topc) implies: % 173.57/24.28 | (15) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_pre_topc(v0) = v1) | ~ $i(v0) | % 173.57/24.28 | ~ l1_struct_0(v0) | v1_xboole_0(v1)) % 173.57/24.28 | % 173.57/24.28 | ALPHA: (t6_boole) implies: % 173.57/24.28 | (16) ! [v0: $i] : (v0 = k1_xboole_0 | ~ $i(v0) | ~ v1_xboole_0(v0)) % 173.57/24.28 | % 173.57/24.28 | ALPHA: (redefinition_m2_subset_1) implies: % 173.57/24.28 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 173.57/24.28 | (k1_zfmisc_1(v0) = v2) | ~ $i(v3) | ~ $i(v1) | ~ $i(v0) | ~ % 173.57/24.28 | m2_subset_1(v3, v0, v1) | ~ m1_subset_1(v1, v2) | v1_xboole_0(v1) | % 173.57/24.28 | v1_xboole_0(v0) | m1_subset_1(v3, v1)) % 173.57/24.28 | % 173.57/24.28 | ALPHA: (dt_k1_lopclset) implies: % 173.57/24.28 | (18) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 173.57/24.28 | ~ l1_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : ? % 173.57/24.28 | [v4: $i] : (k1_lopclset(v0) = v2 & k1_zfmisc_1(v3) = v4 & % 173.57/24.28 | k1_zfmisc_1(v1) = v3 & $i(v4) & $i(v3) & $i(v2) & m1_subset_1(v2, % 173.57/24.28 | v4))) % 173.57/24.29 | (19) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_lopclset(v0) = v1) | ~ $i(v0) | % 173.57/24.29 | ~ l1_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : ? % 173.57/24.29 | [v4: $i] : (k1_zfmisc_1(v3) = v4 & k1_zfmisc_1(v2) = v3 & % 173.57/24.29 | u1_struct_0(v0) = v2 & $i(v4) & $i(v3) & $i(v2) & m1_subset_1(v1, % 173.57/24.29 | v4))) % 173.57/24.29 | % 173.57/24.29 | ALPHA: (dt_k1_pre_topc) implies: % 173.57/24.29 | (20) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 173.57/24.29 | ~ l1_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : (k1_pre_topc(v0) = % 173.57/24.29 | v2 & k1_zfmisc_1(v1) = v3 & $i(v3) & $i(v2) & m1_subset_1(v2, % 173.57/24.29 | v3))) % 173.57/24.29 | (21) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_pre_topc(v0) = v1) | ~ $i(v0) | % 173.57/24.29 | ~ l1_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : (k1_zfmisc_1(v2) = % 173.57/24.29 | v3 & u1_struct_0(v0) = v2 & $i(v3) & $i(v2) & m1_subset_1(v1, % 173.57/24.29 | v3))) % 173.57/24.29 | % 173.57/24.29 | ALPHA: (dt_k6_lopclset) implies: % 173.57/24.29 | (22) ! [v0: $i] : ! [v1: $i] : ( ~ (k6_lopclset(v0) = v1) | ~ $i(v0) | % 173.57/24.29 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | l3_lattices(v1) | % 173.57/24.29 | v3_struct_0(v0)) % 173.57/24.29 | % 173.57/24.29 | ALPHA: (fc1_finsub_1) implies: % 173.57/24.29 | (23) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ $i(v0) | % 173.57/24.29 | ~ v1_xboole_0(v1)) % 173.57/24.29 | % 173.57/24.29 | ALPHA: (d4_lopclset) implies: % 173.57/24.29 | (24) ! [v0: $i] : ! [v1: $i] : ( ~ (k6_lopclset(v0) = v1) | ~ $i(v0) | % 173.57/24.29 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 173.57/24.29 | $i] : ? [v3: $i] : ? [v4: $i] : (k5_lopclset(v0) = v4 & % 173.57/24.29 | k1_lopclset(v0) = v2 & k4_lopclset(v0) = v3 & g3_lattices(v2, v3, % 173.57/24.29 | v4) = v1 & $i(v4) & $i(v3) & $i(v2) & $i(v1))) % 173.57/24.29 | % 173.57/24.29 | ALPHA: (t7_lopclset) implies: % 173.57/24.29 | (25) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_pre_topc(v0) = v1) | ~ $i(v0) | % 173.57/24.29 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 173.57/24.29 | $i] : ? [v3: $i] : ? [v4: $i] : (k1_lopclset(v0) = v4 & % 173.57/24.29 | k1_zfmisc_1(v2) = v3 & u1_struct_0(v0) = v2 & $i(v4) & $i(v3) & % 173.57/24.29 | $i(v2) & m2_subset_1(v1, v3, v4))) % 173.57/24.29 | % 173.57/24.29 | ALPHA: (function-axioms) implies: % 173.57/24.29 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 173.57/24.29 | (u1_lattices(v2) = v1) | ~ (u1_lattices(v2) = v0)) % 173.57/24.29 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 173.57/24.29 | (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) % 173.57/24.29 | (28) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 173.57/24.29 | (u2_lattices(v2) = v1) | ~ (u2_lattices(v2) = v0)) % 173.57/24.29 | (29) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 173.57/24.29 | (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) % 173.57/24.30 | (30) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 173.57/24.30 | (k4_lopclset(v2) = v1) | ~ (k4_lopclset(v2) = v0)) % 173.57/24.30 | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 173.57/24.30 | (k1_lopclset(v2) = v1) | ~ (k1_lopclset(v2) = v0)) % 173.57/24.30 | (32) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 173.57/24.30 | (k5_lopclset(v2) = v1) | ~ (k5_lopclset(v2) = v0)) % 173.57/24.30 | (33) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 173.57/24.30 | (k1_pre_topc(v2) = v1) | ~ (k1_pre_topc(v2) = v0)) % 173.57/24.30 | (34) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 173.57/24.30 | (k2_zfmisc_1(v3, v2) = v1) | ~ (k2_zfmisc_1(v3, v2) = v0)) % 173.57/24.30 | % 173.96/24.30 | DELTA: instantiating (t16_lopclset) with fresh symbols all_100_0, all_100_1, % 173.96/24.30 | all_100_2, all_100_3 gives: % 173.96/24.30 | (35) k6_lopclset(all_100_3) = all_100_1 & k1_pre_topc(all_100_3) = % 173.96/24.30 | all_100_2 & u1_struct_0(all_100_1) = all_100_0 & $i(all_100_0) & % 173.96/24.30 | $i(all_100_1) & $i(all_100_2) & $i(all_100_3) & l1_pre_topc(all_100_3) % 173.96/24.30 | & v2_pre_topc(all_100_3) & ~ m1_subset_1(all_100_2, all_100_0) & ~ % 173.96/24.30 | v3_struct_0(all_100_3) % 173.96/24.30 | % 173.96/24.30 | ALPHA: (35) implies: % 173.96/24.30 | (36) ~ v3_struct_0(all_100_3) % 173.96/24.30 | (37) ~ m1_subset_1(all_100_2, all_100_0) % 173.96/24.30 | (38) v2_pre_topc(all_100_3) % 173.96/24.30 | (39) l1_pre_topc(all_100_3) % 173.96/24.30 | (40) $i(all_100_3) % 173.96/24.30 | (41) u1_struct_0(all_100_1) = all_100_0 % 173.96/24.30 | (42) k1_pre_topc(all_100_3) = all_100_2 % 173.96/24.30 | (43) k6_lopclset(all_100_3) = all_100_1 % 173.96/24.30 | % 173.96/24.30 | GROUND_INST: instantiating (dt_l1_pre_topc) with all_100_3, simplifying with % 173.96/24.30 | (39), (40) gives: % 173.96/24.30 | (44) l1_struct_0(all_100_3) % 173.96/24.30 | % 173.96/24.30 | GROUND_INST: instantiating (25) with all_100_3, all_100_2, simplifying with % 173.96/24.30 | (36), (38), (39), (40), (42) gives: % 173.96/24.30 | (45) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (k1_lopclset(all_100_3) = v2 % 173.96/24.30 | & k1_zfmisc_1(v0) = v1 & u1_struct_0(all_100_3) = v0 & $i(v2) & % 173.96/24.30 | $i(v1) & $i(v0) & m2_subset_1(all_100_2, v1, v2)) % 173.96/24.30 | % 173.96/24.30 | GROUND_INST: instantiating (22) with all_100_3, all_100_1, simplifying with % 173.96/24.30 | (36), (38), (39), (40), (43) gives: % 173.96/24.30 | (46) l3_lattices(all_100_1) % 173.96/24.30 | % 173.96/24.30 | GROUND_INST: instantiating (24) with all_100_3, all_100_1, simplifying with % 173.96/24.30 | (36), (38), (39), (40), (43) gives: % 173.96/24.30 | (47) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (k5_lopclset(all_100_3) = v2 % 173.96/24.30 | & k1_lopclset(all_100_3) = v0 & k4_lopclset(all_100_3) = v1 & % 173.96/24.30 | g3_lattices(v0, v1, v2) = all_100_1 & $i(v2) & $i(v1) & $i(v0) & % 173.96/24.30 | $i(all_100_1)) % 173.96/24.30 | % 173.96/24.30 | DELTA: instantiating (45) with fresh symbols all_116_0, all_116_1, all_116_2 % 173.96/24.30 | gives: % 173.96/24.31 | (48) k1_lopclset(all_100_3) = all_116_0 & k1_zfmisc_1(all_116_2) = % 173.96/24.31 | all_116_1 & u1_struct_0(all_100_3) = all_116_2 & $i(all_116_0) & % 173.96/24.31 | $i(all_116_1) & $i(all_116_2) & m2_subset_1(all_100_2, all_116_1, % 173.96/24.31 | all_116_0) % 173.96/24.31 | % 173.96/24.31 | ALPHA: (48) implies: % 173.96/24.31 | (49) m2_subset_1(all_100_2, all_116_1, all_116_0) % 173.96/24.31 | (50) u1_struct_0(all_100_3) = all_116_2 % 173.96/24.31 | (51) k1_zfmisc_1(all_116_2) = all_116_1 % 173.96/24.31 | (52) k1_lopclset(all_100_3) = all_116_0 % 173.96/24.31 | % 173.96/24.31 | DELTA: instantiating (47) with fresh symbols all_118_0, all_118_1, all_118_2 % 173.96/24.31 | gives: % 173.96/24.31 | (53) k5_lopclset(all_100_3) = all_118_0 & k1_lopclset(all_100_3) = % 173.96/24.31 | all_118_2 & k4_lopclset(all_100_3) = all_118_1 & % 173.96/24.31 | g3_lattices(all_118_2, all_118_1, all_118_0) = all_100_1 & % 173.96/24.31 | $i(all_118_0) & $i(all_118_1) & $i(all_118_2) & $i(all_100_1) % 173.96/24.31 | % 173.96/24.31 | ALPHA: (53) implies: % 173.96/24.31 | (54) $i(all_100_1) % 173.96/24.31 | (55) g3_lattices(all_118_2, all_118_1, all_118_0) = all_100_1 % 173.96/24.31 | (56) k4_lopclset(all_100_3) = all_118_1 % 173.96/24.31 | (57) k1_lopclset(all_100_3) = all_118_2 % 173.96/24.31 | (58) k5_lopclset(all_100_3) = all_118_0 % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (31) with all_116_0, all_118_2, all_100_3, % 173.96/24.31 | simplifying with (52), (57) gives: % 173.96/24.31 | (59) all_118_2 = all_116_0 % 173.96/24.31 | % 173.96/24.31 | REDUCE: (55), (59) imply: % 173.96/24.31 | (60) g3_lattices(all_116_0, all_118_1, all_118_0) = all_100_1 % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (14) with all_100_1, simplifying with (46), (54) % 173.96/24.31 | gives: % 173.96/24.31 | (61) l2_lattices(all_100_1) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (13) with all_100_1, simplifying with (46), (54) % 173.96/24.31 | gives: % 173.96/24.31 | (62) l1_lattices(all_100_1) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (15) with all_100_3, all_100_2, simplifying with % 173.96/24.31 | (40), (42), (44) gives: % 173.96/24.31 | (63) v1_xboole_0(all_100_2) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (21) with all_100_3, all_100_2, simplifying with % 173.96/24.31 | (40), (42), (44) gives: % 173.96/24.31 | (64) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(v0) = v1 & % 173.96/24.31 | u1_struct_0(all_100_3) = v0 & $i(v1) & $i(v0) & % 173.96/24.31 | m1_subset_1(all_100_2, v1)) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (20) with all_100_3, all_116_2, simplifying with % 173.96/24.31 | (40), (44), (50) gives: % 173.96/24.31 | (65) ? [v0: $i] : ? [v1: $i] : (k1_pre_topc(all_100_3) = v0 & % 173.96/24.31 | k1_zfmisc_1(all_116_2) = v1 & $i(v1) & $i(v0) & m1_subset_1(v0, v1)) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (18) with all_100_3, all_116_2, simplifying with % 173.96/24.31 | (36), (39), (40), (50) gives: % 173.96/24.31 | (66) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (k1_lopclset(all_100_3) = v0 % 173.96/24.31 | & k1_zfmisc_1(v1) = v2 & k1_zfmisc_1(all_116_2) = v1 & $i(v2) & % 173.96/24.31 | $i(v1) & $i(v0) & m1_subset_1(v0, v2)) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (9) with all_100_3, all_118_1, simplifying with % 173.96/24.31 | (36), (38), (39), (40), (56) gives: % 173.96/24.31 | (67) ? [v0: $i] : ? [v1: $i] : (k1_lopclset(all_100_3) = v0 & % 173.96/24.31 | k2_zfmisc_1(v0, v0) = v1 & $i(v1) & $i(v0) & m2_relset_1(all_118_1, % 173.96/24.31 | v1, v0) & v1_funct_2(all_118_1, v1, v0)) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (11) with all_100_3, all_116_0, simplifying with % 173.96/24.31 | (36), (38), (39), (40), (52) gives: % 173.96/24.31 | (68) ? [v0: $i] : ? [v1: $i] : (k5_lopclset(all_100_3) = v0 & % 173.96/24.31 | k2_zfmisc_1(all_116_0, all_116_0) = v1 & $i(v1) & $i(v0) & % 173.96/24.31 | m2_relset_1(v0, v1, all_116_0) & v1_funct_2(v0, v1, all_116_0) & % 173.96/24.31 | v1_funct_1(v0)) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (10) with all_100_3, all_116_0, simplifying with % 173.96/24.31 | (36), (38), (39), (40), (52) gives: % 173.96/24.31 | (69) ? [v0: $i] : ? [v1: $i] : (k4_lopclset(all_100_3) = v0 & % 173.96/24.31 | k2_zfmisc_1(all_116_0, all_116_0) = v1 & $i(v1) & $i(v0) & % 173.96/24.31 | m2_relset_1(v0, v1, all_116_0) & v1_funct_2(v0, v1, all_116_0) & % 173.96/24.31 | v1_funct_1(v0)) % 173.96/24.31 | % 173.96/24.31 | GROUND_INST: instantiating (19) with all_100_3, all_116_0, simplifying with % 173.96/24.31 | (36), (39), (40), (52) gives: % 173.96/24.32 | (70) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & % 173.96/24.32 | k1_zfmisc_1(v0) = v1 & u1_struct_0(all_100_3) = v0 & $i(v2) & $i(v1) % 173.96/24.32 | & $i(v0) & m1_subset_1(all_116_0, v2)) % 173.96/24.32 | % 173.96/24.32 | GROUND_INST: instantiating (12) with all_100_3, all_118_0, simplifying with % 173.96/24.32 | (36), (38), (39), (40), (58) gives: % 173.96/24.32 | (71) ? [v0: $i] : ? [v1: $i] : (k1_lopclset(all_100_3) = v0 & % 173.96/24.32 | k2_zfmisc_1(v0, v0) = v1 & $i(v1) & $i(v0) & m2_relset_1(all_118_0, % 173.96/24.32 | v1, v0) & v1_funct_2(all_118_0, v1, v0)) % 173.96/24.32 | % 173.96/24.32 | DELTA: instantiating (64) with fresh symbols all_130_0, all_130_1 gives: % 173.96/24.32 | (72) k1_zfmisc_1(all_130_1) = all_130_0 & u1_struct_0(all_100_3) = % 173.96/24.32 | all_130_1 & $i(all_130_0) & $i(all_130_1) & m1_subset_1(all_100_2, % 173.96/24.32 | all_130_0) % 173.96/24.32 | % 173.96/24.32 | ALPHA: (72) implies: % 173.96/24.32 | (73) m1_subset_1(all_100_2, all_130_0) % 173.96/24.32 | (74) $i(all_130_1) % 173.96/24.32 | (75) u1_struct_0(all_100_3) = all_130_1 % 173.96/24.32 | (76) k1_zfmisc_1(all_130_1) = all_130_0 % 173.96/24.32 | % 173.96/24.32 | DELTA: instantiating (65) with fresh symbols all_132_0, all_132_1 gives: % 173.96/24.32 | (77) k1_pre_topc(all_100_3) = all_132_1 & k1_zfmisc_1(all_116_2) = % 173.96/24.32 | all_132_0 & $i(all_132_0) & $i(all_132_1) & m1_subset_1(all_132_1, % 173.96/24.32 | all_132_0) % 173.96/24.32 | % 173.96/24.32 | ALPHA: (77) implies: % 173.96/24.32 | (78) $i(all_132_1) % 173.96/24.32 | (79) k1_pre_topc(all_100_3) = all_132_1 % 173.96/24.32 | % 173.96/24.32 | DELTA: instantiating (67) with fresh symbols all_140_0, all_140_1 gives: % 173.96/24.32 | (80) k1_lopclset(all_100_3) = all_140_1 & k2_zfmisc_1(all_140_1, all_140_1) % 173.96/24.32 | = all_140_0 & $i(all_140_0) & $i(all_140_1) & m2_relset_1(all_118_1, % 173.96/24.32 | all_140_0, all_140_1) & v1_funct_2(all_118_1, all_140_0, all_140_1) % 173.96/24.32 | % 173.96/24.32 | ALPHA: (80) implies: % 173.96/24.32 | (81) $i(all_140_1) % 173.96/24.32 | (82) k2_zfmisc_1(all_140_1, all_140_1) = all_140_0 % 173.96/24.32 | (83) k1_lopclset(all_100_3) = all_140_1 % 173.96/24.32 | % 173.96/24.32 | DELTA: instantiating (71) with fresh symbols all_142_0, all_142_1 gives: % 173.96/24.32 | (84) k1_lopclset(all_100_3) = all_142_1 & k2_zfmisc_1(all_142_1, all_142_1) % 173.96/24.32 | = all_142_0 & $i(all_142_0) & $i(all_142_1) & m2_relset_1(all_118_0, % 173.96/24.32 | all_142_0, all_142_1) & v1_funct_2(all_118_0, all_142_0, all_142_1) % 173.96/24.32 | % 173.96/24.32 | ALPHA: (84) implies: % 173.96/24.32 | (85) v1_funct_2(all_118_0, all_142_0, all_142_1) % 173.96/24.32 | (86) m2_relset_1(all_118_0, all_142_0, all_142_1) % 173.96/24.32 | (87) $i(all_142_0) % 173.96/24.32 | (88) k2_zfmisc_1(all_142_1, all_142_1) = all_142_0 % 173.96/24.32 | (89) k1_lopclset(all_100_3) = all_142_1 % 173.96/24.32 | % 173.96/24.32 | DELTA: instantiating (70) with fresh symbols all_144_0, all_144_1, all_144_2 % 173.96/24.32 | gives: % 173.96/24.32 | (90) k1_zfmisc_1(all_144_1) = all_144_0 & k1_zfmisc_1(all_144_2) = % 173.96/24.32 | all_144_1 & u1_struct_0(all_100_3) = all_144_2 & $i(all_144_0) & % 173.96/24.32 | $i(all_144_1) & $i(all_144_2) & m1_subset_1(all_116_0, all_144_0) % 173.96/24.32 | % 173.96/24.32 | ALPHA: (90) implies: % 173.96/24.32 | (91) m1_subset_1(all_116_0, all_144_0) % 173.96/24.32 | (92) $i(all_144_1) % 173.96/24.32 | (93) u1_struct_0(all_100_3) = all_144_2 % 173.96/24.32 | (94) k1_zfmisc_1(all_144_2) = all_144_1 % 173.96/24.32 | (95) k1_zfmisc_1(all_144_1) = all_144_0 % 173.96/24.32 | % 173.96/24.32 | DELTA: instantiating (69) with fresh symbols all_146_0, all_146_1 gives: % 173.96/24.32 | (96) k4_lopclset(all_100_3) = all_146_1 & k2_zfmisc_1(all_116_0, all_116_0) % 173.96/24.32 | = all_146_0 & $i(all_146_0) & $i(all_146_1) & m2_relset_1(all_146_1, % 173.96/24.32 | all_146_0, all_116_0) & v1_funct_2(all_146_1, all_146_0, all_116_0) % 173.96/24.32 | & v1_funct_1(all_146_1) % 173.96/24.32 | % 173.96/24.32 | ALPHA: (96) implies: % 173.96/24.32 | (97) v1_funct_1(all_146_1) % 173.96/24.32 | (98) v1_funct_2(all_146_1, all_146_0, all_116_0) % 173.96/24.32 | (99) m2_relset_1(all_146_1, all_146_0, all_116_0) % 173.96/24.32 | (100) $i(all_146_1) % 173.96/24.32 | (101) k2_zfmisc_1(all_116_0, all_116_0) = all_146_0 % 173.96/24.32 | (102) k4_lopclset(all_100_3) = all_146_1 % 173.96/24.32 | % 173.96/24.32 | DELTA: instantiating (66) with fresh symbols all_148_0, all_148_1, all_148_2 % 173.96/24.32 | gives: % 173.96/24.32 | (103) k1_lopclset(all_100_3) = all_148_2 & k1_zfmisc_1(all_148_1) = % 173.96/24.32 | all_148_0 & k1_zfmisc_1(all_116_2) = all_148_1 & $i(all_148_0) & % 173.96/24.32 | $i(all_148_1) & $i(all_148_2) & m1_subset_1(all_148_2, all_148_0) % 173.96/24.32 | % 173.96/24.32 | ALPHA: (103) implies: % 173.96/24.32 | (104) k1_lopclset(all_100_3) = all_148_2 % 173.96/24.32 | % 173.96/24.32 | DELTA: instantiating (68) with fresh symbols all_150_0, all_150_1 gives: % 173.96/24.32 | (105) k5_lopclset(all_100_3) = all_150_1 & k2_zfmisc_1(all_116_0, % 173.96/24.32 | all_116_0) = all_150_0 & $i(all_150_0) & $i(all_150_1) & % 173.96/24.32 | m2_relset_1(all_150_1, all_150_0, all_116_0) & v1_funct_2(all_150_1, % 173.96/24.32 | all_150_0, all_116_0) & v1_funct_1(all_150_1) % 173.96/24.32 | % 173.96/24.32 | ALPHA: (105) implies: % 173.96/24.32 | (106) v1_funct_1(all_150_1) % 173.96/24.32 | (107) $i(all_150_1) % 173.96/24.32 | (108) k2_zfmisc_1(all_116_0, all_116_0) = all_150_0 % 173.96/24.32 | (109) k5_lopclset(all_100_3) = all_150_1 % 173.96/24.32 | % 173.96/24.32 | GROUND_INST: instantiating (34) with all_146_0, all_150_0, all_116_0, % 173.96/24.32 | all_116_0, simplifying with (101), (108) gives: % 173.96/24.32 | (110) all_150_0 = all_146_0 % 173.96/24.32 | % 173.96/24.32 | GROUND_INST: instantiating (27) with all_116_2, all_144_2, all_100_3, % 173.96/24.32 | simplifying with (50), (93) gives: % 173.96/24.32 | (111) all_144_2 = all_116_2 % 173.96/24.32 | % 173.96/24.32 | GROUND_INST: instantiating (27) with all_130_1, all_144_2, all_100_3, % 173.96/24.32 | simplifying with (75), (93) gives: % 173.96/24.32 | (112) all_144_2 = all_130_1 % 173.96/24.32 | % 173.96/24.32 | GROUND_INST: instantiating (29) with all_116_1, all_144_1, all_116_2, % 173.96/24.32 | simplifying with (51) gives: % 173.96/24.33 | (113) all_144_1 = all_116_1 | ~ (k1_zfmisc_1(all_116_2) = all_144_1) % 173.96/24.33 | % 173.96/24.33 | GROUND_INST: instantiating (29) with all_130_0, all_144_1, all_130_1, % 173.96/24.33 | simplifying with (76) gives: % 173.96/24.33 | (114) all_144_1 = all_130_0 | ~ (k1_zfmisc_1(all_130_1) = all_144_1) % 173.96/24.33 | % 173.96/24.33 | GROUND_INST: instantiating (30) with all_118_1, all_146_1, all_100_3, % 173.96/24.33 | simplifying with (56), (102) gives: % 173.96/24.33 | (115) all_146_1 = all_118_1 % 173.96/24.33 | % 173.96/24.33 | GROUND_INST: instantiating (31) with all_116_0, all_142_1, all_100_3, % 173.96/24.33 | simplifying with (52), (89) gives: % 173.96/24.33 | (116) all_142_1 = all_116_0 % 173.96/24.33 | % 173.96/24.33 | GROUND_INST: instantiating (31) with all_142_1, all_148_2, all_100_3, % 173.96/24.33 | simplifying with (89), (104) gives: % 173.96/24.33 | (117) all_148_2 = all_142_1 % 173.96/24.33 | % 173.96/24.33 | GROUND_INST: instantiating (31) with all_140_1, all_148_2, all_100_3, % 173.96/24.33 | simplifying with (83), (104) gives: % 173.96/24.33 | (118) all_148_2 = all_140_1 % 173.96/24.33 | % 173.96/24.33 | GROUND_INST: instantiating (32) with all_118_0, all_150_1, all_100_3, % 173.96/24.33 | simplifying with (58), (109) gives: % 173.96/24.33 | (119) all_150_1 = all_118_0 % 173.96/24.33 | % 173.96/24.33 | GROUND_INST: instantiating (33) with all_100_2, all_132_1, all_100_3, % 173.96/24.33 | simplifying with (42), (79) gives: % 173.96/24.33 | (120) all_132_1 = all_100_2 % 173.96/24.33 | % 173.96/24.33 | COMBINE_EQS: (117), (118) imply: % 173.96/24.33 | (121) all_142_1 = all_140_1 % 173.96/24.33 | % 173.96/24.33 | SIMP: (121) implies: % 173.96/24.33 | (122) all_142_1 = all_140_1 % 173.96/24.33 | % 173.96/24.33 | COMBINE_EQS: (111), (112) imply: % 173.96/24.33 | (123) all_130_1 = all_116_2 % 173.96/24.33 | % 173.96/24.33 | COMBINE_EQS: (116), (122) imply: % 173.96/24.33 | (124) all_140_1 = all_116_0 % 173.96/24.33 | % 173.96/24.33 | REDUCE: (94), (111) imply: % 173.96/24.33 | (125) k1_zfmisc_1(all_116_2) = all_144_1 % 173.96/24.33 | % 173.96/24.33 | REDUCE: (88), (116) imply: % 173.96/24.33 | (126) k2_zfmisc_1(all_116_0, all_116_0) = all_142_0 % 173.96/24.33 | % 173.96/24.33 | REDUCE: (82), (124) imply: % 173.96/24.33 | (127) k2_zfmisc_1(all_116_0, all_116_0) = all_140_0 % 173.96/24.33 | % 173.96/24.33 | REDUCE: (107), (119) imply: % 173.96/24.33 | (128) $i(all_118_0) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (100), (115) imply: % 173.96/24.33 | (129) $i(all_118_1) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (81), (124) imply: % 173.96/24.33 | (130) $i(all_116_0) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (78), (120) imply: % 173.96/24.33 | (131) $i(all_100_2) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (74), (123) imply: % 173.96/24.33 | (132) $i(all_116_2) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (99), (115) imply: % 173.96/24.33 | (133) m2_relset_1(all_118_1, all_146_0, all_116_0) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (86), (116) imply: % 173.96/24.33 | (134) m2_relset_1(all_118_0, all_142_0, all_116_0) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (98), (115) imply: % 173.96/24.33 | (135) v1_funct_2(all_118_1, all_146_0, all_116_0) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (85), (116) imply: % 173.96/24.33 | (136) v1_funct_2(all_118_0, all_142_0, all_116_0) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (106), (119) imply: % 173.96/24.33 | (137) v1_funct_1(all_118_0) % 173.96/24.33 | % 173.96/24.33 | REDUCE: (97), (115) imply: % 173.96/24.33 | (138) v1_funct_1(all_118_1) % 173.96/24.33 | % 173.96/24.33 | BETA: splitting (114) gives: % 173.96/24.33 | % 173.96/24.33 | Case 1: % 173.96/24.33 | | % 173.96/24.33 | | (139) ~ (k1_zfmisc_1(all_130_1) = all_144_1) % 173.96/24.33 | | % 173.96/24.33 | | REDUCE: (123), (139) imply: % 173.96/24.33 | | (140) ~ (k1_zfmisc_1(all_116_2) = all_144_1) % 173.96/24.33 | | % 173.96/24.33 | | PRED_UNIFY: (125), (140) imply: % 173.96/24.33 | | (141) $false % 173.96/24.33 | | % 173.96/24.33 | | CLOSE: (141) is inconsistent. % 173.96/24.33 | | % 173.96/24.33 | Case 2: % 173.96/24.33 | | % 173.96/24.33 | | (142) all_144_1 = all_130_0 % 173.96/24.33 | | % 173.96/24.33 | | REDUCE: (95), (142) imply: % 173.96/24.33 | | (143) k1_zfmisc_1(all_130_0) = all_144_0 % 173.96/24.33 | | % 173.96/24.33 | | REDUCE: (125), (142) imply: % 173.96/24.33 | | (144) k1_zfmisc_1(all_116_2) = all_130_0 % 173.96/24.33 | | % 173.96/24.33 | | REDUCE: (92), (142) imply: % 173.96/24.33 | | (145) $i(all_130_0) % 173.96/24.33 | | % 173.96/24.33 | | BETA: splitting (113) gives: % 173.96/24.33 | | % 173.96/24.33 | | Case 1: % 173.96/24.33 | | | % 173.96/24.33 | | | (146) ~ (k1_zfmisc_1(all_116_2) = all_144_1) % 173.96/24.33 | | | % 173.96/24.33 | | | PRED_UNIFY: (125), (146) imply: % 173.96/24.34 | | | (147) $false % 173.96/24.34 | | | % 173.96/24.34 | | | CLOSE: (147) is inconsistent. % 173.96/24.34 | | | % 173.96/24.34 | | Case 2: % 173.96/24.34 | | | % 173.96/24.34 | | | (148) all_144_1 = all_116_1 % 173.96/24.34 | | | % 173.96/24.34 | | | COMBINE_EQS: (142), (148) imply: % 173.96/24.34 | | | (149) all_130_0 = all_116_1 % 173.96/24.34 | | | % 173.96/24.34 | | | SIMP: (149) implies: % 173.96/24.34 | | | (150) all_130_0 = all_116_1 % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (143), (150) imply: % 173.96/24.34 | | | (151) k1_zfmisc_1(all_116_1) = all_144_0 % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (145), (150) imply: % 173.96/24.34 | | | (152) $i(all_116_1) % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (73), (150) imply: % 173.96/24.34 | | | (153) m1_subset_1(all_100_2, all_116_1) % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (34) with all_146_0, all_140_0, all_116_0, % 173.96/24.34 | | | all_116_0, simplifying with (101), (127) gives: % 173.96/24.34 | | | (154) all_146_0 = all_140_0 % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (34) with all_146_0, all_142_0, all_116_0, % 173.96/24.34 | | | all_116_0, simplifying with (101), (126) gives: % 173.96/24.34 | | | (155) all_146_0 = all_142_0 % 173.96/24.34 | | | % 173.96/24.34 | | | COMBINE_EQS: (154), (155) imply: % 173.96/24.34 | | | (156) all_142_0 = all_140_0 % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (87), (156) imply: % 173.96/24.34 | | | (157) $i(all_140_0) % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (134), (156) imply: % 173.96/24.34 | | | (158) m2_relset_1(all_118_0, all_140_0, all_116_0) % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (133), (154) imply: % 173.96/24.34 | | | (159) m2_relset_1(all_118_1, all_140_0, all_116_0) % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (136), (156) imply: % 173.96/24.34 | | | (160) v1_funct_2(all_118_0, all_140_0, all_116_0) % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (135), (154) imply: % 173.96/24.34 | | | (161) v1_funct_2(all_118_1, all_140_0, all_116_0) % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (t2_subset) with all_100_2, all_116_1, % 173.96/24.34 | | | simplifying with (131), (152), (153) gives: % 173.96/24.34 | | | (162) v1_xboole_0(all_116_1) | r2_hidden(all_100_2, all_116_1) % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (1) with all_100_1, all_100_0, simplifying with % 173.96/24.34 | | | (41), (54), (62) gives: % 173.96/24.34 | | | (163) ? [v0: $i] : ? [v1: $i] : (u1_lattices(all_100_1) = v0 & % 173.96/24.34 | | | k2_zfmisc_1(all_100_0, all_100_0) = v1 & $i(v1) & $i(v0) & % 173.96/24.34 | | | m2_relset_1(v0, v1, all_100_0) & v1_funct_2(v0, v1, all_100_0) % 173.96/24.34 | | | & v1_funct_1(v0)) % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (8) with all_116_0, all_118_1, all_118_0, % 173.96/24.34 | | | all_100_1, simplifying with (60), (128), (129), (130), (137), % 173.96/24.34 | | | (138) gives: % 173.96/24.34 | | | (164) v3_lattices(all_100_1) | ? [v0: $i] : (k2_zfmisc_1(all_116_0, % 173.96/24.34 | | | all_116_0) = v0 & $i(v0) & ( ~ m1_relset_1(all_118_0, v0, % 173.96/24.34 | | | all_116_0) | ~ m1_relset_1(all_118_1, v0, all_116_0) | ~ % 173.96/24.34 | | | v1_funct_2(all_118_0, v0, all_116_0) | ~ % 173.96/24.34 | | | v1_funct_2(all_118_1, v0, all_116_0))) % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (6) with all_140_0, all_116_0, all_118_1, % 173.96/24.34 | | | simplifying with (129), (130), (157), (159) gives: % 173.96/24.34 | | | (165) m1_relset_1(all_118_1, all_140_0, all_116_0) % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (6) with all_140_0, all_116_0, all_118_0, % 173.96/24.34 | | | simplifying with (128), (130), (157), (158) gives: % 173.96/24.34 | | | (166) m1_relset_1(all_118_0, all_140_0, all_116_0) % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (2) with all_100_1, all_100_0, simplifying with % 173.96/24.34 | | | (41), (54), (61) gives: % 173.96/24.34 | | | (167) ? [v0: $i] : ? [v1: $i] : (u2_lattices(all_100_1) = v0 & % 173.96/24.34 | | | k2_zfmisc_1(all_100_0, all_100_0) = v1 & $i(v1) & $i(v0) & % 173.96/24.34 | | | m2_relset_1(v0, v1, all_100_0) & v1_funct_2(v0, v1, all_100_0) % 173.96/24.34 | | | & v1_funct_1(v0)) % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (16) with all_100_2, simplifying with (63), % 173.96/24.34 | | | (131) gives: % 173.96/24.34 | | | (168) all_100_2 = k1_xboole_0 % 173.96/24.34 | | | % 173.96/24.34 | | | GROUND_INST: instantiating (17) with all_116_1, all_116_0, all_144_0, % 173.96/24.34 | | | all_100_2, simplifying with (49), (91), (130), (131), (151), % 173.96/24.34 | | | (152) gives: % 173.96/24.34 | | | (169) v1_xboole_0(all_116_0) | v1_xboole_0(all_116_1) | % 173.96/24.34 | | | m1_subset_1(all_100_2, all_116_0) % 173.96/24.34 | | | % 173.96/24.34 | | | DELTA: instantiating (163) with fresh symbols all_178_0, all_178_1 gives: % 173.96/24.34 | | | (170) u1_lattices(all_100_1) = all_178_1 & k2_zfmisc_1(all_100_0, % 173.96/24.34 | | | all_100_0) = all_178_0 & $i(all_178_0) & $i(all_178_1) & % 173.96/24.34 | | | m2_relset_1(all_178_1, all_178_0, all_100_0) & % 173.96/24.34 | | | v1_funct_2(all_178_1, all_178_0, all_100_0) & % 173.96/24.34 | | | v1_funct_1(all_178_1) % 173.96/24.34 | | | % 173.96/24.34 | | | ALPHA: (170) implies: % 173.96/24.34 | | | (171) v1_funct_1(all_178_1) % 173.96/24.34 | | | (172) u1_lattices(all_100_1) = all_178_1 % 173.96/24.34 | | | % 173.96/24.34 | | | DELTA: instantiating (167) with fresh symbols all_180_0, all_180_1 gives: % 173.96/24.34 | | | (173) u2_lattices(all_100_1) = all_180_1 & k2_zfmisc_1(all_100_0, % 173.96/24.34 | | | all_100_0) = all_180_0 & $i(all_180_0) & $i(all_180_1) & % 173.96/24.34 | | | m2_relset_1(all_180_1, all_180_0, all_100_0) & % 173.96/24.34 | | | v1_funct_2(all_180_1, all_180_0, all_100_0) & % 173.96/24.34 | | | v1_funct_1(all_180_1) % 173.96/24.34 | | | % 173.96/24.34 | | | ALPHA: (173) implies: % 173.96/24.34 | | | (174) v1_funct_1(all_180_1) % 173.96/24.34 | | | (175) u2_lattices(all_100_1) = all_180_1 % 173.96/24.34 | | | % 173.96/24.34 | | | REDUCE: (37), (168) imply: % 173.96/24.34 | | | (176) ~ m1_subset_1(k1_xboole_0, all_100_0) % 173.96/24.34 | | | % 173.96/24.34 | | | BETA: splitting (164) gives: % 173.96/24.34 | | | % 173.96/24.34 | | | Case 1: % 173.96/24.34 | | | | % 173.96/24.34 | | | | (177) v3_lattices(all_100_1) % 173.96/24.34 | | | | % 173.96/24.34 | | | | GROUND_INST: instantiating (4) with all_100_1, all_100_0, simplifying % 173.96/24.34 | | | | with (41), (46), (54), (177) gives: % 173.96/24.34 | | | | (178) ? [v0: $i] : ? [v1: $i] : (g3_lattices(all_100_0, v0, v1) = % 173.96/24.34 | | | | all_100_1 & u2_lattices(all_100_1) = v0 & % 173.96/24.34 | | | | u1_lattices(all_100_1) = v1 & $i(v1) & $i(v0)) % 173.96/24.34 | | | | % 173.96/24.34 | | | | GROUND_INST: instantiating (3) with all_100_1, all_178_1, simplifying % 173.96/24.34 | | | | with (46), (54), (172), (177) gives: % 173.96/24.35 | | | | (179) ? [v0: $i] : ? [v1: $i] : (g3_lattices(v0, v1, all_178_1) = % 173.96/24.35 | | | | all_100_1 & u2_lattices(all_100_1) = v1 & % 173.96/24.35 | | | | u1_struct_0(all_100_1) = v0 & $i(v1) & $i(v0)) % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (5) with all_100_1, all_180_1, simplifying % 173.96/24.35 | | | | with (46), (54), (175), (177) gives: % 173.96/24.35 | | | | (180) ? [v0: $i] : ? [v1: $i] : (g3_lattices(v0, all_180_1, v1) = % 173.96/24.35 | | | | all_100_1 & u1_struct_0(all_100_1) = v0 & % 173.96/24.35 | | | | u1_lattices(all_100_1) = v1 & $i(v1) & $i(v0)) % 173.96/24.35 | | | | % 173.96/24.35 | | | | DELTA: instantiating (178) with fresh symbols all_208_0, all_208_1 % 173.96/24.35 | | | | gives: % 173.96/24.35 | | | | (181) g3_lattices(all_100_0, all_208_1, all_208_0) = all_100_1 & % 173.96/24.35 | | | | u2_lattices(all_100_1) = all_208_1 & u1_lattices(all_100_1) = % 173.96/24.35 | | | | all_208_0 & $i(all_208_0) & $i(all_208_1) % 173.96/24.35 | | | | % 173.96/24.35 | | | | ALPHA: (181) implies: % 173.96/24.35 | | | | (182) $i(all_208_1) % 173.96/24.35 | | | | (183) $i(all_208_0) % 173.96/24.35 | | | | (184) u1_lattices(all_100_1) = all_208_0 % 173.96/24.35 | | | | (185) u2_lattices(all_100_1) = all_208_1 % 173.96/24.35 | | | | (186) g3_lattices(all_100_0, all_208_1, all_208_0) = all_100_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | DELTA: instantiating (180) with fresh symbols all_210_0, all_210_1 % 173.96/24.35 | | | | gives: % 173.96/24.35 | | | | (187) g3_lattices(all_210_1, all_180_1, all_210_0) = all_100_1 & % 173.96/24.35 | | | | u1_struct_0(all_100_1) = all_210_1 & u1_lattices(all_100_1) = % 173.96/24.35 | | | | all_210_0 & $i(all_210_0) & $i(all_210_1) % 173.96/24.35 | | | | % 173.96/24.35 | | | | ALPHA: (187) implies: % 173.96/24.35 | | | | (188) $i(all_210_1) % 173.96/24.35 | | | | (189) u1_lattices(all_100_1) = all_210_0 % 173.96/24.35 | | | | (190) u1_struct_0(all_100_1) = all_210_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | DELTA: instantiating (179) with fresh symbols all_212_0, all_212_1 % 173.96/24.35 | | | | gives: % 173.96/24.35 | | | | (191) g3_lattices(all_212_1, all_212_0, all_178_1) = all_100_1 & % 173.96/24.35 | | | | u2_lattices(all_100_1) = all_212_0 & u1_struct_0(all_100_1) = % 173.96/24.35 | | | | all_212_1 & $i(all_212_0) & $i(all_212_1) % 173.96/24.35 | | | | % 173.96/24.35 | | | | ALPHA: (191) implies: % 173.96/24.35 | | | | (192) u1_struct_0(all_100_1) = all_212_1 % 173.96/24.35 | | | | (193) u2_lattices(all_100_1) = all_212_0 % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (26) with all_178_1, all_210_0, all_100_1, % 173.96/24.35 | | | | simplifying with (172), (189) gives: % 173.96/24.35 | | | | (194) all_210_0 = all_178_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (26) with all_208_0, all_210_0, all_100_1, % 173.96/24.35 | | | | simplifying with (184), (189) gives: % 173.96/24.35 | | | | (195) all_210_0 = all_208_0 % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (27) with all_100_0, all_212_1, all_100_1, % 173.96/24.35 | | | | simplifying with (41), (192) gives: % 173.96/24.35 | | | | (196) all_212_1 = all_100_0 % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (27) with all_210_1, all_212_1, all_100_1, % 173.96/24.35 | | | | simplifying with (190), (192) gives: % 173.96/24.35 | | | | (197) all_212_1 = all_210_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (28) with all_180_1, all_212_0, all_100_1, % 173.96/24.35 | | | | simplifying with (175), (193) gives: % 173.96/24.35 | | | | (198) all_212_0 = all_180_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (28) with all_208_1, all_212_0, all_100_1, % 173.96/24.35 | | | | simplifying with (185), (193) gives: % 173.96/24.35 | | | | (199) all_212_0 = all_208_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | COMBINE_EQS: (198), (199) imply: % 173.96/24.35 | | | | (200) all_208_1 = all_180_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | COMBINE_EQS: (196), (197) imply: % 173.96/24.35 | | | | (201) all_210_1 = all_100_0 % 173.96/24.35 | | | | % 173.96/24.35 | | | | SIMP: (201) implies: % 173.96/24.35 | | | | (202) all_210_1 = all_100_0 % 173.96/24.35 | | | | % 173.96/24.35 | | | | COMBINE_EQS: (194), (195) imply: % 173.96/24.35 | | | | (203) all_208_0 = all_178_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | SIMP: (203) implies: % 173.96/24.35 | | | | (204) all_208_0 = all_178_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | REDUCE: (186), (200), (204) imply: % 173.96/24.35 | | | | (205) g3_lattices(all_100_0, all_180_1, all_178_1) = all_100_1 % 173.96/24.35 | | | | % 173.96/24.35 | | | | REDUCE: (188), (202) imply: % 173.96/24.35 | | | | (206) $i(all_100_0) % 173.96/24.35 | | | | % 173.96/24.35 | | | | REDUCE: (183), (204) imply: % 173.96/24.35 | | | | (207) $i(all_178_1) % 173.96/24.35 | | | | % 173.96/24.35 | | | | REDUCE: (182), (200) imply: % 173.96/24.35 | | | | (208) $i(all_180_1) % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (7) with all_100_0, all_180_1, all_178_1, % 173.96/24.35 | | | | all_100_1, all_116_0, all_118_1, all_118_0, simplifying % 173.96/24.35 | | | | with (60), (128), (129), (130), (171), (174), (205), (206), % 173.96/24.35 | | | | (207), (208) gives: % 173.96/24.35 | | | | (209) all_116_0 = all_100_0 | ? [v0: $i] : (k2_zfmisc_1(all_100_0, % 173.96/24.35 | | | | all_100_0) = v0 & $i(v0) & ( ~ m1_relset_1(all_180_1, v0, % 173.96/24.35 | | | | all_100_0) | ~ m1_relset_1(all_178_1, v0, all_100_0) | % 173.96/24.35 | | | | ~ v1_funct_2(all_180_1, v0, all_100_0) | ~ % 173.96/24.35 | | | | v1_funct_2(all_178_1, v0, all_100_0))) % 173.96/24.35 | | | | % 173.96/24.35 | | | | GROUND_INST: instantiating (7) with all_116_0, all_118_1, all_118_0, % 173.96/24.35 | | | | all_100_1, all_100_0, all_180_1, all_178_1, simplifying % 173.96/24.35 | | | | with (60), (128), (129), (130), (137), (138), (205), (206), % 173.96/24.35 | | | | (207), (208) gives: % 173.96/24.35 | | | | (210) all_116_0 = all_100_0 | ? [v0: $i] : (k2_zfmisc_1(all_116_0, % 173.96/24.35 | | | | all_116_0) = v0 & $i(v0) & ( ~ m1_relset_1(all_118_0, v0, % 173.96/24.35 | | | | all_116_0) | ~ m1_relset_1(all_118_1, v0, all_116_0) | % 173.96/24.35 | | | | ~ v1_funct_2(all_118_0, v0, all_116_0) | ~ % 173.96/24.35 | | | | v1_funct_2(all_118_1, v0, all_116_0))) % 173.96/24.35 | | | | % 173.96/24.35 | | | | BETA: splitting (209) gives: % 173.96/24.35 | | | | % 173.96/24.35 | | | | Case 1: % 173.96/24.35 | | | | | % 173.96/24.35 | | | | | (211) all_116_0 = all_100_0 % 173.96/24.35 | | | | | % 173.96/24.35 | | | | | REDUCE: (52), (211) imply: % 173.96/24.35 | | | | | (212) k1_lopclset(all_100_3) = all_100_0 % 173.96/24.35 | | | | | % 173.96/24.35 | | | | | BETA: splitting (162) gives: % 173.96/24.35 | | | | | % 173.96/24.35 | | | | | Case 1: % 173.96/24.35 | | | | | | % 173.96/24.35 | | | | | | (213) v1_xboole_0(all_116_1) % 173.96/24.35 | | | | | | % 173.96/24.35 | | | | | | GROUND_INST: instantiating (23) with all_116_2, all_116_1, % 173.96/24.35 | | | | | | simplifying with (51), (132), (213) gives: % 173.96/24.35 | | | | | | (214) $false % 173.96/24.35 | | | | | | % 173.96/24.35 | | | | | | CLOSE: (214) is inconsistent. % 173.96/24.35 | | | | | | % 173.96/24.35 | | | | | Case 2: % 173.96/24.35 | | | | | | % 173.96/24.35 | | | | | | (215) ~ v1_xboole_0(all_116_1) % 173.96/24.35 | | | | | | % 173.96/24.35 | | | | | | BETA: splitting (169) gives: % 173.96/24.35 | | | | | | % 173.96/24.35 | | | | | | Case 1: % 173.96/24.35 | | | | | | | % 173.96/24.35 | | | | | | | (216) v1_xboole_0(all_116_0) % 173.96/24.35 | | | | | | | % 173.96/24.35 | | | | | | | REDUCE: (211), (216) imply: % 173.96/24.35 | | | | | | | (217) v1_xboole_0(all_100_0) % 173.96/24.35 | | | | | | | % 173.96/24.35 | | | | | | | GROUND_INST: instantiating (fc1_lopclset) with all_100_3, % 173.96/24.35 | | | | | | | all_100_0, simplifying with (36), (38), (39), (40), % 173.96/24.35 | | | | | | | (212), (217) gives: % 173.96/24.35 | | | | | | | (218) $false % 173.96/24.35 | | | | | | | % 173.96/24.35 | | | | | | | CLOSE: (218) is inconsistent. % 173.96/24.35 | | | | | | | % 173.96/24.35 | | | | | | Case 2: % 173.96/24.35 | | | | | | | % 173.96/24.35 | | | | | | | (219) v1_xboole_0(all_116_1) | m1_subset_1(all_100_2, % 173.96/24.35 | | | | | | | all_116_0) % 173.96/24.35 | | | | | | | % 173.96/24.35 | | | | | | | BETA: splitting (219) gives: % 173.96/24.35 | | | | | | | % 173.96/24.35 | | | | | | | Case 1: % 173.96/24.35 | | | | | | | | % 173.96/24.35 | | | | | | | | (220) v1_xboole_0(all_116_1) % 173.96/24.35 | | | | | | | | % 173.96/24.35 | | | | | | | | PRED_UNIFY: (215), (220) imply: % 173.96/24.35 | | | | | | | | (221) $false % 173.96/24.35 | | | | | | | | % 173.96/24.35 | | | | | | | | CLOSE: (221) is inconsistent. % 173.96/24.35 | | | | | | | | % 173.96/24.35 | | | | | | | Case 2: % 173.96/24.35 | | | | | | | | % 173.96/24.35 | | | | | | | | (222) m1_subset_1(all_100_2, all_116_0) % 173.96/24.35 | | | | | | | | % 173.96/24.36 | | | | | | | | REDUCE: (168), (211), (222) imply: % 173.96/24.36 | | | | | | | | (223) m1_subset_1(k1_xboole_0, all_100_0) % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | PRED_UNIFY: (176), (223) imply: % 173.96/24.36 | | | | | | | | (224) $false % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | CLOSE: (224) is inconsistent. % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | End of split % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | End of split % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | End of split % 173.96/24.36 | | | | | % 173.96/24.36 | | | | Case 2: % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | (225) ~ (all_116_0 = all_100_0) % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | BETA: splitting (210) gives: % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | Case 1: % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | (226) all_116_0 = all_100_0 % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | REDUCE: (225), (226) imply: % 173.96/24.36 | | | | | | (227) $false % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | CLOSE: (227) is inconsistent. % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | Case 2: % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | (228) ? [v0: $i] : (k2_zfmisc_1(all_116_0, all_116_0) = v0 & % 173.96/24.36 | | | | | | $i(v0) & ( ~ m1_relset_1(all_118_0, v0, all_116_0) | ~ % 173.96/24.36 | | | | | | m1_relset_1(all_118_1, v0, all_116_0) | ~ % 173.96/24.36 | | | | | | v1_funct_2(all_118_0, v0, all_116_0) | ~ % 173.96/24.36 | | | | | | v1_funct_2(all_118_1, v0, all_116_0))) % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | DELTA: instantiating (228) with fresh symbol all_296_0 gives: % 173.96/24.36 | | | | | | (229) k2_zfmisc_1(all_116_0, all_116_0) = all_296_0 & % 173.96/24.36 | | | | | | $i(all_296_0) & ( ~ m1_relset_1(all_118_0, all_296_0, % 173.96/24.36 | | | | | | all_116_0) | ~ m1_relset_1(all_118_1, all_296_0, % 173.96/24.36 | | | | | | all_116_0) | ~ v1_funct_2(all_118_0, all_296_0, % 173.96/24.36 | | | | | | all_116_0) | ~ v1_funct_2(all_118_1, all_296_0, % 173.96/24.36 | | | | | | all_116_0)) % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | ALPHA: (229) implies: % 173.96/24.36 | | | | | | (230) k2_zfmisc_1(all_116_0, all_116_0) = all_296_0 % 173.96/24.36 | | | | | | (231) ~ m1_relset_1(all_118_0, all_296_0, all_116_0) | ~ % 173.96/24.36 | | | | | | m1_relset_1(all_118_1, all_296_0, all_116_0) | ~ % 173.96/24.36 | | | | | | v1_funct_2(all_118_0, all_296_0, all_116_0) | ~ % 173.96/24.36 | | | | | | v1_funct_2(all_118_1, all_296_0, all_116_0) % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | GROUND_INST: instantiating (34) with all_140_0, all_296_0, % 173.96/24.36 | | | | | | all_116_0, all_116_0, simplifying with (127), (230) % 173.96/24.36 | | | | | | gives: % 173.96/24.36 | | | | | | (232) all_296_0 = all_140_0 % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | BETA: splitting (231) gives: % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | Case 1: % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | (233) ~ m1_relset_1(all_118_0, all_296_0, all_116_0) % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | REDUCE: (232), (233) imply: % 173.96/24.36 | | | | | | | (234) ~ m1_relset_1(all_118_0, all_140_0, all_116_0) % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | PRED_UNIFY: (166), (234) imply: % 173.96/24.36 | | | | | | | (235) $false % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | CLOSE: (235) is inconsistent. % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | Case 2: % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | (236) ~ m1_relset_1(all_118_1, all_296_0, all_116_0) | ~ % 173.96/24.36 | | | | | | | v1_funct_2(all_118_0, all_296_0, all_116_0) | ~ % 173.96/24.36 | | | | | | | v1_funct_2(all_118_1, all_296_0, all_116_0) % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | BETA: splitting (236) gives: % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | Case 1: % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | (237) ~ m1_relset_1(all_118_1, all_296_0, all_116_0) % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | REDUCE: (232), (237) imply: % 173.96/24.36 | | | | | | | | (238) ~ m1_relset_1(all_118_1, all_140_0, all_116_0) % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | PRED_UNIFY: (165), (238) imply: % 173.96/24.36 | | | | | | | | (239) $false % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | CLOSE: (239) is inconsistent. % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | Case 2: % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | (240) ~ v1_funct_2(all_118_0, all_296_0, all_116_0) | ~ % 173.96/24.36 | | | | | | | | v1_funct_2(all_118_1, all_296_0, all_116_0) % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | BETA: splitting (240) gives: % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | | Case 1: % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | | (241) ~ v1_funct_2(all_118_0, all_296_0, all_116_0) % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | | REDUCE: (232), (241) imply: % 173.96/24.36 | | | | | | | | | (242) ~ v1_funct_2(all_118_0, all_140_0, all_116_0) % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | | PRED_UNIFY: (160), (242) imply: % 173.96/24.36 | | | | | | | | | (243) $false % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | | CLOSE: (243) is inconsistent. % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | Case 2: % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | | (244) ~ v1_funct_2(all_118_1, all_296_0, all_116_0) % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | | REDUCE: (232), (244) imply: % 173.96/24.36 | | | | | | | | | (245) ~ v1_funct_2(all_118_1, all_140_0, all_116_0) % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | | PRED_UNIFY: (161), (245) imply: % 173.96/24.36 | | | | | | | | | (246) $false % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | | CLOSE: (246) is inconsistent. % 173.96/24.36 | | | | | | | | | % 173.96/24.36 | | | | | | | | End of split % 173.96/24.36 | | | | | | | | % 173.96/24.36 | | | | | | | End of split % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | End of split % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | End of split % 173.96/24.36 | | | | | % 173.96/24.36 | | | | End of split % 173.96/24.36 | | | | % 173.96/24.36 | | | Case 2: % 173.96/24.36 | | | | % 173.96/24.36 | | | | (247) ? [v0: $i] : (k2_zfmisc_1(all_116_0, all_116_0) = v0 & $i(v0) % 173.96/24.36 | | | | & ( ~ m1_relset_1(all_118_0, v0, all_116_0) | ~ % 173.96/24.36 | | | | m1_relset_1(all_118_1, v0, all_116_0) | ~ % 173.96/24.36 | | | | v1_funct_2(all_118_0, v0, all_116_0) | ~ % 173.96/24.36 | | | | v1_funct_2(all_118_1, v0, all_116_0))) % 173.96/24.36 | | | | % 173.96/24.36 | | | | DELTA: instantiating (247) with fresh symbol all_186_0 gives: % 173.96/24.36 | | | | (248) k2_zfmisc_1(all_116_0, all_116_0) = all_186_0 & $i(all_186_0) & % 173.96/24.36 | | | | ( ~ m1_relset_1(all_118_0, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | m1_relset_1(all_118_1, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | v1_funct_2(all_118_0, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | v1_funct_2(all_118_1, all_186_0, all_116_0)) % 173.96/24.36 | | | | % 173.96/24.36 | | | | ALPHA: (248) implies: % 173.96/24.36 | | | | (249) k2_zfmisc_1(all_116_0, all_116_0) = all_186_0 % 173.96/24.36 | | | | (250) ~ m1_relset_1(all_118_0, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | m1_relset_1(all_118_1, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | v1_funct_2(all_118_0, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | v1_funct_2(all_118_1, all_186_0, all_116_0) % 173.96/24.36 | | | | % 173.96/24.36 | | | | GROUND_INST: instantiating (34) with all_140_0, all_186_0, all_116_0, % 173.96/24.36 | | | | all_116_0, simplifying with (127), (249) gives: % 173.96/24.36 | | | | (251) all_186_0 = all_140_0 % 173.96/24.36 | | | | % 173.96/24.36 | | | | BETA: splitting (250) gives: % 173.96/24.36 | | | | % 173.96/24.36 | | | | Case 1: % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | (252) ~ m1_relset_1(all_118_0, all_186_0, all_116_0) % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | REDUCE: (251), (252) imply: % 173.96/24.36 | | | | | (253) ~ m1_relset_1(all_118_0, all_140_0, all_116_0) % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | PRED_UNIFY: (166), (253) imply: % 173.96/24.36 | | | | | (254) $false % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | CLOSE: (254) is inconsistent. % 173.96/24.36 | | | | | % 173.96/24.36 | | | | Case 2: % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | (255) ~ m1_relset_1(all_118_1, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | | v1_funct_2(all_118_0, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | | v1_funct_2(all_118_1, all_186_0, all_116_0) % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | BETA: splitting (255) gives: % 173.96/24.36 | | | | | % 173.96/24.36 | | | | | Case 1: % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | (256) ~ m1_relset_1(all_118_1, all_186_0, all_116_0) % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | REDUCE: (251), (256) imply: % 173.96/24.36 | | | | | | (257) ~ m1_relset_1(all_118_1, all_140_0, all_116_0) % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | PRED_UNIFY: (165), (257) imply: % 173.96/24.36 | | | | | | (258) $false % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | CLOSE: (258) is inconsistent. % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | Case 2: % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | (259) ~ v1_funct_2(all_118_0, all_186_0, all_116_0) | ~ % 173.96/24.36 | | | | | | v1_funct_2(all_118_1, all_186_0, all_116_0) % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | BETA: splitting (259) gives: % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | | Case 1: % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | (260) ~ v1_funct_2(all_118_0, all_186_0, all_116_0) % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | REDUCE: (251), (260) imply: % 173.96/24.36 | | | | | | | (261) ~ v1_funct_2(all_118_0, all_140_0, all_116_0) % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | PRED_UNIFY: (160), (261) imply: % 173.96/24.36 | | | | | | | (262) $false % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | CLOSE: (262) is inconsistent. % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | Case 2: % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | (263) ~ v1_funct_2(all_118_1, all_186_0, all_116_0) % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | REDUCE: (251), (263) imply: % 173.96/24.36 | | | | | | | (264) ~ v1_funct_2(all_118_1, all_140_0, all_116_0) % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | PRED_UNIFY: (161), (264) imply: % 173.96/24.36 | | | | | | | (265) $false % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | | CLOSE: (265) is inconsistent. % 173.96/24.36 | | | | | | | % 173.96/24.36 | | | | | | End of split % 173.96/24.36 | | | | | | % 173.96/24.36 | | | | | End of split % 173.96/24.36 | | | | | % 173.96/24.36 | | | | End of split % 173.96/24.36 | | | | % 173.96/24.36 | | | End of split % 173.96/24.36 | | | % 173.96/24.37 | | End of split % 173.96/24.37 | | % 173.96/24.37 | End of split % 173.96/24.37 | % 173.96/24.37 End of proof % 173.96/24.37 % SZS output end Proof for theBenchmark % 173.96/24.37 % 173.96/24.37 23752ms %------------------------------------------------------------------------------