%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : TOP024+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 : n023.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 : Fri Sep 1 05:58:49 EDT 2023 % Result : Theorem 26.03s 4.11s % Output : Proof 59.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : TOP024+1 : TPTP v8.1.2. Released v3.4.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n023.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 : Sat Aug 26 23:22:11 EDT 2023 % 0.12/0.34 % CPUTime : % 0.64/0.67 ________ _____ % 0.64/0.67 ___ __ \_________(_)________________________________ % 0.64/0.67 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.64/0.67 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.64/0.67 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.64/0.67 % 0.64/0.67 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.64/0.67 (2023-06-19) % 0.64/0.67 % 0.64/0.67 (c) Philipp Rümmer, 2009-2023 % 0.64/0.67 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.64/0.67 Amanda Stjerna. % 0.64/0.67 Free software under BSD-3-Clause. % 0.64/0.67 % 0.64/0.67 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.64/0.67 % 0.64/0.67 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.64/0.68 Running up to 7 provers in parallel. % 0.77/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.77/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.77/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.77/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.77/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.77/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.77/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.31/1.22 Prover 4: Preprocessing ... % 3.31/1.22 Prover 1: Preprocessing ... % 3.82/1.26 Prover 3: Preprocessing ... % 3.82/1.26 Prover 5: Preprocessing ... % 3.82/1.26 Prover 0: Preprocessing ... % 3.82/1.26 Prover 2: Preprocessing ... % 3.82/1.26 Prover 6: Preprocessing ... % 8.70/1.93 Prover 5: Proving ... % 8.70/1.94 Prover 1: Warning: ignoring some quantifiers % 9.55/1.99 Prover 1: Constructing countermodel ... % 9.96/2.04 Prover 3: Warning: ignoring some quantifiers % 10.11/2.06 Prover 2: Proving ... % 10.11/2.06 Prover 6: Proving ... % 10.11/2.07 Prover 3: Constructing countermodel ... % 14.60/2.63 Prover 4: Warning: ignoring some quantifiers % 15.21/2.74 Prover 4: Constructing countermodel ... % 17.99/3.11 Prover 0: Proving ... % 25.72/4.11 Prover 5: proved (3418ms) % 26.03/4.11 % 26.03/4.11 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 26.03/4.11 % 26.03/4.11 Prover 0: stopped % 26.03/4.11 Prover 6: stopped % 26.03/4.11 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 26.03/4.11 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 26.03/4.11 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 26.03/4.12 Prover 2: stopped % 26.03/4.13 Prover 3: stopped % 26.24/4.14 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 26.24/4.14 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 26.90/4.24 Prover 10: Preprocessing ... % 26.90/4.24 Prover 7: Preprocessing ... % 26.90/4.27 Prover 8: Preprocessing ... % 26.90/4.28 Prover 13: Preprocessing ... % 27.38/4.30 Prover 11: Preprocessing ... % 27.94/4.36 Prover 10: Warning: ignoring some quantifiers % 28.09/4.39 Prover 7: Warning: ignoring some quantifiers % 28.09/4.39 Prover 10: Constructing countermodel ... % 28.09/4.41 Prover 7: Constructing countermodel ... % 28.42/4.44 Prover 13: Warning: ignoring some quantifiers % 28.64/4.46 Prover 13: Constructing countermodel ... % 28.64/4.46 Prover 8: Warning: ignoring some quantifiers % 28.64/4.47 Prover 8: Constructing countermodel ... % 30.95/4.80 Prover 10: gave up % 30.95/4.81 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 32.05/4.92 Prover 16: Preprocessing ... % 32.81/4.99 Prover 16: Warning: ignoring some quantifiers % 32.81/5.00 Prover 16: Constructing countermodel ... % 33.22/5.07 Prover 11: Warning: ignoring some quantifiers % 33.22/5.11 Prover 11: Constructing countermodel ... % 47.21/6.89 Prover 7: gave up % 47.94/6.92 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 48.67/7.01 Prover 19: Preprocessing ... % 49.37/7.18 Prover 19: Warning: ignoring some quantifiers % 50.19/7.20 Prover 19: Constructing countermodel ... % 57.22/8.09 Prover 13: Found proof (size 547) % 57.22/8.09 Prover 13: proved (3952ms) % 57.22/8.09 Prover 19: stopped % 57.22/8.09 Prover 16: stopped % 57.22/8.09 Prover 11: stopped % 57.22/8.10 Prover 8: stopped % 57.22/8.10 Prover 4: stopped % 57.22/8.10 Prover 1: stopped % 57.22/8.10 % 57.22/8.10 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 57.22/8.10 % 58.09/8.34 % SZS output start Proof for theBenchmark % 58.09/8.35 Assumptions after simplification: % 58.09/8.35 --------------------------------- % 58.09/8.35 % 58.09/8.35 (cc1_tops_1) % 58.43/8.37 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.43/8.37 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & % 58.43/8.37 $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ % 58.43/8.37 m1_subset_1(v3, v2) | v4_pre_topc(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | % 58.43/8.37 ~ v1_xboole_0(v3) | ~ m1_subset_1(v3, v2) | v3_pre_topc(v3, v0)))) & ! % 58.43/8.37 [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] % 58.43/8.38 : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & % 58.43/8.38 $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ % 58.43/8.38 m1_subset_1(v3, v2) | v4_pre_topc(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | % 58.43/8.38 ~ v1_xboole_0(v3) | ~ m1_subset_1(v3, v2) | v3_pre_topc(v3, v0)))) % 58.43/8.38 % 58.43/8.38 (cc2_tops_1) % 58.46/8.38 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.46/8.38 l1_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] % 58.46/8.38 : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ m1_subset_1(v3, v2) | v2_tops_1(v3, % 58.46/8.38 v0)))) & ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ? [v1: $i] : % 58.46/8.38 ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & $i(v1) % 58.46/8.38 & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ m1_subset_1(v3, v2) | % 58.46/8.38 v2_tops_1(v3, v0)))) % 58.46/8.38 % 58.46/8.38 (cc3_tops_1) % 58.46/8.38 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.46/8.38 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & % 58.46/8.38 $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ % 58.46/8.38 m1_subset_1(v3, v2) | v3_tops_1(v3, v0)))) & ! [v0: $i] : ( ~ $i(v0) | % 58.46/8.38 ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] : ? [v2: $i] : % 58.46/8.38 (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & $i(v1) & ! [v3: $i] % 58.46/8.38 : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ m1_subset_1(v3, v2) | v3_tops_1(v3, % 58.46/8.38 v0)))) % 58.46/8.38 % 58.46/8.38 (cc4_tops_1) % 58.46/8.39 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.46/8.39 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & % 58.46/8.39 $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ % 58.46/8.39 m1_subset_1(v3, v2) | v2_tops_1(v3, v0)))) & ! [v0: $i] : ( ~ $i(v0) | % 58.46/8.39 ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] : ? [v2: $i] : % 58.46/8.39 (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & $i(v1) & ! [v3: $i] % 58.46/8.39 : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.46/8.39 v2_tops_1(v3, v0)))) % 58.46/8.39 % 58.46/8.39 (cc5_tops_1) % 58.46/8.39 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.46/8.39 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & % 58.46/8.39 $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ v2_tops_1(v3, v0) | ~ % 58.46/8.39 v4_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | v3_tops_1(v3, v0)))) & ! % 58.46/8.39 [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] % 58.46/8.39 : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & % 58.46/8.39 $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ v2_tops_1(v3, v0) | ~ % 58.46/8.39 v4_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | v3_tops_1(v3, v0)))) % 58.46/8.39 % 58.46/8.39 (cc6_tops_1) % 58.46/8.40 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.46/8.40 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & % 58.46/8.40 $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ % 58.46/8.40 v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | v2_tops_1(v3, v0)) & ! % 58.46/8.40 [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ % 58.46/8.40 m1_subset_1(v3, v2) | v4_pre_topc(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | % 58.46/8.40 ~ v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.46/8.40 v1_xboole_0(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ % 58.46/8.40 v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | v5_membered(v3)) & ! % 58.46/8.40 [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ % 58.46/8.40 m1_subset_1(v3, v2) | v4_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.46/8.40 v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.46/8.40 v3_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ % 58.46/8.40 v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | v2_membered(v3)) & ! % 58.46/8.40 [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ % 58.46/8.40 m1_subset_1(v3, v2) | v1_membered(v3)))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 58.46/8.40 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] : ? [v2: $i] : % 58.46/8.40 (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & $i(v1) & ! [v3: $i] % 58.46/8.40 : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ % 58.46/8.40 m1_subset_1(v3, v2) | v2_tops_1(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.46/8.40 v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.46/8.40 v4_pre_topc(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | % 58.46/8.40 ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | v1_xboole_0(v3)) & ! % 58.46/8.40 [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ % 58.46/8.40 m1_subset_1(v3, v2) | v5_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.46/8.40 v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.46/8.40 v4_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ % 58.46/8.40 v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | v3_membered(v3)) & ! % 58.46/8.40 [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ % 58.46/8.40 m1_subset_1(v3, v2) | v2_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.46/8.40 v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.46/8.40 v1_membered(v3)))) % 58.46/8.40 % 58.46/8.40 (d2_tops_3) % 58.61/8.41 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.41 l1_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] % 58.61/8.41 : ! [v4: $i] : (v4 = v1 | ~ (k6_pre_topc(v0, v3) = v4) | ~ $i(v3) | ~ % 58.61/8.41 v1_tops_1(v3, v0) | ~ m1_subset_1(v3, v2)) & ! [v3: $i] : ( ~ % 58.61/8.41 (k6_pre_topc(v0, v3) = v1) | ~ $i(v3) | ~ m1_subset_1(v3, v2) | % 58.61/8.41 v1_tops_1(v3, v0)))) & ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | % 58.61/8.41 ? [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & % 58.61/8.41 $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ m1_subset_1(v3, v2) | ? % 58.61/8.41 [v4: $i] : (k6_pre_topc(v0, v3) = v4 & $i(v4) & ( ~ (v4 = v1) | % 58.61/8.41 v1_tops_1(v3, v0)) & (v4 = v1 | ~ v1_tops_1(v3, v0)))))) % 58.61/8.41 % 58.61/8.41 (d5_tsp_2) % 58.61/8.41 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.41 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : % 58.61/8.41 (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : (v4 = v1 | ~ % 58.61/8.41 (k3_tex_4(v0, v3) = v4) | ~ $i(v3) | ~ v1_tsp_2(v3, v0) | ~ % 58.61/8.41 m1_subset_1(v3, v2)) & ! [v3: $i] : ! [v4: $i] : ( ~ (k3_tex_4(v0, v3) % 58.61/8.41 = v4) | ~ $i(v3) | ~ v1_tsp_2(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.61/8.41 v1_tsp_1(v3, v0)) & ! [v3: $i] : ( ~ (k3_tex_4(v0, v3) = v1) | ~ % 58.61/8.41 $i(v3) | ~ v1_tsp_1(v3, v0) | ~ m1_subset_1(v3, v2) | v1_tsp_2(v3, % 58.61/8.41 v0)))) & ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ % 58.61/8.41 v2_pre_topc(v0) | v3_struct_0(v0) | ? [v1: $i] : ? [v2: $i] : % 58.61/8.41 (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & $i(v1) & ! [v3: $i] % 58.61/8.41 : ( ~ $i(v3) | ~ m1_subset_1(v3, v2) | ? [v4: $i] : (k3_tex_4(v0, v3) = % 58.61/8.41 v4 & $i(v4) & ( ~ (v4 = v1) | ~ v1_tsp_1(v3, v0) | v1_tsp_2(v3, v0)) % 58.61/8.41 & ( ~ v1_tsp_2(v3, v0) | (v4 = v1 & v1_tsp_1(v3, v0))))))) % 58.61/8.41 % 58.61/8.41 (dt_k2_pre_topc) % 58.61/8.41 ! [v0: $i] : ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.41 l1_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v2 & % 58.61/8.41 k1_zfmisc_1(v2) = v3 & $i(v3) & $i(v2) & m1_subset_1(v1, v3))) & ! [v0: % 58.61/8.41 $i] : ( ~ $i(v0) | ~ l1_struct_0(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: % 58.61/8.41 $i] : (k2_pre_topc(v0) = v1 & u1_struct_0(v0) = v2 & k1_zfmisc_1(v2) = v3 % 58.61/8.41 & $i(v3) & $i(v2) & $i(v1) & m1_subset_1(v1, v3))) % 58.61/8.41 % 58.61/8.41 (dt_l1_pre_topc) % 58.61/8.42 ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | l1_struct_0(v0)) % 58.61/8.42 % 58.61/8.42 (fc1_struct_0) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.42 l1_struct_0(v0) | ~ v1_xboole_0(v1) | v3_struct_0(v0)) & ! [v0: $i] : ( ~ % 58.61/8.42 $i(v0) | ~ l1_struct_0(v0) | v3_struct_0(v0) | ? [v1: $i] : % 58.61/8.42 (u1_struct_0(v0) = v1 & $i(v1) & ~ v1_xboole_0(v1))) % 58.61/8.42 % 58.61/8.42 (fc1_subset_1) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.42 v1_xboole_0(v1)) % 58.61/8.42 % 58.61/8.42 (fc2_pre_topc) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.42 l1_struct_0(v0) | ~ v1_xboole_0(v1) | v3_struct_0(v0)) & ! [v0: $i] : ( ~ % 58.61/8.42 $i(v0) | ~ l1_struct_0(v0) | v3_struct_0(v0) | ? [v1: $i] : % 58.61/8.42 (k2_pre_topc(v0) = v1 & $i(v1) & ~ v1_xboole_0(v1))) % 58.61/8.42 % 58.61/8.42 (fc5_pre_topc) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.42 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v4_pre_topc(v1, v0)) & ! [v0: $i] : % 58.61/8.42 ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] : % 58.61/8.42 (k2_pre_topc(v0) = v1 & $i(v1) & v4_pre_topc(v1, v0))) % 58.61/8.42 % 58.61/8.42 (fc8_tops_1) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.42 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v4_pre_topc(v1, v0)) & ! [v0: $i] : % 58.61/8.42 ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | ~ l1_pre_topc(v0) | ~ % 58.61/8.42 v2_pre_topc(v0) | v3_pre_topc(v1, v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 58.61/8.42 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] : (k2_pre_topc(v0) = v1 & % 58.61/8.42 $i(v1) & v4_pre_topc(v1, v0) & v3_pre_topc(v1, v0))) % 58.61/8.42 % 58.61/8.42 (fc9_tops_1) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.42 l1_pre_topc(v0) | v1_tops_1(v1, v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 58.61/8.42 l1_pre_topc(v0) | ? [v1: $i] : (k2_pre_topc(v0) = v1 & $i(v1) & % 58.61/8.42 v1_tops_1(v1, v0))) % 58.61/8.42 % 58.61/8.42 (rc1_subset_1) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ $i(v0) | % 58.61/8.42 v1_xboole_0(v0) | ? [v2: $i] : ($i(v2) & m1_subset_1(v2, v1) & ~ % 58.61/8.42 v1_xboole_0(v2))) % 58.61/8.42 % 58.61/8.42 (rc1_tops_1) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.42 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : % 58.61/8.42 (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v3_pre_topc(v3, v0) & % 58.61/8.42 m1_subset_1(v3, v2))) & ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ % 58.61/8.42 v2_pre_topc(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) % 58.61/8.42 = v1 & k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & v3_pre_topc(v3, % 58.61/8.42 v0) & m1_subset_1(v3, v2))) % 58.61/8.42 % 58.61/8.42 (rc2_tops_1) % 58.61/8.42 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.61/8.42 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : % 58.61/8.42 (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v4_pre_topc(v3, v0) & % 58.61/8.42 v3_pre_topc(v3, v0) & m1_subset_1(v3, v2))) & ! [v0: $i] : ( ~ $i(v0) | % 58.61/8.42 ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: % 58.61/8.42 $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & % 58.61/8.42 $i(v1) & v4_pre_topc(v3, v0) & v3_pre_topc(v3, v0) & m1_subset_1(v3, v2))) % 58.61/8.42 % 58.61/8.42 (rc3_struct_0) % 58.61/8.42 ? [v0: $i] : ($i(v0) & l1_struct_0(v0) & ~ v3_struct_0(v0)) % 58.61/8.42 % 58.61/8.42 (rc3_tops_1) % 58.71/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.43 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? % 58.71/8.43 [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v4_pre_topc(v3, v0) & % 58.71/8.43 v3_pre_topc(v3, v0) & m1_subset_1(v3, v2) & ~ v1_xboole_0(v3))) & ! [v0: % 58.71/8.43 $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) % 58.71/8.43 | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & % 58.71/8.43 k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & v4_pre_topc(v3, v0) & % 58.71/8.43 v3_pre_topc(v3, v0) & m1_subset_1(v3, v2) & ~ v1_xboole_0(v3))) % 58.71/8.43 % 58.71/8.43 (rc4_tops_1) % 58.71/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.43 l1_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) % 58.71/8.43 & $i(v2) & v2_tops_1(v3, v0) & v1_xboole_0(v3) & v5_membered(v3) & % 58.71/8.43 v4_membered(v3) & v3_membered(v3) & v2_membered(v3) & v1_membered(v3) & % 58.71/8.43 m1_subset_1(v3, v2))) & ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ? % 58.71/8.43 [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & % 58.71/8.43 k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & v2_tops_1(v3, v0) & % 58.71/8.43 v1_xboole_0(v3) & v5_membered(v3) & v4_membered(v3) & v3_membered(v3) & % 58.71/8.43 v2_membered(v3) & v1_membered(v3) & m1_subset_1(v3, v2))) % 58.71/8.43 % 58.71/8.43 (rc5_struct_0) % 58.71/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.43 l1_struct_0(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : % 58.71/8.43 (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & m1_subset_1(v3, v2) & ~ % 58.71/8.43 v1_xboole_0(v3))) & ! [v0: $i] : ( ~ $i(v0) | ~ l1_struct_0(v0) | % 58.71/8.43 v3_struct_0(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) % 58.71/8.43 = v1 & k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & m1_subset_1(v3, % 58.71/8.43 v2) & ~ v1_xboole_0(v3))) % 58.71/8.43 % 58.71/8.43 (rc5_tops_1) % 58.71/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.43 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : % 58.71/8.43 (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v3_tops_1(v3, v0) & v2_tops_1(v3, % 58.71/8.43 v0) & v4_pre_topc(v3, v0) & v3_pre_topc(v3, v0) & v1_xboole_0(v3) & % 58.71/8.43 v5_membered(v3) & v4_membered(v3) & v3_membered(v3) & v2_membered(v3) & % 58.71/8.43 v1_membered(v3) & m1_subset_1(v3, v2))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 58.71/8.43 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: % 58.71/8.43 $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & % 58.71/8.43 $i(v1) & v3_tops_1(v3, v0) & v2_tops_1(v3, v0) & v4_pre_topc(v3, v0) & % 58.71/8.43 v3_pre_topc(v3, v0) & v1_xboole_0(v3) & v5_membered(v3) & v4_membered(v3) % 58.71/8.43 & v3_membered(v3) & v2_membered(v3) & v1_membered(v3) & m1_subset_1(v3, % 58.71/8.43 v2))) % 58.71/8.43 % 58.71/8.43 (rc6_pre_topc) % 58.71/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.43 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : % 58.71/8.43 (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v4_pre_topc(v3, v0) & % 58.71/8.43 m1_subset_1(v3, v2))) & ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ % 58.71/8.43 v2_pre_topc(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) % 58.71/8.43 = v1 & k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & v4_pre_topc(v3, % 58.71/8.43 v0) & m1_subset_1(v3, v2))) % 58.71/8.43 % 58.71/8.43 (rc7_pre_topc) % 58.71/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.43 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : ? % 58.71/8.43 [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v4_pre_topc(v3, v0) & % 58.71/8.43 m1_subset_1(v3, v2) & ~ v1_xboole_0(v3))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 58.71/8.43 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v1: $i] : ? % 58.71/8.43 [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & % 58.71/8.43 $i(v3) & $i(v2) & $i(v1) & v4_pre_topc(v3, v0) & m1_subset_1(v3, v2) & ~ % 58.71/8.43 v1_xboole_0(v3))) % 58.71/8.43 % 58.71/8.43 (t12_pre_topc) % 58.71/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.43 l1_struct_0(v0) | (u1_struct_0(v0) = v1 & $i(v1))) & ! [v0: $i] : ( ~ % 58.71/8.43 $i(v0) | ~ l1_struct_0(v0) | ? [v1: $i] : (k2_pre_topc(v0) = v1 & % 58.71/8.43 u1_struct_0(v0) = v1 & $i(v1))) % 58.71/8.43 % 58.71/8.43 (t2_subset) % 58.71/8.43 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ m1_subset_1(v0, v1) | % 58.71/8.43 v1_xboole_0(v1) | r2_hidden(v0, v1)) % 58.71/8.43 % 58.71/8.43 (t2_tsp_2) % 58.71/8.43 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 % 58.71/8.43 & k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & v1_tsp_2(v3, % 58.71/8.43 v0) & m1_subset_1(v3, v2) & l1_pre_topc(v0) & v2_pre_topc(v0) & ~ % 58.71/8.43 v1_tops_1(v3, v0) & ~ v3_struct_0(v0)) % 58.71/8.43 % 58.71/8.44 (t52_pre_topc) % 58.71/8.44 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.44 l1_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] % 58.71/8.44 : ! [v4: $i] : (v4 = v3 | ~ (k6_pre_topc(v0, v3) = v4) | ~ $i(v3) | ~ % 58.71/8.44 v4_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2)) & ! [v3: $i] : ( ~ % 58.71/8.44 (k6_pre_topc(v0, v3) = v3) | ~ $i(v3) | ~ m1_subset_1(v3, v2) | ~ % 58.71/8.44 v2_pre_topc(v0) | v4_pre_topc(v3, v0)))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 58.71/8.44 l1_pre_topc(v0) | ? [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 & % 58.71/8.44 k1_zfmisc_1(v1) = v2 & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.44 m1_subset_1(v3, v2) | ? [v4: $i] : (k6_pre_topc(v0, v3) = v4 & $i(v4) & % 58.71/8.44 ( ~ (v4 = v3) | ~ v2_pre_topc(v0) | v4_pre_topc(v3, v0)) & (v4 = v3 | % 58.71/8.44 ~ v4_pre_topc(v3, v0)))))) % 58.71/8.44 % 58.71/8.44 (t64_tex_4) % 58.71/8.44 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.44 l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: $i] : % 58.71/8.44 (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( % 58.71/8.44 ~ (k3_tex_4(v0, v3) = v4) | ~ (k6_pre_topc(v0, v4) = v5) | ~ $i(v3) | % 58.71/8.44 ~ m1_subset_1(v3, v2) | (k6_pre_topc(v0, v3) = v5 & $i(v5))))) & ! [v0: % 58.71/8.44 $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) % 58.71/8.44 | ? [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & % 58.71/8.44 $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ m1_subset_1(v3, v2) | ? % 58.71/8.44 [v4: $i] : ? [v5: $i] : (k3_tex_4(v0, v3) = v4 & k6_pre_topc(v0, v4) = % 58.71/8.44 v5 & k6_pre_topc(v0, v3) = v5 & $i(v5) & $i(v4))))) % 58.71/8.44 % 58.71/8.44 (function-axioms) % 58.71/8.44 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 58.71/8.44 (k3_tex_4(v3, v2) = v1) | ~ (k3_tex_4(v3, v2) = v0)) & ! [v0: $i] : ! % 58.71/8.44 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (k6_pre_topc(v3, v2) = % 58.71/8.44 v1) | ~ (k6_pre_topc(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 58.71/8.44 $i] : (v1 = v0 | ~ (k2_pre_topc(v2) = v1) | ~ (k2_pre_topc(v2) = v0)) & ! % 58.71/8.44 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (u1_struct_0(v2) = v1) | % 58.71/8.44 ~ (u1_struct_0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = % 58.71/8.44 v0 | ~ (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) % 58.71/8.44 % 58.71/8.44 Further assumptions not needed in the proof: % 58.71/8.44 -------------------------------------------- % 58.71/8.44 antisymmetry_r2_hidden, cc10_membered, cc11_membered, cc12_membered, % 58.71/8.44 cc13_membered, cc14_membered, cc15_membered, cc16_membered, cc17_membered, % 58.71/8.44 cc18_membered, cc19_membered, cc1_membered, cc20_membered, cc2_membered, % 58.71/8.44 cc3_membered, cc4_membered, dt_k1_xboole_0, dt_k1_zfmisc_1, dt_k3_tex_4, % 58.71/8.44 dt_k6_pre_topc, dt_l1_struct_0, dt_m1_subset_1, dt_u1_struct_0, % 58.71/8.44 existence_l1_pre_topc, existence_l1_struct_0, existence_m1_subset_1, fc2_tops_1, % 58.71/8.44 fc6_membered, rc1_membered, rc2_subset_1, reflexivity_r1_tarski, t1_subset, % 58.71/8.44 t3_subset, t4_subset, t5_subset, t6_boole, t7_boole, t8_boole % 58.71/8.44 % 58.71/8.44 Those formulas are unsatisfiable: % 58.71/8.44 --------------------------------- % 58.71/8.44 % 58.71/8.44 Begin of proof % 58.71/8.44 | % 58.71/8.44 | ALPHA: (cc1_tops_1) implies: % 58.71/8.45 | (1) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? % 58.71/8.45 | [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 % 58.71/8.45 | & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | % 58.71/8.45 | ~ m1_subset_1(v3, v2) | v4_pre_topc(v3, v0)) & ! [v3: $i] : ( ~ % 58.71/8.45 | $i(v3) | ~ v1_xboole_0(v3) | ~ m1_subset_1(v3, v2) | % 58.71/8.45 | v3_pre_topc(v3, v0)))) % 58.71/8.45 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.45 | l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) % 58.71/8.45 | = v2 & $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ % 58.71/8.45 | m1_subset_1(v3, v2) | v4_pre_topc(v3, v0)) & ! [v3: $i] : ( ~ % 58.71/8.45 | $i(v3) | ~ v1_xboole_0(v3) | ~ m1_subset_1(v3, v2) | % 58.71/8.45 | v3_pre_topc(v3, v0)))) % 58.71/8.45 | % 58.71/8.45 | ALPHA: (cc2_tops_1) implies: % 58.71/8.45 | (3) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ? [v1: $i] : ? [v2: % 58.71/8.45 | $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & % 58.71/8.45 | $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ % 58.71/8.45 | m1_subset_1(v3, v2) | v2_tops_1(v3, v0)))) % 58.71/8.45 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.45 | l1_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & ! % 58.71/8.45 | [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ m1_subset_1(v3, v2) % 58.71/8.45 | | v2_tops_1(v3, v0)))) % 58.71/8.45 | % 58.71/8.45 | ALPHA: (cc3_tops_1) implies: % 58.71/8.45 | (5) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? % 58.71/8.45 | [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 % 58.71/8.45 | & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | % 58.71/8.45 | ~ m1_subset_1(v3, v2) | v3_tops_1(v3, v0)))) % 58.71/8.45 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.45 | l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) % 58.71/8.45 | = v2 & $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ v1_xboole_0(v3) | ~ % 58.71/8.45 | m1_subset_1(v3, v2) | v3_tops_1(v3, v0)))) % 58.71/8.45 | % 58.71/8.45 | ALPHA: (cc4_tops_1) implies: % 58.71/8.45 | (7) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? % 58.71/8.45 | [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 % 58.71/8.45 | & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) % 58.71/8.45 | | ~ m1_subset_1(v3, v2) | v2_tops_1(v3, v0)))) % 58.71/8.45 | (8) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 58.71/8.45 | l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) % 58.71/8.45 | = v2 & $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, v0) | % 58.71/8.45 | ~ m1_subset_1(v3, v2) | v2_tops_1(v3, v0)))) % 58.71/8.45 | % 58.71/8.45 | ALPHA: (cc5_tops_1) implies: % 58.71/8.45 | (9) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? % 58.71/8.45 | [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 % 58.71/8.45 | & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ v2_tops_1(v3, v0) % 58.71/8.45 | | ~ v4_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | v3_tops_1(v3, % 58.71/8.45 | v0)))) % 58.71/8.45 | (10) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.45 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : % 58.71/8.45 | (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.45 | v2_tops_1(v3, v0) | ~ v4_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.45 | v2) | v3_tops_1(v3, v0)))) % 58.71/8.45 | % 58.71/8.45 | ALPHA: (cc6_tops_1) implies: % 58.71/8.45 | (11) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.45 | ? [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = % 58.71/8.45 | v2 & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, % 58.71/8.45 | v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.71/8.45 | v2_tops_1(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | ~ v3_tops_1(v3, % 58.71/8.46 | v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, v2) | % 58.71/8.46 | v4_pre_topc(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v1_xboole_0(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v5_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v4_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v3_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v2_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v1_membered(v3)))) % 58.71/8.46 | (12) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.46 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : % 58.71/8.46 | (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v2_tops_1(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v4_pre_topc(v3, v0)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v1_xboole_0(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v5_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v4_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v3_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v2_membered(v3)) & ! [v3: $i] : ( ~ $i(v3) | ~ % 58.71/8.46 | v3_tops_1(v3, v0) | ~ v3_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2) | v1_membered(v3)))) % 58.71/8.46 | % 58.71/8.46 | ALPHA: (d2_tops_3) implies: % 58.71/8.46 | (13) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ? [v1: $i] : ? [v2: % 58.71/8.46 | $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & % 58.71/8.46 | $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ m1_subset_1(v3, v2) | ? % 58.71/8.46 | [v4: $i] : (k6_pre_topc(v0, v3) = v4 & $i(v4) & ( ~ (v4 = v1) | % 58.71/8.46 | v1_tops_1(v3, v0)) & (v4 = v1 | ~ v1_tops_1(v3, v0)))))) % 58.71/8.46 | (14) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.46 | ~ l1_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & % 58.71/8.46 | ! [v3: $i] : ! [v4: $i] : (v4 = v1 | ~ (k6_pre_topc(v0, v3) = % 58.71/8.46 | v4) | ~ $i(v3) | ~ v1_tops_1(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.46 | v2)) & ! [v3: $i] : ( ~ (k6_pre_topc(v0, v3) = v1) | ~ % 58.71/8.46 | $i(v3) | ~ m1_subset_1(v3, v2) | v1_tops_1(v3, v0)))) % 58.71/8.46 | % 58.71/8.46 | ALPHA: (d5_tsp_2) implies: % 58.71/8.46 | (15) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.46 | v3_struct_0(v0) | ? [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 % 58.71/8.46 | & k1_zfmisc_1(v1) = v2 & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ % 58.71/8.46 | $i(v3) | ~ m1_subset_1(v3, v2) | ? [v4: $i] : (k3_tex_4(v0, % 58.71/8.46 | v3) = v4 & $i(v4) & ( ~ (v4 = v1) | ~ v1_tsp_1(v3, v0) | % 58.71/8.46 | v1_tsp_2(v3, v0)) & ( ~ v1_tsp_2(v3, v0) | (v4 = v1 & % 58.71/8.46 | v1_tsp_1(v3, v0))))))) % 58.71/8.46 | (16) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.46 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 58.71/8.46 | $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : % 58.71/8.46 | (v4 = v1 | ~ (k3_tex_4(v0, v3) = v4) | ~ $i(v3) | ~ % 58.71/8.46 | v1_tsp_2(v3, v0) | ~ m1_subset_1(v3, v2)) & ! [v3: $i] : ! % 58.71/8.46 | [v4: $i] : ( ~ (k3_tex_4(v0, v3) = v4) | ~ $i(v3) | ~ % 58.71/8.46 | v1_tsp_2(v3, v0) | ~ m1_subset_1(v3, v2) | v1_tsp_1(v3, v0)) & % 58.71/8.46 | ! [v3: $i] : ( ~ (k3_tex_4(v0, v3) = v1) | ~ $i(v3) | ~ % 58.71/8.46 | v1_tsp_1(v3, v0) | ~ m1_subset_1(v3, v2) | v1_tsp_2(v3, v0)))) % 58.71/8.46 | % 58.71/8.46 | ALPHA: (dt_k2_pre_topc) implies: % 58.71/8.46 | (17) ! [v0: $i] : ( ~ $i(v0) | ~ l1_struct_0(v0) | ? [v1: $i] : ? [v2: % 58.71/8.46 | $i] : ? [v3: $i] : (k2_pre_topc(v0) = v1 & u1_struct_0(v0) = v2 & % 58.71/8.46 | k1_zfmisc_1(v2) = v3 & $i(v3) & $i(v2) & $i(v1) & m1_subset_1(v1, % 58.71/8.47 | v3))) % 58.71/8.47 | (18) ! [v0: $i] : ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | % 58.71/8.47 | ~ l1_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = % 58.71/8.47 | v2 & k1_zfmisc_1(v2) = v3 & $i(v3) & $i(v2) & m1_subset_1(v1, % 58.71/8.47 | v3))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (fc1_struct_0) implies: % 58.71/8.47 | (19) ! [v0: $i] : ( ~ $i(v0) | ~ l1_struct_0(v0) | v3_struct_0(v0) | ? % 58.71/8.47 | [v1: $i] : (u1_struct_0(v0) = v1 & $i(v1) & ~ v1_xboole_0(v1))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (fc2_pre_topc) implies: % 58.71/8.47 | (20) ! [v0: $i] : ( ~ $i(v0) | ~ l1_struct_0(v0) | v3_struct_0(v0) | ? % 58.71/8.47 | [v1: $i] : (k2_pre_topc(v0) = v1 & $i(v1) & ~ v1_xboole_0(v1))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (fc5_pre_topc) implies: % 58.71/8.47 | (21) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.47 | ? [v1: $i] : (k2_pre_topc(v0) = v1 & $i(v1) & v4_pre_topc(v1, v0))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (fc8_tops_1) implies: % 58.71/8.47 | (22) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.47 | ? [v1: $i] : (k2_pre_topc(v0) = v1 & $i(v1) & v4_pre_topc(v1, v0) & % 58.71/8.47 | v3_pre_topc(v1, v0))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (fc9_tops_1) implies: % 58.71/8.47 | (23) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ? [v1: $i] : % 58.71/8.47 | (k2_pre_topc(v0) = v1 & $i(v1) & v1_tops_1(v1, v0))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (rc1_tops_1) implies: % 58.71/8.47 | (24) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.47 | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & % 58.71/8.47 | k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & v3_pre_topc(v3, % 58.71/8.47 | v0) & m1_subset_1(v3, v2))) % 58.71/8.47 | (25) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.47 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : % 58.71/8.47 | (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v3_pre_topc(v3, v0) & % 58.71/8.47 | m1_subset_1(v3, v2))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (rc2_tops_1) implies: % 58.71/8.47 | (26) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.47 | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & % 58.71/8.47 | k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & v4_pre_topc(v3, % 58.71/8.47 | v0) & v3_pre_topc(v3, v0) & m1_subset_1(v3, v2))) % 58.71/8.47 | (27) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.47 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : % 58.71/8.47 | (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v4_pre_topc(v3, v0) & % 58.71/8.47 | v3_pre_topc(v3, v0) & m1_subset_1(v3, v2))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (rc3_tops_1) implies: % 58.71/8.47 | (28) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.47 | v3_struct_0(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 58.71/8.47 | (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & % 58.71/8.47 | $i(v1) & v4_pre_topc(v3, v0) & v3_pre_topc(v3, v0) & % 58.71/8.47 | m1_subset_1(v3, v2) & ~ v1_xboole_0(v3))) % 58.71/8.47 | (29) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.47 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 58.71/8.47 | $i] : ? [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & % 58.71/8.47 | v4_pre_topc(v3, v0) & v3_pre_topc(v3, v0) & m1_subset_1(v3, v2) & % 58.71/8.47 | ~ v1_xboole_0(v3))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (rc4_tops_1) implies: % 58.71/8.47 | (30) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ? [v1: $i] : ? [v2: % 58.71/8.47 | $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & % 58.71/8.47 | $i(v3) & $i(v2) & $i(v1) & v2_tops_1(v3, v0) & v1_xboole_0(v3) & % 58.71/8.47 | v5_membered(v3) & v4_membered(v3) & v3_membered(v3) & % 58.71/8.47 | v2_membered(v3) & v1_membered(v3) & m1_subset_1(v3, v2))) % 58.71/8.47 | (31) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.47 | ~ l1_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : (k1_zfmisc_1(v1) = % 58.71/8.47 | v2 & $i(v3) & $i(v2) & v2_tops_1(v3, v0) & v1_xboole_0(v3) & % 58.71/8.47 | v5_membered(v3) & v4_membered(v3) & v3_membered(v3) & % 58.71/8.47 | v2_membered(v3) & v1_membered(v3) & m1_subset_1(v3, v2))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (rc5_struct_0) implies: % 58.71/8.47 | (32) ! [v0: $i] : ( ~ $i(v0) | ~ l1_struct_0(v0) | v3_struct_0(v0) | ? % 58.71/8.47 | [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & % 58.71/8.47 | k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & m1_subset_1(v3, % 58.71/8.47 | v2) & ~ v1_xboole_0(v3))) % 58.71/8.47 | (33) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.47 | ~ l1_struct_0(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : % 58.71/8.47 | (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & m1_subset_1(v3, v2) & ~ % 58.71/8.47 | v1_xboole_0(v3))) % 58.71/8.47 | % 58.71/8.47 | ALPHA: (rc5_tops_1) implies: % 58.71/8.47 | (34) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.47 | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & % 58.71/8.48 | k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & v3_tops_1(v3, % 58.71/8.48 | v0) & v2_tops_1(v3, v0) & v4_pre_topc(v3, v0) & v3_pre_topc(v3, % 58.71/8.48 | v0) & v1_xboole_0(v3) & v5_membered(v3) & v4_membered(v3) & % 58.71/8.48 | v3_membered(v3) & v2_membered(v3) & v1_membered(v3) & % 58.71/8.48 | m1_subset_1(v3, v2))) % 58.71/8.48 | (35) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.48 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : % 58.71/8.48 | (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v3_tops_1(v3, v0) & % 58.71/8.48 | v2_tops_1(v3, v0) & v4_pre_topc(v3, v0) & v3_pre_topc(v3, v0) & % 58.71/8.48 | v1_xboole_0(v3) & v5_membered(v3) & v4_membered(v3) & % 58.71/8.48 | v3_membered(v3) & v2_membered(v3) & v1_membered(v3) & % 58.71/8.48 | m1_subset_1(v3, v2))) % 58.71/8.48 | % 58.71/8.48 | ALPHA: (rc6_pre_topc) implies: % 58.71/8.48 | (36) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.48 | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (u1_struct_0(v0) = v1 & % 58.71/8.48 | k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & $i(v1) & v4_pre_topc(v3, % 58.71/8.48 | v0) & m1_subset_1(v3, v2))) % 58.71/8.48 | (37) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.48 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | ? [v2: $i] : ? [v3: $i] : % 58.71/8.48 | (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v4_pre_topc(v3, v0) & % 58.71/8.48 | m1_subset_1(v3, v2))) % 58.71/8.48 | % 58.71/8.48 | ALPHA: (rc7_pre_topc) implies: % 58.71/8.48 | (38) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.48 | v3_struct_0(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 58.71/8.48 | (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & % 58.71/8.48 | $i(v1) & v4_pre_topc(v3, v0) & m1_subset_1(v3, v2) & ~ % 58.71/8.48 | v1_xboole_0(v3))) % 58.71/8.48 | (39) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.48 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 58.71/8.48 | $i] : ? [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & % 58.71/8.48 | v4_pre_topc(v3, v0) & m1_subset_1(v3, v2) & ~ v1_xboole_0(v3))) % 58.71/8.48 | % 58.71/8.48 | ALPHA: (t12_pre_topc) implies: % 58.71/8.48 | (40) ! [v0: $i] : ( ~ $i(v0) | ~ l1_struct_0(v0) | ? [v1: $i] : % 58.71/8.48 | (k2_pre_topc(v0) = v1 & u1_struct_0(v0) = v1 & $i(v1))) % 58.71/8.48 | (41) ! [v0: $i] : ! [v1: $i] : ( ~ (k2_pre_topc(v0) = v1) | ~ $i(v0) | % 58.71/8.48 | ~ l1_struct_0(v0) | (u1_struct_0(v0) = v1 & $i(v1))) % 58.71/8.48 | % 58.71/8.48 | ALPHA: (t52_pre_topc) implies: % 58.71/8.48 | (42) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ? [v1: $i] : ? [v2: % 58.71/8.48 | $i] : (u1_struct_0(v0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & % 58.71/8.48 | $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ m1_subset_1(v3, v2) | ? % 58.71/8.48 | [v4: $i] : (k6_pre_topc(v0, v3) = v4 & $i(v4) & ( ~ (v4 = v3) | % 58.71/8.48 | ~ v2_pre_topc(v0) | v4_pre_topc(v3, v0)) & (v4 = v3 | ~ % 58.71/8.48 | v4_pre_topc(v3, v0)))))) % 58.71/8.48 | (43) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.48 | ~ l1_pre_topc(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & % 58.71/8.48 | ! [v3: $i] : ! [v4: $i] : (v4 = v3 | ~ (k6_pre_topc(v0, v3) = % 58.71/8.48 | v4) | ~ $i(v3) | ~ v4_pre_topc(v3, v0) | ~ m1_subset_1(v3, % 58.71/8.48 | v2)) & ! [v3: $i] : ( ~ (k6_pre_topc(v0, v3) = v3) | ~ % 58.71/8.48 | $i(v3) | ~ m1_subset_1(v3, v2) | ~ v2_pre_topc(v0) | % 58.71/8.48 | v4_pre_topc(v3, v0)))) % 58.71/8.48 | % 58.71/8.48 | ALPHA: (t64_tex_4) implies: % 58.71/8.48 | (44) ! [v0: $i] : ( ~ $i(v0) | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | % 58.71/8.48 | v3_struct_0(v0) | ? [v1: $i] : ? [v2: $i] : (u1_struct_0(v0) = v1 % 58.71/8.48 | & k1_zfmisc_1(v1) = v2 & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ % 58.71/8.48 | $i(v3) | ~ m1_subset_1(v3, v2) | ? [v4: $i] : ? [v5: $i] : % 58.71/8.48 | (k3_tex_4(v0, v3) = v4 & k6_pre_topc(v0, v4) = v5 & % 58.71/8.48 | k6_pre_topc(v0, v3) = v5 & $i(v5) & $i(v4))))) % 58.71/8.48 | (45) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 58.71/8.48 | ~ l1_pre_topc(v0) | ~ v2_pre_topc(v0) | v3_struct_0(v0) | ? [v2: % 58.71/8.48 | $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : % 58.71/8.48 | ! [v5: $i] : ( ~ (k3_tex_4(v0, v3) = v4) | ~ (k6_pre_topc(v0, % 58.71/8.48 | v4) = v5) | ~ $i(v3) | ~ m1_subset_1(v3, v2) | % 58.71/8.48 | (k6_pre_topc(v0, v3) = v5 & $i(v5))))) % 58.71/8.48 | % 58.71/8.48 | ALPHA: (function-axioms) implies: % 58.71/8.48 | (46) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 58.71/8.48 | (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) % 58.71/8.48 | (47) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 58.71/8.48 | (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) % 58.71/8.48 | (48) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 58.71/8.48 | (k2_pre_topc(v2) = v1) | ~ (k2_pre_topc(v2) = v0)) % 58.71/8.48 | (49) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 58.71/8.48 | (k6_pre_topc(v3, v2) = v1) | ~ (k6_pre_topc(v3, v2) = v0)) % 58.71/8.48 | (50) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 58.71/8.48 | (k3_tex_4(v3, v2) = v1) | ~ (k3_tex_4(v3, v2) = v0)) % 58.71/8.48 | % 58.71/8.48 | DELTA: instantiating (rc3_struct_0) with fresh symbol all_65_0 gives: % 58.71/8.48 | (51) $i(all_65_0) & l1_struct_0(all_65_0) & ~ v3_struct_0(all_65_0) % 58.71/8.48 | % 58.71/8.48 | ALPHA: (51) implies: % 58.71/8.48 | (52) ~ v3_struct_0(all_65_0) % 58.71/8.48 | (53) l1_struct_0(all_65_0) % 58.71/8.48 | (54) $i(all_65_0) % 58.71/8.48 | % 58.71/8.48 | DELTA: instantiating (t2_tsp_2) with fresh symbols all_73_0, all_73_1, % 58.71/8.48 | all_73_2, all_73_3 gives: % 58.71/8.48 | (55) u1_struct_0(all_73_3) = all_73_2 & k1_zfmisc_1(all_73_2) = all_73_1 & % 58.71/8.48 | $i(all_73_0) & $i(all_73_1) & $i(all_73_2) & $i(all_73_3) & % 58.71/8.48 | v1_tsp_2(all_73_0, all_73_3) & m1_subset_1(all_73_0, all_73_1) & % 58.71/8.48 | l1_pre_topc(all_73_3) & v2_pre_topc(all_73_3) & ~ v1_tops_1(all_73_0, % 58.71/8.48 | all_73_3) & ~ v3_struct_0(all_73_3) % 58.71/8.48 | % 58.71/8.48 | ALPHA: (55) implies: % 58.71/8.48 | (56) ~ v3_struct_0(all_73_3) % 58.71/8.48 | (57) ~ v1_tops_1(all_73_0, all_73_3) % 58.71/8.49 | (58) v2_pre_topc(all_73_3) % 58.71/8.49 | (59) l1_pre_topc(all_73_3) % 58.71/8.49 | (60) m1_subset_1(all_73_0, all_73_1) % 58.71/8.49 | (61) v1_tsp_2(all_73_0, all_73_3) % 58.71/8.49 | (62) $i(all_73_3) % 58.71/8.49 | (63) $i(all_73_2) % 58.71/8.49 | (64) $i(all_73_0) % 58.71/8.49 | (65) k1_zfmisc_1(all_73_2) = all_73_1 % 58.71/8.49 | (66) u1_struct_0(all_73_3) = all_73_2 % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (28) with all_73_3, simplifying with (56), (58), % 58.71/8.49 | (59), (62) gives: % 58.71/8.49 | (67) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_73_3) = v0 % 58.71/8.49 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & v4_pre_topc(v2, % 58.71/8.49 | all_73_3) & v3_pre_topc(v2, all_73_3) & m1_subset_1(v2, v1) & ~ % 58.71/8.49 | v1_xboole_0(v2)) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (38) with all_73_3, simplifying with (56), (58), % 58.71/8.49 | (59), (62) gives: % 58.71/8.49 | (68) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_73_3) = v0 % 58.71/8.49 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & v4_pre_topc(v2, % 58.71/8.49 | all_73_3) & m1_subset_1(v2, v1) & ~ v1_xboole_0(v2)) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (44) with all_73_3, simplifying with (56), (58), % 58.71/8.49 | (59), (62) gives: % 58.71/8.49 | (69) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.49 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.49 | ~ m1_subset_1(v2, v1) | ? [v3: $i] : ? [v4: $i] : % 58.71/8.49 | (k3_tex_4(all_73_3, v2) = v3 & k6_pre_topc(all_73_3, v3) = v4 & % 58.71/8.49 | k6_pre_topc(all_73_3, v2) = v4 & $i(v4) & $i(v3)))) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (15) with all_73_3, simplifying with (56), (58), % 58.71/8.49 | (59), (62) gives: % 58.71/8.49 | (70) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.49 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.49 | ~ m1_subset_1(v2, v1) | ? [v3: $i] : (k3_tex_4(all_73_3, v2) = v3 % 58.71/8.49 | & $i(v3) & ( ~ (v3 = v0) | ~ v1_tsp_1(v2, all_73_3) | % 58.71/8.49 | v1_tsp_2(v2, all_73_3)) & ( ~ v1_tsp_2(v2, all_73_3) | (v3 = % 58.71/8.49 | v0 & v1_tsp_1(v2, all_73_3)))))) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (34) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (71) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_73_3) = v0 % 58.71/8.49 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & v3_tops_1(v2, % 58.71/8.49 | all_73_3) & v2_tops_1(v2, all_73_3) & v4_pre_topc(v2, all_73_3) & % 58.71/8.49 | v3_pre_topc(v2, all_73_3) & v1_xboole_0(v2) & v5_membered(v2) & % 58.71/8.49 | v4_membered(v2) & v3_membered(v2) & v2_membered(v2) & % 58.71/8.49 | v1_membered(v2) & m1_subset_1(v2, v1)) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (26) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (72) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_73_3) = v0 % 58.71/8.49 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & v4_pre_topc(v2, % 58.71/8.49 | all_73_3) & v3_pre_topc(v2, all_73_3) & m1_subset_1(v2, v1)) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (36) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (73) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_73_3) = v0 % 58.71/8.49 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & v4_pre_topc(v2, % 58.71/8.49 | all_73_3) & m1_subset_1(v2, v1)) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (24) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (74) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_73_3) = v0 % 58.71/8.49 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & v3_pre_topc(v2, % 58.71/8.49 | all_73_3) & m1_subset_1(v2, v1)) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (11) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (75) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.49 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.49 | ~ v3_tops_1(v2, all_73_3) | ~ v3_pre_topc(v2, all_73_3) | ~ % 58.71/8.49 | m1_subset_1(v2, v1) | v2_tops_1(v2, all_73_3)) & ! [v2: $i] : ( ~ % 58.71/8.49 | $i(v2) | ~ v3_tops_1(v2, all_73_3) | ~ v3_pre_topc(v2, all_73_3) % 58.71/8.49 | | ~ m1_subset_1(v2, v1) | v4_pre_topc(v2, all_73_3)) & ! [v2: % 58.71/8.49 | $i] : ( ~ $i(v2) | ~ v3_tops_1(v2, all_73_3) | ~ v3_pre_topc(v2, % 58.71/8.49 | all_73_3) | ~ m1_subset_1(v2, v1) | v1_xboole_0(v2)) & ! [v2: % 58.71/8.49 | $i] : ( ~ $i(v2) | ~ v3_tops_1(v2, all_73_3) | ~ v3_pre_topc(v2, % 58.71/8.49 | all_73_3) | ~ m1_subset_1(v2, v1) | v5_membered(v2)) & ! [v2: % 58.71/8.49 | $i] : ( ~ $i(v2) | ~ v3_tops_1(v2, all_73_3) | ~ v3_pre_topc(v2, % 58.71/8.49 | all_73_3) | ~ m1_subset_1(v2, v1) | v4_membered(v2)) & ! [v2: % 58.71/8.49 | $i] : ( ~ $i(v2) | ~ v3_tops_1(v2, all_73_3) | ~ v3_pre_topc(v2, % 58.71/8.49 | all_73_3) | ~ m1_subset_1(v2, v1) | v3_membered(v2)) & ! [v2: % 58.71/8.49 | $i] : ( ~ $i(v2) | ~ v3_tops_1(v2, all_73_3) | ~ v3_pre_topc(v2, % 58.71/8.49 | all_73_3) | ~ m1_subset_1(v2, v1) | v2_membered(v2)) & ! [v2: % 58.71/8.49 | $i] : ( ~ $i(v2) | ~ v3_tops_1(v2, all_73_3) | ~ v3_pre_topc(v2, % 58.71/8.49 | all_73_3) | ~ m1_subset_1(v2, v1) | v1_membered(v2))) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (7) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (76) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.49 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.49 | ~ v3_tops_1(v2, all_73_3) | ~ m1_subset_1(v2, v1) | v2_tops_1(v2, % 58.71/8.49 | all_73_3))) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (9) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (77) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.49 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.49 | ~ v2_tops_1(v2, all_73_3) | ~ v4_pre_topc(v2, all_73_3) | ~ % 58.71/8.49 | m1_subset_1(v2, v1) | v3_tops_1(v2, all_73_3))) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (5) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (78) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.49 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.49 | ~ v1_xboole_0(v2) | ~ m1_subset_1(v2, v1) | v3_tops_1(v2, % 58.71/8.49 | all_73_3))) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (1) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (79) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.49 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.49 | ~ v1_xboole_0(v2) | ~ m1_subset_1(v2, v1) | v4_pre_topc(v2, % 58.71/8.49 | all_73_3)) & ! [v2: $i] : ( ~ $i(v2) | ~ v1_xboole_0(v2) | ~ % 58.71/8.49 | m1_subset_1(v2, v1) | v3_pre_topc(v2, all_73_3))) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (22) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (80) ? [v0: $i] : (k2_pre_topc(all_73_3) = v0 & $i(v0) & v4_pre_topc(v0, % 58.71/8.49 | all_73_3) & v3_pre_topc(v0, all_73_3)) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (21) with all_73_3, simplifying with (58), (59), % 58.71/8.49 | (62) gives: % 58.71/8.49 | (81) ? [v0: $i] : (k2_pre_topc(all_73_3) = v0 & $i(v0) & v4_pre_topc(v0, % 58.71/8.49 | all_73_3)) % 58.71/8.49 | % 58.71/8.49 | GROUND_INST: instantiating (dt_l1_pre_topc) with all_73_3, simplifying with % 58.71/8.49 | (59), (62) gives: % 58.71/8.50 | (82) l1_struct_0(all_73_3) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (30) with all_73_3, simplifying with (59), (62) % 58.71/8.50 | gives: % 58.71/8.50 | (83) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_73_3) = v0 % 58.71/8.50 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & v2_tops_1(v2, % 58.71/8.50 | all_73_3) & v1_xboole_0(v2) & v5_membered(v2) & v4_membered(v2) & % 58.71/8.50 | v3_membered(v2) & v2_membered(v2) & v1_membered(v2) & % 58.71/8.50 | m1_subset_1(v2, v1)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (3) with all_73_3, simplifying with (59), (62) % 58.71/8.50 | gives: % 58.71/8.50 | (84) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.50 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.50 | ~ v1_xboole_0(v2) | ~ m1_subset_1(v2, v1) | v2_tops_1(v2, % 58.71/8.50 | all_73_3))) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (42) with all_73_3, simplifying with (59), (62) % 58.71/8.50 | gives: % 58.71/8.50 | (85) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.50 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.50 | ~ m1_subset_1(v2, v1) | ? [v3: $i] : (k6_pre_topc(all_73_3, v2) = % 58.71/8.50 | v3 & $i(v3) & ( ~ (v3 = v2) | ~ v2_pre_topc(all_73_3) | % 58.71/8.50 | v4_pre_topc(v2, all_73_3)) & (v3 = v2 | ~ v4_pre_topc(v2, % 58.71/8.50 | all_73_3))))) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (13) with all_73_3, simplifying with (59), (62) % 58.71/8.50 | gives: % 58.71/8.50 | (86) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 58.71/8.50 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ $i(v2) | % 58.71/8.50 | ~ m1_subset_1(v2, v1) | ? [v3: $i] : (k6_pre_topc(all_73_3, v2) = % 58.71/8.50 | v3 & $i(v3) & ( ~ (v3 = v0) | v1_tops_1(v2, all_73_3)) & (v3 = % 58.71/8.50 | v0 | ~ v1_tops_1(v2, all_73_3))))) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (23) with all_73_3, simplifying with (59), (62) % 58.71/8.50 | gives: % 58.71/8.50 | (87) ? [v0: $i] : (k2_pre_topc(all_73_3) = v0 & $i(v0) & v1_tops_1(v0, % 58.71/8.50 | all_73_3)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (32) with all_65_0, simplifying with (52), (53), % 58.71/8.50 | (54) gives: % 58.71/8.50 | (88) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_65_0) = v0 % 58.71/8.50 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & m1_subset_1(v2, % 58.71/8.50 | v1) & ~ v1_xboole_0(v2)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (20) with all_65_0, simplifying with (52), (53), % 58.71/8.50 | (54) gives: % 58.71/8.50 | (89) ? [v0: $i] : (k2_pre_topc(all_65_0) = v0 & $i(v0) & ~ % 58.71/8.50 | v1_xboole_0(v0)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (19) with all_65_0, simplifying with (52), (53), % 58.71/8.50 | (54) gives: % 58.71/8.50 | (90) ? [v0: $i] : (u1_struct_0(all_65_0) = v0 & $i(v0) & ~ % 58.71/8.50 | v1_xboole_0(v0)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (17) with all_65_0, simplifying with (53), (54) % 58.71/8.50 | gives: % 58.71/8.50 | (91) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (k2_pre_topc(all_65_0) = v0 % 58.71/8.50 | & u1_struct_0(all_65_0) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & % 58.71/8.50 | $i(v1) & $i(v0) & m1_subset_1(v0, v2)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (40) with all_65_0, simplifying with (53), (54) % 58.71/8.50 | gives: % 58.71/8.50 | (92) ? [v0: $i] : (k2_pre_topc(all_65_0) = v0 & u1_struct_0(all_65_0) = v0 % 58.71/8.50 | & $i(v0)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (rc1_subset_1) with all_73_2, all_73_1, simplifying % 58.71/8.50 | with (63), (65) gives: % 58.71/8.50 | (93) v1_xboole_0(all_73_2) | ? [v0: $i] : ($i(v0) & m1_subset_1(v0, % 58.71/8.50 | all_73_1) & ~ v1_xboole_0(v0)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (29) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (56), (58), (59), (62), (66) gives: % 58.71/8.50 | (94) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v1) & % 58.71/8.50 | $i(v0) & v4_pre_topc(v1, all_73_3) & v3_pre_topc(v1, all_73_3) & % 58.71/8.50 | m1_subset_1(v1, v0) & ~ v1_xboole_0(v1)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (39) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (56), (58), (59), (62), (66) gives: % 58.71/8.50 | (95) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v1) & % 58.71/8.50 | $i(v0) & v4_pre_topc(v1, all_73_3) & m1_subset_1(v1, v0) & ~ % 58.71/8.50 | v1_xboole_0(v1)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (45) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (56), (58), (59), (62), (66) gives: % 58.71/8.50 | (96) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ! % 58.71/8.50 | [v2: $i] : ! [v3: $i] : ( ~ (k3_tex_4(all_73_3, v1) = v2) | ~ % 58.71/8.50 | (k6_pre_topc(all_73_3, v2) = v3) | ~ $i(v1) | ~ m1_subset_1(v1, % 58.71/8.50 | v0) | (k6_pre_topc(all_73_3, v1) = v3 & $i(v3)))) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (16) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (56), (58), (59), (62), (66) gives: % 58.71/8.50 | (97) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ! % 58.71/8.50 | [v2: int] : (v2 = all_73_2 | ~ (k3_tex_4(all_73_3, v1) = v2) | ~ % 58.71/8.50 | $i(v1) | ~ v1_tsp_2(v1, all_73_3) | ~ m1_subset_1(v1, v0)) & ! % 58.71/8.50 | [v1: $i] : ! [v2: $i] : ( ~ (k3_tex_4(all_73_3, v1) = v2) | ~ % 58.71/8.50 | $i(v1) | ~ v1_tsp_2(v1, all_73_3) | ~ m1_subset_1(v1, v0) | % 58.71/8.50 | v1_tsp_1(v1, all_73_3)) & ! [v1: $i] : ( ~ (k3_tex_4(all_73_3, % 58.71/8.50 | v1) = all_73_2) | ~ $i(v1) | ~ v1_tsp_1(v1, all_73_3) | ~ % 58.71/8.50 | m1_subset_1(v1, v0) | v1_tsp_2(v1, all_73_3))) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (35) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (58), (59), (62), (66) gives: % 58.71/8.50 | (98) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v1) & % 58.71/8.50 | $i(v0) & v3_tops_1(v1, all_73_3) & v2_tops_1(v1, all_73_3) & % 58.71/8.50 | v4_pre_topc(v1, all_73_3) & v3_pre_topc(v1, all_73_3) & % 58.71/8.50 | v1_xboole_0(v1) & v5_membered(v1) & v4_membered(v1) & % 58.71/8.50 | v3_membered(v1) & v2_membered(v1) & v1_membered(v1) & % 58.71/8.50 | m1_subset_1(v1, v0)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (27) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (58), (59), (62), (66) gives: % 58.71/8.50 | (99) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v1) & % 58.71/8.50 | $i(v0) & v4_pre_topc(v1, all_73_3) & v3_pre_topc(v1, all_73_3) & % 58.71/8.50 | m1_subset_1(v1, v0)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (37) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (58), (59), (62), (66) gives: % 58.71/8.50 | (100) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v1) & % 58.71/8.50 | $i(v0) & v4_pre_topc(v1, all_73_3) & m1_subset_1(v1, v0)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (25) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (58), (59), (62), (66) gives: % 58.71/8.50 | (101) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v1) & % 58.71/8.50 | $i(v0) & v3_pre_topc(v1, all_73_3) & m1_subset_1(v1, v0)) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (12) with all_73_3, all_73_2, simplifying with % 58.71/8.50 | (58), (59), (62), (66) gives: % 58.71/8.50 | (102) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ( % 58.71/8.50 | ~ $i(v1) | ~ v3_tops_1(v1, all_73_3) | ~ v3_pre_topc(v1, % 58.71/8.50 | all_73_3) | ~ m1_subset_1(v1, v0) | v2_tops_1(v1, all_73_3)) & % 58.71/8.50 | ! [v1: $i] : ( ~ $i(v1) | ~ v3_tops_1(v1, all_73_3) | ~ % 58.71/8.50 | v3_pre_topc(v1, all_73_3) | ~ m1_subset_1(v1, v0) | % 58.71/8.50 | v4_pre_topc(v1, all_73_3)) & ! [v1: $i] : ( ~ $i(v1) | ~ % 58.71/8.50 | v3_tops_1(v1, all_73_3) | ~ v3_pre_topc(v1, all_73_3) | ~ % 58.71/8.50 | m1_subset_1(v1, v0) | v1_xboole_0(v1)) & ! [v1: $i] : ( ~ $i(v1) % 58.71/8.50 | | ~ v3_tops_1(v1, all_73_3) | ~ v3_pre_topc(v1, all_73_3) | ~ % 58.71/8.50 | m1_subset_1(v1, v0) | v5_membered(v1)) & ! [v1: $i] : ( ~ $i(v1) % 58.71/8.50 | | ~ v3_tops_1(v1, all_73_3) | ~ v3_pre_topc(v1, all_73_3) | ~ % 58.71/8.50 | m1_subset_1(v1, v0) | v4_membered(v1)) & ! [v1: $i] : ( ~ $i(v1) % 58.71/8.50 | | ~ v3_tops_1(v1, all_73_3) | ~ v3_pre_topc(v1, all_73_3) | ~ % 58.71/8.50 | m1_subset_1(v1, v0) | v3_membered(v1)) & ! [v1: $i] : ( ~ $i(v1) % 58.71/8.50 | | ~ v3_tops_1(v1, all_73_3) | ~ v3_pre_topc(v1, all_73_3) | ~ % 58.71/8.50 | m1_subset_1(v1, v0) | v2_membered(v1)) & ! [v1: $i] : ( ~ $i(v1) % 58.71/8.50 | | ~ v3_tops_1(v1, all_73_3) | ~ v3_pre_topc(v1, all_73_3) | ~ % 58.71/8.50 | m1_subset_1(v1, v0) | v1_membered(v1))) % 58.71/8.50 | % 58.71/8.50 | GROUND_INST: instantiating (8) with all_73_3, all_73_2, simplifying with (58), % 58.71/8.50 | (59), (62), (66) gives: % 58.71/8.51 | (103) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ( % 58.71/8.51 | ~ $i(v1) | ~ v3_tops_1(v1, all_73_3) | ~ m1_subset_1(v1, v0) | % 58.71/8.51 | v2_tops_1(v1, all_73_3))) % 58.71/8.51 | % 58.71/8.51 | GROUND_INST: instantiating (10) with all_73_3, all_73_2, simplifying with % 58.71/8.51 | (58), (59), (62), (66) gives: % 58.71/8.51 | (104) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ( % 58.71/8.51 | ~ $i(v1) | ~ v2_tops_1(v1, all_73_3) | ~ v4_pre_topc(v1, % 58.71/8.51 | all_73_3) | ~ m1_subset_1(v1, v0) | v3_tops_1(v1, all_73_3))) % 58.71/8.51 | % 58.71/8.51 | GROUND_INST: instantiating (6) with all_73_3, all_73_2, simplifying with (58), % 58.71/8.51 | (59), (62), (66) gives: % 58.71/8.51 | (105) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ( % 58.71/8.51 | ~ $i(v1) | ~ v1_xboole_0(v1) | ~ m1_subset_1(v1, v0) | % 58.71/8.51 | v3_tops_1(v1, all_73_3))) % 58.71/8.51 | % 58.71/8.51 | GROUND_INST: instantiating (2) with all_73_3, all_73_2, simplifying with (58), % 58.71/8.51 | (59), (62), (66) gives: % 58.71/8.51 | (106) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ( % 58.71/8.51 | ~ $i(v1) | ~ v1_xboole_0(v1) | ~ m1_subset_1(v1, v0) | % 58.71/8.51 | v4_pre_topc(v1, all_73_3)) & ! [v1: $i] : ( ~ $i(v1) | ~ % 58.71/8.51 | v1_xboole_0(v1) | ~ m1_subset_1(v1, v0) | v3_pre_topc(v1, % 58.71/8.51 | all_73_3))) % 58.71/8.51 | % 58.71/8.51 | GROUND_INST: instantiating (31) with all_73_3, all_73_2, simplifying with % 58.71/8.51 | (59), (62), (66) gives: % 58.71/8.51 | (107) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v1) & % 58.71/8.51 | $i(v0) & v2_tops_1(v1, all_73_3) & v1_xboole_0(v1) & % 58.71/8.51 | v5_membered(v1) & v4_membered(v1) & v3_membered(v1) & % 58.71/8.51 | v2_membered(v1) & v1_membered(v1) & m1_subset_1(v1, v0)) % 58.71/8.51 | % 58.71/8.51 | GROUND_INST: instantiating (43) with all_73_3, all_73_2, simplifying with % 58.71/8.51 | (59), (62), (66) gives: % 58.71/8.51 | (108) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ! % 58.71/8.51 | [v2: $i] : (v2 = v1 | ~ (k6_pre_topc(all_73_3, v1) = v2) | ~ % 58.71/8.51 | $i(v1) | ~ v4_pre_topc(v1, all_73_3) | ~ m1_subset_1(v1, v0)) & % 58.71/8.51 | ! [v1: $i] : ( ~ (k6_pre_topc(all_73_3, v1) = v1) | ~ $i(v1) | ~ % 58.71/8.51 | m1_subset_1(v1, v0) | ~ v2_pre_topc(all_73_3) | v4_pre_topc(v1, % 58.71/8.51 | all_73_3))) % 58.71/8.51 | % 58.71/8.51 | GROUND_INST: instantiating (14) with all_73_3, all_73_2, simplifying with % 58.71/8.51 | (59), (62), (66) gives: % 58.71/8.51 | (109) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ! % 58.71/8.51 | [v2: int] : (v2 = all_73_2 | ~ (k6_pre_topc(all_73_3, v1) = v2) | % 58.71/8.51 | ~ $i(v1) | ~ v1_tops_1(v1, all_73_3) | ~ m1_subset_1(v1, v0)) & % 58.71/8.51 | ! [v1: $i] : ( ~ (k6_pre_topc(all_73_3, v1) = all_73_2) | ~ % 58.71/8.51 | $i(v1) | ~ m1_subset_1(v1, v0) | v1_tops_1(v1, all_73_3))) % 58.71/8.51 | % 58.71/8.51 | GROUND_INST: instantiating (4) with all_73_3, all_73_2, simplifying with (59), % 58.71/8.51 | (62), (66) gives: % 58.71/8.51 | (110) ? [v0: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v0) & ! [v1: $i] : ( % 58.71/8.51 | ~ $i(v1) | ~ v1_xboole_0(v1) | ~ m1_subset_1(v1, v0) | % 58.71/8.51 | v2_tops_1(v1, all_73_3))) % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (81) with fresh symbol all_87_0 gives: % 58.71/8.51 | (111) k2_pre_topc(all_73_3) = all_87_0 & $i(all_87_0) & % 58.71/8.51 | v4_pre_topc(all_87_0, all_73_3) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (111) implies: % 58.71/8.51 | (112) k2_pre_topc(all_73_3) = all_87_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (92) with fresh symbol all_89_0 gives: % 58.71/8.51 | (113) k2_pre_topc(all_65_0) = all_89_0 & u1_struct_0(all_65_0) = all_89_0 & % 58.71/8.51 | $i(all_89_0) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (113) implies: % 58.71/8.51 | (114) u1_struct_0(all_65_0) = all_89_0 % 58.71/8.51 | (115) k2_pre_topc(all_65_0) = all_89_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (89) with fresh symbol all_93_0 gives: % 58.71/8.51 | (116) k2_pre_topc(all_65_0) = all_93_0 & $i(all_93_0) & ~ % 58.71/8.51 | v1_xboole_0(all_93_0) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (116) implies: % 58.71/8.51 | (117) $i(all_93_0) % 58.71/8.51 | (118) k2_pre_topc(all_65_0) = all_93_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (90) with fresh symbol all_95_0 gives: % 58.71/8.51 | (119) u1_struct_0(all_65_0) = all_95_0 & $i(all_95_0) & ~ % 58.71/8.51 | v1_xboole_0(all_95_0) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (119) implies: % 58.71/8.51 | (120) u1_struct_0(all_65_0) = all_95_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (87) with fresh symbol all_97_0 gives: % 58.71/8.51 | (121) k2_pre_topc(all_73_3) = all_97_0 & $i(all_97_0) & v1_tops_1(all_97_0, % 58.71/8.51 | all_73_3) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (121) implies: % 58.71/8.51 | (122) v1_tops_1(all_97_0, all_73_3) % 58.71/8.51 | (123) k2_pre_topc(all_73_3) = all_97_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (80) with fresh symbol all_101_0 gives: % 58.71/8.51 | (124) k2_pre_topc(all_73_3) = all_101_0 & $i(all_101_0) & % 58.71/8.51 | v4_pre_topc(all_101_0, all_73_3) & v3_pre_topc(all_101_0, all_73_3) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (124) implies: % 58.71/8.51 | (125) k2_pre_topc(all_73_3) = all_101_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (101) with fresh symbols all_103_0, all_103_1 gives: % 58.71/8.51 | (126) k1_zfmisc_1(all_73_2) = all_103_1 & $i(all_103_0) & $i(all_103_1) & % 58.71/8.51 | v3_pre_topc(all_103_0, all_73_3) & m1_subset_1(all_103_0, all_103_1) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (126) implies: % 58.71/8.51 | (127) k1_zfmisc_1(all_73_2) = all_103_1 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (100) with fresh symbols all_105_0, all_105_1 gives: % 58.71/8.51 | (128) k1_zfmisc_1(all_73_2) = all_105_1 & $i(all_105_0) & $i(all_105_1) & % 58.71/8.51 | v4_pre_topc(all_105_0, all_73_3) & m1_subset_1(all_105_0, all_105_1) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (128) implies: % 58.71/8.51 | (129) k1_zfmisc_1(all_73_2) = all_105_1 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (105) with fresh symbol all_107_0 gives: % 58.71/8.51 | (130) k1_zfmisc_1(all_73_2) = all_107_0 & $i(all_107_0) & ! [v0: $i] : ( ~ % 58.71/8.51 | $i(v0) | ~ v1_xboole_0(v0) | ~ m1_subset_1(v0, all_107_0) | % 58.71/8.51 | v3_tops_1(v0, all_73_3)) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (130) implies: % 58.71/8.51 | (131) k1_zfmisc_1(all_73_2) = all_107_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (110) with fresh symbol all_110_0 gives: % 58.71/8.51 | (132) k1_zfmisc_1(all_73_2) = all_110_0 & $i(all_110_0) & ! [v0: $i] : ( ~ % 58.71/8.51 | $i(v0) | ~ v1_xboole_0(v0) | ~ m1_subset_1(v0, all_110_0) | % 58.71/8.51 | v2_tops_1(v0, all_73_3)) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (132) implies: % 58.71/8.51 | (133) k1_zfmisc_1(all_73_2) = all_110_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (103) with fresh symbol all_113_0 gives: % 58.71/8.51 | (134) k1_zfmisc_1(all_73_2) = all_113_0 & $i(all_113_0) & ! [v0: $i] : ( ~ % 58.71/8.51 | $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ m1_subset_1(v0, all_113_0) % 58.71/8.51 | | v2_tops_1(v0, all_73_3)) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (134) implies: % 58.71/8.51 | (135) k1_zfmisc_1(all_73_2) = all_113_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (95) with fresh symbols all_116_0, all_116_1 gives: % 58.71/8.51 | (136) k1_zfmisc_1(all_73_2) = all_116_1 & $i(all_116_0) & $i(all_116_1) & % 58.71/8.51 | v4_pre_topc(all_116_0, all_73_3) & m1_subset_1(all_116_0, all_116_1) % 58.71/8.51 | & ~ v1_xboole_0(all_116_0) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (136) implies: % 58.71/8.51 | (137) k1_zfmisc_1(all_73_2) = all_116_1 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (99) with fresh symbols all_118_0, all_118_1 gives: % 58.71/8.51 | (138) k1_zfmisc_1(all_73_2) = all_118_1 & $i(all_118_0) & $i(all_118_1) & % 58.71/8.51 | v4_pre_topc(all_118_0, all_73_3) & v3_pre_topc(all_118_0, all_73_3) & % 58.71/8.51 | m1_subset_1(all_118_0, all_118_1) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (138) implies: % 58.71/8.51 | (139) k1_zfmisc_1(all_73_2) = all_118_1 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (94) with fresh symbols all_122_0, all_122_1 gives: % 58.71/8.51 | (140) k1_zfmisc_1(all_73_2) = all_122_1 & $i(all_122_0) & $i(all_122_1) & % 58.71/8.51 | v4_pre_topc(all_122_0, all_73_3) & v3_pre_topc(all_122_0, all_73_3) & % 58.71/8.51 | m1_subset_1(all_122_0, all_122_1) & ~ v1_xboole_0(all_122_0) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (140) implies: % 58.71/8.51 | (141) k1_zfmisc_1(all_73_2) = all_122_1 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (104) with fresh symbol all_124_0 gives: % 58.71/8.51 | (142) k1_zfmisc_1(all_73_2) = all_124_0 & $i(all_124_0) & ! [v0: $i] : ( ~ % 58.71/8.51 | $i(v0) | ~ v2_tops_1(v0, all_73_3) | ~ v4_pre_topc(v0, all_73_3) % 58.71/8.51 | | ~ m1_subset_1(v0, all_124_0) | v3_tops_1(v0, all_73_3)) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (142) implies: % 58.71/8.51 | (143) k1_zfmisc_1(all_73_2) = all_124_0 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (88) with fresh symbols all_127_0, all_127_1, all_127_2 % 58.71/8.51 | gives: % 58.71/8.51 | (144) u1_struct_0(all_65_0) = all_127_2 & k1_zfmisc_1(all_127_2) = % 58.71/8.51 | all_127_1 & $i(all_127_0) & $i(all_127_1) & $i(all_127_2) & % 58.71/8.51 | m1_subset_1(all_127_0, all_127_1) & ~ v1_xboole_0(all_127_0) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (144) implies: % 58.71/8.51 | (145) m1_subset_1(all_127_0, all_127_1) % 58.71/8.51 | (146) $i(all_127_0) % 58.71/8.51 | (147) k1_zfmisc_1(all_127_2) = all_127_1 % 58.71/8.51 | (148) u1_struct_0(all_65_0) = all_127_2 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (91) with fresh symbols all_129_0, all_129_1, all_129_2 % 58.71/8.51 | gives: % 58.71/8.51 | (149) k2_pre_topc(all_65_0) = all_129_2 & u1_struct_0(all_65_0) = all_129_1 % 58.71/8.51 | & k1_zfmisc_1(all_129_1) = all_129_0 & $i(all_129_0) & $i(all_129_1) % 58.71/8.51 | & $i(all_129_2) & m1_subset_1(all_129_2, all_129_0) % 58.71/8.51 | % 58.71/8.51 | ALPHA: (149) implies: % 58.71/8.51 | (150) $i(all_129_0) % 58.71/8.51 | (151) k1_zfmisc_1(all_129_1) = all_129_0 % 58.71/8.51 | (152) u1_struct_0(all_65_0) = all_129_1 % 58.71/8.51 | (153) k2_pre_topc(all_65_0) = all_129_2 % 58.71/8.51 | % 58.71/8.51 | DELTA: instantiating (74) with fresh symbols all_131_0, all_131_1, all_131_2 % 58.71/8.51 | gives: % 58.71/8.52 | (154) u1_struct_0(all_73_3) = all_131_2 & k1_zfmisc_1(all_131_2) = % 58.71/8.52 | all_131_1 & $i(all_131_0) & $i(all_131_1) & $i(all_131_2) & % 58.71/8.52 | v3_pre_topc(all_131_0, all_73_3) & m1_subset_1(all_131_0, all_131_1) % 58.71/8.52 | % 58.71/8.52 | ALPHA: (154) implies: % 58.71/8.52 | (155) m1_subset_1(all_131_0, all_131_1) % 58.71/8.52 | (156) $i(all_131_1) % 58.71/8.52 | (157) $i(all_131_0) % 58.71/8.52 | (158) k1_zfmisc_1(all_131_2) = all_131_1 % 58.71/8.52 | (159) u1_struct_0(all_73_3) = all_131_2 % 58.71/8.52 | % 58.71/8.52 | DELTA: instantiating (73) with fresh symbols all_133_0, all_133_1, all_133_2 % 58.71/8.52 | gives: % 58.71/8.52 | (160) u1_struct_0(all_73_3) = all_133_2 & k1_zfmisc_1(all_133_2) = % 58.71/8.52 | all_133_1 & $i(all_133_0) & $i(all_133_1) & $i(all_133_2) & % 58.71/8.52 | v4_pre_topc(all_133_0, all_73_3) & m1_subset_1(all_133_0, all_133_1) % 58.71/8.52 | % 58.71/8.52 | ALPHA: (160) implies: % 58.71/8.52 | (161) k1_zfmisc_1(all_133_2) = all_133_1 % 58.71/8.52 | (162) u1_struct_0(all_73_3) = all_133_2 % 58.71/8.52 | % 58.71/8.52 | DELTA: instantiating (84) with fresh symbols all_135_0, all_135_1 gives: % 58.71/8.52 | (163) u1_struct_0(all_73_3) = all_135_1 & k1_zfmisc_1(all_135_1) = % 58.71/8.52 | all_135_0 & $i(all_135_0) & $i(all_135_1) & ! [v0: $i] : ( ~ $i(v0) % 58.71/8.52 | | ~ v1_xboole_0(v0) | ~ m1_subset_1(v0, all_135_0) | % 58.71/8.52 | v2_tops_1(v0, all_73_3)) % 58.71/8.52 | % 58.71/8.52 | ALPHA: (163) implies: % 58.71/8.52 | (164) k1_zfmisc_1(all_135_1) = all_135_0 % 58.71/8.52 | (165) u1_struct_0(all_73_3) = all_135_1 % 58.71/8.52 | % 58.71/8.52 | DELTA: instantiating (78) with fresh symbols all_141_0, all_141_1 gives: % 58.71/8.52 | (166) u1_struct_0(all_73_3) = all_141_1 & k1_zfmisc_1(all_141_1) = % 58.71/8.52 | all_141_0 & $i(all_141_0) & $i(all_141_1) & ! [v0: $i] : ( ~ $i(v0) % 58.71/8.52 | | ~ v1_xboole_0(v0) | ~ m1_subset_1(v0, all_141_0) | % 58.71/8.52 | v3_tops_1(v0, all_73_3)) % 58.71/8.52 | % 58.71/8.52 | ALPHA: (166) implies: % 58.71/8.52 | (167) k1_zfmisc_1(all_141_1) = all_141_0 % 58.71/8.52 | (168) u1_struct_0(all_73_3) = all_141_1 % 58.71/8.52 | % 58.71/8.52 | DELTA: instantiating (96) with fresh symbol all_144_0 gives: % 58.71/8.52 | (169) k1_zfmisc_1(all_73_2) = all_144_0 & $i(all_144_0) & ! [v0: $i] : ! % 58.71/8.52 | [v1: $i] : ! [v2: $i] : ( ~ (k3_tex_4(all_73_3, v0) = v1) | ~ % 58.71/8.52 | (k6_pre_topc(all_73_3, v1) = v2) | ~ $i(v0) | ~ m1_subset_1(v0, % 58.71/8.52 | all_144_0) | (k6_pre_topc(all_73_3, v0) = v2 & $i(v2))) % 58.71/8.52 | % 58.71/8.52 | ALPHA: (169) implies: % 58.71/8.52 | (170) k1_zfmisc_1(all_73_2) = all_144_0 % 58.71/8.52 | % 58.71/8.52 | DELTA: instantiating (68) with fresh symbols all_147_0, all_147_1, all_147_2 % 58.71/8.52 | gives: % 59.16/8.52 | (171) u1_struct_0(all_73_3) = all_147_2 & k1_zfmisc_1(all_147_2) = % 59.16/8.52 | all_147_1 & $i(all_147_0) & $i(all_147_1) & $i(all_147_2) & % 59.16/8.52 | v4_pre_topc(all_147_0, all_73_3) & m1_subset_1(all_147_0, all_147_1) % 59.16/8.52 | & ~ v1_xboole_0(all_147_0) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (171) implies: % 59.16/8.52 | (172) k1_zfmisc_1(all_147_2) = all_147_1 % 59.16/8.52 | (173) u1_struct_0(all_73_3) = all_147_2 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (72) with fresh symbols all_149_0, all_149_1, all_149_2 % 59.16/8.52 | gives: % 59.16/8.52 | (174) u1_struct_0(all_73_3) = all_149_2 & k1_zfmisc_1(all_149_2) = % 59.16/8.52 | all_149_1 & $i(all_149_0) & $i(all_149_1) & $i(all_149_2) & % 59.16/8.52 | v4_pre_topc(all_149_0, all_73_3) & v3_pre_topc(all_149_0, all_73_3) & % 59.16/8.52 | m1_subset_1(all_149_0, all_149_1) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (174) implies: % 59.16/8.52 | (175) k1_zfmisc_1(all_149_2) = all_149_1 % 59.16/8.52 | (176) u1_struct_0(all_73_3) = all_149_2 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (76) with fresh symbols all_151_0, all_151_1 gives: % 59.16/8.52 | (177) u1_struct_0(all_73_3) = all_151_1 & k1_zfmisc_1(all_151_1) = % 59.16/8.52 | all_151_0 & $i(all_151_0) & $i(all_151_1) & ! [v0: $i] : ( ~ $i(v0) % 59.16/8.52 | | ~ v3_tops_1(v0, all_73_3) | ~ m1_subset_1(v0, all_151_0) | % 59.16/8.52 | v2_tops_1(v0, all_73_3)) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (177) implies: % 59.16/8.52 | (178) k1_zfmisc_1(all_151_1) = all_151_0 % 59.16/8.52 | (179) u1_struct_0(all_73_3) = all_151_1 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (67) with fresh symbols all_154_0, all_154_1, all_154_2 % 59.16/8.52 | gives: % 59.16/8.52 | (180) u1_struct_0(all_73_3) = all_154_2 & k1_zfmisc_1(all_154_2) = % 59.16/8.52 | all_154_1 & $i(all_154_0) & $i(all_154_1) & $i(all_154_2) & % 59.16/8.52 | v4_pre_topc(all_154_0, all_73_3) & v3_pre_topc(all_154_0, all_73_3) & % 59.16/8.52 | m1_subset_1(all_154_0, all_154_1) & ~ v1_xboole_0(all_154_0) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (180) implies: % 59.16/8.52 | (181) k1_zfmisc_1(all_154_2) = all_154_1 % 59.16/8.52 | (182) u1_struct_0(all_73_3) = all_154_2 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (77) with fresh symbols all_156_0, all_156_1 gives: % 59.16/8.52 | (183) u1_struct_0(all_73_3) = all_156_1 & k1_zfmisc_1(all_156_1) = % 59.16/8.52 | all_156_0 & $i(all_156_0) & $i(all_156_1) & ! [v0: $i] : ( ~ $i(v0) % 59.16/8.52 | | ~ v2_tops_1(v0, all_73_3) | ~ v4_pre_topc(v0, all_73_3) | ~ % 59.16/8.52 | m1_subset_1(v0, all_156_0) | v3_tops_1(v0, all_73_3)) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (183) implies: % 59.16/8.52 | (184) k1_zfmisc_1(all_156_1) = all_156_0 % 59.16/8.52 | (185) u1_struct_0(all_73_3) = all_156_1 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (106) with fresh symbol all_159_0 gives: % 59.16/8.52 | (186) k1_zfmisc_1(all_73_2) = all_159_0 & $i(all_159_0) & ! [v0: $i] : ( ~ % 59.16/8.52 | $i(v0) | ~ v1_xboole_0(v0) | ~ m1_subset_1(v0, all_159_0) | % 59.16/8.52 | v4_pre_topc(v0, all_73_3)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 59.16/8.52 | v1_xboole_0(v0) | ~ m1_subset_1(v0, all_159_0) | v3_pre_topc(v0, % 59.16/8.52 | all_73_3)) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (186) implies: % 59.16/8.52 | (187) k1_zfmisc_1(all_73_2) = all_159_0 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (69) with fresh symbols all_162_0, all_162_1 gives: % 59.16/8.52 | (188) u1_struct_0(all_73_3) = all_162_1 & k1_zfmisc_1(all_162_1) = % 59.16/8.52 | all_162_0 & $i(all_162_0) & $i(all_162_1) & ! [v0: $i] : ( ~ $i(v0) % 59.16/8.52 | | ~ m1_subset_1(v0, all_162_0) | ? [v1: $i] : ? [v2: $i] : % 59.16/8.52 | (k3_tex_4(all_73_3, v0) = v1 & k6_pre_topc(all_73_3, v1) = v2 & % 59.16/8.52 | k6_pre_topc(all_73_3, v0) = v2 & $i(v2) & $i(v1))) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (188) implies: % 59.16/8.52 | (189) k1_zfmisc_1(all_162_1) = all_162_0 % 59.16/8.52 | (190) u1_struct_0(all_73_3) = all_162_1 % 59.16/8.52 | (191) ! [v0: $i] : ( ~ $i(v0) | ~ m1_subset_1(v0, all_162_0) | ? [v1: % 59.16/8.52 | $i] : ? [v2: $i] : (k3_tex_4(all_73_3, v0) = v1 & % 59.16/8.52 | k6_pre_topc(all_73_3, v1) = v2 & k6_pre_topc(all_73_3, v0) = v2 & % 59.16/8.52 | $i(v2) & $i(v1))) % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (107) with fresh symbols all_165_0, all_165_1 gives: % 59.16/8.52 | (192) k1_zfmisc_1(all_73_2) = all_165_1 & $i(all_165_0) & $i(all_165_1) & % 59.16/8.52 | v2_tops_1(all_165_0, all_73_3) & v1_xboole_0(all_165_0) & % 59.16/8.52 | v5_membered(all_165_0) & v4_membered(all_165_0) & % 59.16/8.52 | v3_membered(all_165_0) & v2_membered(all_165_0) & % 59.16/8.52 | v1_membered(all_165_0) & m1_subset_1(all_165_0, all_165_1) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (192) implies: % 59.16/8.52 | (193) k1_zfmisc_1(all_73_2) = all_165_1 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (109) with fresh symbol all_167_0 gives: % 59.16/8.52 | (194) k1_zfmisc_1(all_73_2) = all_167_0 & $i(all_167_0) & ! [v0: $i] : ! % 59.16/8.52 | [v1: int] : (v1 = all_73_2 | ~ (k6_pre_topc(all_73_3, v0) = v1) | ~ % 59.16/8.52 | $i(v0) | ~ v1_tops_1(v0, all_73_3) | ~ m1_subset_1(v0, % 59.16/8.52 | all_167_0)) & ! [v0: $i] : ( ~ (k6_pre_topc(all_73_3, v0) = % 59.16/8.52 | all_73_2) | ~ $i(v0) | ~ m1_subset_1(v0, all_167_0) | % 59.16/8.52 | v1_tops_1(v0, all_73_3)) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (194) implies: % 59.16/8.52 | (195) k1_zfmisc_1(all_73_2) = all_167_0 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (108) with fresh symbol all_173_0 gives: % 59.16/8.52 | (196) k1_zfmisc_1(all_73_2) = all_173_0 & $i(all_173_0) & ! [v0: $i] : ! % 59.16/8.52 | [v1: $i] : (v1 = v0 | ~ (k6_pre_topc(all_73_3, v0) = v1) | ~ $i(v0) % 59.16/8.52 | | ~ v4_pre_topc(v0, all_73_3) | ~ m1_subset_1(v0, all_173_0)) & % 59.16/8.52 | ! [v0: $i] : ( ~ (k6_pre_topc(all_73_3, v0) = v0) | ~ $i(v0) | ~ % 59.16/8.52 | m1_subset_1(v0, all_173_0) | ~ v2_pre_topc(all_73_3) | % 59.16/8.52 | v4_pre_topc(v0, all_73_3)) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (196) implies: % 59.16/8.52 | (197) k1_zfmisc_1(all_73_2) = all_173_0 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (79) with fresh symbols all_176_0, all_176_1 gives: % 59.16/8.52 | (198) u1_struct_0(all_73_3) = all_176_1 & k1_zfmisc_1(all_176_1) = % 59.16/8.52 | all_176_0 & $i(all_176_0) & $i(all_176_1) & ! [v0: $i] : ( ~ $i(v0) % 59.16/8.52 | | ~ v1_xboole_0(v0) | ~ m1_subset_1(v0, all_176_0) | % 59.16/8.52 | v4_pre_topc(v0, all_73_3)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 59.16/8.52 | v1_xboole_0(v0) | ~ m1_subset_1(v0, all_176_0) | v3_pre_topc(v0, % 59.16/8.52 | all_73_3)) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (198) implies: % 59.16/8.52 | (199) k1_zfmisc_1(all_176_1) = all_176_0 % 59.16/8.52 | (200) u1_struct_0(all_73_3) = all_176_1 % 59.16/8.52 | % 59.16/8.52 | DELTA: instantiating (86) with fresh symbols all_179_0, all_179_1 gives: % 59.16/8.52 | (201) u1_struct_0(all_73_3) = all_179_1 & k1_zfmisc_1(all_179_1) = % 59.16/8.52 | all_179_0 & $i(all_179_0) & $i(all_179_1) & ! [v0: $i] : ( ~ $i(v0) % 59.16/8.52 | | ~ m1_subset_1(v0, all_179_0) | ? [v1: $i] : % 59.16/8.52 | (k6_pre_topc(all_73_3, v0) = v1 & $i(v1) & ( ~ (v1 = all_179_1) | % 59.16/8.52 | v1_tops_1(v0, all_73_3)) & (v1 = all_179_1 | ~ v1_tops_1(v0, % 59.16/8.52 | all_73_3)))) % 59.16/8.52 | % 59.16/8.52 | ALPHA: (201) implies: % 59.16/8.52 | (202) k1_zfmisc_1(all_179_1) = all_179_0 % 59.16/8.52 | (203) u1_struct_0(all_73_3) = all_179_1 % 59.16/8.53 | (204) ! [v0: $i] : ( ~ $i(v0) | ~ m1_subset_1(v0, all_179_0) | ? [v1: % 59.16/8.53 | $i] : (k6_pre_topc(all_73_3, v0) = v1 & $i(v1) & ( ~ (v1 = % 59.16/8.53 | all_179_1) | v1_tops_1(v0, all_73_3)) & (v1 = all_179_1 | ~ % 59.16/8.53 | v1_tops_1(v0, all_73_3)))) % 59.16/8.53 | % 59.16/8.53 | DELTA: instantiating (85) with fresh symbols all_185_0, all_185_1 gives: % 59.16/8.53 | (205) u1_struct_0(all_73_3) = all_185_1 & k1_zfmisc_1(all_185_1) = % 59.16/8.53 | all_185_0 & $i(all_185_0) & $i(all_185_1) & ! [v0: $i] : ( ~ $i(v0) % 59.16/8.53 | | ~ m1_subset_1(v0, all_185_0) | ? [v1: $i] : % 59.16/8.53 | (k6_pre_topc(all_73_3, v0) = v1 & $i(v1) & ( ~ (v1 = v0) | ~ % 59.16/8.53 | v2_pre_topc(all_73_3) | v4_pre_topc(v0, all_73_3)) & (v1 = v0 | % 59.16/8.53 | ~ v4_pre_topc(v0, all_73_3)))) % 59.16/8.53 | % 59.16/8.53 | ALPHA: (205) implies: % 59.16/8.53 | (206) k1_zfmisc_1(all_185_1) = all_185_0 % 59.16/8.53 | (207) u1_struct_0(all_73_3) = all_185_1 % 59.16/8.53 | (208) ! [v0: $i] : ( ~ $i(v0) | ~ m1_subset_1(v0, all_185_0) | ? [v1: % 59.16/8.53 | $i] : (k6_pre_topc(all_73_3, v0) = v1 & $i(v1) & ( ~ (v1 = v0) | % 59.16/8.53 | ~ v2_pre_topc(all_73_3) | v4_pre_topc(v0, all_73_3)) & (v1 = v0 % 59.16/8.53 | | ~ v4_pre_topc(v0, all_73_3)))) % 59.16/8.53 | % 59.16/8.53 | DELTA: instantiating (83) with fresh symbols all_190_0, all_190_1, all_190_2 % 59.16/8.53 | gives: % 59.16/8.53 | (209) u1_struct_0(all_73_3) = all_190_2 & k1_zfmisc_1(all_190_2) = % 59.16/8.53 | all_190_1 & $i(all_190_0) & $i(all_190_1) & $i(all_190_2) & % 59.16/8.53 | v2_tops_1(all_190_0, all_73_3) & v1_xboole_0(all_190_0) & % 59.16/8.53 | v5_membered(all_190_0) & v4_membered(all_190_0) & % 59.16/8.53 | v3_membered(all_190_0) & v2_membered(all_190_0) & % 59.16/8.53 | v1_membered(all_190_0) & m1_subset_1(all_190_0, all_190_1) % 59.16/8.53 | % 59.16/8.53 | ALPHA: (209) implies: % 59.16/8.53 | (210) k1_zfmisc_1(all_190_2) = all_190_1 % 59.16/8.53 | (211) u1_struct_0(all_73_3) = all_190_2 % 59.16/8.53 | % 59.16/8.53 | DELTA: instantiating (70) with fresh symbols all_192_0, all_192_1 gives: % 59.16/8.53 | (212) u1_struct_0(all_73_3) = all_192_1 & k1_zfmisc_1(all_192_1) = % 59.16/8.53 | all_192_0 & $i(all_192_0) & $i(all_192_1) & ! [v0: $i] : ( ~ $i(v0) % 59.16/8.53 | | ~ m1_subset_1(v0, all_192_0) | ? [v1: $i] : (k3_tex_4(all_73_3, % 59.16/8.53 | v0) = v1 & $i(v1) & ( ~ (v1 = all_192_1) | ~ v1_tsp_1(v0, % 59.16/8.53 | all_73_3) | v1_tsp_2(v0, all_73_3)) & ( ~ v1_tsp_2(v0, % 59.16/8.53 | all_73_3) | (v1 = all_192_1 & v1_tsp_1(v0, all_73_3))))) % 59.16/8.53 | % 59.16/8.53 | ALPHA: (212) implies: % 59.16/8.53 | (213) k1_zfmisc_1(all_192_1) = all_192_0 % 59.16/8.53 | (214) u1_struct_0(all_73_3) = all_192_1 % 59.16/8.53 | (215) ! [v0: $i] : ( ~ $i(v0) | ~ m1_subset_1(v0, all_192_0) | ? [v1: % 59.16/8.53 | $i] : (k3_tex_4(all_73_3, v0) = v1 & $i(v1) & ( ~ (v1 = % 59.16/8.53 | all_192_1) | ~ v1_tsp_1(v0, all_73_3) | v1_tsp_2(v0, % 59.16/8.53 | all_73_3)) & ( ~ v1_tsp_2(v0, all_73_3) | (v1 = all_192_1 & % 59.16/8.53 | v1_tsp_1(v0, all_73_3))))) % 59.16/8.53 | % 59.16/8.53 | DELTA: instantiating (98) with fresh symbols all_195_0, all_195_1 gives: % 59.16/8.53 | (216) k1_zfmisc_1(all_73_2) = all_195_1 & $i(all_195_0) & $i(all_195_1) & % 59.16/8.53 | v3_tops_1(all_195_0, all_73_3) & v2_tops_1(all_195_0, all_73_3) & % 59.16/8.53 | v4_pre_topc(all_195_0, all_73_3) & v3_pre_topc(all_195_0, all_73_3) & % 59.16/8.53 | v1_xboole_0(all_195_0) & v5_membered(all_195_0) & % 59.16/8.53 | v4_membered(all_195_0) & v3_membered(all_195_0) & % 59.16/8.53 | v2_membered(all_195_0) & v1_membered(all_195_0) & % 59.16/8.53 | m1_subset_1(all_195_0, all_195_1) % 59.16/8.53 | % 59.16/8.53 | ALPHA: (216) implies: % 59.16/8.53 | (217) k1_zfmisc_1(all_73_2) = all_195_1 % 59.16/8.53 | % 59.16/8.53 | DELTA: instantiating (71) with fresh symbols all_197_0, all_197_1, all_197_2 % 59.16/8.53 | gives: % 59.16/8.53 | (218) u1_struct_0(all_73_3) = all_197_2 & k1_zfmisc_1(all_197_2) = % 59.16/8.53 | all_197_1 & $i(all_197_0) & $i(all_197_1) & $i(all_197_2) & % 59.16/8.53 | v3_tops_1(all_197_0, all_73_3) & v2_tops_1(all_197_0, all_73_3) & % 59.16/8.53 | v4_pre_topc(all_197_0, all_73_3) & v3_pre_topc(all_197_0, all_73_3) & % 59.16/8.53 | v1_xboole_0(all_197_0) & v5_membered(all_197_0) & % 59.16/8.53 | v4_membered(all_197_0) & v3_membered(all_197_0) & % 59.16/8.53 | v2_membered(all_197_0) & v1_membered(all_197_0) & % 59.16/8.53 | m1_subset_1(all_197_0, all_197_1) % 59.16/8.53 | % 59.16/8.53 | ALPHA: (218) implies: % 59.16/8.53 | (219) k1_zfmisc_1(all_197_2) = all_197_1 % 59.16/8.53 | (220) u1_struct_0(all_73_3) = all_197_2 % 59.16/8.53 | % 59.16/8.53 | DELTA: instantiating (97) with fresh symbol all_199_0 gives: % 59.16/8.53 | (221) k1_zfmisc_1(all_73_2) = all_199_0 & $i(all_199_0) & ! [v0: $i] : ! % 59.16/8.53 | [v1: int] : (v1 = all_73_2 | ~ (k3_tex_4(all_73_3, v0) = v1) | ~ % 59.16/8.53 | $i(v0) | ~ v1_tsp_2(v0, all_73_3) | ~ m1_subset_1(v0, all_199_0)) % 59.16/8.53 | & ! [v0: $i] : ! [v1: $i] : ( ~ (k3_tex_4(all_73_3, v0) = v1) | ~ % 59.16/8.53 | $i(v0) | ~ v1_tsp_2(v0, all_73_3) | ~ m1_subset_1(v0, all_199_0) % 59.16/8.53 | | v1_tsp_1(v0, all_73_3)) & ! [v0: $i] : ( ~ (k3_tex_4(all_73_3, % 59.16/8.53 | v0) = all_73_2) | ~ $i(v0) | ~ v1_tsp_1(v0, all_73_3) | ~ % 59.16/8.53 | m1_subset_1(v0, all_199_0) | v1_tsp_2(v0, all_73_3)) % 59.16/8.53 | % 59.16/8.53 | ALPHA: (221) implies: % 59.16/8.53 | (222) k1_zfmisc_1(all_73_2) = all_199_0 % 59.16/8.53 | % 59.16/8.53 | DELTA: instantiating (102) with fresh symbol all_202_0 gives: % 59.16/8.53 | (223) k1_zfmisc_1(all_73_2) = all_202_0 & $i(all_202_0) & ! [v0: $i] : ( ~ % 59.16/8.53 | $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, all_73_3) % 59.16/8.53 | | ~ m1_subset_1(v0, all_202_0) | v2_tops_1(v0, all_73_3)) & ! % 59.16/8.53 | [v0: $i] : ( ~ $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ % 59.16/8.53 | v3_pre_topc(v0, all_73_3) | ~ m1_subset_1(v0, all_202_0) | % 59.16/8.53 | v4_pre_topc(v0, all_73_3)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 59.16/8.53 | v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, all_73_3) | ~ % 59.16/8.53 | m1_subset_1(v0, all_202_0) | v1_xboole_0(v0)) & ! [v0: $i] : ( ~ % 59.16/8.53 | $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, all_73_3) % 59.16/8.53 | | ~ m1_subset_1(v0, all_202_0) | v5_membered(v0)) & ! [v0: $i] : % 59.16/8.53 | ( ~ $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, % 59.16/8.53 | all_73_3) | ~ m1_subset_1(v0, all_202_0) | v4_membered(v0)) & ! % 59.16/8.53 | [v0: $i] : ( ~ $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ % 59.16/8.53 | v3_pre_topc(v0, all_73_3) | ~ m1_subset_1(v0, all_202_0) | % 59.16/8.53 | v3_membered(v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ v3_tops_1(v0, % 59.16/8.53 | all_73_3) | ~ v3_pre_topc(v0, all_73_3) | ~ m1_subset_1(v0, % 59.16/8.53 | all_202_0) | v2_membered(v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 59.16/8.53 | v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, all_73_3) | ~ % 59.16/8.53 | m1_subset_1(v0, all_202_0) | v1_membered(v0)) % 59.16/8.53 | % 59.16/8.53 | ALPHA: (223) implies: % 59.16/8.53 | (224) k1_zfmisc_1(all_73_2) = all_202_0 % 59.16/8.53 | % 59.16/8.53 | DELTA: instantiating (75) with fresh symbols all_205_0, all_205_1 gives: % 59.16/8.53 | (225) u1_struct_0(all_73_3) = all_205_1 & k1_zfmisc_1(all_205_1) = % 59.16/8.53 | all_205_0 & $i(all_205_0) & $i(all_205_1) & ! [v0: $i] : ( ~ $i(v0) % 59.16/8.53 | | ~ v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, all_73_3) | ~ % 59.16/8.53 | m1_subset_1(v0, all_205_0) | v2_tops_1(v0, all_73_3)) & ! [v0: $i] % 59.16/8.53 | : ( ~ $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, % 59.16/8.53 | all_73_3) | ~ m1_subset_1(v0, all_205_0) | v4_pre_topc(v0, % 59.16/8.53 | all_73_3)) & ! [v0: $i] : ( ~ $i(v0) | ~ v3_tops_1(v0, % 59.16/8.53 | all_73_3) | ~ v3_pre_topc(v0, all_73_3) | ~ m1_subset_1(v0, % 59.16/8.53 | all_205_0) | v1_xboole_0(v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 59.16/8.53 | v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, all_73_3) | ~ % 59.16/8.53 | m1_subset_1(v0, all_205_0) | v5_membered(v0)) & ! [v0: $i] : ( ~ % 59.16/8.53 | $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, all_73_3) % 59.16/8.53 | | ~ m1_subset_1(v0, all_205_0) | v4_membered(v0)) & ! [v0: $i] : % 59.16/8.53 | ( ~ $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ v3_pre_topc(v0, % 59.16/8.53 | all_73_3) | ~ m1_subset_1(v0, all_205_0) | v3_membered(v0)) & ! % 59.16/8.53 | [v0: $i] : ( ~ $i(v0) | ~ v3_tops_1(v0, all_73_3) | ~ % 59.16/8.53 | v3_pre_topc(v0, all_73_3) | ~ m1_subset_1(v0, all_205_0) | % 59.16/8.53 | v2_membered(v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ v3_tops_1(v0, % 59.16/8.53 | all_73_3) | ~ v3_pre_topc(v0, all_73_3) | ~ m1_subset_1(v0, % 59.16/8.53 | all_205_0) | v1_membered(v0)) % 59.16/8.53 | % 59.16/8.53 | ALPHA: (225) implies: % 59.16/8.53 | (226) k1_zfmisc_1(all_205_1) = all_205_0 % 59.16/8.53 | (227) u1_struct_0(all_73_3) = all_205_1 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_73_1, all_107_0, all_73_2, % 59.16/8.53 | simplifying with (65), (131) gives: % 59.16/8.53 | (228) all_107_0 = all_73_1 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_107_0, all_110_0, all_73_2, % 59.16/8.53 | simplifying with (131), (133) gives: % 59.16/8.53 | (229) all_110_0 = all_107_0 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_103_1, all_110_0, all_73_2, % 59.16/8.53 | simplifying with (127), (133) gives: % 59.16/8.53 | (230) all_110_0 = all_103_1 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_107_0, all_118_1, all_73_2, % 59.16/8.53 | simplifying with (131), (139) gives: % 59.16/8.53 | (231) all_118_1 = all_107_0 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_118_1, all_165_1, all_73_2, % 59.16/8.53 | simplifying with (139), (193) gives: % 59.16/8.53 | (232) all_165_1 = all_118_1 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_116_1, all_165_1, all_73_2, % 59.16/8.53 | simplifying with (137), (193) gives: % 59.16/8.53 | (233) all_165_1 = all_116_1 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_118_1, all_167_0, all_73_2, % 59.16/8.53 | simplifying with (139), (195) gives: % 59.16/8.53 | (234) all_167_0 = all_118_1 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_113_0, all_167_0, all_73_2, % 59.16/8.53 | simplifying with (135), (195) gives: % 59.16/8.53 | (235) all_167_0 = all_113_0 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_144_0, all_173_0, all_73_2, % 59.16/8.53 | simplifying with (170), (197) gives: % 59.16/8.53 | (236) all_173_0 = all_144_0 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_167_0, all_195_1, all_73_2, % 59.16/8.53 | simplifying with (195), (217) gives: % 59.16/8.53 | (237) all_195_1 = all_167_0 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_124_0, all_195_1, all_73_2, % 59.16/8.53 | simplifying with (143), (217) gives: % 59.16/8.53 | (238) all_195_1 = all_124_0 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_173_0, all_199_0, all_73_2, % 59.16/8.53 | simplifying with (197), (222) gives: % 59.16/8.53 | (239) all_199_0 = all_173_0 % 59.16/8.53 | % 59.16/8.53 | GROUND_INST: instantiating (46) with all_159_0, all_199_0, all_73_2, % 59.16/8.53 | simplifying with (187), (222) gives: % 59.16/8.54 | (240) all_199_0 = all_159_0 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (46) with all_122_1, all_199_0, all_73_2, % 59.16/8.54 | simplifying with (141), (222) gives: % 59.16/8.54 | (241) all_199_0 = all_122_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (46) with all_118_1, all_199_0, all_73_2, % 59.16/8.54 | simplifying with (139), (222) gives: % 59.16/8.54 | (242) all_199_0 = all_118_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (46) with all_199_0, all_202_0, all_73_2, % 59.16/8.54 | simplifying with (222), (224) gives: % 59.16/8.54 | (243) all_202_0 = all_199_0 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (46) with all_105_1, all_202_0, all_73_2, % 59.16/8.54 | simplifying with (129), (224) gives: % 59.16/8.54 | (244) all_202_0 = all_105_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_89_0, all_127_2, all_65_0, % 59.16/8.54 | simplifying with (114), (148) gives: % 59.16/8.54 | (245) all_127_2 = all_89_0 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_127_2, all_129_1, all_65_0, % 59.16/8.54 | simplifying with (148), (152) gives: % 59.16/8.54 | (246) all_129_1 = all_127_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_95_0, all_129_1, all_65_0, % 59.16/8.54 | simplifying with (120), (152) gives: % 59.16/8.54 | (247) all_129_1 = all_95_0 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_133_2, all_135_1, all_73_3, % 59.16/8.54 | simplifying with (162), (165) gives: % 59.16/8.54 | (248) all_135_1 = all_133_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_73_2, all_147_2, all_73_3, % 59.16/8.54 | simplifying with (66), (173) gives: % 59.16/8.54 | (249) all_147_2 = all_73_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_135_1, all_147_2, all_73_3, % 59.16/8.54 | simplifying with (165), (173) gives: % 59.16/8.54 | (250) all_147_2 = all_135_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_151_1, all_156_1, all_73_3, % 59.16/8.54 | simplifying with (179), (185) gives: % 59.16/8.54 | (251) all_156_1 = all_151_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_149_2, all_156_1, all_73_3, % 59.16/8.54 | simplifying with (176), (185) gives: % 59.16/8.54 | (252) all_156_1 = all_149_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_147_2, all_156_1, all_73_3, % 59.16/8.54 | simplifying with (173), (185) gives: % 59.16/8.54 | (253) all_156_1 = all_147_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_176_1, all_185_1, all_73_3, % 59.16/8.54 | simplifying with (200), (207) gives: % 59.16/8.54 | (254) all_185_1 = all_176_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_154_2, all_190_2, all_73_3, % 59.16/8.54 | simplifying with (182), (211) gives: % 59.16/8.54 | (255) all_190_2 = all_154_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_151_1, all_190_2, all_73_3, % 59.16/8.54 | simplifying with (179), (211) gives: % 59.16/8.54 | (256) all_190_2 = all_151_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_190_2, all_192_1, all_73_3, % 59.16/8.54 | simplifying with (211), (214) gives: % 59.16/8.54 | (257) all_192_1 = all_190_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_179_1, all_192_1, all_73_3, % 59.16/8.54 | simplifying with (203), (214) gives: % 59.16/8.54 | (258) all_192_1 = all_179_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_176_1, all_192_1, all_73_3, % 59.16/8.54 | simplifying with (200), (214) gives: % 59.16/8.54 | (259) all_192_1 = all_176_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_162_1, all_192_1, all_73_3, % 59.16/8.54 | simplifying with (190), (214) gives: % 59.16/8.54 | (260) all_192_1 = all_162_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_185_1, all_197_2, all_73_3, % 59.16/8.54 | simplifying with (207), (220) gives: % 59.16/8.54 | (261) all_197_2 = all_185_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_141_1, all_197_2, all_73_3, % 59.16/8.54 | simplifying with (168), (220) gives: % 59.16/8.54 | (262) all_197_2 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_133_2, all_205_1, all_73_3, % 59.16/8.54 | simplifying with (162), (227) gives: % 59.16/8.54 | (263) all_205_1 = all_133_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (47) with all_131_2, all_205_1, all_73_3, % 59.16/8.54 | simplifying with (159), (227) gives: % 59.16/8.54 | (264) all_205_1 = all_131_2 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (48) with all_93_0, all_129_2, all_65_0, % 59.16/8.54 | simplifying with (118), (153) gives: % 59.16/8.54 | (265) all_129_2 = all_93_0 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (48) with all_89_0, all_129_2, all_65_0, % 59.16/8.54 | simplifying with (115), (153) gives: % 59.16/8.54 | (266) all_129_2 = all_89_0 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (48) with all_97_0, all_101_0, all_73_3, % 59.16/8.54 | simplifying with (123), (125) gives: % 59.16/8.54 | (267) all_101_0 = all_97_0 % 59.16/8.54 | % 59.16/8.54 | GROUND_INST: instantiating (48) with all_87_0, all_101_0, all_73_3, % 59.16/8.54 | simplifying with (112), (125) gives: % 59.16/8.54 | (268) all_101_0 = all_87_0 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (263), (264) imply: % 59.16/8.54 | (269) all_133_2 = all_131_2 % 59.16/8.54 | % 59.16/8.54 | SIMP: (269) implies: % 59.16/8.54 | (270) all_133_2 = all_131_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (243), (244) imply: % 59.16/8.54 | (271) all_199_0 = all_105_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (271) implies: % 59.16/8.54 | (272) all_199_0 = all_105_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (240), (272) imply: % 59.16/8.54 | (273) all_159_0 = all_105_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (240), (242) imply: % 59.16/8.54 | (274) all_159_0 = all_118_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (240), (241) imply: % 59.16/8.54 | (275) all_159_0 = all_122_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (239), (240) imply: % 59.16/8.54 | (276) all_173_0 = all_159_0 % 59.16/8.54 | % 59.16/8.54 | SIMP: (276) implies: % 59.16/8.54 | (277) all_173_0 = all_159_0 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (261), (262) imply: % 59.16/8.54 | (278) all_185_1 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (278) implies: % 59.16/8.54 | (279) all_185_1 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (237), (238) imply: % 59.16/8.54 | (280) all_167_0 = all_124_0 % 59.16/8.54 | % 59.16/8.54 | SIMP: (280) implies: % 59.16/8.54 | (281) all_167_0 = all_124_0 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (258), (259) imply: % 59.16/8.54 | (282) all_179_1 = all_176_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (257), (258) imply: % 59.16/8.54 | (283) all_190_2 = all_179_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (283) implies: % 59.16/8.54 | (284) all_190_2 = all_179_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (258), (260) imply: % 59.16/8.54 | (285) all_179_1 = all_162_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (255), (284) imply: % 59.16/8.54 | (286) all_179_1 = all_154_2 % 59.16/8.54 | % 59.16/8.54 | SIMP: (286) implies: % 59.16/8.54 | (287) all_179_1 = all_154_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (255), (256) imply: % 59.16/8.54 | (288) all_154_2 = all_151_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (254), (279) imply: % 59.16/8.54 | (289) all_176_1 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (289) implies: % 59.16/8.54 | (290) all_176_1 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (282), (285) imply: % 59.16/8.54 | (291) all_176_1 = all_162_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (291) implies: % 59.16/8.54 | (292) all_176_1 = all_162_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (285), (287) imply: % 59.16/8.54 | (293) all_162_1 = all_154_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (290), (292) imply: % 59.16/8.54 | (294) all_162_1 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (294) implies: % 59.16/8.54 | (295) all_162_1 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (236), (277) imply: % 59.16/8.54 | (296) all_159_0 = all_144_0 % 59.16/8.54 | % 59.16/8.54 | SIMP: (296) implies: % 59.16/8.54 | (297) all_159_0 = all_144_0 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (235), (281) imply: % 59.16/8.54 | (298) all_124_0 = all_113_0 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (234), (281) imply: % 59.16/8.54 | (299) all_124_0 = all_118_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (232), (233) imply: % 59.16/8.54 | (300) all_118_1 = all_116_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (300) implies: % 59.16/8.54 | (301) all_118_1 = all_116_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (293), (295) imply: % 59.16/8.54 | (302) all_154_2 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (302) implies: % 59.16/8.54 | (303) all_154_2 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (274), (297) imply: % 59.16/8.54 | (304) all_144_0 = all_118_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (275), (297) imply: % 59.16/8.54 | (305) all_144_0 = all_122_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (273), (297) imply: % 59.16/8.54 | (306) all_144_0 = all_105_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (251), (252) imply: % 59.16/8.54 | (307) all_151_1 = all_149_2 % 59.16/8.54 | % 59.16/8.54 | SIMP: (307) implies: % 59.16/8.54 | (308) all_151_1 = all_149_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (252), (253) imply: % 59.16/8.54 | (309) all_149_2 = all_147_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (288), (303) imply: % 59.16/8.54 | (310) all_151_1 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (310) implies: % 59.16/8.54 | (311) all_151_1 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (308), (311) imply: % 59.16/8.54 | (312) all_149_2 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (312) implies: % 59.16/8.54 | (313) all_149_2 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (309), (313) imply: % 59.16/8.54 | (314) all_147_2 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | SIMP: (314) implies: % 59.16/8.54 | (315) all_147_2 = all_141_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (249), (315) imply: % 59.16/8.54 | (316) all_141_1 = all_73_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (250), (315) imply: % 59.16/8.54 | (317) all_141_1 = all_135_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (304), (305) imply: % 59.16/8.54 | (318) all_122_1 = all_118_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (305), (306) imply: % 59.16/8.54 | (319) all_122_1 = all_105_1 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (316), (317) imply: % 59.16/8.54 | (320) all_135_1 = all_73_2 % 59.16/8.54 | % 59.16/8.54 | SIMP: (320) implies: % 59.16/8.54 | (321) all_135_1 = all_73_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (248), (321) imply: % 59.16/8.54 | (322) all_133_2 = all_73_2 % 59.16/8.54 | % 59.16/8.54 | SIMP: (322) implies: % 59.16/8.54 | (323) all_133_2 = all_73_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (270), (323) imply: % 59.16/8.54 | (324) all_131_2 = all_73_2 % 59.16/8.54 | % 59.16/8.54 | SIMP: (324) implies: % 59.16/8.54 | (325) all_131_2 = all_73_2 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (246), (247) imply: % 59.16/8.54 | (326) all_127_2 = all_95_0 % 59.16/8.54 | % 59.16/8.54 | SIMP: (326) implies: % 59.16/8.54 | (327) all_127_2 = all_95_0 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (265), (266) imply: % 59.16/8.54 | (328) all_93_0 = all_89_0 % 59.16/8.54 | % 59.16/8.54 | SIMP: (328) implies: % 59.16/8.54 | (329) all_93_0 = all_89_0 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (245), (327) imply: % 59.16/8.54 | (330) all_95_0 = all_89_0 % 59.16/8.54 | % 59.16/8.54 | COMBINE_EQS: (298), (299) imply: % 59.16/8.55 | (331) all_118_1 = all_113_0 % 59.16/8.55 | % 59.16/8.55 | SIMP: (331) implies: % 59.16/8.55 | (332) all_118_1 = all_113_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (318), (319) imply: % 59.16/8.55 | (333) all_118_1 = all_105_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (333) implies: % 59.16/8.55 | (334) all_118_1 = all_105_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (231), (301) imply: % 59.16/8.55 | (335) all_116_1 = all_107_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (301), (332) imply: % 59.16/8.55 | (336) all_116_1 = all_113_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (301), (334) imply: % 59.16/8.55 | (337) all_116_1 = all_105_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (335), (336) imply: % 59.16/8.55 | (338) all_113_0 = all_107_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (336), (337) imply: % 59.16/8.55 | (339) all_113_0 = all_105_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (338), (339) imply: % 59.16/8.55 | (340) all_107_0 = all_105_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (340) implies: % 59.16/8.55 | (341) all_107_0 = all_105_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (229), (230) imply: % 59.16/8.55 | (342) all_107_0 = all_103_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (342) implies: % 59.16/8.55 | (343) all_107_0 = all_103_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (228), (341) imply: % 59.16/8.55 | (344) all_105_1 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (341), (343) imply: % 59.16/8.55 | (345) all_105_1 = all_103_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (344), (345) imply: % 59.16/8.55 | (346) all_103_1 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (346) implies: % 59.16/8.55 | (347) all_103_1 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (267), (268) imply: % 59.16/8.55 | (348) all_97_0 = all_87_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (247), (330) imply: % 59.16/8.55 | (349) all_129_1 = all_89_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (313), (316) imply: % 59.16/8.55 | (350) all_149_2 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (311), (316) imply: % 59.16/8.55 | (351) all_151_1 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (303), (316) imply: % 59.16/8.55 | (352) all_154_2 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (252), (350) imply: % 59.16/8.55 | (353) all_156_1 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (295), (316) imply: % 59.16/8.55 | (354) all_162_1 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (290), (316) imply: % 59.16/8.55 | (355) all_176_1 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (285), (354) imply: % 59.16/8.55 | (356) all_179_1 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (279), (316) imply: % 59.16/8.55 | (357) all_185_1 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (255), (352) imply: % 59.16/8.55 | (358) all_190_2 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (258), (356) imply: % 59.16/8.55 | (359) all_192_1 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (262), (316) imply: % 59.16/8.55 | (360) all_197_2 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (264), (325) imply: % 59.16/8.55 | (361) all_205_1 = all_73_2 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (226), (361) imply: % 59.16/8.55 | (362) k1_zfmisc_1(all_73_2) = all_205_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (219), (360) imply: % 59.16/8.55 | (363) k1_zfmisc_1(all_73_2) = all_197_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (213), (359) imply: % 59.16/8.55 | (364) k1_zfmisc_1(all_73_2) = all_192_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (210), (358) imply: % 59.16/8.55 | (365) k1_zfmisc_1(all_73_2) = all_190_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (206), (357) imply: % 59.16/8.55 | (366) k1_zfmisc_1(all_73_2) = all_185_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (202), (356) imply: % 59.16/8.55 | (367) k1_zfmisc_1(all_73_2) = all_179_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (199), (355) imply: % 59.16/8.55 | (368) k1_zfmisc_1(all_73_2) = all_176_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (189), (354) imply: % 59.16/8.55 | (369) k1_zfmisc_1(all_73_2) = all_162_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (184), (353) imply: % 59.16/8.55 | (370) k1_zfmisc_1(all_73_2) = all_156_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (181), (352) imply: % 59.16/8.55 | (371) k1_zfmisc_1(all_73_2) = all_154_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (178), (351) imply: % 59.16/8.55 | (372) k1_zfmisc_1(all_73_2) = all_151_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (175), (350) imply: % 59.16/8.55 | (373) k1_zfmisc_1(all_73_2) = all_149_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (172), (249) imply: % 59.16/8.55 | (374) k1_zfmisc_1(all_73_2) = all_147_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (167), (316) imply: % 59.16/8.55 | (375) k1_zfmisc_1(all_73_2) = all_141_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (164), (321) imply: % 59.16/8.55 | (376) k1_zfmisc_1(all_73_2) = all_135_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (161), (323) imply: % 59.16/8.55 | (377) k1_zfmisc_1(all_73_2) = all_133_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (158), (325) imply: % 59.16/8.55 | (378) k1_zfmisc_1(all_73_2) = all_131_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (151), (349) imply: % 59.16/8.55 | (379) k1_zfmisc_1(all_89_0) = all_129_0 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (147), (245) imply: % 59.16/8.55 | (380) k1_zfmisc_1(all_89_0) = all_127_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (117), (329) imply: % 59.16/8.55 | (381) $i(all_89_0) % 59.16/8.55 | % 59.16/8.55 | REDUCE: (122), (348) imply: % 59.16/8.55 | (382) v1_tops_1(all_87_0, all_73_3) % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_133_1, all_135_0, all_73_2, % 59.16/8.55 | simplifying with (376), (377) gives: % 59.16/8.55 | (383) all_135_0 = all_133_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_147_1, all_149_1, all_73_2, % 59.16/8.55 | simplifying with (373), (374) gives: % 59.16/8.55 | (384) all_149_1 = all_147_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_135_0, all_151_0, all_73_2, % 59.16/8.55 | simplifying with (372), (376) gives: % 59.16/8.55 | (385) all_151_0 = all_135_0 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_147_1, all_154_1, all_73_2, % 59.16/8.55 | simplifying with (371), (374) gives: % 59.16/8.55 | (386) all_154_1 = all_147_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_133_1, all_154_1, all_73_2, % 59.16/8.55 | simplifying with (371), (377) gives: % 59.16/8.55 | (387) all_154_1 = all_133_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_149_1, all_156_0, all_73_2, % 59.16/8.55 | simplifying with (370), (373) gives: % 59.16/8.55 | (388) all_156_0 = all_149_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_73_1, all_179_0, all_73_2, % 59.16/8.55 | simplifying with (65), (367) gives: % 59.16/8.55 | (389) all_179_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_151_0, all_179_0, all_73_2, % 59.16/8.55 | simplifying with (367), (372) gives: % 59.16/8.55 | (390) all_179_0 = all_151_0 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_154_1, all_185_0, all_73_2, % 59.16/8.55 | simplifying with (366), (371) gives: % 59.16/8.55 | (391) all_185_0 = all_154_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_141_0, all_185_0, all_73_2, % 59.16/8.55 | simplifying with (366), (375) gives: % 59.16/8.55 | (392) all_185_0 = all_141_0 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_131_1, all_190_1, all_73_2, % 59.16/8.55 | simplifying with (365), (378) gives: % 59.16/8.55 | (393) all_190_1 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_190_1, all_192_0, all_73_2, % 59.16/8.55 | simplifying with (364), (365) gives: % 59.16/8.55 | (394) all_192_0 = all_190_1 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_156_0, all_192_0, all_73_2, % 59.16/8.55 | simplifying with (364), (370) gives: % 59.16/8.55 | (395) all_192_0 = all_156_0 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_192_0, all_197_1, all_73_2, % 59.16/8.55 | simplifying with (363), (364) gives: % 59.16/8.55 | (396) all_197_1 = all_192_0 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_176_0, all_197_1, all_73_2, % 59.16/8.55 | simplifying with (363), (368) gives: % 59.16/8.55 | (397) all_197_1 = all_176_0 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_179_0, all_205_0, all_73_2, % 59.16/8.55 | simplifying with (362), (367) gives: % 59.16/8.55 | (398) all_205_0 = all_179_0 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_162_0, all_205_0, all_73_2, % 59.16/8.55 | simplifying with (362), (369) gives: % 59.16/8.55 | (399) all_205_0 = all_162_0 % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (46) with all_127_1, all_129_0, all_89_0, % 59.16/8.55 | simplifying with (379), (380) gives: % 59.16/8.55 | (400) all_129_0 = all_127_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (398), (399) imply: % 59.16/8.55 | (401) all_179_0 = all_162_0 % 59.16/8.55 | % 59.16/8.55 | SIMP: (401) implies: % 59.16/8.55 | (402) all_179_0 = all_162_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (396), (397) imply: % 59.16/8.55 | (403) all_192_0 = all_176_0 % 59.16/8.55 | % 59.16/8.55 | SIMP: (403) implies: % 59.16/8.55 | (404) all_192_0 = all_176_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (394), (404) imply: % 59.16/8.55 | (405) all_190_1 = all_176_0 % 59.16/8.55 | % 59.16/8.55 | SIMP: (405) implies: % 59.16/8.55 | (406) all_190_1 = all_176_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (395), (404) imply: % 59.16/8.55 | (407) all_176_0 = all_156_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (393), (406) imply: % 59.16/8.55 | (408) all_176_0 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (408) implies: % 59.16/8.55 | (409) all_176_0 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (391), (392) imply: % 59.16/8.55 | (410) all_154_1 = all_141_0 % 59.16/8.55 | % 59.16/8.55 | SIMP: (410) implies: % 59.16/8.55 | (411) all_154_1 = all_141_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (390), (402) imply: % 59.16/8.55 | (412) all_162_0 = all_151_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (389), (402) imply: % 59.16/8.55 | (413) all_162_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (407), (409) imply: % 59.16/8.55 | (414) all_156_0 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (414) implies: % 59.16/8.55 | (415) all_156_0 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (412), (413) imply: % 59.16/8.55 | (416) all_151_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (416) implies: % 59.16/8.55 | (417) all_151_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (388), (415) imply: % 59.16/8.55 | (418) all_149_1 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (418) implies: % 59.16/8.55 | (419) all_149_1 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (387), (411) imply: % 59.16/8.55 | (420) all_141_0 = all_133_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (386), (411) imply: % 59.16/8.55 | (421) all_147_1 = all_141_0 % 59.16/8.55 | % 59.16/8.55 | SIMP: (421) implies: % 59.16/8.55 | (422) all_147_1 = all_141_0 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (385), (417) imply: % 59.16/8.55 | (423) all_135_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (423) implies: % 59.16/8.55 | (424) all_135_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (384), (419) imply: % 59.16/8.55 | (425) all_147_1 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (425) implies: % 59.16/8.55 | (426) all_147_1 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (422), (426) imply: % 59.16/8.55 | (427) all_141_0 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (427) implies: % 59.16/8.55 | (428) all_141_0 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (420), (428) imply: % 59.16/8.55 | (429) all_133_1 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (429) implies: % 59.16/8.55 | (430) all_133_1 = all_131_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (383), (424) imply: % 59.16/8.55 | (431) all_133_1 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (431) implies: % 59.16/8.55 | (432) all_133_1 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (430), (432) imply: % 59.16/8.55 | (433) all_131_1 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | SIMP: (433) implies: % 59.16/8.55 | (434) all_131_1 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (428), (434) imply: % 59.16/8.55 | (435) all_141_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (409), (434) imply: % 59.16/8.55 | (436) all_176_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (392), (435) imply: % 59.16/8.55 | (437) all_185_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | COMBINE_EQS: (404), (436) imply: % 59.16/8.55 | (438) all_192_0 = all_73_1 % 59.16/8.55 | % 59.16/8.55 | REDUCE: (156), (434) imply: % 59.16/8.55 | (439) $i(all_73_1) % 59.16/8.55 | % 59.16/8.55 | REDUCE: (150), (400) imply: % 59.16/8.55 | (440) $i(all_127_1) % 59.16/8.55 | % 59.16/8.55 | REDUCE: (155), (434) imply: % 59.16/8.55 | (441) m1_subset_1(all_131_0, all_73_1) % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (t2_subset) with all_127_0, all_127_1, simplifying % 59.16/8.55 | with (145), (146), (440) gives: % 59.16/8.55 | (442) v1_xboole_0(all_127_1) | r2_hidden(all_127_0, all_127_1) % 59.16/8.55 | % 59.16/8.55 | GROUND_INST: instantiating (t2_subset) with all_131_0, all_73_1, simplifying % 59.16/8.55 | with (157), (439), (441) gives: % 59.16/8.55 | (443) v1_xboole_0(all_73_1) | r2_hidden(all_131_0, all_73_1) % 59.16/8.55 | % 59.16/8.56 | GROUND_INST: instantiating (33) with all_73_3, all_73_2, simplifying with % 59.16/8.56 | (56), (62), (66), (82) gives: % 59.16/8.56 | (444) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_73_2) = v0 & $i(v1) & % 59.16/8.56 | $i(v0) & m1_subset_1(v1, v0) & ~ v1_xboole_0(v1)) % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (32) with all_73_3, simplifying with (56), (62), % 59.16/8.56 | (82) gives: % 59.16/8.56 | (445) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_73_3) = v0 % 59.16/8.56 | & k1_zfmisc_1(v0) = v1 & $i(v2) & $i(v1) & $i(v0) & m1_subset_1(v2, % 59.16/8.56 | v1) & ~ v1_xboole_0(v2)) % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (19) with all_73_3, simplifying with (56), (62), % 59.16/8.56 | (82) gives: % 59.16/8.56 | (446) ? [v0: $i] : (u1_struct_0(all_73_3) = v0 & $i(v0) & ~ % 59.16/8.56 | v1_xboole_0(v0)) % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (17) with all_73_3, simplifying with (62), (82) % 59.16/8.56 | gives: % 59.16/8.56 | (447) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (k2_pre_topc(all_73_3) = v0 % 59.16/8.56 | & u1_struct_0(all_73_3) = v1 & k1_zfmisc_1(v1) = v2 & $i(v2) & % 59.16/8.56 | $i(v1) & $i(v0) & m1_subset_1(v0, v2)) % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (40) with all_73_3, simplifying with (62), (82) % 59.16/8.56 | gives: % 59.16/8.56 | (448) ? [v0: $i] : (k2_pre_topc(all_73_3) = v0 & u1_struct_0(all_73_3) = % 59.16/8.56 | v0 & $i(v0)) % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (33) with all_65_0, all_89_0, simplifying with % 59.16/8.56 | (52), (53), (54), (114) gives: % 59.16/8.56 | (449) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_89_0) = v0 & $i(v1) & % 59.16/8.56 | $i(v0) & m1_subset_1(v1, v0) & ~ v1_xboole_0(v1)) % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (18) with all_73_3, all_87_0, simplifying with % 59.16/8.56 | (62), (82), (112) gives: % 59.16/8.56 | (450) ? [v0: $i] : ? [v1: $i] : (u1_struct_0(all_73_3) = v0 & % 59.16/8.56 | k1_zfmisc_1(v0) = v1 & $i(v1) & $i(v0) & m1_subset_1(all_87_0, v1)) % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (41) with all_73_3, all_87_0, simplifying with % 59.16/8.56 | (62), (82), (112) gives: % 59.16/8.56 | (451) u1_struct_0(all_73_3) = all_87_0 & $i(all_87_0) % 59.16/8.56 | % 59.16/8.56 | ALPHA: (451) implies: % 59.16/8.56 | (452) $i(all_87_0) % 59.16/8.56 | (453) u1_struct_0(all_73_3) = all_87_0 % 59.16/8.56 | % 59.16/8.56 | DELTA: instantiating (446) with fresh symbol all_230_0 gives: % 59.16/8.56 | (454) u1_struct_0(all_73_3) = all_230_0 & $i(all_230_0) & ~ % 59.16/8.56 | v1_xboole_0(all_230_0) % 59.16/8.56 | % 59.16/8.56 | ALPHA: (454) implies: % 59.16/8.56 | (455) ~ v1_xboole_0(all_230_0) % 59.16/8.56 | (456) u1_struct_0(all_73_3) = all_230_0 % 59.16/8.56 | % 59.16/8.56 | DELTA: instantiating (448) with fresh symbol all_232_0 gives: % 59.16/8.56 | (457) k2_pre_topc(all_73_3) = all_232_0 & u1_struct_0(all_73_3) = all_232_0 % 59.16/8.56 | & $i(all_232_0) % 59.16/8.56 | % 59.16/8.56 | ALPHA: (457) implies: % 59.16/8.56 | (458) u1_struct_0(all_73_3) = all_232_0 % 59.16/8.56 | % 59.16/8.56 | DELTA: instantiating (450) with fresh symbols all_238_0, all_238_1 gives: % 59.16/8.56 | (459) u1_struct_0(all_73_3) = all_238_1 & k1_zfmisc_1(all_238_1) = % 59.16/8.56 | all_238_0 & $i(all_238_0) & $i(all_238_1) & m1_subset_1(all_87_0, % 59.16/8.56 | all_238_0) % 59.16/8.56 | % 59.16/8.56 | ALPHA: (459) implies: % 59.16/8.56 | (460) m1_subset_1(all_87_0, all_238_0) % 59.16/8.56 | (461) k1_zfmisc_1(all_238_1) = all_238_0 % 59.16/8.56 | (462) u1_struct_0(all_73_3) = all_238_1 % 59.16/8.56 | % 59.16/8.56 | DELTA: instantiating (444) with fresh symbols all_240_0, all_240_1 gives: % 59.16/8.56 | (463) k1_zfmisc_1(all_73_2) = all_240_1 & $i(all_240_0) & $i(all_240_1) & % 59.16/8.56 | m1_subset_1(all_240_0, all_240_1) & ~ v1_xboole_0(all_240_0) % 59.16/8.56 | % 59.16/8.56 | ALPHA: (463) implies: % 59.16/8.56 | (464) k1_zfmisc_1(all_73_2) = all_240_1 % 59.16/8.56 | % 59.16/8.56 | DELTA: instantiating (449) with fresh symbols all_244_0, all_244_1 gives: % 59.16/8.56 | (465) k1_zfmisc_1(all_89_0) = all_244_1 & $i(all_244_0) & $i(all_244_1) & % 59.16/8.56 | m1_subset_1(all_244_0, all_244_1) & ~ v1_xboole_0(all_244_0) % 59.16/8.56 | % 59.16/8.56 | ALPHA: (465) implies: % 59.16/8.56 | (466) m1_subset_1(all_244_0, all_244_1) % 59.16/8.56 | (467) $i(all_244_1) % 59.16/8.56 | (468) $i(all_244_0) % 59.16/8.56 | (469) k1_zfmisc_1(all_89_0) = all_244_1 % 59.16/8.56 | % 59.16/8.56 | DELTA: instantiating (445) with fresh symbols all_251_0, all_251_1, all_251_2 % 59.16/8.56 | gives: % 59.16/8.56 | (470) u1_struct_0(all_73_3) = all_251_2 & k1_zfmisc_1(all_251_2) = % 59.16/8.56 | all_251_1 & $i(all_251_0) & $i(all_251_1) & $i(all_251_2) & % 59.16/8.56 | m1_subset_1(all_251_0, all_251_1) & ~ v1_xboole_0(all_251_0) % 59.16/8.56 | % 59.16/8.56 | ALPHA: (470) implies: % 59.16/8.56 | (471) k1_zfmisc_1(all_251_2) = all_251_1 % 59.16/8.56 | (472) u1_struct_0(all_73_3) = all_251_2 % 59.16/8.56 | % 59.16/8.56 | DELTA: instantiating (447) with fresh symbols all_253_0, all_253_1, all_253_2 % 59.16/8.56 | gives: % 59.16/8.56 | (473) k2_pre_topc(all_73_3) = all_253_2 & u1_struct_0(all_73_3) = all_253_1 % 59.16/8.56 | & k1_zfmisc_1(all_253_1) = all_253_0 & $i(all_253_0) & $i(all_253_1) % 59.16/8.56 | & $i(all_253_2) & m1_subset_1(all_253_2, all_253_0) % 59.16/8.56 | % 59.16/8.56 | ALPHA: (473) implies: % 59.16/8.56 | (474) k1_zfmisc_1(all_253_1) = all_253_0 % 59.16/8.56 | (475) u1_struct_0(all_73_3) = all_253_1 % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (46) with all_73_1, all_240_1, all_73_2, % 59.16/8.56 | simplifying with (65), (464) gives: % 59.16/8.56 | (476) all_240_1 = all_73_1 % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (46) with all_127_1, all_244_1, all_89_0, % 59.16/8.56 | simplifying with (380), (469) gives: % 59.16/8.56 | (477) all_244_1 = all_127_1 % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (47) with all_87_0, all_230_0, all_73_3, % 59.16/8.56 | simplifying with (453), (456) gives: % 59.16/8.56 | (478) all_230_0 = all_87_0 % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (47) with all_73_2, all_251_2, all_73_3, % 59.16/8.56 | simplifying with (66), (472) gives: % 59.16/8.56 | (479) all_251_2 = all_73_2 % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (47) with all_232_0, all_251_2, all_73_3, % 59.16/8.56 | simplifying with (458), (472) gives: % 59.16/8.56 | (480) all_251_2 = all_232_0 % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (47) with all_230_0, all_251_2, all_73_3, % 59.16/8.56 | simplifying with (456), (472) gives: % 59.16/8.56 | (481) all_251_2 = all_230_0 % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (47) with all_251_2, all_253_1, all_73_3, % 59.16/8.56 | simplifying with (472), (475) gives: % 59.16/8.56 | (482) all_253_1 = all_251_2 % 59.16/8.56 | % 59.16/8.56 | GROUND_INST: instantiating (47) with all_238_1, all_253_1, all_73_3, % 59.16/8.56 | simplifying with (462), (475) gives: % 59.16/8.56 | (483) all_253_1 = all_238_1 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (482), (483) imply: % 59.16/8.56 | (484) all_251_2 = all_238_1 % 59.16/8.56 | % 59.16/8.56 | SIMP: (484) implies: % 59.16/8.56 | (485) all_251_2 = all_238_1 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (480), (485) imply: % 59.16/8.56 | (486) all_238_1 = all_232_0 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (481), (485) imply: % 59.16/8.56 | (487) all_238_1 = all_230_0 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (479), (485) imply: % 59.16/8.56 | (488) all_238_1 = all_73_2 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (486), (487) imply: % 59.16/8.56 | (489) all_232_0 = all_230_0 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (486), (488) imply: % 59.16/8.56 | (490) all_232_0 = all_73_2 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (489), (490) imply: % 59.16/8.56 | (491) all_230_0 = all_73_2 % 59.16/8.56 | % 59.16/8.56 | SIMP: (491) implies: % 59.16/8.56 | (492) all_230_0 = all_73_2 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (478), (492) imply: % 59.16/8.56 | (493) all_87_0 = all_73_2 % 59.16/8.56 | % 59.16/8.56 | SIMP: (493) implies: % 59.16/8.56 | (494) all_87_0 = all_73_2 % 59.16/8.56 | % 59.16/8.56 | COMBINE_EQS: (483), (488) imply: % 59.16/8.56 | (495) all_253_1 = all_73_2 % 59.16/8.56 | % 59.16/8.56 | REDUCE: (474), (495) imply: % 59.16/8.56 | (496) k1_zfmisc_1(all_73_2) = all_253_0 % 59.16/8.56 | % 59.16/8.56 | REDUCE: (471), (479) imply: % 59.16/8.56 | (497) k1_zfmisc_1(all_73_2) = all_251_1 % 59.16/8.56 | % 59.16/8.56 | REDUCE: (461), (488) imply: % 59.16/8.56 | (498) k1_zfmisc_1(all_73_2) = all_238_0 % 59.16/8.56 | % 59.16/8.56 | REDUCE: (382), (494) imply: % 59.16/8.56 | (499) v1_tops_1(all_73_2, all_73_3) % 59.16/8.56 | % 59.16/8.56 | REDUCE: (466), (477) imply: % 59.16/8.56 | (500) m1_subset_1(all_244_0, all_127_1) % 59.16/8.56 | % 59.16/8.56 | REDUCE: (460), (494) imply: % 59.16/8.56 | (501) m1_subset_1(all_73_2, all_238_0) % 59.16/8.56 | % 59.16/8.56 | REDUCE: (455), (492) imply: % 59.16/8.56 | (502) ~ v1_xboole_0(all_73_2) % 59.16/8.56 | % 59.16/8.56 | BETA: splitting (93) gives: % 59.16/8.56 | % 59.16/8.56 | Case 1: % 59.16/8.56 | | % 59.16/8.56 | | (503) v1_xboole_0(all_73_2) % 59.16/8.56 | | % 59.16/8.56 | | PRED_UNIFY: (502), (503) imply: % 59.16/8.56 | | (504) $false % 59.16/8.56 | | % 59.16/8.56 | | CLOSE: (504) is inconsistent. % 59.16/8.56 | | % 59.16/8.56 | Case 2: % 59.16/8.56 | | % 59.16/8.56 | | % 59.16/8.56 | | GROUND_INST: instantiating (46) with all_73_1, all_251_1, all_73_2, % 59.16/8.56 | | simplifying with (65), (497) gives: % 59.16/8.56 | | (505) all_251_1 = all_73_1 % 59.16/8.56 | | % 59.16/8.56 | | GROUND_INST: instantiating (46) with all_251_1, all_253_0, all_73_2, % 59.16/8.56 | | simplifying with (496), (497) gives: % 59.16/8.56 | | (506) all_253_0 = all_251_1 % 59.16/8.56 | | % 59.16/8.56 | | GROUND_INST: instantiating (46) with all_238_0, all_253_0, all_73_2, % 59.16/8.56 | | simplifying with (496), (498) gives: % 59.16/8.56 | | (507) all_253_0 = all_238_0 % 59.16/8.56 | | % 59.16/8.56 | | COMBINE_EQS: (506), (507) imply: % 59.16/8.56 | | (508) all_251_1 = all_238_0 % 59.16/8.56 | | % 59.16/8.56 | | SIMP: (508) implies: % 59.16/8.56 | | (509) all_251_1 = all_238_0 % 59.16/8.56 | | % 59.16/8.56 | | COMBINE_EQS: (505), (509) imply: % 59.16/8.56 | | (510) all_238_0 = all_73_1 % 59.16/8.56 | | % 59.16/8.56 | | REDUCE: (501), (510) imply: % 59.16/8.56 | | (511) m1_subset_1(all_73_2, all_73_1) % 59.16/8.56 | | % 59.16/8.56 | | BETA: splitting (443) gives: % 59.16/8.56 | | % 59.16/8.56 | | Case 1: % 59.16/8.56 | | | % 59.16/8.56 | | | (512) v1_xboole_0(all_73_1) % 59.16/8.56 | | | % 59.16/8.56 | | | GROUND_INST: instantiating (fc1_subset_1) with all_73_2, all_73_1, % 59.16/8.56 | | | simplifying with (63), (65), (512) gives: % 59.16/8.56 | | | (513) $false % 59.16/8.56 | | | % 59.16/8.56 | | | CLOSE: (513) is inconsistent. % 59.16/8.56 | | | % 59.16/8.56 | | Case 2: % 59.16/8.56 | | | % 59.16/8.56 | | | % 59.16/8.56 | | | GROUND_INST: instantiating (t2_subset) with all_244_0, all_127_1, % 59.16/8.56 | | | simplifying with (440), (468), (500) gives: % 59.16/8.56 | | | (514) v1_xboole_0(all_127_1) | r2_hidden(all_244_0, all_127_1) % 59.16/8.56 | | | % 59.16/8.56 | | | BETA: splitting (442) gives: % 59.16/8.56 | | | % 59.16/8.56 | | | Case 1: % 59.16/8.56 | | | | % 59.16/8.56 | | | | (515) v1_xboole_0(all_127_1) % 59.16/8.56 | | | | % 59.16/8.57 | | | | GROUND_INST: instantiating (fc1_subset_1) with all_89_0, all_127_1, % 59.16/8.57 | | | | simplifying with (380), (381), (515) gives: % 59.16/8.57 | | | | (516) $false % 59.16/8.57 | | | | % 59.16/8.57 | | | | CLOSE: (516) is inconsistent. % 59.16/8.57 | | | | % 59.16/8.57 | | | Case 2: % 59.16/8.57 | | | | % 59.16/8.57 | | | | (517) ~ v1_xboole_0(all_127_1) % 59.16/8.57 | | | | % 59.16/8.57 | | | | BETA: splitting (514) gives: % 59.16/8.57 | | | | % 59.16/8.57 | | | | Case 1: % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | (518) v1_xboole_0(all_127_1) % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | PRED_UNIFY: (517), (518) imply: % 59.16/8.57 | | | | | (519) $false % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | CLOSE: (519) is inconsistent. % 59.16/8.57 | | | | | % 59.16/8.57 | | | | Case 2: % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | GROUND_INST: instantiating (204) with all_73_2, simplifying with (63) % 59.16/8.57 | | | | | gives: % 59.16/8.57 | | | | | (520) ~ m1_subset_1(all_73_2, all_179_0) | ? [v0: $i] : % 59.16/8.57 | | | | | (k6_pre_topc(all_73_3, all_73_2) = v0 & $i(v0) & ( ~ (v0 = % 59.16/8.57 | | | | | all_179_1) | v1_tops_1(all_73_2, all_73_3)) & (v0 = % 59.16/8.57 | | | | | all_179_1 | ~ v1_tops_1(all_73_2, all_73_3))) % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | GROUND_INST: instantiating (191) with all_73_2, simplifying with (63) % 59.16/8.57 | | | | | gives: % 59.16/8.57 | | | | | (521) ~ m1_subset_1(all_73_2, all_162_0) | ? [v0: $i] : ? [v1: % 59.16/8.57 | | | | | $i] : (k3_tex_4(all_73_3, all_73_2) = v0 & % 59.16/8.57 | | | | | k6_pre_topc(all_73_3, v0) = v1 & k6_pre_topc(all_73_3, % 59.16/8.57 | | | | | all_73_2) = v1 & $i(v1) & $i(v0)) % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | GROUND_INST: instantiating (215) with all_73_0, simplifying with (64) % 59.16/8.57 | | | | | gives: % 59.16/8.57 | | | | | (522) ~ m1_subset_1(all_73_0, all_192_0) | ? [v0: $i] : % 59.16/8.57 | | | | | (k3_tex_4(all_73_3, all_73_0) = v0 & $i(v0) & ( ~ (v0 = % 59.16/8.57 | | | | | all_192_1) | ~ v1_tsp_1(all_73_0, all_73_3) | % 59.16/8.57 | | | | | v1_tsp_2(all_73_0, all_73_3)) & ( ~ v1_tsp_2(all_73_0, % 59.16/8.57 | | | | | all_73_3) | (v0 = all_192_1 & v1_tsp_1(all_73_0, % 59.16/8.57 | | | | | all_73_3)))) % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | GROUND_INST: instantiating (208) with all_73_0, simplifying with (64) % 59.16/8.57 | | | | | gives: % 59.16/8.57 | | | | | (523) ~ m1_subset_1(all_73_0, all_185_0) | ? [v0: $i] : % 59.16/8.57 | | | | | (k6_pre_topc(all_73_3, all_73_0) = v0 & $i(v0) & ( ~ (v0 = % 59.16/8.57 | | | | | all_73_0) | ~ v2_pre_topc(all_73_3) | % 59.16/8.57 | | | | | v4_pre_topc(all_73_0, all_73_3)) & (v0 = all_73_0 | ~ % 59.16/8.57 | | | | | v4_pre_topc(all_73_0, all_73_3))) % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | GROUND_INST: instantiating (204) with all_73_0, simplifying with (64) % 59.16/8.57 | | | | | gives: % 59.16/8.57 | | | | | (524) ~ m1_subset_1(all_73_0, all_179_0) | ? [v0: $i] : % 59.16/8.57 | | | | | (k6_pre_topc(all_73_3, all_73_0) = v0 & $i(v0) & ( ~ (v0 = % 59.16/8.57 | | | | | all_179_1) | v1_tops_1(all_73_0, all_73_3)) & (v0 = % 59.16/8.57 | | | | | all_179_1 | ~ v1_tops_1(all_73_0, all_73_3))) % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | GROUND_INST: instantiating (191) with all_73_0, simplifying with (64) % 59.16/8.57 | | | | | gives: % 59.16/8.57 | | | | | (525) ~ m1_subset_1(all_73_0, all_162_0) | ? [v0: $i] : ? [v1: % 59.16/8.57 | | | | | $i] : (k3_tex_4(all_73_3, all_73_0) = v0 & % 59.16/8.57 | | | | | k6_pre_topc(all_73_3, v0) = v1 & k6_pre_topc(all_73_3, % 59.16/8.57 | | | | | all_73_0) = v1 & $i(v1) & $i(v0)) % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | BETA: splitting (524) gives: % 59.16/8.57 | | | | | % 59.16/8.57 | | | | | Case 1: % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | (526) ~ m1_subset_1(all_73_0, all_179_0) % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | REDUCE: (389), (526) imply: % 59.16/8.57 | | | | | | (527) ~ m1_subset_1(all_73_0, all_73_1) % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | PRED_UNIFY: (60), (527) imply: % 59.16/8.57 | | | | | | (528) $false % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | CLOSE: (528) is inconsistent. % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | Case 2: % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | (529) m1_subset_1(all_73_0, all_179_0) % 59.16/8.57 | | | | | | (530) ? [v0: $i] : (k6_pre_topc(all_73_3, all_73_0) = v0 & % 59.16/8.57 | | | | | | $i(v0) & ( ~ (v0 = all_179_1) | v1_tops_1(all_73_0, % 59.16/8.57 | | | | | | all_73_3)) & (v0 = all_179_1 | ~ v1_tops_1(all_73_0, % 59.16/8.57 | | | | | | all_73_3))) % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | DELTA: instantiating (530) with fresh symbol all_710_0 gives: % 59.16/8.57 | | | | | | (531) k6_pre_topc(all_73_3, all_73_0) = all_710_0 & $i(all_710_0) % 59.16/8.57 | | | | | | & ( ~ (all_710_0 = all_179_1) | v1_tops_1(all_73_0, % 59.16/8.57 | | | | | | all_73_3)) & (all_710_0 = all_179_1 | ~ % 59.16/8.57 | | | | | | v1_tops_1(all_73_0, all_73_3)) % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | ALPHA: (531) implies: % 59.16/8.57 | | | | | | (532) k6_pre_topc(all_73_3, all_73_0) = all_710_0 % 59.16/8.57 | | | | | | (533) ~ (all_710_0 = all_179_1) | v1_tops_1(all_73_0, all_73_3) % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | BETA: splitting (525) gives: % 59.16/8.57 | | | | | | % 59.16/8.57 | | | | | | Case 1: % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | (534) ~ m1_subset_1(all_73_0, all_162_0) % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | REDUCE: (413), (534) imply: % 59.16/8.57 | | | | | | | (535) ~ m1_subset_1(all_73_0, all_73_1) % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | PRED_UNIFY: (60), (535) imply: % 59.16/8.57 | | | | | | | (536) $false % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | CLOSE: (536) is inconsistent. % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | Case 2: % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | (537) m1_subset_1(all_73_0, all_162_0) % 59.16/8.57 | | | | | | | (538) ? [v0: $i] : ? [v1: $i] : (k3_tex_4(all_73_3, all_73_0) % 59.16/8.57 | | | | | | | = v0 & k6_pre_topc(all_73_3, v0) = v1 & % 59.16/8.57 | | | | | | | k6_pre_topc(all_73_3, all_73_0) = v1 & $i(v1) & $i(v0)) % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | DELTA: instantiating (538) with fresh symbols all_725_0, all_725_1 % 59.16/8.57 | | | | | | | gives: % 59.16/8.57 | | | | | | | (539) k3_tex_4(all_73_3, all_73_0) = all_725_1 & % 59.16/8.57 | | | | | | | k6_pre_topc(all_73_3, all_725_1) = all_725_0 & % 59.16/8.57 | | | | | | | k6_pre_topc(all_73_3, all_73_0) = all_725_0 & % 59.16/8.57 | | | | | | | $i(all_725_0) & $i(all_725_1) % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | ALPHA: (539) implies: % 59.16/8.57 | | | | | | | (540) k6_pre_topc(all_73_3, all_73_0) = all_725_0 % 59.16/8.57 | | | | | | | (541) k6_pre_topc(all_73_3, all_725_1) = all_725_0 % 59.16/8.57 | | | | | | | (542) k3_tex_4(all_73_3, all_73_0) = all_725_1 % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | BETA: splitting (523) gives: % 59.16/8.57 | | | | | | | % 59.16/8.57 | | | | | | | Case 1: % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | (543) ~ m1_subset_1(all_73_0, all_185_0) % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | REDUCE: (437), (543) imply: % 59.16/8.57 | | | | | | | | (544) ~ m1_subset_1(all_73_0, all_73_1) % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | PRED_UNIFY: (60), (544) imply: % 59.16/8.57 | | | | | | | | (545) $false % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | CLOSE: (545) is inconsistent. % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | Case 2: % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | (546) m1_subset_1(all_73_0, all_185_0) % 59.16/8.57 | | | | | | | | (547) ? [v0: $i] : (k6_pre_topc(all_73_3, all_73_0) = v0 & % 59.16/8.57 | | | | | | | | $i(v0) & ( ~ (v0 = all_73_0) | ~ % 59.16/8.57 | | | | | | | | v2_pre_topc(all_73_3) | v4_pre_topc(all_73_0, % 59.16/8.57 | | | | | | | | all_73_3)) & (v0 = all_73_0 | ~ % 59.16/8.57 | | | | | | | | v4_pre_topc(all_73_0, all_73_3))) % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | DELTA: instantiating (547) with fresh symbol all_730_0 gives: % 59.16/8.57 | | | | | | | | (548) k6_pre_topc(all_73_3, all_73_0) = all_730_0 & % 59.16/8.57 | | | | | | | | $i(all_730_0) & ( ~ (all_730_0 = all_73_0) | ~ % 59.16/8.57 | | | | | | | | v2_pre_topc(all_73_3) | v4_pre_topc(all_73_0, % 59.16/8.57 | | | | | | | | all_73_3)) & (all_730_0 = all_73_0 | ~ % 59.16/8.57 | | | | | | | | v4_pre_topc(all_73_0, all_73_3)) % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | ALPHA: (548) implies: % 59.16/8.57 | | | | | | | | (549) k6_pre_topc(all_73_3, all_73_0) = all_730_0 % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | BETA: splitting (533) gives: % 59.16/8.57 | | | | | | | | % 59.16/8.57 | | | | | | | | Case 1: % 59.16/8.57 | | | | | | | | | % 59.16/8.57 | | | | | | | | | (550) v1_tops_1(all_73_0, all_73_3) % 59.16/8.57 | | | | | | | | | % 59.16/8.57 | | | | | | | | | PRED_UNIFY: (57), (550) imply: % 59.16/8.57 | | | | | | | | | (551) $false % 59.16/8.57 | | | | | | | | | % 59.16/8.57 | | | | | | | | | CLOSE: (551) is inconsistent. % 59.16/8.57 | | | | | | | | | % 59.16/8.57 | | | | | | | | Case 2: % 59.16/8.57 | | | | | | | | | % 59.16/8.57 | | | | | | | | | (552) ~ (all_710_0 = all_179_1) % 59.16/8.57 | | | | | | | | | % 59.16/8.57 | | | | | | | | | REDUCE: (356), (552) imply: % 59.16/8.57 | | | | | | | | | (553) ~ (all_710_0 = all_73_2) % 59.16/8.57 | | | | | | | | | % 59.16/8.57 | | | | | | | | | BETA: splitting (522) gives: % 59.16/8.57 | | | | | | | | | % 59.16/8.57 | | | | | | | | | Case 1: % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | (554) ~ m1_subset_1(all_73_0, all_192_0) % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | REDUCE: (438), (554) imply: % 59.16/8.57 | | | | | | | | | | (555) ~ m1_subset_1(all_73_0, all_73_1) % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | PRED_UNIFY: (60), (555) imply: % 59.16/8.57 | | | | | | | | | | (556) $false % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | CLOSE: (556) is inconsistent. % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | Case 2: % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | (557) ? [v0: $i] : (k3_tex_4(all_73_3, all_73_0) = v0 & % 59.16/8.57 | | | | | | | | | | $i(v0) & ( ~ (v0 = all_192_1) | ~ % 59.16/8.57 | | | | | | | | | | v1_tsp_1(all_73_0, all_73_3) | % 59.16/8.57 | | | | | | | | | | v1_tsp_2(all_73_0, all_73_3)) & ( ~ % 59.16/8.57 | | | | | | | | | | v1_tsp_2(all_73_0, all_73_3) | (v0 = all_192_1 % 59.16/8.57 | | | | | | | | | | & v1_tsp_1(all_73_0, all_73_3)))) % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | DELTA: instantiating (557) with fresh symbol all_990_0 % 59.16/8.57 | | | | | | | | | | gives: % 59.16/8.57 | | | | | | | | | | (558) k3_tex_4(all_73_3, all_73_0) = all_990_0 & % 59.16/8.57 | | | | | | | | | | $i(all_990_0) & ( ~ (all_990_0 = all_192_1) | ~ % 59.16/8.57 | | | | | | | | | | v1_tsp_1(all_73_0, all_73_3) | v1_tsp_2(all_73_0, % 59.16/8.57 | | | | | | | | | | all_73_3)) & ( ~ v1_tsp_2(all_73_0, all_73_3) | % 59.16/8.57 | | | | | | | | | | (all_990_0 = all_192_1 & v1_tsp_1(all_73_0, % 59.16/8.57 | | | | | | | | | | all_73_3))) % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | ALPHA: (558) implies: % 59.16/8.57 | | | | | | | | | | (559) k3_tex_4(all_73_3, all_73_0) = all_990_0 % 59.16/8.57 | | | | | | | | | | (560) ~ v1_tsp_2(all_73_0, all_73_3) | (all_990_0 = % 59.16/8.57 | | | | | | | | | | all_192_1 & v1_tsp_1(all_73_0, all_73_3)) % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | BETA: splitting (521) gives: % 59.16/8.57 | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | Case 1: % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | (561) ~ m1_subset_1(all_73_2, all_162_0) % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | REDUCE: (413), (561) imply: % 59.16/8.57 | | | | | | | | | | | (562) ~ m1_subset_1(all_73_2, all_73_1) % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | PRED_UNIFY: (511), (562) imply: % 59.16/8.57 | | | | | | | | | | | (563) $false % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | CLOSE: (563) is inconsistent. % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | Case 2: % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | (564) m1_subset_1(all_73_2, all_162_0) % 59.16/8.57 | | | | | | | | | | | (565) ? [v0: $i] : ? [v1: $i] : (k3_tex_4(all_73_3, % 59.16/8.57 | | | | | | | | | | | all_73_2) = v0 & k6_pre_topc(all_73_3, v0) = % 59.16/8.57 | | | | | | | | | | | v1 & k6_pre_topc(all_73_3, all_73_2) = v1 & % 59.16/8.57 | | | | | | | | | | | $i(v1) & $i(v0)) % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | DELTA: instantiating (565) with fresh symbols all_1043_0, % 59.16/8.57 | | | | | | | | | | | all_1043_1 gives: % 59.16/8.57 | | | | | | | | | | | (566) k3_tex_4(all_73_3, all_73_2) = all_1043_1 & % 59.16/8.57 | | | | | | | | | | | k6_pre_topc(all_73_3, all_1043_1) = all_1043_0 & % 59.16/8.57 | | | | | | | | | | | k6_pre_topc(all_73_3, all_73_2) = all_1043_0 & % 59.16/8.57 | | | | | | | | | | | $i(all_1043_0) & $i(all_1043_1) % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | ALPHA: (566) implies: % 59.16/8.57 | | | | | | | | | | | (567) k6_pre_topc(all_73_3, all_73_2) = all_1043_0 % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | BETA: splitting (520) gives: % 59.16/8.57 | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | Case 1: % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | (568) ~ m1_subset_1(all_73_2, all_179_0) % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | REDUCE: (389), (568) imply: % 59.16/8.57 | | | | | | | | | | | | (569) ~ m1_subset_1(all_73_2, all_73_1) % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | PRED_UNIFY: (511), (569) imply: % 59.16/8.57 | | | | | | | | | | | | (570) $false % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | CLOSE: (570) is inconsistent. % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | Case 2: % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | (571) ? [v0: $i] : (k6_pre_topc(all_73_3, all_73_2) = % 59.16/8.57 | | | | | | | | | | | | v0 & $i(v0) & ( ~ (v0 = all_179_1) | % 59.16/8.57 | | | | | | | | | | | | v1_tops_1(all_73_2, all_73_3)) & (v0 = % 59.16/8.57 | | | | | | | | | | | | all_179_1 | ~ v1_tops_1(all_73_2, all_73_3))) % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | DELTA: instantiating (571) with fresh symbol all_1054_0 % 59.16/8.57 | | | | | | | | | | | | gives: % 59.16/8.57 | | | | | | | | | | | | (572) k6_pre_topc(all_73_3, all_73_2) = all_1054_0 & % 59.16/8.57 | | | | | | | | | | | | $i(all_1054_0) & ( ~ (all_1054_0 = all_179_1) | % 59.16/8.57 | | | | | | | | | | | | v1_tops_1(all_73_2, all_73_3)) & (all_1054_0 = % 59.16/8.57 | | | | | | | | | | | | all_179_1 | ~ v1_tops_1(all_73_2, all_73_3)) % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | ALPHA: (572) implies: % 59.16/8.57 | | | | | | | | | | | | (573) k6_pre_topc(all_73_3, all_73_2) = all_1054_0 % 59.16/8.57 | | | | | | | | | | | | (574) all_1054_0 = all_179_1 | ~ v1_tops_1(all_73_2, % 59.16/8.57 | | | | | | | | | | | | all_73_3) % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | BETA: splitting (560) gives: % 59.16/8.57 | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | Case 1: % 59.16/8.57 | | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | | (575) ~ v1_tsp_2(all_73_0, all_73_3) % 59.16/8.57 | | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | | PRED_UNIFY: (61), (575) imply: % 59.16/8.57 | | | | | | | | | | | | | (576) $false % 59.16/8.57 | | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | | CLOSE: (576) is inconsistent. % 59.16/8.57 | | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | Case 2: % 59.16/8.57 | | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | | (577) all_990_0 = all_192_1 & v1_tsp_1(all_73_0, % 59.16/8.57 | | | | | | | | | | | | | all_73_3) % 59.16/8.57 | | | | | | | | | | | | | % 59.16/8.57 | | | | | | | | | | | | | ALPHA: (577) implies: % 59.16/8.58 | | | | | | | | | | | | | (578) all_990_0 = all_192_1 % 59.16/8.58 | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | COMBINE_EQS: (359), (578) imply: % 59.16/8.58 | | | | | | | | | | | | | (579) all_990_0 = all_73_2 % 59.16/8.58 | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | REDUCE: (559), (579) imply: % 59.16/8.58 | | | | | | | | | | | | | (580) k3_tex_4(all_73_3, all_73_0) = all_73_2 % 59.16/8.58 | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | BETA: splitting (574) gives: % 59.16/8.58 | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | Case 1: % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | (581) ~ v1_tops_1(all_73_2, all_73_3) % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | PRED_UNIFY: (499), (581) imply: % 59.16/8.58 | | | | | | | | | | | | | | (582) $false % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | CLOSE: (582) is inconsistent. % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | Case 2: % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | (583) all_1054_0 = all_179_1 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | COMBINE_EQS: (356), (583) imply: % 59.16/8.58 | | | | | | | | | | | | | | (584) all_1054_0 = all_73_2 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | REDUCE: (573), (584) imply: % 59.16/8.58 | | | | | | | | | | | | | | (585) k6_pre_topc(all_73_3, all_73_2) = all_73_2 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (49) with all_73_2, all_1043_0, % 59.16/8.58 | | | | | | | | | | | | | | all_73_2, all_73_3, simplifying with (567), (585) % 59.16/8.58 | | | | | | | | | | | | | | gives: % 59.16/8.58 | | | | | | | | | | | | | | (586) all_1043_0 = all_73_2 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (49) with all_725_0, all_730_0, % 59.16/8.58 | | | | | | | | | | | | | | all_73_0, all_73_3, simplifying with (540), (549) % 59.16/8.58 | | | | | | | | | | | | | | gives: % 59.16/8.58 | | | | | | | | | | | | | | (587) all_730_0 = all_725_0 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (49) with all_710_0, all_730_0, % 59.16/8.58 | | | | | | | | | | | | | | all_73_0, all_73_3, simplifying with (532), (549) % 59.16/8.58 | | | | | | | | | | | | | | gives: % 59.16/8.58 | | | | | | | | | | | | | | (588) all_730_0 = all_710_0 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (50) with all_73_2, all_725_1, % 59.16/8.58 | | | | | | | | | | | | | | all_73_0, all_73_3, simplifying with (542), (580) % 59.16/8.58 | | | | | | | | | | | | | | gives: % 59.16/8.58 | | | | | | | | | | | | | | (589) all_725_1 = all_73_2 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | COMBINE_EQS: (587), (588) imply: % 59.16/8.58 | | | | | | | | | | | | | | (590) all_725_0 = all_710_0 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | SIMP: (590) implies: % 59.16/8.58 | | | | | | | | | | | | | | (591) all_725_0 = all_710_0 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | REDUCE: (541), (589), (591) imply: % 59.16/8.58 | | | | | | | | | | | | | | (592) k6_pre_topc(all_73_3, all_73_2) = all_710_0 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | GROUND_INST: instantiating (49) with all_73_2, all_710_0, % 59.16/8.58 | | | | | | | | | | | | | | all_73_2, all_73_3, simplifying with (585), (592) % 59.16/8.58 | | | | | | | | | | | | | | gives: % 59.16/8.58 | | | | | | | | | | | | | | (593) all_710_0 = all_73_2 % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | REDUCE: (553), (593) imply: % 59.16/8.58 | | | | | | | | | | | | | | (594) $false % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | | CLOSE: (594) is inconsistent. % 59.16/8.58 | | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | | End of split % 59.16/8.58 | | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | | End of split % 59.16/8.58 | | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | | End of split % 59.16/8.58 | | | | | | | | | | | % 59.16/8.58 | | | | | | | | | | End of split % 59.16/8.58 | | | | | | | | | | % 59.16/8.58 | | | | | | | | | End of split % 59.16/8.58 | | | | | | | | | % 59.16/8.58 | | | | | | | | End of split % 59.16/8.58 | | | | | | | | % 59.16/8.58 | | | | | | | End of split % 59.16/8.58 | | | | | | | % 59.16/8.58 | | | | | | End of split % 59.16/8.58 | | | | | | % 59.16/8.58 | | | | | End of split % 59.16/8.58 | | | | | % 59.16/8.58 | | | | End of split % 59.16/8.58 | | | | % 59.16/8.58 | | | End of split % 59.16/8.58 | | | % 59.16/8.58 | | End of split % 59.16/8.58 | | % 59.16/8.58 | End of split % 59.16/8.58 | % 59.16/8.58 End of proof % 59.16/8.58 % SZS output end Proof for theBenchmark % 59.16/8.58 % 59.16/8.58 7912ms %------------------------------------------------------------------------------