%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO653-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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 45.26s 45.46s % Output : Refutation 48.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYO653-1 : TPTP v8.1.0. Released v7.3.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sat Jul 9 11:39:36 EDT 2022 % 0.12/0.34 % CPUTime : % 45.26/45.46 % 45.26/45.46 SPASS V 3.9 % 45.26/45.46 SPASS beiseite: Proof found. % 45.26/45.46 % SZS status Theorem % 45.26/45.46 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 45.26/45.46 SPASS derived 6930 clauses, backtracked 0 clauses, performed 0 splits and kept 2302 clauses. % 45.26/45.46 SPASS allocated 77878 KBytes. % 45.26/45.46 SPASS spent 0:0:45.12 on the problem. % 45.26/45.46 0:00:00.05 for the input. % 45.26/45.46 0:00:00.00 for the FLOTTER CNF translation. % 45.26/45.46 0:00:00.77 for inferences. % 45.26/45.46 0:00:00.00 for the backtracking. % 45.26/45.46 0:0:44.13 for the reduction. % 45.26/45.46 % 45.26/45.46 % 45.26/45.46 Here is a proof with depth 7, length 193 : % 45.26/45.46 % SZS output start Refutation % 45.26/45.46 1[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.46 2[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 3[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w)))*. % 45.26/45.47 4[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 5[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 6[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 7[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> E(f(x),f(suc(x)))*. % 45.26/45.47 8[0:Inp] || 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(w))) E(0,f(suc(x))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(x),f(suc(x)))* E(f(w),f(suc(w)))*. % 45.26/45.47 9[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))* E(f(x),f(suc(x)))*. % 45.26/45.47 10[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 45.26/45.47 11[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 45.26/45.47 12[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 45.26/45.47 13[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 14[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 15[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))* E(f(x),f(suc(x)))*. % 45.26/45.47 16[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 17[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 45.26/45.47 18[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 19[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 20[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)). % 45.26/45.47 21[0:Inp] || LE(f(z__dfg),0)* -> . % 45.26/45.47 22[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 45.26/45.47 23[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))* E(f(x),f(suc(x)))*. % 45.26/45.47 24[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 45.26/45.47 25[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 26[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 27[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 28[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 45.26/45.47 29[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(x),f(suc(x)))*. % 45.26/45.47 30[0:Inp] || -> LE(f(u),s(0))*. % 45.26/45.47 31[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 32[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 45.26/45.47 33[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))*. % 45.26/45.47 34[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 35[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 36[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w)))*. % 45.26/45.47 37[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(w),f(suc(suc(w))))*. % 45.26/45.47 38[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 45.26/45.47 39[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 40[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 41[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) iLEQ(suc(v),suc(w))* -> E(f(w),f(suc(w)))* E(f(x),f(suc(x)))*. % 45.26/45.47 42[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> E(f(x),f(suc(suc(x))))*. % 45.26/45.47 43[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 45.26/45.47 44[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(w),f(suc(w)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 45[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))*. % 45.26/45.47 46[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 47[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(v),f(suc(v)))*. % 45.26/45.47 48[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 49[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 50[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 45.26/45.47 51[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(w),f(suc(suc(w))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 52[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))*. % 45.26/45.47 53[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 54[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 45.26/45.47 55[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(w),f(suc(w)))*. % 45.26/45.47 56[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> . % 45.26/45.47 57[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 58[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 59[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 45.26/45.47 60[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 61[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(w),f(suc(w)))*. % 45.26/45.47 62[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))*. % 45.26/45.47 63[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 45.26/45.47 64[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 65[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))*. % 45.26/45.47 66[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))*. % 45.26/45.47 67[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))* E(f(x),f(suc(x)))*. % 45.26/45.47 68[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 69[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))*. % 45.26/45.47 70[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))*. % 45.26/45.47 71[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(suc(x))))) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) E(0,f(suc(suc(suc(w))))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))*. % 45.26/45.47 72[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 73[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(f(v),f(suc(suc(v))))* E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) iLEQ(suc(v),suc(w))* -> E(f(w),f(suc(suc(w))))* E(f(x),f(suc(x)))*. % 45.26/45.47 74[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 75[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 45.26/45.47 76[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 45.26/45.47 77[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 78[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 45.26/45.47 79[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 80[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))) -> iLEQ(suc(u),suc(u)). % 45.26/45.47 81[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 45.26/45.47 82[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 45.26/45.47 83[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(f(u),f(suc(suc(u))))* E(0,f(suc(v))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 84[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 45.26/45.47 85[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 86[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(0,f(suc(suc(v)))) E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(v))))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))*. % 45.26/45.47 87[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 45.26/45.47 88[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(v))) iLEQ(suc(w),suc(x))* E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(v)) E(0,f(u)) E(0,f(x)) E(0,f(suc(w))) E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w))) E(0,f(suc(suc(w)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(suc(x))) E(0,f(w)) E(0,f(suc(suc(x)))) E(f(x),f(suc(x))) iLEQ(suc(v),suc(w))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 89[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(x),f(suc(x))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 45.26/45.47 90[0:Inp] || E(0,f(suc(u))) iLEQ(suc(v),suc(w))* E(0,f(suc(suc(u)))) E(0,f(suc(x))) E(0,f(u)) E(0,f(x)) E(0,f(w)) E(0,f(suc(v))) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(u))) iLEQ(suc(x),suc(u))* E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(suc(w))))) E(0,f(suc(suc(w)))) E(f(w),f(suc(w))) iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 45.26/45.47 91[0:MRR:54.0,30.0] || -> E(0,f(u))* LE(f(u),0). % 45.26/45.47 92[0:MRR:50.0,30.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 45.26/45.47 93[0:MRR:75.0,30.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 45.26/45.47 94[0:MRR:59.0,30.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 45.26/45.47 95[0:MRR:20.2,84.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))))*. % 45.26/45.47 96[0:MRR:80.4,80.5,95.3,84.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))*. % 45.26/45.47 97[0:MRR:14.11,8.14] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v))))+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 98[0:MRR:17.7,8.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u))))+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 99[0:MRR:63.8,8.11] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(w))))+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(x),f(suc(x)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 100[0:MRR:87.8,8.12] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(x))))+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 101[0:MRR:24.7,24.13,97.15,8.14] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(x)))* E(f(w),f(suc(w)))*. % 45.26/45.47 102[0:MRR:29.9,29.10,99.12,8.11] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(x),f(suc(x)))*. % 45.26/45.47 103[0:MRR:69.7,69.8,98.14,8.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(w),f(suc(w)))*. % 45.26/45.47 104[0:MRR:76.8,76.10,100.13,8.12] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))*. % 45.26/45.47 105[0:MRR:12.9,12.10,100.12,99.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(w))))+ E(0,f(suc(suc(x)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 106[0:MRR:18.8,18.13,97.12,99.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(w)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 107[0:MRR:74.8,74.13,97.13,100.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(x)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 108[0:MRR:78.8,78.10,99.14,98.12] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(w)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 109[0:MRR:81.8,81.10,100.14,98.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(x)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 110[0:MRR:85.7,85.13,97.14,98.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(u)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 111[0:MRR:9.10,9.11,9.12,105.13,100.12,102.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 112[0:MRR:25.9,25.10,25.15,106.13,97.12,102.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 113[0:MRR:28.8,28.10,28.12,109.14,104.14,98.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 114[0:MRR:32.9,32.11,32.12,105.14,104.13,99.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 115[0:MRR:36.8,36.9,36.11,109.15,100.14,103.14] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 116[0:MRR:48.7,48.8,48.14,110.15,97.14,103.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 117[0:MRR:58.7,58.8,58.15,110.16,101.15,98.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 118[0:MRR:67.9,67.10,67.12,108.13,102.14,98.12] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 119[0:MRR:83.8,83.10,83.15,107.14,97.13,104.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 120[0:MRR:86.8,86.9,86.11,108.15,99.14,103.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 121[0:MRR:89.8,89.9,89.15,106.16,101.13,99.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(x)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 122[0:MRR:90.8,90.9,90.15,107.16,101.14,100.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 123[0:MRR:2.8,2.10,2.15,106.15,110.13,108.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 124[0:MRR:35.9,35.10,35.15,107.13,106.14,105.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 125[0:MRR:60.8,60.10,60.15,107.15,110.14,109.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 126[0:MRR:82.9,82.11,82.12,105.15,109.13,108.14] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 127[0:MRR:10.9,10.10,10.11,10.17,112.16,121.14,101.13,102.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(x)))*. % 45.26/45.47 128[0:MRR:11.9,11.10,11.11,11.13,118.15,120.14,102.14,103.13] || 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(w))) E(0,f(suc(x))) 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(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(x)))*. % 45.26/45.47 129[0:MRR:41.10,41.12,41.13,41.14,111.14,114.14,104.13,102.13] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 45.26/45.47 130[0:MRR:45.8,45.10,45.11,45.13,115.15,113.15,104.14,103.14] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 45.26/45.47 131[0:MRR:52.7,52.8,52.9,52.16,116.16,117.16,101.15,103.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(w)))*. % 45.26/45.47 132[0:MRR:70.8,70.10,70.11,70.17,122.15,119.16,101.14,104.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))*. % 45.26/45.47 133[0:MRR:3.9,3.10,3.12,3.13,126.16,105.15,115.14,120.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 134[0:MRR:13.10,13.11,13.12,13.17,124.14,107.13,112.14,111.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 135[0:MRR:15.10,15.11,15.13,15.14,126.14,111.15,109.13,118.14] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 136[0:MRR:22.9,22.11,22.13,22.14,126.15,114.15,113.14,108.14] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 137[0:MRR:27.9,27.10,27.12,27.17,123.14,112.15,110.13,118.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 138[0:MRR:38.9,38.10,38.11,38.17,124.17,122.14,121.15,105.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 139[0:MRR:39.8,39.9,39.11,39.16,125.16,107.15,116.15,115.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 140[0:MRR:40.8,40.9,40.11,40.17,125.17,122.16,117.15,109.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 141[0:MRR:57.9,57.11,57.12,57.17,124.15,119.14,106.14,114.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 142[0:MRR:64.8,64.9,64.11,64.16,123.16,106.15,116.14,120.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 143[0:MRR:72.8,72.10,72.12,72.17,125.15,119.15,110.14,113.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 144[0:MRR:77.8,77.9,77.11,77.17,123.17,121.16,117.14,108.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 145[0:MRR:68.9,68.11,68.12,68.17,124.16,125.14,123.15,126.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 146[0:MRR:6.9,6.10,6.11,6.13,6.19,137.17,144.15,127.16,117.14,118.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 147[0:MRR:16.8,16.10,16.11,16.13,16.18,139.16,143.16,119.15,116.15,130.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 148[0:MRR:23.10,23.11,23.12,23.14,23.15,135.16,133.15,111.15,115.14,128.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 149[0:MRR:26.8,26.9,26.10,26.12,26.18,139.17,140.17,122.16,131.16,115.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(w)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 150[0:MRR:31.9,31.10,31.11,31.13,31.18,137.16,142.15,112.15,116.14,128.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) 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(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 151[0:MRR:33.8,33.9,33.10,33.12,33.18,142.17,144.17,121.16,131.15,120.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) 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(v)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 152[0:MRR:43.10,43.11,43.12,43.13,43.19,134.17,138.15,122.14,127.15,111.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 153[0:MRR:44.10,44.12,44.13,44.14,44.19,134.15,141.15,119.14,112.14,129.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 45.26/45.47 154[0:MRR:46.8,46.10,46.11,46.13,46.19,140.16,143.17,132.16,117.15,113.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 155[0:MRR:47.9,47.11,47.12,47.13,47.19,138.16,141.17,132.15,121.15,114.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 156[0:MRR:55.9,55.11,55.12,55.14,55.15,133.16,136.16,114.15,130.15,120.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 157[0:MRR:73.10,73.12,73.13,73.15,73.16,135.15,136.15,129.15,113.14,118.14] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 158[0:MRR:19.9,19.10,19.12,19.13,19.18,145.17,124.16,139.15,142.16,133.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 159[0:MRR:49.9,49.10,49.12,49.13,49.19,145.18,138.17,140.15,144.16,126.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 160[0:MRR:53.9,53.11,53.13,53.14,53.19,145.16,141.16,143.15,123.15,136.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 161[0:MRR:88.10,88.11,88.13,88.14,88.19,145.15,134.16,125.14,137.15,135.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 162[0:MRR:7.10,7.12,7.13,7.14,7.16,7.17,148.16,157.16,156.16,129.15,130.15,128.15] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(x)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(v)))*. % 45.26/45.47 163[0:MRR:61.10,61.12,61.13,61.14,61.15,61.21,152.16,153.17,155.16,132.15,127.15,129.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(x)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(u)))*. % 45.26/45.47 164[0:MRR:65.8,65.10,65.11,65.12,65.14,65.20,149.17,147.17,154.17,132.16,131.16,130.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(w)))*. % 45.26/45.47 165[0:MRR:66.9,66.10,66.11,66.12,66.14,66.20,150.17,146.17,151.16,127.16,131.15,128.16] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) 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(v)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(x)))*. % 45.26/45.47 166[0:MRR:1.10,1.11,1.12,1.14,1.15,1.21,161.18,159.16,152.17,140.15,146.16,135.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 167[0:MRR:4.9,4.11,4.12,4.14,4.15,4.21,159.17,160.18,155.17,154.16,144.16,136.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 168[0:MRR:5.10,5.11,5.12,5.14,5.15,5.20,161.17,158.16,134.16,139.15,150.16,148.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(x),f(suc(suc(x))))*. % 45.26/45.47 169[0:MRR:34.9,34.10,34.11,34.13,34.14,34.20,158.18,159.18,138.17,149.16,151.17,133.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 170[0:MRR:51.10,51.12,51.13,51.15,51.16,51.21,161.16,160.16,153.16,143.15,137.15,157.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(x)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 45.26/45.47 171[0:MRR:79.9,79.11,79.12,79.14,79.15,79.20,158.17,160.17,141.16,147.16,142.16,156.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 45.26/45.47 172[0:MRR:37.10,37.12,37.13,37.14,37.16,37.17,37.23,166.17,170.18,167.17,163.17,154.16,146.16,157.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(x)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(u),f(suc(suc(u))))*. % 45.26/45.47 173[0:MRR:42.10,42.12,42.13,42.14,42.16,42.17,42.22,168.17,170.17,171.17,153.16,147.16,150.16,162.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(x)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(v),f(suc(suc(v))))*. % 45.26/45.47 174[0:MRR:62.9,62.11,62.12,62.13,62.15,62.16,62.22,169.18,171.18,167.18,155.17,164.17,151.17,156.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(x)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(w),f(suc(suc(w))))*. % 45.26/45.47 175[0:MRR:71.10,71.11,71.12,71.13,71.15,71.16,71.22,168.18,166.18,169.17,152.17,149.16,165.17,148.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> E(f(x),f(suc(suc(x))))*. % 45.26/45.47 176[0:MRR:56.10,56.12,56.13,56.14,56.15,56.17,56.18,56.24,175.18,173.18,172.18,174.18,163.17,164.17,165.17,162.17] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(x)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> . % 45.26/45.47 180[0:Res:94.0,96.3] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))* -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 45.26/45.47 181[0:MRR:180.0,180.1,180.2,91.0,92.0,93.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 45.26/45.47 3336[0:Res:94.0,176.12] || 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(w))) E(0,f(suc(x))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u))))* E(0,f(suc(suc(w)))) E(0,f(suc(suc(x)))) E(0,f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(x)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(x),suc(u))* iLEQ(suc(w),suc(x))* iLEQ(suc(u),suc(v))* -> LE(f(u),0). % 45.26/45.47 3337[0:MRR:3336.0,3336.5,3336.9,91.0,92.0,93.0] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) 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(v)))))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* -> LE(f(x),0). % 48.28/48.50 8093[0:Res:94.0,3337.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(suc(u))))* E(0,f(suc(suc(v)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))* E(0,f(suc(suc(suc(v)))))* iLEQ(suc(w),suc(x))* iLEQ(suc(v),suc(w))* iLEQ(suc(x),suc(u))* -> LE(f(u),0) LE(f(x),0). % 48.28/48.50 8094[0:MRR:8093.0,8093.3,8093.6,91.0,92.0,93.0] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(u)))))* iLEQ(suc(v),suc(w))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* -> LE(f(x),0) LE(f(w),0). % 48.28/48.50 11497[0:Res:94.0,8094.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v))))* E(0,f(suc(suc(suc(u)))))* iLEQ(suc(v),suc(w))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* -> LE(f(v),0) LE(f(x),0) LE(f(w),0). % 48.28/48.50 11498[0:MRR:11497.1,11497.3,11497.5,91.0,92.0,93.0] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(w))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* -> LE(f(v),0) LE(f(x),0) LE(f(w),0). % 48.28/48.50 11504[0:Res:94.0,11498.3] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))* iLEQ(suc(v),suc(w))* iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(x))* -> LE(f(u),0) LE(f(v),0) LE(f(x),0) LE(f(w),0). % 48.28/48.50 11505[0:MRR:11504.0,11504.1,11504.2,91.0,92.0,93.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* iLEQ(suc(v),suc(x))* -> LE(f(w),0) LE(f(u),0) LE(f(x),0) LE(f(v),0). % 48.28/48.50 11516[0:Res:181.1,11505.0] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(v),0) LE(f(u),0) LE(f(v),0) LE(f(w),0) LE(f(v),0). % 48.28/48.50 11520[0:Obv:11516.4] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(u),0) LE(f(w),0) LE(f(v),0). % 48.28/48.50 11526[0:Res:181.1,11520.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(u),0) LE(f(v),0) LE(f(u),0). % 48.28/48.50 11530[0:Obv:11526.2] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 48.28/48.50 11536[0:Res:181.1,11530.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 48.28/48.50 11540[0:Obv:11536.1] || -> LE(f(u),0)*. % 48.28/48.50 11541[0:UnC:11540.0,21.0] || -> . % 48.28/48.50 % SZS output end Refutation % 48.28/48.50 Formulae used in the proof : clause_2175 clause_482 clause_50 clause_1508 clause_1036 clause_286 clause_2102 clause_102 clause_704 clause_971 clause_1371 clause_1048 clause_2031 clause_419 clause_554 clause_1556 clause_54 clause_316 clause_2134 clause_1719 clause_1057 clause_1596 clause_383 clause_498 clause_1550 clause_114 clause_244 clause_306 clause_872 clause_2036 clause_1387 clause_1143 clause_912 clause_961 clause_903 clause_683 clause_227 clause_268 clause_541 clause_1773 clause_51 clause_2198 clause_68 clause_765 clause_1091 clause_1221 clause_1893 clause_1277 clause_1976 clause_1983 clause_714 clause_1480 clause_2157 clause_148 clause_142 clause_1836 clause_1953 clause_1615 clause_1528 clause_295 clause_263 clause_433 clause_107 clause_1791 clause_94 clause_1568 clause_1883 clause_1384 clause_2160 clause_2101 clause_1148 clause_1315 clause_1934 clause_931 clause_38 clause_1337 clause_391 clause_1597 clause_1404 clause_972 clause_878 clause_20 clause_1039 clause_354 clause_246 clause_877 clause_1801 clause_942 clause_380 clause_1161 % 48.28/48.50 %------------------------------------------------------------------------------