%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG103+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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:27 EDT 2022 % Result : Theorem 0.77s 0.96s % Output : Refutation 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : ALG103+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/0.12 % Command : run_spass %d %s % 0.11/0.32 % Computer : n018.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Wed Jun 8 13:42:22 EDT 2022 % 0.11/0.32 % CPUTime : % 0.77/0.96 % 0.77/0.96 SPASS V 3.9 % 0.77/0.96 SPASS beiseite: Proof found. % 0.77/0.96 % SZS status Theorem % 0.77/0.96 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.77/0.96 SPASS derived 1187 clauses, backtracked 1113 clauses, performed 11 splits and kept 2114 clauses. % 0.77/0.96 SPASS allocated 87710 KBytes. % 0.77/0.96 SPASS spent 0:00:00.63 on the problem. % 0.77/0.96 0:00:00.04 for the input. % 0.77/0.96 0:00:00.20 for the FLOTTER CNF translation. % 0.77/0.96 0:00:00.00 for inferences. % 0.77/0.96 0:00:00.01 for the backtracking. % 0.77/0.96 0:00:00.34 for the reduction. % 0.77/0.96 % 0.77/0.96 % 0.77/0.96 Here is a proof with depth 2, length 1248 : % 0.77/0.96 % SZS output start Refutation % 0.77/0.96 1[0:Inp] || equal(e11,e10)** -> . % 0.77/0.96 2[0:Inp] || equal(e12,e10)** -> . % 0.77/0.96 3[0:Inp] || equal(e13,e10)** -> . % 0.77/0.96 4[0:Inp] || equal(e12,e11)** -> . % 0.77/0.96 5[0:Inp] || equal(e13,e11)** -> . % 0.77/0.96 6[0:Inp] || equal(e13,e12)** -> . % 0.77/0.96 7[0:Inp] || equal(e21,e20)** -> . % 0.77/0.96 8[0:Inp] || equal(e22,e20)** -> . % 0.77/0.96 9[0:Inp] || equal(e23,e20)** -> . % 0.77/0.96 10[0:Inp] || equal(e22,e21)** -> . % 0.77/0.96 11[0:Inp] || equal(e23,e21)** -> . % 0.77/0.96 12[0:Inp] || equal(e23,e22)** -> . % 0.77/0.96 29[0:Inp] || -> equal(h1(e10),e20)**. % 0.77/0.96 30[0:Inp] || -> equal(h2(e10),e21)**. % 0.77/0.96 32[0:Inp] || -> equal(h4(e10),e23)**. % 0.77/0.96 33[0:Inp] || -> equal(op1(e10,e10),e11)**. % 0.77/0.96 34[0:Inp] || -> equal(op2(e20,e20),e21)**. % 0.77/0.96 35[0:Inp] || equal(h1(e10),e20)** -> SkC132. % 0.77/0.96 40[0:Inp] || equal(h1(e11),e21)** -> SkC133. % 0.77/0.96 45[0:Inp] || equal(h1(e12),e22)** -> SkC134. % 0.77/0.96 50[0:Inp] || equal(h2(e13),e20)** -> SkC135. % 0.77/0.96 51[0:Inp] || equal(h2(e10),e21)** -> SkC136. % 0.77/0.96 57[0:Inp] || equal(h2(e12),e22)** -> SkC137. % 0.77/0.96 72[0:Inp] || equal(h4(e11),e20)** -> SkC141. % 0.77/0.96 78[0:Inp] || equal(h4(e13),e21)** -> SkC142. % 0.77/0.96 81[0:Inp] || equal(h4(e12),e22)** -> SkC143. % 0.77/0.96 83[0:Inp] || -> equal(op2(e20,e20),h1(e11))**. % 0.77/0.96 84[0:Inp] || -> equal(op2(e21,e21),h2(e11))**. % 0.77/0.96 85[0:Inp] || -> equal(op2(e22,e22),h3(e11))**. % 0.77/0.96 86[0:Inp] || -> equal(op2(e23,e23),h4(e11))**. % 0.77/0.96 87[0:Inp] || SkC0 -> equal(op1(e10,e10),e10)**. % 0.77/0.96 89[0:Inp] || SkC2 -> equal(op1(e12,e12),e12)**. % 0.77/0.96 90[0:Inp] || SkC3 -> equal(op1(e10,e10),e10)**. % 0.77/0.96 91[0:Inp] || SkC4 -> equal(op1(e10,e10),e10)**. % 0.77/0.96 93[0:Inp] || SkC5 -> equal(op1(e10,e10),e10)**. % 0.77/0.96 95[0:Inp] || SkC6 -> equal(op1(e10,e10),e10)**. % 0.77/0.96 97[0:Inp] || SkC7 -> equal(op1(e10,e11),e10)**. % 0.77/0.96 99[0:Inp] || SkC8 -> equal(op1(e10,e11),e10)**. % 0.77/0.96 101[0:Inp] || SkC9 -> equal(op1(e10,e11),e10)**. % 0.77/0.96 103[0:Inp] || SkC10 -> equal(op1(e10,e11),e10)**. % 0.77/0.96 106[0:Inp] || SkC11 -> equal(op1(e10,e10),e12)**. % 0.77/0.96 108[0:Inp] || SkC12 -> equal(op1(e11,e11),e12)**. % 0.77/0.96 110[0:Inp] || SkC13 -> equal(op1(e12,e12),e12)**. % 0.77/0.96 112[0:Inp] || SkC14 -> equal(op1(e13,e13),e12)**. % 0.77/0.96 114[0:Inp] || SkC15 -> equal(op1(e10,e10),e13)**. % 0.77/0.96 115[0:Inp] || SkC16 -> equal(op1(e10,e13),e10)**. % 0.77/0.96 118[0:Inp] || SkC17 -> equal(op1(e12,e12),e13)**. % 0.77/0.96 120[0:Inp] || SkC18 -> equal(op1(e13,e13),e13)**. % 0.77/0.96 122[0:Inp] || SkC19 -> equal(op1(e10,e10),e10)**. % 0.77/0.96 123[0:Inp] || SkC20 -> equal(op1(e11,e10),e11)**. % 0.77/0.96 125[0:Inp] || SkC21 -> equal(op1(e11,e10),e11)**. % 0.77/0.96 127[0:Inp] || SkC22 -> equal(op1(e11,e10),e11)**. % 0.77/0.96 129[0:Inp] || SkC23 -> equal(op1(e11,e11),e11)**. % 0.77/0.96 131[0:Inp] || SkC24 -> equal(op1(e11,e11),e11)**. % 0.77/0.96 132[0:Inp] || SkC25 -> equal(op1(e11,e11),e11)**. % 0.77/0.96 134[0:Inp] || SkC26 -> equal(op1(e11,e11),e11)**. % 0.77/0.96 137[0:Inp] || SkC27 -> equal(op1(e10,e10),e12)**. % 0.77/0.96 138[0:Inp] || SkC28 -> equal(op1(e11,e12),e11)**. % 0.77/0.96 141[0:Inp] || SkC29 -> equal(op1(e12,e12),e12)**. % 0.77/0.96 143[0:Inp] || SkC30 -> equal(op1(e13,e13),e12)**. % 0.77/0.96 145[0:Inp] || SkC31 -> equal(op1(e10,e10),e13)**. % 0.77/0.96 146[0:Inp] || SkC32 -> equal(op1(e11,e13),e11)**. % 0.77/0.96 149[0:Inp] || SkC33 -> equal(op1(e12,e12),e13)**. % 0.77/0.96 151[0:Inp] || SkC34 -> equal(op1(e13,e13),e13)**. % 0.77/0.96 153[0:Inp] || SkC35 -> equal(op1(e10,e10),e10)**. % 0.77/0.96 154[0:Inp] || SkC36 -> equal(op1(e12,e10),e12)**. % 0.77/0.96 156[0:Inp] || SkC37 -> equal(op1(e12,e10),e12)**. % 0.77/0.96 158[0:Inp] || SkC38 -> equal(op1(e12,e10),e12)**. % 0.77/0.96 160[0:Inp] || SkC39 -> equal(op1(e12,e11),e12)**. % 0.77/0.96 163[0:Inp] || SkC40 -> equal(op1(e11,e11),e11)**. % 0.77/0.96 164[0:Inp] || SkC41 -> equal(op1(e12,e11),e12)**. % 0.77/0.96 166[0:Inp] || SkC42 -> equal(op1(e12,e11),e12)**. % 0.77/0.96 169[0:Inp] || SkC43 -> equal(op1(e10,e10),e12)**. % 0.77/0.96 170[0:Inp] || SkC44 -> equal(op1(e12,e12),e12)**. % 0.77/0.96 172[0:Inp] || SkC45 -> equal(op1(e12,e12),e12)**. % 0.77/0.96 173[0:Inp] || SkC46 -> equal(op1(e12,e12),e12)**. % 0.77/0.96 176[0:Inp] || SkC47 -> equal(op1(e10,e10),e13)**. % 0.77/0.96 177[0:Inp] || SkC48 -> equal(op1(e12,e13),e12)**. % 0.77/0.96 179[0:Inp] || SkC49 -> equal(op1(e12,e13),e12)**. % 0.77/0.96 182[0:Inp] || SkC50 -> equal(op1(e13,e13),e13)**. % 0.77/0.96 184[0:Inp] || SkC51 -> equal(op1(e10,e10),e10)**. % 0.77/0.96 185[0:Inp] || SkC52 -> equal(op1(e13,e10),e13)**. % 0.77/0.96 187[0:Inp] || SkC53 -> equal(op1(e13,e10),e13)**. % 0.77/0.96 189[0:Inp] || SkC54 -> equal(op1(e13,e10),e13)**. % 0.77/0.96 191[0:Inp] || SkC55 -> equal(op1(e13,e11),e13)**. % 0.77/0.96 194[0:Inp] || SkC56 -> equal(op1(e11,e11),e11)**. % 0.77/0.96 195[0:Inp] || SkC57 -> equal(op1(e13,e11),e13)**. % 0.77/0.96 196[0:Inp] || SkC57 -> equal(op1(e12,e12),e11)**. % 0.77/0.96 197[0:Inp] || SkC58 -> equal(op1(e13,e11),e13)**. % 0.77/0.96 200[0:Inp] || SkC59 -> equal(op1(e10,e10),e12)**. % 0.77/0.96 202[0:Inp] || SkC60 -> equal(op1(e11,e11),e12)**. % 0.77/0.96 204[0:Inp] || SkC61 -> equal(op1(e12,e12),e12)**. % 0.77/0.96 205[0:Inp] || SkC62 -> equal(op1(e13,e12),e13)**. % 0.77/0.96 208[0:Inp] || SkC63 -> equal(op1(e10,e10),e13)**. % 0.77/0.96 209[0:Inp] || SkC64 -> equal(op1(e13,e13),e13)**. % 0.77/0.96 211[0:Inp] || SkC65 -> equal(op1(e13,e13),e13)**. % 0.77/0.96 213[0:Inp] || SkC66 -> equal(op2(e20,e20),e20)**. % 0.77/0.96 215[0:Inp] || SkC68 -> equal(op2(e22,e22),e22)**. % 0.77/0.96 216[0:Inp] || SkC69 -> equal(op2(e20,e20),e20)**. % 0.77/0.96 217[0:Inp] || SkC70 -> equal(op2(e20,e20),e20)**. % 0.77/0.96 219[0:Inp] || SkC71 -> equal(op2(e20,e20),e20)**. % 0.77/0.96 221[0:Inp] || SkC72 -> equal(op2(e20,e20),e20)**. % 0.77/0.96 223[0:Inp] || SkC73 -> equal(op2(e20,e21),e20)**. % 0.77/0.96 225[0:Inp] || SkC74 -> equal(op2(e20,e21),e20)**. % 0.77/0.96 227[0:Inp] || SkC75 -> equal(op2(e20,e21),e20)**. % 0.77/0.96 229[0:Inp] || SkC76 -> equal(op2(e20,e21),e20)**. % 0.77/0.96 232[0:Inp] || SkC77 -> equal(op2(e20,e20),e22)**. % 0.77/0.96 234[0:Inp] || SkC78 -> equal(op2(e21,e21),e22)**. % 0.77/0.96 236[0:Inp] || SkC79 -> equal(op2(e22,e22),e22)**. % 0.77/0.96 238[0:Inp] || SkC80 -> equal(op2(e23,e23),e22)**. % 0.77/0.96 240[0:Inp] || SkC81 -> equal(op2(e20,e20),e23)**. % 0.77/0.96 241[0:Inp] || SkC82 -> equal(op2(e20,e23),e20)**. % 0.77/0.96 244[0:Inp] || SkC83 -> equal(op2(e22,e22),e23)**. % 0.77/0.96 246[0:Inp] || SkC84 -> equal(op2(e23,e23),e23)**. % 0.77/0.96 248[0:Inp] || SkC85 -> equal(op2(e20,e20),e20)**. % 0.77/0.96 249[0:Inp] || SkC86 -> equal(op2(e21,e20),e21)**. % 0.77/0.96 251[0:Inp] || SkC87 -> equal(op2(e21,e20),e21)**. % 0.77/0.96 253[0:Inp] || SkC88 -> equal(op2(e21,e20),e21)**. % 0.77/0.96 255[0:Inp] || SkC89 -> equal(op2(e21,e21),e21)**. % 0.77/0.96 257[0:Inp] || SkC90 -> equal(op2(e21,e21),e21)**. % 0.77/0.96 258[0:Inp] || SkC91 -> equal(op2(e21,e21),e21)**. % 0.77/0.96 260[0:Inp] || SkC92 -> equal(op2(e21,e21),e21)**. % 0.77/0.96 263[0:Inp] || SkC93 -> equal(op2(e20,e20),e22)**. % 0.77/0.96 264[0:Inp] || SkC94 -> equal(op2(e21,e22),e21)**. % 0.77/0.96 267[0:Inp] || SkC95 -> equal(op2(e22,e22),e22)**. % 0.77/0.96 269[0:Inp] || SkC96 -> equal(op2(e23,e23),e22)**. % 0.77/0.96 271[0:Inp] || SkC97 -> equal(op2(e20,e20),e23)**. % 0.77/0.96 272[0:Inp] || SkC98 -> equal(op2(e21,e23),e21)**. % 0.77/0.96 275[0:Inp] || SkC99 -> equal(op2(e22,e22),e23)**. % 0.77/0.96 277[0:Inp] || SkC100 -> equal(op2(e23,e23),e23)**. % 0.77/0.96 279[0:Inp] || SkC101 -> equal(op2(e20,e20),e20)**. % 0.77/0.96 280[0:Inp] || SkC102 -> equal(op2(e22,e20),e22)**. % 0.77/0.96 282[0:Inp] || SkC103 -> equal(op2(e22,e20),e22)**. % 0.77/0.96 284[0:Inp] || SkC104 -> equal(op2(e22,e20),e22)**. % 0.77/0.96 286[0:Inp] || SkC105 -> equal(op2(e22,e21),e22)**. % 0.77/0.96 289[0:Inp] || SkC106 -> equal(op2(e21,e21),e21)**. % 0.77/0.96 290[0:Inp] || SkC107 -> equal(op2(e22,e21),e22)**. % 0.77/0.96 292[0:Inp] || SkC108 -> equal(op2(e22,e21),e22)**. % 0.77/0.96 295[0:Inp] || SkC109 -> equal(op2(e20,e20),e22)**. % 0.77/0.96 296[0:Inp] || SkC110 -> equal(op2(e22,e22),e22)**. % 0.77/0.96 298[0:Inp] || SkC111 -> equal(op2(e22,e22),e22)**. % 0.77/0.96 299[0:Inp] || SkC112 -> equal(op2(e22,e22),e22)**. % 0.77/0.96 302[0:Inp] || SkC113 -> equal(op2(e20,e20),e23)**. % 0.77/0.96 303[0:Inp] || SkC114 -> equal(op2(e22,e23),e22)**. % 0.77/0.96 305[0:Inp] || SkC115 -> equal(op2(e22,e23),e22)**. % 0.77/0.96 308[0:Inp] || SkC116 -> equal(op2(e23,e23),e23)**. % 0.77/0.96 310[0:Inp] || SkC117 -> equal(op2(e20,e20),e20)**. % 0.77/0.96 311[0:Inp] || SkC118 -> equal(op2(e23,e20),e23)**. % 0.77/0.96 313[0:Inp] || SkC119 -> equal(op2(e23,e20),e23)**. % 0.77/0.96 315[0:Inp] || SkC120 -> equal(op2(e23,e20),e23)**. % 0.77/0.96 317[0:Inp] || SkC121 -> equal(op2(e23,e21),e23)**. % 0.77/0.96 320[0:Inp] || SkC122 -> equal(op2(e21,e21),e21)**. % 0.77/0.96 321[0:Inp] || SkC123 -> equal(op2(e23,e21),e23)**. % 0.77/0.96 322[0:Inp] || SkC123 -> equal(op2(e22,e22),e21)**. % 0.77/0.96 323[0:Inp] || SkC124 -> equal(op2(e23,e21),e23)**. % 0.77/0.96 326[0:Inp] || SkC125 -> equal(op2(e20,e20),e22)**. % 0.77/0.96 328[0:Inp] || SkC126 -> equal(op2(e21,e21),e22)**. % 0.77/0.96 330[0:Inp] || SkC127 -> equal(op2(e22,e22),e22)**. % 0.77/0.96 331[0:Inp] || SkC128 -> equal(op2(e23,e22),e23)**. % 0.77/0.96 334[0:Inp] || SkC129 -> equal(op2(e20,e20),e23)**. % 0.77/0.96 335[0:Inp] || SkC130 -> equal(op2(e23,e23),e23)**. % 0.77/0.96 337[0:Inp] || SkC131 -> equal(op2(e23,e23),e23)**. % 0.77/0.96 339[0:Inp] || -> equal(op1(e10,op1(e10,e10)),e12)**. % 0.77/0.96 340[0:Inp] || -> equal(op2(e20,op2(e20,e20)),e22)**. % 0.77/0.96 341[0:Inp] || equal(op1(e11,e10),op1(e10,e10))** -> . % 0.77/0.96 343[0:Inp] || equal(op1(e13,e10),op1(e10,e10))** -> . % 0.77/0.96 344[0:Inp] || equal(op1(e12,e10),op1(e11,e10))** -> . % 0.77/0.96 345[0:Inp] || equal(op1(e13,e10),op1(e11,e10))** -> . % 0.77/0.96 346[0:Inp] || equal(op1(e13,e10),op1(e12,e10))** -> . % 0.77/0.96 347[0:Inp] || equal(op1(e11,e11),op1(e10,e11))** -> . % 0.77/0.96 348[0:Inp] || equal(op1(e12,e11),op1(e10,e11))** -> . % 0.77/0.96 349[0:Inp] || equal(op1(e13,e11),op1(e10,e11))** -> . % 0.77/0.96 351[0:Inp] || equal(op1(e13,e11),op1(e11,e11))** -> . % 0.77/0.96 352[0:Inp] || equal(op1(e13,e11),op1(e12,e11))** -> . % 0.77/0.96 356[0:Inp] || equal(op1(e12,e12),op1(e11,e12))** -> . % 0.77/0.96 357[0:Inp] || equal(op1(e13,e12),op1(e11,e12))** -> . % 0.77/0.96 358[0:Inp] || equal(op1(e13,e12),op1(e12,e12))** -> . % 0.77/0.96 359[0:Inp] || equal(op1(e11,e13),op1(e10,e13))** -> . % 0.77/0.96 360[0:Inp] || equal(op1(e12,e13),op1(e10,e13))** -> . % 0.77/0.96 361[0:Inp] || equal(op1(e13,e13),op1(e10,e13))** -> . % 0.77/0.96 363[0:Inp] || equal(op1(e13,e13),op1(e11,e13))** -> . % 0.77/0.96 364[0:Inp] || equal(op1(e13,e13),op1(e12,e13))** -> . % 0.77/0.96 366[0:Inp] || equal(op1(e10,e12),op1(e10,e10))** -> . % 0.77/0.96 367[0:Inp] || equal(op1(e10,e13),op1(e10,e10))** -> . % 0.77/0.96 368[0:Inp] || equal(op1(e10,e12),op1(e10,e11))** -> . % 0.77/0.96 369[0:Inp] || equal(op1(e10,e13),op1(e10,e11))** -> . % 0.77/0.96 371[0:Inp] || equal(op1(e11,e11),op1(e11,e10))** -> . % 0.77/0.96 373[0:Inp] || equal(op1(e11,e13),op1(e11,e10))** -> . % 0.77/0.96 376[0:Inp] || equal(op1(e11,e13),op1(e11,e12))** -> . % 0.77/0.96 377[0:Inp] || equal(op1(e12,e11),op1(e12,e10))** -> . % 0.77/0.96 378[0:Inp] || equal(op1(e12,e12),op1(e12,e10))** -> . % 0.77/0.96 379[0:Inp] || equal(op1(e12,e13),op1(e12,e10))** -> . % 0.77/0.96 381[0:Inp] || equal(op1(e12,e13),op1(e12,e11))** -> . % 0.77/0.96 382[0:Inp] || equal(op1(e12,e13),op1(e12,e12))** -> . % 0.77/0.96 385[0:Inp] || equal(op1(e13,e13),op1(e13,e10))** -> . % 0.77/0.96 386[0:Inp] || equal(op1(e13,e12),op1(e13,e11))** -> . % 0.77/0.96 387[0:Inp] || equal(op1(e13,e13),op1(e13,e11))** -> . % 0.77/0.96 388[0:Inp] || equal(op1(e13,e13),op1(e13,e12))** -> . % 0.77/0.96 389[0:Inp] || equal(op2(e21,e20),op2(e20,e20))** -> . % 0.77/0.96 392[0:Inp] || equal(op2(e22,e20),op2(e21,e20))** -> . % 0.77/0.96 393[0:Inp] || equal(op2(e23,e20),op2(e21,e20))** -> . % 0.77/0.96 394[0:Inp] || equal(op2(e23,e20),op2(e22,e20))** -> . % 0.77/0.96 395[0:Inp] || equal(op2(e21,e21),op2(e20,e21))** -> . % 0.77/0.96 396[0:Inp] || equal(op2(e22,e21),op2(e20,e21))** -> . % 0.77/0.96 397[0:Inp] || equal(op2(e23,e21),op2(e20,e21))** -> . % 0.77/0.96 399[0:Inp] || equal(op2(e23,e21),op2(e21,e21))** -> . % 0.77/0.96 400[0:Inp] || equal(op2(e23,e21),op2(e22,e21))** -> . % 0.77/0.96 404[0:Inp] || equal(op2(e22,e22),op2(e21,e22))** -> . % 0.77/0.96 406[0:Inp] || equal(op2(e23,e22),op2(e22,e22))** -> . % 0.77/0.96 407[0:Inp] || equal(op2(e21,e23),op2(e20,e23))** -> . % 0.77/0.96 408[0:Inp] || equal(op2(e22,e23),op2(e20,e23))** -> . % 0.77/0.96 409[0:Inp] || equal(op2(e23,e23),op2(e20,e23))** -> . % 0.77/0.96 411[0:Inp] || equal(op2(e23,e23),op2(e21,e23))** -> . % 0.77/0.96 412[0:Inp] || equal(op2(e23,e23),op2(e22,e23))** -> . % 0.77/0.96 414[0:Inp] || equal(op2(e20,e22),op2(e20,e20))** -> . % 0.77/0.96 415[0:Inp] || equal(op2(e20,e23),op2(e20,e20))** -> . % 0.77/0.96 417[0:Inp] || equal(op2(e20,e23),op2(e20,e21))** -> . % 0.77/0.96 419[0:Inp] || equal(op2(e21,e21),op2(e21,e20))** -> . % 0.77/0.96 421[0:Inp] || equal(op2(e21,e23),op2(e21,e20))** -> . % 0.77/0.96 422[0:Inp] || equal(op2(e21,e22),op2(e21,e21))** -> . % 0.77/0.96 425[0:Inp] || equal(op2(e22,e21),op2(e22,e20))** -> . % 0.77/0.96 426[0:Inp] || equal(op2(e22,e22),op2(e22,e20))** -> . % 0.77/0.96 427[0:Inp] || equal(op2(e22,e23),op2(e22,e20))** -> . % 0.77/0.96 430[0:Inp] || equal(op2(e22,e23),op2(e22,e22))** -> . % 0.77/0.96 434[0:Inp] || equal(op2(e23,e22),op2(e23,e21))** -> . % 0.77/0.96 435[0:Inp] || equal(op2(e23,e23),op2(e23,e21))** -> . % 0.77/0.96 436[0:Inp] || equal(op2(e23,e23),op2(e23,e22))** -> . % 0.77/0.96 437[0:Inp] || -> equal(op1(e13,e13),e13)** SkC0 SkC1 SkC2. % 0.77/0.96 458[0:Inp] || equal(op1(e12,e12),e12)** SkC13 -> . % 0.77/0.96 460[0:Inp] || SkC14 equal(op1(e13,e12),e13)** -> . % 0.77/0.96 464[0:Inp] || SkC16 equal(op1(e11,e13),e11)** -> . % 0.77/0.96 468[0:Inp] || equal(op1(e13,e13),e13)** SkC18 -> . % 0.77/0.96 472[0:Inp] || equal(op1(e11,e10),e11)** SkC20 -> . % 0.77/0.96 477[0:Inp] || equal(op1(e11,e11),e11)** SkC23 -> . % 0.77/0.96 479[0:Inp] || equal(op1(e11,e11),e11)** SkC24 -> . % 0.77/0.96 480[0:Inp] || equal(op1(e11,e11),e11)** SkC25 -> . % 0.77/0.96 482[0:Inp] || equal(op1(e11,e11),e11)** SkC26 -> . % 0.77/0.96 487[0:Inp] || equal(op1(e11,e12),e11)** SkC28 -> . % 0.77/0.96 489[0:Inp] || equal(op1(e12,e12),e12)** SkC29 -> . % 0.77/0.96 491[0:Inp] || SkC30 equal(op1(e13,e12),e13)** -> . % 0.77/0.96 495[0:Inp] || equal(op1(e11,e13),e11)** SkC32 -> . % 0.77/0.96 499[0:Inp] || equal(op1(e13,e13),e13)** SkC34 -> . % 0.77/0.96 505[0:Inp] || equal(op1(e12,e10),e12)** SkC37 -> . % 0.77/0.96 511[0:Inp] || equal(op1(e11,e11),e11)** SkC40 -> . % 0.77/0.96 513[0:Inp] || equal(op1(e12,e11),e12)** SkC41 -> . % 0.77/0.96 518[0:Inp] || equal(op1(e12,e12),e12)** SkC44 -> . % 0.77/0.96 520[0:Inp] || equal(op1(e12,e12),e12)** SkC45 -> . % 0.77/0.96 521[0:Inp] || equal(op1(e12,e12),e12)** SkC46 -> . % 0.77/0.96 526[0:Inp] || SkC48 equal(op1(e11,e13),e11)** -> . % 0.77/0.96 528[0:Inp] || equal(op1(e12,e13),e12)** SkC49 -> . % 0.77/0.96 530[0:Inp] || equal(op1(e13,e13),e13)** SkC50 -> . % 0.77/0.96 538[0:Inp] || equal(op1(e13,e10),e13)** SkC54 -> . % 0.77/0.96 539[0:Inp] || SkC55 equal(op1(e13,e13),e11)** -> . % 0.77/0.96 542[0:Inp] || equal(op1(e11,e11),e11)** SkC56 -> . % 0.77/0.96 546[0:Inp] || equal(op1(e13,e11),e13)** SkC58 -> . % 0.77/0.96 552[0:Inp] || equal(op1(e12,e12),e12)** SkC61 -> . % 0.77/0.96 554[0:Inp] || equal(op1(e13,e12),e13)** SkC62 -> . % 0.77/0.96 557[0:Inp] || equal(op1(e13,e13),e13)** SkC64 -> . % 0.77/0.96 559[0:Inp] || equal(op1(e13,e13),e13)** SkC65 -> . % 0.77/0.96 561[0:Inp] || -> equal(op2(e23,e23),e23)** SkC66 SkC67 SkC68. % 0.77/0.96 582[0:Inp] || equal(op2(e22,e22),e22)** SkC79 -> . % 0.77/0.96 584[0:Inp] || SkC80 equal(op2(e23,e22),e23)** -> . % 0.77/0.96 588[0:Inp] || SkC82 equal(op2(e21,e23),e21)** -> . % 0.77/0.96 592[0:Inp] || equal(op2(e23,e23),e23)** SkC84 -> . % 0.77/0.96 596[0:Inp] || equal(op2(e21,e20),e21)** SkC86 -> . % 0.77/0.96 601[0:Inp] || equal(op2(e21,e21),e21)** SkC89 -> . % 0.77/0.96 603[0:Inp] || equal(op2(e21,e21),e21)** SkC90 -> . % 0.77/0.96 604[0:Inp] || equal(op2(e21,e21),e21)** SkC91 -> . % 0.77/0.96 606[0:Inp] || equal(op2(e21,e21),e21)** SkC92 -> . % 0.77/0.96 611[0:Inp] || equal(op2(e21,e22),e21)** SkC94 -> . % 0.77/0.96 613[0:Inp] || equal(op2(e22,e22),e22)** SkC95 -> . % 0.77/0.96 615[0:Inp] || SkC96 equal(op2(e23,e22),e23)** -> . % 0.77/0.96 619[0:Inp] || equal(op2(e21,e23),e21)** SkC98 -> . % 0.77/0.96 623[0:Inp] || equal(op2(e23,e23),e23)** SkC100 -> . % 0.77/0.96 629[0:Inp] || equal(op2(e22,e20),e22)** SkC103 -> . % 0.77/0.96 635[0:Inp] || equal(op2(e21,e21),e21)** SkC106 -> . % 0.77/0.96 637[0:Inp] || equal(op2(e22,e21),e22)** SkC107 -> . % 0.77/0.96 642[0:Inp] || equal(op2(e22,e22),e22)** SkC110 -> . % 0.77/0.96 644[0:Inp] || equal(op2(e22,e22),e22)** SkC111 -> . % 0.77/0.96 645[0:Inp] || equal(op2(e22,e22),e22)** SkC112 -> . % 0.77/0.96 650[0:Inp] || SkC114 equal(op2(e21,e23),e21)** -> . % 0.77/0.96 652[0:Inp] || equal(op2(e22,e23),e22)** SkC115 -> . % 0.77/0.96 654[0:Inp] || equal(op2(e23,e23),e23)** SkC116 -> . % 0.77/0.96 662[0:Inp] || equal(op2(e23,e20),e23)** SkC120 -> . % 0.77/0.96 663[0:Inp] || equal(op2(e23,e23),e21)** SkC121 -> . % 0.77/0.96 666[0:Inp] || equal(op2(e21,e21),e21)** SkC122 -> . % 0.77/0.96 670[0:Inp] || equal(op2(e23,e21),e23)** SkC124 -> . % 0.77/0.96 676[0:Inp] || equal(op2(e22,e22),e22)** SkC127 -> . % 0.77/0.96 678[0:Inp] || equal(op2(e23,e22),e23)** SkC128 -> . % 0.77/0.96 681[0:Inp] || equal(op2(e23,e23),e23)** SkC130 -> . % 0.77/0.96 683[0:Inp] || equal(op2(e23,e23),e23)** SkC131 -> . % 0.77/0.96 685[0:Inp] || -> equal(op2(e20,op2(e20,e20)),h1(e12))**. % 0.77/0.96 686[0:Inp] || -> equal(op2(e21,op2(e21,e21)),h2(e12))**. % 0.77/0.96 688[0:Inp] || -> equal(op2(e23,op2(e23,e23)),h4(e12))**. % 0.77/0.96 689[0:Inp] || -> equal(op1(op1(e10,op1(e10,e10)),e10),e13)**. % 0.77/0.96 690[0:Inp] || -> equal(op2(op2(e20,op2(e20,e20)),e20),e23)**. % 0.77/0.96 691[0:Inp] || -> equal(op2(op2(e20,op2(e20,e20)),e20),h1(e13))**. % 0.77/0.96 692[0:Inp] || -> equal(op2(op2(e21,op2(e21,e21)),e21),h2(e13))**. % 0.77/0.96 694[0:Inp] || -> equal(op2(op2(e23,op2(e23,e23)),e23),h4(e13))**. % 0.77/0.96 698[0:Inp] || equal(op1(e10,e10),e11) SkC1 -> equal(op1(e10,e11),e10)**. % 0.77/0.96 703[0:Inp] || SkC2 equal(op1(e13,e13),e12)** -> equal(op1(e13,e12),e13). % 0.77/0.96 707[0:Inp] || equal(op2(e20,e20),e21) SkC67 -> equal(op2(e20,e21),e20)**. % 0.77/0.96 712[0:Inp] || equal(op2(e23,e23),e22)** SkC68 -> equal(op2(e23,e22),e23). % 0.77/0.96 714[0:Inp] || equal(op1(e11,e11),e13) -> equal(op1(e11,e13),e11)** SkC0 SkC1 SkC2. % 0.77/0.96 717[0:Inp] || equal(op2(e21,e21),e23) -> equal(op2(e21,e23),e21)** SkC66 SkC67 SkC68. % 0.77/0.96 719[0:Inp] || -> equal(op2(e20,e23),e23) equal(op2(e21,e23),e23) equal(op2(e22,e23),e23) equal(op2(e23,e23),e23)**. % 0.77/0.96 721[0:Inp] || -> equal(op2(e20,e23),e22) equal(op2(e21,e23),e22) equal(op2(e22,e23),e22) equal(op2(e23,e23),e22)**. % 0.77/0.96 722[0:Inp] || -> equal(op2(e23,e20),e22) equal(op2(e23,e21),e22) equal(op2(e23,e22),e22) equal(op2(e23,e23),e22)**. % 0.77/0.96 731[0:Inp] || -> equal(op2(e20,e22),e21) equal(op2(e21,e22),e21) equal(op2(e22,e22),e21) equal(op2(e23,e22),e21)**. % 0.77/0.96 734[0:Inp] || -> equal(op2(e22,e20),e20) equal(op2(e22,e21),e20) equal(op2(e22,e22),e20) equal(op2(e22,e23),e20)**. % 0.77/0.96 735[0:Inp] || -> equal(op2(e20,e21),e23) equal(op2(e21,e21),e23) equal(op2(e22,e21),e23) equal(op2(e23,e21),e23)**. % 0.77/0.96 736[0:Inp] || -> equal(op2(e21,e20),e23) equal(op2(e21,e21),e23) equal(op2(e21,e22),e23) equal(op2(e21,e23),e23)**. % 0.77/0.96 738[0:Inp] || -> equal(op2(e21,e20),e22) equal(op2(e21,e21),e22) equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.77/0.96 740[0:Inp] || -> equal(op2(e21,e20),e21) equal(op2(e21,e21),e21) equal(op2(e21,e22),e21) equal(op2(e21,e23),e21)**. % 0.77/0.96 742[0:Inp] || -> equal(op2(e21,e20),e20) equal(op2(e21,e21),e20) equal(op2(e21,e22),e20) equal(op2(e21,e23),e20)**. % 0.77/0.96 744[0:Inp] || -> equal(op2(e20,e20),e23) equal(op2(e20,e21),e23) equal(op2(e20,e22),e23) equal(op2(e20,e23),e23)**. % 0.77/0.96 750[0:Inp] || -> equal(op2(e20,e20),e20) equal(op2(e20,e21),e20) equal(op2(e20,e22),e20) equal(op2(e20,e23),e20)**. % 0.77/0.96 751[0:Inp] || -> equal(op2(e23,e23),e20) equal(op2(e23,e23),e21) equal(op2(e23,e23),e22) equal(op2(e23,e23),e23)**. % 0.77/0.96 752[0:Inp] || -> equal(op2(e23,e22),e23)** equal(op2(e23,e22),e22) equal(op2(e23,e22),e21) equal(op2(e23,e22),e20). % 0.77/0.96 753[0:Inp] || -> equal(op2(e23,e21),e20) equal(op2(e23,e21),e21) equal(op2(e23,e21),e22) equal(op2(e23,e21),e23)**. % 0.77/0.96 755[0:Inp] || -> equal(op2(e22,e23),e20) equal(op2(e22,e23),e21) equal(op2(e22,e23),e22) equal(op2(e22,e23),e23)**. % 0.77/0.96 756[0:Inp] || -> equal(op2(e22,e22),e20) equal(op2(e22,e22),e21) equal(op2(e22,e22),e22) equal(op2(e22,e22),e23)**. % 0.77/0.96 761[0:Inp] || -> equal(op2(e21,e21),e20) equal(op2(e21,e21),e21) equal(op2(e21,e21),e22) equal(op2(e21,e21),e23)**. % 0.77/0.96 762[0:Inp] || -> equal(op2(e21,e20),e20) equal(op2(e21,e20),e21) equal(op2(e21,e20),e22) equal(op2(e21,e20),e23)**. % 0.77/0.96 763[0:Inp] || -> equal(op2(e20,e23),e20) equal(op2(e20,e23),e21) equal(op2(e20,e23),e22) equal(op2(e20,e23),e23)**. % 0.77/0.96 767[0:Inp] || -> equal(op1(e10,e13),e13) equal(op1(e11,e13),e13) equal(op1(e12,e13),e13) equal(op1(e13,e13),e13)**. % 0.77/0.96 769[0:Inp] || -> equal(op1(e10,e13),e12) equal(op1(e11,e13),e12) equal(op1(e12,e13),e12) equal(op1(e13,e13),e12)**. % 0.77/0.96 770[0:Inp] || -> equal(op1(e13,e10),e12) equal(op1(e13,e11),e12) equal(op1(e13,e12),e12) equal(op1(e13,e13),e12)**. % 0.77/0.96 771[0:Inp] || -> equal(op1(e10,e13),e11) equal(op1(e11,e13),e11) equal(op1(e12,e13),e11) equal(op1(e13,e13),e11)**. % 0.77/0.96 772[0:Inp] || -> equal(op1(e13,e10),e11) equal(op1(e13,e11),e11) equal(op1(e13,e12),e11) equal(op1(e13,e13),e11)**. % 0.77/0.96 775[0:Inp] || -> equal(op1(e10,e12),e13) equal(op1(e11,e12),e13) equal(op1(e12,e12),e13) equal(op1(e13,e12),e13)**. % 0.77/0.96 777[0:Inp] || -> equal(op1(e10,e12),e12) equal(op1(e11,e12),e12) equal(op1(e12,e12),e12) equal(op1(e13,e12),e12)**. % 0.77/0.96 779[0:Inp] || -> equal(op1(e10,e12),e11) equal(op1(e11,e12),e11) equal(op1(e12,e12),e11) equal(op1(e13,e12),e11)**. % 0.77/0.96 782[0:Inp] || -> equal(op1(e12,e10),e10) equal(op1(e12,e11),e10) equal(op1(e12,e12),e10) equal(op1(e12,e13),e10)**. % 0.77/0.96 783[0:Inp] || -> equal(op1(e10,e11),e13) equal(op1(e11,e11),e13) equal(op1(e12,e11),e13) equal(op1(e13,e11),e13)**. % 0.77/0.96 786[0:Inp] || -> equal(op1(e11,e10),e12) equal(op1(e11,e11),e12) equal(op1(e11,e12),e12) equal(op1(e11,e13),e12)**. % 0.77/0.96 787[0:Inp] || -> equal(op1(e10,e11),e11) equal(op1(e11,e11),e11) equal(op1(e12,e11),e11) equal(op1(e13,e11),e11)**. % 0.77/0.96 788[0:Inp] || -> equal(op1(e11,e10),e11) equal(op1(e11,e11),e11) equal(op1(e11,e12),e11) equal(op1(e11,e13),e11)**. % 0.77/0.96 790[0:Inp] || -> equal(op1(e11,e11),e10) equal(op1(e11,e10),e10) equal(op1(e11,e13),e10)** equal(op1(e11,e12),e10). % 0.77/0.96 792[0:Inp] || -> equal(op1(e10,e10),e13) equal(op1(e10,e11),e13) equal(op1(e10,e12),e13) equal(op1(e10,e13),e13)**. % 0.77/0.96 793[0:Inp] || -> equal(op1(e10,e10),e12) equal(op1(e11,e10),e12) equal(op1(e12,e10),e12) equal(op1(e13,e10),e12)**. % 0.77/0.96 798[0:Inp] || -> equal(op1(e10,e10),e10) equal(op1(e10,e11),e10) equal(op1(e10,e12),e10) equal(op1(e10,e13),e10)**. % 0.77/0.96 799[0:Inp] || -> equal(op1(e13,e13),e13)** equal(op1(e13,e13),e12) equal(op1(e13,e13),e11) equal(op1(e13,e13),e10). % 0.77/0.96 800[0:Inp] || -> equal(op1(e13,e12),e13)** equal(op1(e13,e12),e12) equal(op1(e13,e12),e11) equal(op1(e13,e12),e10). % 0.77/0.96 803[0:Inp] || -> equal(op1(e12,e13),e10) equal(op1(e12,e13),e11) equal(op1(e12,e13),e12) equal(op1(e12,e13),e13)**. % 0.77/0.96 805[0:Inp] || -> equal(op1(e12,e11),e10) equal(op1(e12,e11),e11) equal(op1(e12,e11),e12) equal(op1(e12,e11),e13)**. % 0.77/0.96 807[0:Inp] || -> equal(op1(e11,e13),e13)** equal(op1(e11,e13),e11) equal(op1(e11,e13),e12) equal(op1(e11,e13),e10). % 0.77/0.96 809[0:Inp] || -> equal(op1(e11,e11),e10) equal(op1(e11,e11),e11) equal(op1(e11,e11),e12) equal(op1(e11,e11),e13)**. % 0.77/0.96 810[0:Inp] || -> equal(op1(e11,e10),e10) equal(op1(e11,e10),e11) equal(op1(e11,e10),e12) equal(op1(e11,e10),e13)**. % 0.77/0.96 811[0:Inp] || -> equal(op1(e10,e13),e10) equal(op1(e10,e13),e11) equal(op1(e10,e13),e12) equal(op1(e10,e13),e13)**. % 0.77/0.96 815[0:Inp] || -> equal(op2(e23,e23),e23)** SkC69 SkC70 SkC71 SkC72 SkC73 SkC74 SkC75 SkC76 SkC77 SkC78 SkC79 SkC80 SkC81 SkC82 SkC83 SkC84 SkC85 SkC86 SkC87 SkC88 SkC89 SkC90 SkC91 SkC92 SkC93 SkC94 SkC95 SkC96 SkC97 SkC98 SkC99 SkC100 SkC101 SkC102 SkC103 SkC104 SkC105 SkC106 SkC107 SkC108 SkC109 SkC110 SkC111 SkC112 SkC113 SkC114 SkC115 SkC116 SkC117 SkC118 SkC119 SkC120 SkC121 SkC122 SkC123 SkC124 SkC125 SkC126 SkC127 SkC128 SkC129 SkC130 SkC131. % 0.77/0.96 816[0:Inp] || -> equal(op1(e13,e13),e13)** SkC3 SkC4 SkC5 SkC6 SkC7 SkC8 SkC9 SkC10 SkC11 SkC12 SkC13 SkC14 SkC15 SkC16 SkC17 SkC18 SkC19 SkC20 SkC21 SkC22 SkC23 SkC24 SkC25 SkC26 SkC27 SkC28 SkC29 SkC30 SkC31 SkC32 SkC33 SkC34 SkC35 SkC36 SkC37 SkC38 SkC39 SkC40 SkC41 SkC42 SkC43 SkC44 SkC45 SkC46 SkC47 SkC48 SkC49 SkC50 SkC51 SkC52 SkC53 SkC54 SkC55 SkC56 SkC57 SkC58 SkC59 SkC60 SkC61 SkC62 SkC63 SkC64 SkC65. % 0.77/0.96 817[0:Inp] || equal(op2(e23,e23),e23)** -> SkC69 SkC70 SkC71 SkC72 SkC73 SkC74 SkC75 SkC76 SkC77 SkC78 SkC79 SkC80 SkC81 SkC82 SkC83 SkC84 SkC85 SkC86 SkC87 SkC88 SkC89 SkC90 SkC91 SkC92 SkC93 SkC94 SkC95 SkC96 SkC97 SkC98 SkC99 SkC100 SkC101 SkC102 SkC103 SkC104 SkC105 SkC106 SkC107 SkC108 SkC109 SkC110 SkC111 SkC112 SkC113 SkC114 SkC115 SkC116 SkC117 SkC118 SkC119 SkC120 SkC121 SkC122 SkC123 SkC124 SkC125 SkC126 SkC127 SkC128 SkC129 SkC130 SkC131. % 0.77/0.96 818[0:Inp] || equal(op1(e13,e13),e13)** -> SkC3 SkC4 SkC5 SkC6 SkC7 SkC8 SkC9 SkC10 SkC11 SkC12 SkC13 SkC14 SkC15 SkC16 SkC17 SkC18 SkC19 SkC20 SkC21 SkC22 SkC23 SkC24 SkC25 SkC26 SkC27 SkC28 SkC29 SkC30 SkC31 SkC32 SkC33 SkC34 SkC35 SkC36 SkC37 SkC38 SkC39 SkC40 SkC41 SkC42 SkC43 SkC44 SkC45 SkC46 SkC47 SkC48 SkC49 SkC50 SkC51 SkC52 SkC53 SkC54 SkC55 SkC56 SkC57 SkC58 SkC59 SkC60 SkC61 SkC62 SkC63 SkC64 SkC65. % 0.77/0.96 822[0:Inp] || equal(h4(e10),e23) equal(op2(h4(e10),h4(e10)),h4(op1(e10,e10))) equal(op2(h4(e10),h4(e11)),h4(op1(e10,e11))) equal(op2(h4(e10),h4(e12)),h4(op1(e10,e12))) equal(op2(h4(e10),h4(e13)),h4(op1(e10,e13))) equal(op2(h4(e11),h4(e10)),h4(op1(e11,e10))) equal(op2(h4(e11),h4(e11)),h4(op1(e11,e11))) equal(op2(h4(e11),h4(e12)),h4(op1(e11,e12))) equal(op2(h4(e11),h4(e13)),h4(op1(e11,e13))) equal(op2(h4(e12),h4(e10)),h4(op1(e12,e10))) equal(op2(h4(e12),h4(e11)),h4(op1(e12,e11))) equal(op2(h4(e12),h4(e12)),h4(op1(e12,e12))) equal(op2(h4(e12),h4(e13)),h4(op1(e12,e13))) equal(op2(h4(e13),h4(e10)),h4(op1(e13,e10))) equal(op2(h4(e13),h4(e11)),h4(op1(e13,e11))) equal(op2(h4(e13),h4(e12)),h4(op1(e13,e12))) equal(op2(h4(e13),h4(e13)),h4(op1(e13,e13)))** SkC141 SkC142 SkC143 -> . % 0.77/0.96 829[0:Inp] || equal(h2(e11),e23) equal(op2(h2(e10),h2(e10)),h2(op1(e10,e10))) equal(op2(h2(e10),h2(e11)),h2(op1(e10,e11))) equal(op2(h2(e10),h2(e12)),h2(op1(e10,e12))) equal(op2(h2(e10),h2(e13)),h2(op1(e10,e13))) equal(op2(h2(e11),h2(e10)),h2(op1(e11,e10))) equal(op2(h2(e11),h2(e11)),h2(op1(e11,e11))) equal(op2(h2(e11),h2(e12)),h2(op1(e11,e12))) equal(op2(h2(e11),h2(e13)),h2(op1(e11,e13))) equal(op2(h2(e12),h2(e10)),h2(op1(e12,e10))) equal(op2(h2(e12),h2(e11)),h2(op1(e12,e11))) equal(op2(h2(e12),h2(e12)),h2(op1(e12,e12))) equal(op2(h2(e12),h2(e13)),h2(op1(e12,e13))) equal(op2(h2(e13),h2(e10)),h2(op1(e13,e10))) equal(op2(h2(e13),h2(e11)),h2(op1(e13,e11))) equal(op2(h2(e13),h2(e12)),h2(op1(e13,e12))) equal(op2(h2(e13),h2(e13)),h2(op1(e13,e13)))** SkC135 SkC136 SkC137 -> . % 0.77/0.96 831[0:Inp] || equal(h1(e13),e23) equal(op2(h1(e10),h1(e10)),h1(op1(e10,e10))) equal(op2(h1(e10),h1(e11)),h1(op1(e10,e11))) equal(op2(h1(e10),h1(e12)),h1(op1(e10,e12))) equal(op2(h1(e10),h1(e13)),h1(op1(e10,e13))) equal(op2(h1(e11),h1(e10)),h1(op1(e11,e10))) equal(op2(h1(e11),h1(e11)),h1(op1(e11,e11))) equal(op2(h1(e11),h1(e12)),h1(op1(e11,e12))) equal(op2(h1(e11),h1(e13)),h1(op1(e11,e13))) equal(op2(h1(e12),h1(e10)),h1(op1(e12,e10))) equal(op2(h1(e12),h1(e11)),h1(op1(e12,e11))) equal(op2(h1(e12),h1(e12)),h1(op1(e12,e12))) equal(op2(h1(e12),h1(e13)),h1(op1(e12,e13))) equal(op2(h1(e13),h1(e10)),h1(op1(e13,e10))) equal(op2(h1(e13),h1(e11)),h1(op1(e13,e11))) equal(op2(h1(e13),h1(e12)),h1(op1(e13,e12))) equal(op2(h1(e13),h1(e13)),h1(op1(e13,e13)))** SkC132 SkC133 SkC134 -> . % 0.77/0.96 835[0:Rew:34.0,83.0] || -> equal(h1(e11),e21)**. % 0.77/0.96 844[0:Rew:30.0,51.0] || equal(e21,e21) -> SkC136*. % 0.77/0.96 845[0:Obv:844.0] || -> SkC136*. % 0.77/0.96 849[0:Rew:835.0,40.0] || equal(e21,e21) -> SkC133*. % 0.77/0.96 850[0:Obv:849.0] || -> SkC133*. % 0.77/0.96 852[0:Rew:29.0,35.0] || equal(e20,e20) -> SkC132*. % 0.77/0.96 853[0:Obv:852.0] || -> SkC132*. % 0.77/0.96 854[0:Rew:34.0,340.0] || -> equal(op2(e20,e21),e22)**. % 0.77/0.96 855[0:Rew:33.0,339.0] || -> equal(op1(e10,e11),e12)**. % 0.77/0.96 857[0:Rew:86.0,337.1] || SkC131 -> equal(h4(e11),e23)**. % 0.77/0.96 859[0:Rew:86.0,335.1] || SkC130 -> equal(h4(e11),e23)**. % 0.77/0.96 860[0:Rew:34.0,334.1] || SkC129* -> equal(e23,e21). % 0.77/0.96 861[0:MRR:860.1,11.0] || SkC129* -> . % 0.77/0.96 863[0:Rew:85.0,330.1] || SkC127 -> equal(h3(e11),e22)**. % 0.77/0.96 864[0:Rew:84.0,328.1] || SkC126 -> equal(h2(e11),e22)**. % 0.77/0.96 865[0:Rew:34.0,326.1] || SkC125* -> equal(e22,e21). % 0.77/0.96 866[0:MRR:865.1,10.0] || SkC125* -> . % 0.77/0.96 868[0:Rew:85.0,322.1] || SkC123 -> equal(h3(e11),e21)**. % 0.77/0.96 869[0:Rew:84.0,320.1] || SkC122 -> equal(h2(e11),e21)**. % 0.77/0.96 873[0:Rew:34.0,310.1] || SkC117* -> equal(e21,e20). % 0.77/0.96 874[0:MRR:873.1,7.0] || SkC117* -> . % 0.77/0.96 875[0:Rew:86.0,308.1] || SkC116 -> equal(h4(e11),e23)**. % 0.77/0.96 878[0:Rew:34.0,302.1] || SkC113* -> equal(e23,e21). % 0.77/0.96 879[0:MRR:878.1,11.0] || SkC113* -> . % 0.77/0.96 881[0:Rew:85.0,299.1] || SkC112 -> equal(h3(e11),e22)**. % 0.77/0.96 882[0:Rew:85.0,298.1] || SkC111 -> equal(h3(e11),e22)**. % 0.77/0.96 884[0:Rew:85.0,296.1] || SkC110 -> equal(h3(e11),e22)**. % 0.77/0.96 885[0:Rew:34.0,295.1] || SkC109* -> equal(e22,e21). % 0.77/0.96 886[0:MRR:885.1,10.0] || SkC109* -> . % 0.77/0.96 889[0:Rew:84.0,289.1] || SkC106 -> equal(h2(e11),e21)**. % 0.77/0.96 893[0:Rew:34.0,279.1] || SkC101* -> equal(e21,e20). % 0.77/0.96 894[0:MRR:893.1,7.0] || SkC101* -> . % 0.77/0.96 895[0:Rew:86.0,277.1] || SkC100 -> equal(h4(e11),e23)**. % 0.77/0.96 896[0:Rew:85.0,275.1] || SkC99 -> equal(h3(e11),e23)**. % 0.77/0.96 898[0:Rew:34.0,271.1] || SkC97* -> equal(e23,e21). % 0.77/0.96 899[0:MRR:898.1,11.0] || SkC97* -> . % 0.77/0.96 900[0:Rew:86.0,269.1] || SkC96 -> equal(h4(e11),e22)**. % 0.77/0.96 901[0:Rew:85.0,267.1] || SkC95 -> equal(h3(e11),e22)**. % 0.77/0.96 903[0:Rew:34.0,263.1] || SkC93* -> equal(e22,e21). % 0.77/0.96 904[0:MRR:903.1,10.0] || SkC93* -> . % 0.77/0.96 906[0:Rew:84.0,260.1] || SkC92 -> equal(h2(e11),e21)**. % 0.77/0.96 908[0:Rew:84.0,258.1] || SkC91 -> equal(h2(e11),e21)**. % 0.77/0.96 909[0:Rew:84.0,257.1] || SkC90 -> equal(h2(e11),e21)**. % 0.77/0.96 910[0:Rew:84.0,255.1] || SkC89 -> equal(h2(e11),e21)**. % 0.77/0.96 914[0:Rew:34.0,248.1] || SkC85* -> equal(e21,e20). % 0.77/0.96 915[0:MRR:914.1,7.0] || SkC85* -> . % 0.77/0.96 916[0:Rew:86.0,246.1] || SkC84 -> equal(h4(e11),e23)**. % 0.77/0.96 917[0:Rew:85.0,244.1] || SkC83 -> equal(h3(e11),e23)**. % 0.77/0.96 919[0:Rew:34.0,240.1] || SkC81* -> equal(e23,e21). % 0.77/0.96 920[0:MRR:919.1,11.0] || SkC81* -> . % 0.77/0.96 921[0:Rew:86.0,238.1] || SkC80 -> equal(h4(e11),e22)**. % 0.77/0.96 922[0:Rew:85.0,236.1] || SkC79 -> equal(h3(e11),e22)**. % 0.77/0.96 923[0:Rew:84.0,234.1] || SkC78 -> equal(h2(e11),e22)**. % 0.77/0.96 924[0:Rew:34.0,232.1] || SkC77* -> equal(e22,e21). % 0.77/0.96 925[0:MRR:924.1,10.0] || SkC77* -> . % 0.77/0.96 927[0:Rew:854.0,229.1] || SkC76* -> equal(e22,e20). % 0.77/0.96 928[0:MRR:927.1,8.0] || SkC76* -> . % 0.77/0.96 930[0:Rew:854.0,227.1] || SkC75* -> equal(e22,e20). % 0.77/0.96 931[0:MRR:930.1,8.0] || SkC75* -> . % 0.77/0.96 933[0:Rew:854.0,225.1] || SkC74* -> equal(e22,e20). % 0.77/0.96 934[0:MRR:933.1,8.0] || SkC74* -> . % 0.77/0.96 935[0:Rew:854.0,223.1] || SkC73* -> equal(e22,e20). % 0.77/0.96 936[0:MRR:935.1,8.0] || SkC73* -> . % 0.77/0.96 938[0:Rew:34.0,221.1] || SkC72* -> equal(e21,e20). % 0.77/0.96 939[0:MRR:938.1,7.0] || SkC72* -> . % 0.77/0.96 941[0:Rew:34.0,219.1] || SkC71* -> equal(e21,e20). % 0.77/0.96 942[0:MRR:941.1,7.0] || SkC71* -> . % 0.77/0.96 944[0:Rew:34.0,217.1] || SkC70* -> equal(e21,e20). % 0.77/0.96 945[0:MRR:944.1,7.0] || SkC70* -> . % 0.77/0.96 946[0:Rew:34.0,216.1] || SkC69* -> equal(e21,e20). % 0.77/0.96 947[0:MRR:946.1,7.0] || SkC69* -> . % 0.77/0.96 948[0:Rew:85.0,215.1] || SkC68 -> equal(h3(e11),e22)**. % 0.77/0.96 950[0:Rew:34.0,213.1] || SkC66* -> equal(e21,e20). % 0.77/0.96 951[0:MRR:950.1,7.0] || SkC66* -> . % 0.77/0.96 952[0:Rew:33.0,208.1] || SkC63* -> equal(e13,e11). % 0.77/0.96 953[0:MRR:952.1,5.0] || SkC63* -> . % 0.77/0.96 954[0:Rew:33.0,200.1] || SkC59* -> equal(e12,e11). % 0.77/0.96 955[0:MRR:954.1,4.0] || SkC59* -> . % 0.77/0.96 956[0:Rew:33.0,184.1] || SkC51* -> equal(e11,e10). % 0.77/0.96 957[0:MRR:956.1,1.0] || SkC51* -> . % 0.77/0.96 958[0:Rew:33.0,176.1] || SkC47* -> equal(e13,e11). % 0.77/0.96 959[0:MRR:958.1,5.0] || SkC47* -> . % 0.77/0.96 960[0:Rew:33.0,169.1] || SkC43* -> equal(e12,e11). % 0.77/0.96 961[0:MRR:960.1,4.0] || SkC43* -> . % 0.77/0.96 962[0:Rew:33.0,153.1] || SkC35* -> equal(e11,e10). % 0.77/0.96 963[0:MRR:962.1,1.0] || SkC35* -> . % 0.77/0.96 964[0:Rew:33.0,145.1] || SkC31* -> equal(e13,e11). % 0.77/0.96 965[0:MRR:964.1,5.0] || SkC31* -> . % 0.77/0.96 966[0:Rew:33.0,137.1] || SkC27* -> equal(e12,e11). % 0.77/0.96 967[0:MRR:966.1,4.0] || SkC27* -> . % 0.77/0.96 968[0:Rew:33.0,122.1] || SkC19* -> equal(e11,e10). % 0.77/0.96 969[0:MRR:968.1,1.0] || SkC19* -> . % 0.77/0.96 970[0:Rew:33.0,114.1] || SkC15* -> equal(e13,e11). % 0.77/0.96 971[0:MRR:970.1,5.0] || SkC15* -> . % 0.77/0.96 972[0:Rew:33.0,106.1] || SkC11* -> equal(e12,e11). % 0.77/0.96 973[0:MRR:972.1,4.0] || SkC11* -> . % 0.77/0.96 974[0:Rew:855.0,103.1] || SkC10* -> equal(e12,e10). % 0.77/0.96 975[0:MRR:974.1,2.0] || SkC10* -> . % 0.77/0.96 976[0:Rew:855.0,101.1] || SkC9* -> equal(e12,e10). % 0.77/0.96 977[0:MRR:976.1,2.0] || SkC9* -> . % 0.77/0.96 978[0:Rew:855.0,99.1] || SkC8* -> equal(e12,e10). % 0.77/0.96 979[0:MRR:978.1,2.0] || SkC8* -> . % 0.77/0.96 980[0:Rew:855.0,97.1] || SkC7* -> equal(e12,e10). % 0.77/0.96 981[0:MRR:980.1,2.0] || SkC7* -> . % 0.77/0.96 982[0:Rew:33.0,95.1] || SkC6* -> equal(e11,e10). % 0.77/0.96 983[0:MRR:982.1,1.0] || SkC6* -> . % 0.77/0.96 984[0:Rew:33.0,93.1] || SkC5* -> equal(e11,e10). % 0.77/0.96 985[0:MRR:984.1,1.0] || SkC5* -> . % 0.77/0.96 986[0:Rew:33.0,91.1] || SkC4* -> equal(e11,e10). % 0.77/0.96 987[0:MRR:986.1,1.0] || SkC4* -> . % 0.77/0.96 988[0:Rew:33.0,90.1] || SkC3* -> equal(e11,e10). % 0.77/0.96 989[0:MRR:988.1,1.0] || SkC3* -> . % 0.77/0.96 990[0:Rew:33.0,87.1] || SkC0* -> equal(e11,e10). % 0.77/0.96 991[0:MRR:990.1,1.0] || SkC0* -> . % 0.77/0.96 992[0:Rew:86.0,688.0] || -> equal(op2(e23,h4(e11)),h4(e12))**. % 0.77/0.96 994[0:Rew:84.0,686.0] || -> equal(op2(e21,h2(e11)),h2(e12))**. % 0.77/0.96 995[0:Rew:854.0,685.0,34.0,685.0] || -> equal(h1(e12),e22)**. % 0.77/0.96 996[0:Rew:995.0,45.0] || equal(e22,e22) -> SkC134*. % 0.77/0.96 997[0:Obv:996.0] || -> SkC134*. % 0.77/0.96 998[0:Rew:857.1,683.0,86.0,683.0] || equal(e23,e23) SkC131* -> . % 0.77/0.96 999[0:Obv:998.0] || SkC131* -> . % 0.77/0.96 1000[0:Rew:859.1,681.0,86.0,681.0] || equal(e23,e23) SkC130* -> . % 0.77/0.96 1001[0:Obv:1000.0] || SkC130* -> . % 0.77/0.96 1002[0:Rew:331.1,678.0] || equal(e23,e23) SkC128* -> . % 0.77/0.96 1003[0:Obv:1002.0] || SkC128* -> . % 0.77/0.96 1004[0:Rew:863.1,676.0,85.0,676.0] || equal(e22,e22) SkC127* -> . % 0.77/0.96 1005[0:Obv:1004.0] || SkC127* -> . % 0.77/0.96 1007[0:Rew:323.1,670.0] || equal(e23,e23) SkC124* -> . % 0.77/0.96 1008[0:Obv:1007.0] || SkC124* -> . % 0.77/0.96 1010[0:Rew:869.1,666.0,84.0,666.0] || equal(e21,e21) SkC122* -> . % 0.77/0.96 1011[0:Obv:1010.0] || SkC122* -> . % 0.77/0.96 1013[0:Rew:86.0,663.0] || SkC121 equal(h4(e11),e21)** -> . % 0.77/0.96 1014[0:Rew:315.1,662.0] || equal(e23,e23) SkC120* -> . % 0.77/0.96 1015[0:Obv:1014.0] || SkC120* -> . % 0.77/0.96 1018[0:Rew:875.1,654.0,86.0,654.0] || equal(e23,e23) SkC116* -> . % 0.77/0.96 1019[0:Obv:1018.0] || SkC116* -> . % 0.77/0.96 1020[0:Rew:305.1,652.0] || equal(e22,e22) SkC115* -> . % 0.77/0.96 1021[0:Obv:1020.0] || SkC115* -> . % 0.77/0.96 1023[0:Rew:881.1,645.0,85.0,645.0] || equal(e22,e22) SkC112* -> . % 0.77/0.96 1024[0:Obv:1023.0] || SkC112* -> . % 0.77/0.96 1025[0:Rew:882.1,644.0,85.0,644.0] || equal(e22,e22) SkC111* -> . % 0.77/0.96 1026[0:Obv:1025.0] || SkC111* -> . % 0.77/0.96 1027[0:Rew:884.1,642.0,85.0,642.0] || equal(e22,e22) SkC110* -> . % 0.77/0.96 1028[0:Obv:1027.0] || SkC110* -> . % 0.77/0.96 1030[0:Rew:290.1,637.0] || equal(e22,e22) SkC107* -> . % 0.77/0.96 1031[0:Obv:1030.0] || SkC107* -> . % 0.77/0.96 1032[0:Rew:889.1,635.0,84.0,635.0] || equal(e21,e21) SkC106* -> . % 0.77/0.96 1033[0:Obv:1032.0] || SkC106* -> . % 0.77/0.96 1037[0:Rew:282.1,629.0] || equal(e22,e22) SkC103* -> . % 0.77/0.96 1038[0:Obv:1037.0] || SkC103* -> . % 0.77/0.96 1040[0:Rew:895.1,623.0,86.0,623.0] || equal(e23,e23) SkC100* -> . % 0.77/0.96 1041[0:Obv:1040.0] || SkC100* -> . % 0.77/0.96 1043[0:Rew:272.1,619.0] || equal(e21,e21) SkC98* -> . % 0.77/0.96 1044[0:Obv:1043.0] || SkC98* -> . % 0.77/0.96 1046[0:Rew:901.1,613.0,85.0,613.0] || equal(e22,e22) SkC95* -> . % 0.77/0.96 1047[0:Obv:1046.0] || SkC95* -> . % 0.77/0.96 1048[0:Rew:264.1,611.0] || equal(e21,e21) SkC94* -> . % 0.77/0.96 1049[0:Obv:1048.0] || SkC94* -> . % 0.77/0.96 1050[0:Rew:906.1,606.0,84.0,606.0] || equal(e21,e21) SkC92* -> . % 0.77/0.96 1051[0:Obv:1050.0] || SkC92* -> . % 0.77/0.96 1052[0:Rew:908.1,604.0,84.0,604.0] || equal(e21,e21) SkC91* -> . % 0.77/0.96 1053[0:Obv:1052.0] || SkC91* -> . % 0.77/0.96 1054[0:Rew:909.1,603.0,84.0,603.0] || equal(e21,e21) SkC90* -> . % 0.77/0.96 1055[0:Obv:1054.0] || SkC90* -> . % 0.77/0.96 1057[0:Rew:910.1,601.0,84.0,601.0] || equal(e21,e21) SkC89* -> . % 0.77/0.96 1058[0:Obv:1057.0] || SkC89* -> . % 0.77/0.96 1061[0:Rew:249.1,596.0] || equal(e21,e21) SkC86* -> . % 0.77/0.96 1062[0:Obv:1061.0] || SkC86* -> . % 0.77/0.96 1063[0:Rew:916.1,592.0,86.0,592.0] || equal(e23,e23) SkC84* -> . % 0.77/0.96 1064[0:Obv:1063.0] || SkC84* -> . % 0.77/0.96 1068[0:Rew:922.1,582.0,85.0,582.0] || equal(e22,e22) SkC79* -> . % 0.77/0.96 1069[0:Obv:1068.0] || SkC79* -> . % 0.77/0.96 1071[0:Rew:86.0,561.0] || -> equal(h4(e11),e23)** SkC66 SkC67 SkC68. % 0.77/0.96 1072[0:MRR:1071.1,951.0] || -> equal(h4(e11),e23)** SkC67 SkC68. % 0.77/0.96 1073[0:Rew:211.1,559.0] || equal(e13,e13) SkC65* -> . % 0.77/0.96 1074[0:Obv:1073.0] || SkC65* -> . % 0.77/0.96 1075[0:Rew:209.1,557.0] || equal(e13,e13) SkC64* -> . % 0.77/0.96 1076[0:Obv:1075.0] || SkC64* -> . % 0.77/0.96 1077[0:Rew:205.1,554.0] || equal(e13,e13) SkC62* -> . % 0.77/0.96 1078[0:Obv:1077.0] || SkC62* -> . % 0.77/0.96 1079[0:Rew:204.1,552.0] || equal(e12,e12) SkC61* -> . % 0.77/0.96 1080[0:Obv:1079.0] || SkC61* -> . % 0.77/0.96 1081[0:Rew:197.1,546.0] || equal(e13,e13) SkC58* -> . % 0.77/0.96 1082[0:Obv:1081.0] || SkC58* -> . % 0.77/0.96 1083[0:Rew:194.1,542.0] || equal(e11,e11) SkC56* -> . % 0.77/0.96 1084[0:Obv:1083.0] || SkC56* -> . % 0.77/0.96 1086[0:Rew:189.1,538.0] || equal(e13,e13) SkC54* -> . % 0.77/0.96 1087[0:Obv:1086.0] || SkC54* -> . % 0.77/0.96 1088[0:Rew:182.1,530.0] || equal(e13,e13) SkC50* -> . % 0.77/0.96 1089[0:Obv:1088.0] || SkC50* -> . % 0.77/0.96 1090[0:Rew:179.1,528.0] || equal(e12,e12) SkC49* -> . % 0.77/0.96 1091[0:Obv:1090.0] || SkC49* -> . % 0.77/0.96 1092[0:Rew:173.1,521.0] || equal(e12,e12) SkC46* -> . % 0.77/0.96 1093[0:Obv:1092.0] || SkC46* -> . % 0.77/0.96 1094[0:Rew:172.1,520.0] || equal(e12,e12) SkC45* -> . % 0.77/0.96 1095[0:Obv:1094.0] || SkC45* -> . % 0.77/0.96 1096[0:Rew:170.1,518.0] || equal(e12,e12) SkC44* -> . % 0.77/0.96 1097[0:Obv:1096.0] || SkC44* -> . % 0.77/0.96 1098[0:Rew:164.1,513.0] || equal(e12,e12) SkC41* -> . % 0.77/0.96 1099[0:Obv:1098.0] || SkC41* -> . % 0.77/0.96 1100[0:Rew:163.1,511.0] || equal(e11,e11) SkC40* -> . % 0.77/0.96 1101[0:Obv:1100.0] || SkC40* -> . % 0.77/0.96 1103[0:Rew:156.1,505.0] || equal(e12,e12) SkC37* -> . % 0.77/0.96 1104[0:Obv:1103.0] || SkC37* -> . % 0.77/0.96 1105[0:Rew:151.1,499.0] || equal(e13,e13) SkC34* -> . % 0.77/0.96 1106[0:Obv:1105.0] || SkC34* -> . % 0.77/0.96 1107[0:Rew:146.1,495.0] || equal(e11,e11) SkC32* -> . % 0.77/0.96 1108[0:Obv:1107.0] || SkC32* -> . % 0.77/0.96 1109[0:Rew:141.1,489.0] || equal(e12,e12) SkC29* -> . % 0.77/0.96 1110[0:Obv:1109.0] || SkC29* -> . % 0.77/0.96 1111[0:Rew:138.1,487.0] || equal(e11,e11) SkC28* -> . % 0.77/0.96 1112[0:Obv:1111.0] || SkC28* -> . % 0.77/0.96 1113[0:Rew:134.1,482.0] || equal(e11,e11) SkC26* -> . % 0.77/0.96 1114[0:Obv:1113.0] || SkC26* -> . % 0.77/0.96 1115[0:Rew:132.1,480.0] || equal(e11,e11) SkC25* -> . % 0.77/0.96 1116[0:Obv:1115.0] || SkC25* -> . % 0.77/0.96 1117[0:Rew:131.1,479.0] || equal(e11,e11) SkC24* -> . % 0.77/0.96 1118[0:Obv:1117.0] || SkC24* -> . % 0.77/0.96 1120[0:Rew:129.1,477.0] || equal(e11,e11) SkC23* -> . % 0.77/0.96 1121[0:Obv:1120.0] || SkC23* -> . % 0.77/0.96 1122[0:Rew:123.1,472.0] || equal(e11,e11) SkC20* -> . % 0.77/0.96 1123[0:Obv:1122.0] || SkC20* -> . % 0.77/0.96 1124[0:Rew:120.1,468.0] || equal(e13,e13) SkC18* -> . % 0.77/0.96 1125[0:Obv:1124.0] || SkC18* -> . % 0.77/0.96 1129[0:Rew:110.1,458.0] || equal(e12,e12) SkC13* -> . % 0.77/0.96 1130[0:Obv:1129.0] || SkC13* -> . % 0.77/0.96 1132[0:MRR:437.1,991.0] || -> equal(op1(e13,e13),e13)** SkC1 SkC2. % 0.77/0.96 1133[0:Rew:86.0,436.0] || equal(op2(e23,e22),h4(e11))** -> . % 0.77/0.96 1134[0:Rew:86.0,435.0] || equal(op2(e23,e21),h4(e11))** -> . % 0.77/0.96 1136[0:Rew:85.0,430.0] || equal(op2(e22,e23),h3(e11))** -> . % 0.77/0.96 1138[0:Rew:85.0,426.0] || equal(op2(e22,e20),h3(e11))** -> . % 0.77/0.96 1140[0:Rew:84.0,422.0] || equal(op2(e21,e22),h2(e11))** -> . % 0.77/0.96 1141[0:Rew:84.0,419.0] || equal(op2(e21,e20),h2(e11))** -> . % 0.77/0.96 1142[0:Rew:854.0,417.0] || equal(op2(e20,e23),e22)** -> . % 0.77/0.96 1144[0:Rew:34.0,415.0] || equal(op2(e20,e23),e21)** -> . % 0.77/0.96 1145[0:Rew:34.0,414.0] || equal(op2(e20,e22),e21)** -> . % 0.77/0.96 1147[0:Rew:86.0,412.0] || equal(op2(e22,e23),h4(e11))** -> . % 0.77/0.96 1148[0:Rew:86.0,411.0] || equal(op2(e21,e23),h4(e11))** -> . % 0.77/0.96 1149[0:Rew:86.0,409.0] || equal(op2(e20,e23),h4(e11))** -> . % 0.77/0.96 1150[0:Rew:85.0,406.0] || equal(op2(e23,e22),h3(e11))** -> . % 0.77/0.96 1151[0:Rew:85.0,404.0] || equal(op2(e21,e22),h3(e11))** -> . % 0.77/0.96 1153[0:Rew:84.0,399.0] || equal(op2(e23,e21),h2(e11))** -> . % 0.77/0.96 1155[0:Rew:854.0,397.0] || equal(op2(e23,e21),e22)** -> . % 0.77/0.96 1156[0:Rew:854.0,396.0] || equal(op2(e22,e21),e22)** -> . % 0.77/0.96 1157[0:MRR:292.1,1156.0] || SkC108* -> . % 0.77/0.96 1158[0:MRR:286.1,1156.0] || SkC105* -> . % 0.77/0.96 1159[0:Rew:84.0,395.0,854.0,395.0] || equal(h2(e11),e22)** -> . % 0.77/0.96 1160[0:MRR:864.1,1159.0] || SkC126* -> . % 0.77/0.96 1161[0:MRR:923.1,1159.0] || SkC78* -> . % 0.77/0.96 1164[0:Rew:34.0,389.0] || equal(op2(e21,e20),e21)** -> . % 0.77/0.96 1165[0:MRR:253.1,1164.0] || SkC88* -> . % 0.77/0.96 1166[0:MRR:251.1,1164.0] || SkC87* -> . % 0.77/0.96 1167[0:Rew:855.0,369.0] || equal(op1(e10,e13),e12)** -> . % 0.77/0.96 1168[0:Rew:855.0,368.0] || equal(op1(e10,e12),e12)** -> . % 0.77/0.96 1169[0:Rew:33.0,367.0] || equal(op1(e10,e13),e11)** -> . % 0.77/0.96 1170[0:Rew:33.0,366.0] || equal(op1(e10,e12),e11)** -> . % 0.77/0.96 1172[0:Rew:855.0,349.0] || equal(op1(e13,e11),e12)** -> . % 0.77/0.96 1173[0:Rew:855.0,348.0] || equal(op1(e12,e11),e12)** -> . % 0.77/0.96 1174[0:MRR:166.1,1173.0] || SkC42* -> . % 0.77/0.96 1175[0:MRR:160.1,1173.0] || SkC39* -> . % 0.77/0.96 1176[0:Rew:855.0,347.0] || equal(op1(e11,e11),e12)** -> . % 0.77/0.96 1177[0:MRR:202.1,1176.0] || SkC60* -> . % 0.77/0.96 1178[0:MRR:108.1,1176.0] || SkC12* -> . % 0.77/0.96 1179[0:Rew:33.0,343.0] || equal(op1(e13,e10),e11)** -> . % 0.77/0.96 1181[0:Rew:33.0,341.0] || equal(op1(e11,e10),e11)** -> . % 0.77/0.96 1182[0:MRR:127.1,1181.0] || SkC22* -> . % 0.77/0.96 1183[0:MRR:125.1,1181.0] || SkC21* -> . % 0.77/0.96 1184[0:Rew:854.0,690.0,34.0,690.0] || -> equal(op2(e22,e20),e23)**. % 0.77/0.96 1186[0:Rew:1184.0,280.1] || SkC102* -> equal(e23,e22). % 0.77/0.96 1187[0:Rew:1184.0,284.1] || SkC104* -> equal(e23,e22). % 0.77/0.96 1188[0:Rew:1184.0,427.0] || equal(op2(e22,e23),e23)** -> . % 0.77/0.96 1189[0:Rew:1184.0,1138.0] || equal(h3(e11),e23)** -> . % 0.77/0.96 1190[0:Rew:1184.0,425.0] || equal(op2(e22,e21),e23)** -> . % 0.77/0.96 1191[0:Rew:1184.0,394.0] || equal(op2(e23,e20),e23)** -> . % 0.77/0.96 1192[0:Rew:1184.0,392.0] || equal(op2(e21,e20),e23)** -> . % 0.77/0.96 1194[0:MRR:1186.1,12.0] || SkC102* -> . % 0.77/0.96 1195[0:MRR:1187.1,12.0] || SkC104* -> . % 0.77/0.96 1196[0:MRR:896.1,1189.0] || SkC99* -> . % 0.77/0.96 1197[0:MRR:917.1,1189.0] || SkC83* -> . % 0.77/0.96 1198[0:MRR:313.1,1191.0] || SkC119* -> . % 0.77/0.96 1199[0:MRR:311.1,1191.0] || SkC118* -> . % 0.77/0.96 1200[0:Rew:855.0,689.0,33.0,689.0] || -> equal(op1(e12,e10),e13)**. % 0.77/0.96 1202[0:Rew:1200.0,154.1] || SkC36* -> equal(e13,e12). % 0.77/0.96 1203[0:Rew:1200.0,158.1] || SkC38* -> equal(e13,e12). % 0.77/0.96 1204[0:Rew:1200.0,379.0] || equal(op1(e12,e13),e13)** -> . % 0.77/0.96 1205[0:Rew:1200.0,378.0] || equal(op1(e12,e12),e13)** -> . % 0.77/0.96 1206[0:Rew:1200.0,377.0] || equal(op1(e12,e11),e13)** -> . % 0.77/0.96 1207[0:Rew:1200.0,346.0] || equal(op1(e13,e10),e13)** -> . % 0.77/0.96 1208[0:Rew:1200.0,344.0] || equal(op1(e11,e10),e13)** -> . % 0.77/0.96 1210[0:MRR:1202.1,6.0] || SkC36* -> . % 0.77/0.96 1211[0:MRR:1203.1,6.0] || SkC38* -> . % 0.77/0.96 1212[0:MRR:149.1,1205.0] || SkC33* -> . % 0.77/0.96 1213[0:MRR:118.1,1205.0] || SkC17* -> . % 0.77/0.96 1214[0:MRR:187.1,1207.0] || SkC53* -> . % 0.77/0.96 1215[0:MRR:185.1,1207.0] || SkC52* -> . % 0.77/0.96 1216[0:Rew:992.0,694.0,86.0,694.0] || -> equal(op2(h4(e12),e23),h4(e13))**. % 0.77/0.96 1218[0:Rew:994.0,692.0,84.0,692.0] || -> equal(op2(h2(e12),e21),h2(e13))**. % 0.77/0.96 1219[0:Rew:1184.0,691.0,854.0,691.0,34.0,691.0] || -> equal(h1(e13),e23)**. % 0.77/0.96 1220[0:Rew:86.0,712.0] || SkC68 equal(h4(e11),e22) -> equal(op2(e23,e22),e23)**. % 0.77/0.96 1226[0:Rew:854.0,707.2,34.0,707.0] || equal(e21,e21) SkC67* -> equal(e22,e20). % 0.77/0.96 1227[0:Obv:1226.0] || SkC67* -> equal(e22,e20). % 0.77/0.96 1228[0:MRR:1227.1,8.0] || SkC67* -> . % 0.77/0.96 1229[0:MRR:1072.1,1228.0] || -> SkC68 equal(h4(e11),e23)**. % 0.77/0.96 1232[0:Rew:855.0,698.2,33.0,698.0] || equal(e11,e11) SkC1* -> equal(e12,e10). % 0.77/0.96 1233[0:Obv:1232.0] || SkC1* -> equal(e12,e10). % 0.77/0.96 1234[0:MRR:1233.1,2.0] || SkC1* -> . % 0.77/0.96 1235[0:MRR:1132.1,1234.0] || -> SkC2 equal(op1(e13,e13),e13)**. % 0.77/0.96 1237[0:Rew:84.0,717.0] || equal(h2(e11),e23) -> equal(op2(e21,e23),e21)** SkC66 SkC67 SkC68. % 0.77/0.96 1238[0:MRR:1237.2,1237.3,951.0,1228.0] || equal(h2(e11),e23) -> SkC68 equal(op2(e21,e23),e21)**. % 0.77/0.96 1240[0:MRR:714.2,714.3,991.0,1234.0] || equal(op1(e11,e11),e13) -> SkC2 equal(op1(e11,e13),e11)**. % 0.77/0.96 1242[0:Rew:86.0,719.3] || -> equal(op2(e20,e23),e23) equal(op2(e21,e23),e23) equal(op2(e22,e23),e23)** equal(h4(e11),e23). % 0.77/0.96 1243[0:MRR:1242.2,1188.0] || -> equal(h4(e11),e23) equal(op2(e21,e23),e23)** equal(op2(e20,e23),e23). % 0.77/0.96 1246[0:Rew:86.0,721.3] || -> equal(op2(e20,e23),e22) equal(op2(e21,e23),e22) equal(op2(e22,e23),e22)** equal(h4(e11),e22). % 0.77/0.96 1247[0:MRR:1246.0,1142.0] || -> equal(h4(e11),e22) equal(op2(e22,e23),e22)** equal(op2(e21,e23),e22). % 0.77/0.96 1248[0:Rew:86.0,722.3] || -> equal(op2(e23,e20),e22) equal(op2(e23,e21),e22) equal(op2(e23,e22),e22)** equal(h4(e11),e22). % 0.77/0.96 1249[0:MRR:1248.1,1155.0] || -> equal(h4(e11),e22) equal(op2(e23,e22),e22)** equal(op2(e23,e20),e22). % 0.77/0.96 1262[0:Rew:85.0,731.2] || -> equal(op2(e20,e22),e21) equal(op2(e21,e22),e21) equal(h3(e11),e21) equal(op2(e23,e22),e21)**. % 0.77/0.96 1263[0:MRR:1262.0,1145.0] || -> equal(h3(e11),e21) equal(op2(e21,e22),e21) equal(op2(e23,e22),e21)**. % 0.77/0.96 1267[0:Rew:85.0,734.2,1184.0,734.0] || -> equal(e23,e20) equal(op2(e22,e21),e20) equal(h3(e11),e20) equal(op2(e22,e23),e20)**. % 0.77/0.96 1268[0:MRR:1267.0,9.0] || -> equal(h3(e11),e20) equal(op2(e22,e23),e20)** equal(op2(e22,e21),e20). % 0.77/0.96 1269[0:Rew:84.0,735.1,854.0,735.0] || -> equal(e23,e22) equal(h2(e11),e23) equal(op2(e22,e21),e23) equal(op2(e23,e21),e23)**. % 0.77/0.96 1270[0:MRR:1269.0,1269.2,12.0,1190.0] || -> equal(h2(e11),e23) equal(op2(e23,e21),e23)**. % 0.77/0.96 1271[0:Rew:84.0,736.1] || -> equal(op2(e21,e20),e23) equal(h2(e11),e23) equal(op2(e21,e22),e23) equal(op2(e21,e23),e23)**. % 0.77/0.96 1272[0:MRR:1271.0,1192.0] || -> equal(h2(e11),e23) equal(op2(e21,e23),e23)** equal(op2(e21,e22),e23). % 0.77/0.96 1273[0:Rew:84.0,738.1] || -> equal(op2(e21,e20),e22) equal(h2(e11),e22) equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.77/0.96 1274[0:MRR:1273.1,1159.0] || -> equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)** equal(op2(e21,e20),e22). % 0.77/0.96 1277[0:Rew:84.0,740.1] || -> equal(op2(e21,e20),e21) equal(h2(e11),e21) equal(op2(e21,e22),e21) equal(op2(e21,e23),e21)**. % 0.77/0.96 1278[0:MRR:1277.0,1164.0] || -> equal(h2(e11),e21) equal(op2(e21,e23),e21)** equal(op2(e21,e22),e21). % 0.77/0.96 1281[0:Rew:84.0,742.1] || -> equal(h2(e11),e20) equal(op2(e21,e20),e20) equal(op2(e21,e23),e20)** equal(op2(e21,e22),e20). % 0.77/0.96 1282[0:Rew:854.0,744.1,34.0,744.0] || -> equal(e23,e21) equal(e23,e22) equal(op2(e20,e22),e23) equal(op2(e20,e23),e23)**. % 0.77/0.96 1283[0:MRR:1282.0,1282.1,11.0,12.0] || -> equal(op2(e20,e23),e23)** equal(op2(e20,e22),e23). % 0.77/0.96 1288[0:Rew:854.0,750.1,34.0,750.0] || -> equal(e21,e20) equal(e22,e20) equal(op2(e20,e22),e20) equal(op2(e20,e23),e20)**. % 0.77/0.96 1289[0:MRR:1288.0,1288.1,7.0,8.0] || -> equal(op2(e20,e23),e20)** equal(op2(e20,e22),e20). % 0.77/0.96 1290[0:Rew:86.0,751.3,86.0,751.2,86.0,751.1,86.0,751.0] || -> equal(h4(e11),e23)** equal(h4(e11),e22) equal(h4(e11),e21) equal(h4(e11),e20). % 0.77/0.96 1291[0:MRR:753.2,1155.0] || -> equal(op2(e23,e21),e23)** equal(op2(e23,e21),e21) equal(op2(e23,e21),e20). % 0.77/0.96 1293[0:MRR:755.3,1188.0] || -> equal(op2(e22,e23),e22)** equal(op2(e22,e23),e21) equal(op2(e22,e23),e20). % 0.77/0.96 1294[0:Rew:85.0,756.3,85.0,756.2,85.0,756.1,85.0,756.0] || -> equal(h3(e11),e20) equal(h3(e11),e21) equal(h3(e11),e22) equal(h3(e11),e23)**. % 0.77/0.96 1295[0:MRR:1294.3,1189.0] || -> equal(h3(e11),e22)** equal(h3(e11),e21) equal(h3(e11),e20). % 0.77/0.96 1297[0:Rew:84.0,761.3,84.0,761.2,84.0,761.1,84.0,761.0] || -> equal(h2(e11),e20) equal(h2(e11),e21) equal(h2(e11),e22) equal(h2(e11),e23)**. % 0.77/0.96 1298[0:MRR:1297.2,1159.0] || -> equal(h2(e11),e23)** equal(h2(e11),e21) equal(h2(e11),e20). % 0.77/0.96 1299[0:MRR:762.1,762.3,1164.0,1192.0] || -> equal(op2(e21,e20),e20) equal(op2(e21,e20),e22)**. % 0.77/0.96 1300[0:MRR:763.1,763.2,1144.0,1142.0] || -> equal(op2(e20,e23),e23)** equal(op2(e20,e23),e20). % 0.77/0.96 1302[0:MRR:767.2,1204.0] || -> equal(op1(e13,e13),e13)** equal(op1(e11,e13),e13) equal(op1(e10,e13),e13). % 0.77/0.96 1304[0:MRR:769.0,1167.0] || -> equal(op1(e13,e13),e12)** equal(op1(e12,e13),e12) equal(op1(e11,e13),e12). % 0.77/0.96 1305[0:MRR:770.1,1172.0] || -> equal(op1(e13,e13),e12)** equal(op1(e13,e12),e12) equal(op1(e13,e10),e12). % 0.77/0.96 1306[0:MRR:771.0,1169.0] || -> equal(op1(e13,e13),e11)** equal(op1(e11,e13),e11) equal(op1(e12,e13),e11). % 0.77/0.96 1307[0:MRR:772.0,1179.0] || -> equal(op1(e13,e13),e11)** equal(op1(e13,e11),e11) equal(op1(e13,e12),e11). % 0.77/0.96 1308[0:MRR:775.2,1205.0] || -> equal(op1(e13,e12),e13)** equal(op1(e11,e12),e13) equal(op1(e10,e12),e13). % 0.77/0.96 1309[0:MRR:777.0,1168.0] || -> equal(op1(e12,e12),e12) equal(op1(e13,e12),e12)** equal(op1(e11,e12),e12). % 0.77/0.96 1312[0:MRR:779.0,1170.0] || -> equal(op1(e12,e12),e11) equal(op1(e11,e12),e11) equal(op1(e13,e12),e11)**. % 0.77/0.96 1315[0:Rew:1200.0,782.0] || -> equal(e13,e10) equal(op1(e12,e11),e10) equal(op1(e12,e12),e10) equal(op1(e12,e13),e10)**. % 0.77/0.96 1316[0:MRR:1315.0,3.0] || -> equal(op1(e12,e12),e10) equal(op1(e12,e13),e10)** equal(op1(e12,e11),e10). % 0.77/0.96 1317[0:Rew:855.0,783.0] || -> equal(e13,e12) equal(op1(e11,e11),e13) equal(op1(e12,e11),e13) equal(op1(e13,e11),e13)**. % 0.77/0.96 1318[0:MRR:1317.0,1317.2,6.0,1206.0] || -> equal(op1(e13,e11),e13)** equal(op1(e11,e11),e13). % 0.77/0.96 1320[0:MRR:786.1,1176.0] || -> equal(op1(e11,e12),e12) equal(op1(e11,e13),e12)** equal(op1(e11,e10),e12). % 0.77/0.96 1321[0:Rew:855.0,787.0] || -> equal(e12,e11) equal(op1(e11,e11),e11) equal(op1(e12,e11),e11) equal(op1(e13,e11),e11)**. % 0.77/0.96 1322[0:MRR:1321.0,4.0] || -> equal(op1(e11,e11),e11) equal(op1(e13,e11),e11)** equal(op1(e12,e11),e11). % 0.77/0.96 1323[0:MRR:788.0,1181.0] || -> equal(op1(e11,e11),e11) equal(op1(e11,e13),e11)** equal(op1(e11,e12),e11). % 0.77/0.96 1326[0:Rew:855.0,792.1,33.0,792.0] || -> equal(e13,e11) equal(e13,e12) equal(op1(e10,e12),e13) equal(op1(e10,e13),e13)**. % 0.77/0.96 1327[0:MRR:1326.0,1326.1,5.0,6.0] || -> equal(op1(e10,e13),e13)** equal(op1(e10,e12),e13). % 0.77/0.96 1328[0:Rew:1200.0,793.2,33.0,793.0] || -> equal(e12,e11) equal(op1(e11,e10),e12) equal(e13,e12) equal(op1(e13,e10),e12)**. % 0.77/0.96 1329[0:MRR:1328.0,1328.2,4.0,6.0] || -> equal(op1(e13,e10),e12)** equal(op1(e11,e10),e12). % 0.77/0.96 1332[0:Rew:855.0,798.1,33.0,798.0] || -> equal(e11,e10) equal(e12,e10) equal(op1(e10,e12),e10) equal(op1(e10,e13),e10)**. % 0.77/0.96 1333[0:MRR:1332.0,1332.1,1.0,2.0] || -> equal(op1(e10,e13),e10)** equal(op1(e10,e12),e10). % 0.77/0.96 1336[0:MRR:803.3,1204.0] || -> equal(op1(e12,e13),e12)** equal(op1(e12,e13),e11) equal(op1(e12,e13),e10). % 0.77/0.96 1338[0:MRR:805.2,805.3,1173.0,1206.0] || -> equal(op1(e12,e11),e11)** equal(op1(e12,e11),e10). % 0.77/0.96 1339[0:MRR:809.2,1176.0] || -> equal(op1(e11,e11),e11) equal(op1(e11,e11),e13)** equal(op1(e11,e11),e10). % 0.77/0.96 1340[0:MRR:810.1,810.3,1181.0,1208.0] || -> equal(op1(e11,e10),e10) equal(op1(e11,e10),e12)**. % 0.77/0.96 1341[0:MRR:811.1,811.2,1169.0,1167.0] || -> equal(op1(e10,e13),e13)** equal(op1(e10,e13),e10). % 0.77/0.96 1343[0:Rew:86.0,815.0] || -> equal(h4(e11),e23)** SkC69 SkC70 SkC71 SkC72 SkC73 SkC74 SkC75 SkC76 SkC77 SkC78 SkC79 SkC80 SkC81 SkC82 SkC83 SkC84 SkC85 SkC86 SkC87 SkC88 SkC89 SkC90 SkC91 SkC92 SkC93 SkC94 SkC95 SkC96 SkC97 SkC98 SkC99 SkC100 SkC101 SkC102 SkC103 SkC104 SkC105 SkC106 SkC107 SkC108 SkC109 SkC110 SkC111 SkC112 SkC113 SkC114 SkC115 SkC116 SkC117 SkC118 SkC119 SkC120 SkC121 SkC122 SkC123 SkC124 SkC125 SkC126 SkC127 SkC128 SkC129 SkC130 SkC131. % 0.77/0.96 1344[0:MRR:1343.1,1343.2,1343.3,1343.4,1343.5,1343.6,1343.7,1343.8,1343.9,1343.10,1343.11,1343.13,1343.15,1343.16,1343.17,1343.18,1343.19,1343.20,1343.21,1343.22,1343.23,1343.24,1343.25,1343.26,1343.27,1343.29,1343.30,1343.31,1343.32,1343.33,1343.34,1343.35,1343.36,1343.37,1343.38,1343.39,1343.40,1343.41,1343.42,1343.43,1343.44,1343.45,1343.47,1343.48,1343.49,1343.50,1343.51,1343.52,1343.54,1343.56,1343.57,1343.58,1343.59,1343.60,1343.61,1343.62,1343.63,947.0,945.0,942.0,939.0,936.0,934.0,931.0,928.0,925.0,1161.0,1069.0,920.0,1197.0,1064.0,915.0,1062.0,1166.0,1165.0,1058.0,1055.0,1053.0,1051.0,904.0,1049.0,1047.0,899.0,1044.0,1196.0,1041.0,894.0,1194.0,1038.0,1195.0,1158.0,1033.0,1031.0,1157.0,886.0,1028.0,1026.0,1024.0,879.0,1021.0,1019.0,874.0,1199.0,1198.0,1015.0,1011.0,1008.0,866.0,1160.0,1005.0,1003.0,861.0,1001.0,999.0] || -> equal(h4(e11),e23)** SkC80 SkC82 SkC96 SkC114 SkC121 SkC123. % 0.77/0.96 1345[0:MRR:816.1,816.2,816.3,816.4,816.5,816.6,816.7,816.8,816.9,816.10,816.11,816.13,816.15,816.16,816.17,816.18,816.19,816.20,816.21,816.22,816.23,816.24,816.25,816.26,816.27,816.29,816.30,816.31,816.32,816.33,816.34,816.35,816.36,816.37,816.38,816.39,816.40,816.41,816.42,816.43,816.44,816.45,816.47,816.48,816.49,816.50,816.51,816.52,816.54,816.56,816.57,816.58,816.59,816.60,816.61,816.62,816.63,989.0,987.0,985.0,983.0,981.0,979.0,977.0,975.0,973.0,1178.0,1130.0,971.0,1213.0,1125.0,969.0,1123.0,1183.0,1182.0,1121.0,1118.0,1116.0,1114.0,967.0,1112.0,1110.0,965.0,1108.0,1212.0,1106.0,963.0,1210.0,1104.0,1211.0,1175.0,1101.0,1099.0,1174.0,961.0,1097.0,1095.0,1093.0,959.0,1091.0,1089.0,957.0,1215.0,1214.0,1087.0,1084.0,1082.0,955.0,1177.0,1080.0,1078.0,953.0,1076.0,1074.0] || -> equal(op1(e13,e13),e13)** SkC14 SkC16 SkC30 SkC48 SkC55 SkC57. % 0.77/0.96 1346[0:Rew:1344.0,817.0,86.0,817.0] || equal(e23,e23) -> SkC69* SkC70 SkC71 SkC72 SkC73 SkC74 SkC75 SkC76 SkC77 SkC78 SkC79 SkC80 SkC81 SkC82 SkC83 SkC84 SkC85 SkC86 SkC87 SkC88 SkC89 SkC90 SkC91 SkC92 SkC93 SkC94 SkC95 SkC96 SkC97 SkC98 SkC99 SkC100 SkC101 SkC102 SkC103 SkC104 SkC105 SkC106 SkC107 SkC108 SkC109 SkC110 SkC111 SkC112 SkC113 SkC114 SkC115 SkC116 SkC117 SkC118 SkC119 SkC120 SkC121 SkC122 SkC123 SkC124 SkC125 SkC126 SkC127 SkC128 SkC129 SkC130 SkC131. % 0.77/0.96 1347[0:Obv:1346.0] || -> SkC69* SkC70 SkC71 SkC72 SkC73 SkC74 SkC75 SkC76 SkC77 SkC78 SkC79 SkC80 SkC81 SkC82 SkC83 SkC84 SkC85 SkC86 SkC87 SkC88 SkC89 SkC90 SkC91 SkC92 SkC93 SkC94 SkC95 SkC96 SkC97 SkC98 SkC99 SkC100 SkC101 SkC102 SkC103 SkC104 SkC105 SkC106 SkC107 SkC108 SkC109 SkC110 SkC111 SkC112 SkC113 SkC114 SkC115 SkC116 SkC117 SkC118 SkC119 SkC120 SkC121 SkC122 SkC123 SkC124 SkC125 SkC126 SkC127 SkC128 SkC129 SkC130 SkC131. % 0.77/0.96 1348[0:MRR:1347.0,1347.1,1347.2,1347.3,1347.4,1347.5,1347.6,1347.7,1347.8,1347.9,1347.10,1347.12,1347.14,1347.15,1347.16,1347.17,1347.18,1347.19,1347.20,1347.21,1347.22,1347.23,1347.24,1347.25,1347.26,1347.28,1347.29,1347.30,1347.31,1347.32,1347.33,1347.34,1347.35,1347.36,1347.37,1347.38,1347.39,1347.40,1347.41,1347.42,1347.43,1347.44,1347.46,1347.47,1347.48,1347.49,1347.50,1347.51,1347.53,1347.55,1347.56,1347.57,1347.58,1347.59,1347.60,1347.61,1347.62,947.0,945.0,942.0,939.0,936.0,934.0,931.0,928.0,925.0,1161.0,1069.0,920.0,1197.0,1064.0,915.0,1062.0,1166.0,1165.0,1058.0,1055.0,1053.0,1051.0,904.0,1049.0,1047.0,899.0,1044.0,1196.0,1041.0,894.0,1194.0,1038.0,1195.0,1158.0,1033.0,1031.0,1157.0,886.0,1028.0,1026.0,1024.0,879.0,1021.0,1019.0,874.0,1199.0,1198.0,1015.0,1011.0,1008.0,866.0,1160.0,1005.0,1003.0,861.0,1001.0,999.0] || -> SkC123 SkC121 SkC114 SkC96 SkC82 SkC80*. % 0.77/0.96 1349[0:Rew:1345.0,818.0] || equal(e13,e13) -> SkC3* SkC4 SkC5 SkC6 SkC7 SkC8 SkC9 SkC10 SkC11 SkC12 SkC13 SkC14 SkC15 SkC16 SkC17 SkC18 SkC19 SkC20 SkC21 SkC22 SkC23 SkC24 SkC25 SkC26 SkC27 SkC28 SkC29 SkC30 SkC31 SkC32 SkC33 SkC34 SkC35 SkC36 SkC37 SkC38 SkC39 SkC40 SkC41 SkC42 SkC43 SkC44 SkC45 SkC46 SkC47 SkC48 SkC49 SkC50 SkC51 SkC52 SkC53 SkC54 SkC55 SkC56 SkC57 SkC58 SkC59 SkC60 SkC61 SkC62 SkC63 SkC64 SkC65. % 0.77/0.96 1350[0:Obv:1349.0] || -> SkC3* SkC4 SkC5 SkC6 SkC7 SkC8 SkC9 SkC10 SkC11 SkC12 SkC13 SkC14 SkC15 SkC16 SkC17 SkC18 SkC19 SkC20 SkC21 SkC22 SkC23 SkC24 SkC25 SkC26 SkC27 SkC28 SkC29 SkC30 SkC31 SkC32 SkC33 SkC34 SkC35 SkC36 SkC37 SkC38 SkC39 SkC40 SkC41 SkC42 SkC43 SkC44 SkC45 SkC46 SkC47 SkC48 SkC49 SkC50 SkC51 SkC52 SkC53 SkC54 SkC55 SkC56 SkC57 SkC58 SkC59 SkC60 SkC61 SkC62 SkC63 SkC64 SkC65. % 0.77/0.96 1351[0:MRR:1350.0,1350.1,1350.2,1350.3,1350.4,1350.5,1350.6,1350.7,1350.8,1350.9,1350.10,1350.12,1350.14,1350.15,1350.16,1350.17,1350.18,1350.19,1350.20,1350.21,1350.22,1350.23,1350.24,1350.25,1350.26,1350.28,1350.29,1350.30,1350.31,1350.32,1350.33,1350.34,1350.35,1350.36,1350.37,1350.38,1350.39,1350.40,1350.41,1350.42,1350.43,1350.44,1350.46,1350.47,1350.48,1350.49,1350.50,1350.51,1350.53,1350.55,1350.56,1350.57,1350.58,1350.59,1350.60,1350.61,1350.62,989.0,987.0,985.0,983.0,981.0,979.0,977.0,975.0,973.0,1178.0,1130.0,971.0,1213.0,1125.0,969.0,1123.0,1183.0,1182.0,1121.0,1118.0,1116.0,1114.0,967.0,1112.0,1110.0,965.0,1108.0,1212.0,1106.0,963.0,1210.0,1104.0,1211.0,1175.0,1101.0,1099.0,1174.0,961.0,1097.0,1095.0,1093.0,959.0,1091.0,1089.0,957.0,1215.0,1214.0,1087.0,1084.0,1082.0,955.0,1177.0,1080.0,1078.0,953.0,1076.0,1074.0] || -> SkC57 SkC55 SkC48 SkC30 SkC16 SkC14*. % 0.77/0.96 1358[0:Rew:32.0,822.13,1216.0,822.9,32.0,822.9,1200.0,822.9,32.0,822.5,32.0,822.4,32.0,822.3,992.0,822.2,32.0,822.2,855.0,822.2,86.0,822.1,32.0,822.1,33.0,822.1,32.0,822.0] || equal(e23,e23) equal(h4(e11),h4(e11)) equal(h4(e12),h4(e12)) equal(op2(e23,h4(e12)),h4(op1(e10,e12))) equal(op2(e23,h4(e13)),h4(op1(e10,e13))) equal(op2(h4(e11),e23),h4(op1(e11,e10))) equal(op2(h4(e11),h4(e11)),h4(op1(e11,e11))) equal(op2(h4(e11),h4(e12)),h4(op1(e11,e12))) equal(op2(h4(e11),h4(e13)),h4(op1(e11,e13))) equal(h4(e13),h4(e13)) equal(op2(h4(e12),h4(e11)),h4(op1(e12,e11))) equal(op2(h4(e12),h4(e12)),h4(op1(e12,e12))) equal(op2(h4(e12),h4(e13)),h4(op1(e12,e13))) equal(op2(h4(e13),e23),h4(op1(e13,e10))) equal(op2(h4(e13),h4(e11)),h4(op1(e13,e11))) equal(op2(h4(e13),h4(e12)),h4(op1(e13,e12))) equal(op2(h4(e13),h4(e13)),h4(op1(e13,e13)))** SkC141 SkC142 SkC143 -> . % 0.77/0.96 1359[0:Obv:1358.9] || SkC143 SkC142 SkC141 equal(op2(e23,h4(e13)),h4(op1(e10,e13))) equal(op2(e23,h4(e12)),h4(op1(e10,e12))) equal(op2(h4(e13),e23),h4(op1(e13,e10))) equal(op2(h4(e11),e23),h4(op1(e11,e10))) equal(op2(h4(e13),h4(e13)),h4(op1(e13,e13)))** equal(op2(h4(e12),h4(e12)),h4(op1(e12,e12))) equal(op2(h4(e11),h4(e11)),h4(op1(e11,e11))) equal(op2(h4(e13),h4(e12)),h4(op1(e13,e12))) equal(op2(h4(e13),h4(e11)),h4(op1(e13,e11))) equal(op2(h4(e12),h4(e13)),h4(op1(e12,e13))) equal(op2(h4(e12),h4(e11)),h4(op1(e12,e11))) equal(op2(h4(e11),h4(e13)),h4(op1(e11,e13))) equal(op2(h4(e11),h4(e12)),h4(op1(e11,e12))) -> . % 0.77/0.96 1374[0:Rew:30.0,829.13,1218.0,829.9,30.0,829.9,1200.0,829.9,30.0,829.5,30.0,829.4,30.0,829.3,994.0,829.2,30.0,829.2,855.0,829.2,84.0,829.1,30.0,829.1,33.0,829.1] || equal(h2(e11),e23) equal(h2(e11),h2(e11)) equal(h2(e12),h2(e12)) equal(op2(e21,h2(e12)),h2(op1(e10,e12))) equal(op2(e21,h2(e13)),h2(op1(e10,e13))) equal(op2(h2(e11),e21),h2(op1(e11,e10))) equal(op2(h2(e11),h2(e11)),h2(op1(e11,e11))) equal(op2(h2(e11),h2(e12)),h2(op1(e11,e12))) equal(op2(h2(e11),h2(e13)),h2(op1(e11,e13))) equal(h2(e13),h2(e13)) equal(op2(h2(e12),h2(e11)),h2(op1(e12,e11))) equal(op2(h2(e12),h2(e12)),h2(op1(e12,e12))) equal(op2(h2(e12),h2(e13)),h2(op1(e12,e13))) equal(op2(h2(e13),e21),h2(op1(e13,e10))) equal(op2(h2(e13),h2(e11)),h2(op1(e13,e11))) equal(op2(h2(e13),h2(e12)),h2(op1(e13,e12))) equal(op2(h2(e13),h2(e13)),h2(op1(e13,e13)))** SkC135 SkC136 SkC137 -> . % 0.77/0.96 1375[0:Obv:1374.9] || equal(h2(e11),e23) equal(op2(e21,h2(e12)),h2(op1(e10,e12))) equal(op2(e21,h2(e13)),h2(op1(e10,e13))) equal(op2(h2(e11),e21),h2(op1(e11,e10))) equal(op2(h2(e11),h2(e11)),h2(op1(e11,e11))) equal(op2(h2(e11),h2(e12)),h2(op1(e11,e12))) equal(op2(h2(e11),h2(e13)),h2(op1(e11,e13))) equal(op2(h2(e12),h2(e11)),h2(op1(e12,e11))) equal(op2(h2(e12),h2(e12)),h2(op1(e12,e12))) equal(op2(h2(e12),h2(e13)),h2(op1(e12,e13))) equal(op2(h2(e13),e21),h2(op1(e13,e10))) equal(op2(h2(e13),h2(e11)),h2(op1(e13,e11))) equal(op2(h2(e13),h2(e12)),h2(op1(e13,e12))) equal(op2(h2(e13),h2(e13)),h2(op1(e13,e13)))** SkC135 SkC136 SkC137 -> . % 0.77/0.96 1376[0:MRR:1375.15,845.0] || SkC137 SkC135 equal(h2(e11),e23) equal(op2(e21,h2(e13)),h2(op1(e10,e13))) equal(op2(e21,h2(e12)),h2(op1(e10,e12))) equal(op2(h2(e13),e21),h2(op1(e13,e10))) equal(op2(h2(e11),e21),h2(op1(e11,e10))) equal(op2(h2(e13),h2(e13)),h2(op1(e13,e13)))** equal(op2(h2(e12),h2(e12)),h2(op1(e12,e12))) equal(op2(h2(e11),h2(e11)),h2(op1(e11,e11))) equal(op2(h2(e13),h2(e12)),h2(op1(e13,e12))) equal(op2(h2(e13),h2(e11)),h2(op1(e13,e11))) equal(op2(h2(e12),h2(e13)),h2(op1(e12,e13))) equal(op2(h2(e12),h2(e11)),h2(op1(e12,e11))) equal(op2(h2(e11),h2(e13)),h2(op1(e11,e13))) equal(op2(h2(e11),h2(e12)),h2(op1(e11,e12))) -> . % 0.77/0.96 1379[0:Rew:86.0,831.16,1219.0,831.16,1219.0,831.15,995.0,831.15,1219.0,831.14,835.0,831.14,1219.0,831.13,29.0,831.13,995.0,831.12,1219.0,831.12,85.0,831.11,995.0,831.11,995.0,831.10,835.0,831.10,1184.0,831.9,995.0,831.9,29.0,831.9,1219.0,831.9,1200.0,831.9,835.0,831.8,1219.0,831.8,835.0,831.7,995.0,831.7,84.0,831.6,835.0,831.6,835.0,831.5,29.0,831.5,29.0,831.4,1219.0,831.4,29.0,831.3,995.0,831.3,854.0,831.2,29.0,831.2,835.0,831.2,995.0,831.2,855.0,831.2,34.0,831.1,29.0,831.1,835.0,831.1,33.0,831.1,1219.0,831.0] || equal(e23,e23) equal(e21,e21) equal(e22,e22) equal(h1(op1(e10,e12)),op2(e20,e22)) equal(h1(op1(e10,e13)),op2(e20,e23)) equal(h1(op1(e11,e10)),op2(e21,e20)) equal(h1(op1(e11,e11)),h2(e11)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e13)),op2(e21,e23)) equal(e23,e23) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e12)),op2(e23,e22)) equal(h1(op1(e13,e13)),h4(e11))** SkC132 SkC133 SkC134 -> . % 0.77/0.96 1380[0:Obv:1379.9] || equal(h1(op1(e10,e12)),op2(e20,e22)) equal(h1(op1(e10,e13)),op2(e20,e23)) equal(h1(op1(e11,e10)),op2(e21,e20)) equal(h1(op1(e11,e11)),h2(e11)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e13)),op2(e21,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e12)),op2(e23,e22)) equal(h1(op1(e13,e13)),h4(e11))** SkC132 SkC133 SkC134 -> . % 0.77/0.96 1381[0:MRR:1380.13,1380.14,1380.15,853.0,850.0,997.0] || equal(h1(op1(e11,e11)),h2(e11)) equal(h1(op1(e13,e13)),h4(e11))** equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e13,e12)),op2(e23,e22)) equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e11,e13)),op2(e21,e23)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e10)),op2(e21,e20)) equal(h1(op1(e10,e13)),op2(e20,e23)) equal(h1(op1(e10,e12)),op2(e20,e22)) -> . % 0.77/0.96 1388[1:Spt:1290.0] || -> equal(h4(e11),e23)**. % 0.77/0.96 1389[1:Rew:1388.0,1249.0] || -> equal(e23,e22) equal(op2(e23,e22),e22)** equal(op2(e23,e20),e22). % 0.77/0.96 1390[1:Rew:1388.0,1247.0] || -> equal(e23,e22) equal(op2(e22,e23),e22)** equal(op2(e21,e23),e22). % 0.77/0.96 1392[1:Rew:1388.0,921.1] || SkC80* -> equal(e23,e22). % 0.77/0.96 1393[1:Rew:1388.0,900.1] || SkC96* -> equal(e23,e22). % 0.77/0.96 1403[1:Rew:1388.0,86.0] || -> equal(op2(e23,e23),e23)**. % 0.77/0.96 1405[1:Rew:1388.0,1133.0] || equal(op2(e23,e22),e23)** -> . % 0.77/0.96 1406[1:Rew:1388.0,1134.0] || equal(op2(e23,e21),e23)** -> . % 0.77/0.96 1410[1:Rew:1388.0,1149.0] || equal(op2(e20,e23),e23)** -> . % 0.77/0.96 1411[1:Rew:1388.0,1381.1] || equal(h1(op1(e11,e11)),h2(e11)) equal(h1(op1(e13,e13)),e23)** equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e13,e12)),op2(e23,e22)) equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e11,e13)),op2(e21,e23)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e10)),op2(e21,e20)) equal(h1(op1(e10,e13)),op2(e20,e23)) equal(h1(op1(e10,e12)),op2(e20,e22)) -> . % 0.77/0.96 1413[1:MRR:1392.1,12.0] || SkC80* -> . % 0.77/0.96 1414[1:MRR:1348.5,1413.0] || -> SkC123 SkC121 SkC114 SkC96 SkC82*. % 0.77/0.96 1415[1:MRR:1393.1,12.0] || SkC96* -> . % 0.77/0.96 1416[1:MRR:1414.3,1415.0] || -> SkC123 SkC121 SkC114 SkC82*. % 0.77/0.96 1423[1:MRR:752.0,1405.0] || -> equal(op2(e23,e22),e22)** equal(op2(e23,e22),e21) equal(op2(e23,e22),e20). % 0.77/0.96 1424[1:MRR:321.1,1406.0] || SkC123* -> . % 0.77/0.96 1425[1:MRR:317.1,1406.0] || SkC121* -> . % 0.77/0.96 1426[1:MRR:1270.1,1406.0] || -> equal(h2(e11),e23)**. % 0.77/0.96 1427[1:MRR:1291.0,1406.0] || -> equal(op2(e23,e21),e21)** equal(op2(e23,e21),e20). % 0.77/0.96 1428[1:MRR:1416.0,1424.0] || -> SkC121 SkC114 SkC82*. % 0.77/0.96 1429[1:MRR:1428.0,1425.0] || -> SkC114 SkC82*. % 0.77/0.96 1433[1:Rew:1426.0,1376.2] || SkC137 SkC135 equal(e23,e23) equal(op2(e21,h2(e13)),h2(op1(e10,e13))) equal(op2(e21,h2(e12)),h2(op1(e10,e12))) equal(op2(h2(e13),e21),h2(op1(e13,e10))) equal(op2(h2(e11),e21),h2(op1(e11,e10))) equal(op2(h2(e13),h2(e13)),h2(op1(e13,e13)))** equal(op2(h2(e12),h2(e12)),h2(op1(e12,e12))) equal(op2(h2(e11),h2(e11)),h2(op1(e11,e11))) equal(op2(h2(e13),h2(e12)),h2(op1(e13,e12))) equal(op2(h2(e13),h2(e11)),h2(op1(e13,e11))) equal(op2(h2(e12),h2(e13)),h2(op1(e12,e13))) equal(op2(h2(e12),h2(e11)),h2(op1(e12,e11))) equal(op2(h2(e11),h2(e13)),h2(op1(e11,e13))) equal(op2(h2(e11),h2(e12)),h2(op1(e11,e12))) -> . % 0.77/0.96 1434[1:Rew:1426.0,1238.0] || equal(e23,e23) -> SkC68 equal(op2(e21,e23),e21)**. % 0.77/0.96 1435[1:Rew:1426.0,1278.0] || -> equal(e23,e21) equal(op2(e21,e23),e21)** equal(op2(e21,e22),e21). % 0.77/0.96 1441[1:Rew:1426.0,994.0] || -> equal(op2(e21,e23),h2(e12))**. % 0.77/0.96 1448[1:MRR:1283.0,1410.0] || -> equal(op2(e20,e22),e23)**. % 0.77/0.96 1449[1:MRR:1300.0,1410.0] || -> equal(op2(e20,e23),e20)**. % 0.77/0.96 1460[1:Rew:1449.0,408.0] || equal(op2(e22,e23),e20)** -> . % 0.77/0.96 1467[1:Rew:1441.0,588.1] || SkC82 equal(h2(e12),e21)** -> . % 0.77/0.96 1468[1:Rew:1441.0,650.1] || SkC114 equal(h2(e12),e21)** -> . % 0.77/0.96 1471[1:Rew:1441.0,421.0] || equal(op2(e21,e20),h2(e12))** -> . % 0.77/0.96 1477[1:MRR:1268.1,1460.0] || -> equal(h3(e11),e20) equal(op2(e22,e21),e20)**. % 0.77/0.96 1478[1:MRR:1293.2,1460.0] || -> equal(op2(e22,e23),e22)** equal(op2(e22,e23),e21). % 0.77/0.96 1480[1:Obv:1434.0] || -> SkC68 equal(op2(e21,e23),e21)**. % 0.77/0.96 1481[1:Rew:1441.0,1480.1] || -> SkC68 equal(h2(e12),e21)**. % 0.77/0.96 1482[1:MRR:1389.0,12.0] || -> equal(op2(e23,e22),e22)** equal(op2(e23,e20),e22). % 0.77/0.96 1483[1:Rew:1441.0,1390.2] || -> equal(e23,e22) equal(op2(e22,e23),e22)** equal(h2(e12),e22). % 0.77/0.96 1484[1:MRR:1483.0,12.0] || -> equal(op2(e22,e23),e22)** equal(h2(e12),e22). % 0.77/0.96 1489[1:Rew:1441.0,1435.1] || -> equal(e23,e21) equal(h2(e12),e21) equal(op2(e21,e22),e21)**. % 0.77/0.96 1490[1:MRR:1489.0,11.0] || -> equal(h2(e12),e21) equal(op2(e21,e22),e21)**. % 0.77/0.96 1498[1:Rew:1448.0,1411.12,1449.0,1411.11,1441.0,1411.8,1426.0,1411.0] || equal(h1(op1(e11,e11)),e23) equal(h1(op1(e13,e13)),e23)** equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e13,e12)),op2(e23,e22)) equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e11,e13)),h2(e12)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e10)),op2(e21,e20)) equal(h1(op1(e10,e13)),e20) equal(h1(op1(e10,e12)),e23) -> . % 0.77/0.96 1500[1:Obv:1433.2] || SkC137 SkC135 equal(op2(e21,h2(e13)),h2(op1(e10,e13))) equal(op2(e21,h2(e12)),h2(op1(e10,e12))) equal(op2(h2(e13),e21),h2(op1(e13,e10))) equal(op2(h2(e11),e21),h2(op1(e11,e10))) equal(op2(h2(e13),h2(e13)),h2(op1(e13,e13)))** equal(op2(h2(e12),h2(e12)),h2(op1(e12,e12))) equal(op2(h2(e11),h2(e11)),h2(op1(e11,e11))) equal(op2(h2(e13),h2(e12)),h2(op1(e13,e12))) equal(op2(h2(e13),h2(e11)),h2(op1(e13,e11))) equal(op2(h2(e12),h2(e13)),h2(op1(e12,e13))) equal(op2(h2(e12),h2(e11)),h2(op1(e12,e11))) equal(op2(h2(e11),h2(e13)),h2(op1(e11,e13))) equal(op2(h2(e11),h2(e12)),h2(op1(e11,e12))) -> . % 0.77/0.96 1501[1:Rew:1426.0,1500.14,1426.0,1500.13,1426.0,1500.12,1426.0,1500.10,1403.0,1500.8,1426.0,1500.8,1426.0,1500.5] || SkC137 SkC135 equal(op2(e21,h2(e13)),h2(op1(e10,e13))) equal(op2(e21,h2(e12)),h2(op1(e10,e12))) equal(op2(h2(e13),e21),h2(op1(e13,e10))) equal(h2(op1(e11,e10)),op2(e23,e21)) equal(op2(h2(e13),h2(e13)),h2(op1(e13,e13)))** equal(op2(h2(e12),h2(e12)),h2(op1(e12,e12))) equal(h2(op1(e11,e11)),e23) equal(op2(h2(e13),h2(e12)),h2(op1(e13,e12))) equal(op2(h2(e13),e23),h2(op1(e13,e11))) equal(op2(h2(e12),h2(e13)),h2(op1(e12,e13))) equal(op2(h2(e12),e23),h2(op1(e12,e11))) equal(op2(e23,h2(e13)),h2(op1(e11,e13))) equal(op2(e23,h2(e12)),h2(op1(e11,e12))) -> . % 0.77/0.96 1504[2:Spt:799.0] || -> equal(op1(e13,e13),e13)**. % 0.77/0.96 1508[2:Rew:1504.0,112.1] || SkC14* -> equal(e13,e12). % 0.77/0.96 1509[2:Rew:1504.0,143.1] || SkC30* -> equal(e13,e12). % 0.77/0.96 1510[2:Rew:1504.0,1307.0] || -> equal(e13,e11) equal(op1(e13,e11),e11) equal(op1(e13,e12),e11)**. % 0.77/0.96 1511[2:Rew:1504.0,1306.0] || -> equal(e13,e11) equal(op1(e11,e13),e11) equal(op1(e12,e13),e11)**. % 0.77/0.96 1518[2:Rew:1504.0,388.0] || equal(op1(e13,e12),e13)** -> . % 0.77/0.96 1519[2:Rew:1504.0,387.0] || equal(op1(e13,e11),e13)** -> . % 0.77/0.96 1522[2:Rew:1504.0,363.0] || equal(op1(e11,e13),e13)** -> . % 0.77/0.96 1523[2:Rew:1504.0,361.0] || equal(op1(e10,e13),e13)** -> . % 0.77/0.96 1524[2:Rew:1504.0,1498.1] || equal(h1(op1(e11,e11)),e23) equal(h1(e13),e23) equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e11,e13)),h2(e12)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e10)),op2(e21,e20)) equal(h1(op1(e10,e13)),e20) equal(h1(op1(e10,e12)),e23) -> . % 0.77/0.96 1527[2:MRR:1508.1,6.0] || SkC14* -> . % 0.77/0.96 1528[2:MRR:1351.5,1527.0] || -> SkC57 SkC55 SkC48 SkC30 SkC16*. % 0.77/0.96 1529[2:MRR:1509.1,6.0] || SkC30* -> . % 0.77/0.96 1530[2:MRR:1528.3,1529.0] || -> SkC57 SkC55 SkC48 SkC16*. % 0.77/0.96 1532[2:MRR:800.0,1518.0] || -> equal(op1(e13,e12),e12)** equal(op1(e13,e12),e11) equal(op1(e13,e12),e10). % 0.77/0.96 1533[2:MRR:195.1,1519.0] || SkC57* -> . % 0.77/0.96 1534[2:MRR:191.1,1519.0] || SkC55* -> . % 0.77/0.96 1535[2:MRR:1318.0,1519.0] || -> equal(op1(e11,e11),e13)**. % 0.77/0.96 1537[2:MRR:1530.0,1533.0] || -> SkC55 SkC48 SkC16*. % 0.77/0.96 1538[2:MRR:1537.0,1534.0] || -> SkC48 SkC16*. % 0.77/0.96 1539[2:Rew:1535.0,1240.0] || equal(e13,e13) -> SkC2 equal(op1(e11,e13),e11)**. % 0.77/0.96 1540[2:Rew:1535.0,1323.0] || -> equal(e13,e11) equal(op1(e11,e13),e11)** equal(op1(e11,e12),e11). % 0.77/0.96 1550[2:MRR:807.0,1522.0] || -> equal(op1(e11,e13),e11) equal(op1(e11,e13),e12)** equal(op1(e11,e13),e10). % 0.77/0.96 1551[2:MRR:1327.0,1523.0] || -> equal(op1(e10,e12),e13)**. % 0.77/0.96 1552[2:MRR:1341.0,1523.0] || -> equal(op1(e10,e13),e10)**. % 0.77/0.96 1564[2:Rew:1552.0,359.0] || equal(op1(e11,e13),e10)** -> . % 0.77/0.96 1570[2:Obv:1539.0] || -> SkC2 equal(op1(e11,e13),e11)**. % 0.77/0.96 1573[2:MRR:1510.0,5.0] || -> equal(op1(e13,e11),e11) equal(op1(e13,e12),e11)**. % 0.77/0.96 1574[2:MRR:1511.0,5.0] || -> equal(op1(e11,e13),e11) equal(op1(e12,e13),e11)**. % 0.77/0.96 1575[2:MRR:1540.0,5.0] || -> equal(op1(e11,e13),e11)** equal(op1(e11,e12),e11). % 0.77/0.96 1578[2:MRR:1550.2,1564.0] || -> equal(op1(e11,e13),e11) equal(op1(e11,e13),e12)**. % 0.77/0.96 1584[2:Rew:1219.0,1524.12,1551.0,1524.12,29.0,1524.11,1552.0,1524.11,1219.0,1524.1,1219.0,1524.0,1535.0,1524.0] || equal(e23,e23) equal(e23,e23) equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e11,e13)),h2(e12)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e10)),op2(e21,e20)) equal(e20,e20) equal(e23,e23) -> . % 0.77/0.96 1585[2:Obv:1584.12] || equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e11,e13)),h2(e12)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e10)),op2(e21,e20)) -> . % 0.77/0.96 1590[3:Spt:1312.0] || -> equal(op1(e12,e12),e11)**. % 0.77/0.96 1593[3:Rew:1590.0,89.1] || SkC2* -> equal(e12,e11). % 0.77/0.96 1606[3:MRR:1593.1,4.0] || SkC2* -> . % 0.77/0.96 1607[3:MRR:1570.0,1606.0] || -> equal(op1(e11,e13),e11)**. % 0.77/0.96 1608[3:Rew:1607.0,464.1] || SkC16* equal(e11,e11) -> . % 0.77/0.96 1609[3:Rew:1607.0,526.1] || SkC48* equal(e11,e11) -> . % 0.77/0.96 1635[3:Obv:1608.1] || SkC16* -> . % 0.77/0.96 1636[3:MRR:1538.1,1635.0] || -> SkC48*. % 0.77/0.96 1637[3:Obv:1609.1] || SkC48* -> . % 0.77/0.96 1638[3:MRR:1637.0,1636.0] || -> . % 0.77/0.96 1656[3:Spt:1638.0,1312.0,1590.0] || equal(op1(e12,e12),e11)** -> . % 0.77/0.96 1657[3:Spt:1638.0,1312.1,1312.2] || -> equal(op1(e11,e12),e11) equal(op1(e13,e12),e11)**. % 0.77/0.96 1660[4:Spt:1657.0] || -> equal(op1(e11,e12),e11)**. % 0.77/0.96 1662[4:Rew:1660.0,357.0] || equal(op1(e13,e12),e11)** -> . % 0.77/0.96 1667[4:Rew:1660.0,376.0] || equal(op1(e11,e13),e11)** -> . % 0.77/0.96 1671[4:Rew:1660.0,1585.7] || equal(h1(op1(e12,e12)),h3(e11)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e11,e13)),h2(e12)) equal(op2(e21,e22),h1(e11)) equal(h1(op1(e11,e10)),op2(e21,e20)) -> . % 0.77/0.96 1675[4:MRR:1573.1,1662.0] || -> equal(op1(e13,e11),e11)**. % 0.77/0.96 1676[4:MRR:1532.1,1662.0] || -> equal(op1(e13,e12),e12)** equal(op1(e13,e12),e10). % 0.77/0.96 1679[4:Rew:1675.0,352.0] || equal(op1(e12,e11),e11)** -> . % 0.77/0.96 1684[4:MRR:1570.1,1667.0] || -> SkC2*. % 0.77/0.96 1685[4:MRR:1574.0,1667.0] || -> equal(op1(e12,e13),e11)**. % 0.77/0.96 1686[4:MRR:1578.0,1667.0] || -> equal(op1(e11,e13),e12)**. % 0.77/0.96 1687[4:MRR:89.0,1684.0] || -> equal(op1(e12,e12),e12)**. % 0.77/0.96 1698[4:Rew:1686.0,373.0] || equal(op1(e11,e10),e12)** -> . % 0.77/0.96 1702[4:Rew:1687.0,358.0] || equal(op1(e13,e12),e12)** -> . % 0.77/0.96 1707[4:MRR:1338.0,1679.0] || -> equal(op1(e12,e11),e10)**. % 0.77/0.96 1714[4:MRR:1329.1,1698.0] || -> equal(op1(e13,e10),e12)**. % 0.77/0.96 1715[4:MRR:1340.1,1698.0] || -> equal(op1(e11,e10),e10)**. % 0.77/0.96 1726[4:MRR:1676.0,1702.0] || -> equal(op1(e13,e12),e10)**. % 0.77/0.96 1736[4:Rew:29.0,1671.8,1715.0,1671.8,835.0,1671.7,995.0,1671.6,1686.0,1671.6,29.0,1671.5,1707.0,1671.5,835.0,1671.4,1685.0,1671.4,995.0,1671.3,1714.0,1671.3,835.0,1671.2,1675.0,1671.2,29.0,1671.1,1726.0,1671.1,995.0,1671.0,1687.0,1671.0] || equal(h3(e11),e22) equal(op2(e23,e22),e20)** equal(op2(e23,e21),e21) equal(op2(e23,e20),e22) equal(op2(e22,e23),e21) equal(op2(e22,e21),e20) equal(h2(e12),e22) equal(op2(e21,e22),e21) equal(op2(e21,e20),e20) -> . % 0.77/0.96 1741[5:Spt:1295.0] || -> equal(h3(e11),e22)**. % 0.77/0.96 1746[5:Rew:1741.0,1477.0] || -> equal(e22,e20) equal(op2(e22,e21),e20)**. % 0.77/0.96 1748[5:Rew:1741.0,1736.0] || equal(e22,e22) equal(op2(e23,e22),e20)** equal(op2(e23,e21),e21) equal(op2(e23,e20),e22) equal(op2(e22,e23),e21) equal(op2(e22,e21),e20) equal(h2(e12),e22) equal(op2(e21,e22),e21) equal(op2(e21,e20),e20) -> . % 0.77/0.96 1752[5:Rew:1741.0,1136.0] || equal(op2(e22,e23),e22)** -> . % 0.77/0.96 1754[5:Rew:1741.0,1150.0] || equal(op2(e23,e22),e22)** -> . % 0.77/0.96 1763[5:MRR:1478.0,1752.0] || -> equal(op2(e22,e23),e21)**. % 0.77/0.96 1764[5:MRR:1484.0,1752.0] || -> equal(h2(e12),e22)**. % 0.77/0.96 1768[5:Rew:1764.0,1218.0] || -> equal(op2(e22,e21),h2(e13))**. % 0.77/0.96 1772[5:Rew:1764.0,1490.0] || -> equal(e22,e21) equal(op2(e21,e22),e21)**. % 0.77/0.96 1776[5:Rew:1764.0,1471.0] || equal(op2(e21,e20),e22)** -> . % 0.77/0.96 1786[5:MRR:1482.0,1754.0] || -> equal(op2(e23,e20),e22)**. % 0.77/0.96 1787[5:MRR:1423.0,1754.0] || -> equal(op2(e23,e22),e21)** equal(op2(e23,e22),e20). % 0.77/0.96 1804[5:Rew:1768.0,400.0] || equal(op2(e23,e21),h2(e13))** -> . % 0.77/0.96 1805[5:MRR:1299.1,1776.0] || -> equal(op2(e21,e20),e20)**. % 0.77/0.96 1813[5:Rew:1768.0,1746.1] || -> equal(e22,e20) equal(h2(e13),e20)**. % 0.77/0.96 1814[5:MRR:1813.0,8.0] || -> equal(h2(e13),e20)**. % 0.77/0.96 1816[5:Rew:1814.0,1768.0] || -> equal(op2(e22,e21),e20)**. % 0.77/0.96 1820[5:Rew:1814.0,1804.0] || equal(op2(e23,e21),e20)** -> . % 0.77/0.96 1822[5:MRR:1427.1,1820.0] || -> equal(op2(e23,e21),e21)**. % 0.77/0.96 1824[5:Rew:1822.0,434.0] || equal(op2(e23,e22),e21)** -> . % 0.77/0.96 1827[5:MRR:1772.0,10.0] || -> equal(op2(e21,e22),e21)**. % 0.77/0.96 1832[5:MRR:1787.0,1824.0] || -> equal(op2(e23,e22),e20)**. % 0.77/0.96 1836[5:Obv:1748.0] || equal(op2(e23,e22),e20)** equal(op2(e23,e21),e21) equal(op2(e23,e20),e22) equal(op2(e22,e23),e21) equal(op2(e22,e21),e20) equal(h2(e12),e22) equal(op2(e21,e22),e21) equal(op2(e21,e20),e20) -> . % 0.77/0.96 1837[5:Rew:1805.0,1836.7,1827.0,1836.6,1764.0,1836.5,1816.0,1836.4,1763.0,1836.3,1786.0,1836.2,1822.0,1836.1,1832.0,1836.0] || equal(e20,e20) equal(e21,e21) equal(e22,e22)* equal(e21,e21) equal(e20,e20) equal(e22,e22)* equal(e21,e21) equal(e20,e20) -> . % 0.77/0.96 1838[5:Obv:1837.7] || -> . % 0.77/0.96 1845[5:Spt:1838.0,1295.0,1741.0] || equal(h3(e11),e22)** -> . % 0.77/0.96 1846[5:Spt:1838.0,1295.1,1295.2] || -> equal(h3(e11),e21)** equal(h3(e11),e20). % 0.77/0.96 1847[5:MRR:948.1,1845.0] || SkC68* -> . % 0.77/0.96 1848[5:MRR:1481.0,1847.0] || -> equal(h2(e12),e21)**. % 0.77/0.96 1853[5:Rew:1848.0,1468.1] || SkC114* equal(e21,e21) -> . % 0.77/0.96 1854[5:Obv:1853.1] || SkC114* -> . % 0.77/0.96 1855[5:MRR:1429.0,1854.0] || -> SkC82*. % 0.77/0.96 1856[5:Rew:1848.0,1467.1] || SkC82* equal(e21,e21) -> . % 0.77/0.96 1857[5:Obv:1856.1] || SkC82* -> . % 0.77/0.96 1858[5:MRR:1857.0,1855.0] || -> . % 0.77/0.96 1880[4:Spt:1858.0,1657.0,1660.0] || equal(op1(e11,e12),e11)** -> . % 0.77/0.96 1881[4:Spt:1858.0,1657.1] || -> equal(op1(e13,e12),e11)**. % 0.77/0.96 1887[4:MRR:1575.1,1880.0] || -> equal(op1(e11,e13),e11)**. % 0.77/0.96 1888[4:Rew:1887.0,464.1] || SkC16* equal(e11,e11) -> . % 0.77/0.96 1889[4:Rew:1887.0,526.1] || SkC48* equal(e11,e11) -> . % 0.77/0.96 1895[4:Obv:1888.1] || SkC16* -> . % 0.77/0.96 1896[4:MRR:1538.1,1895.0] || -> SkC48*. % 0.77/0.96 1902[4:Obv:1889.1] || SkC48* -> . % 0.77/0.96 1903[4:MRR:1902.0,1896.0] || -> . % 0.77/0.96 1943[2:Spt:1903.0,799.0,1504.0] || equal(op1(e13,e13),e13)** -> . % 0.77/0.96 1944[2:Spt:1903.0,799.1,799.2,799.3] || -> equal(op1(e13,e13),e12)** equal(op1(e13,e13),e11) equal(op1(e13,e13),e10). % 0.77/0.96 1945[2:MRR:1235.1,1943.0] || -> SkC2*. % 0.77/0.96 1946[2:MRR:89.0,1945.0] || -> equal(op1(e12,e12),e12)**. % 0.77/0.96 1948[2:Rew:1946.0,196.1] || SkC57* -> equal(e12,e11). % 0.77/0.96 1949[2:MRR:1948.1,4.0] || SkC57* -> . % 0.77/0.96 1950[2:MRR:1351.0,1949.0] || -> SkC55 SkC48 SkC30 SkC16 SkC14*. % 0.77/0.96 1951[2:Rew:1946.0,358.0] || equal(op1(e13,e12),e12)** -> . % 0.77/0.96 1952[2:Rew:1946.0,382.0] || equal(op1(e12,e13),e12)** -> . % 0.77/0.96 1953[2:MRR:177.1,1952.0] || SkC48* -> . % 0.77/0.96 1954[2:MRR:1950.1,1953.0] || -> SkC55 SkC30 SkC16 SkC14*. % 0.77/0.96 1956[2:Rew:1946.0,356.0] || equal(op1(e11,e12),e12)** -> . % 0.77/0.96 1958[2:MRR:703.0,1945.0] || equal(op1(e13,e13),e12)** -> equal(op1(e13,e12),e13). % 0.77/0.96 1959[2:MRR:1320.0,1956.0] || -> equal(op1(e11,e13),e12)** equal(op1(e11,e10),e12). % 0.77/0.96 1962[2:Rew:1946.0,1312.0] || -> equal(e12,e11) equal(op1(e11,e12),e11) equal(op1(e13,e12),e11)**. % 0.77/0.96 1963[2:MRR:1962.0,4.0] || -> equal(op1(e11,e12),e11) equal(op1(e13,e12),e11)**. % 0.77/0.96 1964[2:MRR:1302.0,1943.0] || -> equal(op1(e11,e13),e13)** equal(op1(e10,e13),e13). % 0.77/0.96 1966[2:MRR:1304.1,1952.0] || -> equal(op1(e13,e13),e12)** equal(op1(e11,e13),e12). % 0.77/0.96 1967[2:MRR:1305.1,1951.0] || -> equal(op1(e13,e13),e12)** equal(op1(e13,e10),e12). % 0.77/0.96 1968[2:MRR:1336.0,1952.0] || -> equal(op1(e12,e13),e11)** equal(op1(e12,e13),e10). % 0.77/0.96 1969[2:Rew:1946.0,1316.0] || -> equal(e12,e10) equal(op1(e12,e13),e10)** equal(op1(e12,e11),e10). % 0.77/0.96 1970[2:MRR:1969.0,2.0] || -> equal(op1(e12,e13),e10)** equal(op1(e12,e11),e10). % 0.77/0.96 1978[2:Rew:1946.0,1501.7] || SkC137 SkC135 equal(op2(e21,h2(e13)),h2(op1(e10,e13))) equal(op2(e21,h2(e12)),h2(op1(e10,e12))) equal(op2(h2(e13),e21),h2(op1(e13,e10))) equal(h2(op1(e11,e10)),op2(e23,e21)) equal(op2(h2(e13),h2(e13)),h2(op1(e13,e13)))** equal(op2(h2(e12),h2(e12)),h2(e12)) equal(h2(op1(e11,e11)),e23) equal(op2(h2(e13),h2(e12)),h2(op1(e13,e12))) equal(op2(h2(e13),e23),h2(op1(e13,e11))) equal(op2(h2(e12),h2(e13)),h2(op1(e12,e13))) equal(op2(h2(e12),e23),h2(op1(e12,e11))) equal(op2(e23,h2(e13)),h2(op1(e11,e13))) equal(op2(e23,h2(e12)),h2(op1(e11,e12))) -> . % 0.77/0.96 1981[3:Spt:1944.0] || -> equal(op1(e13,e13),e12)**. % 0.77/0.96 1983[3:Rew:1981.0,1958.0] || equal(e12,e12) -> equal(op1(e13,e12),e13)**. % 0.77/0.96 1985[3:Rew:1981.0,363.0] || equal(op1(e11,e13),e12)** -> . % 0.77/0.96 2000[3:MRR:1959.0,1985.0] || -> equal(op1(e11,e10),e12)**. % 0.77/0.96 2008[3:Rew:2000.0,790.1] || -> equal(op1(e11,e11),e10) equal(e12,e10) equal(op1(e11,e13),e10)** equal(op1(e11,e12),e10). % 0.77/0.96 2021[3:Obv:1983.0] || -> equal(op1(e13,e12),e13)**. % 0.77/0.96 2023[3:Rew:2021.0,386.0] || equal(op1(e13,e11),e13)** -> . % 0.77/0.96 2025[3:Rew:2021.0,491.1] || SkC30* equal(e13,e13) -> . % 0.77/0.96 2026[3:Rew:2021.0,460.1] || SkC14* equal(e13,e13) -> . % 0.77/0.96 2028[3:Rew:2021.0,1963.1] || -> equal(op1(e11,e12),e11)** equal(e13,e11). % 0.77/0.96 2032[3:MRR:191.1,2023.0] || SkC55* -> . % 0.77/0.96 2033[3:MRR:1318.0,2023.0] || -> equal(op1(e11,e11),e13)**. % 0.77/0.96 2034[3:MRR:1954.0,2032.0] || -> SkC30 SkC16 SkC14*. % 0.77/0.96 2042[3:Obv:2025.1] || SkC30* -> . % 0.77/0.96 2043[3:MRR:2034.0,2042.0] || -> SkC16 SkC14*. % 0.77/0.96 2044[3:Obv:2026.1] || SkC14* -> . % 0.77/0.96 2045[3:MRR:2043.1,2044.0] || -> SkC16*. % 0.77/0.96 2046[3:MRR:115.0,2045.0] || -> equal(op1(e10,e13),e10)**. % 0.77/0.96 2051[3:Rew:2046.0,359.0] || equal(op1(e11,e13),e10)** -> . % 0.77/0.96 2073[3:MRR:2028.1,5.0] || -> equal(op1(e11,e12),e11)**. % 0.77/0.96 2087[3:Rew:2073.0,2008.3,2033.0,2008.0] || -> equal(e13,e10) equal(e12,e10) equal(op1(e11,e13),e10)** equal(e11,e10). % 0.77/0.96 2088[3:MRR:2087.0,2087.1,2087.2,2087.3,3.0,2.0,2051.0,1.0] || -> . % 0.77/0.96 2098[3:Spt:2088.0,1944.0,1981.0] || equal(op1(e13,e13),e12)** -> . % 0.77/0.96 2099[3:Spt:2088.0,1944.1,1944.2] || -> equal(op1(e13,e13),e11)** equal(op1(e13,e13),e10). % 0.77/0.96 2100[3:MRR:143.1,2098.0] || SkC30* -> . % 0.77/0.96 2101[3:MRR:1954.1,2100.0] || -> SkC55 SkC16 SkC14*. % 0.77/0.96 2102[3:MRR:112.1,2098.0] || SkC14* -> . % 0.77/0.96 2103[3:MRR:2101.2,2102.0] || -> SkC55 SkC16*. % 0.77/0.96 2104[3:MRR:1966.0,2098.0] || -> equal(op1(e11,e13),e12)**. % 0.77/0.96 2106[3:Rew:2104.0,373.0] || equal(op1(e11,e10),e12)** -> . % 0.77/0.96 2112[3:MRR:1967.0,2098.0] || -> equal(op1(e13,e10),e12)**. % 0.77/0.96 2119[3:MRR:1340.1,2106.0] || -> equal(op1(e11,e10),e10)**. % 0.77/0.96 2122[3:Rew:2119.0,371.0] || equal(op1(e11,e11),e10)** -> . % 0.77/0.96 2125[3:Rew:2104.0,1964.0] || -> equal(e13,e12) equal(op1(e10,e13),e13)**. % 0.77/0.96 2126[3:MRR:2125.0,6.0] || -> equal(op1(e10,e13),e13)**. % 0.77/0.96 2129[3:Rew:2126.0,1333.0] || -> equal(e13,e10) equal(op1(e10,e12),e10)**. % 0.77/0.96 2130[3:Rew:2126.0,115.1] || SkC16* -> equal(e13,e10). % 0.77/0.96 2134[3:MRR:2130.1,3.0] || SkC16* -> . % 0.77/0.96 2135[3:MRR:2103.1,2134.0] || -> SkC55*. % 0.77/0.96 2136[3:MRR:191.0,2135.0] || -> equal(op1(e13,e11),e13)**. % 0.77/0.96 2137[3:MRR:539.0,2135.0] || equal(op1(e13,e13),e11)** -> . % 0.77/0.96 2141[3:Rew:2136.0,351.0] || equal(op1(e11,e11),e13)** -> . % 0.77/0.96 2143[3:MRR:2129.0,3.0] || -> equal(op1(e10,e12),e10)**. % 0.77/0.96 2149[3:MRR:2099.0,2137.0] || -> equal(op1(e13,e13),e10)**. % 0.77/0.96 2153[3:Rew:2149.0,364.0] || equal(op1(e12,e13),e10)** -> . % 0.77/0.96 2155[3:MRR:1970.0,2153.0] || -> equal(op1(e12,e11),e10)**. % 0.77/0.96 2156[3:MRR:1968.1,2153.0] || -> equal(op1(e12,e13),e11)**. % 0.77/0.96 2167[3:Rew:2136.0,1307.1,2149.0,1307.0] || -> equal(e11,e10) equal(e13,e11) equal(op1(e13,e12),e11)**. % 0.77/0.96 2168[3:MRR:2167.0,2167.1,1.0,5.0] || -> equal(op1(e13,e12),e11)**. % 0.77/0.96 2173[3:Rew:2143.0,1308.2,2168.0,1308.0] || -> equal(e13,e11) equal(op1(e11,e12),e13)** equal(e13,e10). % 0.77/0.96 2174[3:MRR:2173.0,2173.2,5.0,3.0] || -> equal(op1(e11,e12),e13)**. % 0.77/0.96 2179[3:MRR:1339.1,1339.2,2141.0,2122.0] || -> equal(op1(e11,e11),e11)**. % 0.77/0.96 2189[3:Rew:2174.0,1978.14,2104.0,1978.13,30.0,1978.12,2155.0,1978.12,1426.0,1978.11,2156.0,1978.11,2136.0,1978.10,1426.0,1978.9,2168.0,1978.9,1426.0,1978.8,2179.0,1978.8,30.0,1978.6,2149.0,1978.6,30.0,1978.5,2119.0,1978.5,2112.0,1978.4,30.0,1978.3,2143.0,1978.3,2126.0,1978.2] || SkC137 SkC135 equal(op2(e21,h2(e13)),h2(e13)) equal(op2(e21,h2(e12)),e21) equal(op2(h2(e13),e21),h2(e12)) equal(op2(e23,e21),e21) equal(op2(h2(e13),h2(e13)),e21)** equal(op2(h2(e12),h2(e12)),h2(e12)) equal(e23,e23) equal(op2(h2(e13),h2(e12)),e23) equal(op2(h2(e13),e23),h2(e13)) equal(op2(h2(e12),h2(e13)),e23) equal(op2(h2(e12),e23),e21) equal(op2(e23,h2(e13)),h2(e12)) equal(op2(e23,h2(e12)),h2(e13)) -> . % 0.77/0.96 2190[3:Obv:2189.8] || SkC137 SkC135 equal(op2(e21,h2(e13)),h2(e13)) equal(op2(e21,h2(e12)),e21) equal(op2(h2(e13),e21),h2(e12)) equal(op2(e23,e21),e21) equal(op2(h2(e13),h2(e13)),e21)** equal(op2(h2(e12),h2(e12)),h2(e12)) equal(op2(h2(e13),h2(e12)),e23) equal(op2(h2(e13),e23),h2(e13)) equal(op2(h2(e12),h2(e13)),e23) equal(op2(h2(e12),e23),e21) equal(op2(e23,h2(e13)),h2(e12)) equal(op2(e23,h2(e12)),h2(e13)) -> . % 0.77/0.96 2193[4:Spt:1295.0] || -> equal(h3(e11),e22)**. % 0.77/0.96 2195[4:Rew:2193.0,85.0] || -> equal(op2(e22,e22),e22)**. % 0.77/0.96 2197[4:Rew:2193.0,1477.0] || -> equal(e22,e20) equal(op2(e22,e21),e20)**. % 0.77/0.96 2203[4:Rew:2193.0,1150.0] || equal(op2(e23,e22),e22)** -> . % 0.77/0.96 2206[4:Rew:2193.0,1136.0] || equal(op2(e22,e23),e22)** -> . % 0.77/0.96 2211[4:MRR:1482.0,2203.0] || -> equal(op2(e23,e20),e22)**. % 0.77/0.96 2212[4:MRR:1423.0,2203.0] || -> equal(op2(e23,e22),e21)** equal(op2(e23,e22),e20). % 0.77/0.96 2215[4:Rew:2211.0,393.0] || equal(op2(e21,e20),e22)** -> . % 0.77/0.96 2225[4:MRR:1484.0,2206.0] || -> equal(h2(e12),e22)**. % 0.77/0.96 2226[4:MRR:1478.0,2206.0] || -> equal(op2(e22,e23),e21)**. % 0.77/0.96 2229[4:Rew:2225.0,1490.0] || -> equal(e22,e21) equal(op2(e21,e22),e21)**. % 0.77/0.96 2235[4:Rew:2225.0,57.0] || equal(e22,e22) -> SkC137*. % 0.77/0.96 2239[4:Rew:2225.0,1218.0] || -> equal(op2(e22,e21),h2(e13))**. % 0.77/0.96 2240[4:Rew:2225.0,2190.3] || SkC137 SkC135 equal(op2(e21,h2(e13)),h2(e13)) equal(op2(e21,e22),e21) equal(op2(h2(e13),e21),h2(e12)) equal(op2(e23,e21),e21) equal(op2(h2(e13),h2(e13)),e21)** equal(op2(h2(e12),h2(e12)),h2(e12)) equal(op2(h2(e13),h2(e12)),e23) equal(op2(h2(e13),e23),h2(e13)) equal(op2(h2(e12),h2(e13)),e23) equal(op2(h2(e12),e23),e21) equal(op2(e23,h2(e13)),h2(e12)) equal(op2(e23,h2(e12)),h2(e13)) -> . % 0.77/0.96 2247[4:Obv:2235.0] || -> SkC137*. % 0.77/0.96 2248[4:MRR:1299.1,2215.0] || -> equal(op2(e21,e20),e20)**. % 0.77/0.96 2260[4:Rew:2239.0,400.0] || equal(op2(e23,e21),h2(e13))** -> . % 0.77/0.96 2265[4:Rew:2239.0,2197.1] || -> equal(e22,e20) equal(h2(e13),e20)**. % 0.77/0.96 2266[4:MRR:2265.0,8.0] || -> equal(h2(e13),e20)**. % 0.77/0.96 2267[4:Rew:2266.0,50.0] || equal(e20,e20) -> SkC135*. % 0.77/0.96 2272[4:Rew:2266.0,2260.0] || equal(op2(e23,e21),e20)** -> . % 0.77/0.96 2273[4:Obv:2267.0] || -> SkC135*. % 0.77/0.96 2274[4:MRR:1427.1,2272.0] || -> equal(op2(e23,e21),e21)**. % 0.77/0.96 2277[4:Rew:2274.0,434.0] || equal(op2(e23,e22),e21)** -> . % 0.77/0.96 2279[4:MRR:2229.0,10.0] || -> equal(op2(e21,e22),e21)**. % 0.77/0.96 2284[4:MRR:2212.0,2277.0] || -> equal(op2(e23,e22),e20)**. % 0.77/0.96 2288[4:Rew:2284.0,2240.13,2225.0,2240.13,2266.0,2240.13,2211.0,2240.12,2266.0,2240.12,2225.0,2240.12,2226.0,2240.11,2225.0,2240.11,1184.0,2240.10,2225.0,2240.10,2266.0,2240.10,1449.0,2240.9,2266.0,2240.9,1448.0,2240.8,2266.0,2240.8,2225.0,2240.8,2195.0,2240.7,2225.0,2240.7,34.0,2240.6,2266.0,2240.6,2274.0,2240.5,854.0,2240.4,2266.0,2240.4,2225.0,2240.4,2279.0,2240.3,2248.0,2240.2,2266.0,2240.2] || SkC137 SkC135* equal(e20,e20) equal(e21,e21) equal(e22,e22) equal(e21,e21) equal(e21,e21) equal(e22,e22) equal(e23,e23) equal(e20,e20) equal(e23,e23) equal(e21,e21) equal(e22,e22) equal(e20,e20) -> . % 0.77/0.96 2289[4:Obv:2288.13] || SkC137 SkC135* -> . % 0.77/0.96 2290[4:MRR:2289.0,2289.1,2247.0,2273.0] || -> . % 0.77/0.96 2295[4:Spt:2290.0,1295.0,2193.0] || equal(h3(e11),e22)** -> . % 0.77/0.96 2296[4:Spt:2290.0,1295.1,1295.2] || -> equal(h3(e11),e21)** equal(h3(e11),e20). % 0.77/0.96 2297[4:MRR:948.1,2295.0] || SkC68* -> . % 0.77/0.96 2298[4:MRR:1481.0,2297.0] || -> equal(h2(e12),e21)**. % 0.77/0.96 2303[4:Rew:2298.0,1468.1] || SkC114* equal(e21,e21) -> . % 0.77/0.96 2304[4:Obv:2303.1] || SkC114* -> . % 0.77/0.96 2305[4:MRR:1429.0,2304.0] || -> SkC82*. % 0.77/0.96 2306[4:Rew:2298.0,1467.1] || SkC82* equal(e21,e21) -> . % 0.77/0.96 2307[4:Obv:2306.1] || SkC82* -> . % 0.77/0.96 2308[4:MRR:2307.0,2305.0] || -> . % 0.77/0.96 2330[1:Spt:2308.0,1290.0,1388.0] || equal(h4(e11),e23)** -> . % 0.77/0.96 2331[1:Spt:2308.0,1290.1,1290.2,1290.3] || -> equal(h4(e11),e22)** equal(h4(e11),e21) equal(h4(e11),e20). % 0.77/0.96 2332[1:MRR:1229.1,2330.0] || -> SkC68*. % 0.77/0.96 2333[1:MRR:948.0,2332.0] || -> equal(h3(e11),e22)**. % 0.77/0.96 2337[1:Rew:2333.0,85.0] || -> equal(op2(e22,e22),e22)**. % 0.77/0.96 2340[1:Rew:2333.0,1150.0] || equal(op2(e23,e22),e22)** -> . % 0.77/0.96 2341[1:Rew:2333.0,1151.0] || equal(op2(e21,e22),e22)** -> . % 0.77/0.96 2342[1:Rew:2333.0,868.1] || SkC123* -> equal(e22,e21). % 0.77/0.96 2343[1:MRR:2342.1,10.0] || SkC123* -> . % 0.77/0.96 2344[1:MRR:1348.0,2343.0] || -> SkC121 SkC114 SkC96 SkC82 SkC80*. % 0.77/0.96 2352[1:Rew:2333.0,1136.0] || equal(op2(e22,e23),e22)** -> . % 0.77/0.96 2353[1:MRR:303.1,2352.0] || SkC114* -> . % 0.77/0.96 2354[1:MRR:2344.1,2353.0] || -> SkC121 SkC96 SkC82 SkC80*. % 0.77/0.96 2356[1:MRR:1220.0,2332.0] || equal(h4(e11),e22) -> equal(op2(e23,e22),e23)**. % 0.77/0.96 2357[1:Rew:2333.0,1263.0] || -> equal(e22,e21) equal(op2(e21,e22),e21) equal(op2(e23,e22),e21)**. % 0.77/0.96 2358[1:MRR:2357.0,10.0] || -> equal(op2(e21,e22),e21) equal(op2(e23,e22),e21)**. % 0.77/0.96 2361[1:MRR:1243.0,2330.0] || -> equal(op2(e21,e23),e23)** equal(op2(e20,e23),e23). % 0.77/0.96 2363[1:MRR:1247.1,2352.0] || -> equal(h4(e11),e22) equal(op2(e21,e23),e22)**. % 0.77/0.96 2364[1:MRR:1249.1,2340.0] || -> equal(h4(e11),e22) equal(op2(e23,e20),e22)**. % 0.77/0.96 2365[1:Rew:2333.0,1268.0] || -> equal(e22,e20) equal(op2(e22,e23),e20)** equal(op2(e22,e21),e20). % 0.77/0.96 2366[1:MRR:2365.0,8.0] || -> equal(op2(e22,e23),e20)** equal(op2(e22,e21),e20). % 0.77/0.96 2367[1:MRR:1274.0,2341.0] || -> equal(op2(e21,e23),e22)** equal(op2(e21,e20),e22). % 0.77/0.96 2368[1:MRR:1293.0,2352.0] || -> equal(op2(e22,e23),e21)** equal(op2(e22,e23),e20). % 0.77/0.96 2373[1:Rew:2333.0,1381.2] || equal(h1(op1(e11,e11)),h2(e11)) equal(h1(op1(e13,e13)),h4(e11))** equal(h1(op1(e12,e12)),e22) equal(h1(op1(e13,e12)),op2(e23,e22)) equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e10)),op2(e23,e20)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e11,e13)),op2(e21,e23)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e10)),op2(e21,e20)) equal(h1(op1(e10,e13)),op2(e20,e23)) equal(h1(op1(e10,e12)),op2(e20,e22)) -> . % 0.77/0.96 2376[2:Spt:2331.0] || -> equal(h4(e11),e22)**. % 0.77/0.96 2386[2:Rew:2376.0,2356.0] || equal(e22,e22) -> equal(op2(e23,e22),e23)**. % 0.77/0.96 2389[2:Rew:2376.0,1148.0] || equal(op2(e21,e23),e22)** -> . % 0.77/0.96 2394[2:Rew:2376.0,992.0] || -> equal(op2(e23,e22),h4(e12))**. % 0.77/0.96 2398[2:MRR:2367.0,2389.0] || -> equal(op2(e21,e20),e22)**. % 0.77/0.96 2404[2:Rew:2398.0,1281.1] || -> equal(h2(e11),e20) equal(e22,e20) equal(op2(e21,e23),e20)** equal(op2(e21,e22),e20). % 0.77/0.96 2414[2:Rew:2394.0,434.0] || equal(op2(e23,e21),h4(e12))** -> . % 0.77/0.96 2420[2:Rew:2394.0,615.1] || SkC96 equal(h4(e12),e23)** -> . % 0.77/0.96 2421[2:Rew:2394.0,584.1] || SkC80 equal(h4(e12),e23)** -> . % 0.77/0.96 2423[2:Rew:2394.0,2358.1] || -> equal(op2(e21,e22),e21)** equal(h4(e12),e21). % 0.77/0.96 2429[2:Obv:2386.0] || -> equal(op2(e23,e22),e23)**. % 0.77/0.96 2430[2:Rew:2394.0,2429.0] || -> equal(h4(e12),e23)**. % 0.77/0.96 2436[2:Rew:2430.0,2414.0] || equal(op2(e23,e21),e23)** -> . % 0.77/0.96 2438[2:Rew:2430.0,2421.1] || SkC80* equal(e23,e23) -> . % 0.77/0.96 2439[2:Rew:2430.0,2420.1] || SkC96* equal(e23,e23) -> . % 0.77/0.96 2444[2:MRR:317.1,2436.0] || SkC121* -> . % 0.77/0.96 2445[2:MRR:1270.1,2436.0] || -> equal(h2(e11),e23)**. % 0.77/0.96 2446[2:MRR:2354.0,2444.0] || -> SkC96 SkC82 SkC80*. % 0.77/0.96 2455[2:Rew:2445.0,994.0] || -> equal(op2(e21,e23),h2(e12))**. % 0.77/0.96 2461[2:Obv:2438.1] || SkC80* -> . % 0.77/0.96 2462[2:MRR:2446.2,2461.0] || -> SkC96 SkC82*. % 0.77/0.96 2463[2:Obv:2439.1] || SkC96* -> . % 0.77/0.96 2464[2:MRR:2462.0,2463.0] || -> SkC82*. % 0.77/0.96 2465[2:MRR:241.0,2464.0] || -> equal(op2(e20,e23),e20)**. % 0.77/0.96 2470[2:Rew:2465.0,407.0] || equal(op2(e21,e23),e20)** -> . % 0.77/0.96 2486[2:Rew:2455.0,2470.0] || equal(h2(e12),e20)** -> . % 0.77/0.96 2504[2:Rew:2430.0,2423.1] || -> equal(op2(e21,e22),e21)** equal(e23,e21). % 0.77/0.96 2505[2:MRR:2504.1,11.0] || -> equal(op2(e21,e22),e21)**. % 0.77/0.96 2516[2:Rew:2505.0,2404.3,2455.0,2404.2,2445.0,2404.0] || -> equal(e23,e20) equal(e22,e20) equal(h2(e12),e20)** equal(e21,e20). % 0.77/0.96 2517[2:MRR:2516.0,2516.1,2516.2,2516.3,9.0,8.0,2486.0,7.0] || -> . % 0.77/0.96 2524[2:Spt:2517.0,2331.0,2376.0] || equal(h4(e11),e22)** -> . % 0.77/0.96 2525[2:Spt:2517.0,2331.1,2331.2] || -> equal(h4(e11),e21)** equal(h4(e11),e20). % 0.77/0.96 2526[2:MRR:900.1,2524.0] || SkC96* -> . % 0.77/0.96 2527[2:MRR:2354.1,2526.0] || -> SkC121 SkC82 SkC80*. % 0.77/0.96 2528[2:MRR:921.1,2524.0] || SkC80* -> . % 0.77/0.96 2529[2:MRR:2527.2,2528.0] || -> SkC121 SkC82*. % 0.77/0.96 2530[2:MRR:2363.0,2524.0] || -> equal(op2(e21,e23),e22)**. % 0.77/0.96 2533[2:Rew:2530.0,421.0] || equal(op2(e21,e20),e22)** -> . % 0.77/0.96 2538[2:MRR:2364.0,2524.0] || -> equal(op2(e23,e20),e22)**. % 0.77/0.96 2545[2:MRR:1299.1,2533.0] || -> equal(op2(e21,e20),e20)**. % 0.77/0.96 2548[2:Rew:2545.0,1141.0] || equal(h2(e11),e20)** -> . % 0.77/0.96 2551[2:Rew:2530.0,2361.0] || -> equal(e23,e22) equal(op2(e20,e23),e23)**. % 0.77/0.96 2552[2:MRR:2551.0,12.0] || -> equal(op2(e20,e23),e23)**. % 0.77/0.96 2556[2:Rew:2552.0,1289.0] || -> equal(e23,e20) equal(op2(e20,e22),e20)**. % 0.77/0.96 2557[2:Rew:2552.0,241.1] || SkC82* -> equal(e23,e20). % 0.77/0.96 2560[2:MRR:2557.1,9.0] || SkC82* -> . % 0.77/0.96 2561[2:MRR:2529.1,2560.0] || -> SkC121*. % 0.77/0.96 2562[2:MRR:1013.0,2561.0] || equal(h4(e11),e21)** -> . % 0.77/0.96 2563[2:MRR:317.0,2561.0] || -> equal(op2(e23,e21),e23)**. % 0.77/0.96 2564[2:MRR:2525.0,2562.0] || -> equal(h4(e11),e20)**. % 0.77/0.96 2567[2:Rew:2564.0,72.0] || equal(e20,e20) -> SkC141*. % 0.77/0.96 2569[2:Rew:2564.0,992.0] || -> equal(op2(e23,e20),h4(e12))**. % 0.77/0.96 2572[2:Rew:2564.0,1147.0] || equal(op2(e22,e23),e20)** -> . % 0.77/0.96 2575[2:Rew:2563.0,1153.0] || equal(h2(e11),e23)** -> . % 0.77/0.96 2578[2:Obv:2567.0] || -> SkC141*. % 0.77/0.96 2579[2:Rew:2538.0,2569.0] || -> equal(h4(e12),e22)**. % 0.77/0.96 2580[2:Rew:2579.0,81.0] || equal(e22,e22) -> SkC143*. % 0.77/0.96 2582[2:Rew:2579.0,1216.0] || -> equal(op2(e22,e23),h4(e13))**. % 0.77/0.96 2583[2:Obv:2580.0] || -> SkC143*. % 0.77/0.96 2588[2:Rew:2582.0,2572.0] || equal(h4(e13),e20)** -> . % 0.77/0.96 2589[2:MRR:2556.0,9.0] || -> equal(op2(e20,e22),e20)**. % 0.77/0.96 2595[2:Rew:2582.0,2368.1,2582.0,2368.0] || -> equal(h4(e13),e21)** equal(h4(e13),e20). % 0.77/0.96 2596[2:MRR:2595.1,2588.0] || -> equal(h4(e13),e21)**. % 0.77/0.96 2597[2:Rew:2596.0,78.0] || equal(e21,e21) -> SkC142*. % 0.77/0.96 2598[2:Rew:2596.0,2582.0] || -> equal(op2(e22,e23),e21)**. % 0.77/0.96 2603[2:Obv:2597.0] || -> SkC142*. % 0.77/0.96 2604[2:Rew:2598.0,2366.0] || -> equal(e21,e20) equal(op2(e22,e21),e20)**. % 0.77/0.96 2605[2:MRR:2604.0,7.0] || -> equal(op2(e22,e21),e20)**. % 0.77/0.96 2610[2:MRR:1298.0,1298.2,2575.0,2548.0] || -> equal(h2(e11),e21)**. % 0.77/0.96 2612[2:Rew:2610.0,84.0] || -> equal(op2(e21,e21),e21)**. % 0.77/0.96 2614[2:Rew:2610.0,1140.0] || equal(op2(e21,e22),e21)** -> . % 0.77/0.96 2621[2:MRR:2358.0,2614.0] || -> equal(op2(e23,e22),e21)**. % 0.77/0.96 2629[2:Rew:2530.0,1272.1,2610.0,1272.0] || -> equal(e23,e21) equal(e23,e22) equal(op2(e21,e22),e23)**. % 0.77/0.96 2630[2:MRR:2629.0,2629.1,11.0,12.0] || -> equal(op2(e21,e22),e23)**. % 0.77/0.96 2634[2:Rew:2589.0,2373.12,2552.0,2373.11,2545.0,2373.10,2630.0,2373.9,2530.0,2373.8,2605.0,2373.7,2598.0,2373.6,2538.0,2373.5,2563.0,2373.4,2621.0,2373.3,2564.0,2373.1,2610.0,2373.0] || equal(h1(op1(e11,e11)),e21) equal(h1(op1(e13,e13)),e20)** equal(h1(op1(e12,e12)),e22) equal(h1(op1(e13,e12)),e21) equal(h1(op1(e13,e11)),e23) equal(h1(op1(e13,e10)),e22) equal(h1(op1(e12,e13)),e21) equal(h1(op1(e12,e11)),e20) equal(h1(op1(e11,e13)),e22) equal(h1(op1(e11,e12)),e23) equal(h1(op1(e11,e10)),e20) equal(h1(op1(e10,e13)),e23) equal(h1(op1(e10,e12)),e20) -> . % 0.77/0.96 2635[2:Rew:2589.0,1359.15,2564.0,1359.15,2579.0,1359.15,854.0,1359.14,2564.0,1359.14,2596.0,1359.14,1184.0,1359.13,2579.0,1359.13,2564.0,1359.13,2605.0,1359.12,2579.0,1359.12,2596.0,1359.12,2545.0,1359.11,2596.0,1359.11,2564.0,1359.11,2630.0,1359.10,2596.0,1359.10,2579.0,1359.10,34.0,1359.9,2564.0,1359.9,2337.0,1359.8,2579.0,1359.8,2612.0,1359.7,2596.0,1359.7,2552.0,1359.6,2564.0,1359.6,2530.0,1359.5,2596.0,1359.5,2621.0,1359.4,2579.0,1359.4,2563.0,1359.3,2596.0,1359.3] || SkC143 SkC142 SkC141 equal(h4(op1(e10,e13)),e23) equal(h4(op1(e10,e12)),e21) equal(h4(op1(e13,e10)),e22) equal(h4(op1(e11,e10)),e23) equal(h4(op1(e13,e13)),e21)** equal(h4(op1(e12,e12)),e22) equal(h4(op1(e11,e11)),e21) equal(h4(op1(e13,e12)),e23) equal(h4(op1(e13,e11)),e20) equal(h4(op1(e12,e13)),e20) equal(h4(op1(e12,e11)),e23) equal(h4(op1(e11,e13)),e22) equal(h4(op1(e11,e12)),e20) -> . % 0.77/0.96 2636[2:MRR:2635.0,2635.1,2635.2,2583.0,2603.0,2578.0] || equal(h4(op1(e10,e13)),e23) equal(h4(op1(e10,e12)),e21) equal(h4(op1(e13,e10)),e22) equal(h4(op1(e11,e10)),e23) equal(h4(op1(e13,e13)),e21)** equal(h4(op1(e12,e12)),e22) equal(h4(op1(e11,e11)),e21) equal(h4(op1(e13,e12)),e23) equal(h4(op1(e13,e11)),e20) equal(h4(op1(e12,e13)),e20) equal(h4(op1(e12,e11)),e23) equal(h4(op1(e11,e13)),e22) equal(h4(op1(e11,e12)),e20) -> . % 0.77/0.96 2640[3:Spt:799.0] || -> equal(op1(e13,e13),e13)**. % 0.77/0.96 2641[3:Rew:2640.0,1305.0] || -> equal(e13,e12) equal(op1(e13,e12),e12)** equal(op1(e13,e10),e12). % 0.77/0.96 2642[3:Rew:2640.0,1304.0] || -> equal(e13,e12) equal(op1(e12,e13),e12)** equal(op1(e11,e13),e12). % 0.77/0.96 2644[3:Rew:2640.0,112.1] || SkC14* -> equal(e13,e12). % 0.77/0.96 2645[3:Rew:2640.0,143.1] || SkC30* -> equal(e13,e12). % 0.77/0.96 2648[3:Rew:2640.0,361.0] || equal(op1(e10,e13),e13)** -> . % 0.77/0.96 2653[3:Rew:2640.0,387.0] || equal(op1(e13,e11),e13)** -> . % 0.77/0.96 2655[3:Rew:2640.0,388.0] || equal(op1(e13,e12),e13)** -> . % 0.77/0.96 2659[3:Rew:2640.0,2636.4] || equal(h4(op1(e10,e13)),e23) equal(h4(op1(e10,e12)),e21) equal(h4(op1(e13,e10)),e22) equal(h4(op1(e11,e10)),e23) equal(h4(e13),e21) equal(h4(op1(e12,e12)),e22) equal(h4(op1(e11,e11)),e21) equal(h4(op1(e13,e12)),e23)** equal(h4(op1(e13,e11)),e20) equal(h4(op1(e12,e13)),e20) equal(h4(op1(e12,e11)),e23) equal(h4(op1(e11,e13)),e22) equal(h4(op1(e11,e12)),e20) -> . % 0.77/0.96 2660[3:MRR:2644.1,6.0] || SkC14* -> . % 0.77/0.96 2661[3:MRR:1351.5,2660.0] || -> SkC57 SkC55 SkC48 SkC30 SkC16*. % 0.77/0.96 2662[3:MRR:2645.1,6.0] || SkC30* -> . % 0.77/0.96 2663[3:MRR:2661.3,2662.0] || -> SkC57 SkC55 SkC48 SkC16*. % 0.77/0.96 2666[3:MRR:1341.0,2648.0] || -> equal(op1(e10,e13),e10)**. % 0.77/0.96 2667[3:MRR:1327.0,2648.0] || -> equal(op1(e10,e12),e13)**. % 0.77/0.96 2672[3:Rew:2666.0,360.0] || equal(op1(e12,e13),e10)** -> . % 0.77/0.96 2680[3:MRR:191.1,2653.0] || SkC55* -> . % 0.77/0.96 2681[3:MRR:195.1,2653.0] || SkC57* -> . % 0.77/0.96 2682[3:MRR:1318.0,2653.0] || -> equal(op1(e11,e11),e13)**. % 0.77/0.96 2684[3:MRR:2663.1,2680.0] || -> SkC57 SkC48 SkC16*. % 0.77/0.96 2685[3:MRR:2684.0,2681.0] || -> SkC48 SkC16*. % 0.77/0.96 2687[3:Rew:2682.0,1240.0] || equal(e13,e13) -> SkC2 equal(op1(e11,e13),e11)**. % 0.77/0.96 2695[3:Rew:2682.0,1323.0] || -> equal(e13,e11) equal(op1(e11,e13),e11)** equal(op1(e11,e12),e11). % 0.77/0.96 2696[3:Rew:2682.0,1322.0] || -> equal(e13,e11) equal(op1(e13,e11),e11)** equal(op1(e12,e11),e11). % 0.77/0.96 2697[3:MRR:800.0,2655.0] || -> equal(op1(e13,e12),e12)** equal(op1(e13,e12),e11) equal(op1(e13,e12),e10). % 0.77/0.96 2699[3:MRR:1336.2,2672.0] || -> equal(op1(e12,e13),e12)** equal(op1(e12,e13),e11). % 0.77/0.96 2702[3:Obv:2687.0] || -> SkC2 equal(op1(e11,e13),e11)**. % 0.77/0.96 2703[3:MRR:2641.0,6.0] || -> equal(op1(e13,e12),e12)** equal(op1(e13,e10),e12). % 0.77/0.96 2704[3:MRR:2642.0,6.0] || -> equal(op1(e12,e13),e12)** equal(op1(e11,e13),e12). % 0.77/0.96 2708[3:MRR:2695.0,5.0] || -> equal(op1(e11,e13),e11)** equal(op1(e11,e12),e11). % 0.77/0.96 2709[3:MRR:2696.0,5.0] || -> equal(op1(e13,e11),e11)** equal(op1(e12,e11),e11). % 0.77/0.96 2716[3:Rew:2596.0,2659.6,2682.0,2659.6,2596.0,2659.4,2596.0,2659.1,2667.0,2659.1,32.0,2659.0,2666.0,2659.0] || equal(e23,e23) equal(e21,e21) equal(h4(op1(e13,e10)),e22) equal(h4(op1(e11,e10)),e23) equal(e21,e21) equal(h4(op1(e12,e12)),e22) equal(e21,e21) equal(h4(op1(e13,e12)),e23)** equal(h4(op1(e13,e11)),e20) equal(h4(op1(e12,e13)),e20) equal(h4(op1(e12,e11)),e23) equal(h4(op1(e11,e13)),e22) equal(h4(op1(e11,e12)),e20) -> . % 0.77/0.96 2717[3:Obv:2716.6] || equal(h4(op1(e13,e10)),e22) equal(h4(op1(e11,e10)),e23) equal(h4(op1(e12,e12)),e22) equal(h4(op1(e13,e12)),e23)** equal(h4(op1(e13,e11)),e20) equal(h4(op1(e12,e13)),e20) equal(h4(op1(e12,e11)),e23) equal(h4(op1(e11,e13)),e22) equal(h4(op1(e11,e12)),e20) -> . % 0.77/0.96 2719[4:Spt:1309.0] || -> equal(op1(e12,e12),e12)**. % 0.77/0.96 2723[4:Rew:2719.0,358.0] || equal(op1(e13,e12),e12)** -> . % 0.77/0.96 2724[4:Rew:2719.0,382.0] || equal(op1(e12,e13),e12)** -> . % 0.77/0.96 2729[4:Rew:2719.0,2717.2] || equal(h4(op1(e13,e10)),e22) equal(h4(op1(e11,e10)),e23) equal(h4(e12),e22) equal(h4(op1(e13,e12)),e23)** equal(h4(op1(e13,e11)),e20) equal(h4(op1(e12,e13)),e20) equal(h4(op1(e12,e11)),e23) equal(h4(op1(e11,e13)),e22) equal(h4(op1(e11,e12)),e20) -> . % 0.77/0.96 2730[4:MRR:2703.0,2723.0] || -> equal(op1(e13,e10),e12)**. % 0.77/0.96 2731[4:MRR:2697.0,2723.0] || -> equal(op1(e13,e12),e11)** equal(op1(e13,e12),e10). % 0.77/0.96 2736[4:Rew:2730.0,345.0] || equal(op1(e11,e10),e12)** -> . % 0.77/0.96 2740[4:MRR:2699.0,2724.0] || -> equal(op1(e12,e13),e11)**. % 0.77/0.96 2741[4:MRR:2704.0,2724.0] || -> equal(op1(e11,e13),e12)**. % 0.77/0.96 2746[4:Rew:2740.0,381.0] || equal(op1(e12,e11),e11)** -> . % 0.77/0.96 2750[4:Rew:2741.0,2708.0] || -> equal(e12,e11) equal(op1(e11,e12),e11)**. % 0.77/0.96 2757[4:MRR:1340.1,2736.0] || -> equal(op1(e11,e10),e10)**. % 0.77/0.96 2764[4:MRR:1338.0,2746.0] || -> equal(op1(e12,e11),e10)**. % 0.77/0.96 2765[4:MRR:2709.1,2746.0] || -> equal(op1(e13,e11),e11)**. % 0.77/0.96 2771[4:Rew:2765.0,386.0] || equal(op1(e13,e12),e11)** -> . % 0.77/0.96 2775[4:MRR:2750.0,4.0] || -> equal(op1(e11,e12),e11)**. % 0.77/0.96 2780[4:MRR:2731.0,2771.0] || -> equal(op1(e13,e12),e10)**. % 0.77/0.96 2784[4:Rew:2564.0,2729.8,2775.0,2729.8,2579.0,2729.7,2741.0,2729.7,32.0,2729.6,2764.0,2729.6,2564.0,2729.5,2740.0,2729.5,2564.0,2729.4,2765.0,2729.4,32.0,2729.3,2780.0,2729.3,2579.0,2729.2,32.0,2729.1,2757.0,2729.1,2579.0,2729.0,2730.0,2729.0] || equal(e22,e22) equal(e23,e23)* equal(e22,e22) equal(e23,e23)* equal(e20,e20) equal(e20,e20) equal(e23,e23)* equal(e22,e22) equal(e20,e20) -> . % 0.77/0.96 2785[4:Obv:2784.8] || -> . % 0.77/0.96 2786[4:Spt:2785.0,1309.0,2719.0] || equal(op1(e12,e12),e12)** -> . % 0.77/0.96 2787[4:Spt:2785.0,1309.1,1309.2] || -> equal(op1(e13,e12),e12)** equal(op1(e11,e12),e12). % 0.77/0.96 2788[4:MRR:89.1,2786.0] || SkC2* -> . % 0.77/0.96 2789[4:MRR:2702.0,2788.0] || -> equal(op1(e11,e13),e11)**. % 0.77/0.96 2792[4:Rew:2789.0,526.1] || SkC48* equal(e11,e11) -> . % 0.77/0.96 2793[4:Obv:2792.1] || SkC48* -> . % 0.77/0.96 2794[4:MRR:2685.0,2793.0] || -> SkC16*. % 0.77/0.96 2795[4:Rew:2789.0,464.1] || SkC16* equal(e11,e11) -> . % 0.77/0.96 2796[4:Obv:2795.1] || SkC16* -> . % 0.77/0.96 2797[4:MRR:2796.0,2794.0] || -> . % 0.77/0.96 2816[3:Spt:2797.0,799.0,2640.0] || equal(op1(e13,e13),e13)** -> . % 0.77/0.96 2817[3:Spt:2797.0,799.1,799.2,799.3] || -> equal(op1(e13,e13),e12)** equal(op1(e13,e13),e11) equal(op1(e13,e13),e10). % 0.77/0.96 2818[3:MRR:1235.1,2816.0] || -> SkC2*. % 0.77/0.96 2819[3:MRR:89.0,2818.0] || -> equal(op1(e12,e12),e12)**. % 0.77/0.97 2823[3:Rew:2819.0,358.0] || equal(op1(e13,e12),e12)** -> . % 0.77/0.97 2824[3:Rew:2819.0,196.1] || SkC57* -> equal(e12,e11). % 0.77/0.97 2825[3:MRR:2824.1,4.0] || SkC57* -> . % 0.77/0.97 2826[3:MRR:1351.0,2825.0] || -> SkC55 SkC48 SkC30 SkC16 SkC14*. % 0.77/0.97 2827[3:Rew:2819.0,382.0] || equal(op1(e12,e13),e12)** -> . % 0.77/0.97 2828[3:MRR:177.1,2827.0] || SkC48* -> . % 0.77/0.97 2829[3:MRR:2826.1,2828.0] || -> SkC55 SkC30 SkC16 SkC14*. % 0.77/0.97 2831[3:MRR:703.0,2818.0] || equal(op1(e13,e13),e12)** -> equal(op1(e13,e12),e13). % 0.77/0.97 2834[3:Rew:2819.0,1312.0] || -> equal(e12,e11) equal(op1(e11,e12),e11) equal(op1(e13,e12),e11)**. % 0.77/0.97 2835[3:MRR:2834.0,4.0] || -> equal(op1(e11,e12),e11) equal(op1(e13,e12),e11)**. % 0.77/0.97 2837[3:MRR:1302.0,2816.0] || -> equal(op1(e11,e13),e13)** equal(op1(e10,e13),e13). % 0.77/0.97 2839[3:MRR:1304.1,2827.0] || -> equal(op1(e13,e13),e12)** equal(op1(e11,e13),e12). % 0.77/0.97 2840[3:MRR:1305.1,2823.0] || -> equal(op1(e13,e13),e12)** equal(op1(e13,e10),e12). % 0.77/0.97 2841[3:Rew:2819.0,1316.0] || -> equal(e12,e10) equal(op1(e12,e13),e10)** equal(op1(e12,e11),e10). % 0.77/0.97 2842[3:MRR:2841.0,2.0] || -> equal(op1(e12,e13),e10)** equal(op1(e12,e11),e10). % 0.77/0.97 2843[3:MRR:1336.0,2827.0] || -> equal(op1(e12,e13),e11)** equal(op1(e12,e13),e10). % 0.77/0.97 2848[3:Rew:995.0,2634.2,2819.0,2634.2] || equal(h1(op1(e11,e11)),e21) equal(h1(op1(e13,e13)),e20)** equal(e22,e22) equal(h1(op1(e13,e12)),e21) equal(h1(op1(e13,e11)),e23) equal(h1(op1(e13,e10)),e22) equal(h1(op1(e12,e13)),e21) equal(h1(op1(e12,e11)),e20) equal(h1(op1(e11,e13)),e22) equal(h1(op1(e11,e12)),e23) equal(h1(op1(e11,e10)),e20) equal(h1(op1(e10,e13)),e23) equal(h1(op1(e10,e12)),e20) -> . % 0.77/0.97 2849[3:Obv:2848.2] || equal(h1(op1(e11,e11)),e21) equal(h1(op1(e13,e13)),e20)** equal(h1(op1(e13,e12)),e21) equal(h1(op1(e13,e11)),e23) equal(h1(op1(e13,e10)),e22) equal(h1(op1(e12,e13)),e21) equal(h1(op1(e12,e11)),e20) equal(h1(op1(e11,e13)),e22) equal(h1(op1(e11,e12)),e23) equal(h1(op1(e11,e10)),e20) equal(h1(op1(e10,e13)),e23) equal(h1(op1(e10,e12)),e20) -> . % 0.77/0.97 2852[4:Spt:2817.0] || -> equal(op1(e13,e13),e12)**. % 0.77/0.97 2854[4:Rew:2852.0,2831.0] || equal(e12,e12) -> equal(op1(e13,e12),e13)**. % 0.77/0.97 2862[4:Rew:2852.0,385.0] || equal(op1(e13,e10),e12)** -> . % 0.77/0.97 2868[4:MRR:1329.0,2862.0] || -> equal(op1(e11,e10),e12)**. % 0.77/0.97 2874[4:Rew:2868.0,790.1] || -> equal(op1(e11,e11),e10) equal(e12,e10) equal(op1(e11,e13),e10)** equal(op1(e11,e12),e10). % 0.77/0.97 2889[4:Obv:2854.0] || -> equal(op1(e13,e12),e13)**. % 0.77/0.97 2890[4:Rew:2889.0,386.0] || equal(op1(e13,e11),e13)** -> . % 0.77/0.97 2893[4:Rew:2889.0,491.1] || SkC30* equal(e13,e13) -> . % 0.77/0.97 2894[4:Rew:2889.0,460.1] || SkC14* equal(e13,e13) -> . % 0.77/0.97 2896[4:Rew:2889.0,2835.1] || -> equal(op1(e11,e12),e11)** equal(e13,e11). % 0.77/0.97 2898[4:MRR:191.1,2890.0] || SkC55* -> . % 0.77/0.97 2899[4:MRR:1318.0,2890.0] || -> equal(op1(e11,e11),e13)**. % 0.77/0.97 2900[4:MRR:2829.0,2898.0] || -> SkC30 SkC16 SkC14*. % 0.77/0.97 2909[4:Obv:2893.1] || SkC30* -> . % 0.77/0.97 2910[4:MRR:2900.0,2909.0] || -> SkC16 SkC14*. % 0.77/0.97 2911[4:Obv:2894.1] || SkC14* -> . % 0.77/0.97 2912[4:MRR:2910.1,2911.0] || -> SkC16*. % 0.77/0.97 2913[4:MRR:115.0,2912.0] || -> equal(op1(e10,e13),e10)**. % 0.77/0.97 2919[4:Rew:2913.0,359.0] || equal(op1(e11,e13),e10)** -> . % 0.77/0.97 2941[4:MRR:2896.1,5.0] || -> equal(op1(e11,e12),e11)**. % 0.77/0.97 2955[4:Rew:2941.0,2874.3,2899.0,2874.0] || -> equal(e13,e10) equal(e12,e10) equal(op1(e11,e13),e10)** equal(e11,e10). % 0.77/0.97 2956[4:MRR:2955.0,2955.1,2955.2,2955.3,3.0,2.0,2919.0,1.0] || -> . % 0.77/0.97 2961[4:Spt:2956.0,2817.0,2852.0] || equal(op1(e13,e13),e12)** -> . % 0.77/0.97 2962[4:Spt:2956.0,2817.1,2817.2] || -> equal(op1(e13,e13),e11)** equal(op1(e13,e13),e10). % 0.77/0.97 2963[4:MRR:143.1,2961.0] || SkC30* -> . % 0.77/0.97 2964[4:MRR:2829.1,2963.0] || -> SkC55 SkC16 SkC14*. % 0.77/0.97 2965[4:MRR:112.1,2961.0] || SkC14* -> . % 0.77/0.97 2966[4:MRR:2964.2,2965.0] || -> SkC55 SkC16*. % 0.77/0.97 2967[4:MRR:2839.0,2961.0] || -> equal(op1(e11,e13),e12)**. % 0.77/0.97 2969[4:Rew:2967.0,373.0] || equal(op1(e11,e10),e12)** -> . % 0.77/0.97 2975[4:MRR:2840.0,2961.0] || -> equal(op1(e13,e10),e12)**. % 0.77/0.97 2982[4:MRR:1340.1,2969.0] || -> equal(op1(e11,e10),e10)**. % 0.77/0.97 2985[4:Rew:2982.0,371.0] || equal(op1(e11,e11),e10)** -> . % 0.77/0.97 2988[4:Rew:2967.0,2837.0] || -> equal(e13,e12) equal(op1(e10,e13),e13)**. % 0.77/0.97 2989[4:MRR:2988.0,6.0] || -> equal(op1(e10,e13),e13)**. % 0.77/0.97 2992[4:Rew:2989.0,1333.0] || -> equal(e13,e10) equal(op1(e10,e12),e10)**. % 0.77/0.97 2993[4:Rew:2989.0,115.1] || SkC16* -> equal(e13,e10). % 0.77/0.97 2997[4:MRR:2993.1,3.0] || SkC16* -> . % 0.77/0.97 2998[4:MRR:2966.1,2997.0] || -> SkC55*. % 0.77/0.97 2999[4:MRR:191.0,2998.0] || -> equal(op1(e13,e11),e13)**. % 0.77/0.97 3000[4:MRR:539.0,2998.0] || equal(op1(e13,e13),e11)** -> . % 0.77/0.97 3004[4:Rew:2999.0,351.0] || equal(op1(e11,e11),e13)** -> . % 0.77/0.97 3006[4:MRR:2992.0,3.0] || -> equal(op1(e10,e12),e10)**. % 0.77/0.97 3012[4:MRR:2962.0,3000.0] || -> equal(op1(e13,e13),e10)**. % 0.77/0.97 3015[4:Rew:3012.0,364.0] || equal(op1(e12,e13),e10)** -> . % 0.77/0.97 3018[4:MRR:2843.1,3015.0] || -> equal(op1(e12,e13),e11)**. % 0.77/0.97 3019[4:MRR:2842.0,3015.0] || -> equal(op1(e12,e11),e10)**. % 0.77/0.97 3029[4:Rew:2999.0,1307.1,3012.0,1307.0] || -> equal(e11,e10) equal(e13,e11) equal(op1(e13,e12),e11)**. % 0.77/0.97 3030[4:MRR:3029.0,3029.1,1.0,5.0] || -> equal(op1(e13,e12),e11)**. % 0.77/0.97 3035[4:Rew:3006.0,1308.2,3030.0,1308.0] || -> equal(e13,e11) equal(op1(e11,e12),e13)** equal(e13,e10). % 0.77/0.97 3036[4:MRR:3035.0,3035.2,5.0,3.0] || -> equal(op1(e11,e12),e13)**. % 0.77/0.97 3041[4:MRR:1339.1,1339.2,3004.0,2985.0] || -> equal(op1(e11,e11),e11)**. % 0.77/0.97 3045[4:Rew:29.0,2849.11,3006.0,2849.11,1219.0,2849.10,2989.0,2849.10,29.0,2849.9,2982.0,2849.9,1219.0,2849.8,3036.0,2849.8,995.0,2849.7,2967.0,2849.7,29.0,2849.6,3019.0,2849.6,835.0,2849.5,3018.0,2849.5,995.0,2849.4,2975.0,2849.4,1219.0,2849.3,2999.0,2849.3,835.0,2849.2,3030.0,2849.2,29.0,2849.1,3012.0,2849.1,835.0,2849.0,3041.0,2849.0] || equal(e21,e21) equal(e20,e20) equal(e21,e21) equal(e23,e23)* equal(e22,e22) equal(e21,e21) equal(e20,e20) equal(e22,e22) equal(e23,e23)* equal(e20,e20) equal(e23,e23)* equal(e20,e20) -> . % 0.77/0.97 3046[4:Obv:3045.11] || -> . % 0.77/0.97 % SZS output end Refutation % 0.77/0.97 Formulae used in the proof : ax7 ax8 ax14 ax15 ax17 ax12 ax13 co1 ax16 ax10 ax11 ax5 ax6 ax4 ax3 ax2 ax1 % 0.77/0.97 %------------------------------------------------------------------------------