%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO651-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:20 EDT 2022 % Result : Unsatisfiable 9.26s 9.47s % Output : Refutation 10.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SYO651-1 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n019.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Fri Jul 8 17:43:23 EDT 2022 % 0.13/0.35 % CPUTime : % 9.26/9.47 % 9.26/9.47 SPASS V 3.9 % 9.26/9.47 SPASS beiseite: Proof found. % 9.26/9.47 % SZS status Theorem % 9.26/9.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 9.26/9.47 SPASS derived 5771 clauses, backtracked 0 clauses, performed 0 splits and kept 1477 clauses. % 9.26/9.47 SPASS allocated 72039 KBytes. % 9.26/9.47 SPASS spent 0:00:09.10 on the problem. % 9.26/9.47 0:00:00.04 for the input. % 9.26/9.47 0:00:00.00 for the FLOTTER CNF translation. % 9.26/9.47 0:00:00.31 for inferences. % 9.26/9.47 0:00:00.00 for the backtracking. % 9.26/9.47 0:00:08.67 for the reduction. % 9.26/9.47 % 9.26/9.47 % 9.26/9.47 Here is a proof with depth 5, length 159 : % 9.26/9.47 % SZS output start Refutation % 9.26/9.47 1[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(f(v),f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) 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)))))*. % 9.26/9.47 2[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w)))) E(f(v),f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 3[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(0,f(suc(suc(suc(suc(u)))))) -> iLEQ(suc(u),suc(u)). % 9.26/9.47 4[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(u)) E(f(u),f(suc(suc(u)))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 5[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) 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))))*. % 9.26/9.47 6[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(v)) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w)))*. % 9.26/9.47 7[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) 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))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 8[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(f(u),f(suc(suc(u)))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 9[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 10[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(w),f(suc(suc(suc(w)))))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 11[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 9.26/9.47 12[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))*. % 9.26/9.47 13[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(suc(w)))))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))*. % 9.26/9.47 14[0:Inp] || -> LE(f(u),s(0))*. % 9.26/9.47 15[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(f(w),f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 16[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) 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(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 17[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(f(u),f(suc(suc(u)))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(w)))*. % 9.26/9.47 18[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(v)) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(u)) E(f(u),f(suc(suc(u)))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 9.26/9.47 19[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 20[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w)))) E(f(v),f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) 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)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 21[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 9.26/9.47 22[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 23[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 24[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(0,f(w)) 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)))))* E(f(w),f(suc(w)))*. % 9.26/9.47 25[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 26[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 27[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(v))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 28[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(f(v),f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 29[0:Inp] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v)))+ E(0,f(suc(w))) E(0,f(suc(u))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 9.26/9.47 30[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(f(v),f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 31[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 32[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(f(u),f(suc(suc(u)))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 33[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) 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))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 34[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) 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(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(w),f(suc(w)))*. % 9.26/9.47 35[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))*. % 9.26/9.47 36[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 9.26/9.47 37[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 38[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 9.26/9.47 39[0:Inp] || LE(f(z__dfg),0)* -> . % 9.26/9.47 40[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(u)) E(f(u),f(suc(suc(u)))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 9.26/9.47 41[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 9.26/9.47 42[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(f(v),f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 43[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) 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))))* E(f(w),f(suc(w)))*. % 9.26/9.47 44[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(0))* -> E(0,f(suc(suc(suc(suc(u)))))) LE(f(u),0). % 9.26/9.47 45[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(f(v),f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 46[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(suc(u)))))* iLEQ(suc(u),suc(u)). % 9.26/9.47 47[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(suc(w)))))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))*. % 9.26/9.47 48[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 49[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(v))) -> E(f(v),f(suc(v)))*. % 9.26/9.47 50[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) 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(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(w)))*. % 9.26/9.47 51[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 9.26/9.47 52[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 53[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(w)))*. % 9.26/9.47 54[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(v))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 9.26/9.47 55[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) 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(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(w),f(suc(suc(w))))*. % 9.26/9.47 56[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 9.26/9.47 57[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 9.26/9.47 58[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(v)) iLEQ(suc(u),suc(w))* E(0,f(u)) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w)))*. % 9.26/9.47 59[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(u)) E(f(u),f(suc(suc(u)))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 60[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 61[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 9.26/9.47 62[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(0,f(w)) 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)))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 63[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 64[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(suc(suc(w)))))* E(0,f(v)) E(f(w),f(suc(suc(w)))) E(f(v),f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(0,f(suc(suc(suc(suc(u)))))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> . % 9.26/9.47 65[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(v)) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(f(u),f(suc(suc(u)))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(w)))*. % 9.26/9.47 66[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 67[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)). % 9.26/9.47 68[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(f(w),f(suc(suc(suc(w)))))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 9.26/9.47 69[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 70[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 71[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 72[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(v))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 73[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(f(w),f(suc(suc(suc(w)))))* E(0,f(u)) E(f(w),f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(suc(suc(suc(w)))))) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 9.26/9.47 74[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 9.26/9.47 75[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 76[0:MRR:57.0,14.0] || -> E(0,f(u))* LE(f(u),0). % 9.26/9.47 77[0:MRR:11.0,14.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 9.26/9.47 78[0:MRR:36.0,14.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 9.26/9.47 79[0:MRR:61.0,14.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 9.26/9.47 80[0:MRR:44.0,14.0] || -> E(0,f(suc(suc(suc(suc(u))))))* LE(f(u),0). % 9.26/9.47 81[0:MRR:67.2,74.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))))*. % 9.26/9.47 82[0:MRR:46.4,46.5,81.3,74.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)))))*. % 9.26/9.47 83[0:MRR:3.2,3.5,3.6,82.4,81.3,74.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))*. % 9.26/9.47 84[0:MRR:19.3,29.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))*. % 9.26/9.47 85[0:MRR:21.6,29.8] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 86[0:MRR:58.8,29.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(v))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))*. % 9.26/9.47 87[0:MRR:6.7,6.10,86.9,85.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w))))+ E(0,f(suc(suc(v)))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 88[0:MRR:69.3,69.8,85.11,84.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 89[0:MRR:75.4,75.10,86.11,84.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(v)))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 9.26/9.47 90[0:MRR:38.6,38.8,85.9,29.8] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 91[0:MRR:52.3,52.8,29.10,84.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 92[0:MRR:65.8,65.10,86.10,29.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 93[0:MRR:18.8,18.10,18.12,92.11,86.10,29.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) 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))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))*. % 9.26/9.47 94[0:MRR:41.3,41.7,41.9,29.10,91.12,84.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) 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))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 9.26/9.47 95[0:MRR:54.4,54.7,54.9,90.10,85.9,29.8] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 9.26/9.47 96[0:MRR:25.4,25.9,25.12,87.12,89.10,88.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 97[0:MRR:17.8,17.10,17.12,92.10,87.11,85.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 98[0:MRR:23.4,23.9,23.12,86.11,89.12,91.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 99[0:MRR:32.4,32.10,32.12,92.12,89.11,84.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 100[0:MRR:43.7,43.9,43.12,87.10,86.9,90.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(w)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 101[0:MRR:70.4,70.8,70.10,90.12,88.10,84.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 102[0:MRR:71.3,71.8,71.10,85.11,91.10,88.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 103[0:MRR:27.4,27.5,27.9,27.11,95.12,101.11,88.10,84.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 9.26/9.47 104[0:MRR:40.8,40.10,40.12,40.14,93.11,97.12,87.11,85.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) 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))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 105[0:MRR:51.5,51.8,51.10,51.14,100.11,87.10,86.9,95.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 9.26/9.47 106[0:MRR:56.3,56.8,56.9,56.11,85.11,94.11,102.13,88.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 107[0:MRR:59.4,59.10,59.12,59.14,93.12,99.12,89.11,84.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) 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))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))*. % 9.26/9.47 108[0:MRR:68.4,68.8,68.10,68.14,86.11,98.13,89.12,94.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))*. % 9.26/9.47 109[0:MRR:8.4,8.10,8.12,8.14,97.13,99.11,96.12,88.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 110[0:MRR:31.4,31.9,31.11,31.14,87.12,98.11,96.13,102.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 111[0:MRR:33.5,33.9,33.11,33.14,100.13,96.11,89.10,101.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(w)))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 112[0:MRR:24.8,24.10,24.12,24.14,97.11,92.10,100.12,90.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))+ E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 113[0:MRR:37.4,37.10,37.11,37.14,92.12,99.13,98.12,91.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))+ E(0,f(suc(suc(suc(v))))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 114[0:MRR:60.4,60.8,60.10,60.12,90.12,102.11,91.10,101.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u)))))+ E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 115[0:MRR:4.4,4.10,4.12,4.14,4.16,104.13,107.12,109.13,96.12,88.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) 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))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 116[0:MRR:22.5,22.6,22.10,22.12,22.16,105.13,111.12,96.11,89.10,103.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 9.26/9.47 117[0:MRR:73.4,73.9,73.10,73.12,73.16,87.12,108.12,110.14,96.13,106.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 9.26/9.47 118[0:MRR:10.4,10.9,10.11,10.12,10.16,92.12,113.14,99.13,108.13,94.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 119[0:MRR:12.4,12.8,12.10,12.11,12.13,90.12,106.12,94.11,114.14,101.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 120[0:MRR:48.4,48.10,48.12,48.13,48.16,93.12,113.13,107.13,98.12,91.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 121[0:MRR:50.8,50.10,50.12,50.14,50.16,104.12,93.11,112.13,100.12,90.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(v))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 122[0:MRR:53.5,53.9,53.11,53.13,53.16,112.12,97.11,92.10,105.12,95.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 123[0:MRR:72.4,72.5,72.9,72.11,72.13,95.12,114.12,102.11,91.10,103.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 124[0:MRR:7.5,7.9,7.11,7.13,7.16,100.13,110.12,98.11,111.14,114.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))+ E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 125[0:MRR:15.4,15.10,15.12,15.13,15.16,97.13,113.12,109.14,110.13,102.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))+ E(0,f(suc(suc(suc(v))))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 126[0:MRR:62.5,62.10,62.12,62.14,62.16,112.14,109.12,99.11,111.13,101.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))+ E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 127[0:MRR:34.5,34.9,34.11,34.13,34.15,34.18,121.13,104.12,93.11,122.13,105.12,95.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))*. % 9.26/9.47 128[0:MRR:47.4,47.10,47.11,47.13,47.14,47.18,93.12,118.14,120.14,107.13,108.13,94.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(u))))))*+ E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))*. % 9.26/9.47 129[0:MRR:49.4,49.5,49.9,49.11,49.12,49.14,95.12,119.13,106.12,94.11,123.14,103.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ E(0,f(suc(suc(suc(suc(u))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))*. % 9.26/9.47 130[0:MRR:5.5,5.9,5.11,5.12,5.14,5.18,100.13,117.13,108.12,124.15,111.14,119.14] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 131[0:MRR:9.4,9.10,9.11,9.13,9.14,9.18,97.13,118.13,125.15,109.14,117.14,106.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 132[0:MRR:16.5,16.10,16.12,16.14,16.16,16.18,121.14,115.13,107.12,126.14,111.13,101.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(v))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 133[0:MRR:26.5,26.6,26.10,26.12,26.14,26.18,105.13,124.13,110.12,98.11,116.14,123.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 134[0:MRR:63.5,63.6,63.11,63.13,63.15,63.18,122.14,126.13,109.12,99.11,116.13,103.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 135[0:MRR:66.4,66.10,66.12,66.14,66.15,66.18,104.13,120.13,125.14,115.14,110.13,102.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 136[0:MRR:20.5,20.10,20.12,20.14,20.15,20.18,112.14,125.13,113.12,126.15,124.14,114.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))+ E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 137[0:MRR:13.4,13.10,13.12,13.13,13.15,13.16,13.20,104.13,128.14,131.15,135.15,115.14,117.14,106.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(u))))))*+ E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(suc(w))))*. % 9.26/9.47 138[0:MRR:35.5,35.6,35.10,35.12,35.13,35.15,35.20,105.13,130.14,117.13,108.12,133.15,116.14,129.14] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ E(0,f(suc(suc(suc(suc(u))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(v))))*. % 9.26/9.47 139[0:MRR:55.5,55.6,55.11,55.13,55.15,55.17,55.20,127.14,132.14,115.13,107.12,134.14,116.13,103.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))*. % 9.26/9.47 140[0:MRR:1.5,1.10,1.12,1.13,1.15,1.16,1.20,112.14,131.14,118.13,136.16,126.15,130.15,119.14] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(suc(v)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 141[0:MRR:2.5,2.6,2.11,2.13,2.15,2.16,2.20,122.14,136.14,125.13,113.12,134.15,133.14,123.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 142[0:MRR:28.5,28.10,28.12,28.14,28.16,28.17,28.20,121.14,135.14,120.13,136.15,132.15,124.14,114.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(v))))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 143[0:MRR:30.5,30.6,30.11,30.13,30.15,30.17,30.18,30.22,127.14,142.15,135.14,120.13,141.15,139.15,133.14,123.13] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(suc(u)))))*. % 9.26/9.47 144[0:MRR:42.5,42.10,42.12,42.14,42.15,42.17,42.18,42.22,121.14,137.15,128.14,140.16,142.16,132.15,130.15,119.14] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(u))))))*+ E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(suc(suc(w)))))*. % 9.26/9.47 145[0:MRR:45.5,45.6,45.11,45.13,45.14,45.16,45.17,45.22,122.14,140.15,131.14,118.13,141.16,134.15,138.15,129.14] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ E(0,f(suc(suc(suc(suc(u))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(suc(v)))))*. % 9.26/9.47 146[0:MRR:64.5,64.6,64.11,64.13,64.15,64.16,64.18,64.19,64.24,127.14,144.16,137.15,128.14,145.16,143.16,139.15,138.15,129.14] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(suc(suc(w))))))*+ E(0,f(suc(suc(suc(suc(u))))))* E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> . % 10.53/10.76 151[0:Res:80.0,83.4] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))* -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 10.53/10.76 152[0:MRR:151.0,151.1,151.2,151.3,76.0,77.0,78.0,79.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 10.53/10.76 3498[0:Res:80.0,146.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(w)))))* E(0,f(suc(suc(suc(suc(u))))))* E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> LE(f(w),0). % 10.53/10.76 3499[0:MRR:3498.2,3498.4,3498.7,3498.11,76.0,77.0,78.0,79.0] || E(0,f(u)) E(0,f(v)) E(0,f(suc(v))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(u))))))*+ E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> LE(f(w),0). % 10.53/10.76 9058[0:Res:80.0,3499.8] || E(0,f(u)) E(0,f(v)) E(0,f(suc(v))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> LE(f(u),0) LE(f(w),0). % 10.53/10.76 9059[0:MRR:9058.0,9058.3,9058.4,9058.6,76.0,77.0,78.0,79.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))))))*+ iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* -> LE(f(v),0) LE(f(w),0). % 10.53/10.76 9283[0:Res:80.0,9059.4] || 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(v))* iLEQ(suc(w),suc(u))* -> LE(f(u),0) LE(f(v),0) LE(f(w),0). % 10.53/10.76 9284[0:MRR:9283.0,9283.1,9283.2,9283.3,76.0,77.0,78.0,79.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* -> LE(f(u),0) LE(f(v),0) LE(f(w),0). % 10.53/10.76 9289[0:Res:152.1,9284.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(v),0) LE(f(v),0) LE(f(u),0). % 10.53/10.76 9296[0:Obv:9289.2] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 10.53/10.76 9312[0:Res:152.1,9296.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 10.53/10.76 9319[0:Obv:9312.1] || -> LE(f(u),0)*. % 10.53/10.76 9320[0:UnC:9319.0,39.0] || -> . % 10.53/10.76 % SZS output end Refutation % 10.53/10.76 Formulae used in the proof : clause_2802 clause_2744 clause_1772 clause_613 clause_1532 clause_3823 clause_733 clause_1536 clause_1318 clause_3677 clause_2650 clause_2891 clause_1098 clause_3530 clause_3578 clause_187 clause_492 clause_2573 clause_3275 clause_3274 clause_1875 clause_627 clause_2277 clause_3412 clause_2612 clause_2529 clause_935 clause_255 clause_2887 clause_1563 clause_3718 clause_3339 clause_2312 clause_426 clause_3575 clause_3112 clause_2518 clause_1816 clause_1829 clause_1564 clause_408 clause_1901 clause_3408 clause_619 clause_403 clause_3827 clause_960 clause_752 clause_3337 clause_55 clause_1587 clause_896 clause_930 clause_2899 clause_3669 clause_2721 clause_2386 clause_1550 clause_3129 clause_1229 clause_3293 clause_249 clause_698 clause_3360 clause_1427 clause_2015 clause_2993 clause_2195 clause_1366 clause_2665 clause_1375 clause_3155 clause_2054 clause_636 clause_3679 % 10.53/10.76 %------------------------------------------------------------------------------