%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO525+1.018 : 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 : n029.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 128.99s 32.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SYO525+1.018 : 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 : n029.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:45 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 128.99/32.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 128.99/32.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 128.99/32.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 128.99/32.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 128.99/32.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 128.99/32.83 Execution lmodel_grow ended with status: unsatisfiable
% 128.99/32.83 Used heuristic: lmodel_grow
% 128.99/32.83
% 128.99/32.83 Input Clauses:
% 128.99/32.83
% 128.99/32.83 Predicates: bin_count goal
% 128.99/32.83 Fol Constants: n0 n1
% 128.99/32.83 Fol Functions:
% 128.99/32.83 Problem Properties:
% 128.99/32.83 This is a Bernays Schoenfinkel problem.
% 128.99/32.83
% 128.99/32.83 After reduction: Problem Properties:
% 128.99/32.83 This is a Bernays Schoenfinkel problem.
% 128.99/32.83
% 128.99/32.83
% 128.99/32.83 Reduced Input Clauses:
% 128.99/32.83 31:1:9:[30.0,2.1]:TopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) ->
% 128.99/32.83
% 128.99/32.83 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
% 128.99/32.83
% 128.99/32.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 76 atoms initially, heuristics mode: lmodel_grow ===
% 128.99/32.83
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 100
% 128.99/32.83 === Backtracking. Learning clause 32: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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 122
% 128.99/32.83 === Backtracking. Learning clause 33:2:21:[5.2,32.1,32.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 145
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 173
% 128.99/32.83 === Backtracking. Learning clause 34:2:21:[5.2,32.1,32.2,6.1,33.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,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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 201
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 229
% 128.99/32.83 === Backtracking. Learning clause 35:2:23:[5.1,32.2,32.1,6.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,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,x21,x22,n1,n1,n1,n1)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 256
% 128.99/32.83 === Backtracking. Learning clause 36:2:22:[5.2,32.1,32.2,7.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,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,x21,n1,n0,n1,n1,n1)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 283
% 128.99/32.83 === Backtracking. Learning clause 37:2:21:[5.1,32.2,32.1,33.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,n0,n0,n1,n1,n1)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 313
% 128.99/32.83 === Backtracking. Learning clause 38:2:24:[5.1,32.2,32.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 339
% 128.99/32.83 === Conflict found: 36:2:22:[5.2,32.1,32.2,7.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,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,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 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n0, x17 -> n1, x18 -> n1, x19 -> n1, x20 -> n0, x21 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 39:2:22:[36.1,35.2,35.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,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,x21,n1,n1,n1,n1,n1)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 367
% 128.99/32.83 === Conflict found: 38:2:24:[5.1,32.2,32.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) {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, x16 -> n0, x17 -> n1, x18 -> n0, x19 -> n1, x20 -> n0, x21 -> n1, x22 -> n0, x23 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 40:2:22:[38.2,39.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 392
% 128.99/32.83 === Backtracking. Learning clause 41:2:22:[6.1,38.2,38.1,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,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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 413
% 128.99/32.83 === Conflict found: 34:2:21:[5.2,32.1,32.2,6.1,33.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,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1, x16 -> n0, x17 -> n1, x18 -> n0, x19 -> n0, x20 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 42:2:20:[34.2,40.1,41.2,9.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,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,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 434
% 128.99/32.83 === Backtracking. Learning clause 43:2:21:[8.1,40.2,40.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 450
% 128.99/32.83 === Conflict found: 42:2:20:[34.2,40.1,41.2,9.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,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,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n0, x16 -> n1, x17 -> n1, x18 -> n1, x19 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 44:2:20:[42.1,43.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 465
% 128.99/32.83 === Backtracking. Learning clause 45:2:23:[6.1,38.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,n0,n0,n0)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 479
% 128.99/32.83 === Conflict found: 45:2:23:[6.1,38.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,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, x18 -> n0, x19 -> n0, x20 -> n1, x21 -> n0, x22 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 46:2:22:[45.1,41.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 493
% 128.99/32.83 === Conflict found: 35:2:23:[5.1,32.2,32.1,6.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,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,x21,x22,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 -> n1, x18 -> n0, x19 -> n0, x20 -> n1, x21 -> n0, x22 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 47:2:23:[35.1,38.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,n1,n1)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 507
% 128.99/32.83 === Backtracking. Learning clause 48:2:19:[10.1,44.2,44.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 519
% 128.99/32.83 === Backtracking. Learning clause 49:2:18:[11.1,48.2,48.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 531
% 128.99/32.83 === Backtracking. Learning clause 50:2:15:[12.2,49.1,49.2,13.1,49.1,12.1,49.1,14.1]: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,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 541
% 128.99/32.83 === Backtracking. Learning clause 51:2:17:[12.2,49.1,49.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,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 547
% 128.99/32.83 === Backtracking. Learning clause 52:2:16:[13.1,51.2,51.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,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 43:2:21:[8.1,40.2,40.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) {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 -> n1, x16 -> n1, x17 -> n1, x18 -> n1, x19 -> n0, x20 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 53:2:18:[43.2,9.1,11.2,48.2,41.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,n0,n1,n0,n1,n0,n0,n0,n0)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 551
% 128.99/32.83 === Backtracking. Learning clause 54:2:15:[14.2,52.1,52.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,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 555
% 128.99/32.83 === Backtracking. Learning clause 55:2:12:[15.1,54.2,54.1,17.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,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,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 559
% 128.99/32.83 === Backtracking. Learning clause 56:2:13:[15.2,54.1,54.2,16.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,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,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 564
% 128.99/32.83 === Backtracking. Learning clause 57:2:11:[15.2,54.1,54.2,18.1,56.1,55.1]:TopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n0,n1,n1,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,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 48:2:19:[10.1,44.2,44.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) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n0, x16 -> n1, x17 -> n0, x18 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 58:2:17:[48.2,12.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n1,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)
% 128.99/32.83 === Conflict found: 48:2:19:[10.1,44.2,44.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) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n1, x16 -> n0, x17 -> n1, x18 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 59:2:10:[48.2,13.1,11.2,51.1,44.2,19.1,10.2,42.2]:TopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 59:2:10:[48.2,13.1,11.2,51.1,44.2,19.1,10.2,42.2]:TopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n1,n0,n0,n0,n0,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 -> n1, x8 -> n0, x9 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 60:2:10:[59.2,56.1]:TopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n1,n0,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 51:2:17:[12.2,49.1,49.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,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 -> n1, x11 -> n0, x12 -> n1, x13 -> n0, x14 -> n0, x15 -> n1, x16 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 61:2:14:[51.1,13.2,15.1,49.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,n1,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)
% 128.99/32.83 === Conflict found: 55:2:12:[15.1,54.2,54.1,17.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,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,n1,n0,n0,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n1, x11 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 62:2:10:[55.1,60.2,56.1,57.1]:TopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 55:2:12:[15.1,54.2,54.1,17.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,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,n1,n0,n0,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 63:2:12:[55.1,16.2,56.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,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,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 64:2:16:[13.1,51.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)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 573
% 128.99/32.83 === Backtracking. Learning clause 65:2:14:[15.2,54.1,54.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,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 65:2:14:[15.2,54.1,54.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,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n1, x11 -> n1, x12 -> n1, x13 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 66:1:9:[65.1,56.2,31.1,62.2]:TopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,n1,n0,n1,n1,n1,n1,n1,n0,n1,n0,n0,n0,n1,n1,n1,n1,n1,n1) ->
% 128.99/32.83 === Conflict found: 54:2:15:[14.2,52.1,52.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,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n0, x14 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 67:2:13:[54.2,16.1,61.2]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,n0,n1,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,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 51:2:17:[12.2,49.1,49.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,n1,n1,n1,n1,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n0, x16 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 68:2:15:[51.1,13.2,14.1,52.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,n0,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,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 65:2:14:[15.2,54.1,54.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,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 -> n1, x9 -> n1, x10 -> n1, x11 -> n0, x12 -> n0, x13 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 69:2:10:[65.1,19.2,63.1,54.2,57.1]:TopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n0,n1,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 70:2:18:[11.1,48.2,43.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,n0,n0,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 48:2:19:[10.1,44.2,44.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) {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, x16 -> n0, x17 -> n1, x18 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 71:2:14:[48.2,11.1,12.2,49.2,50.2,15.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,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,x13,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 72:2:20:[9.1,43.2,46.1,33.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,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)
% 128.99/32.83 === Backtracking. Learning clause 73:1:0:[11.2,58.1,48.2,1.1,43.1,9.1,46.1]:: -> bin_count(n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n0,n1,n0,n1,n1,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 74:2:15:[12.1,49.2,48.1,64.2,50.2,11.1]: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,n1,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 58:2:17:[48.2,12.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n1,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n1, x15 -> n0, x16 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 75:2:17:[58.2,49.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,n0,n1,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)
% 128.99/32.83 === Backtracking. Learning clause 76:2:13:[15.1,51.2,54.1,16.1,65.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,n0,n1,n1,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,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Backtracking. Learning clause 77:2:10:[19.1,65.2,56.1,55.1,56.1,16.2]:TopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n0,n1,n1,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,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 78:2:14:[10.1,44.2,41.1,38.1,12.2,49.2,50.2,15.2,54.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,n1,n0,n1,n0,n0,n1,n0,n1,n1,n1)
% 128.99/32.83 === Conflict found: 65:2:14:[15.2,54.1,54.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,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n1, x11 -> n1, x12 -> n1, x13 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 79:1:9:[65.1,56.2,31.1,57.2,77.2]:TopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,n1,n0,n1,n1,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) ->
% 128.99/32.83 === Conflict found: 56:2:13:[15.2,54.1,54.2,16.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,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,n1,n0,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 -> n1, x11 -> n0, x12 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 80:2:10:[56.2,65.1,19.2,65.2,56.2,57.2,63.2,65.2]:TopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n0,n0,n0,n0,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,n1,n0,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 49:2:18:[11.1,48.2,48.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) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n0, x9 -> n0, x10 -> n1, x11 -> n0, x12 -> n1, x13 -> n0, x14 -> n0, x15 -> n1, x16 -> n0, x17 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 81:2:15:[49.1,50.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,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 56:2:13:[15.2,54.1,54.2,16.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,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,n1,n0,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 -> n1, x9 -> n1, x10 -> n1, x11 -> n1, x12 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 82:1:9:[56.1,57.2,65.1,31.1]:TopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) ->
% 128.99/32.83 === Conflict found: 44:2:20:[42.1,43.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 -> n1, x13 -> n1, x14 -> n0, x15 -> n1, x16 -> n0, x17 -> n1, x18 -> n1, x19 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 83:2:15:[44.2,10.1,11.2,48.2,12.2,81.2,72.1]: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)
% 128.99/32.83 === Backtracking. Learning clause 84:2:15:[14.2,52.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,n0,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,x13,x14,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 56:2:13:[15.2,54.1,54.2,16.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,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,n1,n0,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 -> n1, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 85:2:12:[56.1,17.2,65.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,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,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 47:2:23:[35.1,38.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,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 -> n1, x16 -> n1, x17 -> n1, x18 -> n1, x19 -> n0, x20 -> n1, x21 -> n1, x22 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 86:2:20:[47.1,72.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,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 81:2:15:[49.1,50.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,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 -> n1, x11 -> n0, x12 -> n1, x13 -> n0, x14 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 87:2:12:[81.1,17.2,12.1,49.1,13.1,51.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,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,n1,n0,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 80:2:10:[56.2,65.1,19.2,65.2,56.2,57.2,63.2,65.2]:TopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,n0,n0,n0,n0,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,n1,n0,n0,n1,n1,n1,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}
% 128.99/32.83 === Backtracking. Learning clause 88:1:0:[80.1,1.1,17.1,81.1]:: -> bin_count(n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n1,n0,n1,n0,n0,n1,n0,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 57:2:11:[15.2,54.1,54.2,18.1,56.1,55.1]:TopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n0,n1,n1,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,n1,n1,n0,n0,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 89:2:11:[57.1,63.2,65.1,51.2,13.2]:TopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n0,n0,n0,n1,n1,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1) -> bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n1,n1,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 52:2:16:[13.1,51.2,51.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,n1,n1,n1,n1,n1) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n0, x8 -> n1, x9 -> n1, x10 -> n1, x11 -> n1, x12 -> n0, x13 -> n1, x14 -> n1, x15 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 90:2:12:[52.2,85.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,n1,n1,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,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Backtracking. Learning clause 91:1:9:[17.2,56.1,80.2,82.1]:TopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) ->
% 128.99/32.83 === Conflict found: 54:2:15:[14.2,52.1,52.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,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 -> n1, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n0, x14 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 92:1:9:[54.2,79.1]:TopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,n1,n0,n1,n1,n0,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0) ->
% 128.99/32.83 === Backtracking. Learning clause 93:2:18:[11.1,48.2]: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,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 94:2:14:[15.2,50.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,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,x13,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 95:2:19:[10.1,44.2,32.1,5.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,n0,n0,n0,n0,n1,n0,n0)
% 128.99/32.83 === Conflict found: 32: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 -> n0, x18 -> n0, x19 -> n1, x20 -> n0, x21 -> n0, x22 -> n1, x23 -> n0, x24 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 96:2:22:[32.2,5.1,41.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,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 97:2:16:[13.2,51.1]: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)
% 128.99/32.83 === Backtracking. Learning clause 98:2:19:[10.2,44.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)
% 128.99/32.83 === Conflict found: 54:2:15:[14.2,52.1,52.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,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n1, x11 -> n0, x12 -> n0, x13 -> n0, x14 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 99:2:12:[54.2,63.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n0,n1,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,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 98:2:19:[10.2,44.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) {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, x16 -> n0, x17 -> n1, x18 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 100:2:12:[98.2,13.1,44.2,93.2,12.2,81.2,63.2,65.2]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n0,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,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 54:2:15:[14.2,52.1,52.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,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n0, x12 -> n0, x13 -> n1, x14 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 101:2:12:[54.1,61.2,17.1,12.2,49.2,14.2]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,n0,n0,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,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 102:2:12:[17.2,56.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,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,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 103:2:16:[11.2,48.1,42.2,97.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,n0,n1,n0,n1,n0,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)
% 128.99/32.83 === Conflict found: 46:2:22:[45.1,41.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) {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, x16 -> n0, x17 -> n1, x18 -> n1, x19 -> n0, x20 -> n1, x21 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 104:2:20:[46.1,9.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,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,n1,n0,n1,n1,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 105:2:24:[5.2,3.1,32.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,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,n0,n1)
% 128.99/32.83 === Conflict found: 44:2:20:[42.1,43.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}
% 128.99/32.83 === Backtracking. Learning clause 106:2:16:[44.2,10.1,93.2,46.1,33.1,12.2,49.2,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,n0,n1,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 56:2:13:[15.2,54.1,54.2,16.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,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,n1,n0,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 107:2:11:[56.2,55.1,18.2]:TopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n0,n1,n1,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,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Conflict found: 54:2:15:[14.2,52.1,52.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,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 -> n1, x9 -> n1, x10 -> n1, x11 -> n0, x12 -> n1, x13 -> n0, x14 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 108:2:13:[54.1,15.2,16.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,n0,n0,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,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Backtracking. Learning clause 109:2:12:[15.1,97.2,54.1,85.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,n1,n0,n1,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,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 49:2:18:[11.1,48.2,48.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) {x0 -> n0, x1 -> n0, x2 -> n0, x3 -> n0, x4 -> n0, x5 -> n0, x6 -> n0, x7 -> n1, x8 -> n0, x9 -> n1, x10 -> n0, x11 -> n1, x12 -> n1, x13 -> n1, x14 -> n0, x15 -> n0, x16 -> n0, x17 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 110:2:14:[49.2,68.1,12.2,71.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,n0,n0,n0,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,n1,n1,n0,n1,n1,n0,n0,n0,n0,n0,n0,n0,n0)
% 128.99/32.83 === Clause set with instances from active satisfied. Growing active. New size: 593
% 128.99/32.83 === Conflict found: 63:2:12:[55.1,16.2,56.1]:TopTopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,n0,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,n1,n1,n0,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 -> n1, x8 -> n0, x9 -> n0, x10 -> n1, x11 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 111:2:11:[63.2,65.1,65.2,18.2,65.2]:TopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n0,n1,n1,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,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 107:2:11:[56.2,55.1,18.2]:TopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n0,n1,n1,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,n1,n1,n0,n0,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 -> n1, x8 -> n0, x9 -> n1, x10 -> n0}
% 128.99/32.83 === Backtracking. Learning clause 112:2:11:[107.2,65.1,85.2]:TopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n0,n0,n1,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,n1,n1,n0,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1,n1)
% 128.99/32.83 === Conflict found: 105:2:24:[5.2,3.1,32.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,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,n0,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 -> n0, x22 -> n0, x23 -> n1}
% 128.99/32.83 === Backtracking. Learning clause 113:2:23:[105.1,45.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,n1)
% 128.99/32.83 === Conflict found: 111:2:11:[63.2,65.1,65.2,18.2,65.2]:TopTopTopTopTopTopTopTopTopTopTop: bin_count(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,n0,n1,n1,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,n1,n1,n1,n1,n1,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 -> n1}
% 128.99/32.83
% 128.99/32.83 SZS status Unsatisfiable
% 128.99/32.83
% 128.99/32.83 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 128.99/32.83
% 128.99/32.83 SPASS-SCL-FOL Statistics:
% 128.99/32.83 Number of learned clauses: 82
% 128.99/32.83 Number of propagations: 19929
% 128.99/32.83 Number of decisions: 3692
% 128.99/32.83 Number of resolutions: 238
% 128.99/32.83 Number of condensations: 0
% 128.99/32.83 Number of sub resolutions: 1
% 128.99/32.83 Number of input literals (deduplicated): 39
% 128.99/32.83 Number of grows: 29
% 128.99/32.83 Number of considered ground atoms: 593
% 128.99/32.83
% 128.99/32.83 Needed: 0:0:32.25
% 128.99/32.83
%------------------------------------------------------------------------------