%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWV403+1 : TPTP v8.1.2. Released v3.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n023.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 22:56:11 EDT 2023 % Result : Theorem 8.85s 1.88s % Output : Proof 10.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV403+1 : TPTP v8.1.2. Released v3.3.0. % 0.03/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Aug 29 04:19:10 EDT 2023 % 0.12/0.33 % CPUTime : % 0.55/0.60 ________ _____ % 0.55/0.60 ___ __ \_________(_)________________________________ % 0.55/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.55/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.55/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.55/0.60 % 0.55/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.55/0.60 (2023-06-19) % 0.55/0.60 % 0.55/0.60 (c) Philipp Rümmer, 2009-2023 % 0.55/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.55/0.60 Amanda Stjerna. % 0.55/0.60 Free software under BSD-3-Clause. % 0.55/0.60 % 0.55/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.55/0.60 % 0.55/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.55/0.61 Running up to 7 provers in parallel. % 0.55/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.55/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.55/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.55/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.55/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.55/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.55/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 2.78/1.05 Prover 4: Preprocessing ... % 2.78/1.06 Prover 1: Preprocessing ... % 3.06/1.09 Prover 5: Preprocessing ... % 3.06/1.09 Prover 3: Preprocessing ... % 3.06/1.09 Prover 6: Preprocessing ... % 3.06/1.10 Prover 2: Preprocessing ... % 3.06/1.10 Prover 0: Preprocessing ... % 5.73/1.45 Prover 5: Proving ... % 5.73/1.46 Prover 1: Constructing countermodel ... % 5.73/1.47 Prover 6: Proving ... % 5.98/1.50 Prover 3: Constructing countermodel ... % 5.98/1.52 Prover 2: Proving ... % 6.46/1.54 Prover 4: Constructing countermodel ... % 6.46/1.54 Prover 0: Proving ... % 8.85/1.88 Prover 3: proved (1246ms) % 8.85/1.88 % 8.85/1.88 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.85/1.88 % 8.85/1.88 Prover 6: stopped % 8.85/1.88 Prover 0: stopped % 8.85/1.88 Prover 5: stopped % 8.85/1.89 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.85/1.89 Prover 2: stopped % 8.85/1.89 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.85/1.89 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 8.85/1.89 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 8.85/1.90 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 8.85/1.91 Prover 7: Preprocessing ... % 9.40/1.92 Prover 8: Preprocessing ... % 9.40/1.95 Prover 10: Preprocessing ... % 9.40/1.96 Prover 13: Preprocessing ... % 9.40/1.96 Prover 11: Preprocessing ... % 9.75/1.99 Prover 7: Warning: ignoring some quantifiers % 9.75/2.00 Prover 7: Constructing countermodel ... % 9.75/2.03 Prover 10: Warning: ignoring some quantifiers % 9.75/2.03 Prover 8: Warning: ignoring some quantifiers % 9.75/2.04 Prover 8: Constructing countermodel ... % 9.75/2.04 Prover 10: Constructing countermodel ... % 9.75/2.04 Prover 1: Found proof (size 96) % 9.75/2.04 Prover 1: proved (1424ms) % 9.75/2.04 Prover 7: stopped % 9.75/2.04 Prover 8: stopped % 9.75/2.04 Prover 11: stopped % 9.75/2.04 Prover 4: stopped % 9.75/2.04 Prover 10: stopped % 9.75/2.04 Prover 13: stopped % 9.75/2.05 % 9.75/2.05 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.75/2.05 % 10.34/2.06 % SZS output start Proof for theBenchmark % 10.34/2.06 Assumptions after simplification: % 10.34/2.06 --------------------------------- % 10.34/2.06 % 10.34/2.06 (ax23) % 10.46/2.09 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 10.46/2.09 $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | ~ (pair_in_list(v6, v2, v4) = % 10.46/2.09 v7) | ~ (pair(v1, v3) = v5) | ~ (insert_slb(v0, v5) = v6) | ~ $i(v4) | % 10.46/2.09 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ( ? [v8: int] : ( ~ (v8 = 0) % 10.46/2.09 & pair_in_list(v0, v2, v4) = v8) & ( ~ (v4 = v3) | ~ (v2 = v1)))) & ! % 10.46/2.09 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 10.46/2.09 : ! [v6: $i] : ( ~ (pair_in_list(v6, v2, v4) = 0) | ~ (pair(v1, v3) = v5) | % 10.46/2.09 ~ (insert_slb(v0, v5) = v6) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 10.46/2.09 | ~ $i(v0) | pair_in_list(v0, v2, v4) = 0 | (v4 = v3 & v2 = v1)) % 10.46/2.09 % 10.46/2.09 (ax29) % 10.46/2.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 10.46/2.10 $i] : ! [v6: $i] : ( ~ (update_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | % 10.46/2.10 ~ (insert_slb(v0, v4) = v5) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 10.46/2.10 | ? [v7: any] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : (update_slb(v0, % 10.46/2.10 v2) = v8 & pair(v1, v2) = v9 & insert_slb(v8, v9) = v10 & % 10.46/2.10 strictly_less_than(v3, v2) = v7 & $i(v10) & $i(v9) & $i(v8) & ( ~ (v7 = 0) % 10.46/2.10 | v10 = v6))) % 10.46/2.10 % 10.46/2.10 (ax30) % 10.46/2.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 10.46/2.10 $i] : ! [v6: $i] : ( ~ (update_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | % 10.46/2.10 ~ (insert_slb(v0, v4) = v5) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 10.46/2.10 | ? [v7: any] : ? [v8: $i] : ? [v9: $i] : (update_slb(v0, v2) = v8 & % 10.46/2.10 insert_slb(v8, v4) = v9 & less_than(v2, v3) = v7 & $i(v9) & $i(v8) & ( ~ % 10.46/2.10 (v7 = 0) | v9 = v6))) % 10.46/2.10 % 10.46/2.10 (l39_co) % 10.46/2.10 ? [v0: $i] : ($i(v0) & ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 10.46/2.10 : ! [v5: int] : (v5 = 0 | ~ (update_slb(v0, v3) = v4) | ~ % 10.46/2.10 (pair_in_list(v4, v1, v3) = v5) | ~ (strictly_less_than(v2, v3) = 0) | ~ % 10.46/2.10 $i(v3) | ~ $i(v2) | ~ $i(v1) | ? [v6: int] : ( ~ (v6 = 0) & % 10.46/2.10 pair_in_list(v0, v1, v2) = v6)) & ? [v1: $i] : ? [v2: $i] : ? [v3: % 10.46/2.10 $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] % 10.46/2.10 : ? [v9: int] : ( ~ (v9 = 0) & update_slb(v7, v3) = v8 & pair_in_list(v8, % 10.46/2.10 v1, v3) = v9 & pair_in_list(v7, v1, v2) = 0 & pair(v4, v5) = v6 & % 10.46/2.10 insert_slb(v0, v6) = v7 & strictly_less_than(v2, v3) = 0 & $i(v8) & $i(v7) % 10.46/2.10 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1))) % 10.46/2.10 % 10.46/2.10 (stricly_smaller_definition) % 10.46/2.11 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ % 10.46/2.11 (strictly_less_than(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : % 10.46/2.11 ? [v4: any] : (less_than(v1, v0) = v4 & less_than(v0, v1) = v3 & ( ~ (v3 = % 10.46/2.11 0) | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ( ~ % 10.46/2.11 (strictly_less_than(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: int] : ( % 10.46/2.11 ~ (v2 = 0) & less_than(v1, v0) = v2 & less_than(v0, v1) = 0)) % 10.46/2.11 % 10.46/2.11 (totality) % 10.46/2.11 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (less_than(v0, v1) = % 10.46/2.11 v2) | ~ $i(v1) | ~ $i(v0) | less_than(v1, v0) = 0) % 10.46/2.11 % 10.46/2.11 (transitivity) % 10.46/2.11 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 10.46/2.11 (less_than(v0, v2) = v3) | ~ (less_than(v0, v1) = 0) | ~ $i(v2) | ~ % 10.46/2.11 $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & less_than(v1, v2) = v4)) % 10.46/2.11 % 10.46/2.11 (function-axioms) % 10.46/2.11 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 10.46/2.11 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (pair_in_list(v4, v3, v2) = v1) | ~ % 10.46/2.11 (pair_in_list(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 10.46/2.11 ! [v3: $i] : (v1 = v0 | ~ (update_slb(v3, v2) = v1) | ~ (update_slb(v3, v2) % 10.46/2.11 = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 % 10.46/2.11 | ~ (lookup_slb(v3, v2) = v1) | ~ (lookup_slb(v3, v2) = v0)) & ! [v0: $i] % 10.46/2.11 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (remove_slb(v3, v2) % 10.46/2.11 = v1) | ~ (remove_slb(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 10.46/2.11 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 10.46/2.11 (contains_slb(v3, v2) = v1) | ~ (contains_slb(v3, v2) = v0)) & ! [v0: $i] % 10.46/2.11 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (pair(v3, v2) = v1) % 10.46/2.11 | ~ (pair(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 10.46/2.11 [v3: $i] : (v1 = v0 | ~ (insert_slb(v3, v2) = v1) | ~ (insert_slb(v3, v2) = % 10.46/2.11 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 10.46/2.11 $i] : ! [v3: $i] : (v1 = v0 | ~ (strictly_less_than(v3, v2) = v1) | ~ % 10.46/2.11 (strictly_less_than(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 10.46/2.11 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 10.46/2.11 (less_than(v3, v2) = v1) | ~ (less_than(v3, v2) = v0)) & ! [v0: % 10.46/2.11 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 10.46/2.11 ~ (isnonempty_slb(v2) = v1) | ~ (isnonempty_slb(v2) = v0)) % 10.46/2.11 % 10.46/2.11 Further assumptions not needed in the proof: % 10.46/2.11 -------------------------------------------- % 10.46/2.11 ax18, ax19, ax20, ax21, ax22, ax24, ax25, ax26, ax27, ax28, bottom_smallest, % 10.46/2.11 reflexivity % 10.46/2.11 % 10.46/2.11 Those formulas are unsatisfiable: % 10.46/2.11 --------------------------------- % 10.46/2.11 % 10.46/2.11 Begin of proof % 10.46/2.11 | % 10.46/2.11 | ALPHA: (stricly_smaller_definition) implies: % 10.46/2.12 | (1) ! [v0: $i] : ! [v1: $i] : ( ~ (strictly_less_than(v0, v1) = 0) | ~ % 10.46/2.12 | $i(v1) | ~ $i(v0) | ? [v2: int] : ( ~ (v2 = 0) & less_than(v1, v0) % 10.46/2.12 | = v2 & less_than(v0, v1) = 0)) % 10.46/2.12 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ % 10.46/2.12 | (strictly_less_than(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 10.46/2.12 | any] : ? [v4: any] : (less_than(v1, v0) = v4 & less_than(v0, v1) = % 10.46/2.12 | v3 & ( ~ (v3 = 0) | v4 = 0))) % 10.46/2.12 | % 10.46/2.12 | ALPHA: (ax23) implies: % 10.46/2.12 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 10.46/2.12 | ! [v5: $i] : ! [v6: $i] : ( ~ (pair_in_list(v6, v2, v4) = 0) | ~ % 10.46/2.12 | (pair(v1, v3) = v5) | ~ (insert_slb(v0, v5) = v6) | ~ $i(v4) | ~ % 10.46/2.12 | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | pair_in_list(v0, v2, v4) % 10.46/2.12 | = 0 | (v4 = v3 & v2 = v1)) % 10.46/2.12 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 10.46/2.12 | ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | ~ % 10.46/2.12 | (pair_in_list(v6, v2, v4) = v7) | ~ (pair(v1, v3) = v5) | ~ % 10.46/2.12 | (insert_slb(v0, v5) = v6) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 10.46/2.12 | $i(v1) | ~ $i(v0) | ( ? [v8: int] : ( ~ (v8 = 0) & pair_in_list(v0, % 10.46/2.12 | v2, v4) = v8) & ( ~ (v4 = v3) | ~ (v2 = v1)))) % 10.46/2.12 | % 10.46/2.12 | ALPHA: (function-axioms) implies: % 10.46/2.12 | (5) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 10.46/2.12 | ! [v3: $i] : (v1 = v0 | ~ (less_than(v3, v2) = v1) | ~ % 10.46/2.12 | (less_than(v3, v2) = v0)) % 10.46/2.12 | (6) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 10.46/2.12 | ! [v3: $i] : (v1 = v0 | ~ (strictly_less_than(v3, v2) = v1) | ~ % 10.46/2.12 | (strictly_less_than(v3, v2) = v0)) % 10.46/2.12 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 10.46/2.12 | (update_slb(v3, v2) = v1) | ~ (update_slb(v3, v2) = v0)) % 10.71/2.12 | (8) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 10.71/2.12 | ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (pair_in_list(v4, v3, v2) = % 10.71/2.12 | v1) | ~ (pair_in_list(v4, v3, v2) = v0)) % 10.71/2.12 | % 10.71/2.12 | DELTA: instantiating (l39_co) with fresh symbol all_23_0 gives: % 10.71/2.12 | (9) $i(all_23_0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 10.71/2.12 | ! [v4: int] : (v4 = 0 | ~ (update_slb(all_23_0, v2) = v3) | ~ % 10.71/2.12 | (pair_in_list(v3, v0, v2) = v4) | ~ (strictly_less_than(v1, v2) = 0) % 10.71/2.12 | | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & % 10.71/2.12 | pair_in_list(all_23_0, v0, v1) = v5)) & ? [v0: $i] : ? [v1: $i] : % 10.71/2.12 | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 10.71/2.12 | ? [v7: $i] : ? [v8: int] : ( ~ (v8 = 0) & update_slb(v6, v2) = v7 & % 10.71/2.12 | pair_in_list(v7, v0, v2) = v8 & pair_in_list(v6, v0, v1) = 0 & % 10.71/2.12 | pair(v3, v4) = v5 & insert_slb(all_23_0, v5) = v6 & % 10.71/2.12 | strictly_less_than(v1, v2) = 0 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & % 10.71/2.13 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 10.71/2.13 | % 10.71/2.13 | ALPHA: (9) implies: % 10.71/2.13 | (10) $i(all_23_0) % 10.71/2.13 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 10.71/2.13 | (v4 = 0 | ~ (update_slb(all_23_0, v2) = v3) | ~ (pair_in_list(v3, % 10.71/2.13 | v0, v2) = v4) | ~ (strictly_less_than(v1, v2) = 0) | ~ $i(v2) % 10.71/2.13 | | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & % 10.71/2.13 | pair_in_list(all_23_0, v0, v1) = v5)) % 10.71/2.13 | (12) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 10.71/2.13 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: int] : ( ~ (v8 = 0) & % 10.71/2.13 | update_slb(v6, v2) = v7 & pair_in_list(v7, v0, v2) = v8 & % 10.71/2.13 | pair_in_list(v6, v0, v1) = 0 & pair(v3, v4) = v5 & % 10.71/2.13 | insert_slb(all_23_0, v5) = v6 & strictly_less_than(v1, v2) = 0 & % 10.71/2.13 | $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 10.71/2.13 | $i(v0)) % 10.71/2.13 | % 10.71/2.13 | DELTA: instantiating (12) with fresh symbols all_26_0, all_26_1, all_26_2, % 10.71/2.13 | all_26_3, all_26_4, all_26_5, all_26_6, all_26_7, all_26_8 gives: % 10.71/2.13 | (13) ~ (all_26_0 = 0) & update_slb(all_26_2, all_26_6) = all_26_1 & % 10.71/2.13 | pair_in_list(all_26_1, all_26_8, all_26_6) = all_26_0 & % 10.71/2.13 | pair_in_list(all_26_2, all_26_8, all_26_7) = 0 & pair(all_26_5, % 10.71/2.13 | all_26_4) = all_26_3 & insert_slb(all_23_0, all_26_3) = all_26_2 & % 10.71/2.13 | strictly_less_than(all_26_7, all_26_6) = 0 & $i(all_26_1) & % 10.71/2.13 | $i(all_26_2) & $i(all_26_3) & $i(all_26_4) & $i(all_26_5) & % 10.71/2.13 | $i(all_26_6) & $i(all_26_7) & $i(all_26_8) % 10.71/2.13 | % 10.71/2.13 | ALPHA: (13) implies: % 10.71/2.13 | (14) ~ (all_26_0 = 0) % 10.71/2.13 | (15) $i(all_26_8) % 10.71/2.13 | (16) $i(all_26_7) % 10.71/2.13 | (17) $i(all_26_6) % 10.71/2.13 | (18) $i(all_26_5) % 10.71/2.13 | (19) $i(all_26_4) % 10.71/2.13 | (20) strictly_less_than(all_26_7, all_26_6) = 0 % 10.71/2.13 | (21) insert_slb(all_23_0, all_26_3) = all_26_2 % 10.71/2.13 | (22) pair(all_26_5, all_26_4) = all_26_3 % 10.71/2.13 | (23) pair_in_list(all_26_2, all_26_8, all_26_7) = 0 % 10.71/2.13 | (24) pair_in_list(all_26_1, all_26_8, all_26_6) = all_26_0 % 10.71/2.13 | (25) update_slb(all_26_2, all_26_6) = all_26_1 % 10.71/2.13 | % 10.71/2.13 | GROUND_INST: instantiating (1) with all_26_7, all_26_6, simplifying with (16), % 10.71/2.13 | (17), (20) gives: % 10.71/2.13 | (26) ? [v0: int] : ( ~ (v0 = 0) & less_than(all_26_6, all_26_7) = v0 & % 10.71/2.13 | less_than(all_26_7, all_26_6) = 0) % 10.71/2.13 | % 10.71/2.13 | GROUND_INST: instantiating (3) with all_23_0, all_26_5, all_26_8, all_26_4, % 10.71/2.13 | all_26_7, all_26_3, all_26_2, simplifying with (10), (15), (16), % 10.71/2.13 | (18), (19), (21), (22), (23) gives: % 10.71/2.13 | (27) pair_in_list(all_23_0, all_26_8, all_26_7) = 0 | (all_26_4 = all_26_7 % 10.71/2.13 | & all_26_5 = all_26_8) % 10.71/2.13 | % 10.71/2.13 | GROUND_INST: instantiating (ax29) with all_23_0, all_26_5, all_26_6, all_26_4, % 10.71/2.13 | all_26_3, all_26_2, all_26_1, simplifying with (10), (17), (18), % 10.71/2.13 | (19), (21), (22), (25) gives: % 10.71/2.14 | (28) ? [v0: any] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 10.71/2.14 | (update_slb(all_23_0, all_26_6) = v1 & pair(all_26_5, all_26_6) = v2 & % 10.71/2.14 | insert_slb(v1, v2) = v3 & strictly_less_than(all_26_4, all_26_6) = % 10.71/2.14 | v0 & $i(v3) & $i(v2) & $i(v1) & ( ~ (v0 = 0) | v3 = all_26_1)) % 10.71/2.14 | % 10.71/2.14 | GROUND_INST: instantiating (ax30) with all_23_0, all_26_5, all_26_6, all_26_4, % 10.71/2.14 | all_26_3, all_26_2, all_26_1, simplifying with (10), (17), (18), % 10.71/2.14 | (19), (21), (22), (25) gives: % 10.71/2.14 | (29) ? [v0: any] : ? [v1: $i] : ? [v2: $i] : (update_slb(all_23_0, % 10.71/2.14 | all_26_6) = v1 & insert_slb(v1, all_26_3) = v2 & % 10.71/2.14 | less_than(all_26_6, all_26_4) = v0 & $i(v2) & $i(v1) & ( ~ (v0 = 0) % 10.71/2.14 | | v2 = all_26_1)) % 10.71/2.14 | % 10.71/2.14 | DELTA: instantiating (26) with fresh symbol all_34_0 gives: % 10.71/2.14 | (30) ~ (all_34_0 = 0) & less_than(all_26_6, all_26_7) = all_34_0 & % 10.71/2.14 | less_than(all_26_7, all_26_6) = 0 % 10.71/2.14 | % 10.71/2.14 | ALPHA: (30) implies: % 10.71/2.14 | (31) ~ (all_34_0 = 0) % 10.71/2.14 | (32) less_than(all_26_6, all_26_7) = all_34_0 % 10.71/2.14 | % 10.71/2.14 | DELTA: instantiating (29) with fresh symbols all_36_0, all_36_1, all_36_2 % 10.71/2.14 | gives: % 10.71/2.14 | (33) update_slb(all_23_0, all_26_6) = all_36_1 & insert_slb(all_36_1, % 10.71/2.14 | all_26_3) = all_36_0 & less_than(all_26_6, all_26_4) = all_36_2 & % 10.71/2.14 | $i(all_36_0) & $i(all_36_1) & ( ~ (all_36_2 = 0) | all_36_0 = % 10.71/2.14 | all_26_1) % 10.71/2.14 | % 10.71/2.14 | ALPHA: (33) implies: % 10.71/2.14 | (34) less_than(all_26_6, all_26_4) = all_36_2 % 10.71/2.14 | (35) insert_slb(all_36_1, all_26_3) = all_36_0 % 10.71/2.14 | (36) update_slb(all_23_0, all_26_6) = all_36_1 % 10.71/2.14 | (37) ~ (all_36_2 = 0) | all_36_0 = all_26_1 % 10.71/2.14 | % 10.71/2.14 | DELTA: instantiating (28) with fresh symbols all_38_0, all_38_1, all_38_2, % 10.71/2.14 | all_38_3 gives: % 10.71/2.14 | (38) update_slb(all_23_0, all_26_6) = all_38_2 & pair(all_26_5, all_26_6) = % 10.71/2.14 | all_38_1 & insert_slb(all_38_2, all_38_1) = all_38_0 & % 10.71/2.14 | strictly_less_than(all_26_4, all_26_6) = all_38_3 & $i(all_38_0) & % 10.71/2.14 | $i(all_38_1) & $i(all_38_2) & ( ~ (all_38_3 = 0) | all_38_0 = % 10.71/2.14 | all_26_1) % 10.71/2.14 | % 10.71/2.14 | ALPHA: (38) implies: % 10.71/2.14 | (39) $i(all_38_2) % 10.71/2.14 | (40) strictly_less_than(all_26_4, all_26_6) = all_38_3 % 10.71/2.14 | (41) insert_slb(all_38_2, all_38_1) = all_38_0 % 10.71/2.14 | (42) pair(all_26_5, all_26_6) = all_38_1 % 10.71/2.14 | (43) update_slb(all_23_0, all_26_6) = all_38_2 % 10.71/2.14 | (44) ~ (all_38_3 = 0) | all_38_0 = all_26_1 % 10.71/2.14 | % 10.71/2.14 | GROUND_INST: instantiating (7) with all_36_1, all_38_2, all_26_6, all_23_0, % 10.71/2.14 | simplifying with (36), (43) gives: % 10.71/2.14 | (45) all_38_2 = all_36_1 % 10.71/2.14 | % 10.71/2.14 | REDUCE: (41), (45) imply: % 10.71/2.14 | (46) insert_slb(all_36_1, all_38_1) = all_38_0 % 10.71/2.14 | % 10.71/2.14 | REDUCE: (39), (45) imply: % 10.71/2.14 | (47) $i(all_36_1) % 10.71/2.14 | % 10.71/2.14 | GROUND_INST: instantiating (totality) with all_26_6, all_26_4, all_36_2, % 10.71/2.14 | simplifying with (17), (19), (34) gives: % 10.71/2.14 | (48) all_36_2 = 0 | less_than(all_26_4, all_26_6) = 0 % 10.71/2.14 | % 10.71/2.14 | GROUND_INST: instantiating (2) with all_26_4, all_26_6, all_38_3, simplifying % 10.71/2.14 | with (17), (19), (40) gives: % 10.71/2.14 | (49) all_38_3 = 0 | ? [v0: any] : ? [v1: any] : (less_than(all_26_4, % 10.71/2.14 | all_26_6) = v0 & less_than(all_26_6, all_26_4) = v1 & ( ~ (v0 = 0) % 10.71/2.14 | | v1 = 0)) % 10.71/2.14 | % 10.71/2.14 | BETA: splitting (27) gives: % 10.71/2.14 | % 10.71/2.15 | Case 1: % 10.71/2.15 | | % 10.71/2.15 | | (50) pair_in_list(all_23_0, all_26_8, all_26_7) = 0 % 10.71/2.15 | | % 10.71/2.15 | | BETA: splitting (37) gives: % 10.71/2.15 | | % 10.71/2.15 | | Case 1: % 10.71/2.15 | | | % 10.71/2.15 | | | (51) ~ (all_36_2 = 0) % 10.71/2.15 | | | % 10.71/2.15 | | | BETA: splitting (48) gives: % 10.71/2.15 | | | % 10.71/2.15 | | | Case 1: % 10.71/2.15 | | | | % 10.71/2.15 | | | | (52) less_than(all_26_4, all_26_6) = 0 % 10.71/2.15 | | | | % 10.71/2.15 | | | | BETA: splitting (49) gives: % 10.71/2.15 | | | | % 10.71/2.15 | | | | Case 1: % 10.71/2.15 | | | | | % 10.71/2.15 | | | | | (53) all_38_3 = 0 % 10.71/2.15 | | | | | % 10.71/2.15 | | | | | BETA: splitting (44) gives: % 10.71/2.15 | | | | | % 10.71/2.15 | | | | | Case 1: % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | | (54) ~ (all_38_3 = 0) % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | | REDUCE: (53), (54) imply: % 10.71/2.15 | | | | | | (55) $false % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | | CLOSE: (55) is inconsistent. % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | Case 2: % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | | (56) all_38_0 = all_26_1 % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | | REDUCE: (46), (56) imply: % 10.71/2.15 | | | | | | (57) insert_slb(all_36_1, all_38_1) = all_26_1 % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | | GROUND_INST: instantiating (4) with all_36_1, all_26_5, all_26_8, % 10.71/2.15 | | | | | | all_26_6, all_26_6, all_38_1, all_26_1, all_26_0, % 10.71/2.15 | | | | | | simplifying with (15), (17), (18), (24), (42), (47), % 10.71/2.15 | | | | | | (57) gives: % 10.71/2.15 | | | | | | (58) all_26_0 = 0 | ( ~ (all_26_5 = all_26_8) & ? [v0: int] : ( % 10.71/2.15 | | | | | | ~ (v0 = 0) & pair_in_list(all_36_1, all_26_8, all_26_6) % 10.71/2.15 | | | | | | = v0)) % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | | BETA: splitting (58) gives: % 10.71/2.15 | | | | | | % 10.71/2.15 | | | | | | Case 1: % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | (59) all_26_0 = 0 % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | REDUCE: (14), (59) imply: % 10.71/2.15 | | | | | | | (60) $false % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | CLOSE: (60) is inconsistent. % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | Case 2: % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | (61) ~ (all_26_5 = all_26_8) & ? [v0: int] : ( ~ (v0 = 0) & % 10.71/2.15 | | | | | | | pair_in_list(all_36_1, all_26_8, all_26_6) = v0) % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | ALPHA: (61) implies: % 10.71/2.15 | | | | | | | (62) ? [v0: int] : ( ~ (v0 = 0) & pair_in_list(all_36_1, % 10.71/2.15 | | | | | | | all_26_8, all_26_6) = v0) % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | DELTA: instantiating (62) with fresh symbol all_83_0 gives: % 10.71/2.15 | | | | | | | (63) ~ (all_83_0 = 0) & pair_in_list(all_36_1, all_26_8, % 10.71/2.15 | | | | | | | all_26_6) = all_83_0 % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | ALPHA: (63) implies: % 10.71/2.15 | | | | | | | (64) ~ (all_83_0 = 0) % 10.71/2.15 | | | | | | | (65) pair_in_list(all_36_1, all_26_8, all_26_6) = all_83_0 % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | GROUND_INST: instantiating (11) with all_26_8, all_26_7, all_26_6, % 10.71/2.15 | | | | | | | all_36_1, all_83_0, simplifying with (15), (16), % 10.71/2.15 | | | | | | | (17), (20), (36), (65) gives: % 10.71/2.15 | | | | | | | (66) all_83_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 10.71/2.15 | | | | | | | pair_in_list(all_23_0, all_26_8, all_26_7) = v0) % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | BETA: splitting (66) gives: % 10.71/2.15 | | | | | | | % 10.71/2.15 | | | | | | | Case 1: % 10.71/2.15 | | | | | | | | % 10.71/2.15 | | | | | | | | (67) all_83_0 = 0 % 10.71/2.15 | | | | | | | | % 10.71/2.15 | | | | | | | | REDUCE: (64), (67) imply: % 10.71/2.15 | | | | | | | | (68) $false % 10.71/2.15 | | | | | | | | % 10.71/2.15 | | | | | | | | CLOSE: (68) is inconsistent. % 10.71/2.15 | | | | | | | | % 10.71/2.15 | | | | | | | Case 2: % 10.71/2.15 | | | | | | | | % 10.71/2.15 | | | | | | | | (69) ? [v0: int] : ( ~ (v0 = 0) & pair_in_list(all_23_0, % 10.71/2.15 | | | | | | | | all_26_8, all_26_7) = v0) % 10.71/2.15 | | | | | | | | % 10.71/2.15 | | | | | | | | DELTA: instantiating (69) with fresh symbol all_102_0 gives: % 10.71/2.15 | | | | | | | | (70) ~ (all_102_0 = 0) & pair_in_list(all_23_0, all_26_8, % 10.71/2.15 | | | | | | | | all_26_7) = all_102_0 % 10.71/2.15 | | | | | | | | % 10.71/2.16 | | | | | | | | REF_CLOSE: (8), (50), (70) are inconsistent by sub-proof #1. % 10.71/2.16 | | | | | | | | % 10.71/2.16 | | | | | | | End of split % 10.71/2.16 | | | | | | | % 10.71/2.16 | | | | | | End of split % 10.71/2.16 | | | | | | % 10.71/2.16 | | | | | End of split % 10.71/2.16 | | | | | % 10.71/2.16 | | | | Case 2: % 10.71/2.16 | | | | | % 10.71/2.16 | | | | | (71) ? [v0: any] : ? [v1: any] : (less_than(all_26_4, all_26_6) = % 10.71/2.16 | | | | | v0 & less_than(all_26_6, all_26_4) = v1 & ( ~ (v0 = 0) | v1 % 10.71/2.16 | | | | | = 0)) % 10.71/2.16 | | | | | % 10.71/2.16 | | | | | DELTA: instantiating (71) with fresh symbols all_72_0, all_72_1 gives: % 10.71/2.16 | | | | | (72) less_than(all_26_4, all_26_6) = all_72_1 & less_than(all_26_6, % 10.71/2.16 | | | | | all_26_4) = all_72_0 & ( ~ (all_72_1 = 0) | all_72_0 = 0) % 10.71/2.16 | | | | | % 10.71/2.16 | | | | | ALPHA: (72) implies: % 10.71/2.16 | | | | | (73) less_than(all_26_6, all_26_4) = all_72_0 % 10.71/2.16 | | | | | (74) less_than(all_26_4, all_26_6) = all_72_1 % 10.71/2.16 | | | | | (75) ~ (all_72_1 = 0) | all_72_0 = 0 % 10.71/2.16 | | | | | % 10.89/2.16 | | | | | GROUND_INST: instantiating (5) with all_36_2, all_72_0, all_26_4, % 10.89/2.16 | | | | | all_26_6, simplifying with (34), (73) gives: % 10.89/2.16 | | | | | (76) all_72_0 = all_36_2 % 10.89/2.16 | | | | | % 10.89/2.16 | | | | | GROUND_INST: instantiating (5) with 0, all_72_1, all_26_6, all_26_4, % 10.89/2.16 | | | | | simplifying with (52), (74) gives: % 10.89/2.16 | | | | | (77) all_72_1 = 0 % 10.89/2.16 | | | | | % 10.89/2.16 | | | | | BETA: splitting (75) gives: % 10.89/2.16 | | | | | % 10.89/2.16 | | | | | Case 1: % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | | (78) ~ (all_72_1 = 0) % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | | REDUCE: (77), (78) imply: % 10.89/2.16 | | | | | | (79) $false % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | | CLOSE: (79) is inconsistent. % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | Case 2: % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | | (80) all_72_0 = 0 % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | | COMBINE_EQS: (76), (80) imply: % 10.89/2.16 | | | | | | (81) all_36_2 = 0 % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | | REDUCE: (51), (81) imply: % 10.89/2.16 | | | | | | (82) $false % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | | CLOSE: (82) is inconsistent. % 10.89/2.16 | | | | | | % 10.89/2.16 | | | | | End of split % 10.89/2.16 | | | | | % 10.89/2.16 | | | | End of split % 10.89/2.16 | | | | % 10.89/2.16 | | | Case 2: % 10.89/2.16 | | | | % 10.89/2.16 | | | | (83) all_36_2 = 0 % 10.89/2.16 | | | | % 10.89/2.16 | | | | REDUCE: (51), (83) imply: % 10.89/2.16 | | | | (84) $false % 10.89/2.16 | | | | % 10.89/2.16 | | | | CLOSE: (84) is inconsistent. % 10.89/2.16 | | | | % 10.89/2.16 | | | End of split % 10.89/2.16 | | | % 10.89/2.16 | | Case 2: % 10.89/2.16 | | | % 10.89/2.16 | | | (85) all_36_2 = 0 % 10.89/2.16 | | | (86) all_36_0 = all_26_1 % 10.89/2.16 | | | % 10.89/2.16 | | | REDUCE: (35), (86) imply: % 10.89/2.16 | | | (87) insert_slb(all_36_1, all_26_3) = all_26_1 % 10.89/2.16 | | | % 10.89/2.16 | | | REDUCE: (34), (85) imply: % 10.89/2.16 | | | (88) less_than(all_26_6, all_26_4) = 0 % 10.89/2.16 | | | % 10.89/2.16 | | | GROUND_INST: instantiating (transitivity) with all_26_6, all_26_4, % 10.89/2.16 | | | all_26_7, all_34_0, simplifying with (16), (17), (19), (32), % 10.89/2.16 | | | (88) gives: % 10.89/2.16 | | | (89) all_34_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & less_than(all_26_4, % 10.89/2.16 | | | all_26_7) = v0) % 10.89/2.16 | | | % 10.89/2.16 | | | GROUND_INST: instantiating (4) with all_36_1, all_26_5, all_26_8, % 10.89/2.16 | | | all_26_4, all_26_6, all_26_3, all_26_1, all_26_0, simplifying % 10.89/2.16 | | | with (15), (17), (18), (19), (22), (24), (47), (87) gives: % 10.89/2.16 | | | (90) all_26_0 = 0 | ( ? [v0: int] : ( ~ (v0 = 0) & % 10.89/2.16 | | | pair_in_list(all_36_1, all_26_8, all_26_6) = v0) & ( ~ % 10.89/2.16 | | | (all_26_4 = all_26_6) | ~ (all_26_5 = all_26_8))) % 10.89/2.16 | | | % 10.89/2.16 | | | BETA: splitting (90) gives: % 10.89/2.16 | | | % 10.89/2.16 | | | Case 1: % 10.89/2.16 | | | | % 10.89/2.16 | | | | (91) all_26_0 = 0 % 10.89/2.16 | | | | % 10.89/2.16 | | | | REDUCE: (14), (91) imply: % 10.89/2.16 | | | | (92) $false % 10.89/2.17 | | | | % 10.89/2.17 | | | | CLOSE: (92) is inconsistent. % 10.89/2.17 | | | | % 10.89/2.17 | | | Case 2: % 10.89/2.17 | | | | % 10.89/2.17 | | | | (93) ? [v0: int] : ( ~ (v0 = 0) & pair_in_list(all_36_1, all_26_8, % 10.89/2.17 | | | | all_26_6) = v0) & ( ~ (all_26_4 = all_26_6) | ~ (all_26_5 = % 10.89/2.17 | | | | all_26_8)) % 10.89/2.17 | | | | % 10.89/2.17 | | | | ALPHA: (93) implies: % 10.89/2.17 | | | | (94) ? [v0: int] : ( ~ (v0 = 0) & pair_in_list(all_36_1, all_26_8, % 10.89/2.17 | | | | all_26_6) = v0) % 10.89/2.17 | | | | % 10.89/2.17 | | | | DELTA: instantiating (94) with fresh symbol all_80_0 gives: % 10.89/2.17 | | | | (95) ~ (all_80_0 = 0) & pair_in_list(all_36_1, all_26_8, all_26_6) = % 10.89/2.17 | | | | all_80_0 % 10.89/2.17 | | | | % 10.89/2.17 | | | | ALPHA: (95) implies: % 10.89/2.17 | | | | (96) ~ (all_80_0 = 0) % 10.89/2.17 | | | | (97) pair_in_list(all_36_1, all_26_8, all_26_6) = all_80_0 % 10.89/2.17 | | | | % 10.89/2.17 | | | | BETA: splitting (89) gives: % 10.89/2.17 | | | | % 10.89/2.17 | | | | Case 1: % 10.89/2.17 | | | | | % 10.89/2.17 | | | | | (98) all_34_0 = 0 % 10.89/2.17 | | | | | % 10.89/2.17 | | | | | REDUCE: (31), (98) imply: % 10.89/2.17 | | | | | (99) $false % 10.89/2.17 | | | | | % 10.89/2.17 | | | | | CLOSE: (99) is inconsistent. % 10.89/2.17 | | | | | % 10.89/2.17 | | | | Case 2: % 10.89/2.17 | | | | | % 10.89/2.17 | | | | | % 10.89/2.17 | | | | | GROUND_INST: instantiating (11) with all_26_8, all_26_7, all_26_6, % 10.89/2.17 | | | | | all_36_1, all_80_0, simplifying with (15), (16), (17), % 10.89/2.17 | | | | | (20), (36), (97) gives: % 10.89/2.17 | | | | | (100) all_80_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 10.89/2.17 | | | | | pair_in_list(all_23_0, all_26_8, all_26_7) = v0) % 10.89/2.17 | | | | | % 10.89/2.17 | | | | | BETA: splitting (100) gives: % 10.89/2.17 | | | | | % 10.89/2.17 | | | | | Case 1: % 10.89/2.17 | | | | | | % 10.89/2.17 | | | | | | (101) all_80_0 = 0 % 10.89/2.17 | | | | | | % 10.89/2.17 | | | | | | REDUCE: (96), (101) imply: % 10.89/2.17 | | | | | | (102) $false % 10.89/2.17 | | | | | | % 10.89/2.17 | | | | | | CLOSE: (102) is inconsistent. % 10.89/2.17 | | | | | | % 10.89/2.17 | | | | | Case 2: % 10.89/2.17 | | | | | | % 10.89/2.17 | | | | | | (103) ? [v0: int] : ( ~ (v0 = 0) & pair_in_list(all_23_0, % 10.89/2.17 | | | | | | all_26_8, all_26_7) = v0) % 10.89/2.17 | | | | | | % 10.89/2.17 | | | | | | DELTA: instantiating (103) with fresh symbol all_102_0 gives: % 10.89/2.17 | | | | | | (104) ~ (all_102_0 = 0) & pair_in_list(all_23_0, all_26_8, % 10.89/2.17 | | | | | | all_26_7) = all_102_0 % 10.89/2.17 | | | | | | % 10.89/2.17 | | | | | | REF_CLOSE: (8), (50), (104) are inconsistent by sub-proof #1. % 10.89/2.17 | | | | | | % 10.89/2.17 | | | | | End of split % 10.89/2.17 | | | | | % 10.89/2.17 | | | | End of split % 10.89/2.17 | | | | % 10.89/2.17 | | | End of split % 10.89/2.17 | | | % 10.89/2.17 | | End of split % 10.89/2.17 | | % 10.89/2.17 | Case 2: % 10.89/2.17 | | % 10.89/2.17 | | (105) all_26_4 = all_26_7 & all_26_5 = all_26_8 % 10.89/2.17 | | % 10.89/2.17 | | ALPHA: (105) implies: % 10.89/2.17 | | (106) all_26_5 = all_26_8 % 10.89/2.17 | | (107) all_26_4 = all_26_7 % 10.89/2.17 | | % 10.89/2.17 | | REDUCE: (42), (106) imply: % 10.89/2.17 | | (108) pair(all_26_8, all_26_6) = all_38_1 % 10.89/2.17 | | % 10.89/2.17 | | REDUCE: (40), (107) imply: % 10.89/2.17 | | (109) strictly_less_than(all_26_7, all_26_6) = all_38_3 % 10.89/2.17 | | % 10.89/2.17 | | GROUND_INST: instantiating (6) with 0, all_38_3, all_26_6, all_26_7, % 10.89/2.17 | | simplifying with (20), (109) gives: % 10.89/2.17 | | (110) all_38_3 = 0 % 10.89/2.17 | | % 10.89/2.17 | | BETA: splitting (44) gives: % 10.89/2.17 | | % 10.89/2.17 | | Case 1: % 10.89/2.17 | | | % 10.89/2.17 | | | (111) ~ (all_38_3 = 0) % 10.89/2.17 | | | % 10.89/2.17 | | | REDUCE: (110), (111) imply: % 10.89/2.17 | | | (112) $false % 10.89/2.17 | | | % 10.89/2.17 | | | CLOSE: (112) is inconsistent. % 10.89/2.17 | | | % 10.89/2.17 | | Case 2: % 10.89/2.17 | | | % 10.89/2.17 | | | (113) all_38_0 = all_26_1 % 10.89/2.17 | | | % 10.89/2.17 | | | REDUCE: (46), (113) imply: % 10.89/2.17 | | | (114) insert_slb(all_36_1, all_38_1) = all_26_1 % 10.89/2.17 | | | % 10.89/2.17 | | | GROUND_INST: instantiating (4) with all_36_1, all_26_8, all_26_8, % 10.89/2.17 | | | all_26_6, all_26_6, all_38_1, all_26_1, all_26_0, simplifying % 10.89/2.17 | | | with (15), (17), (24), (47), (108), (114) gives: % 10.89/2.17 | | | (115) all_26_0 = 0 % 10.89/2.17 | | | % 10.89/2.17 | | | REDUCE: (14), (115) imply: % 10.89/2.17 | | | (116) $false % 10.89/2.17 | | | % 10.89/2.17 | | | CLOSE: (116) is inconsistent. % 10.89/2.17 | | | % 10.89/2.17 | | End of split % 10.89/2.17 | | % 10.89/2.17 | End of split % 10.89/2.17 | % 10.89/2.17 End of proof % 10.89/2.17 % 10.89/2.17 Sub-proof #1 shows that the following formulas are inconsistent: % 10.89/2.17 ---------------------------------------------------------------- % 10.89/2.17 (1) ~ (all_102_0 = 0) & pair_in_list(all_23_0, all_26_8, all_26_7) = % 10.89/2.17 all_102_0 % 10.89/2.18 (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 10.89/2.18 ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (pair_in_list(v4, v3, v2) = v1) % 10.89/2.18 | ~ (pair_in_list(v4, v3, v2) = v0)) % 10.89/2.18 (3) pair_in_list(all_23_0, all_26_8, all_26_7) = 0 % 10.89/2.18 % 10.89/2.18 Begin of proof % 10.89/2.18 | % 10.89/2.18 | ALPHA: (1) implies: % 10.89/2.18 | (4) ~ (all_102_0 = 0) % 10.89/2.18 | (5) pair_in_list(all_23_0, all_26_8, all_26_7) = all_102_0 % 10.89/2.18 | % 10.89/2.18 | GROUND_INST: instantiating (2) with 0, all_102_0, all_26_7, all_26_8, % 10.89/2.18 | all_23_0, simplifying with (3), (5) gives: % 10.89/2.18 | (6) all_102_0 = 0 % 10.89/2.18 | % 10.89/2.18 | REDUCE: (4), (6) imply: % 10.89/2.18 | (7) $false % 10.89/2.18 | % 10.89/2.18 | CLOSE: (7) is inconsistent. % 10.89/2.18 | % 10.89/2.18 End of proof % 10.89/2.18 % SZS output end Proof for theBenchmark % 10.89/2.18 % 10.89/2.18 1578ms %------------------------------------------------------------------------------