%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP063+1 : TPTP v9.2.1. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:29:08 PM UTC 2026
% Result : CounterSatisfiable 21.24s 5.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : NLP063+1 : TPTP v9.2.1. Released v2.4.0.
% 0.12/0.15 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.37 % Computer : n002.cluster.edu
% 0.21/0.37 % Model : x86_64 x86_64
% 0.21/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.37 % Memory : 8042.1875MB
% 0.21/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.21/0.37 % CPULimit : 300
% 0.21/0.37 % WCLimit : 300
% 0.21/0.37 % DateTime : Thu May 7 12:44:47 EDT 2026
% 0.21/0.37 % CPUTime :
% 0.21/0.37 SPASS-SCL-FOL version:
% 0.31/0.47 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 21.24/5.82 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.24/5.82 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.24/5.82 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.24/5.82 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.24/5.82 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.24/5.82 Execution lmodel_grow ended with status: satisfiable
% 21.24/5.82 Used heuristic: lmodel_grow
% 21.24/5.82
% 21.24/5.82 Input Clauses:
% 21.24/5.82
% 21.24/5.82 Predicates: actual_world male member man of cannon event agent patient present nonreflexive fire from_loc six group shot ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8
% 21.24/5.82 Fol Constants: skc1 skc2 skc3 skc11 skc12 skc13
% 21.24/5.82 Fol Functions: skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf14 skf15 skf16
% 21.24/5.82 Problem Properties:
% 21.24/5.82 This is a full first-order problem without equality.
% 21.24/5.82
% 21.24/5.82 After reduction: Problem Properties:
% 21.24/5.82 This is a full first-order problem without equality.
% 21.24/5.82
% 21.24/5.82
% 21.24/5.82 Reduced Input Clauses:
% 21.24/5.82
% 21.24/5.82 Most General Atoms: ren1(x0,x1,x2,x3,x4,x5) man(x0,x1) of(x0,x1,x2) cannon(x0,x1) member(x0,x1,x2) event(x0,x1) agent(x0,x1,x2) patient(x0,x1,x3) present(x0,x1) nonreflexive(x0,x1) fire(x0,x1) from_loc(x0,x1,x4) ren2(x0,x2,x4,x5,x3,x6) ren3(x0,x1,x2) shot(x0,x1) ren4 actual_world(x0) male(x0,x1) six(x0,x2) group(x0,x2) ren5(x0,x1,x2,x3,x4) ren6(x0,x5,x6,x3) ren7(x0,x1,x2) ren8
% 21.24/5.82
% 21.24/5.82 === Starting SPASS-SCL-FOL A Little Less Naive, considering 80 atoms initially, heuristics mode: lmodel_grow ===
% 21.24/5.82
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 94
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 119
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 136
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 146
% 21.24/5.82 === Backtracking. Learning clause 44:4:15:[33.1,1.2,5.2,6.2,7.2,8.2,2.2,10.2,3.2,9.2,4.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ren1(x0,x1,x2,x3,x4,x5),ren1(x0,x6,x7,x8,x9,x10),ren1(x0,x11,x7,x12,x4,x13) -> ren6(x0,x5,x14,x8)
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 151
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 157
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 172
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 179
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 185
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 192
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 197
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 205
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 212
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 215
% 21.24/5.82 === Backtracking. Learning clause 45:3:2:[41.2,35.1]:TopTop: member(skc11,x0,skc13) -> ren8,ren7(skc11,x0,x1)
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 225
% 21.24/5.82 === Conflict found: 45:3:2:[41.2,35.1]:TopTop: member(skc11,x0,skc13) -> ren8,ren7(skc11,x0,x1) {x0 -> skf16(skc1,skc13), x1 -> skc13}
% 21.24/5.82 === Backtracking. Learning clause 46:2:1:[45.1,34.1]:Top: -> ren8,ren7(skc11,x0,skc13)
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 235
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 243
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 247
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 253
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 268
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 278
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 296
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 306
% 21.24/5.82 === Backtracking. Learning clause 47:6:3:[29.1,38.5]:TopTopTop: man(skc11,x0),of(skc11,x1,skc12),cannon(skc11,x1),member(skc11,x2,skc13) -> nonreflexive(skc11,skf14(x0,x1,x2)),ren8
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 317
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 332
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 344
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 355
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 368
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 386
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 399
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 412
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 424
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 437
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 449
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 460
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 471
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 481
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 492
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 502
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 513
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 528
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 537
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 544
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 553
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 561
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 570
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 581
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 590
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 598
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 606
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 615
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 622
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 632
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 640
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 652
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 662
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 670
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 681
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 695
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 703
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 712
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 725
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 736
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 744
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 754
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 762
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 772
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 781
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 791
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 799
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 808
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 819
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 827
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 836
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 846
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 856
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 868
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 881
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 891
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 900
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 911
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 922
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 934
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 944
% 21.24/5.82 === Backtracking. Learning clause 49:10:10:[13.0,48.1,33.2,12.1]:TopTopTopTopTopTopTopTopTopTop: man(x0,x1),event(x0,x2),agent(x0,x2,x1),patient(x0,x2,x3),present(x0,x2),nonreflexive(x0,x2),fire(x0,x2),from_loc(x0,x2,x4) -> ren6(x0,x3,x5,x6),ren2(x0,x7,x4,x6,x8,x9)
% 21.24/5.82 === Backtracking. Learning clause 50:6:3:[31.1,38.5]:TopTopTop: man(skc11,x0),of(skc11,x1,skc12),cannon(skc11,x1),member(skc11,x2,skc13) -> from_loc(skc11,skf14(x0,x1,x2),x1),ren8
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 961
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 979
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 994
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1010
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1021
% 21.24/5.82 === Backtracking. Learning clause 55:7:9:[25.1,51.3,28.1,52.6,29.1,53.7,30.1,54.8,33.10,31.2]:TopTopTopTopTopTopTopTopTop: man(x0,x1),of(x0,x2,x3),cannon(x0,x2),agent(x0,x4,x1),patient(x0,x4,x5),ren5(x0,x4,x6,x7,x2) -> ren6(x0,x5,x8,x3)
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1037
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1053
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1069
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1080
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1092
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1107
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1121
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1139
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1151
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1162
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1173
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1184
% 21.24/5.82 === Backtracking. Learning clause 56:6:3:[38.5,25.1]:TopTopTop: man(skc11,x0),of(skc11,x1,skc12),cannon(skc11,x1),member(skc11,x2,skc13) -> ren8,event(skc11,skf14(x0,x1,x2))
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1197
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1210
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1223
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1238
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1253
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1265
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1274
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1282
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1290
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1301
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1310
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1323
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1334
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1348
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1358
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1375
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1393
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1404
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1415
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1425
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1439
% 21.24/5.82 === Conflict found: 55:7:9:[25.1,51.3,28.1,52.6,29.1,53.7,30.1,54.8,33.10,31.2]:TopTopTopTopTopTopTopTopTop: man(x0,x1),of(x0,x2,x3),cannon(x0,x2),agent(x0,x4,x1),patient(x0,x4,x5),ren5(x0,x4,x6,x7,x2) -> ren6(x0,x5,x8,x3) {x0 -> skc11, x1 -> skc12, x2 -> skc1, x3 -> skc1, x4 -> skf14(skc12,skc1,skf15(skc12,skc1,skc1)), x5 -> skf15(skc12,skc1,skc1), x6 -> skc12, x7 -> skf15(skc12,skc1,skc1), x8 -> skc13}
% 21.24/5.82 === Backtracking. Learning clause 57:7:5:[55.5,27.2,26.2,38.5]:TopTopTopTopTop: of(skc11,x1,x2),man(skc11,x0),of(skc11,x1,skc12),cannon(skc11,x1),member(skc11,x3,skc13) -> ren6(skc11,x3,x4,x2),ren8
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1453
% 21.24/5.82 === Backtracking. Learning clause 58:7:6:[32.1,57.5]:TopTopTopTopTopTop: of(skc11,x0,x1),man(skc11,x2),of(skc11,x0,skc12),cannon(skc11,x0) -> ren6(skc11,x3,skc13,x4),ren6(skc11,x3,x5,x1),ren8
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1461
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1470
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1478
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1487
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1495
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1503
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1512
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1521
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1528
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1536
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1545
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1552
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1561
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1570
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1577
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1585
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1593
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1603
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1612
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1621
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1628
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1635
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1643
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1650
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1658
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1667
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1675
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1682
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1690
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1698
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1706
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1712
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1720
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1729
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1739
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1746
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1753
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1760
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1767
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1776
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1783
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1790
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1796
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1804
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1812
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1821
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1830
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1838
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1847
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1855
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1862
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1869
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1876
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1884
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1892
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1901
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1908
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1913
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1916
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1917
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1918
% 21.24/5.82 === Clause set with instances from active satisfied. Growing active. New size: 1919
% 21.24/5.82
% 21.24/5.82 Linear Model Building succeeded.
% 21.24/5.82 SZS status Satisfiable
% 21.24/5.82
% 21.24/5.82 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.24/5.82
% 21.24/5.82 SPASS-SCL-FOL Statistics:
% 21.24/5.82 Number of learned clauses: 10
% 21.24/5.82 Number of propagations: 3177
% 21.24/5.82 Number of decisions: 4914
% 21.24/5.82 Number of resolutions: 21
% 21.24/5.82 Number of condensations: 2
% 21.24/5.82 Number of sub resolutions: 5
% 21.24/5.82 Number of input literals (deduplicated): 45
% 21.24/5.82 Number of grows: 185
% 21.24/5.82 Number of considered ground atoms: 1919
% 21.24/5.82
% 21.24/5.82 Needed: 0:00:05.17
% 21.24/5.82
%------------------------------------------------------------------------------