SPASS---3.9.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : SPASS---3.9
% Problem  : ALG192+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm  : none
% Format   : tptp
% Command  : run_spass %d %s

% Computer : n025.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:53 EDT 2022

% Result   : Unsatisfiable 1.31s 1.48s
% Output   : Refutation 1.36s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11  % Problem  : ALG192+1 : TPTP v8.1.0. Released v2.7.0.
% 0.11/0.12  % Command  : run_spass %d %s
% 0.12/0.33  % Computer : n025.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 600
% 0.12/0.33  % DateTime : Wed Jun  8 20:44:20 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 1.31/1.48  
% 1.31/1.48  SPASS V 3.9 
% 1.31/1.48  SPASS beiseite: Proof found.
% 1.31/1.48  % SZS status Theorem
% 1.31/1.48  Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p 
% 1.31/1.48  SPASS derived 7994 clauses, backtracked 9211 clauses, performed 48 splits and kept 12061 clauses.
% 1.31/1.48  SPASS allocated 90560 KBytes.
% 1.31/1.48  SPASS spent	0:00:01.13 on the problem.
% 1.31/1.48  		0:00:00.04 for the input.
% 1.31/1.48  		0:00:00.06 for the FLOTTER CNF translation.
% 1.31/1.48  		0:00:00.00 for inferences.
% 1.31/1.48  		0:00:00.02 for the backtracking.
% 1.31/1.48  		0:00:00.97 for the reduction.
% 1.31/1.48  
% 1.31/1.48  
% 1.31/1.48  Here is a proof with depth 4, length 1605 :
% 1.31/1.48  % SZS output start Refutation
% 1.31/1.48  1[0:Inp] || equal(e1,e0)** -> .
% 1.31/1.48  2[0:Inp] || equal(e2,e0)** -> .
% 1.31/1.48  3[0:Inp] || equal(e3,e0)** -> .
% 1.31/1.48  4[0:Inp] || equal(e4,e0)** -> .
% 1.31/1.48  5[0:Inp] || equal(e2,e1)** -> .
% 1.31/1.48  6[0:Inp] || equal(e3,e1)** -> .
% 1.31/1.48  7[0:Inp] || equal(e4,e1)** -> .
% 1.31/1.48  8[0:Inp] || equal(e3,e2)** -> .
% 1.31/1.48  9[0:Inp] || equal(e4,e2)** -> .
% 1.31/1.48  10[0:Inp] || equal(e4,e3)** -> .
% 1.31/1.48  11[0:Inp] ||  -> equal(op(e0,op(e0,e0)),e0)**.
% 1.31/1.48  12[0:Inp] ||  -> equal(op(e0,op(e0,e1)),e1)**.
% 1.31/1.48  13[0:Inp] ||  -> equal(op(e0,op(e0,e2)),e2)**.
% 1.31/1.48  14[0:Inp] ||  -> equal(op(e0,op(e0,e3)),e3)**.
% 1.31/1.48  15[0:Inp] ||  -> equal(op(e0,op(e0,e4)),e4)**.
% 1.31/1.48  16[0:Inp] ||  -> equal(op(e1,op(e1,e0)),e0)**.
% 1.31/1.48  17[0:Inp] ||  -> equal(op(e1,op(e1,e1)),e1)**.
% 1.31/1.48  18[0:Inp] ||  -> equal(op(e1,op(e1,e2)),e2)**.
% 1.31/1.48  19[0:Inp] ||  -> equal(op(e1,op(e1,e3)),e3)**.
% 1.31/1.48  20[0:Inp] ||  -> equal(op(e1,op(e1,e4)),e4)**.
% 1.31/1.48  21[0:Inp] ||  -> equal(op(e2,op(e2,e0)),e0)**.
% 1.31/1.48  22[0:Inp] ||  -> equal(op(e2,op(e2,e1)),e1)**.
% 1.31/1.48  23[0:Inp] ||  -> equal(op(e2,op(e2,e2)),e2)**.
% 1.31/1.48  24[0:Inp] ||  -> equal(op(e2,op(e2,e3)),e3)**.
% 1.31/1.48  25[0:Inp] ||  -> equal(op(e2,op(e2,e4)),e4)**.
% 1.31/1.48  26[0:Inp] ||  -> equal(op(e3,op(e3,e0)),e0)**.
% 1.31/1.48  27[0:Inp] ||  -> equal(op(e3,op(e3,e1)),e1)**.
% 1.31/1.48  28[0:Inp] ||  -> equal(op(e3,op(e3,e2)),e2)**.
% 1.31/1.48  29[0:Inp] ||  -> equal(op(e3,op(e3,e3)),e3)**.
% 1.31/1.48  30[0:Inp] ||  -> equal(op(e3,op(e3,e4)),e4)**.
% 1.31/1.48  31[0:Inp] ||  -> equal(op(e4,op(e4,e0)),e0)**.
% 1.31/1.48  32[0:Inp] ||  -> equal(op(e4,op(e4,e1)),e1)**.
% 1.31/1.48  33[0:Inp] ||  -> equal(op(e4,op(e4,e2)),e2)**.
% 1.31/1.48  34[0:Inp] ||  -> equal(op(e4,op(e4,e3)),e3)**.
% 1.31/1.48  35[0:Inp] ||  -> equal(op(e4,op(e4,e4)),e4)**.
% 1.31/1.48  36[0:Inp] || equal(op(e1,e0),op(e0,e0))** -> .
% 1.31/1.48  37[0:Inp] || equal(op(e2,e0),op(e0,e0))** -> .
% 1.31/1.48  38[0:Inp] || equal(op(e3,e0),op(e0,e0))** -> .
% 1.31/1.48  39[0:Inp] || equal(op(e4,e0),op(e0,e0))** -> .
% 1.31/1.48  40[0:Inp] || equal(op(e2,e0),op(e1,e0))** -> .
% 1.31/1.48  41[0:Inp] || equal(op(e3,e0),op(e1,e0))** -> .
% 1.31/1.48  42[0:Inp] || equal(op(e4,e0),op(e1,e0))** -> .
% 1.31/1.48  43[0:Inp] || equal(op(e3,e0),op(e2,e0))** -> .
% 1.31/1.48  44[0:Inp] || equal(op(e4,e0),op(e2,e0))** -> .
% 1.31/1.48  45[0:Inp] || equal(op(e4,e0),op(e3,e0))** -> .
% 1.31/1.48  46[0:Inp] || equal(op(e1,e1),op(e0,e1))** -> .
% 1.31/1.48  47[0:Inp] || equal(op(e2,e1),op(e0,e1))** -> .
% 1.31/1.48  48[0:Inp] || equal(op(e3,e1),op(e0,e1))** -> .
% 1.31/1.48  49[0:Inp] || equal(op(e4,e1),op(e0,e1))** -> .
% 1.31/1.48  50[0:Inp] || equal(op(e2,e1),op(e1,e1))** -> .
% 1.31/1.48  51[0:Inp] || equal(op(e3,e1),op(e1,e1))** -> .
% 1.31/1.48  52[0:Inp] || equal(op(e4,e1),op(e1,e1))** -> .
% 1.31/1.48  53[0:Inp] || equal(op(e3,e1),op(e2,e1))** -> .
% 1.31/1.48  54[0:Inp] || equal(op(e4,e1),op(e2,e1))** -> .
% 1.31/1.48  56[0:Inp] || equal(op(e1,e2),op(e0,e2))** -> .
% 1.31/1.48  57[0:Inp] || equal(op(e2,e2),op(e0,e2))** -> .
% 1.31/1.48  58[0:Inp] || equal(op(e3,e2),op(e0,e2))** -> .
% 1.31/1.48  59[0:Inp] || equal(op(e4,e2),op(e0,e2))** -> .
% 1.31/1.48  60[0:Inp] || equal(op(e2,e2),op(e1,e2))** -> .
% 1.31/1.48  61[0:Inp] || equal(op(e3,e2),op(e1,e2))** -> .
% 1.31/1.48  62[0:Inp] || equal(op(e4,e2),op(e1,e2))** -> .
% 1.31/1.48  63[0:Inp] || equal(op(e3,e2),op(e2,e2))** -> .
% 1.31/1.48  64[0:Inp] || equal(op(e4,e2),op(e2,e2))** -> .
% 1.31/1.48  65[0:Inp] || equal(op(e4,e2),op(e3,e2))** -> .
% 1.31/1.48  66[0:Inp] || equal(op(e1,e3),op(e0,e3))** -> .
% 1.31/1.48  67[0:Inp] || equal(op(e2,e3),op(e0,e3))** -> .
% 1.31/1.48  69[0:Inp] || equal(op(e4,e3),op(e0,e3))** -> .
% 1.31/1.48  70[0:Inp] || equal(op(e2,e3),op(e1,e3))** -> .
% 1.31/1.48  71[0:Inp] || equal(op(e3,e3),op(e1,e3))** -> .
% 1.31/1.48  72[0:Inp] || equal(op(e4,e3),op(e1,e3))** -> .
% 1.31/1.48  73[0:Inp] || equal(op(e3,e3),op(e2,e3))** -> .
% 1.31/1.48  74[0:Inp] || equal(op(e4,e3),op(e2,e3))** -> .
% 1.31/1.48  75[0:Inp] || equal(op(e4,e3),op(e3,e3))** -> .
% 1.31/1.48  76[0:Inp] || equal(op(e1,e4),op(e0,e4))** -> .
% 1.31/1.48  77[0:Inp] || equal(op(e2,e4),op(e0,e4))** -> .
% 1.31/1.48  78[0:Inp] || equal(op(e3,e4),op(e0,e4))** -> .
% 1.31/1.48  79[0:Inp] || equal(op(e4,e4),op(e0,e4))** -> .
% 1.31/1.48  80[0:Inp] || equal(op(e2,e4),op(e1,e4))** -> .
% 1.31/1.48  81[0:Inp] || equal(op(e3,e4),op(e1,e4))** -> .
% 1.31/1.48  82[0:Inp] || equal(op(e4,e4),op(e1,e4))** -> .
% 1.31/1.48  84[0:Inp] || equal(op(e4,e4),op(e2,e4))** -> .
% 1.31/1.48  85[0:Inp] || equal(op(e4,e4),op(e3,e4))** -> .
% 1.31/1.48  86[0:Inp] || equal(op(e0,e1),op(e0,e0))** -> .
% 1.31/1.48  87[0:Inp] || equal(op(e0,e2),op(e0,e0))** -> .
% 1.31/1.48  88[0:Inp] || equal(op(e0,e3),op(e0,e0))** -> .
% 1.31/1.48  89[0:Inp] || equal(op(e0,e4),op(e0,e0))** -> .
% 1.31/1.48  90[0:Inp] || equal(op(e0,e2),op(e0,e1))** -> .
% 1.31/1.48  91[0:Inp] || equal(op(e0,e3),op(e0,e1))** -> .
% 1.31/1.48  92[0:Inp] || equal(op(e0,e4),op(e0,e1))** -> .
% 1.31/1.48  93[0:Inp] || equal(op(e0,e3),op(e0,e2))** -> .
% 1.31/1.48  94[0:Inp] || equal(op(e0,e4),op(e0,e2))** -> .
% 1.31/1.48  95[0:Inp] || equal(op(e0,e4),op(e0,e3))** -> .
% 1.31/1.48  97[0:Inp] || equal(op(e1,e2),op(e1,e0))** -> .
% 1.31/1.48  98[0:Inp] || equal(op(e1,e3),op(e1,e0))** -> .
% 1.31/1.48  99[0:Inp] || equal(op(e1,e4),op(e1,e0))** -> .
% 1.31/1.48  100[0:Inp] || equal(op(e1,e2),op(e1,e1))** -> .
% 1.31/1.48  101[0:Inp] || equal(op(e1,e3),op(e1,e1))** -> .
% 1.31/1.48  102[0:Inp] || equal(op(e1,e4),op(e1,e1))** -> .
% 1.31/1.48  103[0:Inp] || equal(op(e1,e3),op(e1,e2))** -> .
% 1.31/1.48  104[0:Inp] || equal(op(e1,e4),op(e1,e2))** -> .
% 1.31/1.48  105[0:Inp] || equal(op(e1,e4),op(e1,e3))** -> .
% 1.31/1.48  106[0:Inp] || equal(op(e2,e1),op(e2,e0))** -> .
% 1.31/1.48  107[0:Inp] || equal(op(e2,e2),op(e2,e0))** -> .
% 1.31/1.48  108[0:Inp] || equal(op(e2,e3),op(e2,e0))** -> .
% 1.31/1.48  109[0:Inp] || equal(op(e2,e4),op(e2,e0))** -> .
% 1.31/1.48  110[0:Inp] || equal(op(e2,e2),op(e2,e1))** -> .
% 1.31/1.48  111[0:Inp] || equal(op(e2,e3),op(e2,e1))** -> .
% 1.31/1.48  112[0:Inp] || equal(op(e2,e4),op(e2,e1))** -> .
% 1.31/1.48  113[0:Inp] || equal(op(e2,e3),op(e2,e2))** -> .
% 1.31/1.48  114[0:Inp] || equal(op(e2,e4),op(e2,e2))** -> .
% 1.31/1.48  115[0:Inp] || equal(op(e2,e4),op(e2,e3))** -> .
% 1.31/1.48  116[0:Inp] || equal(op(e3,e1),op(e3,e0))** -> .
% 1.31/1.48  117[0:Inp] || equal(op(e3,e2),op(e3,e0))** -> .
% 1.31/1.48  118[0:Inp] || equal(op(e3,e3),op(e3,e0))** -> .
% 1.31/1.48  119[0:Inp] || equal(op(e3,e4),op(e3,e0))** -> .
% 1.31/1.48  120[0:Inp] || equal(op(e3,e2),op(e3,e1))** -> .
% 1.31/1.48  121[0:Inp] || equal(op(e3,e3),op(e3,e1))** -> .
% 1.31/1.48  122[0:Inp] || equal(op(e3,e4),op(e3,e1))** -> .
% 1.31/1.48  123[0:Inp] || equal(op(e3,e3),op(e3,e2))** -> .
% 1.31/1.48  124[0:Inp] || equal(op(e3,e4),op(e3,e2))** -> .
% 1.31/1.48  125[0:Inp] || equal(op(e3,e4),op(e3,e3))** -> .
% 1.31/1.48  127[0:Inp] || equal(op(e4,e2),op(e4,e0))** -> .
% 1.31/1.48  128[0:Inp] || equal(op(e4,e3),op(e4,e0))** -> .
% 1.31/1.48  129[0:Inp] || equal(op(e4,e4),op(e4,e0))** -> .
% 1.31/1.48  130[0:Inp] || equal(op(e4,e2),op(e4,e1))** -> .
% 1.31/1.48  132[0:Inp] || equal(op(e4,e4),op(e4,e1))** -> .
% 1.31/1.48  133[0:Inp] || equal(op(e4,e3),op(e4,e2))** -> .
% 1.31/1.48  134[0:Inp] || equal(op(e4,e4),op(e4,e2))** -> .
% 1.31/1.48  135[0:Inp] || equal(op(e4,e4),op(e4,e3))** -> .
% 1.31/1.48  136[0:Inp] ||  -> equal(op(op(e0,e0),op(e0,e0)),e0)**.
% 1.31/1.48  137[0:Inp] ||  -> equal(op(op(e1,e0),op(e0,e1)),e0)**.
% 1.31/1.48  138[0:Inp] ||  -> equal(op(op(e2,e0),op(e0,e2)),e0)**.
% 1.31/1.48  139[0:Inp] ||  -> equal(op(op(e3,e0),op(e0,e3)),e0)**.
% 1.31/1.48  140[0:Inp] ||  -> equal(op(op(e4,e0),op(e0,e4)),e0)**.
% 1.31/1.48  141[0:Inp] ||  -> equal(op(op(e0,e1),op(e1,e0)),e1)**.
% 1.31/1.48  142[0:Inp] ||  -> equal(op(op(e1,e1),op(e1,e1)),e1)**.
% 1.31/1.48  143[0:Inp] ||  -> equal(op(op(e2,e1),op(e1,e2)),e1)**.
% 1.31/1.48  144[0:Inp] ||  -> equal(op(op(e3,e1),op(e1,e3)),e1)**.
% 1.31/1.48  145[0:Inp] ||  -> equal(op(op(e4,e1),op(e1,e4)),e1)**.
% 1.31/1.48  146[0:Inp] ||  -> equal(op(op(e0,e2),op(e2,e0)),e2)**.
% 1.31/1.48  147[0:Inp] ||  -> equal(op(op(e1,e2),op(e2,e1)),e2)**.
% 1.31/1.48  148[0:Inp] ||  -> equal(op(op(e2,e2),op(e2,e2)),e2)**.
% 1.31/1.48  149[0:Inp] ||  -> equal(op(op(e3,e2),op(e2,e3)),e2)**.
% 1.31/1.48  150[0:Inp] ||  -> equal(op(op(e4,e2),op(e2,e4)),e2)**.
% 1.31/1.48  151[0:Inp] ||  -> equal(op(op(e0,e3),op(e3,e0)),e3)**.
% 1.31/1.48  152[0:Inp] ||  -> equal(op(op(e1,e3),op(e3,e1)),e3)**.
% 1.31/1.48  153[0:Inp] ||  -> equal(op(op(e2,e3),op(e3,e2)),e3)**.
% 1.31/1.48  154[0:Inp] ||  -> equal(op(op(e3,e3),op(e3,e3)),e3)**.
% 1.31/1.48  156[0:Inp] ||  -> equal(op(op(e0,e4),op(e4,e0)),e4)**.
% 1.31/1.48  157[0:Inp] ||  -> equal(op(op(e1,e4),op(e4,e1)),e4)**.
% 1.31/1.48  158[0:Inp] ||  -> equal(op(op(e2,e4),op(e4,e2)),e4)**.
% 1.31/1.48  160[0:Inp] ||  -> equal(op(op(e4,e4),op(e4,e4)),e4)**.
% 1.31/1.48  165[0:Inp] || equal(op(e2,e3),e1) equal(op(e2,op(op(e2,e3),e2)),e0)** equal(op(op(e2,e3),e2),e4) -> .
% 1.31/1.48  168[0:Inp] || equal(op(e0,e2),e1) equal(op(e0,op(op(e0,e2),e0)),e3)** equal(op(op(e0,e2),e0),e4) -> .
% 1.31/1.48  181[0:Inp] || equal(op(e3,e0),e1) equal(op(e3,op(op(e3,e0),e3)),e2)** equal(op(op(e3,e0),e3),e4) -> .
% 1.31/1.48  198[0:Inp] || equal(op(e0,e1),e2) equal(op(e0,op(op(e0,e1),e0)),e4)** equal(op(op(e0,e1),e0),e3) -> .
% 1.31/1.48  200[0:Inp] || equal(op(e0,e1),e4) equal(op(e0,op(op(e0,e1),e0)),e2)** equal(op(op(e0,e1),e0),e3) -> .
% 1.31/1.48  201[0:Inp] || equal(op(e4,e1),e2) equal(op(e4,op(op(e4,e1),e4)),e0)** equal(op(op(e4,e1),e4),e3) -> .
% 1.31/1.48  209[0:Inp] || equal(op(e1,e4),e0) equal(op(e1,op(op(e1,e4),e1)),e3)** equal(op(op(e1,e4),e1),e2) -> .
% 1.31/1.48  210[0:Inp] || equal(op(e0,e4),e1) equal(op(e0,op(op(e0,e4),e0)),e3)** equal(op(op(e0,e4),e0),e2) -> .
% 1.31/1.48  228[0:Inp] || equal(op(e1,e0),e3) equal(op(e1,op(op(e1,e0),e1)),e4)** equal(op(op(e1,e0),e1),e2) -> .
% 1.31/1.48  255[0:Inp] || equal(op(e4,e0),e3) equal(op(e4,op(op(e4,e0),e4)),e2)** equal(op(op(e4,e0),e4),e1) -> .
% 1.31/1.48  258[0:Inp] || equal(op(e1,e4),e2) equal(op(e1,op(op(e1,e4),e1)),e3)** equal(op(op(e1,e4),e1),e0) -> .
% 1.31/1.48  260[0:Inp] || equal(op(e1,e4),e3) equal(op(e1,op(op(e1,e4),e1)),e2)** equal(op(op(e1,e4),e1),e0) -> .
% 1.31/1.48  266[0:Inp] || equal(op(e1,e3),e4) equal(op(e1,op(op(e1,e3),e1)),e2)** equal(op(op(e1,e3),e1),e0) -> .
% 1.31/1.48  268[0:Inp] || equal(op(e2,e3),e4) equal(op(e2,op(op(e2,e3),e2)),e1)** equal(op(op(e2,e3),e2),e0) -> .
% 1.31/1.48  272[0:Inp] || equal(op(e1,e2),e4) equal(op(e1,op(op(e1,e2),e1)),e3)** equal(op(op(e1,e2),e1),e0) -> .
% 1.31/1.48  280[0:Inp] || equal(op(e3,e1),e4) equal(op(e3,op(op(e3,e1),e3)),e2)** equal(op(op(e3,e1),e3),e0) -> .
% 1.31/1.48  282[0:Inp] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e3),e4) equal(op(e4,e2),e4) equal(op(e4,e1),e4) equal(op(e4,e0),e4).
% 1.31/1.48  283[0:Inp] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3) equal(op(e2,e4),e3) equal(op(e1,e4),e3) equal(op(e0,e4),e3).
% 1.31/1.48  284[0:Inp] ||  -> equal(op(e4,e4),e3)** equal(op(e4,e3),e3) equal(op(e4,e2),e3) equal(op(e4,e1),e3) equal(op(e4,e0),e3).
% 1.31/1.48  285[0:Inp] ||  -> equal(op(e4,e4),e2)** equal(op(e2,e4),e2) equal(op(e3,e4),e2) equal(op(e1,e4),e2) equal(op(e0,e4),e2).
% 1.31/1.48  286[0:Inp] ||  -> equal(op(e4,e4),e2)** equal(op(e4,e2),e2) equal(op(e4,e3),e2) equal(op(e4,e1),e2) equal(op(e4,e0),e2).
% 1.31/1.48  287[0:Inp] ||  -> equal(op(e4,e4),e1)** equal(op(e1,e4),e1) equal(op(e3,e4),e1) equal(op(e2,e4),e1) equal(op(e0,e4),e1).
% 1.31/1.48  288[0:Inp] ||  -> equal(op(e4,e4),e1)** equal(op(e4,e1),e1) equal(op(e4,e3),e1) equal(op(e4,e2),e1) equal(op(e4,e0),e1).
% 1.31/1.48  289[0:Inp] ||  -> equal(op(e4,e4),e0)** equal(op(e0,e4),e0) equal(op(e3,e4),e0) equal(op(e2,e4),e0) equal(op(e1,e4),e0).
% 1.31/1.48  290[0:Inp] ||  -> equal(op(e4,e4),e0)** equal(op(e4,e0),e0) equal(op(e4,e3),e0) equal(op(e4,e2),e0) equal(op(e4,e1),e0).
% 1.31/1.48  291[0:Inp] ||  -> equal(op(e4,e3),e4)** equal(op(e3,e3),e4) equal(op(e2,e3),e4) equal(op(e1,e3),e4) equal(op(e0,e3),e4).
% 1.31/1.48  292[0:Inp] ||  -> equal(op(e3,e4),e4)** equal(op(e3,e3),e4) equal(op(e3,e2),e4) equal(op(e3,e1),e4) equal(op(e3,e0),e4).
% 1.31/1.48  293[0:Inp] ||  -> equal(op(e3,e3),e3) equal(op(e4,e3),e3)** equal(op(e2,e3),e3) equal(op(e1,e3),e3) equal(op(e0,e3),e3).
% 1.31/1.48  294[0:Inp] ||  -> equal(op(e3,e3),e3) equal(op(e3,e4),e3)** equal(op(e3,e2),e3) equal(op(e3,e1),e3) equal(op(e3,e0),e3).
% 1.31/1.48  295[0:Inp] ||  -> equal(op(e3,e3),e2) equal(op(e2,e3),e2) equal(op(e4,e3),e2)** equal(op(e1,e3),e2) equal(op(e0,e3),e2).
% 1.31/1.48  296[0:Inp] ||  -> equal(op(e3,e3),e2) equal(op(e3,e2),e2) equal(op(e3,e4),e2)** equal(op(e3,e1),e2) equal(op(e3,e0),e2).
% 1.31/1.48  297[0:Inp] ||  -> equal(op(e3,e3),e1) equal(op(e1,e3),e1) equal(op(e4,e3),e1)** equal(op(e2,e3),e1) equal(op(e0,e3),e1).
% 1.31/1.48  298[0:Inp] ||  -> equal(op(e3,e3),e1) equal(op(e3,e1),e1) equal(op(e3,e4),e1)** equal(op(e3,e2),e1) equal(op(e3,e0),e1).
% 1.31/1.48  299[0:Inp] ||  -> equal(op(e3,e3),e0) equal(op(e0,e3),e0) equal(op(e4,e3),e0)** equal(op(e2,e3),e0) equal(op(e1,e3),e0).
% 1.31/1.48  301[0:Inp] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e3,e2),e4) equal(op(e1,e2),e4) equal(op(e0,e2),e4).
% 1.31/1.48  302[0:Inp] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4) equal(op(e2,e3),e4) equal(op(e2,e1),e4) equal(op(e2,e0),e4).
% 1.31/1.48  303[0:Inp] ||  -> equal(op(e3,e2),e3) equal(op(e2,e2),e3) equal(op(e4,e2),e3)** equal(op(e1,e2),e3) equal(op(e0,e2),e3).
% 1.31/1.48  307[0:Inp] ||  -> equal(op(e2,e2),e1) equal(op(e1,e2),e1) equal(op(e4,e2),e1)** equal(op(e3,e2),e1) equal(op(e0,e2),e1).
% 1.31/1.48  308[0:Inp] ||  -> equal(op(e2,e2),e1) equal(op(e2,e1),e1) equal(op(e2,e4),e1)** equal(op(e2,e3),e1) equal(op(e2,e0),e1).
% 1.31/1.48  309[0:Inp] ||  -> equal(op(e2,e2),e0) equal(op(e0,e2),e0) equal(op(e4,e2),e0)** equal(op(e3,e2),e0) equal(op(e1,e2),e0).
% 1.31/1.48  310[0:Inp] ||  -> equal(op(e2,e2),e0) equal(op(e2,e0),e0) equal(op(e2,e4),e0)** equal(op(e2,e3),e0) equal(op(e2,e1),e0).
% 1.31/1.48  311[0:Inp] ||  -> equal(op(e4,e1),e4)** equal(op(e1,e1),e4) equal(op(e3,e1),e4) equal(op(e2,e1),e4) equal(op(e0,e1),e4).
% 1.31/1.48  312[0:Inp] ||  -> equal(op(e1,e4),e4)** equal(op(e1,e1),e4) equal(op(e1,e3),e4) equal(op(e1,e2),e4) equal(op(e1,e0),e4).
% 1.31/1.48  313[0:Inp] ||  -> equal(op(e3,e1),e3) equal(op(e1,e1),e3) equal(op(e4,e1),e3)** equal(op(e2,e1),e3) equal(op(e0,e1),e3).
% 1.31/1.48  314[0:Inp] ||  -> equal(op(e1,e3),e3) equal(op(e1,e1),e3) equal(op(e1,e4),e3)** equal(op(e1,e2),e3) equal(op(e1,e0),e3).
% 1.31/1.48  315[0:Inp] ||  -> equal(op(e2,e1),e2) equal(op(e1,e1),e2) equal(op(e4,e1),e2)** equal(op(e3,e1),e2) equal(op(e0,e1),e2).
% 1.31/1.48  316[0:Inp] ||  -> equal(op(e1,e2),e2) equal(op(e1,e1),e2) equal(op(e1,e4),e2)** equal(op(e1,e3),e2) equal(op(e1,e0),e2).
% 1.31/1.48  317[0:Inp] ||  -> equal(op(e1,e1),e1) equal(op(e4,e1),e1)** equal(op(e3,e1),e1) equal(op(e2,e1),e1) equal(op(e0,e1),e1).
% 1.31/1.48  318[0:Inp] ||  -> equal(op(e1,e1),e1) equal(op(e1,e4),e1)** equal(op(e1,e3),e1) equal(op(e1,e2),e1) equal(op(e1,e0),e1).
% 1.31/1.48  319[0:Inp] ||  -> equal(op(e1,e1),e0) equal(op(e0,e1),e0) equal(op(e4,e1),e0)** equal(op(e3,e1),e0) equal(op(e2,e1),e0).
% 1.31/1.48  320[0:Inp] ||  -> equal(op(e1,e1),e0) equal(op(e1,e0),e0) equal(op(e1,e4),e0)** equal(op(e1,e3),e0) equal(op(e1,e2),e0).
% 1.31/1.48  321[0:Inp] ||  -> equal(op(e4,e0),e4)** equal(op(e0,e0),e4) equal(op(e3,e0),e4) equal(op(e2,e0),e4) equal(op(e1,e0),e4).
% 1.31/1.48  322[0:Inp] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e0),e4) equal(op(e0,e3),e4) equal(op(e0,e2),e4) equal(op(e0,e1),e4).
% 1.31/1.48  323[0:Inp] ||  -> equal(op(e3,e0),e3) equal(op(e0,e0),e3) equal(op(e4,e0),e3)** equal(op(e2,e0),e3) equal(op(e1,e0),e3).
% 1.31/1.48  324[0:Inp] ||  -> equal(op(e0,e3),e3) equal(op(e0,e0),e3) equal(op(e0,e4),e3)** equal(op(e0,e2),e3) equal(op(e0,e1),e3).
% 1.31/1.48  325[0:Inp] ||  -> equal(op(e2,e0),e2) equal(op(e0,e0),e2) equal(op(e4,e0),e2)** equal(op(e3,e0),e2) equal(op(e1,e0),e2).
% 1.31/1.48  326[0:Inp] ||  -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e4),e2)** equal(op(e0,e3),e2) equal(op(e0,e1),e2).
% 1.31/1.48  327[0:Inp] ||  -> equal(op(e1,e0),e1) equal(op(e0,e0),e1) equal(op(e4,e0),e1)** equal(op(e3,e0),e1) equal(op(e2,e0),e1).
% 1.31/1.48  329[0:Inp] ||  -> equal(op(e0,e0),e0) equal(op(e4,e0),e0)** equal(op(e3,e0),e0) equal(op(e2,e0),e0) equal(op(e1,e0),e0).
% 1.31/1.48  330[0:Inp] ||  -> equal(op(e0,e0),e0) equal(op(e0,e4),e0)** equal(op(e0,e3),e0) equal(op(e0,e2),e0) equal(op(e0,e1),e0).
% 1.31/1.48  331[0:Inp] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e4),e3) equal(op(e4,e4),e2) equal(op(e4,e4),e1) equal(op(e4,e4),e0).
% 1.31/1.48  332[0:Inp] ||  -> equal(op(e4,e3),e4)** equal(op(e4,e3),e3) equal(op(e4,e3),e2) equal(op(e4,e3),e1) equal(op(e4,e3),e0).
% 1.31/1.48  333[0:Inp] ||  -> equal(op(e4,e2),e4)** equal(op(e4,e2),e2) equal(op(e4,e2),e3) equal(op(e4,e2),e1) equal(op(e4,e2),e0).
% 1.31/1.48  335[0:Inp] ||  -> equal(op(e4,e0),e4)** equal(op(e4,e0),e0) equal(op(e4,e0),e3) equal(op(e4,e0),e2) equal(op(e4,e0),e1).
% 1.31/1.48  336[0:Inp] ||  -> equal(op(e3,e4),e4)** equal(op(e3,e4),e3) equal(op(e3,e4),e2) equal(op(e3,e4),e1) equal(op(e3,e4),e0).
% 1.31/1.48  337[0:Inp] ||  -> equal(op(e3,e3),e3) equal(op(e3,e3),e4)** equal(op(e3,e3),e2) equal(op(e3,e3),e1) equal(op(e3,e3),e0).
% 1.31/1.48  338[0:Inp] ||  -> equal(op(e3,e2),e3) equal(op(e3,e2),e2) equal(op(e3,e2),e4)** equal(op(e3,e2),e1) equal(op(e3,e2),e0).
% 1.31/1.48  339[0:Inp] ||  -> equal(op(e3,e1),e3) equal(op(e3,e1),e1) equal(op(e3,e1),e4)** equal(op(e3,e1),e2) equal(op(e3,e1),e0).
% 1.31/1.48  340[0:Inp] ||  -> equal(op(e3,e0),e3) equal(op(e3,e0),e0) equal(op(e3,e0),e4)** equal(op(e3,e0),e2) equal(op(e3,e0),e1).
% 1.31/1.48  341[0:Inp] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e4),e2) equal(op(e2,e4),e3) equal(op(e2,e4),e1) equal(op(e2,e4),e0).
% 1.31/1.48  342[0:Inp] ||  -> equal(op(e2,e3),e3) equal(op(e2,e3),e2) equal(op(e2,e3),e4)** equal(op(e2,e3),e1) equal(op(e2,e3),e0).
% 1.31/1.48  343[0:Inp] ||  -> equal(op(e2,e2),e2) equal(op(e2,e2),e4)** equal(op(e2,e2),e3) equal(op(e2,e2),e1) equal(op(e2,e2),e0).
% 1.31/1.48  344[0:Inp] ||  -> equal(op(e2,e1),e2) equal(op(e2,e1),e1) equal(op(e2,e1),e4)** equal(op(e2,e1),e3) equal(op(e2,e1),e0).
% 1.31/1.48  345[0:Inp] ||  -> equal(op(e2,e0),e2) equal(op(e2,e0),e0) equal(op(e2,e0),e4)** equal(op(e2,e0),e3) equal(op(e2,e0),e1).
% 1.31/1.48  346[0:Inp] ||  -> equal(op(e1,e4),e4)** equal(op(e1,e4),e1) equal(op(e1,e4),e3) equal(op(e1,e4),e2) equal(op(e1,e4),e0).
% 1.31/1.48  347[0:Inp] ||  -> equal(op(e1,e3),e3) equal(op(e1,e3),e1) equal(op(e1,e3),e4)** equal(op(e1,e3),e2) equal(op(e1,e3),e0).
% 1.31/1.48  348[0:Inp] ||  -> equal(op(e1,e2),e2) equal(op(e1,e2),e1) equal(op(e1,e2),e4)** equal(op(e1,e2),e3) equal(op(e1,e2),e0).
% 1.31/1.48  349[0:Inp] ||  -> equal(op(e1,e1),e1) equal(op(e1,e1),e4)** equal(op(e1,e1),e3) equal(op(e1,e1),e2) equal(op(e1,e1),e0).
% 1.31/1.48  350[0:Inp] ||  -> equal(op(e1,e0),e1) equal(op(e1,e0),e0) equal(op(e1,e0),e4)** equal(op(e1,e0),e3) equal(op(e1,e0),e2).
% 1.31/1.48  351[0:Inp] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e4),e0) equal(op(e0,e4),e3) equal(op(e0,e4),e2) equal(op(e0,e4),e1).
% 1.31/1.48  352[0:Inp] ||  -> equal(op(e0,e3),e3) equal(op(e0,e3),e0) equal(op(e0,e3),e4)** equal(op(e0,e3),e2) equal(op(e0,e3),e1).
% 1.31/1.48  353[0:Inp] ||  -> equal(op(e0,e2),e2) equal(op(e0,e2),e0) equal(op(e0,e2),e4)** equal(op(e0,e2),e3) equal(op(e0,e2),e1).
% 1.31/1.48  354[0:Inp] ||  -> equal(op(e0,e1),e1) equal(op(e0,e1),e0) equal(op(e0,e1),e4)** equal(op(e0,e1),e3) equal(op(e0,e1),e2).
% 1.31/1.48  355[0:Inp] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e4)** equal(op(e0,e0),e3) equal(op(e0,e0),e2) equal(op(e0,e0),e1).
% 1.31/1.48  356[1:Spt:354.0] ||  -> equal(op(e0,e1),e1)**.
% 1.31/1.48  380[1:Rew:356.0,141.0] ||  -> equal(op(e1,op(e1,e0)),e1)**.
% 1.31/1.48  398[1:Rew:16.0,380.0] ||  -> equal(e1,e0)**.
% 1.31/1.48  399[1:MRR:398.0,1.0] ||  -> .
% 1.31/1.48  424[1:Spt:399.0,354.0,356.0] || equal(op(e0,e1),e1)** -> .
% 1.31/1.48  425[1:Spt:399.0,354.1,354.2,354.3,354.4] ||  -> equal(op(e0,e1),e0) equal(op(e0,e1),e4)** equal(op(e0,e1),e3) equal(op(e0,e1),e2).
% 1.31/1.48  426[1:MRR:317.4,424.0] ||  -> equal(op(e1,e1),e1) equal(op(e4,e1),e1)** equal(op(e3,e1),e1) equal(op(e2,e1),e1).
% 1.31/1.48  428[2:Spt:425.0] ||  -> equal(op(e0,e1),e0)**.
% 1.31/1.48  430[2:Rew:428.0,12.0] ||  -> equal(op(e0,e0),e1)**.
% 1.31/1.48  440[2:Rew:428.0,141.0] ||  -> equal(op(e0,op(e1,e0)),e1)**.
% 1.31/1.48  465[2:Rew:430.0,136.0] ||  -> equal(op(e1,e1),e0)**.
% 1.31/1.48  469[2:Rew:465.0,17.0] ||  -> equal(op(e1,e0),e1)**.
% 1.31/1.48  525[2:Rew:428.0,440.0,469.0,440.0] ||  -> equal(e1,e0)**.
% 1.31/1.48  526[2:MRR:525.0,1.0] ||  -> .
% 1.31/1.48  573[2:Spt:526.0,425.0,428.0] || equal(op(e0,e1),e0)** -> .
% 1.31/1.48  574[2:Spt:526.0,425.1,425.2,425.3] ||  -> equal(op(e0,e1),e4)** equal(op(e0,e1),e3) equal(op(e0,e1),e2).
% 1.31/1.48  575[2:MRR:330.4,573.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e4),e0)** equal(op(e0,e3),e0) equal(op(e0,e2),e0).
% 1.31/1.48  576[2:MRR:319.1,573.0] ||  -> equal(op(e1,e1),e0) equal(op(e4,e1),e0)** equal(op(e3,e1),e0) equal(op(e2,e1),e0).
% 1.31/1.48  577[3:Spt:574.0] ||  -> equal(op(e0,e1),e4)**.
% 1.31/1.48  580[3:Rew:577.0,12.0] ||  -> equal(op(e0,e4),e1)**.
% 1.31/1.48  582[3:Rew:577.0,91.0] || equal(op(e0,e3),e4)** -> .
% 1.31/1.48  583[3:Rew:577.0,90.0] || equal(op(e0,e2),e4)** -> .
% 1.31/1.48  584[3:Rew:577.0,86.0] || equal(op(e0,e0),e4)** -> .
% 1.31/1.48  585[3:Rew:577.0,49.0] || equal(op(e4,e1),e4)** -> .
% 1.31/1.48  587[3:Rew:577.0,47.0] || equal(op(e2,e1),e4)** -> .
% 1.31/1.48  588[3:Rew:577.0,46.0] || equal(op(e1,e1),e4)** -> .
% 1.31/1.48  589[3:Rew:577.0,141.0] ||  -> equal(op(e4,op(e1,e0)),e1)**.
% 1.31/1.48  590[3:Rew:577.0,137.0] ||  -> equal(op(op(e1,e0),e4),e0)**.
% 1.31/1.48  592[3:Rew:577.0,200.0] || equal(e4,e4) equal(op(e0,op(op(e0,e1),e0)),e2)** equal(op(op(e0,e1),e0),e3) -> .
% 1.31/1.48  593[3:Rew:577.0,313.4] ||  -> equal(op(e3,e1),e3) equal(op(e1,e1),e3) equal(op(e4,e1),e3)** equal(op(e2,e1),e3) equal(e4,e3).
% 1.31/1.48  594[3:Rew:577.0,324.4] ||  -> equal(op(e0,e3),e3) equal(op(e0,e0),e3) equal(op(e0,e4),e3)** equal(op(e0,e2),e3) equal(e4,e3).
% 1.31/1.48  598[3:Rew:577.0,326.4] ||  -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e4),e2)** equal(op(e0,e3),e2) equal(e4,e2).
% 1.31/1.48  605[3:Rew:580.0,210.1] || equal(op(e0,e4),e1) equal(op(e0,op(e1,e0)),e3) equal(op(op(e0,e4),e0),e2)** -> .
% 1.31/1.48  608[3:Rew:580.0,283.4] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3) equal(op(e2,e4),e3) equal(op(e1,e4),e3) equal(e3,e1).
% 1.31/1.48  611[3:Rew:580.0,95.0] || equal(op(e0,e3),e1)** -> .
% 1.31/1.48  612[3:Rew:580.0,94.0] || equal(op(e0,e2),e1)** -> .
% 1.31/1.48  613[3:Rew:580.0,79.0] || equal(op(e4,e4),e1)** -> .
% 1.31/1.48  614[3:Rew:580.0,78.0] || equal(op(e3,e4),e1)** -> .
% 1.31/1.48  615[3:Rew:580.0,77.0] || equal(op(e2,e4),e1)** -> .
% 1.31/1.48  616[3:Rew:580.0,76.0] || equal(op(e1,e4),e1)** -> .
% 1.31/1.48  617[3:Rew:580.0,156.0] ||  -> equal(op(e1,op(e4,e0)),e4)**.
% 1.31/1.48  618[3:Rew:580.0,140.0] ||  -> equal(op(op(e4,e0),e1),e0)**.
% 1.31/1.48  619[3:Rew:580.0,89.0] || equal(op(e0,e0),e1)** -> .
% 1.31/1.48  621[3:Rew:580.0,289.1] ||  -> equal(op(e4,e4),e0)** equal(e1,e0) equal(op(e3,e4),e0) equal(op(e2,e4),e0) equal(op(e1,e4),e0).
% 1.31/1.48  623[3:MRR:291.4,582.0] ||  -> equal(op(e4,e3),e4)** equal(op(e3,e3),e4) equal(op(e2,e3),e4) equal(op(e1,e3),e4).
% 1.31/1.48  624[3:MRR:352.2,582.0] ||  -> equal(op(e0,e3),e3)** equal(op(e0,e3),e0) equal(op(e0,e3),e2) equal(op(e0,e3),e1).
% 1.31/1.48  625[3:MRR:301.4,583.0] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e3,e2),e4) equal(op(e1,e2),e4).
% 1.31/1.48  626[3:MRR:353.2,583.0] ||  -> equal(op(e0,e2),e2) equal(op(e0,e2),e0) equal(op(e0,e2),e3)** equal(op(e0,e2),e1).
% 1.31/1.48  627[3:MRR:321.1,584.0] ||  -> equal(op(e4,e0),e4)** equal(op(e3,e0),e4) equal(op(e2,e0),e4) equal(op(e1,e0),e4).
% 1.31/1.48  628[3:MRR:355.1,584.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e3)** equal(op(e0,e0),e2) equal(op(e0,e0),e1).
% 1.31/1.48  629[3:MRR:282.3,585.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e3),e4) equal(op(e4,e2),e4) equal(op(e4,e0),e4).
% 1.31/1.48  633[3:MRR:302.3,587.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4) equal(op(e2,e3),e4) equal(op(e2,e0),e4).
% 1.31/1.48  635[3:MRR:312.1,588.0] ||  -> equal(op(e1,e4),e4)** equal(op(e1,e3),e4) equal(op(e1,e2),e4) equal(op(e1,e0),e4).
% 1.31/1.48  637[3:MRR:297.4,611.0] ||  -> equal(op(e3,e3),e1) equal(op(e1,e3),e1) equal(op(e4,e3),e1)** equal(op(e2,e3),e1).
% 1.31/1.48  638[3:MRR:307.4,612.0] ||  -> equal(op(e2,e2),e1) equal(op(e1,e2),e1) equal(op(e4,e2),e1)** equal(op(e3,e2),e1).
% 1.31/1.48  639[3:MRR:331.3,613.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e4),e3) equal(op(e4,e4),e2) equal(op(e4,e4),e0).
% 1.31/1.48  640[3:MRR:288.0,613.0] ||  -> equal(op(e4,e1),e1) equal(op(e4,e3),e1)** equal(op(e4,e2),e1) equal(op(e4,e0),e1).
% 1.31/1.48  642[3:MRR:298.2,614.0] ||  -> equal(op(e3,e3),e1)** equal(op(e3,e1),e1) equal(op(e3,e2),e1) equal(op(e3,e0),e1).
% 1.31/1.48  643[3:MRR:341.3,615.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e4),e2) equal(op(e2,e4),e3) equal(op(e2,e4),e0).
% 1.31/1.48  646[3:MRR:318.1,616.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e3),e1)** equal(op(e1,e2),e1) equal(op(e1,e0),e1).
% 1.31/1.48  647[3:MRR:327.1,619.0] ||  -> equal(op(e1,e0),e1) equal(op(e4,e0),e1)** equal(op(e3,e0),e1) equal(op(e2,e0),e1).
% 1.31/1.48  649[3:MRR:624.3,611.0] ||  -> equal(op(e0,e3),e3)** equal(op(e0,e3),e0) equal(op(e0,e3),e2).
% 1.31/1.48  650[3:MRR:626.3,612.0] ||  -> equal(op(e0,e2),e2) equal(op(e0,e2),e0) equal(op(e0,e2),e3)**.
% 1.31/1.48  651[3:MRR:628.3,619.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e3)** equal(op(e0,e0),e2).
% 1.31/1.48  654[3:Obv:592.0] || equal(op(e0,op(op(e0,e1),e0)),e2)** equal(op(op(e0,e1),e0),e3) -> .
% 1.31/1.48  655[3:Rew:577.0,654.1,577.0,654.0] || equal(op(e0,op(e4,e0)),e2)** equal(op(e4,e0),e3) -> .
% 1.31/1.48  661[3:Rew:580.0,605.2,580.0,605.0] || equal(e1,e1) equal(op(e0,op(e1,e0)),e3)** equal(op(e1,e0),e2) -> .
% 1.31/1.48  662[3:Obv:661.0] || equal(op(e0,op(e1,e0)),e3)** equal(op(e1,e0),e2) -> .
% 1.31/1.48  664[3:MRR:593.4,10.0] ||  -> equal(op(e3,e1),e3) equal(op(e1,e1),e3) equal(op(e4,e1),e3)** equal(op(e2,e1),e3).
% 1.31/1.48  665[3:Rew:580.0,594.2] ||  -> equal(op(e0,e3),e3)** equal(op(e0,e0),e3) equal(e3,e1) equal(op(e0,e2),e3) equal(e4,e3).
% 1.31/1.48  666[3:MRR:665.2,665.4,6.0,10.0] ||  -> equal(op(e0,e3),e3)** equal(op(e0,e0),e3) equal(op(e0,e2),e3).
% 1.31/1.48  668[3:Rew:580.0,598.2] ||  -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(e2,e1) equal(op(e0,e3),e2)** equal(e4,e2).
% 1.31/1.48  669[3:MRR:668.2,668.4,5.0,9.0] ||  -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e3),e2)**.
% 1.31/1.48  671[3:MRR:608.4,6.0] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3) equal(op(e2,e4),e3) equal(op(e1,e4),e3).
% 1.31/1.48  673[3:MRR:621.1,1.0] ||  -> equal(op(e4,e4),e0)** equal(op(e3,e4),e0) equal(op(e2,e4),e0) equal(op(e1,e4),e0).
% 1.31/1.48  675[4:Spt:342.0] ||  -> equal(op(e2,e3),e3)**.
% 1.31/1.48  699[4:Rew:675.0,153.0] ||  -> equal(op(e3,op(e3,e2)),e3)**.
% 1.31/1.48  717[4:Rew:28.0,699.0] ||  -> equal(e3,e2)**.
% 1.31/1.48  718[4:MRR:717.0,8.0] ||  -> .
% 1.31/1.48  743[4:Spt:718.0,342.0,675.0] || equal(op(e2,e3),e3)** -> .
% 1.31/1.48  744[4:Spt:718.0,342.1,342.2,342.3,342.4] ||  -> equal(op(e2,e3),e2) equal(op(e2,e3),e4)** equal(op(e2,e3),e1) equal(op(e2,e3),e0).
% 1.31/1.48  747[5:Spt:744.0] ||  -> equal(op(e2,e3),e2)**.
% 1.31/1.48  749[5:Rew:747.0,24.0] ||  -> equal(op(e2,e2),e3)**.
% 1.31/1.48  759[5:Rew:747.0,153.0] ||  -> equal(op(e2,op(e3,e2)),e3)**.
% 1.31/1.48  784[5:Rew:749.0,148.0] ||  -> equal(op(e3,e3),e2)**.
% 1.31/1.48  788[5:Rew:784.0,29.0] ||  -> equal(op(e3,e2),e3)**.
% 1.31/1.48  844[5:Rew:747.0,759.0,788.0,759.0] ||  -> equal(e3,e2)**.
% 1.31/1.48  845[5:MRR:844.0,8.0] ||  -> .
% 1.31/1.48  892[5:Spt:845.0,744.0,747.0] || equal(op(e2,e3),e2)** -> .
% 1.31/1.48  893[5:Spt:845.0,744.1,744.2,744.3] ||  -> equal(op(e2,e3),e4)** equal(op(e2,e3),e1) equal(op(e2,e3),e0).
% 1.31/1.48  896[6:Spt:893.0] ||  -> equal(op(e2,e3),e4)**.
% 1.31/1.48  899[6:Rew:896.0,24.0] ||  -> equal(op(e2,e4),e3)**.
% 1.31/1.48  901[6:Rew:896.0,113.0] || equal(op(e2,e2),e4)** -> .
% 1.31/1.48  903[6:Rew:896.0,108.0] || equal(op(e2,e0),e4)** -> .
% 1.31/1.48  904[6:Rew:896.0,74.0] || equal(op(e4,e3),e4)** -> .
% 1.31/1.48  905[6:Rew:896.0,73.0] || equal(op(e3,e3),e4)** -> .
% 1.31/1.48  906[6:Rew:896.0,70.0] || equal(op(e1,e3),e4)** -> .
% 1.31/1.48  908[6:Rew:896.0,153.0] ||  -> equal(op(e4,op(e3,e2)),e3)**.
% 1.31/1.48  909[6:Rew:896.0,149.0] ||  -> equal(op(op(e3,e2),e4),e2)**.
% 1.31/1.48  915[6:Rew:896.0,637.3] ||  -> equal(op(e3,e3),e1) equal(op(e1,e3),e1) equal(op(e4,e3),e1)** equal(e4,e1).
% 1.31/1.48  926[6:Rew:899.0,112.0] || equal(op(e2,e1),e3)** -> .
% 1.31/1.48  927[6:Rew:899.0,109.0] || equal(op(e2,e0),e3)** -> .
% 1.31/1.48  928[6:Rew:899.0,84.0] || equal(op(e4,e4),e3)** -> .
% 1.31/1.48  932[6:Rew:899.0,150.0] ||  -> equal(op(op(e4,e2),e3),e2)**.
% 1.31/1.48  935[6:Rew:899.0,114.0] || equal(op(e2,e2),e3)** -> .
% 1.31/1.48  939[6:MRR:625.1,901.0] ||  -> equal(op(e4,e2),e4)** equal(op(e3,e2),e4) equal(op(e1,e2),e4).
% 1.31/1.48  941[6:MRR:627.2,903.0] ||  -> equal(op(e4,e0),e4)** equal(op(e3,e0),e4) equal(op(e1,e0),e4).
% 1.31/1.48  943[6:MRR:629.1,904.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e2),e4) equal(op(e4,e0),e4).
% 1.31/1.48  946[6:MRR:337.1,905.0] ||  -> equal(op(e3,e3),e3)** equal(op(e3,e3),e2) equal(op(e3,e3),e1) equal(op(e3,e3),e0).
% 1.31/1.48  947[6:MRR:635.1,906.0] ||  -> equal(op(e1,e4),e4)** equal(op(e1,e2),e4) equal(op(e1,e0),e4).
% 1.31/1.48  948[6:MRR:347.2,906.0] ||  -> equal(op(e1,e3),e3)** equal(op(e1,e3),e1) equal(op(e1,e3),e2) equal(op(e1,e3),e0).
% 1.31/1.48  949[6:MRR:664.3,926.0] ||  -> equal(op(e3,e1),e3) equal(op(e1,e1),e3) equal(op(e4,e1),e3)**.
% 1.31/1.48  951[6:MRR:323.3,927.0] ||  -> equal(op(e3,e0),e3) equal(op(e0,e0),e3) equal(op(e4,e0),e3)** equal(op(e1,e0),e3).
% 1.31/1.48  952[6:MRR:639.1,928.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e4),e2) equal(op(e4,e4),e0).
% 1.31/1.48  953[6:MRR:284.0,928.0] ||  -> equal(op(e4,e3),e3)** equal(op(e4,e2),e3) equal(op(e4,e1),e3) equal(op(e4,e0),e3).
% 1.31/1.48  958[6:MRR:303.1,935.0] ||  -> equal(op(e3,e2),e3) equal(op(e4,e2),e3)** equal(op(e1,e2),e3) equal(op(e0,e2),e3).
% 1.31/1.48  960[6:MRR:915.3,7.0] ||  -> equal(op(e3,e3),e1) equal(op(e1,e3),e1) equal(op(e4,e3),e1)**.
% 1.31/1.48  981[7:Spt:335.0] ||  -> equal(op(e4,e0),e4)**.
% 1.31/1.48  994[7:Rew:981.0,31.0] ||  -> equal(op(e4,e4),e0)**.
% 1.31/1.48  997[7:Rew:981.0,127.0] || equal(op(e4,e2),e4)** -> .
% 1.31/1.48  1007[7:Rew:981.0,617.0] ||  -> equal(op(e1,e4),e4)**.
% 1.31/1.48  1027[7:Rew:1007.0,104.0] || equal(op(e1,e2),e4)** -> .
% 1.31/1.48  1057[7:MRR:939.0,997.0] ||  -> equal(op(e3,e2),e4)** equal(op(e1,e2),e4).
% 1.31/1.48  1077[7:MRR:1057.1,1027.0] ||  -> equal(op(e3,e2),e4)**.
% 1.31/1.48  1102[7:Rew:1077.0,909.0] ||  -> equal(op(e4,e4),e2)**.
% 1.31/1.48  1117[7:Rew:994.0,1102.0] ||  -> equal(e2,e0)**.
% 1.31/1.48  1118[7:MRR:1117.0,2.0] ||  -> .
% 1.31/1.48  1181[7:Spt:1118.0,335.0,981.0] || equal(op(e4,e0),e4)** -> .
% 1.31/1.48  1182[7:Spt:1118.0,335.1,335.2,335.3,335.4] ||  -> equal(op(e4,e0),e0) equal(op(e4,e0),e3)** equal(op(e4,e0),e2) equal(op(e4,e0),e1).
% 1.31/1.48  1183[7:MRR:941.0,1181.0] ||  -> equal(op(e3,e0),e4)** equal(op(e1,e0),e4).
% 1.31/1.48  1184[7:MRR:943.2,1181.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e2),e4).
% 1.31/1.48  1185[8:Spt:1182.0] ||  -> equal(op(e4,e0),e0)**.
% 1.31/1.48  1188[8:Rew:1185.0,617.0] ||  -> equal(op(e1,e0),e4)**.
% 1.31/1.48  1203[8:Rew:1185.0,953.3] ||  -> equal(op(e4,e3),e3)** equal(op(e4,e2),e3) equal(op(e4,e1),e3) equal(e3,e0).
% 1.31/1.48  1214[8:Rew:1188.0,16.0] ||  -> equal(op(e1,e4),e0)**.
% 1.31/1.48  1233[8:Rew:1188.0,590.0] ||  -> equal(op(e4,e4),e0)**.
% 1.31/1.48  1244[8:Rew:1214.0,145.0] ||  -> equal(op(op(e4,e1),e0),e1)**.
% 1.31/1.48  1261[8:Rew:1233.0,1184.0] ||  -> equal(e4,e0) equal(op(e4,e2),e4)**.
% 1.31/1.48  1289[8:MRR:1261.0,4.0] ||  -> equal(op(e4,e2),e4)**.
% 1.31/1.48  1303[8:Rew:1289.0,932.0] ||  -> equal(op(e4,e3),e2)**.
% 1.31/1.48  1305[8:Rew:1289.0,65.0] || equal(op(e3,e2),e4)** -> .
% 1.31/1.48  1331[8:Rew:1303.0,75.0] || equal(op(e3,e3),e2)** -> .
% 1.31/1.48  1339[8:MRR:338.2,1305.0] ||  -> equal(op(e3,e2),e3)** equal(op(e3,e2),e2) equal(op(e3,e2),e1) equal(op(e3,e2),e0).
% 1.31/1.48  1342[8:MRR:946.1,1331.0] ||  -> equal(op(e3,e3),e3)** equal(op(e3,e3),e1) equal(op(e3,e3),e0).
% 1.31/1.48  1358[8:Rew:1289.0,1203.1,1303.0,1203.0] ||  -> equal(e3,e2) equal(e4,e3) equal(op(e4,e1),e3)** equal(e3,e0).
% 1.31/1.48  1359[8:MRR:1358.0,1358.1,1358.3,8.0,10.0,3.0] ||  -> equal(op(e4,e1),e3)**.
% 1.31/1.48  1369[8:Rew:1359.0,1244.0] ||  -> equal(op(e3,e0),e1)**.
% 1.31/1.48  1378[8:Rew:1369.0,26.0] ||  -> equal(op(e3,e1),e0)**.
% 1.31/1.48  1384[8:Rew:1369.0,118.0] || equal(op(e3,e3),e1)** -> .
% 1.31/1.48  1385[8:Rew:1369.0,117.0] || equal(op(e3,e2),e1)** -> .
% 1.31/1.48  1397[8:Rew:1378.0,121.0] || equal(op(e3,e3),e0)** -> .
% 1.31/1.48  1398[8:Rew:1378.0,120.0] || equal(op(e3,e2),e0)** -> .
% 1.31/1.48  1445[8:MRR:1342.1,1384.0] ||  -> equal(op(e3,e3),e3)** equal(op(e3,e3),e0).
% 1.31/1.48  1515[8:MRR:1445.1,1397.0] ||  -> equal(op(e3,e3),e3)**.
% 1.31/1.48  1519[8:Rew:1515.0,123.0] || equal(op(e3,e2),e3)** -> .
% 1.31/1.48  1543[8:MRR:1339.0,1339.2,1339.3,1519.0,1385.0,1398.0] ||  -> equal(op(e3,e2),e2)**.
% 1.31/1.48  1545[8:Rew:1543.0,908.0] ||  -> equal(op(e4,e2),e3)**.
% 1.31/1.48  1553[8:Rew:1289.0,1545.0] ||  -> equal(e4,e3)**.
% 1.31/1.48  1554[8:MRR:1553.0,10.0] ||  -> .
% 1.31/1.48  1601[8:Spt:1554.0,1182.0,1185.0] || equal(op(e4,e0),e0)** -> .
% 1.31/1.48  1602[8:Spt:1554.0,1182.1,1182.2,1182.3] ||  -> equal(op(e4,e0),e3)** equal(op(e4,e0),e2) equal(op(e4,e0),e1).
% 1.31/1.48  1605[9:Spt:1602.0] ||  -> equal(op(e4,e0),e3)**.
% 1.31/1.48  1608[9:Rew:1605.0,31.0] ||  -> equal(op(e4,e3),e0)**.
% 1.31/1.48  1610[9:Rew:1605.0,618.0] ||  -> equal(op(e3,e1),e0)**.
% 1.31/1.48  1613[9:Rew:1605.0,127.0] || equal(op(e4,e2),e3)** -> .
% 1.31/1.48  1620[9:Rew:1605.0,655.0] || equal(op(e0,e3),e2) equal(op(e4,e0),e3)** -> .
% 1.31/1.48  1633[9:Rew:1608.0,135.0] || equal(op(e4,e4),e0)** -> .
% 1.31/1.48  1634[9:Rew:1608.0,133.0] || equal(op(e4,e2),e0)** -> .
% 1.31/1.48  1637[9:Rew:1608.0,69.0] || equal(op(e0,e3),e0)** -> .
% 1.31/1.48  1643[9:Rew:1608.0,960.2] ||  -> equal(op(e3,e3),e1)** equal(op(e1,e3),e1) equal(e1,e0).
% 1.31/1.48  1652[9:Rew:1610.0,27.0] ||  -> equal(op(e3,e0),e1)**.
% 1.31/1.48  1676[9:Rew:1652.0,118.0] || equal(op(e3,e3),e1)** -> .
% 1.31/1.48  1684[9:Rew:1652.0,1183.0] ||  -> equal(e4,e1) equal(op(e1,e0),e4)**.
% 1.31/1.48  1691[9:MRR:958.1,1613.0] ||  -> equal(op(e3,e2),e3)** equal(op(e1,e2),e3) equal(op(e0,e2),e3).
% 1.31/1.48  1692[9:MRR:333.2,1613.0] ||  -> equal(op(e4,e2),e4)** equal(op(e4,e2),e2) equal(op(e4,e2),e1) equal(op(e4,e2),e0).
% 1.31/1.48  1700[9:MRR:952.2,1633.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e4),e2).
% 1.31/1.48  1704[9:MRR:649.1,1637.0] ||  -> equal(op(e0,e3),e3)** equal(op(e0,e3),e2).
% 1.31/1.48  1717[9:MRR:1684.0,7.0] ||  -> equal(op(e1,e0),e4)**.
% 1.31/1.48  1720[9:Rew:1717.0,16.0] ||  -> equal(op(e1,e4),e0)**.
% 1.31/1.48  1723[9:Rew:1717.0,97.0] || equal(op(e1,e2),e4)** -> .
% 1.31/1.48  1741[9:Rew:1720.0,104.0] || equal(op(e1,e2),e0)** -> .
% 1.31/1.48  1755[9:MRR:348.2,1723.0] ||  -> equal(op(e1,e2),e2) equal(op(e1,e2),e1) equal(op(e1,e2),e3)** equal(op(e1,e2),e0).
% 1.31/1.48  1757[9:Rew:1605.0,1620.1] || equal(op(e0,e3),e2)** equal(e3,e3) -> .
% 1.31/1.48  1758[9:Obv:1757.1] || equal(op(e0,e3),e2)** -> .
% 1.31/1.48  1760[9:MRR:1704.1,1758.0] ||  -> equal(op(e0,e3),e3)**.
% 1.31/1.48  1765[9:Rew:1760.0,93.0] || equal(op(e0,e2),e3)** -> .
% 1.31/1.48  1777[9:MRR:1643.0,1643.2,1676.0,1.0] ||  -> equal(op(e1,e3),e1)**.
% 1.31/1.48  1779[9:Rew:1777.0,19.0] ||  -> equal(op(e1,e1),e3)**.
% 1.31/1.48  1782[9:Rew:1777.0,103.0] || equal(op(e1,e2),e1)** -> .
% 1.31/1.48  1792[9:Rew:1779.0,100.0] || equal(op(e1,e2),e3)** -> .
% 1.31/1.48  1805[9:MRR:1691.1,1691.2,1792.0,1765.0] ||  -> equal(op(e3,e2),e3)**.
% 1.31/1.48  1808[9:Rew:1805.0,909.0] ||  -> equal(op(e3,e4),e2)**.
% 1.31/1.48  1834[9:Rew:1808.0,85.0] || equal(op(e4,e4),e2)** -> .
% 1.31/1.48  1850[9:MRR:1700.1,1834.0] ||  -> equal(op(e4,e4),e4)**.
% 1.31/1.48  1854[9:Rew:1850.0,134.0] || equal(op(e4,e2),e4)** -> .
% 1.31/1.48  1872[9:MRR:1692.0,1692.3,1854.0,1634.0] ||  -> equal(op(e4,e2),e2)** equal(op(e4,e2),e1).
% 1.31/1.48  1875[9:MRR:1755.1,1755.2,1755.3,1782.0,1792.0,1741.0] ||  -> equal(op(e1,e2),e2)**.
% 1.31/1.48  1877[9:Rew:1875.0,62.0] || equal(op(e4,e2),e2)** -> .
% 1.31/1.48  1886[9:MRR:1872.0,1877.0] ||  -> equal(op(e4,e2),e1)**.
% 1.31/1.48  1889[9:Rew:1886.0,33.0] ||  -> equal(op(e4,e1),e2)**.
% 1.31/1.48  1907[9:Rew:1889.0,201.0] || equal(e2,e2) equal(op(e4,op(op(e4,e1),e4)),e0)** equal(op(op(e4,e1),e4),e3) -> .
% 1.31/1.48  2025[9:Obv:1907.0] || equal(op(e4,op(op(e4,e1),e4)),e0)** equal(op(op(e4,e1),e4),e3) -> .
% 1.31/1.48  2026[9:Rew:899.0,2025.1,1889.0,2025.1,1608.0,2025.0,899.0,2025.0,1889.0,2025.0] || equal(e0,e0) equal(e3,e3)* -> .
% 1.31/1.48  2027[9:Obv:2026.1] ||  -> .
% 1.31/1.48  2031[9:Spt:2027.0,1602.0,1605.0] || equal(op(e4,e0),e3)** -> .
% 1.31/1.48  2032[9:Spt:2027.0,1602.1,1602.2] ||  -> equal(op(e4,e0),e2)** equal(op(e4,e0),e1).
% 1.31/1.48  2034[9:MRR:951.2,2031.0] ||  -> equal(op(e3,e0),e3)** equal(op(e0,e0),e3) equal(op(e1,e0),e3).
% 1.31/1.48  2035[10:Spt:2032.0] ||  -> equal(op(e4,e0),e2)**.
% 1.31/1.48  2039[10:Rew:2035.0,618.0] ||  -> equal(op(e2,e1),e0)**.
% 1.31/1.48  2040[10:Rew:2035.0,617.0] ||  -> equal(op(e1,e2),e4)**.
% 1.31/1.48  2041[10:Rew:2035.0,31.0] ||  -> equal(op(e4,e2),e0)**.
% 1.31/1.48  2059[10:Rew:2039.0,22.0] ||  -> equal(op(e2,e0),e1)**.
% 1.31/1.48  2098[10:Rew:2041.0,932.0] ||  -> equal(op(e0,e3),e2)**.
% 1.31/1.48  2122[10:Rew:2059.0,146.0] ||  -> equal(op(op(e0,e2),e1),e2)**.
% 1.31/1.48  2123[10:Rew:2059.0,138.0] ||  -> equal(op(e1,op(e0,e2)),e0)**.
% 1.31/1.48  2165[10:Rew:2098.0,14.0] ||  -> equal(op(e0,e2),e3)**.
% 1.31/1.48  2223[10:Rew:2165.0,2122.0] ||  -> equal(op(e3,e1),e2)**.
% 1.31/1.48  2268[10:Rew:2165.0,2123.0] ||  -> equal(op(e1,e3),e0)**.
% 1.31/1.48  2270[10:Rew:2268.0,19.0] ||  -> equal(op(e1,e0),e3)**.
% 1.31/1.48  2284[10:Rew:2270.0,228.0] || equal(e3,e3) equal(op(e1,op(op(e1,e0),e1)),e4)** equal(op(op(e1,e0),e1),e2) -> .
% 1.31/1.48  2448[10:Obv:2284.0] || equal(op(e1,op(op(e1,e0),e1)),e4)** equal(op(op(e1,e0),e1),e2) -> .
% 1.31/1.48  2449[10:Rew:2223.0,2448.1,2270.0,2448.1,2040.0,2448.0,2223.0,2448.0,2270.0,2448.0] || equal(e4,e4)* equal(e2,e2) -> .
% 1.31/1.48  2450[10:Obv:2449.1] ||  -> .
% 1.31/1.48  2454[10:Spt:2450.0,2032.0,2035.0] || equal(op(e4,e0),e2)** -> .
% 1.31/1.48  2455[10:Spt:2450.0,2032.1] ||  -> equal(op(e4,e0),e1)**.
% 1.31/1.48  2460[10:Rew:2455.0,31.0] ||  -> equal(op(e4,e1),e0)**.
% 1.31/1.48  2464[10:Rew:2455.0,618.0] ||  -> equal(op(e1,e1),e0)**.
% 1.31/1.48  2467[10:Rew:2464.0,17.0] ||  -> equal(op(e1,e0),e1)**.
% 1.31/1.48  2468[10:Rew:2467.0,590.0] ||  -> equal(op(e1,e4),e0)**.
% 1.31/1.48  2494[10:Rew:2468.0,105.0] || equal(op(e1,e3),e0)** -> .
% 1.31/1.48  2508[10:Rew:2467.0,98.0] || equal(op(e1,e3),e1)** -> .
% 1.31/1.48  2517[10:Rew:2467.0,1183.1] ||  -> equal(op(e3,e0),e4)** equal(e4,e1).
% 1.31/1.48  2518[10:MRR:2517.1,7.0] ||  -> equal(op(e3,e0),e4)**.
% 1.31/1.48  2536[10:Rew:2467.0,947.2,2468.0,947.0] ||  -> equal(e4,e0) equal(op(e1,e2),e4)** equal(e4,e1).
% 1.31/1.48  2537[10:MRR:2536.0,2536.2,4.0,7.0] ||  -> equal(op(e1,e2),e4)**.
% 1.31/1.48  2575[10:Rew:2467.0,2034.2,2518.0,2034.0] ||  -> equal(e4,e3) equal(op(e0,e0),e3)** equal(e3,e1).
% 1.31/1.48  2576[10:MRR:2575.0,2575.2,10.0,6.0] ||  -> equal(op(e0,e0),e3)**.
% 1.31/1.48  2579[10:Rew:2576.0,11.0] ||  -> equal(op(e0,e3),e0)**.
% 1.31/1.48  2583[10:Rew:2576.0,136.0] ||  -> equal(op(e3,e3),e0)**.
% 1.31/1.48  2610[10:Rew:2579.0,669.2,2576.0,669.1] ||  -> equal(op(e0,e2),e2)** equal(e3,e2) equal(e2,e0).
% 1.31/1.48  2611[10:MRR:2610.1,2610.2,8.0,2.0] ||  -> equal(op(e0,e2),e2)**.
% 1.31/1.48  2626[10:Rew:2460.0,949.2,2464.0,949.1] ||  -> equal(op(e3,e1),e3)** equal(e3,e0) equal(e3,e0).
% 1.31/1.48  2627[10:Obv:2626.1] ||  -> equal(op(e3,e1),e3)** equal(e3,e0).
% 1.31/1.48  2628[10:MRR:2627.1,3.0] ||  -> equal(op(e3,e1),e3)**.
% 1.31/1.48  2641[10:MRR:948.1,948.3,2508.0,2494.0] ||  -> equal(op(e1,e3),e3)** equal(op(e1,e3),e2).
% 1.31/1.48  2649[10:Rew:2518.0,642.3,2628.0,642.1,2583.0,642.0] ||  -> equal(e1,e0) equal(e3,e1) equal(op(e3,e2),e1)** equal(e4,e1).
% 1.31/1.48  2650[10:MRR:2649.0,2649.1,2649.3,1.0,6.0,7.0] ||  -> equal(op(e3,e2),e1)**.
% 1.31/1.48  2704[10:Rew:2611.0,958.3,2537.0,958.2,2650.0,958.0] ||  -> equal(e3,e1) equal(op(e4,e2),e3)** equal(e4,e3) equal(e3,e2).
% 1.31/1.48  2705[10:MRR:2704.0,2704.2,2704.3,6.0,10.0,8.0] ||  -> equal(op(e4,e2),e3)**.
% 1.31/1.48  2708[10:Rew:2705.0,33.0] ||  -> equal(op(e4,e3),e2)**.
% 1.31/1.48  2722[10:Rew:2708.0,72.0] || equal(op(e1,e3),e2)** -> .
% 1.31/1.48  2731[10:MRR:2641.1,2722.0] ||  -> equal(op(e1,e3),e3)**.
% 1.31/1.48  2856[10:Rew:2467.0,316.4,2731.0,316.3,2468.0,316.2,2464.0,316.1,2537.0,316.0] ||  -> equal(e4,e2)** equal(e2,e0) equal(e2,e0) equal(e3,e2) equal(e2,e1).
% 1.31/1.48  2857[10:Obv:2856.1] ||  -> equal(e4,e2)** equal(e2,e0) equal(e3,e2) equal(e2,e1).
% 1.31/1.48  2858[10:MRR:2857.0,2857.1,2857.2,2857.3,9.0,2.0,8.0,5.0] ||  -> .
% 1.31/1.48  2859[6:Spt:2858.0,893.0,896.0] || equal(op(e2,e3),e4)** -> .
% 1.31/1.48  2860[6:Spt:2858.0,893.1,893.2] ||  -> equal(op(e2,e3),e1)** equal(op(e2,e3),e0).
% 1.31/1.48  2861[6:MRR:633.2,2859.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4) equal(op(e2,e0),e4).
% 1.31/1.48  2862[6:MRR:623.2,2859.0] ||  -> equal(op(e4,e3),e4)** equal(op(e3,e3),e4) equal(op(e1,e3),e4).
% 1.31/1.48  2863[7:Spt:2860.0] ||  -> equal(op(e2,e3),e1)**.
% 1.31/1.48  2867[7:Rew:2863.0,24.0] ||  -> equal(op(e2,e1),e3)**.
% 1.31/1.48  2869[7:Rew:2863.0,70.0] || equal(op(e1,e3),e1)** -> .
% 1.31/1.48  2871[7:Rew:2863.0,74.0] || equal(op(e4,e3),e1)** -> .
% 1.31/1.48  2874[7:Rew:2863.0,113.0] || equal(op(e2,e2),e1)** -> .
% 1.31/1.48  2879[7:Rew:2863.0,165.0] || equal(e1,e1) equal(op(e2,op(op(e2,e3),e2)),e0)** equal(op(op(e2,e3),e2),e4) -> .
% 1.31/1.48  2881[7:Rew:2863.0,310.3] ||  -> equal(op(e2,e2),e0) equal(op(e2,e0),e0) equal(op(e2,e4),e0)** equal(e1,e0) equal(op(e2,e1),e0).
% 1.31/1.48  2886[7:Rew:2867.0,54.0] || equal(op(e4,e1),e3)** -> .
% 1.31/1.48  2889[7:Rew:2867.0,110.0] || equal(op(e2,e2),e3)** -> .
% 1.31/1.48  2891[7:Rew:2867.0,112.0] || equal(op(e2,e4),e3)** -> .
% 1.31/1.48  2892[7:Rew:2867.0,147.0] ||  -> equal(op(op(e1,e2),e3),e2)**.
% 1.31/1.48  2898[7:Rew:2867.0,426.3] ||  -> equal(op(e1,e1),e1) equal(op(e4,e1),e1)** equal(op(e3,e1),e1) equal(e3,e1).
% 1.31/1.48  2902[7:MRR:646.1,2869.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e2),e1)** equal(op(e1,e0),e1).
% 1.31/1.48  2906[7:MRR:640.1,2871.0] ||  -> equal(op(e4,e1),e1) equal(op(e4,e2),e1)** equal(op(e4,e0),e1).
% 1.31/1.48  2907[7:MRR:332.3,2871.0] ||  -> equal(op(e4,e3),e4)** equal(op(e4,e3),e3) equal(op(e4,e3),e2) equal(op(e4,e3),e0).
% 1.31/1.48  2911[7:MRR:638.0,2874.0] ||  -> equal(op(e1,e2),e1) equal(op(e4,e2),e1)** equal(op(e3,e2),e1).
% 1.31/1.48  2912[7:MRR:343.3,2874.0] ||  -> equal(op(e2,e2),e2) equal(op(e2,e2),e4)** equal(op(e2,e2),e3) equal(op(e2,e2),e0).
% 1.32/1.48  2914[7:MRR:284.3,2886.0] ||  -> equal(op(e4,e4),e3)** equal(op(e4,e3),e3) equal(op(e4,e2),e3) equal(op(e4,e0),e3).
% 1.32/1.48  2919[7:MRR:303.1,2889.0] ||  -> equal(op(e3,e2),e3) equal(op(e4,e2),e3)** equal(op(e1,e2),e3) equal(op(e0,e2),e3).
% 1.32/1.48  2921[7:MRR:643.2,2891.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e4),e2) equal(op(e2,e4),e0).
% 1.32/1.48  2922[7:MRR:671.2,2891.0] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3) equal(op(e1,e4),e3).
% 1.32/1.48  2925[7:MRR:2898.3,6.0] ||  -> equal(op(e1,e1),e1) equal(op(e4,e1),e1)** equal(op(e3,e1),e1).
% 1.32/1.48  2928[7:MRR:2912.2,2889.0] ||  -> equal(op(e2,e2),e2) equal(op(e2,e2),e4)** equal(op(e2,e2),e0).
% 1.32/1.48  2931[7:Obv:2879.0] || equal(op(e2,op(op(e2,e3),e2)),e0)** equal(op(op(e2,e3),e2),e4) -> .
% 1.32/1.48  2932[7:Rew:2863.0,2931.1,2863.0,2931.0] || equal(op(e2,op(e1,e2)),e0)** equal(op(e1,e2),e4) -> .
% 1.32/1.48  2938[7:Rew:2867.0,2881.4] ||  -> equal(op(e2,e2),e0) equal(op(e2,e0),e0) equal(op(e2,e4),e0)** equal(e1,e0) equal(e3,e0).
% 1.32/1.48  2939[7:MRR:2938.3,2938.4,1.0,3.0] ||  -> equal(op(e2,e2),e0) equal(op(e2,e0),e0) equal(op(e2,e4),e0)**.
% 1.32/1.48  2941[8:Spt:335.0] ||  -> equal(op(e4,e0),e4)**.
% 1.32/1.48  2942[8:Rew:2941.0,31.0] ||  -> equal(op(e4,e4),e0)**.
% 1.32/1.48  2943[8:Rew:2941.0,617.0] ||  -> equal(op(e1,e4),e4)**.
% 1.32/1.48  2944[8:Rew:2941.0,618.0] ||  -> equal(op(e4,e1),e0)**.
% 1.32/1.48  2946[8:Rew:2941.0,128.0] || equal(op(e4,e3),e4)** -> .
% 1.32/1.48  2950[8:Rew:2941.0,44.0] || equal(op(e2,e0),e4)** -> .
% 1.32/1.48  2956[8:Rew:2941.0,286.4] ||  -> equal(op(e4,e4),e2)** equal(op(e4,e2),e2) equal(op(e4,e3),e2) equal(op(e4,e1),e2) equal(e4,e2).
% 1.32/1.48  2964[8:Rew:2941.0,2906.2] ||  -> equal(op(e4,e1),e1) equal(op(e4,e2),e1)** equal(e4,e1).
% 1.32/1.48  2973[8:Rew:2942.0,135.0] || equal(op(e4,e3),e0)** -> .
% 1.32/1.48  2984[8:Rew:2943.0,105.0] || equal(op(e1,e3),e4)** -> .
% 1.32/1.48  2988[8:Rew:2943.0,80.0] || equal(op(e2,e4),e4)** -> .
% 1.32/1.48  3017[8:MRR:2862.0,2946.0] ||  -> equal(op(e3,e3),e4)** equal(op(e1,e3),e4).
% 1.32/1.48  3018[8:MRR:2907.0,2946.0] ||  -> equal(op(e4,e3),e3)** equal(op(e4,e3),e2) equal(op(e4,e3),e0).
% 1.32/1.48  3024[8:MRR:2861.2,2950.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4).
% 1.32/1.48  3042[8:MRR:3017.1,2984.0] ||  -> equal(op(e3,e3),e4)**.
% 1.32/1.48  3043[8:Rew:3042.0,29.0] ||  -> equal(op(e3,e4),e3)**.
% 1.32/1.48  3061[8:Rew:3043.0,124.0] || equal(op(e3,e2),e3)** -> .
% 1.32/1.48  3073[8:MRR:2919.0,3061.0] ||  -> equal(op(e4,e2),e3)** equal(op(e1,e2),e3) equal(op(e0,e2),e3).
% 1.32/1.48  3074[8:MRR:3024.0,2988.0] ||  -> equal(op(e2,e2),e4)**.
% 1.32/1.48  3075[8:Rew:3074.0,23.0] ||  -> equal(op(e2,e4),e2)**.
% 1.32/1.48  3090[8:Rew:3075.0,150.0] ||  -> equal(op(op(e4,e2),e2),e2)**.
% 1.32/1.48  3118[8:Rew:2944.0,2964.0] ||  -> equal(e1,e0) equal(op(e4,e2),e1)** equal(e4,e1).
% 1.32/1.48  3119[8:MRR:3118.0,3118.2,1.0,7.0] ||  -> equal(op(e4,e2),e1)**.
% 1.32/1.48  3131[8:Rew:3119.0,3090.0] ||  -> equal(op(e1,e2),e2)**.
% 1.32/1.48  3225[8:MRR:3018.2,2973.0] ||  -> equal(op(e4,e3),e3)** equal(op(e4,e3),e2).
% 1.32/1.48  3229[8:Rew:3131.0,3073.1,3119.0,3073.0] ||  -> equal(e3,e1) equal(e3,e2) equal(op(e0,e2),e3)**.
% 1.32/1.48  3230[8:MRR:3229.0,3229.1,6.0,8.0] ||  -> equal(op(e0,e2),e3)**.
% 1.32/1.48  3233[8:Rew:3230.0,13.0] ||  -> equal(op(e0,e3),e2)**.
% 1.32/1.48  3243[8:Rew:3233.0,69.0] || equal(op(e4,e3),e2)** -> .
% 1.32/1.48  3266[8:MRR:3225.1,3243.0] ||  -> equal(op(e4,e3),e3)**.
% 1.32/1.48  3343[8:Rew:2944.0,2956.3,3266.0,2956.2,3119.0,2956.1,2942.0,2956.0] ||  -> equal(e2,e0) equal(e2,e1) equal(e3,e2) equal(e2,e0) equal(e4,e2)**.
% 1.32/1.48  3344[8:Obv:3343.0] ||  -> equal(e2,e1) equal(e3,e2) equal(e2,e0) equal(e4,e2)**.
% 1.32/1.48  3345[8:MRR:3344.0,3344.1,3344.2,3344.3,5.0,8.0,2.0,9.0] ||  -> .
% 1.32/1.48  3346[8:Spt:3345.0,335.0,2941.0] || equal(op(e4,e0),e4)** -> .
% 1.32/1.48  3347[8:Spt:3345.0,335.1,335.2,335.3,335.4] ||  -> equal(op(e4,e0),e0) equal(op(e4,e0),e3)** equal(op(e4,e0),e2) equal(op(e4,e0),e1).
% 1.32/1.48  3348[8:MRR:627.0,3346.0] ||  -> equal(op(e3,e0),e4)** equal(op(e2,e0),e4) equal(op(e1,e0),e4).
% 1.32/1.48  3349[8:MRR:629.3,3346.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e3),e4) equal(op(e4,e2),e4).
% 1.32/1.48  3350[9:Spt:3347.0] ||  -> equal(op(e4,e0),e0)**.
% 1.32/1.48  3353[9:Rew:3350.0,617.0] ||  -> equal(op(e1,e0),e4)**.
% 1.32/1.48  3369[9:Rew:3350.0,286.4] ||  -> equal(op(e4,e4),e2)** equal(op(e4,e2),e2) equal(op(e4,e3),e2) equal(op(e4,e1),e2) equal(e2,e0).
% 1.32/1.48  3376[9:Rew:3350.0,2906.2] ||  -> equal(op(e4,e1),e1) equal(op(e4,e2),e1)** equal(e1,e0).
% 1.32/1.48  3379[9:Rew:3353.0,590.0] ||  -> equal(op(e4,e4),e0)**.
% 1.32/1.48  3381[9:Rew:3353.0,16.0] ||  -> equal(op(e1,e4),e0)**.
% 1.32/1.48  3397[9:Rew:3353.0,2902.2] ||  -> equal(op(e1,e1),e1) equal(op(e1,e2),e1)** equal(e4,e1).
% 1.32/1.48  3410[9:Rew:3379.0,2922.0] ||  -> equal(e3,e0) equal(op(e3,e4),e3)** equal(op(e1,e4),e3).
% 1.32/1.48  3411[9:Rew:3379.0,3349.0] ||  -> equal(e4,e0) equal(op(e4,e3),e4)** equal(op(e4,e2),e4).
% 1.32/1.48  3585[9:MRR:3376.2,1.0] ||  -> equal(op(e4,e1),e1) equal(op(e4,e2),e1)**.
% 1.32/1.48  3586[9:MRR:3397.2,7.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e2),e1)**.
% 1.32/1.48  3587[9:Rew:3381.0,3410.2] ||  -> equal(e3,e0) equal(op(e3,e4),e3)** equal(e3,e0).
% 1.32/1.48  3588[9:Obv:3587.0] ||  -> equal(op(e3,e4),e3)** equal(e3,e0).
% 1.32/1.48  3589[9:MRR:3588.1,3.0] ||  -> equal(op(e3,e4),e3)**.
% 1.32/1.48  3591[9:Rew:3589.0,30.0] ||  -> equal(op(e3,e3),e4)**.
% 1.32/1.48  3603[9:Rew:3591.0,75.0] || equal(op(e4,e3),e4)** -> .
% 1.32/1.48  3611[9:MRR:3411.0,3411.1,4.0,3603.0] ||  -> equal(op(e4,e2),e4)**.
% 1.32/1.48  3619[9:Rew:3611.0,3585.1] ||  -> equal(op(e4,e1),e1)** equal(e4,e1).
% 1.32/1.48  3625[9:MRR:3619.1,7.0] ||  -> equal(op(e4,e1),e1)**.
% 1.32/1.48  3630[9:Rew:3625.0,52.0] || equal(op(e1,e1),e1)** -> .
% 1.32/1.48  3639[9:MRR:3586.0,3630.0] ||  -> equal(op(e1,e2),e1)**.
% 1.32/1.48  3649[9:Rew:3639.0,2892.0] ||  -> equal(op(e1,e3),e2)**.
% 1.32/1.48  3663[9:Rew:3649.0,72.0] || equal(op(e4,e3),e2)** -> .
% 1.32/1.48  3741[9:Rew:3625.0,3369.3,3611.0,3369.1,3379.0,3369.0] ||  -> equal(e2,e0) equal(e4,e2) equal(op(e4,e3),e2)** equal(e2,e1) equal(e2,e0).
% 1.32/1.48  3742[9:Obv:3741.0] ||  -> equal(e4,e2) equal(op(e4,e3),e2)** equal(e2,e1) equal(e2,e0).
% 1.32/1.48  3743[9:MRR:3742.0,3742.1,3742.2,3742.3,9.0,3663.0,5.0,2.0] ||  -> .
% 1.32/1.48  3744[9:Spt:3743.0,3347.0,3350.0] || equal(op(e4,e0),e0)** -> .
% 1.32/1.48  3745[9:Spt:3743.0,3347.1,3347.2,3347.3] ||  -> equal(op(e4,e0),e3)** equal(op(e4,e0),e2) equal(op(e4,e0),e1).
% 1.32/1.48  3746[9:MRR:329.1,3744.0] ||  -> equal(op(e0,e0),e0) equal(op(e3,e0),e0)** equal(op(e2,e0),e0) equal(op(e1,e0),e0).
% 1.32/1.48  3748[10:Spt:3745.0] ||  -> equal(op(e4,e0),e3)**.
% 1.32/1.48  3752[10:Rew:3748.0,617.0] ||  -> equal(op(e1,e3),e4)**.
% 1.32/1.48  3753[10:Rew:3748.0,618.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  3763[10:Rew:3748.0,655.0] || equal(op(e0,e3),e2) equal(op(e4,e0),e3)** -> .
% 1.32/1.48  3794[10:Rew:3752.0,98.0] || equal(op(e1,e0),e4)** -> .
% 1.32/1.48  3813[10:Rew:3753.0,27.0] ||  -> equal(op(e3,e0),e1)**.
% 1.32/1.48  3861[10:Rew:3813.0,3348.0] ||  -> equal(e4,e1) equal(op(e2,e0),e4)** equal(op(e1,e0),e4).
% 1.32/1.48  3865[10:Rew:3813.0,3746.1] ||  -> equal(op(e0,e0),e0) equal(e1,e0) equal(op(e2,e0),e0)** equal(op(e1,e0),e0).
% 1.32/1.48  3892[10:Rew:3748.0,3763.1] || equal(op(e0,e3),e2)** equal(e3,e3) -> .
% 1.32/1.48  3893[10:Obv:3892.1] || equal(op(e0,e3),e2)** -> .
% 1.32/1.48  3894[10:MRR:669.2,3893.0] ||  -> equal(op(e0,e2),e2)** equal(op(e0,e0),e2).
% 1.32/1.48  3915[10:MRR:3861.0,3861.2,7.0,3794.0] ||  -> equal(op(e2,e0),e4)**.
% 1.32/1.48  3918[10:Rew:3915.0,21.0] ||  -> equal(op(e2,e4),e0)**.
% 1.32/1.48  3922[10:Rew:3915.0,107.0] || equal(op(e2,e2),e4)** -> .
% 1.32/1.48  3933[10:Rew:3918.0,114.0] || equal(op(e2,e2),e0)** -> .
% 1.32/1.48  3940[10:MRR:2928.1,3922.0] ||  -> equal(op(e2,e2),e2)** equal(op(e2,e2),e0).
% 1.32/1.48  3941[10:MRR:3940.1,3933.0] ||  -> equal(op(e2,e2),e2)**.
% 1.32/1.48  3946[10:Rew:3941.0,57.0] || equal(op(e0,e2),e2)** -> .
% 1.32/1.48  3952[10:MRR:3894.0,3946.0] ||  -> equal(op(e0,e0),e2)**.
% 1.32/1.48  4089[10:Rew:3915.0,3865.2,3952.0,3865.0] ||  -> equal(e2,e0) equal(e1,e0) equal(e4,e0) equal(op(e1,e0),e0)**.
% 1.32/1.48  4090[10:MRR:4089.0,4089.1,4089.2,2.0,1.0,4.0] ||  -> equal(op(e1,e0),e0)**.
% 1.32/1.48  4093[10:Rew:4090.0,590.0] ||  -> equal(op(e0,e4),e0)**.
% 1.32/1.48  4100[10:Rew:580.0,4093.0] ||  -> equal(e1,e0)**.
% 1.32/1.48  4101[10:MRR:4100.0,1.0] ||  -> .
% 1.32/1.48  4147[10:Spt:4101.0,3745.0,3748.0] || equal(op(e4,e0),e3)** -> .
% 1.32/1.48  4148[10:Spt:4101.0,3745.1,3745.2] ||  -> equal(op(e4,e0),e2)** equal(op(e4,e0),e1).
% 1.32/1.48  4150[10:MRR:2914.3,4147.0] ||  -> equal(op(e4,e4),e3)** equal(op(e4,e3),e3) equal(op(e4,e2),e3).
% 1.32/1.48  4151[11:Spt:4148.0] ||  -> equal(op(e4,e0),e2)**.
% 1.32/1.48  4156[11:Rew:4151.0,617.0] ||  -> equal(op(e1,e2),e4)**.
% 1.32/1.48  4157[11:Rew:4151.0,31.0] ||  -> equal(op(e4,e2),e0)**.
% 1.32/1.48  4159[11:Rew:4151.0,39.0] || equal(op(e0,e0),e2)** -> .
% 1.32/1.48  4176[11:Rew:4156.0,2892.0] ||  -> equal(op(e4,e3),e2)**.
% 1.32/1.48  4177[11:Rew:4156.0,18.0] ||  -> equal(op(e1,e4),e2)**.
% 1.32/1.48  4186[11:Rew:4156.0,2932.0] || equal(op(e2,e4),e0)** equal(op(e1,e2),e4) -> .
% 1.32/1.48  4204[11:Rew:4157.0,64.0] || equal(op(e2,e2),e0)** -> .
% 1.32/1.48  4216[11:Rew:4157.0,4150.2] ||  -> equal(op(e4,e4),e3)** equal(op(e4,e3),e3) equal(e3,e0).
% 1.32/1.48  4239[11:Rew:4177.0,80.0] || equal(op(e2,e4),e2)** -> .
% 1.32/1.48  4254[11:Rew:4177.0,673.3] ||  -> equal(op(e4,e4),e0)** equal(op(e3,e4),e0) equal(op(e2,e4),e0) equal(e2,e0).
% 1.32/1.48  4258[11:MRR:651.2,4159.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e3)**.
% 1.32/1.48  4279[11:MRR:2939.0,4204.0] ||  -> equal(op(e2,e0),e0) equal(op(e2,e4),e0)**.
% 1.32/1.48  4286[11:MRR:2921.1,4239.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e4),e0).
% 1.32/1.48  4387[11:Rew:4156.0,4186.1] || equal(op(e2,e4),e0)** equal(e4,e4) -> .
% 1.32/1.48  4388[11:Obv:4387.1] || equal(op(e2,e4),e0)** -> .
% 1.32/1.48  4389[11:MRR:4279.1,4388.0] ||  -> equal(op(e2,e0),e0)**.
% 1.32/1.48  4390[11:MRR:4286.1,4388.0] ||  -> equal(op(e2,e4),e4)**.
% 1.32/1.48  4397[11:Rew:4389.0,37.0] || equal(op(e0,e0),e0)** -> .
% 1.32/1.48  4419[11:MRR:4258.0,4397.0] ||  -> equal(op(e0,e0),e3)**.
% 1.32/1.48  4426[11:Rew:4419.0,136.0] ||  -> equal(op(e3,e3),e0)**.
% 1.32/1.48  4441[11:Rew:4426.0,125.0] || equal(op(e3,e4),e0)** -> .
% 1.32/1.48  4468[11:Rew:4176.0,4216.1] ||  -> equal(op(e4,e4),e3)** equal(e3,e2) equal(e3,e0).
% 1.32/1.48  4469[11:MRR:4468.1,4468.2,8.0,3.0] ||  -> equal(op(e4,e4),e3)**.
% 1.32/1.48  4498[11:Rew:4390.0,4254.2,4469.0,4254.0] ||  -> equal(e3,e0) equal(op(e3,e4),e0)** equal(e4,e0) equal(e2,e0).
% 1.32/1.48  4499[11:MRR:4498.0,4498.1,4498.2,4498.3,3.0,4441.0,4.0,2.0] ||  -> .
% 1.32/1.48  4539[11:Spt:4499.0,4148.0,4151.0] || equal(op(e4,e0),e2)** -> .
% 1.32/1.48  4540[11:Spt:4499.0,4148.1] ||  -> equal(op(e4,e0),e1)**.
% 1.32/1.48  4545[11:Rew:4540.0,31.0] ||  -> equal(op(e4,e1),e0)**.
% 1.32/1.48  4550[11:Rew:4540.0,618.0] ||  -> equal(op(e1,e1),e0)**.
% 1.32/1.48  4554[11:Rew:4550.0,17.0] ||  -> equal(op(e1,e0),e1)**.
% 1.32/1.48  4565[11:Rew:4540.0,127.0] || equal(op(e4,e2),e1)** -> .
% 1.32/1.48  4572[11:Rew:4554.0,97.0] || equal(op(e1,e2),e1)** -> .
% 1.32/1.48  4604[11:MRR:2911.0,2911.1,4572.0,4565.0] ||  -> equal(op(e3,e2),e1)**.
% 1.32/1.48  4605[11:Rew:4604.0,28.0] ||  -> equal(op(e3,e1),e2)**.
% 1.32/1.48  4640[11:Rew:4605.0,2925.2,4545.0,2925.1,4550.0,2925.0] ||  -> equal(e1,e0) equal(e1,e0) equal(e2,e1)**.
% 1.32/1.48  4641[11:Obv:4640.0] ||  -> equal(e1,e0) equal(e2,e1)**.
% 1.32/1.48  4642[11:MRR:4641.0,4641.1,1.0,5.0] ||  -> .
% 1.32/1.48  4733[7:Spt:4642.0,2860.0,2863.0] || equal(op(e2,e3),e1)** -> .
% 1.32/1.48  4734[7:Spt:4642.0,2860.1] ||  -> equal(op(e2,e3),e0)**.
% 1.32/1.48  4739[7:Rew:4734.0,24.0] ||  -> equal(op(e2,e0),e3)**.
% 1.32/1.48  4741[7:Rew:4739.0,37.0] || equal(op(e0,e0),e3)** -> .
% 1.32/1.48  4742[7:Rew:4739.0,109.0] || equal(op(e2,e4),e3)** -> .
% 1.32/1.48  4749[7:Rew:4739.0,2861.2] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4) equal(e4,e3).
% 1.32/1.48  4750[7:MRR:651.1,4741.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e2)**.
% 1.32/1.48  4751[7:MRR:666.1,4741.0] ||  -> equal(op(e0,e3),e3)** equal(op(e0,e2),e3).
% 1.32/1.48  4754[7:Rew:4734.0,115.0] || equal(op(e2,e4),e0)** -> .
% 1.32/1.48  4767[7:MRR:4749.2,10.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4).
% 1.32/1.48  4768[7:MRR:643.2,643.3,4742.0,4754.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e4),e2).
% 1.32/1.48  4770[7:Rew:4739.0,647.3] ||  -> equal(op(e1,e0),e1) equal(op(e4,e0),e1)** equal(op(e3,e0),e1) equal(e3,e1).
% 1.32/1.48  4771[7:MRR:4770.3,6.0] ||  -> equal(op(e1,e0),e1) equal(op(e4,e0),e1)** equal(op(e3,e0),e1).
% 1.32/1.48  4783[7:MRR:673.2,4754.0] ||  -> equal(op(e4,e4),e0)** equal(op(e3,e4),e0) equal(op(e1,e4),e0).
% 1.32/1.48  4816[8:Spt:348.0] ||  -> equal(op(e1,e2),e2)**.
% 1.32/1.48  4837[8:Rew:4816.0,147.0] ||  -> equal(op(e2,op(e2,e1)),e2)**.
% 1.32/1.48  4858[8:Rew:22.0,4837.0] ||  -> equal(e2,e1)**.
% 1.32/1.48  4859[8:MRR:4858.0,5.0] ||  -> .
% 1.32/1.48  4870[8:Spt:4859.0,348.0,4816.0] || equal(op(e1,e2),e2)** -> .
% 1.32/1.48  4871[8:Spt:4859.0,348.1,348.2,348.3,348.4] ||  -> equal(op(e1,e2),e1) equal(op(e1,e2),e4)** equal(op(e1,e2),e3) equal(op(e1,e2),e0).
% 1.32/1.48  4874[9:Spt:4871.0] ||  -> equal(op(e1,e2),e1)**.
% 1.32/1.48  4876[9:Rew:4874.0,18.0] ||  -> equal(op(e1,e1),e2)**.
% 1.32/1.48  4907[9:Rew:4876.0,142.0] ||  -> equal(op(e2,e2),e1)**.
% 1.32/1.48  4911[9:Rew:4907.0,23.0] ||  -> equal(op(e2,e1),e2)**.
% 1.32/1.48  4926[9:Rew:4911.0,112.0] || equal(op(e2,e4),e2)** -> .
% 1.32/1.48  4952[9:MRR:4768.1,4926.0] ||  -> equal(op(e2,e4),e4)**.
% 1.32/1.48  4958[9:Rew:4952.0,158.0] ||  -> equal(op(e4,op(e4,e2)),e4)**.
% 1.32/1.48  4975[9:Rew:33.0,4958.0] ||  -> equal(e4,e2)**.
% 1.32/1.48  4976[9:MRR:4975.0,9.0] ||  -> .
% 1.32/1.48  5000[9:Spt:4976.0,4871.0,4874.0] || equal(op(e1,e2),e1)** -> .
% 1.32/1.48  5001[9:Spt:4976.0,4871.1,4871.2,4871.3] ||  -> equal(op(e1,e2),e4)** equal(op(e1,e2),e3) equal(op(e1,e2),e0).
% 1.32/1.48  5004[10:Spt:5001.0] ||  -> equal(op(e1,e2),e4)**.
% 1.32/1.48  5010[10:Rew:5004.0,60.0] || equal(op(e2,e2),e4)** -> .
% 1.32/1.48  5049[10:MRR:4767.1,5010.0] ||  -> equal(op(e2,e4),e4)**.
% 1.32/1.48  5059[10:Rew:5049.0,158.0] ||  -> equal(op(e4,op(e4,e2)),e4)**.
% 1.32/1.48  5078[10:Rew:33.0,5059.0] ||  -> equal(e4,e2)**.
% 1.32/1.48  5079[10:MRR:5078.0,9.0] ||  -> .
% 1.32/1.48  5115[10:Spt:5079.0,5001.0,5004.0] || equal(op(e1,e2),e4)** -> .
% 1.32/1.48  5116[10:Spt:5079.0,5001.1,5001.2] ||  -> equal(op(e1,e2),e3)** equal(op(e1,e2),e0).
% 1.32/1.48  5119[11:Spt:5116.0] ||  -> equal(op(e1,e2),e3)**.
% 1.32/1.48  5130[11:Rew:5119.0,56.0] || equal(op(e0,e2),e3)** -> .
% 1.32/1.48  5166[11:MRR:4751.1,5130.0] ||  -> equal(op(e0,e3),e3)**.
% 1.32/1.48  5175[11:Rew:5166.0,151.0] ||  -> equal(op(e3,op(e3,e0)),e3)**.
% 1.32/1.48  5192[11:Rew:26.0,5175.0] ||  -> equal(e3,e0)**.
% 1.32/1.48  5193[11:MRR:5192.0,3.0] ||  -> .
% 1.32/1.48  5227[11:Spt:5193.0,5116.0,5119.0] || equal(op(e1,e2),e3)** -> .
% 1.32/1.48  5228[11:Spt:5193.0,5116.1] ||  -> equal(op(e1,e2),e0)**.
% 1.32/1.48  5233[11:Rew:5228.0,18.0] ||  -> equal(op(e1,e0),e2)**.
% 1.32/1.48  5235[11:Rew:5233.0,589.0] ||  -> equal(op(e4,e2),e1)**.
% 1.32/1.48  5238[11:Rew:5233.0,36.0] || equal(op(e0,e0),e2)** -> .
% 1.32/1.48  5243[11:Rew:5233.0,4771.0] ||  -> equal(e2,e1) equal(op(e4,e0),e1)** equal(op(e3,e0),e1).
% 1.32/1.48  5252[11:Rew:5235.0,127.0] || equal(op(e4,e0),e1)** -> .
% 1.32/1.48  5254[11:Rew:5235.0,65.0] || equal(op(e3,e2),e1)** -> .
% 1.32/1.48  5286[11:MRR:4750.1,5238.0] ||  -> equal(op(e0,e0),e0)**.
% 1.32/1.48  5290[11:Rew:5286.0,87.0] || equal(op(e0,e2),e0)** -> .
% 1.32/1.48  5320[11:Rew:5228.0,104.0] || equal(op(e1,e4),e0)** -> .
% 1.32/1.48  5321[11:MRR:4783.2,5320.0] ||  -> equal(op(e4,e4),e0)** equal(op(e3,e4),e0).
% 1.32/1.48  5322[11:Rew:5228.0,61.0] || equal(op(e3,e2),e0)** -> .
% 1.32/1.48  5330[11:MRR:5243.0,5243.1,5.0,5252.0] ||  -> equal(op(e3,e0),e1)**.
% 1.32/1.48  5331[11:Rew:5330.0,26.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  5347[11:Rew:5331.0,122.0] || equal(op(e3,e4),e0)** -> .
% 1.32/1.48  5357[11:MRR:5321.1,5347.0] ||  -> equal(op(e4,e4),e0)**.
% 1.32/1.48  5359[11:Rew:5357.0,35.0] ||  -> equal(op(e4,e0),e4)**.
% 1.32/1.48  5369[11:Rew:5359.0,617.0] ||  -> equal(op(e1,e4),e4)**.
% 1.32/1.48  5371[11:Rew:5359.0,128.0] || equal(op(e4,e3),e4)** -> .
% 1.32/1.48  5380[11:Rew:5369.0,80.0] || equal(op(e2,e4),e4)** -> .
% 1.32/1.48  5387[11:Rew:5369.0,105.0] || equal(op(e1,e3),e4)** -> .
% 1.32/1.48  5395[11:MRR:4767.0,5380.0] ||  -> equal(op(e2,e2),e4)**.
% 1.32/1.48  5400[11:Rew:5395.0,63.0] || equal(op(e3,e2),e4)** -> .
% 1.32/1.48  5420[11:Rew:5233.0,662.1,5233.0,662.0] || equal(op(e0,e2),e3)** equal(e2,e2) -> .
% 1.32/1.48  5421[11:Obv:5420.1] || equal(op(e0,e2),e3)** -> .
% 1.32/1.48  5436[11:MRR:2862.0,2862.2,5371.0,5387.0] ||  -> equal(op(e3,e3),e4)**.
% 1.32/1.48  5437[11:Rew:5436.0,29.0] ||  -> equal(op(e3,e4),e3)**.
% 1.32/1.48  5450[11:Rew:5437.0,124.0] || equal(op(e3,e2),e3)** -> .
% 1.32/1.48  5481[11:MRR:650.1,650.2,5290.0,5421.0] ||  -> equal(op(e0,e2),e2)**.
% 1.32/1.48  5487[11:Rew:5481.0,58.0] || equal(op(e3,e2),e2)** -> .
% 1.32/1.48  5559[11:MRR:338.0,338.1,338.2,338.3,338.4,5450.0,5487.0,5400.0,5254.0,5322.0] ||  -> .
% 1.32/1.48  5560[3:Spt:5559.0,574.0,577.0] || equal(op(e0,e1),e4)** -> .
% 1.32/1.48  5561[3:Spt:5559.0,574.1,574.2] ||  -> equal(op(e0,e1),e3)** equal(op(e0,e1),e2).
% 1.32/1.48  5562[3:MRR:311.4,5560.0] ||  -> equal(op(e4,e1),e4)** equal(op(e1,e1),e4) equal(op(e3,e1),e4) equal(op(e2,e1),e4).
% 1.32/1.48  5563[3:MRR:322.4,5560.0] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e0),e4) equal(op(e0,e3),e4) equal(op(e0,e2),e4).
% 1.32/1.48  5564[4:Spt:5561.0] ||  -> equal(op(e0,e1),e3)**.
% 1.32/1.48  5568[4:Rew:5564.0,12.0] ||  -> equal(op(e0,e3),e1)**.
% 1.32/1.48  5569[4:Rew:5564.0,46.0] || equal(op(e1,e1),e3)** -> .
% 1.32/1.48  5570[4:Rew:5564.0,47.0] || equal(op(e2,e1),e3)** -> .
% 1.32/1.48  5571[4:Rew:5564.0,48.0] || equal(op(e3,e1),e3)** -> .
% 1.32/1.48  5573[4:Rew:5564.0,86.0] || equal(op(e0,e0),e3)** -> .
% 1.32/1.48  5574[4:Rew:5564.0,90.0] || equal(op(e0,e2),e3)** -> .
% 1.32/1.48  5576[4:Rew:5564.0,92.0] || equal(op(e0,e4),e3)** -> .
% 1.32/1.48  5577[4:Rew:5564.0,137.0] ||  -> equal(op(op(e1,e0),e3),e0)**.
% 1.32/1.48  5578[4:Rew:5564.0,141.0] ||  -> equal(op(e3,op(e1,e0)),e1)**.
% 1.32/1.48  5581[4:Rew:5564.0,326.4] ||  -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e4),e2)** equal(op(e0,e3),e2) equal(e3,e2).
% 1.32/1.48  5582[4:Rew:5564.0,315.4] ||  -> equal(op(e2,e1),e2) equal(op(e1,e1),e2) equal(op(e4,e1),e2)** equal(op(e3,e1),e2) equal(e3,e2).
% 1.32/1.48  5586[4:Rew:5568.0,88.0] || equal(op(e0,e0),e1)** -> .
% 1.32/1.48  5587[4:Rew:5568.0,69.0] || equal(op(e4,e3),e1)** -> .
% 1.32/1.48  5590[4:Rew:5568.0,66.0] || equal(op(e1,e3),e1)** -> .
% 1.32/1.48  5591[4:Rew:5568.0,67.0] || equal(op(e2,e3),e1)** -> .
% 1.32/1.48  5592[4:Rew:5568.0,95.0] || equal(op(e0,e4),e1)** -> .
% 1.32/1.48  5593[4:Rew:5568.0,151.0] ||  -> equal(op(e1,op(e3,e0)),e3)**.
% 1.32/1.48  5594[4:Rew:5568.0,139.0] ||  -> equal(op(op(e3,e0),e1),e0)**.
% 1.32/1.48  5596[4:Rew:5568.0,575.2] ||  -> equal(op(e0,e0),e0) equal(op(e0,e4),e0)** equal(e1,e0) equal(op(e0,e2),e0).
% 1.32/1.48  5605[4:Rew:5568.0,295.4] ||  -> equal(op(e3,e3),e2) equal(op(e2,e3),e2) equal(op(e4,e3),e2)** equal(op(e1,e3),e2) equal(e2,e1).
% 1.32/1.48  5607[4:MRR:349.2,5569.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e1),e4)** equal(op(e1,e1),e2) equal(op(e1,e1),e0).
% 1.32/1.48  5608[4:MRR:314.1,5569.0] ||  -> equal(op(e1,e3),e3) equal(op(e1,e4),e3)** equal(op(e1,e2),e3) equal(op(e1,e0),e3).
% 1.32/1.48  5609[4:MRR:344.3,5570.0] ||  -> equal(op(e2,e1),e2) equal(op(e2,e1),e1) equal(op(e2,e1),e4)** equal(op(e2,e1),e0).
% 1.32/1.48  5611[4:MRR:339.0,5571.0] ||  -> equal(op(e3,e1),e1) equal(op(e3,e1),e4)** equal(op(e3,e1),e2) equal(op(e3,e1),e0).
% 1.32/1.48  5612[4:MRR:294.3,5571.0] ||  -> equal(op(e3,e3),e3) equal(op(e3,e4),e3)** equal(op(e3,e2),e3) equal(op(e3,e0),e3).
% 1.32/1.48  5615[4:MRR:355.2,5573.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e4)** equal(op(e0,e0),e2) equal(op(e0,e0),e1).
% 1.32/1.48  5616[4:MRR:323.1,5573.0] ||  -> equal(op(e3,e0),e3) equal(op(e4,e0),e3)** equal(op(e2,e0),e3) equal(op(e1,e0),e3).
% 1.32/1.48  5618[4:MRR:303.4,5574.0] ||  -> equal(op(e3,e2),e3) equal(op(e2,e2),e3) equal(op(e4,e2),e3)** equal(op(e1,e2),e3).
% 1.32/1.48  5620[4:MRR:283.4,5576.0] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3) equal(op(e2,e4),e3) equal(op(e1,e4),e3).
% 1.32/1.48  5622[4:MRR:327.1,5586.0] ||  -> equal(op(e1,e0),e1) equal(op(e4,e0),e1)** equal(op(e3,e0),e1) equal(op(e2,e0),e1).
% 1.32/1.48  5623[4:MRR:288.2,5587.0] ||  -> equal(op(e4,e4),e1)** equal(op(e4,e1),e1) equal(op(e4,e2),e1) equal(op(e4,e0),e1).
% 1.32/1.48  5628[4:MRR:318.2,5590.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e4),e1)** equal(op(e1,e2),e1) equal(op(e1,e0),e1).
% 1.32/1.48  5630[4:MRR:308.3,5591.0] ||  -> equal(op(e2,e2),e1) equal(op(e2,e1),e1) equal(op(e2,e4),e1)** equal(op(e2,e0),e1).
% 1.32/1.48  5632[4:MRR:287.4,5592.0] ||  -> equal(op(e4,e4),e1)** equal(op(e1,e4),e1) equal(op(e3,e4),e1) equal(op(e2,e4),e1).
% 1.32/1.48  5633[4:MRR:5596.2,1.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e4),e0)** equal(op(e0,e2),e0).
% 1.32/1.48  5635[4:MRR:5615.3,5586.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e4)** equal(op(e0,e0),e2).
% 1.32/1.48  5650[4:Rew:5568.0,5581.3] ||  -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e4),e2)** equal(e2,e1) equal(e3,e2).
% 1.32/1.48  5651[4:MRR:5650.3,5650.4,5.0,8.0] ||  -> equal(op(e0,e2),e2) equal(op(e0,e0),e2) equal(op(e0,e4),e2)**.
% 1.32/1.48  5652[4:MRR:5582.4,8.0] ||  -> equal(op(e2,e1),e2) equal(op(e1,e1),e2) equal(op(e4,e1),e2)** equal(op(e3,e1),e2).
% 1.32/1.48  5655[4:MRR:5605.4,5.0] ||  -> equal(op(e3,e3),e2) equal(op(e2,e3),e2) equal(op(e4,e3),e2)** equal(op(e1,e3),e2).
% 1.32/1.48  5658[5:Spt:346.0] ||  -> equal(op(e1,e4),e4)**.
% 1.32/1.48  5668[5:Rew:5658.0,157.0] ||  -> equal(op(e4,op(e4,e1)),e4)**.
% 1.32/1.48  5700[5:Rew:32.0,5668.0] ||  -> equal(e4,e1)**.
% 1.32/1.48  5701[5:MRR:5700.0,7.0] ||  -> .
% 1.32/1.48  5720[5:Spt:5701.0,346.0,5658.0] || equal(op(e1,e4),e4)** -> .
% 1.32/1.48  5721[5:Spt:5701.0,346.1,346.2,346.3,346.4] ||  -> equal(op(e1,e4),e1) equal(op(e1,e4),e3)** equal(op(e1,e4),e2) equal(op(e1,e4),e0).
% 1.32/1.48  5724[6:Spt:5721.0] ||  -> equal(op(e1,e4),e1)**.
% 1.32/1.48  5726[6:Rew:5724.0,20.0] ||  -> equal(op(e1,e1),e4)**.
% 1.32/1.48  5736[6:Rew:5724.0,157.0] ||  -> equal(op(e1,op(e4,e1)),e4)**.
% 1.32/1.48  5756[6:Rew:5726.0,142.0] ||  -> equal(op(e4,e4),e1)**.
% 1.32/1.48  5761[6:Rew:5756.0,35.0] ||  -> equal(op(e4,e1),e4)**.
% 1.32/1.48  5813[6:Rew:5724.0,5736.0,5761.0,5736.0] ||  -> equal(e4,e1)**.
% 1.32/1.48  5814[6:MRR:5813.0,7.0] ||  -> .
% 1.32/1.48  5853[6:Spt:5814.0,5721.0,5724.0] || equal(op(e1,e4),e1)** -> .
% 1.32/1.48  5854[6:Spt:5814.0,5721.1,5721.2,5721.3] ||  -> equal(op(e1,e4),e3)** equal(op(e1,e4),e2) equal(op(e1,e4),e0).
% 1.32/1.48  5855[6:MRR:5628.1,5853.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e2),e1)** equal(op(e1,e0),e1).
% 1.32/1.48  5856[6:MRR:5632.1,5853.0] ||  -> equal(op(e4,e4),e1)** equal(op(e3,e4),e1) equal(op(e2,e4),e1).
% 1.32/1.48  5857[7:Spt:5854.0] ||  -> equal(op(e1,e4),e3)**.
% 1.32/1.48  5860[7:Rew:5857.0,20.0] ||  -> equal(op(e1,e3),e4)**.
% 1.32/1.48  5861[7:Rew:5857.0,99.0] || equal(op(e1,e0),e3)** -> .
% 1.32/1.48  5862[7:Rew:5857.0,104.0] || equal(op(e1,e2),e3)** -> .
% 1.32/1.48  5865[7:Rew:5857.0,81.0] || equal(op(e3,e4),e3)** -> .
% 1.32/1.48  5869[7:Rew:5857.0,157.0] ||  -> equal(op(e3,op(e4,e1)),e4)**.
% 1.32/1.48  5871[7:Rew:5857.0,260.0] || equal(e3,e3) equal(op(e1,op(op(e1,e4),e1)),e2)** equal(op(op(e1,e4),e1),e0) -> .
% 1.32/1.48  5873[7:Rew:5857.0,316.2] ||  -> equal(op(e1,e2),e2) equal(op(e1,e1),e2) equal(e3,e2) equal(op(e1,e3),e2)** equal(op(e1,e0),e2).
% 1.32/1.48  5874[7:Rew:5857.0,285.3] ||  -> equal(op(e4,e4),e2)** equal(op(e2,e4),e2) equal(op(e3,e4),e2) equal(e3,e2) equal(op(e0,e4),e2).
% 1.32/1.48  5878[7:Rew:5857.0,289.4] ||  -> equal(op(e4,e4),e0)** equal(op(e0,e4),e0) equal(op(e3,e4),e0) equal(op(e2,e4),e0) equal(e3,e0).
% 1.32/1.48  5882[7:Rew:5860.0,103.0] || equal(op(e1,e2),e4)** -> .
% 1.32/1.48  5883[7:Rew:5860.0,98.0] || equal(op(e1,e0),e4)** -> .
% 1.32/1.48  5888[7:Rew:5860.0,152.0] ||  -> equal(op(e4,op(e3,e1)),e3)**.
% 1.32/1.48  5893[7:Rew:5860.0,266.1] || equal(op(e1,e3),e4) equal(op(e1,op(e4,e1)),e2) equal(op(op(e1,e3),e1),e0)** -> .
% 1.32/1.48  5896[7:Rew:5860.0,5655.3] ||  -> equal(op(e3,e3),e2) equal(op(e2,e3),e2) equal(op(e4,e3),e2)** equal(e4,e2).
% 1.32/1.48  5899[7:Rew:5860.0,101.0] || equal(op(e1,e1),e4)** -> .
% 1.32/1.48  5900[7:MRR:5616.3,5861.0] ||  -> equal(op(e3,e0),e3) equal(op(e4,e0),e3)** equal(op(e2,e0),e3).
% 1.32/1.48  5901[7:MRR:350.3,5861.0] ||  -> equal(op(e1,e0),e1) equal(op(e1,e0),e0) equal(op(e1,e0),e4)** equal(op(e1,e0),e2).
% 1.32/1.48  5902[7:MRR:5618.3,5862.0] ||  -> equal(op(e3,e2),e3) equal(op(e2,e2),e3) equal(op(e4,e2),e3)**.
% 1.32/1.48  5908[7:MRR:336.1,5865.0] ||  -> equal(op(e3,e4),e4)** equal(op(e3,e4),e2) equal(op(e3,e4),e1) equal(op(e3,e4),e0).
% 1.32/1.48  5911[7:MRR:301.3,5882.0] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e3,e2),e4) equal(op(e0,e2),e4).
% 1.32/1.48  5912[7:MRR:321.4,5883.0] ||  -> equal(op(e4,e0),e4)** equal(op(e0,e0),e4) equal(op(e3,e0),e4) equal(op(e2,e0),e4).
% 1.32/1.48  5920[7:MRR:5562.1,5899.0] ||  -> equal(op(e4,e1),e4)** equal(op(e3,e1),e4) equal(op(e2,e1),e4).
% 1.32/1.48  5922[7:MRR:5896.3,9.0] ||  -> equal(op(e3,e3),e2) equal(op(e2,e3),e2) equal(op(e4,e3),e2)**.
% 1.32/1.48  5924[7:MRR:5901.2,5883.0] ||  -> equal(op(e1,e0),e1) equal(op(e1,e0),e0) equal(op(e1,e0),e2)**.
% 1.32/1.48  5926[7:Obv:5871.0] || equal(op(e1,op(op(e1,e4),e1)),e2)** equal(op(op(e1,e4),e1),e0) -> .
% 1.32/1.48  5927[7:Rew:5857.0,5926.1,5857.0,5926.0] || equal(op(e1,op(e3,e1)),e2)** equal(op(e3,e1),e0) -> .
% 1.32/1.48  5931[7:Rew:5860.0,5893.2,5860.0,5893.0] || equal(e4,e4) equal(op(e1,op(e4,e1)),e2)** equal(op(e4,e1),e0) -> .
% 1.32/1.48  5932[7:Obv:5931.0] || equal(op(e1,op(e4,e1)),e2)** equal(op(e4,e1),e0) -> .
% 1.32/1.48  5936[7:Rew:5860.0,5873.3] ||  -> equal(op(e1,e2),e2)** equal(op(e1,e1),e2) equal(e3,e2) equal(e4,e2) equal(op(e1,e0),e2).
% 1.32/1.48  5937[7:MRR:5936.2,5936.3,8.0,9.0] ||  -> equal(op(e1,e2),e2)** equal(op(e1,e1),e2) equal(op(e1,e0),e2).
% 1.32/1.48  5938[7:MRR:5874.3,8.0] ||  -> equal(op(e4,e4),e2)** equal(op(e2,e4),e2) equal(op(e3,e4),e2) equal(op(e0,e4),e2).
% 1.32/1.48  5941[7:MRR:5878.4,3.0] ||  -> equal(op(e4,e4),e0)** equal(op(e0,e4),e0) equal(op(e3,e4),e0) equal(op(e2,e4),e0).
% 1.32/1.48  5943[8:Spt:340.0] ||  -> equal(op(e3,e0),e3)**.
% 1.32/1.48  5944[8:Rew:5943.0,26.0] ||  -> equal(op(e3,e3),e0)**.
% 1.32/1.48  5948[8:Rew:5943.0,117.0] || equal(op(e3,e2),e3)** -> .
% 1.32/1.48  5954[8:Rew:5943.0,296.4] ||  -> equal(op(e3,e3),e2) equal(op(e3,e2),e2) equal(op(e3,e4),e2)** equal(op(e3,e1),e2) equal(e3,e2).
% 1.32/1.48  5955[8:Rew:5943.0,325.3] ||  -> equal(op(e2,e0),e2) equal(op(e0,e0),e2) equal(op(e4,e0),e2)** equal(e3,e2) equal(op(e1,e0),e2).
% 1.32/1.48  5970[8:Rew:5943.0,5594.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  5974[8:Rew:5944.0,125.0] || equal(op(e3,e4),e0)** -> .
% 1.32/1.48  5988[8:Rew:5970.0,5927.1] || equal(op(e1,op(e3,e1)),e2)** equal(e0,e0) -> .
% 1.32/1.48  6001[8:Rew:5970.0,5920.1] ||  -> equal(op(e4,e1),e4)** equal(e4,e0) equal(op(e2,e1),e4).
% 1.32/1.48  6003[8:Rew:5970.0,5888.0] ||  -> equal(op(e4,e0),e3)**.
% 1.32/1.48  6008[8:Rew:6003.0,31.0] ||  -> equal(op(e4,e3),e0)**.
% 1.32/1.48  6010[8:Rew:6003.0,127.0] || equal(op(e4,e2),e3)** -> .
% 1.32/1.48  6022[8:Rew:6003.0,286.4] ||  -> equal(op(e4,e4),e2)** equal(op(e4,e2),e2) equal(op(e4,e3),e2) equal(op(e4,e1),e2) equal(e3,e2).
% 1.32/1.48  6038[8:Rew:6008.0,135.0] || equal(op(e4,e4),e0)** -> .
% 1.32/1.48  6043[8:MRR:5902.0,5948.0] ||  -> equal(op(e2,e2),e3) equal(op(e4,e2),e3)**.
% 1.32/1.48  6053[8:MRR:5941.2,5974.0] ||  -> equal(op(e4,e4),e0)** equal(op(e0,e4),e0) equal(op(e2,e4),e0).
% 1.32/1.48  6065[8:MRR:6043.1,6010.0] ||  -> equal(op(e2,e2),e3)**.
% 1.32/1.48  6066[8:Rew:6065.0,23.0] ||  -> equal(op(e2,e3),e2)**.
% 1.32/1.48  6085[8:Rew:6066.0,108.0] || equal(op(e2,e0),e2)** -> .
% 1.32/1.48  6096[8:Obv:5988.1] || equal(op(e1,op(e3,e1)),e2)** -> .
% 1.32/1.48  6097[8:Rew:5970.0,6096.0] || equal(op(e1,e0),e2)** -> .
% 1.32/1.48  6103[8:MRR:6001.1,4.0] ||  -> equal(op(e4,e1),e4)** equal(op(e2,e1),e4).
% 1.32/1.48  6104[8:MRR:6053.0,6038.0] ||  -> equal(op(e0,e4),e0) equal(op(e2,e4),e0)**.
% 1.32/1.48  6159[8:Rew:5970.0,5954.3,5944.0,5954.0] ||  -> equal(e2,e0) equal(op(e3,e2),e2) equal(op(e3,e4),e2)** equal(e2,e0) equal(e3,e2).
% 1.32/1.48  6160[8:Obv:6159.0] ||  -> equal(op(e3,e2),e2) equal(op(e3,e4),e2)** equal(e2,e0) equal(e3,e2).
% 1.32/1.48  6161[8:MRR:6160.2,6160.3,2.0,8.0] ||  -> equal(op(e3,e2),e2) equal(op(e3,e4),e2)**.
% 1.32/1.48  6162[8:Rew:6003.0,5955.2] ||  -> equal(op(e2,e0),e2)** equal(op(e0,e0),e2) equal(e3,e2) equal(e3,e2) equal(op(e1,e0),e2).
% 1.32/1.48  6163[8:Obv:6162.2] ||  -> equal(op(e2,e0),e2)** equal(op(e0,e0),e2) equal(e3,e2) equal(op(e1,e0),e2).
% 1.32/1.48  6164[8:MRR:6163.0,6163.2,6163.3,6085.0,8.0,6097.0] ||  -> equal(op(e0,e0),e2)**.
% 1.32/1.48  6165[8:Rew:6164.0,11.0] ||  -> equal(op(e0,e2),e0)**.
% 1.32/1.48  6180[8:Rew:6165.0,94.0] || equal(op(e0,e4),e0)** -> .
% 1.32/1.48  6210[8:MRR:6104.0,6180.0] ||  -> equal(op(e2,e4),e0)**.
% 1.32/1.48  6211[8:Rew:6210.0,25.0] ||  -> equal(op(e2,e0),e4)**.
% 1.32/1.48  6230[8:Rew:6211.0,106.0] || equal(op(e2,e1),e4)** -> .
% 1.32/1.48  6239[8:MRR:6103.1,6230.0] ||  -> equal(op(e4,e1),e4)**.
% 1.32/1.48  6242[8:Rew:6239.0,32.0] ||  -> equal(op(e4,e4),e1)**.
% 1.32/1.48  6251[8:Rew:6239.0,5869.0] ||  -> equal(op(e3,e4),e4)**.
% 1.32/1.48  6278[8:Rew:6251.0,6161.1] ||  -> equal(op(e3,e2),e2)** equal(e4,e2).
% 1.32/1.48  6323[8:MRR:6278.1,9.0] ||  -> equal(op(e3,e2),e2)**.
% 1.32/1.48  6325[8:Rew:6323.0,65.0] || equal(op(e4,e2),e2)** -> .
% 1.32/1.48  6363[8:Rew:6239.0,6022.3,6008.0,6022.2,6242.0,6022.0] ||  -> equal(e2,e1) equal(op(e4,e2),e2)** equal(e2,e0) equal(e4,e2) equal(e3,e2).
% 1.32/1.48  6364[8:MRR:6363.0,6363.1,6363.2,6363.3,6363.4,5.0,6325.0,2.0,9.0,8.0] ||  -> .
% 1.32/1.48  6365[8:Spt:6364.0,340.0,5943.0] || equal(op(e3,e0),e3)** -> .
% 1.32/1.48  6366[8:Spt:6364.0,340.1,340.2,340.3,340.4] ||  -> equal(op(e3,e0),e0) equal(op(e3,e0),e4)** equal(op(e3,e0),e2) equal(op(e3,e0),e1).
% 1.32/1.48  6367[8:MRR:5900.0,6365.0] ||  -> equal(op(e4,e0),e3)** equal(op(e2,e0),e3).
% 1.32/1.48  6369[9:Spt:6366.0] ||  -> equal(op(e3,e0),e0)**.
% 1.32/1.48  6372[9:Rew:6369.0,5593.0] ||  -> equal(op(e1,e0),e3)**.
% 1.32/1.48  6398[9:MRR:6372.0,5861.0] ||  -> .
% 1.32/1.48  6423[9:Spt:6398.0,6366.0,6369.0] || equal(op(e3,e0),e0)** -> .
% 1.32/1.48  6424[9:Spt:6398.0,6366.1,6366.2,6366.3] ||  -> equal(op(e3,e0),e4)** equal(op(e3,e0),e2) equal(op(e3,e0),e1).
% 1.32/1.48  6426[9:MRR:329.2,6423.0] ||  -> equal(op(e0,e0),e0) equal(op(e4,e0),e0)** equal(op(e2,e0),e0) equal(op(e1,e0),e0).
% 1.32/1.48  6427[10:Spt:6424.0] ||  -> equal(op(e3,e0),e4)**.
% 1.32/1.48  6430[10:Rew:6427.0,26.0] ||  -> equal(op(e3,e4),e0)**.
% 1.32/1.48  6432[10:Rew:6427.0,5594.0] ||  -> equal(op(e4,e1),e0)**.
% 1.32/1.48  6435[10:Rew:6427.0,116.0] || equal(op(e3,e1),e4)** -> .
% 1.32/1.48  6436[10:Rew:6427.0,117.0] || equal(op(e3,e2),e4)** -> .
% 1.32/1.48  6456[10:Rew:6430.0,122.0] || equal(op(e3,e1),e0)** -> .
% 1.32/1.48  6459[10:Rew:6430.0,78.0] || equal(op(e0,e4),e0)** -> .
% 1.32/1.48  6465[10:Rew:6430.0,5856.1] ||  -> equal(op(e4,e4),e1)** equal(e1,e0) equal(op(e2,e4),e1).
% 1.32/1.48  6475[10:Rew:6432.0,32.0] ||  -> equal(op(e4,e0),e1)**.
% 1.32/1.48  6483[10:Rew:6432.0,5932.0] || equal(op(e1,e0),e2) equal(op(e4,e1),e0)** -> .
% 1.32/1.48  6496[10:Rew:6475.0,129.0] || equal(op(e4,e4),e1)** -> .
% 1.32/1.48  6501[10:Rew:6475.0,42.0] || equal(op(e1,e0),e1)** -> .
% 1.32/1.48  6507[10:Rew:6475.0,6367.0] ||  -> equal(e3,e1) equal(op(e2,e0),e3)**.
% 1.32/1.48  6515[10:MRR:5611.1,6435.0] ||  -> equal(op(e3,e1),e1) equal(op(e3,e1),e2)** equal(op(e3,e1),e0).
% 1.32/1.48  6516[10:MRR:5911.2,6436.0] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e0,e2),e4).
% 1.32/1.48  6528[10:MRR:5633.1,6459.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e2),e0)**.
% 1.32/1.48  6538[10:MRR:5855.2,6501.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e2),e1)**.
% 1.32/1.48  6539[10:MRR:5924.0,6501.0] ||  -> equal(op(e1,e0),e0) equal(op(e1,e0),e2)**.
% 1.32/1.48  6540[10:MRR:6507.0,6.0] ||  -> equal(op(e2,e0),e3)**.
% 1.32/1.48  6541[10:Rew:6540.0,21.0] ||  -> equal(op(e2,e3),e0)**.
% 1.32/1.48  6568[10:Rew:6541.0,5922.1] ||  -> equal(op(e3,e3),e2) equal(e2,e0) equal(op(e4,e3),e2)**.
% 1.32/1.48  6593[10:Rew:6432.0,6483.1] || equal(op(e1,e0),e2)** equal(e0,e0) -> .
% 1.32/1.48  6594[10:Obv:6593.1] || equal(op(e1,e0),e2)** -> .
% 1.32/1.48  6596[10:MRR:6539.1,6594.0] ||  -> equal(op(e1,e0),e0)**.
% 1.32/1.48  6602[10:Rew:6596.0,36.0] || equal(op(e0,e0),e0)** -> .
% 1.32/1.48  6612[10:MRR:6528.0,6602.0] ||  -> equal(op(e0,e2),e0)**.
% 1.32/1.48  6640[10:MRR:6465.0,6465.1,6496.0,1.0] ||  -> equal(op(e2,e4),e1)**.
% 1.32/1.48  6642[10:Rew:6640.0,25.0] ||  -> equal(op(e2,e1),e4)**.
% 1.32/1.48  6655[10:Rew:6642.0,110.0] || equal(op(e2,e2),e4)** -> .
% 1.32/1.48  6658[10:Rew:6642.0,143.0] ||  -> equal(op(e4,op(e1,e2)),e1)**.
% 1.32/1.48  6665[10:MRR:6568.1,2.0] ||  -> equal(op(e3,e3),e2) equal(op(e4,e3),e2)**.
% 1.32/1.48  6666[10:MRR:6515.2,6456.0] ||  -> equal(op(e3,e1),e1) equal(op(e3,e1),e2)**.
% 1.32/1.48  6667[10:Rew:6612.0,6516.2] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(e4,e0).
% 1.32/1.48  6668[10:MRR:6667.1,6667.2,6655.0,4.0] ||  -> equal(op(e4,e2),e4)**.
% 1.32/1.48  6669[10:Rew:6668.0,33.0] ||  -> equal(op(e4,e4),e2)**.
% 1.32/1.48  6685[10:Rew:6669.0,135.0] || equal(op(e4,e3),e2)** -> .
% 1.32/1.48  6697[10:MRR:6665.1,6685.0] ||  -> equal(op(e3,e3),e2)**.
% 1.32/1.48  6710[10:Rew:6697.0,121.0] || equal(op(e3,e1),e2)** -> .
% 1.32/1.48  6735[10:MRR:6666.1,6710.0] ||  -> equal(op(e3,e1),e1)**.
% 1.32/1.48  6740[10:Rew:6735.0,51.0] || equal(op(e1,e1),e1)** -> .
% 1.32/1.48  6750[10:MRR:6538.0,6740.0] ||  -> equal(op(e1,e2),e1)**.
% 1.32/1.48  6764[10:Rew:6750.0,6658.0] ||  -> equal(op(e4,e1),e1)**.
% 1.32/1.48  6768[10:Rew:6432.0,6764.0] ||  -> equal(e1,e0)**.
% 1.32/1.48  6769[10:MRR:6768.0,1.0] ||  -> .
% 1.32/1.48  6821[10:Spt:6769.0,6424.0,6427.0] || equal(op(e3,e0),e4)** -> .
% 1.32/1.48  6822[10:Spt:6769.0,6424.1,6424.2] ||  -> equal(op(e3,e0),e2)** equal(op(e3,e0),e1).
% 1.32/1.48  6824[10:MRR:5912.2,6821.0] ||  -> equal(op(e4,e0),e4)** equal(op(e0,e0),e4) equal(op(e2,e0),e4).
% 1.32/1.48  6825[11:Spt:6822.0] ||  -> equal(op(e3,e0),e2)**.
% 1.32/1.48  6829[11:Rew:6825.0,5594.0] ||  -> equal(op(e2,e1),e0)**.
% 1.32/1.48  6833[11:Rew:6825.0,118.0] || equal(op(e3,e3),e2)** -> .
% 1.32/1.48  6834[11:Rew:6825.0,119.0] || equal(op(e3,e4),e2)** -> .
% 1.32/1.48  6838[11:Rew:6825.0,38.0] || equal(op(e0,e0),e2)** -> .
% 1.32/1.48  6839[11:Rew:6825.0,41.0] || equal(op(e1,e0),e2)** -> .
% 1.32/1.48  6848[11:Rew:6829.0,22.0] ||  -> equal(op(e2,e0),e1)**.
% 1.32/1.48  6861[11:Rew:6829.0,5920.2] ||  -> equal(op(e4,e1),e4)** equal(op(e3,e1),e4) equal(e4,e0).
% 1.32/1.48  6894[11:Rew:6848.0,40.0] || equal(op(e1,e0),e1)** -> .
% 1.32/1.48  6903[11:Rew:6848.0,6367.1] ||  -> equal(op(e4,e0),e3)** equal(e3,e1).
% 1.32/1.48  6912[11:MRR:5922.0,6833.0] ||  -> equal(op(e2,e3),e2) equal(op(e4,e3),e2)**.
% 1.32/1.48  6913[11:MRR:5938.2,6834.0] ||  -> equal(op(e4,e4),e2)** equal(op(e2,e4),e2) equal(op(e0,e4),e2).
% 1.32/1.48  6919[11:MRR:5635.2,6838.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e4)**.
% 1.32/1.48  6921[11:MRR:5924.2,6839.0] ||  -> equal(op(e1,e0),e1)** equal(op(e1,e0),e0).
% 1.32/1.48  6953[11:MRR:6903.1,6.0] ||  -> equal(op(e4,e0),e3)**.
% 1.32/1.48  6954[11:Rew:6953.0,31.0] ||  -> equal(op(e4,e3),e0)**.
% 1.32/1.48  6984[11:Rew:6954.0,6912.1] ||  -> equal(op(e2,e3),e2)** equal(e2,e0).
% 1.32/1.48  6985[11:MRR:6984.1,2.0] ||  -> equal(op(e2,e3),e2)**.
% 1.32/1.48  6989[11:Rew:6985.0,115.0] || equal(op(e2,e4),e2)** -> .
% 1.32/1.48  7026[11:MRR:6921.0,6894.0] ||  -> equal(op(e1,e0),e0)**.
% 1.32/1.48  7034[11:Rew:7026.0,36.0] || equal(op(e0,e0),e0)** -> .
% 1.32/1.48  7041[11:MRR:6919.0,7034.0] ||  -> equal(op(e0,e0),e4)**.
% 1.32/1.48  7044[11:Rew:7041.0,11.0] ||  -> equal(op(e0,e4),e0)**.
% 1.32/1.48  7091[11:MRR:6861.2,4.0] ||  -> equal(op(e4,e1),e4)** equal(op(e3,e1),e4).
% 1.32/1.48  7093[11:Rew:7044.0,6913.2] ||  -> equal(op(e4,e4),e2)** equal(op(e2,e4),e2) equal(e2,e0).
% 1.32/1.48  7094[11:MRR:7093.1,7093.2,6989.0,2.0] ||  -> equal(op(e4,e4),e2)**.
% 1.32/1.48  7096[11:Rew:7094.0,35.0] ||  -> equal(op(e4,e2),e4)**.
% 1.32/1.48  7105[11:Rew:7096.0,130.0] || equal(op(e4,e1),e4)** -> .
% 1.32/1.48  7115[11:MRR:7091.0,7105.0] ||  -> equal(op(e3,e1),e4)**.
% 1.32/1.48  7123[11:Rew:7115.0,280.0] || equal(e4,e4) equal(op(e3,op(op(e3,e1),e3)),e2)** equal(op(op(e3,e1),e3),e0) -> .
% 1.32/1.48  7194[11:Obv:7123.0] || equal(op(e3,op(op(e3,e1),e3)),e2)** equal(op(op(e3,e1),e3),e0) -> .
% 1.32/1.48  7195[11:Rew:6954.0,7194.1,7115.0,7194.1,6825.0,7194.0,6954.0,7194.0,7115.0,7194.0] || equal(e2,e2)* equal(e0,e0) -> .
% 1.32/1.48  7196[11:Obv:7195.1] ||  -> .
% 1.32/1.48  7201[11:Spt:7196.0,6822.0,6825.0] || equal(op(e3,e0),e2)** -> .
% 1.32/1.48  7202[11:Spt:7196.0,6822.1] ||  -> equal(op(e3,e0),e1)**.
% 1.32/1.48  7207[11:Rew:7202.0,26.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  7211[11:Rew:7202.0,5594.0] ||  -> equal(op(e1,e1),e0)**.
% 1.32/1.48  7214[11:Rew:7211.0,17.0] ||  -> equal(op(e1,e0),e1)**.
% 1.32/1.48  7224[11:Rew:7207.0,5888.0] ||  -> equal(op(e4,e0),e3)**.
% 1.32/1.48  7236[11:Rew:7202.0,117.0] || equal(op(e3,e2),e1)** -> .
% 1.32/1.48  7238[11:Rew:7202.0,119.0] || equal(op(e3,e4),e1)** -> .
% 1.32/1.48  7243[11:Rew:7207.0,120.0] || equal(op(e3,e2),e0)** -> .
% 1.32/1.48  7266[11:Rew:7207.0,122.0] || equal(op(e3,e4),e0)** -> .
% 1.32/1.48  7278[11:Rew:7207.0,5920.1] ||  -> equal(op(e4,e1),e4)** equal(e4,e0) equal(op(e2,e1),e4).
% 1.32/1.48  7279[11:MRR:7278.1,4.0] ||  -> equal(op(e4,e1),e4)** equal(op(e2,e1),e4).
% 1.32/1.48  7283[11:Rew:7224.0,6824.0] ||  -> equal(e4,e3) equal(op(e0,e0),e4) equal(op(e2,e0),e4)**.
% 1.32/1.48  7284[11:MRR:7283.0,10.0] ||  -> equal(op(e0,e0),e4) equal(op(e2,e0),e4)**.
% 1.32/1.48  7289[11:Rew:7214.0,5937.2,7211.0,5937.1] ||  -> equal(op(e1,e2),e2)** equal(e2,e0) equal(e2,e1).
% 1.32/1.48  7290[11:MRR:7289.1,7289.2,2.0,5.0] ||  -> equal(op(e1,e2),e2)**.
% 1.32/1.48  7294[11:Rew:7290.0,61.0] || equal(op(e3,e2),e2)** -> .
% 1.32/1.48  7317[11:MRR:5908.2,5908.3,7238.0,7266.0] ||  -> equal(op(e3,e4),e4)** equal(op(e3,e4),e2).
% 1.32/1.48  7318[11:Rew:7214.0,6426.3,7224.0,6426.1] ||  -> equal(op(e0,e0),e0) equal(e3,e0) equal(op(e2,e0),e0)** equal(e1,e0).
% 1.32/1.48  7319[11:MRR:7318.1,7318.3,3.0,1.0] ||  -> equal(op(e0,e0),e0) equal(op(e2,e0),e0)**.
% 1.32/1.48  7326[11:Rew:7207.0,5652.3,7211.0,5652.1] ||  -> equal(op(e2,e1),e2) equal(e2,e0) equal(op(e4,e1),e2)** equal(e2,e0).
% 1.32/1.48  7327[11:Obv:7326.1] ||  -> equal(op(e2,e1),e2) equal(op(e4,e1),e2)** equal(e2,e0).
% 1.32/1.48  7328[11:MRR:7327.2,2.0] ||  -> equal(op(e2,e1),e2) equal(op(e4,e1),e2)**.
% 1.32/1.48  7363[11:Rew:5860.0,181.2,7202.0,181.2,5860.0,181.1,7202.0,181.1,7202.0,181.0] || equal(e1,e1) equal(op(e3,e4),e2)** equal(e4,e4) -> .
% 1.32/1.48  7364[11:Obv:7363.2] || equal(op(e3,e4),e2)** -> .
% 1.32/1.48  7366[11:MRR:7317.1,7364.0] ||  -> equal(op(e3,e4),e4)**.
% 1.32/1.48  7370[11:Rew:7366.0,124.0] || equal(op(e3,e2),e4)** -> .
% 1.32/1.48  7396[11:MRR:338.1,338.2,338.3,338.4,7294.0,7370.0,7236.0,7243.0] ||  -> equal(op(e3,e2),e3)**.
% 1.32/1.48  7397[11:Rew:7396.0,28.0] ||  -> equal(op(e3,e3),e2)**.
% 1.32/1.48  7413[11:Rew:7397.0,154.0] ||  -> equal(op(e2,e2),e3)**.
% 1.32/1.48  7415[11:Rew:7413.0,23.0] ||  -> equal(op(e2,e3),e2)**.
% 1.32/1.48  7431[11:Rew:7415.0,111.0] || equal(op(e2,e1),e2)** -> .
% 1.32/1.48  7441[11:MRR:7328.0,7431.0] ||  -> equal(op(e4,e1),e2)**.
% 1.32/1.48  7455[11:Rew:7441.0,7279.0] ||  -> equal(e4,e2) equal(op(e2,e1),e4)**.
% 1.32/1.48  7500[11:MRR:7455.0,9.0] ||  -> equal(op(e2,e1),e4)**.
% 1.32/1.48  7505[11:Rew:7500.0,106.0] || equal(op(e2,e0),e4)** -> .
% 1.32/1.48  7509[11:MRR:7284.1,7505.0] ||  -> equal(op(e0,e0),e4)**.
% 1.32/1.48  7518[11:Rew:7509.0,7319.0] ||  -> equal(e4,e0) equal(op(e2,e0),e0)**.
% 1.32/1.48  7554[11:MRR:7518.0,4.0] ||  -> equal(op(e2,e0),e0)**.
% 1.32/1.48  7589[11:Rew:7214.0,325.4,7202.0,325.3,7224.0,325.2,7509.0,325.1,7554.0,325.0] ||  -> equal(e2,e0) equal(e4,e2)** equal(e3,e2) equal(e2,e1) equal(e2,e1).
% 1.32/1.48  7590[11:Obv:7589.3] ||  -> equal(e2,e0) equal(e4,e2)** equal(e3,e2) equal(e2,e1).
% 1.32/1.48  7591[11:MRR:7590.0,7590.1,7590.2,7590.3,2.0,9.0,8.0,5.0] ||  -> .
% 1.32/1.48  7592[7:Spt:7591.0,5854.0,5857.0] || equal(op(e1,e4),e3)** -> .
% 1.32/1.48  7593[7:Spt:7591.0,5854.1,5854.2] ||  -> equal(op(e1,e4),e2)** equal(op(e1,e4),e0).
% 1.32/1.48  7594[7:MRR:5620.3,7592.0] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3) equal(op(e2,e4),e3).
% 1.32/1.48  7595[7:MRR:5608.1,7592.0] ||  -> equal(op(e1,e3),e3)** equal(op(e1,e2),e3) equal(op(e1,e0),e3).
% 1.32/1.48  7596[8:Spt:7593.0] ||  -> equal(op(e1,e4),e2)**.
% 1.32/1.48  7600[8:Rew:7596.0,20.0] ||  -> equal(op(e1,e2),e4)**.
% 1.32/1.48  7601[8:Rew:7596.0,76.0] || equal(op(e0,e4),e2)** -> .
% 1.32/1.48  7603[8:Rew:7596.0,102.0] || equal(op(e1,e1),e2)** -> .
% 1.32/1.48  7604[8:Rew:7596.0,81.0] || equal(op(e3,e4),e2)** -> .
% 1.32/1.48  7605[8:Rew:7596.0,105.0] || equal(op(e1,e3),e2)** -> .
% 1.32/1.48  7610[8:Rew:7596.0,157.0] ||  -> equal(op(e2,op(e4,e1)),e4)**.
% 1.32/1.48  7611[8:Rew:7596.0,258.0] || equal(e2,e2) equal(op(e1,op(op(e1,e4),e1)),e3)** equal(op(op(e1,e4),e1),e0) -> .
% 1.32/1.48  7618[8:Rew:7600.0,97.0] || equal(op(e1,e0),e4)** -> .
% 1.32/1.48  7619[8:Rew:7600.0,100.0] || equal(op(e1,e1),e4)** -> .
% 1.32/1.48  7625[8:Rew:7600.0,143.0] ||  -> equal(op(op(e2,e1),e4),e1)**.
% 1.32/1.48  7626[8:Rew:7600.0,147.0] ||  -> equal(op(e4,op(e2,e1)),e2)**.
% 1.32/1.48  7631[8:Rew:7600.0,7595.1] ||  -> equal(op(e1,e3),e3)** equal(e4,e3) equal(op(e1,e0),e3).
% 1.32/1.48  7634[8:Rew:7600.0,272.0] || equal(e4,e4) equal(op(e1,op(op(e1,e2),e1)),e3)** equal(op(op(e1,e2),e1),e0) -> .
% 1.32/1.48  7639[8:MRR:5651.2,7601.0] ||  -> equal(op(e0,e2),e2)** equal(op(e0,e0),e2).
% 1.32/1.48  7643[8:MRR:5607.2,7603.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e1),e4)** equal(op(e1,e1),e0).
% 1.32/1.48  7644[8:MRR:5652.1,7603.0] ||  -> equal(op(e2,e1),e2) equal(op(e4,e1),e2)** equal(op(e3,e1),e2).
% 1.32/1.48  7646[8:MRR:296.2,7604.0] ||  -> equal(op(e3,e3),e2)** equal(op(e3,e2),e2) equal(op(e3,e1),e2) equal(op(e3,e0),e2).
% 1.32/1.48  7647[8:MRR:5655.3,7605.0] ||  -> equal(op(e3,e3),e2) equal(op(e2,e3),e2) equal(op(e4,e3),e2)**.
% 1.32/1.48  7654[8:MRR:321.4,7618.0] ||  -> equal(op(e4,e0),e4)** equal(op(e0,e0),e4) equal(op(e3,e0),e4) equal(op(e2,e0),e4).
% 1.32/1.48  7655[8:MRR:5562.1,7619.0] ||  -> equal(op(e4,e1),e4)** equal(op(e3,e1),e4) equal(op(e2,e1),e4).
% 1.32/1.48  7666[8:MRR:7631.1,10.0] ||  -> equal(op(e1,e3),e3)** equal(op(e1,e0),e3).
% 1.32/1.48  7667[8:MRR:7643.1,7619.0] ||  -> equal(op(e1,e1),e1)** equal(op(e1,e1),e0).
% 1.32/1.48  7672[8:Obv:7611.0] || equal(op(e1,op(op(e1,e4),e1)),e3)** equal(op(op(e1,e4),e1),e0) -> .
% 1.32/1.48  7673[8:Rew:7596.0,7672.1,7596.0,7672.0] || equal(op(e1,op(e2,e1)),e3)** equal(op(e2,e1),e0) -> .
% 1.32/1.48  7678[8:Obv:7634.0] || equal(op(e1,op(op(e1,e2),e1)),e3)** equal(op(op(e1,e2),e1),e0) -> .
% 1.32/1.48  7679[8:Rew:7600.0,7678.1,7600.0,7678.0] || equal(op(e1,op(e4,e1)),e3)** equal(op(e4,e1),e0) -> .
% 1.32/1.48  7688[9:Spt:340.0] ||  -> equal(op(e3,e0),e3)**.
% 1.32/1.48  7689[9:Rew:7688.0,26.0] ||  -> equal(op(e3,e3),e0)**.
% 1.32/1.48  7691[9:Rew:7688.0,5594.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  7703[9:Rew:7688.0,7646.3] ||  -> equal(op(e3,e3),e2)** equal(op(e3,e2),e2) equal(op(e3,e1),e2) equal(e3,e2).
% 1.32/1.48  7707[9:Rew:7688.0,7654.2] ||  -> equal(op(e4,e0),e4)** equal(op(e0,e0),e4) equal(e4,e3) equal(op(e2,e0),e4).
% 1.32/1.48  7719[9:Rew:7689.0,75.0] || equal(op(e4,e3),e0)** -> .
% 1.32/1.48  7727[9:Rew:7689.0,7647.0] ||  -> equal(e2,e0) equal(op(e2,e3),e2) equal(op(e4,e3),e2)**.
% 1.32/1.48  7743[9:Rew:7691.0,53.0] || equal(op(e2,e1),e0)** -> .
% 1.32/1.48  7745[9:Rew:7691.0,51.0] || equal(op(e1,e1),e0)** -> .
% 1.32/1.48  7754[9:Rew:7691.0,7644.2] ||  -> equal(op(e2,e1),e2) equal(op(e4,e1),e2)** equal(e2,e0).
% 1.32/1.48  7774[9:MRR:290.2,7719.0] ||  -> equal(op(e4,e4),e0)** equal(op(e4,e0),e0) equal(op(e4,e2),e0) equal(op(e4,e1),e0).
% 1.32/1.48  7780[9:MRR:5609.3,7743.0] ||  -> equal(op(e2,e1),e2) equal(op(e2,e1),e1) equal(op(e2,e1),e4)**.
% 1.32/1.48  7781[9:MRR:7667.1,7745.0] ||  -> equal(op(e1,e1),e1)**.
% 1.32/1.48  7784[9:Rew:7781.0,50.0] || equal(op(e2,e1),e1)** -> .
% 1.32/1.48  7816[9:MRR:7727.0,2.0] ||  -> equal(op(e2,e3),e2) equal(op(e4,e3),e2)**.
% 1.32/1.48  7818[9:MRR:7754.2,2.0] ||  -> equal(op(e2,e1),e2) equal(op(e4,e1),e2)**.
% 1.32/1.48  7825[9:MRR:7780.1,7784.0] ||  -> equal(op(e2,e1),e2) equal(op(e2,e1),e4)**.
% 1.32/1.48  7828[9:Rew:7691.0,7703.2,7689.0,7703.0] ||  -> equal(e2,e0) equal(op(e3,e2),e2)** equal(e2,e0) equal(e3,e2).
% 1.32/1.48  7829[9:Obv:7828.0] ||  -> equal(op(e3,e2),e2)** equal(e2,e0) equal(e3,e2).
% 1.32/1.48  7830[9:MRR:7829.1,7829.2,2.0,8.0] ||  -> equal(op(e3,e2),e2)**.
% 1.32/1.48  7833[9:Rew:7830.0,58.0] || equal(op(e0,e2),e2)** -> .
% 1.32/1.48  7844[9:MRR:7639.0,7833.0] ||  -> equal(op(e0,e0),e2)**.
% 1.32/1.48  7853[9:Rew:7844.0,136.0] ||  -> equal(op(e2,e2),e0)**.
% 1.32/1.48  7866[9:Rew:7853.0,23.0] ||  -> equal(op(e2,e0),e2)**.
% 1.32/1.48  7880[9:Rew:7866.0,108.0] || equal(op(e2,e3),e2)** -> .
% 1.32/1.48  7881[9:Rew:7866.0,106.0] || equal(op(e2,e1),e2)** -> .
% 1.32/1.48  7912[9:MRR:7816.0,7880.0] ||  -> equal(op(e4,e3),e2)**.
% 1.32/1.48  7915[9:Rew:7912.0,34.0] ||  -> equal(op(e4,e2),e3)**.
% 1.32/1.48  7963[9:MRR:7818.0,7881.0] ||  -> equal(op(e4,e1),e2)**.
% 1.32/1.48  7964[9:MRR:7825.0,7881.0] ||  -> equal(op(e2,e1),e4)**.
% 1.32/1.48  7981[9:Rew:7964.0,7625.0] ||  -> equal(op(e4,e4),e1)**.
% 1.32/1.48  8060[9:Rew:7866.0,7707.3,7844.0,7707.1] ||  -> equal(op(e4,e0),e4)** equal(e4,e2) equal(e4,e3) equal(e4,e2).
% 1.32/1.48  8061[9:Obv:8060.1] ||  -> equal(op(e4,e0),e4)** equal(e4,e3) equal(e4,e2).
% 1.32/1.48  8062[9:MRR:8061.1,8061.2,10.0,9.0] ||  -> equal(op(e4,e0),e4)**.
% 1.32/1.48  8075[9:Rew:7963.0,7774.3,7915.0,7774.2,8062.0,7774.1,7981.0,7774.0] ||  -> equal(e1,e0) equal(e4,e0)** equal(e3,e0) equal(e2,e0).
% 1.32/1.48  8076[9:MRR:8075.0,8075.1,8075.2,8075.3,1.0,4.0,3.0,2.0] ||  -> .
% 1.32/1.48  8114[9:Spt:8076.0,340.0,7688.0] || equal(op(e3,e0),e3)** -> .
% 1.32/1.48  8115[9:Spt:8076.0,340.1,340.2,340.3,340.4] ||  -> equal(op(e3,e0),e0) equal(op(e3,e0),e4)** equal(op(e3,e0),e2) equal(op(e3,e0),e1).
% 1.32/1.48  8117[9:MRR:5612.3,8114.0] ||  -> equal(op(e3,e3),e3) equal(op(e3,e4),e3)** equal(op(e3,e2),e3).
% 1.32/1.48  8118[10:Spt:8115.0] ||  -> equal(op(e3,e0),e0)**.
% 1.32/1.48  8121[10:Rew:8118.0,5593.0] ||  -> equal(op(e1,e0),e3)**.
% 1.32/1.48  8150[10:Rew:8121.0,5577.0] ||  -> equal(op(e3,e3),e0)**.
% 1.32/1.48  8151[10:Rew:8121.0,16.0] ||  -> equal(op(e1,e3),e0)**.
% 1.32/1.48  8164[10:Rew:8150.0,71.0] || equal(op(e1,e3),e0)** -> .
% 1.32/1.48  8207[10:Rew:8151.0,8164.0] || equal(e0,e0)* -> .
% 1.32/1.48  8208[10:Obv:8207.0] ||  -> .
% 1.32/1.48  8261[10:Spt:8208.0,8115.0,8118.0] || equal(op(e3,e0),e0)** -> .
% 1.32/1.48  8262[10:Spt:8208.0,8115.1,8115.2,8115.3] ||  -> equal(op(e3,e0),e4)** equal(op(e3,e0),e2) equal(op(e3,e0),e1).
% 1.32/1.48  8265[11:Spt:8262.0] ||  -> equal(op(e3,e0),e4)**.
% 1.32/1.48  8268[11:Rew:8265.0,26.0] ||  -> equal(op(e3,e4),e0)**.
% 1.32/1.48  8270[11:Rew:8265.0,5594.0] ||  -> equal(op(e4,e1),e0)**.
% 1.32/1.48  8300[11:Rew:8268.0,8117.1] ||  -> equal(op(e3,e3),e3)** equal(e3,e0) equal(op(e3,e2),e3).
% 1.32/1.48  8312[11:Rew:8270.0,7610.0] ||  -> equal(op(e2,e0),e4)**.
% 1.32/1.48  8321[11:Rew:8270.0,7679.0] || equal(op(e1,e0),e3) equal(op(e4,e1),e0)** -> .
% 1.32/1.48  8330[11:Rew:8270.0,52.0] || equal(op(e1,e1),e0)** -> .
% 1.32/1.48  8333[11:Rew:8312.0,21.0] ||  -> equal(op(e2,e4),e0)**.
% 1.32/1.48  8345[11:Rew:8312.0,5630.3] ||  -> equal(op(e2,e2),e1) equal(op(e2,e1),e1) equal(op(e2,e4),e1)** equal(e4,e1).
% 1.32/1.48  8414[11:MRR:7667.1,8330.0] ||  -> equal(op(e1,e1),e1)**.
% 1.32/1.48  8422[11:Rew:8414.0,50.0] || equal(op(e2,e1),e1)** -> .
% 1.32/1.48  8469[11:Rew:8270.0,8321.1] || equal(op(e1,e0),e3)** equal(e0,e0) -> .
% 1.32/1.48  8470[11:Obv:8469.1] || equal(op(e1,e0),e3)** -> .
% 1.32/1.48  8471[11:MRR:7666.1,8470.0] ||  -> equal(op(e1,e3),e3)**.
% 1.32/1.48  8478[11:Rew:8471.0,71.0] || equal(op(e3,e3),e3)** -> .
% 1.32/1.48  8526[11:MRR:8300.0,8300.1,8478.0,3.0] ||  -> equal(op(e3,e2),e3)**.
% 1.32/1.48  8528[11:Rew:8526.0,28.0] ||  -> equal(op(e3,e3),e2)**.
% 1.32/1.48  8543[11:Rew:8528.0,154.0] ||  -> equal(op(e2,e2),e3)**.
% 1.32/1.48  8598[11:Rew:8333.0,8345.2,8543.0,8345.0] ||  -> equal(e3,e1) equal(op(e2,e1),e1)** equal(e1,e0) equal(e4,e1).
% 1.32/1.48  8599[11:MRR:8598.0,8598.1,8598.2,8598.3,6.0,8422.0,1.0,7.0] ||  -> .
% 1.32/1.48  8638[11:Spt:8599.0,8262.0,8265.0] || equal(op(e3,e0),e4)** -> .
% 1.32/1.48  8639[11:Spt:8599.0,8262.1,8262.2] ||  -> equal(op(e3,e0),e2)** equal(op(e3,e0),e1).
% 1.32/1.48  8642[12:Spt:8639.0] ||  -> equal(op(e3,e0),e2)**.
% 1.32/1.48  8646[12:Rew:8642.0,5594.0] ||  -> equal(op(e2,e1),e0)**.
% 1.32/1.48  8648[12:Rew:8642.0,26.0] ||  -> equal(op(e3,e2),e0)**.
% 1.32/1.48  8665[12:Rew:8646.0,7626.0] ||  -> equal(op(e4,e0),e2)**.
% 1.32/1.48  8675[12:Rew:8646.0,7673.0] || equal(op(e1,e0),e3) equal(op(e2,e1),e0)** -> .
% 1.32/1.48  8681[12:Rew:8646.0,7655.2] ||  -> equal(op(e4,e1),e4)** equal(op(e3,e1),e4) equal(e4,e0).
% 1.32/1.48  8699[12:Rew:8648.0,8117.2] ||  -> equal(op(e3,e3),e3) equal(op(e3,e4),e3)** equal(e3,e0).
% 1.32/1.48  8706[12:Rew:8665.0,31.0] ||  -> equal(op(e4,e2),e0)**.
% 1.32/1.48  8728[12:Rew:8665.0,5623.3] ||  -> equal(op(e4,e4),e1)** equal(op(e4,e1),e1) equal(op(e4,e2),e1) equal(e2,e1).
% 1.32/1.48  8840[12:Rew:8646.0,8675.1] || equal(op(e1,e0),e3)** equal(e0,e0) -> .
% 1.32/1.48  8841[12:Obv:8840.1] || equal(op(e1,e0),e3)** -> .
% 1.32/1.48  8842[12:MRR:7666.1,8841.0] ||  -> equal(op(e1,e3),e3)**.
% 1.32/1.48  8849[12:Rew:8842.0,71.0] || equal(op(e3,e3),e3)** -> .
% 1.32/1.48  8897[12:MRR:8681.2,4.0] ||  -> equal(op(e4,e1),e4)** equal(op(e3,e1),e4).
% 1.32/1.48  8899[12:MRR:8699.0,8699.2,8849.0,3.0] ||  -> equal(op(e3,e4),e3)**.
% 1.32/1.48  8901[12:Rew:8899.0,30.0] ||  -> equal(op(e3,e3),e4)**.
% 1.32/1.48  8916[12:Rew:8901.0,121.0] || equal(op(e3,e1),e4)** -> .
% 1.32/1.48  8917[12:Rew:8901.0,154.0] ||  -> equal(op(e4,e4),e3)**.
% 1.32/1.48  8939[12:MRR:8897.1,8916.0] ||  -> equal(op(e4,e1),e4)**.
% 1.32/1.48  8986[12:Rew:8706.0,8728.2,8939.0,8728.1,8917.0,8728.0] ||  -> equal(e3,e1) equal(e4,e1)** equal(e1,e0) equal(e2,e1).
% 1.32/1.48  8987[12:MRR:8986.0,8986.1,8986.2,8986.3,6.0,7.0,1.0,5.0] ||  -> .
% 1.32/1.48  9017[12:Spt:8987.0,8639.0,8642.0] || equal(op(e3,e0),e2)** -> .
% 1.32/1.48  9018[12:Spt:8987.0,8639.1] ||  -> equal(op(e3,e0),e1)**.
% 1.32/1.48  9028[12:Rew:9018.0,5594.0] ||  -> equal(op(e1,e1),e0)**.
% 1.32/1.48  9032[12:Rew:9028.0,17.0] ||  -> equal(op(e1,e0),e1)**.
% 1.32/1.48  9036[12:Rew:9032.0,5577.0] ||  -> equal(op(e1,e3),e0)**.
% 1.32/1.48  9079[12:Rew:9032.0,7666.1,9036.0,7666.0] ||  -> equal(e3,e0) equal(e3,e1)**.
% 1.32/1.48  9080[12:MRR:9079.0,9079.1,3.0,6.0] ||  -> .
% 1.32/1.48  9143[8:Spt:9080.0,7593.0,7596.0] || equal(op(e1,e4),e2)** -> .
% 1.32/1.48  9144[8:Spt:9080.0,7593.1] ||  -> equal(op(e1,e4),e0)**.
% 1.32/1.48  9149[8:Rew:9144.0,20.0] ||  -> equal(op(e1,e0),e4)**.
% 1.32/1.48  9151[8:Rew:9149.0,5577.0] ||  -> equal(op(e4,e3),e0)**.
% 1.32/1.48  9152[8:Rew:9149.0,5578.0] ||  -> equal(op(e3,e4),e1)**.
% 1.32/1.48  9154[8:Rew:9151.0,34.0] ||  -> equal(op(e4,e0),e3)**.
% 1.32/1.48  9166[8:Rew:9152.0,30.0] ||  -> equal(op(e3,e1),e4)**.
% 1.32/1.48  9172[8:Rew:9152.0,7594.1] ||  -> equal(op(e4,e4),e3)** equal(e3,e1) equal(op(e2,e4),e3).
% 1.32/1.48  9177[8:Rew:9154.0,129.0] || equal(op(e4,e4),e3)** -> .
% 1.32/1.48  9182[8:Rew:9154.0,255.0] || equal(e3,e3) equal(op(e4,op(op(e4,e0),e4)),e2)** equal(op(op(e4,e0),e4),e1) -> .
% 1.32/1.48  9192[8:Rew:9149.0,41.0] || equal(op(e3,e0),e4)** -> .
% 1.32/1.48  9194[8:Rew:9154.0,45.0] || equal(op(e3,e0),e3)** -> .
% 1.32/1.48  9195[8:Rew:9152.0,119.0] || equal(op(e3,e0),e1)** -> .
% 1.32/1.48  9223[8:MRR:9172.0,9172.1,9177.0,6.0] ||  -> equal(op(e2,e4),e3)**.
% 1.32/1.48  9224[8:Rew:9223.0,25.0] ||  -> equal(op(e2,e3),e4)**.
% 1.32/1.48  9275[8:Rew:9151.0,5655.2,9224.0,5655.1] ||  -> equal(op(e3,e3),e2)** equal(e4,e2) equal(e2,e0) equal(op(e1,e3),e2).
% 1.32/1.48  9276[8:MRR:9275.1,9275.2,9.0,2.0] ||  -> equal(op(e3,e3),e2)** equal(op(e1,e3),e2).
% 1.32/1.48  9279[8:Rew:9166.0,5652.3] ||  -> equal(op(e2,e1),e2) equal(op(e1,e1),e2) equal(op(e4,e1),e2)** equal(e4,e2).
% 1.32/1.48  9280[8:MRR:9279.3,9.0] ||  -> equal(op(e2,e1),e2) equal(op(e1,e1),e2) equal(op(e4,e1),e2)**.
% 1.32/1.48  9285[8:Rew:9154.0,5622.1,9149.0,5622.0] ||  -> equal(e4,e1) equal(e3,e1) equal(op(e3,e0),e1)** equal(op(e2,e0),e1).
% 1.32/1.48  9286[8:MRR:9285.0,9285.1,9285.2,7.0,6.0,9195.0] ||  -> equal(op(e2,e0),e1)**.
% 1.32/1.48  9287[8:Rew:9286.0,21.0] ||  -> equal(op(e2,e1),e0)**.
% 1.32/1.48  9304[8:Rew:9287.0,9280.0] ||  -> equal(e2,e0) equal(op(e1,e1),e2) equal(op(e4,e1),e2)**.
% 1.32/1.48  9307[8:MRR:9304.0,2.0] ||  -> equal(op(e1,e1),e2) equal(op(e4,e1),e2)**.
% 1.32/1.48  9316[8:Obv:9182.0] || equal(op(e4,op(op(e4,e0),e4)),e2)** equal(op(op(e4,e0),e4),e1) -> .
% 1.32/1.48  9317[8:Rew:9152.0,9316.1,9154.0,9316.1,9152.0,9316.0,9154.0,9316.0] || equal(op(e4,e1),e2)** equal(e1,e1) -> .
% 1.32/1.48  9318[8:Obv:9317.1] || equal(op(e4,e1),e2)** -> .
% 1.32/1.48  9319[8:MRR:9307.1,9318.0] ||  -> equal(op(e1,e1),e2)**.
% 1.32/1.48  9324[8:Rew:9319.0,101.0] || equal(op(e1,e3),e2)** -> .
% 1.32/1.48  9361[8:MRR:9276.1,9324.0] ||  -> equal(op(e3,e3),e2)**.
% 1.32/1.48  9368[8:Rew:9361.0,118.0] || equal(op(e3,e0),e2)** -> .
% 1.32/1.48  9559[8:MRR:340.0,340.2,340.3,340.4,9194.0,9192.0,9368.0,9195.0] ||  -> equal(op(e3,e0),e0)**.
% 1.32/1.48  9562[8:Rew:9559.0,5594.0] ||  -> equal(op(e0,e1),e0)**.
% 1.32/1.48  9569[8:Rew:5564.0,9562.0] ||  -> equal(e3,e0)**.
% 1.32/1.48  9570[8:MRR:9569.0,3.0] ||  -> .
% 1.32/1.48  9571[4:Spt:9570.0,5561.0,5564.0] || equal(op(e0,e1),e3)** -> .
% 1.32/1.48  9572[4:Spt:9570.0,5561.1] ||  -> equal(op(e0,e1),e2)**.
% 1.32/1.48  9577[4:Rew:9572.0,12.0] ||  -> equal(op(e0,e2),e1)**.
% 1.32/1.48  9579[4:Rew:9577.0,94.0] || equal(op(e0,e4),e1)** -> .
% 1.32/1.48  9580[4:Rew:9577.0,56.0] || equal(op(e1,e2),e1)** -> .
% 1.32/1.48  9582[4:Rew:9577.0,57.0] || equal(op(e2,e2),e1)** -> .
% 1.32/1.48  9583[4:Rew:9577.0,87.0] || equal(op(e0,e0),e1)** -> .
% 1.32/1.48  9584[4:Rew:9577.0,59.0] || equal(op(e4,e2),e1)** -> .
% 1.32/1.48  9585[4:Rew:9572.0,92.0] || equal(op(e0,e4),e2)** -> .
% 1.32/1.48  9586[4:Rew:9572.0,91.0] || equal(op(e0,e3),e2)** -> .
% 1.32/1.48  9588[4:Rew:9572.0,86.0] || equal(op(e0,e0),e2)** -> .
% 1.32/1.48  9590[4:Rew:9572.0,48.0] || equal(op(e3,e1),e2)** -> .
% 1.32/1.48  9593[4:Rew:9577.0,93.0] || equal(op(e0,e3),e1)** -> .
% 1.32/1.48  9594[4:Rew:9577.0,138.0] ||  -> equal(op(op(e2,e0),e1),e0)**.
% 1.32/1.48  9595[4:Rew:9577.0,146.0] ||  -> equal(op(e1,op(e2,e0)),e2)**.
% 1.32/1.48  9597[4:Rew:9572.0,137.0] ||  -> equal(op(op(e1,e0),e2),e0)**.
% 1.32/1.48  9600[4:Rew:9577.0,5563.3] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e0),e4) equal(op(e0,e3),e4) equal(e4,e1).
% 1.32/1.48  9601[4:MRR:9600.3,7.0] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e0),e4) equal(op(e0,e3),e4).
% 1.32/1.48  9604[4:Rew:9577.0,168.2,9577.0,168.1,9577.0,168.0] || equal(e1,e1) equal(op(e0,op(e1,e0)),e3)** equal(op(e1,e0),e4) -> .
% 1.32/1.48  9605[4:Obv:9604.0] || equal(op(e0,op(e1,e0)),e3)** equal(op(e1,e0),e4) -> .
% 1.32/1.48  9610[4:Rew:9572.0,198.2,9572.0,198.1,9572.0,198.0] || equal(e2,e2) equal(op(e0,op(e2,e0)),e4)** equal(op(e2,e0),e3) -> .
% 1.32/1.48  9611[4:Obv:9610.0] || equal(op(e0,op(e2,e0)),e4)** equal(op(e2,e0),e3) -> .
% 1.32/1.48  9616[4:MRR:287.4,9579.0] ||  -> equal(op(e4,e4),e1)** equal(op(e1,e4),e1) equal(op(e3,e4),e1) equal(op(e2,e4),e1).
% 1.32/1.48  9617[4:MRR:308.0,9582.0] ||  -> equal(op(e2,e1),e1) equal(op(e2,e4),e1)** equal(op(e2,e3),e1) equal(op(e2,e0),e1).
% 1.32/1.48  9618[4:MRR:318.3,9580.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e4),e1)** equal(op(e1,e3),e1) equal(op(e1,e0),e1).
% 1.32/1.48  9621[4:MRR:327.1,9583.0] ||  -> equal(op(e1,e0),e1) equal(op(e4,e0),e1)** equal(op(e3,e0),e1) equal(op(e2,e0),e1).
% 1.32/1.48  9622[4:MRR:351.3,351.4,9585.0,9579.0] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e4),e0) equal(op(e0,e4),e3).
% 1.32/1.48  9623[4:Rew:9577.0,303.4] ||  -> equal(op(e3,e2),e3) equal(op(e2,e2),e3) equal(op(e4,e2),e3)** equal(op(e1,e2),e3) equal(e3,e1).
% 1.32/1.48  9624[4:MRR:9623.4,6.0] ||  -> equal(op(e3,e2),e3) equal(op(e2,e2),e3) equal(op(e4,e2),e3)** equal(op(e1,e2),e3).
% 1.32/1.48  9625[4:MRR:355.3,355.4,9588.0,9583.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e4)** equal(op(e0,e0),e3).
% 1.32/1.48  9627[4:MRR:339.3,9590.0] ||  -> equal(op(e3,e1),e3) equal(op(e3,e1),e1) equal(op(e3,e1),e4)** equal(op(e3,e1),e0).
% 1.32/1.48  9630[4:MRR:295.4,9586.0] ||  -> equal(op(e3,e3),e2) equal(op(e2,e3),e2) equal(op(e4,e3),e2)** equal(op(e1,e3),e2).
% 1.32/1.48  9631[4:MRR:352.3,352.4,9586.0,9593.0] ||  -> equal(op(e0,e3),e3) equal(op(e0,e3),e0) equal(op(e0,e3),e4)**.
% 1.32/1.48  9632[4:MRR:297.4,9593.0] ||  -> equal(op(e3,e3),e1) equal(op(e1,e3),e1) equal(op(e4,e3),e1)** equal(op(e2,e3),e1).
% 1.32/1.48  9633[4:Rew:9572.0,324.4,9577.0,324.3] ||  -> equal(op(e0,e3),e3) equal(op(e0,e0),e3) equal(op(e0,e4),e3)** equal(e3,e1) equal(e3,e2).
% 1.32/1.48  9634[4:MRR:9633.3,9633.4,6.0,8.0] ||  -> equal(op(e0,e3),e3) equal(op(e0,e0),e3) equal(op(e0,e4),e3)**.
% 1.32/1.48  9635[4:Rew:9572.0,313.4] ||  -> equal(op(e3,e1),e3) equal(op(e1,e1),e3) equal(op(e4,e1),e3)** equal(op(e2,e1),e3) equal(e3,e2).
% 1.32/1.48  9636[4:MRR:9635.4,8.0] ||  -> equal(op(e3,e1),e3) equal(op(e1,e1),e3) equal(op(e4,e1),e3)** equal(op(e2,e1),e3).
% 1.32/1.48  9639[4:Rew:9577.0,301.4] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e3,e2),e4) equal(op(e1,e2),e4) equal(e4,e1).
% 1.32/1.48  9640[4:MRR:9639.4,7.0] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e3,e2),e4) equal(op(e1,e2),e4).
% 1.32/1.48  9644[4:Rew:9577.0,309.1] ||  -> equal(op(e2,e2),e0) equal(e1,e0) equal(op(e4,e2),e0)** equal(op(e3,e2),e0) equal(op(e1,e2),e0).
% 1.32/1.48  9645[4:MRR:9644.1,1.0] ||  -> equal(op(e2,e2),e0) equal(op(e4,e2),e0)** equal(op(e3,e2),e0) equal(op(e1,e2),e0).
% 1.32/1.48  9649[4:MRR:325.1,9588.0] ||  -> equal(op(e2,e0),e2) equal(op(e4,e0),e2)** equal(op(e3,e0),e2) equal(op(e1,e0),e2).
% 1.32/1.48  9650[4:MRR:333.3,9584.0] ||  -> equal(op(e4,e2),e4)** equal(op(e4,e2),e2) equal(op(e4,e2),e3) equal(op(e4,e2),e0).
% 1.32/1.48  9654[5:Spt:342.0] ||  -> equal(op(e2,e3),e3)**.
% 1.32/1.48  9664[5:Rew:9654.0,153.0] ||  -> equal(op(e3,op(e3,e2)),e3)**.
% 1.32/1.48  9696[5:Rew:28.0,9664.0] ||  -> equal(e3,e2)**.
% 1.32/1.48  9697[5:MRR:9696.0,8.0] ||  -> .
% 1.32/1.48  9716[5:Spt:9697.0,342.0,9654.0] || equal(op(e2,e3),e3)** -> .
% 1.32/1.48  9717[5:Spt:9697.0,342.1,342.2,342.3,342.4] ||  -> equal(op(e2,e3),e2) equal(op(e2,e3),e4)** equal(op(e2,e3),e1) equal(op(e2,e3),e0).
% 1.32/1.48  9718[5:MRR:293.2,9716.0] ||  -> equal(op(e3,e3),e3) equal(op(e4,e3),e3)** equal(op(e1,e3),e3) equal(op(e0,e3),e3).
% 1.32/1.48  9720[6:Spt:9717.0] ||  -> equal(op(e2,e3),e2)**.
% 1.32/1.48  9722[6:Rew:9720.0,24.0] ||  -> equal(op(e2,e2),e3)**.
% 1.32/1.48  9732[6:Rew:9720.0,153.0] ||  -> equal(op(e2,op(e3,e2)),e3)**.
% 1.32/1.48  9753[6:Rew:9722.0,148.0] ||  -> equal(op(e3,e3),e2)**.
% 1.32/1.48  9757[6:Rew:9753.0,29.0] ||  -> equal(op(e3,e2),e3)**.
% 1.32/1.48  9809[6:Rew:9720.0,9732.0,9757.0,9732.0] ||  -> equal(e3,e2)**.
% 1.32/1.48  9810[6:MRR:9809.0,8.0] ||  -> .
% 1.32/1.48  9849[6:Spt:9810.0,9717.0,9720.0] || equal(op(e2,e3),e2)** -> .
% 1.32/1.48  9850[6:Spt:9810.0,9717.1,9717.2,9717.3] ||  -> equal(op(e2,e3),e4)** equal(op(e2,e3),e1) equal(op(e2,e3),e0).
% 1.32/1.48  9851[6:MRR:9630.1,9849.0] ||  -> equal(op(e3,e3),e2) equal(op(e4,e3),e2)** equal(op(e1,e3),e2).
% 1.32/1.48  9853[7:Spt:9850.0] ||  -> equal(op(e2,e3),e4)**.
% 1.32/1.48  9856[7:Rew:9853.0,24.0] ||  -> equal(op(e2,e4),e3)**.
% 1.32/1.48  9857[7:Rew:9853.0,74.0] || equal(op(e4,e3),e4)** -> .
% 1.32/1.48  9862[7:Rew:9853.0,108.0] || equal(op(e2,e0),e4)** -> .
% 1.32/1.48  9864[7:Rew:9853.0,67.0] || equal(op(e0,e3),e4)** -> .
% 1.32/1.48  9868[7:Rew:9853.0,268.0] || equal(e4,e4) equal(op(e2,op(op(e2,e3),e2)),e1)** equal(op(op(e2,e3),e2),e0) -> .
% 1.32/1.48  9871[7:Rew:9853.0,9632.3] ||  -> equal(op(e3,e3),e1) equal(op(e1,e3),e1) equal(op(e4,e3),e1)** equal(e4,e1).
% 1.32/1.48  9872[7:Rew:9853.0,9617.2] ||  -> equal(op(e2,e1),e1) equal(op(e2,e4),e1)** equal(e4,e1) equal(op(e2,e0),e1).
% 1.32/1.48  9881[7:Rew:9856.0,77.0] || equal(op(e0,e4),e3)** -> .
% 1.32/1.48  9882[7:Rew:9856.0,109.0] || equal(op(e2,e0),e3)** -> .
% 1.32/1.48  9884[7:Rew:9856.0,158.0] ||  -> equal(op(e3,op(e4,e2)),e4)**.
% 1.32/1.48  9898[7:MRR:282.1,9857.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e2),e4) equal(op(e4,e1),e4) equal(op(e4,e0),e4).
% 1.32/1.48  9908[7:MRR:345.2,9862.0] ||  -> equal(op(e2,e0),e2) equal(op(e2,e0),e0) equal(op(e2,e0),e3)** equal(op(e2,e0),e1).
% 1.32/1.48  9911[7:MRR:9601.2,9864.0] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e0),e4).
% 1.32/1.48  9912[7:MRR:9631.2,9864.0] ||  -> equal(op(e0,e3),e3)** equal(op(e0,e3),e0).
% 1.32/1.48  9920[7:MRR:9634.2,9881.0] ||  -> equal(op(e0,e3),e3)** equal(op(e0,e0),e3).
% 1.32/1.48  9927[7:MRR:9871.3,7.0] ||  -> equal(op(e3,e3),e1) equal(op(e1,e3),e1) equal(op(e4,e3),e1)**.
% 1.32/1.48  9928[7:Rew:9856.0,9872.1] ||  -> equal(op(e2,e1),e1)** equal(e3,e1) equal(e4,e1) equal(op(e2,e0),e1).
% 1.32/1.48  9929[7:MRR:9928.1,9928.2,6.0,7.0] ||  -> equal(op(e2,e1),e1)** equal(op(e2,e0),e1).
% 1.32/1.48  9932[7:MRR:9908.2,9882.0] ||  -> equal(op(e2,e0),e2)** equal(op(e2,e0),e0) equal(op(e2,e0),e1).
% 1.32/1.48  9935[7:Obv:9868.0] || equal(op(e2,op(op(e2,e3),e2)),e1)** equal(op(op(e2,e3),e2),e0) -> .
% 1.32/1.48  9936[7:Rew:9853.0,9935.1,9853.0,9935.0] || equal(op(e2,op(e4,e2)),e1)** equal(op(e4,e2),e0) -> .
% 1.32/1.48  9951[8:Spt:335.0] ||  -> equal(op(e4,e0),e4)**.
% 1.32/1.48  9952[8:Rew:9951.0,31.0] ||  -> equal(op(e4,e4),e0)**.
% 1.32/1.48  9984[8:Rew:9952.0,160.0] ||  -> equal(op(e0,e0),e4)**.
% 1.32/1.48  9989[8:Rew:9984.0,11.0] ||  -> equal(op(e0,e4),e0)**.
% 1.32/1.48  10005[8:Rew:9989.0,95.0] || equal(op(e0,e3),e0)** -> .
% 1.32/1.48  10029[8:MRR:9912.1,10005.0] ||  -> equal(op(e0,e3),e3)**.
% 1.32/1.48  10036[8:Rew:10029.0,151.0] ||  -> equal(op(e3,op(e3,e0)),e3)**.
% 1.32/1.48  10052[8:Rew:26.0,10036.0] ||  -> equal(e3,e0)**.
% 1.32/1.48  10053[8:MRR:10052.0,3.0] ||  -> .
% 1.32/1.48  10083[8:Spt:10053.0,335.0,9951.0] || equal(op(e4,e0),e4)** -> .
% 1.32/1.48  10084[8:Spt:10053.0,335.1,335.2,335.3,335.4] ||  -> equal(op(e4,e0),e0) equal(op(e4,e0),e3)** equal(op(e4,e0),e2) equal(op(e4,e0),e1).
% 1.32/1.48  10086[8:MRR:9898.3,10083.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e2),e4) equal(op(e4,e1),e4).
% 1.32/1.48  10087[9:Spt:10084.0] ||  -> equal(op(e4,e0),e0)**.
% 1.32/1.48  10098[9:Rew:10087.0,140.0] ||  -> equal(op(e0,op(e0,e4)),e0)**.
% 1.32/1.48  10128[9:Rew:15.0,10098.0] ||  -> equal(e4,e0)**.
% 1.32/1.48  10129[9:MRR:10128.0,4.0] ||  -> .
% 1.32/1.48  10136[9:Spt:10129.0,10084.0,10087.0] || equal(op(e4,e0),e0)** -> .
% 1.32/1.48  10137[9:Spt:10129.0,10084.1,10084.2,10084.3] ||  -> equal(op(e4,e0),e3)** equal(op(e4,e0),e2) equal(op(e4,e0),e1).
% 1.32/1.48  10140[10:Spt:10137.0] ||  -> equal(op(e4,e0),e3)**.
% 1.32/1.48  10149[10:Rew:10140.0,39.0] || equal(op(e0,e0),e3)** -> .
% 1.32/1.48  10188[10:MRR:9920.1,10149.0] ||  -> equal(op(e0,e3),e3)**.
% 1.32/1.48  10198[10:Rew:10188.0,151.0] ||  -> equal(op(e3,op(e3,e0)),e3)**.
% 1.32/1.48  10214[10:Rew:26.0,10198.0] ||  -> equal(e3,e0)**.
% 1.32/1.48  10215[10:MRR:10214.0,3.0] ||  -> .
% 1.32/1.48  10253[10:Spt:10215.0,10137.0,10140.0] || equal(op(e4,e0),e3)** -> .
% 1.32/1.48  10254[10:Spt:10215.0,10137.1,10137.2] ||  -> equal(op(e4,e0),e2)** equal(op(e4,e0),e1).
% 1.32/1.48  10257[11:Spt:10254.0] ||  -> equal(op(e4,e0),e2)**.
% 1.32/1.48  10261[11:Rew:10257.0,31.0] ||  -> equal(op(e4,e2),e0)**.
% 1.32/1.48  10267[11:Rew:10257.0,44.0] || equal(op(e2,e0),e2)** -> .
% 1.32/1.48  10269[11:Rew:10257.0,128.0] || equal(op(e4,e3),e2)** -> .
% 1.32/1.48  10280[11:Rew:10261.0,62.0] || equal(op(e1,e2),e0)** -> .
% 1.32/1.48  10285[11:Rew:10261.0,9884.0] ||  -> equal(op(e3,e0),e4)**.
% 1.32/1.48  10288[11:Rew:10261.0,10086.1] ||  -> equal(op(e4,e4),e4)** equal(e4,e0) equal(op(e4,e1),e4).
% 1.32/1.48  10291[11:Rew:10261.0,9936.0] || equal(op(e2,e0),e1) equal(op(e4,e2),e0)** -> .
% 1.32/1.48  10311[11:Rew:10285.0,38.0] || equal(op(e0,e0),e4)** -> .
% 1.32/1.48  10346[11:MRR:9932.0,10267.0] ||  -> equal(op(e2,e0),e0) equal(op(e2,e0),e1)**.
% 1.32/1.48  10357[11:MRR:9851.1,10269.0] ||  -> equal(op(e3,e3),e2)** equal(op(e1,e3),e2).
% 1.32/1.48  10362[11:MRR:320.4,10280.0] ||  -> equal(op(e1,e1),e0) equal(op(e1,e0),e0) equal(op(e1,e4),e0)** equal(op(e1,e3),e0).
% 1.32/1.48  10370[11:MRR:9911.1,10311.0] ||  -> equal(op(e0,e4),e4)**.
% 1.32/1.48  10376[11:Rew:10370.0,79.0] || equal(op(e4,e4),e4)** -> .
% 1.32/1.48  10388[11:Rew:10261.0,10291.1] || equal(op(e2,e0),e1)** equal(e0,e0) -> .
% 1.32/1.48  10389[11:Obv:10388.1] || equal(op(e2,e0),e1)** -> .
% 1.32/1.48  10391[11:MRR:10346.1,10389.0] ||  -> equal(op(e2,e0),e0)**.
% 1.32/1.48  10405[11:Rew:10391.0,40.0] || equal(op(e1,e0),e0)** -> .
% 1.32/1.48  10452[11:MRR:10288.0,10288.1,10376.0,4.0] ||  -> equal(op(e4,e1),e4)**.
% 1.32/1.48  10453[11:Rew:10452.0,32.0] ||  -> equal(op(e4,e4),e1)**.
% 1.32/1.48  10469[11:Rew:10453.0,160.0] ||  -> equal(op(e1,e1),e4)**.
% 1.32/1.48  10470[11:Rew:10453.0,135.0] || equal(op(e4,e3),e1)** -> .
% 1.32/1.48  10474[11:Rew:10469.0,17.0] ||  -> equal(op(e1,e4),e1)**.
% 1.32/1.48  10486[11:Rew:10474.0,105.0] || equal(op(e1,e3),e1)** -> .
% 1.32/1.48  10497[11:MRR:9927.2,10470.0] ||  -> equal(op(e3,e3),e1)** equal(op(e1,e3),e1).
% 1.32/1.48  10503[11:MRR:10497.1,10486.0] ||  -> equal(op(e3,e3),e1)**.
% 1.32/1.48  10512[11:Rew:10503.0,10357.0] ||  -> equal(e2,e1) equal(op(e1,e3),e2)**.
% 1.32/1.48  10524[11:MRR:10512.0,5.0] ||  -> equal(op(e1,e3),e2)**.
% 1.32/1.48  10576[11:Rew:10524.0,10362.3,10474.0,10362.2,10469.0,10362.0] ||  -> equal(e4,e0) equal(op(e1,e0),e0)** equal(e1,e0) equal(e2,e0).
% 1.32/1.48  10577[11:MRR:10576.0,10576.1,10576.2,10576.3,4.0,10405.0,1.0,2.0] ||  -> .
% 1.32/1.48  10615[11:Spt:10577.0,10254.0,10257.0] || equal(op(e4,e0),e2)** -> .
% 1.32/1.48  10616[11:Spt:10577.0,10254.1] ||  -> equal(op(e4,e0),e1)**.
% 1.32/1.48  10626[11:Rew:10616.0,44.0] || equal(op(e2,e0),e1)** -> .
% 1.32/1.48  10642[11:MRR:9929.1,10626.0] ||  -> equal(op(e2,e1),e1)**.
% 1.32/1.48  10653[11:Rew:10642.0,143.0] ||  -> equal(op(e1,op(e1,e2)),e1)**.
% 1.32/1.48  10654[11:Rew:18.0,10653.0] ||  -> equal(e2,e1)**.
% 1.32/1.48  10655[11:MRR:10654.0,5.0] ||  -> .
% 1.32/1.48  10707[7:Spt:10655.0,9850.0,9853.0] || equal(op(e2,e3),e4)** -> .
% 1.32/1.48  10708[7:Spt:10655.0,9850.1,9850.2] ||  -> equal(op(e2,e3),e1)** equal(op(e2,e3),e0).
% 1.32/1.48  10709[7:MRR:302.2,10707.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4) equal(op(e2,e1),e4) equal(op(e2,e0),e4).
% 1.32/1.48  10710[7:MRR:291.2,10707.0] ||  -> equal(op(e4,e3),e4)** equal(op(e3,e3),e4) equal(op(e1,e3),e4) equal(op(e0,e3),e4).
% 1.32/1.48  10711[8:Spt:10708.0] ||  -> equal(op(e2,e3),e1)**.
% 1.32/1.48  10715[8:Rew:10711.0,24.0] ||  -> equal(op(e2,e1),e3)**.
% 1.32/1.48  10718[8:Rew:10711.0,108.0] || equal(op(e2,e0),e1)** -> .
% 1.32/1.48  10721[8:Rew:10711.0,70.0] || equal(op(e1,e3),e1)** -> .
% 1.32/1.48  10722[8:Rew:10711.0,115.0] || equal(op(e2,e4),e1)** -> .
% 1.32/1.48  10727[8:Rew:10711.0,165.0] || equal(e1,e1) equal(op(e2,op(op(e2,e3),e2)),e0)** equal(op(op(e2,e3),e2),e4) -> .
% 1.32/1.48  10728[8:Rew:10711.0,299.3] ||  -> equal(op(e3,e3),e0) equal(op(e0,e3),e0) equal(op(e4,e3),e0)** equal(e1,e0) equal(op(e1,e3),e0).
% 1.32/1.48  10735[8:Rew:10715.0,53.0] || equal(op(e3,e1),e3)** -> .
% 1.32/1.48  10736[8:Rew:10715.0,106.0] || equal(op(e2,e0),e3)** -> .
% 1.32/1.48  10738[8:Rew:10715.0,110.0] || equal(op(e2,e2),e3)** -> .
% 1.32/1.48  10739[8:Rew:10715.0,112.0] || equal(op(e2,e4),e3)** -> .
% 1.32/1.48  10740[8:Rew:10715.0,143.0] ||  -> equal(op(e3,op(e1,e2)),e1)**.
% 1.32/1.48  10741[8:Rew:10715.0,147.0] ||  -> equal(op(op(e1,e2),e3),e2)**.
% 1.32/1.48  10744[8:Rew:10715.0,10709.2] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4) equal(e4,e3) equal(op(e2,e0),e4).
% 1.32/1.48  10747[8:Rew:10715.0,5562.3] ||  -> equal(op(e4,e1),e4)** equal(op(e1,e1),e4) equal(op(e3,e1),e4) equal(e4,e3).
% 1.32/1.48  10748[8:Rew:10715.0,426.3] ||  -> equal(op(e1,e1),e1) equal(op(e4,e1),e1)** equal(op(e3,e1),e1) equal(e3,e1).
% 1.32/1.48  10751[8:Rew:10715.0,576.3] ||  -> equal(op(e1,e1),e0) equal(op(e4,e1),e0)** equal(op(e3,e1),e0) equal(e3,e0).
% 1.32/1.48  10753[8:MRR:9621.3,10718.0] ||  -> equal(op(e1,e0),e1) equal(op(e4,e0),e1)** equal(op(e3,e0),e1).
% 1.32/1.48  10754[8:MRR:345.4,10718.0] ||  -> equal(op(e2,e0),e2) equal(op(e2,e0),e0) equal(op(e2,e0),e4)** equal(op(e2,e0),e3).
% 1.32/1.48  10757[8:MRR:9618.2,10721.0] ||  -> equal(op(e1,e1),e1) equal(op(e1,e4),e1)** equal(op(e1,e0),e1).
% 1.32/1.48  10759[8:MRR:9616.3,10722.0] ||  -> equal(op(e4,e4),e1)** equal(op(e1,e4),e1) equal(op(e3,e4),e1).
% 1.32/1.48  10760[8:MRR:341.3,10722.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e4),e2) equal(op(e2,e4),e3) equal(op(e2,e4),e0).
% 1.32/1.48  10765[8:MRR:9627.0,10735.0] ||  -> equal(op(e3,e1),e1) equal(op(e3,e1),e4)** equal(op(e3,e1),e0).
% 1.32/1.48  10767[8:MRR:323.3,10736.0] ||  -> equal(op(e3,e0),e3) equal(op(e0,e0),e3) equal(op(e4,e0),e3)** equal(op(e1,e0),e3).
% 1.32/1.48  10770[8:MRR:9624.1,10738.0] ||  -> equal(op(e3,e2),e3) equal(op(e4,e2),e3)** equal(op(e1,e2),e3).
% 1.32/1.48  10772[8:MRR:283.2,10739.0] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3) equal(op(e1,e4),e3) equal(op(e0,e4),e3).
% 1.32/1.48  10773[8:MRR:10744.2,10.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4) equal(op(e2,e0),e4).
% 1.32/1.48  10774[8:MRR:10747.3,10.0] ||  -> equal(op(e4,e1),e4)** equal(op(e1,e1),e4) equal(op(e3,e1),e4).
% 1.32/1.48  10775[8:MRR:10748.3,6.0] ||  -> equal(op(e1,e1),e1) equal(op(e4,e1),e1)** equal(op(e3,e1),e1).
% 1.32/1.48  10776[8:MRR:10751.3,3.0] ||  -> equal(op(e1,e1),e0) equal(op(e4,e1),e0)** equal(op(e3,e1),e0).
% 1.32/1.48  10777[8:MRR:10754.3,10736.0] ||  -> equal(op(e2,e0),e2) equal(op(e2,e0),e0) equal(op(e2,e0),e4)**.
% 1.32/1.48  10778[8:MRR:10760.2,10739.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e4),e2) equal(op(e2,e4),e0).
% 1.32/1.48  10781[8:Obv:10727.0] || equal(op(e2,op(op(e2,e3),e2)),e0)** equal(op(op(e2,e3),e2),e4) -> .
% 1.32/1.48  10782[8:Rew:10711.0,10781.1,10711.0,10781.0] || equal(op(e2,op(e1,e2)),e0)** equal(op(e1,e2),e4) -> .
% 1.32/1.48  10787[8:MRR:10728.3,1.0] ||  -> equal(op(e3,e3),e0) equal(op(e0,e3),e0) equal(op(e4,e3),e0)** equal(op(e1,e3),e0).
% 1.32/1.48  10791[9:Spt:346.0] ||  -> equal(op(e1,e4),e4)**.
% 1.32/1.48  10812[9:Rew:10791.0,157.0] ||  -> equal(op(e4,op(e4,e1)),e4)**.
% 1.32/1.48  10835[9:Rew:32.0,10812.0] ||  -> equal(e4,e1)**.
% 1.32/1.48  10836[9:MRR:10835.0,7.0] ||  -> .
% 1.32/1.48  10847[9:Spt:10836.0,346.0,10791.0] || equal(op(e1,e4),e4)** -> .
% 1.32/1.48  10848[9:Spt:10836.0,346.1,346.2,346.3,346.4] ||  -> equal(op(e1,e4),e1) equal(op(e1,e4),e3)** equal(op(e1,e4),e2) equal(op(e1,e4),e0).
% 1.32/1.48  10851[10:Spt:10848.0] ||  -> equal(op(e1,e4),e1)**.
% 1.32/1.48  10853[10:Rew:10851.0,20.0] ||  -> equal(op(e1,e1),e4)**.
% 1.32/1.48  10855[10:Rew:10851.0,99.0] || equal(op(e1,e0),e1)** -> .
% 1.32/1.48  10882[10:Rew:10853.0,142.0] ||  -> equal(op(e4,e4),e1)**.
% 1.32/1.48  10886[10:Rew:10853.0,10775.0] ||  -> equal(e4,e1) equal(op(e4,e1),e1)** equal(op(e3,e1),e1).
% 1.32/1.48  10887[10:Rew:10882.0,35.0] ||  -> equal(op(e4,e1),e4)**.
% 1.32/1.48  10893[10:Rew:10882.0,129.0] || equal(op(e4,e0),e1)** -> .
% 1.32/1.48  10910[10:MRR:10753.0,10855.0] ||  -> equal(op(e4,e0),e1)** equal(op(e3,e0),e1).
% 1.32/1.48  10934[10:MRR:10910.0,10893.0] ||  -> equal(op(e3,e0),e1)**.
% 1.32/1.48  10935[10:Rew:10934.0,26.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  10974[10:Rew:10935.0,10886.2,10887.0,10886.1] ||  -> equal(e4,e1)** equal(e4,e1)** equal(e1,e0).
% 1.32/1.48  10975[10:Obv:10974.0] ||  -> equal(e4,e1)** equal(e1,e0).
% 1.32/1.48  10976[10:MRR:10975.0,10975.1,7.0,1.0] ||  -> .
% 1.32/1.48  11017[10:Spt:10976.0,10848.0,10851.0] || equal(op(e1,e4),e1)** -> .
% 1.32/1.48  11018[10:Spt:10976.0,10848.1,10848.2,10848.3] ||  -> equal(op(e1,e4),e3)** equal(op(e1,e4),e2) equal(op(e1,e4),e0).
% 1.32/1.48  11019[10:MRR:10757.1,11017.0] ||  -> equal(op(e1,e1),e1)** equal(op(e1,e0),e1).
% 1.32/1.48  11020[10:MRR:10759.1,11017.0] ||  -> equal(op(e4,e4),e1)** equal(op(e3,e4),e1).
% 1.32/1.48  11021[11:Spt:11018.0] ||  -> equal(op(e1,e4),e3)**.
% 1.32/1.48  11024[11:Rew:11021.0,20.0] ||  -> equal(op(e1,e3),e4)**.
% 1.32/1.48  11026[11:Rew:11021.0,76.0] || equal(op(e0,e4),e3)** -> .
% 1.32/1.48  11030[11:Rew:11021.0,104.0] || equal(op(e1,e2),e3)** -> .
% 1.32/1.48  11031[11:Rew:11021.0,99.0] || equal(op(e1,e0),e3)** -> .
% 1.32/1.48  11034[11:Rew:11021.0,157.0] ||  -> equal(op(e3,op(e4,e1)),e4)**.
% 1.32/1.48  11036[11:Rew:11021.0,260.0] || equal(e3,e3) equal(op(e1,op(op(e1,e4),e1)),e2)** equal(op(op(e1,e4),e1),e0) -> .
% 1.32/1.48  11046[11:Rew:11024.0,66.0] || equal(op(e0,e3),e4)** -> .
% 1.32/1.48  11047[11:Rew:11024.0,71.0] || equal(op(e3,e3),e4)** -> .
% 1.32/1.48  11049[11:Rew:11024.0,103.0] || equal(op(e1,e2),e4)** -> .
% 1.32/1.48  11053[11:Rew:11024.0,9851.2] ||  -> equal(op(e3,e3),e2) equal(op(e4,e3),e2)** equal(e4,e2).
% 1.32/1.48  11054[11:Rew:11024.0,9718.2] ||  -> equal(op(e3,e3),e3) equal(op(e4,e3),e3)** equal(e4,e3) equal(op(e0,e3),e3).
% 1.32/1.48  11061[11:Rew:11024.0,101.0] || equal(op(e1,e1),e4)** -> .
% 1.32/1.48  11062[11:Rew:11024.0,152.0] ||  -> equal(op(e4,op(e3,e1)),e3)**.
% 1.32/1.48  11063[11:Rew:11024.0,144.0] ||  -> equal(op(op(e3,e1),e4),e1)**.
% 1.32/1.48  11067[11:MRR:9622.2,11026.0] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e4),e0).
% 1.32/1.48  11071[11:MRR:10770.2,11030.0] ||  -> equal(op(e3,e2),e3) equal(op(e4,e2),e3)**.
% 1.32/1.48  11073[11:MRR:10767.3,11031.0] ||  -> equal(op(e3,e0),e3) equal(op(e0,e0),e3) equal(op(e4,e0),e3)**.
% 1.32/1.48  11076[11:MRR:9601.2,11046.0] ||  -> equal(op(e0,e4),e4)** equal(op(e0,e0),e4).
% 1.32/1.48  11078[11:MRR:292.1,11047.0] ||  -> equal(op(e3,e4),e4)** equal(op(e3,e2),e4) equal(op(e3,e1),e4) equal(op(e3,e0),e4).
% 1.32/1.48  11081[11:MRR:9640.3,11049.0] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e3,e2),e4).
% 1.32/1.48  11083[11:MRR:10774.1,11061.0] ||  -> equal(op(e4,e1),e4)** equal(op(e3,e1),e4).
% 1.32/1.48  11085[11:MRR:11053.2,9.0] ||  -> equal(op(e3,e3),e2) equal(op(e4,e3),e2)**.
% 1.32/1.48  11090[11:MRR:11054.2,10.0] ||  -> equal(op(e3,e3),e3) equal(op(e4,e3),e3)** equal(op(e0,e3),e3).
% 1.32/1.48  11095[11:Obv:11036.0] || equal(op(e1,op(op(e1,e4),e1)),e2)** equal(op(op(e1,e4),e1),e0) -> .
% 1.32/1.48  11096[11:Rew:11021.0,11095.1,11021.0,11095.0] || equal(op(e1,op(e3,e1)),e2)** equal(op(e3,e1),e0) -> .
% 1.32/1.48  11105[12:Spt:340.0] ||  -> equal(op(e3,e0),e3)**.
% 1.32/1.48  11106[12:Rew:11105.0,26.0] ||  -> equal(op(e3,e3),e0)**.
% 1.32/1.48  11113[12:Rew:11105.0,117.0] || equal(op(e3,e2),e3)** -> .
% 1.32/1.48  11136[12:Rew:11106.0,154.0] ||  -> equal(op(e0,e0),e3)**.
% 1.32/1.48  11141[12:Rew:11106.0,11090.0] ||  -> equal(e3,e0) equal(op(e4,e3),e3)** equal(op(e0,e3),e3).
% 1.32/1.48  11144[12:Rew:11136.0,11.0] ||  -> equal(op(e0,e3),e0)**.
% 1.32/1.48  11163[12:MRR:11071.0,11113.0] ||  -> equal(op(e4,e2),e3)**.
% 1.32/1.48  11165[12:Rew:11163.0,33.0] ||  -> equal(op(e4,e3),e2)**.
% 1.32/1.48  11234[12:Rew:11144.0,11141.2,11165.0,11141.1] ||  -> equal(e3,e0) equal(e3,e2)** equal(e3,e0).
% 1.32/1.48  11235[12:Obv:11234.0] ||  -> equal(e3,e2)** equal(e3,e0).
% 1.32/1.48  11236[12:MRR:11235.0,11235.1,8.0,3.0] ||  -> .
% 1.32/1.48  11271[12:Spt:11236.0,340.0,11105.0] || equal(op(e3,e0),e3)** -> .
% 1.32/1.48  11272[12:Spt:11236.0,340.1,340.2,340.3,340.4] ||  -> equal(op(e3,e0),e0) equal(op(e3,e0),e4)** equal(op(e3,e0),e2) equal(op(e3,e0),e1).
% 1.32/1.48  11274[12:MRR:11073.0,11271.0] ||  -> equal(op(e0,e0),e3) equal(op(e4,e0),e3)**.
% 1.32/1.48  11275[13:Spt:11272.0] ||  -> equal(op(e3,e0),e0)**.
% 1.32/1.48  11287[13:Rew:11275.0,139.0] ||  -> equal(op(e0,op(e0,e3)),e0)**.
% 1.32/1.48  11316[13:Rew:14.0,11287.0] ||  -> equal(e3,e0)**.
% 1.32/1.48  11317[13:MRR:11316.0,3.0] ||  -> .
% 1.32/1.48  11324[13:Spt:11317.0,11272.0,11275.0] || equal(op(e3,e0),e0)** -> .
% 1.32/1.48  11325[13:Spt:11317.0,11272.1,11272.2,11272.3] ||  -> equal(op(e3,e0),e4)** equal(op(e3,e0),e2) equal(op(e3,e0),e1).
% 1.32/1.48  11328[14:Spt:11325.0] ||  -> equal(op(e3,e0),e4)**.
% 1.32/1.48  11331[14:Rew:11328.0,26.0] ||  -> equal(op(e3,e4),e0)**.
% 1.32/1.48  11334[14:Rew:11328.0,116.0] || equal(op(e3,e1),e4)** -> .
% 1.32/1.48  11336[14:Rew:11328.0,43.0] || equal(op(e2,e0),e4)** -> .
% 1.32/1.48  11339[14:Rew:11328.0,38.0] || equal(op(e0,e0),e4)** -> .
% 1.32/1.48  11351[14:Rew:11328.0,9649.2] ||  -> equal(op(e2,e0),e2) equal(op(e4,e0),e2)** equal(e4,e2) equal(op(e1,e0),e2).
% 1.32/1.48  11363[14:Rew:11331.0,122.0] || equal(op(e3,e1),e0)** -> .
% 1.32/1.48  11373[14:MRR:11083.1,11334.0] ||  -> equal(op(e4,e1),e4)**.
% 1.32/1.48  11374[14:MRR:10765.1,11334.0] ||  -> equal(op(e3,e1),e1)** equal(op(e3,e1),e0).
% 1.32/1.48  11377[14:Rew:11373.0,32.0] ||  -> equal(op(e4,e4),e1)**.
% 1.32/1.48  11384[14:Rew:11373.0,290.4] ||  -> equal(op(e4,e4),e0)** equal(op(e4,e0),e0) equal(op(e4,e3),e0) equal(op(e4,e2),e0) equal(e4,e0).
% 1.32/1.48  11391[14:Rew:11373.0,130.0] || equal(op(e4,e2),e4)** -> .
% 1.32/1.48  11407[14:MRR:10773.2,11336.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e2),e4).
% 1.32/1.48  11408[14:MRR:10777.2,11336.0] ||  -> equal(op(e2,e0),e2)** equal(op(e2,e0),e0).
% 1.32/1.48  11411[14:MRR:11076.1,11339.0] ||  -> equal(op(e0,e4),e4)**.
% 1.32/1.48  11419[14:Rew:11411.0,77.0] || equal(op(e2,e4),e4)** -> .
% 1.32/1.48  11431[14:MRR:9650.0,11391.0] ||  -> equal(op(e4,e2),e2) equal(op(e4,e2),e3)** equal(op(e4,e2),e0).
% 1.32/1.48  11439[14:MRR:11374.1,11363.0] ||  -> equal(op(e3,e1),e1)**.
% 1.32/1.48  11443[14:Rew:11439.0,51.0] || equal(op(e1,e1),e1)** -> .
% 1.32/1.48  11454[14:MRR:11019.0,11443.0] ||  -> equal(op(e1,e0),e1)**.
% 1.32/1.48  11458[14:Rew:11454.0,9597.0] ||  -> equal(op(e1,e2),e0)**.
% 1.32/1.48  11492[14:Rew:11458.0,62.0] || equal(op(e4,e2),e0)** -> .
% 1.32/1.48  11506[14:MRR:11407.0,11419.0] ||  -> equal(op(e2,e2),e4)**.
% 1.32/1.48  11508[14:Rew:11506.0,23.0] ||  -> equal(op(e2,e4),e2)**.
% 1.32/1.48  11518[14:Rew:11508.0,109.0] || equal(op(e2,e0),e2)** -> .
% 1.32/1.48  11528[14:MRR:11408.0,11518.0] ||  -> equal(op(e2,e0),e0)**.
% 1.32/1.48  11571[14:MRR:11431.2,11492.0] ||  -> equal(op(e4,e2),e2) equal(op(e4,e2),e3)**.
% 1.32/1.48  11574[14:Rew:11454.0,11351.3,11528.0,11351.0] ||  -> equal(e2,e0) equal(op(e4,e0),e2)** equal(e4,e2) equal(e2,e1).
% 1.32/1.48  11575[14:MRR:11574.0,11574.2,11574.3,2.0,9.0,5.0] ||  -> equal(op(e4,e0),e2)**.
% 1.32/1.48  11577[14:Rew:11575.0,127.0] || equal(op(e4,e2),e2)** -> .
% 1.32/1.48  11587[14:MRR:11571.0,11577.0] ||  -> equal(op(e4,e2),e3)**.
% 1.32/1.48  11589[14:Rew:11587.0,33.0] ||  -> equal(op(e4,e3),e2)**.
% 1.32/1.48  11675[14:Rew:11587.0,11384.3,11589.0,11384.2,11575.0,11384.1,11377.0,11384.0] ||  -> equal(e1,e0) equal(e2,e0) equal(e2,e0) equal(e3,e0) equal(e4,e0)**.
% 1.32/1.48  11676[14:Obv:11675.1] ||  -> equal(e1,e0) equal(e2,e0) equal(e3,e0) equal(e4,e0)**.
% 1.32/1.48  11677[14:MRR:11676.0,11676.1,11676.2,11676.3,1.0,2.0,3.0,4.0] ||  -> .
% 1.32/1.48  11678[14:Spt:11677.0,11325.0,11328.0] || equal(op(e3,e0),e4)** -> .
% 1.32/1.48  11679[14:Spt:11677.0,11325.1,11325.2] ||  -> equal(op(e3,e0),e2)** equal(op(e3,e0),e1).
% 1.32/1.48  11681[14:MRR:11078.3,11678.0] ||  -> equal(op(e3,e4),e4)** equal(op(e3,e2),e4) equal(op(e3,e1),e4).
% 1.32/1.48  11682[15:Spt:11679.0] ||  -> equal(op(e3,e0),e2)**.
% 1.32/1.48  11686[15:Rew:11682.0,26.0] ||  -> equal(op(e3,e2),e0)**.
% 1.32/1.48  11689[15:Rew:11682.0,118.0] || equal(op(e3,e3),e2)** -> .
% 1.32/1.48  11696[15:Rew:11682.0,139.0] ||  -> equal(op(e2,op(e0,e3)),e0)**.
% 1.32/1.48  11719[15:Rew:11686.0,11681.1] ||  -> equal(op(e3,e4),e4)** equal(e4,e0) equal(op(e3,e1),e4).
% 1.32/1.48  11726[15:MRR:11085.0,11689.0] ||  -> equal(op(e4,e3),e2)**.
% 1.32/1.48  11730[15:Rew:11726.0,34.0] ||  -> equal(op(e4,e2),e3)**.
% 1.32/1.48  11741[15:Rew:11726.0,290.2] ||  -> equal(op(e4,e4),e0)** equal(op(e4,e0),e0) equal(e2,e0) equal(op(e4,e2),e0) equal(op(e4,e1),e0).
% 1.32/1.48  11753[15:Rew:11730.0,127.0] || equal(op(e4,e0),e3)** -> .
% 1.32/1.48  11795[15:MRR:11274.1,11753.0] ||  -> equal(op(e0,e0),e3)**.
% 1.32/1.48  11798[15:Rew:11795.0,11.0] ||  -> equal(op(e0,e3),e0)**.
% 1.32/1.48  11813[15:Rew:11798.0,95.0] || equal(op(e0,e4),e0)** -> .
% 1.32/1.48  11817[15:MRR:11067.1,11813.0] ||  -> equal(op(e0,e4),e4)**.
% 1.32/1.48  11822[15:Rew:11817.0,78.0] || equal(op(e3,e4),e4)** -> .
% 1.32/1.48  11832[15:Rew:11798.0,11696.0] ||  -> equal(op(e2,e0),e0)**.
% 1.32/1.48  11841[15:Rew:11832.0,44.0] || equal(op(e4,e0),e0)** -> .
% 1.32/1.48  11919[15:MRR:11719.0,11719.1,11822.0,4.0] ||  -> equal(op(e3,e1),e4)**.
% 1.32/1.48  11922[15:Rew:11919.0,11063.0] ||  -> equal(op(e4,e4),e1)**.
% 1.32/1.48  11932[15:Rew:11922.0,35.0] ||  -> equal(op(e4,e1),e4)**.
% 1.32/1.48  12011[15:Rew:11932.0,11741.4,11730.0,11741.3,11922.0,11741.0] ||  -> equal(e1,e0) equal(op(e4,e0),e0)** equal(e2,e0) equal(e3,e0) equal(e4,e0).
% 1.32/1.48  12012[15:MRR:12011.0,12011.1,12011.2,12011.3,12011.4,1.0,11841.0,2.0,3.0,4.0] ||  -> .
% 1.32/1.48  12013[15:Spt:12012.0,11679.0,11682.0] || equal(op(e3,e0),e2)** -> .
% 1.32/1.48  12014[15:Spt:12012.0,11679.1] ||  -> equal(op(e3,e0),e1)**.
% 1.32/1.48  12019[15:Rew:12014.0,26.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  12023[15:Rew:12019.0,11062.0] ||  -> equal(op(e4,e0),e3)**.
% 1.32/1.48  12045[15:Rew:12023.0,127.0] || equal(op(e4,e2),e3)** -> .
% 1.32/1.48  12061[15:MRR:11071.1,12045.0] ||  -> equal(op(e3,e2),e3)**.
% 1.32/1.48  12109[15:Rew:12019.0,11083.1] ||  -> equal(op(e4,e1),e4)** equal(e4,e0).
% 1.32/1.48  12110[15:MRR:12109.1,4.0] ||  -> equal(op(e4,e1),e4)**.
% 1.32/1.48  12115[15:Rew:12110.0,11034.0] ||  -> equal(op(e3,e4),e4)**.
% 1.32/1.48  12117[15:Rew:12110.0,130.0] || equal(op(e4,e2),e4)** -> .
% 1.32/1.48  12133[15:Rew:12115.0,78.0] || equal(op(e0,e4),e4)** -> .
% 1.32/1.48  12146[15:MRR:11076.0,12133.0] ||  -> equal(op(e0,e0),e4)**.
% 1.32/1.48  12152[15:Rew:12146.0,37.0] || equal(op(e2,e0),e4)** -> .
% 1.32/1.48  12173[15:Rew:12019.0,11096.1,12019.0,11096.0] || equal(op(e1,e0),e2)** equal(e0,e0) -> .
% 1.32/1.48  12174[15:Obv:12173.1] || equal(op(e1,e0),e2)** -> .
% 1.32/1.48  12191[15:Rew:12061.0,11081.2] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(e4,e3).
% 1.32/1.48  12192[15:MRR:12191.0,12191.2,12117.0,10.0] ||  -> equal(op(e2,e2),e4)**.
% 1.32/1.48  12195[15:Rew:12192.0,23.0] ||  -> equal(op(e2,e4),e2)**.
% 1.32/1.48  12204[15:Rew:12195.0,109.0] || equal(op(e2,e0),e2)** -> .
% 1.32/1.48  12212[15:MRR:10777.0,10777.2,12204.0,12152.0] ||  -> equal(op(e2,e0),e0)**.
% 1.32/1.48  12232[15:Rew:12014.0,9649.2,12023.0,9649.1,12212.0,9649.0] ||  -> equal(e2,e0) equal(e3,e2) equal(e2,e1) equal(op(e1,e0),e2)**.
% 1.32/1.48  12233[15:MRR:12232.0,12232.1,12232.2,12232.3,2.0,8.0,5.0,12174.0] ||  -> .
% 1.32/1.48  12292[11:Spt:12233.0,11018.0,11021.0] || equal(op(e1,e4),e3)** -> .
% 1.32/1.48  12293[11:Spt:12233.0,11018.1,11018.2] ||  -> equal(op(e1,e4),e2)** equal(op(e1,e4),e0).
% 1.32/1.48  12294[11:MRR:10772.2,12292.0] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3) equal(op(e0,e4),e3).
% 1.32/1.48  12296[12:Spt:12293.0] ||  -> equal(op(e1,e4),e2)**.
% 1.32/1.48  12300[12:Rew:12296.0,20.0] ||  -> equal(op(e1,e2),e4)**.
% 1.32/1.48  12301[12:Rew:12296.0,80.0] || equal(op(e2,e4),e2)** -> .
% 1.32/1.48  12306[12:Rew:12296.0,82.0] || equal(op(e4,e4),e2)** -> .
% 1.32/1.48  12318[12:Rew:12300.0,10741.0] ||  -> equal(op(e4,e3),e2)**.
% 1.32/1.48  12319[12:Rew:12300.0,10740.0] ||  -> equal(op(e3,e4),e1)**.
% 1.32/1.48  12328[12:Rew:12300.0,10782.0] || equal(op(e2,e4),e0)** equal(op(e1,e2),e4) -> .
% 1.32/1.48  12340[12:Rew:12318.0,34.0] ||  -> equal(op(e4,e2),e3)**.
% 1.32/1.48  12359[12:Rew:12318.0,10787.2] ||  -> equal(op(e3,e3),e0)** equal(op(e0,e3),e0) equal(e2,e0) equal(op(e1,e3),e0).
% 1.32/1.48  12360[12:Rew:12319.0,30.0] ||  -> equal(op(e3,e1),e4)**.
% 1.32/1.48  12365[12:Rew:12319.0,85.0] || equal(op(e4,e4),e1)** -> .
% 1.32/1.48  12370[12:Rew:12319.0,12294.1] ||  -> equal(op(e4,e4),e3)** equal(e3,e1) equal(op(e0,e4),e3).
% 1.32/1.48  12385[12:Rew:12340.0,134.0] || equal(op(e4,e4),e3)** -> .
% 1.32/1.48  12406[12:Rew:12360.0,10776.2] ||  -> equal(op(e1,e1),e0) equal(op(e4,e1),e0)** equal(e4,e0).
% 1.32/1.48  12410[12:MRR:10778.1,12301.0] ||  -> equal(op(e2,e4),e4)** equal(op(e2,e4),e0).
% 1.32/1.48  12415[12:MRR:331.2,12306.0] ||  -> equal(op(e4,e4),e4)** equal(op(e4,e4),e3) equal(op(e4,e4),e1) equal(op(e4,e4),e0).
% 1.32/1.48  12435[12:Rew:12300.0,12328.1] || equal(op(e2,e4),e0)** equal(e4,e4) -> .
% 1.32/1.48  12436[12:Obv:12435.1] || equal(op(e2,e4),e0)** -> .
% 1.32/1.48  12438[12:MRR:12410.1,12436.0] ||  -> equal(op(e2,e4),e4)**.
% 1.32/1.48  12442[12:Rew:12438.0,84.0] || equal(op(e4,e4),e4)** -> .
% 1.32/1.48  12458[12:MRR:12370.0,12370.1,12385.0,6.0] ||  -> equal(op(e0,e4),e3)**.
% 1.32/1.48  12461[12:Rew:12458.0,15.0] ||  -> equal(op(e0,e3),e4)**.
% 1.32/1.48  12478[12:Rew:12461.0,151.0] ||  -> equal(op(e4,op(e3,e0)),e3)**.
% 1.32/1.48  12522[12:MRR:12406.2,4.0] ||  -> equal(op(e1,e1),e0) equal(op(e4,e1),e0)**.
% 1.32/1.48  12543[12:Rew:12461.0,12359.1] ||  -> equal(op(e3,e3),e0)** equal(e4,e0) equal(e2,e0) equal(op(e1,e3),e0).
% 1.32/1.48  12544[12:MRR:12543.1,12543.2,4.0,2.0] ||  -> equal(op(e3,e3),e0)** equal(op(e1,e3),e0).
% 1.32/1.48  12548[12:MRR:12415.0,12415.1,12415.2,12442.0,12385.0,12365.0] ||  -> equal(op(e4,e4),e0)**.
% 1.32/1.48  12551[12:Rew:12548.0,132.0] || equal(op(e4,e1),e0)** -> .
% 1.32/1.48  12578[12:MRR:12522.1,12551.0] ||  -> equal(op(e1,e1),e0)**.
% 1.32/1.48  12591[12:Rew:12578.0,101.0] || equal(op(e1,e3),e0)** -> .
% 1.32/1.48  12623[12:MRR:12544.1,12591.0] ||  -> equal(op(e3,e3),e0)**.
% 1.32/1.48  12633[12:Rew:12623.0,29.0] ||  -> equal(op(e3,e0),e3)**.
% 1.32/1.48  12647[12:Rew:12633.0,12478.0] ||  -> equal(op(e4,e3),e3)**.
% 1.32/1.48  12654[12:Rew:12318.0,12647.0] ||  -> equal(e3,e2)**.
% 1.32/1.48  12655[12:MRR:12654.0,8.0] ||  -> .
% 1.32/1.48  12705[12:Spt:12655.0,12293.0,12296.0] || equal(op(e1,e4),e2)** -> .
% 1.32/1.48  12706[12:Spt:12655.0,12293.1] ||  -> equal(op(e1,e4),e0)**.
% 1.32/1.48  12711[12:Rew:12706.0,20.0] ||  -> equal(op(e1,e0),e4)**.
% 1.32/1.48  12712[12:Rew:12711.0,9597.0] ||  -> equal(op(e4,e2),e0)**.
% 1.32/1.48  12733[12:Rew:12712.0,130.0] || equal(op(e4,e1),e0)** -> .
% 1.32/1.48  12753[12:Rew:12711.0,11019.1] ||  -> equal(op(e1,e1),e1)** equal(e4,e1).
% 1.32/1.48  12754[12:MRR:12753.1,7.0] ||  -> equal(op(e1,e1),e1)**.
% 1.32/1.48  12765[12:Rew:12711.0,9605.1,12711.0,9605.0] || equal(op(e0,e4),e3)** equal(e4,e4) -> .
% 1.32/1.48  12766[12:Obv:12765.1] || equal(op(e0,e4),e3)** -> .
% 1.32/1.48  12768[12:Rew:12712.0,10770.1] ||  -> equal(op(e3,e2),e3)** equal(e3,e0) equal(op(e1,e2),e3).
% 1.32/1.48  12769[12:MRR:12768.1,3.0] ||  -> equal(op(e3,e2),e3)** equal(op(e1,e2),e3).
% 1.32/1.48  12774[12:MRR:12294.2,12766.0] ||  -> equal(op(e4,e4),e3)** equal(op(e3,e4),e3).
% 1.32/1.48  12778[12:Rew:12754.0,10776.0] ||  -> equal(e1,e0) equal(op(e4,e1),e0)** equal(op(e3,e1),e0).
% 1.32/1.48  12779[12:MRR:12778.0,12778.1,1.0,12733.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  12782[12:Rew:12779.0,27.0] ||  -> equal(op(e3,e0),e1)**.
% 1.32/1.48  12793[12:Rew:12782.0,119.0] || equal(op(e3,e4),e1)** -> .
% 1.32/1.48  12803[12:MRR:11020.1,12793.0] ||  -> equal(op(e4,e4),e1)**.
% 1.32/1.48  12813[12:Rew:12803.0,12774.0] ||  -> equal(e3,e1) equal(op(e3,e4),e3)**.
% 1.32/1.48  12842[12:MRR:12813.0,6.0] ||  -> equal(op(e3,e4),e3)**.
% 1.32/1.48  12847[12:Rew:12842.0,124.0] || equal(op(e3,e2),e3)** -> .
% 1.32/1.48  12864[12:MRR:12769.0,12847.0] ||  -> equal(op(e1,e2),e3)**.
% 1.32/1.48  13072[12:Rew:12706.0,209.2,12706.0,209.1,12706.0,209.0] || equal(e0,e0) equal(op(e1,op(e0,e1)),e3)** equal(op(e0,e1),e2) -> .
% 1.32/1.48  13073[12:Obv:13072.0] || equal(op(e1,op(e0,e1)),e3)** equal(op(e0,e1),e2) -> .
% 1.32/1.48  13074[12:Rew:9572.0,13073.1,9572.0,13073.0] || equal(op(e1,e2),e3)** equal(e2,e2) -> .
% 1.32/1.48  13075[12:Obv:13074.1] || equal(op(e1,e2),e3)** -> .
% 1.32/1.48  13076[12:Rew:12864.0,13075.0] || equal(e3,e3)* -> .
% 1.32/1.48  13077[12:Obv:13076.0] ||  -> .
% 1.32/1.48  13078[8:Spt:13077.0,10708.0,10711.0] || equal(op(e2,e3),e1)** -> .
% 1.32/1.48  13079[8:Spt:13077.0,10708.1] ||  -> equal(op(e2,e3),e0)**.
% 1.32/1.48  13084[8:Rew:13079.0,24.0] ||  -> equal(op(e2,e0),e3)**.
% 1.32/1.48  13086[8:Rew:13084.0,9594.0] ||  -> equal(op(e3,e1),e0)**.
% 1.32/1.48  13087[8:Rew:13084.0,9595.0] ||  -> equal(op(e1,e3),e2)**.
% 1.32/1.48  13090[8:Rew:13087.0,19.0] ||  -> equal(op(e1,e2),e3)**.
% 1.32/1.48  13105[8:Rew:13090.0,100.0] || equal(op(e1,e1),e3)** -> .
% 1.36/1.52  13107[8:Rew:13086.0,120.0] || equal(op(e3,e2),e0)** -> .
% 1.36/1.52  13124[8:Rew:13084.0,37.0] || equal(op(e0,e0),e3)** -> .
% 1.36/1.52  13129[8:Rew:13079.0,113.0] || equal(op(e2,e2),e0)** -> .
% 1.36/1.52  13132[8:Rew:13079.0,67.0] || equal(op(e0,e3),e0)** -> .
% 1.36/1.52  13133[8:Rew:13084.0,106.0] || equal(op(e2,e1),e3)** -> .
% 1.36/1.52  13144[8:Rew:13084.0,9611.1,13084.0,9611.0] || equal(op(e0,e3),e4)** equal(e3,e3) -> .
% 1.36/1.52  13145[8:Obv:13144.1] || equal(op(e0,e3),e4)** -> .
% 1.36/1.52  13151[8:MRR:9631.1,9631.2,13132.0,13145.0] ||  -> equal(op(e0,e3),e3)**.
% 1.36/1.52  13168[8:MRR:9625.2,13124.0] ||  -> equal(op(e0,e0),e0) equal(op(e0,e0),e4)**.
% 1.36/1.52  13178[8:Rew:13086.0,5562.2] ||  -> equal(op(e4,e1),e4)** equal(op(e1,e1),e4) equal(e4,e0) equal(op(e2,e1),e4).
% 1.36/1.52  13179[8:MRR:13178.2,4.0] ||  -> equal(op(e4,e1),e4)** equal(op(e1,e1),e4) equal(op(e2,e1),e4).
% 1.36/1.52  13183[8:Rew:13086.0,9636.0] ||  -> equal(e3,e0) equal(op(e1,e1),e3) equal(op(e4,e1),e3)** equal(op(e2,e1),e3).
% 1.36/1.52  13184[8:MRR:13183.0,13183.1,13183.3,3.0,13105.0,13133.0] ||  -> equal(op(e4,e1),e3)**.
% 1.36/1.52  13186[8:Rew:13184.0,32.0] ||  -> equal(op(e4,e3),e1)**.
% 1.36/1.52  13196[8:Rew:13184.0,13179.0] ||  -> equal(e4,e3) equal(op(e1,e1),e4) equal(op(e2,e1),e4)**.
% 1.36/1.52  13211[8:MRR:13196.0,10.0] ||  -> equal(op(e1,e1),e4) equal(op(e2,e1),e4)**.
% 1.36/1.52  13216[8:Rew:13090.0,9640.3] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e3,e2),e4) equal(e4,e3).
% 1.36/1.52  13217[8:MRR:13216.3,10.0] ||  -> equal(op(e4,e2),e4)** equal(op(e2,e2),e4) equal(op(e3,e2),e4).
% 1.36/1.52  13220[8:Rew:13090.0,9645.3] ||  -> equal(op(e2,e2),e0) equal(op(e4,e2),e0)** equal(op(e3,e2),e0) equal(e3,e0).
% 1.36/1.52  13221[8:MRR:13220.0,13220.2,13220.3,13129.0,13107.0,3.0] ||  -> equal(op(e4,e2),e0)**.
% 1.36/1.52  13226[8:Rew:13221.0,134.0] || equal(op(e4,e4),e0)** -> .
% 1.36/1.52  13231[8:Rew:13221.0,13217.0] ||  -> equal(e4,e0) equal(op(e2,e2),e4) equal(op(e3,e2),e4)**.
% 1.36/1.52  13243[8:MRR:13231.0,4.0] ||  -> equal(op(e2,e2),e4) equal(op(e3,e2),e4)**.
% 1.36/1.52  13245[8:Rew:13151.0,10710.3,13087.0,10710.2,13186.0,10710.0] ||  -> equal(e4,e1) equal(op(e3,e3),e4)** equal(e4,e2) equal(e4,e3).
% 1.36/1.52  13246[8:MRR:13245.0,13245.2,13245.3,7.0,9.0,10.0] ||  -> equal(op(e3,e3),e4)**.
% 1.36/1.52  13252[8:Rew:13246.0,123.0] || equal(op(e3,e2),e4)** -> .
% 1.36/1.52  13272[8:MRR:13243.1,13252.0] ||  -> equal(op(e2,e2),e4)**.
% 1.36/1.52  13279[8:Rew:13272.0,110.0] || equal(op(e2,e1),e4)** -> .
% 1.36/1.52  13302[8:MRR:13211.1,13279.0] ||  -> equal(op(e1,e1),e4)**.
% 1.36/1.52  13312[8:Rew:13302.0,17.0] ||  -> equal(op(e1,e4),e1)**.
% 1.36/1.52  13482[8:Rew:13090.0,320.4,13087.0,320.3,13312.0,320.2,13302.0,320.0] ||  -> equal(e4,e0) equal(op(e1,e0),e0)** equal(e1,e0) equal(e2,e0) equal(e3,e0).
% 1.36/1.52  13483[8:MRR:13482.0,13482.2,13482.3,13482.4,4.0,1.0,2.0,3.0] ||  -> equal(op(e1,e0),e0)**.
% 1.36/1.52  13488[8:Rew:13483.0,36.0] || equal(op(e0,e0),e0)** -> .
% 1.36/1.52  13497[8:MRR:13168.0,13488.0] ||  -> equal(op(e0,e0),e4)**.
% 1.36/1.52  13512[8:Rew:13497.0,136.0] ||  -> equal(op(e4,e4),e0)**.
% 1.36/1.52  13518[8:MRR:13512.0,13226.0] ||  -> .
% 1.36/1.52  % SZS output end Refutation
% 1.36/1.52  Formulae used in the proof : ax5 ax6 ax4 ax3 ax122 ax119 ax106 ax89 ax87 ax86 ax78 ax77 ax59 ax32 ax29 ax27 ax21 ax19 ax15 ax7 ax2 ax1
% 1.36/1.52  
%------------------------------------------------------------------------------