%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR056+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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 : Fri Jul 15 23:24:47 EDT 2022 % Result : Theorem 0.18s 0.44s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR056+1 : TPTP v8.1.0. Released v3.4.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n023.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 : Thu Jun 9 22:14:37 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.44 % 0.18/0.44 SPASS V 3.9 % 0.18/0.44 SPASS beiseite: Proof found. % 0.18/0.44 % SZS status Theorem % 0.18/0.44 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.44 SPASS derived 75 clauses, backtracked 0 clauses, performed 0 splits and kept 87 clauses. % 0.18/0.44 SPASS allocated 97736 KBytes. % 0.18/0.44 SPASS spent 0:00:00.09 on the problem. % 0.18/0.44 0:00:00.04 for the input. % 0.18/0.44 0:00:00.03 for the FLOTTER CNF translation. % 0.18/0.44 0:00:00.00 for inferences. % 0.18/0.44 0:00:00.00 for the backtracking. % 0.18/0.44 0:00:00.00 for the reduction. % 0.18/0.44 % 0.18/0.44 % 0.18/0.44 Here is a proof with depth 6, length 18 : % 0.18/0.44 % SZS output start Refutation % 0.18/0.44 1[0:Inp] || -> mtvisible(c_tptp_member3717_mt)*. % 0.18/0.44 10[0:Inp] || -> genlmt(c_tptp_spindleheadmt,c_cyclistsmt)*r. % 0.18/0.44 11[0:Inp] || -> genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)*r. % 0.18/0.44 13[0:Inp] || tptpofobject(c_tptpartsupplies,u)* -> . % 0.18/0.44 15[0:Inp] artsupplies(u) || -> supplies(u)*. % 0.18/0.44 16[0:Inp] || mtvisible(c_cyclistsmt) -> artsupplies(c_tptpartsupplies)*. % 0.18/0.44 57[0:Inp] mtvisible(u) || genlmt(u,v)* -> mtvisible(v)*. % 0.18/0.44 58[0:Inp] supplies(u) || mtvisible(c_tptp_spindleheadmt) -> tptpofobject(u,f_tptpquantityfn_14(n_232))*. % 0.18/0.44 66[0:Inp] || genlmt(u,v)* genlmt(v,w)* -> genlmt(u,w)*. % 0.18/0.44 71[0:Res:1.0,57.0] || genlmt(c_tptp_member3717_mt,u) -> mtvisible(u)*. % 0.18/0.44 72[0:Res:58.2,13.0] supplies(c_tptpartsupplies) || mtvisible(c_tptp_spindleheadmt)* -> . % 0.18/0.44 102[0:SoR:72.0,15.1] artsupplies(c_tptpartsupplies) || mtvisible(c_tptp_spindleheadmt)* -> . % 0.18/0.44 103[0:SoR:102.0,16.1] || mtvisible(c_tptp_spindleheadmt) mtvisible(c_cyclistsmt)* -> . % 0.18/0.44 126[0:Res:71.1,103.1] || genlmt(c_tptp_member3717_mt,c_cyclistsmt) mtvisible(c_tptp_spindleheadmt)* -> . % 0.18/0.44 173[0:Res:71.1,126.1] || genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt) genlmt(c_tptp_member3717_mt,c_cyclistsmt)*r -> . % 0.18/0.44 174[0:MRR:173.0,11.0] || genlmt(c_tptp_member3717_mt,c_cyclistsmt)*r -> . % 0.18/0.44 175[0:NCh:66.2,66.1,174.0,10.0] || genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)*r -> . % 0.18/0.44 176[0:MRR:175.0,11.0] || -> . % 0.18/0.44 % SZS output end Refutation % 0.18/0.44 Formulae used in the proof : query56 just8 just9 just2 just12 just47 just10 just52 % 0.18/0.44 %------------------------------------------------------------------------------