%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO630-1 : TPTP v8.1.0. Released v7.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n004.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 21 19:55:10 EDT 2022 % Result : Unsatisfiable 0.68s 0.86s % Output : Refutation 0.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO630-1 : TPTP v8.1.0. Released v7.1.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n004.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jul 8 22:58:07 EDT 2022 % 0.13/0.34 % CPUTime : % 0.68/0.86 % 0.68/0.86 SPASS V 3.9 % 0.68/0.86 SPASS beiseite: Proof found. % 0.68/0.86 % SZS status Theorem % 0.68/0.86 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.68/0.86 SPASS derived 1128 clauses, backtracked 0 clauses, performed 0 splits and kept 647 clauses. % 0.68/0.86 SPASS allocated 64395 KBytes. % 0.68/0.86 SPASS spent 0:00:00.51 on the problem. % 0.68/0.86 0:00:00.04 for the input. % 0.68/0.86 0:00:00.00 for the FLOTTER CNF translation. % 0.68/0.86 0:00:00.08 for inferences. % 0.68/0.86 0:00:00.00 for the backtracking. % 0.68/0.86 0:00:00.36 for the reduction. % 0.68/0.86 % 0.68/0.86 % 0.68/0.86 Here is a proof with depth 179, length 342 : % 0.68/0.86 % SZS output start Refutation % 0.68/0.86 1[0:Inp] || -> LE(f(u),s(s(s(s(s(0)))))) E(s(s(s(s(s(0))))),f(u))*. % 0.68/0.86 6[0:Inp] || LE(f(u),s(0))* iLEQ(u,v)* -> E(0,f(v))* LE(f(v),0). % 0.68/0.86 7[0:Inp] || LE(f(u),0)* -> . % 0.68/0.86 10[0:Inp] || E(s(s(s(s(s(0))))),f(u)) E(s(s(s(s(s(0))))),f(g(u)))* -> E(f(u),f(g(u)))*. % 0.68/0.86 11[0:Inp] || E(s(s(s(0))),f(u)) E(s(s(s(0))),f(g(u)))* -> E(f(u),f(g(u)))*. % 0.68/0.86 12[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(g(u)))* -> E(f(u),f(g(u)))*. % 0.68/0.86 13[0:Inp] || E(s(0),f(u)) E(s(0),f(g(u)))* -> E(f(u),f(g(u)))*. % 0.68/0.86 15[0:Inp] || iLEQ(u,v)* LE(f(u),s(s(s(0))))*+ -> LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 16[0:Inp] || iLEQ(u,v)* LE(f(u),s(s(s(s(s(0))))))*+ -> LE(f(v),s(s(s(s(0))))) E(s(s(s(s(0)))),f(v))*. % 0.68/0.86 17[0:Inp] || iLEQ(u,v)* LE(f(u),s(s(s(s(0)))))*+ -> LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 24[0:Inp] || E(0,f(u)) E(0,f(g(u))) -> E(f(u),f(g(u)))*. % 0.68/0.86 25[0:Inp] || -> iLEQ(u,g(u))*. % 0.68/0.86 29[0:Inp] || -> iLEQ(u,u)*. % 0.68/0.86 30[0:Inp] || E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(g(u)))* -> E(f(u),f(g(u)))*. % 0.68/0.86 31[0:Inp] || E(f(u),f(g(u)))* -> . % 0.68/0.86 32[0:Inp] || iLEQ(u,v)* LE(f(u),s(s(0)))*+ -> LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 33[0:MRR:24.2,31.0] || E(0,f(u)) E(0,f(g(u)))* -> . % 0.68/0.86 34[0:MRR:6.3,7.0] || iLEQ(u,v)* LE(f(u),s(0))*+ -> E(0,f(v))*. % 0.68/0.86 35[0:MRR:13.2,31.0] || E(s(0),f(u)) E(s(0),f(g(u)))* -> . % 0.68/0.86 36[0:MRR:12.2,31.0] || E(s(s(0)),f(u)) E(s(s(0)),f(g(u)))* -> . % 0.68/0.86 37[0:MRR:11.2,31.0] || E(s(s(s(0))),f(u)) E(s(s(s(0))),f(g(u)))* -> . % 0.68/0.86 38[0:MRR:30.2,31.0] || E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(g(u)))* -> . % 0.68/0.86 39[0:MRR:10.2,31.0] || E(s(s(s(s(s(0))))),f(u)) E(s(s(s(s(s(0))))),f(g(u)))* -> . % 0.68/0.86 40[0:Res:1.1,39.1] || E(s(s(s(s(s(0))))),f(u)) -> LE(f(g(u)),s(s(s(s(s(0))))))*. % 0.68/0.86 41[0:Res:40.1,16.1] || E(s(s(s(s(s(0))))),f(u))*+ iLEQ(g(u),v)* -> LE(f(v),s(s(s(s(0))))) E(s(s(s(s(0)))),f(v))*. % 0.68/0.86 42[0:Res:1.1,41.0] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(s(0))))))* LE(f(v),s(s(s(s(0))))) E(s(s(s(s(0)))),f(v))*. % 0.68/0.86 43[0:Res:29.0,42.0] || -> LE(f(u),s(s(s(s(s(0)))))) LE(f(g(u)),s(s(s(s(0))))) E(s(s(s(s(0)))),f(g(u)))*. % 0.68/0.86 44[0:Res:25.0,42.0] || -> LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(s(s(0))))) E(s(s(s(s(0)))),f(g(g(u))))*. % 0.68/0.86 47[0:Res:44.2,38.1] || E(s(s(s(s(0)))),f(g(u))) -> LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(s(s(0)))))*. % 0.68/0.86 48[0:Res:47.2,17.1] || E(s(s(s(s(0)))),f(g(u)))*+ iLEQ(g(g(u)),v)* -> LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 51[0:Res:43.2,48.0] || iLEQ(g(g(u)),v)* -> LE(f(u),s(s(s(s(s(0)))))) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 53[0:Obv:51.1] || iLEQ(g(g(u)),v)*+ -> LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 54[0:Res:29.0,53.0] || -> LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(s(0)))) E(s(s(s(0))),f(g(g(u))))*. % 0.68/0.86 55[0:Res:25.0,53.0] || -> LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(s(0)))) E(s(s(s(0))),f(g(g(g(u)))))*. % 0.68/0.86 58[0:Res:55.3,37.1] || E(s(s(s(0))),f(g(g(u)))) -> LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(s(0))))*. % 0.68/0.86 61[0:Res:58.3,15.1] || E(s(s(s(0))),f(g(g(u))))*+ iLEQ(g(g(g(u))),v)* -> LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 64[0:Res:54.3,61.0] || iLEQ(g(g(g(u))),v)* -> LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 66[0:Obv:64.2] || iLEQ(g(g(g(u))),v)*+ -> LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 67[0:Res:29.0,66.0] || -> LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(0))) E(s(s(0)),f(g(g(g(u)))))*. % 0.68/0.86 68[0:Res:25.0,66.0] || -> LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(s(0))) E(s(s(0)),f(g(g(g(g(u))))))*. % 0.68/0.86 72[0:Res:68.4,36.1] || E(s(s(0)),f(g(g(g(u))))) -> LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(s(0)))*. % 0.68/0.86 73[0:Res:72.4,32.1] || E(s(s(0)),f(g(g(g(u)))))*+ iLEQ(g(g(g(g(u)))),v)* -> LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 81[0:Res:67.4,73.0] || iLEQ(g(g(g(g(u)))),v)* -> LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(0)))* LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 83[0:Obv:81.3] || iLEQ(g(g(g(g(u)))),v)*+ -> LE(f(g(g(g(u)))),s(s(0)))* LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 84[0:Res:29.0,83.0] || -> LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0)) E(s(0),f(g(g(g(g(u))))))*. % 0.68/0.86 85[0:Res:25.0,83.0] || -> LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(g(u)))))),s(0)) E(s(0),f(g(g(g(g(g(u)))))))*. % 0.68/0.86 91[0:Res:85.5,35.1] || E(s(0),f(g(g(g(g(u)))))) -> LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(g(u)))))),s(0))*. % 0.68/0.86 92[0:Res:91.5,34.1] || E(s(0),f(g(g(g(g(u))))))*+ iLEQ(g(g(g(g(g(u))))),v)* -> LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(v)). % 0.68/0.86 100[0:Res:84.5,92.0] || iLEQ(g(g(g(g(g(u))))),v)* -> LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0))* LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(v)). % 0.68/0.86 102[0:Obv:100.4] || iLEQ(g(g(g(g(g(u))))),v)*+ -> LE(f(g(g(g(g(u))))),s(0))* LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(v)). % 0.68/0.86 103[0:Res:29.0,102.0] || -> LE(f(g(g(g(g(u))))),s(0)) LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(g(u)))))))*. % 0.68/0.86 104[0:Res:25.0,102.0] || -> LE(f(g(g(g(g(u))))),s(0)) LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(g(g(u))))))))*. % 0.68/0.86 112[0:Res:104.5,33.1] || E(0,f(g(g(g(g(g(u)))))))* -> LE(f(g(g(g(g(u))))),s(0)) LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))). % 0.68/0.86 113[0:MRR:112.0,103.5] || -> LE(f(g(g(g(g(u))))),s(0))* LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))). % 0.68/0.86 114[0:Res:113.0,34.1] || iLEQ(g(g(g(g(u)))),v)*+ -> LE(f(g(g(g(u)))),s(s(0)))* LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(v)). % 0.68/0.86 117[0:Res:29.0,114.0] || -> LE(f(g(g(g(u)))),s(s(0)))* LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(u)))))). % 0.68/0.86 118[0:Res:25.0,114.0] || -> LE(f(g(g(g(u)))),s(s(0))) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(g(u)))))))*. % 0.68/0.86 120[0:Res:118.4,33.1] || E(0,f(g(g(g(g(u)))))) -> LE(f(g(g(g(u)))),s(s(0)))* LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))). % 0.68/0.86 121[0:MRR:120.0,117.4] || -> LE(f(g(g(g(u)))),s(s(0)))* LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))). % 0.68/0.86 122[0:Res:121.0,32.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 125[0:Res:29.0,122.0] || -> LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))). % 0.68/0.86 126[0:Res:25.0,122.0] || -> LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0)) E(s(0),f(g(g(g(g(u))))))*. % 0.68/0.86 127[0:Res:125.0,15.1] || iLEQ(g(g(u)),v)*+ -> LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 128[0:Res:126.4,35.1] || E(s(0),f(g(g(g(u))))) -> LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0))*. % 0.68/0.86 129[0:Res:128.4,34.1] || E(s(0),f(g(g(g(u)))))+ iLEQ(g(g(g(g(u)))),v)* -> LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(v)). % 0.68/0.86 133[0:Res:29.0,127.0] || -> LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))). % 0.68/0.86 134[0:Res:25.0,127.0] || -> LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(s(0))) E(s(s(0)),f(g(g(g(u)))))*. % 0.68/0.86 135[0:Res:133.0,17.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 136[0:Res:134.5,36.1] || E(s(s(0)),f(g(g(u)))) -> LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 155[0:Res:136.5,32.1] || E(s(s(0)),f(g(g(u))))+ iLEQ(g(g(g(u))),v)* -> LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 160[0:Res:29.0,135.0] || -> LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))). % 0.68/0.86 161[0:Res:25.0,135.0] || -> LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(g(u))),s(s(s(0)))) E(s(s(s(0))),f(g(g(u))))*. % 0.68/0.86 162[0:Res:160.0,16.1] || iLEQ(u,v)*+ -> LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))* LE(f(v),s(s(s(s(0))))) E(s(s(s(s(0)))),f(v))*. % 0.68/0.86 165[0:Res:161.6,37.1] || E(s(s(s(0))),f(g(u))) -> LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 171[0:Res:165.6,15.1] || E(s(s(s(0))),f(g(u)))+ iLEQ(g(g(u)),v)* -> LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 183[0:Res:29.0,162.0] || -> LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))) LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(u))*. % 0.68/0.86 184[0:Res:25.0,162.0] || -> LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))) LE(f(g(u)),s(s(s(s(0))))) E(s(s(s(s(0)))),f(g(u)))*. % 0.68/0.86 190[0:Res:184.7,38.1] || E(s(s(s(s(0)))),f(u)) -> LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))) LE(f(g(u)),s(s(s(s(0)))))*. % 0.68/0.86 192[0:Res:190.7,17.1] || E(s(s(s(s(0)))),f(u))*+ iLEQ(g(u),v)* -> LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))) LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 332[0:Res:183.7,192.0] || iLEQ(g(u),v)* -> LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))* LE(f(u),s(s(s(s(0))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 336[0:Obv:332.6] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 337[0:Res:29.0,336.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))* LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 339[0:Obv:337.6] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 354[0:Res:339.6,171.0] || iLEQ(g(g(u)),v)* -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 361[0:Obv:354.5] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 396[0:Res:29.0,361.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))). % 0.68/0.86 398[0:Obv:396.6] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))). % 0.68/0.86 399[0:Res:398.2,16.1] || iLEQ(u,v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))* LE(f(v),s(s(s(s(0))))) E(s(s(s(s(0)))),f(v))*. % 0.68/0.86 400[0:Res:29.0,399.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(u))*. % 0.68/0.86 401[0:Res:25.0,399.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(s(0))))) E(s(s(s(s(0)))),f(g(u)))*. % 0.68/0.86 402[0:Obv:400.0] || -> LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(u))*. % 0.68/0.86 431[0:Res:401.7,38.1] || E(s(s(s(s(0)))),f(u)) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(s(0)))))*. % 0.68/0.86 432[0:MRR:431.0,402.6] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(u)),s(s(s(s(0)))))*. % 0.68/0.86 433[0:Res:432.6,17.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 440[0:Res:25.0,433.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(g(u))),s(s(s(0)))) E(s(s(s(0))),f(g(g(u))))*. % 0.68/0.86 449[0:Res:440.7,37.1] || E(s(s(s(0))),f(g(u))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 453[0:MRR:449.0,339.6] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 454[0:Res:453.6,15.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 455[0:Res:29.0,454.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))* LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))*. % 0.68/0.86 457[0:Obv:455.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))*. % 0.68/0.86 465[0:Res:457.5,155.0] || iLEQ(g(g(g(u))),v)* -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(0))) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 467[0:Obv:465.4] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 495[0:Res:29.0,467.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))). % 0.68/0.86 497[0:Obv:495.6] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))). % 0.68/0.86 501[0:Res:497.3,17.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 502[0:Res:29.0,501.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))). % 0.68/0.86 503[0:Res:25.0,501.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(s(0)))) E(s(s(s(0))),f(g(g(u))))*. % 0.68/0.86 504[0:Obv:502.1] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))). % 0.68/0.86 508[0:Res:503.7,37.1] || E(s(s(s(0))),f(g(u))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 512[0:MRR:508.0,504.6] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 517[0:Res:512.6,15.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 519[0:Res:25.0,517.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(s(0))) E(s(s(0)),f(g(g(g(u)))))*. % 0.68/0.86 522[0:Res:519.7,36.1] || E(s(s(0)),f(g(g(u)))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 529[0:MRR:522.0,457.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 534[0:Res:529.6,32.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 536[0:Res:29.0,534.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))). % 0.68/0.86 538[0:Obv:536.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))). % 0.68/0.86 539[0:Res:538.3,16.1] || iLEQ(u,v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))* LE(f(v),s(s(s(s(0))))) E(s(s(s(s(0)))),f(v))*. % 0.68/0.86 540[0:Res:29.0,539.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(u))*. % 0.68/0.86 541[0:Res:25.0,539.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(u)),s(s(s(s(0))))) E(s(s(s(s(0)))),f(g(u)))*. % 0.68/0.86 542[0:Obv:540.0] || -> LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(u))*. % 0.68/0.86 574[0:Res:541.6,38.1] || E(s(s(s(s(0)))),f(u)) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(u)),s(s(s(s(0)))))*. % 0.68/0.86 575[0:MRR:574.0,542.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(u)),s(s(s(s(0)))))*. % 0.68/0.86 577[0:Res:575.5,17.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 578[0:Res:29.0,577.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 579[0:Res:25.0,577.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(s(0)))) E(s(s(s(0))),f(g(g(u))))*. % 0.68/0.86 580[0:Obv:578.1] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 608[0:Res:579.6,37.1] || E(s(s(s(0))),f(g(u))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 612[0:MRR:608.0,580.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 613[0:Res:612.5,15.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 616[0:Res:25.0,613.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(s(0))) E(s(s(0)),f(g(g(g(u)))))*. % 0.68/0.86 619[0:Res:616.6,36.1] || E(s(s(0)),f(g(g(u)))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 626[0:MRR:619.0,457.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 629[0:Res:626.5,32.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))* LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 630[0:Res:29.0,629.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))* LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))*. % 0.68/0.86 632[0:Obv:630.4] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))*. % 0.68/0.86 638[0:Res:632.4,129.0] || iLEQ(g(g(g(g(u)))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(v)). % 0.68/0.86 647[0:Res:29.0,638.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(u)))))). % 0.68/0.86 648[0:Res:25.0,638.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(s(0)))) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(g(u)))))))*. % 0.68/0.86 651[0:Res:648.7,33.1] || E(0,f(g(g(g(g(u)))))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))). % 0.68/0.86 652[0:MRR:651.0,647.7] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(s(0))))* LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))). % 0.68/0.86 653[0:Res:652.4,15.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 654[0:Res:29.0,653.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))). % 0.68/0.86 655[0:Res:25.0,653.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(0))) E(s(s(0)),f(g(g(g(u)))))*. % 0.68/0.86 656[0:Obv:654.2] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))). % 0.68/0.86 661[0:Res:655.7,36.1] || E(s(s(0)),f(g(g(u)))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 667[0:MRR:661.0,656.6] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 672[0:Res:667.6,32.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 674[0:Res:25.0,672.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0)) E(s(0),f(g(g(g(g(u))))))*. % 0.68/0.86 679[0:Res:674.7,35.1] || E(s(0),f(g(g(g(u))))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0))*. % 0.68/0.86 683[0:MRR:679.0,632.4] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0))*. % 0.68/0.86 685[0:Res:683.6,34.1] || iLEQ(g(g(g(g(u)))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) E(0,f(v)). % 0.68/0.86 686[0:Res:29.0,685.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(u)))))). % 0.68/0.86 687[0:Res:25.0,685.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0))))) LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(g(u)))))))*. % 0.68/0.86 699[0:Res:687.6,33.1] || E(0,f(g(g(g(g(u)))))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))). % 0.68/0.86 700[0:MRR:699.0,686.6] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))* LE(f(u),s(s(s(s(s(0)))))). % 0.68/0.86 701[0:Res:700.4,17.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 702[0:Res:29.0,701.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))). % 0.68/0.86 703[0:Res:25.0,701.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(s(0)))) E(s(s(s(0))),f(g(g(u))))*. % 0.68/0.86 704[0:Obv:702.1] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u))). % 0.68/0.86 717[0:Res:703.6,37.1] || E(s(s(s(0))),f(g(u))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 721[0:MRR:717.0,704.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 724[0:Res:721.5,15.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 725[0:Res:29.0,724.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))). % 0.68/0.86 726[0:Res:25.0,724.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(0))) E(s(s(0)),f(g(g(g(u)))))*. % 0.68/0.86 727[0:Obv:725.2] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u)))). % 0.68/0.86 730[0:Res:726.6,36.1] || E(s(s(0)),f(g(g(u)))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 736[0:MRR:730.0,727.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 740[0:Res:736.5,32.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 742[0:Res:25.0,740.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0)) E(s(0),f(g(g(g(g(u))))))*. % 0.68/0.86 744[0:Res:742.6,35.1] || E(s(0),f(g(g(g(u))))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0))*. % 0.68/0.86 749[0:MRR:744.0,632.4] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) LE(f(g(g(g(g(u))))),s(0))*. % 0.68/0.86 754[0:Res:749.5,34.1] || iLEQ(g(g(g(g(u)))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* E(0,f(v)). % 0.68/0.86 755[0:Res:29.0,754.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))* E(0,f(g(g(g(g(u)))))). % 0.68/0.86 756[0:Res:25.0,754.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0)))))) E(0,f(g(g(g(g(g(u)))))))*. % 0.68/0.86 758[0:Res:756.5,33.1] || E(0,f(g(g(g(g(u)))))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))*. % 0.68/0.86 759[0:MRR:758.0,755.5] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(s(0))))))*. % 0.68/0.86 774[0:Res:759.4,16.1] || iLEQ(u,v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0))* LE(f(v),s(s(s(s(0))))) E(s(s(s(s(0)))),f(v))*. % 0.68/0.86 775[0:Res:29.0,774.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(u))*. % 0.68/0.86 776[0:Res:25.0,774.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0))))) E(s(s(s(s(0)))),f(g(u)))*. % 0.68/0.86 777[0:Obv:775.0] || -> LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(u))*. % 0.68/0.86 801[0:Res:776.5,38.1] || E(s(s(s(s(0)))),f(u)) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))*. % 0.68/0.86 802[0:MRR:801.0,777.4] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(s(0)))))*. % 0.68/0.86 803[0:Res:802.4,17.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 804[0:Res:29.0,803.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 805[0:Res:25.0,803.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(s(0)))) E(s(s(s(0))),f(g(g(u))))*. % 0.68/0.86 806[0:Obv:804.1] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 839[0:Res:805.5,37.1] || E(s(s(s(0))),f(g(u))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 843[0:MRR:839.0,806.4] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(s(0))))*. % 0.68/0.86 853[0:Res:843.4,15.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 854[0:Res:29.0,853.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))*. % 0.68/0.86 855[0:Res:25.0,853.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(g(u)))),s(s(0))) E(s(s(0)),f(g(g(g(u)))))*. % 0.68/0.86 856[0:Obv:854.2] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))*. % 0.68/0.86 882[0:Res:855.5,36.1] || E(s(s(0)),f(g(g(u)))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 890[0:MRR:882.0,856.4] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(g(u)))),s(s(0)))*. % 0.68/0.86 894[0:Res:890.4,32.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0))* LE(f(v),s(0)) E(s(0),f(v)). % 0.68/0.86 896[0:Res:25.0,894.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(g(g(u))))),s(0)) E(s(0),f(g(g(g(g(u))))))*. % 0.68/0.86 908[0:Res:896.5,35.1] || E(s(0),f(g(g(g(u))))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(g(g(u))))),s(0))*. % 0.68/0.86 914[0:MRR:908.0,632.4] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) LE(f(g(g(g(g(u))))),s(0))*. % 0.68/0.86 917[0:Res:914.4,34.1] || iLEQ(g(g(g(g(u)))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0))* E(0,f(v)). % 0.68/0.86 918[0:Res:29.0,917.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(0,f(g(g(g(g(u))))))*. % 0.68/0.86 919[0:Res:25.0,917.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)) E(0,f(g(g(g(g(g(u)))))))*. % 0.68/0.86 933[0:Res:919.4,33.1] || E(0,f(g(g(g(g(u))))))* -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0)). % 0.68/0.86 934[0:MRR:933.0,918.4] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) LE(f(g(g(g(u)))),s(0))*. % 0.68/0.86 935[0:Res:934.3,34.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0)))* E(0,f(v)). % 0.68/0.86 936[0:Res:29.0,935.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0)))* E(0,f(g(g(g(u))))). % 0.68/0.86 937[0:Res:25.0,935.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0))) E(0,f(g(g(g(g(u))))))*. % 0.68/0.86 940[0:Res:937.3,33.1] || E(0,f(g(g(g(u))))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 941[0:MRR:940.0,936.3] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 942[0:Res:941.2,32.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0))))* LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 943[0:Res:29.0,942.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))). % 0.68/0.86 944[0:Res:25.0,942.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))*. % 0.68/0.86 946[0:Res:943.1,15.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(s(0)))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 947[0:Res:944.3,35.1] || E(s(0),f(g(g(u)))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) LE(f(g(g(g(u)))),s(0))*. % 0.68/0.86 953[0:Res:947.3,34.1] || E(s(0),f(g(g(u))))+ iLEQ(g(g(g(u))),v)* -> LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0))))* E(0,f(v)). % 0.68/0.86 959[0:Res:29.0,946.0] || -> LE(f(u),s(s(s(s(0)))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u))). % 0.68/0.86 960[0:Res:25.0,946.0] || -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))*. % 0.68/0.86 961[0:Res:959.0,17.1] || iLEQ(u,v)*+ -> LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 962[0:Res:960.4,36.1] || E(s(s(0)),f(g(u))) -> LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 971[0:Res:962.4,32.1] || E(s(s(0)),f(g(u)))+ iLEQ(g(g(u)),v)* -> LE(f(u),s(s(s(s(0)))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 974[0:Res:29.0,961.0] || -> LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u))) LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u))*. % 0.68/0.86 975[0:Res:25.0,961.0] || -> LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 985[0:Res:975.5,37.1] || E(s(s(s(0))),f(u)) -> LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u))) LE(f(g(u)),s(s(s(0))))*. % 0.68/0.86 989[0:Res:985.5,15.1] || E(s(s(s(0))),f(u))*+ iLEQ(g(u),v)* -> LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u))) LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 1028[0:Res:974.5,989.0] || iLEQ(g(u),v)* -> LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))* LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 1034[0:Obv:1028.4] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 1035[0:Res:29.0,1034.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))* LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))*. % 0.68/0.86 1037[0:Obv:1035.4] || -> LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))*. % 0.68/0.86 1038[0:Res:1037.4,971.0] || iLEQ(g(g(u)),v)* -> LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(0))) LE(f(u),s(s(s(s(0)))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 1045[0:Obv:1038.3] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(u),s(s(s(s(0)))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 1067[0:Res:29.0,1045.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(u),s(s(s(s(0)))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))). % 0.68/0.86 1069[0:Obv:1067.4] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(u),s(s(s(s(0)))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))). % 0.68/0.86 1073[0:Res:1069.2,17.1] || iLEQ(u,v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u))))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 1074[0:Res:29.0,1073.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u))*. % 0.68/0.86 1075[0:Res:25.0,1073.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 1076[0:Obv:1074.0] || -> LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u))*. % 0.68/0.86 1105[0:Res:1075.5,37.1] || E(s(s(s(0))),f(u)) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(s(0))))*. % 0.68/0.86 1109[0:MRR:1105.0,1076.4] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(u)),s(s(s(0))))*. % 0.68/0.86 1110[0:Res:1109.4,15.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u))))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 1115[0:Res:25.0,1110.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))*. % 0.68/0.86 1119[0:Res:1115.5,36.1] || E(s(s(0)),f(g(u))) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 1125[0:MRR:1119.0,1037.4] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u)))) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 1126[0:Res:1125.4,32.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u))))* LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 1127[0:Res:29.0,1126.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u))))* LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u))))*. % 0.68/0.86 1129[0:Obv:1127.3] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u))))*. % 0.68/0.86 1139[0:Res:1129.3,953.0] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0))))* E(0,f(v)). % 0.68/0.86 1147[0:Res:29.0,1139.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0))))* E(0,f(g(g(g(u))))). % 0.68/0.86 1148[0:Res:25.0,1139.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0)))) E(0,f(g(g(g(g(u))))))*. % 0.68/0.86 1151[0:Res:1148.5,33.1] || E(0,f(g(g(g(u))))) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0))))*. % 0.68/0.86 1152[0:MRR:1151.0,1147.5] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(u)),s(s(s(0))))*. % 0.68/0.86 1153[0:Res:1152.4,15.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0)))))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 1154[0:Res:29.0,1153.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0)))))* LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u))). % 0.68/0.86 1155[0:Res:25.0,1153.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))*. % 0.68/0.86 1156[0:Obv:1154.1] || -> LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0)))))* LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u))). % 0.68/0.86 1167[0:Res:1155.5,36.1] || E(s(s(0)),f(g(u))) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 1173[0:MRR:1167.0,1156.4] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 1176[0:Res:1173.4,32.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0)))))* LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 1178[0:Res:25.0,1176.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))*. % 0.68/0.86 1188[0:Res:1178.5,35.1] || E(s(0),f(g(g(u)))) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(g(g(u)))),s(0))*. % 0.68/0.86 1192[0:MRR:1188.0,1129.3] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) LE(f(g(g(g(u)))),s(0))*. % 0.68/0.86 1195[0:Res:1192.4,34.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0)))))* E(0,f(v)). % 0.68/0.86 1196[0:Res:29.0,1195.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0)))))* E(0,f(g(g(g(u))))). % 0.68/0.86 1197[0:Res:25.0,1195.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0))))) E(0,f(g(g(g(g(u))))))*. % 0.68/0.86 1211[0:Res:1197.4,33.1] || E(0,f(g(g(g(u))))) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0)))))*. % 0.68/0.86 1212[0:MRR:1211.0,1196.4] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(s(0)))))*. % 0.68/0.86 1213[0:Res:1212.3,17.1] || iLEQ(u,v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0))* LE(f(v),s(s(s(0)))) E(s(s(s(0))),f(v))*. % 0.68/0.86 1214[0:Res:29.0,1213.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u))*. % 0.68/0.86 1215[0:Res:25.0,1213.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(u)),s(s(s(0)))) E(s(s(s(0))),f(g(u)))*. % 0.68/0.86 1216[0:Obv:1214.0] || -> LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u))*. % 0.68/0.86 1247[0:Res:1215.4,37.1] || E(s(s(s(0))),f(u)) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(u)),s(s(s(0))))*. % 0.68/0.86 1251[0:MRR:1247.0,1216.3] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(u)),s(s(s(0))))*. % 0.68/0.86 1252[0:Res:1251.3,15.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 1254[0:Res:29.0,1252.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))*. % 0.68/0.86 1255[0:Res:25.0,1252.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(g(u))),s(s(0))) E(s(s(0)),f(g(g(u))))*. % 0.68/0.86 1256[0:Obv:1254.1] || -> LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0)) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))*. % 0.68/0.86 1283[0:Res:1255.4,36.1] || E(s(s(0)),f(g(u))) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 1289[0:MRR:1283.0,1256.3] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(g(u))),s(s(0)))*. % 0.68/0.86 1290[0:Res:1289.3,32.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0))* LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 1292[0:Res:25.0,1290.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(g(g(u)))),s(0)) E(s(0),f(g(g(g(u)))))*. % 0.68/0.86 1295[0:Res:1292.4,35.1] || E(s(0),f(g(g(u)))) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(g(g(u)))),s(0))*. % 0.68/0.86 1299[0:MRR:1295.0,1129.3] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) LE(f(g(g(g(u)))),s(0))*. % 0.68/0.86 1303[0:Res:1299.3,34.1] || iLEQ(g(g(g(u))),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0))* E(0,f(v)). % 0.68/0.86 1304[0:Res:29.0,1303.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(0,f(g(g(g(u)))))*. % 0.68/0.86 1305[0:Res:25.0,1303.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)) E(0,f(g(g(g(g(u))))))*. % 0.68/0.86 1311[0:Res:1305.3,33.1] || E(0,f(g(g(g(u)))))* -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0)). % 0.68/0.86 1312[0:MRR:1311.0,1304.3] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) LE(f(g(g(u))),s(0))*. % 0.68/0.86 1313[0:Res:1312.2,34.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0)))* E(0,f(v)). % 0.68/0.86 1314[0:Res:29.0,1313.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0)))* E(0,f(g(g(u)))). % 0.68/0.86 1315[0:Res:25.0,1313.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0))) E(0,f(g(g(g(u)))))*. % 0.68/0.86 1319[0:Res:1315.2,33.1] || E(0,f(g(g(u)))) -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0)))*. % 0.68/0.86 1320[0:MRR:1319.0,1314.2] || -> LE(f(u),s(s(s(0)))) LE(f(g(u)),s(s(0)))*. % 0.68/0.86 1321[0:Res:1320.1,32.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(s(0))))* LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 1322[0:Res:29.0,1321.0] || -> LE(f(u),s(s(s(0))))* LE(f(g(u)),s(0)) E(s(0),f(g(u))). % 0.68/0.86 1323[0:Res:25.0,1321.0] || -> LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u))))*. % 0.68/0.86 1324[0:Res:1322.0,15.1] || iLEQ(u,v)*+ -> LE(f(g(u)),s(0)) E(s(0),f(g(u)))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.86 1327[0:Res:1323.2,35.1] || E(s(0),f(g(u))) -> LE(f(u),s(s(s(0)))) LE(f(g(g(u))),s(0))*. % 0.68/0.86 1329[0:Res:1327.2,34.1] || E(s(0),f(g(u)))+ iLEQ(g(g(u)),v)* -> LE(f(u),s(s(s(0))))* E(0,f(v)). % 0.68/0.86 1331[0:Res:29.0,1324.0] || -> LE(f(g(u)),s(0)) E(s(0),f(g(u))) LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 0.68/0.86 1332[0:Res:25.0,1324.0] || -> LE(f(g(u)),s(0)) E(s(0),f(g(u))) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))*. % 0.68/0.86 1343[0:Res:1332.3,36.1] || E(s(s(0)),f(u)) -> LE(f(g(u)),s(0)) E(s(0),f(g(u))) LE(f(g(u)),s(s(0)))*. % 0.68/0.86 1349[0:Res:1343.3,32.1] || E(s(s(0)),f(u))*+ iLEQ(g(u),v)* -> LE(f(g(u)),s(0)) E(s(0),f(g(u))) LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.86 1384[0:Res:1331.3,1349.0] || iLEQ(g(u),v)* -> LE(f(g(u)),s(0)) E(s(0),f(g(u)))* LE(f(u),s(s(0))) LE(f(g(u)),s(0)) E(s(0),f(g(u)))* LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.88 1392[0:Obv:1384.2] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) E(s(0),f(g(u)))* LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.88 1393[0:Res:29.0,1392.0] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) E(s(0),f(g(u)))* LE(f(g(u)),s(0)) E(s(0),f(g(u)))*. % 0.68/0.88 1395[0:Obv:1393.2] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) E(s(0),f(g(u)))*. % 0.68/0.88 1403[0:Res:1395.2,1329.0] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(u),s(s(s(0))))* E(0,f(v)). % 0.68/0.88 1408[0:Res:29.0,1403.0] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(u),s(s(s(0))))* E(0,f(g(g(u)))). % 0.68/0.88 1409[0:Res:25.0,1403.0] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(u),s(s(s(0)))) E(0,f(g(g(g(u)))))*. % 0.68/0.88 1411[0:Res:1409.3,33.1] || E(0,f(g(g(u)))) -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(u),s(s(s(0))))*. % 0.68/0.88 1412[0:MRR:1411.0,1408.3] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(u),s(s(s(0))))*. % 0.68/0.88 1413[0:Res:1412.2,15.1] || iLEQ(u,v)*+ -> LE(f(u),s(s(0))) LE(f(g(u)),s(0))* LE(f(v),s(s(0))) E(s(s(0)),f(v))*. % 0.68/0.88 1414[0:Res:29.0,1413.0] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 0.68/0.88 1415[0:Res:25.0,1413.0] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(g(u)),s(s(0))) E(s(s(0)),f(g(u)))*. % 0.68/0.88 1416[0:Obv:1414.0] || -> LE(f(g(u)),s(0)) LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 0.68/0.88 1439[0:Res:1415.3,36.1] || E(s(s(0)),f(u)) -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(g(u)),s(s(0)))*. % 0.68/0.88 1445[0:MRR:1439.0,1416.2] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(g(u)),s(s(0)))*. % 0.68/0.88 1448[0:Res:1445.2,32.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(0))) LE(f(g(u)),s(0))* LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.88 1450[0:Res:25.0,1448.0] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(g(g(u))),s(0)) E(s(0),f(g(g(u))))*. % 0.68/0.88 1454[0:Res:1450.3,35.1] || E(s(0),f(g(u))) -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(g(g(u))),s(0))*. % 0.68/0.88 1455[0:MRR:1454.0,1395.2] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) LE(f(g(g(u))),s(0))*. % 0.68/0.88 1456[0:Res:1455.2,34.1] || iLEQ(g(g(u)),v)*+ -> LE(f(u),s(s(0))) LE(f(g(u)),s(0))* E(0,f(v)). % 0.68/0.88 1466[0:Res:29.0,1456.0] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) E(0,f(g(g(u))))*. % 0.68/0.88 1467[0:Res:25.0,1456.0] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)) E(0,f(g(g(g(u)))))*. % 0.68/0.88 1470[0:Res:1467.2,33.1] || E(0,f(g(g(u))))* -> LE(f(u),s(s(0))) LE(f(g(u)),s(0)). % 0.68/0.88 1471[0:MRR:1470.0,1466.2] || -> LE(f(u),s(s(0))) LE(f(g(u)),s(0))*. % 0.68/0.88 1473[0:Res:1471.1,34.1] || iLEQ(g(u),v)*+ -> LE(f(u),s(s(0)))* E(0,f(v))*. % 0.68/0.88 1474[0:Res:29.0,1473.0] || -> LE(f(u),s(s(0)))* E(0,f(g(u))). % 0.68/0.88 1475[0:Res:25.0,1473.0] || -> LE(f(u),s(s(0))) E(0,f(g(g(u))))*. % 0.68/0.88 1477[0:Res:1475.1,33.1] || E(0,f(g(u))) -> LE(f(u),s(s(0)))*. % 0.68/0.88 1478[0:MRR:1477.0,1474.1] || -> LE(f(u),s(s(0)))*. % 0.68/0.88 1479[0:MRR:32.1,1478.0] || iLEQ(u,v)*+ -> LE(f(v),s(0)) E(s(0),f(v))*. % 0.68/0.88 1480[0:Res:29.0,1479.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 0.68/0.88 1483[0:Res:1480.1,35.1] || E(s(0),f(u)) -> LE(f(g(u)),s(0))*. % 0.68/0.88 1484[0:Res:1483.1,34.1] || E(s(0),f(u))*+ iLEQ(g(u),v)* -> E(0,f(v))*. % 0.68/0.88 1485[0:Res:1480.1,1484.0] || iLEQ(g(u),v)*+ -> LE(f(u),s(0))* E(0,f(v))*. % 0.68/0.88 1486[0:Res:29.0,1485.0] || -> LE(f(u),s(0)) E(0,f(g(u)))*. % 0.68/0.88 1487[0:Res:25.0,1485.0] || -> LE(f(u),s(0)) E(0,f(g(g(u))))*. % 0.68/0.88 1490[0:Res:1487.1,33.1] || E(0,f(g(u)))* -> LE(f(u),s(0)). % 0.68/0.88 1491[0:MRR:1490.0,1486.1] || -> LE(f(u),s(0))*. % 0.68/0.88 1492[0:MRR:34.1,1491.0] || iLEQ(u,v)*+ -> E(0,f(v))*. % 0.68/0.88 1493[0:Res:29.0,1492.0] || -> E(0,f(u))*. % 0.68/0.88 1495[0:MRR:33.1,33.0,1493.0] || -> . % 0.68/0.88 % SZS output end Refutation % 0.68/0.88 Formulae used in the proof : clause_8_01 clause_1_06 clause_6_07 clause_3_10 clause_21_11 clause_27_12 clause_30_13 clause_16_15 clause_7_16 clause_26_17 clause_29_24 clause_22_25 clause_2_29 clause_12_30 clause_24_31 clause_17_32 % 0.68/0.88 %------------------------------------------------------------------------------