%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ALG219+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 : n013.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 16:40:00 EDT 2023 % Result : Theorem 163.43s 22.75s % Output : Proof 164.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG219+1 : TPTP v8.1.2. Released v3.4.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n013.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon Aug 28 02:55:47 EDT 2023 % 0.12/0.33 % CPUTime : % 0.19/0.65 ________ _____ % 0.19/0.65 ___ __ \_________(_)________________________________ % 0.19/0.65 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.65 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.65 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.65 % 0.19/0.65 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.65 (2023-06-19) % 0.19/0.65 % 0.19/0.65 (c) Philipp Rümmer, 2009-2023 % 0.19/0.65 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.65 Amanda Stjerna. % 0.19/0.65 Free software under BSD-3-Clause. % 0.19/0.65 % 0.19/0.65 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.65 % 0.19/0.65 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.67 Running up to 7 provers in parallel. % 0.19/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.43/1.55 Prover 4: Preprocessing ... % 4.43/1.55 Prover 1: Preprocessing ... % 5.12/1.61 Prover 0: Preprocessing ... % 5.12/1.61 Prover 3: Preprocessing ... % 5.12/1.61 Prover 2: Preprocessing ... % 5.17/1.62 Prover 6: Preprocessing ... % 5.17/1.62 Prover 5: Preprocessing ... % 14.81/2.98 Prover 1: Warning: ignoring some quantifiers % 15.26/3.02 Prover 5: Proving ... % 15.26/3.05 Prover 3: Warning: ignoring some quantifiers % 15.63/3.08 Prover 1: Constructing countermodel ... % 15.63/3.10 Prover 3: Constructing countermodel ... % 16.54/3.21 Prover 6: Proving ... % 16.91/3.29 Prover 2: Proving ... % 59.46/8.97 Prover 4: Warning: ignoring some quantifiers % 60.19/9.07 Prover 4: Constructing countermodel ... % 60.19/9.27 Prover 0: Proving ... % 79.12/11.74 Prover 2: stopped % 79.12/11.76 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 82.20/11.90 Prover 7: Preprocessing ... % 83.65/12.16 Prover 7: Warning: ignoring some quantifiers % 84.55/12.21 Prover 7: Constructing countermodel ... % 98.20/14.03 Prover 5: stopped % 98.20/14.03 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 98.20/14.17 Prover 8: Preprocessing ... % 100.74/14.41 Prover 8: Warning: ignoring some quantifiers % 100.74/14.42 Prover 8: Constructing countermodel ... % 111.51/16.03 Prover 1: stopped % 113.56/16.06 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 114.91/16.22 Prover 9: Preprocessing ... % 127.59/17.94 Prover 6: stopped % 127.80/17.94 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 128.87/18.10 Prover 10: Preprocessing ... % 129.45/18.22 Prover 10: Warning: ignoring some quantifiers % 129.45/18.23 Prover 10: Constructing countermodel ... % 148.28/20.89 Prover 9: Warning: ignoring some quantifiers % 151.14/21.08 Prover 9: Constructing countermodel ... % 163.43/22.73 Prover 7: Found proof (size 87) % 163.43/22.74 Prover 7: proved (10801ms) % 163.43/22.74 Prover 9: stopped % 163.43/22.74 Prover 3: stopped % 163.43/22.74 Prover 8: stopped % 163.43/22.74 Prover 0: stopped % 163.43/22.75 Prover 4: stopped % 163.43/22.75 Prover 10: stopped % 163.43/22.75 % 163.43/22.75 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 163.43/22.75 % 163.43/22.77 % SZS output start Proof for theBenchmark % 163.79/22.78 Assumptions after simplification: % 163.79/22.78 --------------------------------- % 163.79/22.78 % 163.79/22.78 (abstractness_v3_vectsp_2) % 163.79/22.82 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (u1_vectsp_2(v0, v1) = v2) | ~ % 163.79/22.82 $i(v1) | ~ $i(v0) | ~ l1_struct_0(v0) | ~ l1_vectsp_2(v1, v0) | ~ % 163.79/22.82 v3_vectsp_2(v1, v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 163.79/22.82 (u1_struct_0(v1) = v3 & u1_rlvect_1(v1) = v4 & u2_struct_0(v1) = v5 & % 163.79/22.82 g1_vectsp_2(v0, v3, v4, v5, v2) = v1 & $i(v5) & $i(v4) & $i(v3))) % 163.79/22.82 % 163.79/22.82 (d4_rmod_2) % 163.79/22.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k2_rmod_2(v0, v1) = v2) | ~ % 163.79/22.85 $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, v0) | ~ % 163.79/22.85 l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) | ~ % 163.79/22.85 v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 163.79/22.85 v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 163.79/22.85 v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 163.79/22.85 v3_rlvect_1(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v3: $i] : ? [v4: % 163.79/22.85 $i] : ? [v5: $i] : ? [v6: $i] : (u1_vectsp_2(v0, v1) = v6 & % 163.79/22.85 u1_struct_0(v1) = v3 & u1_rlvect_1(v1) = v4 & u2_struct_0(v1) = v5 & % 163.79/22.85 g1_vectsp_2(v0, v3, v4, v5, v6) = v2 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 163.79/22.85 $i(v2))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (u1_vectsp_2(v0, % 163.79/22.85 v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ % 163.79/22.85 v5_vectsp_2(v1, v0) | ~ l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ % 163.79/22.85 v7_vectsp_1(v0) | ~ v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ % 163.79/22.85 v6_rlvect_1(v1) | ~ v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ % 163.79/22.86 v5_rlvect_1(v0) | ~ v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ % 163.79/22.86 v3_rlvect_1(v1) | ~ v3_rlvect_1(v0) | v3_struct_0(v1) | v3_struct_0(v0) | % 163.79/22.86 ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : (k2_rmod_2(v0, v1) = % 164.18/22.86 v3 & u1_struct_0(v1) = v4 & u1_rlvect_1(v1) = v5 & u2_struct_0(v1) = v6 & % 164.18/22.86 g1_vectsp_2(v0, v4, v5, v6, v2) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 164.18/22.86 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (u1_struct_0(v1) = v2) | ~ % 164.18/22.86 $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, v0) | ~ % 164.18/22.86 l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) | ~ % 164.18/22.86 v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 164.18/22.86 v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 164.18/22.86 v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 164.18/22.86 v3_rlvect_1(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v3: $i] : ? [v4: % 164.18/22.86 $i] : ? [v5: $i] : ? [v6: $i] : (k2_rmod_2(v0, v1) = v3 & % 164.18/22.86 u1_vectsp_2(v0, v1) = v6 & u1_rlvect_1(v1) = v4 & u2_struct_0(v1) = v5 & % 164.18/22.86 g1_vectsp_2(v0, v2, v4, v5, v6) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 164.18/22.86 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (u1_rlvect_1(v1) = v2) | ~ % 164.18/22.86 $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, v0) | ~ % 164.18/22.86 l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) | ~ % 164.18/22.86 v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 164.18/22.86 v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 164.18/22.86 v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 164.18/22.86 v3_rlvect_1(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v3: $i] : ? [v4: % 164.18/22.86 $i] : ? [v5: $i] : ? [v6: $i] : (k2_rmod_2(v0, v1) = v3 & % 164.18/22.86 u1_vectsp_2(v0, v1) = v6 & u1_struct_0(v1) = v4 & u2_struct_0(v1) = v5 & % 164.18/22.86 g1_vectsp_2(v0, v4, v2, v5, v6) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 164.18/22.86 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (u2_struct_0(v1) = v2) | ~ % 164.18/22.86 $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, v0) | ~ % 164.18/22.86 l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) | ~ % 164.18/22.86 v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 164.18/22.86 v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 164.18/22.86 v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 164.18/22.86 v3_rlvect_1(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v3: $i] : ? [v4: % 164.18/22.86 $i] : ? [v5: $i] : ? [v6: $i] : (k2_rmod_2(v0, v1) = v3 & % 164.18/22.86 u1_vectsp_2(v0, v1) = v6 & u1_struct_0(v1) = v4 & u1_rlvect_1(v1) = v5 & % 164.18/22.86 g1_vectsp_2(v0, v4, v5, v2, v6) = v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 164.18/22.86 % 164.18/22.86 (dt_k2_rmod_2) % 164.18/22.87 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k2_rmod_2(v0, v1) = v2) | ~ % 164.18/22.87 $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, v0) | ~ % 164.18/22.87 l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) | ~ % 164.18/22.87 v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 164.18/22.87 v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 164.18/22.87 v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 164.18/22.87 v3_rlvect_1(v0) | m1_rmod_2(v2, v0, v1) | v3_struct_0(v1) | v3_struct_0(v0)) % 164.18/22.87 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k2_rmod_2(v0, v1) = v2) | ~ % 164.18/22.87 $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, v0) | ~ % 164.18/22.87 l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) | ~ % 164.18/22.87 v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 164.18/22.87 v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 164.18/22.87 v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 164.18/22.87 v3_rlvect_1(v0) | v3_vectsp_2(v2, v0) | v3_struct_0(v1) | v3_struct_0(v0)) % 164.18/22.87 % 164.18/22.87 (dt_l1_vectsp_2) % 164.18/22.87 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ l1_struct_0(v0) | ~ % 164.18/22.87 l1_vectsp_2(v1, v0) | l1_rlvect_1(v1)) % 164.18/22.87 % 164.18/22.87 (dt_l2_struct_0) % 164.18/22.87 ! [v0: $i] : ( ~ $i(v0) | ~ l2_struct_0(v0) | l1_struct_0(v0)) % 164.18/22.87 % 164.18/22.87 (dt_l2_vectsp_1) % 164.18/22.87 ! [v0: $i] : ( ~ $i(v0) | ~ l2_vectsp_1(v0) | l2_struct_0(v0)) & ! [v0: $i] % 164.18/22.87 : ( ~ $i(v0) | ~ l2_vectsp_1(v0) | l1_vectsp_1(v0)) % 164.18/22.87 % 164.18/22.87 (dt_l3_vectsp_1) % 164.18/22.87 ! [v0: $i] : ( ~ $i(v0) | ~ l3_vectsp_1(v0) | l2_vectsp_1(v0)) & ! [v0: $i] % 164.18/22.87 : ( ~ $i(v0) | ~ l3_vectsp_1(v0) | l1_rlvect_1(v0)) % 164.18/22.87 % 164.18/22.87 (dt_u1_rlvect_1) % 164.18/22.88 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 164.18/22.88 l1_rlvect_1(v0) | ? [v2: $i] : ? [v3: $i] : (k2_zfmisc_1(v1, v1) = v3 & % 164.18/22.88 u1_rlvect_1(v0) = v2 & $i(v3) & $i(v2) & m2_relset_1(v2, v3, v1) & % 164.18/22.88 v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) & ! [v0: $i] : ! [v1: $i] : ( % 164.18/22.88 ~ (u1_rlvect_1(v0) = v1) | ~ $i(v0) | ~ l1_rlvect_1(v0) | v1_funct_1(v1)) % 164.18/22.88 & ! [v0: $i] : ! [v1: $i] : ( ~ (u1_rlvect_1(v0) = v1) | ~ $i(v0) | ~ % 164.18/22.88 l1_rlvect_1(v0) | ? [v2: $i] : ? [v3: $i] : (k2_zfmisc_1(v2, v2) = v3 & % 164.18/22.88 u1_struct_0(v0) = v2 & $i(v3) & $i(v2) & m2_relset_1(v1, v3, v2) & % 164.18/22.88 v1_funct_2(v1, v3, v2))) % 164.18/22.88 % 164.18/22.88 (dt_u1_vectsp_2) % 164.30/22.89 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 164.30/22.89 (k2_zfmisc_1(v2, v3) = v4) | ~ (u1_struct_0(v1) = v2) | ~ (u1_struct_0(v0) % 164.30/22.89 = v3) | ~ $i(v1) | ~ $i(v0) | ~ l1_struct_0(v0) | ~ l1_vectsp_2(v1, % 164.30/22.89 v0) | ? [v5: $i] : (u1_vectsp_2(v0, v1) = v5 & $i(v5) & m2_relset_1(v5, % 164.30/22.89 v4, v2) & v1_funct_2(v5, v4, v2) & v1_funct_1(v5))) & ! [v0: $i] : ! % 164.30/22.89 [v1: $i] : ! [v2: $i] : ( ~ (u1_vectsp_2(v0, v1) = v2) | ~ $i(v1) | ~ % 164.30/22.89 $i(v0) | ~ l1_struct_0(v0) | ~ l1_vectsp_2(v1, v0) | v1_funct_1(v2)) & ! % 164.30/22.89 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (u1_vectsp_2(v0, v1) = v2) | ~ % 164.30/22.89 $i(v1) | ~ $i(v0) | ~ l1_struct_0(v0) | ~ l1_vectsp_2(v1, v0) | ? [v3: % 164.30/22.89 $i] : ? [v4: $i] : ? [v5: $i] : (k2_zfmisc_1(v3, v4) = v5 & % 164.30/22.89 u1_struct_0(v1) = v3 & u1_struct_0(v0) = v4 & $i(v5) & $i(v4) & $i(v3) & % 164.30/22.89 m2_relset_1(v2, v5, v3) & v1_funct_2(v2, v5, v3))) % 164.30/22.89 % 164.30/22.89 (t13_rmod_5) % 164.30/22.90 ! [v0: $i] : ! [v1: $i] : ( ~ (k2_group_1(v0) = v1) | ~ $i(v0) | ~ % 164.30/22.90 l3_vectsp_1(v0) | ~ v2_vectsp_2(v0) | ~ v8_vectsp_1(v0) | ~ % 164.30/22.90 v7_vectsp_1(v0) | ~ v6_vectsp_1(v0) | ~ v7_group_1(v0) | ~ v4_group_1(v0) % 164.30/22.90 | ~ v6_rlvect_1(v0) | ~ v5_rlvect_1(v0) | ~ v4_rlvect_1(v0) | ~ % 164.30/22.90 v3_rlvect_1(v0) | v10_vectsp_1(v0) | v3_struct_0(v0) | ? [v2: $i] : % 164.30/22.90 (k1_rlvect_1(v0) = v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ( ~ % 164.30/22.90 (u1_struct_0(v3) = v4) | ~ $i(v3) | ~ l1_vectsp_2(v3, v0) | ~ % 164.30/22.90 v5_vectsp_2(v3, v0) | ~ v6_rlvect_1(v3) | ~ v5_rlvect_1(v3) | ~ % 164.30/22.90 v4_rlvect_1(v3) | ~ v3_rlvect_1(v3) | v3_struct_0(v3) | ? [v5: $i] : % 164.30/22.90 (k1_zfmisc_1(v4) = v5 & $i(v5) & ! [v6: $i] : ! [v7: $i] : ! [v8: $i] % 164.30/22.90 : (v8 = v7 | v2 = v1 | ~ (k1_rmod_5(v0, v3, v6) = v7) | ~ % 164.30/22.90 (u1_struct_0(v8) = v6) | ~ $i(v8) | ~ $i(v6) | ~ m1_rmod_2(v8, % 164.30/22.90 v0, v3) | ~ m1_subset_1(v6, v5) | ~ v3_vectsp_2(v8, v0)))))) & % 164.30/22.90 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_rlvect_1(v0) = v1) | ~ $i(v0) | ~ % 164.30/22.90 l3_vectsp_1(v0) | ~ v2_vectsp_2(v0) | ~ v8_vectsp_1(v0) | ~ % 164.30/22.90 v7_vectsp_1(v0) | ~ v6_vectsp_1(v0) | ~ v7_group_1(v0) | ~ v4_group_1(v0) % 164.30/22.90 | ~ v6_rlvect_1(v0) | ~ v5_rlvect_1(v0) | ~ v4_rlvect_1(v0) | ~ % 164.30/22.90 v3_rlvect_1(v0) | v10_vectsp_1(v0) | v3_struct_0(v0) | ? [v2: $i] : % 164.30/22.90 (k2_group_1(v0) = v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ( ~ % 164.30/22.90 (u1_struct_0(v3) = v4) | ~ $i(v3) | ~ l1_vectsp_2(v3, v0) | ~ % 164.30/22.90 v5_vectsp_2(v3, v0) | ~ v6_rlvect_1(v3) | ~ v5_rlvect_1(v3) | ~ % 164.30/22.90 v4_rlvect_1(v3) | ~ v3_rlvect_1(v3) | v3_struct_0(v3) | ? [v5: $i] : % 164.30/22.90 (k1_zfmisc_1(v4) = v5 & $i(v5) & ! [v6: $i] : ! [v7: $i] : ! [v8: $i] % 164.30/22.90 : (v8 = v7 | v2 = v1 | ~ (k1_rmod_5(v0, v3, v6) = v7) | ~ % 164.30/22.90 (u1_struct_0(v8) = v6) | ~ $i(v8) | ~ $i(v6) | ~ m1_rmod_2(v8, % 164.30/22.90 v0, v3) | ~ m1_subset_1(v6, v5) | ~ v3_vectsp_2(v8, v0)))))) % 164.30/22.90 % 164.30/22.90 (t14_rmod_5) % 164.30/22.90 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 164.30/22.90 $i] : ? [v6: $i] : ( ~ (v6 = v3) & ~ (v2 = v1) & k2_group_1(v0) = v2 & % 164.30/22.90 k1_rmod_5(v0, v3, v4) = v6 & k1_rlvect_1(v0) = v1 & k1_zfmisc_1(v4) = v5 & % 164.30/22.90 u1_struct_0(v3) = v4 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 164.30/22.90 $i(v0) & m1_subset_1(v4, v5) & l1_vectsp_2(v3, v0) & v5_vectsp_2(v3, v0) & % 164.30/22.90 v3_vectsp_2(v3, v0) & l3_vectsp_1(v0) & v2_vectsp_2(v0) & v8_vectsp_1(v0) & % 164.30/22.90 v7_vectsp_1(v0) & v6_vectsp_1(v0) & v7_group_1(v0) & v4_group_1(v0) & % 164.30/22.90 v6_rlvect_1(v3) & v6_rlvect_1(v0) & v5_rlvect_1(v3) & v5_rlvect_1(v0) & % 164.30/22.90 v4_rlvect_1(v3) & v4_rlvect_1(v0) & v3_rlvect_1(v3) & v3_rlvect_1(v0) & ~ % 164.30/22.90 v10_vectsp_1(v0) & ~ v3_struct_0(v3) & ~ v3_struct_0(v0)) % 164.30/22.90 % 164.30/22.90 (function-axioms) % 164.30/22.91 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 164.30/22.91 $i] : ! [v6: $i] : (v1 = v0 | ~ (g1_vectsp_2(v6, v5, v4, v3, v2) = v1) | % 164.30/22.91 ~ (g1_vectsp_2(v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 164.30/22.91 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (k1_rmod_5(v4, v3, v2) = % 164.30/22.91 v1) | ~ (k1_rmod_5(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 164.30/22.91 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (k2_rmod_2(v3, v2) = v1) | ~ % 164.30/22.91 (k2_rmod_2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 164.30/22.91 [v3: $i] : (v1 = v0 | ~ (k2_zfmisc_1(v3, v2) = v1) | ~ (k2_zfmisc_1(v3, v2) % 164.30/22.91 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 164.30/22.91 | ~ (u1_vectsp_2(v3, v2) = v1) | ~ (u1_vectsp_2(v3, v2) = v0)) & ! [v0: % 164.30/22.91 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k2_group_1(v2) = v1) | ~ % 164.30/22.91 (k2_group_1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 164.30/22.91 | ~ (k1_rlvect_1(v2) = v1) | ~ (k1_rlvect_1(v2) = v0)) & ! [v0: $i] : ! % 164.30/22.91 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k1_zfmisc_1(v2) = v1) | ~ % 164.30/22.91 (k1_zfmisc_1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 164.30/22.91 | ~ (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) & ! [v0: $i] : ! % 164.30/22.91 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (u1_rlvect_1(v2) = v1) | ~ % 164.30/22.91 (u1_rlvect_1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 164.30/22.91 | ~ (u2_struct_0(v2) = v1) | ~ (u2_struct_0(v2) = v0)) % 164.30/22.91 % 164.30/22.91 Further assumptions not needed in the proof: % 164.30/22.91 -------------------------------------------- % 164.30/22.91 antisymmetry_r2_hidden, cc1_relset_1, cc2_vectsp_2, cc3_vectsp_2, % 164.30/22.91 dt_g1_vectsp_2, dt_k1_rlvect_1, dt_k1_rmod_5, dt_k1_xboole_0, dt_k1_zfmisc_1, % 164.30/22.91 dt_k2_group_1, dt_k2_zfmisc_1, dt_l1_group_1, dt_l1_rlvect_1, dt_l1_struct_0, % 164.30/22.91 dt_l1_vectsp_1, dt_m1_relset_1, dt_m1_rmod_2, dt_m1_subset_1, dt_m2_relset_1, % 164.30/22.91 dt_u1_struct_0, dt_u2_struct_0, existence_l1_group_1, existence_l1_rlvect_1, % 164.30/22.91 existence_l1_struct_0, existence_l1_vectsp_1, existence_l1_vectsp_2, % 164.30/22.91 existence_l2_struct_0, existence_l2_vectsp_1, existence_l3_vectsp_1, % 164.30/22.91 existence_m1_relset_1, existence_m1_rmod_2, existence_m1_subset_1, % 164.30/22.91 existence_m2_relset_1, fc1_struct_0, fc1_subset_1, fc1_vectsp_2, fc1_xboole_0, % 164.30/22.91 fc4_subset_1, free_g1_vectsp_2, rc13_vectsp_2, rc16_vectsp_2, rc1_rmod_2, % 164.30/22.91 rc1_subset_1, rc1_xboole_0, rc2_subset_1, rc2_xboole_0, rc3_struct_0, % 164.30/22.91 rc4_struct_0, rc5_struct_0, rc8_vectsp_2, rc9_vectsp_2, % 164.30/22.91 redefinition_m2_relset_1, reflexivity_r1_tarski, t1_subset, t2_subset, % 164.30/22.91 t3_subset, t4_subset, t5_subset, t6_boole, t7_boole, t8_boole % 164.30/22.91 % 164.30/22.91 Those formulas are unsatisfiable: % 164.30/22.91 --------------------------------- % 164.30/22.91 % 164.30/22.91 Begin of proof % 164.30/22.92 | % 164.30/22.92 | ALPHA: (d4_rmod_2) implies: % 164.30/22.92 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (u1_struct_0(v1) = v2) | % 164.30/22.92 | ~ $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, % 164.30/22.92 | v0) | ~ l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) % 164.30/22.92 | | ~ v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 164.30/22.92 | v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 164.30/22.92 | v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 164.30/22.92 | v3_rlvect_1(v0) | v3_struct_0(v1) | v3_struct_0(v0) | ? [v3: $i] : % 164.30/22.92 | ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : (k2_rmod_2(v0, v1) = v3 & % 164.30/22.92 | u1_vectsp_2(v0, v1) = v6 & u1_rlvect_1(v1) = v4 & u2_struct_0(v1) = % 164.30/22.92 | v5 & g1_vectsp_2(v0, v2, v4, v5, v6) = v3 & $i(v6) & $i(v5) & % 164.30/22.92 | $i(v4) & $i(v3))) % 164.30/22.92 | % 164.30/22.92 | ALPHA: (dt_k2_rmod_2) implies: % 164.30/22.94 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k2_rmod_2(v0, v1) = v2) % 164.30/22.94 | | ~ $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, % 164.30/22.94 | v0) | ~ l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) % 164.30/22.94 | | ~ v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 164.30/22.94 | v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 164.30/22.94 | v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 164.30/22.94 | v3_rlvect_1(v0) | v3_vectsp_2(v2, v0) | v3_struct_0(v1) | % 164.30/22.94 | v3_struct_0(v0)) % 164.30/22.94 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k2_rmod_2(v0, v1) = v2) % 164.30/22.94 | | ~ $i(v1) | ~ $i(v0) | ~ l1_vectsp_2(v1, v0) | ~ v5_vectsp_2(v1, % 164.30/22.94 | v0) | ~ l3_vectsp_1(v0) | ~ v8_vectsp_1(v0) | ~ v7_vectsp_1(v0) % 164.30/22.94 | | ~ v6_vectsp_1(v0) | ~ v4_group_1(v0) | ~ v6_rlvect_1(v1) | ~ % 164.30/22.94 | v6_rlvect_1(v0) | ~ v5_rlvect_1(v1) | ~ v5_rlvect_1(v0) | ~ % 164.30/22.94 | v4_rlvect_1(v1) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v1) | ~ % 164.30/22.94 | v3_rlvect_1(v0) | m1_rmod_2(v2, v0, v1) | v3_struct_0(v1) | % 164.30/22.94 | v3_struct_0(v0)) % 164.30/22.94 | % 164.30/22.94 | ALPHA: (dt_l2_vectsp_1) implies: % 164.30/22.94 | (4) ! [v0: $i] : ( ~ $i(v0) | ~ l2_vectsp_1(v0) | l2_struct_0(v0)) % 164.30/22.94 | % 164.30/22.94 | ALPHA: (dt_l3_vectsp_1) implies: % 164.30/22.94 | (5) ! [v0: $i] : ( ~ $i(v0) | ~ l3_vectsp_1(v0) | l2_vectsp_1(v0)) % 164.30/22.94 | % 164.30/22.94 | ALPHA: (dt_u1_rlvect_1) implies: % 164.30/22.94 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_rlvect_1(v0) = v1) | ~ $i(v0) | ~ % 164.30/22.94 | l1_rlvect_1(v0) | ? [v2: $i] : ? [v3: $i] : (k2_zfmisc_1(v2, v2) = % 164.30/22.94 | v3 & u1_struct_0(v0) = v2 & $i(v3) & $i(v2) & m2_relset_1(v1, v3, % 164.30/22.94 | v2) & v1_funct_2(v1, v3, v2))) % 164.30/22.94 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 164.30/22.94 | l1_rlvect_1(v0) | ? [v2: $i] : ? [v3: $i] : (k2_zfmisc_1(v1, v1) = % 164.30/22.94 | v3 & u1_rlvect_1(v0) = v2 & $i(v3) & $i(v2) & m2_relset_1(v2, v3, % 164.30/22.94 | v1) & v1_funct_2(v2, v3, v1) & v1_funct_1(v2))) % 164.30/22.94 | % 164.30/22.94 | ALPHA: (dt_u1_vectsp_2) implies: % 164.30/22.95 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (u1_vectsp_2(v0, v1) = % 164.30/22.95 | v2) | ~ $i(v1) | ~ $i(v0) | ~ l1_struct_0(v0) | ~ % 164.30/22.95 | l1_vectsp_2(v1, v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 164.30/22.95 | (k2_zfmisc_1(v3, v4) = v5 & u1_struct_0(v1) = v3 & u1_struct_0(v0) = % 164.30/22.95 | v4 & $i(v5) & $i(v4) & $i(v3) & m2_relset_1(v2, v5, v3) & % 164.30/22.95 | v1_funct_2(v2, v5, v3))) % 164.30/22.95 | % 164.30/22.95 | ALPHA: (t13_rmod_5) implies: % 164.30/22.95 | (9) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_rlvect_1(v0) = v1) | ~ $i(v0) | ~ % 164.30/22.95 | l3_vectsp_1(v0) | ~ v2_vectsp_2(v0) | ~ v8_vectsp_1(v0) | ~ % 164.30/22.95 | v7_vectsp_1(v0) | ~ v6_vectsp_1(v0) | ~ v7_group_1(v0) | ~ % 164.30/22.95 | v4_group_1(v0) | ~ v6_rlvect_1(v0) | ~ v5_rlvect_1(v0) | ~ % 164.30/22.95 | v4_rlvect_1(v0) | ~ v3_rlvect_1(v0) | v10_vectsp_1(v0) | % 164.30/22.95 | v3_struct_0(v0) | ? [v2: $i] : (k2_group_1(v0) = v2 & $i(v2) & ! % 164.30/22.95 | [v3: $i] : ! [v4: $i] : ( ~ (u1_struct_0(v3) = v4) | ~ $i(v3) | % 164.30/22.95 | ~ l1_vectsp_2(v3, v0) | ~ v5_vectsp_2(v3, v0) | ~ % 164.30/22.95 | v6_rlvect_1(v3) | ~ v5_rlvect_1(v3) | ~ v4_rlvect_1(v3) | ~ % 164.30/22.95 | v3_rlvect_1(v3) | v3_struct_0(v3) | ? [v5: $i] : % 164.30/22.95 | (k1_zfmisc_1(v4) = v5 & $i(v5) & ! [v6: $i] : ! [v7: $i] : ! % 164.30/22.95 | [v8: $i] : (v8 = v7 | v2 = v1 | ~ (k1_rmod_5(v0, v3, v6) = v7) % 164.30/22.95 | | ~ (u1_struct_0(v8) = v6) | ~ $i(v8) | ~ $i(v6) | ~ % 164.30/22.95 | m1_rmod_2(v8, v0, v3) | ~ m1_subset_1(v6, v5) | ~ % 164.30/22.95 | v3_vectsp_2(v8, v0)))))) % 164.30/22.96 | (10) ! [v0: $i] : ! [v1: $i] : ( ~ (k2_group_1(v0) = v1) | ~ $i(v0) | ~ % 164.30/22.96 | l3_vectsp_1(v0) | ~ v2_vectsp_2(v0) | ~ v8_vectsp_1(v0) | ~ % 164.30/22.96 | v7_vectsp_1(v0) | ~ v6_vectsp_1(v0) | ~ v7_group_1(v0) | ~ % 164.30/22.96 | v4_group_1(v0) | ~ v6_rlvect_1(v0) | ~ v5_rlvect_1(v0) | ~ % 164.30/22.96 | v4_rlvect_1(v0) | ~ v3_rlvect_1(v0) | v10_vectsp_1(v0) | % 164.30/22.96 | v3_struct_0(v0) | ? [v2: $i] : (k1_rlvect_1(v0) = v2 & $i(v2) & ! % 164.30/22.96 | [v3: $i] : ! [v4: $i] : ( ~ (u1_struct_0(v3) = v4) | ~ $i(v3) | % 164.30/22.96 | ~ l1_vectsp_2(v3, v0) | ~ v5_vectsp_2(v3, v0) | ~ % 164.30/22.96 | v6_rlvect_1(v3) | ~ v5_rlvect_1(v3) | ~ v4_rlvect_1(v3) | ~ % 164.30/22.96 | v3_rlvect_1(v3) | v3_struct_0(v3) | ? [v5: $i] : % 164.30/22.96 | (k1_zfmisc_1(v4) = v5 & $i(v5) & ! [v6: $i] : ! [v7: $i] : ! % 164.30/22.96 | [v8: $i] : (v8 = v7 | v2 = v1 | ~ (k1_rmod_5(v0, v3, v6) = % 164.30/22.96 | v7) | ~ (u1_struct_0(v8) = v6) | ~ $i(v8) | ~ $i(v6) | % 164.30/22.96 | ~ m1_rmod_2(v8, v0, v3) | ~ m1_subset_1(v6, v5) | ~ % 164.30/22.96 | v3_vectsp_2(v8, v0)))))) % 164.30/22.96 | % 164.30/22.96 | ALPHA: (function-axioms) implies: % 164.30/22.96 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 164.30/22.96 | (u2_struct_0(v2) = v1) | ~ (u2_struct_0(v2) = v0)) % 164.30/22.96 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 164.30/22.96 | (u1_rlvect_1(v2) = v1) | ~ (u1_rlvect_1(v2) = v0)) % 164.30/22.96 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 164.30/22.96 | (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) % 164.30/22.96 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 164.30/22.96 | (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) % 164.30/22.97 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 164.30/22.97 | (k1_rlvect_1(v2) = v1) | ~ (k1_rlvect_1(v2) = v0)) % 164.30/22.97 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 164.30/22.97 | ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (g1_vectsp_2(v6, v5, v4, v3, % 164.30/22.97 | v2) = v1) | ~ (g1_vectsp_2(v6, v5, v4, v3, v2) = v0)) % 164.30/22.97 | % 164.30/22.97 | DELTA: instantiating (t14_rmod_5) with fresh symbols all_78_0, all_78_1, % 164.30/22.97 | all_78_2, all_78_3, all_78_4, all_78_5, all_78_6 gives: % 164.30/22.97 | (17) ~ (all_78_0 = all_78_3) & ~ (all_78_4 = all_78_5) & % 164.30/22.97 | k2_group_1(all_78_6) = all_78_4 & k1_rmod_5(all_78_6, all_78_3, % 164.30/22.97 | all_78_2) = all_78_0 & k1_rlvect_1(all_78_6) = all_78_5 & % 164.30/22.97 | k1_zfmisc_1(all_78_2) = all_78_1 & u1_struct_0(all_78_3) = all_78_2 & % 164.30/22.97 | $i(all_78_0) & $i(all_78_1) & $i(all_78_2) & $i(all_78_3) & % 164.30/22.97 | $i(all_78_4) & $i(all_78_5) & $i(all_78_6) & m1_subset_1(all_78_2, % 164.30/22.97 | all_78_1) & l1_vectsp_2(all_78_3, all_78_6) & v5_vectsp_2(all_78_3, % 164.30/22.97 | all_78_6) & v3_vectsp_2(all_78_3, all_78_6) & l3_vectsp_1(all_78_6) % 164.30/22.97 | & v2_vectsp_2(all_78_6) & v8_vectsp_1(all_78_6) & % 164.30/22.97 | v7_vectsp_1(all_78_6) & v6_vectsp_1(all_78_6) & v7_group_1(all_78_6) & % 164.30/22.97 | v4_group_1(all_78_6) & v6_rlvect_1(all_78_3) & v6_rlvect_1(all_78_6) & % 164.30/22.97 | v5_rlvect_1(all_78_3) & v5_rlvect_1(all_78_6) & v4_rlvect_1(all_78_3) % 164.30/22.97 | & v4_rlvect_1(all_78_6) & v3_rlvect_1(all_78_3) & % 164.30/22.97 | v3_rlvect_1(all_78_6) & ~ v10_vectsp_1(all_78_6) & ~ % 164.30/22.97 | v3_struct_0(all_78_3) & ~ v3_struct_0(all_78_6) % 164.30/22.97 | % 164.30/22.97 | ALPHA: (17) implies: % 164.30/22.97 | (18) ~ (all_78_4 = all_78_5) % 164.30/22.97 | (19) ~ (all_78_0 = all_78_3) % 164.30/22.97 | (20) ~ v3_struct_0(all_78_6) % 164.30/22.97 | (21) ~ v3_struct_0(all_78_3) % 164.30/22.97 | (22) ~ v10_vectsp_1(all_78_6) % 164.30/22.97 | (23) v3_rlvect_1(all_78_6) % 164.30/22.97 | (24) v3_rlvect_1(all_78_3) % 164.30/22.98 | (25) v4_rlvect_1(all_78_6) % 164.30/22.98 | (26) v4_rlvect_1(all_78_3) % 164.30/22.98 | (27) v5_rlvect_1(all_78_6) % 164.30/22.98 | (28) v5_rlvect_1(all_78_3) % 164.30/22.98 | (29) v6_rlvect_1(all_78_6) % 164.30/22.98 | (30) v6_rlvect_1(all_78_3) % 164.30/22.98 | (31) v4_group_1(all_78_6) % 164.30/22.98 | (32) v7_group_1(all_78_6) % 164.30/22.98 | (33) v6_vectsp_1(all_78_6) % 164.30/22.98 | (34) v7_vectsp_1(all_78_6) % 164.30/22.98 | (35) v8_vectsp_1(all_78_6) % 164.30/22.98 | (36) v2_vectsp_2(all_78_6) % 164.30/22.98 | (37) l3_vectsp_1(all_78_6) % 164.30/22.98 | (38) v3_vectsp_2(all_78_3, all_78_6) % 164.30/22.98 | (39) v5_vectsp_2(all_78_3, all_78_6) % 164.30/22.98 | (40) l1_vectsp_2(all_78_3, all_78_6) % 164.30/22.98 | (41) m1_subset_1(all_78_2, all_78_1) % 164.30/22.98 | (42) $i(all_78_6) % 164.30/22.98 | (43) $i(all_78_3) % 164.30/22.98 | (44) u1_struct_0(all_78_3) = all_78_2 % 164.30/22.98 | (45) k1_zfmisc_1(all_78_2) = all_78_1 % 164.30/22.98 | (46) k1_rlvect_1(all_78_6) = all_78_5 % 164.30/22.98 | (47) k1_rmod_5(all_78_6, all_78_3, all_78_2) = all_78_0 % 164.30/22.98 | (48) k2_group_1(all_78_6) = all_78_4 % 164.30/22.98 | % 164.30/22.98 | GROUND_INST: instantiating (5) with all_78_6, simplifying with (37), (42) % 164.30/22.98 | gives: % 164.30/22.98 | (49) l2_vectsp_1(all_78_6) % 164.30/22.98 | % 164.30/22.98 | GROUND_INST: instantiating (1) with all_78_6, all_78_3, all_78_2, simplifying % 164.30/22.98 | with (20), (21), (23), (24), (25), (26), (27), (28), (29), (30), % 164.30/22.98 | (31), (33), (34), (35), (37), (39), (40), (42), (43), (44) gives: % 164.30/22.99 | (50) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 164.30/22.99 | (k2_rmod_2(all_78_6, all_78_3) = v0 & u1_vectsp_2(all_78_6, all_78_3) % 164.30/22.99 | = v3 & u1_rlvect_1(all_78_3) = v1 & u2_struct_0(all_78_3) = v2 & % 164.30/22.99 | g1_vectsp_2(all_78_6, all_78_2, v1, v2, v3) = v0 & $i(v3) & $i(v2) & % 164.30/22.99 | $i(v1) & $i(v0)) % 164.30/22.99 | % 164.30/22.99 | GROUND_INST: instantiating (9) with all_78_6, all_78_5, simplifying with (20), % 164.30/22.99 | (22), (23), (25), (27), (29), (31), (32), (33), (34), (35), (36), % 164.30/22.99 | (37), (42), (46) gives: % 164.30/22.99 | (51) ? [v0: $i] : (k2_group_1(all_78_6) = v0 & $i(v0) & ! [v1: $i] : ! % 164.30/22.99 | [v2: $i] : ( ~ (u1_struct_0(v1) = v2) | ~ $i(v1) | ~ % 164.30/22.99 | l1_vectsp_2(v1, all_78_6) | ~ v5_vectsp_2(v1, all_78_6) | ~ % 164.30/22.99 | v6_rlvect_1(v1) | ~ v5_rlvect_1(v1) | ~ v4_rlvect_1(v1) | ~ % 164.30/22.99 | v3_rlvect_1(v1) | v3_struct_0(v1) | ? [v3: $i] : (k1_zfmisc_1(v2) % 164.30/22.99 | = v3 & $i(v3) & ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v6 = % 164.30/22.99 | v5 | v0 = all_78_5 | ~ (k1_rmod_5(all_78_6, v1, v4) = v5) | % 164.30/22.99 | ~ (u1_struct_0(v6) = v4) | ~ $i(v6) | ~ $i(v4) | ~ % 164.30/22.99 | m1_rmod_2(v6, all_78_6, v1) | ~ m1_subset_1(v4, v3) | ~ % 164.30/22.99 | v3_vectsp_2(v6, all_78_6))))) % 164.30/22.99 | % 164.30/22.99 | GROUND_INST: instantiating (10) with all_78_6, all_78_4, simplifying with % 164.30/22.99 | (20), (22), (23), (25), (27), (29), (31), (32), (33), (34), (35), % 164.30/22.99 | (36), (37), (42), (48) gives: % 164.30/23.00 | (52) ? [v0: $i] : (k1_rlvect_1(all_78_6) = v0 & $i(v0) & ! [v1: $i] : ! % 164.30/23.00 | [v2: $i] : ( ~ (u1_struct_0(v1) = v2) | ~ $i(v1) | ~ % 164.30/23.00 | l1_vectsp_2(v1, all_78_6) | ~ v5_vectsp_2(v1, all_78_6) | ~ % 164.30/23.00 | v6_rlvect_1(v1) | ~ v5_rlvect_1(v1) | ~ v4_rlvect_1(v1) | ~ % 164.30/23.00 | v3_rlvect_1(v1) | v3_struct_0(v1) | ? [v3: $i] : (k1_zfmisc_1(v2) % 164.30/23.00 | = v3 & $i(v3) & ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v6 = % 164.30/23.00 | v5 | v0 = all_78_4 | ~ (k1_rmod_5(all_78_6, v1, v4) = v5) | % 164.30/23.00 | ~ (u1_struct_0(v6) = v4) | ~ $i(v6) | ~ $i(v4) | ~ % 164.30/23.00 | m1_rmod_2(v6, all_78_6, v1) | ~ m1_subset_1(v4, v3) | ~ % 164.30/23.00 | v3_vectsp_2(v6, all_78_6))))) % 164.30/23.00 | % 164.30/23.00 | DELTA: instantiating (50) with fresh symbols all_112_0, all_112_1, all_112_2, % 164.30/23.00 | all_112_3 gives: % 164.30/23.00 | (53) k2_rmod_2(all_78_6, all_78_3) = all_112_3 & u1_vectsp_2(all_78_6, % 164.30/23.00 | all_78_3) = all_112_0 & u1_rlvect_1(all_78_3) = all_112_2 & % 164.30/23.00 | u2_struct_0(all_78_3) = all_112_1 & g1_vectsp_2(all_78_6, all_78_2, % 164.30/23.00 | all_112_2, all_112_1, all_112_0) = all_112_3 & $i(all_112_0) & % 164.30/23.00 | $i(all_112_1) & $i(all_112_2) & $i(all_112_3) % 164.30/23.00 | % 164.30/23.00 | ALPHA: (53) implies: % 164.30/23.00 | (54) $i(all_112_3) % 164.30/23.00 | (55) g1_vectsp_2(all_78_6, all_78_2, all_112_2, all_112_1, all_112_0) = % 164.30/23.00 | all_112_3 % 164.30/23.00 | (56) u2_struct_0(all_78_3) = all_112_1 % 164.30/23.00 | (57) u1_rlvect_1(all_78_3) = all_112_2 % 164.30/23.00 | (58) u1_vectsp_2(all_78_6, all_78_3) = all_112_0 % 164.30/23.00 | (59) k2_rmod_2(all_78_6, all_78_3) = all_112_3 % 164.30/23.00 | % 164.30/23.00 | DELTA: instantiating (52) with fresh symbol all_114_0 gives: % 164.30/23.01 | (60) k1_rlvect_1(all_78_6) = all_114_0 & $i(all_114_0) & ! [v0: $i] : ! % 164.30/23.01 | [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ l1_vectsp_2(v0, % 164.30/23.01 | all_78_6) | ~ v5_vectsp_2(v0, all_78_6) | ~ v6_rlvect_1(v0) | ~ % 164.30/23.01 | v5_rlvect_1(v0) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v0) | % 164.30/23.01 | v3_struct_0(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & ! % 164.30/23.01 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | all_114_0 = % 164.30/23.01 | all_78_4 | ~ (k1_rmod_5(all_78_6, v0, v3) = v4) | ~ % 164.30/23.01 | (u1_struct_0(v5) = v3) | ~ $i(v5) | ~ $i(v3) | ~ % 164.30/23.01 | m1_rmod_2(v5, all_78_6, v0) | ~ m1_subset_1(v3, v2) | ~ % 164.30/23.01 | v3_vectsp_2(v5, all_78_6)))) % 164.30/23.01 | % 164.30/23.01 | ALPHA: (60) implies: % 164.30/23.01 | (61) k1_rlvect_1(all_78_6) = all_114_0 % 164.30/23.01 | (62) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 164.30/23.01 | ~ l1_vectsp_2(v0, all_78_6) | ~ v5_vectsp_2(v0, all_78_6) | ~ % 164.30/23.01 | v6_rlvect_1(v0) | ~ v5_rlvect_1(v0) | ~ v4_rlvect_1(v0) | ~ % 164.30/23.01 | v3_rlvect_1(v0) | v3_struct_0(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = % 164.30/23.01 | v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | % 164.30/23.01 | all_114_0 = all_78_4 | ~ (k1_rmod_5(all_78_6, v0, v3) = v4) | % 164.30/23.01 | ~ (u1_struct_0(v5) = v3) | ~ $i(v5) | ~ $i(v3) | ~ % 164.30/23.01 | m1_rmod_2(v5, all_78_6, v0) | ~ m1_subset_1(v3, v2) | ~ % 164.30/23.01 | v3_vectsp_2(v5, all_78_6)))) % 164.30/23.01 | % 164.30/23.01 | GROUND_INST: instantiating (62) with all_78_3, all_78_2, simplifying with % 164.30/23.01 | (21), (24), (26), (28), (30), (39), (40), (43), (44) gives: % 164.30/23.01 | (63) ? [v0: $i] : (k1_zfmisc_1(all_78_2) = v0 & $i(v0) & ! [v1: $i] : ! % 164.30/23.01 | [v2: $i] : ! [v3: $i] : (v3 = v2 | all_114_0 = all_78_4 | ~ % 164.30/23.01 | (k1_rmod_5(all_78_6, all_78_3, v1) = v2) | ~ (u1_struct_0(v3) = % 164.30/23.01 | v1) | ~ $i(v3) | ~ $i(v1) | ~ m1_rmod_2(v3, all_78_6, % 164.30/23.01 | all_78_3) | ~ m1_subset_1(v1, v0) | ~ v3_vectsp_2(v3, % 164.30/23.01 | all_78_6))) % 164.30/23.01 | % 164.30/23.01 | DELTA: instantiating (51) with fresh symbol all_117_0 gives: % 164.30/23.02 | (64) k2_group_1(all_78_6) = all_117_0 & $i(all_117_0) & ! [v0: $i] : ! % 164.30/23.02 | [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ l1_vectsp_2(v0, % 164.30/23.02 | all_78_6) | ~ v5_vectsp_2(v0, all_78_6) | ~ v6_rlvect_1(v0) | ~ % 164.30/23.02 | v5_rlvect_1(v0) | ~ v4_rlvect_1(v0) | ~ v3_rlvect_1(v0) | % 164.30/23.02 | v3_struct_0(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = v2 & $i(v2) & ! % 164.30/23.02 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | all_117_0 = % 164.30/23.02 | all_78_5 | ~ (k1_rmod_5(all_78_6, v0, v3) = v4) | ~ % 164.30/23.02 | (u1_struct_0(v5) = v3) | ~ $i(v5) | ~ $i(v3) | ~ % 164.30/23.02 | m1_rmod_2(v5, all_78_6, v0) | ~ m1_subset_1(v3, v2) | ~ % 164.30/23.02 | v3_vectsp_2(v5, all_78_6)))) % 164.30/23.02 | % 164.30/23.02 | ALPHA: (64) implies: % 164.30/23.02 | (65) ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | % 164.30/23.02 | ~ l1_vectsp_2(v0, all_78_6) | ~ v5_vectsp_2(v0, all_78_6) | ~ % 164.30/23.02 | v6_rlvect_1(v0) | ~ v5_rlvect_1(v0) | ~ v4_rlvect_1(v0) | ~ % 164.30/23.02 | v3_rlvect_1(v0) | v3_struct_0(v0) | ? [v2: $i] : (k1_zfmisc_1(v1) = % 164.30/23.02 | v2 & $i(v2) & ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v5 = v4 | % 164.30/23.02 | all_117_0 = all_78_5 | ~ (k1_rmod_5(all_78_6, v0, v3) = v4) | % 164.30/23.02 | ~ (u1_struct_0(v5) = v3) | ~ $i(v5) | ~ $i(v3) | ~ % 164.30/23.02 | m1_rmod_2(v5, all_78_6, v0) | ~ m1_subset_1(v3, v2) | ~ % 164.30/23.02 | v3_vectsp_2(v5, all_78_6)))) % 164.30/23.02 | % 164.30/23.02 | GROUND_INST: instantiating (65) with all_78_3, all_78_2, simplifying with % 164.30/23.02 | (21), (24), (26), (28), (30), (39), (40), (43), (44) gives: % 164.30/23.02 | (66) ? [v0: $i] : (k1_zfmisc_1(all_78_2) = v0 & $i(v0) & ! [v1: $i] : ! % 164.30/23.02 | [v2: $i] : ! [v3: $i] : (v3 = v2 | all_117_0 = all_78_5 | ~ % 164.30/23.02 | (k1_rmod_5(all_78_6, all_78_3, v1) = v2) | ~ (u1_struct_0(v3) = % 164.30/23.02 | v1) | ~ $i(v3) | ~ $i(v1) | ~ m1_rmod_2(v3, all_78_6, % 164.30/23.02 | all_78_3) | ~ m1_subset_1(v1, v0) | ~ v3_vectsp_2(v3, % 164.30/23.02 | all_78_6))) % 164.30/23.02 | % 164.30/23.02 | DELTA: instantiating (63) with fresh symbol all_120_0 gives: % 164.30/23.02 | (67) k1_zfmisc_1(all_78_2) = all_120_0 & $i(all_120_0) & ! [v0: $i] : ! % 164.30/23.02 | [v1: $i] : ! [v2: $i] : (v2 = v1 | all_114_0 = all_78_4 | ~ % 164.30/23.02 | (k1_rmod_5(all_78_6, all_78_3, v0) = v1) | ~ (u1_struct_0(v2) = v0) % 164.30/23.02 | | ~ $i(v2) | ~ $i(v0) | ~ m1_rmod_2(v2, all_78_6, all_78_3) | ~ % 164.30/23.02 | m1_subset_1(v0, all_120_0) | ~ v3_vectsp_2(v2, all_78_6)) % 164.30/23.02 | % 164.30/23.02 | ALPHA: (67) implies: % 164.30/23.02 | (68) k1_zfmisc_1(all_78_2) = all_120_0 % 164.30/23.03 | (69) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | all_114_0 = % 164.30/23.03 | all_78_4 | ~ (k1_rmod_5(all_78_6, all_78_3, v0) = v1) | ~ % 164.30/23.03 | (u1_struct_0(v2) = v0) | ~ $i(v2) | ~ $i(v0) | ~ m1_rmod_2(v2, % 164.30/23.03 | all_78_6, all_78_3) | ~ m1_subset_1(v0, all_120_0) | ~ % 164.30/23.03 | v3_vectsp_2(v2, all_78_6)) % 164.30/23.03 | % 164.30/23.03 | DELTA: instantiating (66) with fresh symbol all_123_0 gives: % 164.30/23.03 | (70) k1_zfmisc_1(all_78_2) = all_123_0 & $i(all_123_0) & ! [v0: $i] : ! % 164.30/23.03 | [v1: $i] : ! [v2: $i] : (v2 = v1 | all_117_0 = all_78_5 | ~ % 164.30/23.03 | (k1_rmod_5(all_78_6, all_78_3, v0) = v1) | ~ (u1_struct_0(v2) = v0) % 164.30/23.03 | | ~ $i(v2) | ~ $i(v0) | ~ m1_rmod_2(v2, all_78_6, all_78_3) | ~ % 164.30/23.03 | m1_subset_1(v0, all_123_0) | ~ v3_vectsp_2(v2, all_78_6)) % 164.30/23.03 | % 164.30/23.03 | ALPHA: (70) implies: % 164.30/23.03 | (71) k1_zfmisc_1(all_78_2) = all_123_0 % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (14) with all_78_1, all_123_0, all_78_2, % 164.30/23.03 | simplifying with (45), (71) gives: % 164.30/23.03 | (72) all_123_0 = all_78_1 % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (14) with all_120_0, all_123_0, all_78_2, % 164.30/23.03 | simplifying with (68), (71) gives: % 164.30/23.03 | (73) all_123_0 = all_120_0 % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (15) with all_78_5, all_114_0, all_78_6, % 164.30/23.03 | simplifying with (46), (61) gives: % 164.30/23.03 | (74) all_114_0 = all_78_5 % 164.30/23.03 | % 164.30/23.03 | COMBINE_EQS: (72), (73) imply: % 164.30/23.03 | (75) all_120_0 = all_78_1 % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (4) with all_78_6, simplifying with (42), (49) % 164.30/23.03 | gives: % 164.30/23.03 | (76) l2_struct_0(all_78_6) % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (3) with all_78_6, all_78_3, all_112_3, simplifying % 164.30/23.03 | with (20), (21), (23), (24), (25), (26), (27), (28), (29), (30), % 164.30/23.03 | (31), (33), (34), (35), (37), (39), (40), (42), (43), (59) gives: % 164.30/23.03 | (77) m1_rmod_2(all_112_3, all_78_6, all_78_3) % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (2) with all_78_6, all_78_3, all_112_3, simplifying % 164.30/23.03 | with (20), (21), (23), (24), (25), (26), (27), (28), (29), (30), % 164.30/23.03 | (31), (33), (34), (35), (37), (39), (40), (42), (43), (59) gives: % 164.30/23.03 | (78) v3_vectsp_2(all_112_3, all_78_6) % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (dt_l2_struct_0) with all_78_6, simplifying with % 164.30/23.03 | (42), (76) gives: % 164.30/23.03 | (79) l1_struct_0(all_78_6) % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (7) with all_78_3, all_78_2, simplifying with (43), % 164.30/23.03 | (44) gives: % 164.30/23.03 | (80) ~ l1_rlvect_1(all_78_3) | ? [v0: $i] : ? [v1: $i] : % 164.30/23.03 | (k2_zfmisc_1(all_78_2, all_78_2) = v1 & u1_rlvect_1(all_78_3) = v0 & % 164.30/23.03 | $i(v1) & $i(v0) & m2_relset_1(v0, v1, all_78_2) & v1_funct_2(v0, v1, % 164.30/23.03 | all_78_2) & v1_funct_1(v0)) % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (6) with all_78_3, all_112_2, simplifying with % 164.30/23.03 | (43), (57) gives: % 164.30/23.03 | (81) ~ l1_rlvect_1(all_78_3) | ? [v0: $i] : ? [v1: $i] : % 164.30/23.03 | (k2_zfmisc_1(v0, v0) = v1 & u1_struct_0(all_78_3) = v0 & $i(v1) & % 164.30/23.03 | $i(v0) & m2_relset_1(all_112_2, v1, v0) & v1_funct_2(all_112_2, v1, % 164.30/23.03 | v0)) % 164.30/23.03 | % 164.30/23.03 | GROUND_INST: instantiating (abstractness_v3_vectsp_2) with all_78_6, all_78_3, % 164.30/23.03 | all_112_0, simplifying with (38), (40), (42), (43), (58), (79) % 164.30/23.03 | gives: % 164.30/23.04 | (82) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (u1_struct_0(all_78_3) = v0 % 164.30/23.04 | & u1_rlvect_1(all_78_3) = v1 & u2_struct_0(all_78_3) = v2 & % 164.30/23.04 | g1_vectsp_2(all_78_6, v0, v1, v2, all_112_0) = all_78_3 & $i(v2) & % 164.30/23.04 | $i(v1) & $i(v0)) % 164.30/23.04 | % 164.30/23.04 | GROUND_INST: instantiating (8) with all_78_6, all_78_3, all_112_0, simplifying % 164.30/23.04 | with (40), (42), (43), (58), (79) gives: % 164.30/23.04 | (83) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (k2_zfmisc_1(v0, v1) = v2 & % 164.30/23.04 | u1_struct_0(all_78_3) = v0 & u1_struct_0(all_78_6) = v1 & $i(v2) & % 164.30/23.04 | $i(v1) & $i(v0) & m2_relset_1(all_112_0, v2, v0) & % 164.30/23.04 | v1_funct_2(all_112_0, v2, v0)) % 164.30/23.04 | % 164.30/23.04 | GROUND_INST: instantiating (dt_l1_vectsp_2) with all_78_6, all_78_3, % 164.30/23.04 | simplifying with (40), (42), (43), (79) gives: % 164.30/23.04 | (84) l1_rlvect_1(all_78_3) % 164.30/23.04 | % 164.30/23.04 | DELTA: instantiating (82) with fresh symbols all_266_0, all_266_1, all_266_2 % 164.30/23.04 | gives: % 164.30/23.04 | (85) u1_struct_0(all_78_3) = all_266_2 & u1_rlvect_1(all_78_3) = all_266_1 % 164.30/23.04 | & u2_struct_0(all_78_3) = all_266_0 & g1_vectsp_2(all_78_6, all_266_2, % 164.30/23.04 | all_266_1, all_266_0, all_112_0) = all_78_3 & $i(all_266_0) & % 164.30/23.04 | $i(all_266_1) & $i(all_266_2) % 164.30/23.04 | % 164.30/23.04 | ALPHA: (85) implies: % 164.30/23.04 | (86) $i(all_266_2) % 164.30/23.04 | (87) g1_vectsp_2(all_78_6, all_266_2, all_266_1, all_266_0, all_112_0) = % 164.30/23.04 | all_78_3 % 164.30/23.04 | (88) u2_struct_0(all_78_3) = all_266_0 % 164.30/23.04 | (89) u1_rlvect_1(all_78_3) = all_266_1 % 164.30/23.04 | (90) u1_struct_0(all_78_3) = all_266_2 % 164.30/23.04 | % 164.30/23.04 | DELTA: instantiating (83) with fresh symbols all_270_0, all_270_1, all_270_2 % 164.30/23.04 | gives: % 164.30/23.04 | (91) k2_zfmisc_1(all_270_2, all_270_1) = all_270_0 & u1_struct_0(all_78_3) % 164.30/23.04 | = all_270_2 & u1_struct_0(all_78_6) = all_270_1 & $i(all_270_0) & % 164.30/23.04 | $i(all_270_1) & $i(all_270_2) & m2_relset_1(all_112_0, all_270_0, % 164.30/23.04 | all_270_2) & v1_funct_2(all_112_0, all_270_0, all_270_2) % 164.30/23.04 | % 164.30/23.04 | ALPHA: (91) implies: % 164.30/23.04 | (92) u1_struct_0(all_78_3) = all_270_2 % 164.30/23.04 | % 164.30/23.04 | BETA: splitting (81) gives: % 164.30/23.04 | % 164.30/23.04 | Case 1: % 164.30/23.04 | | % 164.30/23.04 | | (93) ~ l1_rlvect_1(all_78_3) % 164.30/23.04 | | % 164.30/23.04 | | PRED_UNIFY: (84), (93) imply: % 164.30/23.04 | | (94) $false % 164.30/23.04 | | % 164.30/23.04 | | CLOSE: (94) is inconsistent. % 164.30/23.04 | | % 164.30/23.04 | Case 2: % 164.30/23.04 | | % 164.30/23.04 | | (95) ? [v0: $i] : ? [v1: $i] : (k2_zfmisc_1(v0, v0) = v1 & % 164.30/23.04 | | u1_struct_0(all_78_3) = v0 & $i(v1) & $i(v0) & % 164.30/23.04 | | m2_relset_1(all_112_2, v1, v0) & v1_funct_2(all_112_2, v1, v0)) % 164.30/23.04 | | % 164.30/23.04 | | DELTA: instantiating (95) with fresh symbols all_281_0, all_281_1 gives: % 164.30/23.05 | | (96) k2_zfmisc_1(all_281_1, all_281_1) = all_281_0 & % 164.30/23.05 | | u1_struct_0(all_78_3) = all_281_1 & $i(all_281_0) & $i(all_281_1) & % 164.30/23.05 | | m2_relset_1(all_112_2, all_281_0, all_281_1) & v1_funct_2(all_112_2, % 164.30/23.05 | | all_281_0, all_281_1) % 164.30/23.05 | | % 164.30/23.05 | | ALPHA: (96) implies: % 164.30/23.05 | | (97) u1_struct_0(all_78_3) = all_281_1 % 164.30/23.05 | | % 164.30/23.05 | | BETA: splitting (80) gives: % 164.30/23.05 | | % 164.30/23.05 | | Case 1: % 164.30/23.05 | | | % 164.30/23.05 | | | (98) ~ l1_rlvect_1(all_78_3) % 164.30/23.05 | | | % 164.30/23.05 | | | PRED_UNIFY: (84), (98) imply: % 164.30/23.05 | | | (99) $false % 164.30/23.05 | | | % 164.30/23.05 | | | CLOSE: (99) is inconsistent. % 164.30/23.05 | | | % 164.30/23.05 | | Case 2: % 164.30/23.05 | | | % 164.30/23.05 | | | (100) ? [v0: $i] : ? [v1: $i] : (k2_zfmisc_1(all_78_2, all_78_2) = v1 % 164.30/23.05 | | | & u1_rlvect_1(all_78_3) = v0 & $i(v1) & $i(v0) & % 164.30/23.05 | | | m2_relset_1(v0, v1, all_78_2) & v1_funct_2(v0, v1, all_78_2) & % 164.30/23.05 | | | v1_funct_1(v0)) % 164.30/23.05 | | | % 164.30/23.05 | | | DELTA: instantiating (100) with fresh symbols all_287_0, all_287_1 gives: % 164.30/23.05 | | | (101) k2_zfmisc_1(all_78_2, all_78_2) = all_287_0 & % 164.30/23.05 | | | u1_rlvect_1(all_78_3) = all_287_1 & $i(all_287_0) & $i(all_287_1) % 164.30/23.05 | | | & m2_relset_1(all_287_1, all_287_0, all_78_2) & % 164.30/23.05 | | | v1_funct_2(all_287_1, all_287_0, all_78_2) & % 164.30/23.05 | | | v1_funct_1(all_287_1) % 164.30/23.05 | | | % 164.30/23.05 | | | ALPHA: (101) implies: % 164.30/23.05 | | | (102) u1_rlvect_1(all_78_3) = all_287_1 % 164.30/23.05 | | | % 164.30/23.05 | | | GROUND_INST: instantiating (11) with all_112_1, all_266_0, all_78_3, % 164.30/23.05 | | | simplifying with (56), (88) gives: % 164.30/23.05 | | | (103) all_266_0 = all_112_1 % 164.30/23.05 | | | % 164.30/23.05 | | | GROUND_INST: instantiating (12) with all_112_2, all_287_1, all_78_3, % 164.30/23.05 | | | simplifying with (57), (102) gives: % 164.30/23.05 | | | (104) all_287_1 = all_112_2 % 164.30/23.05 | | | % 164.30/23.05 | | | GROUND_INST: instantiating (12) with all_266_1, all_287_1, all_78_3, % 164.30/23.05 | | | simplifying with (89), (102) gives: % 164.30/23.05 | | | (105) all_287_1 = all_266_1 % 164.30/23.05 | | | % 164.30/23.05 | | | GROUND_INST: instantiating (13) with all_78_2, all_281_1, all_78_3, % 164.30/23.05 | | | simplifying with (44), (97) gives: % 164.30/23.05 | | | (106) all_281_1 = all_78_2 % 164.30/23.05 | | | % 164.30/23.05 | | | GROUND_INST: instantiating (13) with all_270_2, all_281_1, all_78_3, % 164.30/23.05 | | | simplifying with (92), (97) gives: % 164.30/23.05 | | | (107) all_281_1 = all_270_2 % 164.30/23.05 | | | % 164.30/23.05 | | | GROUND_INST: instantiating (13) with all_266_2, all_281_1, all_78_3, % 164.30/23.05 | | | simplifying with (90), (97) gives: % 164.30/23.05 | | | (108) all_281_1 = all_266_2 % 164.30/23.05 | | | % 164.30/23.05 | | | COMBINE_EQS: (104), (105) imply: % 164.30/23.05 | | | (109) all_266_1 = all_112_2 % 164.30/23.05 | | | % 164.30/23.05 | | | COMBINE_EQS: (106), (107) imply: % 164.30/23.05 | | | (110) all_270_2 = all_78_2 % 164.30/23.05 | | | % 164.30/23.05 | | | COMBINE_EQS: (107), (108) imply: % 164.30/23.05 | | | (111) all_270_2 = all_266_2 % 164.30/23.05 | | | % 164.30/23.05 | | | COMBINE_EQS: (110), (111) imply: % 164.30/23.05 | | | (112) all_266_2 = all_78_2 % 164.30/23.05 | | | % 164.30/23.05 | | | SIMP: (112) implies: % 164.30/23.05 | | | (113) all_266_2 = all_78_2 % 164.30/23.05 | | | % 164.30/23.05 | | | REDUCE: (87), (103), (109), (113) imply: % 164.30/23.05 | | | (114) g1_vectsp_2(all_78_6, all_78_2, all_112_2, all_112_1, all_112_0) % 164.30/23.05 | | | = all_78_3 % 164.30/23.05 | | | % 164.30/23.05 | | | REDUCE: (86), (113) imply: % 164.30/23.05 | | | (115) $i(all_78_2) % 164.30/23.05 | | | % 164.30/23.05 | | | GROUND_INST: instantiating (16) with all_112_3, all_78_3, all_112_0, % 164.30/23.05 | | | all_112_1, all_112_2, all_78_2, all_78_6, simplifying with % 164.30/23.05 | | | (55), (114) gives: % 164.30/23.05 | | | (116) all_112_3 = all_78_3 % 164.30/23.05 | | | % 164.30/23.05 | | | REDUCE: (77), (116) imply: % 164.30/23.05 | | | (117) m1_rmod_2(all_78_3, all_78_6, all_78_3) % 164.30/23.05 | | | % 164.30/23.05 | | | GROUND_INST: instantiating (69) with all_78_2, all_78_0, all_78_3, % 164.30/23.05 | | | simplifying with (38), (43), (44), (47), (115), (117) gives: % 164.30/23.05 | | | (118) all_114_0 = all_78_4 | all_78_0 = all_78_3 | ~ % 164.30/23.05 | | | m1_subset_1(all_78_2, all_120_0) % 164.30/23.05 | | | % 164.30/23.05 | | | BETA: splitting (118) gives: % 164.30/23.05 | | | % 164.30/23.05 | | | Case 1: % 164.30/23.05 | | | | % 164.30/23.05 | | | | (119) ~ m1_subset_1(all_78_2, all_120_0) % 164.30/23.05 | | | | % 164.30/23.05 | | | | REDUCE: (75), (119) imply: % 164.30/23.05 | | | | (120) ~ m1_subset_1(all_78_2, all_78_1) % 164.30/23.05 | | | | % 164.30/23.05 | | | | PRED_UNIFY: (41), (120) imply: % 164.30/23.05 | | | | (121) $false % 164.30/23.05 | | | | % 164.30/23.05 | | | | CLOSE: (121) is inconsistent. % 164.30/23.05 | | | | % 164.30/23.06 | | | Case 2: % 164.30/23.06 | | | | % 164.30/23.06 | | | | (122) all_114_0 = all_78_4 | all_78_0 = all_78_3 % 164.30/23.06 | | | | % 164.30/23.06 | | | | BETA: splitting (122) gives: % 164.30/23.06 | | | | % 164.30/23.06 | | | | Case 1: % 164.30/23.06 | | | | | % 164.30/23.06 | | | | | (123) all_114_0 = all_78_4 % 164.30/23.06 | | | | | % 164.30/23.06 | | | | | COMBINE_EQS: (74), (123) imply: % 164.30/23.06 | | | | | (124) all_78_4 = all_78_5 % 164.30/23.06 | | | | | % 164.30/23.06 | | | | | REDUCE: (18), (124) imply: % 164.30/23.06 | | | | | (125) $false % 164.30/23.06 | | | | | % 164.30/23.06 | | | | | CLOSE: (125) is inconsistent. % 164.30/23.06 | | | | | % 164.30/23.06 | | | | Case 2: % 164.30/23.06 | | | | | % 164.30/23.06 | | | | | (126) all_78_0 = all_78_3 % 164.30/23.06 | | | | | % 164.30/23.06 | | | | | REDUCE: (19), (126) imply: % 164.30/23.06 | | | | | (127) $false % 164.30/23.06 | | | | | % 164.30/23.06 | | | | | CLOSE: (127) is inconsistent. % 164.30/23.06 | | | | | % 164.30/23.06 | | | | End of split % 164.30/23.06 | | | | % 164.30/23.06 | | | End of split % 164.30/23.06 | | | % 164.30/23.06 | | End of split % 164.30/23.06 | | % 164.30/23.06 | End of split % 164.30/23.06 | % 164.30/23.06 End of proof % 164.30/23.06 % SZS output end Proof for theBenchmark % 164.30/23.06 % 164.30/23.06 22407ms %------------------------------------------------------------------------------