%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP367_1 : TPTP v8.1.2. Released v8.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n004.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 04:11:53 EDT 2023 % Result : Theorem 63.71s 9.36s % Output : Proof 100.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : ITP367_1 : TPTP v8.1.2. Released v8.0.0. % 0.00/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.32 % Computer : n004.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Sun Aug 27 11:45:07 EDT 2023 % 0.10/0.32 % CPUTime : % 0.17/0.62 ________ _____ % 0.17/0.62 ___ __ \_________(_)________________________________ % 0.17/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.17/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.17/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.17/0.62 % 0.17/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.17/0.62 (2023-06-19) % 0.17/0.62 % 0.17/0.62 (c) Philipp Rümmer, 2009-2023 % 0.17/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.17/0.62 Amanda Stjerna. % 0.17/0.62 Free software under BSD-3-Clause. % 0.17/0.62 % 0.17/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.17/0.62 % 0.17/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.17/0.64 Running up to 7 provers in parallel. % 0.17/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.17/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.17/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.17/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.17/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.17/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.17/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 20.95/3.65 Prover 4: Preprocessing ... % 21.54/3.73 Prover 6: Preprocessing ... % 21.54/3.73 Prover 2: Preprocessing ... % 21.54/3.76 Prover 1: Preprocessing ... % 21.83/3.80 Prover 0: Preprocessing ... % 22.65/3.91 Prover 3: Preprocessing ... % 23.07/3.93 Prover 5: Preprocessing ... % 50.36/7.60 Prover 3: Warning: ignoring some quantifiers % 50.36/7.74 Prover 3: Constructing countermodel ... % 50.36/7.77 Prover 1: Warning: ignoring some quantifiers % 50.90/7.81 Prover 6: Proving ... % 54.64/8.13 Prover 1: Constructing countermodel ... % 63.71/9.36 Prover 3: proved (8705ms) % 63.71/9.36 % 63.71/9.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 63.71/9.36 % 63.71/9.36 Prover 6: stopped % 63.71/9.38 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 63.71/9.38 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 65.24/9.57 Prover 4: Warning: ignoring some quantifiers % 65.97/9.81 Prover 0: Proving ... % 65.97/9.81 Prover 0: stopped % 65.97/9.87 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 66.89/9.94 Prover 4: Constructing countermodel ... % 69.66/10.20 Prover 5: Proving ... % 69.66/10.20 Prover 5: stopped % 69.66/10.21 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 72.84/10.58 Prover 7: Preprocessing ... % 72.84/10.85 Prover 2: Proving ... % 72.84/10.85 Prover 2: stopped % 72.84/10.85 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 76.52/11.05 Prover 8: Preprocessing ... % 78.82/11.38 Prover 10: Preprocessing ... % 81.60/11.75 Prover 11: Preprocessing ... % 83.37/11.97 Prover 13: Preprocessing ... % 89.76/12.80 Prover 1: Found proof (size 117) % 89.76/12.80 Prover 1: proved (12155ms) % 89.76/12.80 Prover 4: stopped % 89.76/12.80 Prover 13: stopped % 90.07/12.92 Prover 7: Warning: ignoring some quantifiers % 91.85/13.09 Prover 8: Warning: ignoring some quantifiers % 91.85/13.15 Prover 10: Warning: ignoring some quantifiers % 91.85/13.16 Prover 7: Constructing countermodel ... % 92.82/13.28 Prover 8: Constructing countermodel ... % 93.38/13.37 Prover 10: Constructing countermodel ... % 93.82/13.42 Prover 8: stopped % 93.82/13.43 Prover 7: stopped % 94.56/13.59 Prover 10: stopped % 97.36/14.22 Prover 11: Warning: ignoring some quantifiers % 98.50/14.44 Prover 11: Constructing countermodel ... % 99.31/14.63 Prover 11: stopped % 99.31/14.63 % 99.31/14.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 99.31/14.63 % 99.45/14.69 % SZS output start Proof for theBenchmark % 99.72/14.75 Assumptions after simplification: % 99.72/14.75 --------------------------------- % 99.72/14.75 % 99.72/14.75 (axiom20) % 99.84/14.80 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$(sup$) & % 99.84/14.80 A_ltln_set_bool_fun$(finite$) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : % 99.84/14.80 ! [v2: A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 99.84/14.80 (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 99.84/14.80 A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : ? [v6: % 99.84/14.80 any] : (fun_app$a(finite$, v3) = v6 & fun_app$a(finite$, v1) = v5 & % 99.84/14.80 fun_app$a(finite$, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | v6 = 0))) % 99.84/14.80 % 99.84/14.80 (axiom22) % 99.84/14.80 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$(sup$) & % 99.84/14.80 A_ltln_set_bool_fun$(finite$) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : % 99.84/14.80 ! [v2: A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 99.84/14.80 (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 99.84/14.80 A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : % 99.84/14.80 (fun_app$a(finite$, v3) = v5 & fun_app$a(finite$, v0) = v4 & ( ~ (v5 = 0) | % 99.84/14.80 v4 = 0))) % 99.84/14.80 % 99.84/14.80 (axiom260) % 99.84/14.81 A_ltln_set_bool_fun$(finite$) & A_ltln_set_a_ltln_set_bool_fun_fun$(less_eq$) % 99.84/14.81 & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: A_ltln_set_bool_fun$] % 99.84/14.81 : ( ~ (fun_app$g(less_eq$, v0) = v2) | ~ (fun_app$a(v2, v1) = 0) | ~ % 99.84/14.81 A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v3: any] : ? [v4: any] : % 99.84/14.81 (fun_app$a(finite$, v1) = v4 & fun_app$a(finite$, v0) = v3 & ( ~ (v4 = 0) | % 99.84/14.81 v3 = 0))) % 99.84/14.81 % 99.84/14.81 (axiom262) % 99.84/14.82 A_ltln_set_bool_fun$(finite$) & A_ltln_set_a_ltln_set_bool_fun_fun$(less_eq$) % 99.84/14.82 & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: A_ltln_set_bool_fun$] % 99.84/14.82 : ( ~ (fun_app$g(less_eq$, v1) = v2) | ~ (fun_app$a(v2, v0) = 0) | ~ % 99.84/14.82 A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v3: any] : ? [v4: any] : % 99.84/14.82 (fun_app$a(finite$, v1) = v4 & fun_app$a(finite$, v0) = v3 & ( ~ (v3 = 0) | % 99.84/14.82 v4 = 0))) % 99.84/14.82 % 99.84/14.82 (axiom287) % 99.84/14.82 A_ltln_a_ltln_set_fun$(subformulas_mu$) & A_ltln_set_bool_fun$(finite$) & ! % 99.84/14.82 [v0: A_ltln$] : ! [v1: A_ltln_set$] : ( ~ (fun_app$h(subformulas_mu$, v0) = % 99.84/14.82 v1) | ~ A_ltln$(v0) | fun_app$a(finite$, v1) = 0) % 99.84/14.82 % 99.84/14.82 (axiom288) % 99.84/14.82 A_ltln_a_ltln_set_fun$(subformulas_nu$) & A_ltln_set_bool_fun$(finite$) & ! % 99.84/14.82 [v0: A_ltln$] : ! [v1: A_ltln_set$] : ( ~ (fun_app$h(subformulas_nu$, v0) = % 99.84/14.82 v1) | ~ A_ltln$(v0) | fun_app$a(finite$, v1) = 0) % 99.84/14.82 % 99.84/14.83 (axiom4) % 100.10/14.83 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$(sup$) & % 100.10/14.83 A_ltln_set_bool_fun$(finite$) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : % 100.10/14.83 ! [v2: A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 100.10/14.83 (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 100.10/14.83 A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : ? [v6: % 100.10/14.83 any] : (fun_app$a(finite$, v3) = v6 & fun_app$a(finite$, v1) = v5 & % 100.10/14.83 fun_app$a(finite$, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | v6 = 0))) & ! % 100.10/14.83 [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: A_ltln_set_a_ltln_set_fun$] % 100.10/14.83 : ! [v3: A_ltln_set$] : ( ~ (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, % 100.10/14.83 v1) = v3) | ~ A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? % 100.10/14.83 [v5: any] : ? [v6: any] : (fun_app$a(finite$, v3) = v4 & fun_app$a(finite$, % 100.10/14.83 v1) = v6 & fun_app$a(finite$, v0) = v5 & ( ~ (v4 = 0) | (v6 = 0 & v5 = % 100.10/14.83 0)))) % 100.10/14.83 % 100.10/14.83 (axiom64) % 100.10/14.84 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$(sup$) & % 100.10/14.84 A_ltln_set_bool_fun$(finite$) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : % 100.10/14.84 ! [v2: A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 100.10/14.84 (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 100.10/14.84 A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : ? [v6: % 100.10/14.84 any] : (fun_app$a(finite$, v3) = v6 & fun_app$a(finite$, v1) = v5 & % 100.10/14.84 fun_app$a(finite$, v0) = v4 & ( ~ (v6 = 0) | (v5 = 0 & v4 = 0)))) & ! % 100.10/14.84 [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: A_ltln_set_a_ltln_set_fun$] % 100.10/14.84 : ! [v3: A_ltln_set$] : ( ~ (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, % 100.10/14.84 v1) = v3) | ~ A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? % 100.10/14.84 [v5: any] : ? [v6: any] : (fun_app$a(finite$, v3) = v4 & fun_app$a(finite$, % 100.10/14.84 v1) = v6 & fun_app$a(finite$, v0) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | v4 % 100.10/14.84 = 0))) % 100.10/14.84 % 100.10/14.84 (axiom69) % 100.10/14.84 A_ltln_a_ltln_set_fun$(subformulas_nu$) & A_ltln$(phi$) & A_ltln_set$(y$) & % 100.10/14.84 A_ltln_set_a_ltln_set_bool_fun_fun$(less_eq$) & ? [v0: A_ltln_set_bool_fun$] % 100.10/14.84 : ? [v1: A_ltln_set$] : (fun_app$g(less_eq$, y$) = v0 & % 100.10/14.84 fun_app$h(subformulas_nu$, phi$) = v1 & fun_app$a(v0, v1) = 0 & % 100.10/14.84 A_ltln_set$(v1) & A_ltln_set_bool_fun$(v0)) % 100.10/14.84 % 100.10/14.84 (axiom70) % 100.10/14.84 A_ltln_a_ltln_set_fun$(subformulas_mu$) & A_ltln$(phi$) & A_ltln_set$(x$) & % 100.10/14.84 A_ltln_set_a_ltln_set_bool_fun_fun$(less_eq$) & ? [v0: A_ltln_set_bool_fun$] % 100.10/14.84 : ? [v1: A_ltln_set$] : (fun_app$g(less_eq$, x$) = v0 & % 100.10/14.84 fun_app$h(subformulas_mu$, phi$) = v1 & fun_app$a(v0, v1) = 0 & % 100.10/14.84 A_ltln_set$(v1) & A_ltln_set_bool_fun$(v0)) % 100.10/14.84 % 100.10/14.84 (conjecture2) % 100.10/14.84 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$(sup$) & A_ltln_set$(y$) & % 100.10/14.84 A_ltln_set$(x$) & A_ltln_set_bool_fun$(finite$) & ? [v0: % 100.10/14.84 A_ltln_set_a_ltln_set_fun$] : ? [v1: A_ltln_set$] : ? [v2: int] : ( ~ (v2 % 100.10/14.84 = 0) & fun_app$d(sup$, x$) = v0 & fun_app$c(v0, y$) = v1 & % 100.10/14.84 fun_app$a(finite$, v1) = v2 & A_ltln_set_a_ltln_set_fun$(v0) & % 100.10/14.84 A_ltln_set$(v1)) % 100.10/14.84 % 100.10/14.84 (function-axioms) % 100.26/14.87 ! [v0: A_ltln_set_set_a_ltln_set_fun$] : ! [v1: % 100.26/14.87 A_ltln_set_set_a_ltln_set_fun$] : ! [v2: A_ltln_set$] : ! [v3: % 100.26/14.87 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$] : (v1 = v0 | ~ (fold$a(v3, v2) = % 100.26/14.87 v1) | ~ (fold$a(v3, v2) = v0)) & ! [v0: A_ltln_set_set_set$] : ! [v1: % 100.26/14.87 A_ltln_set_set_set$] : ! [v2: A_ltln_set_set_set$] : ! [v3: % 100.26/14.87 A_ltln_set_set_set$] : (v1 = v0 | ~ (minus$(v3, v2) = v1) | ~ (minus$(v3, % 100.26/14.87 v2) = v0)) & ! [v0: A_ltln_set_a_ltln_set_fun$] : ! [v1: % 100.26/14.87 A_ltln_set_a_ltln_set_fun$] : ! [v2: A_ltln$] : ! [v3: % 100.26/14.87 A_ltln_a_ltln_set_a_ltln_set_fun_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = % 100.26/14.87 v1) | ~ (fun_app$n(v3, v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_set_a_ltln_set_set_fun$] : ! [v1: % 100.26/14.87 A_ltln_set_set_a_ltln_set_set_fun$] : ! [v2: A_ltln_set$] : ! [v3: % 100.26/14.87 A_ltln_set_a_ltln_set_set_a_ltln_set_set_fun_fun$] : (v1 = v0 | ~ % 100.26/14.87 (fun_app$m(v3, v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_set_set$] : ! [v1: A_ltln_set_set_set$] : ! [v2: % 100.26/14.87 A_ltln_set_set_set$] : ! [v3: A_ltln_set_set$] : (v1 = v0 | ~ (insert$(v3, % 100.26/14.87 v2) = v1) | ~ (insert$(v3, v2) = v0)) & ! [v0: A_ltln_set_set_set$] : % 100.26/14.87 ! [v1: A_ltln_set_set_set$] : ! [v2: A_ltln_set_set_set$] : ! [v3: % 100.26/14.87 A_ltln_set_set_set$] : (v1 = v0 | ~ (sup$b(v3, v2) = v1) | ~ (sup$b(v3, % 100.26/14.87 v2) = v0)) & ! [v0: A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! % 100.26/14.87 [v2: A_ltln$] : ! [v3: A_ltln_a_ltln_bool_fun_fun$] : (v1 = v0 | ~ % 100.26/14.87 (fun_app$l(v3, v2) = v1) | ~ (fun_app$l(v3, v2) = v0)) & ! [v0: % 100.26/14.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 100.26/14.87 A_ltln_set_set_set$] : ! [v3: A_ltln_set_set_set$] : (v1 = v0 | ~ % 100.26/14.87 (less_eq$b(v3, v2) = v1) | ~ (less_eq$b(v3, v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: A_ltln_a_ltln_set_fun$] : ! % 100.26/14.87 [v3: A_ltln_set$] : (v1 = v0 | ~ (bind$c(v3, v2) = v1) | ~ (bind$c(v3, v2) = % 100.26/14.87 v0)) & ! [v0: A_ltln_set_set$] : ! [v1: A_ltln_set_set$] : ! [v2: % 100.26/14.87 A_ltln_set_a_ltln_set_set_fun$] : ! [v3: A_ltln_set_set$] : (v1 = v0 | ~ % 100.26/14.87 (bind$b(v3, v2) = v1) | ~ (bind$b(v3, v2) = v0)) & ! [v0: A_ltln_set_set$] % 100.26/14.87 : ! [v1: A_ltln_set_set$] : ! [v2: A_ltln_set$] : ! [v3: % 100.26/14.87 A_ltln_set_a_ltln_set_set_fun$] : (v1 = v0 | ~ (fun_app$k(v3, v2) = v1) | % 100.26/14.87 ~ (fun_app$k(v3, v2) = v0)) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : % 100.26/14.87 ! [v2: A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set_set$] : (v1 = v0 | ~ % 100.26/14.87 (bind$a(v3, v2) = v1) | ~ (bind$a(v3, v2) = v0)) & ! [v0: A_ltln_set_set$] % 100.26/14.87 : ! [v1: A_ltln_set_set$] : ! [v2: A_ltln_a_ltln_set_set_fun$] : ! [v3: % 100.26/14.87 A_ltln_set$] : (v1 = v0 | ~ (bind$(v3, v2) = v1) | ~ (bind$(v3, v2) = v0)) % 100.26/14.87 & ! [v0: A_ltln_set_set$] : ! [v1: A_ltln_set_set$] : ! [v2: A_ltln$] : ! % 100.26/14.87 [v3: A_ltln_a_ltln_set_set_fun$] : (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | ~ % 100.26/14.87 (fun_app$j(v3, v2) = v0)) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! % 100.26/14.87 [v2: A_ltln_set_set$] : ! [v3: A_ltln_set_set_a_ltln_set_fun$] : (v1 = v0 | % 100.26/14.87 ~ (fun_app$i(v3, v2) = v1) | ~ (fun_app$i(v3, v2) = v0)) & ! [v0: % 100.26/14.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 100.26/14.87 A_ltln_set_set_set$] : ! [v3: A_ltln_set_set$] : (v1 = v0 | ~ % 100.26/14.87 (member$b(v3, v2) = v1) | ~ (member$b(v3, v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_bool_fun$] : ! [v1: A_ltln_set_bool_fun$] : ! [v2: A_ltln_set$] % 100.26/14.87 : ! [v3: A_ltln_set_a_ltln_set_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$g(v3, % 100.26/14.87 v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! [v0: A_ltln_set$] : ! % 100.26/14.87 [v1: A_ltln_set$] : ! [v2: A_ltln$] : ! [v3: A_ltln_a_ltln_set_fun$] : (v1 = % 100.26/14.87 v0 | ~ (fun_app$h(v3, v2) = v1) | ~ (fun_app$h(v3, v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_a_ltln_set_fun$] : ! [v1: A_ltln_set_a_ltln_set_fun$] : ! [v2: % 100.26/14.87 A_ltln_set$] : ! [v3: A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$] : (v1 = v0 % 100.26/14.87 | ~ (fun_app$d(v3, v2) = v1) | ~ (fun_app$d(v3, v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: A_ltln_set$] : ! [v3: % 100.26/14.87 A_ltln_set_a_ltln_set_fun$] : (v1 = v0 | ~ (fun_app$c(v3, v2) = v1) | ~ % 100.26/14.87 (fun_app$c(v3, v2) = v0)) & ! [v0: A_ltln_set_set_a_ltln_set_set_fun$] : ! % 100.26/14.87 [v1: A_ltln_set_set_a_ltln_set_set_fun$] : ! [v2: A_ltln_set_set$] : ! [v3: % 100.26/14.87 A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$] : (v1 = v0 | ~ % 100.26/14.87 (fun_app$f(v3, v2) = v1) | ~ (fun_app$f(v3, v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_set$] : ! [v1: A_ltln_set_set$] : ! [v2: A_ltln_set_set$] : ! % 100.26/14.87 [v3: A_ltln_set_set_a_ltln_set_set_fun$] : (v1 = v0 | ~ (fun_app$e(v3, v2) = % 100.26/14.87 v1) | ~ (fun_app$e(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 100.26/14.87 MultipleValueBool] : ! [v2: A_ltln_set_set$] : ! [v3: % 100.26/14.87 A_ltln_set_set_bool_fun$] : (v1 = v0 | ~ (fun_app$b(v3, v2) = v1) | ~ % 100.26/14.87 (fun_app$b(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 100.26/14.87 MultipleValueBool] : ! [v2: A_ltln$] : ! [v3: A_ltln_bool_fun$] : (v1 = v0 % 100.26/14.87 | ~ (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, v2) = v0)) & ! [v0: % 100.26/14.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_ltln_set$] : ! % 100.26/14.87 [v3: A_ltln_set_bool_fun$] : (v1 = v0 | ~ (fun_app$a(v3, v2) = v1) | ~ % 100.26/14.87 (fun_app$a(v3, v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$] : ! [v1: % 100.26/14.87 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$] : ! [v2: % 100.26/14.87 A_ltln_a_ltln_set_a_ltln_set_fun_fun$] : (v1 = v0 | ~ (fold$(v2) = v1) | ~ % 100.26/14.87 (fold$(v2) = v0)) & ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! [v2: % 100.26/14.87 A_ltln_set$] : (v1 = v0 | ~ (the_elem$(v2) = v1) | ~ (the_elem$(v2) = v0)) % 100.26/14.87 & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 100.26/14.87 A_ltln_a_ltln_set_a_ltln_set_fun_fun$] : (v1 = v0 | ~ (comp_fun_idem$c(v2) % 100.26/14.87 = v1) | ~ (comp_fun_idem$c(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 100.26/14.87 [v1: MultipleValueBool] : ! [v2: % 100.26/14.87 A_ltln_set_a_ltln_set_set_a_ltln_set_set_fun_fun$] : (v1 = v0 | ~ % 100.26/14.87 (comp_fun_idem$b(v2) = v1) | ~ (comp_fun_idem$b(v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_set$] : ! [v1: A_ltln_set_set$] : ! [v2: A_ltln_set_set_set$] : % 100.26/14.87 (v1 = v0 | ~ (sup_fin$(v2) = v1) | ~ (sup_fin$(v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_set_bool_fun$] : ! [v1: A_ltln_set_set_bool_fun$] : ! [v2: % 100.26/14.87 A_ltln_set_set$] : (v1 = v0 | ~ (less_eq$a(v2) = v1) | ~ (less_eq$a(v2) = % 100.26/14.87 v0)) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 100.26/14.87 A_ltln_bool_fun$] : (v1 = v0 | ~ (collect$a(v2) = v1) | ~ (collect$a(v2) = % 100.26/14.87 v0)) & ! [v0: A_ltln_set_set$] : ! [v1: A_ltln_set_set$] : ! [v2: % 100.26/14.87 A_ltln_set_bool_fun$] : (v1 = v0 | ~ (collect$(v2) = v1) | ~ (collect$(v2) % 100.26/14.87 = v0)) & ! [v0: A_ltln_set_set_bool_fun$] : ! [v1: % 100.26/14.87 A_ltln_set_set_bool_fun$] : ! [v2: A_ltln_set_set$] : (v1 = v0 | ~ % 100.26/14.87 (disjnt$(v2) = v1) | ~ (disjnt$(v2) = v0)) & ! [v0: A_ltln_set_set$] : ! % 100.26/14.87 [v1: A_ltln_set_set$] : ! [v2: A_ltln_set_set_set$] : (v1 = v0 | ~ % 100.26/14.87 (inf_fin$(v2) = v1) | ~ (inf_fin$(v2) = v0)) & ! [v0: MultipleValueBool] : % 100.26/14.87 ! [v1: MultipleValueBool] : ! [v2: A_ltln_set_set_set$] : (v1 = v0 | ~ % 100.26/14.87 (finite$b(v2) = v1) | ~ (finite$b(v2) = v0)) & ! [v0: MultipleValueBool] : % 100.26/14.87 ! [v1: MultipleValueBool] : ! [v2: % 100.26/14.87 A_ltln_set_a_ltln_set_a_ltln_set_fun_fun$] : (v1 = v0 | ~ % 100.26/14.87 (comp_fun_idem$a(v2) = v1) | ~ (comp_fun_idem$a(v2) = v0)) & ! [v0: % 100.26/14.87 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 100.26/14.87 A_ltln_set_set_a_ltln_set_set_a_ltln_set_set_fun_fun$] : (v1 = v0 | ~ % 100.26/14.87 (comp_fun_idem$(v2) = v1) | ~ (comp_fun_idem$(v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_a_ltln_set_fun$] : ! [v1: A_ltln_set_a_ltln_set_fun$] : ! [v2: % 100.26/14.87 A_ltln_bool_fun$] : (v1 = v0 | ~ (filter$a(v2) = v1) | ~ (filter$a(v2) = % 100.26/14.87 v0)) & ! [v0: A_ltln_set_set_a_ltln_set_set_fun$] : ! [v1: % 100.26/14.87 A_ltln_set_set_a_ltln_set_set_fun$] : ! [v2: A_ltln_set_bool_fun$] : (v1 = % 100.26/14.87 v0 | ~ (filter$(v2) = v1) | ~ (filter$(v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_bool_fun$] : ! [v1: A_ltln_set_bool_fun$] : ! [v2: % 100.26/14.87 A_ltln_set_set$] : (v1 = v0 | ~ (uu$(v2) = v1) | ~ (uu$(v2) = v0)) & ! % 100.26/14.87 [v0: A_ltln_set_set_bool_fun$] : ! [v1: A_ltln_set_set_bool_fun$] : ! [v2: % 100.26/14.87 A_ltln_set$] : (v1 = v0 | ~ (member$a(v2) = v1) | ~ (member$a(v2) = v0)) & % 100.26/14.87 ! [v0: A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: A_ltln_set$] : % 100.26/14.87 (v1 = v0 | ~ (uua$(v2) = v1) | ~ (uua$(v2) = v0)) & ! [v0: % 100.26/14.87 A_ltln_set_bool_fun$] : ! [v1: A_ltln_set_bool_fun$] : ! [v2: A_ltln$] : % 100.26/14.87 (v1 = v0 | ~ (member$(v2) = v1) | ~ (member$(v2) = v0)) % 100.26/14.87 % 100.26/14.87 Further assumptions not needed in the proof: % 100.26/14.87 -------------------------------------------- % 100.26/14.87 axiom0, axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, % 100.26/14.87 axiom105, axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, % 100.26/14.87 axiom112, axiom113, axiom114, axiom115, axiom116, axiom117, axiom118, axiom119, % 100.26/14.87 axiom12, axiom120, axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, % 100.26/14.87 axiom127, axiom128, axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, % 100.26/14.87 axiom134, axiom135, axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, % 100.26/14.87 axiom141, axiom142, axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, % 100.26/14.87 axiom149, axiom15, axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, % 100.26/14.87 axiom156, axiom157, axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, % 100.26/14.87 axiom163, axiom164, axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, % 100.26/14.87 axiom170, axiom171, axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, % 100.26/14.87 axiom178, axiom179, axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, % 100.26/14.87 axiom185, axiom186, axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, % 100.26/14.87 axiom192, axiom193, axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, % 100.26/14.87 axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, % 100.26/14.87 axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, axiom214, % 100.26/14.87 axiom215, axiom216, axiom217, axiom218, axiom219, axiom220, axiom221, axiom222, % 100.26/14.87 axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, axiom23, % 100.26/14.87 axiom230, axiom231, axiom232, axiom233, axiom234, axiom235, axiom236, axiom237, % 100.26/14.87 axiom238, axiom239, axiom24, axiom240, axiom241, axiom242, axiom243, axiom244, % 100.26/14.87 axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, axiom251, % 100.26/14.87 axiom252, axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, axiom259, % 100.26/14.87 axiom26, axiom261, axiom263, axiom264, axiom265, axiom266, axiom267, axiom268, % 100.26/14.87 axiom269, axiom27, axiom270, axiom271, axiom272, axiom273, axiom274, axiom275, % 100.26/14.87 axiom276, axiom277, axiom278, axiom279, axiom28, axiom280, axiom281, axiom282, % 100.26/14.87 axiom283, axiom284, axiom285, axiom286, axiom289, axiom29, axiom290, axiom291, % 100.26/14.87 axiom292, axiom293, axiom294, axiom295, axiom296, axiom297, axiom298, axiom299, % 100.26/14.87 axiom3, axiom30, axiom300, axiom301, axiom302, axiom303, axiom304, axiom305, % 100.26/14.87 axiom306, axiom307, axiom308, axiom309, axiom31, axiom310, axiom311, axiom312, % 100.26/14.87 axiom313, axiom314, axiom315, axiom316, axiom317, axiom318, axiom319, axiom32, % 100.26/14.87 axiom320, axiom321, axiom322, axiom323, axiom324, axiom325, axiom326, axiom327, % 100.26/14.87 axiom328, axiom329, axiom33, axiom330, axiom331, axiom332, axiom333, axiom334, % 100.26/14.87 axiom335, axiom336, axiom337, axiom338, axiom339, axiom34, axiom340, axiom341, % 100.26/14.87 axiom342, axiom343, axiom344, axiom345, axiom346, axiom347, axiom348, axiom349, % 100.26/14.87 axiom35, axiom350, axiom351, axiom352, axiom353, axiom354, axiom355, axiom356, % 100.26/14.87 axiom357, axiom358, axiom359, axiom36, axiom360, axiom361, axiom362, axiom363, % 100.26/14.87 axiom364, axiom365, axiom366, axiom367, axiom368, axiom369, axiom37, axiom370, % 100.26/14.87 axiom371, axiom372, axiom373, axiom374, axiom375, axiom376, axiom377, axiom378, % 100.26/14.87 axiom379, axiom38, axiom380, axiom381, axiom382, axiom383, axiom384, axiom385, % 100.26/14.87 axiom386, axiom387, axiom388, axiom389, axiom39, axiom390, axiom391, axiom392, % 100.26/14.87 axiom393, axiom394, axiom395, axiom396, axiom397, axiom398, axiom399, axiom40, % 100.26/14.87 axiom400, axiom401, axiom402, axiom403, axiom404, axiom405, axiom406, axiom407, % 100.26/14.87 axiom408, axiom409, axiom41, axiom410, axiom411, axiom412, axiom413, axiom414, % 100.26/14.87 axiom415, axiom416, axiom417, axiom418, axiom419, axiom42, axiom420, axiom421, % 100.26/14.87 axiom422, axiom423, axiom424, axiom425, axiom426, axiom427, axiom428, axiom429, % 100.26/14.87 axiom43, axiom430, axiom431, axiom432, axiom433, axiom434, axiom435, axiom436, % 100.26/14.87 axiom437, axiom438, axiom439, axiom44, axiom440, axiom441, axiom442, axiom443, % 100.26/14.87 axiom444, axiom445, axiom446, axiom447, axiom448, axiom449, axiom45, axiom450, % 100.26/14.87 axiom451, axiom452, axiom453, axiom454, axiom455, axiom456, axiom457, axiom458, % 100.26/14.87 axiom459, axiom46, axiom460, axiom461, axiom462, axiom463, axiom464, axiom465, % 100.26/14.87 axiom466, axiom467, axiom468, axiom469, axiom47, axiom470, axiom471, axiom472, % 100.26/14.87 axiom473, axiom474, axiom475, axiom476, axiom477, axiom478, axiom479, axiom48, % 100.26/14.87 axiom480, axiom481, axiom482, axiom483, axiom484, axiom485, axiom486, axiom487, % 100.26/14.87 axiom488, axiom489, axiom49, axiom490, axiom491, axiom492, axiom493, axiom494, % 100.26/14.87 axiom495, axiom496, axiom497, axiom498, axiom499, axiom5, axiom50, axiom500, % 100.26/14.87 axiom501, axiom502, axiom503, axiom504, axiom505, axiom506, axiom507, axiom508, % 100.26/14.87 axiom509, axiom51, axiom510, axiom511, axiom512, axiom513, axiom514, axiom515, % 100.26/14.87 axiom516, axiom517, axiom518, axiom519, axiom52, axiom520, axiom521, axiom522, % 100.26/14.87 axiom523, axiom524, axiom525, axiom526, axiom527, axiom528, axiom529, axiom53, % 100.26/14.87 axiom530, axiom531, axiom532, axiom533, axiom534, axiom535, axiom536, axiom537, % 100.26/14.87 axiom538, axiom539, axiom54, axiom540, axiom541, axiom542, axiom543, axiom544, % 100.26/14.87 axiom545, axiom546, axiom547, axiom548, axiom549, axiom55, axiom550, axiom551, % 100.26/14.87 axiom552, axiom553, axiom554, axiom555, axiom556, axiom557, axiom558, axiom559, % 100.26/14.87 axiom56, axiom560, axiom561, axiom562, axiom563, axiom564, axiom565, axiom566, % 100.26/14.87 axiom567, axiom568, axiom569, axiom57, axiom570, axiom571, axiom572, axiom573, % 100.26/14.87 axiom574, axiom575, axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, % 100.26/14.87 axiom581, axiom582, axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, % 100.26/14.87 axiom589, axiom59, axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, % 100.26/14.87 axiom596, axiom597, axiom598, axiom599, axiom6, axiom60, axiom600, axiom601, % 100.26/14.87 axiom602, axiom603, axiom604, axiom605, axiom606, axiom607, axiom608, axiom609, % 100.26/14.87 axiom61, axiom610, axiom611, axiom612, axiom613, axiom614, axiom615, axiom616, % 100.26/14.87 axiom617, axiom618, axiom619, axiom62, axiom620, axiom621, axiom622, axiom623, % 100.26/14.87 axiom624, axiom625, axiom626, axiom627, axiom628, axiom629, axiom63, axiom630, % 100.26/14.87 axiom631, axiom632, axiom633, axiom634, axiom635, axiom636, axiom637, axiom638, % 100.26/14.87 axiom639, axiom65, axiom66, axiom67, axiom68, axiom7, axiom71, axiom72, axiom73, % 100.26/14.87 axiom74, axiom75, axiom76, axiom77, axiom78, axiom79, axiom8, axiom80, axiom81, % 100.26/14.87 axiom82, axiom83, axiom84, axiom85, axiom86, axiom87, axiom88, axiom89, axiom9, % 100.26/14.87 axiom90, axiom91, axiom92, axiom93, axiom94, axiom95, axiom96, axiom97, axiom98, % 100.26/14.87 axiom99 % 100.26/14.87 % 100.26/14.87 Those formulas are unsatisfiable: % 100.26/14.87 --------------------------------- % 100.26/14.87 % 100.26/14.87 Begin of proof % 100.26/14.88 | % 100.26/14.88 | ALPHA: (axiom4) implies: % 100.26/14.88 | (1) ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 100.26/14.88 | A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 100.26/14.88 | (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 100.26/14.88 | A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : % 100.26/14.88 | ? [v6: any] : (fun_app$a(finite$, v3) = v4 & fun_app$a(finite$, v1) = % 100.26/14.88 | v6 & fun_app$a(finite$, v0) = v5 & ( ~ (v4 = 0) | (v6 = 0 & v5 = % 100.26/14.88 | 0)))) % 100.26/14.88 | % 100.26/14.88 | ALPHA: (axiom20) implies: % 100.26/14.88 | (2) ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 100.26/14.88 | A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 100.26/14.88 | (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 100.26/14.88 | A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : % 100.26/14.88 | ? [v6: any] : (fun_app$a(finite$, v3) = v6 & fun_app$a(finite$, v1) = % 100.26/14.88 | v5 & fun_app$a(finite$, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | v6 % 100.26/14.88 | = 0))) % 100.26/14.88 | % 100.26/14.88 | ALPHA: (axiom22) implies: % 100.26/14.88 | (3) ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 100.26/14.88 | A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 100.26/14.88 | (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 100.26/14.88 | A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : % 100.26/14.88 | (fun_app$a(finite$, v3) = v5 & fun_app$a(finite$, v0) = v4 & ( ~ (v5 % 100.26/14.88 | = 0) | v4 = 0))) % 100.26/14.88 | % 100.26/14.88 | ALPHA: (axiom64) implies: % 100.26/14.89 | (4) ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 100.26/14.89 | A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 100.26/14.89 | (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 100.26/14.89 | A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : % 100.26/14.89 | ? [v6: any] : (fun_app$a(finite$, v3) = v4 & fun_app$a(finite$, v1) = % 100.26/14.89 | v6 & fun_app$a(finite$, v0) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0) | v4 % 100.26/14.89 | = 0))) % 100.26/14.89 | (5) ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 100.26/14.89 | A_ltln_set_a_ltln_set_fun$] : ! [v3: A_ltln_set$] : ( ~ % 100.26/14.89 | (fun_app$d(sup$, v0) = v2) | ~ (fun_app$c(v2, v1) = v3) | ~ % 100.26/14.89 | A_ltln_set$(v1) | ~ A_ltln_set$(v0) | ? [v4: any] : ? [v5: any] : % 100.26/14.89 | ? [v6: any] : (fun_app$a(finite$, v3) = v6 & fun_app$a(finite$, v1) = % 100.26/14.89 | v5 & fun_app$a(finite$, v0) = v4 & ( ~ (v6 = 0) | (v5 = 0 & v4 = % 100.26/14.89 | 0)))) % 100.26/14.89 | % 100.26/14.89 | ALPHA: (axiom69) implies: % 100.26/14.89 | (6) ? [v0: A_ltln_set_bool_fun$] : ? [v1: A_ltln_set$] : % 100.26/14.89 | (fun_app$g(less_eq$, y$) = v0 & fun_app$h(subformulas_nu$, phi$) = v1 & % 100.26/14.89 | fun_app$a(v0, v1) = 0 & A_ltln_set$(v1) & A_ltln_set_bool_fun$(v0)) % 100.26/14.89 | % 100.26/14.89 | ALPHA: (axiom70) implies: % 100.26/14.89 | (7) A_ltln$(phi$) % 100.26/14.89 | (8) ? [v0: A_ltln_set_bool_fun$] : ? [v1: A_ltln_set$] : % 100.26/14.89 | (fun_app$g(less_eq$, x$) = v0 & fun_app$h(subformulas_mu$, phi$) = v1 & % 100.26/14.89 | fun_app$a(v0, v1) = 0 & A_ltln_set$(v1) & A_ltln_set_bool_fun$(v0)) % 100.26/14.89 | % 100.26/14.89 | ALPHA: (axiom260) implies: % 100.26/14.89 | (9) ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 100.26/14.89 | A_ltln_set_bool_fun$] : ( ~ (fun_app$g(less_eq$, v0) = v2) | ~ % 100.26/14.89 | (fun_app$a(v2, v1) = 0) | ~ A_ltln_set$(v1) | ~ A_ltln_set$(v0) | % 100.26/14.89 | ? [v3: any] : ? [v4: any] : (fun_app$a(finite$, v1) = v4 & % 100.26/14.89 | fun_app$a(finite$, v0) = v3 & ( ~ (v4 = 0) | v3 = 0))) % 100.26/14.89 | % 100.26/14.89 | ALPHA: (axiom262) implies: % 100.26/14.90 | (10) ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 100.26/14.90 | A_ltln_set_bool_fun$] : ( ~ (fun_app$g(less_eq$, v1) = v2) | ~ % 100.26/14.90 | (fun_app$a(v2, v0) = 0) | ~ A_ltln_set$(v1) | ~ A_ltln_set$(v0) | % 100.26/14.90 | ? [v3: any] : ? [v4: any] : (fun_app$a(finite$, v1) = v4 & % 100.26/14.90 | fun_app$a(finite$, v0) = v3 & ( ~ (v3 = 0) | v4 = 0))) % 100.26/14.90 | % 100.26/14.90 | ALPHA: (axiom287) implies: % 100.26/14.90 | (11) ! [v0: A_ltln$] : ! [v1: A_ltln_set$] : ( ~ % 100.26/14.90 | (fun_app$h(subformulas_mu$, v0) = v1) | ~ A_ltln$(v0) | % 100.26/14.90 | fun_app$a(finite$, v1) = 0) % 100.26/14.90 | % 100.26/14.90 | ALPHA: (axiom288) implies: % 100.26/14.90 | (12) ! [v0: A_ltln$] : ! [v1: A_ltln_set$] : ( ~ % 100.26/14.90 | (fun_app$h(subformulas_nu$, v0) = v1) | ~ A_ltln$(v0) | % 100.26/14.90 | fun_app$a(finite$, v1) = 0) % 100.26/14.90 | % 100.26/14.90 | ALPHA: (conjecture2) implies: % 100.26/14.90 | (13) A_ltln_set$(x$) % 100.26/14.90 | (14) A_ltln_set$(y$) % 100.26/14.90 | (15) ? [v0: A_ltln_set_a_ltln_set_fun$] : ? [v1: A_ltln_set$] : ? [v2: % 100.26/14.90 | int] : ( ~ (v2 = 0) & fun_app$d(sup$, x$) = v0 & fun_app$c(v0, y$) = % 100.26/14.90 | v1 & fun_app$a(finite$, v1) = v2 & A_ltln_set_a_ltln_set_fun$(v0) & % 100.26/14.90 | A_ltln_set$(v1)) % 100.26/14.90 | % 100.26/14.90 | ALPHA: (function-axioms) implies: % 100.26/14.90 | (16) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 100.26/14.90 | A_ltln_set$] : ! [v3: A_ltln_set_bool_fun$] : (v1 = v0 | ~ % 100.26/14.90 | (fun_app$a(v3, v2) = v1) | ~ (fun_app$a(v3, v2) = v0)) % 100.26/14.90 | % 100.26/14.90 | DELTA: instantiating (8) with fresh symbols all_648_0, all_648_1 gives: % 100.26/14.90 | (17) fun_app$g(less_eq$, x$) = all_648_1 & fun_app$h(subformulas_mu$, phi$) % 100.26/14.90 | = all_648_0 & fun_app$a(all_648_1, all_648_0) = 0 & % 100.26/14.90 | A_ltln_set$(all_648_0) & A_ltln_set_bool_fun$(all_648_1) % 100.26/14.90 | % 100.26/14.90 | ALPHA: (17) implies: % 100.26/14.90 | (18) A_ltln_set$(all_648_0) % 100.26/14.90 | (19) fun_app$a(all_648_1, all_648_0) = 0 % 100.26/14.90 | (20) fun_app$h(subformulas_mu$, phi$) = all_648_0 % 100.26/14.90 | (21) fun_app$g(less_eq$, x$) = all_648_1 % 100.26/14.90 | % 100.26/14.90 | DELTA: instantiating (6) with fresh symbols all_662_0, all_662_1 gives: % 100.26/14.90 | (22) fun_app$g(less_eq$, y$) = all_662_1 & fun_app$h(subformulas_nu$, phi$) % 100.26/14.90 | = all_662_0 & fun_app$a(all_662_1, all_662_0) = 0 & % 100.26/14.90 | A_ltln_set$(all_662_0) & A_ltln_set_bool_fun$(all_662_1) % 100.26/14.90 | % 100.26/14.90 | ALPHA: (22) implies: % 100.26/14.90 | (23) A_ltln_set$(all_662_0) % 100.26/14.91 | (24) fun_app$a(all_662_1, all_662_0) = 0 % 100.26/14.91 | (25) fun_app$h(subformulas_nu$, phi$) = all_662_0 % 100.26/14.91 | (26) fun_app$g(less_eq$, y$) = all_662_1 % 100.26/14.91 | % 100.26/14.91 | DELTA: instantiating (15) with fresh symbols all_702_0, all_702_1, all_702_2 % 100.26/14.91 | gives: % 100.26/14.91 | (27) ~ (all_702_0 = 0) & fun_app$d(sup$, x$) = all_702_2 & % 100.26/14.91 | fun_app$c(all_702_2, y$) = all_702_1 & fun_app$a(finite$, all_702_1) = % 100.26/14.91 | all_702_0 & A_ltln_set_a_ltln_set_fun$(all_702_2) & % 100.26/14.91 | A_ltln_set$(all_702_1) % 100.26/14.91 | % 100.26/14.91 | ALPHA: (27) implies: % 100.26/14.91 | (28) ~ (all_702_0 = 0) % 100.26/14.91 | (29) fun_app$a(finite$, all_702_1) = all_702_0 % 100.26/14.91 | (30) fun_app$c(all_702_2, y$) = all_702_1 % 100.26/14.91 | (31) fun_app$d(sup$, x$) = all_702_2 % 100.26/14.91 | % 100.26/14.91 | GROUND_INST: instantiating (5) with x$, y$, all_702_2, all_702_1, simplifying % 100.26/14.91 | with (13), (14), (30), (31) gives: % 100.26/14.91 | (32) ? [v0: any] : ? [v1: any] : ? [v2: any] : (fun_app$a(finite$, % 100.26/14.91 | all_702_1) = v2 & fun_app$a(finite$, y$) = v1 & fun_app$a(finite$, % 100.26/14.91 | x$) = v0 & ( ~ (v2 = 0) | (v1 = 0 & v0 = 0))) % 100.26/14.91 | % 100.26/14.91 | GROUND_INST: instantiating (2) with x$, y$, all_702_2, all_702_1, simplifying % 100.26/14.91 | with (13), (14), (30), (31) gives: % 100.26/14.91 | (33) ? [v0: any] : ? [v1: any] : ? [v2: any] : (fun_app$a(finite$, % 100.26/14.91 | all_702_1) = v2 & fun_app$a(finite$, y$) = v1 & fun_app$a(finite$, % 100.26/14.91 | x$) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 100.26/14.91 | % 100.26/14.91 | GROUND_INST: instantiating (4) with x$, y$, all_702_2, all_702_1, simplifying % 100.26/14.91 | with (13), (14), (30), (31) gives: % 100.26/14.91 | (34) ? [v0: any] : ? [v1: any] : ? [v2: any] : (fun_app$a(finite$, % 100.26/14.91 | all_702_1) = v0 & fun_app$a(finite$, y$) = v2 & fun_app$a(finite$, % 100.26/14.91 | x$) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | v0 = 0)) % 100.26/14.91 | % 100.26/14.91 | GROUND_INST: instantiating (1) with x$, y$, all_702_2, all_702_1, simplifying % 100.26/14.91 | with (13), (14), (30), (31) gives: % 100.26/14.92 | (35) ? [v0: any] : ? [v1: any] : ? [v2: any] : (fun_app$a(finite$, % 100.26/14.92 | all_702_1) = v0 & fun_app$a(finite$, y$) = v2 & fun_app$a(finite$, % 100.26/14.92 | x$) = v1 & ( ~ (v0 = 0) | (v2 = 0 & v1 = 0))) % 100.26/14.92 | % 100.26/14.92 | GROUND_INST: instantiating (3) with x$, y$, all_702_2, all_702_1, simplifying % 100.26/14.92 | with (13), (14), (30), (31) gives: % 100.26/14.92 | (36) ? [v0: any] : ? [v1: any] : (fun_app$a(finite$, all_702_1) = v1 & % 100.26/14.92 | fun_app$a(finite$, x$) = v0 & ( ~ (v1 = 0) | v0 = 0)) % 100.26/14.92 | % 100.26/14.92 | GROUND_INST: instantiating (12) with phi$, all_662_0, simplifying with (7), % 100.26/14.92 | (25) gives: % 100.26/14.92 | (37) fun_app$a(finite$, all_662_0) = 0 % 100.26/14.92 | % 100.26/14.92 | GROUND_INST: instantiating (11) with phi$, all_648_0, simplifying with (7), % 100.26/14.92 | (20) gives: % 100.26/14.92 | (38) fun_app$a(finite$, all_648_0) = 0 % 100.26/14.92 | % 100.26/14.92 | GROUND_INST: instantiating (10) with all_648_0, x$, all_648_1, simplifying % 100.26/14.92 | with (13), (18), (19), (21) gives: % 100.26/14.92 | (39) ? [v0: any] : ? [v1: any] : (fun_app$a(finite$, all_648_0) = v0 & % 100.26/14.92 | fun_app$a(finite$, x$) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 100.26/14.92 | % 100.26/14.92 | GROUND_INST: instantiating (9) with x$, all_648_0, all_648_1, simplifying with % 100.26/14.92 | (13), (18), (19), (21) gives: % 100.26/14.92 | (40) ? [v0: any] : ? [v1: any] : (fun_app$a(finite$, all_648_0) = v1 & % 100.26/14.92 | fun_app$a(finite$, x$) = v0 & ( ~ (v1 = 0) | v0 = 0)) % 100.26/14.92 | % 100.26/14.92 | GROUND_INST: instantiating (10) with all_662_0, y$, all_662_1, simplifying % 100.26/14.92 | with (14), (23), (24), (26) gives: % 100.26/14.92 | (41) ? [v0: any] : ? [v1: any] : (fun_app$a(finite$, all_662_0) = v0 & % 100.26/14.92 | fun_app$a(finite$, y$) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 100.26/14.92 | % 100.26/14.92 | GROUND_INST: instantiating (9) with y$, all_662_0, all_662_1, simplifying with % 100.26/14.92 | (14), (23), (24), (26) gives: % 100.26/14.93 | (42) ? [v0: any] : ? [v1: any] : (fun_app$a(finite$, all_662_0) = v1 & % 100.26/14.93 | fun_app$a(finite$, y$) = v0 & ( ~ (v1 = 0) | v0 = 0)) % 100.26/14.93 | % 100.26/14.93 | DELTA: instantiating (42) with fresh symbols all_745_0, all_745_1 gives: % 100.26/14.93 | (43) fun_app$a(finite$, all_662_0) = all_745_0 & fun_app$a(finite$, y$) = % 100.26/14.93 | all_745_1 & ( ~ (all_745_0 = 0) | all_745_1 = 0) % 100.26/14.93 | % 100.26/14.93 | ALPHA: (43) implies: % 100.26/14.93 | (44) fun_app$a(finite$, y$) = all_745_1 % 100.26/14.93 | (45) fun_app$a(finite$, all_662_0) = all_745_0 % 100.26/14.93 | (46) ~ (all_745_0 = 0) | all_745_1 = 0 % 100.26/14.93 | % 100.26/14.93 | DELTA: instantiating (41) with fresh symbols all_747_0, all_747_1 gives: % 100.26/14.93 | (47) fun_app$a(finite$, all_662_0) = all_747_1 & fun_app$a(finite$, y$) = % 100.26/14.93 | all_747_0 & ( ~ (all_747_1 = 0) | all_747_0 = 0) % 100.26/14.93 | % 100.26/14.93 | ALPHA: (47) implies: % 100.26/14.93 | (48) fun_app$a(finite$, y$) = all_747_0 % 100.26/14.93 | (49) fun_app$a(finite$, all_662_0) = all_747_1 % 100.26/14.93 | % 100.26/14.93 | DELTA: instantiating (39) with fresh symbols all_751_0, all_751_1 gives: % 100.26/14.93 | (50) fun_app$a(finite$, all_648_0) = all_751_1 & fun_app$a(finite$, x$) = % 100.26/14.93 | all_751_0 & ( ~ (all_751_1 = 0) | all_751_0 = 0) % 100.26/14.93 | % 100.26/14.93 | ALPHA: (50) implies: % 100.26/14.93 | (51) fun_app$a(finite$, x$) = all_751_0 % 100.26/14.93 | (52) fun_app$a(finite$, all_648_0) = all_751_1 % 100.26/14.93 | (53) ~ (all_751_1 = 0) | all_751_0 = 0 % 100.26/14.93 | % 100.26/14.93 | DELTA: instantiating (40) with fresh symbols all_753_0, all_753_1 gives: % 100.26/14.93 | (54) fun_app$a(finite$, all_648_0) = all_753_0 & fun_app$a(finite$, x$) = % 100.26/14.93 | all_753_1 & ( ~ (all_753_0 = 0) | all_753_1 = 0) % 100.26/14.93 | % 100.26/14.93 | ALPHA: (54) implies: % 100.26/14.93 | (55) fun_app$a(finite$, x$) = all_753_1 % 100.26/14.93 | (56) fun_app$a(finite$, all_648_0) = all_753_0 % 100.26/14.93 | % 100.26/14.93 | DELTA: instantiating (36) with fresh symbols all_755_0, all_755_1 gives: % 100.26/14.93 | (57) fun_app$a(finite$, all_702_1) = all_755_0 & fun_app$a(finite$, x$) = % 100.26/14.93 | all_755_1 & ( ~ (all_755_0 = 0) | all_755_1 = 0) % 100.26/14.93 | % 100.26/14.93 | ALPHA: (57) implies: % 100.26/14.93 | (58) fun_app$a(finite$, x$) = all_755_1 % 100.26/14.93 | (59) fun_app$a(finite$, all_702_1) = all_755_0 % 100.26/14.93 | % 100.26/14.93 | DELTA: instantiating (34) with fresh symbols all_757_0, all_757_1, all_757_2 % 100.26/14.93 | gives: % 100.26/14.93 | (60) fun_app$a(finite$, all_702_1) = all_757_2 & fun_app$a(finite$, y$) = % 100.26/14.93 | all_757_0 & fun_app$a(finite$, x$) = all_757_1 & ( ~ (all_757_0 = 0) | % 100.26/14.93 | ~ (all_757_1 = 0) | all_757_2 = 0) % 100.26/14.93 | % 100.26/14.93 | ALPHA: (60) implies: % 100.26/14.94 | (61) fun_app$a(finite$, x$) = all_757_1 % 100.26/14.94 | (62) fun_app$a(finite$, y$) = all_757_0 % 100.26/14.94 | (63) fun_app$a(finite$, all_702_1) = all_757_2 % 100.26/14.94 | % 100.26/14.94 | DELTA: instantiating (33) with fresh symbols all_759_0, all_759_1, all_759_2 % 100.26/14.94 | gives: % 100.26/14.94 | (64) fun_app$a(finite$, all_702_1) = all_759_0 & fun_app$a(finite$, y$) = % 100.26/14.94 | all_759_1 & fun_app$a(finite$, x$) = all_759_2 & ( ~ (all_759_1 = 0) | % 100.26/14.94 | ~ (all_759_2 = 0) | all_759_0 = 0) % 100.26/14.94 | % 100.26/14.94 | ALPHA: (64) implies: % 100.26/14.94 | (65) fun_app$a(finite$, x$) = all_759_2 % 100.26/14.94 | (66) fun_app$a(finite$, y$) = all_759_1 % 100.26/14.94 | (67) fun_app$a(finite$, all_702_1) = all_759_0 % 100.26/14.94 | (68) ~ (all_759_1 = 0) | ~ (all_759_2 = 0) | all_759_0 = 0 % 100.26/14.94 | % 100.26/14.94 | DELTA: instantiating (35) with fresh symbols all_761_0, all_761_1, all_761_2 % 100.26/14.94 | gives: % 100.26/14.94 | (69) fun_app$a(finite$, all_702_1) = all_761_2 & fun_app$a(finite$, y$) = % 100.26/14.94 | all_761_0 & fun_app$a(finite$, x$) = all_761_1 & ( ~ (all_761_2 = 0) | % 100.26/14.94 | (all_761_0 = 0 & all_761_1 = 0)) % 100.26/14.94 | % 100.26/14.94 | ALPHA: (69) implies: % 100.26/14.94 | (70) fun_app$a(finite$, x$) = all_761_1 % 100.26/14.94 | (71) fun_app$a(finite$, y$) = all_761_0 % 100.26/14.94 | (72) fun_app$a(finite$, all_702_1) = all_761_2 % 100.26/14.94 | % 100.26/14.94 | DELTA: instantiating (32) with fresh symbols all_763_0, all_763_1, all_763_2 % 100.26/14.94 | gives: % 100.26/14.94 | (73) fun_app$a(finite$, all_702_1) = all_763_0 & fun_app$a(finite$, y$) = % 100.26/14.94 | all_763_1 & fun_app$a(finite$, x$) = all_763_2 & ( ~ (all_763_0 = 0) | % 100.26/14.94 | (all_763_1 = 0 & all_763_2 = 0)) % 100.26/14.94 | % 100.26/14.94 | ALPHA: (73) implies: % 100.26/14.94 | (74) fun_app$a(finite$, x$) = all_763_2 % 100.26/14.94 | (75) fun_app$a(finite$, y$) = all_763_1 % 100.26/14.95 | (76) fun_app$a(finite$, all_702_1) = all_763_0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_755_1, all_757_1, x$, finite$, % 100.26/14.95 | simplifying with (58), (61) gives: % 100.26/14.95 | (77) all_757_1 = all_755_1 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_755_1, all_759_2, x$, finite$, % 100.26/14.95 | simplifying with (58), (65) gives: % 100.26/14.95 | (78) all_759_2 = all_755_1 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_753_1, all_759_2, x$, finite$, % 100.26/14.95 | simplifying with (55), (65) gives: % 100.26/14.95 | (79) all_759_2 = all_753_1 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_761_1, all_763_2, x$, finite$, % 100.26/14.95 | simplifying with (70), (74) gives: % 100.26/14.95 | (80) all_763_2 = all_761_1 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_757_1, all_763_2, x$, finite$, % 100.26/14.95 | simplifying with (61), (74) gives: % 100.26/14.95 | (81) all_763_2 = all_757_1 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_751_0, all_763_2, x$, finite$, % 100.26/14.95 | simplifying with (51), (74) gives: % 100.26/14.95 | (82) all_763_2 = all_751_0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_757_0, all_759_1, y$, finite$, % 100.26/14.95 | simplifying with (62), (66) gives: % 100.26/14.95 | (83) all_759_1 = all_757_0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_747_0, all_759_1, y$, finite$, % 100.26/14.95 | simplifying with (48), (66) gives: % 100.26/14.95 | (84) all_759_1 = all_747_0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_761_0, all_763_1, y$, finite$, % 100.26/14.95 | simplifying with (71), (75) gives: % 100.26/14.95 | (85) all_763_1 = all_761_0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_757_0, all_763_1, y$, finite$, % 100.26/14.95 | simplifying with (62), (75) gives: % 100.26/14.95 | (86) all_763_1 = all_757_0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_745_1, all_763_1, y$, finite$, % 100.26/14.95 | simplifying with (44), (75) gives: % 100.26/14.95 | (87) all_763_1 = all_745_1 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_751_1, all_753_0, all_648_0, finite$, % 100.26/14.95 | simplifying with (52), (56) gives: % 100.26/14.95 | (88) all_753_0 = all_751_1 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with 0, all_753_0, all_648_0, finite$, % 100.26/14.95 | simplifying with (38), (56) gives: % 100.26/14.95 | (89) all_753_0 = 0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_745_0, all_747_1, all_662_0, finite$, % 100.26/14.95 | simplifying with (45), (49) gives: % 100.26/14.95 | (90) all_747_1 = all_745_0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with 0, all_747_1, all_662_0, finite$, % 100.26/14.95 | simplifying with (37), (49) gives: % 100.26/14.95 | (91) all_747_1 = 0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_702_0, all_757_2, all_702_1, finite$, % 100.26/14.95 | simplifying with (29), (63) gives: % 100.26/14.95 | (92) all_757_2 = all_702_0 % 100.26/14.95 | % 100.26/14.95 | GROUND_INST: instantiating (16) with all_757_2, all_759_0, all_702_1, finite$, % 100.26/14.95 | simplifying with (63), (67) gives: % 100.26/14.95 | (93) all_759_0 = all_757_2 % 100.26/14.95 | % 100.26/14.96 | GROUND_INST: instantiating (16) with all_759_0, all_761_2, all_702_1, finite$, % 100.26/14.96 | simplifying with (67), (72) gives: % 100.26/14.96 | (94) all_761_2 = all_759_0 % 100.26/14.96 | % 100.26/14.96 | GROUND_INST: instantiating (16) with all_761_2, all_763_0, all_702_1, finite$, % 100.26/14.96 | simplifying with (72), (76) gives: % 100.26/14.96 | (95) all_763_0 = all_761_2 % 100.26/14.96 | % 100.26/14.96 | GROUND_INST: instantiating (16) with all_755_0, all_763_0, all_702_1, finite$, % 100.26/14.96 | simplifying with (59), (76) gives: % 100.26/14.96 | (96) all_763_0 = all_755_0 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (95), (96) imply: % 100.26/14.96 | (97) all_761_2 = all_755_0 % 100.26/14.96 | % 100.26/14.96 | SIMP: (97) implies: % 100.26/14.96 | (98) all_761_2 = all_755_0 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (85), (87) imply: % 100.26/14.96 | (99) all_761_0 = all_745_1 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (85), (86) imply: % 100.26/14.96 | (100) all_761_0 = all_757_0 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (80), (81) imply: % 100.26/14.96 | (101) all_761_1 = all_757_1 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (80), (82) imply: % 100.26/14.96 | (102) all_761_1 = all_751_0 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (99), (100) imply: % 100.26/14.96 | (103) all_757_0 = all_745_1 % 100.26/14.96 | % 100.26/14.96 | SIMP: (103) implies: % 100.26/14.96 | (104) all_757_0 = all_745_1 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (101), (102) imply: % 100.26/14.96 | (105) all_757_1 = all_751_0 % 100.26/14.96 | % 100.26/14.96 | SIMP: (105) implies: % 100.26/14.96 | (106) all_757_1 = all_751_0 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (94), (98) imply: % 100.26/14.96 | (107) all_759_0 = all_755_0 % 100.26/14.96 | % 100.26/14.96 | SIMP: (107) implies: % 100.26/14.96 | (108) all_759_0 = all_755_0 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (93), (108) imply: % 100.26/14.96 | (109) all_757_2 = all_755_0 % 100.26/14.96 | % 100.26/14.96 | SIMP: (109) implies: % 100.26/14.96 | (110) all_757_2 = all_755_0 % 100.26/14.96 | % 100.26/14.96 | COMBINE_EQS: (83), (84) imply: % 100.26/14.96 | (111) all_757_0 = all_747_0 % 100.26/14.96 | % 100.26/14.97 | SIMP: (111) implies: % 100.26/14.97 | (112) all_757_0 = all_747_0 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (78), (79) imply: % 100.26/14.97 | (113) all_755_1 = all_753_1 % 100.26/14.97 | % 100.26/14.97 | SIMP: (113) implies: % 100.26/14.97 | (114) all_755_1 = all_753_1 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (104), (112) imply: % 100.26/14.97 | (115) all_747_0 = all_745_1 % 100.26/14.97 | % 100.26/14.97 | SIMP: (115) implies: % 100.26/14.97 | (116) all_747_0 = all_745_1 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (77), (106) imply: % 100.26/14.97 | (117) all_755_1 = all_751_0 % 100.26/14.97 | % 100.26/14.97 | SIMP: (117) implies: % 100.26/14.97 | (118) all_755_1 = all_751_0 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (92), (110) imply: % 100.26/14.97 | (119) all_755_0 = all_702_0 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (114), (118) imply: % 100.26/14.97 | (120) all_753_1 = all_751_0 % 100.26/14.97 | % 100.26/14.97 | SIMP: (120) implies: % 100.26/14.97 | (121) all_753_1 = all_751_0 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (88), (89) imply: % 100.26/14.97 | (122) all_751_1 = 0 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (90), (91) imply: % 100.26/14.97 | (123) all_745_0 = 0 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (79), (121) imply: % 100.26/14.97 | (124) all_759_2 = all_751_0 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (84), (116) imply: % 100.26/14.97 | (125) all_759_1 = all_745_1 % 100.26/14.97 | % 100.26/14.97 | COMBINE_EQS: (108), (119) imply: % 100.26/14.97 | (126) all_759_0 = all_702_0 % 100.26/14.97 | % 100.26/14.97 | BETA: splitting (46) gives: % 100.26/14.97 | % 100.26/14.97 | Case 1: % 100.26/14.97 | | % 100.26/14.97 | | (127) ~ (all_745_0 = 0) % 100.26/14.97 | | % 100.26/14.97 | | REDUCE: (123), (127) imply: % 100.26/14.97 | | (128) $false % 100.26/14.97 | | % 100.26/14.97 | | CLOSE: (128) is inconsistent. % 100.26/14.97 | | % 100.26/14.97 | Case 2: % 100.26/14.97 | | % 100.26/14.97 | | (129) all_745_1 = 0 % 100.26/14.97 | | % 100.26/14.97 | | COMBINE_EQS: (125), (129) imply: % 100.26/14.97 | | (130) all_759_1 = 0 % 100.26/14.97 | | % 100.26/14.97 | | BETA: splitting (53) gives: % 100.26/14.97 | | % 100.26/14.97 | | Case 1: % 100.26/14.97 | | | % 100.26/14.97 | | | (131) ~ (all_751_1 = 0) % 100.26/14.97 | | | % 100.26/14.97 | | | REDUCE: (122), (131) imply: % 100.26/14.97 | | | (132) $false % 100.26/14.97 | | | % 100.26/14.97 | | | CLOSE: (132) is inconsistent. % 100.26/14.97 | | | % 100.26/14.97 | | Case 2: % 100.26/14.97 | | | % 100.26/14.97 | | | (133) all_751_0 = 0 % 100.26/14.97 | | | % 100.26/14.97 | | | COMBINE_EQS: (124), (133) imply: % 100.26/14.97 | | | (134) all_759_2 = 0 % 100.26/14.97 | | | % 100.26/14.97 | | | BETA: splitting (68) gives: % 100.26/14.97 | | | % 100.26/14.97 | | | Case 1: % 100.26/14.97 | | | | % 100.26/14.97 | | | | (135) ~ (all_759_1 = 0) % 100.26/14.97 | | | | % 100.26/14.97 | | | | REDUCE: (130), (135) imply: % 100.26/14.97 | | | | (136) $false % 100.26/14.97 | | | | % 100.26/14.97 | | | | CLOSE: (136) is inconsistent. % 100.26/14.97 | | | | % 100.26/14.97 | | | Case 2: % 100.26/14.97 | | | | % 100.26/14.97 | | | | (137) ~ (all_759_2 = 0) | all_759_0 = 0 % 100.26/14.97 | | | | % 100.26/14.97 | | | | BETA: splitting (137) gives: % 100.26/14.97 | | | | % 100.26/14.97 | | | | Case 1: % 100.26/14.97 | | | | | % 100.26/14.97 | | | | | (138) ~ (all_759_2 = 0) % 100.26/14.97 | | | | | % 100.26/14.97 | | | | | REDUCE: (134), (138) imply: % 100.26/14.97 | | | | | (139) $false % 100.26/14.97 | | | | | % 100.26/14.97 | | | | | CLOSE: (139) is inconsistent. % 100.26/14.97 | | | | | % 100.26/14.97 | | | | Case 2: % 100.26/14.97 | | | | | % 100.26/14.97 | | | | | (140) all_759_0 = 0 % 100.26/14.97 | | | | | % 100.26/14.97 | | | | | COMBINE_EQS: (126), (140) imply: % 100.26/14.98 | | | | | (141) all_702_0 = 0 % 100.26/14.98 | | | | | % 100.26/14.98 | | | | | SIMP: (141) implies: % 100.26/14.98 | | | | | (142) all_702_0 = 0 % 100.26/14.98 | | | | | % 100.26/14.98 | | | | | REDUCE: (28), (142) imply: % 100.26/14.98 | | | | | (143) $false % 100.26/14.98 | | | | | % 100.26/14.98 | | | | | CLOSE: (143) is inconsistent. % 100.26/14.98 | | | | | % 100.26/14.98 | | | | End of split % 100.26/14.98 | | | | % 100.26/14.98 | | | End of split % 100.26/14.98 | | | % 100.26/14.98 | | End of split % 100.26/14.98 | | % 100.26/14.98 | End of split % 100.26/14.98 | % 100.26/14.98 End of proof % 100.26/14.98 % SZS output end Proof for theBenchmark % 100.26/14.98 % 100.26/14.98 14355ms %------------------------------------------------------------------------------