%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG046+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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:06 EDT 2022 % Result : Unsatisfiable 0.40s 0.57s % Output : Refutation 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG046+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n017.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Wed Jun 8 04:14:18 EDT 2022 % 0.14/0.34 % CPUTime : % 0.40/0.57 % 0.40/0.57 SPASS V 3.9 % 0.40/0.57 SPASS beiseite: Proof found. % 0.40/0.57 % SZS status Theorem % 0.40/0.57 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.40/0.57 SPASS derived 980 clauses, backtracked 1089 clauses, performed 15 splits and kept 1224 clauses. % 0.40/0.57 SPASS allocated 86204 KBytes. % 0.40/0.57 SPASS spent 0:00:00.22 on the problem. % 0.40/0.57 0:00:00.04 for the input. % 0.40/0.57 0:00:00.04 for the FLOTTER CNF translation. % 0.40/0.57 0:00:00.00 for inferences. % 0.40/0.57 0:00:00.00 for the backtracking. % 0.40/0.57 0:00:00.11 for the reduction. % 0.40/0.57 % 0.40/0.57 % 0.40/0.57 Here is a proof with depth 3, length 583 : % 0.40/0.57 % SZS output start Refutation % 0.40/0.57 1[0:Inp] || equal(e1,e0)** -> . % 0.40/0.57 2[0:Inp] || equal(e2,e0)** -> . % 0.40/0.57 3[0:Inp] || equal(e3,e0)** -> . % 0.40/0.57 4[0:Inp] || equal(e2,e1)** -> . % 0.40/0.57 5[0:Inp] || equal(e3,e1)** -> . % 0.40/0.57 6[0:Inp] || equal(e3,e2)** -> . % 0.40/0.57 7[0:Inp] || -> equal(op(unit,e0),e0)**. % 0.40/0.57 8[0:Inp] || -> equal(op(e0,unit),e0)**. % 0.40/0.57 9[0:Inp] || -> equal(op(unit,e1),e1)**. % 0.40/0.57 10[0:Inp] || -> equal(op(e1,unit),e1)**. % 0.40/0.57 11[0:Inp] || -> equal(op(unit,e2),e2)**. % 0.40/0.57 12[0:Inp] || -> equal(op(e2,unit),e2)**. % 0.40/0.57 13[0:Inp] || -> equal(op(unit,e3),e3)**. % 0.40/0.57 14[0:Inp] || -> equal(op(e3,unit),e3)**. % 0.40/0.57 15[0:Inp] || equal(op(e1,e0),op(e0,e0))** -> . % 0.40/0.57 16[0:Inp] || equal(op(e2,e0),op(e0,e0))** -> . % 0.40/0.57 17[0:Inp] || equal(op(e3,e0),op(e0,e0))** -> . % 0.40/0.57 18[0:Inp] || equal(op(e2,e0),op(e1,e0))** -> . % 0.40/0.57 19[0:Inp] || equal(op(e3,e0),op(e1,e0))** -> . % 0.40/0.57 20[0:Inp] || equal(op(e3,e0),op(e2,e0))** -> . % 0.40/0.57 21[0:Inp] || equal(op(e1,e1),op(e0,e1))** -> . % 0.40/0.57 22[0:Inp] || equal(op(e2,e1),op(e0,e1))** -> . % 0.40/0.57 23[0:Inp] || equal(op(e3,e1),op(e0,e1))** -> . % 0.40/0.57 25[0:Inp] || equal(op(e3,e1),op(e1,e1))** -> . % 0.40/0.57 26[0:Inp] || equal(op(e3,e1),op(e2,e1))** -> . % 0.40/0.57 27[0:Inp] || equal(op(e1,e2),op(e0,e2))** -> . % 0.40/0.57 28[0:Inp] || equal(op(e2,e2),op(e0,e2))** -> . % 0.40/0.57 29[0:Inp] || equal(op(e3,e2),op(e0,e2))** -> . % 0.40/0.57 30[0:Inp] || equal(op(e2,e2),op(e1,e2))** -> . % 0.40/0.57 31[0:Inp] || equal(op(e3,e2),op(e1,e2))** -> . % 0.40/0.57 32[0:Inp] || equal(op(e3,e2),op(e2,e2))** -> . % 0.40/0.57 33[0:Inp] || equal(op(e1,e3),op(e0,e3))** -> . % 0.40/0.57 35[0:Inp] || equal(op(e3,e3),op(e0,e3))** -> . % 0.40/0.57 36[0:Inp] || equal(op(e2,e3),op(e1,e3))** -> . % 0.40/0.57 37[0:Inp] || equal(op(e3,e3),op(e1,e3))** -> . % 0.40/0.57 38[0:Inp] || equal(op(e3,e3),op(e2,e3))** -> . % 0.40/0.57 39[0:Inp] || equal(op(e0,e1),op(e0,e0))** -> . % 0.40/0.57 40[0:Inp] || equal(op(e0,e2),op(e0,e0))** -> . % 0.40/0.57 41[0:Inp] || equal(op(e0,e3),op(e0,e0))** -> . % 0.40/0.57 42[0:Inp] || equal(op(e0,e2),op(e0,e1))** -> . % 0.40/0.57 43[0:Inp] || equal(op(e0,e3),op(e0,e1))** -> . % 0.40/0.57 44[0:Inp] || equal(op(e0,e3),op(e0,e2))** -> . % 0.40/0.57 45[0:Inp] || equal(op(e1,e1),op(e1,e0))** -> . % 0.40/0.57 46[0:Inp] || equal(op(e1,e2),op(e1,e0))** -> . % 0.40/0.57 47[0:Inp] || equal(op(e1,e3),op(e1,e0))** -> . % 0.40/0.57 48[0:Inp] || equal(op(e1,e2),op(e1,e1))** -> . % 0.40/0.57 49[0:Inp] || equal(op(e1,e3),op(e1,e1))** -> . % 0.40/0.57 50[0:Inp] || equal(op(e1,e3),op(e1,e2))** -> . % 0.40/0.57 51[0:Inp] || equal(op(e2,e1),op(e2,e0))** -> . % 0.40/0.57 52[0:Inp] || equal(op(e2,e2),op(e2,e0))** -> . % 0.40/0.57 53[0:Inp] || equal(op(e2,e3),op(e2,e0))** -> . % 0.40/0.57 55[0:Inp] || equal(op(e2,e3),op(e2,e1))** -> . % 0.40/0.57 56[0:Inp] || equal(op(e2,e3),op(e2,e2))** -> . % 0.40/0.57 57[0:Inp] || equal(op(e3,e1),op(e3,e0))** -> . % 0.40/0.57 58[0:Inp] || equal(op(e3,e2),op(e3,e0))** -> . % 0.40/0.57 59[0:Inp] || equal(op(e3,e3),op(e3,e0))** -> . % 0.40/0.57 60[0:Inp] || equal(op(e3,e2),op(e3,e1))** -> . % 0.40/0.58 61[0:Inp] || equal(op(e3,e3),op(e3,e1))** -> . % 0.40/0.58 62[0:Inp] || equal(op(e3,e3),op(e3,e2))** -> . % 0.40/0.58 63[0:Inp] || -> equal(e3,unit)** equal(e2,unit) equal(e1,unit) equal(e0,unit). % 0.40/0.58 66[0:Inp] || -> equal(op(e3,e3),e2)** equal(op(e2,e3),e2) equal(op(e1,e3),e2) equal(op(e0,e3),e2). % 0.40/0.58 67[0:Inp] || -> equal(op(e3,e3),e2)** equal(op(e3,e2),e2) equal(op(e3,e1),e2) equal(op(e3,e0),e2). % 0.40/0.58 68[0:Inp] || -> equal(op(e3,e3),e1)** equal(op(e1,e3),e1) equal(op(e2,e3),e1) equal(op(e0,e3),e1). % 0.40/0.58 69[0:Inp] || -> equal(op(e3,e3),e1)** equal(op(e3,e1),e1) equal(op(e3,e2),e1) equal(op(e3,e0),e1). % 0.40/0.58 70[0:Inp] || -> equal(op(e3,e3),e0)** equal(op(e0,e3),e0) equal(op(e2,e3),e0) equal(op(e1,e3),e0). % 0.40/0.58 71[0:Inp] || -> equal(op(e3,e3),e0)** equal(op(e3,e0),e0) equal(op(e3,e2),e0) equal(op(e3,e1),e0). % 0.40/0.58 76[0:Inp] || -> equal(op(e2,e2),e1) equal(op(e1,e2),e1) equal(op(e3,e2),e1)** equal(op(e0,e2),e1). % 0.40/0.58 78[0:Inp] || -> equal(op(e2,e2),e0) equal(op(e0,e2),e0) equal(op(e3,e2),e0)** equal(op(e1,e2),e0). % 0.40/0.58 79[0:Inp] || -> equal(op(e2,e2),e0) equal(op(e2,e0),e0) equal(op(e2,e3),e0)** equal(op(e2,e1),e0). % 0.40/0.58 80[0:Inp] || -> equal(op(e3,e1),e3)** equal(op(e1,e1),e3) equal(op(e2,e1),e3) equal(op(e0,e1),e3). % 0.40/0.58 81[0:Inp] || -> equal(op(e1,e3),e3)** equal(op(e1,e1),e3) equal(op(e1,e2),e3) equal(op(e1,e0),e3). % 0.40/0.58 82[0:Inp] || -> equal(op(e2,e1),e2) equal(op(e1,e1),e2) equal(op(e3,e1),e2)** equal(op(e0,e1),e2). % 0.40/0.58 83[0:Inp] || -> equal(op(e1,e2),e2) equal(op(e1,e1),e2) equal(op(e1,e3),e2)** equal(op(e1,e0),e2). % 0.40/0.58 87[0:Inp] || -> equal(op(e1,e1),e0) equal(op(e1,e0),e0) equal(op(e1,e3),e0)** equal(op(e1,e2),e0). % 0.40/0.58 88[0:Inp] || -> equal(op(e3,e0),e3)** equal(op(e0,e0),e3) equal(op(e2,e0),e3) equal(op(e1,e0),e3). % 0.40/0.58 90[0:Inp] || -> equal(op(e2,e0),e2) equal(op(e0,e0),e2) equal(op(e3,e0),e2)** equal(op(e1,e0),e2). % 0.40/0.58 91[0:Inp] || -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e3),e2)** equal(op(e0,e1),e2). % 0.40/0.58 93[0:Inp] || -> equal(op(e0,e1),e1) equal(op(e0,e0),e1) equal(op(e0,e3),e1)** equal(op(e0,e2),e1). % 0.40/0.58 96[0:Inp] || -> equal(op(e3,e3),e3)** equal(op(e3,e3),e2) equal(op(e3,e3),e1) equal(op(e3,e3),e0). % 0.40/0.58 97[0:Inp] || -> equal(op(e3,e2),e3)** equal(op(e3,e2),e2) equal(op(e3,e2),e1) equal(op(e3,e2),e0). % 0.40/0.58 98[0:Inp] || -> equal(op(e3,e1),e3)** equal(op(e3,e1),e1) equal(op(e3,e1),e2) equal(op(e3,e1),e0). % 0.40/0.58 99[0:Inp] || -> equal(op(e3,e0),e3)** equal(op(e3,e0),e0) equal(op(e3,e0),e2) equal(op(e3,e0),e1). % 0.40/0.58 100[0:Inp] || -> equal(op(e2,e3),e3)** equal(op(e2,e3),e2) equal(op(e2,e3),e1) equal(op(e2,e3),e0). % 0.40/0.58 101[0:Inp] || -> equal(op(e2,e2),e2) equal(op(e2,e2),e3)** equal(op(e2,e2),e1) equal(op(e2,e2),e0). % 0.40/0.58 104[0:Inp] || -> equal(op(e1,e3),e3)** equal(op(e1,e3),e1) equal(op(e1,e3),e2) equal(op(e1,e3),e0). % 0.40/0.58 105[0:Inp] || -> equal(op(e1,e2),e2) equal(op(e1,e2),e1) equal(op(e1,e2),e3)** equal(op(e1,e2),e0). % 0.40/0.58 106[0:Inp] || -> equal(op(e1,e1),e1) equal(op(e1,e1),e3)** equal(op(e1,e1),e2) equal(op(e1,e1),e0). % 0.40/0.58 109[0:Inp] || -> equal(op(e0,e2),e2) equal(op(e0,e2),e0) equal(op(e0,e2),e3)** equal(op(e0,e2),e1). % 0.40/0.58 110[0:Inp] || -> equal(op(e0,e1),e1) equal(op(e0,e1),e0) equal(op(e0,e1),e3)** equal(op(e0,e1),e2). % 0.40/0.58 111[0:Inp] || -> equal(op(e0,e0),e0) equal(op(e0,e0),e3)** equal(op(e0,e0),e2) equal(op(e0,e0),e1). % 0.40/0.58 114[0:Inp] || equal(op(e1,e1),e0) equal(op(e1,op(e1,e1)),e2) equal(op(e1,op(e1,op(e1,e1))),e3)** -> . % 0.40/0.58 116[0:Inp] || equal(op(e0,e0),e1) equal(op(e0,op(e0,e0)),e2) equal(op(e0,op(e0,op(e0,e0))),e3)** -> . % 0.40/0.58 117[0:Inp] || equal(op(e0,e0),e2) equal(op(e0,op(e0,e0)),e1) equal(op(e0,op(e0,op(e0,e0))),e3)** -> . % 0.40/0.58 118[0:Inp] || equal(op(e3,e3),e0) equal(op(e3,op(e3,e3)),e1) equal(op(e3,op(e3,op(e3,e3))),e2)** -> . % 0.40/0.58 119[0:Inp] || equal(op(e3,e3),e1) equal(op(e3,op(e3,e3)),e0) equal(op(e3,op(e3,op(e3,e3))),e2)** -> . % 0.40/0.58 123[0:Inp] || equal(op(e0,e0),e3) equal(op(e0,op(e0,e0)),e1) equal(op(e0,op(e0,op(e0,e0))),e2)** -> . % 0.40/0.58 125[0:Inp] || equal(op(e3,e3),e2) equal(op(e3,op(e3,e3)),e0) equal(op(e3,op(e3,op(e3,e3))),e1)** -> . % 0.40/0.58 126[0:Inp] || equal(op(e2,e2),e0) equal(op(e2,op(e2,e2)),e3) equal(op(e2,op(e2,op(e2,e2))),e1)** -> . % 0.40/0.58 129[0:Inp] || equal(op(e0,e0),e3) equal(op(e0,op(e0,e0)),e2) equal(op(e0,op(e0,op(e0,e0))),e1)** -> . % 0.40/0.58 130[0:Inp] || equal(op(e3,e3),e1) equal(op(e3,op(e3,e3)),e2) equal(op(e3,op(e3,op(e3,e3))),e0)** -> . % 0.40/0.58 131[0:Inp] || equal(op(e3,e3),e2) equal(op(e3,op(e3,e3)),e1) equal(op(e3,op(e3,op(e3,e3))),e0)** -> . % 0.40/0.58 135[0:Inp] || equal(op(e1,e1),e3) equal(op(e1,op(e1,e1)),e2) equal(op(e1,op(e1,op(e1,e1))),e0)** -> . % 0.40/0.58 136[0:Inp] || equal(op(e3,e3),e3)** equal(op(e2,e2),e3) equal(op(e1,e1),e3) equal(op(e0,e0),e3) -> . % 0.40/0.58 137[0:Inp] || equal(op(e2,e2),e2) equal(op(e3,e3),e2)** equal(op(e1,e1),e2) equal(op(e0,e0),e2) -> . % 0.40/0.58 138[0:Inp] || equal(op(e1,e1),e1) equal(op(e3,e3),e1)** equal(op(e2,e2),e1) equal(op(e0,e0),e1) -> . % 0.40/0.58 139[0:Inp] || equal(op(e0,e0),e0) equal(op(e3,e3),e0)** equal(op(e2,e2),e0) equal(op(e1,e1),e0) -> . % 0.40/0.58 140[1:Spt:63.0] || -> equal(e3,unit)**. % 0.40/0.58 145[1:Rew:140.0,76.2] || -> equal(op(e2,e2),e1)** equal(op(e1,e2),e1) equal(op(unit,e2),e1) equal(op(e0,e2),e1). % 0.40/0.58 147[1:Rew:140.0,78.2] || -> equal(op(e2,e2),e0)** equal(op(e0,e2),e0) equal(op(unit,e2),e0) equal(op(e1,e2),e0). % 0.40/0.58 148[1:Rew:140.0,32.0] || equal(op(e2,e2),op(unit,e2))** -> . % 0.40/0.58 149[1:Rew:140.0,31.0] || equal(op(e1,e2),op(unit,e2))** -> . % 0.40/0.58 150[1:Rew:140.0,29.0] || equal(op(e0,e2),op(unit,e2))** -> . % 0.40/0.58 165[1:Rew:140.0,82.2] || -> equal(op(e2,e1),e2)** equal(op(e1,e1),e2) equal(op(unit,e1),e2) equal(op(e0,e1),e2). % 0.40/0.58 172[1:Rew:140.0,25.0] || equal(op(e1,e1),op(unit,e1))** -> . % 0.40/0.58 173[1:Rew:140.0,23.0] || equal(op(e0,e1),op(unit,e1))** -> . % 0.40/0.58 174[1:Rew:140.0,90.2] || -> equal(op(e2,e0),e2)** equal(op(e0,e0),e2) equal(op(unit,e0),e2) equal(op(e1,e0),e2). % 0.40/0.58 182[1:Rew:140.0,19.0] || equal(op(e1,e0),op(unit,e0))** -> . % 0.40/0.58 183[1:Rew:140.0,17.0] || equal(op(e0,e0),op(unit,e0))** -> . % 0.40/0.58 189[1:Rew:140.0,55.0] || equal(op(e2,e1),op(e2,unit))** -> . % 0.40/0.58 190[1:Rew:140.0,53.0] || equal(op(e2,e0),op(e2,unit))** -> . % 0.40/0.58 195[1:Rew:140.0,87.2] || -> equal(op(e1,e1),e0) equal(op(e1,e0),e0) equal(op(e1,unit),e0) equal(op(e1,e2),e0)**. % 0.40/0.58 196[1:Rew:140.0,50.0] || equal(op(e1,e2),op(e1,unit))** -> . % 0.40/0.58 203[1:Rew:140.0,93.2] || -> equal(op(e0,e1),e1) equal(op(e0,e0),e1) equal(op(e0,unit),e1) equal(op(e0,e2),e1)**. % 0.40/0.58 205[1:Rew:140.0,44.0] || equal(op(e0,e2),op(e0,unit))** -> . % 0.40/0.58 206[1:Rew:140.0,43.0] || equal(op(e0,e1),op(e0,unit))** -> . % 0.40/0.58 215[1:Rew:140.0,136.0] || equal(op(unit,unit),unit) equal(op(e2,e2),e3)** equal(op(e1,e1),e3) equal(op(e0,e0),e3) -> . % 0.40/0.58 220[1:Rew:140.0,109.2] || -> equal(op(e0,e2),e2)** equal(op(e0,e2),e0) equal(op(e0,e2),unit) equal(op(e0,e2),e1). % 0.40/0.58 221[1:Rew:140.0,105.2] || -> equal(op(e1,e2),e2)** equal(op(e1,e2),e1) equal(op(e1,e2),unit) equal(op(e1,e2),e0). % 0.40/0.58 224[1:Rew:140.0,101.1] || -> equal(op(e2,e2),e2)** equal(op(e2,e2),unit) equal(op(e2,e2),e1) equal(op(e2,e2),e0). % 0.40/0.58 227[1:Rew:140.0,110.2] || -> equal(op(e0,e1),e1) equal(op(e0,e1),e0) equal(op(e0,e1),unit) equal(op(e0,e1),e2)**. % 0.40/0.58 230[1:Rew:140.0,106.1] || -> equal(op(e1,e1),e1) equal(op(e1,e1),unit) equal(op(e1,e1),e2)** equal(op(e1,e1),e0). % 0.40/0.58 234[1:Rew:140.0,111.1] || -> equal(op(e0,e0),e0) equal(op(e0,e0),unit) equal(op(e0,e0),e2)** equal(op(e0,e0),e1). % 0.40/0.58 237[1:Rew:140.0,114.2] || equal(op(e1,e1),e0) equal(op(e1,op(e1,e1)),e2) equal(op(e1,op(e1,op(e1,e1))),unit)** -> . % 0.40/0.58 239[1:Rew:140.0,116.2] || equal(op(e0,e0),e1) equal(op(e0,op(e0,e0)),e2) equal(op(e0,op(e0,op(e0,e0))),unit)** -> . % 0.40/0.58 240[1:Rew:140.0,117.2] || equal(op(e0,e0),e2) equal(op(e0,op(e0,e0)),e1) equal(op(e0,op(e0,op(e0,e0))),unit)** -> . % 0.40/0.58 250[1:Rew:140.0,14.0] || -> equal(op(unit,unit),unit)**. % 0.40/0.58 252[1:Rew:11.0,148.0] || equal(op(e2,e2),e2)** -> . % 0.40/0.58 253[1:Rew:11.0,149.0] || equal(op(e1,e2),e2)** -> . % 0.40/0.58 254[1:Rew:11.0,150.0] || equal(op(e0,e2),e2)** -> . % 0.40/0.58 259[1:Rew:9.0,172.0] || equal(op(e1,e1),e1)** -> . % 0.40/0.58 260[1:Rew:9.0,173.0] || equal(op(e0,e1),e1)** -> . % 0.40/0.58 265[1:Rew:7.0,182.0] || equal(op(e1,e0),e0)** -> . % 0.40/0.58 266[1:Rew:7.0,183.0] || equal(op(e0,e0),e0)** -> . % 0.40/0.58 268[1:Rew:12.0,189.0] || equal(op(e2,e1),e2)** -> . % 0.40/0.58 269[1:Rew:12.0,190.0] || equal(op(e2,e0),e2)** -> . % 0.40/0.58 271[1:Rew:10.0,196.0] || equal(op(e1,e2),e1)** -> . % 0.40/0.58 276[1:Rew:8.0,205.0] || equal(op(e0,e2),e0)** -> . % 0.40/0.58 277[1:Rew:8.0,206.0] || equal(op(e0,e1),e0)** -> . % 0.40/0.58 283[1:Rew:11.0,145.2] || -> equal(op(e2,e2),e1)** equal(op(e1,e2),e1) equal(e2,e1) equal(op(e0,e2),e1). % 0.40/0.58 284[1:MRR:283.1,283.2,271.0,4.0] || -> equal(op(e2,e2),e1)** equal(op(e0,e2),e1). % 0.40/0.58 286[1:Rew:11.0,147.2] || -> equal(op(e2,e2),e0)** equal(op(e0,e2),e0) equal(e2,e0) equal(op(e1,e2),e0). % 0.40/0.58 287[1:MRR:286.1,286.2,276.0,2.0] || -> equal(op(e2,e2),e0)** equal(op(e1,e2),e0). % 0.40/0.58 292[1:Rew:9.0,165.2] || -> equal(op(e2,e1),e2)** equal(op(e1,e1),e2) equal(e2,e1) equal(op(e0,e1),e2). % 0.40/0.58 293[1:MRR:292.0,292.2,268.0,4.0] || -> equal(op(e1,e1),e2)** equal(op(e0,e1),e2). % 0.40/0.58 297[1:Rew:7.0,174.2] || -> equal(op(e2,e0),e2)** equal(op(e0,e0),e2) equal(e2,e0) equal(op(e1,e0),e2). % 0.40/0.58 298[1:MRR:297.0,297.2,269.0,2.0] || -> equal(op(e0,e0),e2) equal(op(e1,e0),e2)**. % 0.40/0.58 309[1:Rew:10.0,195.2] || -> equal(op(e1,e1),e0) equal(op(e1,e0),e0) equal(e1,e0) equal(op(e1,e2),e0)**. % 0.40/0.58 310[1:MRR:309.1,309.2,265.0,1.0] || -> equal(op(e1,e1),e0) equal(op(e1,e2),e0)**. % 0.40/0.58 314[1:Rew:8.0,203.2] || -> equal(op(e0,e1),e1) equal(op(e0,e0),e1) equal(e1,e0) equal(op(e0,e2),e1)**. % 0.40/0.58 315[1:MRR:314.0,314.2,260.0,1.0] || -> equal(op(e0,e0),e1) equal(op(e0,e2),e1)**. % 0.40/0.58 329[1:MRR:220.0,220.1,254.0,276.0] || -> equal(op(e0,e2),unit) equal(op(e0,e2),e1)**. % 0.40/0.58 330[1:MRR:221.0,221.1,253.0,271.0] || -> equal(op(e1,e2),unit) equal(op(e1,e2),e0)**. % 0.40/0.58 331[1:MRR:224.0,252.0] || -> equal(op(e2,e2),unit) equal(op(e2,e2),e1)** equal(op(e2,e2),e0). % 0.40/0.58 334[1:MRR:227.0,227.1,260.0,277.0] || -> equal(op(e0,e1),unit) equal(op(e0,e1),e2)**. % 0.40/0.58 335[1:MRR:230.0,259.0] || -> equal(op(e1,e1),unit) equal(op(e1,e1),e2)** equal(op(e1,e1),e0). % 0.40/0.58 337[1:MRR:234.0,266.0] || -> equal(op(e0,e0),unit) equal(op(e0,e0),e2)** equal(op(e0,e0),e1). % 0.40/0.58 344[1:Rew:140.0,215.3,140.0,215.2,140.0,215.1,250.0,215.0] || equal(unit,unit) equal(op(e2,e2),unit)** equal(op(e1,e1),unit) equal(op(e0,e0),unit) -> . % 0.40/0.58 345[1:Obv:344.0] || equal(op(e2,e2),unit)** equal(op(e1,e1),unit) equal(op(e0,e0),unit) -> . % 0.40/0.58 354[2:Spt:284.1] || -> equal(op(e0,e2),e1)**. % 0.40/0.58 359[2:Rew:354.0,40.0] || equal(op(e0,e0),e1)** -> . % 0.40/0.58 360[2:Rew:354.0,28.0] || equal(op(e2,e2),e1)** -> . % 0.40/0.58 364[2:MRR:337.2,359.0] || -> equal(op(e0,e0),unit) equal(op(e0,e0),e2)**. % 0.40/0.58 373[2:MRR:331.1,360.0] || -> equal(op(e2,e2),unit) equal(op(e2,e2),e0)**. % 0.40/0.58 380[3:Spt:287.1] || -> equal(op(e1,e2),e0)**. % 0.40/0.58 384[3:Rew:380.0,48.0] || equal(op(e1,e1),e0)** -> . % 0.40/0.58 385[3:Rew:380.0,30.0] || equal(op(e2,e2),e0)** -> . % 0.40/0.58 389[3:MRR:335.2,384.0] || -> equal(op(e1,e1),unit) equal(op(e1,e1),e2)**. % 0.40/0.58 397[3:MRR:373.1,385.0] || -> equal(op(e2,e2),unit)**. % 0.40/0.58 402[3:Rew:397.0,345.0] || equal(unit,unit) equal(op(e1,e1),unit)** equal(op(e0,e0),unit) -> . % 0.40/0.58 407[3:Obv:402.0] || equal(op(e1,e1),unit)** equal(op(e0,e0),unit) -> . % 0.40/0.58 417[4:Spt:293.0] || -> equal(op(e1,e1),e2)**. % 0.40/0.58 419[4:Rew:417.0,45.0] || equal(op(e1,e0),e2)** -> . % 0.40/0.58 420[4:Rew:417.0,21.0] || equal(op(e0,e1),e2)** -> . % 0.40/0.58 429[4:MRR:298.1,419.0] || -> equal(op(e0,e0),e2)**. % 0.40/0.58 436[4:Rew:429.0,240.0] || equal(e2,e2) equal(op(e0,op(e0,e0)),e1) equal(op(e0,op(e0,op(e0,e0))),unit)** -> . % 0.40/0.58 444[4:MRR:334.1,420.0] || -> equal(op(e0,e1),unit)**. % 0.40/0.58 462[4:Obv:436.0] || equal(op(e0,op(e0,e0)),e1) equal(op(e0,op(e0,op(e0,e0))),unit)** -> . % 0.40/0.58 463[4:Rew:429.0,462.1,429.0,462.0] || equal(op(e0,e2),e1) equal(op(e0,op(e0,e2)),unit)** -> . % 0.40/0.58 464[4:Rew:354.0,463.1,354.0,463.0] || equal(e1,e1) equal(op(e0,e1),unit)** -> . % 0.40/0.58 465[4:Obv:464.0] || equal(op(e0,e1),unit)** -> . % 0.40/0.58 466[4:Rew:444.0,465.0] || equal(unit,unit)* -> . % 0.40/0.58 467[4:Obv:466.0] || -> . % 0.40/0.58 468[4:Spt:467.0,293.0,417.0] || equal(op(e1,e1),e2)** -> . % 0.40/0.58 469[4:Spt:467.0,293.1] || -> equal(op(e0,e1),e2)**. % 0.40/0.58 473[4:Rew:469.0,39.0] || equal(op(e0,e0),e2)** -> . % 0.40/0.58 479[4:MRR:389.1,468.0] || -> equal(op(e1,e1),unit)**. % 0.40/0.58 483[4:MRR:364.1,473.0] || -> equal(op(e0,e0),unit)**. % 0.40/0.58 487[4:Rew:483.0,407.1,479.0,407.0] || equal(unit,unit)* equal(unit,unit)* -> . % 0.40/0.58 488[4:Obv:487.1] || -> . % 0.40/0.58 505[3:Spt:488.0,287.1,380.0] || equal(op(e1,e2),e0)** -> . % 0.40/0.58 506[3:Spt:488.0,287.0] || -> equal(op(e2,e2),e0)**. % 0.40/0.58 511[3:MRR:310.1,505.0] || -> equal(op(e1,e1),e0)**. % 0.40/0.58 517[3:Rew:511.0,293.0] || -> equal(e2,e0) equal(op(e0,e1),e2)**. % 0.40/0.58 519[3:MRR:517.0,2.0] || -> equal(op(e0,e1),e2)**. % 0.40/0.58 522[3:Rew:519.0,39.0] || equal(op(e0,e0),e2)** -> . % 0.40/0.58 525[3:MRR:298.0,522.0] || -> equal(op(e1,e0),e2)**. % 0.40/0.58 536[3:MRR:330.1,505.0] || -> equal(op(e1,e2),unit)**. % 0.40/0.58 559[3:Rew:536.0,237.2,525.0,237.2,511.0,237.2,525.0,237.1,511.0,237.1,511.0,237.0] || equal(e0,e0) equal(e2,e2)* equal(unit,unit) -> . % 0.40/0.58 560[3:Obv:559.2] || -> . % 0.40/0.58 575[2:Spt:560.0,284.1,354.0] || equal(op(e0,e2),e1)** -> . % 0.40/0.58 576[2:Spt:560.0,284.0] || -> equal(op(e2,e2),e1)**. % 0.40/0.58 595[2:MRR:315.1,575.0] || -> equal(op(e0,e0),e1)**. % 0.40/0.58 601[2:Rew:595.0,298.0] || -> equal(e2,e1) equal(op(e1,e0),e2)**. % 0.40/0.58 603[2:MRR:601.0,4.0] || -> equal(op(e1,e0),e2)**. % 0.40/0.58 606[2:Rew:603.0,45.0] || equal(op(e1,e1),e2)** -> . % 0.40/0.58 608[2:MRR:293.0,606.0] || -> equal(op(e0,e1),e2)**. % 0.40/0.58 613[2:MRR:329.1,575.0] || -> equal(op(e0,e2),unit)**. % 0.40/0.58 634[2:Rew:613.0,239.2,608.0,239.2,595.0,239.2,608.0,239.1,595.0,239.1,595.0,239.0] || equal(e1,e1) equal(e2,e2)* equal(unit,unit) -> . % 0.40/0.58 635[2:Obv:634.2] || -> . % 0.40/0.58 658[1:Spt:635.0,63.0,140.0] || equal(e3,unit)** -> . % 0.40/0.58 659[1:Spt:635.0,63.1,63.2,63.3] || -> equal(e2,unit)** equal(e1,unit) equal(e0,unit). % 0.40/0.58 660[2:Spt:659.0] || -> equal(e2,unit)**. % 0.40/0.58 663[2:Rew:660.0,12.0] || -> equal(op(unit,unit),unit)**. % 0.40/0.58 667[2:Rew:660.0,48.0] || equal(op(e1,e1),op(e1,unit))** -> . % 0.40/0.58 668[2:Rew:660.0,50.0] || equal(op(e1,e3),op(e1,unit))** -> . % 0.40/0.58 672[2:Rew:660.0,87.3] || -> equal(op(e1,e1),e0) equal(op(e1,e0),e0) equal(op(e1,e3),e0)** equal(op(e1,unit),e0). % 0.40/0.58 675[2:Rew:660.0,81.2] || -> equal(op(e1,e3),e3)** equal(op(e1,e1),e3) equal(op(e1,unit),e3) equal(op(e1,e0),e3). % 0.40/0.58 691[2:Rew:660.0,22.0] || equal(op(e0,e1),op(unit,e1))** -> . % 0.40/0.58 693[2:Rew:660.0,26.0] || equal(op(e3,e1),op(unit,e1))** -> . % 0.40/0.58 700[2:Rew:660.0,40.0] || equal(op(e0,e0),op(e0,unit))** -> . % 0.40/0.58 701[2:Rew:660.0,42.0] || equal(op(e0,e1),op(e0,unit))** -> . % 0.40/0.58 702[2:Rew:660.0,44.0] || equal(op(e0,e3),op(e0,unit))** -> . % 0.40/0.58 704[2:Rew:660.0,93.3] || -> equal(op(e0,e1),e1) equal(op(e0,e0),e1) equal(op(e0,e3),e1)** equal(op(e0,unit),e1). % 0.40/0.58 710[2:Rew:660.0,18.0] || equal(op(e1,e0),op(unit,e0))** -> . % 0.40/0.58 711[2:Rew:660.0,20.0] || equal(op(e3,e0),op(unit,e0))** -> . % 0.40/0.58 715[2:Rew:660.0,88.2] || -> equal(op(e3,e0),e3)** equal(op(e0,e0),e3) equal(op(unit,e0),e3) equal(op(e1,e0),e3). % 0.40/0.58 717[2:Rew:660.0,36.0] || equal(op(e1,e3),op(unit,e3))** -> . % 0.40/0.58 718[2:Rew:660.0,38.0] || equal(op(e3,e3),op(unit,e3))** -> . % 0.40/0.58 723[2:Rew:660.0,68.2] || -> equal(op(e3,e3),e1)** equal(op(e1,e3),e1) equal(op(unit,e3),e1) equal(op(e0,e3),e1). % 0.40/0.58 724[2:Rew:660.0,70.2] || -> equal(op(e3,e3),e0)** equal(op(e0,e3),e0) equal(op(unit,e3),e0) equal(op(e1,e3),e0). % 0.40/0.58 726[2:Rew:660.0,58.0] || equal(op(e3,e0),op(e3,unit))** -> . % 0.40/0.58 727[2:Rew:660.0,60.0] || equal(op(e3,e1),op(e3,unit))** -> . % 0.40/0.58 734[2:Rew:660.0,69.2] || -> equal(op(e3,e3),e1)** equal(op(e3,e1),e1) equal(op(e3,unit),e1) equal(op(e3,e0),e1). % 0.40/0.58 735[2:Rew:660.0,71.2] || -> equal(op(e3,e3),e0)** equal(op(e3,e0),e0) equal(op(e3,unit),e0) equal(op(e3,e1),e0). % 0.40/0.58 736[2:Rew:660.0,137.1] || equal(op(e2,e2),e2) equal(op(e3,e3),unit)** equal(op(e1,e1),e2) equal(op(e0,e0),e2) -> . % 0.40/0.58 739[2:Rew:660.0,96.1] || -> equal(op(e3,e3),e3)** equal(op(e3,e3),unit) equal(op(e3,e3),e1) equal(op(e3,e3),e0). % 0.40/0.58 743[2:Rew:660.0,98.2] || -> equal(op(e3,e1),e3)** equal(op(e3,e1),e1) equal(op(e3,e1),unit) equal(op(e3,e1),e0). % 0.40/0.58 745[2:Rew:660.0,99.2] || -> equal(op(e3,e0),e3)** equal(op(e3,e0),e0) equal(op(e3,e0),unit) equal(op(e3,e0),e1). % 0.40/0.58 754[2:Rew:660.0,106.2] || -> equal(op(e1,e1),e1) equal(op(e1,e1),e3)** equal(op(e1,e1),unit) equal(op(e1,e1),e0). % 0.40/0.58 755[2:Rew:660.0,110.3] || -> equal(op(e0,e1),e1) equal(op(e0,e1),e0) equal(op(e0,e1),e3)** equal(op(e0,e1),unit). % 0.40/0.58 758[2:Rew:660.0,111.2] || -> equal(op(e0,e0),e0) equal(op(e0,e0),e3)** equal(op(e0,e0),unit) equal(op(e0,e0),e1). % 0.40/0.58 760[2:Rew:660.0,118.2] || equal(op(e3,e3),e0) equal(op(e3,op(e3,e3)),e1) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.58 761[2:Rew:660.0,119.2] || equal(op(e3,e3),e1) equal(op(e3,op(e3,e3)),e0) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.58 769[2:Rew:660.0,123.2] || equal(op(e0,e0),e3) equal(op(e0,op(e0,e0)),e1) equal(op(e0,op(e0,op(e0,e0))),unit)** -> . % 0.40/0.58 773[2:Rew:10.0,667.0] || equal(op(e1,e1),e1)** -> . % 0.40/0.58 774[2:Rew:10.0,668.0] || equal(op(e1,e3),e1)** -> . % 0.40/0.58 779[2:Rew:9.0,691.0] || equal(op(e0,e1),e1)** -> . % 0.40/0.58 781[2:Rew:9.0,693.0] || equal(op(e3,e1),e1)** -> . % 0.40/0.58 785[2:Rew:8.0,700.0] || equal(op(e0,e0),e0)** -> . % 0.40/0.58 786[2:Rew:8.0,701.0] || equal(op(e0,e1),e0)** -> . % 0.40/0.58 787[2:Rew:8.0,702.0] || equal(op(e0,e3),e0)** -> . % 0.40/0.58 792[2:Rew:7.0,710.0] || equal(op(e1,e0),e0)** -> . % 0.40/0.58 793[2:Rew:7.0,711.0] || equal(op(e3,e0),e0)** -> . % 0.40/0.58 795[2:Rew:13.0,717.0] || equal(op(e1,e3),e3)** -> . % 0.40/0.58 796[2:Rew:13.0,718.0] || equal(op(e3,e3),e3)** -> . % 0.40/0.58 802[2:Rew:14.0,726.0] || equal(op(e3,e0),e3)** -> . % 0.40/0.58 803[2:Rew:14.0,727.0] || equal(op(e3,e1),e3)** -> . % 0.40/0.58 810[2:Rew:10.0,672.3] || -> equal(op(e1,e1),e0) equal(op(e1,e0),e0) equal(op(e1,e3),e0)** equal(e1,e0). % 0.40/0.58 811[2:MRR:810.3,1.0] || -> equal(op(e1,e1),e0) equal(op(e1,e0),e0) equal(op(e1,e3),e0)**. % 0.40/0.58 812[2:MRR:811.1,792.0] || -> equal(op(e1,e1),e0) equal(op(e1,e3),e0)**. % 0.40/0.58 817[2:Rew:10.0,675.2] || -> equal(op(e1,e3),e3)** equal(op(e1,e1),e3) equal(e3,e1) equal(op(e1,e0),e3). % 0.40/0.58 818[2:MRR:817.0,817.2,795.0,5.0] || -> equal(op(e1,e1),e3)** equal(op(e1,e0),e3). % 0.40/0.58 830[2:Rew:8.0,704.3] || -> equal(op(e0,e1),e1) equal(op(e0,e0),e1) equal(op(e0,e3),e1)** equal(e1,e0). % 0.40/0.58 831[2:MRR:830.3,1.0] || -> equal(op(e0,e1),e1) equal(op(e0,e0),e1) equal(op(e0,e3),e1)**. % 0.40/0.58 832[2:MRR:831.0,779.0] || -> equal(op(e0,e0),e1) equal(op(e0,e3),e1)**. % 0.40/0.58 840[2:Rew:7.0,715.2] || -> equal(op(e3,e0),e3)** equal(op(e0,e0),e3) equal(e3,e0) equal(op(e1,e0),e3). % 0.40/0.58 841[2:MRR:840.0,840.2,802.0,3.0] || -> equal(op(e0,e0),e3) equal(op(e1,e0),e3)**. % 0.40/0.58 843[2:Rew:13.0,723.2] || -> equal(op(e3,e3),e1)** equal(op(e1,e3),e1) equal(e3,e1) equal(op(e0,e3),e1). % 0.40/0.58 844[2:MRR:843.1,843.2,774.0,5.0] || -> equal(op(e3,e3),e1)** equal(op(e0,e3),e1). % 0.40/0.58 845[2:Rew:13.0,724.2] || -> equal(op(e3,e3),e0)** equal(op(e0,e3),e0) equal(e3,e0) equal(op(e1,e3),e0). % 0.40/0.58 846[2:MRR:845.1,845.2,787.0,3.0] || -> equal(op(e3,e3),e0)** equal(op(e1,e3),e0). % 0.40/0.58 847[2:Rew:14.0,734.2] || -> equal(op(e3,e3),e1)** equal(op(e3,e1),e1) equal(e3,e1) equal(op(e3,e0),e1). % 0.40/0.58 848[2:MRR:847.1,847.2,781.0,5.0] || -> equal(op(e3,e3),e1)** equal(op(e3,e0),e1). % 0.40/0.58 849[2:Rew:14.0,735.2] || -> equal(op(e3,e3),e0)** equal(op(e3,e0),e0) equal(e3,e0) equal(op(e3,e1),e0). % 0.40/0.58 850[2:MRR:849.1,849.2,793.0,3.0] || -> equal(op(e3,e3),e0)** equal(op(e3,e1),e0). % 0.40/0.58 851[2:MRR:739.0,796.0] || -> equal(op(e3,e3),unit) equal(op(e3,e3),e1)** equal(op(e3,e3),e0). % 0.40/0.58 857[2:MRR:743.0,743.1,803.0,781.0] || -> equal(op(e3,e1),unit) equal(op(e3,e1),e0)**. % 0.40/0.58 861[2:MRR:745.0,745.1,802.0,793.0] || -> equal(op(e3,e0),unit) equal(op(e3,e0),e1)**. % 0.40/0.58 873[2:MRR:754.0,773.0] || -> equal(op(e1,e1),e3)** equal(op(e1,e1),unit) equal(op(e1,e1),e0). % 0.40/0.58 874[2:MRR:755.0,755.1,779.0,786.0] || -> equal(op(e0,e1),e3)** equal(op(e0,e1),unit). % 0.40/0.58 875[2:MRR:758.0,785.0] || -> equal(op(e0,e0),e3)** equal(op(e0,e0),unit) equal(op(e0,e0),e1). % 0.40/0.58 883[2:Rew:660.0,736.3,660.0,736.2,663.0,736.0,660.0,736.0] || equal(unit,unit) equal(op(e3,e3),unit)** equal(op(e1,e1),unit) equal(op(e0,e0),unit) -> . % 0.40/0.58 884[2:Obv:883.0] || equal(op(e3,e3),unit)** equal(op(e1,e1),unit) equal(op(e0,e0),unit) -> . % 0.40/0.58 889[3:Spt:812.1] || -> equal(op(e1,e3),e0)**. % 0.40/0.58 893[3:Rew:889.0,37.0] || equal(op(e3,e3),e0)** -> . % 0.40/0.58 895[3:Rew:889.0,49.0] || equal(op(e1,e1),e0)** -> . % 0.40/0.58 898[3:MRR:850.0,893.0] || -> equal(op(e3,e1),e0)**. % 0.40/0.58 899[3:MRR:851.2,893.0] || -> equal(op(e3,e3),unit) equal(op(e3,e3),e1)**. % 0.40/0.58 908[3:MRR:873.2,895.0] || -> equal(op(e1,e1),e3)** equal(op(e1,e1),unit). % 0.40/0.58 915[4:Spt:818.1] || -> equal(op(e1,e0),e3)**. % 0.40/0.58 918[4:Rew:915.0,15.0] || equal(op(e0,e0),e3)** -> . % 0.40/0.58 919[4:Rew:915.0,45.0] || equal(op(e1,e1),e3)** -> . % 0.40/0.58 924[4:MRR:875.0,918.0] || -> equal(op(e0,e0),unit) equal(op(e0,e0),e1)**. % 0.40/0.58 932[4:MRR:908.0,919.0] || -> equal(op(e1,e1),unit)**. % 0.40/0.58 937[4:Rew:932.0,884.1] || equal(op(e3,e3),unit)** equal(unit,unit) equal(op(e0,e0),unit) -> . % 0.40/0.58 942[4:Obv:937.1] || equal(op(e3,e3),unit)** equal(op(e0,e0),unit) -> . % 0.40/0.58 952[5:Spt:832.0] || -> equal(op(e0,e0),e1)**. % 0.40/0.58 954[5:Rew:952.0,41.0] || equal(op(e0,e3),e1)** -> . % 0.40/0.58 955[5:Rew:952.0,17.0] || equal(op(e3,e0),e1)** -> . % 0.40/0.58 964[5:MRR:844.1,954.0] || -> equal(op(e3,e3),e1)**. % 0.40/0.58 971[5:Rew:964.0,761.0] || equal(e1,e1) equal(op(e3,op(e3,e3)),e0) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.58 979[5:MRR:861.1,955.0] || -> equal(op(e3,e0),unit)**. % 0.40/0.58 997[5:Obv:971.0] || equal(op(e3,op(e3,e3)),e0) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.58 998[5:Rew:964.0,997.1,964.0,997.0] || equal(op(e3,e1),e0) equal(op(e3,op(e3,e1)),unit)** -> . % 0.40/0.58 999[5:Rew:898.0,998.1,898.0,998.0] || equal(e0,e0) equal(op(e3,e0),unit)** -> . % 0.40/0.58 1000[5:Obv:999.0] || equal(op(e3,e0),unit)** -> . % 0.40/0.58 1001[5:Rew:979.0,1000.0] || equal(unit,unit)* -> . % 0.40/0.58 1002[5:Obv:1001.0] || -> . % 0.40/0.58 1003[5:Spt:1002.0,832.0,952.0] || equal(op(e0,e0),e1)** -> . % 0.40/0.58 1004[5:Spt:1002.0,832.1] || -> equal(op(e0,e3),e1)**. % 0.40/0.58 1008[5:Rew:1004.0,35.0] || equal(op(e3,e3),e1)** -> . % 0.40/0.58 1014[5:MRR:924.1,1003.0] || -> equal(op(e0,e0),unit)**. % 0.40/0.58 1018[5:MRR:899.1,1008.0] || -> equal(op(e3,e3),unit)**. % 0.40/0.58 1022[5:Rew:1014.0,942.1,1018.0,942.0] || equal(unit,unit)* equal(unit,unit)* -> . % 0.40/0.58 1023[5:Obv:1022.1] || -> . % 0.40/0.58 1040[4:Spt:1023.0,818.1,915.0] || equal(op(e1,e0),e3)** -> . % 0.40/0.58 1041[4:Spt:1023.0,818.0] || -> equal(op(e1,e1),e3)**. % 0.40/0.58 1045[4:Rew:1041.0,21.0] || equal(op(e0,e1),e3)** -> . % 0.40/0.58 1046[4:MRR:841.1,1040.0] || -> equal(op(e0,e0),e3)**. % 0.40/0.58 1052[4:Rew:1046.0,832.0] || -> equal(e3,e1) equal(op(e0,e3),e1)**. % 0.40/0.58 1054[4:MRR:1052.0,5.0] || -> equal(op(e0,e3),e1)**. % 0.40/0.58 1075[4:MRR:874.0,1045.0] || -> equal(op(e0,e1),unit)**. % 0.40/0.58 1094[4:Rew:1075.0,769.2,1054.0,769.2,1046.0,769.2,1054.0,769.1,1046.0,769.1,1046.0,769.0] || equal(e3,e3)* equal(e1,e1) equal(unit,unit) -> . % 0.40/0.58 1095[4:Obv:1094.2] || -> . % 0.40/0.58 1110[3:Spt:1095.0,812.1,889.0] || equal(op(e1,e3),e0)** -> . % 0.40/0.58 1111[3:Spt:1095.0,812.0] || -> equal(op(e1,e1),e0)**. % 0.40/0.58 1116[3:Rew:1111.0,25.0] || equal(op(e3,e1),e0)** -> . % 0.40/0.58 1130[3:MRR:846.1,1110.0] || -> equal(op(e3,e3),e0)**. % 0.40/0.58 1136[3:Rew:1130.0,848.0] || -> equal(e1,e0) equal(op(e3,e0),e1)**. % 0.40/0.58 1138[3:MRR:1136.0,1.0] || -> equal(op(e3,e0),e1)**. % 0.40/0.58 1152[3:MRR:857.1,1116.0] || -> equal(op(e3,e1),unit)**. % 0.40/0.58 1169[3:Rew:1152.0,760.2,1138.0,760.2,1130.0,760.2,1138.0,760.1,1130.0,760.1,1130.0,760.0] || equal(e0,e0) equal(e1,e1)* equal(unit,unit) -> . % 0.40/0.58 1170[3:Obv:1169.2] || -> . % 0.40/0.58 1193[2:Spt:1170.0,659.0,660.0] || equal(e2,unit)** -> . % 0.40/0.58 1194[2:Spt:1170.0,659.1,659.2] || -> equal(e1,unit)** equal(e0,unit). % 0.40/0.58 1195[3:Spt:1194.0] || -> equal(e1,unit)**. % 0.40/0.58 1197[3:Rew:1195.0,10.0] || -> equal(op(unit,unit),unit)**. % 0.40/0.58 1201[3:Rew:1195.0,19.0] || equal(op(e3,e0),op(unit,e0))** -> . % 0.40/0.58 1202[3:Rew:1195.0,15.0] || equal(op(e0,e0),op(unit,e0))** -> . % 0.40/0.58 1207[3:Rew:1195.0,88.3] || -> equal(op(e3,e0),e3)** equal(op(e0,e0),e3) equal(op(e2,e0),e3) equal(op(unit,e0),e3). % 0.40/0.58 1210[3:Rew:1195.0,90.3] || -> equal(op(e2,e0),e2) equal(op(e0,e0),e2) equal(op(e3,e0),e2)** equal(op(unit,e0),e2). % 0.40/0.58 1226[3:Rew:1195.0,43.0] || equal(op(e0,e3),op(e0,unit))** -> . % 0.40/0.58 1228[3:Rew:1195.0,42.0] || equal(op(e0,e2),op(e0,unit))** -> . % 0.40/0.58 1232[3:Rew:1195.0,91.3] || -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e3),e2)** equal(op(e0,unit),e2). % 0.40/0.58 1235[3:Rew:1195.0,37.0] || equal(op(e3,e3),op(unit,e3))** -> . % 0.40/0.58 1237[3:Rew:1195.0,36.0] || equal(op(e2,e3),op(unit,e3))** -> . % 0.40/0.58 1239[3:Rew:1195.0,70.3] || -> equal(op(e3,e3),e0)** equal(op(e0,e3),e0) equal(op(e2,e3),e0) equal(op(unit,e3),e0). % 0.40/0.58 1245[3:Rew:1195.0,57.0] || equal(op(e3,e0),op(e3,unit))** -> . % 0.40/0.58 1250[3:Rew:1195.0,67.2] || -> equal(op(e3,e3),e2)** equal(op(e3,e2),e2) equal(op(e3,unit),e2) equal(op(e3,e0),e2). % 0.40/0.58 1251[3:Rew:1195.0,31.0] || equal(op(e3,e2),op(unit,e2))** -> . % 0.40/0.58 1252[3:Rew:1195.0,27.0] || equal(op(e0,e2),op(unit,e2))** -> . % 0.40/0.58 1253[3:Rew:1195.0,30.0] || equal(op(e2,e2),op(unit,e2))** -> . % 0.40/0.58 1260[3:Rew:1195.0,78.3] || -> equal(op(e2,e2),e0) equal(op(e0,e2),e0) equal(op(e3,e2),e0)** equal(op(unit,e2),e0). % 0.40/0.58 1261[3:Rew:1195.0,55.0] || equal(op(e2,e3),op(e2,unit))** -> . % 0.40/0.58 1262[3:Rew:1195.0,51.0] || equal(op(e2,e0),op(e2,unit))** -> . % 0.40/0.58 1273[3:Rew:1195.0,138.0] || equal(op(unit,unit),unit) equal(op(e3,e3),e1)** equal(op(e2,e2),e1) equal(op(e0,e0),e1) -> . % 0.40/0.58 1280[3:Rew:1195.0,101.2] || -> equal(op(e2,e2),e2) equal(op(e2,e2),e3)** equal(op(e2,e2),unit) equal(op(e2,e2),e0). % 0.40/0.58 1284[3:Rew:1195.0,109.3] || -> equal(op(e0,e2),e2) equal(op(e0,e2),e0) equal(op(e0,e2),e3)** equal(op(e0,e2),unit). % 0.40/0.58 1285[3:Rew:1195.0,100.2] || -> equal(op(e2,e3),e3)** equal(op(e2,e3),e2) equal(op(e2,e3),unit) equal(op(e2,e3),e0). % 0.40/0.58 1289[3:Rew:1195.0,111.3] || -> equal(op(e0,e0),e0) equal(op(e0,e0),e3)** equal(op(e0,e0),e2) equal(op(e0,e0),unit). % 0.40/0.58 1291[3:Rew:1195.0,99.3] || -> equal(op(e3,e0),e3)** equal(op(e3,e0),e0) equal(op(e3,e0),e2) equal(op(e3,e0),unit). % 0.40/0.58 1294[3:Rew:1195.0,96.2] || -> equal(op(e3,e3),e3)** equal(op(e3,e3),e2) equal(op(e3,e3),unit) equal(op(e3,e3),e0). % 0.40/0.58 1296[3:Rew:1195.0,126.2] || equal(op(e2,e2),e0) equal(op(e2,op(e2,e2)),e3) equal(op(e2,op(e2,op(e2,e2))),unit)** -> . % 0.40/0.58 1302[3:Rew:1195.0,125.2] || equal(op(e3,e3),e2) equal(op(e3,op(e3,e3)),e0) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.58 1303[3:Rew:1195.0,129.2] || equal(op(e0,e0),e3) equal(op(e0,op(e0,e0)),e2) equal(op(e0,op(e0,op(e0,e0))),unit)** -> . % 0.40/0.58 1307[3:Rew:7.0,1201.0] || equal(op(e3,e0),e0)** -> . % 0.40/0.58 1308[3:Rew:7.0,1202.0] || equal(op(e0,e0),e0)** -> . % 0.40/0.58 1314[3:Rew:8.0,1226.0] || equal(op(e0,e3),e0)** -> . % 0.40/0.58 1316[3:Rew:8.0,1228.0] || equal(op(e0,e2),e0)** -> . % 0.40/0.58 1320[3:Rew:13.0,1235.0] || equal(op(e3,e3),e3)** -> . % 0.40/0.58 1322[3:Rew:13.0,1237.0] || equal(op(e2,e3),e3)** -> . % 0.40/0.58 1327[3:Rew:14.0,1245.0] || equal(op(e3,e0),e3)** -> . % 0.40/0.58 1329[3:Rew:11.0,1251.0] || equal(op(e3,e2),e2)** -> . % 0.40/0.58 1330[3:Rew:11.0,1252.0] || equal(op(e0,e2),e2)** -> . % 0.40/0.58 1331[3:Rew:11.0,1253.0] || equal(op(e2,e2),e2)** -> . % 0.40/0.58 1337[3:Rew:12.0,1261.0] || equal(op(e2,e3),e2)** -> . % 0.40/0.58 1338[3:Rew:12.0,1262.0] || equal(op(e2,e0),e2)** -> . % 0.40/0.58 1345[3:Rew:7.0,1207.3] || -> equal(op(e3,e0),e3)** equal(op(e0,e0),e3) equal(op(e2,e0),e3) equal(e3,e0). % 0.40/0.58 1346[3:MRR:1345.3,3.0] || -> equal(op(e3,e0),e3)** equal(op(e0,e0),e3) equal(op(e2,e0),e3). % 0.40/0.58 1347[3:MRR:1346.0,1327.0] || -> equal(op(e0,e0),e3) equal(op(e2,e0),e3)**. % 0.40/0.58 1352[3:Rew:7.0,1210.3] || -> equal(op(e2,e0),e2) equal(op(e0,e0),e2) equal(op(e3,e0),e2)** equal(e2,e0). % 0.40/0.58 1353[3:MRR:1352.0,1352.3,1338.0,2.0] || -> equal(op(e0,e0),e2) equal(op(e3,e0),e2)**. % 0.40/0.58 1361[3:Rew:8.0,1232.3] || -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e3),e2)** equal(e2,e0). % 0.40/0.58 1362[3:MRR:1361.0,1361.3,1330.0,2.0] || -> equal(op(e0,e0),e2) equal(op(e0,e3),e2)**. % 0.40/0.58 1365[3:Rew:13.0,1239.3] || -> equal(op(e3,e3),e0)** equal(op(e0,e3),e0) equal(op(e2,e3),e0) equal(e3,e0). % 0.40/0.58 1366[3:MRR:1365.3,3.0] || -> equal(op(e3,e3),e0)** equal(op(e0,e3),e0) equal(op(e2,e3),e0). % 0.40/0.58 1367[3:MRR:1366.1,1314.0] || -> equal(op(e3,e3),e0)** equal(op(e2,e3),e0). % 0.40/0.58 1375[3:Rew:14.0,1250.2] || -> equal(op(e3,e3),e2)** equal(op(e3,e2),e2) equal(e3,e2) equal(op(e3,e0),e2). % 0.40/0.58 1376[3:MRR:1375.1,1375.2,1329.0,6.0] || -> equal(op(e3,e3),e2)** equal(op(e3,e0),e2). % 0.40/0.58 1379[3:Rew:11.0,1260.3] || -> equal(op(e2,e2),e0) equal(op(e0,e2),e0) equal(op(e3,e2),e0)** equal(e2,e0). % 0.40/0.58 1380[3:MRR:1379.1,1379.3,1316.0,2.0] || -> equal(op(e2,e2),e0) equal(op(e3,e2),e0)**. % 0.40/0.58 1397[3:MRR:1280.0,1331.0] || -> equal(op(e2,e2),e3)** equal(op(e2,e2),unit) equal(op(e2,e2),e0). % 0.40/0.58 1405[3:MRR:1284.0,1284.1,1330.0,1316.0] || -> equal(op(e0,e2),e3)** equal(op(e0,e2),unit). % 0.40/0.58 1406[3:MRR:1285.0,1285.1,1322.0,1337.0] || -> equal(op(e2,e3),unit) equal(op(e2,e3),e0)**. % 0.40/0.58 1408[3:MRR:1289.0,1308.0] || -> equal(op(e0,e0),e3)** equal(op(e0,e0),e2) equal(op(e0,e0),unit). % 0.40/0.58 1410[3:MRR:1291.0,1291.1,1327.0,1307.0] || -> equal(op(e3,e0),e2)** equal(op(e3,e0),unit). % 0.40/0.58 1411[3:MRR:1294.0,1320.0] || -> equal(op(e3,e3),e2)** equal(op(e3,e3),unit) equal(op(e3,e3),e0). % 0.40/0.58 1418[3:Rew:1195.0,1273.3,1195.0,1273.2,1195.0,1273.1,1197.0,1273.0] || equal(unit,unit) equal(op(e3,e3),unit)** equal(op(e2,e2),unit) equal(op(e0,e0),unit) -> . % 0.40/0.58 1419[3:Obv:1418.0] || equal(op(e3,e3),unit)** equal(op(e2,e2),unit) equal(op(e0,e0),unit) -> . % 0.40/0.58 1424[4:Spt:1347.1] || -> equal(op(e2,e0),e3)**. % 0.40/0.58 1429[4:Rew:1424.0,16.0] || equal(op(e0,e0),e3)** -> . % 0.40/0.58 1430[4:Rew:1424.0,52.0] || equal(op(e2,e2),e3)** -> . % 0.40/0.58 1434[4:MRR:1408.0,1429.0] || -> equal(op(e0,e0),e2)** equal(op(e0,e0),unit). % 0.40/0.58 1443[4:MRR:1397.0,1430.0] || -> equal(op(e2,e2),unit) equal(op(e2,e2),e0)**. % 0.40/0.58 1450[5:Spt:1353.1] || -> equal(op(e3,e0),e2)**. % 0.40/0.58 1453[5:Rew:1450.0,59.0] || equal(op(e3,e3),e2)** -> . % 0.40/0.58 1454[5:Rew:1450.0,17.0] || equal(op(e0,e0),e2)** -> . % 0.40/0.58 1459[5:MRR:1411.0,1453.0] || -> equal(op(e3,e3),unit) equal(op(e3,e3),e0)**. % 0.40/0.58 1467[5:MRR:1434.0,1454.0] || -> equal(op(e0,e0),unit)**. % 0.40/0.58 1472[5:Rew:1467.0,1419.2] || equal(op(e3,e3),unit)** equal(op(e2,e2),unit) equal(unit,unit) -> . % 0.40/0.58 1477[5:Obv:1472.2] || equal(op(e3,e3),unit)** equal(op(e2,e2),unit) -> . % 0.40/0.58 1487[6:Spt:1367.0] || -> equal(op(e3,e3),e0)**. % 0.40/0.58 1489[6:Rew:1487.0,62.0] || equal(op(e3,e2),e0)** -> . % 0.40/0.58 1490[6:Rew:1487.0,38.0] || equal(op(e2,e3),e0)** -> . % 0.40/0.58 1499[6:MRR:1380.1,1489.0] || -> equal(op(e2,e2),e0)**. % 0.40/0.58 1506[6:Rew:1499.0,1296.0] || equal(e0,e0) equal(op(e2,op(e2,e2)),e3) equal(op(e2,op(e2,op(e2,e2))),unit)** -> . % 0.40/0.58 1514[6:MRR:1406.1,1490.0] || -> equal(op(e2,e3),unit)**. % 0.40/0.58 1532[6:Obv:1506.0] || equal(op(e2,op(e2,e2)),e3) equal(op(e2,op(e2,op(e2,e2))),unit)** -> . % 0.40/0.58 1533[6:Rew:1499.0,1532.1,1499.0,1532.0] || equal(op(e2,e0),e3) equal(op(e2,op(e2,e0)),unit)** -> . % 0.40/0.58 1534[6:Rew:1424.0,1533.1,1424.0,1533.0] || equal(e3,e3) equal(op(e2,e3),unit)** -> . % 0.40/0.58 1535[6:Obv:1534.0] || equal(op(e2,e3),unit)** -> . % 0.40/0.58 1536[6:Rew:1514.0,1535.0] || equal(unit,unit)* -> . % 0.40/0.58 1537[6:Obv:1536.0] || -> . % 0.40/0.58 1538[6:Spt:1537.0,1367.0,1487.0] || equal(op(e3,e3),e0)** -> . % 0.40/0.58 1539[6:Spt:1537.0,1367.1] || -> equal(op(e2,e3),e0)**. % 0.40/0.58 1543[6:Rew:1539.0,56.0] || equal(op(e2,e2),e0)** -> . % 0.40/0.58 1549[6:MRR:1459.1,1538.0] || -> equal(op(e3,e3),unit)**. % 0.40/0.58 1553[6:MRR:1443.1,1543.0] || -> equal(op(e2,e2),unit)**. % 0.40/0.58 1557[6:Rew:1553.0,1477.1,1549.0,1477.0] || equal(unit,unit)* equal(unit,unit)* -> . % 0.40/0.58 1558[6:Obv:1557.1] || -> . % 0.40/0.58 1575[5:Spt:1558.0,1353.1,1450.0] || equal(op(e3,e0),e2)** -> . % 0.40/0.58 1576[5:Spt:1558.0,1353.0] || -> equal(op(e0,e0),e2)**. % 0.40/0.58 1581[5:MRR:1376.1,1575.0] || -> equal(op(e3,e3),e2)**. % 0.40/0.58 1587[5:Rew:1581.0,1367.0] || -> equal(e2,e0) equal(op(e2,e3),e0)**. % 0.40/0.58 1589[5:MRR:1587.0,2.0] || -> equal(op(e2,e3),e0)**. % 0.40/0.58 1592[5:Rew:1589.0,56.0] || equal(op(e2,e2),e0)** -> . % 0.40/0.58 1595[5:MRR:1380.0,1592.0] || -> equal(op(e3,e2),e0)**. % 0.40/0.58 1606[5:MRR:1410.0,1575.0] || -> equal(op(e3,e0),unit)**. % 0.40/0.58 1627[5:Rew:1606.0,1302.2,1595.0,1302.2,1581.0,1302.2,1595.0,1302.1,1581.0,1302.1,1581.0,1302.0] || equal(e2,e2)* equal(e0,e0) equal(unit,unit) -> . % 0.40/0.58 1628[5:Obv:1627.2] || -> . % 0.40/0.58 1645[4:Spt:1628.0,1347.1,1424.0] || equal(op(e2,e0),e3)** -> . % 0.40/0.58 1646[4:Spt:1628.0,1347.0] || -> equal(op(e0,e0),e3)**. % 0.40/0.58 1651[4:Rew:1646.0,40.0] || equal(op(e0,e2),e3)** -> . % 0.40/0.58 1652[4:Rew:1646.0,1362.0] || -> equal(e3,e2) equal(op(e0,e3),e2)**. % 0.40/0.58 1653[4:MRR:1652.0,6.0] || -> equal(op(e0,e3),e2)**. % 0.40/0.58 1687[4:MRR:1405.0,1651.0] || -> equal(op(e0,e2),unit)**. % 0.40/0.58 1704[4:Rew:1687.0,1303.2,1653.0,1303.2,1646.0,1303.2,1653.0,1303.1,1646.0,1303.1,1646.0,1303.0] || equal(e3,e3)* equal(e2,e2) equal(unit,unit) -> . % 0.40/0.58 1705[4:Obv:1704.2] || -> . % 0.40/0.58 1728[3:Spt:1705.0,1194.0,1195.0] || equal(e1,unit)** -> . % 0.40/0.58 1729[3:Spt:1705.0,1194.1] || -> equal(e0,unit)**. % 0.40/0.58 1730[3:Rew:1729.0,8.0] || -> equal(op(unit,unit),unit)**. % 0.40/0.58 1747[3:Rew:1729.0,35.0] || equal(op(e3,e3),op(unit,e3))** -> . % 0.40/0.58 1748[3:Rew:13.0,1747.0] || equal(op(e3,e3),e3)** -> . % 0.40/0.58 1751[3:Rew:1729.0,58.0] || equal(op(e3,e2),op(e3,unit))** -> . % 0.40/0.58 1752[3:Rew:14.0,1751.0] || equal(op(e3,e2),e3)** -> . % 0.40/0.58 1755[3:Rew:1729.0,28.0] || equal(op(e2,e2),op(unit,e2))** -> . % 0.40/0.58 1756[3:Rew:11.0,1755.0] || equal(op(e2,e2),e2)** -> . % 0.40/0.58 1759[3:Rew:1729.0,29.0] || equal(op(e3,e2),op(unit,e2))** -> . % 0.40/0.58 1760[3:Rew:11.0,1759.0] || equal(op(e3,e2),e2)** -> . % 0.40/0.58 1761[3:Rew:1729.0,53.0] || equal(op(e2,e3),op(e2,unit))** -> . % 0.40/0.58 1762[3:Rew:12.0,1761.0] || equal(op(e2,e3),e2)** -> . % 0.40/0.58 1764[3:Rew:1729.0,51.0] || equal(op(e2,e1),op(e2,unit))** -> . % 0.40/0.58 1765[3:Rew:12.0,1764.0] || equal(op(e2,e1),e2)** -> . % 0.40/0.58 1766[3:Rew:10.0,46.0,1729.0,46.0] || equal(op(e1,e2),e1)** -> . % 0.40/0.58 1767[3:Rew:1729.0,27.0] || equal(op(e1,e2),op(unit,e2))** -> . % 0.40/0.58 1768[3:Rew:11.0,1767.0] || equal(op(e1,e2),e2)** -> . % 0.40/0.58 1769[3:Rew:1729.0,57.0] || equal(op(e3,e1),op(e3,unit))** -> . % 0.40/0.58 1770[3:Rew:14.0,1769.0] || equal(op(e3,e1),e3)** -> . % 0.40/0.58 1771[3:Rew:9.0,23.0,1729.0,23.0] || equal(op(e3,e1),e1)** -> . % 0.40/0.58 1772[3:Rew:1729.0,33.0] || equal(op(e1,e3),op(unit,e3))** -> . % 0.40/0.58 1773[3:Rew:13.0,1772.0] || equal(op(e1,e3),e3)** -> . % 0.40/0.58 1774[3:Rew:10.0,47.0,1729.0,47.0] || equal(op(e1,e3),e1)** -> . % 0.40/0.58 1780[3:Rew:9.0,21.0,1729.0,21.0] || equal(op(e1,e1),e1)** -> . % 0.40/0.58 1792[3:Rew:10.0,81.3,1729.0,81.3] || -> equal(op(e1,e3),e3)** equal(op(e1,e1),e3) equal(op(e1,e2),e3) equal(e3,e1). % 0.40/0.58 1793[3:MRR:1792.0,1792.3,1773.0,5.0] || -> equal(op(e1,e1),e3) equal(op(e1,e2),e3)**. % 0.40/0.58 1794[3:Rew:10.0,83.3,1729.0,83.3] || -> equal(op(e1,e2),e2) equal(op(e1,e1),e2) equal(op(e1,e3),e2)** equal(e2,e1). % 0.40/0.58 1795[3:MRR:1794.0,1794.3,1768.0,4.0] || -> equal(op(e1,e1),e2) equal(op(e1,e3),e2)**. % 0.40/0.58 1797[3:Rew:1729.0,106.3] || -> equal(op(e1,e1),e1) equal(op(e1,e1),e3)** equal(op(e1,e1),e2) equal(op(e1,e1),unit). % 0.40/0.58 1798[3:MRR:1797.0,1780.0] || -> equal(op(e1,e1),e3)** equal(op(e1,e1),e2) equal(op(e1,e1),unit). % 0.40/0.58 1801[3:Rew:9.0,80.3,1729.0,80.3] || -> equal(op(e3,e1),e3)** equal(op(e1,e1),e3) equal(op(e2,e1),e3) equal(e3,e1). % 0.40/0.58 1802[3:MRR:1801.0,1801.3,1770.0,5.0] || -> equal(op(e1,e1),e3) equal(op(e2,e1),e3)**. % 0.40/0.58 1803[3:Rew:9.0,82.3,1729.0,82.3] || -> equal(op(e2,e1),e2) equal(op(e1,e1),e2) equal(op(e3,e1),e2)** equal(e2,e1). % 0.40/0.58 1804[3:MRR:1803.0,1803.3,1765.0,4.0] || -> equal(op(e1,e1),e2) equal(op(e3,e1),e2)**. % 0.40/0.58 1809[3:Rew:1729.0,104.3] || -> equal(op(e1,e3),e3)** equal(op(e1,e3),e1) equal(op(e1,e3),e2) equal(op(e1,e3),unit). % 0.40/0.58 1810[3:MRR:1809.0,1809.1,1773.0,1774.0] || -> equal(op(e1,e3),e2)** equal(op(e1,e3),unit). % 0.40/0.58 1815[3:Rew:1729.0,66.3] || -> equal(op(e3,e3),e2)** equal(op(e2,e3),e2) equal(op(e1,e3),e2) equal(op(unit,e3),e2). % 0.40/0.58 1816[3:Rew:13.0,1815.3] || -> equal(op(e3,e3),e2)** equal(op(e2,e3),e2) equal(op(e1,e3),e2) equal(e3,e2). % 0.40/0.58 1817[3:MRR:1816.3,6.0] || -> equal(op(e3,e3),e2)** equal(op(e2,e3),e2) equal(op(e1,e3),e2). % 0.40/0.58 1818[3:MRR:1817.1,1762.0] || -> equal(op(e3,e3),e2)** equal(op(e1,e3),e2). % 0.40/0.58 1819[3:Rew:1729.0,98.3] || -> equal(op(e3,e1),e3)** equal(op(e3,e1),e1) equal(op(e3,e1),e2) equal(op(e3,e1),unit). % 0.40/0.58 1820[3:MRR:1819.0,1819.1,1770.0,1771.0] || -> equal(op(e3,e1),e2)** equal(op(e3,e1),unit). % 0.40/0.58 1825[3:Rew:1729.0,67.3] || -> equal(op(e3,e3),e2)** equal(op(e3,e2),e2) equal(op(e3,e1),e2) equal(op(e3,unit),e2). % 0.40/0.58 1826[3:Rew:14.0,1825.3] || -> equal(op(e3,e3),e2)** equal(op(e3,e2),e2) equal(op(e3,e1),e2) equal(e3,e2). % 0.40/0.58 1827[3:MRR:1826.3,6.0] || -> equal(op(e3,e3),e2)** equal(op(e3,e2),e2) equal(op(e3,e1),e2). % 0.40/0.58 1828[3:MRR:1827.1,1760.0] || -> equal(op(e3,e3),e2)** equal(op(e3,e1),e2). % 0.40/0.58 1830[3:Rew:1729.0,105.3] || -> equal(op(e1,e2),e2) equal(op(e1,e2),e1) equal(op(e1,e2),e3)** equal(op(e1,e2),unit). % 0.40/0.58 1831[3:MRR:1830.0,1830.1,1768.0,1766.0] || -> equal(op(e1,e2),e3)** equal(op(e1,e2),unit). % 0.40/0.58 1841[3:Rew:1729.0,79.3,1729.0,79.2,1729.0,79.1,1729.0,79.0] || -> equal(op(e2,e2),unit) equal(op(e2,unit),unit) equal(op(e2,e3),unit)** equal(op(e2,e1),unit). % 0.40/0.58 1842[3:Rew:12.0,1841.1] || -> equal(op(e2,e2),unit) equal(e2,unit) equal(op(e2,e3),unit)** equal(op(e2,e1),unit). % 0.40/0.58 1843[3:MRR:1842.1,1193.0] || -> equal(op(e2,e2),unit) equal(op(e2,e3),unit)** equal(op(e2,e1),unit). % 0.40/0.58 1849[3:Rew:1729.0,76.3] || -> equal(op(e2,e2),e1) equal(op(e1,e2),e1) equal(op(e3,e2),e1)** equal(op(unit,e2),e1). % 0.40/0.58 1850[3:Rew:11.0,1849.3] || -> equal(op(e2,e2),e1) equal(op(e1,e2),e1) equal(op(e3,e2),e1)** equal(e2,e1). % 0.40/0.58 1851[3:MRR:1850.1,1850.3,1766.0,4.0] || -> equal(op(e2,e2),e1) equal(op(e3,e2),e1)**. % 0.40/0.58 1861[3:Rew:1729.0,101.3] || -> equal(op(e2,e2),e2) equal(op(e2,e2),e3)** equal(op(e2,e2),e1) equal(op(e2,e2),unit). % 0.40/0.58 1862[3:MRR:1861.0,1756.0] || -> equal(op(e2,e2),e3)** equal(op(e2,e2),e1) equal(op(e2,e2),unit). % 0.40/0.58 1863[3:Rew:1729.0,69.3] || -> equal(op(e3,e3),e1)** equal(op(e3,e1),e1) equal(op(e3,e2),e1) equal(op(e3,unit),e1). % 0.40/0.58 1864[3:Rew:14.0,1863.3] || -> equal(op(e3,e3),e1)** equal(op(e3,e1),e1) equal(op(e3,e2),e1) equal(e3,e1). % 0.40/0.58 1865[3:MRR:1864.1,1864.3,1771.0,5.0] || -> equal(op(e3,e3),e1)** equal(op(e3,e2),e1). % 0.40/0.58 1866[3:Rew:1729.0,97.3] || -> equal(op(e3,e2),e3)** equal(op(e3,e2),e2) equal(op(e3,e2),e1) equal(op(e3,e2),unit). % 0.40/0.58 1867[3:MRR:1866.0,1866.1,1752.0,1760.0] || -> equal(op(e3,e2),e1)** equal(op(e3,e2),unit). % 0.40/0.58 1876[3:Rew:1729.0,96.3] || -> equal(op(e3,e3),e3)** equal(op(e3,e3),e2) equal(op(e3,e3),e1) equal(op(e3,e3),unit). % 0.40/0.58 1877[3:MRR:1876.0,1748.0] || -> equal(op(e3,e3),e2)** equal(op(e3,e3),e1) equal(op(e3,e3),unit). % 0.40/0.58 1880[3:Rew:1729.0,139.3,1729.0,139.2,1729.0,139.1,1730.0,139.0,1729.0,139.0] || equal(unit,unit) equal(op(e3,e3),unit)** equal(op(e2,e2),unit) equal(op(e1,e1),unit) -> . % 0.40/0.58 1881[3:Obv:1880.0] || equal(op(e3,e3),unit)** equal(op(e2,e2),unit) equal(op(e1,e1),unit) -> . % 0.40/0.58 1882[3:Rew:1729.0,135.2] || equal(op(e1,e1),e3) equal(op(e1,op(e1,e1)),e2) equal(op(e1,op(e1,op(e1,e1))),unit)** -> . % 0.40/0.58 1890[3:Rew:1729.0,130.2] || equal(op(e3,e3),e1) equal(op(e3,op(e3,e3)),e2) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.58 1897[3:Rew:1729.0,131.2] || equal(op(e3,e3),e2) equal(op(e3,op(e3,e3)),e1) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.58 1908[4:Spt:1793.1] || -> equal(op(e1,e2),e3)**. % 0.40/0.58 1911[4:Rew:1908.0,48.0] || equal(op(e1,e1),e3)** -> . % 0.40/0.58 1913[4:Rew:1908.0,30.0] || equal(op(e2,e2),e3)** -> . % 0.40/0.58 1917[4:MRR:1798.0,1911.0] || -> equal(op(e1,e1),e2)** equal(op(e1,e1),unit). % 0.40/0.58 1918[4:MRR:1802.0,1911.0] || -> equal(op(e2,e1),e3)**. % 0.40/0.58 1925[4:Rew:1918.0,1843.2] || -> equal(op(e2,e2),unit) equal(op(e2,e3),unit)** equal(e3,unit). % 0.40/0.58 1927[4:MRR:1862.0,1913.0] || -> equal(op(e2,e2),e1)** equal(op(e2,e2),unit). % 0.40/0.58 1930[4:MRR:1925.2,658.0] || -> equal(op(e2,e2),unit) equal(op(e2,e3),unit)**. % 0.40/0.59 1934[5:Spt:1795.1] || -> equal(op(e1,e3),e2)**. % 0.40/0.59 1938[5:Rew:1934.0,37.0] || equal(op(e3,e3),e2)** -> . % 0.40/0.59 1939[5:Rew:1934.0,49.0] || equal(op(e1,e1),e2)** -> . % 0.40/0.59 1942[5:MRR:1828.0,1938.0] || -> equal(op(e3,e1),e2)**. % 0.40/0.59 1943[5:MRR:1877.0,1938.0] || -> equal(op(e3,e3),e1)** equal(op(e3,e3),unit). % 0.40/0.59 1951[5:MRR:1917.0,1939.0] || -> equal(op(e1,e1),unit)**. % 0.40/0.59 1954[5:Rew:1951.0,1881.2] || equal(op(e3,e3),unit)** equal(op(e2,e2),unit) equal(unit,unit) -> . % 0.40/0.59 1961[5:Obv:1954.2] || equal(op(e3,e3),unit)** equal(op(e2,e2),unit) -> . % 0.40/0.59 1971[6:Spt:1851.0] || -> equal(op(e2,e2),e1)**. % 0.40/0.59 1973[6:Rew:1971.0,32.0] || equal(op(e3,e2),e1)** -> . % 0.40/0.59 1983[6:MRR:1865.1,1973.0] || -> equal(op(e3,e3),e1)**. % 0.40/0.59 1984[6:MRR:1867.0,1973.0] || -> equal(op(e3,e2),unit)**. % 0.40/0.59 1994[6:Rew:1983.0,1890.0] || equal(e1,e1) equal(op(e3,op(e3,e3)),e2) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.59 2016[6:Obv:1994.0] || equal(op(e3,op(e3,e3)),e2) equal(op(e3,op(e3,op(e3,e3))),unit)** -> . % 0.40/0.59 2017[6:Rew:1983.0,2016.1,1983.0,2016.0] || equal(op(e3,e1),e2) equal(op(e3,op(e3,e1)),unit)** -> . % 0.40/0.59 2018[6:Rew:1942.0,2017.1,1942.0,2017.0] || equal(e2,e2) equal(op(e3,e2),unit)** -> . % 0.40/0.59 2019[6:Obv:2018.0] || equal(op(e3,e2),unit)** -> . % 0.40/0.59 2020[6:Rew:1984.0,2019.0] || equal(unit,unit)* -> . % 0.40/0.59 2021[6:Obv:2020.0] || -> . % 0.40/0.59 2022[6:Spt:2021.0,1851.0,1971.0] || equal(op(e2,e2),e1)** -> . % 0.40/0.59 2023[6:Spt:2021.0,1851.1] || -> equal(op(e3,e2),e1)**. % 0.40/0.59 2027[6:Rew:2023.0,62.0] || equal(op(e3,e3),e1)** -> . % 0.40/0.59 2033[6:MRR:1927.0,2022.0] || -> equal(op(e2,e2),unit)**. % 0.40/0.59 2037[6:MRR:1943.0,2027.0] || -> equal(op(e3,e3),unit)**. % 0.40/0.59 2041[6:Rew:2033.0,1961.1,2037.0,1961.0] || equal(unit,unit)* equal(unit,unit)* -> . % 0.40/0.59 2042[6:Obv:2041.1] || -> . % 0.40/0.59 2059[5:Spt:2042.0,1795.1,1934.0] || equal(op(e1,e3),e2)** -> . % 0.40/0.59 2060[5:Spt:2042.0,1795.0] || -> equal(op(e1,e1),e2)**. % 0.40/0.59 2064[5:Rew:2060.0,25.0] || equal(op(e3,e1),e2)** -> . % 0.40/0.59 2065[5:MRR:1810.0,2059.0] || -> equal(op(e1,e3),unit)**. % 0.40/0.59 2070[5:Rew:2065.0,36.0] || equal(op(e2,e3),unit)** -> . % 0.40/0.59 2071[5:MRR:1930.1,2070.0] || -> equal(op(e2,e2),unit)**. % 0.40/0.59 2075[5:Rew:2071.0,32.0] || equal(op(e3,e2),unit)** -> . % 0.40/0.59 2083[5:MRR:1867.1,2075.0] || -> equal(op(e3,e2),e1)**. % 0.40/0.59 2090[5:Rew:2065.0,1818.1] || -> equal(op(e3,e3),e2)** equal(e2,unit). % 0.40/0.59 2091[5:MRR:2090.1,1193.0] || -> equal(op(e3,e3),e2)**. % 0.40/0.59 2096[5:MRR:1820.0,2064.0] || -> equal(op(e3,e1),unit)**. % 0.40/0.59 2115[5:Rew:2096.0,1897.2,2083.0,1897.2,2091.0,1897.2,2083.0,1897.1,2091.0,1897.1,2091.0,1897.0] || equal(e2,e2)* equal(e1,e1) equal(unit,unit) -> . % 0.40/0.59 2116[5:Obv:2115.2] || -> . % 0.40/0.59 2131[4:Spt:2116.0,1793.1,1908.0] || equal(op(e1,e2),e3)** -> . % 0.40/0.59 2132[4:Spt:2116.0,1793.0] || -> equal(op(e1,e1),e3)**. % 0.40/0.59 2138[4:Rew:2132.0,1804.0] || -> equal(e3,e2) equal(op(e3,e1),e2)**. % 0.40/0.59 2139[4:MRR:2138.0,6.0] || -> equal(op(e3,e1),e2)**. % 0.40/0.59 2143[4:Rew:2139.0,61.0] || equal(op(e3,e3),e2)** -> . % 0.40/0.59 2145[4:MRR:1818.0,2143.0] || -> equal(op(e1,e3),e2)**. % 0.40/0.59 2151[4:MRR:1831.0,2131.0] || -> equal(op(e1,e2),unit)**. % 0.40/0.59 2192[4:Rew:2151.0,1882.2,2145.0,1882.2,2132.0,1882.2,2145.0,1882.1,2132.0,1882.1,2132.0,1882.0] || equal(e3,e3)* equal(e2,e2) equal(unit,unit) -> . % 0.40/0.59 2193[4:Obv:2192.2] || -> . % 0.40/0.59 % SZS output end Refutation % 0.40/0.59 Formulae used in the proof : ax5 ax2 ax4 ax3 ax1 ax28 ax26 ax25 ax24 ax23 ax19 ax17 ax16 ax13 ax12 ax11 ax7 ax6 % 0.40/0.59 %------------------------------------------------------------------------------