%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SWV406+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n022.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:16 EDT 2022 % Result : Theorem 21.30s 5.61s % Output : Proof 23.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV406+1 : TPTP v8.1.0. Released v3.3.0. % 0.00/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n022.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 15 09:42:03 EDT 2022 % 0.13/0.34 % CPUTime : % 0.58/0.59 ____ _ % 0.58/0.59 ___ / __ \_____(_)___ ________ __________ % 0.58/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.58/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.58/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.58/0.59 % 0.58/0.59 A Theorem Prover for First-Order Logic % 0.58/0.59 (ePrincess v.1.0) % 0.58/0.59 % 0.58/0.59 (c) Philipp Rümmer, 2009-2015 % 0.58/0.59 (c) Peter Backeman, 2014-2015 % 0.58/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.58/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.58/0.59 Bug reports to peter@backeman.se % 0.58/0.59 % 0.58/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.58/0.59 % 0.58/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.71/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.81/0.98 Prover 0: Preprocessing ... % 2.85/1.32 Prover 0: Warning: ignoring some quantifiers % 3.22/1.35 Prover 0: Constructing countermodel ... % 6.66/2.22 Prover 0: gave up % 6.66/2.22 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 7.14/2.27 Prover 1: Preprocessing ... % 7.57/2.38 Prover 1: Constructing countermodel ... % 20.00/5.38 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 20.40/5.44 Prover 2: Preprocessing ... % 20.82/5.53 Prover 2: Warning: ignoring some quantifiers % 20.82/5.53 Prover 2: Constructing countermodel ... % 21.30/5.60 Prover 2: proved (223ms) % 21.30/5.61 Prover 1: stopped % 21.30/5.61 % 21.30/5.61 No countermodel exists, formula is valid % 21.30/5.61 % SZS status Theorem for theBenchmark % 21.30/5.61 % 21.30/5.61 Generating proof ... Warning: ignoring some quantifiers % 23.14/6.04 found it (size 162) % 23.14/6.05 % 23.14/6.05 % SZS output start Proof for theBenchmark % 23.14/6.05 Assumed formulas after preprocessing and simplification: % 23.14/6.05 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v0 = 0) & triple(v2, v7, v3) = v8 & check_cpq(v8) = v9 & pair(v4, v5) = v6 & insert_slb(v1, v6) = v7 & isnonempty_slb(create_slb) = v0 & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : (v21 = 0 | ~ (pair_in_list(v20, v16, v18) = v21) | ~ (pair(v15, v17) = v19) | ~ (insert_slb(v14, v19) = v20) | ? [v22] : ( ~ (v22 = 0) & pair_in_list(v14, v16, v18) = v22)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (insert_pqp(v14, v17) = v18) | ~ (triple(v18, v20, v16) = v21) | ~ (pair(v17, bottom) = v19) | ~ (insert_slb(v15, v19) = v20) | ? [v22] : (triple(v14, v15, v16) = v22 & insert_cpq(v22, v17) = v21)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (triple(v14, v20, v16) = v21) | ~ (pair(v17, v18) = v19) | ~ (insert_slb(v15, v19) = v20) | ? [v22] : ? [v23] : ? [v24] : (( ~ (v22 = 0) & less_than(v18, v17) = v22) | (((v24 = 0 & triple(v14, v15, v16) = v23 & check_cpq(v23) = 0) | ( ~ (v22 = 0) & check_cpq(v21) = v22)) & ((v22 = 0 & check_cpq(v21) = 0) | ( ~ (v24 = 0) & triple(v14, v15, v16) = v23 & check_cpq(v23) = v24))))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ! [v21] : ( ~ (triple(v14, v20, v16) = v21) | ~ (pair(v17, v18) = v19) | ~ (insert_slb(v15, v19) = v20) | ? [v22] : (( ~ (v22 = 0) & check_cpq(v21) = v22) | ( ~ (v22 = 0) & strictly_less_than(v17, v18) = v22))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v20 = 0 | ~ (contains_slb(v19, v16) = v20) | ~ (pair(v15, v17) = v18) | ~ (insert_slb(v14, v18) = v19) | ? [v21] : ( ~ (v21 = 0) & contains_slb(v14, v16) = v21)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v18 = v17 | ~ (pair_in_list(v20, v16, v18) = 0) | ~ (pair(v15, v17) = v19) | ~ (insert_slb(v14, v19) = v20) | pair_in_list(v14, v16, v18) = 0) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v16 = v15 | ~ (lookup_slb(v19, v16) = v20) | ~ (pair(v15, v17) = v18) | ~ (insert_slb(v14, v18) = v19) | ? [v21] : ((v21 = v20 & lookup_slb(v14, v16) = v20) | ( ~ (v21 = 0) & contains_slb(v14, v16) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v16 = v15 | ~ (remove_slb(v19, v16) = v20) | ~ (pair(v15, v17) = v18) | ~ (insert_slb(v14, v18) = v19) | ? [v21] : ? [v22] : ((v22 = v20 & remove_slb(v14, v16) = v21 & insert_slb(v21, v18) = v20) | ( ~ (v21 = 0) & contains_slb(v14, v16) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v16 = v15 | ~ (remove_slb(v14, v16) = v19) | ~ (pair(v15, v17) = v18) | ~ (insert_slb(v19, v18) = v20) | ? [v21] : ? [v22] : ((v22 = v20 & remove_slb(v21, v16) = v20 & insert_slb(v14, v18) = v21) | ( ~ (v21 = 0) & contains_slb(v14, v16) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : (v16 = v15 | ~ (pair_in_list(v20, v16, v18) = 0) | ~ (pair(v15, v17) = v19) | ~ (insert_slb(v14, v19) = v20) | pair_in_list(v14, v16, v18) = 0) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (remove_pqp(v14, v17) = v18) | ~ (triple(v18, v19, v16) = v20) | ~ (remove_slb(v15, v17) = v19) | ? [v21] : ? [v22] : ((v22 = v20 & triple(v14, v15, v16) = v21 & remove_cpq(v21, v17) = v20) | ( ~ (v22 = 0) & lookup_slb(v15, v17) = v21 & less_than(v21, v17) = v22) | ( ~ (v21 = 0) & contains_slb(v15, v17) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (update_slb(v19, v16) = v20) | ~ (pair(v15, v17) = v18) | ~ (insert_slb(v14, v18) = v19) | ? [v21] : ? [v22] : ? [v23] : ((v23 = v20 & update_slb(v14, v16) = v21 & pair(v15, v16) = v22 & insert_slb(v21, v22) = v20) | ( ~ (v21 = 0) & strictly_less_than(v17, v16) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (update_slb(v19, v16) = v20) | ~ (pair(v15, v17) = v18) | ~ (insert_slb(v14, v18) = v19) | ? [v21] : ? [v22] : ((v22 = v20 & update_slb(v14, v16) = v21 & insert_slb(v21, v18) = v20) | ( ~ (v21 = 0) & less_than(v16, v17) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ! [v20] : ( ~ (update_slb(v14, v16) = v19) | ~ (pair(v15, v17) = v18) | ~ (insert_slb(v19, v18) = v20) | ? [v21] : ? [v22] : ((v22 = v20 & update_slb(v21, v16) = v20 & insert_slb(v14, v18) = v21) | ( ~ (v21 = 0) & less_than(v16, v17) = v21))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = 0 | ~ (contains_cpq(v18, v17) = v19) | ~ (triple(v14, v15, v16) = v18) | ? [v20] : ( ~ (v20 = 0) & contains_slb(v15, v17) = v20)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = 0 | ~ (triple(v14, v1, v15) = v16) | ~ (less_than(v18, v17) = v19) | ? [v20] : (( ~ (v20 = 0) & check_cpq(v16) = v20) | ( ~ (v20 = 0) & pair_in_list(v1, v17, v18) = v20))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = 0 | ~ (pair_in_list(v18, v15, v16) = v19) | ~ (pair(v15, v16) = v17) | ~ (insert_slb(v14, v17) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v19 = 0 | ~ (contains_slb(v18, v15) = v19) | ~ (pair(v15, v16) = v17) | ~ (insert_slb(v14, v17) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v16 = v15 | ~ (contains_slb(v19, v16) = 0) | ~ (pair(v15, v17) = v18) | ~ (insert_slb(v14, v18) = v19) | contains_slb(v14, v16) = 0) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : (v15 = create_slb | ~ (findmin_pqp_res(v14) = v17) | ~ (triple(v14, v18, v16) = v19) | ~ (update_slb(v15, v17) = v18) | ? [v20] : ? [v21] : ((v21 = v19 & triple(v14, v15, v16) = v20 & findmin_cpq_eff(v20) = v19) | ( ~ (v21 = 0) & lookup_slb(v15, v17) = v20 & less_than(v20, v17) = v21) | ( ~ (v20 = 0) & contains_slb(v15, v17) = v20))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (triple(v14, v15, v16) = v18) | ~ (remove_cpq(v18, v17) = v19) | ? [v20] : ? [v21] : ? [v22] : ((v22 = v19 & remove_pqp(v14, v17) = v20 & triple(v20, v21, v16) = v19 & remove_slb(v15, v17) = v21) | ( ~ (v21 = 0) & lookup_slb(v15, v17) = v20 & less_than(v20, v17) = v21) | ( ~ (v20 = 0) & contains_slb(v15, v17) = v20))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (triple(v14, v15, v16) = v18) | ~ (remove_cpq(v18, v17) = v19) | ? [v20] : ? [v21] : ? [v22] : ((v22 = v19 & remove_pqp(v14, v17) = v20 & triple(v20, v21, bad) = v19 & remove_slb(v15, v17) = v21) | ( ~ (v21 = 0) & lookup_slb(v15, v17) = v20 & strictly_less_than(v17, v20) = v21) | ( ~ (v20 = 0) & contains_slb(v15, v17) = v20))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (triple(v14, v15, v16) = v18) | ~ (remove_cpq(v18, v17) = v19) | ? [v20] : ((v20 = v19 & triple(v14, v15, bad) = v19) | (v20 = 0 & contains_slb(v15, v17) = 0))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ! [v19] : ( ~ (triple(v14, v15, v16) = v18) | ~ (insert_cpq(v18, v17) = v19) | ? [v20] : ? [v21] : ? [v22] : (insert_pqp(v14, v17) = v20 & triple(v20, v22, v16) = v19 & pair(v17, bottom) = v21 & insert_slb(v15, v21) = v22)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = 0 | ~ (remove_cpq(v15, v16) = v17) | ~ (succ_cpq(v14, v17) = v18) | ? [v19] : ( ~ (v19 = 0) & succ_cpq(v14, v15) = v19)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v18 = 0 | ~ (insert_cpq(v15, v16) = v17) | ~ (succ_cpq(v14, v17) = v18) | ? [v19] : ( ~ (v19 = 0) & succ_cpq(v14, v15) = v19)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = v14 | ~ (triple(v18, v17, v16) = v15) | ~ (triple(v18, v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = v14 | ~ (pair_in_list(v18, v17, v16) = v15) | ~ (pair_in_list(v18, v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = create_slb | ~ (findmin_cpq_res(v17) = v18) | ~ (triple(v14, v15, v16) = v17) | findmin_pqp_res(v14) = v18) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = create_slb | ~ (triple(v14, v15, v16) = v17) | ~ (findmin_cpq_eff(v17) = v18) | ? [v19] : ? [v20] : ? [v21] : (findmin_pqp_res(v14) = v19 & ((v21 = v18 & triple(v14, v20, v16) = v18 & update_slb(v15, v19) = v20) | ( ~ (v21 = 0) & lookup_slb(v15, v19) = v20 & less_than(v20, v19) = v21) | ( ~ (v20 = 0) & contains_slb(v15, v19) = v20)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = create_slb | ~ (triple(v14, v15, v16) = v17) | ~ (findmin_cpq_eff(v17) = v18) | ? [v19] : ? [v20] : ? [v21] : (findmin_pqp_res(v14) = v19 & ((v21 = v18 & triple(v14, v20, bad) = v18 & update_slb(v15, v19) = v20) | (v20 = 0 & contains_slb(v15, v19) = 0)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : (v15 = create_slb | ~ (triple(v14, v15, v16) = v17) | ~ (findmin_cpq_eff(v17) = v18) | ? [v19] : ? [v20] : ? [v21] : (findmin_pqp_res(v14) = v19 & ((v21 = v18 & triple(v14, v20, bad) = v18 & update_slb(v15, v19) = v20) | ( ~ (v21 = 0) & lookup_slb(v15, v19) = v20 & strictly_less_than(v19, v20) = v21) | ( ~ (v20 = 0) & contains_slb(v15, v19) = v20)))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (contains_cpq(v18, v17) = 0) | ~ (triple(v14, v15, v16) = v18) | contains_slb(v15, v17) = 0) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (triple(v14, v1, v15) = v16) | ~ (pair_in_list(v1, v17, v18) = 0) | ? [v19] : ((v19 = 0 & less_than(v18, v17) = 0) | ( ~ (v19 = 0) & check_cpq(v16) = v19))) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (pair(v15, v16) = v17) | ~ (insert_slb(v14, v17) = v18) | lookup_slb(v18, v15) = v16) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (pair(v15, v16) = v17) | ~ (insert_slb(v14, v17) = v18) | remove_slb(v18, v15) = v14) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (pair(v15, v16) = v17) | ~ (insert_slb(v14, v17) = v18) | isnonempty_slb(v18) = 0) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (removemin_cpq_eff(v15) = v16) | ~ (succ_cpq(v14, v16) = v17) | ? [v18] : ( ~ (v18 = 0) & succ_cpq(v14, v15) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (findmin_cpq_eff(v15) = v16) | ~ (succ_cpq(v14, v16) = v17) | ? [v18] : ( ~ (v18 = 0) & succ_cpq(v14, v15) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (less_than(v15, v16) = 0) | ~ (less_than(v14, v16) = v17) | ? [v18] : ( ~ (v18 = 0) & less_than(v14, v15) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v17 = 0 | ~ (less_than(v14, v16) = v17) | ~ (less_than(v14, v15) = 0) | ? [v18] : ( ~ (v18 = 0) & less_than(v15, v16) = v18)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v16 = bad | ~ (triple(v14, v15, v16) = v17) | ok(v17) = 0) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (remove_pqp(v17, v16) = v15) | ~ (remove_pqp(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (insert_pqp(v17, v16) = v15) | ~ (insert_pqp(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (contains_cpq(v17, v16) = v15) | ~ (contains_cpq(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (remove_cpq(v17, v16) = v15) | ~ (remove_cpq(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (insert_cpq(v17, v16) = v15) | ~ (insert_cpq(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (succ_cpq(v17, v16) = v15) | ~ (succ_cpq(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (update_slb(v17, v16) = v15) | ~ (update_slb(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (lookup_slb(v17, v16) = v15) | ~ (lookup_slb(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (remove_slb(v17, v16) = v15) | ~ (remove_slb(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (contains_slb(v17, v16) = v15) | ~ (contains_slb(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (pair(v17, v16) = v15) | ~ (pair(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (insert_slb(v17, v16) = v15) | ~ (insert_slb(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (strictly_less_than(v17, v16) = v15) | ~ (strictly_less_than(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v15 = v14 | ~ (less_than(v17, v16) = v15) | ~ (less_than(v17, v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (strictly_less_than(v14, v15) = v16) | ? [v17] : ((v17 = 0 & less_than(v15, v14) = 0) | ( ~ (v17 = 0) & less_than(v14, v15) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (less_than(v15, v14) = v16) | less_than(v14, v15) = 0) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (less_than(v15, v14) = v16) | ? [v17] : ((v17 = 0 & strictly_less_than(v14, v15) = 0) | ( ~ (v17 = 0) & less_than(v14, v15) = v17))) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (less_than(v14, v15) = v16) | less_than(v15, v14) = 0) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (removemin_cpq_res(v16) = v15) | ~ (removemin_cpq_res(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (findmin_cpq_res(v16) = v15) | ~ (findmin_cpq_res(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (findmin_pqp_res(v16) = v15) | ~ (findmin_pqp_res(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (ok(v16) = v15) | ~ (ok(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (check_cpq(v16) = v15) | ~ (check_cpq(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (removemin_cpq_eff(v16) = v15) | ~ (removemin_cpq_eff(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (findmin_cpq_eff(v16) = v15) | ~ (findmin_cpq_eff(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (isnonempty_slb(v16) = v15) | ~ (isnonempty_slb(v16) = v14)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (triple(v14, v15, bad) = v16) | ? [v17] : ( ~ (v17 = 0) & ok(v16) = v17)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (triple(v14, v1, v15) = v16) | ? [v17] : ? [v18] : ? [v19] : ? [v20] : ((v19 = 0 & ~ (v20 = 0) & pair_in_list(v1, v17, v18) = 0 & less_than(v18, v17) = v20) | (v17 = 0 & check_cpq(v16) = 0))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (triple(v14, create_slb, v15) = v16) | findmin_cpq_res(v16) = bottom) & ! [v14] : ! [v15] : ! [v16] : ( ~ (triple(v14, create_slb, v15) = v16) | check_cpq(v16) = 0) & ! [v14] : ! [v15] : ! [v16] : ( ~ (triple(v14, create_slb, v15) = v16) | ? [v17] : (triple(v14, create_slb, bad) = v17 & findmin_cpq_eff(v16) = v17)) & ! [v14] : ! [v15] : ! [v16] : ( ~ (less_than(v15, v16) = 0) | ~ (less_than(v14, v15) = 0) | less_than(v14, v16) = 0) & ! [v14] : ! [v15] : ! [v16] : ( ~ (less_than(v15, v14) = v16) | ? [v17] : ((v17 = 0 & ~ (v16 = 0) & less_than(v14, v15) = 0) | ( ~ (v17 = 0) & strictly_less_than(v14, v15) = v17))) & ! [v14] : ! [v15] : ! [v16] : ( ~ (less_than(v14, v15) = v16) | ? [v17] : ((v16 = 0 & ~ (v17 = 0) & less_than(v15, v14) = v17) | ( ~ (v17 = 0) & strictly_less_than(v14, v15) = v17))) & ! [v14] : ! [v15] : (v15 = create_slb | ~ (update_slb(create_slb, v14) = v15)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (succ_cpq(v14, v14) = v15)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (less_than(v14, v14) = v15)) & ! [v14] : ! [v15] : (v15 = 0 | ~ (less_than(bottom, v14) = v15)) & ! [v14] : ! [v15] : ( ~ (removemin_cpq_res(v14) = v15) | findmin_cpq_res(v14) = v15) & ! [v14] : ! [v15] : ( ~ (findmin_cpq_res(v14) = v15) | removemin_cpq_res(v14) = v15) & ! [v14] : ! [v15] : ( ~ (findmin_cpq_res(v14) = v15) | ? [v16] : ? [v17] : (removemin_cpq_eff(v14) = v16 & findmin_cpq_eff(v14) = v17 & remove_cpq(v17, v15) = v16)) & ! [v14] : ! [v15] : ( ~ (removemin_cpq_eff(v14) = v15) | ? [v16] : ? [v17] : (findmin_cpq_res(v14) = v17 & findmin_cpq_eff(v14) = v16 & remove_cpq(v16, v17) = v15)) & ! [v14] : ! [v15] : ( ~ (findmin_cpq_eff(v14) = v15) | ? [v16] : ? [v17] : (findmin_cpq_res(v14) = v17 & removemin_cpq_eff(v14) = v16 & remove_cpq(v15, v17) = v16)) & ! [v14] : ! [v15] : ( ~ (succ_cpq(v14, v15) = 0) | ? [v16] : (removemin_cpq_eff(v15) = v16 & succ_cpq(v14, v16) = 0)) & ! [v14] : ! [v15] : ( ~ (succ_cpq(v14, v15) = 0) | ? [v16] : (findmin_cpq_eff(v15) = v16 & succ_cpq(v14, v16) = 0)) & ! [v14] : ! [v15] : ~ (pair_in_list(create_slb, v14, v15) = 0) & ! [v14] : ! [v15] : ( ~ (strictly_less_than(v14, v15) = 0) | ? [v16] : ( ~ (v16 = 0) & less_than(v15, v14) = v16 & less_than(v14, v15) = 0)) & ! [v14] : ! [v15] : ( ~ (less_than(v14, v15) = 0) | ? [v16] : ((v16 = 0 & strictly_less_than(v14, v15) = 0) | (v16 = 0 & less_than(v15, v14) = 0))) & ! [v14] : ~ (contains_slb(create_slb, v14) = 0) & ? [v14] : ? [v15] : ? [v16] : ? [v17] : triple(v16, v15, v14) = v17 & ? [v14] : ? [v15] : ? [v16] : ? [v17] : pair_in_list(v16, v15, v14) = v17 & ? [v14] : ? [v15] : ? [v16] : remove_pqp(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : insert_pqp(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : contains_cpq(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : remove_cpq(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : insert_cpq(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : succ_cpq(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : update_slb(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : lookup_slb(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : remove_slb(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : contains_slb(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : pair(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : insert_slb(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : strictly_less_than(v15, v14) = v16 & ? [v14] : ? [v15] : ? [v16] : less_than(v15, v14) = v16 & ? [v14] : ? [v15] : removemin_cpq_res(v14) = v15 & ? [v14] : ? [v15] : findmin_cpq_res(v14) = v15 & ? [v14] : ? [v15] : findmin_pqp_res(v14) = v15 & ? [v14] : ? [v15] : ok(v14) = v15 & ? [v14] : ? [v15] : check_cpq(v14) = v15 & ? [v14] : ? [v15] : removemin_cpq_eff(v14) = v15 & ? [v14] : ? [v15] : findmin_cpq_eff(v14) = v15 & ? [v14] : ? [v15] : isnonempty_slb(v14) = v15 & ((v12 = 0 & v9 = 0 & ~ (v13 = 0) & pair_in_list(v7, v10, v11) = 0 & less_than(v11, v10) = v13) | ( ~ (v9 = 0) & ! [v14] : ! [v15] : ! [v16] : (v16 = 0 | ~ (less_than(v15, v14) = v16) | ? [v17] : ( ~ (v17 = 0) & pair_in_list(v7, v14, v15) = v17)) & ! [v14] : ! [v15] : ( ~ (pair_in_list(v7, v14, v15) = 0) | less_than(v15, v14) = 0)))) % 23.14/6.10 | 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, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13 yields: % 23.14/6.10 | (1) ~ (all_0_13_13 = 0) & triple(all_0_11_11, all_0_6_6, all_0_10_10) = all_0_5_5 & check_cpq(all_0_5_5) = all_0_4_4 & pair(all_0_9_9, all_0_8_8) = all_0_7_7 & insert_slb(all_0_12_12, all_0_7_7) = all_0_6_6 & isnonempty_slb(create_slb) = all_0_13_13 & ! [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 | ~ (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 | ~ (triple(v0, all_0_12_12, v1) = v2) | ~ (less_than(v4, v3) = v5) | ? [v6] : (( ~ (v6 = 0) & check_cpq(v2) = v6) | ( ~ (v6 = 0) & pair_in_list(all_0_12_12, v3, v4) = 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] : ( ~ (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] : (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] : ( ~ (triple(v0, all_0_12_12, v1) = v2) | ~ (pair_in_list(all_0_12_12, v3, v4) = 0) | ? [v5] : ((v5 = 0 & less_than(v4, v3) = 0) | ( ~ (v5 = 0) & check_cpq(v2) = v5))) & ! [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] : (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, all_0_12_12, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & ~ (v6 = 0) & pair_in_list(all_0_12_12, v3, v4) = 0 & less_than(v4, v3) = v6) | (v3 = 0 & check_cpq(v2) = 0))) & ! [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 & ((all_0_1_1 = 0 & all_0_4_4 = 0 & ~ (all_0_0_0 = 0) & pair_in_list(all_0_6_6, all_0_3_3, all_0_2_2) = 0 & less_than(all_0_2_2, all_0_3_3) = all_0_0_0) | ( ~ (all_0_4_4 = 0) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & pair_in_list(all_0_6_6, v0, v1) = v3)) & ! [v0] : ! [v1] : ( ~ (pair_in_list(all_0_6_6, v0, v1) = 0) | less_than(v1, v0) = 0))) % 23.56/6.12 | % 23.56/6.12 | Applying alpha-rule on (1) yields: % 23.56/6.13 | (2) ? [v0] : ? [v1] : findmin_cpq_eff(v0) = v1 % 23.56/6.13 | (3) ? [v0] : ? [v1] : ? [v2] : insert_slb(v1, v0) = v2 % 23.56/6.13 | (4) ? [v0] : ? [v1] : ? [v2] : contains_slb(v1, v0) = v2 % 23.56/6.13 | (5) ! [v0] : ! [v1] : ! [v2] : ( ~ (less_than(v1, v2) = 0) | ~ (less_than(v0, v1) = 0) | less_than(v0, v2) = 0) % 23.56/6.13 | (6) check_cpq(all_0_5_5) = all_0_4_4 % 23.56/6.13 | (7) ! [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))) % 23.56/6.13 | (8) ! [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)) % 23.56/6.13 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (strictly_less_than(v3, v2) = v1) | ~ (strictly_less_than(v3, v2) = v0)) % 23.56/6.13 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (pair(v3, v2) = v1) | ~ (pair(v3, v2) = v0)) % 23.56/6.13 | (11) ? [v0] : ? [v1] : ? [v2] : remove_cpq(v1, v0) = v2 % 23.56/6.13 | (12) ! [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))) % 23.56/6.13 | (13) ! [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)))) % 23.56/6.13 | (14) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v0, v1) = v2) | less_than(v1, v0) = 0) % 23.56/6.13 | (15) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | less_than(v0, v1) = 0) % 23.56/6.13 | (16) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_cpq_eff(v2) = v1) | ~ (findmin_cpq_eff(v2) = v0)) % 23.56/6.13 | (17) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_than(v0, v0) = v1)) % 23.56/6.13 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | remove_slb(v4, v1) = v0) % 23.56/6.13 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_cpq(v3, v2) = v1) | ~ (insert_cpq(v3, v2) = v0)) % 23.56/6.13 | (20) ! [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)) % 23.56/6.13 | (21) ! [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)) % 23.56/6.13 | (22) ! [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))) % 23.56/6.13 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | isnonempty_slb(v4) = 0) % 23.56/6.13 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | check_cpq(v2) = 0) % 23.56/6.13 | (25) ! [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) % 23.56/6.13 | (26) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_pqp_res(v2) = v1) | ~ (findmin_pqp_res(v2) = v0)) % 23.56/6.13 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (less_than(v0, v2) = v3) | ~ (less_than(v0, v1) = 0) | ? [v4] : ( ~ (v4 = 0) & less_than(v1, v2) = v4)) % 23.56/6.13 | (28) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (isnonempty_slb(v2) = v1) | ~ (isnonempty_slb(v2) = v0)) % 23.56/6.13 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_pqp(v3, v2) = v1) | ~ (remove_pqp(v3, v2) = v0)) % 23.56/6.13 | (30) ! [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))))) % 23.56/6.13 | (31) ! [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))) % 23.56/6.13 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (contains_slb(v3, v2) = v1) | ~ (contains_slb(v3, v2) = v0)) % 23.56/6.14 | (33) ? [v0] : ? [v1] : ? [v2] : contains_cpq(v1, v0) = v2 % 23.56/6.14 | (34) ! [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))) % 23.56/6.14 | (35) ! [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)))) % 23.56/6.14 | (36) ? [v0] : ? [v1] : ? [v2] : remove_pqp(v1, v0) = v2 % 23.56/6.14 | (37) ? [v0] : ? [v1] : isnonempty_slb(v0) = v1 % 23.56/6.14 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (triple(v4, v3, v2) = v1) | ~ (triple(v4, v3, v2) = v0)) % 23.56/6.14 | (39) ! [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)) % 23.56/6.14 | (40) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (ok(v2) = v1) | ~ (ok(v2) = v0)) % 23.56/6.14 | (41) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, v1, bad) = v2) | ? [v3] : ( ~ (v3 = 0) & ok(v2) = v3)) % 23.56/6.14 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = v0 | ~ (pair_in_list(v4, v3, v2) = v1) | ~ (pair_in_list(v4, v3, v2) = v0)) % 23.56/6.14 | (43) ! [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) % 23.56/6.14 | (44) ! [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))) % 23.56/6.14 | (45) ! [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)))) % 23.56/6.14 | (46) ? [v0] : ? [v1] : ? [v2] : ? [v3] : triple(v2, v1, v0) = v3 % 23.56/6.14 | (47) ! [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))) % 23.56/6.14 | (48) ! [v0] : ! [v1] : ( ~ (less_than(v0, v1) = 0) | ? [v2] : ((v2 = 0 & strictly_less_than(v0, v1) = 0) | (v2 = 0 & less_than(v1, v0) = 0))) % 23.56/6.14 | (49) ! [v0] : ~ (contains_slb(create_slb, v0) = 0) % 23.56/6.14 | (50) ! [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))) % 23.56/6.14 | (51) ! [v0] : ! [v1] : ~ (pair_in_list(create_slb, v0, v1) = 0) % 23.56/6.14 | (52) ? [v0] : ? [v1] : ? [v2] : remove_slb(v1, v0) = v2 % 23.56/6.14 | (53) ! [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))) % 23.56/6.14 | (54) ? [v0] : ? [v1] : ? [v2] : pair(v1, v0) = v2 % 23.56/6.14 | (55) ! [v0] : ! [v1] : ( ~ (strictly_less_than(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & less_than(v1, v0) = v2 & less_than(v0, v1) = 0)) % 23.56/6.14 | (56) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (succ_cpq(v3, v2) = v1) | ~ (succ_cpq(v3, v2) = v0)) % 23.56/6.14 | (57) ? [v0] : ? [v1] : findmin_cpq_res(v0) = v1 % 23.56/6.14 | (58) ? [v0] : ? [v1] : ? [v2] : update_slb(v1, v0) = v2 % 23.56/6.14 | (59) ! [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)) % 23.56/6.14 | (60) ? [v0] : ? [v1] : ? [v2] : ? [v3] : pair_in_list(v2, v1, v0) = v3 % 23.56/6.14 | (61) ? [v0] : ? [v1] : removemin_cpq_res(v0) = v1 % 23.56/6.14 | (62) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (findmin_cpq_eff(v1) = v2) | ~ (succ_cpq(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & succ_cpq(v0, v1) = v4)) % 23.56/6.14 | (63) ! [v0] : ! [v1] : ( ~ (findmin_cpq_res(v0) = v1) | removemin_cpq_res(v0) = v1) % 23.56/6.14 | (64) ! [v0] : ! [v1] : ( ~ (removemin_cpq_res(v0) = v1) | findmin_cpq_res(v0) = v1) % 23.56/6.14 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (removemin_cpq_res(v2) = v1) | ~ (removemin_cpq_res(v2) = v0)) % 23.56/6.14 | (66) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (contains_cpq(v4, v3) = 0) | ~ (triple(v0, v1, v2) = v4) | contains_slb(v1, v3) = 0) % 23.56/6.14 | (67) ? [v0] : ? [v1] : ? [v2] : insert_pqp(v1, v0) = v2 % 23.56/6.14 | (68) ? [v0] : ? [v1] : ? [v2] : succ_cpq(v1, v0) = v2 % 23.56/6.14 | (69) ! [v0] : ! [v1] : (v1 = create_slb | ~ (update_slb(create_slb, v0) = v1)) % 23.56/6.14 | (70) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (check_cpq(v2) = v1) | ~ (check_cpq(v2) = v0)) % 23.56/6.14 | (71) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (lookup_slb(v3, v2) = v1) | ~ (lookup_slb(v3, v2) = v0)) % 23.56/6.14 | (72) ? [v0] : ? [v1] : ? [v2] : lookup_slb(v1, v0) = v2 % 23.56/6.14 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (less_than(v3, v2) = v1) | ~ (less_than(v3, v2) = v0)) % 23.56/6.15 | (74) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (triple(v0, all_0_12_12, v1) = v2) | ~ (pair_in_list(all_0_12_12, v3, v4) = 0) | ? [v5] : ((v5 = 0 & less_than(v4, v3) = 0) | ( ~ (v5 = 0) & check_cpq(v2) = v5))) % 23.56/6.15 | (75) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (triple(v0, all_0_12_12, v1) = v2) | ~ (less_than(v4, v3) = v5) | ? [v6] : (( ~ (v6 = 0) & check_cpq(v2) = v6) | ( ~ (v6 = 0) & pair_in_list(all_0_12_12, v3, v4) = v6))) % 23.56/6.15 | (76) pair(all_0_9_9, all_0_8_8) = all_0_7_7 % 23.56/6.15 | (77) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (contains_slb(v4, v1) = v5) | ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4)) % 23.56/6.15 | (78) (all_0_1_1 = 0 & all_0_4_4 = 0 & ~ (all_0_0_0 = 0) & pair_in_list(all_0_6_6, all_0_3_3, all_0_2_2) = 0 & less_than(all_0_2_2, all_0_3_3) = all_0_0_0) | ( ~ (all_0_4_4 = 0) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & pair_in_list(all_0_6_6, v0, v1) = v3)) & ! [v0] : ! [v1] : ( ~ (pair_in_list(all_0_6_6, v0, v1) = 0) | less_than(v1, v0) = 0)) % 23.56/6.15 | (79) ! [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))) % 23.56/6.15 | (80) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | findmin_cpq_res(v2) = bottom) % 23.56/6.15 | (81) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (findmin_cpq_res(v2) = v1) | ~ (findmin_cpq_res(v2) = v0)) % 23.56/6.15 | (82) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_slb(v3, v2) = v1) | ~ (remove_slb(v3, v2) = v0)) % 23.56/6.15 | (83) ? [v0] : ? [v1] : findmin_pqp_res(v0) = v1 % 23.56/6.15 | (84) triple(all_0_11_11, all_0_6_6, all_0_10_10) = all_0_5_5 % 23.56/6.15 | (85) ! [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))) % 23.56/6.15 | (86) ! [v0] : ! [v1] : (v1 = 0 | ~ (less_than(bottom, v0) = v1)) % 23.56/6.15 | (87) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (less_than(v1, v2) = 0) | ~ (less_than(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & less_than(v0, v1) = v4)) % 23.56/6.15 | (88) ! [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) % 23.56/6.15 | (89) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4) | lookup_slb(v4, v1) = v2) % 23.56/6.15 | (90) ! [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))) % 23.56/6.15 | (91) ! [v0] : ! [v1] : ( ~ (findmin_cpq_res(v0) = v1) | ? [v2] : ? [v3] : (removemin_cpq_eff(v0) = v2 & findmin_cpq_eff(v0) = v3 & remove_cpq(v3, v1) = v2)) % 23.56/6.15 | (92) ! [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))) % 23.56/6.15 | (93) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (removemin_cpq_eff(v2) = v1) | ~ (removemin_cpq_eff(v2) = v0)) % 23.56/6.15 | (94) ! [v0] : ! [v1] : (v1 = 0 | ~ (succ_cpq(v0, v0) = v1)) % 23.56/6.15 | (95) ? [v0] : ? [v1] : ? [v2] : strictly_less_than(v1, v0) = v2 % 23.56/6.15 | (96) ! [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))) % 23.56/6.15 | (97) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (update_slb(v3, v2) = v1) | ~ (update_slb(v3, v2) = v0)) % 23.56/6.15 | (98) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, create_slb, v1) = v2) | ? [v3] : (triple(v0, create_slb, bad) = v3 & findmin_cpq_eff(v2) = v3)) % 23.56/6.15 | (99) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : (v5 = 0 | ~ (pair_in_list(v4, v1, v2) = v5) | ~ (pair(v1, v2) = v3) | ~ (insert_slb(v0, v3) = v4)) % 23.56/6.15 | (100) ? [v0] : ? [v1] : ? [v2] : insert_cpq(v1, v0) = v2 % 23.56/6.15 | (101) ? [v0] : ? [v1] : ok(v0) = v1 % 23.56/6.15 | (102) ! [v0] : ! [v1] : ( ~ (succ_cpq(v0, v1) = 0) | ? [v2] : (removemin_cpq_eff(v1) = v2 & succ_cpq(v0, v2) = 0)) % 23.56/6.15 | (103) ~ (all_0_13_13 = 0) % 23.56/6.15 | (104) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_pqp(v3, v2) = v1) | ~ (insert_pqp(v3, v2) = v0)) % 23.56/6.15 | (105) ! [v0] : ! [v1] : ! [v2] : ( ~ (triple(v0, all_0_12_12, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ((v5 = 0 & ~ (v6 = 0) & pair_in_list(all_0_12_12, v3, v4) = 0 & less_than(v4, v3) = v6) | (v3 = 0 & check_cpq(v2) = 0))) % 23.56/6.15 | (106) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = bad | ~ (triple(v0, v1, v2) = v3) | ok(v3) = 0) % 23.56/6.15 | (107) isnonempty_slb(create_slb) = all_0_13_13 % 23.56/6.15 | (108) ? [v0] : ? [v1] : ? [v2] : less_than(v1, v0) = v2 % 23.56/6.15 | (109) ! [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)) % 23.56/6.15 | (110) ? [v0] : ? [v1] : removemin_cpq_eff(v0) = v1 % 23.56/6.15 | (111) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v1 = create_slb | ~ (findmin_cpq_res(v3) = v4) | ~ (triple(v0, v1, v2) = v3) | findmin_pqp_res(v0) = v4) % 23.56/6.15 | (112) ! [v0] : ! [v1] : ( ~ (succ_cpq(v0, v1) = 0) | ? [v2] : (findmin_cpq_eff(v1) = v2 & succ_cpq(v0, v2) = 0)) % 23.56/6.15 | (113) ! [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))) % 23.56/6.16 | (114) ! [v0] : ! [v1] : ( ~ (findmin_cpq_eff(v0) = v1) | ? [v2] : ? [v3] : (findmin_cpq_res(v0) = v3 & removemin_cpq_eff(v0) = v2 & remove_cpq(v1, v3) = v2)) % 23.56/6.16 | (115) ! [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))) % 23.56/6.16 | (116) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (contains_cpq(v3, v2) = v1) | ~ (contains_cpq(v3, v2) = v0)) % 23.56/6.16 | (117) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = 0 | ~ (removemin_cpq_eff(v1) = v2) | ~ (succ_cpq(v0, v2) = v3) | ? [v4] : ( ~ (v4 = 0) & succ_cpq(v0, v1) = v4)) % 23.56/6.16 | (118) insert_slb(all_0_12_12, all_0_7_7) = all_0_6_6 % 23.56/6.16 | (119) ! [v0] : ! [v1] : ( ~ (removemin_cpq_eff(v0) = v1) | ? [v2] : ? [v3] : (findmin_cpq_res(v0) = v3 & findmin_cpq_eff(v0) = v2 & remove_cpq(v2, v3) = v1)) % 23.56/6.16 | (120) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (remove_cpq(v3, v2) = v1) | ~ (remove_cpq(v3, v2) = v0)) % 23.56/6.16 | (121) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (insert_slb(v3, v2) = v1) | ~ (insert_slb(v3, v2) = v0)) % 23.56/6.16 | (122) ! [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)) % 23.56/6.16 | (123) ? [v0] : ? [v1] : check_cpq(v0) = v1 % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (30) with all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_12_12, all_0_11_11 and discharging atoms triple(all_0_11_11, all_0_6_6, all_0_10_10) = all_0_5_5, pair(all_0_9_9, all_0_8_8) = all_0_7_7, insert_slb(all_0_12_12, all_0_7_7) = all_0_6_6, yields: % 23.56/6.16 | (124) ? [v0] : ? [v1] : ? [v2] : (( ~ (v0 = 0) & less_than(all_0_8_8, all_0_9_9) = v0) | (((v2 = 0 & triple(all_0_11_11, all_0_12_12, all_0_10_10) = v1 & check_cpq(v1) = 0) | ( ~ (v0 = 0) & check_cpq(all_0_5_5) = v0)) & ((v0 = 0 & check_cpq(all_0_5_5) = 0) | ( ~ (v2 = 0) & triple(all_0_11_11, all_0_12_12, all_0_10_10) = v1 & check_cpq(v1) = v2)))) % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (96) with all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_12_12, all_0_11_11 and discharging atoms triple(all_0_11_11, all_0_6_6, all_0_10_10) = all_0_5_5, pair(all_0_9_9, all_0_8_8) = all_0_7_7, insert_slb(all_0_12_12, all_0_7_7) = all_0_6_6, yields: % 23.56/6.16 | (125) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_0_5_5) = v0) | ( ~ (v0 = 0) & strictly_less_than(all_0_9_9, all_0_8_8) = v0)) % 23.56/6.16 | % 23.56/6.16 | Instantiating (125) with all_57_0_80 yields: % 23.56/6.16 | (126) ( ~ (all_57_0_80 = 0) & check_cpq(all_0_5_5) = all_57_0_80) | ( ~ (all_57_0_80 = 0) & strictly_less_than(all_0_9_9, all_0_8_8) = all_57_0_80) % 23.56/6.16 | % 23.56/6.16 | Instantiating (124) with all_58_0_81, all_58_1_82, all_58_2_83 yields: % 23.56/6.16 | (127) ( ~ (all_58_2_83 = 0) & less_than(all_0_8_8, all_0_9_9) = all_58_2_83) | (((all_58_0_81 = 0 & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = 0) | ( ~ (all_58_2_83 = 0) & check_cpq(all_0_5_5) = all_58_2_83)) & ((all_58_2_83 = 0 & check_cpq(all_0_5_5) = 0) | ( ~ (all_58_0_81 = 0) & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = all_58_0_81))) % 23.56/6.16 | % 23.56/6.16 +-Applying beta-rule and splitting (78), into two cases. % 23.56/6.16 |-Branch one: % 23.56/6.16 | (128) all_0_1_1 = 0 & all_0_4_4 = 0 & ~ (all_0_0_0 = 0) & pair_in_list(all_0_6_6, all_0_3_3, all_0_2_2) = 0 & less_than(all_0_2_2, all_0_3_3) = all_0_0_0 % 23.56/6.16 | % 23.56/6.16 | Applying alpha-rule on (128) yields: % 23.56/6.16 | (129) pair_in_list(all_0_6_6, all_0_3_3, all_0_2_2) = 0 % 23.56/6.16 | (130) all_0_4_4 = 0 % 23.56/6.16 | (131) ~ (all_0_0_0 = 0) % 23.56/6.16 | (132) all_0_1_1 = 0 % 23.56/6.16 | (133) less_than(all_0_2_2, all_0_3_3) = all_0_0_0 % 23.56/6.16 | % 23.56/6.16 | From (130) and (6) follows: % 23.56/6.16 | (134) check_cpq(all_0_5_5) = 0 % 23.56/6.16 | % 23.56/6.16 +-Applying beta-rule and splitting (126), into two cases. % 23.56/6.16 |-Branch one: % 23.56/6.16 | (135) ~ (all_57_0_80 = 0) & check_cpq(all_0_5_5) = all_57_0_80 % 23.56/6.16 | % 23.56/6.16 | Applying alpha-rule on (135) yields: % 23.56/6.16 | (136) ~ (all_57_0_80 = 0) % 23.56/6.16 | (137) check_cpq(all_0_5_5) = all_57_0_80 % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (70) with all_0_5_5, 0, all_57_0_80 and discharging atoms check_cpq(all_0_5_5) = all_57_0_80, check_cpq(all_0_5_5) = 0, yields: % 23.56/6.16 | (138) all_57_0_80 = 0 % 23.56/6.16 | % 23.56/6.16 | Equations (138) can reduce 136 to: % 23.56/6.16 | (139) $false % 23.56/6.16 | % 23.56/6.16 |-The branch is then unsatisfiable % 23.56/6.16 |-Branch two: % 23.56/6.16 | (140) ~ (all_57_0_80 = 0) & strictly_less_than(all_0_9_9, all_0_8_8) = all_57_0_80 % 23.56/6.16 | % 23.56/6.16 | Applying alpha-rule on (140) yields: % 23.56/6.16 | (136) ~ (all_57_0_80 = 0) % 23.56/6.16 | (142) strictly_less_than(all_0_9_9, all_0_8_8) = all_57_0_80 % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (43) with all_0_6_6, all_0_7_7, all_0_2_2, all_0_8_8, all_0_3_3, all_0_9_9, all_0_12_12 and discharging atoms pair_in_list(all_0_6_6, all_0_3_3, all_0_2_2) = 0, pair(all_0_9_9, all_0_8_8) = all_0_7_7, insert_slb(all_0_12_12, all_0_7_7) = all_0_6_6, yields: % 23.56/6.16 | (143) all_0_2_2 = all_0_8_8 | pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = 0 % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (88) with all_0_6_6, all_0_7_7, all_0_2_2, all_0_8_8, all_0_3_3, all_0_9_9, all_0_12_12 and discharging atoms pair_in_list(all_0_6_6, all_0_3_3, all_0_2_2) = 0, pair(all_0_9_9, all_0_8_8) = all_0_7_7, insert_slb(all_0_12_12, all_0_7_7) = all_0_6_6, yields: % 23.56/6.16 | (144) all_0_3_3 = all_0_9_9 | pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = 0 % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (50) with all_57_0_80, all_0_8_8, all_0_9_9 and discharging atoms strictly_less_than(all_0_9_9, all_0_8_8) = all_57_0_80, yields: % 23.56/6.16 | (145) all_57_0_80 = 0 | ? [v0] : ((v0 = 0 & less_than(all_0_8_8, all_0_9_9) = 0) | ( ~ (v0 = 0) & less_than(all_0_9_9, all_0_8_8) = v0)) % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (15) with all_0_0_0, all_0_2_2, all_0_3_3 and discharging atoms less_than(all_0_2_2, all_0_3_3) = all_0_0_0, yields: % 23.56/6.16 | (146) all_0_0_0 = 0 | less_than(all_0_3_3, all_0_2_2) = 0 % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (113) with all_0_0_0, all_0_2_2, all_0_3_3 and discharging atoms less_than(all_0_2_2, all_0_3_3) = all_0_0_0, yields: % 23.56/6.16 | (147) all_0_0_0 = 0 | ? [v0] : ((v0 = 0 & strictly_less_than(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_3_3, all_0_2_2) = v0)) % 23.56/6.16 | % 23.56/6.16 | Instantiating formula (31) with all_0_0_0, all_0_2_2, all_0_3_3 and discharging atoms less_than(all_0_2_2, all_0_3_3) = all_0_0_0, yields: % 23.56/6.16 | (148) ? [v0] : ((v0 = 0 & ~ (all_0_0_0 = 0) & less_than(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & strictly_less_than(all_0_3_3, all_0_2_2) = v0)) % 23.56/6.16 | % 23.56/6.16 | Instantiating (148) with all_76_0_85 yields: % 23.56/6.16 | (149) (all_76_0_85 = 0 & ~ (all_0_0_0 = 0) & less_than(all_0_3_3, all_0_2_2) = 0) | ( ~ (all_76_0_85 = 0) & strictly_less_than(all_0_3_3, all_0_2_2) = all_76_0_85) % 23.56/6.16 | % 23.56/6.16 +-Applying beta-rule and splitting (146), into two cases. % 23.56/6.16 |-Branch one: % 23.56/6.16 | (150) less_than(all_0_3_3, all_0_2_2) = 0 % 23.56/6.16 | % 23.56/6.16 +-Applying beta-rule and splitting (147), into two cases. % 23.56/6.16 |-Branch one: % 23.56/6.16 | (151) all_0_0_0 = 0 % 23.56/6.16 | % 23.56/6.16 | Equations (151) can reduce 131 to: % 23.56/6.16 | (139) $false % 23.56/6.16 | % 23.56/6.16 |-The branch is then unsatisfiable % 23.56/6.16 |-Branch two: % 23.56/6.16 | (131) ~ (all_0_0_0 = 0) % 23.56/6.16 | (154) ? [v0] : ((v0 = 0 & strictly_less_than(all_0_3_3, all_0_2_2) = 0) | ( ~ (v0 = 0) & less_than(all_0_3_3, all_0_2_2) = v0)) % 23.56/6.16 | % 23.56/6.16 | Instantiating (154) with all_87_0_86 yields: % 23.56/6.16 | (155) (all_87_0_86 = 0 & strictly_less_than(all_0_3_3, all_0_2_2) = 0) | ( ~ (all_87_0_86 = 0) & less_than(all_0_3_3, all_0_2_2) = all_87_0_86) % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (145), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (138) all_57_0_80 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (138) can reduce 136 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (136) ~ (all_57_0_80 = 0) % 23.56/6.17 | (159) ? [v0] : ((v0 = 0 & less_than(all_0_8_8, all_0_9_9) = 0) | ( ~ (v0 = 0) & less_than(all_0_9_9, all_0_8_8) = v0)) % 23.56/6.17 | % 23.56/6.17 | Instantiating (159) with all_91_0_87 yields: % 23.56/6.17 | (160) (all_91_0_87 = 0 & less_than(all_0_8_8, all_0_9_9) = 0) | ( ~ (all_91_0_87 = 0) & less_than(all_0_9_9, all_0_8_8) = all_91_0_87) % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (155), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (161) all_87_0_86 = 0 & strictly_less_than(all_0_3_3, all_0_2_2) = 0 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (161) yields: % 23.56/6.17 | (162) all_87_0_86 = 0 % 23.56/6.17 | (163) strictly_less_than(all_0_3_3, all_0_2_2) = 0 % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (149), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (164) all_76_0_85 = 0 & ~ (all_0_0_0 = 0) & less_than(all_0_3_3, all_0_2_2) = 0 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (164) yields: % 23.56/6.17 | (165) all_76_0_85 = 0 % 23.56/6.17 | (131) ~ (all_0_0_0 = 0) % 23.56/6.17 | (150) less_than(all_0_3_3, all_0_2_2) = 0 % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (127), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (168) ~ (all_58_2_83 = 0) & less_than(all_0_8_8, all_0_9_9) = all_58_2_83 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (168) yields: % 23.56/6.17 | (169) ~ (all_58_2_83 = 0) % 23.56/6.17 | (170) less_than(all_0_8_8, all_0_9_9) = all_58_2_83 % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (160), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (171) all_91_0_87 = 0 & less_than(all_0_8_8, all_0_9_9) = 0 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (171) yields: % 23.56/6.17 | (172) all_91_0_87 = 0 % 23.56/6.17 | (173) less_than(all_0_8_8, all_0_9_9) = 0 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (73) with all_0_8_8, all_0_9_9, 0, all_58_2_83 and discharging atoms less_than(all_0_8_8, all_0_9_9) = all_58_2_83, less_than(all_0_8_8, all_0_9_9) = 0, yields: % 23.56/6.17 | (174) all_58_2_83 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (174) can reduce 169 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (176) ~ (all_91_0_87 = 0) & less_than(all_0_9_9, all_0_8_8) = all_91_0_87 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (176) yields: % 23.56/6.17 | (177) ~ (all_91_0_87 = 0) % 23.56/6.17 | (178) less_than(all_0_9_9, all_0_8_8) = all_91_0_87 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (15) with all_91_0_87, all_0_9_9, all_0_8_8 and discharging atoms less_than(all_0_9_9, all_0_8_8) = all_91_0_87, yields: % 23.56/6.17 | (179) all_91_0_87 = 0 | less_than(all_0_8_8, all_0_9_9) = 0 % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (179), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (173) less_than(all_0_8_8, all_0_9_9) = 0 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (73) with all_0_8_8, all_0_9_9, 0, all_58_2_83 and discharging atoms less_than(all_0_8_8, all_0_9_9) = all_58_2_83, less_than(all_0_8_8, all_0_9_9) = 0, yields: % 23.56/6.17 | (174) all_58_2_83 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (174) can reduce 169 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (183) ~ (less_than(all_0_8_8, all_0_9_9) = 0) % 23.56/6.17 | (172) all_91_0_87 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (172) can reduce 177 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (186) ((all_58_0_81 = 0 & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = 0) | ( ~ (all_58_2_83 = 0) & check_cpq(all_0_5_5) = all_58_2_83)) & ((all_58_2_83 = 0 & check_cpq(all_0_5_5) = 0) | ( ~ (all_58_0_81 = 0) & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = all_58_0_81)) % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (186) yields: % 23.56/6.17 | (187) (all_58_0_81 = 0 & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = 0) | ( ~ (all_58_2_83 = 0) & check_cpq(all_0_5_5) = all_58_2_83) % 23.56/6.17 | (188) (all_58_2_83 = 0 & check_cpq(all_0_5_5) = 0) | ( ~ (all_58_0_81 = 0) & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = all_58_0_81) % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (143), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (189) pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = 0 % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (187), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (190) all_58_0_81 = 0 & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = 0 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (190) yields: % 23.56/6.17 | (191) all_58_0_81 = 0 % 23.56/6.17 | (192) triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 % 23.56/6.17 | (193) check_cpq(all_58_1_82) = 0 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (75) with all_0_0_0, all_0_2_2, all_0_3_3, all_58_1_82, all_0_10_10, all_0_11_11 and discharging atoms triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82, less_than(all_0_2_2, all_0_3_3) = all_0_0_0, yields: % 23.56/6.17 | (194) all_0_0_0 = 0 | ? [v0] : (( ~ (v0 = 0) & check_cpq(all_58_1_82) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = v0)) % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (74) with all_0_2_2, all_0_3_3, all_58_1_82, all_0_10_10, all_0_11_11 and discharging atoms triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82, pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = 0, yields: % 23.56/6.17 | (195) ? [v0] : ((v0 = 0 & less_than(all_0_2_2, all_0_3_3) = 0) | ( ~ (v0 = 0) & check_cpq(all_58_1_82) = v0)) % 23.56/6.17 | % 23.56/6.17 | Instantiating (195) with all_130_0_94 yields: % 23.56/6.17 | (196) (all_130_0_94 = 0 & less_than(all_0_2_2, all_0_3_3) = 0) | ( ~ (all_130_0_94 = 0) & check_cpq(all_58_1_82) = all_130_0_94) % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (194), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (151) all_0_0_0 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (151) can reduce 131 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (131) ~ (all_0_0_0 = 0) % 23.56/6.17 | (200) ? [v0] : (( ~ (v0 = 0) & check_cpq(all_58_1_82) = v0) | ( ~ (v0 = 0) & pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = v0)) % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (196), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (201) all_130_0_94 = 0 & less_than(all_0_2_2, all_0_3_3) = 0 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (201) yields: % 23.56/6.17 | (202) all_130_0_94 = 0 % 23.56/6.17 | (203) less_than(all_0_2_2, all_0_3_3) = 0 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (73) with all_0_2_2, all_0_3_3, 0, all_0_0_0 and discharging atoms less_than(all_0_2_2, all_0_3_3) = all_0_0_0, less_than(all_0_2_2, all_0_3_3) = 0, yields: % 23.56/6.17 | (151) all_0_0_0 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (151) can reduce 131 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (206) ~ (all_130_0_94 = 0) & check_cpq(all_58_1_82) = all_130_0_94 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (206) yields: % 23.56/6.17 | (207) ~ (all_130_0_94 = 0) % 23.56/6.17 | (208) check_cpq(all_58_1_82) = all_130_0_94 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (70) with all_58_1_82, all_130_0_94, 0 and discharging atoms check_cpq(all_58_1_82) = all_130_0_94, check_cpq(all_58_1_82) = 0, yields: % 23.56/6.17 | (202) all_130_0_94 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (202) can reduce 207 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (211) ~ (all_58_2_83 = 0) & check_cpq(all_0_5_5) = all_58_2_83 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (211) yields: % 23.56/6.17 | (169) ~ (all_58_2_83 = 0) % 23.56/6.17 | (213) check_cpq(all_0_5_5) = all_58_2_83 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (70) with all_0_5_5, all_58_2_83, 0 and discharging atoms check_cpq(all_0_5_5) = all_58_2_83, check_cpq(all_0_5_5) = 0, yields: % 23.56/6.17 | (174) all_58_2_83 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (174) can reduce 169 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (216) ~ (pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = 0) % 23.56/6.17 | (217) all_0_2_2 = all_0_8_8 % 23.56/6.17 | % 23.56/6.17 | From (217) and (163) follows: % 23.56/6.17 | (218) strictly_less_than(all_0_3_3, all_0_8_8) = 0 % 23.56/6.17 | % 23.56/6.17 | From (217) and (216) follows: % 23.56/6.17 | (219) ~ (pair_in_list(all_0_12_12, all_0_3_3, all_0_8_8) = 0) % 23.56/6.17 | % 23.56/6.17 +-Applying beta-rule and splitting (144), into two cases. % 23.56/6.17 |-Branch one: % 23.56/6.17 | (189) pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = 0 % 23.56/6.17 | % 23.56/6.17 | From (217) and (189) follows: % 23.56/6.17 | (221) pair_in_list(all_0_12_12, all_0_3_3, all_0_8_8) = 0 % 23.56/6.17 | % 23.56/6.17 | Using (221) and (219) yields: % 23.56/6.17 | (222) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (216) ~ (pair_in_list(all_0_12_12, all_0_3_3, all_0_2_2) = 0) % 23.56/6.17 | (224) all_0_3_3 = all_0_9_9 % 23.56/6.17 | % 23.56/6.17 | From (224) and (218) follows: % 23.56/6.17 | (225) strictly_less_than(all_0_9_9, all_0_8_8) = 0 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (9) with all_0_9_9, all_0_8_8, 0, all_57_0_80 and discharging atoms strictly_less_than(all_0_9_9, all_0_8_8) = all_57_0_80, strictly_less_than(all_0_9_9, all_0_8_8) = 0, yields: % 23.56/6.17 | (138) all_57_0_80 = 0 % 23.56/6.17 | % 23.56/6.17 | Equations (138) can reduce 136 to: % 23.56/6.17 | (139) $false % 23.56/6.17 | % 23.56/6.17 |-The branch is then unsatisfiable % 23.56/6.17 |-Branch two: % 23.56/6.17 | (228) ~ (all_76_0_85 = 0) & strictly_less_than(all_0_3_3, all_0_2_2) = all_76_0_85 % 23.56/6.17 | % 23.56/6.17 | Applying alpha-rule on (228) yields: % 23.56/6.17 | (229) ~ (all_76_0_85 = 0) % 23.56/6.17 | (230) strictly_less_than(all_0_3_3, all_0_2_2) = all_76_0_85 % 23.56/6.17 | % 23.56/6.17 | Instantiating formula (9) with all_0_3_3, all_0_2_2, 0, all_76_0_85 and discharging atoms strictly_less_than(all_0_3_3, all_0_2_2) = all_76_0_85, strictly_less_than(all_0_3_3, all_0_2_2) = 0, yields: % 23.56/6.17 | (165) all_76_0_85 = 0 % 23.56/6.17 | % 23.56/6.18 | Equations (165) can reduce 229 to: % 23.56/6.18 | (139) $false % 23.56/6.18 | % 23.56/6.18 |-The branch is then unsatisfiable % 23.56/6.18 |-Branch two: % 23.56/6.18 | (233) ~ (all_87_0_86 = 0) & less_than(all_0_3_3, all_0_2_2) = all_87_0_86 % 23.56/6.18 | % 23.56/6.18 | Applying alpha-rule on (233) yields: % 23.56/6.18 | (234) ~ (all_87_0_86 = 0) % 23.56/6.18 | (235) less_than(all_0_3_3, all_0_2_2) = all_87_0_86 % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (73) with all_0_3_3, all_0_2_2, 0, all_87_0_86 and discharging atoms less_than(all_0_3_3, all_0_2_2) = all_87_0_86, less_than(all_0_3_3, all_0_2_2) = 0, yields: % 23.56/6.18 | (162) all_87_0_86 = 0 % 23.56/6.18 | % 23.56/6.18 | Equations (162) can reduce 234 to: % 23.56/6.18 | (139) $false % 23.56/6.18 | % 23.56/6.18 |-The branch is then unsatisfiable % 23.56/6.18 |-Branch two: % 23.56/6.18 | (238) ~ (less_than(all_0_3_3, all_0_2_2) = 0) % 23.56/6.18 | (151) all_0_0_0 = 0 % 23.56/6.18 | % 23.56/6.18 | Equations (151) can reduce 131 to: % 23.56/6.18 | (139) $false % 23.56/6.18 | % 23.56/6.18 |-The branch is then unsatisfiable % 23.56/6.18 |-Branch two: % 23.56/6.18 | (241) ~ (all_0_4_4 = 0) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & pair_in_list(all_0_6_6, v0, v1) = v3)) & ! [v0] : ! [v1] : ( ~ (pair_in_list(all_0_6_6, v0, v1) = 0) | less_than(v1, v0) = 0) % 23.56/6.18 | % 23.56/6.18 | Applying alpha-rule on (241) yields: % 23.56/6.18 | (242) ~ (all_0_4_4 = 0) % 23.56/6.18 | (243) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (less_than(v1, v0) = v2) | ? [v3] : ( ~ (v3 = 0) & pair_in_list(all_0_6_6, v0, v1) = v3)) % 23.56/6.18 | (244) ! [v0] : ! [v1] : ( ~ (pair_in_list(all_0_6_6, v0, v1) = 0) | less_than(v1, v0) = 0) % 23.56/6.18 | % 23.56/6.18 +-Applying beta-rule and splitting (127), into two cases. % 23.56/6.18 |-Branch one: % 23.56/6.18 | (168) ~ (all_58_2_83 = 0) & less_than(all_0_8_8, all_0_9_9) = all_58_2_83 % 23.56/6.18 | % 23.56/6.18 | Applying alpha-rule on (168) yields: % 23.56/6.18 | (169) ~ (all_58_2_83 = 0) % 23.56/6.18 | (170) less_than(all_0_8_8, all_0_9_9) = all_58_2_83 % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (243) with all_58_2_83, all_0_8_8, all_0_9_9 and discharging atoms less_than(all_0_8_8, all_0_9_9) = all_58_2_83, yields: % 23.56/6.18 | (248) all_58_2_83 = 0 | ? [v0] : ( ~ (v0 = 0) & pair_in_list(all_0_6_6, all_0_9_9, all_0_8_8) = v0) % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (113) with all_58_2_83, all_0_8_8, all_0_9_9 and discharging atoms less_than(all_0_8_8, all_0_9_9) = all_58_2_83, yields: % 23.56/6.18 | (249) all_58_2_83 = 0 | ? [v0] : ((v0 = 0 & strictly_less_than(all_0_9_9, all_0_8_8) = 0) | ( ~ (v0 = 0) & less_than(all_0_9_9, all_0_8_8) = v0)) % 23.56/6.18 | % 23.56/6.18 +-Applying beta-rule and splitting (249), into two cases. % 23.56/6.18 |-Branch one: % 23.56/6.18 | (174) all_58_2_83 = 0 % 23.56/6.18 | % 23.56/6.18 | Equations (174) can reduce 169 to: % 23.56/6.18 | (139) $false % 23.56/6.18 | % 23.56/6.18 |-The branch is then unsatisfiable % 23.56/6.18 |-Branch two: % 23.56/6.18 | (169) ~ (all_58_2_83 = 0) % 23.56/6.18 | (253) ? [v0] : ((v0 = 0 & strictly_less_than(all_0_9_9, all_0_8_8) = 0) | ( ~ (v0 = 0) & less_than(all_0_9_9, all_0_8_8) = v0)) % 23.56/6.18 | % 23.56/6.18 +-Applying beta-rule and splitting (248), into two cases. % 23.56/6.18 |-Branch one: % 23.56/6.18 | (174) all_58_2_83 = 0 % 23.56/6.18 | % 23.56/6.18 | Equations (174) can reduce 169 to: % 23.56/6.18 | (139) $false % 23.56/6.18 | % 23.56/6.18 |-The branch is then unsatisfiable % 23.56/6.18 |-Branch two: % 23.56/6.18 | (169) ~ (all_58_2_83 = 0) % 23.56/6.18 | (257) ? [v0] : ( ~ (v0 = 0) & pair_in_list(all_0_6_6, all_0_9_9, all_0_8_8) = v0) % 23.56/6.18 | % 23.56/6.18 | Instantiating (257) with all_110_0_106 yields: % 23.56/6.18 | (258) ~ (all_110_0_106 = 0) & pair_in_list(all_0_6_6, all_0_9_9, all_0_8_8) = all_110_0_106 % 23.56/6.18 | % 23.56/6.18 | Applying alpha-rule on (258) yields: % 23.56/6.18 | (259) ~ (all_110_0_106 = 0) % 23.56/6.18 | (260) pair_in_list(all_0_6_6, all_0_9_9, all_0_8_8) = all_110_0_106 % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (99) with all_110_0_106, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_12_12 and discharging atoms pair_in_list(all_0_6_6, all_0_9_9, all_0_8_8) = all_110_0_106, pair(all_0_9_9, all_0_8_8) = all_0_7_7, insert_slb(all_0_12_12, all_0_7_7) = all_0_6_6, yields: % 23.56/6.18 | (261) all_110_0_106 = 0 % 23.56/6.18 | % 23.56/6.18 | Equations (261) can reduce 259 to: % 23.56/6.18 | (139) $false % 23.56/6.18 | % 23.56/6.18 |-The branch is then unsatisfiable % 23.56/6.18 |-Branch two: % 23.56/6.18 | (186) ((all_58_0_81 = 0 & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = 0) | ( ~ (all_58_2_83 = 0) & check_cpq(all_0_5_5) = all_58_2_83)) & ((all_58_2_83 = 0 & check_cpq(all_0_5_5) = 0) | ( ~ (all_58_0_81 = 0) & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = all_58_0_81)) % 23.56/6.18 | % 23.56/6.18 | Applying alpha-rule on (186) yields: % 23.56/6.18 | (187) (all_58_0_81 = 0 & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = 0) | ( ~ (all_58_2_83 = 0) & check_cpq(all_0_5_5) = all_58_2_83) % 23.56/6.18 | (188) (all_58_2_83 = 0 & check_cpq(all_0_5_5) = 0) | ( ~ (all_58_0_81 = 0) & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = all_58_0_81) % 23.56/6.18 | % 23.56/6.18 +-Applying beta-rule and splitting (188), into two cases. % 23.56/6.18 |-Branch one: % 23.56/6.18 | (266) all_58_2_83 = 0 & check_cpq(all_0_5_5) = 0 % 23.56/6.18 | % 23.56/6.18 | Applying alpha-rule on (266) yields: % 23.56/6.18 | (174) all_58_2_83 = 0 % 23.56/6.18 | (134) check_cpq(all_0_5_5) = 0 % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (70) with all_0_5_5, 0, all_0_4_4 and discharging atoms check_cpq(all_0_5_5) = all_0_4_4, check_cpq(all_0_5_5) = 0, yields: % 23.56/6.18 | (130) all_0_4_4 = 0 % 23.56/6.18 | % 23.56/6.18 | Equations (130) can reduce 242 to: % 23.56/6.18 | (139) $false % 23.56/6.18 | % 23.56/6.18 |-The branch is then unsatisfiable % 23.56/6.18 |-Branch two: % 23.56/6.18 | (271) ~ (all_58_0_81 = 0) & triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 & check_cpq(all_58_1_82) = all_58_0_81 % 23.56/6.18 | % 23.56/6.18 | Applying alpha-rule on (271) yields: % 23.56/6.18 | (272) ~ (all_58_0_81 = 0) % 23.56/6.18 | (192) triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82 % 23.56/6.18 | (274) check_cpq(all_58_1_82) = all_58_0_81 % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (105) with all_58_1_82, all_0_10_10, all_0_11_11 and discharging atoms triple(all_0_11_11, all_0_12_12, all_0_10_10) = all_58_1_82, yields: % 23.56/6.18 | (275) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ((v2 = 0 & ~ (v3 = 0) & pair_in_list(all_0_12_12, v0, v1) = 0 & less_than(v1, v0) = v3) | (v0 = 0 & check_cpq(all_58_1_82) = 0)) % 23.56/6.18 | % 23.56/6.18 | Instantiating (275) with all_99_0_117, all_99_1_118, all_99_2_119, all_99_3_120 yields: % 23.56/6.18 | (276) (all_99_1_118 = 0 & ~ (all_99_0_117 = 0) & pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = 0 & less_than(all_99_2_119, all_99_3_120) = all_99_0_117) | (all_99_3_120 = 0 & check_cpq(all_58_1_82) = 0) % 23.56/6.18 | % 23.56/6.18 +-Applying beta-rule and splitting (276), into two cases. % 23.56/6.18 |-Branch one: % 23.56/6.18 | (277) all_99_1_118 = 0 & ~ (all_99_0_117 = 0) & pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = 0 & less_than(all_99_2_119, all_99_3_120) = all_99_0_117 % 23.56/6.18 | % 23.56/6.18 | Applying alpha-rule on (277) yields: % 23.56/6.18 | (278) all_99_1_118 = 0 % 23.56/6.18 | (279) ~ (all_99_0_117 = 0) % 23.56/6.18 | (280) pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = 0 % 23.56/6.18 | (281) less_than(all_99_2_119, all_99_3_120) = all_99_0_117 % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (15) with all_99_0_117, all_99_2_119, all_99_3_120 and discharging atoms less_than(all_99_2_119, all_99_3_120) = all_99_0_117, yields: % 23.56/6.18 | (282) all_99_0_117 = 0 | less_than(all_99_3_120, all_99_2_119) = 0 % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (243) with all_99_0_117, all_99_2_119, all_99_3_120 and discharging atoms less_than(all_99_2_119, all_99_3_120) = all_99_0_117, yields: % 23.56/6.18 | (283) all_99_0_117 = 0 | ? [v0] : ( ~ (v0 = 0) & pair_in_list(all_0_6_6, all_99_3_120, all_99_2_119) = v0) % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (113) with all_99_0_117, all_99_2_119, all_99_3_120 and discharging atoms less_than(all_99_2_119, all_99_3_120) = all_99_0_117, yields: % 23.56/6.18 | (284) all_99_0_117 = 0 | ? [v0] : ((v0 = 0 & strictly_less_than(all_99_3_120, all_99_2_119) = 0) | ( ~ (v0 = 0) & less_than(all_99_3_120, all_99_2_119) = v0)) % 23.56/6.18 | % 23.56/6.18 | Instantiating formula (31) with all_99_0_117, all_99_2_119, all_99_3_120 and discharging atoms less_than(all_99_2_119, all_99_3_120) = all_99_0_117, yields: % 23.56/6.18 | (285) ? [v0] : ((v0 = 0 & ~ (all_99_0_117 = 0) & less_than(all_99_3_120, all_99_2_119) = 0) | ( ~ (v0 = 0) & strictly_less_than(all_99_3_120, all_99_2_119) = v0)) % 23.56/6.18 | % 23.56/6.18 | Instantiating (285) with all_113_0_123 yields: % 23.56/6.18 | (286) (all_113_0_123 = 0 & ~ (all_99_0_117 = 0) & less_than(all_99_3_120, all_99_2_119) = 0) | ( ~ (all_113_0_123 = 0) & strictly_less_than(all_99_3_120, all_99_2_119) = all_113_0_123) % 23.56/6.18 | % 23.56/6.18 +-Applying beta-rule and splitting (284), into two cases. % 23.56/6.18 |-Branch one: % 23.56/6.18 | (287) all_99_0_117 = 0 % 23.56/6.18 | % 23.56/6.18 | Equations (287) can reduce 279 to: % 23.56/6.18 | (139) $false % 23.56/6.18 | % 23.56/6.18 |-The branch is then unsatisfiable % 23.56/6.18 |-Branch two: % 23.56/6.18 | (279) ~ (all_99_0_117 = 0) % 23.56/6.18 | (290) ? [v0] : ((v0 = 0 & strictly_less_than(all_99_3_120, all_99_2_119) = 0) | ( ~ (v0 = 0) & less_than(all_99_3_120, all_99_2_119) = v0)) % 23.56/6.18 | % 23.56/6.18 | Instantiating (290) with all_123_0_124 yields: % 23.56/6.18 | (291) (all_123_0_124 = 0 & strictly_less_than(all_99_3_120, all_99_2_119) = 0) | ( ~ (all_123_0_124 = 0) & less_than(all_99_3_120, all_99_2_119) = all_123_0_124) % 23.56/6.18 | % 23.56/6.18 +-Applying beta-rule and splitting (282), into two cases. % 23.56/6.18 |-Branch one: % 23.56/6.18 | (292) less_than(all_99_3_120, all_99_2_119) = 0 % 23.56/6.18 | % 23.56/6.19 +-Applying beta-rule and splitting (291), into two cases. % 23.56/6.19 |-Branch one: % 23.56/6.19 | (293) all_123_0_124 = 0 & strictly_less_than(all_99_3_120, all_99_2_119) = 0 % 23.56/6.19 | % 23.56/6.19 | Applying alpha-rule on (293) yields: % 23.56/6.19 | (294) all_123_0_124 = 0 % 23.56/6.19 | (295) strictly_less_than(all_99_3_120, all_99_2_119) = 0 % 23.56/6.19 | % 23.56/6.19 +-Applying beta-rule and splitting (286), into two cases. % 23.56/6.19 |-Branch one: % 23.56/6.19 | (296) all_113_0_123 = 0 & ~ (all_99_0_117 = 0) & less_than(all_99_3_120, all_99_2_119) = 0 % 23.56/6.19 | % 23.56/6.19 | Applying alpha-rule on (296) yields: % 23.56/6.19 | (297) all_113_0_123 = 0 % 23.56/6.19 | (279) ~ (all_99_0_117 = 0) % 23.56/6.19 | (292) less_than(all_99_3_120, all_99_2_119) = 0 % 23.56/6.19 | % 23.56/6.19 +-Applying beta-rule and splitting (283), into two cases. % 23.56/6.19 |-Branch one: % 23.56/6.19 | (287) all_99_0_117 = 0 % 23.56/6.19 | % 23.56/6.19 | Equations (287) can reduce 279 to: % 23.56/6.19 | (139) $false % 23.56/6.19 | % 23.56/6.19 |-The branch is then unsatisfiable % 23.56/6.19 |-Branch two: % 23.56/6.19 | (279) ~ (all_99_0_117 = 0) % 23.56/6.19 | (303) ? [v0] : ( ~ (v0 = 0) & pair_in_list(all_0_6_6, all_99_3_120, all_99_2_119) = v0) % 23.56/6.19 | % 23.56/6.19 | Instantiating (303) with all_140_0_125 yields: % 23.56/6.19 | (304) ~ (all_140_0_125 = 0) & pair_in_list(all_0_6_6, all_99_3_120, all_99_2_119) = all_140_0_125 % 23.56/6.19 | % 23.56/6.19 | Applying alpha-rule on (304) yields: % 23.56/6.19 | (305) ~ (all_140_0_125 = 0) % 23.56/6.19 | (306) pair_in_list(all_0_6_6, all_99_3_120, all_99_2_119) = all_140_0_125 % 23.56/6.19 | % 23.56/6.19 | Instantiating formula (21) with all_140_0_125, all_0_6_6, all_0_7_7, all_99_2_119, all_0_8_8, all_99_3_120, all_0_9_9, all_0_12_12 and discharging atoms pair_in_list(all_0_6_6, all_99_3_120, all_99_2_119) = all_140_0_125, pair(all_0_9_9, all_0_8_8) = all_0_7_7, insert_slb(all_0_12_12, all_0_7_7) = all_0_6_6, yields: % 23.56/6.19 | (307) all_140_0_125 = 0 | ? [v0] : ( ~ (v0 = 0) & pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = v0) % 23.97/6.19 | % 23.97/6.19 +-Applying beta-rule and splitting (307), into two cases. % 23.97/6.19 |-Branch one: % 23.97/6.19 | (308) all_140_0_125 = 0 % 23.97/6.19 | % 23.97/6.19 | Equations (308) can reduce 305 to: % 23.97/6.19 | (139) $false % 23.97/6.19 | % 23.97/6.19 |-The branch is then unsatisfiable % 23.97/6.19 |-Branch two: % 23.97/6.19 | (305) ~ (all_140_0_125 = 0) % 23.97/6.19 | (311) ? [v0] : ( ~ (v0 = 0) & pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = v0) % 23.97/6.19 | % 23.97/6.19 | Instantiating (311) with all_153_0_126 yields: % 23.97/6.19 | (312) ~ (all_153_0_126 = 0) & pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = all_153_0_126 % 23.97/6.19 | % 23.97/6.19 | Applying alpha-rule on (312) yields: % 23.97/6.19 | (313) ~ (all_153_0_126 = 0) % 23.97/6.19 | (314) pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = all_153_0_126 % 23.97/6.19 | % 23.97/6.19 | Instantiating formula (42) with all_0_12_12, all_99_3_120, all_99_2_119, all_153_0_126, 0 and discharging atoms pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = all_153_0_126, pair_in_list(all_0_12_12, all_99_3_120, all_99_2_119) = 0, yields: % 23.97/6.19 | (315) all_153_0_126 = 0 % 23.97/6.19 | % 23.97/6.19 | Equations (315) can reduce 313 to: % 23.97/6.19 | (139) $false % 23.97/6.19 | % 23.97/6.19 |-The branch is then unsatisfiable % 23.97/6.19 |-Branch two: % 23.97/6.19 | (317) ~ (all_113_0_123 = 0) & strictly_less_than(all_99_3_120, all_99_2_119) = all_113_0_123 % 23.97/6.19 | % 23.97/6.19 | Applying alpha-rule on (317) yields: % 23.97/6.19 | (318) ~ (all_113_0_123 = 0) % 23.97/6.19 | (319) strictly_less_than(all_99_3_120, all_99_2_119) = all_113_0_123 % 23.97/6.19 | % 23.97/6.19 | Instantiating formula (9) with all_99_3_120, all_99_2_119, 0, all_113_0_123 and discharging atoms strictly_less_than(all_99_3_120, all_99_2_119) = all_113_0_123, strictly_less_than(all_99_3_120, all_99_2_119) = 0, yields: % 23.97/6.19 | (297) all_113_0_123 = 0 % 23.97/6.19 | % 23.97/6.19 | Equations (297) can reduce 318 to: % 23.97/6.19 | (139) $false % 23.97/6.19 | % 23.97/6.19 |-The branch is then unsatisfiable % 23.97/6.19 |-Branch two: % 23.97/6.19 | (322) ~ (all_123_0_124 = 0) & less_than(all_99_3_120, all_99_2_119) = all_123_0_124 % 23.97/6.19 | % 23.97/6.19 | Applying alpha-rule on (322) yields: % 23.97/6.19 | (323) ~ (all_123_0_124 = 0) % 23.97/6.19 | (324) less_than(all_99_3_120, all_99_2_119) = all_123_0_124 % 23.97/6.19 | % 23.97/6.19 | Instantiating formula (73) with all_99_3_120, all_99_2_119, 0, all_123_0_124 and discharging atoms less_than(all_99_3_120, all_99_2_119) = all_123_0_124, less_than(all_99_3_120, all_99_2_119) = 0, yields: % 23.97/6.19 | (294) all_123_0_124 = 0 % 23.97/6.19 | % 23.97/6.19 | Equations (294) can reduce 323 to: % 23.97/6.19 | (139) $false % 23.97/6.19 | % 23.97/6.19 |-The branch is then unsatisfiable % 23.97/6.19 |-Branch two: % 23.97/6.19 | (327) ~ (less_than(all_99_3_120, all_99_2_119) = 0) % 23.97/6.19 | (287) all_99_0_117 = 0 % 23.97/6.19 | % 23.97/6.19 | Equations (287) can reduce 279 to: % 23.97/6.19 | (139) $false % 23.97/6.19 | % 23.97/6.19 |-The branch is then unsatisfiable % 23.97/6.19 |-Branch two: % 23.97/6.19 | (330) all_99_3_120 = 0 & check_cpq(all_58_1_82) = 0 % 23.97/6.19 | % 23.97/6.19 | Applying alpha-rule on (330) yields: % 23.97/6.19 | (331) all_99_3_120 = 0 % 23.97/6.19 | (193) check_cpq(all_58_1_82) = 0 % 23.97/6.19 | % 23.97/6.19 | Instantiating formula (70) with all_58_1_82, 0, all_58_0_81 and discharging atoms check_cpq(all_58_1_82) = all_58_0_81, check_cpq(all_58_1_82) = 0, yields: % 23.97/6.19 | (191) all_58_0_81 = 0 % 23.97/6.19 | % 23.97/6.19 | Equations (191) can reduce 272 to: % 23.97/6.19 | (139) $false % 23.97/6.19 | % 23.97/6.19 |-The branch is then unsatisfiable % 23.97/6.19 % SZS output end Proof for theBenchmark % 23.97/6.19 % 23.97/6.19 5594ms %------------------------------------------------------------------------------