%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR036+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 : n011.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:38 PM UTC 2026
% Result : Theorem 1.70s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR036+1 : TPTP v9.2.1. Released v3.4.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n011.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Thu May 7 11:38:13 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 SPASS-SCL-FOL version:
% 0.13/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.70/0.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.70/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.70/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.70/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.70/0.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.70/0.83 Execution resolution_1 ended with status: unsatisfiable
% 1.70/0.83 Used heuristic: resolution_1
% 1.70/0.83
% 1.70/0.83 Input Clauses:
% 1.70/0.83
% 1.70/0.83 Predicates: genlmt transitivebinarypredicate genls tptpcol_2_2 tptpcol_1_1 tptpcol_3_16386 tptpcol_4_16387 tptpcol_5_20483 tptpcol_6_20484 tptpcol_7_21508 tptpcol_8_22020 tptpcol_9_22021 tptpcol_10_22022 tptpcol_11_22023 tptpcol_12_22055 tptpcol_13_22071 tptpcol_14_22072 tptpcol_15_22076 tptpcol_2_65537 tptpcol_1_65536 tptpcol_3_65538 tptpcol_4_65539 tptpcol_5_69635 tptpcol_6_71683 tptpcol_7_72707 tptpcol_8_72708 tptpcol_9_72709 tptpcol_10_72710 tptpcol_11_72774 tptpcol_12_72775 tptpcol_13_72791 tptpcol_14_72792 tptpcol_15_72793 tptpcol_16_72795 disjointwith isa genlinverse genlpreds predicate binarypredicate collection mtvisible thing microtheory
% 1.70/0.83 Fol Constants: c_calendarsmt c_calendarsvocabularymt c_genlmt c_basekb c_universalvocabularymt c_cyclistsmt c_tptpcol_2_2 c_tptpcol_1_1 c_tptpcol_3_16386 c_tptpcol_4_16387 c_tptpcol_5_20483 c_tptpcol_6_20484 c_tptpcol_7_21508 c_tptpcol_8_22020 c_tptpcol_9_22021 c_tptpcol_10_22022 c_tptpcol_11_22023 c_tptpcol_12_22055 c_tptpcol_13_22071 c_tptpcol_14_22072 c_tptpcol_15_22076 c_tptpcol_2_65537 c_tptpcol_1_65536 c_tptpcol_3_65538 c_tptpcol_4_65539 c_tptpcol_5_69635 c_tptpcol_6_71683 c_tptpcol_7_72707 c_tptpcol_8_72708 c_tptpcol_9_72709 c_tptpcol_10_72710 c_tptpcol_11_72774 c_tptpcol_12_72775 c_tptpcol_13_72791 c_tptpcol_14_72792 c_tptpcol_15_72793 c_tptpcol_16_72795 c_tptp_spindleheadmt c_tptp_member974_mt c_transitivebinarypredicate
% 1.70/0.83 Fol Functions:
% 1.70/0.83 Problem Properties:
% 1.70/0.83 This is a Bernays Schoenfinkel problem.
% 1.70/0.83
% 1.70/0.83 After reduction: Problem Properties:
% 1.70/0.83 This is a Bernays Schoenfinkel problem.
% 1.70/0.83
% 1.70/0.83
% 1.70/0.83 Reduced Input Clauses:
% 1.70/0.83
% 1.70/0.83 Most General Atoms: tptpcol_2_2(x0) tptpcol_1_1(x0) tptpcol_3_16386(x0) tptpcol_4_16387(x0) tptpcol_5_20483(x0) tptpcol_6_20484(x0) tptpcol_7_21508(x0) tptpcol_8_22020(x0) tptpcol_9_22021(x0) tptpcol_10_22022(x0) tptpcol_11_22023(x0) tptpcol_12_22055(x0) tptpcol_13_22071(x0) tptpcol_14_22072(x0) tptpcol_15_22076(x0) tptpcol_2_65537(x0) tptpcol_1_65536(x0) tptpcol_3_65538(x0) tptpcol_4_65539(x0) tptpcol_5_69635(x0) tptpcol_6_71683(x0) tptpcol_7_72707(x0) tptpcol_8_72708(x0) tptpcol_9_72709(x0) tptpcol_10_72710(x0) tptpcol_11_72774(x0) tptpcol_12_72775(x0) tptpcol_13_72791(x0) tptpcol_14_72792(x0) tptpcol_15_72793(x0) tptpcol_16_72795(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) transitivebinarypredicate(x0) thing(x0)
% 1.70/0.83
% 1.70/0.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 53 atoms initially, heuristics mode: resolution_1 ===
% 1.70/0.83
% 1.70/0.83 === Backtracking. Learning clause 176:2:1:[35.2,65.2]:Top: tptpcol_2_65537(x0),tptpcol_1_1(x0) ->
% 1.70/0.83 === Backtracking. Learning clause 177:1:0:[81.1,64.1]:: -> collection(c_tptpcol_1_65536)
% 1.70/0.83 === Backtracking. Learning clause 178:1:0:[82.1,64.1]:: -> collection(c_tptpcol_1_1)
% 1.70/0.83 === Backtracking. Learning clause 179:3:3:[69.3,71.1]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2) -> predicate(x2)
% 1.70/0.83 === Clause set with instances from active satisfied. Growing active. New size: 117
% 1.70/0.83 === Restarting.
% 1.70/0.83 === Clause set with instances from active satisfied. Growing active. New size: 195
% 1.70/0.83 === Restarting.
% 1.70/0.83 === Backtracking. Learning clause 180:1:0:[151.1,8.1]:: -> collection(c_tptpcol_3_16386)
% 1.70/0.83 === Backtracking. Learning clause 181:1:0:[151.1,10.1]:: -> collection(c_tptpcol_4_16387)
% 1.70/0.83 === Backtracking. Learning clause 182:1:0:[151.1,12.1]:: -> collection(c_tptpcol_5_20483)
% 1.70/0.83 === Backtracking. Learning clause 183:1:0:[151.1,16.1]:: -> collection(c_tptpcol_7_21508)
% 1.70/0.83 === Backtracking. Learning clause 184:1:0:[151.1,26.1]:: -> collection(c_tptpcol_12_22055)
% 1.70/0.83 === Backtracking. Learning clause 185:1:0:[151.1,28.1]:: -> collection(c_tptpcol_13_22071)
% 1.70/0.83 === Backtracking. Learning clause 186:1:0:[151.1,46.1]:: -> collection(c_tptpcol_8_72708)
% 1.70/0.83 === Backtracking. Learning clause 187:1:0:[151.1,54.1]:: -> collection(c_tptpcol_12_72775)
% 1.70/0.83 === Backtracking. Learning clause 188:1:0:[151.1,56.1]:: -> collection(c_tptpcol_13_72791)
% 1.70/0.83 === Backtracking. Learning clause 189:1:0:[151.1,58.1]:: -> collection(c_tptpcol_14_72792)
% 1.70/0.83 === Clause set with instances from active satisfied. Growing active. New size: 281
% 1.70/0.83 === Restarting.
% 1.70/0.83 === Backtracking. Learning clause 190:1:0:[167.1,1.1]:: -> microtheory(c_calendarsvocabularymt)
% 1.70/0.83 === Backtracking. Learning clause 191:1:0:[169.1,1.1]:: -> microtheory(c_calendarsmt)
% 1.70/0.83 === Backtracking. Learning clause 192:2:0:[165.2,1.1]:: mtvisible(c_calendarsmt) -> mtvisible(c_calendarsvocabularymt)
% 1.70/0.83 === Backtracking. Learning clause 193:2:1:[170.2,5.1]:Top: genlmt(x0,c_calendarsvocabularymt) -> genlmt(x0,c_basekb)
% 1.70/0.83 === Backtracking. Learning clause 194:1:0:[169.1,66.1]:: -> microtheory(c_tptp_spindleheadmt)
% 1.70/0.83 === Backtracking. Learning clause 195:2:1:[170.2,66.1]:Top: genlmt(x0,c_tptp_spindleheadmt) -> genlmt(x0,c_cyclistsmt)
% 1.70/0.83 === Backtracking. Learning clause 196:2:1:[170.1,66.1]:Top: genlmt(c_cyclistsmt,x0) -> genlmt(c_tptp_spindleheadmt,x0)
% 1.70/0.83 === Backtracking. Learning clause 197:2:0:[165.2,66.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_cyclistsmt)
% 1.70/0.83 === Backtracking. Learning clause 198:1:0:[169.1,67.1]:: -> microtheory(c_tptp_member974_mt)
% 1.70/0.83 === Backtracking. Learning clause 199:1:0:[165.2,67.1,174.1,197.1]:: -> mtvisible(c_cyclistsmt)
% 1.70/0.83 === Backtracking. Learning clause 200:1:0:[151.1,6.1]:: -> collection(c_tptpcol_2_2)
% 1.70/0.83 === Backtracking. Learning clause 201:1:0:[151.1,14.1]:: -> collection(c_tptpcol_6_20484)
% 1.70/0.83 === Backtracking. Learning clause 202:1:0:[151.1,30.1]:: -> collection(c_tptpcol_14_22072)
% 1.70/0.83 === Backtracking. Learning clause 203:1:0:[151.1,38.1]:: -> collection(c_tptpcol_4_65539)
% 1.70/0.83 === Backtracking. Learning clause 204:1:0:[151.1,40.1]:: -> collection(c_tptpcol_5_69635)
% 1.70/0.83 === Backtracking. Learning clause 205:1:0:[151.1,42.1]:: -> collection(c_tptpcol_6_71683)
% 1.70/0.83 === Backtracking. Learning clause 206:1:0:[151.1,44.1]:: -> collection(c_tptpcol_7_72707)
% 1.70/0.83 === Backtracking. Learning clause 207:1:0:[151.1,50.1]:: -> collection(c_tptpcol_10_72710)
% 1.70/0.83 === Backtracking. Learning clause 208:1:0:[151.1,60.1]:: -> collection(c_tptpcol_15_72793)
% 1.70/0.83 === Clause set with instances from active satisfied. Growing active. New size: 294
% 1.70/0.83 === Restarting.
% 1.70/0.83 === Backtracking. Learning clause 209:1:0:[165.2,4.1,199.1]:: -> mtvisible(c_calendarsmt)
% 1.70/0.83 === Backtracking. Learning clause 210:1:0:[169.1,4.1]:: -> microtheory(c_cyclistsmt)
% 1.70/0.83 === Backtracking. Learning clause 211:3:2:[170.1,67.1,170.1]:TopTop: genlmt(c_tptp_spindleheadmt,x0),genlmt(x0,x1) -> genlmt(c_tptp_member974_mt,x1)
% 1.70/0.83 === Backtracking. Learning clause 212:2:1:[156.2,6.1]:Top: genls(x0,c_tptpcol_2_2) -> genls(x0,c_tptpcol_1_1)
% 1.70/0.83 === Backtracking. Learning clause 213:2:1:[156.1,10.1]:Top: genls(c_tptpcol_3_16386,x0) -> genls(c_tptpcol_4_16387,x0)
% 1.70/0.83 === Backtracking. Learning clause 214:2:1:[156.1,12.1]:Top: genls(c_tptpcol_4_16387,x0) -> genls(c_tptpcol_5_20483,x0)
% 1.70/0.83 === Backtracking. Learning clause 215:2:1:[156.2,12.1]:Top: genls(x0,c_tptpcol_5_20483) -> genls(x0,c_tptpcol_4_16387)
% 1.70/0.83 === Backtracking. Learning clause 216:2:1:[156.2,14.1]:Top: genls(x0,c_tptpcol_6_20484) -> genls(x0,c_tptpcol_5_20483)
% 1.70/0.83 === Backtracking. Learning clause 217:2:1:[156.2,16.1]:Top: genls(x0,c_tptpcol_7_21508) -> genls(x0,c_tptpcol_6_20484)
% 1.70/0.83 === Backtracking. Learning clause 218:2:1:[156.2,18.1]:Top: genls(x0,c_tptpcol_8_22020) -> genls(x0,c_tptpcol_7_21508)
% 1.70/0.83 === Backtracking. Learning clause 219:2:1:[156.1,20.1]:Top: genls(c_tptpcol_8_22020,x0) -> genls(c_tptpcol_9_22021,x0)
% 1.70/0.83 === Backtracking. Learning clause 220:2:1:[156.2,20.1]:Top: genls(x0,c_tptpcol_9_22021) -> genls(x0,c_tptpcol_8_22020)
% 1.70/0.83 === Backtracking. Learning clause 221:2:1:[156.1,22.1,151.1,219.2]:Top: genls(c_tptpcol_8_22020,x0) -> collection(c_tptpcol_10_22022)
% 1.70/0.83 === Backtracking. Learning clause 222:2:1:[156.1,18.1,221.1]:Top: genls(c_tptpcol_7_21508,x0) -> collection(c_tptpcol_10_22022)
% 1.70/0.83 === Backtracking. Learning clause 223:2:1:[156.1,16.1,222.1]:Top: genls(c_tptpcol_6_20484,x0) -> collection(c_tptpcol_10_22022)
% 1.70/0.83 === Backtracking. Learning clause 224:2:1:[156.1,14.1,223.1,214.2,213.2]:Top: genls(c_tptpcol_3_16386,x0) -> collection(c_tptpcol_10_22022)
% 1.70/0.83 === Conflict found: 224:2:1:[156.1,14.1,223.1,214.2,213.2]:Top: genls(c_tptpcol_3_16386,x0) -> collection(c_tptpcol_10_22022) {x0 -> c_tptpcol_2_2}
% 1.70/0.83 === Backtracking. Learning clause 225:1:0:[224.1,8.1]:: -> collection(c_tptpcol_10_22022)
% 1.70/0.83 === Backtracking. Learning clause 226:2:1:[156.1,22.1]:Top: genls(c_tptpcol_9_22021,x0) -> genls(c_tptpcol_10_22022,x0)
% 1.70/0.83 === Backtracking. Learning clause 227:2:1:[156.1,24.1]:Top: genls(c_tptpcol_10_22022,x0) -> genls(c_tptpcol_11_22023,x0)
% 1.70/0.83 === Backtracking. Learning clause 228:2:1:[156.2,26.1]:Top: genls(x0,c_tptpcol_12_22055) -> genls(x0,c_tptpcol_11_22023)
% 1.70/0.83 === Backtracking. Learning clause 229:2:1:[156.1,28.1]:Top: genls(c_tptpcol_12_22055,x0) -> genls(c_tptpcol_13_22071,x0)
% 1.70/0.83 === Backtracking. Learning clause 230:2:1:[156.2,30.1]:Top: genls(x0,c_tptpcol_14_22072) -> genls(x0,c_tptpcol_13_22071)
% 1.70/0.83 === Backtracking. Learning clause 231:2:1:[156.2,32.1]:Top: genls(x0,c_tptpcol_15_22076) -> genls(x0,c_tptpcol_14_22072)
% 1.70/0.83 === Backtracking. Learning clause 232:2:1:[156.1,36.1,151.1]:Top: genls(c_tptpcol_2_65537,x0) -> collection(c_tptpcol_3_65538)
% 1.70/0.83 === Conflict found: 232:2:1:[156.1,36.1,151.1]:Top: genls(c_tptpcol_2_65537,x0) -> collection(c_tptpcol_3_65538) {x0 -> c_tptpcol_1_65536}
% 1.70/0.83 === Backtracking. Learning clause 233:1:0:[232.1,34.1]:: -> collection(c_tptpcol_3_65538)
% 1.70/0.83 === Backtracking. Learning clause 234:2:1:[156.1,38.1]:Top: genls(c_tptpcol_3_65538,x0) -> genls(c_tptpcol_4_65539,x0)
% 1.70/0.83 === Backtracking. Learning clause 235:2:1:[156.2,40.1]:Top: genls(x0,c_tptpcol_5_69635) -> genls(x0,c_tptpcol_4_65539)
% 1.70/0.83 === Backtracking. Learning clause 236:2:1:[156.2,46.1]:Top: genls(x0,c_tptpcol_8_72708) -> genls(x0,c_tptpcol_7_72707)
% 1.70/0.83 === Backtracking. Learning clause 237:2:1:[156.1,48.1]:Top: genls(c_tptpcol_8_72708,x0) -> genls(c_tptpcol_9_72709,x0)
% 1.70/0.83 === Backtracking. Learning clause 238:2:1:[156.1,50.1]:Top: genls(c_tptpcol_9_72709,x0) -> genls(c_tptpcol_10_72710,x0)
% 1.70/0.83 === Backtracking. Learning clause 239:2:1:[156.2,56.1]:Top: genls(x0,c_tptpcol_13_72791) -> genls(x0,c_tptpcol_12_72775)
% 1.70/0.83 === Backtracking. Learning clause 240:2:1:[156.1,58.1]:Top: genls(c_tptpcol_13_72791,x0) -> genls(c_tptpcol_14_72792,x0)
% 1.70/0.83 === Backtracking. Learning clause 241:2:1:[156.1,60.1]:Top: genls(c_tptpcol_14_72792,x0) -> genls(c_tptpcol_15_72793,x0)
% 1.70/0.83 === Backtracking. Learning clause 242:1:0:[151.1,62.1]:: -> collection(c_tptpcol_16_72795)
% 1.70/0.83 === Backtracking. Learning clause 243:2:1:[156.2,62.1]:Top: genls(x0,c_tptpcol_16_72795) -> genls(x0,c_tptpcol_15_72793)
% 1.70/0.83 === Backtracking. Learning clause 244:3:2:[84.1,64.1,85.1]:TopTop: genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1) -> disjointwith(x1,x0)
% 1.70/0.83 === Backtracking. Learning clause 245:2:1:[84.1,64.1,83.1]:Top: genls(x0,c_tptpcol_1_65536) -> disjointwith(x0,c_tptpcol_1_1)
% 1.70/0.83 === Backtracking. Learning clause 246:2:1:[85.1,64.1]:Top: genls(x0,c_tptpcol_1_1) -> disjointwith(x0,c_tptpcol_1_65536)
% 1.70/0.83 === Backtracking. Learning clause 247:4:2:[84.3,175.1,85.3,244.3]:TopTop: genls(c_tptpcol_16_72795,x0),genls(c_tptpcol_15_22076,x1),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 248:4:2:[156.1,62.1,247.1,241.2,240.2]:TopTop: genls(c_tptpcol_15_22076,x0),genls(x1,c_tptpcol_1_65536),genls(x0,c_tptpcol_1_1),genls(c_tptpcol_13_72791,x1) ->
% 1.70/0.83 === Backtracking. Learning clause 249:4:2:[156.1,56.1,248.4]:TopTop: genls(c_tptpcol_12_72775,x0),genls(c_tptpcol_15_22076,x1),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 250:4:2:[156.1,54.1,249.1]:TopTop: genls(c_tptpcol_11_72774,x0),genls(c_tptpcol_15_22076,x1),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 251:4:2:[156.1,52.1,250.1,238.2,237.2]:TopTop: genls(c_tptpcol_15_22076,x0),genls(x1,c_tptpcol_1_65536),genls(x0,c_tptpcol_1_1),genls(c_tptpcol_8_72708,x1) ->
% 1.70/0.83 === Backtracking. Learning clause 252:4:2:[156.1,46.1,251.4]:TopTop: genls(c_tptpcol_7_72707,x0),genls(c_tptpcol_15_22076,x1),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 253:4:2:[156.1,44.1,252.1]:TopTop: genls(c_tptpcol_6_71683,x0),genls(c_tptpcol_15_22076,x1),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 254:4:2:[156.1,42.1,253.1]:TopTop: genls(c_tptpcol_5_69635,x0),genls(c_tptpcol_15_22076,x1),genls(x0,c_tptpcol_1_65536),genls(x1,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 255:4:2:[156.1,40.1,254.1,234.2]:TopTop: genls(c_tptpcol_15_22076,x0),genls(x1,c_tptpcol_1_65536),genls(x0,c_tptpcol_1_1),genls(c_tptpcol_3_65538,x1) ->
% 1.70/0.83 === Conflict found: 255:4:2:[156.1,40.1,254.1,234.2]:TopTop: genls(c_tptpcol_15_22076,x0),genls(x1,c_tptpcol_1_65536),genls(x0,c_tptpcol_1_1),genls(c_tptpcol_3_65538,x1) -> {x0 -> c_calendarsmt, x1 -> c_tptpcol_2_65537}
% 1.70/0.83 === Backtracking. Learning clause 256:2:1:[255.4,36.1,34.1]:Top: genls(c_tptpcol_15_22076,x0),genls(x0,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 257:2:1:[156.1,32.1,256.1]:Top: genls(c_tptpcol_14_22072,x0),genls(x0,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 258:2:1:[156.1,30.1,257.1,229.2]:Top: genls(x0,c_tptpcol_1_1),genls(c_tptpcol_12_22055,x0) ->
% 1.70/0.83 === Backtracking. Learning clause 259:2:1:[156.1,26.1,258.2,227.2,226.2,219.2]:Top: genls(x0,c_tptpcol_1_1),genls(c_tptpcol_8_22020,x0) ->
% 1.70/0.83 === Backtracking. Learning clause 260:2:1:[156.1,18.1,259.2]:Top: genls(c_tptpcol_7_21508,x0),genls(x0,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 261:2:1:[156.1,16.1,260.1]:Top: genls(c_tptpcol_6_20484,x0),genls(x0,c_tptpcol_1_1) ->
% 1.70/0.83 === Backtracking. Learning clause 262:2:1:[156.1,14.1,261.1,214.2,213.2]:Top: genls(x0,c_tptpcol_1_1),genls(c_tptpcol_3_16386,x0) ->
% 1.70/0.83 === Conflict found: 262:2:1:[156.1,14.1,261.1,214.2,213.2]:Top: genls(x0,c_tptpcol_1_1),genls(c_tptpcol_3_16386,x0) -> {x0 -> c_tptpcol_2_2}
% 1.70/0.83
% 1.70/0.83 SZS status Unsatisfiable
% 1.70/0.83
% 1.70/0.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.70/0.83
% 1.70/0.83 SPASS-SCL-FOL Statistics:
% 1.70/0.83 Number of learned clauses: 87
% 1.70/0.83 Number of propagations: 4366
% 1.70/0.83 Number of decisions: 1974
% 1.70/0.83 Number of resolutions: 131
% 1.70/0.83 Number of condensations: 0
% 1.70/0.83 Number of sub resolutions: 0
% 1.70/0.83 Number of input literals (deduplicated): 120
% 1.70/0.83 Number of grows: 4
% 1.70/0.83 Number of considered ground atoms: 294
% 1.70/0.83
% 1.70/0.83 Needed: 0:00:00.29
% 1.70/0.83
%------------------------------------------------------------------------------