%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO525+1.015 : TPTP v9.2.1. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:41:06 PM UTC 2026
% Result : Theorem 61.84s 12.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYO525+1.015 : TPTP v9.2.1. Released v5.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n005.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 13:54:31 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]
% 61.84/12.95 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.84/12.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.84/12.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.84/12.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.84/12.95 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.84/12.95 Execution lmodel_grow ended with status: unsatisfiable
% 61.84/12.95 Used heuristic: lmodel_grow
% 61.84/12.95
% 61.84/12.95 Input Clauses:
% 61.84/12.95
% 61.84/12.95 Predicates: bin_count goal
% 61.84/12.95 Fol Constants: n0 n1
% 61.84/12.95 Fol Functions:
% 61.84/12.95 Problem Properties:
% 61.84/12.95 This is a Bernays Schoenfinkel problem.
% 61.84/12.95
% 61.84/12.95 After reduction: Problem Properties:
% 61.84/12.95 This is a Bernays Schoenfinkel problem.
% 61.84/12.95
% 61.84/12.95
% 61.84/12.95 Reduced Input Clauses:
% 61.84/12.95 31:1:12:[30.0,2.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) ->
% 61.84/12.95
% 61.84/12.95 Most General Atoms: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,n0) bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,n1) goal
% 61.84/12.95
% 61.84/12.95 === Starting SPASS-SCL-FOL A Little Less Naive, considering 64 atoms initially, heuristics mode: lmodel_grow ===
% 61.84/12.95
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 84
% 61.84/12.95 === Backtracking. Learning clause 32:2:22:[4.2,3.1,3.2,7.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n1,n1,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n0,n0,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 107
% 61.84/12.95 === Backtracking. Learning clause 33:2:24:[4.1,3.2,3.1,5.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,n0,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 130
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 153
% 61.84/12.95 === Backtracking. Learning clause 34:2:25:[4.1,3.2,3.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 172
% 61.84/12.95 === Conflict found: 33:2:24:[4.1,3.2,3.1,5.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,n0,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n0, x17 -> n0, x18 -> n1, x19 -> n1, x20 -> n1, x21 -> n0, x22 -> n1, x23 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 35:2:21:[33.1,34.2,8.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n1,n1,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n0,n0,n0,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 192
% 61.84/12.95 === Conflict found: 34:2:25:[4.1,3.2,3.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n0, x17 -> n1, x18 -> n1, x19 -> n1, x20 -> n1, x21 -> n1, x22 -> n0, x23 -> n0, x24 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 36:2:24:[34.2,33.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 210
% 61.84/12.95 === Backtracking. Learning clause 37:2:23:[6.1,36.2,36.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 227
% 61.84/12.95 === Conflict found: 34:2:25:[4.1,3.2,3.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n1, x17 -> n0, x18 -> n0, x19 -> n0, x20 -> n1, x21 -> n1, x22 -> n0, x23 -> n1, x24 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 38:2:23:[34.1,6.2,5.1,36.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,n1,n1,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 243
% 61.84/12.95 === Backtracking. Learning clause 39:2:23:[6.1,36.2,3.1,4.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,n1,n0,n1,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 259
% 61.84/12.95 === Conflict found: 32:2:22:[4.2,3.1,3.2,7.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n1,n1,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n1, x17 -> n0, x18 -> n0, x19 -> n0, x20 -> n0, x21 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 40:2:21:[32.1,38.2,37.1,35.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n1,n1,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 274
% 61.84/12.95 === Backtracking. Learning clause 41:2:20:[7.1,37.2,37.1,9.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n1,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n0,n0,n0,n0,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 292
% 61.84/12.95 === Backtracking. Learning clause 42:2:24:[3.2,33.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,n0,n1,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 306
% 61.84/12.95 === Backtracking. Learning clause 43:2:22:[7.2,36.1,37.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n0,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 320
% 61.84/12.95 === Conflict found: 32:2:22:[4.2,3.1,3.2,7.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n1,n1,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n1, x17 -> n1, x18 -> n1, x19 -> n0, x20 -> n0, x21 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 44:2:22:[32.1,38.2,37.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 335
% 61.84/12.95 === Conflict found: 44:2:22:[32.1,38.2,37.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n1, x17 -> n1, x18 -> n1, x19 -> n0, x20 -> n0, x21 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 45:2:18:[44.2,8.1,11.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n0,n0,n1,n0,n0,n0,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 351
% 61.84/12.95 === Backtracking. Learning clause 46:2:21:[8.1,44.2,44.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 368
% 61.84/12.95 === Backtracking. Learning clause 47:2:22:[6.1,43.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n1,n0,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 381
% 61.84/12.95 === Conflict found: 35:2:21:[33.1,34.2,8.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n1,n1,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n1, x17 -> n0, x18 -> n0, x19 -> n1, x20 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 48:2:21:[35.1,47.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n0,n0,n0,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 397
% 61.84/12.95 === Conflict found: 41:2:20:[7.1,37.2,37.1,9.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n1,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n0,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n1, x17 -> n1, x18 -> n0, x19 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 49:2:20:[41.2,46.1,48.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 406
% 61.84/12.95 === Conflict found: 41:2:20:[7.1,37.2,37.1,9.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n1,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n0,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1, x16 -> n1, x17 -> n1, x18 -> n1, x19 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 50:2:20:[41.2,46.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n1,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 413
% 61.84/12.95 === Backtracking. Learning clause 51:2:19:[10.2,49.1,50.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n0,n0,n1,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 421
% 61.84/12.95 === Conflict found: 48:2:21:[35.1,47.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1, x16 -> n1, x17 -> n1, x18 -> n0, x19 -> n0, x20 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 52:2:19:[48.2,51.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 430
% 61.84/12.95 === Conflict found: 45:2:18:[44.2,8.1,11.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n0,n0,n1,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1, x16 -> n1, x17 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 53:2:18:[45.1,52.2,51.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 54:2:20:[9.2,48.1,46.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n1,n0,n0,n0,n0,n0)
% 61.84/12.95 === Backtracking. Learning clause 55:2:19:[10.2,54.1,49.2,37.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n1,n1,n1,n0,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 436
% 61.84/12.95 === Backtracking. Learning clause 56:2:16:[10.1,46.2,49.1,12.1,53.1,13.1,53.1,12.1,53.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 57:2:16:[13.1,53.2,53.1,12.2,49.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 58:2:15:[14.2,53.1,53.2,12.2,12.1,53.2,52.1,11.1,49.1,10.1,54.1,13.2,53.2,12.2,53.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,n1,n0,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0)
% 61.84/12.95 === Conflict found: 49:2:20:[41.2,46.1,48.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1, x16 -> n1, x17 -> n1, x18 -> n0, x19 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 59:2:18:[49.2,45.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n1,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n0,n0,n1,n0,n0,n0,n0,n0)
% 61.84/12.95 === Backtracking. Learning clause 60:2:21:[8.1,42.2,44.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n1,n1,n0,n1,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 446
% 61.84/12.95 === Backtracking. Learning clause 61:2:16:[12.2,53.1,53.2,13.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 62:2:19:[10.1,46.2,49.1,9.2,37.2,7.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n0,n0,n1,n0,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 61:2:16:[12.2,53.1,53.2,13.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 63:1:12:[61.2,31.1,49.2,10.2,46.2,9.2,37.2]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n1,n1,n1,n1,n0,n1,n1,n0,n0,n1,n1,n0,n0,n0,n0) ->
% 61.84/12.95 === Backtracking. Learning clause 64:2:17:[12.1,53.2,53.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 65:2:14:[15.1,53.2,58.1,44.1,12.2,51.2,45.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,n1,n1,n0,n0,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n1,n1,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 61:2:16:[12.2,53.1,53.2,13.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 66:2:14:[61.1,64.2,15.1,14.2,61.2,53.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 61.84/12.95 === Backtracking. Learning clause 67:2:15:[10.1,49.2,46.1,14.2,61.2,64.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,n1,n0,n0,n0,n1,n0,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 66:2:14:[61.1,64.2,15.1,14.2,61.2,53.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 68:2:14:[66.2,67.1,12.2,53.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n1,n1,n0,n0,n0,n1,n0,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 50:2:20:[41.2,46.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n1,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n1, x17 -> n0, x18 -> n1, x19 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 69:2:14:[50.1,8.2,12.1,53.1,15.1,58.1,44.1,61.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,n1,n1,n0,n1,n1,n0,n0,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 64:2:17:[12.1,53.2,53.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1, x16 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 70:1:12:[64.2,31.1,13.2,44.2]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n1,n1,n1,n1,n0,n1,n1,n1,n1,n1,n0,n0,n0,n0,n0) ->
% 61.84/12.95 === Conflict found: 68:2:14:[66.2,67.1,12.2,53.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n1,n1,n0,n0,n0,n1,n0,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 71:1:0:[68.1,1.1]:: -> bin_count(n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n1,n1,n0,n0,n0,n1,n0,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 72:2:19:[10.1,46.2,49.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n0,n1,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 64:2:17:[12.1,53.2,53.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n0, x16 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 73:2:13:[64.1,15.2,61.1,14.1,64.1,61.2,64.2,14.2,61.2,64.2,16.2]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n1,n1,n1,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 61:2:16:[12.2,53.1,53.2,13.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 74:1:12:[61.2,31.1,64.2,14.2,61.2,64.2,15.2,61.2,64.2]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) ->
% 61.84/12.95 === Conflict found: 61:2:16:[12.2,53.1,53.2,13.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n1, x15 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 75:2:16:[61.1,64.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 49:2:20:[41.2,46.1,48.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n1, x17 -> n1, x18 -> n1, x19 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 76:2:17:[49.2,10.1,11.2,54.1,52.2,12.2,53.2,36.1,6.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0)
% 61.84/12.95 === Backtracking. Learning clause 77:2:18:[10.1,49.2,46.1,11.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n1,n0,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 78:2:17:[11.2,52.1,49.2,12.1,53.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 56:2:16:[10.1,46.2,49.1,12.1,53.1,13.1,53.1,12.1,53.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 79:2:15:[56.2,14.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,n0,n0,n0,n1,n0,n1,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 61.84/12.95 === Conflict found: 43:2:22:[7.2,36.1,37.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n0,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n0, x17 -> n0, x18 -> n0, x19 -> n0, x20 -> n0, x21 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 80:2:21:[43.1,48.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n1,n0,n1,n1,n1)
% 61.84/12.95 === Conflict found: 44:2:22:[32.1,38.2,37.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n0, x17 -> n0, x18 -> n0, x19 -> n0, x20 -> n1, x21 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 81:2:20:[44.1,41.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n0,n1,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,n1,n0,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 82:2:17:[12.1,53.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 61.84/12.95 === Backtracking. Learning clause 83:2:16:[13.1,64.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 458
% 61.84/12.95 === Backtracking. Learning clause 84:2:17:[12.2,53.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Conflict found: 45:2:18:[44.2,8.1,11.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n0,n0,n1,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1, x16 -> n1, x17 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 85:2:18:[45.2,51.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 86:2:22:[7.1,37.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n0,n0,n0,n0)
% 61.84/12.95 === Conflict found: 82:2:17:[12.1,53.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 87:2:16:[82.1,83.2,52.1,11.1,49.1,10.1,54.1,36.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n0,n0,n1,n1,n1)
% 61.84/12.95 === Conflict found: 44:2:22:[32.1,38.2,37.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n0, x17 -> n1, x18 -> n1, x19 -> n1, x20 -> n1, x21 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 88:2:16:[44.2,61.1,35.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n1,n1,n1,n1,n0,n1,n1,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 89:2:18:[9.1,77.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n1,n1,n0,n0,n0,n0,n0,n0)
% 61.84/12.95 === Conflict found: 89:2:18:[9.1,77.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n1,n1,n0,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n0, x17 -> n1}
% 61.84/12.95 === Backtracking. Learning clause 90:2:18:[89.1,52.2,48.1,38.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,n1,n1,n1,n1,n0,n1,n1,n0,n0)
% 61.84/12.95 === Conflict found: 82:2:17:[12.1,53.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n0, x15 -> n0, x16 -> n0}
% 61.84/12.95 === Backtracking. Learning clause 91:1:0:[82.2,52.1,1.1,89.1]:: -> bin_count(n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0)
% 61.84/12.95 === Backtracking. Learning clause 92:2:19:[10.2,49.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n0,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n1,n1,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 93:2:21:[8.2,44.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n0,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,n1,n1,n1,n1,n1,n1)
% 61.84/12.95 === Backtracking. Learning clause 94:2:19:[10.1,49.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,n1,n0,n0,n0,n0,n0,n0,n0)
% 61.84/12.95 === Clause set with instances from active satisfied. Growing active. New size: 475
% 61.84/12.95
% 61.84/12.95 SZS status Unsatisfiable
% 61.84/12.95
% 61.84/12.95 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.84/12.95
% 61.84/12.95 SPASS-SCL-FOL Statistics:
% 61.84/12.95 Number of learned clauses: 63
% 61.84/12.95 Number of propagations: 12300
% 61.84/12.95 Number of decisions: 2386
% 61.84/12.95 Number of resolutions: 203
% 61.84/12.95 Number of condensations: 0
% 61.84/12.95 Number of sub resolutions: 1
% 61.84/12.95 Number of input literals (deduplicated): 33
% 61.84/12.95 Number of grows: 27
% 61.84/12.95 Number of considered ground atoms: 475
% 61.84/12.95
% 61.84/12.95 Needed: 0:0:12.42
% 61.84/12.95
%------------------------------------------------------------------------------