%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : LCL665+1.001 : TPTP v9.2.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n001.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:11 PM UTC 2026 % Result : CounterSatisfiable 9.59s 2.50s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : LCL665+1.001 : TPTP v9.2.1. Released v4.0.0. % 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.14/0.34 % Computer : n001.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu May 7 12:38:49 EDT 2026 % 0.14/0.34 % CPUTime : % 0.14/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 9.59/2.50 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.59/2.50 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.59/2.50 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.59/2.50 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.59/2.50 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 9.59/2.50 Execution lmodel_grow ended with status: satisfiable % 9.59/2.50 Used heuristic: lmodel_grow % 9.59/2.50 % 9.59/2.50 Input Clauses: % 9.59/2.50 % 9.59/2.50 Predicates: r1 p26 p25 p24 p22 p16 p14 p23 p15 p21 p13 p11 p12 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 % 9.59/2.50 Fol Constants: skc1 skc14 skc15 skc16 skc17 % 9.59/2.50 Fol Functions: skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 % 9.59/2.50 Problem Properties: % 9.59/2.50 This is a full first-order problem without equality. % 9.59/2.50 % 9.59/2.50 After reduction: Problem Properties: % 9.59/2.50 This is a full first-order problem without equality. % 9.59/2.50 % 9.59/2.50 % 9.59/2.50 Reduced Input Clauses: % 9.59/2.50 % 9.59/2.50 Most General Atoms: r1(x0,x1) ren1(x1,x0) ren2(x1,x0) ren3(x1,x0) ren4(x1,x0) ren5(x1,x0) ren6(x1,x0) p23(x0) ren7(x1,x0) p21(x0) ren8(x1,x0) ren9(x1,x0) ren10(x1,x0) ren11(x1,x0) ren12(x1,x0) p26(x1) p25(x1) p24(x1) p22(x1) p16(x0) p14(x0) p15(x0) p13(x0) p11(x0) p12(skc16) % 9.59/2.50 % 9.59/2.50 === Starting SPASS-SCL-FOL A Little Less Naive, considering 84 atoms initially, heuristics mode: lmodel_grow === % 9.59/2.50 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 97 % 9.59/2.50 === Backtracking. Learning clause 50:2:1:[26.3,3.1,2.1,30.2]:Top: r1(skc1,x0) -> p16(x0) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 112 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 120 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 128 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 132 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 136 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 141 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 146 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 149 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 154 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 159 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 164 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 170 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 176 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 181 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 187 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 192 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 197 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 202 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 207 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 212 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 217 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 222 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 227 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 231 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 235 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 239 % 9.59/2.50 === Backtracking. Learning clause 51:2:1:[29.3,13.1,12.1,35.2]:Top: r1(skc1,x0) -> p14(x0) % 9.59/2.50 === Backtracking. Learning clause 52:2:2:[29.3,13.1,12.1]:TopTop: r1(skc1,x0) -> ren6(x0,x1) % 9.59/2.50 === Backtracking. Learning clause 53:2:2:[26.2,2.1,3.1]:TopTop: r1(skc1,x0) -> ren1(x0,x1) % 9.59/2.50 === Backtracking. Learning clause 54:1:1:[29.1,48.1,13.1,12.1]:Top: -> ren6(skc17,x0) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 245 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 249 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 253 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 256 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 260 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 264 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 268 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 272 % 9.59/2.50 === Backtracking. Learning clause 55:3:3:[9.1,28.3]:TopTopTop: r1(skc1,x0),r1(x0,x1) -> ren4(x2,x1) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 279 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 286 % 9.59/2.50 === Backtracking. Learning clause 57:2:2:[5.0,56.2,4.1,26.2]:TopTop: r1(skc1,x0) -> ren2(x0,x1) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 295 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 304 % 9.59/2.50 === Backtracking. Learning clause 58:2:2:[8.1,55.2]:TopTop: r1(skc1,x0) -> ren4(x0,x1) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 309 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 314 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 319 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 324 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 329 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 334 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 340 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 345 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 350 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 356 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 360 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 365 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 370 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 375 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 380 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 385 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 389 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 393 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 397 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 401 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 405 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 409 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 413 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 417 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 420 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 427 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 432 % 9.59/2.50 === Backtracking. Learning clause 59:3:2:[22.1,29.2]:TopTop: r1(skc1,x0) -> ren11(x0,x1),p22(x1) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 436 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 439 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 445 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 451 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 456 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 461 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 464 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 469 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 474 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 479 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 484 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 489 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 494 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 499 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 504 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 509 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 514 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 519 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 524 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 529 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 533 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 536 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 541 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 546 % 9.59/2.50 === Backtracking. Learning clause 60:3:2:[24.1,26.2]:TopTop: r1(skc1,x0) -> ren12(x0,x1),p26(x1) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 550 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 553 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 555 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 558 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 561 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 564 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 567 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 571 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 574 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 577 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 580 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 583 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 586 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 590 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 594 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 599 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 604 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 607 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 610 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 613 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 617 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 620 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 624 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 627 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 630 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 633 % 9.59/2.50 === Backtracking. Learning clause 61:3:2:[20.1,28.2]:TopTop: r1(skc1,x0) -> ren10(x0,x1),p24(x1) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 640 % 9.59/2.50 === Backtracking. Learning clause 63:2:2:[11.0,62.2,10.1,29.2]:TopTop: r1(skc1,x0) -> ren5(x0,x1) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 649 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 657 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 664 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 671 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 679 % 9.59/2.50 === Backtracking. Learning clause 64:3:2:[18.1,26.2]:TopTop: r1(skc1,x0) -> ren9(x0,x1),p26(x1) % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 691 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 703 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 713 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 722 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 730 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 739 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 749 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 757 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 765 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 772 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 779 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 786 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 794 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 800 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 809 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 816 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 822 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 827 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 832 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 837 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 842 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 848 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 854 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 859 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 865 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 871 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 876 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 882 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 886 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 889 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 892 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 896 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 901 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 905 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 909 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 913 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 916 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 919 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 922 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 925 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 930 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 933 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 936 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 938 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 941 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 945 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 949 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 952 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 955 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 959 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 963 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 966 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 970 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 973 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 976 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 980 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 985 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 992 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 998 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1002 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1006 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1011 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1016 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1019 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1022 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1025 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1029 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1033 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1036 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1039 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1042 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1045 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1049 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1053 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1056 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1059 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1062 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1065 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1068 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1071 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1075 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1079 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1082 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1086 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1090 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1095 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1099 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1102 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1106 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1110 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1113 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1116 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1118 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1121 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1123 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1124 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1126 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1127 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1130 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1133 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1136 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1140 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1144 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1147 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1149 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1152 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1155 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1159 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1163 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1167 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1170 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1175 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1179 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1182 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1184 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1188 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1190 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1194 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1196 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1198 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1200 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1201 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1202 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1203 % 9.59/2.50 === Clause set with instances from active satisfied. Growing active. New size: 1204 % 9.59/2.50 % 9.59/2.50 Linear Model Building succeeded. % 9.59/2.50 SZS status Satisfiable % 9.59/2.50 % 9.59/2.50 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 9.59/2.50 % 9.59/2.50 SPASS-SCL-FOL Statistics: % 9.59/2.50 Number of learned clauses: 13 % 9.59/2.50 Number of propagations: 2708 % 9.59/2.50 Number of decisions: 2576 % 9.59/2.50 Number of resolutions: 21 % 9.59/2.50 Number of condensations: 4 % 9.59/2.50 Number of sub resolutions: 2 % 9.59/2.50 Number of input literals (deduplicated): 46 % 9.59/2.50 Number of grows: 247 % 9.59/2.50 Number of considered ground atoms: 1204 % 9.59/2.50 % 9.59/2.50 Needed: 0:00:01.92 % 9.59/2.50 %------------------------------------------------------------------------------