%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN037-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:26 EDT 2022 % Result : Unsatisfiable 0.20s 0.43s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYN037-1 : TPTP v8.1.0. Released v1.0.0. % 0.08/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n013.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon Jul 11 23:09:14 EDT 2022 % 0.13/0.35 % CPUTime : % 0.20/0.43 % 0.20/0.43 SPASS V 3.9 % 0.20/0.43 SPASS beiseite: Proof found. % 0.20/0.43 % SZS status Theorem % 0.20/0.43 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.43 SPASS derived 143 clauses, backtracked 296 clauses, performed 11 splits and kept 416 clauses. % 0.20/0.43 SPASS allocated 75676 KBytes. % 0.20/0.43 SPASS spent 0:00:00.07 on the problem. % 0.20/0.43 0:00:00.03 for the input. % 0.20/0.43 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.43 0:00:00.00 for inferences. % 0.20/0.43 0:00:00.00 for the backtracking. % 0.20/0.43 0:00:00.01 for the reduction. % 0.20/0.43 % 0.20/0.43 % 0.20/0.43 Here is a proof with depth 2, length 204 : % 0.20/0.43 % SZS output start Refutation % 0.20/0.43 1[0:Inp] || n10* n6 n9 n2 -> . % 0.20/0.43 2[0:Inp] || n9 n2 -> n10* n6. % 0.20/0.43 3[0:Inp] || n10* n6 -> n9 n2. % 0.20/0.43 4[0:Inp] || -> n10* n6 n9 n2. % 0.20/0.43 5[0:Inp] || n6 n2 -> n10* n9. % 0.20/0.43 6[0:Inp] || n10* n2 -> n6 n9. % 0.20/0.43 7[0:Inp] || n6 n9 -> n10* n2. % 0.20/0.43 9[0:Inp] || q(s8)* -> n8. % 0.20/0.43 10[0:Inp] || n8 -> q(u)*. % 0.20/0.43 11[0:Inp] p(u) || -> n7*. % 0.20/0.43 12[0:Inp] || n7 -> p(s7)*. % 0.20/0.43 13[0:Inp] n5(u) || -> n6*. % 0.20/0.43 14[0:Inp] || n6 -> n5(s6)*. % 0.20/0.43 15[0:Inp] q(u) || q(s5(u))* -> n5(u). % 0.20/0.43 16[0:Inp] || -> n5(u) q(u) q(s5(u))*. % 0.20/0.43 17[0:Inp] q(u) n5(v) || -> q(v)*. % 0.20/0.43 18[0:Inp] q(u) n5(u) || -> q(v)*. % 0.20/0.43 19[0:Inp] || p(s4)* -> n4. % 0.20/0.43 20[0:Inp] || n4 -> p(u)*. % 0.20/0.43 21[0:Inp] q(u) || -> n3*. % 0.20/0.43 22[0:Inp] || n3 -> q(s3)*. % 0.20/0.43 23[0:Inp] n1(u) || -> n2*. % 0.20/0.43 24[0:Inp] || n2 -> n1(s2)*. % 0.20/0.43 25[0:Inp] p(u) || p(s1(u))* -> n1(u). % 0.20/0.43 26[0:Inp] || -> n1(u) p(u) p(s1(u))*. % 0.20/0.43 27[0:Inp] p(u) n1(u) || -> p(v)*. % 0.20/0.43 28[0:Inp] p(u) n1(v) || -> p(v)*. % 0.20/0.43 29[0:Inp] || n4 n3* -> n9. % 0.20/0.43 30[0:Inp] || -> n9 n4 n3*. % 0.20/0.43 31[0:Inp] || n9 n3* -> n4. % 0.20/0.43 32[0:Inp] || n9 n4 -> n3*. % 0.20/0.43 33[0:Inp] || n8 n7* -> n10. % 0.20/0.43 34[0:Inp] || -> n10 n8 n7*. % 0.20/0.43 35[0:Inp] || n10 n7* -> n8. % 0.20/0.43 36[0:Inp] || n10 n8 -> n7*. % 0.20/0.43 55[1:Spt:5.2] || -> n10*. % 0.20/0.43 56[1:MRR:36.0,55.0] || n8 -> n7*. % 0.20/0.43 57[1:MRR:35.0,55.0] || n7* -> n8. % 0.20/0.43 59[1:MRR:6.0,55.0] || n2 -> n6* n9. % 0.20/0.43 60[1:MRR:3.0,55.0] || n6* -> n9 n2. % 0.20/0.43 61[1:MRR:1.0,55.0] || n6* n9 n2 -> . % 0.20/0.43 62[2:Spt:30.0] || -> n9*. % 0.20/0.43 64[2:MRR:31.0,62.0] || n3* -> n4. % 0.20/0.43 66[2:MRR:61.1,62.0] || n6* n2 -> . % 0.20/0.43 67[3:Spt:20.1] || -> p(u)*. % 0.20/0.43 68[3:MRR:11.0,67.0] || -> n7*. % 0.20/0.43 69[3:MRR:25.1,25.0,67.0] || -> n1(u)*. % 0.20/0.43 71[3:MRR:57.0,68.0] || -> n8*. % 0.20/0.43 73[3:MRR:10.0,71.0] || -> q(u)*. % 0.20/0.43 75[3:MRR:23.0,69.0] || -> n2*. % 0.20/0.43 76[3:MRR:66.1,75.0] || n6* -> . % 0.20/0.43 77[3:MRR:15.1,15.0,73.0] || -> n5(u)*. % 0.20/0.43 78[3:MRR:13.1,76.0] n5(u) || -> . % 0.20/0.43 79[3:MRR:78.0,77.0] || -> . % 0.20/0.43 80[3:Spt:79.0,20.0] || n4* -> . % 0.20/0.43 81[3:MRR:64.1,80.0] || n3* -> . % 0.20/0.43 83[3:MRR:21.1,81.0] q(u) || -> . % 0.20/0.43 84[3:MRR:10.1,83.0] || n8* -> . % 0.20/0.43 85[3:MRR:57.1,84.0] || n7* -> . % 0.20/0.43 87[3:MRR:11.1,85.0] p(u) || -> . % 0.20/0.43 88[3:MRR:26.1,26.2,87.0,87.0] || -> n1(u)*. % 0.20/0.43 89[3:MRR:23.0,88.0] || -> n2*. % 0.20/0.43 90[3:MRR:66.1,89.0] || n6* -> . % 0.20/0.43 91[3:MRR:13.1,90.0] n5(u) || -> . % 0.20/0.43 92[3:MRR:16.0,16.1,16.2,91.0,83.0,83.0] || -> . % 0.20/0.43 93[2:Spt:92.0,30.0,62.0] || n9* -> . % 0.20/0.43 94[2:Spt:92.0,30.1,30.2] || -> n4 n3*. % 0.20/0.43 95[2:MRR:59.2,93.0] || n2 -> n6*. % 0.20/0.43 96[2:MRR:60.1,93.0] || n6* -> n2. % 0.20/0.43 97[2:MRR:29.2,93.0] || n4 n3* -> . % 0.20/0.43 98[3:Spt:94.0] || -> n4*. % 0.20/0.43 99[3:MRR:20.0,98.0] || -> p(u)*. % 0.20/0.43 100[3:MRR:97.0,98.0] || n3* -> . % 0.20/0.43 101[3:MRR:11.0,99.0] || -> n7*. % 0.20/0.43 103[3:MRR:57.0,101.0] || -> n8*. % 0.20/0.43 104[3:MRR:10.0,103.0] || -> q(u)*. % 0.20/0.43 105[3:MRR:21.1,100.0] q(u) || -> . % 0.20/0.43 110[3:MRR:105.0,104.0] || -> . % 0.20/0.43 111[3:Spt:110.0,94.0,98.0] || n4* -> . % 0.20/0.43 112[3:Spt:110.0,94.1] || -> n3*. % 0.20/0.43 113[3:MRR:19.1,111.0] || p(s4)* -> . % 0.20/0.43 114[3:MRR:22.0,112.0] || -> q(s3)*. % 0.20/0.43 115[4:Spt:10.1] || -> q(u)*. % 0.20/0.43 116[4:MRR:9.0,115.0] || -> n8*. % 0.20/0.43 117[4:MRR:15.1,15.0,115.0] || -> n5(u)*. % 0.20/0.43 118[4:MRR:56.0,116.0] || -> n7*. % 0.20/0.43 119[4:MRR:12.0,118.0] || -> p(s7)*. % 0.20/0.43 120[4:MRR:13.0,117.0] || -> n6*. % 0.20/0.43 121[4:MRR:96.0,120.0] || -> n2*. % 0.20/0.43 122[4:MRR:24.0,121.0] || -> n1(s2)*. % 0.20/0.43 123[0:EmS:28.0,26.2] n1(u) || -> p(u)* p(v) n1(v)*. % 0.20/0.43 124[4:EmS:28.0,119.0] n1(u) || -> p(u)*. % 0.20/0.43 126[4:MRR:27.0,124.1] n1(u) || -> p(v)*. % 0.20/0.43 127[4:EmS:126.0,122.0] || -> p(u)*. % 0.20/0.43 128[4:UnC:127.0,113.0] || -> . % 0.20/0.43 129[4:Spt:128.0,10.0] || n8* -> . % 0.20/0.43 130[4:MRR:57.1,129.0] || n7* -> . % 0.20/0.43 131[4:MRR:9.1,129.0] || q(s8)* -> . % 0.20/0.43 132[4:MRR:11.1,130.0] p(u) || -> . % 0.20/0.43 133[4:MRR:26.1,26.2,132.0,132.0] || -> n1(u)*. % 0.20/0.43 134[4:MRR:23.0,133.0] || -> n2*. % 0.20/0.43 135[4:MRR:95.0,134.0] || -> n6*. % 0.20/0.43 136[4:MRR:14.0,135.0] || -> n5(s6)*. % 0.20/0.43 137[0:EmS:17.0,16.2] n5(u) || -> q(u)* q(v) n5(v)*. % 0.20/0.43 138[3:EmS:17.0,114.0] n5(u) || -> q(u)*. % 0.20/0.43 140[3:MRR:18.0,138.1] n5(u) || -> q(v)*. % 0.20/0.43 141[4:EmS:140.0,136.0] || -> q(u)*. % 0.20/0.43 142[4:UnC:141.0,131.0] || -> . % 0.20/0.43 143[1:Spt:142.0,5.2,55.0] || n10* -> . % 0.20/0.43 144[1:Spt:142.0,5.0,5.1,5.3] || n6* n2 -> n9. % 0.20/0.43 145[1:MRR:34.0,143.0] || -> n8 n7*. % 0.20/0.43 146[1:MRR:4.0,143.0] || -> n6* n9 n2. % 0.20/0.43 147[1:MRR:33.2,143.0] || n8 n7* -> . % 0.20/0.43 148[1:MRR:7.2,143.0] || n6* n9 -> n2. % 0.20/0.43 149[1:MRR:2.2,143.0] || n9 n2 -> n6*. % 0.20/0.43 150[0:MRR:123.1,27.0] n1(u) || -> p(v) n1(v)*. % 0.20/0.43 151[0:MRR:137.1,18.0] n5(u) || -> q(v) n5(v)*. % 0.20/0.43 152[2:Spt:30.0] || -> n9*. % 0.20/0.43 153[2:MRR:31.0,152.0] || n3* -> n4. % 0.20/0.43 154[2:MRR:32.0,152.0] || n4 -> n3*. % 0.20/0.43 155[2:MRR:148.1,152.0] || n6* -> n2. % 0.20/0.43 156[2:MRR:149.0,152.0] || n2 -> n6*. % 0.20/0.43 157[3:Spt:10.1] || -> q(u)*. % 0.20/0.43 159[3:MRR:21.0,157.0] || -> n3*. % 0.20/0.43 160[3:MRR:9.0,157.0] || -> n8*. % 0.20/0.43 161[3:MRR:153.0,159.0] || -> n4*. % 0.20/0.43 162[3:MRR:147.0,160.0] || n7* -> . % 0.20/0.43 163[3:MRR:20.0,161.0] || -> p(u)*. % 0.20/0.43 167[3:MRR:11.1,162.0] p(u) || -> . % 0.20/0.43 169[3:MRR:167.0,163.0] || -> . % 0.20/0.43 170[3:Spt:169.0,10.0] || n8* -> . % 0.20/0.43 171[3:MRR:145.0,170.0] || -> n7*. % 0.20/0.43 172[3:MRR:9.1,170.0] || q(s8)* -> . % 0.20/0.43 173[3:MRR:12.0,171.0] || -> p(s7)*. % 0.20/0.43 174[4:Spt:20.1] || -> p(u)*. % 0.20/0.43 175[4:MRR:19.0,174.0] || -> n4*. % 0.20/0.43 176[4:MRR:25.1,25.0,174.0] || -> n1(u)*. % 0.20/0.43 177[4:MRR:154.0,175.0] || -> n3*. % 0.20/0.43 178[4:MRR:22.0,177.0] || -> q(s3)*. % 0.20/0.43 179[4:MRR:23.0,176.0] || -> n2*. % 0.20/0.43 180[4:MRR:156.0,179.0] || -> n6*. % 0.20/0.43 181[4:MRR:14.0,180.0] || -> n5(s6)*. % 0.20/0.43 182[4:EmS:151.0,181.0] || -> q(u) n5(u)*. % 0.20/0.43 184[4:MRR:17.1,182.1] q(u) || -> q(v)*. % 0.20/0.43 185[4:EmS:184.0,178.0] || -> q(u)*. % 0.20/0.43 186[4:UnC:185.0,172.0] || -> . % 0.20/0.43 187[4:Spt:186.0,20.0] || n4* -> . % 0.20/0.43 188[4:MRR:153.1,187.0] || n3* -> . % 0.20/0.43 189[4:MRR:19.1,187.0] || p(s4)* -> . % 0.20/0.43 190[4:MRR:21.1,188.0] q(u) || -> . % 0.20/0.43 191[4:MRR:16.1,16.2,190.0,190.0] || -> n5(u)*. % 0.20/0.43 192[4:MRR:13.0,191.0] || -> n6*. % 0.20/0.43 193[4:MRR:155.0,192.0] || -> n2*. % 0.20/0.43 194[4:MRR:24.0,193.0] || -> n1(s2)*. % 0.20/0.43 196[3:EmS:28.0,173.0] n1(u) || -> p(u)*. % 0.20/0.43 198[3:MRR:150.2,196.0] n1(u) || -> p(v)*. % 0.20/0.43 200[4:EmS:198.0,194.0] || -> p(u)*. % 0.20/0.43 201[4:UnC:200.0,189.0] || -> . % 0.20/0.43 202[2:Spt:201.0,30.0,152.0] || n9* -> . % 0.20/0.43 203[2:Spt:201.0,30.1,30.2] || -> n4 n3*. % 0.20/0.43 204[2:MRR:146.1,202.0] || -> n6* n2. % 0.20/0.43 205[2:MRR:144.2,202.0] || n6* n2 -> . % 0.20/0.43 206[2:MRR:29.2,202.0] || n4 n3* -> . % 0.20/0.43 207[3:Spt:203.0] || -> n4*. % 0.20/0.43 208[3:MRR:20.0,207.0] || -> p(u)*. % 0.20/0.43 209[3:MRR:206.0,207.0] || n3* -> . % 0.20/0.43 210[3:MRR:25.1,25.0,208.0] || -> n1(u)*. % 0.20/0.43 213[3:MRR:21.1,209.0] q(u) || -> . % 0.20/0.43 214[3:MRR:23.0,210.0] || -> n2*. % 0.20/0.43 215[3:MRR:205.1,214.0] || n6* -> . % 0.20/0.43 217[3:MRR:13.1,215.0] n5(u) || -> . % 0.20/0.43 218[3:MRR:16.2,16.1,213.0] || -> n5(u)*. % 0.20/0.43 220[3:MRR:217.0,218.0] || -> . % 0.20/0.43 221[3:Spt:220.0,203.0,207.0] || n4* -> . % 0.20/0.43 222[3:Spt:220.0,203.1] || -> n3*. % 0.20/0.43 223[3:MRR:19.1,221.0] || p(s4)* -> . % 0.20/0.43 224[3:MRR:22.0,222.0] || -> q(s3)*. % 0.20/0.43 225[4:Spt:10.1] || -> q(u)*. % 0.20/0.43 226[4:MRR:15.1,15.0,225.0] || -> n5(u)*. % 0.20/0.43 227[4:MRR:9.0,225.0] || -> n8*. % 0.20/0.43 228[4:MRR:147.0,227.0] || n7* -> . % 0.20/0.43 229[4:MRR:13.0,226.0] || -> n6*. % 0.20/0.43 230[4:MRR:205.0,229.0] || n2* -> . % 0.20/0.43 231[4:MRR:11.1,228.0] p(u) || -> . % 0.20/0.43 232[4:MRR:23.1,230.0] n1(u) || -> . % 0.20/0.43 233[4:MRR:26.2,26.1,231.0] || -> n1(u)*. % 0.20/0.43 235[4:MRR:232.0,233.0] || -> . % 0.20/0.43 236[4:Spt:235.0,10.0] || n8* -> . % 0.20/0.43 237[4:MRR:145.0,236.0] || -> n7*. % 0.20/0.43 238[4:MRR:9.1,236.0] || q(s8)* -> . % 0.20/0.43 239[4:MRR:12.0,237.0] || -> p(s7)*. % 0.20/0.43 240[5:Spt:14.0] || n6* -> . % 0.20/0.43 241[5:MRR:204.0,240.0] || -> n2*. % 0.20/0.43 243[5:MRR:24.0,241.0] || -> n1(s2)*. % 0.20/0.43 247[5:EmS:150.0,243.0] || -> p(u) n1(u)*. % 0.20/0.43 249[5:MRR:28.1,247.1] p(u) || -> p(v)*. % 0.20/0.43 250[5:EmS:249.0,239.0] || -> p(u)*. % 0.20/0.43 251[5:UnC:250.0,223.0] || -> . % 0.20/0.43 252[5:Spt:251.0,14.0,240.0] || -> n6*. % 0.20/0.43 253[5:Spt:251.0,14.1] || -> n5(s6)*. % 0.20/0.43 259[5:EmS:151.0,253.0] || -> q(u) n5(u)*. % 0.20/0.43 261[5:MRR:17.1,259.1] q(u) || -> q(v)*. % 0.20/0.43 262[5:EmS:261.0,224.0] || -> q(u)*. % 0.20/0.43 263[5:UnC:262.0,238.0] || -> . % 0.20/0.43 % SZS output end Refutation % 0.20/0.43 Formulae used in the proof : clause_1 clause_2 clause_3 clause_4 clause_5 clause_6 clause_7 clause_9 clause_10 clause_11 clause_12 clause_13 clause_14 clause_15 clause_16 clause_17 clause_18 clause_19 clause_20 clause_21 clause_22 clause_23 clause_24 clause_25 clause_26 clause_27 clause_28 clause_29 clause_30 clause_31 clause_32 clause_33 clause_34 clause_35 clause_36 % 0.20/0.43 %------------------------------------------------------------------------------