%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : LCL647+1.001 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:28:06 PM UTC 2026
% Result : CounterSatisfiable 136.95s 28.07s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL647+1.001 : TPTP v9.2.1. Released v4.0.0.
% 0.13/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n013.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 12:34:57 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 136.95/28.07 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 136.95/28.07 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 136.95/28.07 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 136.95/28.07 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 136.95/28.07 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 136.95/28.07 Execution lmodel_grow ended with status: satisfiable
% 136.95/28.07 Used heuristic: lmodel_grow
% 136.95/28.07
% 136.95/28.07 Input Clauses:
% 136.95/28.07
% 136.95/28.07 Predicates: r1 p6 p5 p4 p2 p3 p1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12
% 136.95/28.07 Fol Constants: skc1 skc14 skc15 skc16 skc17
% 136.95/28.07 Fol Functions: skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13
% 136.95/28.07 Problem Properties:
% 136.95/28.07 This is a full first-order problem without equality.
% 136.95/28.07
% 136.95/28.07 After reduction: Problem Properties:
% 136.95/28.07 This is a full first-order problem without equality.
% 136.95/28.07
% 136.95/28.07
% 136.95/28.07 Reduced Input Clauses:
% 136.95/28.07
% 136.95/28.07 Most General Atoms: r1(x0,x1) ren1(x1,x0) ren2(x1,x0) ren3(x1,x0) ren4(x1,x0) ren5(x1,x0) ren6(x1,x0) p3(x0) ren7(x1,x0) p1(x0) ren8(x1,x0) ren9(x1,x0) ren10(x1,x0) ren11(x1,x0) ren12(x1,x0) p6(x1) p4(x1) p2(x1) p5(x0)
% 136.95/28.07
% 136.95/28.07 === Starting SPASS-SCL-FOL A Little Less Naive, considering 72 atoms initially, heuristics mode: lmodel_grow ===
% 136.95/28.07
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 94
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 115
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 144
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 165
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 188
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 208
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 227
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 246
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 275
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 297
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 316
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 335
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 357
% 136.95/28.07 === Backtracking. Learning clause 49:3:3:[28.3,10.1]:TopTopTop: r1(skc1,x0),r1(x0,x1) -> ren5(x2,x1)
% 136.95/28.07 === Backtracking. Learning clause 50:2:2:[9.1,49.2,33.2,2.1]:TopTop: r1(skc1,x0) -> ren1(x1,x0)
% 136.95/28.07 === Backtracking. Learning clause 51:2:1:[9.1,49.2,33.2]:Top: r1(skc1,x0) -> p6(x0)
% 136.95/28.07 === Conflict found: 51:2:1:[9.1,49.2,33.2]:Top: r1(skc1,x0) -> p6(x0) {x0 -> skc15}
% 136.95/28.07 === Backtracking. Learning clause 52:1:0:[51.1,43.1]:: -> p6(skc15)
% 136.95/28.07 === Backtracking. Learning clause 53:2:2:[9.1,49.2]:TopTop: r1(skc1,x0) -> ren5(x0,x1)
% 136.95/28.07 === Backtracking. Learning clause 54:1:1:[1.1,50.1]:Top: -> ren1(skc1,x0)
% 136.95/28.07 === Backtracking. Learning clause 55:2:2:[27.2,5.1,6.1]:TopTop: r1(skc1,x0) -> ren3(x0,x1)
% 136.95/28.07 === Backtracking. Learning clause 56:2:2:[28.2,11.1,12.1]:TopTop: r1(skc1,x0) -> ren6(x0,x1)
% 136.95/28.07 === Backtracking. Learning clause 58:1:0:[43.0,57.0,37.3,44.1]:: ren9(skc15,skf10(skc15)) ->
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 389
% 136.95/28.07 === Backtracking. Learning clause 59:2:1:[34.2,56.2]:Top: r1(skc1,x0) -> p4(x0)
% 136.95/28.07 === Conflict found: 59:2:1:[34.2,56.2]:Top: r1(skc1,x0) -> p4(x0) {x0 -> skf5(skc1)}
% 136.95/28.07 === Backtracking. Learning clause 60:1:1:[59.2,8.1,7.1]:Top: -> ren4(skc1,x0)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 416
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 440
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 456
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 471
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 484
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 497
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 507
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 518
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 528
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 538
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 548
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 558
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 569
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 579
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 590
% 136.95/28.07 === Backtracking. Learning clause 61:2:2:[27.3,8.1,7.1]:TopTop: r1(skc1,x0) -> ren4(x0,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 610
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 624
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 638
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 647
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 657
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 663
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 670
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 677
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 683
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 688
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 693
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 698
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 703
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 708
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 713
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 718
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 724
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 729
% 136.95/28.07 === Backtracking. Learning clause 62:3:2:[3.1,27.2]:TopTop: r1(skc1,x0) -> ren2(x0,x1),p4(x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 752
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 761
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 767
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 773
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 778
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 783
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 789
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 793
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 799
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 804
% 136.95/28.07 === Backtracking. Learning clause 64:2:2:[4.0,63.2,3.1,25.2]:TopTop: r1(skc1,x0) -> ren2(x0,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 814
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 820
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 827
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 835
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 843
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 849
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 855
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 862
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 868
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 875
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 882
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 890
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 898
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 906
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 916
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 926
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 933
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 941
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 949
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 956
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 963
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 970
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 976
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 982
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 988
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 993
% 136.95/28.07 === Backtracking. Learning clause 65:3:2:[23.1,27.2]:TopTop: r1(skc1,x0) -> ren12(x0,x1),p4(x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1012
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1028
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1038
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1049
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1059
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1069
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1083
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1093
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1101
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1108
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1115
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1121
% 136.95/28.07 === Backtracking. Learning clause 66:3:3:[2.1,25.3]:TopTopTop: r1(skc1,x0),r1(x0,x1) -> ren1(x2,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1137
% 136.95/28.07 === Backtracking. Learning clause 67:2:2:[1.1,66.2]:TopTop: r1(skc1,x0) -> ren1(x0,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1152
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1168
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1180
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1193
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1206
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1217
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1228
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1236
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1242
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1247
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1252
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1257
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1261
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1265
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1270
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1274
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1279
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1284
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1288
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1295
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1300
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1305
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1311
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1317
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1323
% 136.95/28.07 === Backtracking. Learning clause 68:3:2:[28.2,21.1]:TopTop: r1(skc1,x0) -> p2(x1),ren11(x0,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1347
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1363
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1371
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1378
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1384
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1390
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1396
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1402
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1407
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1412
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1417
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1422
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1427
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1433
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1440
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1446
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1451
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1457
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1463
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1469
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1474
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1478
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1482
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1486
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1491
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1495
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1498
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1501
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1504
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1507
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1510
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1512
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1514
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1516
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1518
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1520
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1522
% 136.95/28.07 === Backtracking. Learning clause 69:3:2:[28.2,17.1]:TopTop: r1(skc1,x0) -> p2(x1),ren9(x0,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1549
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1573
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1595
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1619
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1643
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1671
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1696
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1728
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1761
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1785
% 136.95/28.07 === Backtracking. Learning clause 70:3:2:[27.2,13.1]:TopTop: r1(skc1,x0) -> p4(x1),ren7(x0,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1818
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1853
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1884
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1910
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1935
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1956
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 1980
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2000
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2023
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2044
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2068
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2090
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2114
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2129
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2146
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2162
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2179
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2188
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2198
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2208
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2218
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2225
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2233
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2241
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2249
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2256
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2263
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2270
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2277
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2283
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2289
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2295
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2300
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2306
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2312
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2318
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2324
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2331
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2338
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2345
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2352
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2357
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2362
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2368
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2372
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2376
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2380
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2384
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2388
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2392
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2397
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2401
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2405
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2409
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2413
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2417
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2421
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2425
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2429
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2433
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2438
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2444
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2449
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2454
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2459
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2464
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2469
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2474
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2479
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2484
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2488
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2492
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2495
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2499
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2503
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2506
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2509
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2513
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2519
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2524
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2529
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2532
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2537
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2541
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2546
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2549
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2553
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2559
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2563
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2567
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2571
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2575
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2579
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2583
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2587
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2591
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2595
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2598
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2602
% 136.95/28.07 === Backtracking. Learning clause 72:2:1:[20.0,71.1,23.1,28.2,40.2,19.1]:Top: -> p2(skf13(x0)),ren10(skc1,x0)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2625
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2643
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2656
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2667
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2679
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2688
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2698
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2706
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2715
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2722
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2730
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2737
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2744
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2751
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2758
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2765
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2772
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2778
% 136.95/28.07 === Backtracking. Learning clause 73:3:2:[28.2,19.1]:TopTop: r1(skc1,x0) -> p2(x1),ren10(x0,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2800
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2817
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2827
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2837
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2845
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2855
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2863
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2871
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2878
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2885
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2891
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2898
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2905
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2911
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2915
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2920
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2925
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2929
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2934
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2939
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2944
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2949
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2954
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2959
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2964
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2970
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2975
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2980
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2985
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2991
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 2996
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3001
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3007
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3013
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3018
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3023
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3028
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3033
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3037
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3041
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3045
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3049
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3053
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3059
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3063
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3067
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3072
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3075
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3080
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3085
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3090
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3095
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3101
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3108
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3115
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3123
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3130
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3138
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3144
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3152
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3159
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3167
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3173
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3178
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3184
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3189
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3196
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3200
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3204
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3208
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3212
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3215
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3218
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3221
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3224
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3228
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3233
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3237
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3240
% 136.95/28.07 === Backtracking. Learning clause 74:3:2:[25.2,17.1]:TopTop: r1(skc1,x0) -> p6(x1),ren9(x0,x1)
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3264
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3281
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3294
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3307
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3317
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3326
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3335
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3341
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3347
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3353
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3359
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3365
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3371
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3376
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3381
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3386
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3390
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3394
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3398
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3402
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3406
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3411
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3415
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3420
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3425
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3430
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3435
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3440
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3446
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3451
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3456
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3461
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3466
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3471
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3476
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3481
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3486
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3491
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3495
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3499
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3503
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3507
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3512
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3516
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3520
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3524
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3528
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3532
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3535
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3538
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3543
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3547
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3550
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3553
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3556
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3559
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3562
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3566
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3569
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3573
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3577
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3581
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3584
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3587
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3590
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3593
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3596
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3599
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3603
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3609
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3616
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3620
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3624
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3628
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3631
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3635
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3638
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3643
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3648
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3654
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3659
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3664
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3666
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3669
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3672
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3675
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3679
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3682
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3685
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3688
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3692
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3696
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3700
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3703
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3706
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3709
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3712
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3716
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3721
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3724
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3727
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3730
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3733
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3736
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3739
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3742
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3745
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3747
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3748
% 136.95/28.07 === Clause set with instances from active satisfied. Growing active. New size: 3749
% 136.95/28.07
% 136.95/28.07 Linear Model Building succeeded.
% 136.95/28.07 SZS status Satisfiable
% 136.95/28.07
% 136.95/28.07 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 136.95/28.07
% 136.95/28.07 SPASS-SCL-FOL Statistics:
% 136.95/28.07 Number of learned clauses: 23
% 136.95/28.07 Number of propagations: 11163
% 136.95/28.07 Number of decisions: 11725
% 136.95/28.07 Number of resolutions: 32
% 136.95/28.07 Number of condensations: 7
% 136.95/28.07 Number of sub resolutions: 3
% 136.95/28.07 Number of input literals (deduplicated): 40
% 136.95/28.07 Number of grows: 474
% 136.95/28.07 Number of considered ground atoms: 3749
% 136.95/28.07
% 136.95/28.07 Needed: 0:0:27.48
% 136.95/28.07
%------------------------------------------------------------------------------