%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO660-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:23 EDT 2022 % Result : Unsatisfiable 7.37s 7.54s % Output : Refutation 9.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYO660-1 : TPTP v8.1.0. Released v7.3.0. % 0.04/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n007.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sat Jul 9 07:38:46 EDT 2022 % 0.12/0.34 % CPUTime : % 7.37/7.54 % 7.37/7.54 SPASS V 3.9 % 7.37/7.54 SPASS beiseite: Proof found. % 7.37/7.54 % SZS status Theorem % 7.37/7.54 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.37/7.54 SPASS derived 9112 clauses, backtracked 0 clauses, performed 0 splits and kept 1731 clauses. % 7.37/7.54 SPASS allocated 73759 KBytes. % 7.37/7.54 SPASS spent 0:00:07.18 on the problem. % 7.37/7.54 0:00:00.04 for the input. % 7.37/7.54 0:00:00.00 for the FLOTTER CNF translation. % 7.37/7.54 0:00:00.33 for inferences. % 7.37/7.54 0:00:00.00 for the backtracking. % 7.37/7.54 0:00:06.76 for the reduction. % 7.37/7.54 % 7.37/7.54 % 7.37/7.54 Here is a proof with depth 3, length 159 : % 7.37/7.54 % SZS output start Refutation % 7.37/7.54 1[0:Inp] || LE(f(suc(u)),s(s(0)))* -> E(s(0),f(suc(u))) LE(f(u),s(0)). % 7.37/7.54 2[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 3[0:Inp] || LE(f(z__dfg),0)* -> . % 7.37/7.54 4[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 7.37/7.54 5[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 7.37/7.54 6[0:Inp] || E(s(0),f(u)) E(s(0),f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 7.37/7.54 7[0:Inp] || E(s(0),f(suc(suc(suc(suc(suc(u)))))))* iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(suc(suc(suc(v)))))))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(suc(suc(v))))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> . % 7.37/7.54 8[0:Inp] || E(s(0),f(suc(suc(suc(suc(suc(u)))))))* iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(u),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 9[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 10[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(u))))))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))*. % 7.37/7.54 11[0:Inp] || E(s(0),f(suc(suc(suc(suc(suc(u)))))))* iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(f(u),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(suc(suc(u))))) -> E(f(v),f(suc(v)))*. % 7.37/7.54 12[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(suc(suc(u))))))* iLEQ(suc(u),suc(u)). % 7.37/7.54 13[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 14[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(u))))))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(0,f(suc(v))) -> E(f(v),f(suc(v)))*. % 7.37/7.54 15[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))*. % 7.37/7.54 16[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(u))))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 17[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(v))))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(suc(suc(v))))))* E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 18[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 19[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 20[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(u))))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 21[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 22[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(v),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 23[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(suc(suc(suc(v)))))))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(suc(suc(v))))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 24[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 7.37/7.54 25[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(v))))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(v)) E(f(v),f(suc(suc(suc(suc(v))))))* E(f(v),f(suc(suc(v)))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(u)))*. % 7.37/7.54 26[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(v)))*. % 7.37/7.54 27[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(v))))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(v)) E(f(v),f(suc(suc(suc(suc(v))))))* E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))*. % 7.37/7.54 28[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 7.37/7.54 29[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(0)))* -> E(s(0),f(suc(suc(suc(u))))) LE(f(u),s(0)). % 7.37/7.54 30[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 31[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 32[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 33[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 34[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 35[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(s(0)))* -> E(s(0),f(suc(suc(suc(suc(u)))))) LE(f(u),s(0)). % 7.37/7.54 36[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 37[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 38[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 39[0:Inp] || E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> E(f(u),f(suc(suc(suc(suc(u))))))* iLEQ(suc(u),suc(u)). % 7.37/7.54 40[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> E(s(0),f(suc(suc(u)))) LE(f(u),s(0)). % 7.37/7.54 41[0:Inp] || E(0,f(suc(suc(u)))) E(0,f(suc(u))) E(f(u),f(suc(u))) E(0,f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 7.37/7.54 42[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(0))* -> E(0,f(suc(suc(suc(suc(u)))))) LE(f(u),0). % 7.37/7.54 43[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(suc(u)))))* iLEQ(suc(u),suc(u)). % 7.37/7.54 44[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 45[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(u))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 7.37/7.54 46[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 47[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 48[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(suc(suc(suc(v)))))))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(suc(suc(v))))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(u))))*. % 7.37/7.54 49[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(v))))))) E(0,f(suc(suc(suc(suc(suc(u))))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(suc(suc(v))))))* E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> . % 7.37/7.54 50[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(v)))*. % 7.37/7.54 51[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(suc(suc(suc(v)))))))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(suc(suc(v))))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 52[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))*. % 7.37/7.54 53[0:Inp] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u)))+ E(0,f(suc(v))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 7.37/7.54 54[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(suc(suc(u))))))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(u))) -> iLEQ(suc(u),suc(u)). % 7.37/7.54 55[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 56[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(suc(suc(suc(v)))))))* E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(suc(suc(v))))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(v),f(suc(suc(suc(v))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(u)))*. % 7.37/7.54 57[0:Inp] || LE(f(suc(suc(suc(suc(suc(u)))))),s(s(0)))* -> E(s(0),f(suc(suc(suc(suc(suc(u))))))) LE(f(u),s(0)). % 7.37/7.54 58[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(suc(v))))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(suc(suc(v))))))* E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 59[0:Inp] || LE(f(suc(suc(suc(suc(suc(u)))))),s(0))* -> E(0,f(suc(suc(suc(suc(suc(u))))))) LE(f(u),0). % 7.37/7.54 60[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 61[0:Inp] || LE(f(u),s(s(0)))* -> E(s(0),f(u)) LE(f(u),s(0)). % 7.37/7.54 62[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 7.37/7.54 63[0:Inp] || E(s(0),f(suc(suc(suc(suc(suc(u)))))))* iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(u),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(suc(suc(u))))) -> E(f(v),f(suc(suc(v))))*. % 7.37/7.54 64[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 65[0:Inp] || E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(u))) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> E(f(u),f(suc(suc(suc(u)))))* iLEQ(suc(u),suc(u)). % 7.37/7.54 66[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 67[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v)))+ E(s(0),f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 7.37/7.54 68[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 69[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 70[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 7.37/7.54 71[0:Inp] || E(s(0),f(suc(suc(u)))) E(s(0),f(suc(u))) E(f(u),f(suc(u))) E(s(0),f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 7.37/7.54 72[0:Inp] || E(s(0),f(suc(suc(suc(suc(suc(u)))))))* iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 73[0:Inp] || -> LE(f(u),s(s(0)))*. % 7.37/7.54 74[0:Inp] || E(s(0),f(suc(suc(suc(suc(suc(u)))))))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(f(u),f(suc(suc(suc(u))))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(f(u),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(suc(suc(u))))) -> iLEQ(suc(u),suc(u)). % 7.37/7.54 75[0:MRR:61.0,73.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 7.37/7.54 76[0:MRR:1.0,73.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 7.37/7.54 77[0:MRR:40.0,73.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 7.37/7.54 78[0:MRR:29.0,73.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u)))))*. % 7.37/7.54 79[0:MRR:35.0,73.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 80[0:MRR:57.0,73.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(suc(suc(u)))))))*. % 7.37/7.54 81[0:MRR:41.2,70.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 7.37/7.54 82[0:MRR:71.2,6.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 7.37/7.54 83[0:MRR:43.2,43.5,81.3,70.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 84[0:MRR:45.5,53.5] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 85[0:MRR:46.5,53.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u))))+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 7.37/7.54 86[0:MRR:65.3,65.4,82.3,6.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 87[0:MRR:60.6,67.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v))))+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 88[0:MRR:62.6,67.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 7.37/7.54 89[0:MRR:68.6,68.7,85.6,84.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 7.37/7.54 90[0:MRR:32.6,32.7,85.7,53.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 91[0:MRR:52.2,52.7,84.6,53.5] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 92[0:MRR:12.2,12.5,12.7,81.3,83.4,70.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 93[0:MRR:69.7,69.8,88.7,87.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v))))+ E(s(0),f(suc(suc(u)))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 7.37/7.54 94[0:MRR:2.7,2.8,67.6,87.7] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 95[0:MRR:15.6,15.7,88.6,67.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 96[0:MRR:39.2,39.5,39.6,86.4,82.3,6.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u)))))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 97[0:MRR:54.2,54.6,54.7,54.9,81.3,92.5,83.4,70.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(suc(u)))))))*+ -> iLEQ(suc(u),suc(u))*. % 7.37/7.54 98[0:MRR:19.7,19.8,19.9,89.8,90.7,84.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 99[0:MRR:47.3,47.8,47.9,89.7,85.6,91.8] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v)))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 100[0:MRR:74.3,74.6,74.7,74.8,86.4,82.3,6.2,96.5] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(suc(u)))))))*+ -> iLEQ(suc(u),suc(u))*. % 7.37/7.54 101[0:MRR:9.6,9.8,9.9,90.8,85.7,53.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 102[0:MRR:50.2,50.6,50.9,84.6,91.7,53.5] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v))))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 103[0:MRR:13.7,13.8,13.9,93.7,95.8,87.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))+ -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 104[0:MRR:30.8,30.9,30.10,88.7,94.7,93.8] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(v)))))+ -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 105[0:MRR:22.8,22.9,22.10,67.6,94.8,87.7] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v))))))+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 106[0:MRR:26.3,26.8,26.9,95.7,88.6,67.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u))))))+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 107[0:MRR:14.2,14.7,14.8,14.11,84.6,102.8,91.7,53.5] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(0,f(suc(suc(suc(suc(suc(v)))))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))*. % 7.37/7.54 108[0:MRR:25.7,25.9,25.10,25.11,90.8,101.9,85.7,53.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(suc(u)))))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))*. % 7.37/7.54 109[0:MRR:33.3,33.9,33.10,33.11,98.8,99.9,90.7,91.8] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v)))))+ E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 110[0:MRR:18.7,18.9,18.10,18.11,98.9,89.8,101.8,84.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 111[0:MRR:37.3,37.7,37.10,37.11,89.7,99.8,85.6,102.9] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v))))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 112[0:MRR:11.4,11.9,11.10,11.11,95.7,88.6,67.5,106.8] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(suc(u)))))))*+ -> E(f(v),f(suc(v)))*. % 7.37/7.54 113[0:MRR:56.7,56.10,56.11,56.12,105.9,67.6,94.8,87.7] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(suc(suc(suc(suc(suc(v)))))))*+ -> E(f(u),f(suc(u)))*. % 7.37/7.54 114[0:MRR:55.8,55.9,55.10,55.12,104.8,95.8,94.7,103.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))+ E(s(0),f(suc(suc(suc(v))))) -> E(f(v),f(suc(suc(suc(v)))))* E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 115[0:MRR:21.9,21.10,21.11,21.12,88.7,105.8,104.9,93.8] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v))))))+ -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 116[0:MRR:66.4,66.9,66.10,66.11,103.8,93.7,106.9,87.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u))))))+ -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 117[0:MRR:10.3,10.8,10.9,10.12,10.13,89.7,111.9,99.8,85.6,107.9] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(0,f(suc(suc(suc(suc(suc(v)))))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))*. % 7.37/7.54 118[0:MRR:27.8,27.10,27.11,27.12,27.13,98.9,110.10,89.8,108.9,84.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(suc(u)))))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(v))))*. % 7.37/7.54 119[0:MRR:31.3,31.8,31.11,31.12,31.13,98.8,109.9,111.10,90.7,102.9] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(v))))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 120[0:MRR:34.3,34.8,34.11,34.12,34.13,110.9,109.10,99.9,101.8,91.8] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(suc(v)))))* E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 121[0:MRR:48.8,48.11,48.12,48.13,48.14,115.10,88.7,113.9,104.9,93.8] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(suc(suc(suc(suc(suc(v)))))))*+ -> E(f(u),f(suc(suc(u))))*. % 7.37/7.54 122[0:MRR:63.5,63.10,63.11,63.12,63.13,103.8,93.7,112.9,87.6,116.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(suc(u)))))))*+ -> E(f(v),f(suc(suc(v))))*. % 7.37/7.54 123[0:MRR:38.4,38.10,38.11,38.12,38.14,114.9,104.8,106.9,94.7,116.10] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(u))))))+ -> E(f(v),f(suc(suc(suc(v)))))* E(f(u),f(suc(suc(suc(suc(u))))))*. % 7.37/7.54 124[0:MRR:44.9,44.10,44.11,44.12,44.14,115.9,95.8,105.8,114.10,103.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v))))))+ -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 125[0:MRR:16.3,16.9,16.10,16.13,16.14,16.15,98.8,119.10,109.9,117.10,90.7,107.9] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(v)))))) E(0,f(suc(suc(suc(suc(suc(v)))))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(suc(u)))))*. % 7.37/7.54 126[0:MRR:17.3,17.9,17.12,17.13,17.14,17.15,118.10,109.10,120.11,99.9,108.9,91.8] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(suc(u)))))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(suc(v)))))*. % 7.37/7.54 127[0:MRR:36.3,36.8,36.10,36.13,36.14,36.15,110.9,120.10,119.11,111.10,101.8,102.9] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))+ E(0,f(suc(suc(suc(suc(v)))))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(suc(suc(u))))))* E(f(v),f(suc(suc(suc(suc(v))))))*. % 7.37/7.54 128[0:MRR:8.5,8.11,8.12,8.13,8.14,8.16,114.9,104.8,112.9,94.7,123.10,122.10] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(suc(u)))))))*+ -> E(f(v),f(suc(suc(suc(v)))))*. % 9.55/9.72 129[0:MRR:51.8,51.11,51.12,51.13,51.14,51.16,124.11,121.10,95.8,113.9,114.10,103.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(suc(suc(suc(suc(suc(v)))))))*+ -> E(f(u),f(suc(suc(suc(u)))))*. % 9.55/9.72 130[0:MRR:64.5,64.11,64.12,64.13,64.14,64.16,124.10,115.9,106.9,105.8,123.11,116.10] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(u))))))+ E(s(0),f(suc(suc(suc(suc(v)))))) -> E(f(v),f(suc(suc(suc(suc(v))))))* E(f(u),f(suc(suc(suc(suc(u))))))*. % 9.55/9.72 131[0:MRR:20.3,20.9,20.10,20.12,20.15,20.16,20.17,110.9,127.11,120.10,125.11,117.10,101.8,107.9] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(v)))))) E(0,f(suc(suc(suc(suc(suc(v)))))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(suc(suc(u))))))*. % 9.55/9.72 132[0:MRR:58.3,58.9,58.11,58.14,58.15,58.16,58.17,118.10,126.11,119.11,127.12,111.10,108.9,102.9] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(v)))))) E(0,f(suc(suc(suc(suc(suc(u)))))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(suc(suc(v))))))*. % 9.55/9.72 133[0:MRR:23.6,23.10,23.13,23.14,23.15,23.16,23.18,129.11,130.12,121.10,106.9,113.9,123.11,116.10] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(suc(suc(suc(suc(suc(v)))))))*+ -> E(f(u),f(suc(suc(suc(suc(u))))))*. % 9.55/9.72 134[0:MRR:49.3,49.10,49.11,49.13,49.16,49.17,49.18,49.19,118.10,132.12,126.11,125.11,131.12,117.10,108.9,107.9] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(v)))))) E(0,f(suc(suc(suc(suc(suc(v)))))))*+ E(0,f(suc(suc(suc(suc(suc(u)))))))* iLEQ(suc(v),suc(u))* -> . % 9.55/9.72 135[0:MRR:72.6,72.12,72.13,72.14,72.15,72.16,72.18,124.10,115.9,112.9,105.8,128.11,130.11,122.10] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(suc(suc(suc(suc(suc(u)))))))*+ -> E(f(v),f(suc(suc(suc(suc(v))))))*. % 9.55/9.72 136[0:MRR:7.7,7.11,7.14,7.15,7.16,7.17,7.18,7.20,129.11,135.12,121.10,112.9,113.9,128.11,133.12,122.10] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(v)))))) E(s(0),f(suc(suc(suc(suc(suc(v)))))))*+ E(s(0),f(suc(suc(suc(suc(suc(u)))))))* -> . % 9.55/9.72 219[0:Res:80.1,100.5] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u))))))* -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 9.55/9.72 220[0:MRR:219.0,219.1,219.2,219.3,219.4,75.1,76.1,77.1,78.1,79.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 9.55/9.72 6297[0:Res:80.1,136.11] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(v))))))* E(s(0),f(suc(suc(suc(suc(suc(u)))))))* -> LE(f(v),s(0)). % 9.55/9.72 6298[0:MRR:6297.1,6297.3,6297.5,6297.8,6297.10,75.1,76.1,77.1,78.1,79.1] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u)))))) E(s(0),f(suc(suc(suc(suc(suc(u)))))))*+ -> LE(f(v),s(0)). % 9.55/9.72 10969[0:Res:80.1,6298.6] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u))))))* -> LE(f(u),s(0)) LE(f(v),s(0)). % 9.55/9.72 10970[0:MRR:10969.1,10969.2,10969.3,10969.4,10969.5,75.1,76.1,77.1,78.1,79.1] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(0)) LE(f(v),s(0)). % 9.55/9.72 10975[0:Res:220.1,10970.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 9.55/9.72 11028[0:Obv:10975.1] || -> LE(f(u),s(0))*. % 9.55/9.72 11029[0:MRR:4.0,11028.0] || -> E(0,f(u))* LE(f(u),0). % 9.55/9.72 11030[0:MRR:24.0,11028.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 9.55/9.72 11031[0:MRR:5.0,11028.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 9.55/9.72 11032[0:MRR:28.0,11028.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 9.55/9.72 11033[0:MRR:42.0,11028.0] || -> E(0,f(suc(suc(suc(suc(u))))))* LE(f(u),0). % 9.55/9.72 11034[0:MRR:59.0,11028.0] || -> E(0,f(suc(suc(suc(suc(suc(u)))))))* LE(f(u),0). % 9.55/9.72 11333[0:Res:11034.0,97.5] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))* -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 9.55/9.72 11334[0:Res:11034.0,134.10] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(v))))))* E(0,f(suc(suc(suc(suc(suc(u)))))))* iLEQ(suc(v),suc(u))* -> LE(f(v),0). % 9.55/9.72 11347[0:MRR:11333.0,11333.1,11333.2,11333.3,11333.4,11029.0,11030.0,11031.0,11032.0,11033.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 9.55/9.72 11371[0:MRR:11334.1,11334.3,11334.4,11334.6,11334.9,11029.0,11030.0,11031.0,11032.0,11033.0] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(suc(suc(u)))))))*+ iLEQ(suc(v),suc(u))* -> LE(f(v),0). % 9.55/9.72 13927[0:Res:11034.0,11371.5] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))* iLEQ(suc(v),suc(u))* -> LE(f(u),0) LE(f(v),0). % 9.55/9.72 13928[0:MRR:13927.0,13927.1,13927.2,13927.3,13927.4,11029.0,11030.0,11031.0,11032.0,11033.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 9.55/9.72 13934[0:Res:11347.1,13928.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 9.55/9.72 13945[0:Obv:13934.1] || -> LE(f(u),0)*. % 9.55/9.72 13946[0:UnC:13945.0,3.0] || -> . % 9.55/9.72 % SZS output end Refutation % 9.55/9.72 Formulae used in the proof : clause_1847 clause_794 clause_1502 clause_1962 clause_2540 clause_1397 clause_2034 clause_2529 clause_467 clause_2680 clause_2600 clause_2932 clause_2724 clause_169 clause_572 clause_623 clause_147 clause_2543 clause_1826 clause_1946 clause_724 clause_2580 clause_2384 clause_2165 clause_1707 clause_3037 clause_733 clause_2700 clause_1276 clause_1696 clause_1388 clause_1114 clause_1574 clause_2118 clause_410 clause_1151 clause_669 clause_1225 clause_664 clause_2336 clause_70 clause_514 clause_2196 clause_1410 clause_1927 clause_3120 clause_1896 clause_2649 clause_165 clause_842 clause_344 clause_2349 clause_997 clause_249 clause_2494 clause_1158 clause_1595 clause_1195 clause_1204 clause_1186 clause_934 clause_1137 clause_1944 clause_2717 clause_2795 clause_692 clause_2550 clause_1325 clause_720 clause_1634 clause_307 clause_2827 clause_1215 clause_2367 % 9.55/9.72 %------------------------------------------------------------------------------