%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO658-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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:22 EDT 2022 % Result : Unsatisfiable 0.37s 0.60s % Output : Refutation 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SYO658-1 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n015.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 10:03:52 EDT 2022 % 0.12/0.33 % CPUTime : % 0.37/0.60 % 0.37/0.60 SPASS V 3.9 % 0.37/0.60 SPASS beiseite: Proof found. % 0.37/0.60 % SZS status Theorem % 0.37/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.37/0.60 SPASS derived 765 clauses, backtracked 0 clauses, performed 0 splits and kept 240 clauses. % 0.37/0.60 SPASS allocated 64035 KBytes. % 0.37/0.60 SPASS spent 0:00:00.26 on the problem. % 0.37/0.60 0:00:00.04 for the input. % 0.37/0.60 0:00:00.00 for the FLOTTER CNF translation. % 0.37/0.60 0:00:00.03 for inferences. % 0.37/0.60 0:00:00.00 for the backtracking. % 0.37/0.60 0:00:00.15 for the reduction. % 0.37/0.60 % 0.37/0.60 % 0.37/0.60 Here is a proof with depth 3, length 79 : % 0.37/0.60 % SZS output start Refutation % 0.37/0.60 1[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))) -> . % 0.37/0.60 2[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(0)))* -> E(s(0),f(suc(suc(suc(u))))) LE(f(u),s(0)). % 0.37/0.60 3[0:Inp] || LE(f(suc(u)),s(s(0)))* -> E(s(0),f(suc(u))) LE(f(u),s(0)). % 0.37/0.60 4[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.37/0.60 5[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(v),f(suc(v)))*. % 0.37/0.60 6[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)))*. % 0.37/0.60 7[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 0.37/0.60 8[0:Inp] || LE(f(z__dfg),0)* -> . % 0.37/0.60 9[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))))*. % 0.37/0.60 10[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)). % 0.37/0.60 11[0:Inp] || -> LE(f(u),s(s(0)))*. % 0.37/0.60 12[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)))*. % 0.37/0.60 13[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)))*. % 0.37/0.60 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(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))))* -> . % 0.37/0.60 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(v),f(suc(v))) E(f(u),f(suc(u))) E(f(v),f(suc(suc(v))))* -> E(f(u),f(suc(suc(u))))*. % 0.37/0.60 16[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))))*. % 0.37/0.60 17[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))) -> iLEQ(suc(u),suc(u)). % 0.37/0.60 18[0:Inp] || LE(f(u),s(s(0)))* -> E(s(0),f(u)) LE(f(u),s(0)). % 0.37/0.60 19[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))))*. % 0.37/0.60 20[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(v),f(suc(suc(v))))*. % 0.37/0.60 21[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 0.37/0.60 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(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))))*. % 0.37/0.60 23[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(v),f(suc(v)))*. % 0.37/0.60 24[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(v),f(suc(suc(v))))*. % 0.37/0.60 25[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))))*. % 0.37/0.60 26[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)). % 0.37/0.60 27[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 0.37/0.60 28[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> E(s(0),f(suc(suc(u)))) LE(f(u),s(0)). % 0.37/0.60 29[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)))*. % 0.37/0.60 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)))*. % 0.37/0.60 31[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 0.37/0.60 32[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)))*. % 0.37/0.60 33[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 0.37/0.60 34[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)))))* -> iLEQ(suc(u),suc(u)). % 0.37/0.60 35[0:MRR:18.0,11.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 0.37/0.60 36[0:MRR:3.0,11.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 0.37/0.60 37[0:MRR:28.0,11.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 0.37/0.60 38[0:MRR:2.0,11.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u)))))*. % 0.37/0.60 39[0:MRR:10.2,33.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))))*. % 0.37/0.60 40[0:MRR:26.2,4.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))))*. % 0.37/0.60 41[0:MRR:17.2,17.5,39.3,33.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))*. % 0.37/0.60 42[0:MRR:34.3,34.4,40.3,4.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))*. % 0.37/0.60 43[0:MRR:13.5,29.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))))*. % 0.37/0.60 44[0:MRR:22.5,29.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))))*. % 0.37/0.60 45[0:MRR:19.6,12.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))))*. % 0.37/0.60 46[0:MRR:30.6,12.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))))*. % 0.37/0.60 47[0:MRR:23.2,23.7,43.6,29.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)))*. % 0.37/0.60 48[0:MRR:32.6,32.7,44.7,29.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)))*. % 0.37/0.60 49[0:MRR:5.6,5.7,46.6,12.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)))*. % 0.37/0.60 50[0:MRR:6.7,6.8,12.6,45.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)))*. % 0.37/0.60 51[0:MRR:9.6,9.7,44.6,43.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))))*. % 0.37/0.60 52[0:MRR:16.7,16.8,46.7,45.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))))*. % 0.46/0.62 53[0:MRR:20.3,20.8,20.9,51.7,44.6,47.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))))*. % 0.46/0.62 54[0:MRR:25.7,25.8,25.9,51.8,48.7,43.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))))*. % 0.46/0.62 55[0:MRR:15.8,15.9,15.10,46.7,50.7,52.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))))*. % 0.46/0.62 56[0:MRR:24.7,24.8,24.9,52.7,49.7,45.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))))*. % 0.46/0.62 57[0:MRR:1.3,1.9,1.10,1.11,54.8,53.8,48.7,47.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)))))*+ E(0,f(suc(suc(suc(u)))))* iLEQ(suc(v),suc(u))* -> . % 0.46/0.62 58[0:MRR:14.8,14.9,14.10,14.12,55.8,49.7,50.7,56.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(u)))))*+ E(s(0),f(suc(suc(suc(v)))))* -> . % 0.46/0.62 62[0:Res:38.1,42.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))*. % 0.46/0.62 63[0:MRR:62.0,62.1,62.2,35.1,36.1,37.1] || -> LE(f(u),s(0)) iLEQ(suc(u),suc(u))*. % 0.46/0.62 935[0:Res:38.1,58.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(u))))* E(s(0),f(suc(suc(suc(v)))))* -> LE(f(u),s(0)). % 0.46/0.62 936[0:MRR:935.2,935.4,935.6,35.1,36.1,37.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)))))*+ -> LE(f(u),s(0)). % 0.46/0.62 1008[0:Res:38.1,936.4] || iLEQ(suc(u),suc(v))* E(s(0),f(v)) E(s(0),f(suc(v))) E(s(0),f(suc(suc(v))))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 0.46/0.62 1009[0:MRR:1008.1,1008.2,1008.3,35.1,36.1,37.1] || iLEQ(suc(u),suc(v))* -> LE(f(v),s(0)) LE(f(u),s(0)). % 0.46/0.62 1012[0:Res:63.1,1009.0] || -> LE(f(u),s(0))* LE(f(u),s(0))* LE(f(u),s(0))*. % 0.46/0.62 1030[0:Obv:1012.1] || -> LE(f(u),s(0))*. % 0.46/0.62 1031[0:MRR:27.0,1030.0] || -> E(0,f(u))* LE(f(u),0). % 0.46/0.62 1032[0:MRR:31.0,1030.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 0.46/0.62 1033[0:MRR:7.0,1030.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 0.46/0.62 1034[0:MRR:21.0,1030.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 0.46/0.62 1106[0:Res:1034.0,41.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))*. % 0.46/0.62 1107[0:Res:1034.0,57.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(u)))))* iLEQ(suc(v),suc(u))* -> LE(f(v),0). % 0.46/0.62 1112[0:MRR:1106.0,1106.1,1106.2,1031.0,1032.0,1033.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 0.46/0.62 1120[0:MRR:1107.1,1107.3,1107.4,1031.0,1032.0,1033.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(u))* -> LE(f(v),0). % 0.46/0.62 1299[0:Res:1034.0,1120.3] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u))))* iLEQ(suc(v),suc(u))* -> LE(f(u),0) LE(f(v),0). % 0.46/0.62 1300[0:MRR:1299.0,1299.1,1299.2,1031.0,1032.0,1033.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 0.46/0.62 1304[0:Res:1112.1,1300.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 0.46/0.62 1308[0:Obv:1304.1] || -> LE(f(u),0)*. % 0.46/0.62 1309[0:UnC:1308.0,8.0] || -> . % 0.46/0.62 % SZS output end Refutation % 0.46/0.62 Formulae used in the proof : clause_167 clause_75 clause_104 clause_81 clause_36 clause_150 clause_141 clause_87 clause_78 clause_4 clause_72 clause_142 clause_108 clause_140 clause_80 clause_41 clause_139 clause_51 clause_71 clause_30 clause_151 clause_174 clause_29 clause_40 clause_130 clause_16 clause_109 clause_129 clause_55 clause_65 clause_122 clause_162 clause_93 clause_134 % 0.46/0.62 %------------------------------------------------------------------------------