%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : LAT347+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 : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 06:24:59 EDT 2023 % Result : Theorem 23.38s 3.88s % Output : Proof 37.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : LAT347+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.20/0.35 % Computer : n017.cluster.edu % 0.20/0.35 % Model : x86_64 x86_64 % 0.20/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.20/0.35 % Memory : 8042.1875MB % 0.20/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.20/0.36 % CPULimit : 300 % 0.20/0.36 % WCLimit : 300 % 0.20/0.36 % DateTime : Thu Aug 24 04:35:09 EDT 2023 % 0.20/0.36 % 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/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.63 Running up to 7 provers in parallel. % 0.21/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.30/1.36 Prover 1: Preprocessing ... % 4.78/1.38 Prover 4: Preprocessing ... % 4.78/1.41 Prover 5: Preprocessing ... % 4.78/1.41 Prover 6: Preprocessing ... % 4.78/1.41 Prover 0: Preprocessing ... % 4.78/1.43 Prover 2: Preprocessing ... % 4.78/1.43 Prover 3: Preprocessing ... % 10.97/2.28 Prover 1: Warning: ignoring some quantifiers % 11.84/2.36 Prover 5: Proving ... % 11.84/2.36 Prover 2: Proving ... % 11.84/2.38 Prover 1: Constructing countermodel ... % 12.57/2.46 Prover 3: Warning: ignoring some quantifiers % 12.57/2.48 Prover 6: Proving ... % 13.04/2.49 Prover 3: Constructing countermodel ... % 17.11/3.07 Prover 4: Warning: ignoring some quantifiers % 17.90/3.19 Prover 4: Constructing countermodel ... % 20.20/3.59 Prover 0: Proving ... % 22.65/3.85 Prover 3: proved (3212ms) % 22.65/3.85 % 23.38/3.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.38/3.88 % 23.38/3.88 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 23.38/3.89 Prover 2: stopped % 23.38/3.89 Prover 0: stopped % 23.38/3.89 Prover 5: stopped % 23.38/3.89 Prover 6: stopped % 23.47/3.91 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 23.47/3.91 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 23.47/3.91 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 23.47/3.91 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 24.36/4.03 Prover 10: Preprocessing ... % 24.36/4.04 Prover 7: Preprocessing ... % 24.36/4.06 Prover 8: Preprocessing ... % 24.36/4.08 Prover 11: Preprocessing ... % 24.99/4.10 Prover 13: Preprocessing ... % 25.75/4.24 Prover 10: Warning: ignoring some quantifiers % 25.75/4.26 Prover 7: Warning: ignoring some quantifiers % 25.75/4.28 Prover 10: Constructing countermodel ... % 25.75/4.29 Prover 7: Constructing countermodel ... % 26.74/4.37 Prover 13: Warning: ignoring some quantifiers % 27.06/4.40 Prover 13: Constructing countermodel ... % 27.06/4.42 Prover 8: Warning: ignoring some quantifiers % 27.06/4.43 Prover 8: Constructing countermodel ... % 31.14/5.00 Prover 11: Warning: ignoring some quantifiers % 31.97/5.04 Prover 11: Constructing countermodel ... % 35.49/5.62 Prover 10: Found proof (size 116) % 35.49/5.62 Prover 10: proved (1732ms) % 35.49/5.62 Prover 11: stopped % 35.49/5.62 Prover 8: stopped % 35.49/5.62 Prover 7: stopped % 35.49/5.62 Prover 1: stopped % 35.49/5.63 Prover 13: stopped % 35.49/5.63 Prover 4: stopped % 35.49/5.63 % 35.49/5.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.49/5.63 % 36.38/5.65 % SZS output start Proof for theBenchmark % 36.70/5.65 Assumptions after simplification: % 36.70/5.65 --------------------------------- % 36.70/5.65 % 36.70/5.65 (cc1_yellow_0) % 36.70/5.66 ! [v0: $i] : ( ~ $i(v0) | ~ v3_lattice3(v0) | ~ l1_orders_2(v0) | % 36.70/5.66 v1_lattice3(v0) | v3_struct_0(v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ % 36.70/5.66 v3_lattice3(v0) | ~ l1_orders_2(v0) | v3_struct_0(v0) | v2_lattice3(v0)) % 36.70/5.66 % 36.70/5.66 (cc2_lattice3) % 36.70/5.66 ! [v0: $i] : ( ~ $i(v0) | ~ v3_struct_0(v0) | ~ l1_orders_2(v0) | ~ % 36.70/5.66 v2_lattice3(v0)) % 36.70/5.66 % 36.70/5.66 (dt_k1_yellow_0) % 36.70/5.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (k1_yellow_0(v0, v1) = v2) | ~ % 36.70/5.68 $i(v1) | ~ $i(v0) | ~ l1_orders_2(v0) | ? [v3: $i] : (u1_struct_0(v0) = % 36.70/5.68 v3 & $i(v3) & m1_subset_1(v2, v3))) % 36.70/5.68 % 36.70/5.68 (dt_k2_yellow_1) % 36.70/5.68 ! [v0: $i] : ! [v1: $i] : ( ~ (k2_yellow_1(v0) = v1) | ~ $i(v0) | % 36.70/5.68 v1_orders_2(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ (k2_yellow_1(v0) = v1) | % 36.70/5.68 ~ $i(v0) | l1_orders_2(v1)) % 36.70/5.68 % 36.70/5.68 (dt_k7_lattice3) % 36.70/5.68 ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.68 l1_orders_2(v0) | v1_orders_2(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 36.70/5.68 (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ l1_orders_2(v0) | l1_orders_2(v1)) % 36.70/5.68 % 36.70/5.68 (dt_l1_orders_2) % 36.70/5.68 ! [v0: $i] : ( ~ $i(v0) | ~ l1_orders_2(v0) | l1_struct_0(v0)) % 36.70/5.68 % 36.70/5.68 (fc10_yellow_7) % 36.70/5.68 ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.68 l1_orders_2(v0) | ~ v2_yellow_0(v0) | v1_yellow_0(v1)) & ! [v0: $i] : ! % 36.70/5.68 [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ l1_orders_2(v0) | ~ % 36.70/5.68 v2_yellow_0(v0) | v1_orders_2(v1)) % 36.70/5.68 % 36.70/5.68 (fc1_subset_1) % 36.70/5.69 ! [v0: $i] : ! [v1: $i] : ( ~ (k1_zfmisc_1(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.69 v1_xboole_0(v1)) % 36.70/5.69 % 36.70/5.69 (fc1_yellow_7) % 36.70/5.69 ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.69 l1_orders_2(v0) | ~ v2_orders_2(v0) | v1_orders_2(v1)) & ! [v0: $i] : ! % 36.70/5.69 [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ l1_orders_2(v0) | ~ % 36.70/5.69 v2_orders_2(v0) | v2_orders_2(v1)) % 36.70/5.69 % 36.70/5.69 (fc2_waybel16) % 36.70/5.69 ! [v0: $i] : ! [v1: $i] : ( ~ (k9_waybel_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.69 l1_orders_2(v0) | ~ v2_lattice3(v0) | ~ v2_yellow_0(v0) | ~ % 36.70/5.69 v4_orders_2(v0) | ~ v3_orders_2(v0) | ~ v2_orders_2(v0) | ? [v2: $i] : % 36.70/5.69 (k2_yellow_1(v1) = v2 & $i(v2) & v1_yellow_0(v2) & v25_waybel_0(v2) & % 36.70/5.69 v24_waybel_0(v2) & v3_lattice3(v2) & v1_orders_2(v2) & v2_lattice3(v2) & % 36.70/5.69 v4_orders_2(v2) & v3_orders_2(v2) & v2_orders_2(v2) & ~ v3_struct_0(v2))) % 36.70/5.69 % 36.70/5.69 (fc2_yellow_7) % 36.70/5.69 ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.69 l1_orders_2(v0) | ~ v3_orders_2(v0) | v1_orders_2(v1)) & ! [v0: $i] : ! % 36.70/5.69 [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ l1_orders_2(v0) | ~ % 36.70/5.69 v3_orders_2(v0) | v3_orders_2(v1)) % 36.70/5.69 % 36.70/5.69 (fc3_yellow_7) % 36.70/5.69 ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.69 l1_orders_2(v0) | ~ v4_orders_2(v0) | v1_orders_2(v1)) & ! [v0: $i] : ! % 36.70/5.69 [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ l1_orders_2(v0) | ~ % 36.70/5.69 v4_orders_2(v0) | v4_orders_2(v1)) % 36.70/5.69 % 36.70/5.69 (fc5_yellow_7) % 36.70/5.69 ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.69 v3_struct_0(v1) | ~ l1_orders_2(v0) | ~ v2_lattice3(v0)) & ! [v0: $i] : % 36.70/5.69 ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ l1_orders_2(v0) | ~ % 36.70/5.69 v2_lattice3(v0) | v1_lattice3(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 36.70/5.69 (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ l1_orders_2(v0) | ~ v2_lattice3(v0) % 36.70/5.69 | v1_orders_2(v1)) % 36.70/5.69 % 36.70/5.69 (rc10_waybel_0) % 36.70/5.69 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.69 l1_orders_2(v0) | ~ v3_orders_2(v0) | ~ v2_orders_2(v0) | v3_struct_0(v0) % 36.70/5.69 | ? [v2: $i] : ? [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & % 36.70/5.69 v13_waybel_0(v3, v0) & v2_waybel_0(v3, v0) & m1_subset_1(v3, v2) & ~ % 36.70/5.69 v1_xboole_0(v3))) % 36.70/5.69 % 36.70/5.69 (rc11_waybel_0) % 36.70/5.69 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.69 v1_lattice3(v0) | ~ l1_orders_2(v0) | ~ v2_lattice3(v0) | ~ % 36.70/5.69 v4_orders_2(v0) | ~ v3_orders_2(v0) | ~ v2_orders_2(v0) | ? [v2: $i] : ? % 36.70/5.69 [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v13_waybel_0(v3, v0) & % 36.70/5.69 v2_waybel_0(v3, v0) & v12_waybel_0(v3, v0) & m1_subset_1(v3, v2) & % 36.70/5.69 v1_waybel_0(v3, v0) & ~ v1_xboole_0(v3))) % 36.70/5.69 % 36.70/5.69 (rc1_waybel_0) % 36.70/5.70 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.70 l1_orders_2(v0) | ? [v2: $i] : ? [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) % 36.70/5.70 & $i(v2) & v2_waybel_0(v3, v0) & m1_subset_1(v3, v2) & v1_waybel_0(v3, % 36.70/5.70 v0))) % 36.70/5.70 % 36.70/5.70 (rc5_struct_0) % 36.70/5.70 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.70 l1_struct_0(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : % 36.70/5.70 (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & m1_subset_1(v3, v2) & ~ % 36.70/5.70 v1_xboole_0(v3))) % 36.70/5.70 % 36.70/5.70 (rc7_waybel_0) % 36.70/5.70 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.70 l1_orders_2(v0) | ? [v2: $i] : ? [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) % 36.70/5.70 & $i(v2) & v13_waybel_0(v3, v0) & v12_waybel_0(v3, v0) & m1_subset_1(v3, % 36.70/5.70 v2))) % 36.70/5.70 % 36.70/5.70 (rc8_waybel_0) % 36.70/5.70 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.70 l1_orders_2(v0) | v3_struct_0(v0) | ? [v2: $i] : ? [v3: $i] : % 36.70/5.70 (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & v13_waybel_0(v3, v0) & % 36.70/5.70 v12_waybel_0(v3, v0) & m1_subset_1(v3, v2) & ~ v1_xboole_0(v3))) % 36.70/5.70 % 36.70/5.70 (rc9_waybel_0) % 36.70/5.70 ! [v0: $i] : ! [v1: $i] : ( ~ (u1_struct_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.70 l1_orders_2(v0) | ~ v3_orders_2(v0) | ~ v2_orders_2(v0) | v3_struct_0(v0) % 36.70/5.70 | ? [v2: $i] : ? [v3: $i] : (k1_zfmisc_1(v1) = v2 & $i(v3) & $i(v2) & % 36.70/5.70 v12_waybel_0(v3, v0) & m1_subset_1(v3, v2) & v1_waybel_0(v3, v0) & ~ % 36.70/5.70 v1_xboole_0(v3))) % 36.70/5.70 % 36.70/5.70 (t1_waybel22) % 36.70/5.70 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 36.70/5.70 $i] : ? [v6: $i] : ? [v7: $i] : ( ~ (v7 = v6) & k3_tarski(v5) = v7 & % 36.70/5.70 k2_yellow_1(v1) = v2 & k1_yellow_0(v2, v5) = v6 & k9_waybel_0(v0) = v1 & % 36.70/5.70 k1_zfmisc_1(v3) = v4 & u1_struct_0(v2) = v3 & $i(v7) & $i(v6) & $i(v5) & % 36.70/5.70 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & m1_subset_1(v5, v4) & % 36.70/5.70 v1_waybel_0(v5, v2) & l1_orders_2(v0) & v2_lattice3(v0) & v2_yellow_0(v0) & % 36.70/5.70 v4_orders_2(v0) & v3_orders_2(v0) & v2_orders_2(v0) & ~ v1_xboole_0(v5)) % 36.70/5.70 % 36.70/5.70 (t2_subset) % 36.70/5.70 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ m1_subset_1(v0, v1) | % 36.70/5.70 r2_hidden(v0, v1) | v1_xboole_0(v1)) % 36.70/5.70 % 36.70/5.70 (t7_waybel16) % 36.70/5.70 ! [v0: $i] : ! [v1: $i] : ( ~ (k9_waybel_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.70 l1_orders_2(v0) | ~ v3_orders_2(v0) | ~ v2_orders_2(v0) | v3_struct_0(v0) % 36.70/5.70 | ? [v2: $i] : (k7_lattice3(v0) = v2 & k8_waybel_0(v2) = v1 & $i(v2) & % 36.70/5.70 $i(v1))) % 36.70/5.70 % 36.70/5.70 (t9_waybel13) % 36.70/5.70 ! [v0: $i] : ! [v1: $i] : ( ~ (k8_waybel_0(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.70 v1_lattice3(v0) | ~ v1_yellow_0(v0) | ~ l1_orders_2(v0) | ~ % 36.70/5.70 v4_orders_2(v0) | ~ v3_orders_2(v0) | ~ v2_orders_2(v0) | ? [v2: $i] : ? % 36.70/5.70 [v3: $i] : ? [v4: $i] : (k2_yellow_1(v1) = v2 & k1_zfmisc_1(v3) = v4 & % 36.70/5.70 u1_struct_0(v2) = v3 & $i(v4) & $i(v3) & $i(v2) & ! [v5: $i] : ! [v6: % 36.70/5.70 $i] : ( ~ (k1_yellow_0(v2, v5) = v6) | ~ $i(v5) | ~ m1_subset_1(v5, % 36.70/5.70 v4) | ~ v1_waybel_0(v5, v2) | v1_xboole_0(v5) | (k3_tarski(v5) = v6 & % 36.70/5.70 $i(v6))))) % 36.70/5.70 % 36.70/5.70 (function-axioms) % 36.70/5.71 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 % 36.70/5.71 | ~ (k6_relset_1(v4, v3, v2) = v1) | ~ (k6_relset_1(v4, v3, v2) = v0)) & % 36.70/5.71 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 36.70/5.71 (k1_yellow_0(v3, v2) = v1) | ~ (k1_yellow_0(v3, v2) = v0)) & ! [v0: $i] : % 36.70/5.71 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (k2_zfmisc_1(v3, v2) = % 36.70/5.71 v1) | ~ (k2_zfmisc_1(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 36.70/5.71 $i] : ! [v3: $i] : (v1 = v0 | ~ (g1_orders_2(v3, v2) = v1) | ~ % 36.70/5.71 (g1_orders_2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 % 36.70/5.71 = v0 | ~ (k3_tarski(v2) = v1) | ~ (k3_tarski(v2) = v0)) & ! [v0: $i] : ! % 36.70/5.71 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k4_relat_1(v2) = v1) | ~ % 36.70/5.71 (k4_relat_1(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 36.70/5.71 | ~ (k2_yellow_1(v2) = v1) | ~ (k2_yellow_1(v2) = v0)) & ! [v0: $i] : ! % 36.70/5.71 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k7_lattice3(v2) = v1) | ~ % 36.70/5.71 (k7_lattice3(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 36.70/5.71 | ~ (a_1_1_waybel_0(v2) = v1) | ~ (a_1_1_waybel_0(v2) = v0)) & ! [v0: $i] % 36.70/5.71 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k9_waybel_0(v2) = v1) | ~ % 36.70/5.71 (k9_waybel_0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 36.70/5.71 | ~ (a_1_0_waybel_0(v2) = v1) | ~ (a_1_0_waybel_0(v2) = v0)) & ! [v0: $i] % 36.70/5.71 : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k8_waybel_0(v2) = v1) | ~ % 36.70/5.71 (k8_waybel_0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 36.70/5.71 | ~ (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) & ! [v0: $i] : ! % 36.70/5.71 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (u1_struct_0(v2) = v1) | ~ % 36.70/5.71 (u1_struct_0(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 36.70/5.71 | ~ (u1_orders_2(v2) = v1) | ~ (u1_orders_2(v2) = v0)) % 36.70/5.71 % 36.70/5.71 Further assumptions not needed in the proof: % 36.70/5.71 -------------------------------------------- % 36.70/5.71 abstractness_v1_orders_2, antisymmetry_r2_hidden, cc10_waybel_0, cc11_waybel_0, % 36.70/5.71 cc12_waybel_0, cc13_waybel_0, cc14_waybel_0, cc1_funct_1, cc1_lattice3, % 36.70/5.71 cc1_relset_1, cc2_funct_1, cc3_yellow_0, cc4_yellow_0, cc5_yellow_0, % 36.70/5.71 cc9_waybel_0, d23_waybel_0, d24_waybel_0, d5_lattice3, dt_g1_orders_2, % 36.70/5.71 dt_k1_xboole_0, dt_k1_zfmisc_1, dt_k2_zfmisc_1, dt_k3_tarski, dt_k4_relat_1, % 36.70/5.71 dt_k6_relset_1, dt_k8_waybel_0, dt_k9_waybel_0, dt_l1_struct_0, dt_m1_relset_1, % 36.70/5.71 dt_m1_subset_1, dt_m2_relset_1, dt_u1_orders_2, dt_u1_struct_0, % 36.70/5.71 existence_l1_orders_2, existence_l1_struct_0, existence_m1_relset_1, % 36.70/5.71 existence_m1_subset_1, existence_m2_relset_1, fc10_waybel_8, fc1_struct_0, % 36.70/5.71 fc1_waybel16, fc1_xboole_0, fc3_funct_1, fc4_subset_1, fc4_waybel_8, % 36.70/5.71 fc5_lattice3, fc5_waybel_8, fc6_lattice3, fc6_waybel_8, fc6_yellow_7, % 36.70/5.71 fc7_waybel_8, fc7_yellow_7, fc8_waybel_8, fc9_waybel_8, fc9_yellow_7, % 36.70/5.71 fraenkel_a_1_0_waybel_0, fraenkel_a_1_1_waybel_0, free_g1_orders_2, % 36.70/5.71 involutiveness_k4_relat_1, involutiveness_k6_relset_1, rc13_waybel_0, % 36.70/5.71 rc1_funct_1, rc1_lattice3, rc1_subset_1, rc1_xboole_0, rc2_funct_1, % 36.70/5.71 rc2_lattice3, rc2_subset_1, rc2_xboole_0, rc2_yellow_0, rc3_funct_1, % 36.70/5.71 rc3_struct_0, redefinition_k6_relset_1, redefinition_m2_relset_1, % 36.70/5.71 reflexivity_r1_tarski, t1_subset, t2_tarski, t3_subset, t4_subset, t5_subset, % 36.70/5.71 t6_boole, t7_boole, t8_boole % 36.70/5.71 % 36.70/5.71 Those formulas are unsatisfiable: % 36.70/5.71 --------------------------------- % 36.70/5.71 % 36.70/5.71 Begin of proof % 36.70/5.71 | % 36.70/5.71 | ALPHA: (cc1_yellow_0) implies: % 36.70/5.71 | (1) ! [v0: $i] : ( ~ $i(v0) | ~ v3_lattice3(v0) | ~ l1_orders_2(v0) | % 36.70/5.71 | v1_lattice3(v0) | v3_struct_0(v0)) % 36.70/5.71 | % 36.70/5.71 | ALPHA: (dt_k2_yellow_1) implies: % 36.70/5.71 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (k2_yellow_1(v0) = v1) | ~ $i(v0) | % 36.70/5.71 | l1_orders_2(v1)) % 36.70/5.71 | % 36.70/5.71 | ALPHA: (dt_k7_lattice3) implies: % 36.70/5.71 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.71 | l1_orders_2(v0) | l1_orders_2(v1)) % 36.70/5.71 | % 36.70/5.71 | ALPHA: (fc10_yellow_7) implies: % 36.70/5.71 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.71 | l1_orders_2(v0) | ~ v2_yellow_0(v0) | v1_yellow_0(v1)) % 36.70/5.71 | % 36.70/5.71 | ALPHA: (fc1_yellow_7) implies: % 36.70/5.71 | (5) ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.71 | l1_orders_2(v0) | ~ v2_orders_2(v0) | v2_orders_2(v1)) % 36.70/5.71 | % 36.70/5.71 | ALPHA: (fc2_yellow_7) implies: % 36.70/5.71 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.72 | l1_orders_2(v0) | ~ v3_orders_2(v0) | v3_orders_2(v1)) % 36.70/5.72 | % 36.70/5.72 | ALPHA: (fc3_yellow_7) implies: % 36.70/5.72 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.72 | l1_orders_2(v0) | ~ v4_orders_2(v0) | v4_orders_2(v1)) % 36.70/5.72 | % 36.70/5.72 | ALPHA: (fc5_yellow_7) implies: % 36.70/5.72 | (8) ! [v0: $i] : ! [v1: $i] : ( ~ (k7_lattice3(v0) = v1) | ~ $i(v0) | ~ % 36.70/5.72 | l1_orders_2(v0) | ~ v2_lattice3(v0) | v1_lattice3(v1)) % 36.70/5.72 | % 36.70/5.72 | ALPHA: (function-axioms) implies: % 36.70/5.72 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 36.70/5.72 | (u1_struct_0(v2) = v1) | ~ (u1_struct_0(v2) = v0)) % 36.70/5.72 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 36.70/5.72 | (k1_zfmisc_1(v2) = v1) | ~ (k1_zfmisc_1(v2) = v0)) % 36.70/5.72 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 36.70/5.72 | (k2_yellow_1(v2) = v1) | ~ (k2_yellow_1(v2) = v0)) % 36.70/5.72 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (k3_tarski(v2) % 36.70/5.72 | = v1) | ~ (k3_tarski(v2) = v0)) % 36.70/5.72 | % 36.70/5.72 | DELTA: instantiating (t1_waybel22) with fresh symbols all_110_0, all_110_1, % 36.70/5.72 | all_110_2, all_110_3, all_110_4, all_110_5, all_110_6, all_110_7 gives: % 36.70/5.72 | (13) ~ (all_110_0 = all_110_1) & k3_tarski(all_110_2) = all_110_0 & % 36.70/5.72 | k2_yellow_1(all_110_6) = all_110_5 & k1_yellow_0(all_110_5, all_110_2) % 36.70/5.72 | = all_110_1 & k9_waybel_0(all_110_7) = all_110_6 & % 36.70/5.72 | k1_zfmisc_1(all_110_4) = all_110_3 & u1_struct_0(all_110_5) = % 36.70/5.72 | all_110_4 & $i(all_110_0) & $i(all_110_1) & $i(all_110_2) & % 36.70/5.72 | $i(all_110_3) & $i(all_110_4) & $i(all_110_5) & $i(all_110_6) & % 36.70/5.72 | $i(all_110_7) & m1_subset_1(all_110_2, all_110_3) & % 36.70/5.72 | v1_waybel_0(all_110_2, all_110_5) & l1_orders_2(all_110_7) & % 36.70/5.72 | v2_lattice3(all_110_7) & v2_yellow_0(all_110_7) & % 36.70/5.72 | v4_orders_2(all_110_7) & v3_orders_2(all_110_7) & % 36.70/5.72 | v2_orders_2(all_110_7) & ~ v1_xboole_0(all_110_2) % 36.70/5.72 | % 36.70/5.72 | ALPHA: (13) implies: % 36.70/5.72 | (14) ~ (all_110_0 = all_110_1) % 36.70/5.72 | (15) ~ v1_xboole_0(all_110_2) % 36.70/5.72 | (16) v2_orders_2(all_110_7) % 36.70/5.72 | (17) v3_orders_2(all_110_7) % 36.70/5.72 | (18) v4_orders_2(all_110_7) % 36.70/5.72 | (19) v2_yellow_0(all_110_7) % 36.70/5.72 | (20) v2_lattice3(all_110_7) % 36.70/5.72 | (21) l1_orders_2(all_110_7) % 36.70/5.72 | (22) v1_waybel_0(all_110_2, all_110_5) % 36.70/5.72 | (23) m1_subset_1(all_110_2, all_110_3) % 36.70/5.72 | (24) $i(all_110_7) % 36.70/5.72 | (25) $i(all_110_6) % 36.70/5.72 | (26) $i(all_110_3) % 36.70/5.72 | (27) $i(all_110_2) % 36.70/5.72 | (28) u1_struct_0(all_110_5) = all_110_4 % 36.70/5.72 | (29) k1_zfmisc_1(all_110_4) = all_110_3 % 36.70/5.72 | (30) k9_waybel_0(all_110_7) = all_110_6 % 36.70/5.72 | (31) k1_yellow_0(all_110_5, all_110_2) = all_110_1 % 36.70/5.72 | (32) k2_yellow_1(all_110_6) = all_110_5 % 36.70/5.72 | (33) k3_tarski(all_110_2) = all_110_0 % 36.70/5.72 | % 36.70/5.72 | GROUND_INST: instantiating (t2_subset) with all_110_2, all_110_3, simplifying % 36.70/5.72 | with (23), (26), (27) gives: % 36.70/5.72 | (34) r2_hidden(all_110_2, all_110_3) | v1_xboole_0(all_110_3) % 36.70/5.72 | % 36.70/5.73 | GROUND_INST: instantiating (fc2_waybel16) with all_110_7, all_110_6, % 36.70/5.73 | simplifying with (16), (17), (18), (19), (20), (21), (24), (30) % 36.70/5.73 | gives: % 36.70/5.73 | (35) ? [v0: $i] : (k2_yellow_1(all_110_6) = v0 & $i(v0) & v1_yellow_0(v0) % 36.70/5.73 | & v25_waybel_0(v0) & v24_waybel_0(v0) & v3_lattice3(v0) & % 36.70/5.73 | v1_orders_2(v0) & v2_lattice3(v0) & v4_orders_2(v0) & % 36.70/5.73 | v3_orders_2(v0) & v2_orders_2(v0) & ~ v3_struct_0(v0)) % 36.70/5.73 | % 36.70/5.73 | GROUND_INST: instantiating (t7_waybel16) with all_110_7, all_110_6, % 36.70/5.73 | simplifying with (16), (17), (21), (24), (30) gives: % 36.70/5.73 | (36) v3_struct_0(all_110_7) | ? [v0: $i] : (k7_lattice3(all_110_7) = v0 & % 36.70/5.73 | k8_waybel_0(v0) = all_110_6 & $i(v0) & $i(all_110_6)) % 36.70/5.73 | % 36.70/5.73 | GROUND_INST: instantiating (2) with all_110_6, all_110_5, simplifying with % 36.70/5.73 | (25), (32) gives: % 36.70/5.73 | (37) l1_orders_2(all_110_5) % 36.70/5.73 | % 36.70/5.73 | DELTA: instantiating (35) with fresh symbol all_124_0 gives: % 36.70/5.73 | (38) k2_yellow_1(all_110_6) = all_124_0 & $i(all_124_0) & % 36.70/5.73 | v1_yellow_0(all_124_0) & v25_waybel_0(all_124_0) & % 36.70/5.73 | v24_waybel_0(all_124_0) & v3_lattice3(all_124_0) & % 36.70/5.73 | v1_orders_2(all_124_0) & v2_lattice3(all_124_0) & % 36.70/5.73 | v4_orders_2(all_124_0) & v3_orders_2(all_124_0) & % 36.70/5.73 | v2_orders_2(all_124_0) & ~ v3_struct_0(all_124_0) % 36.70/5.73 | % 36.70/5.73 | ALPHA: (38) implies: % 36.70/5.73 | (39) ~ v3_struct_0(all_124_0) % 36.70/5.73 | (40) v2_orders_2(all_124_0) % 36.70/5.73 | (41) v3_orders_2(all_124_0) % 36.70/5.73 | (42) v4_orders_2(all_124_0) % 36.70/5.73 | (43) v2_lattice3(all_124_0) % 36.70/5.73 | (44) v3_lattice3(all_124_0) % 36.70/5.73 | (45) $i(all_124_0) % 36.70/5.73 | (46) k2_yellow_1(all_110_6) = all_124_0 % 36.70/5.73 | % 36.70/5.73 | GROUND_INST: instantiating (11) with all_110_5, all_124_0, all_110_6, % 36.70/5.73 | simplifying with (32), (46) gives: % 36.70/5.73 | (47) all_124_0 = all_110_5 % 36.70/5.73 | % 36.70/5.73 | REDUCE: (45), (47) imply: % 36.70/5.73 | (48) $i(all_110_5) % 36.70/5.73 | % 36.70/5.73 | REDUCE: (44), (47) imply: % 36.70/5.73 | (49) v3_lattice3(all_110_5) % 36.70/5.73 | % 36.70/5.73 | REDUCE: (43), (47) imply: % 36.70/5.73 | (50) v2_lattice3(all_110_5) % 36.70/5.73 | % 36.70/5.73 | REDUCE: (42), (47) imply: % 36.70/5.73 | (51) v4_orders_2(all_110_5) % 36.70/5.73 | % 36.70/5.73 | REDUCE: (41), (47) imply: % 36.70/5.73 | (52) v3_orders_2(all_110_5) % 36.70/5.73 | % 36.70/5.73 | REDUCE: (40), (47) imply: % 36.70/5.73 | (53) v2_orders_2(all_110_5) % 36.70/5.73 | % 36.70/5.73 | REDUCE: (39), (47) imply: % 36.70/5.73 | (54) ~ v3_struct_0(all_110_5) % 36.70/5.73 | % 36.70/5.73 | GROUND_INST: instantiating (rc10_waybel_0) with all_110_5, all_110_4, % 36.70/5.73 | simplifying with (28), (37), (48), (52), (53), (54) gives: % 36.70/5.73 | (55) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_110_4) = v0 & $i(v1) & % 36.70/5.73 | $i(v0) & v13_waybel_0(v1, all_110_5) & v2_waybel_0(v1, all_110_5) & % 36.70/5.73 | m1_subset_1(v1, v0) & ~ v1_xboole_0(v1)) % 36.70/5.73 | % 36.70/5.73 | GROUND_INST: instantiating (rc9_waybel_0) with all_110_5, all_110_4, % 36.70/5.73 | simplifying with (28), (37), (48), (52), (53), (54) gives: % 36.70/5.73 | (56) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_110_4) = v0 & $i(v1) & % 36.70/5.73 | $i(v0) & v12_waybel_0(v1, all_110_5) & m1_subset_1(v1, v0) & % 36.70/5.73 | v1_waybel_0(v1, all_110_5) & ~ v1_xboole_0(v1)) % 36.70/5.73 | % 36.70/5.73 | GROUND_INST: instantiating (rc8_waybel_0) with all_110_5, all_110_4, % 36.70/5.73 | simplifying with (28), (37), (48), (54) gives: % 36.70/5.73 | (57) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_110_4) = v0 & $i(v1) & % 36.70/5.73 | $i(v0) & v13_waybel_0(v1, all_110_5) & v12_waybel_0(v1, all_110_5) & % 36.70/5.73 | m1_subset_1(v1, v0) & ~ v1_xboole_0(v1)) % 36.70/5.73 | % 36.70/5.73 | GROUND_INST: instantiating (rc7_waybel_0) with all_110_5, all_110_4, % 36.70/5.73 | simplifying with (28), (37), (48) gives: % 36.70/5.74 | (58) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_110_4) = v0 & $i(v1) & % 36.70/5.74 | $i(v0) & v13_waybel_0(v1, all_110_5) & v12_waybel_0(v1, all_110_5) & % 36.70/5.74 | m1_subset_1(v1, v0)) % 36.70/5.74 | % 36.70/5.74 | GROUND_INST: instantiating (rc1_waybel_0) with all_110_5, all_110_4, % 36.70/5.74 | simplifying with (28), (37), (48) gives: % 36.70/5.74 | (59) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_110_4) = v0 & $i(v1) & % 36.70/5.74 | $i(v0) & v2_waybel_0(v1, all_110_5) & m1_subset_1(v1, v0) & % 36.70/5.74 | v1_waybel_0(v1, all_110_5)) % 36.70/5.74 | % 36.70/5.74 | GROUND_INST: instantiating (dt_k1_yellow_0) with all_110_5, all_110_2, % 36.70/5.74 | all_110_1, simplifying with (27), (31), (37), (48) gives: % 36.70/5.74 | (60) ? [v0: $i] : (u1_struct_0(all_110_5) = v0 & $i(v0) & % 36.70/5.74 | m1_subset_1(all_110_1, v0)) % 36.70/5.74 | % 36.70/5.74 | GROUND_INST: instantiating (dt_l1_orders_2) with all_110_5, simplifying with % 36.70/5.74 | (37), (48) gives: % 36.70/5.74 | (61) l1_struct_0(all_110_5) % 36.70/5.74 | % 36.70/5.74 | GROUND_INST: instantiating (1) with all_110_5, simplifying with (37), (48), % 36.70/5.74 | (49), (54) gives: % 36.70/5.74 | (62) v1_lattice3(all_110_5) % 36.70/5.74 | % 36.70/5.74 | DELTA: instantiating (60) with fresh symbol all_136_0 gives: % 36.70/5.74 | (63) u1_struct_0(all_110_5) = all_136_0 & $i(all_136_0) & % 36.70/5.74 | m1_subset_1(all_110_1, all_136_0) % 36.70/5.74 | % 36.70/5.74 | ALPHA: (63) implies: % 36.70/5.74 | (64) $i(all_136_0) % 36.70/5.74 | (65) u1_struct_0(all_110_5) = all_136_0 % 36.70/5.74 | % 36.70/5.74 | DELTA: instantiating (58) with fresh symbols all_138_0, all_138_1 gives: % 36.70/5.74 | (66) k1_zfmisc_1(all_110_4) = all_138_1 & $i(all_138_0) & $i(all_138_1) & % 36.70/5.74 | v13_waybel_0(all_138_0, all_110_5) & v12_waybel_0(all_138_0, % 37.12/5.74 | all_110_5) & m1_subset_1(all_138_0, all_138_1) % 37.12/5.74 | % 37.12/5.74 | ALPHA: (66) implies: % 37.12/5.74 | (67) k1_zfmisc_1(all_110_4) = all_138_1 % 37.12/5.74 | % 37.12/5.74 | DELTA: instantiating (59) with fresh symbols all_140_0, all_140_1 gives: % 37.12/5.74 | (68) k1_zfmisc_1(all_110_4) = all_140_1 & $i(all_140_0) & $i(all_140_1) & % 37.12/5.74 | v2_waybel_0(all_140_0, all_110_5) & m1_subset_1(all_140_0, all_140_1) % 37.12/5.74 | & v1_waybel_0(all_140_0, all_110_5) % 37.12/5.74 | % 37.12/5.74 | ALPHA: (68) implies: % 37.12/5.74 | (69) k1_zfmisc_1(all_110_4) = all_140_1 % 37.12/5.74 | % 37.12/5.74 | DELTA: instantiating (56) with fresh symbols all_142_0, all_142_1 gives: % 37.12/5.74 | (70) k1_zfmisc_1(all_110_4) = all_142_1 & $i(all_142_0) & $i(all_142_1) & % 37.12/5.74 | v12_waybel_0(all_142_0, all_110_5) & m1_subset_1(all_142_0, all_142_1) % 37.12/5.74 | & v1_waybel_0(all_142_0, all_110_5) & ~ v1_xboole_0(all_142_0) % 37.12/5.74 | % 37.12/5.74 | ALPHA: (70) implies: % 37.12/5.74 | (71) k1_zfmisc_1(all_110_4) = all_142_1 % 37.12/5.74 | % 37.12/5.74 | DELTA: instantiating (55) with fresh symbols all_144_0, all_144_1 gives: % 37.12/5.74 | (72) k1_zfmisc_1(all_110_4) = all_144_1 & $i(all_144_0) & $i(all_144_1) & % 37.12/5.74 | v13_waybel_0(all_144_0, all_110_5) & v2_waybel_0(all_144_0, all_110_5) % 37.12/5.74 | & m1_subset_1(all_144_0, all_144_1) & ~ v1_xboole_0(all_144_0) % 37.12/5.74 | % 37.12/5.74 | ALPHA: (72) implies: % 37.12/5.74 | (73) k1_zfmisc_1(all_110_4) = all_144_1 % 37.12/5.74 | % 37.12/5.74 | DELTA: instantiating (57) with fresh symbols all_146_0, all_146_1 gives: % 37.12/5.74 | (74) k1_zfmisc_1(all_110_4) = all_146_1 & $i(all_146_0) & $i(all_146_1) & % 37.12/5.74 | v13_waybel_0(all_146_0, all_110_5) & v12_waybel_0(all_146_0, % 37.12/5.74 | all_110_5) & m1_subset_1(all_146_0, all_146_1) & ~ % 37.12/5.74 | v1_xboole_0(all_146_0) % 37.12/5.74 | % 37.12/5.74 | ALPHA: (74) implies: % 37.12/5.74 | (75) k1_zfmisc_1(all_110_4) = all_146_1 % 37.12/5.74 | % 37.12/5.74 | GROUND_INST: instantiating (9) with all_110_4, all_136_0, all_110_5, % 37.12/5.74 | simplifying with (28), (65) gives: % 37.12/5.74 | (76) all_136_0 = all_110_4 % 37.12/5.74 | % 37.12/5.74 | GROUND_INST: instantiating (10) with all_110_3, all_142_1, all_110_4, % 37.12/5.74 | simplifying with (29), (71) gives: % 37.12/5.74 | (77) all_142_1 = all_110_3 % 37.12/5.74 | % 37.12/5.74 | GROUND_INST: instantiating (10) with all_140_1, all_142_1, all_110_4, % 37.12/5.74 | simplifying with (69), (71) gives: % 37.12/5.74 | (78) all_142_1 = all_140_1 % 37.12/5.74 | % 37.12/5.74 | GROUND_INST: instantiating (10) with all_142_1, all_144_1, all_110_4, % 37.12/5.74 | simplifying with (71), (73) gives: % 37.12/5.74 | (79) all_144_1 = all_142_1 % 37.12/5.74 | % 37.12/5.74 | GROUND_INST: instantiating (10) with all_144_1, all_146_1, all_110_4, % 37.12/5.74 | simplifying with (73), (75) gives: % 37.12/5.74 | (80) all_146_1 = all_144_1 % 37.12/5.74 | % 37.12/5.74 | GROUND_INST: instantiating (10) with all_138_1, all_146_1, all_110_4, % 37.12/5.74 | simplifying with (67), (75) gives: % 37.12/5.74 | (81) all_146_1 = all_138_1 % 37.12/5.74 | % 37.12/5.74 | COMBINE_EQS: (80), (81) imply: % 37.12/5.74 | (82) all_144_1 = all_138_1 % 37.12/5.74 | % 37.12/5.74 | SIMP: (82) implies: % 37.12/5.74 | (83) all_144_1 = all_138_1 % 37.12/5.74 | % 37.12/5.74 | COMBINE_EQS: (79), (83) imply: % 37.12/5.74 | (84) all_142_1 = all_138_1 % 37.12/5.74 | % 37.12/5.74 | SIMP: (84) implies: % 37.12/5.74 | (85) all_142_1 = all_138_1 % 37.12/5.74 | % 37.12/5.74 | COMBINE_EQS: (77), (78) imply: % 37.12/5.74 | (86) all_140_1 = all_110_3 % 37.12/5.74 | % 37.12/5.74 | COMBINE_EQS: (78), (85) imply: % 37.12/5.74 | (87) all_140_1 = all_138_1 % 37.12/5.74 | % 37.12/5.74 | COMBINE_EQS: (86), (87) imply: % 37.12/5.74 | (88) all_138_1 = all_110_3 % 37.12/5.74 | % 37.12/5.75 | REDUCE: (64), (76) imply: % 37.12/5.75 | (89) $i(all_110_4) % 37.12/5.75 | % 37.12/5.75 | GROUND_INST: instantiating (rc11_waybel_0) with all_110_5, all_110_4, % 37.12/5.75 | simplifying with (28), (37), (48), (50), (51), (52), (53), (62) % 37.12/5.75 | gives: % 37.12/5.75 | (90) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_110_4) = v0 & $i(v1) & % 37.12/5.75 | $i(v0) & v13_waybel_0(v1, all_110_5) & v2_waybel_0(v1, all_110_5) & % 37.12/5.75 | v12_waybel_0(v1, all_110_5) & m1_subset_1(v1, v0) & v1_waybel_0(v1, % 37.12/5.75 | all_110_5) & ~ v1_xboole_0(v1)) % 37.12/5.75 | % 37.12/5.75 | GROUND_INST: instantiating (rc5_struct_0) with all_110_5, all_110_4, % 37.12/5.75 | simplifying with (28), (48), (54), (61) gives: % 37.12/5.75 | (91) ? [v0: $i] : ? [v1: $i] : (k1_zfmisc_1(all_110_4) = v0 & $i(v1) & % 37.12/5.75 | $i(v0) & m1_subset_1(v1, v0) & ~ v1_xboole_0(v1)) % 37.12/5.75 | % 37.12/5.75 | DELTA: instantiating (91) with fresh symbols all_158_0, all_158_1 gives: % 37.12/5.75 | (92) k1_zfmisc_1(all_110_4) = all_158_1 & $i(all_158_0) & $i(all_158_1) & % 37.12/5.75 | m1_subset_1(all_158_0, all_158_1) & ~ v1_xboole_0(all_158_0) % 37.12/5.75 | % 37.12/5.75 | ALPHA: (92) implies: % 37.12/5.75 | (93) k1_zfmisc_1(all_110_4) = all_158_1 % 37.12/5.75 | % 37.12/5.75 | DELTA: instantiating (90) with fresh symbols all_160_0, all_160_1 gives: % 37.12/5.75 | (94) k1_zfmisc_1(all_110_4) = all_160_1 & $i(all_160_0) & $i(all_160_1) & % 37.12/5.75 | v13_waybel_0(all_160_0, all_110_5) & v2_waybel_0(all_160_0, all_110_5) % 37.12/5.75 | & v12_waybel_0(all_160_0, all_110_5) & m1_subset_1(all_160_0, % 37.12/5.75 | all_160_1) & v1_waybel_0(all_160_0, all_110_5) & ~ % 37.12/5.75 | v1_xboole_0(all_160_0) % 37.12/5.75 | % 37.12/5.75 | ALPHA: (94) implies: % 37.12/5.75 | (95) k1_zfmisc_1(all_110_4) = all_160_1 % 37.12/5.75 | % 37.12/5.75 | GROUND_INST: instantiating (10) with all_110_3, all_160_1, all_110_4, % 37.12/5.75 | simplifying with (29), (95) gives: % 37.12/5.75 | (96) all_160_1 = all_110_3 % 37.12/5.75 | % 37.12/5.75 | GROUND_INST: instantiating (10) with all_158_1, all_160_1, all_110_4, % 37.12/5.75 | simplifying with (93), (95) gives: % 37.12/5.75 | (97) all_160_1 = all_158_1 % 37.12/5.75 | % 37.12/5.75 | COMBINE_EQS: (96), (97) imply: % 37.12/5.75 | (98) all_158_1 = all_110_3 % 37.12/5.75 | % 37.12/5.75 | BETA: splitting (36) gives: % 37.12/5.75 | % 37.12/5.75 | Case 1: % 37.12/5.75 | | % 37.12/5.75 | | (99) v3_struct_0(all_110_7) % 37.12/5.75 | | % 37.12/5.75 | | GROUND_INST: instantiating (cc2_lattice3) with all_110_7, simplifying with % 37.12/5.75 | | (20), (21), (24), (99) gives: % 37.12/5.75 | | (100) $false % 37.12/5.75 | | % 37.12/5.75 | | CLOSE: (100) is inconsistent. % 37.12/5.75 | | % 37.12/5.75 | Case 2: % 37.12/5.75 | | % 37.12/5.75 | | (101) ? [v0: $i] : (k7_lattice3(all_110_7) = v0 & k8_waybel_0(v0) = % 37.12/5.75 | | all_110_6 & $i(v0) & $i(all_110_6)) % 37.12/5.75 | | % 37.12/5.75 | | DELTA: instantiating (101) with fresh symbol all_232_0 gives: % 37.12/5.75 | | (102) k7_lattice3(all_110_7) = all_232_0 & k8_waybel_0(all_232_0) = % 37.12/5.75 | | all_110_6 & $i(all_232_0) & $i(all_110_6) % 37.12/5.75 | | % 37.12/5.75 | | ALPHA: (102) implies: % 37.12/5.75 | | (103) $i(all_232_0) % 37.12/5.75 | | (104) k8_waybel_0(all_232_0) = all_110_6 % 37.12/5.75 | | (105) k7_lattice3(all_110_7) = all_232_0 % 37.12/5.75 | | % 37.12/5.75 | | BETA: splitting (34) gives: % 37.12/5.75 | | % 37.12/5.75 | | Case 1: % 37.12/5.75 | | | % 37.12/5.75 | | | % 37.12/5.75 | | | GROUND_INST: instantiating (8) with all_110_7, all_232_0, simplifying with % 37.12/5.75 | | | (20), (21), (24), (105) gives: % 37.12/5.75 | | | (106) v1_lattice3(all_232_0) % 37.12/5.75 | | | % 37.12/5.75 | | | GROUND_INST: instantiating (4) with all_110_7, all_232_0, simplifying with % 37.12/5.75 | | | (19), (21), (24), (105) gives: % 37.12/5.75 | | | (107) v1_yellow_0(all_232_0) % 37.12/5.75 | | | % 37.12/5.75 | | | GROUND_INST: instantiating (7) with all_110_7, all_232_0, simplifying with % 37.12/5.75 | | | (18), (21), (24), (105) gives: % 37.12/5.75 | | | (108) v4_orders_2(all_232_0) % 37.12/5.75 | | | % 37.12/5.75 | | | GROUND_INST: instantiating (6) with all_110_7, all_232_0, simplifying with % 37.12/5.75 | | | (17), (21), (24), (105) gives: % 37.12/5.75 | | | (109) v3_orders_2(all_232_0) % 37.12/5.75 | | | % 37.12/5.75 | | | GROUND_INST: instantiating (5) with all_110_7, all_232_0, simplifying with % 37.12/5.75 | | | (16), (21), (24), (105) gives: % 37.12/5.75 | | | (110) v2_orders_2(all_232_0) % 37.12/5.75 | | | % 37.12/5.75 | | | GROUND_INST: instantiating (3) with all_110_7, all_232_0, simplifying with % 37.12/5.75 | | | (21), (24), (105) gives: % 37.12/5.75 | | | (111) l1_orders_2(all_232_0) % 37.12/5.75 | | | % 37.12/5.75 | | | GROUND_INST: instantiating (t9_waybel13) with all_232_0, all_110_6, % 37.12/5.75 | | | simplifying with (103), (104), (106), (107), (108), (109), % 37.12/5.75 | | | (110), (111) gives: % 37.12/5.76 | | | (112) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (k2_yellow_1(all_110_6) % 37.12/5.76 | | | = v0 & k1_zfmisc_1(v1) = v2 & u1_struct_0(v0) = v1 & $i(v2) & % 37.12/5.76 | | | $i(v1) & $i(v0) & ! [v3: $i] : ! [v4: $i] : ( ~ % 37.12/5.76 | | | (k1_yellow_0(v0, v3) = v4) | ~ $i(v3) | ~ m1_subset_1(v3, % 37.12/5.76 | | | v2) | ~ v1_waybel_0(v3, v0) | v1_xboole_0(v3) | % 37.12/5.76 | | | (k3_tarski(v3) = v4 & $i(v4)))) % 37.12/5.76 | | | % 37.12/5.76 | | | DELTA: instantiating (112) with fresh symbols all_258_0, all_258_1, % 37.12/5.76 | | | all_258_2 gives: % 37.12/5.76 | | | (113) k2_yellow_1(all_110_6) = all_258_2 & k1_zfmisc_1(all_258_1) = % 37.12/5.76 | | | all_258_0 & u1_struct_0(all_258_2) = all_258_1 & $i(all_258_0) & % 37.12/5.76 | | | $i(all_258_1) & $i(all_258_2) & ! [v0: $i] : ! [v1: $i] : ( ~ % 37.12/5.76 | | | (k1_yellow_0(all_258_2, v0) = v1) | ~ $i(v0) | ~ % 37.12/5.76 | | | m1_subset_1(v0, all_258_0) | ~ v1_waybel_0(v0, all_258_2) | % 37.12/5.76 | | | v1_xboole_0(v0) | (k3_tarski(v0) = v1 & $i(v1))) % 37.12/5.76 | | | % 37.12/5.76 | | | ALPHA: (113) implies: % 37.12/5.76 | | | (114) u1_struct_0(all_258_2) = all_258_1 % 37.12/5.76 | | | (115) k1_zfmisc_1(all_258_1) = all_258_0 % 37.12/5.76 | | | (116) k2_yellow_1(all_110_6) = all_258_2 % 37.12/5.76 | | | (117) ! [v0: $i] : ! [v1: $i] : ( ~ (k1_yellow_0(all_258_2, v0) = v1) % 37.12/5.76 | | | | ~ $i(v0) | ~ m1_subset_1(v0, all_258_0) | ~ % 37.12/5.76 | | | v1_waybel_0(v0, all_258_2) | v1_xboole_0(v0) | (k3_tarski(v0) = % 37.12/5.76 | | | v1 & $i(v1))) % 37.12/5.76 | | | % 37.12/5.76 | | | GROUND_INST: instantiating (11) with all_110_5, all_258_2, all_110_6, % 37.12/5.76 | | | simplifying with (32), (116) gives: % 37.12/5.76 | | | (118) all_258_2 = all_110_5 % 37.12/5.76 | | | % 37.12/5.76 | | | REDUCE: (114), (118) imply: % 37.12/5.76 | | | (119) u1_struct_0(all_110_5) = all_258_1 % 37.12/5.76 | | | % 37.12/5.76 | | | GROUND_INST: instantiating (9) with all_110_4, all_258_1, all_110_5, % 37.12/5.76 | | | simplifying with (28), (119) gives: % 37.12/5.76 | | | (120) all_258_1 = all_110_4 % 37.12/5.76 | | | % 37.12/5.76 | | | REDUCE: (115), (120) imply: % 37.12/5.76 | | | (121) k1_zfmisc_1(all_110_4) = all_258_0 % 37.12/5.76 | | | % 37.12/5.76 | | | GROUND_INST: instantiating (10) with all_110_3, all_258_0, all_110_4, % 37.12/5.76 | | | simplifying with (29), (121) gives: % 37.12/5.76 | | | (122) all_258_0 = all_110_3 % 37.12/5.76 | | | % 37.12/5.76 | | | GROUND_INST: instantiating (117) with all_110_2, all_110_1, simplifying % 37.12/5.76 | | | with (15), (27) gives: % 37.12/5.76 | | | (123) ~ (k1_yellow_0(all_258_2, all_110_2) = all_110_1) | ~ % 37.12/5.76 | | | m1_subset_1(all_110_2, all_258_0) | ~ v1_waybel_0(all_110_2, % 37.12/5.76 | | | all_258_2) | (k3_tarski(all_110_2) = all_110_1 & $i(all_110_1)) % 37.12/5.76 | | | % 37.12/5.76 | | | BETA: splitting (123) gives: % 37.12/5.76 | | | % 37.12/5.76 | | | Case 1: % 37.12/5.76 | | | | % 37.12/5.76 | | | | (124) ~ (k1_yellow_0(all_258_2, all_110_2) = all_110_1) % 37.12/5.76 | | | | % 37.12/5.76 | | | | REDUCE: (118), (124) imply: % 37.12/5.76 | | | | (125) ~ (k1_yellow_0(all_110_5, all_110_2) = all_110_1) % 37.12/5.76 | | | | % 37.12/5.76 | | | | PRED_UNIFY: (31), (125) imply: % 37.12/5.76 | | | | (126) $false % 37.12/5.76 | | | | % 37.12/5.76 | | | | CLOSE: (126) is inconsistent. % 37.12/5.76 | | | | % 37.12/5.76 | | | Case 2: % 37.12/5.76 | | | | % 37.12/5.76 | | | | (127) ~ m1_subset_1(all_110_2, all_258_0) | ~ % 37.12/5.76 | | | | v1_waybel_0(all_110_2, all_258_2) | (k3_tarski(all_110_2) = % 37.12/5.76 | | | | all_110_1 & $i(all_110_1)) % 37.12/5.76 | | | | % 37.12/5.76 | | | | BETA: splitting (127) gives: % 37.12/5.76 | | | | % 37.12/5.76 | | | | Case 1: % 37.12/5.76 | | | | | % 37.12/5.76 | | | | | (128) ~ m1_subset_1(all_110_2, all_258_0) % 37.12/5.76 | | | | | % 37.12/5.76 | | | | | REDUCE: (122), (128) imply: % 37.12/5.76 | | | | | (129) ~ m1_subset_1(all_110_2, all_110_3) % 37.12/5.76 | | | | | % 37.12/5.76 | | | | | PRED_UNIFY: (23), (129) imply: % 37.12/5.76 | | | | | (130) $false % 37.12/5.76 | | | | | % 37.12/5.76 | | | | | CLOSE: (130) is inconsistent. % 37.12/5.76 | | | | | % 37.12/5.76 | | | | Case 2: % 37.12/5.76 | | | | | % 37.12/5.76 | | | | | (131) ~ v1_waybel_0(all_110_2, all_258_2) | (k3_tarski(all_110_2) % 37.12/5.76 | | | | | = all_110_1 & $i(all_110_1)) % 37.12/5.76 | | | | | % 37.12/5.76 | | | | | BETA: splitting (131) gives: % 37.12/5.76 | | | | | % 37.12/5.76 | | | | | Case 1: % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | (132) ~ v1_waybel_0(all_110_2, all_258_2) % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | REDUCE: (118), (132) imply: % 37.12/5.76 | | | | | | (133) ~ v1_waybel_0(all_110_2, all_110_5) % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | PRED_UNIFY: (22), (133) imply: % 37.12/5.76 | | | | | | (134) $false % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | CLOSE: (134) is inconsistent. % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | Case 2: % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | (135) k3_tarski(all_110_2) = all_110_1 & $i(all_110_1) % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | ALPHA: (135) implies: % 37.12/5.76 | | | | | | (136) k3_tarski(all_110_2) = all_110_1 % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | GROUND_INST: instantiating (12) with all_110_0, all_110_1, % 37.12/5.76 | | | | | | all_110_2, simplifying with (33), (136) gives: % 37.12/5.76 | | | | | | (137) all_110_0 = all_110_1 % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | REDUCE: (14), (137) imply: % 37.12/5.76 | | | | | | (138) $false % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | | CLOSE: (138) is inconsistent. % 37.12/5.76 | | | | | | % 37.12/5.76 | | | | | End of split % 37.12/5.76 | | | | | % 37.12/5.76 | | | | End of split % 37.12/5.76 | | | | % 37.12/5.76 | | | End of split % 37.12/5.76 | | | % 37.12/5.76 | | Case 2: % 37.12/5.76 | | | % 37.12/5.76 | | | (139) v1_xboole_0(all_110_3) % 37.12/5.76 | | | % 37.12/5.76 | | | GROUND_INST: instantiating (fc1_subset_1) with all_110_4, all_110_3, % 37.12/5.76 | | | simplifying with (29), (89), (139) gives: % 37.12/5.76 | | | (140) $false % 37.12/5.76 | | | % 37.12/5.76 | | | CLOSE: (140) is inconsistent. % 37.12/5.76 | | | % 37.12/5.76 | | End of split % 37.12/5.76 | | % 37.12/5.76 | End of split % 37.12/5.76 | % 37.12/5.76 End of proof % 37.12/5.76 % SZS output end Proof for theBenchmark % 37.12/5.76 % 37.12/5.76 5149ms %------------------------------------------------------------------------------