%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEU373+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 : n008.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:44:21 EDT 2023 % Result : Theorem 21.61s 3.78s % Output : Proof 33.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SEU373+1 : TPTP v8.1.2. Released v3.3.0. % 0.12/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n008.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Aug 23 20:06:32 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.62 Running up to 7 provers in parallel. % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.94/1.18 Prover 4: Preprocessing ... % 2.94/1.18 Prover 1: Preprocessing ... % 3.40/1.22 Prover 5: Preprocessing ... % 3.40/1.22 Prover 3: Preprocessing ... % 3.40/1.22 Prover 2: Preprocessing ... % 3.40/1.22 Prover 6: Preprocessing ... % 3.40/1.22 Prover 0: Preprocessing ... % 7.37/1.76 Prover 1: Warning: ignoring some quantifiers % 7.93/1.86 Prover 1: Constructing countermodel ... % 7.93/1.87 Prover 5: Proving ... % 8.27/1.92 Prover 3: Warning: ignoring some quantifiers % 8.27/1.93 Prover 2: Proving ... % 8.74/1.94 Prover 3: Constructing countermodel ... % 8.74/1.94 Prover 6: Proving ... % 10.94/2.27 Prover 4: Warning: ignoring some quantifiers % 11.44/2.37 Prover 4: Constructing countermodel ... % 12.09/2.45 Prover 0: Proving ... % 21.61/3.78 Prover 5: proved (3146ms) % 21.61/3.78 % 21.61/3.78 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 21.61/3.78 % 21.61/3.79 Prover 2: stopped % 21.61/3.79 Prover 0: stopped % 22.13/3.80 Prover 3: stopped % 22.13/3.80 Prover 6: stopped % 22.13/3.80 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 22.13/3.80 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 22.13/3.80 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 22.13/3.80 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 22.13/3.82 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 22.73/3.88 Prover 7: Preprocessing ... % 22.73/3.89 Prover 10: Preprocessing ... % 22.95/3.90 Prover 11: Preprocessing ... % 22.95/3.91 Prover 8: Preprocessing ... % 22.95/3.92 Prover 13: Preprocessing ... % 23.14/3.98 Prover 10: Warning: ignoring some quantifiers % 23.14/3.99 Prover 10: Constructing countermodel ... % 23.14/4.01 Prover 7: Warning: ignoring some quantifiers % 23.92/4.03 Prover 7: Constructing countermodel ... % 23.92/4.08 Prover 13: Warning: ignoring some quantifiers % 24.48/4.11 Prover 8: Warning: ignoring some quantifiers % 24.48/4.12 Prover 13: Constructing countermodel ... % 24.48/4.12 Prover 8: Constructing countermodel ... % 24.48/4.21 Prover 11: Warning: ignoring some quantifiers % 24.48/4.22 Prover 11: Constructing countermodel ... % 32.43/5.16 Prover 13: Found proof (size 189) % 32.43/5.16 Prover 13: proved (1334ms) % 32.43/5.16 Prover 7: stopped % 32.43/5.16 Prover 10: stopped % 32.43/5.16 Prover 11: stopped % 32.43/5.16 Prover 4: stopped % 32.43/5.16 Prover 8: stopped % 32.43/5.16 Prover 1: stopped % 32.43/5.16 % 32.43/5.16 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 32.43/5.16 % 32.49/5.19 % SZS output start Proof for theBenchmark % 32.49/5.20 Assumptions after simplification: % 32.49/5.20 --------------------------------- % 32.49/5.20 % 32.49/5.20 (d13_yellow_0) % 32.67/5.22 ! [v0: $i] : ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 32.67/5.22 rel_str(v0) | ? [v2: $i] : (the_carrier(v0) = v2 & $i(v2) & ! [v3: $i] : % 32.67/5.22 ! [v4: $i] : ( ~ (the_InternalRel(v3) = v4) | ~ $i(v3) | ~ rel_str(v3) | % 32.67/5.22 ? [v5: $i] : (the_carrier(v3) = v5 & $i(v5) & ( ~ subset(v5, v2) | ~ % 32.67/5.22 subset(v4, v1) | subrelstr(v3, v0)) & ( ~ subrelstr(v3, v0) | % 32.67/5.23 (subset(v5, v2) & subset(v4, v1))))))) & ! [v0: $i] : ( ~ $i(v0) | % 32.67/5.23 ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] : (the_carrier(v0) = v1 & % 32.67/5.23 the_InternalRel(v0) = v2 & $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ % 32.67/5.23 rel_str(v3) | ? [v4: $i] : ? [v5: $i] : (the_carrier(v3) = v4 & % 32.67/5.23 the_InternalRel(v3) = v5 & $i(v5) & $i(v4) & ( ~ subset(v5, v2) | ~ % 32.67/5.23 subset(v4, v1) | subrelstr(v3, v0)) & ( ~ subrelstr(v3, v0) | % 32.67/5.23 (subset(v5, v2) & subset(v4, v1))))))) % 32.67/5.23 % 32.67/5.23 (d8_yellow_6) % 32.67/5.23 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (the_mapping(v0, % 32.67/5.23 v2) = v3) | ~ (the_carrier(v0) = v1) | ~ $i(v2) | ~ $i(v0) | ~ % 32.67/5.23 net_str(v2, v0) | ~ one_sorted_str(v0) | ? [v4: $i] : (the_carrier(v2) = % 32.67/5.23 v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ( ~ % 32.67/5.23 (relation_dom_restr_as_relation_of(v4, v1, v3, v6) = v7) | ~ % 32.67/5.23 (the_carrier(v5) = v6) | ~ $i(v5) | ~ net_str(v5, v0) | ? [v8: $i] : % 32.67/5.23 (the_mapping(v0, v5) = v8 & $i(v8) & ( ~ (v8 = v7) | ~ subrelstr(v5, % 32.67/5.23 v2) | subnetstr(v5, v0, v2)) & ( ~ subnetstr(v5, v0, v2) | (v8 = % 32.67/5.23 v7 & subrelstr(v5, v2))))))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 32.67/5.23 one_sorted_str(v0) | ? [v1: $i] : (the_carrier(v0) = v1 & $i(v1) & ! [v2: % 32.67/5.23 $i] : ( ~ $i(v2) | ~ net_str(v2, v0) | ? [v3: $i] : ? [v4: $i] : % 32.67/5.23 (the_mapping(v0, v2) = v4 & the_carrier(v2) = v3 & $i(v4) & $i(v3) & ! % 32.67/5.23 [v5: $i] : ( ~ $i(v5) | ~ net_str(v5, v0) | ? [v6: $i] : ? [v7: $i] % 32.67/5.23 : ? [v8: $i] : (the_mapping(v0, v5) = v6 & % 32.67/5.23 relation_dom_restr_as_relation_of(v3, v1, v4, v7) = v8 & % 32.67/5.23 the_carrier(v5) = v7 & $i(v8) & $i(v7) & $i(v6) & ( ~ (v8 = v6) | % 32.67/5.23 ~ subrelstr(v5, v2) | subnetstr(v5, v0, v2)) & ( ~ subnetstr(v5, % 32.67/5.23 v0, v2) | (v8 = v6 & subrelstr(v5, v2))))))))) % 32.67/5.23 % 32.67/5.23 (dt_l1_waybel_0) % 32.67/5.23 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ net_str(v1, v0) | ~ % 32.67/5.23 one_sorted_str(v0) | rel_str(v1)) % 32.67/5.23 % 32.67/5.23 (dt_m1_yellow_0) % 32.67/5.23 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ subrelstr(v1, v0) | ~ % 32.67/5.23 rel_str(v0) | rel_str(v1)) % 32.67/5.23 % 32.67/5.23 (dt_m1_yellow_6) % 32.67/5.23 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 32.67/5.23 ~ subnetstr(v2, v0, v1) | ~ net_str(v1, v0) | ~ one_sorted_str(v0) | % 32.67/5.23 net_str(v2, v0)) % 32.67/5.23 % 32.67/5.23 (dt_u1_orders_2) % 32.67/5.23 ! [v0: $i] : ! [v1: $i] : ( ~ (the_InternalRel(v0) = v1) | ~ $i(v0) | ~ % 32.67/5.23 rel_str(v0) | ? [v2: $i] : (the_carrier(v0) = v2 & $i(v2) & % 32.67/5.23 relation_of2_as_subset(v1, v2, v2))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 32.67/5.23 rel_str(v0) | ? [v1: $i] : ? [v2: $i] : (the_carrier(v0) = v2 & % 32.67/5.23 the_InternalRel(v0) = v1 & $i(v2) & $i(v1) & relation_of2_as_subset(v1, % 32.67/5.23 v2, v2))) % 32.67/5.23 % 32.67/5.23 (dt_u1_waybel_0) % 32.67/5.24 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (the_mapping(v0, v1) = v2) | ~ % 32.67/5.24 $i(v1) | ~ $i(v0) | ~ net_str(v1, v0) | ~ one_sorted_str(v0) | % 32.67/5.24 function(v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 32.67/5.24 (the_mapping(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ net_str(v1, v0) | ~ % 32.67/5.24 one_sorted_str(v0) | ? [v3: $i] : ? [v4: $i] : (the_carrier(v1) = v3 & % 32.67/5.24 the_carrier(v0) = v4 & $i(v4) & $i(v3) & quasi_total(v2, v3, v4) & % 32.67/5.24 relation_of2_as_subset(v2, v3, v4))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 32.67/5.24 $i(v1) | ~ $i(v0) | ~ net_str(v1, v0) | ~ one_sorted_str(v0) | ? [v2: % 32.67/5.24 $i] : ? [v3: $i] : ? [v4: $i] : (the_mapping(v0, v1) = v2 & % 32.67/5.24 the_carrier(v1) = v3 & the_carrier(v0) = v4 & $i(v4) & $i(v3) & $i(v2) & % 32.67/5.24 quasi_total(v2, v3, v4) & relation_of2_as_subset(v2, v3, v4) & % 32.67/5.24 function(v2))) % 32.67/5.24 % 32.67/5.24 (existence_l1_orders_2) % 32.67/5.24 ? [v0: $i] : ($i(v0) & rel_str(v0)) % 32.67/5.24 % 32.67/5.24 (existence_l1_waybel_0) % 32.67/5.24 ! [v0: $i] : ( ~ $i(v0) | ~ one_sorted_str(v0) | ? [v1: $i] : ($i(v1) & % 32.67/5.24 net_str(v1, v0))) % 32.67/5.24 % 32.67/5.24 (existence_m1_yellow_0) % 32.67/5.24 ! [v0: $i] : ( ~ $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ($i(v1) & % 32.82/5.24 subrelstr(v1, v0))) % 32.82/5.24 % 32.82/5.24 (existence_m1_yellow_6) % 32.82/5.24 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ net_str(v1, v0) | ~ % 32.82/5.24 one_sorted_str(v0) | ? [v2: $i] : ($i(v2) & subnetstr(v2, v0, v1))) % 32.82/5.24 % 32.82/5.24 (t19_yellow_6) % 32.82/5.24 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 32.82/5.24 (the_carrier(v3) = v4 & the_carrier(v1) = v2 & $i(v4) & $i(v3) & $i(v2) & % 32.82/5.24 $i(v1) & $i(v0) & subnetstr(v3, v0, v1) & net_str(v1, v0) & % 32.82/5.24 one_sorted_str(v0) & ~ subset(v4, v2)) % 32.82/5.24 % 32.82/5.24 (function-axioms) % 32.82/5.24 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 32.82/5.24 $i] : (v1 = v0 | ~ (relation_dom_restr_as_relation_of(v5, v4, v3, v2) = v1) % 32.82/5.24 | ~ (relation_dom_restr_as_relation_of(v5, v4, v3, v2) = v0)) & ! [v0: $i] % 32.82/5.24 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 32.82/5.24 (relation_dom_restriction(v3, v2) = v1) | ~ (relation_dom_restriction(v3, % 32.82/5.24 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 32.82/5.24 = v0 | ~ (the_mapping(v3, v2) = v1) | ~ (the_mapping(v3, v2) = v0)) & ! % 32.82/5.24 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 32.82/5.24 (cartesian_product2(v3, v2) = v1) | ~ (cartesian_product2(v3, v2) = v0)) & % 32.82/5.24 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (the_carrier(v2) = v1) % 32.82/5.24 | ~ (the_carrier(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 % 32.82/5.24 = v0 | ~ (the_InternalRel(v2) = v1) | ~ (the_InternalRel(v2) = v0)) & ! % 32.82/5.24 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (powerset(v2) = v1) | ~ % 32.82/5.24 (powerset(v2) = v0)) % 32.82/5.24 % 32.82/5.24 Further assumptions not needed in the proof: % 32.82/5.24 -------------------------------------------- % 32.82/5.24 antisymmetry_r2_hidden, cc1_funct_1, cc1_relat_1, cc1_relset_1, cc2_funct_1, % 32.82/5.24 dt_k1_xboole_0, dt_k1_zfmisc_1, dt_k2_zfmisc_1, dt_k7_relat_1, dt_k8_relset_1, % 32.82/5.24 dt_l1_orders_2, dt_l1_struct_0, dt_m1_relset_1, dt_m1_subset_1, dt_m2_relset_1, % 32.82/5.24 dt_u1_struct_0, existence_l1_struct_0, existence_m1_relset_1, % 32.82/5.24 existence_m1_subset_1, existence_m2_relset_1, fc12_relat_1, fc13_relat_1, % 32.82/5.24 fc1_subset_1, fc4_funct_1, fc4_relat_1, fc4_subset_1, rc1_funct_1, rc1_pboole, % 32.82/5.24 rc1_relat_1, rc1_subset_1, rc2_funct_1, rc2_relat_1, rc2_subset_1, rc3_funct_1, % 32.82/5.24 rc3_relat_1, rc4_funct_1, redefinition_k8_relset_1, redefinition_m2_relset_1, % 32.82/5.24 reflexivity_r1_tarski, t1_subset, t2_subset, t3_subset, t4_subset, t5_subset, % 32.82/5.24 t6_boole, t7_boole, t8_boole % 32.82/5.24 % 32.82/5.24 Those formulas are unsatisfiable: % 32.82/5.24 --------------------------------- % 32.82/5.24 % 32.82/5.24 Begin of proof % 32.82/5.24 | % 32.82/5.24 | ALPHA: (d13_yellow_0) implies: % 32.82/5.24 | (1) ! [v0: $i] : ( ~ $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] : % 32.82/5.24 | (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) & $i(v1) & % 32.82/5.24 | ! [v3: $i] : ( ~ $i(v3) | ~ rel_str(v3) | ? [v4: $i] : ? [v5: % 32.82/5.24 | $i] : (the_carrier(v3) = v4 & the_InternalRel(v3) = v5 & $i(v5) % 32.82/5.24 | & $i(v4) & ( ~ subset(v5, v2) | ~ subset(v4, v1) | % 32.82/5.24 | subrelstr(v3, v0)) & ( ~ subrelstr(v3, v0) | (subset(v5, v2) % 32.82/5.24 | & subset(v4, v1))))))) % 32.82/5.24 | % 32.82/5.24 | ALPHA: (d8_yellow_6) implies: % 32.82/5.25 | (2) ! [v0: $i] : ( ~ $i(v0) | ~ one_sorted_str(v0) | ? [v1: $i] : % 32.82/5.25 | (the_carrier(v0) = v1 & $i(v1) & ! [v2: $i] : ( ~ $i(v2) | ~ % 32.82/5.25 | net_str(v2, v0) | ? [v3: $i] : ? [v4: $i] : (the_mapping(v0, % 32.82/5.25 | v2) = v4 & the_carrier(v2) = v3 & $i(v4) & $i(v3) & ! [v5: % 32.82/5.25 | $i] : ( ~ $i(v5) | ~ net_str(v5, v0) | ? [v6: $i] : ? [v7: % 32.82/5.25 | $i] : ? [v8: $i] : (the_mapping(v0, v5) = v6 & % 32.82/5.25 | relation_dom_restr_as_relation_of(v3, v1, v4, v7) = v8 & % 32.82/5.25 | the_carrier(v5) = v7 & $i(v8) & $i(v7) & $i(v6) & ( ~ (v8 = % 32.82/5.25 | v6) | ~ subrelstr(v5, v2) | subnetstr(v5, v0, v2)) & ( % 32.82/5.25 | ~ subnetstr(v5, v0, v2) | (v8 = v6 & subrelstr(v5, % 32.82/5.25 | v2))))))))) % 32.82/5.25 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 32.82/5.25 | (the_mapping(v0, v2) = v3) | ~ (the_carrier(v0) = v1) | ~ $i(v2) | % 32.82/5.25 | ~ $i(v0) | ~ net_str(v2, v0) | ~ one_sorted_str(v0) | ? [v4: $i] : % 32.82/5.25 | (the_carrier(v2) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ! [v7: % 32.82/5.25 | $i] : ( ~ (relation_dom_restr_as_relation_of(v4, v1, v3, v6) = % 32.82/5.25 | v7) | ~ (the_carrier(v5) = v6) | ~ $i(v5) | ~ net_str(v5, % 32.82/5.25 | v0) | ? [v8: $i] : (the_mapping(v0, v5) = v8 & $i(v8) & ( ~ % 32.82/5.25 | (v8 = v7) | ~ subrelstr(v5, v2) | subnetstr(v5, v0, v2)) & ( % 32.82/5.25 | ~ subnetstr(v5, v0, v2) | (v8 = v7 & subrelstr(v5, v2))))))) % 32.82/5.25 | % 32.82/5.25 | ALPHA: (dt_u1_orders_2) implies: % 32.82/5.25 | (4) ! [v0: $i] : ( ~ $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] : % 32.82/5.25 | (the_carrier(v0) = v2 & the_InternalRel(v0) = v1 & $i(v2) & $i(v1) & % 32.82/5.25 | relation_of2_as_subset(v1, v2, v2))) % 32.82/5.25 | % 32.82/5.25 | ALPHA: (dt_u1_waybel_0) implies: % 32.82/5.25 | (5) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ net_str(v1, v0) % 32.82/5.25 | | ~ one_sorted_str(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 32.82/5.25 | (the_mapping(v0, v1) = v2 & the_carrier(v1) = v3 & the_carrier(v0) = % 32.82/5.25 | v4 & $i(v4) & $i(v3) & $i(v2) & quasi_total(v2, v3, v4) & % 32.82/5.25 | relation_of2_as_subset(v2, v3, v4) & function(v2))) % 32.82/5.25 | % 32.82/5.25 | ALPHA: (function-axioms) implies: % 32.82/5.25 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 32.82/5.25 | (the_carrier(v2) = v1) | ~ (the_carrier(v2) = v0)) % 32.82/5.25 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 32.82/5.25 | (the_mapping(v3, v2) = v1) | ~ (the_mapping(v3, v2) = v0)) % 32.82/5.25 | % 32.82/5.25 | DELTA: instantiating (existence_l1_orders_2) with fresh symbol all_39_0 gives: % 32.82/5.25 | (8) $i(all_39_0) & rel_str(all_39_0) % 32.82/5.25 | % 32.82/5.25 | ALPHA: (8) implies: % 32.82/5.25 | (9) rel_str(all_39_0) % 32.82/5.25 | (10) $i(all_39_0) % 32.82/5.25 | % 32.82/5.25 | DELTA: instantiating (t19_yellow_6) with fresh symbols all_77_0, all_77_1, % 32.82/5.25 | all_77_2, all_77_3, all_77_4 gives: % 32.82/5.25 | (11) the_carrier(all_77_1) = all_77_0 & the_carrier(all_77_3) = all_77_2 & % 32.82/5.25 | $i(all_77_0) & $i(all_77_1) & $i(all_77_2) & $i(all_77_3) & % 32.82/5.25 | $i(all_77_4) & subnetstr(all_77_1, all_77_4, all_77_3) & % 32.82/5.25 | net_str(all_77_3, all_77_4) & one_sorted_str(all_77_4) & ~ % 32.82/5.25 | subset(all_77_0, all_77_2) % 32.82/5.25 | % 32.82/5.25 | ALPHA: (11) implies: % 32.82/5.25 | (12) ~ subset(all_77_0, all_77_2) % 32.82/5.25 | (13) one_sorted_str(all_77_4) % 32.82/5.25 | (14) net_str(all_77_3, all_77_4) % 32.82/5.25 | (15) subnetstr(all_77_1, all_77_4, all_77_3) % 32.82/5.25 | (16) $i(all_77_4) % 32.82/5.25 | (17) $i(all_77_3) % 32.82/5.25 | (18) $i(all_77_1) % 32.82/5.25 | (19) the_carrier(all_77_3) = all_77_2 % 32.82/5.25 | (20) the_carrier(all_77_1) = all_77_0 % 32.82/5.25 | % 32.82/5.25 | GROUND_INST: instantiating (1) with all_39_0, simplifying with (9), (10) % 32.82/5.25 | gives: % 32.82/5.26 | (21) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_39_0) = v0 & % 32.82/5.26 | the_InternalRel(all_39_0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ % 32.82/5.26 | $i(v2) | ~ rel_str(v2) | ? [v3: $i] : ? [v4: $i] : % 32.82/5.26 | (the_carrier(v2) = v3 & the_InternalRel(v2) = v4 & $i(v4) & $i(v3) % 32.82/5.26 | & ( ~ subset(v4, v1) | ~ subset(v3, v0) | subrelstr(v2, % 32.82/5.26 | all_39_0)) & ( ~ subrelstr(v2, all_39_0) | (subset(v4, v1) & % 32.82/5.26 | subset(v3, v0)))))) % 32.82/5.26 | % 32.82/5.26 | GROUND_INST: instantiating (existence_m1_yellow_0) with all_39_0, simplifying % 32.82/5.26 | with (9), (10) gives: % 32.82/5.26 | (22) ? [v0: $i] : ($i(v0) & subrelstr(v0, all_39_0)) % 32.82/5.26 | % 32.82/5.26 | GROUND_INST: instantiating (2) with all_77_4, simplifying with (13), (16) % 32.82/5.26 | gives: % 32.82/5.26 | (23) ? [v0: $i] : (the_carrier(all_77_4) = v0 & $i(v0) & ! [v1: $i] : ( ~ % 32.82/5.26 | $i(v1) | ~ net_str(v1, all_77_4) | ? [v2: $i] : ? [v3: $i] : % 32.82/5.26 | (the_mapping(all_77_4, v1) = v3 & the_carrier(v1) = v2 & $i(v3) & % 32.82/5.26 | $i(v2) & ! [v4: $i] : ( ~ $i(v4) | ~ net_str(v4, all_77_4) | % 32.82/5.26 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : % 32.82/5.26 | (the_mapping(all_77_4, v4) = v5 & % 32.82/5.26 | relation_dom_restr_as_relation_of(v2, v0, v3, v6) = v7 & % 32.82/5.26 | the_carrier(v4) = v6 & $i(v7) & $i(v6) & $i(v5) & ( ~ (v7 = % 32.82/5.26 | v5) | ~ subrelstr(v4, v1) | subnetstr(v4, all_77_4, % 32.82/5.26 | v1)) & ( ~ subnetstr(v4, all_77_4, v1) | (v7 = v5 & % 32.82/5.26 | subrelstr(v4, v1)))))))) % 32.82/5.26 | % 32.82/5.26 | GROUND_INST: instantiating (existence_l1_waybel_0) with all_77_4, simplifying % 32.82/5.26 | with (13), (16) gives: % 32.82/5.26 | (24) ? [v0: $i] : ($i(v0) & net_str(v0, all_77_4)) % 32.82/5.26 | % 32.82/5.26 | GROUND_INST: instantiating (dt_l1_waybel_0) with all_77_4, all_77_3, % 32.82/5.26 | simplifying with (13), (14), (16), (17) gives: % 32.82/5.26 | (25) rel_str(all_77_3) % 32.82/5.26 | % 32.82/5.26 | GROUND_INST: instantiating (5) with all_77_4, all_77_3, simplifying with (13), % 32.82/5.26 | (14), (16), (17) gives: % 32.82/5.26 | (26) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.26 | all_77_3) = v0 & the_carrier(all_77_3) = v1 & % 32.82/5.26 | the_carrier(all_77_4) = v2 & $i(v2) & $i(v1) & $i(v0) & % 32.82/5.26 | quasi_total(v0, v1, v2) & relation_of2_as_subset(v0, v1, v2) & % 32.82/5.26 | function(v0)) % 32.82/5.26 | % 32.82/5.26 | GROUND_INST: instantiating (existence_m1_yellow_6) with all_77_4, all_77_3, % 32.82/5.26 | simplifying with (13), (14), (16), (17) gives: % 32.82/5.26 | (27) ? [v0: $i] : ($i(v0) & subnetstr(v0, all_77_4, all_77_3)) % 32.82/5.26 | % 32.82/5.26 | GROUND_INST: instantiating (dt_m1_yellow_6) with all_77_4, all_77_3, all_77_1, % 32.82/5.26 | simplifying with (13), (14), (15), (16), (17), (18) gives: % 32.82/5.26 | (28) net_str(all_77_1, all_77_4) % 32.82/5.26 | % 32.82/5.26 | DELTA: instantiating (27) with fresh symbol all_85_0 gives: % 32.82/5.26 | (29) $i(all_85_0) & subnetstr(all_85_0, all_77_4, all_77_3) % 32.82/5.26 | % 32.82/5.26 | ALPHA: (29) implies: % 32.82/5.26 | (30) subnetstr(all_85_0, all_77_4, all_77_3) % 32.82/5.26 | (31) $i(all_85_0) % 32.82/5.26 | % 32.82/5.26 | DELTA: instantiating (24) with fresh symbol all_87_0 gives: % 32.82/5.26 | (32) $i(all_87_0) & net_str(all_87_0, all_77_4) % 32.82/5.26 | % 32.82/5.26 | ALPHA: (32) implies: % 32.82/5.26 | (33) net_str(all_87_0, all_77_4) % 32.82/5.26 | (34) $i(all_87_0) % 32.82/5.26 | % 32.82/5.26 | DELTA: instantiating (22) with fresh symbol all_91_0 gives: % 32.82/5.26 | (35) $i(all_91_0) & subrelstr(all_91_0, all_39_0) % 32.82/5.26 | % 32.82/5.26 | ALPHA: (35) implies: % 32.82/5.26 | (36) subrelstr(all_91_0, all_39_0) % 32.82/5.26 | (37) $i(all_91_0) % 32.82/5.26 | % 32.82/5.26 | DELTA: instantiating (26) with fresh symbols all_95_0, all_95_1, all_95_2 % 32.82/5.26 | gives: % 32.82/5.26 | (38) the_mapping(all_77_4, all_77_3) = all_95_2 & the_carrier(all_77_3) = % 32.82/5.26 | all_95_1 & the_carrier(all_77_4) = all_95_0 & $i(all_95_0) & % 32.82/5.26 | $i(all_95_1) & $i(all_95_2) & quasi_total(all_95_2, all_95_1, % 32.82/5.26 | all_95_0) & relation_of2_as_subset(all_95_2, all_95_1, all_95_0) & % 32.82/5.26 | function(all_95_2) % 32.82/5.26 | % 32.82/5.26 | ALPHA: (38) implies: % 32.82/5.26 | (39) the_carrier(all_77_4) = all_95_0 % 32.82/5.26 | (40) the_carrier(all_77_3) = all_95_1 % 32.82/5.26 | (41) the_mapping(all_77_4, all_77_3) = all_95_2 % 32.82/5.26 | % 32.82/5.26 | DELTA: instantiating (21) with fresh symbols all_97_0, all_97_1 gives: % 32.82/5.26 | (42) the_carrier(all_39_0) = all_97_1 & the_InternalRel(all_39_0) = % 32.82/5.26 | all_97_0 & $i(all_97_0) & $i(all_97_1) & ! [v0: $i] : ( ~ $i(v0) | ~ % 32.82/5.26 | rel_str(v0) | ? [v1: $i] : ? [v2: $i] : (the_carrier(v0) = v1 & % 32.82/5.26 | the_InternalRel(v0) = v2 & $i(v2) & $i(v1) & ( ~ subset(v2, % 32.82/5.26 | all_97_0) | ~ subset(v1, all_97_1) | subrelstr(v0, all_39_0)) % 32.82/5.26 | & ( ~ subrelstr(v0, all_39_0) | (subset(v2, all_97_0) & subset(v1, % 32.82/5.26 | all_97_1))))) % 32.82/5.26 | % 32.82/5.26 | ALPHA: (42) implies: % 32.82/5.27 | (43) ! [v0: $i] : ( ~ $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] % 32.82/5.27 | : (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) & $i(v1) % 32.82/5.27 | & ( ~ subset(v2, all_97_0) | ~ subset(v1, all_97_1) | % 32.82/5.27 | subrelstr(v0, all_39_0)) & ( ~ subrelstr(v0, all_39_0) | % 32.82/5.27 | (subset(v2, all_97_0) & subset(v1, all_97_1))))) % 32.82/5.27 | % 32.82/5.27 | DELTA: instantiating (23) with fresh symbol all_100_0 gives: % 32.82/5.27 | (44) the_carrier(all_77_4) = all_100_0 & $i(all_100_0) & ! [v0: $i] : ( ~ % 32.82/5.27 | $i(v0) | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? [v2: $i] : % 32.82/5.27 | (the_mapping(all_77_4, v0) = v2 & the_carrier(v0) = v1 & $i(v2) & % 32.82/5.27 | $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ net_str(v3, all_77_4) | ? % 32.82/5.27 | [v4: $i] : ? [v5: $i] : ? [v6: $i] : (the_mapping(all_77_4, % 32.82/5.27 | v3) = v4 & relation_dom_restr_as_relation_of(v1, all_100_0, % 32.82/5.27 | v2, v5) = v6 & the_carrier(v3) = v5 & $i(v6) & $i(v5) & % 32.82/5.27 | $i(v4) & ( ~ (v6 = v4) | ~ subrelstr(v3, v0) | subnetstr(v3, % 32.82/5.27 | all_77_4, v0)) & ( ~ subnetstr(v3, all_77_4, v0) | (v6 = % 32.82/5.27 | v4 & subrelstr(v3, v0))))))) % 32.82/5.27 | % 32.82/5.27 | ALPHA: (44) implies: % 32.82/5.27 | (45) the_carrier(all_77_4) = all_100_0 % 32.82/5.27 | (46) ! [v0: $i] : ( ~ $i(v0) | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? % 32.82/5.27 | [v2: $i] : (the_mapping(all_77_4, v0) = v2 & the_carrier(v0) = v1 & % 32.82/5.27 | $i(v2) & $i(v1) & ! [v3: $i] : ( ~ $i(v3) | ~ net_str(v3, % 32.82/5.27 | all_77_4) | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 32.82/5.27 | (the_mapping(all_77_4, v3) = v4 & % 32.82/5.27 | relation_dom_restr_as_relation_of(v1, all_100_0, v2, v5) = v6 % 32.82/5.27 | & the_carrier(v3) = v5 & $i(v6) & $i(v5) & $i(v4) & ( ~ (v6 = % 32.82/5.27 | v4) | ~ subrelstr(v3, v0) | subnetstr(v3, all_77_4, v0)) % 32.82/5.27 | & ( ~ subnetstr(v3, all_77_4, v0) | (v6 = v4 & subrelstr(v3, % 32.82/5.27 | v0))))))) % 32.82/5.27 | % 32.82/5.27 | GROUND_INST: instantiating (46) with all_77_3, simplifying with (14), (17) % 32.82/5.27 | gives: % 32.82/5.27 | (47) ? [v0: $i] : ? [v1: $i] : (the_mapping(all_77_4, all_77_3) = v1 & % 32.82/5.27 | the_carrier(all_77_3) = v0 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ % 32.82/5.27 | $i(v2) | ~ net_str(v2, all_77_4) | ? [v3: $i] : ? [v4: $i] : ? % 32.82/5.27 | [v5: $i] : (the_mapping(all_77_4, v2) = v3 & % 32.82/5.27 | relation_dom_restr_as_relation_of(v0, all_100_0, v1, v4) = v5 & % 32.82/5.27 | the_carrier(v2) = v4 & $i(v5) & $i(v4) & $i(v3) & ( ~ (v5 = v3) % 32.82/5.27 | | ~ subrelstr(v2, all_77_3) | subnetstr(v2, all_77_4, % 32.82/5.27 | all_77_3)) & ( ~ subnetstr(v2, all_77_4, all_77_3) | (v5 = % 32.82/5.27 | v3 & subrelstr(v2, all_77_3)))))) % 32.82/5.27 | % 32.82/5.27 | DELTA: instantiating (47) with fresh symbols all_108_0, all_108_1 gives: % 32.82/5.27 | (48) the_mapping(all_77_4, all_77_3) = all_108_0 & the_carrier(all_77_3) = % 32.82/5.27 | all_108_1 & $i(all_108_0) & $i(all_108_1) & ! [v0: $i] : ( ~ $i(v0) | % 32.82/5.27 | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 32.82/5.27 | (the_mapping(all_77_4, v0) = v1 & % 32.82/5.27 | relation_dom_restr_as_relation_of(all_108_1, all_100_0, all_108_0, % 32.82/5.27 | v2) = v3 & the_carrier(v0) = v2 & $i(v3) & $i(v2) & $i(v1) & ( ~ % 32.82/5.27 | (v3 = v1) | ~ subrelstr(v0, all_77_3) | subnetstr(v0, all_77_4, % 32.82/5.27 | all_77_3)) & ( ~ subnetstr(v0, all_77_4, all_77_3) | (v3 = v1 % 32.82/5.27 | & subrelstr(v0, all_77_3))))) % 32.82/5.27 | % 32.82/5.27 | ALPHA: (48) implies: % 32.82/5.27 | (49) the_carrier(all_77_3) = all_108_1 % 32.82/5.27 | (50) the_mapping(all_77_4, all_77_3) = all_108_0 % 32.82/5.27 | (51) ! [v0: $i] : ( ~ $i(v0) | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? % 32.82/5.27 | [v2: $i] : ? [v3: $i] : (the_mapping(all_77_4, v0) = v1 & % 32.82/5.27 | relation_dom_restr_as_relation_of(all_108_1, all_100_0, all_108_0, % 32.82/5.27 | v2) = v3 & the_carrier(v0) = v2 & $i(v3) & $i(v2) & $i(v1) & ( ~ % 32.82/5.27 | (v3 = v1) | ~ subrelstr(v0, all_77_3) | subnetstr(v0, all_77_4, % 32.82/5.27 | all_77_3)) & ( ~ subnetstr(v0, all_77_4, all_77_3) | (v3 = v1 % 32.82/5.27 | & subrelstr(v0, all_77_3))))) % 32.82/5.27 | % 32.82/5.27 | GROUND_INST: instantiating (51) with all_77_3, simplifying with (14), (17) % 32.82/5.27 | gives: % 32.82/5.27 | (52) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.27 | all_77_3) = v0 & relation_dom_restr_as_relation_of(all_108_1, % 32.82/5.27 | all_100_0, all_108_0, v1) = v2 & the_carrier(all_77_3) = v1 & % 32.82/5.27 | $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v0) | ~ subrelstr(all_77_3, % 32.82/5.27 | all_77_3) | subnetstr(all_77_3, all_77_4, all_77_3)) & ( ~ % 32.82/5.27 | subnetstr(all_77_3, all_77_4, all_77_3) | (v2 = v0 & % 32.82/5.27 | subrelstr(all_77_3, all_77_3)))) % 32.82/5.27 | % 32.82/5.27 | DELTA: instantiating (52) with fresh symbols all_111_0, all_111_1, all_111_2 % 32.82/5.27 | gives: % 32.82/5.28 | (53) the_mapping(all_77_4, all_77_3) = all_111_2 & % 32.82/5.28 | relation_dom_restr_as_relation_of(all_108_1, all_100_0, all_108_0, % 32.82/5.28 | all_111_1) = all_111_0 & the_carrier(all_77_3) = all_111_1 & % 32.82/5.28 | $i(all_111_0) & $i(all_111_1) & $i(all_111_2) & ( ~ (all_111_0 = % 32.82/5.28 | all_111_2) | ~ subrelstr(all_77_3, all_77_3) | % 32.82/5.28 | subnetstr(all_77_3, all_77_4, all_77_3)) & ( ~ subnetstr(all_77_3, % 32.82/5.28 | all_77_4, all_77_3) | (all_111_0 = all_111_2 & subrelstr(all_77_3, % 32.82/5.28 | all_77_3))) % 32.82/5.28 | % 32.82/5.28 | ALPHA: (53) implies: % 32.82/5.28 | (54) the_carrier(all_77_3) = all_111_1 % 32.82/5.28 | (55) the_mapping(all_77_4, all_77_3) = all_111_2 % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (6) with all_95_0, all_100_0, all_77_4, simplifying % 32.82/5.28 | with (39), (45) gives: % 32.82/5.28 | (56) all_100_0 = all_95_0 % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (6) with all_77_2, all_108_1, all_77_3, simplifying % 32.82/5.28 | with (19), (49) gives: % 32.82/5.28 | (57) all_108_1 = all_77_2 % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (6) with all_108_1, all_111_1, all_77_3, % 32.82/5.28 | simplifying with (49), (54) gives: % 32.82/5.28 | (58) all_111_1 = all_108_1 % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (6) with all_95_1, all_111_1, all_77_3, simplifying % 32.82/5.28 | with (40), (54) gives: % 32.82/5.28 | (59) all_111_1 = all_95_1 % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (7) with all_108_0, all_111_2, all_77_3, all_77_4, % 32.82/5.28 | simplifying with (50), (55) gives: % 32.82/5.28 | (60) all_111_2 = all_108_0 % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (7) with all_95_2, all_111_2, all_77_3, all_77_4, % 32.82/5.28 | simplifying with (41), (55) gives: % 32.82/5.28 | (61) all_111_2 = all_95_2 % 32.82/5.28 | % 32.82/5.28 | COMBINE_EQS: (58), (59) imply: % 32.82/5.28 | (62) all_108_1 = all_95_1 % 32.82/5.28 | % 32.82/5.28 | SIMP: (62) implies: % 32.82/5.28 | (63) all_108_1 = all_95_1 % 32.82/5.28 | % 32.82/5.28 | COMBINE_EQS: (60), (61) imply: % 32.82/5.28 | (64) all_108_0 = all_95_2 % 32.82/5.28 | % 32.82/5.28 | COMBINE_EQS: (57), (63) imply: % 32.82/5.28 | (65) all_95_1 = all_77_2 % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (4) with all_77_3, simplifying with (17), (25) % 32.82/5.28 | gives: % 32.82/5.28 | (66) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_3) = v1 & % 32.82/5.28 | the_InternalRel(all_77_3) = v0 & $i(v1) & $i(v0) & % 32.82/5.28 | relation_of2_as_subset(v0, v1, v1)) % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (1) with all_77_3, simplifying with (17), (25) % 32.82/5.28 | gives: % 32.82/5.28 | (67) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_3) = v0 & % 32.82/5.28 | the_InternalRel(all_77_3) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ % 32.82/5.28 | $i(v2) | ~ rel_str(v2) | ? [v3: $i] : ? [v4: $i] : % 32.82/5.28 | (the_carrier(v2) = v3 & the_InternalRel(v2) = v4 & $i(v4) & $i(v3) % 32.82/5.28 | & ( ~ subset(v4, v1) | ~ subset(v3, v0) | subrelstr(v2, % 32.82/5.28 | all_77_3)) & ( ~ subrelstr(v2, all_77_3) | (subset(v4, v1) & % 32.82/5.28 | subset(v3, v0)))))) % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (43) with all_77_3, simplifying with (17), (25) % 32.82/5.28 | gives: % 32.82/5.28 | (68) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_3) = v0 & % 32.82/5.28 | the_InternalRel(all_77_3) = v1 & $i(v1) & $i(v0) & ( ~ subset(v1, % 32.82/5.28 | all_97_0) | ~ subset(v0, all_97_1) | subrelstr(all_77_3, % 32.82/5.28 | all_39_0)) & ( ~ subrelstr(all_77_3, all_39_0) | (subset(v1, % 32.82/5.28 | all_97_0) & subset(v0, all_97_1)))) % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (dt_m1_yellow_0) with all_39_0, all_91_0, % 32.82/5.28 | simplifying with (9), (10), (36), (37) gives: % 32.82/5.28 | (69) rel_str(all_91_0) % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (dt_l1_waybel_0) with all_77_4, all_77_1, % 32.82/5.28 | simplifying with (13), (16), (18), (28) gives: % 32.82/5.28 | (70) rel_str(all_77_1) % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (5) with all_77_4, all_77_1, simplifying with (13), % 32.82/5.28 | (16), (18), (28) gives: % 32.82/5.28 | (71) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.28 | all_77_1) = v0 & the_carrier(all_77_1) = v1 & % 32.82/5.28 | the_carrier(all_77_4) = v2 & $i(v2) & $i(v1) & $i(v0) & % 32.82/5.28 | quasi_total(v0, v1, v2) & relation_of2_as_subset(v0, v1, v2) & % 32.82/5.28 | function(v0)) % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (51) with all_77_1, simplifying with (18), (28) % 32.82/5.28 | gives: % 32.82/5.28 | (72) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.28 | all_77_1) = v0 & relation_dom_restr_as_relation_of(all_108_1, % 32.82/5.28 | all_100_0, all_108_0, v1) = v2 & the_carrier(all_77_1) = v1 & % 32.82/5.28 | $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v0) | ~ subrelstr(all_77_1, % 32.82/5.28 | all_77_3) | subnetstr(all_77_1, all_77_4, all_77_3)) & ( ~ % 32.82/5.28 | subnetstr(all_77_1, all_77_4, all_77_3) | (v2 = v0 & % 32.82/5.28 | subrelstr(all_77_1, all_77_3)))) % 32.82/5.28 | % 32.82/5.28 | GROUND_INST: instantiating (46) with all_77_1, simplifying with (18), (28) % 32.82/5.28 | gives: % 32.82/5.29 | (73) ? [v0: $i] : ? [v1: $i] : (the_mapping(all_77_4, all_77_1) = v1 & % 32.82/5.29 | the_carrier(all_77_1) = v0 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ % 32.82/5.29 | $i(v2) | ~ net_str(v2, all_77_4) | ? [v3: $i] : ? [v4: $i] : ? % 32.82/5.29 | [v5: $i] : (the_mapping(all_77_4, v2) = v3 & % 32.82/5.29 | relation_dom_restr_as_relation_of(v0, all_100_0, v1, v4) = v5 & % 32.82/5.29 | the_carrier(v2) = v4 & $i(v5) & $i(v4) & $i(v3) & ( ~ (v5 = v3) % 32.82/5.29 | | ~ subrelstr(v2, all_77_1) | subnetstr(v2, all_77_4, % 32.82/5.29 | all_77_1)) & ( ~ subnetstr(v2, all_77_4, all_77_1) | (v5 = % 32.82/5.29 | v3 & subrelstr(v2, all_77_1)))))) % 32.82/5.29 | % 32.82/5.29 | GROUND_INST: instantiating (dt_l1_waybel_0) with all_77_4, all_87_0, % 32.82/5.29 | simplifying with (13), (16), (33), (34) gives: % 32.82/5.29 | (74) rel_str(all_87_0) % 32.82/5.29 | % 32.82/5.29 | GROUND_INST: instantiating (46) with all_87_0, simplifying with (33), (34) % 32.82/5.29 | gives: % 32.82/5.29 | (75) ? [v0: $i] : ? [v1: $i] : (the_mapping(all_77_4, all_87_0) = v1 & % 32.82/5.29 | the_carrier(all_87_0) = v0 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ % 32.82/5.29 | $i(v2) | ~ net_str(v2, all_77_4) | ? [v3: $i] : ? [v4: $i] : ? % 32.82/5.29 | [v5: $i] : (the_mapping(all_77_4, v2) = v3 & % 32.82/5.29 | relation_dom_restr_as_relation_of(v0, all_100_0, v1, v4) = v5 & % 32.82/5.29 | the_carrier(v2) = v4 & $i(v5) & $i(v4) & $i(v3) & ( ~ (v5 = v3) % 32.82/5.29 | | ~ subrelstr(v2, all_87_0) | subnetstr(v2, all_77_4, % 32.82/5.29 | all_87_0)) & ( ~ subnetstr(v2, all_77_4, all_87_0) | (v5 = % 32.82/5.29 | v3 & subrelstr(v2, all_87_0)))))) % 32.82/5.29 | % 32.82/5.29 | GROUND_INST: instantiating (dt_m1_yellow_6) with all_77_4, all_77_3, all_85_0, % 32.82/5.29 | simplifying with (13), (14), (16), (17), (30), (31) gives: % 32.82/5.29 | (76) net_str(all_85_0, all_77_4) % 32.82/5.29 | % 32.82/5.29 | GROUND_INST: instantiating (3) with all_77_4, all_95_0, all_77_3, all_95_2, % 32.82/5.29 | simplifying with (13), (14), (16), (17), (39), (41) gives: % 32.82/5.29 | (77) ? [v0: $i] : (the_carrier(all_77_3) = v0 & $i(v0) & ! [v1: $i] : ! % 32.82/5.29 | [v2: $i] : ! [v3: $i] : ( ~ (relation_dom_restr_as_relation_of(v0, % 32.82/5.29 | all_95_0, all_95_2, v2) = v3) | ~ (the_carrier(v1) = v2) | ~ % 32.82/5.29 | $i(v1) | ~ net_str(v1, all_77_4) | ? [v4: $i] : % 32.82/5.29 | (the_mapping(all_77_4, v1) = v4 & $i(v4) & ( ~ (v4 = v3) | ~ % 32.82/5.29 | subrelstr(v1, all_77_3) | subnetstr(v1, all_77_4, all_77_3)) & % 32.82/5.29 | ( ~ subnetstr(v1, all_77_4, all_77_3) | (v4 = v3 & subrelstr(v1, % 32.82/5.29 | all_77_3)))))) % 32.82/5.29 | % 32.82/5.29 | DELTA: instantiating (66) with fresh symbols all_137_0, all_137_1 gives: % 32.82/5.29 | (78) the_carrier(all_77_3) = all_137_0 & the_InternalRel(all_77_3) = % 32.82/5.29 | all_137_1 & $i(all_137_0) & $i(all_137_1) & % 32.82/5.29 | relation_of2_as_subset(all_137_1, all_137_0, all_137_0) % 32.82/5.29 | % 32.82/5.29 | ALPHA: (78) implies: % 32.82/5.29 | (79) the_carrier(all_77_3) = all_137_0 % 32.82/5.29 | % 32.82/5.29 | DELTA: instantiating (71) with fresh symbols all_139_0, all_139_1, all_139_2 % 32.82/5.29 | gives: % 32.82/5.29 | (80) the_mapping(all_77_4, all_77_1) = all_139_2 & the_carrier(all_77_1) = % 32.82/5.29 | all_139_1 & the_carrier(all_77_4) = all_139_0 & $i(all_139_0) & % 32.82/5.29 | $i(all_139_1) & $i(all_139_2) & quasi_total(all_139_2, all_139_1, % 32.82/5.29 | all_139_0) & relation_of2_as_subset(all_139_2, all_139_1, all_139_0) % 32.82/5.29 | & function(all_139_2) % 32.82/5.29 | % 32.82/5.29 | ALPHA: (80) implies: % 32.82/5.29 | (81) the_carrier(all_77_1) = all_139_1 % 32.82/5.29 | % 32.82/5.29 | DELTA: instantiating (68) with fresh symbols all_145_0, all_145_1 gives: % 32.82/5.29 | (82) the_carrier(all_77_3) = all_145_1 & the_InternalRel(all_77_3) = % 32.82/5.29 | all_145_0 & $i(all_145_0) & $i(all_145_1) & ( ~ subset(all_145_0, % 32.82/5.29 | all_97_0) | ~ subset(all_145_1, all_97_1) | subrelstr(all_77_3, % 32.82/5.29 | all_39_0)) & ( ~ subrelstr(all_77_3, all_39_0) | % 32.82/5.29 | (subset(all_145_0, all_97_0) & subset(all_145_1, all_97_1))) % 32.82/5.29 | % 32.82/5.29 | ALPHA: (82) implies: % 32.82/5.29 | (83) the_carrier(all_77_3) = all_145_1 % 32.82/5.29 | % 32.82/5.29 | DELTA: instantiating (72) with fresh symbols all_147_0, all_147_1, all_147_2 % 32.82/5.29 | gives: % 32.82/5.29 | (84) the_mapping(all_77_4, all_77_1) = all_147_2 & % 32.82/5.29 | relation_dom_restr_as_relation_of(all_108_1, all_100_0, all_108_0, % 32.82/5.29 | all_147_1) = all_147_0 & the_carrier(all_77_1) = all_147_1 & % 32.82/5.29 | $i(all_147_0) & $i(all_147_1) & $i(all_147_2) & ( ~ (all_147_0 = % 32.82/5.29 | all_147_2) | ~ subrelstr(all_77_1, all_77_3) | % 32.82/5.29 | subnetstr(all_77_1, all_77_4, all_77_3)) & ( ~ subnetstr(all_77_1, % 32.82/5.29 | all_77_4, all_77_3) | (all_147_0 = all_147_2 & subrelstr(all_77_1, % 32.82/5.29 | all_77_3))) % 32.82/5.29 | % 32.82/5.29 | ALPHA: (84) implies: % 32.82/5.29 | (85) the_carrier(all_77_1) = all_147_1 % 32.82/5.29 | (86) ~ subnetstr(all_77_1, all_77_4, all_77_3) | (all_147_0 = all_147_2 & % 32.82/5.29 | subrelstr(all_77_1, all_77_3)) % 32.82/5.29 | % 32.82/5.29 | DELTA: instantiating (77) with fresh symbol all_154_0 gives: % 32.82/5.29 | (87) the_carrier(all_77_3) = all_154_0 & $i(all_154_0) & ! [v0: $i] : ! % 32.82/5.29 | [v1: $i] : ! [v2: $i] : ( ~ % 32.82/5.29 | (relation_dom_restr_as_relation_of(all_154_0, all_95_0, all_95_2, % 32.82/5.29 | v1) = v2) | ~ (the_carrier(v0) = v1) | ~ $i(v0) | ~ % 32.82/5.29 | net_str(v0, all_77_4) | ? [v3: $i] : (the_mapping(all_77_4, v0) = % 32.82/5.29 | v3 & $i(v3) & ( ~ (v3 = v2) | ~ subrelstr(v0, all_77_3) | % 32.82/5.29 | subnetstr(v0, all_77_4, all_77_3)) & ( ~ subnetstr(v0, all_77_4, % 32.82/5.29 | all_77_3) | (v3 = v2 & subrelstr(v0, all_77_3))))) % 32.82/5.29 | % 32.82/5.29 | ALPHA: (87) implies: % 32.82/5.29 | (88) the_carrier(all_77_3) = all_154_0 % 32.82/5.29 | % 32.82/5.29 | DELTA: instantiating (67) with fresh symbols all_157_0, all_157_1 gives: % 32.82/5.29 | (89) the_carrier(all_77_3) = all_157_1 & the_InternalRel(all_77_3) = % 32.82/5.29 | all_157_0 & $i(all_157_0) & $i(all_157_1) & ! [v0: $i] : ( ~ $i(v0) | % 32.82/5.29 | ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] : (the_carrier(v0) = v1 & % 32.82/5.29 | the_InternalRel(v0) = v2 & $i(v2) & $i(v1) & ( ~ subset(v2, % 32.82/5.29 | all_157_0) | ~ subset(v1, all_157_1) | subrelstr(v0, % 32.82/5.29 | all_77_3)) & ( ~ subrelstr(v0, all_77_3) | (subset(v2, % 32.82/5.29 | all_157_0) & subset(v1, all_157_1))))) % 32.82/5.29 | % 32.82/5.29 | ALPHA: (89) implies: % 32.82/5.29 | (90) the_carrier(all_77_3) = all_157_1 % 32.82/5.29 | (91) ! [v0: $i] : ( ~ $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] % 32.82/5.29 | : (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) & $i(v1) % 32.82/5.29 | & ( ~ subset(v2, all_157_0) | ~ subset(v1, all_157_1) | % 32.82/5.29 | subrelstr(v0, all_77_3)) & ( ~ subrelstr(v0, all_77_3) | % 32.82/5.29 | (subset(v2, all_157_0) & subset(v1, all_157_1))))) % 32.82/5.29 | % 32.82/5.29 | GROUND_INST: instantiating (91) with all_77_3, simplifying with (17), (25) % 32.82/5.29 | gives: % 32.82/5.29 | (92) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_3) = v0 & % 32.82/5.29 | the_InternalRel(all_77_3) = v1 & $i(v1) & $i(v0) & ( ~ subset(v1, % 32.82/5.29 | all_157_0) | ~ subset(v0, all_157_1) | subrelstr(all_77_3, % 32.82/5.29 | all_77_3)) & ( ~ subrelstr(all_77_3, all_77_3) | (subset(v1, % 32.82/5.29 | all_157_0) & subset(v0, all_157_1)))) % 32.82/5.29 | % 32.82/5.29 | DELTA: instantiating (75) with fresh symbols all_160_0, all_160_1 gives: % 32.82/5.30 | (93) the_mapping(all_77_4, all_87_0) = all_160_0 & the_carrier(all_87_0) = % 32.82/5.30 | all_160_1 & $i(all_160_0) & $i(all_160_1) & ! [v0: $i] : ( ~ $i(v0) | % 32.82/5.30 | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 32.82/5.30 | (the_mapping(all_77_4, v0) = v1 & % 32.82/5.30 | relation_dom_restr_as_relation_of(all_160_1, all_100_0, all_160_0, % 32.82/5.30 | v2) = v3 & the_carrier(v0) = v2 & $i(v3) & $i(v2) & $i(v1) & ( ~ % 32.82/5.30 | (v3 = v1) | ~ subrelstr(v0, all_87_0) | subnetstr(v0, all_77_4, % 32.82/5.30 | all_87_0)) & ( ~ subnetstr(v0, all_77_4, all_87_0) | (v3 = v1 % 32.82/5.30 | & subrelstr(v0, all_87_0))))) % 32.82/5.30 | % 32.82/5.30 | ALPHA: (93) implies: % 32.82/5.30 | (94) ! [v0: $i] : ( ~ $i(v0) | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? % 32.82/5.30 | [v2: $i] : ? [v3: $i] : (the_mapping(all_77_4, v0) = v1 & % 32.82/5.30 | relation_dom_restr_as_relation_of(all_160_1, all_100_0, all_160_0, % 32.82/5.30 | v2) = v3 & the_carrier(v0) = v2 & $i(v3) & $i(v2) & $i(v1) & ( ~ % 32.82/5.30 | (v3 = v1) | ~ subrelstr(v0, all_87_0) | subnetstr(v0, all_77_4, % 32.82/5.30 | all_87_0)) & ( ~ subnetstr(v0, all_77_4, all_87_0) | (v3 = v1 % 32.82/5.30 | & subrelstr(v0, all_87_0))))) % 32.82/5.30 | % 32.82/5.30 | GROUND_INST: instantiating (94) with all_77_3, simplifying with (14), (17) % 32.82/5.30 | gives: % 32.82/5.30 | (95) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.30 | all_77_3) = v0 & relation_dom_restr_as_relation_of(all_160_1, % 32.82/5.30 | all_100_0, all_160_0, v1) = v2 & the_carrier(all_77_3) = v1 & % 32.82/5.30 | $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v0) | ~ subrelstr(all_77_3, % 32.82/5.30 | all_87_0) | subnetstr(all_77_3, all_77_4, all_87_0)) & ( ~ % 32.82/5.30 | subnetstr(all_77_3, all_77_4, all_87_0) | (v2 = v0 & % 32.82/5.30 | subrelstr(all_77_3, all_87_0)))) % 32.82/5.30 | % 32.82/5.30 | GROUND_INST: instantiating (94) with all_77_1, simplifying with (18), (28) % 32.82/5.30 | gives: % 32.82/5.30 | (96) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.30 | all_77_1) = v0 & relation_dom_restr_as_relation_of(all_160_1, % 32.82/5.30 | all_100_0, all_160_0, v1) = v2 & the_carrier(all_77_1) = v1 & % 32.82/5.30 | $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v0) | ~ subrelstr(all_77_1, % 32.82/5.30 | all_87_0) | subnetstr(all_77_1, all_77_4, all_87_0)) & ( ~ % 32.82/5.30 | subnetstr(all_77_1, all_77_4, all_87_0) | (v2 = v0 & % 32.82/5.30 | subrelstr(all_77_1, all_87_0)))) % 32.82/5.30 | % 32.82/5.30 | DELTA: instantiating (73) with fresh symbols all_166_0, all_166_1 gives: % 32.82/5.30 | (97) the_mapping(all_77_4, all_77_1) = all_166_0 & the_carrier(all_77_1) = % 32.82/5.30 | all_166_1 & $i(all_166_0) & $i(all_166_1) & ! [v0: $i] : ( ~ $i(v0) | % 32.82/5.30 | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 32.82/5.30 | (the_mapping(all_77_4, v0) = v1 & % 32.82/5.30 | relation_dom_restr_as_relation_of(all_166_1, all_100_0, all_166_0, % 32.82/5.30 | v2) = v3 & the_carrier(v0) = v2 & $i(v3) & $i(v2) & $i(v1) & ( ~ % 32.82/5.30 | (v3 = v1) | ~ subrelstr(v0, all_77_1) | subnetstr(v0, all_77_4, % 32.82/5.30 | all_77_1)) & ( ~ subnetstr(v0, all_77_4, all_77_1) | (v3 = v1 % 32.82/5.30 | & subrelstr(v0, all_77_1))))) % 32.82/5.30 | % 32.82/5.30 | ALPHA: (97) implies: % 32.82/5.30 | (98) the_carrier(all_77_1) = all_166_1 % 32.82/5.30 | (99) ! [v0: $i] : ( ~ $i(v0) | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? % 32.82/5.30 | [v2: $i] : ? [v3: $i] : (the_mapping(all_77_4, v0) = v1 & % 32.82/5.30 | relation_dom_restr_as_relation_of(all_166_1, all_100_0, all_166_0, % 32.82/5.30 | v2) = v3 & the_carrier(v0) = v2 & $i(v3) & $i(v2) & $i(v1) & ( ~ % 32.82/5.30 | (v3 = v1) | ~ subrelstr(v0, all_77_1) | subnetstr(v0, all_77_4, % 32.82/5.30 | all_77_1)) & ( ~ subnetstr(v0, all_77_4, all_77_1) | (v3 = v1 % 32.82/5.30 | & subrelstr(v0, all_77_1))))) % 32.82/5.30 | % 32.82/5.30 | GROUND_INST: instantiating (99) with all_77_3, simplifying with (14), (17) % 32.82/5.30 | gives: % 32.82/5.30 | (100) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.30 | all_77_3) = v0 & relation_dom_restr_as_relation_of(all_166_1, % 32.82/5.30 | all_100_0, all_166_0, v1) = v2 & the_carrier(all_77_3) = v1 & % 32.82/5.30 | $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v0) | ~ subrelstr(all_77_3, % 32.82/5.30 | all_77_1) | subnetstr(all_77_3, all_77_4, all_77_1)) & ( ~ % 32.82/5.30 | subnetstr(all_77_3, all_77_4, all_77_1) | (v2 = v0 & % 32.82/5.30 | subrelstr(all_77_3, all_77_1)))) % 32.82/5.30 | % 32.82/5.30 | GROUND_INST: instantiating (99) with all_77_1, simplifying with (18), (28) % 32.82/5.30 | gives: % 32.82/5.30 | (101) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.30 | all_77_1) = v0 & relation_dom_restr_as_relation_of(all_166_1, % 32.82/5.30 | all_100_0, all_166_0, v1) = v2 & the_carrier(all_77_1) = v1 & % 32.82/5.30 | $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v0) | ~ subrelstr(all_77_1, % 32.82/5.30 | all_77_1) | subnetstr(all_77_1, all_77_4, all_77_1)) & ( ~ % 32.82/5.30 | subnetstr(all_77_1, all_77_4, all_77_1) | (v2 = v0 & % 32.82/5.30 | subrelstr(all_77_1, all_77_1)))) % 32.82/5.30 | % 32.82/5.30 | DELTA: instantiating (92) with fresh symbols all_174_0, all_174_1 gives: % 32.82/5.30 | (102) the_carrier(all_77_3) = all_174_1 & the_InternalRel(all_77_3) = % 32.82/5.30 | all_174_0 & $i(all_174_0) & $i(all_174_1) & ( ~ subset(all_174_0, % 32.82/5.30 | all_157_0) | ~ subset(all_174_1, all_157_1) | % 32.82/5.30 | subrelstr(all_77_3, all_77_3)) & ( ~ subrelstr(all_77_3, all_77_3) % 32.82/5.30 | | (subset(all_174_0, all_157_0) & subset(all_174_1, all_157_1))) % 32.82/5.30 | % 32.82/5.30 | ALPHA: (102) implies: % 32.82/5.30 | (103) the_carrier(all_77_3) = all_174_1 % 32.82/5.30 | % 32.82/5.30 | DELTA: instantiating (96) with fresh symbols all_180_0, all_180_1, all_180_2 % 32.82/5.30 | gives: % 32.82/5.30 | (104) the_mapping(all_77_4, all_77_1) = all_180_2 & % 32.82/5.30 | relation_dom_restr_as_relation_of(all_160_1, all_100_0, all_160_0, % 32.82/5.30 | all_180_1) = all_180_0 & the_carrier(all_77_1) = all_180_1 & % 32.82/5.30 | $i(all_180_0) & $i(all_180_1) & $i(all_180_2) & ( ~ (all_180_0 = % 32.82/5.30 | all_180_2) | ~ subrelstr(all_77_1, all_87_0) | % 32.82/5.30 | subnetstr(all_77_1, all_77_4, all_87_0)) & ( ~ subnetstr(all_77_1, % 32.82/5.30 | all_77_4, all_87_0) | (all_180_0 = all_180_2 & % 32.82/5.30 | subrelstr(all_77_1, all_87_0))) % 32.82/5.30 | % 32.82/5.30 | ALPHA: (104) implies: % 32.82/5.30 | (105) the_carrier(all_77_1) = all_180_1 % 32.82/5.30 | % 32.82/5.30 | DELTA: instantiating (95) with fresh symbols all_182_0, all_182_1, all_182_2 % 32.82/5.30 | gives: % 32.82/5.30 | (106) the_mapping(all_77_4, all_77_3) = all_182_2 & % 32.82/5.30 | relation_dom_restr_as_relation_of(all_160_1, all_100_0, all_160_0, % 32.82/5.30 | all_182_1) = all_182_0 & the_carrier(all_77_3) = all_182_1 & % 32.82/5.30 | $i(all_182_0) & $i(all_182_1) & $i(all_182_2) & ( ~ (all_182_0 = % 32.82/5.30 | all_182_2) | ~ subrelstr(all_77_3, all_87_0) | % 32.82/5.30 | subnetstr(all_77_3, all_77_4, all_87_0)) & ( ~ subnetstr(all_77_3, % 32.82/5.30 | all_77_4, all_87_0) | (all_182_0 = all_182_2 & % 32.82/5.30 | subrelstr(all_77_3, all_87_0))) % 32.82/5.30 | % 32.82/5.30 | ALPHA: (106) implies: % 32.82/5.30 | (107) the_carrier(all_77_3) = all_182_1 % 32.82/5.30 | % 32.82/5.30 | DELTA: instantiating (101) with fresh symbols all_188_0, all_188_1, all_188_2 % 32.82/5.30 | gives: % 32.82/5.30 | (108) the_mapping(all_77_4, all_77_1) = all_188_2 & % 32.82/5.30 | relation_dom_restr_as_relation_of(all_166_1, all_100_0, all_166_0, % 32.82/5.30 | all_188_1) = all_188_0 & the_carrier(all_77_1) = all_188_1 & % 32.82/5.30 | $i(all_188_0) & $i(all_188_1) & $i(all_188_2) & ( ~ (all_188_0 = % 32.82/5.30 | all_188_2) | ~ subrelstr(all_77_1, all_77_1) | % 32.82/5.30 | subnetstr(all_77_1, all_77_4, all_77_1)) & ( ~ subnetstr(all_77_1, % 32.82/5.30 | all_77_4, all_77_1) | (all_188_0 = all_188_2 & % 32.82/5.30 | subrelstr(all_77_1, all_77_1))) % 32.82/5.30 | % 32.82/5.30 | ALPHA: (108) implies: % 32.82/5.30 | (109) the_carrier(all_77_1) = all_188_1 % 32.82/5.30 | % 32.82/5.30 | DELTA: instantiating (100) with fresh symbols all_190_0, all_190_1, all_190_2 % 32.82/5.30 | gives: % 32.82/5.30 | (110) the_mapping(all_77_4, all_77_3) = all_190_2 & % 32.82/5.30 | relation_dom_restr_as_relation_of(all_166_1, all_100_0, all_166_0, % 32.82/5.30 | all_190_1) = all_190_0 & the_carrier(all_77_3) = all_190_1 & % 32.82/5.30 | $i(all_190_0) & $i(all_190_1) & $i(all_190_2) & ( ~ (all_190_0 = % 32.82/5.30 | all_190_2) | ~ subrelstr(all_77_3, all_77_1) | % 32.82/5.30 | subnetstr(all_77_3, all_77_4, all_77_1)) & ( ~ subnetstr(all_77_3, % 32.82/5.30 | all_77_4, all_77_1) | (all_190_0 = all_190_2 & % 32.82/5.30 | subrelstr(all_77_3, all_77_1))) % 32.82/5.30 | % 32.82/5.30 | ALPHA: (110) implies: % 32.82/5.30 | (111) the_carrier(all_77_3) = all_190_1 % 32.82/5.30 | % 32.82/5.30 | BETA: splitting (86) gives: % 32.82/5.30 | % 32.82/5.30 | Case 1: % 32.82/5.30 | | % 32.82/5.30 | | (112) ~ subnetstr(all_77_1, all_77_4, all_77_3) % 32.82/5.30 | | % 32.82/5.30 | | PRED_UNIFY: (15), (112) imply: % 32.82/5.30 | | (113) $false % 32.82/5.30 | | % 32.82/5.30 | | CLOSE: (113) is inconsistent. % 32.82/5.30 | | % 32.82/5.30 | Case 2: % 32.82/5.30 | | % 32.82/5.30 | | (114) all_147_0 = all_147_2 & subrelstr(all_77_1, all_77_3) % 32.82/5.31 | | % 32.82/5.31 | | ALPHA: (114) implies: % 32.82/5.31 | | (115) subrelstr(all_77_1, all_77_3) % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_77_2, all_157_1, all_77_3, % 32.82/5.31 | | simplifying with (19), (90) gives: % 32.82/5.31 | | (116) all_157_1 = all_77_2 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_154_0, all_157_1, all_77_3, % 32.82/5.31 | | simplifying with (88), (90) gives: % 32.82/5.31 | | (117) all_157_1 = all_154_0 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_157_1, all_174_1, all_77_3, % 32.82/5.31 | | simplifying with (90), (103) gives: % 32.82/5.31 | | (118) all_174_1 = all_157_1 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_154_0, all_182_1, all_77_3, % 32.82/5.31 | | simplifying with (88), (107) gives: % 32.82/5.31 | | (119) all_182_1 = all_154_0 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_137_0, all_182_1, all_77_3, % 32.82/5.31 | | simplifying with (79), (107) gives: % 32.82/5.31 | | (120) all_182_1 = all_137_0 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_174_1, all_190_1, all_77_3, % 32.82/5.31 | | simplifying with (103), (111) gives: % 32.82/5.31 | | (121) all_190_1 = all_174_1 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_145_1, all_190_1, all_77_3, % 32.82/5.31 | | simplifying with (83), (111) gives: % 32.82/5.31 | | (122) all_190_1 = all_145_1 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_77_0, all_166_1, all_77_1, % 32.82/5.31 | | simplifying with (20), (98) gives: % 32.82/5.31 | | (123) all_166_1 = all_77_0 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_166_1, all_180_1, all_77_1, % 32.82/5.31 | | simplifying with (98), (105) gives: % 32.82/5.31 | | (124) all_180_1 = all_166_1 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_139_1, all_180_1, all_77_1, % 32.82/5.31 | | simplifying with (81), (105) gives: % 32.82/5.31 | | (125) all_180_1 = all_139_1 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_166_1, all_188_1, all_77_1, % 32.82/5.31 | | simplifying with (98), (109) gives: % 32.82/5.31 | | (126) all_188_1 = all_166_1 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (6) with all_147_1, all_188_1, all_77_1, % 32.82/5.31 | | simplifying with (85), (109) gives: % 32.82/5.31 | | (127) all_188_1 = all_147_1 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (121), (122) imply: % 32.82/5.31 | | (128) all_174_1 = all_145_1 % 32.82/5.31 | | % 32.82/5.31 | | SIMP: (128) implies: % 32.82/5.31 | | (129) all_174_1 = all_145_1 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (126), (127) imply: % 32.82/5.31 | | (130) all_166_1 = all_147_1 % 32.82/5.31 | | % 32.82/5.31 | | SIMP: (130) implies: % 32.82/5.31 | | (131) all_166_1 = all_147_1 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (119), (120) imply: % 32.82/5.31 | | (132) all_154_0 = all_137_0 % 32.82/5.31 | | % 32.82/5.31 | | SIMP: (132) implies: % 32.82/5.31 | | (133) all_154_0 = all_137_0 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (124), (125) imply: % 32.82/5.31 | | (134) all_166_1 = all_139_1 % 32.82/5.31 | | % 32.82/5.31 | | SIMP: (134) implies: % 32.82/5.31 | | (135) all_166_1 = all_139_1 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (118), (129) imply: % 32.82/5.31 | | (136) all_157_1 = all_145_1 % 32.82/5.31 | | % 32.82/5.31 | | SIMP: (136) implies: % 32.82/5.31 | | (137) all_157_1 = all_145_1 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (123), (131) imply: % 32.82/5.31 | | (138) all_147_1 = all_77_0 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (131), (135) imply: % 32.82/5.31 | | (139) all_147_1 = all_139_1 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (116), (137) imply: % 32.82/5.31 | | (140) all_145_1 = all_77_2 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (117), (137) imply: % 32.82/5.31 | | (141) all_154_0 = all_145_1 % 32.82/5.31 | | % 32.82/5.31 | | SIMP: (141) implies: % 32.82/5.31 | | (142) all_154_0 = all_145_1 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (133), (142) imply: % 32.82/5.31 | | (143) all_145_1 = all_137_0 % 32.82/5.31 | | % 32.82/5.31 | | SIMP: (143) implies: % 32.82/5.31 | | (144) all_145_1 = all_137_0 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (138), (139) imply: % 32.82/5.31 | | (145) all_139_1 = all_77_0 % 32.82/5.31 | | % 32.82/5.31 | | SIMP: (145) implies: % 32.82/5.31 | | (146) all_139_1 = all_77_0 % 32.82/5.31 | | % 32.82/5.31 | | COMBINE_EQS: (140), (144) imply: % 32.82/5.31 | | (147) all_137_0 = all_77_2 % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (1) with all_77_1, simplifying with (18), (70) % 32.82/5.31 | | gives: % 32.82/5.31 | | (148) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_1) = v0 & % 32.82/5.31 | | the_InternalRel(all_77_1) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : % 32.82/5.31 | | ( ~ $i(v2) | ~ rel_str(v2) | ? [v3: $i] : ? [v4: $i] : % 32.82/5.31 | | (the_carrier(v2) = v3 & the_InternalRel(v2) = v4 & $i(v4) & % 32.82/5.31 | | $i(v3) & ( ~ subset(v4, v1) | ~ subset(v3, v0) | % 32.82/5.31 | | subrelstr(v2, all_77_1)) & ( ~ subrelstr(v2, all_77_1) | % 32.82/5.31 | | (subset(v4, v1) & subset(v3, v0)))))) % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (91) with all_77_1, simplifying with (18), (70) % 32.82/5.31 | | gives: % 32.82/5.31 | | (149) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_1) = v0 & % 32.82/5.31 | | the_InternalRel(all_77_1) = v1 & $i(v1) & $i(v0) & ( ~ subset(v1, % 32.82/5.31 | | all_157_0) | ~ subset(v0, all_157_1) | subrelstr(all_77_1, % 32.82/5.31 | | all_77_3)) & ( ~ subrelstr(all_77_1, all_77_3) | (subset(v1, % 32.82/5.31 | | all_157_0) & subset(v0, all_157_1)))) % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (43) with all_77_1, simplifying with (18), (70) % 32.82/5.31 | | gives: % 32.82/5.31 | | (150) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_1) = v0 & % 32.82/5.31 | | the_InternalRel(all_77_1) = v1 & $i(v1) & $i(v0) & ( ~ subset(v1, % 32.82/5.31 | | all_97_0) | ~ subset(v0, all_97_1) | subrelstr(all_77_1, % 32.82/5.31 | | all_39_0)) & ( ~ subrelstr(all_77_1, all_39_0) | (subset(v1, % 32.82/5.31 | | all_97_0) & subset(v0, all_97_1)))) % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (1) with all_87_0, simplifying with (34), (74) % 32.82/5.31 | | gives: % 32.82/5.31 | | (151) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_87_0) = v0 & % 32.82/5.31 | | the_InternalRel(all_87_0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : % 32.82/5.31 | | ( ~ $i(v2) | ~ rel_str(v2) | ? [v3: $i] : ? [v4: $i] : % 32.82/5.31 | | (the_carrier(v2) = v3 & the_InternalRel(v2) = v4 & $i(v4) & % 32.82/5.31 | | $i(v3) & ( ~ subset(v4, v1) | ~ subset(v3, v0) | % 32.82/5.31 | | subrelstr(v2, all_87_0)) & ( ~ subrelstr(v2, all_87_0) | % 32.82/5.31 | | (subset(v4, v1) & subset(v3, v0)))))) % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (1) with all_91_0, simplifying with (37), (69) % 32.82/5.31 | | gives: % 32.82/5.31 | | (152) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_91_0) = v0 & % 32.82/5.31 | | the_InternalRel(all_91_0) = v1 & $i(v1) & $i(v0) & ! [v2: $i] : % 32.82/5.31 | | ( ~ $i(v2) | ~ rel_str(v2) | ? [v3: $i] : ? [v4: $i] : % 32.82/5.31 | | (the_carrier(v2) = v3 & the_InternalRel(v2) = v4 & $i(v4) & % 32.82/5.31 | | $i(v3) & ( ~ subset(v4, v1) | ~ subset(v3, v0) | % 32.82/5.31 | | subrelstr(v2, all_91_0)) & ( ~ subrelstr(v2, all_91_0) | % 32.82/5.31 | | (subset(v4, v1) & subset(v3, v0)))))) % 32.82/5.31 | | % 32.82/5.31 | | GROUND_INST: instantiating (46) with all_85_0, simplifying with (31), (76) % 32.82/5.31 | | gives: % 32.82/5.31 | | (153) ? [v0: $i] : ? [v1: $i] : (the_mapping(all_77_4, all_85_0) = v1 & % 32.82/5.31 | | the_carrier(all_85_0) = v0 & $i(v1) & $i(v0) & ! [v2: $i] : ( ~ % 32.82/5.31 | | $i(v2) | ~ net_str(v2, all_77_4) | ? [v3: $i] : ? [v4: $i] : % 32.82/5.31 | | ? [v5: $i] : (the_mapping(all_77_4, v2) = v3 & % 32.82/5.31 | | relation_dom_restr_as_relation_of(v0, all_100_0, v1, v4) = v5 % 32.82/5.31 | | & the_carrier(v2) = v4 & $i(v5) & $i(v4) & $i(v3) & ( ~ (v5 = % 32.82/5.31 | | v3) | ~ subrelstr(v2, all_85_0) | subnetstr(v2, % 32.82/5.31 | | all_77_4, all_85_0)) & ( ~ subnetstr(v2, all_77_4, % 32.82/5.31 | | all_85_0) | (v5 = v3 & subrelstr(v2, all_85_0)))))) % 32.82/5.31 | | % 32.82/5.31 | | DELTA: instantiating (149) with fresh symbols all_252_0, all_252_1 gives: % 32.82/5.31 | | (154) the_carrier(all_77_1) = all_252_1 & the_InternalRel(all_77_1) = % 32.82/5.31 | | all_252_0 & $i(all_252_0) & $i(all_252_1) & ( ~ subset(all_252_0, % 32.82/5.31 | | all_157_0) | ~ subset(all_252_1, all_157_1) | % 32.82/5.31 | | subrelstr(all_77_1, all_77_3)) & ( ~ subrelstr(all_77_1, % 32.82/5.31 | | all_77_3) | (subset(all_252_0, all_157_0) & subset(all_252_1, % 32.82/5.31 | | all_157_1))) % 32.82/5.31 | | % 32.82/5.31 | | ALPHA: (154) implies: % 32.82/5.31 | | (155) the_carrier(all_77_1) = all_252_1 % 32.82/5.31 | | (156) ~ subrelstr(all_77_1, all_77_3) | (subset(all_252_0, all_157_0) & % 32.82/5.31 | | subset(all_252_1, all_157_1)) % 32.82/5.31 | | % 32.82/5.31 | | DELTA: instantiating (150) with fresh symbols all_254_0, all_254_1 gives: % 32.82/5.32 | | (157) the_carrier(all_77_1) = all_254_1 & the_InternalRel(all_77_1) = % 32.82/5.32 | | all_254_0 & $i(all_254_0) & $i(all_254_1) & ( ~ subset(all_254_0, % 32.82/5.32 | | all_97_0) | ~ subset(all_254_1, all_97_1) | % 32.82/5.32 | | subrelstr(all_77_1, all_39_0)) & ( ~ subrelstr(all_77_1, % 32.82/5.32 | | all_39_0) | (subset(all_254_0, all_97_0) & subset(all_254_1, % 32.82/5.32 | | all_97_1))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (157) implies: % 32.82/5.32 | | (158) the_carrier(all_77_1) = all_254_1 % 32.82/5.32 | | % 32.82/5.32 | | DELTA: instantiating (148) with fresh symbols all_280_0, all_280_1 gives: % 32.82/5.32 | | (159) the_carrier(all_77_1) = all_280_1 & the_InternalRel(all_77_1) = % 32.82/5.32 | | all_280_0 & $i(all_280_0) & $i(all_280_1) & ! [v0: $i] : ( ~ % 32.82/5.32 | | $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] : % 32.82/5.32 | | (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) & % 32.82/5.32 | | $i(v1) & ( ~ subset(v2, all_280_0) | ~ subset(v1, all_280_1) | % 32.82/5.32 | | subrelstr(v0, all_77_1)) & ( ~ subrelstr(v0, all_77_1) | % 32.82/5.32 | | (subset(v2, all_280_0) & subset(v1, all_280_1))))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (159) implies: % 32.82/5.32 | | (160) the_carrier(all_77_1) = all_280_1 % 32.82/5.32 | | (161) ! [v0: $i] : ( ~ $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: % 32.82/5.32 | | $i] : (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) % 32.82/5.32 | | & $i(v1) & ( ~ subset(v2, all_280_0) | ~ subset(v1, all_280_1) % 32.82/5.32 | | | subrelstr(v0, all_77_1)) & ( ~ subrelstr(v0, all_77_1) | % 32.82/5.32 | | (subset(v2, all_280_0) & subset(v1, all_280_1))))) % 32.82/5.32 | | % 32.82/5.32 | | GROUND_INST: instantiating (161) with all_77_1, simplifying with (18), (70) % 32.82/5.32 | | gives: % 32.82/5.32 | | (162) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_1) = v0 & % 32.82/5.32 | | the_InternalRel(all_77_1) = v1 & $i(v1) & $i(v0) & ( ~ subset(v1, % 32.82/5.32 | | all_280_0) | ~ subset(v0, all_280_1) | subrelstr(all_77_1, % 32.82/5.32 | | all_77_1)) & ( ~ subrelstr(all_77_1, all_77_1) | (subset(v1, % 32.82/5.32 | | all_280_0) & subset(v0, all_280_1)))) % 32.82/5.32 | | % 32.82/5.32 | | DELTA: instantiating (152) with fresh symbols all_283_0, all_283_1 gives: % 32.82/5.32 | | (163) the_carrier(all_91_0) = all_283_1 & the_InternalRel(all_91_0) = % 32.82/5.32 | | all_283_0 & $i(all_283_0) & $i(all_283_1) & ! [v0: $i] : ( ~ % 32.82/5.32 | | $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] : % 32.82/5.32 | | (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) & % 32.82/5.32 | | $i(v1) & ( ~ subset(v2, all_283_0) | ~ subset(v1, all_283_1) | % 32.82/5.32 | | subrelstr(v0, all_91_0)) & ( ~ subrelstr(v0, all_91_0) | % 32.82/5.32 | | (subset(v2, all_283_0) & subset(v1, all_283_1))))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (163) implies: % 32.82/5.32 | | (164) ! [v0: $i] : ( ~ $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: % 32.82/5.32 | | $i] : (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) % 32.82/5.32 | | & $i(v1) & ( ~ subset(v2, all_283_0) | ~ subset(v1, all_283_1) % 32.82/5.32 | | | subrelstr(v0, all_91_0)) & ( ~ subrelstr(v0, all_91_0) | % 32.82/5.32 | | (subset(v2, all_283_0) & subset(v1, all_283_1))))) % 32.82/5.32 | | % 32.82/5.32 | | GROUND_INST: instantiating (164) with all_77_1, simplifying with (18), (70) % 32.82/5.32 | | gives: % 32.82/5.32 | | (165) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_1) = v0 & % 32.82/5.32 | | the_InternalRel(all_77_1) = v1 & $i(v1) & $i(v0) & ( ~ subset(v1, % 32.82/5.32 | | all_283_0) | ~ subset(v0, all_283_1) | subrelstr(all_77_1, % 32.82/5.32 | | all_91_0)) & ( ~ subrelstr(all_77_1, all_91_0) | (subset(v1, % 32.82/5.32 | | all_283_0) & subset(v0, all_283_1)))) % 32.82/5.32 | | % 32.82/5.32 | | DELTA: instantiating (151) with fresh symbols all_289_0, all_289_1 gives: % 32.82/5.32 | | (166) the_carrier(all_87_0) = all_289_1 & the_InternalRel(all_87_0) = % 32.82/5.32 | | all_289_0 & $i(all_289_0) & $i(all_289_1) & ! [v0: $i] : ( ~ % 32.82/5.32 | | $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: $i] : % 32.82/5.32 | | (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) & % 32.82/5.32 | | $i(v1) & ( ~ subset(v2, all_289_0) | ~ subset(v1, all_289_1) | % 32.82/5.32 | | subrelstr(v0, all_87_0)) & ( ~ subrelstr(v0, all_87_0) | % 32.82/5.32 | | (subset(v2, all_289_0) & subset(v1, all_289_1))))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (166) implies: % 32.82/5.32 | | (167) ! [v0: $i] : ( ~ $i(v0) | ~ rel_str(v0) | ? [v1: $i] : ? [v2: % 32.82/5.32 | | $i] : (the_carrier(v0) = v1 & the_InternalRel(v0) = v2 & $i(v2) % 32.82/5.32 | | & $i(v1) & ( ~ subset(v2, all_289_0) | ~ subset(v1, all_289_1) % 32.82/5.32 | | | subrelstr(v0, all_87_0)) & ( ~ subrelstr(v0, all_87_0) | % 32.82/5.32 | | (subset(v2, all_289_0) & subset(v1, all_289_1))))) % 32.82/5.32 | | % 32.82/5.32 | | GROUND_INST: instantiating (167) with all_77_1, simplifying with (18), (70) % 32.82/5.32 | | gives: % 32.82/5.32 | | (168) ? [v0: $i] : ? [v1: $i] : (the_carrier(all_77_1) = v0 & % 32.82/5.32 | | the_InternalRel(all_77_1) = v1 & $i(v1) & $i(v0) & ( ~ subset(v1, % 32.82/5.32 | | all_289_0) | ~ subset(v0, all_289_1) | subrelstr(all_77_1, % 32.82/5.32 | | all_87_0)) & ( ~ subrelstr(all_77_1, all_87_0) | (subset(v1, % 32.82/5.32 | | all_289_0) & subset(v0, all_289_1)))) % 32.82/5.32 | | % 32.82/5.32 | | DELTA: instantiating (153) with fresh symbols all_292_0, all_292_1 gives: % 32.82/5.32 | | (169) the_mapping(all_77_4, all_85_0) = all_292_0 & the_carrier(all_85_0) % 32.82/5.32 | | = all_292_1 & $i(all_292_0) & $i(all_292_1) & ! [v0: $i] : ( ~ % 32.82/5.32 | | $i(v0) | ~ net_str(v0, all_77_4) | ? [v1: $i] : ? [v2: $i] : % 32.82/5.32 | | ? [v3: $i] : (the_mapping(all_77_4, v0) = v1 & % 32.82/5.32 | | relation_dom_restr_as_relation_of(all_292_1, all_100_0, % 32.82/5.32 | | all_292_0, v2) = v3 & the_carrier(v0) = v2 & $i(v3) & $i(v2) % 32.82/5.32 | | & $i(v1) & ( ~ (v3 = v1) | ~ subrelstr(v0, all_85_0) | % 32.82/5.32 | | subnetstr(v0, all_77_4, all_85_0)) & ( ~ subnetstr(v0, % 32.82/5.32 | | all_77_4, all_85_0) | (v3 = v1 & subrelstr(v0, % 32.82/5.32 | | all_85_0))))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (169) implies: % 32.82/5.32 | | (170) ! [v0: $i] : ( ~ $i(v0) | ~ net_str(v0, all_77_4) | ? [v1: $i] : % 32.82/5.32 | | ? [v2: $i] : ? [v3: $i] : (the_mapping(all_77_4, v0) = v1 & % 32.82/5.32 | | relation_dom_restr_as_relation_of(all_292_1, all_100_0, % 32.82/5.32 | | all_292_0, v2) = v3 & the_carrier(v0) = v2 & $i(v3) & $i(v2) % 32.82/5.32 | | & $i(v1) & ( ~ (v3 = v1) | ~ subrelstr(v0, all_85_0) | % 32.82/5.32 | | subnetstr(v0, all_77_4, all_85_0)) & ( ~ subnetstr(v0, % 32.82/5.32 | | all_77_4, all_85_0) | (v3 = v1 & subrelstr(v0, % 32.82/5.32 | | all_85_0))))) % 32.82/5.32 | | % 32.82/5.32 | | GROUND_INST: instantiating (170) with all_77_1, simplifying with (18), (28) % 32.82/5.32 | | gives: % 32.82/5.32 | | (171) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (the_mapping(all_77_4, % 32.82/5.32 | | all_77_1) = v0 & relation_dom_restr_as_relation_of(all_292_1, % 32.82/5.32 | | all_100_0, all_292_0, v1) = v2 & the_carrier(all_77_1) = v1 & % 32.82/5.32 | | $i(v2) & $i(v1) & $i(v0) & ( ~ (v2 = v0) | ~ subrelstr(all_77_1, % 32.82/5.32 | | all_85_0) | subnetstr(all_77_1, all_77_4, all_85_0)) & ( ~ % 32.82/5.32 | | subnetstr(all_77_1, all_77_4, all_85_0) | (v2 = v0 & % 32.82/5.32 | | subrelstr(all_77_1, all_85_0)))) % 32.82/5.32 | | % 32.82/5.32 | | DELTA: instantiating (162) with fresh symbols all_311_0, all_311_1 gives: % 32.82/5.32 | | (172) the_carrier(all_77_1) = all_311_1 & the_InternalRel(all_77_1) = % 32.82/5.32 | | all_311_0 & $i(all_311_0) & $i(all_311_1) & ( ~ subset(all_311_0, % 32.82/5.32 | | all_280_0) | ~ subset(all_311_1, all_280_1) | % 32.82/5.32 | | subrelstr(all_77_1, all_77_1)) & ( ~ subrelstr(all_77_1, % 32.82/5.32 | | all_77_1) | (subset(all_311_0, all_280_0) & subset(all_311_1, % 32.82/5.32 | | all_280_1))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (172) implies: % 32.82/5.32 | | (173) the_carrier(all_77_1) = all_311_1 % 32.82/5.32 | | % 32.82/5.32 | | DELTA: instantiating (165) with fresh symbols all_327_0, all_327_1 gives: % 32.82/5.32 | | (174) the_carrier(all_77_1) = all_327_1 & the_InternalRel(all_77_1) = % 32.82/5.32 | | all_327_0 & $i(all_327_0) & $i(all_327_1) & ( ~ subset(all_327_0, % 32.82/5.32 | | all_283_0) | ~ subset(all_327_1, all_283_1) | % 32.82/5.32 | | subrelstr(all_77_1, all_91_0)) & ( ~ subrelstr(all_77_1, % 32.82/5.32 | | all_91_0) | (subset(all_327_0, all_283_0) & subset(all_327_1, % 32.82/5.32 | | all_283_1))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (174) implies: % 32.82/5.32 | | (175) the_carrier(all_77_1) = all_327_1 % 32.82/5.32 | | % 32.82/5.32 | | DELTA: instantiating (168) with fresh symbols all_347_0, all_347_1 gives: % 32.82/5.32 | | (176) the_carrier(all_77_1) = all_347_1 & the_InternalRel(all_77_1) = % 32.82/5.32 | | all_347_0 & $i(all_347_0) & $i(all_347_1) & ( ~ subset(all_347_0, % 32.82/5.32 | | all_289_0) | ~ subset(all_347_1, all_289_1) | % 32.82/5.32 | | subrelstr(all_77_1, all_87_0)) & ( ~ subrelstr(all_77_1, % 32.82/5.32 | | all_87_0) | (subset(all_347_0, all_289_0) & subset(all_347_1, % 32.82/5.32 | | all_289_1))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (176) implies: % 32.82/5.32 | | (177) the_carrier(all_77_1) = all_347_1 % 32.82/5.32 | | % 32.82/5.32 | | DELTA: instantiating (171) with fresh symbols all_357_0, all_357_1, % 32.82/5.32 | | all_357_2 gives: % 32.82/5.32 | | (178) the_mapping(all_77_4, all_77_1) = all_357_2 & % 32.82/5.32 | | relation_dom_restr_as_relation_of(all_292_1, all_100_0, all_292_0, % 32.82/5.32 | | all_357_1) = all_357_0 & the_carrier(all_77_1) = all_357_1 & % 32.82/5.32 | | $i(all_357_0) & $i(all_357_1) & $i(all_357_2) & ( ~ (all_357_0 = % 32.82/5.32 | | all_357_2) | ~ subrelstr(all_77_1, all_85_0) | % 32.82/5.32 | | subnetstr(all_77_1, all_77_4, all_85_0)) & ( ~ % 32.82/5.32 | | subnetstr(all_77_1, all_77_4, all_85_0) | (all_357_0 = all_357_2 % 32.82/5.32 | | & subrelstr(all_77_1, all_85_0))) % 32.82/5.32 | | % 32.82/5.32 | | ALPHA: (178) implies: % 32.82/5.32 | | (179) the_carrier(all_77_1) = all_357_1 % 32.82/5.32 | | % 32.82/5.32 | | BETA: splitting (156) gives: % 32.82/5.32 | | % 32.82/5.32 | | Case 1: % 32.82/5.32 | | | % 32.82/5.32 | | | (180) ~ subrelstr(all_77_1, all_77_3) % 32.82/5.32 | | | % 32.82/5.32 | | | PRED_UNIFY: (115), (180) imply: % 32.82/5.32 | | | (181) $false % 32.82/5.32 | | | % 32.82/5.32 | | | CLOSE: (181) is inconsistent. % 32.82/5.32 | | | % 32.82/5.32 | | Case 2: % 32.82/5.32 | | | % 32.82/5.32 | | | (182) subset(all_252_0, all_157_0) & subset(all_252_1, all_157_1) % 32.82/5.32 | | | % 32.82/5.32 | | | ALPHA: (182) implies: % 32.82/5.32 | | | (183) subset(all_252_1, all_157_1) % 32.82/5.32 | | | % 32.82/5.32 | | | REDUCE: (116), (183) imply: % 32.82/5.32 | | | (184) subset(all_252_1, all_77_2) % 32.82/5.32 | | | % 32.82/5.32 | | | GROUND_INST: instantiating (6) with all_77_0, all_311_1, all_77_1, % 32.82/5.32 | | | simplifying with (20), (173) gives: % 32.82/5.33 | | | (185) all_311_1 = all_77_0 % 32.82/5.33 | | | % 32.82/5.33 | | | GROUND_INST: instantiating (6) with all_254_1, all_311_1, all_77_1, % 32.82/5.33 | | | simplifying with (158), (173) gives: % 32.82/5.33 | | | (186) all_311_1 = all_254_1 % 32.82/5.33 | | | % 32.82/5.33 | | | GROUND_INST: instantiating (6) with all_311_1, all_327_1, all_77_1, % 32.82/5.33 | | | simplifying with (173), (175) gives: % 32.82/5.33 | | | (187) all_327_1 = all_311_1 % 32.82/5.33 | | | % 32.82/5.33 | | | GROUND_INST: instantiating (6) with all_252_1, all_327_1, all_77_1, % 32.82/5.33 | | | simplifying with (155), (175) gives: % 32.82/5.33 | | | (188) all_327_1 = all_252_1 % 32.82/5.33 | | | % 32.82/5.33 | | | GROUND_INST: instantiating (6) with all_327_1, all_347_1, all_77_1, % 32.82/5.33 | | | simplifying with (175), (177) gives: % 32.82/5.33 | | | (189) all_347_1 = all_327_1 % 32.82/5.33 | | | % 32.82/5.33 | | | GROUND_INST: instantiating (6) with all_347_1, all_357_1, all_77_1, % 32.82/5.33 | | | simplifying with (177), (179) gives: % 32.82/5.33 | | | (190) all_357_1 = all_347_1 % 32.82/5.33 | | | % 32.82/5.33 | | | GROUND_INST: instantiating (6) with all_280_1, all_357_1, all_77_1, % 32.82/5.33 | | | simplifying with (160), (179) gives: % 32.82/5.33 | | | (191) all_357_1 = all_280_1 % 32.82/5.33 | | | % 32.82/5.33 | | | COMBINE_EQS: (190), (191) imply: % 32.82/5.33 | | | (192) all_347_1 = all_280_1 % 32.82/5.33 | | | % 32.82/5.33 | | | SIMP: (192) implies: % 32.82/5.33 | | | (193) all_347_1 = all_280_1 % 32.82/5.33 | | | % 32.82/5.33 | | | COMBINE_EQS: (189), (193) imply: % 32.82/5.33 | | | (194) all_327_1 = all_280_1 % 32.82/5.33 | | | % 32.82/5.33 | | | SIMP: (194) implies: % 32.82/5.33 | | | (195) all_327_1 = all_280_1 % 32.82/5.33 | | | % 32.82/5.33 | | | COMBINE_EQS: (188), (195) imply: % 32.82/5.33 | | | (196) all_280_1 = all_252_1 % 32.82/5.33 | | | % 32.82/5.33 | | | COMBINE_EQS: (187), (195) imply: % 32.82/5.33 | | | (197) all_311_1 = all_280_1 % 32.82/5.33 | | | % 32.82/5.33 | | | SIMP: (197) implies: % 32.82/5.33 | | | (198) all_311_1 = all_280_1 % 32.82/5.33 | | | % 32.82/5.33 | | | COMBINE_EQS: (185), (186) imply: % 32.82/5.33 | | | (199) all_254_1 = all_77_0 % 32.82/5.33 | | | % 32.82/5.33 | | | COMBINE_EQS: (186), (198) imply: % 32.82/5.33 | | | (200) all_280_1 = all_254_1 % 32.82/5.33 | | | % 32.82/5.33 | | | SIMP: (200) implies: % 32.82/5.33 | | | (201) all_280_1 = all_254_1 % 32.82/5.33 | | | % 33.26/5.33 | | | COMBINE_EQS: (196), (201) imply: % 33.26/5.33 | | | (202) all_254_1 = all_252_1 % 33.26/5.33 | | | % 33.26/5.33 | | | SIMP: (202) implies: % 33.26/5.33 | | | (203) all_254_1 = all_252_1 % 33.26/5.33 | | | % 33.26/5.33 | | | COMBINE_EQS: (199), (203) imply: % 33.26/5.33 | | | (204) all_252_1 = all_77_0 % 33.26/5.33 | | | % 33.26/5.33 | | | REDUCE: (184), (204) imply: % 33.26/5.33 | | | (205) subset(all_77_0, all_77_2) % 33.26/5.33 | | | % 33.26/5.33 | | | PRED_UNIFY: (12), (205) imply: % 33.26/5.33 | | | (206) $false % 33.26/5.33 | | | % 33.26/5.33 | | | CLOSE: (206) is inconsistent. % 33.26/5.33 | | | % 33.26/5.33 | | End of split % 33.26/5.33 | | % 33.26/5.33 | End of split % 33.26/5.33 | % 33.26/5.33 End of proof % 33.26/5.33 % SZS output end Proof for theBenchmark % 33.26/5.33 % 33.26/5.33 4719ms %------------------------------------------------------------------------------