%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SET623+3 : TPTP v8.1.2. Released v2.2.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 15:25:42 EDT 2023 % Result : Theorem 47.17s 7.10s % Output : Proof 134.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.10 % Problem : SET623+3 : TPTP v8.1.2. Released v2.2.0. % 0.09/0.10 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.31 % Computer : n002.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Sat Aug 26 14:14:48 EDT 2023 % 0.10/0.31 % CPUTime : % 0.16/0.60 ________ _____ % 0.16/0.60 ___ __ \_________(_)________________________________ % 0.16/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.60 % 0.16/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.60 (2023-06-19) % 0.16/0.60 % 0.16/0.60 (c) Philipp Rümmer, 2009-2023 % 0.16/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.60 Amanda Stjerna. % 0.16/0.60 Free software under BSD-3-Clause. % 0.16/0.60 % 0.16/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.60 % 0.16/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.16/0.61 Running up to 7 provers in parallel. % 0.60/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.60/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.60/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.60/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.60/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.60/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.60/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.53/1.12 Prover 1: Preprocessing ... % 2.53/1.12 Prover 4: Preprocessing ... % 3.01/1.19 Prover 5: Preprocessing ... % 3.01/1.19 Prover 3: Preprocessing ... % 3.01/1.19 Prover 2: Preprocessing ... % 3.01/1.19 Prover 0: Preprocessing ... % 3.01/1.19 Prover 6: Preprocessing ... % 5.93/1.62 Prover 1: Warning: ignoring some quantifiers % 5.93/1.64 Prover 3: Warning: ignoring some quantifiers % 5.93/1.66 Prover 5: Proving ... % 5.93/1.66 Prover 6: Proving ... % 5.93/1.66 Prover 3: Constructing countermodel ... % 5.93/1.67 Prover 1: Constructing countermodel ... % 6.51/1.69 Prover 4: Warning: ignoring some quantifiers % 6.51/1.73 Prover 0: Proving ... % 6.51/1.75 Prover 4: Constructing countermodel ... % 6.51/1.76 Prover 2: Proving ... % 8.18/1.94 Prover 1: gave up % 8.18/1.94 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.18/1.95 Prover 3: gave up % 8.18/1.96 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.75/2.00 Prover 8: Preprocessing ... % 8.75/2.00 Prover 7: Preprocessing ... % 9.36/2.14 Prover 8: Warning: ignoring some quantifiers % 9.36/2.17 Prover 8: Constructing countermodel ... % 9.36/2.19 Prover 7: Warning: ignoring some quantifiers % 9.36/2.21 Prover 7: Constructing countermodel ... % 11.18/2.37 Prover 8: gave up % 11.18/2.37 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 11.81/2.43 Prover 9: Preprocessing ... % 13.47/2.71 Prover 9: Warning: ignoring some quantifiers % 14.03/2.72 Prover 9: Constructing countermodel ... % 47.17/7.10 Prover 0: proved (6454ms) % 47.17/7.10 % 47.17/7.10 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 47.17/7.10 % 47.17/7.10 Prover 9: stopped % 47.17/7.10 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 47.17/7.10 Prover 6: stopped % 47.17/7.10 Prover 2: stopped % 47.17/7.11 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 47.17/7.11 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 47.17/7.11 Prover 5: stopped % 47.17/7.11 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 47.17/7.12 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 47.17/7.14 Prover 13: Preprocessing ... % 47.17/7.14 Prover 10: Preprocessing ... % 47.17/7.15 Prover 11: Preprocessing ... % 47.17/7.16 Prover 16: Preprocessing ... % 47.78/7.23 Prover 19: Preprocessing ... % 47.78/7.26 Prover 13: Warning: ignoring some quantifiers % 47.78/7.26 Prover 13: Constructing countermodel ... % 47.78/7.27 Prover 10: Warning: ignoring some quantifiers % 47.78/7.28 Prover 10: Constructing countermodel ... % 48.50/7.34 Prover 16: Warning: ignoring some quantifiers % 48.50/7.34 Prover 10: gave up % 48.50/7.34 Prover 16: Constructing countermodel ... % 48.50/7.35 Prover 11: Warning: ignoring some quantifiers % 49.18/7.36 Prover 11: Constructing countermodel ... % 49.18/7.36 Prover 13: gave up % 49.18/7.38 Prover 19: Warning: ignoring some quantifiers % 49.32/7.38 Prover 19: Constructing countermodel ... % 49.75/7.46 Prover 19: gave up % 49.75/7.49 Prover 16: gave up % 127.95/26.02 Prover 7: stopped % 132.10/27.60 Prover 4: Found proof (size 558) % 132.10/27.60 Prover 4: proved (26962ms) % 132.41/27.60 Prover 11: stopped % 132.41/27.60 % 132.41/27.60 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 132.41/27.60 % 132.86/27.82 % SZS output start Proof for theBenchmark % 132.86/27.82 Assumptions after simplification: % 132.86/27.82 --------------------------------- % 132.86/27.82 % 132.86/27.82 (associativity_of_intersection) % 132.86/27.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 132.86/27.85 (intersection(v3, v2) = v4) | ~ (intersection(v0, v1) = v3) | ~ $i(v2) | % 132.86/27.85 ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (intersection(v1, v2) = v5 & % 132.86/27.85 intersection(v0, v5) = v4 & $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: $i] % 132.86/27.85 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (intersection(v1, v2) = v3) | % 132.86/27.85 ~ (intersection(v0, v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 132.86/27.85 $i] : (intersection(v5, v2) = v4 & intersection(v0, v1) = v5 & $i(v5) & % 132.86/27.85 $i(v4))) % 132.86/27.85 % 132.86/27.85 (associativity_of_union) % 133.08/27.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 133.08/27.86 (union(v3, v2) = v4) | ~ (union(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 133.08/27.86 $i(v0) | ? [v5: $i] : (union(v1, v2) = v5 & union(v0, v5) = v4 & $i(v5) & % 133.08/27.86 $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 133.08/27.86 $i] : ( ~ (union(v1, v2) = v3) | ~ (union(v0, v3) = v4) | ~ $i(v2) | ~ % 133.08/27.86 $i(v1) | ~ $i(v0) | ? [v5: $i] : (union(v5, v2) = v4 & union(v0, v1) = v5 % 133.08/27.86 & $i(v5) & $i(v4))) % 133.08/27.86 % 133.08/27.86 (commutativity_of_intersection) % 133.08/27.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (intersection(v1, v0) = v2) | ~ % 133.08/27.86 $i(v1) | ~ $i(v0) | (intersection(v0, v1) = v2 & $i(v2))) & ! [v0: $i] : % 133.08/27.86 ! [v1: $i] : ! [v2: $i] : ( ~ (intersection(v0, v1) = v2) | ~ $i(v1) | ~ % 133.08/27.86 $i(v0) | (intersection(v1, v0) = v2 & $i(v2))) % 133.08/27.86 % 133.08/27.86 (commutativity_of_symmetric_difference) % 133.08/27.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (symmetric_difference(v1, v0) = % 133.08/27.86 v2) | ~ $i(v1) | ~ $i(v0) | (symmetric_difference(v0, v1) = v2 & % 133.08/27.87 $i(v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 133.08/27.87 (symmetric_difference(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 133.08/27.87 (symmetric_difference(v1, v0) = v2 & $i(v2))) % 133.08/27.87 % 133.08/27.87 (commutativity_of_union) % 133.08/27.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (union(v1, v0) = v2) | ~ $i(v1) % 133.08/27.87 | ~ $i(v0) | (union(v0, v1) = v2 & $i(v2))) & ! [v0: $i] : ! [v1: $i] : % 133.08/27.87 ! [v2: $i] : ( ~ (union(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | (union(v1, v0) % 133.08/27.87 = v2 & $i(v2))) % 133.08/27.87 % 133.08/27.87 (difference_difference_union1) % 133.08/27.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 133.08/27.87 $i] : ( ~ (intersection(v0, v2) = v4) | ~ (difference(v0, v1) = v3) | ~ % 133.08/27.87 (union(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: $i] : % 133.08/27.87 (difference(v1, v2) = v6 & difference(v0, v6) = v5 & $i(v6) & $i(v5))) & ! % 133.08/27.87 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 133.08/27.87 (difference(v1, v2) = v3) | ~ (difference(v0, v3) = v4) | ~ $i(v2) | ~ % 133.08/27.87 $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : (intersection(v0, v2) = v6 % 133.08/27.87 & difference(v0, v1) = v5 & union(v5, v6) = v4 & $i(v6) & $i(v5) & % 133.08/27.87 $i(v4))) % 133.08/27.87 % 133.08/27.87 (difference_difference_union2) % 133.08/27.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 133.08/27.88 (difference(v3, v2) = v4) | ~ (difference(v0, v1) = v3) | ~ $i(v2) | ~ % 133.08/27.88 $i(v1) | ~ $i(v0) | ? [v5: $i] : (difference(v0, v5) = v4 & union(v1, v2) % 133.08/27.88 = v5 & $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 133.08/27.88 [v3: $i] : ! [v4: $i] : ( ~ (difference(v0, v3) = v4) | ~ (union(v1, v2) = % 133.08/27.88 v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (difference(v5, % 133.08/27.88 v2) = v4 & difference(v0, v1) = v5 & $i(v5) & $i(v4))) % 133.08/27.88 % 133.08/27.88 (difference_distributes_over_union) % 133.08/27.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 133.08/27.88 $i] : ( ~ (difference(v1, v2) = v4) | ~ (difference(v0, v2) = v3) | ~ % 133.08/27.88 (union(v3, v4) = v5) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: $i] : % 133.08/27.88 (difference(v6, v2) = v5 & union(v0, v1) = v6 & $i(v6) & $i(v5))) & ! [v0: % 133.08/27.88 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 133.08/27.88 (difference(v3, v2) = v4) | ~ (union(v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 133.08/27.88 | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : (difference(v1, v2) = v6 & % 133.08/27.88 difference(v0, v2) = v5 & union(v5, v6) = v4 & $i(v6) & $i(v5) & $i(v4))) % 133.08/27.88 % 133.08/27.88 (difference_union_intersection) % 133.08/27.89 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (intersection(v0, v1) = v2) | ~ % 133.08/27.89 $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 133.08/27.89 (difference(v3, v2) = v4 & difference(v1, v0) = v6 & difference(v0, v1) = v5 % 133.08/27.89 & union(v5, v6) = v4 & union(v0, v1) = v3 & $i(v6) & $i(v5) & $i(v4) & % 133.08/27.89 $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (difference(v1, % 133.08/27.89 v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 133.08/27.89 $i] : ? [v6: $i] : (intersection(v0, v1) = v4 & difference(v3, v4) = v5 & % 133.08/27.89 difference(v0, v1) = v6 & union(v6, v2) = v5 & union(v0, v1) = v3 & $i(v6) % 133.08/27.89 & $i(v5) & $i(v4) & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( % 133.08/27.89 ~ (difference(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: % 133.08/27.89 $i] : ? [v5: $i] : ? [v6: $i] : (intersection(v0, v1) = v4 & % 133.08/27.89 difference(v3, v4) = v5 & difference(v1, v0) = v6 & union(v2, v6) = v5 & % 133.08/27.89 union(v0, v1) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) & ! [v0: $i] : % 133.08/27.89 ! [v1: $i] : ! [v2: $i] : ( ~ (union(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 133.08/27.89 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : (intersection(v0, v1) % 133.08/27.89 = v3 & difference(v2, v3) = v4 & difference(v1, v0) = v6 & difference(v0, % 133.08/27.89 v1) = v5 & union(v5, v6) = v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 133.08/27.89 % 133.08/27.89 (prove_th99) % 133.28/27.90 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 133.28/27.90 $i] : ? [v6: $i] : ( ~ (v6 = v4) & symmetric_difference(v3, v2) = v4 & % 133.28/27.90 symmetric_difference(v1, v2) = v5 & symmetric_difference(v0, v5) = v6 & % 133.28/27.90 symmetric_difference(v0, v1) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 133.28/27.90 $i(v2) & $i(v1) & $i(v0)) % 133.28/27.90 % 133.28/27.90 (symmetric_difference_defn) % 133.28/27.90 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (symmetric_difference(v0, v1) = % 133.28/27.90 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : (difference(v1, % 133.28/27.90 v0) = v4 & difference(v0, v1) = v3 & union(v3, v4) = v2 & $i(v4) & % 133.28/27.90 $i(v3) & $i(v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 133.28/27.90 (difference(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: % 133.28/27.90 $i] : (symmetric_difference(v0, v1) = v3 & difference(v0, v1) = v4 & % 133.28/27.90 union(v4, v2) = v3 & $i(v4) & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! % 133.28/27.90 [v2: $i] : ( ~ (difference(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] % 133.28/27.90 : ? [v4: $i] : (symmetric_difference(v0, v1) = v3 & difference(v1, v0) = v4 % 133.28/27.90 & union(v2, v4) = v3 & $i(v4) & $i(v3))) % 133.28/27.90 % 133.28/27.90 (function-axioms) % 133.28/27.91 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 133.28/27.91 [v3: $i] : (v1 = v0 | ~ (member(v3, v2) = v1) | ~ (member(v3, v2) = v0)) & % 133.28/27.91 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 133.28/27.91 $i] : (v1 = v0 | ~ (subset(v3, v2) = v1) | ~ (subset(v3, v2) = v0)) & ! % 133.28/27.91 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 133.28/27.91 (intersection(v3, v2) = v1) | ~ (intersection(v3, v2) = v0)) & ! [v0: $i] % 133.28/27.91 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 133.28/27.91 (symmetric_difference(v3, v2) = v1) | ~ (symmetric_difference(v3, v2) = % 133.28/27.91 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 133.28/27.91 ~ (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) & ! [v0: $i] : % 133.28/27.91 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (union(v3, v2) = v1) | % 133.28/27.91 ~ (union(v3, v2) = v0)) % 133.28/27.91 % 133.28/27.91 Further assumptions not needed in the proof: % 133.28/27.91 -------------------------------------------- % 133.28/27.91 equal_defn, equal_member_defn, reflexivity_of_subset, subset_defn % 133.28/27.91 % 133.28/27.91 Those formulas are unsatisfiable: % 133.28/27.91 --------------------------------- % 133.28/27.91 % 133.28/27.91 Begin of proof % 133.28/27.92 | % 133.28/27.92 | ALPHA: (symmetric_difference_defn) implies: % 133.28/27.92 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (difference(v0, v1) = v2) % 133.28/27.92 | | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : % 133.28/27.92 | (symmetric_difference(v0, v1) = v3 & difference(v1, v0) = v4 & % 133.28/27.92 | union(v2, v4) = v3 & $i(v4) & $i(v3))) % 133.28/27.92 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (difference(v1, v0) = v2) % 133.28/27.92 | | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : % 133.28/27.92 | (symmetric_difference(v0, v1) = v3 & difference(v0, v1) = v4 & % 133.28/27.92 | union(v4, v2) = v3 & $i(v4) & $i(v3))) % 133.28/27.92 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (symmetric_difference(v0, % 133.28/27.93 | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : % 133.28/27.93 | (difference(v1, v0) = v4 & difference(v0, v1) = v3 & union(v3, v4) = % 133.28/27.93 | v2 & $i(v4) & $i(v3) & $i(v2))) % 133.28/27.93 | % 133.28/27.93 | ALPHA: (associativity_of_union) implies: % 133.28/27.93 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 133.28/27.93 | ~ (union(v1, v2) = v3) | ~ (union(v0, v3) = v4) | ~ $i(v2) | ~ % 133.28/27.93 | $i(v1) | ~ $i(v0) | ? [v5: $i] : (union(v5, v2) = v4 & union(v0, % 133.28/27.93 | v1) = v5 & $i(v5) & $i(v4))) % 133.28/27.93 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 133.28/27.93 | ~ (union(v3, v2) = v4) | ~ (union(v0, v1) = v3) | ~ $i(v2) | ~ % 133.28/27.93 | $i(v1) | ~ $i(v0) | ? [v5: $i] : (union(v1, v2) = v5 & union(v0, % 133.28/27.93 | v5) = v4 & $i(v5) & $i(v4))) % 133.28/27.93 | % 133.28/27.93 | ALPHA: (associativity_of_intersection) implies: % 133.28/27.93 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 133.28/27.93 | ~ (intersection(v1, v2) = v3) | ~ (intersection(v0, v3) = v4) | ~ % 133.28/27.93 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (intersection(v5, v2) % 133.28/27.93 | = v4 & intersection(v0, v1) = v5 & $i(v5) & $i(v4))) % 133.28/27.93 | % 133.28/27.93 | ALPHA: (difference_difference_union1) implies: % 133.28/27.93 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 133.28/27.93 | ~ (difference(v1, v2) = v3) | ~ (difference(v0, v3) = v4) | ~ % 133.28/27.93 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : % 133.28/27.93 | (intersection(v0, v2) = v6 & difference(v0, v1) = v5 & union(v5, v6) % 133.28/27.93 | = v4 & $i(v6) & $i(v5) & $i(v4))) % 133.28/27.93 | % 133.28/27.93 | ALPHA: (difference_union_intersection) implies: % 133.49/27.94 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (union(v0, v1) = v2) | ~ % 133.49/27.94 | $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? % 133.49/27.94 | [v6: $i] : (intersection(v0, v1) = v3 & difference(v2, v3) = v4 & % 133.49/27.94 | difference(v1, v0) = v6 & difference(v0, v1) = v5 & union(v5, v6) = % 133.49/27.94 | v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 133.49/27.94 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (difference(v0, v1) = v2) % 133.49/27.94 | | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 133.49/27.94 | ? [v6: $i] : (intersection(v0, v1) = v4 & difference(v3, v4) = v5 & % 133.49/27.94 | difference(v1, v0) = v6 & union(v2, v6) = v5 & union(v0, v1) = v3 & % 133.49/27.94 | $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 133.49/27.94 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (difference(v1, v0) = % 133.49/27.94 | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 133.49/27.94 | $i] : ? [v6: $i] : (intersection(v0, v1) = v4 & difference(v3, % 133.49/27.94 | v4) = v5 & difference(v0, v1) = v6 & union(v6, v2) = v5 & % 133.49/27.94 | union(v0, v1) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 133.49/27.94 | % 133.49/27.94 | ALPHA: (difference_difference_union2) implies: % 133.49/27.95 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 133.49/27.95 | ( ~ (difference(v0, v3) = v4) | ~ (union(v1, v2) = v3) | ~ $i(v2) | % 133.49/27.95 | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (difference(v5, v2) = v4 & % 133.49/27.95 | difference(v0, v1) = v5 & $i(v5) & $i(v4))) % 133.49/27.95 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 133.49/27.95 | ( ~ (difference(v3, v2) = v4) | ~ (difference(v0, v1) = v3) | ~ % 133.49/27.95 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (difference(v0, v5) = % 133.49/27.95 | v4 & union(v1, v2) = v5 & $i(v5) & $i(v4))) % 133.49/27.95 | % 133.49/27.95 | ALPHA: (difference_distributes_over_union) implies: % 133.49/27.95 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 133.49/27.95 | ( ~ (difference(v3, v2) = v4) | ~ (union(v0, v1) = v3) | ~ $i(v2) | % 133.49/27.95 | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : (difference(v1, % 133.49/27.95 | v2) = v6 & difference(v0, v2) = v5 & union(v5, v6) = v4 & $i(v6) % 133.49/27.95 | & $i(v5) & $i(v4))) % 133.49/27.95 | % 133.49/27.95 | ALPHA: (commutativity_of_union) implies: % 133.49/27.95 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (union(v1, v0) = v2) | % 133.49/27.95 | ~ $i(v1) | ~ $i(v0) | (union(v0, v1) = v2 & $i(v2))) % 133.49/27.95 | % 133.49/27.95 | ALPHA: (commutativity_of_intersection) implies: % 133.49/27.95 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (intersection(v1, v0) = % 133.49/27.95 | v2) | ~ $i(v1) | ~ $i(v0) | (intersection(v0, v1) = v2 & % 133.49/27.95 | $i(v2))) % 133.49/27.95 | % 133.49/27.95 | ALPHA: (commutativity_of_symmetric_difference) implies: % 133.49/27.96 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 133.49/27.96 | (symmetric_difference(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | % 133.49/27.96 | (symmetric_difference(v0, v1) = v2 & $i(v2))) % 133.49/27.96 | % 133.49/27.96 | ALPHA: (function-axioms) implies: % 133.49/27.96 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 133.49/27.96 | (union(v3, v2) = v1) | ~ (union(v3, v2) = v0)) % 133.49/27.96 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 133.49/27.96 | (difference(v3, v2) = v1) | ~ (difference(v3, v2) = v0)) % 133.49/27.96 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 133.49/27.96 | (symmetric_difference(v3, v2) = v1) | ~ (symmetric_difference(v3, % 133.49/27.96 | v2) = v0)) % 133.49/27.96 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 133.49/27.96 | (intersection(v3, v2) = v1) | ~ (intersection(v3, v2) = v0)) % 133.49/27.96 | % 133.49/27.96 | DELTA: instantiating (prove_th99) with fresh symbols all_17_0, all_17_1, % 133.49/27.96 | all_17_2, all_17_3, all_17_4, all_17_5, all_17_6 gives: % 133.49/27.97 | (21) ~ (all_17_0 = all_17_2) & symmetric_difference(all_17_3, all_17_4) = % 133.49/27.97 | all_17_2 & symmetric_difference(all_17_5, all_17_4) = all_17_1 & % 133.49/27.97 | symmetric_difference(all_17_6, all_17_1) = all_17_0 & % 133.49/27.97 | symmetric_difference(all_17_6, all_17_5) = all_17_3 & $i(all_17_0) & % 133.49/27.97 | $i(all_17_1) & $i(all_17_2) & $i(all_17_3) & $i(all_17_4) & % 133.49/27.97 | $i(all_17_5) & $i(all_17_6) % 133.49/27.97 | % 133.49/27.97 | ALPHA: (21) implies: % 133.49/27.97 | (22) ~ (all_17_0 = all_17_2) % 133.49/27.97 | (23) $i(all_17_6) % 133.49/27.97 | (24) $i(all_17_5) % 133.49/27.97 | (25) $i(all_17_4) % 133.49/27.97 | (26) $i(all_17_1) % 133.49/27.97 | (27) symmetric_difference(all_17_6, all_17_5) = all_17_3 % 133.49/27.97 | (28) symmetric_difference(all_17_6, all_17_1) = all_17_0 % 133.49/27.97 | (29) symmetric_difference(all_17_5, all_17_4) = all_17_1 % 133.49/27.97 | (30) symmetric_difference(all_17_3, all_17_4) = all_17_2 % 133.49/27.97 | % 133.49/27.97 | GROUND_INST: instantiating (16) with all_17_5, all_17_6, all_17_3, simplifying % 133.49/27.97 | with (23), (24), (27) gives: % 133.49/27.97 | (31) symmetric_difference(all_17_5, all_17_6) = all_17_3 & $i(all_17_3) % 133.49/27.97 | % 133.49/27.97 | ALPHA: (31) implies: % 133.49/27.97 | (32) $i(all_17_3) % 133.49/27.97 | (33) symmetric_difference(all_17_5, all_17_6) = all_17_3 % 133.49/27.97 | % 133.49/27.97 | GROUND_INST: instantiating (3) with all_17_6, all_17_5, all_17_3, simplifying % 133.49/27.97 | with (23), (24), (27) gives: % 133.49/27.97 | (34) ? [v0: $i] : ? [v1: $i] : (difference(all_17_5, all_17_6) = v1 & % 133.49/27.97 | difference(all_17_6, all_17_5) = v0 & union(v0, v1) = all_17_3 & % 133.49/27.97 | $i(v1) & $i(v0) & $i(all_17_3)) % 133.49/27.97 | % 133.49/27.97 | GROUND_INST: instantiating (16) with all_17_1, all_17_6, all_17_0, simplifying % 133.49/27.97 | with (23), (26), (28) gives: % 133.49/27.97 | (35) symmetric_difference(all_17_1, all_17_6) = all_17_0 & $i(all_17_0) % 133.49/27.97 | % 133.49/27.97 | ALPHA: (35) implies: % 133.49/27.98 | (36) symmetric_difference(all_17_1, all_17_6) = all_17_0 % 133.49/27.98 | % 133.49/27.98 | GROUND_INST: instantiating (3) with all_17_6, all_17_1, all_17_0, simplifying % 133.49/27.98 | with (23), (26), (28) gives: % 133.49/27.98 | (37) ? [v0: $i] : ? [v1: $i] : (difference(all_17_1, all_17_6) = v1 & % 133.49/27.98 | difference(all_17_6, all_17_1) = v0 & union(v0, v1) = all_17_0 & % 133.49/27.98 | $i(v1) & $i(v0) & $i(all_17_0)) % 133.49/27.98 | % 133.49/27.98 | GROUND_INST: instantiating (16) with all_17_4, all_17_5, all_17_1, simplifying % 133.49/27.98 | with (24), (25), (29) gives: % 133.49/27.98 | (38) symmetric_difference(all_17_4, all_17_5) = all_17_1 & $i(all_17_1) % 133.49/27.98 | % 133.49/27.98 | ALPHA: (38) implies: % 133.49/27.98 | (39) symmetric_difference(all_17_4, all_17_5) = all_17_1 % 133.49/27.98 | % 133.49/27.98 | GROUND_INST: instantiating (3) with all_17_5, all_17_4, all_17_1, simplifying % 133.49/27.98 | with (24), (25), (29) gives: % 133.49/27.98 | (40) ? [v0: $i] : ? [v1: $i] : (difference(all_17_4, all_17_5) = v1 & % 133.49/27.98 | difference(all_17_5, all_17_4) = v0 & union(v0, v1) = all_17_1 & % 133.49/27.98 | $i(v1) & $i(v0) & $i(all_17_1)) % 133.49/27.98 | % 133.49/27.98 | GROUND_INST: instantiating (16) with all_17_4, all_17_3, all_17_2, simplifying % 133.49/27.98 | with (25), (30), (32) gives: % 133.49/27.98 | (41) symmetric_difference(all_17_4, all_17_3) = all_17_2 & $i(all_17_2) % 133.49/27.98 | % 133.49/27.98 | ALPHA: (41) implies: % 133.49/27.98 | (42) symmetric_difference(all_17_4, all_17_3) = all_17_2 % 133.49/27.98 | % 133.49/27.98 | GROUND_INST: instantiating (3) with all_17_3, all_17_4, all_17_2, simplifying % 133.49/27.98 | with (25), (30), (32) gives: % 133.49/27.98 | (43) ? [v0: $i] : ? [v1: $i] : (difference(all_17_3, all_17_4) = v0 & % 133.49/27.98 | difference(all_17_4, all_17_3) = v1 & union(v0, v1) = all_17_2 & % 133.49/27.98 | $i(v1) & $i(v0) & $i(all_17_2)) % 133.49/27.98 | % 133.49/27.98 | DELTA: instantiating (40) with fresh symbols all_25_0, all_25_1 gives: % 133.49/27.98 | (44) difference(all_17_4, all_17_5) = all_25_0 & difference(all_17_5, % 133.49/27.98 | all_17_4) = all_25_1 & union(all_25_1, all_25_0) = all_17_1 & % 133.49/27.98 | $i(all_25_0) & $i(all_25_1) & $i(all_17_1) % 133.49/27.99 | % 133.49/27.99 | ALPHA: (44) implies: % 133.49/27.99 | (45) $i(all_25_1) % 133.49/27.99 | (46) $i(all_25_0) % 133.49/27.99 | (47) union(all_25_1, all_25_0) = all_17_1 % 133.49/27.99 | (48) difference(all_17_5, all_17_4) = all_25_1 % 133.49/27.99 | (49) difference(all_17_4, all_17_5) = all_25_0 % 133.49/27.99 | % 133.49/27.99 | DELTA: instantiating (34) with fresh symbols all_27_0, all_27_1 gives: % 133.49/27.99 | (50) difference(all_17_5, all_17_6) = all_27_0 & difference(all_17_6, % 133.49/27.99 | all_17_5) = all_27_1 & union(all_27_1, all_27_0) = all_17_3 & % 133.49/27.99 | $i(all_27_0) & $i(all_27_1) & $i(all_17_3) % 133.49/27.99 | % 133.49/27.99 | ALPHA: (50) implies: % 133.49/27.99 | (51) $i(all_27_1) % 133.49/27.99 | (52) $i(all_27_0) % 133.49/27.99 | (53) union(all_27_1, all_27_0) = all_17_3 % 133.49/27.99 | (54) difference(all_17_6, all_17_5) = all_27_1 % 133.49/27.99 | (55) difference(all_17_5, all_17_6) = all_27_0 % 133.49/27.99 | % 133.49/27.99 | DELTA: instantiating (43) with fresh symbols all_29_0, all_29_1 gives: % 133.49/27.99 | (56) difference(all_17_3, all_17_4) = all_29_1 & difference(all_17_4, % 133.49/27.99 | all_17_3) = all_29_0 & union(all_29_1, all_29_0) = all_17_2 & % 133.49/27.99 | $i(all_29_0) & $i(all_29_1) & $i(all_17_2) % 133.49/27.99 | % 133.49/27.99 | ALPHA: (56) implies: % 133.49/27.99 | (57) difference(all_17_4, all_17_3) = all_29_0 % 133.49/27.99 | (58) difference(all_17_3, all_17_4) = all_29_1 % 133.49/27.99 | % 133.49/27.99 | DELTA: instantiating (37) with fresh symbols all_31_0, all_31_1 gives: % 133.49/27.99 | (59) difference(all_17_1, all_17_6) = all_31_0 & difference(all_17_6, % 133.49/27.99 | all_17_1) = all_31_1 & union(all_31_1, all_31_0) = all_17_0 & % 133.49/27.99 | $i(all_31_0) & $i(all_31_1) & $i(all_17_0) % 133.49/27.99 | % 133.49/27.99 | ALPHA: (59) implies: % 133.49/27.99 | (60) $i(all_31_1) % 133.49/27.99 | (61) $i(all_31_0) % 133.49/27.99 | (62) union(all_31_1, all_31_0) = all_17_0 % 133.49/27.99 | (63) difference(all_17_6, all_17_1) = all_31_1 % 133.49/27.99 | (64) difference(all_17_1, all_17_6) = all_31_0 % 133.49/27.99 | % 133.49/27.99 | GROUND_INST: instantiating (14) with all_25_0, all_25_1, all_17_1, simplifying % 133.49/27.99 | with (45), (46), (47) gives: % 133.49/27.99 | (65) union(all_25_0, all_25_1) = all_17_1 & $i(all_17_1) % 133.49/27.99 | % 133.49/27.99 | GROUND_INST: instantiating (14) with all_27_0, all_27_1, all_17_3, simplifying % 133.49/27.99 | with (51), (52), (53) gives: % 133.49/28.00 | (66) union(all_27_0, all_27_1) = all_17_3 & $i(all_17_3) % 133.49/28.00 | % 133.49/28.00 | GROUND_INST: instantiating (8) with all_31_1, all_31_0, all_17_0, simplifying % 133.49/28.00 | with (60), (61), (62) gives: % 133.76/28.00 | (67) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.00 | (intersection(all_31_1, all_31_0) = v0 & difference(all_31_0, % 133.76/28.00 | all_31_1) = v3 & difference(all_31_1, all_31_0) = v2 & % 133.76/28.00 | difference(all_17_0, v0) = v1 & union(v2, v3) = v1 & $i(v3) & $i(v2) % 133.76/28.00 | & $i(v1) & $i(v0)) % 133.76/28.00 | % 133.76/28.00 | GROUND_INST: instantiating (10) with all_17_5, all_17_6, all_27_1, simplifying % 133.76/28.00 | with (23), (24), (54) gives: % 133.76/28.00 | (68) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.00 | (intersection(all_17_5, all_17_6) = v1 & difference(v0, v1) = v2 & % 133.76/28.00 | difference(all_17_5, all_17_6) = v3 & union(v3, all_27_1) = v2 & % 133.76/28.00 | union(all_17_5, all_17_6) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.00 | % 133.76/28.00 | GROUND_INST: instantiating (2) with all_17_5, all_17_6, all_27_1, simplifying % 133.76/28.00 | with (23), (24), (54) gives: % 133.76/28.00 | (69) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_5, all_17_6) % 133.76/28.00 | = v0 & difference(all_17_5, all_17_6) = v1 & union(v1, all_27_1) = % 133.76/28.00 | v0 & $i(v1) & $i(v0)) % 133.76/28.00 | % 133.76/28.00 | GROUND_INST: instantiating (9) with all_17_6, all_17_5, all_27_1, simplifying % 133.76/28.00 | with (23), (24), (54) gives: % 133.76/28.00 | (70) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.00 | (intersection(all_17_6, all_17_5) = v1 & difference(v0, v1) = v2 & % 133.76/28.00 | difference(all_17_5, all_17_6) = v3 & union(all_27_1, v3) = v2 & % 133.76/28.00 | union(all_17_6, all_17_5) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.00 | % 133.76/28.00 | GROUND_INST: instantiating (11) with all_17_6, all_25_1, all_25_0, all_17_1, % 133.76/28.00 | all_31_1, simplifying with (23), (45), (46), (47), (63) gives: % 133.76/28.01 | (71) ? [v0: $i] : (difference(v0, all_25_0) = all_31_1 & % 133.76/28.01 | difference(all_17_6, all_25_1) = v0 & $i(v0) & $i(all_31_1)) % 133.76/28.01 | % 133.76/28.01 | GROUND_INST: instantiating (10) with all_17_1, all_17_6, all_31_1, simplifying % 133.76/28.01 | with (23), (26), (63) gives: % 133.76/28.01 | (72) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.01 | (intersection(all_17_1, all_17_6) = v1 & difference(v0, v1) = v2 & % 133.76/28.01 | difference(all_17_1, all_17_6) = v3 & union(v3, all_31_1) = v2 & % 133.76/28.01 | union(all_17_1, all_17_6) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.01 | % 133.76/28.01 | GROUND_INST: instantiating (2) with all_17_1, all_17_6, all_31_1, simplifying % 133.76/28.01 | with (23), (26), (63) gives: % 133.76/28.01 | (73) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_1, all_17_6) % 133.76/28.01 | = v0 & difference(all_17_1, all_17_6) = v1 & union(v1, all_31_1) = % 133.76/28.01 | v0 & $i(v1) & $i(v0)) % 133.76/28.01 | % 133.76/28.01 | GROUND_INST: instantiating (9) with all_17_6, all_17_1, all_31_1, simplifying % 133.76/28.01 | with (23), (26), (63) gives: % 133.76/28.01 | (74) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.01 | (intersection(all_17_6, all_17_1) = v1 & difference(v0, v1) = v2 & % 133.76/28.01 | difference(all_17_1, all_17_6) = v3 & union(all_31_1, v3) = v2 & % 133.76/28.01 | union(all_17_6, all_17_1) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.01 | % 133.76/28.01 | GROUND_INST: instantiating (10) with all_17_6, all_17_5, all_27_0, simplifying % 133.76/28.01 | with (23), (24), (55) gives: % 133.76/28.01 | (75) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.01 | (intersection(all_17_6, all_17_5) = v1 & difference(v0, v1) = v2 & % 133.76/28.01 | difference(all_17_6, all_17_5) = v3 & union(v3, all_27_0) = v2 & % 133.76/28.01 | union(all_17_6, all_17_5) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.01 | % 133.76/28.01 | GROUND_INST: instantiating (9) with all_17_5, all_17_6, all_27_0, simplifying % 133.76/28.01 | with (23), (24), (55) gives: % 133.76/28.02 | (76) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.02 | (intersection(all_17_5, all_17_6) = v1 & difference(v0, v1) = v2 & % 133.76/28.02 | difference(all_17_6, all_17_5) = v3 & union(all_27_0, v3) = v2 & % 133.76/28.02 | union(all_17_5, all_17_6) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.02 | % 133.76/28.02 | GROUND_INST: instantiating (1) with all_17_5, all_17_6, all_27_0, simplifying % 133.76/28.02 | with (23), (24), (55) gives: % 133.76/28.02 | (77) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_5, all_17_6) % 133.76/28.02 | = v0 & difference(all_17_6, all_17_5) = v1 & union(all_27_0, v1) = % 133.76/28.02 | v0 & $i(v1) & $i(v0)) % 133.76/28.02 | % 133.76/28.02 | GROUND_INST: instantiating (10) with all_17_4, all_17_5, all_25_1, simplifying % 133.76/28.02 | with (24), (25), (48) gives: % 133.76/28.02 | (78) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.02 | (intersection(all_17_4, all_17_5) = v1 & difference(v0, v1) = v2 & % 133.76/28.02 | difference(all_17_4, all_17_5) = v3 & union(v3, all_25_1) = v2 & % 133.76/28.02 | union(all_17_4, all_17_5) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.02 | % 133.76/28.02 | GROUND_INST: instantiating (2) with all_17_4, all_17_5, all_25_1, simplifying % 133.76/28.02 | with (24), (25), (48) gives: % 133.76/28.02 | (79) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_4, all_17_5) % 133.76/28.02 | = v0 & difference(all_17_4, all_17_5) = v1 & union(v1, all_25_1) = % 133.76/28.02 | v0 & $i(v1) & $i(v0)) % 133.76/28.02 | % 133.76/28.02 | GROUND_INST: instantiating (9) with all_17_5, all_17_4, all_25_1, simplifying % 133.76/28.02 | with (24), (25), (48) gives: % 133.76/28.02 | (80) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.02 | (intersection(all_17_5, all_17_4) = v1 & difference(v0, v1) = v2 & % 133.76/28.02 | difference(all_17_4, all_17_5) = v3 & union(all_25_1, v3) = v2 & % 133.76/28.02 | union(all_17_5, all_17_4) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.02 | % 133.76/28.02 | GROUND_INST: instantiating (10) with all_17_5, all_17_4, all_25_0, simplifying % 133.76/28.02 | with (24), (25), (49) gives: % 133.76/28.03 | (81) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.03 | (intersection(all_17_5, all_17_4) = v1 & difference(v0, v1) = v2 & % 133.76/28.03 | difference(all_17_5, all_17_4) = v3 & union(v3, all_25_0) = v2 & % 133.76/28.03 | union(all_17_5, all_17_4) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.03 | % 133.76/28.03 | GROUND_INST: instantiating (9) with all_17_4, all_17_5, all_25_0, simplifying % 133.76/28.03 | with (24), (25), (49) gives: % 133.76/28.03 | (82) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.03 | (intersection(all_17_4, all_17_5) = v1 & difference(v0, v1) = v2 & % 133.76/28.03 | difference(all_17_5, all_17_4) = v3 & union(all_25_0, v3) = v2 & % 133.76/28.03 | union(all_17_4, all_17_5) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.03 | % 133.76/28.03 | GROUND_INST: instantiating (1) with all_17_4, all_17_5, all_25_0, simplifying % 133.76/28.03 | with (24), (25), (49) gives: % 133.76/28.03 | (83) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_4, all_17_5) % 133.76/28.03 | = v0 & difference(all_17_5, all_17_4) = v1 & union(all_25_0, v1) = % 133.76/28.03 | v0 & $i(v1) & $i(v0)) % 133.76/28.03 | % 133.76/28.03 | GROUND_INST: instantiating (11) with all_17_4, all_27_1, all_27_0, all_17_3, % 133.76/28.03 | all_29_0, simplifying with (25), (51), (52), (53), (57) gives: % 133.76/28.03 | (84) ? [v0: $i] : (difference(v0, all_27_0) = all_29_0 & % 133.76/28.03 | difference(all_17_4, all_27_1) = v0 & $i(v0) & $i(all_29_0)) % 133.76/28.03 | % 133.76/28.03 | GROUND_INST: instantiating (10) with all_17_3, all_17_4, all_29_0, simplifying % 133.76/28.03 | with (25), (32), (57) gives: % 133.76/28.03 | (85) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.03 | (intersection(all_17_3, all_17_4) = v1 & difference(v0, v1) = v2 & % 133.76/28.03 | difference(all_17_3, all_17_4) = v3 & union(v3, all_29_0) = v2 & % 133.76/28.03 | union(all_17_3, all_17_4) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.03 | % 133.76/28.03 | GROUND_INST: instantiating (9) with all_17_4, all_17_3, all_29_0, simplifying % 133.76/28.03 | with (25), (32), (57) gives: % 133.76/28.04 | (86) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.04 | (intersection(all_17_4, all_17_3) = v1 & difference(v0, v1) = v2 & % 133.76/28.04 | difference(all_17_3, all_17_4) = v3 & union(all_29_0, v3) = v2 & % 133.76/28.04 | union(all_17_4, all_17_3) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.04 | % 133.76/28.04 | GROUND_INST: instantiating (1) with all_17_4, all_17_3, all_29_0, simplifying % 133.76/28.04 | with (25), (32), (57) gives: % 133.76/28.04 | (87) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_4, all_17_3) % 133.76/28.04 | = v0 & difference(all_17_3, all_17_4) = v1 & union(all_29_0, v1) = % 133.76/28.04 | v0 & $i(v1) & $i(v0)) % 133.76/28.04 | % 133.76/28.04 | GROUND_INST: instantiating (13) with all_27_1, all_27_0, all_17_4, all_17_3, % 133.76/28.04 | all_29_1, simplifying with (25), (51), (52), (53), (58) gives: % 133.76/28.04 | (88) ? [v0: $i] : ? [v1: $i] : (difference(all_27_0, all_17_4) = v1 & % 133.76/28.04 | difference(all_27_1, all_17_4) = v0 & union(v0, v1) = all_29_1 & % 133.76/28.04 | $i(v1) & $i(v0) & $i(all_29_1)) % 133.76/28.04 | % 133.76/28.04 | GROUND_INST: instantiating (10) with all_17_4, all_17_3, all_29_1, simplifying % 133.76/28.04 | with (25), (32), (58) gives: % 133.76/28.04 | (89) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.04 | (intersection(all_17_4, all_17_3) = v1 & difference(v0, v1) = v2 & % 133.76/28.04 | difference(all_17_4, all_17_3) = v3 & union(v3, all_29_1) = v2 & % 133.76/28.04 | union(all_17_4, all_17_3) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.04 | % 133.76/28.04 | GROUND_INST: instantiating (2) with all_17_4, all_17_3, all_29_1, simplifying % 133.76/28.04 | with (25), (32), (58) gives: % 133.76/28.04 | (90) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_4, all_17_3) % 133.76/28.04 | = v0 & difference(all_17_4, all_17_3) = v1 & union(v1, all_29_1) = % 133.76/28.04 | v0 & $i(v1) & $i(v0)) % 133.76/28.04 | % 133.76/28.04 | GROUND_INST: instantiating (9) with all_17_3, all_17_4, all_29_1, simplifying % 133.76/28.04 | with (25), (32), (58) gives: % 133.76/28.04 | (91) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.04 | (intersection(all_17_3, all_17_4) = v1 & difference(v0, v1) = v2 & % 133.76/28.04 | difference(all_17_4, all_17_3) = v3 & union(all_29_1, v3) = v2 & % 133.76/28.04 | union(all_17_3, all_17_4) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.04 | % 133.76/28.05 | GROUND_INST: instantiating (13) with all_25_1, all_25_0, all_17_6, all_17_1, % 133.76/28.05 | all_31_0, simplifying with (23), (45), (46), (47), (64) gives: % 133.76/28.05 | (92) ? [v0: $i] : ? [v1: $i] : (difference(all_25_0, all_17_6) = v1 & % 133.76/28.05 | difference(all_25_1, all_17_6) = v0 & union(v0, v1) = all_31_0 & % 133.76/28.05 | $i(v1) & $i(v0) & $i(all_31_0)) % 133.76/28.05 | % 133.76/28.05 | GROUND_INST: instantiating (10) with all_17_6, all_17_1, all_31_0, simplifying % 133.76/28.05 | with (23), (26), (64) gives: % 133.76/28.05 | (93) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.05 | (intersection(all_17_6, all_17_1) = v1 & difference(v0, v1) = v2 & % 133.76/28.05 | difference(all_17_6, all_17_1) = v3 & union(v3, all_31_0) = v2 & % 133.76/28.05 | union(all_17_6, all_17_1) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.05 | % 133.76/28.05 | GROUND_INST: instantiating (9) with all_17_1, all_17_6, all_31_0, simplifying % 133.76/28.05 | with (23), (26), (64) gives: % 133.76/28.05 | (94) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 133.76/28.05 | (intersection(all_17_1, all_17_6) = v1 & difference(v0, v1) = v2 & % 133.76/28.05 | difference(all_17_6, all_17_1) = v3 & union(all_31_0, v3) = v2 & % 133.76/28.05 | union(all_17_1, all_17_6) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 133.76/28.05 | % 133.76/28.05 | GROUND_INST: instantiating (1) with all_17_1, all_17_6, all_31_0, simplifying % 133.76/28.05 | with (23), (26), (64) gives: % 133.76/28.05 | (95) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_1, all_17_6) % 133.76/28.05 | = v0 & difference(all_17_6, all_17_1) = v1 & union(all_31_0, v1) = % 133.76/28.05 | v0 & $i(v1) & $i(v0)) % 133.76/28.05 | % 133.76/28.05 | GROUND_INST: instantiating (3) with all_17_5, all_17_6, all_17_3, simplifying % 133.76/28.05 | with (23), (24), (33) gives: % 133.76/28.05 | (96) ? [v0: $i] : ? [v1: $i] : (difference(all_17_5, all_17_6) = v0 & % 133.76/28.05 | difference(all_17_6, all_17_5) = v1 & union(v0, v1) = all_17_3 & % 133.76/28.05 | $i(v1) & $i(v0) & $i(all_17_3)) % 133.76/28.05 | % 133.76/28.05 | GROUND_INST: instantiating (3) with all_17_4, all_17_5, all_17_1, simplifying % 133.76/28.05 | with (24), (25), (39) gives: % 134.06/28.06 | (97) ? [v0: $i] : ? [v1: $i] : (difference(all_17_4, all_17_5) = v0 & % 134.06/28.06 | difference(all_17_5, all_17_4) = v1 & union(v0, v1) = all_17_1 & % 134.06/28.06 | $i(v1) & $i(v0) & $i(all_17_1)) % 134.06/28.06 | % 134.06/28.06 | GROUND_INST: instantiating (3) with all_17_4, all_17_3, all_17_2, simplifying % 134.06/28.06 | with (25), (32), (42) gives: % 134.06/28.06 | (98) ? [v0: $i] : ? [v1: $i] : (difference(all_17_3, all_17_4) = v1 & % 134.06/28.06 | difference(all_17_4, all_17_3) = v0 & union(v0, v1) = all_17_2 & % 134.06/28.06 | $i(v1) & $i(v0) & $i(all_17_2)) % 134.06/28.06 | % 134.06/28.06 | GROUND_INST: instantiating (3) with all_17_1, all_17_6, all_17_0, simplifying % 134.06/28.06 | with (23), (26), (36) gives: % 134.06/28.06 | (99) ? [v0: $i] : ? [v1: $i] : (difference(all_17_1, all_17_6) = v0 & % 134.06/28.06 | difference(all_17_6, all_17_1) = v1 & union(v0, v1) = all_17_0 & % 134.06/28.06 | $i(v1) & $i(v0) & $i(all_17_0)) % 134.06/28.06 | % 134.06/28.06 | DELTA: instantiating (84) with fresh symbol all_39_0 gives: % 134.06/28.06 | (100) difference(all_39_0, all_27_0) = all_29_0 & difference(all_17_4, % 134.06/28.06 | all_27_1) = all_39_0 & $i(all_39_0) & $i(all_29_0) % 134.06/28.06 | % 134.06/28.06 | ALPHA: (100) implies: % 134.06/28.06 | (101) difference(all_17_4, all_27_1) = all_39_0 % 134.06/28.06 | % 134.06/28.06 | DELTA: instantiating (71) with fresh symbol all_41_0 gives: % 134.06/28.06 | (102) difference(all_41_0, all_25_0) = all_31_1 & difference(all_17_6, % 134.06/28.06 | all_25_1) = all_41_0 & $i(all_41_0) & $i(all_31_1) % 134.06/28.06 | % 134.06/28.06 | ALPHA: (102) implies: % 134.06/28.06 | (103) $i(all_41_0) % 134.06/28.06 | (104) difference(all_17_6, all_25_1) = all_41_0 % 134.06/28.06 | (105) difference(all_41_0, all_25_0) = all_31_1 % 134.06/28.06 | % 134.06/28.06 | DELTA: instantiating (90) with fresh symbols all_43_0, all_43_1 gives: % 134.06/28.06 | (106) symmetric_difference(all_17_4, all_17_3) = all_43_1 & % 134.06/28.06 | difference(all_17_4, all_17_3) = all_43_0 & union(all_43_0, all_29_1) % 134.06/28.06 | = all_43_1 & $i(all_43_0) & $i(all_43_1) % 134.06/28.06 | % 134.06/28.06 | ALPHA: (106) implies: % 134.06/28.06 | (107) $i(all_43_0) % 134.06/28.06 | (108) difference(all_17_4, all_17_3) = all_43_0 % 134.06/28.06 | (109) symmetric_difference(all_17_4, all_17_3) = all_43_1 % 134.06/28.06 | % 134.06/28.06 | DELTA: instantiating (87) with fresh symbols all_45_0, all_45_1 gives: % 134.06/28.06 | (110) symmetric_difference(all_17_4, all_17_3) = all_45_1 & % 134.06/28.06 | difference(all_17_3, all_17_4) = all_45_0 & union(all_29_0, all_45_0) % 134.06/28.06 | = all_45_1 & $i(all_45_0) & $i(all_45_1) % 134.06/28.06 | % 134.06/28.06 | ALPHA: (110) implies: % 134.06/28.06 | (111) union(all_29_0, all_45_0) = all_45_1 % 134.06/28.06 | (112) difference(all_17_3, all_17_4) = all_45_0 % 134.06/28.06 | (113) symmetric_difference(all_17_4, all_17_3) = all_45_1 % 134.06/28.06 | % 134.06/28.06 | DELTA: instantiating (69) with fresh symbols all_47_0, all_47_1 gives: % 134.06/28.06 | (114) symmetric_difference(all_17_5, all_17_6) = all_47_1 & % 134.06/28.06 | difference(all_17_5, all_17_6) = all_47_0 & union(all_47_0, all_27_1) % 134.06/28.06 | = all_47_1 & $i(all_47_0) & $i(all_47_1) % 134.06/28.06 | % 134.06/28.06 | ALPHA: (114) implies: % 134.06/28.06 | (115) $i(all_47_0) % 134.06/28.06 | (116) difference(all_17_5, all_17_6) = all_47_0 % 134.06/28.06 | (117) symmetric_difference(all_17_5, all_17_6) = all_47_1 % 134.06/28.06 | % 134.06/28.06 | DELTA: instantiating (83) with fresh symbols all_49_0, all_49_1 gives: % 134.06/28.07 | (118) symmetric_difference(all_17_4, all_17_5) = all_49_1 & % 134.06/28.07 | difference(all_17_5, all_17_4) = all_49_0 & union(all_25_0, all_49_0) % 134.06/28.07 | = all_49_1 & $i(all_49_0) & $i(all_49_1) % 134.06/28.07 | % 134.06/28.07 | ALPHA: (118) implies: % 134.06/28.07 | (119) $i(all_49_0) % 134.06/28.07 | (120) union(all_25_0, all_49_0) = all_49_1 % 134.06/28.07 | (121) difference(all_17_5, all_17_4) = all_49_0 % 134.06/28.07 | (122) symmetric_difference(all_17_4, all_17_5) = all_49_1 % 134.06/28.07 | % 134.06/28.07 | DELTA: instantiating (73) with fresh symbols all_51_0, all_51_1 gives: % 134.06/28.07 | (123) symmetric_difference(all_17_1, all_17_6) = all_51_1 & % 134.06/28.07 | difference(all_17_1, all_17_6) = all_51_0 & union(all_51_0, all_31_1) % 134.06/28.07 | = all_51_1 & $i(all_51_0) & $i(all_51_1) % 134.06/28.07 | % 134.06/28.07 | ALPHA: (123) implies: % 134.06/28.07 | (124) difference(all_17_1, all_17_6) = all_51_0 % 134.06/28.07 | (125) symmetric_difference(all_17_1, all_17_6) = all_51_1 % 134.06/28.07 | % 134.06/28.07 | DELTA: instantiating (79) with fresh symbols all_53_0, all_53_1 gives: % 134.06/28.07 | (126) symmetric_difference(all_17_4, all_17_5) = all_53_1 & % 134.06/28.07 | difference(all_17_4, all_17_5) = all_53_0 & union(all_53_0, all_25_1) % 134.06/28.07 | = all_53_1 & $i(all_53_0) & $i(all_53_1) % 134.06/28.07 | % 134.06/28.07 | ALPHA: (126) implies: % 134.06/28.07 | (127) $i(all_53_0) % 134.06/28.07 | (128) difference(all_17_4, all_17_5) = all_53_0 % 134.06/28.07 | (129) symmetric_difference(all_17_4, all_17_5) = all_53_1 % 134.06/28.07 | % 134.06/28.07 | DELTA: instantiating (77) with fresh symbols all_55_0, all_55_1 gives: % 134.06/28.07 | (130) symmetric_difference(all_17_5, all_17_6) = all_55_1 & % 134.06/28.07 | difference(all_17_6, all_17_5) = all_55_0 & union(all_27_0, all_55_0) % 134.06/28.07 | = all_55_1 & $i(all_55_0) & $i(all_55_1) % 134.06/28.07 | % 134.06/28.07 | ALPHA: (130) implies: % 134.06/28.07 | (131) $i(all_55_0) % 134.06/28.07 | (132) union(all_27_0, all_55_0) = all_55_1 % 134.06/28.07 | (133) difference(all_17_6, all_17_5) = all_55_0 % 134.06/28.07 | (134) symmetric_difference(all_17_5, all_17_6) = all_55_1 % 134.06/28.07 | % 134.06/28.07 | DELTA: instantiating (95) with fresh symbols all_57_0, all_57_1 gives: % 134.06/28.07 | (135) symmetric_difference(all_17_1, all_17_6) = all_57_1 & % 134.06/28.07 | difference(all_17_6, all_17_1) = all_57_0 & union(all_31_0, all_57_0) % 134.06/28.07 | = all_57_1 & $i(all_57_0) & $i(all_57_1) % 134.06/28.07 | % 134.06/28.07 | ALPHA: (135) implies: % 134.06/28.07 | (136) $i(all_57_0) % 134.06/28.07 | (137) union(all_31_0, all_57_0) = all_57_1 % 134.06/28.07 | (138) difference(all_17_6, all_17_1) = all_57_0 % 134.06/28.07 | (139) symmetric_difference(all_17_1, all_17_6) = all_57_1 % 134.06/28.07 | % 134.06/28.07 | DELTA: instantiating (99) with fresh symbols all_59_0, all_59_1 gives: % 134.06/28.07 | (140) difference(all_17_1, all_17_6) = all_59_1 & difference(all_17_6, % 134.06/28.07 | all_17_1) = all_59_0 & union(all_59_1, all_59_0) = all_17_0 & % 134.06/28.07 | $i(all_59_0) & $i(all_59_1) & $i(all_17_0) % 134.06/28.07 | % 134.06/28.07 | ALPHA: (140) implies: % 134.06/28.07 | (141) difference(all_17_6, all_17_1) = all_59_0 % 134.06/28.07 | (142) difference(all_17_1, all_17_6) = all_59_1 % 134.06/28.07 | % 134.06/28.07 | DELTA: instantiating (88) with fresh symbols all_61_0, all_61_1 gives: % 134.06/28.07 | (143) difference(all_27_0, all_17_4) = all_61_0 & difference(all_27_1, % 134.06/28.07 | all_17_4) = all_61_1 & union(all_61_1, all_61_0) = all_29_1 & % 134.06/28.07 | $i(all_61_0) & $i(all_61_1) & $i(all_29_1) % 134.06/28.07 | % 134.06/28.07 | ALPHA: (143) implies: % 134.06/28.07 | (144) $i(all_61_1) % 134.06/28.07 | (145) $i(all_61_0) % 134.06/28.07 | (146) union(all_61_1, all_61_0) = all_29_1 % 134.06/28.07 | (147) difference(all_27_1, all_17_4) = all_61_1 % 134.06/28.07 | (148) difference(all_27_0, all_17_4) = all_61_0 % 134.06/28.07 | % 134.06/28.07 | DELTA: instantiating (98) with fresh symbols all_63_0, all_63_1 gives: % 134.06/28.08 | (149) difference(all_17_3, all_17_4) = all_63_0 & difference(all_17_4, % 134.06/28.08 | all_17_3) = all_63_1 & union(all_63_1, all_63_0) = all_17_2 & % 134.06/28.08 | $i(all_63_0) & $i(all_63_1) & $i(all_17_2) % 134.06/28.08 | % 134.06/28.08 | ALPHA: (149) implies: % 134.06/28.08 | (150) difference(all_17_4, all_17_3) = all_63_1 % 134.06/28.08 | (151) difference(all_17_3, all_17_4) = all_63_0 % 134.06/28.08 | % 134.06/28.08 | DELTA: instantiating (97) with fresh symbols all_65_0, all_65_1 gives: % 134.06/28.08 | (152) difference(all_17_4, all_17_5) = all_65_1 & difference(all_17_5, % 134.06/28.08 | all_17_4) = all_65_0 & union(all_65_1, all_65_0) = all_17_1 & % 134.06/28.08 | $i(all_65_0) & $i(all_65_1) & $i(all_17_1) % 134.06/28.08 | % 134.06/28.08 | ALPHA: (152) implies: % 134.06/28.08 | (153) difference(all_17_5, all_17_4) = all_65_0 % 134.06/28.08 | (154) difference(all_17_4, all_17_5) = all_65_1 % 134.06/28.08 | % 134.06/28.08 | DELTA: instantiating (96) with fresh symbols all_67_0, all_67_1 gives: % 134.06/28.08 | (155) difference(all_17_5, all_17_6) = all_67_1 & difference(all_17_6, % 134.06/28.08 | all_17_5) = all_67_0 & union(all_67_1, all_67_0) = all_17_3 & % 134.06/28.08 | $i(all_67_0) & $i(all_67_1) & $i(all_17_3) % 134.06/28.08 | % 134.06/28.08 | ALPHA: (155) implies: % 134.06/28.08 | (156) difference(all_17_6, all_17_5) = all_67_0 % 134.06/28.08 | (157) difference(all_17_5, all_17_6) = all_67_1 % 134.06/28.08 | % 134.06/28.08 | DELTA: instantiating (92) with fresh symbols all_69_0, all_69_1 gives: % 134.06/28.08 | (158) difference(all_25_0, all_17_6) = all_69_0 & difference(all_25_1, % 134.06/28.08 | all_17_6) = all_69_1 & union(all_69_1, all_69_0) = all_31_0 & % 134.06/28.08 | $i(all_69_0) & $i(all_69_1) & $i(all_31_0) % 134.06/28.08 | % 134.06/28.08 | ALPHA: (158) implies: % 134.06/28.08 | (159) $i(all_69_1) % 134.06/28.08 | (160) $i(all_69_0) % 134.06/28.08 | (161) union(all_69_1, all_69_0) = all_31_0 % 134.06/28.08 | (162) difference(all_25_1, all_17_6) = all_69_1 % 134.06/28.08 | (163) difference(all_25_0, all_17_6) = all_69_0 % 134.06/28.08 | % 134.06/28.08 | DELTA: instantiating (94) with fresh symbols all_71_0, all_71_1, all_71_2, % 134.06/28.08 | all_71_3 gives: % 134.06/28.08 | (164) intersection(all_17_1, all_17_6) = all_71_2 & difference(all_71_3, % 134.06/28.08 | all_71_2) = all_71_1 & difference(all_17_6, all_17_1) = all_71_0 & % 134.06/28.08 | union(all_31_0, all_71_0) = all_71_1 & union(all_17_1, all_17_6) = % 134.06/28.08 | all_71_3 & $i(all_71_0) & $i(all_71_1) & $i(all_71_2) & $i(all_71_3) % 134.06/28.08 | % 134.06/28.08 | ALPHA: (164) implies: % 134.06/28.08 | (165) union(all_17_1, all_17_6) = all_71_3 % 134.06/28.08 | (166) union(all_31_0, all_71_0) = all_71_1 % 134.06/28.08 | (167) difference(all_17_6, all_17_1) = all_71_0 % 134.06/28.08 | (168) difference(all_71_3, all_71_2) = all_71_1 % 134.06/28.08 | (169) intersection(all_17_1, all_17_6) = all_71_2 % 134.06/28.09 | % 134.06/28.09 | DELTA: instantiating (76) with fresh symbols all_73_0, all_73_1, all_73_2, % 134.06/28.09 | all_73_3 gives: % 134.06/28.09 | (170) intersection(all_17_5, all_17_6) = all_73_2 & difference(all_73_3, % 134.06/28.09 | all_73_2) = all_73_1 & difference(all_17_6, all_17_5) = all_73_0 & % 134.06/28.09 | union(all_27_0, all_73_0) = all_73_1 & union(all_17_5, all_17_6) = % 134.06/28.09 | all_73_3 & $i(all_73_0) & $i(all_73_1) & $i(all_73_2) & $i(all_73_3) % 134.06/28.09 | % 134.06/28.09 | ALPHA: (170) implies: % 134.06/28.09 | (171) union(all_17_5, all_17_6) = all_73_3 % 134.06/28.09 | (172) union(all_27_0, all_73_0) = all_73_1 % 134.06/28.09 | (173) difference(all_17_6, all_17_5) = all_73_0 % 134.06/28.09 | (174) difference(all_73_3, all_73_2) = all_73_1 % 134.06/28.09 | (175) intersection(all_17_5, all_17_6) = all_73_2 % 134.06/28.09 | % 134.06/28.09 | DELTA: instantiating (75) with fresh symbols all_75_0, all_75_1, all_75_2, % 134.06/28.09 | all_75_3 gives: % 134.06/28.09 | (176) intersection(all_17_6, all_17_5) = all_75_2 & difference(all_75_3, % 134.06/28.09 | all_75_2) = all_75_1 & difference(all_17_6, all_17_5) = all_75_0 & % 134.06/28.09 | union(all_75_0, all_27_0) = all_75_1 & union(all_17_6, all_17_5) = % 134.06/28.09 | all_75_3 & $i(all_75_0) & $i(all_75_1) & $i(all_75_2) & $i(all_75_3) % 134.06/28.09 | % 134.06/28.09 | ALPHA: (176) implies: % 134.06/28.09 | (177) union(all_17_6, all_17_5) = all_75_3 % 134.06/28.09 | (178) difference(all_17_6, all_17_5) = all_75_0 % 134.06/28.09 | (179) difference(all_75_3, all_75_2) = all_75_1 % 134.06/28.09 | (180) intersection(all_17_6, all_17_5) = all_75_2 % 134.06/28.09 | % 134.06/28.09 | DELTA: instantiating (93) with fresh symbols all_79_0, all_79_1, all_79_2, % 134.06/28.09 | all_79_3 gives: % 134.06/28.09 | (181) intersection(all_17_6, all_17_1) = all_79_2 & difference(all_79_3, % 134.06/28.09 | all_79_2) = all_79_1 & difference(all_17_6, all_17_1) = all_79_0 & % 134.06/28.09 | union(all_79_0, all_31_0) = all_79_1 & union(all_17_6, all_17_1) = % 134.06/28.09 | all_79_3 & $i(all_79_0) & $i(all_79_1) & $i(all_79_2) & $i(all_79_3) % 134.06/28.09 | % 134.06/28.09 | ALPHA: (181) implies: % 134.06/28.09 | (182) union(all_17_6, all_17_1) = all_79_3 % 134.06/28.09 | (183) union(all_79_0, all_31_0) = all_79_1 % 134.06/28.09 | (184) difference(all_17_6, all_17_1) = all_79_0 % 134.06/28.09 | (185) difference(all_79_3, all_79_2) = all_79_1 % 134.06/28.09 | (186) intersection(all_17_6, all_17_1) = all_79_2 % 134.06/28.09 | % 134.06/28.09 | DELTA: instantiating (91) with fresh symbols all_81_0, all_81_1, all_81_2, % 134.06/28.09 | all_81_3 gives: % 134.06/28.10 | (187) intersection(all_17_3, all_17_4) = all_81_2 & difference(all_81_3, % 134.06/28.10 | all_81_2) = all_81_1 & difference(all_17_4, all_17_3) = all_81_0 & % 134.06/28.10 | union(all_29_1, all_81_0) = all_81_1 & union(all_17_3, all_17_4) = % 134.06/28.10 | all_81_3 & $i(all_81_0) & $i(all_81_1) & $i(all_81_2) & $i(all_81_3) % 134.06/28.10 | % 134.06/28.10 | ALPHA: (187) implies: % 134.06/28.10 | (188) difference(all_17_4, all_17_3) = all_81_0 % 134.06/28.10 | % 134.06/28.10 | DELTA: instantiating (80) with fresh symbols all_83_0, all_83_1, all_83_2, % 134.06/28.10 | all_83_3 gives: % 134.06/28.10 | (189) intersection(all_17_5, all_17_4) = all_83_2 & difference(all_83_3, % 134.06/28.10 | all_83_2) = all_83_1 & difference(all_17_4, all_17_5) = all_83_0 & % 134.06/28.10 | union(all_25_1, all_83_0) = all_83_1 & union(all_17_5, all_17_4) = % 134.06/28.10 | all_83_3 & $i(all_83_0) & $i(all_83_1) & $i(all_83_2) & $i(all_83_3) % 134.06/28.10 | % 134.06/28.10 | ALPHA: (189) implies: % 134.06/28.10 | (190) union(all_17_5, all_17_4) = all_83_3 % 134.06/28.10 | (191) difference(all_17_4, all_17_5) = all_83_0 % 134.06/28.10 | (192) difference(all_83_3, all_83_2) = all_83_1 % 134.06/28.10 | (193) intersection(all_17_5, all_17_4) = all_83_2 % 134.06/28.10 | % 134.06/28.10 | DELTA: instantiating (78) with fresh symbols all_85_0, all_85_1, all_85_2, % 134.06/28.10 | all_85_3 gives: % 134.06/28.10 | (194) intersection(all_17_4, all_17_5) = all_85_2 & difference(all_85_3, % 134.06/28.10 | all_85_2) = all_85_1 & difference(all_17_4, all_17_5) = all_85_0 & % 134.06/28.10 | union(all_85_0, all_25_1) = all_85_1 & union(all_17_4, all_17_5) = % 134.06/28.10 | all_85_3 & $i(all_85_0) & $i(all_85_1) & $i(all_85_2) & $i(all_85_3) % 134.06/28.10 | % 134.06/28.10 | ALPHA: (194) implies: % 134.06/28.10 | (195) union(all_17_4, all_17_5) = all_85_3 % 134.06/28.10 | (196) union(all_85_0, all_25_1) = all_85_1 % 134.06/28.10 | (197) difference(all_17_4, all_17_5) = all_85_0 % 134.06/28.10 | (198) difference(all_85_3, all_85_2) = all_85_1 % 134.06/28.10 | (199) intersection(all_17_4, all_17_5) = all_85_2 % 134.06/28.10 | % 134.06/28.10 | DELTA: instantiating (72) with fresh symbols all_87_0, all_87_1, all_87_2, % 134.06/28.10 | all_87_3 gives: % 134.06/28.10 | (200) intersection(all_17_1, all_17_6) = all_87_2 & difference(all_87_3, % 134.06/28.10 | all_87_2) = all_87_1 & difference(all_17_1, all_17_6) = all_87_0 & % 134.06/28.10 | union(all_87_0, all_31_1) = all_87_1 & union(all_17_1, all_17_6) = % 134.06/28.10 | all_87_3 & $i(all_87_0) & $i(all_87_1) & $i(all_87_2) & $i(all_87_3) % 134.06/28.10 | % 134.06/28.10 | ALPHA: (200) implies: % 134.06/28.10 | (201) union(all_17_1, all_17_6) = all_87_3 % 134.06/28.10 | (202) union(all_87_0, all_31_1) = all_87_1 % 134.06/28.10 | (203) difference(all_17_1, all_17_6) = all_87_0 % 134.06/28.10 | (204) difference(all_87_3, all_87_2) = all_87_1 % 134.06/28.10 | (205) intersection(all_17_1, all_17_6) = all_87_2 % 134.06/28.10 | % 134.06/28.10 | DELTA: instantiating (70) with fresh symbols all_89_0, all_89_1, all_89_2, % 134.06/28.10 | all_89_3 gives: % 134.06/28.11 | (206) intersection(all_17_6, all_17_5) = all_89_2 & difference(all_89_3, % 134.06/28.11 | all_89_2) = all_89_1 & difference(all_17_5, all_17_6) = all_89_0 & % 134.06/28.11 | union(all_27_1, all_89_0) = all_89_1 & union(all_17_6, all_17_5) = % 134.06/28.11 | all_89_3 & $i(all_89_0) & $i(all_89_1) & $i(all_89_2) & $i(all_89_3) % 134.06/28.11 | % 134.06/28.11 | ALPHA: (206) implies: % 134.06/28.11 | (207) $i(all_89_2) % 134.06/28.11 | (208) union(all_17_6, all_17_5) = all_89_3 % 134.06/28.11 | (209) union(all_27_1, all_89_0) = all_89_1 % 134.06/28.11 | (210) difference(all_17_5, all_17_6) = all_89_0 % 134.06/28.11 | (211) difference(all_89_3, all_89_2) = all_89_1 % 134.06/28.11 | (212) intersection(all_17_6, all_17_5) = all_89_2 % 134.06/28.11 | % 134.06/28.11 | DELTA: instantiating (74) with fresh symbols all_93_0, all_93_1, all_93_2, % 134.06/28.11 | all_93_3 gives: % 134.06/28.11 | (213) intersection(all_17_6, all_17_1) = all_93_2 & difference(all_93_3, % 134.06/28.11 | all_93_2) = all_93_1 & difference(all_17_1, all_17_6) = all_93_0 & % 134.06/28.11 | union(all_31_1, all_93_0) = all_93_1 & union(all_17_6, all_17_1) = % 134.06/28.11 | all_93_3 & $i(all_93_0) & $i(all_93_1) & $i(all_93_2) & $i(all_93_3) % 134.06/28.11 | % 134.06/28.11 | ALPHA: (213) implies: % 134.06/28.11 | (214) union(all_17_6, all_17_1) = all_93_3 % 134.06/28.11 | (215) union(all_31_1, all_93_0) = all_93_1 % 134.06/28.11 | (216) difference(all_17_1, all_17_6) = all_93_0 % 134.06/28.11 | (217) difference(all_93_3, all_93_2) = all_93_1 % 134.06/28.11 | (218) intersection(all_17_6, all_17_1) = all_93_2 % 134.06/28.11 | % 134.06/28.11 | DELTA: instantiating (68) with fresh symbols all_97_0, all_97_1, all_97_2, % 134.06/28.11 | all_97_3 gives: % 134.06/28.11 | (219) intersection(all_17_5, all_17_6) = all_97_2 & difference(all_97_3, % 134.06/28.11 | all_97_2) = all_97_1 & difference(all_17_5, all_17_6) = all_97_0 & % 134.06/28.11 | union(all_97_0, all_27_1) = all_97_1 & union(all_17_5, all_17_6) = % 134.06/28.11 | all_97_3 & $i(all_97_0) & $i(all_97_1) & $i(all_97_2) & $i(all_97_3) % 134.06/28.11 | % 134.06/28.11 | ALPHA: (219) implies: % 134.06/28.11 | (220) $i(all_97_2) % 134.06/28.11 | (221) union(all_17_5, all_17_6) = all_97_3 % 134.06/28.11 | (222) union(all_97_0, all_27_1) = all_97_1 % 134.06/28.11 | (223) difference(all_17_5, all_17_6) = all_97_0 % 134.06/28.11 | (224) difference(all_97_3, all_97_2) = all_97_1 % 134.06/28.11 | (225) intersection(all_17_5, all_17_6) = all_97_2 % 134.06/28.11 | % 134.06/28.11 | DELTA: instantiating (67) with fresh symbols all_99_0, all_99_1, all_99_2, % 134.06/28.11 | all_99_3 gives: % 134.06/28.11 | (226) intersection(all_31_1, all_31_0) = all_99_3 & difference(all_31_0, % 134.06/28.11 | all_31_1) = all_99_0 & difference(all_31_1, all_31_0) = all_99_1 & % 134.06/28.11 | difference(all_17_0, all_99_3) = all_99_2 & union(all_99_1, all_99_0) % 134.06/28.11 | = all_99_2 & $i(all_99_0) & $i(all_99_1) & $i(all_99_2) & % 134.06/28.11 | $i(all_99_3) % 134.06/28.11 | % 134.06/28.11 | ALPHA: (226) implies: % 134.06/28.11 | (227) difference(all_31_0, all_31_1) = all_99_0 % 134.06/28.11 | % 134.06/28.11 | DELTA: instantiating (89) with fresh symbols all_101_0, all_101_1, all_101_2, % 134.06/28.11 | all_101_3 gives: % 134.06/28.12 | (228) intersection(all_17_4, all_17_3) = all_101_2 & difference(all_101_3, % 134.06/28.12 | all_101_2) = all_101_1 & difference(all_17_4, all_17_3) = all_101_0 % 134.06/28.12 | & union(all_101_0, all_29_1) = all_101_1 & union(all_17_4, all_17_3) % 134.06/28.12 | = all_101_3 & $i(all_101_0) & $i(all_101_1) & $i(all_101_2) & % 134.06/28.12 | $i(all_101_3) % 134.06/28.12 | % 134.06/28.12 | ALPHA: (228) implies: % 134.06/28.12 | (229) union(all_17_4, all_17_3) = all_101_3 % 134.06/28.12 | (230) union(all_101_0, all_29_1) = all_101_1 % 134.06/28.12 | (231) difference(all_17_4, all_17_3) = all_101_0 % 134.06/28.12 | (232) difference(all_101_3, all_101_2) = all_101_1 % 134.06/28.12 | (233) intersection(all_17_4, all_17_3) = all_101_2 % 134.06/28.12 | % 134.06/28.12 | DELTA: instantiating (86) with fresh symbols all_103_0, all_103_1, all_103_2, % 134.06/28.12 | all_103_3 gives: % 134.06/28.12 | (234) intersection(all_17_4, all_17_3) = all_103_2 & difference(all_103_3, % 134.06/28.12 | all_103_2) = all_103_1 & difference(all_17_3, all_17_4) = all_103_0 % 134.06/28.12 | & union(all_29_0, all_103_0) = all_103_1 & union(all_17_4, all_17_3) % 134.06/28.12 | = all_103_3 & $i(all_103_0) & $i(all_103_1) & $i(all_103_2) & % 134.06/28.12 | $i(all_103_3) % 134.06/28.12 | % 134.06/28.12 | ALPHA: (234) implies: % 134.06/28.12 | (235) union(all_17_4, all_17_3) = all_103_3 % 134.06/28.12 | (236) union(all_29_0, all_103_0) = all_103_1 % 134.06/28.12 | (237) difference(all_17_3, all_17_4) = all_103_0 % 134.06/28.12 | (238) difference(all_103_3, all_103_2) = all_103_1 % 134.06/28.12 | (239) intersection(all_17_4, all_17_3) = all_103_2 % 134.06/28.12 | % 134.06/28.12 | DELTA: instantiating (82) with fresh symbols all_105_0, all_105_1, all_105_2, % 134.06/28.12 | all_105_3 gives: % 134.06/28.12 | (240) intersection(all_17_4, all_17_5) = all_105_2 & difference(all_105_3, % 134.06/28.12 | all_105_2) = all_105_1 & difference(all_17_5, all_17_4) = all_105_0 % 134.06/28.12 | & union(all_25_0, all_105_0) = all_105_1 & union(all_17_4, all_17_5) % 134.06/28.12 | = all_105_3 & $i(all_105_0) & $i(all_105_1) & $i(all_105_2) & % 134.06/28.12 | $i(all_105_3) % 134.06/28.12 | % 134.06/28.12 | ALPHA: (240) implies: % 134.06/28.12 | (241) $i(all_105_2) % 134.06/28.12 | (242) union(all_17_4, all_17_5) = all_105_3 % 134.06/28.12 | (243) union(all_25_0, all_105_0) = all_105_1 % 134.06/28.12 | (244) difference(all_17_5, all_17_4) = all_105_0 % 134.06/28.12 | (245) difference(all_105_3, all_105_2) = all_105_1 % 134.06/28.12 | (246) intersection(all_17_4, all_17_5) = all_105_2 % 134.06/28.12 | % 134.06/28.12 | DELTA: instantiating (81) with fresh symbols all_107_0, all_107_1, all_107_2, % 134.06/28.12 | all_107_3 gives: % 134.06/28.12 | (247) intersection(all_17_5, all_17_4) = all_107_2 & difference(all_107_3, % 134.06/28.12 | all_107_2) = all_107_1 & difference(all_17_5, all_17_4) = all_107_0 % 134.06/28.12 | & union(all_107_0, all_25_0) = all_107_1 & union(all_17_5, all_17_4) % 134.06/28.12 | = all_107_3 & $i(all_107_0) & $i(all_107_1) & $i(all_107_2) & % 134.06/28.12 | $i(all_107_3) % 134.06/28.12 | % 134.06/28.12 | ALPHA: (247) implies: % 134.06/28.12 | (248) $i(all_107_2) % 134.06/28.13 | (249) union(all_17_5, all_17_4) = all_107_3 % 134.06/28.13 | (250) union(all_107_0, all_25_0) = all_107_1 % 134.06/28.13 | (251) difference(all_17_5, all_17_4) = all_107_0 % 134.06/28.13 | (252) difference(all_107_3, all_107_2) = all_107_1 % 134.06/28.13 | (253) intersection(all_17_5, all_17_4) = all_107_2 % 134.06/28.13 | % 134.06/28.13 | DELTA: instantiating (85) with fresh symbols all_109_0, all_109_1, all_109_2, % 134.06/28.13 | all_109_3 gives: % 134.06/28.13 | (254) intersection(all_17_3, all_17_4) = all_109_2 & difference(all_109_3, % 134.06/28.13 | all_109_2) = all_109_1 & difference(all_17_3, all_17_4) = all_109_0 % 134.06/28.13 | & union(all_109_0, all_29_0) = all_109_1 & union(all_17_3, all_17_4) % 134.06/28.13 | = all_109_3 & $i(all_109_0) & $i(all_109_1) & $i(all_109_2) & % 134.06/28.13 | $i(all_109_3) % 134.06/28.13 | % 134.06/28.13 | ALPHA: (254) implies: % 134.06/28.13 | (255) difference(all_17_3, all_17_4) = all_109_0 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (17) with all_75_3, all_89_3, all_17_5, all_17_6, % 134.06/28.13 | simplifying with (177), (208) gives: % 134.06/28.13 | (256) all_89_3 = all_75_3 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (17) with all_79_3, all_93_3, all_17_1, all_17_6, % 134.06/28.13 | simplifying with (182), (214) gives: % 134.06/28.13 | (257) all_93_3 = all_79_3 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (17) with all_73_3, all_97_3, all_17_6, all_17_5, % 134.06/28.13 | simplifying with (171), (221) gives: % 134.06/28.13 | (258) all_97_3 = all_73_3 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (17) with all_83_3, all_107_3, all_17_4, all_17_5, % 134.06/28.13 | simplifying with (190), (249) gives: % 134.06/28.13 | (259) all_107_3 = all_83_3 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (17) with all_85_3, all_105_3, all_17_5, all_17_4, % 134.06/28.13 | simplifying with (195), (242) gives: % 134.06/28.13 | (260) all_105_3 = all_85_3 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (17) with all_101_3, all_103_3, all_17_3, all_17_4, % 134.06/28.13 | simplifying with (229), (235) gives: % 134.06/28.13 | (261) all_103_3 = all_101_3 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (17) with all_71_3, all_87_3, all_17_6, all_17_1, % 134.06/28.13 | simplifying with (165), (201) gives: % 134.06/28.13 | (262) all_87_3 = all_71_3 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (18) with all_55_0, all_67_0, all_17_5, all_17_6, % 134.06/28.13 | simplifying with (133), (156) gives: % 134.06/28.13 | (263) all_67_0 = all_55_0 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (18) with all_67_0, all_73_0, all_17_5, all_17_6, % 134.06/28.13 | simplifying with (156), (173) gives: % 134.06/28.13 | (264) all_73_0 = all_67_0 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (18) with all_27_1, all_75_0, all_17_5, all_17_6, % 134.06/28.13 | simplifying with (54), (178) gives: % 134.06/28.13 | (265) all_75_0 = all_27_1 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (18) with all_73_0, all_75_0, all_17_5, all_17_6, % 134.06/28.13 | simplifying with (173), (178) gives: % 134.06/28.13 | (266) all_75_0 = all_73_0 % 134.06/28.13 | % 134.06/28.13 | GROUND_INST: instantiating (18) with all_57_0, all_59_0, all_17_1, all_17_6, % 134.06/28.13 | simplifying with (138), (141) gives: % 134.06/28.13 | (267) all_59_0 = all_57_0 % 134.06/28.13 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_31_1, all_79_0, all_17_1, all_17_6, % 134.06/28.14 | simplifying with (63), (184) gives: % 134.06/28.14 | (268) all_79_0 = all_31_1 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_71_0, all_79_0, all_17_1, all_17_6, % 134.06/28.14 | simplifying with (167), (184) gives: % 134.06/28.14 | (269) all_79_0 = all_71_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_59_0, all_79_0, all_17_1, all_17_6, % 134.06/28.14 | simplifying with (141), (184) gives: % 134.06/28.14 | (270) all_79_0 = all_59_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_27_0, all_67_1, all_17_6, all_17_5, % 134.06/28.14 | simplifying with (55), (157) gives: % 134.06/28.14 | (271) all_67_1 = all_27_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_67_1, all_89_0, all_17_6, all_17_5, % 134.06/28.14 | simplifying with (157), (210) gives: % 134.06/28.14 | (272) all_89_0 = all_67_1 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_89_0, all_97_0, all_17_6, all_17_5, % 134.06/28.14 | simplifying with (210), (223) gives: % 134.06/28.14 | (273) all_97_0 = all_89_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_47_0, all_97_0, all_17_6, all_17_5, % 134.06/28.14 | simplifying with (116), (223) gives: % 134.06/28.14 | (274) all_97_0 = all_47_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_25_1, all_105_0, all_17_4, all_17_5, % 134.06/28.14 | simplifying with (48), (244) gives: % 134.06/28.14 | (275) all_105_0 = all_25_1 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_65_0, all_105_0, all_17_4, all_17_5, % 134.06/28.14 | simplifying with (153), (244) gives: % 134.06/28.14 | (276) all_105_0 = all_65_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_65_0, all_107_0, all_17_4, all_17_5, % 134.06/28.14 | simplifying with (153), (251) gives: % 134.06/28.14 | (277) all_107_0 = all_65_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_49_0, all_107_0, all_17_4, all_17_5, % 134.06/28.14 | simplifying with (121), (251) gives: % 134.06/28.14 | (278) all_107_0 = all_49_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_25_0, all_65_1, all_17_5, all_17_4, % 134.06/28.14 | simplifying with (49), (154) gives: % 134.06/28.14 | (279) all_65_1 = all_25_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_65_1, all_83_0, all_17_5, all_17_4, % 134.06/28.14 | simplifying with (154), (191) gives: % 134.06/28.14 | (280) all_83_0 = all_65_1 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_83_0, all_85_0, all_17_5, all_17_4, % 134.06/28.14 | simplifying with (191), (197) gives: % 134.06/28.14 | (281) all_85_0 = all_83_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_53_0, all_85_0, all_17_5, all_17_4, % 134.06/28.14 | simplifying with (128), (197) gives: % 134.06/28.14 | (282) all_85_0 = all_53_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_29_0, all_63_1, all_17_3, all_17_4, % 134.06/28.14 | simplifying with (57), (150) gives: % 134.06/28.14 | (283) all_63_1 = all_29_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_81_0, all_101_0, all_17_3, all_17_4, % 134.06/28.14 | simplifying with (188), (231) gives: % 134.06/28.14 | (284) all_101_0 = all_81_0 % 134.06/28.14 | % 134.06/28.14 | GROUND_INST: instantiating (18) with all_63_1, all_101_0, all_17_3, all_17_4, % 134.06/28.14 | simplifying with (150), (231) gives: % 134.06/28.14 | (285) all_101_0 = all_63_1 % 134.06/28.14 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_43_0, all_101_0, all_17_3, all_17_4, % 134.06/28.15 | simplifying with (108), (231) gives: % 134.06/28.15 | (286) all_101_0 = all_43_0 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_29_1, all_63_0, all_17_4, all_17_3, % 134.06/28.15 | simplifying with (58), (151) gives: % 134.06/28.15 | (287) all_63_0 = all_29_1 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_63_0, all_103_0, all_17_4, all_17_3, % 134.06/28.15 | simplifying with (151), (237) gives: % 134.06/28.15 | (288) all_103_0 = all_63_0 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_103_0, all_109_0, all_17_4, all_17_3, % 134.06/28.15 | simplifying with (237), (255) gives: % 134.06/28.15 | (289) all_109_0 = all_103_0 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_45_0, all_109_0, all_17_4, all_17_3, % 134.06/28.15 | simplifying with (112), (255) gives: % 134.06/28.15 | (290) all_109_0 = all_45_0 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_31_0, all_59_1, all_17_6, all_17_1, % 134.06/28.15 | simplifying with (64), (142) gives: % 134.06/28.15 | (291) all_59_1 = all_31_0 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_87_0, all_93_0, all_17_6, all_17_1, % 134.06/28.15 | simplifying with (203), (216) gives: % 134.06/28.15 | (292) all_93_0 = all_87_0 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_59_1, all_93_0, all_17_6, all_17_1, % 134.06/28.15 | simplifying with (142), (216) gives: % 134.06/28.15 | (293) all_93_0 = all_59_1 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (18) with all_51_0, all_93_0, all_17_6, all_17_1, % 134.06/28.15 | simplifying with (124), (216) gives: % 134.06/28.15 | (294) all_93_0 = all_51_0 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (19) with all_17_3, all_55_1, all_17_6, all_17_5, % 134.06/28.15 | simplifying with (33), (134) gives: % 134.06/28.15 | (295) all_55_1 = all_17_3 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (19) with all_47_1, all_55_1, all_17_6, all_17_5, % 134.06/28.15 | simplifying with (117), (134) gives: % 134.06/28.15 | (296) all_55_1 = all_47_1 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (19) with all_17_1, all_53_1, all_17_5, all_17_4, % 134.06/28.15 | simplifying with (39), (129) gives: % 134.06/28.15 | (297) all_53_1 = all_17_1 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (19) with all_49_1, all_53_1, all_17_5, all_17_4, % 134.06/28.15 | simplifying with (122), (129) gives: % 134.06/28.15 | (298) all_53_1 = all_49_1 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (19) with all_17_2, all_45_1, all_17_3, all_17_4, % 134.06/28.15 | simplifying with (42), (113) gives: % 134.06/28.15 | (299) all_45_1 = all_17_2 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (19) with all_43_1, all_45_1, all_17_3, all_17_4, % 134.06/28.15 | simplifying with (109), (113) gives: % 134.06/28.15 | (300) all_45_1 = all_43_1 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (19) with all_17_0, all_57_1, all_17_6, all_17_1, % 134.06/28.15 | simplifying with (36), (139) gives: % 134.06/28.15 | (301) all_57_1 = all_17_0 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (19) with all_51_1, all_57_1, all_17_6, all_17_1, % 134.06/28.15 | simplifying with (125), (139) gives: % 134.06/28.15 | (302) all_57_1 = all_51_1 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (20) with all_75_2, all_89_2, all_17_5, all_17_6, % 134.06/28.15 | simplifying with (180), (212) gives: % 134.06/28.15 | (303) all_89_2 = all_75_2 % 134.06/28.15 | % 134.06/28.15 | GROUND_INST: instantiating (20) with all_79_2, all_93_2, all_17_1, all_17_6, % 134.06/28.15 | simplifying with (186), (218) gives: % 134.06/28.15 | (304) all_93_2 = all_79_2 % 134.06/28.15 | % 134.52/28.15 | GROUND_INST: instantiating (20) with all_73_2, all_97_2, all_17_6, all_17_5, % 134.52/28.15 | simplifying with (175), (225) gives: % 134.52/28.16 | (305) all_97_2 = all_73_2 % 134.52/28.16 | % 134.52/28.16 | GROUND_INST: instantiating (20) with all_83_2, all_107_2, all_17_4, all_17_5, % 134.52/28.16 | simplifying with (193), (253) gives: % 134.52/28.16 | (306) all_107_2 = all_83_2 % 134.52/28.16 | % 134.52/28.16 | GROUND_INST: instantiating (20) with all_85_2, all_105_2, all_17_5, all_17_4, % 134.52/28.16 | simplifying with (199), (246) gives: % 134.52/28.16 | (307) all_105_2 = all_85_2 % 134.52/28.16 | % 134.52/28.16 | GROUND_INST: instantiating (20) with all_101_2, all_103_2, all_17_3, all_17_4, % 134.52/28.16 | simplifying with (233), (239) gives: % 134.52/28.16 | (308) all_103_2 = all_101_2 % 134.52/28.16 | % 134.52/28.16 | GROUND_INST: instantiating (20) with all_71_2, all_87_2, all_17_6, all_17_1, % 134.52/28.16 | simplifying with (169), (205) gives: % 134.52/28.16 | (309) all_87_2 = all_71_2 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (289), (290) imply: % 134.52/28.16 | (310) all_103_0 = all_45_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (310) implies: % 134.52/28.16 | (311) all_103_0 = all_45_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (277), (278) imply: % 134.52/28.16 | (312) all_65_0 = all_49_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (312) implies: % 134.52/28.16 | (313) all_65_0 = all_49_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (275), (276) imply: % 134.52/28.16 | (314) all_65_0 = all_25_1 % 134.52/28.16 | % 134.52/28.16 | SIMP: (314) implies: % 134.52/28.16 | (315) all_65_0 = all_25_1 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (288), (311) imply: % 134.52/28.16 | (316) all_63_0 = all_45_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (316) implies: % 134.52/28.16 | (317) all_63_0 = all_45_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (284), (286) imply: % 134.52/28.16 | (318) all_81_0 = all_43_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (284), (285) imply: % 134.52/28.16 | (319) all_81_0 = all_63_1 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (273), (274) imply: % 134.52/28.16 | (320) all_89_0 = all_47_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (320) implies: % 134.52/28.16 | (321) all_89_0 = all_47_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (292), (293) imply: % 134.52/28.16 | (322) all_87_0 = all_59_1 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (292), (294) imply: % 134.52/28.16 | (323) all_87_0 = all_51_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (272), (321) imply: % 134.52/28.16 | (324) all_67_1 = all_47_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (324) implies: % 134.52/28.16 | (325) all_67_1 = all_47_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (322), (323) imply: % 134.52/28.16 | (326) all_59_1 = all_51_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (326) implies: % 134.52/28.16 | (327) all_59_1 = all_51_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (281), (282) imply: % 134.52/28.16 | (328) all_83_0 = all_53_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (328) implies: % 134.52/28.16 | (329) all_83_0 = all_53_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (280), (329) imply: % 134.52/28.16 | (330) all_65_1 = all_53_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (330) implies: % 134.52/28.16 | (331) all_65_1 = all_53_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (318), (319) imply: % 134.52/28.16 | (332) all_63_1 = all_43_0 % 134.52/28.16 | % 134.52/28.16 | SIMP: (332) implies: % 134.52/28.16 | (333) all_63_1 = all_43_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (268), (269) imply: % 134.52/28.16 | (334) all_71_0 = all_31_1 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (269), (270) imply: % 134.52/28.16 | (335) all_71_0 = all_59_0 % 134.52/28.16 | % 134.52/28.16 | COMBINE_EQS: (265), (266) imply: % 134.52/28.16 | (336) all_73_0 = all_27_1 % 134.52/28.16 | % 134.52/28.16 | SIMP: (336) implies: % 134.52/28.17 | (337) all_73_0 = all_27_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (264), (337) imply: % 134.52/28.17 | (338) all_67_0 = all_27_1 % 134.52/28.17 | % 134.52/28.17 | SIMP: (338) implies: % 134.52/28.17 | (339) all_67_0 = all_27_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (334), (335) imply: % 134.52/28.17 | (340) all_59_0 = all_31_1 % 134.52/28.17 | % 134.52/28.17 | SIMP: (340) implies: % 134.52/28.17 | (341) all_59_0 = all_31_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (263), (339) imply: % 134.52/28.17 | (342) all_55_0 = all_27_1 % 134.52/28.17 | % 134.52/28.17 | SIMP: (342) implies: % 134.52/28.17 | (343) all_55_0 = all_27_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (271), (325) imply: % 134.52/28.17 | (344) all_47_0 = all_27_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (313), (315) imply: % 134.52/28.17 | (345) all_49_0 = all_25_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (279), (331) imply: % 134.52/28.17 | (346) all_53_0 = all_25_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (287), (317) imply: % 134.52/28.17 | (347) all_45_0 = all_29_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (283), (333) imply: % 134.52/28.17 | (348) all_43_0 = all_29_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (267), (341) imply: % 134.52/28.17 | (349) all_57_0 = all_31_1 % 134.52/28.17 | % 134.52/28.17 | SIMP: (349) implies: % 134.52/28.17 | (350) all_57_0 = all_31_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (291), (327) imply: % 134.52/28.17 | (351) all_51_0 = all_31_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (301), (302) imply: % 134.52/28.17 | (352) all_51_1 = all_17_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (295), (296) imply: % 134.52/28.17 | (353) all_47_1 = all_17_3 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (297), (298) imply: % 134.52/28.17 | (354) all_49_1 = all_17_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (299), (300) imply: % 134.52/28.17 | (355) all_43_1 = all_17_2 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (318), (348) imply: % 134.52/28.17 | (356) all_81_0 = all_29_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (282), (346) imply: % 134.52/28.17 | (357) all_85_0 = all_25_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (323), (351) imply: % 134.52/28.17 | (358) all_87_0 = all_31_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (321), (344) imply: % 134.52/28.17 | (359) all_89_0 = all_27_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (292), (358) imply: % 134.52/28.17 | (360) all_93_0 = all_31_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (274), (344) imply: % 134.52/28.17 | (361) all_97_0 = all_27_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (284), (356) imply: % 134.52/28.17 | (362) all_101_0 = all_29_0 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (311), (347) imply: % 134.52/28.17 | (363) all_103_0 = all_29_1 % 134.52/28.17 | % 134.52/28.17 | COMBINE_EQS: (278), (345) imply: % 134.52/28.17 | (364) all_107_0 = all_25_1 % 134.52/28.17 | % 134.52/28.17 | REDUCE: (252), (259), (306) imply: % 134.52/28.17 | (365) difference(all_83_3, all_83_2) = all_107_1 % 134.52/28.17 | % 134.52/28.17 | REDUCE: (245), (260), (307) imply: % 134.52/28.17 | (366) difference(all_85_3, all_85_2) = all_105_1 % 134.52/28.17 | % 134.52/28.17 | REDUCE: (238), (261), (308) imply: % 134.52/28.17 | (367) difference(all_101_3, all_101_2) = all_103_1 % 134.52/28.17 | % 134.52/28.17 | REDUCE: (224), (258), (305) imply: % 134.52/28.18 | (368) difference(all_73_3, all_73_2) = all_97_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (217), (257), (304) imply: % 134.52/28.18 | (369) difference(all_79_3, all_79_2) = all_93_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (211), (256), (303) imply: % 134.52/28.18 | (370) difference(all_75_3, all_75_2) = all_89_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (204), (262), (309) imply: % 134.52/28.18 | (371) difference(all_71_3, all_71_2) = all_87_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (250), (364) imply: % 134.52/28.18 | (372) union(all_25_1, all_25_0) = all_107_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (230), (362) imply: % 134.52/28.18 | (373) union(all_29_0, all_29_1) = all_101_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (222), (361) imply: % 134.52/28.18 | (374) union(all_27_0, all_27_1) = all_97_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (202), (358) imply: % 134.52/28.18 | (375) union(all_31_0, all_31_1) = all_87_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (196), (357) imply: % 134.52/28.18 | (376) union(all_25_0, all_25_1) = all_85_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (183), (268) imply: % 134.52/28.18 | (377) union(all_31_1, all_31_0) = all_79_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (166), (334) imply: % 134.52/28.18 | (378) union(all_31_0, all_31_1) = all_71_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (137), (301), (350) imply: % 134.52/28.18 | (379) union(all_31_0, all_31_1) = all_17_0 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (215), (360) imply: % 134.52/28.18 | (380) union(all_31_1, all_31_0) = all_93_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (236), (363) imply: % 134.52/28.18 | (381) union(all_29_0, all_29_1) = all_103_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (111), (299), (347) imply: % 134.52/28.18 | (382) union(all_29_0, all_29_1) = all_17_2 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (172), (337) imply: % 134.52/28.18 | (383) union(all_27_0, all_27_1) = all_73_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (132), (295), (343) imply: % 134.52/28.18 | (384) union(all_27_0, all_27_1) = all_17_3 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (209), (359) imply: % 134.52/28.18 | (385) union(all_27_1, all_27_0) = all_89_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (243), (275) imply: % 134.52/28.18 | (386) union(all_25_0, all_25_1) = all_105_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (120), (345), (354) imply: % 134.52/28.18 | (387) union(all_25_0, all_25_1) = all_17_1 % 134.52/28.18 | % 134.52/28.18 | REDUCE: (248), (306) imply: % 134.52/28.18 | (388) $i(all_83_2) % 134.52/28.18 | % 134.52/28.18 | REDUCE: (241), (307) imply: % 134.52/28.18 | (389) $i(all_85_2) % 134.52/28.18 | % 134.52/28.18 | REDUCE: (220), (305) imply: % 134.52/28.18 | (390) $i(all_73_2) % 134.52/28.18 | % 134.52/28.18 | REDUCE: (207), (303) imply: % 134.52/28.18 | (391) $i(all_75_2) % 134.52/28.18 | % 134.52/28.18 | REDUCE: (107), (348) imply: % 134.52/28.18 | (392) $i(all_29_0) % 134.52/28.18 | % 134.52/28.18 | GROUND_INST: instantiating (17) with all_17_1, all_107_1, all_25_0, all_25_1, % 134.52/28.18 | simplifying with (47), (372) gives: % 134.52/28.18 | (393) all_107_1 = all_17_1 % 134.52/28.18 | % 134.52/28.18 | GROUND_INST: instantiating (17) with all_17_1, all_105_1, all_25_1, all_25_0, % 134.52/28.18 | simplifying with (386), (387) gives: % 134.52/28.19 | (394) all_105_1 = all_17_1 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (17) with all_17_3, all_89_1, all_27_0, all_27_1, % 134.52/28.19 | simplifying with (53), (385) gives: % 134.52/28.19 | (395) all_89_1 = all_17_3 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (17) with all_17_3, all_97_1, all_27_1, all_27_0, % 134.52/28.19 | simplifying with (374), (384) gives: % 134.52/28.19 | (396) all_97_1 = all_17_3 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (17) with all_17_2, all_103_1, all_29_1, all_29_0, % 134.52/28.19 | simplifying with (381), (382) gives: % 134.52/28.19 | (397) all_103_1 = all_17_2 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (17) with all_17_0, all_93_1, all_31_0, all_31_1, % 134.52/28.19 | simplifying with (62), (380) gives: % 134.52/28.19 | (398) all_93_1 = all_17_0 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (17) with all_17_0, all_87_1, all_31_1, all_31_0, % 134.52/28.19 | simplifying with (375), (379) gives: % 134.52/28.19 | (399) all_87_1 = all_17_0 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (18) with all_71_1, all_87_1, all_71_2, all_71_3, % 134.52/28.19 | simplifying with (168), (371) gives: % 134.52/28.19 | (400) all_87_1 = all_71_1 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (18) with all_73_1, all_97_1, all_73_2, all_73_3, % 134.52/28.19 | simplifying with (174), (368) gives: % 134.52/28.19 | (401) all_97_1 = all_73_1 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (18) with all_75_1, all_89_1, all_75_2, all_75_3, % 134.52/28.19 | simplifying with (179), (370) gives: % 134.52/28.19 | (402) all_89_1 = all_75_1 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (18) with all_79_1, all_93_1, all_79_2, all_79_3, % 134.52/28.19 | simplifying with (185), (369) gives: % 134.52/28.19 | (403) all_93_1 = all_79_1 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (18) with all_83_1, all_107_1, all_83_2, all_83_3, % 134.52/28.19 | simplifying with (192), (365) gives: % 134.52/28.19 | (404) all_107_1 = all_83_1 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (18) with all_85_1, all_105_1, all_85_2, all_85_3, % 134.52/28.19 | simplifying with (198), (366) gives: % 134.52/28.19 | (405) all_105_1 = all_85_1 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (18) with all_101_1, all_103_1, all_101_2, % 134.52/28.19 | all_101_3, simplifying with (232), (367) gives: % 134.52/28.19 | (406) all_103_1 = all_101_1 % 134.52/28.19 | % 134.52/28.19 | COMBINE_EQS: (393), (404) imply: % 134.52/28.19 | (407) all_83_1 = all_17_1 % 134.52/28.19 | % 134.52/28.19 | COMBINE_EQS: (394), (405) imply: % 134.52/28.19 | (408) all_85_1 = all_17_1 % 134.52/28.19 | % 134.52/28.19 | COMBINE_EQS: (397), (406) imply: % 134.52/28.19 | (409) all_101_1 = all_17_2 % 134.52/28.19 | % 134.52/28.19 | COMBINE_EQS: (396), (401) imply: % 134.52/28.19 | (410) all_73_1 = all_17_3 % 134.52/28.19 | % 134.52/28.19 | COMBINE_EQS: (398), (403) imply: % 134.52/28.19 | (411) all_79_1 = all_17_0 % 134.52/28.19 | % 134.52/28.19 | COMBINE_EQS: (395), (402) imply: % 134.52/28.19 | (412) all_75_1 = all_17_3 % 134.52/28.19 | % 134.52/28.19 | COMBINE_EQS: (399), (400) imply: % 134.52/28.19 | (413) all_71_1 = all_17_0 % 134.52/28.19 | % 134.52/28.19 | REDUCE: (198), (408) imply: % 134.52/28.19 | (414) difference(all_85_3, all_85_2) = all_17_1 % 134.52/28.19 | % 134.52/28.19 | REDUCE: (192), (407) imply: % 134.52/28.19 | (415) difference(all_83_3, all_83_2) = all_17_1 % 134.52/28.19 | % 134.52/28.19 | REDUCE: (179), (412) imply: % 134.52/28.19 | (416) difference(all_75_3, all_75_2) = all_17_3 % 134.52/28.19 | % 134.52/28.19 | REDUCE: (174), (410) imply: % 134.52/28.19 | (417) difference(all_73_3, all_73_2) = all_17_3 % 134.52/28.19 | % 134.52/28.19 | GROUND_INST: instantiating (14) with all_17_5, all_17_6, all_75_3, simplifying % 134.52/28.19 | with (23), (24), (177) gives: % 134.52/28.19 | (418) union(all_17_5, all_17_6) = all_75_3 & $i(all_75_3) % 134.52/28.19 | % 134.52/28.19 | ALPHA: (418) implies: % 134.52/28.19 | (419) $i(all_75_3) % 134.52/28.20 | (420) union(all_17_5, all_17_6) = all_75_3 % 134.52/28.20 | % 134.52/28.20 | GROUND_INST: instantiating (14) with all_17_6, all_17_5, all_73_3, simplifying % 134.52/28.20 | with (23), (24), (171) gives: % 134.52/28.20 | (421) union(all_17_6, all_17_5) = all_73_3 & $i(all_73_3) % 134.70/28.20 | % 134.70/28.20 | ALPHA: (421) implies: % 134.70/28.20 | (422) $i(all_73_3) % 134.70/28.20 | % 134.70/28.20 | GROUND_INST: instantiating (14) with all_17_4, all_17_5, all_83_3, simplifying % 134.70/28.20 | with (24), (25), (190) gives: % 134.70/28.20 | (423) union(all_17_4, all_17_5) = all_83_3 & $i(all_83_3) % 134.70/28.20 | % 134.70/28.20 | ALPHA: (423) implies: % 134.70/28.20 | (424) $i(all_83_3) % 134.70/28.20 | % 134.70/28.20 | GROUND_INST: instantiating (14) with all_17_5, all_17_4, all_85_3, simplifying % 134.70/28.20 | with (24), (25), (195) gives: % 134.70/28.20 | (425) union(all_17_5, all_17_4) = all_85_3 & $i(all_85_3) % 134.70/28.20 | % 134.70/28.20 | ALPHA: (425) implies: % 134.70/28.20 | (426) $i(all_85_3) % 134.70/28.20 | (427) union(all_17_5, all_17_4) = all_85_3 % 134.70/28.20 | % 134.70/28.20 | GROUND_INST: instantiating (13) with all_25_0, all_25_1, all_17_6, all_17_1, % 134.70/28.20 | all_31_0, simplifying with (23), (45), (46), (64), (387) gives: % 134.70/28.20 | (428) ? [v0: $i] : ? [v1: $i] : (difference(all_25_0, all_17_6) = v0 & % 134.70/28.20 | difference(all_25_1, all_17_6) = v1 & union(v0, v1) = all_31_0 & % 134.70/28.20 | $i(v1) & $i(v0) & $i(all_31_0)) % 134.70/28.20 | % 134.70/28.20 | GROUND_INST: instantiating (11) with all_17_4, all_27_0, all_27_1, all_17_3, % 134.70/28.20 | all_29_0, simplifying with (25), (51), (52), (57), (384) gives: % 134.70/28.20 | (429) ? [v0: $i] : (difference(v0, all_27_1) = all_29_0 & % 134.70/28.20 | difference(all_17_4, all_27_0) = v0 & $i(v0) & $i(all_29_0)) % 134.70/28.20 | % 134.70/28.20 | GROUND_INST: instantiating (4) with all_29_0, all_61_1, all_61_0, all_29_1, % 134.70/28.20 | all_17_2, simplifying with (144), (145), (146), (382), (392) % 134.70/28.20 | gives: % 134.70/28.20 | (430) ? [v0: $i] : (union(v0, all_61_0) = all_17_2 & union(all_29_0, % 134.70/28.20 | all_61_1) = v0 & $i(v0) & $i(all_17_2)) % 134.70/28.20 | % 134.70/28.20 | GROUND_INST: instantiating (5) with all_69_1, all_69_0, all_31_1, all_31_0, % 134.70/28.20 | all_17_0, simplifying with (60), (159), (160), (161), (379) % 134.70/28.20 | gives: % 134.70/28.20 | (431) ? [v0: $i] : (union(all_69_0, all_31_1) = v0 & union(all_69_1, v0) = % 134.70/28.20 | all_17_0 & $i(v0) & $i(all_17_0)) % 134.70/28.20 | % 134.70/28.20 | GROUND_INST: instantiating (7) with all_17_6, all_17_5, all_17_4, all_25_1, % 134.70/28.20 | all_41_0, simplifying with (23), (24), (25), (48), (104) gives: % 134.70/28.20 | (432) ? [v0: $i] : ? [v1: $i] : (intersection(all_17_6, all_17_4) = v1 & % 134.70/28.21 | difference(all_17_6, all_17_5) = v0 & union(v0, v1) = all_41_0 & % 134.70/28.21 | $i(v1) & $i(v0) & $i(all_41_0)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (10) with all_25_1, all_17_6, all_41_0, simplifying % 134.70/28.21 | with (23), (45), (104) gives: % 134.70/28.21 | (433) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.21 | (intersection(all_25_1, all_17_6) = v1 & difference(v0, v1) = v2 & % 134.70/28.21 | difference(all_25_1, all_17_6) = v3 & union(v3, all_41_0) = v2 & % 134.70/28.21 | union(all_25_1, all_17_6) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (2) with all_25_1, all_17_6, all_41_0, simplifying % 134.70/28.21 | with (23), (45), (104) gives: % 134.70/28.21 | (434) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_25_1, all_17_6) % 134.70/28.21 | = v0 & difference(all_25_1, all_17_6) = v1 & union(v1, all_41_0) = % 134.70/28.21 | v0 & $i(v1) & $i(v0)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (9) with all_17_6, all_25_1, all_41_0, simplifying % 134.70/28.21 | with (23), (45), (104) gives: % 134.70/28.21 | (435) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.21 | (intersection(all_17_6, all_25_1) = v1 & difference(v0, v1) = v2 & % 134.70/28.21 | difference(all_25_1, all_17_6) = v3 & union(all_41_0, v3) = v2 & % 134.70/28.21 | union(all_17_6, all_25_1) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (1) with all_17_6, all_25_1, all_41_0, simplifying % 134.70/28.21 | with (23), (45), (104) gives: % 134.70/28.21 | (436) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_6, all_25_1) % 134.70/28.21 | = v0 & difference(all_25_1, all_17_6) = v1 & union(all_41_0, v1) = % 134.70/28.21 | v0 & $i(v1) & $i(v0)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (7) with all_17_4, all_17_6, all_17_5, all_27_1, % 134.70/28.21 | all_39_0, simplifying with (23), (24), (25), (54), (101) gives: % 134.70/28.21 | (437) ? [v0: $i] : ? [v1: $i] : (intersection(all_17_4, all_17_5) = v1 & % 134.70/28.21 | difference(all_17_4, all_17_6) = v0 & union(v0, v1) = all_39_0 & % 134.70/28.21 | $i(v1) & $i(v0) & $i(all_39_0)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (12) with all_17_5, all_17_4, all_17_6, all_25_1, % 134.70/28.21 | all_69_1, simplifying with (23), (24), (25), (48), (162) gives: % 134.70/28.21 | (438) ? [v0: $i] : (difference(all_17_5, v0) = all_69_1 & union(all_17_4, % 134.70/28.21 | all_17_6) = v0 & $i(v0) & $i(all_69_1)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (12) with all_17_4, all_17_5, all_17_6, all_25_0, % 134.70/28.21 | all_69_0, simplifying with (23), (24), (25), (49), (163) gives: % 134.70/28.21 | (439) ? [v0: $i] : (difference(all_17_4, v0) = all_69_0 & union(all_17_5, % 134.70/28.21 | all_17_6) = v0 & $i(v0) & $i(all_69_0)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (12) with all_17_6, all_17_5, all_17_4, all_27_1, % 134.70/28.21 | all_61_1, simplifying with (23), (24), (25), (54), (147) gives: % 134.70/28.21 | (440) ? [v0: $i] : (difference(all_17_6, v0) = all_61_1 & union(all_17_5, % 134.70/28.21 | all_17_4) = v0 & $i(v0) & $i(all_61_1)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (12) with all_17_5, all_17_6, all_17_4, all_27_0, % 134.70/28.21 | all_61_0, simplifying with (23), (24), (25), (55), (148) gives: % 134.70/28.21 | (441) ? [v0: $i] : (difference(all_17_5, v0) = all_61_0 & union(all_17_6, % 134.70/28.21 | all_17_4) = v0 & $i(v0) & $i(all_61_0)) % 134.70/28.21 | % 134.70/28.21 | GROUND_INST: instantiating (10) with all_17_4, all_27_0, all_61_0, simplifying % 134.70/28.21 | with (25), (52), (148) gives: % 134.70/28.22 | (442) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.22 | (intersection(all_17_4, all_27_0) = v1 & difference(v0, v1) = v2 & % 134.70/28.22 | difference(all_17_4, all_27_0) = v3 & union(v3, all_61_0) = v2 & % 134.70/28.22 | union(all_17_4, all_27_0) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (2) with all_17_4, all_27_0, all_61_0, simplifying % 134.70/28.22 | with (25), (52), (148) gives: % 134.70/28.22 | (443) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_17_4, all_27_0) % 134.70/28.22 | = v0 & difference(all_17_4, all_27_0) = v1 & union(v1, all_61_0) = % 134.70/28.22 | v0 & $i(v1) & $i(v0)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (9) with all_27_0, all_17_4, all_61_0, simplifying % 134.70/28.22 | with (25), (52), (148) gives: % 134.70/28.22 | (444) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.22 | (intersection(all_27_0, all_17_4) = v1 & difference(v0, v1) = v2 & % 134.70/28.22 | difference(all_17_4, all_27_0) = v3 & union(all_61_0, v3) = v2 & % 134.70/28.22 | union(all_27_0, all_17_4) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (1) with all_27_0, all_17_4, all_61_0, simplifying % 134.70/28.22 | with (25), (52), (148) gives: % 134.70/28.22 | (445) ? [v0: $i] : ? [v1: $i] : (symmetric_difference(all_27_0, all_17_4) % 134.70/28.22 | = v0 & difference(all_17_4, all_27_0) = v1 & union(all_61_0, v1) = % 134.70/28.22 | v0 & $i(v1) & $i(v0)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (13) with all_69_1, all_69_0, all_31_1, all_31_0, % 134.70/28.22 | all_99_0, simplifying with (60), (159), (160), (161), (227) % 134.70/28.22 | gives: % 134.70/28.22 | (446) ? [v0: $i] : ? [v1: $i] : (difference(all_69_0, all_31_1) = v1 & % 134.70/28.22 | difference(all_69_1, all_31_1) = v0 & union(v0, v1) = all_99_0 & % 134.70/28.22 | $i(v1) & $i(v0) & $i(all_99_0)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (7) with all_41_0, all_17_4, all_17_5, all_25_0, % 134.70/28.22 | all_31_1, simplifying with (24), (25), (49), (103), (105) gives: % 134.70/28.22 | (447) ? [v0: $i] : ? [v1: $i] : (intersection(all_41_0, all_17_5) = v1 & % 134.70/28.22 | difference(all_41_0, all_17_4) = v0 & union(v0, v1) = all_31_1 & % 134.70/28.22 | $i(v1) & $i(v0) & $i(all_31_1)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (7) with all_17_4, all_73_3, all_73_2, all_17_3, % 134.70/28.22 | all_29_0, simplifying with (25), (57), (390), (417), (422) gives: % 134.70/28.22 | (448) ? [v0: $i] : ? [v1: $i] : (intersection(all_17_4, all_73_2) = v1 & % 134.70/28.22 | difference(all_17_4, all_73_3) = v0 & union(v0, v1) = all_29_0 & % 134.70/28.22 | $i(v1) & $i(v0) & $i(all_29_0)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (7) with all_17_4, all_75_3, all_75_2, all_17_3, % 134.70/28.22 | all_29_0, simplifying with (25), (57), (391), (416), (419) gives: % 134.70/28.22 | (449) ? [v0: $i] : ? [v1: $i] : (intersection(all_17_4, all_75_2) = v1 & % 134.70/28.22 | difference(all_17_4, all_75_3) = v0 & union(v0, v1) = all_29_0 & % 134.70/28.22 | $i(v1) & $i(v0) & $i(all_29_0)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (7) with all_17_6, all_83_3, all_83_2, all_17_1, % 134.70/28.22 | all_31_1, simplifying with (23), (63), (388), (415), (424) gives: % 134.70/28.22 | (450) ? [v0: $i] : ? [v1: $i] : (intersection(all_17_6, all_83_2) = v1 & % 134.70/28.22 | difference(all_17_6, all_83_3) = v0 & union(v0, v1) = all_31_1 & % 134.70/28.22 | $i(v1) & $i(v0) & $i(all_31_1)) % 134.70/28.22 | % 134.70/28.22 | GROUND_INST: instantiating (7) with all_17_6, all_85_3, all_85_2, all_17_1, % 134.70/28.22 | all_31_1, simplifying with (23), (63), (389), (414), (426) gives: % 134.70/28.23 | (451) ? [v0: $i] : ? [v1: $i] : (intersection(all_17_6, all_85_2) = v1 & % 134.70/28.23 | difference(all_17_6, all_85_3) = v0 & union(v0, v1) = all_31_1 & % 134.70/28.23 | $i(v1) & $i(v0) & $i(all_31_1)) % 134.70/28.23 | % 134.70/28.23 | GROUND_INST: instantiating (15) with all_17_5, all_17_6, all_75_2, simplifying % 134.70/28.23 | with (23), (24), (180) gives: % 134.70/28.23 | (452) intersection(all_17_5, all_17_6) = all_75_2 & $i(all_75_2) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (452) implies: % 134.70/28.23 | (453) intersection(all_17_5, all_17_6) = all_75_2 % 134.70/28.23 | % 134.70/28.23 | GROUND_INST: instantiating (15) with all_17_4, all_17_5, all_83_2, simplifying % 134.70/28.23 | with (24), (25), (193) gives: % 134.70/28.23 | (454) intersection(all_17_4, all_17_5) = all_83_2 & $i(all_83_2) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (454) implies: % 134.70/28.23 | (455) intersection(all_17_4, all_17_5) = all_83_2 % 134.70/28.23 | % 134.70/28.23 | DELTA: instantiating (440) with fresh symbol all_131_0 gives: % 134.70/28.23 | (456) difference(all_17_6, all_131_0) = all_61_1 & union(all_17_5, % 134.70/28.23 | all_17_4) = all_131_0 & $i(all_131_0) & $i(all_61_1) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (456) implies: % 134.70/28.23 | (457) union(all_17_5, all_17_4) = all_131_0 % 134.70/28.23 | (458) difference(all_17_6, all_131_0) = all_61_1 % 134.70/28.23 | % 134.70/28.23 | DELTA: instantiating (431) with fresh symbol all_141_0 gives: % 134.70/28.23 | (459) union(all_69_0, all_31_1) = all_141_0 & union(all_69_1, all_141_0) = % 134.70/28.23 | all_17_0 & $i(all_141_0) & $i(all_17_0) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (459) implies: % 134.70/28.23 | (460) union(all_69_0, all_31_1) = all_141_0 % 134.70/28.23 | % 134.70/28.23 | DELTA: instantiating (429) with fresh symbol all_143_0 gives: % 134.70/28.23 | (461) difference(all_143_0, all_27_1) = all_29_0 & difference(all_17_4, % 134.70/28.23 | all_27_0) = all_143_0 & $i(all_143_0) & $i(all_29_0) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (461) implies: % 134.70/28.23 | (462) difference(all_17_4, all_27_0) = all_143_0 % 134.70/28.23 | % 134.70/28.23 | DELTA: instantiating (438) with fresh symbol all_145_0 gives: % 134.70/28.23 | (463) difference(all_17_5, all_145_0) = all_69_1 & union(all_17_4, % 134.70/28.23 | all_17_6) = all_145_0 & $i(all_145_0) & $i(all_69_1) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (463) implies: % 134.70/28.23 | (464) union(all_17_4, all_17_6) = all_145_0 % 134.70/28.23 | (465) difference(all_17_5, all_145_0) = all_69_1 % 134.70/28.23 | % 134.70/28.23 | DELTA: instantiating (439) with fresh symbol all_147_0 gives: % 134.70/28.23 | (466) difference(all_17_4, all_147_0) = all_69_0 & union(all_17_5, % 134.70/28.23 | all_17_6) = all_147_0 & $i(all_147_0) & $i(all_69_0) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (466) implies: % 134.70/28.23 | (467) union(all_17_5, all_17_6) = all_147_0 % 134.70/28.23 | (468) difference(all_17_4, all_147_0) = all_69_0 % 134.70/28.23 | % 134.70/28.23 | DELTA: instantiating (430) with fresh symbol all_151_0 gives: % 134.70/28.23 | (469) union(all_151_0, all_61_0) = all_17_2 & union(all_29_0, all_61_1) = % 134.70/28.23 | all_151_0 & $i(all_151_0) & $i(all_17_2) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (469) implies: % 134.70/28.23 | (470) union(all_29_0, all_61_1) = all_151_0 % 134.70/28.23 | (471) union(all_151_0, all_61_0) = all_17_2 % 134.70/28.23 | % 134.70/28.23 | DELTA: instantiating (441) with fresh symbol all_157_0 gives: % 134.70/28.23 | (472) difference(all_17_5, all_157_0) = all_61_0 & union(all_17_6, % 134.70/28.23 | all_17_4) = all_157_0 & $i(all_157_0) & $i(all_61_0) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (472) implies: % 134.70/28.23 | (473) union(all_17_6, all_17_4) = all_157_0 % 134.70/28.23 | (474) difference(all_17_5, all_157_0) = all_61_0 % 134.70/28.23 | % 134.70/28.23 | DELTA: instantiating (443) with fresh symbols all_211_0, all_211_1 gives: % 134.70/28.23 | (475) symmetric_difference(all_17_4, all_27_0) = all_211_1 & % 134.70/28.23 | difference(all_17_4, all_27_0) = all_211_0 & union(all_211_0, % 134.70/28.23 | all_61_0) = all_211_1 & $i(all_211_0) & $i(all_211_1) % 134.70/28.23 | % 134.70/28.23 | ALPHA: (475) implies: % 134.70/28.24 | (476) difference(all_17_4, all_27_0) = all_211_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (445) with fresh symbols all_231_0, all_231_1 gives: % 134.70/28.24 | (477) symmetric_difference(all_27_0, all_17_4) = all_231_1 & % 134.70/28.24 | difference(all_17_4, all_27_0) = all_231_0 & union(all_61_0, % 134.70/28.24 | all_231_0) = all_231_1 & $i(all_231_0) & $i(all_231_1) % 134.70/28.24 | % 134.70/28.24 | ALPHA: (477) implies: % 134.70/28.24 | (478) difference(all_17_4, all_27_0) = all_231_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (436) with fresh symbols all_307_0, all_307_1 gives: % 134.70/28.24 | (479) symmetric_difference(all_17_6, all_25_1) = all_307_1 & % 134.70/28.24 | difference(all_25_1, all_17_6) = all_307_0 & union(all_41_0, % 134.70/28.24 | all_307_0) = all_307_1 & $i(all_307_0) & $i(all_307_1) % 134.70/28.24 | % 134.70/28.24 | ALPHA: (479) implies: % 134.70/28.24 | (480) $i(all_307_0) % 134.70/28.24 | (481) difference(all_25_1, all_17_6) = all_307_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (434) with fresh symbols all_315_0, all_315_1 gives: % 134.70/28.24 | (482) symmetric_difference(all_25_1, all_17_6) = all_315_1 & % 134.70/28.24 | difference(all_25_1, all_17_6) = all_315_0 & union(all_315_0, % 134.70/28.24 | all_41_0) = all_315_1 & $i(all_315_0) & $i(all_315_1) % 134.70/28.24 | % 134.70/28.24 | ALPHA: (482) implies: % 134.70/28.24 | (483) difference(all_25_1, all_17_6) = all_315_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (437) with fresh symbols all_321_0, all_321_1 gives: % 134.70/28.24 | (484) intersection(all_17_4, all_17_5) = all_321_0 & difference(all_17_4, % 134.70/28.24 | all_17_6) = all_321_1 & union(all_321_1, all_321_0) = all_39_0 & % 134.70/28.24 | $i(all_321_0) & $i(all_321_1) & $i(all_39_0) % 134.70/28.24 | % 134.70/28.24 | ALPHA: (484) implies: % 134.70/28.24 | (485) difference(all_17_4, all_17_6) = all_321_1 % 134.70/28.24 | (486) intersection(all_17_4, all_17_5) = all_321_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (446) with fresh symbols all_323_0, all_323_1 gives: % 134.70/28.24 | (487) difference(all_69_0, all_31_1) = all_323_0 & difference(all_69_1, % 134.70/28.24 | all_31_1) = all_323_1 & union(all_323_1, all_323_0) = all_99_0 & % 134.70/28.24 | $i(all_323_0) & $i(all_323_1) & $i(all_99_0) % 134.70/28.24 | % 134.70/28.24 | ALPHA: (487) implies: % 134.70/28.24 | (488) difference(all_69_0, all_31_1) = all_323_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (450) with fresh symbols all_327_0, all_327_1 gives: % 134.70/28.24 | (489) intersection(all_17_6, all_83_2) = all_327_0 & difference(all_17_6, % 134.70/28.24 | all_83_3) = all_327_1 & union(all_327_1, all_327_0) = all_31_1 & % 134.70/28.24 | $i(all_327_0) & $i(all_327_1) & $i(all_31_1) % 134.70/28.24 | % 134.70/28.24 | ALPHA: (489) implies: % 134.70/28.24 | (490) $i(all_327_1) % 134.70/28.24 | (491) union(all_327_1, all_327_0) = all_31_1 % 134.70/28.24 | (492) difference(all_17_6, all_83_3) = all_327_1 % 134.70/28.24 | (493) intersection(all_17_6, all_83_2) = all_327_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (432) with fresh symbols all_329_0, all_329_1 gives: % 134.70/28.24 | (494) intersection(all_17_6, all_17_4) = all_329_0 & difference(all_17_6, % 134.70/28.24 | all_17_5) = all_329_1 & union(all_329_1, all_329_0) = all_41_0 & % 134.70/28.24 | $i(all_329_0) & $i(all_329_1) & $i(all_41_0) % 134.70/28.24 | % 134.70/28.24 | ALPHA: (494) implies: % 134.70/28.24 | (495) intersection(all_17_6, all_17_4) = all_329_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (449) with fresh symbols all_339_0, all_339_1 gives: % 134.70/28.24 | (496) intersection(all_17_4, all_75_2) = all_339_0 & difference(all_17_4, % 134.70/28.24 | all_75_3) = all_339_1 & union(all_339_1, all_339_0) = all_29_0 & % 134.70/28.24 | $i(all_339_0) & $i(all_339_1) & $i(all_29_0) % 134.70/28.24 | % 134.70/28.24 | ALPHA: (496) implies: % 134.70/28.24 | (497) $i(all_339_1) % 134.70/28.24 | (498) union(all_339_1, all_339_0) = all_29_0 % 134.70/28.24 | (499) difference(all_17_4, all_75_3) = all_339_1 % 134.70/28.24 | (500) intersection(all_17_4, all_75_2) = all_339_0 % 134.70/28.24 | % 134.70/28.24 | DELTA: instantiating (428) with fresh symbols all_363_0, all_363_1 gives: % 134.70/28.25 | (501) difference(all_25_0, all_17_6) = all_363_1 & difference(all_25_1, % 134.70/28.25 | all_17_6) = all_363_0 & union(all_363_1, all_363_0) = all_31_0 & % 134.70/28.25 | $i(all_363_0) & $i(all_363_1) & $i(all_31_0) % 134.70/28.25 | % 134.70/28.25 | ALPHA: (501) implies: % 134.70/28.25 | (502) union(all_363_1, all_363_0) = all_31_0 % 134.70/28.25 | (503) difference(all_25_1, all_17_6) = all_363_0 % 134.70/28.25 | (504) difference(all_25_0, all_17_6) = all_363_1 % 134.70/28.25 | % 134.70/28.25 | DELTA: instantiating (451) with fresh symbols all_379_0, all_379_1 gives: % 134.70/28.25 | (505) intersection(all_17_6, all_85_2) = all_379_0 & difference(all_17_6, % 134.70/28.25 | all_85_3) = all_379_1 & union(all_379_1, all_379_0) = all_31_1 & % 134.70/28.25 | $i(all_379_0) & $i(all_379_1) & $i(all_31_1) % 134.70/28.25 | % 134.70/28.25 | ALPHA: (505) implies: % 134.70/28.25 | (506) $i(all_379_0) % 134.70/28.25 | (507) difference(all_17_6, all_85_3) = all_379_1 % 134.70/28.25 | (508) intersection(all_17_6, all_85_2) = all_379_0 % 134.70/28.25 | % 134.70/28.25 | DELTA: instantiating (448) with fresh symbols all_387_0, all_387_1 gives: % 134.70/28.25 | (509) intersection(all_17_4, all_73_2) = all_387_0 & difference(all_17_4, % 134.70/28.25 | all_73_3) = all_387_1 & union(all_387_1, all_387_0) = all_29_0 & % 134.70/28.25 | $i(all_387_0) & $i(all_387_1) & $i(all_29_0) % 134.70/28.25 | % 134.70/28.25 | ALPHA: (509) implies: % 134.70/28.25 | (510) $i(all_387_0) % 134.70/28.25 | (511) difference(all_17_4, all_73_3) = all_387_1 % 134.70/28.25 | (512) intersection(all_17_4, all_73_2) = all_387_0 % 134.70/28.25 | % 134.70/28.25 | DELTA: instantiating (447) with fresh symbols all_391_0, all_391_1 gives: % 134.70/28.25 | (513) intersection(all_41_0, all_17_5) = all_391_0 & difference(all_41_0, % 134.70/28.25 | all_17_4) = all_391_1 & union(all_391_1, all_391_0) = all_31_1 & % 134.70/28.25 | $i(all_391_0) & $i(all_391_1) & $i(all_31_1) % 134.70/28.25 | % 134.70/28.25 | ALPHA: (513) implies: % 134.70/28.25 | (514) $i(all_391_1) % 134.70/28.25 | (515) $i(all_391_0) % 134.70/28.25 | (516) union(all_391_1, all_391_0) = all_31_1 % 134.70/28.25 | % 134.70/28.25 | DELTA: instantiating (435) with fresh symbols all_409_0, all_409_1, all_409_2, % 134.70/28.25 | all_409_3 gives: % 134.70/28.25 | (517) intersection(all_17_6, all_25_1) = all_409_2 & difference(all_409_3, % 134.70/28.25 | all_409_2) = all_409_1 & difference(all_25_1, all_17_6) = all_409_0 % 134.70/28.25 | & union(all_41_0, all_409_0) = all_409_1 & union(all_17_6, all_25_1) % 134.70/28.25 | = all_409_3 & $i(all_409_0) & $i(all_409_1) & $i(all_409_2) & % 134.70/28.25 | $i(all_409_3) % 134.70/28.25 | % 134.70/28.25 | ALPHA: (517) implies: % 134.70/28.25 | (518) difference(all_25_1, all_17_6) = all_409_0 % 134.70/28.25 | % 134.70/28.25 | DELTA: instantiating (433) with fresh symbols all_411_0, all_411_1, all_411_2, % 134.70/28.25 | all_411_3 gives: % 134.70/28.25 | (519) intersection(all_25_1, all_17_6) = all_411_2 & difference(all_411_3, % 134.70/28.25 | all_411_2) = all_411_1 & difference(all_25_1, all_17_6) = all_411_0 % 134.70/28.25 | & union(all_411_0, all_41_0) = all_411_1 & union(all_25_1, all_17_6) % 134.70/28.25 | = all_411_3 & $i(all_411_0) & $i(all_411_1) & $i(all_411_2) & % 134.70/28.25 | $i(all_411_3) % 134.70/28.25 | % 134.70/28.25 | ALPHA: (519) implies: % 134.70/28.25 | (520) difference(all_25_1, all_17_6) = all_411_0 % 134.70/28.25 | % 134.70/28.25 | DELTA: instantiating (444) with fresh symbols all_487_0, all_487_1, all_487_2, % 134.70/28.25 | all_487_3 gives: % 134.70/28.25 | (521) intersection(all_27_0, all_17_4) = all_487_2 & difference(all_487_3, % 134.70/28.25 | all_487_2) = all_487_1 & difference(all_17_4, all_27_0) = all_487_0 % 134.70/28.25 | & union(all_61_0, all_487_0) = all_487_1 & union(all_27_0, all_17_4) % 134.70/28.25 | = all_487_3 & $i(all_487_0) & $i(all_487_1) & $i(all_487_2) & % 134.70/28.25 | $i(all_487_3) % 134.70/28.25 | % 134.70/28.25 | ALPHA: (521) implies: % 134.70/28.25 | (522) difference(all_17_4, all_27_0) = all_487_0 % 134.70/28.25 | % 134.70/28.25 | DELTA: instantiating (442) with fresh symbols all_499_0, all_499_1, all_499_2, % 134.70/28.25 | all_499_3 gives: % 134.70/28.25 | (523) intersection(all_17_4, all_27_0) = all_499_2 & difference(all_499_3, % 134.70/28.25 | all_499_2) = all_499_1 & difference(all_17_4, all_27_0) = all_499_0 % 134.70/28.25 | & union(all_499_0, all_61_0) = all_499_1 & union(all_17_4, all_27_0) % 134.70/28.25 | = all_499_3 & $i(all_499_0) & $i(all_499_1) & $i(all_499_2) & % 134.70/28.25 | $i(all_499_3) % 134.70/28.25 | % 134.70/28.25 | ALPHA: (523) implies: % 134.70/28.25 | (524) difference(all_17_4, all_27_0) = all_499_0 % 134.70/28.25 | % 134.70/28.25 | GROUND_INST: instantiating (17) with all_73_3, all_147_0, all_17_6, all_17_5, % 134.70/28.25 | simplifying with (171), (467) gives: % 134.70/28.25 | (525) all_147_0 = all_73_3 % 134.70/28.25 | % 134.70/28.25 | GROUND_INST: instantiating (17) with all_75_3, all_147_0, all_17_6, all_17_5, % 134.70/28.25 | simplifying with (420), (467) gives: % 134.70/28.25 | (526) all_147_0 = all_75_3 % 134.70/28.25 | % 134.70/28.25 | GROUND_INST: instantiating (17) with all_83_3, all_131_0, all_17_4, all_17_5, % 134.70/28.25 | simplifying with (190), (457) gives: % 134.70/28.25 | (527) all_131_0 = all_83_3 % 134.70/28.25 | % 134.70/28.25 | GROUND_INST: instantiating (17) with all_85_3, all_131_0, all_17_4, all_17_5, % 134.70/28.25 | simplifying with (427), (457) gives: % 134.70/28.25 | (528) all_131_0 = all_85_3 % 134.70/28.25 | % 134.70/28.25 | GROUND_INST: instantiating (18) with all_143_0, all_231_0, all_27_0, all_17_4, % 134.70/28.25 | simplifying with (462), (478) gives: % 134.70/28.25 | (529) all_231_0 = all_143_0 % 134.70/28.25 | % 134.70/28.25 | GROUND_INST: instantiating (18) with all_487_0, all_499_0, all_27_0, all_17_4, % 134.70/28.25 | simplifying with (522), (524) gives: % 134.70/28.25 | (530) all_499_0 = all_487_0 % 134.70/28.25 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_231_0, all_499_0, all_27_0, all_17_4, % 134.70/28.26 | simplifying with (478), (524) gives: % 134.70/28.26 | (531) all_499_0 = all_231_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_211_0, all_499_0, all_27_0, all_17_4, % 134.70/28.26 | simplifying with (476), (524) gives: % 134.70/28.26 | (532) all_499_0 = all_211_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_363_0, all_409_0, all_17_6, all_25_1, % 134.70/28.26 | simplifying with (503), (518) gives: % 134.70/28.26 | (533) all_409_0 = all_363_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_315_0, all_409_0, all_17_6, all_25_1, % 134.70/28.26 | simplifying with (483), (518) gives: % 134.70/28.26 | (534) all_409_0 = all_315_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_307_0, all_409_0, all_17_6, all_25_1, % 134.70/28.26 | simplifying with (481), (518) gives: % 134.70/28.26 | (535) all_409_0 = all_307_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_69_1, all_411_0, all_17_6, all_25_1, % 134.70/28.26 | simplifying with (162), (520) gives: % 134.70/28.26 | (536) all_411_0 = all_69_1 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_409_0, all_411_0, all_17_6, all_25_1, % 134.70/28.26 | simplifying with (518), (520) gives: % 134.70/28.26 | (537) all_411_0 = all_409_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_69_0, all_363_1, all_17_6, all_25_0, % 134.70/28.26 | simplifying with (163), (504) gives: % 134.70/28.26 | (538) all_363_1 = all_69_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (20) with all_73_2, all_75_2, all_17_6, all_17_5, % 134.70/28.26 | simplifying with (175), (453) gives: % 134.70/28.26 | (539) all_75_2 = all_73_2 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (20) with all_85_2, all_321_0, all_17_5, all_17_4, % 134.70/28.26 | simplifying with (199), (486) gives: % 134.70/28.26 | (540) all_321_0 = all_85_2 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (20) with all_83_2, all_321_0, all_17_5, all_17_4, % 134.70/28.26 | simplifying with (455), (486) gives: % 134.70/28.26 | (541) all_321_0 = all_83_2 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (530), (532) imply: % 134.70/28.26 | (542) all_487_0 = all_211_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (530), (531) imply: % 134.70/28.26 | (543) all_487_0 = all_231_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (542), (543) imply: % 134.70/28.26 | (544) all_231_0 = all_211_0 % 134.70/28.26 | % 134.70/28.26 | SIMP: (544) implies: % 134.70/28.26 | (545) all_231_0 = all_211_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (536), (537) imply: % 134.70/28.26 | (546) all_409_0 = all_69_1 % 134.70/28.26 | % 134.70/28.26 | SIMP: (546) implies: % 134.70/28.26 | (547) all_409_0 = all_69_1 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (533), (535) imply: % 134.70/28.26 | (548) all_363_0 = all_307_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (533), (547) imply: % 134.70/28.26 | (549) all_363_0 = all_69_1 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (533), (534) imply: % 134.70/28.26 | (550) all_363_0 = all_315_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (548), (550) imply: % 134.70/28.26 | (551) all_315_0 = all_307_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (549), (550) imply: % 134.70/28.26 | (552) all_315_0 = all_69_1 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (540), (541) imply: % 134.70/28.26 | (553) all_85_2 = all_83_2 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (551), (552) imply: % 134.70/28.26 | (554) all_307_0 = all_69_1 % 134.70/28.26 | % 134.70/28.26 | SIMP: (554) implies: % 134.70/28.26 | (555) all_307_0 = all_69_1 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (529), (545) imply: % 134.70/28.26 | (556) all_211_0 = all_143_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (525), (526) imply: % 134.70/28.26 | (557) all_75_3 = all_73_3 % 134.70/28.26 | % 134.70/28.26 | SIMP: (557) implies: % 134.70/28.26 | (558) all_75_3 = all_73_3 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (527), (528) imply: % 134.70/28.26 | (559) all_85_3 = all_83_3 % 134.70/28.26 | % 134.70/28.26 | SIMP: (559) implies: % 134.70/28.26 | (560) all_85_3 = all_83_3 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (500), (539) imply: % 134.70/28.26 | (561) intersection(all_17_4, all_73_2) = all_339_0 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (508), (553) imply: % 134.70/28.26 | (562) intersection(all_17_6, all_83_2) = all_379_0 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (180), (539) imply: % 134.70/28.26 | (563) intersection(all_17_6, all_17_5) = all_73_2 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (468), (525) imply: % 134.70/28.26 | (564) difference(all_17_4, all_73_3) = all_69_0 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (499), (558) imply: % 134.70/28.26 | (565) difference(all_17_4, all_73_3) = all_339_1 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (458), (527) imply: % 134.70/28.26 | (566) difference(all_17_6, all_83_3) = all_61_1 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (507), (560) imply: % 134.70/28.26 | (567) difference(all_17_6, all_83_3) = all_379_1 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (502), (538), (549) imply: % 134.70/28.26 | (568) union(all_69_0, all_69_1) = all_31_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_327_1, all_379_1, all_83_3, all_17_6, % 134.70/28.26 | simplifying with (492), (567) gives: % 134.70/28.26 | (569) all_379_1 = all_327_1 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_61_1, all_379_1, all_83_3, all_17_6, % 134.70/28.26 | simplifying with (566), (567) gives: % 134.70/28.26 | (570) all_379_1 = all_61_1 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_387_1, all_69_0, all_73_3, all_17_4, % 134.70/28.26 | simplifying with (511), (564) gives: % 134.70/28.26 | (571) all_387_1 = all_69_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (18) with all_387_1, all_339_1, all_73_3, all_17_4, % 134.70/28.26 | simplifying with (511), (565) gives: % 134.70/28.26 | (572) all_387_1 = all_339_1 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (20) with all_327_0, all_379_0, all_83_2, all_17_6, % 134.70/28.26 | simplifying with (493), (562) gives: % 134.70/28.26 | (573) all_379_0 = all_327_0 % 134.70/28.26 | % 134.70/28.26 | GROUND_INST: instantiating (20) with all_387_0, all_339_0, all_73_2, all_17_4, % 134.70/28.26 | simplifying with (512), (561) gives: % 134.70/28.26 | (574) all_387_0 = all_339_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (571), (572) imply: % 134.70/28.26 | (575) all_339_1 = all_69_0 % 134.70/28.26 | % 134.70/28.26 | COMBINE_EQS: (569), (570) imply: % 134.70/28.26 | (576) all_327_1 = all_61_1 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (498), (575) imply: % 134.70/28.26 | (577) union(all_69_0, all_339_0) = all_29_0 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (491), (576) imply: % 134.70/28.26 | (578) union(all_61_1, all_327_0) = all_31_1 % 134.70/28.26 | % 134.70/28.26 | REDUCE: (510), (574) imply: % 134.70/28.26 | (579) $i(all_339_0) % 134.70/28.26 | % 134.70/28.26 | REDUCE: (506), (573) imply: % 134.70/28.27 | (580) $i(all_327_0) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (14) with all_17_4, all_17_6, all_157_0, % 134.70/28.27 | simplifying with (23), (25), (473) gives: % 134.70/28.27 | (581) union(all_17_4, all_17_6) = all_157_0 & $i(all_157_0) % 134.70/28.27 | % 134.70/28.27 | ALPHA: (581) implies: % 134.70/28.27 | (582) union(all_17_4, all_17_6) = all_157_0 % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (8) with all_17_6, all_17_4, all_157_0, simplifying % 134.70/28.27 | with (23), (25), (473) gives: % 134.70/28.27 | (583) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.27 | (intersection(all_17_6, all_17_4) = v0 & difference(all_157_0, v0) = % 134.70/28.27 | v1 & difference(all_17_4, all_17_6) = v3 & difference(all_17_6, % 134.70/28.27 | all_17_4) = v2 & union(v2, v3) = v1 & $i(v3) & $i(v2) & $i(v1) & % 134.70/28.27 | $i(v0)) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (8) with all_17_4, all_17_6, all_145_0, simplifying % 134.70/28.27 | with (23), (25), (464) gives: % 134.70/28.27 | (584) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.27 | (intersection(all_17_4, all_17_6) = v0 & difference(all_145_0, v0) = % 134.70/28.27 | v1 & difference(all_17_4, all_17_6) = v2 & difference(all_17_6, % 134.70/28.27 | all_17_4) = v3 & union(v2, v3) = v1 & $i(v3) & $i(v2) & $i(v1) & % 134.70/28.27 | $i(v0)) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (14) with all_327_0, all_61_1, all_31_1, % 134.70/28.27 | simplifying with (144), (578), (580) gives: % 134.70/28.27 | (585) union(all_327_0, all_61_1) = all_31_1 & $i(all_31_1) % 134.70/28.27 | % 134.70/28.27 | ALPHA: (585) implies: % 134.70/28.27 | (586) union(all_327_0, all_61_1) = all_31_1 % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (14) with all_31_1, all_69_0, all_141_0, % 134.70/28.27 | simplifying with (60), (160), (460) gives: % 134.70/28.27 | (587) union(all_31_1, all_69_0) = all_141_0 & $i(all_141_0) % 134.70/28.27 | % 134.70/28.27 | ALPHA: (587) implies: % 134.70/28.27 | (588) union(all_31_1, all_69_0) = all_141_0 % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (4) with all_31_1, all_69_0, all_69_1, all_31_0, % 134.70/28.27 | all_17_0, simplifying with (60), (62), (159), (160), (568) gives: % 134.70/28.27 | (589) ? [v0: $i] : (union(v0, all_69_1) = all_17_0 & union(all_31_1, % 134.70/28.27 | all_69_0) = v0 & $i(v0) & $i(all_17_0)) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (5) with all_69_0, all_339_0, all_61_1, all_29_0, % 134.70/28.27 | all_151_0, simplifying with (144), (160), (470), (577), (579) % 134.70/28.27 | gives: % 134.70/28.27 | (590) ? [v0: $i] : (union(all_339_0, all_61_1) = v0 & union(all_69_0, v0) % 134.70/28.27 | = all_151_0 & $i(v0) & $i(all_151_0)) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (14) with all_391_0, all_391_1, all_31_1, % 134.70/28.27 | simplifying with (514), (515), (516) gives: % 134.70/28.27 | (591) union(all_391_0, all_391_1) = all_31_1 & $i(all_31_1) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (10) with all_17_6, all_17_4, all_321_1, % 134.70/28.27 | simplifying with (23), (25), (485) gives: % 134.70/28.27 | (592) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.27 | (intersection(all_17_6, all_17_4) = v1 & difference(v0, v1) = v2 & % 134.70/28.27 | difference(all_17_6, all_17_4) = v3 & union(v3, all_321_1) = v2 & % 134.70/28.27 | union(all_17_6, all_17_4) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (9) with all_17_4, all_17_6, all_321_1, simplifying % 134.70/28.27 | with (23), (25), (485) gives: % 134.70/28.27 | (593) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.27 | (intersection(all_17_4, all_17_6) = v1 & difference(v0, v1) = v2 & % 134.70/28.27 | difference(all_17_6, all_17_4) = v3 & union(all_321_1, v3) = v2 & % 134.70/28.27 | union(all_17_4, all_17_6) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (7) with all_17_4, all_17_5, all_17_6, all_27_0, % 134.70/28.27 | all_143_0, simplifying with (23), (24), (25), (55), (462) gives: % 134.70/28.27 | (594) ? [v0: $i] : ? [v1: $i] : (intersection(all_17_4, all_17_6) = v1 & % 134.70/28.27 | difference(all_17_4, all_17_5) = v0 & union(v0, v1) = all_143_0 & % 134.70/28.27 | $i(v1) & $i(v0) & $i(all_143_0)) % 134.70/28.27 | % 134.70/28.27 | GROUND_INST: instantiating (10) with all_31_1, all_69_0, all_323_0, % 134.70/28.27 | simplifying with (60), (160), (488) gives: % 134.70/28.28 | (595) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.28 | (intersection(all_31_1, all_69_0) = v1 & difference(v0, v1) = v2 & % 134.70/28.28 | difference(all_31_1, all_69_0) = v3 & union(v3, all_323_0) = v2 & % 134.70/28.28 | union(all_31_1, all_69_0) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 134.70/28.28 | % 134.70/28.28 | GROUND_INST: instantiating (9) with all_69_0, all_31_1, all_323_0, simplifying % 134.70/28.28 | with (60), (160), (488) gives: % 134.70/28.28 | (596) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 134.70/28.28 | (intersection(all_69_0, all_31_1) = v1 & difference(v0, v1) = v2 & % 134.70/28.28 | difference(all_31_1, all_69_0) = v3 & union(all_323_0, v3) = v2 & % 134.70/28.28 | union(all_69_0, all_31_1) = v0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 134.70/28.28 | % 134.70/28.28 | GROUND_INST: instantiating (15) with all_17_4, all_17_6, all_329_0, % 134.70/28.28 | simplifying with (23), (25), (495) gives: % 134.70/28.28 | (597) intersection(all_17_4, all_17_6) = all_329_0 & $i(all_329_0) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (597) implies: % 134.70/28.28 | (598) intersection(all_17_4, all_17_6) = all_329_0 % 134.70/28.28 | % 134.70/28.28 | GROUND_INST: instantiating (6) with all_17_6, all_17_4, all_17_5, all_83_2, % 134.70/28.28 | all_327_0, simplifying with (23), (24), (25), (455), (493) gives: % 134.70/28.28 | (599) ? [v0: $i] : (intersection(v0, all_17_5) = all_327_0 & % 134.70/28.28 | intersection(all_17_6, all_17_4) = v0 & $i(v0) & $i(all_327_0)) % 134.70/28.28 | % 134.70/28.28 | GROUND_INST: instantiating (6) with all_17_4, all_17_6, all_17_5, all_73_2, % 134.70/28.28 | all_339_0, simplifying with (23), (24), (25), (561), (563) gives: % 134.70/28.28 | (600) ? [v0: $i] : (intersection(v0, all_17_5) = all_339_0 & % 134.70/28.28 | intersection(all_17_4, all_17_6) = v0 & $i(v0) & $i(all_339_0)) % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (600) with fresh symbol all_1051_0 gives: % 134.70/28.28 | (601) intersection(all_1051_0, all_17_5) = all_339_0 & % 134.70/28.28 | intersection(all_17_4, all_17_6) = all_1051_0 & $i(all_1051_0) & % 134.70/28.28 | $i(all_339_0) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (601) implies: % 134.70/28.28 | (602) intersection(all_17_4, all_17_6) = all_1051_0 % 134.70/28.28 | (603) intersection(all_1051_0, all_17_5) = all_339_0 % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (599) with fresh symbol all_1055_0 gives: % 134.70/28.28 | (604) intersection(all_1055_0, all_17_5) = all_327_0 & % 134.70/28.28 | intersection(all_17_6, all_17_4) = all_1055_0 & $i(all_1055_0) & % 134.70/28.28 | $i(all_327_0) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (604) implies: % 134.70/28.28 | (605) intersection(all_17_6, all_17_4) = all_1055_0 % 134.70/28.28 | (606) intersection(all_1055_0, all_17_5) = all_327_0 % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (589) with fresh symbol all_1113_0 gives: % 134.70/28.28 | (607) union(all_1113_0, all_69_1) = all_17_0 & union(all_31_1, all_69_0) = % 134.70/28.28 | all_1113_0 & $i(all_1113_0) & $i(all_17_0) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (607) implies: % 134.70/28.28 | (608) union(all_31_1, all_69_0) = all_1113_0 % 134.70/28.28 | (609) union(all_1113_0, all_69_1) = all_17_0 % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (590) with fresh symbol all_1299_0 gives: % 134.70/28.28 | (610) union(all_339_0, all_61_1) = all_1299_0 & union(all_69_0, all_1299_0) % 134.70/28.28 | = all_151_0 & $i(all_1299_0) & $i(all_151_0) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (610) implies: % 134.70/28.28 | (611) union(all_69_0, all_1299_0) = all_151_0 % 134.70/28.28 | (612) union(all_339_0, all_61_1) = all_1299_0 % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (594) with fresh symbols all_1855_0, all_1855_1 gives: % 134.70/28.28 | (613) intersection(all_17_4, all_17_6) = all_1855_0 & difference(all_17_4, % 134.70/28.28 | all_17_5) = all_1855_1 & union(all_1855_1, all_1855_0) = all_143_0 % 134.70/28.28 | & $i(all_1855_0) & $i(all_1855_1) & $i(all_143_0) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (613) implies: % 134.70/28.28 | (614) intersection(all_17_4, all_17_6) = all_1855_0 % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (583) with fresh symbols all_2341_0, all_2341_1, % 134.70/28.28 | all_2341_2, all_2341_3 gives: % 134.70/28.28 | (615) intersection(all_17_6, all_17_4) = all_2341_3 & difference(all_157_0, % 134.70/28.28 | all_2341_3) = all_2341_2 & difference(all_17_4, all_17_6) = % 134.70/28.28 | all_2341_0 & difference(all_17_6, all_17_4) = all_2341_1 & % 134.70/28.28 | union(all_2341_1, all_2341_0) = all_2341_2 & $i(all_2341_0) & % 134.70/28.28 | $i(all_2341_1) & $i(all_2341_2) & $i(all_2341_3) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (615) implies: % 134.70/28.28 | (616) intersection(all_17_6, all_17_4) = all_2341_3 % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (584) with fresh symbols all_2405_0, all_2405_1, % 134.70/28.28 | all_2405_2, all_2405_3 gives: % 134.70/28.28 | (617) intersection(all_17_4, all_17_6) = all_2405_3 & difference(all_145_0, % 134.70/28.28 | all_2405_3) = all_2405_2 & difference(all_17_4, all_17_6) = % 134.70/28.28 | all_2405_1 & difference(all_17_6, all_17_4) = all_2405_0 & % 134.70/28.28 | union(all_2405_1, all_2405_0) = all_2405_2 & $i(all_2405_0) & % 134.70/28.28 | $i(all_2405_1) & $i(all_2405_2) & $i(all_2405_3) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (617) implies: % 134.70/28.28 | (618) intersection(all_17_4, all_17_6) = all_2405_3 % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (595) with fresh symbols all_2455_0, all_2455_1, % 134.70/28.28 | all_2455_2, all_2455_3 gives: % 134.70/28.28 | (619) intersection(all_31_1, all_69_0) = all_2455_2 & % 134.70/28.28 | difference(all_2455_3, all_2455_2) = all_2455_1 & % 134.70/28.28 | difference(all_31_1, all_69_0) = all_2455_0 & union(all_2455_0, % 134.70/28.28 | all_323_0) = all_2455_1 & union(all_31_1, all_69_0) = all_2455_3 & % 134.70/28.28 | $i(all_2455_0) & $i(all_2455_1) & $i(all_2455_2) & $i(all_2455_3) % 134.70/28.28 | % 134.70/28.28 | ALPHA: (619) implies: % 134.70/28.28 | (620) union(all_31_1, all_69_0) = all_2455_3 % 134.70/28.28 | % 134.70/28.28 | DELTA: instantiating (593) with fresh symbols all_2507_0, all_2507_1, % 134.70/28.28 | all_2507_2, all_2507_3 gives: % 134.70/28.29 | (621) intersection(all_17_4, all_17_6) = all_2507_2 & % 134.70/28.29 | difference(all_2507_3, all_2507_2) = all_2507_1 & % 134.70/28.29 | difference(all_17_6, all_17_4) = all_2507_0 & union(all_321_1, % 134.70/28.29 | all_2507_0) = all_2507_1 & union(all_17_4, all_17_6) = all_2507_3 & % 134.70/28.29 | $i(all_2507_0) & $i(all_2507_1) & $i(all_2507_2) & $i(all_2507_3) % 134.70/28.29 | % 134.70/28.29 | ALPHA: (621) implies: % 134.70/28.29 | (622) union(all_17_4, all_17_6) = all_2507_3 % 134.70/28.29 | (623) intersection(all_17_4, all_17_6) = all_2507_2 % 134.70/28.29 | % 134.70/28.29 | DELTA: instantiating (596) with fresh symbols all_2705_0, all_2705_1, % 134.70/28.29 | all_2705_2, all_2705_3 gives: % 134.70/28.29 | (624) intersection(all_69_0, all_31_1) = all_2705_2 & % 134.70/28.29 | difference(all_2705_3, all_2705_2) = all_2705_1 & % 134.70/28.29 | difference(all_31_1, all_69_0) = all_2705_0 & union(all_323_0, % 134.70/28.29 | all_2705_0) = all_2705_1 & union(all_69_0, all_31_1) = all_2705_3 & % 134.70/28.29 | $i(all_2705_0) & $i(all_2705_1) & $i(all_2705_2) & $i(all_2705_3) % 134.70/28.29 | % 134.70/28.29 | ALPHA: (624) implies: % 134.70/28.29 | (625) union(all_69_0, all_31_1) = all_2705_3 % 134.70/28.29 | % 134.70/28.29 | DELTA: instantiating (592) with fresh symbols all_2865_0, all_2865_1, % 134.70/28.29 | all_2865_2, all_2865_3 gives: % 134.70/28.29 | (626) intersection(all_17_6, all_17_4) = all_2865_2 & % 134.70/28.29 | difference(all_2865_3, all_2865_2) = all_2865_1 & % 134.70/28.29 | difference(all_17_6, all_17_4) = all_2865_0 & union(all_2865_0, % 134.70/28.29 | all_321_1) = all_2865_1 & union(all_17_6, all_17_4) = all_2865_3 & % 134.70/28.29 | $i(all_2865_0) & $i(all_2865_1) & $i(all_2865_2) & $i(all_2865_3) % 134.70/28.29 | % 134.70/28.29 | ALPHA: (626) implies: % 134.70/28.29 | (627) intersection(all_17_6, all_17_4) = all_2865_2 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (17) with all_145_0, all_2507_3, all_17_6, % 134.70/28.29 | all_17_4, simplifying with (464), (622) gives: % 134.70/28.29 | (628) all_2507_3 = all_145_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (17) with all_157_0, all_2507_3, all_17_6, % 134.70/28.29 | all_17_4, simplifying with (582), (622) gives: % 134.70/28.29 | (629) all_2507_3 = all_157_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (17) with all_1113_0, all_2455_3, all_69_0, % 134.70/28.29 | all_31_1, simplifying with (608), (620) gives: % 134.70/28.29 | (630) all_2455_3 = all_1113_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (17) with all_141_0, all_2455_3, all_69_0, % 134.70/28.29 | all_31_1, simplifying with (588), (620) gives: % 134.70/28.29 | (631) all_2455_3 = all_141_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (17) with all_141_0, all_2705_3, all_31_1, % 134.70/28.29 | all_69_0, simplifying with (460), (625) gives: % 134.70/28.29 | (632) all_2705_3 = all_141_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (20) with all_329_0, all_2341_3, all_17_4, % 134.70/28.29 | all_17_6, simplifying with (495), (616) gives: % 134.70/28.29 | (633) all_2341_3 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (20) with all_2341_3, all_2865_2, all_17_4, % 134.70/28.29 | all_17_6, simplifying with (616), (627) gives: % 134.70/28.29 | (634) all_2865_2 = all_2341_3 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (20) with all_1055_0, all_2865_2, all_17_4, % 134.70/28.29 | all_17_6, simplifying with (605), (627) gives: % 134.70/28.29 | (635) all_2865_2 = all_1055_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (20) with all_1051_0, all_1855_0, all_17_6, % 134.70/28.29 | all_17_4, simplifying with (602), (614) gives: % 134.70/28.29 | (636) all_1855_0 = all_1051_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (20) with all_1855_0, all_2405_3, all_17_6, % 134.70/28.29 | all_17_4, simplifying with (614), (618) gives: % 134.70/28.29 | (637) all_2405_3 = all_1855_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (20) with all_2405_3, all_2507_2, all_17_6, % 134.70/28.29 | all_17_4, simplifying with (618), (623) gives: % 134.70/28.29 | (638) all_2507_2 = all_2405_3 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (20) with all_329_0, all_2507_2, all_17_6, % 134.70/28.29 | all_17_4, simplifying with (598), (623) gives: % 134.70/28.29 | (639) all_2507_2 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | COMBINE_EQS: (634), (635) imply: % 134.70/28.29 | (640) all_2341_3 = all_1055_0 % 134.70/28.29 | % 134.70/28.29 | SIMP: (640) implies: % 134.70/28.29 | (641) all_2341_3 = all_1055_0 % 134.70/28.29 | % 134.70/28.29 | COMBINE_EQS: (638), (639) imply: % 134.70/28.29 | (642) all_2405_3 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | SIMP: (642) implies: % 134.70/28.29 | (643) all_2405_3 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | COMBINE_EQS: (628), (629) imply: % 134.70/28.29 | (644) all_157_0 = all_145_0 % 134.70/28.29 | % 134.70/28.29 | COMBINE_EQS: (630), (631) imply: % 134.70/28.29 | (645) all_1113_0 = all_141_0 % 134.70/28.29 | % 134.70/28.29 | COMBINE_EQS: (637), (643) imply: % 134.70/28.29 | (646) all_1855_0 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | SIMP: (646) implies: % 134.70/28.29 | (647) all_1855_0 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | COMBINE_EQS: (633), (641) imply: % 134.70/28.29 | (648) all_1055_0 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | COMBINE_EQS: (636), (647) imply: % 134.70/28.29 | (649) all_1051_0 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | SIMP: (649) implies: % 134.70/28.29 | (650) all_1051_0 = all_329_0 % 134.70/28.29 | % 134.70/28.29 | REDUCE: (606), (648) imply: % 134.70/28.29 | (651) intersection(all_329_0, all_17_5) = all_327_0 % 134.70/28.29 | % 134.70/28.29 | REDUCE: (603), (650) imply: % 134.70/28.29 | (652) intersection(all_329_0, all_17_5) = all_339_0 % 134.70/28.29 | % 134.70/28.29 | REDUCE: (474), (644) imply: % 134.70/28.29 | (653) difference(all_17_5, all_145_0) = all_61_0 % 134.70/28.29 | % 134.70/28.29 | REDUCE: (609), (645) imply: % 134.70/28.29 | (654) union(all_141_0, all_69_1) = all_17_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (18) with all_69_1, all_61_0, all_145_0, all_17_5, % 134.70/28.29 | simplifying with (465), (653) gives: % 134.70/28.29 | (655) all_69_1 = all_61_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (20) with all_327_0, all_339_0, all_17_5, % 134.70/28.29 | all_329_0, simplifying with (651), (652) gives: % 134.70/28.29 | (656) all_339_0 = all_327_0 % 134.70/28.29 | % 134.70/28.29 | REDUCE: (612), (656) imply: % 134.70/28.29 | (657) union(all_327_0, all_61_1) = all_1299_0 % 134.70/28.29 | % 134.70/28.29 | REDUCE: (654), (655) imply: % 134.70/28.29 | (658) union(all_141_0, all_61_0) = all_17_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (17) with all_31_1, all_1299_0, all_61_1, % 134.70/28.29 | all_327_0, simplifying with (586), (657) gives: % 134.70/28.29 | (659) all_1299_0 = all_31_1 % 134.70/28.29 | % 134.70/28.29 | REDUCE: (611), (659) imply: % 134.70/28.29 | (660) union(all_69_0, all_31_1) = all_151_0 % 134.70/28.29 | % 134.70/28.29 | GROUND_INST: instantiating (17) with all_141_0, all_151_0, all_31_1, all_69_0, % 134.70/28.29 | simplifying with (460), (660) gives: % 134.70/28.29 | (661) all_151_0 = all_141_0 % 134.70/28.29 | % 134.70/28.29 | REDUCE: (471), (661) imply: % 134.70/28.30 | (662) union(all_141_0, all_61_0) = all_17_2 % 134.70/28.30 | % 134.70/28.30 | GROUND_INST: instantiating (17) with all_17_0, all_17_2, all_61_0, all_141_0, % 134.70/28.30 | simplifying with (658), (662) gives: % 134.70/28.30 | (663) all_17_0 = all_17_2 % 134.70/28.30 | % 134.70/28.30 | REDUCE: (22), (663) imply: % 134.70/28.30 | (664) $false % 134.70/28.30 | % 134.70/28.30 | CLOSE: (664) is inconsistent. % 134.70/28.30 | % 134.70/28.30 End of proof % 134.70/28.30 % SZS output end Proof for theBenchmark % 134.70/28.30 % 134.70/28.30 27700ms %------------------------------------------------------------------------------