%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEU174+1 : TPTP v8.1.2. Released v3.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 17:43:03 EDT 2023 % Result : Theorem 19.64s 3.39s % Output : Proof 29.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU174+1 : TPTP v8.1.2. Released v3.3.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.34 % Computer : n023.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Aug 23 14:36:13 EDT 2023 % 0.14/0.34 % CPUTime : % 0.65/0.63 ________ _____ % 0.65/0.63 ___ __ \_________(_)________________________________ % 0.65/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.65/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.65/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.65/0.63 % 0.65/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.65/0.63 (2023-06-19) % 0.65/0.63 % 0.65/0.63 (c) Philipp Rümmer, 2009-2023 % 0.65/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.65/0.63 Amanda Stjerna. % 0.65/0.63 Free software under BSD-3-Clause. % 0.65/0.63 % 0.65/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.65/0.63 % 0.65/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.65/0.65 Running up to 7 provers in parallel. % 0.65/0.67 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.65/0.67 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.65/0.67 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.65/0.67 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.65/0.67 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.65/0.67 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.65/0.67 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.48/1.09 Prover 4: Preprocessing ... % 2.48/1.09 Prover 1: Preprocessing ... % 2.48/1.13 Prover 3: Preprocessing ... % 2.48/1.13 Prover 6: Preprocessing ... % 2.48/1.13 Prover 0: Preprocessing ... % 2.48/1.13 Prover 2: Preprocessing ... % 2.48/1.13 Prover 5: Preprocessing ... % 5.86/1.55 Prover 1: Warning: ignoring some quantifiers % 5.86/1.56 Prover 3: Warning: ignoring some quantifiers % 5.86/1.57 Prover 5: Proving ... % 5.86/1.57 Prover 6: Proving ... % 5.86/1.57 Prover 2: Proving ... % 5.86/1.58 Prover 3: Constructing countermodel ... % 5.86/1.59 Prover 1: Constructing countermodel ... % 6.50/1.62 Prover 4: Warning: ignoring some quantifiers % 6.50/1.66 Prover 4: Constructing countermodel ... % 6.87/1.72 Prover 0: Proving ... % 19.64/3.39 Prover 2: proved (2726ms) % 19.64/3.39 % 19.64/3.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 19.64/3.39 % 19.64/3.39 Prover 0: stopped % 19.64/3.40 Prover 5: stopped % 19.64/3.42 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 19.64/3.42 Prover 3: stopped % 19.64/3.43 Prover 6: stopped % 19.64/3.43 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 19.64/3.43 Prover 7: Preprocessing ... % 19.64/3.43 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 19.64/3.43 Prover 8: Preprocessing ... % 19.64/3.43 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 19.64/3.43 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 20.15/3.46 Prover 10: Preprocessing ... % 20.28/3.47 Prover 13: Preprocessing ... % 20.28/3.47 Prover 11: Preprocessing ... % 20.28/3.50 Prover 7: Warning: ignoring some quantifiers % 20.28/3.50 Prover 8: Warning: ignoring some quantifiers % 20.28/3.50 Prover 10: Warning: ignoring some quantifiers % 20.28/3.50 Prover 7: Constructing countermodel ... % 20.28/3.50 Prover 10: Constructing countermodel ... % 20.28/3.50 Prover 8: Constructing countermodel ... % 20.66/3.57 Prover 13: Warning: ignoring some quantifiers % 20.66/3.58 Prover 13: Constructing countermodel ... % 20.66/3.62 Prover 11: Warning: ignoring some quantifiers % 20.66/3.62 Prover 11: Constructing countermodel ... % 28.14/4.50 Prover 10: gave up % 28.14/4.50 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 28.33/4.56 Prover 16: Preprocessing ... % 29.03/4.62 Prover 7: Found proof (size 110) % 29.03/4.63 Prover 7: proved (1232ms) % 29.03/4.63 Prover 16: Warning: ignoring some quantifiers % 29.03/4.63 Prover 8: stopped % 29.03/4.63 Prover 13: stopped % 29.03/4.63 Prover 1: stopped % 29.03/4.63 Prover 4: stopped % 29.03/4.63 Prover 11: stopped % 29.03/4.63 Prover 16: Constructing countermodel ... % 29.03/4.63 Prover 16: stopped % 29.03/4.63 % 29.03/4.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 29.03/4.63 % 29.03/4.64 % SZS output start Proof for theBenchmark % 29.03/4.65 Assumptions after simplification: % 29.03/4.65 --------------------------------- % 29.03/4.65 % 29.03/4.65 (d8_setfam_1) % 29.03/4.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (complements_of_subsets(v0, v1) % 29.03/4.68 = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : (powerset(v3) % 29.03/4.68 = v4 & powerset(v0) = v3 & $i(v4) & $i(v3) & ( ~ element(v1, v4) | ( ! % 29.03/4.68 [v5: $i] : ! [v6: $i] : ( ~ (subset_complement(v0, v5) = v6) | ~ % 29.03/4.68 $i(v5) | ~ $i(v2) | ~ element(v5, v3) | ~ element(v2, v4) | ~ % 29.03/4.68 in(v6, v1) | in(v5, v2)) & ! [v5: $i] : ! [v6: $i] : ( ~ % 29.03/4.68 (subset_complement(v0, v5) = v6) | ~ $i(v5) | ~ $i(v2) | ~ % 29.03/4.68 element(v5, v3) | ~ element(v2, v4) | ~ in(v5, v2) | in(v6, v1)) & % 29.03/4.68 ! [v5: $i] : (v5 = v2 | ~ $i(v5) | ~ element(v5, v4) | ? [v6: $i] % 29.03/4.68 : ? [v7: $i] : ($i(v6) & element(v6, v3) & ( ~ in(v6, v5) | % 29.03/4.68 (subset_complement(v0, v6) = v7 & $i(v7) & ~ in(v7, v1))) & % 29.03/4.68 (in(v6, v5) | (subset_complement(v0, v6) = v7 & $i(v7) & in(v7, % 29.03/4.68 v1))))))))) % 29.03/4.68 % 29.03/4.68 (dt_k7_setfam_1) % 29.03/4.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (complements_of_subsets(v0, v1) % 29.03/4.68 = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : (powerset(v3) % 29.03/4.68 = v4 & powerset(v0) = v3 & $i(v4) & $i(v3) & ( ~ element(v1, v4) | % 29.03/4.68 element(v2, v4)))) % 29.03/4.68 % 29.03/4.68 (involutiveness_k7_setfam_1) % 29.03/4.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (complements_of_subsets(v0, v1) % 29.03/4.68 = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 29.03/4.68 ((v5 = v1 & complements_of_subsets(v0, v2) = v1) | (powerset(v3) = v4 & % 29.03/4.68 powerset(v0) = v3 & $i(v4) & $i(v3) & ~ element(v1, v4)))) % 29.03/4.68 % 29.03/4.68 (rc1_xboole_0) % 29.03/4.68 ? [v0: $i] : ($i(v0) & empty(v0)) % 29.03/4.68 % 29.03/4.68 (rc2_subset_1) % 29.03/4.68 ! [v0: $i] : ! [v1: $i] : ( ~ (powerset(v0) = v1) | ~ $i(v0) | ? [v2: $i] % 29.03/4.68 : ($i(v2) & empty(v2) & element(v2, v1))) % 29.03/4.68 % 29.03/4.68 (t46_setfam_1) % 29.03/4.68 $i(empty_set) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ % 29.03/4.68 (v1 = empty_set) & complements_of_subsets(v0, v1) = empty_set & powerset(v2) % 29.03/4.68 = v3 & powerset(v0) = v2 & $i(v3) & $i(v2) & $i(v1) & $i(v0) & element(v1, % 29.03/4.68 v3)) % 29.03/4.68 % 29.03/4.68 (t6_boole) % 29.03/4.69 $i(empty_set) & ! [v0: $i] : (v0 = empty_set | ~ $i(v0) | ~ empty(v0)) % 29.03/4.69 % 29.03/4.69 (t7_boole) % 29.03/4.69 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ empty(v1) | ~ in(v0, % 29.03/4.69 v1)) % 29.03/4.69 % 29.03/4.69 (t8_boole) % 29.03/4.69 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ empty(v1) | % 29.03/4.69 ~ empty(v0)) % 29.03/4.69 % 29.03/4.69 (function-axioms) % 29.03/4.69 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 29.03/4.69 (complements_of_subsets(v3, v2) = v1) | ~ (complements_of_subsets(v3, v2) = % 29.03/4.69 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 29.03/4.69 ~ (subset_complement(v3, v2) = v1) | ~ (subset_complement(v3, v2) = v0)) & % 29.03/4.69 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (powerset(v2) = v1) | % 29.03/4.69 ~ (powerset(v2) = v0)) % 29.03/4.69 % 29.03/4.69 Further assumptions not needed in the proof: % 29.03/4.69 -------------------------------------------- % 29.03/4.69 antisymmetry_r2_hidden, d3_tarski, dt_k1_xboole_0, dt_k1_zfmisc_1, % 29.03/4.69 dt_k3_subset_1, dt_m1_subset_1, existence_m1_subset_1, fc1_subset_1, % 29.03/4.69 fc1_xboole_0, involutiveness_k3_subset_1, rc1_subset_1, rc2_xboole_0, % 29.03/4.69 reflexivity_r1_tarski, t1_subset, t2_subset, t3_subset, t4_subset, t5_subset % 29.03/4.69 % 29.03/4.69 Those formulas are unsatisfiable: % 29.03/4.69 --------------------------------- % 29.03/4.69 % 29.03/4.69 Begin of proof % 29.03/4.69 | % 29.03/4.69 | ALPHA: (t6_boole) implies: % 29.03/4.69 | (1) ! [v0: $i] : (v0 = empty_set | ~ $i(v0) | ~ empty(v0)) % 29.03/4.69 | % 29.03/4.69 | ALPHA: (t46_setfam_1) implies: % 29.03/4.69 | (2) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ( ~ (v1 = % 29.03/4.69 | empty_set) & complements_of_subsets(v0, v1) = empty_set & % 29.03/4.69 | powerset(v2) = v3 & powerset(v0) = v2 & $i(v3) & $i(v2) & $i(v1) & % 29.03/4.69 | $i(v0) & element(v1, v3)) % 29.03/4.69 | % 29.03/4.69 | ALPHA: (function-axioms) implies: % 29.03/4.69 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (powerset(v2) = % 29.03/4.69 | v1) | ~ (powerset(v2) = v0)) % 29.03/4.69 | % 29.39/4.69 | DELTA: instantiating (rc1_xboole_0) with fresh symbol all_24_0 gives: % 29.39/4.69 | (4) $i(all_24_0) & empty(all_24_0) % 29.39/4.69 | % 29.39/4.69 | ALPHA: (4) implies: % 29.39/4.70 | (5) empty(all_24_0) % 29.39/4.70 | (6) $i(all_24_0) % 29.39/4.70 | % 29.39/4.70 | DELTA: instantiating (2) with fresh symbols all_29_0, all_29_1, all_29_2, % 29.39/4.70 | all_29_3 gives: % 29.39/4.70 | (7) ~ (all_29_2 = empty_set) & complements_of_subsets(all_29_3, all_29_2) % 29.39/4.70 | = empty_set & powerset(all_29_1) = all_29_0 & powerset(all_29_3) = % 29.39/4.70 | all_29_1 & $i(all_29_0) & $i(all_29_1) & $i(all_29_2) & $i(all_29_3) & % 29.39/4.70 | element(all_29_2, all_29_0) % 29.39/4.70 | % 29.39/4.70 | ALPHA: (7) implies: % 29.39/4.70 | (8) ~ (all_29_2 = empty_set) % 29.39/4.70 | (9) element(all_29_2, all_29_0) % 29.39/4.70 | (10) $i(all_29_3) % 29.39/4.70 | (11) $i(all_29_2) % 29.39/4.70 | (12) $i(all_29_1) % 29.39/4.70 | (13) powerset(all_29_3) = all_29_1 % 29.39/4.70 | (14) powerset(all_29_1) = all_29_0 % 29.39/4.70 | (15) complements_of_subsets(all_29_3, all_29_2) = empty_set % 29.39/4.70 | % 29.39/4.70 | GROUND_INST: instantiating (1) with all_24_0, simplifying with (5), (6) gives: % 29.39/4.70 | (16) all_24_0 = empty_set % 29.39/4.70 | % 29.39/4.70 | GROUND_INST: instantiating (rc2_subset_1) with all_29_3, all_29_1, simplifying % 29.39/4.70 | with (10), (13) gives: % 29.39/4.70 | (17) ? [v0: $i] : ($i(v0) & empty(v0) & element(v0, all_29_1)) % 29.39/4.70 | % 29.39/4.70 | GROUND_INST: instantiating (rc2_subset_1) with all_29_1, all_29_0, simplifying % 29.39/4.70 | with (12), (14) gives: % 29.39/4.70 | (18) ? [v0: $i] : ($i(v0) & empty(v0) & element(v0, all_29_0)) % 29.39/4.70 | % 29.39/4.70 | GROUND_INST: instantiating (involutiveness_k7_setfam_1) with all_29_3, % 29.39/4.70 | all_29_2, empty_set, simplifying with (10), (11), (15) gives: % 29.39/4.70 | (19) ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ((v2 = all_29_2 & % 29.39/4.70 | complements_of_subsets(all_29_3, empty_set) = all_29_2) | % 29.39/4.70 | (powerset(v0) = v1 & powerset(all_29_3) = v0 & $i(v1) & $i(v0) & ~ % 29.39/4.70 | element(all_29_2, v1))) % 29.39/4.70 | % 29.39/4.70 | GROUND_INST: instantiating (dt_k7_setfam_1) with all_29_3, all_29_2, % 29.39/4.70 | empty_set, simplifying with (10), (11), (15) gives: % 29.39/4.70 | (20) ? [v0: $i] : ? [v1: $i] : (powerset(v0) = v1 & powerset(all_29_3) = % 29.39/4.70 | v0 & $i(v1) & $i(v0) & ( ~ element(all_29_2, v1) | % 29.39/4.70 | element(empty_set, v1))) % 29.39/4.70 | % 29.39/4.70 | GROUND_INST: instantiating (d8_setfam_1) with all_29_3, all_29_2, empty_set, % 29.39/4.70 | simplifying with (10), (11), (15) gives: % 29.39/4.71 | (21) ? [v0: $i] : ? [v1: $i] : (powerset(v0) = v1 & powerset(all_29_3) = % 29.39/4.71 | v0 & $i(v1) & $i(v0) & ( ~ element(all_29_2, v1) | ( ! [v2: $i] : ! % 29.39/4.71 | [v3: $i] : ( ~ (subset_complement(all_29_3, v2) = v3) | ~ % 29.39/4.71 | $i(v2) | ~ $i(empty_set) | ~ element(v2, v0) | ~ % 29.39/4.71 | element(empty_set, v1) | ~ in(v3, all_29_2) | in(v2, % 29.39/4.71 | empty_set)) & ! [v2: $i] : ! [v3: $i] : ( ~ % 29.39/4.71 | (subset_complement(all_29_3, v2) = v3) | ~ $i(v2) | ~ % 29.39/4.71 | $i(empty_set) | ~ element(v2, v0) | ~ element(empty_set, v1) % 29.39/4.71 | | ~ in(v2, empty_set) | in(v3, all_29_2)) & ! [v2: $i] : (v2 % 29.39/4.71 | = empty_set | ~ $i(v2) | ~ element(v2, v1) | ? [v3: $i] : % 29.39/4.71 | ? [v4: $i] : ($i(v3) & element(v3, v0) & ( ~ in(v3, v2) | % 29.39/4.71 | (subset_complement(all_29_3, v3) = v4 & $i(v4) & ~ in(v4, % 29.39/4.71 | all_29_2))) & (in(v3, v2) | % 29.39/4.71 | (subset_complement(all_29_3, v3) = v4 & $i(v4) & in(v4, % 29.39/4.71 | all_29_2)))))))) % 29.39/4.71 | % 29.39/4.71 | DELTA: instantiating (18) with fresh symbol all_41_0 gives: % 29.39/4.71 | (22) $i(all_41_0) & empty(all_41_0) & element(all_41_0, all_29_0) % 29.39/4.71 | % 29.39/4.71 | ALPHA: (22) implies: % 29.39/4.71 | (23) element(all_41_0, all_29_0) % 29.39/4.71 | (24) empty(all_41_0) % 29.39/4.71 | (25) $i(all_41_0) % 29.39/4.71 | % 29.39/4.71 | DELTA: instantiating (17) with fresh symbol all_43_0 gives: % 29.39/4.71 | (26) $i(all_43_0) & empty(all_43_0) & element(all_43_0, all_29_1) % 29.39/4.71 | % 29.39/4.71 | ALPHA: (26) implies: % 29.39/4.71 | (27) empty(all_43_0) % 29.39/4.71 | (28) $i(all_43_0) % 29.39/4.71 | % 29.39/4.71 | DELTA: instantiating (20) with fresh symbols all_45_0, all_45_1 gives: % 29.39/4.71 | (29) powerset(all_45_1) = all_45_0 & powerset(all_29_3) = all_45_1 & % 29.39/4.71 | $i(all_45_0) & $i(all_45_1) & ( ~ element(all_29_2, all_45_0) | % 29.39/4.71 | element(empty_set, all_45_0)) % 29.39/4.71 | % 29.39/4.71 | ALPHA: (29) implies: % 29.39/4.71 | (30) powerset(all_29_3) = all_45_1 % 29.39/4.71 | (31) powerset(all_45_1) = all_45_0 % 29.39/4.71 | % 29.39/4.71 | DELTA: instantiating (19) with fresh symbols all_47_0, all_47_1, all_47_2 % 29.39/4.71 | gives: % 29.39/4.71 | (32) (all_47_0 = all_29_2 & complements_of_subsets(all_29_3, empty_set) = % 29.39/4.71 | all_29_2) | (powerset(all_47_2) = all_47_1 & powerset(all_29_3) = % 29.39/4.71 | all_47_2 & $i(all_47_1) & $i(all_47_2) & ~ element(all_29_2, % 29.39/4.71 | all_47_1)) % 29.39/4.71 | % 29.39/4.71 | DELTA: instantiating (21) with fresh symbols all_48_0, all_48_1 gives: % 29.39/4.71 | (33) powerset(all_48_1) = all_48_0 & powerset(all_29_3) = all_48_1 & % 29.39/4.71 | $i(all_48_0) & $i(all_48_1) & ( ~ element(all_29_2, all_48_0) | ( ! % 29.39/4.71 | [v0: $i] : ! [v1: $i] : ( ~ (subset_complement(all_29_3, v0) = % 29.39/4.71 | v1) | ~ $i(v0) | ~ $i(empty_set) | ~ element(v0, all_48_1) % 29.39/4.71 | | ~ element(empty_set, all_48_0) | ~ in(v1, all_29_2) | in(v0, % 29.39/4.71 | empty_set)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 29.39/4.71 | (subset_complement(all_29_3, v0) = v1) | ~ $i(v0) | ~ % 29.39/4.71 | $i(empty_set) | ~ element(v0, all_48_1) | ~ element(empty_set, % 29.39/4.71 | all_48_0) | ~ in(v0, empty_set) | in(v1, all_29_2)) & ! [v0: % 29.39/4.71 | $i] : (v0 = empty_set | ~ $i(v0) | ~ element(v0, all_48_0) | % 29.39/4.71 | ? [v1: $i] : ? [v2: $i] : ($i(v1) & element(v1, all_48_1) & ( ~ % 29.39/4.71 | in(v1, v0) | (subset_complement(all_29_3, v1) = v2 & $i(v2) % 29.39/4.71 | & ~ in(v2, all_29_2))) & (in(v1, v0) | % 29.39/4.71 | (subset_complement(all_29_3, v1) = v2 & $i(v2) & in(v2, % 29.39/4.71 | all_29_2))))))) % 29.39/4.71 | % 29.39/4.71 | ALPHA: (33) implies: % 29.39/4.71 | (34) powerset(all_29_3) = all_48_1 % 29.39/4.71 | (35) powerset(all_48_1) = all_48_0 % 29.39/4.71 | (36) ~ element(all_29_2, all_48_0) | ( ! [v0: $i] : ! [v1: $i] : ( ~ % 29.39/4.71 | (subset_complement(all_29_3, v0) = v1) | ~ $i(v0) | ~ % 29.39/4.71 | $i(empty_set) | ~ element(v0, all_48_1) | ~ element(empty_set, % 29.39/4.71 | all_48_0) | ~ in(v1, all_29_2) | in(v0, empty_set)) & ! [v0: % 29.39/4.71 | $i] : ! [v1: $i] : ( ~ (subset_complement(all_29_3, v0) = v1) | % 29.39/4.71 | ~ $i(v0) | ~ $i(empty_set) | ~ element(v0, all_48_1) | ~ % 29.39/4.71 | element(empty_set, all_48_0) | ~ in(v0, empty_set) | in(v1, % 29.39/4.71 | all_29_2)) & ! [v0: $i] : (v0 = empty_set | ~ $i(v0) | ~ % 29.39/4.71 | element(v0, all_48_0) | ? [v1: $i] : ? [v2: $i] : ($i(v1) & % 29.39/4.71 | element(v1, all_48_1) & ( ~ in(v1, v0) | % 29.39/4.71 | (subset_complement(all_29_3, v1) = v2 & $i(v2) & ~ in(v2, % 29.39/4.71 | all_29_2))) & (in(v1, v0) | (subset_complement(all_29_3, % 29.39/4.71 | v1) = v2 & $i(v2) & in(v2, all_29_2)))))) % 29.39/4.71 | % 29.39/4.71 | REDUCE: (6), (16) imply: % 29.39/4.71 | (37) $i(empty_set) % 29.39/4.71 | % 29.39/4.71 | GROUND_INST: instantiating (3) with all_29_1, all_48_1, all_29_3, simplifying % 29.39/4.71 | with (13), (34) gives: % 29.39/4.71 | (38) all_48_1 = all_29_1 % 29.39/4.71 | % 29.39/4.71 | GROUND_INST: instantiating (3) with all_45_1, all_48_1, all_29_3, simplifying % 29.39/4.71 | with (30), (34) gives: % 29.39/4.71 | (39) all_48_1 = all_45_1 % 29.39/4.71 | % 29.39/4.71 | GROUND_INST: instantiating (3) with all_29_0, all_48_0, all_29_1, simplifying % 29.39/4.71 | with (14) gives: % 29.39/4.72 | (40) all_48_0 = all_29_0 | ~ (powerset(all_29_1) = all_48_0) % 29.39/4.72 | % 29.39/4.72 | GROUND_INST: instantiating (3) with all_45_0, all_48_0, all_45_1, simplifying % 29.39/4.72 | with (31) gives: % 29.39/4.72 | (41) all_48_0 = all_45_0 | ~ (powerset(all_45_1) = all_48_0) % 29.39/4.72 | % 29.39/4.72 | COMBINE_EQS: (38), (39) imply: % 29.39/4.72 | (42) all_45_1 = all_29_1 % 29.39/4.72 | % 29.39/4.72 | REDUCE: (35), (38) imply: % 29.39/4.72 | (43) powerset(all_29_1) = all_48_0 % 29.39/4.72 | % 29.39/4.72 | BETA: splitting (41) gives: % 29.39/4.72 | % 29.39/4.72 | Case 1: % 29.39/4.72 | | % 29.39/4.72 | | (44) ~ (powerset(all_45_1) = all_48_0) % 29.39/4.72 | | % 29.39/4.72 | | REDUCE: (42), (44) imply: % 29.39/4.72 | | (45) ~ (powerset(all_29_1) = all_48_0) % 29.39/4.72 | | % 29.39/4.72 | | PRED_UNIFY: (43), (45) imply: % 29.39/4.72 | | (46) $false % 29.39/4.72 | | % 29.39/4.72 | | CLOSE: (46) is inconsistent. % 29.39/4.72 | | % 29.39/4.72 | Case 2: % 29.39/4.72 | | % 29.39/4.72 | | (47) all_48_0 = all_45_0 % 29.39/4.72 | | % 29.39/4.72 | | REDUCE: (43), (47) imply: % 29.39/4.72 | | (48) powerset(all_29_1) = all_45_0 % 29.39/4.72 | | % 29.39/4.72 | | BETA: splitting (40) gives: % 29.39/4.72 | | % 29.39/4.72 | | Case 1: % 29.39/4.72 | | | % 29.39/4.72 | | | (49) ~ (powerset(all_29_1) = all_48_0) % 29.39/4.72 | | | % 29.39/4.72 | | | PRED_UNIFY: (43), (49) imply: % 29.39/4.72 | | | (50) $false % 29.39/4.72 | | | % 29.39/4.72 | | | CLOSE: (50) is inconsistent. % 29.39/4.72 | | | % 29.39/4.72 | | Case 2: % 29.39/4.72 | | | % 29.39/4.72 | | | (51) all_48_0 = all_29_0 % 29.39/4.72 | | | % 29.39/4.72 | | | COMBINE_EQS: (47), (51) imply: % 29.39/4.72 | | | (52) all_45_0 = all_29_0 % 29.39/4.72 | | | % 29.39/4.72 | | | BETA: splitting (32) gives: % 29.39/4.72 | | | % 29.39/4.72 | | | Case 1: % 29.39/4.72 | | | | % 29.39/4.72 | | | | (53) all_47_0 = all_29_2 & complements_of_subsets(all_29_3, % 29.39/4.72 | | | | empty_set) = all_29_2 % 29.39/4.72 | | | | % 29.39/4.72 | | | | ALPHA: (53) implies: % 29.39/4.72 | | | | (54) complements_of_subsets(all_29_3, empty_set) = all_29_2 % 29.39/4.72 | | | | % 29.39/4.72 | | | | BETA: splitting (36) gives: % 29.39/4.72 | | | | % 29.39/4.72 | | | | Case 1: % 29.39/4.72 | | | | | % 29.39/4.72 | | | | | (55) ~ element(all_29_2, all_48_0) % 29.39/4.72 | | | | | % 29.39/4.72 | | | | | REDUCE: (51), (55) imply: % 29.39/4.72 | | | | | (56) ~ element(all_29_2, all_29_0) % 29.39/4.72 | | | | | % 29.39/4.72 | | | | | PRED_UNIFY: (9), (56) imply: % 29.39/4.72 | | | | | (57) $false % 29.39/4.72 | | | | | % 29.39/4.72 | | | | | CLOSE: (57) is inconsistent. % 29.39/4.72 | | | | | % 29.39/4.72 | | | | Case 2: % 29.39/4.72 | | | | | % 29.39/4.72 | | | | | (58) element(all_29_2, all_48_0) % 29.39/4.72 | | | | | (59) ! [v0: $i] : ! [v1: $i] : ( ~ (subset_complement(all_29_3, % 29.39/4.72 | | | | | v0) = v1) | ~ $i(v0) | ~ $i(empty_set) | ~ % 29.39/4.72 | | | | | element(v0, all_48_1) | ~ element(empty_set, all_48_0) | ~ % 29.39/4.72 | | | | | in(v1, all_29_2) | in(v0, empty_set)) & ! [v0: $i] : ! % 29.39/4.72 | | | | | [v1: $i] : ( ~ (subset_complement(all_29_3, v0) = v1) | ~ % 29.39/4.72 | | | | | $i(v0) | ~ $i(empty_set) | ~ element(v0, all_48_1) | ~ % 29.39/4.72 | | | | | element(empty_set, all_48_0) | ~ in(v0, empty_set) | in(v1, % 29.39/4.72 | | | | | all_29_2)) & ! [v0: $i] : (v0 = empty_set | ~ $i(v0) | % 29.39/4.72 | | | | | ~ element(v0, all_48_0) | ? [v1: $i] : ? [v2: $i] : % 29.39/4.72 | | | | | ($i(v1) & element(v1, all_48_1) & ( ~ in(v1, v0) | % 29.39/4.72 | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & ~ % 29.39/4.72 | | | | | in(v2, all_29_2))) & (in(v1, v0) | % 29.39/4.72 | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & in(v2, % 29.39/4.72 | | | | | all_29_2))))) % 29.39/4.72 | | | | | % 29.39/4.72 | | | | | ALPHA: (59) implies: % 29.39/4.72 | | | | | (60) ! [v0: $i] : (v0 = empty_set | ~ $i(v0) | ~ element(v0, % 29.39/4.72 | | | | | all_48_0) | ? [v1: $i] : ? [v2: $i] : ($i(v1) & % 29.39/4.72 | | | | | element(v1, all_48_1) & ( ~ in(v1, v0) | % 29.39/4.72 | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & ~ % 29.39/4.72 | | | | | in(v2, all_29_2))) & (in(v1, v0) | % 29.39/4.72 | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & in(v2, % 29.39/4.72 | | | | | all_29_2))))) % 29.39/4.72 | | | | | % 29.39/4.72 | | | | | GROUND_INST: instantiating (60) with all_29_2, simplifying with (11) % 29.39/4.72 | | | | | gives: % 29.39/4.72 | | | | | (61) all_29_2 = empty_set | ~ element(all_29_2, all_48_0) | ? % 29.39/4.72 | | | | | [v0: $i] : ? [v1: $i] : ($i(v0) & element(v0, all_48_1) & ( ~ % 29.39/4.72 | | | | | in(v0, all_29_2) | (subset_complement(all_29_3, v0) = v1 & % 29.39/4.73 | | | | | $i(v1) & ~ in(v1, all_29_2))) & (in(v0, all_29_2) | % 29.39/4.73 | | | | | (subset_complement(all_29_3, v0) = v1 & $i(v1) & in(v1, % 29.39/4.73 | | | | | all_29_2)))) % 29.39/4.73 | | | | | % 29.39/4.73 | | | | | BETA: splitting (61) gives: % 29.39/4.73 | | | | | % 29.39/4.73 | | | | | Case 1: % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | (62) ~ element(all_29_2, all_48_0) % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | REDUCE: (51), (62) imply: % 29.39/4.73 | | | | | | (63) ~ element(all_29_2, all_29_0) % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | PRED_UNIFY: (9), (63) imply: % 29.39/4.73 | | | | | | (64) $false % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | CLOSE: (64) is inconsistent. % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | Case 2: % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | GROUND_INST: instantiating (t8_boole) with all_41_0, all_43_0, % 29.39/4.73 | | | | | | simplifying with (24), (25), (27), (28) gives: % 29.39/4.73 | | | | | | (65) all_43_0 = all_41_0 % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | GROUND_INST: instantiating (1) with all_43_0, simplifying with (27), % 29.39/4.73 | | | | | | (28) gives: % 29.39/4.73 | | | | | | (66) all_43_0 = empty_set % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | GROUND_INST: instantiating (d8_setfam_1) with all_29_3, empty_set, % 29.39/4.73 | | | | | | all_29_2, simplifying with (10), (37), (54) gives: % 29.39/4.73 | | | | | | (67) ? [v0: $i] : ? [v1: $i] : (powerset(v0) = v1 & % 29.39/4.73 | | | | | | powerset(all_29_3) = v0 & $i(v1) & $i(v0) & ( ~ % 29.39/4.73 | | | | | | element(empty_set, v1) | ( ! [v2: $i] : ! [v3: $i] : ( % 29.39/4.73 | | | | | | ~ (subset_complement(all_29_3, v2) = v3) | ~ $i(v2) % 29.39/4.73 | | | | | | | ~ $i(all_29_2) | ~ element(v2, v0) | ~ % 29.39/4.73 | | | | | | element(all_29_2, v1) | ~ in(v3, empty_set) | % 29.39/4.73 | | | | | | in(v2, all_29_2)) & ! [v2: $i] : ! [v3: $i] : ( ~ % 29.39/4.73 | | | | | | (subset_complement(all_29_3, v2) = v3) | ~ $i(v2) | % 29.39/4.73 | | | | | | ~ $i(all_29_2) | ~ element(v2, v0) | ~ % 29.39/4.73 | | | | | | element(all_29_2, v1) | ~ in(v2, all_29_2) | in(v3, % 29.39/4.73 | | | | | | empty_set)) & ! [v2: any] : (v2 = all_29_2 | ~ % 29.39/4.73 | | | | | | $i(v2) | ~ element(v2, v1) | ? [v3: $i] : ? [v4: % 29.39/4.73 | | | | | | $i] : ($i(v3) & element(v3, v0) & ( ~ in(v3, v2) | % 29.39/4.73 | | | | | | (subset_complement(all_29_3, v3) = v4 & $i(v4) & % 29.39/4.73 | | | | | | ~ in(v4, empty_set))) & (in(v3, v2) | % 29.39/4.73 | | | | | | (subset_complement(all_29_3, v3) = v4 & $i(v4) & % 29.39/4.73 | | | | | | in(v4, empty_set)))))))) % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | COMBINE_EQS: (65), (66) imply: % 29.39/4.73 | | | | | | (68) all_41_0 = empty_set % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | DELTA: instantiating (67) with fresh symbols all_90_0, all_90_1 % 29.39/4.73 | | | | | | gives: % 29.39/4.73 | | | | | | (69) powerset(all_90_1) = all_90_0 & powerset(all_29_3) = % 29.39/4.73 | | | | | | all_90_1 & $i(all_90_0) & $i(all_90_1) & ( ~ % 29.39/4.73 | | | | | | element(empty_set, all_90_0) | ( ! [v0: $i] : ! [v1: $i] % 29.39/4.73 | | | | | | : ( ~ (subset_complement(all_29_3, v0) = v1) | ~ $i(v0) % 29.39/4.73 | | | | | | | ~ $i(all_29_2) | ~ element(v0, all_90_1) | ~ % 29.39/4.73 | | | | | | element(all_29_2, all_90_0) | ~ in(v1, empty_set) | % 29.39/4.73 | | | | | | in(v0, all_29_2)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 29.39/4.73 | | | | | | (subset_complement(all_29_3, v0) = v1) | ~ $i(v0) | % 29.39/4.73 | | | | | | ~ $i(all_29_2) | ~ element(v0, all_90_1) | ~ % 29.39/4.73 | | | | | | element(all_29_2, all_90_0) | ~ in(v0, all_29_2) | % 29.39/4.73 | | | | | | in(v1, empty_set)) & ! [v0: any] : (v0 = all_29_2 | % 29.39/4.73 | | | | | | ~ $i(v0) | ~ element(v0, all_90_0) | ? [v1: $i] : ? % 29.39/4.73 | | | | | | [v2: $i] : ($i(v1) & element(v1, all_90_1) & ( ~ % 29.39/4.73 | | | | | | in(v1, v0) | (subset_complement(all_29_3, v1) = v2 % 29.39/4.73 | | | | | | & $i(v2) & ~ in(v2, empty_set))) & (in(v1, v0) % 29.39/4.73 | | | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & % 29.39/4.73 | | | | | | in(v2, empty_set))))))) % 29.39/4.73 | | | | | | % 29.39/4.73 | | | | | | ALPHA: (69) implies: % 29.39/4.73 | | | | | | (70) powerset(all_29_3) = all_90_1 % 29.39/4.73 | | | | | | (71) powerset(all_90_1) = all_90_0 % 29.39/4.73 | | | | | | (72) ~ element(empty_set, all_90_0) | ( ! [v0: $i] : ! [v1: $i] % 29.39/4.73 | | | | | | : ( ~ (subset_complement(all_29_3, v0) = v1) | ~ $i(v0) | % 29.39/4.73 | | | | | | ~ $i(all_29_2) | ~ element(v0, all_90_1) | ~ % 29.39/4.73 | | | | | | element(all_29_2, all_90_0) | ~ in(v1, empty_set) | % 29.39/4.73 | | | | | | in(v0, all_29_2)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 29.39/4.73 | | | | | | (subset_complement(all_29_3, v0) = v1) | ~ $i(v0) | ~ % 29.39/4.73 | | | | | | $i(all_29_2) | ~ element(v0, all_90_1) | ~ % 29.39/4.73 | | | | | | element(all_29_2, all_90_0) | ~ in(v0, all_29_2) | % 29.39/4.73 | | | | | | in(v1, empty_set)) & ! [v0: any] : (v0 = all_29_2 | ~ % 29.39/4.73 | | | | | | $i(v0) | ~ element(v0, all_90_0) | ? [v1: $i] : ? % 29.39/4.73 | | | | | | [v2: $i] : ($i(v1) & element(v1, all_90_1) & ( ~ in(v1, % 29.39/4.73 | | | | | | v0) | (subset_complement(all_29_3, v1) = v2 & % 29.39/4.73 | | | | | | $i(v2) & ~ in(v2, empty_set))) & (in(v1, v0) | % 29.39/4.73 | | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & % 29.39/4.73 | | | | | | in(v2, empty_set)))))) % 29.39/4.74 | | | | | | % 29.39/4.74 | | | | | | REDUCE: (24), (68) imply: % 29.39/4.74 | | | | | | (73) empty(empty_set) % 29.39/4.74 | | | | | | % 29.39/4.74 | | | | | | REDUCE: (23), (68) imply: % 29.39/4.74 | | | | | | (74) element(empty_set, all_29_0) % 29.39/4.74 | | | | | | % 29.39/4.74 | | | | | | GROUND_INST: instantiating (3) with all_29_1, all_90_1, all_29_3, % 29.39/4.74 | | | | | | simplifying with (13), (70) gives: % 29.39/4.74 | | | | | | (75) all_90_1 = all_29_1 % 29.39/4.74 | | | | | | % 29.39/4.74 | | | | | | GROUND_INST: instantiating (3) with all_29_0, all_90_0, all_29_1, % 29.39/4.74 | | | | | | simplifying with (14) gives: % 29.39/4.74 | | | | | | (76) all_90_0 = all_29_0 | ~ (powerset(all_29_1) = all_90_0) % 29.39/4.74 | | | | | | % 29.39/4.74 | | | | | | REDUCE: (71), (75) imply: % 29.39/4.74 | | | | | | (77) powerset(all_29_1) = all_90_0 % 29.39/4.74 | | | | | | % 29.39/4.74 | | | | | | BETA: splitting (76) gives: % 29.39/4.74 | | | | | | % 29.39/4.74 | | | | | | Case 1: % 29.39/4.74 | | | | | | | % 29.39/4.74 | | | | | | | (78) ~ (powerset(all_29_1) = all_90_0) % 29.39/4.74 | | | | | | | % 29.39/4.74 | | | | | | | PRED_UNIFY: (77), (78) imply: % 29.39/4.74 | | | | | | | (79) $false % 29.39/4.74 | | | | | | | % 29.39/4.74 | | | | | | | CLOSE: (79) is inconsistent. % 29.39/4.74 | | | | | | | % 29.39/4.74 | | | | | | Case 2: % 29.39/4.74 | | | | | | | % 29.39/4.74 | | | | | | | (80) all_90_0 = all_29_0 % 29.39/4.74 | | | | | | | % 29.39/4.74 | | | | | | | BETA: splitting (72) gives: % 29.39/4.74 | | | | | | | % 29.39/4.74 | | | | | | | Case 1: % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | (81) ~ element(empty_set, all_90_0) % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | REDUCE: (80), (81) imply: % 29.39/4.74 | | | | | | | | (82) ~ element(empty_set, all_29_0) % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | PRED_UNIFY: (74), (82) imply: % 29.39/4.74 | | | | | | | | (83) $false % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | CLOSE: (83) is inconsistent. % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | Case 2: % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | (84) element(empty_set, all_90_0) % 29.39/4.74 | | | | | | | | (85) ! [v0: $i] : ! [v1: $i] : ( ~ % 29.39/4.74 | | | | | | | | (subset_complement(all_29_3, v0) = v1) | ~ $i(v0) | % 29.39/4.74 | | | | | | | | ~ $i(all_29_2) | ~ element(v0, all_90_1) | ~ % 29.39/4.74 | | | | | | | | element(all_29_2, all_90_0) | ~ in(v1, empty_set) | % 29.39/4.74 | | | | | | | | in(v0, all_29_2)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 29.39/4.74 | | | | | | | | (subset_complement(all_29_3, v0) = v1) | ~ $i(v0) | % 29.39/4.74 | | | | | | | | ~ $i(all_29_2) | ~ element(v0, all_90_1) | ~ % 29.39/4.74 | | | | | | | | element(all_29_2, all_90_0) | ~ in(v0, all_29_2) | % 29.39/4.74 | | | | | | | | in(v1, empty_set)) & ! [v0: any] : (v0 = all_29_2 | % 29.39/4.74 | | | | | | | | ~ $i(v0) | ~ element(v0, all_90_0) | ? [v1: $i] : ? % 29.39/4.74 | | | | | | | | [v2: $i] : ($i(v1) & element(v1, all_90_1) & ( ~ % 29.39/4.74 | | | | | | | | in(v1, v0) | (subset_complement(all_29_3, v1) = v2 % 29.39/4.74 | | | | | | | | & $i(v2) & ~ in(v2, empty_set))) & (in(v1, v0) % 29.39/4.74 | | | | | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & % 29.39/4.74 | | | | | | | | in(v2, empty_set))))) % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | ALPHA: (85) implies: % 29.39/4.74 | | | | | | | | (86) ! [v0: any] : (v0 = all_29_2 | ~ $i(v0) | ~ % 29.39/4.74 | | | | | | | | element(v0, all_90_0) | ? [v1: $i] : ? [v2: $i] : % 29.39/4.74 | | | | | | | | ($i(v1) & element(v1, all_90_1) & ( ~ in(v1, v0) | % 29.39/4.74 | | | | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & % 29.39/4.74 | | | | | | | | ~ in(v2, empty_set))) & (in(v1, v0) | % 29.39/4.74 | | | | | | | | (subset_complement(all_29_3, v1) = v2 & $i(v2) & % 29.39/4.74 | | | | | | | | in(v2, empty_set))))) % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | GROUND_INST: instantiating (86) with empty_set, simplifying with % 29.39/4.74 | | | | | | | | (37) gives: % 29.39/4.74 | | | | | | | | (87) all_29_2 = empty_set | ~ element(empty_set, all_90_0) | % 29.39/4.74 | | | | | | | | ? [v0: $i] : ? [v1: $i] : ($i(v0) & element(v0, % 29.39/4.74 | | | | | | | | all_90_1) & ( ~ in(v0, empty_set) | % 29.39/4.74 | | | | | | | | (subset_complement(all_29_3, v0) = v1 & $i(v1) & ~ % 29.39/4.74 | | | | | | | | in(v1, empty_set))) & (in(v0, empty_set) | % 29.39/4.74 | | | | | | | | (subset_complement(all_29_3, v0) = v1 & $i(v1) & % 29.39/4.74 | | | | | | | | in(v1, empty_set)))) % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | BETA: splitting (87) gives: % 29.39/4.74 | | | | | | | | % 29.39/4.74 | | | | | | | | Case 1: % 29.39/4.74 | | | | | | | | | % 29.39/4.74 | | | | | | | | | (88) ~ element(empty_set, all_90_0) % 29.39/4.74 | | | | | | | | | % 29.39/4.74 | | | | | | | | | REDUCE: (80), (88) imply: % 29.39/4.74 | | | | | | | | | (89) ~ element(empty_set, all_29_0) % 29.39/4.74 | | | | | | | | | % 29.39/4.74 | | | | | | | | | PRED_UNIFY: (74), (89) imply: % 29.39/4.74 | | | | | | | | | (90) $false % 29.39/4.74 | | | | | | | | | % 29.39/4.74 | | | | | | | | | CLOSE: (90) is inconsistent. % 29.39/4.74 | | | | | | | | | % 29.39/4.74 | | | | | | | | Case 2: % 29.39/4.74 | | | | | | | | | % 29.39/4.74 | | | | | | | | | (91) all_29_2 = empty_set | ? [v0: $i] : ? [v1: $i] : % 29.39/4.74 | | | | | | | | | ($i(v0) & element(v0, all_90_1) & ( ~ in(v0, % 29.39/4.74 | | | | | | | | | empty_set) | (subset_complement(all_29_3, v0) = % 29.39/4.74 | | | | | | | | | v1 & $i(v1) & ~ in(v1, empty_set))) & (in(v0, % 29.39/4.74 | | | | | | | | | empty_set) | (subset_complement(all_29_3, v0) = % 29.39/4.74 | | | | | | | | | v1 & $i(v1) & in(v1, empty_set)))) % 29.39/4.74 | | | | | | | | | % 29.39/4.74 | | | | | | | | | BETA: splitting (91) gives: % 29.39/4.74 | | | | | | | | | % 29.39/4.74 | | | | | | | | | Case 1: % 29.39/4.74 | | | | | | | | | | % 29.39/4.74 | | | | | | | | | | (92) all_29_2 = empty_set % 29.39/4.74 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | REDUCE: (8), (92) imply: % 29.39/4.75 | | | | | | | | | | (93) $false % 29.39/4.75 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | CLOSE: (93) is inconsistent. % 29.39/4.75 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | Case 2: % 29.39/4.75 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | (94) ? [v0: $i] : ? [v1: $i] : ($i(v0) & element(v0, % 29.39/4.75 | | | | | | | | | | all_90_1) & ( ~ in(v0, empty_set) | % 29.39/4.75 | | | | | | | | | | (subset_complement(all_29_3, v0) = v1 & $i(v1) & % 29.39/4.75 | | | | | | | | | | ~ in(v1, empty_set))) & (in(v0, empty_set) | % 29.39/4.75 | | | | | | | | | | (subset_complement(all_29_3, v0) = v1 & $i(v1) & % 29.39/4.75 | | | | | | | | | | in(v1, empty_set)))) % 29.39/4.75 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | DELTA: instantiating (94) with fresh symbols all_153_0, % 29.39/4.75 | | | | | | | | | | all_153_1 gives: % 29.39/4.75 | | | | | | | | | | (95) $i(all_153_1) & element(all_153_1, all_90_1) & ( ~ % 29.39/4.75 | | | | | | | | | | in(all_153_1, empty_set) | % 29.39/4.75 | | | | | | | | | | (subset_complement(all_29_3, all_153_1) = % 29.39/4.75 | | | | | | | | | | all_153_0 & $i(all_153_0) & ~ in(all_153_0, % 29.39/4.75 | | | | | | | | | | empty_set))) & (in(all_153_1, empty_set) | % 29.39/4.75 | | | | | | | | | | (subset_complement(all_29_3, all_153_1) = % 29.39/4.75 | | | | | | | | | | all_153_0 & $i(all_153_0) & in(all_153_0, % 29.39/4.75 | | | | | | | | | | empty_set))) % 29.39/4.75 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | ALPHA: (95) implies: % 29.39/4.75 | | | | | | | | | | (96) $i(all_153_1) % 29.39/4.75 | | | | | | | | | | (97) in(all_153_1, empty_set) | % 29.39/4.75 | | | | | | | | | | (subset_complement(all_29_3, all_153_1) = all_153_0 % 29.39/4.75 | | | | | | | | | | & $i(all_153_0) & in(all_153_0, empty_set)) % 29.39/4.75 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | BETA: splitting (97) gives: % 29.39/4.75 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | Case 1: % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | | (98) in(all_153_1, empty_set) % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | | GROUND_INST: instantiating (t7_boole) with all_153_1, % 29.39/4.75 | | | | | | | | | | | empty_set, simplifying with (37), (73), (96), (98) % 29.39/4.75 | | | | | | | | | | | gives: % 29.39/4.75 | | | | | | | | | | | (99) $false % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | | CLOSE: (99) is inconsistent. % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | Case 2: % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | | (100) subset_complement(all_29_3, all_153_1) = all_153_0 % 29.39/4.75 | | | | | | | | | | | & $i(all_153_0) & in(all_153_0, empty_set) % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | | ALPHA: (100) implies: % 29.39/4.75 | | | | | | | | | | | (101) in(all_153_0, empty_set) % 29.39/4.75 | | | | | | | | | | | (102) $i(all_153_0) % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | | GROUND_INST: instantiating (t7_boole) with all_153_0, % 29.39/4.75 | | | | | | | | | | | empty_set, simplifying with (37), (73), (101), % 29.39/4.75 | | | | | | | | | | | (102) gives: % 29.39/4.75 | | | | | | | | | | | (103) $false % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | | CLOSE: (103) is inconsistent. % 29.39/4.75 | | | | | | | | | | | % 29.39/4.75 | | | | | | | | | | End of split % 29.39/4.75 | | | | | | | | | | % 29.39/4.75 | | | | | | | | | End of split % 29.39/4.75 | | | | | | | | | % 29.39/4.75 | | | | | | | | End of split % 29.39/4.75 | | | | | | | | % 29.39/4.75 | | | | | | | End of split % 29.39/4.75 | | | | | | | % 29.39/4.75 | | | | | | End of split % 29.39/4.75 | | | | | | % 29.39/4.75 | | | | | End of split % 29.39/4.75 | | | | | % 29.39/4.75 | | | | End of split % 29.39/4.75 | | | | % 29.39/4.75 | | | Case 2: % 29.39/4.75 | | | | % 29.39/4.75 | | | | (104) powerset(all_47_2) = all_47_1 & powerset(all_29_3) = all_47_2 & % 29.39/4.75 | | | | $i(all_47_1) & $i(all_47_2) & ~ element(all_29_2, all_47_1) % 29.39/4.75 | | | | % 29.39/4.75 | | | | ALPHA: (104) implies: % 29.39/4.75 | | | | (105) ~ element(all_29_2, all_47_1) % 29.39/4.75 | | | | (106) powerset(all_29_3) = all_47_2 % 29.39/4.75 | | | | (107) powerset(all_47_2) = all_47_1 % 29.39/4.75 | | | | % 29.39/4.75 | | | | GROUND_INST: instantiating (3) with all_29_1, all_47_2, all_29_3, % 29.39/4.75 | | | | simplifying with (13), (106) gives: % 29.39/4.75 | | | | (108) all_47_2 = all_29_1 % 29.39/4.75 | | | | % 29.39/4.75 | | | | GROUND_INST: instantiating (3) with all_29_0, all_47_1, all_29_1, % 29.39/4.75 | | | | simplifying with (14) gives: % 29.39/4.75 | | | | (109) all_47_1 = all_29_0 | ~ (powerset(all_29_1) = all_47_1) % 29.39/4.75 | | | | % 29.39/4.75 | | | | PRED_UNIFY: (9), (105) imply: % 29.39/4.75 | | | | (110) ~ (all_47_1 = all_29_0) % 29.39/4.75 | | | | % 29.39/4.75 | | | | REDUCE: (107), (108) imply: % 29.39/4.75 | | | | (111) powerset(all_29_1) = all_47_1 % 29.39/4.75 | | | | % 29.39/4.75 | | | | BETA: splitting (109) gives: % 29.39/4.75 | | | | % 29.39/4.75 | | | | Case 1: % 29.39/4.75 | | | | | % 29.39/4.75 | | | | | (112) ~ (powerset(all_29_1) = all_47_1) % 29.39/4.75 | | | | | % 29.39/4.75 | | | | | PRED_UNIFY: (111), (112) imply: % 29.39/4.75 | | | | | (113) $false % 29.39/4.75 | | | | | % 29.39/4.75 | | | | | CLOSE: (113) is inconsistent. % 29.39/4.75 | | | | | % 29.39/4.75 | | | | Case 2: % 29.39/4.75 | | | | | % 29.39/4.75 | | | | | (114) all_47_1 = all_29_0 % 29.39/4.75 | | | | | % 29.39/4.75 | | | | | REDUCE: (110), (114) imply: % 29.39/4.75 | | | | | (115) $false % 29.39/4.75 | | | | | % 29.39/4.75 | | | | | CLOSE: (115) is inconsistent. % 29.39/4.75 | | | | | % 29.39/4.75 | | | | End of split % 29.39/4.75 | | | | % 29.39/4.75 | | | End of split % 29.39/4.75 | | | % 29.39/4.75 | | End of split % 29.39/4.75 | | % 29.39/4.75 | End of split % 29.39/4.75 | % 29.39/4.75 End of proof % 29.39/4.75 % SZS output end Proof for theBenchmark % 29.39/4.75 % 29.39/4.75 4118ms %------------------------------------------------------------------------------