%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP125-3.005 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n010.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 : Sat Jul 16 11:45:35 EDT 2022 % Result : Unsatisfiable 11.58s 11.82s % Output : Refutation 17.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP125-3.005 : TPTP v8.1.0. Released v1.2.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n010.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 : Mon Jun 13 14:46:24 EDT 2022 % 0.12/0.33 % CPUTime : % 11.58/11.82 % 11.58/11.82 SPASS V 3.9 % 11.58/11.82 SPASS beiseite: Proof found. % 11.58/11.82 % SZS status Theorem % 11.58/11.82 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 11.58/11.82 SPASS derived 21859 clauses, backtracked 7006 clauses, performed 184 splits and kept 10400 clauses. % 11.58/11.82 SPASS allocated 99589 KBytes. % 11.58/11.82 SPASS spent 0:0:11.46 on the problem. % 11.58/11.82 0:00:00.03 for the input. % 11.58/11.82 0:00:00.00 for the FLOTTER CNF translation. % 11.58/11.82 0:00:00.35 for inferences. % 11.58/11.82 0:00:00.18 for the backtracking. % 11.58/11.82 0:0:10.74 for the reduction. % 11.58/11.82 % 11.58/11.82 % 11.58/11.82 Here is a proof with depth 22, length 1004 : % 11.58/11.82 % SZS output start Refutation % 11.58/11.82 1[0:Inp] || -> next(e_0,e_1)*. % 11.58/11.82 2[0:Inp] || -> next(e_1,e_2)*. % 11.58/11.82 3[0:Inp] || -> next(e_2,e_3)*. % 11.58/11.82 4[0:Inp] || -> next(e_3,e_4)*. % 11.58/11.82 5[0:Inp] || -> next(e_4,e_5)*. % 11.58/11.82 6[0:Inp] || -> greater(e_1,e_0)*. % 11.58/11.82 7[0:Inp] || -> greater(e_2,e_0)*. % 11.58/11.82 8[0:Inp] || -> greater(e_3,e_0)*. % 11.58/11.82 9[0:Inp] || -> greater(e_4,e_0)*. % 11.58/11.82 11[0:Inp] || -> greater(e_2,e_1)*. % 11.58/11.82 12[0:Inp] || -> greater(e_3,e_1)*. % 11.58/11.82 15[0:Inp] || -> greater(e_3,e_2)*. % 11.58/11.82 16[0:Inp] || -> greater(e_4,e_2)*. % 11.58/11.82 17[0:Inp] || -> greater(e_5,e_2)*. % 11.58/11.82 18[0:Inp] || -> greater(e_4,e_3)*. % 11.58/11.82 19[0:Inp] || -> greater(e_5,e_3)*. % 11.58/11.82 22[0:Inp] group_element(u) || -> cycle(u,e_4) cycle(u,e_3) cycle(u,e_2) cycle(u,e_1) cycle(u,e_0)*. % 11.58/11.82 23[0:Inp] || -> cycle(e_5,e_0)*. % 11.58/11.82 24[0:Inp] || next(u,v)*+ next(w,x)* cycle(x,u)* cycle(w,y)* greater(y,e_0) -> equalish(y,v)*. % 11.58/11.82 25[0:Inp] || greater(u,v)*+ greater(w,x)* next(w,y)* cycle(y,v)* cycle(x,u)* cycle(w,e_0) -> . % 11.58/11.82 26[0:Inp] || greater(u,v) cycle(v,e_0) product(v,e_1,u)*+ -> . % 11.58/11.82 27[0:Inp] || next(u,v)* cycle(u,w)* greater(w,e_0)* product(u,e_1,x)*+ -> equalish(x,v)*. % 11.58/11.82 28[0:Inp] || -> group_element(e_1)*. % 11.58/11.82 29[0:Inp] || -> group_element(e_2)*. % 11.58/11.82 30[0:Inp] || -> group_element(e_3)*. % 11.58/11.82 31[0:Inp] || -> group_element(e_4)*. % 11.58/11.82 32[0:Inp] || -> group_element(e_5)*. % 11.58/11.82 33[0:Inp] || equalish(e_1,e_2)*+ -> . % 11.58/11.82 34[0:Inp] || equalish(e_1,e_3)*+ -> . % 11.58/11.82 35[0:Inp] || equalish(e_1,e_4)*+ -> . % 11.58/11.82 36[0:Inp] || equalish(e_1,e_5)*+ -> . % 11.58/11.82 37[0:Inp] || equalish(e_2,e_1)*+ -> . % 11.58/11.82 38[0:Inp] || equalish(e_2,e_3)*+ -> . % 11.58/11.82 39[0:Inp] || equalish(e_2,e_4)*+ -> . % 11.58/11.82 40[0:Inp] || equalish(e_2,e_5)*+ -> . % 11.58/11.82 41[0:Inp] || equalish(e_3,e_1)*+ -> . % 11.58/11.82 42[0:Inp] || equalish(e_3,e_2)*+ -> . % 11.58/11.82 43[0:Inp] || equalish(e_3,e_4)*+ -> . % 11.58/11.82 45[0:Inp] || equalish(e_4,e_1)*+ -> . % 11.58/11.82 46[0:Inp] || equalish(e_4,e_2)*+ -> . % 11.58/11.82 47[0:Inp] || equalish(e_4,e_3)*+ -> . % 11.58/11.82 50[0:Inp] || equalish(e_5,e_2)*+ -> . % 11.58/11.82 51[0:Inp] || equalish(e_5,e_3)*+ -> . % 11.58/11.82 52[0:Inp] || equalish(e_5,e_4)*+ -> . % 11.58/11.82 53[0:Inp] group_element(u) group_element(v) || -> product(v,u,e_5) product(v,u,e_4) product(v,u,e_3) product(v,u,e_2) product(v,u,e_1)*. % 11.58/11.82 54[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 11.58/11.82 55[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 11.58/11.82 56[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 11.58/11.82 57[0:Inp] || -> product(u,u,u)*. % 11.58/11.82 58[0:Inp] || product(u,v,w)*+ product(v,u,x)* -> product(x,w,v)*. % 11.58/11.82 71[0:Res:57.0,56.0] || product(u,v,v)*+ -> equalish(u,v). % 11.58/11.82 73[0:Res:57.0,55.0] || product(u,v,u)*+ -> equalish(v,u). % 11.58/11.82 75[0:Res:57.0,54.0] || product(u,u,v)*+ -> equalish(v,u). % 11.58/11.82 83[0:Res:3.0,24.0] || next(u,v)*+ cycle(v,e_2) cycle(u,w)* greater(w,e_0) -> equalish(w,e_3)*. % 11.58/11.82 84[0:Res:2.0,24.0] || next(u,v)*+ cycle(v,e_1) cycle(u,w)* greater(w,e_0) -> equalish(w,e_2)*. % 11.58/11.82 85[0:Res:1.0,24.0] || next(u,v)*+ cycle(v,e_0) cycle(u,w)* greater(w,e_0) -> equalish(w,e_1)*. % 11.58/11.82 103[0:Res:9.0,25.0] || greater(u,v)*+ next(u,w)* cycle(w,e_0) cycle(v,e_4) cycle(u,e_0) -> . % 11.58/11.82 104[0:Res:15.0,25.0] || greater(u,v)*+ next(u,w)* cycle(w,e_2) cycle(v,e_3) cycle(u,e_0) -> . % 11.58/11.82 105[0:Res:12.0,25.0] || greater(u,v)*+ next(u,w)* cycle(w,e_1) cycle(v,e_3) cycle(u,e_0) -> . % 11.58/11.82 106[0:Res:8.0,25.0] || greater(u,v)*+ next(u,w)* cycle(w,e_0) cycle(v,e_3) cycle(u,e_0) -> . % 11.58/11.82 107[0:Res:11.0,25.0] || greater(u,v)*+ next(u,w)* cycle(w,e_1) cycle(v,e_2) cycle(u,e_0) -> . % 11.58/11.82 108[0:Res:7.0,25.0] || greater(u,v)*+ next(u,w)* cycle(w,e_0) cycle(v,e_2) cycle(u,e_0) -> . % 11.58/11.82 109[0:Res:6.0,25.0] || greater(u,v)*+ next(u,w)* cycle(w,e_0) cycle(v,e_1) cycle(u,e_0) -> . % 11.58/11.82 113[0:Res:53.6,73.0] group_element(u) group_element(e_1) || -> product(e_1,u,e_5) product(e_1,u,e_4) product(e_1,u,e_3) product(e_1,u,e_2)* equalish(u,e_1). % 11.58/11.82 115[0:Res:53.6,58.0] group_element(u) group_element(v) || product(u,v,w)*+ -> product(v,u,e_5) product(v,u,e_4) product(v,u,e_3) product(v,u,e_2)* product(w,e_1,u)*. % 11.58/11.82 117[0:Res:53.6,55.0] group_element(u) group_element(v) || product(v,w,e_1)*+ -> product(v,u,e_5) product(v,u,e_4) product(v,u,e_3) product(v,u,e_2)* equalish(w,u)*. % 11.58/11.82 118[0:Res:53.6,56.0] group_element(u) group_element(v) || product(w,u,e_1)*+ -> product(v,u,e_5) product(v,u,e_4) product(v,u,e_3) product(v,u,e_2)* equalish(w,v)*. % 11.58/11.82 119[0:Res:53.6,71.0] group_element(e_1) group_element(u) || -> product(u,e_1,e_5) product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(u,e_1). % 11.58/11.82 120[0:Res:53.6,27.3] group_element(e_1) group_element(u) || next(u,v)* cycle(u,w)* greater(w,e_0)* -> product(u,e_1,e_5) product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(e_1,v)*. % 11.58/11.82 121[0:SSi:119.0,28.0] group_element(u) || -> product(u,e_1,e_5) product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(u,e_1). % 11.58/11.82 122[0:SSi:113.1,28.0] group_element(u) || -> product(e_1,u,e_5) product(e_1,u,e_4) product(e_1,u,e_3) product(e_1,u,e_2)* equalish(u,e_1). % 11.58/11.82 127[0:SSi:120.0,28.0] group_element(u) || next(u,v)*+ cycle(u,w)* greater(w,e_0)* -> product(u,e_1,e_5) product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(e_1,v)*. % 11.58/11.82 135[0:Res:3.0,83.0] || cycle(e_3,e_2)+ cycle(e_2,u) greater(u,e_0) -> equalish(u,e_3)*. % 11.58/11.82 139[0:Res:4.0,84.0] || cycle(e_4,e_1)+ cycle(e_3,u) greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 140[0:Res:3.0,84.0] || cycle(e_3,e_1)+ cycle(e_2,u) greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 143[0:Res:5.0,85.0] || cycle(e_5,e_0) cycle(e_4,u) greater(u,e_0) -> equalish(u,e_1)*. % 11.58/11.82 148[0:MRR:143.0,23.0] || cycle(e_4,u)+ greater(u,e_0) -> equalish(u,e_1)*. % 11.58/11.82 160[0:Res:18.0,109.0] || next(e_4,u)*+ cycle(u,e_0) cycle(e_3,e_1) cycle(e_4,e_0) -> . % 11.58/11.82 168[0:Res:7.0,109.0] || next(e_2,u)*+ cycle(u,e_0) cycle(e_0,e_1) cycle(e_2,e_0) -> . % 11.58/11.82 180[0:Res:18.0,108.0] || next(e_4,u)*+ cycle(u,e_0) cycle(e_3,e_2) cycle(e_4,e_0) -> . % 11.58/11.82 187[0:Res:11.0,108.0] || next(e_2,u)*+ cycle(u,e_0) cycle(e_1,e_2) cycle(e_2,e_0) -> . % 11.58/11.82 189[0:Res:6.0,108.0] || next(e_1,u)*+ cycle(u,e_0) cycle(e_0,e_2) cycle(e_1,e_0) -> . % 11.58/11.82 207[0:Res:11.0,107.0] || next(e_2,u)*+ cycle(u,e_1) cycle(e_1,e_2) cycle(e_2,e_0) -> . % 11.58/11.82 209[0:Res:6.0,107.0] || next(e_1,u)*+ cycle(u,e_1) cycle(e_0,e_2) cycle(e_1,e_0) -> . % 11.58/11.82 220[0:Res:18.0,106.0] || next(e_4,u)*+ cycle(u,e_0) cycle(e_3,e_3) cycle(e_4,e_0) -> . % 11.58/11.82 221[0:Res:16.0,106.0] || next(e_4,u)*+ cycle(u,e_0) cycle(e_2,e_3) cycle(e_4,e_0) -> . % 11.58/11.82 227[0:Res:11.0,106.0] || next(e_2,u)*+ cycle(u,e_0) cycle(e_1,e_3) cycle(e_2,e_0) -> . % 11.58/11.82 229[0:Res:6.0,106.0] || next(e_1,u)*+ cycle(u,e_0) cycle(e_0,e_3) cycle(e_1,e_0) -> . % 11.58/11.82 244[0:Res:15.0,105.0] || next(e_3,u)*+ cycle(u,e_1) cycle(e_2,e_3) cycle(e_3,e_0) -> . % 11.58/11.82 247[0:Res:11.0,105.0] || next(e_2,u)*+ cycle(u,e_1) cycle(e_1,e_3) cycle(e_2,e_0) -> . % 11.58/11.82 249[0:Res:6.0,105.0] || next(e_1,u)*+ cycle(u,e_1) cycle(e_0,e_3) cycle(e_1,e_0) -> . % 11.58/11.82 267[0:Res:11.0,104.0] || next(e_2,u)*+ cycle(u,e_2) cycle(e_1,e_3) cycle(e_2,e_0) -> . % 11.58/11.82 269[0:Res:6.0,104.0] || next(e_1,u)*+ cycle(u,e_2) cycle(e_0,e_3) cycle(e_1,e_0) -> . % 11.58/11.82 280[0:Res:18.0,103.0] || next(e_4,u)* cycle(u,e_0) cycle(e_3,e_4) cycle(e_4,e_0) -> . % 11.58/11.82 459[0:Res:57.0,118.2] group_element(e_1) group_element(u) || -> product(u,e_1,e_5) product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(e_1,u). % 11.58/11.82 461[0:SSi:459.0,28.0] group_element(u) || -> product(u,e_1,e_5) product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(e_1,u). % 11.58/11.82 463[0:Res:57.0,117.2] group_element(u) group_element(e_1) || -> product(e_1,u,e_5) product(e_1,u,e_4) product(e_1,u,e_3) product(e_1,u,e_2)* equalish(e_1,u). % 11.58/11.82 465[0:SSi:463.1,28.0] group_element(u) || -> product(e_1,u,e_5) product(e_1,u,e_4) product(e_1,u,e_3) product(e_1,u,e_2)* equalish(e_1,u). % 11.58/11.82 473[0:Res:5.0,160.0] || cycle(e_5,e_0) cycle(e_3,e_1)* cycle(e_4,e_0) -> . % 11.58/11.82 474[0:MRR:473.0,23.0] || cycle(e_3,e_1)*+ cycle(e_4,e_0) -> . % 11.58/11.82 478[0:Res:53.6,115.2] group_element(u) group_element(v) group_element(v) group_element(u) || -> product(v,u,e_5) product(v,u,e_4) product(v,u,e_3) product(v,u,e_2)* product(u,v,e_5) product(u,v,e_4) product(u,v,e_3) product(u,v,e_2)* product(e_1,e_1,v)*. % 11.58/11.82 480[0:Obv:478.1] group_element(u) group_element(v) || -> product(u,v,e_5) product(u,v,e_4) product(u,v,e_3) product(u,v,e_2)* product(v,u,e_5) product(v,u,e_4) product(v,u,e_3) product(v,u,e_2)* product(e_1,e_1,u)*. % 11.58/11.82 485[0:Res:5.0,127.1] group_element(e_4) || cycle(e_4,u) greater(u,e_0)* -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) product(e_4,e_1,e_2)* equalish(e_1,e_5). % 11.58/11.82 494[0:SSi:485.0,31.0] || cycle(e_4,u) greater(u,e_0)* -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) product(e_4,e_1,e_2)* equalish(e_1,e_5). % 11.58/11.82 495[0:MRR:494.6,36.0] || cycle(e_4,u)+ greater(u,e_0)* -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) product(e_4,e_1,e_2)*. % 11.58/11.82 500[0:Res:3.0,168.0] || cycle(e_3,e_0)+ cycle(e_0,e_1)* cycle(e_2,e_0) -> . % 11.58/11.82 503[0:Res:22.5,500.0] group_element(e_3) || cycle(e_0,e_1)* cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1). % 11.58/11.82 504[0:SSi:503.0,30.0] || cycle(e_0,e_1)* cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1). % 11.58/11.82 508[0:Res:5.0,180.0] || cycle(e_5,e_0) cycle(e_3,e_2)* cycle(e_4,e_0) -> . % 11.58/11.82 509[0:MRR:508.0,23.0] || cycle(e_3,e_2)*+ cycle(e_4,e_0) -> . % 11.58/11.82 519[0:Res:3.0,187.0] || cycle(e_3,e_0)+ cycle(e_1,e_2)* cycle(e_2,e_0) -> . % 11.58/11.82 520[0:Res:22.5,519.0] group_element(e_3) || cycle(e_1,e_2)* cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1). % 11.58/11.82 521[0:SSi:520.0,30.0] || cycle(e_1,e_2)* cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1). % 11.58/11.82 525[0:Res:2.0,189.0] || cycle(e_2,e_0)+ cycle(e_0,e_2)* cycle(e_1,e_0) -> . % 11.58/11.82 526[0:Res:22.5,525.0] group_element(e_2) || cycle(e_0,e_2)* cycle(e_1,e_0) -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1). % 11.58/11.82 527[0:SSi:526.0,29.0] || cycle(e_0,e_2)* cycle(e_1,e_0) -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1). % 11.58/11.82 531[0:Res:3.0,207.0] || cycle(e_3,e_1)+ cycle(e_1,e_2)* cycle(e_2,e_0) -> . % 11.58/11.82 532[0:MRR:521.5,531.0] || cycle(e_1,e_2)* cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2). % 11.58/11.82 535[0:Res:2.0,209.0] || cycle(e_2,e_1)+ cycle(e_0,e_2)* cycle(e_1,e_0) -> . % 11.58/11.82 536[0:MRR:527.5,535.0] || cycle(e_0,e_2)* cycle(e_1,e_0) -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2). % 11.58/11.82 537[0:Res:5.0,220.0] || cycle(e_5,e_0) cycle(e_3,e_3)* cycle(e_4,e_0) -> . % 11.58/11.82 538[0:MRR:537.0,23.0] || cycle(e_3,e_3)*+ cycle(e_4,e_0) -> . % 11.58/11.82 539[0:Res:5.0,221.0] || cycle(e_5,e_0) cycle(e_2,e_3)* cycle(e_4,e_0) -> . % 11.58/11.82 540[0:MRR:539.0,23.0] || cycle(e_2,e_3)*+ cycle(e_4,e_0) -> . % 11.58/11.82 548[0:Res:3.0,227.0] || cycle(e_3,e_0)+ cycle(e_1,e_3)* cycle(e_2,e_0) -> . % 11.58/11.82 549[0:Res:22.5,548.0] group_element(e_3) || cycle(e_1,e_3)* cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1). % 11.58/11.82 550[0:SSi:549.0,30.0] || cycle(e_1,e_3)* cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1). % 11.58/11.82 554[0:Res:2.0,229.0] || cycle(e_2,e_0)+ cycle(e_0,e_3)* cycle(e_1,e_0) -> . % 11.58/11.82 555[0:Res:4.0,244.0] || cycle(e_4,e_1)+ cycle(e_2,e_3)* cycle(e_3,e_0) -> . % 11.58/11.82 556[0:Res:22.5,554.0] group_element(e_2) || cycle(e_0,e_3)* cycle(e_1,e_0) -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1). % 11.58/11.82 557[0:SSi:556.0,29.0] || cycle(e_0,e_3)* cycle(e_1,e_0) -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1). % 11.58/11.82 560[0:Res:3.0,247.0] || cycle(e_3,e_1)+ cycle(e_1,e_3)* cycle(e_2,e_0) -> . % 11.58/11.82 561[0:MRR:550.5,560.0] || cycle(e_1,e_3)* cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2). % 11.58/11.82 564[0:Res:2.0,249.0] || cycle(e_2,e_1)+ cycle(e_0,e_3)* cycle(e_1,e_0) -> . % 11.58/11.82 565[0:MRR:557.5,564.0] || cycle(e_0,e_3)* cycle(e_1,e_0) -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2). % 11.58/11.82 569[0:Res:3.0,267.0] || cycle(e_3,e_2)+ cycle(e_1,e_3)* cycle(e_2,e_0) -> . % 11.58/11.82 570[0:MRR:561.4,569.0] || cycle(e_1,e_3)*+ cycle(e_2,e_0) -> cycle(e_3,e_4) cycle(e_3,e_3). % 11.58/11.82 573[1:Spt:570.2] || -> cycle(e_3,e_4)*. % 11.58/11.82 579[1:MRR:280.2,573.0] || next(e_4,u)*+ cycle(u,e_0) cycle(e_4,e_0) -> . % 11.58/11.82 589[1:Res:5.0,579.0] || cycle(e_5,e_0) cycle(e_4,e_0)* -> . % 11.58/11.82 590[1:MRR:589.0,23.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 591[1:Res:22.5,590.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 592[1:SSi:591.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 593[2:Spt:592.3] || -> cycle(e_4,e_1)*. % 11.58/11.82 594[2:MRR:139.0,593.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 607[2:Res:573.0,594.0] || greater(e_4,e_0) -> equalish(e_4,e_2)*. % 11.58/11.82 608[2:MRR:607.0,607.1,9.0,46.0] || -> . % 11.58/11.82 609[2:Spt:608.0,592.3,593.0] || cycle(e_4,e_1)*+ -> . % 11.58/11.82 610[2:Spt:608.0,592.0,592.1,592.2] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2)*. % 11.58/11.82 611[3:Spt:610.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 618[3:Res:611.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 619[3:MRR:618.0,618.1,9.0,45.0] || -> . % 11.58/11.82 620[3:Spt:619.0,610.0,611.0] || cycle(e_4,e_4)* -> . % 11.58/11.82 621[3:Spt:619.0,610.1,610.2] || -> cycle(e_4,e_3) cycle(e_4,e_2)*. % 11.58/11.82 622[4:Spt:621.1] || -> cycle(e_4,e_2)*. % 11.58/11.82 629[4:Res:622.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 630[4:MRR:629.0,629.1,7.0,37.0] || -> . % 11.58/11.82 631[4:Spt:630.0,621.1,622.0] || cycle(e_4,e_2)* -> . % 11.58/11.82 632[4:Spt:630.0,621.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 635[4:Res:632.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 636[4:MRR:635.0,635.1,8.0,41.0] || -> . % 11.58/11.82 637[1:Spt:636.0,570.2,573.0] || cycle(e_3,e_4)*+ -> . % 11.58/11.82 638[1:Spt:636.0,570.0,570.1,570.3] || cycle(e_1,e_3)*+ cycle(e_2,e_0) -> cycle(e_3,e_3). % 11.58/11.82 640[1:MRR:532.2,637.0] || cycle(e_1,e_2)*+ cycle(e_2,e_0) -> cycle(e_3,e_3) cycle(e_3,e_2). % 11.58/11.82 642[1:MRR:504.2,637.0] || cycle(e_0,e_1)* cycle(e_2,e_0) -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1). % 11.58/11.82 649[2:Spt:640.2] || -> cycle(e_3,e_3)*. % 11.58/11.82 651[2:MRR:538.0,649.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 657[2:Res:22.5,651.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 658[2:SSi:657.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 663[3:Spt:658.3] || -> cycle(e_4,e_1)*. % 11.58/11.82 670[3:MRR:139.0,663.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 675[3:Res:649.0,670.0] || greater(e_3,e_0) -> equalish(e_3,e_2)*. % 11.58/11.82 676[3:MRR:675.0,675.1,8.0,42.0] || -> . % 11.58/11.82 677[3:Spt:676.0,658.3,663.0] || cycle(e_4,e_1)*+ -> . % 11.58/11.82 678[3:Spt:676.0,658.0,658.1,658.2] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2)*. % 11.58/11.82 679[4:Spt:678.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 687[4:Res:679.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 688[4:MRR:687.0,687.1,9.0,45.0] || -> . % 11.58/11.82 689[4:Spt:688.0,678.0,679.0] || cycle(e_4,e_4)* -> . % 11.58/11.82 690[4:Spt:688.0,678.1,678.2] || -> cycle(e_4,e_3) cycle(e_4,e_2)*. % 11.58/11.82 691[5:Spt:690.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 695[5:Res:691.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 696[5:MRR:695.0,695.1,8.0,41.0] || -> . % 11.58/11.82 697[5:Spt:696.0,690.0,691.0] || cycle(e_4,e_3)* -> . % 11.58/11.82 698[5:Spt:696.0,690.1] || -> cycle(e_4,e_2)*. % 11.58/11.82 704[5:Res:698.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 705[5:MRR:704.0,704.1,7.0,37.0] || -> . % 11.58/11.82 706[2:Spt:705.0,640.2,649.0] || cycle(e_3,e_3)*+ -> . % 11.58/11.82 707[2:Spt:705.0,640.0,640.1,640.3] || cycle(e_1,e_2)*+ cycle(e_2,e_0) -> cycle(e_3,e_2). % 11.58/11.82 711[2:MRR:642.2,706.0] || cycle(e_0,e_1)*+ cycle(e_2,e_0) -> cycle(e_3,e_2) cycle(e_3,e_1). % 11.58/11.82 716[3:Spt:711.2] || -> cycle(e_3,e_2)*. % 11.58/11.82 717[3:MRR:135.0,716.0] || cycle(e_2,u)+ greater(u,e_0) -> equalish(u,e_3)*. % 11.58/11.82 718[3:MRR:509.0,716.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 723[3:Res:22.5,718.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 724[3:SSi:723.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 729[4:Spt:724.3] || -> cycle(e_4,e_1)*. % 11.58/11.82 741[0:Res:2.0,269.0] || cycle(e_2,e_2)+ cycle(e_0,e_3)* cycle(e_1,e_0) -> . % 11.58/11.82 742[0:MRR:565.4,741.0] || cycle(e_0,e_3)*+ cycle(e_1,e_0) -> cycle(e_2,e_4) cycle(e_2,e_3). % 11.58/11.82 744[5:Spt:742.2] || -> cycle(e_2,e_4)*. % 11.58/11.82 753[5:Res:744.0,717.0] || greater(e_4,e_0) -> equalish(e_4,e_3)*. % 11.58/11.82 754[5:MRR:753.0,753.1,9.0,47.0] || -> . % 11.58/11.82 755[5:Spt:754.0,742.2,744.0] || cycle(e_2,e_4)*+ -> . % 11.58/11.82 756[5:Spt:754.0,742.0,742.1,742.3] || cycle(e_0,e_3)*+ cycle(e_1,e_0) -> cycle(e_2,e_3). % 11.58/11.82 757[5:MRR:536.2,755.0] || cycle(e_0,e_2)*+ cycle(e_1,e_0) -> cycle(e_2,e_3) cycle(e_2,e_2). % 11.58/11.82 760[6:Spt:757.2] || -> cycle(e_2,e_3)*. % 11.58/11.82 801[0:Res:121.4,73.0] group_element(e_2) || -> product(e_2,e_1,e_5) product(e_2,e_1,e_4) product(e_2,e_1,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 11.58/11.82 809[0:SSi:801.0,29.0] || -> product(e_2,e_1,e_5) product(e_2,e_1,e_4) product(e_2,e_1,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 11.58/11.82 810[0:MRR:809.3,809.4,37.0,33.0] || -> product(e_2,e_1,e_5) product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 11.58/11.82 823[0:Res:122.4,71.0] group_element(e_2) || -> product(e_1,e_2,e_5) product(e_1,e_2,e_4) product(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 11.58/11.82 825[0:SSi:823.0,29.0] || -> product(e_1,e_2,e_5) product(e_1,e_2,e_4) product(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 11.58/11.82 826[0:MRR:825.3,825.4,37.0,33.0] || -> product(e_1,e_2,e_5) product(e_1,e_2,e_4) product(e_1,e_2,e_3)*. % 11.58/11.82 830[0:Res:810.2,26.2] || greater(e_3,e_2) cycle(e_2,e_0) -> product(e_2,e_1,e_5) product(e_2,e_1,e_4)*. % 11.58/11.82 832[0:Res:810.2,58.0] || product(e_1,e_2,u)* -> product(e_2,e_1,e_5) product(e_2,e_1,e_4) product(u,e_3,e_1)*. % 11.58/11.82 835[0:Res:810.2,56.0] || product(u,e_1,e_3)* -> product(e_2,e_1,e_5) product(e_2,e_1,e_4)* equalish(u,e_2). % 11.58/11.82 837[0:MRR:830.0,15.0] || cycle(e_2,e_0)+ -> product(e_2,e_1,e_5) product(e_2,e_1,e_4)*. % 11.58/11.82 841[0:Res:826.2,58.0] || product(e_2,e_1,u)* -> product(e_1,e_2,e_5) product(e_1,e_2,e_4)* product(u,e_3,e_2)*. % 11.58/11.82 846[7:Spt:837.1] || -> product(e_2,e_1,e_5)*. % 11.58/11.82 854[7:Res:846.0,27.3] || next(e_2,u)+ cycle(e_2,v) greater(v,e_0)* -> equalish(e_5,u)*. % 11.58/11.82 868[0:Res:461.4,27.3] group_element(u) || next(u,v)*+ cycle(u,w)* greater(w,e_0)* -> product(u,e_1,e_5) product(u,e_1,e_4) product(u,e_1,e_3)* equalish(e_1,u) equalish(e_2,v)*. % 11.58/11.82 887[0:Res:465.4,58.0] group_element(u) || product(u,e_1,v)*+ -> product(e_1,u,e_5) product(e_1,u,e_4) product(e_1,u,e_3)* equalish(e_1,u) product(v,e_2,u)*. % 11.58/11.82 1159[7:Res:3.0,854.0] || cycle(e_2,u) greater(u,e_0)* -> equalish(e_5,e_3)*. % 11.58/11.82 1160[7:MRR:1159.2,51.0] || cycle(e_2,u)+ greater(u,e_0)* -> . % 11.58/11.82 1162[7:Res:760.0,1160.0] || greater(e_3,e_0)* -> . % 11.58/11.82 1163[7:MRR:1162.0,8.0] || -> . % 11.58/11.82 1164[7:Spt:1163.0,837.1,846.0] || product(e_2,e_1,e_5)*+ -> . % 11.58/11.82 1165[7:Spt:1163.0,837.0,837.2] || cycle(e_2,e_0)+ -> product(e_2,e_1,e_4)*. % 11.58/11.82 1166[7:MRR:810.0,1164.0] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 11.58/11.82 1169[7:MRR:835.1,1164.0] || product(u,e_1,e_3)* -> product(e_2,e_1,e_4)* equalish(u,e_2). % 11.58/11.82 1170[7:MRR:832.1,1164.0] || product(e_1,e_2,u)* -> product(e_2,e_1,e_4) product(u,e_3,e_1)*. % 11.58/11.82 1173[8:Spt:1166.0] || -> product(e_2,e_1,e_4)*. % 11.58/11.82 1181[8:Res:1173.0,27.3] || next(e_2,u)+ cycle(e_2,v) greater(v,e_0)* -> equalish(e_4,u)*. % 11.58/11.82 1185[4:Res:729.0,495.0] || greater(e_1,e_0) -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) product(e_4,e_1,e_2)*. % 11.58/11.82 1186[4:MRR:1185.0,6.0] || -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) product(e_4,e_1,e_2)*. % 11.58/11.82 1217[0:Res:480.9,71.0] group_element(e_2) group_element(u) || -> product(e_2,u,e_5) product(e_2,u,e_4) product(e_2,u,e_3) product(e_2,u,e_2)* product(u,e_2,e_5) product(u,e_2,e_4) product(u,e_2,e_3)* product(e_1,e_1,e_2)* equalish(u,e_2). % 11.58/11.82 1238[0:SSi:1217.0,29.0] group_element(u) || -> product(e_2,u,e_5) product(e_2,u,e_4) product(e_2,u,e_3) product(e_2,u,e_2)* product(u,e_2,e_5) product(u,e_2,e_4) product(u,e_2,e_3)* product(e_1,e_1,e_2)* equalish(u,e_2). % 11.58/11.82 1239[0:MRR:1238.4,73.0] group_element(u) || -> product(e_2,u,e_5) product(e_2,u,e_4) product(e_2,u,e_3)* product(u,e_2,e_5) product(u,e_2,e_4) product(u,e_2,e_3)* product(e_1,e_1,e_2)* equalish(u,e_2). % 11.58/11.82 1514[8:Res:3.0,1181.0] || cycle(e_2,u) greater(u,e_0)* -> equalish(e_4,e_3)*. % 11.58/11.82 1515[8:MRR:1514.2,47.0] || cycle(e_2,u)+ greater(u,e_0)* -> . % 11.58/11.82 1517[8:Res:760.0,1515.0] || greater(e_3,e_0)* -> . % 11.58/11.82 1518[8:MRR:1517.0,8.0] || -> . % 11.58/11.82 1519[8:Spt:1518.0,1166.0,1173.0] || product(e_2,e_1,e_4)*+ -> . % 11.58/11.82 1520[8:Spt:1518.0,1166.1] || -> product(e_2,e_1,e_3)*. % 11.58/11.82 1524[8:MRR:1169.1,1519.0] || product(u,e_1,e_3)*+ -> equalish(u,e_2). % 11.58/11.82 1525[8:MRR:1170.1,1519.0] || product(e_1,e_2,u)*+ -> product(u,e_3,e_1)*. % 11.58/11.82 1564[9:Spt:826.0] || -> product(e_1,e_2,e_5)*. % 11.58/11.82 1568[9:Res:1564.0,58.0] || product(e_2,e_1,u)*+ -> product(u,e_5,e_2)*. % 11.58/11.82 1570[9:Res:1564.0,55.0] || product(e_1,u,e_5)*+ -> equalish(u,e_2). % 11.58/11.82 1685[9:Res:1520.0,1568.0] || -> product(e_3,e_5,e_2)*. % 11.58/11.82 1689[9:Res:1685.0,54.0] || product(e_3,e_5,u)*+ -> equalish(u,e_2). % 11.58/11.82 1690[9:Res:1685.0,55.0] || product(e_3,u,e_2)*+ -> equalish(u,e_5). % 11.58/11.82 1702[9:Res:121.4,1690.0] group_element(e_3) || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_3,e_1) equalish(e_1,e_5). % 11.58/11.82 1708[9:SSi:1702.0,30.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_3,e_1) equalish(e_1,e_5). % 11.58/11.82 1709[9:MRR:1708.3,1708.4,41.0,36.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)*. % 11.58/11.82 1777[9:Res:1709.2,73.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4)* equalish(e_1,e_3). % 11.58/11.82 1786[9:MRR:1777.2,34.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4)*. % 11.58/11.82 1822[9:Res:1786.1,58.0] || product(e_1,e_3,u)*+ -> product(e_3,e_1,e_5) product(u,e_4,e_1)*. % 11.58/11.82 1823[9:Res:1786.1,54.0] || product(e_3,e_1,u)*+ -> product(e_3,e_1,e_5)* equalish(u,e_4). % 11.58/11.82 1825[9:Res:1786.1,56.0] || product(u,e_1,e_4)*+ -> product(e_3,e_1,e_5)* equalish(u,e_3). % 11.58/11.82 1837[10:Spt:1823.0,1823.2] || product(e_3,e_1,u)*+ -> equalish(u,e_4). % 11.58/11.82 1882[11:Spt:1825.0,1825.2] || product(u,e_1,e_4)*+ -> equalish(u,e_3). % 11.58/11.82 1888[12:Spt:1822.1] || -> product(e_3,e_1,e_5)*. % 11.58/11.82 1897[12:Res:1888.0,1837.0] || -> equalish(e_5,e_4)*. % 11.58/11.82 1898[12:MRR:1897.0,52.0] || -> . % 11.58/11.82 1900[12:Spt:1898.0,1822.1,1888.0] || product(e_3,e_1,e_5)*+ -> . % 11.58/11.82 1901[12:Spt:1898.0,1822.0,1822.2] || product(e_1,e_3,u)*+ -> product(u,e_4,e_1)*. % 11.58/11.82 1907[12:Res:122.4,1901.0] group_element(e_3) || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_3,e_1) product(e_2,e_4,e_1). % 11.58/11.82 1914[12:SSi:1907.0,30.0] || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_3,e_1) product(e_2,e_4,e_1). % 11.58/11.82 1915[12:MRR:1914.3,41.0] || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* product(e_2,e_4,e_1). % 11.58/11.82 1972[4:Res:1186.3,27.3] || next(e_4,u) cycle(e_4,v) greater(v,e_0)* -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3)* equalish(e_2,u)*. % 11.58/11.82 1976[13:Spt:1915.0] || -> product(e_1,e_3,e_5)*. % 11.58/11.82 1978[13:Res:1976.0,1570.0] || -> equalish(e_3,e_2)*. % 11.58/11.82 1985[13:MRR:1978.0,42.0] || -> . % 11.58/11.82 1986[13:Spt:1985.0,1915.0,1976.0] || product(e_1,e_3,e_5)*+ -> . % 11.58/11.82 1987[13:Spt:1985.0,1915.1,1915.2,1915.3] || -> product(e_1,e_3,e_4) product(e_1,e_3,e_3)* product(e_2,e_4,e_1). % 11.58/11.82 1990[14:Spt:1987.0] || -> product(e_1,e_3,e_4)*. % 11.58/11.82 1997[14:Res:1990.0,1901.0] || -> product(e_4,e_4,e_1)*. % 11.58/11.82 1998[14:Res:1997.0,75.0] || -> equalish(e_1,e_4)*. % 11.58/11.82 2009[14:MRR:1998.0,35.0] || -> . % 11.58/11.82 2014[14:Spt:2009.0,1987.0,1990.0] || product(e_1,e_3,e_4)*+ -> . % 11.58/11.82 2015[14:Spt:2009.0,1987.1,1987.2] || -> product(e_1,e_3,e_3)* product(e_2,e_4,e_1). % 11.58/11.82 2018[15:Spt:2015.0] || -> product(e_1,e_3,e_3)*. % 11.58/11.82 2025[15:Res:2018.0,71.0] || -> equalish(e_1,e_3)*. % 11.58/11.82 2027[15:MRR:2025.0,34.0] || -> . % 11.58/11.82 2028[15:Spt:2027.0,2015.0,2018.0] || product(e_1,e_3,e_3)*+ -> . % 11.58/11.82 2029[15:Spt:2027.0,2015.1] || -> product(e_2,e_4,e_1)*. % 11.58/11.82 2037[15:Res:2029.0,55.0] || product(e_2,u,e_1)*+ -> equalish(u,e_4). % 11.58/11.82 2308[16:Spt:1186.0] || -> product(e_4,e_1,e_5)*. % 11.58/11.82 2312[16:Res:2308.0,58.0] || product(e_1,e_4,u)*+ -> product(u,e_5,e_1)*. % 11.58/11.82 2381[16:Res:122.4,2312.0] group_element(e_4) || -> product(e_1,e_4,e_5) product(e_1,e_4,e_4) product(e_1,e_4,e_3)* equalish(e_4,e_1) product(e_2,e_5,e_1). % 11.58/11.82 2390[16:SSi:2381.0,31.0] || -> product(e_1,e_4,e_5) product(e_1,e_4,e_4) product(e_1,e_4,e_3)* equalish(e_4,e_1) product(e_2,e_5,e_1). % 11.58/11.82 2391[16:MRR:2390.3,45.0] || -> product(e_1,e_4,e_5) product(e_1,e_4,e_4) product(e_1,e_4,e_3)* product(e_2,e_5,e_1). % 11.58/11.82 2433[17:Spt:2391.0] || -> product(e_1,e_4,e_5)*. % 11.58/11.82 2435[17:Res:2433.0,1570.0] || -> equalish(e_4,e_2)*. % 11.58/11.82 2442[17:MRR:2435.0,46.0] || -> . % 11.58/11.82 2443[17:Spt:2442.0,2391.0,2433.0] || product(e_1,e_4,e_5)* -> . % 11.58/11.82 2444[17:Spt:2442.0,2391.1,2391.2,2391.3] || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)* product(e_2,e_5,e_1). % 11.58/11.82 2447[18:Spt:2444.0] || -> product(e_1,e_4,e_4)*. % 11.58/11.82 2454[18:Res:2447.0,71.0] || -> equalish(e_1,e_4)*. % 11.58/11.82 2456[18:MRR:2454.0,35.0] || -> . % 11.58/11.82 2457[18:Spt:2456.0,2444.0,2447.0] || product(e_1,e_4,e_4)* -> . % 11.58/11.82 2458[18:Spt:2456.0,2444.1,2444.2] || -> product(e_1,e_4,e_3)* product(e_2,e_5,e_1). % 11.58/11.82 2461[19:Spt:2458.0] || -> product(e_1,e_4,e_3)*. % 11.58/11.82 2468[19:Res:2461.0,2312.0] || -> product(e_3,e_5,e_1)*. % 11.58/11.82 2472[19:Res:2468.0,1689.0] || -> equalish(e_1,e_2)*. % 11.58/11.82 2479[19:MRR:2472.0,33.0] || -> . % 11.58/11.82 2482[19:Spt:2479.0,2458.0,2461.0] || product(e_1,e_4,e_3)* -> . % 11.58/11.82 2483[19:Spt:2479.0,2458.1] || -> product(e_2,e_5,e_1)*. % 11.58/11.82 2494[19:Res:2483.0,2037.0] || -> equalish(e_5,e_4)*. % 11.58/11.82 2495[19:MRR:2494.0,52.0] || -> . % 11.58/11.82 2499[16:Spt:2495.0,1186.0,2308.0] || product(e_4,e_1,e_5)*+ -> . % 11.58/11.82 2500[16:Spt:2495.0,1186.1,1186.2,1186.3] || -> product(e_4,e_1,e_4) product(e_4,e_1,e_3) product(e_4,e_1,e_2)*. % 11.58/11.82 2505[16:MRR:1972.3,2499.0] || next(e_4,u) cycle(e_4,v) greater(v,e_0)* -> product(e_4,e_1,e_4) product(e_4,e_1,e_3)* equalish(e_2,u)*. % 11.58/11.82 2507[17:Spt:2500.0] || -> product(e_4,e_1,e_4)*. % 11.58/11.82 2517[17:Res:2507.0,1882.0] || -> equalish(e_4,e_3)*. % 11.58/11.82 2519[17:MRR:2517.0,47.0] || -> . % 11.58/11.82 2520[17:Spt:2519.0,2500.0,2507.0] || product(e_4,e_1,e_4)*+ -> . % 11.58/11.82 2521[17:Spt:2519.0,2500.1,2500.2] || -> product(e_4,e_1,e_3) product(e_4,e_1,e_2)*. % 11.58/11.82 2526[17:MRR:2505.3,2520.0] || next(e_4,u) cycle(e_4,v) greater(v,e_0)* -> product(e_4,e_1,e_3)* equalish(e_2,u)*. % 11.58/11.82 2528[18:Spt:2521.0] || -> product(e_4,e_1,e_3)*. % 11.58/11.82 2538[18:Res:2528.0,1524.0] || -> equalish(e_4,e_2)*. % 11.58/11.82 2540[18:MRR:2538.0,46.0] || -> . % 11.58/11.82 2541[18:Spt:2540.0,2521.0,2528.0] || product(e_4,e_1,e_3)*+ -> . % 11.58/11.82 2542[18:Spt:2540.0,2521.1] || -> product(e_4,e_1,e_2)*. % 11.58/11.82 2547[18:MRR:2526.3,2541.0] || next(e_4,u)+ cycle(e_4,v) greater(v,e_0)* -> equalish(e_2,u)*. % 11.58/11.82 2626[18:Res:5.0,2547.0] || cycle(e_4,u) greater(u,e_0)* -> equalish(e_2,e_5)*. % 11.58/11.82 2627[18:MRR:2626.2,40.0] || cycle(e_4,u)+ greater(u,e_0)* -> . % 11.58/11.82 2629[18:Res:729.0,2627.0] || greater(e_1,e_0)* -> . % 11.58/11.82 2630[18:MRR:2629.0,6.0] || -> . % 11.58/11.82 2631[11:Spt:2630.0,1825.1] || -> product(e_3,e_1,e_5)*. % 11.58/11.82 2640[11:Res:2631.0,1837.0] || -> equalish(e_5,e_4)*. % 11.58/11.82 2641[11:MRR:2640.0,52.0] || -> . % 11.58/11.82 2643[10:Spt:2641.0,1823.1] || -> product(e_3,e_1,e_5)*. % 11.58/11.82 2651[10:Res:2643.0,27.3] || next(e_3,u)+ cycle(e_3,v) greater(v,e_0)* -> equalish(e_5,u)*. % 11.58/11.82 2686[10:Res:4.0,2651.0] || cycle(e_3,u) greater(u,e_0)* -> equalish(e_5,e_4)*. % 11.58/11.82 2687[10:MRR:2686.2,52.0] || cycle(e_3,u)+ greater(u,e_0)* -> . % 11.58/11.82 2689[10:Res:716.0,2687.0] || greater(e_2,e_0)* -> . % 11.58/11.82 2690[10:MRR:2689.0,7.0] || -> . % 11.58/11.82 2691[9:Spt:2690.0,826.0,1564.0] || product(e_1,e_2,e_5)*+ -> . % 11.58/11.82 2692[9:Spt:2690.0,826.1,826.2] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)*. % 11.58/11.82 2700[10:Spt:2692.0] || -> product(e_1,e_2,e_4)*. % 11.58/11.82 2704[10:Res:2700.0,58.0] || product(e_2,e_1,u)*+ -> product(u,e_4,e_2)*. % 11.58/11.82 2706[10:Res:2700.0,55.0] || product(e_1,u,e_4)*+ -> equalish(u,e_2). % 11.58/11.82 2707[10:Res:2700.0,56.0] || product(u,e_2,e_4)*+ -> equalish(u,e_1). % 11.58/11.82 2772[10:Res:1520.0,2704.0] || -> product(e_3,e_4,e_2)*. % 11.58/11.82 2777[10:Res:2772.0,55.0] || product(e_3,u,e_2)*+ -> equalish(u,e_4). % 11.58/11.82 2778[10:Res:2772.0,56.0] || product(u,e_4,e_2)*+ -> equalish(u,e_3). % 11.58/11.82 2789[10:Res:121.4,2777.0] group_element(e_3) || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_3,e_1) equalish(e_1,e_4). % 11.58/11.82 2795[10:SSi:2789.0,30.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_3,e_1) equalish(e_1,e_4). % 11.58/11.82 2796[10:MRR:2795.3,2795.4,41.0,35.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)*. % 11.58/11.82 2803[10:Res:122.4,2778.0] group_element(e_4) || -> product(e_1,e_4,e_5) product(e_1,e_4,e_4) product(e_1,e_4,e_3)* equalish(e_4,e_1) equalish(e_1,e_3). % 11.58/11.82 2812[10:SSi:2803.0,31.0] || -> product(e_1,e_4,e_5) product(e_1,e_4,e_4) product(e_1,e_4,e_3)* equalish(e_4,e_1) equalish(e_1,e_3). % 11.58/11.82 2813[10:MRR:2812.3,2812.4,45.0,34.0] || -> product(e_1,e_4,e_5) product(e_1,e_4,e_4) product(e_1,e_4,e_3)*. % 11.58/11.82 2831[10:Res:2796.2,73.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4)* equalish(e_1,e_3). % 11.58/11.82 2840[10:MRR:2831.2,34.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4)*. % 11.58/11.82 2845[10:Res:2840.1,58.0] || product(e_1,e_3,u)*+ -> product(e_3,e_1,e_5) product(u,e_4,e_1)*. % 11.58/11.82 2846[10:Res:2840.1,54.0] || product(e_3,e_1,u)*+ -> product(e_3,e_1,e_5)* equalish(u,e_4). % 11.58/11.82 2848[10:Res:2840.1,56.0] || product(u,e_1,e_4)*+ -> product(e_3,e_1,e_5)* equalish(u,e_3). % 11.58/11.82 2854[10:Res:2813.2,58.0] || product(e_4,e_1,u)* -> product(e_1,e_4,e_5) product(e_1,e_4,e_4)* product(u,e_3,e_4)*. % 11.58/11.82 2856[10:Res:2813.2,55.0] || product(e_1,u,e_3)* -> product(e_1,e_4,e_5) product(e_1,e_4,e_4)* equalish(u,e_4). % 11.58/11.82 2857[10:Res:2813.2,56.0] || product(u,e_4,e_3)* -> product(e_1,e_4,e_5) product(e_1,e_4,e_4)* equalish(u,e_1). % 11.58/11.82 2861[11:Spt:2846.0,2846.2] || product(e_3,e_1,u)*+ -> equalish(u,e_4). % 11.58/11.82 2875[12:Spt:2848.0,2848.2] || product(u,e_1,e_4)*+ -> equalish(u,e_3). % 11.58/11.82 2882[13:Spt:2845.1] || -> product(e_3,e_1,e_5)*. % 11.58/11.82 2891[13:Res:2882.0,2861.0] || -> equalish(e_5,e_4)*. % 11.58/11.82 2892[13:MRR:2891.0,52.0] || -> . % 11.58/11.82 2894[13:Spt:2892.0,2845.1,2882.0] || product(e_3,e_1,e_5)*+ -> . % 11.58/11.82 2895[13:Spt:2892.0,2845.0,2845.2] || product(e_1,e_3,u)*+ -> product(u,e_4,e_1)*. % 11.58/11.82 2896[13:MRR:2840.0,2894.0] || -> product(e_3,e_1,e_4)*. % 11.58/11.82 2901[13:Res:122.4,2895.0] group_element(e_3) || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_3,e_1) product(e_2,e_4,e_1). % 11.58/11.82 2910[13:SSi:2901.0,30.0] || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_3,e_1) product(e_2,e_4,e_1). % 11.58/11.82 2911[13:MRR:2910.3,41.0] || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* product(e_2,e_4,e_1). % 11.58/11.82 2925[14:Spt:1186.0] || -> product(e_4,e_1,e_5)*. % 11.58/11.82 2929[14:Res:2925.0,58.0] || product(e_1,e_4,u)*+ -> product(u,e_5,e_1)*. % 11.58/11.82 2931[14:Res:2925.0,55.0] || product(e_4,u,e_5)*+ -> equalish(u,e_1). % 11.58/11.82 2967[14:Res:2813.2,2929.0] || -> product(e_1,e_4,e_5) product(e_1,e_4,e_4)* product(e_3,e_5,e_1). % 11.58/11.82 2968[15:Spt:2967.0] || -> product(e_1,e_4,e_5)*. % 11.58/11.82 2975[15:Res:2968.0,2929.0] || -> product(e_5,e_5,e_1)*. % 11.58/11.82 3004[15:Res:2975.0,75.0] || -> equalish(e_1,e_5)*. % 11.58/11.82 3015[15:MRR:3004.0,36.0] || -> . % 11.58/11.82 3020[15:Spt:3015.0,2967.0,2968.0] || product(e_1,e_4,e_5)*+ -> . % 11.58/11.82 3021[15:Spt:3015.0,2967.1,2967.2] || -> product(e_1,e_4,e_4)* product(e_3,e_5,e_1). % 11.58/11.82 3024[15:MRR:2856.1,3020.0] || product(e_1,u,e_3)* -> product(e_1,e_4,e_4)* equalish(u,e_4). % 11.58/11.82 3025[15:MRR:2857.1,3020.0] || product(u,e_4,e_3)* -> product(e_1,e_4,e_4)* equalish(u,e_1). % 11.58/11.82 3026[15:MRR:2854.1,3020.0] || product(e_4,e_1,u)* -> product(e_1,e_4,e_4)* product(u,e_3,e_4)*. % 11.58/11.82 3027[16:Spt:3021.0] || -> product(e_1,e_4,e_4)*. % 11.58/11.82 3035[16:Res:3027.0,71.0] || -> equalish(e_1,e_4)*. % 11.58/11.82 3038[16:MRR:3035.0,35.0] || -> . % 11.58/11.82 3039[16:Spt:3038.0,3021.0,3027.0] || product(e_1,e_4,e_4)*+ -> . % 11.58/11.82 3040[16:Spt:3038.0,3021.1] || -> product(e_3,e_5,e_1)*. % 11.58/11.82 3043[16:MRR:3024.1,3039.0] || product(e_1,u,e_3)*+ -> equalish(u,e_4). % 11.58/11.82 3044[16:MRR:3025.1,3039.0] || product(u,e_4,e_3)*+ -> equalish(u,e_1). % 11.58/11.82 3045[16:MRR:3026.1,3039.0] || product(e_4,e_1,u)*+ -> product(u,e_3,e_4)*. % 11.58/11.82 3242[16:Res:2925.0,3045.0] || -> product(e_5,e_3,e_4)*. % 11.58/11.82 3248[16:Res:3242.0,56.0] || product(u,e_3,e_4)*+ -> equalish(u,e_5). % 11.58/11.82 3357[17:Spt:2911.0] || -> product(e_1,e_3,e_5)*. % 11.58/11.82 3360[17:Res:3357.0,58.0] || product(e_3,e_1,u)*+ -> product(u,e_5,e_3)*. % 11.58/11.82 3363[17:Res:3357.0,56.0] || product(u,e_3,e_5)*+ -> equalish(u,e_1). % 11.58/11.82 3516[17:Res:2896.0,3360.0] || -> product(e_4,e_5,e_3)*. % 11.58/11.82 3521[17:Res:3516.0,55.0] || product(e_4,u,e_3)*+ -> equalish(u,e_5). % 11.58/11.82 7011[13:Res:2896.0,887.1] group_element(e_3) || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_1,e_3) product(e_4,e_2,e_3). % 11.58/11.82 17357[0:Res:5.0,868.1] group_element(e_4) || cycle(e_4,u) greater(u,e_0)* -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3)* equalish(e_1,e_4) equalish(e_2,e_5). % 11.58/11.82 17770[18:Spt:1239.0,1239.1,1239.2,1239.3,1239.4,1239.5,1239.6,1239.8] group_element(u) || -> product(e_2,u,e_5) product(e_2,u,e_4) product(e_2,u,e_3)* product(u,e_2,e_5) product(u,e_2,e_4) product(u,e_2,e_3)* equalish(u,e_2). % 11.58/11.82 17780[18:Res:17770.3,71.0] group_element(e_3) || -> product(e_2,e_3,e_5) product(e_2,e_3,e_4)* product(e_3,e_2,e_5) product(e_3,e_2,e_4) product(e_3,e_2,e_3) equalish(e_3,e_2) equalish(e_2,e_3). % 11.58/11.82 17781[18:Res:17770.3,3044.0] group_element(e_4) || -> product(e_2,e_4,e_5) product(e_2,e_4,e_4)* product(e_4,e_2,e_5) product(e_4,e_2,e_4) product(e_4,e_2,e_3) equalish(e_4,e_2) equalish(e_2,e_1). % 11.58/11.82 17802[18:SSi:17781.0,31.0] || -> product(e_2,e_4,e_5) product(e_2,e_4,e_4)* product(e_4,e_2,e_5) product(e_4,e_2,e_4) product(e_4,e_2,e_3) equalish(e_4,e_2) equalish(e_2,e_1). % 11.58/11.82 17803[18:MRR:17802.2,17802.5,17802.6,2931.0,46.0,37.0] || -> product(e_2,e_4,e_5) product(e_2,e_4,e_4)* product(e_4,e_2,e_4) product(e_4,e_2,e_3). % 11.58/11.82 17804[18:SSi:17780.0,30.0] || -> product(e_2,e_3,e_5) product(e_2,e_3,e_4)* product(e_3,e_2,e_5) product(e_3,e_2,e_4) product(e_3,e_2,e_3) equalish(e_3,e_2) equalish(e_2,e_3). % 11.58/11.82 17805[18:MRR:17804.4,17804.5,17804.6,73.0,42.0,38.0] || -> product(e_2,e_3,e_5) product(e_2,e_3,e_4)* product(e_3,e_2,e_5) product(e_3,e_2,e_4). % 11.58/11.82 17827[18:Res:17803.1,71.0] || -> product(e_2,e_4,e_5)* product(e_4,e_2,e_4) product(e_4,e_2,e_3) equalish(e_2,e_4). % 11.58/11.82 17828[18:MRR:17827.1,17827.3,73.0,39.0] || -> product(e_2,e_4,e_5)* product(e_4,e_2,e_3). % 11.58/11.82 17833[18:Res:17828.0,58.0] || product(e_4,e_2,u)*+ -> product(e_4,e_2,e_3)* product(u,e_5,e_4)*. % 11.58/11.82 17984[19:Spt:17833.1] || -> product(e_4,e_2,e_3)*. % 11.58/11.82 17991[19:Res:17984.0,3521.0] || -> equalish(e_2,e_5)*. % 11.58/11.82 17992[19:MRR:17991.0,40.0] || -> . % 11.58/11.82 17993[19:Spt:17992.0,17833.1,17984.0] || product(e_4,e_2,e_3)*+ -> . % 11.58/11.82 17994[19:Spt:17992.0,17833.0,17833.2] || product(e_4,e_2,u)*+ -> product(u,e_5,e_4)*. % 11.58/11.82 18180[20:Spt:17805.0] || -> product(e_2,e_3,e_5)*. % 11.58/11.82 18188[20:Res:18180.0,3363.0] || -> equalish(e_2,e_1)*. % 11.58/11.82 18190[20:MRR:18188.0,37.0] || -> . % 11.58/11.82 18192[20:Spt:18190.0,17805.0,18180.0] || product(e_2,e_3,e_5)*+ -> . % 11.58/11.82 18193[20:Spt:18190.0,17805.1,17805.2,17805.3] || -> product(e_2,e_3,e_4)* product(e_3,e_2,e_5) product(e_3,e_2,e_4). % 11.58/11.82 18194[21:Spt:18193.0] || -> product(e_2,e_3,e_4)*. % 11.58/11.82 18201[21:Res:18194.0,3248.0] || -> equalish(e_2,e_5)*. % 11.58/11.82 18202[21:MRR:18201.0,40.0] || -> . % 11.58/11.82 18204[21:Spt:18202.0,18193.0,18194.0] || product(e_2,e_3,e_4)*+ -> . % 11.58/11.82 18205[21:Spt:18202.0,18193.1,18193.2] || -> product(e_3,e_2,e_5) product(e_3,e_2,e_4)*. % 11.58/11.82 18212[21:Res:18205.1,2707.0] || -> product(e_3,e_2,e_5)* equalish(e_3,e_1). % 11.58/11.82 18214[21:MRR:18212.1,41.0] || -> product(e_3,e_2,e_5)*. % 11.58/11.82 18217[21:Res:18214.0,115.2] group_element(e_3) group_element(e_2) || -> product(e_2,e_3,e_5) product(e_2,e_3,e_4) product(e_2,e_3,e_3) product(e_2,e_3,e_2)* product(e_5,e_1,e_3). % 11.58/11.82 18222[21:SSi:18217.1,18217.0,29.0,30.0] || -> product(e_2,e_3,e_5) product(e_2,e_3,e_4) product(e_2,e_3,e_3) product(e_2,e_3,e_2)* product(e_5,e_1,e_3). % 11.58/11.82 18223[21:MRR:18222.0,18222.1,18192.0,18204.0] || -> product(e_2,e_3,e_3) product(e_2,e_3,e_2)* product(e_5,e_1,e_3). % 11.58/11.82 18652[22:Spt:18223.0] || -> product(e_2,e_3,e_3)*. % 11.58/11.82 18662[22:Res:18652.0,71.0] || -> equalish(e_2,e_3)*. % 11.58/11.82 18664[22:MRR:18662.0,38.0] || -> . % 11.58/11.82 18666[22:Spt:18664.0,18223.0,18652.0] || product(e_2,e_3,e_3)* -> . % 11.58/11.82 18667[22:Spt:18664.0,18223.1,18223.2] || -> product(e_2,e_3,e_2)* product(e_5,e_1,e_3). % 11.58/11.82 18681[22:Res:18667.0,73.0] || -> product(e_5,e_1,e_3)* equalish(e_3,e_2). % 11.58/11.82 18694[22:MRR:18681.1,42.0] || -> product(e_5,e_1,e_3)*. % 11.58/11.82 18704[22:Res:18694.0,1524.0] || -> equalish(e_5,e_2)*. % 11.58/11.82 18711[22:MRR:18704.0,50.0] || -> . % 11.58/11.82 18719[18:Spt:18711.0,1239.7] || -> product(e_1,e_1,e_2)*. % 11.58/11.82 18747[18:Res:18719.0,75.0] || -> equalish(e_2,e_1)*. % 11.58/11.82 18788[18:MRR:18747.0,37.0] || -> . % 11.58/11.82 18805[17:Spt:18788.0,2911.0,3357.0] || product(e_1,e_3,e_5)*+ -> . % 11.58/11.82 18806[17:Spt:18788.0,2911.1,2911.2,2911.3] || -> product(e_1,e_3,e_4) product(e_1,e_3,e_3)* product(e_2,e_4,e_1). % 11.58/11.82 18809[13:SSi:7011.0,30.0] || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_1,e_3) product(e_4,e_2,e_3). % 11.58/11.82 18810[13:MRR:18809.2,18809.3,71.0,34.0] || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4)* product(e_4,e_2,e_3). % 11.58/11.82 18811[17:MRR:18810.0,18805.0] || -> product(e_1,e_3,e_4)* product(e_4,e_2,e_3). % 11.58/11.82 18858[18:Spt:18806.0] || -> product(e_1,e_3,e_4)*. % 11.58/11.82 18866[18:Res:18858.0,3248.0] || -> equalish(e_1,e_5)*. % 11.58/11.82 18872[18:MRR:18866.0,36.0] || -> . % 11.58/11.82 18878[18:Spt:18872.0,18806.0,18858.0] || product(e_1,e_3,e_4)*+ -> . % 11.58/11.82 18879[18:Spt:18872.0,18806.1,18806.2] || -> product(e_1,e_3,e_3)* product(e_2,e_4,e_1). % 11.58/11.82 18880[18:MRR:18811.0,18878.0] || -> product(e_4,e_2,e_3)*. % 11.58/11.82 18883[19:Spt:18879.0] || -> product(e_1,e_3,e_3)*. % 11.58/11.82 18892[19:Res:18883.0,71.0] || -> equalish(e_1,e_3)*. % 11.58/11.82 18898[19:MRR:18892.0,34.0] || -> . % 11.58/11.82 18904[19:Spt:18898.0,18879.0,18883.0] || product(e_1,e_3,e_3)*+ -> . % 11.58/11.82 18905[19:Spt:18898.0,18879.1] || -> product(e_2,e_4,e_1)*. % 11.58/11.82 18920[18:Res:18880.0,58.0] || product(e_2,e_4,u)*+ -> product(u,e_3,e_2)*. % 11.58/11.82 19242[19:Res:18905.0,18920.0] || -> product(e_1,e_3,e_2)*. % 11.58/11.82 19251[19:Res:19242.0,55.0] || product(e_1,u,e_2)*+ -> equalish(u,e_3). % 11.58/11.82 19954[19:Res:465.4,19251.0] group_element(u) || -> product(e_1,u,e_5) product(e_1,u,e_4) product(e_1,u,e_3)* equalish(e_1,u) equalish(u,e_3). % 11.58/11.82 19990[19:Res:19954.3,3043.0] group_element(u) || -> product(e_1,u,e_5) product(e_1,u,e_4)* equalish(e_1,u) equalish(u,e_3) equalish(u,e_4). % 11.58/11.82 20046[19:Res:19990.2,2706.0] group_element(u) || -> product(e_1,u,e_5)* equalish(e_1,u) equalish(u,e_3) equalish(u,e_4) equalish(u,e_2). % 11.58/11.82 20114[19:Res:20046.1,71.0] group_element(e_5) || -> equalish(e_1,e_5)* equalish(e_5,e_3) equalish(e_5,e_4) equalish(e_5,e_2) equalish(e_1,e_5)*. % 11.58/11.82 20129[19:Obv:20114.1] group_element(e_5) || -> equalish(e_5,e_3) equalish(e_5,e_4) equalish(e_5,e_2) equalish(e_1,e_5)*. % 11.58/11.82 20130[19:SSi:20129.0,32.0] || -> equalish(e_5,e_3) equalish(e_5,e_4) equalish(e_5,e_2) equalish(e_1,e_5)*. % 11.58/11.82 20131[19:MRR:20130.0,20130.1,20130.2,20130.3,51.0,52.0,50.0,36.0] || -> . % 11.58/11.82 20148[14:Spt:20131.0,1186.0,2925.0] || product(e_4,e_1,e_5)*+ -> . % 11.58/11.82 20149[14:Spt:20131.0,1186.1,1186.2,1186.3] || -> product(e_4,e_1,e_4) product(e_4,e_1,e_3) product(e_4,e_1,e_2)*. % 11.58/11.82 20155[0:SSi:17357.0,31.0] || cycle(e_4,u) greater(u,e_0)* -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3)* equalish(e_1,e_4) equalish(e_2,e_5). % 11.58/11.82 20156[0:MRR:20155.3,20155.5,20155.6,73.0,35.0,40.0] || cycle(e_4,u) greater(u,e_0)* -> product(e_4,e_1,e_5) product(e_4,e_1,e_3)*. % 11.58/11.82 20157[14:MRR:20156.2,20148.0] || cycle(e_4,u) greater(u,e_0)* -> product(e_4,e_1,e_3)*. % 11.58/11.82 20216[15:Spt:20149.0] || -> product(e_4,e_1,e_4)*. % 11.58/11.82 20228[15:Res:20216.0,2875.0] || -> equalish(e_4,e_3)*. % 11.58/11.82 20232[15:MRR:20228.0,47.0] || -> . % 11.58/11.82 20238[15:Spt:20232.0,20149.0,20216.0] || product(e_4,e_1,e_4)*+ -> . % 11.58/11.82 20239[15:Spt:20232.0,20149.1,20149.2] || -> product(e_4,e_1,e_3) product(e_4,e_1,e_2)*. % 11.58/11.82 20244[16:Spt:20239.0] || -> product(e_4,e_1,e_3)*. % 11.58/11.82 20254[16:Res:20244.0,1524.0] || -> equalish(e_4,e_2)*. % 11.58/11.82 20257[16:MRR:20254.0,46.0] || -> . % 11.58/11.82 20262[16:Spt:20257.0,20239.0,20244.0] || product(e_4,e_1,e_3)*+ -> . % 11.58/11.82 20263[16:Spt:20257.0,20239.1] || -> product(e_4,e_1,e_2)*. % 11.58/11.82 20264[16:MRR:20157.2,20262.0] || cycle(e_4,u)+ greater(u,e_0)* -> . % 11.58/11.82 20305[16:Res:729.0,20264.0] || greater(e_1,e_0)* -> . % 11.58/11.82 20306[16:MRR:20305.0,6.0] || -> . % 11.58/11.82 20307[12:Spt:20306.0,2848.1] || -> product(e_3,e_1,e_5)*. % 11.58/11.82 20319[12:Res:20307.0,2861.0] || -> equalish(e_5,e_4)*. % 11.58/11.82 20320[12:MRR:20319.0,52.0] || -> . % 11.58/11.82 20331[11:Spt:20320.0,2846.1] || -> product(e_3,e_1,e_5)*. % 11.58/11.82 20348[11:Res:20331.0,58.0] || product(e_1,e_3,u)*+ -> product(u,e_5,e_1)*. % 11.58/11.82 20351[11:Res:20331.0,56.0] || product(u,e_1,e_5)*+ -> equalish(u,e_3). % 11.58/11.82 20511[11:Res:465.4,20348.0] group_element(e_3) || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_1,e_3) product(e_2,e_5,e_1). % 11.58/11.82 20514[11:SSi:20511.0,30.0] || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_1,e_3) product(e_2,e_5,e_1). % 11.58/11.82 20515[11:MRR:20514.2,20514.3,71.0,34.0] || -> product(e_1,e_3,e_5) product(e_1,e_3,e_4)* product(e_2,e_5,e_1). % 11.58/11.82 20517[12:Spt:2813.0] || -> product(e_1,e_4,e_5)*. % 11.58/11.82 20520[12:Res:20517.0,58.0] || product(e_4,e_1,u)*+ -> product(u,e_5,e_4)*. % 11.58/11.82 20522[12:Res:20517.0,55.0] || product(e_1,u,e_5)*+ -> equalish(u,e_4). % 11.58/11.82 20666[12:Res:461.4,20520.0] group_element(e_4) || -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) equalish(e_1,e_4) product(e_2,e_5,e_4)*. % 11.58/11.82 20687[12:SSi:20666.0,31.0] || -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) equalish(e_1,e_4) product(e_2,e_5,e_4)*. % 11.58/11.82 20688[12:MRR:20687.1,20687.3,73.0,35.0] || -> product(e_4,e_1,e_5) product(e_4,e_1,e_3) product(e_2,e_5,e_4)*. % 11.58/11.82 20689[13:Spt:20515.0] || -> product(e_1,e_3,e_5)*. % 11.58/11.82 20700[13:Res:20689.0,20522.0] || -> equalish(e_3,e_4)*. % 11.58/11.82 20701[13:MRR:20700.0,43.0] || -> . % 11.58/11.82 20707[13:Spt:20701.0,20515.0,20689.0] || product(e_1,e_3,e_5)*+ -> . % 11.58/11.82 20708[13:Spt:20701.0,20515.1,20515.2] || -> product(e_1,e_3,e_4)* product(e_2,e_5,e_1). % 11.58/11.82 20711[14:Spt:20708.0] || -> product(e_1,e_3,e_4)*. % 11.58/11.82 20713[14:Res:20711.0,2706.0] || -> equalish(e_3,e_2)*. % 11.58/11.82 20723[14:MRR:20713.0,42.0] || -> . % 11.58/11.82 20729[14:Spt:20723.0,20708.0,20711.0] || product(e_1,e_3,e_4)*+ -> . % 11.58/11.82 20730[14:Spt:20723.0,20708.1] || -> product(e_2,e_5,e_1)*. % 11.58/11.82 20737[14:Res:20730.0,54.0] || product(e_2,e_5,u)*+ -> equalish(u,e_1). % 11.58/11.82 20878[15:Spt:20688.0] || -> product(e_4,e_1,e_5)*. % 11.58/11.82 20888[15:Res:20878.0,20351.0] || -> equalish(e_4,e_3)*. % 11.58/11.82 20892[15:MRR:20888.0,47.0] || -> . % 11.58/11.82 20897[15:Spt:20892.0,20688.0,20878.0] || product(e_4,e_1,e_5)* -> . % 11.58/11.82 20898[15:Spt:20892.0,20688.1,20688.2] || -> product(e_4,e_1,e_3) product(e_2,e_5,e_4)*. % 11.58/11.82 20905[16:Spt:20898.0] || -> product(e_4,e_1,e_3)*. % 11.58/11.82 20915[16:Res:20905.0,1524.0] || -> equalish(e_4,e_2)*. % 11.58/11.82 20919[16:MRR:20915.0,46.0] || -> . % 11.58/11.82 20924[16:Spt:20919.0,20898.0,20905.0] || product(e_4,e_1,e_3)* -> . % 11.58/11.82 20925[16:Spt:20919.0,20898.1] || -> product(e_2,e_5,e_4)*. % 11.58/11.82 20933[16:Res:20925.0,20737.0] || -> equalish(e_4,e_1)*. % 11.58/11.82 20939[16:MRR:20933.0,45.0] || -> . % 11.58/11.82 20943[12:Spt:20939.0,2813.0,20517.0] || product(e_1,e_4,e_5)*+ -> . % 11.58/11.82 20944[12:Spt:20939.0,2813.1,2813.2] || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)*. % 11.58/11.82 20948[12:MRR:2854.1,20943.0] || product(e_4,e_1,u)* -> product(e_1,e_4,e_4)* product(u,e_3,e_4)*. % 11.58/11.82 20949[13:Spt:20944.0] || -> product(e_1,e_4,e_4)*. % 11.58/11.82 20958[13:Res:20949.0,71.0] || -> equalish(e_1,e_4)*. % 11.58/11.82 20963[13:MRR:20958.0,35.0] || -> . % 11.58/11.82 20980[13:Spt:20963.0,20944.0,20949.0] || product(e_1,e_4,e_4)*+ -> . % 11.58/11.82 20981[13:Spt:20963.0,20944.1] || -> product(e_1,e_4,e_3)*. % 11.58/11.82 20985[13:MRR:20948.1,20980.0] || product(e_4,e_1,u)*+ -> product(u,e_3,e_4)*. % 11.58/11.82 21118[13:Res:461.4,20985.0] group_element(e_4) || -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) equalish(e_1,e_4) product(e_2,e_3,e_4)*. % 11.58/11.82 21138[13:SSi:21118.0,31.0] || -> product(e_4,e_1,e_5) product(e_4,e_1,e_4) product(e_4,e_1,e_3) equalish(e_1,e_4) product(e_2,e_3,e_4)*. % 11.58/11.82 21139[13:MRR:21138.1,21138.3,73.0,35.0] || -> product(e_4,e_1,e_5) product(e_4,e_1,e_3) product(e_2,e_3,e_4)*. % 11.58/11.82 21140[14:Spt:20515.0] || -> product(e_1,e_3,e_5)*. % 11.58/11.82 21148[14:Res:21140.0,20348.0] || -> product(e_5,e_5,e_1)*. % 11.58/11.82 21164[14:Res:21148.0,75.0] || -> equalish(e_1,e_5)*. % 11.58/11.82 21175[14:MRR:21164.0,36.0] || -> . % 11.58/11.82 21180[14:Spt:21175.0,20515.0,21140.0] || product(e_1,e_3,e_5)*+ -> . % 11.58/11.82 21181[14:Spt:21175.0,20515.1,20515.2] || -> product(e_1,e_3,e_4)* product(e_2,e_5,e_1). % 11.58/11.82 21184[15:Spt:21181.0] || -> product(e_1,e_3,e_4)*. % 11.58/11.82 21186[15:Res:21184.0,2706.0] || -> equalish(e_3,e_2)*. % 11.58/11.82 21196[15:MRR:21186.0,42.0] || -> . % 11.58/11.82 21202[15:Spt:21196.0,21181.0,21184.0] || product(e_1,e_3,e_4)*+ -> . % 11.58/11.82 21203[15:Spt:21196.0,21181.1] || -> product(e_2,e_5,e_1)*. % 11.58/11.82 21351[16:Spt:21139.0] || -> product(e_4,e_1,e_5)*. % 11.58/11.82 21361[16:Res:21351.0,20351.0] || -> equalish(e_4,e_3)*. % 11.58/11.82 21365[16:MRR:21361.0,47.0] || -> . % 11.58/11.82 21370[16:Spt:21365.0,21139.0,21351.0] || product(e_4,e_1,e_5)*+ -> . % 11.58/11.82 21371[16:Spt:21365.0,21139.1,21139.2] || -> product(e_4,e_1,e_3) product(e_2,e_3,e_4)*. % 11.58/11.82 21372[16:MRR:20156.2,21370.0] || cycle(e_4,u) greater(u,e_0)* -> product(e_4,e_1,e_3)*. % 11.58/11.82 21378[17:Spt:21371.0] || -> product(e_4,e_1,e_3)*. % 11.58/11.82 21388[17:Res:21378.0,1524.0] || -> equalish(e_4,e_2)*. % 11.58/11.82 21392[17:MRR:21388.0,46.0] || -> . % 11.58/11.82 21397[17:Spt:21392.0,21371.0,21378.0] || product(e_4,e_1,e_3)*+ -> . % 11.58/11.82 21398[17:Spt:21392.0,21371.1] || -> product(e_2,e_3,e_4)*. % 11.58/11.82 21399[17:MRR:21372.2,21397.0] || cycle(e_4,u)+ greater(u,e_0)* -> . % 11.58/11.82 21475[17:Res:729.0,21399.0] || greater(e_1,e_0)* -> . % 11.58/11.82 21476[17:MRR:21475.0,6.0] || -> . % 11.58/11.82 21477[10:Spt:21476.0,2692.0,2700.0] || product(e_1,e_2,e_4)* -> . % 11.58/11.82 21478[10:Spt:21476.0,2692.1] || -> product(e_1,e_2,e_3)*. % 11.58/11.82 21577[10:Res:21478.0,1525.0] || -> product(e_3,e_3,e_1)*. % 11.58/11.82 21594[10:Res:21577.0,75.0] || -> equalish(e_1,e_3)*. % 11.58/11.82 21605[10:MRR:21594.0,34.0] || -> . % 11.58/11.82 21610[6:Spt:21605.0,757.2,760.0] || cycle(e_2,e_3)*+ -> . % 11.58/11.82 21611[6:Spt:21605.0,757.0,757.1,757.3] || cycle(e_0,e_2)*+ cycle(e_1,e_0) -> cycle(e_2,e_2). % 11.58/11.82 21644[7:Spt:826.0] || -> product(e_1,e_2,e_5)*. % 11.58/11.82 21647[7:Res:21644.0,58.0] || product(e_2,e_1,u)*+ -> product(u,e_5,e_2)*. % 11.58/11.82 21852[8:Spt:810.0] || -> product(e_2,e_1,e_5)*. % 11.58/11.82 21856[8:Res:21852.0,21647.0] || -> product(e_5,e_5,e_2)*. % 11.58/11.82 21888[8:Res:21856.0,75.0] || -> equalish(e_2,e_5)*. % 11.58/11.82 21905[8:MRR:21888.0,40.0] || -> . % 11.58/11.82 21908[8:Spt:21905.0,810.0,21852.0] || product(e_2,e_1,e_5)*+ -> . % 11.58/11.82 21909[8:Spt:21905.0,810.1,810.2] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 11.58/11.82 21910[8:MRR:837.1,21908.0] || cycle(e_2,e_0) -> product(e_2,e_1,e_4)*. % 11.58/11.82 21917[9:Spt:21909.0] || -> product(e_2,e_1,e_4)*. % 11.58/11.82 21920[9:Res:21917.0,26.2] || greater(e_4,e_2)* cycle(e_2,e_0) -> . % 11.58/11.82 21930[9:MRR:21920.0,16.0] || cycle(e_2,e_0)*+ -> . % 11.58/11.82 21960[9:Res:22.5,21930.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 21961[9:SSi:21960.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 21962[9:MRR:21961.0,21961.1,755.0,21610.0] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 21963[10:Spt:21962.0] || -> cycle(e_2,e_2)*. % 11.58/11.82 21967[10:Res:21963.0,717.0] || greater(e_2,e_0) -> equalish(e_2,e_3)*. % 11.58/11.82 21968[10:MRR:21967.0,21967.1,7.0,38.0] || -> . % 11.58/11.82 21969[10:Spt:21968.0,21962.0,21963.0] || cycle(e_2,e_2)* -> . % 11.58/11.82 21970[10:Spt:21968.0,21962.1] || -> cycle(e_2,e_1)*. % 11.58/11.82 21975[10:Res:21970.0,717.0] || greater(e_1,e_0) -> equalish(e_1,e_3)*. % 11.58/11.82 21976[10:MRR:21975.0,21975.1,6.0,34.0] || -> . % 11.58/11.82 21977[9:Spt:21976.0,21909.0,21917.0] || product(e_2,e_1,e_4)*+ -> . % 11.58/11.82 21978[9:Spt:21976.0,21909.1] || -> product(e_2,e_1,e_3)*. % 11.58/11.82 21979[9:MRR:21910.1,21977.0] || cycle(e_2,e_0)*+ -> . % 11.58/11.82 22010[9:Res:22.5,21979.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22011[9:SSi:22010.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22012[9:MRR:22011.0,22011.1,755.0,21610.0] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22027[10:Spt:22012.0] || -> cycle(e_2,e_2)*. % 11.58/11.82 22031[10:Res:22027.0,717.0] || greater(e_2,e_0) -> equalish(e_2,e_3)*. % 11.58/11.82 22032[10:MRR:22031.0,22031.1,7.0,38.0] || -> . % 11.58/11.82 22033[10:Spt:22032.0,22012.0,22027.0] || cycle(e_2,e_2)* -> . % 11.58/11.82 22034[10:Spt:22032.0,22012.1] || -> cycle(e_2,e_1)*. % 11.58/11.82 22039[10:Res:22034.0,717.0] || greater(e_1,e_0) -> equalish(e_1,e_3)*. % 11.58/11.82 22040[10:MRR:22039.0,22039.1,6.0,34.0] || -> . % 11.58/11.82 22041[7:Spt:22040.0,826.0,21644.0] || product(e_1,e_2,e_5)*+ -> . % 11.58/11.82 22042[7:Spt:22040.0,826.1,826.2] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)*. % 11.58/11.82 22046[7:MRR:841.1,22041.0] || product(e_2,e_1,u)* -> product(e_1,e_2,e_4)* product(u,e_3,e_2)*. % 11.58/11.82 22047[8:Spt:22042.0] || -> product(e_1,e_2,e_4)*. % 11.58/11.82 22050[8:Res:22047.0,58.0] || product(e_2,e_1,u)*+ -> product(u,e_4,e_2)*. % 11.58/11.82 22210[9:Spt:837.1] || -> product(e_2,e_1,e_5)*. % 11.58/11.82 22213[9:Res:22210.0,26.2] || greater(e_5,e_2)* cycle(e_2,e_0) -> . % 11.58/11.82 22223[9:MRR:22213.0,17.0] || cycle(e_2,e_0)*+ -> . % 11.58/11.82 22252[9:Res:22.5,22223.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22253[9:SSi:22252.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22254[9:MRR:22253.0,22253.1,755.0,21610.0] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22255[10:Spt:22254.0] || -> cycle(e_2,e_2)*. % 11.58/11.82 22259[10:Res:22255.0,717.0] || greater(e_2,e_0) -> equalish(e_2,e_3)*. % 11.58/11.82 22260[10:MRR:22259.0,22259.1,7.0,38.0] || -> . % 11.58/11.82 22261[10:Spt:22260.0,22254.0,22255.0] || cycle(e_2,e_2)* -> . % 11.58/11.82 22262[10:Spt:22260.0,22254.1] || -> cycle(e_2,e_1)*. % 11.58/11.82 22267[10:Res:22262.0,717.0] || greater(e_1,e_0) -> equalish(e_1,e_3)*. % 11.58/11.82 22268[10:MRR:22267.0,22267.1,6.0,34.0] || -> . % 11.58/11.82 22269[9:Spt:22268.0,837.1,22210.0] || product(e_2,e_1,e_5)*+ -> . % 11.58/11.82 22270[9:Spt:22268.0,837.0,837.2] || cycle(e_2,e_0)+ -> product(e_2,e_1,e_4)*. % 11.58/11.82 22271[9:MRR:810.0,22269.0] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 11.58/11.82 22278[9:Res:22.5,22270.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 11.58/11.82 22279[9:SSi:22278.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 11.58/11.82 22280[9:MRR:22279.0,22279.1,755.0,21610.0] || -> cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 11.58/11.82 22281[10:Spt:22271.0] || -> product(e_2,e_1,e_4)*. % 11.58/11.82 22285[10:Res:22281.0,22050.0] || -> product(e_4,e_4,e_2)*. % 11.58/11.82 22318[10:Res:22285.0,75.0] || -> equalish(e_2,e_4)*. % 11.58/11.82 22335[10:MRR:22318.0,39.0] || -> . % 11.58/11.82 22338[10:Spt:22335.0,22271.0,22281.0] || product(e_2,e_1,e_4)*+ -> . % 11.58/11.82 22339[10:Spt:22335.0,22271.1] || -> product(e_2,e_1,e_3)*. % 11.58/11.82 22341[10:MRR:22280.2,22338.0] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22387[11:Spt:22341.0] || -> cycle(e_2,e_2)*. % 11.58/11.82 22391[11:Res:22387.0,717.0] || greater(e_2,e_0) -> equalish(e_2,e_3)*. % 11.58/11.82 22392[11:MRR:22391.0,22391.1,7.0,38.0] || -> . % 11.58/11.82 22393[11:Spt:22392.0,22341.0,22387.0] || cycle(e_2,e_2)* -> . % 11.58/11.82 22394[11:Spt:22392.0,22341.1] || -> cycle(e_2,e_1)*. % 11.58/11.82 22399[11:Res:22394.0,717.0] || greater(e_1,e_0) -> equalish(e_1,e_3)*. % 11.58/11.82 22400[11:MRR:22399.0,22399.1,6.0,34.0] || -> . % 11.58/11.82 22401[8:Spt:22400.0,22042.0,22047.0] || product(e_1,e_2,e_4)*+ -> . % 11.58/11.82 22402[8:Spt:22400.0,22042.1] || -> product(e_1,e_2,e_3)*. % 11.58/11.82 22406[8:MRR:22046.1,22401.0] || product(e_2,e_1,u)*+ -> product(u,e_3,e_2)*. % 11.58/11.82 22569[9:Spt:810.0] || -> product(e_2,e_1,e_5)*. % 11.58/11.82 22572[9:Res:22569.0,26.2] || greater(e_5,e_2)* cycle(e_2,e_0) -> . % 11.58/11.82 22582[9:MRR:22572.0,17.0] || cycle(e_2,e_0)*+ -> . % 11.58/11.82 22613[9:Res:22.5,22582.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22614[9:SSi:22613.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22615[9:MRR:22614.0,22614.1,755.0,21610.0] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22616[10:Spt:22615.0] || -> cycle(e_2,e_2)*. % 11.58/11.82 22620[10:Res:22616.0,717.0] || greater(e_2,e_0) -> equalish(e_2,e_3)*. % 11.58/11.82 22621[10:MRR:22620.0,22620.1,7.0,38.0] || -> . % 11.58/11.82 22622[10:Spt:22621.0,22615.0,22616.0] || cycle(e_2,e_2)* -> . % 11.58/11.82 22623[10:Spt:22621.0,22615.1] || -> cycle(e_2,e_1)*. % 11.58/11.82 22628[10:Res:22623.0,717.0] || greater(e_1,e_0) -> equalish(e_1,e_3)*. % 11.58/11.82 22629[10:MRR:22628.0,22628.1,6.0,34.0] || -> . % 11.58/11.82 22630[9:Spt:22629.0,810.0,22569.0] || product(e_2,e_1,e_5)*+ -> . % 11.58/11.82 22631[9:Spt:22629.0,810.1,810.2] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 11.58/11.82 22639[10:Spt:22631.0] || -> product(e_2,e_1,e_4)*. % 11.58/11.82 22642[10:Res:22639.0,26.2] || greater(e_4,e_2)* cycle(e_2,e_0) -> . % 11.58/11.82 22652[10:MRR:22642.0,16.0] || cycle(e_2,e_0)*+ -> . % 11.58/11.82 22682[10:Res:22.5,22652.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22683[10:SSi:22682.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22684[10:MRR:22683.0,22683.1,755.0,21610.0] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22685[11:Spt:22684.0] || -> cycle(e_2,e_2)*. % 11.58/11.82 22689[11:Res:22685.0,717.0] || greater(e_2,e_0) -> equalish(e_2,e_3)*. % 11.58/11.82 22690[11:MRR:22689.0,22689.1,7.0,38.0] || -> . % 11.58/11.82 22691[11:Spt:22690.0,22684.0,22685.0] || cycle(e_2,e_2)* -> . % 11.58/11.82 22692[11:Spt:22690.0,22684.1] || -> cycle(e_2,e_1)*. % 11.58/11.82 22697[11:Res:22692.0,717.0] || greater(e_1,e_0) -> equalish(e_1,e_3)*. % 11.58/11.82 22698[11:MRR:22697.0,22697.1,6.0,34.0] || -> . % 11.58/11.82 22699[10:Spt:22698.0,22631.0,22639.0] || product(e_2,e_1,e_4)* -> . % 11.58/11.82 22700[10:Spt:22698.0,22631.1] || -> product(e_2,e_1,e_3)*. % 11.58/11.82 22723[10:Res:22700.0,22406.0] || -> product(e_3,e_3,e_2)*. % 11.58/11.82 22743[10:Res:22723.0,75.0] || -> equalish(e_2,e_3)*. % 11.58/11.82 22760[10:MRR:22743.0,38.0] || -> . % 11.58/11.82 22763[4:Spt:22760.0,724.3,729.0] || cycle(e_4,e_1)*+ -> . % 11.58/11.82 22764[4:Spt:22760.0,724.0,724.1,724.2] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2)*. % 11.58/11.82 22767[5:Spt:22764.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 22779[5:Res:22767.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 22780[5:MRR:22779.0,22779.1,9.0,45.0] || -> . % 11.58/11.82 22781[5:Spt:22780.0,22764.0,22767.0] || cycle(e_4,e_4)* -> . % 11.58/11.82 22782[5:Spt:22780.0,22764.1,22764.2] || -> cycle(e_4,e_3) cycle(e_4,e_2)*. % 11.58/11.82 22783[6:Spt:22782.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 22788[6:Res:22783.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 22789[6:MRR:22788.0,22788.1,8.0,41.0] || -> . % 11.58/11.82 22790[6:Spt:22789.0,22782.0,22783.0] || cycle(e_4,e_3)* -> . % 11.58/11.82 22791[6:Spt:22789.0,22782.1] || -> cycle(e_4,e_2)*. % 11.58/11.82 22798[6:Res:22791.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 22799[6:MRR:22798.0,22798.1,7.0,37.0] || -> . % 11.58/11.82 22800[3:Spt:22799.0,711.2,716.0] || cycle(e_3,e_2)*+ -> . % 11.58/11.82 22801[3:Spt:22799.0,711.0,711.1,711.3] || cycle(e_0,e_1)*+ cycle(e_2,e_0) -> cycle(e_3,e_1). % 11.58/11.82 22813[4:Spt:837.1] || -> product(e_2,e_1,e_5)*. % 11.58/11.82 22816[4:Res:22813.0,26.2] || greater(e_5,e_2)* cycle(e_2,e_0) -> . % 11.58/11.82 22818[4:Res:22813.0,58.0] || product(e_1,e_2,u)*+ -> product(u,e_5,e_1)*. % 11.58/11.82 22822[4:Res:22813.0,27.3] || next(e_2,u)+ cycle(e_2,v) greater(v,e_0)* -> equalish(e_5,u)*. % 11.58/11.82 22825[4:MRR:22816.0,17.0] || cycle(e_2,e_0)*+ -> . % 11.58/11.82 22840[4:Res:22.5,22825.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 22841[4:SSi:22840.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 23031[5:Spt:826.0] || -> product(e_1,e_2,e_5)*. % 11.58/11.82 23039[5:Res:23031.0,22818.0] || -> product(e_5,e_5,e_1)*. % 11.58/11.82 23062[5:Res:23039.0,75.0] || -> equalish(e_1,e_5)*. % 11.58/11.82 23073[5:MRR:23062.0,36.0] || -> . % 11.58/11.82 23078[5:Spt:23073.0,826.0,23031.0] || product(e_1,e_2,e_5)*+ -> . % 11.58/11.82 23079[5:Spt:23073.0,826.1,826.2] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)*. % 11.58/11.82 23536[6:Spt:22841.1] || -> cycle(e_2,e_3)*. % 11.58/11.82 23537[6:MRR:540.0,23536.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 23541[6:MRR:555.1,23536.0] || cycle(e_4,e_1)+ cycle(e_3,e_0)* -> . % 11.58/11.82 23552[6:Res:22.5,23537.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 23553[6:SSi:23552.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 23556[7:Spt:23553.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 23564[7:Res:23556.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 23565[7:MRR:23564.0,23564.1,9.0,45.0] || -> . % 11.58/11.82 23566[7:Spt:23565.0,23553.0,23556.0] || cycle(e_4,e_4)*+ -> . % 11.58/11.82 23567[7:Spt:23565.0,23553.1,23553.2,23553.3] || -> cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 23569[8:Spt:23567.1] || -> cycle(e_4,e_2)*. % 11.58/11.82 23574[8:Res:23569.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 23575[8:MRR:23574.0,23574.1,7.0,37.0] || -> . % 11.58/11.82 23576[8:Spt:23575.0,23567.1,23569.0] || cycle(e_4,e_2)*+ -> . % 11.58/11.82 23577[8:Spt:23575.0,23567.0,23567.2] || -> cycle(e_4,e_3) cycle(e_4,e_1)*. % 11.58/11.82 23578[9:Spt:23577.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 23582[9:Res:23578.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 23583[9:MRR:23582.0,23582.1,8.0,41.0] || -> . % 11.58/11.82 23584[9:Spt:23583.0,23577.0,23578.0] || cycle(e_4,e_3)*+ -> . % 11.58/11.82 23585[9:Spt:23583.0,23577.1] || -> cycle(e_4,e_1)*. % 11.58/11.82 23586[9:MRR:139.0,23585.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 23587[9:MRR:23541.0,23585.0] || cycle(e_3,e_0)*+ -> . % 11.58/11.82 23591[9:Res:22.5,23587.0] group_element(e_3) || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 11.58/11.82 23592[9:SSi:23591.0,30.0] || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 11.58/11.82 23593[9:MRR:23592.0,23592.1,23592.2,637.0,706.0,22800.0] || -> cycle(e_3,e_1)*. % 11.58/11.82 23600[9:Res:23593.0,23586.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 23601[9:MRR:23600.0,23600.1,6.0,33.0] || -> . % 11.58/11.82 23602[6:Spt:23601.0,22841.1,23536.0] || cycle(e_2,e_3)*+ -> . % 11.58/11.82 23603[6:Spt:23601.0,22841.0,22841.2,22841.3] || -> cycle(e_2,e_4) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 23606[7:Spt:23603.2] || -> cycle(e_2,e_1)*. % 11.58/11.82 25826[4:Res:3.0,22822.0] || cycle(e_2,u) greater(u,e_0)* -> equalish(e_5,e_3)*. % 11.58/11.82 25827[4:MRR:25826.2,51.0] || cycle(e_2,u)+ greater(u,e_0)* -> . % 11.58/11.82 25829[7:Res:23606.0,25827.0] || greater(e_1,e_0)* -> . % 11.58/11.82 25830[7:MRR:25829.0,6.0] || -> . % 11.58/11.82 25831[7:Spt:25830.0,23603.2,23606.0] || cycle(e_2,e_1)* -> . % 11.58/11.82 25832[7:Spt:25830.0,23603.0,23603.1] || -> cycle(e_2,e_4) cycle(e_2,e_2)*. % 11.58/11.82 25834[8:Spt:25832.0] || -> cycle(e_2,e_4)*. % 11.58/11.82 25852[8:Res:25834.0,25827.0] || greater(e_4,e_0)* -> . % 11.58/11.82 25853[8:MRR:25852.0,9.0] || -> . % 11.58/11.82 25854[8:Spt:25853.0,25832.0,25834.0] || cycle(e_2,e_4)* -> . % 11.58/11.82 25855[8:Spt:25853.0,25832.1] || -> cycle(e_2,e_2)*. % 11.58/11.82 25867[8:Res:25855.0,25827.0] || greater(e_2,e_0)* -> . % 11.58/11.82 25868[8:MRR:25867.0,7.0] || -> . % 11.58/11.82 25869[4:Spt:25868.0,837.1,22813.0] || product(e_2,e_1,e_5)*+ -> . % 11.58/11.82 25870[4:Spt:25868.0,837.0,837.2] || cycle(e_2,e_0)+ -> product(e_2,e_1,e_4)*. % 11.58/11.82 25871[4:MRR:810.0,25869.0] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 11.58/11.82 25875[4:MRR:832.1,25869.0] || product(e_1,e_2,u)* -> product(e_2,e_1,e_4) product(u,e_3,e_1)*. % 11.58/11.82 25877[4:Res:22.5,25870.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 11.58/11.82 25878[4:SSi:25877.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 11.58/11.82 25880[5:Spt:25871.0] || -> product(e_2,e_1,e_4)*. % 11.58/11.82 25883[5:Res:25880.0,26.2] || greater(e_4,e_2)* cycle(e_2,e_0) -> . % 11.58/11.82 25889[5:Res:25880.0,27.3] || next(e_2,u)+ cycle(e_2,v) greater(v,e_0)* -> equalish(e_4,u)*. % 11.58/11.82 25892[5:MRR:25883.0,16.0] || cycle(e_2,e_0)*+ -> . % 11.58/11.82 25908[5:Res:22.5,25892.0] group_element(e_2) || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 25909[5:SSi:25908.0,29.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 26540[6:Spt:25909.1] || -> cycle(e_2,e_3)*. % 11.58/11.82 26541[6:MRR:540.0,26540.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 26542[6:MRR:555.1,26540.0] || cycle(e_4,e_1)+ cycle(e_3,e_0)* -> . % 11.58/11.82 26556[6:Res:22.5,26541.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 26557[6:SSi:26556.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 26560[7:Spt:26557.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 26568[7:Res:26560.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 26569[7:MRR:26568.0,26568.1,9.0,45.0] || -> . % 11.58/11.82 26570[7:Spt:26569.0,26557.0,26560.0] || cycle(e_4,e_4)*+ -> . % 11.58/11.82 26571[7:Spt:26569.0,26557.1,26557.2,26557.3] || -> cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 26573[8:Spt:26571.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 26580[8:Res:26573.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 26581[8:MRR:26580.0,26580.1,8.0,41.0] || -> . % 11.58/11.82 26582[8:Spt:26581.0,26571.0,26573.0] || cycle(e_4,e_3)*+ -> . % 11.58/11.82 26583[8:Spt:26581.0,26571.1,26571.2] || -> cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 26584[9:Spt:26583.0] || -> cycle(e_4,e_2)*. % 11.58/11.82 26589[9:Res:26584.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 26590[9:MRR:26589.0,26589.1,7.0,37.0] || -> . % 11.58/11.82 26591[9:Spt:26590.0,26583.0,26584.0] || cycle(e_4,e_2)*+ -> . % 11.58/11.82 26592[9:Spt:26590.0,26583.1] || -> cycle(e_4,e_1)*. % 11.58/11.82 26593[9:MRR:139.0,26592.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 26594[9:MRR:26542.0,26592.0] || cycle(e_3,e_0)*+ -> . % 11.58/11.82 26601[9:Res:22.5,26594.0] group_element(e_3) || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 11.58/11.82 26602[9:SSi:26601.0,30.0] || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 11.58/11.82 26603[9:MRR:26602.0,26602.1,26602.2,637.0,706.0,22800.0] || -> cycle(e_3,e_1)*. % 11.58/11.82 26607[9:Res:26603.0,26593.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 26608[9:MRR:26607.0,26607.1,6.0,33.0] || -> . % 11.58/11.82 26609[6:Spt:26608.0,25909.1,26540.0] || cycle(e_2,e_3)*+ -> . % 11.58/11.82 26610[6:Spt:26608.0,25909.0,25909.2,25909.3] || -> cycle(e_2,e_4) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 26613[7:Spt:26610.2] || -> cycle(e_2,e_1)*. % 11.58/11.82 28778[5:Res:3.0,25889.0] || cycle(e_2,u) greater(u,e_0)* -> equalish(e_4,e_3)*. % 11.58/11.82 28779[5:MRR:28778.2,47.0] || cycle(e_2,u)+ greater(u,e_0)* -> . % 11.58/11.82 28781[7:Res:26613.0,28779.0] || greater(e_1,e_0)* -> . % 11.58/11.82 28782[7:MRR:28781.0,6.0] || -> . % 11.58/11.82 28783[7:Spt:28782.0,26610.2,26613.0] || cycle(e_2,e_1)* -> . % 11.58/11.82 28784[7:Spt:28782.0,26610.0,26610.1] || -> cycle(e_2,e_4) cycle(e_2,e_2)*. % 11.58/11.82 28785[8:Spt:28784.0] || -> cycle(e_2,e_4)*. % 11.58/11.82 28803[8:Res:28785.0,28779.0] || greater(e_4,e_0)* -> . % 11.58/11.82 28804[8:MRR:28803.0,9.0] || -> . % 11.58/11.82 28805[8:Spt:28804.0,28784.0,28785.0] || cycle(e_2,e_4)* -> . % 11.58/11.82 28806[8:Spt:28804.0,28784.1] || -> cycle(e_2,e_2)*. % 11.58/11.82 28818[8:Res:28806.0,28779.0] || greater(e_2,e_0)* -> . % 11.58/11.82 28819[8:MRR:28818.0,7.0] || -> . % 11.58/11.82 28820[5:Spt:28819.0,25871.0,25880.0] || product(e_2,e_1,e_4)*+ -> . % 11.58/11.82 28821[5:Spt:28819.0,25871.1] || -> product(e_2,e_1,e_3)*. % 11.58/11.82 28826[5:MRR:25875.1,28820.0] || product(e_1,e_2,u)*+ -> product(u,e_3,e_1)*. % 11.58/11.82 28827[5:MRR:25878.4,28820.0] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 11.58/11.82 28985[6:Spt:826.0] || -> product(e_1,e_2,e_5)*. % 11.58/11.82 28988[6:Res:28985.0,58.0] || product(e_2,e_1,u)*+ -> product(u,e_5,e_2)*. % 11.58/11.82 29260[6:Res:28821.0,28988.0] || -> product(e_3,e_5,e_2)*. % 11.58/11.82 29270[6:Res:29260.0,55.0] || product(e_3,u,e_2)*+ -> equalish(u,e_5). % 11.58/11.82 29315[6:Res:461.4,29270.0] group_element(e_3) || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_1,e_3) equalish(e_1,e_5). % 11.58/11.82 29329[6:SSi:29315.0,30.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_1,e_3) equalish(e_1,e_5). % 11.58/11.82 29330[6:MRR:29329.2,29329.3,29329.4,73.0,34.0,36.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4)*. % 11.58/11.82 29341[6:Res:29330.1,26.2] || greater(e_4,e_3) cycle(e_3,e_0) -> product(e_3,e_1,e_5)*. % 11.58/11.82 29350[6:MRR:29341.0,18.0] || cycle(e_3,e_0)+ -> product(e_3,e_1,e_5)*. % 11.58/11.82 29353[6:Res:22.5,29350.0] group_element(e_3) || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1) product(e_3,e_1,e_5)*. % 11.58/11.82 29354[6:SSi:29353.0,30.0] || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1) product(e_3,e_1,e_5)*. % 11.58/11.82 29355[6:MRR:29354.0,29354.1,29354.2,637.0,706.0,22800.0] || -> cycle(e_3,e_1) product(e_3,e_1,e_5)*. % 11.58/11.82 29356[7:Spt:29355.1] || -> product(e_3,e_1,e_5)*. % 11.58/11.82 29359[7:Res:29356.0,26.2] || greater(e_5,e_3)* cycle(e_3,e_0) -> . % 11.58/11.82 29368[7:MRR:29359.0,19.0] || cycle(e_3,e_0)*+ -> . % 11.58/11.82 29379[7:Res:22.5,29368.0] group_element(e_3) || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 11.58/11.82 29380[7:SSi:29379.0,30.0] || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 11.58/11.82 29381[7:MRR:29380.0,29380.1,29380.2,637.0,706.0,22800.0] || -> cycle(e_3,e_1)*. % 11.58/11.82 29382[7:MRR:474.0,29381.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 29384[7:MRR:140.0,29381.0] || cycle(e_2,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 29387[7:Res:22.5,29382.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 29388[7:SSi:29387.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 29638[8:Spt:28827.3] || -> cycle(e_2,e_1)*. % 11.58/11.82 29645[8:Res:29638.0,29384.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 29646[8:MRR:29645.0,29645.1,6.0,33.0] || -> . % 11.58/11.82 29647[8:Spt:29646.0,28827.3,29638.0] || cycle(e_2,e_1)*+ -> . % 11.58/11.82 29648[8:Spt:29646.0,28827.0,28827.1,28827.2] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2)*. % 11.58/11.82 29649[9:Spt:29648.0] || -> cycle(e_2,e_4)*. % 11.58/11.82 29655[9:Res:29649.0,29384.0] || greater(e_4,e_0) -> equalish(e_4,e_2)*. % 11.58/11.82 29656[9:MRR:29655.0,29655.1,9.0,46.0] || -> . % 11.58/11.82 29657[9:Spt:29656.0,29648.0,29649.0] || cycle(e_2,e_4)*+ -> . % 11.58/11.82 29658[9:Spt:29656.0,29648.1,29648.2] || -> cycle(e_2,e_3) cycle(e_2,e_2)*. % 11.58/11.82 29662[10:Spt:29658.0] || -> cycle(e_2,e_3)*. % 11.58/11.82 29667[10:Res:29662.0,29384.0] || greater(e_3,e_0) -> equalish(e_3,e_2)*. % 11.58/11.82 29668[10:MRR:29667.0,29667.1,8.0,42.0] || -> . % 11.58/11.82 29669[10:Spt:29668.0,29658.0,29662.0] || cycle(e_2,e_3)*+ -> . % 11.58/11.82 29670[10:Spt:29668.0,29658.1] || -> cycle(e_2,e_2)*. % 11.58/11.82 29678[11:Spt:29388.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 29684[11:Res:29678.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 29685[11:MRR:29684.0,29684.1,9.0,45.0] || -> . % 11.58/11.82 29686[11:Spt:29685.0,29388.0,29678.0] || cycle(e_4,e_4)*+ -> . % 11.58/11.82 29687[11:Spt:29685.0,29388.1,29388.2,29388.3] || -> cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 29688[12:Spt:29687.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 29693[12:Res:29688.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 29694[12:MRR:29693.0,29693.1,8.0,41.0] || -> . % 11.58/11.82 29695[12:Spt:29694.0,29687.0,29688.0] || cycle(e_4,e_3)*+ -> . % 11.58/11.82 29696[12:Spt:29694.0,29687.1,29687.2] || -> cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 29697[13:Spt:29696.0] || -> cycle(e_4,e_2)*. % 11.58/11.82 29701[13:Res:29697.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 29702[13:MRR:29701.0,29701.1,7.0,37.0] || -> . % 11.58/11.82 29703[13:Spt:29702.0,29696.0,29697.0] || cycle(e_4,e_2)*+ -> . % 11.58/11.82 29704[13:Spt:29702.0,29696.1] || -> cycle(e_4,e_1)*. % 11.58/11.82 29705[13:MRR:139.0,29704.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 29710[13:Res:29381.0,29705.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 29711[13:MRR:29710.0,29710.1,6.0,33.0] || -> . % 11.58/11.82 29712[7:Spt:29711.0,29355.1,29356.0] || product(e_3,e_1,e_5)*+ -> . % 11.58/11.82 29713[7:Spt:29711.0,29355.0] || -> cycle(e_3,e_1)*. % 11.58/11.82 29716[7:MRR:474.0,29713.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 29722[7:MRR:140.0,29713.0] || cycle(e_2,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 29748[7:Res:22.5,29716.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 29749[7:SSi:29748.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 29872[8:Spt:28827.3] || -> cycle(e_2,e_1)*. % 11.58/11.82 29879[8:Res:29872.0,29722.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 29880[8:MRR:29879.0,29879.1,6.0,33.0] || -> . % 11.58/11.82 29881[8:Spt:29880.0,28827.3,29872.0] || cycle(e_2,e_1)*+ -> . % 11.58/11.82 29882[8:Spt:29880.0,28827.0,28827.1,28827.2] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2)*. % 11.58/11.82 29883[9:Spt:29882.0] || -> cycle(e_2,e_4)*. % 11.58/11.82 29889[9:Res:29883.0,29722.0] || greater(e_4,e_0) -> equalish(e_4,e_2)*. % 11.58/11.82 29890[9:MRR:29889.0,29889.1,9.0,46.0] || -> . % 11.58/11.82 29891[9:Spt:29890.0,29882.0,29883.0] || cycle(e_2,e_4)*+ -> . % 11.58/11.82 29892[9:Spt:29890.0,29882.1,29882.2] || -> cycle(e_2,e_3) cycle(e_2,e_2)*. % 11.58/11.82 29896[10:Spt:29892.0] || -> cycle(e_2,e_3)*. % 11.58/11.82 29901[10:Res:29896.0,29722.0] || greater(e_3,e_0) -> equalish(e_3,e_2)*. % 11.58/11.82 29902[10:MRR:29901.0,29901.1,8.0,42.0] || -> . % 11.58/11.82 29903[10:Spt:29902.0,29892.0,29896.0] || cycle(e_2,e_3)*+ -> . % 11.58/11.82 29904[10:Spt:29902.0,29892.1] || -> cycle(e_2,e_2)*. % 11.58/11.82 29912[11:Spt:29749.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 29918[11:Res:29912.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 29919[11:MRR:29918.0,29918.1,9.0,45.0] || -> . % 11.58/11.82 29920[11:Spt:29919.0,29749.0,29912.0] || cycle(e_4,e_4)*+ -> . % 11.58/11.82 29921[11:Spt:29919.0,29749.1,29749.2,29749.3] || -> cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 29922[12:Spt:29921.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 29927[12:Res:29922.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 29928[12:MRR:29927.0,29927.1,8.0,41.0] || -> . % 11.58/11.82 29929[12:Spt:29928.0,29921.0,29922.0] || cycle(e_4,e_3)*+ -> . % 11.58/11.82 29930[12:Spt:29928.0,29921.1,29921.2] || -> cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 29931[13:Spt:29930.0] || -> cycle(e_4,e_2)*. % 11.58/11.82 29935[13:Res:29931.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 29936[13:MRR:29935.0,29935.1,7.0,37.0] || -> . % 11.58/11.82 29937[13:Spt:29936.0,29930.0,29931.0] || cycle(e_4,e_2)*+ -> . % 11.58/11.82 29938[13:Spt:29936.0,29930.1] || -> cycle(e_4,e_1)*. % 11.58/11.82 29939[13:MRR:139.0,29938.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 29944[13:Res:29713.0,29939.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 29945[13:MRR:29944.0,29944.1,6.0,33.0] || -> . % 11.58/11.82 29946[6:Spt:29945.0,826.0,28985.0] || product(e_1,e_2,e_5)*+ -> . % 11.58/11.82 29947[6:Spt:29945.0,826.1,826.2] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)*. % 11.58/11.82 29954[7:Spt:29947.0] || -> product(e_1,e_2,e_4)*. % 11.58/11.82 29957[7:Res:29954.0,58.0] || product(e_2,e_1,u)*+ -> product(u,e_4,e_2)*. % 11.58/11.82 30200[7:Res:28821.0,29957.0] || -> product(e_3,e_4,e_2)*. % 11.58/11.82 30209[7:Res:30200.0,55.0] || product(e_3,u,e_2)*+ -> equalish(u,e_4). % 11.58/11.82 30260[7:Res:461.4,30209.0] group_element(e_3) || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_1,e_3) equalish(e_1,e_4). % 11.58/11.82 30274[7:SSi:30260.0,30.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_1,e_3) equalish(e_1,e_4). % 11.58/11.82 30275[7:MRR:30274.2,30274.3,30274.4,73.0,34.0,35.0] || -> product(e_3,e_1,e_5) product(e_3,e_1,e_4)*. % 11.58/11.82 30286[7:Res:30275.1,26.2] || greater(e_4,e_3) cycle(e_3,e_0) -> product(e_3,e_1,e_5)*. % 11.58/11.82 30295[7:MRR:30286.0,18.0] || cycle(e_3,e_0)+ -> product(e_3,e_1,e_5)*. % 11.58/11.82 30298[7:Res:22.5,30295.0] group_element(e_3) || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1) product(e_3,e_1,e_5)*. % 11.58/11.82 30299[7:SSi:30298.0,30.0] || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1) product(e_3,e_1,e_5)*. % 11.58/11.82 30300[7:MRR:30299.0,30299.1,30299.2,637.0,706.0,22800.0] || -> cycle(e_3,e_1) product(e_3,e_1,e_5)*. % 11.58/11.82 30301[8:Spt:30300.1] || -> product(e_3,e_1,e_5)*. % 11.58/11.82 30304[8:Res:30301.0,26.2] || greater(e_5,e_3)* cycle(e_3,e_0) -> . % 11.58/11.82 30313[8:MRR:30304.0,19.0] || cycle(e_3,e_0)*+ -> . % 11.58/11.82 30324[8:Res:22.5,30313.0] group_element(e_3) || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 11.58/11.82 30325[8:SSi:30324.0,30.0] || -> cycle(e_3,e_4) cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 11.58/11.82 30326[8:MRR:30325.0,30325.1,30325.2,637.0,706.0,22800.0] || -> cycle(e_3,e_1)*. % 11.58/11.82 30327[8:MRR:474.0,30326.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 30329[8:MRR:140.0,30326.0] || cycle(e_2,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 30332[8:Res:22.5,30327.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 30333[8:SSi:30332.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 30601[9:Spt:28827.3] || -> cycle(e_2,e_1)*. % 11.58/11.82 30608[9:Res:30601.0,30329.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 30609[9:MRR:30608.0,30608.1,6.0,33.0] || -> . % 11.58/11.82 30610[9:Spt:30609.0,28827.3,30601.0] || cycle(e_2,e_1)*+ -> . % 11.58/11.82 30611[9:Spt:30609.0,28827.0,28827.1,28827.2] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2)*. % 11.58/11.82 30612[10:Spt:30611.0] || -> cycle(e_2,e_4)*. % 11.58/11.82 30618[10:Res:30612.0,30329.0] || greater(e_4,e_0) -> equalish(e_4,e_2)*. % 11.58/11.82 30619[10:MRR:30618.0,30618.1,9.0,46.0] || -> . % 11.58/11.82 30620[10:Spt:30619.0,30611.0,30612.0] || cycle(e_2,e_4)*+ -> . % 11.58/11.82 30621[10:Spt:30619.0,30611.1,30611.2] || -> cycle(e_2,e_3) cycle(e_2,e_2)*. % 11.58/11.82 30625[11:Spt:30621.0] || -> cycle(e_2,e_3)*. % 11.58/11.82 30630[11:Res:30625.0,30329.0] || greater(e_3,e_0) -> equalish(e_3,e_2)*. % 11.58/11.82 30631[11:MRR:30630.0,30630.1,8.0,42.0] || -> . % 11.58/11.82 30632[11:Spt:30631.0,30621.0,30625.0] || cycle(e_2,e_3)*+ -> . % 11.58/11.82 30633[11:Spt:30631.0,30621.1] || -> cycle(e_2,e_2)*. % 11.58/11.82 30641[12:Spt:30333.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 30647[12:Res:30641.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 30648[12:MRR:30647.0,30647.1,9.0,45.0] || -> . % 11.58/11.82 30649[12:Spt:30648.0,30333.0,30641.0] || cycle(e_4,e_4)*+ -> . % 11.58/11.82 30650[12:Spt:30648.0,30333.1,30333.2,30333.3] || -> cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 30651[13:Spt:30650.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 30656[13:Res:30651.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 30657[13:MRR:30656.0,30656.1,8.0,41.0] || -> . % 11.58/11.82 30658[13:Spt:30657.0,30650.0,30651.0] || cycle(e_4,e_3)*+ -> . % 11.58/11.82 30659[13:Spt:30657.0,30650.1,30650.2] || -> cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 30660[14:Spt:30659.0] || -> cycle(e_4,e_2)*. % 11.58/11.82 30664[14:Res:30660.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 30665[14:MRR:30664.0,30664.1,7.0,37.0] || -> . % 11.58/11.82 30666[14:Spt:30665.0,30659.0,30660.0] || cycle(e_4,e_2)*+ -> . % 11.58/11.82 30667[14:Spt:30665.0,30659.1] || -> cycle(e_4,e_1)*. % 11.58/11.82 30668[14:MRR:139.0,30667.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 30673[14:Res:30326.0,30668.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 30674[14:MRR:30673.0,30673.1,6.0,33.0] || -> . % 11.58/11.82 30675[8:Spt:30674.0,30300.1,30301.0] || product(e_3,e_1,e_5)*+ -> . % 11.58/11.82 30676[8:Spt:30674.0,30300.0] || -> cycle(e_3,e_1)*. % 11.58/11.82 30679[8:MRR:474.0,30676.0] || cycle(e_4,e_0)*+ -> . % 11.58/11.82 30685[8:MRR:140.0,30676.0] || cycle(e_2,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 11.58/11.82 30711[8:Res:22.5,30679.0] group_element(e_4) || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 30712[8:SSi:30711.0,31.0] || -> cycle(e_4,e_4) cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 30833[9:Spt:28827.3] || -> cycle(e_2,e_1)*. % 11.58/11.82 30840[9:Res:30833.0,30685.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 11.58/11.82 30841[9:MRR:30840.0,30840.1,6.0,33.0] || -> . % 11.58/11.82 30842[9:Spt:30841.0,28827.3,30833.0] || cycle(e_2,e_1)*+ -> . % 11.58/11.82 30843[9:Spt:30841.0,28827.0,28827.1,28827.2] || -> cycle(e_2,e_4) cycle(e_2,e_3) cycle(e_2,e_2)*. % 11.58/11.82 30844[10:Spt:30843.0] || -> cycle(e_2,e_4)*. % 11.58/11.82 30850[10:Res:30844.0,30685.0] || greater(e_4,e_0) -> equalish(e_4,e_2)*. % 11.58/11.82 30851[10:MRR:30850.0,30850.1,9.0,46.0] || -> . % 11.58/11.82 30852[10:Spt:30851.0,30843.0,30844.0] || cycle(e_2,e_4)*+ -> . % 11.58/11.82 30853[10:Spt:30851.0,30843.1,30843.2] || -> cycle(e_2,e_3) cycle(e_2,e_2)*. % 11.58/11.82 30857[11:Spt:30853.0] || -> cycle(e_2,e_3)*. % 11.58/11.82 30862[11:Res:30857.0,30685.0] || greater(e_3,e_0) -> equalish(e_3,e_2)*. % 11.58/11.82 30863[11:MRR:30862.0,30862.1,8.0,42.0] || -> . % 11.58/11.82 30864[11:Spt:30863.0,30853.0,30857.0] || cycle(e_2,e_3)*+ -> . % 11.58/11.82 30865[11:Spt:30863.0,30853.1] || -> cycle(e_2,e_2)*. % 11.58/11.82 30873[12:Spt:30712.0] || -> cycle(e_4,e_4)*. % 11.58/11.82 30879[12:Res:30873.0,148.0] || greater(e_4,e_0) -> equalish(e_4,e_1)*. % 11.58/11.82 30880[12:MRR:30879.0,30879.1,9.0,45.0] || -> . % 11.58/11.82 30881[12:Spt:30880.0,30712.0,30873.0] || cycle(e_4,e_4)*+ -> . % 11.58/11.82 30882[12:Spt:30880.0,30712.1,30712.2,30712.3] || -> cycle(e_4,e_3) cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 30883[13:Spt:30882.0] || -> cycle(e_4,e_3)*. % 11.58/11.82 30888[13:Res:30883.0,148.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 11.58/11.82 30889[13:MRR:30888.0,30888.1,8.0,41.0] || -> . % 11.58/11.82 30890[13:Spt:30889.0,30882.0,30883.0] || cycle(e_4,e_3)*+ -> . % 11.58/11.82 30891[13:Spt:30889.0,30882.1,30882.2] || -> cycle(e_4,e_2) cycle(e_4,e_1)*. % 11.58/11.82 30892[14:Spt:30891.0] || -> cycle(e_4,e_2)*. % 11.58/11.82 30896[14:Res:30892.0,148.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 11.58/11.82 30897[14:MRR:30896.0,30896.1,7.0,37.0] || -> . % 11.58/11.82 30898[14:Spt:30897.0,30891.0,30892.0] || cycle(e_4,e_2)*+ -> . % 11.58/11.82 30899[14:Spt:30897.0,30891.1] || -> cycle(e_4,e_1)*. % 11.58/11.82 30900[14:MRR:139.0,30899.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 17.18/17.41 30905[14:Res:30676.0,30900.0] || greater(e_1,e_0) -> equalish(e_1,e_2)*. % 17.18/17.41 30906[14:MRR:30905.0,30905.1,6.0,33.0] || -> . % 17.18/17.41 30907[7:Spt:30906.0,29947.0,29954.0] || product(e_1,e_2,e_4)* -> . % 17.18/17.41 30908[7:Spt:30906.0,29947.1] || -> product(e_1,e_2,e_3)*. % 17.18/17.41 30934[7:Res:30908.0,28826.0] || -> product(e_3,e_3,e_1)*. % 17.18/17.41 30945[7:Res:30934.0,75.0] || -> equalish(e_1,e_3)*. % 17.18/17.41 30956[7:MRR:30945.0,34.0] || -> . % 17.18/17.41 % SZS output end Refutation % 17.18/17.41 Formulae used in the proof : e_0_then_e_1 e_1_then_e_2 e_2_then_e_3 e_3_then_e_4 e_4_then_e_5 e_1_greater_e_0 e_2_greater_e_0 e_3_greater_e_0 e_4_greater_e_0 e_2_greater_e_1 e_3_greater_e_1 e_3_greater_e_2 e_4_greater_e_2 e_5_greater_e_2 e_4_greater_e_3 e_5_greater_e_3 cycle2 cycle3 cycle4 cycle5 cycle6 cycle7 element_1 element_2 element_3 element_4 element_5 e_1_is_not_e_2 e_1_is_not_e_3 e_1_is_not_e_4 e_1_is_not_e_5 e_2_is_not_e_1 e_2_is_not_e_3 e_2_is_not_e_4 e_2_is_not_e_5 e_3_is_not_e_1 e_3_is_not_e_2 e_3_is_not_e_4 e_4_is_not_e_1 e_4_is_not_e_2 e_4_is_not_e_3 e_5_is_not_e_2 e_5_is_not_e_3 e_5_is_not_e_4 product_total_function1 product_total_function2 product_right_cancellation product_left_cancellation product_idempotence qg3 % 17.18/17.41 %------------------------------------------------------------------------------