%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV399+1 : TPTP v8.1.0. Released v3.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 : Wed Jul 20 21:42:39 EDT 2022 % Result : Theorem 0.21s 0.45s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SWV399+1 : TPTP v8.1.0. Released v3.3.0. % 0.08/0.14 % Command : run_spass %d %s % 0.15/0.35 % Computer : n007.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 600 % 0.15/0.35 % DateTime : Wed Jun 15 17:58:11 EDT 2022 % 0.15/0.35 % CPUTime : % 0.21/0.45 % 0.21/0.45 SPASS V 3.9 % 0.21/0.45 SPASS beiseite: Proof found. % 0.21/0.45 % SZS status Theorem % 0.21/0.45 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.21/0.45 SPASS derived 38 clauses, backtracked 0 clauses, performed 0 splits and kept 50 clauses. % 0.21/0.45 SPASS allocated 85230 KBytes. % 0.21/0.45 SPASS spent 0:00:00.09 on the problem. % 0.21/0.45 0:00:00.03 for the input. % 0.21/0.45 0:00:00.03 for the FLOTTER CNF translation. % 0.21/0.45 0:00:00.00 for inferences. % 0.21/0.45 0:00:00.00 for the backtracking. % 0.21/0.45 0:00:00.00 for the reduction. % 0.21/0.45 % 0.21/0.45 % 0.21/0.45 Here is a proof with depth 5, length 21 : % 0.21/0.45 % SZS output start Refutation % 0.21/0.45 1[0:Inp] || -> strictly_less_than(skc5,skc6)*. % 0.21/0.45 5[0:Inp] || -> pair_in_list(skc4,skc5,skc6)*. % 0.21/0.45 9[0:Inp] || -> less_than(u,v)* less_than(v,u)*. % 0.21/0.45 11[0:Inp] || strictly_less_than(u,v)* -> less_than(u,v). % 0.21/0.45 15[0:Inp] || less_than(u,v) -> less_than(v,u) strictly_less_than(u,v)*. % 0.21/0.45 16[0:Inp] || strictly_less_than(u,v) pair_in_list(update_slb(skc4,skc7),u,v)* -> . % 0.21/0.45 17[0:Inp] || less_than(u,v)* less_than(v,w)* -> less_than(u,w)*. % 0.21/0.45 22[0:Inp] || less_than(u,v) pair_in_list(w,x,v) -> pair_in_list(update_slb(w,u),x,v)*. % 0.21/0.45 23[0:Inp] || strictly_less_than(u,v)* pair_in_list(w,x,u)*+ -> pair_in_list(update_slb(w,v),x,v)*. % 0.21/0.45 31[0:MRR:15.0,9.0] || -> strictly_less_than(u,v)* less_than(v,u). % 0.21/0.45 33[0:Res:1.0,11.0] || -> less_than(skc5,skc6)*r. % 0.21/0.45 34[0:Res:1.0,16.1] || pair_in_list(update_slb(skc4,skc7),skc5,skc6)* -> . % 0.21/0.45 37[0:Res:5.0,22.0] || less_than(u,skc6) -> pair_in_list(update_slb(skc4,u),skc5,skc6)*. % 0.21/0.45 38[0:Res:5.0,23.0] || strictly_less_than(skc6,u) -> pair_in_list(update_slb(skc4,u),skc5,u)*. % 0.21/0.45 46[0:Res:38.1,16.1] || strictly_less_than(skc6,skc7)* strictly_less_than(skc5,skc7) -> . % 0.21/0.45 47[0:Res:31.0,46.0] || strictly_less_than(skc5,skc7)* -> less_than(skc7,skc6). % 0.21/0.45 49[0:Res:31.0,47.0] || -> less_than(skc7,skc5) less_than(skc7,skc6)*l. % 0.21/0.45 56[0:Res:37.1,34.0] || less_than(skc7,skc6)*l -> . % 0.21/0.45 59[0:MRR:49.1,56.0] || -> less_than(skc7,skc5)*l. % 0.21/0.45 68[0:NCh:17.2,17.0,56.0,59.0] || less_than(skc5,skc6)*r -> . % 0.21/0.45 70[0:MRR:68.0,33.0] || -> . % 0.21/0.45 % SZS output end Refutation % 0.21/0.45 Formulae used in the proof : l35_co totality stricly_smaller_definition transitivity l35_li3637 l35_li3839 % 0.21/0.45 %------------------------------------------------------------------------------