%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRA001-1 : TPTP v8.1.0. Released v1.0.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 : Sat Jul 16 07:22:08 EDT 2022 % Result : Unsatisfiable 0.20s 0.42s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRA001-1 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n025.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Tue May 31 02:57:42 EDT 2022 % 0.14/0.34 % CPUTime : % 0.20/0.42 % 0.20/0.42 SPASS V 3.9 % 0.20/0.42 SPASS beiseite: Proof found. % 0.20/0.42 % SZS status Theorem % 0.20/0.42 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.42 SPASS derived 16 clauses, backtracked 31 clauses, performed 3 splits and kept 47 clauses. % 0.20/0.42 SPASS allocated 63099 KBytes. % 0.20/0.42 SPASS spent 0:00:00.06 on the problem. % 0.20/0.42 0:00:00.04 for the input. % 0.20/0.42 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.42 0:00:00.00 for inferences. % 0.20/0.42 0:00:00.00 for the backtracking. % 0.20/0.42 0:00:00.00 for the reduction. % 0.20/0.42 % 0.20/0.42 % 0.20/0.42 Here is a proof with depth 1, length 44 : % 0.20/0.42 % SZS output start Refutation % 0.20/0.42 1[0:Inp] || -> b* a. % 0.20/0.42 2[0:Inp] || b* a -> . % 0.20/0.42 3[0:Inp] || d* -> c a. % 0.20/0.42 4[0:Inp] || c -> d* a. % 0.20/0.42 5[0:Inp] || a -> d* c. % 0.20/0.42 6[0:Inp] || d* c a -> . % 0.20/0.42 7[0:Inp] || e*+ -> c b. % 0.20/0.42 8[0:Inp] || c -> e* b. % 0.20/0.42 9[0:Inp] || b -> e* c. % 0.20/0.42 10[0:Inp] || e* c b -> . % 0.20/0.42 11[0:Inp] || e* -> d. % 0.20/0.42 12[0:Inp] || d -> e*. % 0.20/0.42 13[1:Spt:7.1] || -> c*. % 0.20/0.42 14[1:MRR:8.0,13.0] || -> e* b. % 0.20/0.42 15[1:MRR:4.0,13.0] || -> d* a. % 0.20/0.42 16[1:MRR:10.1,13.0] || e* b -> . % 0.20/0.42 17[1:MRR:6.1,13.0] || d* a -> . % 0.20/0.42 18[2:Spt:1.0] || -> b*. % 0.20/0.42 19[2:MRR:2.0,18.0] || a* -> . % 0.20/0.42 20[2:MRR:16.1,18.0] || e* -> . % 0.20/0.42 21[2:MRR:15.1,19.0] || -> d*. % 0.20/0.42 22[2:MRR:12.0,21.0] || -> e*. % 0.20/0.42 23[2:MRR:20.0,22.0] || -> . % 0.20/0.42 24[2:Spt:23.0,1.0,18.0] || b* -> . % 0.20/0.42 25[2:Spt:23.0,1.1] || -> a*. % 0.20/0.42 26[2:MRR:14.1,24.0] || -> e*. % 0.20/0.42 27[2:MRR:11.0,26.0] || -> d*. % 0.20/0.42 28[2:MRR:17.0,17.1,27.0,25.0] || -> . % 0.20/0.42 29[1:Spt:28.0,7.1,13.0] || c* -> . % 0.20/0.42 30[1:Spt:28.0,7.0,7.2] || e*+ -> b. % 0.20/0.42 31[1:MRR:9.2,29.0] || b -> e*. % 0.20/0.42 32[1:MRR:5.2,29.0] || a -> d*. % 0.20/0.42 33[1:MRR:3.1,29.0] || d* -> a. % 0.20/0.42 34[2:Spt:1.0] || -> b*. % 0.20/0.42 35[2:MRR:2.0,34.0] || a* -> . % 0.20/0.42 36[2:MRR:31.0,34.0] || -> e*. % 0.20/0.42 37[2:MRR:11.0,36.0] || -> d*. % 0.20/0.42 38[2:MRR:33.0,37.0] || -> a*. % 0.20/0.42 39[2:MRR:35.0,38.0] || -> . % 0.20/0.42 40[2:Spt:39.0,1.0,34.0] || b* -> . % 0.20/0.42 41[2:Spt:39.0,1.1] || -> a*. % 0.20/0.42 42[2:MRR:30.1,40.0] || e* -> . % 0.20/0.42 43[2:MRR:12.1,42.0] || d* -> . % 0.20/0.42 44[2:MRR:32.0,32.1,41.0,43.0] || -> . % 0.20/0.42 % SZS output end Refutation % 0.20/0.42 Formulae used in the proof : clause_1 clause_2 clause_3 clause_4 clause_5 clause_6 clause_7 clause_8 clause_9 clause_10 clause_11 clause_12 % 0.20/0.42 %------------------------------------------------------------------------------