%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG106+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 14 18:02:28 EDT 2022 % Result : Theorem 0.71s 0.88s % Output : Refutation 0.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : ALG106+1 : TPTP v8.1.0. Released v2.7.0. % 0.08/0.14 % Command : run_spass %d %s % 0.15/0.36 % Computer : n020.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Wed Jun 8 22:47:21 EDT 2022 % 0.15/0.36 % CPUTime : % 0.71/0.88 % 0.71/0.88 SPASS V 3.9 % 0.71/0.88 SPASS beiseite: Proof found. % 0.71/0.88 % SZS status Theorem % 0.71/0.88 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.88 SPASS derived 1427 clauses, backtracked 1475 clauses, performed 14 splits and kept 2362 clauses. % 0.71/0.88 SPASS allocated 87523 KBytes. % 0.71/0.88 SPASS spent 0:00:00.51 on the problem. % 0.71/0.88 0:00:00.04 for the input. % 0.71/0.88 0:00:00.10 for the FLOTTER CNF translation. % 0.71/0.88 0:00:00.00 for inferences. % 0.71/0.88 0:00:00.01 for the backtracking. % 0.71/0.88 0:00:00.33 for the reduction. % 0.71/0.88 % 0.71/0.88 % 0.71/0.88 Here is a proof with depth 3, length 917 : % 0.71/0.88 % SZS output start Refutation % 0.71/0.88 1[0:Inp] || equal(e11,e10)** -> . % 0.71/0.88 2[0:Inp] || equal(e12,e10)** -> . % 0.71/0.88 3[0:Inp] || equal(e13,e10)** -> . % 0.71/0.88 4[0:Inp] || equal(e12,e11)** -> . % 0.71/0.88 5[0:Inp] || equal(e13,e11)** -> . % 0.71/0.88 6[0:Inp] || equal(e13,e12)** -> . % 0.71/0.88 7[0:Inp] || equal(e21,e20)** -> . % 0.71/0.88 8[0:Inp] || equal(e22,e20)** -> . % 0.71/0.88 9[0:Inp] || equal(e23,e20)** -> . % 0.71/0.88 10[0:Inp] || equal(e22,e21)** -> . % 0.71/0.88 11[0:Inp] || equal(e23,e21)** -> . % 0.71/0.88 12[0:Inp] || equal(e23,e22)** -> . % 0.71/0.88 31[0:Inp] || -> equal(h3(e13),e22)**. % 0.71/0.88 33[0:Inp] || -> equal(op1(e13,e13),e11)**. % 0.71/0.88 34[0:Inp] || -> equal(op2(e23,e23),e21)**. % 0.71/0.88 59[0:Inp] || equal(h3(e10),e20)** -> SkC36. % 0.71/0.88 64[0:Inp] || equal(h3(e11),e21)** -> SkC37. % 0.71/0.88 70[0:Inp] || equal(h3(e13),e22)** -> SkC38. % 0.71/0.88 83[0:Inp] || -> equal(op2(e20,e20),h1(e11))**. % 0.71/0.88 84[0:Inp] || -> equal(op2(e21,e21),h2(e11))**. % 0.71/0.88 85[0:Inp] || -> equal(op2(e22,e22),h3(e11))**. % 0.71/0.88 87[0:Inp] || SkC0 -> equal(op1(e10,e10),e10)**. % 0.71/0.88 91[0:Inp] || SkC2 -> equal(op1(e12,e10),e10)**. % 0.71/0.88 92[0:Inp] || SkC3 -> equal(op1(e10,e13),e10)**. % 0.71/0.88 94[0:Inp] || SkC4 -> equal(op1(e11,e10),e11)**. % 0.71/0.88 95[0:Inp] || SkC4 -> equal(op1(e10,e11),e11)**. % 0.71/0.88 97[0:Inp] || SkC6 -> equal(op1(e11,e12),e11)**. % 0.71/0.88 98[0:Inp] || SkC6 -> equal(op1(e12,e11),e11)**. % 0.71/0.88 100[0:Inp] || SkC7 -> equal(op1(e13,e11),e11)**. % 0.71/0.88 101[0:Inp] || SkC8 -> equal(op1(e12,e10),e12)**. % 0.71/0.88 102[0:Inp] || SkC8 -> equal(op1(e10,e12),e12)**. % 0.71/0.88 105[0:Inp] || SkC10 -> equal(op1(e12,e12),e12)**. % 0.71/0.88 107[0:Inp] || SkC11 -> equal(op1(e13,e12),e12)**. % 0.71/0.88 108[0:Inp] || SkC12 -> equal(op1(e13,e10),e13)**. % 0.71/0.88 109[0:Inp] || SkC12 -> equal(op1(e10,e13),e13)**. % 0.71/0.88 110[0:Inp] || SkC13 -> equal(op1(e13,e11),e13)**. % 0.71/0.88 113[0:Inp] || SkC14 -> equal(op1(e12,e13),e13)**. % 0.71/0.88 114[0:Inp] || SkC15 -> equal(op2(e20,e20),e20)**. % 0.71/0.88 118[0:Inp] || SkC17 -> equal(op2(e22,e20),e20)**. % 0.71/0.88 119[0:Inp] || SkC18 -> equal(op2(e20,e23),e20)**. % 0.71/0.88 121[0:Inp] || SkC19 -> equal(op2(e21,e20),e21)**. % 0.71/0.88 124[0:Inp] || SkC21 -> equal(op2(e21,e22),e21)**. % 0.71/0.88 125[0:Inp] || SkC21 -> equal(op2(e22,e21),e21)**. % 0.71/0.88 127[0:Inp] || SkC22 -> equal(op2(e23,e21),e21)**. % 0.71/0.88 128[0:Inp] || SkC23 -> equal(op2(e22,e20),e22)**. % 0.71/0.88 129[0:Inp] || SkC23 -> equal(op2(e20,e22),e22)**. % 0.71/0.88 132[0:Inp] || SkC25 -> equal(op2(e22,e22),e22)**. % 0.71/0.88 134[0:Inp] || SkC26 -> equal(op2(e23,e22),e22)**. % 0.71/0.88 135[0:Inp] || SkC27 -> equal(op2(e23,e20),e23)**. % 0.71/0.88 136[0:Inp] || SkC27 -> equal(op2(e20,e23),e23)**. % 0.71/0.88 137[0:Inp] || SkC28 -> equal(op2(e23,e21),e23)**. % 0.71/0.88 140[0:Inp] || SkC29 -> equal(op2(e22,e23),e23)**. % 0.71/0.88 141[0:Inp] || -> equal(op1(e13,op1(e13,e13)),e12)**. % 0.71/0.88 142[0:Inp] || -> equal(op2(e23,op2(e23,e23)),e22)**. % 0.71/0.88 143[0:Inp] || equal(op1(e11,e10),op1(e10,e10))** -> . % 0.71/0.88 144[0:Inp] || equal(op1(e12,e10),op1(e10,e10))** -> . % 0.71/0.88 145[0:Inp] || equal(op1(e13,e10),op1(e10,e10))** -> . % 0.71/0.88 146[0:Inp] || equal(op1(e12,e10),op1(e11,e10))** -> . % 0.71/0.88 147[0:Inp] || equal(op1(e13,e10),op1(e11,e10))** -> . % 0.71/0.88 149[0:Inp] || equal(op1(e11,e11),op1(e10,e11))** -> . % 0.71/0.88 150[0:Inp] || equal(op1(e12,e11),op1(e10,e11))** -> . % 0.71/0.88 151[0:Inp] || equal(op1(e13,e11),op1(e10,e11))** -> . % 0.71/0.88 152[0:Inp] || equal(op1(e12,e11),op1(e11,e11))** -> . % 0.71/0.88 153[0:Inp] || equal(op1(e13,e11),op1(e11,e11))** -> . % 0.71/0.88 154[0:Inp] || equal(op1(e13,e11),op1(e12,e11))** -> . % 0.71/0.88 155[0:Inp] || equal(op1(e11,e12),op1(e10,e12))** -> . % 0.71/0.88 159[0:Inp] || equal(op1(e13,e12),op1(e11,e12))** -> . % 0.71/0.88 160[0:Inp] || equal(op1(e13,e12),op1(e12,e12))** -> . % 0.71/0.88 161[0:Inp] || equal(op1(e11,e13),op1(e10,e13))** -> . % 0.71/0.88 162[0:Inp] || equal(op1(e12,e13),op1(e10,e13))** -> . % 0.71/0.88 163[0:Inp] || equal(op1(e13,e13),op1(e10,e13))** -> . % 0.71/0.88 164[0:Inp] || equal(op1(e12,e13),op1(e11,e13))** -> . % 0.71/0.88 165[0:Inp] || equal(op1(e13,e13),op1(e11,e13))** -> . % 0.71/0.88 167[0:Inp] || equal(op1(e10,e11),op1(e10,e10))** -> . % 0.71/0.88 168[0:Inp] || equal(op1(e10,e12),op1(e10,e10))** -> . % 0.71/0.88 169[0:Inp] || equal(op1(e10,e13),op1(e10,e10))** -> . % 0.71/0.88 170[0:Inp] || equal(op1(e10,e12),op1(e10,e11))** -> . % 0.71/0.88 171[0:Inp] || equal(op1(e10,e13),op1(e10,e11))** -> . % 0.71/0.88 172[0:Inp] || equal(op1(e10,e13),op1(e10,e12))** -> . % 0.71/0.88 173[0:Inp] || equal(op1(e11,e11),op1(e11,e10))** -> . % 0.71/0.88 174[0:Inp] || equal(op1(e11,e12),op1(e11,e10))** -> . % 0.71/0.88 175[0:Inp] || equal(op1(e11,e13),op1(e11,e10))** -> . % 0.71/0.88 177[0:Inp] || equal(op1(e11,e13),op1(e11,e11))** -> . % 0.71/0.88 178[0:Inp] || equal(op1(e11,e13),op1(e11,e12))** -> . % 0.71/0.88 180[0:Inp] || equal(op1(e12,e12),op1(e12,e10))** -> . % 0.71/0.88 181[0:Inp] || equal(op1(e12,e13),op1(e12,e10))** -> . % 0.71/0.88 183[0:Inp] || equal(op1(e12,e13),op1(e12,e11))** -> . % 0.71/0.88 184[0:Inp] || equal(op1(e12,e13),op1(e12,e12))** -> . % 0.71/0.88 185[0:Inp] || equal(op1(e13,e11),op1(e13,e10))** -> . % 0.71/0.88 186[0:Inp] || equal(op1(e13,e12),op1(e13,e10))** -> . % 0.71/0.88 187[0:Inp] || equal(op1(e13,e13),op1(e13,e10))** -> . % 0.71/0.88 188[0:Inp] || equal(op1(e13,e12),op1(e13,e11))** -> . % 0.71/0.88 190[0:Inp] || equal(op1(e13,e13),op1(e13,e12))** -> . % 0.71/0.88 191[0:Inp] || equal(op2(e21,e20),op2(e20,e20))** -> . % 0.71/0.88 192[0:Inp] || equal(op2(e22,e20),op2(e20,e20))** -> . % 0.71/0.88 193[0:Inp] || equal(op2(e23,e20),op2(e20,e20))** -> . % 0.71/0.88 194[0:Inp] || equal(op2(e22,e20),op2(e21,e20))** -> . % 0.71/0.88 195[0:Inp] || equal(op2(e23,e20),op2(e21,e20))** -> . % 0.71/0.88 197[0:Inp] || equal(op2(e21,e21),op2(e20,e21))** -> . % 0.71/0.88 198[0:Inp] || equal(op2(e22,e21),op2(e20,e21))** -> . % 0.71/0.88 199[0:Inp] || equal(op2(e23,e21),op2(e20,e21))** -> . % 0.71/0.88 200[0:Inp] || equal(op2(e22,e21),op2(e21,e21))** -> . % 0.71/0.88 201[0:Inp] || equal(op2(e23,e21),op2(e21,e21))** -> . % 0.71/0.88 202[0:Inp] || equal(op2(e23,e21),op2(e22,e21))** -> . % 0.71/0.88 203[0:Inp] || equal(op2(e21,e22),op2(e20,e22))** -> . % 0.71/0.88 205[0:Inp] || equal(op2(e23,e22),op2(e20,e22))** -> . % 0.71/0.88 208[0:Inp] || equal(op2(e23,e22),op2(e22,e22))** -> . % 0.71/0.88 209[0:Inp] || equal(op2(e21,e23),op2(e20,e23))** -> . % 0.71/0.88 210[0:Inp] || equal(op2(e22,e23),op2(e20,e23))** -> . % 0.71/0.88 211[0:Inp] || equal(op2(e23,e23),op2(e20,e23))** -> . % 0.71/0.88 212[0:Inp] || equal(op2(e22,e23),op2(e21,e23))** -> . % 0.71/0.88 213[0:Inp] || equal(op2(e23,e23),op2(e21,e23))** -> . % 0.71/0.88 215[0:Inp] || equal(op2(e20,e21),op2(e20,e20))** -> . % 0.71/0.88 216[0:Inp] || equal(op2(e20,e22),op2(e20,e20))** -> . % 0.71/0.88 217[0:Inp] || equal(op2(e20,e23),op2(e20,e20))** -> . % 0.71/0.88 218[0:Inp] || equal(op2(e20,e22),op2(e20,e21))** -> . % 0.71/0.88 219[0:Inp] || equal(op2(e20,e23),op2(e20,e21))** -> . % 0.71/0.88 220[0:Inp] || equal(op2(e20,e23),op2(e20,e22))** -> . % 0.71/0.88 222[0:Inp] || equal(op2(e21,e22),op2(e21,e20))** -> . % 0.71/0.88 223[0:Inp] || equal(op2(e21,e23),op2(e21,e20))** -> . % 0.71/0.88 224[0:Inp] || equal(op2(e21,e22),op2(e21,e21))** -> . % 0.71/0.88 225[0:Inp] || equal(op2(e21,e23),op2(e21,e21))** -> . % 0.71/0.88 226[0:Inp] || equal(op2(e21,e23),op2(e21,e22))** -> . % 0.71/0.88 227[0:Inp] || equal(op2(e22,e21),op2(e22,e20))** -> . % 0.71/0.88 228[0:Inp] || equal(op2(e22,e22),op2(e22,e20))** -> . % 0.71/0.88 229[0:Inp] || equal(op2(e22,e23),op2(e22,e20))** -> . % 0.71/0.88 230[0:Inp] || equal(op2(e22,e22),op2(e22,e21))** -> . % 0.71/0.88 231[0:Inp] || equal(op2(e22,e23),op2(e22,e21))** -> . % 0.71/0.88 232[0:Inp] || equal(op2(e22,e23),op2(e22,e22))** -> . % 0.71/0.88 233[0:Inp] || equal(op2(e23,e21),op2(e23,e20))** -> . % 0.71/0.88 234[0:Inp] || equal(op2(e23,e22),op2(e23,e20))** -> . % 0.71/0.88 235[0:Inp] || equal(op2(e23,e23),op2(e23,e20))** -> . % 0.71/0.88 236[0:Inp] || equal(op2(e23,e22),op2(e23,e21))** -> . % 0.71/0.88 238[0:Inp] || equal(op2(e23,e23),op2(e23,e22))** -> . % 0.71/0.88 239[0:Inp] || equal(op1(e10,e10),e10)** SkC0 -> . % 0.71/0.88 246[0:Inp] || equal(op1(e13,e13),e11)** SkC1 -> . % 0.71/0.88 255[0:Inp] || SkC4 equal(op1(e10,e10),e10)** -> . % 0.71/0.88 262[0:Inp] || equal(op1(e13,e13),e11)** SkC5 -> . % 0.71/0.88 263[0:Inp] || SkC6 equal(op1(e10,e10),e12)** -> . % 0.71/0.88 265[0:Inp] || SkC6 equal(op1(e12,e12),e12)** -> . % 0.71/0.88 271[0:Inp] || SkC8 equal(op1(e10,e10),e10)** -> . % 0.71/0.88 272[0:Inp] || SkC8 equal(op1(e11,e11),e10)** -> . % 0.71/0.88 278[0:Inp] || equal(op1(e13,e13),e11)** SkC9 -> . % 0.71/0.88 281[0:Inp] || equal(op1(e12,e12),e12)** SkC10 -> . % 0.71/0.88 287[0:Inp] || SkC12 equal(op1(e10,e10),e10)** -> . % 0.71/0.88 288[0:Inp] || SkC12 equal(op1(e11,e11),e10)** -> . % 0.71/0.88 299[0:Inp] || equal(op2(e20,e20),e20)** SkC15 -> . % 0.71/0.88 306[0:Inp] || equal(op2(e23,e23),e21)** SkC16 -> . % 0.71/0.88 315[0:Inp] || equal(op2(e20,e20),e20)** SkC19 -> . % 0.71/0.88 316[0:Inp] || equal(op2(e21,e21),e20)** SkC19 -> . % 0.71/0.88 322[0:Inp] || equal(op2(e23,e23),e21)** SkC20 -> . % 0.71/0.88 323[0:Inp] || equal(op2(e20,e20),e22)** SkC21 -> . % 0.71/0.88 325[0:Inp] || equal(op2(e22,e22),e22)** SkC21 -> . % 0.71/0.88 331[0:Inp] || equal(op2(e20,e20),e20)** SkC23 -> . % 0.71/0.88 332[0:Inp] || equal(op2(e21,e21),e20)** SkC23 -> . % 0.71/0.88 338[0:Inp] || equal(op2(e23,e23),e21)** SkC24 -> . % 0.71/0.88 341[0:Inp] || equal(op2(e22,e22),e22)** SkC25 -> . % 0.71/0.88 347[0:Inp] || equal(op2(e20,e20),e20)** SkC27 -> . % 0.71/0.88 348[0:Inp] || equal(op2(e21,e21),e20)** SkC27 -> . % 0.71/0.88 359[0:Inp] || -> equal(op2(e20,op2(e20,e20)),h1(e12))**. % 0.71/0.88 360[0:Inp] || -> equal(op2(e21,op2(e21,e21)),h2(e12))**. % 0.71/0.88 361[0:Inp] || -> equal(op2(e22,op2(e22,e22)),h3(e12))**. % 0.71/0.88 363[0:Inp] || -> equal(op1(op1(e13,op1(e13,e13)),e13),e10)**. % 0.71/0.88 364[0:Inp] || -> equal(op2(op2(e23,op2(e23,e23)),e23),e20)**. % 0.71/0.88 365[0:Inp] || -> equal(op2(op2(e20,op2(e20,e20)),e20),h1(e10))**. % 0.71/0.88 367[0:Inp] || -> equal(op2(op2(e22,op2(e22,e22)),e22),h3(e10))**. % 0.71/0.88 369[0:Inp] || -> equal(op2(e23,e23),e23)** SkC15 SkC16 SkC17 SkC18 SkC19 SkC20 SkC21 SkC22 SkC23 SkC24 SkC25 SkC26 SkC27 SkC28 SkC29. % 0.71/0.88 370[0:Inp] || -> equal(op1(e13,e13),e13)** SkC0 SkC1 SkC2 SkC3 SkC4 SkC5 SkC6 SkC7 SkC8 SkC9 SkC10 SkC11 SkC12 SkC13 SkC14. % 0.71/0.88 371[0:Inp] || -> equal(op2(e20,e23),e23) equal(op2(e21,e23),e23) equal(op2(e22,e23),e23) equal(op2(e23,e23),e23)**. % 0.71/0.88 373[0:Inp] || -> equal(op2(e20,e23),e22) equal(op2(e21,e23),e22) equal(op2(e22,e23),e22) equal(op2(e23,e23),e22)**. % 0.71/0.88 379[0:Inp] || -> equal(op2(e20,e22),e23) equal(op2(e21,e22),e23) equal(op2(e22,e22),e23) equal(op2(e23,e22),e23)**. % 0.71/0.88 381[0:Inp] || -> equal(op2(e20,e22),e22) equal(op2(e21,e22),e22) equal(op2(e22,e22),e22) equal(op2(e23,e22),e22)**. % 0.71/0.88 382[0:Inp] || -> equal(op2(e22,e20),e22) equal(op2(e22,e21),e22) equal(op2(e22,e22),e22) equal(op2(e22,e23),e22)**. % 0.71/0.88 384[0:Inp] || -> equal(op2(e22,e20),e21) equal(op2(e22,e21),e21) equal(op2(e22,e22),e21) equal(op2(e22,e23),e21)**. % 0.71/0.88 385[0:Inp] || -> equal(op2(e20,e22),e20) equal(op2(e21,e22),e20) equal(op2(e22,e22),e20) equal(op2(e23,e22),e20)**. % 0.71/0.88 387[0:Inp] || -> equal(op2(e20,e21),e23) equal(op2(e21,e21),e23) equal(op2(e22,e21),e23) equal(op2(e23,e21),e23)**. % 0.71/0.88 390[0:Inp] || -> equal(op2(e21,e20),e22) equal(op2(e21,e21),e22) equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.71/0.88 393[0:Inp] || -> equal(op2(e20,e21),e20) equal(op2(e21,e21),e20) equal(op2(e22,e21),e20) equal(op2(e23,e21),e20)**. % 0.71/0.88 394[0:Inp] || -> equal(op2(e21,e20),e20) equal(op2(e21,e21),e20) equal(op2(e21,e22),e20) equal(op2(e21,e23),e20)**. % 0.71/0.88 395[0:Inp] || -> equal(op2(e20,e20),e23) equal(op2(e21,e20),e23) equal(op2(e22,e20),e23) equal(op2(e23,e20),e23)**. % 0.71/0.88 397[0:Inp] || -> equal(op2(e20,e20),e22) equal(op2(e21,e20),e22) equal(op2(e22,e20),e22) equal(op2(e23,e20),e22)**. % 0.71/0.88 399[0:Inp] || -> equal(op2(e20,e20),e21) equal(op2(e21,e20),e21) equal(op2(e22,e20),e21) equal(op2(e23,e20),e21)**. % 0.71/0.88 400[0:Inp] || -> equal(op2(e20,e20),e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21) equal(op2(e20,e23),e21)**. % 0.71/0.88 401[0:Inp] || -> equal(op2(e20,e20),e20) equal(op2(e21,e20),e20) equal(op2(e22,e20),e20) equal(op2(e23,e20),e20)**. % 0.71/0.88 404[0:Inp] || -> equal(op2(e23,e22),e20) equal(op2(e23,e22),e21) equal(op2(e23,e22),e22) equal(op2(e23,e22),e23)**. % 0.71/0.88 406[0:Inp] || -> equal(op2(e23,e20),e20) equal(op2(e23,e20),e21) equal(op2(e23,e20),e22) equal(op2(e23,e20),e23)**. % 0.71/0.88 408[0:Inp] || -> equal(op2(e22,e22),e20) equal(op2(e22,e22),e21) equal(op2(e22,e22),e22) equal(op2(e22,e22),e23)**. % 0.71/0.88 409[0:Inp] || -> equal(op2(e22,e21),e20) equal(op2(e22,e21),e21) equal(op2(e22,e21),e22) equal(op2(e22,e21),e23)**. % 0.71/0.88 410[0:Inp] || -> equal(op2(e22,e20),e20) equal(op2(e22,e20),e21) equal(op2(e22,e20),e22) equal(op2(e22,e20),e23)**. % 0.71/0.88 411[0:Inp] || -> equal(op2(e21,e23),e20) equal(op2(e21,e23),e21) equal(op2(e21,e23),e22) equal(op2(e21,e23),e23)**. % 0.71/0.88 412[0:Inp] || -> equal(op2(e21,e22),e22) equal(op2(e21,e22),e21) equal(op2(e21,e22),e23)** equal(op2(e21,e22),e20). % 0.71/0.88 413[0:Inp] || -> equal(op2(e21,e21),e20) equal(op2(e21,e21),e21) equal(op2(e21,e21),e22) equal(op2(e21,e21),e23)**. % 0.71/0.88 414[0:Inp] || -> equal(op2(e21,e20),e21) equal(op2(e21,e20),e20) equal(op2(e21,e20),e23)** equal(op2(e21,e20),e22). % 0.71/0.88 415[0:Inp] || -> equal(op2(e20,e23),e20) equal(op2(e20,e23),e21) equal(op2(e20,e23),e22) equal(op2(e20,e23),e23)**. % 0.71/0.88 416[0:Inp] || -> equal(op2(e20,e22),e22) equal(op2(e20,e22),e20) equal(op2(e20,e22),e23)** equal(op2(e20,e22),e21). % 0.71/0.88 417[0:Inp] || -> equal(op2(e20,e21),e20) equal(op2(e20,e21),e21) equal(op2(e20,e21),e22) equal(op2(e20,e21),e23)**. % 0.71/0.88 418[0:Inp] || -> equal(op2(e20,e20),e20) equal(op2(e20,e20),e21) equal(op2(e20,e20),e22) equal(op2(e20,e20),e23)**. % 0.71/0.88 419[0:Inp] || -> equal(op1(e10,e13),e13) equal(op1(e11,e13),e13) equal(op1(e12,e13),e13) equal(op1(e13,e13),e13)**. % 0.71/0.88 420[0:Inp] || -> equal(op1(e13,e10),e13) equal(op1(e13,e11),e13) equal(op1(e13,e12),e13) equal(op1(e13,e13),e13)**. % 0.71/0.88 421[0:Inp] || -> equal(op1(e10,e13),e12) equal(op1(e11,e13),e12) equal(op1(e12,e13),e12) equal(op1(e13,e13),e12)**. % 0.71/0.88 426[0:Inp] || -> equal(op1(e13,e10),e10) equal(op1(e13,e11),e10) equal(op1(e13,e12),e10) equal(op1(e13,e13),e10)**. % 0.71/0.88 427[0:Inp] || -> equal(op1(e13,e12),e13)** equal(op1(e12,e12),e13) equal(op1(e11,e12),e13) equal(op1(e10,e12),e13). % 0.71/0.88 428[0:Inp] || -> equal(op1(e12,e10),e13) equal(op1(e12,e11),e13) equal(op1(e12,e12),e13) equal(op1(e12,e13),e13)**. % 0.71/0.88 429[0:Inp] || -> equal(op1(e10,e12),e12) equal(op1(e11,e12),e12) equal(op1(e12,e12),e12) equal(op1(e13,e12),e12)**. % 0.71/0.88 430[0:Inp] || -> equal(op1(e12,e10),e12) equal(op1(e12,e11),e12) equal(op1(e12,e12),e12) equal(op1(e12,e13),e12)**. % 0.71/0.88 432[0:Inp] || -> equal(op1(e12,e10),e11) equal(op1(e12,e11),e11) equal(op1(e12,e12),e11) equal(op1(e12,e13),e11)**. % 0.71/0.88 433[0:Inp] || -> equal(op1(e10,e12),e10) equal(op1(e11,e12),e10) equal(op1(e12,e12),e10) equal(op1(e13,e12),e10)**. % 0.71/0.88 436[0:Inp] || -> equal(op1(e11,e13),e13)** equal(op1(e11,e11),e13) equal(op1(e11,e12),e13) equal(op1(e11,e10),e13). % 0.71/0.88 439[0:Inp] || -> equal(op1(e10,e11),e11) equal(op1(e11,e11),e11) equal(op1(e12,e11),e11) equal(op1(e13,e11),e11)**. % 0.71/0.88 440[0:Inp] || -> equal(op1(e11,e10),e11) equal(op1(e11,e11),e11) equal(op1(e11,e12),e11) equal(op1(e11,e13),e11)**. % 0.71/0.88 441[0:Inp] || -> equal(op1(e10,e11),e10) equal(op1(e11,e11),e10) equal(op1(e12,e11),e10) equal(op1(e13,e11),e10)**. % 0.71/0.88 442[0:Inp] || -> equal(op1(e11,e10),e10) equal(op1(e11,e11),e10) equal(op1(e11,e12),e10) equal(op1(e11,e13),e10)**. % 0.71/0.88 443[0:Inp] || -> equal(op1(e13,e10),e13)** equal(op1(e10,e10),e13) equal(op1(e12,e10),e13) equal(op1(e11,e10),e13). % 0.71/0.88 445[0:Inp] || -> equal(op1(e10,e10),e12) equal(op1(e11,e10),e12) equal(op1(e12,e10),e12) equal(op1(e13,e10),e12)**. % 0.71/0.88 449[0:Inp] || -> equal(op1(e10,e10),e10) equal(op1(e11,e10),e10) equal(op1(e12,e10),e10) equal(op1(e13,e10),e10)**. % 0.71/0.88 450[0:Inp] || -> equal(op1(e10,e10),e10) equal(op1(e10,e11),e10) equal(op1(e10,e12),e10) equal(op1(e10,e13),e10)**. % 0.71/0.88 452[0:Inp] || -> equal(op1(e13,e12),e10) equal(op1(e13,e12),e11) equal(op1(e13,e12),e12) equal(op1(e13,e12),e13)**. % 0.71/0.88 454[0:Inp] || -> equal(op1(e13,e10),e10) equal(op1(e13,e10),e11) equal(op1(e13,e10),e12) equal(op1(e13,e10),e13)**. % 0.71/0.88 456[0:Inp] || -> equal(op1(e12,e12),e10) equal(op1(e12,e12),e11) equal(op1(e12,e12),e12) equal(op1(e12,e12),e13)**. % 0.71/0.88 457[0:Inp] || -> equal(op1(e12,e11),e10) equal(op1(e12,e11),e11) equal(op1(e12,e11),e12) equal(op1(e12,e11),e13)**. % 0.71/0.88 458[0:Inp] || -> equal(op1(e12,e10),e10) equal(op1(e12,e10),e11) equal(op1(e12,e10),e12) equal(op1(e12,e10),e13)**. % 0.71/0.88 459[0:Inp] || -> equal(op1(e11,e13),e10) equal(op1(e11,e13),e11) equal(op1(e11,e13),e12) equal(op1(e11,e13),e13)**. % 0.71/0.88 461[0:Inp] || -> equal(op1(e11,e11),e10) equal(op1(e11,e11),e11) equal(op1(e11,e11),e12) equal(op1(e11,e11),e13)**. % 0.71/0.88 462[0:Inp] || -> equal(op1(e11,e10),e11) equal(op1(e11,e10),e10) equal(op1(e11,e10),e13)** equal(op1(e11,e10),e12). % 0.71/0.88 463[0:Inp] || -> equal(op1(e10,e13),e10) equal(op1(e10,e13),e11) equal(op1(e10,e13),e12) equal(op1(e10,e13),e13)**. % 0.71/0.88 464[0:Inp] || -> equal(op1(e10,e12),e12) equal(op1(e10,e12),e10) equal(op1(e10,e12),e13)** equal(op1(e10,e12),e11). % 0.71/0.88 465[0:Inp] || -> equal(op1(e10,e11),e10) equal(op1(e10,e11),e11) equal(op1(e10,e11),e12) equal(op1(e10,e11),e13)**. % 0.71/0.88 466[0:Inp] || -> equal(op1(e10,e10),e10) equal(op1(e10,e10),e13)** equal(op1(e10,e10),e12) equal(op1(e10,e10),e11). % 0.71/0.88 475[0:Inp] || -> equal(op2(e20,op2(e20,e23)),e20) equal(op2(e21,op2(e21,e23)),e21) equal(op2(e22,op2(e22,e23)),e22) equal(op2(e23,op2(e23,e23)),e23)**. % 0.71/0.88 476[0:Inp] || -> equal(op2(e20,op2(e20,e22)),e20) equal(op2(e21,op2(e21,e22)),e21) equal(op2(e22,op2(e22,e22)),e22) equal(op2(e23,op2(e23,e22)),e23)**. % 0.71/0.88 477[0:Inp] || -> equal(op2(e20,op2(e20,e21)),e20) equal(op2(e21,op2(e21,e21)),e21) equal(op2(e22,op2(e22,e21)),e22) equal(op2(e23,op2(e23,e21)),e23)**. % 0.71/0.88 478[0:Inp] || -> equal(op2(e20,op2(e20,e20)),e20) equal(op2(e21,op2(e21,e20)),e21) equal(op2(e22,op2(e22,e20)),e22) equal(op2(e23,op2(e23,e20)),e23)**. % 0.71/0.88 479[0:Inp] || -> equal(op1(e10,op1(e10,e13)),e10) equal(op1(e11,op1(e11,e13)),e11) equal(op1(e12,op1(e12,e13)),e12) equal(op1(e13,op1(e13,e13)),e13)**. % 0.71/0.88 480[0:Inp] || -> equal(op1(e12,op1(e12,e12)),e12) equal(op1(e13,op1(e13,e12)),e13)** equal(op1(e11,op1(e11,e12)),e11) equal(op1(e10,op1(e10,e12)),e10). % 0.71/0.88 481[0:Inp] || -> equal(op1(e10,op1(e10,e11)),e10) equal(op1(e11,op1(e11,e11)),e11) equal(op1(e12,op1(e12,e11)),e12) equal(op1(e13,op1(e13,e11)),e13)**. % 0.71/0.88 488[0:Inp] || equal(h3(e12),e23) equal(op2(h3(e10),h3(e10)),h3(op1(e10,e10))) equal(op2(h3(e10),h3(e11)),h3(op1(e10,e11))) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),h3(e13)),h3(op1(e10,e13))) equal(op2(h3(e11),h3(e10)),h3(op1(e11,e10))) equal(op2(h3(e11),h3(e11)),h3(op1(e11,e11))) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),h3(e13)),h3(op1(e11,e13))) equal(op2(h3(e12),h3(e10)),h3(op1(e12,e10))) equal(op2(h3(e12),h3(e11)),h3(op1(e12,e11))) equal(op2(h3(e12),h3(e12)),h3(op1(e12,e12))) equal(op2(h3(e12),h3(e13)),h3(op1(e12,e13))) equal(op2(h3(e13),h3(e10)),h3(op1(e13,e10))) equal(op2(h3(e13),h3(e11)),h3(op1(e13,e11))) equal(op2(h3(e13),h3(e12)),h3(op1(e13,e12))) equal(op2(h3(e13),h3(e13)),h3(op1(e13,e13)))** SkC36 SkC37 SkC38 -> . % 0.71/0.88 507[0:Rew:31.0,70.0] || equal(e22,e22) -> SkC38*. % 0.71/0.88 508[0:Obv:507.0] || -> SkC38*. % 0.71/0.88 519[0:Rew:34.0,142.0] || -> equal(op2(e23,e21),e22)**. % 0.71/0.88 520[0:Rew:33.0,141.0] || -> equal(op1(e13,e11),e12)**. % 0.71/0.88 521[0:Rew:519.0,137.1] || SkC28* -> equal(e23,e22). % 0.71/0.88 522[0:MRR:521.1,12.0] || SkC28* -> . % 0.71/0.88 523[0:Rew:85.0,132.1] || SkC25 -> equal(h3(e11),e22)**. % 0.71/0.88 524[0:Rew:519.0,127.1] || SkC22* -> equal(e22,e21). % 0.71/0.88 525[0:MRR:524.1,10.0] || SkC22* -> . % 0.71/0.88 527[0:Rew:83.0,114.1] || SkC15 -> equal(h1(e11),e20)**. % 0.71/0.88 528[0:Rew:520.0,110.1] || SkC13* -> equal(e13,e12). % 0.71/0.88 529[0:MRR:528.1,6.0] || SkC13* -> . % 0.71/0.88 530[0:Rew:520.0,100.1] || SkC7* -> equal(e12,e11). % 0.71/0.88 531[0:MRR:530.1,4.0] || SkC7* -> . % 0.71/0.88 536[0:Rew:85.0,361.0] || -> equal(op2(e22,h3(e11)),h3(e12))**. % 0.71/0.88 537[0:Rew:84.0,360.0] || -> equal(op2(e21,h2(e11)),h2(e12))**. % 0.71/0.88 538[0:Rew:83.0,359.0] || -> equal(op2(e20,h1(e11)),h1(e12))**. % 0.71/0.88 545[0:Rew:84.0,348.0] || SkC27 equal(h2(e11),e20)** -> . % 0.71/0.88 546[0:Rew:83.0,347.0] || SkC27 equal(h1(e11),e20)** -> . % 0.71/0.88 552[0:Rew:523.1,341.0,85.0,341.0] || equal(e22,e22) SkC25* -> . % 0.71/0.88 553[0:Obv:552.0] || SkC25* -> . % 0.71/0.88 554[0:Rew:34.0,338.0] || equal(e21,e21) SkC24* -> . % 0.71/0.88 555[0:Obv:554.0] || SkC24* -> . % 0.71/0.88 558[0:Rew:84.0,332.0] || SkC23 equal(h2(e11),e20)** -> . % 0.71/0.88 559[0:Rew:83.0,331.0] || SkC23 equal(h1(e11),e20)** -> . % 0.71/0.88 561[0:Rew:85.0,325.0] || SkC21 equal(h3(e11),e22)** -> . % 0.71/0.88 563[0:Rew:83.0,323.0] || SkC21 equal(h1(e11),e22)** -> . % 0.71/0.88 564[0:Rew:34.0,322.0] || equal(e21,e21) SkC20* -> . % 0.71/0.88 565[0:Obv:564.0] || SkC20* -> . % 0.71/0.88 568[0:Rew:84.0,316.0] || SkC19 equal(h2(e11),e20)** -> . % 0.71/0.88 569[0:Rew:83.0,315.0] || SkC19 equal(h1(e11),e20)** -> . % 0.71/0.88 578[0:Rew:34.0,306.0] || equal(e21,e21) SkC16* -> . % 0.71/0.88 579[0:Obv:578.0] || SkC16* -> . % 0.71/0.88 583[0:Rew:527.1,299.0,83.0,299.0] || equal(e20,e20) SkC15* -> . % 0.71/0.88 584[0:Obv:583.0] || SkC15* -> . % 0.71/0.88 589[0:Rew:105.1,281.0] || equal(e12,e12) SkC10* -> . % 0.71/0.88 590[0:Obv:589.0] || SkC10* -> . % 0.71/0.88 591[0:Rew:33.0,278.0] || equal(e11,e11) SkC9* -> . % 0.71/0.88 592[0:Obv:591.0] || SkC9* -> . % 0.71/0.88 595[0:Rew:33.0,262.0] || equal(e11,e11) SkC5* -> . % 0.71/0.88 596[0:Obv:595.0] || SkC5* -> . % 0.71/0.88 600[0:Rew:33.0,246.0] || equal(e11,e11) SkC1* -> . % 0.71/0.88 601[0:Obv:600.0] || SkC1* -> . % 0.71/0.88 603[0:Rew:87.1,239.0] || equal(e10,e10) SkC0* -> . % 0.71/0.88 604[0:Obv:603.0] || SkC0* -> . % 0.71/0.88 605[0:Rew:34.0,238.0] || equal(op2(e23,e22),e21)** -> . % 0.71/0.88 607[0:Rew:519.0,236.0] || equal(op2(e23,e22),e22)** -> . % 0.71/0.88 608[0:MRR:134.1,607.0] || SkC26* -> . % 0.71/0.88 609[0:Rew:34.0,235.0] || equal(op2(e23,e20),e21)** -> . % 0.71/0.88 610[0:Rew:519.0,233.0] || equal(op2(e23,e20),e22)** -> . % 0.71/0.88 611[0:Rew:85.0,232.0] || equal(op2(e22,e23),h3(e11))** -> . % 0.71/0.88 612[0:Rew:85.0,230.0] || equal(op2(e22,e21),h3(e11))** -> . % 0.71/0.88 613[0:Rew:85.0,228.0] || equal(op2(e22,e20),h3(e11))** -> . % 0.71/0.88 614[0:Rew:84.0,225.0] || equal(op2(e21,e23),h2(e11))** -> . % 0.71/0.88 615[0:Rew:84.0,224.0] || equal(op2(e21,e22),h2(e11))** -> . % 0.71/0.88 617[0:Rew:83.0,217.0] || equal(op2(e20,e23),h1(e11))** -> . % 0.71/0.88 618[0:Rew:83.0,216.0] || equal(op2(e20,e22),h1(e11))** -> . % 0.71/0.88 619[0:Rew:83.0,215.0] || equal(op2(e20,e21),h1(e11))** -> . % 0.71/0.88 621[0:Rew:34.0,213.0] || equal(op2(e21,e23),e21)** -> . % 0.71/0.88 622[0:Rew:34.0,211.0] || equal(op2(e20,e23),e21)** -> . % 0.71/0.88 623[0:Rew:85.0,208.0] || equal(op2(e23,e22),h3(e11))** -> . % 0.71/0.88 626[0:Rew:519.0,202.0] || equal(op2(e22,e21),e22)** -> . % 0.71/0.88 627[0:Rew:519.0,201.0,84.0,201.0] || equal(h2(e11),e22)** -> . % 0.71/0.88 628[0:Rew:84.0,200.0] || equal(op2(e22,e21),h2(e11))** -> . % 0.71/0.88 629[0:Rew:519.0,199.0] || equal(op2(e20,e21),e22)** -> . % 0.71/0.88 630[0:Rew:84.0,197.0] || equal(op2(e20,e21),h2(e11))** -> . % 0.71/0.88 631[0:Rew:83.0,193.0] || equal(op2(e23,e20),h1(e11))** -> . % 0.71/0.88 632[0:Rew:83.0,192.0] || equal(op2(e22,e20),h1(e11))** -> . % 0.71/0.88 633[0:Rew:83.0,191.0] || equal(op2(e21,e20),h1(e11))** -> . % 0.71/0.88 634[0:Rew:33.0,190.0] || equal(op1(e13,e12),e11)** -> . % 0.71/0.88 636[0:Rew:520.0,188.0] || equal(op1(e13,e12),e12)** -> . % 0.71/0.88 637[0:MRR:107.1,636.0] || SkC11* -> . % 0.71/0.88 638[0:Rew:33.0,187.0] || equal(op1(e13,e10),e11)** -> . % 0.71/0.88 639[0:Rew:520.0,185.0] || equal(op1(e13,e10),e12)** -> . % 0.71/0.88 641[0:Rew:33.0,165.0] || equal(op1(e11,e13),e11)** -> . % 0.71/0.88 642[0:Rew:33.0,163.0] || equal(op1(e10,e13),e11)** -> . % 0.71/0.88 643[0:Rew:520.0,154.0] || equal(op1(e12,e11),e12)** -> . % 0.71/0.88 644[0:Rew:520.0,153.0] || equal(op1(e11,e11),e12)** -> . % 0.71/0.88 645[0:Rew:520.0,151.0] || equal(op1(e10,e11),e12)** -> . % 0.71/0.88 646[0:Rew:519.0,364.0,34.0,364.0] || -> equal(op2(e22,e23),e20)**. % 0.71/0.88 647[0:Rew:646.0,140.1] || SkC29* -> equal(e23,e20). % 0.71/0.88 648[0:Rew:646.0,611.0] || equal(h3(e11),e20)** -> . % 0.71/0.88 649[0:Rew:646.0,231.0] || equal(op2(e22,e21),e20)** -> . % 0.71/0.88 650[0:Rew:646.0,229.0] || equal(op2(e22,e20),e20)** -> . % 0.71/0.88 652[0:Rew:646.0,212.0] || equal(op2(e21,e23),e20)** -> . % 0.71/0.88 653[0:Rew:646.0,210.0] || equal(op2(e20,e23),e20)** -> . % 0.71/0.88 654[0:MRR:647.1,9.0] || SkC29* -> . % 0.71/0.88 655[0:MRR:118.1,650.0] || SkC17* -> . % 0.71/0.88 656[0:MRR:119.1,653.0] || SkC18* -> . % 0.71/0.88 657[0:Rew:520.0,363.0,33.0,363.0] || -> equal(op1(e12,e13),e10)**. % 0.71/0.88 658[0:Rew:657.0,113.1] || SkC14* -> equal(e13,e10). % 0.71/0.88 659[0:Rew:657.0,184.0] || equal(op1(e12,e12),e10)** -> . % 0.71/0.88 660[0:Rew:657.0,183.0] || equal(op1(e12,e11),e10)** -> . % 0.71/0.88 661[0:Rew:657.0,181.0] || equal(op1(e12,e10),e10)** -> . % 0.71/0.88 663[0:Rew:657.0,164.0] || equal(op1(e11,e13),e10)** -> . % 0.71/0.88 664[0:Rew:657.0,162.0] || equal(op1(e10,e13),e10)** -> . % 0.71/0.88 665[0:MRR:658.1,3.0] || SkC14* -> . % 0.71/0.88 666[0:MRR:91.1,661.0] || SkC2* -> . % 0.71/0.88 667[0:MRR:92.1,664.0] || SkC3* -> . % 0.71/0.88 671[0:Rew:536.0,367.0,85.0,367.0] || -> equal(op2(h3(e12),e22),h3(e10))**. % 0.71/0.88 673[0:Rew:538.0,365.0,83.0,365.0] || -> equal(op2(h1(e12),e20),h1(e10))**. % 0.71/0.88 674[0:Rew:34.0,369.0] || -> equal(e23,e21) SkC15* SkC16 SkC17 SkC18 SkC19 SkC20 SkC21 SkC22 SkC23 SkC24 SkC25 SkC26 SkC27 SkC28 SkC29. % 0.71/0.88 675[0:MRR:674.0,674.1,674.2,674.3,674.4,674.6,674.8,674.10,674.11,674.12,674.14,674.15,11.0,584.0,579.0,655.0,656.0,565.0,525.0,555.0,553.0,608.0,522.0,654.0] || -> SkC27 SkC23 SkC21 SkC19*. % 0.71/0.88 676[0:Rew:33.0,370.0] || -> equal(e13,e11) SkC0* SkC1 SkC2 SkC3 SkC4 SkC5 SkC6 SkC7 SkC8 SkC9 SkC10 SkC11 SkC12 SkC13 SkC14. % 0.71/0.88 677[0:MRR:676.0,676.1,676.2,676.3,676.4,676.6,676.8,676.10,676.11,676.12,676.14,676.15,5.0,604.0,601.0,666.0,667.0,596.0,531.0,592.0,590.0,637.0,529.0,665.0] || -> SkC12 SkC8 SkC6 SkC4*. % 0.71/0.88 678[0:Rew:34.0,371.3,646.0,371.2] || -> equal(op2(e20,e23),e23) equal(op2(e21,e23),e23)** equal(e23,e20) equal(e23,e21). % 0.71/0.88 679[0:MRR:678.2,678.3,9.0,11.0] || -> equal(op2(e21,e23),e23)** equal(op2(e20,e23),e23). % 0.71/0.88 682[0:Rew:34.0,373.3,646.0,373.2] || -> equal(op2(e20,e23),e22) equal(op2(e21,e23),e22)** equal(e22,e20) equal(e22,e21). % 0.71/0.88 683[0:MRR:682.2,682.3,8.0,10.0] || -> equal(op2(e21,e23),e22)** equal(op2(e20,e23),e22). % 0.71/0.88 686[0:Rew:85.0,379.2] || -> equal(h3(e11),e23) equal(op2(e23,e22),e23)** equal(op2(e21,e22),e23) equal(op2(e20,e22),e23). % 0.71/0.88 689[0:Rew:85.0,381.2] || -> equal(op2(e20,e22),e22) equal(op2(e21,e22),e22) equal(h3(e11),e22) equal(op2(e23,e22),e22)**. % 0.71/0.88 690[0:MRR:689.3,607.0] || -> equal(h3(e11),e22) equal(op2(e21,e22),e22)** equal(op2(e20,e22),e22). % 0.71/0.88 691[0:Rew:646.0,382.3,85.0,382.2] || -> equal(op2(e22,e20),e22) equal(op2(e22,e21),e22)** equal(h3(e11),e22) equal(e22,e20). % 0.71/0.88 692[0:MRR:691.1,691.3,626.0,8.0] || -> equal(h3(e11),e22) equal(op2(e22,e20),e22)**. % 0.71/0.88 695[0:Rew:646.0,384.3,85.0,384.2] || -> equal(op2(e22,e20),e21) equal(op2(e22,e21),e21)** equal(h3(e11),e21) equal(e21,e20). % 0.71/0.88 696[0:MRR:695.3,7.0] || -> equal(h3(e11),e21) equal(op2(e22,e21),e21)** equal(op2(e22,e20),e21). % 0.71/0.88 697[0:Rew:85.0,385.2] || -> equal(op2(e20,e22),e20) equal(op2(e21,e22),e20) equal(h3(e11),e20) equal(op2(e23,e22),e20)**. % 0.71/0.88 698[0:MRR:697.2,648.0] || -> equal(op2(e20,e22),e20) equal(op2(e23,e22),e20)** equal(op2(e21,e22),e20). % 0.71/0.88 699[0:Rew:519.0,387.3,84.0,387.1] || -> equal(op2(e20,e21),e23) equal(h2(e11),e23) equal(op2(e22,e21),e23)** equal(e23,e22). % 0.71/0.88 700[0:MRR:699.3,12.0] || -> equal(h2(e11),e23) equal(op2(e22,e21),e23)** equal(op2(e20,e21),e23). % 0.71/0.88 702[0:Rew:84.0,390.1] || -> equal(op2(e21,e20),e22) equal(h2(e11),e22) equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)**. % 0.71/0.88 703[0:MRR:702.1,627.0] || -> equal(op2(e21,e22),e22) equal(op2(e21,e23),e22)** equal(op2(e21,e20),e22). % 0.71/0.88 708[0:Rew:519.0,393.3,84.0,393.1] || -> equal(op2(e20,e21),e20) equal(h2(e11),e20) equal(op2(e22,e21),e20)** equal(e22,e20). % 0.71/0.88 709[0:MRR:708.2,708.3,649.0,8.0] || -> equal(h2(e11),e20) equal(op2(e20,e21),e20)**. % 0.71/0.88 710[0:Rew:84.0,394.1] || -> equal(op2(e21,e20),e20) equal(h2(e11),e20) equal(op2(e21,e22),e20) equal(op2(e21,e23),e20)**. % 0.71/0.88 711[0:MRR:710.3,652.0] || -> equal(h2(e11),e20) equal(op2(e21,e20),e20) equal(op2(e21,e22),e20)**. % 0.71/0.88 712[0:Rew:83.0,395.0] || -> equal(h1(e11),e23) equal(op2(e23,e20),e23)** equal(op2(e22,e20),e23) equal(op2(e21,e20),e23). % 0.71/0.88 714[0:Rew:83.0,397.0] || -> equal(h1(e11),e22) equal(op2(e21,e20),e22) equal(op2(e22,e20),e22) equal(op2(e23,e20),e22)**. % 0.71/0.88 715[0:MRR:714.3,610.0] || -> equal(h1(e11),e22) equal(op2(e22,e20),e22)** equal(op2(e21,e20),e22). % 0.71/0.88 718[0:Rew:83.0,399.0] || -> equal(h1(e11),e21) equal(op2(e21,e20),e21) equal(op2(e22,e20),e21) equal(op2(e23,e20),e21)**. % 0.71/0.88 719[0:MRR:718.3,609.0] || -> equal(h1(e11),e21) equal(op2(e21,e20),e21) equal(op2(e22,e20),e21)**. % 0.71/0.88 720[0:Rew:83.0,400.0] || -> equal(h1(e11),e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21) equal(op2(e20,e23),e21)**. % 0.71/0.88 721[0:MRR:720.3,622.0] || -> equal(h1(e11),e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21)**. % 0.71/0.88 722[0:Rew:83.0,401.0] || -> equal(h1(e11),e20) equal(op2(e21,e20),e20) equal(op2(e22,e20),e20) equal(op2(e23,e20),e20)**. % 0.71/0.88 723[0:MRR:722.2,650.0] || -> equal(h1(e11),e20) equal(op2(e23,e20),e20)** equal(op2(e21,e20),e20). % 0.71/0.88 726[0:MRR:404.1,404.2,605.0,607.0] || -> equal(op2(e23,e22),e23)** equal(op2(e23,e22),e20). % 0.71/0.88 727[0:MRR:406.1,406.2,609.0,610.0] || -> equal(op2(e23,e20),e23)** equal(op2(e23,e20),e20). % 0.71/0.88 728[0:Rew:85.0,408.3,85.0,408.2,85.0,408.1,85.0,408.0] || -> equal(h3(e11),e20) equal(h3(e11),e21) equal(h3(e11),e22) equal(h3(e11),e23)**. % 0.71/0.88 729[0:MRR:728.0,648.0] || -> equal(h3(e11),e23)** equal(h3(e11),e22) equal(h3(e11),e21). % 0.71/0.88 730[0:MRR:409.0,409.2,649.0,626.0] || -> equal(op2(e22,e21),e21) equal(op2(e22,e21),e23)**. % 0.71/0.88 731[0:MRR:410.0,650.0] || -> equal(op2(e22,e20),e22) equal(op2(e22,e20),e23)** equal(op2(e22,e20),e21). % 0.71/0.88 732[0:MRR:411.0,411.1,652.0,621.0] || -> equal(op2(e21,e23),e23)** equal(op2(e21,e23),e22). % 0.71/0.88 733[0:Rew:84.0,413.3,84.0,413.2,84.0,413.1,84.0,413.0] || -> equal(h2(e11),e20) equal(h2(e11),e21) equal(h2(e11),e22) equal(h2(e11),e23)**. % 0.71/0.88 734[0:MRR:733.2,627.0] || -> equal(h2(e11),e23)** equal(h2(e11),e21) equal(h2(e11),e20). % 0.71/0.88 735[0:MRR:415.0,415.1,653.0,622.0] || -> equal(op2(e20,e23),e23)** equal(op2(e20,e23),e22). % 0.71/0.88 736[0:MRR:417.2,629.0] || -> equal(op2(e20,e21),e21) equal(op2(e20,e21),e20) equal(op2(e20,e21),e23)**. % 0.71/0.88 737[0:Rew:83.0,418.3,83.0,418.2,83.0,418.1,83.0,418.0] || -> equal(h1(e11),e23)** equal(h1(e11),e22) equal(h1(e11),e21) equal(h1(e11),e20). % 0.71/0.88 738[0:Rew:33.0,419.3,657.0,419.2] || -> equal(op1(e10,e13),e13) equal(op1(e11,e13),e13)** equal(e13,e10) equal(e13,e11). % 0.71/0.88 739[0:MRR:738.2,738.3,3.0,5.0] || -> equal(op1(e11,e13),e13)** equal(op1(e10,e13),e13). % 0.71/0.88 740[0:Rew:33.0,420.3,520.0,420.1] || -> equal(op1(e13,e10),e13) equal(e13,e12) equal(op1(e13,e12),e13)** equal(e13,e11). % 0.71/0.88 741[0:MRR:740.1,740.3,6.0,5.0] || -> equal(op1(e13,e12),e13)** equal(op1(e13,e10),e13). % 0.71/0.88 742[0:Rew:33.0,421.3,657.0,421.2] || -> equal(op1(e10,e13),e12) equal(op1(e11,e13),e12)** equal(e12,e10) equal(e12,e11). % 0.71/0.88 743[0:MRR:742.2,742.3,2.0,4.0] || -> equal(op1(e11,e13),e12)** equal(op1(e10,e13),e12). % 0.71/0.88 744[0:Rew:33.0,426.3,520.0,426.1] || -> equal(op1(e13,e10),e10) equal(e12,e10) equal(op1(e13,e12),e10)** equal(e11,e10). % 0.71/0.88 745[0:MRR:744.1,744.3,2.0,1.0] || -> equal(op1(e13,e10),e10) equal(op1(e13,e12),e10)**. % 0.71/0.88 746[0:Rew:657.0,428.3] || -> equal(op1(e12,e10),e13) equal(op1(e12,e11),e13) equal(op1(e12,e12),e13)** equal(e13,e10). % 0.71/0.88 747[0:MRR:746.3,3.0] || -> equal(op1(e12,e12),e13)** equal(op1(e12,e11),e13) equal(op1(e12,e10),e13). % 0.71/0.88 748[0:MRR:429.3,636.0] || -> equal(op1(e12,e12),e12)** equal(op1(e11,e12),e12) equal(op1(e10,e12),e12). % 0.71/0.88 749[0:Rew:657.0,430.3] || -> equal(op1(e12,e10),e12) equal(op1(e12,e11),e12) equal(op1(e12,e12),e12)** equal(e12,e10). % 0.71/0.88 750[0:MRR:749.1,749.3,643.0,2.0] || -> equal(op1(e12,e12),e12)** equal(op1(e12,e10),e12). % 0.71/0.88 752[0:Rew:657.0,432.3] || -> equal(op1(e12,e10),e11) equal(op1(e12,e11),e11) equal(op1(e12,e12),e11)** equal(e11,e10). % 0.71/0.88 753[0:MRR:752.3,1.0] || -> equal(op1(e12,e12),e11)** equal(op1(e12,e11),e11) equal(op1(e12,e10),e11). % 0.71/0.88 754[0:MRR:433.2,659.0] || -> equal(op1(e10,e12),e10) equal(op1(e13,e12),e10)** equal(op1(e11,e12),e10). % 0.71/0.88 758[0:Rew:520.0,439.3] || -> equal(op1(e10,e11),e11) equal(op1(e11,e11),e11) equal(op1(e12,e11),e11)** equal(e12,e11). % 0.71/0.88 759[0:MRR:758.3,4.0] || -> equal(op1(e11,e11),e11) equal(op1(e12,e11),e11)** equal(op1(e10,e11),e11). % 0.71/0.88 760[0:MRR:440.3,641.0] || -> equal(op1(e11,e11),e11) equal(op1(e11,e12),e11)** equal(op1(e11,e10),e11). % 0.71/0.88 761[0:Rew:520.0,441.3] || -> equal(op1(e10,e11),e10) equal(op1(e11,e11),e10) equal(op1(e12,e11),e10)** equal(e12,e10). % 0.71/0.88 762[0:MRR:761.2,761.3,660.0,2.0] || -> equal(op1(e11,e11),e10)** equal(op1(e10,e11),e10). % 0.71/0.88 763[0:MRR:442.3,663.0] || -> equal(op1(e11,e11),e10) equal(op1(e11,e10),e10) equal(op1(e11,e12),e10)**. % 0.71/0.88 764[0:MRR:445.3,639.0] || -> equal(op1(e12,e10),e12)** equal(op1(e10,e10),e12) equal(op1(e11,e10),e12). % 0.71/0.88 768[0:MRR:449.2,661.0] || -> equal(op1(e10,e10),e10) equal(op1(e13,e10),e10)** equal(op1(e11,e10),e10). % 0.71/0.88 769[0:MRR:450.3,664.0] || -> equal(op1(e10,e10),e10) equal(op1(e10,e12),e10)** equal(op1(e10,e11),e10). % 0.71/0.88 770[0:MRR:452.1,452.2,634.0,636.0] || -> equal(op1(e13,e12),e13)** equal(op1(e13,e12),e10). % 0.71/0.88 771[0:MRR:454.1,454.2,638.0,639.0] || -> equal(op1(e13,e10),e13)** equal(op1(e13,e10),e10). % 0.71/0.88 772[0:MRR:456.0,659.0] || -> equal(op1(e12,e12),e12) equal(op1(e12,e12),e13)** equal(op1(e12,e12),e11). % 0.71/0.88 773[0:MRR:457.0,457.2,660.0,643.0] || -> equal(op1(e12,e11),e11) equal(op1(e12,e11),e13)**. % 0.71/0.88 774[0:MRR:458.0,661.0] || -> equal(op1(e12,e10),e12) equal(op1(e12,e10),e13)** equal(op1(e12,e10),e11). % 0.71/0.88 775[0:MRR:459.0,459.1,663.0,641.0] || -> equal(op1(e11,e13),e13)** equal(op1(e11,e13),e12). % 0.71/0.88 776[0:MRR:461.2,644.0] || -> equal(op1(e11,e11),e11) equal(op1(e11,e11),e13)** equal(op1(e11,e11),e10). % 0.71/0.88 777[0:MRR:463.0,463.1,664.0,642.0] || -> equal(op1(e10,e13),e13)** equal(op1(e10,e13),e12). % 0.71/0.88 778[0:MRR:465.2,645.0] || -> equal(op1(e10,e11),e11) equal(op1(e10,e11),e10) equal(op1(e10,e11),e13)**. % 0.71/0.88 779[0:Rew:519.0,475.3,34.0,475.3,646.0,475.2] || -> equal(op2(e20,op2(e20,e23)),e20) equal(op2(e21,op2(e21,e23)),e21)** equal(op2(e22,e20),e22) equal(e23,e22). % 0.71/0.88 780[0:MRR:779.3,12.0] || -> equal(op2(e22,e20),e22) equal(op2(e21,op2(e21,e23)),e21)** equal(op2(e20,op2(e20,e23)),e20). % 0.71/0.88 781[0:Rew:536.0,476.2,85.0,476.2] || -> equal(h3(e12),e22) equal(op2(e23,op2(e23,e22)),e23)** equal(op2(e21,op2(e21,e22)),e21) equal(op2(e20,op2(e20,e22)),e20). % 0.71/0.88 782[0:Rew:519.0,477.3,537.0,477.1,84.0,477.1] || -> equal(h2(e12),e21) equal(op2(e23,e22),e23) equal(op2(e22,op2(e22,e21)),e22)** equal(op2(e20,op2(e20,e21)),e20). % 0.71/0.88 783[0:Rew:538.0,478.0,83.0,478.0] || -> equal(h1(e12),e20) equal(op2(e23,op2(e23,e20)),e23)** equal(op2(e22,op2(e22,e20)),e22) equal(op2(e21,op2(e21,e20)),e21). % 0.71/0.88 784[0:Rew:520.0,479.3,33.0,479.3,657.0,479.2] || -> equal(op1(e10,op1(e10,e13)),e10) equal(op1(e11,op1(e11,e13)),e11)** equal(op1(e12,e10),e12) equal(e13,e12). % 0.71/0.88 785[0:MRR:784.3,6.0] || -> equal(op1(e12,e10),e12) equal(op1(e11,op1(e11,e13)),e11)** equal(op1(e10,op1(e10,e13)),e10). % 0.71/0.88 786[0:Rew:520.0,481.3] || -> equal(op1(e13,e12),e13) equal(op1(e11,op1(e11,e11)),e11) equal(op1(e12,op1(e12,e11)),e12)** equal(op1(e10,op1(e10,e11)),e10). % 0.71/0.88 798[0:Rew:85.0,488.16,31.0,488.16,33.0,488.16,31.0,488.15,536.0,488.14,31.0,488.14,520.0,488.14,31.0,488.13,671.0,488.12,31.0,488.12,657.0,488.12,31.0,488.8,31.0,488.4] || equal(h3(e12),e23) equal(op2(h3(e10),h3(e10)),h3(op1(e10,e10))) equal(op2(h3(e10),h3(e11)),h3(op1(e10,e11))) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),e22),h3(op1(e10,e13))) equal(op2(h3(e11),h3(e10)),h3(op1(e11,e10))) equal(op2(h3(e11),h3(e11)),h3(op1(e11,e11))) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),e22),h3(op1(e11,e13))) equal(op2(h3(e12),h3(e10)),h3(op1(e12,e10))) equal(op2(h3(e12),h3(e11)),h3(op1(e12,e11))) equal(op2(h3(e12),h3(e12)),h3(op1(e12,e12)))** equal(h3(e10),h3(e10)) equal(op2(e22,h3(e10)),h3(op1(e13,e10))) equal(h3(e12),h3(e12)) equal(op2(e22,h3(e12)),h3(op1(e13,e12))) equal(h3(e11),h3(e11)) SkC36 SkC37 SkC38 -> . % 0.71/0.88 799[0:Obv:798.16] || equal(h3(e12),e23) equal(op2(h3(e10),h3(e10)),h3(op1(e10,e10))) equal(op2(h3(e10),h3(e11)),h3(op1(e10,e11))) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),e22),h3(op1(e10,e13))) equal(op2(h3(e11),h3(e10)),h3(op1(e11,e10))) equal(op2(h3(e11),h3(e11)),h3(op1(e11,e11))) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),e22),h3(op1(e11,e13))) equal(op2(h3(e12),h3(e10)),h3(op1(e12,e10))) equal(op2(h3(e12),h3(e11)),h3(op1(e12,e11))) equal(op2(h3(e12),h3(e12)),h3(op1(e12,e12)))** equal(op2(e22,h3(e10)),h3(op1(e13,e10))) equal(op2(e22,h3(e12)),h3(op1(e13,e12))) SkC36 SkC37 SkC38 -> . % 0.71/0.88 800[0:MRR:799.16,508.0] || SkC37 SkC36 equal(h3(e12),e23) equal(op2(e22,h3(e12)),h3(op1(e13,e12))) equal(op2(e22,h3(e10)),h3(op1(e13,e10))) equal(op2(h3(e11),e22),h3(op1(e11,e13))) equal(op2(h3(e10),e22),h3(op1(e10,e13))) equal(op2(h3(e12),h3(e12)),h3(op1(e12,e12)))** equal(op2(h3(e11),h3(e11)),h3(op1(e11,e11))) equal(op2(h3(e10),h3(e10)),h3(op1(e10,e10))) equal(op2(h3(e12),h3(e11)),h3(op1(e12,e11))) equal(op2(h3(e12),h3(e10)),h3(op1(e12,e10))) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),h3(e10)),h3(op1(e11,e10))) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),h3(e11)),h3(op1(e10,e11))) -> . % 0.71/0.88 829[1:Spt:466.0] || -> equal(op1(e10,e10),e10)**. % 0.71/0.88 830[1:Rew:829.0,255.1] || SkC4* equal(e10,e10) -> . % 0.71/0.88 831[1:Rew:829.0,271.1] || SkC8* equal(e10,e10) -> . % 0.71/0.88 832[1:Rew:829.0,287.1] || SkC12* equal(e10,e10) -> . % 0.71/0.88 851[1:Rew:829.0,167.0] || equal(op1(e10,e11),e10)** -> . % 0.71/0.88 852[1:Rew:829.0,145.0] || equal(op1(e13,e10),e10)** -> . % 0.71/0.89 857[1:Obv:830.1] || SkC4* -> . % 0.71/0.89 858[1:MRR:677.3,857.0] || -> SkC12 SkC8 SkC6*. % 0.71/0.89 859[1:Obv:831.1] || SkC8* -> . % 0.71/0.89 860[1:MRR:858.1,859.0] || -> SkC12 SkC6*. % 0.71/0.89 861[1:Obv:832.1] || SkC12* -> . % 0.71/0.89 862[1:MRR:860.0,861.0] || -> SkC6*. % 0.71/0.89 863[1:MRR:98.0,862.0] || -> equal(op1(e12,e11),e11)**. % 0.71/0.89 864[1:MRR:97.0,862.0] || -> equal(op1(e11,e12),e11)**. % 0.71/0.89 873[1:Rew:863.0,150.0] || equal(op1(e10,e11),e11)** -> . % 0.71/0.89 874[1:Rew:863.0,786.2] || -> equal(op1(e13,e12),e13) equal(op1(e11,op1(e11,e11)),e11)** equal(op1(e12,e11),e12) equal(op1(e10,op1(e10,e11)),e10). % 0.71/0.89 883[1:Rew:864.0,174.0] || equal(op1(e11,e10),e11)** -> . % 0.71/0.89 889[1:MRR:762.1,851.0] || -> equal(op1(e11,e11),e10)**. % 0.71/0.89 890[1:MRR:778.1,851.0] || -> equal(op1(e10,e11),e11) equal(op1(e10,e11),e13)**. % 0.71/0.89 895[1:MRR:745.0,852.0] || -> equal(op1(e13,e12),e10)**. % 0.71/0.89 920[1:MRR:890.0,873.0] || -> equal(op1(e10,e11),e13)**. % 0.71/0.89 922[1:Rew:920.0,171.0] || equal(op1(e10,e13),e13)** -> . % 0.71/0.89 927[1:MRR:777.0,922.0] || -> equal(op1(e10,e13),e12)**. % 0.71/0.89 953[1:Rew:927.0,874.3,920.0,874.3,863.0,874.2,889.0,874.1,895.0,874.0] || -> equal(e13,e10) equal(op1(e11,e10),e11)** equal(e12,e11) equal(e12,e10). % 0.71/0.89 954[1:MRR:953.0,953.1,953.2,953.3,3.0,883.0,4.0,2.0] || -> . % 0.71/0.89 966[1:Spt:954.0,466.0,829.0] || equal(op1(e10,e10),e10)** -> . % 0.71/0.89 967[1:Spt:954.0,466.1,466.2,466.3] || -> equal(op1(e10,e10),e13)** equal(op1(e10,e10),e12) equal(op1(e10,e10),e11). % 0.71/0.89 968[1:MRR:768.0,966.0] || -> equal(op1(e13,e10),e10)** equal(op1(e11,e10),e10). % 0.71/0.89 969[1:MRR:769.0,966.0] || -> equal(op1(e10,e12),e10)** equal(op1(e10,e11),e10). % 0.71/0.89 970[2:Spt:967.0] || -> equal(op1(e10,e10),e13)**. % 0.71/0.89 973[2:Rew:970.0,144.0] || equal(op1(e12,e10),e13)** -> . % 0.71/0.89 974[2:Rew:970.0,145.0] || equal(op1(e13,e10),e13)** -> . % 0.71/0.89 977[2:Rew:970.0,169.0] || equal(op1(e10,e13),e13)** -> . % 0.71/0.89 996[2:MRR:747.2,973.0] || -> equal(op1(e12,e12),e13)** equal(op1(e12,e11),e13). % 0.71/0.89 997[2:MRR:774.1,973.0] || -> equal(op1(e12,e10),e12)** equal(op1(e12,e10),e11). % 0.71/0.89 998[2:MRR:108.1,974.0] || SkC12* -> . % 0.71/0.89 1000[2:MRR:741.1,974.0] || -> equal(op1(e13,e12),e13)**. % 0.71/0.89 1001[2:MRR:677.0,998.0] || -> SkC8 SkC6 SkC4*. % 0.71/0.89 1012[2:Rew:1000.0,160.0] || equal(op1(e12,e12),e13)** -> . % 0.71/0.89 1014[2:Rew:1000.0,480.1] || -> equal(op1(e12,op1(e12,e12)),e12)** equal(op1(e13,e13),e13) equal(op1(e11,op1(e11,e12)),e11) equal(op1(e10,op1(e10,e12)),e10). % 0.71/0.89 1018[2:MRR:777.0,977.0] || -> equal(op1(e10,e13),e12)**. % 0.71/0.89 1024[2:Rew:1018.0,172.0] || equal(op1(e10,e12),e12)** -> . % 0.71/0.89 1036[2:MRR:772.1,1012.0] || -> equal(op1(e12,e12),e12)** equal(op1(e12,e12),e11). % 0.71/0.89 1038[2:MRR:102.1,1024.0] || SkC8* -> . % 0.71/0.89 1039[2:MRR:748.2,1024.0] || -> equal(op1(e12,e12),e12)** equal(op1(e11,e12),e12). % 0.71/0.89 1040[2:MRR:1001.0,1038.0] || -> SkC6 SkC4*. % 0.71/0.89 1042[2:MRR:996.0,1012.0] || -> equal(op1(e12,e11),e13)**. % 0.71/0.89 1047[2:Rew:1042.0,98.1] || SkC6* -> equal(e13,e11). % 0.71/0.89 1052[2:MRR:1047.1,5.0] || SkC6* -> . % 0.71/0.89 1053[2:MRR:1040.0,1052.0] || -> SkC4*. % 0.71/0.89 1054[2:MRR:95.0,1053.0] || -> equal(op1(e10,e11),e11)**. % 0.71/0.89 1055[2:MRR:94.0,1053.0] || -> equal(op1(e11,e10),e11)**. % 0.71/0.89 1060[2:Rew:1054.0,969.1] || -> equal(op1(e10,e12),e10)** equal(e11,e10). % 0.71/0.89 1065[2:Rew:1055.0,146.0] || equal(op1(e12,e10),e11)** -> . % 0.71/0.89 1070[2:MRR:1060.1,1.0] || -> equal(op1(e10,e12),e10)**. % 0.71/0.89 1077[2:MRR:997.1,1065.0] || -> equal(op1(e12,e10),e12)**. % 0.71/0.89 1079[2:Rew:1077.0,180.0] || equal(op1(e12,e12),e12)** -> . % 0.71/0.89 1083[2:MRR:1036.0,1079.0] || -> equal(op1(e12,e12),e11)**. % 0.71/0.89 1088[2:Rew:1083.0,1039.0] || -> equal(e12,e11) equal(op1(e11,e12),e12)**. % 0.71/0.89 1089[2:MRR:1088.0,4.0] || -> equal(op1(e11,e12),e12)**. % 0.71/0.89 1097[2:Rew:970.0,1014.3,1070.0,1014.3,1089.0,1014.2,1089.0,1014.2,33.0,1014.1,1042.0,1014.0,1083.0,1014.0] || -> equal(e13,e12)** equal(e13,e11) equal(e12,e11) equal(e13,e10). % 0.71/0.89 1098[2:MRR:1097.0,1097.1,1097.2,1097.3,6.0,5.0,4.0,3.0] || -> . % 0.71/0.89 1109[2:Spt:1098.0,967.0,970.0] || equal(op1(e10,e10),e13)** -> . % 0.71/0.89 1110[2:Spt:1098.0,967.1,967.2] || -> equal(op1(e10,e10),e12)** equal(op1(e10,e10),e11). % 0.71/0.89 1112[2:MRR:443.1,1109.0] || -> equal(op1(e13,e10),e13)** equal(op1(e12,e10),e13) equal(op1(e11,e10),e13). % 0.71/0.89 1113[3:Spt:1110.0] || -> equal(op1(e10,e10),e12)**. % 0.71/0.89 1116[3:Rew:1113.0,263.1] || SkC6* equal(e12,e12) -> . % 0.71/0.89 1117[3:Rew:1113.0,169.0] || equal(op1(e10,e13),e12)** -> . % 0.71/0.89 1118[3:Rew:1113.0,168.0] || equal(op1(e10,e12),e12)** -> . % 0.71/0.89 1121[3:Rew:1113.0,144.0] || equal(op1(e12,e10),e12)** -> . % 0.71/0.89 1136[3:Obv:1116.1] || SkC6* -> . % 0.71/0.89 1137[3:MRR:677.2,1136.0] || -> SkC12 SkC8 SkC4*. % 0.71/0.89 1138[3:MRR:777.1,1117.0] || -> equal(op1(e10,e13),e13)**. % 0.71/0.89 1139[3:MRR:743.1,1117.0] || -> equal(op1(e11,e13),e12)**. % 0.71/0.89 1142[3:Rew:1138.0,172.0] || equal(op1(e10,e12),e13)** -> . % 0.71/0.89 1145[3:Rew:1138.0,785.2] || -> equal(op1(e12,e10),e12) equal(op1(e11,op1(e11,e13)),e11)** equal(op1(e10,e13),e10). % 0.71/0.89 1153[3:MRR:102.1,1118.0] || SkC8* -> . % 0.71/0.89 1155[3:MRR:464.0,1118.0] || -> equal(op1(e10,e12),e10) equal(op1(e10,e12),e13)** equal(op1(e10,e12),e11). % 0.71/0.89 1156[3:MRR:1137.1,1153.0] || -> SkC12 SkC4*. % 0.71/0.89 1157[3:MRR:750.1,1121.0] || -> equal(op1(e12,e12),e12)**. % 0.71/0.89 1165[3:Rew:1157.0,427.1] || -> equal(op1(e13,e12),e13)** equal(e13,e12) equal(op1(e11,e12),e13) equal(op1(e10,e12),e13). % 0.71/0.89 1180[3:MRR:1155.1,1142.0] || -> equal(op1(e10,e12),e10) equal(op1(e10,e12),e11)**. % 0.71/0.89 1181[3:Rew:1138.0,1145.2,1139.0,1145.1] || -> equal(op1(e12,e10),e12)** equal(op1(e11,e12),e11) equal(e13,e10). % 0.71/0.89 1182[3:MRR:1181.0,1181.2,1121.0,3.0] || -> equal(op1(e11,e12),e11)**. % 0.71/0.89 1184[3:Rew:1182.0,174.0] || equal(op1(e11,e10),e11)** -> . % 0.71/0.89 1185[3:Rew:1182.0,155.0] || equal(op1(e10,e12),e11)** -> . % 0.71/0.89 1190[3:MRR:94.1,1184.0] || SkC4* -> . % 0.71/0.89 1193[3:MRR:1156.1,1190.0] || -> SkC12*. % 0.71/0.89 1194[3:MRR:108.0,1193.0] || -> equal(op1(e13,e10),e13)**. % 0.71/0.89 1206[3:Rew:1194.0,186.0] || equal(op1(e13,e12),e13)** -> . % 0.71/0.89 1210[3:MRR:1180.1,1185.0] || -> equal(op1(e10,e12),e10)**. % 0.71/0.89 1230[3:MRR:770.0,1206.0] || -> equal(op1(e13,e12),e10)**. % 0.71/0.89 1247[3:Rew:1210.0,1165.3,1182.0,1165.2,1230.0,1165.0] || -> equal(e13,e10) equal(e13,e12)** equal(e13,e11) equal(e13,e10). % 0.71/0.89 1248[3:Obv:1247.0] || -> equal(e13,e12)** equal(e13,e11) equal(e13,e10). % 0.71/0.89 1249[3:MRR:1248.0,1248.1,1248.2,6.0,5.0,3.0] || -> . % 0.71/0.89 1262[3:Spt:1249.0,1110.0,1113.0] || equal(op1(e10,e10),e12)** -> . % 0.71/0.89 1263[3:Spt:1249.0,1110.1] || -> equal(op1(e10,e10),e11)**. % 0.71/0.89 1267[3:Rew:1263.0,143.0] || equal(op1(e11,e10),e11)** -> . % 0.71/0.89 1268[3:MRR:94.1,1267.0] || SkC4* -> . % 0.71/0.89 1269[3:MRR:677.3,1268.0] || -> SkC12 SkC8 SkC6*. % 0.71/0.89 1270[3:Rew:1263.0,144.0] || equal(op1(e12,e10),e11)** -> . % 0.71/0.89 1272[3:Rew:1263.0,167.0] || equal(op1(e10,e11),e11)** -> . % 0.71/0.89 1273[3:Rew:1263.0,168.0] || equal(op1(e10,e12),e11)** -> . % 0.71/0.89 1276[3:Rew:1263.0,764.1] || -> equal(op1(e12,e10),e12)** equal(e12,e11) equal(op1(e11,e10),e12). % 0.71/0.89 1277[3:MRR:1276.1,4.0] || -> equal(op1(e12,e10),e12)** equal(op1(e11,e10),e12). % 0.71/0.89 1281[3:MRR:753.2,1270.0] || -> equal(op1(e12,e12),e11)** equal(op1(e12,e11),e11). % 0.71/0.89 1283[3:MRR:778.0,1272.0] || -> equal(op1(e10,e11),e10) equal(op1(e10,e11),e13)**. % 0.71/0.89 1284[3:MRR:760.2,1267.0] || -> equal(op1(e11,e11),e11) equal(op1(e11,e12),e11)**. % 0.71/0.89 1285[3:MRR:759.2,1272.0] || -> equal(op1(e11,e11),e11) equal(op1(e12,e11),e11)**. % 0.71/0.89 1286[3:MRR:462.0,1267.0] || -> equal(op1(e11,e10),e10) equal(op1(e11,e10),e13)** equal(op1(e11,e10),e12). % 0.71/0.89 1287[3:MRR:464.3,1273.0] || -> equal(op1(e10,e12),e12) equal(op1(e10,e12),e10) equal(op1(e10,e12),e13)**. % 0.71/0.89 1290[3:Rew:1263.0,800.9] || SkC37 SkC36 equal(h3(e12),e23) equal(op2(e22,h3(e12)),h3(op1(e13,e12))) equal(op2(e22,h3(e10)),h3(op1(e13,e10))) equal(op2(h3(e11),e22),h3(op1(e11,e13))) equal(op2(h3(e10),e22),h3(op1(e10,e13))) equal(op2(h3(e12),h3(e12)),h3(op1(e12,e12)))** equal(op2(h3(e11),h3(e11)),h3(op1(e11,e11))) equal(op2(h3(e10),h3(e10)),h3(e11)) equal(op2(h3(e12),h3(e11)),h3(op1(e12,e11))) equal(op2(h3(e12),h3(e10)),h3(op1(e12,e10))) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),h3(e10)),h3(op1(e11,e10))) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),h3(e11)),h3(op1(e10,e11))) -> . % 0.71/0.89 1300[4:Spt:763.2] || -> equal(op1(e11,e12),e10)**. % 0.71/0.89 1301[4:Rew:1300.0,1284.1] || -> equal(op1(e11,e11),e11)** equal(e11,e10). % 0.71/0.89 1303[4:Rew:1300.0,97.1] || SkC6* -> equal(e11,e10). % 0.71/0.89 1308[4:Rew:1300.0,174.0] || equal(op1(e11,e10),e10)** -> . % 0.71/0.89 1309[4:Rew:1300.0,159.0] || equal(op1(e13,e12),e10)** -> . % 0.71/0.89 1314[4:Rew:1300.0,480.2] || -> equal(op1(e12,op1(e12,e12)),e12) equal(op1(e13,op1(e13,e12)),e13)** equal(op1(e11,e10),e11) equal(op1(e10,op1(e10,e12)),e10). % 0.71/0.89 1325[4:MRR:1303.1,1.0] || SkC6* -> . % 0.71/0.89 1326[4:MRR:1269.2,1325.0] || -> SkC12 SkC8*. % 0.71/0.89 1339[4:MRR:968.1,1308.0] || -> equal(op1(e13,e10),e10)**. % 0.71/0.89 1340[4:MRR:1286.0,1308.0] || -> equal(op1(e11,e10),e13)** equal(op1(e11,e10),e12). % 0.71/0.89 1345[4:Rew:1339.0,108.1] || SkC12* -> equal(e13,e10). % 0.71/0.89 1349[4:MRR:1345.1,3.0] || SkC12* -> . % 0.71/0.89 1350[4:MRR:1326.0,1349.0] || -> SkC8*. % 0.71/0.89 1351[4:MRR:102.0,1350.0] || -> equal(op1(e10,e12),e12)**. % 0.71/0.89 1352[4:MRR:101.0,1350.0] || -> equal(op1(e12,e10),e12)**. % 0.71/0.89 1361[4:Rew:1352.0,146.0] || equal(op1(e11,e10),e12)** -> . % 0.71/0.89 1364[4:MRR:770.1,1309.0] || -> equal(op1(e13,e12),e13)**. % 0.71/0.89 1386[4:MRR:1301.1,1.0] || -> equal(op1(e11,e11),e11)**. % 0.71/0.89 1388[4:Rew:1386.0,152.0] || equal(op1(e12,e11),e11)** -> . % 0.71/0.89 1391[4:MRR:773.0,1388.0] || -> equal(op1(e12,e11),e13)**. % 0.71/0.89 1392[4:MRR:1281.1,1388.0] || -> equal(op1(e12,e12),e11)**. % 0.71/0.89 1401[4:MRR:1340.1,1361.0] || -> equal(op1(e11,e10),e13)**. % 0.71/0.89 1405[4:Rew:1351.0,1314.3,1351.0,1314.3,1401.0,1314.2,33.0,1314.1,1364.0,1314.1,1391.0,1314.0,1392.0,1314.0] || -> equal(e13,e12)** equal(e13,e11) equal(e13,e11) equal(e12,e10). % 0.71/0.89 1406[4:Obv:1405.1] || -> equal(e13,e12)** equal(e13,e11) equal(e12,e10). % 0.71/0.89 1407[4:MRR:1406.0,1406.1,1406.2,6.0,5.0,2.0] || -> . % 0.71/0.89 1418[4:Spt:1407.0,763.2,1300.0] || equal(op1(e11,e12),e10)** -> . % 0.71/0.89 1419[4:Spt:1407.0,763.0,763.1] || -> equal(op1(e11,e11),e10)** equal(op1(e11,e10),e10). % 0.71/0.89 1420[4:MRR:754.2,1418.0] || -> equal(op1(e10,e12),e10) equal(op1(e13,e12),e10)**. % 0.71/0.89 1422[5:Spt:1419.0] || -> equal(op1(e11,e11),e10)**. % 0.71/0.89 1425[5:Rew:1422.0,288.1] || SkC12* equal(e10,e10) -> . % 0.71/0.89 1426[5:Rew:1422.0,272.1] || SkC8* equal(e10,e10) -> . % 0.71/0.89 1427[5:Rew:1422.0,149.0] || equal(op1(e10,e11),e10)** -> . % 0.71/0.89 1429[5:Rew:1422.0,173.0] || equal(op1(e11,e10),e10)** -> . % 0.71/0.89 1446[5:Obv:1425.1] || SkC12* -> . % 0.71/0.89 1447[5:MRR:1269.0,1446.0] || -> SkC8 SkC6*. % 0.71/0.89 1448[5:Obv:1426.1] || SkC8* -> . % 0.71/0.89 1449[5:MRR:1447.0,1448.0] || -> SkC6*. % 0.71/0.89 1452[5:MRR:265.0,1449.0] || equal(op1(e12,e12),e12)** -> . % 0.71/0.89 1470[5:MRR:1283.0,1427.0] || -> equal(op1(e10,e11),e13)**. % 0.71/0.89 1481[5:Rew:1470.0,171.0] || equal(op1(e10,e13),e13)** -> . % 0.71/0.89 1483[5:MRR:968.1,1429.0] || -> equal(op1(e13,e10),e10)**. % 0.71/0.89 1487[5:Rew:1483.0,1112.0] || -> equal(e13,e10) equal(op1(e12,e10),e13)** equal(op1(e11,e10),e13). % 0.71/0.89 1493[5:MRR:750.0,1452.0] || -> equal(op1(e12,e10),e12)**. % 0.71/0.89 1509[5:MRR:739.1,1481.0] || -> equal(op1(e11,e13),e13)**. % 0.71/0.89 1516[5:Rew:1509.0,175.0] || equal(op1(e11,e10),e13)** -> . % 0.71/0.89 1528[5:Rew:1493.0,1487.1] || -> equal(e13,e10) equal(e13,e12) equal(op1(e11,e10),e13)**. % 0.71/0.89 1529[5:MRR:1528.0,1528.1,1528.2,3.0,6.0,1516.0] || -> . % 0.71/0.89 1546[5:Spt:1529.0,1419.0,1422.0] || equal(op1(e11,e11),e10)** -> . % 0.71/0.89 1547[5:Spt:1529.0,1419.1] || -> equal(op1(e11,e10),e10)**. % 0.71/0.89 1551[5:Rew:1547.0,147.0] || equal(op1(e13,e10),e10)** -> . % 0.71/0.89 1554[5:MRR:762.0,1546.0] || -> equal(op1(e10,e11),e10)**. % 0.71/0.89 1559[5:Rew:1554.0,170.0] || equal(op1(e10,e12),e10)** -> . % 0.71/0.89 1561[5:MRR:1420.0,1559.0] || -> equal(op1(e13,e12),e10)**. % 0.71/0.89 1568[5:MRR:771.1,1551.0] || -> equal(op1(e13,e10),e13)**. % 0.71/0.89 1573[5:Rew:1547.0,1277.1] || -> equal(op1(e12,e10),e12)** equal(e12,e10). % 0.71/0.89 1574[5:MRR:1573.1,2.0] || -> equal(op1(e12,e10),e12)**. % 0.71/0.89 1580[5:MRR:776.2,1546.0] || -> equal(op1(e11,e11),e11) equal(op1(e11,e11),e13)**. % 0.71/0.89 1588[5:MRR:1287.1,1559.0] || -> equal(op1(e10,e12),e12) equal(op1(e10,e12),e13)**. % 0.71/0.89 1592[5:Rew:1561.0,427.0] || -> equal(e13,e10) equal(op1(e12,e12),e13)** equal(op1(e11,e12),e13) equal(op1(e10,e12),e13). % 0.71/0.89 1593[5:MRR:1592.0,3.0] || -> equal(op1(e12,e12),e13)** equal(op1(e11,e12),e13) equal(op1(e10,e12),e13). % 0.71/0.89 1594[5:Rew:1547.0,436.3] || -> equal(op1(e11,e13),e13)** equal(op1(e11,e11),e13) equal(op1(e11,e12),e13) equal(e13,e10). % 0.71/0.89 1595[5:MRR:1594.3,3.0] || -> equal(op1(e11,e13),e13)** equal(op1(e11,e11),e13) equal(op1(e11,e12),e13). % 0.71/0.89 1596[5:Rew:1554.0,786.3,1561.0,786.0] || -> equal(e13,e10) equal(op1(e11,op1(e11,e11)),e11) equal(op1(e12,op1(e12,e11)),e12)** equal(op1(e10,e10),e10). % 0.71/0.89 1597[5:Rew:1263.0,1596.3] || -> equal(e13,e10) equal(op1(e11,op1(e11,e11)),e11) equal(op1(e12,op1(e12,e11)),e12)** equal(e11,e10). % 0.71/0.89 1598[5:MRR:1597.0,1597.3,3.0,1.0] || -> equal(op1(e11,op1(e11,e11)),e11) equal(op1(e12,op1(e12,e11)),e12)**. % 0.71/0.89 1601[5:Rew:1554.0,1290.15,1547.0,1290.13,1574.0,1290.11,31.0,1290.4,1568.0,1290.4,1561.0,1290.3] || SkC37 SkC36 equal(h3(e12),e23) equal(op2(e22,h3(e12)),h3(e10)) equal(op2(e22,h3(e10)),e22) equal(op2(h3(e11),e22),h3(op1(e11,e13))) equal(op2(h3(e10),e22),h3(op1(e10,e13))) equal(op2(h3(e12),h3(e12)),h3(op1(e12,e12)))** equal(op2(h3(e11),h3(e11)),h3(op1(e11,e11))) equal(op2(h3(e10),h3(e10)),h3(e11)) equal(op2(h3(e12),h3(e11)),h3(op1(e12,e11))) equal(op2(h3(e12),h3(e10)),h3(e12)) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),h3(e10)),h3(e10)) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),h3(e11)),h3(e10)) -> . % 0.71/0.89 1611[6:Spt:737.0] || -> equal(h1(e11),e23)**. % 0.71/0.89 1627[6:Rew:1611.0,538.0] || -> equal(op2(e20,e23),h1(e12))**. % 0.71/0.89 1628[6:Rew:1611.0,617.0] || equal(op2(e20,e23),e23)** -> . % 0.71/0.89 1630[6:Rew:1611.0,619.0] || equal(op2(e20,e21),e23)** -> . % 0.71/0.89 1631[6:Rew:1611.0,631.0] || equal(op2(e23,e20),e23)** -> . % 0.71/0.89 1636[6:Rew:1627.0,735.0] || -> equal(h1(e12),e23) equal(op2(e20,e23),e22)**. % 0.71/0.89 1642[6:Rew:1627.0,220.0] || equal(op2(e20,e22),h1(e12))** -> . % 0.71/0.89 1644[6:Rew:1627.0,209.0] || equal(op2(e21,e23),h1(e12))** -> . % 0.71/0.89 1645[6:Rew:1627.0,780.2] || -> equal(op2(e22,e20),e22) equal(op2(e21,op2(e21,e23)),e21)** equal(op2(e20,h1(e12)),e20). % 0.71/0.89 1647[6:Rew:1627.0,1628.0] || equal(h1(e12),e23)** -> . % 0.71/0.89 1650[6:MRR:700.2,1630.0] || -> equal(h2(e11),e23) equal(op2(e22,e21),e23)**. % 0.71/0.89 1652[6:MRR:135.1,1631.0] || SkC27* -> . % 0.71/0.89 1654[6:MRR:727.0,1631.0] || -> equal(op2(e23,e20),e20)**. % 0.71/0.89 1655[6:MRR:675.0,1652.0] || -> SkC23 SkC21 SkC19*. % 0.71/0.89 1668[6:Rew:1654.0,195.0] || equal(op2(e21,e20),e20)** -> . % 0.71/0.89 1677[6:MRR:711.1,1668.0] || -> equal(h2(e11),e20) equal(op2(e21,e22),e20)**. % 0.71/0.89 1678[6:Rew:1627.0,1636.1] || -> equal(h1(e12),e23)** equal(h1(e12),e22). % 0.71/0.89 1679[6:MRR:1678.0,1647.0] || -> equal(h1(e12),e22)**. % 0.71/0.89 1681[6:Rew:1679.0,673.0] || -> equal(op2(e22,e20),h1(e10))**. % 0.71/0.89 1686[6:Rew:1679.0,1642.0] || equal(op2(e20,e22),e22)** -> . % 0.71/0.89 1688[6:Rew:1679.0,1644.0] || equal(op2(e21,e23),e22)** -> . % 0.71/0.89 1694[6:Rew:1681.0,613.0] || equal(h3(e11),h1(e10))** -> . % 0.71/0.89 1698[6:MRR:129.1,1686.0] || SkC23* -> . % 0.71/0.89 1699[6:MRR:690.2,1686.0] || -> equal(h3(e11),e22) equal(op2(e21,e22),e22)**. % 0.71/0.89 1700[6:MRR:1655.0,1698.0] || -> SkC21 SkC19*. % 0.71/0.89 1701[6:MRR:732.1,1688.0] || -> equal(op2(e21,e23),e23)**. % 0.71/0.89 1705[6:Rew:1701.0,614.0] || equal(h2(e11),e23)** -> . % 0.71/0.89 1709[6:MRR:734.0,1705.0] || -> equal(h2(e11),e21)** equal(h2(e11),e20). % 0.71/0.89 1710[6:MRR:1650.0,1705.0] || -> equal(op2(e22,e21),e23)**. % 0.71/0.89 1712[6:Rew:1710.0,125.1] || SkC21* -> equal(e23,e21). % 0.71/0.89 1719[6:MRR:1712.1,11.0] || SkC21* -> . % 0.71/0.89 1720[6:MRR:1700.0,1719.0] || -> SkC19*. % 0.71/0.89 1723[6:MRR:568.0,1720.0] || equal(h2(e11),e20)** -> . % 0.71/0.89 1734[6:MRR:1709.1,1723.0] || -> equal(h2(e11),e21)**. % 0.71/0.89 1759[6:Rew:1734.0,1677.0] || -> equal(e21,e20) equal(op2(e21,e22),e20)**. % 0.71/0.89 1760[6:MRR:1759.0,7.0] || -> equal(op2(e21,e22),e20)**. % 0.71/0.89 1762[6:Rew:1760.0,203.0] || equal(op2(e20,e22),e20)** -> . % 0.71/0.89 1765[6:Rew:1760.0,1699.1] || -> equal(h3(e11),e22)** equal(e22,e20). % 0.71/0.89 1766[6:MRR:1765.1,8.0] || -> equal(h3(e11),e22)**. % 0.71/0.89 1775[6:Rew:1766.0,1694.0] || equal(h1(e10),e22)** -> . % 0.71/0.89 1796[6:Rew:1679.0,1645.2,1701.0,1645.1,1701.0,1645.1,1681.0,1645.0] || -> equal(h1(e10),e22) equal(e23,e21) equal(op2(e20,e22),e20)**. % 0.71/0.89 1797[6:MRR:1796.0,1796.1,1796.2,1775.0,11.0,1762.0] || -> . % 0.71/0.89 1811[6:Spt:1797.0,737.0,1611.0] || equal(h1(e11),e23)** -> . % 0.71/0.89 1812[6:Spt:1797.0,737.1,737.2,737.3] || -> equal(h1(e11),e22)** equal(h1(e11),e21) equal(h1(e11),e20). % 0.71/0.89 1813[6:MRR:712.0,1811.0] || -> equal(op2(e23,e20),e23)** equal(op2(e22,e20),e23) equal(op2(e21,e20),e23). % 0.71/0.89 1815[7:Spt:1812.0] || -> equal(h1(e11),e22)**. % 0.71/0.89 1819[7:Rew:1815.0,721.0] || -> equal(e22,e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21)**. % 0.71/0.89 1820[7:Rew:1815.0,719.0] || -> equal(e22,e21) equal(op2(e21,e20),e21) equal(op2(e22,e20),e21)**. % 0.71/0.89 1822[7:Rew:1815.0,563.1] || SkC21* equal(e22,e22) -> . % 0.71/0.89 1825[7:Rew:1815.0,632.0] || equal(op2(e22,e20),e22)** -> . % 0.71/0.89 1829[7:Rew:1815.0,617.0] || equal(op2(e20,e23),e22)** -> . % 0.71/0.89 1830[7:Rew:1815.0,538.0] || -> equal(op2(e20,e22),h1(e12))**. % 0.71/0.89 1832[7:Rew:1815.0,723.0] || -> equal(e22,e20) equal(op2(e23,e20),e20)** equal(op2(e21,e20),e20). % 0.71/0.89 1839[7:Obv:1822.1] || SkC21* -> . % 0.71/0.89 1840[7:MRR:675.2,1839.0] || -> SkC27 SkC23 SkC19*. % 0.71/0.89 1843[7:MRR:128.1,1825.0] || SkC23* -> . % 0.71/0.89 1846[7:MRR:780.0,1825.0] || -> equal(op2(e21,op2(e21,e23)),e21)** equal(op2(e20,op2(e20,e23)),e20). % 0.71/0.89 1847[7:MRR:1840.1,1843.0] || -> SkC27 SkC19*. % 0.71/0.89 1865[7:MRR:683.1,1829.0] || -> equal(op2(e21,e23),e22)**. % 0.71/0.89 1866[7:MRR:735.1,1829.0] || -> equal(op2(e20,e23),e23)**. % 0.71/0.89 1880[7:Rew:1830.0,205.0] || equal(op2(e23,e22),h1(e12))** -> . % 0.71/0.89 1882[7:Rew:1830.0,203.0] || equal(op2(e21,e22),h1(e12))** -> . % 0.71/0.89 1899[7:Rew:1830.0,1819.2] || -> equal(e22,e21) equal(op2(e20,e21),e21)** equal(h1(e12),e21). % 0.71/0.89 1900[7:MRR:1899.0,10.0] || -> equal(op2(e20,e21),e21)** equal(h1(e12),e21). % 0.71/0.89 1901[7:MRR:1820.0,10.0] || -> equal(op2(e21,e20),e21) equal(op2(e22,e20),e21)**. % 0.71/0.89 1904[7:MRR:1832.0,8.0] || -> equal(op2(e23,e20),e20)** equal(op2(e21,e20),e20). % 0.71/0.89 1909[7:Rew:1866.0,1846.1,1866.0,1846.1,1865.0,1846.0] || -> equal(op2(e21,e22),e21)** equal(e23,e20). % 0.71/0.89 1910[7:MRR:1909.1,9.0] || -> equal(op2(e21,e22),e21)**. % 0.71/0.89 1913[7:Rew:1910.0,222.0] || equal(op2(e21,e20),e21)** -> . % 0.71/0.89 1916[7:Rew:1910.0,1882.0] || equal(h1(e12),e21)** -> . % 0.71/0.89 1919[7:MRR:1900.1,1916.0] || -> equal(op2(e20,e21),e21)**. % 0.71/0.89 1922[7:Rew:1919.0,198.0] || equal(op2(e22,e21),e21)** -> . % 0.71/0.89 1928[7:MRR:121.1,1913.0] || SkC19* -> . % 0.71/0.89 1929[7:MRR:1901.0,1913.0] || -> equal(op2(e22,e20),e21)**. % 0.71/0.89 1930[7:MRR:1847.1,1928.0] || -> SkC27*. % 0.71/0.89 1931[7:MRR:135.0,1930.0] || -> equal(op2(e23,e20),e23)**. % 0.71/0.89 1939[7:Rew:1929.0,783.2] || -> equal(h1(e12),e20) equal(op2(e23,op2(e23,e20)),e23)** equal(op2(e22,e21),e22) equal(op2(e21,op2(e21,e20)),e21). % 0.71/0.89 1943[7:Rew:1931.0,234.0] || equal(op2(e23,e22),e23)** -> . % 0.71/0.89 1945[7:Rew:1931.0,1904.0] || -> equal(e23,e20) equal(op2(e21,e20),e20)**. % 0.71/0.89 1947[7:MRR:730.0,1922.0] || -> equal(op2(e22,e21),e23)**. % 0.71/0.89 1954[7:MRR:726.0,1943.0] || -> equal(op2(e23,e22),e20)**. % 0.71/0.89 1957[7:Rew:1954.0,1880.0] || equal(h1(e12),e20)** -> . % 0.71/0.89 1962[7:MRR:1945.0,9.0] || -> equal(op2(e21,e20),e20)**. % 0.71/0.89 1988[7:Rew:1962.0,1939.3,1962.0,1939.3,1947.0,1939.2,34.0,1939.1,1931.0,1939.1] || -> equal(h1(e12),e20)** equal(e23,e21) equal(e23,e22) equal(e21,e20). % 0.71/0.89 1989[7:MRR:1988.0,1988.1,1988.2,1988.3,1957.0,11.0,12.0,7.0] || -> . % 0.71/0.89 1998[7:Spt:1989.0,1812.0,1815.0] || equal(h1(e11),e22)** -> . % 0.71/0.89 1999[7:Spt:1989.0,1812.1,1812.2] || -> equal(h1(e11),e21)** equal(h1(e11),e20). % 0.71/0.89 2000[7:MRR:715.0,1998.0] || -> equal(op2(e22,e20),e22)** equal(op2(e21,e20),e22). % 0.71/0.89 2002[8:Spt:1999.0] || -> equal(h1(e11),e21)**. % 0.71/0.89 2007[8:Rew:2002.0,83.0] || -> equal(op2(e20,e20),e21)**. % 0.71/0.89 2013[8:Rew:2002.0,538.0] || -> equal(op2(e20,e21),h1(e12))**. % 0.71/0.89 2015[8:Rew:2002.0,618.0] || equal(op2(e20,e22),e21)** -> . % 0.71/0.89 2016[8:Rew:2002.0,619.0] || equal(op2(e20,e21),e21)** -> . % 0.71/0.89 2018[8:Rew:2002.0,632.0] || equal(op2(e22,e20),e21)** -> . % 0.71/0.89 2019[8:Rew:2002.0,633.0] || equal(op2(e21,e20),e21)** -> . % 0.71/0.89 2024[8:Rew:2013.0,736.0] || -> equal(h1(e12),e21) equal(op2(e20,e21),e20) equal(op2(e20,e21),e23)**. % 0.71/0.89 2027[8:Rew:2013.0,630.0] || equal(h2(e11),h1(e12))** -> . % 0.71/0.89 2028[8:Rew:2013.0,219.0] || equal(op2(e20,e23),h1(e12))** -> . % 0.71/0.89 2029[8:Rew:2013.0,218.0] || equal(op2(e20,e22),h1(e12))** -> . % 0.71/0.89 2030[8:Rew:2013.0,198.0] || equal(op2(e22,e21),h1(e12))** -> . % 0.71/0.89 2034[8:Rew:2013.0,782.3] || -> equal(h2(e12),e21) equal(op2(e23,e22),e23) equal(op2(e22,op2(e22,e21)),e22)** equal(op2(e20,h1(e12)),e20). % 0.71/0.89 2036[8:MRR:416.3,2015.0] || -> equal(op2(e20,e22),e22) equal(op2(e20,e22),e20) equal(op2(e20,e22),e23)**. % 0.71/0.89 2037[8:Rew:2013.0,2016.0] || equal(h1(e12),e21)** -> . % 0.71/0.89 2038[8:MRR:696.2,2018.0] || -> equal(h3(e11),e21) equal(op2(e22,e21),e21)**. % 0.71/0.89 2039[8:MRR:731.2,2018.0] || -> equal(op2(e22,e20),e22) equal(op2(e22,e20),e23)**. % 0.71/0.89 2040[8:MRR:121.1,2019.0] || SkC19* -> . % 0.71/0.89 2042[8:MRR:414.0,2019.0] || -> equal(op2(e21,e20),e20) equal(op2(e21,e20),e23)** equal(op2(e21,e20),e22). % 0.71/0.89 2043[8:MRR:675.3,2040.0] || -> SkC27 SkC23 SkC21*. % 0.71/0.89 2048[8:Rew:2013.0,2024.2,2013.0,2024.1] || -> equal(h1(e12),e21) equal(h1(e12),e20) equal(h1(e12),e23)**. % 0.71/0.89 2049[8:MRR:2048.0,2037.0] || -> equal(h1(e12),e20) equal(h1(e12),e23)**. % 0.71/0.89 2057[9:Spt:773.0] || -> equal(op1(e12,e11),e11)**. % 0.71/0.89 2060[9:Rew:2057.0,152.0] || equal(op1(e11,e11),e11)** -> . % 0.71/0.89 2064[9:Rew:2057.0,1598.1] || -> equal(op1(e11,op1(e11,e11)),e11)** equal(op1(e12,e11),e12). % 0.71/0.89 2075[9:MRR:1580.0,2060.0] || -> equal(op1(e11,e11),e13)**. % 0.71/0.89 2087[9:Rew:2075.0,177.0] || equal(op1(e11,e13),e13)** -> . % 0.71/0.89 2097[9:MRR:775.0,2087.0] || -> equal(op1(e11,e13),e12)**. % 0.71/0.89 2113[9:Rew:2057.0,2064.1,2097.0,2064.0,2075.0,2064.0] || -> equal(e12,e11)** equal(e12,e11)**. % 0.71/0.89 2114[9:Obv:2113.0] || -> equal(e12,e11)**. % 0.71/0.89 2115[9:MRR:2114.0,4.0] || -> . % 0.71/0.89 2129[9:Spt:2115.0,773.0,2057.0] || equal(op1(e12,e11),e11)** -> . % 0.71/0.89 2130[9:Spt:2115.0,773.1] || -> equal(op1(e12,e11),e13)**. % 0.71/0.89 2134[9:Rew:2130.0,98.1] || SkC6* -> equal(e13,e11). % 0.71/0.89 2135[9:MRR:2134.1,5.0] || SkC6* -> . % 0.71/0.89 2136[9:MRR:1269.2,2135.0] || -> SkC12 SkC8*. % 0.71/0.89 2139[9:Rew:2130.0,1285.1] || -> equal(op1(e11,e11),e11)** equal(e13,e11). % 0.71/0.89 2140[9:MRR:2139.1,5.0] || -> equal(op1(e11,e11),e11)**. % 0.71/0.89 2146[9:Rew:2130.0,1281.1] || -> equal(op1(e12,e12),e11)** equal(e13,e11). % 0.71/0.89 2147[9:MRR:2146.1,5.0] || -> equal(op1(e12,e12),e11)**. % 0.71/0.89 2155[9:Rew:2147.0,1593.0] || -> equal(e13,e11) equal(op1(e11,e12),e13)** equal(op1(e10,e12),e13). % 0.71/0.89 2156[9:MRR:2155.0,5.0] || -> equal(op1(e11,e12),e13)** equal(op1(e10,e12),e13). % 0.71/0.89 2157[9:Rew:2140.0,1595.1] || -> equal(op1(e11,e13),e13)** equal(e13,e11) equal(op1(e11,e12),e13). % 0.71/0.89 2158[9:MRR:2157.1,5.0] || -> equal(op1(e11,e13),e13)** equal(op1(e11,e12),e13). % 0.71/0.89 2168[9:Rew:31.0,1601.10,2130.0,1601.10,2140.0,1601.8,2147.0,1601.7] || SkC37 SkC36 equal(h3(e12),e23) equal(op2(e22,h3(e12)),h3(e10)) equal(op2(e22,h3(e10)),e22) equal(op2(h3(e11),e22),h3(op1(e11,e13))) equal(op2(h3(e10),e22),h3(op1(e10,e13))) equal(op2(h3(e12),h3(e12)),h3(e11))** equal(op2(h3(e11),h3(e11)),h3(e11)) equal(op2(h3(e10),h3(e10)),h3(e11)) equal(op2(h3(e12),h3(e11)),e22) equal(op2(h3(e12),h3(e10)),h3(e12)) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),h3(e10)),h3(e10)) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),h3(e11)),h3(e10)) -> . % 0.71/0.89 2171[10:Spt:777.0] || -> equal(op1(e10,e13),e13)**. % 0.71/0.89 2174[10:Rew:2171.0,161.0] || equal(op1(e11,e13),e13)** -> . % 0.71/0.89 2175[10:Rew:2171.0,172.0] || equal(op1(e10,e12),e13)** -> . % 0.71/0.89 2185[10:Rew:2171.0,2168.6] || SkC37 SkC36 equal(h3(e12),e23) equal(op2(e22,h3(e12)),h3(e10)) equal(op2(e22,h3(e10)),e22) equal(op2(h3(e11),e22),h3(op1(e11,e13))) equal(op2(h3(e10),e22),h3(e13)) equal(op2(h3(e12),h3(e12)),h3(e11))** equal(op2(h3(e11),h3(e11)),h3(e11)) equal(op2(h3(e10),h3(e10)),h3(e11)) equal(op2(h3(e12),h3(e11)),e22) equal(op2(h3(e12),h3(e10)),h3(e12)) equal(op2(h3(e11),h3(e12)),h3(op1(e11,e12))) equal(op2(h3(e11),h3(e10)),h3(e10)) equal(op2(h3(e10),h3(e12)),h3(op1(e10,e12))) equal(op2(h3(e10),h3(e11)),h3(e10)) -> . % 0.71/0.89 2187[10:MRR:775.0,2174.0] || -> equal(op1(e11,e13),e12)**. % 0.71/0.89 2188[10:MRR:2158.0,2174.0] || -> equal(op1(e11,e12),e13)**. % 0.71/0.89 2197[10:MRR:1588.1,2175.0] || -> equal(op1(e10,e12),e12)**. % 0.71/0.89 2210[10:Rew:2197.0,2185.14,31.0,2185.12,2188.0,2185.12,31.0,2185.6,2187.0,2185.5] || SkC37 SkC36 equal(h3(e12),e23) equal(op2(e22,h3(e12)),h3(e10)) equal(op2(e22,h3(e10)),e22) equal(op2(h3(e11),e22),h3(e12)) equal(op2(h3(e10),e22),e22) equal(op2(h3(e12),h3(e12)),h3(e11))** equal(op2(h3(e11),h3(e11)),h3(e11)) equal(op2(h3(e10),h3(e10)),h3(e11)) equal(op2(h3(e12),h3(e11)),e22) equal(op2(h3(e12),h3(e10)),h3(e12)) equal(op2(h3(e11),h3(e12)),e22) equal(op2(h3(e11),h3(e10)),h3(e10)) equal(op2(h3(e10),h3(e12)),h3(e12)) equal(op2(h3(e10),h3(e11)),h3(e10)) -> . % 0.71/0.89 2213[11:Spt:734.0] || -> equal(h2(e11),e23)**. % 0.71/0.89 2221[11:Rew:2213.0,614.0] || equal(op2(e21,e23),e23)** -> . % 0.71/0.89 2223[11:Rew:2213.0,628.0] || equal(op2(e22,e21),e23)** -> . % 0.71/0.89 2225[11:Rew:2213.0,537.0] || -> equal(op2(e21,e23),h2(e12))**. % 0.71/0.89 2232[11:Rew:2213.0,2027.0] || equal(h1(e12),e23)** -> . % 0.71/0.89 2235[11:MRR:2049.1,2232.0] || -> equal(h1(e12),e20)**. % 0.71/0.89 2244[11:Rew:2235.0,2034.3] || -> equal(h2(e12),e21) equal(op2(e23,e22),e23) equal(op2(e22,op2(e22,e21)),e22)** equal(op2(e20,e20),e20). % 0.71/0.89 2246[11:MRR:732.0,2221.0] || -> equal(op2(e21,e23),e22)**. % 0.71/0.89 2251[11:Rew:2246.0,223.0] || equal(op2(e21,e20),e22)** -> . % 0.71/0.89 2261[11:MRR:730.1,2223.0] || -> equal(op2(e22,e21),e21)**. % 0.71/0.89 2265[11:Rew:2261.0,612.0] || equal(h3(e11),e21)** -> . % 0.71/0.89 2268[11:MRR:729.2,2265.0] || -> equal(h3(e11),e23)** equal(h3(e11),e22). % 0.71/0.89 2280[11:Rew:2246.0,2225.0] || -> equal(h2(e12),e22)**. % 0.71/0.89 2291[11:MRR:2000.1,2251.0] || -> equal(op2(e22,e20),e22)**. % 0.71/0.89 2293[11:Rew:2291.0,613.0] || equal(h3(e11),e22)** -> . % 0.71/0.89 2307[11:MRR:2268.1,2293.0] || -> equal(h3(e11),e23)**. % 0.71/0.89 2311[11:Rew:2307.0,623.0] || equal(op2(e23,e22),e23)** -> . % 0.71/0.89 2323[11:MRR:726.0,2311.0] || -> equal(op2(e23,e22),e20)**. % 0.71/0.89 2340[11:Rew:2007.0,2244.3,2261.0,2244.2,2261.0,2244.2,2323.0,2244.1,2280.0,2244.0] || -> equal(e22,e21) equal(e23,e20)** equal(e22,e21) equal(e21,e20). % 0.71/0.89 2341[11:Obv:2340.0] || -> equal(e23,e20)** equal(e22,e21) equal(e21,e20). % 0.71/0.89 2342[11:MRR:2341.0,2341.1,2341.2,9.0,10.0,7.0] || -> . % 0.71/0.89 2358[11:Spt:2342.0,734.0,2213.0] || equal(h2(e11),e23)** -> . % 0.71/0.89 2359[11:Spt:2342.0,734.1,734.2] || -> equal(h2(e11),e21)** equal(h2(e11),e20). % 0.71/0.89 2362[12:Spt:2359.0] || -> equal(h2(e11),e21)**. % 0.71/0.89 2366[12:Rew:2362.0,84.0] || -> equal(op2(e21,e21),e21)**. % 0.71/0.89 2374[12:Rew:2362.0,628.0] || equal(op2(e22,e21),e21)** -> . % 0.71/0.89 2375[12:Rew:2362.0,615.0] || equal(op2(e21,e22),e21)** -> . % 0.71/0.89 2386[12:MRR:125.1,2374.0] || SkC21* -> . % 0.71/0.89 2387[12:MRR:2038.1,2374.0] || -> equal(h3(e11),e21)**. % 0.71/0.89 2388[12:MRR:730.0,2374.0] || -> equal(op2(e22,e21),e23)**. % 0.71/0.89 2389[12:MRR:2043.2,2386.0] || -> SkC27 SkC23*. % 0.71/0.89 2391[12:Rew:2387.0,64.0] || equal(e21,e21) -> SkC37*. % 0.71/0.89 2400[12:Rew:2387.0,536.0] || -> equal(op2(e22,e21),h3(e12))**. % 0.71/0.89 2402[12:Rew:2387.0,686.0] || -> equal(e23,e21) equal(op2(e23,e22),e23)** equal(op2(e21,e22),e23) equal(op2(e20,e22),e23). % 0.71/0.89 2404[12:Rew:2387.0,2210.5] || SkC37 SkC36 equal(h3(e12),e23) equal(op2(e22,h3(e12)),h3(e10)) equal(op2(e22,h3(e10)),e22) equal(op2(e21,e22),h3(e12)) equal(op2(h3(e10),e22),e22) equal(op2(h3(e12),h3(e12)),h3(e11))** equal(op2(h3(e11),h3(e11)),h3(e11)) equal(op2(h3(e10),h3(e10)),h3(e11)) equal(op2(h3(e12),h3(e11)),e22) equal(op2(h3(e12),h3(e10)),h3(e12)) equal(op2(h3(e11),h3(e12)),e22) equal(op2(h3(e11),h3(e10)),h3(e10)) equal(op2(h3(e10),h3(e12)),h3(e12)) equal(op2(h3(e10),h3(e11)),h3(e10)) -> . % 0.71/0.89 2408[12:Rew:2388.0,2030.0] || equal(h1(e12),e23)** -> . % 0.71/0.89 2409[12:Rew:2388.0,227.0] || equal(op2(e22,e20),e23)** -> . % 0.71/0.89 2411[12:Obv:2391.0] || -> SkC37*. % 0.71/0.89 2412[12:MRR:2049.1,2408.0] || -> equal(h1(e12),e20)**. % 0.71/0.89 2416[12:Rew:2412.0,2013.0] || -> equal(op2(e20,e21),e20)**. % 0.71/0.89 2417[12:Rew:2412.0,2029.0] || equal(op2(e20,e22),e20)** -> . % 0.71/0.89 2421[12:MRR:412.1,2375.0] || -> equal(op2(e21,e22),e22) equal(op2(e21,e22),e23)** equal(op2(e21,e22),e20). % 0.71/0.89 2426[12:Rew:2388.0,2400.0] || -> equal(h3(e12),e23)**. % 0.71/0.89 2428[12:Rew:2426.0,671.0] || -> equal(op2(e23,e22),h3(e10))**. % 0.71/0.89 2429[12:Rew:2426.0,781.0] || -> equal(e23,e22) equal(op2(e23,op2(e23,e22)),e23)** equal(op2(e21,op2(e21,e22)),e21) equal(op2(e20,op2(e20,e22)),e20). % 0.71/0.89 2430[12:MRR:2039.1,2409.0] || -> equal(op2(e22,e20),e22)**. % 0.71/0.89 2431[12:MRR:1813.1,2409.0] || -> equal(op2(e23,e20),e23)** equal(op2(e21,e20),e23). % 0.71/0.89 2435[12:Rew:2430.0,194.0] || equal(op2(e21,e20),e22)** -> . % 0.71/0.89 2437[12:MRR:698.0,2417.0] || -> equal(op2(e23,e22),e20)** equal(op2(e21,e22),e20). % 0.71/0.89 2438[12:MRR:2036.1,2417.0] || -> equal(op2(e20,e22),e22) equal(op2(e20,e22),e23)**. % 0.71/0.89 2445[12:Rew:2428.0,234.0] || equal(op2(e23,e20),h3(e10))** -> . % 0.71/0.89 2447[12:Rew:2428.0,726.0] || -> equal(h3(e10),e23) equal(op2(e23,e22),e20)**. % 0.71/0.89 2450[12:MRR:2042.2,2435.0] || -> equal(op2(e21,e20),e20) equal(op2(e21,e20),e23)**. % 0.71/0.89 2451[12:Rew:2428.0,2447.1] || -> equal(h3(e10),e23)** equal(h3(e10),e20). % 0.71/0.89 2452[12:Rew:2428.0,2437.0] || -> equal(h3(e10),e20) equal(op2(e21,e22),e20)**. % 0.71/0.89 2455[12:Rew:2428.0,2402.1] || -> equal(e23,e21) equal(h3(e10),e23) equal(op2(e21,e22),e23)** equal(op2(e20,e22),e23). % 0.71/0.89 2456[12:MRR:2455.0,11.0] || -> equal(h3(e10),e23) equal(op2(e21,e22),e23)** equal(op2(e20,e22),e23). % 0.71/0.89 2457[12:Rew:2428.0,2429.1] || -> equal(e23,e22) equal(op2(e23,h3(e10)),e23) equal(op2(e21,op2(e21,e22)),e21)** equal(op2(e20,op2(e20,e22)),e20). % 0.71/0.89 2458[12:MRR:2457.0,12.0] || -> equal(op2(e23,h3(e10)),e23) equal(op2(e21,op2(e21,e22)),e21)** equal(op2(e20,op2(e20,e22)),e20). % 0.71/0.89 2472[12:Rew:2387.0,2404.15,2426.0,2404.14,2387.0,2404.13,2387.0,2404.12,2426.0,2404.12,2426.0,2404.11,519.0,2404.10,2426.0,2404.10,2387.0,2404.10,2387.0,2404.9,2366.0,2404.8,2387.0,2404.8,34.0,2404.7,2426.0,2404.7,2387.0,2404.7,2426.0,2404.5,646.0,2404.3,2426.0,2404.3,2426.0,2404.2] || SkC37 SkC36 equal(e23,e23) equal(h3(e10),e20) equal(op2(e22,h3(e10)),e22) equal(op2(e21,e22),e23) equal(op2(h3(e10),e22),e22) equal(e21,e21) equal(e21,e21) equal(op2(h3(e10),h3(e10)),e21)** equal(e22,e22) equal(op2(e23,h3(e10)),e23) equal(op2(e21,e23),e22) equal(op2(e21,h3(e10)),h3(e10)) equal(op2(h3(e10),e23),e23) equal(op2(h3(e10),e21),h3(e10)) -> . % 0.71/0.89 2473[12:Obv:2472.10] || SkC37 SkC36 equal(h3(e10),e20) equal(op2(e22,h3(e10)),e22) equal(op2(e21,e22),e23) equal(op2(h3(e10),e22),e22) equal(op2(h3(e10),h3(e10)),e21)** equal(op2(e23,h3(e10)),e23) equal(op2(e21,e23),e22) equal(op2(e21,h3(e10)),h3(e10)) equal(op2(h3(e10),e23),e23) equal(op2(h3(e10),e21),h3(e10)) -> . % 0.71/0.89 2474[12:MRR:2473.0,2473.1,2411.0,59.1] || equal(h3(e10),e20) equal(op2(e22,h3(e10)),e22) equal(op2(e21,e22),e23) equal(op2(h3(e10),e22),e22) equal(op2(h3(e10),h3(e10)),e21)** equal(op2(e23,h3(e10)),e23) equal(op2(e21,e23),e22) equal(op2(e21,h3(e10)),h3(e10)) equal(op2(h3(e10),e23),e23) equal(op2(h3(e10),e21),h3(e10)) -> . % 0.71/0.90 2478[13:Spt:735.0] || -> equal(op2(e20,e23),e23)**. % 0.71/0.90 2482[13:Rew:2478.0,209.0] || equal(op2(e21,e23),e23)** -> . % 0.71/0.90 2483[13:Rew:2478.0,220.0] || equal(op2(e20,e22),e23)** -> . % 0.71/0.90 2486[13:MRR:732.0,2482.0] || -> equal(op2(e21,e23),e22)**. % 0.71/0.90 2492[13:Rew:2486.0,2474.6] || equal(h3(e10),e20) equal(op2(e22,h3(e10)),e22) equal(op2(e21,e22),e23) equal(op2(h3(e10),e22),e22) equal(op2(h3(e10),h3(e10)),e21)** equal(op2(e23,h3(e10)),e23) equal(e22,e22) equal(op2(e21,h3(e10)),h3(e10)) equal(op2(h3(e10),e23),e23) equal(op2(h3(e10),e21),h3(e10)) -> . % 0.71/0.90 2494[13:MRR:2438.1,2483.0] || -> equal(op2(e20,e22),e22)**. % 0.71/0.90 2495[13:MRR:2456.2,2483.0] || -> equal(h3(e10),e23) equal(op2(e21,e22),e23)**. % 0.71/0.90 2500[13:Rew:2494.0,2458.2] || -> equal(op2(e23,h3(e10)),e23) equal(op2(e21,op2(e21,e22)),e21)** equal(op2(e20,e22),e20). % 0.71/0.90 2503[13:Rew:2494.0,2500.2] || -> equal(op2(e23,h3(e10)),e23) equal(op2(e21,op2(e21,e22)),e21)** equal(e22,e20). % 0.71/0.90 2504[13:MRR:2503.2,8.0] || -> equal(op2(e23,h3(e10)),e23) equal(op2(e21,op2(e21,e22)),e21)**. % 0.71/0.90 2508[13:Obv:2492.6] || equal(h3(e10),e20) equal(op2(e22,h3(e10)),e22) equal(op2(e21,e22),e23) equal(op2(h3(e10),e22),e22) equal(op2(h3(e10),h3(e10)),e21)** equal(op2(e23,h3(e10)),e23) equal(op2(e21,h3(e10)),h3(e10)) equal(op2(h3(e10),e23),e23) equal(op2(h3(e10),e21),h3(e10)) -> . % 0.71/0.90 2510[14:Spt:727.0] || -> equal(op2(e23,e20),e23)**. % 0.71/0.90 2514[14:Rew:2510.0,195.0] || equal(op2(e21,e20),e23)** -> . % 0.71/0.90 2517[14:Rew:2510.0,2445.0] || equal(h3(e10),e23)** -> . % 0.71/0.90 2518[14:MRR:2451.0,2517.0] || -> equal(h3(e10),e20)**. % 0.71/0.90 2519[14:MRR:2495.0,2517.0] || -> equal(op2(e21,e22),e23)**. % 0.71/0.90 2520[14:Rew:2518.0,2508.0] || equal(e20,e20) equal(op2(e22,h3(e10)),e22) equal(op2(e21,e22),e23) equal(op2(h3(e10),e22),e22) equal(op2(h3(e10),h3(e10)),e21)** equal(op2(e23,h3(e10)),e23) equal(op2(e21,h3(e10)),h3(e10)) equal(op2(h3(e10),e23),e23) equal(op2(h3(e10),e21),h3(e10)) -> . % 0.71/0.90 2533[14:MRR:2450.1,2514.0] || -> equal(op2(e21,e20),e20)**. % 0.71/0.90 2542[14:Obv:2520.0] || equal(op2(e22,h3(e10)),e22) equal(op2(e21,e22),e23) equal(op2(h3(e10),e22),e22) equal(op2(h3(e10),h3(e10)),e21)** equal(op2(e23,h3(e10)),e23) equal(op2(e21,h3(e10)),h3(e10)) equal(op2(h3(e10),e23),e23) equal(op2(h3(e10),e21),h3(e10)) -> . % 0.71/0.90 2543[14:Rew:2416.0,2542.7,2518.0,2542.7,2518.0,2542.6,2533.0,2542.5,2518.0,2542.5,2510.0,2542.4,2518.0,2542.4,2007.0,2542.3,2518.0,2542.3,2494.0,2542.2,2518.0,2542.2,2519.0,2542.1,2430.0,2542.0,2518.0,2542.0] || equal(e22,e22) equal(e23,e23) equal(e22,e22) equal(e21,e21) equal(e23,e23) equal(e20,e20) equal(op2(e20,e23),e23)** equal(e20,e20) -> . % 0.71/0.90 2544[14:Obv:2543.7] || equal(op2(e20,e23),e23)** -> . % 0.71/0.90 2545[14:Rew:2478.0,2544.0] || equal(e23,e23)* -> . % 0.71/0.90 2546[14:Obv:2545.0] || -> . % 0.71/0.90 2547[14:Spt:2546.0,727.0,2510.0] || equal(op2(e23,e20),e23)** -> . % 0.71/0.90 2548[14:Spt:2546.0,727.1] || -> equal(op2(e23,e20),e20)**. % 0.71/0.90 2555[14:Rew:2548.0,2445.0] || equal(h3(e10),e20)** -> . % 0.71/0.90 2557[14:MRR:2451.1,2555.0] || -> equal(h3(e10),e23)**. % 0.71/0.90 2563[14:Rew:2557.0,2452.0] || -> equal(e23,e20) equal(op2(e21,e22),e20)**. % 0.71/0.90 2564[14:MRR:2563.0,9.0] || -> equal(op2(e21,e22),e20)**. % 0.71/0.90 2569[14:Rew:2548.0,2431.0] || -> equal(e23,e20) equal(op2(e21,e20),e23)**. % 0.71/0.90 2570[14:MRR:2569.0,9.0] || -> equal(op2(e21,e20),e23)**. % 0.71/0.90 2574[14:Rew:2570.0,2504.1,2564.0,2504.1,34.0,2504.0,2557.0,2504.0] || -> equal(e23,e21)** equal(e23,e21)**. % 0.71/0.90 2575[14:Obv:2574.0] || -> equal(e23,e21)**. % 0.71/0.90 2576[14:MRR:2575.0,11.0] || -> . % 0.71/0.90 2581[13:Spt:2576.0,735.0,2478.0] || equal(op2(e20,e23),e23)** -> . % 0.71/0.90 2582[13:Spt:2576.0,735.1] || -> equal(op2(e20,e23),e22)**. % 0.71/0.90 2586[13:Rew:2582.0,136.1] || SkC27* -> equal(e23,e22). % 0.71/0.90 2587[13:MRR:2586.1,12.0] || SkC27* -> . % 0.71/0.90 2588[13:MRR:2389.0,2587.0] || -> SkC23*. % 0.71/0.90 2589[13:MRR:129.0,2588.0] || -> equal(op2(e20,e22),e22)**. % 0.71/0.90 2596[13:Rew:2589.0,203.0] || equal(op2(e21,e22),e22)** -> . % 0.71/0.90 2597[13:Rew:2582.0,679.1] || -> equal(op2(e21,e23),e23)** equal(e23,e22). % 0.71/0.90 2598[13:MRR:2597.1,12.0] || -> equal(op2(e21,e23),e23)**. % 0.71/0.90 2602[13:Rew:2598.0,226.0] || equal(op2(e21,e22),e23)** -> . % 0.71/0.90 2603[13:Rew:2598.0,223.0] || equal(op2(e21,e20),e23)** -> . % 0.71/0.90 2605[13:MRR:2450.1,2603.0] || -> equal(op2(e21,e20),e20)**. % 0.71/0.90 2614[13:Rew:2605.0,222.0] || equal(op2(e21,e22),e20)** -> . % 0.71/0.90 2632[13:MRR:2421.0,2421.1,2421.2,2596.0,2602.0,2614.0] || -> . % 0.71/0.90 2634[12:Spt:2632.0,2359.0,2362.0] || equal(h2(e11),e21)** -> . % 0.71/0.90 2635[12:Spt:2632.0,2359.1] || -> equal(h2(e11),e20)**. % 0.71/0.90 2642[12:Rew:2635.0,2027.0] || equal(h1(e12),e20)** -> . % 0.71/0.90 2647[12:Rew:2635.0,537.0] || -> equal(op2(e21,e20),h2(e12))**. % 0.71/0.90 2650[12:Rew:2635.0,558.1] || SkC23* equal(e20,e20) -> . % 0.71/0.90 2651[12:Obv:2650.1] || SkC23* -> . % 0.71/0.90 2652[12:MRR:2043.1,2651.0] || -> SkC27 SkC21*. % 0.71/0.90 2653[12:Rew:2635.0,545.1] || SkC27* equal(e20,e20) -> . % 0.71/0.90 2654[12:Obv:2653.1] || SkC27* -> . % 0.71/0.90 2655[12:MRR:2652.0,2654.0] || -> SkC21*. % 0.71/0.90 2659[12:MRR:124.0,2655.0] || -> equal(op2(e21,e22),e21)**. % 0.71/0.90 2661[12:MRR:561.0,2655.0] || equal(h3(e11),e22)** -> . % 0.71/0.90 2671[12:MRR:2049.0,2642.0] || -> equal(h1(e12),e23)**. % 0.71/0.90 2677[12:Rew:2671.0,2028.0] || equal(op2(e20,e23),e23)** -> . % 0.71/0.90 2682[12:Rew:2647.0,194.0] || equal(op2(e22,e20),h2(e12))** -> . % 0.71/0.90 2686[12:MRR:692.0,2661.0] || -> equal(op2(e22,e20),e22)**. % 0.71/0.90 2690[12:Rew:2686.0,2682.0] || equal(h2(e12),e22)** -> . % 0.71/0.90 2699[12:MRR:679.1,2677.0] || -> equal(op2(e21,e23),e23)**. % 0.71/0.90 2731[12:Rew:2647.0,703.2,2699.0,703.1,2659.0,703.0] || -> equal(e22,e21) equal(e23,e22) equal(h2(e12),e22)**. % 0.71/0.90 2732[12:MRR:2731.0,2731.1,2731.2,10.0,12.0,2690.0] || -> . % 0.71/0.90 2761[10:Spt:2732.0,777.0,2171.0] || equal(op1(e10,e13),e13)** -> . % 0.71/0.90 2762[10:Spt:2732.0,777.1] || -> equal(op1(e10,e13),e12)**. % 0.71/0.90 2766[10:Rew:2762.0,109.1] || SkC12* -> equal(e13,e12). % 0.71/0.90 2767[10:MRR:2766.1,6.0] || SkC12* -> . % 0.71/0.90 2768[10:MRR:2136.0,2767.0] || -> SkC8*. % 0.71/0.90 2769[10:MRR:102.0,2768.0] || -> equal(op1(e10,e12),e12)**. % 0.71/0.90 2776[10:Rew:2762.0,739.1] || -> equal(op1(e11,e13),e13)** equal(e13,e12). % 0.71/0.90 2777[10:MRR:2776.1,6.0] || -> equal(op1(e11,e13),e13)**. % 0.71/0.90 2781[10:Rew:2777.0,178.0] || equal(op1(e11,e12),e13)** -> . % 0.71/0.90 2788[10:Rew:2769.0,2156.1] || -> equal(op1(e11,e12),e13)** equal(e13,e12). % 0.71/0.90 2789[10:MRR:2788.0,2788.1,2781.0,6.0] || -> . % 0.71/0.90 2799[8:Spt:2789.0,1999.0,2002.0] || equal(h1(e11),e21)** -> . % 0.71/0.90 2800[8:Spt:2789.0,1999.1] || -> equal(h1(e11),e20)**. % 0.71/0.90 2806[8:Rew:2800.0,633.0] || equal(op2(e21,e20),e20)** -> . % 0.71/0.90 2809[8:Rew:2800.0,631.0] || equal(op2(e23,e20),e20)** -> . % 0.71/0.90 2810[8:MRR:727.1,2809.0] || -> equal(op2(e23,e20),e23)**. % 0.71/0.90 2814[8:Rew:2810.0,195.0] || equal(op2(e21,e20),e23)** -> . % 0.71/0.90 2830[8:Rew:2800.0,619.0] || equal(op2(e20,e21),e20)** -> . % 0.71/0.90 2840[8:Rew:2800.0,546.1] || SkC27* equal(e20,e20) -> . % 0.71/0.90 2841[8:Obv:2840.1] || SkC27* -> . % 0.71/0.90 2842[8:MRR:675.0,2841.0] || -> SkC23 SkC21 SkC19*. % 0.71/0.90 2843[8:Rew:2800.0,559.1] || SkC23* equal(e20,e20) -> . % 0.71/0.90 2844[8:Obv:2843.1] || SkC23* -> . % 0.71/0.90 2845[8:MRR:2842.0,2844.0] || -> SkC21 SkC19*. % 0.71/0.90 2846[8:Rew:2800.0,569.1] || SkC19* equal(e20,e20) -> . % 0.71/0.90 2847[8:Obv:2846.1] || SkC19* -> . % 0.71/0.90 2848[8:MRR:2845.1,2847.0] || -> SkC21*. % 0.71/0.90 2850[8:MRR:124.0,2848.0] || -> equal(op2(e21,e22),e21)**. % 0.71/0.90 2851[8:MRR:561.0,2848.0] || equal(h3(e11),e22)** -> . % 0.71/0.90 2861[8:Rew:2850.0,222.0] || equal(op2(e21,e20),e21)** -> . % 0.71/0.90 2865[8:MRR:692.0,2851.0] || -> equal(op2(e22,e20),e22)**. % 0.71/0.90 2870[8:Rew:2865.0,194.0] || equal(op2(e21,e20),e22)** -> . % 0.71/0.90 2892[8:MRR:709.1,2830.0] || -> equal(h2(e11),e20)**. % 0.71/0.90 2898[8:Rew:2892.0,537.0] || -> equal(op2(e21,e20),h2(e12))**. % 0.71/0.90 2903[8:Rew:2898.0,2806.0] || equal(h2(e12),e20)** -> . % 0.71/0.90 2904[8:Rew:2898.0,2814.0] || equal(h2(e12),e23)** -> . % 0.71/0.90 2905[8:Rew:2898.0,2861.0] || equal(h2(e12),e21)** -> . % 0.71/0.90 2906[8:Rew:2898.0,2870.0] || equal(h2(e12),e22)** -> . % 0.71/0.90 2936[8:Rew:2898.0,414.3,2898.0,414.2,2898.0,414.1,2898.0,414.0] || -> equal(h2(e12),e21) equal(h2(e12),e20) equal(h2(e12),e23)** equal(h2(e12),e22). % 0.71/0.90 2937[8:MRR:2936.0,2936.1,2936.2,2936.3,2905.0,2903.0,2904.0,2906.0] || -> . % 0.71/0.90 % SZS output end Refutation % 0.71/0.90 Formulae used in the proof : ax7 ax8 ax16 ax12 ax13 co1 ax14 ax15 ax10 ax11 ax5 ax6 ax4 ax3 ax2 ax1 % 0.71/0.90 %------------------------------------------------------------------------------