%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG107+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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 : Thu Jul 14 18:02:28 EDT 2022 % Result : Theorem 0.64s 0.81s % Output : Refutation 0.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : ALG107+1 : TPTP v8.1.0. Released v2.7.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 9 03:08:06 EDT 2022 % 0.12/0.33 % CPUTime : % 0.64/0.81 % 0.64/0.81 SPASS V 3.9 % 0.64/0.81 SPASS beiseite: Proof found. % 0.64/0.81 % SZS status Theorem % 0.64/0.81 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.64/0.81 SPASS derived 2251 clauses, backtracked 2260 clauses, performed 26 splits and kept 3302 clauses. % 0.64/0.81 SPASS allocated 87532 KBytes. % 0.64/0.81 SPASS spent 0:00:00.47 on the problem. % 0.64/0.81 0:00:00.04 for the input. % 0.64/0.81 0:00:00.07 for the FLOTTER CNF translation. % 0.64/0.81 0:00:00.00 for inferences. % 0.64/0.81 0:00:00.01 for the backtracking. % 0.64/0.81 0:00:00.32 for the reduction. % 0.64/0.81 % 0.64/0.81 % 0.64/0.81 Here is a proof with depth 3, length 956 : % 0.64/0.81 % SZS output start Refutation % 0.64/0.81 1[0:Inp] || equal(e11,e10)** -> . % 0.64/0.81 2[0:Inp] || equal(e12,e10)** -> . % 0.64/0.81 3[0:Inp] || equal(e13,e10)** -> . % 0.64/0.81 4[0:Inp] || equal(e12,e11)** -> . % 0.64/0.81 5[0:Inp] || equal(e13,e11)** -> . % 0.64/0.81 6[0:Inp] || equal(e13,e12)** -> . % 0.64/0.81 7[0:Inp] || equal(e21,e20)** -> . % 0.64/0.81 8[0:Inp] || equal(e22,e20)** -> . % 0.64/0.81 9[0:Inp] || equal(e23,e20)** -> . % 0.64/0.81 10[0:Inp] || equal(e22,e21)** -> . % 0.64/0.81 11[0:Inp] || equal(e23,e21)** -> . % 0.64/0.81 12[0:Inp] || equal(e23,e22)** -> . % 0.64/0.81 31[0:Inp] || -> equal(h3(e12),e22)**. % 0.64/0.81 33[0:Inp] || -> equal(op1(e12,e12),e10)**. % 0.64/0.81 34[0:Inp] || -> equal(op2(e22,e22),e20)**. % 0.64/0.81 59[0:Inp] || equal(h3(e10),e20)** -> SkC12. % 0.64/0.81 64[0:Inp] || equal(h3(e11),e21)** -> SkC13. % 0.64/0.81 69[0:Inp] || equal(h3(e12),e22)** -> SkC14. % 0.64/0.81 83[0:Inp] || -> equal(op2(e20,e20),h1(e10))**. % 0.64/0.81 84[0:Inp] || -> equal(op2(e21,e21),h2(e10))**. % 0.64/0.81 85[0:Inp] || -> equal(op2(e22,e22),h3(e10))**. % 0.64/0.81 86[0:Inp] || -> equal(op2(e23,e23),h4(e10))**. % 0.64/0.81 87[0:Inp] || -> equal(op1(e12,op1(e12,e12)),e11)**. % 0.64/0.81 88[0:Inp] || -> equal(op2(e22,op2(e22,e22)),e21)**. % 0.64/0.81 89[0:Inp] || equal(op1(e11,e10),op1(e10,e10))** -> . % 0.64/0.81 90[0:Inp] || equal(op1(e12,e10),op1(e10,e10))** -> . % 0.64/0.81 91[0:Inp] || equal(op1(e13,e10),op1(e10,e10))** -> . % 0.64/0.81 93[0:Inp] || equal(op1(e13,e10),op1(e11,e10))** -> . % 0.64/0.81 94[0:Inp] || equal(op1(e13,e10),op1(e12,e10))** -> . % 0.64/0.81 95[0:Inp] || equal(op1(e11,e11),op1(e10,e11))** -> . % 0.64/0.81 96[0:Inp] || equal(op1(e12,e11),op1(e10,e11))** -> . % 0.64/0.81 97[0:Inp] || equal(op1(e13,e11),op1(e10,e11))** -> . % 0.64/0.81 100[0:Inp] || equal(op1(e13,e11),op1(e12,e11))** -> . % 0.64/0.81 101[0:Inp] || equal(op1(e11,e12),op1(e10,e12))** -> . % 0.64/0.81 102[0:Inp] || equal(op1(e12,e12),op1(e10,e12))** -> . % 0.64/0.81 103[0:Inp] || equal(op1(e13,e12),op1(e10,e12))** -> . % 0.64/0.81 104[0:Inp] || equal(op1(e12,e12),op1(e11,e12))** -> . % 0.64/0.81 105[0:Inp] || equal(op1(e13,e12),op1(e11,e12))** -> . % 0.64/0.81 107[0:Inp] || equal(op1(e11,e13),op1(e10,e13))** -> . % 0.64/0.81 108[0:Inp] || equal(op1(e12,e13),op1(e10,e13))** -> . % 0.64/0.81 109[0:Inp] || equal(op1(e13,e13),op1(e10,e13))** -> . % 0.64/0.81 112[0:Inp] || equal(op1(e13,e13),op1(e12,e13))** -> . % 0.64/0.81 113[0:Inp] || equal(op1(e10,e11),op1(e10,e10))** -> . % 0.64/0.81 114[0:Inp] || equal(op1(e10,e12),op1(e10,e10))** -> . % 0.64/0.81 115[0:Inp] || equal(op1(e10,e13),op1(e10,e10))** -> . % 0.64/0.81 117[0:Inp] || equal(op1(e10,e13),op1(e10,e11))** -> . % 0.64/0.81 118[0:Inp] || equal(op1(e10,e13),op1(e10,e12))** -> . % 0.64/0.81 119[0:Inp] || equal(op1(e11,e11),op1(e11,e10))** -> . % 0.64/0.81 120[0:Inp] || equal(op1(e11,e12),op1(e11,e10))** -> . % 0.64/0.81 122[0:Inp] || equal(op1(e11,e12),op1(e11,e11))** -> . % 0.64/0.81 124[0:Inp] || equal(op1(e11,e13),op1(e11,e12))** -> . % 0.64/0.81 125[0:Inp] || equal(op1(e12,e11),op1(e12,e10))** -> . % 0.64/0.81 127[0:Inp] || equal(op1(e12,e13),op1(e12,e10))** -> . % 0.64/0.81 128[0:Inp] || equal(op1(e12,e12),op1(e12,e11))** -> . % 0.64/0.81 130[0:Inp] || equal(op1(e12,e13),op1(e12,e12))** -> . % 0.64/0.81 131[0:Inp] || equal(op1(e13,e11),op1(e13,e10))** -> . % 0.64/0.81 134[0:Inp] || equal(op1(e13,e12),op1(e13,e11))** -> . % 0.64/0.81 135[0:Inp] || equal(op1(e13,e13),op1(e13,e11))** -> . % 0.64/0.81 137[0:Inp] || equal(op2(e21,e20),op2(e20,e20))** -> . % 0.64/0.81 138[0:Inp] || equal(op2(e22,e20),op2(e20,e20))** -> . % 0.64/0.81 141[0:Inp] || equal(op2(e23,e20),op2(e21,e20))** -> . % 0.64/0.81 142[0:Inp] || equal(op2(e23,e20),op2(e22,e20))** -> . % 0.64/0.81 143[0:Inp] || equal(op2(e21,e21),op2(e20,e21))** -> . % 0.64/0.81 144[0:Inp] || equal(op2(e22,e21),op2(e20,e21))** -> . % 0.64/0.81 145[0:Inp] || equal(op2(e23,e21),op2(e20,e21))** -> . % 0.64/0.81 146[0:Inp] || equal(op2(e22,e21),op2(e21,e21))** -> . % 0.64/0.81 147[0:Inp] || equal(op2(e23,e21),op2(e21,e21))** -> . % 0.64/0.81 148[0:Inp] || equal(op2(e23,e21),op2(e22,e21))** -> . % 0.64/0.81 149[0:Inp] || equal(op2(e21,e22),op2(e20,e22))** -> . % 0.64/0.81 150[0:Inp] || equal(op2(e22,e22),op2(e20,e22))** -> . % 0.64/0.81 151[0:Inp] || equal(op2(e23,e22),op2(e20,e22))** -> . % 0.64/0.81 152[0:Inp] || equal(op2(e22,e22),op2(e21,e22))** -> . % 0.64/0.81 153[0:Inp] || equal(op2(e23,e22),op2(e21,e22))** -> . % 0.64/0.81 154[0:Inp] || equal(op2(e23,e22),op2(e22,e22))** -> . % 0.64/0.81 155[0:Inp] || equal(op2(e21,e23),op2(e20,e23))** -> . % 0.64/0.81 156[0:Inp] || equal(op2(e22,e23),op2(e20,e23))** -> . % 0.64/0.81 157[0:Inp] || equal(op2(e23,e23),op2(e20,e23))** -> . % 0.64/0.81 158[0:Inp] || equal(op2(e22,e23),op2(e21,e23))** -> . % 0.64/0.81 159[0:Inp] || equal(op2(e23,e23),op2(e21,e23))** -> . % 0.64/0.81 160[0:Inp] || equal(op2(e23,e23),op2(e22,e23))** -> . % 0.64/0.81 164[0:Inp] || equal(op2(e20,e22),op2(e20,e21))** -> . % 0.64/0.81 165[0:Inp] || equal(op2(e20,e23),op2(e20,e21))** -> . % 0.64/0.81 166[0:Inp] || equal(op2(e20,e23),op2(e20,e22))** -> . % 0.64/0.81 167[0:Inp] || equal(op2(e21,e21),op2(e21,e20))** -> . % 0.64/0.81 168[0:Inp] || equal(op2(e21,e22),op2(e21,e20))** -> . % 0.64/0.81 169[0:Inp] || equal(op2(e21,e23),op2(e21,e20))** -> . % 0.64/0.81 170[0:Inp] || equal(op2(e21,e22),op2(e21,e21))** -> . % 0.64/0.81 171[0:Inp] || equal(op2(e21,e23),op2(e21,e21))** -> . % 0.64/0.81 172[0:Inp] || equal(op2(e21,e23),op2(e21,e22))** -> . % 0.64/0.81 173[0:Inp] || equal(op2(e22,e21),op2(e22,e20))** -> . % 0.64/0.81 175[0:Inp] || equal(op2(e22,e23),op2(e22,e20))** -> . % 0.64/0.81 176[0:Inp] || equal(op2(e22,e22),op2(e22,e21))** -> . % 0.64/0.81 177[0:Inp] || equal(op2(e22,e23),op2(e22,e21))** -> . % 0.64/0.81 178[0:Inp] || equal(op2(e22,e23),op2(e22,e22))** -> . % 0.64/0.81 179[0:Inp] || equal(op2(e23,e21),op2(e23,e20))** -> . % 0.64/0.81 180[0:Inp] || equal(op2(e23,e22),op2(e23,e20))** -> . % 0.64/0.81 181[0:Inp] || equal(op2(e23,e23),op2(e23,e20))** -> . % 0.64/0.81 182[0:Inp] || equal(op2(e23,e22),op2(e23,e21))** -> . % 0.64/0.81 183[0:Inp] || equal(op2(e23,e23),op2(e23,e21))** -> . % 0.64/0.81 184[0:Inp] || equal(op2(e23,e23),op2(e23,e22))** -> . % 0.64/0.81 185[0:Inp] || -> equal(op2(e20,op2(e20,e20)),h1(e11))**. % 0.64/0.81 186[0:Inp] || -> equal(op2(e21,op2(e21,e21)),h2(e11))**. % 0.64/0.81 187[0:Inp] || -> equal(op2(e22,op2(e22,e22)),h3(e11))**. % 0.64/0.81 188[0:Inp] || -> equal(op2(e23,op2(e23,e23)),h4(e11))**. % 0.64/0.81 189[0:Inp] || SkC0 -> equal(op1(e10,op1(e10,e10)),e10)**. % 0.64/0.81 190[0:Inp] || SkC0 -> equal(op1(e11,op1(e10,e11)),e11)**. % 0.64/0.81 192[0:Inp] || SkC0 -> equal(op1(e13,op1(e10,e13)),e13)**. % 0.64/0.81 193[0:Inp] || SkC1 -> equal(op1(e10,op1(e11,e10)),e10)**. % 0.64/0.81 194[0:Inp] || SkC1 -> equal(op1(e11,op1(e11,e11)),e11)**. % 0.64/0.81 199[0:Inp] || SkC2 -> equal(op1(e12,op1(e12,e12)),e12)**. % 0.64/0.81 201[0:Inp] || SkC3 -> equal(op2(e20,op2(e20,e20)),e20)**. % 0.64/0.81 202[0:Inp] || SkC3 -> equal(op2(e21,op2(e20,e21)),e21)**. % 0.64/0.81 203[0:Inp] || SkC3 -> equal(op2(e22,op2(e20,e22)),e22)**. % 0.64/0.81 204[0:Inp] || SkC3 -> equal(op2(e23,op2(e20,e23)),e23)**. % 0.64/0.81 205[0:Inp] || SkC4 -> equal(op2(e20,op2(e21,e20)),e20)**. % 0.64/0.81 206[0:Inp] || SkC4 -> equal(op2(e21,op2(e21,e21)),e21)**. % 0.64/0.81 207[0:Inp] || SkC4 -> equal(op2(e22,op2(e21,e22)),e22)**. % 0.64/0.81 211[0:Inp] || SkC5 -> equal(op2(e22,op2(e22,e22)),e22)**. % 0.64/0.81 213[0:Inp] || -> equal(op1(e10,op1(e13,e10)),e10)** SkC0 SkC1 SkC2. % 0.64/0.81 214[0:Inp] || -> equal(op1(e11,op1(e13,e11)),e11)** SkC0 SkC1 SkC2. % 0.64/0.81 215[0:Inp] || -> equal(op1(e12,op1(e13,e12)),e12)** SkC0 SkC1 SkC2. % 0.64/0.81 216[0:Inp] || -> equal(op1(e13,op1(e13,e13)),e13)** SkC0 SkC1 SkC2. % 0.64/0.81 217[0:Inp] || -> equal(op2(e20,op2(e23,e20)),e20)** SkC3 SkC4 SkC5. % 0.64/0.81 218[0:Inp] || -> equal(op2(e21,op2(e23,e21)),e21)** SkC3 SkC4 SkC5. % 0.64/0.81 219[0:Inp] || -> equal(op2(e22,op2(e23,e22)),e22)** SkC3 SkC4 SkC5. % 0.64/0.81 220[0:Inp] || -> equal(op2(e23,op2(e23,e23)),e23)** SkC3 SkC4 SkC5. % 0.64/0.81 221[0:Inp] || -> equal(op1(op1(e12,op1(e12,e12)),op1(e12,e12)),e13)**. % 0.64/0.81 222[0:Inp] || -> equal(op2(op2(e22,op2(e22,e22)),op2(e22,e22)),e23)**. % 0.64/0.81 223[0:Inp] || -> equal(op2(op2(e20,op2(e20,e20)),op2(e20,e20)),h1(e13))**. % 0.64/0.81 224[0:Inp] || -> equal(op2(op2(e21,op2(e21,e21)),op2(e21,e21)),h2(e13))**. % 0.64/0.81 225[0:Inp] || -> equal(op2(op2(e22,op2(e22,e22)),op2(e22,e22)),h3(e13))**. % 0.64/0.81 226[0:Inp] || -> equal(op2(op2(e23,op2(e23,e23)),op2(e23,e23)),h4(e13))**. % 0.64/0.81 227[0:Inp] || -> equal(op2(e20,e23),e23) equal(op2(e21,e23),e23) equal(op2(e22,e23),e23) equal(op2(e23,e23),e23)**. % 0.64/0.81 228[0:Inp] || -> equal(op2(e23,e20),e23) equal(op2(e23,e21),e23) equal(op2(e23,e22),e23) equal(op2(e23,e23),e23)**. % 0.64/0.81 232[0:Inp] || -> equal(op2(e23,e20),e21) equal(op2(e23,e21),e21) equal(op2(e23,e22),e21) equal(op2(e23,e23),e21)**. % 0.64/0.81 234[0:Inp] || -> equal(op2(e23,e20),e20) equal(op2(e23,e21),e20) equal(op2(e23,e22),e20) equal(op2(e23,e23),e20)**. % 0.64/0.81 235[0:Inp] || -> equal(op2(e20,e22),e23) equal(op2(e21,e22),e23) equal(op2(e22,e22),e23) equal(op2(e23,e22),e23)**. % 0.64/0.81 236[0:Inp] || -> equal(op2(e22,e20),e23) equal(op2(e22,e21),e23) equal(op2(e22,e22),e23) equal(op2(e22,e23),e23)**. % 0.64/0.81 237[0:Inp] || -> equal(op2(e20,e22),e22) equal(op2(e21,e22),e22) equal(op2(e22,e22),e22) equal(op2(e23,e22),e22)**. % 0.64/0.81 238[0:Inp] || -> equal(op2(e22,e20),e22) equal(op2(e22,e21),e22) equal(op2(e22,e22),e22) equal(op2(e22,e23),e22)**. % 0.64/0.81 239[0:Inp] || -> equal(op2(e20,e22),e21) equal(op2(e21,e22),e21) equal(op2(e22,e22),e21) equal(op2(e23,e22),e21)**. % 0.64/0.81 243[0:Inp] || -> equal(op2(e20,e21),e23) equal(op2(e21,e21),e23) equal(op2(e22,e21),e23) equal(op2(e23,e21),e23)**. % 0.64/0.81 246[0:Inp] || -> equal(op2(e21,e20),e22) equal(op2(e21,e21),e22) equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.64/0.81 247[0:Inp] || -> equal(op2(e20,e21),e21) equal(op2(e21,e21),e21) equal(op2(e22,e21),e21) equal(op2(e23,e21),e21)**. % 0.64/0.81 248[0:Inp] || -> equal(op2(e21,e20),e21) equal(op2(e21,e21),e21) equal(op2(e21,e22),e21) equal(op2(e21,e23),e21)**. % 0.64/0.81 250[0:Inp] || -> equal(op2(e21,e20),e20) equal(op2(e21,e21),e20) equal(op2(e21,e22),e20) equal(op2(e21,e23),e20)**. % 0.64/0.81 252[0:Inp] || -> equal(op2(e20,e20),e23) equal(op2(e20,e21),e23) equal(op2(e20,e22),e23) equal(op2(e20,e23),e23)**. % 0.64/0.81 253[0:Inp] || -> equal(op2(e20,e20),e22) equal(op2(e21,e20),e22) equal(op2(e22,e20),e22) equal(op2(e23,e20),e22)**. % 0.64/0.81 254[0:Inp] || -> equal(op2(e20,e20),e22) equal(op2(e20,e21),e22) equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)**. % 0.64/0.81 256[0:Inp] || -> equal(op2(e20,e20),e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21) equal(op2(e20,e23),e21)**. % 0.64/0.81 257[0:Inp] || -> equal(op2(e20,e20),e20) equal(op2(e21,e20),e20) equal(op2(e22,e20),e20) equal(op2(e23,e20),e20)**. % 0.64/0.81 259[0:Inp] || -> equal(op2(e23,e23),e20) equal(op2(e23,e23),e21) equal(op2(e23,e23),e22) equal(op2(e23,e23),e23)**. % 0.64/0.81 260[0:Inp] || -> equal(op2(e23,e22),e20) equal(op2(e23,e22),e21) equal(op2(e23,e22),e22) equal(op2(e23,e22),e23)**. % 0.64/0.81 261[0:Inp] || -> equal(op2(e23,e21),e23)** equal(op2(e23,e21),e21) equal(op2(e23,e21),e22) equal(op2(e23,e21),e20). % 0.64/0.81 262[0:Inp] || -> equal(op2(e23,e20),e20) equal(op2(e23,e20),e21) equal(op2(e23,e20),e22) equal(op2(e23,e20),e23)**. % 0.64/0.81 263[0:Inp] || -> equal(op2(e22,e23),e20) equal(op2(e22,e23),e21) equal(op2(e22,e23),e22) equal(op2(e22,e23),e23)**. % 0.64/0.81 265[0:Inp] || -> equal(op2(e22,e21),e20) equal(op2(e22,e21),e21) equal(op2(e22,e21),e22) equal(op2(e22,e21),e23)**. % 0.64/0.81 267[0:Inp] || -> equal(op2(e21,e23),e20) equal(op2(e21,e23),e21) equal(op2(e21,e23),e22) equal(op2(e21,e23),e23)**. % 0.64/0.81 268[0:Inp] || -> equal(op2(e21,e22),e20) equal(op2(e21,e22),e21) equal(op2(e21,e22),e22) equal(op2(e21,e22),e23)**. % 0.64/0.81 269[0:Inp] || -> equal(op2(e21,e21),e20) equal(op2(e21,e21),e21) equal(op2(e21,e21),e22) equal(op2(e21,e21),e23)**. % 0.64/0.81 271[0:Inp] || -> equal(op2(e20,e23),e23)** equal(op2(e20,e23),e20) equal(op2(e20,e23),e22) equal(op2(e20,e23),e21). % 0.64/0.81 272[0:Inp] || -> equal(op2(e20,e22),e20) equal(op2(e20,e22),e21) equal(op2(e20,e22),e22) equal(op2(e20,e22),e23)**. % 0.64/0.81 273[0:Inp] || -> equal(op2(e20,e21),e21) equal(op2(e20,e21),e20) equal(op2(e20,e21),e23)** equal(op2(e20,e21),e22). % 0.64/0.81 276[0:Inp] || -> equal(op1(e13,e10),e13) equal(op1(e13,e11),e13) equal(op1(e13,e12),e13) equal(op1(e13,e13),e13)**. % 0.64/0.81 278[0:Inp] || -> equal(op1(e13,e13),e12)** equal(op1(e13,e12),e12) equal(op1(e13,e11),e12) equal(op1(e13,e10),e12). % 0.64/0.81 280[0:Inp] || -> equal(op1(e13,e10),e11) equal(op1(e13,e11),e11) equal(op1(e13,e12),e11) equal(op1(e13,e13),e11)**. % 0.64/0.81 281[0:Inp] || -> equal(op1(e10,e13),e10) equal(op1(e11,e13),e10) equal(op1(e12,e13),e10) equal(op1(e13,e13),e10)**. % 0.64/0.81 283[0:Inp] || -> equal(op1(e10,e12),e13) equal(op1(e11,e12),e13) equal(op1(e12,e12),e13) equal(op1(e13,e12),e13)**. % 0.64/0.81 284[0:Inp] || -> equal(op1(e12,e10),e13) equal(op1(e12,e11),e13) equal(op1(e12,e12),e13) equal(op1(e12,e13),e13)**. % 0.64/0.81 286[0:Inp] || -> equal(op1(e12,e10),e12) equal(op1(e12,e11),e12) equal(op1(e12,e12),e12) equal(op1(e12,e13),e12)**. % 0.64/0.81 291[0:Inp] || -> equal(op1(e10,e11),e13) equal(op1(e11,e11),e13) equal(op1(e12,e11),e13) equal(op1(e13,e11),e13)**. % 0.64/0.81 293[0:Inp] || -> equal(op1(e12,e11),e12) equal(op1(e11,e11),e12) equal(op1(e13,e11),e12)** equal(op1(e10,e11),e12). % 0.64/0.81 295[0:Inp] || -> equal(op1(e10,e11),e11) equal(op1(e11,e11),e11) equal(op1(e12,e11),e11) equal(op1(e13,e11),e11)**. % 0.64/0.81 297[0:Inp] || -> equal(op1(e10,e11),e10) equal(op1(e11,e11),e10) equal(op1(e12,e11),e10) equal(op1(e13,e11),e10)**. % 0.64/0.81 298[0:Inp] || -> equal(op1(e11,e10),e10) equal(op1(e11,e11),e10) equal(op1(e11,e12),e10) equal(op1(e11,e13),e10)**. % 0.64/0.81 300[0:Inp] || -> equal(op1(e10,e10),e13) equal(op1(e10,e11),e13) equal(op1(e10,e12),e13) equal(op1(e10,e13),e13)**. % 0.64/0.81 301[0:Inp] || -> equal(op1(e10,e10),e12) equal(op1(e11,e10),e12) equal(op1(e12,e10),e12) equal(op1(e13,e10),e12)**. % 0.64/0.81 302[0:Inp] || -> equal(op1(e10,e12),e12) equal(op1(e10,e10),e12) equal(op1(e10,e13),e12)** equal(op1(e10,e11),e12). % 0.64/0.81 305[0:Inp] || -> equal(op1(e10,e10),e10) equal(op1(e11,e10),e10) equal(op1(e12,e10),e10) equal(op1(e13,e10),e10)**. % 0.64/0.81 306[0:Inp] || -> equal(op1(e10,e10),e10) equal(op1(e10,e11),e10) equal(op1(e10,e12),e10) equal(op1(e10,e13),e10)**. % 0.64/0.81 307[0:Inp] || -> equal(op1(e13,e13),e13)** equal(op1(e13,e13),e12) equal(op1(e13,e13),e11) equal(op1(e13,e13),e10). % 0.64/0.81 309[0:Inp] || -> equal(op1(e13,e11),e13)** equal(op1(e13,e11),e11) equal(op1(e13,e11),e12) equal(op1(e13,e11),e10). % 0.64/0.81 310[0:Inp] || -> equal(op1(e13,e10),e10) equal(op1(e13,e10),e11) equal(op1(e13,e10),e12) equal(op1(e13,e10),e13)**. % 0.64/0.81 311[0:Inp] || -> equal(op1(e12,e13),e10) equal(op1(e12,e13),e11) equal(op1(e12,e13),e12) equal(op1(e12,e13),e13)**. % 0.64/0.81 313[0:Inp] || -> equal(op1(e12,e11),e10) equal(op1(e12,e11),e11) equal(op1(e12,e11),e12) equal(op1(e12,e11),e13)**. % 0.64/0.81 316[0:Inp] || -> equal(op1(e11,e12),e10) equal(op1(e11,e12),e11) equal(op1(e11,e12),e12) equal(op1(e11,e12),e13)**. % 0.64/0.81 319[0:Inp] || -> equal(op1(e10,e13),e13)** equal(op1(e10,e13),e10) equal(op1(e10,e13),e12) equal(op1(e10,e13),e11). % 0.64/0.81 320[0:Inp] || -> equal(op1(e10,e12),e10) equal(op1(e10,e12),e11) equal(op1(e10,e12),e12) equal(op1(e10,e12),e13)**. % 0.64/0.81 321[0:Inp] || -> equal(op1(e10,e11),e11) equal(op1(e10,e11),e10) equal(op1(e10,e11),e13)** equal(op1(e10,e11),e12). % 0.64/0.81 322[0:Inp] || -> equal(op1(e10,e10),e10) equal(op1(e10,e10),e11) equal(op1(e10,e10),e12) equal(op1(e10,e10),e13)**. % 0.64/0.81 327[0:Inp] || equal(h3(e13),e23) equal(op2(h3(e10),h3(e10)),h3(op1(e10,e10))) equal(op2(h3(e10),h3(e11)),h3(op1(e10,e11))) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),h3(e13)),h3(op1(e10,e13))) equal(op2(h3(e11),h3(e10)),h3(op1(e11,e10))) equal(op2(h3(e11),h3(e11)),h3(op1(e11,e11))) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),h3(e13)),h3(op1(e11,e13))) equal(op2(h3(e12),h3(e10)),h3(op1(e12,e10))) equal(op2(h3(e12),h3(e11)),h3(op1(e12,e11))) equal(op2(h3(e12),h3(e12)),h3(op1(e12,e12))) equal(op2(h3(e12),h3(e13)),h3(op1(e12,e13))) equal(op2(h3(e13),h3(e10)),h3(op1(e13,e10))) equal(op2(h3(e13),h3(e11)),h3(op1(e13,e11))) equal(op2(h3(e13),h3(e12)),h3(op1(e13,e12))) equal(op2(h3(e13),h3(e13)),h3(op1(e13,e13)))** SkC12 SkC13 SkC14 -> . % 0.64/0.81 339[0:Rew:34.0,85.0] || -> equal(h3(e10),e20)**. % 0.64/0.81 343[0:Rew:31.0,69.0] || equal(e22,e22) -> SkC14*. % 0.64/0.81 344[0:Obv:343.0] || -> SkC14*. % 0.64/0.81 348[0:Rew:339.0,59.0] || equal(e20,e20) -> SkC12*. % 0.64/0.81 349[0:Obv:348.0] || -> SkC12*. % 0.64/0.81 358[0:Rew:34.0,88.0] || -> equal(op2(e22,e20),e21)**. % 0.64/0.81 359[0:Rew:33.0,87.0] || -> equal(op1(e12,e10),e11)**. % 0.64/0.81 360[0:Rew:86.0,188.0] || -> equal(op2(e23,h4(e10)),h4(e11))**. % 0.64/0.81 361[0:Rew:358.0,187.0,34.0,187.0] || -> equal(h3(e11),e21)**. % 0.64/0.81 362[0:Rew:361.0,64.0] || equal(e21,e21) -> SkC13*. % 0.64/0.81 363[0:Obv:362.0] || -> SkC13*. % 0.64/0.81 364[0:Rew:84.0,186.0] || -> equal(op2(e21,h2(e10)),h2(e11))**. % 0.64/0.81 365[0:Rew:83.0,185.0] || -> equal(op2(e20,h1(e10)),h1(e11))**. % 0.64/0.81 366[0:Rew:86.0,184.0] || equal(op2(e23,e22),h4(e10))** -> . % 0.64/0.81 367[0:Rew:86.0,183.0] || equal(op2(e23,e21),h4(e10))** -> . % 0.64/0.81 368[0:Rew:86.0,181.0] || equal(op2(e23,e20),h4(e10))** -> . % 0.64/0.81 369[0:Rew:34.0,178.0] || equal(op2(e22,e23),e20)** -> . % 0.64/0.81 370[0:Rew:34.0,176.0] || equal(op2(e22,e21),e20)** -> . % 0.64/0.81 371[0:Rew:358.0,175.0] || equal(op2(e22,e23),e21)** -> . % 0.64/0.81 373[0:Rew:358.0,173.0] || equal(op2(e22,e21),e21)** -> . % 0.64/0.81 374[0:Rew:84.0,171.0] || equal(op2(e21,e23),h2(e10))** -> . % 0.64/0.81 375[0:Rew:84.0,170.0] || equal(op2(e21,e22),h2(e10))** -> . % 0.64/0.81 376[0:Rew:84.0,167.0] || equal(op2(e21,e20),h2(e10))** -> . % 0.64/0.81 380[0:Rew:86.0,160.0] || equal(op2(e22,e23),h4(e10))** -> . % 0.64/0.81 381[0:Rew:86.0,159.0] || equal(op2(e21,e23),h4(e10))** -> . % 0.64/0.81 382[0:Rew:86.0,157.0] || equal(op2(e20,e23),h4(e10))** -> . % 0.64/0.81 383[0:Rew:34.0,154.0] || equal(op2(e23,e22),e20)** -> . % 0.64/0.81 384[0:Rew:34.0,152.0] || equal(op2(e21,e22),e20)** -> . % 0.64/0.81 385[0:Rew:34.0,150.0] || equal(op2(e20,e22),e20)** -> . % 0.64/0.81 386[0:Rew:84.0,147.0] || equal(op2(e23,e21),h2(e10))** -> . % 0.64/0.81 387[0:Rew:84.0,146.0] || equal(op2(e22,e21),h2(e10))** -> . % 0.64/0.81 388[0:Rew:84.0,143.0] || equal(op2(e20,e21),h2(e10))** -> . % 0.64/0.81 389[0:Rew:358.0,142.0] || equal(op2(e23,e20),e21)** -> . % 0.64/0.81 392[0:Rew:358.0,138.0,83.0,138.0] || equal(h1(e10),e21)** -> . % 0.64/0.81 393[0:Rew:83.0,137.0] || equal(op2(e21,e20),h1(e10))** -> . % 0.64/0.81 394[0:Rew:33.0,130.0] || equal(op1(e12,e13),e10)** -> . % 0.64/0.81 395[0:Rew:33.0,128.0] || equal(op1(e12,e11),e10)** -> . % 0.64/0.81 396[0:Rew:359.0,127.0] || equal(op1(e12,e13),e11)** -> . % 0.64/0.81 398[0:Rew:359.0,125.0] || equal(op1(e12,e11),e11)** -> . % 0.64/0.81 400[0:Rew:33.0,104.0] || equal(op1(e11,e12),e10)** -> . % 0.64/0.81 401[0:Rew:33.0,102.0] || equal(op1(e10,e12),e10)** -> . % 0.64/0.81 402[0:Rew:359.0,94.0] || equal(op1(e13,e10),e11)** -> . % 0.64/0.81 404[0:Rew:359.0,90.0] || equal(op1(e10,e10),e11)** -> . % 0.64/0.81 405[0:Rew:358.0,211.1,34.0,211.1] || SkC5* -> equal(e22,e21). % 0.64/0.81 406[0:MRR:405.1,10.0] || SkC5* -> . % 0.64/0.81 407[0:Rew:364.0,206.1,84.0,206.1] || SkC4 -> equal(h2(e11),e21)**. % 0.64/0.81 408[0:Rew:365.0,201.1,83.0,201.1] || SkC3 -> equal(h1(e11),e20)**. % 0.64/0.81 409[0:Rew:359.0,199.1,33.0,199.1] || SkC2* -> equal(e12,e11). % 0.64/0.81 410[0:MRR:409.1,4.0] || SkC2* -> . % 0.64/0.81 411[0:Rew:360.0,220.0,86.0,220.0] || -> equal(h4(e11),e23)** SkC3 SkC4 SkC5. % 0.64/0.81 412[0:MRR:411.3,406.0] || -> SkC4 SkC3 equal(h4(e11),e23)**. % 0.64/0.81 413[0:MRR:219.3,406.0] || -> SkC4 SkC3 equal(op2(e22,op2(e23,e22)),e22)**. % 0.64/0.81 414[0:MRR:218.3,406.0] || -> SkC4 SkC3 equal(op2(e21,op2(e23,e21)),e21)**. % 0.64/0.81 415[0:MRR:217.3,406.0] || -> SkC4 SkC3 equal(op2(e20,op2(e23,e20)),e20)**. % 0.64/0.81 416[0:MRR:216.3,410.0] || -> SkC1 SkC0 equal(op1(e13,op1(e13,e13)),e13)**. % 0.64/0.81 417[0:MRR:215.3,410.0] || -> SkC1 SkC0 equal(op1(e12,op1(e13,e12)),e12)**. % 0.64/0.81 418[0:MRR:214.3,410.0] || -> SkC1 SkC0 equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.81 419[0:MRR:213.3,410.0] || -> SkC1 SkC0 equal(op1(e10,op1(e13,e10)),e10)**. % 0.64/0.81 420[0:Rew:358.0,222.0,34.0,222.0] || -> equal(op2(e21,e20),e23)**. % 0.64/0.81 421[0:Rew:420.0,169.0] || equal(op2(e21,e23),e23)** -> . % 0.64/0.81 422[0:Rew:420.0,168.0] || equal(op2(e21,e22),e23)** -> . % 0.64/0.81 423[0:Rew:420.0,376.0] || equal(h2(e10),e23)** -> . % 0.64/0.81 424[0:Rew:420.0,141.0] || equal(op2(e23,e20),e23)** -> . % 0.64/0.81 426[0:Rew:420.0,393.0] || equal(h1(e10),e23)** -> . % 0.64/0.81 427[0:Rew:420.0,205.1] || SkC4 -> equal(op2(e20,e23),e20)**. % 0.64/0.81 428[0:Rew:359.0,221.0,33.0,221.0] || -> equal(op1(e11,e10),e13)**. % 0.64/0.81 430[0:Rew:428.0,120.0] || equal(op1(e11,e12),e13)** -> . % 0.64/0.81 431[0:Rew:428.0,119.0] || equal(op1(e11,e11),e13)** -> . % 0.64/0.81 432[0:Rew:428.0,93.0] || equal(op1(e13,e10),e13)** -> . % 0.64/0.81 434[0:Rew:428.0,89.0] || equal(op1(e10,e10),e13)** -> . % 0.64/0.81 435[0:Rew:428.0,193.1] || SkC1 -> equal(op1(e10,e13),e10)**. % 0.64/0.81 436[0:Rew:360.0,226.0,86.0,226.0] || -> equal(op2(h4(e11),h4(e10)),h4(e13))**. % 0.64/0.81 437[0:Rew:420.0,225.0,358.0,225.0,34.0,225.0] || -> equal(h3(e13),e23)**. % 0.64/0.81 438[0:Rew:364.0,224.0,84.0,224.0] || -> equal(op2(h2(e11),h2(e10)),h2(e13))**. % 0.64/0.81 439[0:Rew:365.0,223.0,83.0,223.0] || -> equal(op2(h1(e11),h1(e10)),h1(e13))**. % 0.64/0.81 440[0:Rew:86.0,227.3] || -> equal(op2(e20,e23),e23) equal(op2(e21,e23),e23) equal(op2(e22,e23),e23)** equal(h4(e10),e23). % 0.64/0.81 441[0:MRR:440.1,421.0] || -> equal(h4(e10),e23) equal(op2(e22,e23),e23)** equal(op2(e20,e23),e23). % 0.64/0.81 442[0:Rew:86.0,228.3] || -> equal(op2(e23,e20),e23) equal(op2(e23,e21),e23) equal(op2(e23,e22),e23)** equal(h4(e10),e23). % 0.64/0.81 443[0:MRR:442.0,424.0] || -> equal(h4(e10),e23) equal(op2(e23,e22),e23)** equal(op2(e23,e21),e23). % 0.64/0.81 448[0:Rew:86.0,232.3] || -> equal(op2(e23,e20),e21) equal(op2(e23,e21),e21) equal(op2(e23,e22),e21)** equal(h4(e10),e21). % 0.64/0.81 449[0:MRR:448.0,389.0] || -> equal(h4(e10),e21) equal(op2(e23,e21),e21) equal(op2(e23,e22),e21)**. % 0.64/0.81 452[0:Rew:86.0,234.3] || -> equal(op2(e23,e20),e20) equal(op2(e23,e21),e20) equal(op2(e23,e22),e20)** equal(h4(e10),e20). % 0.64/0.81 453[0:MRR:452.2,383.0] || -> equal(h4(e10),e20) equal(op2(e23,e20),e20) equal(op2(e23,e21),e20)**. % 0.64/0.81 454[0:Rew:34.0,235.2] || -> equal(op2(e20,e22),e23) equal(op2(e21,e22),e23) equal(e23,e20) equal(op2(e23,e22),e23)**. % 0.64/0.81 455[0:MRR:454.1,454.2,422.0,9.0] || -> equal(op2(e23,e22),e23)** equal(op2(e20,e22),e23). % 0.64/0.81 456[0:Rew:34.0,236.2,358.0,236.0] || -> equal(e23,e21) equal(op2(e22,e21),e23) equal(e23,e20) equal(op2(e22,e23),e23)**. % 0.64/0.81 457[0:MRR:456.0,456.2,11.0,9.0] || -> equal(op2(e22,e23),e23)** equal(op2(e22,e21),e23). % 0.64/0.81 458[0:Rew:34.0,237.2] || -> equal(op2(e20,e22),e22) equal(op2(e21,e22),e22) equal(e22,e20) equal(op2(e23,e22),e22)**. % 0.64/0.81 459[0:MRR:458.2,8.0] || -> equal(op2(e23,e22),e22)** equal(op2(e21,e22),e22) equal(op2(e20,e22),e22). % 0.64/0.81 460[0:Rew:34.0,238.2,358.0,238.0] || -> equal(e22,e21) equal(op2(e22,e21),e22) equal(e22,e20) equal(op2(e22,e23),e22)**. % 0.64/0.81 461[0:MRR:460.0,460.2,10.0,8.0] || -> equal(op2(e22,e23),e22)** equal(op2(e22,e21),e22). % 0.64/0.81 462[0:Rew:34.0,239.2] || -> equal(op2(e20,e22),e21) equal(op2(e21,e22),e21) equal(e21,e20) equal(op2(e23,e22),e21)**. % 0.64/0.81 463[0:MRR:462.2,7.0] || -> equal(op2(e21,e22),e21) equal(op2(e23,e22),e21)** equal(op2(e20,e22),e21). % 0.64/0.81 464[0:Rew:84.0,243.1] || -> equal(op2(e20,e21),e23) equal(h2(e10),e23) equal(op2(e22,e21),e23) equal(op2(e23,e21),e23)**. % 0.64/0.81 465[0:MRR:464.1,423.0] || -> equal(op2(e23,e21),e23)** equal(op2(e22,e21),e23) equal(op2(e20,e21),e23). % 0.64/0.81 467[0:Rew:84.0,246.1,420.0,246.0] || -> equal(e23,e22) equal(h2(e10),e22) equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.64/0.81 468[0:MRR:467.0,12.0] || -> equal(h2(e10),e22) equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.64/0.81 469[0:Rew:84.0,247.1] || -> equal(op2(e20,e21),e21) equal(h2(e10),e21) equal(op2(e22,e21),e21) equal(op2(e23,e21),e21)**. % 0.64/0.81 470[0:MRR:469.2,373.0] || -> equal(h2(e10),e21) equal(op2(e23,e21),e21)** equal(op2(e20,e21),e21). % 0.64/0.81 471[0:Rew:84.0,248.1,420.0,248.0] || -> equal(e23,e21) equal(h2(e10),e21) equal(op2(e21,e22),e21) equal(op2(e21,e23),e21)**. % 0.64/0.81 472[0:MRR:471.0,11.0] || -> equal(h2(e10),e21) equal(op2(e21,e23),e21)** equal(op2(e21,e22),e21). % 0.64/0.81 475[0:Rew:84.0,250.1,420.0,250.0] || -> equal(e23,e20) equal(h2(e10),e20) equal(op2(e21,e22),e20) equal(op2(e21,e23),e20)**. % 0.64/0.81 476[0:MRR:475.0,475.2,9.0,384.0] || -> equal(h2(e10),e20) equal(op2(e21,e23),e20)**. % 0.64/0.81 477[0:Rew:83.0,252.0] || -> equal(h1(e10),e23) equal(op2(e20,e21),e23) equal(op2(e20,e22),e23) equal(op2(e20,e23),e23)**. % 0.64/0.81 478[0:MRR:477.0,426.0] || -> equal(op2(e20,e23),e23)** equal(op2(e20,e22),e23) equal(op2(e20,e21),e23). % 0.64/0.81 479[0:Rew:358.0,253.2,420.0,253.1,83.0,253.0] || -> equal(h1(e10),e22) equal(e23,e22) equal(e22,e21) equal(op2(e23,e20),e22)**. % 0.64/0.81 480[0:MRR:479.1,479.2,12.0,10.0] || -> equal(h1(e10),e22) equal(op2(e23,e20),e22)**. % 0.64/0.81 481[0:Rew:83.0,254.0] || -> equal(h1(e10),e22) equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)** equal(op2(e20,e21),e22). % 0.64/0.81 482[0:Rew:83.0,256.0] || -> equal(h1(e10),e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21) equal(op2(e20,e23),e21)**. % 0.64/0.81 483[0:MRR:482.0,392.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e23),e21)** equal(op2(e20,e22),e21). % 0.64/0.81 484[0:Rew:358.0,257.2,420.0,257.1,83.0,257.0] || -> equal(h1(e10),e20) equal(e23,e20) equal(e21,e20) equal(op2(e23,e20),e20)**. % 0.64/0.81 485[0:MRR:484.1,484.2,9.0,7.0] || -> equal(h1(e10),e20) equal(op2(e23,e20),e20)**. % 0.64/0.81 488[0:Rew:86.0,259.3,86.0,259.2,86.0,259.1,86.0,259.0] || -> equal(h4(e10),e23)** equal(h4(e10),e22) equal(h4(e10),e21) equal(h4(e10),e20). % 0.64/0.81 489[0:MRR:260.0,383.0] || -> equal(op2(e23,e22),e23)** equal(op2(e23,e22),e22) equal(op2(e23,e22),e21). % 0.64/0.81 490[0:MRR:262.1,262.3,389.0,424.0] || -> equal(op2(e23,e20),e20) equal(op2(e23,e20),e22)**. % 0.64/0.81 491[0:MRR:263.0,263.1,369.0,371.0] || -> equal(op2(e22,e23),e23)** equal(op2(e22,e23),e22). % 0.64/0.81 492[0:MRR:265.0,265.1,370.0,373.0] || -> equal(op2(e22,e21),e22) equal(op2(e22,e21),e23)**. % 0.64/0.81 493[0:MRR:267.3,421.0] || -> equal(op2(e21,e23),e21) equal(op2(e21,e23),e22)** equal(op2(e21,e23),e20). % 0.64/0.81 494[0:MRR:268.0,268.3,384.0,422.0] || -> equal(op2(e21,e22),e22)** equal(op2(e21,e22),e21). % 0.64/0.81 495[0:Rew:84.0,269.3,84.0,269.2,84.0,269.1,84.0,269.0] || -> equal(h2(e10),e20) equal(h2(e10),e21) equal(h2(e10),e22) equal(h2(e10),e23)**. % 0.64/0.81 496[0:MRR:495.3,423.0] || -> equal(h2(e10),e22)** equal(h2(e10),e21) equal(h2(e10),e20). % 0.64/0.81 497[0:MRR:272.0,385.0] || -> equal(op2(e20,e22),e22) equal(op2(e20,e22),e23)** equal(op2(e20,e22),e21). % 0.64/0.81 501[0:MRR:276.0,432.0] || -> equal(op1(e13,e13),e13)** equal(op1(e13,e12),e13) equal(op1(e13,e11),e13). % 0.64/0.81 503[0:MRR:280.0,402.0] || -> equal(op1(e13,e13),e11)** equal(op1(e13,e11),e11) equal(op1(e13,e12),e11). % 0.64/0.81 504[0:MRR:281.2,394.0] || -> equal(op1(e13,e13),e10)** equal(op1(e10,e13),e10) equal(op1(e11,e13),e10). % 0.64/0.81 506[0:Rew:33.0,283.2] || -> equal(op1(e10,e12),e13) equal(op1(e11,e12),e13) equal(e13,e10) equal(op1(e13,e12),e13)**. % 0.64/0.81 507[0:MRR:506.1,506.2,430.0,3.0] || -> equal(op1(e13,e12),e13)** equal(op1(e10,e12),e13). % 0.64/0.81 508[0:Rew:33.0,284.2,359.0,284.0] || -> equal(e13,e11) equal(op1(e12,e11),e13) equal(e13,e10) equal(op1(e12,e13),e13)**. % 0.64/0.81 509[0:MRR:508.0,508.2,5.0,3.0] || -> equal(op1(e12,e13),e13)** equal(op1(e12,e11),e13). % 0.64/0.81 512[0:Rew:33.0,286.2,359.0,286.0] || -> equal(e12,e11) equal(op1(e12,e11),e12) equal(e12,e10) equal(op1(e12,e13),e12)**. % 0.64/0.81 513[0:MRR:512.0,512.2,4.0,2.0] || -> equal(op1(e12,e13),e12)** equal(op1(e12,e11),e12). % 0.64/0.81 516[0:MRR:291.1,431.0] || -> equal(op1(e13,e11),e13)** equal(op1(e12,e11),e13) equal(op1(e10,e11),e13). % 0.64/0.81 519[0:MRR:295.2,398.0] || -> equal(op1(e11,e11),e11) equal(op1(e13,e11),e11)** equal(op1(e10,e11),e11). % 0.64/0.81 522[0:MRR:297.2,395.0] || -> equal(op1(e11,e11),e10) equal(op1(e10,e11),e10) equal(op1(e13,e11),e10)**. % 0.64/0.81 523[0:Rew:428.0,298.0] || -> equal(e13,e10) equal(op1(e11,e11),e10) equal(op1(e11,e12),e10) equal(op1(e11,e13),e10)**. % 0.64/0.81 524[0:MRR:523.0,523.2,3.0,400.0] || -> equal(op1(e11,e11),e10) equal(op1(e11,e13),e10)**. % 0.64/0.81 525[0:MRR:300.0,434.0] || -> equal(op1(e10,e13),e13)** equal(op1(e10,e12),e13) equal(op1(e10,e11),e13). % 0.64/0.81 526[0:Rew:359.0,301.2,428.0,301.1] || -> equal(op1(e10,e10),e12) equal(e13,e12) equal(e12,e11) equal(op1(e13,e10),e12)**. % 0.64/0.81 527[0:MRR:526.1,526.2,6.0,4.0] || -> equal(op1(e10,e10),e12) equal(op1(e13,e10),e12)**. % 0.64/0.81 529[0:Rew:359.0,305.2,428.0,305.1] || -> equal(op1(e10,e10),e10) equal(e13,e10) equal(e11,e10) equal(op1(e13,e10),e10)**. % 0.64/0.81 530[0:MRR:529.1,529.2,3.0,1.0] || -> equal(op1(e10,e10),e10) equal(op1(e13,e10),e10)**. % 0.64/0.81 531[0:MRR:306.2,401.0] || -> equal(op1(e10,e10),e10) equal(op1(e10,e13),e10)** equal(op1(e10,e11),e10). % 0.64/0.81 533[0:MRR:310.1,310.3,402.0,432.0] || -> equal(op1(e13,e10),e10) equal(op1(e13,e10),e12)**. % 0.64/0.81 534[0:MRR:311.0,311.1,394.0,396.0] || -> equal(op1(e12,e13),e13)** equal(op1(e12,e13),e12). % 0.64/0.81 535[0:MRR:313.0,313.1,395.0,398.0] || -> equal(op1(e12,e11),e12) equal(op1(e12,e11),e13)**. % 0.64/0.81 537[0:MRR:316.0,316.3,400.0,430.0] || -> equal(op1(e11,e12),e12)** equal(op1(e11,e12),e11). % 0.64/0.81 539[0:MRR:320.0,401.0] || -> equal(op1(e10,e12),e12) equal(op1(e10,e12),e13)** equal(op1(e10,e12),e11). % 0.64/0.81 540[0:MRR:322.1,322.3,404.0,434.0] || -> equal(op1(e10,e10),e10) equal(op1(e10,e10),e12)**. % 0.64/0.81 549[0:Rew:86.0,327.16,437.0,327.16,437.0,327.15,31.0,327.15,437.0,327.14,361.0,327.14,437.0,327.13,339.0,327.13,31.0,327.12,437.0,327.12,34.0,327.11,31.0,327.11,339.0,327.11,33.0,327.11,31.0,327.10,361.0,327.10,358.0,327.9,31.0,327.9,339.0,327.9,361.0,327.9,359.0,327.9,361.0,327.8,437.0,327.8,361.0,327.7,31.0,327.7,84.0,327.6,361.0,327.6,420.0,327.5,361.0,327.5,339.0,327.5,437.0,327.5,428.0,327.5,339.0,327.4,437.0,327.4,339.0,327.3,31.0,327.3,339.0,327.2,361.0,327.2,83.0,327.1,339.0,327.1,437.0,327.0] || equal(e23,e23) equal(h3(op1(e10,e10)),h1(e10)) equal(h3(op1(e10,e11)),op2(e20,e21)) equal(h3(op1(e10,e12)),op2(e20,e22)) equal(h3(op1(e10,e13)),op2(e20,e23)) equal(e23,e23) equal(h3(op1(e11,e11)),h2(e10)) equal(h3(op1(e11,e12)),op2(e21,e22)) equal(h3(op1(e11,e13)),op2(e21,e23)) equal(e21,e21) equal(h3(op1(e12,e11)),op2(e22,e21)) equal(e20,e20) equal(h3(op1(e12,e13)),op2(e22,e23)) equal(h3(op1(e13,e10)),op2(e23,e20)) equal(h3(op1(e13,e11)),op2(e23,e21)) equal(h3(op1(e13,e12)),op2(e23,e22)) equal(h3(op1(e13,e13)),h4(e10))** SkC12 SkC13 SkC14 -> . % 0.64/0.81 550[0:Obv:549.11] || equal(h3(op1(e10,e10)),h1(e10)) equal(h3(op1(e10,e11)),op2(e20,e21)) equal(h3(op1(e10,e12)),op2(e20,e22)) equal(h3(op1(e10,e13)),op2(e20,e23)) equal(h3(op1(e11,e11)),h2(e10)) equal(h3(op1(e11,e12)),op2(e21,e22)) equal(h3(op1(e11,e13)),op2(e21,e23)) equal(h3(op1(e12,e11)),op2(e22,e21)) equal(h3(op1(e12,e13)),op2(e22,e23)) equal(h3(op1(e13,e10)),op2(e23,e20)) equal(h3(op1(e13,e11)),op2(e23,e21)) equal(h3(op1(e13,e12)),op2(e23,e22)) equal(h3(op1(e13,e13)),h4(e10))** SkC12 SkC13 SkC14 -> . % 0.64/0.81 551[0:MRR:550.13,550.14,550.15,349.0,363.0,344.0] || equal(h3(op1(e10,e10)),h1(e10)) equal(h3(op1(e13,e13)),h4(e10))** equal(h3(op1(e11,e11)),h2(e10)) equal(h3(op1(e13,e12)),op2(e23,e22)) equal(h3(op1(e13,e11)),op2(e23,e21)) equal(h3(op1(e13,e10)),op2(e23,e20)) equal(h3(op1(e12,e13)),op2(e22,e23)) equal(h3(op1(e12,e11)),op2(e22,e21)) equal(h3(op1(e11,e13)),op2(e21,e23)) equal(h3(op1(e11,e12)),op2(e21,e22)) equal(h3(op1(e10,e13)),op2(e20,e23)) equal(h3(op1(e10,e12)),op2(e20,e22)) equal(h3(op1(e10,e11)),op2(e20,e21)) -> . % 0.64/0.81 574[1:Spt:488.0] || -> equal(h4(e10),e23)**. % 0.64/0.81 578[1:Rew:574.0,449.0] || -> equal(e23,e21) equal(op2(e23,e21),e21) equal(op2(e23,e22),e21)**. % 0.64/0.81 581[1:Rew:574.0,453.0] || -> equal(e23,e20) equal(op2(e23,e20),e20) equal(op2(e23,e21),e20)**. % 0.64/0.81 586[1:Rew:574.0,366.0] || equal(op2(e23,e22),e23)** -> . % 0.64/0.81 587[1:Rew:574.0,367.0] || equal(op2(e23,e21),e23)** -> . % 0.64/0.81 589[1:Rew:574.0,380.0] || equal(op2(e22,e23),e23)** -> . % 0.64/0.81 591[1:Rew:574.0,382.0] || equal(op2(e20,e23),e23)** -> . % 0.64/0.81 599[1:MRR:455.0,586.0] || -> equal(op2(e20,e22),e23)**. % 0.64/0.81 601[1:Rew:599.0,481.1] || -> equal(h1(e10),e22) equal(e23,e22) equal(op2(e20,e23),e22)** equal(op2(e20,e21),e22). % 0.64/0.81 602[1:Rew:599.0,459.2] || -> equal(op2(e23,e22),e22)** equal(op2(e21,e22),e22) equal(e23,e22). % 0.64/0.81 603[1:Rew:599.0,483.2] || -> equal(op2(e20,e21),e21) equal(op2(e20,e23),e21)** equal(e23,e21). % 0.64/0.81 604[1:Rew:599.0,463.2] || -> equal(op2(e21,e22),e21) equal(op2(e23,e22),e21)** equal(e23,e21). % 0.64/0.81 614[1:MRR:457.0,589.0] || -> equal(op2(e22,e21),e23)**. % 0.64/0.81 615[1:MRR:491.0,589.0] || -> equal(op2(e22,e23),e22)**. % 0.64/0.81 626[1:Rew:615.0,158.0] || equal(op2(e21,e23),e22)** -> . % 0.64/0.81 627[1:Rew:615.0,156.0] || equal(op2(e20,e23),e22)** -> . % 0.64/0.81 629[1:MRR:271.0,591.0] || -> equal(op2(e20,e23),e20) equal(op2(e20,e23),e22)** equal(op2(e20,e23),e21). % 0.64/0.81 632[1:MRR:468.2,626.0] || -> equal(h2(e10),e22) equal(op2(e21,e22),e22)**. % 0.64/0.81 638[1:MRR:578.0,11.0] || -> equal(op2(e23,e21),e21) equal(op2(e23,e22),e21)**. % 0.64/0.81 640[1:MRR:581.0,9.0] || -> equal(op2(e23,e20),e20) equal(op2(e23,e21),e20)**. % 0.64/0.81 642[1:MRR:602.2,12.0] || -> equal(op2(e23,e22),e22)** equal(op2(e21,e22),e22). % 0.64/0.81 643[1:MRR:603.2,11.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e23),e21)**. % 0.64/0.81 644[1:MRR:604.2,11.0] || -> equal(op2(e21,e22),e21) equal(op2(e23,e22),e21)**. % 0.64/0.81 645[1:MRR:629.1,627.0] || -> equal(op2(e20,e23),e20) equal(op2(e20,e23),e21)**. % 0.64/0.81 646[1:MRR:601.1,601.2,12.0,627.0] || -> equal(h1(e10),e22) equal(op2(e20,e21),e22)**. % 0.64/0.81 652[2:Spt:319.0] || -> equal(op1(e10,e13),e13)**. % 0.64/0.81 653[2:Rew:652.0,531.1] || -> equal(op1(e10,e10),e10) equal(e13,e10) equal(op1(e10,e11),e10)**. % 0.64/0.81 655[2:Rew:652.0,435.1] || SkC1* -> equal(e13,e10). % 0.64/0.81 664[2:Rew:652.0,118.0] || equal(op1(e10,e12),e13)** -> . % 0.64/0.81 667[2:Rew:652.0,109.0] || equal(op1(e13,e13),e13)** -> . % 0.64/0.81 668[2:Rew:652.0,108.0] || equal(op1(e12,e13),e13)** -> . % 0.64/0.81 670[2:Rew:652.0,192.1] || SkC0 -> equal(op1(e13,e13),e13)**. % 0.64/0.81 673[2:MRR:655.1,3.0] || SkC1* -> . % 0.64/0.81 676[2:MRR:418.0,673.0] || -> SkC0 equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.81 677[2:MRR:419.0,673.0] || -> SkC0 equal(op1(e10,op1(e13,e10)),e10)**. % 0.64/0.81 678[2:MRR:507.1,664.0] || -> equal(op1(e13,e12),e13)**. % 0.64/0.81 680[2:Rew:678.0,278.1] || -> equal(op1(e13,e13),e12)** equal(e13,e12) equal(op1(e13,e11),e12) equal(op1(e13,e10),e12). % 0.64/0.81 686[2:Rew:678.0,134.0] || equal(op1(e13,e11),e13)** -> . % 0.64/0.81 694[2:MRR:534.0,668.0] || -> equal(op1(e12,e13),e12)**. % 0.64/0.81 705[2:Rew:694.0,112.0] || equal(op1(e13,e13),e12)** -> . % 0.64/0.81 708[2:MRR:309.0,686.0] || -> equal(op1(e13,e11),e11) equal(op1(e13,e11),e12)** equal(op1(e13,e11),e10). % 0.64/0.81 712[2:MRR:670.1,667.0] || SkC0* -> . % 0.64/0.81 715[2:MRR:676.0,712.0] || -> equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.81 716[2:MRR:677.0,712.0] || -> equal(op1(e10,op1(e13,e10)),e10)**. % 0.64/0.81 717[2:MRR:653.1,3.0] || -> equal(op1(e10,e10),e10) equal(op1(e10,e11),e10)**. % 0.64/0.81 726[2:MRR:680.0,680.1,705.0,6.0] || -> equal(op1(e13,e11),e12)** equal(op1(e13,e10),e12). % 0.64/0.81 737[3:Spt:522.2] || -> equal(op1(e13,e11),e10)**. % 0.64/0.81 741[3:Rew:737.0,131.0] || equal(op1(e13,e10),e10)** -> . % 0.64/0.81 772[3:MRR:533.0,741.0] || -> equal(op1(e13,e10),e12)**. % 0.64/0.81 782[3:Rew:772.0,716.0] || -> equal(op1(e10,e12),e10)**. % 0.64/0.81 784[3:MRR:782.0,401.0] || -> . % 0.64/0.81 804[3:Spt:784.0,522.2,737.0] || equal(op1(e13,e11),e10)** -> . % 0.64/0.81 805[3:Spt:784.0,522.0,522.1] || -> equal(op1(e11,e11),e10)** equal(op1(e10,e11),e10). % 0.64/0.81 807[3:MRR:708.2,804.0] || -> equal(op1(e13,e11),e11) equal(op1(e13,e11),e12)**. % 0.64/0.81 808[4:Spt:805.0] || -> equal(op1(e11,e11),e10)**. % 0.64/0.81 813[4:Rew:808.0,95.0] || equal(op1(e10,e11),e10)** -> . % 0.64/0.81 823[4:MRR:717.1,813.0] || -> equal(op1(e10,e10),e10)**. % 0.64/0.81 827[4:Rew:823.0,91.0] || equal(op1(e13,e10),e10)** -> . % 0.64/0.81 847[4:MRR:533.0,827.0] || -> equal(op1(e13,e10),e12)**. % 0.64/0.81 851[4:Rew:847.0,131.0] || equal(op1(e13,e11),e12)** -> . % 0.64/0.81 865[4:MRR:807.1,851.0] || -> equal(op1(e13,e11),e11)**. % 0.64/0.81 868[4:Rew:865.0,715.0] || -> equal(op1(e11,e11),e11)**. % 0.64/0.81 871[4:Rew:808.0,868.0] || -> equal(e11,e10)**. % 0.64/0.81 872[4:MRR:871.0,1.0] || -> . % 0.64/0.81 888[4:Spt:872.0,805.0,808.0] || equal(op1(e11,e11),e10)** -> . % 0.64/0.81 889[4:Spt:872.0,805.1] || -> equal(op1(e10,e11),e10)**. % 0.64/0.81 892[4:Rew:889.0,113.0] || equal(op1(e10,e10),e10)** -> . % 0.64/0.81 901[4:MRR:530.0,892.0] || -> equal(op1(e13,e10),e10)**. % 0.64/0.81 921[4:Rew:901.0,726.1] || -> equal(op1(e13,e11),e12)** equal(e12,e10). % 0.64/0.81 922[4:MRR:921.1,2.0] || -> equal(op1(e13,e11),e12)**. % 0.64/0.81 925[4:Rew:922.0,715.0] || -> equal(op1(e11,e12),e11)**. % 0.64/0.81 930[4:Rew:925.0,122.0] || equal(op1(e11,e11),e11)** -> . % 0.64/0.81 940[4:Rew:889.0,519.2,922.0,519.1] || -> equal(op1(e11,e11),e11)** equal(e12,e11) equal(e11,e10). % 0.64/0.81 941[4:MRR:940.0,940.1,940.2,930.0,4.0,1.0] || -> . % 0.64/0.81 950[2:Spt:941.0,319.0,652.0] || equal(op1(e10,e13),e13)** -> . % 0.64/0.81 951[2:Spt:941.0,319.1,319.2,319.3] || -> equal(op1(e10,e13),e10) equal(op1(e10,e13),e12)** equal(op1(e10,e13),e11). % 0.64/0.81 954[3:Spt:951.0] || -> equal(op1(e10,e13),e10)**. % 0.64/0.81 956[3:Rew:954.0,107.0] || equal(op1(e11,e13),e10)** -> . % 0.64/0.81 959[3:Rew:954.0,115.0] || equal(op1(e10,e10),e10)** -> . % 0.64/0.81 962[3:Rew:954.0,192.1] || SkC0 -> equal(op1(e13,e10),e13)**. % 0.64/0.81 973[3:MRR:524.1,956.0] || -> equal(op1(e11,e11),e10)**. % 0.64/0.81 981[3:Rew:973.0,194.1] || SkC1 -> equal(op1(e11,e10),e11)**. % 0.64/0.81 988[3:MRR:530.0,959.0] || -> equal(op1(e13,e10),e10)**. % 0.64/0.81 989[3:MRR:540.0,959.0] || -> equal(op1(e10,e10),e12)**. % 0.64/0.81 996[3:Rew:988.0,419.2] || -> SkC1 SkC0 equal(op1(e10,e10),e10)**. % 0.64/0.81 1010[3:Rew:988.0,962.1] || SkC0* -> equal(e13,e10). % 0.64/0.81 1011[3:MRR:1010.1,3.0] || SkC0* -> . % 0.64/0.81 1015[3:Rew:428.0,981.1] || SkC1* -> equal(e13,e11). % 0.64/0.81 1016[3:MRR:1015.1,5.0] || SkC1* -> . % 0.64/0.81 1017[3:Rew:989.0,996.2] || -> SkC1 SkC0* equal(e12,e10). % 0.64/0.81 1018[3:MRR:1017.0,1017.1,1017.2,1016.0,1011.0,2.0] || -> . % 0.64/0.81 1042[3:Spt:1018.0,951.0,954.0] || equal(op1(e10,e13),e10)** -> . % 0.64/0.81 1043[3:Spt:1018.0,951.1,951.2] || -> equal(op1(e10,e13),e12)** equal(op1(e10,e13),e11). % 0.64/0.81 1177[4:Spt:496.0] || -> equal(h2(e10),e22)**. % 0.64/0.81 1180[4:Rew:1177.0,476.0] || -> equal(e22,e20) equal(op2(e21,e23),e20)**. % 0.64/0.81 1185[4:Rew:1177.0,84.0] || -> equal(op2(e21,e21),e22)**. % 0.64/0.81 1186[4:Rew:1177.0,364.0] || -> equal(op2(e21,e22),h2(e11))**. % 0.64/0.81 1188[4:Rew:1177.0,375.0] || equal(op2(e21,e22),e22)** -> . % 0.64/0.81 1190[4:Rew:1177.0,388.0] || equal(op2(e20,e21),e22)** -> . % 0.64/0.81 1195[4:Rew:1186.0,642.1] || -> equal(op2(e23,e22),e22)** equal(h2(e11),e22). % 0.64/0.81 1203[4:Rew:1186.0,1188.0] || equal(h2(e11),e22)** -> . % 0.64/0.81 1207[4:MRR:646.1,1190.0] || -> equal(h1(e10),e22)**. % 0.64/0.81 1214[4:Rew:1207.0,365.0] || -> equal(op2(e20,e22),h1(e11))**. % 0.64/0.81 1218[4:Rew:1207.0,439.0] || -> equal(op2(h1(e11),e22),h1(e13))**. % 0.64/0.81 1222[4:Rew:599.0,1214.0] || -> equal(h1(e11),e23)**. % 0.64/0.81 1224[4:Rew:1222.0,408.1] || SkC3* -> equal(e23,e20). % 0.64/0.81 1225[4:MRR:1224.1,9.0] || SkC3* -> . % 0.64/0.81 1227[4:MRR:414.1,1225.0] || -> SkC4 equal(op2(e21,op2(e23,e21)),e21)**. % 0.64/0.81 1235[4:Rew:1222.0,1218.0] || -> equal(op2(e23,e22),h1(e13))**. % 0.64/0.81 1240[4:Rew:1235.0,638.1] || -> equal(op2(e23,e21),e21)** equal(h1(e13),e21). % 0.64/0.81 1242[4:MRR:1180.0,8.0] || -> equal(op2(e21,e23),e20)**. % 0.64/0.81 1245[4:Rew:1242.0,155.0] || equal(op2(e20,e23),e20)** -> . % 0.64/0.81 1249[4:MRR:427.1,1245.0] || SkC4* -> . % 0.64/0.81 1257[4:MRR:1227.0,1249.0] || -> equal(op2(e21,op2(e23,e21)),e21)**. % 0.64/0.81 1260[4:Rew:1235.0,1195.0] || -> equal(h1(e13),e22) equal(h2(e11),e22)**. % 0.64/0.81 1261[4:MRR:1260.1,1203.0] || -> equal(h1(e13),e22)**. % 0.64/0.81 1280[4:Rew:1261.0,1240.1] || -> equal(op2(e23,e21),e21)** equal(e22,e21). % 0.64/0.81 1281[4:MRR:1280.1,10.0] || -> equal(op2(e23,e21),e21)**. % 0.64/0.81 1286[4:Rew:1281.0,1257.0] || -> equal(op2(e21,e21),e21)**. % 0.64/0.81 1287[4:Rew:1185.0,1286.0] || -> equal(e22,e21)**. % 0.64/0.81 1288[4:MRR:1287.0,10.0] || -> . % 0.64/0.81 1301[4:Spt:1288.0,496.0,1177.0] || equal(h2(e10),e22)** -> . % 0.64/0.81 1302[4:Spt:1288.0,496.1,496.2] || -> equal(h2(e10),e21)** equal(h2(e10),e20). % 0.64/0.81 1303[4:MRR:632.0,1301.0] || -> equal(op2(e21,e22),e22)**. % 0.64/0.81 1309[4:Rew:34.0,207.1,1303.0,207.1] || SkC4* -> equal(e22,e20). % 0.64/0.81 1310[4:MRR:1309.1,8.0] || SkC4* -> . % 0.64/0.81 1313[4:MRR:413.0,1310.0] || -> SkC3 equal(op2(e22,op2(e23,e22)),e22)**. % 0.64/0.81 1314[4:Rew:1303.0,644.0] || -> equal(e22,e21) equal(op2(e23,e22),e21)**. % 0.64/0.81 1315[4:MRR:1314.0,10.0] || -> equal(op2(e23,e22),e21)**. % 0.64/0.81 1319[4:Rew:1315.0,182.0] || equal(op2(e23,e21),e21)** -> . % 0.64/0.81 1321[4:Rew:1315.0,1313.1] || -> SkC3 equal(op2(e22,e21),e22)**. % 0.64/0.81 1322[4:Rew:614.0,1321.1] || -> SkC3* equal(e23,e22). % 0.64/0.81 1323[4:MRR:1322.1,12.0] || -> SkC3*. % 0.64/0.81 1325[4:MRR:204.0,1323.0] || -> equal(op2(e23,op2(e20,e23)),e23)**. % 0.64/0.81 1335[4:MRR:470.1,1319.0] || -> equal(h2(e10),e21) equal(op2(e20,e21),e21)**. % 0.64/0.81 1345[5:Spt:1302.0] || -> equal(h2(e10),e21)**. % 0.64/0.81 1352[5:Rew:1345.0,388.0] || equal(op2(e20,e21),e21)** -> . % 0.64/0.81 1359[5:MRR:643.0,1352.0] || -> equal(op2(e20,e23),e21)**. % 0.64/0.81 1366[5:Rew:1359.0,1325.0] || -> equal(op2(e23,e21),e23)**. % 0.64/0.81 1369[5:MRR:1366.0,587.0] || -> . % 0.64/0.81 1387[5:Spt:1369.0,1302.0,1345.0] || equal(h2(e10),e21)** -> . % 0.64/0.81 1388[5:Spt:1369.0,1302.1] || -> equal(h2(e10),e20)**. % 0.64/0.81 1398[5:Rew:1388.0,386.0] || equal(op2(e23,e21),e20)** -> . % 0.64/0.81 1399[5:MRR:640.1,1398.0] || -> equal(op2(e23,e20),e20)**. % 0.64/0.81 1427[5:Rew:1388.0,1335.0] || -> equal(e21,e20) equal(op2(e20,e21),e21)**. % 0.64/0.81 1428[5:MRR:1427.0,7.0] || -> equal(op2(e20,e21),e21)**. % 0.64/0.81 1433[5:Rew:1428.0,165.0] || equal(op2(e20,e23),e21)** -> . % 0.64/0.81 1442[5:MRR:645.1,1433.0] || -> equal(op2(e20,e23),e20)**. % 0.64/0.81 1445[5:Rew:1442.0,1325.0] || -> equal(op2(e23,e20),e23)**. % 0.64/0.81 1447[5:Rew:1399.0,1445.0] || -> equal(e23,e20)**. % 0.64/0.81 1448[5:MRR:1447.0,9.0] || -> . % 0.64/0.81 1453[1:Spt:1448.0,488.0,574.0] || equal(h4(e10),e23)** -> . % 0.64/0.81 1454[1:Spt:1448.0,488.1,488.2,488.3] || -> equal(h4(e10),e22)** equal(h4(e10),e21) equal(h4(e10),e20). % 0.64/0.81 1455[1:MRR:441.0,1453.0] || -> equal(op2(e22,e23),e23)** equal(op2(e20,e23),e23). % 0.64/0.81 1456[1:MRR:443.0,1453.0] || -> equal(op2(e23,e22),e23)** equal(op2(e23,e21),e23). % 0.64/0.81 1457[2:Spt:1454.0] || -> equal(h4(e10),e22)**. % 0.64/0.81 1468[2:Rew:1457.0,381.0] || equal(op2(e21,e23),e22)** -> . % 0.64/0.81 1470[2:Rew:1457.0,368.0] || equal(op2(e23,e20),e22)** -> . % 0.64/0.81 1480[2:MRR:468.2,1468.0] || -> equal(h2(e10),e22) equal(op2(e21,e22),e22)**. % 0.64/0.81 1497[2:MRR:480.1,1470.0] || -> equal(h1(e10),e22)**. % 0.64/0.81 1498[2:MRR:490.1,1470.0] || -> equal(op2(e23,e20),e20)**. % 0.64/0.81 1502[2:Rew:1497.0,83.0] || -> equal(op2(e20,e20),e22)**. % 0.64/0.81 1506[2:Rew:1497.0,365.0] || -> equal(op2(e20,e22),h1(e11))**. % 0.64/0.81 1517[2:Rew:1498.0,415.2] || -> SkC4 SkC3 equal(op2(e20,e20),e20)**. % 0.64/0.81 1536[2:Rew:1506.0,385.0] || equal(h1(e11),e20)** -> . % 0.64/0.81 1543[2:MRR:408.1,1536.0] || SkC3* -> . % 0.64/0.81 1549[2:Rew:1502.0,1517.2] || -> SkC4 SkC3* equal(e22,e20). % 0.64/0.81 1550[2:MRR:1549.1,1549.2,1543.0,8.0] || -> SkC4*. % 0.64/0.81 1552[2:MRR:427.0,1550.0] || -> equal(op2(e20,e23),e20)**. % 0.64/0.81 1553[2:MRR:207.0,1550.0] || -> equal(op2(e22,op2(e21,e22)),e22)**. % 0.64/0.81 1562[2:Rew:1552.0,155.0] || equal(op2(e21,e23),e20)** -> . % 0.64/0.81 1565[2:MRR:476.1,1562.0] || -> equal(h2(e10),e20)**. % 0.64/0.81 1584[2:Rew:1565.0,1480.0] || -> equal(e22,e20) equal(op2(e21,e22),e22)**. % 0.64/0.81 1585[2:MRR:1584.0,8.0] || -> equal(op2(e21,e22),e22)**. % 0.64/0.81 1591[2:Rew:1585.0,1553.0] || -> equal(op2(e22,e22),e22)**. % 0.64/0.81 1592[2:Rew:34.0,1591.0] || -> equal(e22,e20)**. % 0.64/0.81 1593[2:MRR:1592.0,8.0] || -> . % 0.64/0.81 1649[2:Spt:1593.0,1454.0,1457.0] || equal(h4(e10),e22)** -> . % 0.64/0.81 1650[2:Spt:1593.0,1454.1,1454.2] || -> equal(h4(e10),e21)** equal(h4(e10),e20). % 0.64/0.81 1653[3:Spt:1650.0] || -> equal(h4(e10),e21)**. % 0.64/0.81 1661[3:Rew:1653.0,360.0] || -> equal(op2(e23,e21),h4(e11))**. % 0.64/0.81 1662[3:Rew:1653.0,366.0] || equal(op2(e23,e22),e21)** -> . % 0.64/0.81 1663[3:Rew:1653.0,367.0] || equal(op2(e23,e21),e21)** -> . % 0.64/0.81 1666[3:Rew:1653.0,381.0] || equal(op2(e21,e23),e21)** -> . % 0.64/0.81 1667[3:Rew:1653.0,382.0] || equal(op2(e20,e23),e21)** -> . % 0.64/0.81 1668[3:Rew:1653.0,436.0] || -> equal(op2(h4(e11),e21),h4(e13))**. % 0.64/0.81 1672[3:Rew:1661.0,386.0] || equal(h4(e11),h2(e10))** -> . % 0.64/0.81 1673[3:Rew:1661.0,148.0] || equal(op2(e22,e21),h4(e11))** -> . % 0.64/0.81 1675[3:Rew:1661.0,182.0] || equal(op2(e23,e22),h4(e11))** -> . % 0.64/0.81 1677[3:Rew:1661.0,414.2] || -> SkC4 SkC3 equal(op2(e21,h4(e11)),e21)**. % 0.64/0.81 1678[3:Rew:1661.0,261.0] || -> equal(h4(e11),e23) equal(op2(e23,e21),e21) equal(op2(e23,e21),e22)** equal(op2(e23,e21),e20). % 0.64/0.81 1679[3:Rew:1661.0,465.0] || -> equal(h4(e11),e23) equal(op2(e22,e21),e23)** equal(op2(e20,e21),e23). % 0.64/0.81 1680[3:Rew:1661.0,1456.1] || -> equal(op2(e23,e22),e23)** equal(h4(e11),e23). % 0.64/0.81 1681[3:Rew:1661.0,470.1] || -> equal(h2(e10),e21) equal(h4(e11),e21) equal(op2(e20,e21),e21)**. % 0.64/0.81 1685[3:MRR:489.2,1662.0] || -> equal(op2(e23,e22),e23)** equal(op2(e23,e22),e22). % 0.64/0.81 1687[3:Rew:1661.0,1663.0] || equal(h4(e11),e21)** -> . % 0.64/0.81 1688[3:MRR:472.1,1666.0] || -> equal(h2(e10),e21) equal(op2(e21,e22),e21)**. % 0.64/0.81 1689[3:MRR:493.0,1666.0] || -> equal(op2(e21,e23),e22)** equal(op2(e21,e23),e20). % 0.64/0.81 1690[3:MRR:483.1,1667.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e22),e21)**. % 0.64/0.81 1692[3:Rew:412.2,1677.2] || -> SkC4 SkC3 equal(op2(e21,e23),e21)**. % 0.64/0.81 1693[3:MRR:1692.2,1666.0] || -> SkC4 SkC3*. % 0.64/0.81 1697[3:MRR:1681.1,1687.0] || -> equal(h2(e10),e21) equal(op2(e20,e21),e21)**. % 0.64/0.81 1698[3:Rew:1661.0,1678.3,1661.0,1678.2,1661.0,1678.1] || -> equal(h4(e11),e23)** equal(h4(e11),e21) equal(h4(e11),e22) equal(h4(e11),e20). % 0.64/0.81 1699[3:MRR:1698.1,1687.0] || -> equal(h4(e11),e23)** equal(h4(e11),e22) equal(h4(e11),e20). % 0.64/0.81 1704[4:Spt:319.0] || -> equal(op1(e10,e13),e13)**. % 0.64/0.81 1705[4:Rew:1704.0,531.1] || -> equal(op1(e10,e10),e10) equal(e13,e10) equal(op1(e10,e11),e10)**. % 0.64/0.81 1707[4:Rew:1704.0,435.1] || SkC1* -> equal(e13,e10). % 0.64/0.81 1709[4:Rew:1704.0,108.0] || equal(op1(e12,e13),e13)** -> . % 0.64/0.81 1710[4:Rew:1704.0,109.0] || equal(op1(e13,e13),e13)** -> . % 0.64/0.81 1713[4:Rew:1704.0,118.0] || equal(op1(e10,e12),e13)** -> . % 0.64/0.81 1714[4:Rew:1704.0,192.1] || SkC0 -> equal(op1(e13,e13),e13)**. % 0.64/0.81 1725[4:MRR:1707.1,3.0] || SkC1* -> . % 0.64/0.81 1727[4:MRR:416.0,1725.0] || -> SkC0 equal(op1(e13,op1(e13,e13)),e13)**. % 0.64/0.81 1729[4:MRR:418.0,1725.0] || -> SkC0 equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.81 1730[4:MRR:534.0,1709.0] || -> equal(op1(e12,e13),e12)**. % 0.64/0.81 1731[4:MRR:509.0,1709.0] || -> equal(op1(e12,e11),e13)**. % 0.64/0.81 1734[4:Rew:1730.0,112.0] || equal(op1(e13,e13),e12)** -> . % 0.64/0.81 1741[4:Rew:1731.0,100.0] || equal(op1(e13,e11),e13)** -> . % 0.64/0.81 1745[4:MRR:307.0,1710.0] || -> equal(op1(e13,e13),e12)** equal(op1(e13,e13),e11) equal(op1(e13,e13),e10). % 0.64/0.81 1747[4:MRR:507.1,1713.0] || -> equal(op1(e13,e12),e13)**. % 0.64/0.81 1755[4:Rew:1747.0,278.1] || -> equal(op1(e13,e13),e12)** equal(e13,e12) equal(op1(e13,e11),e12) equal(op1(e13,e10),e12). % 0.64/0.81 1762[4:MRR:309.0,1741.0] || -> equal(op1(e13,e11),e11) equal(op1(e13,e11),e12)** equal(op1(e13,e11),e10). % 0.64/0.81 1763[4:MRR:1714.1,1710.0] || SkC0* -> . % 0.64/0.81 1765[4:MRR:1727.0,1763.0] || -> equal(op1(e13,op1(e13,e13)),e13)**. % 0.64/0.81 1767[4:MRR:1729.0,1763.0] || -> equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.81 1768[4:MRR:1705.1,3.0] || -> equal(op1(e10,e10),e10) equal(op1(e10,e11),e10)**. % 0.64/0.81 1775[4:MRR:1745.0,1734.0] || -> equal(op1(e13,e13),e11)** equal(op1(e13,e13),e10). % 0.64/0.81 1778[4:MRR:1755.0,1755.1,1734.0,6.0] || -> equal(op1(e13,e11),e12)** equal(op1(e13,e10),e12). % 0.64/0.81 1786[5:Spt:522.2] || -> equal(op1(e13,e11),e10)**. % 0.64/0.81 1789[5:Rew:1786.0,135.0] || equal(op1(e13,e13),e10)** -> . % 0.64/0.81 1822[5:MRR:1775.1,1789.0] || -> equal(op1(e13,e13),e11)**. % 0.64/0.81 1832[5:Rew:1822.0,1765.0] || -> equal(op1(e13,e11),e13)**. % 0.64/0.81 1834[5:Rew:1786.0,1832.0] || -> equal(e13,e10)**. % 0.64/0.81 1835[5:MRR:1834.0,3.0] || -> . % 0.64/0.81 1853[5:Spt:1835.0,522.2,1786.0] || equal(op1(e13,e11),e10)** -> . % 0.64/0.81 1854[5:Spt:1835.0,522.0,522.1] || -> equal(op1(e11,e11),e10)** equal(op1(e10,e11),e10). % 0.64/0.81 1856[5:MRR:1762.2,1853.0] || -> equal(op1(e13,e11),e11) equal(op1(e13,e11),e12)**. % 0.64/0.81 1857[6:Spt:1854.0] || -> equal(op1(e11,e11),e10)**. % 0.64/0.81 1859[6:Rew:1857.0,95.0] || equal(op1(e10,e11),e10)** -> . % 0.64/0.81 1873[6:MRR:1768.1,1859.0] || -> equal(op1(e10,e10),e10)**. % 0.64/0.81 1877[6:Rew:1873.0,91.0] || equal(op1(e13,e10),e10)** -> . % 0.64/0.81 1897[6:MRR:533.0,1877.0] || -> equal(op1(e13,e10),e12)**. % 0.64/0.81 1901[6:Rew:1897.0,131.0] || equal(op1(e13,e11),e12)** -> . % 0.64/0.81 1915[6:MRR:1856.1,1901.0] || -> equal(op1(e13,e11),e11)**. % 0.64/0.81 1918[6:Rew:1915.0,1767.0] || -> equal(op1(e11,e11),e11)**. % 0.64/0.81 1921[6:Rew:1857.0,1918.0] || -> equal(e11,e10)**. % 0.64/0.81 1922[6:MRR:1921.0,1.0] || -> . % 0.64/0.81 1936[6:Spt:1922.0,1854.0,1857.0] || equal(op1(e11,e11),e10)** -> . % 0.64/0.81 1937[6:Spt:1922.0,1854.1] || -> equal(op1(e10,e11),e10)**. % 0.64/0.81 1940[6:Rew:1937.0,113.0] || equal(op1(e10,e10),e10)** -> . % 0.64/0.81 1949[6:MRR:530.0,1940.0] || -> equal(op1(e13,e10),e10)**. % 0.64/0.81 1969[6:Rew:1949.0,1778.1] || -> equal(op1(e13,e11),e12)** equal(e12,e10). % 0.64/0.81 1970[6:MRR:1969.1,2.0] || -> equal(op1(e13,e11),e12)**. % 0.64/0.81 1973[6:Rew:1970.0,1767.0] || -> equal(op1(e11,e12),e11)**. % 0.64/0.81 1978[6:Rew:1973.0,122.0] || equal(op1(e11,e11),e11)** -> . % 0.64/0.81 1988[6:Rew:1937.0,519.2,1970.0,519.1] || -> equal(op1(e11,e11),e11)** equal(e12,e11) equal(e11,e10). % 0.64/0.81 1989[6:MRR:1988.0,1988.1,1988.2,1978.0,4.0,1.0] || -> . % 0.64/0.81 1997[4:Spt:1989.0,319.0,1704.0] || equal(op1(e10,e13),e13)** -> . % 0.64/0.81 1998[4:Spt:1989.0,319.1,319.2,319.3] || -> equal(op1(e10,e13),e10) equal(op1(e10,e13),e12)** equal(op1(e10,e13),e11). % 0.64/0.81 2001[5:Spt:1998.0] || -> equal(op1(e10,e13),e10)**. % 0.64/0.81 2005[5:Rew:2001.0,115.0] || equal(op1(e10,e10),e10)** -> . % 0.64/0.81 2008[5:Rew:2001.0,107.0] || equal(op1(e11,e13),e10)** -> . % 0.64/0.81 2009[5:Rew:2001.0,192.1] || SkC0 -> equal(op1(e13,e10),e13)**. % 0.64/0.81 2022[5:MRR:530.0,2005.0] || -> equal(op1(e13,e10),e10)**. % 0.64/0.81 2023[5:MRR:540.0,2005.0] || -> equal(op1(e10,e10),e12)**. % 0.64/0.81 2030[5:Rew:2022.0,419.2] || -> SkC1 SkC0 equal(op1(e10,e10),e10)**. % 0.64/0.81 2040[5:MRR:524.1,2008.0] || -> equal(op1(e11,e11),e10)**. % 0.64/0.81 2048[5:Rew:2040.0,194.1] || SkC1 -> equal(op1(e11,e10),e11)**. % 0.64/0.81 2057[5:Rew:2022.0,2009.1] || SkC0* -> equal(e13,e10). % 0.64/0.81 2058[5:MRR:2057.1,3.0] || SkC0* -> . % 0.64/0.81 2062[5:Rew:2023.0,2030.2] || -> SkC1 SkC0* equal(e12,e10). % 0.64/0.81 2063[5:MRR:2062.1,2062.2,2058.0,2.0] || -> SkC1*. % 0.64/0.81 2066[5:Rew:428.0,2048.1] || SkC1* -> equal(e13,e11). % 0.64/0.81 2067[5:MRR:2066.0,2066.1,2063.0,5.0] || -> . % 0.64/0.81 2084[5:Spt:2067.0,1998.0,2001.0] || equal(op1(e10,e13),e10)** -> . % 0.64/0.81 2085[5:Spt:2067.0,1998.1,1998.2] || -> equal(op1(e10,e13),e12)** equal(op1(e10,e13),e11). % 0.64/0.81 2216[6:Spt:496.0] || -> equal(h2(e10),e22)**. % 0.64/0.81 2223[6:Rew:2216.0,387.0] || equal(op2(e22,e21),e22)** -> . % 0.64/0.81 2227[6:Rew:2216.0,374.0] || equal(op2(e21,e23),e22)** -> . % 0.64/0.81 2230[6:Rew:2216.0,1697.0] || -> equal(e22,e21) equal(op2(e20,e21),e21)**. % 0.64/0.81 2239[6:MRR:492.0,2223.0] || -> equal(op2(e22,e21),e23)**. % 0.64/0.81 2250[6:Rew:2239.0,1673.0] || equal(h4(e11),e23)** -> . % 0.64/0.81 2252[6:MRR:1680.1,2250.0] || -> equal(op2(e23,e22),e23)**. % 0.64/0.81 2255[6:Rew:2252.0,151.0] || equal(op2(e20,e22),e23)** -> . % 0.64/0.81 2270[6:MRR:1689.0,2227.0] || -> equal(op2(e21,e23),e20)**. % 0.64/0.81 2272[6:Rew:2270.0,155.0] || equal(op2(e20,e23),e20)** -> . % 0.64/0.81 2280[6:MRR:497.1,2255.0] || -> equal(op2(e20,e22),e22)** equal(op2(e20,e22),e21). % 0.64/0.81 2282[6:MRR:427.1,2272.0] || SkC4* -> . % 0.64/0.81 2284[6:MRR:1693.0,2282.0] || -> SkC3*. % 0.64/0.81 2286[6:MRR:203.0,2284.0] || -> equal(op2(e22,op2(e20,e22)),e22)**. % 0.64/0.81 2299[6:MRR:2230.0,10.0] || -> equal(op2(e20,e21),e21)**. % 0.64/0.81 2301[6:Rew:2299.0,164.0] || equal(op2(e20,e22),e21)** -> . % 0.64/0.81 2353[6:MRR:2280.1,2301.0] || -> equal(op2(e20,e22),e22)**. % 0.64/0.81 2356[6:Rew:2353.0,2286.0] || -> equal(op2(e22,e22),e22)**. % 0.64/0.81 2358[6:Rew:34.0,2356.0] || -> equal(e22,e20)**. % 0.64/0.81 2359[6:MRR:2358.0,8.0] || -> . % 0.64/0.81 2368[6:Spt:2359.0,496.0,2216.0] || equal(h2(e10),e22)** -> . % 0.64/0.81 2369[6:Spt:2359.0,496.1,496.2] || -> equal(h2(e10),e21)** equal(h2(e10),e20). % 0.64/0.81 2370[6:MRR:468.0,2368.0] || -> equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.64/0.81 2372[7:Spt:2369.0] || -> equal(h2(e10),e21)**. % 0.64/0.81 2381[7:Rew:2372.0,388.0] || equal(op2(e20,e21),e21)** -> . % 0.64/0.81 2382[7:Rew:2372.0,375.0] || equal(op2(e21,e22),e21)** -> . % 0.64/0.81 2389[7:MRR:1690.0,2381.0] || -> equal(op2(e20,e22),e21)**. % 0.64/0.81 2397[7:Rew:2389.0,203.1] || SkC3 -> equal(op2(e22,e21),e22)**. % 0.64/0.81 2402[7:MRR:494.1,2382.0] || -> equal(op2(e21,e22),e22)**. % 0.64/0.81 2405[7:Rew:2402.0,153.0] || equal(op2(e23,e22),e22)** -> . % 0.64/0.81 2406[7:Rew:2402.0,172.0] || equal(op2(e21,e23),e22)** -> . % 0.64/0.81 2413[7:MRR:1685.1,2405.0] || -> equal(op2(e23,e22),e23)**. % 0.64/0.81 2417[7:Rew:2413.0,1675.0] || equal(h4(e11),e23)** -> . % 0.64/0.81 2420[7:MRR:1699.0,2417.0] || -> equal(h4(e11),e22)** equal(h4(e11),e20). % 0.64/0.81 2421[7:MRR:1679.0,2417.0] || -> equal(op2(e22,e21),e23)** equal(op2(e20,e21),e23). % 0.64/0.81 2422[7:MRR:1689.0,2406.0] || -> equal(op2(e21,e23),e20)**. % 0.64/0.81 2427[7:Rew:2422.0,155.0] || equal(op2(e20,e23),e20)** -> . % 0.64/0.81 2430[7:MRR:427.1,2427.0] || SkC4* -> . % 0.64/0.81 2433[7:MRR:1693.0,2430.0] || -> SkC3*. % 0.64/0.81 2436[7:MRR:202.0,2433.0] || -> equal(op2(e21,op2(e20,e21)),e21)**. % 0.64/0.81 2446[7:MRR:2397.0,2433.0] || -> equal(op2(e22,e21),e22)**. % 0.64/0.81 2449[7:Rew:2446.0,1673.0] || equal(h4(e11),e22)** -> . % 0.64/0.81 2461[7:MRR:2420.0,2449.0] || -> equal(h4(e11),e20)**. % 0.64/0.81 2467[7:Rew:2461.0,1668.0] || -> equal(op2(e20,e21),h4(e13))**. % 0.64/0.81 2488[7:Rew:2467.0,2436.0] || -> equal(op2(e21,h4(e13)),e21)**. % 0.64/0.81 2492[7:Rew:2467.0,2421.1,2446.0,2421.0] || -> equal(e23,e22) equal(h4(e13),e23)**. % 0.64/0.81 2493[7:MRR:2492.0,12.0] || -> equal(h4(e13),e23)**. % 0.64/0.81 2498[7:Rew:2493.0,2488.0] || -> equal(op2(e21,e23),e21)**. % 0.64/0.81 2500[7:Rew:2422.0,2498.0] || -> equal(e21,e20)**. % 0.64/0.81 2501[7:MRR:2500.0,7.0] || -> . % 0.64/0.81 2517[7:Spt:2501.0,2369.0,2372.0] || equal(h2(e10),e21)** -> . % 0.64/0.81 2518[7:Spt:2501.0,2369.1] || -> equal(h2(e10),e20)**. % 0.64/0.81 2525[7:Rew:2518.0,1672.0] || equal(h4(e11),e20)** -> . % 0.64/0.81 2527[7:Rew:420.0,364.0,2518.0,364.0] || -> equal(h2(e11),e23)**. % 0.64/0.81 2528[7:Rew:2527.0,407.1] || SkC4* -> equal(e23,e21). % 0.64/0.81 2530[7:MRR:2528.1,11.0] || SkC4* -> . % 0.64/0.81 2531[7:MRR:1693.0,2530.0] || -> SkC3*. % 0.64/0.81 2548[7:Rew:2518.0,1688.0] || -> equal(e21,e20) equal(op2(e21,e22),e21)**. % 0.64/0.81 2549[7:MRR:2548.0,7.0] || -> equal(op2(e21,e22),e21)**. % 0.64/0.81 2563[7:MRR:203.0,2531.0] || -> equal(op2(e22,op2(e20,e22)),e22)**. % 0.64/0.81 2587[7:Rew:2549.0,2370.0] || -> equal(e22,e21) equal(op2(e21,e23),e22)**. % 0.64/0.81 2588[7:MRR:2587.0,10.0] || -> equal(op2(e21,e23),e22)**. % 0.64/0.81 2593[7:Rew:2588.0,158.0] || equal(op2(e22,e23),e22)** -> . % 0.64/0.81 2603[7:MRR:461.0,2593.0] || -> equal(op2(e22,e21),e22)**. % 0.64/0.81 2606[7:Rew:2603.0,1673.0] || equal(h4(e11),e22)** -> . % 0.64/0.81 2608[7:Rew:2603.0,457.1] || -> equal(op2(e22,e23),e23)** equal(e23,e22). % 0.64/0.81 2609[7:MRR:2608.1,12.0] || -> equal(op2(e22,e23),e23)**. % 0.64/0.81 2613[7:MRR:1699.1,1699.2,2606.0,2525.0] || -> equal(h4(e11),e23)**. % 0.64/0.81 2617[7:Rew:2613.0,1675.0] || equal(op2(e23,e22),e23)** -> . % 0.64/0.81 2620[7:MRR:455.0,2617.0] || -> equal(op2(e20,e22),e23)**. % 0.64/0.81 2625[7:Rew:2620.0,2563.0] || -> equal(op2(e22,e23),e22)**. % 0.64/0.81 2630[7:Rew:2609.0,2625.0] || -> equal(e23,e22)**. % 0.64/0.81 2631[7:MRR:2630.0,12.0] || -> . % 0.64/0.81 2646[3:Spt:2631.0,1650.0,1653.0] || equal(h4(e10),e21)** -> . % 0.64/0.81 2647[3:Spt:2631.0,1650.1] || -> equal(h4(e10),e20)**. % 0.64/0.81 2655[3:Rew:2647.0,382.0] || equal(op2(e20,e23),e20)** -> . % 0.64/0.81 2656[3:MRR:427.1,2655.0] || SkC4* -> . % 0.64/0.81 2657[3:MRR:412.0,2656.0] || -> SkC3 equal(h4(e11),e23)**. % 0.64/0.81 2658[3:Rew:2647.0,381.0] || equal(op2(e21,e23),e20)** -> . % 0.64/0.81 2660[3:Rew:2647.0,368.0] || equal(op2(e23,e20),e20)** -> . % 0.64/0.81 2661[3:Rew:2647.0,367.0] || equal(op2(e23,e21),e20)** -> . % 0.64/0.81 2663[3:Rew:2647.0,360.0] || -> equal(op2(e23,e20),h4(e11))**. % 0.64/0.81 2665[3:Rew:2663.0,424.0] || equal(h4(e11),e23)** -> . % 0.64/0.81 2667[3:Rew:2663.0,2660.0] || equal(h4(e11),e20)** -> . % 0.64/0.81 2668[3:MRR:2657.1,2665.0] || -> SkC3*. % 0.64/0.81 2673[3:Rew:2663.0,180.0] || equal(op2(e23,e22),h4(e11))** -> . % 0.64/0.81 2678[3:Rew:2663.0,179.0] || equal(op2(e23,e21),h4(e11))** -> . % 0.64/0.81 2679[3:MRR:476.1,2658.0] || -> equal(h2(e10),e20)**. % 0.64/0.81 2685[3:Rew:2679.0,364.0] || -> equal(op2(e21,e20),h2(e11))**. % 0.64/0.81 2687[3:Rew:2679.0,388.0] || equal(op2(e20,e21),e20)** -> . % 0.64/0.81 2690[3:Rew:2679.0,438.0] || -> equal(op2(h2(e11),e20),h2(e13))**. % 0.64/0.81 2692[3:Rew:420.0,2685.0] || -> equal(h2(e11),e23)**. % 0.64/0.81 2694[3:Rew:2663.0,2690.0,2692.0,2690.0] || -> equal(h4(e11),h2(e13))**. % 0.64/0.81 2696[3:Rew:2694.0,2663.0] || -> equal(op2(e23,e20),h2(e13))**. % 0.64/0.81 2699[3:Rew:2694.0,2667.0] || equal(h2(e13),e20)** -> . % 0.64/0.81 2701[3:Rew:2694.0,2673.0] || equal(op2(e23,e22),h2(e13))** -> . % 0.64/0.81 2703[3:Rew:2694.0,2678.0] || equal(op2(e23,e21),h2(e13))** -> . % 0.64/0.81 2704[3:MRR:203.0,2668.0] || -> equal(op2(e22,op2(e20,e22)),e22)**. % 0.64/0.81 2705[3:MRR:202.0,2668.0] || -> equal(op2(e21,op2(e20,e21)),e21)**. % 0.64/0.81 2706[3:MRR:204.0,2668.0] || -> equal(op2(e23,op2(e20,e23)),e23)**. % 0.64/0.81 2707[3:Rew:2696.0,485.1] || -> equal(h1(e10),e20) equal(h2(e13),e20)**. % 0.64/0.81 2708[3:MRR:2707.1,2699.0] || -> equal(h1(e10),e20)**. % 0.64/0.81 2718[3:Rew:2696.0,480.1,2708.0,480.0] || -> equal(e22,e20) equal(h2(e13),e22)**. % 0.64/0.81 2719[3:MRR:2718.0,8.0] || -> equal(h2(e13),e22)**. % 0.64/0.81 2726[3:Rew:2719.0,2696.0] || -> equal(op2(e23,e20),e22)**. % 0.64/0.81 2727[3:Rew:2719.0,2701.0] || equal(op2(e23,e22),e22)** -> . % 0.64/0.81 2729[3:Rew:2719.0,2703.0] || equal(op2(e23,e21),e22)** -> . % 0.64/0.81 2735[3:Rew:2679.0,468.0] || -> equal(e22,e20) equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.64/0.81 2736[3:MRR:2735.0,8.0] || -> equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.64/0.81 2746[3:MRR:489.1,2727.0] || -> equal(op2(e23,e22),e23)** equal(op2(e23,e22),e21). % 0.64/0.81 2748[3:Rew:2708.0,481.0] || -> equal(e22,e20) equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)** equal(op2(e20,e21),e22). % 0.64/0.81 2749[3:MRR:2748.0,8.0] || -> equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)** equal(op2(e20,e21),e22). % 0.64/0.81 2752[3:MRR:271.1,2655.0] || -> equal(op2(e20,e23),e23)** equal(op2(e20,e23),e22) equal(op2(e20,e23),e21). % 0.64/0.81 2753[3:MRR:261.2,261.3,2729.0,2661.0] || -> equal(op2(e23,e21),e23)** equal(op2(e23,e21),e21). % 0.64/0.81 2754[3:MRR:273.1,2687.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e21),e23)** equal(op2(e20,e21),e22). % 0.64/0.81 2755[3:Rew:2726.0,551.5,2679.0,551.2,2647.0,551.1,2708.0,551.0] || equal(h3(op1(e10,e10)),e20) equal(h3(op1(e13,e13)),e20)** equal(h3(op1(e11,e11)),e20) equal(h3(op1(e13,e12)),op2(e23,e22)) equal(h3(op1(e13,e11)),op2(e23,e21)) equal(h3(op1(e13,e10)),e22) equal(h3(op1(e12,e13)),op2(e22,e23)) equal(h3(op1(e12,e11)),op2(e22,e21)) equal(h3(op1(e11,e13)),op2(e21,e23)) equal(h3(op1(e11,e12)),op2(e21,e22)) equal(h3(op1(e10,e13)),op2(e20,e23)) equal(h3(op1(e10,e12)),op2(e20,e22)) equal(h3(op1(e10,e11)),op2(e20,e21)) -> . % 0.64/0.81 2765[4:Spt:319.0] || -> equal(op1(e10,e13),e13)**. % 0.64/0.81 2766[4:Rew:2765.0,531.1] || -> equal(op1(e10,e10),e10) equal(e13,e10) equal(op1(e10,e11),e10)**. % 0.64/0.81 2768[4:Rew:2765.0,435.1] || SkC1* -> equal(e13,e10). % 0.64/0.81 2769[4:Rew:2765.0,118.0] || equal(op1(e10,e12),e13)** -> . % 0.64/0.81 2772[4:Rew:2765.0,109.0] || equal(op1(e13,e13),e13)** -> . % 0.64/0.81 2773[4:Rew:2765.0,108.0] || equal(op1(e12,e13),e13)** -> . % 0.64/0.81 2775[4:Rew:2765.0,192.1] || SkC0 -> equal(op1(e13,e13),e13)**. % 0.64/0.81 2783[4:MRR:2768.1,3.0] || SkC1* -> . % 0.64/0.81 2785[4:MRR:416.0,2783.0] || -> SkC0 equal(op1(e13,op1(e13,e13)),e13)**. % 0.64/0.81 2787[4:MRR:418.0,2783.0] || -> SkC0 equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.81 2788[4:MRR:507.1,2769.0] || -> equal(op1(e13,e12),e13)**. % 0.64/0.81 2793[4:Rew:2788.0,134.0] || equal(op1(e13,e11),e13)** -> . % 0.64/0.81 2796[4:Rew:2788.0,278.1] || -> equal(op1(e13,e13),e12)** equal(e13,e12) equal(op1(e13,e11),e12) equal(op1(e13,e10),e12). % 0.64/0.81 2802[4:MRR:307.0,2772.0] || -> equal(op1(e13,e13),e12)** equal(op1(e13,e13),e11) equal(op1(e13,e13),e10). % 0.64/0.81 2803[4:MRR:534.0,2773.0] || -> equal(op1(e12,e13),e12)**. % 0.64/0.81 2807[4:Rew:2803.0,112.0] || equal(op1(e13,e13),e12)** -> . % 0.64/0.81 2817[4:MRR:309.0,2793.0] || -> equal(op1(e13,e11),e11) equal(op1(e13,e11),e12)** equal(op1(e13,e11),e10). % 0.64/0.81 2821[4:MRR:2775.1,2772.0] || SkC0* -> . % 0.64/0.81 2823[4:MRR:2785.0,2821.0] || -> equal(op1(e13,op1(e13,e13)),e13)**. % 0.64/0.81 2825[4:MRR:2787.0,2821.0] || -> equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.81 2826[4:MRR:2766.1,3.0] || -> equal(op1(e10,e10),e10) equal(op1(e10,e11),e10)**. % 0.64/0.81 2833[4:MRR:2802.0,2807.0] || -> equal(op1(e13,e13),e11)** equal(op1(e13,e13),e10). % 0.64/0.81 2835[4:MRR:2796.0,2796.1,2807.0,6.0] || -> equal(op1(e13,e11),e12)** equal(op1(e13,e10),e12). % 0.64/0.81 2841[5:Spt:522.2] || -> equal(op1(e13,e11),e10)**. % 0.64/0.81 2844[5:Rew:2841.0,135.0] || equal(op1(e13,e13),e10)** -> . % 0.64/0.81 2874[5:MRR:2833.1,2844.0] || -> equal(op1(e13,e13),e11)**. % 0.64/0.81 2884[5:Rew:2874.0,2823.0] || -> equal(op1(e13,e11),e13)**. % 0.64/0.81 2886[5:Rew:2841.0,2884.0] || -> equal(e13,e10)**. % 0.64/0.81 2887[5:MRR:2886.0,3.0] || -> . % 0.64/0.81 2901[5:Spt:2887.0,522.2,2841.0] || equal(op1(e13,e11),e10)** -> . % 0.64/0.81 2902[5:Spt:2887.0,522.0,522.1] || -> equal(op1(e11,e11),e10)** equal(op1(e10,e11),e10). % 0.64/0.81 2904[5:MRR:2817.2,2901.0] || -> equal(op1(e13,e11),e11) equal(op1(e13,e11),e12)**. % 0.64/0.81 2905[6:Spt:2902.0] || -> equal(op1(e11,e11),e10)**. % 0.64/0.81 2907[6:Rew:2905.0,95.0] || equal(op1(e10,e11),e10)** -> . % 0.64/0.81 2918[6:MRR:2826.1,2907.0] || -> equal(op1(e10,e10),e10)**. % 0.64/0.81 2922[6:Rew:2918.0,91.0] || equal(op1(e13,e10),e10)** -> . % 0.64/0.81 2942[6:MRR:533.0,2922.0] || -> equal(op1(e13,e10),e12)**. % 0.64/0.81 2946[6:Rew:2942.0,131.0] || equal(op1(e13,e11),e12)** -> . % 0.64/0.81 2960[6:MRR:2904.1,2946.0] || -> equal(op1(e13,e11),e11)**. % 0.64/0.81 2963[6:Rew:2960.0,2825.0] || -> equal(op1(e11,e11),e11)**. % 0.64/0.81 2966[6:Rew:2905.0,2963.0] || -> equal(e11,e10)**. % 0.64/0.81 2967[6:MRR:2966.0,1.0] || -> . % 0.64/0.81 2983[6:Spt:2967.0,2902.0,2905.0] || equal(op1(e11,e11),e10)** -> . % 0.64/0.81 2984[6:Spt:2967.0,2902.1] || -> equal(op1(e10,e11),e10)**. % 0.64/0.81 2987[6:Rew:2984.0,113.0] || equal(op1(e10,e10),e10)** -> . % 0.64/0.81 2996[6:MRR:530.0,2987.0] || -> equal(op1(e13,e10),e10)**. % 0.64/0.81 3016[6:Rew:2996.0,2835.1] || -> equal(op1(e13,e11),e12)** equal(e12,e10). % 0.64/0.81 3017[6:MRR:3016.1,2.0] || -> equal(op1(e13,e11),e12)**. % 0.64/0.81 3020[6:Rew:3017.0,2825.0] || -> equal(op1(e11,e12),e11)**. % 0.64/0.81 3025[6:Rew:3020.0,122.0] || equal(op1(e11,e11),e11)** -> . % 0.64/0.81 3035[6:Rew:2984.0,519.2,3017.0,519.1] || -> equal(op1(e11,e11),e11)** equal(e12,e11) equal(e11,e10). % 0.64/0.81 3036[6:MRR:3035.0,3035.1,3035.2,3025.0,4.0,1.0] || -> . % 0.64/0.81 3042[4:Spt:3036.0,319.0,2765.0] || equal(op1(e10,e13),e13)** -> . % 0.64/0.81 3043[4:Spt:3036.0,319.1,319.2,319.3] || -> equal(op1(e10,e13),e10) equal(op1(e10,e13),e12)** equal(op1(e10,e13),e11). % 0.64/0.81 3045[4:MRR:525.0,3042.0] || -> equal(op1(e10,e12),e13)** equal(op1(e10,e11),e13). % 0.64/0.81 3046[5:Spt:3043.0] || -> equal(op1(e10,e13),e10)**. % 0.64/0.81 3048[5:Rew:3046.0,107.0] || equal(op1(e11,e13),e10)** -> . % 0.64/0.81 3051[5:Rew:3046.0,115.0] || equal(op1(e10,e10),e10)** -> . % 0.64/0.81 3054[5:Rew:3046.0,192.1] || SkC0 -> equal(op1(e13,e10),e13)**. % 0.64/0.81 3062[5:MRR:524.1,3048.0] || -> equal(op1(e11,e11),e10)**. % 0.64/0.81 3070[5:Rew:3062.0,194.1] || SkC1 -> equal(op1(e11,e10),e11)**. % 0.64/0.81 3077[5:MRR:530.0,3051.0] || -> equal(op1(e13,e10),e10)**. % 0.64/0.81 3078[5:MRR:540.0,3051.0] || -> equal(op1(e10,e10),e12)**. % 0.64/0.81 3085[5:Rew:3077.0,419.2] || -> SkC1 SkC0 equal(op1(e10,e10),e10)**. % 0.64/0.81 3099[5:Rew:3077.0,3054.1] || SkC0* -> equal(e13,e10). % 0.64/0.81 3100[5:MRR:3099.1,3.0] || SkC0* -> . % 0.64/0.81 3104[5:Rew:428.0,3070.1] || SkC1* -> equal(e13,e11). % 0.64/0.81 3105[5:MRR:3104.1,5.0] || SkC1* -> . % 0.64/0.81 3106[5:Rew:3078.0,3085.2] || -> SkC1 SkC0* equal(e12,e10). % 0.64/0.81 3107[5:MRR:3106.0,3106.1,3106.2,3105.0,3100.0,2.0] || -> . % 0.64/0.81 3125[5:Spt:3107.0,3043.0,3046.0] || equal(op1(e10,e13),e10)** -> . % 0.64/0.81 3126[5:Spt:3107.0,3043.1,3043.2] || -> equal(op1(e10,e13),e12)** equal(op1(e10,e13),e11). % 0.64/0.81 3127[5:MRR:435.1,3125.0] || SkC1* -> . % 0.64/0.81 3128[5:MRR:419.0,3127.0] || -> SkC0 equal(op1(e10,op1(e13,e10)),e10)**. % 0.64/0.81 3130[5:MRR:417.0,3127.0] || -> SkC0 equal(op1(e12,op1(e13,e12)),e12)**. % 0.64/0.81 3131[5:MRR:418.0,3127.0] || -> SkC0 equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.81 3132[5:MRR:504.1,3125.0] || -> equal(op1(e13,e13),e10)** equal(op1(e11,e13),e10). % 0.64/0.81 3133[5:MRR:531.1,3125.0] || -> equal(op1(e10,e10),e10) equal(op1(e10,e11),e10)**. % 0.64/0.81 3134[6:Spt:3126.0] || -> equal(op1(e10,e13),e12)**. % 0.64/0.81 3137[6:Rew:3134.0,118.0] || equal(op1(e10,e12),e12)** -> . % 0.64/0.81 3139[6:Rew:3134.0,115.0] || equal(op1(e10,e10),e12)** -> . % 0.64/0.81 3141[6:Rew:3134.0,108.0] || equal(op1(e12,e13),e12)** -> . % 0.64/0.81 3143[6:Rew:3134.0,192.1] || SkC0 -> equal(op1(e13,e12),e13)**. % 0.64/0.81 3146[6:Rew:3134.0,2755.10] || equal(h3(op1(e10,e10)),e20) equal(h3(op1(e13,e13)),e20)** equal(h3(op1(e11,e11)),e20) equal(h3(op1(e13,e12)),op2(e23,e22)) equal(h3(op1(e13,e11)),op2(e23,e21)) equal(h3(op1(e13,e10)),e22) equal(h3(op1(e12,e13)),op2(e22,e23)) equal(h3(op1(e12,e11)),op2(e22,e21)) equal(h3(op1(e11,e13)),op2(e21,e23)) equal(h3(op1(e11,e12)),op2(e21,e22)) equal(op2(e20,e23),h3(e12)) equal(h3(op1(e10,e12)),op2(e20,e22)) equal(h3(op1(e10,e11)),op2(e20,e21)) -> . % 0.64/0.81 3150[6:MRR:539.0,3137.0] || -> equal(op1(e10,e12),e13)** equal(op1(e10,e12),e11). % 0.64/0.81 3153[6:MRR:540.1,3139.0] || -> equal(op1(e10,e10),e10)**. % 0.64/0.81 3154[6:MRR:527.0,3139.0] || -> equal(op1(e13,e10),e12)**. % 0.64/0.81 3167[6:Rew:3154.0,3128.1] || -> SkC0 equal(op1(e10,e12),e10)**. % 0.64/0.81 3170[6:MRR:534.1,3141.0] || -> equal(op1(e12,e13),e13)**. % 0.64/0.81 3171[6:MRR:513.0,3141.0] || -> equal(op1(e12,e11),e12)**. % 0.64/0.81 3190[6:MRR:3167.1,401.0] || -> SkC0*. % 0.64/0.81 3192[6:MRR:190.0,3190.0] || -> equal(op1(e11,op1(e10,e11)),e11)**. % 0.64/0.81 3196[6:MRR:3143.0,3190.0] || -> equal(op1(e13,e12),e13)**. % 0.64/0.81 3198[6:Rew:3196.0,103.0] || equal(op1(e10,e12),e13)** -> . % 0.64/0.81 3203[6:Rew:3196.0,503.2] || -> equal(op1(e13,e13),e11)** equal(op1(e13,e11),e11) equal(e13,e11). % 0.64/0.81 3205[6:MRR:3045.0,3198.0] || -> equal(op1(e10,e11),e13)**. % 0.64/0.81 3212[6:Rew:3205.0,3192.0] || -> equal(op1(e11,e13),e11)**. % 0.64/0.81 3214[6:Rew:3212.0,124.0] || equal(op1(e11,e12),e11)** -> . % 0.64/0.81 3217[6:Rew:3212.0,3132.1] || -> equal(op1(e13,e13),e10)** equal(e11,e10). % 0.64/0.81 3218[6:Rew:3212.0,524.1] || -> equal(op1(e11,e11),e10)** equal(e11,e10). % 0.64/0.81 3220[6:MRR:537.1,3214.0] || -> equal(op1(e11,e12),e12)**. % 0.64/0.81 3226[6:MRR:3217.1,1.0] || -> equal(op1(e13,e13),e10)**. % 0.64/0.81 3231[6:MRR:3218.1,1.0] || -> equal(op1(e11,e11),e10)**. % 0.64/0.81 3236[6:MRR:3150.0,3198.0] || -> equal(op1(e10,e12),e11)**. % 0.64/0.81 3241[6:Rew:3226.0,3203.0] || -> equal(e11,e10) equal(op1(e13,e11),e11)** equal(e13,e11). % 0.64/0.81 3242[6:MRR:3241.0,3241.2,1.0,5.0] || -> equal(op1(e13,e11),e11)**. % 0.64/0.81 3246[6:Rew:437.0,3146.12,3205.0,3146.12,361.0,3146.11,3236.0,3146.11,31.0,3146.10,31.0,3146.9,3220.0,3146.9,361.0,3146.8,3212.0,3146.8,31.0,3146.7,3171.0,3146.7,437.0,3146.6,3170.0,3146.6,31.0,3146.5,3154.0,3146.5,361.0,3146.4,3242.0,3146.4,437.0,3146.3,3196.0,3146.3,339.0,3146.2,3231.0,3146.2,339.0,3146.1,3226.0,3146.1,339.0,3146.0,3153.0,3146.0] || equal(e20,e20) equal(e20,e20) equal(e20,e20) equal(op2(e23,e22),e23)** equal(op2(e23,e21),e21) equal(e22,e22) equal(op2(e22,e23),e23) equal(op2(e22,e21),e22) equal(op2(e21,e23),e21) equal(op2(e21,e22),e22) equal(op2(e20,e23),e22) equal(op2(e20,e22),e21) equal(op2(e20,e21),e23) -> . % 0.64/0.81 3247[6:Obv:3246.5] || equal(op2(e23,e22),e23)** equal(op2(e23,e21),e21) equal(op2(e22,e23),e23) equal(op2(e22,e21),e22) equal(op2(e21,e23),e21) equal(op2(e21,e22),e22) equal(op2(e20,e23),e22) equal(op2(e20,e22),e21) equal(op2(e20,e21),e23) -> . % 0.64/0.81 3253[7:Spt:478.0] || -> equal(op2(e20,e23),e23)**. % 0.64/0.81 3257[7:Rew:3253.0,156.0] || equal(op2(e22,e23),e23)** -> . % 0.64/0.81 3258[7:Rew:3253.0,166.0] || equal(op2(e20,e22),e23)** -> . % 0.64/0.81 3269[7:MRR:457.0,3257.0] || -> equal(op2(e22,e21),e23)**. % 0.64/0.81 3270[7:MRR:491.0,3257.0] || -> equal(op2(e22,e23),e22)**. % 0.64/0.81 3280[7:Rew:3270.0,158.0] || equal(op2(e21,e23),e22)** -> . % 0.64/0.81 3283[7:MRR:497.1,3258.0] || -> equal(op2(e20,e22),e22)** equal(op2(e20,e22),e21). % 0.64/0.81 3297[7:MRR:2736.1,3280.0] || -> equal(op2(e21,e22),e22)**. % 0.64/0.81 3302[7:Rew:3297.0,149.0] || equal(op2(e20,e22),e22)** -> . % 0.64/0.81 3318[7:MRR:3283.0,3302.0] || -> equal(op2(e20,e22),e21)**. % 0.64/0.81 3320[7:Rew:3318.0,2704.0] || -> equal(op2(e22,e21),e22)**. % 0.64/0.81 3323[7:Rew:3269.0,3320.0] || -> equal(e23,e22)**. % 0.64/0.81 3324[7:MRR:3323.0,12.0] || -> . % 0.64/0.81 3325[7:Spt:3324.0,478.0,3253.0] || equal(op2(e20,e23),e23)** -> . % 0.64/0.81 3326[7:Spt:3324.0,478.1,478.2] || -> equal(op2(e20,e22),e23)** equal(op2(e20,e21),e23). % 0.64/0.81 3327[7:MRR:1455.1,3325.0] || -> equal(op2(e22,e23),e23)**. % 0.64/0.81 3331[7:Rew:3327.0,177.0] || equal(op2(e22,e21),e23)** -> . % 0.64/0.81 3333[7:MRR:492.1,3331.0] || -> equal(op2(e22,e21),e22)**. % 0.64/0.81 3337[7:Rew:3333.0,144.0] || equal(op2(e20,e21),e22)** -> . % 0.64/0.81 3339[7:MRR:2752.0,3325.0] || -> equal(op2(e20,e23),e22)** equal(op2(e20,e23),e21). % 0.64/0.81 3342[7:MRR:2749.2,3337.0] || -> equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)**. % 0.64/0.81 3343[7:MRR:2754.2,3337.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e21),e23)**. % 0.64/0.81 3346[7:Rew:3333.0,3247.3,3327.0,3247.2] || equal(op2(e23,e22),e23)** equal(op2(e23,e21),e21) equal(e23,e23) equal(e22,e22) equal(op2(e21,e23),e21) equal(op2(e21,e22),e22) equal(op2(e20,e23),e22) equal(op2(e20,e22),e21) equal(op2(e20,e21),e23) -> . % 0.64/0.81 3347[7:Obv:3346.3] || equal(op2(e23,e22),e23)** equal(op2(e23,e21),e21) equal(op2(e21,e23),e21) equal(op2(e21,e22),e22) equal(op2(e20,e23),e22) equal(op2(e20,e22),e21) equal(op2(e20,e21),e23) -> . % 0.64/0.81 3348[8:Spt:3326.0] || -> equal(op2(e20,e22),e23)**. % 0.64/0.81 3352[8:Rew:3348.0,151.0] || equal(op2(e23,e22),e23)** -> . % 0.64/0.81 3354[8:Rew:3348.0,164.0] || equal(op2(e20,e21),e23)** -> . % 0.64/0.81 3363[8:MRR:2746.0,3352.0] || -> equal(op2(e23,e22),e21)**. % 0.64/0.81 3374[8:MRR:3343.1,3354.0] || -> equal(op2(e20,e21),e21)**. % 0.64/0.81 3377[8:Rew:3374.0,165.0] || equal(op2(e20,e23),e21)** -> . % 0.64/0.81 3394[8:MRR:3339.1,3377.0] || -> equal(op2(e20,e23),e22)**. % 0.64/0.81 3397[8:Rew:3394.0,2706.0] || -> equal(op2(e23,e22),e23)**. % 0.64/0.81 3399[8:Rew:3363.0,3397.0] || -> equal(e23,e21)**. % 0.64/0.82 3400[8:MRR:3399.0,11.0] || -> . % 0.64/0.82 3403[8:Spt:3400.0,3326.0,3348.0] || equal(op2(e20,e22),e23)** -> . % 0.64/0.82 3404[8:Spt:3400.0,3326.1] || -> equal(op2(e20,e21),e23)**. % 0.64/0.82 3407[8:Rew:3404.0,2705.0] || -> equal(op2(e21,e23),e21)**. % 0.64/0.82 3411[8:Rew:3404.0,145.0] || equal(op2(e23,e21),e23)** -> . % 0.64/0.82 3413[8:Rew:3407.0,172.0] || equal(op2(e21,e22),e21)** -> . % 0.64/0.82 3415[8:MRR:455.1,3403.0] || -> equal(op2(e23,e22),e23)**. % 0.64/0.82 3421[8:MRR:2753.0,3411.0] || -> equal(op2(e23,e21),e21)**. % 0.64/0.82 3425[8:MRR:494.1,3413.0] || -> equal(op2(e21,e22),e22)**. % 0.64/0.82 3428[8:Rew:3425.0,149.0] || equal(op2(e20,e22),e22)** -> . % 0.64/0.82 3430[8:MRR:3342.0,3428.0] || -> equal(op2(e20,e23),e22)**. % 0.64/0.82 3436[8:MRR:497.0,497.1,3428.0,3403.0] || -> equal(op2(e20,e22),e21)**. % 0.64/0.82 3441[8:Rew:3404.0,3347.6,3436.0,3347.5,3430.0,3347.4,3425.0,3347.3,3407.0,3347.2,3421.0,3347.1,3415.0,3347.0] || equal(e23,e23)* equal(e21,e21) equal(e21,e21) equal(e22,e22) equal(e22,e22) equal(e21,e21) equal(e23,e23)* -> . % 0.64/0.82 3442[8:Obv:3441.6] || -> . % 0.64/0.82 3443[6:Spt:3442.0,3126.0,3134.0] || equal(op1(e10,e13),e12)** -> . % 0.64/0.82 3444[6:Spt:3442.0,3126.1] || -> equal(op1(e10,e13),e11)**. % 0.64/0.82 3448[6:Rew:3444.0,107.0] || equal(op1(e11,e13),e11)** -> . % 0.64/0.82 3450[6:Rew:3444.0,109.0] || equal(op1(e13,e13),e11)** -> . % 0.64/0.82 3452[6:Rew:3444.0,117.0] || equal(op1(e10,e11),e11)** -> . % 0.64/0.82 3453[6:Rew:3444.0,118.0] || equal(op1(e10,e12),e11)** -> . % 0.64/0.82 3454[6:Rew:3444.0,192.1] || SkC0 -> equal(op1(e13,e11),e13)**. % 0.64/0.82 3455[6:MRR:539.2,3453.0] || -> equal(op1(e10,e12),e12) equal(op1(e10,e12),e13)**. % 0.64/0.82 3457[6:MRR:503.0,3450.0] || -> equal(op1(e13,e11),e11) equal(op1(e13,e12),e11)**. % 0.64/0.82 3462[6:MRR:321.0,3452.0] || -> equal(op1(e10,e11),e10) equal(op1(e10,e11),e13)** equal(op1(e10,e11),e12). % 0.64/0.82 3465[6:Rew:3444.0,302.2] || -> equal(op1(e10,e12),e12)** equal(op1(e10,e10),e12) equal(e12,e11) equal(op1(e10,e11),e12). % 0.64/0.82 3466[6:MRR:3465.2,4.0] || -> equal(op1(e10,e12),e12)** equal(op1(e10,e10),e12) equal(op1(e10,e11),e12). % 0.64/0.82 3471[7:Spt:309.0] || -> equal(op1(e13,e11),e13)**. % 0.64/0.82 3473[7:Rew:3471.0,100.0] || equal(op1(e12,e11),e13)** -> . % 0.64/0.82 3474[7:Rew:3471.0,3131.1] || -> SkC0 equal(op1(e11,e13),e11)**. % 0.64/0.82 3475[7:Rew:3471.0,134.0] || equal(op1(e13,e12),e13)** -> . % 0.64/0.82 3476[7:Rew:3471.0,97.0] || equal(op1(e10,e11),e13)** -> . % 0.64/0.82 3489[7:MRR:535.1,3473.0] || -> equal(op1(e12,e11),e12)**. % 0.64/0.82 3500[7:Rew:3489.0,96.0] || equal(op1(e10,e11),e12)** -> . % 0.64/0.82 3502[7:MRR:3474.1,3448.0] || -> SkC0*. % 0.64/0.82 3503[7:MRR:189.0,3502.0] || -> equal(op1(e10,op1(e10,e10)),e10)**. % 0.64/0.82 3506[7:MRR:507.0,3475.0] || -> equal(op1(e10,e12),e13)**. % 0.64/0.82 3516[7:MRR:3462.1,3476.0] || -> equal(op1(e10,e11),e10) equal(op1(e10,e11),e12)**. % 0.64/0.82 3547[7:MRR:3516.1,3500.0] || -> equal(op1(e10,e11),e10)**. % 0.64/0.82 3549[7:Rew:3547.0,113.0] || equal(op1(e10,e10),e10)** -> . % 0.64/0.82 3555[7:MRR:540.0,3549.0] || -> equal(op1(e10,e10),e12)**. % 0.64/0.82 3560[7:Rew:3555.0,3503.0] || -> equal(op1(e10,e12),e10)**. % 0.64/0.82 3565[7:Rew:3506.0,3560.0] || -> equal(e13,e10)**. % 0.64/0.82 3566[7:MRR:3565.0,3.0] || -> . % 0.64/0.82 3578[7:Spt:3566.0,309.0,3471.0] || equal(op1(e13,e11),e13)** -> . % 0.64/0.82 3579[7:Spt:3566.0,309.1,309.2,309.3] || -> equal(op1(e13,e11),e11) equal(op1(e13,e11),e12)** equal(op1(e13,e11),e10). % 0.64/0.82 3580[7:MRR:3454.1,3578.0] || SkC0* -> . % 0.64/0.82 3581[7:MRR:3131.0,3580.0] || -> equal(op1(e11,op1(e13,e11)),e11)**. % 0.64/0.82 3584[7:MRR:3130.0,3580.0] || -> equal(op1(e12,op1(e13,e12)),e12)**. % 0.64/0.82 3585[7:MRR:516.0,3578.0] || -> equal(op1(e12,e11),e13)** equal(op1(e10,e11),e13). % 0.64/0.82 3586[7:MRR:501.2,3578.0] || -> equal(op1(e13,e13),e13)** equal(op1(e13,e12),e13). % 0.64/0.82 3587[8:Spt:3579.0] || -> equal(op1(e13,e11),e11)**. % 0.64/0.82 3593[8:Rew:3587.0,3581.0] || -> equal(op1(e11,e11),e11)**. % 0.64/0.82 3596[8:Rew:3587.0,522.2] || -> equal(op1(e11,e11),e10)** equal(op1(e10,e11),e10) equal(e11,e10). % 0.64/0.82 3599[8:Rew:3587.0,293.2] || -> equal(op1(e12,e11),e12)** equal(op1(e11,e11),e12) equal(e12,e11) equal(op1(e10,e11),e12). % 0.64/0.82 3629[8:Rew:3593.0,3596.0] || -> equal(e11,e10) equal(op1(e10,e11),e10)** equal(e11,e10). % 0.64/0.82 3630[8:Obv:3629.0] || -> equal(op1(e10,e11),e10)** equal(e11,e10). % 0.64/0.82 3631[8:MRR:3630.1,1.0] || -> equal(op1(e10,e11),e10)**. % 0.64/0.82 3635[8:Rew:3631.0,113.0] || equal(op1(e10,e10),e10)** -> . % 0.64/0.82 3640[8:MRR:540.0,3635.0] || -> equal(op1(e10,e10),e12)**. % 0.64/0.82 3650[8:Rew:3640.0,114.0] || equal(op1(e10,e12),e12)** -> . % 0.64/0.82 3655[8:MRR:3455.0,3650.0] || -> equal(op1(e10,e12),e13)**. % 0.64/0.82 3658[8:Rew:3655.0,103.0] || equal(op1(e13,e12),e13)** -> . % 0.64/0.82 3660[8:MRR:3586.1,3658.0] || -> equal(op1(e13,e13),e13)**. % 0.64/0.82 3663[8:Rew:3660.0,112.0] || equal(op1(e12,e13),e13)** -> . % 0.64/0.82 3673[8:MRR:509.0,3663.0] || -> equal(op1(e12,e11),e13)**. % 0.64/0.82 3687[8:Rew:3631.0,3599.3,3593.0,3599.1,3673.0,3599.0] || -> equal(e13,e12)** equal(e12,e11) equal(e12,e11) equal(e12,e10). % 0.64/0.82 3688[8:Obv:3687.1] || -> equal(e13,e12)** equal(e12,e11) equal(e12,e10). % 0.64/0.82 3689[8:MRR:3688.0,3688.1,3688.2,6.0,4.0,2.0] || -> . % 0.64/0.82 3695[8:Spt:3689.0,3579.0,3587.0] || equal(op1(e13,e11),e11)** -> . % 0.64/0.82 3696[8:Spt:3689.0,3579.1,3579.2] || -> equal(op1(e13,e11),e12)** equal(op1(e13,e11),e10). % 0.64/0.82 3697[8:MRR:3457.0,3695.0] || -> equal(op1(e13,e12),e11)**. % 0.64/0.82 3699[8:Rew:3697.0,3584.0] || -> equal(op1(e12,e11),e12)**. % 0.64/0.82 3701[8:Rew:3697.0,105.0] || equal(op1(e11,e12),e11)** -> . % 0.64/0.82 3725[8:MRR:537.1,3701.0] || -> equal(op1(e11,e12),e12)**. % 0.64/0.82 3728[8:Rew:3725.0,101.0] || equal(op1(e10,e12),e12)** -> . % 0.64/0.82 3730[8:Rew:3699.0,3585.0] || -> equal(e13,e12) equal(op1(e10,e11),e13)**. % 0.64/0.82 3731[8:MRR:3730.0,6.0] || -> equal(op1(e10,e11),e13)**. % 0.64/0.82 3737[8:Rew:3731.0,3133.1] || -> equal(op1(e10,e10),e10)** equal(e13,e10). % 0.64/0.82 3738[8:MRR:3737.1,3.0] || -> equal(op1(e10,e10),e10)**. % 0.64/0.82 3774[8:Rew:3731.0,3466.2,3738.0,3466.1] || -> equal(op1(e10,e12),e12)** equal(e12,e10) equal(e13,e12). % 0.64/0.82 3775[8:MRR:3774.0,3774.1,3774.2,3728.0,2.0,6.0] || -> . % 0.64/0.82 % SZS output end Refutation % 0.64/0.82 Formulae used in the proof : ax7 ax8 ax16 ax12 ax13 co1 ax14 ax15 ax17 ax5 ax6 ax10 ax11 ax4 ax3 ax2 ax1 % 0.64/0.82 %------------------------------------------------------------------------------