%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO648-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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 0.38s 0.61s % Output : Refutation 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SYO648-1 : TPTP v8.1.0. Released v7.3.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n011.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 04:05:55 EDT 2022 % 0.12/0.33 % CPUTime : % 0.38/0.61 % 0.38/0.61 SPASS V 3.9 % 0.38/0.61 SPASS beiseite: Proof found. % 0.38/0.61 % SZS status Theorem % 0.38/0.61 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.61 SPASS derived 682 clauses, backtracked 0 clauses, performed 0 splits and kept 225 clauses. % 0.38/0.61 SPASS allocated 63928 KBytes. % 0.38/0.61 SPASS spent 0:00:00.27 on the problem. % 0.38/0.61 0:00:00.04 for the input. % 0.38/0.61 0:00:00.00 for the FLOTTER CNF translation. % 0.38/0.61 0:00:00.03 for inferences. % 0.38/0.61 0:00:00.00 for the backtracking. % 0.38/0.61 0:00:00.18 for the reduction. % 0.38/0.61 % 0.38/0.61 % 0.38/0.61 Here is a proof with depth 3, length 59 : % 0.38/0.61 % SZS output start Refutation % 0.38/0.61 1[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(v))) iLEQ(suc(u),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)))*. % 0.38/0.61 2[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 0.38/0.61 3[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> iLEQ(suc(u),suc(u)) E(f(u),f(suc(u)))*. % 0.38/0.61 4[0:Inp] || E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(u))) E(0,f(suc(suc(v)))) -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 0.38/0.61 5[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(f(v),f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(0,f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 0.38/0.61 6[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))) -> E(f(u),f(suc(suc(suc(u)))))* iLEQ(suc(u),suc(u)). % 0.38/0.61 7[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(f(v),f(suc(suc(v)))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(suc(u)))))) -> E(f(v),f(suc(suc(suc(v)))))*. % 0.38/0.61 8[0:Inp] || -> LE(f(u),s(0))*. % 0.38/0.61 9[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(u))) E(f(u),f(suc(suc(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))) E(0,f(suc(suc(suc(suc(u)))))) -> iLEQ(suc(u),suc(u)). % 0.38/0.61 10[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 0.38/0.61 11[0:Inp] || E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(suc(u)))) E(0,f(suc(v))) E(0,f(v)) E(0,f(suc(u))) E(f(u),f(suc(u))) iLEQ(suc(v),suc(u))* E(0,f(u)) E(0,f(suc(suc(u)))) -> E(f(v),f(suc(v)))* E(f(u),f(suc(suc(suc(u)))))*. % 0.38/0.61 12[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(0,f(suc(suc(suc(suc(u)))))) -> E(f(v),f(suc(v)))*. % 0.38/0.61 13[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(0,f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v)))*. % 0.38/0.61 14[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.38/0.61 15[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(0))* -> E(0,f(suc(suc(suc(suc(u)))))) LE(f(u),0). % 0.38/0.61 16[0:Inp] || E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(suc(u)))) E(0,f(suc(v))) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(u))) iLEQ(suc(v),suc(u))* E(0,f(u)) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) -> E(f(v),f(suc(v)))*. % 0.38/0.61 17[0:Inp] || E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(suc(u)))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(u))) E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(u))) iLEQ(suc(v),suc(u))* E(0,f(u)) E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(v))) E(0,f(suc(suc(u)))) -> E(f(v),f(suc(suc(v))))*. % 0.38/0.61 18[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.38/0.61 19[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 0.38/0.61 20[0:Inp] || E(0,f(suc(suc(suc(u))))) E(f(u),f(suc(suc(u)))) E(0,f(suc(v))) E(0,f(suc(suc(v)))) E(0,f(v)) E(0,f(suc(u))) E(f(u),f(suc(u))) iLEQ(suc(v),suc(u))* E(0,f(u)) E(f(v),f(suc(v))) E(0,f(suc(suc(u)))) -> E(f(v),f(suc(suc(v))))* E(f(u),f(suc(suc(suc(u)))))*. % 0.38/0.61 21[0:Inp] || LE(f(z__dfg),0)* -> . % 0.38/0.61 22[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(suc(u)))))) -> E(f(v),f(suc(suc(v))))*. % 0.38/0.61 23[0:Inp] || E(0,f(suc(u))) E(0,f(u)) E(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(0,f(suc(suc(v)))) -> E(f(u),f(suc(u)))* E(f(v),f(suc(suc(v))))*. % 0.38/0.61 24[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(f(v),f(suc(suc(v)))) E(0,f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(suc(suc(v)))))* E(f(u),f(suc(u))) E(0,f(suc(suc(v)))) E(0,f(suc(suc(suc(suc(u)))))) -> . % 0.38/0.61 25[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(0,f(suc(v))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(suc(u)))) E(f(u),f(suc(u))) E(0,f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(v))))*. % 0.38/0.61 26[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 0.38/0.61 27[0:Inp] || E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(f(v),f(suc(suc(v)))) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(u)) E(0,f(suc(v))) E(0,f(suc(suc(suc(suc(v)))))) E(f(v),f(suc(v))) iLEQ(suc(u),suc(v))* E(0,f(v)) E(f(u),f(suc(suc(u)))) E(f(v),f(suc(suc(suc(v)))))* E(f(u),f(suc(u))) E(0,f(suc(suc(v)))) -> E(f(u),f(suc(suc(suc(u)))))*. % 0.38/0.61 28[0:MRR:26.0,8.0] || -> E(0,f(u))* LE(f(u),0). % 0.38/0.61 29[0:MRR:10.0,8.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 0.38/0.61 30[0:MRR:19.0,8.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 0.38/0.61 31[0:MRR:2.0,8.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 0.38/0.61 32[0:MRR:15.0,8.0] || -> E(0,f(suc(suc(suc(suc(u))))))* LE(f(u),0). % 0.38/0.61 33[0:MRR:18.2,3.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.38/0.61 34[0:MRR:6.4,6.5,33.3,3.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)))))*. % 0.38/0.61 35[0:MRR:1.6,14.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.38/0.61 36[0:MRR:23.3,14.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.38/0.61 37[0:MRR:9.2,9.5,9.6,34.4,33.3,3.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))*. % 0.38/0.61 38[0:MRR:4.4,4.7,35.7,36.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(v)))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(u))))* E(f(v),f(suc(suc(v))))*. % 0.38/0.61 39[0:MRR:11.1,11.5,36.7,14.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)))))*. % 0.38/0.61 40[0:MRR:13.7,13.8,35.6,14.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)))))*. % 0.38/0.61 41[0:MRR:12.2,12.8,12.9,40.7,35.6,14.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)))*. % 0.38/0.61 42[0:MRR:16.1,16.6,16.9,36.7,14.6,39.8] || 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)))*. % 0.38/0.61 43[0:MRR:20.1,20.6,20.9,38.8,35.7,39.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(v)))) 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)))))*. % 0.38/0.61 44[0:MRR:25.5,25.8,25.9,40.8,38.7,36.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(v)))) 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)))))*. % 0.38/0.62 45[0:MRR:17.1,17.7,17.10,17.11,38.8,35.7,43.9,42.8] || 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(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(v))))*. % 0.38/0.62 46[0:MRR:22.2,22.6,22.9,22.10,44.8,41.8,38.7,36.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(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(suc(u))))*. % 0.38/0.62 47[0:MRR:5.2,5.7,5.10,5.11,44.9,40.8,43.8,39.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(v)))) E(0,f(suc(suc(suc(u)))))+ E(0,f(suc(suc(suc(v))))) iLEQ(suc(v),suc(u))* -> E(f(u),f(suc(suc(suc(u)))))* E(f(v),f(suc(suc(suc(v)))))*. % 0.38/0.62 48[0:MRR:7.2,7.4,7.8,7.11,7.12,46.9,47.9,41.8,43.8,39.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(v)))) E(0,f(suc(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(suc(u)))))*. % 0.38/0.62 49[0:MRR:27.2,27.8,27.11,27.12,27.13,44.9,40.8,45.9,47.10,42.8] || 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(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(u))))))*+ iLEQ(suc(v),suc(u))* -> E(f(v),f(suc(suc(suc(v)))))*. % 0.38/0.62 50[0:MRR:24.2,24.4,24.9,24.12,24.13,24.14,46.9,49.10,41.8,45.9,48.10,42.8] || 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(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v))))) E(0,f(suc(suc(suc(suc(v))))))*+ E(0,f(suc(suc(suc(suc(u))))))* iLEQ(suc(v),suc(u))* -> . % 0.38/0.62 55[0:Res:32.0,37.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))*. % 0.38/0.62 56[0:MRR:55.0,55.1,55.2,55.3,28.0,29.0,30.0,31.0] || -> LE(f(u),0) iLEQ(suc(u),suc(u))*. % 0.38/0.62 679[0:Res:32.0,50.8] || 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(v)))) E(0,f(suc(suc(suc(u))))) E(0,f(suc(suc(suc(v)))))* E(0,f(suc(suc(suc(suc(u))))))* iLEQ(suc(v),suc(u))* -> LE(f(v),0). % 0.38/0.62 680[0:MRR:679.1,679.3,679.5,679.7,28.0,29.0,30.0,31.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(v),suc(u))* -> LE(f(v),0). % 0.38/0.62 1107[0:Res:32.0,680.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(v),suc(u))* -> LE(f(u),0) LE(f(v),0). % 0.38/0.62 1108[0:MRR:1107.0,1107.1,1107.2,1107.3,28.0,29.0,30.0,31.0] || iLEQ(suc(u),suc(v))* -> LE(f(v),0) LE(f(u),0). % 0.38/0.62 1113[0:Res:56.1,1108.0] || -> LE(f(u),0)* LE(f(u),0)* LE(f(u),0)*. % 0.38/0.62 1120[0:Obv:1113.1] || -> LE(f(u),0)*. % 0.38/0.62 1121[0:UnC:1120.0,21.0] || -> . % 0.38/0.62 % SZS output end Refutation % 0.38/0.62 Formulae used in the proof : clause_113 clause_260 clause_48 clause_79 clause_90 clause_326 clause_203 clause_299 clause_157 clause_328 clause_217 clause_44 clause_72 clause_168 clause_231 clause_46 clause_278 clause_254 clause_114 clause_223 clause_160 clause_277 clause_29 clause_145 clause_221 clause_62 clause_237 % 0.38/0.62 %------------------------------------------------------------------------------