%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO686-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:32 EDT 2022 % Result : Unsatisfiable 1.31s 1.50s % Output : Refutation 1.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO686-1 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n016.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:26:54 EDT 2022 % 0.12/0.33 % CPUTime : % 1.31/1.50 % 1.31/1.50 SPASS V 3.9 % 1.31/1.50 SPASS beiseite: Proof found. % 1.31/1.50 % SZS status Theorem % 1.31/1.50 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.31/1.50 SPASS derived 4986 clauses, backtracked 0 clauses, performed 0 splits and kept 1326 clauses. % 1.31/1.50 SPASS allocated 68552 KBytes. % 1.31/1.50 SPASS spent 0:00:01.16 on the problem. % 1.31/1.50 0:00:00.04 for the input. % 1.31/1.50 0:00:00.00 for the FLOTTER CNF translation. % 1.31/1.50 0:00:00.18 for inferences. % 1.31/1.50 0:00:00.00 for the backtracking. % 1.31/1.50 0:00:00.90 for the reduction. % 1.31/1.50 % 1.31/1.50 % 1.31/1.50 Here is a proof with depth 3, length 193 : % 1.31/1.50 % SZS output start Refutation % 1.31/1.50 1[0:Inp] || E(s(s(0)),f(suc(u))) E(s(s(0)),f(u)) E(s(s(0)),f(suc(v))) E(f(v),f(suc(suc(v))))* E(s(s(0)),f(suc(suc(v)))) iLEQ(suc(v),suc(u))* E(f(v),f(suc(v))) E(s(s(0)),f(suc(suc(suc(v)))))* E(f(u),f(suc(u))) E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(u))))* -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 2[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(v))) E(0,f(v)) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 1.31/1.50 3[0:Inp] || E(f(u),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))* E(s(0),f(suc(u))) E(f(u),f(suc(suc(u))))* E(s(0),f(u)) -> iLEQ(suc(u),suc(u)). % 1.31/1.50 4[0:Inp] || E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(suc(u)))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 1.31/1.50 5[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 1.31/1.50 6[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v)))) E(s(0),f(v)) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))* E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(suc(u))) E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v))) E(s(0),f(u)) E(f(v),f(suc(suc(v))))* -> . % 1.31/1.50 7[0:Inp] || LE(f(suc(u)),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(u))). % 1.31/1.50 8[0:Inp] || E(s(s(s(s(0)))),f(u)) iLEQ(suc(v),suc(u))* E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(v))))* E(s(s(s(s(0)))),f(suc(v))) E(f(v),f(suc(v))) E(f(u),f(suc(suc(u))))* E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 9[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u))))). % 1.31/1.50 10[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(s(s(0)))))* -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(suc(suc(u))))). % 1.31/1.50 11[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(suc(u))))* E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 1.31/1.50 12[0:Inp] || E(s(s(s(s(0)))),f(u)) iLEQ(suc(v),suc(u))* E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) -> E(f(v),f(suc(v)))*. % 1.31/1.50 13[0:Inp] || E(s(s(0)),f(suc(u))) E(s(s(0)),f(u)) E(s(s(0)),f(suc(v)))* iLEQ(suc(v),suc(u))* E(f(u),f(suc(u))) E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(u))))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 14[0:Inp] || E(s(s(0)),f(suc(u))) E(s(s(0)),f(u)) E(s(s(0)),f(suc(v))) E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(v)))) iLEQ(suc(v),suc(u))* E(f(v),f(suc(v))) E(s(s(0)),f(suc(suc(suc(v)))))* E(s(s(0)),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(u)))) -> . % 1.31/1.50 15[0:Inp] || E(s(s(0)),f(suc(u))) E(f(u),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(suc(u)))))* E(s(s(0)),f(u)) -> iLEQ(suc(u),suc(u)). % 1.31/1.50 16[0:Inp] || -> LE(f(u),s(s(s(s(s(0))))))*. % 1.31/1.50 17[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 1.31/1.50 18[0:Inp] || E(s(s(s(s(0)))),f(suc(suc(suc(u)))))* E(s(s(s(s(0)))),f(suc(suc(u)))) E(f(u),f(suc(suc(u))))* E(s(s(s(s(0)))),f(suc(u))) E(f(u),f(suc(u))) E(s(s(s(s(0)))),f(u)) -> iLEQ(suc(u),suc(u)). % 1.31/1.50 19[0:Inp] || E(f(u),f(suc(u))) E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(v)) E(0,f(suc(v))) E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(suc(u))))* E(0,f(suc(u))) E(0,f(u)) -> E(f(v),f(suc(v)))*. % 1.31/1.50 20[0:Inp] || E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(suc(u))) E(f(u),f(suc(u))) E(s(s(0)),f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 1.31/1.50 21[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(u)) E(f(v),f(suc(v))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v))))* E(s(s(s(0))),f(suc(suc(u))))* E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 22[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(suc(suc(v)))))* E(s(s(s(0))),f(u)) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v)))) -> E(f(u),f(suc(u)))*. % 1.31/1.50 23[0:Inp] || LE(f(suc(u)),s(s(s(s(s(0))))))* -> E(s(s(s(s(0)))),f(suc(u))) LE(f(u),s(s(s(s(0))))). % 1.31/1.50 24[0:Inp] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u)))+ E(0,f(suc(v))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 1.31/1.50 25[0:Inp] || E(s(0),f(suc(suc(u))))* E(s(0),f(suc(u))) E(f(u),f(suc(u))) E(s(0),f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 1.31/1.50 26[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(suc(suc(v)))))* E(s(s(s(0))),f(u)) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v)))) E(s(s(s(0))),f(suc(suc(u))))* E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 27[0:Inp] || E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(u)))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 1.31/1.50 28[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 1.31/1.50 29[0:Inp] || E(0,f(u)) E(0,f(suc(suc(suc(u))))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(u))) E(f(u),f(suc(suc(u))))* -> iLEQ(suc(u),suc(u)). % 1.31/1.50 30[0:Inp] || LE(f(suc(suc(u))),s(s(s(0))))* -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(u)))). % 1.31/1.50 31[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(u))) E(s(0),f(suc(v)))* E(s(0),f(v)) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))* E(s(0),f(suc(u))) E(f(u),f(suc(suc(u))))* E(s(0),f(u)) -> E(f(v),f(suc(v)))*. % 1.31/1.50 32[0:Inp] || E(s(s(s(s(0)))),f(u)) iLEQ(suc(v),suc(u))* E(s(s(s(s(0)))),f(suc(u)))* E(s(s(s(s(0)))),f(suc(suc(v))))* E(s(s(s(s(0)))),f(suc(v))) E(f(v),f(suc(v))) E(s(s(s(s(0)))),f(v)) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(u)))*. % 1.31/1.50 33[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u)))*+ E(s(s(0)),f(suc(v)))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 1.31/1.50 34[0:Inp] || E(s(s(0)),f(suc(u)))* E(s(s(0)),f(u)) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))* iLEQ(suc(v),suc(u))* E(f(v),f(suc(v))) E(s(s(0)),f(v)) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(u)))*. % 1.31/1.50 35[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v))))* E(s(0),f(v)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(u))) E(f(v),f(suc(v))) E(s(0),f(u)) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 36[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(s(0))))* -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(suc(u))))). % 1.31/1.50 37[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v))))* E(s(0),f(v)) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))* E(s(0),f(suc(u))) E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v))) E(s(0),f(u)) -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 38[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v)))) E(s(0),f(v)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(suc(u))) E(f(v),f(suc(v))) E(s(0),f(u)) E(f(v),f(suc(suc(v))))* -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 39[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v)))*+ E(s(s(s(0))),f(suc(u)))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 1.31/1.50 40[0:Inp] || E(f(u),f(suc(u))) E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(v)) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(u)) E(f(v),f(suc(v))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 41[0:Inp] || LE(f(suc(u)),s(s(s(0))))* -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u))). % 1.31/1.50 42[0:Inp] || E(f(u),f(suc(u))) E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(v)) E(0,f(suc(suc(suc(v))))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(u)) E(f(v),f(suc(v))) E(f(v),f(suc(suc(v))))* -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 43[0:Inp] || E(s(s(s(s(0)))),f(u)) iLEQ(suc(v),suc(u))* E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(suc(v)))))* E(s(s(s(s(0)))),f(suc(suc(v)))) E(f(v),f(suc(suc(v))))* E(s(s(s(s(0)))),f(suc(v))) E(f(v),f(suc(v))) E(f(u),f(suc(suc(u))))* E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) -> . % 1.31/1.50 44[0:Inp] || E(s(s(s(s(0)))),f(suc(suc(u))))* E(s(s(s(s(0)))),f(suc(u))) E(f(u),f(suc(u))) E(s(s(s(s(0)))),f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 1.31/1.50 45[0:Inp] || LE(f(u),s(s(s(s(0)))))* -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u)). % 1.31/1.50 46[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(suc(u))))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(suc(u)))))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(u)) E(f(v),f(suc(v))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v))))* E(s(s(s(0))),f(suc(suc(u)))) E(f(u),f(suc(u))) -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 47[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(u)) E(0,f(suc(suc(suc(u))))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(v))) E(0,f(v)) E(f(u),f(suc(u))) E(f(u),f(suc(suc(u))))* -> E(f(v),f(suc(v)))*. % 1.31/1.50 48[0:Inp] || E(s(s(s(0))),f(suc(suc(u))))* E(s(s(s(0))),f(suc(u))) E(f(u),f(suc(u))) E(s(s(s(0))),f(u)) -> E(f(u),f(suc(suc(u))))* iLEQ(suc(u),suc(u)). % 1.31/1.50 49[0:Inp] || E(s(s(s(s(0)))),f(u)) iLEQ(suc(v),suc(u))* E(s(s(s(s(0)))),f(suc(suc(u))))* E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(suc(v)))))* E(s(s(s(s(0)))),f(suc(suc(v)))) E(f(v),f(suc(suc(v))))* E(s(s(s(s(0)))),f(suc(v))) E(f(v),f(suc(v))) E(s(s(s(s(0)))),f(v)) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 50[0:Inp] || E(f(u),f(suc(u))) E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(v)) E(0,f(suc(suc(suc(v))))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(suc(u))))* E(0,f(suc(u))) E(0,f(u)) E(f(v),f(suc(v))) E(f(v),f(suc(suc(v))))* -> . % 1.31/1.50 51[0:Inp] || E(s(s(s(s(0)))),f(u)) iLEQ(suc(v),suc(u))* E(s(s(s(s(0)))),f(suc(suc(u))))* E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(v))))* E(s(s(s(s(0)))),f(suc(v))) E(f(v),f(suc(v))) E(s(s(s(s(0)))),f(v)) E(f(u),f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 52[0:Inp] || LE(f(suc(suc(u))),s(s(s(s(s(0))))))* -> E(s(s(s(s(0)))),f(suc(suc(u)))) LE(f(u),s(s(s(s(0))))). % 1.31/1.50 53[0:Inp] || E(s(s(0)),f(suc(u))) E(s(s(0)),f(u)) E(s(s(0)),f(suc(v)))* E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(u))* E(s(s(0)),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(u)))) -> E(f(v),f(suc(v)))*. % 1.31/1.50 54[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(suc(u))))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(suc(u)))))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(suc(u)))) E(f(u),f(suc(u))) -> E(f(v),f(suc(v)))*. % 1.31/1.50 55[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 1.31/1.50 56[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 1.31/1.50 57[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(suc(u))))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(suc(u)))))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(suc(suc(v)))))* E(s(s(s(0))),f(u)) E(f(v),f(suc(suc(v))))* E(f(v),f(suc(v))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v)))) E(s(s(s(0))),f(suc(suc(u)))) E(f(u),f(suc(u))) -> . % 1.31/1.50 58[0:Inp] || E(s(s(s(s(0)))),f(u)) iLEQ(suc(v),suc(u))* E(s(s(s(s(0)))),f(suc(u)))* E(s(s(s(s(0)))),f(suc(suc(suc(v)))))* E(s(s(s(s(0)))),f(suc(suc(v)))) E(f(v),f(suc(suc(v))))* E(s(s(s(s(0)))),f(suc(v))) E(f(v),f(suc(v))) E(s(s(s(s(0)))),f(v)) -> E(f(u),f(suc(u)))*. % 1.31/1.50 59[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(v))))* E(s(0),f(v)) E(s(0),f(suc(u)))* E(f(v),f(suc(v))) E(s(0),f(u)) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 60[0:Inp] || LE(f(suc(u)),s(s(s(s(0)))))* -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(u))). % 1.31/1.50 61[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(u)) E(f(v),f(suc(v))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v))))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 62[0:Inp] || E(s(s(s(s(0)))),f(u)) iLEQ(suc(v),suc(u))* E(s(s(s(s(0)))),f(suc(suc(u))))* E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v)))* E(s(s(s(s(0)))),f(v)) E(f(u),f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 63[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(v)))) E(s(0),f(v)) E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(suc(u)))* E(f(v),f(suc(v))) E(s(0),f(u)) E(f(v),f(suc(suc(v))))* -> E(f(u),f(suc(u)))*. % 1.31/1.50 64[0:Inp] || E(f(u),f(suc(suc(u))))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(suc(u)))))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(suc(u)))) E(f(u),f(suc(u))) -> iLEQ(suc(u),suc(u)). % 1.31/1.50 65[0:Inp] || LE(f(u),s(s(s(0))))* -> LE(f(u),s(s(0))) E(s(s(0)),f(u)). % 1.31/1.50 66[0:Inp] || E(s(s(0)),f(suc(u))) E(s(s(0)),f(u)) E(s(s(0)),f(suc(v))) E(f(u),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(v))))* iLEQ(suc(v),suc(u))* E(f(v),f(suc(v))) E(s(s(0)),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(u)))) -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 67[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u)))*+ E(s(0),f(suc(v)))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 1.31/1.50 68[0:Inp] || E(s(s(0)),f(suc(u))) E(s(s(0)),f(u)) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))* iLEQ(suc(v),suc(u))* E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(u))))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 69[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)). % 1.31/1.50 70[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(suc(u)))). % 1.31/1.50 71[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(s(s(s(0))))))* -> E(s(s(s(s(0)))),f(suc(suc(suc(u))))) LE(f(u),s(s(s(s(0))))). % 1.31/1.50 72[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u)))*+ E(s(s(s(s(0)))),f(suc(v)))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 1.31/1.50 73[0:Inp] || iLEQ(suc(u),suc(v))* E(f(u),f(suc(u))) E(s(0),f(suc(v)))* E(s(0),f(v)) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(u))) E(s(0),f(u)) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 1.31/1.50 74[0:Inp] || E(f(u),f(suc(u))) E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(v)) E(0,f(suc(v))) E(0,f(suc(u))) E(0,f(u)) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 75[0:Inp] || E(s(0),f(u)) E(s(0),f(suc(u)))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 1.31/1.50 76[0:Inp] || LE(f(suc(suc(u))),s(s(s(s(0)))))* -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(suc(u)))). % 1.31/1.50 77[0:Inp] || LE(f(z__dfg),0)* -> . % 1.31/1.50 78[0:Inp] || E(s(s(0)),f(suc(u)))* E(s(s(0)),f(u)) E(s(s(0)),f(suc(v))) E(f(v),f(suc(suc(v))))* E(s(s(0)),f(suc(suc(v)))) iLEQ(suc(v),suc(u))* E(f(v),f(suc(v))) E(s(s(0)),f(suc(suc(suc(v)))))* E(s(s(0)),f(v)) -> E(f(u),f(suc(u)))*. % 1.31/1.50 79[0:Inp] || LE(f(u),s(s(s(s(s(0))))))* -> E(s(s(s(s(0)))),f(u)) LE(f(u),s(s(s(s(0))))). % 1.31/1.50 80[0:Inp] || E(f(u),f(suc(u))) E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(v)) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(suc(u))))* E(0,f(suc(u))) E(0,f(u)) E(f(v),f(suc(v))) -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 81[0:Inp] || LE(f(u),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(u)). % 1.31/1.50 82[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 1.31/1.50 83[0:MRR:79.0,16.0] || -> LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(u))*. % 1.31/1.50 84[0:MRR:23.0,16.0] || -> LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(suc(u)))*. % 1.31/1.50 85[0:MRR:52.0,16.0] || -> LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(suc(suc(u))))*. % 1.31/1.50 86[0:MRR:71.0,16.0] || -> LE(f(u),s(s(s(s(0))))) E(s(s(s(s(0)))),f(suc(suc(suc(u)))))*. % 1.31/1.50 87[0:MRR:69.2,5.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))))*. % 1.31/1.50 88[0:MRR:25.2,75.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 1.31/1.50 89[0:MRR:20.2,17.2] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 1.31/1.50 90[0:MRR:29.4,29.5,5.2,87.3] || 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))*. % 1.31/1.50 91[0:MRR:48.2,27.2] || E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 1.31/1.50 92[0:MRR:44.2,4.2] || E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(u))))*. % 1.31/1.50 93[0:MRR:3.0,3.4,75.2,88.3] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))*+ -> iLEQ(suc(u),suc(u))*. % 1.31/1.50 94[0:MRR:15.1,15.3,89.3,17.2] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))*+ -> iLEQ(suc(u),suc(u))*. % 1.31/1.50 95[0:MRR:2.6,24.5] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 96[0:MRR:74.0,24.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u))))+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 97[0:MRR:64.0,64.5,91.3,27.2] || E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u)))) E(s(s(s(0))),f(suc(suc(suc(u)))))*+ -> iLEQ(suc(u),suc(u))*. % 1.31/1.50 98[0:MRR:59.5,67.6] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u)))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(v))))*+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 99[0:MRR:73.1,67.5] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(v)))* E(s(0),f(suc(suc(u))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 100[0:MRR:18.2,18.4,92.3,4.2] || E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(suc(suc(u)))))*+ -> iLEQ(suc(u),suc(u))*. % 1.31/1.50 101[0:MRR:19.0,19.6,24.6,96.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))*. % 1.31/1.50 102[0:MRR:47.7,47.8,24.5,95.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))*. % 1.31/1.50 103[0:MRR:13.4,33.6] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))*+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 104[0:MRR:34.5,33.5] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(suc(u))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 105[0:MRR:11.6,39.5] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 106[0:MRR:31.1,31.7,67.5,99.6] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(v)))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(v)))*. % 1.31/1.50 107[0:MRR:40.0,40.8,95.7,96.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v))))+ E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 108[0:MRR:61.4,39.6] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(suc(suc(v))))*+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 109[0:MRR:63.6,63.8,67.6,98.7] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u)))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(u)))*. % 1.31/1.50 110[0:MRR:32.5,72.5] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v)))* E(s(s(s(s(0)))),f(suc(suc(u))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 111[0:MRR:62.6,72.6] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u)))* E(s(s(s(s(0)))),f(suc(v))) E(s(s(s(s(0)))),f(suc(suc(v))))*+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.31/1.50 112[0:MRR:35.1,35.7,98.6,99.7] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 113[0:MRR:53.3,53.6,103.7,33.6] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v)))) E(s(s(0)),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(u)))*. % 1.31/1.50 114[0:MRR:78.3,78.6,104.6,33.5] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(v)))*. % 1.31/1.50 115[0:MRR:42.0,42.9,42.10,102.7,96.6,107.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 116[0:MRR:80.0,80.7,80.10,95.7,107.8,101.7] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 117[0:MRR:22.5,22.6,108.7,39.6] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(suc(suc(v)))) E(s(s(s(0))),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(u)))*. % 1.31/1.50 118[0:MRR:54.1,54.8,105.6,39.5] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u)))) E(s(s(s(0))),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(v)))*. % 1.31/1.50 119[0:MRR:68.5,68.6,103.6,104.7] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))*+ E(s(s(0)),f(suc(suc(u))))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 120[0:MRR:37.1,37.8,37.9,98.6,112.7,106.7] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 121[0:MRR:38.1,38.8,38.10,109.7,99.7,112.8] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 122[0:MRR:12.5,12.8,111.7,72.6] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u)))* E(s(s(s(s(0)))),f(suc(v))) E(s(s(s(s(0)))),f(suc(suc(v)))) E(s(s(s(s(0)))),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(u)))*. % 1.31/1.50 123[0:MRR:21.4,21.8,105.7,108.6] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u))))*+ E(s(s(s(0))),f(suc(suc(v))))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 124[0:MRR:50.0,50.8,50.11,50.12,102.7,115.8,101.7,116.8] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* iLEQ(suc(v),suc(u))* -> . % 1.31/1.50 125[0:MRR:58.5,58.7,110.6,72.5] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v)))* E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(v)))*. % 1.31/1.50 126[0:MRR:1.3,1.6,1.8,119.7,103.6,114.7] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 127[0:MRR:66.3,66.6,66.8,119.8,113.7,104.7] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v)))) E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 128[0:MRR:51.6,51.8,111.6,110.7] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v))) E(s(s(s(s(0)))),f(suc(suc(u))))*+ E(s(s(s(s(0)))),f(suc(suc(v))))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.31/1.50 129[0:MRR:6.1,6.9,6.10,6.12,109.7,121.8,106.7,120.8] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))*+ E(s(0),f(suc(suc(suc(u)))))* -> . % 1.31/1.50 130[0:MRR:26.5,26.6,26.10,123.8,105.7,117.7] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u))))* E(s(s(s(0))),f(suc(suc(v)))) E(s(s(s(0))),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 131[0:MRR:46.1,46.6,46.10,123.7,118.7,108.6] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u)))) E(s(s(s(0))),f(suc(suc(v))))* E(s(s(s(0))),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 132[0:MRR:14.3,14.4,14.7,14.10,127.8,126.8,113.7,114.7] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v)))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(v)))))*+ E(s(s(0)),f(suc(suc(suc(u)))))* -> . % 1.31/1.50 133[0:MRR:8.6,8.7,8.10,122.7,128.8,110.7] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v))) E(s(s(s(s(0)))),f(suc(suc(u))))* E(s(s(s(s(0)))),f(suc(suc(v)))) E(s(s(s(s(0)))),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(suc(u))))*. % 1.31/1.50 134[0:MRR:49.6,49.8,49.10,128.7,111.6,125.7] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v))) E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(suc(v))))* E(s(s(s(s(0)))),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(suc(v))))*. % 1.31/1.50 135[0:MRR:57.1,57.7,57.8,57.12,130.8,131.8,118.7,117.7] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u)))) E(s(s(s(0))),f(suc(suc(v)))) E(s(s(s(0))),f(suc(suc(suc(v)))))*+ E(s(s(s(0))),f(suc(suc(suc(u)))))* -> . % 1.31/1.50 136[0:MRR:43.6,43.8,43.9,43.12,133.8,122.7,134.8,125.7] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v))) E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(suc(v)))) E(s(s(s(s(0)))),f(suc(suc(suc(v)))))*+ E(s(s(s(s(0)))),f(suc(suc(suc(u)))))* -> . % 1.31/1.50 177[0:Res:86.1,100.3] || E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(u))))* -> LE(f(u),s(s(s(s(0))))) iLEQ(suc(u),suc(u))*. % 1.31/1.50 178[0:MRR:177.0,177.1,177.2,83.1,84.1,85.1] || -> LE(f(u),s(s(s(s(0)))))* iLEQ(suc(u),suc(u))*. % 1.31/1.50 4091[0:Res:86.1,136.7] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(v)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(v))) E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(suc(v))))* E(s(s(s(s(0)))),f(suc(suc(suc(u)))))* -> LE(f(v),s(s(s(s(0))))). % 1.31/1.50 4092[0:MRR:4091.2,4091.4,4091.6,83.1,84.1,85.1] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(u)))) E(s(s(s(s(0)))),f(suc(suc(suc(u)))))*+ -> LE(f(v),s(s(s(s(0)))))*. % 1.31/1.50 5100[0:Res:86.1,4092.4] || iLEQ(suc(u),suc(v))* E(s(s(s(s(0)))),f(u)) E(s(s(s(s(0)))),f(suc(u))) E(s(s(s(s(0)))),f(suc(suc(u))))* -> LE(f(u),s(s(s(s(0))))) LE(f(v),s(s(s(s(0)))))*. % 1.31/1.50 5101[0:MRR:5100.1,5100.2,5100.3,83.1,84.1,85.1] || iLEQ(suc(u),suc(v))*+ -> LE(f(u),s(s(s(s(0)))))* LE(f(v),s(s(s(s(0)))))*. % 1.31/1.50 5105[0:Res:178.1,5101.0] || -> LE(f(u),s(s(s(s(0)))))* LE(f(u),s(s(s(s(0)))))* LE(f(u),s(s(s(s(0)))))*. % 1.31/1.50 5161[0:Obv:5105.1] || -> LE(f(u),s(s(s(s(0)))))*. % 1.31/1.50 5162[0:MRR:45.0,5161.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u))*. % 1.31/1.50 5163[0:MRR:60.0,5161.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(u)))*. % 1.31/1.50 5164[0:MRR:76.0,5161.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(suc(u))))*. % 1.31/1.50 5165[0:MRR:10.0,5161.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(suc(suc(u)))))*. % 1.31/1.50 5292[0:Res:5165.1,97.3] || E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u))))* -> LE(f(u),s(s(s(0)))) iLEQ(suc(u),suc(u))*. % 1.31/1.50 5293[0:Res:5165.1,135.7] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u)))) E(s(s(s(0))),f(suc(suc(v))))* E(s(s(s(0))),f(suc(suc(suc(u)))))* -> LE(f(v),s(s(s(0)))). % 1.31/1.50 5299[0:MRR:5292.0,5292.1,5292.2,5162.1,5163.1,5164.1] || -> LE(f(u),s(s(s(0))))* iLEQ(suc(u),suc(u))*. % 1.31/1.50 5309[0:MRR:5293.2,5293.3,5293.6,5162.1,5163.1,5164.1] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u)))) E(s(s(s(0))),f(suc(suc(suc(u)))))*+ -> LE(f(v),s(s(s(0))))*. % 1.31/1.50 6118[0:Res:5165.1,5309.4] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(u))))* -> LE(f(u),s(s(s(0)))) LE(f(v),s(s(s(0))))*. % 1.31/1.50 6119[0:MRR:6118.1,6118.2,6118.3,5162.1,5163.1,5164.1] || iLEQ(suc(u),suc(v))*+ -> LE(f(u),s(s(s(0))))* LE(f(v),s(s(s(0))))*. % 1.31/1.50 6123[0:Res:5299.1,6119.0] || -> LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 1.31/1.50 6149[0:Obv:6123.1] || -> LE(f(u),s(s(s(0))))*. % 1.31/1.50 6150[0:MRR:65.0,6149.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 1.31/1.50 6151[0:MRR:41.0,6149.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u)))*. % 1.31/1.50 6152[0:MRR:30.0,6149.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(u))))*. % 1.31/1.50 6153[0:MRR:36.0,6149.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(suc(u)))))*. % 1.31/1.50 6246[0:Res:6153.1,94.3] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u))))* -> LE(f(u),s(s(0))) iLEQ(suc(u),suc(u))*. % 1.31/1.50 6247[0:Res:6153.1,132.7] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))* -> LE(f(v),s(s(0))). % 1.31/1.50 6253[0:MRR:6246.0,6246.1,6246.2,6150.1,6151.1,6152.1] || -> LE(f(u),s(s(0)))* iLEQ(suc(u),suc(u))*. % 1.31/1.50 6263[0:MRR:6247.2,6247.4,6247.5,6150.1,6151.1,6152.1] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))*+ -> LE(f(v),s(s(0)))*. % 1.31/1.50 6964[0:Res:6153.1,6263.4] || iLEQ(suc(u),suc(v))* E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u))))* -> LE(f(u),s(s(0))) LE(f(v),s(s(0)))*. % 1.31/1.50 6965[0:MRR:6964.1,6964.2,6964.3,6150.1,6151.1,6152.1] || iLEQ(suc(u),suc(v))*+ -> LE(f(u),s(s(0)))* LE(f(v),s(s(0)))*. % 1.31/1.50 6969[0:Res:6253.1,6965.0] || -> LE(f(u),s(s(0)))* LE(f(u),s(s(0)))* LE(f(u),s(s(0)))*. % 1.31/1.50 6990[0:Obv:6969.1] || -> LE(f(u),s(s(0)))*. % 1.31/1.50 6991[0:MRR:81.0,6990.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 1.31/1.50 6992[0:MRR:7.0,6990.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 1.31/1.50 6993[0:MRR:70.0,6990.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 1.31/1.50 6994[0:MRR:9.0,6990.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u)))))*. % 1.31/1.50 7083[0:Res:6994.1,93.3] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))* -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 1.31/1.50 7084[0:Res:6994.1,129.7] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(suc(u)))))* -> LE(f(v),s(0)). % 1.31/1.50 7088[0:MRR:7083.0,7083.1,7083.2,6991.1,6992.1,6993.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 1.31/1.50 7098[0:MRR:7084.2,7084.4,7084.6,6991.1,6992.1,6993.1] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))*+ -> LE(f(v),s(0)). % 1.31/1.50 7746[0:Res:6994.1,7098.4] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))* -> LE(f(u),s(0)) LE(f(v),s(0)). % 1.31/1.50 7747[0:MRR:7746.1,7746.2,7746.3,6991.1,6992.1,6993.1] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(0)) LE(f(v),s(0)). % 1.31/1.50 7750[0:Res:7088.1,7747.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 1.31/1.50 7768[0:Obv:7750.1] || -> LE(f(u),s(0))*. % 1.31/1.50 7769[0:MRR:56.0,7768.0] || -> E(0,f(u))* LE(f(u),0). % 1.31/1.50 7770[0:MRR:82.0,7768.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 1.31/1.50 7771[0:MRR:55.0,7768.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 1.31/1.50 7772[0:MRR:28.0,7768.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 1.31/1.50 7842[0:Res:7772.0,124.6] || E(0,f(u)) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u))))* E(0,f(suc(suc(suc(v)))))* iLEQ(suc(v),suc(u))* -> LE(f(u),0). % 1.31/1.50 7845[0:Res:7772.0,90.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))*. % 1.31/1.50 7850[0:MRR:7845.0,7845.1,7845.2,7769.0,7770.0,7771.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 1.31/1.50 7858[0:MRR:7842.0,7842.2,7842.5,7769.0,7770.0,7771.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(u),suc(v))* -> LE(f(v),0). % 1.31/1.50 8037[0:Res:7772.0,7858.3] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))* iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0). % 1.31/1.50 8038[0:MRR:8037.0,8037.1,8037.2,7769.0,7770.0,7771.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0). % 1.31/1.50 8042[0:Res:7850.1,8038.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 1.31/1.50 8046[0:Obv:8042.1] || -> LE(f(u),0)*. % 1.31/1.50 8047[0:UnC:8046.0,77.0] || -> . % 1.31/1.50 % SZS output end Refutation % 1.31/1.50 Formulae used in the proof : clause_91 clause_465 clause_322 clause_380 clause_59 clause_340 clause_92 clause_15 clause_313 clause_327 clause_511 clause_493 clause_191 clause_226 clause_575 clause_159 clause_432 clause_614 clause_600 clause_638 clause_308 clause_489 clause_569 clause_494 clause_354 clause_328 clause_86 clause_478 clause_643 clause_300 clause_5 clause_181 clause_355 clause_102 clause_558 clause_232 clause_414 clause_310 clause_139 clause_431 clause_263 clause_518 clause_93 clause_267 clause_294 clause_456 clause_579 clause_57 clause_342 clause_250 clause_425 clause_282 clause_615 clause_235 clause_41 clause_503 clause_149 clause_64 clause_610 clause_335 clause_297 clause_642 clause_444 clause_323 clause_368 clause_567 clause_264 clause_550 clause_573 clause_356 clause_603 clause_105 clause_374 clause_384 clause_601 clause_158 clause_295 clause_98 clause_345 clause_216 clause_534 clause_486 % 1.78/1.97 %------------------------------------------------------------------------------