%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO659-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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:23 EDT 2022 % Result : Unsatisfiable 1.28s 1.51s % Output : Refutation 1.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYO659-1 : TPTP v8.1.0. Released v7.3.0. % 0.12/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n026.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sat Jul 9 03:31:40 EDT 2022 % 0.14/0.34 % CPUTime : % 1.28/1.51 % 1.28/1.51 SPASS V 3.9 % 1.28/1.51 SPASS beiseite: Proof found. % 1.28/1.51 % SZS status Theorem % 1.28/1.51 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.28/1.51 SPASS derived 3285 clauses, backtracked 0 clauses, performed 0 splits and kept 773 clauses. % 1.28/1.51 SPASS allocated 66863 KBytes. % 1.28/1.51 SPASS spent 0:00:01.16 on the problem. % 1.28/1.51 0:00:00.04 for the input. % 1.28/1.51 0:00:00.00 for the FLOTTER CNF translation. % 1.28/1.51 0:00:00.11 for inferences. % 1.28/1.51 0:00:00.00 for the backtracking. % 1.28/1.51 0:00:00.97 for the reduction. % 1.28/1.51 % 1.28/1.51 % 1.28/1.51 Here is a proof with depth 3, length 115 : % 1.28/1.51 % SZS output start Refutation % 1.28/1.51 1[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u)))))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 2[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.28/1.51 3[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 1.28/1.51 4[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> E(s(0),f(suc(suc(u)))) LE(f(u),s(0)). % 1.28/1.51 5[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(u))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 1.28/1.51 6[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v)))))* E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(u)))*. % 1.28/1.51 7[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.28/1.51 8[0:Inp] || E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(u))) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u)))))* -> E(f(u),f(suc(suc(suc(u)))))* iLEQ(suc(u),suc(u)). % 1.28/1.51 9[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(suc(suc(v))))))* E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u)))* E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(v),f(suc(suc(suc(v)))))* E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(u)))*. % 1.28/1.51 10[0:Inp] || LE(f(u),s(s(0)))* -> E(s(0),f(u)) LE(f(u),s(0)). % 1.28/1.51 11[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))*. % 1.28/1.51 12[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(s(0)))* -> E(s(0),f(suc(suc(suc(suc(u)))))) LE(f(u),s(0)). % 1.28/1.51 13[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v)))*+ E(s(0),f(suc(u)))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(u)))*. % 1.28/1.51 14[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u)))))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(v))))*. % 1.28/1.51 15[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 16[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v)))))* E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))*. % 1.28/1.51 17[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))*. % 1.28/1.51 18[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(u))) -> iLEQ(suc(u),suc(u)). % 1.28/1.51 19[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 1.28/1.51 20[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 1.28/1.51 21[0:Inp] || LE(f(z__dfg),0)* -> . % 1.28/1.51 22[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 23[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.28/1.51 24[0:Inp] || -> LE(f(u),s(s(0)))*. % 1.28/1.51 25[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(f(u),f(suc(suc(suc(u)))))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(v)))* E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> E(f(v),f(suc(v)))*. % 1.28/1.51 26[0:Inp] || E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(f(u),f(suc(suc(suc(u)))))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> iLEQ(suc(u),suc(u)). % 1.28/1.51 27[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 28[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u))))) -> E(f(v),f(suc(suc(v))))*. % 1.28/1.51 29[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 30[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u))))* E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(v)))* E(s(0),f(v)) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 1.28/1.51 31[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(v)))* E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(s(0),f(suc(suc(suc(u)))))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))*. % 1.28/1.51 32[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u))))* E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 33[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.28/1.51 34[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u))))* E(s(0),f(u)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 1.28/1.51 35[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(u)))))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> . % 1.28/1.51 36[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 1.28/1.51 37[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(v),f(suc(suc(v)))) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 38[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(0)))* -> E(s(0),f(suc(suc(suc(u))))) LE(f(u),s(0)). % 1.28/1.51 39[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(0))* -> E(0,f(suc(suc(suc(suc(u)))))) LE(f(u),0). % 1.28/1.51 40[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v))))))* E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(f(u),f(suc(suc(suc(u)))))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u))))))* E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v)))))* E(s(0),f(suc(suc(suc(u))))) E(f(v),f(suc(suc(v)))) -> . % 1.28/1.51 41[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 1.28/1.51 42[0:Inp] || LE(f(suc(u)),s(s(0)))* -> E(s(0),f(suc(u))) LE(f(u),s(0)). % 1.28/1.51 43[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(suc(u)))))* iLEQ(suc(u),suc(u)). % 1.28/1.51 44[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(v))))*. % 1.28/1.51 45[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(suc(suc(v))))))* E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v)))))* E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(u))))*. % 1.28/1.51 46[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(u)))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.28/1.51 47[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(0,f(suc(v))) -> E(f(v),f(suc(v)))*. % 1.28/1.51 48[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.28/1.51 49[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(suc(v))))))* E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(v))) E(s(0),f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(suc(v)))))* E(s(0),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(u)))))*. % 1.28/1.51 50[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(u)))) E(f(u),f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(u),suc(v))* E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(suc(u))))) E(0,f(v)) E(f(u),f(suc(u))) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))*. % 1.28/1.51 51[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 1.28/1.51 52[0:Inp] || iLEQ(suc(u),suc(v))* E(s(0),f(u)) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(u)))* E(s(0),f(suc(suc(suc(v)))))* E(s(0),f(suc(v))) E(s(0),f(v)) E(f(v),f(suc(v))) E(f(v),f(suc(suc(v)))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 53[0:MRR:10.0,24.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 1.28/1.51 54[0:MRR:42.0,24.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 1.28/1.51 55[0:MRR:4.0,24.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 1.28/1.51 56[0:MRR:38.0,24.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u)))))*. % 1.28/1.51 57[0:MRR:12.0,24.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(suc(u))))))*. % 1.28/1.51 58[0:MRR:7.2,41.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.28/1.51 59[0:MRR:23.2,2.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.28/1.51 60[0:MRR:43.2,43.5,58.3,41.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(suc(suc(u)))))*. % 1.28/1.51 61[0:MRR:5.5,33.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.28/1.51 62[0:MRR:48.5,33.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.28/1.51 63[0:MRR:8.3,8.4,59.3,2.2] || 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)) E(f(u),f(suc(suc(suc(u)))))*. % 1.28/1.51 64[0:MRR:30.6,13.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v)))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.28/1.51 65[0:MRR:46.6,13.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u)))* E(s(0),f(suc(suc(v))))*+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.28/1.51 66[0:MRR:18.2,18.5,18.7,58.3,60.4,41.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))*+ -> iLEQ(suc(u),suc(u))*. % 1.28/1.51 67[0:MRR:26.2,26.5,26.6,63.4,59.3,2.2] || 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))))) E(s(0),f(suc(suc(suc(suc(u))))))*+ -> iLEQ(suc(u),suc(u))*. % 1.28/1.51 68[0:MRR:36.6,36.7,62.6,61.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)))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 1.28/1.51 69[0:MRR:11.2,11.7,61.6,33.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)))) E(0,f(suc(suc(suc(v)))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 70[0:MRR:22.6,22.7,62.7,33.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(suc(u)))))+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))*. % 1.28/1.51 71[0:MRR:34.7,34.8,64.7,65.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v))))*+ E(s(0),f(suc(suc(u))))* -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.28/1.51 72[0:MRR:31.6,31.7,64.6,13.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v)))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))*. % 1.28/1.51 73[0:MRR:52.7,52.8,13.6,65.7] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u)))* E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 74[0:MRR:6.6,6.8,6.9,70.8,62.7,33.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(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(v)))*. % 1.28/1.51 75[0:MRR:47.2,47.6,47.9,61.6,69.7,33.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)))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v))))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(u)))*. % 1.28/1.51 76[0:MRR:29.7,29.8,29.9,68.8,70.7,61.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))))* E(f(u),f(suc(suc(suc(u)))))*. % 1.28/1.51 77[0:MRR:44.3,44.8,44.9,68.7,62.6,69.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(v)))))+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 78[0:MRR:9.8,9.9,9.10,13.6,73.8,65.7] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u)))* E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v))))))*+ -> E(f(u),f(suc(u)))*. % 1.28/1.51 79[0:MRR:25.3,25.8,25.9,72.7,64.6,13.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v)))* E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u))))))*+ -> E(f(v),f(suc(v)))*. % 1.28/1.51 80[0:MRR:14.7,14.8,14.9,71.7,72.8,65.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))*+ -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))*. % 1.28/1.51 81[0:MRR:32.8,32.9,32.10,64.7,73.7,71.8] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(suc(v)))))*+ -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(suc(v)))))*. % 1.28/1.51 82[0:MRR:16.7,16.9,16.10,16.11,76.9,68.8,74.8,61.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))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(v))))*. % 1.56/1.73 83[0:MRR:50.3,50.7,50.10,50.11,68.7,77.8,62.6,75.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(v))))) E(0,f(suc(suc(suc(suc(v))))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))*. % 1.56/1.73 84[0:MRR:37.3,37.9,37.10,37.11,76.8,77.9,70.7,69.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(v)))))+ E(0,f(suc(suc(suc(u))))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 1.56/1.73 85[0:MRR:28.4,28.9,28.10,28.11,80.8,71.7,79.8,65.6] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v))))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(s(0),f(suc(suc(suc(suc(u))))))*+ -> E(f(v),f(suc(suc(v))))*. % 1.56/1.73 86[0:MRR:45.9,45.10,45.11,45.12,64.7,78.8,81.9,71.8] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(u))))* E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v))))))*+ -> E(f(u),f(suc(suc(u))))*. % 1.56/1.73 87[0:MRR:15.8,15.9,15.10,15.12,81.8,72.8,73.7,80.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(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(f(v),f(suc(suc(suc(v)))))* E(f(u),f(suc(suc(suc(u)))))*. % 1.56/1.73 88[0:MRR:17.3,17.8,17.11,17.12,17.13,82.9,84.10,77.9,74.8,69.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(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(suc(v)))))*. % 1.56/1.73 89[0:MRR:27.3,27.8,27.11,27.12,27.13,76.8,84.9,83.9,70.7,75.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(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(v))))))*+ iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(suc(u)))))*. % 1.56/1.73 90[0:MRR:1.4,1.10,1.11,1.12,1.14,87.9,81.8,79.8,73.7,85.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(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(suc(suc(suc(u))))))*+ -> E(f(v),f(suc(suc(suc(v)))))*. % 1.56/1.73 91[0:MRR:49.9,49.10,49.11,49.12,49.14,86.9,72.8,78.8,87.10,80.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(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(suc(suc(suc(v))))))*+ -> E(f(u),f(suc(suc(suc(u)))))*. % 1.56/1.73 92[0:MRR:35.3,35.8,35.10,35.13,35.14,35.15,82.9,88.10,89.10,83.9,74.8,75.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(v))))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))*+ E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* -> . % 1.56/1.73 93[0:MRR:40.5,40.11,40.12,40.13,40.14,40.16,91.10,86.9,79.8,78.8,90.10,85.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(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(suc(suc(suc(u))))))*+ E(s(0),f(suc(suc(suc(suc(v))))))* -> . % 1.56/1.73 143[0:Res:57.1,67.4] || 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(u),s(0)) iLEQ(suc(u),suc(u))*. % 1.56/1.73 144[0:MRR:143.0,143.1,143.2,143.3,53.1,54.1,55.1,56.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 1.56/1.73 2768[0:Res:57.1,93.9] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(u)) E(s(0),f(suc(v))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(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(suc(suc(suc(v))))))* -> LE(f(u),s(0)). % 1.56/1.73 2769[0:MRR:2768.2,2768.4,2768.6,2768.7,53.1,54.1,55.1,56.1] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v))))) E(s(0),f(suc(suc(suc(suc(v))))))*+ -> LE(f(u),s(0)). % 1.56/1.73 4035[0:Res:57.1,2769.5] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v)))) E(s(0),f(suc(suc(suc(v)))))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 1.56/1.73 4036[0:MRR:4035.1,4035.2,4035.3,4035.4,53.1,54.1,55.1,56.1] || iLEQ(suc(u),suc(v))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 1.56/1.73 4040[0:Res:144.1,4036.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 1.56/1.73 4073[0:Obv:4040.1] || -> LE(f(u),s(0))*. % 1.56/1.73 4074[0:MRR:20.0,4073.0] || -> E(0,f(u))* LE(f(u),0). % 1.56/1.73 4075[0:MRR:19.0,4073.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 1.56/1.73 4076[0:MRR:51.0,4073.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 1.56/1.73 4077[0:MRR:3.0,4073.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 1.56/1.73 4078[0:MRR:39.0,4073.0] || -> E(0,f(suc(suc(suc(suc(u))))))* LE(f(u),0). % 1.56/1.73 4234[0:Res:4078.0,92.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(v))))) E(0,f(suc(suc(suc(u)))))* E(0,f(suc(suc(suc(suc(v))))))* iLEQ(suc(v),suc(u))* -> LE(f(u),0). % 1.56/1.73 4238[0:Res:4078.0,66.4] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))* -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 1.56/1.73 4247[0:MRR:4238.0,4238.1,4238.2,4238.3,4074.0,4075.0,4076.0,4077.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 1.56/1.73 4262[0:MRR:4234.0,4234.2,4234.5,4234.7,4074.0,4075.0,4076.0,4077.0] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(u),suc(v))* -> LE(f(v),0). % 1.56/1.73 5023[0:Res:4078.0,4262.4] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))* iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0). % 1.56/1.73 5024[0:MRR:5023.0,5023.1,5023.2,5023.3,4074.0,4075.0,4076.0,4077.0] || iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0). % 1.56/1.73 5029[0:Res:4247.1,5024.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 1.56/1.73 5036[0:Obv:5029.1] || -> LE(f(u),0)*. % 1.56/1.73 5037[0:UnC:5036.0,21.0] || -> . % 1.56/1.73 % SZS output end Refutation % 1.56/1.73 Formulae used in the proof : clause_603 clause_307 clause_575 clause_490 clause_417 clause_475 clause_14 clause_600 clause_352 clause_200 clause_494 clause_91 clause_538 clause_582 clause_529 clause_636 clause_660 clause_667 clause_460 clause_423 clause_332 clause_246 clause_66 clause_271 clause_165 clause_551 clause_451 clause_366 clause_399 clause_253 clause_128 clause_374 clause_217 clause_162 clause_618 clause_290 clause_347 clause_282 clause_112 clause_531 clause_359 clause_402 clause_465 clause_409 clause_145 clause_267 clause_604 clause_672 clause_447 clause_205 clause_537 clause_173 % 1.56/1.73 %------------------------------------------------------------------------------