%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN059+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n003.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:17:46 EDT 2022 % Result : Theorem 0.19s 0.43s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN059+1 : TPTP v8.1.0. Released v2.0.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n003.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 Jul 12 00:28:00 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.43 % 0.19/0.43 SPASS V 3.9 % 0.19/0.43 SPASS beiseite: Proof found. % 0.19/0.43 % SZS status Theorem % 0.19/0.43 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.43 SPASS derived 16 clauses, backtracked 9 clauses, performed 2 splits and kept 30 clauses. % 0.19/0.43 SPASS allocated 97586 KBytes. % 0.19/0.43 SPASS spent 0:00:00.08 on the problem. % 0.19/0.43 0:00:00.03 for the input. % 0.19/0.43 0:00:00.02 for the FLOTTER CNF translation. % 0.19/0.43 0:00:00.00 for inferences. % 0.19/0.43 0:00:00.00 for the backtracking. % 0.19/0.43 0:00:00.00 for the reduction. % 0.19/0.43 % 0.19/0.43 % 0.19/0.43 Here is a proof with depth 3, length 35 : % 0.19/0.43 % SZS output start Refutation % 0.19/0.43 1[0:Inp] || -> big_g(skc9)*. % 0.19/0.43 2[0:Inp] || -> big_f(skc8)*. % 0.19/0.43 3[0:Inp] || -> big_f(skc7)*. % 0.19/0.43 4[0:Inp] || -> big_g(skc6)*. % 0.19/0.43 7[0:Inp] big_f(u) || SkC0+ -> big_h(u)*. % 0.19/0.43 8[0:Inp] big_g(u) || SkC0+ -> big_j(u)*. % 0.19/0.43 9[0:Inp] || big_j(skc9)*+ big_h(skc8) -> SkC0. % 0.19/0.43 10[0:Inp] || SkC0 big_j(skc6)* big_h(skc7) -> . % 0.19/0.43 11[0:Inp] big_f(u) big_g(v) || -> big_h(u)* SkC0. % 0.19/0.43 12[0:Inp] big_f(u) big_g(v) || -> big_j(v)* SkC0. % 0.19/0.43 13[0:MRR:12.3,8.1] big_g(u) big_f(v) || -> big_j(u)*. % 0.19/0.43 14[0:MRR:11.3,7.1] big_g(u) big_f(v) || -> big_h(v)*. % 0.19/0.43 25[1:Spt:8.0,8.2] big_g(u) || -> big_j(u)*. % 0.19/0.43 26[2:Spt:7.0,7.2] big_f(u) || -> big_h(u)*. % 0.19/0.43 27[1:Res:25.1,9.0] big_g(skc9) || big_h(skc8)* -> SkC0. % 0.19/0.43 28[1:SSi:27.0,1.0] || big_h(skc8)*+ -> SkC0. % 0.19/0.43 29[2:Res:26.1,28.0] big_f(skc8) || -> SkC0*. % 0.19/0.43 30[2:SSi:29.0,2.0] || -> SkC0*. % 0.19/0.43 31[2:MRR:10.0,30.0] || big_j(skc6)*+ big_h(skc7) -> . % 0.19/0.43 32[2:Res:25.1,31.0] big_g(skc6) || big_h(skc7)* -> . % 0.19/0.43 33[2:SSi:32.0,4.0] || big_h(skc7)*+ -> . % 0.19/0.43 34[2:Res:26.1,33.0] big_f(skc7) || -> . % 0.19/0.43 35[2:SSi:34.0,3.0] || -> . % 0.19/0.43 36[2:Spt:35.0,7.1] || SkC0*+ -> . % 0.19/0.43 37[2:MRR:28.1,36.0] || big_h(skc8)*+ -> . % 0.19/0.43 38[0:EmS:14.0,1.0] big_f(u) || -> big_h(u)*. % 0.19/0.43 41[2:Res:38.1,37.0] big_f(skc8) || -> . % 0.19/0.43 42[2:SSi:41.0,2.0] || -> . % 0.19/0.43 43[1:Spt:42.0,8.1] || SkC0*+ -> . % 0.19/0.43 44[1:MRR:9.2,43.0] || big_j(skc9)*+ big_h(skc8) -> . % 0.19/0.43 45[0:EmS:13.1,2.0] big_g(u) || -> big_j(u)*. % 0.19/0.43 48[1:Res:45.1,44.0] big_g(skc9) || big_h(skc8)* -> . % 0.19/0.43 49[1:SSi:48.0,1.0] || big_h(skc8)*+ -> . % 0.19/0.43 50[1:Res:38.1,49.0] big_f(skc8) || -> . % 0.19/0.43 51[1:SSi:50.0,2.0] || -> . % 0.19/0.43 % SZS output end Refutation % 0.19/0.43 Formulae used in the proof : pel29 pel29_2 pel29_1 % 0.19/0.43 %------------------------------------------------------------------------------