%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO665-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:25 EDT 2022 % Result : Unsatisfiable 19.02s 19.20s % Output : Refutation 20.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYO665-1 : TPTP v8.1.0. Released v7.3.0. % 0.11/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n016.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 : Fri Jul 8 20:01:23 EDT 2022 % 0.12/0.34 % CPUTime : % 19.02/19.20 % 19.02/19.20 SPASS V 3.9 % 19.02/19.20 SPASS beiseite: Proof found. % 19.02/19.20 % SZS status Theorem % 19.02/19.20 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.02/19.20 SPASS derived 4771 clauses, backtracked 0 clauses, performed 0 splits and kept 1681 clauses. % 19.02/19.20 SPASS allocated 75180 KBytes. % 19.02/19.20 SPASS spent 0:0:18.85 on the problem. % 19.02/19.20 0:00:00.04 for the input. % 19.02/19.20 0:00:00.00 for the FLOTTER CNF translation. % 19.02/19.20 0:00:00.49 for inferences. % 19.02/19.20 0:00:00.00 for the backtracking. % 19.02/19.20 0:0:18.20 for the reduction. % 19.02/19.20 % 19.02/19.20 % 19.02/19.20 Here is a proof with depth 9, length 187 : % 19.02/19.20 % SZS output start Refutation % 19.02/19.20 1[0:Inp] || LE(f(z__dfg),0)* -> . % 19.02/19.20 2[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 3[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(y))))* E(s(0),f(suc(suc(x))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(s(0),f(suc(y))) -> E(f(u),f(suc(u)))*. % 19.02/19.20 4[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))*. % 19.02/19.20 5[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(suc(y))) E(0,f(x)) E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))*. % 19.02/19.20 6[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(x))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(y),f(suc(y)))*. % 19.02/19.20 7[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v)))+ E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(x),f(suc(x)))* E(f(v),f(suc(v)))*. % 19.02/19.20 8[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 19.02/19.20 9[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(w))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))*. % 19.02/19.20 10[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(y))))* E(s(0),f(suc(suc(w))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))*. % 19.02/19.20 11[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)) -> iLEQ(suc(u),suc(u)). % 19.02/19.20 12[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(u))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))*. % 19.02/19.20 13[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> E(s(0),f(suc(suc(u)))) LE(f(u),s(0)). % 19.02/19.20 14[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(v)) E(0,f(suc(y))) E(0,f(x)) E(f(w),f(suc(w)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 15[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 19.02/19.20 16[0:Inp] || E(0,f(suc(suc(u)))) E(0,f(suc(u))) E(f(u),f(suc(u)))* E(0,f(u)) -> iLEQ(suc(u),suc(u)). % 19.02/19.20 17[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(y),f(suc(y)))* E(f(w),f(suc(w)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(y))))* E(s(0),f(suc(suc(w))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))*. % 19.02/19.20 18[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 19.02/19.20 19[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(y),f(suc(y)))* E(f(x),f(suc(x)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(y))))* E(s(0),f(suc(suc(x))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(s(0),f(suc(y))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 20[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(w))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))*. % 19.02/19.20 21[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> . % 19.02/19.20 22[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 19.02/19.20 23[0:Inp] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w)))+ E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(y),f(suc(y)))* E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 19.02/19.20 24[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(x)) E(f(w),f(suc(w)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 25[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(y),f(suc(y)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(y))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))*. % 19.02/19.20 26[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(v)) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(u),f(suc(u)))*. % 19.02/19.20 27[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 19.02/19.20 28[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(x)) E(f(u),f(suc(u)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))*. % 19.02/19.20 29[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(x)) E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))* E(f(y),f(suc(y)))*. % 19.02/19.20 30[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(w),f(suc(w)))*. % 19.02/19.20 31[0:Inp] || LE(f(u),s(s(0)))* -> E(s(0),f(u)) LE(f(u),s(0)). % 19.02/19.20 32[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(x),f(suc(x)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(x))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(y),f(suc(y)))* E(f(v),f(suc(v)))*. % 19.02/19.20 33[0:Inp] || LE(f(suc(u)),s(s(0)))* -> E(s(0),f(suc(u))) LE(f(u),s(0)). % 19.02/19.20 34[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 19.02/19.20 35[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(w),f(suc(w)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(u),f(suc(u)))*. % 19.02/19.20 36[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(v)) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(u),f(suc(u)))*. % 19.02/19.20 37[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(y),f(suc(y)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(y))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 19.02/19.20 38[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(v)) E(0,f(suc(y))) E(0,f(x)) E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 39[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(suc(y))) E(0,f(x)) E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(y),f(suc(y)))*. % 19.02/19.20 40[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(v),f(suc(v)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(y),f(suc(y)))*. % 19.02/19.20 41[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 19.02/19.20 42[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(y),f(suc(y)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(y))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 43[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(x)) E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 44[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 45[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(y),f(suc(y)))* E(f(w),f(suc(w)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(y))))* E(s(0),f(suc(suc(w))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 46[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(v)) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(x),f(suc(x)))* E(f(u),f(suc(u)))*. % 19.02/19.20 47[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(y),f(suc(y)))* E(f(x),f(suc(x)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(y))))* E(s(0),f(suc(suc(x))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(v),f(suc(v)))*. % 19.02/19.20 48[0:Inp] || -> LE(f(u),s(s(0)))*. % 19.02/19.20 49[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(suc(y))) E(0,f(x)) E(f(u),f(suc(u)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(x),f(suc(x)))* E(f(y),f(suc(y)))*. % 19.02/19.20 50[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(v),f(suc(v)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))*. % 19.02/19.20 51[0:Inp] || E(s(0),f(u)) E(s(0),f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 19.02/19.20 52[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(x)) E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 53[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(y))))* E(s(0),f(suc(suc(x))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> . % 19.02/19.20 54[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(x),f(suc(x)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(x))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(s(0),f(suc(y))) -> E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 55[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(w),f(suc(w)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(w))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 56[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(u))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))*. % 19.02/19.20 57[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(x))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(s(0),f(suc(y))) -> E(f(y),f(suc(y)))* E(f(u),f(suc(u)))*. % 19.02/19.20 58[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(x)) -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 59[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(y))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))*. % 19.02/19.20 60[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(v),f(suc(v)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))*. % 19.02/19.20 61[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(x),f(suc(x)))*. % 19.02/19.20 62[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(y))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 19.02/19.20 63[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(y))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))*. % 19.02/19.20 64[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(x)) E(f(u),f(suc(u)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(y),f(suc(y)))*. % 19.02/19.20 65[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(y))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))*. % 19.02/19.20 66[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(v)) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(w),f(suc(w)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))*. % 19.02/19.20 67[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(f(x),f(suc(x)))* E(0,f(v)) E(0,f(suc(suc(x)))) E(0,f(suc(y))) E(0,f(x)) E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(y),f(suc(y)))*. % 19.02/19.20 68[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(y))))* E(s(0),f(suc(suc(w))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))*. % 19.02/19.20 69[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(suc(y))) E(0,f(x)) E(f(u),f(suc(u)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(y),f(suc(y)))*. % 19.02/19.20 70[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(x))) E(s(0),f(w)) E(s(0),f(suc(w))) iLEQ(suc(w),suc(x))* E(f(y),f(suc(y)))* E(s(0),f(x)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(y))))* E(f(w),f(suc(w)))* iLEQ(suc(u),suc(v))* iLEQ(suc(x),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 71[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 19.02/19.20 72[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(w)))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(v)) E(0,f(suc(y))) E(0,f(x)) E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 73[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(0,f(suc(suc(v)))) E(f(v),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(x),f(suc(x)))*. % 19.02/19.20 74[0:Inp] || E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(w))) iLEQ(suc(w),suc(v))* iLEQ(suc(v),suc(x))* E(0,f(suc(u))) E(0,f(w)) iLEQ(suc(x),suc(u))* E(0,f(y)) iLEQ(suc(u),suc(y))* E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(suc(y))) E(0,f(suc(suc(y)))) E(0,f(x)) E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 75[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(w),f(suc(w)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(w))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(f(u),f(suc(u)))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))*. % 19.02/19.20 76[0:Inp] || E(s(0),f(suc(u))) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(x)) E(s(0),f(suc(x))) iLEQ(suc(x),suc(w))* E(f(v),f(suc(v)))* E(s(0),f(w)) iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(y)) E(s(0),f(suc(suc(v))))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(y))* E(s(0),f(suc(y))) -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))*. % 19.02/19.20 77[0:MRR:31.0,48.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 19.02/19.20 78[0:MRR:33.0,48.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 19.02/19.20 79[0:MRR:13.0,48.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 19.02/19.20 80[0:MRR:16.2,34.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u))*. % 19.02/19.20 81[0:MRR:11.2,51.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u))*. % 19.02/19.20 82[0:MRR:26.15,23.15] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))*+ iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 83[0:MRR:38.15,23.18] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(x),f(suc(x)))*. % 19.02/19.20 84[0:MRR:58.11,23.14] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(u))))*+ iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 85[0:MRR:69.15,23.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(y))))*+ iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 86[0:MRR:72.15,23.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(x))))*+ iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 87[0:MRR:14.15,14.17,83.15,86.15] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(u),f(suc(u)))*. % 19.02/19.20 88[0:MRR:18.11,18.17,82.17,84.18] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))*+ E(0,f(suc(suc(u))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(y),f(suc(y)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 89[0:MRR:36.16,36.17,86.18,82.15] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))*+ E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 90[0:MRR:39.16,39.17,86.17,85.15] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(y))))*+ E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 91[0:MRR:43.11,43.17,83.16,84.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(u))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(x),f(suc(x)))*. % 19.02/19.20 92[0:MRR:46.15,46.17,83.18,82.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(w))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(y),f(suc(y)))* E(f(u),f(suc(u)))* E(f(x),f(suc(x)))*. % 19.02/19.20 93[0:MRR:49.15,49.17,83.17,85.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(y))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))* E(f(x),f(suc(x)))*. % 19.02/19.20 94[0:MRR:52.12,52.17,86.16,84.15] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(u))))*+ E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))* E(f(v),f(suc(v)))*. % 19.02/19.20 95[0:MRR:64.12,64.17,85.17,84.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(u))))*+ E(0,f(suc(suc(y))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 96[0:MRR:74.16,74.17,85.18,82.18] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))*+ E(0,f(suc(suc(y))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 97[0:MRR:12.14,7.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(w))))*+ -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 98[0:MRR:42.7,7.14] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 99[0:MRR:44.12,7.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(y))))*+ -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 19.02/19.20 100[0:MRR:55.7,7.16] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(y),f(suc(y)))*. % 19.02/19.20 101[0:MRR:76.7,7.15] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(x))))*+ -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 102[0:MRR:2.17,2.18,2.19,90.18,89.18,96.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))*+ E(0,f(suc(suc(y))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 19.02/19.20 103[0:MRR:5.16,5.17,5.19,87.17,93.16,90.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(y))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 19.02/19.20 104[0:MRR:8.11,8.17,8.19,92.17,91.18,88.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(w))))* E(0,f(suc(suc(u))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(y),f(suc(y)))* E(f(x),f(suc(x)))*. % 19.02/19.20 105[0:MRR:22.12,22.18,22.19,89.17,94.18,88.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))*+ E(0,f(suc(suc(u))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(y),f(suc(y)))* E(f(v),f(suc(v)))*. % 19.02/19.20 106[0:MRR:24.12,24.17,24.19,87.16,91.16,94.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(u))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))*. % 19.02/19.20 107[0:MRR:27.12,27.18,27.19,96.18,95.18,88.18] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))*+ E(0,f(suc(suc(u))))* E(0,f(suc(suc(y))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 19.02/19.20 108[0:MRR:28.12,28.17,28.19,93.17,91.17,95.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(u))))* E(0,f(suc(suc(y))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(x),f(suc(x)))*. % 19.02/19.20 109[0:MRR:29.13,29.18,29.19,90.17,94.17,95.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(u))))*+ E(0,f(suc(suc(y))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 19.02/19.20 110[0:MRR:66.16,66.17,66.19,87.18,92.16,89.16] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(w))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(y),f(suc(y)))* E(f(u),f(suc(u)))*. % 19.02/19.20 111[0:MRR:73.16,73.17,73.19,93.18,92.18,96.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(w))))* E(0,f(suc(suc(y))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(x)))*. % 19.02/19.20 112[0:MRR:20.7,20.8,100.18,101.16] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(x))))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(y),f(suc(y)))*. % 19.02/19.20 113[0:MRR:37.7,37.16,97.17,98.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(w))))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 114[0:MRR:40.7,40.16,97.18,101.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(w))))*+ E(s(0),f(suc(suc(x))))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 115[0:MRR:45.7,45.8,100.16,98.16] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(y),f(suc(y)))*. % 19.02/19.20 116[0:MRR:54.8,54.14,99.15,100.15] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(y))))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 19.02/19.20 117[0:MRR:56.13,56.16,97.15,99.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(w))))*+ E(s(0),f(suc(suc(y))))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 19.02/19.20 118[0:MRR:60.8,60.14,99.18,101.15] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(x))))*+ E(s(0),f(suc(suc(y))))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 19.02/19.20 119[0:MRR:62.7,62.8,101.17,98.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(x))))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 120[0:MRR:70.8,70.14,99.16,98.15] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(y))))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 19.02/19.20 121[0:MRR:75.7,75.16,97.16,100.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(w))))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))* E(f(y),f(suc(y)))*. % 19.02/19.20 122[0:MRR:4.13,4.19,4.20,4.21,102.18,109.18,105.18,107.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))*+ E(0,f(suc(suc(u))))* E(0,f(suc(suc(y))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(v),f(suc(v)))*. % 19.02/19.20 123[0:MRR:30.12,30.18,30.19,30.21,111.18,108.18,104.18,107.18] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(w))))* E(0,f(suc(suc(u))))* E(0,f(suc(suc(y))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(x),f(suc(x)))*. % 19.02/19.20 124[0:MRR:35.12,35.18,35.19,35.21,110.17,106.18,104.17,105.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(w))))* E(0,f(suc(suc(u))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(y),f(suc(y)))*. % 19.02/19.20 125[0:MRR:61.17,61.18,61.19,61.21,103.18,110.18,111.17,102.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(w))))* E(0,f(suc(suc(y))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(u),f(suc(u)))*. % 19.02/19.20 126[0:MRR:67.13,67.18,67.19,67.21,103.17,106.17,108.17,109.17] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(u))))* E(0,f(suc(suc(y))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> E(f(w),f(suc(w)))*. % 19.02/19.20 127[0:MRR:9.7,9.8,9.18,121.18,114.17,112.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* -> E(f(v),f(suc(v)))* E(f(y),f(suc(y)))*. % 19.02/19.20 128[0:MRR:10.7,10.8,10.9,112.17,115.18,119.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(x))))* -> E(f(w),f(suc(w)))* E(f(y),f(suc(y)))*. % 19.02/19.20 129[0:MRR:17.7,17.8,17.18,121.17,113.17,115.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(w))))* -> E(f(x),f(suc(x)))* E(f(y),f(suc(y)))*. % 19.02/19.20 130[0:MRR:19.8,19.9,19.16,116.16,120.16,115.16] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(y))))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))*. % 19.02/19.20 131[0:MRR:25.8,25.15,25.18,117.17,113.16,120.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(y))))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))*. % 19.02/19.20 132[0:MRR:32.8,32.15,32.18,117.16,121.16,116.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(y))))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))*. % 19.02/19.20 133[0:MRR:50.8,50.15,50.18,117.18,114.16,118.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(w))))*+ E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 19.02/19.20 134[0:MRR:57.8,57.9,57.16,116.18,118.16,112.16] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 19.02/19.20 135[0:MRR:63.7,63.8,63.18,114.18,113.18,119.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* -> E(f(u),f(suc(u)))* E(f(y),f(suc(y)))*. % 19.02/19.20 136[0:MRR:65.8,65.9,65.16,118.17,120.18,119.16] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 19.02/19.20 137[0:MRR:21.13,21.19,21.20,21.21,21.23,125.18,126.18,124.18,123.18,122.18] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(w))))* E(0,f(suc(suc(u))))* E(0,f(suc(suc(y))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> . % 19.02/19.20 138[0:MRR:3.8,3.9,3.10,3.18,134.17,130.18,136.17,128.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> E(f(w),f(suc(w)))*. % 19.02/19.20 139[0:MRR:6.8,6.9,6.17,6.20,132.18,133.17,127.17,134.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> E(f(v),f(suc(v)))*. % 19.02/19.20 140[0:MRR:47.8,47.9,47.17,47.20,132.17,131.17,129.17,130.17] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(y))))* -> E(f(x),f(suc(x)))*. % 19.02/19.20 141[0:MRR:59.8,59.9,59.17,59.20,133.18,131.18,135.17,136.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> E(f(u),f(suc(u)))*. % 19.02/19.20 142[0:MRR:68.7,68.8,68.9,68.20,127.18,129.18,135.18,128.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* -> E(f(y),f(suc(y)))*. % 19.02/19.20 143[0:MRR:53.8,53.9,53.10,53.19,53.22,139.18,140.18,141.18,142.18,138.18] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> . % 19.02/19.20 146[0:Res:79.1,81.2] || E(s(0),f(u)) E(s(0),f(suc(u)))* -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 19.02/19.20 147[0:MRR:146.0,146.1,77.1,78.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 19.02/19.20 1734[0:Res:79.1,143.14] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(u)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(u)))* E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> LE(f(u),s(0)). % 19.02/19.20 1735[0:MRR:1734.6,1734.11,77.1,78.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(y))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> LE(f(u),s(0)). % 19.02/19.20 3085[0:Res:79.1,1735.12] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(v)) E(s(0),f(x)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(v)))* E(s(0),f(suc(y))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 3086[0:MRR:3085.4,3085.8,77.1,78.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(x)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(y))) E(s(0),f(suc(x))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(w))))*+ E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5705[0:Res:79.1,3086.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(x)) E(s(0),f(y)) E(s(0),f(w)) E(s(0),f(suc(y))) E(s(0),f(suc(x))) E(s(0),f(suc(w)))* E(s(0),f(suc(suc(x))))* E(s(0),f(suc(suc(y))))* -> LE(f(w),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5706[0:MRR:5705.6,5705.9,77.1,78.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(x)) E(s(0),f(y)) E(s(0),f(suc(y))) E(s(0),f(suc(x))) E(s(0),f(suc(suc(x))))*+ E(s(0),f(suc(suc(y))))* -> LE(f(w),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5891[0:Res:79.1,5706.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(x)) E(s(0),f(y)) E(s(0),f(suc(y))) E(s(0),f(suc(x)))* E(s(0),f(suc(suc(y))))* -> LE(f(x),s(0)) LE(f(w),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5892[0:MRR:5891.4,5891.7,77.1,78.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(y)) E(s(0),f(suc(y))) E(s(0),f(suc(suc(y))))*+ -> LE(f(x),s(0)) LE(f(w),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5896[0:Res:79.1,5892.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* E(s(0),f(y)) E(s(0),f(suc(y)))* -> LE(f(y),s(0)) LE(f(x),s(0)) LE(f(w),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5897[0:MRR:5896.4,5896.5,77.1,78.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(y),suc(u))* -> LE(f(y),s(0)) LE(f(x),s(0)) LE(f(w),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5899[0:Res:147.1,5897.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* iLEQ(suc(x),suc(w))* -> LE(f(w),s(0)) LE(f(x),s(0)) LE(f(v),s(0)) LE(f(u),s(0)) LE(f(w),s(0)) LE(f(w),s(0)). % 19.02/19.20 5906[0:Obv:5899.7] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* iLEQ(suc(x),suc(w))* -> LE(f(x),s(0)) LE(f(v),s(0)) LE(f(u),s(0)) LE(f(w),s(0)). % 19.02/19.20 5917[0:Res:147.1,5906.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* -> LE(f(v),s(0)) LE(f(w),s(0)) LE(f(v),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5924[0:Obv:5917.4] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* -> LE(f(w),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 19.02/19.20 5931[0:Res:147.1,5924.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),s(0)) LE(f(u),s(0)) LE(f(v),s(0)) LE(f(v),s(0)). % 19.02/19.20 5938[0:Obv:5931.3] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(0)) LE(f(v),s(0)). % 19.02/19.20 5945[0:Res:147.1,5938.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 19.02/19.20 5952[0:Obv:5945.1] || -> LE(f(u),s(0))*. % 19.02/19.20 5953[0:MRR:41.0,5952.0] || -> E(0,f(u))* LE(f(u),0). % 19.02/19.20 5954[0:MRR:15.0,5952.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 19.02/19.20 5955[0:MRR:71.0,5952.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 19.02/19.20 6065[0:Res:5955.0,80.2] || E(0,f(u)) E(0,f(suc(u))) -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 19.02/19.20 6077[0:Res:5955.0,137.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(y)) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(y))) E(0,f(suc(x))) E(0,f(suc(v))) E(0,f(suc(suc(w))))* E(0,f(suc(suc(u))))* E(0,f(suc(suc(y))))* E(0,f(suc(suc(x))))* iLEQ(suc(y),suc(w))* iLEQ(suc(u),suc(y))* iLEQ(suc(v),suc(u))* iLEQ(suc(x),suc(v))* -> LE(f(v),0). % 19.02/19.20 6094[0:MRR:6065.0,6065.1,5953.0,5954.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 19.02/19.20 6126[0:MRR:6077.1,6077.9,5953.0,5954.0] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(suc(v))) E(0,f(suc(u))) E(0,f(suc(x))) E(0,f(suc(w))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(u))))* E(0,f(suc(suc(x))))* E(0,f(suc(suc(w))))* iLEQ(suc(x),suc(v))* iLEQ(suc(u),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(w),suc(y))* -> LE(f(y),0). % 19.02/19.20 6892[0:Res:5955.0,6126.8] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(x)) E(0,f(suc(v))) E(0,f(suc(u))) E(0,f(suc(x))) E(0,f(suc(w))) E(0,f(suc(suc(u))))* E(0,f(suc(suc(x))))* E(0,f(suc(suc(w))))* iLEQ(suc(x),suc(v))* iLEQ(suc(u),suc(x))* iLEQ(suc(y),suc(u))* iLEQ(suc(w),suc(y))* -> LE(f(v),0) LE(f(y),0). % 19.02/19.20 6893[0:MRR:6892.1,6892.4,5953.0,5954.0] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(u))) E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(suc(u))))*+ E(0,f(suc(suc(w))))* E(0,f(suc(suc(v))))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(w))* iLEQ(suc(y),suc(u))* iLEQ(suc(v),suc(y))* -> LE(f(x),0) LE(f(y),0). % 19.02/19.20 8437[0:Res:5955.0,6893.6] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(u))) E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(suc(w))))* E(0,f(suc(suc(v))))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(w))* iLEQ(suc(y),suc(u))* iLEQ(suc(v),suc(y))* -> LE(f(u),0) LE(f(x),0) LE(f(y),0). % 19.02/19.20 8438[0:MRR:8437.0,8437.3,5953.0,5954.0] || E(0,f(u)) E(0,f(v)) E(0,f(suc(v))) E(0,f(suc(u))) E(0,f(suc(suc(v))))*+ E(0,f(suc(suc(u))))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(v))* iLEQ(suc(y),suc(x))* iLEQ(suc(u),suc(y))* -> LE(f(x),0) LE(f(w),0) LE(f(y),0). % 19.02/19.20 8447[0:Res:5955.0,8438.4] || E(0,f(u)) E(0,f(v)) E(0,f(suc(v))) E(0,f(suc(u))) E(0,f(suc(suc(u))))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(v))* iLEQ(suc(y),suc(x))* iLEQ(suc(u),suc(y))* -> LE(f(v),0) LE(f(x),0) LE(f(w),0) LE(f(y),0). % 19.02/19.20 8448[0:MRR:8447.1,8447.2,5953.0,5954.0] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))*+ iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(v))* iLEQ(suc(y),suc(x))* iLEQ(suc(u),suc(y))* -> LE(f(v),0) LE(f(x),0) LE(f(w),0) LE(f(y),0). % 19.02/19.20 8452[0:Res:5955.0,8448.2] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(v))* iLEQ(suc(y),suc(x))* iLEQ(suc(u),suc(y))* -> LE(f(u),0) LE(f(v),0) LE(f(x),0) LE(f(w),0) LE(f(y),0). % 19.02/19.20 8453[0:MRR:8452.0,8452.1,5953.0,5954.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* iLEQ(suc(x),suc(w))* iLEQ(suc(y),suc(x))* -> LE(f(y),0) LE(f(u),0) LE(f(w),0) LE(f(v),0) LE(f(x),0). % 19.02/19.20 8456[0:Res:6094.1,8453.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* iLEQ(suc(x),suc(w))* -> LE(f(v),0) LE(f(x),0) LE(f(v),0) LE(f(u),0) LE(f(v),0) LE(f(w),0). % 19.02/19.20 8458[0:Obv:8456.5] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* iLEQ(suc(x),suc(w))* -> LE(f(x),0) LE(f(u),0) LE(f(v),0) LE(f(w),0). % 20.55/20.75 8470[0:Res:6094.1,8458.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* -> LE(f(v),0) LE(f(w),0) LE(f(v),0) LE(f(v),0) LE(f(u),0). % 20.55/20.75 8472[0:Obv:8470.4] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* -> LE(f(w),0) LE(f(v),0) LE(f(u),0). % 20.55/20.75 8476[0:Res:6094.1,8472.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0) LE(f(v),0) LE(f(v),0). % 20.55/20.75 8478[0:Obv:8476.3] || iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0). % 20.55/20.75 8482[0:Res:6094.1,8478.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 20.55/20.75 8484[0:Obv:8482.1] || -> LE(f(u),0)*. % 20.55/20.75 8485[0:UnC:8484.0,1.0] || -> . % 20.55/20.75 % SZS output end Refutation % 20.55/20.75 Formulae used in the proof : clause_877 clause_782 clause_412 clause_14 clause_298 clause_82 clause_528 clause_624 clause_966 clause_438 clause_206 clause_175 clause_372 clause_1209 clause_1504 clause_1303 clause_1794 clause_264 clause_1153 clause_1025 clause_948 clause_1520 clause_672 clause_836 clause_1041 clause_270 clause_409 clause_1061 clause_851 clause_395 clause_174 clause_71 clause_1111 clause_977 clause_20 clause_998 clause_351 clause_1741 clause_1344 clause_1480 clause_1187 clause_754 clause_848 clause_1410 clause_1073 clause_1441 clause_992 clause_681 clause_1275 clause_1040 clause_804 clause_1391 clause_1256 clause_1768 clause_49 clause_1848 clause_315 clause_682 clause_1020 clause_679 clause_1283 clause_1394 clause_703 clause_307 clause_509 clause_809 clause_1536 clause_1802 clause_1752 clause_1442 clause_138 clause_1699 clause_1270 clause_319 clause_169 clause_1039 % 20.55/20.75 %------------------------------------------------------------------------------