%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN393+1.003 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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:21:03 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.03/0.12 % Problem : SYN393+1.003 : TPTP v8.1.0. Released v2.0.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n028.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 21:43:59 EDT 2022 % 0.12/0.33 % 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 34 clauses, backtracked 67 clauses, performed 7 splits and kept 91 clauses. % 0.19/0.43 SPASS allocated 85082 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 86 : % 0.19/0.43 % SZS output start Refutation % 0.19/0.43 1[0:Inp] || -> SkC0* p2 p1. % 0.19/0.43 2[0:Inp] || -> SkC1* p3 p2. % 0.19/0.43 3[0:Inp] || -> SkC1* p1 p3 SkC0. % 0.19/0.43 4[0:Inp] || SkC0* p1 -> p2. % 0.19/0.43 5[0:Inp] || SkC0* p2 -> p1. % 0.19/0.43 6[0:Inp] || p2 p1 -> SkC0*. % 0.19/0.43 7[0:Inp] || SkC1* p2 -> p3. % 0.19/0.43 8[0:Inp] || SkC1* p3 -> p2. % 0.19/0.43 9[0:Inp] || p3 p2 -> SkC1*. % 0.19/0.43 10[0:Inp] || SkC1* p3 -> p1 SkC0. % 0.19/0.43 11[0:Inp] || p1 p3 -> SkC1* SkC0. % 0.19/0.43 12[0:Inp] || SkC0 SkC1* -> p3 p1. % 0.19/0.43 13[0:Inp] || p1 SkC0 -> SkC1* p3. % 0.19/0.43 14[0:Inp] || p3 SkC0 -> SkC1* p1. % 0.19/0.43 15[0:Inp] || SkC1* p1 -> p3 SkC0. % 0.19/0.43 16[0:Inp] || SkC1* p1 p3 SkC0 -> . % 0.19/0.43 17[1:Spt:3.0] || -> SkC1*. % 0.19/0.43 18[1:MRR:8.0,17.0] || p3* -> p2. % 0.19/0.43 19[1:MRR:7.0,17.0] || p2 -> p3*. % 0.19/0.43 20[1:MRR:15.0,17.0] || p1 -> p3 SkC0*. % 0.19/0.43 21[1:MRR:12.1,17.0] || SkC0* -> p3 p1. % 0.19/0.43 22[1:MRR:10.0,17.0] || p3 -> p1 SkC0*. % 0.19/0.43 23[1:MRR:16.0,17.0] || p1 p3 SkC0* -> . % 0.19/0.43 24[2:Spt:1.0] || -> SkC0*. % 0.19/0.43 25[2:MRR:5.0,24.0] || p2* -> p1. % 0.19/0.43 26[2:MRR:4.0,24.0] || p1 -> p2*. % 0.19/0.43 27[2:MRR:21.0,24.0] || -> p3* p1. % 0.19/0.43 28[2:MRR:23.2,24.0] || p1 p3* -> . % 0.19/0.43 29[3:Spt:27.0] || -> p3*. % 0.19/0.43 30[3:MRR:18.0,29.0] || -> p2*. % 0.19/0.43 31[3:MRR:28.1,29.0] || p1* -> . % 0.19/0.43 32[3:MRR:25.0,30.0] || -> p1*. % 0.19/0.43 33[3:MRR:31.0,32.0] || -> . % 0.19/0.43 34[3:Spt:33.0,27.0,29.0] || p3* -> . % 0.19/0.43 35[3:Spt:33.0,27.1] || -> p1*. % 0.19/0.43 36[3:MRR:19.1,34.0] || p2* -> . % 0.19/0.43 37[3:MRR:26.0,26.1,35.0,36.0] || -> . % 0.19/0.43 38[2:Spt:37.0,1.0,24.0] || SkC0* -> . % 0.19/0.43 39[2:Spt:37.0,1.1,1.2] || -> p2* p1. % 0.19/0.43 40[2:MRR:20.2,38.0] || p1 -> p3*. % 0.19/0.43 41[2:MRR:22.2,38.0] || p3* -> p1. % 0.19/0.43 42[2:MRR:6.2,38.0] || p2* p1 -> . % 0.19/0.43 43[3:Spt:39.0] || -> p2*. % 0.19/0.43 44[3:MRR:19.0,43.0] || -> p3*. % 0.19/0.43 45[3:MRR:42.0,43.0] || p1* -> . % 0.19/0.43 46[3:MRR:41.0,44.0] || -> p1*. % 0.19/0.43 47[3:MRR:45.0,46.0] || -> . % 0.19/0.43 48[3:Spt:47.0,39.0,43.0] || p2* -> . % 0.19/0.43 49[3:Spt:47.0,39.1] || -> p1*. % 0.19/0.43 50[3:MRR:18.1,48.0] || p3* -> . % 0.19/0.43 51[3:MRR:40.0,40.1,49.0,50.0] || -> . % 0.19/0.43 52[1:Spt:51.0,3.0,17.0] || SkC1*+ -> . % 0.19/0.43 53[1:Spt:51.0,3.1,3.2,3.3] || -> p1 p3 SkC0*. % 0.19/0.43 54[1:MRR:2.0,52.0] || -> p3* p2. % 0.19/0.43 55[1:MRR:9.2,52.0] || p3* p2 -> . % 0.19/0.43 56[1:MRR:14.2,52.0] || p3 SkC0* -> p1. % 0.19/0.43 57[1:MRR:13.2,52.0] || p1 SkC0* -> p3. % 0.19/0.43 58[1:MRR:11.2,52.0] || p1 p3 -> SkC0*. % 0.19/0.43 59[2:Spt:53.0] || -> p1*. % 0.19/0.43 60[2:MRR:6.1,59.0] || p2 -> SkC0*. % 0.19/0.43 61[2:MRR:4.1,59.0] || SkC0* -> p2. % 0.19/0.43 62[2:MRR:57.0,59.0] || SkC0* -> p3. % 0.19/0.43 63[2:MRR:58.0,59.0] || p3 -> SkC0*. % 0.19/0.43 64[3:Spt:54.0] || -> p3*. % 0.19/0.43 65[3:MRR:55.0,64.0] || p2* -> . % 0.19/0.43 66[3:MRR:63.0,64.0] || -> SkC0*. % 0.19/0.43 67[3:MRR:61.0,66.0] || -> p2*. % 0.19/0.43 68[3:MRR:65.0,67.0] || -> . % 0.19/0.43 69[3:Spt:68.0,54.0,64.0] || p3* -> . % 0.19/0.43 70[3:Spt:68.0,54.1] || -> p2*. % 0.19/0.43 71[3:MRR:62.1,69.0] || SkC0* -> . % 0.19/0.43 72[3:MRR:60.0,60.1,70.0,71.0] || -> . % 0.19/0.43 73[2:Spt:72.0,53.0,59.0] || p1* -> . % 0.19/0.43 74[2:Spt:72.0,53.1,53.2] || -> p3 SkC0*. % 0.19/0.43 75[2:MRR:1.2,73.0] || -> SkC0* p2. % 0.19/0.43 76[2:MRR:5.2,73.0] || SkC0* p2 -> . % 0.19/0.43 77[2:MRR:56.2,73.0] || p3 SkC0* -> . % 0.19/0.43 78[3:Spt:74.0] || -> p3*. % 0.19/0.43 79[3:MRR:55.0,78.0] || p2* -> . % 0.19/0.43 80[3:MRR:77.0,78.0] || SkC0* -> . % 0.19/0.43 81[3:MRR:75.1,79.0] || -> SkC0*. % 0.19/0.43 82[3:MRR:80.0,81.0] || -> . % 0.19/0.43 83[3:Spt:82.0,74.0,78.0] || p3* -> . % 0.19/0.43 84[3:Spt:82.0,74.1] || -> SkC0*. % 0.19/0.43 85[3:MRR:54.0,83.0] || -> p2*. % 0.19/0.43 86[3:MRR:76.0,76.1,84.0,85.0] || -> . % 0.19/0.43 % SZS output end Refutation % 0.19/0.43 Formulae used in the proof : pel12 % 0.19/0.43 %------------------------------------------------------------------------------