%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV408+1 : TPTP v8.1.0. Released v3.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 : Wed Jul 20 21:42:41 EDT 2022 % Result : Theorem 0.20s 0.49s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SWV408+1 : TPTP v8.1.0. Released v3.3.0. % 0.08/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n028.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % 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 : Wed Jun 15 23:22:26 EDT 2022 % 0.14/0.36 % CPUTime : % 0.20/0.49 % 0.20/0.49 SPASS V 3.9 % 0.20/0.49 SPASS beiseite: Proof found. % 0.20/0.49 % SZS status Theorem % 0.20/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.49 SPASS derived 47 clauses, backtracked 0 clauses, performed 0 splits and kept 83 clauses. % 0.20/0.49 SPASS allocated 85359 KBytes. % 0.20/0.49 SPASS spent 0:00:00.11 on the problem. % 0.20/0.49 0:00:00.04 for the input. % 0.20/0.49 0:00:00.04 for the FLOTTER CNF translation. % 0.20/0.49 0:00:00.00 for inferences. % 0.20/0.49 0:00:00.00 for the backtracking. % 0.20/0.49 0:00:00.01 for the reduction. % 0.20/0.49 % 0.20/0.49 % 0.20/0.49 Here is a proof with depth 1, length 18 : % 0.20/0.49 % SZS output start Refutation % 0.20/0.49 1[0:Inp] || -> contains_slb(skc4,skc5)*. % 0.20/0.49 6[0:Inp] || contains_slb(create_slb,u)* -> . % 0.20/0.49 10[0:Inp] || -> equal(findmin_cpq_res(u),removemin_cpq_res(u))**. % 0.20/0.49 11[0:Inp] || -> less_than(u,skf1(v,u,w))*r. % 0.20/0.49 15[0:Inp] || -> strictly_less_than(skc5,findmin_cpq_res(triple(skc6,skc4,skc7)))*. % 0.20/0.49 23[0:Inp] || pair_in_list(update_slb(skc4,findmin_pqp_res(skc6)),skc5,findmin_pqp_res(skc6))* -> . % 0.20/0.49 35[0:Inp] || -> equal(findmin_cpq_res(triple(u,v,w)),findmin_pqp_res(u))** equal(v,create_slb). % 0.20/0.49 36[0:Inp] || less_than(findmin_pqp_res(skc6),u) pair_in_list(update_slb(skc4,findmin_pqp_res(skc6)),skc5,u)* -> . % 0.20/0.49 52[0:Inp] || strictly_less_than(u,v) contains_slb(w,u) -> pair_in_list(update_slb(w,v),u,v) pair_in_list(update_slb(w,v),u,skf1(u,v,w))*. % 0.20/0.49 58[0:Rew:10.0,15.0] || -> strictly_less_than(skc5,removemin_cpq_res(triple(skc6,skc4,skc7)))*. % 0.20/0.49 60[0:Rew:10.0,35.0] || -> equal(u,create_slb) equal(removemin_cpq_res(triple(v,u,w)),findmin_pqp_res(v))**. % 0.20/0.49 75[0:Res:52.2,23.0] || contains_slb(skc4,skc5) strictly_less_than(skc5,findmin_pqp_res(skc6)) -> pair_in_list(update_slb(skc4,findmin_pqp_res(skc6)),skc5,skf1(skc5,findmin_pqp_res(skc6),skc4))*. % 0.20/0.49 79[0:Res:11.0,36.1] || pair_in_list(update_slb(skc4,findmin_pqp_res(skc6)),skc5,skf1(u,findmin_pqp_res(skc6),v))* -> . % 0.20/0.49 80[0:MRR:75.0,75.2,1.0,79.0] || strictly_less_than(skc5,findmin_pqp_res(skc6))* -> . % 0.20/0.49 101[0:SpR:60.1,58.0] || -> equal(skc4,create_slb) strictly_less_than(skc5,findmin_pqp_res(skc6))*. % 0.20/0.49 104[0:MRR:101.1,80.0] || -> equal(skc4,create_slb)**. % 0.20/0.49 105[0:Rew:104.0,1.0] || -> contains_slb(create_slb,skc5)*. % 0.20/0.49 119[0:MRR:105.0,6.0] || -> . % 0.20/0.49 % SZS output end Refutation % 0.20/0.49 Formulae used in the proof : l44_co ax20 ax53 l44_l45 reflexivity transitivity ax51 % 0.20/0.49 %------------------------------------------------------------------------------