%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : LCL658+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 12:54:33 PM UTC 2026 % Result : Theorem 168.90s 22.17s % Output : Proof 170.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL658+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.10/0.37 % Computer : n003.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Sat Sep 5 08:01:50 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.38 OpenJDK 64-Bit Server VM warning: Options -Xverify:none and -noverify were deprecated in JDK 13 and will likely be removed in a future release. % 0.65/0.71 ________ _____ % 0.65/0.71 ___ __ \_________(_)________________________________ % 0.65/0.71 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.65/0.71 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.65/0.71 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.65/0.71 % 0.65/0.71 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.65/0.71 (2023-06-19) % 0.65/0.71 % 0.65/0.71 (c) Philipp Rümmer, 2009-2023 % 0.65/0.71 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.65/0.71 Amanda Stjerna. % 0.65/0.71 Free software under BSD-3-Clause. % 0.65/0.71 % 0.65/0.71 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.65/0.71 % 0.65/0.71 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.65/0.73 Running up to 7 provers in parallel. % 0.65/0.74 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.65/0.74 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.65/0.74 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.65/0.74 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.65/0.75 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.65/0.75 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.65/0.75 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 10.72/2.19 Prover 1: Preprocessing ... % 11.14/2.24 Prover 4: Preprocessing ... % 11.14/2.24 Prover 5: Preprocessing ... % 11.14/2.24 Prover 2: Preprocessing ... % 11.14/2.24 Prover 6: Preprocessing ... % 11.14/2.24 Prover 3: Preprocessing ... % 11.14/2.25 Prover 0: Preprocessing ... % 19.85/3.37 Prover 2: Proving ... % 22.30/3.69 Prover 5: Proving ... % 32.56/4.92 Prover 6: Proving ... % 33.57/5.06 Prover 3: Constructing countermodel ... % 33.57/5.08 Prover 1: Constructing countermodel ... % 33.57/5.12 Prover 0: Proving ... % 35.73/5.36 Prover 4: Constructing countermodel ... % 78.38/10.74 Prover 2: stopped % 78.38/10.74 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 81.89/11.15 Prover 7: Preprocessing ... % 82.35/11.26 Prover 7: Warning: ignoring some quantifiers % 82.35/11.29 Prover 7: Constructing countermodel ... % 105.07/14.07 Prover 5: stopped % 105.07/14.07 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 108.49/14.57 Prover 8: Preprocessing ... % 113.77/15.17 Prover 8: Warning: ignoring some quantifiers % 114.03/15.20 Prover 8: Constructing countermodel ... % 120.95/16.08 Prover 1: stopped % 120.95/16.09 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 122.76/16.35 Prover 9: Preprocessing ... % 128.61/17.13 Prover 9: Constructing countermodel ... % 135.51/17.99 Prover 6: stopped % 135.51/17.99 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 139.37/18.43 Prover 10: Preprocessing ... % 140.13/18.55 Prover 10: Warning: ignoring some quantifiers % 140.13/18.56 Prover 10: Constructing countermodel ... % 168.09/22.13 Prover 10: Found proof (size 50) % 168.90/22.14 Prover 10: proved (4141ms) % 168.90/22.14 Prover 8: stopped % 168.90/22.14 Prover 0: stopped % 168.90/22.14 Prover 9: stopped % 168.90/22.14 Prover 4: stopped % 168.90/22.15 Prover 7: stopped % 168.90/22.17 Prover 3: stopped % 168.90/22.17 % 168.90/22.17 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 168.90/22.17 % 168.90/22.17 % SZS output start Proof for theBenchmark % 168.90/22.18 Assumptions after simplification: % 168.90/22.18 --------------------------------- % 168.90/22.18 % 168.90/22.18 (main) % 169.18/22.27 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 169.18/22.27 $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : % 169.18/22.27 ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ($i(v13) & $i(v12) & $i(v11) & % 169.18/22.27 $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 169.18/22.27 $i(v2) & $i(v1) & $i(v0) & r1(v11, v13) & r1(v11, v12) & r1(v10, v11) & % 169.18/22.27 r1(v9, v10) & r1(v8, v9) & r1(v7, v8) & r1(v6, v7) & r1(v5, v6) & r1(v4, v5) % 169.18/22.27 & r1(v3, v4) & r1(v2, v3) & r1(v1, v2) & r1(v0, v1) & ~ p1(v13) & ! [v14: % 169.18/22.27 $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : ! [v19: % 169.18/22.27 $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! [v24: % 169.18/22.27 $i] : ! [v25: $i] : ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ! [v29: % 169.18/22.27 $i] : ! [v30: $i] : ! [v31: $i] : ! [v32: $i] : ! [v33: $i] : ! [v34: % 169.18/22.27 $i] : ( ~ $i(v34) | ~ $i(v33) | ~ $i(v32) | ~ $i(v31) | ~ $i(v30) | ~ % 169.18/22.27 $i(v29) | ~ $i(v28) | ~ $i(v27) | ~ $i(v26) | ~ $i(v25) | ~ $i(v24) | % 169.18/22.27 ~ $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ % 169.18/22.27 $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v33, % 169.18/22.27 v34) | ~ r1(v32, v33) | ~ r1(v31, v32) | ~ r1(v30, v31) | ~ r1(v29, % 169.18/22.27 v30) | ~ r1(v28, v29) | ~ r1(v27, v28) | ~ r1(v26, v27) | ~ r1(v25, % 169.18/22.27 v26) | ~ r1(v24, v25) | ~ r1(v23, v24) | ~ r1(v22, v23) | ~ r1(v21, % 169.18/22.27 v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ r1(v17, % 169.18/22.27 v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, % 169.18/22.27 v14) | p1(v34) | ? [v35: $i] : ($i(v35) & r1(v32, v35) & ~ p1(v35))) & % 169.18/22.27 ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : % 169.18/22.27 ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! % 169.18/22.27 [v24: $i] : ! [v25: $i] : ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ! % 169.18/22.27 [v29: $i] : ! [v30: $i] : ! [v31: $i] : ! [v32: $i] : ! [v33: $i] : ( ~ % 169.18/22.27 $i(v33) | ~ $i(v32) | ~ $i(v31) | ~ $i(v30) | ~ $i(v29) | ~ $i(v28) | % 169.18/22.27 ~ $i(v27) | ~ $i(v26) | ~ $i(v25) | ~ $i(v24) | ~ $i(v23) | ~ % 169.18/22.28 $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | % 169.18/22.28 ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v32, v33) | ~ r1(v31, v32) | % 169.18/22.28 ~ r1(v30, v31) | ~ r1(v29, v30) | ~ r1(v28, v29) | ~ r1(v27, v28) | ~ % 169.18/22.28 r1(v26, v27) | ~ r1(v25, v26) | ~ r1(v24, v25) | ~ r1(v23, v24) | ~ % 169.18/22.28 r1(v22, v23) | ~ r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ % 169.18/22.28 r1(v18, v19) | ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ % 169.18/22.28 r1(v14, v15) | ~ r1(v0, v14) | p1(v33) | ? [v34: $i] : ($i(v34) & % 169.18/22.28 r1(v31, v34) & ~ p1(v34))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] % 169.18/22.28 : ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : % 169.18/22.28 ! [v22: $i] : ! [v23: $i] : ! [v24: $i] : ! [v25: $i] : ! [v26: $i] : % 169.18/22.28 ! [v27: $i] : ! [v28: $i] : ! [v29: $i] : ! [v30: $i] : ! [v31: $i] : ! % 169.18/22.28 [v32: $i] : ( ~ $i(v32) | ~ $i(v31) | ~ $i(v30) | ~ $i(v29) | ~ $i(v28) % 169.18/22.28 | ~ $i(v27) | ~ $i(v26) | ~ $i(v25) | ~ $i(v24) | ~ $i(v23) | ~ % 169.18/22.28 $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | % 169.18/22.28 ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v31, v32) | ~ r1(v30, v31) | % 169.18/22.28 ~ r1(v29, v30) | ~ r1(v28, v29) | ~ r1(v27, v28) | ~ r1(v26, v27) | ~ % 169.18/22.28 r1(v25, v26) | ~ r1(v24, v25) | ~ r1(v23, v24) | ~ r1(v22, v23) | ~ % 169.18/22.28 r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ % 169.18/22.28 r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ % 169.18/22.28 r1(v0, v14) | p1(v32) | ? [v33: $i] : ($i(v33) & r1(v30, v33) & ~ % 169.18/22.28 p1(v33))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : % 169.18/22.28 ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! % 169.18/22.28 [v23: $i] : ! [v24: $i] : ! [v25: $i] : ! [v26: $i] : ! [v27: $i] : ! % 169.18/22.28 [v28: $i] : ! [v29: $i] : ! [v30: $i] : ! [v31: $i] : ( ~ $i(v31) | ~ % 169.18/22.28 $i(v30) | ~ $i(v29) | ~ $i(v28) | ~ $i(v27) | ~ $i(v26) | ~ $i(v25) | % 169.18/22.28 ~ $i(v24) | ~ $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ % 169.18/22.28 $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | % 169.18/22.28 ~ r1(v30, v31) | ~ r1(v29, v30) | ~ r1(v28, v29) | ~ r1(v27, v28) | ~ % 169.18/22.28 r1(v26, v27) | ~ r1(v25, v26) | ~ r1(v24, v25) | ~ r1(v23, v24) | ~ % 169.18/22.28 r1(v22, v23) | ~ r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ % 169.18/22.28 r1(v18, v19) | ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ % 169.18/22.28 r1(v14, v15) | ~ r1(v0, v14) | p1(v31) | ? [v32: $i] : ($i(v32) & % 169.18/22.28 r1(v29, v32) & ~ p1(v32))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] % 169.18/22.28 : ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : % 169.18/22.28 ! [v22: $i] : ! [v23: $i] : ! [v24: $i] : ! [v25: $i] : ! [v26: $i] : % 169.18/22.28 ! [v27: $i] : ! [v28: $i] : ! [v29: $i] : ! [v30: $i] : ( ~ $i(v30) | ~ % 169.18/22.28 $i(v29) | ~ $i(v28) | ~ $i(v27) | ~ $i(v26) | ~ $i(v25) | ~ $i(v24) | % 169.18/22.28 ~ $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ % 169.18/22.28 $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v29, % 169.18/22.28 v30) | ~ r1(v28, v29) | ~ r1(v27, v28) | ~ r1(v26, v27) | ~ r1(v25, % 169.18/22.28 v26) | ~ r1(v24, v25) | ~ r1(v23, v24) | ~ r1(v22, v23) | ~ r1(v21, % 169.18/22.28 v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ r1(v17, % 169.18/22.28 v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, % 169.18/22.28 v14) | p1(v30) | ? [v31: $i] : ($i(v31) & r1(v28, v31) & ~ p1(v31))) & % 169.18/22.28 ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : % 169.18/22.28 ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! % 169.18/22.28 [v24: $i] : ! [v25: $i] : ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ! % 169.18/22.28 [v29: $i] : ( ~ $i(v29) | ~ $i(v28) | ~ $i(v27) | ~ $i(v26) | ~ $i(v25) % 169.18/22.28 | ~ $i(v24) | ~ $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ % 169.18/22.28 $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | % 169.18/22.28 ~ r1(v28, v29) | ~ r1(v27, v28) | ~ r1(v26, v27) | ~ r1(v25, v26) | ~ % 169.18/22.28 r1(v24, v25) | ~ r1(v23, v24) | ~ r1(v22, v23) | ~ r1(v21, v22) | ~ % 169.18/22.28 r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ r1(v17, v18) | ~ % 169.18/22.28 r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, v14) | % 169.18/22.28 p1(v29) | ? [v30: $i] : ($i(v30) & r1(v27, v30) & ~ p1(v30))) & ! [v14: % 169.18/22.28 $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : ! [v19: % 169.18/22.28 $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! [v24: % 169.18/22.28 $i] : ! [v25: $i] : ! [v26: $i] : ! [v27: $i] : ! [v28: $i] : ( ~ % 169.18/22.28 $i(v28) | ~ $i(v27) | ~ $i(v26) | ~ $i(v25) | ~ $i(v24) | ~ $i(v23) | % 169.18/22.28 ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ % 169.18/22.28 $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v27, v28) | ~ % 169.18/22.28 r1(v26, v27) | ~ r1(v25, v26) | ~ r1(v24, v25) | ~ r1(v23, v24) | ~ % 169.18/22.28 r1(v22, v23) | ~ r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ % 169.18/22.28 r1(v18, v19) | ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ % 169.18/22.28 r1(v14, v15) | ~ r1(v0, v14) | p1(v28) | ? [v29: $i] : ($i(v29) & % 169.18/22.28 r1(v26, v29) & ~ p1(v29))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] % 169.18/22.28 : ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : % 169.18/22.28 ! [v22: $i] : ! [v23: $i] : ! [v24: $i] : ! [v25: $i] : ! [v26: $i] : % 169.18/22.28 ! [v27: $i] : ( ~ $i(v27) | ~ $i(v26) | ~ $i(v25) | ~ $i(v24) | ~ % 169.18/22.28 $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | % 169.18/22.28 ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v26, v27) | ~ % 169.18/22.28 r1(v25, v26) | ~ r1(v24, v25) | ~ r1(v23, v24) | ~ r1(v22, v23) | ~ % 169.18/22.28 r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ % 169.18/22.28 r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ % 169.18/22.29 r1(v0, v14) | p1(v27) | ? [v28: $i] : ($i(v28) & r1(v25, v28) & ~ % 169.18/22.29 p1(v28))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : % 169.18/22.29 ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! % 169.18/22.29 [v23: $i] : ! [v24: $i] : ! [v25: $i] : ! [v26: $i] : ( ~ $i(v26) | ~ % 169.18/22.29 $i(v25) | ~ $i(v24) | ~ $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | % 169.18/22.29 ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ % 169.18/22.29 $i(v14) | ~ p1(v24) | ~ r1(v24, v26) | ~ r1(v24, v25) | ~ r1(v23, v24) % 169.18/22.29 | ~ r1(v22, v23) | ~ r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | % 169.18/22.29 ~ r1(v18, v19) | ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ % 169.18/22.29 r1(v14, v15) | ~ r1(v0, v14) | p1(v26) | ? [v27: $i] : ? [v28: $i] : % 169.18/22.29 ($i(v28) & $i(v27) & ((p1(v27) & r1(v27, v28) & r1(v25, v27) & ~ p1(v28)) % 169.18/22.29 | (p1(v27) & r1(v27, v28) & r1(v24, v27) & ~ p1(v28) & ! [v29: $i] : % 169.18/22.29 ! [v30: $i] : ! [v31: $i] : ( ~ $i(v31) | ~ $i(v30) | ~ $i(v29) % 169.18/22.29 | ~ p1(v30) | ~ r1(v30, v31) | ~ r1(v29, v30) | ~ r1(v27, v29) % 169.18/22.29 | p1(v31) | p1(v29)) & ! [v29: $i] : ! [v30: $i] : ! [v31: $i] % 169.18/22.29 : ( ~ $i(v31) | ~ $i(v30) | ~ $i(v29) | ~ p1(v30) | ~ r1(v30, % 169.18/22.29 v31) | ~ r1(v29, v30) | ~ r1(v27, v29) | p1(v31) | ? [v32: % 169.18/22.29 $i] : ($i(v32) & r1(v29, v32) & ~ p1(v32))))))) & ! [v14: $i] % 169.18/22.29 : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : % 169.18/22.29 ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! [v24: $i] : % 169.18/22.29 ! [v25: $i] : ! [v26: $i] : ( ~ $i(v26) | ~ $i(v25) | ~ $i(v24) | ~ % 169.18/22.29 $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | % 169.18/22.29 ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v25, v26) | ~ % 169.18/22.29 r1(v24, v25) | ~ r1(v23, v24) | ~ r1(v22, v23) | ~ r1(v21, v22) | ~ % 169.18/22.29 r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ r1(v17, v18) | ~ % 169.18/22.29 r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, v14) | % 169.18/22.29 p1(v26) | ? [v27: $i] : ? [v28: $i] : ($i(v28) & $i(v27) & ((p1(v27) & % 169.18/22.29 r1(v27, v28) & r1(v26, v27) & ~ p1(v28)) | (r1(v24, v27) & ~ % 169.18/22.29 p1(v27) & ! [v29: $i] : ! [v30: $i] : ( ~ $i(v30) | ~ $i(v29) | % 169.18/22.29 ~ p1(v29) | ~ r1(v29, v30) | ~ r1(v27, v29) | p1(v30)))))) & ! % 169.18/22.29 [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : ! % 169.18/22.29 [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! [v23: $i] : ! % 169.18/22.29 [v24: $i] : ! [v25: $i] : ( ~ $i(v25) | ~ $i(v24) | ~ $i(v23) | ~ % 169.18/22.29 $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | % 169.18/22.29 ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v24, v25) | ~ r1(v23, v24) | % 169.18/22.29 ~ r1(v22, v23) | ~ r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ % 169.18/22.29 r1(v18, v19) | ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ % 169.18/22.29 r1(v14, v15) | ~ r1(v0, v14) | p1(v25) | ? [v26: $i] : ($i(v26) & % 169.18/22.29 r1(v23, v26) & ~ p1(v26))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] % 169.18/22.29 : ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : % 169.18/22.29 ! [v22: $i] : ! [v23: $i] : ! [v24: $i] : ! [v25: $i] : ( ~ $i(v25) | ~ % 169.18/22.29 $i(v24) | ~ $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | % 169.18/22.29 ~ $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ % 169.18/22.29 r1(v24, v25) | ~ r1(v23, v24) | ~ r1(v22, v23) | ~ r1(v21, v22) | ~ % 169.18/22.29 r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ r1(v17, v18) | ~ % 169.18/22.29 r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, v14) | % 169.18/22.29 p1(v24) | ? [v26: $i] : ($i(v26) & ((r1(v25, v26) & ~ p1(v26)) | % 169.18/22.29 (r1(v24, v26) & ~ p1(v26) & ! [v27: $i] : ! [v28: $i] : ( ~ $i(v28) % 169.18/22.29 | ~ $i(v27) | ~ p1(v27) | ~ r1(v27, v28) | ~ r1(v26, v27) | % 169.18/22.29 p1(v28)))))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! % 169.18/22.29 [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! % 169.18/22.29 [v22: $i] : ! [v23: $i] : ! [v24: $i] : ( ~ $i(v24) | ~ $i(v23) | ~ % 169.18/22.29 $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | % 169.18/22.29 ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v23, v24) | ~ r1(v22, v23) | % 169.18/22.29 ~ r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ % 169.18/22.29 r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ % 169.18/22.29 r1(v0, v14) | p1(v24) | ? [v25: $i] : ($i(v25) & r1(v22, v25) & ~ % 169.18/22.29 p1(v25))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : % 169.18/22.29 ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ! [v22: $i] : ! % 169.18/22.29 [v23: $i] : ( ~ $i(v23) | ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) % 169.18/22.29 | ~ $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ % 169.18/22.29 r1(v22, v23) | ~ r1(v21, v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ % 169.18/22.29 r1(v18, v19) | ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ % 169.18/22.29 r1(v14, v15) | ~ r1(v0, v14) | p1(v23) | ? [v24: $i] : ($i(v24) & % 169.18/22.29 r1(v21, v24) & ~ p1(v24))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] % 169.18/22.29 : ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : % 169.18/22.29 ! [v22: $i] : ( ~ $i(v22) | ~ $i(v21) | ~ $i(v20) | ~ $i(v19) | ~ % 169.18/22.29 $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v21, % 169.18/22.29 v22) | ~ r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ r1(v17, % 169.18/22.29 v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, % 169.18/22.29 v14) | p1(v22) | ? [v23: $i] : ($i(v23) & r1(v20, v23) & ~ p1(v23))) & % 169.18/22.29 ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : % 169.18/22.29 ! [v19: $i] : ! [v20: $i] : ! [v21: $i] : ( ~ $i(v21) | ~ $i(v20) | ~ % 169.18/22.29 $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | % 169.18/22.29 ~ r1(v20, v21) | ~ r1(v19, v20) | ~ r1(v18, v19) | ~ r1(v17, v18) | ~ % 169.18/22.29 r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, v14) | % 169.18/22.30 p1(v21) | ? [v22: $i] : ($i(v22) & r1(v19, v22) & ~ p1(v22))) & ! [v14: % 169.18/22.30 $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : ! [v19: % 169.18/22.30 $i] : ! [v20: $i] : ( ~ $i(v20) | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | % 169.18/22.30 ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v19, v20) | ~ r1(v18, v19) | % 169.18/22.30 ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ % 169.18/22.30 r1(v0, v14) | p1(v20) | ? [v21: $i] : ($i(v21) & r1(v18, v21) & ~ % 169.18/22.30 p1(v21))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : % 169.18/22.30 ! [v18: $i] : ! [v19: $i] : ( ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ % 169.18/22.30 $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v18, v19) | ~ r1(v17, v18) | ~ % 169.18/22.30 r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, v14) | % 169.18/22.30 p1(v19) | ? [v20: $i] : ($i(v20) & r1(v17, v20) & ~ p1(v20))) & ! [v14: % 169.18/22.30 $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : ( ~ % 169.18/22.30 $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v17, % 169.68/22.30 v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v0, % 169.68/22.30 v14) | p1(v18) | ? [v19: $i] : ($i(v19) & r1(v16, v19) & ~ p1(v19))) & % 169.68/22.30 ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ( ~ $i(v17) | ~ % 169.68/22.30 $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ % 169.68/22.30 r1(v14, v15) | ~ r1(v0, v14) | p1(v17) | ? [v18: $i] : ($i(v18) & % 169.68/22.30 r1(v15, v18) & ~ p1(v18))) & ! [v14: $i] : ! [v15: $i] : ! [v16: $i] % 169.68/22.30 : ( ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ r1(v15, v16) | ~ r1(v14, v15) % 169.68/22.30 | ~ r1(v0, v14) | p1(v16) | ? [v17: $i] : ($i(v17) & r1(v14, v17) & ~ % 169.68/22.30 p1(v17))) & ! [v14: $i] : ( ~ $i(v14) | ~ r1(v12, v14) | p1(v14)) & ! % 169.68/22.30 [v14: $i] : ( ~ $i(v14) | ~ r1(v11, v14) | p1(v14) | ? [v15: $i] : ? % 169.68/22.30 [v16: $i] : ($i(v16) & $i(v15) & p1(v15) & r1(v15, v16) & r1(v14, v15) & % 169.68/22.30 ~ p1(v16)))) % 169.68/22.30 % 169.68/22.30 Further assumptions not needed in the proof: % 169.68/22.30 -------------------------------------------- % 169.68/22.30 reflexivity % 169.68/22.30 % 169.68/22.30 Those formulas are unsatisfiable: % 169.68/22.30 --------------------------------- % 169.68/22.30 % 169.68/22.30 Begin of proof % 169.68/22.30 | % 169.68/22.30 | DELTA: instantiating (main) with fresh symbols all_3_0, all_3_1, all_3_2, % 169.68/22.30 | all_3_3, all_3_4, all_3_5, all_3_6, all_3_7, all_3_8, all_3_9, % 169.68/22.30 | all_3_10, all_3_11, all_3_12, all_3_13 gives: % 169.68/22.35 | (1) $i(all_3_0) & $i(all_3_1) & $i(all_3_2) & $i(all_3_3) & $i(all_3_4) & % 169.68/22.35 | $i(all_3_5) & $i(all_3_6) & $i(all_3_7) & $i(all_3_8) & $i(all_3_9) & % 169.68/22.35 | $i(all_3_10) & $i(all_3_11) & $i(all_3_12) & $i(all_3_13) & r1(all_3_2, % 169.68/22.35 | all_3_0) & r1(all_3_2, all_3_1) & r1(all_3_3, all_3_2) & r1(all_3_4, % 169.68/22.35 | all_3_3) & r1(all_3_5, all_3_4) & r1(all_3_6, all_3_5) & r1(all_3_7, % 169.68/22.35 | all_3_6) & r1(all_3_8, all_3_7) & r1(all_3_9, all_3_8) & r1(all_3_10, % 169.68/22.35 | all_3_9) & r1(all_3_11, all_3_10) & r1(all_3_12, all_3_11) & % 169.68/22.35 | r1(all_3_13, all_3_12) & ~ p1(all_3_0) & ! [v0: $i] : ! [v1: $i] : % 169.68/22.35 | ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! % 169.68/22.35 | [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! % 169.68/22.35 | [v12: $i] : ! [v13: $i] : ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : % 169.68/22.35 | ! [v17: $i] : ! [v18: $i] : ! [v19: $i] : ! [v20: $i] : ( ~ $i(v20) % 169.68/22.35 | | ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ % 169.68/22.35 | $i(v14) | ~ $i(v13) | ~ $i(v12) | ~ $i(v11) | ~ $i(v10) | ~ % 169.68/22.35 | $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | % 169.68/22.35 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v19, v20) | ~ % 169.68/22.35 | r1(v18, v19) | ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | % 169.68/22.35 | ~ r1(v14, v15) | ~ r1(v13, v14) | ~ r1(v12, v13) | ~ r1(v11, v12) % 169.68/22.35 | | ~ r1(v10, v11) | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ r1(v7, v8) | % 169.68/22.35 | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ % 169.68/22.35 | r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | % 169.68/22.35 | p1(v20) | ? [v21: $i] : ($i(v21) & r1(v18, v21) & ~ p1(v21))) & ! % 169.68/22.35 | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 169.68/22.35 | [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! % 169.68/22.35 | [v10: $i] : ! [v11: $i] : ! [v12: $i] : ! [v13: $i] : ! [v14: $i] : % 169.68/22.35 | ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : ! [v19: % 169.68/22.35 | $i] : ( ~ $i(v19) | ~ $i(v18) | ~ $i(v17) | ~ $i(v16) | ~ $i(v15) % 169.68/22.35 | | ~ $i(v14) | ~ $i(v13) | ~ $i(v12) | ~ $i(v11) | ~ $i(v10) | ~ % 169.68/22.35 | $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | % 169.68/22.35 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v18, v19) | ~ % 169.68/22.35 | r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | % 169.68/22.35 | ~ r1(v13, v14) | ~ r1(v12, v13) | ~ r1(v11, v12) | ~ r1(v10, v11) % 169.68/22.35 | | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ % 169.68/22.35 | r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ % 169.68/22.35 | r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v19) | ? [v20: % 169.68/22.35 | $i] : ($i(v20) & r1(v17, v20) & ~ p1(v20))) & ! [v0: $i] : ! % 169.68/22.35 | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! % 169.68/22.35 | [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! % 169.68/22.35 | [v11: $i] : ! [v12: $i] : ! [v13: $i] : ! [v14: $i] : ! [v15: $i] : % 169.68/22.35 | ! [v16: $i] : ! [v17: $i] : ! [v18: $i] : ( ~ $i(v18) | ~ $i(v17) | % 169.68/22.35 | ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ $i(v13) | ~ $i(v12) | ~ % 169.68/22.35 | $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) % 169.68/22.35 | | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 169.68/22.35 | $i(v0) | ~ r1(v17, v18) | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ % 169.68/22.35 | r1(v14, v15) | ~ r1(v13, v14) | ~ r1(v12, v13) | ~ r1(v11, v12) | % 169.68/22.35 | ~ r1(v10, v11) | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ % 169.68/22.35 | r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ % 169.68/22.35 | r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | % 169.68/22.35 | p1(v18) | ? [v19: $i] : ($i(v19) & r1(v16, v19) & ~ p1(v19))) & ! % 169.68/22.35 | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 169.68/22.35 | [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! % 169.68/22.35 | [v10: $i] : ! [v11: $i] : ! [v12: $i] : ! [v13: $i] : ! [v14: $i] : % 169.68/22.35 | ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ( ~ $i(v17) | ~ $i(v16) | % 169.68/22.35 | ~ $i(v15) | ~ $i(v14) | ~ $i(v13) | ~ $i(v12) | ~ $i(v11) | ~ % 169.68/22.35 | $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | % 169.68/22.35 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 169.68/22.35 | r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v13, v14) | % 169.68/22.35 | ~ r1(v12, v13) | ~ r1(v11, v12) | ~ r1(v10, v11) | ~ r1(v9, v10) | % 169.68/22.35 | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ % 169.68/22.35 | r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ % 169.68/22.35 | r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v17) | ? [v18: $i] : ($i(v18) % 169.68/22.35 | & r1(v15, v18) & ~ p1(v18))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 169.68/22.35 | $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: % 169.68/22.35 | $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! % 169.68/22.35 | [v12: $i] : ! [v13: $i] : ! [v14: $i] : ! [v15: $i] : ! [v16: $i] : % 169.68/22.35 | ( ~ $i(v16) | ~ $i(v15) | ~ $i(v14) | ~ $i(v13) | ~ $i(v12) | ~ % 169.68/22.35 | $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) % 169.68/22.35 | | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 169.68/22.35 | $i(v0) | ~ r1(v15, v16) | ~ r1(v14, v15) | ~ r1(v13, v14) | ~ % 169.68/22.35 | r1(v12, v13) | ~ r1(v11, v12) | ~ r1(v10, v11) | ~ r1(v9, v10) | % 169.68/22.35 | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ % 169.68/22.35 | r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ % 169.68/22.35 | r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v16) | ? [v17: $i] : ($i(v17) % 169.68/22.35 | & r1(v14, v17) & ~ p1(v17))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 169.68/22.35 | $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: % 169.68/22.35 | $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! % 169.68/22.35 | [v12: $i] : ! [v13: $i] : ! [v14: $i] : ! [v15: $i] : ( ~ $i(v15) | % 169.68/22.35 | ~ $i(v14) | ~ $i(v13) | ~ $i(v12) | ~ $i(v11) | ~ $i(v10) | ~ % 169.68/22.35 | $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | % 169.68/22.35 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v14, v15) | ~ % 169.68/22.35 | r1(v13, v14) | ~ r1(v12, v13) | ~ r1(v11, v12) | ~ r1(v10, v11) | % 169.68/22.35 | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ % 169.68/22.35 | r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ % 169.68/22.35 | r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v15) | ? [v16: % 169.68/22.35 | $i] : ($i(v16) & r1(v13, v16) & ~ p1(v16))) & ! [v0: $i] : ! % 169.68/22.35 | [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! % 169.68/22.35 | [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! % 169.68/22.35 | [v11: $i] : ! [v12: $i] : ! [v13: $i] : ! [v14: $i] : ( ~ $i(v14) | % 169.68/22.35 | ~ $i(v13) | ~ $i(v12) | ~ $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ % 169.68/22.35 | $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | % 169.68/22.35 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v13, v14) | ~ r1(v12, v13) % 169.68/22.35 | | ~ r1(v11, v12) | ~ r1(v10, v11) | ~ r1(v9, v10) | ~ r1(v8, v9) % 169.68/22.35 | | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ % 169.68/22.35 | r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 169.68/22.35 | r1(all_3_13, v0) | p1(v14) | ? [v15: $i] : ($i(v15) & r1(v12, v15) & % 169.68/22.35 | ~ p1(v15))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 169.68/22.35 | $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: % 169.68/22.35 | $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : ! % 169.68/22.35 | [v13: $i] : ( ~ $i(v13) | ~ $i(v12) | ~ $i(v11) | ~ $i(v10) | ~ % 169.68/22.35 | $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | % 169.68/22.35 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v12, v13) | ~ % 169.68/22.35 | r1(v11, v12) | ~ r1(v10, v11) | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ % 169.68/22.35 | r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ % 169.68/22.35 | r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 169.68/22.35 | r1(all_3_13, v0) | p1(v13) | ? [v14: $i] : ($i(v14) & r1(v11, v14) & % 169.68/22.35 | ~ p1(v14))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 169.68/22.35 | $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: % 169.68/22.35 | $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : ( ~ % 169.68/22.35 | $i(v12) | ~ $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) % 169.68/22.35 | | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 169.68/22.35 | $i(v1) | ~ $i(v0) | ~ p1(v10) | ~ r1(v10, v12) | ~ r1(v10, v11) | % 169.68/22.35 | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ % 169.68/22.35 | r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ % 169.68/22.35 | r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v12) | ? [v13: % 169.68/22.35 | $i] : ? [v14: $i] : ($i(v14) & $i(v13) & ((p1(v13) & r1(v13, v14) % 169.68/22.36 | & r1(v11, v13) & ~ p1(v14)) | (p1(v13) & r1(v13, v14) & % 169.68/22.36 | r1(v10, v13) & ~ p1(v14) & ! [v15: $i] : ! [v16: $i] : ! % 169.68/22.36 | [v17: $i] : ( ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ p1(v16) % 169.68/22.36 | | ~ r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v13, v15) | % 169.68/22.36 | p1(v17) | p1(v15)) & ! [v15: $i] : ! [v16: $i] : ! [v17: % 169.68/22.36 | $i] : ( ~ $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ p1(v16) | ~ % 169.68/22.36 | r1(v16, v17) | ~ r1(v15, v16) | ~ r1(v13, v15) | p1(v17) | % 169.68/22.36 | ? [v18: $i] : ($i(v18) & r1(v15, v18) & ~ p1(v18))))))) & ! % 169.68/22.36 | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 169.68/22.36 | [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! % 169.68/22.36 | [v10: $i] : ! [v11: $i] : ! [v12: $i] : ( ~ $i(v12) | ~ $i(v11) | ~ % 169.68/22.36 | $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | % 169.68/22.36 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 169.68/22.36 | r1(v11, v12) | ~ r1(v10, v11) | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ % 169.68/22.36 | r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ % 169.68/22.36 | r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 169.68/22.36 | r1(all_3_13, v0) | p1(v12) | ? [v13: $i] : ? [v14: $i] : ($i(v14) & % 169.68/22.36 | $i(v13) & ((p1(v13) & r1(v13, v14) & r1(v12, v13) & ~ p1(v14)) | % 169.68/22.36 | (r1(v10, v13) & ~ p1(v13) & ! [v15: $i] : ! [v16: $i] : ( ~ % 169.68/22.36 | $i(v16) | ~ $i(v15) | ~ p1(v15) | ~ r1(v15, v16) | ~ % 169.68/22.36 | r1(v13, v15) | p1(v16)))))) & ! [v0: $i] : ! [v1: $i] : ! % 169.68/22.36 | [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! % 169.68/22.36 | [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ( % 169.68/22.36 | ~ $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ % 169.68/22.36 | $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 169.68/22.36 | ~ $i(v0) | ~ r1(v10, v11) | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ % 169.68/22.36 | r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ % 169.68/22.36 | r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 169.68/22.36 | r1(all_3_13, v0) | p1(v11) | ? [v12: $i] : ($i(v12) & r1(v9, v12) & % 169.68/22.36 | ~ p1(v12))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 169.68/22.36 | : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : % 169.68/22.36 | ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ( ~ $i(v11) | ~ $i(v10) | % 169.68/22.36 | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) % 169.68/22.36 | | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v10, v11) | % 169.68/22.36 | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ % 169.68/22.36 | r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ % 169.68/22.36 | r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v10) | ? [v12: % 169.68/22.36 | $i] : ($i(v12) & ((r1(v11, v12) & ~ p1(v12)) | (r1(v10, v12) & ~ % 169.68/22.36 | p1(v12) & ! [v13: $i] : ! [v14: $i] : ( ~ $i(v14) | ~ % 169.68/22.36 | $i(v13) | ~ p1(v13) | ~ r1(v13, v14) | ~ r1(v12, v13) | % 169.68/22.36 | p1(v14)))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 169.68/22.36 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! % 169.68/22.36 | [v8: $i] : ! [v9: $i] : ! [v10: $i] : ( ~ $i(v10) | ~ $i(v9) | ~ % 169.68/22.36 | $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | % 169.68/22.36 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v9, v10) | ~ r1(v8, v9) | % 169.68/22.36 | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ % 169.68/22.36 | r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 169.68/22.36 | r1(all_3_13, v0) | p1(v10) | ? [v11: $i] : ($i(v11) & r1(v8, v11) & % 169.68/22.36 | ~ p1(v11))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 169.68/22.36 | : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : % 169.68/22.36 | ! [v9: $i] : ( ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ % 169.68/22.36 | $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 169.68/22.36 | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ % 169.68/22.36 | r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ % 169.68/22.36 | r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v9) | ? [v10: $i] : ($i(v10) & % 169.68/22.36 | r1(v7, v10) & ~ p1(v10))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 169.68/22.36 | $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: % 169.68/22.36 | $i] : ! [v8: $i] : ( ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | % 169.68/22.36 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v7, % 169.68/22.36 | v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) % 169.68/22.36 | | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) % 169.68/22.36 | | p1(v8) | ? [v9: $i] : ($i(v9) & r1(v6, v9) & ~ p1(v9))) & ! [v0: % 169.68/22.36 | $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 169.68/22.36 | $i] : ! [v6: $i] : ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) % 169.68/22.36 | | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 169.68/22.36 | r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ % 169.68/22.36 | r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | % 169.68/22.36 | p1(v7) | ? [v8: $i] : ($i(v8) & r1(v5, v8) & ~ p1(v8))) & ! [v0: % 169.68/22.36 | $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 169.68/22.36 | $i] : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | % 169.68/22.36 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ % 169.68/22.36 | r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 169.68/22.36 | r1(all_3_13, v0) | p1(v6) | ? [v7: $i] : ($i(v7) & r1(v4, v7) & ~ % 169.68/22.36 | p1(v7))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 169.68/22.36 | ! [v4: $i] : ! [v5: $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 169.68/22.36 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ % 169.68/22.36 | r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | % 169.68/22.36 | p1(v5) | ? [v6: $i] : ($i(v6) & r1(v3, v6) & ~ p1(v6))) & ! [v0: % 169.68/22.36 | $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 169.68/22.36 | $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v3, % 169.68/22.36 | v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 169.68/22.36 | r1(all_3_13, v0) | p1(v4) | ? [v5: $i] : ($i(v5) & r1(v2, v5) & ~ % 169.68/22.36 | p1(v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 169.68/22.36 | ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v2, v3) | ~ % 169.68/22.36 | r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v3) | ? [v4: % 169.68/22.36 | $i] : ($i(v4) & r1(v1, v4) & ~ p1(v4))) & ! [v0: $i] : ! [v1: % 169.68/22.36 | $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v1, % 169.68/22.36 | v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v2) | ? [v3: $i] : % 169.68/22.36 | ($i(v3) & r1(v0, v3) & ~ p1(v3))) & ! [v0: $i] : ( ~ $i(v0) | ~ % 169.68/22.36 | r1(all_3_1, v0) | p1(v0)) & ! [v0: $i] : ( ~ $i(v0) | ~ r1(all_3_2, % 169.68/22.36 | v0) | p1(v0) | ? [v1: $i] : ? [v2: $i] : ($i(v2) & $i(v1) & % 169.68/22.36 | p1(v1) & r1(v1, v2) & r1(v0, v1) & ~ p1(v2))) % 169.68/22.36 | % 169.68/22.36 | ALPHA: (1) implies: % 169.68/22.37 | (2) ~ p1(all_3_0) % 169.68/22.37 | (3) r1(all_3_13, all_3_12) % 169.68/22.37 | (4) r1(all_3_12, all_3_11) % 169.68/22.37 | (5) r1(all_3_11, all_3_10) % 169.68/22.37 | (6) r1(all_3_10, all_3_9) % 169.68/22.37 | (7) r1(all_3_9, all_3_8) % 169.68/22.37 | (8) r1(all_3_8, all_3_7) % 169.68/22.37 | (9) r1(all_3_7, all_3_6) % 169.68/22.37 | (10) r1(all_3_6, all_3_5) % 169.68/22.37 | (11) r1(all_3_5, all_3_4) % 169.68/22.37 | (12) r1(all_3_4, all_3_3) % 169.68/22.37 | (13) r1(all_3_3, all_3_2) % 169.68/22.37 | (14) r1(all_3_2, all_3_1) % 169.68/22.37 | (15) r1(all_3_2, all_3_0) % 169.68/22.37 | (16) $i(all_3_12) % 169.68/22.37 | (17) $i(all_3_11) % 169.68/22.37 | (18) $i(all_3_10) % 169.68/22.37 | (19) $i(all_3_9) % 169.68/22.37 | (20) $i(all_3_8) % 169.68/22.37 | (21) $i(all_3_7) % 169.68/22.37 | (22) $i(all_3_6) % 169.68/22.37 | (23) $i(all_3_5) % 169.68/22.37 | (24) $i(all_3_4) % 169.68/22.37 | (25) $i(all_3_3) % 169.68/22.37 | (26) $i(all_3_2) % 169.68/22.37 | (27) $i(all_3_1) % 169.68/22.37 | (28) $i(all_3_0) % 169.68/22.37 | (29) ! [v0: $i] : ( ~ $i(v0) | ~ r1(all_3_2, v0) | p1(v0) | ? [v1: $i] : % 169.68/22.37 | ? [v2: $i] : ($i(v2) & $i(v1) & p1(v1) & r1(v1, v2) & r1(v0, v1) & % 169.68/22.37 | ~ p1(v2))) % 169.68/22.37 | (30) ! [v0: $i] : ( ~ $i(v0) | ~ r1(all_3_1, v0) | p1(v0)) % 169.68/22.37 | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 169.68/22.37 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : % 169.68/22.37 | ! [v10: $i] : ! [v11: $i] : ( ~ $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ % 169.68/22.37 | $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | % 169.68/22.37 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ r1(v10, v11) | ~ r1(v9, v10) % 169.68/22.37 | | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ % 169.68/22.37 | r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ % 169.68/22.37 | r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v10) | ? [v12: $i] : ($i(v12) % 169.68/22.37 | & ((r1(v11, v12) & ~ p1(v12)) | (r1(v10, v12) & ~ p1(v12) & ! % 169.68/22.37 | [v13: $i] : ! [v14: $i] : ( ~ $i(v14) | ~ $i(v13) | ~ % 169.68/22.37 | p1(v13) | ~ r1(v13, v14) | ~ r1(v12, v13) | p1(v14)))))) % 169.68/22.38 | (32) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 169.68/22.38 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : % 169.68/22.38 | ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : ( ~ $i(v12) | ~ $i(v11) | % 169.68/22.38 | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ % 169.68/22.38 | $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 169.68/22.38 | ~ r1(v11, v12) | ~ r1(v10, v11) | ~ r1(v9, v10) | ~ r1(v8, v9) | % 169.68/22.38 | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ % 169.68/22.38 | r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 169.68/22.38 | r1(all_3_13, v0) | p1(v12) | ? [v13: $i] : ? [v14: $i] : ($i(v14) % 169.68/22.38 | & $i(v13) & ((p1(v13) & r1(v13, v14) & r1(v12, v13) & ~ p1(v14)) % 169.68/22.38 | | (r1(v10, v13) & ~ p1(v13) & ! [v15: $i] : ! [v16: $i] : ( ~ % 169.68/22.38 | $i(v16) | ~ $i(v15) | ~ p1(v15) | ~ r1(v15, v16) | ~ % 169.68/22.38 | r1(v13, v15) | p1(v16)))))) % 169.68/22.38 | (33) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 169.68/22.38 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : % 169.68/22.38 | ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : ( ~ $i(v12) | ~ $i(v11) | % 169.68/22.38 | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | ~ % 169.68/22.38 | $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 169.68/22.38 | ~ p1(v10) | ~ r1(v10, v12) | ~ r1(v10, v11) | ~ r1(v9, v10) | ~ % 169.68/22.38 | r1(v8, v9) | ~ r1(v7, v8) | ~ r1(v6, v7) | ~ r1(v5, v6) | ~ % 169.68/22.38 | r1(v4, v5) | ~ r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v1, v2) | ~ % 169.68/22.38 | r1(v0, v1) | ~ r1(all_3_13, v0) | p1(v12) | ? [v13: $i] : ? [v14: % 169.68/22.38 | $i] : ($i(v14) & $i(v13) & ((p1(v13) & r1(v13, v14) & r1(v11, v13) % 169.68/22.38 | & ~ p1(v14)) | (p1(v13) & r1(v13, v14) & r1(v10, v13) & ~ % 169.68/22.38 | p1(v14) & ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ( ~ % 169.68/22.38 | $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ p1(v16) | ~ r1(v16, % 169.68/22.38 | v17) | ~ r1(v15, v16) | ~ r1(v13, v15) | p1(v17) | % 169.68/22.38 | p1(v15)) & ! [v15: $i] : ! [v16: $i] : ! [v17: $i] : ( ~ % 169.68/22.38 | $i(v17) | ~ $i(v16) | ~ $i(v15) | ~ p1(v16) | ~ r1(v16, % 169.68/22.38 | v17) | ~ r1(v15, v16) | ~ r1(v13, v15) | p1(v17) | ? % 169.68/22.38 | [v18: $i] : ($i(v18) & r1(v15, v18) & ~ p1(v18))))))) % 169.68/22.39 | (34) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 169.68/22.39 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : % 169.68/22.39 | ! [v10: $i] : ! [v11: $i] : ! [v12: $i] : ! [v13: $i] : ( ~ $i(v13) % 169.68/22.39 | | ~ $i(v12) | ~ $i(v11) | ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ % 169.68/22.39 | $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 169.68/22.39 | ~ $i(v1) | ~ $i(v0) | ~ r1(v12, v13) | ~ r1(v11, v12) | ~ % 169.68/22.39 | r1(v10, v11) | ~ r1(v9, v10) | ~ r1(v8, v9) | ~ r1(v7, v8) | ~ % 169.68/22.39 | r1(v6, v7) | ~ r1(v5, v6) | ~ r1(v4, v5) | ~ r1(v3, v4) | ~ % 169.68/22.39 | r1(v2, v3) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_3_13, v0) | % 169.68/22.39 | p1(v13) | ? [v14: $i] : ($i(v14) & r1(v11, v14) & ~ p1(v14))) % 169.68/22.39 | % 169.68/22.39 | GROUND_INST: instantiating (31) with all_3_12, all_3_11, all_3_10, all_3_9, % 169.68/22.39 | all_3_8, all_3_7, all_3_6, all_3_5, all_3_4, all_3_3, all_3_2, % 169.68/22.39 | all_3_1, simplifying with (3), (4), (5), (6), (7), (8), (9), % 169.68/22.39 | (10), (11), (12), (13), (14), (16), (17), (18), (19), (20), (21), % 169.68/22.39 | (22), (23), (24), (25), (26), (27) gives: % 169.68/22.39 | (35) p1(all_3_2) | ? [v0: $i] : ($i(v0) & ((r1(all_3_1, v0) & ~ p1(v0)) | % 169.68/22.39 | (r1(all_3_2, v0) & ~ p1(v0) & ! [v1: $i] : ! [v2: $i] : ( ~ % 169.68/22.39 | $i(v2) | ~ $i(v1) | ~ p1(v1) | ~ r1(v1, v2) | ~ r1(v0, v1) % 169.68/22.39 | | p1(v2))))) % 169.68/22.39 | % 169.68/22.39 | GROUND_INST: instantiating (31) with all_3_12, all_3_11, all_3_10, all_3_9, % 169.68/22.39 | all_3_8, all_3_7, all_3_6, all_3_5, all_3_4, all_3_3, all_3_2, % 169.68/22.39 | all_3_0, simplifying with (3), (4), (5), (6), (7), (8), (9), % 169.68/22.39 | (10), (11), (12), (13), (15), (16), (17), (18), (19), (20), (21), % 169.68/22.39 | (22), (23), (24), (25), (26), (28) gives: % 169.68/22.40 | (36) p1(all_3_2) | ? [v0: $i] : ($i(v0) & ((r1(all_3_0, v0) & ~ p1(v0)) | % 169.68/22.40 | (r1(all_3_2, v0) & ~ p1(v0) & ! [v1: $i] : ! [v2: $i] : ( ~ % 169.68/22.40 | $i(v2) | ~ $i(v1) | ~ p1(v1) | ~ r1(v1, v2) | ~ r1(v0, v1) % 169.68/22.40 | | p1(v2))))) % 169.68/22.40 | % 169.68/22.40 | BETA: splitting (36) gives: % 169.68/22.40 | % 169.68/22.40 | Case 1: % 169.68/22.40 | | % 170.18/22.40 | | (37) p1(all_3_2) % 170.18/22.40 | | % 170.18/22.40 | | GROUND_INST: instantiating (33) with all_3_12, all_3_11, all_3_10, all_3_9, % 170.18/22.40 | | all_3_8, all_3_7, all_3_6, all_3_5, all_3_4, all_3_3, all_3_2, % 170.18/22.40 | | all_3_1, all_3_0, simplifying with (2), (3), (4), (5), (6), % 170.18/22.40 | | (7), (8), (9), (10), (11), (12), (13), (14), (15), (16), (17), % 170.18/22.40 | | (18), (19), (20), (21), (22), (23), (24), (25), (26), (27), % 170.18/22.40 | | (28), (37) gives: % 170.18/22.40 | | (38) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & ((p1(v0) & r1(v0, v1) % 170.18/22.40 | | & r1(all_3_1, v0) & ~ p1(v1)) | (p1(v0) & r1(v0, v1) & % 170.18/22.40 | | r1(all_3_2, v0) & ~ p1(v1) & ! [v2: $i] : ! [v3: $i] : ! % 170.18/22.40 | | [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ p1(v3) | ~ % 170.18/22.40 | | r1(v3, v4) | ~ r1(v2, v3) | ~ r1(v0, v2) | p1(v4) | % 170.18/22.40 | | p1(v2)) & ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 170.18/22.40 | | $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ p1(v3) | ~ r1(v3, v4) | % 170.18/22.40 | | ~ r1(v2, v3) | ~ r1(v0, v2) | p1(v4) | ? [v5: $i] : % 170.18/22.40 | | ($i(v5) & r1(v2, v5) & ~ p1(v5)))))) % 170.18/22.40 | | % 170.18/22.41 | | DELTA: instantiating (38) with fresh symbols all_173_0, all_173_1 gives: % 170.18/22.41 | | (39) $i(all_173_0) & $i(all_173_1) & ((p1(all_173_1) & r1(all_173_1, % 170.18/22.41 | | all_173_0) & r1(all_3_1, all_173_1) & ~ p1(all_173_0)) | % 170.18/22.41 | | (p1(all_173_1) & r1(all_173_1, all_173_0) & r1(all_3_2, all_173_1) % 170.18/22.41 | | & ~ p1(all_173_0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( % 170.18/22.41 | | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ p1(v1) | ~ r1(v1, v2) | % 170.18/22.41 | | ~ r1(v0, v1) | ~ r1(all_173_1, v0) | p1(v2) | p1(v0)) & ! % 170.18/22.41 | | [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | % 170.18/22.41 | | ~ $i(v0) | ~ p1(v1) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 170.18/22.41 | | r1(all_173_1, v0) | p1(v2) | ? [v3: $i] : ($i(v3) & r1(v0, % 170.18/22.41 | | v3) & ~ p1(v3))))) % 170.18/22.41 | | % 170.18/22.41 | | ALPHA: (39) implies: % 170.18/22.41 | | (40) $i(all_173_1) % 170.18/22.41 | | (41) $i(all_173_0) % 170.18/22.41 | | (42) (p1(all_173_1) & r1(all_173_1, all_173_0) & r1(all_3_1, all_173_1) & % 170.18/22.41 | | ~ p1(all_173_0)) | (p1(all_173_1) & r1(all_173_1, all_173_0) & % 170.18/22.41 | | r1(all_3_2, all_173_1) & ~ p1(all_173_0) & ! [v0: $i] : ! [v1: % 170.18/22.41 | | $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 170.18/22.41 | | p1(v1) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ r1(all_173_1, v0) | % 170.18/22.41 | | p1(v2) | p1(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 170.18/22.41 | | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ p1(v1) | ~ r1(v1, v2) | ~ % 170.18/22.41 | | r1(v0, v1) | ~ r1(all_173_1, v0) | p1(v2) | ? [v3: $i] : % 170.18/22.41 | | ($i(v3) & r1(v0, v3) & ~ p1(v3)))) % 170.18/22.41 | | % 170.18/22.41 | | BETA: splitting (42) gives: % 170.18/22.41 | | % 170.18/22.41 | | Case 1: % 170.18/22.41 | | | % 170.18/22.41 | | | (43) p1(all_173_1) & r1(all_173_1, all_173_0) & r1(all_3_1, all_173_1) % 170.18/22.41 | | | & ~ p1(all_173_0) % 170.18/22.41 | | | % 170.18/22.41 | | | ALPHA: (43) implies: % 170.18/22.41 | | | (44) ~ p1(all_173_0) % 170.18/22.41 | | | (45) r1(all_3_1, all_173_1) % 170.18/22.41 | | | (46) r1(all_173_1, all_173_0) % 170.18/22.41 | | | % 170.18/22.42 | | | GROUND_INST: instantiating (34) with all_3_12, all_3_11, all_3_10, % 170.18/22.42 | | | all_3_9, all_3_8, all_3_7, all_3_6, all_3_5, all_3_4, % 170.18/22.42 | | | all_3_3, all_3_2, all_3_1, all_173_1, all_173_0, simplifying % 170.18/22.42 | | | with (3), (4), (5), (6), (7), (8), (9), (10), (11), (12), % 170.18/22.42 | | | (13), (14), (16), (17), (18), (19), (20), (21), (22), (23), % 170.18/22.42 | | | (24), (25), (26), (27), (40), (41), (44), (45), (46) gives: % 170.18/22.42 | | | (47) ? [v0: $i] : ($i(v0) & r1(all_3_1, v0) & ~ p1(v0)) % 170.18/22.42 | | | % 170.18/22.42 | | | DELTA: instantiating (47) with fresh symbol all_253_0 gives: % 170.18/22.42 | | | (48) $i(all_253_0) & r1(all_3_1, all_253_0) & ~ p1(all_253_0) % 170.18/22.42 | | | % 170.18/22.42 | | | ALPHA: (48) implies: % 170.18/22.42 | | | (49) ~ p1(all_253_0) % 170.18/22.42 | | | (50) r1(all_3_1, all_253_0) % 170.18/22.42 | | | (51) $i(all_253_0) % 170.18/22.42 | | | % 170.18/22.42 | | | GROUND_INST: instantiating (30) with all_253_0, simplifying with (49), % 170.18/22.42 | | | (50), (51) gives: % 170.18/22.42 | | | (52) $false % 170.18/22.42 | | | % 170.18/22.42 | | | CLOSE: (52) is inconsistent. % 170.18/22.42 | | | % 170.18/22.42 | | Case 2: % 170.18/22.42 | | | % 170.18/22.43 | | | (53) p1(all_173_1) & r1(all_173_1, all_173_0) & r1(all_3_2, all_173_1) % 170.18/22.43 | | | & ~ p1(all_173_0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 170.18/22.43 | | | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ p1(v1) | ~ r1(v1, v2) | ~ % 170.18/22.43 | | | r1(v0, v1) | ~ r1(all_173_1, v0) | p1(v2) | p1(v0)) & ! [v0: % 170.18/22.43 | | | $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 170.18/22.43 | | | $i(v0) | ~ p1(v1) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 170.18/22.43 | | | r1(all_173_1, v0) | p1(v2) | ? [v3: $i] : ($i(v3) & r1(v0, v3) % 170.18/22.43 | | | & ~ p1(v3))) % 170.18/22.43 | | | % 170.18/22.43 | | | ALPHA: (53) implies: % 170.18/22.43 | | | (54) ~ p1(all_173_0) % 170.18/22.43 | | | (55) r1(all_3_2, all_173_1) % 170.18/22.43 | | | (56) r1(all_173_1, all_173_0) % 170.18/22.43 | | | (57) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | % 170.18/22.43 | | | ~ $i(v0) | ~ p1(v1) | ~ r1(v1, v2) | ~ r1(v0, v1) | ~ % 170.18/22.43 | | | r1(all_173_1, v0) | p1(v2) | p1(v0)) % 170.18/22.43 | | | % 170.18/22.43 | | | GROUND_INST: instantiating (32) with all_3_12, all_3_11, all_3_10, % 170.18/22.43 | | | all_3_9, all_3_8, all_3_7, all_3_6, all_3_5, all_3_4, % 170.18/22.43 | | | all_3_3, all_3_2, all_173_1, all_173_0, simplifying with (3), % 170.18/22.43 | | | (4), (5), (6), (7), (8), (9), (10), (11), (12), (13), (16), % 170.18/22.43 | | | (17), (18), (19), (20), (21), (22), (23), (24), (25), (26), % 170.18/22.43 | | | (40), (41), (54), (55), (56) gives: % 170.18/22.43 | | | (58) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & ((p1(v0) & r1(v0, % 170.18/22.43 | | | v1) & r1(all_173_0, v0) & ~ p1(v1)) | (r1(all_3_2, v0) & % 170.18/22.43 | | | ~ p1(v0) & ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 170.18/22.43 | | | $i(v2) | ~ p1(v2) | ~ r1(v2, v3) | ~ r1(v0, v2) | % 170.18/22.43 | | | p1(v3))))) % 170.18/22.43 | | | % 170.18/22.43 | | | DELTA: instantiating (58) with fresh symbols all_254_0, all_254_1 gives: % 170.18/22.44 | | | (59) $i(all_254_0) & $i(all_254_1) & ((p1(all_254_1) & r1(all_254_1, % 170.18/22.44 | | | all_254_0) & r1(all_173_0, all_254_1) & ~ p1(all_254_0)) | % 170.18/22.44 | | | (r1(all_3_2, all_254_1) & ~ p1(all_254_1) & ! [v0: $i] : ! % 170.18/22.44 | | | [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ p1(v0) | ~ r1(v0, v1) % 170.18/22.44 | | | | ~ r1(all_254_1, v0) | p1(v1)))) % 170.18/22.44 | | | % 170.18/22.44 | | | ALPHA: (59) implies: % 170.18/22.44 | | | (60) $i(all_254_1) % 170.18/22.44 | | | (61) $i(all_254_0) % 170.18/22.44 | | | (62) (p1(all_254_1) & r1(all_254_1, all_254_0) & r1(all_173_0, % 170.18/22.44 | | | all_254_1) & ~ p1(all_254_0)) | (r1(all_3_2, all_254_1) & ~ % 170.18/22.44 | | | p1(all_254_1) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 170.18/22.44 | | | $i(v0) | ~ p1(v0) | ~ r1(v0, v1) | ~ r1(all_254_1, v0) | % 170.18/22.44 | | | p1(v1))) % 170.18/22.44 | | | % 170.18/22.44 | | | BETA: splitting (62) gives: % 170.18/22.44 | | | % 170.18/22.44 | | | Case 1: % 170.18/22.44 | | | | % 170.18/22.44 | | | | (63) p1(all_254_1) & r1(all_254_1, all_254_0) & r1(all_173_0, % 170.18/22.44 | | | | all_254_1) & ~ p1(all_254_0) % 170.18/22.44 | | | | % 170.18/22.44 | | | | ALPHA: (63) implies: % 170.18/22.44 | | | | (64) ~ p1(all_254_0) % 170.18/22.44 | | | | (65) r1(all_173_0, all_254_1) % 170.18/22.44 | | | | (66) r1(all_254_1, all_254_0) % 170.18/22.44 | | | | (67) p1(all_254_1) % 170.18/22.44 | | | | % 170.18/22.45 | | | | GROUND_INST: instantiating (57) with all_173_0, all_254_1, all_254_0, % 170.18/22.45 | | | | simplifying with (41), (54), (56), (60), (61), (64), (65), % 170.18/22.45 | | | | (66), (67) gives: % 170.18/22.45 | | | | (68) $false % 170.18/22.45 | | | | % 170.18/22.45 | | | | CLOSE: (68) is inconsistent. % 170.18/22.45 | | | | % 170.18/22.45 | | | Case 2: % 170.18/22.45 | | | | % 170.18/22.45 | | | | (69) r1(all_3_2, all_254_1) & ~ p1(all_254_1) & ! [v0: $i] : ! % 170.18/22.45 | | | | [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ p1(v0) | ~ r1(v0, v1) | % 170.18/22.45 | | | | ~ r1(all_254_1, v0) | p1(v1)) % 170.18/22.45 | | | | % 170.18/22.45 | | | | ALPHA: (69) implies: % 170.18/22.45 | | | | (70) ~ p1(all_254_1) % 170.18/22.45 | | | | (71) r1(all_3_2, all_254_1) % 170.18/22.45 | | | | (72) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ p1(v0) | % 170.18/22.45 | | | | ~ r1(v0, v1) | ~ r1(all_254_1, v0) | p1(v1)) % 170.18/22.45 | | | | % 170.18/22.45 | | | | GROUND_INST: instantiating (29) with all_254_1, simplifying with (60), % 170.18/22.45 | | | | (70), (71) gives: % 170.18/22.45 | | | | (73) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & p1(v0) & r1(v0, % 170.18/22.45 | | | | v1) & r1(all_254_1, v0) & ~ p1(v1)) % 170.18/22.45 | | | | % 170.18/22.45 | | | | DELTA: instantiating (73) with fresh symbols all_322_0, all_322_1 gives: % 170.18/22.45 | | | | (74) $i(all_322_0) & $i(all_322_1) & p1(all_322_1) & r1(all_322_1, % 170.18/22.45 | | | | all_322_0) & r1(all_254_1, all_322_1) & ~ p1(all_322_0) % 170.18/22.45 | | | | % 170.18/22.45 | | | | ALPHA: (74) implies: % 170.18/22.45 | | | | (75) ~ p1(all_322_0) % 170.18/22.45 | | | | (76) r1(all_254_1, all_322_1) % 170.18/22.45 | | | | (77) r1(all_322_1, all_322_0) % 170.18/22.45 | | | | (78) p1(all_322_1) % 170.18/22.45 | | | | (79) $i(all_322_1) % 170.18/22.45 | | | | (80) $i(all_322_0) % 170.18/22.45 | | | | % 170.18/22.45 | | | | GROUND_INST: instantiating (72) with all_322_1, all_322_0, simplifying % 170.18/22.45 | | | | with (75), (76), (77), (78), (79), (80) gives: % 170.18/22.45 | | | | (81) $false % 170.18/22.45 | | | | % 170.18/22.45 | | | | CLOSE: (81) is inconsistent. % 170.18/22.45 | | | | % 170.18/22.45 | | | End of split % 170.18/22.45 | | | % 170.18/22.46 | | End of split % 170.18/22.46 | | % 170.18/22.46 | Case 2: % 170.18/22.46 | | % 170.18/22.46 | | (82) ~ p1(all_3_2) % 170.18/22.46 | | % 170.18/22.46 | | BETA: splitting (35) gives: % 170.18/22.46 | | % 170.18/22.46 | | Case 1: % 170.18/22.46 | | | % 170.18/22.46 | | | (83) p1(all_3_2) % 170.18/22.46 | | | % 170.18/22.46 | | | PRED_UNIFY: (82), (83) imply: % 170.18/22.46 | | | (84) $false % 170.18/22.46 | | | % 170.18/22.46 | | | CLOSE: (84) is inconsistent. % 170.18/22.46 | | | % 170.18/22.46 | | Case 2: % 170.18/22.46 | | | % 170.18/22.46 | | | (85) ? [v0: $i] : ($i(v0) & ((r1(all_3_1, v0) & ~ p1(v0)) | % 170.18/22.46 | | | (r1(all_3_2, v0) & ~ p1(v0) & ! [v1: $i] : ! [v2: $i] : ( ~ % 170.18/22.46 | | | $i(v2) | ~ $i(v1) | ~ p1(v1) | ~ r1(v1, v2) | ~ r1(v0, % 170.18/22.46 | | | v1) | p1(v2))))) % 170.18/22.46 | | | % 170.18/22.46 | | | DELTA: instantiating (85) with fresh symbol all_141_0 gives: % 170.18/22.46 | | | (86) $i(all_141_0) & ((r1(all_3_1, all_141_0) & ~ p1(all_141_0)) | % 170.18/22.46 | | | (r1(all_3_2, all_141_0) & ~ p1(all_141_0) & ! [v0: $i] : ! % 170.18/22.46 | | | [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ p1(v0) | ~ r1(v0, v1) % 170.18/22.46 | | | | ~ r1(all_141_0, v0) | p1(v1)))) % 170.18/22.46 | | | % 170.18/22.46 | | | ALPHA: (86) implies: % 170.18/22.46 | | | (87) $i(all_141_0) % 170.18/22.46 | | | (88) (r1(all_3_1, all_141_0) & ~ p1(all_141_0)) | (r1(all_3_2, % 170.18/22.46 | | | all_141_0) & ~ p1(all_141_0) & ! [v0: $i] : ! [v1: $i] : ( % 170.18/22.46 | | | ~ $i(v1) | ~ $i(v0) | ~ p1(v0) | ~ r1(v0, v1) | ~ % 170.18/22.46 | | | r1(all_141_0, v0) | p1(v1))) % 170.18/22.46 | | | % 170.18/22.46 | | | BETA: splitting (88) gives: % 170.18/22.46 | | | % 170.18/22.46 | | | Case 1: % 170.18/22.46 | | | | % 170.18/22.46 | | | | (89) r1(all_3_1, all_141_0) & ~ p1(all_141_0) % 170.18/22.46 | | | | % 170.18/22.46 | | | | ALPHA: (89) implies: % 170.18/22.46 | | | | (90) ~ p1(all_141_0) % 170.18/22.46 | | | | (91) r1(all_3_1, all_141_0) % 170.18/22.46 | | | | % 170.18/22.46 | | | | GROUND_INST: instantiating (30) with all_141_0, simplifying with (87), % 170.18/22.46 | | | | (90), (91) gives: % 170.18/22.46 | | | | (92) $false % 170.18/22.46 | | | | % 170.18/22.46 | | | | CLOSE: (92) is inconsistent. % 170.18/22.46 | | | | % 170.18/22.46 | | | Case 2: % 170.18/22.46 | | | | % 170.18/22.46 | | | | (93) r1(all_3_2, all_141_0) & ~ p1(all_141_0) & ! [v0: $i] : ! % 170.18/22.46 | | | | [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ p1(v0) | ~ r1(v0, v1) | % 170.18/22.46 | | | | ~ r1(all_141_0, v0) | p1(v1)) % 170.18/22.46 | | | | % 170.18/22.46 | | | | ALPHA: (93) implies: % 170.18/22.46 | | | | (94) ~ p1(all_141_0) % 170.18/22.46 | | | | (95) r1(all_3_2, all_141_0) % 170.18/22.46 | | | | (96) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ p1(v0) | % 170.18/22.46 | | | | ~ r1(v0, v1) | ~ r1(all_141_0, v0) | p1(v1)) % 170.18/22.46 | | | | % 170.18/22.47 | | | | GROUND_INST: instantiating (29) with all_141_0, simplifying with (87), % 170.18/22.47 | | | | (94), (95) gives: % 170.18/22.47 | | | | (97) ? [v0: $i] : ? [v1: $i] : ($i(v1) & $i(v0) & p1(v0) & r1(v0, % 170.18/22.47 | | | | v1) & r1(all_141_0, v0) & ~ p1(v1)) % 170.18/22.47 | | | | % 170.18/22.47 | | | | DELTA: instantiating (97) with fresh symbols all_271_0, all_271_1 gives: % 170.18/22.47 | | | | (98) $i(all_271_0) & $i(all_271_1) & p1(all_271_1) & r1(all_271_1, % 170.18/22.47 | | | | all_271_0) & r1(all_141_0, all_271_1) & ~ p1(all_271_0) % 170.18/22.47 | | | | % 170.18/22.47 | | | | ALPHA: (98) implies: % 170.18/22.47 | | | | (99) ~ p1(all_271_0) % 170.18/22.47 | | | | (100) r1(all_141_0, all_271_1) % 170.18/22.47 | | | | (101) r1(all_271_1, all_271_0) % 170.18/22.47 | | | | (102) p1(all_271_1) % 170.18/22.47 | | | | (103) $i(all_271_1) % 170.18/22.47 | | | | (104) $i(all_271_0) % 170.18/22.47 | | | | % 170.18/22.47 | | | | GROUND_INST: instantiating (96) with all_271_1, all_271_0, simplifying % 170.18/22.47 | | | | with (99), (100), (101), (102), (103), (104) gives: % 170.18/22.47 | | | | (105) $false % 170.18/22.47 | | | | % 170.18/22.47 | | | | CLOSE: (105) is inconsistent. % 170.18/22.47 | | | | % 170.18/22.47 | | | End of split % 170.18/22.47 | | | % 170.18/22.47 | | End of split % 170.18/22.47 | | % 170.18/22.47 | End of split % 170.18/22.47 | % 170.18/22.47 End of proof % 170.18/22.47 % SZS output end Proof for theBenchmark % 170.18/22.47 % 170.18/22.47 21756ms %------------------------------------------------------------------------------