%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO650-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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:19 EDT 2022 % Result : Unsatisfiable 1.09s 1.28s % Output : Refutation 1.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO650-1 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n028.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 02:05:25 EDT 2022 % 0.13/0.34 % CPUTime : % 1.09/1.28 % 1.09/1.28 SPASS V 3.9 % 1.09/1.28 SPASS beiseite: Proof found. % 1.09/1.28 % SZS status Theorem % 1.09/1.28 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.09/1.28 SPASS derived 1236 clauses, backtracked 0 clauses, performed 0 splits and kept 444 clauses. % 1.09/1.28 SPASS allocated 65134 KBytes. % 1.09/1.28 SPASS spent 0:00:00.93 on the problem. % 1.09/1.28 0:00:00.04 for the input. % 1.09/1.28 0:00:00.00 for the FLOTTER CNF translation. % 1.09/1.28 0:00:00.06 for inferences. % 1.09/1.28 0:00:00.00 for the backtracking. % 1.09/1.28 0:00:00.80 for the reduction. % 1.09/1.28 % 1.09/1.28 % 1.09/1.28 Here is a proof with depth 5, length 81 : % 1.09/1.28 % SZS output start Refutation % 1.09/1.28 1[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(v)) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(f(u),f(suc(suc(u))))* E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 1.09/1.28 2[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(f(w),f(suc(suc(w))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.09/1.28 3[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(f(w),f(suc(suc(w))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))*. % 1.09/1.28 4[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 1.09/1.28 5[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(f(u),f(suc(suc(u))))* E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 1.09/1.28 6[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 7[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 1.09/1.28 8[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 9[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))*. % 1.09/1.28 10[0:Inp] || -> LE(f(u),s(0))*. % 1.09/1.28 11[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 1.09/1.28 12[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(v),f(suc(suc(v))))* E(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(w),f(suc(w)))*. % 1.09/1.28 13[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))*. % 1.09/1.28 14[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u))))* E(f(u),f(suc(u))) -> iLEQ(suc(u),suc(u)). % 1.09/1.28 15[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 16[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 17[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(0,f(v)) E(f(w),f(suc(suc(w))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 1.09/1.28 18[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(v),f(suc(suc(v))))* E(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(w),f(suc(suc(w))))*. % 1.09/1.28 19[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 1.09/1.28 20[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 21[0:Inp] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v)))+ E(0,f(suc(w))) E(0,f(suc(u))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 1.09/1.28 22[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 1.09/1.28 23[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(f(u),f(suc(suc(u))))* E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 24[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(v))))) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w))))* E(f(v),f(suc(suc(v))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> . % 1.09/1.28 25[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(0,f(u)) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))*. % 1.09/1.28 26[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.09/1.28 27[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(f(u),f(suc(suc(u))))* E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 28[0:Inp] || LE(f(z__dfg),0)* -> . % 1.09/1.28 29[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(f(w),f(suc(w))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(f(w),f(suc(suc(w))))* E(f(u),f(suc(suc(u))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))*. % 1.09/1.28 30[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(suc(w)))) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(f(w),f(suc(suc(w))))* E(0,f(suc(suc(suc(w))))) E(0,f(w)) E(0,f(suc(v))) -> E(f(v),f(suc(v)))*. % 1.09/1.28 31[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(v)) iLEQ(suc(u),suc(w))* E(0,f(u)) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w)))*. % 1.09/1.28 32[0:Inp] || E(0,f(suc(suc(u)))) iLEQ(suc(v),suc(u))* E(0,f(suc(w))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(v)) iLEQ(suc(u),suc(w))* E(f(v),f(suc(v))) E(0,f(u)) E(0,f(w)) E(f(u),f(suc(u))) E(0,f(suc(u))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(w)))*. % 1.09/1.28 33[0:Inp] || E(0,f(suc(suc(suc(u))))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 1.09/1.28 34[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 1.09/1.28 35[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(v)))) iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(f(u),f(suc(suc(u))))* iLEQ(suc(v),suc(w))* E(f(u),f(suc(u))) E(0,f(v)) E(0,f(w)) E(f(v),f(suc(v))) E(0,f(suc(v))) -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(w)))*. % 1.09/1.28 36[0:Inp] || iLEQ(suc(u),suc(v))* E(0,f(suc(w))) E(0,f(suc(u))) E(f(w),f(suc(w))) E(0,f(u)) E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(w))* E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 37[0:MRR:7.0,10.0] || -> E(0,f(u))* LE(f(u),0). % 1.09/1.28 38[0:MRR:19.0,10.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 1.09/1.28 39[0:MRR:11.0,10.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 1.09/1.28 40[0:MRR:22.0,10.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 1.09/1.28 41[0:MRR:26.2,34.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.09/1.28 42[0:MRR:14.4,14.5,41.3,34.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))*. % 1.09/1.28 43[0:MRR:4.6,21.8] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 44[0:MRR:31.8,21.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(v))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))*. % 1.09/1.28 45[0:MRR:36.3,21.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))*. % 1.09/1.28 46[0:MRR:1.8,1.10,44.10,21.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(w)))*. % 1.09/1.28 47[0:MRR:17.3,17.8,21.10,45.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(w)))*. % 1.09/1.28 48[0:MRR:33.6,33.8,43.9,21.8] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(v)))*. % 1.09/1.28 49[0:MRR:6.4,6.10,44.11,45.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(v)))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 1.09/1.28 50[0:MRR:16.3,16.8,43.11,45.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(w)))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 51[0:MRR:32.7,32.10,44.9,43.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w))))+ E(0,f(suc(suc(v)))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 52[0:MRR:2.4,2.9,2.12,44.11,49.12,47.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(v),f(suc(suc(v))))*. % 1.09/1.28 53[0:MRR:5.8,5.10,5.12,46.10,51.11,43.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 54[0:MRR:8.4,8.8,8.10,48.11,50.10,45.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(u))))*. % 1.09/1.28 55[0:MRR:13.3,13.8,13.10,43.11,47.10,50.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 56[0:MRR:23.4,23.10,23.12,46.11,49.11,45.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))* E(f(u),f(suc(suc(u))))*. % 1.09/1.28 57[0:MRR:35.7,35.9,35.12,51.10,44.9,48.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 1.09/1.28 58[0:MRR:15.4,15.9,15.12,51.12,49.10,50.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))+ E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 59[0:MRR:12.8,12.10,12.12,12.14,53.11,46.10,57.11,48.10] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(u)))*. % 1.09/1.28 60[0:MRR:25.4,25.10,25.11,25.14,46.11,56.12,52.12,47.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(w)))*. % 1.09/1.28 61[0:MRR:30.4,30.8,30.10,30.12,48.11,55.11,47.10,54.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(v)))*. % 1.09/1.28 62[0:MRR:3.4,3.9,3.11,3.14,51.12,52.11,58.13,55.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(v))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 63[0:MRR:20.5,20.9,20.11,20.14,57.12,58.11,49.10,54.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(w)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 1.09/1.28 64[0:MRR:27.4,27.10,27.12,27.14,53.12,56.11,58.12,50.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))* E(f(w),f(suc(suc(w))))*. % 1.09/1.28 65[0:MRR:9.5,9.9,9.11,9.13,9.16,57.12,62.12,52.11,63.13,61.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(v),f(suc(suc(v))))*. % 1.09/1.28 66[0:MRR:18.5,18.10,18.12,18.14,18.16,59.12,64.12,56.11,63.12,54.11] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))*+ E(0,f(suc(suc(suc(w)))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(u),f(suc(suc(u))))*. % 1.09/1.32 67[0:MRR:29.4,29.10,29.12,29.13,29.16,53.12,60.12,64.13,62.13,55.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> E(f(w),f(suc(suc(w))))*. % 1.09/1.32 68[0:MRR:24.5,24.10,24.12,24.14,24.15,24.18,59.12,67.13,60.12,66.13,65.13,61.12] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> . % 1.09/1.32 72[0:Res:40.0,42.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.09/1.32 73[0:MRR:72.0,72.1,72.2,37.0,38.0,39.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 1.09/1.32 1010[0:Res:40.0,68.9] || E(0,f(u)) E(0,f(v)) E(0,f(w)) E(0,f(suc(v))) E(0,f(suc(w))) E(0,f(suc(u))) E(0,f(suc(suc(u))))* E(0,f(suc(suc(w)))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(w)))))* iLEQ(suc(v),suc(u))* iLEQ(suc(w),suc(v))* -> LE(f(u),0). % 1.09/1.32 1011[0:MRR:1010.0,1010.5,1010.6,37.0,38.0,39.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)))) E(0,f(suc(suc(suc(u)))))*+ E(0,f(suc(suc(suc(v)))))* iLEQ(suc(u),suc(w))* iLEQ(suc(v),suc(u))* -> LE(f(w),0). % 1.09/1.32 2054[0:Res:40.0,1011.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(u),suc(w))* iLEQ(suc(v),suc(u))* -> LE(f(u),0) LE(f(w),0). % 1.09/1.32 2055[0:MRR:2054.0,2054.2,2054.5,37.0,38.0,39.0] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u)))))*+ iLEQ(suc(v),suc(w))* iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(w),0). % 1.09/1.32 2081[0:Res:40.0,2055.3] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))* iLEQ(suc(v),suc(w))* iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0) LE(f(w),0). % 1.09/1.32 2082[0:MRR:2081.0,2081.1,2081.2,37.0,38.0,39.0] || iLEQ(suc(u),suc(v))*+ iLEQ(suc(w),suc(u))* -> LE(f(w),0) LE(f(u),0) LE(f(v),0). % 1.09/1.32 2091[0:Res:73.1,2082.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0) LE(f(v),0) LE(f(v),0). % 1.09/1.32 2095[0:Obv:2091.3] || iLEQ(suc(u),suc(v))* -> LE(f(u),0) LE(f(v),0). % 1.09/1.32 2101[0:Res:73.1,2095.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 1.09/1.32 2105[0:Obv:2101.1] || -> LE(f(u),0)*. % 1.09/1.32 2106[0:UnC:2105.0,28.0] || -> . % 1.09/1.32 % SZS output end Refutation % 1.09/1.32 Formulae used in the proof : clause_338 clause_150 clause_437 clause_211 clause_436 clause_419 clause_278 clause_217 clause_129 clause_406 clause_359 clause_109 clause_110 clause_189 clause_309 clause_145 clause_447 clause_24 clause_313 clause_2 clause_333 clause_376 clause_308 clause_135 clause_319 clause_345 clause_282 clause_206 clause_253 clause_88 clause_167 clause_441 clause_416 clause_64 clause_451 clause_371 % 1.09/1.32 %------------------------------------------------------------------------------