%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : NUM377+1.010 : TPTP v8.1.2. Released v3.2.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 11:47:27 EDT 2023 % Result : Unsatisfiable 46.66s 6.73s % Output : Proof 261.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : NUM377+1.010 : TPTP v8.1.2. Released v3.2.0. % 0.12/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 : Fri Aug 25 15:39:11 EDT 2023 % 0.12/0.33 % CPUTime : % 0.63/0.60 ________ _____ % 0.63/0.60 ___ __ \_________(_)________________________________ % 0.63/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.63/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.63/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.63/0.60 % 0.63/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.63/0.60 (2023-06-19) % 0.63/0.60 % 0.63/0.60 (c) Philipp Rümmer, 2009-2023 % 0.63/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.63/0.60 Amanda Stjerna. % 0.63/0.60 Free software under BSD-3-Clause. % 0.63/0.60 % 0.63/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.63/0.60 % 0.63/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.63/0.61 Running up to 7 provers in parallel. % 0.63/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.63/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.63/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.63/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.63/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.63/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.63/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.19/1.15 Prover 1: Preprocessing ... % 3.19/1.15 Prover 4: Preprocessing ... % 3.67/1.20 Prover 6: Preprocessing ... % 3.67/1.21 Prover 3: Preprocessing ... % 3.67/1.21 Prover 2: Preprocessing ... % 3.67/1.21 Prover 0: Preprocessing ... % 3.67/1.21 Prover 5: Preprocessing ... % 7.10/1.66 Prover 4: Constructing countermodel ... % 7.10/1.66 Prover 3: Constructing countermodel ... % 7.10/1.67 Prover 0: Constructing countermodel ... % 7.10/1.67 Prover 1: Constructing countermodel ... % 7.10/1.67 Prover 5: Constructing countermodel ... % 7.10/1.67 Prover 2: Constructing countermodel ... % 7.10/1.67 Prover 6: Constructing countermodel ... % 46.66/6.73 Prover 3: proved (6108ms) % 46.66/6.73 % 46.66/6.73 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 46.66/6.73 % 46.66/6.73 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 46.66/6.73 Prover 0: stopped % 46.66/6.73 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 46.66/6.75 Prover 2: stopped % 46.66/6.75 Prover 6: stopped % 46.66/6.75 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 46.66/6.75 Prover 5: stopped % 46.66/6.75 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 46.66/6.76 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 47.21/6.85 Prover 7: Preprocessing ... % 47.21/6.87 Prover 13: Preprocessing ... % 47.75/6.91 Prover 10: Preprocessing ... % 47.75/6.91 Prover 11: Preprocessing ... % 47.75/6.92 Prover 8: Preprocessing ... % 47.75/6.95 Prover 7: Constructing countermodel ... % 48.50/6.99 Prover 13: Constructing countermodel ... % 48.50/6.99 Prover 11: Constructing countermodel ... % 48.50/7.00 Prover 8: Constructing countermodel ... % 48.72/7.01 Prover 10: Constructing countermodel ... % 82.70/11.43 Prover 13: stopped % 82.70/11.43 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 83.46/11.48 Prover 16: Preprocessing ... % 83.95/11.55 Prover 16: Constructing countermodel ... % 118.81/15.96 Prover 1: stopped % 118.81/15.96 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 119.27/16.03 Prover 19: Preprocessing ... % 119.51/16.11 Prover 19: Constructing countermodel ... % 125.21/16.80 Prover 16: stopped % 143.44/19.54 Prover 19: stopped % 186.50/27.95 Prover 4: stopped % 188.87/28.45 Prover 7: stopped % 225.54/40.11 Prover 11: stopped % 226.56/40.53 Prover 8: stopped % 243.30/56.01 Prover 10: Found proof (size 202087) % 243.30/56.01 Prover 10: proved (49258ms) % 243.30/56.01 % 243.30/56.01 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 243.30/56.01 % 252.07/63.83 % SZS output start Proof for theBenchmark % 252.22/63.93 Assumptions after simplification: % 252.22/63.93 --------------------------------- % 252.22/63.93 % 252.22/63.93 (try_satisfy_this) % 252.32/64.02 $i(n10) & $i(n9) & $i(n8) & $i(n7) & $i(n6) & $i(n5) & $i(n4) & $i(n3) & % 252.32/64.02 $i(n2) & $i(n1) & $i(n0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: % 252.32/64.02 $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : % 252.32/64.02 ? [v9: $i] : ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? % 252.32/64.02 [v14: $i] : ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : ? % 252.32/64.02 [v19: $i] : ? [v20: $i] : ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : ? % 252.32/64.02 [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? [v28: $i] : ? % 252.32/64.02 [v29: $i] : ? [v30: $i] : ? [v31: $i] : ? [v32: $i] : ? [v33: $i] : ? % 252.32/64.02 [v34: $i] : ? [v35: $i] : ? [v36: $i] : ? [v37: $i] : ? [v38: $i] : ? % 252.32/64.02 [v39: $i] : ? [v40: $i] : ? [v41: $i] : ? [v42: $i] : ? [v43: $i] : ? % 252.32/64.02 [v44: $i] : ? [v45: $i] : ? [v46: $i] : ? [v47: $i] : ? [v48: $i] : ? % 252.32/64.02 [v49: $i] : ? [v50: $i] : ? [v51: $i] : ? [v52: $i] : ? [v53: $i] : ? % 252.32/64.02 [v54: $i] : ? [v55: $i] : ? [v56: $i] : ? [v57: $i] : ? [v58: $i] : ? % 252.32/64.02 [v59: $i] : ? [v60: $i] : ? [v61: $i] : ? [v62: $i] : ? [v63: $i] : ? % 252.32/64.02 [v64: $i] : ? [v65: $i] : ? [v66: $i] : ? [v67: $i] : ? [v68: $i] : ? % 252.32/64.02 [v69: $i] : ? [v70: $i] : ? [v71: $i] : ? [v72: $i] : ? [v73: $i] : ? % 252.32/64.02 [v74: $i] : ? [v75: $i] : ? [v76: $i] : ? [v77: $i] : ? [v78: $i] : ? % 252.32/64.02 [v79: $i] : ? [v80: $i] : ? [v81: $i] : ? [v82: $i] : ? [v83: $i] : ? % 252.32/64.02 [v84: $i] : ? [v85: $i] : ? [v86: $i] : ? [v87: $i] : ? [v88: $i] : ? % 252.32/64.02 [v89: $i] : ? [v90: $i] : ? [v91: $i] : ? [v92: $i] : ? [v93: $i] : ? % 252.32/64.02 [v94: $i] : ? [v95: $i] : ? [v96: $i] : ? [v97: $i] : ? [v98: $i] : ? % 252.32/64.02 [v99: $i] : ? [v100: $i] : ? [v101: $i] : ( ~ (n10 = n9) & ~ (n10 = n8) & % 252.32/64.02 ~ (n10 = n7) & ~ (n10 = n6) & ~ (n10 = n5) & ~ (n10 = n4) & ~ (n10 = n3) % 252.32/64.02 & ~ (n10 = n2) & ~ (n10 = n1) & ~ (n10 = n0) & ~ (n9 = n8) & ~ (n9 = % 252.32/64.02 n7) & ~ (n9 = n6) & ~ (n9 = n5) & ~ (n9 = n4) & ~ (n9 = n3) & ~ (n9 = % 252.32/64.02 n2) & ~ (n9 = n1) & ~ (n9 = n0) & ~ (n8 = n7) & ~ (n8 = n6) & ~ (n8 = % 252.32/64.02 n5) & ~ (n8 = n4) & ~ (n8 = n3) & ~ (n8 = n2) & ~ (n8 = n1) & ~ (n8 = % 252.32/64.02 n0) & ~ (n7 = n6) & ~ (n7 = n5) & ~ (n7 = n4) & ~ (n7 = n3) & ~ (n7 = % 252.32/64.02 n2) & ~ (n7 = n1) & ~ (n7 = n0) & ~ (n6 = n5) & ~ (n6 = n4) & ~ (n6 = % 252.32/64.02 n3) & ~ (n6 = n2) & ~ (n6 = n1) & ~ (n6 = n0) & ~ (n5 = n4) & ~ (n5 = % 252.32/64.02 n3) & ~ (n5 = n2) & ~ (n5 = n1) & ~ (n5 = n0) & ~ (n4 = n3) & ~ (n4 = % 252.32/64.02 n2) & ~ (n4 = n1) & ~ (n4 = n0) & ~ (n3 = n2) & ~ (n3 = n1) & ~ (n3 = % 252.32/64.02 n0) & ~ (n2 = n1) & ~ (n2 = n0) & ~ (n1 = n0) & pred(v19) = v97 & % 252.32/64.02 pred(v18) = v94 & pred(v17) = v89 & pred(v16) = v86 & pred(v15) = v81 & % 252.32/64.02 pred(v14) = v78 & pred(v13) = v73 & pred(v12) = v70 & pred(v11) = v65 & % 252.32/64.02 pred(v10) = v62 & pred(v9) = v57 & pred(v8) = v54 & pred(v7) = v49 & % 252.32/64.02 pred(v6) = v46 & pred(v5) = v41 & pred(v4) = v38 & pred(v3) = v33 & pred(v2) % 252.32/64.02 = v30 & pred(v1) = v25 & pred(v0) = v22 & pred(n10) = n9 & pred(n9) = n8 & % 252.32/64.02 pred(n8) = n7 & pred(n7) = n6 & pred(n6) = n5 & pred(n5) = n4 & pred(n4) = % 252.32/64.02 n3 & pred(n3) = n2 & pred(n2) = n1 & pred(n1) = n0 & pred(n0) = n10 & % 252.32/64.02 succ(v19) = v95 & succ(v18) = v98 & succ(v17) = v87 & succ(v16) = v90 & % 252.32/64.02 succ(v15) = v79 & succ(v14) = v82 & succ(v13) = v71 & succ(v12) = v74 & % 252.32/64.02 succ(v11) = v63 & succ(v10) = v66 & succ(v9) = v55 & succ(v8) = v58 & % 252.32/64.02 succ(v7) = v47 & succ(v6) = v50 & succ(v5) = v39 & succ(v4) = v42 & succ(v3) % 252.32/64.02 = v31 & succ(v2) = v34 & succ(v1) = v23 & succ(v0) = v26 & succ(n10) = n0 & % 252.32/64.02 succ(n9) = n10 & succ(n8) = n9 & succ(n7) = n8 & succ(n6) = n7 & succ(n5) = % 252.32/64.02 n6 & succ(n4) = n5 & succ(n3) = n4 & succ(n2) = n3 & succ(n1) = n2 & % 252.32/64.02 succ(n0) = n1 & sum(v100, v101) = v21 & sum(v97, v98) = v99 & sum(v97, v95) % 252.32/64.02 = v101 & sum(v96, v99) = v20 & sum(v94, v98) = v100 & sum(v94, v95) = v96 & % 252.32/64.02 sum(v92, v93) = v19 & sum(v89, v90) = v91 & sum(v89, v87) = v93 & sum(v88, % 252.32/64.02 v91) = v18 & sum(v86, v90) = v92 & sum(v86, v87) = v88 & sum(v84, v85) = % 252.32/64.02 v17 & sum(v81, v82) = v83 & sum(v81, v79) = v85 & sum(v80, v83) = v16 & % 252.32/64.02 sum(v78, v82) = v84 & sum(v78, v79) = v80 & sum(v76, v77) = v15 & sum(v73, % 252.32/64.02 v74) = v75 & sum(v73, v71) = v77 & sum(v72, v75) = v14 & sum(v70, v74) = % 252.32/64.02 v76 & sum(v70, v71) = v72 & sum(v68, v69) = v13 & sum(v65, v66) = v67 & % 252.32/64.02 sum(v65, v63) = v69 & sum(v64, v67) = v12 & sum(v62, v66) = v68 & sum(v62, % 252.32/64.02 v63) = v64 & sum(v60, v61) = v11 & sum(v57, v58) = v59 & sum(v57, v55) = % 252.32/64.02 v61 & sum(v56, v59) = v10 & sum(v54, v58) = v60 & sum(v54, v55) = v56 & % 252.32/64.02 sum(v52, v53) = v9 & sum(v49, v50) = v51 & sum(v49, v47) = v53 & sum(v48, % 252.32/64.02 v51) = v8 & sum(v46, v50) = v52 & sum(v46, v47) = v48 & sum(v44, v45) = v7 % 252.32/64.02 & sum(v41, v42) = v43 & sum(v41, v39) = v45 & sum(v40, v43) = v6 & sum(v38, % 252.32/64.02 v42) = v44 & sum(v38, v39) = v40 & sum(v36, v37) = v5 & sum(v33, v34) = % 252.32/64.02 v35 & sum(v33, v31) = v37 & sum(v32, v35) = v4 & sum(v30, v34) = v36 & % 252.32/64.02 sum(v30, v31) = v32 & sum(v28, v29) = v3 & sum(v25, v26) = v27 & sum(v25, % 252.32/64.02 v23) = v29 & sum(v24, v27) = v2 & sum(v22, v26) = v28 & sum(v22, v23) = % 252.32/64.02 v24 & sum(n10, n10) = n9 & sum(n10, n9) = n8 & sum(n10, n8) = n7 & sum(n10, % 252.32/64.02 n7) = n6 & sum(n10, n6) = n5 & sum(n10, n5) = n4 & sum(n10, n4) = n3 & % 252.32/64.02 sum(n10, n3) = n2 & sum(n10, n2) = n1 & sum(n10, n1) = n0 & sum(n10, n0) = % 252.32/64.02 n10 & sum(n9, n10) = n8 & sum(n9, n9) = n7 & sum(n9, n8) = n6 & sum(n9, n7) % 252.32/64.02 = n5 & sum(n9, n6) = n4 & sum(n9, n5) = n3 & sum(n9, n4) = n2 & sum(n9, n3) % 252.32/64.02 = n1 & sum(n9, n2) = n0 & sum(n9, n1) = n10 & sum(n9, n0) = n9 & sum(n8, % 252.32/64.02 n10) = n7 & sum(n8, n9) = n6 & sum(n8, n8) = n5 & sum(n8, n7) = n4 & % 252.32/64.02 sum(n8, n6) = n3 & sum(n8, n5) = n2 & sum(n8, n4) = n1 & sum(n8, n3) = n0 & % 252.32/64.02 sum(n8, n2) = n10 & sum(n8, n1) = n9 & sum(n8, n0) = n8 & sum(n7, n10) = n6 % 252.32/64.02 & sum(n7, n9) = n5 & sum(n7, n8) = n4 & sum(n7, n7) = n3 & sum(n7, n6) = n2 % 252.32/64.02 & sum(n7, n5) = n1 & sum(n7, n4) = n0 & sum(n7, n3) = n10 & sum(n7, n2) = n9 % 252.32/64.02 & sum(n7, n1) = n8 & sum(n7, n0) = n7 & sum(n6, n10) = n5 & sum(n6, n9) = n4 % 252.32/64.02 & sum(n6, n8) = n3 & sum(n6, n7) = n2 & sum(n6, n6) = n1 & sum(n6, n5) = n0 % 252.32/64.02 & sum(n6, n4) = n10 & sum(n6, n3) = n9 & sum(n6, n2) = n8 & sum(n6, n1) = n7 % 252.32/64.02 & sum(n6, n0) = n6 & sum(n5, n10) = n4 & sum(n5, n9) = n3 & sum(n5, n8) = n2 % 252.32/64.02 & sum(n5, n7) = n1 & sum(n5, n6) = n0 & sum(n5, n5) = n10 & sum(n5, n4) = n9 % 252.32/64.02 & sum(n5, n3) = n8 & sum(n5, n2) = n7 & sum(n5, n1) = n6 & sum(n5, n0) = n5 % 252.32/64.02 & sum(n4, n10) = n3 & sum(n4, n9) = n2 & sum(n4, n8) = n1 & sum(n4, n7) = n0 % 252.32/64.02 & sum(n4, n6) = n10 & sum(n4, n5) = n9 & sum(n4, n4) = n8 & sum(n4, n3) = n7 % 252.32/64.02 & sum(n4, n2) = n6 & sum(n4, n1) = n5 & sum(n4, n0) = n4 & sum(n3, n10) = n2 % 252.32/64.02 & sum(n3, n9) = n1 & sum(n3, n8) = n0 & sum(n3, n7) = n10 & sum(n3, n6) = n9 % 252.32/64.02 & sum(n3, n5) = n8 & sum(n3, n4) = n7 & sum(n3, n3) = n6 & sum(n3, n2) = n5 % 252.32/64.02 & sum(n3, n1) = n4 & sum(n3, n0) = n3 & sum(n2, n10) = n1 & sum(n2, n9) = n0 % 252.32/64.02 & sum(n2, n8) = n10 & sum(n2, n7) = n9 & sum(n2, n6) = n8 & sum(n2, n5) = n7 % 252.32/64.02 & sum(n2, n4) = n6 & sum(n2, n3) = n5 & sum(n2, n2) = n4 & sum(n2, n1) = n3 % 252.32/64.02 & sum(n2, n0) = n2 & sum(n1, n10) = n0 & sum(n1, n9) = n10 & sum(n1, n8) = % 252.32/64.02 n9 & sum(n1, n7) = n8 & sum(n1, n6) = n7 & sum(n1, n5) = n6 & sum(n1, n4) = % 252.32/64.02 n5 & sum(n1, n3) = n4 & sum(n1, n2) = n3 & sum(n1, n1) = n2 & sum(n1, n0) = % 252.32/64.02 n1 & sum(n0, n10) = n10 & sum(n0, n9) = n9 & sum(n0, n8) = n8 & sum(n0, n7) % 252.32/64.02 = n7 & sum(n0, n6) = n6 & sum(n0, n5) = n5 & sum(n0, n4) = n4 & sum(n0, n3) % 252.32/64.02 = n3 & sum(n0, n2) = n2 & sum(n0, n1) = n1 & sum(n0, n0) = n0 & $i(v101) & % 252.32/64.02 $i(v100) & $i(v99) & $i(v98) & $i(v97) & $i(v96) & $i(v95) & $i(v94) & % 252.32/64.02 $i(v93) & $i(v92) & $i(v91) & $i(v90) & $i(v89) & $i(v88) & $i(v87) & % 252.32/64.02 $i(v86) & $i(v85) & $i(v84) & $i(v83) & $i(v82) & $i(v81) & $i(v80) & % 252.32/64.02 $i(v79) & $i(v78) & $i(v77) & $i(v76) & $i(v75) & $i(v74) & $i(v73) & % 252.32/64.02 $i(v72) & $i(v71) & $i(v70) & $i(v69) & $i(v68) & $i(v67) & $i(v66) & % 252.32/64.02 $i(v65) & $i(v64) & $i(v63) & $i(v62) & $i(v61) & $i(v60) & $i(v59) & % 252.32/64.02 $i(v58) & $i(v57) & $i(v56) & $i(v55) & $i(v54) & $i(v53) & $i(v52) & % 252.32/64.02 $i(v51) & $i(v50) & $i(v49) & $i(v48) & $i(v47) & $i(v46) & $i(v45) & % 252.32/64.02 $i(v44) & $i(v43) & $i(v42) & $i(v41) & $i(v40) & $i(v39) & $i(v38) & % 252.32/64.02 $i(v37) & $i(v36) & $i(v35) & $i(v34) & $i(v33) & $i(v32) & $i(v31) & % 252.32/64.02 $i(v30) & $i(v29) & $i(v28) & $i(v27) & $i(v26) & $i(v25) & $i(v24) & % 252.32/64.03 $i(v23) & $i(v22) & $i(v21) & $i(v20) & $i(v19) & $i(v18) & $i(v17) & % 252.32/64.03 $i(v16) & $i(v15) & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) % 252.32/64.03 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 252.32/64.03 $i(v0) & ( ~ (v21 = v20) | ~ (v19 = v18) | ~ (v17 = v16) | ~ (v15 = v14) % 252.32/64.03 | ~ (v13 = v12) | ~ (v11 = v10) | ~ (v9 = v8) | ~ (v7 = v6) | ~ (v5 = % 252.32/64.03 v4) | ~ (v3 = v2)) & (v1 = n10 | v1 = n9 | v1 = n8 | v1 = n7 | v1 = n6 % 252.32/64.03 | v1 = n5 | v1 = n4 | v1 = n3 | v1 = n2 | v1 = n1 | v1 = n0) & (v0 = n10 | % 252.32/64.03 v0 = n9 | v0 = n8 | v0 = n7 | v0 = n6 | v0 = n5 | v0 = n4 | v0 = n3 | v0 = % 252.32/64.03 n2 | v0 = n1 | v0 = n0)) % 252.32/64.03 % 252.32/64.03 (function-axioms) % 252.32/64.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (sum(v3, % 252.32/64.03 v2) = v1) | ~ (sum(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 252.32/64.03 $i] : (v1 = v0 | ~ (pred(v2) = v1) | ~ (pred(v2) = v0)) & ! [v0: $i] : ! % 252.32/64.03 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (succ(v2) = v1) | ~ (succ(v2) = v0)) % 252.32/64.03 % 252.32/64.03 Those formulas are unsatisfiable: % 252.32/64.03 --------------------------------- % 252.32/64.03 % 252.32/64.03 Begin of proof % 252.32/64.03 | % 252.32/64.03 | ALPHA: (try_satisfy_this) implies: % 252.79/64.06 | (1) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 252.79/64.06 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 252.79/64.06 | [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 252.79/64.06 | ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : ? [v19: % 252.79/64.06 | $i] : ? [v20: $i] : ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : ? % 252.79/64.06 | [v24: $i] : ? [v25: $i] : ? [v26: $i] : ? [v27: $i] : ? [v28: $i] : % 252.79/64.06 | ? [v29: $i] : ? [v30: $i] : ? [v31: $i] : ? [v32: $i] : ? [v33: % 252.79/64.06 | $i] : ? [v34: $i] : ? [v35: $i] : ? [v36: $i] : ? [v37: $i] : ? % 252.79/64.06 | [v38: $i] : ? [v39: $i] : ? [v40: $i] : ? [v41: $i] : ? [v42: $i] : % 252.79/64.06 | ? [v43: $i] : ? [v44: $i] : ? [v45: $i] : ? [v46: $i] : ? [v47: % 252.79/64.06 | $i] : ? [v48: $i] : ? [v49: $i] : ? [v50: $i] : ? [v51: $i] : ? % 252.79/64.06 | [v52: $i] : ? [v53: $i] : ? [v54: $i] : ? [v55: $i] : ? [v56: $i] : % 252.79/64.06 | ? [v57: $i] : ? [v58: $i] : ? [v59: $i] : ? [v60: $i] : ? [v61: % 252.79/64.06 | $i] : ? [v62: $i] : ? [v63: $i] : ? [v64: $i] : ? [v65: $i] : ? % 252.79/64.06 | [v66: $i] : ? [v67: $i] : ? [v68: $i] : ? [v69: $i] : ? [v70: $i] : % 252.79/64.06 | ? [v71: $i] : ? [v72: $i] : ? [v73: $i] : ? [v74: $i] : ? [v75: % 252.79/64.06 | $i] : ? [v76: $i] : ? [v77: $i] : ? [v78: $i] : ? [v79: $i] : ? % 252.79/64.06 | [v80: $i] : ? [v81: $i] : ? [v82: $i] : ? [v83: $i] : ? [v84: $i] : % 252.79/64.06 | ? [v85: $i] : ? [v86: $i] : ? [v87: $i] : ? [v88: $i] : ? [v89: % 252.79/64.06 | $i] : ? [v90: $i] : ? [v91: $i] : ? [v92: $i] : ? [v93: $i] : ? % 252.79/64.07 | [v94: $i] : ? [v95: $i] : ? [v96: $i] : ? [v97: $i] : ? [v98: $i] : % 252.79/64.07 | ? [v99: $i] : ? [v100: $i] : ? [v101: $i] : ( ~ (n10 = n9) & ~ (n10 % 252.79/64.07 | = n8) & ~ (n10 = n7) & ~ (n10 = n6) & ~ (n10 = n5) & ~ (n10 = % 252.79/64.07 | n4) & ~ (n10 = n3) & ~ (n10 = n2) & ~ (n10 = n1) & ~ (n10 = n0) % 252.79/64.07 | & ~ (n9 = n8) & ~ (n9 = n7) & ~ (n9 = n6) & ~ (n9 = n5) & ~ (n9 % 252.79/64.07 | = n4) & ~ (n9 = n3) & ~ (n9 = n2) & ~ (n9 = n1) & ~ (n9 = n0) & % 252.79/64.07 | ~ (n8 = n7) & ~ (n8 = n6) & ~ (n8 = n5) & ~ (n8 = n4) & ~ (n8 = % 252.79/64.07 | n3) & ~ (n8 = n2) & ~ (n8 = n1) & ~ (n8 = n0) & ~ (n7 = n6) & % 252.79/64.07 | ~ (n7 = n5) & ~ (n7 = n4) & ~ (n7 = n3) & ~ (n7 = n2) & ~ (n7 = % 252.79/64.07 | n1) & ~ (n7 = n0) & ~ (n6 = n5) & ~ (n6 = n4) & ~ (n6 = n3) & % 252.79/64.07 | ~ (n6 = n2) & ~ (n6 = n1) & ~ (n6 = n0) & ~ (n5 = n4) & ~ (n5 = % 252.79/64.07 | n3) & ~ (n5 = n2) & ~ (n5 = n1) & ~ (n5 = n0) & ~ (n4 = n3) & % 252.79/64.07 | ~ (n4 = n2) & ~ (n4 = n1) & ~ (n4 = n0) & ~ (n3 = n2) & ~ (n3 = % 252.79/64.07 | n1) & ~ (n3 = n0) & ~ (n2 = n1) & ~ (n2 = n0) & ~ (n1 = n0) & % 252.79/64.07 | pred(v19) = v97 & pred(v18) = v94 & pred(v17) = v89 & pred(v16) = v86 % 252.79/64.07 | & pred(v15) = v81 & pred(v14) = v78 & pred(v13) = v73 & pred(v12) = % 252.79/64.07 | v70 & pred(v11) = v65 & pred(v10) = v62 & pred(v9) = v57 & pred(v8) = % 252.79/64.07 | v54 & pred(v7) = v49 & pred(v6) = v46 & pred(v5) = v41 & pred(v4) = % 252.79/64.07 | v38 & pred(v3) = v33 & pred(v2) = v30 & pred(v1) = v25 & pred(v0) = % 252.79/64.07 | v22 & pred(n10) = n9 & pred(n9) = n8 & pred(n8) = n7 & pred(n7) = n6 % 252.79/64.07 | & pred(n6) = n5 & pred(n5) = n4 & pred(n4) = n3 & pred(n3) = n2 & % 252.79/64.07 | pred(n2) = n1 & pred(n1) = n0 & pred(n0) = n10 & succ(v19) = v95 & % 252.79/64.07 | succ(v18) = v98 & succ(v17) = v87 & succ(v16) = v90 & succ(v15) = v79 % 252.79/64.07 | & succ(v14) = v82 & succ(v13) = v71 & succ(v12) = v74 & succ(v11) = % 252.79/64.07 | v63 & succ(v10) = v66 & succ(v9) = v55 & succ(v8) = v58 & succ(v7) = % 252.79/64.07 | v47 & succ(v6) = v50 & succ(v5) = v39 & succ(v4) = v42 & succ(v3) = % 252.79/64.07 | v31 & succ(v2) = v34 & succ(v1) = v23 & succ(v0) = v26 & succ(n10) = % 252.79/64.07 | n0 & succ(n9) = n10 & succ(n8) = n9 & succ(n7) = n8 & succ(n6) = n7 & % 252.79/64.07 | succ(n5) = n6 & succ(n4) = n5 & succ(n3) = n4 & succ(n2) = n3 & % 252.79/64.07 | succ(n1) = n2 & succ(n0) = n1 & sum(v100, v101) = v21 & sum(v97, v98) % 252.79/64.07 | = v99 & sum(v97, v95) = v101 & sum(v96, v99) = v20 & sum(v94, v98) = % 252.79/64.07 | v100 & sum(v94, v95) = v96 & sum(v92, v93) = v19 & sum(v89, v90) = % 252.79/64.07 | v91 & sum(v89, v87) = v93 & sum(v88, v91) = v18 & sum(v86, v90) = v92 % 252.79/64.07 | & sum(v86, v87) = v88 & sum(v84, v85) = v17 & sum(v81, v82) = v83 & % 252.79/64.07 | sum(v81, v79) = v85 & sum(v80, v83) = v16 & sum(v78, v82) = v84 & % 252.79/64.07 | sum(v78, v79) = v80 & sum(v76, v77) = v15 & sum(v73, v74) = v75 & % 252.79/64.07 | sum(v73, v71) = v77 & sum(v72, v75) = v14 & sum(v70, v74) = v76 & % 252.79/64.07 | sum(v70, v71) = v72 & sum(v68, v69) = v13 & sum(v65, v66) = v67 & % 252.79/64.07 | sum(v65, v63) = v69 & sum(v64, v67) = v12 & sum(v62, v66) = v68 & % 252.79/64.07 | sum(v62, v63) = v64 & sum(v60, v61) = v11 & sum(v57, v58) = v59 & % 252.79/64.07 | sum(v57, v55) = v61 & sum(v56, v59) = v10 & sum(v54, v58) = v60 & % 252.79/64.07 | sum(v54, v55) = v56 & sum(v52, v53) = v9 & sum(v49, v50) = v51 & % 252.79/64.07 | sum(v49, v47) = v53 & sum(v48, v51) = v8 & sum(v46, v50) = v52 & % 252.79/64.07 | sum(v46, v47) = v48 & sum(v44, v45) = v7 & sum(v41, v42) = v43 & % 252.79/64.07 | sum(v41, v39) = v45 & sum(v40, v43) = v6 & sum(v38, v42) = v44 & % 252.79/64.07 | sum(v38, v39) = v40 & sum(v36, v37) = v5 & sum(v33, v34) = v35 & % 252.79/64.07 | sum(v33, v31) = v37 & sum(v32, v35) = v4 & sum(v30, v34) = v36 & % 252.79/64.07 | sum(v30, v31) = v32 & sum(v28, v29) = v3 & sum(v25, v26) = v27 & % 252.79/64.07 | sum(v25, v23) = v29 & sum(v24, v27) = v2 & sum(v22, v26) = v28 & % 252.79/64.07 | sum(v22, v23) = v24 & sum(n10, n10) = n9 & sum(n10, n9) = n8 & % 252.79/64.07 | sum(n10, n8) = n7 & sum(n10, n7) = n6 & sum(n10, n6) = n5 & sum(n10, % 252.79/64.07 | n5) = n4 & sum(n10, n4) = n3 & sum(n10, n3) = n2 & sum(n10, n2) = % 252.79/64.07 | n1 & sum(n10, n1) = n0 & sum(n10, n0) = n10 & sum(n9, n10) = n8 & % 252.79/64.07 | sum(n9, n9) = n7 & sum(n9, n8) = n6 & sum(n9, n7) = n5 & sum(n9, n6) % 252.79/64.07 | = n4 & sum(n9, n5) = n3 & sum(n9, n4) = n2 & sum(n9, n3) = n1 & % 252.79/64.07 | sum(n9, n2) = n0 & sum(n9, n1) = n10 & sum(n9, n0) = n9 & sum(n8, % 252.79/64.07 | n10) = n7 & sum(n8, n9) = n6 & sum(n8, n8) = n5 & sum(n8, n7) = n4 % 252.79/64.07 | & sum(n8, n6) = n3 & sum(n8, n5) = n2 & sum(n8, n4) = n1 & sum(n8, % 252.79/64.07 | n3) = n0 & sum(n8, n2) = n10 & sum(n8, n1) = n9 & sum(n8, n0) = n8 % 252.79/64.07 | & sum(n7, n10) = n6 & sum(n7, n9) = n5 & sum(n7, n8) = n4 & sum(n7, % 252.79/64.07 | n7) = n3 & sum(n7, n6) = n2 & sum(n7, n5) = n1 & sum(n7, n4) = n0 & % 252.79/64.07 | sum(n7, n3) = n10 & sum(n7, n2) = n9 & sum(n7, n1) = n8 & sum(n7, n0) % 252.79/64.07 | = n7 & sum(n6, n10) = n5 & sum(n6, n9) = n4 & sum(n6, n8) = n3 & % 252.79/64.07 | sum(n6, n7) = n2 & sum(n6, n6) = n1 & sum(n6, n5) = n0 & sum(n6, n4) % 252.79/64.07 | = n10 & sum(n6, n3) = n9 & sum(n6, n2) = n8 & sum(n6, n1) = n7 & % 252.79/64.07 | sum(n6, n0) = n6 & sum(n5, n10) = n4 & sum(n5, n9) = n3 & sum(n5, n8) % 252.79/64.07 | = n2 & sum(n5, n7) = n1 & sum(n5, n6) = n0 & sum(n5, n5) = n10 & % 252.79/64.07 | sum(n5, n4) = n9 & sum(n5, n3) = n8 & sum(n5, n2) = n7 & sum(n5, n1) % 252.79/64.07 | = n6 & sum(n5, n0) = n5 & sum(n4, n10) = n3 & sum(n4, n9) = n2 & % 252.79/64.07 | sum(n4, n8) = n1 & sum(n4, n7) = n0 & sum(n4, n6) = n10 & sum(n4, n5) % 252.79/64.07 | = n9 & sum(n4, n4) = n8 & sum(n4, n3) = n7 & sum(n4, n2) = n6 & % 252.79/64.07 | sum(n4, n1) = n5 & sum(n4, n0) = n4 & sum(n3, n10) = n2 & sum(n3, n9) % 252.79/64.07 | = n1 & sum(n3, n8) = n0 & sum(n3, n7) = n10 & sum(n3, n6) = n9 & % 252.79/64.07 | sum(n3, n5) = n8 & sum(n3, n4) = n7 & sum(n3, n3) = n6 & sum(n3, n2) % 252.79/64.07 | = n5 & sum(n3, n1) = n4 & sum(n3, n0) = n3 & sum(n2, n10) = n1 & % 252.79/64.07 | sum(n2, n9) = n0 & sum(n2, n8) = n10 & sum(n2, n7) = n9 & sum(n2, n6) % 252.79/64.07 | = n8 & sum(n2, n5) = n7 & sum(n2, n4) = n6 & sum(n2, n3) = n5 & % 252.79/64.07 | sum(n2, n2) = n4 & sum(n2, n1) = n3 & sum(n2, n0) = n2 & sum(n1, n10) % 252.79/64.07 | = n0 & sum(n1, n9) = n10 & sum(n1, n8) = n9 & sum(n1, n7) = n8 & % 252.79/64.07 | sum(n1, n6) = n7 & sum(n1, n5) = n6 & sum(n1, n4) = n5 & sum(n1, n3) % 252.79/64.07 | = n4 & sum(n1, n2) = n3 & sum(n1, n1) = n2 & sum(n1, n0) = n1 & % 252.79/64.07 | sum(n0, n10) = n10 & sum(n0, n9) = n9 & sum(n0, n8) = n8 & sum(n0, % 252.79/64.07 | n7) = n7 & sum(n0, n6) = n6 & sum(n0, n5) = n5 & sum(n0, n4) = n4 & % 252.79/64.07 | sum(n0, n3) = n3 & sum(n0, n2) = n2 & sum(n0, n1) = n1 & sum(n0, n0) % 252.79/64.07 | = n0 & $i(v101) & $i(v100) & $i(v99) & $i(v98) & $i(v97) & $i(v96) & % 252.79/64.07 | $i(v95) & $i(v94) & $i(v93) & $i(v92) & $i(v91) & $i(v90) & $i(v89) & % 252.79/64.07 | $i(v88) & $i(v87) & $i(v86) & $i(v85) & $i(v84) & $i(v83) & $i(v82) & % 252.79/64.07 | $i(v81) & $i(v80) & $i(v79) & $i(v78) & $i(v77) & $i(v76) & $i(v75) & % 252.79/64.07 | $i(v74) & $i(v73) & $i(v72) & $i(v71) & $i(v70) & $i(v69) & $i(v68) & % 252.79/64.07 | $i(v67) & $i(v66) & $i(v65) & $i(v64) & $i(v63) & $i(v62) & $i(v61) & % 252.79/64.07 | $i(v60) & $i(v59) & $i(v58) & $i(v57) & $i(v56) & $i(v55) & $i(v54) & % 252.79/64.07 | $i(v53) & $i(v52) & $i(v51) & $i(v50) & $i(v49) & $i(v48) & $i(v47) & % 252.79/64.07 | $i(v46) & $i(v45) & $i(v44) & $i(v43) & $i(v42) & $i(v41) & $i(v40) & % 252.79/64.07 | $i(v39) & $i(v38) & $i(v37) & $i(v36) & $i(v35) & $i(v34) & $i(v33) & % 252.79/64.07 | $i(v32) & $i(v31) & $i(v30) & $i(v29) & $i(v28) & $i(v27) & $i(v26) & % 252.79/64.07 | $i(v25) & $i(v24) & $i(v23) & $i(v22) & $i(v21) & $i(v20) & $i(v19) & % 252.79/64.07 | $i(v18) & $i(v17) & $i(v16) & $i(v15) & $i(v14) & $i(v13) & $i(v12) & % 252.79/64.07 | $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 252.79/64.07 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & ( ~ (v21 = v20) | ~ % 252.79/64.07 | (v19 = v18) | ~ (v17 = v16) | ~ (v15 = v14) | ~ (v13 = v12) | ~ % 252.79/64.07 | (v11 = v10) | ~ (v9 = v8) | ~ (v7 = v6) | ~ (v5 = v4) | ~ (v3 = % 252.79/64.07 | v2)) & (v1 = n10 | v1 = n9 | v1 = n8 | v1 = n7 | v1 = n6 | v1 = % 252.79/64.07 | n5 | v1 = n4 | v1 = n3 | v1 = n2 | v1 = n1 | v1 = n0) & (v0 = n10 | % 252.79/64.07 | v0 = n9 | v0 = n8 | v0 = n7 | v0 = n6 | v0 = n5 | v0 = n4 | v0 = n3 % 252.79/64.07 | | v0 = n2 | v0 = n1 | v0 = n0)) % 252.79/64.07 | % 252.79/64.07 | ALPHA: (function-axioms) implies: % 252.79/64.07 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (succ(v2) = v1) % 252.79/64.07 | | ~ (succ(v2) = v0)) % 252.79/64.07 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (pred(v2) = v1) % 252.79/64.07 | | ~ (pred(v2) = v0)) % 252.79/64.07 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 252.79/64.07 | (sum(v3, v2) = v1) | ~ (sum(v3, v2) = v0)) % 252.79/64.07 | % 252.79/64.07 | DELTA: instantiating (1) with fresh symbols all_4_0, all_4_1, all_4_2, % 252.79/64.07 | all_4_3, all_4_4, all_4_5, all_4_6, all_4_7, all_4_8, all_4_9, % 252.79/64.07 | all_4_10, all_4_11, all_4_12, all_4_13, all_4_14, all_4_15, all_4_16, % 252.79/64.07 | all_4_17, all_4_18, all_4_19, all_4_20, all_4_21, all_4_22, all_4_23, % 252.79/64.07 | all_4_24, all_4_25, all_4_26, all_4_27, all_4_28, all_4_29, all_4_30, % 252.79/64.07 | all_4_31, all_4_32, all_4_33, all_4_34, all_4_35, all_4_36, all_4_37, % 252.79/64.07 | all_4_38, all_4_39, all_4_40, all_4_41, all_4_42, all_4_43, all_4_44, % 252.79/64.07 | all_4_45, all_4_46, all_4_47, all_4_48, all_4_49, all_4_50, all_4_51, % 252.79/64.07 | all_4_52, all_4_53, all_4_54, all_4_55, all_4_56, all_4_57, all_4_58, % 252.79/64.07 | all_4_59, all_4_60, all_4_61, all_4_62, all_4_63, all_4_64, all_4_65, % 252.79/64.07 | all_4_66, all_4_67, all_4_68, all_4_69, all_4_70, all_4_71, all_4_72, % 252.79/64.07 | all_4_73, all_4_74, all_4_75, all_4_76, all_4_77, all_4_78, all_4_79, % 252.79/64.07 | all_4_80, all_4_81, all_4_82, all_4_83, all_4_84, all_4_85, all_4_86, % 252.79/64.07 | all_4_87, all_4_88, all_4_89, all_4_90, all_4_91, all_4_92, all_4_93, % 252.79/64.07 | all_4_94, all_4_95, all_4_96, all_4_97, all_4_98, all_4_99, all_4_100, % 252.79/64.07 | all_4_101 gives: % 253.04/64.10 | (5) ~ (n10 = n9) & ~ (n10 = n8) & ~ (n10 = n7) & ~ (n10 = n6) & ~ (n10 % 253.04/64.10 | = n5) & ~ (n10 = n4) & ~ (n10 = n3) & ~ (n10 = n2) & ~ (n10 = n1) % 253.04/64.10 | & ~ (n10 = n0) & ~ (n9 = n8) & ~ (n9 = n7) & ~ (n9 = n6) & ~ (n9 = % 253.04/64.10 | n5) & ~ (n9 = n4) & ~ (n9 = n3) & ~ (n9 = n2) & ~ (n9 = n1) & ~ % 253.04/64.10 | (n9 = n0) & ~ (n8 = n7) & ~ (n8 = n6) & ~ (n8 = n5) & ~ (n8 = n4) & % 253.04/64.10 | ~ (n8 = n3) & ~ (n8 = n2) & ~ (n8 = n1) & ~ (n8 = n0) & ~ (n7 = % 253.04/64.10 | n6) & ~ (n7 = n5) & ~ (n7 = n4) & ~ (n7 = n3) & ~ (n7 = n2) & ~ % 253.04/64.10 | (n7 = n1) & ~ (n7 = n0) & ~ (n6 = n5) & ~ (n6 = n4) & ~ (n6 = n3) & % 253.04/64.10 | ~ (n6 = n2) & ~ (n6 = n1) & ~ (n6 = n0) & ~ (n5 = n4) & ~ (n5 = % 253.04/64.10 | n3) & ~ (n5 = n2) & ~ (n5 = n1) & ~ (n5 = n0) & ~ (n4 = n3) & ~ % 253.04/64.10 | (n4 = n2) & ~ (n4 = n1) & ~ (n4 = n0) & ~ (n3 = n2) & ~ (n3 = n1) & % 253.04/64.10 | ~ (n3 = n0) & ~ (n2 = n1) & ~ (n2 = n0) & ~ (n1 = n0) & % 253.04/64.10 | pred(all_4_82) = all_4_4 & pred(all_4_83) = all_4_7 & pred(all_4_84) = % 253.04/64.10 | all_4_12 & pred(all_4_85) = all_4_15 & pred(all_4_86) = all_4_20 & % 253.04/64.10 | pred(all_4_87) = all_4_23 & pred(all_4_88) = all_4_28 & pred(all_4_89) % 253.04/64.10 | = all_4_31 & pred(all_4_90) = all_4_36 & pred(all_4_91) = all_4_39 & % 253.04/64.10 | pred(all_4_92) = all_4_44 & pred(all_4_93) = all_4_47 & pred(all_4_94) % 253.04/64.10 | = all_4_52 & pred(all_4_95) = all_4_55 & pred(all_4_96) = all_4_60 & % 253.04/64.10 | pred(all_4_97) = all_4_63 & pred(all_4_98) = all_4_68 & pred(all_4_99) % 253.04/64.10 | = all_4_71 & pred(all_4_100) = all_4_76 & pred(all_4_101) = all_4_79 & % 253.04/64.10 | pred(n10) = n9 & pred(n9) = n8 & pred(n8) = n7 & pred(n7) = n6 & % 253.04/64.10 | pred(n6) = n5 & pred(n5) = n4 & pred(n4) = n3 & pred(n3) = n2 & % 253.04/64.10 | pred(n2) = n1 & pred(n1) = n0 & pred(n0) = n10 & succ(all_4_82) = % 253.04/64.10 | all_4_6 & succ(all_4_83) = all_4_3 & succ(all_4_84) = all_4_14 & % 253.04/64.10 | succ(all_4_85) = all_4_11 & succ(all_4_86) = all_4_22 & succ(all_4_87) % 253.04/64.10 | = all_4_19 & succ(all_4_88) = all_4_30 & succ(all_4_89) = all_4_27 & % 253.04/64.10 | succ(all_4_90) = all_4_38 & succ(all_4_91) = all_4_35 & succ(all_4_92) % 253.04/64.10 | = all_4_46 & succ(all_4_93) = all_4_43 & succ(all_4_94) = all_4_54 & % 253.04/64.10 | succ(all_4_95) = all_4_51 & succ(all_4_96) = all_4_62 & succ(all_4_97) % 253.04/64.10 | = all_4_59 & succ(all_4_98) = all_4_70 & succ(all_4_99) = all_4_67 & % 253.04/64.10 | succ(all_4_100) = all_4_78 & succ(all_4_101) = all_4_75 & succ(n10) = % 253.04/64.10 | n0 & succ(n9) = n10 & succ(n8) = n9 & succ(n7) = n8 & succ(n6) = n7 & % 253.04/64.10 | succ(n5) = n6 & succ(n4) = n5 & succ(n3) = n4 & succ(n2) = n3 & % 253.04/64.10 | succ(n1) = n2 & succ(n0) = n1 & sum(all_4_1, all_4_0) = all_4_80 & % 253.04/64.10 | sum(all_4_4, all_4_3) = all_4_2 & sum(all_4_4, all_4_6) = all_4_0 & % 253.04/64.10 | sum(all_4_5, all_4_2) = all_4_81 & sum(all_4_7, all_4_3) = all_4_1 & % 253.04/64.10 | sum(all_4_7, all_4_6) = all_4_5 & sum(all_4_9, all_4_8) = all_4_82 & % 253.04/64.10 | sum(all_4_12, all_4_11) = all_4_10 & sum(all_4_12, all_4_14) = all_4_8 % 253.04/64.10 | & sum(all_4_13, all_4_10) = all_4_83 & sum(all_4_15, all_4_11) = % 253.04/64.10 | all_4_9 & sum(all_4_15, all_4_14) = all_4_13 & sum(all_4_17, all_4_16) % 253.04/64.10 | = all_4_84 & sum(all_4_20, all_4_19) = all_4_18 & sum(all_4_20, % 253.04/64.10 | all_4_22) = all_4_16 & sum(all_4_21, all_4_18) = all_4_85 & % 253.04/64.10 | sum(all_4_23, all_4_19) = all_4_17 & sum(all_4_23, all_4_22) = all_4_21 % 253.04/64.10 | & sum(all_4_25, all_4_24) = all_4_86 & sum(all_4_28, all_4_27) = % 253.04/64.10 | all_4_26 & sum(all_4_28, all_4_30) = all_4_24 & sum(all_4_29, all_4_26) % 253.04/64.10 | = all_4_87 & sum(all_4_31, all_4_27) = all_4_25 & sum(all_4_31, % 253.04/64.10 | all_4_30) = all_4_29 & sum(all_4_33, all_4_32) = all_4_88 & % 253.04/64.10 | sum(all_4_36, all_4_35) = all_4_34 & sum(all_4_36, all_4_38) = all_4_32 % 253.04/64.10 | & sum(all_4_37, all_4_34) = all_4_89 & sum(all_4_39, all_4_35) = % 253.04/64.10 | all_4_33 & sum(all_4_39, all_4_38) = all_4_37 & sum(all_4_41, all_4_40) % 253.04/64.10 | = all_4_90 & sum(all_4_44, all_4_43) = all_4_42 & sum(all_4_44, % 253.04/64.10 | all_4_46) = all_4_40 & sum(all_4_45, all_4_42) = all_4_91 & % 253.04/64.10 | sum(all_4_47, all_4_43) = all_4_41 & sum(all_4_47, all_4_46) = all_4_45 % 253.04/64.10 | & sum(all_4_49, all_4_48) = all_4_92 & sum(all_4_52, all_4_51) = % 253.04/64.10 | all_4_50 & sum(all_4_52, all_4_54) = all_4_48 & sum(all_4_53, all_4_50) % 253.04/64.10 | = all_4_93 & sum(all_4_55, all_4_51) = all_4_49 & sum(all_4_55, % 253.04/64.10 | all_4_54) = all_4_53 & sum(all_4_57, all_4_56) = all_4_94 & % 253.04/64.10 | sum(all_4_60, all_4_59) = all_4_58 & sum(all_4_60, all_4_62) = all_4_56 % 253.04/64.10 | & sum(all_4_61, all_4_58) = all_4_95 & sum(all_4_63, all_4_59) = % 253.04/64.10 | all_4_57 & sum(all_4_63, all_4_62) = all_4_61 & sum(all_4_65, all_4_64) % 253.04/64.10 | = all_4_96 & sum(all_4_68, all_4_67) = all_4_66 & sum(all_4_68, % 253.04/64.10 | all_4_70) = all_4_64 & sum(all_4_69, all_4_66) = all_4_97 & % 253.04/64.10 | sum(all_4_71, all_4_67) = all_4_65 & sum(all_4_71, all_4_70) = all_4_69 % 253.04/64.10 | & sum(all_4_73, all_4_72) = all_4_98 & sum(all_4_76, all_4_75) = % 253.04/64.10 | all_4_74 & sum(all_4_76, all_4_78) = all_4_72 & sum(all_4_77, all_4_74) % 253.04/64.10 | = all_4_99 & sum(all_4_79, all_4_75) = all_4_73 & sum(all_4_79, % 253.04/64.10 | all_4_78) = all_4_77 & sum(n10, n10) = n9 & sum(n10, n9) = n8 & % 253.04/64.10 | sum(n10, n8) = n7 & sum(n10, n7) = n6 & sum(n10, n6) = n5 & sum(n10, % 253.04/64.10 | n5) = n4 & sum(n10, n4) = n3 & sum(n10, n3) = n2 & sum(n10, n2) = n1 % 253.04/64.10 | & sum(n10, n1) = n0 & sum(n10, n0) = n10 & sum(n9, n10) = n8 & sum(n9, % 253.04/64.10 | n9) = n7 & sum(n9, n8) = n6 & sum(n9, n7) = n5 & sum(n9, n6) = n4 & % 253.04/64.10 | sum(n9, n5) = n3 & sum(n9, n4) = n2 & sum(n9, n3) = n1 & sum(n9, n2) = % 253.04/64.10 | n0 & sum(n9, n1) = n10 & sum(n9, n0) = n9 & sum(n8, n10) = n7 & sum(n8, % 253.04/64.10 | n9) = n6 & sum(n8, n8) = n5 & sum(n8, n7) = n4 & sum(n8, n6) = n3 & % 253.04/64.10 | sum(n8, n5) = n2 & sum(n8, n4) = n1 & sum(n8, n3) = n0 & sum(n8, n2) = % 253.04/64.10 | n10 & sum(n8, n1) = n9 & sum(n8, n0) = n8 & sum(n7, n10) = n6 & sum(n7, % 253.04/64.10 | n9) = n5 & sum(n7, n8) = n4 & sum(n7, n7) = n3 & sum(n7, n6) = n2 & % 253.04/64.10 | sum(n7, n5) = n1 & sum(n7, n4) = n0 & sum(n7, n3) = n10 & sum(n7, n2) = % 253.04/64.10 | n9 & sum(n7, n1) = n8 & sum(n7, n0) = n7 & sum(n6, n10) = n5 & sum(n6, % 253.04/64.10 | n9) = n4 & sum(n6, n8) = n3 & sum(n6, n7) = n2 & sum(n6, n6) = n1 & % 253.04/64.10 | sum(n6, n5) = n0 & sum(n6, n4) = n10 & sum(n6, n3) = n9 & sum(n6, n2) = % 253.04/64.10 | n8 & sum(n6, n1) = n7 & sum(n6, n0) = n6 & sum(n5, n10) = n4 & sum(n5, % 253.04/64.10 | n9) = n3 & sum(n5, n8) = n2 & sum(n5, n7) = n1 & sum(n5, n6) = n0 & % 253.04/64.10 | sum(n5, n5) = n10 & sum(n5, n4) = n9 & sum(n5, n3) = n8 & sum(n5, n2) = % 253.04/64.10 | n7 & sum(n5, n1) = n6 & sum(n5, n0) = n5 & sum(n4, n10) = n3 & sum(n4, % 253.04/64.10 | n9) = n2 & sum(n4, n8) = n1 & sum(n4, n7) = n0 & sum(n4, n6) = n10 & % 253.04/64.10 | sum(n4, n5) = n9 & sum(n4, n4) = n8 & sum(n4, n3) = n7 & sum(n4, n2) = % 253.04/64.10 | n6 & sum(n4, n1) = n5 & sum(n4, n0) = n4 & sum(n3, n10) = n2 & sum(n3, % 253.04/64.10 | n9) = n1 & sum(n3, n8) = n0 & sum(n3, n7) = n10 & sum(n3, n6) = n9 & % 253.04/64.10 | sum(n3, n5) = n8 & sum(n3, n4) = n7 & sum(n3, n3) = n6 & sum(n3, n2) = % 253.04/64.10 | n5 & sum(n3, n1) = n4 & sum(n3, n0) = n3 & sum(n2, n10) = n1 & sum(n2, % 253.04/64.10 | n9) = n0 & sum(n2, n8) = n10 & sum(n2, n7) = n9 & sum(n2, n6) = n8 & % 253.04/64.10 | sum(n2, n5) = n7 & sum(n2, n4) = n6 & sum(n2, n3) = n5 & sum(n2, n2) = % 253.04/64.10 | n4 & sum(n2, n1) = n3 & sum(n2, n0) = n2 & sum(n1, n10) = n0 & sum(n1, % 253.04/64.10 | n9) = n10 & sum(n1, n8) = n9 & sum(n1, n7) = n8 & sum(n1, n6) = n7 & % 253.04/64.10 | sum(n1, n5) = n6 & sum(n1, n4) = n5 & sum(n1, n3) = n4 & sum(n1, n2) = % 253.04/64.10 | n3 & sum(n1, n1) = n2 & sum(n1, n0) = n1 & sum(n0, n10) = n10 & sum(n0, % 253.04/64.10 | n9) = n9 & sum(n0, n8) = n8 & sum(n0, n7) = n7 & sum(n0, n6) = n6 & % 253.04/64.10 | sum(n0, n5) = n5 & sum(n0, n4) = n4 & sum(n0, n3) = n3 & sum(n0, n2) = % 253.04/64.10 | n2 & sum(n0, n1) = n1 & sum(n0, n0) = n0 & $i(all_4_0) & $i(all_4_1) & % 253.04/64.10 | $i(all_4_2) & $i(all_4_3) & $i(all_4_4) & $i(all_4_5) & $i(all_4_6) & % 253.04/64.10 | $i(all_4_7) & $i(all_4_8) & $i(all_4_9) & $i(all_4_10) & $i(all_4_11) & % 253.04/64.10 | $i(all_4_12) & $i(all_4_13) & $i(all_4_14) & $i(all_4_15) & % 253.04/64.10 | $i(all_4_16) & $i(all_4_17) & $i(all_4_18) & $i(all_4_19) & % 253.04/64.10 | $i(all_4_20) & $i(all_4_21) & $i(all_4_22) & $i(all_4_23) & % 253.04/64.10 | $i(all_4_24) & $i(all_4_25) & $i(all_4_26) & $i(all_4_27) & % 253.04/64.10 | $i(all_4_28) & $i(all_4_29) & $i(all_4_30) & $i(all_4_31) & % 253.04/64.10 | $i(all_4_32) & $i(all_4_33) & $i(all_4_34) & $i(all_4_35) & % 253.04/64.10 | $i(all_4_36) & $i(all_4_37) & $i(all_4_38) & $i(all_4_39) & % 253.04/64.10 | $i(all_4_40) & $i(all_4_41) & $i(all_4_42) & $i(all_4_43) & % 253.04/64.10 | $i(all_4_44) & $i(all_4_45) & $i(all_4_46) & $i(all_4_47) & % 253.04/64.10 | $i(all_4_48) & $i(all_4_49) & $i(all_4_50) & $i(all_4_51) & % 253.04/64.10 | $i(all_4_52) & $i(all_4_53) & $i(all_4_54) & $i(all_4_55) & % 253.04/64.10 | $i(all_4_56) & $i(all_4_57) & $i(all_4_58) & $i(all_4_59) & % 253.04/64.10 | $i(all_4_60) & $i(all_4_61) & $i(all_4_62) & $i(all_4_63) & % 253.04/64.10 | $i(all_4_64) & $i(all_4_65) & $i(all_4_66) & $i(all_4_67) & % 253.04/64.10 | $i(all_4_68) & $i(all_4_69) & $i(all_4_70) & $i(all_4_71) & % 253.04/64.10 | $i(all_4_72) & $i(all_4_73) & $i(all_4_74) & $i(all_4_75) & % 253.04/64.10 | $i(all_4_76) & $i(all_4_77) & $i(all_4_78) & $i(all_4_79) & % 253.04/64.10 | $i(all_4_80) & $i(all_4_81) & $i(all_4_82) & $i(all_4_83) & % 253.04/64.10 | $i(all_4_84) & $i(all_4_85) & $i(all_4_86) & $i(all_4_87) & % 253.04/64.10 | $i(all_4_88) & $i(all_4_89) & $i(all_4_90) & $i(all_4_91) & % 253.04/64.10 | $i(all_4_92) & $i(all_4_93) & $i(all_4_94) & $i(all_4_95) & % 253.04/64.10 | $i(all_4_96) & $i(all_4_97) & $i(all_4_98) & $i(all_4_99) & % 253.04/64.10 | $i(all_4_100) & $i(all_4_101) & ( ~ (all_4_80 = all_4_81) | ~ % 253.04/64.10 | (all_4_82 = all_4_83) | ~ (all_4_84 = all_4_85) | ~ (all_4_86 = % 253.04/64.10 | all_4_87) | ~ (all_4_88 = all_4_89) | ~ (all_4_90 = all_4_91) | % 253.04/64.10 | ~ (all_4_92 = all_4_93) | ~ (all_4_94 = all_4_95) | ~ (all_4_96 = % 253.04/64.10 | all_4_97) | ~ (all_4_98 = all_4_99)) & (all_4_100 = n10 | % 253.04/64.10 | all_4_100 = n9 | all_4_100 = n8 | all_4_100 = n7 | all_4_100 = n6 | % 253.04/64.10 | all_4_100 = n5 | all_4_100 = n4 | all_4_100 = n3 | all_4_100 = n2 | % 253.04/64.10 | all_4_100 = n1 | all_4_100 = n0) &