%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR039+1 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 : 300s
% DateTime : Thu May 7 07:19:41 PM UTC 2026
% Result : Theorem 0.38s 0.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.18 % Problem : CSR039+1 : TPTP v9.2.1. Released v3.4.0.
% 0.11/0.19 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.40 % Computer : n014.cluster.edu
% 0.17/0.40 % Model : x86_64 x86_64
% 0.17/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.40 % Memory : 8042.1875MB
% 0.17/0.40 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.40 % CPULimit : 300
% 0.17/0.40 % WCLimit : 300
% 0.17/0.40 % DateTime : Thu May 7 11:38:17 EDT 2026
% 0.17/0.41 % CPUTime :
% 0.17/0.41 SPASS-SCL-FOL version:
% 0.23/0.50 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.38/0.86 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.86 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.86 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.86 Execution resolution_1 ended with status: unsatisfiable
% 0.38/0.86 Used heuristic: resolution_1
% 0.38/0.86
% 0.38/0.86 Input Clauses:
% 0.38/0.86
% 0.38/0.86 Predicates: genlmt transitivebinarypredicate genls tptpcol_2_2 tptpcol_1_1 tptpcol_3_16386 tptpcol_4_16387 tptpcol_5_16388 tptpcol_6_18436 tptpcol_7_18437 tptpcol_8_18438 tptpcol_9_18439 tptpcol_10_18567 tptpcol_11_18631 tptpcol_12_18663 tptpcol_13_18664 tptpcol_2_65537 tptpcol_1_65536 tptpcol_3_81921 tptpcol_4_90113 tptpcol_5_90114 tptpcol_6_92162 tptpcol_7_93186 tptpcol_8_93698 tptpcol_9_93699 tptpcol_10_93700 tptpcol_11_93764 tptpcol_12_93765 tptpcol_13_93766 tptpcol_14_93774 tptpcol_15_93775 disjointwith isa genlinverse genlpreds predicate binarypredicate collection natfunction natargument uniformresourcelocator computerdataartifact microtheory thing mtvisible
% 0.38/0.86 Fol Constants: c_cycorpproductsmt c_basekb c_cycnounlearnermt c_genlmt s_http_wwwpoweripodsearchinfobrown_ipodhtml c_translation_7 c_machinelearningspindleheadmt c_universalvocabularymt c_tptpcol_2_2 c_tptpcol_1_1 c_tptpcol_3_16386 c_tptpcol_4_16387 c_tptpcol_5_16388 c_tptpcol_6_18436 c_tptpcol_7_18437 c_tptpcol_8_18438 c_tptpcol_9_18439 c_tptpcol_10_18567 c_tptpcol_11_18631 c_tptpcol_12_18663 c_tptpcol_13_18664 c_tptpcol_2_65537 c_tptpcol_1_65536 c_tptpcol_3_81921 c_tptpcol_4_90113 c_tptpcol_5_90114 c_tptpcol_6_92162 c_tptpcol_7_93186 c_tptpcol_8_93698 c_tptpcol_9_93699 c_tptpcol_10_93700 c_tptpcol_11_93764 c_tptpcol_12_93765 c_tptpcol_13_93766 c_tptpcol_14_93774 c_tptpcol_15_93775 c_urlfn n_1 c_urlreferentfn c_contentmtofcdafromeventfn n_2 c_transitivebinarypredicate
% 0.38/0.86 Fol Functions: f_urlfn f_urlreferentfn f_contentmtofcdafromeventfn
% 0.38/0.86 Problem Properties:
% 0.38/0.86 This is a full first-order problem without equality.
% 0.38/0.86
% 0.38/0.86 After reduction: Problem Properties:
% 0.38/0.86 This is a full first-order problem without equality.
% 0.38/0.86
% 0.38/0.86
% 0.38/0.86 Reduced Input Clauses:
% 0.38/0.86
% 0.38/0.86 Most General Atoms: tptpcol_2_2(x0) tptpcol_1_1(x0) tptpcol_3_16386(x0) tptpcol_4_16387(x0) tptpcol_5_16388(x0) tptpcol_6_18436(x0) tptpcol_7_18437(x0) tptpcol_8_18438(x0) tptpcol_9_18439(x0) tptpcol_10_18567(x0) tptpcol_11_18631(x0) tptpcol_12_18663(x0) tptpcol_13_18664(x0) tptpcol_2_65537(x0) tptpcol_1_65536(x0) tptpcol_3_81921(x0) tptpcol_4_90113(x0) tptpcol_5_90114(x0) tptpcol_6_92162(x0) tptpcol_7_93186(x0) tptpcol_8_93698(x0) tptpcol_9_93699(x0) tptpcol_10_93700(x0) tptpcol_11_93764(x0) tptpcol_12_93765(x0) tptpcol_13_93766(x0) tptpcol_14_93774(x0) tptpcol_15_93775(x0) isa(x0,x2) predicate(x0) binarypredicate(x0) genlpreds(x2,x0) genlinverse(x0,x2) collection(x0) disjointwith(x2,x1) genlmt(x0,x2) microtheory(x1) mtvisible(x1) genls(x0,x2) natfunction(f_urlfn(x0),c_urlfn) natargument(f_urlfn(x0),n_1,x0) uniformresourcelocator(f_urlfn(x0)) natfunction(f_urlreferentfn(x0),c_urlreferentfn) natargument(f_urlreferentfn(x0),n_1,x0) computerdataartifact(f_urlreferentfn(x0)) natfunction(f_contentmtofcdafromeventfn(x0,x1),c_contentmtofcdafromeventfn) natargument(f_contentmtofcdafromeventfn(x0,x1),n_1,x0) natargument(f_contentmtofcdafromeventfn(x0,x1),n_2,x1) transitivebinarypredicate(x0) thing(x0)
% 0.38/0.86
% 0.38/0.86 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_1 ===
% 0.38/0.86
% 0.38/0.86 === Backtracking. Learning clause 173:2:1:[32.2,60.2]:Top: tptpcol_2_65537(x0),tptpcol_1_1(x0) ->
% 0.38/0.86 === Backtracking. Learning clause 174:1:0:[74.1,59.1]:: -> collection(c_tptpcol_1_65536)
% 0.38/0.86 === Backtracking. Learning clause 175:1:0:[75.1,59.1]:: -> collection(c_tptpcol_1_1)
% 0.38/0.86 === Backtracking. Learning clause 176:1:0:[76.2,172.1]:: disjointwith(c_tptpcol_13_18664,c_tptpcol_15_93775) ->
% 0.38/0.86 === Backtracking. Learning clause 177:3:3:[62.3,64.1]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2) -> predicate(x2)
% 0.38/0.86 === Clause set with instances from active satisfied. Growing active. New size: 114
% 0.38/0.86 === Restarting.
% 0.38/0.86 === Clause set with instances from active satisfied. Growing active. New size: 178
% 0.38/0.86 === Restarting.
% 0.38/0.86 === Backtracking. Learning clause 178:1:0:[138.1,9.1]:: -> collection(c_tptpcol_3_16386)
% 0.38/0.86 === Backtracking. Learning clause 179:1:0:[138.1,11.1]:: -> collection(c_tptpcol_4_16387)
% 0.38/0.86 === Backtracking. Learning clause 180:1:0:[138.1,13.1]:: -> collection(c_tptpcol_5_16388)
% 0.38/0.86 === Backtracking. Learning clause 181:1:0:[138.1,17.1]:: -> collection(c_tptpcol_7_18437)
% 0.38/0.86 === Backtracking. Learning clause 182:1:0:[138.1,27.1]:: -> collection(c_tptpcol_12_18663)
% 0.38/0.86 === Backtracking. Learning clause 183:1:0:[138.1,31.1]:: -> collection(c_tptpcol_2_65537)
% 0.38/0.86 === Backtracking. Learning clause 184:1:0:[138.1,47.1]:: -> collection(c_tptpcol_10_93700)
% 0.38/0.86 === Backtracking. Learning clause 185:1:0:[138.1,55.1]:: -> collection(c_tptpcol_14_93774)
% 0.38/0.86 === Clause set with instances from active satisfied. Growing active. New size: 254
% 0.38/0.86 === Restarting.
% 0.38/0.86 === Backtracking. Learning clause 186:1:0:[166.1,2.1]:: -> microtheory(c_cycnounlearnermt)
% 0.38/0.86 === Backtracking. Learning clause 187:1:0:[166.1,5.1]:: -> microtheory(c_machinelearningspindleheadmt)
% 0.38/0.86 === Backtracking. Learning clause 188:2:0:[167.1,5.1,162.2,2.1]:: mtvisible(c_machinelearningspindleheadmt) -> mtvisible(c_cycorpproductsmt)
% 0.38/0.86 === Backtracking. Learning clause 189:2:1:[167.1,5.1]:Top: genlmt(c_cycnounlearnermt,x0) -> genlmt(c_machinelearningspindleheadmt,x0)
% 0.38/0.86 === Backtracking. Learning clause 190:1:0:[138.1,7.1]:: -> collection(c_tptpcol_2_2)
% 0.38/0.86 === Backtracking. Learning clause 191:1:0:[138.1,15.1]:: -> collection(c_tptpcol_6_18436)
% 0.38/0.86 === Backtracking. Learning clause 192:1:0:[138.1,29.1]:: -> collection(c_tptpcol_13_18664)
% 0.38/0.86 === Backtracking. Learning clause 193:1:0:[138.1,39.1]:: -> collection(c_tptpcol_6_92162)
% 0.38/0.86 === Backtracking. Learning clause 194:1:0:[138.1,41.1]:: -> collection(c_tptpcol_7_93186)
% 0.38/0.86 === Backtracking. Learning clause 195:1:0:[138.1,43.1]:: -> collection(c_tptpcol_8_93698)
% 0.38/0.86 === Backtracking. Learning clause 196:1:0:[138.1,45.1]:: -> collection(c_tptpcol_9_93699)
% 0.38/0.86 === Backtracking. Learning clause 197:1:0:[138.1,51.1]:: -> collection(c_tptpcol_12_93765)
% 0.38/0.86 === Backtracking. Learning clause 198:1:0:[138.1,57.1]:: -> collection(c_tptpcol_15_93775)
% 0.38/0.86 === Backtracking. Learning clause 199:1:0:[167.1,4.1,162.2,171.1,189.2,2.1]:: -> mtvisible(c_cycorpproductsmt)
% 0.38/0.86 === Backtracking. Learning clause 200:2:0:[162.2,5.1]:: mtvisible(c_machinelearningspindleheadmt) -> mtvisible(c_cycnounlearnermt)
% 0.38/0.86 === Backtracking. Learning clause 201:1:0:[162.2,4.1,171.1,200.1]:: -> mtvisible(c_cycnounlearnermt)
% 0.38/0.86 === Clause set with instances from active satisfied. Growing active. New size: 264
% 0.38/0.86 === Restarting.
% 0.38/0.86 === Backtracking. Learning clause 202:1:0:[164.1,1.1]:: -> microtheory(c_basekb)
% 0.38/0.86 === Backtracking. Learning clause 203:2:1:[143.2,7.1]:Top: genls(x0,c_tptpcol_2_2) -> genls(x0,c_tptpcol_1_1)
% 0.38/0.86 === Backtracking. Learning clause 204:2:1:[143.1,11.1]:Top: genls(c_tptpcol_3_16386,x0) -> genls(c_tptpcol_4_16387,x0)
% 0.38/0.86 === Backtracking. Learning clause 205:2:1:[143.1,13.1]:Top: genls(c_tptpcol_4_16387,x0) -> genls(c_tptpcol_5_16388,x0)
% 0.38/0.86 === Backtracking. Learning clause 206:2:1:[143.2,13.1]:Top: genls(x0,c_tptpcol_5_16388) -> genls(x0,c_tptpcol_4_16387)
% 0.38/0.86 === Backtracking. Learning clause 207:2:1:[143.1,15.1]:Top: genls(c_tptpcol_5_16388,x0) -> genls(c_tptpcol_6_18436,x0)
% 0.38/0.86 === Backtracking. Learning clause 208:2:1:[143.2,15.1]:Top: genls(x0,c_tptpcol_6_18436) -> genls(x0,c_tptpcol_5_16388)
% 0.38/0.86 === Backtracking. Learning clause 209:2:1:[143.1,17.1]:Top: genls(c_tptpcol_6_18436,x0) -> genls(c_tptpcol_7_18437,x0)
% 0.38/0.86 === Backtracking. Learning clause 210:2:1:[143.1,19.1,138.1,209.2,207.2,205.2,204.2]:Top: genls(c_tptpcol_3_16386,x0) -> collection(c_tptpcol_8_18438)
% 0.38/0.86 === Conflict found: 210:2:1:[143.1,19.1,138.1,209.2,207.2,205.2,204.2]:Top: genls(c_tptpcol_3_16386,x0) -> collection(c_tptpcol_8_18438) {x0 -> c_tptpcol_2_2}
% 0.38/0.86 === Backtracking. Learning clause 211:1:0:[210.1,9.1]:: -> collection(c_tptpcol_8_18438)
% 0.38/0.86 === Backtracking. Learning clause 212:2:1:[143.1,19.1]:Top: genls(c_tptpcol_7_18437,x0) -> genls(c_tptpcol_8_18438,x0)
% 0.38/0.86 === Backtracking. Learning clause 213:2:1:[143.2,19.1]:Top: genls(x0,c_tptpcol_8_18438) -> genls(x0,c_tptpcol_7_18437)
% 0.38/0.86 === Backtracking. Learning clause 214:2:1:[143.1,21.1]:Top: genls(c_tptpcol_8_18438,x0) -> genls(c_tptpcol_9_18439,x0)
% 0.38/0.86 === Backtracking. Learning clause 215:2:1:[143.2,21.1]:Top: genls(x0,c_tptpcol_9_18439) -> genls(x0,c_tptpcol_8_18438)
% 0.38/0.86 === Backtracking. Learning clause 216:2:1:[143.1,23.1]:Top: genls(c_tptpcol_9_18439,x0) -> genls(c_tptpcol_10_18567,x0)
% 0.38/0.86 === Backtracking. Learning clause 217:2:1:[143.1,25.1]:Top: genls(c_tptpcol_10_18567,x0) -> genls(c_tptpcol_11_18631,x0)
% 0.38/0.86 === Backtracking. Learning clause 218:2:1:[143.2,29.1]:Top: genls(x0,c_tptpcol_13_18664) -> genls(x0,c_tptpcol_12_18663)
% 0.38/0.86 === Backtracking. Learning clause 219:2:1:[143.1,29.1]:Top: genls(c_tptpcol_12_18663,x0) -> genls(c_tptpcol_13_18664,x0)
% 0.38/0.86 === Backtracking. Learning clause 220:1:0:[138.1,33.1]:: -> collection(c_tptpcol_3_81921)
% 0.38/0.86 === Backtracking. Learning clause 221:2:1:[143.1,37.1]:Top: genls(c_tptpcol_4_90113,x0) -> genls(c_tptpcol_5_90114,x0)
% 0.38/0.86 === Backtracking. Learning clause 222:2:1:[143.1,39.1]:Top: genls(c_tptpcol_5_90114,x0) -> genls(c_tptpcol_6_92162,x0)
% 0.38/0.86 === Backtracking. Learning clause 223:2:1:[143.1,41.1]:Top: genls(c_tptpcol_6_92162,x0) -> genls(c_tptpcol_7_93186,x0)
% 0.38/0.86 === Backtracking. Learning clause 224:2:1:[143.2,41.1]:Top: genls(x0,c_tptpcol_7_93186) -> genls(x0,c_tptpcol_6_92162)
% 0.38/0.86 === Backtracking. Learning clause 225:2:1:[143.1,43.1]:Top: genls(c_tptpcol_7_93186,x0) -> genls(c_tptpcol_8_93698,x0)
% 0.38/0.86 === Backtracking. Learning clause 226:2:1:[143.2,45.1]:Top: genls(x0,c_tptpcol_9_93699) -> genls(x0,c_tptpcol_8_93698)
% 0.38/0.86 === Backtracking. Learning clause 227:2:1:[143.1,47.1]:Top: genls(c_tptpcol_9_93699,x0) -> genls(c_tptpcol_10_93700,x0)
% 0.38/0.86 === Backtracking. Learning clause 228:2:1:[143.2,47.1]:Top: genls(x0,c_tptpcol_10_93700) -> genls(x0,c_tptpcol_9_93699)
% 0.38/0.86 === Backtracking. Learning clause 229:2:1:[143.2,49.1]:Top: genls(x0,c_tptpcol_11_93764) -> genls(x0,c_tptpcol_10_93700)
% 0.38/0.86 === Backtracking. Learning clause 230:2:1:[143.2,51.1]:Top: genls(x0,c_tptpcol_12_93765) -> genls(x0,c_tptpcol_11_93764)
% 0.38/0.86 === Backtracking. Learning clause 231:2:1:[143.1,53.1,138.1]:Top: genls(c_tptpcol_12_93765,x0) -> collection(c_tptpcol_13_93766)
% 0.38/0.86 === Backtracking. Learning clause 232:2:1:[143.1,51.1,231.1]:Top: genls(c_tptpcol_11_93764,x0) -> collection(c_tptpcol_13_93766)
% 0.38/0.86 === Backtracking. Learning clause 233:2:1:[143.1,49.1,232.1,227.2]:Top: genls(c_tptpcol_9_93699,x0) -> collection(c_tptpcol_13_93766)
% 0.38/0.86 === Backtracking. Learning clause 234:2:1:[143.1,45.1,233.1,225.2,223.2,222.2,221.2]:Top: genls(c_tptpcol_4_90113,x0) -> collection(c_tptpcol_13_93766)
% 0.38/0.86 === Backtracking. Learning clause 235:2:1:[143.1,35.1,234.1]:Top: genls(c_tptpcol_3_81921,x0) -> collection(c_tptpcol_13_93766)
% 0.38/0.86 === Conflict found: 235:2:1:[143.1,35.1,234.1]:Top: genls(c_tptpcol_3_81921,x0) -> collection(c_tptpcol_13_93766) {x0 -> c_tptpcol_2_65537}
% 0.38/0.86 === Backtracking. Learning clause 236:1:0:[235.1,33.1]:: -> collection(c_tptpcol_13_93766)
% 0.38/0.86 === Backtracking. Learning clause 237:2:1:[143.1,53.1]:Top: genls(c_tptpcol_12_93765,x0) -> genls(c_tptpcol_13_93766,x0)
% 0.38/0.86 === Backtracking. Learning clause 238:2:1:[143.2,53.1]:Top: genls(x0,c_tptpcol_13_93766) -> genls(x0,c_tptpcol_12_93765)
% 0.38/0.86 === Backtracking. Learning clause 239:2:1:[143.1,55.1]:Top: genls(c_tptpcol_13_93766,x0) -> genls(c_tptpcol_14_93774,x0)
% 0.38/0.86 === Backtracking. Learning clause 240:2:1:[143.2,57.1]:Top: genls(x0,c_tptpcol_15_93775) -> genls(x0,c_tptpcol_14_93774)
% 0.38/0.86 === Backtracking. Learning clause 241:2:1:[78.1,59.1]:Top: genls(x0,c_tptpcol_1_1) -> disjointwith(x0,c_tptpcol_1_65536)
% 0.38/0.86 === Backtracking. Learning clause 242:3:2:[77.3,176.1,78.3]:TopTop: genls(c_tptpcol_15_93775,x0),disjointwith(x1,x0),genls(c_tptpcol_13_18664,x1) ->
% 0.38/0.86 === Backtracking. Learning clause 243:4:2:[77.1,241.2,242.2]:TopTop: genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1),genls(c_tptpcol_15_93775,x0),genls(c_tptpcol_13_18664,x1) ->
% 0.38/0.86 === Backtracking. Learning clause 244:4:2:[143.1,57.1,243.3,239.2,237.2]:TopTop: genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1),genls(c_tptpcol_13_18664,x1),genls(c_tptpcol_12_93765,x0) ->
% 0.38/0.86 === Backtracking. Learning clause 245:4:2:[143.1,51.1,244.4]:TopTop: genls(c_tptpcol_11_93764,x0),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1),genls(c_tptpcol_13_18664,x1) ->
% 0.38/0.86 === Backtracking. Learning clause 246:4:2:[143.1,49.1,245.1,227.2]:TopTop: genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1),genls(c_tptpcol_13_18664,x1),genls(c_tptpcol_9_93699,x0) ->
% 0.38/0.86 === Backtracking. Learning clause 247:4:2:[143.1,45.1,246.4,225.2,223.2,222.2,221.2]:TopTop: genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1),genls(c_tptpcol_13_18664,x1),genls(c_tptpcol_4_90113,x0) ->
% 0.38/0.86 === Backtracking. Learning clause 248:4:2:[143.1,35.1,247.4]:TopTop: genls(c_tptpcol_3_81921,x0),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1),genls(c_tptpcol_13_18664,x1) ->
% 0.38/0.86 === Conflict found: 248:4:2:[143.1,35.1,247.4]:TopTop: genls(c_tptpcol_3_81921,x0),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1),genls(c_tptpcol_13_18664,x1) -> {x0 -> c_tptpcol_2_65537, x1 -> c_cycorpproductsmt}
% 0.38/0.86 === Backtracking. Learning clause 249:2:1:[248.1,33.1,31.1,219.2]:Top: genls(x0,c_tptpcol_1_1),genls(c_tptpcol_12_18663,x0) ->
% 0.38/0.86 === Backtracking. Learning clause 250:2:1:[143.1,27.1,249.2,217.2,216.2,214.2,212.2,209.2,207.2,205.2,204.2]:Top: genls(x0,c_tptpcol_1_1),genls(c_tptpcol_3_16386,x0) ->
% 0.38/0.86 === Conflict found: 250:2:1:[143.1,27.1,249.2,217.2,216.2,214.2,212.2,209.2,207.2,205.2,204.2]:Top: genls(x0,c_tptpcol_1_1),genls(c_tptpcol_3_16386,x0) -> {x0 -> c_tptpcol_2_2}
% 0.38/0.86
% 0.38/0.86 SZS status Unsatisfiable
% 0.38/0.86
% 0.38/0.86 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/0.86
% 0.38/0.86 SPASS-SCL-FOL Statistics:
% 0.38/0.86 Number of learned clauses: 78
% 0.38/0.86 Number of propagations: 3950
% 0.38/0.86 Number of decisions: 1469
% 0.38/0.86 Number of resolutions: 128
% 0.38/0.86 Number of condensations: 0
% 0.38/0.86 Number of sub resolutions: 0
% 0.38/0.86 Number of input literals (deduplicated): 120
% 0.38/0.86 Number of grows: 4
% 0.38/0.86 Number of considered ground atoms: 264
% 0.38/0.86
% 0.38/0.86 Needed: 0:00:00.25
% 0.38/0.86
%------------------------------------------------------------------------------