%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG129+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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:34 EDT 2022 % Result : Theorem 1.28s 1.51s % Output : Refutation 1.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : ALG129+1 : TPTP v8.1.0. Released v2.7.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 9 04:51:08 EDT 2022 % 0.12/0.34 % CPUTime : % 1.28/1.51 % 1.28/1.51 SPASS V 3.9 % 1.28/1.51 SPASS beiseite: Proof found. % 1.28/1.51 % SZS status Theorem % 1.28/1.51 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.28/1.51 SPASS derived 2908 clauses, backtracked 3416 clauses, performed 31 splits and kept 5024 clauses. % 1.28/1.51 SPASS allocated 88621 KBytes. % 1.28/1.51 SPASS spent 0:00:01.17 on the problem. % 1.28/1.51 0:00:00.04 for the input. % 1.28/1.51 0:00:00.24 for the FLOTTER CNF translation. % 1.28/1.51 0:00:00.00 for inferences. % 1.28/1.51 0:00:00.02 for the backtracking. % 1.28/1.51 0:00:00.81 for the reduction. % 1.28/1.51 % 1.28/1.51 % 1.28/1.51 Here is a proof with depth 3, length 1613 : % 1.28/1.51 % SZS output start Refutation % 1.28/1.51 1[0:Inp] || equal(e11,e10)** -> . % 1.28/1.51 2[0:Inp] || equal(e12,e10)** -> . % 1.28/1.51 3[0:Inp] || equal(e13,e10)** -> . % 1.28/1.51 4[0:Inp] || equal(e12,e11)** -> . % 1.28/1.51 5[0:Inp] || equal(e13,e11)** -> . % 1.28/1.51 6[0:Inp] || equal(e13,e12)** -> . % 1.28/1.51 7[0:Inp] || equal(e21,e20)** -> . % 1.28/1.51 8[0:Inp] || equal(e22,e20)** -> . % 1.28/1.51 9[0:Inp] || equal(e23,e20)** -> . % 1.28/1.51 10[0:Inp] || equal(e22,e21)** -> . % 1.28/1.51 11[0:Inp] || equal(e23,e21)** -> . % 1.28/1.51 12[0:Inp] || equal(e23,e22)** -> . % 1.28/1.51 29[0:Inp] || -> equal(h1(e10),e20)**. % 1.28/1.51 33[0:Inp] || -> equal(op1(e10,e10),e13)**. % 1.28/1.51 34[0:Inp] || -> equal(op2(e20,e20),e23)**. % 1.28/1.51 35[0:Inp] || equal(h1(e10),e20)** -> SkC132. % 1.28/1.51 40[0:Inp] || equal(h1(e11),e21)** -> SkC133. % 1.28/1.51 45[0:Inp] || equal(h1(e12),e22)** -> SkC134. % 1.28/1.51 83[0:Inp] || -> equal(op2(e20,e20),h1(e13))**. % 1.28/1.51 84[0:Inp] || -> equal(op2(e21,e21),h2(e13))**. % 1.28/1.51 85[0:Inp] || -> equal(op2(e22,e22),h3(e13))**. % 1.28/1.51 86[0:Inp] || -> equal(op2(e23,e23),h4(e13))**. % 1.28/1.51 87[0:Inp] || SkC0 -> equal(op1(e10,e10),e10)**. % 1.28/1.51 88[0:Inp] || SkC1 -> equal(op1(e10,e10),e10)**. % 1.28/1.51 90[0:Inp] || SkC2 -> equal(op1(e10,e10),e10)**. % 1.28/1.51 92[0:Inp] || SkC3 -> equal(op1(e10,e10),e10)**. % 1.28/1.51 95[0:Inp] || SkC4 -> equal(op1(e10,e10),e11)**. % 1.28/1.51 97[0:Inp] || SkC5 -> equal(op1(e11,e11),e11)**. % 1.28/1.51 98[0:Inp] || SkC6 -> equal(op1(e10,e11),e10)**. % 1.28/1.51 99[0:Inp] || SkC6 -> equal(op1(e12,e12),e11)**. % 1.28/1.51 100[0:Inp] || SkC7 -> equal(op1(e10,e11),e10)**. % 1.28/1.51 103[0:Inp] || SkC8 -> equal(op1(e10,e10),e12)**. % 1.28/1.51 104[0:Inp] || SkC9 -> equal(op1(e10,e12),e10)**. % 1.28/1.51 105[0:Inp] || SkC9 -> equal(op1(e11,e11),e12)**. % 1.28/1.51 107[0:Inp] || SkC10 -> equal(op1(e12,e12),e12)**. % 1.28/1.51 109[0:Inp] || SkC11 -> equal(op1(e13,e13),e12)**. % 1.28/1.51 110[0:Inp] || SkC12 -> equal(op1(e10,e13),e10)**. % 1.28/1.51 117[0:Inp] || SkC15 -> equal(op1(e13,e13),e13)**. % 1.28/1.51 119[0:Inp] || SkC16 -> equal(op1(e10,e10),e10)**. % 1.28/1.51 120[0:Inp] || SkC17 -> equal(op1(e11,e10),e11)**. % 1.28/1.51 122[0:Inp] || SkC18 -> equal(op1(e11,e10),e11)**. % 1.28/1.51 123[0:Inp] || SkC18 -> equal(op1(e12,e12),e10)**. % 1.28/1.51 125[0:Inp] || SkC19 -> equal(op1(e13,e13),e10)**. % 1.28/1.51 127[0:Inp] || SkC20 -> equal(op1(e10,e10),e11)**. % 1.28/1.51 128[0:Inp] || SkC21 -> equal(op1(e11,e11),e11)**. % 1.28/1.51 129[0:Inp] || SkC22 -> equal(op1(e11,e11),e11)**. % 1.28/1.51 131[0:Inp] || SkC23 -> equal(op1(e11,e11),e11)**. % 1.28/1.51 134[0:Inp] || SkC24 -> equal(op1(e10,e10),e12)**. % 1.28/1.51 135[0:Inp] || SkC25 -> equal(op1(e11,e12),e11)**. % 1.28/1.51 138[0:Inp] || SkC26 -> equal(op1(e12,e12),e12)**. % 1.28/1.51 140[0:Inp] || SkC27 -> equal(op1(e13,e13),e12)**. % 1.28/1.51 141[0:Inp] || SkC28 -> equal(op1(e11,e13),e11)**. % 1.28/1.51 143[0:Inp] || SkC29 -> equal(op1(e11,e13),e11)**. % 1.28/1.51 145[0:Inp] || SkC30 -> equal(op1(e11,e13),e11)**. % 1.28/1.51 148[0:Inp] || SkC31 -> equal(op1(e13,e13),e13)**. % 1.28/1.51 150[0:Inp] || SkC32 -> equal(op1(e10,e10),e10)**. % 1.28/1.51 151[0:Inp] || SkC33 -> equal(op1(e12,e10),e12)**. % 1.28/1.51 153[0:Inp] || SkC34 -> equal(op1(e12,e10),e12)**. % 1.28/1.51 155[0:Inp] || SkC35 -> equal(op1(e12,e10),e12)**. % 1.28/1.51 158[0:Inp] || SkC36 -> equal(op1(e10,e10),e11)**. % 1.28/1.51 160[0:Inp] || SkC37 -> equal(op1(e11,e11),e11)**. % 1.28/1.51 161[0:Inp] || SkC38 -> equal(op1(e12,e11),e12)**. % 1.28/1.51 163[0:Inp] || SkC39 -> equal(op1(e12,e11),e12)**. % 1.28/1.51 166[0:Inp] || SkC40 -> equal(op1(e10,e10),e12)**. % 1.28/1.51 167[0:Inp] || SkC41 -> equal(op1(e12,e12),e12)**. % 1.28/1.51 169[0:Inp] || SkC42 -> equal(op1(e12,e12),e12)**. % 1.28/1.51 170[0:Inp] || SkC43 -> equal(op1(e12,e12),e12)**. % 1.28/1.51 172[0:Inp] || SkC44 -> equal(op1(e12,e13),e12)**. % 1.28/1.51 174[0:Inp] || SkC45 -> equal(op1(e12,e13),e12)**. % 1.28/1.51 175[0:Inp] || SkC45 -> equal(op1(e11,e11),e13)**. % 1.28/1.51 176[0:Inp] || SkC46 -> equal(op1(e12,e13),e12)**. % 1.28/1.51 179[0:Inp] || SkC47 -> equal(op1(e13,e13),e13)**. % 1.28/1.51 181[0:Inp] || SkC48 -> equal(op1(e10,e10),e10)**. % 1.28/1.51 182[0:Inp] || SkC49 -> equal(op1(e13,e10),e13)**. % 1.28/1.51 184[0:Inp] || SkC50 -> equal(op1(e13,e10),e13)**. % 1.28/1.51 186[0:Inp] || SkC51 -> equal(op1(e13,e10),e13)**. % 1.28/1.51 189[0:Inp] || SkC52 -> equal(op1(e10,e10),e11)**. % 1.28/1.51 191[0:Inp] || SkC53 -> equal(op1(e11,e11),e11)**. % 1.28/1.51 194[0:Inp] || SkC55 -> equal(op1(e13,e11),e13)**. % 1.28/1.51 197[0:Inp] || SkC56 -> equal(op1(e10,e10),e12)**. % 1.28/1.51 198[0:Inp] || SkC57 -> equal(op1(e13,e12),e13)**. % 1.28/1.51 199[0:Inp] || SkC57 -> equal(op1(e11,e11),e12)**. % 1.28/1.51 201[0:Inp] || SkC58 -> equal(op1(e12,e12),e12)**. % 1.28/1.51 202[0:Inp] || SkC59 -> equal(op1(e13,e12),e13)**. % 1.28/1.51 204[0:Inp] || SkC60 -> equal(op1(e13,e13),e13)**. % 1.28/1.51 206[0:Inp] || SkC61 -> equal(op1(e13,e13),e13)**. % 1.28/1.51 208[0:Inp] || SkC62 -> equal(op1(e13,e13),e13)**. % 1.28/1.51 210[0:Inp] || SkC66 -> equal(op2(e20,e20),e20)**. % 1.28/1.51 211[0:Inp] || SkC67 -> equal(op2(e20,e20),e20)**. % 1.28/1.51 213[0:Inp] || SkC68 -> equal(op2(e20,e20),e20)**. % 1.28/1.51 215[0:Inp] || SkC69 -> equal(op2(e20,e20),e20)**. % 1.28/1.51 218[0:Inp] || SkC70 -> equal(op2(e20,e20),e21)**. % 1.28/1.51 220[0:Inp] || SkC71 -> equal(op2(e21,e21),e21)**. % 1.28/1.51 221[0:Inp] || SkC72 -> equal(op2(e20,e21),e20)**. % 1.28/1.51 222[0:Inp] || SkC72 -> equal(op2(e22,e22),e21)**. % 1.28/1.51 223[0:Inp] || SkC73 -> equal(op2(e20,e21),e20)**. % 1.28/1.51 226[0:Inp] || SkC74 -> equal(op2(e20,e20),e22)**. % 1.28/1.51 227[0:Inp] || SkC75 -> equal(op2(e20,e22),e20)**. % 1.28/1.51 228[0:Inp] || SkC75 -> equal(op2(e21,e21),e22)**. % 1.28/1.51 230[0:Inp] || SkC76 -> equal(op2(e22,e22),e22)**. % 1.28/1.51 232[0:Inp] || SkC77 -> equal(op2(e23,e23),e22)**. % 1.28/1.51 233[0:Inp] || SkC78 -> equal(op2(e20,e23),e20)**. % 1.28/1.51 240[0:Inp] || SkC81 -> equal(op2(e23,e23),e23)**. % 1.28/1.51 242[0:Inp] || SkC82 -> equal(op2(e20,e20),e20)**. % 1.28/1.51 243[0:Inp] || SkC83 -> equal(op2(e21,e20),e21)**. % 1.28/1.51 245[0:Inp] || SkC84 -> equal(op2(e21,e20),e21)**. % 1.28/1.51 246[0:Inp] || SkC84 -> equal(op2(e22,e22),e20)**. % 1.28/1.51 248[0:Inp] || SkC85 -> equal(op2(e23,e23),e20)**. % 1.28/1.51 250[0:Inp] || SkC86 -> equal(op2(e20,e20),e21)**. % 1.28/1.51 251[0:Inp] || SkC87 -> equal(op2(e21,e21),e21)**. % 1.28/1.51 252[0:Inp] || SkC88 -> equal(op2(e21,e21),e21)**. % 1.28/1.51 254[0:Inp] || SkC89 -> equal(op2(e21,e21),e21)**. % 1.28/1.51 257[0:Inp] || SkC90 -> equal(op2(e20,e20),e22)**. % 1.28/1.51 258[0:Inp] || SkC91 -> equal(op2(e21,e22),e21)**. % 1.28/1.51 261[0:Inp] || SkC92 -> equal(op2(e22,e22),e22)**. % 1.28/1.51 263[0:Inp] || SkC93 -> equal(op2(e23,e23),e22)**. % 1.28/1.51 264[0:Inp] || SkC94 -> equal(op2(e21,e23),e21)**. % 1.28/1.51 266[0:Inp] || SkC95 -> equal(op2(e21,e23),e21)**. % 1.28/1.51 268[0:Inp] || SkC96 -> equal(op2(e21,e23),e21)**. % 1.28/1.51 271[0:Inp] || SkC97 -> equal(op2(e23,e23),e23)**. % 1.28/1.51 273[0:Inp] || SkC98 -> equal(op2(e20,e20),e20)**. % 1.28/1.51 274[0:Inp] || SkC99 -> equal(op2(e22,e20),e22)**. % 1.28/1.51 276[0:Inp] || SkC100 -> equal(op2(e22,e20),e22)**. % 1.28/1.51 278[0:Inp] || SkC101 -> equal(op2(e22,e20),e22)**. % 1.28/1.51 281[0:Inp] || SkC102 -> equal(op2(e20,e20),e21)**. % 1.28/1.51 283[0:Inp] || SkC103 -> equal(op2(e21,e21),e21)**. % 1.28/1.51 284[0:Inp] || SkC104 -> equal(op2(e22,e21),e22)**. % 1.28/1.51 286[0:Inp] || SkC105 -> equal(op2(e22,e21),e22)**. % 1.28/1.51 289[0:Inp] || SkC106 -> equal(op2(e20,e20),e22)**. % 1.28/1.51 290[0:Inp] || SkC107 -> equal(op2(e22,e22),e22)**. % 1.28/1.51 292[0:Inp] || SkC108 -> equal(op2(e22,e22),e22)**. % 1.28/1.51 293[0:Inp] || SkC109 -> equal(op2(e22,e22),e22)**. % 1.28/1.51 295[0:Inp] || SkC110 -> equal(op2(e22,e23),e22)**. % 1.28/1.51 297[0:Inp] || SkC111 -> equal(op2(e22,e23),e22)**. % 1.28/1.51 298[0:Inp] || SkC111 -> equal(op2(e21,e21),e23)**. % 1.28/1.51 299[0:Inp] || SkC112 -> equal(op2(e22,e23),e22)**. % 1.28/1.51 302[0:Inp] || SkC113 -> equal(op2(e23,e23),e23)**. % 1.28/1.51 304[0:Inp] || SkC114 -> equal(op2(e20,e20),e20)**. % 1.28/1.51 305[0:Inp] || SkC115 -> equal(op2(e23,e20),e23)**. % 1.28/1.51 307[0:Inp] || SkC116 -> equal(op2(e23,e20),e23)**. % 1.28/1.51 309[0:Inp] || SkC117 -> equal(op2(e23,e20),e23)**. % 1.28/1.51 312[0:Inp] || SkC118 -> equal(op2(e20,e20),e21)**. % 1.28/1.51 314[0:Inp] || SkC119 -> equal(op2(e21,e21),e21)**. % 1.28/1.51 317[0:Inp] || SkC121 -> equal(op2(e23,e21),e23)**. % 1.28/1.51 320[0:Inp] || SkC122 -> equal(op2(e20,e20),e22)**. % 1.28/1.51 321[0:Inp] || SkC123 -> equal(op2(e23,e22),e23)**. % 1.28/1.51 322[0:Inp] || SkC123 -> equal(op2(e21,e21),e22)**. % 1.28/1.51 324[0:Inp] || SkC124 -> equal(op2(e22,e22),e22)**. % 1.28/1.51 325[0:Inp] || SkC125 -> equal(op2(e23,e22),e23)**. % 1.28/1.51 327[0:Inp] || SkC126 -> equal(op2(e23,e23),e23)**. % 1.28/1.51 329[0:Inp] || SkC127 -> equal(op2(e23,e23),e23)**. % 1.28/1.51 331[0:Inp] || SkC128 -> equal(op2(e23,e23),e23)**. % 1.28/1.51 333[0:Inp] || -> equal(op1(op1(e10,e10),e10),e12)**. % 1.28/1.51 334[0:Inp] || -> equal(op2(op2(e20,e20),e20),e22)**. % 1.28/1.51 335[0:Inp] || equal(op1(e11,e10),op1(e10,e10))** -> . % 1.28/1.51 336[0:Inp] || equal(op1(e12,e10),op1(e10,e10))** -> . % 1.28/1.51 338[0:Inp] || equal(op1(e12,e10),op1(e11,e10))** -> . % 1.28/1.51 339[0:Inp] || equal(op1(e13,e10),op1(e11,e10))** -> . % 1.28/1.51 340[0:Inp] || equal(op1(e13,e10),op1(e12,e10))** -> . % 1.28/1.51 341[0:Inp] || equal(op1(e11,e11),op1(e10,e11))** -> . % 1.28/1.51 342[0:Inp] || equal(op1(e12,e11),op1(e10,e11))** -> . % 1.28/1.51 343[0:Inp] || equal(op1(e13,e11),op1(e10,e11))** -> . % 1.28/1.51 344[0:Inp] || equal(op1(e12,e11),op1(e11,e11))** -> . % 1.28/1.51 345[0:Inp] || equal(op1(e13,e11),op1(e11,e11))** -> . % 1.28/1.51 346[0:Inp] || equal(op1(e13,e11),op1(e12,e11))** -> . % 1.28/1.51 347[0:Inp] || equal(op1(e11,e12),op1(e10,e12))** -> . % 1.28/1.51 348[0:Inp] || equal(op1(e12,e12),op1(e10,e12))** -> . % 1.28/1.51 349[0:Inp] || equal(op1(e13,e12),op1(e10,e12))** -> . % 1.28/1.51 350[0:Inp] || equal(op1(e12,e12),op1(e11,e12))** -> . % 1.28/1.51 351[0:Inp] || equal(op1(e13,e12),op1(e11,e12))** -> . % 1.28/1.51 352[0:Inp] || equal(op1(e13,e12),op1(e12,e12))** -> . % 1.28/1.51 355[0:Inp] || equal(op1(e13,e13),op1(e10,e13))** -> . % 1.28/1.51 356[0:Inp] || equal(op1(e12,e13),op1(e11,e13))** -> . % 1.28/1.51 357[0:Inp] || equal(op1(e13,e13),op1(e11,e13))** -> . % 1.28/1.51 358[0:Inp] || equal(op1(e13,e13),op1(e12,e13))** -> . % 1.28/1.51 359[0:Inp] || equal(op1(e10,e11),op1(e10,e10))** -> . % 1.28/1.51 360[0:Inp] || equal(op1(e10,e12),op1(e10,e10))** -> . % 1.28/1.51 361[0:Inp] || equal(op1(e10,e13),op1(e10,e10))** -> . % 1.28/1.51 362[0:Inp] || equal(op1(e10,e12),op1(e10,e11))** -> . % 1.28/1.51 363[0:Inp] || equal(op1(e10,e13),op1(e10,e11))** -> . % 1.28/1.51 364[0:Inp] || equal(op1(e10,e13),op1(e10,e12))** -> . % 1.28/1.51 365[0:Inp] || equal(op1(e11,e11),op1(e11,e10))** -> . % 1.28/1.51 366[0:Inp] || equal(op1(e11,e12),op1(e11,e10))** -> . % 1.28/1.51 367[0:Inp] || equal(op1(e11,e13),op1(e11,e10))** -> . % 1.28/1.51 368[0:Inp] || equal(op1(e11,e12),op1(e11,e11))** -> . % 1.28/1.51 369[0:Inp] || equal(op1(e11,e13),op1(e11,e11))** -> . % 1.28/1.51 370[0:Inp] || equal(op1(e11,e13),op1(e11,e12))** -> . % 1.28/1.51 372[0:Inp] || equal(op1(e12,e12),op1(e12,e10))** -> . % 1.28/1.51 374[0:Inp] || equal(op1(e12,e12),op1(e12,e11))** -> . % 1.28/1.51 376[0:Inp] || equal(op1(e12,e13),op1(e12,e12))** -> . % 1.28/1.51 377[0:Inp] || equal(op1(e13,e11),op1(e13,e10))** -> . % 1.28/1.51 378[0:Inp] || equal(op1(e13,e12),op1(e13,e10))** -> . % 1.28/1.51 379[0:Inp] || equal(op1(e13,e13),op1(e13,e10))** -> . % 1.28/1.51 380[0:Inp] || equal(op1(e13,e12),op1(e13,e11))** -> . % 1.28/1.51 381[0:Inp] || equal(op1(e13,e13),op1(e13,e11))** -> . % 1.28/1.51 382[0:Inp] || equal(op1(e13,e13),op1(e13,e12))** -> . % 1.28/1.51 383[0:Inp] || equal(op2(e21,e20),op2(e20,e20))** -> . % 1.28/1.51 384[0:Inp] || equal(op2(e22,e20),op2(e20,e20))** -> . % 1.28/1.51 387[0:Inp] || equal(op2(e23,e20),op2(e21,e20))** -> . % 1.28/1.51 388[0:Inp] || equal(op2(e23,e20),op2(e22,e20))** -> . % 1.28/1.51 389[0:Inp] || equal(op2(e21,e21),op2(e20,e21))** -> . % 1.28/1.51 390[0:Inp] || equal(op2(e22,e21),op2(e20,e21))** -> . % 1.28/1.51 391[0:Inp] || equal(op2(e23,e21),op2(e20,e21))** -> . % 1.28/1.51 392[0:Inp] || equal(op2(e22,e21),op2(e21,e21))** -> . % 1.28/1.51 393[0:Inp] || equal(op2(e23,e21),op2(e21,e21))** -> . % 1.28/1.51 394[0:Inp] || equal(op2(e23,e21),op2(e22,e21))** -> . % 1.28/1.51 396[0:Inp] || equal(op2(e22,e22),op2(e20,e22))** -> . % 1.28/1.51 398[0:Inp] || equal(op2(e22,e22),op2(e21,e22))** -> . % 1.28/1.51 399[0:Inp] || equal(op2(e23,e22),op2(e21,e22))** -> . % 1.28/1.51 400[0:Inp] || equal(op2(e23,e22),op2(e22,e22))** -> . % 1.28/1.51 401[0:Inp] || equal(op2(e21,e23),op2(e20,e23))** -> . % 1.28/1.51 403[0:Inp] || equal(op2(e23,e23),op2(e20,e23))** -> . % 1.28/1.51 404[0:Inp] || equal(op2(e22,e23),op2(e21,e23))** -> . % 1.28/1.51 405[0:Inp] || equal(op2(e23,e23),op2(e21,e23))** -> . % 1.28/1.51 406[0:Inp] || equal(op2(e23,e23),op2(e22,e23))** -> . % 1.28/1.51 407[0:Inp] || equal(op2(e20,e21),op2(e20,e20))** -> . % 1.28/1.51 409[0:Inp] || equal(op2(e20,e23),op2(e20,e20))** -> . % 1.28/1.51 410[0:Inp] || equal(op2(e20,e22),op2(e20,e21))** -> . % 1.28/1.51 411[0:Inp] || equal(op2(e20,e23),op2(e20,e21))** -> . % 1.28/1.51 412[0:Inp] || equal(op2(e20,e23),op2(e20,e22))** -> . % 1.28/1.51 413[0:Inp] || equal(op2(e21,e21),op2(e21,e20))** -> . % 1.28/1.51 414[0:Inp] || equal(op2(e21,e22),op2(e21,e20))** -> . % 1.28/1.51 415[0:Inp] || equal(op2(e21,e23),op2(e21,e20))** -> . % 1.28/1.51 416[0:Inp] || equal(op2(e21,e22),op2(e21,e21))** -> . % 1.28/1.51 417[0:Inp] || equal(op2(e21,e23),op2(e21,e21))** -> . % 1.28/1.51 418[0:Inp] || equal(op2(e21,e23),op2(e21,e22))** -> . % 1.28/1.51 419[0:Inp] || equal(op2(e22,e21),op2(e22,e20))** -> . % 1.28/1.51 420[0:Inp] || equal(op2(e22,e22),op2(e22,e20))** -> . % 1.28/1.51 422[0:Inp] || equal(op2(e22,e22),op2(e22,e21))** -> . % 1.28/1.51 423[0:Inp] || equal(op2(e22,e23),op2(e22,e21))** -> . % 1.28/1.51 424[0:Inp] || equal(op2(e22,e23),op2(e22,e22))** -> . % 1.28/1.51 425[0:Inp] || equal(op2(e23,e21),op2(e23,e20))** -> . % 1.28/1.51 426[0:Inp] || equal(op2(e23,e22),op2(e23,e20))** -> . % 1.28/1.51 427[0:Inp] || equal(op2(e23,e23),op2(e23,e20))** -> . % 1.28/1.51 428[0:Inp] || equal(op2(e23,e22),op2(e23,e21))** -> . % 1.28/1.51 429[0:Inp] || equal(op2(e23,e23),op2(e23,e21))** -> . % 1.28/1.51 430[0:Inp] || equal(op2(e23,e23),op2(e23,e22))** -> . % 1.28/1.51 441[0:Inp] || equal(op1(e11,e11),e11)** SkC5 -> . % 1.28/1.51 445[0:Inp] || SkC7 equal(op1(e13,e11),e13)** -> . % 1.28/1.51 451[0:Inp] || equal(op1(e12,e12),e12)** SkC10 -> . % 1.28/1.51 455[0:Inp] || equal(op1(e10,e13),e10)** SkC12 -> . % 1.28/1.51 456[0:Inp] || equal(op1(e10,e10),e13)** SkC13 -> . % 1.28/1.51 458[0:Inp] || equal(op1(e10,e10),e13)** SkC14 -> . % 1.28/1.51 461[0:Inp] || equal(op1(e13,e13),e13)** SkC15 -> . % 1.28/1.51 465[0:Inp] || equal(op1(e11,e10),e11)** SkC17 -> . % 1.28/1.51 472[0:Inp] || equal(op1(e11,e11),e11)** SkC21 -> . % 1.28/1.51 473[0:Inp] || equal(op1(e11,e11),e11)** SkC22 -> . % 1.28/1.51 475[0:Inp] || equal(op1(e11,e11),e11)** SkC23 -> . % 1.28/1.51 480[0:Inp] || equal(op1(e11,e12),e11)** SkC25 -> . % 1.28/1.51 482[0:Inp] || equal(op1(e12,e12),e12)** SkC26 -> . % 1.28/1.51 488[0:Inp] || equal(op1(e11,e13),e11)** SkC29 -> . % 1.28/1.51 492[0:Inp] || equal(op1(e13,e13),e13)** SkC31 -> . % 1.28/1.51 498[0:Inp] || equal(op1(e12,e10),e12)** SkC34 -> . % 1.28/1.51 504[0:Inp] || equal(op1(e11,e11),e11)** SkC37 -> . % 1.28/1.51 506[0:Inp] || equal(op1(e12,e11),e12)** SkC38 -> . % 1.28/1.51 507[0:Inp] || SkC39 equal(op1(e12,e12),e11)** -> . % 1.28/1.51 508[0:Inp] || SkC39 equal(op1(e13,e11),e13)** -> . % 1.28/1.51 511[0:Inp] || equal(op1(e12,e12),e12)** SkC41 -> . % 1.28/1.51 513[0:Inp] || equal(op1(e12,e12),e12)** SkC42 -> . % 1.28/1.51 514[0:Inp] || equal(op1(e12,e12),e12)** SkC43 -> . % 1.28/1.51 516[0:Inp] || SkC44 equal(op1(e12,e12),e13)** -> . % 1.28/1.51 517[0:Inp] || SkC44 equal(op1(e10,e13),e10)** -> . % 1.28/1.51 518[0:Inp] || SkC45 equal(op1(e12,e12),e13)** -> . % 1.28/1.51 521[0:Inp] || equal(op1(e12,e13),e12)** SkC46 -> . % 1.28/1.51 523[0:Inp] || equal(op1(e13,e13),e13)** SkC47 -> . % 1.28/1.51 535[0:Inp] || equal(op1(e11,e11),e11)** SkC53 -> . % 1.28/1.51 536[0:Inp] || equal(op1(e13,e13),e11)** SkC54 -> . % 1.28/1.51 539[0:Inp] || equal(op1(e13,e11),e13)** SkC55 -> . % 1.28/1.51 545[0:Inp] || equal(op1(e12,e12),e12)** SkC58 -> . % 1.28/1.51 547[0:Inp] || equal(op1(e13,e12),e13)** SkC59 -> . % 1.28/1.51 548[0:Inp] || equal(op1(e13,e13),e13)** SkC60 -> . % 1.28/1.51 550[0:Inp] || equal(op1(e13,e13),e13)** SkC61 -> . % 1.28/1.51 552[0:Inp] || equal(op1(e13,e13),e13)** SkC62 -> . % 1.28/1.51 564[0:Inp] || equal(op2(e21,e21),e21)** SkC71 -> . % 1.28/1.51 568[0:Inp] || SkC73 equal(op2(e23,e21),e23)** -> . % 1.28/1.51 574[0:Inp] || equal(op2(e22,e22),e22)** SkC76 -> . % 1.28/1.51 578[0:Inp] || equal(op2(e20,e23),e20)** SkC78 -> . % 1.28/1.51 579[0:Inp] || equal(op2(e20,e20),e23)** SkC79 -> . % 1.28/1.51 581[0:Inp] || equal(op2(e20,e20),e23)** SkC80 -> . % 1.28/1.51 584[0:Inp] || equal(op2(e23,e23),e23)** SkC81 -> . % 1.28/1.51 588[0:Inp] || equal(op2(e21,e20),e21)** SkC83 -> . % 1.28/1.51 589[0:Inp] || equal(op2(e21,e21),e20)** SkC84 -> . % 1.28/1.51 595[0:Inp] || equal(op2(e21,e21),e21)** SkC87 -> . % 1.28/1.51 596[0:Inp] || equal(op2(e21,e21),e21)** SkC88 -> . % 1.28/1.51 598[0:Inp] || equal(op2(e21,e21),e21)** SkC89 -> . % 1.28/1.51 603[0:Inp] || equal(op2(e21,e22),e21)** SkC91 -> . % 1.28/1.51 605[0:Inp] || equal(op2(e22,e22),e22)** SkC92 -> . % 1.28/1.51 611[0:Inp] || equal(op2(e21,e23),e21)** SkC95 -> . % 1.28/1.51 615[0:Inp] || equal(op2(e23,e23),e23)** SkC97 -> . % 1.28/1.51 621[0:Inp] || equal(op2(e22,e20),e22)** SkC100 -> . % 1.28/1.51 627[0:Inp] || equal(op2(e21,e21),e21)** SkC103 -> . % 1.28/1.51 629[0:Inp] || equal(op2(e22,e21),e22)** SkC104 -> . % 1.28/1.51 630[0:Inp] || equal(op2(e22,e22),e21)** SkC105 -> . % 1.28/1.51 631[0:Inp] || SkC105 equal(op2(e23,e21),e23)** -> . % 1.28/1.52 634[0:Inp] || equal(op2(e22,e22),e22)** SkC107 -> . % 1.28/1.52 636[0:Inp] || equal(op2(e22,e22),e22)** SkC108 -> . % 1.28/1.52 637[0:Inp] || equal(op2(e22,e22),e22)** SkC109 -> . % 1.28/1.52 639[0:Inp] || equal(op2(e22,e22),e23)** SkC110 -> . % 1.28/1.52 640[0:Inp] || SkC110 equal(op2(e20,e23),e20)** -> . % 1.28/1.52 644[0:Inp] || equal(op2(e22,e23),e22)** SkC112 -> . % 1.28/1.52 646[0:Inp] || equal(op2(e23,e23),e23)** SkC113 -> . % 1.28/1.52 658[0:Inp] || equal(op2(e21,e21),e21)** SkC119 -> . % 1.28/1.52 659[0:Inp] || equal(op2(e23,e23),e21)** SkC120 -> . % 1.28/1.52 662[0:Inp] || equal(op2(e23,e21),e23)** SkC121 -> . % 1.28/1.52 666[0:Inp] || SkC123 equal(op2(e21,e22),e21)** -> . % 1.28/1.52 668[0:Inp] || equal(op2(e22,e22),e22)** SkC124 -> . % 1.28/1.52 670[0:Inp] || equal(op2(e23,e22),e23)** SkC125 -> . % 1.28/1.52 671[0:Inp] || equal(op2(e23,e23),e23)** SkC126 -> . % 1.28/1.52 673[0:Inp] || equal(op2(e23,e23),e23)** SkC127 -> . % 1.28/1.52 675[0:Inp] || equal(op2(e23,e23),e23)** SkC128 -> . % 1.28/1.52 677[0:Inp] || -> equal(op2(op2(e20,e20),e20),h1(e12))**. % 1.28/1.52 678[0:Inp] || -> equal(op2(op2(e21,e21),e21),h2(e12))**. % 1.28/1.52 680[0:Inp] || -> equal(op2(op2(e23,e23),e23),h4(e12))**. % 1.28/1.52 681[0:Inp] || SkC63 -> equal(op1(e10,op1(e10,e10)),e10)**. % 1.28/1.52 687[0:Inp] || SkC64 -> equal(op1(e11,op1(e11,e12)),e12)**. % 1.28/1.52 690[0:Inp] || SkC65 -> equal(op1(e12,op1(e12,e11)),e11)**. % 1.28/1.52 691[0:Inp] || SkC65 -> equal(op1(e12,op1(e12,e12)),e12)**. % 1.28/1.52 693[0:Inp] || SkC129 -> equal(op2(e20,op2(e20,e20)),e20)**. % 1.28/1.52 695[0:Inp] || SkC129 -> equal(op2(e20,op2(e20,e22)),e22)**. % 1.28/1.52 701[0:Inp] || SkC131 -> equal(op2(e22,op2(e22,e20)),e20)**. % 1.28/1.52 702[0:Inp] || SkC131 -> equal(op2(e22,op2(e22,e21)),e21)**. % 1.28/1.52 703[0:Inp] || SkC131 -> equal(op2(e22,op2(e22,e22)),e22)**. % 1.28/1.52 705[0:Inp] || -> equal(op1(op1(e10,e10),op1(e10,e10)),e11)**. % 1.28/1.52 706[0:Inp] || -> equal(op2(op2(e20,e20),op2(e20,e20)),e21)**. % 1.28/1.52 707[0:Inp] || -> equal(op1(e13,op1(e13,e10)),e10)** SkC63 SkC64 SkC65. % 1.28/1.52 710[0:Inp] || -> equal(op1(e13,op1(e13,e13)),e13)** SkC63 SkC64 SkC65. % 1.28/1.52 714[0:Inp] || -> equal(op2(e23,op2(e23,e23)),e23)** SkC129 SkC130 SkC131. % 1.28/1.52 715[0:Inp] || -> equal(op2(op2(e20,e20),op2(e20,e20)),h1(e11))**. % 1.28/1.52 716[0:Inp] || -> equal(op2(op2(e21,e21),op2(e21,e21)),h2(e11))**. % 1.28/1.52 720[0:Inp] || equal(op1(e12,e12),e10)** SkC63 -> equal(op1(e12,e10),e12). % 1.28/1.52 724[0:Inp] || equal(op1(e13,e13),e11)** SkC64 -> equal(op1(e13,e11),e13). % 1.28/1.52 729[0:Inp] || equal(op2(e22,e22),e20)** SkC129 -> equal(op2(e22,e20),e22). % 1.28/1.52 733[0:Inp] || equal(op2(e23,e23),e21)** SkC130 -> equal(op2(e23,e21),e23). % 1.28/1.52 737[0:Inp] || equal(op1(e10,e10),e13) -> equal(op1(e10,e13),e10)** SkC63 SkC64 SkC65. % 1.28/1.52 740[0:Inp] || equal(op2(e20,e20),e23) -> equal(op2(e20,e23),e20)** SkC129 SkC130 SkC131. % 1.28/1.52 743[0:Inp] || -> equal(op2(e20,e23),e23) equal(op2(e21,e23),e23) equal(op2(e22,e23),e23) equal(op2(e23,e23),e23)**. % 1.28/1.52 744[0:Inp] || -> equal(op2(e23,e20),e23) equal(op2(e23,e21),e23) equal(op2(e23,e22),e23) equal(op2(e23,e23),e23)**. % 1.28/1.52 745[0:Inp] || -> equal(op2(e20,e23),e22) equal(op2(e21,e23),e22) equal(op2(e22,e23),e22) equal(op2(e23,e23),e22)**. % 1.28/1.52 749[0:Inp] || -> equal(op2(e20,e23),e20) equal(op2(e21,e23),e20) equal(op2(e22,e23),e20) equal(op2(e23,e23),e20)**. % 1.28/1.52 750[0:Inp] || -> equal(op2(e23,e20),e20) equal(op2(e23,e21),e20) equal(op2(e23,e22),e20) equal(op2(e23,e23),e20)**. % 1.28/1.52 752[0:Inp] || -> equal(op2(e22,e20),e23) equal(op2(e22,e21),e23) equal(op2(e22,e22),e23) equal(op2(e22,e23),e23)**. % 1.28/1.52 753[0:Inp] || -> equal(op2(e20,e22),e22) equal(op2(e21,e22),e22) equal(op2(e22,e22),e22) equal(op2(e23,e22),e22)**. % 1.28/1.52 754[0:Inp] || -> equal(op2(e22,e20),e22) equal(op2(e22,e21),e22) equal(op2(e22,e22),e22) equal(op2(e22,e23),e22)**. % 1.28/1.52 755[0:Inp] || -> equal(op2(e20,e22),e21) equal(op2(e21,e22),e21) equal(op2(e22,e22),e21) equal(op2(e23,e22),e21)**. % 1.28/1.52 756[0:Inp] || -> equal(op2(e22,e20),e21) equal(op2(e22,e21),e21) equal(op2(e22,e22),e21) equal(op2(e22,e23),e21)**. % 1.28/1.52 757[0:Inp] || -> equal(op2(e20,e22),e20) equal(op2(e21,e22),e20) equal(op2(e22,e22),e20) equal(op2(e23,e22),e20)**. % 1.28/1.52 759[0:Inp] || -> equal(op2(e20,e21),e23) equal(op2(e21,e21),e23) equal(op2(e22,e21),e23) equal(op2(e23,e21),e23)**. % 1.28/1.52 760[0:Inp] || -> equal(op2(e21,e20),e23) equal(op2(e21,e21),e23) equal(op2(e21,e22),e23) equal(op2(e21,e23),e23)**. % 1.28/1.52 761[0:Inp] || -> equal(op2(e20,e21),e22) equal(op2(e21,e21),e22) equal(op2(e22,e21),e22) equal(op2(e23,e21),e22)**. % 1.28/1.52 763[0:Inp] || -> equal(op2(e20,e21),e21) equal(op2(e21,e21),e21) equal(op2(e22,e21),e21) equal(op2(e23,e21),e21)**. % 1.28/1.52 765[0:Inp] || -> equal(op2(e20,e21),e20) equal(op2(e21,e21),e20) equal(op2(e22,e21),e20) equal(op2(e23,e21),e20)**. % 1.28/1.52 770[0:Inp] || -> equal(op2(e20,e20),e22) equal(op2(e20,e21),e22) equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)**. % 1.28/1.52 771[0:Inp] || -> equal(op2(e20,e20),e21) equal(op2(e21,e20),e21) equal(op2(e22,e20),e21) equal(op2(e23,e20),e21)**. % 1.28/1.52 772[0:Inp] || -> equal(op2(e20,e20),e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21) equal(op2(e20,e23),e21)**. % 1.28/1.52 773[0:Inp] || -> equal(op2(e20,e20),e20) equal(op2(e21,e20),e20) equal(op2(e22,e20),e20) equal(op2(e23,e20),e20)**. % 1.28/1.52 777[0:Inp] || -> equal(op2(e23,e21),e20) equal(op2(e23,e21),e21) equal(op2(e23,e21),e22) equal(op2(e23,e21),e23)**. % 1.28/1.52 780[0:Inp] || -> equal(op2(e22,e22),e20) equal(op2(e22,e22),e21) equal(op2(e22,e22),e22) equal(op2(e22,e22),e23)**. % 1.28/1.52 781[0:Inp] || -> equal(op2(e22,e21),e22) equal(op2(e22,e21),e21) equal(op2(e22,e21),e23)** equal(op2(e22,e21),e20). % 1.28/1.52 783[0:Inp] || -> equal(op2(e21,e23),e20) equal(op2(e21,e23),e21) equal(op2(e21,e23),e22) equal(op2(e21,e23),e23)**. % 1.28/1.52 784[0:Inp] || -> equal(op2(e21,e22),e22) equal(op2(e21,e22),e21) equal(op2(e21,e22),e23)** equal(op2(e21,e22),e20). % 1.28/1.52 785[0:Inp] || -> equal(op2(e21,e21),e20) equal(op2(e21,e21),e21) equal(op2(e21,e21),e22) equal(op2(e21,e21),e23)**. % 1.28/1.52 786[0:Inp] || -> equal(op2(e21,e20),e20) equal(op2(e21,e20),e21) equal(op2(e21,e20),e22) equal(op2(e21,e20),e23)**. % 1.28/1.52 787[0:Inp] || -> equal(op2(e20,e23),e20) equal(op2(e20,e23),e21) equal(op2(e20,e23),e22) equal(op2(e20,e23),e23)**. % 1.28/1.52 789[0:Inp] || -> equal(op2(e20,e21),e20) equal(op2(e20,e21),e21) equal(op2(e20,e21),e22) equal(op2(e20,e21),e23)**. % 1.28/1.52 791[0:Inp] || -> equal(op1(e10,e13),e13) equal(op1(e11,e13),e13) equal(op1(e12,e13),e13) equal(op1(e13,e13),e13)**. % 1.28/1.52 792[0:Inp] || -> equal(op1(e13,e10),e13) equal(op1(e13,e11),e13) equal(op1(e13,e12),e13) equal(op1(e13,e13),e13)**. % 1.28/1.52 793[0:Inp] || -> equal(op1(e10,e13),e12) equal(op1(e11,e13),e12) equal(op1(e12,e13),e12) equal(op1(e13,e13),e12)**. % 1.28/1.52 797[0:Inp] || -> equal(op1(e10,e13),e10) equal(op1(e11,e13),e10) equal(op1(e12,e13),e10) equal(op1(e13,e13),e10)**. % 1.28/1.52 798[0:Inp] || -> equal(op1(e13,e10),e10) equal(op1(e13,e11),e10) equal(op1(e13,e12),e10) equal(op1(e13,e13),e10)**. % 1.28/1.52 799[0:Inp] || -> equal(op1(e10,e12),e13) equal(op1(e11,e12),e13) equal(op1(e12,e12),e13) equal(op1(e13,e12),e13)**. % 1.28/1.52 800[0:Inp] || -> equal(op1(e12,e10),e13) equal(op1(e12,e11),e13) equal(op1(e12,e12),e13) equal(op1(e12,e13),e13)**. % 1.28/1.52 801[0:Inp] || -> equal(op1(e10,e12),e12) equal(op1(e11,e12),e12) equal(op1(e12,e12),e12) equal(op1(e13,e12),e12)**. % 1.28/1.52 802[0:Inp] || -> equal(op1(e12,e10),e12) equal(op1(e12,e11),e12) equal(op1(e12,e12),e12) equal(op1(e12,e13),e12)**. % 1.28/1.52 803[0:Inp] || -> equal(op1(e10,e12),e11) equal(op1(e11,e12),e11) equal(op1(e12,e12),e11) equal(op1(e13,e12),e11)**. % 1.28/1.52 804[0:Inp] || -> equal(op1(e12,e10),e11) equal(op1(e12,e11),e11) equal(op1(e12,e12),e11) equal(op1(e12,e13),e11)**. % 1.28/1.52 805[0:Inp] || -> equal(op1(e12,e12),e10) equal(op1(e10,e12),e10) equal(op1(e13,e12),e10)** equal(op1(e11,e12),e10). % 1.28/1.52 807[0:Inp] || -> equal(op1(e10,e11),e13) equal(op1(e11,e11),e13) equal(op1(e12,e11),e13) equal(op1(e13,e11),e13)**. % 1.28/1.52 808[0:Inp] || -> equal(op1(e11,e10),e13) equal(op1(e11,e11),e13) equal(op1(e11,e12),e13) equal(op1(e11,e13),e13)**. % 1.28/1.52 810[0:Inp] || -> equal(op1(e11,e10),e12) equal(op1(e11,e11),e12) equal(op1(e11,e12),e12) equal(op1(e11,e13),e12)**. % 1.28/1.52 811[0:Inp] || -> equal(op1(e10,e11),e11) equal(op1(e11,e11),e11) equal(op1(e12,e11),e11) equal(op1(e13,e11),e11)**. % 1.28/1.52 819[0:Inp] || -> equal(op1(e10,e10),e11) equal(op1(e11,e10),e11) equal(op1(e12,e10),e11) equal(op1(e13,e10),e11)**. % 1.28/1.52 820[0:Inp] || -> equal(op1(e10,e10),e11) equal(op1(e10,e11),e11) equal(op1(e10,e12),e11) equal(op1(e10,e13),e11)**. % 1.28/1.52 824[0:Inp] || -> equal(op1(e13,e12),e10) equal(op1(e13,e12),e11) equal(op1(e13,e12),e12) equal(op1(e13,e12),e13)**. % 1.28/1.52 825[0:Inp] || -> equal(op1(e13,e11),e10) equal(op1(e13,e11),e11) equal(op1(e13,e11),e12) equal(op1(e13,e11),e13)**. % 1.28/1.52 828[0:Inp] || -> equal(op1(e12,e12),e12) equal(op1(e12,e12),e13)** equal(op1(e12,e12),e11) equal(op1(e12,e12),e10). % 1.28/1.52 830[0:Inp] || -> equal(op1(e12,e10),e10) equal(op1(e12,e10),e11) equal(op1(e12,e10),e12) equal(op1(e12,e10),e13)**. % 1.28/1.52 832[0:Inp] || -> equal(op1(e11,e12),e12) equal(op1(e11,e12),e11) equal(op1(e11,e12),e13)** equal(op1(e11,e12),e10). % 1.28/1.52 833[0:Inp] || -> equal(op1(e11,e11),e11) equal(op1(e11,e11),e13)** equal(op1(e11,e11),e12) equal(op1(e11,e11),e10). % 1.28/1.52 834[0:Inp] || -> equal(op1(e11,e10),e10) equal(op1(e11,e10),e11) equal(op1(e11,e10),e12) equal(op1(e11,e10),e13)**. % 1.28/1.52 835[0:Inp] || -> equal(op1(e10,e13),e10) equal(op1(e10,e13),e11) equal(op1(e10,e13),e12) equal(op1(e10,e13),e13)**. % 1.28/1.52 836[0:Inp] || -> equal(op1(e10,e12),e10) equal(op1(e10,e12),e11) equal(op1(e10,e12),e12) equal(op1(e10,e12),e13)**. % 1.28/1.52 837[0:Inp] || -> equal(op1(e10,e11),e10) equal(op1(e10,e11),e11) equal(op1(e10,e11),e12) equal(op1(e10,e11),e13)**. % 1.28/1.52 839[0:Inp] || -> equal(op2(e23,e23),e23)** SkC66 SkC67 SkC68 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. % 1.28/1.52 840[0:Inp] || -> equal(op1(e13,e13),e13)** SkC0 SkC1 SkC2 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. % 1.28/1.52 855[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 -> . % 1.28/1.52 859[0:Rew:34.0,83.0] || -> equal(h1(e13),e23)**. % 1.28/1.52 876[0:Rew:29.0,35.0] || equal(e20,e20) -> SkC132*. % 1.28/1.52 877[0:Obv:876.0] || -> SkC132*. % 1.28/1.52 878[0:Rew:34.0,334.0] || -> equal(op2(e23,e20),e22)**. % 1.28/1.52 879[0:Rew:33.0,333.0] || -> equal(op1(e13,e10),e12)**. % 1.28/1.52 881[0:Rew:86.0,331.1] || SkC128 -> equal(h4(e13),e23)**. % 1.28/1.52 883[0:Rew:86.0,329.1] || SkC127 -> equal(h4(e13),e23)**. % 1.28/1.52 884[0:Rew:86.0,327.1] || SkC126 -> equal(h4(e13),e23)**. % 1.28/1.52 886[0:Rew:85.0,324.1] || SkC124 -> equal(h3(e13),e22)**. % 1.28/1.52 887[0:Rew:84.0,322.1] || SkC123 -> equal(h2(e13),e22)**. % 1.28/1.52 888[0:Rew:34.0,320.1] || SkC122* -> equal(e23,e22). % 1.28/1.52 889[0:MRR:888.1,12.0] || SkC122* -> . % 1.28/1.52 892[0:Rew:84.0,314.1] || SkC119 -> equal(h2(e13),e21)**. % 1.28/1.52 893[0:Rew:34.0,312.1] || SkC118* -> equal(e23,e21). % 1.28/1.52 894[0:MRR:893.1,11.0] || SkC118* -> . % 1.28/1.52 896[0:Rew:878.0,309.1] || SkC117* -> equal(e23,e22). % 1.28/1.52 897[0:MRR:896.1,12.0] || SkC117* -> . % 1.28/1.52 899[0:Rew:878.0,307.1] || SkC116* -> equal(e23,e22). % 1.28/1.52 900[0:MRR:899.1,12.0] || SkC116* -> . % 1.28/1.52 902[0:Rew:878.0,305.1] || SkC115* -> equal(e23,e22). % 1.28/1.52 903[0:MRR:902.1,12.0] || SkC115* -> . % 1.28/1.52 904[0:Rew:34.0,304.1] || SkC114* -> equal(e23,e20). % 1.28/1.52 905[0:MRR:904.1,9.0] || SkC114* -> . % 1.28/1.52 906[0:Rew:86.0,302.1] || SkC113 -> equal(h4(e13),e23)**. % 1.28/1.52 908[0:Rew:84.0,298.1] || SkC111 -> equal(h2(e13),e23)**. % 1.28/1.52 910[0:Rew:85.0,293.1] || SkC109 -> equal(h3(e13),e22)**. % 1.28/1.52 911[0:Rew:85.0,292.1] || SkC108 -> equal(h3(e13),e22)**. % 1.28/1.52 913[0:Rew:85.0,290.1] || SkC107 -> equal(h3(e13),e22)**. % 1.28/1.52 914[0:Rew:34.0,289.1] || SkC106* -> equal(e23,e22). % 1.28/1.52 915[0:MRR:914.1,12.0] || SkC106* -> . % 1.28/1.52 918[0:Rew:84.0,283.1] || SkC103 -> equal(h2(e13),e21)**. % 1.28/1.52 919[0:Rew:34.0,281.1] || SkC102* -> equal(e23,e21). % 1.28/1.52 920[0:MRR:919.1,11.0] || SkC102* -> . % 1.28/1.52 924[0:Rew:34.0,273.1] || SkC98* -> equal(e23,e20). % 1.28/1.52 925[0:MRR:924.1,9.0] || SkC98* -> . % 1.28/1.52 926[0:Rew:86.0,271.1] || SkC97 -> equal(h4(e13),e23)**. % 1.28/1.52 929[0:Rew:86.0,263.1] || SkC93 -> equal(h4(e13),e22)**. % 1.28/1.52 930[0:Rew:85.0,261.1] || SkC92 -> equal(h3(e13),e22)**. % 1.28/1.52 932[0:Rew:34.0,257.1] || SkC90* -> equal(e23,e22). % 1.28/1.52 933[0:MRR:932.1,12.0] || SkC90* -> . % 1.28/1.52 935[0:Rew:84.0,254.1] || SkC89 -> equal(h2(e13),e21)**. % 1.28/1.52 937[0:Rew:84.0,252.1] || SkC88 -> equal(h2(e13),e21)**. % 1.28/1.52 938[0:Rew:84.0,251.1] || SkC87 -> equal(h2(e13),e21)**. % 1.28/1.52 939[0:Rew:34.0,250.1] || SkC86* -> equal(e23,e21). % 1.28/1.52 940[0:MRR:939.1,11.0] || SkC86* -> . % 1.28/1.52 941[0:Rew:86.0,248.1] || SkC85 -> equal(h4(e13),e20)**. % 1.28/1.52 942[0:Rew:85.0,246.1] || SkC84 -> equal(h3(e13),e20)**. % 1.28/1.52 944[0:Rew:34.0,242.1] || SkC82* -> equal(e23,e20). % 1.28/1.52 945[0:MRR:944.1,9.0] || SkC82* -> . % 1.28/1.52 946[0:Rew:86.0,240.1] || SkC81 -> equal(h4(e13),e23)**. % 1.28/1.52 949[0:Rew:86.0,232.1] || SkC77 -> equal(h4(e13),e22)**. % 1.28/1.52 950[0:Rew:85.0,230.1] || SkC76 -> equal(h3(e13),e22)**. % 1.28/1.52 951[0:Rew:84.0,228.1] || SkC75 -> equal(h2(e13),e22)**. % 1.28/1.52 952[0:Rew:34.0,226.1] || SkC74* -> equal(e23,e22). % 1.28/1.52 953[0:MRR:952.1,12.0] || SkC74* -> . % 1.28/1.52 955[0:Rew:85.0,222.1] || SkC72 -> equal(h3(e13),e21)**. % 1.28/1.52 956[0:Rew:84.0,220.1] || SkC71 -> equal(h2(e13),e21)**. % 1.28/1.52 957[0:Rew:34.0,218.1] || SkC70* -> equal(e23,e21). % 1.28/1.52 958[0:MRR:957.1,11.0] || SkC70* -> . % 1.28/1.52 960[0:Rew:34.0,215.1] || SkC69* -> equal(e23,e20). % 1.28/1.52 961[0:MRR:960.1,9.0] || SkC69* -> . % 1.28/1.52 963[0:Rew:34.0,213.1] || SkC68* -> equal(e23,e20). % 1.28/1.52 964[0:MRR:963.1,9.0] || SkC68* -> . % 1.28/1.52 966[0:Rew:34.0,211.1] || SkC67* -> equal(e23,e20). % 1.28/1.52 967[0:MRR:966.1,9.0] || SkC67* -> . % 1.28/1.52 968[0:Rew:34.0,210.1] || SkC66* -> equal(e23,e20). % 1.28/1.52 969[0:MRR:968.1,9.0] || SkC66* -> . % 1.28/1.52 970[0:Rew:33.0,197.1] || SkC56* -> equal(e13,e12). % 1.28/1.52 971[0:MRR:970.1,6.0] || SkC56* -> . % 1.28/1.52 972[0:Rew:33.0,189.1] || SkC52* -> equal(e13,e11). % 1.28/1.52 973[0:MRR:972.1,5.0] || SkC52* -> . % 1.28/1.52 974[0:Rew:879.0,186.1] || SkC51* -> equal(e13,e12). % 1.28/1.52 975[0:MRR:974.1,6.0] || SkC51* -> . % 1.28/1.52 976[0:Rew:879.0,184.1] || SkC50* -> equal(e13,e12). % 1.28/1.52 977[0:MRR:976.1,6.0] || SkC50* -> . % 1.28/1.52 978[0:Rew:879.0,182.1] || SkC49* -> equal(e13,e12). % 1.28/1.52 979[0:MRR:978.1,6.0] || SkC49* -> . % 1.28/1.52 980[0:Rew:33.0,181.1] || SkC48* -> equal(e13,e10). % 1.28/1.52 981[0:MRR:980.1,3.0] || SkC48* -> . % 1.28/1.52 982[0:Rew:33.0,166.1] || SkC40* -> equal(e13,e12). % 1.28/1.52 983[0:MRR:982.1,6.0] || SkC40* -> . % 1.28/1.52 984[0:Rew:33.0,158.1] || SkC36* -> equal(e13,e11). % 1.28/1.52 985[0:MRR:984.1,5.0] || SkC36* -> . % 1.28/1.52 986[0:Rew:33.0,150.1] || SkC32* -> equal(e13,e10). % 1.28/1.52 987[0:MRR:986.1,3.0] || SkC32* -> . % 1.28/1.52 988[0:Rew:33.0,134.1] || SkC24* -> equal(e13,e12). % 1.28/1.52 989[0:MRR:988.1,6.0] || SkC24* -> . % 1.28/1.52 990[0:Rew:33.0,127.1] || SkC20* -> equal(e13,e11). % 1.28/1.52 991[0:MRR:990.1,5.0] || SkC20* -> . % 1.28/1.52 992[0:Rew:33.0,119.1] || SkC16* -> equal(e13,e10). % 1.28/1.52 993[0:MRR:992.1,3.0] || SkC16* -> . % 1.28/1.52 994[0:Rew:33.0,103.1] || SkC8* -> equal(e13,e12). % 1.28/1.52 995[0:MRR:994.1,6.0] || SkC8* -> . % 1.28/1.52 996[0:Rew:33.0,95.1] || SkC4* -> equal(e13,e11). % 1.28/1.52 997[0:MRR:996.1,5.0] || SkC4* -> . % 1.28/1.52 998[0:Rew:33.0,92.1] || SkC3* -> equal(e13,e10). % 1.28/1.52 999[0:MRR:998.1,3.0] || SkC3* -> . % 1.28/1.52 1000[0:Rew:33.0,90.1] || SkC2* -> equal(e13,e10). % 1.28/1.52 1001[0:MRR:1000.1,3.0] || SkC2* -> . % 1.28/1.52 1002[0:Rew:33.0,88.1] || SkC1* -> equal(e13,e10). % 1.28/1.52 1003[0:MRR:1002.1,3.0] || SkC1* -> . % 1.28/1.52 1004[0:Rew:33.0,87.1] || SkC0* -> equal(e13,e10). % 1.28/1.52 1005[0:MRR:1004.1,3.0] || SkC0* -> . % 1.28/1.52 1006[0:Rew:86.0,680.0] || -> equal(op2(h4(e13),e23),h4(e12))**. % 1.28/1.52 1008[0:Rew:84.0,678.0] || -> equal(op2(h2(e13),e21),h2(e12))**. % 1.28/1.52 1009[0:Rew:878.0,677.0,34.0,677.0] || -> equal(h1(e12),e22)**. % 1.28/1.52 1010[0:Rew:1009.0,45.0] || equal(e22,e22) -> SkC134*. % 1.28/1.52 1012[0:Obv:1010.0] || -> SkC134*. % 1.28/1.52 1013[0:Rew:881.1,675.0,86.0,675.0] || equal(e23,e23) SkC128* -> . % 1.28/1.52 1014[0:Obv:1013.0] || SkC128* -> . % 1.28/1.52 1015[0:Rew:883.1,673.0,86.0,673.0] || equal(e23,e23) SkC127* -> . % 1.28/1.52 1016[0:Obv:1015.0] || SkC127* -> . % 1.28/1.52 1017[0:Rew:884.1,671.0,86.0,671.0] || equal(e23,e23) SkC126* -> . % 1.28/1.52 1018[0:Obv:1017.0] || SkC126* -> . % 1.28/1.52 1019[0:Rew:325.1,670.0] || equal(e23,e23) SkC125* -> . % 1.28/1.52 1020[0:Obv:1019.0] || SkC125* -> . % 1.28/1.52 1021[0:Rew:886.1,668.0,85.0,668.0] || equal(e22,e22) SkC124* -> . % 1.28/1.52 1022[0:Obv:1021.0] || SkC124* -> . % 1.28/1.52 1024[0:Rew:317.1,662.0] || equal(e23,e23) SkC121* -> . % 1.28/1.52 1025[0:Obv:1024.0] || SkC121* -> . % 1.28/1.52 1026[0:Rew:86.0,659.0] || equal(h4(e13),e21)** SkC120 -> . % 1.28/1.52 1027[0:Rew:892.1,658.0,84.0,658.0] || equal(e21,e21) SkC119* -> . % 1.28/1.52 1028[0:Obv:1027.0] || SkC119* -> . % 1.28/1.52 1029[0:Rew:906.1,646.0,86.0,646.0] || equal(e23,e23) SkC113* -> . % 1.28/1.52 1030[0:Obv:1029.0] || SkC113* -> . % 1.28/1.52 1031[0:Rew:299.1,644.0] || equal(e22,e22) SkC112* -> . % 1.28/1.52 1032[0:Obv:1031.0] || SkC112* -> . % 1.28/1.52 1034[0:Rew:85.0,639.0] || SkC110 equal(h3(e13),e23)** -> . % 1.28/1.52 1035[0:Rew:910.1,637.0,85.0,637.0] || equal(e22,e22) SkC109* -> . % 1.28/1.52 1036[0:Obv:1035.0] || SkC109* -> . % 1.28/1.52 1037[0:Rew:911.1,636.0,85.0,636.0] || equal(e22,e22) SkC108* -> . % 1.28/1.52 1038[0:Obv:1037.0] || SkC108* -> . % 1.28/1.52 1039[0:Rew:913.1,634.0,85.0,634.0] || equal(e22,e22) SkC107* -> . % 1.28/1.52 1040[0:Obv:1039.0] || SkC107* -> . % 1.28/1.52 1041[0:Rew:85.0,630.0] || SkC105 equal(h3(e13),e21)** -> . % 1.28/1.52 1042[0:Rew:284.1,629.0] || equal(e22,e22) SkC104* -> . % 1.28/1.52 1043[0:Obv:1042.0] || SkC104* -> . % 1.28/1.52 1044[0:Rew:918.1,627.0,84.0,627.0] || equal(e21,e21) SkC103* -> . % 1.28/1.52 1045[0:Obv:1044.0] || SkC103* -> . % 1.28/1.52 1048[0:Rew:276.1,621.0] || equal(e22,e22) SkC100* -> . % 1.28/1.52 1049[0:Obv:1048.0] || SkC100* -> . % 1.28/1.52 1051[0:Rew:926.1,615.0,86.0,615.0] || equal(e23,e23) SkC97* -> . % 1.28/1.52 1052[0:Obv:1051.0] || SkC97* -> . % 1.28/1.52 1054[0:Rew:266.1,611.0] || equal(e21,e21) SkC95* -> . % 1.28/1.52 1055[0:Obv:1054.0] || SkC95* -> . % 1.28/1.52 1058[0:Rew:930.1,605.0,85.0,605.0] || equal(e22,e22) SkC92* -> . % 1.28/1.52 1059[0:Obv:1058.0] || SkC92* -> . % 1.28/1.52 1060[0:Rew:258.1,603.0] || equal(e21,e21) SkC91* -> . % 1.28/1.52 1061[0:Obv:1060.0] || SkC91* -> . % 1.28/1.52 1062[0:Rew:935.1,598.0,84.0,598.0] || equal(e21,e21) SkC89* -> . % 1.28/1.52 1063[0:Obv:1062.0] || SkC89* -> . % 1.28/1.52 1064[0:Rew:937.1,596.0,84.0,596.0] || equal(e21,e21) SkC88* -> . % 1.28/1.52 1065[0:Obv:1064.0] || SkC88* -> . % 1.28/1.52 1066[0:Rew:938.1,595.0,84.0,595.0] || equal(e21,e21) SkC87* -> . % 1.28/1.52 1067[0:Obv:1066.0] || SkC87* -> . % 1.28/1.52 1070[0:Rew:84.0,589.0] || SkC84 equal(h2(e13),e20)** -> . % 1.28/1.52 1071[0:Rew:243.1,588.0] || equal(e21,e21) SkC83* -> . % 1.28/1.52 1072[0:Obv:1071.0] || SkC83* -> . % 1.28/1.52 1073[0:Rew:946.1,584.0,86.0,584.0] || equal(e23,e23) SkC81* -> . % 1.28/1.52 1074[0:Obv:1073.0] || SkC81* -> . % 1.28/1.52 1075[0:Rew:34.0,581.0] || equal(e23,e23) SkC80* -> . % 1.28/1.52 1076[0:Obv:1075.0] || SkC80* -> . % 1.28/1.52 1077[0:Rew:34.0,579.0] || equal(e23,e23) SkC79* -> . % 1.28/1.52 1078[0:Obv:1077.0] || SkC79* -> . % 1.28/1.52 1079[0:Rew:233.1,578.0] || equal(e20,e20) SkC78* -> . % 1.28/1.52 1080[0:Obv:1079.0] || SkC78* -> . % 1.28/1.52 1082[0:Rew:950.1,574.0,85.0,574.0] || equal(e22,e22) SkC76* -> . % 1.28/1.52 1083[0:Obv:1082.0] || SkC76* -> . % 1.28/1.52 1087[0:Rew:956.1,564.0,84.0,564.0] || equal(e21,e21) SkC71* -> . % 1.28/1.52 1088[0:Obv:1087.0] || SkC71* -> . % 1.28/1.52 1089[0:Rew:208.1,552.0] || equal(e13,e13) SkC62* -> . % 1.28/1.52 1090[0:Obv:1089.0] || SkC62* -> . % 1.28/1.52 1091[0:Rew:206.1,550.0] || equal(e13,e13) SkC61* -> . % 1.28/1.52 1092[0:Obv:1091.0] || SkC61* -> . % 1.28/1.52 1093[0:Rew:204.1,548.0] || equal(e13,e13) SkC60* -> . % 1.28/1.52 1094[0:Obv:1093.0] || SkC60* -> . % 1.28/1.52 1095[0:Rew:202.1,547.0] || equal(e13,e13) SkC59* -> . % 1.28/1.52 1096[0:Obv:1095.0] || SkC59* -> . % 1.28/1.52 1097[0:Rew:201.1,545.0] || equal(e12,e12) SkC58* -> . % 1.28/1.52 1098[0:Obv:1097.0] || SkC58* -> . % 1.28/1.52 1099[0:Rew:194.1,539.0] || equal(e13,e13) SkC55* -> . % 1.28/1.52 1100[0:Obv:1099.0] || SkC55* -> . % 1.28/1.52 1101[0:Rew:191.1,535.0] || equal(e11,e11) SkC53* -> . % 1.28/1.52 1102[0:Obv:1101.0] || SkC53* -> . % 1.28/1.52 1103[0:Rew:179.1,523.0] || equal(e13,e13) SkC47* -> . % 1.28/1.52 1104[0:Obv:1103.0] || SkC47* -> . % 1.28/1.52 1105[0:Rew:176.1,521.0] || equal(e12,e12) SkC46* -> . % 1.28/1.52 1106[0:Obv:1105.0] || SkC46* -> . % 1.28/1.52 1107[0:Rew:170.1,514.0] || equal(e12,e12) SkC43* -> . % 1.28/1.52 1108[0:Obv:1107.0] || SkC43* -> . % 1.28/1.52 1109[0:Rew:169.1,513.0] || equal(e12,e12) SkC42* -> . % 1.28/1.52 1110[0:Obv:1109.0] || SkC42* -> . % 1.28/1.52 1111[0:Rew:167.1,511.0] || equal(e12,e12) SkC41* -> . % 1.28/1.52 1112[0:Obv:1111.0] || SkC41* -> . % 1.28/1.52 1113[0:Rew:161.1,506.0] || equal(e12,e12) SkC38* -> . % 1.28/1.52 1114[0:Obv:1113.0] || SkC38* -> . % 1.28/1.52 1115[0:Rew:160.1,504.0] || equal(e11,e11) SkC37* -> . % 1.28/1.52 1116[0:Obv:1115.0] || SkC37* -> . % 1.28/1.52 1118[0:Rew:153.1,498.0] || equal(e12,e12) SkC34* -> . % 1.28/1.52 1119[0:Obv:1118.0] || SkC34* -> . % 1.28/1.52 1120[0:Rew:148.1,492.0] || equal(e13,e13) SkC31* -> . % 1.28/1.52 1121[0:Obv:1120.0] || SkC31* -> . % 1.28/1.52 1122[0:Rew:143.1,488.0] || equal(e11,e11) SkC29* -> . % 1.28/1.52 1123[0:Obv:1122.0] || SkC29* -> . % 1.28/1.52 1124[0:Rew:138.1,482.0] || equal(e12,e12) SkC26* -> . % 1.28/1.52 1125[0:Obv:1124.0] || SkC26* -> . % 1.28/1.52 1126[0:Rew:135.1,480.0] || equal(e11,e11) SkC25* -> . % 1.28/1.52 1127[0:Obv:1126.0] || SkC25* -> . % 1.28/1.52 1128[0:Rew:131.1,475.0] || equal(e11,e11) SkC23* -> . % 1.28/1.52 1129[0:Obv:1128.0] || SkC23* -> . % 1.28/1.52 1130[0:Rew:129.1,473.0] || equal(e11,e11) SkC22* -> . % 1.28/1.52 1131[0:Obv:1130.0] || SkC22* -> . % 1.28/1.52 1132[0:Rew:128.1,472.0] || equal(e11,e11) SkC21* -> . % 1.28/1.52 1133[0:Obv:1132.0] || SkC21* -> . % 1.28/1.52 1135[0:Rew:120.1,465.0] || equal(e11,e11) SkC17* -> . % 1.28/1.52 1136[0:Obv:1135.0] || SkC17* -> . % 1.28/1.52 1137[0:Rew:117.1,461.0] || equal(e13,e13) SkC15* -> . % 1.28/1.52 1138[0:Obv:1137.0] || SkC15* -> . % 1.28/1.52 1139[0:Rew:33.0,458.0] || equal(e13,e13) SkC14* -> . % 1.28/1.52 1140[0:Obv:1139.0] || SkC14* -> . % 1.28/1.52 1141[0:Rew:33.0,456.0] || equal(e13,e13) SkC13* -> . % 1.28/1.52 1142[0:Obv:1141.0] || SkC13* -> . % 1.28/1.52 1143[0:Rew:110.1,455.0] || equal(e10,e10) SkC12* -> . % 1.28/1.52 1144[0:Obv:1143.0] || SkC12* -> . % 1.28/1.52 1146[0:Rew:107.1,451.0] || equal(e12,e12) SkC10* -> . % 1.28/1.52 1147[0:Obv:1146.0] || SkC10* -> . % 1.28/1.52 1151[0:Rew:97.1,441.0] || equal(e11,e11) SkC5* -> . % 1.28/1.52 1152[0:Obv:1151.0] || SkC5* -> . % 1.28/1.52 1153[0:Rew:86.0,430.0] || equal(op2(e23,e22),h4(e13))** -> . % 1.28/1.52 1154[0:Rew:86.0,429.0] || equal(op2(e23,e21),h4(e13))** -> . % 1.28/1.52 1155[0:Rew:86.0,427.0,878.0,427.0] || equal(h4(e13),e22)** -> . % 1.28/1.52 1156[0:MRR:929.1,1155.0] || SkC93* -> . % 1.28/1.52 1157[0:MRR:949.1,1155.0] || SkC77* -> . % 1.28/1.52 1158[0:Rew:878.0,426.0] || equal(op2(e23,e22),e22)** -> . % 1.28/1.52 1159[0:Rew:878.0,425.0] || equal(op2(e23,e21),e22)** -> . % 1.28/1.52 1160[0:Rew:85.0,424.0] || equal(op2(e22,e23),h3(e13))** -> . % 1.28/1.52 1161[0:Rew:85.0,422.0] || equal(op2(e22,e21),h3(e13))** -> . % 1.28/1.52 1162[0:Rew:85.0,420.0] || equal(op2(e22,e20),h3(e13))** -> . % 1.28/1.52 1163[0:Rew:84.0,417.0] || equal(op2(e21,e23),h2(e13))** -> . % 1.28/1.52 1164[0:Rew:84.0,416.0] || equal(op2(e21,e22),h2(e13))** -> . % 1.28/1.52 1165[0:Rew:84.0,413.0] || equal(op2(e21,e20),h2(e13))** -> . % 1.28/1.52 1166[0:Rew:34.0,409.0] || equal(op2(e20,e23),e23)** -> . % 1.28/1.52 1168[0:Rew:34.0,407.0] || equal(op2(e20,e21),e23)** -> . % 1.28/1.52 1169[0:Rew:86.0,406.0] || equal(op2(e22,e23),h4(e13))** -> . % 1.28/1.52 1170[0:Rew:86.0,405.0] || equal(op2(e21,e23),h4(e13))** -> . % 1.28/1.52 1171[0:Rew:86.0,403.0] || equal(op2(e20,e23),h4(e13))** -> . % 1.28/1.52 1172[0:Rew:85.0,400.0] || equal(op2(e23,e22),h3(e13))** -> . % 1.28/1.52 1173[0:Rew:85.0,398.0] || equal(op2(e21,e22),h3(e13))** -> . % 1.28/1.52 1174[0:Rew:85.0,396.0] || equal(op2(e20,e22),h3(e13))** -> . % 1.28/1.52 1175[0:Rew:84.0,393.0] || equal(op2(e23,e21),h2(e13))** -> . % 1.28/1.52 1176[0:Rew:84.0,392.0] || equal(op2(e22,e21),h2(e13))** -> . % 1.28/1.52 1177[0:Rew:84.0,389.0] || equal(op2(e20,e21),h2(e13))** -> . % 1.28/1.52 1178[0:Rew:878.0,388.0] || equal(op2(e22,e20),e22)** -> . % 1.28/1.52 1179[0:MRR:278.1,1178.0] || SkC101* -> . % 1.28/1.52 1180[0:MRR:274.1,1178.0] || SkC99* -> . % 1.28/1.52 1181[0:Rew:878.0,387.0] || equal(op2(e21,e20),e22)** -> . % 1.28/1.52 1183[0:Rew:34.0,384.0] || equal(op2(e22,e20),e23)** -> . % 1.28/1.52 1184[0:Rew:34.0,383.0] || equal(op2(e21,e20),e23)** -> . % 1.28/1.52 1185[0:Rew:879.0,379.0] || equal(op1(e13,e13),e12)** -> . % 1.28/1.52 1186[0:MRR:140.1,1185.0] || SkC27* -> . % 1.28/1.52 1187[0:MRR:109.1,1185.0] || SkC11* -> . % 1.28/1.52 1188[0:Rew:879.0,378.0] || equal(op1(e13,e12),e12)** -> . % 1.28/1.52 1189[0:Rew:879.0,377.0] || equal(op1(e13,e11),e12)** -> . % 1.28/1.52 1190[0:Rew:33.0,361.0] || equal(op1(e10,e13),e13)** -> . % 1.28/1.52 1191[0:Rew:33.0,360.0] || equal(op1(e10,e12),e13)** -> . % 1.28/1.52 1192[0:Rew:33.0,359.0] || equal(op1(e10,e11),e13)** -> . % 1.28/1.52 1193[0:Rew:879.0,340.0] || equal(op1(e12,e10),e12)** -> . % 1.28/1.52 1194[0:MRR:155.1,1193.0] || SkC35* -> . % 1.28/1.52 1195[0:MRR:151.1,1193.0] || SkC33* -> . % 1.28/1.52 1196[0:Rew:879.0,339.0] || equal(op1(e11,e10),e12)** -> . % 1.28/1.52 1198[0:Rew:33.0,336.0] || equal(op1(e12,e10),e13)** -> . % 1.28/1.52 1199[0:Rew:33.0,335.0] || equal(op1(e11,e10),e13)** -> . % 1.28/1.52 1200[0:Rew:86.0,706.0,34.0,706.0] || -> equal(h4(e13),e21)**. % 1.28/1.52 1201[0:Rew:1200.0,86.0] || -> equal(op2(e23,e23),e21)**. % 1.28/1.52 1202[0:Rew:1200.0,1026.0] || equal(e21,e21) SkC120* -> . % 1.28/1.52 1204[0:Rew:1200.0,941.1] || SkC85* -> equal(e21,e20). % 1.28/1.52 1206[0:Rew:1200.0,1006.0] || -> equal(op2(e21,e23),h4(e12))**. % 1.28/1.52 1207[0:Rew:1200.0,1153.0] || equal(op2(e23,e22),e21)** -> . % 1.28/1.52 1208[0:Rew:1200.0,1154.0] || equal(op2(e23,e21),e21)** -> . % 1.28/1.52 1210[0:Rew:1200.0,1169.0] || equal(op2(e22,e23),e21)** -> . % 1.28/1.52 1211[0:Rew:1200.0,1170.0] || equal(op2(e21,e23),e21)** -> . % 1.28/1.52 1212[0:Rew:1200.0,1171.0] || equal(op2(e20,e23),e21)** -> . % 1.28/1.52 1214[0:MRR:1204.1,7.0] || SkC85* -> . % 1.28/1.52 1215[0:Obv:1202.0] || SkC120* -> . % 1.28/1.52 1217[0:Rew:1206.0,264.1] || SkC94 -> equal(h4(e12),e21)**. % 1.28/1.52 1218[0:Rew:1206.0,268.1] || SkC96 -> equal(h4(e12),e21)**. % 1.28/1.52 1219[0:Rew:1206.0,418.0] || equal(op2(e21,e22),h4(e12))** -> . % 1.28/1.52 1220[0:Rew:1206.0,1163.0] || equal(h4(e12),h2(e13))** -> . % 1.28/1.52 1221[0:Rew:1206.0,415.0] || equal(op2(e21,e20),h4(e12))** -> . % 1.28/1.52 1222[0:Rew:1206.0,404.0] || equal(op2(e22,e23),h4(e12))** -> . % 1.28/1.52 1223[0:Rew:1206.0,401.0] || equal(op2(e20,e23),h4(e12))** -> . % 1.28/1.52 1224[0:Rew:1206.0,1211.0] || equal(h4(e12),e21)** -> . % 1.28/1.52 1225[0:MRR:1217.1,1224.0] || SkC94* -> . % 1.28/1.52 1226[0:MRR:1218.1,1224.0] || SkC96* -> . % 1.28/1.52 1227[0:Rew:33.0,705.0] || -> equal(op1(e13,e13),e11)**. % 1.28/1.52 1228[0:Rew:1227.0,536.0] || equal(e11,e11) SkC54* -> . % 1.28/1.52 1229[0:Rew:1227.0,125.1] || SkC19* -> equal(e11,e10). % 1.28/1.52 1230[0:Rew:1227.0,382.0] || equal(op1(e13,e12),e11)** -> . % 1.28/1.52 1231[0:Rew:1227.0,381.0] || equal(op1(e13,e11),e11)** -> . % 1.28/1.52 1233[0:Rew:1227.0,358.0] || equal(op1(e12,e13),e11)** -> . % 1.28/1.52 1234[0:Rew:1227.0,357.0] || equal(op1(e11,e13),e11)** -> . % 1.28/1.52 1235[0:Rew:1227.0,355.0] || equal(op1(e10,e13),e11)** -> . % 1.28/1.52 1236[0:MRR:1229.1,1.0] || SkC19* -> . % 1.28/1.52 1237[0:Obv:1228.0] || SkC54* -> . % 1.28/1.52 1238[0:MRR:145.1,1234.0] || SkC30* -> . % 1.28/1.52 1239[0:MRR:141.1,1234.0] || SkC28* -> . % 1.28/1.52 1240[0:Rew:85.0,703.1] || SkC131 -> equal(op2(e22,h3(e13)),e22)**. % 1.28/1.52 1243[0:Rew:34.0,693.1] || SkC129 -> equal(op2(e20,e23),e20)**. % 1.28/1.52 1245[0:Rew:33.0,681.1] || SkC63 -> equal(op1(e10,e13),e10)**. % 1.28/1.52 1251[0:Rew:84.0,716.0] || -> equal(op2(h2(e13),h2(e13)),h2(e11))**. % 1.28/1.52 1252[0:Rew:1201.0,715.0,34.0,715.0] || -> equal(h1(e11),e21)**. % 1.28/1.52 1253[0:Rew:1252.0,40.0] || equal(e21,e21) -> SkC133*. % 1.28/1.52 1254[0:Obv:1253.0] || -> SkC133*. % 1.28/1.52 1255[0:Rew:1201.0,714.0] || -> equal(op2(e23,e21),e23)** SkC129 SkC130 SkC131. % 1.28/1.52 1259[0:Rew:1227.0,710.0] || -> equal(op1(e13,e11),e13)** SkC63 SkC64 SkC65. % 1.28/1.52 1261[0:Rew:879.0,707.0] || -> SkC65 SkC64 SkC63 equal(op1(e13,e12),e10)**. % 1.28/1.52 1266[0:Rew:1201.0,733.0] || equal(e21,e21) SkC130 -> equal(op2(e23,e21),e23)**. % 1.28/1.52 1267[0:Obv:1266.0] || SkC130 -> equal(op2(e23,e21),e23)**. % 1.28/1.52 1268[0:MRR:1255.2,1267.0] || -> SkC131 SkC129 equal(op2(e23,e21),e23)**. % 1.28/1.52 1272[0:Rew:85.0,729.0] || equal(h3(e13),e20) SkC129 -> equal(op2(e22,e20),e22)**. % 1.28/1.52 1273[0:MRR:1272.2,1178.0] || SkC129 equal(h3(e13),e20)** -> . % 1.28/1.52 1277[0:Rew:1227.0,724.0] || equal(e11,e11) SkC64 -> equal(op1(e13,e11),e13)**. % 1.28/1.52 1278[0:Obv:1277.0] || SkC64 -> equal(op1(e13,e11),e13)**. % 1.28/1.52 1279[0:MRR:1259.2,1278.0] || -> SkC65 SkC63 equal(op1(e13,e11),e13)**. % 1.28/1.52 1282[0:MRR:720.2,1193.0] || SkC63 equal(op1(e12,e12),e10)** -> . % 1.28/1.52 1286[0:Rew:34.0,740.0] || equal(e23,e23) -> equal(op2(e20,e23),e20)** SkC129 SkC130 SkC131. % 1.28/1.52 1287[0:Obv:1286.0] || -> equal(op2(e20,e23),e20)** SkC129 SkC130 SkC131. % 1.28/1.52 1288[0:MRR:1287.1,1243.0] || -> SkC131 SkC130 equal(op2(e20,e23),e20)**. % 1.28/1.52 1290[0:Rew:33.0,737.0] || equal(e13,e13) -> equal(op1(e10,e13),e10)** SkC63 SkC64 SkC65. % 1.28/1.52 1291[0:Obv:1290.0] || -> equal(op1(e10,e13),e10)** SkC63 SkC64 SkC65. % 1.28/1.52 1292[0:MRR:1291.1,1245.0] || -> SkC65 SkC64 equal(op1(e10,e13),e10)**. % 1.28/1.52 1293[0:Rew:1201.0,743.3,1206.0,743.1] || -> equal(op2(e20,e23),e23) equal(h4(e12),e23) equal(op2(e22,e23),e23)** equal(e23,e21). % 1.28/1.52 1294[0:MRR:1293.0,1293.3,1166.0,11.0] || -> equal(h4(e12),e23) equal(op2(e22,e23),e23)**. % 1.28/1.52 1295[0:Rew:1201.0,744.3,878.0,744.0] || -> equal(e23,e22) equal(op2(e23,e21),e23) equal(op2(e23,e22),e23)** equal(e23,e21). % 1.28/1.52 1296[0:MRR:1295.0,1295.3,12.0,11.0] || -> equal(op2(e23,e22),e23)** equal(op2(e23,e21),e23). % 1.28/1.52 1297[0:Rew:1201.0,745.3,1206.0,745.1] || -> equal(op2(e20,e23),e22) equal(h4(e12),e22) equal(op2(e22,e23),e22)** equal(e22,e21). % 1.28/1.52 1298[0:MRR:1297.3,10.0] || -> equal(h4(e12),e22) equal(op2(e22,e23),e22)** equal(op2(e20,e23),e22). % 1.28/1.52 1299[0:Rew:1201.0,749.3,1206.0,749.1] || -> equal(op2(e20,e23),e20) equal(h4(e12),e20) equal(op2(e22,e23),e20)** equal(e21,e20). % 1.28/1.52 1300[0:MRR:1299.3,7.0] || -> equal(h4(e12),e20) equal(op2(e20,e23),e20) equal(op2(e22,e23),e20)**. % 1.28/1.52 1301[0:Rew:1201.0,750.3,878.0,750.0] || -> equal(e22,e20) equal(op2(e23,e21),e20) equal(op2(e23,e22),e20)** equal(e21,e20). % 1.28/1.52 1302[0:MRR:1301.0,1301.3,8.0,7.0] || -> equal(op2(e23,e22),e20)** equal(op2(e23,e21),e20). % 1.28/1.52 1305[0:Rew:85.0,752.2] || -> equal(op2(e22,e20),e23) equal(op2(e22,e21),e23) equal(h3(e13),e23) equal(op2(e22,e23),e23)**. % 1.28/1.52 1306[0:MRR:1305.0,1183.0] || -> equal(h3(e13),e23) equal(op2(e22,e23),e23)** equal(op2(e22,e21),e23). % 1.28/1.52 1307[0:Rew:85.0,753.2] || -> equal(op2(e20,e22),e22) equal(op2(e21,e22),e22) equal(h3(e13),e22) equal(op2(e23,e22),e22)**. % 1.28/1.52 1308[0:MRR:1307.3,1158.0] || -> equal(h3(e13),e22) equal(op2(e21,e22),e22)** equal(op2(e20,e22),e22). % 1.28/1.52 1309[0:Rew:85.0,754.2] || -> equal(op2(e22,e20),e22) equal(op2(e22,e21),e22) equal(h3(e13),e22) equal(op2(e22,e23),e22)**. % 1.28/1.52 1310[0:MRR:1309.0,1178.0] || -> equal(h3(e13),e22) equal(op2(e22,e23),e22)** equal(op2(e22,e21),e22). % 1.28/1.52 1311[0:Rew:85.0,755.2] || -> equal(op2(e20,e22),e21) equal(op2(e21,e22),e21) equal(h3(e13),e21) equal(op2(e23,e22),e21)**. % 1.28/1.52 1312[0:MRR:1311.3,1207.0] || -> equal(h3(e13),e21) equal(op2(e21,e22),e21)** equal(op2(e20,e22),e21). % 1.28/1.52 1313[0:Rew:85.0,756.2] || -> equal(op2(e22,e20),e21) equal(op2(e22,e21),e21) equal(h3(e13),e21) equal(op2(e22,e23),e21)**. % 1.28/1.52 1314[0:MRR:1313.3,1210.0] || -> equal(h3(e13),e21) equal(op2(e22,e21),e21)** equal(op2(e22,e20),e21). % 1.28/1.52 1315[0:Rew:85.0,757.2] || -> equal(h3(e13),e20) equal(op2(e20,e22),e20) equal(op2(e23,e22),e20)** equal(op2(e21,e22),e20). % 1.28/1.52 1317[0:Rew:84.0,759.1] || -> equal(op2(e20,e21),e23) equal(h2(e13),e23) equal(op2(e22,e21),e23) equal(op2(e23,e21),e23)**. % 1.28/1.52 1318[0:MRR:1317.0,1168.0] || -> equal(h2(e13),e23) equal(op2(e23,e21),e23)** equal(op2(e22,e21),e23). % 1.28/1.52 1319[0:Rew:1206.0,760.3,84.0,760.1] || -> equal(op2(e21,e20),e23) equal(h2(e13),e23) equal(op2(e21,e22),e23)** equal(h4(e12),e23). % 1.28/1.52 1320[0:MRR:1319.0,1184.0] || -> equal(h4(e12),e23) equal(h2(e13),e23) equal(op2(e21,e22),e23)**. % 1.28/1.52 1321[0:Rew:84.0,761.1] || -> equal(op2(e20,e21),e22) equal(h2(e13),e22) equal(op2(e22,e21),e22) equal(op2(e23,e21),e22)**. % 1.28/1.52 1322[0:MRR:1321.3,1159.0] || -> equal(h2(e13),e22) equal(op2(e22,e21),e22)** equal(op2(e20,e21),e22). % 1.28/1.52 1325[0:Rew:84.0,763.1] || -> equal(op2(e20,e21),e21) equal(h2(e13),e21) equal(op2(e22,e21),e21) equal(op2(e23,e21),e21)**. % 1.28/1.52 1326[0:MRR:1325.3,1208.0] || -> equal(h2(e13),e21) equal(op2(e22,e21),e21)** equal(op2(e20,e21),e21). % 1.28/1.52 1329[0:Rew:84.0,765.1] || -> equal(h2(e13),e20) equal(op2(e20,e21),e20) equal(op2(e23,e21),e20)** equal(op2(e22,e21),e20). % 1.28/1.52 1331[0:Rew:34.0,770.0] || -> equal(e23,e22) equal(op2(e20,e21),e22) equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)**. % 1.28/1.52 1332[0:MRR:1331.0,12.0] || -> equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)** equal(op2(e20,e21),e22). % 1.28/1.52 1333[0:Rew:878.0,771.3,34.0,771.0] || -> equal(e23,e21) equal(op2(e21,e20),e21) equal(op2(e22,e20),e21)** equal(e22,e21). % 1.28/1.52 1334[0:MRR:1333.0,1333.3,11.0,10.0] || -> equal(op2(e21,e20),e21) equal(op2(e22,e20),e21)**. % 1.28/1.52 1335[0:Rew:34.0,772.0] || -> equal(e23,e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21) equal(op2(e20,e23),e21)**. % 1.28/1.52 1336[0:MRR:1335.0,1335.3,11.0,1212.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e22),e21)**. % 1.28/1.52 1337[0:Rew:878.0,773.3,34.0,773.0] || -> equal(e23,e20) equal(op2(e21,e20),e20) equal(op2(e22,e20),e20)** equal(e22,e20). % 1.28/1.52 1338[0:MRR:1337.0,1337.3,9.0,8.0] || -> equal(op2(e22,e20),e20)** equal(op2(e21,e20),e20). % 1.28/1.52 1342[0:MRR:777.1,777.2,1208.0,1159.0] || -> equal(op2(e23,e21),e23)** equal(op2(e23,e21),e20). % 1.28/1.52 1344[0:Rew:85.0,780.3,85.0,780.2,85.0,780.1,85.0,780.0] || -> equal(h3(e13),e23)** equal(h3(e13),e22) equal(h3(e13),e21) equal(h3(e13),e20). % 1.28/1.52 1346[0:Rew:1206.0,783.3,1206.0,783.2,1206.0,783.1,1206.0,783.0] || -> equal(h4(e12),e20) equal(h4(e12),e21) equal(h4(e12),e22) equal(h4(e12),e23)**. % 1.28/1.52 1347[0:MRR:1346.1,1224.0] || -> equal(h4(e12),e23)** equal(h4(e12),e22) equal(h4(e12),e20). % 1.28/1.52 1348[0:Rew:84.0,785.3,84.0,785.2,84.0,785.1,84.0,785.0] || -> equal(h2(e13),e23)** equal(h2(e13),e22) equal(h2(e13),e21) equal(h2(e13),e20). % 1.28/1.52 1349[0:MRR:786.2,786.3,1181.0,1184.0] || -> equal(op2(e21,e20),e21)** equal(op2(e21,e20),e20). % 1.28/1.52 1350[0:MRR:787.1,787.3,1212.0,1166.0] || -> equal(op2(e20,e23),e20) equal(op2(e20,e23),e22)**. % 1.28/1.52 1352[0:MRR:789.3,1168.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e21),e20) equal(op2(e20,e21),e22)**. % 1.28/1.52 1353[0:Rew:1227.0,791.3] || -> equal(op1(e10,e13),e13) equal(op1(e11,e13),e13) equal(op1(e12,e13),e13)** equal(e13,e11). % 1.28/1.52 1354[0:MRR:1353.0,1353.3,1190.0,5.0] || -> equal(op1(e12,e13),e13)** equal(op1(e11,e13),e13). % 1.28/1.52 1355[0:Rew:1227.0,792.3,879.0,792.0] || -> equal(e13,e12) equal(op1(e13,e11),e13) equal(op1(e13,e12),e13)** equal(e13,e11). % 1.28/1.52 1356[0:MRR:1355.0,1355.3,6.0,5.0] || -> equal(op1(e13,e12),e13)** equal(op1(e13,e11),e13). % 1.28/1.52 1357[0:Rew:1227.0,793.3] || -> equal(op1(e10,e13),e12) equal(op1(e11,e13),e12) equal(op1(e12,e13),e12)** equal(e12,e11). % 1.28/1.52 1358[0:MRR:1357.3,4.0] || -> equal(op1(e12,e13),e12)** equal(op1(e11,e13),e12) equal(op1(e10,e13),e12). % 1.28/1.52 1359[0:Rew:1227.0,797.3] || -> equal(op1(e10,e13),e10) equal(op1(e11,e13),e10) equal(op1(e12,e13),e10)** equal(e11,e10). % 1.28/1.52 1360[0:MRR:1359.3,1.0] || -> equal(op1(e10,e13),e10) equal(op1(e12,e13),e10)** equal(op1(e11,e13),e10). % 1.28/1.52 1361[0:Rew:1227.0,798.3,879.0,798.0] || -> equal(e12,e10) equal(op1(e13,e11),e10) equal(op1(e13,e12),e10)** equal(e11,e10). % 1.28/1.52 1362[0:MRR:1361.0,1361.3,2.0,1.0] || -> equal(op1(e13,e12),e10)** equal(op1(e13,e11),e10). % 1.28/1.52 1363[0:MRR:799.0,1191.0] || -> equal(op1(e13,e12),e13)** equal(op1(e12,e12),e13) equal(op1(e11,e12),e13). % 1.28/1.52 1364[0:MRR:800.0,1198.0] || -> equal(op1(e12,e13),e13)** equal(op1(e12,e12),e13) equal(op1(e12,e11),e13). % 1.28/1.52 1365[0:MRR:801.3,1188.0] || -> equal(op1(e12,e12),e12)** equal(op1(e11,e12),e12) equal(op1(e10,e12),e12). % 1.28/1.52 1366[0:MRR:802.0,1193.0] || -> equal(op1(e12,e12),e12) equal(op1(e12,e13),e12)** equal(op1(e12,e11),e12). % 1.28/1.52 1367[0:MRR:803.3,1230.0] || -> equal(op1(e12,e12),e11)** equal(op1(e11,e12),e11) equal(op1(e10,e12),e11). % 1.28/1.52 1368[0:MRR:804.3,1233.0] || -> equal(op1(e12,e12),e11)** equal(op1(e12,e11),e11) equal(op1(e12,e10),e11). % 1.28/1.52 1369[0:MRR:807.0,1192.0] || -> equal(op1(e13,e11),e13)** equal(op1(e11,e11),e13) equal(op1(e12,e11),e13). % 1.28/1.52 1370[0:MRR:808.0,1199.0] || -> equal(op1(e11,e13),e13)** equal(op1(e11,e11),e13) equal(op1(e11,e12),e13). % 1.28/1.52 1372[0:MRR:810.0,1196.0] || -> equal(op1(e11,e12),e12) equal(op1(e11,e11),e12) equal(op1(e11,e13),e12)**. % 1.28/1.52 1373[0:MRR:811.3,1231.0] || -> equal(op1(e11,e11),e11) equal(op1(e12,e11),e11)** equal(op1(e10,e11),e11). % 1.28/1.52 1377[0:Rew:879.0,819.3,33.0,819.0] || -> equal(e13,e11) equal(op1(e11,e10),e11) equal(op1(e12,e10),e11)** equal(e12,e11). % 1.28/1.52 1378[0:MRR:1377.0,1377.3,5.0,4.0] || -> equal(op1(e11,e10),e11) equal(op1(e12,e10),e11)**. % 1.28/1.52 1379[0:Rew:33.0,820.0] || -> equal(e13,e11) equal(op1(e10,e11),e11) equal(op1(e10,e12),e11) equal(op1(e10,e13),e11)**. % 1.28/1.52 1380[0:MRR:1379.0,1379.3,5.0,1235.0] || -> equal(op1(e10,e11),e11) equal(op1(e10,e12),e11)**. % 1.28/1.52 1385[0:MRR:824.1,824.2,1230.0,1188.0] || -> equal(op1(e13,e12),e13)** equal(op1(e13,e12),e10). % 1.28/1.52 1386[0:MRR:825.1,825.2,1231.0,1189.0] || -> equal(op1(e13,e11),e13)** equal(op1(e13,e11),e10). % 1.28/1.52 1388[0:MRR:830.2,830.3,1193.0,1198.0] || -> equal(op1(e12,e10),e10) equal(op1(e12,e10),e11)**. % 1.28/1.52 1390[0:MRR:834.2,834.3,1196.0,1199.0] || -> equal(op1(e11,e10),e11)** equal(op1(e11,e10),e10). % 1.28/1.52 1391[0:MRR:835.1,835.3,1235.0,1190.0] || -> equal(op1(e10,e13),e10) equal(op1(e10,e13),e12)**. % 1.28/1.52 1392[0:MRR:836.3,1191.0] || -> equal(op1(e10,e12),e12)** equal(op1(e10,e12),e10) equal(op1(e10,e12),e11). % 1.28/1.52 1393[0:MRR:837.3,1192.0] || -> equal(op1(e10,e11),e11) equal(op1(e10,e11),e10) equal(op1(e10,e11),e12)**. % 1.28/1.52 1394[0:Rew:1201.0,839.0] || -> equal(e23,e21) SkC66* SkC67 SkC68 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. % 1.28/1.52 1395[0:MRR:1394.0,1394.1,1394.2,1394.3,1394.4,1394.5,1394.6,1394.9,1394.11,1394.12,1394.13,1394.14,1394.15,1394.16,1394.17,1394.18,1394.20,1394.21,1394.22,1394.23,1394.24,1394.25,1394.26,1394.27,1394.28,1394.29,1394.30,1394.31,1394.32,1394.33,1394.34,1394.35,1394.36,1394.37,1394.38,1394.39,1394.41,1394.42,1394.43,1394.44,1394.47,1394.48,1394.49,1394.50,1394.51,1394.52,1394.53,1394.54,1394.55,1394.56,1394.57,1394.59,1394.60,1394.61,1394.62,1394.63,11.0,969.0,967.0,964.0,961.0,958.0,1088.0,953.0,1083.0,1157.0,1080.0,1078.0,1076.0,1074.0,945.0,1072.0,1214.0,940.0,1067.0,1065.0,1063.0,933.0,1061.0,1059.0,1156.0,1225.0,1055.0,1226.0,1052.0,925.0,1180.0,1049.0,1179.0,920.0,1045.0,1043.0,915.0,1040.0,1038.0,1036.0,1032.0,1030.0,905.0,903.0,900.0,897.0,894.0,1028.0,1215.0,1025.0,889.0,1022.0,1020.0,1018.0,1016.0,1014.0] || -> SkC123 SkC111 SkC110 SkC105 SkC84 SkC75 SkC73 SkC72*. % 1.28/1.52 1396[0:Rew:1227.0,840.0] || -> equal(e13,e11) SkC0* SkC1 SkC2 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. % 1.28/1.52 1397[0:MRR:1396.0,1396.1,1396.2,1396.3,1396.4,1396.5,1396.6,1396.9,1396.11,1396.12,1396.13,1396.14,1396.15,1396.16,1396.17,1396.18,1396.20,1396.21,1396.22,1396.23,1396.24,1396.25,1396.26,1396.27,1396.28,1396.29,1396.30,1396.31,1396.32,1396.33,1396.34,1396.35,1396.36,1396.37,1396.38,1396.39,1396.41,1396.42,1396.43,1396.44,1396.47,1396.48,1396.49,1396.50,1396.51,1396.52,1396.53,1396.54,1396.55,1396.56,1396.57,1396.59,1396.60,1396.61,1396.62,1396.63,5.0,1005.0,1003.0,1001.0,999.0,997.0,1152.0,995.0,1147.0,1187.0,1144.0,1142.0,1140.0,1138.0,993.0,1136.0,1236.0,991.0,1133.0,1131.0,1129.0,989.0,1127.0,1125.0,1186.0,1239.0,1123.0,1238.0,1121.0,987.0,1195.0,1119.0,1194.0,985.0,1116.0,1114.0,983.0,1112.0,1110.0,1108.0,1106.0,1104.0,981.0,979.0,977.0,975.0,973.0,1102.0,1237.0,1100.0,971.0,1098.0,1096.0,1094.0,1092.0,1090.0] || -> SkC57 SkC45 SkC44 SkC39 SkC18 SkC9 SkC7 SkC6*. % 1.28/1.52 1431[0:Rew:1201.0,855.16,859.0,855.16,1252.0,855.16,1227.0,855.16,859.0,855.15,1009.0,855.15,859.0,855.14,1252.0,855.14,878.0,855.13,859.0,855.13,29.0,855.13,1009.0,855.13,879.0,855.13,1009.0,855.12,859.0,855.12,85.0,855.11,1009.0,855.11,1009.0,855.10,1252.0,855.10,1009.0,855.9,29.0,855.9,1206.0,855.8,1252.0,855.8,859.0,855.8,1252.0,855.7,1009.0,855.7,84.0,855.6,1252.0,855.6,1252.0,855.5,29.0,855.5,29.0,855.4,859.0,855.4,29.0,855.3,1009.0,855.3,29.0,855.2,1252.0,855.2,34.0,855.1,29.0,855.1,859.0,855.1,33.0,855.1,859.0,855.0] || equal(e23,e23) equal(e23,e23) equal(h1(op1(e10,e11)),op2(e20,e21)) 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(e13)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e13)),h4(e12)) equal(h1(op1(e12,e10)),op2(e22,e20)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e12,e12)),h3(e13)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(e22,e22) equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(e21,e21) SkC132 SkC133 SkC134 -> . % 1.28/1.52 1432[0:Obv:1431.16] || equal(h1(op1(e10,e11)),op2(e20,e21)) 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(e13)) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(h1(op1(e11,e13)),h4(e12)) equal(h1(op1(e12,e10)),op2(e22,e20)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e12,e12)),h3(e13)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e13,e12)),op2(e23,e22))** SkC132 SkC133 SkC134 -> . % 1.28/1.52 1433[0:MRR:1432.13,1432.14,1432.15,877.0,1254.0,1012.0] || equal(h1(op1(e12,e12)),h3(e13)) equal(h1(op1(e11,e11)),h2(e13)) equal(h1(op1(e11,e13)),h4(e12)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e12,e10)),op2(e22,e20)) 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)) equal(h1(op1(e10,e11)),op2(e20,e21)) -> . % 1.28/1.52 1440[1:Spt:1348.0] || -> equal(h2(e13),e23)**. % 1.28/1.52 1445[1:Rew:1440.0,951.1] || SkC75* -> equal(e23,e22). % 1.28/1.52 1446[1:Rew:1440.0,887.1] || SkC123* -> equal(e23,e22). % 1.28/1.52 1461[1:Rew:1440.0,1326.0] || -> equal(e23,e21) equal(op2(e22,e21),e21)** equal(op2(e20,e21),e21). % 1.28/1.52 1464[1:Rew:1440.0,1220.0] || equal(h4(e12),e23)** -> . % 1.28/1.52 1465[1:Rew:1440.0,1008.0] || -> equal(op2(e23,e21),h2(e12))**. % 1.28/1.52 1466[1:Rew:1440.0,1164.0] || equal(op2(e21,e22),e23)** -> . % 1.28/1.52 1468[1:Rew:1440.0,1175.0] || equal(op2(e23,e21),e23)** -> . % 1.28/1.52 1473[1:MRR:1445.1,12.0] || SkC75* -> . % 1.28/1.52 1474[1:MRR:1395.5,1473.0] || -> SkC123 SkC111 SkC110 SkC105 SkC84 SkC73 SkC72*. % 1.28/1.52 1475[1:MRR:1446.1,12.0] || SkC123* -> . % 1.28/1.52 1476[1:MRR:1294.0,1464.0] || -> equal(op2(e22,e23),e23)**. % 1.28/1.52 1479[1:Rew:1476.0,1298.1] || -> equal(h4(e12),e22) equal(e23,e22) equal(op2(e20,e23),e22)**. % 1.28/1.52 1481[1:Rew:1476.0,295.1] || SkC110* -> equal(e23,e22). % 1.28/1.52 1482[1:Rew:1476.0,297.1] || SkC111* -> equal(e23,e22). % 1.28/1.52 1486[1:Rew:1476.0,1160.0] || equal(h3(e13),e23)** -> . % 1.28/1.52 1492[1:MRR:1481.1,12.0] || SkC110* -> . % 1.28/1.52 1493[1:MRR:1482.1,12.0] || SkC111* -> . % 1.28/1.52 1495[1:MRR:1344.0,1486.0] || -> equal(h3(e13),e22)** equal(h3(e13),e21) equal(h3(e13),e20). % 1.28/1.52 1496[1:Rew:1465.0,1342.0] || -> equal(h2(e12),e23) equal(op2(e23,e21),e20)**. % 1.28/1.52 1500[1:Rew:1465.0,1268.2] || -> SkC131 SkC129 equal(h2(e12),e23)**. % 1.28/1.52 1507[1:Rew:1465.0,391.0] || equal(op2(e20,e21),h2(e12))** -> . % 1.28/1.52 1508[1:MRR:784.2,1466.0] || -> equal(op2(e21,e22),e22)** equal(op2(e21,e22),e21) equal(op2(e21,e22),e20). % 1.28/1.52 1509[1:Rew:1465.0,1468.0] || equal(h2(e12),e23)** -> . % 1.28/1.52 1514[1:MRR:1500.2,1509.0] || -> SkC131 SkC129*. % 1.28/1.52 1518[1:MRR:1474.0,1474.1,1474.2,1475.0,1493.0,1492.0] || -> SkC105 SkC84 SkC73 SkC72*. % 1.28/1.52 1519[1:Rew:1465.0,1496.1] || -> equal(h2(e12),e23)** equal(h2(e12),e20). % 1.28/1.52 1520[1:MRR:1519.0,1509.0] || -> equal(h2(e12),e20)**. % 1.28/1.52 1528[1:Rew:1520.0,1507.0] || equal(op2(e20,e21),e20)** -> . % 1.28/1.52 1538[1:MRR:223.1,1528.0] || SkC73* -> . % 1.28/1.52 1539[1:MRR:221.1,1528.0] || SkC72* -> . % 1.28/1.52 1541[1:MRR:1352.1,1528.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e21),e22)**. % 1.28/1.52 1542[1:MRR:1518.2,1538.0] || -> SkC105 SkC84 SkC72*. % 1.28/1.52 1543[1:MRR:1542.2,1539.0] || -> SkC105 SkC84*. % 1.28/1.52 1546[1:MRR:1479.1,12.0] || -> equal(h4(e12),e22) equal(op2(e20,e23),e22)**. % 1.28/1.52 1550[1:MRR:1461.0,11.0] || -> equal(op2(e22,e21),e21)** equal(op2(e20,e21),e21). % 1.28/1.52 1562[2:Spt:828.0] || -> equal(op1(e12,e12),e12)**. % 1.28/1.52 1563[2:Rew:1562.0,1364.1] || -> equal(op1(e12,e13),e13)** equal(e13,e12) equal(op1(e12,e11),e13). % 1.28/1.52 1564[2:Rew:1562.0,1363.1] || -> equal(op1(e13,e12),e13)** equal(e13,e12) equal(op1(e11,e12),e13). % 1.28/1.52 1569[2:Rew:1562.0,1367.0] || -> equal(e12,e11) equal(op1(e11,e12),e11)** equal(op1(e10,e12),e11). % 1.28/1.52 1572[2:Rew:1562.0,99.1] || SkC6* -> equal(e12,e11). % 1.28/1.52 1573[2:Rew:1562.0,805.0] || -> equal(e12,e10) equal(op1(e10,e12),e10) equal(op1(e13,e12),e10)** equal(op1(e11,e12),e10). % 1.28/1.52 1576[2:Rew:1562.0,123.1] || SkC18* -> equal(e12,e10). % 1.28/1.52 1579[2:Rew:1562.0,376.0] || equal(op1(e12,e13),e12)** -> . % 1.28/1.52 1580[2:Rew:1562.0,374.0] || equal(op1(e12,e11),e12)** -> . % 1.28/1.52 1583[2:Rew:1562.0,350.0] || equal(op1(e11,e12),e12)** -> . % 1.28/1.52 1584[2:Rew:1562.0,348.0] || equal(op1(e10,e12),e12)** -> . % 1.28/1.52 1589[2:MRR:1572.1,4.0] || SkC6* -> . % 1.28/1.52 1590[2:MRR:1397.7,1589.0] || -> SkC57 SkC45 SkC44 SkC39 SkC18 SkC9 SkC7*. % 1.28/1.52 1591[2:MRR:1576.1,2.0] || SkC18* -> . % 1.28/1.52 1592[2:MRR:174.1,1579.0] || SkC45* -> . % 1.28/1.52 1593[2:MRR:172.1,1579.0] || SkC44* -> . % 1.28/1.52 1594[2:MRR:1358.0,1579.0] || -> equal(op1(e11,e13),e12)** equal(op1(e10,e13),e12). % 1.28/1.52 1596[2:MRR:163.1,1580.0] || SkC39* -> . % 1.28/1.52 1599[2:MRR:1372.0,1583.0] || -> equal(op1(e11,e11),e12) equal(op1(e11,e13),e12)**. % 1.28/1.52 1600[2:MRR:832.0,1583.0] || -> equal(op1(e11,e12),e11) equal(op1(e11,e12),e13)** equal(op1(e11,e12),e10). % 1.28/1.52 1602[2:MRR:1392.0,1584.0] || -> equal(op1(e10,e12),e10) equal(op1(e10,e12),e11)**. % 1.28/1.52 1603[2:MRR:1590.1,1590.2,1590.3,1590.4,1592.0,1593.0,1596.0,1591.0] || -> SkC57 SkC9 SkC7*. % 1.28/1.52 1604[2:MRR:1563.1,6.0] || -> equal(op1(e12,e13),e13)** equal(op1(e12,e11),e13). % 1.28/1.52 1605[2:MRR:1564.1,6.0] || -> equal(op1(e13,e12),e13)** equal(op1(e11,e12),e13). % 1.28/1.52 1607[2:MRR:1569.0,4.0] || -> equal(op1(e11,e12),e11)** equal(op1(e10,e12),e11). % 1.28/1.52 1608[2:MRR:1573.0,2.0] || -> equal(op1(e10,e12),e10) equal(op1(e13,e12),e10)** equal(op1(e11,e12),e10). % 1.28/1.52 1613[3:Spt:833.0] || -> equal(op1(e11,e11),e11)**. % 1.28/1.52 1620[3:Rew:1613.0,105.1] || SkC9* -> equal(e12,e11). % 1.28/1.52 1621[3:Rew:1613.0,199.1] || SkC57* -> equal(e12,e11). % 1.28/1.52 1626[3:Rew:1613.0,368.0] || equal(op1(e11,e12),e11)** -> . % 1.28/1.52 1627[3:Rew:1613.0,365.0] || equal(op1(e11,e10),e11)** -> . % 1.28/1.52 1636[3:MRR:1620.1,4.0] || SkC9* -> . % 1.28/1.52 1637[3:MRR:1603.1,1636.0] || -> SkC57 SkC7*. % 1.28/1.52 1638[3:MRR:1621.1,4.0] || SkC57* -> . % 1.28/1.52 1639[3:MRR:1637.0,1638.0] || -> SkC7*. % 1.28/1.52 1641[3:MRR:445.0,1639.0] || equal(op1(e13,e11),e13)** -> . % 1.28/1.52 1650[3:MRR:1607.0,1626.0] || -> equal(op1(e10,e12),e11)**. % 1.28/1.52 1652[3:Rew:1650.0,1608.0] || -> equal(e11,e10) equal(op1(e13,e12),e10)** equal(op1(e11,e12),e10). % 1.28/1.52 1660[3:MRR:1390.0,1627.0] || -> equal(op1(e11,e10),e10)**. % 1.28/1.52 1672[3:Rew:1660.0,366.0] || equal(op1(e11,e12),e10)** -> . % 1.28/1.52 1679[3:MRR:1356.1,1641.0] || -> equal(op1(e13,e12),e13)**. % 1.28/1.52 1737[3:Rew:1679.0,1652.1] || -> equal(e11,e10) equal(e13,e10) equal(op1(e11,e12),e10)**. % 1.28/1.52 1738[3:MRR:1737.0,1737.1,1737.2,1.0,3.0,1672.0] || -> . % 1.28/1.52 1745[3:Spt:1738.0,833.0,1613.0] || equal(op1(e11,e11),e11)** -> . % 1.28/1.52 1746[3:Spt:1738.0,833.1,833.2,833.3] || -> equal(op1(e11,e11),e13)** equal(op1(e11,e11),e12) equal(op1(e11,e11),e10). % 1.28/1.52 1747[3:MRR:1373.0,1745.0] || -> equal(op1(e12,e11),e11)** equal(op1(e10,e11),e11). % 1.28/1.52 1749[4:Spt:1746.0] || -> equal(op1(e11,e11),e13)**. % 1.28/1.52 1754[4:Rew:1749.0,105.1] || SkC9* -> equal(e13,e12). % 1.28/1.52 1755[4:Rew:1749.0,199.1] || SkC57* -> equal(e13,e12). % 1.28/1.52 1757[4:Rew:1749.0,344.0] || equal(op1(e12,e11),e13)** -> . % 1.28/1.52 1760[4:Rew:1749.0,368.0] || equal(op1(e11,e12),e13)** -> . % 1.28/1.52 1771[4:MRR:1754.1,6.0] || SkC9* -> . % 1.28/1.52 1772[4:MRR:1603.1,1771.0] || -> SkC57 SkC7*. % 1.28/1.52 1773[4:MRR:1755.1,6.0] || SkC57* -> . % 1.28/1.52 1774[4:MRR:1772.0,1773.0] || -> SkC7*. % 1.28/1.52 1775[4:MRR:100.0,1774.0] || -> equal(op1(e10,e11),e10)**. % 1.28/1.52 1780[4:Rew:1775.0,362.0] || equal(op1(e10,e12),e10)** -> . % 1.28/1.52 1781[4:Rew:1775.0,363.0] || equal(op1(e10,e13),e10)** -> . % 1.28/1.52 1787[4:MRR:1604.1,1757.0] || -> equal(op1(e12,e13),e13)**. % 1.28/1.52 1796[4:Rew:1787.0,1360.1] || -> equal(op1(e10,e13),e10) equal(e13,e10) equal(op1(e11,e13),e10)**. % 1.28/1.52 1813[4:MRR:1600.1,1760.0] || -> equal(op1(e11,e12),e11)** equal(op1(e11,e12),e10). % 1.28/1.52 1818[4:MRR:1602.0,1780.0] || -> equal(op1(e10,e12),e11)**. % 1.28/1.52 1821[4:Rew:1818.0,347.0] || equal(op1(e11,e12),e11)** -> . % 1.28/1.52 1826[4:MRR:1391.0,1781.0] || -> equal(op1(e10,e13),e12)**. % 1.28/1.52 1861[4:MRR:1813.0,1821.0] || -> equal(op1(e11,e12),e10)**. % 1.28/1.52 1863[4:Rew:1861.0,370.0] || equal(op1(e11,e13),e10)** -> . % 1.28/1.52 1867[4:Rew:1826.0,1796.0] || -> equal(e12,e10) equal(e13,e10) equal(op1(e11,e13),e10)**. % 1.28/1.52 1868[4:MRR:1867.0,1867.1,1867.2,2.0,3.0,1863.0] || -> . % 1.28/1.52 1875[4:Spt:1868.0,1746.0,1749.0] || equal(op1(e11,e11),e13)** -> . % 1.28/1.52 1876[4:Spt:1868.0,1746.1,1746.2] || -> equal(op1(e11,e11),e12)** equal(op1(e11,e11),e10). % 1.28/1.52 1877[4:MRR:1369.1,1875.0] || -> equal(op1(e13,e11),e13)** equal(op1(e12,e11),e13). % 1.28/1.52 1879[5:Spt:1876.0] || -> equal(op1(e11,e11),e12)**. % 1.28/1.52 1883[5:Rew:1879.0,369.0] || equal(op1(e11,e13),e12)** -> . % 1.28/1.52 1888[5:Rew:1879.0,341.0] || equal(op1(e10,e11),e12)** -> . % 1.28/1.52 1897[5:MRR:1594.0,1883.0] || -> equal(op1(e10,e13),e12)**. % 1.28/1.52 1901[5:Rew:1897.0,1360.0] || -> equal(e12,e10) equal(op1(e12,e13),e10)** equal(op1(e11,e13),e10). % 1.28/1.52 1903[5:Rew:1897.0,1245.1] || SkC63* -> equal(e12,e10). % 1.28/1.52 1909[5:MRR:1903.1,2.0] || SkC63* -> . % 1.28/1.52 1910[5:MRR:1279.1,1909.0] || -> SkC65 equal(op1(e13,e11),e13)**. % 1.28/1.52 1913[5:MRR:1393.2,1888.0] || -> equal(op1(e10,e11),e11)** equal(op1(e10,e11),e10). % 1.28/1.52 1916[5:MRR:1901.0,2.0] || -> equal(op1(e12,e13),e10)** equal(op1(e11,e13),e10). % 1.28/1.52 1924[6:Spt:1380.0] || -> equal(op1(e10,e11),e11)**. % 1.28/1.52 1929[6:Rew:1924.0,362.0] || equal(op1(e10,e12),e11)** -> . % 1.28/1.52 1937[6:MRR:1602.1,1929.0] || -> equal(op1(e10,e12),e10)**. % 1.28/1.52 1938[6:MRR:1607.1,1929.0] || -> equal(op1(e11,e12),e11)**. % 1.28/1.52 1941[6:Rew:1937.0,349.0] || equal(op1(e13,e12),e10)** -> . % 1.28/1.52 1948[6:Rew:1938.0,366.0] || equal(op1(e11,e10),e11)** -> . % 1.28/1.52 1963[6:MRR:1362.0,1941.0] || -> equal(op1(e13,e11),e10)**. % 1.28/1.52 1967[6:Rew:1963.0,1910.1] || -> SkC65* equal(e13,e10). % 1.28/1.52 1968[6:Rew:1963.0,1877.0] || -> equal(e13,e10) equal(op1(e12,e11),e13)**. % 1.28/1.52 1973[6:MRR:1967.1,3.0] || -> SkC65*. % 1.28/1.52 1975[6:MRR:690.0,1973.0] || -> equal(op1(e12,op1(e12,e11)),e11)**. % 1.28/1.52 1986[6:MRR:1390.0,1948.0] || -> equal(op1(e11,e10),e10)**. % 1.28/1.52 1989[6:Rew:1986.0,367.0] || equal(op1(e11,e13),e10)** -> . % 1.28/1.52 1994[6:MRR:1916.1,1989.0] || -> equal(op1(e12,e13),e10)**. % 1.28/1.52 2007[6:MRR:1968.0,3.0] || -> equal(op1(e12,e11),e13)**. % 1.28/1.52 2011[6:Rew:2007.0,1975.0] || -> equal(op1(e12,e13),e11)**. % 1.28/1.52 2012[6:Rew:1994.0,2011.0] || -> equal(e11,e10)**. % 1.28/1.52 2013[6:MRR:2012.0,1.0] || -> . % 1.28/1.52 2016[6:Spt:2013.0,1380.0,1924.0] || equal(op1(e10,e11),e11)** -> . % 1.28/1.52 2017[6:Spt:2013.0,1380.1] || -> equal(op1(e10,e12),e11)**. % 1.28/1.52 2020[6:Rew:2017.0,104.1] || SkC9* -> equal(e11,e10). % 1.28/1.52 2021[6:MRR:2020.1,1.0] || SkC9* -> . % 1.28/1.52 2022[6:MRR:1603.1,2021.0] || -> SkC57 SkC7*. % 1.28/1.52 2033[6:MRR:1747.1,2016.0] || -> equal(op1(e12,e11),e11)**. % 1.28/1.52 2040[6:MRR:1913.0,2016.0] || -> equal(op1(e10,e11),e10)**. % 1.28/1.52 2044[6:Rew:2040.0,343.0] || equal(op1(e13,e11),e10)** -> . % 1.28/1.52 2057[6:MRR:1362.1,2044.0] || -> equal(op1(e13,e12),e10)**. % 1.28/1.52 2061[6:Rew:2057.0,198.1] || SkC57* -> equal(e13,e10). % 1.28/1.52 2064[6:MRR:2061.1,3.0] || SkC57* -> . % 1.28/1.52 2065[6:MRR:2022.0,2064.0] || -> SkC7*. % 1.28/1.52 2066[6:MRR:445.0,2065.0] || equal(op1(e13,e11),e13)** -> . % 1.28/1.52 2075[6:Rew:2033.0,1877.1] || -> equal(op1(e13,e11),e13)** equal(e13,e11). % 1.28/1.52 2076[6:MRR:2075.0,2075.1,2066.0,5.0] || -> . % 1.28/1.52 2090[5:Spt:2076.0,1876.0,1879.0] || equal(op1(e11,e11),e12)** -> . % 1.28/1.52 2091[5:Spt:2076.0,1876.1] || -> equal(op1(e11,e11),e10)**. % 1.28/1.52 2095[5:Rew:2091.0,199.1] || SkC57* -> equal(e12,e10). % 1.28/1.52 2096[5:MRR:2095.1,2.0] || SkC57* -> . % 1.28/1.52 2097[5:MRR:1603.0,2096.0] || -> SkC9 SkC7*. % 1.28/1.52 2098[5:Rew:2091.0,105.1] || SkC9* -> equal(e12,e10). % 1.28/1.52 2099[5:MRR:2098.1,2.0] || SkC9* -> . % 1.28/1.52 2100[5:MRR:2097.0,2099.0] || -> SkC7*. % 1.28/1.52 2101[5:MRR:100.0,2100.0] || -> equal(op1(e10,e11),e10)**. % 1.28/1.52 2105[5:Rew:2101.0,343.0] || equal(op1(e13,e11),e10)** -> . % 1.28/1.52 2117[5:Rew:2101.0,363.0] || equal(op1(e10,e13),e10)** -> . % 1.28/1.52 2151[5:MRR:1362.1,2105.0] || -> equal(op1(e13,e12),e10)**. % 1.28/1.52 2156[5:Rew:2151.0,1605.0] || -> equal(e13,e10) equal(op1(e11,e12),e13)**. % 1.28/1.52 2157[5:MRR:2156.0,3.0] || -> equal(op1(e11,e12),e13)**. % 1.28/1.52 2159[5:Rew:2157.0,370.0] || equal(op1(e11,e13),e13)** -> . % 1.28/1.52 2167[5:MRR:1354.1,2159.0] || -> equal(op1(e12,e13),e13)**. % 1.28/1.52 2177[5:Rew:2091.0,1599.0] || -> equal(e12,e10) equal(op1(e11,e13),e12)**. % 1.28/1.52 2178[5:MRR:2177.0,2.0] || -> equal(op1(e11,e13),e12)**. % 1.28/1.52 2187[5:Rew:2178.0,1360.2,2167.0,1360.1] || -> equal(op1(e10,e13),e10)** equal(e13,e10) equal(e12,e10). % 1.28/1.52 2188[5:MRR:2187.0,2187.1,2187.2,2117.0,3.0,2.0] || -> . % 1.28/1.52 2195[2:Spt:2188.0,828.0,1562.0] || equal(op1(e12,e12),e12)** -> . % 1.28/1.52 2196[2:Spt:2188.0,828.1,828.2,828.3] || -> equal(op1(e12,e12),e13)** equal(op1(e12,e12),e11) equal(op1(e12,e12),e10). % 1.28/1.52 2199[3:Spt:2196.0] || -> equal(op1(e12,e12),e13)**. % 1.28/1.52 2204[3:Rew:2199.0,123.1] || SkC18* -> equal(e13,e10). % 1.28/1.52 2209[3:Rew:2199.0,99.1] || SkC6* -> equal(e13,e11). % 1.28/1.52 2212[3:Rew:2199.0,352.0] || equal(op1(e13,e12),e13)** -> . % 1.28/1.52 2217[3:Rew:2199.0,516.1] || SkC44* equal(e13,e13) -> . % 1.28/1.52 2218[3:Rew:2199.0,518.1] || SkC45* equal(e13,e13) -> . % 1.28/1.52 2225[3:MRR:2204.1,3.0] || SkC18* -> . % 1.28/1.52 2226[3:MRR:1397.4,2225.0] || -> SkC57 SkC45 SkC44 SkC39 SkC9 SkC7 SkC6*. % 1.28/1.52 2227[3:MRR:2209.1,5.0] || SkC6* -> . % 1.28/1.52 2230[3:MRR:198.1,2212.0] || SkC57* -> . % 1.28/1.52 2231[3:MRR:1385.0,2212.0] || -> equal(op1(e13,e12),e10)**. % 1.28/1.52 2232[3:MRR:1356.0,2212.0] || -> equal(op1(e13,e11),e13)**. % 1.28/1.52 2235[3:Rew:2231.0,349.0] || equal(op1(e10,e12),e10)** -> . % 1.28/1.52 2241[3:Rew:2232.0,508.1] || SkC39* equal(e13,e13) -> . % 1.28/1.52 2242[3:Rew:2232.0,445.1] || SkC7* equal(e13,e13) -> . % 1.28/1.52 2261[3:Obv:2217.1] || SkC44* -> . % 1.28/1.52 2262[3:Obv:2218.1] || SkC45* -> . % 1.28/1.52 2263[3:MRR:104.1,2235.0] || SkC9* -> . % 1.28/1.52 2267[3:Obv:2241.1] || SkC39* -> . % 1.28/1.52 2268[3:Obv:2242.1] || SkC7* -> . % 1.28/1.52 2271[3:MRR:2226.0,2226.1,2226.2,2226.3,2226.4,2226.5,2226.6,2230.0,2262.0,2261.0,2267.0,2263.0,2268.0,2227.0] || -> . % 1.28/1.52 2291[3:Spt:2271.0,2196.0,2199.0] || equal(op1(e12,e12),e13)** -> . % 1.28/1.52 2292[3:Spt:2271.0,2196.1,2196.2] || -> equal(op1(e12,e12),e11)** equal(op1(e12,e12),e10). % 1.28/1.52 2635[4:Spt:1312.0] || -> equal(h3(e13),e21)**. % 1.28/1.52 2636[4:Rew:2635.0,1041.1] || SkC105* equal(e21,e21) -> . % 1.28/1.52 2641[4:Rew:2635.0,942.1] || SkC84* -> equal(e21,e20). % 1.28/1.52 2657[4:MRR:2641.1,7.0] || SkC84* -> . % 1.28/1.52 2658[4:MRR:1543.1,2657.0] || -> SkC105*. % 1.28/1.52 2666[4:Obv:2636.1] || SkC105* -> . % 1.28/1.52 2667[4:MRR:2666.0,2658.0] || -> . % 1.28/1.52 2714[4:Spt:2667.0,1312.0,2635.0] || equal(h3(e13),e21)** -> . % 1.28/1.52 2715[4:Spt:2667.0,1312.1,1312.2] || -> equal(op2(e21,e22),e21)** equal(op2(e20,e22),e21). % 1.28/1.52 2716[4:MRR:1495.1,2714.0] || -> equal(h3(e13),e22)** equal(h3(e13),e20). % 1.28/1.52 2718[5:Spt:2715.0] || -> equal(op2(e21,e22),e21)**. % 1.28/1.52 2723[5:Rew:2718.0,414.0] || equal(op2(e21,e20),e21)** -> . % 1.28/1.52 2738[5:MRR:245.1,2723.0] || SkC84* -> . % 1.28/1.52 2739[5:MRR:1334.0,2723.0] || -> equal(op2(e22,e20),e21)**. % 1.28/1.52 2741[5:MRR:1543.1,2738.0] || -> SkC105*. % 1.28/1.52 2742[5:MRR:286.0,2741.0] || -> equal(op2(e22,e21),e22)**. % 1.28/1.52 2757[5:Rew:2742.0,1161.0] || equal(h3(e13),e22)** -> . % 1.28/1.52 2767[5:MRR:2716.0,2757.0] || -> equal(h3(e13),e20)**. % 1.28/1.52 2771[5:Rew:2767.0,1273.1] || SkC129* equal(e20,e20) -> . % 1.28/1.52 2778[5:Rew:2767.0,1240.1] || SkC131 -> equal(op2(e22,e20),e22)**. % 1.28/1.52 2790[5:Obv:2771.1] || SkC129* -> . % 1.28/1.52 2791[5:MRR:1514.1,2790.0] || -> SkC131*. % 1.28/1.52 2802[5:Rew:2739.0,2778.1] || SkC131* -> equal(e22,e21). % 1.28/1.52 2803[5:MRR:2802.0,2802.1,2791.0,10.0] || -> . % 1.28/1.52 2814[5:Spt:2803.0,2715.0,2718.0] || equal(op2(e21,e22),e21)** -> . % 1.28/1.52 2815[5:Spt:2803.0,2715.1] || -> equal(op2(e20,e22),e21)**. % 1.28/1.52 2819[5:Rew:2815.0,410.0] || equal(op2(e20,e21),e21)** -> . % 1.28/1.52 2829[5:MRR:1550.1,2819.0] || -> equal(op2(e22,e21),e21)**. % 1.28/1.52 2833[5:Rew:2829.0,286.1] || SkC105* -> equal(e22,e21). % 1.28/1.52 2838[5:MRR:2833.1,10.0] || SkC105* -> . % 1.28/1.52 2839[5:MRR:1543.0,2838.0] || -> SkC84*. % 1.28/1.52 2840[5:MRR:942.0,2839.0] || -> equal(h3(e13),e20)**. % 1.28/1.52 2846[5:Rew:2840.0,1173.0] || equal(op2(e21,e22),e20)** -> . % 1.28/1.52 2863[5:MRR:1541.0,2819.0] || -> equal(op2(e20,e21),e22)**. % 1.28/1.52 2866[5:Rew:2863.0,411.0] || equal(op2(e20,e23),e22)** -> . % 1.28/1.52 2868[5:MRR:1546.1,2866.0] || -> equal(h4(e12),e22)**. % 1.28/1.52 2875[5:Rew:2868.0,1219.0] || equal(op2(e21,e22),e22)** -> . % 1.28/1.52 2889[5:MRR:1508.0,1508.1,1508.2,2875.0,2814.0,2846.0] || -> . % 1.28/1.52 2894[1:Spt:2889.0,1348.0,1440.0] || equal(h2(e13),e23)** -> . % 1.28/1.52 2895[1:Spt:2889.0,1348.1,1348.2,1348.3] || -> equal(h2(e13),e22)** equal(h2(e13),e21) equal(h2(e13),e20). % 1.28/1.52 2896[1:MRR:908.1,2894.0] || SkC111* -> . % 1.28/1.52 2897[1:MRR:1395.1,2896.0] || -> SkC123 SkC110 SkC105 SkC84 SkC75 SkC73 SkC72*. % 1.28/1.52 2898[1:MRR:1320.1,2894.0] || -> equal(h4(e12),e23) equal(op2(e21,e22),e23)**. % 1.28/1.52 2899[1:MRR:1318.0,2894.0] || -> equal(op2(e23,e21),e23)** equal(op2(e22,e21),e23). % 1.28/1.52 2900[2:Spt:2895.0] || -> equal(h2(e13),e22)**. % 1.28/1.52 2903[2:Rew:2900.0,1220.0] || equal(h4(e12),e22)** -> . % 1.28/1.52 2905[2:Rew:2900.0,1329.0] || -> equal(e22,e20) equal(op2(e20,e21),e20) equal(op2(e23,e21),e20)** equal(op2(e22,e21),e20). % 1.28/1.52 2914[2:Rew:2900.0,1177.0] || equal(op2(e20,e21),e22)** -> . % 1.28/1.52 2915[2:Rew:2900.0,1176.0] || equal(op2(e22,e21),e22)** -> . % 1.28/1.52 2918[2:Rew:2900.0,1164.0] || equal(op2(e21,e22),e22)** -> . % 1.28/1.52 2919[2:Rew:2900.0,1008.0] || -> equal(op2(e22,e21),h2(e12))**. % 1.28/1.52 2920[2:Rew:2900.0,1251.0] || -> equal(op2(e22,e22),h2(e11))**. % 1.28/1.52 2926[2:Rew:2900.0,1326.0] || -> equal(e22,e21) equal(op2(e22,e21),e21)** equal(op2(e20,e21),e21). % 1.28/1.52 2927[2:Rew:2900.0,1433.1] || equal(h1(op1(e12,e12)),h3(e13)) equal(h1(op1(e11,e11)),e22) equal(h1(op1(e11,e13)),h4(e12)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),op2(e22,e21)) equal(h1(op1(e12,e10)),op2(e22,e20)) 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)) equal(h1(op1(e10,e11)),op2(e20,e21)) -> . % 1.28/1.52 2928[2:MRR:1347.1,2903.0] || -> equal(h4(e12),e23)** equal(h4(e12),e20). % 1.28/1.52 2932[2:MRR:1332.2,2914.0] || -> equal(op2(e20,e22),e22) equal(op2(e20,e23),e22)**. % 1.28/1.52 2933[2:MRR:1352.2,2914.0] || -> equal(op2(e20,e21),e21)** equal(op2(e20,e21),e20). % 1.28/1.52 2934[2:MRR:286.1,2915.0] || SkC105* -> . % 1.28/1.52 2936[2:MRR:1310.2,2915.0] || -> equal(h3(e13),e22) equal(op2(e22,e23),e22)**. % 1.28/1.52 2938[2:MRR:2897.2,2934.0] || -> SkC123 SkC110 SkC84 SkC75 SkC73 SkC72*. % 1.28/1.52 2939[2:MRR:1308.1,2918.0] || -> equal(h3(e13),e22) equal(op2(e20,e22),e22)**. % 1.28/1.52 2940[2:MRR:784.0,2918.0] || -> equal(op2(e21,e22),e21) equal(op2(e21,e22),e23)** equal(op2(e21,e22),e20). % 1.28/1.52 2942[2:Rew:2919.0,419.0] || equal(op2(e22,e20),h2(e12))** -> . % 1.28/1.52 2944[2:Rew:2919.0,423.0] || equal(op2(e22,e23),h2(e12))** -> . % 1.28/1.52 2945[2:Rew:2919.0,394.0] || equal(op2(e23,e21),h2(e12))** -> . % 1.28/1.52 2946[2:Rew:2919.0,702.1] || SkC131 -> equal(op2(e22,h2(e12)),e21)**. % 1.28/1.52 2947[2:Rew:2919.0,1314.1] || -> equal(h3(e13),e21) equal(h2(e12),e21) equal(op2(e22,e20),e21)**. % 1.28/1.52 2948[2:Rew:2919.0,1306.2] || -> equal(h3(e13),e23) equal(op2(e22,e23),e23)** equal(h2(e12),e23). % 1.28/1.52 2949[2:Rew:2919.0,2899.1] || -> equal(op2(e23,e21),e23)** equal(h2(e12),e23). % 1.28/1.52 2952[2:Rew:85.0,2920.0] || -> equal(h3(e13),h2(e11))**. % 1.28/1.52 2955[2:Rew:2952.0,1273.1] || SkC129 equal(h2(e11),e20)** -> . % 1.28/1.52 2957[2:Rew:2952.0,942.1] || SkC84 -> equal(h2(e11),e20)**. % 1.28/1.52 2960[2:Rew:2952.0,955.1] || SkC72 -> equal(h2(e11),e21)**. % 1.28/1.52 2962[2:Rew:2952.0,1174.0] || equal(op2(e20,e22),h2(e11))** -> . % 1.28/1.52 2964[2:Rew:2952.0,1162.0] || equal(op2(e22,e20),h2(e11))** -> . % 1.28/1.52 2970[2:Rew:2952.0,1034.1] || SkC110 equal(h2(e11),e23)** -> . % 1.28/1.52 2979[2:Rew:2952.0,2936.0] || -> equal(h2(e11),e22) equal(op2(e22,e23),e22)**. % 1.28/1.52 2980[2:Rew:2952.0,2939.0] || -> equal(h2(e11),e22) equal(op2(e20,e22),e22)**. % 1.28/1.52 2983[2:Rew:2919.0,2926.1] || -> equal(e22,e21) equal(h2(e12),e21) equal(op2(e20,e21),e21)**. % 1.28/1.52 2984[2:MRR:2983.0,10.0] || -> equal(h2(e12),e21) equal(op2(e20,e21),e21)**. % 1.28/1.52 2985[2:Rew:2952.0,2947.0] || -> equal(h2(e11),e21) equal(h2(e12),e21) equal(op2(e22,e20),e21)**. % 1.28/1.52 2986[2:Rew:2952.0,2948.0] || -> equal(h2(e11),e23) equal(op2(e22,e23),e23)** equal(h2(e12),e23). % 1.28/1.52 2991[2:Rew:2919.0,2905.3] || -> equal(e22,e20) equal(op2(e20,e21),e20) equal(op2(e23,e21),e20)** equal(h2(e12),e20). % 1.28/1.52 2992[2:MRR:2991.0,8.0] || -> equal(op2(e20,e21),e20) equal(op2(e23,e21),e20)** equal(h2(e12),e20). % 1.28/1.52 2994[2:Rew:2919.0,2927.6,2952.0,2927.0] || equal(h1(op1(e12,e12)),h2(e11)) equal(h1(op1(e11,e11)),e22) equal(h1(op1(e11,e13)),h4(e12)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),h2(e12)) equal(h1(op1(e12,e10)),op2(e22,e20)) 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)) equal(h1(op1(e10,e11)),op2(e20,e21)) -> . % 1.28/1.52 3005[3:Spt:828.0] || -> equal(op1(e12,e12),e12)**. % 1.28/1.52 3006[3:Rew:3005.0,1368.0] || -> equal(e12,e11) equal(op1(e12,e11),e11)** equal(op1(e12,e10),e11). % 1.28/1.52 3007[3:Rew:3005.0,1367.0] || -> equal(e12,e11) equal(op1(e11,e12),e11)** equal(op1(e10,e12),e11). % 1.28/1.52 3010[3:Rew:3005.0,99.1] || SkC6* -> equal(e12,e11). % 1.28/1.52 3012[3:Rew:3005.0,805.0] || -> equal(e12,e10) equal(op1(e10,e12),e10) equal(op1(e13,e12),e10)** equal(op1(e11,e12),e10). % 1.28/1.52 3014[3:Rew:3005.0,123.1] || SkC18* -> equal(e12,e10). % 1.28/1.52 3015[3:Rew:3005.0,348.0] || equal(op1(e10,e12),e12)** -> . % 1.28/1.52 3016[3:Rew:3005.0,350.0] || equal(op1(e11,e12),e12)** -> . % 1.28/1.52 3019[3:Rew:3005.0,374.0] || equal(op1(e12,e11),e12)** -> . % 1.28/1.52 3020[3:Rew:3005.0,376.0] || equal(op1(e12,e13),e12)** -> . % 1.28/1.52 3022[3:Rew:3005.0,1363.1] || -> equal(op1(e13,e12),e13)** equal(e13,e12) equal(op1(e11,e12),e13). % 1.28/1.52 3034[3:MRR:3010.1,4.0] || SkC6* -> . % 1.28/1.52 3035[3:MRR:1397.7,3034.0] || -> SkC57 SkC45 SkC44 SkC39 SkC18 SkC9 SkC7*. % 1.28/1.52 3036[3:MRR:3014.1,2.0] || SkC18* -> . % 1.28/1.52 3037[3:MRR:1392.0,3015.0] || -> equal(op1(e10,e12),e10) equal(op1(e10,e12),e11)**. % 1.28/1.52 3039[3:MRR:1372.0,3016.0] || -> equal(op1(e11,e11),e12) equal(op1(e11,e13),e12)**. % 1.28/1.52 3040[3:MRR:832.0,3016.0] || -> equal(op1(e11,e12),e11) equal(op1(e11,e12),e13)** equal(op1(e11,e12),e10). % 1.28/1.52 3041[3:MRR:163.1,3019.0] || SkC39* -> . % 1.28/1.52 3044[3:MRR:172.1,3020.0] || SkC44* -> . % 1.28/1.52 3045[3:MRR:174.1,3020.0] || SkC45* -> . % 1.28/1.52 3046[3:MRR:1358.0,3020.0] || -> equal(op1(e11,e13),e12)** equal(op1(e10,e13),e12). % 1.28/1.52 3048[3:MRR:3035.1,3035.2,3035.3,3035.4,3045.0,3044.0,3041.0,3036.0] || -> SkC57 SkC9 SkC7*. % 1.28/1.52 3049[3:MRR:3006.0,4.0] || -> equal(op1(e12,e11),e11)** equal(op1(e12,e10),e11). % 1.28/1.52 3050[3:MRR:3007.0,4.0] || -> equal(op1(e11,e12),e11)** equal(op1(e10,e12),e11). % 1.28/1.52 3052[3:MRR:3022.1,6.0] || -> equal(op1(e13,e12),e13)** equal(op1(e11,e12),e13). % 1.28/1.52 3054[3:MRR:3012.0,2.0] || -> equal(op1(e10,e12),e10) equal(op1(e13,e12),e10)** equal(op1(e11,e12),e10). % 1.28/1.52 3057[4:Spt:833.0] || -> equal(op1(e11,e11),e11)**. % 1.28/1.52 3061[4:Rew:3057.0,199.1] || SkC57* -> equal(e12,e11). % 1.28/1.52 3062[4:Rew:3057.0,105.1] || SkC9* -> equal(e12,e11). % 1.28/1.52 3068[4:Rew:3057.0,368.0] || equal(op1(e11,e12),e11)** -> . % 1.28/1.52 3073[4:Rew:3057.0,365.0] || equal(op1(e11,e10),e11)** -> . % 1.28/1.52 3083[4:MRR:3061.1,4.0] || SkC57* -> . % 1.28/1.52 3084[4:MRR:3048.0,3083.0] || -> SkC9 SkC7*. % 1.28/1.52 3085[4:MRR:3062.1,4.0] || SkC9* -> . % 1.28/1.52 3086[4:MRR:3084.0,3085.0] || -> SkC7*. % 1.28/1.52 3088[4:MRR:445.0,3086.0] || equal(op1(e13,e11),e13)** -> . % 1.28/1.52 3107[4:MRR:3050.0,3068.0] || -> equal(op1(e10,e12),e11)**. % 1.28/1.52 3110[4:Rew:3107.0,3054.0] || -> equal(e11,e10) equal(op1(e13,e12),e10)** equal(op1(e11,e12),e10). % 1.28/1.52 3116[4:MRR:1390.0,3073.0] || -> equal(op1(e11,e10),e10)**. % 1.28/1.52 3120[4:Rew:3116.0,366.0] || equal(op1(e11,e12),e10)** -> . % 1.28/1.52 3126[4:MRR:1356.1,3088.0] || -> equal(op1(e13,e12),e13)**. % 1.28/1.52 3184[4:Rew:3126.0,3110.1] || -> equal(e11,e10) equal(e13,e10) equal(op1(e11,e12),e10)**. % 1.28/1.52 3185[4:MRR:3184.0,3184.1,3184.2,1.0,3.0,3120.0] || -> . % 1.28/1.52 3195[4:Spt:3185.0,833.0,3057.0] || equal(op1(e11,e11),e11)** -> . % 1.28/1.52 3196[4:Spt:3185.0,833.1,833.2,833.3] || -> equal(op1(e11,e11),e13)** equal(op1(e11,e11),e12) equal(op1(e11,e11),e10). % 1.28/1.52 3197[4:MRR:1373.0,3195.0] || -> equal(op1(e12,e11),e11)** equal(op1(e10,e11),e11). % 1.28/1.52 3199[5:Spt:3196.0] || -> equal(op1(e11,e11),e13)**. % 1.28/1.52 3204[5:Rew:3199.0,199.1] || SkC57* -> equal(e13,e12). % 1.28/1.52 3205[5:Rew:3199.0,105.1] || SkC9* -> equal(e13,e12). % 1.28/1.52 3209[5:Rew:3199.0,368.0] || equal(op1(e11,e12),e13)** -> . % 1.28/1.52 3210[5:Rew:3199.0,369.0] || equal(op1(e11,e13),e13)** -> . % 1.28/1.52 3224[5:MRR:3204.1,6.0] || SkC57* -> . % 1.28/1.52 3225[5:MRR:3048.0,3224.0] || -> SkC9 SkC7*. % 1.28/1.52 3226[5:MRR:3205.1,6.0] || SkC9* -> . % 1.28/1.52 3227[5:MRR:3225.0,3226.0] || -> SkC7*. % 1.28/1.52 3228[5:MRR:100.0,3227.0] || -> equal(op1(e10,e11),e10)**. % 1.28/1.52 3231[5:Rew:3228.0,362.0] || equal(op1(e10,e12),e10)** -> . % 1.28/1.52 3233[5:Rew:3228.0,363.0] || equal(op1(e10,e13),e10)** -> . % 1.28/1.52 3255[5:MRR:3040.1,3209.0] || -> equal(op1(e11,e12),e11)** equal(op1(e11,e12),e10). % 1.28/1.52 3256[5:MRR:1354.1,3210.0] || -> equal(op1(e12,e13),e13)**. % 1.28/1.52 3265[5:Rew:3256.0,1360.1] || -> equal(op1(e10,e13),e10) equal(e13,e10) equal(op1(e11,e13),e10)**. % 1.28/1.52 3269[5:MRR:3037.0,3231.0] || -> equal(op1(e10,e12),e11)**. % 1.28/1.52 3272[5:Rew:3269.0,347.0] || equal(op1(e11,e12),e11)** -> . % 1.28/1.52 3277[5:MRR:1391.0,3233.0] || -> equal(op1(e10,e13),e12)**. % 1.28/1.52 3314[5:MRR:3255.0,3272.0] || -> equal(op1(e11,e12),e10)**. % 1.28/1.52 3316[5:Rew:3314.0,370.0] || equal(op1(e11,e13),e10)** -> . % 1.28/1.52 3320[5:Rew:3277.0,3265.0] || -> equal(e12,e10) equal(e13,e10) equal(op1(e11,e13),e10)**. % 1.28/1.52 3321[5:MRR:3320.0,3320.1,3320.2,2.0,3.0,3316.0] || -> . % 1.28/1.52 3333[5:Spt:3321.0,3196.0,3199.0] || equal(op1(e11,e11),e13)** -> . % 1.28/1.52 3334[5:Spt:3321.0,3196.1,3196.2] || -> equal(op1(e11,e11),e12)** equal(op1(e11,e11),e10). % 1.28/1.52 3336[5:MRR:1369.1,3333.0] || -> equal(op1(e13,e11),e13)** equal(op1(e12,e11),e13). % 1.28/1.52 3337[6:Spt:3334.0] || -> equal(op1(e11,e11),e12)**. % 1.28/1.52 3342[6:Rew:3337.0,369.0] || equal(op1(e11,e13),e12)** -> . % 1.28/1.52 3346[6:Rew:3337.0,341.0] || equal(op1(e10,e11),e12)** -> . % 1.28/1.52 3358[6:MRR:3046.0,3342.0] || -> equal(op1(e10,e13),e12)**. % 1.28/1.52 3362[6:Rew:3358.0,1360.0] || -> equal(e12,e10) equal(op1(e12,e13),e10)** equal(op1(e11,e13),e10). % 1.28/1.52 3364[6:Rew:3358.0,1245.1] || SkC63* -> equal(e12,e10). % 1.28/1.52 3370[6:MRR:3364.1,2.0] || SkC63* -> . % 1.28/1.52 3371[6:MRR:1279.1,3370.0] || -> SkC65 equal(op1(e13,e11),e13)**. % 1.28/1.52 3374[6:MRR:1393.2,3346.0] || -> equal(op1(e10,e11),e11)** equal(op1(e10,e11),e10). % 1.28/1.52 3377[6:MRR:3362.0,2.0] || -> equal(op1(e12,e13),e10)** equal(op1(e11,e13),e10). % 1.28/1.52 3390[7:Spt:1380.0] || -> equal(op1(e10,e11),e11)**. % 1.28/1.52 3396[7:Rew:3390.0,342.0] || equal(op1(e12,e11),e11)** -> . % 1.28/1.52 3397[7:Rew:3390.0,362.0] || equal(op1(e10,e12),e11)** -> . % 1.28/1.52 3408[7:MRR:3049.0,3396.0] || -> equal(op1(e12,e10),e11)**. % 1.28/1.52 3413[7:Rew:3408.0,338.0] || equal(op1(e11,e10),e11)** -> . % 1.28/1.52 3418[7:MRR:3037.1,3397.0] || -> equal(op1(e10,e12),e10)**. % 1.28/1.52 3422[7:Rew:3418.0,349.0] || equal(op1(e13,e12),e10)** -> . % 1.28/1.52 3434[7:MRR:1390.0,3413.0] || -> equal(op1(e11,e10),e10)**. % 1.28/1.52 3437[7:Rew:3434.0,367.0] || equal(op1(e11,e13),e10)** -> . % 1.28/1.52 3440[7:MRR:1362.0,3422.0] || -> equal(op1(e13,e11),e10)**. % 1.28/1.52 3444[7:Rew:3440.0,3371.1] || -> SkC65* equal(e13,e10). % 1.28/1.52 3445[7:Rew:3440.0,3336.0] || -> equal(e13,e10) equal(op1(e12,e11),e13)**. % 1.28/1.52 3450[7:MRR:3444.1,3.0] || -> SkC65*. % 1.28/1.52 3452[7:MRR:690.0,3450.0] || -> equal(op1(e12,op1(e12,e11)),e11)**. % 1.28/1.52 3465[7:MRR:3377.1,3437.0] || -> equal(op1(e12,e13),e10)**. % 1.28/1.52 3479[7:MRR:3445.0,3.0] || -> equal(op1(e12,e11),e13)**. % 1.28/1.52 3483[7:Rew:3479.0,3452.0] || -> equal(op1(e12,e13),e11)**. % 1.28/1.52 3484[7:Rew:3465.0,3483.0] || -> equal(e11,e10)**. % 1.28/1.52 3485[7:MRR:3484.0,1.0] || -> . % 1.28/1.52 3495[7:Spt:3485.0,1380.0,3390.0] || equal(op1(e10,e11),e11)** -> . % 1.28/1.52 3496[7:Spt:3485.0,1380.1] || -> equal(op1(e10,e12),e11)**. % 1.28/1.52 3499[7:Rew:3496.0,104.1] || SkC9* -> equal(e11,e10). % 1.28/1.52 3500[7:MRR:3499.1,1.0] || SkC9* -> . % 1.28/1.52 3501[7:MRR:3048.1,3500.0] || -> SkC57 SkC7*. % 1.28/1.52 3512[7:MRR:3197.1,3495.0] || -> equal(op1(e12,e11),e11)**. % 1.28/1.52 3519[7:MRR:3374.0,3495.0] || -> equal(op1(e10,e11),e10)**. % 1.28/1.52 3523[7:Rew:3519.0,343.0] || equal(op1(e13,e11),e10)** -> . % 1.28/1.52 3536[7:MRR:1362.1,3523.0] || -> equal(op1(e13,e12),e10)**. % 1.28/1.52 3540[7:Rew:3536.0,198.1] || SkC57* -> equal(e13,e10). % 1.28/1.52 3543[7:MRR:3540.1,3.0] || SkC57* -> . % 1.28/1.52 3544[7:MRR:3501.0,3543.0] || -> SkC7*. % 1.28/1.52 3545[7:MRR:445.0,3544.0] || equal(op1(e13,e11),e13)** -> . % 1.28/1.52 3554[7:Rew:3512.0,3336.1] || -> equal(op1(e13,e11),e13)** equal(e13,e11). % 1.28/1.52 3555[7:MRR:3554.0,3554.1,3545.0,5.0] || -> . % 1.28/1.52 3576[6:Spt:3555.0,3334.0,3337.0] || equal(op1(e11,e11),e12)** -> . % 1.28/1.52 3577[6:Spt:3555.0,3334.1] || -> equal(op1(e11,e11),e10)**. % 1.28/1.52 3581[6:Rew:3577.0,105.1] || SkC9* -> equal(e12,e10). % 1.28/1.52 3582[6:MRR:3581.1,2.0] || SkC9* -> . % 1.28/1.52 3583[6:MRR:3048.1,3582.0] || -> SkC57 SkC7*. % 1.28/1.52 3584[6:Rew:3577.0,199.1] || SkC57* -> equal(e12,e10). % 1.28/1.52 3585[6:MRR:3584.1,2.0] || SkC57* -> . % 1.28/1.52 3586[6:MRR:3583.0,3585.0] || -> SkC7*. % 1.28/1.52 3587[6:MRR:100.0,3586.0] || -> equal(op1(e10,e11),e10)**. % 1.28/1.52 3591[6:Rew:3587.0,343.0] || equal(op1(e13,e11),e10)** -> . % 1.28/1.52 3603[6:Rew:3587.0,363.0] || equal(op1(e10,e13),e10)** -> . % 1.28/1.52 3637[6:MRR:1362.1,3591.0] || -> equal(op1(e13,e12),e10)**. % 1.28/1.52 3642[6:Rew:3637.0,3052.0] || -> equal(e13,e10) equal(op1(e11,e12),e13)**. % 1.28/1.52 3643[6:MRR:3642.0,3.0] || -> equal(op1(e11,e12),e13)**. % 1.28/1.52 3645[6:Rew:3643.0,370.0] || equal(op1(e11,e13),e13)** -> . % 1.28/1.52 3653[6:MRR:1354.1,3645.0] || -> equal(op1(e12,e13),e13)**. % 1.28/1.52 3660[6:Rew:3577.0,3039.0] || -> equal(e12,e10) equal(op1(e11,e13),e12)**. % 1.28/1.52 3661[6:MRR:3660.0,2.0] || -> equal(op1(e11,e13),e12)**. % 1.28/1.52 3673[6:Rew:3661.0,1360.2,3653.0,1360.1] || -> equal(op1(e10,e13),e10)** equal(e13,e10) equal(e12,e10). % 1.28/1.52 3674[6:MRR:3673.0,3673.1,3673.2,3603.0,3.0,2.0] || -> . % 1.28/1.52 3684[3:Spt:3674.0,828.0,3005.0] || equal(op1(e12,e12),e12)** -> . % 1.28/1.52 3685[3:Spt:3674.0,828.1,828.2,828.3] || -> equal(op1(e12,e12),e13)** equal(op1(e12,e12),e11) equal(op1(e12,e12),e10). % 1.28/1.52 3686[3:MRR:1365.0,3684.0] || -> equal(op1(e11,e12),e12)** equal(op1(e10,e12),e12). % 1.28/1.52 3687[3:MRR:1366.0,3684.0] || -> equal(op1(e12,e13),e12)** equal(op1(e12,e11),e12). % 1.28/1.52 3688[4:Spt:3685.0] || -> equal(op1(e12,e12),e13)**. % 1.28/1.52 3693[4:Rew:3688.0,123.1] || SkC18* -> equal(e13,e10). % 1.28/1.52 3698[4:Rew:3688.0,99.1] || SkC6* -> equal(e13,e11). % 1.28/1.52 3700[4:Rew:3688.0,516.1] || SkC44* equal(e13,e13) -> . % 1.28/1.52 3701[4:Rew:3688.0,518.1] || SkC45* equal(e13,e13) -> . % 1.28/1.52 3705[4:Rew:3688.0,352.0] || equal(op1(e13,e12),e13)** -> . % 1.28/1.52 3716[4:MRR:3693.1,3.0] || SkC18* -> . % 1.28/1.52 3717[4:MRR:1397.4,3716.0] || -> SkC57 SkC45 SkC44 SkC39 SkC9 SkC7 SkC6*. % 1.28/1.52 3718[4:MRR:3698.1,5.0] || SkC6* -> . % 1.28/1.52 3719[4:Obv:3700.1] || SkC44* -> . % 1.28/1.52 3720[4:Obv:3701.1] || SkC45* -> . % 1.28/1.52 3736[4:MRR:198.1,3705.0] || SkC57* -> . % 1.28/1.52 3737[4:MRR:1385.0,3705.0] || -> equal(op1(e13,e12),e10)**. % 1.28/1.52 3738[4:MRR:1356.0,3705.0] || -> equal(op1(e13,e11),e13)**. % 1.28/1.52 3741[4:Rew:3737.0,349.0] || equal(op1(e10,e12),e10)** -> . % 1.28/1.52 3747[4:Rew:3738.0,508.1] || SkC39* equal(e13,e13) -> . % 1.28/1.52 3748[4:Rew:3738.0,445.1] || SkC7* equal(e13,e13) -> . % 1.28/1.52 3755[4:MRR:104.1,3741.0] || SkC9* -> . % 1.28/1.52 3759[4:Obv:3747.1] || SkC39* -> . % 1.28/1.52 3760[4:Obv:3748.1] || SkC7* -> . % 1.28/1.52 3762[4:MRR:3717.0,3717.1,3717.2,3717.3,3717.4,3717.5,3717.6,3736.0,3720.0,3719.0,3759.0,3755.0,3760.0,3718.0] || -> . % 1.28/1.52 3785[4:Spt:3762.0,3685.0,3688.0] || equal(op1(e12,e12),e13)** -> . % 1.28/1.52 3786[4:Spt:3762.0,3685.1,3685.2] || -> equal(op1(e12,e12),e11)** equal(op1(e12,e12),e10). % 1.28/1.52 3787[4:MRR:1363.1,3785.0] || -> equal(op1(e13,e12),e13)** equal(op1(e11,e12),e13). % 1.28/1.52 3788[4:MRR:1364.1,3785.0] || -> equal(op1(e12,e13),e13)** equal(op1(e12,e11),e13). % 1.28/1.52 3789[5:Spt:3786.0] || -> equal(op1(e12,e12),e11)**. % 1.28/1.52 3793[5:Rew:3789.0,507.1] || SkC39* equal(e11,e11) -> . % 1.28/1.52 3797[5:Rew:3789.0,123.1] || SkC18* -> equal(e11,e10). % 1.28/1.52 3798[5:Rew:3789.0,348.0] || equal(op1(e10,e12),e11)** -> . % 1.28/1.52 3799[5:Rew:3789.0,350.0] || equal(op1(e11,e12),e11)** -> . % 1.28/1.52 3801[5:Rew:3789.0,372.0] || equal(op1(e12,e10),e11)** -> . % 1.28/1.52 3804[5:Rew:3789.0,691.1] || SkC65 -> equal(op1(e12,e11),e12)**. % 1.28/1.52 3805[5:Rew:3789.0,2994.0] || equal(h2(e11),h1(e11)) equal(h1(op1(e11,e11)),e22) equal(h1(op1(e11,e13)),h4(e12)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),h2(e12)) equal(h1(op1(e12,e10)),op2(e22,e20)) 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)) equal(h1(op1(e10,e11)),op2(e20,e21)) -> . % 1.28/1.52 3812[5:MRR:3797.1,1.0] || SkC18* -> . % 1.28/1.52 3813[5:MRR:1397.4,3812.0] || -> SkC57 SkC45 SkC44 SkC39 SkC9 SkC7 SkC6*. % 1.28/1.52 3814[5:Obv:3793.1] || SkC39* -> . % 1.28/1.52 3815[5:MRR:1380.1,3798.0] || -> equal(op1(e10,e11),e11)**. % 1.28/1.52 3820[5:Rew:3815.0,100.1] || SkC7* -> equal(e11,e10). % 1.28/1.52 3821[5:Rew:3815.0,98.1] || SkC6* -> equal(e11,e10). % 1.28/1.52 3830[5:MRR:3820.1,1.0] || SkC7* -> . % 1.28/1.52 3831[5:MRR:3821.1,1.0] || SkC6* -> . % 1.28/1.52 3834[5:MRR:832.1,3799.0] || -> equal(op1(e11,e12),e12) equal(op1(e11,e12),e13)** equal(op1(e11,e12),e10). % 1.28/1.52 3835[5:MRR:1378.1,3801.0] || -> equal(op1(e11,e10),e11)**. % 1.28/1.52 3836[5:MRR:1388.1,3801.0] || -> equal(op1(e12,e10),e10)**. % 1.28/1.52 3858[5:MRR:3813.3,3813.5,3813.6,3814.0,3830.0,3831.0] || -> SkC57 SkC45 SkC44 SkC9*. % 1.28/1.52 3868[5:Rew:1252.0,3805.12,3815.0,3805.12,1252.0,3805.9,3835.0,3805.9,29.0,3805.7,3836.0,3805.7,1252.0,3805.0] || equal(h2(e11),e21) equal(h1(op1(e11,e11)),e22) equal(h1(op1(e11,e13)),h4(e12)) equal(h1(op1(e13,e12)),op2(e23,e22))** equal(h1(op1(e13,e11)),op2(e23,e21)) equal(h1(op1(e12,e13)),op2(e22,e23)) equal(h1(op1(e12,e11)),h2(e12)) equal(op2(e22,e20),e20) equal(h1(op1(e11,e12)),op2(e21,e22)) equal(op2(e21,e20),e21) equal(h1(op1(e10,e13)),op2(e20,e23)) equal(h1(op1(e10,e12)),op2(e20,e22)) equal(op2(e20,e21),e21) -> . % 1.28/1.52 3876[6:Spt:1369.1] || -> equal(op1(e11,e11),e13)**. % 1.28/1.52 3880[6:Rew:3876.0,105.1] || SkC9* -> equal(e13,e12). % 1.28/1.52 3881[6:Rew:3876.0,199.1] || SkC57* -> equal(e13,e12). % 1.28/1.52 3883[6:Rew:3876.0,344.0] || equal(op1(e12,e11),e13)** -> . % 1.28/1.52 3897[6:MRR:3880.1,6.0] || SkC9* -> . % 1.28/1.52 3898[6:MRR:3858.3,3897.0] || -> SkC57 SkC45 SkC44*. % 1.28/1.52 3899[6:MRR:3881.1,6.0] || SkC57* -> . % 1.28/1.52 3900[6:MRR:3898.0,3899.0] || -> SkC45 SkC44*. % 1.28/1.52 3913[6:MRR:3788.1,3883.0] || -> equal(op1(e12,e13),e13)**. % 1.28/1.52 3917[6:Rew:3913.0,174.1] || SkC45* -> equal(e13,e12). % 1.28/1.52 3918[6:Rew:3913.0,172.1] || SkC44* -> equal(e13,e12). % 1.28/1.52 3929[6:MRR:3917.1,6.0] || SkC45* -> . % 1.28/1.52 3930[6:MRR:3900.0,3929.0] || -> SkC44*. % 1.28/1.52 3932[6:MRR:3918.0,3918.1,3930.0,6.0] || -> . % 1.28/1.52 3976[6:Spt:3932.0,1369.1,3876.0] || equal(op1(e11,e11),e13)** -> . % 1.28/1.52 3977[6:Spt:3932.0,1369.0,1369.2] || -> equal(op1(e13,e11),e13)** equal(op1(e12,e11),e13). % 1.28/1.52 3978[6:MRR:175.1,3976.0] || SkC45* -> . % 1.28/1.52 3979[6:MRR:3858.1,3978.0] || -> SkC57 SkC44 SkC9*. % 1.28/1.52 3980[6:MRR:1370.1,3976.0] || -> equal(op1(e11,e13),e13)** equal(op1(e11,e12),e13). % 1.28/1.52 3982[7:Spt:3977.0] || -> equal(op1(e13,e11),e13)**. % 1.28/1.52 3986[7:Rew:3982.0,380.0] || equal(op1(e13,e12),e13)** -> . % 1.28/1.52 3987[7:Rew:3982.0,346.0] || equal(op1(e12,e11),e13)** -> . % 1.28/1.52 3996[7:MRR:198.1,3986.0] || SkC57* -> . % 1.28/1.52 3997[7:MRR:3787.0,3986.0] || -> equal(op1(e11,e12),e13)**. % 1.28/1.52 3999[7:MRR:3979.0,3996.0] || -> SkC44 SkC9*. % 1.28/1.52 4007[7:Rew:3997.0,3686.0] || -> equal(e13,e12) equal(op1(e10,e12),e12)**. % 1.28/1.52 4015[7:MRR:3788.1,3987.0] || -> equal(op1(e12,e13),e13)**. % 1.28/1.52 4024[7:Rew:4015.0,172.1] || SkC44* -> equal(e13,e12). % 1.28/1.52 4028[7:MRR:4024.1,6.0] || SkC44* -> . % 1.28/1.52 4029[7:MRR:3999.0,4028.0] || -> SkC9*. % 1.28/1.52 4031[7:MRR:104.0,4029.0] || -> equal(op1(e10,e12),e10)**. % 1.28/1.52 4069[7:Rew:4031.0,4007.1] || -> equal(e13,e12)** equal(e12,e10). % 1.28/1.52 4070[7:MRR:4069.0,4069.1,6.0,2.0] || -> . % 1.28/1.52 4082[7:Spt:4070.0,3977.0,3982.0] || equal(op1(e13,e11),e13)** -> . % 1.28/1.52 4083[7:Spt:4070.0,3977.1] || -> equal(op1(e12,e11),e13)**. % 1.28/1.52 4086[7:MRR:1278.1,4082.0] || SkC64* -> . % 1.28/1.52 4088[7:Rew:4083.0,3804.1] || SkC65* -> equal(e13,e12). % 1.28/1.52 4089[7:MRR:4088.1,6.0] || SkC65* -> . % 1.28/1.52 4091[7:MRR:1292.0,1292.1,4089.0,4086.0] || -> equal(op1(e10,e13),e10)**. % 1.28/1.52 4098[7:Rew:4091.0,517.1] || SkC44* equal(e10,e10) -> . % 1.28/1.52 4099[7:Obv:4098.1] || SkC44* -> . % 1.28/1.52 4100[7:MRR:3979.1,4099.0] || -> SkC57 SkC9*. % 1.28/1.52 4101[7:Rew:4091.0,364.0] || equal(op1(e10,e12),e10)** -> . % 1.28/1.52 4102[7:MRR:104.1,4101.0] || SkC9* -> . % 1.28/1.52 4103[7:MRR:4100.1,4102.0] || -> SkC57*. % 1.28/1.52 4104[7:MRR:198.0,4103.0] || -> equal(op1(e13,e12),e13)**. % 1.28/1.52 4105[7:MRR:199.0,4103.0] || -> equal(op1(e11,e11),e12)**. % 1.28/1.52 4109[7:Rew:4104.0,351.0] || equal(op1(e11,e12),e13)** -> . % 1.28/1.52 4114[7:Rew:4105.0,368.0] || equal(op1(e11,e12),e12)** -> . % 1.28/1.52 4118[7:MRR:1386.0,4082.0] || -> equal(op1(e13,e11),e10)**. % 1.28/1.52 4122[7:MRR:3980.1,4109.0] || -> equal(op1(e11,e13),e13)**. % 1.28/1.52 4128[7:MRR:3686.0,4114.0] || -> equal(op1(e10,e12),e12)**. % 1.28/1.52 4134[7:Rew:4083.0,3687.1] || -> equal(op1(e12,e13),e12)** equal(e13,e12). % 1.28/1.52 4135[7:MRR:4134.1,6.0] || -> equal(op1(e12,e13),e12)**. % 1.28/1.52 4139[7:MRR:3834.0,3834.1,4114.0,4109.0] || -> equal(op1(e11,e12),e10)**. % 1.28/1.52 4143[7:Rew:1009.0,3868.11,4128.0,3868.11,29.0,3868.10,4091.0,3868.10,29.0,3868.8,4139.0,3868.8,859.0,3868.6,4083.0,3868.6,1009.0,3868.5,4135.0,3868.5,29.0,3868.4,4118.0,3868.4,859.0,3868.3,4104.0,3868.3,859.0,3868.2,4122.0,3868.2,1009.0,3868.1,4105.0,3868.1] || equal(h2(e11),e21) equal(e22,e22) equal(h4(e12),e23) equal(op2(e23,e22),e23)** equal(op2(e23,e21),e20) equal(op2(e22,e23),e22) equal(h2(e12),e23) equal(op2(e22,e20),e20) equal(op2(e21,e22),e20) equal(op2(e21,e20),e21) equal(op2(e20,e23),e20) equal(op2(e20,e22),e22) equal(op2(e20,e21),e21) -> . % 1.28/1.52 4144[7:Obv:4143.1] || equal(h2(e11),e21) equal(h4(e12),e23) equal(op2(e23,e22),e23)** equal(op2(e23,e21),e20) equal(op2(e22,e23),e22) equal(h2(e12),e23) equal(op2(e22,e20),e20) equal(op2(e21,e22),e20) equal(op2(e21,e20),e21) equal(op2(e20,e23),e20) equal(op2(e20,e22),e22) equal(op2(e20,e21),e21) -> . % 1.28/1.52 4153[8:Spt:1294.1] || -> equal(op2(e22,e23),e23)**. % 1.28/1.52 4155[8:Rew:4153.0,1222.0] || equal(h4(e12),e23)** -> . % 1.28/1.52 4159[8:Rew:4153.0,295.1] || SkC110* -> equal(e23,e22). % 1.28/1.52 4165[8:Rew:4153.0,2944.0] || equal(h2(e12),e23)** -> . % 1.28/1.52 4167[8:MRR:2898.0,4155.0] || -> equal(op2(e21,e22),e23)**. % 1.28/1.52 4168[8:MRR:2928.0,4155.0] || -> equal(h4(e12),e20)**. % 1.28/1.52 4172[8:Rew:4168.0,1221.0] || equal(op2(e21,e20),e20)** -> . % 1.28/1.52 4173[8:Rew:4168.0,1223.0] || equal(op2(e20,e23),e20)** -> . % 1.28/1.52 4178[8:MRR:4159.1,12.0] || SkC110* -> . % 1.28/1.52 4179[8:MRR:2938.1,4178.0] || -> SkC123 SkC84 SkC75 SkC73 SkC72*. % 1.28/1.52 4180[8:MRR:2949.1,4165.0] || -> equal(op2(e23,e21),e23)**. % 1.28/1.52 4192[8:Rew:4167.0,399.0] || equal(op2(e23,e22),e23)** -> . % 1.28/1.52 4199[8:Rew:4180.0,568.1] || SkC73* equal(e23,e23) -> . % 1.28/1.52 4202[8:Rew:4180.0,2992.1] || -> equal(op2(e20,e21),e20)** equal(e23,e20) equal(h2(e12),e20). % 1.28/1.52 4210[8:MRR:1338.1,4172.0] || -> equal(op2(e22,e20),e20)**. % 1.28/1.52 4218[8:Rew:4210.0,2942.0] || equal(h2(e12),e20)** -> . % 1.28/1.52 4219[8:Rew:4210.0,2964.0] || equal(h2(e11),e20)** -> . % 1.28/1.52 4220[8:MRR:2957.1,4219.0] || SkC84* -> . % 1.28/1.52 4221[8:MRR:4179.1,4220.0] || -> SkC123 SkC75 SkC73 SkC72*. % 1.28/1.52 4223[8:MRR:1350.0,4173.0] || -> equal(op2(e20,e23),e22)**. % 1.28/1.52 4227[8:Rew:4223.0,412.0] || equal(op2(e20,e22),e22)** -> . % 1.28/1.52 4232[8:MRR:321.1,4192.0] || SkC123* -> . % 1.28/1.52 4234[8:MRR:4221.0,4232.0] || -> SkC75 SkC73 SkC72*. % 1.28/1.52 4240[8:Obv:4199.1] || SkC73* -> . % 1.28/1.52 4241[8:MRR:4234.1,4240.0] || -> SkC75 SkC72*. % 1.28/1.52 4247[8:MRR:2980.1,4227.0] || -> equal(h2(e11),e22)**. % 1.28/1.52 4252[8:Rew:4247.0,2960.1] || SkC72* -> equal(e22,e21). % 1.28/1.52 4260[8:MRR:4252.1,10.0] || SkC72* -> . % 1.28/1.52 4261[8:MRR:4241.1,4260.0] || -> SkC75*. % 1.28/1.52 4262[8:MRR:227.0,4261.0] || -> equal(op2(e20,e22),e20)**. % 1.28/1.52 4264[8:Rew:4262.0,410.0] || equal(op2(e20,e21),e20)** -> . % 1.28/1.52 4276[8:MRR:2933.1,4264.0] || -> equal(op2(e20,e21),e21)**. % 1.28/1.52 4286[8:Rew:4276.0,4202.0] || -> equal(e21,e20) equal(e23,e20) equal(h2(e12),e20)**. % 1.28/1.52 4287[8:MRR:4286.0,4286.1,4286.2,7.0,9.0,4218.0] || -> . % 1.28/1.52 4292[8:Spt:4287.0,1294.1,4153.0] || equal(op2(e22,e23),e23)** -> . % 1.28/1.52 4293[8:Spt:4287.0,1294.0] || -> equal(h4(e12),e23)**. % 1.28/1.52 4299[8:Rew:4293.0,1219.0] || equal(op2(e21,e22),e23)** -> . % 1.28/1.52 4303[8:MRR:2986.1,4292.0] || -> equal(h2(e11),e23) equal(h2(e12),e23)**. % 1.28/1.52 4304[8:Rew:4293.0,1300.0] || -> equal(e23,e20) equal(op2(e20,e23),e20) equal(op2(e22,e23),e20)**. % 1.28/1.52 4305[8:MRR:4304.0,9.0] || -> equal(op2(e20,e23),e20) equal(op2(e22,e23),e20)**. % 1.28/1.52 4310[8:MRR:2940.1,4299.0] || -> equal(op2(e21,e22),e21)** equal(op2(e21,e22),e20). % 1.28/1.52 4311[8:Rew:4293.0,4144.1] || equal(h2(e11),e21) equal(e23,e23) equal(op2(e23,e22),e23)** equal(op2(e23,e21),e20) equal(op2(e22,e23),e22) equal(h2(e12),e23) equal(op2(e22,e20),e20) equal(op2(e21,e22),e20) equal(op2(e21,e20),e21) equal(op2(e20,e23),e20) equal(op2(e20,e22),e22) equal(op2(e20,e21),e21) -> . % 1.28/1.52 4312[8:Obv:4311.1] || equal(h2(e11),e21) equal(op2(e23,e22),e23)** equal(op2(e23,e21),e20) equal(op2(e22,e23),e22) equal(h2(e12),e23) equal(op2(e22,e20),e20) equal(op2(e21,e22),e20) equal(op2(e21,e20),e21) equal(op2(e20,e23),e20) equal(op2(e20,e22),e22) equal(op2(e20,e21),e21) -> . % 1.28/1.52 4314[9:Spt:1342.0] || -> equal(op2(e23,e21),e23)**. % 1.28/1.52 4317[9:Rew:4314.0,568.1] || SkC73* equal(e23,e23) -> . % 1.28/1.52 4318[9:Rew:4314.0,2945.0] || equal(h2(e12),e23)** -> . % 1.28/1.52 4319[9:Rew:4314.0,428.0] || equal(op2(e23,e22),e23)** -> . % 1.28/1.52 4322[9:Rew:4314.0,2992.1] || -> equal(op2(e20,e21),e20)** equal(e23,e20) equal(h2(e12),e20). % 1.28/1.52 4325[9:MRR:4303.1,4318.0] || -> equal(h2(e11),e23)**. % 1.28/1.52 4330[9:Rew:4325.0,2957.1] || SkC84* -> equal(e23,e20). % 1.28/1.52 4337[9:Rew:4325.0,2960.1] || SkC72* -> equal(e23,e21). % 1.28/1.52 4343[9:Rew:4325.0,2970.1] || SkC110* equal(e23,e23) -> . % 1.28/1.52 4355[9:MRR:4330.1,9.0] || SkC84* -> . % 1.28/1.52 4356[9:MRR:2938.2,4355.0] || -> SkC123 SkC110 SkC75 SkC73 SkC72*. % 1.28/1.52 4357[9:MRR:4337.1,11.0] || SkC72* -> . % 1.28/1.52 4358[9:MRR:4356.4,4357.0] || -> SkC123 SkC110 SkC75 SkC73*. % 1.28/1.52 4359[9:Obv:4317.1] || SkC73* -> . % 1.28/1.52 4360[9:MRR:4358.3,4359.0] || -> SkC123 SkC110 SkC75*. % 1.28/1.52 4361[9:MRR:321.1,4319.0] || SkC123* -> . % 1.28/1.52 4363[9:MRR:4360.0,4361.0] || -> SkC110 SkC75*. % 1.28/1.52 4369[9:Obv:4343.1] || SkC110* -> . % 1.28/1.52 4370[9:MRR:4363.0,4369.0] || -> SkC75*. % 1.28/1.52 4371[9:MRR:227.0,4370.0] || -> equal(op2(e20,e22),e20)**. % 1.28/1.52 4375[9:Rew:4371.0,412.0] || equal(op2(e20,e23),e20)** -> . % 1.28/1.52 4376[9:Rew:4371.0,410.0] || equal(op2(e20,e21),e20)** -> . % 1.28/1.52 4409[9:MRR:4305.0,4375.0] || -> equal(op2(e22,e23),e20)**. % 1.28/1.52 4417[9:Rew:4409.0,2944.0] || equal(h2(e12),e20)** -> . % 1.28/1.52 4420[9:MRR:2933.1,4376.0] || -> equal(op2(e20,e21),e21)**. % 1.28/1.52 4443[9:Rew:4420.0,4322.0] || -> equal(e21,e20) equal(e23,e20) equal(h2(e12),e20)**. % 1.28/1.52 4444[9:MRR:4443.0,4443.1,4443.2,7.0,9.0,4417.0] || -> . % 1.28/1.52 4455[9:Spt:4444.0,1342.0,4314.0] || equal(op2(e23,e21),e23)** -> . % 1.28/1.52 4456[9:Spt:4444.0,1342.1] || -> equal(op2(e23,e21),e20)**. % 1.28/1.52 4460[9:Rew:4456.0,1267.1] || SkC130* -> equal(e23,e20). % 1.28/1.52 4461[9:MRR:4460.1,9.0] || SkC130* -> . % 1.28/1.52 4462[9:Rew:4456.0,1268.2] || -> SkC131 SkC129* equal(e23,e20). % 1.28/1.52 4463[9:MRR:4462.2,9.0] || -> SkC131 SkC129*. % 1.28/1.52 4465[9:MRR:1288.1,4461.0] || -> SkC131 equal(op2(e20,e23),e20)**. % 1.28/1.52 4466[9:Rew:4456.0,391.0] || equal(op2(e20,e21),e20)** -> . % 1.28/1.52 4467[9:MRR:221.1,4466.0] || SkC72* -> . % 1.28/1.52 4468[9:MRR:223.1,4466.0] || SkC73* -> . % 1.28/1.52 4469[9:MRR:2938.5,4467.0] || -> SkC123 SkC110 SkC84 SkC75 SkC73*. % 1.28/1.52 4470[9:MRR:4469.4,4468.0] || -> SkC123 SkC110 SkC84 SkC75*. % 1.28/1.52 4472[9:Rew:4456.0,2949.0] || -> equal(e23,e20) equal(h2(e12),e23)**. % 1.28/1.52 4473[9:MRR:4472.0,9.0] || -> equal(h2(e12),e23)**. % 1.28/1.52 4481[9:Rew:4473.0,2946.1] || SkC131 -> equal(op2(e22,e23),e21)**. % 1.28/1.52 4482[9:MRR:4481.1,1210.0] || SkC131* -> . % 1.28/1.52 4483[9:MRR:4463.0,4482.0] || -> SkC129*. % 1.28/1.52 4484[9:MRR:4465.0,4482.0] || -> equal(op2(e20,e23),e20)**. % 1.28/1.52 4485[9:MRR:2955.0,4483.0] || equal(h2(e11),e20)** -> . % 1.28/1.52 4489[9:Rew:4484.0,640.1] || SkC110* equal(e20,e20) -> . % 1.28/1.52 4490[9:Rew:4484.0,412.0] || equal(op2(e20,e22),e20)** -> . % 1.28/1.52 4493[9:MRR:2957.1,4485.0] || SkC84* -> . % 1.28/1.52 4494[9:MRR:4470.2,4493.0] || -> SkC123 SkC110 SkC75*. % 1.28/1.52 4495[9:Obv:4489.1] || SkC110* -> . % 1.28/1.52 4496[9:MRR:4494.1,4495.0] || -> SkC123 SkC75*. % 1.28/1.52 4497[9:MRR:227.1,4490.0] || SkC75* -> . % 1.28/1.52 4498[9:MRR:4496.1,4497.0] || -> SkC123*. % 1.28/1.52 4499[9:MRR:321.0,4498.0] || -> equal(op2(e23,e22),e23)**. % 1.28/1.52 4500[9:MRR:666.0,4498.0] || equal(op2(e21,e22),e21)** -> . % 1.28/1.52 4509[9:Rew:4473.0,2984.0] || -> equal(e23,e21) equal(op2(e20,e21),e21)**. % 1.28/1.52 4510[9:MRR:4509.0,11.0] || -> equal(op2(e20,e21),e21)**. % 1.28/1.52 4516[9:Rew:4484.0,2932.1] || -> equal(op2(e20,e22),e22)** equal(e22,e20). % 1.28/1.52 4517[9:MRR:4516.1,8.0] || -> equal(op2(e20,e22),e22)**. % 1.28/1.52 4519[9:Rew:4517.0,2962.0] || equal(h2(e11),e22)** -> . % 1.28/1.52 4524[9:MRR:2979.0,4519.0] || -> equal(op2(e22,e23),e22)**. % 1.28/1.52 4530[9:MRR:4310.0,4500.0] || -> equal(op2(e21,e22),e20)**. % 1.28/1.52 4534[9:Rew:4530.0,414.0] || equal(op2(e21,e20),e20)** -> . % 1.28/1.52 4536[9:MRR:1338.1,4534.0] || -> equal(op2(e22,e20),e20)**. % 1.28/1.52 4541[9:MRR:1349.1,4534.0] || -> equal(op2(e21,e20),e21)**. % 1.28/1.52 4545[9:Rew:4536.0,2985.2,4473.0,2985.1] || -> equal(h2(e11),e21)** equal(e23,e21) equal(e21,e20). % 1.28/1.52 4546[9:MRR:4545.1,4545.2,11.0,7.0] || -> equal(h2(e11),e21)**. % 1.28/1.52 4560[9:Rew:4510.0,4312.10,4517.0,4312.9,4484.0,4312.8,4541.0,4312.7,4530.0,4312.6,4536.0,4312.5,4473.0,4312.4,4524.0,4312.3,4456.0,4312.2,4499.0,4312.1,4546.0,4312.0] || equal(e21,e21) equal(e23,e23)* equal(e20,e20) equal(e22,e22) equal(e23,e23)* equal(e20,e20) equal(e20,e20) equal(e21,e21) equal(e20,e20) equal(e22,e22) equal(e21,e21) -> . % 1.28/1.52 4561[9:Obv:4560.10] || -> . % 1.28/1.52 4572[5:Spt:4561.0,3786.0,3789.0] || equal(op1(e12,e12),e11)** -> . % 1.28/1.52 4573[5:Spt:4561.0,3786.1] || -> equal(op1(e12,e12),e10)**. % 1.28/1.52 4577[5:Rew:4573.0,99.1] || SkC6* -> equal(e11,e10). % 1.28/1.52 4578[5:MRR:4577.1,1.0] || SkC6* -> . % 1.28/1.52 4582[5:Rew:4573.0,352.0] || equal(op1(e13,e12),e10)** -> . % 1.28/1.52 4583[5:MRR:1261.3,4582.0] || -> SkC65 SkC64 SkC63*. % 1.28/1.52 4585[5:Rew:4573.0,348.0] || equal(op1(e10,e12),e10)** -> . % 1.28/1.52 4586[5:MRR:104.1,4585.0] || SkC9* -> . % 1.28/1.52 4587[5:Rew:4573.0,1282.1] || SkC63* equal(e10,e10) -> . % 1.28/1.52 4588[5:Obv:4587.1] || SkC63* -> . % 1.28/1.52 4589[5:MRR:1279.1,4588.0] || -> SkC65 equal(op1(e13,e11),e13)**. % 1.28/1.52 4590[5:MRR:4583.2,4588.0] || -> SkC65 SkC64*. % 1.28/1.52 4592[5:MRR:1397.5,1397.7,4586.0,4578.0] || -> SkC57 SkC45 SkC44 SkC39 SkC18 SkC7*. % 1.28/1.52 4593[5:Rew:4573.0,691.1] || SkC65 -> equal(op1(e12,e10),e12)**. % 1.28/1.52 4594[5:MRR:4593.1,1193.0] || SkC65* -> . % 1.28/1.52 4595[5:MRR:4590.0,4594.0] || -> SkC64*. % 1.28/1.52 4596[5:MRR:4589.0,4594.0] || -> equal(op1(e13,e11),e13)**. % 1.28/1.52 4598[5:MRR:687.0,4595.0] || -> equal(op1(e11,op1(e11,e12)),e12)**. % 1.28/1.52 4602[5:Rew:4596.0,445.1] || SkC7* equal(e13,e13) -> . % 1.28/1.52 4603[5:Rew:4596.0,508.1] || SkC39* equal(e13,e13) -> . % 1.28/1.52 4604[5:Rew:4596.0,346.0] || equal(op1(e12,e11),e13)** -> . % 1.28/1.52 4605[5:Rew:4596.0,380.0] || equal(op1(e13,e12),e13)** -> . % 1.28/1.52 4606[5:Rew:4596.0,345.0] || equal(op1(e11,e11),e13)** -> . % 1.28/1.52 4608[5:Obv:4602.1] || SkC7* -> . % 1.28/1.52 4609[5:MRR:4592.5,4608.0] || -> SkC57 SkC45 SkC44 SkC39 SkC18*. % 1.28/1.52 4610[5:Obv:4603.1] || SkC39* -> . % 1.28/1.52 4611[5:MRR:4609.3,4610.0] || -> SkC57 SkC45 SkC44 SkC18*. % 1.28/1.52 4612[5:MRR:198.1,4605.0] || SkC57* -> . % 1.28/1.52 4613[5:MRR:4611.0,4612.0] || -> SkC45 SkC44 SkC18*. % 1.28/1.52 4614[5:MRR:175.1,4606.0] || SkC45* -> . % 1.28/1.52 4615[5:MRR:4613.0,4614.0] || -> SkC44 SkC18*. % 1.28/1.52 4621[5:MRR:3787.0,4605.0] || -> equal(op1(e11,e12),e13)**. % 1.28/1.52 4628[5:Rew:4621.0,4598.0] || -> equal(op1(e11,e13),e12)**. % 1.28/1.52 4632[5:Rew:4628.0,356.0] || equal(op1(e12,e13),e12)** -> . % 1.28/1.52 4636[5:MRR:172.1,4632.0] || SkC44* -> . % 1.28/1.52 4637[5:MRR:4615.0,4636.0] || -> SkC18*. % 1.28/1.52 4638[5:MRR:122.0,4637.0] || -> equal(op1(e11,e10),e11)**. % 1.28/1.52 4642[5:Rew:4638.0,338.0] || equal(op1(e12,e10),e11)** -> . % 1.28/1.52 4661[5:MRR:3788.1,4604.0] || -> equal(op1(e12,e13),e13)**. % 1.28/1.52 4668[5:Rew:4661.0,3687.0] || -> equal(e13,e12) equal(op1(e12,e11),e12)**. % 1.28/1.52 4669[5:MRR:4668.0,6.0] || -> equal(op1(e12,e11),e12)**. % 1.28/1.52 4689[5:Rew:4669.0,1368.1,4573.0,1368.0] || -> equal(e11,e10) equal(e12,e11) equal(op1(e12,e10),e11)**. % 1.28/1.52 4690[5:MRR:4689.0,4689.1,4689.2,1.0,4.0,4642.0] || -> . % 1.28/1.52 4700[2:Spt:4690.0,2895.0,2900.0] || equal(h2(e13),e22)** -> . % 1.28/1.52 4701[2:Spt:4690.0,2895.1,2895.2] || -> equal(h2(e13),e21)** equal(h2(e13),e20). % 1.28/1.52 4702[2:MRR:887.1,4700.0] || SkC123* -> . % 1.28/1.52 4703[2:MRR:951.1,4700.0] || SkC75* -> . % 1.28/1.52 4704[2:MRR:2897.0,2897.4,4702.0,4703.0] || -> SkC110 SkC105 SkC84 SkC73 SkC72*. % 1.28/1.52 4706[2:MRR:1322.0,4700.0] || -> equal(op2(e22,e21),e22)** equal(op2(e20,e21),e22). % 1.28/1.52 4707[3:Spt:4701.0] || -> equal(h2(e13),e21)**. % 1.28/1.52 4721[3:Rew:4707.0,1165.0] || equal(op2(e21,e20),e21)** -> . % 1.28/1.52 4723[3:Rew:4707.0,1176.0] || equal(op2(e22,e21),e21)** -> . % 1.28/1.52 4724[3:Rew:4707.0,1177.0] || equal(op2(e20,e21),e21)** -> . % 1.28/1.52 4736[3:MRR:245.1,4721.0] || SkC84* -> . % 1.28/1.52 4737[3:MRR:1349.0,4721.0] || -> equal(op2(e21,e20),e20)**. % 1.28/1.52 4738[3:MRR:1334.0,4721.0] || -> equal(op2(e22,e20),e21)**. % 1.28/1.52 4739[3:MRR:4704.2,4736.0] || -> SkC110 SkC105 SkC73 SkC72*. % 1.28/1.52 4742[3:Rew:4737.0,1221.0] || equal(h4(e12),e20)** -> . % 1.28/1.52 4743[3:Rew:4737.0,414.0] || equal(op2(e21,e22),e20)** -> . % 1.28/1.52 4750[3:Rew:4738.0,701.1] || SkC131 -> equal(op2(e22,e21),e20)**. % 1.28/1.52 4752[3:Rew:4738.0,1162.0] || equal(h3(e13),e21)** -> . % 1.28/1.52 4755[3:MRR:1347.2,4742.0] || -> equal(h4(e12),e23)** equal(h4(e12),e22). % 1.28/1.52 4756[3:MRR:955.1,4752.0] || SkC72* -> . % 1.28/1.52 4757[3:MRR:1344.2,4752.0] || -> equal(h3(e13),e23)** equal(h3(e13),e22) equal(h3(e13),e20). % 1.28/1.52 4758[3:MRR:4739.3,4756.0] || -> SkC110 SkC105 SkC73*. % 1.28/1.52 4759[3:MRR:781.1,4723.0] || -> equal(op2(e22,e21),e22) equal(op2(e22,e21),e23)** equal(op2(e22,e21),e20). % 1.28/1.52 4760[3:MRR:1336.0,4724.0] || -> equal(op2(e20,e22),e21)**. % 1.28/1.52 4763[3:Rew:4760.0,1315.1] || -> equal(h3(e13),e20) equal(e21,e20) equal(op2(e23,e22),e20)** equal(op2(e21,e22),e20). % 1.28/1.52 4769[3:Rew:4760.0,695.1] || SkC129 -> equal(op2(e20,e21),e22)**. % 1.28/1.52 4771[3:Rew:4760.0,1308.2] || -> equal(h3(e13),e22) equal(op2(e21,e22),e22)** equal(e22,e21). % 1.28/1.52 4779[3:MRR:4771.2,10.0] || -> equal(h3(e13),e22) equal(op2(e21,e22),e22)**. % 1.28/1.52 4784[3:MRR:4763.1,4763.3,7.0,4743.0] || -> equal(h3(e13),e20) equal(op2(e23,e22),e20)**. % 1.28/1.52 5158[4:Spt:1310.0] || -> equal(h3(e13),e22)**. % 1.28/1.52 5160[4:Rew:5158.0,4784.0] || -> equal(e22,e20) equal(op2(e23,e22),e20)**. % 1.28/1.52 5164[4:Rew:5158.0,1161.0] || equal(op2(e22,e21),e22)** -> . % 1.28/1.52 5168[4:Rew:5158.0,1306.0] || -> equal(e23,e22) equal(op2(e22,e23),e23)** equal(op2(e22,e21),e23). % 1.28/1.52 5179[4:MRR:286.1,5164.0] || SkC105* -> . % 1.28/1.52 5180[4:MRR:4706.0,5164.0] || -> equal(op2(e20,e21),e22)**. % 1.28/1.52 5181[4:MRR:4759.0,5164.0] || -> equal(op2(e22,e21),e23)** equal(op2(e22,e21),e20). % 1.28/1.52 5182[4:MRR:4758.1,5179.0] || -> SkC110 SkC73*. % 1.28/1.52 5186[4:Rew:5180.0,223.1] || SkC73* -> equal(e22,e20). % 1.28/1.52 5191[4:MRR:5186.1,8.0] || SkC73* -> . % 1.28/1.52 5192[4:MRR:5182.1,5191.0] || -> SkC110*. % 1.28/1.52 5193[4:MRR:295.0,5192.0] || -> equal(op2(e22,e23),e22)**. % 1.28/1.52 5238[4:MRR:5160.0,8.0] || -> equal(op2(e23,e22),e20)**. % 1.28/1.52 5242[4:Rew:5238.0,428.0] || equal(op2(e23,e21),e20)** -> . % 1.28/1.52 5243[4:MRR:1342.1,5242.0] || -> equal(op2(e23,e21),e23)**. % 1.28/1.52 5246[4:Rew:5243.0,394.0] || equal(op2(e22,e21),e23)** -> . % 1.28/1.52 5248[4:MRR:5181.0,5246.0] || -> equal(op2(e22,e21),e20)**. % 1.28/1.52 5255[4:Rew:5248.0,5168.2,5193.0,5168.1] || -> equal(e23,e22)** equal(e23,e22)** equal(e23,e20). % 1.28/1.52 5256[4:Obv:5255.0] || -> equal(e23,e22)** equal(e23,e20). % 1.28/1.52 5257[4:MRR:5256.0,5256.1,12.0,9.0] || -> . % 1.28/1.52 5262[4:Spt:5257.0,1310.0,5158.0] || equal(h3(e13),e22)** -> . % 1.28/1.52 5263[4:Spt:5257.0,1310.1,1310.2] || -> equal(op2(e22,e23),e22)** equal(op2(e22,e21),e22). % 1.28/1.52 5264[4:MRR:4779.0,5262.0] || -> equal(op2(e21,e22),e22)**. % 1.28/1.52 5268[4:Rew:5264.0,1219.0] || equal(h4(e12),e22)** -> . % 1.28/1.52 5270[4:MRR:4755.1,5268.0] || -> equal(h4(e12),e23)**. % 1.28/1.52 5274[4:Rew:5270.0,1222.0] || equal(op2(e22,e23),e23)** -> . % 1.28/1.52 5279[4:MRR:4757.1,5262.0] || -> equal(h3(e13),e23)** equal(h3(e13),e20). % 1.28/1.52 5280[4:MRR:1306.1,5274.0] || -> equal(h3(e13),e23) equal(op2(e22,e21),e23)**. % 1.28/1.52 5286[5:Spt:5263.0] || -> equal(op2(e22,e23),e22)**. % 1.28/1.52 5289[5:Rew:5286.0,423.0] || equal(op2(e22,e21),e22)** -> . % 1.28/1.52 5295[5:MRR:286.1,5289.0] || SkC105* -> . % 1.28/1.52 5296[5:MRR:4706.0,5289.0] || -> equal(op2(e20,e21),e22)**. % 1.28/1.52 5298[5:MRR:4758.1,5295.0] || -> SkC110 SkC73*. % 1.28/1.52 5303[5:Rew:5296.0,223.1] || SkC73* -> equal(e22,e20). % 1.28/1.52 5307[5:MRR:5303.1,8.0] || SkC73* -> . % 1.28/1.52 5308[5:MRR:5298.1,5307.0] || -> SkC110*. % 1.28/1.52 5309[5:MRR:1034.0,5308.0] || equal(h3(e13),e23)** -> . % 1.28/1.52 5311[5:MRR:5279.0,5309.0] || -> equal(h3(e13),e20)**. % 1.28/1.52 5312[5:MRR:5280.0,5309.0] || -> equal(op2(e22,e21),e23)**. % 1.28/1.52 5316[5:Rew:5311.0,1273.1] || SkC129* equal(e20,e20) -> . % 1.28/1.52 5328[5:Rew:5312.0,4750.1] || SkC131* -> equal(e23,e20). % 1.28/1.52 5329[5:Rew:5312.0,394.0] || equal(op2(e23,e21),e23)** -> . % 1.28/1.52 5337[5:MRR:5328.1,9.0] || SkC131* -> . % 1.28/1.52 5339[5:MRR:1268.0,5337.0] || -> SkC129 equal(op2(e23,e21),e23)**. % 1.28/1.52 5348[5:Obv:5316.1] || SkC129* -> . % 1.28/1.52 5356[5:MRR:1342.0,5329.0] || -> equal(op2(e23,e21),e20)**. % 1.28/1.52 5362[5:Rew:5356.0,5339.1] || -> SkC129* equal(e23,e20). % 1.28/1.52 5363[5:MRR:5362.0,5362.1,5348.0,9.0] || -> . % 1.28/1.52 5369[5:Spt:5363.0,5263.0,5286.0] || equal(op2(e22,e23),e22)** -> . % 1.28/1.52 5370[5:Spt:5363.0,5263.1] || -> equal(op2(e22,e21),e22)**. % 1.28/1.52 5372[5:MRR:295.1,5369.0] || SkC110* -> . % 1.28/1.52 5373[5:MRR:4758.0,5372.0] || -> SkC105 SkC73*. % 1.28/1.52 5375[5:Rew:5370.0,4750.1] || SkC131* -> equal(e22,e20). % 1.28/1.52 5376[5:MRR:5375.1,8.0] || SkC131* -> . % 1.28/1.52 5377[5:MRR:1268.0,5376.0] || -> SkC129 equal(op2(e23,e21),e23)**. % 1.28/1.52 5380[5:Rew:5370.0,390.0] || equal(op2(e20,e21),e22)** -> . % 1.28/1.52 5381[5:MRR:4769.1,5380.0] || SkC129* -> . % 1.28/1.52 5382[5:MRR:5377.0,5381.0] || -> equal(op2(e23,e21),e23)**. % 1.28/1.52 5385[5:Rew:5382.0,631.1] || SkC105* equal(e23,e23) -> . % 1.28/1.52 5387[5:Obv:5385.1] || SkC105* -> . % 1.28/1.52 5388[5:MRR:5373.0,5387.0] || -> SkC73*. % 1.28/1.52 5396[5:Rew:5382.0,568.1] || SkC73* equal(e23,e23) -> . % 1.28/1.52 5397[5:Obv:5396.1] || SkC73* -> . % 1.28/1.52 5398[5:MRR:5397.0,5388.0] || -> . % 1.28/1.52 5440[3:Spt:5398.0,4701.0,4707.0] || equal(h2(e13),e21)** -> . % 1.28/1.52 5441[3:Spt:5398.0,4701.1] || -> equal(h2(e13),e20)**. % 1.28/1.52 5452[3:Rew:5441.0,1177.0] || equal(op2(e20,e21),e20)** -> . % 1.28/1.52 5453[3:MRR:223.1,5452.0] || SkC73* -> . % 1.28/1.52 5454[3:MRR:4704.3,5453.0] || -> SkC110 SkC105 SkC84 SkC72*. % 1.28/1.52 5456[3:Rew:5441.0,1175.0] || equal(op2(e23,e21),e20)** -> . % 1.28/1.52 5459[3:Rew:5441.0,1008.0] || -> equal(op2(e20,e21),h2(e12))**. % 1.28/1.52 5461[3:Rew:5459.0,5452.0] || equal(h2(e12),e20)** -> . % 1.36/1.53 5462[3:Rew:5441.0,1070.1] || SkC84* equal(e20,e20) -> . % 1.36/1.53 5463[3:Obv:5462.1] || SkC84* -> . % 1.36/1.53 5464[3:MRR:5454.2,5463.0] || -> SkC110 SkC105 SkC72*. % 1.36/1.53 5465[3:Rew:5459.0,221.1] || SkC72 -> equal(h2(e12),e20)**. % 1.36/1.53 5466[3:MRR:5465.1,5461.0] || SkC72* -> . % 1.36/1.53 5467[3:MRR:5464.2,5466.0] || -> SkC110 SkC105*. % 1.36/1.53 5477[3:Rew:5459.0,4706.1] || -> equal(op2(e22,e21),e22)** equal(h2(e12),e22). % 1.36/1.53 5478[3:MRR:1302.1,5456.0] || -> equal(op2(e23,e22),e20)**. % 1.36/1.53 5481[3:Rew:5478.0,1172.0] || equal(h3(e13),e20)** -> . % 1.36/1.53 5485[3:Rew:5478.0,1296.0] || -> equal(e23,e20) equal(op2(e23,e21),e23)**. % 1.36/1.53 5486[3:MRR:5485.0,9.0] || -> equal(op2(e23,e21),e23)**. % 1.36/1.53 5489[3:Rew:5486.0,631.1] || SkC105* equal(e23,e23) -> . % 1.36/1.53 5493[3:Obv:5489.1] || SkC105* -> . % 1.36/1.53 5494[3:MRR:5467.1,5493.0] || -> SkC110*. % 1.36/1.53 5495[3:MRR:295.0,5494.0] || -> equal(op2(e22,e23),e22)**. % 1.36/1.53 5496[3:MRR:1034.0,5494.0] || equal(h3(e13),e23)** -> . % 1.36/1.53 5499[3:Rew:5495.0,1160.0] || equal(h3(e13),e22)** -> . % 1.36/1.53 5501[3:Rew:5495.0,423.0] || equal(op2(e22,e21),e22)** -> . % 1.36/1.53 5516[3:MRR:5477.0,5501.0] || -> equal(h2(e12),e22)**. % 1.36/1.53 5518[3:Rew:5516.0,5459.0] || -> equal(op2(e20,e21),e22)**. % 1.36/1.53 5550[3:Rew:5518.0,1336.0] || -> equal(e22,e21) equal(op2(e20,e22),e21)**. % 1.36/1.53 5551[3:MRR:5550.0,10.0] || -> equal(op2(e20,e22),e21)**. % 1.36/1.53 5553[3:Rew:5551.0,1174.0] || equal(h3(e13),e21)** -> . % 1.36/1.53 5571[3:MRR:1344.0,1344.1,1344.2,1344.3,5496.0,5499.0,5553.0,5481.0] || -> . % 1.36/1.53 % SZS output end Refutation % 1.36/1.53 Formulae used in the proof : ax7 ax8 ax14 ax12 ax13 co1 ax15 ax16 ax17 ax10 ax11 ax5 ax6 ax4 ax3 ax2 ax1 % 1.36/1.53 %------------------------------------------------------------------------------