%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN563-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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 12:22:54 EDT 2022 % Result : Unsatisfiable 1.26s 1.46s % Output : Refutation 1.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SYN563-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n025.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 : Mon Jul 11 17:55:32 EDT 2022 % 0.12/0.33 % CPUTime : % 1.26/1.46 % 1.26/1.46 SPASS V 3.9 % 1.26/1.46 SPASS beiseite: Proof found. % 1.26/1.46 % SZS status Theorem % 1.26/1.46 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.26/1.46 SPASS derived 6253 clauses, backtracked 0 clauses, performed 0 splits and kept 3345 clauses. % 1.26/1.46 SPASS allocated 66604 KBytes. % 1.26/1.46 SPASS spent 0:00:01.11 on the problem. % 1.26/1.46 0:00:00.03 for the input. % 1.26/1.46 0:00:00.00 for the FLOTTER CNF translation. % 1.26/1.46 0:00:00.05 for inferences. % 1.26/1.46 0:00:00.00 for the backtracking. % 1.26/1.46 0:00:00.98 for the reduction. % 1.26/1.46 % 1.26/1.46 % 1.26/1.46 Here is a proof with depth 7, length 28 : % 1.26/1.46 % SZS output start Refutation % 1.26/1.46 1[0:Inp] || -> p2(u,u)*. % 1.26/1.46 2[0:Inp] || -> p6(u,u)*. % 1.26/1.46 4[0:Inp] || -> p2(f4(c7),f4(c8))*. % 1.26/1.46 5[0:Inp] || p6(f4(c7),f3(f4(c8)))*r -> . % 1.26/1.46 7[0:Inp] || -> p5(f3(f3(u)),f3(f4(u)))*. % 1.26/1.46 9[0:Inp] || p6(c7,u) -> p6(c7,f3(u))*r. % 1.26/1.46 10[0:Inp] || p5(u,v)* -> p6(f4(u),v). % 1.26/1.46 11[0:Inp] || p2(u,v) -> p2(f3(u),f3(v))*. % 1.26/1.46 13[0:Inp] || p2(u,v)*+ p2(u,w)* -> p2(w,v)*. % 1.26/1.46 14[0:Inp] || p6(u,v)* p6(v,w)* -> p6(u,w)*. % 1.26/1.46 15[0:Inp] || p6(u,v)*+ p5(v,w)* -> p5(u,w)*. % 1.26/1.46 17[0:Inp] || p2(u,v)*+ p5(u,w)* p2(w,x)* -> p5(v,x)*. % 1.26/1.46 18[0:Res:1.0,13.0] || p2(u,v)*+ -> p2(v,u)*. % 1.26/1.46 21[0:Res:11.1,13.0] || p2(u,v)* p2(f3(u),w)*+ -> p2(w,f3(v))*. % 1.26/1.46 73[0:Res:1.0,17.0] || p5(u,v)*+ p2(v,w)* -> p5(u,w)*. % 1.26/1.46 88[0:Res:7.0,73.0] || p2(f3(f4(u)),v) -> p5(f3(f3(u)),v)*. % 1.26/1.46 151[0:NCh:14.2,14.1,9.1,15.0] || p6(c7,u)+ p6(v,c7) p5(f3(u),w)* -> p5(v,w)*. % 1.26/1.46 292[0:Res:11.1,21.1] || p2(u,v)*+ p2(u,w)* -> p2(f3(v),f3(w))*. % 1.26/1.46 577[0:Res:9.1,151.0] || p6(c7,u)+ p6(v,c7) p5(f3(f3(u)),w)* -> p5(v,w)*. % 1.26/1.46 800[0:Res:4.0,292.0] || p2(f4(c7),u) -> p2(f3(f4(c8)),f3(u))*. % 1.26/1.46 994[0:Res:800.1,18.0] || p2(f4(c7),u) -> p2(f3(u),f3(f4(c8)))*. % 1.26/1.46 1851[0:Res:2.0,577.0] || p6(u,c7)+ p5(f3(f3(c7)),v)* -> p5(u,v)*. % 1.26/1.46 6231[0:Res:2.0,1851.0] || p5(f3(f3(c7)),u)* -> p5(c7,u). % 1.26/1.46 6236[0:Res:88.1,6231.0] || p2(f3(f4(c7)),u)* -> p5(c7,u). % 1.26/1.46 6309[0:Res:994.1,6236.0] || p2(f4(c7),f4(c7)) -> p5(c7,f3(f4(c8)))*. % 1.26/1.46 6311[0:MRR:6309.0,1.0] || -> p5(c7,f3(f4(c8)))*. % 1.26/1.46 6313[0:Res:6311.0,10.0] || -> p6(f4(c7),f3(f4(c8)))*r. % 1.26/1.46 6315[0:MRR:6313.0,5.0] || -> . % 1.26/1.46 % SZS output end Refutation % 1.26/1.46 Formulae used in the proof : p2_1 p6_2 p2_4 not_p6_5 p5_7 p6_9 p6_10 p2_11 p2_13 p6_14 p5_15 p5_17 % 1.26/1.46 %------------------------------------------------------------------------------