%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CAT026+1 : TPTP v8.1.2. Released v3.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n018.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 : Wed Aug 30 18:18:23 EDT 2023 % Result : Theorem 113.10s 15.75s % Output : Proof 114.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : CAT026+1 : TPTP v8.1.2. Released v3.4.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n018.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Sun Aug 27 00:35:30 EDT 2023 % 0.14/0.35 % CPUTime : % 0.21/0.61 ________ _____ % 0.21/0.61 ___ __ \_________(_)________________________________ % 0.21/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.61 % 0.21/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.61 (2023-06-19) % 0.21/0.61 % 0.21/0.61 (c) Philipp Rümmer, 2009-2023 % 0.21/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.61 Amanda Stjerna. % 0.21/0.61 Free software under BSD-3-Clause. % 0.21/0.61 % 0.21/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.61 % 0.21/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.21/0.62 Running up to 7 provers in parallel. % 0.21/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.26/1.20 Prover 4: Preprocessing ... % 3.26/1.21 Prover 1: Preprocessing ... % 3.26/1.24 Prover 0: Preprocessing ... % 3.26/1.24 Prover 5: Preprocessing ... % 3.26/1.24 Prover 3: Preprocessing ... % 3.26/1.24 Prover 6: Preprocessing ... % 3.26/1.24 Prover 2: Preprocessing ... % 8.12/1.90 Prover 1: Warning: ignoring some quantifiers % 9.06/2.04 Prover 5: Proving ... % 9.77/2.06 Prover 3: Warning: ignoring some quantifiers % 9.77/2.07 Prover 1: Constructing countermodel ... % 9.77/2.08 Prover 2: Proving ... % 9.77/2.10 Prover 3: Constructing countermodel ... % 9.77/2.11 Prover 6: Proving ... % 16.91/3.09 Prover 4: Warning: ignoring some quantifiers % 16.91/3.12 Prover 0: Proving ... % 18.14/3.22 Prover 4: Constructing countermodel ... % 22.56/3.81 Prover 3: gave up % 22.56/3.82 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 23.48/3.91 Prover 7: Preprocessing ... % 24.62/4.07 Prover 7: Warning: ignoring some quantifiers % 24.62/4.10 Prover 7: Constructing countermodel ... % 62.74/9.29 Prover 2: stopped % 63.93/9.33 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 64.95/9.38 Prover 8: Preprocessing ... % 65.66/9.50 Prover 8: Warning: ignoring some quantifiers % 65.66/9.50 Prover 8: Constructing countermodel ... % 99.94/13.97 Prover 5: stopped % 99.94/13.99 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 100.47/14.06 Prover 9: Preprocessing ... % 105.59/14.75 Prover 9: Warning: ignoring some quantifiers % 105.59/14.78 Prover 9: Constructing countermodel ... % 113.10/15.73 Prover 7: Found proof (size 171) % 113.10/15.73 Prover 7: proved (11806ms) % 113.10/15.73 Prover 6: stopped % 113.10/15.73 Prover 8: stopped % 113.10/15.73 Prover 1: stopped % 113.10/15.73 Prover 0: stopped % 113.10/15.74 Prover 4: stopped % 113.10/15.75 Prover 9: stopped % 113.10/15.75 % 113.10/15.75 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 113.10/15.75 % 113.10/15.80 % SZS output start Proof for theBenchmark % 113.10/15.80 Assumptions after simplification: % 113.10/15.80 --------------------------------- % 113.10/15.80 % 113.10/15.80 (d7_isocat_2) % 113.60/15.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (k8_isocat_2(v1, % 113.60/15.84 v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v2) | ~ % 113.60/15.84 l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v2) | ~ v2_cat_1(v1) | ~ % 113.60/15.84 v2_cat_1(v0) | ? [v4: $i] : (k11_cat_2(v1, v2) = v4 & $i(v4) & ! [v5: $i] % 113.60/15.84 : ! [v6: $i] : ( ~ (k11_isocat_2(v0, v1, v2, v5) = v6) | ~ $i(v5) | ~ % 113.60/15.84 m2_cat_1(v5, v0, v4) | (k2_isocat_1(v0, v4, v1, v5, v3) = v6 & $i(v6))) % 113.60/15.84 & ! [v5: $i] : ! [v6: $i] : ( ~ (k2_isocat_1(v0, v4, v1, v5, v3) = v6) | % 113.60/15.84 ~ $i(v5) | ~ m2_cat_1(v5, v0, v4) | (k11_isocat_2(v0, v1, v2, v5) = v6 % 113.60/15.84 & $i(v6))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 113.60/15.84 ( ~ (k11_cat_2(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 113.60/15.84 l1_cat_1(v2) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v2) | ~ % 113.60/15.84 v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v4: $i] : (k8_isocat_2(v1, v2) = v4 & % 113.60/15.84 $i(v4) & ! [v5: $i] : ! [v6: $i] : ( ~ (k11_isocat_2(v0, v1, v2, v5) = % 113.60/15.84 v6) | ~ $i(v5) | ~ m2_cat_1(v5, v0, v3) | (k2_isocat_1(v0, v3, v1, % 113.60/15.84 v5, v4) = v6 & $i(v6))) & ! [v5: $i] : ! [v6: $i] : ( ~ % 113.60/15.84 (k2_isocat_1(v0, v3, v1, v5, v4) = v6) | ~ $i(v5) | ~ m2_cat_1(v5, v0, % 113.60/15.84 v3) | (k11_isocat_2(v0, v1, v2, v5) = v6 & $i(v6))))) % 113.60/15.84 % 113.60/15.84 (d8_isocat_2) % 113.60/15.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (k9_isocat_2(v1, % 113.60/15.85 v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v2) | ~ % 113.60/15.85 l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v2) | ~ v2_cat_1(v1) | ~ % 113.60/15.85 v2_cat_1(v0) | ? [v4: $i] : (k11_cat_2(v1, v2) = v4 & $i(v4) & ! [v5: $i] % 113.60/15.85 : ! [v6: $i] : ( ~ (k12_isocat_2(v0, v1, v2, v5) = v6) | ~ $i(v5) | ~ % 113.60/15.85 m2_cat_1(v5, v0, v4) | (k2_isocat_1(v0, v4, v2, v5, v3) = v6 & $i(v6))) % 113.60/15.85 & ! [v5: $i] : ! [v6: $i] : ( ~ (k2_isocat_1(v0, v4, v2, v5, v3) = v6) | % 113.60/15.85 ~ $i(v5) | ~ m2_cat_1(v5, v0, v4) | (k12_isocat_2(v0, v1, v2, v5) = v6 % 113.60/15.85 & $i(v6))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 113.60/15.85 ( ~ (k11_cat_2(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 113.60/15.85 l1_cat_1(v2) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v2) | ~ % 113.60/15.85 v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v4: $i] : (k9_isocat_2(v1, v2) = v4 & % 113.60/15.85 $i(v4) & ! [v5: $i] : ! [v6: $i] : ( ~ (k12_isocat_2(v0, v1, v2, v5) = % 113.60/15.85 v6) | ~ $i(v5) | ~ m2_cat_1(v5, v0, v3) | (k2_isocat_1(v0, v3, v2, % 113.60/15.85 v5, v4) = v6 & $i(v6))) & ! [v5: $i] : ! [v6: $i] : ( ~ % 113.60/15.85 (k2_isocat_1(v0, v3, v2, v5, v4) = v6) | ~ $i(v5) | ~ m2_cat_1(v5, v0, % 113.60/15.85 v3) | (k12_isocat_2(v0, v1, v2, v5) = v6 & $i(v6))))) % 113.60/15.85 % 113.60/15.85 (dt_k11_cat_2) % 113.60/15.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k11_cat_2(v0, v1) = v2) | ~ % 113.60/15.85 $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | % 113.60/15.85 ~ v2_cat_1(v0) | l1_cat_1(v2)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( % 113.60/15.85 ~ (k11_cat_2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ % 113.60/15.85 l1_cat_1(v0) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | v2_cat_1(v2)) % 113.60/15.85 % 113.60/15.85 (dt_k16_cat_2) % 113.60/15.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k11_cat_2(v0, v1) = v2) | ~ % 113.60/15.86 $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | % 113.60/15.86 ~ v2_cat_1(v0) | ? [v3: $i] : (k16_cat_2(v0, v1) = v3 & $i(v3) & % 113.60/15.86 m2_cat_1(v3, v2, v0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 113.60/15.86 (k16_cat_2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ % 113.60/15.86 l1_cat_1(v0) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v3: $i] : % 113.60/15.86 (k11_cat_2(v0, v1) = v3 & $i(v3) & m2_cat_1(v2, v3, v0))) % 113.60/15.86 % 113.60/15.86 (dt_k17_cat_2) % 113.60/15.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k17_cat_2(v0, v1) = v2) | ~ % 113.60/15.86 $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | % 113.60/15.86 ~ v2_cat_1(v0) | ? [v3: $i] : (k11_cat_2(v0, v1) = v3 & $i(v3) & % 113.60/15.86 m2_cat_1(v2, v3, v1))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 113.60/15.86 (k11_cat_2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ % 113.60/15.86 l1_cat_1(v0) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v3: $i] : % 113.60/15.86 (k17_cat_2(v0, v1) = v3 & $i(v3) & m2_cat_1(v3, v2, v1))) % 113.60/15.86 % 113.60/15.86 (dt_k8_isocat_2) % 113.60/15.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k8_isocat_2(v0, v1) = v2) | ~ % 113.60/15.86 $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | % 113.60/15.86 ~ v2_cat_1(v0) | ? [v3: $i] : (k11_cat_2(v0, v1) = v3 & $i(v3) & % 113.60/15.86 m2_cat_1(v2, v3, v0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 113.60/15.86 (k11_cat_2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ % 113.60/15.86 l1_cat_1(v0) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v3: $i] : % 113.60/15.86 (k8_isocat_2(v0, v1) = v3 & $i(v3) & m2_cat_1(v3, v2, v0))) % 113.60/15.86 % 113.60/15.86 (dt_k9_isocat_2) % 113.60/15.86 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k9_isocat_2(v0, v1) = v2) | ~ % 113.60/15.86 $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | % 113.60/15.86 ~ v2_cat_1(v0) | ? [v3: $i] : (k11_cat_2(v0, v1) = v3 & $i(v3) & % 113.60/15.86 m2_cat_1(v2, v3, v1))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 113.60/15.86 (k11_cat_2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ % 113.60/15.86 l1_cat_1(v0) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v3: $i] : % 113.60/15.86 (k9_isocat_2(v0, v1) = v3 & $i(v3) & m2_cat_1(v3, v2, v1))) % 113.60/15.86 % 113.60/15.86 (redefinition_k8_isocat_2) % 113.60/15.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k8_isocat_2(v0, v1) = v2) | ~ % 113.60/15.87 $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | % 113.60/15.87 ~ v2_cat_1(v0) | (k16_cat_2(v0, v1) = v2 & $i(v2))) & ! [v0: $i] : ! [v1: % 113.60/15.87 $i] : ! [v2: $i] : ( ~ (k16_cat_2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 113.60/15.87 ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | % 113.60/15.87 (k8_isocat_2(v0, v1) = v2 & $i(v2))) % 113.60/15.87 % 113.60/15.87 (redefinition_k9_isocat_2) % 113.60/15.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k9_isocat_2(v0, v1) = v2) | ~ % 113.60/15.87 $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | % 113.60/15.87 ~ v2_cat_1(v0) | (k17_cat_2(v0, v1) = v2 & $i(v2))) & ! [v0: $i] : ! [v1: % 113.60/15.87 $i] : ! [v2: $i] : ( ~ (k17_cat_2(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 113.60/15.87 ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | % 113.60/15.87 (k9_isocat_2(v0, v1) = v2 & $i(v2))) % 113.60/15.87 % 113.60/15.87 (reflexivity_r2_nattra_1) % 113.60/15.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) % 113.60/15.87 | ~ $i(v1) | ~ $i(v0) | ~ m2_cat_1(v3, v0, v1) | ~ m2_cat_1(v2, v0, v1) % 113.60/15.87 | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | % 113.60/15.87 r2_nattra_1(v0, v1, v2, v2)) % 113.60/15.87 % 113.60/15.87 (t27_isocat_1) % 113.60/15.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 113.60/15.87 $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ (k2_isocat_1(v0, v1, v2, % 113.60/15.87 v4, v7) = v8) | ~ (k2_isocat_1(v0, v1, v2, v3, v5) = v6) | ~ $i(v7) | % 113.60/15.87 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 113.60/15.87 r2_nattra_1(v1, v2, v5, v7) | ~ r2_nattra_1(v0, v1, v3, v4) | ~ % 113.60/15.87 m2_cat_1(v7, v1, v2) | ~ m2_cat_1(v5, v1, v2) | ~ m2_cat_1(v4, v0, v1) | % 113.60/15.87 ~ m2_cat_1(v3, v0, v1) | ~ l1_cat_1(v2) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) % 113.60/15.87 | ~ v2_cat_1(v2) | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | r2_nattra_1(v0, v2, % 113.60/15.87 v6, v8)) % 113.60/15.87 % 113.60/15.87 (t38_isocat_2) % 113.60/15.87 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 113.60/15.87 $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 113.60/15.87 (k12_isocat_2(v0, v1, v2, v4) = v6 & k11_isocat_2(v0, v1, v2, v4) = v5 & % 113.60/15.87 k11_cat_2(v1, v2) = v3 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) % 113.60/15.87 & $i(v1) & $i(v0) & r2_nattra_1(v0, v3, v4, v7) & m2_cat_1(v7, v0, v3) & % 113.60/15.87 m2_cat_1(v4, v0, v3) & l1_cat_1(v2) & l1_cat_1(v1) & l1_cat_1(v0) & % 113.60/15.87 v2_cat_1(v2) & v2_cat_1(v1) & v2_cat_1(v0) & ((k12_isocat_2(v0, v1, v2, v7) % 113.60/15.87 = v9 & $i(v9) & ~ r2_nattra_1(v0, v2, v6, v9)) | (k11_isocat_2(v0, v1, % 113.60/15.87 v2, v7) = v8 & $i(v8) & ~ r2_nattra_1(v0, v1, v5, v8)))) % 113.60/15.87 % 113.60/15.87 (function-axioms) % 113.60/15.88 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 113.60/15.88 $i] : ! [v6: $i] : (v1 = v0 | ~ (k2_isocat_1(v6, v5, v4, v3, v2) = v1) | % 113.60/15.88 ~ (k2_isocat_1(v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 113.60/15.88 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 113.60/15.88 (k12_isocat_2(v5, v4, v3, v2) = v1) | ~ (k12_isocat_2(v5, v4, v3, v2) = % 113.60/15.88 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 113.60/15.88 : ! [v5: $i] : (v1 = v0 | ~ (k11_isocat_2(v5, v4, v3, v2) = v1) | ~ % 113.60/15.88 (k11_isocat_2(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 113.60/15.88 $i] : ! [v3: $i] : (v1 = v0 | ~ (k5_relat_1(v3, v2) = v1) | ~ % 113.60/15.88 (k5_relat_1(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 113.60/15.88 [v3: $i] : (v1 = v0 | ~ (k9_isocat_2(v3, v2) = v1) | ~ (k9_isocat_2(v3, v2) % 113.60/15.88 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 113.60/15.88 | ~ (k8_isocat_2(v3, v2) = v1) | ~ (k8_isocat_2(v3, v2) = v0)) & ! [v0: % 113.60/15.88 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 113.60/15.88 (k2_zfmisc_1(v3, v2) = v1) | ~ (k2_zfmisc_1(v3, v2) = v0)) & ! [v0: $i] : % 113.60/15.88 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (k17_cat_2(v3, v2) = % 113.60/15.88 v1) | ~ (k17_cat_2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 113.60/15.88 $i] : ! [v3: $i] : (v1 = v0 | ~ (k11_cat_2(v3, v2) = v1) | ~ % 113.60/15.88 (k11_cat_2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 113.60/15.88 [v3: $i] : (v1 = v0 | ~ (k16_cat_2(v3, v2) = v1) | ~ (k16_cat_2(v3, v2) = % 113.60/15.88 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 113.60/15.88 (u2_cat_1(v2) = v1) | ~ (u2_cat_1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 113.60/15.88 ! [v2: $i] : (v1 = v0 | ~ (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) % 113.60/15.88 % 113.60/15.88 Further assumptions not needed in the proof: % 113.60/15.88 -------------------------------------------- % 113.60/15.88 antisymmetry_r2_hidden, cc1_relset_1, dt_k11_isocat_2, dt_k12_isocat_2, % 113.60/15.88 dt_k1_xboole_0, dt_k1_zfmisc_1, dt_k2_isocat_1, dt_k2_zfmisc_1, dt_k5_relat_1, % 113.60/15.88 dt_l1_cat_1, dt_m1_relset_1, dt_m1_subset_1, dt_m2_cat_1, dt_m2_relset_1, % 113.60/15.88 dt_u2_cat_1, existence_l1_cat_1, existence_m1_relset_1, existence_m1_subset_1, % 113.60/15.88 existence_m2_cat_1, existence_m2_relset_1, fc1_subset_1, fc1_xboole_0, % 113.60/15.88 fc4_subset_1, rc1_subset_1, rc1_xboole_0, rc2_subset_1, rc2_xboole_0, % 113.60/15.88 redefinition_k2_isocat_1, redefinition_m2_relset_1, reflexivity_r1_tarski, % 113.60/15.88 t1_subset, t2_subset, t3_subset, t4_subset, t5_subset, t6_boole, t7_boole, % 113.60/15.88 t8_boole % 113.60/15.88 % 113.60/15.88 Those formulas are unsatisfiable: % 113.60/15.88 --------------------------------- % 113.60/15.88 % 113.60/15.88 Begin of proof % 113.60/15.88 | % 113.60/15.88 | ALPHA: (dt_k16_cat_2) implies: % 113.60/15.88 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k11_cat_2(v0, v1) = v2) % 113.60/15.88 | | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ % 113.60/15.88 | v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v3: $i] : (k16_cat_2(v0, v1) = % 113.60/15.88 | v3 & $i(v3) & m2_cat_1(v3, v2, v0))) % 113.60/15.88 | % 113.60/15.88 | ALPHA: (dt_k17_cat_2) implies: % 113.60/15.88 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k11_cat_2(v0, v1) = v2) % 113.60/15.88 | | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ % 113.60/15.88 | v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v3: $i] : (k17_cat_2(v0, v1) = % 113.60/15.88 | v3 & $i(v3) & m2_cat_1(v3, v2, v1))) % 113.60/15.88 | % 113.60/15.88 | ALPHA: (redefinition_k8_isocat_2) implies: % 113.60/15.88 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k16_cat_2(v0, v1) = v2) % 113.60/15.88 | | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ % 113.60/15.88 | v2_cat_1(v1) | ~ v2_cat_1(v0) | (k8_isocat_2(v0, v1) = v2 & $i(v2))) % 113.60/15.88 | % 113.60/15.88 | ALPHA: (redefinition_k9_isocat_2) implies: % 113.60/15.88 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k17_cat_2(v0, v1) = v2) % 113.60/15.88 | | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ % 113.60/15.88 | v2_cat_1(v1) | ~ v2_cat_1(v0) | (k9_isocat_2(v0, v1) = v2 & $i(v2))) % 113.60/15.89 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k9_isocat_2(v0, v1) = % 113.60/15.89 | v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | % 113.60/15.89 | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | (k17_cat_2(v0, v1) = v2 & $i(v2))) % 113.60/15.89 | % 113.60/15.89 | ALPHA: (dt_k8_isocat_2) implies: % 113.60/15.89 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k11_cat_2(v0, v1) = v2) % 113.60/15.89 | | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ % 113.60/15.89 | v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v3: $i] : (k8_isocat_2(v0, v1) = % 113.60/15.89 | v3 & $i(v3) & m2_cat_1(v3, v2, v0))) % 113.60/15.89 | % 113.60/15.89 | ALPHA: (dt_k9_isocat_2) implies: % 113.60/15.89 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k11_cat_2(v0, v1) = v2) % 113.60/15.89 | | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ % 113.60/15.89 | v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v3: $i] : (k9_isocat_2(v0, v1) = % 113.60/15.89 | v3 & $i(v3) & m2_cat_1(v3, v2, v1))) % 113.60/15.89 | % 113.60/15.89 | ALPHA: (dt_k11_cat_2) implies: % 113.60/15.89 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k11_cat_2(v0, v1) = v2) % 113.60/15.89 | | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ % 113.60/15.89 | v2_cat_1(v1) | ~ v2_cat_1(v0) | v2_cat_1(v2)) % 113.60/15.89 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k11_cat_2(v0, v1) = v2) % 113.60/15.89 | | ~ $i(v1) | ~ $i(v0) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ % 113.60/15.89 | v2_cat_1(v1) | ~ v2_cat_1(v0) | l1_cat_1(v2)) % 113.60/15.89 | % 113.60/15.89 | ALPHA: (d7_isocat_2) implies: % 113.60/15.89 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 113.60/15.89 | (k11_cat_2(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 113.60/15.89 | l1_cat_1(v2) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v2) | % 113.60/15.89 | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v4: $i] : (k8_isocat_2(v1, % 113.60/15.89 | v2) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ( ~ % 113.60/15.89 | (k11_isocat_2(v0, v1, v2, v5) = v6) | ~ $i(v5) | ~ % 113.60/15.89 | m2_cat_1(v5, v0, v3) | (k2_isocat_1(v0, v3, v1, v5, v4) = v6 & % 113.60/15.89 | $i(v6))) & ! [v5: $i] : ! [v6: $i] : ( ~ (k2_isocat_1(v0, % 113.60/15.89 | v3, v1, v5, v4) = v6) | ~ $i(v5) | ~ m2_cat_1(v5, v0, v3) % 113.60/15.89 | | (k11_isocat_2(v0, v1, v2, v5) = v6 & $i(v6))))) % 113.60/15.89 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 113.60/15.89 | (k8_isocat_2(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 113.60/15.89 | l1_cat_1(v2) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v2) | % 113.60/15.89 | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v4: $i] : (k11_cat_2(v1, v2) % 113.60/15.89 | = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ( ~ (k11_isocat_2(v0, % 113.60/15.89 | v1, v2, v5) = v6) | ~ $i(v5) | ~ m2_cat_1(v5, v0, v4) | % 113.60/15.89 | (k2_isocat_1(v0, v4, v1, v5, v3) = v6 & $i(v6))) & ! [v5: $i] : % 113.60/15.89 | ! [v6: $i] : ( ~ (k2_isocat_1(v0, v4, v1, v5, v3) = v6) | ~ % 113.60/15.89 | $i(v5) | ~ m2_cat_1(v5, v0, v4) | (k11_isocat_2(v0, v1, v2, v5) % 113.60/15.89 | = v6 & $i(v6))))) % 113.60/15.89 | % 113.60/15.89 | ALPHA: (d8_isocat_2) implies: % 114.03/15.89 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 114.03/15.89 | (k11_cat_2(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 114.03/15.89 | l1_cat_1(v2) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v2) | % 114.03/15.89 | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v4: $i] : (k9_isocat_2(v1, % 114.03/15.89 | v2) = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ( ~ % 114.03/15.89 | (k12_isocat_2(v0, v1, v2, v5) = v6) | ~ $i(v5) | ~ % 114.03/15.89 | m2_cat_1(v5, v0, v3) | (k2_isocat_1(v0, v3, v2, v5, v4) = v6 & % 114.03/15.89 | $i(v6))) & ! [v5: $i] : ! [v6: $i] : ( ~ (k2_isocat_1(v0, % 114.03/15.89 | v3, v2, v5, v4) = v6) | ~ $i(v5) | ~ m2_cat_1(v5, v0, v3) % 114.03/15.89 | | (k12_isocat_2(v0, v1, v2, v5) = v6 & $i(v6))))) % 114.03/15.90 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 114.03/15.90 | (k9_isocat_2(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 114.03/15.90 | l1_cat_1(v2) | ~ l1_cat_1(v1) | ~ l1_cat_1(v0) | ~ v2_cat_1(v2) | % 114.03/15.90 | ~ v2_cat_1(v1) | ~ v2_cat_1(v0) | ? [v4: $i] : (k11_cat_2(v1, v2) % 114.03/15.90 | = v4 & $i(v4) & ! [v5: $i] : ! [v6: $i] : ( ~ (k12_isocat_2(v0, % 114.03/15.90 | v1, v2, v5) = v6) | ~ $i(v5) | ~ m2_cat_1(v5, v0, v4) | % 114.03/15.90 | (k2_isocat_1(v0, v4, v2, v5, v3) = v6 & $i(v6))) & ! [v5: $i] : % 114.03/15.90 | ! [v6: $i] : ( ~ (k2_isocat_1(v0, v4, v2, v5, v3) = v6) | ~ % 114.03/15.90 | $i(v5) | ~ m2_cat_1(v5, v0, v4) | (k12_isocat_2(v0, v1, v2, v5) % 114.03/15.90 | = v6 & $i(v6))))) % 114.03/15.90 | % 114.03/15.90 | ALPHA: (function-axioms) implies: % 114.03/15.90 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 114.03/15.90 | (k11_cat_2(v3, v2) = v1) | ~ (k11_cat_2(v3, v2) = v0)) % 114.03/15.90 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 114.03/15.90 | (k8_isocat_2(v3, v2) = v1) | ~ (k8_isocat_2(v3, v2) = v0)) % 114.03/15.90 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 114.03/15.90 | (k9_isocat_2(v3, v2) = v1) | ~ (k9_isocat_2(v3, v2) = v0)) % 114.03/15.90 | % 114.03/15.90 | DELTA: instantiating (t38_isocat_2) with fresh symbols all_49_0, all_49_1, % 114.03/15.90 | all_49_2, all_49_3, all_49_4, all_49_5, all_49_6, all_49_7, all_49_8, % 114.03/15.90 | all_49_9 gives: % 114.03/15.90 | (17) k12_isocat_2(all_49_9, all_49_8, all_49_7, all_49_5) = all_49_3 & % 114.03/15.90 | k11_isocat_2(all_49_9, all_49_8, all_49_7, all_49_5) = all_49_4 & % 114.03/15.90 | k11_cat_2(all_49_8, all_49_7) = all_49_6 & $i(all_49_2) & $i(all_49_3) % 114.03/15.90 | & $i(all_49_4) & $i(all_49_5) & $i(all_49_6) & $i(all_49_7) & % 114.03/15.90 | $i(all_49_8) & $i(all_49_9) & r2_nattra_1(all_49_9, all_49_6, % 114.03/15.90 | all_49_5, all_49_2) & m2_cat_1(all_49_2, all_49_9, all_49_6) & % 114.03/15.90 | m2_cat_1(all_49_5, all_49_9, all_49_6) & l1_cat_1(all_49_7) & % 114.03/15.90 | l1_cat_1(all_49_8) & l1_cat_1(all_49_9) & v2_cat_1(all_49_7) & % 114.03/15.90 | v2_cat_1(all_49_8) & v2_cat_1(all_49_9) & ((k12_isocat_2(all_49_9, % 114.03/15.90 | all_49_8, all_49_7, all_49_2) = all_49_0 & $i(all_49_0) & ~ % 114.03/15.90 | r2_nattra_1(all_49_9, all_49_7, all_49_3, all_49_0)) | % 114.03/15.90 | (k11_isocat_2(all_49_9, all_49_8, all_49_7, all_49_2) = all_49_1 & % 114.03/15.90 | $i(all_49_1) & ~ r2_nattra_1(all_49_9, all_49_8, all_49_4, % 114.03/15.90 | all_49_1))) % 114.03/15.90 | % 114.03/15.90 | ALPHA: (17) implies: % 114.03/15.90 | (18) v2_cat_1(all_49_9) % 114.03/15.90 | (19) v2_cat_1(all_49_8) % 114.03/15.90 | (20) v2_cat_1(all_49_7) % 114.03/15.90 | (21) l1_cat_1(all_49_9) % 114.03/15.90 | (22) l1_cat_1(all_49_8) % 114.03/15.90 | (23) l1_cat_1(all_49_7) % 114.03/15.90 | (24) m2_cat_1(all_49_5, all_49_9, all_49_6) % 114.03/15.90 | (25) m2_cat_1(all_49_2, all_49_9, all_49_6) % 114.03/15.90 | (26) r2_nattra_1(all_49_9, all_49_6, all_49_5, all_49_2) % 114.03/15.90 | (27) $i(all_49_9) % 114.03/15.90 | (28) $i(all_49_8) % 114.03/15.90 | (29) $i(all_49_7) % 114.03/15.90 | (30) $i(all_49_6) % 114.03/15.90 | (31) $i(all_49_5) % 114.03/15.90 | (32) $i(all_49_2) % 114.03/15.90 | (33) k11_cat_2(all_49_8, all_49_7) = all_49_6 % 114.03/15.90 | (34) k11_isocat_2(all_49_9, all_49_8, all_49_7, all_49_5) = all_49_4 % 114.03/15.90 | (35) k12_isocat_2(all_49_9, all_49_8, all_49_7, all_49_5) = all_49_3 % 114.03/15.90 | (36) (k12_isocat_2(all_49_9, all_49_8, all_49_7, all_49_2) = all_49_0 & % 114.03/15.90 | $i(all_49_0) & ~ r2_nattra_1(all_49_9, all_49_7, all_49_3, % 114.03/15.90 | all_49_0)) | (k11_isocat_2(all_49_9, all_49_8, all_49_7, all_49_2) % 114.03/15.90 | = all_49_1 & $i(all_49_1) & ~ r2_nattra_1(all_49_9, all_49_8, % 114.03/15.90 | all_49_4, all_49_1)) % 114.03/15.90 | % 114.03/15.90 | GROUND_INST: instantiating (12) with all_49_7, all_49_8, all_49_7, all_49_6, % 114.03/15.90 | simplifying with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.91 | (37) ? [v0: $i] : (k9_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.91 | $i] : ! [v2: $i] : ( ~ (k12_isocat_2(all_49_7, all_49_8, % 114.03/15.91 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_7, % 114.03/15.91 | all_49_6) | (k2_isocat_1(all_49_7, all_49_6, all_49_7, v1, v0) = % 114.03/15.91 | v2 & $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.91 | (k2_isocat_1(all_49_7, all_49_6, all_49_7, v1, v0) = v2) | ~ % 114.03/15.91 | $i(v1) | ~ m2_cat_1(v1, all_49_7, all_49_6) | % 114.03/15.91 | (k12_isocat_2(all_49_7, all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.91 | % 114.03/15.91 | GROUND_INST: instantiating (10) with all_49_7, all_49_8, all_49_7, all_49_6, % 114.03/15.91 | simplifying with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.91 | (38) ? [v0: $i] : (k8_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.91 | $i] : ! [v2: $i] : ( ~ (k11_isocat_2(all_49_7, all_49_8, % 114.03/15.91 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_7, % 114.03/15.91 | all_49_6) | (k2_isocat_1(all_49_7, all_49_6, all_49_8, v1, v0) = % 114.03/15.91 | v2 & $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.91 | (k2_isocat_1(all_49_7, all_49_6, all_49_8, v1, v0) = v2) | ~ % 114.03/15.91 | $i(v1) | ~ m2_cat_1(v1, all_49_7, all_49_6) | % 114.03/15.91 | (k11_isocat_2(all_49_7, all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.91 | % 114.03/15.91 | GROUND_INST: instantiating (10) with all_49_8, all_49_8, all_49_8, all_49_6, % 114.03/15.91 | simplifying with (19), (22), (28) gives: % 114.03/15.91 | (39) ~ (k11_cat_2(all_49_8, all_49_8) = all_49_6) | ? [v0: $i] : % 114.03/15.91 | (k8_isocat_2(all_49_8, all_49_8) = v0 & $i(v0) & ! [v1: $i] : ! [v2: % 114.03/15.91 | $i] : ( ~ (k11_isocat_2(all_49_8, all_49_8, all_49_8, v1) = v2) | % 114.03/15.91 | ~ $i(v1) | ~ m2_cat_1(v1, all_49_8, all_49_6) | % 114.03/15.91 | (k2_isocat_1(all_49_8, all_49_6, all_49_8, v1, v0) = v2 & $i(v2))) % 114.03/15.91 | & ! [v1: $i] : ! [v2: $i] : ( ~ (k2_isocat_1(all_49_8, all_49_6, % 114.03/15.91 | all_49_8, v1, v0) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, % 114.03/15.91 | all_49_8, all_49_6) | (k11_isocat_2(all_49_8, all_49_8, % 114.03/15.91 | all_49_8, v1) = v2 & $i(v2)))) % 114.03/15.91 | % 114.03/15.91 | GROUND_INST: instantiating (12) with all_49_8, all_49_8, all_49_7, all_49_6, % 114.03/15.91 | simplifying with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.91 | (40) ? [v0: $i] : (k9_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.91 | $i] : ! [v2: $i] : ( ~ (k12_isocat_2(all_49_8, all_49_8, % 114.03/15.91 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_8, % 114.03/15.91 | all_49_6) | (k2_isocat_1(all_49_8, all_49_6, all_49_7, v1, v0) = % 114.03/15.91 | v2 & $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.91 | (k2_isocat_1(all_49_8, all_49_6, all_49_7, v1, v0) = v2) | ~ % 114.03/15.91 | $i(v1) | ~ m2_cat_1(v1, all_49_8, all_49_6) | % 114.03/15.91 | (k12_isocat_2(all_49_8, all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.91 | % 114.03/15.91 | GROUND_INST: instantiating (10) with all_49_8, all_49_8, all_49_7, all_49_6, % 114.03/15.91 | simplifying with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.91 | (41) ? [v0: $i] : (k8_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.91 | $i] : ! [v2: $i] : ( ~ (k11_isocat_2(all_49_8, all_49_8, % 114.03/15.91 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_8, % 114.03/15.91 | all_49_6) | (k2_isocat_1(all_49_8, all_49_6, all_49_8, v1, v0) = % 114.03/15.91 | v2 & $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.91 | (k2_isocat_1(all_49_8, all_49_6, all_49_8, v1, v0) = v2) | ~ % 114.03/15.91 | $i(v1) | ~ m2_cat_1(v1, all_49_8, all_49_6) | % 114.03/15.91 | (k11_isocat_2(all_49_8, all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.91 | % 114.03/15.91 | GROUND_INST: instantiating (12) with all_49_9, all_49_8, all_49_7, all_49_6, % 114.03/15.91 | simplifying with (18), (19), (20), (21), (22), (23), (27), (28), % 114.03/15.91 | (29), (33) gives: % 114.03/15.92 | (42) ? [v0: $i] : (k9_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.92 | $i] : ! [v2: $i] : ( ~ (k12_isocat_2(all_49_9, all_49_8, % 114.03/15.92 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_9, % 114.03/15.92 | all_49_6) | (k2_isocat_1(all_49_9, all_49_6, all_49_7, v1, v0) = % 114.03/15.92 | v2 & $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.92 | (k2_isocat_1(all_49_9, all_49_6, all_49_7, v1, v0) = v2) | ~ % 114.03/15.92 | $i(v1) | ~ m2_cat_1(v1, all_49_9, all_49_6) | % 114.03/15.92 | (k12_isocat_2(all_49_9, all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.92 | % 114.03/15.92 | GROUND_INST: instantiating (10) with all_49_9, all_49_8, all_49_7, all_49_6, % 114.03/15.92 | simplifying with (18), (19), (20), (21), (22), (23), (27), (28), % 114.03/15.92 | (29), (33) gives: % 114.03/15.92 | (43) ? [v0: $i] : (k8_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.92 | $i] : ! [v2: $i] : ( ~ (k11_isocat_2(all_49_9, all_49_8, % 114.03/15.92 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_9, % 114.03/15.92 | all_49_6) | (k2_isocat_1(all_49_9, all_49_6, all_49_8, v1, v0) = % 114.03/15.92 | v2 & $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.92 | (k2_isocat_1(all_49_9, all_49_6, all_49_8, v1, v0) = v2) | ~ % 114.03/15.92 | $i(v1) | ~ m2_cat_1(v1, all_49_9, all_49_6) | % 114.03/15.92 | (k11_isocat_2(all_49_9, all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.92 | % 114.03/15.92 | GROUND_INST: instantiating (9) with all_49_8, all_49_7, all_49_6, simplifying % 114.03/15.92 | with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.92 | (44) l1_cat_1(all_49_6) % 114.03/15.92 | % 114.03/15.92 | GROUND_INST: instantiating (8) with all_49_8, all_49_7, all_49_6, simplifying % 114.03/15.92 | with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.92 | (45) v2_cat_1(all_49_6) % 114.03/15.92 | % 114.03/15.92 | GROUND_INST: instantiating (7) with all_49_8, all_49_7, all_49_6, simplifying % 114.03/15.92 | with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.92 | (46) ? [v0: $i] : (k9_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & % 114.03/15.92 | m2_cat_1(v0, all_49_6, all_49_7)) % 114.03/15.92 | % 114.03/15.92 | GROUND_INST: instantiating (6) with all_49_8, all_49_7, all_49_6, simplifying % 114.03/15.92 | with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.92 | (47) ? [v0: $i] : (k8_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & % 114.03/15.92 | m2_cat_1(v0, all_49_6, all_49_8)) % 114.03/15.92 | % 114.03/15.92 | GROUND_INST: instantiating (2) with all_49_8, all_49_7, all_49_6, simplifying % 114.03/15.92 | with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.92 | (48) ? [v0: $i] : (k17_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & % 114.03/15.92 | m2_cat_1(v0, all_49_6, all_49_7)) % 114.03/15.92 | % 114.03/15.92 | GROUND_INST: instantiating (1) with all_49_8, all_49_7, all_49_6, simplifying % 114.03/15.92 | with (19), (20), (22), (23), (28), (29), (33) gives: % 114.03/15.92 | (49) ? [v0: $i] : (k16_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & % 114.03/15.92 | m2_cat_1(v0, all_49_6, all_49_8)) % 114.03/15.92 | % 114.03/15.92 | DELTA: instantiating (48) with fresh symbol all_79_0 gives: % 114.03/15.92 | (50) k17_cat_2(all_49_8, all_49_7) = all_79_0 & $i(all_79_0) & % 114.03/15.92 | m2_cat_1(all_79_0, all_49_6, all_49_7) % 114.03/15.92 | % 114.03/15.92 | ALPHA: (50) implies: % 114.03/15.92 | (51) m2_cat_1(all_79_0, all_49_6, all_49_7) % 114.03/15.92 | (52) $i(all_79_0) % 114.03/15.92 | (53) k17_cat_2(all_49_8, all_49_7) = all_79_0 % 114.03/15.92 | % 114.03/15.92 | DELTA: instantiating (47) with fresh symbol all_81_0 gives: % 114.03/15.92 | (54) k8_isocat_2(all_49_8, all_49_7) = all_81_0 & $i(all_81_0) & % 114.03/15.92 | m2_cat_1(all_81_0, all_49_6, all_49_8) % 114.03/15.92 | % 114.03/15.92 | ALPHA: (54) implies: % 114.03/15.92 | (55) m2_cat_1(all_81_0, all_49_6, all_49_8) % 114.03/15.92 | (56) k8_isocat_2(all_49_8, all_49_7) = all_81_0 % 114.03/15.92 | % 114.03/15.92 | DELTA: instantiating (46) with fresh symbol all_83_0 gives: % 114.03/15.92 | (57) k9_isocat_2(all_49_8, all_49_7) = all_83_0 & $i(all_83_0) & % 114.03/15.92 | m2_cat_1(all_83_0, all_49_6, all_49_7) % 114.03/15.92 | % 114.03/15.92 | ALPHA: (57) implies: % 114.03/15.93 | (58) m2_cat_1(all_83_0, all_49_6, all_49_7) % 114.03/15.93 | (59) k9_isocat_2(all_49_8, all_49_7) = all_83_0 % 114.03/15.93 | % 114.03/15.93 | DELTA: instantiating (49) with fresh symbol all_85_0 gives: % 114.03/15.93 | (60) k16_cat_2(all_49_8, all_49_7) = all_85_0 & $i(all_85_0) & % 114.03/15.93 | m2_cat_1(all_85_0, all_49_6, all_49_8) % 114.03/15.93 | % 114.03/15.93 | ALPHA: (60) implies: % 114.03/15.93 | (61) m2_cat_1(all_85_0, all_49_6, all_49_8) % 114.03/15.93 | (62) $i(all_85_0) % 114.03/15.93 | (63) k16_cat_2(all_49_8, all_49_7) = all_85_0 % 114.03/15.93 | % 114.03/15.93 | DELTA: instantiating (40) with fresh symbol all_87_0 gives: % 114.03/15.93 | (64) k9_isocat_2(all_49_8, all_49_7) = all_87_0 & $i(all_87_0) & ! [v0: % 114.03/15.93 | $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_8, all_49_8, all_49_7, % 114.03/15.93 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_8, all_49_6) | % 114.03/15.93 | (k2_isocat_1(all_49_8, all_49_6, all_49_7, v0, all_87_0) = v1 & % 114.03/15.93 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_8, % 114.03/15.93 | all_49_6, all_49_7, v0, all_87_0) = v1) | ~ $i(v0) | ~ % 114.03/15.93 | m2_cat_1(v0, all_49_8, all_49_6) | (k12_isocat_2(all_49_8, all_49_8, % 114.03/15.93 | all_49_7, v0) = v1 & $i(v1))) % 114.03/15.93 | % 114.03/15.93 | ALPHA: (64) implies: % 114.03/15.93 | (65) $i(all_87_0) % 114.03/15.93 | (66) k9_isocat_2(all_49_8, all_49_7) = all_87_0 % 114.03/15.93 | % 114.03/15.93 | DELTA: instantiating (37) with fresh symbol all_90_0 gives: % 114.03/15.93 | (67) k9_isocat_2(all_49_8, all_49_7) = all_90_0 & $i(all_90_0) & ! [v0: % 114.03/15.93 | $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_7, all_49_8, all_49_7, % 114.03/15.93 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_7, all_49_6) | % 114.03/15.93 | (k2_isocat_1(all_49_7, all_49_6, all_49_7, v0, all_90_0) = v1 & % 114.03/15.93 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_7, % 114.03/15.93 | all_49_6, all_49_7, v0, all_90_0) = v1) | ~ $i(v0) | ~ % 114.03/15.93 | m2_cat_1(v0, all_49_7, all_49_6) | (k12_isocat_2(all_49_7, all_49_8, % 114.03/15.93 | all_49_7, v0) = v1 & $i(v1))) % 114.03/15.93 | % 114.03/15.93 | ALPHA: (67) implies: % 114.03/15.93 | (68) k9_isocat_2(all_49_8, all_49_7) = all_90_0 % 114.03/15.93 | % 114.03/15.93 | DELTA: instantiating (43) with fresh symbol all_93_0 gives: % 114.03/15.93 | (69) k8_isocat_2(all_49_8, all_49_7) = all_93_0 & $i(all_93_0) & ! [v0: % 114.03/15.93 | $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_9, all_49_8, all_49_7, % 114.03/15.93 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_9, all_49_6) | % 114.03/15.93 | (k2_isocat_1(all_49_9, all_49_6, all_49_8, v0, all_93_0) = v1 & % 114.03/15.93 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_9, % 114.03/15.93 | all_49_6, all_49_8, v0, all_93_0) = v1) | ~ $i(v0) | ~ % 114.03/15.93 | m2_cat_1(v0, all_49_9, all_49_6) | (k11_isocat_2(all_49_9, all_49_8, % 114.03/15.93 | all_49_7, v0) = v1 & $i(v1))) % 114.03/15.93 | % 114.03/15.93 | ALPHA: (69) implies: % 114.03/15.93 | (70) $i(all_93_0) % 114.03/15.93 | (71) k8_isocat_2(all_49_8, all_49_7) = all_93_0 % 114.03/15.93 | (72) ! [v0: $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_9, all_49_8, % 114.03/15.93 | all_49_7, v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_9, % 114.03/15.93 | all_49_6) | (k2_isocat_1(all_49_9, all_49_6, all_49_8, v0, % 114.03/15.93 | all_93_0) = v1 & $i(v1))) % 114.03/15.93 | % 114.03/15.93 | GROUND_INST: instantiating (72) with all_49_5, all_49_4, simplifying with % 114.03/15.93 | (24), (31), (34) gives: % 114.03/15.93 | (73) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_5, all_93_0) = % 114.03/15.93 | all_49_4 & $i(all_49_4) % 114.03/15.93 | % 114.03/15.93 | ALPHA: (73) implies: % 114.03/15.93 | (74) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_5, all_93_0) = % 114.03/15.93 | all_49_4 % 114.03/15.93 | % 114.03/15.93 | DELTA: instantiating (38) with fresh symbol all_97_0 gives: % 114.03/15.93 | (75) k8_isocat_2(all_49_8, all_49_7) = all_97_0 & $i(all_97_0) & ! [v0: % 114.03/15.93 | $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_7, all_49_8, all_49_7, % 114.03/15.93 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_7, all_49_6) | % 114.03/15.93 | (k2_isocat_1(all_49_7, all_49_6, all_49_8, v0, all_97_0) = v1 & % 114.03/15.93 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_7, % 114.03/15.93 | all_49_6, all_49_8, v0, all_97_0) = v1) | ~ $i(v0) | ~ % 114.03/15.93 | m2_cat_1(v0, all_49_7, all_49_6) | (k11_isocat_2(all_49_7, all_49_8, % 114.03/15.93 | all_49_7, v0) = v1 & $i(v1))) % 114.03/15.93 | % 114.03/15.93 | ALPHA: (75) implies: % 114.03/15.93 | (76) k8_isocat_2(all_49_8, all_49_7) = all_97_0 % 114.03/15.93 | % 114.03/15.93 | DELTA: instantiating (42) with fresh symbol all_100_0 gives: % 114.03/15.94 | (77) k9_isocat_2(all_49_8, all_49_7) = all_100_0 & $i(all_100_0) & ! [v0: % 114.03/15.94 | $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_9, all_49_8, all_49_7, % 114.03/15.94 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_9, all_49_6) | % 114.03/15.94 | (k2_isocat_1(all_49_9, all_49_6, all_49_7, v0, all_100_0) = v1 & % 114.03/15.94 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_9, % 114.03/15.94 | all_49_6, all_49_7, v0, all_100_0) = v1) | ~ $i(v0) | ~ % 114.03/15.94 | m2_cat_1(v0, all_49_9, all_49_6) | (k12_isocat_2(all_49_9, all_49_8, % 114.03/15.94 | all_49_7, v0) = v1 & $i(v1))) % 114.03/15.94 | % 114.03/15.94 | ALPHA: (77) implies: % 114.03/15.94 | (78) k9_isocat_2(all_49_8, all_49_7) = all_100_0 % 114.03/15.94 | (79) ! [v0: $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_9, all_49_8, % 114.03/15.94 | all_49_7, v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_9, % 114.03/15.94 | all_49_6) | (k2_isocat_1(all_49_9, all_49_6, all_49_7, v0, % 114.03/15.94 | all_100_0) = v1 & $i(v1))) % 114.03/15.94 | % 114.03/15.94 | GROUND_INST: instantiating (79) with all_49_5, all_49_3, simplifying with % 114.03/15.94 | (24), (31), (35) gives: % 114.03/15.94 | (80) k2_isocat_1(all_49_9, all_49_6, all_49_7, all_49_5, all_100_0) = % 114.03/15.94 | all_49_3 & $i(all_49_3) % 114.03/15.94 | % 114.03/15.94 | ALPHA: (80) implies: % 114.03/15.94 | (81) k2_isocat_1(all_49_9, all_49_6, all_49_7, all_49_5, all_100_0) = % 114.03/15.94 | all_49_3 % 114.03/15.94 | % 114.03/15.94 | DELTA: instantiating (41) with fresh symbol all_104_0 gives: % 114.03/15.94 | (82) k8_isocat_2(all_49_8, all_49_7) = all_104_0 & $i(all_104_0) & ! [v0: % 114.03/15.94 | $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_8, all_49_8, all_49_7, % 114.03/15.94 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_8, all_49_6) | % 114.03/15.94 | (k2_isocat_1(all_49_8, all_49_6, all_49_8, v0, all_104_0) = v1 & % 114.03/15.94 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_8, % 114.03/15.94 | all_49_6, all_49_8, v0, all_104_0) = v1) | ~ $i(v0) | ~ % 114.03/15.94 | m2_cat_1(v0, all_49_8, all_49_6) | (k11_isocat_2(all_49_8, all_49_8, % 114.03/15.94 | all_49_7, v0) = v1 & $i(v1))) % 114.03/15.94 | % 114.03/15.94 | ALPHA: (82) implies: % 114.03/15.94 | (83) k8_isocat_2(all_49_8, all_49_7) = all_104_0 % 114.03/15.94 | % 114.03/15.94 | GROUND_INST: instantiating (15) with all_93_0, all_97_0, all_49_7, all_49_8, % 114.03/15.94 | simplifying with (71), (76) gives: % 114.03/15.94 | (84) all_97_0 = all_93_0 % 114.03/15.94 | % 114.03/15.94 | GROUND_INST: instantiating (15) with all_97_0, all_104_0, all_49_7, all_49_8, % 114.03/15.94 | simplifying with (76), (83) gives: % 114.03/15.94 | (85) all_104_0 = all_97_0 % 114.03/15.94 | % 114.03/15.94 | GROUND_INST: instantiating (15) with all_81_0, all_104_0, all_49_7, all_49_8, % 114.03/15.94 | simplifying with (56), (83) gives: % 114.03/15.94 | (86) all_104_0 = all_81_0 % 114.03/15.94 | % 114.03/15.94 | GROUND_INST: instantiating (16) with all_83_0, all_90_0, all_49_7, all_49_8, % 114.03/15.94 | simplifying with (59), (68) gives: % 114.03/15.94 | (87) all_90_0 = all_83_0 % 114.03/15.94 | % 114.03/15.94 | GROUND_INST: instantiating (16) with all_90_0, all_100_0, all_49_7, all_49_8, % 114.03/15.94 | simplifying with (68), (78) gives: % 114.03/15.94 | (88) all_100_0 = all_90_0 % 114.03/15.94 | % 114.03/15.94 | GROUND_INST: instantiating (16) with all_87_0, all_100_0, all_49_7, all_49_8, % 114.03/15.94 | simplifying with (66), (78) gives: % 114.03/15.94 | (89) all_100_0 = all_87_0 % 114.03/15.94 | % 114.03/15.94 | COMBINE_EQS: (85), (86) imply: % 114.03/15.94 | (90) all_97_0 = all_81_0 % 114.03/15.94 | % 114.03/15.94 | SIMP: (90) implies: % 114.03/15.94 | (91) all_97_0 = all_81_0 % 114.03/15.94 | % 114.03/15.94 | COMBINE_EQS: (88), (89) imply: % 114.03/15.94 | (92) all_90_0 = all_87_0 % 114.03/15.94 | % 114.03/15.94 | SIMP: (92) implies: % 114.03/15.94 | (93) all_90_0 = all_87_0 % 114.03/15.94 | % 114.03/15.94 | COMBINE_EQS: (84), (91) imply: % 114.03/15.94 | (94) all_93_0 = all_81_0 % 114.03/15.94 | % 114.03/15.94 | SIMP: (94) implies: % 114.03/15.94 | (95) all_93_0 = all_81_0 % 114.03/15.94 | % 114.03/15.94 | COMBINE_EQS: (87), (93) imply: % 114.03/15.94 | (96) all_87_0 = all_83_0 % 114.03/15.94 | % 114.03/15.94 | COMBINE_EQS: (89), (96) imply: % 114.03/15.94 | (97) all_100_0 = all_83_0 % 114.03/15.94 | % 114.03/15.94 | REDUCE: (81), (97) imply: % 114.03/15.94 | (98) k2_isocat_1(all_49_9, all_49_6, all_49_7, all_49_5, all_83_0) = % 114.03/15.94 | all_49_3 % 114.03/15.94 | % 114.03/15.94 | REDUCE: (74), (95) imply: % 114.03/15.94 | (99) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_5, all_81_0) = % 114.03/15.94 | all_49_4 % 114.03/15.94 | % 114.03/15.94 | REDUCE: (70), (95) imply: % 114.03/15.94 | (100) $i(all_81_0) % 114.03/15.94 | % 114.03/15.94 | REDUCE: (65), (96) imply: % 114.03/15.94 | (101) $i(all_83_0) % 114.03/15.94 | % 114.03/15.95 | GROUND_INST: instantiating (12) with all_49_6, all_49_8, all_49_7, all_49_6, % 114.03/15.95 | simplifying with (19), (20), (22), (23), (28), (29), (30), (33), % 114.03/15.95 | (44), (45) gives: % 114.03/15.95 | (102) ? [v0: $i] : (k9_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! % 114.03/15.95 | [v1: $i] : ! [v2: $i] : ( ~ (k12_isocat_2(all_49_6, all_49_8, % 114.03/15.95 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_6, % 114.03/15.95 | all_49_6) | (k2_isocat_1(all_49_6, all_49_6, all_49_7, v1, v0) % 114.03/15.95 | = v2 & $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.95 | (k2_isocat_1(all_49_6, all_49_6, all_49_7, v1, v0) = v2) | ~ % 114.03/15.95 | $i(v1) | ~ m2_cat_1(v1, all_49_6, all_49_6) | % 114.03/15.95 | (k12_isocat_2(all_49_6, all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.95 | % 114.03/15.95 | GROUND_INST: instantiating (10) with all_49_6, all_49_8, all_49_7, all_49_6, % 114.03/15.95 | simplifying with (19), (20), (22), (23), (28), (29), (30), (33), % 114.03/15.95 | (44), (45) gives: % 114.03/15.95 | (103) ? [v0: $i] : (k8_isocat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! % 114.03/15.95 | [v1: $i] : ! [v2: $i] : ( ~ (k11_isocat_2(all_49_6, all_49_8, % 114.03/15.95 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_6, % 114.03/15.95 | all_49_6) | (k2_isocat_1(all_49_6, all_49_6, all_49_8, v1, v0) % 114.03/15.95 | = v2 & $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.95 | (k2_isocat_1(all_49_6, all_49_6, all_49_8, v1, v0) = v2) | ~ % 114.03/15.95 | $i(v1) | ~ m2_cat_1(v1, all_49_6, all_49_6) | % 114.03/15.95 | (k11_isocat_2(all_49_6, all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.95 | % 114.03/15.95 | GROUND_INST: instantiating (reflexivity_r2_nattra_1) with all_49_6, all_49_7, % 114.03/15.95 | all_83_0, all_79_0, simplifying with (20), (23), (29), (30), % 114.03/15.95 | (44), (45), (51), (52), (58), (101) gives: % 114.03/15.95 | (104) r2_nattra_1(all_49_6, all_49_7, all_83_0, all_83_0) % 114.03/15.95 | % 114.03/15.95 | GROUND_INST: instantiating (reflexivity_r2_nattra_1) with all_49_6, all_49_8, % 114.03/15.95 | all_85_0, all_81_0, simplifying with (19), (22), (28), (30), % 114.03/15.95 | (44), (45), (55), (61), (62), (100) gives: % 114.03/15.95 | (105) r2_nattra_1(all_49_6, all_49_8, all_85_0, all_85_0) % 114.03/15.95 | % 114.03/15.95 | GROUND_INST: instantiating (3) with all_49_8, all_49_7, all_85_0, simplifying % 114.03/15.95 | with (19), (20), (22), (23), (28), (29), (63) gives: % 114.03/15.95 | (106) k8_isocat_2(all_49_8, all_49_7) = all_85_0 & $i(all_85_0) % 114.03/15.95 | % 114.03/15.95 | ALPHA: (106) implies: % 114.03/15.95 | (107) k8_isocat_2(all_49_8, all_49_7) = all_85_0 % 114.03/15.95 | % 114.03/15.95 | GROUND_INST: instantiating (4) with all_49_8, all_49_7, all_79_0, simplifying % 114.03/15.95 | with (19), (20), (22), (23), (28), (29), (53) gives: % 114.03/15.95 | (108) k9_isocat_2(all_49_8, all_49_7) = all_79_0 & $i(all_79_0) % 114.03/15.95 | % 114.03/15.95 | ALPHA: (108) implies: % 114.03/15.95 | (109) k9_isocat_2(all_49_8, all_49_7) = all_79_0 % 114.03/15.95 | % 114.03/15.95 | GROUND_INST: instantiating (11) with all_49_7, all_49_8, all_49_7, all_81_0, % 114.03/15.95 | simplifying with (19), (20), (22), (23), (28), (29), (56) gives: % 114.03/15.95 | (110) ? [v0: $i] : (k11_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.95 | $i] : ! [v2: $i] : ( ~ (k11_isocat_2(all_49_7, all_49_8, % 114.03/15.95 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_7, % 114.03/15.95 | v0) | (k2_isocat_1(all_49_7, v0, all_49_8, v1, all_81_0) = v2 & % 114.03/15.95 | $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.95 | (k2_isocat_1(all_49_7, v0, all_49_8, v1, all_81_0) = v2) | ~ % 114.03/15.95 | $i(v1) | ~ m2_cat_1(v1, all_49_7, v0) | (k11_isocat_2(all_49_7, % 114.03/15.95 | all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.95 | % 114.03/15.95 | GROUND_INST: instantiating (11) with all_49_8, all_49_8, all_49_7, all_81_0, % 114.03/15.95 | simplifying with (19), (20), (22), (23), (28), (29), (56) gives: % 114.03/15.95 | (111) ? [v0: $i] : (k11_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.95 | $i] : ! [v2: $i] : ( ~ (k11_isocat_2(all_49_8, all_49_8, % 114.03/15.95 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_8, % 114.03/15.95 | v0) | (k2_isocat_1(all_49_8, v0, all_49_8, v1, all_81_0) = v2 & % 114.03/15.95 | $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.95 | (k2_isocat_1(all_49_8, v0, all_49_8, v1, all_81_0) = v2) | ~ % 114.03/15.95 | $i(v1) | ~ m2_cat_1(v1, all_49_8, v0) | (k11_isocat_2(all_49_8, % 114.03/15.95 | all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.95 | % 114.03/15.95 | GROUND_INST: instantiating (11) with all_49_9, all_49_8, all_49_7, all_81_0, % 114.03/15.95 | simplifying with (18), (19), (20), (21), (22), (23), (27), (28), % 114.03/15.95 | (29), (56) gives: % 114.03/15.96 | (112) ? [v0: $i] : (k11_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.96 | $i] : ! [v2: $i] : ( ~ (k11_isocat_2(all_49_9, all_49_8, % 114.03/15.96 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_9, % 114.03/15.96 | v0) | (k2_isocat_1(all_49_9, v0, all_49_8, v1, all_81_0) = v2 & % 114.03/15.96 | $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.96 | (k2_isocat_1(all_49_9, v0, all_49_8, v1, all_81_0) = v2) | ~ % 114.03/15.96 | $i(v1) | ~ m2_cat_1(v1, all_49_9, v0) | (k11_isocat_2(all_49_9, % 114.03/15.96 | all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.96 | % 114.03/15.96 | GROUND_INST: instantiating (11) with all_49_6, all_49_8, all_49_7, all_81_0, % 114.03/15.96 | simplifying with (19), (20), (22), (23), (28), (29), (30), (44), % 114.03/15.96 | (45), (56) gives: % 114.03/15.96 | (113) ? [v0: $i] : (k11_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.96 | $i] : ! [v2: $i] : ( ~ (k11_isocat_2(all_49_6, all_49_8, % 114.03/15.96 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_6, % 114.03/15.96 | v0) | (k2_isocat_1(all_49_6, v0, all_49_8, v1, all_81_0) = v2 & % 114.03/15.96 | $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.96 | (k2_isocat_1(all_49_6, v0, all_49_8, v1, all_81_0) = v2) | ~ % 114.03/15.96 | $i(v1) | ~ m2_cat_1(v1, all_49_6, v0) | (k11_isocat_2(all_49_6, % 114.03/15.96 | all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.96 | % 114.03/15.96 | GROUND_INST: instantiating (13) with all_49_7, all_49_8, all_49_7, all_83_0, % 114.03/15.96 | simplifying with (19), (20), (22), (23), (28), (29), (59) gives: % 114.03/15.96 | (114) ? [v0: $i] : (k11_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.96 | $i] : ! [v2: $i] : ( ~ (k12_isocat_2(all_49_7, all_49_8, % 114.03/15.96 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_7, % 114.03/15.96 | v0) | (k2_isocat_1(all_49_7, v0, all_49_7, v1, all_83_0) = v2 & % 114.03/15.96 | $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.96 | (k2_isocat_1(all_49_7, v0, all_49_7, v1, all_83_0) = v2) | ~ % 114.03/15.96 | $i(v1) | ~ m2_cat_1(v1, all_49_7, v0) | (k12_isocat_2(all_49_7, % 114.03/15.96 | all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.96 | % 114.03/15.96 | GROUND_INST: instantiating (13) with all_49_8, all_49_8, all_49_7, all_83_0, % 114.03/15.96 | simplifying with (19), (20), (22), (23), (28), (29), (59) gives: % 114.03/15.96 | (115) ? [v0: $i] : (k11_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.96 | $i] : ! [v2: $i] : ( ~ (k12_isocat_2(all_49_8, all_49_8, % 114.03/15.96 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_8, % 114.03/15.96 | v0) | (k2_isocat_1(all_49_8, v0, all_49_7, v1, all_83_0) = v2 & % 114.03/15.96 | $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.96 | (k2_isocat_1(all_49_8, v0, all_49_7, v1, all_83_0) = v2) | ~ % 114.03/15.96 | $i(v1) | ~ m2_cat_1(v1, all_49_8, v0) | (k12_isocat_2(all_49_8, % 114.03/15.96 | all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.96 | % 114.03/15.96 | GROUND_INST: instantiating (13) with all_49_9, all_49_8, all_49_7, all_83_0, % 114.03/15.96 | simplifying with (18), (19), (20), (21), (22), (23), (27), (28), % 114.03/15.96 | (29), (59) gives: % 114.03/15.96 | (116) ? [v0: $i] : (k11_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.96 | $i] : ! [v2: $i] : ( ~ (k12_isocat_2(all_49_9, all_49_8, % 114.03/15.96 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_9, % 114.03/15.96 | v0) | (k2_isocat_1(all_49_9, v0, all_49_7, v1, all_83_0) = v2 & % 114.03/15.96 | $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.96 | (k2_isocat_1(all_49_9, v0, all_49_7, v1, all_83_0) = v2) | ~ % 114.03/15.96 | $i(v1) | ~ m2_cat_1(v1, all_49_9, v0) | (k12_isocat_2(all_49_9, % 114.03/15.96 | all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.96 | % 114.03/15.96 | GROUND_INST: instantiating (13) with all_49_6, all_49_8, all_49_7, all_83_0, % 114.03/15.96 | simplifying with (19), (20), (22), (23), (28), (29), (30), (44), % 114.03/15.96 | (45), (59) gives: % 114.03/15.96 | (117) ? [v0: $i] : (k11_cat_2(all_49_8, all_49_7) = v0 & $i(v0) & ! [v1: % 114.03/15.96 | $i] : ! [v2: $i] : ( ~ (k12_isocat_2(all_49_6, all_49_8, % 114.03/15.96 | all_49_7, v1) = v2) | ~ $i(v1) | ~ m2_cat_1(v1, all_49_6, % 114.03/15.96 | v0) | (k2_isocat_1(all_49_6, v0, all_49_7, v1, all_83_0) = v2 & % 114.03/15.96 | $i(v2))) & ! [v1: $i] : ! [v2: $i] : ( ~ % 114.03/15.96 | (k2_isocat_1(all_49_6, v0, all_49_7, v1, all_83_0) = v2) | ~ % 114.03/15.96 | $i(v1) | ~ m2_cat_1(v1, all_49_6, v0) | (k12_isocat_2(all_49_6, % 114.03/15.96 | all_49_8, all_49_7, v1) = v2 & $i(v2)))) % 114.03/15.96 | % 114.03/15.96 | GROUND_INST: instantiating (5) with all_49_8, all_49_7, all_83_0, simplifying % 114.03/15.96 | with (19), (20), (22), (23), (28), (29), (59) gives: % 114.03/15.96 | (118) k17_cat_2(all_49_8, all_49_7) = all_83_0 & $i(all_83_0) % 114.03/15.96 | % 114.03/15.96 | DELTA: instantiating (103) with fresh symbol all_139_0 gives: % 114.03/15.96 | (119) k8_isocat_2(all_49_8, all_49_7) = all_139_0 & $i(all_139_0) & ! [v0: % 114.03/15.96 | $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_6, all_49_8, all_49_7, % 114.03/15.96 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_6, all_49_6) | % 114.03/15.96 | (k2_isocat_1(all_49_6, all_49_6, all_49_8, v0, all_139_0) = v1 & % 114.03/15.96 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_6, % 114.03/15.96 | all_49_6, all_49_8, v0, all_139_0) = v1) | ~ $i(v0) | ~ % 114.03/15.96 | m2_cat_1(v0, all_49_6, all_49_6) | (k11_isocat_2(all_49_6, % 114.03/15.96 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.96 | % 114.03/15.96 | ALPHA: (119) implies: % 114.03/15.96 | (120) k8_isocat_2(all_49_8, all_49_7) = all_139_0 % 114.03/15.96 | % 114.03/15.96 | DELTA: instantiating (102) with fresh symbol all_142_0 gives: % 114.03/15.96 | (121) k9_isocat_2(all_49_8, all_49_7) = all_142_0 & $i(all_142_0) & ! [v0: % 114.03/15.96 | $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_6, all_49_8, all_49_7, % 114.03/15.96 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_6, all_49_6) | % 114.03/15.96 | (k2_isocat_1(all_49_6, all_49_6, all_49_7, v0, all_142_0) = v1 & % 114.03/15.96 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_6, % 114.03/15.96 | all_49_6, all_49_7, v0, all_142_0) = v1) | ~ $i(v0) | ~ % 114.03/15.96 | m2_cat_1(v0, all_49_6, all_49_6) | (k12_isocat_2(all_49_6, % 114.03/15.96 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.96 | % 114.03/15.96 | ALPHA: (121) implies: % 114.03/15.96 | (122) k9_isocat_2(all_49_8, all_49_7) = all_142_0 % 114.03/15.96 | % 114.03/15.96 | DELTA: instantiating (113) with fresh symbol all_145_0 gives: % 114.03/15.96 | (123) k11_cat_2(all_49_8, all_49_7) = all_145_0 & $i(all_145_0) & ! [v0: % 114.03/15.96 | $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_6, all_49_8, all_49_7, % 114.03/15.96 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_6, all_145_0) | % 114.03/15.96 | (k2_isocat_1(all_49_6, all_145_0, all_49_8, v0, all_81_0) = v1 & % 114.03/15.96 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_6, % 114.03/15.96 | all_145_0, all_49_8, v0, all_81_0) = v1) | ~ $i(v0) | ~ % 114.03/15.96 | m2_cat_1(v0, all_49_6, all_145_0) | (k11_isocat_2(all_49_6, % 114.03/15.96 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.96 | % 114.03/15.96 | ALPHA: (123) implies: % 114.03/15.96 | (124) $i(all_145_0) % 114.03/15.97 | (125) k11_cat_2(all_49_8, all_49_7) = all_145_0 % 114.03/15.97 | % 114.03/15.97 | DELTA: instantiating (112) with fresh symbol all_148_0 gives: % 114.03/15.97 | (126) k11_cat_2(all_49_8, all_49_7) = all_148_0 & $i(all_148_0) & ! [v0: % 114.03/15.97 | $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_9, all_49_8, all_49_7, % 114.03/15.97 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_9, all_148_0) | % 114.03/15.97 | (k2_isocat_1(all_49_9, all_148_0, all_49_8, v0, all_81_0) = v1 & % 114.03/15.97 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_9, % 114.03/15.97 | all_148_0, all_49_8, v0, all_81_0) = v1) | ~ $i(v0) | ~ % 114.03/15.97 | m2_cat_1(v0, all_49_9, all_148_0) | (k11_isocat_2(all_49_9, % 114.03/15.97 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.97 | % 114.03/15.97 | ALPHA: (126) implies: % 114.03/15.97 | (127) k11_cat_2(all_49_8, all_49_7) = all_148_0 % 114.03/15.97 | % 114.03/15.97 | DELTA: instantiating (111) with fresh symbol all_151_0 gives: % 114.03/15.97 | (128) k11_cat_2(all_49_8, all_49_7) = all_151_0 & $i(all_151_0) & ! [v0: % 114.03/15.97 | $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_8, all_49_8, all_49_7, % 114.03/15.97 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_8, all_151_0) | % 114.03/15.97 | (k2_isocat_1(all_49_8, all_151_0, all_49_8, v0, all_81_0) = v1 & % 114.03/15.97 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_8, % 114.03/15.97 | all_151_0, all_49_8, v0, all_81_0) = v1) | ~ $i(v0) | ~ % 114.03/15.97 | m2_cat_1(v0, all_49_8, all_151_0) | (k11_isocat_2(all_49_8, % 114.03/15.97 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.97 | % 114.03/15.97 | ALPHA: (128) implies: % 114.03/15.97 | (129) k11_cat_2(all_49_8, all_49_7) = all_151_0 % 114.03/15.97 | % 114.03/15.97 | DELTA: instantiating (116) with fresh symbol all_154_0 gives: % 114.03/15.97 | (130) k11_cat_2(all_49_8, all_49_7) = all_154_0 & $i(all_154_0) & ! [v0: % 114.03/15.97 | $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_9, all_49_8, all_49_7, % 114.03/15.97 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_9, all_154_0) | % 114.03/15.97 | (k2_isocat_1(all_49_9, all_154_0, all_49_7, v0, all_83_0) = v1 & % 114.03/15.97 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_9, % 114.03/15.97 | all_154_0, all_49_7, v0, all_83_0) = v1) | ~ $i(v0) | ~ % 114.03/15.97 | m2_cat_1(v0, all_49_9, all_154_0) | (k12_isocat_2(all_49_9, % 114.03/15.97 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.97 | % 114.03/15.97 | ALPHA: (130) implies: % 114.03/15.97 | (131) k11_cat_2(all_49_8, all_49_7) = all_154_0 % 114.03/15.97 | % 114.03/15.97 | DELTA: instantiating (115) with fresh symbol all_157_0 gives: % 114.03/15.97 | (132) k11_cat_2(all_49_8, all_49_7) = all_157_0 & $i(all_157_0) & ! [v0: % 114.03/15.97 | $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_8, all_49_8, all_49_7, % 114.03/15.97 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_8, all_157_0) | % 114.03/15.97 | (k2_isocat_1(all_49_8, all_157_0, all_49_7, v0, all_83_0) = v1 & % 114.03/15.97 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_8, % 114.03/15.97 | all_157_0, all_49_7, v0, all_83_0) = v1) | ~ $i(v0) | ~ % 114.03/15.97 | m2_cat_1(v0, all_49_8, all_157_0) | (k12_isocat_2(all_49_8, % 114.03/15.97 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.97 | % 114.03/15.97 | ALPHA: (132) implies: % 114.03/15.97 | (133) k11_cat_2(all_49_8, all_49_7) = all_157_0 % 114.03/15.97 | % 114.03/15.97 | DELTA: instantiating (110) with fresh symbol all_160_0 gives: % 114.03/15.97 | (134) k11_cat_2(all_49_8, all_49_7) = all_160_0 & $i(all_160_0) & ! [v0: % 114.03/15.97 | $i] : ! [v1: $i] : ( ~ (k11_isocat_2(all_49_7, all_49_8, all_49_7, % 114.03/15.97 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_7, all_160_0) | % 114.03/15.97 | (k2_isocat_1(all_49_7, all_160_0, all_49_8, v0, all_81_0) = v1 & % 114.03/15.97 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_7, % 114.03/15.97 | all_160_0, all_49_8, v0, all_81_0) = v1) | ~ $i(v0) | ~ % 114.03/15.97 | m2_cat_1(v0, all_49_7, all_160_0) | (k11_isocat_2(all_49_7, % 114.03/15.97 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.97 | % 114.03/15.97 | ALPHA: (134) implies: % 114.03/15.97 | (135) k11_cat_2(all_49_8, all_49_7) = all_160_0 % 114.03/15.97 | % 114.03/15.97 | DELTA: instantiating (117) with fresh symbol all_163_0 gives: % 114.03/15.97 | (136) k11_cat_2(all_49_8, all_49_7) = all_163_0 & $i(all_163_0) & ! [v0: % 114.03/15.97 | $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_6, all_49_8, all_49_7, % 114.03/15.97 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_6, all_163_0) | % 114.03/15.97 | (k2_isocat_1(all_49_6, all_163_0, all_49_7, v0, all_83_0) = v1 & % 114.03/15.97 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_6, % 114.03/15.97 | all_163_0, all_49_7, v0, all_83_0) = v1) | ~ $i(v0) | ~ % 114.03/15.97 | m2_cat_1(v0, all_49_6, all_163_0) | (k12_isocat_2(all_49_6, % 114.03/15.97 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.97 | % 114.03/15.97 | ALPHA: (136) implies: % 114.03/15.97 | (137) k11_cat_2(all_49_8, all_49_7) = all_163_0 % 114.03/15.97 | % 114.03/15.97 | DELTA: instantiating (114) with fresh symbol all_166_0 gives: % 114.03/15.97 | (138) k11_cat_2(all_49_8, all_49_7) = all_166_0 & $i(all_166_0) & ! [v0: % 114.03/15.97 | $i] : ! [v1: $i] : ( ~ (k12_isocat_2(all_49_7, all_49_8, all_49_7, % 114.03/15.97 | v0) = v1) | ~ $i(v0) | ~ m2_cat_1(v0, all_49_7, all_166_0) | % 114.03/15.97 | (k2_isocat_1(all_49_7, all_166_0, all_49_7, v0, all_83_0) = v1 & % 114.03/15.97 | $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_isocat_1(all_49_7, % 114.03/15.97 | all_166_0, all_49_7, v0, all_83_0) = v1) | ~ $i(v0) | ~ % 114.03/15.97 | m2_cat_1(v0, all_49_7, all_166_0) | (k12_isocat_2(all_49_7, % 114.03/15.97 | all_49_8, all_49_7, v0) = v1 & $i(v1))) % 114.03/15.97 | % 114.03/15.97 | ALPHA: (138) implies: % 114.03/15.97 | (139) k11_cat_2(all_49_8, all_49_7) = all_166_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (14) with all_49_6, all_151_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (33), (129) gives: % 114.03/15.97 | (140) all_151_0 = all_49_6 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (14) with all_151_0, all_154_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (129), (131) gives: % 114.03/15.97 | (141) all_154_0 = all_151_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (14) with all_154_0, all_157_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (131), (133) gives: % 114.03/15.97 | (142) all_157_0 = all_154_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (14) with all_157_0, all_163_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (133), (137) gives: % 114.03/15.97 | (143) all_163_0 = all_157_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (14) with all_148_0, all_163_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (127), (137) gives: % 114.03/15.97 | (144) all_163_0 = all_148_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (14) with all_160_0, all_166_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (135), (139) gives: % 114.03/15.97 | (145) all_166_0 = all_160_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (14) with all_151_0, all_166_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (129), (139) gives: % 114.03/15.97 | (146) all_166_0 = all_151_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (14) with all_145_0, all_166_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (125), (139) gives: % 114.03/15.97 | (147) all_166_0 = all_145_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (15) with all_81_0, all_139_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (56), (120) gives: % 114.03/15.97 | (148) all_139_0 = all_81_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (15) with all_85_0, all_139_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (107), (120) gives: % 114.03/15.97 | (149) all_139_0 = all_85_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (16) with all_83_0, all_142_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (59), (122) gives: % 114.03/15.97 | (150) all_142_0 = all_83_0 % 114.03/15.97 | % 114.03/15.97 | GROUND_INST: instantiating (16) with all_79_0, all_142_0, all_49_7, all_49_8, % 114.03/15.97 | simplifying with (109), (122) gives: % 114.03/15.97 | (151) all_142_0 = all_79_0 % 114.03/15.97 | % 114.03/15.97 | COMBINE_EQS: (145), (146) imply: % 114.03/15.97 | (152) all_160_0 = all_151_0 % 114.03/15.97 | % 114.03/15.97 | COMBINE_EQS: (145), (147) imply: % 114.03/15.97 | (153) all_160_0 = all_145_0 % 114.03/15.97 | % 114.03/15.97 | COMBINE_EQS: (143), (144) imply: % 114.03/15.97 | (154) all_157_0 = all_148_0 % 114.03/15.97 | % 114.03/15.97 | SIMP: (154) implies: % 114.03/15.97 | (155) all_157_0 = all_148_0 % 114.03/15.97 | % 114.03/15.97 | COMBINE_EQS: (152), (153) imply: % 114.03/15.98 | (156) all_151_0 = all_145_0 % 114.03/15.98 | % 114.03/15.98 | SIMP: (156) implies: % 114.03/15.98 | (157) all_151_0 = all_145_0 % 114.03/15.98 | % 114.03/15.98 | COMBINE_EQS: (142), (155) imply: % 114.03/15.98 | (158) all_154_0 = all_148_0 % 114.03/15.98 | % 114.03/15.98 | SIMP: (158) implies: % 114.03/15.98 | (159) all_154_0 = all_148_0 % 114.03/15.98 | % 114.03/15.98 | COMBINE_EQS: (141), (159) imply: % 114.03/15.98 | (160) all_151_0 = all_148_0 % 114.03/15.98 | % 114.03/15.98 | SIMP: (160) implies: % 114.03/15.98 | (161) all_151_0 = all_148_0 % 114.03/15.98 | % 114.03/15.98 | COMBINE_EQS: (140), (161) imply: % 114.03/15.98 | (162) all_148_0 = all_49_6 % 114.03/15.98 | % 114.03/15.98 | COMBINE_EQS: (157), (161) imply: % 114.03/15.98 | (163) all_148_0 = all_145_0 % 114.03/15.98 | % 114.03/15.98 | COMBINE_EQS: (162), (163) imply: % 114.03/15.98 | (164) all_145_0 = all_49_6 % 114.03/15.98 | % 114.03/15.98 | COMBINE_EQS: (150), (151) imply: % 114.03/15.98 | (165) all_83_0 = all_79_0 % 114.03/15.98 | % 114.03/15.98 | COMBINE_EQS: (148), (149) imply: % 114.03/15.98 | (166) all_85_0 = all_81_0 % 114.03/15.98 | % 114.03/15.98 | COMBINE_EQS: (97), (165) imply: % 114.03/15.98 | (167) all_100_0 = all_79_0 % 114.03/15.98 | % 114.03/15.98 | REDUCE: (98), (165) imply: % 114.03/15.98 | (168) k2_isocat_1(all_49_9, all_49_6, all_49_7, all_49_5, all_79_0) = % 114.03/15.98 | all_49_3 % 114.03/15.98 | % 114.03/15.98 | REDUCE: (104), (165) imply: % 114.03/15.98 | (169) r2_nattra_1(all_49_6, all_49_7, all_79_0, all_79_0) % 114.03/15.98 | % 114.03/15.98 | REDUCE: (105), (166) imply: % 114.03/15.98 | (170) r2_nattra_1(all_49_6, all_49_8, all_81_0, all_81_0) % 114.03/15.98 | % 114.03/15.98 | BETA: splitting (36) gives: % 114.03/15.98 | % 114.03/15.98 | Case 1: % 114.03/15.98 | | % 114.03/15.98 | | (171) k12_isocat_2(all_49_9, all_49_8, all_49_7, all_49_2) = all_49_0 & % 114.03/15.98 | | $i(all_49_0) & ~ r2_nattra_1(all_49_9, all_49_7, all_49_3, % 114.03/15.98 | | all_49_0) % 114.03/15.98 | | % 114.03/15.98 | | ALPHA: (171) implies: % 114.03/15.98 | | (172) ~ r2_nattra_1(all_49_9, all_49_7, all_49_3, all_49_0) % 114.03/15.98 | | (173) k12_isocat_2(all_49_9, all_49_8, all_49_7, all_49_2) = all_49_0 % 114.03/15.98 | | % 114.03/15.98 | | GROUND_INST: instantiating (79) with all_49_2, all_49_0, simplifying with % 114.03/15.98 | | (25), (32), (173) gives: % 114.03/15.98 | | (174) k2_isocat_1(all_49_9, all_49_6, all_49_7, all_49_2, all_100_0) = % 114.03/15.98 | | all_49_0 & $i(all_49_0) % 114.03/15.98 | | % 114.03/15.98 | | ALPHA: (174) implies: % 114.03/15.98 | | (175) k2_isocat_1(all_49_9, all_49_6, all_49_7, all_49_2, all_100_0) = % 114.03/15.98 | | all_49_0 % 114.03/15.98 | | % 114.03/15.98 | | REDUCE: (167), (175) imply: % 114.03/15.98 | | (176) k2_isocat_1(all_49_9, all_49_6, all_49_7, all_49_2, all_79_0) = % 114.03/15.98 | | all_49_0 % 114.03/15.98 | | % 114.03/15.98 | | GROUND_INST: instantiating (t27_isocat_1) with all_49_9, all_49_6, all_49_7, % 114.03/15.98 | | all_49_5, all_49_2, all_79_0, all_49_3, all_79_0, all_49_0, % 114.03/15.98 | | simplifying with (18), (20), (21), (23), (24), (25), (26), % 114.03/15.98 | | (27), (29), (30), (31), (32), (44), (45), (51), (52), (168), % 114.03/15.98 | | (169), (172), (176) gives: % 114.03/15.98 | | (177) $false % 114.03/15.98 | | % 114.03/15.98 | | CLOSE: (177) is inconsistent. % 114.03/15.98 | | % 114.03/15.98 | Case 2: % 114.03/15.98 | | % 114.03/15.98 | | (178) k11_isocat_2(all_49_9, all_49_8, all_49_7, all_49_2) = all_49_1 & % 114.03/15.98 | | $i(all_49_1) & ~ r2_nattra_1(all_49_9, all_49_8, all_49_4, % 114.03/15.98 | | all_49_1) % 114.03/15.98 | | % 114.03/15.98 | | ALPHA: (178) implies: % 114.03/15.98 | | (179) ~ r2_nattra_1(all_49_9, all_49_8, all_49_4, all_49_1) % 114.03/15.98 | | (180) k11_isocat_2(all_49_9, all_49_8, all_49_7, all_49_2) = all_49_1 % 114.03/15.98 | | % 114.03/15.98 | | BETA: splitting (39) gives: % 114.03/15.98 | | % 114.03/15.98 | | Case 1: % 114.03/15.98 | | | % 114.03/15.98 | | | % 114.03/15.98 | | | GROUND_INST: instantiating (72) with all_49_2, all_49_1, simplifying with % 114.03/15.98 | | | (25), (32), (180) gives: % 114.03/15.98 | | | (181) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_2, all_93_0) = % 114.03/15.98 | | | all_49_1 & $i(all_49_1) % 114.03/15.98 | | | % 114.03/15.98 | | | ALPHA: (181) implies: % 114.03/15.98 | | | (182) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_2, all_93_0) = % 114.03/15.98 | | | all_49_1 % 114.03/15.98 | | | % 114.03/15.98 | | | REDUCE: (95), (182) imply: % 114.03/15.98 | | | (183) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_2, all_81_0) = % 114.03/15.98 | | | all_49_1 % 114.03/15.98 | | | % 114.03/15.98 | | | GROUND_INST: instantiating (t27_isocat_1) with all_49_9, all_49_6, % 114.03/15.98 | | | all_49_8, all_49_5, all_49_2, all_81_0, all_49_4, all_81_0, % 114.03/15.98 | | | all_49_1, simplifying with (18), (19), (21), (22), (24), % 114.03/15.98 | | | (25), (26), (27), (28), (30), (31), (32), (44), (45), (55), % 114.03/15.98 | | | (99), (100), (170), (179), (183) gives: % 114.03/15.98 | | | (184) $false % 114.03/15.98 | | | % 114.03/15.98 | | | CLOSE: (184) is inconsistent. % 114.03/15.98 | | | % 114.03/15.98 | | Case 2: % 114.03/15.98 | | | % 114.03/15.98 | | | (185) k11_cat_2(all_49_8, all_49_8) = all_49_6 % 114.03/15.98 | | | % 114.03/15.98 | | | BETA: splitting (39) gives: % 114.03/15.98 | | | % 114.03/15.98 | | | Case 1: % 114.03/15.98 | | | | % 114.03/15.98 | | | | (186) ~ (k11_cat_2(all_49_8, all_49_8) = all_49_6) % 114.03/15.98 | | | | % 114.03/15.98 | | | | PRED_UNIFY: (185), (186) imply: % 114.03/15.98 | | | | (187) $false % 114.03/15.98 | | | | % 114.03/15.98 | | | | CLOSE: (187) is inconsistent. % 114.03/15.98 | | | | % 114.03/15.98 | | | Case 2: % 114.03/15.98 | | | | % 114.03/15.98 | | | | % 114.03/15.98 | | | | GROUND_INST: instantiating (72) with all_49_2, all_49_1, simplifying % 114.03/15.98 | | | | with (25), (32), (180) gives: % 114.47/15.98 | | | | (188) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_2, all_93_0) = % 114.47/15.98 | | | | all_49_1 & $i(all_49_1) % 114.47/15.98 | | | | % 114.47/15.98 | | | | ALPHA: (188) implies: % 114.47/15.98 | | | | (189) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_2, all_93_0) = % 114.47/15.98 | | | | all_49_1 % 114.47/15.98 | | | | % 114.47/15.98 | | | | REDUCE: (95), (189) imply: % 114.47/15.98 | | | | (190) k2_isocat_1(all_49_9, all_49_6, all_49_8, all_49_2, all_81_0) = % 114.47/15.98 | | | | all_49_1 % 114.47/15.98 | | | | % 114.47/15.98 | | | | GROUND_INST: instantiating (t27_isocat_1) with all_49_9, all_49_6, % 114.47/15.98 | | | | all_49_8, all_49_5, all_49_2, all_81_0, all_49_4, all_81_0, % 114.47/15.98 | | | | all_49_1, simplifying with (18), (19), (21), (22), (24), % 114.47/15.98 | | | | (25), (26), (27), (28), (30), (31), (32), (44), (45), (55), % 114.47/15.98 | | | | (99), (100), (170), (179), (190) gives: % 114.47/15.98 | | | | (191) $false % 114.47/15.98 | | | | % 114.47/15.98 | | | | CLOSE: (191) is inconsistent. % 114.47/15.98 | | | | % 114.47/15.98 | | | End of split % 114.47/15.98 | | | % 114.47/15.98 | | End of split % 114.47/15.98 | | % 114.47/15.98 | End of split % 114.47/15.98 | % 114.47/15.98 End of proof % 114.47/15.98 % SZS output end Proof for theBenchmark % 114.47/15.98 % 114.47/15.99 15372ms %------------------------------------------------------------------------------