%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PLA027+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 : n008.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:14 PM UTC 2026
% Result : CounterSatisfiable 20.38s 4.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : PLA027+1 : TPTP v9.2.1. Bugfixed v2.5.0.
% 0.12/0.15 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.37 % Computer : n008.cluster.edu
% 0.19/0.37 % Model : x86_64 x86_64
% 0.19/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.37 % Memory : 8042.1875MB
% 0.19/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.19/0.37 % CPULimit : 300
% 0.19/0.37 % WCLimit : 300
% 0.19/0.37 % DateTime : Thu May 7 12:56:14 EDT 2026
% 0.19/0.37 % CPUTime :
% 0.19/0.37 SPASS-SCL-FOL version:
% 0.30/0.47 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 20.38/4.67 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.38/4.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.38/4.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.38/4.67 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.38/4.67 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.38/4.67 Execution lmodel_grow ended with status: satisfiable
% 20.38/4.67 Used heuristic: lmodel_grow
% 20.38/4.67
% 20.38/4.67 Input Clauses:
% 20.38/4.67
% 20.38/4.67 Predicates: nonfixed a_block neq time object destination on source clear fixed different goal_time ren1
% 20.38/4.67 Fol Constants: block_1 block_2 block_3 block_4 table time_0 skc1
% 20.38/4.67 Fol Functions: s
% 20.38/4.67 Problem Properties:
% 20.38/4.67 This is a full first-order problem without equality.
% 20.38/4.67
% 20.38/4.67 After reduction: Problem Properties:
% 20.38/4.67 This is a full first-order problem without equality.
% 20.38/4.67
% 20.38/4.67
% 20.38/4.67 Reduced Input Clauses:
% 20.38/4.67
% 20.38/4.67 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)
% 20.38/4.67
% 20.38/4.67 === Starting SPASS-SCL-FOL A Little Less Naive, considering 66 atoms initially, heuristics mode: lmodel_grow ===
% 20.38/4.67
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 82
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 94
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 104
% 20.38/4.67 === Backtracking. Learning clause 64:4:3:[7.3,23.4]:TopTopTop: destination(x0,x1),nonfixed(x2),nonfixed(x0),on(x2,x0,x1) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 115
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 129
% 20.38/4.67 === Backtracking. Learning clause 65:4:3:[6.3,23.4]:TopTopTop: object(x0,x1),nonfixed(x2),nonfixed(x0),on(x2,x0,x1) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 150
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 167
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 172
% 20.38/4.67 === Backtracking. Learning clause 67:5:3:[17.2,66.5,8.3,6.3,23.4]:TopTopTop: time(x0),object(x1,x0),nonfixed(x2),nonfixed(x1),on(x2,x1,s(x0)) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 185
% 20.38/4.67 === Backtracking. Learning clause 69:6:1:[45.0,68.0,17.3,8.4,55.3]:Top: clear(block_2,x0),time(x0) -> clear(block_2,s(x0)),object(block_1,x0),object(block_3,x0),object(block_4,x0)
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 203
% 20.38/4.67 === Backtracking. Learning clause 70:8:3:[9.7,65.4]:TopTopTop: a_block(x1),neq(x0,x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1) -> object(x0,x2)
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 214
% 20.38/4.67 === Backtracking. Learning clause 72:6:2:[6.2,71.1,8.4,17.3,8.3]:TopTop: time(x0),object(x1,x0),nonfixed(x1),time(s(x0)) -> destination(x1,s(x0)),clear(x1,s(s(x0)))
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 226
% 20.38/4.67 === Backtracking. Learning clause 73:5:3:[27.2,15.3,26.2]:TopTopTop: a_block(x0),a_block(x1),destination(x0,x2),destination(x1,x2),different(x1,x0) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 247
% 20.38/4.67 === Backtracking. Learning clause 74:5:3:[27.1,26.2,14.3]:TopTopTop: different(x0,x1),a_block(x1),a_block(x0),source(x1,x2),source(x0,x2) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 259
% 20.38/4.67 === Backtracking. Learning clause 80:9:1:[46.0,75.1,42.0,76.5,45.0,77.7,47.0,78.9,44.0,79.10,10.3,7.3,4.4,54.4,18.3,17.3,7.2,17.3]:Top: time(s(x0)),time(x0),destination(block_3,x0),time(s(s(x0))),source(table,s(s(x0))),object(block_2,s(s(x0))),object(block_1,s(s(x0))) -> source(block_3,s(x0)),clear(block_4,s(s(x0)))
% 20.38/4.67 === Backtracking. Learning clause 81:9:3:[9.7,9.5]:TopTopTop: time(x2),on(x0,x1,x2),nonfixed(x0),a_block(x1),neq(x0,x1),time(s(x2)) -> object(x0,x2),object(x0,s(x2)),on(x0,x1,s(s(x2)))
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 271
% 20.38/4.67 === Backtracking. Learning clause 82:4:2:[6.3,4.4]:TopTop: object(x0,s(x1)),nonfixed(x0),time(x1),destination(x0,x1) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 286
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 302
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 315
% 20.38/4.67 === Backtracking. Learning clause 83:6:2:[3.4,8.3]:TopTop: time(x1),source(x0,x1),nonfixed(x0),time(s(x1)) -> destination(x0,s(x1)),clear(x0,s(s(x1)))
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 326
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 336
% 20.38/4.67 === Backtracking. Learning clause 84:8:3:[5.6,67.5]:TopTopTop: a_block(x1),neq(x0,x1),object(x0,s(x2)),source(x1,s(x2)),time(x2),object(x1,x2),nonfixed(x0),nonfixed(x1) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 343
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 355
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 363
% 20.38/4.67 === Backtracking. Learning clause 87:12:3:[40.0,85.4,42.0,86.9,5.6,22.8,53.4,18.2]:TopTopTop: object(x0,x1),nonfixed(x0),a_block(x2),neq(x0,x2),neq(x0,block_3),neq(x2,block_3),on(x0,x2,x1),time(x1),destination(table,x1) -> source(block_1,x1),source(block_2,x1),source(block_4,x1)
% 20.38/4.67 === Backtracking. Learning clause 88:2:2:[27.1,26.2]:TopTop: different(x0,x1) -> neq(x1,x0)
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 380
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 387
% 20.38/4.67 === Backtracking. Learning clause 89: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) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 396
% 20.38/4.67 === Backtracking. Learning clause 90:20:6:[5.6,12.5,81.8,70.5,13.4]:TopTopTopTopTopTop: source(x1,s(s(x2))),a_block(x1),neq(x0,x1),time(s(x2)),on(x0,x3,s(x2)),a_block(x3),neq(x0,x3),time(s(s(x2))),a_block(x0),neq(x4,x0),time(x2),on(x4,x0,x2),nonfixed(x0),nonfixed(x4),a_block(x5),neq(x4,x5),object(x5,x2) -> destination(x1,s(x2)),on(x0,x1,s(x2)),on(x0,x3,s(s(s(x2))))
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 425
% 20.38/4.67 === Backtracking. Learning clause 96:28:5:[39.0,91.8,88.1,92.9,45.0,93.10,41.0,94.11,47.0,95.21,5.6,22.8,10.4,10.3,5.5,10.3,74.5,10.4,22.8,6.3,6.3,55.3,70.8,81.7,5.4,12.5,7.2]:TopTopTopTopTop: a_block(x0),neq(block_4,x0),neq(block_4,block_2),neq(x0,block_2),on(block_4,x0,s(s(x1))),different(block_2,x2),a_block(x2),time(x1),neq(x2,block_4),time(s(x1)),on(x2,block_4,s(x1)),nonfixed(x2),on(block_4,x3,s(s(x1))),a_block(x3),neq(block_4,x3),time(s(s(s(x1)))),source(x4,s(s(s(x1)))),a_block(x4),neq(block_4,x4),time(s(s(x1))),nonfixed(x4) -> clear(block_2,x1),clear(x2,x1),object(block_1,s(s(s(x1)))),object(block_3,s(s(s(x1)))),on(block_4,x3,s(s(s(s(x1))))),on(block_4,x4,s(s(x1))),clear(x4,s(s(x1)))
% 20.38/4.67 === Backtracking. Learning clause 97:17:5:[5.4,81.8,11.5,70.5]:TopTopTopTopTop: source(x1,s(s(x2))),on(x0,x3,s(x2)),a_block(x3),neq(x0,x3),time(s(s(x2))),a_block(x1),neq(x0,x1),time(s(x2)),a_block(x0),neq(x4,x0),time(x2),on(x4,x0,x2),nonfixed(x4),nonfixed(x0) -> on(x0,x3,s(s(s(x2)))),on(x0,x1,s(x2)),object(x4,x2)
% 20.38/4.67 === Backtracking. Learning clause 100:27:6:[45.0,98.3,39.0,99.20,10.5,10.3,5.5,6.3,10.3,74.5,22.8,10.4,5.5,6.3,55.3,22.8]:TopTopTopTopTopTop: time(s(s(x0))),time(s(x0)),object(x1,s(s(x0))),different(block_2,x2),a_block(x2),nonfixed(x1),a_block(x3),neq(x1,x3),neq(x1,block_2),neq(x3,block_2),on(x1,x3,s(s(x0))),time(x0),object(x4,s(x0)),nonfixed(x2),object(x2,s(x0)),time(s(s(s(x0)))),nonfixed(x4),a_block(x5),neq(x4,x5),neq(x4,block_2),neq(x5,block_2),on(x4,x5,s(x0)) -> clear(block_2,x0),clear(x2,x0),object(block_1,s(s(s(x0)))),object(block_3,s(s(s(x0)))),object(block_4,s(s(s(x0))))
% 20.38/4.67 === Conflict found: 82:4:2:[6.3,4.4]:TopTop: object(x0,s(x1)),nonfixed(x0),time(x1),destination(x0,x1) -> {x0 -> block_1, x1 -> s(s(block_1))}
% 20.38/4.67 === Backtracking. Learning clause 102:6:1:[44.0,101.1,82.4,54.2]:Top: object(block_1,s(x0)),time(x0) -> destination(block_2,x0),destination(block_3,x0),destination(block_4,x0),destination(table,x0)
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 435
% 20.38/4.67 === Backtracking. Learning clause 105:25:7:[67.1,103.25,65.0,104.26,27.1,25.2,70.2,97.17,22.7,81.9]:TopTopTopTopTopTopTop: different(x0,x1),a_block(x1),on(x0,x1,x2),nonfixed(x0),source(x3,s(s(s(x2)))),time(s(s(s(x2)))),a_block(x3),neq(x4,x3),time(s(s(x2))),a_block(x4),neq(x1,x4),on(x1,x4,s(x2)),nonfixed(x1),a_block(x5),neq(x4,x5),neq(x6,x5),on(x4,x5,s(s(s(s(x2))))),time(x2),on(x4,x6,x2),nonfixed(x4),a_block(x6),neq(x4,x6),time(s(x2)) -> object(x0,x2),on(x4,x3,s(s(x2)))
% 20.38/4.67 === Backtracking. Learning clause 108:5:1:[44.0,106.1,45.0,107.3,55.2,16.2,6.2]:Top: time(x0),source(block_1,x0) -> object(block_3,x0),object(block_4,x0),clear(block_2,x0)
% 20.38/4.67 === Conflict found: 70:8:3:[9.7,65.4]:TopTopTop: a_block(x1),neq(x0,x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1) -> object(x0,x2) {x0 -> block_2, x1 -> block_3, x2 -> s(s(time_0))}
% 20.38/4.67 === Backtracking. Learning clause 112:16:3:[46.0,109.1,40.0,110.10,16.1,111.18,70.4,9.7,13.5,55.4,17.2,83.5,9.7]:TopTopTop: time(s(s(x0))),nonfixed(x1),a_block(x2),neq(x1,x2),object(x1,s(s(x0))),time(s(s(s(x0)))),source(x2,x0),time(s(x0)),nonfixed(x2),neq(x2,block_3),time(x0),on(x2,block_3,x0) -> object(block_1,s(s(s(x0)))),object(block_2,s(s(s(x0)))),object(block_4,s(s(s(x0)))),clear(x2,s(s(x0)))
% 20.38/4.67 === Conflict found: 70:8:3:[9.7,65.4]:TopTopTop: a_block(x1),neq(x0,x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1) -> object(x0,x2) {x0 -> block_2, x1 -> block_3, x2 -> s(s(time_0))}
% 20.38/4.67 === Backtracking. Learning clause 116:16:3:[46.0,113.0,40.0,114.1,6.1,115.13,70.5,55.4,81.9,13.5,6.2,10.3,112.7]:TopTopTop: time(s(s(x0))),nonfixed(x1),a_block(x2),neq(x1,x2),object(x1,s(s(x0))),time(s(s(s(x0)))),time(s(x0)),nonfixed(x2),neq(x2,block_3),time(x0),on(x2,block_3,x0) -> clear(x2,x0),object(block_1,s(s(s(x0)))),object(block_2,s(s(s(x0)))),object(block_4,s(s(s(x0)))),clear(x2,s(s(x0)))
% 20.38/4.67 === Backtracking. Learning clause 117:20:6:[9.6,13.4,22.7,12.7,73.4,8.4,9.7]:TopTopTopTopTopTop: time(s(x2)),a_block(x3),neq(x0,x3),object(x3,s(x2)),neq(x1,x4),neq(x0,x4),on(x0,x4,s(s(s(x2)))),a_block(x5),a_block(x4),different(x4,x5),nonfixed(x5),time(s(s(x2))),clear(x5,s(s(x2))),nonfixed(x0),a_block(x1),neq(x0,x1),time(x2),on(x0,x1,x2) -> clear(x5,s(s(s(x2)))),object(x0,x2)
% 20.38/4.67 === Backtracking. Learning clause 121:23:5:[40.0,118.6,46.0,119.7,6.1,120.21,11.5,12.7,13.4,73.4,8.4,81.8,70.4,55.4,13.5,116.16,27.2,25.2]:TopTopTopTopTop: neq(x0,x1),on(x0,x1,s(s(s(x2)))),nonfixed(x0),neq(x0,x3),a_block(x1),different(x1,x3),time(s(s(x2))),nonfixed(x4),a_block(x3),neq(x4,x3),object(x4,s(s(x2))),time(s(s(s(x2)))),time(s(x2)),nonfixed(x3),time(x2),on(x3,block_3,x2),different(x3,block_3) -> on(x0,x1,s(x2)),clear(x3,s(s(s(x2)))),clear(x3,x2),object(block_1,s(s(s(x2)))),object(block_2,s(s(s(x2)))),object(block_4,s(s(s(x2))))
% 20.38/4.67 === Backtracking. Learning clause 122:6:2:[7.2,72.5]:TopTop: time(x1),object(x0,x1),nonfixed(x0),time(s(x1)) -> clear(x0,s(x1)),clear(x0,s(s(x1)))
% 20.38/4.67 === Backtracking. Learning clause 123:11:4:[11.5,11.7,13.4]:TopTopTopTop: time(x2),a_block(x1),neq(x0,x1),time(s(x2)),on(x0,x1,s(s(x2))),nonfixed(x0),a_block(x3),neq(x0,x3),object(x3,x2) -> on(x0,x1,x2),object(x0,s(x2))
% 20.38/4.67 === Conflict found: 70:8:3:[9.7,65.4]:TopTopTop: a_block(x1),neq(x0,x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1) -> object(x0,x2) {x0 -> block_2, x1 -> block_3, x2 -> s(s(time_0))}
% 20.38/4.67 === Backtracking. Learning clause 124:12:3:[70.4,81.9,27.2,25.2,6.2]:TopTopTop: time(s(s(x1))),object(x0,s(s(s(x1)))),nonfixed(x0),time(x1),on(x2,x0,x1),a_block(x0),time(s(x1)),different(x2,x0),nonfixed(x2) -> object(x2,x1),object(x2,s(x1)),clear(x2,s(s(x1)))
% 20.38/4.67 === Conflict found: 70:8:3:[9.7,65.4]:TopTopTop: a_block(x1),neq(x0,x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1) -> object(x0,x2) {x0 -> block_2, x1 -> block_3, x2 -> s(s(time_0))}
% 20.38/4.67 === Backtracking. Learning clause 128:34:8:[46.0,125.0,40.0,126.2,44.0,127.27,70.4,81.9,27.2,25.2,17.2,8.4,124.12,123.9,121.11,55.4,65.1]:TopTopTopTopTopTopTopTop: on(x0,block_3,x1),different(x0,block_3),nonfixed(x0),a_block(x2),neq(x3,x2),on(x3,x2,s(s(s(x1)))),a_block(x0),neq(x3,x0),neq(x4,x5),on(x4,x5,s(s(s(x1)))),nonfixed(x4),neq(x4,x6),a_block(x5),different(x5,x6),time(s(s(x1))),nonfixed(x3),a_block(x6),neq(x3,x6),time(s(x1)),nonfixed(x6),time(x1),on(x6,block_3,x1),different(x6,block_3),time(s(s(s(x1)))),nonfixed(x7),on(x7,block_1,s(s(s(x1)))) -> clear(x0,s(s(s(x1)))),object(x0,x1),on(x3,x2,s(x1)),on(x4,x5,s(x1)),clear(x6,s(s(s(x1)))),clear(x6,x1),object(block_2,s(s(s(x1)))),object(block_4,s(s(s(x1))))
% 20.38/4.67 === Backtracking. Learning clause 129:13:4:[22.6,88.2,1.7,83.5]:TopTopTopTop: a_block(x2),neq(x0,x2),on(x0,x2,s(s(x3))),different(x2,x1),nonfixed(x0),a_block(x1),neq(x0,x1),object(x0,s(x3)),time(x3),source(x1,x3),nonfixed(x1),time(s(x3)) -> clear(x1,s(s(x3)))
% 20.38/4.67 === Backtracking. Learning clause 130:8:3:[27.1,25.2,70.2]:TopTopTop: different(x0,x1),a_block(x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1) -> object(x0,x2)
% 20.38/4.67 === Conflict found: 83:6:2:[3.4,8.3]:TopTop: time(x1),source(x0,x1),nonfixed(x0),time(s(x1)) -> destination(x0,s(x1)),clear(x0,s(s(x1))) {x0 -> block_2, x1 -> time_0}
% 20.38/4.67 === Backtracking. Learning clause 131:6:2:[83.5,17.3]:TopTop: time(x0),source(x1,x0),time(s(x0)),nonfixed(x1),object(x1,s(x0)) -> clear(x1,s(s(x0)))
% 20.38/4.67 === Backtracking. Learning clause 132:4:2:[8.3,6.3,17.3]:TopTop: time(x1),nonfixed(x0),object(x0,x1) -> clear(x0,s(x1))
% 20.38/4.67 === Conflict found: 70:8:3:[9.7,65.4]:TopTopTop: a_block(x1),neq(x0,x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1) -> object(x0,x2) {x0 -> block_3, x1 -> block_4, x2 -> s(time_0)}
% 20.38/4.67 === Backtracking. Learning clause 135:7:2:[41.0,133.2,46.0,134.6,70.7,47.1,9.7,65.1,27.2,25.2,33.1]:TopTop: time(s(x0)),object(block_4,s(s(x0))),time(x0),on(block_3,block_4,x0),nonfixed(x1),on(x1,block_3,x0) -> object(block_3,s(x0))
% 20.38/4.67 === Conflict found: 130:8:3:[27.1,25.2,70.2]:TopTopTop: different(x0,x1),a_block(x1),time(x2),on(x0,x1,x2),object(x1,s(x2)),nonfixed(x0),nonfixed(x1) -> object(x0,x2) {x0 -> block_3, x1 -> block_4, x2 -> time_0}
% 20.38/4.67 === Backtracking. Learning clause 138:5:2:[41.0,136.0,46.0,137.5,130.1,33.1,65.1,47.1]:TopTop: time(x0),on(block_3,block_4,x0),object(block_4,s(x0)),nonfixed(x1),on(x1,block_3,x0) ->
% 20.38/4.67 === Conflict found: 67:5:3:[17.2,66.5,8.3,6.3,23.4]:TopTopTop: time(x0),object(x1,x0),nonfixed(x2),nonfixed(x1),on(x2,x1,s(x0)) -> {x0 -> s(time_0), x1 -> block_3, x2 -> block_2}
% 20.38/4.67 === Backtracking. Learning clause 140:8:3:[46.0,139.1,67.2,135.7]:TopTopTop: nonfixed(x0),on(x0,block_3,s(s(x1))),time(s(x1)),object(block_4,s(s(x1))),time(x1),on(block_3,block_4,x1),nonfixed(x2),on(x2,block_3,x1) ->
% 20.38/4.67 === Conflict found: 88:2:2:[27.1,26.2]:TopTop: different(x0,x1) -> neq(x1,x0) {x0 -> block_2, x1 -> block_3}
% 20.38/4.67 === Backtracking. Learning clause 142:7:2:[46.0,141.0,88.1,31.1,13.3,39.1,135.7]:TopTop: object(block_2,s(x0)),time(s(x0)),object(block_4,s(s(x0))),time(x0),on(block_3,block_4,x0),nonfixed(x1),on(x1,block_3,x0) ->
% 20.38/4.67 === Conflict found: 132:4:2:[8.3,6.3,17.3]:TopTop: time(x1),nonfixed(x0),object(x0,x1) -> clear(x0,s(x1)) {x0 -> block_1, x1 -> time_0}
% 20.38/4.67 === Backtracking. Learning clause 143:17:5:[132.3,130.8,8.3,1.6,22.8,40.1,23.4]:TopTopTopTopTop: different(x1,x2),a_block(x2),time(x0),on(x1,x2,x0),object(x2,s(x0)),nonfixed(x2),time(s(x0)),object(x3,s(x0)),nonfixed(x3),neq(x3,block_3),a_block(x1),neq(x3,x1),neq(block_3,x1),on(x3,block_3,s(s(x0))),nonfixed(x4),nonfixed(x1),on(x4,x1,s(s(x0))) ->
% 20.38/4.67 === Backtracking. Learning clause 144:7:3:[11.3,88.2]:TopTopTop: nonfixed(x0),a_block(x1),time(x2),on(x0,x1,s(x2)),different(x1,x0) -> object(x0,x2),on(x0,x1,x2)
% 20.38/4.67 === Backtracking. Learning clause 153:21:5:[42.0,145.0,46.0,146.1,47.0,147.5,38.0,148.14,28.0,149.18,44.0,150.21,45.0,151.22,41.0,152.24,53.5,3.3,18.2,54.6,64.1,23.4,84.4,81.9,64.1,2.6,9.7,65.1,16.3,1.6,143.17,130.8,40.1,88.2,9.7,39.1]:TopTopTopTopTop: on(x0,block_4,x1),nonfixed(x0),neq(x0,block_4),neq(x2,block_3),on(x2,block_3,x1),nonfixed(x3),nonfixed(x2),on(x3,x2,x1),time(s(x1)),object(x4,s(x1)),neq(x4,block_3),neq(block_3,block_1),on(x4,block_3,s(s(x1))),nonfixed(x4),on(block_1,block_2,x1),object(block_2,s(x1)),different(block_1,x4),time(x1) -> destination(block_2,s(x1)),object(x0,x1),object(x0,s(x1))
% 20.38/4.67 === Backtracking. Learning clause 157:11:2:[45.0,154.6,28.0,155.9,46.0,156.12,25.1,31.1,27.1,153.4,27.2,25.2,33.1,65.1,67.2]:TopTop: on(block_3,block_4,x0),on(block_2,block_3,x0),nonfixed(x1),on(x1,block_2,x0),neq(block_3,block_1),on(block_2,block_3,s(s(x0))),on(block_1,block_2,x0),object(block_2,s(x0)),time(x0),time(s(x0)) -> destination(block_2,s(x0))
% 20.38/4.67 === Backtracking. Learning clause 160:9:2:[47.0,158.0,45.0,159.3,21.5,27.2,27.2,25.2,25.2,32.1,1.7,72.5,23.4]:TopTop: on(block_4,x0,s(s(x1))),different(x0,block_4),a_block(x0),neq(block_2,x0),object(block_2,s(x1)),time(x1),object(x0,x1),time(s(x1)),nonfixed(x0) ->
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 449
% 20.38/4.67 === Conflict found: 64:4:3:[7.3,23.4]:TopTopTop: destination(x0,x1),nonfixed(x2),nonfixed(x0),on(x2,x0,x1) -> {x0 -> block_4, x1 -> s(s(s(time_0))), x2 -> block_3}
% 20.38/4.67 === Backtracking. Learning clause 163:10:2:[47.0,161.0,41.0,162.2,64.4,9.7,54.5]:TopTop: nonfixed(x0),neq(x0,block_4),time(x1),on(x0,block_4,x1),time(s(x1)) -> object(x0,x1),destination(block_1,s(x1)),destination(block_2,s(x1)),destination(block_3,s(x1)),destination(table,s(x1))
% 20.38/4.67 === Backtracking. Learning clause 167:13:3:[45.0,164.4,47.0,165.10,46.0,166.13,55.3,89.3,89.3,16.2]:TopTopTop: time(x0),a_block(x1),neq(block_2,x1),source(x1,x0),nonfixed(x1),clear(x1,x0),a_block(x2),neq(block_4,x2),source(x2,x0),nonfixed(x2),clear(x2,x0),source(block_3,x0) -> object(block_1,x0)
% 20.38/4.67 === Backtracking. Learning clause 176:37:8:[42.0,168.0,41.0,169.1,38.0,170.14,44.0,171.17,40.0,172.20,45.0,173.27,47.0,174.34,46.0,175.36,3.3,53.5,23.4,18.2,9.7,13.4,163.10,1.6,70.4,55.2,5.5,84.3,84.3,16.2]:TopTopTopTopTopTopTopTop: neq(x0,block_4),on(x0,block_4,s(x1)),nonfixed(x0),a_block(x2),neq(x0,x2),object(x2,s(x1)),nonfixed(x3),neq(x3,block_4),time(x1),on(x3,block_4,x1),time(s(x1)),object(x4,s(x1)),neq(x4,block_1),nonfixed(x4),time(s(s(s(x1)))),nonfixed(x5),neq(x5,block_3),object(x5,s(x1)),a_block(x6),neq(block_2,x6),source(x6,s(s(s(x1)))),object(x6,s(s(x1))),nonfixed(x6),a_block(x7),neq(block_4,x7),source(x7,s(s(s(x1)))),time(s(s(x1))),object(x7,s(s(x1))),nonfixed(x7),source(block_3,s(s(s(x1)))) -> source(block_1,s(x1)),source(block_2,s(x1)),object(x3,x1),destination(block_2,s(x1)),destination(block_3,s(x1)),object(x4,s(s(x1))),on(x5,block_3,s(x1))
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 462
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 475
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 484
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 490
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 492
% 20.38/4.67 === Clause set with instances from active satisfied. Growing active. New size: 494
% 20.38/4.67
% 20.38/4.67 Linear Model Building succeeded.
% 20.38/4.67 SZS status Satisfiable
% 20.38/4.67
% 20.38/4.67 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.38/4.67
% 20.38/4.67 SPASS-SCL-FOL Statistics:
% 20.38/4.67 Number of learned clauses: 47
% 20.38/4.67 Number of propagations: 3123
% 20.38/4.67 Number of decisions: 1457
% 20.38/4.67 Number of resolutions: 199
% 20.38/4.67 Number of condensations: 6
% 20.38/4.67 Number of sub resolutions: 66
% 20.38/4.67 Number of input literals (deduplicated): 66
% 20.38/4.67 Number of grows: 35
% 20.38/4.67 Number of considered ground atoms: 494
% 20.38/4.67
% 20.38/4.67 Needed: 0:00:04.01
% 20.38/4.67
%------------------------------------------------------------------------------