%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO681-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n003.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:30 EDT 2022 % Result : Unsatisfiable 0.77s 0.92s % Output : Refutation 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYO681-1 : TPTP v8.1.0. Released v7.3.0. % 0.12/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n003.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jul 9 01:08:28 EDT 2022 % 0.13/0.34 % CPUTime : % 0.77/0.92 % 0.77/0.92 SPASS V 3.9 % 0.77/0.92 SPASS beiseite: Proof found. % 0.77/0.92 % SZS status Theorem % 0.77/0.92 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.77/0.92 SPASS derived 1477 clauses, backtracked 0 clauses, performed 0 splits and kept 447 clauses. % 0.77/0.92 SPASS allocated 65140 KBytes. % 0.77/0.92 SPASS spent 0:00:00.58 on the problem. % 0.77/0.92 0:00:00.04 for the input. % 0.77/0.92 0:00:00.00 for the FLOTTER CNF translation. % 0.77/0.92 0:00:00.08 for inferences. % 0.77/0.92 0:00:00.00 for the backtracking. % 0.77/0.92 0:00:00.41 for the reduction. % 0.77/0.92 % 0.77/0.92 % 0.77/0.92 Here is a proof with depth 5, length 147 : % 0.77/0.92 % SZS output start Refutation % 0.77/0.92 1[0:Inp] || LE(f(u),s(s(s(s(0)))))* -> E(s(s(s(0))),f(u)) LE(f(u),s(s(s(0)))). % 0.77/0.92 2[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(w))) iLEQ(suc(w),suc(u))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(u))))* E(f(u),f(suc(u)))* E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(u)) -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 0.77/0.92 3[0:Inp] || -> LE(f(u),s(s(s(s(0)))))*. % 0.77/0.92 4[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(suc(u))))* E(s(s(s(0))),f(v)) E(f(u),f(suc(u)))* E(s(s(s(0))),f(u)) iLEQ(suc(w),suc(u))* E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(w)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 0.77/0.92 5[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(w))) E(f(v),f(suc(v)))* iLEQ(suc(w),suc(u))* E(s(0),f(suc(v))) E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u))) E(s(0),f(u)) -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 6[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(u)) iLEQ(suc(w),suc(u))* E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(suc(w))))* E(f(w),f(suc(w)))* E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(w))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 0.77/0.92 7[0:Inp] || LE(f(u),s(s(s(0))))* -> LE(f(u),s(s(0))) E(s(s(0)),f(u)). % 0.77/0.92 8[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)) -> iLEQ(suc(u),suc(u)). % 0.77/0.92 9[0:Inp] || 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))) iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 10[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)))). % 0.77/0.92 11[0:Inp] || E(0,f(suc(u))) iLEQ(suc(u),suc(v))* E(f(w),f(suc(w)))* iLEQ(suc(w),suc(u))* E(0,f(suc(v))) E(0,f(suc(suc(w)))) E(0,f(u)) E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(u)))) E(f(u),f(suc(u)))* E(0,f(w)) -> E(f(v),f(suc(v)))*. % 0.77/0.92 12[0:Inp] || E(s(s(0)),f(suc(u))) E(s(s(0)),f(u)) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(v)))* iLEQ(suc(w),suc(u))* E(s(s(0)),f(v)) E(f(u),f(suc(u)))* E(s(s(0)),f(w)) -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 0.77/0.92 13[0:Inp] || E(0,f(suc(u))) iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* E(0,f(suc(v))) E(f(v),f(suc(v)))* E(0,f(u)) E(0,f(suc(suc(v)))) E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(u)))) E(f(u),f(suc(u)))* E(0,f(w)) -> E(f(w),f(suc(w)))*. % 0.77/0.92 14[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u)))*+ E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.77/0.92 15[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v)))+ E(s(0),f(suc(w))) E(s(0),f(suc(u))) -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.77/0.92 16[0:Inp] || E(s(s(0)),f(suc(u))) E(f(v),f(suc(v)))* E(s(s(0)),f(u)) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(w))) E(s(s(0)),f(suc(v))) iLEQ(suc(w),suc(u))* E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(w))))* E(f(u),f(suc(u)))* E(s(s(0)),f(w)) E(f(w),f(suc(w)))* -> . % 0.77/0.92 17[0:Inp] || LE(f(z__dfg),0)* -> . % 0.77/0.92 18[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 0.77/0.92 19[0:Inp] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w)))*+ E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(v)))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.77/0.92 20[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(u)) iLEQ(suc(w),suc(u))* E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(suc(w))))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(suc(suc(v))))* E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(w))) -> E(f(u),f(suc(u)))*. % 0.77/0.92 21[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(w))) iLEQ(suc(w),suc(u))* E(s(0),f(suc(v))) E(f(w),f(suc(w)))* E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(w))))* E(s(0),f(u)) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 0.77/0.92 22[0:Inp] || LE(f(suc(u)),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(u))). % 0.77/0.92 23[0:Inp] || E(s(s(0)),f(suc(u))) E(f(v),f(suc(v)))* E(s(s(0)),f(u)) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(v))) iLEQ(suc(w),suc(u))* E(s(s(0)),f(v)) E(f(u),f(suc(u)))* E(s(s(0)),f(w)) -> E(f(w),f(suc(w)))*. % 0.77/0.92 24[0:Inp] || E(s(0),f(suc(suc(u))))* E(s(0),f(suc(u))) E(f(u),f(suc(u)))* E(s(0),f(u)) -> iLEQ(suc(u),suc(u)). % 0.77/0.92 25[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 0.77/0.92 26[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 0.77/0.92 27[0:Inp] || E(0,f(suc(suc(u)))) E(0,f(suc(u))) E(f(u),f(suc(u)))* E(0,f(u)) -> iLEQ(suc(u),suc(u)). % 0.77/0.92 28[0:Inp] || LE(f(suc(suc(u))),s(s(s(s(0)))))* -> E(s(s(s(0))),f(suc(suc(u)))) LE(f(u),s(s(s(0)))). % 0.77/0.92 29[0:Inp] || E(s(0),f(u)) E(s(0),f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 0.77/0.92 30[0:Inp] || E(0,f(suc(u))) iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* E(0,f(suc(v))) E(f(v),f(suc(v)))* E(0,f(u)) E(0,f(suc(suc(v)))) E(0,f(suc(w))) E(0,f(v)) E(0,f(w)) -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 31[0:Inp] || E(s(s(0)),f(suc(u)))* E(f(v),f(suc(v)))* E(s(s(0)),f(u)) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(v))) iLEQ(suc(w),suc(u))* E(s(s(0)),f(v)) E(s(s(0)),f(w)) -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 32[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)))*. % 0.77/0.92 33[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(suc(u))))* E(s(s(s(0))),f(v)) E(f(u),f(suc(u)))* E(s(s(s(0))),f(u)) iLEQ(suc(w),suc(u))* E(s(s(s(0))),f(w)) E(f(v),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(v))) E(s(s(s(0))),f(suc(w)))* -> E(f(w),f(suc(w)))*. % 0.77/0.92 34[0:Inp] || LE(f(suc(u)),s(s(s(0))))* -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u))). % 0.77/0.92 35[0:Inp] || E(s(s(0)),f(suc(u)))* E(f(v),f(suc(v)))* E(s(s(0)),f(u)) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(v))))* E(s(s(0)),f(suc(w))) E(s(s(0)),f(suc(v))) iLEQ(suc(w),suc(u))* E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(w))))* E(s(s(0)),f(w)) E(f(w),f(suc(w)))* -> E(f(u),f(suc(u)))*. % 0.77/0.92 36[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)) -> iLEQ(suc(u),suc(u)). % 0.77/0.92 37[0:Inp] || E(0,f(suc(u))) iLEQ(suc(u),suc(v))* E(f(w),f(suc(w)))* iLEQ(suc(w),suc(u))* E(0,f(suc(v))) E(0,f(suc(suc(w)))) E(f(v),f(suc(v)))* E(0,f(u)) E(0,f(suc(suc(v)))) E(0,f(suc(w))) E(0,f(v)) E(0,f(w)) -> E(f(u),f(suc(u)))*. % 0.77/0.92 38[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(suc(u))))* E(s(s(s(0))),f(v)) E(f(u),f(suc(u)))* E(s(s(s(0))),f(u)) iLEQ(suc(w),suc(u))* E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(suc(w))))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(suc(v))))* E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(w))) -> . % 0.77/0.92 39[0:Inp] || E(0,f(suc(u))) iLEQ(suc(u),suc(v))* iLEQ(suc(w),suc(u))* E(0,f(suc(v))) E(0,f(u)) E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(u)))) E(f(u),f(suc(u)))* E(0,f(w)) -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 0.77/0.92 40[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(w))) E(f(v),f(suc(v)))* iLEQ(suc(w),suc(u))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(u))))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(w))))* E(s(0),f(u)) -> . % 0.77/0.92 41[0:Inp] || E(0,f(suc(u))) iLEQ(suc(u),suc(v))* E(f(w),f(suc(w)))* iLEQ(suc(w),suc(u))* E(0,f(suc(v))) E(0,f(suc(suc(w)))) E(0,f(u)) E(0,f(suc(w))) E(0,f(v)) E(0,f(w)) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 0.77/0.92 42[0:Inp] || LE(f(u),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(u)). % 0.77/0.92 43[0:Inp] || LE(f(suc(u)),s(s(s(s(0)))))* -> E(s(s(s(0))),f(suc(u))) LE(f(u),s(s(s(0)))). % 0.77/0.92 44[0:Inp] || E(s(s(0)),f(suc(u))) E(s(s(0)),f(u)) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(suc(u))))* E(s(s(0)),f(suc(w))) E(s(s(0)),f(suc(v)))* iLEQ(suc(w),suc(u))* E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(w))))* E(f(u),f(suc(u)))* E(s(s(0)),f(w)) E(f(w),f(suc(w)))* -> E(f(v),f(suc(v)))*. % 0.77/0.92 45[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(suc(suc(u))))* E(s(s(s(0))),f(v)) E(f(u),f(suc(u)))* E(s(s(s(0))),f(u)) iLEQ(suc(w),suc(u))* E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(suc(w))))* E(f(w),f(suc(w)))* E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(w))) -> E(f(v),f(suc(v)))*. % 0.77/0.92 46[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)))*. % 0.77/0.92 47[0:Inp] || iLEQ(suc(u),suc(v))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(u)) iLEQ(suc(w),suc(u))* E(s(s(s(0))),f(w)) E(f(v),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(v))) E(s(s(s(0))),f(suc(w)))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 48[0:Inp] || E(s(s(0)),f(suc(u)))* E(s(s(0)),f(u)) iLEQ(suc(u),suc(v))* E(s(s(0)),f(suc(w))) E(s(s(0)),f(suc(v)))* iLEQ(suc(w),suc(u))* E(s(s(0)),f(v)) E(s(s(0)),f(suc(suc(w))))* E(s(s(0)),f(w)) E(f(w),f(suc(w)))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 0.77/0.92 49[0:Inp] || E(0,f(suc(u))) iLEQ(suc(u),suc(v))* E(f(w),f(suc(w)))* iLEQ(suc(w),suc(u))* E(0,f(suc(v))) E(0,f(suc(suc(w)))) E(f(v),f(suc(v)))* E(0,f(u)) E(0,f(suc(suc(v)))) E(0,f(suc(w))) E(0,f(v)) E(0,f(suc(suc(u)))) E(f(u),f(suc(u)))* E(0,f(w)) -> . % 0.77/0.92 50[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(w))) E(f(v),f(suc(v)))* iLEQ(suc(w),suc(u))* E(s(0),f(suc(v))) E(f(w),f(suc(w)))* E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(w))))* E(s(0),f(u)) -> E(f(u),f(suc(u)))*. % 0.77/0.92 51[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 0.77/0.92 52[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(suc(u)))). % 0.77/0.92 53[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(w))) iLEQ(suc(w),suc(u))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(u))))* E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(w))))* E(s(0),f(u)) -> E(f(v),f(suc(v)))*. % 0.77/0.92 54[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(w))) E(f(v),f(suc(v)))* iLEQ(suc(w),suc(u))* E(s(0),f(suc(v))) E(s(0),f(suc(suc(u))))* E(f(u),f(suc(u)))* E(s(0),f(w)) E(s(0),f(v)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u))) E(s(0),f(u)) -> E(f(w),f(suc(w)))*. % 0.77/0.92 55[0:MRR:1.0,3.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(u))*. % 0.77/0.92 56[0:MRR:43.0,3.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(u)))*. % 0.77/0.92 57[0:MRR:28.0,3.0] || -> LE(f(u),s(s(s(0)))) E(s(s(s(0))),f(suc(suc(u))))*. % 0.77/0.92 58[0:MRR:27.2,26.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u))*. % 0.77/0.92 59[0:MRR:24.2,29.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ -> iLEQ(suc(u),suc(u))*. % 0.77/0.92 60[0:MRR:8.2,46.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))*. % 0.77/0.92 61[0:MRR:36.2,32.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))*. % 0.77/0.92 62[0:MRR:30.4,9.10] || 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(v))))*+ iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 63[0:MRR:39.8,9.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(w))))*+ iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.77/0.92 64[0:MRR:41.2,9.8] || 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))))*+ iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 0.77/0.92 65[0:MRR:2.5,15.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v))))*+ -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 66[0:MRR:5.2,15.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(w))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.77/0.92 67[0:MRR:21.4,15.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 0.77/0.92 68[0:MRR:11.2,11.10,63.9,64.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(w))))*+ E(0,f(suc(suc(u))))* iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))*. % 0.77/0.92 69[0:MRR:13.4,13.10,63.10,62.10] || 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(w))))*+ E(0,f(suc(suc(v))))* iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))*. % 0.77/0.92 70[0:MRR:37.2,37.6,62.9,64.10] || 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(v))))*+ E(0,f(suc(suc(u))))* iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))*. % 0.77/0.92 71[0:MRR:12.8,19.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))*+ -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 72[0:MRR:31.1,19.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w))) E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(suc(w))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.77/0.92 73[0:MRR:48.9,19.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(v)))* E(s(s(0)),f(suc(suc(u))))*+ -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 0.77/0.92 74[0:MRR:49.2,49.6,49.12,69.10,68.10,70.10] || 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(w))))*+ E(0,f(suc(suc(v))))* E(0,f(suc(suc(u))))* iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> . % 0.77/0.92 75[0:MRR:50.2,50.5,67.10,66.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(w))))* -> E(f(v),f(suc(v)))*. % 0.77/0.92 76[0:MRR:53.5,53.6,67.9,65.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(v))))* -> E(f(w),f(suc(w)))*. % 0.77/0.92 77[0:MRR:54.2,54.6,65.10,66.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(w))))*+ E(s(0),f(suc(suc(v))))* -> E(f(u),f(suc(u)))*. % 0.77/0.92 78[0:MRR:4.3,14.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v))))*+ -> E(f(w),f(suc(w)))* E(f(u),f(suc(u)))*. % 0.77/0.92 79[0:MRR:6.6,14.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(suc(u))))*+ -> E(f(w),f(suc(w)))* E(f(v),f(suc(v)))*. % 0.77/0.92 80[0:MRR:47.5,14.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(suc(w))) E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(suc(w))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 0.77/0.92 81[0:MRR:23.1,23.10,71.10,72.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w))) E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(w))))*+ E(s(s(0)),f(suc(suc(v))))* -> E(f(u),f(suc(u)))*. % 0.77/0.92 82[0:MRR:35.1,35.11,73.10,72.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w))) 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(w))))* -> E(f(v),f(suc(v)))*. % 0.77/0.92 83[0:MRR:44.9,44.11,73.9,71.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w)))* 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(v))))* -> E(f(w),f(suc(w)))*. % 0.77/0.92 84[0:MRR:40.2,40.6,40.7,76.10,75.10,77.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(v))))* -> . % 0.77/0.92 85[0:MRR:20.6,20.7,79.10,80.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(w))) E(s(s(s(0))),f(suc(v)))* E(s(s(s(0))),f(suc(suc(w))))*+ E(s(s(s(0))),f(suc(suc(u))))* -> E(f(v),f(suc(v)))*. % 0.77/0.92 86[0:MRR:33.3,33.7,80.10,78.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(suc(w))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(w))))*+ E(s(s(s(0))),f(suc(suc(v))))* -> E(f(u),f(suc(u)))*. % 0.77/0.92 87[0:MRR:45.3,45.8,79.9,78.9] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(u))))*+ E(s(s(s(0))),f(suc(suc(v))))* -> E(f(w),f(suc(w)))*. % 0.77/0.92 88[0:MRR:16.1,16.11,16.13,83.10,82.10,81.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w))) 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(w))))* E(s(s(0)),f(suc(suc(v))))* -> . % 0.77/0.92 89[0:MRR:38.3,38.8,38.9,85.10,87.10,86.10] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(w))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(w))))*+ E(s(s(s(0))),f(suc(suc(u))))* E(s(s(s(0))),f(suc(suc(v))))* -> . % 0.77/0.92 101[0:Res:57.1,61.2] || E(s(s(s(0))),f(u)) E(s(s(s(0))),f(suc(u)))* -> LE(f(u),s(s(s(0)))) iLEQ(suc(u),suc(u))*. % 0.77/0.92 102[0:MRR:101.0,101.1,55.1,56.1] || -> LE(f(u),s(s(s(0))))* iLEQ(suc(u),suc(u))*. % 0.77/0.92 897[0:Res:57.1,89.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(w)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(w)))* E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(u))))* E(s(s(s(0))),f(suc(suc(v))))* -> LE(f(w),s(s(s(0)))). % 0.77/0.92 898[0:MRR:897.4,897.6,55.1,56.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(u))) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(u))))*+ E(s(s(s(0))),f(suc(suc(v))))* -> LE(f(w),s(s(s(0))))*. % 0.77/0.92 1413[0:Res:57.1,898.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(u)) E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(u)))* E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v))))* -> LE(f(u),s(s(s(0)))) LE(f(w),s(s(s(0))))*. % 0.77/0.92 1414[0:MRR:1413.2,1413.4,55.1,56.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v))) E(s(s(s(0))),f(suc(suc(v))))*+ -> LE(f(u),s(s(s(0))))* LE(f(w),s(s(s(0))))*. % 0.77/0.92 1531[0:Res:57.1,1414.4] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(s(0))),f(v)) E(s(s(s(0))),f(suc(v)))* -> LE(f(v),s(s(s(0)))) LE(f(u),s(s(s(0))))* LE(f(w),s(s(s(0))))*. % 0.77/0.92 1532[0:MRR:1531.2,1531.3,55.1,56.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(v),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(w),s(s(s(0))))*. % 0.77/0.92 1535[0:Res:102.1,1532.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(v),s(s(s(0))))*. % 0.77/0.92 1554[0:Obv:1535.2] || iLEQ(suc(u),suc(v))*+ -> LE(f(u),s(s(s(0))))* LE(f(v),s(s(s(0))))*. % 0.77/0.92 1575[0:Res:102.1,1554.0] || -> LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))* LE(f(u),s(s(s(0))))*. % 0.77/0.92 1594[0:Obv:1575.1] || -> LE(f(u),s(s(s(0))))*. % 0.77/0.92 1595[0:MRR:7.0,1594.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 0.77/0.92 1596[0:MRR:34.0,1594.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u)))*. % 0.77/0.92 1597[0:MRR:10.0,1594.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(u))))*. % 0.77/0.92 1648[0:Res:1597.1,88.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(u)) E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w))) E(s(s(0)),f(suc(u)))* E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(w))))* E(s(s(0)),f(suc(suc(v))))* -> LE(f(u),s(s(0))). % 0.77/0.92 1652[0:Res:1597.1,60.2] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))* -> LE(f(u),s(s(0))) iLEQ(suc(u),suc(u))*. % 0.77/0.92 1657[0:MRR:1652.0,1652.1,1595.1,1596.1] || -> LE(f(u),s(s(0)))* iLEQ(suc(u),suc(u))*. % 0.77/0.92 1666[0:MRR:1648.2,1648.6,1595.1,1596.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w))) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(w))))*+ E(s(s(0)),f(suc(suc(v))))* -> LE(f(u),s(s(0)))*. % 0.77/0.92 1963[0:Res:1597.1,1666.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(w)) E(s(s(0)),f(v)) E(s(s(0)),f(suc(w)))* E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))* -> LE(f(w),s(s(0))) LE(f(u),s(s(0)))*. % 0.77/0.92 1964[0:MRR:1963.2,1963.4,1595.1,1596.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(v)) E(s(s(0)),f(suc(v))) E(s(s(0)),f(suc(suc(v))))*+ -> LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.77/0.92 1968[0:Res:1597.1,1964.4] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(s(0)),f(v)) E(s(s(0)),f(suc(v)))* -> LE(f(v),s(s(0))) LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.77/0.92 1969[0:MRR:1968.2,1968.3,1595.1,1596.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(v),s(s(0)))* LE(f(w),s(s(0)))* LE(f(u),s(s(0)))*. % 0.77/0.92 1972[0:Res:1657.1,1969.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(s(0)))* LE(f(u),s(s(0)))* LE(f(v),s(s(0)))* LE(f(u),s(s(0)))*. % 0.77/0.92 1982[0:Obv:1972.2] || iLEQ(suc(u),suc(v))*+ -> LE(f(v),s(s(0)))* LE(f(u),s(s(0)))*. % 0.77/0.92 1994[0:Res:1657.1,1982.0] || -> LE(f(u),s(s(0)))* LE(f(u),s(s(0)))* LE(f(u),s(s(0)))*. % 0.77/0.92 2004[0:Obv:1994.1] || -> LE(f(u),s(s(0)))*. % 0.77/0.92 2005[0:MRR:42.0,2004.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 0.77/0.92 2006[0:MRR:22.0,2004.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 0.77/0.92 2007[0:MRR:52.0,2004.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 0.77/0.92 2045[0:Res:2007.1,84.8] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(u)))* E(s(0),f(suc(suc(w))))* E(s(0),f(suc(suc(v))))* -> LE(f(u),s(0)). % 0.77/0.92 2049[0:Res:2007.1,59.2] || E(s(0),f(u)) E(s(0),f(suc(u)))* -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.77/0.92 2054[0:MRR:2049.0,2049.1,2005.1,2006.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.77/0.92 2062[0:MRR:2045.4,2045.7,2005.1,2006.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(w))) E(s(0),f(suc(suc(w))))*+ E(s(0),f(suc(suc(v))))* -> LE(f(u),s(0)). % 0.77/0.92 2334[0:Res:2007.1,2062.6] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(w)) E(s(0),f(suc(v))) E(s(0),f(suc(w)))* E(s(0),f(suc(suc(v))))* -> LE(f(w),s(0)) LE(f(u),s(0)). % 0.77/0.92 2335[0:MRR:2334.3,2334.5,2005.1,2006.1] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v))))*+ -> LE(f(w),s(0)) LE(f(u),s(0)). % 0.77/0.92 2339[0:Res:2007.1,2335.4] || iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* E(s(0),f(v)) E(s(0),f(suc(v)))* -> LE(f(v),s(0)) LE(f(w),s(0)) LE(f(u),s(0)). % 0.77/0.92 2340[0:MRR:2339.2,2339.3,2005.1,2006.1] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(v),s(0)) LE(f(w),s(0)) LE(f(u),s(0)). % 0.77/0.92 2342[0:Res:2054.1,2340.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),s(0)) LE(f(u),s(0)) LE(f(v),s(0)) LE(f(u),s(0)). % 0.77/0.92 2349[0:Obv:2342.2] || iLEQ(suc(u),suc(v))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 0.77/0.92 2356[0:Res:2054.1,2349.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 0.77/0.92 2363[0:Obv:2356.1] || -> LE(f(u),s(0))*. % 0.77/0.92 2364[0:MRR:18.0,2363.0] || -> E(0,f(u))* LE(f(u),0). % 0.77/0.92 2365[0:MRR:51.0,2363.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 0.77/0.92 2366[0:MRR:25.0,2363.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 0.77/0.92 2402[0:Res:2366.0,58.2] || E(0,f(u)) E(0,f(suc(u))) -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 0.77/0.92 2405[0:Res:2366.0,74.6] || 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(v))))* E(0,f(suc(suc(u))))* iLEQ(suc(u),suc(w))* iLEQ(suc(w),suc(v))* -> LE(f(w),0). % 0.77/0.92 2409[0:MRR:2402.0,2402.1,2364.0,2365.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 0.77/0.92 2416[0:MRR:2405.2,2405.5,2364.0,2365.0] || 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(u),suc(w))* iLEQ(suc(w),suc(v))* -> LE(f(w),0). % 0.77/0.92 2565[0:Res:2366.0,2416.4] || 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(u),suc(w))* iLEQ(suc(w),suc(v))* -> LE(f(v),0) LE(f(w),0). % 0.77/0.99 2566[0:MRR:2565.1,2565.3,2364.0,2365.0] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))*+ iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(w),0) LE(f(v),0). % 0.77/0.99 2570[0:Res:2366.0,2566.2] || E(0,f(u)) E(0,f(suc(u))) iLEQ(suc(u),suc(v))* iLEQ(suc(v),suc(w))* -> LE(f(u),0) LE(f(w),0) LE(f(v),0). % 0.77/0.99 2571[0:MRR:2570.0,2570.1,2364.0,2365.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(v),suc(w))* -> LE(f(u),0) LE(f(w),0) LE(f(v),0). % 0.77/0.99 2574[0:Res:2409.1,2571.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(u),0) LE(f(v),0) LE(f(u),0). % 0.77/0.99 2576[0:Obv:2574.2] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 0.77/0.99 2580[0:Res:2409.1,2576.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 0.77/0.99 2582[0:Obv:2580.1] || -> LE(f(u),0)*. % 0.77/0.99 2583[0:UnC:2582.0,17.0] || -> . % 0.77/0.99 % SZS output end Refutation % 0.77/0.99 Formulae used in the proof : clause_658 clause_592 clause_556 clause_227 clause_80 clause_330 clause_300 clause_415 clause_614 clause_607 clause_479 clause_723 clause_209 clause_486 clause_687 clause_528 clause_359 clause_497 clause_463 clause_534 clause_228 clause_95 clause_352 clause_125 clause_61 clause_713 clause_560 clause_103 clause_563 clause_450 clause_501 clause_283 clause_137 clause_457 clause_515 clause_663 clause_572 clause_131 clause_458 clause_41 clause_223 clause_44 clause_550 clause_325 clause_291 clause_383 clause_473 clause_594 clause_363 clause_145 clause_595 clause_508 clause_671 clause_35 % 0.77/0.99 %------------------------------------------------------------------------------