%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.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 04:11:52 EDT 2023 % Result : Theorem 55.50s 8.23s % Output : Proof 87.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : ITP001_1 : TPTP v8.1.2. Released v8.1.0. % 0.08/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.31 % Computer : n017.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Sun Aug 27 13:11:56 EDT 2023 % 0.10/0.31 % CPUTime : % 0.15/0.58 ________ _____ % 0.15/0.58 ___ __ \_________(_)________________________________ % 0.15/0.58 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.15/0.58 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.15/0.58 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.15/0.58 % 0.15/0.58 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.15/0.58 (2023-06-19) % 0.15/0.58 % 0.15/0.58 (c) Philipp Rümmer, 2009-2023 % 0.15/0.58 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.15/0.58 Amanda Stjerna. % 0.15/0.58 Free software under BSD-3-Clause. % 0.15/0.58 % 0.15/0.58 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.15/0.58 % 0.15/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.15/0.60 Running up to 7 provers in parallel. % 0.15/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.15/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.15/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.15/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.15/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.15/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.15/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 19.61/3.50 Prover 1: Preprocessing ... % 20.22/3.52 Prover 2: Preprocessing ... % 20.22/3.52 Prover 0: Preprocessing ... % 20.22/3.54 Prover 3: Preprocessing ... % 20.22/3.55 Prover 5: Preprocessing ... % 20.81/3.63 Prover 4: Preprocessing ... % 20.81/3.65 Prover 6: Preprocessing ... % 46.71/7.09 Prover 1: Warning: ignoring some quantifiers % 47.92/7.27 Prover 3: Warning: ignoring some quantifiers % 47.92/7.28 Prover 6: Proving ... % 48.92/7.32 Prover 5: Proving ... % 49.35/7.35 Prover 3: Constructing countermodel ... % 49.79/7.44 Prover 1: Constructing countermodel ... % 55.07/8.16 Prover 4: Warning: ignoring some quantifiers % 55.50/8.22 Prover 5: proved (7606ms) % 55.50/8.22 % 55.50/8.23 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 55.50/8.23 % 55.50/8.23 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 56.15/8.27 Prover 3: stopped % 56.15/8.28 Prover 6: stopped % 56.39/8.30 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 56.39/8.30 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 56.88/8.39 Prover 0: Proving ... % 56.88/8.39 Prover 0: stopped % 56.88/8.39 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 58.40/8.60 Prover 4: Constructing countermodel ... % 66.03/9.64 Prover 8: Preprocessing ... % 67.28/9.74 Prover 10: Preprocessing ... % 67.28/9.78 Prover 7: Preprocessing ... % 67.28/9.82 Prover 11: Preprocessing ... % 68.55/9.94 Prover 2: Proving ... % 68.55/9.94 Prover 2: stopped % 68.55/9.95 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 75.19/10.79 Prover 1: Found proof (size 65) % 75.19/10.79 Prover 1: proved (10178ms) % 75.19/10.79 Prover 4: stopped % 76.27/10.94 Prover 13: Preprocessing ... % 79.33/11.37 Prover 10: Warning: ignoring some quantifiers % 79.98/11.45 Prover 13: stopped % 80.56/11.48 Prover 7: Warning: ignoring some quantifiers % 80.56/11.55 Prover 8: Warning: ignoring some quantifiers % 80.56/11.55 Prover 10: Constructing countermodel ... % 81.50/11.66 Prover 10: stopped % 81.50/11.70 Prover 7: Constructing countermodel ... % 82.04/11.75 Prover 8: Constructing countermodel ... % 82.49/11.78 Prover 7: stopped % 82.49/11.81 Prover 8: stopped % 84.78/12.37 Prover 11: Warning: ignoring some quantifiers % 85.53/12.62 Prover 11: Constructing countermodel ... % 86.45/12.74 Prover 11: stopped % 86.45/12.74 % 86.45/12.74 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 86.45/12.74 % 86.45/12.76 % SZS output start Proof for theBenchmark % 86.79/12.80 Assumptions after simplification: % 86.79/12.80 --------------------------------- % 86.79/12.80 % 86.79/12.80 (axiom0) % 86.79/12.83 Nat_bool_fun$(uu$) & Nat_a_set_fun$(w$) & A_ltln$(phi$) & ? [v0: A_ltln_set$] % 86.79/12.83 : (f_G$(phi$, w$) = v0 & A_ltln_set$(v0) & ! [v1: Nat$] : ! [v2: % 86.79/12.83 Nat_a_set_fun$] : ( ~ (suffix$(v1, w$) = v2) | ~ Nat$(v1) | ? [v3: % 86.79/12.83 A_ltln_set$] : ? [v4: any] : (fun_app$(uu$, v1) = v4 & g$(phi$, v2) = % 86.79/12.83 v3 & A_ltln_set$(v3) & ( ~ (v3 = v0) | v4 = 0))) & ! [v1: Nat$] : ! % 86.79/12.83 [v2: Nat_a_set_fun$] : ( ~ (suffix$(v1, w$) = v2) | ~ Nat$(v1) | ? [v3: % 86.79/12.83 any] : ? [v4: A_ltln_set$] : (fun_app$(uu$, v1) = v3 & g$(phi$, v2) = % 86.79/12.83 v4 & A_ltln_set$(v4) & ( ~ (v3 = 0) | v4 = v0)))) % 86.79/12.83 % 86.79/12.83 (axiom116) % 86.79/12.84 ! [v0: Nat_a_set_fun$] : ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! [v3: % 86.79/12.84 A_ltln_bool_fun$] : ! [v4: A_ltln$] : ! [v5: int] : (v5 = 0 | ~ % 86.79/12.84 (semantics_ltln$(v0) = v3) | ~ (release_ltln$(v1, v2) = v4) | ~ % 86.79/12.84 (fun_app$a(v3, v4) = v5) | ~ Nat_a_set_fun$(v0) | ~ A_ltln$(v2) | ~ % 86.79/12.84 A_ltln$(v1) | ? [v6: Nat$] : ? [v7: Nat_a_set_fun$] : ? [v8: % 86.79/12.84 A_ltln_bool_fun$] : ? [v9: int] : ? [v10: int] : ( ~ (v9 = 0) & % 86.79/12.84 of_nat$(v6) = v10 & semantics_ltln$(v7) = v8 & fun_app$a(v8, v2) = v9 & % 86.79/12.84 suffix$(v6, v0) = v7 & Nat_a_set_fun$(v7) & A_ltln_bool_fun$(v8) & % 86.79/12.84 Nat$(v6) & ! [v11: Nat$] : ! [v12: Nat_a_set_fun$] : ! [v13: % 86.79/12.84 A_ltln_bool_fun$] : ( ~ (semantics_ltln$(v12) = v13) | ~ % 86.79/12.84 (fun_app$a(v13, v1) = 0) | ~ (suffix$(v11, v0) = v12) | ~ Nat$(v11) | % 86.79/12.84 ? [v14: int] : ($lesseq(v10, v14) & of_nat$(v11) = v14)))) & ! [v0: % 86.79/12.84 Nat_a_set_fun$] : ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! [v3: % 86.79/12.84 A_ltln_bool_fun$] : ! [v4: A_ltln$] : ( ~ (semantics_ltln$(v0) = v3) | ~ % 86.79/12.84 (release_ltln$(v1, v2) = v4) | ~ (fun_app$a(v3, v4) = 0) | ~ % 86.79/12.84 Nat_a_set_fun$(v0) | ~ A_ltln$(v2) | ~ A_ltln$(v1) | ! [v5: Nat$] : ! % 86.79/12.84 [v6: Nat_a_set_fun$] : ! [v7: A_ltln_bool_fun$] : ! [v8: int] : (v8 = 0 | % 86.79/12.84 ~ (semantics_ltln$(v6) = v7) | ~ (fun_app$a(v7, v2) = v8) | ~ % 86.79/12.84 (suffix$(v5, v0) = v6) | ~ Nat$(v5) | ? [v9: int] : (of_nat$(v5) = v9 & % 86.79/12.84 ? [v10: Nat$] : ? [v11: int] : ? [v12: Nat_a_set_fun$] : ? [v13: % 86.79/12.84 A_ltln_bool_fun$] : ($lesseq(1, $difference(v9, v11)) & of_nat$(v10) = % 86.79/12.84 v11 & semantics_ltln$(v12) = v13 & fun_app$a(v13, v1) = 0 & % 86.79/12.85 suffix$(v10, v0) = v12 & Nat_a_set_fun$(v12) & A_ltln_bool_fun$(v13) & % 86.79/12.85 Nat$(v10))))) % 86.79/12.85 % 86.79/12.85 (axiom32) % 86.79/12.85 Nat_a_set_fun$(w$) & A_ltln$(phi$) & A_ltln$(psi_2$) & A_ltln$(psi_1$) & ? % 86.79/12.85 [v0: A_ltln$] : ? [v1: A_ltln_set$] : (weakUntil_ltln$(psi_1$, psi_2$) = v0 & % 86.79/12.85 member$(v0, v1) = 0 & f_G$(phi$, w$) = v1 & A_ltln$(v0) & A_ltln_set$(v1)) % 86.79/12.85 % 86.79/12.85 (axiom33) % 86.79/12.85 Nat_a_set_fun$(w$) & A_ltln$(phi$) & ? [v0: A_ltln_set$] : (f_G$(phi$, w$) = % 86.79/12.85 v0 & A_ltln_set$(v0) & ? [v1: Nat$] : ? [v2: Nat_a_set_fun$] : % 86.79/12.85 (suffix$(v1, w$) = v2 & g$(phi$, v2) = v0 & Nat_a_set_fun$(v2) & Nat$(v1))) % 86.79/12.85 % 86.79/12.85 (axiom34) % 86.79/12.85 Nat_bool_fun$(uu$) & Nat_a_set_fun$(w$) & A_ltln$(phi$) & ? [v0: A_ltln_set$] % 86.79/12.85 : ? [v1: Nat$] : ? [v2: Nat_a_set_fun$] : (eps$(uu$) = v1 & f_G$(phi$, w$) = % 86.79/12.85 v0 & suffix$(v1, w$) = v2 & g$(phi$, v2) = v0 & Nat_a_set_fun$(v2) & % 86.79/12.85 A_ltln_set$(v0) & Nat$(v1)) % 86.79/12.85 % 86.79/12.85 (axiom39) % 86.79/12.86 A_ltln$(false_ltln$) & ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! [v2: % 86.79/12.86 Nat_a_set_fun$] : ! [v3: A_ltln_set$] : ( ~ (member$(v0, v3) = 0) | ~ % 86.79/12.86 (g$(v1, v2) = v3) | ~ Nat_a_set_fun$(v2) | ~ A_ltln$(v1) | ~ A_ltln$(v0) % 86.79/12.86 | ? [v4: A_ltln_bool_fun$] : ? [v5: A_ltln$] : (semantics_ltln$(v2) = v4 & % 86.79/12.86 release_ltln$(false_ltln$, v0) = v5 & fun_app$a(v4, v5) = 0 & A_ltln$(v5) % 86.79/12.86 & A_ltln_bool_fun$(v4))) % 86.79/12.86 % 86.79/12.86 (axiom442) % 86.79/12.86 A_ltln$(true_ltln$) & A_ltln$(false_ltln$) & ! [v0: A_ltln$] : ! [v1: % 86.79/12.86 A_ltln$] : ! [v2: Nat_a_set_fun$] : ! [v3: A_ltln_set$] : ( ~ (member$(v0, % 86.79/12.86 v3) = 0) | ~ (f_G$(v1, v2) = v3) | ~ Nat_a_set_fun$(v2) | ~ % 86.79/12.86 A_ltln$(v1) | ~ A_ltln$(v0) | ? [v4: A_ltln_bool_fun$] : ? [v5: A_ltln$] % 86.79/12.86 : ? [v6: A_ltln$] : (semantics_ltln$(v2) = v4 & release_ltln$(false_ltln$, % 86.79/12.86 v0) = v5 & fun_app$a(v4, v6) = 0 & until_ltln$(true_ltln$, v5) = v6 & % 86.79/12.86 A_ltln$(v6) & A_ltln$(v5) & A_ltln_bool_fun$(v4))) % 86.79/12.86 % 86.79/12.86 (conjecture30) % 86.79/12.86 Nat_bool_fun$(uu$) & Nat_a_set_fun$(w$) & A_ltln$(psi_2$) & % 86.79/12.86 A_ltln$(false_ltln$) & A_ltln$(psi_1$) & ? [v0: Nat$] : ? [v1: % 86.79/12.86 Nat_a_set_fun$] : ? [v2: A_ltln_bool_fun$] : ? [v3: A_ltln$] : ? [v4: % 86.79/12.86 A_ltln$] : ? [v5: int] : ( ~ (v5 = 0) & eps$(uu$) = v0 & % 86.79/12.86 weakUntil_ltln$(psi_1$, psi_2$) = v3 & semantics_ltln$(v1) = v2 & % 86.79/12.86 release_ltln$(false_ltln$, v3) = v4 & fun_app$a(v2, v4) = v5 & suffix$(v0, % 86.79/12.86 w$) = v1 & Nat_a_set_fun$(v1) & A_ltln$(v4) & A_ltln$(v3) & % 86.79/12.86 A_ltln_bool_fun$(v2) & Nat$(v0)) % 86.79/12.86 % 86.79/12.86 (function-axioms) % 87.18/12.90 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 87.18/12.90 Int_int_bool_fun_fun$] : ! [v3: Int_int_bool_fun_fun$] : ! [v4: % 87.18/12.90 Int_int_int_fun_fun$] : (v1 = v0 | ~ (semilattice_order_set$(v4, v3, v2) = % 87.18/12.90 v1) | ~ (semilattice_order_set$(v4, v3, v2) = v0)) & ! [v0: A_ltln_set$] % 87.18/12.90 : ! [v1: A_ltln_set$] : ! [v2: Nat_a_set_fun$] : ! [v3: A_ltln$] : (v1 = v0 % 87.18/12.90 | ~ (f$(v3, v2) = v1) | ~ (f$(v3, v2) = v0)) & ! [v0: A_ltln$] : ! [v1: % 87.18/12.90 A_ltln$] : ! [v2: A_ltln_set$] : ! [v3: A_ltln$] : (v1 = v0 | ~ % 87.18/12.90 (gF_advice$(v3, v2) = v1) | ~ (gF_advice$(v3, v2) = v0)) & ! [v0: % 87.18/12.90 A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: Nat_a_set_fun$] : ! [v3: % 87.18/12.90 A_ltln$] : (v1 = v0 | ~ (g_F$(v3, v2) = v1) | ~ (g_F$(v3, v2) = v0)) & ! % 87.18/12.90 [v0: Int_int_fun$] : ! [v1: Int_int_fun$] : ! [v2: int] : ! [v3: % 87.18/12.90 Int_int_int_fun_fun$] : (v1 = v0 | ~ (fun_app$o(v3, v2) = v1) | ~ % 87.18/12.90 (fun_app$o(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 87.18/12.90 MultipleValueBool] : ! [v2: Nat_a_set_fun_set$] : ! [v3: % 87.18/12.90 Nat_a_set_fun_set$] : (v1 = v0 | ~ (less_eq$d(v3, v2) = v1) | ~ % 87.18/12.90 (less_eq$d(v3, v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 87.18/12.90 Nat_set$] : ! [v3: Nat_set$] : (v1 = v0 | ~ (inf$b(v3, v2) = v1) | ~ % 87.18/12.90 (inf$b(v3, v2) = v0)) & ! [v0: Nat_a_set_fun_set$] : ! [v1: % 87.18/12.90 Nat_a_set_fun_set$] : ! [v2: Nat_a_set_fun_set$] : ! [v3: % 87.18/12.90 Nat_a_set_fun_set$] : (v1 = v0 | ~ (inf$a(v3, v2) = v1) | ~ (inf$a(v3, v2) % 87.18/12.90 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 87.18/12.90 Nat_set$] : ! [v3: Nat_set$] : (v1 = v0 | ~ (less_eq$c(v3, v2) = v1) | ~ % 87.18/12.90 (less_eq$c(v3, v2) = v0)) & ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! [v2: % 87.18/12.90 A_ltln_set$] : ! [v3: A_ltln$] : (v1 = v0 | ~ (fG_advice$(v3, v2) = v1) | % 87.18/12.90 ~ (fG_advice$(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 87.18/12.90 MultipleValueBool] : ! [v2: A_ltln_bool_fun$] : ! [v3: A_ltln_bool_fun$] : % 87.18/12.90 (v1 = v0 | ~ (less$a(v3, v2) = v1) | ~ (less$a(v3, v2) = v0)) & ! [v0: % 87.18/12.90 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_ltln_set$] : ! % 87.18/12.90 [v3: A_ltln_set$] : (v1 = v0 | ~ (less$(v3, v2) = v1) | ~ (less$(v3, v2) = % 87.18/12.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.90 A_ltln_bool_fun$] : (v1 = v0 | ~ (def_7(v3, v2) = v1) | ~ (def_7(v3, v2) = % 87.18/12.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.90 A_ltln_bool_fun$] : (v1 = v0 | ~ (def_8(v3, v2) = v1) | ~ (def_8(v3, v2) = % 87.18/12.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.90 A_ltln_bool_fun$] : (v1 = v0 | ~ (def_5(v3, v2) = v1) | ~ (def_5(v3, v2) = % 87.18/12.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.90 A_ltln_bool_fun$] : (v1 = v0 | ~ (def_6(v3, v2) = v1) | ~ (def_6(v3, v2) = % 87.18/12.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.90 A_ltln_bool_fun$] : (v1 = v0 | ~ (def_3(v3, v2) = v1) | ~ (def_3(v3, v2) = % 87.18/12.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.90 A_ltln_bool_fun$] : (v1 = v0 | ~ (def_4(v3, v2) = v1) | ~ (def_4(v3, v2) = % 87.18/12.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.90 A_ltln_bool_fun$] : (v1 = v0 | ~ (def_1(v3, v2) = v1) | ~ (def_1(v3, v2) = % 87.18/12.90 v0)) & ! [v0: tlbool] : ! [v1: tlbool] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.90 A_ltln_bool_fun$] : (v1 = v0 | ~ (def_2(v3, v2) = v1) | ~ (def_2(v3, v2) = % 87.18/12.90 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 87.18/12.90 tlbool] : ! [v3: tlbool] : (v1 = v0 | ~ (less_eq$b(v3, v2) = v1) | ~ % 87.18/12.90 (less_eq$b(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ! % 87.18/12.90 [v3: Int_int_fun$] : (v1 = v0 | ~ (fun_app$n(v3, v2) = v1) | ~ % 87.18/12.90 (fun_app$n(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 87.18/12.90 A_ltln_bool_fun$] : ! [v3: A_ltln_bool_fun_int_fun$] : (v1 = v0 | ~ % 87.18/12.90 (fun_app$m(v3, v2) = v1) | ~ (fun_app$m(v3, v2) = v0)) & ! [v0: % 87.18/12.90 A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: A_ltln_set$] : ! [v3: % 87.18/12.90 A_ltln_set_a_ltln_set_fun$] : (v1 = v0 | ~ (fun_app$l(v3, v2) = v1) | ~ % 87.18/12.90 (fun_app$l(v3, v2) = v0)) & ! [v0: int] : ! [v1: int] : ! [v2: % 87.18/12.90 A_ltln_set$] : ! [v3: A_ltln_set_int_fun$] : (v1 = v0 | ~ (fun_app$k(v3, % 87.18/12.90 v2) = v1) | ~ (fun_app$k(v3, v2) = v0)) & ! [v0: A_ltln_bool_fun$] : % 87.18/12.90 ! [v1: A_ltln_bool_fun$] : ! [v2: int] : ! [v3: Int_a_ltln_bool_fun_fun$] : % 87.18/12.90 (v1 = v0 | ~ (fun_app$j(v3, v2) = v1) | ~ (fun_app$j(v3, v2) = v0)) & ! % 87.18/12.90 [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: int] : ! [v3: % 87.18/12.90 Int_a_ltln_set_fun$] : (v1 = v0 | ~ (fun_app$i(v3, v2) = v1) | ~ % 87.18/12.90 (fun_app$i(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat$] : % 87.18/12.90 ! [v3: Nat_nat_fun$] : (v1 = v0 | ~ (fun_app$h(v3, v2) = v1) | ~ % 87.18/12.90 (fun_app$h(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 87.18/12.90 MultipleValueBool] : ! [v2: A_ltln_bool_fun$] : ! [v3: A_ltln_bool_fun$] : % 87.18/12.90 (v1 = v0 | ~ (less_eq$a(v3, v2) = v1) | ~ (less_eq$a(v3, v2) = v0)) & ! % 87.18/12.90 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_ltln_set$] : % 87.18/12.90 ! [v3: A_ltln_set$] : (v1 = v0 | ~ (less_eq$(v3, v2) = v1) | ~ (less_eq$(v3, % 87.18/12.90 v2) = v0)) & ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! % 87.18/12.90 [v3: A_ltln$] : (v1 = v0 | ~ (and_ltln$(v3, v2) = v1) | ~ (and_ltln$(v3, v2) % 87.18/12.90 = v0)) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 87.18/12.90 A_ltln_bool_fun$] : ! [v3: A_ltln_bool_fun_a_ltln_set_fun$] : (v1 = v0 | ~ % 87.18/12.90 (fun_app$g(v3, v2) = v1) | ~ (fun_app$g(v3, v2) = v0)) & ! [v0: A_ltln$] : % 87.18/12.90 ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! [v3: A_ltln$] : (v1 = v0 | ~ % 87.18/12.91 (or_ltln$(v3, v2) = v1) | ~ (or_ltln$(v3, v2) = v0)) & ! [v0: A_ltln$] : % 87.18/12.91 ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! [v3: A_ltln$] : (v1 = v0 | ~ % 87.18/12.91 (weakUntil_ltln$(v3, v2) = v1) | ~ (weakUntil_ltln$(v3, v2) = v0)) & ! % 87.18/12.91 [v0: Nat_a_set_fun_bool_fun$] : ! [v1: Nat_a_set_fun_bool_fun$] : ! [v2: % 87.18/12.91 Nat_a_set_fun_bool_fun$] : ! [v3: Nat_a_set_fun_bool_fun$] : (v1 = v0 | ~ % 87.18/12.91 (uuq$(v3, v2) = v1) | ~ (uuq$(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] : ! % 87.18/12.91 [v1: Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : ! [v3: Nat_set$] : (v1 = v0 | % 87.18/12.91 ~ (uuf$(v3, v2) = v1) | ~ (uuf$(v3, v2) = v0)) & ! [v0: % 87.18/12.91 Nat_a_set_fun_bool_fun$] : ! [v1: Nat_a_set_fun_bool_fun$] : ! [v2: % 87.18/12.91 Nat_a_set_fun_set$] : ! [v3: Nat_a_set_fun_set$] : (v1 = v0 | ~ (uut$(v3, % 87.18/12.91 v2) = v1) | ~ (uut$(v3, v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: % 87.18/12.91 Nat_bool_fun$] : ! [v2: Nat_set$] : ! [v3: Nat_set$] : (v1 = v0 | ~ % 87.18/12.91 (uus$(v3, v2) = v1) | ~ (uus$(v3, v2) = v0)) & ! [v0: A_ltln_bool_fun$] : % 87.18/12.91 ! [v1: A_ltln_bool_fun$] : ! [v2: Nat_a_set_fun$] : ! [v3: A_ltln$] : (v1 = % 87.18/12.91 v0 | ~ (uuz$(v3, v2) = v1) | ~ (uuz$(v3, v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: Nat_a_set_fun$] : ! % 87.18/12.91 [v3: A_ltln$] : (v1 = v0 | ~ (uum$(v3, v2) = v1) | ~ (uum$(v3, v2) = v0)) & % 87.18/12.91 ! [v0: A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: Nat_a_set_fun$] % 87.18/12.91 : ! [v3: A_ltln$] : (v1 = v0 | ~ (uux$(v3, v2) = v1) | ~ (uux$(v3, v2) = % 87.18/12.91 v0)) & ! [v0: A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: % 87.18/12.91 Nat_a_set_fun$] : ! [v3: A_ltln$] : (v1 = v0 | ~ (uuo$(v3, v2) = v1) | ~ % 87.18/12.91 (uuo$(v3, v2) = v0)) & ! [v0: A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] % 87.18/12.91 : ! [v2: A_ltln_bool_fun$] : ! [v3: A_ltln_bool_fun_a_ltln_bool_fun_fun$] : % 87.18/12.91 (v1 = v0 | ~ (fun_app$f(v3, v2) = v1) | ~ (fun_app$f(v3, v2) = v0)) & ! % 87.18/12.91 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 87.18/12.91 Nat_a_set_fun_set$] : ! [v3: Nat_a_set_fun$] : (v1 = v0 | ~ (member$b(v3, % 87.18/12.91 v2) = v1) | ~ (member$b(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 87.18/12.91 ! [v1: MultipleValueBool] : ! [v2: Nat_set$] : ! [v3: Nat$] : (v1 = v0 | ~ % 87.18/12.91 (member$a(v3, v2) = v1) | ~ (member$a(v3, v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: A_ltln_set$] : ! % 87.18/12.91 [v3: A_ltln_set_a_ltln_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$e(v3, v2) = v1) % 87.18/12.91 | ~ (fun_app$e(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 87.18/12.91 MultipleValueBool] : ! [v2: Nat_a_set_fun$] : ! [v3: % 87.18/12.91 Nat_a_set_fun_bool_fun$] : (v1 = v0 | ~ (fun_app$d(v3, v2) = v1) | ~ % 87.18/12.91 (fun_app$d(v3, v2) = v0)) & ! [v0: Int_bool_fun$] : ! [v1: Int_bool_fun$] % 87.18/12.91 : ! [v2: int] : ! [v3: Int_int_bool_fun_fun$] : (v1 = v0 | ~ (fun_app$c(v3, % 87.18/12.91 v2) = v1) | ~ (fun_app$c(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 87.18/12.91 ! [v1: MultipleValueBool] : ! [v2: int] : ! [v3: Int_bool_fun$] : (v1 = v0 | % 87.18/12.91 ~ (fun_app$b(v3, v2) = v1) | ~ (fun_app$b(v3, v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln$] : ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! [v3: A_ltln$] : (v1 = v0 % 87.18/12.91 | ~ (release_ltln$(v3, v2) = v1) | ~ (release_ltln$(v3, v2) = v0)) & ! % 87.18/12.91 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: A_ltln_set$] : % 87.18/12.91 ! [v3: A_ltln$] : (v1 = v0 | ~ (member$(v3, v2) = v1) | ~ (member$(v3, v2) = % 87.18/12.91 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 87.18/12.91 A_ltln$] : ! [v3: A_ltln_bool_fun$] : (v1 = v0 | ~ (fun_app$a(v3, v2) = % 87.18/12.91 v1) | ~ (fun_app$a(v3, v2) = v0)) & ! [v0: A_ltln$] : ! [v1: A_ltln$] : % 87.18/12.91 ! [v2: A_ltln$] : ! [v3: A_ltln$] : (v1 = v0 | ~ (until_ltln$(v3, v2) = v1) % 87.18/12.91 | ~ (until_ltln$(v3, v2) = v0)) & ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! % 87.18/12.91 [v2: A_ltln$] : ! [v3: A_ltln$] : (v1 = v0 | ~ (strongRelease_ltln$(v3, v2) % 87.18/12.91 = v1) | ~ (strongRelease_ltln$(v3, v2) = v0)) & ! [v0: A_ltln_set$] : ! % 87.18/12.91 [v1: A_ltln_set$] : ! [v2: Nat_a_set_fun$] : ! [v3: A_ltln$] : (v1 = v0 | ~ % 87.18/12.91 (f_G$(v3, v2) = v1) | ~ (f_G$(v3, v2) = v0)) & ! [v0: Nat_a_set_fun$] : ! % 87.18/12.91 [v1: Nat_a_set_fun$] : ! [v2: Nat_a_set_fun$] : ! [v3: Nat$] : (v1 = v0 | ~ % 87.18/12.91 (suffix$(v3, v2) = v1) | ~ (suffix$(v3, v2) = v0)) & ! [v0: % 87.18/12.91 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: Nat$] : ! [v3: % 87.18/12.91 Nat_bool_fun$] : (v1 = v0 | ~ (fun_app$(v3, v2) = v1) | ~ (fun_app$(v3, % 87.18/12.91 v2) = v0)) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: % 87.18/12.91 Nat_a_set_fun$] : ! [v3: A_ltln$] : (v1 = v0 | ~ (g$(v3, v2) = v1) | ~ % 87.18/12.91 (g$(v3, v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: int] : (v1 = v0 % 87.18/12.91 | ~ (nat$(v2) = v1) | ~ (nat$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_set_a_ltln_set_fun$] : ! [v1: A_ltln_set_a_ltln_set_fun$] : ! [v2: % 87.18/12.91 A_ltln_set$] : (v1 = v0 | ~ (sup$a(v2) = v1) | ~ (sup$a(v2) = v0)) & ! % 87.18/12.91 [v0: A_ltln_bool_fun_a_ltln_bool_fun_fun$] : ! [v1: % 87.18/12.91 A_ltln_bool_fun_a_ltln_bool_fun_fun$] : ! [v2: A_ltln_bool_fun$] : (v1 = v0 % 87.18/12.91 | ~ (inf$d(v2) = v1) | ~ (inf$d(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_set_a_ltln_set_fun$] : ! [v1: A_ltln_set_a_ltln_set_fun$] : ! [v2: % 87.18/12.91 A_ltln_set$] : (v1 = v0 | ~ (inf$(v2) = v1) | ~ (inf$(v2) = v0)) & ! [v0: % 87.18/12.91 Nat_a_set_fun_bool_fun$] : ! [v1: Nat_a_set_fun_bool_fun$] : ! [v2: % 87.18/12.91 A_ltln$] : (v1 = v0 | ~ (mu_stable$(v2) = v1) | ~ (mu_stable$(v2) = v0)) & % 87.18/12.91 ! [v0: int] : ! [v1: int] : ! [v2: Nat$] : (v1 = v0 | ~ (of_nat$(v2) = v1) % 87.18/12.91 | ~ (of_nat$(v2) = v0)) & ! [v0: Nat_set$] : ! [v1: Nat_set$] : ! [v2: % 87.18/12.91 Nat_bool_fun$] : (v1 = v0 | ~ (collect$a(v2) = v1) | ~ (collect$a(v2) = % 87.18/12.91 v0)) & ! [v0: Nat_a_set_fun_bool_fun$] : ! [v1: Nat_a_set_fun_bool_fun$] % 87.18/12.91 : ! [v2: A_ltln$] : (v1 = v0 | ~ (nu_stable$(v2) = v1) | ~ (nu_stable$(v2) % 87.18/12.91 = v0)) & ! [v0: Nat_a_set_fun_set$] : ! [v1: Nat_a_set_fun_set$] : ! % 87.18/12.91 [v2: A_ltln$] : (v1 = v0 | ~ (language_ltln$(v2) = v1) | ~ % 87.18/12.91 (language_ltln$(v2) = v0)) & ! [v0: Nat_a_set_fun_set$] : ! [v1: % 87.18/12.91 Nat_a_set_fun_set$] : ! [v2: Nat_a_set_fun_bool_fun$] : (v1 = v0 | ~ % 87.18/12.91 (collect$(v2) = v1) | ~ (collect$(v2) = v0)) & ! [v0: A_ltln$] : ! [v1: % 87.18/12.91 A_ltln$] : ! [v2: A_ltln_bool_fun$] : (v1 = v0 | ~ (eps$a(v2) = v1) | ~ % 87.18/12.91 (eps$a(v2) = v0)) & ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat_bool_fun$] : % 87.18/12.91 (v1 = v0 | ~ (eps$(v2) = v1) | ~ (eps$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun_a_ltln_bool_fun_fun$] : ! [v1: % 87.18/12.91 A_ltln_bool_fun_a_ltln_bool_fun_fun$] : ! [v2: A_ltln_bool_fun$] : (v1 = v0 % 87.18/12.91 | ~ (uur$(v2) = v1) | ~ (uur$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun_a_ltln_bool_fun_fun$] : ! [v1: % 87.18/12.91 A_ltln_bool_fun_a_ltln_bool_fun_fun$] : ! [v2: A_ltln_set$] : (v1 = v0 | ~ % 87.18/12.91 (uue$(v2) = v1) | ~ (uue$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_set_a_ltln_bool_fun_fun$] : ! [v1: A_ltln_set_a_ltln_bool_fun_fun$] % 87.18/12.91 : ! [v2: A_ltln_set$] : (v1 = v0 | ~ (uuu$(v2) = v1) | ~ (uuu$(v2) = v0)) & % 87.18/12.91 ! [v0: A_ltln_set_a_ltln_bool_fun_fun$] : ! [v1: % 87.18/12.91 A_ltln_set_a_ltln_bool_fun_fun$] : ! [v2: A_ltln_set$] : (v1 = v0 | ~ % 87.18/12.91 (uvc$(v2) = v1) | ~ (uvc$(v2) = v0)) & ! [v0: A_ltln_set$] : ! [v1: % 87.18/12.91 A_ltln_set$] : ! [v2: A_ltln$] : (v1 = v0 | ~ (subformulas_mu$(v2) = v1) | % 87.18/12.91 ~ (subformulas_mu$(v2) = v0)) & ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] % 87.18/12.91 : ! [v2: A_ltln$] : (v1 = v0 | ~ (subformulas_nu$(v2) = v1) | ~ % 87.18/12.91 (subformulas_nu$(v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: % 87.18/12.91 Nat_bool_fun$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ (uui$(v2) = v1) | ~ % 87.18/12.91 (uui$(v2) = v0)) & ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: % 87.18/12.91 Nat$] : (v1 = v0 | ~ (uub$(v2) = v1) | ~ (uub$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: A_ltln$] : (v1 = v0 % 87.18/12.91 | ~ (uua$(v2) = v1) | ~ (uua$(v2) = v0)) & ! [v0: Nat_bool_fun$] : ! % 87.18/12.91 [v1: Nat_bool_fun$] : ! [v2: Nat$] : (v1 = v0 | ~ (uud$(v2) = v1) | ~ % 87.18/12.91 (uud$(v2) = v0)) & ! [v0: A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : % 87.18/12.91 ! [v2: A_ltln$] : (v1 = v0 | ~ (uuc$(v2) = v1) | ~ (uuc$(v2) = v0)) & ! % 87.18/12.91 [v0: Nat_a_set_fun_bool_fun$] : ! [v1: Nat_a_set_fun_bool_fun$] : ! [v2: % 87.18/12.91 Nat_a_set_fun_set$] : (v1 = v0 | ~ (uuk$(v2) = v1) | ~ (uuk$(v2) = v0)) & % 87.18/12.91 ! [v0: Nat_bool_fun$] : ! [v1: Nat_bool_fun$] : ! [v2: Nat_set$] : (v1 = v0 % 87.18/12.91 | ~ (uuj$(v2) = v1) | ~ (uuj$(v2) = v0)) & ! [v0: % 87.18/12.91 Nat_a_set_fun_bool_fun$] : ! [v1: Nat_a_set_fun_bool_fun$] : ! [v2: % 87.18/12.91 A_ltln$] : (v1 = v0 | ~ (uug$(v2) = v1) | ~ (uug$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: Nat_a_set_fun$] : % 87.18/12.91 (v1 = v0 | ~ (uuy$(v2) = v1) | ~ (uuy$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: Nat_a_set_fun$] : % 87.18/12.91 (v1 = v0 | ~ (uuv$(v2) = v1) | ~ (uuv$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: Nat_a_set_fun$] : % 87.18/12.91 (v1 = v0 | ~ (uup$(v2) = v1) | ~ (uup$(v2) = v0)) & ! [v0: % 87.18/12.91 A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: Nat_a_set_fun$] : % 87.18/12.91 (v1 = v0 | ~ (semantics_ltln$(v2) = v1) | ~ (semantics_ltln$(v2) = v0)) & ! % 87.18/12.91 [v0: A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: Nat_a_set_fun$] : % 87.18/12.91 (v1 = v0 | ~ (uuw$(v2) = v1) | ~ (uuw$(v2) = v0)) & ! [v0: A_ltln_set$] : % 87.18/12.91 ! [v1: A_ltln_set$] : ! [v2: A_ltln$] : (v1 = v0 | ~ (subfrmlsn$(v2) = v1) | % 87.18/12.91 ~ (subfrmlsn$(v2) = v0)) & ! [v0: A_ltln_bool_fun$] : ! [v1: % 87.18/12.91 A_ltln_bool_fun$] : ! [v2: A_ltln$] : (v1 = v0 | ~ (uvb$(v2) = v1) | ~ % 87.18/12.91 (uvb$(v2) = v0)) % 87.18/12.91 % 87.18/12.91 Further assumptions not needed in the proof: % 87.18/12.91 -------------------------------------------- % 87.18/12.92 axiom1, axiom10, axiom100, axiom101, axiom102, axiom103, axiom104, axiom105, % 87.18/12.92 axiom106, axiom107, axiom108, axiom109, axiom11, axiom110, axiom111, axiom112, % 87.18/12.92 axiom113, axiom114, axiom115, axiom117, axiom118, axiom119, axiom12, axiom120, % 87.18/12.92 axiom121, axiom122, axiom123, axiom124, axiom125, axiom126, axiom127, axiom128, % 87.18/12.92 axiom129, axiom13, axiom130, axiom131, axiom132, axiom133, axiom134, axiom135, % 87.18/12.92 axiom136, axiom137, axiom138, axiom139, axiom14, axiom140, axiom141, axiom142, % 87.18/12.92 axiom143, axiom144, axiom145, axiom146, axiom147, axiom148, axiom149, axiom15, % 87.18/12.92 axiom150, axiom151, axiom152, axiom153, axiom154, axiom155, axiom156, axiom157, % 87.18/12.92 axiom158, axiom159, axiom16, axiom160, axiom161, axiom162, axiom163, axiom164, % 87.18/12.92 axiom165, axiom166, axiom167, axiom168, axiom169, axiom17, axiom170, axiom171, % 87.18/12.92 axiom172, axiom173, axiom174, axiom175, axiom176, axiom177, axiom178, axiom179, % 87.18/12.92 axiom18, axiom180, axiom181, axiom182, axiom183, axiom184, axiom185, axiom186, % 87.18/12.92 axiom187, axiom188, axiom189, axiom19, axiom190, axiom191, axiom192, axiom193, % 87.18/12.92 axiom194, axiom195, axiom196, axiom197, axiom198, axiom199, axiom2, axiom20, % 87.18/12.92 axiom200, axiom201, axiom202, axiom203, axiom204, axiom205, axiom206, axiom207, % 87.18/12.92 axiom208, axiom209, axiom21, axiom210, axiom211, axiom212, axiom213, axiom214, % 87.18/12.92 axiom215, axiom216, axiom217, axiom218, axiom219, axiom22, axiom220, axiom221, % 87.18/12.92 axiom222, axiom223, axiom224, axiom225, axiom226, axiom227, axiom228, axiom229, % 87.18/12.92 axiom23, axiom230, axiom231, axiom232, axiom233, axiom234, axiom235, axiom236, % 87.18/12.92 axiom237, axiom238, axiom239, axiom24, axiom240, axiom241, axiom242, axiom243, % 87.18/12.92 axiom244, axiom245, axiom246, axiom247, axiom248, axiom249, axiom25, axiom250, % 87.18/12.92 axiom251, axiom252, axiom253, axiom254, axiom255, axiom256, axiom257, axiom258, % 87.18/12.92 axiom259, axiom26, axiom260, axiom261, axiom262, axiom263, axiom264, axiom265, % 87.18/12.92 axiom266, axiom267, axiom268, axiom269, axiom27, axiom270, axiom271, axiom272, % 87.18/12.92 axiom273, axiom274, axiom275, axiom276, axiom277, axiom278, axiom279, axiom28, % 87.18/12.92 axiom280, axiom281, axiom282, axiom283, axiom284, axiom285, axiom286, axiom287, % 87.18/12.92 axiom288, axiom289, axiom29, axiom290, axiom291, axiom292, axiom293, axiom294, % 87.18/12.92 axiom295, axiom296, axiom297, axiom298, axiom299, axiom3, axiom300, axiom301, % 87.18/12.92 axiom302, axiom303, axiom304, axiom305, axiom306, axiom307, axiom308, axiom309, % 87.18/12.92 axiom31, axiom310, axiom311, axiom312, axiom313, axiom314, axiom315, axiom316, % 87.18/12.92 axiom317, axiom318, axiom319, axiom320, axiom321, axiom322, axiom323, axiom324, % 87.18/12.92 axiom325, axiom326, axiom327, axiom328, axiom329, axiom330, axiom331, axiom332, % 87.18/12.92 axiom333, axiom334, axiom335, axiom336, axiom337, axiom338, axiom339, axiom340, % 87.18/12.92 axiom341, axiom342, axiom343, axiom344, axiom345, axiom346, axiom347, axiom348, % 87.18/12.92 axiom349, axiom35, axiom350, axiom351, axiom352, axiom353, axiom354, axiom355, % 87.18/12.92 axiom356, axiom357, axiom358, axiom359, axiom36, axiom360, axiom361, axiom362, % 87.18/12.92 axiom363, axiom364, axiom365, axiom366, axiom367, axiom368, axiom369, axiom37, % 87.18/12.92 axiom370, axiom371, axiom372, axiom373, axiom374, axiom375, axiom376, axiom377, % 87.18/12.92 axiom378, axiom379, axiom38, axiom380, axiom381, axiom382, axiom383, axiom384, % 87.18/12.92 axiom385, axiom386, axiom387, axiom388, axiom389, axiom390, axiom391, axiom392, % 87.18/12.92 axiom393, axiom394, axiom395, axiom396, axiom397, axiom398, axiom399, axiom4, % 87.18/12.92 axiom40, axiom400, axiom401, axiom402, axiom403, axiom404, axiom405, axiom406, % 87.18/12.92 axiom407, axiom408, axiom409, axiom41, axiom410, axiom411, axiom412, axiom413, % 87.18/12.92 axiom414, axiom415, axiom416, axiom417, axiom418, axiom419, axiom42, axiom420, % 87.18/12.92 axiom421, axiom422, axiom423, axiom424, axiom425, axiom426, axiom427, axiom428, % 87.18/12.92 axiom429, axiom43, axiom430, axiom431, axiom432, axiom433, axiom434, axiom435, % 87.18/12.92 axiom436, axiom437, axiom438, axiom439, axiom44, axiom440, axiom441, axiom443, % 87.18/12.92 axiom444, axiom445, axiom446, axiom447, axiom448, axiom449, axiom45, axiom450, % 87.18/12.92 axiom451, axiom452, axiom453, axiom454, axiom455, axiom456, axiom457, axiom458, % 87.18/12.92 axiom459, axiom46, axiom460, axiom461, axiom462, axiom463, axiom464, axiom465, % 87.18/12.92 axiom466, axiom467, axiom468, axiom469, axiom47, axiom470, axiom471, axiom472, % 87.18/12.92 axiom473, axiom474, axiom475, axiom476, axiom477, axiom478, axiom479, axiom48, % 87.18/12.92 axiom480, axiom481, axiom482, axiom483, axiom484, axiom485, axiom486, axiom487, % 87.18/12.92 axiom488, axiom489, axiom49, axiom490, axiom491, axiom492, axiom493, axiom494, % 87.18/12.92 axiom495, axiom496, axiom497, axiom498, axiom499, axiom5, axiom50, axiom500, % 87.18/12.92 axiom501, axiom502, axiom503, axiom504, axiom505, axiom506, axiom507, axiom508, % 87.18/12.92 axiom509, axiom51, axiom510, axiom511, axiom512, axiom513, axiom514, axiom515, % 87.18/12.92 axiom516, axiom517, axiom518, axiom519, axiom52, axiom520, axiom521, axiom522, % 87.18/12.92 axiom523, axiom524, axiom525, axiom526, axiom527, axiom528, axiom529, axiom53, % 87.18/12.92 axiom530, axiom531, axiom532, axiom533, axiom534, axiom535, axiom536, axiom537, % 87.18/12.92 axiom538, axiom539, axiom54, axiom540, axiom541, axiom542, axiom543, axiom544, % 87.18/12.92 axiom545, axiom546, axiom547, axiom548, axiom549, axiom55, axiom550, axiom551, % 87.18/12.92 axiom552, axiom553, axiom554, axiom555, axiom556, axiom557, axiom558, axiom559, % 87.18/12.92 axiom56, axiom560, axiom561, axiom562, axiom563, axiom564, axiom565, axiom566, % 87.18/12.92 axiom567, axiom568, axiom569, axiom57, axiom570, axiom571, axiom572, axiom573, % 87.18/12.92 axiom574, axiom575, axiom576, axiom577, axiom578, axiom579, axiom58, axiom580, % 87.18/12.92 axiom581, axiom582, axiom583, axiom584, axiom585, axiom586, axiom587, axiom588, % 87.18/12.92 axiom589, axiom59, axiom590, axiom591, axiom592, axiom593, axiom594, axiom595, % 87.18/12.92 axiom596, axiom597, axiom598, axiom599, axiom6, axiom60, axiom600, axiom601, % 87.18/12.92 axiom602, axiom603, axiom604, axiom605, axiom606, axiom607, axiom608, axiom609, % 87.18/12.92 axiom61, axiom610, axiom611, axiom612, axiom613, axiom614, axiom615, axiom616, % 87.18/12.92 axiom617, axiom618, axiom619, axiom62, axiom620, axiom621, axiom622, axiom623, % 87.18/12.92 axiom624, axiom625, axiom626, axiom627, axiom628, axiom629, axiom63, axiom630, % 87.18/12.92 axiom631, axiom632, axiom633, axiom634, axiom635, axiom636, axiom637, axiom638, % 87.18/12.92 axiom639, axiom64, axiom640, axiom641, axiom642, axiom643, axiom644, axiom645, % 87.18/12.92 axiom646, axiom647, axiom65, axiom66, axiom67, axiom68, axiom69, axiom7, % 87.18/12.92 axiom70, axiom71, axiom72, axiom73, axiom74, axiom75, axiom76, axiom77, axiom78, % 87.18/12.92 axiom79, axiom8, axiom80, axiom81, axiom82, axiom83, axiom84, axiom85, axiom86, % 87.18/12.92 axiom87, axiom88, axiom89, axiom9, axiom90, axiom91, axiom92, axiom93, axiom94, % 87.18/12.92 axiom95, axiom96, axiom97, axiom98, axiom99, formula_649, formula_650, % 87.18/12.92 formula_651, formula_652, formula_653, formula_654, formula_655, formula_656, % 87.18/12.92 formula_657, formula_658 % 87.18/12.92 % 87.18/12.92 Those formulas are unsatisfiable: % 87.18/12.92 --------------------------------- % 87.18/12.92 % 87.18/12.92 Begin of proof % 87.18/12.92 | % 87.18/12.92 | ALPHA: (axiom0) implies: % 87.18/12.93 | (1) ? [v0: A_ltln_set$] : (f_G$(phi$, w$) = v0 & A_ltln_set$(v0) & ! [v1: % 87.18/12.93 | Nat$] : ! [v2: Nat_a_set_fun$] : ( ~ (suffix$(v1, w$) = v2) | ~ % 87.18/12.93 | Nat$(v1) | ? [v3: A_ltln_set$] : ? [v4: any] : (fun_app$(uu$, v1) % 87.18/12.93 | = v4 & g$(phi$, v2) = v3 & A_ltln_set$(v3) & ( ~ (v3 = v0) | v4 = % 87.18/12.93 | 0))) & ! [v1: Nat$] : ! [v2: Nat_a_set_fun$] : ( ~ % 87.18/12.93 | (suffix$(v1, w$) = v2) | ~ Nat$(v1) | ? [v3: any] : ? [v4: % 87.18/12.93 | A_ltln_set$] : (fun_app$(uu$, v1) = v3 & g$(phi$, v2) = v4 & % 87.18/12.93 | A_ltln_set$(v4) & ( ~ (v3 = 0) | v4 = v0)))) % 87.18/12.93 | % 87.18/12.93 | ALPHA: (axiom32) implies: % 87.18/12.93 | (2) ? [v0: A_ltln$] : ? [v1: A_ltln_set$] : (weakUntil_ltln$(psi_1$, % 87.18/12.93 | psi_2$) = v0 & member$(v0, v1) = 0 & f_G$(phi$, w$) = v1 & % 87.18/12.93 | A_ltln$(v0) & A_ltln_set$(v1)) % 87.18/12.93 | % 87.18/12.93 | ALPHA: (axiom33) implies: % 87.18/12.93 | (3) ? [v0: A_ltln_set$] : (f_G$(phi$, w$) = v0 & A_ltln_set$(v0) & ? [v1: % 87.18/12.93 | Nat$] : ? [v2: Nat_a_set_fun$] : (suffix$(v1, w$) = v2 & g$(phi$, % 87.18/12.93 | v2) = v0 & Nat_a_set_fun$(v2) & Nat$(v1))) % 87.18/12.93 | % 87.18/12.93 | ALPHA: (axiom34) implies: % 87.18/12.93 | (4) A_ltln$(phi$) % 87.18/12.93 | (5) ? [v0: A_ltln_set$] : ? [v1: Nat$] : ? [v2: Nat_a_set_fun$] : % 87.18/12.93 | (eps$(uu$) = v1 & f_G$(phi$, w$) = v0 & suffix$(v1, w$) = v2 & g$(phi$, % 87.18/12.93 | v2) = v0 & Nat_a_set_fun$(v2) & A_ltln_set$(v0) & Nat$(v1)) % 87.18/12.93 | % 87.18/12.93 | ALPHA: (axiom39) implies: % 87.18/12.94 | (6) ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! [v2: Nat_a_set_fun$] : ! [v3: % 87.18/12.94 | A_ltln_set$] : ( ~ (member$(v0, v3) = 0) | ~ (g$(v1, v2) = v3) | ~ % 87.18/12.94 | Nat_a_set_fun$(v2) | ~ A_ltln$(v1) | ~ A_ltln$(v0) | ? [v4: % 87.18/12.94 | A_ltln_bool_fun$] : ? [v5: A_ltln$] : (semantics_ltln$(v2) = v4 & % 87.18/12.94 | release_ltln$(false_ltln$, v0) = v5 & fun_app$a(v4, v5) = 0 & % 87.18/12.94 | A_ltln$(v5) & A_ltln_bool_fun$(v4))) % 87.18/12.94 | % 87.18/12.94 | ALPHA: (axiom116) implies: % 87.18/12.94 | (7) ! [v0: Nat_a_set_fun$] : ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.94 | A_ltln_bool_fun$] : ! [v4: A_ltln$] : ! [v5: int] : (v5 = 0 | ~ % 87.18/12.94 | (semantics_ltln$(v0) = v3) | ~ (release_ltln$(v1, v2) = v4) | ~ % 87.18/12.94 | (fun_app$a(v3, v4) = v5) | ~ Nat_a_set_fun$(v0) | ~ A_ltln$(v2) | % 87.18/12.94 | ~ A_ltln$(v1) | ? [v6: Nat$] : ? [v7: Nat_a_set_fun$] : ? [v8: % 87.18/12.94 | A_ltln_bool_fun$] : ? [v9: int] : ? [v10: int] : ( ~ (v9 = 0) & % 87.18/12.94 | of_nat$(v6) = v10 & semantics_ltln$(v7) = v8 & fun_app$a(v8, v2) = % 87.18/12.94 | v9 & suffix$(v6, v0) = v7 & Nat_a_set_fun$(v7) & % 87.18/12.94 | A_ltln_bool_fun$(v8) & Nat$(v6) & ! [v11: Nat$] : ! [v12: % 87.18/12.94 | Nat_a_set_fun$] : ! [v13: A_ltln_bool_fun$] : ( ~ % 87.18/12.94 | (semantics_ltln$(v12) = v13) | ~ (fun_app$a(v13, v1) = 0) | ~ % 87.18/12.94 | (suffix$(v11, v0) = v12) | ~ Nat$(v11) | ? [v14: int] : % 87.18/12.94 | ($lesseq(v10, v14) & of_nat$(v11) = v14)))) % 87.18/12.94 | % 87.18/12.94 | ALPHA: (axiom442) implies: % 87.18/12.94 | (8) ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! [v2: Nat_a_set_fun$] : ! [v3: % 87.18/12.94 | A_ltln_set$] : ( ~ (member$(v0, v3) = 0) | ~ (f_G$(v1, v2) = v3) | % 87.18/12.94 | ~ Nat_a_set_fun$(v2) | ~ A_ltln$(v1) | ~ A_ltln$(v0) | ? [v4: % 87.18/12.94 | A_ltln_bool_fun$] : ? [v5: A_ltln$] : ? [v6: A_ltln$] : % 87.18/12.94 | (semantics_ltln$(v2) = v4 & release_ltln$(false_ltln$, v0) = v5 & % 87.18/12.94 | fun_app$a(v4, v6) = 0 & until_ltln$(true_ltln$, v5) = v6 & % 87.18/12.94 | A_ltln$(v6) & A_ltln$(v5) & A_ltln_bool_fun$(v4))) % 87.18/12.94 | % 87.18/12.94 | ALPHA: (conjecture30) implies: % 87.18/12.94 | (9) A_ltln$(false_ltln$) % 87.18/12.94 | (10) Nat_a_set_fun$(w$) % 87.18/12.94 | (11) ? [v0: Nat$] : ? [v1: Nat_a_set_fun$] : ? [v2: A_ltln_bool_fun$] : % 87.18/12.94 | ? [v3: A_ltln$] : ? [v4: A_ltln$] : ? [v5: int] : ( ~ (v5 = 0) & % 87.18/12.94 | eps$(uu$) = v0 & weakUntil_ltln$(psi_1$, psi_2$) = v3 & % 87.18/12.95 | semantics_ltln$(v1) = v2 & release_ltln$(false_ltln$, v3) = v4 & % 87.18/12.95 | fun_app$a(v2, v4) = v5 & suffix$(v0, w$) = v1 & Nat_a_set_fun$(v1) & % 87.18/12.95 | A_ltln$(v4) & A_ltln$(v3) & A_ltln_bool_fun$(v2) & Nat$(v0)) % 87.18/12.95 | % 87.18/12.95 | ALPHA: (function-axioms) implies: % 87.18/12.95 | (12) ! [v0: A_ltln_bool_fun$] : ! [v1: A_ltln_bool_fun$] : ! [v2: % 87.18/12.95 | Nat_a_set_fun$] : (v1 = v0 | ~ (semantics_ltln$(v2) = v1) | ~ % 87.18/12.95 | (semantics_ltln$(v2) = v0)) % 87.18/12.95 | (13) ! [v0: Nat$] : ! [v1: Nat$] : ! [v2: Nat_bool_fun$] : (v1 = v0 | ~ % 87.18/12.95 | (eps$(v2) = v1) | ~ (eps$(v2) = v0)) % 87.18/12.95 | (14) ! [v0: Nat_a_set_fun$] : ! [v1: Nat_a_set_fun$] : ! [v2: % 87.18/12.95 | Nat_a_set_fun$] : ! [v3: Nat$] : (v1 = v0 | ~ (suffix$(v3, v2) = % 87.18/12.95 | v1) | ~ (suffix$(v3, v2) = v0)) % 87.18/12.95 | (15) ! [v0: A_ltln_set$] : ! [v1: A_ltln_set$] : ! [v2: Nat_a_set_fun$] % 87.18/12.95 | : ! [v3: A_ltln$] : (v1 = v0 | ~ (f_G$(v3, v2) = v1) | ~ (f_G$(v3, % 87.18/12.95 | v2) = v0)) % 87.18/12.95 | (16) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 87.18/12.95 | A_ltln$] : ! [v3: A_ltln_bool_fun$] : (v1 = v0 | ~ (fun_app$a(v3, % 87.18/12.95 | v2) = v1) | ~ (fun_app$a(v3, v2) = v0)) % 87.18/12.95 | (17) ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.95 | A_ltln$] : (v1 = v0 | ~ (release_ltln$(v3, v2) = v1) | ~ % 87.18/12.95 | (release_ltln$(v3, v2) = v0)) % 87.18/12.95 | (18) ! [v0: A_ltln$] : ! [v1: A_ltln$] : ! [v2: A_ltln$] : ! [v3: % 87.18/12.95 | A_ltln$] : (v1 = v0 | ~ (weakUntil_ltln$(v3, v2) = v1) | ~ % 87.18/12.95 | (weakUntil_ltln$(v3, v2) = v0)) % 87.18/12.95 | % 87.18/12.95 | DELTA: instantiating (2) with fresh symbols all_593_0, all_593_1 gives: % 87.18/12.95 | (19) weakUntil_ltln$(psi_1$, psi_2$) = all_593_1 & member$(all_593_1, % 87.18/12.95 | all_593_0) = 0 & f_G$(phi$, w$) = all_593_0 & A_ltln$(all_593_1) & % 87.18/12.95 | A_ltln_set$(all_593_0) % 87.18/12.95 | % 87.18/12.95 | ALPHA: (19) implies: % 87.18/12.95 | (20) f_G$(phi$, w$) = all_593_0 % 87.18/12.95 | (21) member$(all_593_1, all_593_0) = 0 % 87.18/12.95 | (22) weakUntil_ltln$(psi_1$, psi_2$) = all_593_1 % 87.18/12.95 | % 87.18/12.95 | DELTA: instantiating (3) with fresh symbol all_615_0 gives: % 87.18/12.95 | (23) f_G$(phi$, w$) = all_615_0 & A_ltln_set$(all_615_0) & ? [v0: Nat$] : % 87.18/12.95 | ? [v1: Nat_a_set_fun$] : (suffix$(v0, w$) = v1 & g$(phi$, v1) = % 87.18/12.95 | all_615_0 & Nat_a_set_fun$(v1) & Nat$(v0)) % 87.18/12.96 | % 87.18/12.96 | ALPHA: (23) implies: % 87.18/12.96 | (24) f_G$(phi$, w$) = all_615_0 % 87.18/12.96 | (25) ? [v0: Nat$] : ? [v1: Nat_a_set_fun$] : (suffix$(v0, w$) = v1 & % 87.18/12.96 | g$(phi$, v1) = all_615_0 & Nat_a_set_fun$(v1) & Nat$(v0)) % 87.18/12.96 | % 87.18/12.96 | DELTA: instantiating (5) with fresh symbols all_619_0, all_619_1, all_619_2 % 87.18/12.96 | gives: % 87.18/12.96 | (26) eps$(uu$) = all_619_1 & f_G$(phi$, w$) = all_619_2 & % 87.18/12.96 | suffix$(all_619_1, w$) = all_619_0 & g$(phi$, all_619_0) = all_619_2 & % 87.18/12.96 | Nat_a_set_fun$(all_619_0) & A_ltln_set$(all_619_2) & Nat$(all_619_1) % 87.18/12.96 | % 87.18/12.96 | ALPHA: (26) implies: % 87.18/12.96 | (27) g$(phi$, all_619_0) = all_619_2 % 87.18/12.96 | (28) suffix$(all_619_1, w$) = all_619_0 % 87.18/12.96 | (29) f_G$(phi$, w$) = all_619_2 % 87.18/12.96 | (30) eps$(uu$) = all_619_1 % 87.18/12.96 | % 87.18/12.96 | DELTA: instantiating (11) with fresh symbols all_623_0, all_623_1, all_623_2, % 87.18/12.96 | all_623_3, all_623_4, all_623_5 gives: % 87.18/12.96 | (31) ~ (all_623_0 = 0) & eps$(uu$) = all_623_5 & weakUntil_ltln$(psi_1$, % 87.18/12.96 | psi_2$) = all_623_2 & semantics_ltln$(all_623_4) = all_623_3 & % 87.18/12.96 | release_ltln$(false_ltln$, all_623_2) = all_623_1 & % 87.18/12.96 | fun_app$a(all_623_3, all_623_1) = all_623_0 & suffix$(all_623_5, w$) = % 87.18/12.96 | all_623_4 & Nat_a_set_fun$(all_623_4) & A_ltln$(all_623_1) & % 87.18/12.96 | A_ltln$(all_623_2) & A_ltln_bool_fun$(all_623_3) & Nat$(all_623_5) % 87.18/12.96 | % 87.18/12.96 | ALPHA: (31) implies: % 87.18/12.96 | (32) ~ (all_623_0 = 0) % 87.18/12.96 | (33) A_ltln$(all_623_2) % 87.18/12.96 | (34) Nat_a_set_fun$(all_623_4) % 87.18/12.96 | (35) suffix$(all_623_5, w$) = all_623_4 % 87.18/12.96 | (36) fun_app$a(all_623_3, all_623_1) = all_623_0 % 87.18/12.96 | (37) release_ltln$(false_ltln$, all_623_2) = all_623_1 % 87.18/12.96 | (38) semantics_ltln$(all_623_4) = all_623_3 % 87.18/12.96 | (39) weakUntil_ltln$(psi_1$, psi_2$) = all_623_2 % 87.18/12.96 | (40) eps$(uu$) = all_623_5 % 87.18/12.96 | % 87.18/12.96 | DELTA: instantiating (1) with fresh symbol all_629_0 gives: % 87.18/12.96 | (41) f_G$(phi$, w$) = all_629_0 & A_ltln_set$(all_629_0) & ! [v0: Nat$] : % 87.18/12.96 | ! [v1: Nat_a_set_fun$] : ( ~ (suffix$(v0, w$) = v1) | ~ Nat$(v0) | ? % 87.18/12.96 | [v2: A_ltln_set$] : ? [v3: any] : (fun_app$(uu$, v0) = v3 & % 87.18/12.96 | g$(phi$, v1) = v2 & A_ltln_set$(v2) & ( ~ (v2 = all_629_0) | v3 = % 87.18/12.96 | 0))) & ! [v0: Nat$] : ! [v1: Nat_a_set_fun$] : ( ~ % 87.18/12.96 | (suffix$(v0, w$) = v1) | ~ Nat$(v0) | ? [v2: any] : ? [v3: % 87.18/12.96 | A_ltln_set$] : (fun_app$(uu$, v0) = v2 & g$(phi$, v1) = v3 & % 87.18/12.96 | A_ltln_set$(v3) & ( ~ (v2 = 0) | v3 = all_629_0))) % 87.18/12.96 | % 87.18/12.96 | ALPHA: (41) implies: % 87.18/12.96 | (42) f_G$(phi$, w$) = all_629_0 % 87.18/12.96 | % 87.18/12.96 | DELTA: instantiating (25) with fresh symbols all_644_0, all_644_1 gives: % 87.18/12.96 | (43) suffix$(all_644_1, w$) = all_644_0 & g$(phi$, all_644_0) = all_615_0 & % 87.18/12.96 | Nat_a_set_fun$(all_644_0) & Nat$(all_644_1) % 87.18/12.96 | % 87.18/12.96 | ALPHA: (43) implies: % 87.18/12.97 | (44) Nat_a_set_fun$(all_644_0) % 87.18/12.97 | (45) g$(phi$, all_644_0) = all_615_0 % 87.18/12.97 | % 87.18/12.97 | GROUND_INST: instantiating (15) with all_615_0, all_619_2, w$, phi$, % 87.18/12.97 | simplifying with (24), (29) gives: % 87.18/12.97 | (46) all_619_2 = all_615_0 % 87.18/12.97 | % 87.18/12.97 | GROUND_INST: instantiating (15) with all_619_2, all_629_0, w$, phi$, % 87.18/12.97 | simplifying with (29), (42) gives: % 87.18/12.97 | (47) all_629_0 = all_619_2 % 87.18/12.97 | % 87.18/12.97 | GROUND_INST: instantiating (15) with all_593_0, all_629_0, w$, phi$, % 87.18/12.97 | simplifying with (20), (42) gives: % 87.18/12.97 | (48) all_629_0 = all_593_0 % 87.18/12.97 | % 87.18/12.97 | GROUND_INST: instantiating (18) with all_593_1, all_623_2, psi_2$, psi_1$, % 87.18/12.97 | simplifying with (22), (39) gives: % 87.18/12.97 | (49) all_623_2 = all_593_1 % 87.18/12.97 | % 87.18/12.97 | GROUND_INST: instantiating (13) with all_619_1, all_623_5, uu$, simplifying % 87.18/12.97 | with (30), (40) gives: % 87.18/12.97 | (50) all_623_5 = all_619_1 % 87.18/12.97 | % 87.18/12.97 | COMBINE_EQS: (47), (48) imply: % 87.18/12.97 | (51) all_619_2 = all_593_0 % 87.18/12.97 | % 87.18/12.97 | SIMP: (51) implies: % 87.18/12.97 | (52) all_619_2 = all_593_0 % 87.18/12.97 | % 87.18/12.97 | COMBINE_EQS: (46), (52) imply: % 87.18/12.97 | (53) all_615_0 = all_593_0 % 87.18/12.97 | % 87.18/12.97 | SIMP: (53) implies: % 87.18/12.97 | (54) all_615_0 = all_593_0 % 87.18/12.97 | % 87.18/12.97 | REDUCE: (37), (49) imply: % 87.18/12.97 | (55) release_ltln$(false_ltln$, all_593_1) = all_623_1 % 87.18/12.97 | % 87.18/12.97 | REDUCE: (35), (50) imply: % 87.18/12.97 | (56) suffix$(all_619_1, w$) = all_623_4 % 87.18/12.97 | % 87.18/12.97 | REDUCE: (45), (54) imply: % 87.18/12.97 | (57) g$(phi$, all_644_0) = all_593_0 % 87.18/12.97 | % 87.18/12.97 | REDUCE: (27), (52) imply: % 87.18/12.97 | (58) g$(phi$, all_619_0) = all_593_0 % 87.18/12.97 | % 87.18/12.97 | REDUCE: (33), (49) imply: % 87.18/12.97 | (59) A_ltln$(all_593_1) % 87.18/12.97 | % 87.18/12.97 | GROUND_INST: instantiating (14) with all_619_0, all_623_4, w$, all_619_1, % 87.18/12.97 | simplifying with (28), (56) gives: % 87.18/12.97 | (60) all_623_4 = all_619_0 % 87.18/12.97 | % 87.18/12.97 | REDUCE: (38), (60) imply: % 87.18/12.97 | (61) semantics_ltln$(all_619_0) = all_623_3 % 87.18/12.97 | % 87.18/12.97 | REDUCE: (34), (60) imply: % 87.18/12.97 | (62) Nat_a_set_fun$(all_619_0) % 87.18/12.97 | % 87.18/12.97 | GROUND_INST: instantiating (8) with all_593_1, phi$, w$, all_593_0, % 87.18/12.97 | simplifying with (4), (10), (20), (21), (59) gives: % 87.18/12.98 | (63) ? [v0: A_ltln_bool_fun$] : ? [v1: A_ltln$] : ? [v2: A_ltln$] : % 87.18/12.98 | (semantics_ltln$(w$) = v0 & release_ltln$(false_ltln$, all_593_1) = v1 % 87.18/12.98 | & fun_app$a(v0, v2) = 0 & until_ltln$(true_ltln$, v1) = v2 & % 87.18/12.98 | A_ltln$(v2) & A_ltln$(v1) & A_ltln_bool_fun$(v0)) % 87.18/12.98 | % 87.18/12.98 | GROUND_INST: instantiating (6) with all_593_1, phi$, all_644_0, all_593_0, % 87.63/12.98 | simplifying with (4), (21), (44), (57), (59) gives: % 87.63/12.98 | (64) ? [v0: A_ltln_bool_fun$] : ? [v1: A_ltln$] : % 87.63/12.98 | (semantics_ltln$(all_644_0) = v0 & release_ltln$(false_ltln$, % 87.63/12.98 | all_593_1) = v1 & fun_app$a(v0, v1) = 0 & A_ltln$(v1) & % 87.63/12.98 | A_ltln_bool_fun$(v0)) % 87.63/12.98 | % 87.63/12.98 | GROUND_INST: instantiating (6) with all_593_1, phi$, all_619_0, all_593_0, % 87.63/12.98 | simplifying with (4), (21), (58), (59), (62) gives: % 87.63/12.98 | (65) ? [v0: A_ltln_bool_fun$] : ? [v1: A_ltln$] : % 87.63/12.98 | (semantics_ltln$(all_619_0) = v0 & release_ltln$(false_ltln$, % 87.63/12.98 | all_593_1) = v1 & fun_app$a(v0, v1) = 0 & A_ltln$(v1) & % 87.63/12.98 | A_ltln_bool_fun$(v0)) % 87.63/12.98 | % 87.63/12.98 | GROUND_INST: instantiating (7) with all_619_0, false_ltln$, all_593_1, % 87.63/12.98 | all_623_3, all_623_1, all_623_0, simplifying with (9), (36), % 87.63/12.98 | (55), (59), (61), (62) gives: % 87.63/12.98 | (66) all_623_0 = 0 | ? [v0: Nat$] : ? [v1: Nat_a_set_fun$] : ? [v2: % 87.63/12.98 | A_ltln_bool_fun$] : ? [v3: int] : ? [v4: int] : ( ~ (v3 = 0) & % 87.63/12.98 | of_nat$(v0) = v4 & semantics_ltln$(v1) = v2 & fun_app$a(v2, % 87.63/12.98 | all_593_1) = v3 & suffix$(v0, all_619_0) = v1 & Nat_a_set_fun$(v1) % 87.63/12.98 | & A_ltln_bool_fun$(v2) & Nat$(v0) & ! [v5: Nat$] : ! [v6: % 87.63/12.98 | Nat_a_set_fun$] : ! [v7: A_ltln_bool_fun$] : ( ~ % 87.63/12.98 | (semantics_ltln$(v6) = v7) | ~ (fun_app$a(v7, false_ltln$) = 0) | % 87.63/12.98 | ~ (suffix$(v5, all_619_0) = v6) | ~ Nat$(v5) | ? [v8: int] : % 87.63/12.98 | ($lesseq(v4, v8) & of_nat$(v5) = v8))) % 87.63/12.98 | % 87.63/12.98 | DELTA: instantiating (65) with fresh symbols all_682_0, all_682_1 gives: % 87.63/12.98 | (67) semantics_ltln$(all_619_0) = all_682_1 & release_ltln$(false_ltln$, % 87.63/12.98 | all_593_1) = all_682_0 & fun_app$a(all_682_1, all_682_0) = 0 & % 87.63/12.98 | A_ltln$(all_682_0) & A_ltln_bool_fun$(all_682_1) % 87.63/12.98 | % 87.63/12.98 | ALPHA: (67) implies: % 87.63/12.98 | (68) fun_app$a(all_682_1, all_682_0) = 0 % 87.63/12.98 | (69) release_ltln$(false_ltln$, all_593_1) = all_682_0 % 87.63/12.98 | (70) semantics_ltln$(all_619_0) = all_682_1 % 87.63/12.98 | % 87.63/12.98 | DELTA: instantiating (64) with fresh symbols all_684_0, all_684_1 gives: % 87.63/12.98 | (71) semantics_ltln$(all_644_0) = all_684_1 & release_ltln$(false_ltln$, % 87.63/12.98 | all_593_1) = all_684_0 & fun_app$a(all_684_1, all_684_0) = 0 & % 87.63/12.98 | A_ltln$(all_684_0) & A_ltln_bool_fun$(all_684_1) % 87.63/12.98 | % 87.63/12.98 | ALPHA: (71) implies: % 87.63/12.98 | (72) release_ltln$(false_ltln$, all_593_1) = all_684_0 % 87.63/12.98 | % 87.63/12.98 | DELTA: instantiating (63) with fresh symbols all_686_0, all_686_1, all_686_2 % 87.63/12.98 | gives: % 87.63/12.99 | (73) semantics_ltln$(w$) = all_686_2 & release_ltln$(false_ltln$, % 87.63/12.99 | all_593_1) = all_686_1 & fun_app$a(all_686_2, all_686_0) = 0 & % 87.63/12.99 | until_ltln$(true_ltln$, all_686_1) = all_686_0 & A_ltln$(all_686_0) & % 87.63/12.99 | A_ltln$(all_686_1) & A_ltln_bool_fun$(all_686_2) % 87.63/12.99 | % 87.63/12.99 | ALPHA: (73) implies: % 87.63/12.99 | (74) release_ltln$(false_ltln$, all_593_1) = all_686_1 % 87.63/12.99 | % 87.63/12.99 | BETA: splitting (66) gives: % 87.63/12.99 | % 87.63/12.99 | Case 1: % 87.63/12.99 | | % 87.63/12.99 | | (75) all_623_0 = 0 % 87.63/12.99 | | % 87.63/12.99 | | REDUCE: (32), (75) imply: % 87.63/12.99 | | (76) $false % 87.63/12.99 | | % 87.63/12.99 | | CLOSE: (76) is inconsistent. % 87.63/12.99 | | % 87.63/12.99 | Case 2: % 87.63/12.99 | | % 87.63/12.99 | | % 87.63/12.99 | | GROUND_INST: instantiating (17) with all_623_1, all_684_0, all_593_1, % 87.63/12.99 | | false_ltln$, simplifying with (55), (72) gives: % 87.63/12.99 | | (77) all_684_0 = all_623_1 % 87.63/12.99 | | % 87.63/12.99 | | GROUND_INST: instantiating (17) with all_684_0, all_686_1, all_593_1, % 87.63/12.99 | | false_ltln$, simplifying with (72), (74) gives: % 87.63/12.99 | | (78) all_686_1 = all_684_0 % 87.63/12.99 | | % 87.63/12.99 | | GROUND_INST: instantiating (17) with all_682_0, all_686_1, all_593_1, % 87.63/12.99 | | false_ltln$, simplifying with (69), (74) gives: % 87.63/12.99 | | (79) all_686_1 = all_682_0 % 87.63/12.99 | | % 87.63/12.99 | | GROUND_INST: instantiating (12) with all_623_3, all_682_1, all_619_0, % 87.63/12.99 | | simplifying with (61), (70) gives: % 87.63/12.99 | | (80) all_682_1 = all_623_3 % 87.63/12.99 | | % 87.63/12.99 | | COMBINE_EQS: (78), (79) imply: % 87.63/12.99 | | (81) all_684_0 = all_682_0 % 87.63/12.99 | | % 87.63/12.99 | | SIMP: (81) implies: % 87.63/12.99 | | (82) all_684_0 = all_682_0 % 87.63/12.99 | | % 87.63/12.99 | | COMBINE_EQS: (77), (82) imply: % 87.63/12.99 | | (83) all_682_0 = all_623_1 % 87.63/12.99 | | % 87.63/12.99 | | REDUCE: (68), (80), (83) imply: % 87.63/12.99 | | (84) fun_app$a(all_623_3, all_623_1) = 0 % 87.63/12.99 | | % 87.63/12.99 | | GROUND_INST: instantiating (16) with all_623_0, 0, all_623_1, all_623_3, % 87.63/12.99 | | simplifying with (36), (84) gives: % 87.63/12.99 | | (85) all_623_0 = 0 % 87.63/12.99 | | % 87.63/12.99 | | REDUCE: (32), (85) imply: % 87.63/12.99 | | (86) $false % 87.63/12.99 | | % 87.63/12.99 | | CLOSE: (86) is inconsistent. % 87.63/12.99 | | % 87.63/12.99 | End of split % 87.63/12.99 | % 87.63/12.99 End of proof % 87.63/12.99 % SZS output end Proof for theBenchmark % 87.71/12.99 % 87.71/12.99 12413ms %------------------------------------------------------------------------------