%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PLA024+1 : TPTP v9.2.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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 0.81s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : PLA024+1 : TPTP v9.2.1. Bugfixed v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n004.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Thu May 7 12:56:03 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.18/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.81/0.65 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.81/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.81/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.81/0.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.81/0.65 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.81/0.65 Execution lmodel_grow ended with status: satisfiable
% 0.81/0.65 Used heuristic: lmodel_grow
% 0.81/0.65
% 0.81/0.65 Input Clauses:
% 0.81/0.66
% 0.81/0.66 Predicates: nonfixed a_block neq time object destination on source clear fixed different goal_time ren1
% 0.81/0.66 Fol Constants: block_1 block_2 block_3 table time_0 skc1
% 0.81/0.66 Fol Functions: s
% 0.81/0.66 Problem Properties:
% 0.81/0.66 This is a full first-order problem without equality.
% 0.81/0.66
% 0.81/0.66 After reduction: Problem Properties:
% 0.81/0.66 This is a full first-order problem without equality.
% 0.81/0.66
% 0.81/0.66
% 0.81/0.66 Reduced Input Clauses:
% 0.81/0.66
% 0.81/0.66 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(time_0)))) goal_time(skc1)
% 0.81/0.66
% 0.81/0.66 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: lmodel_grow ===
% 0.81/0.66
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 72
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 85
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 94
% 0.81/0.66 === Backtracking. Learning clause 58:5:2:[40.0,57.1,6.3,23.4,48.3]:TopTop: nonfixed(x0),on(x0,block_2,x1),time(x1) -> object(block_1,x1),object(block_3,x1)
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 109
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 116
% 0.81/0.66 === Backtracking. Learning clause 60:4:1:[40.0,59.1,48.3,6.2]:Top: time(x0) -> object(block_1,x0),object(block_3,x0),clear(block_2,x0)
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 125
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 129
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 136
% 0.81/0.66 === Backtracking. Learning clause 61:5:3:[27.1,26.2,14.3]:TopTopTop: different(x0,x1),a_block(x1),a_block(x0),source(x1,x2),source(x0,x2) ->
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 152
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 162
% 0.81/0.66 === Backtracking. Learning clause 67:15:3:[34.0,62.1,37.0,63.4,39.0,64.5,40.0,65.7,35.0,66.9,5.3,27.2,46.2,18.2,47.5,4.3,7.3,47.2,7.2,3.3,23.4,9.7]:TopTopTop: nonfixed(x0),object(x0,x1),ren1(x0,block_1),time(s(x1)),nonfixed(x2),neq(x2,block_2),time(x1),on(x2,block_2,x1) -> on(x0,block_1,x1),source(block_3,x1),destination(block_2,x1),destination(block_3,x1),destination(block_3,s(x1)),destination(table,s(x1)),object(x2,x1)
% 0.81/0.66 === Backtracking. Learning clause 72:11:2:[40.0,68.1,35.0,69.3,39.0,70.6,37.0,71.8,7.2,47.3,10.3,7.2,14.5,4.4,47.2,18.3]:TopTop: time(s(x0)),a_block(x1),neq(x1,block_2),source(x1,x0),time(x0),source(table,x0) -> destination(block_3,s(x0)),destination(table,s(x0)),clear(block_2,x0),destination(block_2,x0),destination(block_3,x0)
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 173
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 186
% 0.81/0.66 === Backtracking. Learning clause 75:4:1:[40.0,73.1,41.0,74.3,48.3,17.2,17.2]:Top: time(x0),destination(block_2,x0),destination(block_3,x0) -> object(block_1,x0)
% 0.81/0.66 === Backtracking. Learning clause 78:9:2:[41.0,76.0,39.0,77.6,5.4,48.4,10.4,6.2]:TopTop: a_block(x0),neq(block_3,x0),nonfixed(x0),time(x1),clear(x0,s(x1)) -> on(block_3,x0,x1),object(block_2,x1),clear(x0,x1),clear(block_1,x1)
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 199
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 207
% 0.81/0.66 === Backtracking. Learning clause 83:8:2:[40.0,79.0,35.0,80.3,39.0,81.7,41.0,82.9,10.4,61.4,60.4,17.2,16.2]:TopTop: time(x0),different(x1,block_2),a_block(x1),source(x1,x0),time(s(x0)),destination(block_1,s(x0)),source(block_3,s(x0)) -> clear(block_2,x0)
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 211
% 0.81/0.66 === Backtracking. Learning clause 85:12:3:[34.0,84.1,22.8,1.7,5.6,27.2,25.2,47.2]:TopTopTop: neq(x0,block_1),neq(x1,block_1),object(x1,x2),nonfixed(x1),a_block(x0),object(x1,s(x2)),source(x0,s(x2)),different(x1,x0),time(x2) -> destination(block_2,x2),destination(block_3,x2),destination(table,x2)
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 222
% 0.81/0.66 === Backtracking. Learning clause 91:16:3:[35.0,86.2,30.0,87.4,34.0,88.5,37.0,89.7,41.0,90.14,22.8,5.6,27.2,26.2,27.2,26.2,46.3,5.5,27.2,25.2,18.2,85.12,27.2,16.3,60.3]:TopTopTop: a_block(x0),on(block_3,x0,x1),different(block_2,x0),different(block_3,x0),neq(x2,block_1),a_block(x2),object(block_3,s(x1)),source(x2,s(x1)),different(block_3,x2),ren1(block_3,block_1),time(x1) -> on(block_3,block_1,x1),destination(block_2,x1),destination(block_3,x1),object(block_1,x1),clear(block_2,x1)
% 0.81/0.66 === Backtracking. Learning clause 93:16:3:[39.0,92.0,17.2,91.15,47.2]:TopTopTop: a_block(x0),on(block_3,x0,x1),different(block_2,x0),different(block_3,x0),neq(x2,block_1),a_block(x2),object(block_3,s(x1)),source(x2,s(x1)),different(block_3,x2),ren1(block_3,block_1),time(x1) -> on(block_3,block_1,x1),clear(block_2,x1),destination(block_2,x1),destination(block_3,x1),destination(table,x1)
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 228
% 0.81/0.66 === Backtracking. Learning clause 96:11:3:[37.0,94.2,40.0,95.8,1.7,22.7,47.5,4.3]:TopTopTop: object(x0,x1),nonfixed(x0),neq(x0,table),a_block(x2),neq(x0,x2),neq(table,x2),on(x0,x2,s(x1)),time(x1),clear(block_2,s(x1)) -> destination(block_1,x1),destination(block_3,x1)
% 0.81/0.66 === Backtracking. Learning clause 99:12:3:[35.0,97.2,40.0,98.8,5.6,22.7,10.4,60.4]:TopTopTop: object(x0,x1),nonfixed(x0),neq(x0,block_2),a_block(x2),neq(x0,x2),neq(block_2,x2),on(x0,x2,x1),time(x1),time(s(x1)) -> clear(block_2,x1),object(block_1,s(x1)),object(block_3,s(x1))
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 236
% 0.81/0.66 === Backtracking. Learning clause 100:7:3:[23.3,5.6]:TopTopTop: nonfixed(x1),clear(x1,x2),nonfixed(x0),a_block(x1),neq(x0,x1),object(x0,x2),source(x1,x2) ->
% 0.81/0.66 === Conflict found: 78:9:2:[41.0,76.0,39.0,77.6,5.4,48.4,10.4,6.2]:TopTop: a_block(x0),neq(block_3,x0),nonfixed(x0),time(x1),clear(x0,s(x1)) -> on(block_3,x0,x1),object(block_2,x1),clear(x0,x1),clear(block_1,x1) {x0 -> block_2, x1 -> s(s(time_0))}
% 0.81/0.66 === Backtracking. Learning clause 104:15:3:[40.0,101.0,39.0,102.4,41.0,103.7,78.7,16.2,22.7,27.2,10.3,4.4,26.2,1.7,3.4]:TopTopTop: source(block_2,s(x0)),a_block(x1),neq(block_3,x1),destination(block_1,x0),different(x2,x1),a_block(x2),neq(block_3,x2),time(x0),object(block_3,x0),destination(x2,x0),nonfixed(x1),time(s(x0)),source(x1,s(x0)) -> source(x1,x0),clear(x1,x0)
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 240
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 242
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 243
% 0.81/0.66 === Backtracking. Learning clause 105:2:2:[25.2,27.1]:TopTop: different(x0,x1) -> neq(x0,x1)
% 0.81/0.66 === Backtracking. Learning clause 106:2:0:[3.2,44.1,40.1]:: source(block_2,s(s(time_0))) -> clear(block_2,s(s(s(time_0))))
% 0.81/0.66 === Backtracking. Learning clause 109:3:0:[40.0,107.0,39.0,108.2,21.8,9.7,27.2,26.2,43.1,9.7,105.2,27.2,26.2,28.1,6.2,4.4,42.1,29.1,35.1,49.1,41.1,27.2,26.2,30.1]:: on(block_3,block_2,s(s(time_0))),destination(block_1,time_0) -> object(block_1,time_0)
% 0.81/0.66 === Conflict found: 99:12:3:[35.0,97.2,40.0,98.8,5.6,22.7,10.4,60.4]:TopTopTop: object(x0,x1),nonfixed(x0),neq(x0,block_2),a_block(x2),neq(x0,x2),neq(block_2,x2),on(x0,x2,x1),time(x1),time(s(x1)) -> clear(block_2,x1),object(block_1,s(x1)),object(block_3,s(x1)) {x0 -> block_3, x1 -> s(time_0), x2 -> block_1}
% 0.81/0.66 === Backtracking. Learning clause 112:15:4:[41.0,110.9,39.0,111.13,99.12,5.4,16.2]:TopTopTopTop: object(x0,x1),nonfixed(x0),neq(x0,block_2),a_block(x2),neq(x0,x2),neq(block_2,x2),on(x0,x2,x1),time(x1),time(s(x1)),a_block(x3),neq(block_3,x3),source(x3,s(x1)),source(block_1,s(x1)) -> clear(block_2,x1),on(block_3,x3,s(x1))
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 251
% 0.81/0.66 === Backtracking. Learning clause 114:10:2:[35.0,113.2,5.6,12.5,46.3]:TopTop: object(x0,s(x1)),nonfixed(x0),neq(x0,block_2),time(x1),time(s(x1)) -> destination(block_2,x1),on(x0,block_2,x1),source(block_1,s(x1)),source(block_3,s(x1)),source(table,s(x1))
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 255
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 257
% 0.81/0.66 === Clause set with instances from active satisfied. Growing active. New size: 260
% 0.81/0.66
% 0.81/0.66 Linear Model Building succeeded.
% 0.81/0.66 SZS status Satisfiable
% 0.81/0.66
% 0.81/0.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.81/0.66
% 0.81/0.66 SPASS-SCL-FOL Statistics:
% 0.81/0.66 Number of learned clauses: 20
% 0.81/0.66 Number of propagations: 1192
% 0.81/0.66 Number of decisions: 601
% 0.81/0.66 Number of resolutions: 94
% 0.81/0.66 Number of condensations: 0
% 0.81/0.66 Number of sub resolutions: 38
% 0.81/0.66 Number of input literals (deduplicated): 55
% 0.81/0.66 Number of grows: 25
% 0.81/0.66 Number of considered ground atoms: 260
% 0.81/0.66
% 0.81/0.66 Needed: 0:00:00.11
% 0.81/0.66
%------------------------------------------------------------------------------