%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO667-1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:25 EDT 2022 % Result : Unsatisfiable 0.20s 0.44s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SYO667-1 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n007.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.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sat Jul 9 07:13:01 EDT 2022 % 0.14/0.35 % CPUTime : % 0.20/0.44 % 0.20/0.44 SPASS V 3.9 % 0.20/0.44 SPASS beiseite: Proof found. % 0.20/0.44 % SZS status Theorem % 0.20/0.44 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.44 SPASS derived 70 clauses, backtracked 0 clauses, performed 0 splits and kept 86 clauses. % 0.20/0.44 SPASS allocated 63195 KBytes. % 0.20/0.44 SPASS spent 0:00:00.08 on the problem. % 0.20/0.44 0:00:00.04 for the input. % 0.20/0.44 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.44 0:00:00.00 for inferences. % 0.20/0.44 0:00:00.00 for the backtracking. % 0.20/0.44 0:00:00.01 for the reduction. % 0.20/0.44 % 0.20/0.44 % 0.20/0.44 Here is a proof with depth 1, length 60 : % 0.20/0.44 % SZS output start Refutation % 0.20/0.44 1[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)) -> E(f(u),f(suc(suc(u))))*. % 0.20/0.44 2[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))))*. % 0.20/0.44 3[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(s(s(0))))* -> E(s(s(0)),f(suc(suc(suc(suc(u)))))) LE(f(u),s(s(0))). % 0.20/0.44 4[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(suc(u)))))). % 0.20/0.44 5[0:Inp] || E(f(u),f(suc(suc(u)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(suc(u)))))* E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u))))) E(f(u),f(suc(u))) E(s(0),f(u)) -> . % 0.20/0.44 6[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))))*. % 0.20/0.44 7[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(f(u),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) -> E(f(u),f(suc(suc(suc(u)))))*. % 0.20/0.44 8[0:Inp] || LE(f(suc(suc(suc(u)))),s(0))* -> E(0,f(suc(suc(suc(u))))) LE(f(u),0). % 0.20/0.44 9[0:Inp] || LE(f(suc(suc(u))),s(0))* -> E(0,f(suc(suc(u)))) LE(f(u),0). % 0.20/0.44 10[0:Inp] || LE(f(u),s(0))* -> E(0,f(u)) LE(f(u),0). % 0.20/0.44 11[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u))))). % 0.20/0.44 12[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u)))*+ -> E(f(u),f(suc(u)))*. % 0.20/0.44 13[0:Inp] || LE(f(u),s(s(s(0))))* -> E(s(s(0)),f(u)) LE(f(u),s(s(0))). % 0.20/0.44 14[0:Inp] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(suc(suc(u))))))* E(f(u),f(suc(suc(suc(u)))))* E(f(u),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u))))) E(f(u),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) -> . % 0.20/0.44 15[0:Inp] || E(0,f(suc(suc(suc(suc(u)))))) E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(u)) E(0,f(suc(suc(u)))) E(0,f(suc(u))) E(f(u),f(suc(u))) E(f(u),f(suc(suc(suc(u)))))* -> . % 0.20/0.44 16[0:Inp] || E(0,f(u)) E(0,f(suc(u))) -> E(f(u),f(suc(u)))*. % 0.20/0.44 17[0:Inp] || LE(f(suc(u)),s(0))* -> E(0,f(suc(u))) LE(f(u),0). % 0.20/0.44 18[0:Inp] || LE(f(suc(u)),s(s(s(0))))* -> E(s(s(0)),f(suc(u))) LE(f(u),s(s(0))). % 0.20/0.44 19[0:Inp] || LE(f(suc(suc(suc(u)))),s(s(s(0))))* -> E(s(s(0)),f(suc(suc(suc(u))))) LE(f(u),s(s(0))). % 0.20/0.44 20[0:Inp] || E(f(u),f(suc(suc(u)))) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u)))) E(s(0),f(suc(suc(suc(u)))))* E(f(u),f(suc(u))) E(s(0),f(u)) -> E(f(u),f(suc(suc(suc(u)))))*. % 0.20/0.44 21[0:Inp] || -> LE(f(u),s(s(s(0))))*. % 0.20/0.44 22[0:Inp] || LE(f(suc(u)),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(u))). % 0.20/0.44 23[0:Inp] || LE(f(z__dfg),0)* -> . % 0.20/0.44 24[0:Inp] || E(s(0),f(u)) E(s(0),f(suc(u)))*+ -> E(f(u),f(suc(u)))*. % 0.20/0.44 25[0:Inp] || E(f(u),f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) E(0,f(u)) E(0,f(suc(suc(u)))) E(0,f(suc(u))) E(f(u),f(suc(u))) -> E(f(u),f(suc(suc(suc(u)))))*. % 0.20/0.44 26[0:Inp] || LE(f(suc(suc(u))),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(suc(suc(u)))). % 0.20/0.44 27[0:Inp] || LE(f(suc(suc(suc(suc(u))))),s(0))* -> E(0,f(suc(suc(suc(suc(u)))))) LE(f(u),0). % 0.20/0.44 28[0:Inp] || LE(f(suc(suc(u))),s(s(s(0))))* -> E(s(s(0)),f(suc(suc(u)))) LE(f(u),s(s(0))). % 0.20/0.44 29[0:Inp] || LE(f(u),s(s(0)))* -> LE(f(u),s(0)) E(s(0),f(u)). % 0.20/0.44 30[0:MRR:13.0,21.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(u))*. % 0.20/0.44 31[0:MRR:18.0,21.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(u)))*. % 0.20/0.44 32[0:MRR:28.0,21.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(u))))*. % 0.20/0.44 33[0:MRR:19.0,21.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(suc(u)))))*. % 0.20/0.44 34[0:MRR:3.0,21.0] || -> LE(f(u),s(s(0))) E(s(s(0)),f(suc(suc(suc(suc(u))))))*. % 0.20/0.44 35[0:MRR:6.2,16.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) -> E(f(u),f(suc(suc(u))))*. % 0.20/0.44 36[0:MRR:2.2,24.2] || E(s(0),f(u)) E(s(0),f(suc(u))) E(s(0),f(suc(suc(u))))*+ -> E(f(u),f(suc(suc(u))))*. % 0.20/0.44 37[0:MRR:1.2,12.2] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u))))*+ -> E(f(u),f(suc(suc(u))))*. % 0.20/0.44 38[0:MRR:25.0,25.5,35.3,16.2] || E(0,f(u)) E(0,f(suc(u))) E(0,f(suc(suc(u)))) E(0,f(suc(suc(suc(u))))) -> E(f(u),f(suc(suc(suc(u)))))*. % 0.20/0.44 39[0:MRR:20.0,20.4,36.3,24.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(f(u),f(suc(suc(suc(u)))))*. % 0.20/0.44 40[0:MRR:7.2,7.4,37.3,12.2] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))*+ -> E(f(u),f(suc(suc(suc(u)))))*. % 0.20/0.44 41[0:MRR:15.1,15.6,15.7,35.3,16.2,38.4] || 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))))))* -> . % 0.20/0.44 42[0:MRR:5.0,5.3,5.6,36.3,39.4,24.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))))))* -> . % 0.20/0.44 43[0:MRR:14.3,14.4,14.6,40.4,37.3,12.2] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u))))) E(s(s(0)),f(suc(suc(suc(suc(u))))))* -> . % 0.20/0.44 86[0:Res:34.1,43.4] || E(s(s(0)),f(u)) E(s(s(0)),f(suc(u))) E(s(s(0)),f(suc(suc(u)))) E(s(s(0)),f(suc(suc(suc(u)))))* -> LE(f(u),s(s(0))). % 0.20/0.44 87[0:MRR:86.0,86.1,86.2,86.3,30.1,31.1,32.1,33.1] || -> LE(f(u),s(s(0)))*. % 0.20/0.44 88[0:MRR:29.0,87.0] || -> LE(f(u),s(0)) E(s(0),f(u))*. % 0.20/0.44 89[0:MRR:22.0,87.0] || -> LE(f(u),s(0)) E(s(0),f(suc(u)))*. % 0.20/0.44 90[0:MRR:26.0,87.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(u))))*. % 0.20/0.44 91[0:MRR:11.0,87.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(u)))))*. % 0.20/0.44 92[0:MRR:4.0,87.0] || -> LE(f(u),s(0)) E(s(0),f(suc(suc(suc(suc(u))))))*. % 0.20/0.44 129[0:Res:92.1,42.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)). % 0.20/0.44 132[0:MRR:129.0,129.1,129.2,129.3,88.1,89.1,90.1,91.1] || -> LE(f(u),s(0))*. % 0.20/0.44 133[0:MRR:10.0,132.0] || -> E(0,f(u))* LE(f(u),0). % 0.20/0.44 134[0:MRR:17.0,132.0] || -> E(0,f(suc(u)))* LE(f(u),0). % 0.20/0.44 135[0:MRR:9.0,132.0] || -> E(0,f(suc(suc(u))))* LE(f(u),0). % 0.20/0.44 136[0:MRR:8.0,132.0] || -> E(0,f(suc(suc(suc(u)))))* LE(f(u),0). % 0.20/0.44 137[0:MRR:27.0,132.0] || -> E(0,f(suc(suc(suc(suc(u))))))* LE(f(u),0). % 0.20/0.44 145[0:Res:137.0,41.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). % 0.20/0.44 146[0:MRR:145.0,145.1,145.2,145.3,133.0,134.0,135.0,136.0] || -> LE(f(u),0)*. % 0.20/0.44 147[0:UnC:146.0,23.0] || -> . % 0.20/0.44 % SZS output end Refutation % 0.20/0.44 Formulae used in the proof : clause_44 clause_33 clause_37 clause_8 clause_49 clause_24 clause_27 clause_41 clause_19 clause_13 clause_30 clause_21 clause_2 clause_4 clause_14 clause_23 clause_50 clause_42 clause_40 clause_29 clause_51 clause_3 clause_25 clause_22 clause_32 clause_43 clause_38 clause_6 clause_20 % 0.20/0.44 %------------------------------------------------------------------------------