%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PLA026+1 : TPTP v9.2.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:31:13 PM UTC 2026
% Result : CounterSatisfiable 2.89s 1.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PLA026+1 : TPTP v9.2.1. Bugfixed v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n015.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.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 12:56:17 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 2.89/1.12 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.89/1.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.89/1.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.89/1.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.89/1.12 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.89/1.12 Execution lmodel_grow ended with status: satisfiable
% 2.89/1.12 Used heuristic: lmodel_grow
% 2.89/1.12
% 2.89/1.12 Input Clauses:
% 2.89/1.12
% 2.89/1.12 Predicates: nonfixed a_block neq time object destination on source clear fixed different goal_time ren1
% 2.89/1.12 Fol Constants: block_1 block_2 block_3 block_4 block_5 table time_0 skc1
% 2.89/1.12 Fol Functions: s
% 2.89/1.12 Problem Properties:
% 2.89/1.12 This is a full first-order problem without equality.
% 2.89/1.12
% 2.89/1.12 After reduction: Problem Properties:
% 2.89/1.12 This is a full first-order problem without equality.
% 2.89/1.12
% 2.89/1.12
% 2.89/1.12 Reduced Input Clauses:
% 2.89/1.12
% 2.89/1.12 Most General Atoms: object(x1,x2) source(x0,x2) destination(x0,x2) nonfixed(x2) neq(x1,x2) a_block(x2) on(x0,x2,x3) clear(x1,x2) fixed(x1) different(x0,x1) ren1(x1,x0) time(x0) goal_time(s(s(s(s(time_0))))) goal_time(skc1)
% 2.89/1.12
% 2.89/1.12 === Starting SPASS-SCL-FOL A Little Less Naive, considering 81 atoms initially, heuristics mode: lmodel_grow ===
% 2.89/1.12
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 99
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 116
% 2.89/1.12 === Backtracking. Learning clause 73:4:3:[6.3,23.4]:TopTopTop: object(x0,x1),nonfixed(x2),nonfixed(x0),on(x2,x0,x1) ->
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 125
% 2.89/1.12 === Backtracking. Learning clause 74:4:3:[7.3,23.4]:TopTopTop: destination(x0,x1),nonfixed(x2),nonfixed(x0),on(x2,x0,x1) ->
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 146
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 158
% 2.89/1.12 === Backtracking. Learning clause 75:5:3:[27.2,14.3,26.2]:TopTopTop: a_block(x0),a_block(x1),source(x0,x2),source(x1,x2),different(x1,x0) ->
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 175
% 2.89/1.12 === Backtracking. Learning clause 76:8:3:[10.4,75.3,6.3]:TopTopTop: time(x1),a_block(x0),a_block(x2),source(x2,x1),different(x2,x0),nonfixed(x0),object(x0,s(x1)) -> clear(x0,x1)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 184
% 2.89/1.12 === Backtracking. Learning clause 77:10:3:[10.3,6.3,76.4]:TopTopTop: nonfixed(x0),object(x0,s(x1)),time(x1),a_block(x2),a_block(x0),different(x0,x2),nonfixed(x2),object(x2,s(x1)) -> clear(x0,x1),clear(x2,x1)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 195
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 203
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 205
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 215
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 218
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 220
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 222
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 224
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 228
% 2.89/1.12 === Backtracking. Learning clause 78:8:3:[9.7,73.4,27.2,26.2]:TopTopTop: a_block(x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1),different(x1,x0) -> object(x0,x2)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 235
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 250
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 264
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 267
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 275
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 280
% 2.89/1.12 === Backtracking. Learning clause 79:2:2:[27.1,25.2]:TopTop: different(x0,x1) -> neq(x0,x1)
% 2.89/1.12 === Backtracking. Learning clause 82:5:2:[54.0,80.0,48.0,81.3,22.5,79.2,79.2,42.1]:TopTop: a_block(x0),neq(block_5,x0),on(block_5,x0,x1),on(block_5,table,x1),different(x0,table) ->
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 299
% 2.89/1.12 === Backtracking. Learning clause 83:2:2:[27.1,26.2]:TopTop: different(x0,x1) -> neq(x1,x0)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 322
% 2.89/1.12 === Backtracking. Learning clause 85:10:2:[54.0,84.3,5.6,23.3,62.6]:TopTop: a_block(x0),neq(block_5,x0),source(x0,x1),nonfixed(x0),clear(x0,x1),time(x1) -> object(block_1,x1),object(block_2,x1),object(block_3,x1),object(block_4,x1)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 352
% 2.89/1.12 === Conflict found: 83:2:2:[27.1,26.2]:TopTop: different(x0,x1) -> neq(x1,x0) {x0 -> block_2, x1 -> block_2}
% 2.89/1.12 === Backtracking. Learning clause 86:8:4:[83.2,22.6]:TopTopTopTop: different(x0,x1),nonfixed(x2),a_block(x1),neq(x2,x1),a_block(x0),neq(x2,x0),on(x2,x1,x3),on(x2,x0,x3) ->
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 371
% 2.89/1.12 === Backtracking. Learning clause 87:9:4:[22.8,5.6]:TopTopTopTop: a_block(x1),neq(x0,x1),neq(x1,x2),on(x0,x1,x3),nonfixed(x0),a_block(x2),neq(x0,x2),object(x0,x3),source(x2,x3) ->
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 392
% 2.89/1.12 === Conflict found: 86:8:4:[83.2,22.6]:TopTopTopTop: different(x0,x1),nonfixed(x2),a_block(x1),neq(x2,x1),a_block(x0),neq(x2,x0),on(x2,x1,x3),on(x2,x0,x3) -> {x0 -> block_1, x1 -> table, x2 -> block_2, x3 -> skc1}
% 2.89/1.12 === Backtracking. Learning clause 88:8:4:[86.4,79.2]:TopTopTopTop: different(x0,x1),nonfixed(x2),a_block(x1),a_block(x0),neq(x2,x0),on(x2,x1,x3),on(x2,x0,x3),different(x2,x1) ->
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 405
% 2.89/1.12 === Backtracking. Learning clause 89:10:4:[12.7,86.8]:TopTopTopTop: time(x2),on(x0,x1,s(x2)),different(x1,x3),nonfixed(x0),a_block(x3),neq(x0,x3),a_block(x1),neq(x0,x1),on(x0,x3,x2) -> destination(x1,x2)
% 2.89/1.12 === Conflict found: 89:10:4:[12.7,86.8]:TopTopTopTop: time(x2),on(x0,x1,s(x2)),different(x1,x3),nonfixed(x0),a_block(x3),neq(x0,x3),a_block(x1),neq(x0,x1),on(x0,x3,x2) -> destination(x1,x2) {x0 -> block_5, x1 -> block_2, x2 -> time_0, x3 -> block_4}
% 2.89/1.12 === Backtracking. Learning clause 92:11:3:[46.0,90.1,44.0,91.4,89.3,33.1,11.7,13.4]:TopTopTop: time(x0),neq(x1,block_4),on(x1,block_4,x0),neq(x1,block_2),time(s(x0)),on(x1,block_2,s(s(x0))),nonfixed(x1),a_block(x2),neq(x1,x2),object(x2,s(x0)) -> destination(block_2,x0)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 421
% 2.89/1.12 === Backtracking. Learning clause 94:4:2:[17.2,93.3,8.3,6.3]:TopTop: time(x0),nonfixed(x1),object(x1,x0) -> clear(x1,s(x0))
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 435
% 2.89/1.12 === Conflict found: 73:4:3:[6.3,23.4]:TopTopTop: object(x0,x1),nonfixed(x2),nonfixed(x0),on(x2,x0,x1) -> {x0 -> block_2, x1 -> s(s(s(s(time_0)))), x2 -> block_3}
% 2.89/1.12 === Backtracking. Learning clause 97:14:3:[51.0,95.0,44.0,96.2,73.4,1.7,85.8]:TopTopTop: nonfixed(x0),neq(x0,block_2),time(x1),object(x0,x1),destination(block_2,x1),a_block(x2),neq(block_5,x2),source(x2,s(x1)),nonfixed(x2),clear(x2,s(x1)),time(s(x1)) -> object(block_1,s(x1)),object(block_3,s(x1)),object(block_4,s(x1))
% 2.89/1.12 === Backtracking. Learning clause 98:9:3:[9.5,1.7,16.2]:TopTopTop: time(s(x2)),a_block(x1),neq(x0,x1),time(x2),object(x0,x2),destination(x1,x2),nonfixed(x0),source(x0,s(x2)) -> on(x0,x1,s(s(x2)))
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 445
% 2.89/1.12 === Backtracking. Learning clause 99:10:4:[5.6,21.7]:TopTopTopTop: a_block(x1),object(x0,x2),source(x1,x2),nonfixed(x0),nonfixed(x1),neq(x0,x1),nonfixed(x3),neq(x0,x3),neq(x1,x3),on(x3,x1,x2) ->
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 455
% 2.89/1.12 === Backtracking. Learning clause 111:37:4:[53.0,100.1,44.0,101.3,34.0,102.4,48.0,103.5,47.0,104.13,46.0,105.19,54.0,106.26,51.0,107.27,45.0,108.30,52.0,109.33,50.0,110.35,1.7,99.10,62.5,76.7,4.4,61.6,60.3,5.5,1.5,8.4,16.3,4.3,94.4,87.9,6.3,87.9,9.6,9.5,94.3,99.10,85.5,62.6,6.2]:TopTopTopTop: neq(block_4,block_3),neq(block_5,block_4),neq(block_3,table),neq(block_2,block_3),time(x0),a_block(x1),neq(block_3,x1),neq(x1,block_5),on(block_3,x1,s(x0)),neq(block_3,block_5),a_block(x2),neq(block_3,x2),neq(x2,block_4),on(block_3,x2,s(x0)),neq(block_3,block_4),time(s(x0)),on(block_3,x3,s(x0)),a_block(x3),neq(block_3,x3),time(s(s(x0))),neq(block_5,block_2),neq(block_3,block_2),neq(block_5,block_3),source(block_3,s(s(s(x0)))),time(s(s(s(x0)))) -> object(block_1,s(s(x0))),destination(block_1,x0),destination(block_2,x0),destination(block_4,x0),destination(table,x0),source(block_1,s(x0)),on(block_3,table,s(x0)),on(block_3,x3,s(s(s(x0)))),object(block_2,s(s(s(x0)))),object(block_3,s(s(s(x0)))),object(block_4,s(s(s(x0)))),clear(block_1,s(s(s(x0))))
% 2.89/1.12 === Conflict found: 78:8:3:[9.7,73.4,27.2,26.2]:TopTopTop: a_block(x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1),different(x1,x0) -> object(x0,x2) {x0 -> block_2, x1 -> block_1, x2 -> s(s(s(time_0)))}
% 2.89/1.12 === Backtracking. Learning clause 117:24:3:[43.0,112.0,50.0,113.2,45.0,114.8,52.0,115.17,54.0,116.18,78.8,78.4,85.7,94.4,9.6,9.7,6.2,4.4,61.4,4.3]:TopTopTop: on(x0,block_1,s(s(x1))),different(block_1,x0),a_block(x0),on(block_3,x0,s(x1)),nonfixed(x0),different(x0,block_3),neq(block_5,block_3),source(block_3,s(s(s(x1)))),time(s(s(s(x1)))),time(s(s(x1))),a_block(x2),neq(block_3,x2),time(s(x1)),on(block_3,x2,s(x1)),time(x1),clear(block_5,s(x1)) -> object(block_2,s(s(s(x1)))),object(block_3,s(s(s(x1)))),object(block_4,s(s(s(x1)))),on(block_3,x2,s(s(s(x1)))),destination(block_1,x1),destination(block_2,x1),destination(block_4,x1),destination(table,x1)
% 2.89/1.12 === Backtracking. Learning clause 124:18:2:[54.0,118.1,53.0,119.2,45.0,120.6,52.0,121.9,43.0,122.11,50.0,123.15,1.7,99.10,8.4,62.6,62.5,94.3,85.5,78.4]:TopTop: neq(block_4,block_3),neq(block_5,block_4),neq(block_3,block_4),clear(block_3,x0),neq(block_5,block_3),source(block_3,s(x0)),time(s(x0)),time(x0),on(x1,block_1,x0),nonfixed(x1),different(block_1,x1) -> object(block_1,x0),object(block_2,x0),object(block_5,x0),object(block_2,s(x0)),object(block_3,s(x0)),object(block_4,s(x0)),object(x1,x0)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 463
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 469
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 471
% 2.89/1.12 === Backtracking. Learning clause 126:14:3:[50.0,125.2,5.6,23.3,79.2,85.7]:TopTopTop: a_block(x0),source(x0,x1),nonfixed(x0),clear(x0,x1),different(block_1,x0),a_block(x2),neq(block_5,x2),source(x2,x1),nonfixed(x2),clear(x2,x1),time(x1) -> object(block_2,x1),object(block_3,x1),object(block_4,x1)
% 2.89/1.12 === Backtracking. Learning clause 127:11:4:[9.7,9.5,13.4]:TopTopTopTop: time(x2),on(x0,x1,x2),a_block(x1),neq(x0,x1),time(s(x2)),nonfixed(x0),a_block(x3),neq(x0,x3),object(x3,x2) -> object(x0,s(x2)),on(x0,x1,s(s(x2)))
% 2.89/1.12 === Backtracking. Learning clause 129:19:6:[79.1,128.0,5.6,88.6,9.6,127.2]:TopTopTopTopTopTop: source(x0,x1),different(x2,x0),a_block(x0),a_block(x2),neq(x3,x2),on(x3,x2,x1),different(x3,x0),time(x1),on(x3,x4,x1),time(s(x1)),a_block(x4),neq(x3,x4),time(s(s(x1))),nonfixed(x3),a_block(x5),neq(x3,x5),object(x5,s(x1)) -> object(x3,s(s(x1))),on(x3,x4,s(s(s(x1))))
% 2.89/1.12 === Conflict found: 127:11:4:[9.7,9.5,13.4]:TopTopTopTop: time(x2),on(x0,x1,x2),a_block(x1),neq(x0,x1),time(s(x2)),nonfixed(x0),a_block(x3),neq(x0,x3),object(x3,x2) -> object(x0,s(x2)),on(x0,x1,s(s(x2))) {x0 -> block_2, x1 -> block_1, x2 -> s(time_0), x3 -> block_4}
% 2.89/1.12 === Backtracking. Learning clause 131:28:8:[83.1,130.1,127.11,78.3,79.2,73.1,11.7,73.1,129.19]:TopTopTopTopTopTopTopTop: on(x0,x1,s(x2)),a_block(x3),object(x3,s(x2)),a_block(x1),time(s(s(s(x2)))),object(x1,s(s(s(s(x2))))),nonfixed(x1),different(x1,x0),different(x0,x3),nonfixed(x0),source(x4,x2),different(x5,x4),a_block(x4),a_block(x5),neq(x6,x5),on(x6,x5,x2),different(x6,x4),time(x2),on(x6,x0,x2),time(s(x2)),a_block(x0),neq(x6,x0),time(s(s(x2))),nonfixed(x6),a_block(x7),neq(x6,x7),object(x7,s(x2)) -> object(x6,s(s(x2)))
% 2.89/1.12 === Conflict found: 129:19:6:[79.1,128.0,5.6,88.6,9.6,127.2]:TopTopTopTopTopTop: source(x0,x1),different(x2,x0),a_block(x0),a_block(x2),neq(x3,x2),on(x3,x2,x1),different(x3,x0),time(x1),on(x3,x4,x1),time(s(x1)),a_block(x4),neq(x3,x4),time(s(s(x1))),nonfixed(x3),a_block(x5),neq(x3,x5),object(x5,s(x1)) -> object(x3,s(s(x1))),on(x3,x4,s(s(s(x1)))) {x0 -> block_4, x1 -> time_0, x2 -> block_1, x3 -> block_2, x4 -> block_1, x5 -> block_4}
% 2.89/1.12 === Backtracking. Learning clause 133:25:7:[83.1,132.10,129.18,13.5,79.2,78.3]:TopTopTopTopTopTopTop: source(x0,x1),different(x2,x0),a_block(x0),a_block(x2),neq(x3,x2),on(x3,x2,x1),different(x3,x0),time(x1),on(x3,x4,x1),time(s(x1)),time(s(s(x1))),a_block(x5),object(x5,s(x1)),nonfixed(x6),a_block(x3),neq(x6,x3),object(x6,s(s(x1))),different(x3,x5),a_block(x4),time(s(s(s(x1)))),object(x4,s(s(s(s(x1))))),nonfixed(x3),nonfixed(x4),different(x4,x3) -> object(x3,s(s(s(x1))))
% 2.89/1.12 === Backtracking. Learning clause 143:40:9:[45.0,134.8,52.0,135.10,48.0,136.11,44.0,137.12,51.0,138.15,43.0,139.21,50.0,140.24,47.0,141.31,54.0,142.37,5.6,89.2,60.4,5.5,1.6,83.2,78.3,36.1,18.2,99.3,61.7,99.3,12.5,17.3,78.8,79.2]:TopTopTopTopTopTopTopTopTop: object(x0,s(x1)),different(block_3,x2),nonfixed(x0),a_block(x2),neq(x0,x2),neq(x0,block_3),on(x0,x2,x1),object(x3,s(x1)),object(block_3,s(s(x1))),object(x4,s(x1)),nonfixed(x4),neq(x4,block_2),nonfixed(x5),neq(x4,x5),on(x5,block_2,s(x1)),time(s(x1)),object(x6,s(x1)),nonfixed(x6),neq(x6,block_1),nonfixed(x7),neq(x6,x7),neq(block_1,x7),on(x7,block_1,s(x1)),nonfixed(x3),neq(x3,block_5),a_block(x8),time(x1),on(block_5,x8,x1),object(x8,s(x1)),nonfixed(x8),different(x8,block_5),different(block_2,x5) -> source(block_4,s(x1)),object(block_5,s(x1)),destination(block_1,s(x1)),destination(block_2,s(x1)),destination(block_3,s(x1)),destination(block_4,s(x1)),destination(block_5,s(x1)),on(x3,block_5,x1)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 479
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 480
% 2.89/1.12 === Backtracking. Learning clause 144:7:3:[5.6,23.3]:TopTopTop: a_block(x1),neq(x0,x1),object(x0,x2),source(x1,x2),nonfixed(x0),nonfixed(x1),clear(x1,x2) ->
% 2.89/1.12 === Backtracking. Learning clause 147:47:11:[44.0,145.0,83.1,146.1,9.6,87.8,143.15]:TopTopTopTopTopTopTopTopTopTopTop: on(x0,block_2,x1),a_block(x2),neq(x0,x2),neq(x2,x3),on(x0,x2,x1),a_block(x3),neq(x0,x3),source(x3,x1),object(x4,s(x1)),different(block_3,x5),nonfixed(x4),a_block(x5),neq(x4,x5),neq(x4,block_3),on(x4,x5,x1),object(x6,s(x1)),object(block_3,s(s(x1))),object(x7,s(x1)),nonfixed(x7),neq(x7,block_2),nonfixed(x0),neq(x7,x0),time(s(x1)),object(x8,s(x1)),nonfixed(x8),neq(x8,block_1),nonfixed(x9),neq(x8,x9),neq(block_1,x9),on(x9,block_1,s(x1)),nonfixed(x6),neq(x6,block_5),a_block(x10),time(x1),on(block_5,x10,x1),object(x10,s(x1)),nonfixed(x10),different(x10,block_5),different(block_2,x0) -> source(block_4,s(x1)),object(block_5,s(x1)),destination(block_1,s(x1)),destination(block_2,s(x1)),destination(block_3,s(x1)),destination(block_4,s(x1)),destination(block_5,s(x1)),on(x6,block_5,x1)
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 489
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 493
% 2.89/1.12 === Clause set with instances from active satisfied. Growing active. New size: 494
% 2.89/1.12
% 2.89/1.12 Linear Model Building succeeded.
% 2.89/1.12 SZS status Satisfiable
% 2.89/1.12
% 2.89/1.12 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.89/1.12
% 2.89/1.12 SPASS-SCL-FOL Statistics:
% 2.89/1.12 Number of learned clauses: 30
% 2.89/1.12 Number of propagations: 3649
% 2.89/1.12 Number of decisions: 1608
% 2.89/1.12 Number of resolutions: 104
% 2.89/1.12 Number of condensations: 0
% 2.89/1.12 Number of sub resolutions: 45
% 2.89/1.12 Number of input literals (deduplicated): 81
% 2.89/1.12 Number of grows: 40
% 2.89/1.12 Number of considered ground atoms: 494
% 2.89/1.12
% 2.89/1.12 Needed: 0:00:00.56
% 2.89/1.12
%------------------------------------------------------------------------------