%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN036-3 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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:25 EDT 2022 % Result : Unsatisfiable 0.19s 0.43s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYN036-3 : TPTP v8.1.0. Released v1.0.0. % 0.04/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n024.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 : Mon Jul 11 14:29:58 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 131 clauses, backtracked 270 clauses, performed 13 splits and kept 372 clauses. % 0.19/0.43 SPASS allocated 75676 KBytes. % 0.19/0.43 SPASS spent 0:00:00.07 on the problem. % 0.19/0.43 0:00:00.04 for the input. % 0.19/0.43 0:00:00.00 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.01 for the reduction. % 0.19/0.43 % 0.19/0.43 % 0.19/0.43 Here is a proof with depth 2, length 172 : % 0.19/0.43 % SZS output start Refutation % 0.19/0.43 1[0:Inp] || n10* n6 n9 n2 -> . % 0.19/0.43 4[0:Inp] || -> n10* n6 n9 n2. % 0.19/0.43 5[0:Inp] || n6 n2 -> n10* n9. % 0.19/0.43 6[0:Inp] || n10* n2 -> n6 n9. % 0.19/0.43 7[0:Inp] || n6 n9 -> n10* n2. % 0.19/0.43 9[0:Inp] || p(s8)* -> n8. % 0.19/0.43 10[0:Inp] || n8 -> p(u)*. % 0.19/0.43 11[0:Inp] p(u) || -> n7*. % 0.19/0.43 12[0:Inp] || n7 -> p(s7)*. % 0.19/0.43 13[0:Inp] n5(u) || -> n6*. % 0.19/0.43 14[0:Inp] || n6 -> n5(s6)*. % 0.19/0.43 15[0:Inp] q(u) || q(s5(u))* -> n5(u). % 0.19/0.43 16[0:Inp] || -> n5(u) q(u) q(s5(u))*. % 0.19/0.43 17[0:Inp] q(u) n5(u) || -> q(v)*. % 0.19/0.43 18[0:Inp] q(u) n5(v) || -> q(v)*. % 0.19/0.43 19[0:Inp] || q(s4)* -> n4. % 0.19/0.43 20[0:Inp] || n4 -> q(u)*. % 0.19/0.43 21[0:Inp] q(u) || -> n3*. % 0.19/0.43 22[0:Inp] || n3 -> q(s3)*. % 0.19/0.43 23[0:Inp] n1(u) || -> n2*. % 0.19/0.43 24[0:Inp] || n2 -> n1(s2)*. % 0.19/0.43 25[0:Inp] p(u) || p(s1(u))* -> n1(u). % 0.19/0.43 26[0:Inp] || -> n1(u) p(u) p(s1(u))*. % 0.19/0.43 27[0:Inp] p(u) n1(u) || -> p(v)*. % 0.19/0.43 28[0:Inp] p(u) n1(v) || -> p(v)*. % 0.19/0.43 29[0:Inp] || n4 n3* -> n9. % 0.19/0.43 30[0:Inp] || -> n9 n4 n3*. % 0.19/0.43 31[0:Inp] || n9 n3* -> n4. % 0.19/0.43 33[0:Inp] || n8 n7* -> n10. % 0.19/0.43 34[0:Inp] || -> n10 n8 n7*. % 0.19/0.43 35[0:Inp] || n10 n7* -> n8. % 0.19/0.43 55[1:Spt:5.2] || -> n10*. % 0.19/0.43 57[1:MRR:35.0,55.0] || n7* -> n8. % 0.19/0.43 59[1:MRR:6.0,55.0] || n2 -> n6* n9. % 0.19/0.43 61[1:MRR:1.0,55.0] || n6* n9 n2 -> . % 0.19/0.43 62[2:Spt:30.0] || -> n9*. % 0.19/0.43 64[2:MRR:31.0,62.0] || n3* -> n4. % 0.19/0.43 66[2:MRR:61.1,62.0] || n6* n2 -> . % 0.19/0.43 67[3:Spt:20.1] || -> q(u)*. % 0.19/0.43 69[3:MRR:15.1,15.0,67.0] || -> n5(u)*. % 0.19/0.43 72[3:MRR:13.0,69.0] || -> n6*. % 0.19/0.43 73[3:MRR:66.0,72.0] || n2* -> . % 0.19/0.43 74[3:MRR:23.1,73.0] n1(u) || -> . % 0.19/0.43 75[3:MRR:26.0,74.0] || -> p(u) p(s1(u))*. % 0.19/0.43 76[3:MRR:25.2,74.0] p(u) || p(s1(u))* -> . % 0.19/0.43 77[4:Spt:10.1] || -> p(u)*. % 0.19/0.43 79[4:MRR:76.1,76.0,77.0] || -> . % 0.19/0.43 82[4:Spt:79.0,10.0] || n8* -> . % 0.19/0.43 83[4:MRR:57.1,82.0] || n7* -> . % 0.19/0.43 85[4:MRR:11.1,83.0] p(u) || -> . % 0.19/0.43 86[4:MRR:75.0,75.1,85.0,85.0] || -> . % 0.19/0.43 87[3:Spt:86.0,20.0] || n4* -> . % 0.19/0.43 88[3:MRR:64.1,87.0] || n3* -> . % 0.19/0.43 90[3:MRR:21.1,88.0] q(u) || -> . % 0.19/0.43 91[3:MRR:16.1,16.2,90.0,90.0] || -> n5(u)*. % 0.19/0.43 92[3:MRR:13.0,91.0] || -> n6*. % 0.19/0.43 93[3:MRR:66.0,92.0] || n2* -> . % 0.19/0.43 94[3:MRR:23.1,93.0] n1(u) || -> . % 0.19/0.43 95[3:MRR:26.0,94.0] || -> p(u) p(s1(u))*. % 0.19/0.43 96[3:MRR:25.2,94.0] p(u) || p(s1(u))* -> . % 0.19/0.43 97[4:Spt:10.1] || -> p(u)*. % 0.19/0.43 100[4:MRR:96.1,96.0,97.0] || -> . % 0.19/0.43 102[4:Spt:100.0,10.0] || n8* -> . % 0.19/0.43 103[4:MRR:57.1,102.0] || n7* -> . % 0.19/0.43 104[4:MRR:11.1,103.0] p(u) || -> . % 0.19/0.43 106[4:MRR:95.0,95.1,104.0,104.0] || -> . % 0.19/0.43 107[2:Spt:106.0,30.0,62.0] || n9* -> . % 0.19/0.43 108[2:Spt:106.0,30.1,30.2] || -> n4 n3*. % 0.19/0.43 109[2:MRR:59.2,107.0] || n2 -> n6*. % 0.19/0.43 111[2:MRR:29.2,107.0] || n4 n3* -> . % 0.19/0.43 112[3:Spt:108.0] || -> n4*. % 0.19/0.43 113[3:MRR:20.0,112.0] || -> q(u)*. % 0.19/0.43 114[3:MRR:111.0,112.0] || n3* -> . % 0.19/0.43 115[3:MRR:21.0,113.0] || -> n3*. % 0.19/0.43 117[3:MRR:114.0,115.0] || -> . % 0.19/0.43 121[3:Spt:117.0,108.0,112.0] || n4* -> . % 0.19/0.43 122[3:Spt:117.0,108.1] || -> n3*. % 0.19/0.43 123[3:MRR:19.1,121.0] || q(s4)* -> . % 0.19/0.43 124[3:MRR:22.0,122.0] || -> q(s3)*. % 0.19/0.43 125[4:Spt:10.1] || -> p(u)*. % 0.19/0.43 127[4:MRR:25.1,25.0,125.0] || -> n1(u)*. % 0.19/0.43 130[4:MRR:23.0,127.0] || -> n2*. % 0.19/0.43 131[4:MRR:109.0,130.0] || -> n6*. % 0.19/0.43 132[4:MRR:14.0,131.0] || -> n5(s6)*. % 0.19/0.43 133[0:EmS:18.0,16.2] n5(u) || -> q(u)* q(v)* n5(v). % 0.19/0.43 134[3:EmS:18.0,124.0] n5(u) || -> q(u)*. % 0.19/0.43 136[3:MRR:17.0,134.1] n5(u) || -> q(v)*. % 0.19/0.43 137[4:EmS:136.0,132.0] || -> q(u)*. % 0.19/0.43 138[4:UnC:137.0,123.0] || -> . % 0.19/0.43 139[4:Spt:138.0,10.0] || n8* -> . % 0.19/0.43 140[4:MRR:57.1,139.0] || n7* -> . % 0.19/0.43 142[4:MRR:11.1,140.0] p(u) || -> . % 0.19/0.43 143[4:MRR:26.1,26.2,142.0,142.0] || -> n1(u)*. % 0.19/0.43 144[4:MRR:23.0,143.0] || -> n2*. % 0.19/0.43 145[4:MRR:109.0,144.0] || -> n6*. % 0.19/0.43 146[4:MRR:14.0,145.0] || -> n5(s6)*. % 0.19/0.43 147[4:EmS:136.0,146.0] || -> q(u)*. % 0.19/0.43 148[4:UnC:147.0,123.0] || -> . % 0.19/0.43 149[1:Spt:148.0,5.2,55.0] || n10* -> . % 0.19/0.43 150[1:Spt:148.0,5.0,5.1,5.3] || n6* n2 -> n9. % 0.19/0.43 151[1:MRR:34.0,149.0] || -> n8 n7*. % 0.19/0.43 152[1:MRR:4.0,149.0] || -> n6* n9 n2. % 0.19/0.43 153[1:MRR:33.2,149.0] || n8 n7* -> . % 0.19/0.43 154[1:MRR:7.2,149.0] || n6* n9 -> n2. % 0.19/0.43 156[0:MRR:133.1,17.0] n5(u) || -> q(v)* n5(v). % 0.19/0.43 157[2:Spt:30.0] || -> n9*. % 0.19/0.43 158[2:MRR:31.0,157.0] || n3* -> n4. % 0.19/0.43 160[2:MRR:154.1,157.0] || n6* -> n2. % 0.19/0.43 162[3:Spt:10.1] || -> p(u)*. % 0.19/0.43 163[3:MRR:9.0,162.0] || -> n8*. % 0.19/0.43 164[3:MRR:11.0,162.0] || -> n7*. % 0.19/0.43 166[3:MRR:153.0,163.0] || n7* -> . % 0.19/0.43 170[3:MRR:166.0,164.0] || -> . % 0.19/0.43 171[3:Spt:170.0,10.0] || n8* -> . % 0.19/0.43 172[3:MRR:151.0,171.0] || -> n7*. % 0.19/0.43 173[3:MRR:12.0,172.0] || -> p(s7)*. % 0.19/0.43 174[3:MRR:9.1,171.0] || p(s8)* -> . % 0.19/0.43 175[4:Spt:20.1] || -> q(u)*. % 0.19/0.43 176[4:MRR:15.1,15.0,175.0] || -> n5(u)*. % 0.19/0.43 180[4:MRR:13.0,176.0] || -> n6*. % 0.19/0.43 181[4:MRR:160.0,180.0] || -> n2*. % 0.19/0.43 182[4:MRR:24.0,181.0] || -> n1(s2)*. % 0.19/0.43 183[0:EmS:28.0,26.2] n1(u) || -> p(u)* p(v) n1(v)*. % 0.19/0.43 184[3:EmS:28.0,173.0] n1(u) || -> p(u)*. % 0.19/0.43 186[3:MRR:27.0,184.1] n1(u) || -> p(v)*. % 0.19/0.43 187[4:EmS:186.0,182.0] || -> p(u)*. % 0.19/0.43 188[4:UnC:187.0,174.0] || -> . % 0.19/0.43 189[4:Spt:188.0,20.0] || n4* -> . % 0.19/0.43 190[4:MRR:158.1,189.0] || n3* -> . % 0.19/0.43 192[4:MRR:21.1,190.0] q(u) || -> . % 0.19/0.43 193[4:MRR:16.1,16.2,192.0,192.0] || -> n5(u)*. % 0.19/0.43 194[4:MRR:13.0,193.0] || -> n6*. % 0.19/0.43 195[4:MRR:160.0,194.0] || -> n2*. % 0.19/0.43 196[4:MRR:24.0,195.0] || -> n1(s2)*. % 0.19/0.43 197[4:EmS:186.0,196.0] || -> p(u)*. % 0.19/0.43 198[4:UnC:197.0,174.0] || -> . % 0.19/0.43 199[2:Spt:198.0,30.0,157.0] || n9* -> . % 0.19/0.43 200[2:Spt:198.0,30.1,30.2] || -> n4 n3*. % 0.19/0.43 201[2:MRR:152.1,199.0] || -> n6* n2. % 0.19/0.43 203[2:MRR:29.2,199.0] || n4 n3* -> . % 0.19/0.43 204[0:MRR:183.1,27.0] n1(u) || -> p(v) n1(v)*. % 0.19/0.43 205[3:Spt:200.0] || -> n4*. % 0.19/0.43 206[3:MRR:20.0,205.0] || -> q(u)*. % 0.19/0.43 207[3:MRR:203.0,205.0] || n3* -> . % 0.19/0.43 208[3:MRR:21.0,206.0] || -> n3*. % 0.19/0.43 210[3:MRR:207.0,208.0] || -> . % 0.19/0.43 216[3:Spt:210.0,200.0,205.0] || n4* -> . % 0.19/0.43 217[3:Spt:210.0,200.1] || -> n3*. % 0.19/0.43 218[3:MRR:19.1,216.0] || q(s4)* -> . % 0.19/0.43 219[3:MRR:22.0,217.0] || -> q(s3)*. % 0.19/0.43 220[4:Spt:10.1] || -> p(u)*. % 0.19/0.43 221[4:MRR:11.0,220.0] || -> n7*. % 0.19/0.43 223[4:MRR:9.0,220.0] || -> n8*. % 0.19/0.43 224[4:MRR:153.1,221.0] || n8* -> . % 0.19/0.43 227[4:MRR:224.0,223.0] || -> . % 0.19/0.43 231[4:Spt:227.0,10.0] || n8* -> . % 0.19/0.43 232[4:MRR:151.0,231.0] || -> n7*. % 0.19/0.43 233[4:MRR:12.0,232.0] || -> p(s7)*. % 0.19/0.43 234[4:MRR:9.1,231.0] || p(s8)* -> . % 0.19/0.43 235[5:Spt:24.0] || n2* -> . % 0.19/0.43 236[5:MRR:201.1,235.0] || -> n6*. % 0.19/0.43 238[5:MRR:14.0,236.0] || -> n5(s6)*. % 0.19/0.43 242[5:EmS:156.0,238.0] || -> q(u)* n5(u). % 0.19/0.43 244[5:MRR:18.1,242.1] q(u) || -> q(v)*. % 0.19/0.43 247[5:EmS:244.0,219.0] || -> q(u)*. % 0.19/0.43 248[5:UnC:247.0,218.0] || -> . % 0.19/0.43 250[5:Spt:248.0,24.0,235.0] || -> n2*. % 0.19/0.43 251[5:Spt:248.0,24.1] || -> n1(s2)*. % 0.19/0.43 257[5:EmS:204.0,251.0] || -> p(u) n1(u)*. % 0.19/0.43 259[5:MRR:28.1,257.1] p(u) || -> p(v)*. % 0.19/0.43 260[5:EmS:259.0,233.0] || -> p(u)*. % 0.19/0.43 261[5:UnC:260.0,234.0] || -> . % 0.19/0.43 % SZS output end Refutation % 0.19/0.43 Formulae used in the proof : clause_1 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_33 clause_34 clause_35 % 0.19/0.43 %------------------------------------------------------------------------------