%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SWV407+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n013.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 : 600s % DateTime : Wed Jul 20 17:51:17 EDT 2022 % Result : Theorem 24.14s 6.41s % Output : Proof 29.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SWV407+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.14 % Command : ePrincess-casc -timeout=%d %s % 0.14/0.36 % Computer : n013.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Wed Jun 15 06:21:14 EDT 2022 % 0.14/0.36 % CPUTime : % 0.68/0.64 ____ _ % 0.68/0.64 ___ / __ \_____(_)___ ________ __________ % 0.68/0.64 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.68/0.64 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.68/0.64 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.68/0.65 % 0.68/0.65 A Theorem Prover for First-Order Logic % 0.68/0.65 (ePrincess v.1.0) % 0.68/0.65 % 0.68/0.65 (c) Philipp Rümmer, 2009-2015 % 0.68/0.65 (c) Peter Backeman, 2014-2015 % 0.68/0.65 (contributions by Angelo Brillout, Peter Baumgartner) % 0.68/0.65 Free software under GNU Lesser General Public License (LGPL). % 0.68/0.65 Bug reports to peter@backeman.se % 0.68/0.65 % 0.68/0.65 For more information, visit http://user.uu.se/~petba168/breu/ % 0.68/0.65 % 0.68/0.65 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.84/0.71 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.85/1.05 Prover 0: Preprocessing ... % 3.37/1.41 Prover 0: Warning: ignoring some quantifiers % 3.37/1.44 Prover 0: Constructing countermodel ... % 7.45/2.40 Prover 0: gave up % 7.45/2.40 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 7.45/2.45 Prover 1: Preprocessing ... % 7.91/2.58 Prover 1: Constructing countermodel ... % 20.46/5.53 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 20.46/5.58 Prover 2: Preprocessing ... % 20.87/5.66 Prover 2: Warning: ignoring some quantifiers % 20.87/5.67 Prover 2: Constructing countermodel ... % 24.14/6.41 Prover 2: proved (874ms) % 24.14/6.41 Prover 1: stopped % 24.14/6.41 % 24.14/6.41 No countermodel exists, formula is valid % 24.14/6.41 % SZS status Theorem for theBenchmark % 24.14/6.41 % 24.14/6.41 Generating proof ... Warning: ignoring some quantifiers % 28.99/7.53 found it (size 514) % 28.99/7.53 % 28.99/7.53 % SZS output start Proof for theBenchmark % 28.99/7.53 Assumed formulas after preprocessing and simplification: % 28.99/7.53 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ( ~ (v0 = 0) & findmin_cpq_res(v4) = v5 & contains_cpq(v4, v7) = 0 & triple(v1, v2, v3) = v4 & check_cpq(v6) = 0 & findmin_cpq_eff(v4) = v6 & isnonempty_slb(create_slb) = v0 & strictly_less_than(v7, v5) = 0 & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : (v15 = 0 | ~ (pair_in_list(v14, v10, v12) = v15) | ~ (pair(v9, v11) = v13) | ~ (insert_slb(v8, v13) = v14) | ? [v16] : ( ~ (v16 = 0) & pair_in_list(v8, v10, v12) = v16)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ( ~ (insert_pqp(v8, v11) = v12) | ~ (triple(v12, v14, v10) = v15) | ~ (pair(v11, bottom) = v13) | ~ (insert_slb(v9, v13) = v14) | ? [v16] : (triple(v8, v9, v10) = v16 & insert_cpq(v16, v11) = v15)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ( ~ (triple(v8, v14, v10) = v15) | ~ (pair(v11, v12) = v13) | ~ (insert_slb(v9, v13) = v14) | ? [v16] : ? [v17] : ? [v18] : (( ~ (v16 = 0) & less_than(v12, v11) = v16) | (((v18 = 0 & triple(v8, v9, v10) = v17 & check_cpq(v17) = 0) | ( ~ (v16 = 0) & check_cpq(v15) = v16)) & ((v16 = 0 & check_cpq(v15) = 0) | ( ~ (v18 = 0) & triple(v8, v9, v10) = v17 & check_cpq(v17) = v18))))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ! [v15] : ( ~ (triple(v8, v14, v10) = v15) | ~ (pair(v11, v12) = v13) | ~ (insert_slb(v9, v13) = v14) | ? [v16] : (( ~ (v16 = 0) & check_cpq(v15) = v16) | ( ~ (v16 = 0) & strictly_less_than(v11, v12) = v16))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v14 = 0 | ~ (triple(v8, v9, v10) = v11) | ~ (less_than(v13, v12) = v14) | ? [v15] : (( ~ (v15 = 0) & check_cpq(v11) = v15) | ( ~ (v15 = 0) & pair_in_list(v9, v12, v13) = v15))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v14 = 0 | ~ (contains_slb(v13, v10) = v14) | ~ (pair(v9, v11) = v12) | ~ (insert_slb(v8, v12) = v13) | ? [v15] : ( ~ (v15 = 0) & contains_slb(v8, v10) = v15)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v12 = v11 | ~ (pair_in_list(v14, v10, v12) = 0) | ~ (pair(v9, v11) = v13) | ~ (insert_slb(v8, v13) = v14) | pair_in_list(v8, v10, v12) = 0) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v10 = v9 | ~ (lookup_slb(v13, v10) = v14) | ~ (pair(v9, v11) = v12) | ~ (insert_slb(v8, v12) = v13) | ? [v15] : ((v15 = v14 & lookup_slb(v8, v10) = v14) | ( ~ (v15 = 0) & contains_slb(v8, v10) = v15))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v10 = v9 | ~ (remove_slb(v13, v10) = v14) | ~ (pair(v9, v11) = v12) | ~ (insert_slb(v8, v12) = v13) | ? [v15] : ? [v16] : ((v16 = v14 & remove_slb(v8, v10) = v15 & insert_slb(v15, v12) = v14) | ( ~ (v15 = 0) & contains_slb(v8, v10) = v15))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v10 = v9 | ~ (remove_slb(v8, v10) = v13) | ~ (pair(v9, v11) = v12) | ~ (insert_slb(v13, v12) = v14) | ? [v15] : ? [v16] : ((v16 = v14 & remove_slb(v15, v10) = v14 & insert_slb(v8, v12) = v15) | ( ~ (v15 = 0) & contains_slb(v8, v10) = v15))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : (v10 = v9 | ~ (pair_in_list(v14, v10, v12) = 0) | ~ (pair(v9, v11) = v13) | ~ (insert_slb(v8, v13) = v14) | pair_in_list(v8, v10, v12) = 0) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (remove_pqp(v8, v11) = v12) | ~ (triple(v12, v13, v10) = v14) | ~ (remove_slb(v9, v11) = v13) | ? [v15] : ? [v16] : ((v16 = v14 & triple(v8, v9, v10) = v15 & remove_cpq(v15, v11) = v14) | ( ~ (v16 = 0) & lookup_slb(v9, v11) = v15 & less_than(v15, v11) = v16) | ( ~ (v15 = 0) & contains_slb(v9, v11) = v15))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (update_slb(v13, v10) = v14) | ~ (pair(v9, v11) = v12) | ~ (insert_slb(v8, v12) = v13) | ? [v15] : ? [v16] : ? [v17] : ((v17 = v14 & update_slb(v8, v10) = v15 & pair(v9, v10) = v16 & insert_slb(v15, v16) = v14) | ( ~ (v15 = 0) & strictly_less_than(v11, v10) = v15))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (update_slb(v13, v10) = v14) | ~ (pair(v9, v11) = v12) | ~ (insert_slb(v8, v12) = v13) | ? [v15] : ? [v16] : ((v16 = v14 & update_slb(v8, v10) = v15 & insert_slb(v15, v12) = v14) | ( ~ (v15 = 0) & less_than(v10, v11) = v15))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (update_slb(v8, v10) = v13) | ~ (pair(v9, v11) = v12) | ~ (insert_slb(v13, v12) = v14) | ? [v15] : ? [v16] : ((v16 = v14 & update_slb(v15, v10) = v14 & insert_slb(v8, v12) = v15) | ( ~ (v15 = 0) & less_than(v10, v11) = v15))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v13 = 0 | ~ (contains_cpq(v12, v11) = v13) | ~ (triple(v8, v9, v10) = v12) | ? [v14] : ( ~ (v14 = 0) & contains_slb(v9, v11) = v14)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v13 = 0 | ~ (pair_in_list(v12, v9, v10) = v13) | ~ (pair(v9, v10) = v11) | ~ (insert_slb(v8, v11) = v12)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v13 = 0 | ~ (contains_slb(v12, v9) = v13) | ~ (pair(v9, v10) = v11) | ~ (insert_slb(v8, v11) = v12)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v10 = v9 | ~ (contains_slb(v13, v10) = 0) | ~ (pair(v9, v11) = v12) | ~ (insert_slb(v8, v12) = v13) | contains_slb(v8, v10) = 0) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : (v9 = create_slb | ~ (findmin_pqp_res(v8) = v11) | ~ (triple(v8, v12, v10) = v13) | ~ (update_slb(v9, v11) = v12) | ? [v14] : ? [v15] : ((v15 = v13 & triple(v8, v9, v10) = v14 & findmin_cpq_eff(v14) = v13) | ( ~ (v15 = 0) & lookup_slb(v9, v11) = v14 & less_than(v14, v11) = v15) | ( ~ (v14 = 0) & contains_slb(v9, v11) = v14))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (findmin_cpq_res(v12) = v13) | ~ (triple(v8, v9, v10) = v12) | ~ (strictly_less_than(v11, v13) = 0) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ((v18 = 0 & v17 = 0 & findmin_pqp_res(v8) = v14 & update_slb(v9, v14) = v15 & pair_in_list(v15, v11, v16) = 0 & less_than(v14, v16) = 0) | (v16 = 0 & findmin_pqp_res(v8) = v14 & update_slb(v9, v14) = v15 & pair_in_list(v15, v11, v14) = 0) | ( ~ (v14 = 0) & contains_slb(v9, v11) = v14))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (triple(v8, v9, v10) = v12) | ~ (remove_cpq(v12, v11) = v13) | ? [v14] : ? [v15] : ? [v16] : ((v16 = v13 & remove_pqp(v8, v11) = v14 & triple(v14, v15, v10) = v13 & remove_slb(v9, v11) = v15) | ( ~ (v15 = 0) & lookup_slb(v9, v11) = v14 & less_than(v14, v11) = v15) | ( ~ (v14 = 0) & contains_slb(v9, v11) = v14))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (triple(v8, v9, v10) = v12) | ~ (remove_cpq(v12, v11) = v13) | ? [v14] : ? [v15] : ? [v16] : ((v16 = v13 & remove_pqp(v8, v11) = v14 & triple(v14, v15, bad) = v13 & remove_slb(v9, v11) = v15) | ( ~ (v15 = 0) & lookup_slb(v9, v11) = v14 & strictly_less_than(v11, v14) = v15) | ( ~ (v14 = 0) & contains_slb(v9, v11) = v14))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (triple(v8, v9, v10) = v12) | ~ (remove_cpq(v12, v11) = v13) | ? [v14] : ((v14 = v13 & triple(v8, v9, bad) = v13) | (v14 = 0 & contains_slb(v9, v11) = 0))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (triple(v8, v9, v10) = v12) | ~ (insert_cpq(v12, v11) = v13) | ? [v14] : ? [v15] : ? [v16] : (insert_pqp(v8, v11) = v14 & triple(v14, v16, v10) = v13 & pair(v11, bottom) = v15 & insert_slb(v9, v15) = v16)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (triple(v8, v9, v10) = v11) | ~ (pair_in_list(v9, v12, v13) = 0) | ? [v14] : ((v14 = 0 & less_than(v13, v12) = 0) | ( ~ (v14 = 0) & check_cpq(v11) = v14))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (remove_cpq(v9, v10) = v11) | ~ (succ_cpq(v8, v11) = v12) | ? [v13] : ( ~ (v13 = 0) & succ_cpq(v8, v9) = v13)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = 0 | ~ (insert_cpq(v9, v10) = v11) | ~ (succ_cpq(v8, v11) = v12) | ? [v13] : ( ~ (v13 = 0) & succ_cpq(v8, v9) = v13)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v9 = v8 | ~ (triple(v12, v11, v10) = v9) | ~ (triple(v12, v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v9 = v8 | ~ (pair_in_list(v12, v11, v10) = v9) | ~ (pair_in_list(v12, v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v9 = create_slb | ~ (findmin_cpq_res(v11) = v12) | ~ (triple(v8, v9, v10) = v11) | findmin_pqp_res(v8) = v12) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v9 = create_slb | ~ (triple(v8, v9, v10) = v11) | ~ (findmin_cpq_eff(v11) = v12) | ? [v13] : ? [v14] : ? [v15] : (findmin_pqp_res(v8) = v13 & ((v15 = v12 & triple(v8, v14, v10) = v12 & update_slb(v9, v13) = v14) | ( ~ (v15 = 0) & lookup_slb(v9, v13) = v14 & less_than(v14, v13) = v15) | ( ~ (v14 = 0) & contains_slb(v9, v13) = v14)))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v9 = create_slb | ~ (triple(v8, v9, v10) = v11) | ~ (findmin_cpq_eff(v11) = v12) | ? [v13] : ? [v14] : ? [v15] : (findmin_pqp_res(v8) = v13 & ((v15 = v12 & triple(v8, v14, bad) = v12 & update_slb(v9, v13) = v14) | (v14 = 0 & contains_slb(v9, v13) = 0)))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v9 = create_slb | ~ (triple(v8, v9, v10) = v11) | ~ (findmin_cpq_eff(v11) = v12) | ? [v13] : ? [v14] : ? [v15] : (findmin_pqp_res(v8) = v13 & ((v15 = v12 & triple(v8, v14, bad) = v12 & update_slb(v9, v13) = v14) | ( ~ (v15 = 0) & lookup_slb(v9, v13) = v14 & strictly_less_than(v13, v14) = v15) | ( ~ (v14 = 0) & contains_slb(v9, v13) = v14)))) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (contains_cpq(v12, v11) = 0) | ~ (triple(v8, v9, v10) = v12) | contains_slb(v9, v11) = 0) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (pair(v9, v10) = v11) | ~ (insert_slb(v8, v11) = v12) | lookup_slb(v12, v9) = v10) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (pair(v9, v10) = v11) | ~ (insert_slb(v8, v11) = v12) | remove_slb(v12, v9) = v8) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (pair(v9, v10) = v11) | ~ (insert_slb(v8, v11) = v12) | isnonempty_slb(v12) = 0) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (removemin_cpq_eff(v9) = v10) | ~ (succ_cpq(v8, v10) = v11) | ? [v12] : ( ~ (v12 = 0) & succ_cpq(v8, v9) = v12)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (findmin_cpq_eff(v9) = v10) | ~ (succ_cpq(v8, v10) = v11) | ? [v12] : ( ~ (v12 = 0) & succ_cpq(v8, v9) = v12)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (less_than(v9, v10) = 0) | ~ (less_than(v8, v10) = v11) | ? [v12] : ( ~ (v12 = 0) & less_than(v8, v9) = v12)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v11 = 0 | ~ (less_than(v8, v10) = v11) | ~ (less_than(v8, v9) = 0) | ? [v12] : ( ~ (v12 = 0) & less_than(v9, v10) = v12)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v10 = bad | ~ (triple(v8, v9, v10) = v11) | ok(v11) = 0) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (remove_pqp(v11, v10) = v9) | ~ (remove_pqp(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (insert_pqp(v11, v10) = v9) | ~ (insert_pqp(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (contains_cpq(v11, v10) = v9) | ~ (contains_cpq(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (remove_cpq(v11, v10) = v9) | ~ (remove_cpq(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (insert_cpq(v11, v10) = v9) | ~ (insert_cpq(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (succ_cpq(v11, v10) = v9) | ~ (succ_cpq(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (update_slb(v11, v10) = v9) | ~ (update_slb(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (lookup_slb(v11, v10) = v9) | ~ (lookup_slb(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (remove_slb(v11, v10) = v9) | ~ (remove_slb(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (contains_slb(v11, v10) = v9) | ~ (contains_slb(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (pair(v11, v10) = v9) | ~ (pair(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (insert_slb(v11, v10) = v9) | ~ (insert_slb(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (strictly_less_than(v11, v10) = v9) | ~ (strictly_less_than(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : (v9 = v8 | ~ (less_than(v11, v10) = v9) | ~ (less_than(v11, v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ! [v11] : ( ~ (triple(v8, v9, v10) = v11) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : ((v14 = 0 & ~ (v15 = 0) & pair_in_list(v9, v12, v13) = 0 & less_than(v13, v12) = v15) | (v12 = 0 & check_cpq(v11) = 0))) & ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (strictly_less_than(v8, v9) = v10) | ? [v11] : ((v11 = 0 & less_than(v9, v8) = 0) | ( ~ (v11 = 0) & less_than(v8, v9) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (less_than(v9, v8) = v10) | less_than(v8, v9) = 0) & ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (less_than(v9, v8) = v10) | ? [v11] : ((v11 = 0 & strictly_less_than(v8, v9) = 0) | ( ~ (v11 = 0) & less_than(v8, v9) = v11))) & ! [v8] : ! [v9] : ! [v10] : (v10 = 0 | ~ (less_than(v8, v9) = v10) | less_than(v9, v8) = 0) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (removemin_cpq_res(v10) = v9) | ~ (removemin_cpq_res(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (findmin_cpq_res(v10) = v9) | ~ (findmin_cpq_res(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (findmin_pqp_res(v10) = v9) | ~ (findmin_pqp_res(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (ok(v10) = v9) | ~ (ok(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (check_cpq(v10) = v9) | ~ (check_cpq(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (removemin_cpq_eff(v10) = v9) | ~ (removemin_cpq_eff(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (findmin_cpq_eff(v10) = v9) | ~ (findmin_cpq_eff(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : (v9 = v8 | ~ (isnonempty_slb(v10) = v9) | ~ (isnonempty_slb(v10) = v8)) & ! [v8] : ! [v9] : ! [v10] : ( ~ (triple(v8, v9, bad) = v10) | ? [v11] : ( ~ (v11 = 0) & ok(v10) = v11)) & ! [v8] : ! [v9] : ! [v10] : ( ~ (triple(v8, create_slb, v9) = v10) | findmin_cpq_res(v10) = bottom) & ! [v8] : ! [v9] : ! [v10] : ( ~ (triple(v8, create_slb, v9) = v10) | check_cpq(v10) = 0) & ! [v8] : ! [v9] : ! [v10] : ( ~ (triple(v8, create_slb, v9) = v10) | ? [v11] : (triple(v8, create_slb, bad) = v11 & findmin_cpq_eff(v10) = v11)) & ! [v8] : ! [v9] : ! [v10] : ( ~ (less_than(v9, v10) = 0) | ~ (less_than(v8, v9) = 0) | less_than(v8, v10) = 0) & ! [v8] : ! [v9] : ! [v10] : ( ~ (less_than(v9, v8) = v10) | ? [v11] : ((v11 = 0 & ~ (v10 = 0) & less_than(v8, v9) = 0) | ( ~ (v11 = 0) & strictly_less_than(v8, v9) = v11))) & ! [v8] : ! [v9] : ! [v10] : ( ~ (less_than(v8, v9) = v10) | ? [v11] : ((v10 = 0 & ~ (v11 = 0) & less_than(v9, v8) = v11) | ( ~ (v11 = 0) & strictly_less_than(v8, v9) = v11))) & ! [v8] : ! [v9] : (v9 = create_slb | ~ (update_slb(create_slb, v8) = v9)) & ! [v8] : ! [v9] : (v9 = 0 | ~ (succ_cpq(v8, v8) = v9)) & ! [v8] : ! [v9] : (v9 = 0 | ~ (less_than(v8, v8) = v9)) & ! [v8] : ! [v9] : (v9 = 0 | ~ (less_than(bottom, v8) = v9)) & ! [v8] : ! [v9] : ( ~ (removemin_cpq_res(v8) = v9) | findmin_cpq_res(v8) = v9) & ! [v8] : ! [v9] : ( ~ (findmin_cpq_res(v8) = v9) | removemin_cpq_res(v8) = v9) & ! [v8] : ! [v9] : ( ~ (findmin_cpq_res(v8) = v9) | ? [v10] : ? [v11] : (removemin_cpq_eff(v8) = v10 & findmin_cpq_eff(v8) = v11 & remove_cpq(v11, v9) = v10)) & ! [v8] : ! [v9] : ( ~ (removemin_cpq_eff(v8) = v9) | ? [v10] : ? [v11] : (findmin_cpq_res(v8) = v11 & findmin_cpq_eff(v8) = v10 & remove_cpq(v10, v11) = v9)) & ! [v8] : ! [v9] : ( ~ (findmin_cpq_eff(v8) = v9) | ? [v10] : ? [v11] : (findmin_cpq_res(v8) = v11 & removemin_cpq_eff(v8) = v10 & remove_cpq(v9, v11) = v10)) & ! [v8] : ! [v9] : ( ~ (succ_cpq(v8, v9) = 0) | ? [v10] : (removemin_cpq_eff(v9) = v10 & succ_cpq(v8, v10) = 0)) & ! [v8] : ! [v9] : ( ~ (succ_cpq(v8, v9) = 0) | ? [v10] : (findmin_cpq_eff(v9) = v10 & succ_cpq(v8, v10) = 0)) & ! [v8] : ! [v9] : ~ (pair_in_list(create_slb, v8, v9) = 0) & ! [v8] : ! [v9] : ( ~ (strictly_less_than(v8, v9) = 0) | ? [v10] : ( ~ (v10 = 0) & less_than(v9, v8) = v10 & less_than(v8, v9) = 0)) & ! [v8] : ! [v9] : ( ~ (less_than(v8, v9) = 0) | ? [v10] : ((v10 = 0 & strictly_less_than(v8, v9) = 0) | (v10 = 0 & less_than(v9, v8) = 0))) & ! [v8] : ~ (contains_slb(create_slb, v8) = 0) & ? [v8] : ? [v9] : ? [v10] : ? [v11] : triple(v10, v9, v8) = v11 & ? [v8] : ? [v9] : ? [v10] : ? [v11] : pair_in_list(v10, v9, v8) = v11 & ? [v8] : ? [v9] : ? [v10] : remove_pqp(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : insert_pqp(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : contains_cpq(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : remove_cpq(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : insert_cpq(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : succ_cpq(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : update_slb(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : lookup_slb(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : remove_slb(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : contains_slb(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : pair(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : insert_slb(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : strictly_less_than(v9, v8) = v10 & ? [v8] : ? [v9] : ? [v10] : less_than(v9, v8) = v10 & ? [v8] : ? [v9] : removemin_cpq_res(v8) = v9 & ? [v8] : ? [v9] : findmin_cpq_res(v8) = v9 & ? [v8] : ? [v9] : findmin_pqp_res(v8) = v9 & ? [v8] : ? [v9] : ok(v8) = v9 & ? [v8] : ? [v9] : check_cpq(v8) = v9 & ? [v8] : ? [v9] : removemin_cpq_eff(v8) = v9 & ? [v8] : ? [v9] : findmin_cpq_eff(v8) = v9 & ? [v8] : ? [v9] : isnonempty_slb(v8) = v9) % 29.26/7.61 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7 yields: % 29.26/7.61 | (1) ~ (all_0_7_7 = 0) & findmin_cpq_res(all_0_3_3) = all_0_2_2 & contains_cpq(all_0_3_3, all_0_0_0) = 0 & triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3 & check_cpq(all_0_1_1) = 0 & findmin_cpq_eff(all_0_3_3) = all_0_1_1 & isnonempty_slb(create_slb) = all_0_7_7 & strictly_less_than(all_0_0_0, all_0_2_2) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (pair_in_list(v6, v2, v4) = v7) | ~ (pair(v1, v3) = v5) | ~ (insert_slb(v0, v5) = v6) | ? [v8] : ( ~ (v8 = 0) & pair_in_list(v0, v2, v4) = v8)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (insert_pqp(v0, v3) = v4) | ~ (triple(v4, v6, v2) = v7) | ~ (pair(v3, bottom) = v5) | ~ (insert_slb(v1, v5) = v6) | ? [v8] : (triple(v0, v1, v2) = v8 & insert_cpq(v8, v3) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (triple(v0, v6, v2) = v7) | ~ (pair(v3, v4) = v5) | ~ (insert_slb(v1, v5) = v6) | ? [v8] : ? [v9] : ? [v10] : (( ~ (v8 = 0) & less_than(v4, v3) = v8) | (((v10 = 0 & triple(v0, v1, v2) = v9 & check_cpq(v9) = 0) | ( ~ (v8 = 0) & check_cpq(v7) = v8)) & ((v8 = 0 & check_cpq(v7) = 0) | ( ~ (v10 = 0) & triple(v0, v1, v2) = v9 & check_cpq(v9) = v10))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (triple(v0, v6, v2) = v7) | ~ (pair(v3, v4) = v5) | ~ (insert_slb(v1, v5) = v6) | ? [v8] : (( ~ (v8 = 0) & check_cpq(v7) = v8) | ( ~ (v8 = 0) & strictly_less_than(v3, v4) = v8))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (triple(v0, v1, v2) = v3) | ~ (less_than(v5, v4) = v6) | ? [v7] : (( ~ (v7 = 0) & check_cpq(v3) = v7) | ( ~ (v7 = 0) & pair_in_list(v1, v4, v5) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (contains_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ( ~ (v7 = 0) & contains_slb(v0, v2) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (pair_in_list(v6, v2, v4) = 0) | ~ (pair(v1, v3) = v5) | ~ (insert_slb(v0, v5) = v6) | pair_in_list(v0, v2, v4) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v2 = v1 | ~ (lookup_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ((v7 = v6 & lookup_slb(v0, v2) = v6) | ( ~ (v7 = 0) & contains_slb(v0, v2) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v2 = v1 | ~ (remove_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ? [v8] : ((v8 = v6 & remove_slb(v0, v2) = v7 & insert_slb(v7, v4) = v6) | ( ~ (v7 = 0) & contains_slb(v0, v2) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v2 = v1 | ~ (remove_slb(v0, v2) = v5) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v5, v4) = v6) | ? [v7] : ? [v8] : ((v8 = v6 & remove_slb(v7, v2) = v6 & insert_slb(v0, v4) = v7) | ( ~ (v7 = 0) & contains_slb(v0, v2) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v2 = v1 | ~ (pair_in_list(v6, v2, v4) = 0) | ~ (pair(v1, v3) = v5) | ~ (insert_slb(v0, v5) = v6) | pair_in_list(v0, v2, v4) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (remove_pqp(v0, v3) = v4) | ~ (triple(v4, v5, v2) = v6) | ~ (remove_slb(v1, v3) = v5) | ? [v7] : ? [v8] : ((v8 = v6 & triple(v0, v1, v2) = v7 & remove_cpq(v7, v3) = v6) | ( ~ (v8 = 0) & lookup_slb(v1, v3) = v7 & less_than(v7, v3) = v8) | ( ~ (v7 = 0) & contains_slb(v1, v3) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (update_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ? [v8] : ? [v9] : ((v9 = v6 & update_slb(v0, v2) = v7 & pair(v1, v2) = v8 & insert_slb(v7, v8) = v6) | ( ~ (v7 = 0) & strictly_less_than(v3, v2) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (update_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ? [v8] : ((v8 = v6 & update_slb(v0, v2) = v7 & insert_slb(v7, v4) = v6) | ( ~ (v7 = 0) & less_than(v2, v3) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (update_slb(v0, v2) = v5) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v5, v4) = v6) | ? [v7] : ? [v8] : ((v8 = v6 & update_slb(v7, v2) = v6 & insert_slb(v0, v4) = v7) | ( ~ (v7 = 0) & less_than(v2, v3) = v7))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (contains_cpq(v4, v3) = v5) | ~ (triple(v0, v1, v2) = v4) | ? [v6] : ( ~ (v6 = 0) & contains_slb(v1, v3) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (pair_in_list(v4, v1, v2) = v5) | ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (contains_slb(v4, v1) = v5) | ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v2 = v1 | ~ (contains_slb(v5, v2) = 0) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | contains_slb(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = create_slb | ~ (findmin_pqp_res(v0) = v3) | ~ (triple(v0, v4, v2) = v5) | ~ (update_slb(v1, v3) = v4) | ? [v6] : ? [v7] : ((v7 = v5 & triple(v0, v1, v2) = v6 & findmin_cpq_eff(v6) = v5) | ( ~ (v7 = 0) & lookup_slb(v1, v3) = v6 & less_than(v6, v3) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v3) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (findmin_cpq_res(v4) = v5) | ~ (triple(v0, v1, v2) = v4) | ~ (strictly_less_than(v3, v5) = 0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ((v10 = 0 & v9 = 0 & findmin_pqp_res(v0) = v6 & update_slb(v1, v6) = v7 & pair_in_list(v7, v3, v8) = 0 & less_than(v6, v8) = 0) | (v8 = 0 & findmin_pqp_res(v0) = v6 & update_slb(v1, v6) = v7 & pair_in_list(v7, v3, v6) = 0) | ( ~ (v6 = 0) & contains_slb(v1, v3) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v4) | ~ (remove_cpq(v4, v3) = v5) | ? [v6] : ? [v7] : ? [v8] : ((v8 = v5 & remove_pqp(v0, v3) = v6 & triple(v6, v7, v2) = v5 & remove_slb(v1, v3) = v7) | ( ~ (v7 = 0) & lookup_slb(v1, v3) = v6 & less_than(v6, v3) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v3) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v4) | ~ (remove_cpq(v4, v3) = v5) | ? [v6] : ? [v7] : ? [v8] : ((v8 = v5 & remove_pqp(v0, v3) = v6 & triple(v6, v7, bad) = v5 & remove_slb(v1, v3) = v7) | ( ~ (v7 = 0) & lookup_slb(v1, v3) = v6 & strictly_less_than(v3, v6) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v3) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v4) | ~ (remove_cpq(v4, v3) = v5) | ? [v6] : ((v6 = v5 & triple(v0, v1, bad) = v5) | (v6 = 0 & contains_slb(v1, v3) = 0))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v4) | ~ (insert_cpq(v4, v3) = v5) | ? [v6] : ? [v7] : ? [v8] : (insert_pqp(v0, v3) = v6 & triple(v6, v8, v2) = v5 & pair(v3, bottom) = v7 & insert_slb(v1, v7) = v8)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v3) | ~ (pair_in_list(v1, v4, v5) = 0) | ? [v6] : ((v6 = 0 & less_than(v5, v4) = 0) | ( ~ (v6 = 0) & check_cpq(v3) = v6))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (remove_cpq(v1, v2) = v3) | ~ (succ_cpq(v0, v3) = v4) | ? [v5] : ( ~ (v5 = 0) & succ_cpq(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (insert_cpq(v1, v2) = v3) | ~ (succ_cpq(v0, v3) = v4) | ? [v5] : ( ~ (v5 = 0) & succ_cpq(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (triple(v4, v3, v2) = v1) | ~ (triple(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (pair_in_list(v4, v3, v2) = v1) | ~ (pair_in_list(v4, v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (findmin_cpq_res(v3) = v4) | ~ (triple(v0, v1, v2) = v3) | findmin_pqp_res(v0) = v4) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ (findmin_cpq_eff(v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (findmin_pqp_res(v0) = v5 & ((v7 = v4 & triple(v0, v6, v2) = v4 & update_slb(v1, v5) = v6) | ( ~ (v7 = 0) & lookup_slb(v1, v5) = v6 & less_than(v6, v5) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v5) = v6)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ (findmin_cpq_eff(v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (findmin_pqp_res(v0) = v5 & ((v7 = v4 & triple(v0, v6, bad) = v4 & update_slb(v1, v5) = v6) | (v6 = 0 & contains_slb(v1, v5) = 0)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ (findmin_cpq_eff(v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (findmin_pqp_res(v0) = v5 & ((v7 = v4 & triple(v0, v6, bad) = v4 & update_slb(v1, v5) = v6) | ( ~ (v7 = 0) & lookup_slb(v1, v5) = v6 & strictly_less_than(v5, v6) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v5) = v6)))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (contains_cpq(v4, v3) = 0) | ~ (triple(v0, v1, v2) = v4) | contains_slb(v1, v3) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | lookup_slb(v4, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | remove_slb(v4, v1) = v0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | isnonempty_slb(v4) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (removemin_cpq_eff(v1) = v2) | ~ (succ_cpq(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & succ_cpq(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (findmin_cpq_eff(v1) = v2) | ~ (succ_cpq(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & succ_cpq(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (less_than(v1, v2) = 0) | ~ (less_than(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & less_than(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (less_than(v0, v2) = v3) | ~ (less_than(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & less_than(v1, v2) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = bad | ~ (triple(v0, v1, v2) = v3) | ok(v3) = 0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_pqp(v3, v2) = v1) | ~ (remove_pqp(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_pqp(v3, v2) = v1) | ~ (insert_pqp(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (contains_cpq(v3, v2) = v1) | ~ (contains_cpq(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_cpq(v3, v2) = v1) | ~ (remove_cpq(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_cpq(v3, v2) = v1) | ~ (insert_cpq(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (succ_cpq(v3, v2) = v1) | ~ (succ_cpq(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (update_slb(v3, v2) = v1) | ~ (update_slb(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (lookup_slb(v3, v2) = v1) | ~ (lookup_slb(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_slb(v3, v2) = v1) | ~ (remove_slb(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (contains_slb(v3, v2) = v1) | ~ (contains_slb(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (pair(v3, v2) = v1) | ~ (pair(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_slb(v3, v2) = v1) | ~ (insert_slb(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (strictly_less_than(v3, v2) = v1) | ~ (strictly_less_than(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (less_than(v3, v2) = v1) | ~ (less_than(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (triple(v0, v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ((v6 = 0 & ~ (v7 = 0) & pair_in_list(v1, v4, v5) = 0 & less_than(v5, v4) = v7) | (v4 = 0 & check_cpq(v3) = 0))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (strictly_less_than(v0, v1) = v2) | ? [v3] : ((v3 = 0 & less_than(v1, v0) = 0) | ( ~ (v3 = 0) & less_than(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | less_than(v0, v1) = 0) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | ? [v3] : ((v3 = 0 & strictly_less_than(v0, v1) = 0) | ( ~ (v3 = 0) & less_than(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v0, v1) = v2) | less_than(v1, v0) = 0) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (removemin_cpq_res(v2) = v1) | ~ (removemin_cpq_res(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_cpq_res(v2) = v1) | ~ (findmin_cpq_res(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_pqp_res(v2) = v1) | ~ (findmin_pqp_res(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ok(v2) = v1) | ~ (ok(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (check_cpq(v2) = v1) | ~ (check_cpq(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (removemin_cpq_eff(v2) = v1) | ~ (removemin_cpq_eff(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_cpq_eff(v2) = v1) | ~ (findmin_cpq_eff(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isnonempty_slb(v2) = v1) | ~ (isnonempty_slb(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, v1, bad) = v2) | ? [v3] : ( ~ (v3 = 0) & ok(v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | findmin_cpq_res(v2) = bottom) & ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | check_cpq(v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | ? [v3] : (triple(v0, create_slb, bad) = v3 & findmin_cpq_eff(v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (less_than(v1, v2) = 0) | ~ (less_than(v0, v1) = 0) | less_than(v0, v2) = 0) & ! [v0] : ! [v1] : ! [v2] : ( ~ (less_than(v1, v0) = v2) | ? [v3] : ((v3 = 0 & ~ (v2 = 0) & less_than(v0, v1) = 0) | ( ~ (v3 = 0) & strictly_less_than(v0, v1) = v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (less_than(v0, v1) = v2) | ? [v3] : ((v2 = 0 & ~ (v3 = 0) & less_than(v1, v0) = v3) | ( ~ (v3 = 0) & strictly_less_than(v0, v1) = v3))) & ! [v0] : ! [v1] : (v1 = create_slb | ~ (update_slb(create_slb, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (succ_cpq(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_than(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (less_than(bottom, v0) = v1)) & ! [v0] : ! [v1] : ( ~ (removemin_cpq_res(v0) = v1) | findmin_cpq_res(v0) = v1) & ! [v0] : ! [v1] : ( ~ (findmin_cpq_res(v0) = v1) | removemin_cpq_res(v0) = v1) & ! [v0] : ! [v1] : ( ~ (findmin_cpq_res(v0) = v1) | ? [v2] : ? [v3] : (removemin_cpq_eff(v0) = v2 & findmin_cpq_eff(v0) = v3 & remove_cpq(v3, v1) = v2)) & ! [v0] : ! [v1] : ( ~ (removemin_cpq_eff(v0) = v1) | ? [v2] : ? [v3] : (findmin_cpq_res(v0) = v3 & findmin_cpq_eff(v0) = v2 & remove_cpq(v2, v3) = v1)) & ! [v0] : ! [v1] : ( ~ (findmin_cpq_eff(v0) = v1) | ? [v2] : ? [v3] : (findmin_cpq_res(v0) = v3 & removemin_cpq_eff(v0) = v2 & remove_cpq(v1, v3) = v2)) & ! [v0] : ! [v1] : ( ~ (succ_cpq(v0, v1) = 0) | ? [v2] : (removemin_cpq_eff(v1) = v2 & succ_cpq(v0, v2) = 0)) & ! [v0] : ! [v1] : ( ~ (succ_cpq(v0, v1) = 0) | ? [v2] : (findmin_cpq_eff(v1) = v2 & succ_cpq(v0, v2) = 0)) & ! [v0] : ! [v1] : ~ (pair_in_list(create_slb, v0, v1) = 0) & ! [v0] : ! [v1] : ( ~ (strictly_less_than(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & less_than(v1, v0) = v2 & less_than(v0, v1) = 0)) & ! [v0] : ! [v1] : ( ~ (less_than(v0, v1) = 0) | ? [v2] : ((v2 = 0 & strictly_less_than(v0, v1) = 0) | (v2 = 0 & less_than(v1, v0) = 0))) & ! [v0] : ~ (contains_slb(create_slb, v0) = 0) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : triple(v2, v1, v0) = v3 & ? [v0] : ? [v1] : ? [v2] : ? [v3] : pair_in_list(v2, v1, v0) = v3 & ? [v0] : ? [v1] : ? [v2] : remove_pqp(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : insert_pqp(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : contains_cpq(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : remove_cpq(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : insert_cpq(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : succ_cpq(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : update_slb(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : lookup_slb(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : remove_slb(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : contains_slb(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : pair(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : insert_slb(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : strictly_less_than(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : less_than(v1, v0) = v2 & ? [v0] : ? [v1] : removemin_cpq_res(v0) = v1 & ? [v0] : ? [v1] : findmin_cpq_res(v0) = v1 & ? [v0] : ? [v1] : findmin_pqp_res(v0) = v1 & ? [v0] : ? [v1] : ok(v0) = v1 & ? [v0] : ? [v1] : check_cpq(v0) = v1 & ? [v0] : ? [v1] : removemin_cpq_eff(v0) = v1 & ? [v0] : ? [v1] : findmin_cpq_eff(v0) = v1 & ? [v0] : ? [v1] : isnonempty_slb(v0) = v1 % 29.26/7.64 | % 29.26/7.64 | Applying alpha-rule on (1) yields: % 29.26/7.64 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (remove_pqp(v0, v3) = v4) | ~ (triple(v4, v5, v2) = v6) | ~ (remove_slb(v1, v3) = v5) | ? [v7] : ? [v8] : ((v8 = v6 & triple(v0, v1, v2) = v7 & remove_cpq(v7, v3) = v6) | ( ~ (v8 = 0) & lookup_slb(v1, v3) = v7 & less_than(v7, v3) = v8) | ( ~ (v7 = 0) & contains_slb(v1, v3) = v7))) % 29.26/7.64 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = bad | ~ (triple(v0, v1, v2) = v3) | ok(v3) = 0) % 29.26/7.64 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v4 = v3 | ~ (pair_in_list(v6, v2, v4) = 0) | ~ (pair(v1, v3) = v5) | ~ (insert_slb(v0, v5) = v6) | pair_in_list(v0, v2, v4) = 0) % 29.26/7.64 | (5) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (removemin_cpq_eff(v2) = v1) | ~ (removemin_cpq_eff(v2) = v0)) % 29.26/7.64 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (update_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ? [v8] : ? [v9] : ((v9 = v6 & update_slb(v0, v2) = v7 & pair(v1, v2) = v8 & insert_slb(v7, v8) = v6) | ( ~ (v7 = 0) & strictly_less_than(v3, v2) = v7))) % 29.26/7.64 | (7) ? [v0] : ? [v1] : ? [v2] : succ_cpq(v1, v0) = v2 % 29.26/7.64 | (8) ! [v0] : ! [v1] : ! [v2] : ( ~ (less_than(v0, v1) = v2) | ? [v3] : ((v2 = 0 & ~ (v3 = 0) & less_than(v1, v0) = v3) | ( ~ (v3 = 0) & strictly_less_than(v0, v1) = v3))) % 29.26/7.64 | (9) ! [v0] : ! [v1] : ( ~ (findmin_cpq_res(v0) = v1) | removemin_cpq_res(v0) = v1) % 29.26/7.64 | (10) ! [v0] : ! [v1] : ( ~ (removemin_cpq_res(v0) = v1) | findmin_cpq_res(v0) = v1) % 29.26/7.64 | (11) ! [v0] : ! [v1] : (v1 = 0 | ~ (succ_cpq(v0, v0) = v1)) % 29.26/7.64 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | lookup_slb(v4, v1) = v2) % 29.26/7.64 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (check_cpq(v2) = v1) | ~ (check_cpq(v2) = v0)) % 29.26/7.64 | (14) ? [v0] : ? [v1] : findmin_cpq_res(v0) = v1 % 29.26/7.64 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (less_than(v3, v2) = v1) | ~ (less_than(v3, v2) = v0)) % 29.26/7.64 | (16) ? [v0] : ? [v1] : ? [v2] : ? [v3] : pair_in_list(v2, v1, v0) = v3 % 29.26/7.64 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (contains_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ( ~ (v7 = 0) & contains_slb(v0, v2) = v7)) % 29.26/7.64 | (18) ! [v0] : ! [v1] : (v1 = create_slb | ~ (update_slb(create_slb, v0) = v1)) % 29.26/7.64 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v3) | ~ (pair_in_list(v1, v4, v5) = 0) | ? [v6] : ((v6 = 0 & less_than(v5, v4) = 0) | ( ~ (v6 = 0) & check_cpq(v3) = v6))) % 29.26/7.64 | (20) ? [v0] : ? [v1] : removemin_cpq_res(v0) = v1 % 29.26/7.64 | (21) ? [v0] : ? [v1] : ? [v2] : strictly_less_than(v1, v0) = v2 % 29.26/7.64 | (22) ? [v0] : ? [v1] : isnonempty_slb(v0) = v1 % 29.26/7.64 | (23) ! [v0] : ! [v1] : ( ~ (succ_cpq(v0, v1) = 0) | ? [v2] : (removemin_cpq_eff(v1) = v2 & succ_cpq(v0, v2) = 0)) % 29.26/7.64 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | check_cpq(v2) = 0) % 29.26/7.64 | (25) ! [v0] : ~ (contains_slb(create_slb, v0) = 0) % 29.26/7.64 | (26) ? [v0] : ? [v1] : ? [v2] : insert_cpq(v1, v0) = v2 % 29.26/7.64 | (27) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v0, v1) = v2) | less_than(v1, v0) = 0) % 29.26/7.64 | (28) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | less_than(v0, v1) = 0) % 29.26/7.64 | (29) findmin_cpq_eff(all_0_3_3) = all_0_1_1 % 29.26/7.64 | (30) ? [v0] : ? [v1] : ? [v2] : contains_cpq(v1, v0) = v2 % 29.26/7.64 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v1 = create_slb | ~ (findmin_pqp_res(v0) = v3) | ~ (triple(v0, v4, v2) = v5) | ~ (update_slb(v1, v3) = v4) | ? [v6] : ? [v7] : ((v7 = v5 & triple(v0, v1, v2) = v6 & findmin_cpq_eff(v6) = v5) | ( ~ (v7 = 0) & lookup_slb(v1, v3) = v6 & less_than(v6, v3) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v3) = v6))) % 29.26/7.64 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | remove_slb(v4, v1) = v0) % 29.26/7.64 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_cpq(v3, v2) = v1) | ~ (remove_cpq(v3, v2) = v0)) % 29.26/7.64 | (34) ? [v0] : ? [v1] : ? [v2] : less_than(v1, v0) = v2 % 29.26/7.64 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v2 = v1 | ~ (pair_in_list(v6, v2, v4) = 0) | ~ (pair(v1, v3) = v5) | ~ (insert_slb(v0, v5) = v6) | pair_in_list(v0, v2, v4) = 0) % 29.26/7.65 | (36) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_than(v0, v0) = v1)) % 29.26/7.65 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (less_than(v1, v2) = 0) | ~ (less_than(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & less_than(v0, v1) = v4)) % 29.26/7.65 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (update_slb(v0, v2) = v5) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v5, v4) = v6) | ? [v7] : ? [v8] : ((v8 = v6 & update_slb(v7, v2) = v6 & insert_slb(v0, v4) = v7) | ( ~ (v7 = 0) & less_than(v2, v3) = v7))) % 29.26/7.65 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v2 = v1 | ~ (lookup_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ((v7 = v6 & lookup_slb(v0, v2) = v6) | ( ~ (v7 = 0) & contains_slb(v0, v2) = v7))) % 29.26/7.65 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v2 = v1 | ~ (remove_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ? [v8] : ((v8 = v6 & remove_slb(v0, v2) = v7 & insert_slb(v7, v4) = v6) | ( ~ (v7 = 0) & contains_slb(v0, v2) = v7))) % 29.26/7.65 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v6 = 0 | ~ (triple(v0, v1, v2) = v3) | ~ (less_than(v5, v4) = v6) | ? [v7] : (( ~ (v7 = 0) & check_cpq(v3) = v7) | ( ~ (v7 = 0) & pair_in_list(v1, v4, v5) = v7))) % 29.26/7.65 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v4) | ~ (remove_cpq(v4, v3) = v5) | ? [v6] : ? [v7] : ? [v8] : ((v8 = v5 & remove_pqp(v0, v3) = v6 & triple(v6, v7, bad) = v5 & remove_slb(v1, v3) = v7) | ( ~ (v7 = 0) & lookup_slb(v1, v3) = v6 & strictly_less_than(v3, v6) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v3) = v6))) % 29.26/7.65 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (insert_pqp(v0, v3) = v4) | ~ (triple(v4, v6, v2) = v7) | ~ (pair(v3, bottom) = v5) | ~ (insert_slb(v1, v5) = v6) | ? [v8] : (triple(v0, v1, v2) = v8 & insert_cpq(v8, v3) = v7)) % 29.26/7.65 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (less_than(v0, v2) = v3) | ~ (less_than(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & less_than(v1, v2) = v4)) % 29.26/7.65 | (45) isnonempty_slb(create_slb) = all_0_7_7 % 29.26/7.65 | (46) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (contains_slb(v3, v2) = v1) | ~ (contains_slb(v3, v2) = v0)) % 29.26/7.65 | (47) ? [v0] : ? [v1] : ? [v2] : remove_slb(v1, v0) = v2 % 29.26/7.65 | (48) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_cpq_res(v2) = v1) | ~ (findmin_cpq_res(v2) = v0)) % 29.26/7.65 | (49) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, v1, bad) = v2) | ? [v3] : ( ~ (v3 = 0) & ok(v2) = v3)) % 29.26/7.65 | (50) ? [v0] : ? [v1] : ? [v2] : update_slb(v1, v0) = v2 % 29.26/7.65 | (51) ! [v0] : ! [v1] : ( ~ (succ_cpq(v0, v1) = 0) | ? [v2] : (findmin_cpq_eff(v1) = v2 & succ_cpq(v0, v2) = 0)) % 29.26/7.65 | (52) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_pqp_res(v2) = v1) | ~ (findmin_pqp_res(v2) = v0)) % 29.26/7.65 | (53) ! [v0] : ! [v1] : ~ (pair_in_list(create_slb, v0, v1) = 0) % 29.26/7.65 | (54) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (triple(v0, v6, v2) = v7) | ~ (pair(v3, v4) = v5) | ~ (insert_slb(v1, v5) = v6) | ? [v8] : ? [v9] : ? [v10] : (( ~ (v8 = 0) & less_than(v4, v3) = v8) | (((v10 = 0 & triple(v0, v1, v2) = v9 & check_cpq(v9) = 0) | ( ~ (v8 = 0) & check_cpq(v7) = v8)) & ((v8 = 0 & check_cpq(v7) = 0) | ( ~ (v10 = 0) & triple(v0, v1, v2) = v9 & check_cpq(v9) = v10))))) % 29.26/7.65 | (55) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (lookup_slb(v3, v2) = v1) | ~ (lookup_slb(v3, v2) = v0)) % 29.26/7.65 | (56) findmin_cpq_res(all_0_3_3) = all_0_2_2 % 29.26/7.65 | (57) contains_cpq(all_0_3_3, all_0_0_0) = 0 % 29.26/7.65 | (58) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (update_slb(v3, v2) = v1) | ~ (update_slb(v3, v2) = v0)) % 29.26/7.65 | (59) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (contains_slb(v4, v1) = v5) | ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4)) % 29.26/7.65 | (60) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_slb(v3, v2) = v1) | ~ (remove_slb(v3, v2) = v0)) % 29.26/7.65 | (61) ? [v0] : ? [v1] : ? [v2] : pair(v1, v0) = v2 % 29.26/7.65 | (62) ! [v0] : ! [v1] : ( ~ (findmin_cpq_eff(v0) = v1) | ? [v2] : ? [v3] : (findmin_cpq_res(v0) = v3 & removemin_cpq_eff(v0) = v2 & remove_cpq(v1, v3) = v2)) % 29.26/7.65 | (63) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = 0 | ~ (pair_in_list(v6, v2, v4) = v7) | ~ (pair(v1, v3) = v5) | ~ (insert_slb(v0, v5) = v6) | ? [v8] : ( ~ (v8 = 0) & pair_in_list(v0, v2, v4) = v8)) % 29.26/7.65 | (64) ? [v0] : ? [v1] : ? [v2] : insert_slb(v1, v0) = v2 % 29.26/7.65 | (65) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ (findmin_cpq_eff(v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (findmin_pqp_res(v0) = v5 & ((v7 = v4 & triple(v0, v6, bad) = v4 & update_slb(v1, v5) = v6) | ( ~ (v7 = 0) & lookup_slb(v1, v5) = v6 & strictly_less_than(v5, v6) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v5) = v6)))) % 29.26/7.66 | (66) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_pqp(v3, v2) = v1) | ~ (insert_pqp(v3, v2) = v0)) % 29.26/7.66 | (67) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ok(v2) = v1) | ~ (ok(v2) = v0)) % 29.26/7.66 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (triple(v0, v1, v2) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ((v6 = 0 & ~ (v7 = 0) & pair_in_list(v1, v4, v5) = 0 & less_than(v5, v4) = v7) | (v4 = 0 & check_cpq(v3) = 0))) % 29.26/7.66 | (69) ? [v0] : ? [v1] : findmin_pqp_res(v0) = v1 % 29.26/7.66 | (70) check_cpq(all_0_1_1) = 0 % 29.26/7.66 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v4) | ~ (remove_cpq(v4, v3) = v5) | ? [v6] : ((v6 = v5 & triple(v0, v1, bad) = v5) | (v6 = 0 & contains_slb(v1, v3) = 0))) % 29.26/7.66 | (72) ? [v0] : ? [v1] : ? [v2] : remove_pqp(v1, v0) = v2 % 29.26/7.66 | (73) ? [v0] : ? [v1] : ? [v2] : contains_slb(v1, v0) = v2 % 29.26/7.66 | (74) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | ? [v3] : ((v3 = 0 & strictly_less_than(v0, v1) = 0) | ( ~ (v3 = 0) & less_than(v0, v1) = v3))) % 29.26/7.66 | (75) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (contains_cpq(v4, v3) = v5) | ~ (triple(v0, v1, v2) = v4) | ? [v6] : ( ~ (v6 = 0) & contains_slb(v1, v3) = v6)) % 29.26/7.66 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (pair(v3, v2) = v1) | ~ (pair(v3, v2) = v0)) % 29.26/7.66 | (77) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (contains_cpq(v3, v2) = v1) | ~ (contains_cpq(v3, v2) = v0)) % 29.26/7.66 | (78) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (findmin_cpq_res(v4) = v5) | ~ (triple(v0, v1, v2) = v4) | ~ (strictly_less_than(v3, v5) = 0) | ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ((v10 = 0 & v9 = 0 & findmin_pqp_res(v0) = v6 & update_slb(v1, v6) = v7 & pair_in_list(v7, v3, v8) = 0 & less_than(v6, v8) = 0) | (v8 = 0 & findmin_pqp_res(v0) = v6 & update_slb(v1, v6) = v7 & pair_in_list(v7, v3, v6) = 0) | ( ~ (v6 = 0) & contains_slb(v1, v3) = v6))) % 29.26/7.66 | (79) ! [v0] : ! [v1] : ( ~ (strictly_less_than(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & less_than(v1, v0) = v2 & less_than(v0, v1) = 0)) % 29.26/7.66 | (80) ? [v0] : ? [v1] : check_cpq(v0) = v1 % 29.26/7.66 | (81) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_slb(v3, v2) = v1) | ~ (insert_slb(v3, v2) = v0)) % 29.26/7.66 | (82) ? [v0] : ? [v1] : ok(v0) = v1 % 29.26/7.66 | (83) ! [v0] : ! [v1] : ( ~ (findmin_cpq_res(v0) = v1) | ? [v2] : ? [v3] : (removemin_cpq_eff(v0) = v2 & findmin_cpq_eff(v0) = v3 & remove_cpq(v3, v1) = v2)) % 29.26/7.66 | (84) ! [v0] : ! [v1] : ( ~ (removemin_cpq_eff(v0) = v1) | ? [v2] : ? [v3] : (findmin_cpq_res(v0) = v3 & findmin_cpq_eff(v0) = v2 & remove_cpq(v2, v3) = v1)) % 29.26/7.66 | (85) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ( ~ (update_slb(v5, v2) = v6) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | ? [v7] : ? [v8] : ((v8 = v6 & update_slb(v0, v2) = v7 & insert_slb(v7, v4) = v6) | ( ~ (v7 = 0) & less_than(v2, v3) = v7))) % 29.26/7.66 | (86) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (removemin_cpq_eff(v1) = v2) | ~ (succ_cpq(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & succ_cpq(v0, v1) = v4)) % 29.26/7.66 | (87) strictly_less_than(all_0_0_0, all_0_2_2) = 0 % 29.26/7.66 | (88) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | ? [v3] : (triple(v0, create_slb, bad) = v3 & findmin_cpq_eff(v2) = v3)) % 29.26/7.66 | (89) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (contains_cpq(v4, v3) = 0) | ~ (triple(v0, v1, v2) = v4) | contains_slb(v1, v3) = 0) % 29.26/7.66 | (90) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v2 = v1 | ~ (contains_slb(v5, v2) = 0) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v0, v4) = v5) | contains_slb(v0, v2) = 0) % 29.26/7.66 | (91) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (pair_in_list(v4, v3, v2) = v1) | ~ (pair_in_list(v4, v3, v2) = v0)) % 29.26/7.66 | (92) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (triple(v4, v3, v2) = v1) | ~ (triple(v4, v3, v2) = v0)) % 29.26/7.66 | (93) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (strictly_less_than(v3, v2) = v1) | ~ (strictly_less_than(v3, v2) = v0)) % 29.26/7.66 | (94) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | findmin_cpq_res(v2) = bottom) % 29.26/7.66 | (95) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (removemin_cpq_res(v2) = v1) | ~ (removemin_cpq_res(v2) = v0)) % 29.26/7.66 | (96) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v4) | ~ (remove_cpq(v4, v3) = v5) | ? [v6] : ? [v7] : ? [v8] : ((v8 = v5 & remove_pqp(v0, v3) = v6 & triple(v6, v7, v2) = v5 & remove_slb(v1, v3) = v7) | ( ~ (v7 = 0) & lookup_slb(v1, v3) = v6 & less_than(v6, v3) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v3) = v6))) % 29.26/7.66 | (97) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ (triple(v0, v6, v2) = v7) | ~ (pair(v3, v4) = v5) | ~ (insert_slb(v1, v5) = v6) | ? [v8] : (( ~ (v8 = 0) & check_cpq(v7) = v8) | ( ~ (v8 = 0) & strictly_less_than(v3, v4) = v8))) % 29.26/7.66 | (98) ! [v0] : ! [v1] : ! [v2] : ( ~ (less_than(v1, v2) = 0) | ~ (less_than(v0, v1) = 0) | less_than(v0, v2) = 0) % 29.26/7.67 | (99) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | isnonempty_slb(v4) = 0) % 29.26/7.67 | (100) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (triple(v0, v1, v2) = v4) | ~ (insert_cpq(v4, v3) = v5) | ? [v6] : ? [v7] : ? [v8] : (insert_pqp(v0, v3) = v6 & triple(v6, v8, v2) = v5 & pair(v3, bottom) = v7 & insert_slb(v1, v7) = v8)) % 29.26/7.67 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_cpq(v3, v2) = v1) | ~ (insert_cpq(v3, v2) = v0)) % 29.26/7.67 | (102) ? [v0] : ? [v1] : ? [v2] : lookup_slb(v1, v0) = v2 % 29.26/7.67 | (103) ? [v0] : ? [v1] : ? [v2] : remove_cpq(v1, v0) = v2 % 29.26/7.67 | (104) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ! [v6] : (v2 = v1 | ~ (remove_slb(v0, v2) = v5) | ~ (pair(v1, v3) = v4) | ~ (insert_slb(v5, v4) = v6) | ? [v7] : ? [v8] : ((v8 = v6 & remove_slb(v7, v2) = v6 & insert_slb(v0, v4) = v7) | ( ~ (v7 = 0) & contains_slb(v0, v2) = v7))) % 29.26/7.67 | (105) ! [v0] : ! [v1] : ( ~ (less_than(v0, v1) = 0) | ? [v2] : ((v2 = 0 & strictly_less_than(v0, v1) = 0) | (v2 = 0 & less_than(v1, v0) = 0))) % 29.26/7.67 | (106) ? [v0] : ? [v1] : removemin_cpq_eff(v0) = v1 % 29.26/7.67 | (107) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ (findmin_cpq_eff(v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (findmin_pqp_res(v0) = v5 & ((v7 = v4 & triple(v0, v6, v2) = v4 & update_slb(v1, v5) = v6) | ( ~ (v7 = 0) & lookup_slb(v1, v5) = v6 & less_than(v6, v5) = v7) | ( ~ (v6 = 0) & contains_slb(v1, v5) = v6)))) % 29.26/7.67 | (108) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (triple(v0, v1, v2) = v3) | ~ (findmin_cpq_eff(v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (findmin_pqp_res(v0) = v5 & ((v7 = v4 & triple(v0, v6, bad) = v4 & update_slb(v1, v5) = v6) | (v6 = 0 & contains_slb(v1, v5) = 0)))) % 29.26/7.67 | (109) ! [v0] : ! [v1] : ! [v2] : ( ~ (less_than(v1, v0) = v2) | ? [v3] : ((v3 = 0 & ~ (v2 = 0) & less_than(v0, v1) = 0) | ( ~ (v3 = 0) & strictly_less_than(v0, v1) = v3))) % 29.26/7.67 | (110) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_than(bottom, v0) = v1)) % 29.26/7.67 | (111) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_pqp(v3, v2) = v1) | ~ (remove_pqp(v3, v2) = v0)) % 29.26/7.67 | (112) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (pair_in_list(v4, v1, v2) = v5) | ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4)) % 29.26/7.67 | (113) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (strictly_less_than(v0, v1) = v2) | ? [v3] : ((v3 = 0 & less_than(v1, v0) = 0) | ( ~ (v3 = 0) & less_than(v0, v1) = v3))) % 29.26/7.67 | (114) ? [v0] : ? [v1] : findmin_cpq_eff(v0) = v1 % 29.26/7.67 | (115) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (remove_cpq(v1, v2) = v3) | ~ (succ_cpq(v0, v3) = v4) | ? [v5] : ( ~ (v5 = 0) & succ_cpq(v0, v1) = v5)) % 29.26/7.67 | (116) ? [v0] : ? [v1] : ? [v2] : insert_pqp(v1, v0) = v2 % 29.26/7.67 | (117) ~ (all_0_7_7 = 0) % 29.26/7.67 | (118) triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3 % 29.26/7.67 | (119) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (findmin_cpq_eff(v1) = v2) | ~ (succ_cpq(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & succ_cpq(v0, v1) = v4)) % 29.26/7.67 | (120) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_cpq_eff(v2) = v1) | ~ (findmin_cpq_eff(v2) = v0)) % 29.26/7.67 | (121) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v4 = 0 | ~ (insert_cpq(v1, v2) = v3) | ~ (succ_cpq(v0, v3) = v4) | ? [v5] : ( ~ (v5 = 0) & succ_cpq(v0, v1) = v5)) % 29.26/7.67 | (122) ? [v0] : ? [v1] : ? [v2] : ? [v3] : triple(v2, v1, v0) = v3 % 29.26/7.67 | (123) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (findmin_cpq_res(v3) = v4) | ~ (triple(v0, v1, v2) = v3) | findmin_pqp_res(v0) = v4) % 29.26/7.67 | (124) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isnonempty_slb(v2) = v1) | ~ (isnonempty_slb(v2) = v0)) % 29.26/7.67 | (125) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (succ_cpq(v3, v2) = v1) | ~ (succ_cpq(v3, v2) = v0)) % 29.26/7.67 | % 29.26/7.67 | Instantiating formula (89) with all_0_3_3, all_0_0_0, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms contains_cpq(all_0_3_3, all_0_0_0) = 0, triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, yields: % 29.26/7.67 | (126) contains_slb(all_0_5_5, all_0_0_0) = 0 % 29.26/7.67 | % 29.26/7.67 | Instantiating formula (123) with all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms findmin_cpq_res(all_0_3_3) = all_0_2_2, triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, yields: % 29.26/7.67 | (127) all_0_5_5 = create_slb | findmin_pqp_res(all_0_6_6) = all_0_2_2 % 29.26/7.67 | % 29.26/7.67 | Instantiating formula (107) with all_0_1_1, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, findmin_cpq_eff(all_0_3_3) = all_0_1_1, yields: % 29.26/7.67 | (128) all_0_5_5 = create_slb | ? [v0] : ? [v1] : ? [v2] : (findmin_pqp_res(all_0_6_6) = v0 & ((v2 = all_0_1_1 & triple(all_0_6_6, v1, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, v0) = v1) | ( ~ (v2 = 0) & lookup_slb(all_0_5_5, v0) = v1 & less_than(v1, v0) = v2) | ( ~ (v1 = 0) & contains_slb(all_0_5_5, v0) = v1))) % 29.26/7.67 | % 29.26/7.67 | Instantiating formula (108) with all_0_1_1, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, findmin_cpq_eff(all_0_3_3) = all_0_1_1, yields: % 29.26/7.67 | (129) all_0_5_5 = create_slb | ? [v0] : ? [v1] : ? [v2] : (findmin_pqp_res(all_0_6_6) = v0 & ((v2 = all_0_1_1 & triple(all_0_6_6, v1, bad) = all_0_1_1 & update_slb(all_0_5_5, v0) = v1) | (v1 = 0 & contains_slb(all_0_5_5, v0) = 0))) % 29.26/7.67 | % 29.26/7.67 | Instantiating formula (65) with all_0_1_1, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, findmin_cpq_eff(all_0_3_3) = all_0_1_1, yields: % 29.26/7.67 | (130) all_0_5_5 = create_slb | ? [v0] : ? [v1] : ? [v2] : (findmin_pqp_res(all_0_6_6) = v0 & ((v2 = all_0_1_1 & triple(all_0_6_6, v1, bad) = all_0_1_1 & update_slb(all_0_5_5, v0) = v1) | ( ~ (v2 = 0) & lookup_slb(all_0_5_5, v0) = v1 & strictly_less_than(v0, v1) = v2) | ( ~ (v1 = 0) & contains_slb(all_0_5_5, v0) = v1))) % 29.26/7.68 | % 29.26/7.68 | Instantiating formula (78) with all_0_2_2, all_0_3_3, all_0_0_0, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms findmin_cpq_res(all_0_3_3) = all_0_2_2, triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, strictly_less_than(all_0_0_0, all_0_2_2) = 0, yields: % 29.26/7.68 | (131) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & findmin_pqp_res(all_0_6_6) = v0 & update_slb(all_0_5_5, v0) = v1 & pair_in_list(v1, all_0_0_0, v2) = 0 & less_than(v0, v2) = 0) | (v2 = 0 & findmin_pqp_res(all_0_6_6) = v0 & update_slb(all_0_5_5, v0) = v1 & pair_in_list(v1, all_0_0_0, v0) = 0) | ( ~ (v0 = 0) & contains_slb(all_0_5_5, all_0_0_0) = v0)) % 29.26/7.68 | % 29.26/7.68 | Instantiating formula (79) with all_0_2_2, all_0_0_0 and discharging atoms strictly_less_than(all_0_0_0, all_0_2_2) = 0, yields: % 29.26/7.68 | (132) ? [v0] : ( ~ (v0 = 0) & less_than(all_0_0_0, all_0_2_2) = 0 & less_than(all_0_2_2, all_0_0_0) = v0) % 29.26/7.68 | % 29.26/7.68 | Instantiating (132) with all_57_0_74 yields: % 29.26/7.68 | (133) ~ (all_57_0_74 = 0) & less_than(all_0_0_0, all_0_2_2) = 0 & less_than(all_0_2_2, all_0_0_0) = all_57_0_74 % 29.26/7.68 | % 29.26/7.68 | Applying alpha-rule on (133) yields: % 29.26/7.68 | (134) ~ (all_57_0_74 = 0) % 29.26/7.68 | (135) less_than(all_0_0_0, all_0_2_2) = 0 % 29.26/7.68 | (136) less_than(all_0_2_2, all_0_0_0) = all_57_0_74 % 29.26/7.68 | % 29.26/7.68 | Instantiating (131) with all_61_0_77, all_61_1_78, all_61_2_79, all_61_3_80, all_61_4_81 yields: % 29.26/7.68 | (137) (all_61_0_77 = 0 & all_61_1_78 = 0 & findmin_pqp_res(all_0_6_6) = all_61_4_81 & update_slb(all_0_5_5, all_61_4_81) = all_61_3_80 & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = 0 & less_than(all_61_4_81, all_61_2_79) = 0) | (all_61_2_79 = 0 & findmin_pqp_res(all_0_6_6) = all_61_4_81 & update_slb(all_0_5_5, all_61_4_81) = all_61_3_80 & pair_in_list(all_61_3_80, all_0_0_0, all_61_4_81) = 0) | ( ~ (all_61_4_81 = 0) & contains_slb(all_0_5_5, all_0_0_0) = all_61_4_81) % 29.26/7.68 | % 29.26/7.68 | Instantiating formula (109) with 0, all_0_0_0, all_0_2_2 and discharging atoms less_than(all_0_0_0, all_0_2_2) = 0, yields: % 29.26/7.68 | (138) ? [v0] : ( ~ (v0 = 0) & strictly_less_than(all_0_2_2, all_0_0_0) = v0) % 29.26/7.68 | % 29.26/7.68 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.26/7.68 | (139) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_3_3) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_5_5, all_0_0_0, all_0_2_2) = v0)) % 29.26/7.68 | % 29.26/7.68 | Instantiating formula (8) with all_57_0_74, all_0_0_0, all_0_2_2 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.26/7.68 | (140) ? [v0] : ((all_57_0_74 = 0 & ~ (v0 = 0) & less_than(all_0_0_0, all_0_2_2) = v0) | ( ~ (v0 = 0) & strictly_less_than(all_0_2_2, all_0_0_0) = v0)) % 29.26/7.68 | % 29.26/7.68 | Instantiating (140) with all_74_0_88 yields: % 29.26/7.68 | (141) (all_57_0_74 = 0 & ~ (all_74_0_88 = 0) & less_than(all_0_0_0, all_0_2_2) = all_74_0_88) | ( ~ (all_74_0_88 = 0) & strictly_less_than(all_0_2_2, all_0_0_0) = all_74_0_88) % 29.26/7.68 | % 29.26/7.68 | Instantiating (138) with all_75_0_89 yields: % 29.26/7.68 | (142) ~ (all_75_0_89 = 0) & strictly_less_than(all_0_2_2, all_0_0_0) = all_75_0_89 % 29.26/7.68 | % 29.26/7.68 | Applying alpha-rule on (142) yields: % 29.26/7.68 | (143) ~ (all_75_0_89 = 0) % 29.26/7.68 | (144) strictly_less_than(all_0_2_2, all_0_0_0) = all_75_0_89 % 29.26/7.68 | % 29.26/7.68 +-Applying beta-rule and splitting (141), into two cases. % 29.26/7.68 |-Branch one: % 29.26/7.68 | (145) all_57_0_74 = 0 & ~ (all_74_0_88 = 0) & less_than(all_0_0_0, all_0_2_2) = all_74_0_88 % 29.26/7.68 | % 29.26/7.68 | Applying alpha-rule on (145) yields: % 29.26/7.68 | (146) all_57_0_74 = 0 % 29.26/7.68 | (147) ~ (all_74_0_88 = 0) % 29.26/7.68 | (148) less_than(all_0_0_0, all_0_2_2) = all_74_0_88 % 29.26/7.68 | % 29.26/7.68 | Equations (146) can reduce 134 to: % 29.26/7.68 | (149) $false % 29.26/7.68 | % 29.71/7.68 |-The branch is then unsatisfiable % 29.71/7.68 |-Branch two: % 29.71/7.68 | (150) ~ (all_74_0_88 = 0) & strictly_less_than(all_0_2_2, all_0_0_0) = all_74_0_88 % 29.71/7.69 | % 29.71/7.69 | Applying alpha-rule on (150) yields: % 29.71/7.69 | (147) ~ (all_74_0_88 = 0) % 29.71/7.69 | (152) strictly_less_than(all_0_2_2, all_0_0_0) = all_74_0_88 % 29.71/7.69 | % 29.71/7.69 +-Applying beta-rule and splitting (139), into two cases. % 29.71/7.69 |-Branch one: % 29.71/7.69 | (146) all_57_0_74 = 0 % 29.71/7.69 | % 29.71/7.69 | Equations (146) can reduce 134 to: % 29.71/7.69 | (149) $false % 29.71/7.69 | % 29.71/7.69 |-The branch is then unsatisfiable % 29.71/7.69 |-Branch two: % 29.71/7.69 | (134) ~ (all_57_0_74 = 0) % 29.71/7.69 | (156) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_3_3) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_5_5, all_0_0_0, all_0_2_2) = v0)) % 29.71/7.69 | % 29.71/7.69 | Instantiating formula (93) with all_0_2_2, all_0_0_0, all_74_0_88, all_75_0_89 and discharging atoms strictly_less_than(all_0_2_2, all_0_0_0) = all_75_0_89, strictly_less_than(all_0_2_2, all_0_0_0) = all_74_0_88, yields: % 29.71/7.69 | (157) all_75_0_89 = all_74_0_88 % 29.71/7.69 | % 29.71/7.69 | Equations (157) can reduce 143 to: % 29.71/7.69 | (147) ~ (all_74_0_88 = 0) % 29.71/7.69 | % 29.71/7.69 | From (157) and (144) follows: % 29.71/7.69 | (152) strictly_less_than(all_0_2_2, all_0_0_0) = all_74_0_88 % 29.71/7.69 | % 29.71/7.69 | Instantiating formula (113) with all_74_0_88, all_0_0_0, all_0_2_2 and discharging atoms strictly_less_than(all_0_2_2, all_0_0_0) = all_74_0_88, yields: % 29.71/7.69 | (160) all_74_0_88 = 0 | ? [v0] : ((v0 = 0 & less_than(all_0_0_0, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_0_0_0) = v0)) % 29.71/7.69 | % 29.71/7.69 +-Applying beta-rule and splitting (127), into two cases. % 29.71/7.69 |-Branch one: % 29.71/7.69 | (161) findmin_pqp_res(all_0_6_6) = all_0_2_2 % 29.71/7.69 | % 29.71/7.69 +-Applying beta-rule and splitting (160), into two cases. % 29.71/7.69 |-Branch one: % 29.71/7.69 | (162) all_74_0_88 = 0 % 29.71/7.69 | % 29.71/7.69 | Equations (162) can reduce 147 to: % 29.71/7.69 | (149) $false % 29.71/7.69 | % 29.71/7.69 |-The branch is then unsatisfiable % 29.71/7.69 |-Branch two: % 29.71/7.69 | (147) ~ (all_74_0_88 = 0) % 29.71/7.69 | (165) ? [v0] : ((v0 = 0 & less_than(all_0_0_0, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_0_0_0) = v0)) % 29.71/7.69 | % 29.71/7.69 | Instantiating (165) with all_101_0_91 yields: % 29.71/7.69 | (166) (all_101_0_91 = 0 & less_than(all_0_0_0, all_0_2_2) = 0) | ( ~ (all_101_0_91 = 0) & less_than(all_0_2_2, all_0_0_0) = all_101_0_91) % 29.71/7.69 | % 29.71/7.69 +-Applying beta-rule and splitting (130), into two cases. % 29.71/7.69 |-Branch one: % 29.71/7.69 | (167) all_0_5_5 = create_slb % 29.71/7.69 | % 29.71/7.69 | From (167) and (126) follows: % 29.71/7.69 | (168) contains_slb(create_slb, all_0_0_0) = 0 % 29.71/7.69 | % 29.71/7.69 | Instantiating formula (25) with all_0_0_0 and discharging atoms contains_slb(create_slb, all_0_0_0) = 0, yields: % 29.71/7.69 | (169) $false % 29.71/7.69 | % 29.71/7.69 |-The branch is then unsatisfiable % 29.71/7.69 |-Branch two: % 29.71/7.69 | (170) ~ (all_0_5_5 = create_slb) % 29.71/7.69 | (171) ? [v0] : ? [v1] : ? [v2] : (findmin_pqp_res(all_0_6_6) = v0 & ((v2 = all_0_1_1 & triple(all_0_6_6, v1, bad) = all_0_1_1 & update_slb(all_0_5_5, v0) = v1) | ( ~ (v2 = 0) & lookup_slb(all_0_5_5, v0) = v1 & strictly_less_than(v0, v1) = v2) | ( ~ (v1 = 0) & contains_slb(all_0_5_5, v0) = v1))) % 29.71/7.69 | % 29.71/7.69 | Instantiating (171) with all_109_0_92, all_109_1_93, all_109_2_94 yields: % 29.71/7.69 | (172) findmin_pqp_res(all_0_6_6) = all_109_2_94 & ((all_109_0_92 = all_0_1_1 & triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 & update_slb(all_0_5_5, all_109_2_94) = all_109_1_93) | ( ~ (all_109_0_92 = 0) & lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 & strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92) | ( ~ (all_109_1_93 = 0) & contains_slb(all_0_5_5, all_109_2_94) = all_109_1_93)) % 29.71/7.69 | % 29.71/7.69 | Applying alpha-rule on (172) yields: % 29.71/7.69 | (173) findmin_pqp_res(all_0_6_6) = all_109_2_94 % 29.71/7.69 | (174) (all_109_0_92 = all_0_1_1 & triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 & update_slb(all_0_5_5, all_109_2_94) = all_109_1_93) | ( ~ (all_109_0_92 = 0) & lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 & strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92) | ( ~ (all_109_1_93 = 0) & contains_slb(all_0_5_5, all_109_2_94) = all_109_1_93) % 29.71/7.69 | % 29.71/7.69 +-Applying beta-rule and splitting (128), into two cases. % 29.71/7.69 |-Branch one: % 29.71/7.69 | (167) all_0_5_5 = create_slb % 29.71/7.69 | % 29.71/7.69 | Equations (167) can reduce 170 to: % 29.71/7.69 | (149) $false % 29.71/7.69 | % 29.71/7.69 |-The branch is then unsatisfiable % 29.71/7.69 |-Branch two: % 29.71/7.69 | (170) ~ (all_0_5_5 = create_slb) % 29.71/7.69 | (178) ? [v0] : ? [v1] : ? [v2] : (findmin_pqp_res(all_0_6_6) = v0 & ((v2 = all_0_1_1 & triple(all_0_6_6, v1, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, v0) = v1) | ( ~ (v2 = 0) & lookup_slb(all_0_5_5, v0) = v1 & less_than(v1, v0) = v2) | ( ~ (v1 = 0) & contains_slb(all_0_5_5, v0) = v1))) % 29.71/7.69 | % 29.71/7.69 | Instantiating (178) with all_115_0_95, all_115_1_96, all_115_2_97 yields: % 29.71/7.69 | (179) findmin_pqp_res(all_0_6_6) = all_115_2_97 & ((all_115_0_95 = all_0_1_1 & triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, all_115_2_97) = all_115_1_96) | ( ~ (all_115_0_95 = 0) & lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 & less_than(all_115_1_96, all_115_2_97) = all_115_0_95) | ( ~ (all_115_1_96 = 0) & contains_slb(all_0_5_5, all_115_2_97) = all_115_1_96)) % 29.71/7.70 | % 29.71/7.70 | Applying alpha-rule on (179) yields: % 29.71/7.70 | (180) findmin_pqp_res(all_0_6_6) = all_115_2_97 % 29.71/7.70 | (181) (all_115_0_95 = all_0_1_1 & triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, all_115_2_97) = all_115_1_96) | ( ~ (all_115_0_95 = 0) & lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 & less_than(all_115_1_96, all_115_2_97) = all_115_0_95) | ( ~ (all_115_1_96 = 0) & contains_slb(all_0_5_5, all_115_2_97) = all_115_1_96) % 29.71/7.70 | % 29.71/7.70 +-Applying beta-rule and splitting (129), into two cases. % 29.71/7.70 |-Branch one: % 29.71/7.70 | (167) all_0_5_5 = create_slb % 29.71/7.70 | % 29.71/7.70 | Equations (167) can reduce 170 to: % 29.71/7.70 | (149) $false % 29.71/7.70 | % 29.71/7.70 |-The branch is then unsatisfiable % 29.71/7.70 |-Branch two: % 29.71/7.70 | (170) ~ (all_0_5_5 = create_slb) % 29.71/7.70 | (185) ? [v0] : ? [v1] : ? [v2] : (findmin_pqp_res(all_0_6_6) = v0 & ((v2 = all_0_1_1 & triple(all_0_6_6, v1, bad) = all_0_1_1 & update_slb(all_0_5_5, v0) = v1) | (v1 = 0 & contains_slb(all_0_5_5, v0) = 0))) % 29.71/7.70 | % 29.71/7.70 | Instantiating (185) with all_120_0_98, all_120_1_99, all_120_2_100 yields: % 29.71/7.70 | (186) findmin_pqp_res(all_0_6_6) = all_120_2_100 & ((all_120_0_98 = all_0_1_1 & triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 & update_slb(all_0_5_5, all_120_2_100) = all_120_1_99) | (all_120_1_99 = 0 & contains_slb(all_0_5_5, all_120_2_100) = 0)) % 29.71/7.70 | % 29.71/7.70 | Applying alpha-rule on (186) yields: % 29.71/7.70 | (187) findmin_pqp_res(all_0_6_6) = all_120_2_100 % 29.71/7.70 | (188) (all_120_0_98 = all_0_1_1 & triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 & update_slb(all_0_5_5, all_120_2_100) = all_120_1_99) | (all_120_1_99 = 0 & contains_slb(all_0_5_5, all_120_2_100) = 0) % 29.71/7.70 | % 29.71/7.70 | Instantiating formula (52) with all_0_6_6, all_120_2_100, all_0_2_2 and discharging atoms findmin_pqp_res(all_0_6_6) = all_120_2_100, findmin_pqp_res(all_0_6_6) = all_0_2_2, yields: % 29.71/7.70 | (189) all_120_2_100 = all_0_2_2 % 29.71/7.70 | % 29.71/7.70 | Instantiating formula (52) with all_0_6_6, all_115_2_97, all_120_2_100 and discharging atoms findmin_pqp_res(all_0_6_6) = all_120_2_100, findmin_pqp_res(all_0_6_6) = all_115_2_97, yields: % 29.71/7.70 | (190) all_120_2_100 = all_115_2_97 % 29.71/7.70 | % 29.71/7.70 | Instantiating formula (52) with all_0_6_6, all_109_2_94, all_120_2_100 and discharging atoms findmin_pqp_res(all_0_6_6) = all_120_2_100, findmin_pqp_res(all_0_6_6) = all_109_2_94, yields: % 29.71/7.70 | (191) all_120_2_100 = all_109_2_94 % 29.71/7.70 | % 29.71/7.70 | Combining equations (191,190) yields a new equation: % 29.71/7.70 | (192) all_115_2_97 = all_109_2_94 % 29.71/7.70 | % 29.71/7.70 | Combining equations (189,190) yields a new equation: % 29.71/7.70 | (193) all_115_2_97 = all_0_2_2 % 29.71/7.70 | % 29.71/7.70 | Combining equations (193,192) yields a new equation: % 29.71/7.70 | (194) all_109_2_94 = all_0_2_2 % 29.71/7.70 | % 29.71/7.70 | Combining equations (194,192) yields a new equation: % 29.71/7.70 | (193) all_115_2_97 = all_0_2_2 % 29.71/7.70 | % 29.71/7.70 | Combining equations (193,190) yields a new equation: % 29.71/7.70 | (189) all_120_2_100 = all_0_2_2 % 29.71/7.70 | % 29.71/7.70 | From (194) and (173) follows: % 29.71/7.70 | (161) findmin_pqp_res(all_0_6_6) = all_0_2_2 % 29.71/7.70 | % 29.71/7.70 +-Applying beta-rule and splitting (137), into two cases. % 29.71/7.70 |-Branch one: % 29.71/7.70 | (198) (all_61_0_77 = 0 & all_61_1_78 = 0 & findmin_pqp_res(all_0_6_6) = all_61_4_81 & update_slb(all_0_5_5, all_61_4_81) = all_61_3_80 & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = 0 & less_than(all_61_4_81, all_61_2_79) = 0) | (all_61_2_79 = 0 & findmin_pqp_res(all_0_6_6) = all_61_4_81 & update_slb(all_0_5_5, all_61_4_81) = all_61_3_80 & pair_in_list(all_61_3_80, all_0_0_0, all_61_4_81) = 0) % 29.80/7.70 | % 29.80/7.70 +-Applying beta-rule and splitting (198), into two cases. % 29.80/7.70 |-Branch one: % 29.80/7.70 | (199) all_61_0_77 = 0 & all_61_1_78 = 0 & findmin_pqp_res(all_0_6_6) = all_61_4_81 & update_slb(all_0_5_5, all_61_4_81) = all_61_3_80 & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = 0 & less_than(all_61_4_81, all_61_2_79) = 0 % 29.80/7.70 | % 29.80/7.70 | Applying alpha-rule on (199) yields: % 29.80/7.70 | (200) less_than(all_61_4_81, all_61_2_79) = 0 % 29.80/7.70 | (201) all_61_1_78 = 0 % 29.80/7.70 | (202) pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = 0 % 29.80/7.70 | (203) findmin_pqp_res(all_0_6_6) = all_61_4_81 % 29.80/7.70 | (204) all_61_0_77 = 0 % 29.80/7.70 | (205) update_slb(all_0_5_5, all_61_4_81) = all_61_3_80 % 29.80/7.70 | % 29.80/7.70 | Instantiating formula (52) with all_0_6_6, all_61_4_81, all_0_2_2 and discharging atoms findmin_pqp_res(all_0_6_6) = all_61_4_81, findmin_pqp_res(all_0_6_6) = all_0_2_2, yields: % 29.80/7.70 | (206) all_61_4_81 = all_0_2_2 % 29.80/7.70 | % 29.80/7.70 | From (206) and (205) follows: % 29.80/7.70 | (207) update_slb(all_0_5_5, all_0_2_2) = all_61_3_80 % 29.80/7.70 | % 29.80/7.70 | From (206) and (200) follows: % 29.80/7.70 | (208) less_than(all_0_2_2, all_61_2_79) = 0 % 29.80/7.70 | % 29.80/7.70 | Instantiating formula (98) with all_61_2_79, all_0_2_2, all_0_0_0 and discharging atoms less_than(all_0_0_0, all_0_2_2) = 0, less_than(all_0_2_2, all_61_2_79) = 0, yields: % 29.80/7.70 | (209) less_than(all_0_0_0, all_61_2_79) = 0 % 29.80/7.70 | % 29.80/7.70 | Instantiating formula (44) with all_57_0_74, all_0_0_0, all_61_2_79, all_0_2_2 and discharging atoms less_than(all_0_2_2, all_61_2_79) = 0, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.80/7.70 | (210) all_57_0_74 = 0 | ? [v0] : ( ~ (v0 = 0) & less_than(all_61_2_79, all_0_0_0) = v0) % 29.80/7.70 | % 29.80/7.70 +-Applying beta-rule and splitting (210), into two cases. % 29.80/7.70 |-Branch one: % 29.80/7.70 | (146) all_57_0_74 = 0 % 29.80/7.70 | % 29.80/7.70 | Equations (146) can reduce 134 to: % 29.80/7.71 | (149) $false % 29.80/7.71 | % 29.80/7.71 |-The branch is then unsatisfiable % 29.80/7.71 |-Branch two: % 29.80/7.71 | (134) ~ (all_57_0_74 = 0) % 29.80/7.71 | (214) ? [v0] : ( ~ (v0 = 0) & less_than(all_61_2_79, all_0_0_0) = v0) % 29.80/7.71 | % 29.80/7.71 | Instantiating (214) with all_197_0_112 yields: % 29.80/7.71 | (215) ~ (all_197_0_112 = 0) & less_than(all_61_2_79, all_0_0_0) = all_197_0_112 % 29.80/7.71 | % 29.80/7.71 | Applying alpha-rule on (215) yields: % 29.80/7.71 | (216) ~ (all_197_0_112 = 0) % 29.80/7.71 | (217) less_than(all_61_2_79, all_0_0_0) = all_197_0_112 % 29.80/7.71 | % 29.80/7.71 | Instantiating formula (41) with all_197_0_112, all_61_2_79, all_0_0_0, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, less_than(all_61_2_79, all_0_0_0) = all_197_0_112, yields: % 29.80/7.71 | (218) all_197_0_112 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_3_3) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_5_5, all_0_0_0, all_61_2_79) = v0)) % 29.80/7.71 | % 29.80/7.71 | Instantiating formula (74) with all_197_0_112, all_61_2_79, all_0_0_0 and discharging atoms less_than(all_61_2_79, all_0_0_0) = all_197_0_112, yields: % 29.80/7.71 | (219) all_197_0_112 = 0 | ? [v0] : ((v0 = 0 & strictly_less_than(all_0_0_0, all_61_2_79) = 0) | ( ~ (v0 = 0) & less_than(all_0_0_0, all_61_2_79) = v0)) % 29.80/7.71 | % 29.80/7.71 | Instantiating formula (109) with all_197_0_112, all_61_2_79, all_0_0_0 and discharging atoms less_than(all_61_2_79, all_0_0_0) = all_197_0_112, yields: % 29.80/7.71 | (220) ? [v0] : ((v0 = 0 & ~ (all_197_0_112 = 0) & less_than(all_0_0_0, all_61_2_79) = 0) | ( ~ (v0 = 0) & strictly_less_than(all_0_0_0, all_61_2_79) = v0)) % 29.80/7.71 | % 29.80/7.71 | Instantiating formula (105) with all_61_2_79, all_0_0_0 and discharging atoms less_than(all_0_0_0, all_61_2_79) = 0, yields: % 29.80/7.71 | (221) ? [v0] : ((v0 = 0 & strictly_less_than(all_0_0_0, all_61_2_79) = 0) | (v0 = 0 & less_than(all_61_2_79, all_0_0_0) = 0)) % 29.80/7.71 | % 29.80/7.71 | Instantiating formula (8) with 0, all_61_2_79, all_0_0_0 and discharging atoms less_than(all_0_0_0, all_61_2_79) = 0, yields: % 29.80/7.71 | (222) ? [v0] : (( ~ (v0 = 0) & strictly_less_than(all_0_0_0, all_61_2_79) = v0) | ( ~ (v0 = 0) & less_than(all_61_2_79, all_0_0_0) = v0)) % 29.80/7.71 | % 29.80/7.71 | Instantiating (222) with all_204_0_113 yields: % 29.80/7.71 | (223) ( ~ (all_204_0_113 = 0) & strictly_less_than(all_0_0_0, all_61_2_79) = all_204_0_113) | ( ~ (all_204_0_113 = 0) & less_than(all_61_2_79, all_0_0_0) = all_204_0_113) % 29.80/7.71 | % 29.80/7.71 | Instantiating (221) with all_205_0_114 yields: % 29.80/7.71 | (224) (all_205_0_114 = 0 & strictly_less_than(all_0_0_0, all_61_2_79) = 0) | (all_205_0_114 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) % 29.80/7.71 | % 29.80/7.71 | Instantiating (220) with all_209_0_117 yields: % 29.80/7.71 | (225) (all_209_0_117 = 0 & ~ (all_197_0_112 = 0) & less_than(all_0_0_0, all_61_2_79) = 0) | ( ~ (all_209_0_117 = 0) & strictly_less_than(all_0_0_0, all_61_2_79) = all_209_0_117) % 29.80/7.71 | % 29.80/7.71 +-Applying beta-rule and splitting (219), into two cases. % 29.80/7.71 |-Branch one: % 29.80/7.71 | (226) all_197_0_112 = 0 % 29.80/7.71 | % 29.80/7.71 | Equations (226) can reduce 216 to: % 29.80/7.71 | (149) $false % 29.80/7.71 | % 29.80/7.71 |-The branch is then unsatisfiable % 29.80/7.71 |-Branch two: % 29.80/7.71 | (216) ~ (all_197_0_112 = 0) % 29.80/7.71 | (229) ? [v0] : ((v0 = 0 & strictly_less_than(all_0_0_0, all_61_2_79) = 0) | ( ~ (v0 = 0) & less_than(all_0_0_0, all_61_2_79) = v0)) % 29.80/7.71 | % 29.80/7.71 | Instantiating (229) with all_214_0_118 yields: % 29.80/7.71 | (230) (all_214_0_118 = 0 & strictly_less_than(all_0_0_0, all_61_2_79) = 0) | ( ~ (all_214_0_118 = 0) & less_than(all_0_0_0, all_61_2_79) = all_214_0_118) % 29.80/7.71 | % 29.80/7.71 +-Applying beta-rule and splitting (224), into two cases. % 29.80/7.71 |-Branch one: % 29.80/7.71 | (231) all_205_0_114 = 0 & strictly_less_than(all_0_0_0, all_61_2_79) = 0 % 29.80/7.71 | % 29.80/7.71 | Applying alpha-rule on (231) yields: % 29.80/7.71 | (232) all_205_0_114 = 0 % 29.80/7.71 | (233) strictly_less_than(all_0_0_0, all_61_2_79) = 0 % 29.80/7.71 | % 29.80/7.71 +-Applying beta-rule and splitting (225), into two cases. % 29.80/7.71 |-Branch one: % 29.80/7.71 | (234) all_209_0_117 = 0 & ~ (all_197_0_112 = 0) & less_than(all_0_0_0, all_61_2_79) = 0 % 29.80/7.71 | % 29.80/7.71 | Applying alpha-rule on (234) yields: % 29.80/7.71 | (235) all_209_0_117 = 0 % 29.80/7.71 | (216) ~ (all_197_0_112 = 0) % 29.80/7.71 | (209) less_than(all_0_0_0, all_61_2_79) = 0 % 29.80/7.71 | % 29.80/7.71 +-Applying beta-rule and splitting (230), into two cases. % 29.80/7.71 |-Branch one: % 29.80/7.71 | (238) all_214_0_118 = 0 & strictly_less_than(all_0_0_0, all_61_2_79) = 0 % 29.80/7.71 | % 29.80/7.71 | Applying alpha-rule on (238) yields: % 29.80/7.71 | (239) all_214_0_118 = 0 % 29.80/7.71 | (233) strictly_less_than(all_0_0_0, all_61_2_79) = 0 % 29.80/7.71 | % 29.80/7.71 +-Applying beta-rule and splitting (223), into two cases. % 29.80/7.71 |-Branch one: % 29.80/7.71 | (241) ~ (all_204_0_113 = 0) & strictly_less_than(all_0_0_0, all_61_2_79) = all_204_0_113 % 29.80/7.71 | % 29.80/7.71 | Applying alpha-rule on (241) yields: % 29.80/7.71 | (242) ~ (all_204_0_113 = 0) % 29.80/7.71 | (243) strictly_less_than(all_0_0_0, all_61_2_79) = all_204_0_113 % 29.80/7.71 | % 29.80/7.71 | Instantiating formula (93) with all_0_0_0, all_61_2_79, 0, all_204_0_113 and discharging atoms strictly_less_than(all_0_0_0, all_61_2_79) = all_204_0_113, strictly_less_than(all_0_0_0, all_61_2_79) = 0, yields: % 29.80/7.71 | (244) all_204_0_113 = 0 % 29.80/7.71 | % 29.80/7.71 | Equations (244) can reduce 242 to: % 29.80/7.71 | (149) $false % 29.80/7.71 | % 29.80/7.71 |-The branch is then unsatisfiable % 29.80/7.71 |-Branch two: % 29.80/7.71 | (246) ~ (all_204_0_113 = 0) & less_than(all_61_2_79, all_0_0_0) = all_204_0_113 % 29.80/7.71 | % 29.80/7.71 | Applying alpha-rule on (246) yields: % 29.80/7.71 | (242) ~ (all_204_0_113 = 0) % 29.80/7.71 | (248) less_than(all_61_2_79, all_0_0_0) = all_204_0_113 % 29.80/7.71 | % 29.80/7.71 | Instantiating formula (15) with all_61_2_79, all_0_0_0, all_204_0_113, all_197_0_112 and discharging atoms less_than(all_61_2_79, all_0_0_0) = all_204_0_113, less_than(all_61_2_79, all_0_0_0) = all_197_0_112, yields: % 29.80/7.71 | (249) all_204_0_113 = all_197_0_112 % 29.80/7.71 | % 29.80/7.71 | Equations (249) can reduce 242 to: % 29.80/7.71 | (216) ~ (all_197_0_112 = 0) % 29.80/7.71 | % 29.80/7.71 | From (249) and (248) follows: % 29.80/7.71 | (217) less_than(all_61_2_79, all_0_0_0) = all_197_0_112 % 29.80/7.72 | % 29.80/7.72 +-Applying beta-rule and splitting (174), into two cases. % 29.80/7.72 |-Branch one: % 29.80/7.72 | (252) (all_109_0_92 = all_0_1_1 & triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 & update_slb(all_0_5_5, all_109_2_94) = all_109_1_93) | ( ~ (all_109_0_92 = 0) & lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 & strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92) % 29.80/7.72 | % 29.80/7.72 +-Applying beta-rule and splitting (252), into two cases. % 29.80/7.72 |-Branch one: % 29.80/7.72 | (253) all_109_0_92 = all_0_1_1 & triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 & update_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.80/7.72 | % 29.80/7.72 | Applying alpha-rule on (253) yields: % 29.80/7.72 | (254) all_109_0_92 = all_0_1_1 % 29.80/7.72 | (255) triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 % 29.80/7.72 | (256) update_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.80/7.72 | % 29.80/7.72 | From (194) and (256) follows: % 29.80/7.72 | (257) update_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.80/7.72 | % 29.80/7.72 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_109_1_93, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_109_1_93, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.80/7.72 | (258) all_109_1_93 = all_61_3_80 % 29.80/7.72 | % 29.80/7.72 | From (258) and (255) follows: % 29.80/7.72 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.80/7.72 | % 29.80/7.72 | Instantiating formula (19) with all_61_2_79, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = 0, yields: % 29.80/7.72 | (260) ? [v0] : ((v0 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.80/7.72 | % 29.80/7.72 | Instantiating (260) with all_302_0_161 yields: % 29.80/7.72 | (261) (all_302_0_161 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) | ( ~ (all_302_0_161 = 0) & check_cpq(all_0_1_1) = all_302_0_161) % 29.80/7.72 | % 29.80/7.72 +-Applying beta-rule and splitting (261), into two cases. % 29.80/7.72 |-Branch one: % 29.80/7.72 | (262) all_302_0_161 = 0 & less_than(all_61_2_79, all_0_0_0) = 0 % 29.80/7.72 | % 29.80/7.72 | Applying alpha-rule on (262) yields: % 29.80/7.72 | (263) all_302_0_161 = 0 % 29.80/7.72 | (264) less_than(all_61_2_79, all_0_0_0) = 0 % 29.80/7.72 | % 29.80/7.72 | Instantiating formula (15) with all_61_2_79, all_0_0_0, 0, all_197_0_112 and discharging atoms less_than(all_61_2_79, all_0_0_0) = all_197_0_112, less_than(all_61_2_79, all_0_0_0) = 0, yields: % 29.80/7.72 | (226) all_197_0_112 = 0 % 29.80/7.72 | % 29.80/7.72 | Equations (226) can reduce 216 to: % 29.80/7.72 | (149) $false % 29.80/7.72 | % 29.80/7.72 |-The branch is then unsatisfiable % 29.80/7.72 |-Branch two: % 29.80/7.72 | (267) ~ (all_302_0_161 = 0) & check_cpq(all_0_1_1) = all_302_0_161 % 29.80/7.72 | % 29.80/7.72 | Applying alpha-rule on (267) yields: % 29.80/7.72 | (268) ~ (all_302_0_161 = 0) % 29.80/7.72 | (269) check_cpq(all_0_1_1) = all_302_0_161 % 29.80/7.72 | % 29.80/7.72 | Instantiating formula (13) with all_0_1_1, all_302_0_161, 0 and discharging atoms check_cpq(all_0_1_1) = all_302_0_161, check_cpq(all_0_1_1) = 0, yields: % 29.80/7.72 | (263) all_302_0_161 = 0 % 29.80/7.72 | % 29.80/7.72 | Equations (263) can reduce 268 to: % 29.80/7.72 | (149) $false % 29.80/7.72 | % 29.80/7.72 |-The branch is then unsatisfiable % 29.80/7.72 |-Branch two: % 29.80/7.72 | (272) ~ (all_109_0_92 = 0) & lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 & strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92 % 29.80/7.72 | % 29.80/7.72 | Applying alpha-rule on (272) yields: % 29.80/7.72 | (273) ~ (all_109_0_92 = 0) % 29.80/7.72 | (274) lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.80/7.72 | (275) strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92 % 29.80/7.72 | % 29.80/7.72 | From (194) and (274) follows: % 29.80/7.72 | (276) lookup_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.80/7.72 | % 29.80/7.72 | From (194) and (275) follows: % 29.80/7.72 | (277) strictly_less_than(all_0_2_2, all_109_1_93) = all_109_0_92 % 29.80/7.72 | % 29.80/7.72 +-Applying beta-rule and splitting (188), into two cases. % 29.80/7.72 |-Branch one: % 29.80/7.72 | (278) all_120_0_98 = all_0_1_1 & triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 & update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.80/7.72 | % 29.80/7.72 | Applying alpha-rule on (278) yields: % 29.80/7.72 | (279) all_120_0_98 = all_0_1_1 % 29.80/7.72 | (280) triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 % 29.80/7.72 | (281) update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.80/7.72 | % 29.80/7.72 | From (189) and (281) follows: % 29.80/7.72 | (282) update_slb(all_0_5_5, all_0_2_2) = all_120_1_99 % 29.80/7.72 | % 29.80/7.72 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_120_1_99, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_120_1_99, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.80/7.72 | (283) all_120_1_99 = all_61_3_80 % 29.80/7.72 | % 29.80/7.72 | From (283) and (280) follows: % 29.80/7.72 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.80/7.72 | % 29.80/7.72 | Instantiating formula (41) with all_197_0_112, all_61_2_79, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, less_than(all_61_2_79, all_0_0_0) = all_197_0_112, yields: % 29.80/7.72 | (285) all_197_0_112 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = v0)) % 29.80/7.72 | % 29.80/7.72 | Instantiating formula (19) with all_61_2_79, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = 0, yields: % 29.80/7.72 | (260) ? [v0] : ((v0 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.80/7.73 | % 29.80/7.73 | Instantiating (260) with all_302_0_194 yields: % 29.80/7.73 | (287) (all_302_0_194 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) | ( ~ (all_302_0_194 = 0) & check_cpq(all_0_1_1) = all_302_0_194) % 29.80/7.73 | % 29.80/7.73 +-Applying beta-rule and splitting (285), into two cases. % 29.80/7.73 |-Branch one: % 29.80/7.73 | (226) all_197_0_112 = 0 % 29.80/7.73 | % 29.80/7.73 | Equations (226) can reduce 216 to: % 29.80/7.73 | (149) $false % 29.80/7.73 | % 29.80/7.73 |-The branch is then unsatisfiable % 29.80/7.73 |-Branch two: % 29.80/7.73 | (216) ~ (all_197_0_112 = 0) % 29.80/7.73 | (291) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = v0)) % 29.80/7.73 | % 29.80/7.73 +-Applying beta-rule and splitting (287), into two cases. % 29.80/7.73 |-Branch one: % 29.80/7.73 | (292) all_302_0_194 = 0 & less_than(all_61_2_79, all_0_0_0) = 0 % 29.80/7.73 | % 29.80/7.73 | Applying alpha-rule on (292) yields: % 29.80/7.73 | (293) all_302_0_194 = 0 % 29.80/7.73 | (264) less_than(all_61_2_79, all_0_0_0) = 0 % 29.80/7.73 | % 29.80/7.73 | Instantiating formula (15) with all_61_2_79, all_0_0_0, 0, all_197_0_112 and discharging atoms less_than(all_61_2_79, all_0_0_0) = all_197_0_112, less_than(all_61_2_79, all_0_0_0) = 0, yields: % 29.80/7.73 | (226) all_197_0_112 = 0 % 29.80/7.73 | % 29.80/7.73 | Equations (226) can reduce 216 to: % 29.80/7.73 | (149) $false % 29.80/7.73 | % 29.80/7.73 |-The branch is then unsatisfiable % 29.80/7.73 |-Branch two: % 29.80/7.73 | (297) ~ (all_302_0_194 = 0) & check_cpq(all_0_1_1) = all_302_0_194 % 29.80/7.73 | % 29.80/7.73 | Applying alpha-rule on (297) yields: % 29.80/7.73 | (298) ~ (all_302_0_194 = 0) % 29.80/7.73 | (299) check_cpq(all_0_1_1) = all_302_0_194 % 29.80/7.73 | % 29.80/7.73 | Instantiating formula (13) with all_0_1_1, all_302_0_194, 0 and discharging atoms check_cpq(all_0_1_1) = all_302_0_194, check_cpq(all_0_1_1) = 0, yields: % 29.80/7.73 | (293) all_302_0_194 = 0 % 29.80/7.73 | % 29.80/7.73 | Equations (293) can reduce 298 to: % 29.80/7.73 | (149) $false % 29.80/7.73 | % 29.80/7.73 |-The branch is then unsatisfiable % 29.80/7.73 |-Branch two: % 29.80/7.73 | (302) all_120_1_99 = 0 & contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.80/7.73 | % 29.80/7.73 | Applying alpha-rule on (302) yields: % 29.80/7.73 | (303) all_120_1_99 = 0 % 29.80/7.73 | (304) contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.80/7.73 | % 29.80/7.73 | From (189) and (304) follows: % 29.80/7.73 | (305) contains_slb(all_0_5_5, all_0_2_2) = 0 % 29.80/7.73 | % 29.80/7.73 +-Applying beta-rule and splitting (181), into two cases. % 29.80/7.73 |-Branch one: % 29.80/7.73 | (306) (all_115_0_95 = all_0_1_1 & triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, all_115_2_97) = all_115_1_96) | ( ~ (all_115_0_95 = 0) & lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 & less_than(all_115_1_96, all_115_2_97) = all_115_0_95) % 29.80/7.73 | % 29.80/7.73 +-Applying beta-rule and splitting (306), into two cases. % 29.80/7.73 |-Branch one: % 29.80/7.73 | (307) all_115_0_95 = all_0_1_1 & triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.80/7.73 | % 29.80/7.73 | Applying alpha-rule on (307) yields: % 29.80/7.73 | (308) all_115_0_95 = all_0_1_1 % 29.80/7.73 | (309) triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 % 29.80/7.73 | (310) update_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.80/7.73 | % 29.80/7.73 | From (193) and (310) follows: % 29.80/7.73 | (311) update_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.80/7.73 | % 29.80/7.73 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_115_1_96, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_115_1_96, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.80/7.73 | (312) all_115_1_96 = all_61_3_80 % 29.80/7.73 | % 29.80/7.73 | From (312) and (309) follows: % 29.80/7.73 | (313) triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1 % 29.80/7.73 | % 29.80/7.73 | Instantiating formula (41) with all_197_0_112, all_61_2_79, all_0_0_0, all_0_1_1, all_0_4_4, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1, less_than(all_61_2_79, all_0_0_0) = all_197_0_112, yields: % 29.80/7.73 | (285) all_197_0_112 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = v0)) % 29.80/7.73 | % 29.80/7.73 | Instantiating formula (19) with all_61_2_79, all_0_0_0, all_0_1_1, all_0_4_4, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = 0, yields: % 29.80/7.73 | (260) ? [v0] : ((v0 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.73 | % 29.94/7.73 | Instantiating (260) with all_297_0_226 yields: % 29.94/7.73 | (316) (all_297_0_226 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) | ( ~ (all_297_0_226 = 0) & check_cpq(all_0_1_1) = all_297_0_226) % 29.94/7.73 | % 29.94/7.73 +-Applying beta-rule and splitting (285), into two cases. % 29.94/7.73 |-Branch one: % 29.94/7.73 | (226) all_197_0_112 = 0 % 29.94/7.73 | % 29.94/7.73 | Equations (226) can reduce 216 to: % 29.94/7.73 | (149) $false % 29.94/7.73 | % 29.94/7.73 |-The branch is then unsatisfiable % 29.94/7.73 |-Branch two: % 29.94/7.73 | (216) ~ (all_197_0_112 = 0) % 29.94/7.73 | (291) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = v0)) % 29.94/7.73 | % 29.94/7.73 +-Applying beta-rule and splitting (316), into two cases. % 29.94/7.73 |-Branch one: % 29.94/7.73 | (321) all_297_0_226 = 0 & less_than(all_61_2_79, all_0_0_0) = 0 % 29.94/7.74 | % 29.94/7.74 | Applying alpha-rule on (321) yields: % 29.94/7.74 | (322) all_297_0_226 = 0 % 29.94/7.74 | (264) less_than(all_61_2_79, all_0_0_0) = 0 % 29.94/7.74 | % 29.94/7.74 | Instantiating formula (15) with all_61_2_79, all_0_0_0, 0, all_197_0_112 and discharging atoms less_than(all_61_2_79, all_0_0_0) = all_197_0_112, less_than(all_61_2_79, all_0_0_0) = 0, yields: % 29.94/7.74 | (226) all_197_0_112 = 0 % 29.94/7.74 | % 29.94/7.74 | Equations (226) can reduce 216 to: % 29.94/7.74 | (149) $false % 29.94/7.74 | % 29.94/7.74 |-The branch is then unsatisfiable % 29.94/7.74 |-Branch two: % 29.94/7.74 | (326) ~ (all_297_0_226 = 0) & check_cpq(all_0_1_1) = all_297_0_226 % 29.94/7.74 | % 29.94/7.74 | Applying alpha-rule on (326) yields: % 29.94/7.74 | (327) ~ (all_297_0_226 = 0) % 29.94/7.74 | (328) check_cpq(all_0_1_1) = all_297_0_226 % 29.94/7.74 | % 29.94/7.74 | Instantiating formula (13) with all_0_1_1, all_297_0_226, 0 and discharging atoms check_cpq(all_0_1_1) = all_297_0_226, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.74 | (322) all_297_0_226 = 0 % 29.94/7.74 | % 29.94/7.74 | Equations (322) can reduce 327 to: % 29.94/7.74 | (149) $false % 29.94/7.74 | % 29.94/7.74 |-The branch is then unsatisfiable % 29.94/7.74 |-Branch two: % 29.94/7.74 | (331) ~ (all_115_0_95 = 0) & lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 & less_than(all_115_1_96, all_115_2_97) = all_115_0_95 % 29.94/7.74 | % 29.94/7.74 | Applying alpha-rule on (331) yields: % 29.94/7.74 | (332) ~ (all_115_0_95 = 0) % 29.94/7.74 | (333) lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.74 | (334) less_than(all_115_1_96, all_115_2_97) = all_115_0_95 % 29.94/7.74 | % 29.94/7.74 | From (193) and (333) follows: % 29.94/7.74 | (335) lookup_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.94/7.74 | % 29.94/7.74 | From (193) and (334) follows: % 29.94/7.74 | (336) less_than(all_115_1_96, all_0_2_2) = all_115_0_95 % 29.94/7.74 | % 29.94/7.74 | Instantiating formula (55) with all_0_5_5, all_0_2_2, all_115_1_96, all_109_1_93 and discharging atoms lookup_slb(all_0_5_5, all_0_2_2) = all_115_1_96, lookup_slb(all_0_5_5, all_0_2_2) = all_109_1_93, yields: % 29.94/7.74 | (337) all_115_1_96 = all_109_1_93 % 29.94/7.74 | % 29.94/7.74 | From (337) and (336) follows: % 29.94/7.74 | (338) less_than(all_109_1_93, all_0_2_2) = all_115_0_95 % 29.94/7.74 | % 29.94/7.74 | Instantiating formula (113) with all_109_0_92, all_109_1_93, all_0_2_2 and discharging atoms strictly_less_than(all_0_2_2, all_109_1_93) = all_109_0_92, yields: % 29.94/7.74 | (339) all_109_0_92 = 0 | ? [v0] : ((v0 = 0 & less_than(all_109_1_93, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_109_1_93) = v0)) % 29.94/7.74 | % 29.94/7.74 | Instantiating formula (28) with all_115_0_95, all_109_1_93, all_0_2_2 and discharging atoms less_than(all_109_1_93, all_0_2_2) = all_115_0_95, yields: % 29.94/7.74 | (340) all_115_0_95 = 0 | less_than(all_0_2_2, all_109_1_93) = 0 % 29.94/7.74 | % 29.94/7.74 | Instantiating formula (74) with all_115_0_95, all_109_1_93, all_0_2_2 and discharging atoms less_than(all_109_1_93, all_0_2_2) = all_115_0_95, yields: % 29.94/7.74 | (341) all_115_0_95 = 0 | ? [v0] : ((v0 = 0 & strictly_less_than(all_0_2_2, all_109_1_93) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_109_1_93) = v0)) % 29.94/7.74 | % 29.94/7.74 +-Applying beta-rule and splitting (340), into two cases. % 29.94/7.74 |-Branch one: % 29.94/7.74 | (342) less_than(all_0_2_2, all_109_1_93) = 0 % 29.94/7.74 | % 29.94/7.74 +-Applying beta-rule and splitting (341), into two cases. % 29.94/7.74 |-Branch one: % 29.94/7.74 | (343) all_115_0_95 = 0 % 29.94/7.74 | % 29.94/7.74 | Equations (343) can reduce 332 to: % 29.94/7.74 | (149) $false % 29.94/7.74 | % 29.94/7.74 |-The branch is then unsatisfiable % 29.94/7.74 |-Branch two: % 29.94/7.74 | (332) ~ (all_115_0_95 = 0) % 29.94/7.74 | (346) ? [v0] : ((v0 = 0 & strictly_less_than(all_0_2_2, all_109_1_93) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_109_1_93) = v0)) % 29.94/7.74 | % 29.94/7.74 | Instantiating (346) with all_316_0_260 yields: % 29.94/7.74 | (347) (all_316_0_260 = 0 & strictly_less_than(all_0_2_2, all_109_1_93) = 0) | ( ~ (all_316_0_260 = 0) & less_than(all_0_2_2, all_109_1_93) = all_316_0_260) % 29.94/7.74 | % 29.94/7.74 +-Applying beta-rule and splitting (347), into two cases. % 29.94/7.74 |-Branch one: % 29.94/7.74 | (348) all_316_0_260 = 0 & strictly_less_than(all_0_2_2, all_109_1_93) = 0 % 29.94/7.74 | % 29.94/7.74 | Applying alpha-rule on (348) yields: % 29.94/7.74 | (349) all_316_0_260 = 0 % 29.94/7.74 | (350) strictly_less_than(all_0_2_2, all_109_1_93) = 0 % 29.94/7.74 | % 29.94/7.74 +-Applying beta-rule and splitting (339), into two cases. % 29.94/7.74 |-Branch one: % 29.94/7.74 | (351) all_109_0_92 = 0 % 29.94/7.74 | % 29.94/7.74 | Equations (351) can reduce 273 to: % 29.94/7.74 | (149) $false % 29.94/7.74 | % 29.94/7.74 |-The branch is then unsatisfiable % 29.94/7.74 |-Branch two: % 29.94/7.74 | (273) ~ (all_109_0_92 = 0) % 29.94/7.74 | (354) ? [v0] : ((v0 = 0 & less_than(all_109_1_93, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_109_1_93) = v0)) % 29.94/7.74 | % 29.94/7.74 | Instantiating formula (93) with all_0_2_2, all_109_1_93, 0, all_109_0_92 and discharging atoms strictly_less_than(all_0_2_2, all_109_1_93) = all_109_0_92, strictly_less_than(all_0_2_2, all_109_1_93) = 0, yields: % 29.94/7.74 | (351) all_109_0_92 = 0 % 29.94/7.74 | % 29.94/7.74 | Equations (351) can reduce 273 to: % 29.94/7.74 | (149) $false % 29.94/7.74 | % 29.94/7.74 |-The branch is then unsatisfiable % 29.94/7.74 |-Branch two: % 29.94/7.74 | (357) ~ (all_316_0_260 = 0) & less_than(all_0_2_2, all_109_1_93) = all_316_0_260 % 29.94/7.74 | % 29.94/7.74 | Applying alpha-rule on (357) yields: % 29.94/7.74 | (358) ~ (all_316_0_260 = 0) % 29.94/7.74 | (359) less_than(all_0_2_2, all_109_1_93) = all_316_0_260 % 29.94/7.74 | % 29.94/7.74 | Instantiating formula (15) with all_0_2_2, all_109_1_93, 0, all_316_0_260 and discharging atoms less_than(all_0_2_2, all_109_1_93) = all_316_0_260, less_than(all_0_2_2, all_109_1_93) = 0, yields: % 29.94/7.74 | (349) all_316_0_260 = 0 % 29.94/7.74 | % 29.94/7.74 | Equations (349) can reduce 358 to: % 29.94/7.74 | (149) $false % 29.94/7.74 | % 29.94/7.74 |-The branch is then unsatisfiable % 29.94/7.74 |-Branch two: % 29.94/7.74 | (362) ~ (less_than(all_0_2_2, all_109_1_93) = 0) % 29.94/7.74 | (343) all_115_0_95 = 0 % 29.94/7.74 | % 29.94/7.74 | Equations (343) can reduce 332 to: % 29.94/7.74 | (149) $false % 29.94/7.74 | % 29.94/7.74 |-The branch is then unsatisfiable % 29.94/7.74 |-Branch two: % 29.94/7.74 | (365) ~ (all_115_1_96 = 0) & contains_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.74 | % 29.94/7.74 | Applying alpha-rule on (365) yields: % 29.94/7.74 | (366) ~ (all_115_1_96 = 0) % 29.94/7.74 | (367) contains_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.74 | % 29.94/7.74 | From (193) and (367) follows: % 29.94/7.75 | (368) contains_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (46) with all_0_5_5, all_0_2_2, all_115_1_96, 0 and discharging atoms contains_slb(all_0_5_5, all_0_2_2) = all_115_1_96, contains_slb(all_0_5_5, all_0_2_2) = 0, yields: % 29.94/7.75 | (369) all_115_1_96 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (369) can reduce 366 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (371) ~ (all_109_1_93 = 0) & contains_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (371) yields: % 29.94/7.75 | (372) ~ (all_109_1_93 = 0) % 29.94/7.75 | (373) contains_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.75 | % 29.94/7.75 | From (194) and (373) follows: % 29.94/7.75 | (374) contains_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.94/7.75 | % 29.94/7.75 +-Applying beta-rule and splitting (188), into two cases. % 29.94/7.75 |-Branch one: % 29.94/7.75 | (278) all_120_0_98 = all_0_1_1 & triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 & update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (278) yields: % 29.94/7.75 | (279) all_120_0_98 = all_0_1_1 % 29.94/7.75 | (280) triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 % 29.94/7.75 | (281) update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.75 | % 29.94/7.75 | From (189) and (281) follows: % 29.94/7.75 | (282) update_slb(all_0_5_5, all_0_2_2) = all_120_1_99 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_120_1_99, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_120_1_99, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.75 | (283) all_120_1_99 = all_61_3_80 % 29.94/7.75 | % 29.94/7.75 | From (283) and (280) follows: % 29.94/7.75 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (41) with all_197_0_112, all_61_2_79, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, less_than(all_61_2_79, all_0_0_0) = all_197_0_112, yields: % 29.94/7.75 | (285) all_197_0_112 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = v0)) % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (19) with all_61_2_79, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = 0, yields: % 29.94/7.75 | (260) ? [v0] : ((v0 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.75 | % 29.94/7.75 | Instantiating (260) with all_300_0_268 yields: % 29.94/7.75 | (384) (all_300_0_268 = 0 & less_than(all_61_2_79, all_0_0_0) = 0) | ( ~ (all_300_0_268 = 0) & check_cpq(all_0_1_1) = all_300_0_268) % 29.94/7.75 | % 29.94/7.75 +-Applying beta-rule and splitting (384), into two cases. % 29.94/7.75 |-Branch one: % 29.94/7.75 | (385) all_300_0_268 = 0 & less_than(all_61_2_79, all_0_0_0) = 0 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (385) yields: % 29.94/7.75 | (386) all_300_0_268 = 0 % 29.94/7.75 | (264) less_than(all_61_2_79, all_0_0_0) = 0 % 29.94/7.75 | % 29.94/7.75 +-Applying beta-rule and splitting (285), into two cases. % 29.94/7.75 |-Branch one: % 29.94/7.75 | (226) all_197_0_112 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (226) can reduce 216 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (216) ~ (all_197_0_112 = 0) % 29.94/7.75 | (291) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_61_2_79) = v0)) % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (15) with all_61_2_79, all_0_0_0, 0, all_197_0_112 and discharging atoms less_than(all_61_2_79, all_0_0_0) = all_197_0_112, less_than(all_61_2_79, all_0_0_0) = 0, yields: % 29.94/7.75 | (226) all_197_0_112 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (226) can reduce 216 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (394) ~ (all_300_0_268 = 0) & check_cpq(all_0_1_1) = all_300_0_268 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (394) yields: % 29.94/7.75 | (395) ~ (all_300_0_268 = 0) % 29.94/7.75 | (396) check_cpq(all_0_1_1) = all_300_0_268 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (13) with all_0_1_1, all_300_0_268, 0 and discharging atoms check_cpq(all_0_1_1) = all_300_0_268, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.75 | (386) all_300_0_268 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (386) can reduce 395 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (302) all_120_1_99 = 0 & contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (302) yields: % 29.94/7.75 | (303) all_120_1_99 = 0 % 29.94/7.75 | (304) contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.75 | % 29.94/7.75 | From (189) and (304) follows: % 29.94/7.75 | (305) contains_slb(all_0_5_5, all_0_2_2) = 0 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (46) with all_0_5_5, all_0_2_2, 0, all_109_1_93 and discharging atoms contains_slb(all_0_5_5, all_0_2_2) = all_109_1_93, contains_slb(all_0_5_5, all_0_2_2) = 0, yields: % 29.94/7.75 | (403) all_109_1_93 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (403) can reduce 372 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (405) ~ (all_214_0_118 = 0) & less_than(all_0_0_0, all_61_2_79) = all_214_0_118 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (405) yields: % 29.94/7.75 | (406) ~ (all_214_0_118 = 0) % 29.94/7.75 | (407) less_than(all_0_0_0, all_61_2_79) = all_214_0_118 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (15) with all_0_0_0, all_61_2_79, all_214_0_118, 0 and discharging atoms less_than(all_0_0_0, all_61_2_79) = all_214_0_118, less_than(all_0_0_0, all_61_2_79) = 0, yields: % 29.94/7.75 | (239) all_214_0_118 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (239) can reduce 406 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (410) ~ (all_209_0_117 = 0) & strictly_less_than(all_0_0_0, all_61_2_79) = all_209_0_117 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (410) yields: % 29.94/7.75 | (411) ~ (all_209_0_117 = 0) % 29.94/7.75 | (412) strictly_less_than(all_0_0_0, all_61_2_79) = all_209_0_117 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (93) with all_0_0_0, all_61_2_79, 0, all_209_0_117 and discharging atoms strictly_less_than(all_0_0_0, all_61_2_79) = all_209_0_117, strictly_less_than(all_0_0_0, all_61_2_79) = 0, yields: % 29.94/7.75 | (235) all_209_0_117 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (235) can reduce 411 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (415) all_205_0_114 = 0 & less_than(all_61_2_79, all_0_0_0) = 0 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (415) yields: % 29.94/7.75 | (232) all_205_0_114 = 0 % 29.94/7.75 | (264) less_than(all_61_2_79, all_0_0_0) = 0 % 29.94/7.75 | % 29.94/7.75 +-Applying beta-rule and splitting (218), into two cases. % 29.94/7.75 |-Branch one: % 29.94/7.75 | (226) all_197_0_112 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (226) can reduce 216 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (216) ~ (all_197_0_112 = 0) % 29.94/7.75 | (421) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_3_3) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_5_5, all_0_0_0, all_61_2_79) = v0)) % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (15) with all_61_2_79, all_0_0_0, 0, all_197_0_112 and discharging atoms less_than(all_61_2_79, all_0_0_0) = all_197_0_112, less_than(all_61_2_79, all_0_0_0) = 0, yields: % 29.94/7.75 | (226) all_197_0_112 = 0 % 29.94/7.75 | % 29.94/7.75 | Equations (226) can reduce 216 to: % 29.94/7.75 | (149) $false % 29.94/7.75 | % 29.94/7.75 |-The branch is then unsatisfiable % 29.94/7.75 |-Branch two: % 29.94/7.75 | (424) all_61_2_79 = 0 & findmin_pqp_res(all_0_6_6) = all_61_4_81 & update_slb(all_0_5_5, all_61_4_81) = all_61_3_80 & pair_in_list(all_61_3_80, all_0_0_0, all_61_4_81) = 0 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (424) yields: % 29.94/7.75 | (425) all_61_2_79 = 0 % 29.94/7.75 | (203) findmin_pqp_res(all_0_6_6) = all_61_4_81 % 29.94/7.75 | (205) update_slb(all_0_5_5, all_61_4_81) = all_61_3_80 % 29.94/7.75 | (428) pair_in_list(all_61_3_80, all_0_0_0, all_61_4_81) = 0 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (52) with all_0_6_6, all_61_4_81, all_0_2_2 and discharging atoms findmin_pqp_res(all_0_6_6) = all_61_4_81, findmin_pqp_res(all_0_6_6) = all_0_2_2, yields: % 29.94/7.75 | (206) all_61_4_81 = all_0_2_2 % 29.94/7.75 | % 29.94/7.75 | From (206) and (205) follows: % 29.94/7.75 | (207) update_slb(all_0_5_5, all_0_2_2) = all_61_3_80 % 29.94/7.75 | % 29.94/7.75 | From (206) and (428) follows: % 29.94/7.75 | (431) pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0 % 29.94/7.75 | % 29.94/7.75 +-Applying beta-rule and splitting (166), into two cases. % 29.94/7.75 |-Branch one: % 29.94/7.75 | (432) all_101_0_91 = 0 & less_than(all_0_0_0, all_0_2_2) = 0 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (432) yields: % 29.94/7.75 | (433) all_101_0_91 = 0 % 29.94/7.75 | (135) less_than(all_0_0_0, all_0_2_2) = 0 % 29.94/7.75 | % 29.94/7.75 +-Applying beta-rule and splitting (174), into two cases. % 29.94/7.75 |-Branch one: % 29.94/7.75 | (252) (all_109_0_92 = all_0_1_1 & triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 & update_slb(all_0_5_5, all_109_2_94) = all_109_1_93) | ( ~ (all_109_0_92 = 0) & lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 & strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92) % 29.94/7.75 | % 29.94/7.75 +-Applying beta-rule and splitting (252), into two cases. % 29.94/7.75 |-Branch one: % 29.94/7.75 | (253) all_109_0_92 = all_0_1_1 & triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 & update_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.75 | % 29.94/7.75 | Applying alpha-rule on (253) yields: % 29.94/7.75 | (254) all_109_0_92 = all_0_1_1 % 29.94/7.75 | (255) triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 % 29.94/7.75 | (256) update_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.75 | % 29.94/7.75 | From (194) and (256) follows: % 29.94/7.75 | (257) update_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.94/7.75 | % 29.94/7.75 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_109_1_93, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_109_1_93, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.76 | (258) all_109_1_93 = all_61_3_80 % 29.94/7.76 | % 29.94/7.76 | From (258) and (255) follows: % 29.94/7.76 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.76 | (443) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (19) with all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.76 | (444) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.76 | % 29.94/7.76 | Instantiating (444) with all_222_0_321 yields: % 29.94/7.76 | (445) (all_222_0_321 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_222_0_321 = 0) & check_cpq(all_0_1_1) = all_222_0_321) % 29.94/7.76 | % 29.94/7.76 +-Applying beta-rule and splitting (443), into two cases. % 29.94/7.76 |-Branch one: % 29.94/7.76 | (146) all_57_0_74 = 0 % 29.94/7.76 | % 29.94/7.76 | Equations (146) can reduce 134 to: % 29.94/7.76 | (149) $false % 29.94/7.76 | % 29.94/7.76 |-The branch is then unsatisfiable % 29.94/7.76 |-Branch two: % 29.94/7.76 | (134) ~ (all_57_0_74 = 0) % 29.94/7.76 | (449) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.76 | % 29.94/7.76 +-Applying beta-rule and splitting (445), into two cases. % 29.94/7.76 |-Branch one: % 29.94/7.76 | (450) all_222_0_321 = 0 & less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.76 | % 29.94/7.76 | Applying alpha-rule on (450) yields: % 29.94/7.76 | (451) all_222_0_321 = 0 % 29.94/7.76 | (452) less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (15) with all_0_2_2, all_0_0_0, 0, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, less_than(all_0_2_2, all_0_0_0) = 0, yields: % 29.94/7.76 | (146) all_57_0_74 = 0 % 29.94/7.76 | % 29.94/7.76 | Equations (146) can reduce 134 to: % 29.94/7.76 | (149) $false % 29.94/7.76 | % 29.94/7.76 |-The branch is then unsatisfiable % 29.94/7.76 |-Branch two: % 29.94/7.76 | (455) ~ (all_222_0_321 = 0) & check_cpq(all_0_1_1) = all_222_0_321 % 29.94/7.76 | % 29.94/7.76 | Applying alpha-rule on (455) yields: % 29.94/7.76 | (456) ~ (all_222_0_321 = 0) % 29.94/7.76 | (457) check_cpq(all_0_1_1) = all_222_0_321 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (13) with all_0_1_1, all_222_0_321, 0 and discharging atoms check_cpq(all_0_1_1) = all_222_0_321, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.76 | (451) all_222_0_321 = 0 % 29.94/7.76 | % 29.94/7.76 | Equations (451) can reduce 456 to: % 29.94/7.76 | (149) $false % 29.94/7.76 | % 29.94/7.76 |-The branch is then unsatisfiable % 29.94/7.76 |-Branch two: % 29.94/7.76 | (272) ~ (all_109_0_92 = 0) & lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 & strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92 % 29.94/7.76 | % 29.94/7.76 | Applying alpha-rule on (272) yields: % 29.94/7.76 | (273) ~ (all_109_0_92 = 0) % 29.94/7.76 | (274) lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.76 | (275) strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92 % 29.94/7.76 | % 29.94/7.76 | From (194) and (274) follows: % 29.94/7.76 | (276) lookup_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.94/7.76 | % 29.94/7.76 | From (194) and (275) follows: % 29.94/7.76 | (277) strictly_less_than(all_0_2_2, all_109_1_93) = all_109_0_92 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (113) with all_109_0_92, all_109_1_93, all_0_2_2 and discharging atoms strictly_less_than(all_0_2_2, all_109_1_93) = all_109_0_92, yields: % 29.94/7.76 | (339) all_109_0_92 = 0 | ? [v0] : ((v0 = 0 & less_than(all_109_1_93, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_109_1_93) = v0)) % 29.94/7.76 | % 29.94/7.76 +-Applying beta-rule and splitting (181), into two cases. % 29.94/7.76 |-Branch one: % 29.94/7.76 | (306) (all_115_0_95 = all_0_1_1 & triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, all_115_2_97) = all_115_1_96) | ( ~ (all_115_0_95 = 0) & lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 & less_than(all_115_1_96, all_115_2_97) = all_115_0_95) % 29.94/7.76 | % 29.94/7.76 +-Applying beta-rule and splitting (306), into two cases. % 29.94/7.76 |-Branch one: % 29.94/7.76 | (307) all_115_0_95 = all_0_1_1 & triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.76 | % 29.94/7.76 | Applying alpha-rule on (307) yields: % 29.94/7.76 | (308) all_115_0_95 = all_0_1_1 % 29.94/7.76 | (309) triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 % 29.94/7.76 | (310) update_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.76 | % 29.94/7.76 | From (193) and (310) follows: % 29.94/7.76 | (311) update_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_115_1_96, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_115_1_96, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.76 | (312) all_115_1_96 = all_61_3_80 % 29.94/7.76 | % 29.94/7.76 | From (312) and (309) follows: % 29.94/7.76 | (313) triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_1_1, all_0_4_4, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.76 | (443) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (19) with all_0_2_2, all_0_0_0, all_0_1_1, all_0_4_4, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.76 | (444) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.76 | % 29.94/7.76 | Instantiating (444) with all_232_0_340 yields: % 29.94/7.76 | (477) (all_232_0_340 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_232_0_340 = 0) & check_cpq(all_0_1_1) = all_232_0_340) % 29.94/7.76 | % 29.94/7.76 +-Applying beta-rule and splitting (443), into two cases. % 29.94/7.76 |-Branch one: % 29.94/7.76 | (146) all_57_0_74 = 0 % 29.94/7.76 | % 29.94/7.76 | Equations (146) can reduce 134 to: % 29.94/7.76 | (149) $false % 29.94/7.76 | % 29.94/7.76 |-The branch is then unsatisfiable % 29.94/7.76 |-Branch two: % 29.94/7.76 | (134) ~ (all_57_0_74 = 0) % 29.94/7.76 | (449) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.76 | % 29.94/7.76 +-Applying beta-rule and splitting (477), into two cases. % 29.94/7.76 |-Branch one: % 29.94/7.76 | (482) all_232_0_340 = 0 & less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.76 | % 29.94/7.76 | Applying alpha-rule on (482) yields: % 29.94/7.76 | (483) all_232_0_340 = 0 % 29.94/7.76 | (452) less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (15) with all_0_2_2, all_0_0_0, 0, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, less_than(all_0_2_2, all_0_0_0) = 0, yields: % 29.94/7.76 | (146) all_57_0_74 = 0 % 29.94/7.76 | % 29.94/7.76 | Equations (146) can reduce 134 to: % 29.94/7.76 | (149) $false % 29.94/7.76 | % 29.94/7.76 |-The branch is then unsatisfiable % 29.94/7.76 |-Branch two: % 29.94/7.76 | (487) ~ (all_232_0_340 = 0) & check_cpq(all_0_1_1) = all_232_0_340 % 29.94/7.76 | % 29.94/7.76 | Applying alpha-rule on (487) yields: % 29.94/7.76 | (488) ~ (all_232_0_340 = 0) % 29.94/7.76 | (489) check_cpq(all_0_1_1) = all_232_0_340 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (13) with all_0_1_1, all_232_0_340, 0 and discharging atoms check_cpq(all_0_1_1) = all_232_0_340, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.76 | (483) all_232_0_340 = 0 % 29.94/7.76 | % 29.94/7.76 | Equations (483) can reduce 488 to: % 29.94/7.76 | (149) $false % 29.94/7.76 | % 29.94/7.76 |-The branch is then unsatisfiable % 29.94/7.76 |-Branch two: % 29.94/7.76 | (331) ~ (all_115_0_95 = 0) & lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 & less_than(all_115_1_96, all_115_2_97) = all_115_0_95 % 29.94/7.76 | % 29.94/7.76 | Applying alpha-rule on (331) yields: % 29.94/7.76 | (332) ~ (all_115_0_95 = 0) % 29.94/7.76 | (333) lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.76 | (334) less_than(all_115_1_96, all_115_2_97) = all_115_0_95 % 29.94/7.76 | % 29.94/7.76 | From (193) and (333) follows: % 29.94/7.76 | (335) lookup_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.94/7.76 | % 29.94/7.76 | From (193) and (334) follows: % 29.94/7.76 | (336) less_than(all_115_1_96, all_0_2_2) = all_115_0_95 % 29.94/7.76 | % 29.94/7.76 +-Applying beta-rule and splitting (339), into two cases. % 29.94/7.76 |-Branch one: % 29.94/7.76 | (351) all_109_0_92 = 0 % 29.94/7.76 | % 29.94/7.76 | Equations (351) can reduce 273 to: % 29.94/7.76 | (149) $false % 29.94/7.76 | % 29.94/7.76 |-The branch is then unsatisfiable % 29.94/7.76 |-Branch two: % 29.94/7.76 | (273) ~ (all_109_0_92 = 0) % 29.94/7.76 | (354) ? [v0] : ((v0 = 0 & less_than(all_109_1_93, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_109_1_93) = v0)) % 29.94/7.76 | % 29.94/7.76 | Instantiating (354) with all_220_0_355 yields: % 29.94/7.76 | (502) (all_220_0_355 = 0 & less_than(all_109_1_93, all_0_2_2) = 0) | ( ~ (all_220_0_355 = 0) & less_than(all_0_2_2, all_109_1_93) = all_220_0_355) % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (55) with all_0_5_5, all_0_2_2, all_115_1_96, all_109_1_93 and discharging atoms lookup_slb(all_0_5_5, all_0_2_2) = all_115_1_96, lookup_slb(all_0_5_5, all_0_2_2) = all_109_1_93, yields: % 29.94/7.76 | (337) all_115_1_96 = all_109_1_93 % 29.94/7.76 | % 29.94/7.76 | From (337) and (336) follows: % 29.94/7.76 | (338) less_than(all_109_1_93, all_0_2_2) = all_115_0_95 % 29.94/7.76 | % 29.94/7.76 +-Applying beta-rule and splitting (502), into two cases. % 29.94/7.76 |-Branch one: % 29.94/7.76 | (505) all_220_0_355 = 0 & less_than(all_109_1_93, all_0_2_2) = 0 % 29.94/7.76 | % 29.94/7.76 | Applying alpha-rule on (505) yields: % 29.94/7.76 | (506) all_220_0_355 = 0 % 29.94/7.76 | (507) less_than(all_109_1_93, all_0_2_2) = 0 % 29.94/7.76 | % 29.94/7.76 | Instantiating formula (15) with all_109_1_93, all_0_2_2, 0, all_115_0_95 and discharging atoms less_than(all_109_1_93, all_0_2_2) = all_115_0_95, less_than(all_109_1_93, all_0_2_2) = 0, yields: % 29.94/7.76 | (343) all_115_0_95 = 0 % 29.94/7.76 | % 29.94/7.76 | Equations (343) can reduce 332 to: % 29.94/7.76 | (149) $false % 29.94/7.76 | % 29.94/7.76 |-The branch is then unsatisfiable % 29.94/7.76 |-Branch two: % 29.94/7.76 | (510) ~ (all_220_0_355 = 0) & less_than(all_0_2_2, all_109_1_93) = all_220_0_355 % 29.94/7.76 | % 29.94/7.77 | Applying alpha-rule on (510) yields: % 29.94/7.77 | (511) ~ (all_220_0_355 = 0) % 29.94/7.77 | (512) less_than(all_0_2_2, all_109_1_93) = all_220_0_355 % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (41) with all_115_0_95, all_109_1_93, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, less_than(all_109_1_93, all_0_2_2) = all_115_0_95, yields: % 29.94/7.77 | (513) all_115_0_95 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_3_3) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_5_5, all_0_2_2, all_109_1_93) = v0)) % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (37) with all_115_0_95, all_0_2_2, all_0_0_0, all_109_1_93 and discharging atoms less_than(all_109_1_93, all_0_2_2) = all_115_0_95, less_than(all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.77 | (514) all_115_0_95 = 0 | ? [v0] : ( ~ (v0 = 0) & less_than(all_109_1_93, all_0_0_0) = v0) % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (28) with all_220_0_355, all_0_2_2, all_109_1_93 and discharging atoms less_than(all_0_2_2, all_109_1_93) = all_220_0_355, yields: % 29.94/7.77 | (515) all_220_0_355 = 0 | less_than(all_109_1_93, all_0_2_2) = 0 % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (514), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (343) all_115_0_95 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (343) can reduce 332 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (332) ~ (all_115_0_95 = 0) % 29.94/7.77 | (519) ? [v0] : ( ~ (v0 = 0) & less_than(all_109_1_93, all_0_0_0) = v0) % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (515), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (507) less_than(all_109_1_93, all_0_2_2) = 0 % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (513), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (343) all_115_0_95 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (343) can reduce 332 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (332) ~ (all_115_0_95 = 0) % 29.94/7.77 | (524) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_3_3) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_5_5, all_0_2_2, all_109_1_93) = v0)) % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (15) with all_109_1_93, all_0_2_2, 0, all_115_0_95 and discharging atoms less_than(all_109_1_93, all_0_2_2) = all_115_0_95, less_than(all_109_1_93, all_0_2_2) = 0, yields: % 29.94/7.77 | (343) all_115_0_95 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (343) can reduce 332 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (527) ~ (less_than(all_109_1_93, all_0_2_2) = 0) % 29.94/7.77 | (506) all_220_0_355 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (506) can reduce 511 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (365) ~ (all_115_1_96 = 0) & contains_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.77 | % 29.94/7.77 | Applying alpha-rule on (365) yields: % 29.94/7.77 | (366) ~ (all_115_1_96 = 0) % 29.94/7.77 | (367) contains_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.77 | % 29.94/7.77 | From (193) and (367) follows: % 29.94/7.77 | (368) contains_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (188), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (278) all_120_0_98 = all_0_1_1 & triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 & update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.77 | % 29.94/7.77 | Applying alpha-rule on (278) yields: % 29.94/7.77 | (279) all_120_0_98 = all_0_1_1 % 29.94/7.77 | (280) triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 % 29.94/7.77 | (281) update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.77 | % 29.94/7.77 | From (189) and (281) follows: % 29.94/7.77 | (282) update_slb(all_0_5_5, all_0_2_2) = all_120_1_99 % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_120_1_99, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_120_1_99, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.77 | (283) all_120_1_99 = all_61_3_80 % 29.94/7.77 | % 29.94/7.77 | From (283) and (280) follows: % 29.94/7.77 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.77 | (443) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (19) with all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.77 | (444) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.77 | % 29.94/7.77 | Instantiating (444) with all_240_0_377 yields: % 29.94/7.77 | (543) (all_240_0_377 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_240_0_377 = 0) & check_cpq(all_0_1_1) = all_240_0_377) % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (443), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (146) all_57_0_74 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (146) can reduce 134 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (134) ~ (all_57_0_74 = 0) % 29.94/7.77 | (449) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (543), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (548) all_240_0_377 = 0 & less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.77 | % 29.94/7.77 | Applying alpha-rule on (548) yields: % 29.94/7.77 | (549) all_240_0_377 = 0 % 29.94/7.77 | (452) less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (15) with all_0_2_2, all_0_0_0, 0, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, less_than(all_0_2_2, all_0_0_0) = 0, yields: % 29.94/7.77 | (146) all_57_0_74 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (146) can reduce 134 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (553) ~ (all_240_0_377 = 0) & check_cpq(all_0_1_1) = all_240_0_377 % 29.94/7.77 | % 29.94/7.77 | Applying alpha-rule on (553) yields: % 29.94/7.77 | (554) ~ (all_240_0_377 = 0) % 29.94/7.77 | (555) check_cpq(all_0_1_1) = all_240_0_377 % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (13) with all_0_1_1, all_240_0_377, 0 and discharging atoms check_cpq(all_0_1_1) = all_240_0_377, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.77 | (549) all_240_0_377 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (549) can reduce 554 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (302) all_120_1_99 = 0 & contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.77 | % 29.94/7.77 | Applying alpha-rule on (302) yields: % 29.94/7.77 | (303) all_120_1_99 = 0 % 29.94/7.77 | (304) contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.77 | % 29.94/7.77 | From (189) and (304) follows: % 29.94/7.77 | (305) contains_slb(all_0_5_5, all_0_2_2) = 0 % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (46) with all_0_5_5, all_0_2_2, 0, all_115_1_96 and discharging atoms contains_slb(all_0_5_5, all_0_2_2) = all_115_1_96, contains_slb(all_0_5_5, all_0_2_2) = 0, yields: % 29.94/7.77 | (369) all_115_1_96 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (369) can reduce 366 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (371) ~ (all_109_1_93 = 0) & contains_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.77 | % 29.94/7.77 | Applying alpha-rule on (371) yields: % 29.94/7.77 | (372) ~ (all_109_1_93 = 0) % 29.94/7.77 | (373) contains_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.77 | % 29.94/7.77 | From (194) and (373) follows: % 29.94/7.77 | (374) contains_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (188), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (278) all_120_0_98 = all_0_1_1 & triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 & update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.77 | % 29.94/7.77 | Applying alpha-rule on (278) yields: % 29.94/7.77 | (279) all_120_0_98 = all_0_1_1 % 29.94/7.77 | (280) triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 % 29.94/7.77 | (281) update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.77 | % 29.94/7.77 | From (189) and (281) follows: % 29.94/7.77 | (282) update_slb(all_0_5_5, all_0_2_2) = all_120_1_99 % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_120_1_99, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_120_1_99, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.77 | (283) all_120_1_99 = all_61_3_80 % 29.94/7.77 | % 29.94/7.77 | From (283) and (280) follows: % 29.94/7.77 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.77 | (443) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.77 | % 29.94/7.77 | Instantiating formula (19) with all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.77 | (444) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.77 | % 29.94/7.77 | Instantiating (444) with all_228_0_399 yields: % 29.94/7.77 | (577) (all_228_0_399 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_228_0_399 = 0) & check_cpq(all_0_1_1) = all_228_0_399) % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (443), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (146) all_57_0_74 = 0 % 29.94/7.77 | % 29.94/7.77 | Equations (146) can reduce 134 to: % 29.94/7.77 | (149) $false % 29.94/7.77 | % 29.94/7.77 |-The branch is then unsatisfiable % 29.94/7.77 |-Branch two: % 29.94/7.77 | (134) ~ (all_57_0_74 = 0) % 29.94/7.77 | (449) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.77 | % 29.94/7.77 +-Applying beta-rule and splitting (577), into two cases. % 29.94/7.77 |-Branch one: % 29.94/7.77 | (582) all_228_0_399 = 0 & less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.77 | % 29.94/7.77 | Applying alpha-rule on (582) yields: % 29.94/7.77 | (583) all_228_0_399 = 0 % 29.94/7.77 | (452) less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (15) with all_0_2_2, all_0_0_0, 0, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, less_than(all_0_2_2, all_0_0_0) = 0, yields: % 29.94/7.78 | (146) all_57_0_74 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (146) can reduce 134 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.78 | (587) ~ (all_228_0_399 = 0) & check_cpq(all_0_1_1) = all_228_0_399 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (587) yields: % 29.94/7.78 | (588) ~ (all_228_0_399 = 0) % 29.94/7.78 | (589) check_cpq(all_0_1_1) = all_228_0_399 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (13) with all_0_1_1, all_228_0_399, 0 and discharging atoms check_cpq(all_0_1_1) = all_228_0_399, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.78 | (583) all_228_0_399 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (583) can reduce 588 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.78 | (302) all_120_1_99 = 0 & contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (302) yields: % 29.94/7.78 | (303) all_120_1_99 = 0 % 29.94/7.78 | (304) contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.78 | % 29.94/7.78 | From (189) and (304) follows: % 29.94/7.78 | (305) contains_slb(all_0_5_5, all_0_2_2) = 0 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (46) with all_0_5_5, all_0_2_2, 0, all_109_1_93 and discharging atoms contains_slb(all_0_5_5, all_0_2_2) = all_109_1_93, contains_slb(all_0_5_5, all_0_2_2) = 0, yields: % 29.94/7.78 | (403) all_109_1_93 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (403) can reduce 372 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.78 | (598) ~ (all_101_0_91 = 0) & less_than(all_0_2_2, all_0_0_0) = all_101_0_91 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (598) yields: % 29.94/7.78 | (599) ~ (all_101_0_91 = 0) % 29.94/7.78 | (600) less_than(all_0_2_2, all_0_0_0) = all_101_0_91 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (15) with all_0_2_2, all_0_0_0, all_101_0_91, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_101_0_91, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.78 | (601) all_101_0_91 = all_57_0_74 % 29.94/7.78 | % 29.94/7.78 | Equations (601) can reduce 599 to: % 29.94/7.78 | (134) ~ (all_57_0_74 = 0) % 29.94/7.78 | % 29.94/7.78 | From (601) and (600) follows: % 29.94/7.78 | (136) less_than(all_0_2_2, all_0_0_0) = all_57_0_74 % 29.94/7.78 | % 29.94/7.78 +-Applying beta-rule and splitting (174), into two cases. % 29.94/7.78 |-Branch one: % 29.94/7.78 | (252) (all_109_0_92 = all_0_1_1 & triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 & update_slb(all_0_5_5, all_109_2_94) = all_109_1_93) | ( ~ (all_109_0_92 = 0) & lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 & strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92) % 29.94/7.78 | % 29.94/7.78 +-Applying beta-rule and splitting (252), into two cases. % 29.94/7.78 |-Branch one: % 29.94/7.78 | (253) all_109_0_92 = all_0_1_1 & triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 & update_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (253) yields: % 29.94/7.78 | (254) all_109_0_92 = all_0_1_1 % 29.94/7.78 | (255) triple(all_0_6_6, all_109_1_93, bad) = all_0_1_1 % 29.94/7.78 | (256) update_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.78 | % 29.94/7.78 | From (194) and (256) follows: % 29.94/7.78 | (257) update_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_109_1_93, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_109_1_93, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.78 | (258) all_109_1_93 = all_61_3_80 % 29.94/7.78 | % 29.94/7.78 | From (258) and (255) follows: % 29.94/7.78 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.78 | (443) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (19) with all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.78 | (444) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.78 | % 29.94/7.78 | Instantiating (444) with all_226_0_413 yields: % 29.94/7.78 | (614) (all_226_0_413 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_226_0_413 = 0) & check_cpq(all_0_1_1) = all_226_0_413) % 29.94/7.78 | % 29.94/7.78 +-Applying beta-rule and splitting (443), into two cases. % 29.94/7.78 |-Branch one: % 29.94/7.78 | (146) all_57_0_74 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (146) can reduce 134 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.78 | (134) ~ (all_57_0_74 = 0) % 29.94/7.78 | (449) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.78 | % 29.94/7.78 +-Applying beta-rule and splitting (614), into two cases. % 29.94/7.78 |-Branch one: % 29.94/7.78 | (619) all_226_0_413 = 0 & less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (619) yields: % 29.94/7.78 | (620) all_226_0_413 = 0 % 29.94/7.78 | (452) less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (15) with all_0_2_2, all_0_0_0, 0, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, less_than(all_0_2_2, all_0_0_0) = 0, yields: % 29.94/7.78 | (146) all_57_0_74 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (146) can reduce 134 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.78 | (624) ~ (all_226_0_413 = 0) & check_cpq(all_0_1_1) = all_226_0_413 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (624) yields: % 29.94/7.78 | (625) ~ (all_226_0_413 = 0) % 29.94/7.78 | (626) check_cpq(all_0_1_1) = all_226_0_413 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (13) with all_0_1_1, all_226_0_413, 0 and discharging atoms check_cpq(all_0_1_1) = all_226_0_413, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.78 | (620) all_226_0_413 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (620) can reduce 625 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.78 | (272) ~ (all_109_0_92 = 0) & lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 & strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (272) yields: % 29.94/7.78 | (273) ~ (all_109_0_92 = 0) % 29.94/7.78 | (274) lookup_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.78 | (275) strictly_less_than(all_109_2_94, all_109_1_93) = all_109_0_92 % 29.94/7.78 | % 29.94/7.78 | From (194) and (274) follows: % 29.94/7.78 | (276) lookup_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.94/7.78 | % 29.94/7.78 | From (194) and (275) follows: % 29.94/7.78 | (277) strictly_less_than(all_0_2_2, all_109_1_93) = all_109_0_92 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (113) with all_109_0_92, all_109_1_93, all_0_2_2 and discharging atoms strictly_less_than(all_0_2_2, all_109_1_93) = all_109_0_92, yields: % 29.94/7.78 | (339) all_109_0_92 = 0 | ? [v0] : ((v0 = 0 & less_than(all_109_1_93, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_109_1_93) = v0)) % 29.94/7.78 | % 29.94/7.78 +-Applying beta-rule and splitting (188), into two cases. % 29.94/7.78 |-Branch one: % 29.94/7.78 | (278) all_120_0_98 = all_0_1_1 & triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 & update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (278) yields: % 29.94/7.78 | (279) all_120_0_98 = all_0_1_1 % 29.94/7.78 | (280) triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 % 29.94/7.78 | (281) update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.78 | % 29.94/7.78 | From (189) and (281) follows: % 29.94/7.78 | (282) update_slb(all_0_5_5, all_0_2_2) = all_120_1_99 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_120_1_99, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_120_1_99, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.78 | (283) all_120_1_99 = all_61_3_80 % 29.94/7.78 | % 29.94/7.78 | From (283) and (280) follows: % 29.94/7.78 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.78 | (443) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (19) with all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.78 | (444) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.78 | % 29.94/7.78 | Instantiating (444) with all_238_0_433 yields: % 29.94/7.78 | (645) (all_238_0_433 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_238_0_433 = 0) & check_cpq(all_0_1_1) = all_238_0_433) % 29.94/7.78 | % 29.94/7.78 +-Applying beta-rule and splitting (645), into two cases. % 29.94/7.78 |-Branch one: % 29.94/7.78 | (646) all_238_0_433 = 0 & less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (646) yields: % 29.94/7.78 | (647) all_238_0_433 = 0 % 29.94/7.78 | (452) less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.78 | % 29.94/7.78 +-Applying beta-rule and splitting (443), into two cases. % 29.94/7.78 |-Branch one: % 29.94/7.78 | (146) all_57_0_74 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (146) can reduce 134 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.78 | (134) ~ (all_57_0_74 = 0) % 29.94/7.78 | (449) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (15) with all_0_2_2, all_0_0_0, 0, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, less_than(all_0_2_2, all_0_0_0) = 0, yields: % 29.94/7.78 | (146) all_57_0_74 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (146) can reduce 134 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.78 | (655) ~ (all_238_0_433 = 0) & check_cpq(all_0_1_1) = all_238_0_433 % 29.94/7.78 | % 29.94/7.78 | Applying alpha-rule on (655) yields: % 29.94/7.78 | (656) ~ (all_238_0_433 = 0) % 29.94/7.78 | (657) check_cpq(all_0_1_1) = all_238_0_433 % 29.94/7.78 | % 29.94/7.78 | Instantiating formula (13) with all_0_1_1, all_238_0_433, 0 and discharging atoms check_cpq(all_0_1_1) = all_238_0_433, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.78 | (647) all_238_0_433 = 0 % 29.94/7.78 | % 29.94/7.78 | Equations (647) can reduce 656 to: % 29.94/7.78 | (149) $false % 29.94/7.78 | % 29.94/7.78 |-The branch is then unsatisfiable % 29.94/7.78 |-Branch two: % 29.94/7.79 | (302) all_120_1_99 = 0 & contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (302) yields: % 29.94/7.79 | (303) all_120_1_99 = 0 % 29.94/7.79 | (304) contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.79 | % 29.94/7.79 | From (189) and (304) follows: % 29.94/7.79 | (305) contains_slb(all_0_5_5, all_0_2_2) = 0 % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (339), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (351) all_109_0_92 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (351) can reduce 273 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (273) ~ (all_109_0_92 = 0) % 29.94/7.79 | (354) ? [v0] : ((v0 = 0 & less_than(all_109_1_93, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_2_2, all_109_1_93) = v0)) % 29.94/7.79 | % 29.94/7.79 | Instantiating (354) with all_224_0_445 yields: % 29.94/7.79 | (668) (all_224_0_445 = 0 & less_than(all_109_1_93, all_0_2_2) = 0) | ( ~ (all_224_0_445 = 0) & less_than(all_0_2_2, all_109_1_93) = all_224_0_445) % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (181), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (306) (all_115_0_95 = all_0_1_1 & triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, all_115_2_97) = all_115_1_96) | ( ~ (all_115_0_95 = 0) & lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 & less_than(all_115_1_96, all_115_2_97) = all_115_0_95) % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (306), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (307) all_115_0_95 = all_0_1_1 & triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 & update_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (307) yields: % 29.94/7.79 | (308) all_115_0_95 = all_0_1_1 % 29.94/7.79 | (309) triple(all_0_6_6, all_115_1_96, all_0_4_4) = all_0_1_1 % 29.94/7.79 | (310) update_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.79 | % 29.94/7.79 | From (193) and (310) follows: % 29.94/7.79 | (311) update_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_115_1_96, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_115_1_96, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.79 | (312) all_115_1_96 = all_61_3_80 % 29.94/7.79 | % 29.94/7.79 | From (312) and (309) follows: % 29.94/7.79 | (313) triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1 % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_1_1, all_0_4_4, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.79 | (443) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (19) with all_0_2_2, all_0_0_0, all_0_1_1, all_0_4_4, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, all_0_4_4) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.79 | (444) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.79 | % 29.94/7.79 | Instantiating (444) with all_244_0_457 yields: % 29.94/7.79 | (679) (all_244_0_457 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_244_0_457 = 0) & check_cpq(all_0_1_1) = all_244_0_457) % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (679), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (680) all_244_0_457 = 0 & less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (680) yields: % 29.94/7.79 | (681) all_244_0_457 = 0 % 29.94/7.79 | (452) less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (443), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (146) all_57_0_74 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (146) can reduce 134 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (134) ~ (all_57_0_74 = 0) % 29.94/7.79 | (449) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (15) with all_0_2_2, all_0_0_0, 0, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, less_than(all_0_2_2, all_0_0_0) = 0, yields: % 29.94/7.79 | (146) all_57_0_74 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (146) can reduce 134 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (689) ~ (all_244_0_457 = 0) & check_cpq(all_0_1_1) = all_244_0_457 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (689) yields: % 29.94/7.79 | (690) ~ (all_244_0_457 = 0) % 29.94/7.79 | (691) check_cpq(all_0_1_1) = all_244_0_457 % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (13) with all_0_1_1, all_244_0_457, 0 and discharging atoms check_cpq(all_0_1_1) = all_244_0_457, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.79 | (681) all_244_0_457 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (681) can reduce 690 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (331) ~ (all_115_0_95 = 0) & lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 & less_than(all_115_1_96, all_115_2_97) = all_115_0_95 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (331) yields: % 29.94/7.79 | (332) ~ (all_115_0_95 = 0) % 29.94/7.79 | (333) lookup_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.79 | (334) less_than(all_115_1_96, all_115_2_97) = all_115_0_95 % 29.94/7.79 | % 29.94/7.79 | From (193) and (333) follows: % 29.94/7.79 | (335) lookup_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.94/7.79 | % 29.94/7.79 | From (193) and (334) follows: % 29.94/7.79 | (336) less_than(all_115_1_96, all_0_2_2) = all_115_0_95 % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (55) with all_0_5_5, all_0_2_2, all_115_1_96, all_109_1_93 and discharging atoms lookup_slb(all_0_5_5, all_0_2_2) = all_115_1_96, lookup_slb(all_0_5_5, all_0_2_2) = all_109_1_93, yields: % 29.94/7.79 | (337) all_115_1_96 = all_109_1_93 % 29.94/7.79 | % 29.94/7.79 | From (337) and (336) follows: % 29.94/7.79 | (338) less_than(all_109_1_93, all_0_2_2) = all_115_0_95 % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (668), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (702) all_224_0_445 = 0 & less_than(all_109_1_93, all_0_2_2) = 0 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (702) yields: % 29.94/7.79 | (703) all_224_0_445 = 0 % 29.94/7.79 | (507) less_than(all_109_1_93, all_0_2_2) = 0 % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (15) with all_109_1_93, all_0_2_2, 0, all_115_0_95 and discharging atoms less_than(all_109_1_93, all_0_2_2) = all_115_0_95, less_than(all_109_1_93, all_0_2_2) = 0, yields: % 29.94/7.79 | (343) all_115_0_95 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (343) can reduce 332 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (707) ~ (all_224_0_445 = 0) & less_than(all_0_2_2, all_109_1_93) = all_224_0_445 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (707) yields: % 29.94/7.79 | (708) ~ (all_224_0_445 = 0) % 29.94/7.79 | (709) less_than(all_0_2_2, all_109_1_93) = all_224_0_445 % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (41) with all_115_0_95, all_109_1_93, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6 and discharging atoms triple(all_0_6_6, all_0_5_5, all_0_4_4) = all_0_3_3, less_than(all_109_1_93, all_0_2_2) = all_115_0_95, yields: % 29.94/7.79 | (513) all_115_0_95 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_3_3) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_5_5, all_0_2_2, all_109_1_93) = v0)) % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (37) with all_115_0_95, all_0_2_2, all_0_0_0, all_109_1_93 and discharging atoms less_than(all_109_1_93, all_0_2_2) = all_115_0_95, less_than(all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.79 | (514) all_115_0_95 = 0 | ? [v0] : ( ~ (v0 = 0) & less_than(all_109_1_93, all_0_0_0) = v0) % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (28) with all_224_0_445, all_0_2_2, all_109_1_93 and discharging atoms less_than(all_0_2_2, all_109_1_93) = all_224_0_445, yields: % 29.94/7.79 | (712) all_224_0_445 = 0 | less_than(all_109_1_93, all_0_2_2) = 0 % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (712), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (507) less_than(all_109_1_93, all_0_2_2) = 0 % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (513), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (343) all_115_0_95 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (343) can reduce 332 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (332) ~ (all_115_0_95 = 0) % 29.94/7.79 | (524) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_3_3) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_5_5, all_0_2_2, all_109_1_93) = v0)) % 29.94/7.79 | % 29.94/7.79 +-Applying beta-rule and splitting (514), into two cases. % 29.94/7.79 |-Branch one: % 29.94/7.79 | (343) all_115_0_95 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (343) can reduce 332 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (332) ~ (all_115_0_95 = 0) % 29.94/7.79 | (519) ? [v0] : ( ~ (v0 = 0) & less_than(all_109_1_93, all_0_0_0) = v0) % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (15) with all_109_1_93, all_0_2_2, 0, all_115_0_95 and discharging atoms less_than(all_109_1_93, all_0_2_2) = all_115_0_95, less_than(all_109_1_93, all_0_2_2) = 0, yields: % 29.94/7.79 | (343) all_115_0_95 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (343) can reduce 332 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (527) ~ (less_than(all_109_1_93, all_0_2_2) = 0) % 29.94/7.79 | (703) all_224_0_445 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (703) can reduce 708 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (365) ~ (all_115_1_96 = 0) & contains_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (365) yields: % 29.94/7.79 | (366) ~ (all_115_1_96 = 0) % 29.94/7.79 | (367) contains_slb(all_0_5_5, all_115_2_97) = all_115_1_96 % 29.94/7.79 | % 29.94/7.79 | From (193) and (367) follows: % 29.94/7.79 | (368) contains_slb(all_0_5_5, all_0_2_2) = all_115_1_96 % 29.94/7.79 | % 29.94/7.79 | Instantiating formula (46) with all_0_5_5, all_0_2_2, all_115_1_96, 0 and discharging atoms contains_slb(all_0_5_5, all_0_2_2) = all_115_1_96, contains_slb(all_0_5_5, all_0_2_2) = 0, yields: % 29.94/7.79 | (369) all_115_1_96 = 0 % 29.94/7.79 | % 29.94/7.79 | Equations (369) can reduce 366 to: % 29.94/7.79 | (149) $false % 29.94/7.79 | % 29.94/7.79 |-The branch is then unsatisfiable % 29.94/7.79 |-Branch two: % 29.94/7.79 | (371) ~ (all_109_1_93 = 0) & contains_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.79 | % 29.94/7.79 | Applying alpha-rule on (371) yields: % 29.94/7.79 | (372) ~ (all_109_1_93 = 0) % 29.94/7.79 | (373) contains_slb(all_0_5_5, all_109_2_94) = all_109_1_93 % 29.94/7.79 | % 29.94/7.79 | From (194) and (373) follows: % 29.94/7.80 | (374) contains_slb(all_0_5_5, all_0_2_2) = all_109_1_93 % 29.94/7.80 | % 29.94/7.80 +-Applying beta-rule and splitting (188), into two cases. % 29.94/7.80 |-Branch one: % 29.94/7.80 | (278) all_120_0_98 = all_0_1_1 & triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 & update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.80 | % 29.94/7.80 | Applying alpha-rule on (278) yields: % 29.94/7.80 | (279) all_120_0_98 = all_0_1_1 % 29.94/7.80 | (280) triple(all_0_6_6, all_120_1_99, bad) = all_0_1_1 % 29.94/7.80 | (281) update_slb(all_0_5_5, all_120_2_100) = all_120_1_99 % 29.94/7.80 | % 29.94/7.80 | From (189) and (281) follows: % 29.94/7.80 | (282) update_slb(all_0_5_5, all_0_2_2) = all_120_1_99 % 29.94/7.80 | % 29.94/7.80 | Instantiating formula (58) with all_0_5_5, all_0_2_2, all_120_1_99, all_61_3_80 and discharging atoms update_slb(all_0_5_5, all_0_2_2) = all_120_1_99, update_slb(all_0_5_5, all_0_2_2) = all_61_3_80, yields: % 29.94/7.80 | (283) all_120_1_99 = all_61_3_80 % 29.94/7.80 | % 29.94/7.80 | From (283) and (280) follows: % 29.94/7.80 | (259) triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1 % 29.94/7.80 | % 29.94/7.80 | Instantiating formula (41) with all_57_0_74, all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, less_than(all_0_2_2, all_0_0_0) = all_57_0_74, yields: % 29.94/7.80 | (443) all_57_0_74 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.80 | % 29.94/7.80 | Instantiating formula (19) with all_0_2_2, all_0_0_0, all_0_1_1, bad, all_61_3_80, all_0_6_6 and discharging atoms triple(all_0_6_6, all_61_3_80, bad) = all_0_1_1, pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = 0, yields: % 29.94/7.80 | (444) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0)) % 29.94/7.80 | % 29.94/7.80 | Instantiating (444) with all_232_0_482 yields: % 29.94/7.80 | (746) (all_232_0_482 = 0 & less_than(all_0_2_2, all_0_0_0) = 0) | ( ~ (all_232_0_482 = 0) & check_cpq(all_0_1_1) = all_232_0_482) % 29.94/7.80 | % 29.94/7.80 +-Applying beta-rule and splitting (443), into two cases. % 29.94/7.80 |-Branch one: % 29.94/7.80 | (146) all_57_0_74 = 0 % 29.94/7.80 | % 29.94/7.80 | Equations (146) can reduce 134 to: % 29.94/7.80 | (149) $false % 29.94/7.80 | % 29.94/7.80 |-The branch is then unsatisfiable % 29.94/7.80 |-Branch two: % 29.94/7.80 | (134) ~ (all_57_0_74 = 0) % 29.94/7.80 | (449) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_1_1) = v0) | ( ~ (v0 = 0) & pair_in_list(all_61_3_80, all_0_0_0, all_0_2_2) = v0)) % 29.94/7.80 | % 29.94/7.80 +-Applying beta-rule and splitting (746), into two cases. % 29.94/7.80 |-Branch one: % 29.94/7.80 | (751) all_232_0_482 = 0 & less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.80 | % 29.94/7.80 | Applying alpha-rule on (751) yields: % 29.94/7.80 | (752) all_232_0_482 = 0 % 29.94/7.80 | (452) less_than(all_0_2_2, all_0_0_0) = 0 % 29.94/7.80 | % 29.94/7.80 | Instantiating formula (15) with all_0_2_2, all_0_0_0, 0, all_57_0_74 and discharging atoms less_than(all_0_2_2, all_0_0_0) = all_57_0_74, less_than(all_0_2_2, all_0_0_0) = 0, yields: % 29.94/7.80 | (146) all_57_0_74 = 0 % 29.94/7.80 | % 29.94/7.80 | Equations (146) can reduce 134 to: % 29.94/7.80 | (149) $false % 29.94/7.80 | % 29.94/7.80 |-The branch is then unsatisfiable % 29.94/7.80 |-Branch two: % 29.94/7.80 | (756) ~ (all_232_0_482 = 0) & check_cpq(all_0_1_1) = all_232_0_482 % 29.94/7.80 | % 29.94/7.80 | Applying alpha-rule on (756) yields: % 29.94/7.80 | (757) ~ (all_232_0_482 = 0) % 29.94/7.80 | (758) check_cpq(all_0_1_1) = all_232_0_482 % 29.94/7.80 | % 29.94/7.80 | Instantiating formula (13) with all_0_1_1, all_232_0_482, 0 and discharging atoms check_cpq(all_0_1_1) = all_232_0_482, check_cpq(all_0_1_1) = 0, yields: % 29.94/7.80 | (752) all_232_0_482 = 0 % 29.94/7.80 | % 29.94/7.80 | Equations (752) can reduce 757 to: % 29.94/7.80 | (149) $false % 29.94/7.80 | % 29.94/7.80 |-The branch is then unsatisfiable % 29.94/7.80 |-Branch two: % 29.94/7.80 | (302) all_120_1_99 = 0 & contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.80 | % 29.94/7.80 | Applying alpha-rule on (302) yields: % 29.94/7.80 | (303) all_120_1_99 = 0 % 29.94/7.80 | (304) contains_slb(all_0_5_5, all_120_2_100) = 0 % 29.94/7.80 | % 29.94/7.80 | From (189) and (304) follows: % 29.94/7.80 | (305) contains_slb(all_0_5_5, all_0_2_2) = 0 % 29.94/7.80 | % 29.94/7.80 | Instantiating formula (46) with all_0_5_5, all_0_2_2, 0, all_109_1_93 and discharging atoms contains_slb(all_0_5_5, all_0_2_2) = all_109_1_93, contains_slb(all_0_5_5, all_0_2_2) = 0, yields: % 29.94/7.80 | (403) all_109_1_93 = 0 % 29.94/7.80 | % 29.94/7.80 | Equations (403) can reduce 372 to: % 29.94/7.80 | (149) $false % 29.94/7.80 | % 29.94/7.80 |-The branch is then unsatisfiable % 29.94/7.80 |-Branch two: % 29.94/7.80 | (767) ~ (all_61_4_81 = 0) & contains_slb(all_0_5_5, all_0_0_0) = all_61_4_81 % 29.94/7.80 | % 29.94/7.80 | Applying alpha-rule on (767) yields: % 29.94/7.80 | (768) ~ (all_61_4_81 = 0) % 29.94/7.80 | (769) contains_slb(all_0_5_5, all_0_0_0) = all_61_4_81 % 29.94/7.80 | % 29.94/7.80 | Instantiating formula (46) with all_0_5_5, all_0_0_0, all_61_4_81, 0 and discharging atoms contains_slb(all_0_5_5, all_0_0_0) = all_61_4_81, contains_slb(all_0_5_5, all_0_0_0) = 0, yields: % 29.94/7.80 | (770) all_61_4_81 = 0 % 29.94/7.80 | % 29.94/7.80 | Equations (770) can reduce 768 to: % 29.94/7.80 | (149) $false % 29.94/7.80 | % 29.94/7.80 |-The branch is then unsatisfiable % 29.94/7.80 |-Branch two: % 29.94/7.80 | (772) ~ (findmin_pqp_res(all_0_6_6) = all_0_2_2) % 29.94/7.80 | (167) all_0_5_5 = create_slb % 29.94/7.80 | % 29.94/7.80 | From (167) and (126) follows: % 29.94/7.80 | (168) contains_slb(create_slb, all_0_0_0) = 0 % 29.94/7.80 | % 29.94/7.80 | Instantiating formula (25) with all_0_0_0 and discharging atoms contains_slb(create_slb, all_0_0_0) = 0, yields: % 29.94/7.80 | (169) $false % 29.94/7.80 | % 29.94/7.80 |-The branch is then unsatisfiable % 29.94/7.80 % SZS output end Proof for theBenchmark % 29.94/7.80 % 29.94/7.80 7136ms %------------------------------------------------------------------------------