%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : PUZ028-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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 : Mon Jul 18 18:27:19 EDT 2022 % Result : Satisfiable 0.19s 0.41s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ028-1 : TPTP v8.1.0. Released v1.0.0. % 0.12/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n029.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 : Sat May 28 20:40:27 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.41 % 0.19/0.41 SPASS V 3.9 % 0.19/0.41 SPASS beiseite: Completion found. % 0.19/0.41 % SZS status CounterSatisfiable % 0.19/0.41 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.41 SPASS derived 80 clauses, backtracked 0 clauses, performed 8 splits and kept 93 clauses. % 0.19/0.41 SPASS allocated 75690 KBytes. % 0.19/0.41 SPASS spent 0:00:00.06 on the problem. % 0.19/0.41 0:00:00.04 for the input. % 0.19/0.41 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.41 0:00:00.00 for inferences. % 0.19/0.41 0:00:00.00 for the backtracking. % 0.19/0.41 0:00:00.01 for the reduction. % 0.19/0.41 % 0.19/0.41 % 0.19/0.41 The saturated set of worked-off clauses is : % 0.19/0.41 % SZS output start Saturation % 0.19/0.41 12[0:Inp] || after(u,v)* after(v,w)* -> after(u,w)*. % 0.19/0.41 119[0:NCh:12.2,12.0,107.1,11.0] person(u) || after(six,u)+ -> not_familiar(one,u)* familiar(one,u). % 0.19/0.41 121[0:Res:120.0,15.0] || not_familiar(u,one)*+ not_familiar(six,u)* -> familiar(one,six). % 0.19/0.41 120[0:SSi:118.0,6.0] || -> not_familiar(one,six)* familiar(one,six). % 0.19/0.41 115[0:NCh:12.2,12.0,89.1,11.0] person(u) || after(six,u)+ -> not_familiar(two,u)* familiar(two,u). % 0.19/0.41 107[0:NCh:12.2,12.0,81.1,10.0] person(u) || after(five,u)+ -> not_familiar(one,u)* familiar(one,u). % 0.19/0.41 117[0:Res:116.0,15.0] || not_familiar(u,two)*+ not_familiar(six,u)* -> familiar(two,six). % 0.19/0.41 109[0:Res:108.0,15.0] || not_familiar(u,one)*+ not_familiar(five,u)* -> familiar(one,five). % 0.19/0.41 96[0:Res:95.0,15.0] || not_familiar(u,three)*+ not_familiar(six,u)* -> familiar(three,six). % 0.19/0.41 94[0:NCh:12.2,12.0,64.1,11.0] person(u) || after(six,u)+ -> not_familiar(three,u)* familiar(three,u). % 0.19/0.41 91[0:Res:90.0,15.0] || not_familiar(u,two)*+ not_familiar(five,u)* -> familiar(two,five). % 0.19/0.41 83[0:Res:82.0,15.0] || not_familiar(u,one)*+ not_familiar(four,u)* -> familiar(one,four). % 0.19/0.41 116[0:SSi:114.0,6.0] || -> not_familiar(two,six)* familiar(two,six). % 0.19/0.41 113[8:Res:102.0,111.0] || familiar(six,two)*+ -> . % 0.19/0.41 89[0:NCh:12.2,12.0,55.1,10.0] person(u) || after(five,u)+ -> not_familiar(two,u)* familiar(two,u). % 0.19/0.41 112[8:Res:69.0,111.0] || familiar(six,three)*+ -> . % 0.19/0.41 111[8:Res:110.0,14.0] || familiar(u,four)*+ familiar(six,u)* -> . % 0.19/0.41 110[8:Spt:101.2] || -> familiar(four,six)*. % 0.19/0.41 108[0:SSi:106.0,5.0] || -> not_familiar(one,five)* familiar(one,five). % 0.19/0.41 81[0:NCh:12.2,12.0,48.1,9.0] person(u) || after(four,u)+ -> not_familiar(one,u)* familiar(one,u). % 0.19/0.41 103[7:Res:102.0,14.0] || familiar(u,two)*+ familiar(four,u)* -> . % 0.19/0.41 104[7:Res:102.0,61.0] || familiar(five,two)*+ -> . % 0.19/0.41 102[7:Spt:100.1] || -> familiar(two,four)*. % 0.19/0.41 73[0:NCh:12.2,12.0,40.1,11.0] person(u) || after(six,u)+ -> not_familiar(four,u)* familiar(four,u). % 0.19/0.41 98[6:Res:97.0,14.0] || familiar(u,one)*+ familiar(three,u)* -> . % 0.19/0.41 99[6:Res:97.0,70.0] || familiar(four,one)*+ -> . % 0.19/0.41 97[6:Spt:92.1] || -> familiar(one,three)*. % 0.19/0.41 95[0:SSi:93.0,6.0] || -> not_familiar(three,six)* familiar(three,six). % 0.19/0.41 64[0:NCh:12.2,12.0,39.1,10.0] person(u) || after(five,u)+ -> not_familiar(three,u)* familiar(three,u). % 0.19/0.41 66[0:Res:65.0,15.0] || not_familiar(u,three)*+ not_familiar(five,u)* -> familiar(three,five). % 0.19/0.41 86[5:Res:85.0,14.0] || familiar(u,one)*+ familiar(two,u)* -> . % 0.19/0.41 90[0:SSi:88.0,5.0] || -> not_familiar(two,five)* familiar(two,five). % 0.19/0.41 87[5:Res:85.0,78.0] || familiar(three,one)*+ -> . % 0.19/0.41 55[0:NCh:12.2,12.0,38.1,9.0] person(u) || after(four,u)+ -> not_familiar(two,u)* familiar(two,u). % 0.19/0.41 85[5:Spt:84.1] || -> familiar(one,two)*. % 0.19/0.41 82[0:SSi:80.0,4.0] || -> not_familiar(one,four)* familiar(one,four). % 0.19/0.41 48[0:NCh:12.2,12.0,37.1,8.0] person(u) || after(three,u)+ -> not_familiar(one,u)* familiar(one,u). % 0.19/0.41 78[4:Res:77.0,14.0] || familiar(u,two)*+ familiar(three,u)* -> . % 0.19/0.41 79[4:Res:77.0,70.0] || familiar(four,two)*+ -> . % 0.19/0.41 77[4:Spt:76.2] || -> familiar(two,three)*. % 0.19/0.41 41[0:SSi:27.1,5.0] person(u) || after(six,u)+ -> not_familiar(five,u)* familiar(five,u). % 0.19/0.41 70[3:Res:69.0,14.0] || familiar(u,three)*+ familiar(four,u)* -> . % 0.19/0.41 71[3:Res:69.0,61.0] || familiar(five,three)*+ -> . % 0.19/0.41 40[0:SSi:28.1,4.0] person(u) || after(five,u)+ -> not_familiar(four,u)* familiar(four,u). % 0.19/0.41 69[3:Spt:67.2] || -> familiar(three,four)*. % 0.19/0.41 61[2:Res:60.0,14.0] || familiar(u,four)*+ familiar(five,u)* -> . % 0.19/0.41 65[0:SSi:63.0,5.0] || -> not_familiar(three,five)* familiar(three,five). % 0.19/0.41 39[0:SSi:29.1,3.0] person(u) || after(four,u)+ -> not_familiar(three,u)* familiar(three,u). % 0.19/0.41 62[2:Res:60.0,53.0] || familiar(six,four)*+ -> . % 0.19/0.41 60[2:Spt:58.2] || -> familiar(four,five)*. % 0.19/0.41 38[0:SSi:30.1,2.0] person(u) || after(three,u)+ -> not_familiar(two,u)* familiar(two,u). % 0.19/0.41 53[1:Res:52.0,14.0] || familiar(u,five)*+ familiar(six,u)* -> . % 0.19/0.41 52[1:Spt:51.2] || -> familiar(five,six)*. % 0.19/0.41 37[0:SSi:31.1,1.0] person(u) || after(two,u)+ -> not_familiar(one,u)* familiar(one,u). % 0.19/0.41 13[0:Inp] person(u) person(v) || after(v,u)+ -> not_familiar(v,u)* familiar(v,u). % 0.19/0.41 14[0:Inp] || familiar(u,v)*+ familiar(w,u)* familiar(v,w)* -> . % 0.19/0.41 15[0:Inp] || not_familiar(u,v)*+ not_familiar(w,u)* not_familiar(v,w)* -> . % 0.19/0.41 7[0:Inp] || -> after(one,two)*l. % 0.19/0.41 8[0:Inp] || -> after(two,three)*l. % 0.19/0.41 9[0:Inp] || -> after(three,four)*l. % 0.19/0.41 10[0:Inp] || -> after(four,five)*l. % 0.19/0.41 11[0:Inp] || -> after(five,six)*l. % 0.19/0.41 1[0:Inp] || -> person(one)*. % 0.19/0.41 2[0:Inp] || -> person(two)*. % 0.19/0.41 3[0:Inp] || -> person(three)*. % 0.19/0.41 4[0:Inp] || -> person(four)*. % 0.19/0.41 5[0:Inp] || -> person(five)*. % 0.19/0.41 6[0:Inp] || -> person(six)*. % 0.19/0.41 % SZS output end Saturation %------------------------------------------------------------------------------