%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV409+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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.92s 1.11s % Output : Refutation 0.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWV409+1 : TPTP v8.1.0. Released v3.3.0. % 0.12/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n015.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 14 17:21:24 EDT 2022 % 0.13/0.34 % CPUTime : % 0.92/1.11 % 0.92/1.11 SPASS V 3.9 % 0.92/1.11 SPASS beiseite: Proof found. % 0.92/1.11 % SZS status Theorem % 0.92/1.11 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.92/1.11 SPASS derived 1880 clauses, backtracked 1 clauses, performed 2 splits and kept 1031 clauses. % 0.92/1.11 SPASS allocated 87855 KBytes. % 0.92/1.11 SPASS spent 0:00:00.75 on the problem. % 0.92/1.11 0:00:00.03 for the input. % 0.92/1.11 0:00:00.04 for the FLOTTER CNF translation. % 0.92/1.11 0:00:00.05 for inferences. % 0.92/1.11 0:00:00.00 for the backtracking. % 0.92/1.11 0:00:00.59 for the reduction. % 0.92/1.11 % 0.92/1.11 % 0.92/1.11 Here is a proof with depth 5, length 20 : % 0.92/1.11 % SZS output start Refutation % 0.92/1.11 1[0:Inp] || -> contains_slb(skc5,skc3)*. % 0.92/1.11 2[0:Inp] || -> strictly_less_than(skc3,skc4)*. % 0.92/1.11 9[0:Inp] || -> less_than(u,skf3(v,u,w))*r. % 0.92/1.11 10[0:Inp] || -> less_than(u,v)* less_than(v,u)*. % 0.92/1.11 12[0:Inp] || pair_in_list(update_slb(skc5,skc4),skc3,skc4)* -> . % 0.92/1.11 17[0:Inp] || contains_slb(u,v) -> pair_in_list(u,v,skf2(v,u))*. % 0.92/1.11 18[0:Inp] || less_than(u,v) -> less_than(v,u) strictly_less_than(u,v)*. % 0.92/1.11 19[0:Inp] || less_than(skc4,u) pair_in_list(update_slb(skc5,skc4),skc3,u)* -> . % 0.92/1.11 29[0:Inp] || strictly_less_than(u,v)* strictly_less_than(w,v) pair_in_list(x,w,u)*+ -> pair_in_list(update_slb(x,v),w,v)*. % 0.92/1.11 33[0:Inp] || less_than(u,v)*+ strictly_less_than(w,u) pair_in_list(x,w,v)* -> pair_in_list(update_slb(x,u),w,skf3(w,u,x))*. % 0.92/1.11 34[0:MRR:18.0,10.0] || -> strictly_less_than(u,v)* less_than(v,u). % 0.92/1.11 38[0:Res:2.0,33.1] || less_than(skc4,u)+ pair_in_list(v,skc3,u)* -> pair_in_list(update_slb(v,skc4),skc3,skf3(skc3,skc4,v))*. % 0.92/1.11 44[0:Res:1.0,17.0] || -> pair_in_list(skc5,skc3,skf2(skc3,skc5))*. % 0.92/1.11 45[0:Res:29.3,12.0] || pair_in_list(skc5,skc3,u)* strictly_less_than(skc3,skc4) strictly_less_than(u,skc4) -> . % 0.92/1.11 50[0:MRR:45.1,2.0] || strictly_less_than(u,skc4) pair_in_list(skc5,skc3,u)* -> . % 0.92/1.11 58[0:Res:44.0,50.1] || strictly_less_than(skf2(skc3,skc5),skc4)* -> . % 0.92/1.11 64[0:Res:34.0,58.0] || -> less_than(skc4,skf2(skc3,skc5))*r. % 0.92/1.11 2086[0:Res:64.0,38.0] || pair_in_list(u,skc3,skf2(skc3,skc5)) -> pair_in_list(update_slb(u,skc4),skc3,skf3(skc3,skc4,u))*. % 0.92/1.11 2170[0:Res:2086.1,19.1] || pair_in_list(skc5,skc3,skf2(skc3,skc5))* less_than(skc4,skf3(skc3,skc4,skc5)) -> . % 0.92/1.11 2179[0:MRR:2170.0,2170.1,44.0,9.0] || -> . % 0.92/1.11 % SZS output end Refutation % 0.92/1.11 Formulae used in the proof : l45_co l45_l49 reflexivity transitivity totality l45_li4647 stricly_smaller_definition l45_l48 % 0.92/1.11 %------------------------------------------------------------------------------