%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GRA014+1 : TPTP v9.2.1. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n031.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:22:36 PM UTC 2026
% Result : Theorem 1.14s 1.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA014+1 : TPTP v9.2.1. Released v3.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n031.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 12:00:41 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]
% 3.62/1.30 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.62/1.30 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.62/1.30 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.62/1.30 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.62/1.30 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.62/1.30 Execution resolution_1 ended with status: unsatisfiable
% 3.62/1.30 Used heuristic: resolution_1
% 3.62/1.30
% 3.62/1.30 Input Clauses:
% 3.62/1.30
% 3.62/1.30 Predicates: red goal green less_than
% 3.62/1.30 Fol Constants: n1 n2 n3 n4 n5 n6
% 3.62/1.30 Fol Functions:
% 3.62/1.30 Problem Properties:
% 3.62/1.30 This is a Bernays Schoenfinkel problem.
% 3.62/1.30
% 3.62/1.30 After reduction: Problem Properties:
% 3.62/1.30 This is a Bernays Schoenfinkel problem.
% 3.62/1.30
% 3.62/1.30
% 3.62/1.30 Reduced Input Clauses:
% 3.62/1.30 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) ->
% 3.62/1.30 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) ->
% 3.62/1.30
% 3.62/1.30 Most General Atoms: red(x0,x2) green(x0,x2) less_than(x0,x2) goal
% 3.62/1.30
% 3.62/1.30 === Starting SPASS-SCL-FOL A Little Less Naive, considering 22 atoms initially, heuristics mode: resolution_1 ===
% 3.62/1.30
% 3.62/1.30 === Backtracking. Learning clause 13:2:0:[9.1,3.1]:: -> red(n1,n2),green(n1,n2)
% 3.62/1.30 === Backtracking. Learning clause 14:2:1:[8.2,4.1]:Top: less_than(x0,n2) -> less_than(x0,n3)
% 3.62/1.30 === Backtracking. Learning clause 15:2:0:[9.1,4.1]:: -> red(n2,n3),green(n2,n3)
% 3.62/1.30 === Backtracking. Learning clause 16:2:1:[8.2,5.1]:Top: less_than(x0,n3) -> less_than(x0,n4)
% 3.62/1.30 === Backtracking. Learning clause 17:2:0:[9.1,5.1]:: -> red(n3,n4),green(n3,n4)
% 3.62/1.30 === Backtracking. Learning clause 18:2:1:[8.2,6.1]:Top: less_than(x0,n4) -> less_than(x0,n5)
% 3.62/1.30 === Backtracking. Learning clause 19:2:0:[9.1,6.1]:: -> red(n4,n5),green(n4,n5)
% 3.62/1.30 === Backtracking. Learning clause 20:2:1:[8.2,7.1]:Top: less_than(x0,n5) -> less_than(x0,n6)
% 3.62/1.30 === Backtracking. Learning clause 21:2:0:[9.1,7.1]:: -> red(n5,n6),green(n5,n6)
% 3.62/1.30 === Clause set with instances from active satisfied. Growing active. New size: 34
% 3.62/1.30 === Restarting.
% 3.62/1.30 === Conflict found: 14:2:1:[8.2,4.1]:Top: less_than(x0,n2) -> less_than(x0,n3) {x0 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 22:2:0:[14.2,9.1,3.1]:: -> red(n1,n3),green(n1,n3)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n2, x2 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 23:3:0:[12.2,15.2,22.2,13.2]:: -> red(n2,n3),red(n1,n3),red(n1,n2)
% 3.62/1.30 === Conflict found: 20:2:1:[8.2,7.1]:Top: less_than(x0,n5) -> less_than(x0,n6) {x0 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 24:2:0:[20.2,9.1,18.2,16.2,14.2,3.1]:: -> red(n1,n6),green(n1,n6)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n5, x1 -> n1, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 25:3:1:[12.3,21.2]:Top: green(n5,x0),green(x0,n6) -> red(n5,n6)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n5, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 26:3:0:[12.2,21.2,24.2]:: green(n1,n5) -> red(n5,n6),red(n1,n6)
% 3.62/1.30 === Conflict found: 18:2:1:[8.2,6.1]:Top: less_than(x0,n4) -> less_than(x0,n5) {x0 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 27:3:0:[18.2,9.1,16.2,14.2,3.1,26.1]:: -> red(n1,n5),red(n5,n6),red(n1,n6)
% 3.62/1.30 === Clause set with instances from active satisfied. Growing active. New size: 37
% 3.62/1.30 === Restarting.
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n2, x1 -> n1, x2 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 28:3:1:[12.3,15.2]:Top: green(n2,x0),green(x0,n3) -> red(n2,n3)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n2, x2 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 29:3:1:[12.2,15.2]:Top: green(x0,n2),green(x0,n3) -> red(n2,n3)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n5, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 30:3:1:[12.2,21.2]:Top: green(x0,n5),green(x0,n6) -> red(n5,n6)
% 3.62/1.30 === Conflict found: 16:2:1:[8.2,5.1]:Top: less_than(x0,n3) -> less_than(x0,n4) {x0 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 31:2:0:[16.2,9.1,14.2,3.1]:: -> red(n1,n4),green(n1,n4)
% 3.62/1.30 === Clause set with instances from active satisfied. Growing active. New size: 38
% 3.62/1.30 === Restarting.
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n4, x2 -> n5}
% 3.62/1.30 === Backtracking. Learning clause 32:3:1:[12.2,19.2]:Top: green(x0,n4),green(x0,n5) -> red(n4,n5)
% 3.62/1.30 === Conflict found: 18:2:1:[8.2,6.1]:Top: less_than(x0,n4) -> less_than(x0,n5) {x0 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 33:3:0:[18.2,9.1,16.2,14.2,3.1,32.2]:: green(n1,n4) -> red(n1,n5),red(n4,n5)
% 3.62/1.30 === Clause set with instances from active satisfied. Growing active. New size: 39
% 3.62/1.30 === Restarting.
% 3.62/1.30 === Conflict found: 33:3:0:[18.2,9.1,16.2,14.2,3.1,32.2]:: green(n1,n4) -> red(n1,n5),red(n4,n5) {}
% 3.62/1.30 === Backtracking. Learning clause 34:3:0:[33.1,31.2]:: -> red(n1,n5),red(n4,n5),red(n1,n4)
% 3.62/1.30 === Clause set with instances from active satisfied. Growing active. New size: 40
% 3.62/1.30 === Restarting.
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n3, x1 -> n1, x2 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 35:3:1:[12.3,17.2]:Top: green(n3,x0),green(x0,n4) -> red(n3,n4)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n3, x2 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 36:3:1:[12.2,17.2]:Top: green(x0,n3),green(x0,n4) -> red(n3,n4)
% 3.62/1.30 === Clause set with instances from active satisfied. Growing active. New size: 41
% 3.62/1.30 === Restarting.
% 3.62/1.30 === Clause set with instances from active satisfied. Growing active. New size: 85
% 3.62/1.30 === Backtracking. Learning clause 37:4:1:[9.3,12.2,16.2,11.1,4.1,31.2,13.2]:Top: red(n4,x0),red(n2,x0) -> red(n1,n4),red(n1,n2)
% 3.62/1.30 === Backtracking. Learning clause 38:3:1:[9.2,11.2,7.1]:Top: red(x0,n5),red(x0,n6) -> green(n5,n6)
% 3.62/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n2, x1 -> n3, x2 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 39:4:1:[11.2,17.1,9.2]:Top: red(x0,n4),less_than(x0,n3) -> green(n3,n4),green(x0,n3)
% 3.62/1.30 === Clause set with instances from active satisfied. Growing active. New size: 109
% 3.62/1.30 === Backtracking. Learning clause 40:9:6:[9.1,8.3,11.2,9.2,8.3,12.2,12.2,18.2]:TopTopTopTopTopTop: less_than(x0,x1),less_than(x1,x2),red(x3,x0),less_than(n5,x2),green(x4,x0),green(x4,x2),green(x5,x3),green(x5,x2),less_than(x3,n4) ->
% 3.62/1.30 === Backtracking. Learning clause 41:6:3:[9.2,11.2,30.2,9.3,8.3,8.3,11.2,5.1,8.3,6.1,11.2,7.1]:TopTopTop: red(x0,n3),red(x0,n6),red(x1,n3),red(x1,n5),red(x2,n5),red(x2,n6) ->
% 3.62/1.30 === Conflict found: 37:4:1:[9.3,12.2,16.2,11.1,4.1,31.2,13.2]:Top: red(n4,x0),red(n2,x0) -> red(n1,n4),red(n1,n2) {x0 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 42:9:4:[37.2,9.2,9.2,12.2,12.2,8.3,4.1,8.3]:TopTopTopTop: less_than(n4,x0),green(x1,n4),green(x1,x0),green(x2,n2),green(x2,x0),less_than(n3,x3),less_than(x3,x0) -> red(n1,n4),red(n1,n2)
% 3.62/1.30 === Conflict found: 24:2:0:[20.2,9.1,18.2,16.2,14.2,3.1]:: -> red(n1,n6),green(n1,n6) {}
% 3.62/1.30 === Backtracking. Learning clause 43:4:0:[24.1,41.2,42.3,13.2,5.1,8.3,6.1,7.1,31.2]:: red(n1,n3),red(n1,n5) -> red(n1,n2),red(n1,n4)
% 3.62/1.30 === Conflict found: 42:9:4:[37.2,9.2,9.2,12.2,12.2,8.3,4.1,8.3]:TopTopTopTop: less_than(n4,x0),green(x1,n4),green(x1,x0),green(x2,n2),green(x2,x0),less_than(n3,x3),less_than(x3,x0) -> red(n1,n4),red(n1,n2) {x0 -> n6, x1 -> n1, x2 -> n1, x3 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 44:6:2:[42.4,13.2,5.1,8.3,6.1]:TopTop: green(x0,n4),green(x0,x1),green(n1,x1),less_than(n5,x1) -> red(n1,n4),red(n1,n2)
% 3.62/1.30 === Conflict found: 42:9:4:[37.2,9.2,9.2,12.2,12.2,8.3,4.1,8.3]:TopTopTopTop: less_than(n4,x0),green(x1,n4),green(x1,x0),green(x2,n2),green(x2,x0),less_than(n3,x3),less_than(x3,x0) -> red(n1,n4),red(n1,n2) {x0 -> n6, x1 -> n1, x2 -> n1, x3 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 45:5:1:[42.4,13.2,5.1,20.2,6.1]:Top: green(x0,n4),green(x0,n6),green(n1,n6) -> red(n1,n4),red(n1,n2)
% 3.62/1.30 === Backtracking. Learning clause 46:3:0:[9.2,43.2,8.3,42.3,8.3,14.2,3.1,13.2,5.1,6.1,31.2]:: red(n1,n3) -> red(n1,n2),red(n1,n4)
% 3.62/1.30 === Conflict found: 32:3:1:[12.2,19.2]:Top: green(x0,n4),green(x0,n5) -> red(n4,n5) {x0 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 47:8:2:[32.3,11.2,9.3,11.2,9.3,8.3,11.2,46.3,9.2]:TopTop: less_than(x0,n4),less_than(x0,x1),less_than(x1,n5),red(n1,x0),red(n1,n3),less_than(n1,n5) -> red(n1,n2),green(n1,n5)
% 3.62/1.30 === Conflict found: 32:3:1:[12.2,19.2]:Top: green(x0,n4),green(x0,n5) -> red(n4,n5) {x0 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 49:7:4:[18.1,48.5,32.3,11.2,9.3,11.2,9.3,11.2]:TopTopTopTop: red(x0,n4),red(x0,n5),less_than(x1,n4),red(x2,x1),red(x2,n4),red(x3,x1),red(x3,n5) ->
% 3.62/1.30 === Backtracking. Learning clause 51:11:4:[13.1,50.0,9.3,12.2,11.1,8.3,9.2,12.2,8.3,4.1,8.3,30.3,8.3,47.8,8.3,8.3,14.2,3.1]:TopTopTopTop: less_than(n3,x0),less_than(x0,n6),green(n1,n6),less_than(x1,n4),less_than(x1,x2),less_than(x2,n5),red(n1,x1),red(n1,n3),less_than(x3,n5),less_than(n3,x3) -> red(n1,n2)
% 3.62/1.30 === Conflict found: 47:8:2:[32.3,11.2,9.3,11.2,9.3,8.3,11.2,46.3,9.2]:TopTop: less_than(x0,n4),less_than(x0,x1),less_than(x1,n5),red(n1,x0),red(n1,n3),less_than(n1,n5) -> red(n1,n2),green(n1,n5) {x0 -> n3, x1 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 52:9:3:[47.6,8.3]:TopTopTop: less_than(x0,n4),less_than(x0,x1),less_than(x1,n5),red(n1,x0),red(n1,n3),less_than(n1,x2),less_than(x2,n5) -> red(n1,n2),green(n1,n5)
% 3.62/1.30 === Conflict found: 49:7:4:[18.1,48.5,32.3,11.2,9.3,11.2,9.3,11.2]:TopTopTopTop: red(x0,n4),red(x0,n5),less_than(x1,n4),red(x2,x1),red(x2,n4),red(x3,x1),red(x3,n5) -> {x0 -> n1, x1 -> n3, x2 -> n1, x3 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 53:5:1:[49.1,46.3]:Top: red(n1,n5),less_than(x0,n4),red(n1,x0),red(n1,n3) -> red(n1,n2)
% 3.62/1.30 === Conflict found: 51:11:4:[13.1,50.0,9.3,12.2,11.1,8.3,9.2,12.2,8.3,4.1,8.3,30.3,8.3,47.8,8.3,8.3,14.2,3.1]:TopTopTopTop: less_than(n3,x0),less_than(x0,n6),green(n1,n6),less_than(x1,n4),less_than(x1,x2),less_than(x2,n5),red(n1,x1),red(n1,n3),less_than(x3,n5),less_than(n3,x3) -> red(n1,n2) {x0 -> n4, x1 -> n3, x2 -> n4, x3 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 54:9:3:[51.2,20.2]:TopTopTop: green(n1,n6),less_than(x0,n4),less_than(x0,x1),less_than(x1,n5),red(n1,x0),red(n1,n3),less_than(x2,n5),less_than(n3,x2) -> red(n1,n2)
% 3.62/1.30 === Conflict found: 16:2:1:[8.2,5.1]:Top: less_than(x0,n3) -> less_than(x0,n4) {x0 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 56:5:1:[6.0,55.3,16.2,52.6,14.2,3.1]:Top: less_than(x0,n4),red(n1,x0),red(n1,n3) -> red(n1,n2),green(n1,n5)
% 3.62/1.30 === Backtracking. Learning clause 57:2:0:[9.2,11.2,12.3,9.3,11.2,24.1,8.3,9.3,11.2,46.3,20.2,54.1,5.1,6.1]:: red(n1,n3) -> red(n1,n2)
% 3.62/1.30 === Conflict found: 42:9:4:[37.2,9.2,9.2,12.2,12.2,8.3,4.1,8.3]:TopTopTopTop: less_than(n4,x0),green(x1,n4),green(x1,x0),green(x2,n2),green(x2,x0),less_than(n3,x3),less_than(x3,x0) -> red(n1,n4),red(n1,n2) {x0 -> n6, x1 -> n1, x2 -> n1, x3 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 58:10:4:[42.2,9.3]:TopTopTopTop: less_than(n4,x0),green(x1,x0),green(x2,n2),green(x2,x0),less_than(n3,x3),less_than(x3,x0),less_than(x1,n4) -> red(n1,n4),red(n1,n2),red(x1,n4)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n3, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 59:8:3:[12.1,39.4,9.3,11.2,23.1,57.1,9.2,8.3,12.2,4.1]:TopTopTop: green(x0,x1),red(x0,n4),less_than(x0,n3),less_than(n3,x1),green(x2,n2),green(x2,x1) -> green(n3,n4),red(n1,n2)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n3, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 60:2:0:[12.1,9.3,9.3,11.2,23.1,57.1,9.2,8.3,12.2,4.1,8.3,13.2,14.2,3.1,5.1,20.2,6.1]:: green(n1,n6) -> red(n1,n2)
% 3.62/1.30 === Backtracking. Learning clause 61:8:3:[9.2,41.4,30.1,8.3,11.2,8.3,24.1]:TopTopTop: red(x0,n3),red(x0,n6),green(x0,n6),less_than(x0,x1),red(n1,n5),less_than(x1,x2),less_than(x2,n5) -> green(n1,n6)
% 3.62/1.30 === Backtracking. Learning clause 63:8:3:[57.0,62.6,9.2,11.3,8.3,12.2,9.2,23.1,9.3]:TopTopTop: less_than(n2,x0),less_than(x0,x1),green(x2,n2),less_than(n3,x1),less_than(x2,x1) -> green(n3,x1),red(n1,n2),red(x2,x1)
% 3.62/1.30 === Backtracking. Learning clause 65:6:2:[20.1,64.4,9.2,11.2,30.1,9.2,30.1,9.3]:TopTop: less_than(x0,n5),red(x1,x0),less_than(x1,n5),green(x1,n6) -> red(n5,n6),red(x0,n6)
% 3.62/1.30 === Backtracking. Learning clause 66:8:4:[9.3,12.1,11.3,8.3,9.3,11.2,24.1]:TopTopTopTop: green(x0,n6),red(x0,x1),red(x1,x2),less_than(x0,x3),less_than(x3,x2),less_than(x2,n6),red(n1,x2) -> green(n1,n6)
% 3.62/1.30 === Backtracking. Learning clause 72:9:2:[8.2,67.1,20.1,68.3,13.1,69.6,60.0,70.10,57.0,71.11,9.1,8.3,11.1,65.5,8.3,11.2,9.3,11.2,9.2,24.1,66.1,9.2,23.1,63.8]:TopTop: less_than(x0,n5),less_than(n2,n6),less_than(n2,x1),less_than(x1,x0),less_than(n3,x0),less_than(n1,x0) -> green(n1,n5),green(n3,x0),red(n1,n2)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n3, x2 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1)
% 3.62/1.30 === Backtracking. Learning clause 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2)
% 3.62/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n1, x1 -> n2, x2 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 76:4:1:[13.1,75.2,74.3,57.1,29.2]:Top: less_than(n1,x0),less_than(x0,n3) -> red(n1,n2),red(n2,n3)
% 3.62/1.30 === Conflict found: 63:8:3:[57.0,62.6,9.2,11.3,8.3,12.2,9.2,23.1,9.3]:TopTopTop: less_than(n2,x0),less_than(x0,x1),green(x2,n2),less_than(n3,x1),less_than(x2,x1) -> green(n3,x1),red(n1,n2),red(x2,x1) {x0 -> n3, x1 -> n4, x2 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 79:2:0:[5.0,77.0,3.0,78.1,63.5,8.3,12.2,74.4,57.1,4.1,13.2,14.2,31.2]:: -> red(n1,n2),red(n1,n4)
% 3.62/1.30 === Conflict found: 66:8:4:[9.3,12.1,11.3,8.3,9.3,11.2,24.1]:TopTopTopTop: green(x0,n6),red(x0,x1),red(x1,x2),less_than(x0,x3),less_than(x3,x2),less_than(x2,n6),red(n1,x2) -> green(n1,n6) {x0 -> n2, x1 -> n3, x2 -> n4, x3 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 80:6:1:[66.5,5.1,20.2,6.1,17.1]:Top: green(x0,n6),red(x0,n3),less_than(x0,n3),red(n1,n4) -> green(n1,n6),green(n3,n4)
% 3.62/1.30 === Backtracking. Learning clause 81:7:1:[9.3,12.2,11.2,74.4,5.1,20.2,6.1,80.6,4.1]:Top: red(x0,n4),red(x0,n6),green(n2,n6),red(n2,n3),red(n1,n4) -> red(n3,n6),green(n1,n6)
% 3.62/1.30 === Conflict found: 59:8:3:[12.1,39.4,9.3,11.2,23.1,57.1,9.2,8.3,12.2,4.1]:TopTopTop: green(x0,x1),red(x0,n4),less_than(x0,n3),less_than(n3,x1),green(x2,n2),green(x2,x1) -> green(n3,n4),red(n1,n2) {x0 -> n1, x1 -> n5, x2 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 83:4:0:[79.1,82.0,59.1,74.4,8.3,3.1,11.1,65.5,8.3,13.2,11.2,17.1,4.1,74.4,5.1,20.2,6.1]:: red(n1,n6) -> red(n1,n2),green(n3,n4),red(n3,n6)
% 3.62/1.30 === Backtracking. Learning clause 86:2:0:[79.1,84.0,60.0,85.3,9.3,12.2,11.2,74.4,5.1,20.2,6.1,83.3,24.1]:: -> red(n1,n2),red(n3,n6)
% 3.62/1.30 === Conflict found: 66:8:4:[9.3,12.1,11.3,8.3,9.3,11.2,24.1]:TopTopTopTop: green(x0,n6),red(x0,x1),red(x1,x2),less_than(x0,x3),less_than(x3,x2),less_than(x2,n6),red(n1,x2) -> green(n1,n6) {x0 -> n2, x1 -> n3, x2 -> n4, x3 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 87:7:2:[66.8,60.1,23.1,57.1]:TopTop: green(n2,n6),red(n3,x0),less_than(n2,x1),less_than(x1,x0),less_than(x0,n6),red(n1,x0) -> red(n1,n2)
% 3.62/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n2, x1 -> n3, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 88:2:0:[74.3,11.3,8.3,23.1,57.1,87.1,17.1,4.1,79.2,86.2,5.1,20.2,6.1]:: -> green(n3,n4),red(n1,n2)
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n4, x1 -> n6, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 89:16:9:[73.4,49.5,8.3,74.3,30.1,8.3,11.2]:TopTopTopTopTopTopTopTopTop: green(n4,x0),red(x1,n4),red(x1,n5),less_than(x2,n4),red(x3,x2),red(x4,x2),less_than(x3,x5),less_than(x5,n4),less_than(x4,x6),less_than(x6,n5),green(x4,n6),less_than(x3,x7),less_than(x7,x0),red(x8,n5),red(x8,n6) -> red(x3,x0)
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n4, x1 -> n6, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 92:15:7:[79.1,90.1,60.0,91.16,73.4,49.1,8.3,74.3,12.2,74.4,8.3,3.1,8.3,89.3,8.3,9.3,11.3,13.2,8.3,24.1]:TopTopTopTopTopTopTop: less_than(n2,x0),less_than(x1,n4),red(n2,x1),red(x2,x1),less_than(n2,x3),less_than(x3,n4),less_than(x2,x0),green(x2,n6),less_than(x0,x4),less_than(x4,n5),less_than(n4,x5),red(n2,x6),red(x6,x5) -> red(n4,x5),red(n1,n2)
% 3.62/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n1, x1 -> n3, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 96:8:3:[79.1,93.0,5.0,94.1,86.1,95.9,74.4,60.1,8.3,3.1,8.3,11.3,92.14,23.1,57.1]:TopTopTop: less_than(n2,x0),less_than(x0,n4),less_than(n2,x1),green(n2,n6),less_than(x1,x2),less_than(x2,n5),less_than(n4,n6) -> red(n1,n2)
% 3.62/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n2, x1 -> n3, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 97:1:0:[74.3,11.3,8.3,23.1,57.1,96.4,4.1,86.2,5.1,20.2,6.1]:: -> red(n1,n2)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n4, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 98:5:4:[12.1,74.4]:TopTopTopTop: green(x0,x1),green(x2,x1),less_than(x2,x3),less_than(x3,x0) -> red(x2,x0)
% 3.62/1.30 === Conflict found: 12:3:3:[10.0,2.3]:TopTopTop: green(x0,x1),green(x1,x2),green(x0,x2) -> {x0 -> n1, x1 -> n4, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 99:6:4:[12.2,9.3,74.4]:TopTopTopTop: green(x0,x1),less_than(x2,x1),less_than(x0,x3),less_than(x3,x2) -> red(x2,x1),red(x0,x2)
% 3.62/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n1, x1 -> n3, x2 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 100:6:2:[11.2,9.2,31.1,12.1,9.3]:TopTop: red(n1,x0),less_than(x0,n4),green(n1,x1),less_than(n4,x1) -> green(x0,n4),red(n4,x1)
% 3.62/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n1, x1 -> n2, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 101:2:1:[11.1,97.1]:Top: red(n2,x0),red(n1,x0) ->
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n5, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 102:9:5:[73.3,8.3,74.4,11.2,101.1]:TopTopTopTopTop: less_than(n2,x0),less_than(n2,x1),less_than(x1,x2),less_than(x0,x3),less_than(x3,x2),red(x4,x0),red(x4,x2),red(n1,x2) -> red(n2,x0)
% 3.62/1.30 === Conflict found: 102:9:5:[73.3,8.3,74.4,11.2,101.1]:TopTopTopTopTop: less_than(n2,x0),less_than(n2,x1),less_than(x1,x2),less_than(x0,x3),less_than(x3,x2),red(x4,x0),red(x4,x2),red(n1,x2) -> red(n2,x0) {x0 -> n3, x1 -> n3, x2 -> n5, x3 -> n4, x4 -> n1}
% 3.62/1.30 === Backtracking. Learning clause 103:7:4:[102.3,8.3]:TopTopTopTop: less_than(n2,x0),less_than(x0,x1),less_than(x1,x2),red(x3,x0),red(x3,x2),red(n1,x2) -> red(n2,x0)
% 3.62/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n4, x1 -> n5, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 105:12:4:[101.0,104.11,11.1,34.2,27.2,102.7,11.3,9.2,100.6]:TopTopTopTop: less_than(n2,x0),less_than(n2,x1),less_than(x1,n6),less_than(x0,x2),less_than(x2,n6),red(n1,x0),red(n1,x3),less_than(x3,n4),green(n1,n6),less_than(n4,n6) -> red(n1,n5),green(x3,n4)
% 3.62/1.30 === Conflict found: 24:2:0:[20.2,9.1,18.2,16.2,14.2,3.1]:: -> red(n1,n6),green(n1,n6) {}
% 3.62/1.30 === Backtracking. Learning clause 108:14:6:[101.0,106.13,101.0,107.15,24.1,102.7,105.9,103.5]:TopTopTopTopTopTop: less_than(n2,x0),less_than(x0,x1),less_than(x1,n6),red(n1,x0),less_than(n2,x2),less_than(x2,n6),red(n1,x3),less_than(x3,n4),less_than(n4,n6),less_than(n2,x4),less_than(x4,x5),less_than(x5,n5),red(n1,x4) -> green(x3,n4)
% 3.62/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n2, x1 -> n3, x2 -> n5}
% 3.62/1.30 === Backtracking. Learning clause 109:7:3:[74.4,30.1,101.1,11.2,8.3]:TopTopTop: less_than(n2,x0),green(n2,n6),red(n1,n5),red(x1,n5),red(x1,n6),less_than(x0,x2),less_than(x2,n5) ->
% 3.62/1.30 === Conflict found: 101:2:1:[11.1,97.1]:Top: red(n2,x0),red(n1,x0) -> {x0 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 110:8:3:[101.1,99.6,31.1,12.1,9.3]:TopTopTop: green(n2,x0),less_than(n4,x0),less_than(n2,x1),less_than(x1,n4),green(n1,x2),less_than(n4,x2) -> red(n4,x0),red(n4,x2)
% 3.62/1.30 === Conflict found: 98:5:4:[12.1,74.4]:TopTopTopTop: green(x0,x1),green(x2,x1),less_than(x2,x3),less_than(x3,x0) -> red(x2,x0) {x0 -> n3, x1 -> n6, x2 -> n1, x3 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 112:11:4:[8.2,111.0,98.3,3.1,9.3,11.3,9.2,108.4,110.7]:TopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),green(n2,x3),green(n1,x3),less_than(n4,x3) -> green(x1,n4)
% 3.62/1.30 === Conflict found: 112:11:4:[8.2,111.0,98.3,3.1,9.3,11.3,9.2,108.4,110.7]:TopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),green(n2,x3),green(n1,x3),less_than(n4,x3) -> green(x1,n4) {x0 -> n3, x1 -> n3, x2 -> n4, x3 -> n5}
% 3.62/1.30 === Backtracking. Learning clause 113:15:6:[112.9,74.4,74.4]:TopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3),less_than(n1,x4),less_than(x4,x3),less_than(n2,x5),less_than(x5,x3) -> green(x1,n4),red(n1,x3),red(n2,x3)
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n6, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 115:20:8:[6.0,114.9,73.3,8.3,49.4,99.6,113.15,8.3,9.3]:TopTopTopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n4),green(n2,x1),less_than(n4,x1),less_than(n2,x2),less_than(x2,n6),less_than(x3,n4),less_than(n4,n6),less_than(n2,x3),less_than(x4,n5),less_than(n2,x5),less_than(x5,n5),less_than(n1,x6),less_than(x6,x4),less_than(x0,x7) -> red(n2,x7),red(n4,x1),green(x3,n4),red(n1,n5),red(x0,x7)
% 3.62/1.30 === Conflict found: 113:15:6:[112.9,74.4,74.4]:TopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3),less_than(n1,x4),less_than(x4,x3),less_than(n2,x5),less_than(x5,x3) -> green(x1,n4),red(n1,x3),red(n2,x3) {x0 -> n3, x1 -> n3, x2 -> n4, x3 -> n5, x4 -> n3, x5 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 116:16:7:[113.9,8.3]:TopTopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3),less_than(x4,x3),less_than(n2,x5),less_than(x5,x3),less_than(n1,x6),less_than(x6,x4) -> green(x1,n4),red(n1,x3),red(n2,x3)
% 3.62/1.30 === Conflict found: 115:20:8:[6.0,114.9,73.3,8.3,49.4,99.6,113.15,8.3,9.3]:TopTopTopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n4),green(n2,x1),less_than(n4,x1),less_than(n2,x2),less_than(x2,n6),less_than(x3,n4),less_than(n4,n6),less_than(n2,x3),less_than(x4,n5),less_than(n2,x5),less_than(x5,n5),less_than(n1,x6),less_than(x6,x4),less_than(x0,x7) -> red(n2,x7),red(n4,x1),green(x3,n4),red(n1,n5),red(x0,x7) {x0 -> n3, x1 -> n6, x2 -> n3, x3 -> n3, x4 -> n4, x5 -> n3, x6 -> n3, x7 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 117:20:8:[115.16,101.1]:TopTopTopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n4),green(n2,x1),less_than(n4,x1),less_than(n2,x2),less_than(x2,n6),less_than(x3,n4),less_than(n4,n6),less_than(n2,x3),less_than(x4,n5),less_than(n2,x5),less_than(x5,n5),less_than(n1,x6),less_than(x6,x4),less_than(x0,x7),red(n1,x7) -> red(n4,x1),green(x3,n4),red(n1,n5),red(x0,x7)
% 3.62/1.30 === Conflict found: 65:6:2:[20.1,64.4,9.2,11.2,30.1,9.2,30.1,9.3]:TopTop: less_than(x0,n5),red(x1,x0),less_than(x1,n5),green(x1,n6) -> red(n5,n6),red(x0,n6) {x0 -> n4, x1 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 118:7:3:[65.3,8.3]:TopTopTop: less_than(x0,n5),red(x1,x0),green(x1,n6),less_than(x1,x2),less_than(x2,n5) -> red(n5,n6),red(x0,n6)
% 3.62/1.30 === Conflict found: 99:6:4:[12.2,9.3,74.4]:TopTopTopTop: green(x0,x1),less_than(x2,x1),less_than(x0,x3),less_than(x3,x2) -> red(x2,x1),red(x0,x2) {x0 -> n1, x1 -> n5, x2 -> n3, x3 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 120:23:8:[8.2,119.14,99.5,11.1,74.4,118.6,99.6,8.3,117.20,3.1,8.3,109.3]:TopTopTopTopTopTopTopTop: less_than(x0,n5),green(x1,n6),less_than(x1,x2),green(x1,x3),less_than(x0,x3),less_than(x1,x4),less_than(x4,x0),less_than(x2,n4),green(n2,x5),less_than(n4,x5),less_than(x6,n4),less_than(n4,n6),less_than(n2,x6),less_than(n2,x2),less_than(x2,x7),less_than(x7,n5),green(n2,n6),red(n1,n6) -> red(n1,x2),red(x0,n6),red(x0,x3),red(n4,x5),green(x6,n4)
% 3.62/1.30 === Conflict found: 113:15:6:[112.9,74.4,74.4]:TopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3),less_than(n1,x4),less_than(x4,x3),less_than(n2,x5),less_than(x5,x3) -> green(x1,n4),red(n1,x3),red(n2,x3) {x0 -> n3, x1 -> n3, x2 -> n4, x3 -> n5, x4 -> n3, x5 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 121:15:6:[113.10,8.3]:TopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3),less_than(n1,x4),less_than(n2,x4),less_than(x4,x5),less_than(x5,x3) -> green(x1,n4),red(n1,x3),red(n2,x3)
% 3.62/1.30 === Conflict found: 116:16:7:[113.9,8.3]:TopTopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3),less_than(x4,x3),less_than(n2,x5),less_than(x5,x3),less_than(n1,x6),less_than(x6,x4) -> green(x1,n4),red(n1,x3),red(n2,x3) {x0 -> n3, x1 -> n3, x2 -> n4, x3 -> n5, x4 -> n3, x5 -> n3, x6 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 122:11:4:[116.12,3.1,8.3]:TopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3) -> green(x1,n4),red(n1,x3),red(n2,x3)
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n6, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 123:8:2:[73.3,8.3,118.2,101.1,9.3]:TopTop: less_than(n2,x0),less_than(x0,n5),green(n2,n6),red(n1,x1),less_than(x0,x1) -> red(n5,n6),red(x0,n6),red(x0,x1)
% 3.62/1.30 === Conflict found: 99:6:4:[12.2,9.3,74.4]:TopTopTopTop: green(x0,x1),less_than(x2,x1),less_than(x0,x3),less_than(x3,x2) -> red(x2,x1),red(x0,x2) {x0 -> n1, x1 -> n5, x2 -> n3, x3 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 125:15:5:[6.0,124.10,99.5,11.2,74.4,73.4,8.3,101.1,9.3,8.3,3.1,8.3,122.11,109.3]:TopTopTopTopTop: red(n1,x0),less_than(x1,x0),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n2,x3),less_than(x3,n6),less_than(x4,n4),less_than(n4,n6),less_than(n2,x4),green(n2,n6),red(n1,n6) -> red(n1,x1),red(x1,x0),green(x4,n4)
% 3.62/1.30 === Conflict found: 121:15:6:[113.10,8.3]:TopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3),less_than(n1,x4),less_than(n2,x4),less_than(x4,x5),less_than(x5,x3) -> green(x1,n4),red(n1,x3),red(n2,x3) {x0 -> n3, x1 -> n3, x2 -> n4, x3 -> n5, x4 -> n3, x5 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 127:9:2:[6.0,126.5,121.14,109.3,8.3,3.1]:TopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),green(n2,n6),red(n1,n6) -> green(x1,n4),red(n2,n5)
% 3.62/1.30 === Conflict found: 125:15:5:[6.0,124.10,99.5,11.2,74.4,73.4,8.3,101.1,9.3,8.3,3.1,8.3,122.11,109.3]:TopTopTopTopTop: red(n1,x0),less_than(x1,x0),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n2,x3),less_than(x3,n6),less_than(x4,n4),less_than(n4,n6),less_than(n2,x4),green(n2,n6),red(n1,n6) -> red(n1,x1),red(x1,x0),green(x4,n4) {x0 -> n6, x1 -> n3, x2 -> n4, x3 -> n3, x4 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 128:13:4:[125.13,108.4]:TopTopTopTop: red(n1,x0),less_than(x1,x0),green(n2,n6),red(n1,n6),less_than(n2,x2),less_than(x2,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x3),less_than(x3,n5) -> red(x1,x0),green(x1,n4)
% 3.62/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n3, x1 -> n4, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 131:5:1:[6.0,129.0,8.2,130.1,11.1,9.2,120.20,108.4,128.12,24.1,112.9]:Top: less_than(x0,n4),less_than(n2,x0),green(n2,n6),less_than(n4,n6) -> green(x0,n4)
% 3.62/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n1, x1 -> n3, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 132:11:4:[74.3,109.5,110.5]:TopTopTopTop: less_than(n1,x0),less_than(x0,n6),less_than(n2,x1),green(n2,n6),red(n1,n5),less_than(x1,x2),less_than(x2,n5),less_than(n2,x3),less_than(x3,n4),less_than(n4,n6) -> red(n4,n6)
% 3.62/1.30 === Conflict found: 101:2:1:[11.1,97.1]:Top: red(n2,x0),red(n1,x0) -> {x0 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 133:17:8:[101.1,102.9,99.6,74.4,109.5]:TopTopTopTopTopTopTopTop: less_than(n2,x0),less_than(n2,x1),less_than(x1,x2),less_than(x0,x3),less_than(x3,x2),red(n1,x2),less_than(x0,n6),less_than(n1,x4),less_than(x4,x0),less_than(n1,x5),less_than(x5,n6),less_than(n2,x6),green(n2,n6),red(n1,n5),less_than(x6,x7),less_than(x7,n5) -> red(x0,n6)
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n4, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 135:10:3:[8.2,134.4,73.3,8.3,11.1,131.5,73.5,8.3,9.3,101.1,99.6,110.7]:TopTopTop: less_than(x0,n4),green(n2,n6),less_than(n4,n6),less_than(n2,x0),less_than(n1,x1),less_than(x1,x0),green(n2,x2),green(n1,x2),less_than(n4,x2) -> red(x0,x2)
% 3.62/1.30 === Conflict found: 101:2:1:[11.1,97.1]:Top: red(n2,x0),red(n1,x0) -> {x0 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 136:5:3:[101.1,103.7]:TopTopTop: red(n1,x0),less_than(n2,x0),less_than(x0,x1),less_than(x1,x2),red(n1,x2) ->
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n6, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 137:5:2:[73.3,8.3,101.1,9.3]:TopTop: less_than(n2,x0),red(n1,x1),less_than(x0,x1) -> red(n2,x0),red(x0,x1)
% 3.62/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n1, x1 -> n3, x2 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 139:7:1:[4.0,138.0,74.4,98.2,81.1,131.5,8.3,136.1,137.4,24.1,135.8,3.1]:Top: less_than(n3,n6),less_than(x0,n4),less_than(n2,x0),green(n2,n6),less_than(n4,n6) -> red(n3,n6),red(x0,n6)
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n4, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 140:7:5:[73.3,8.3,11.1]:TopTopTopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x3),less_than(x3,x1),red(x1,x4),red(x2,x4) -> red(x2,x0)
% 3.62/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n4, x2 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 141:6:4:[73.3,8.3]:TopTopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x3),less_than(x3,x1) -> red(x2,x0),red(x2,x1)
% 3.62/1.30 === Conflict found: 141:6:4:[73.3,8.3]:TopTopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x3),less_than(x3,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n4, x2 -> n2, x3 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 142:8:3:[141.1,131.5,11.1]:TopTopTop: less_than(x0,x1),less_than(x1,n4),less_than(n2,x1),green(n2,n6),less_than(n4,n6),red(n4,x2),red(x0,x2) -> red(x0,x1)
% 3.62/1.30 === Conflict found: 135:10:3:[8.2,134.4,73.3,8.3,11.1,131.5,73.5,8.3,9.3,101.1,99.6,110.7]:TopTopTop: less_than(x0,n4),green(n2,n6),less_than(n4,n6),less_than(n2,x0),less_than(n1,x1),less_than(x1,x0),green(n2,x2),green(n1,x2),less_than(n4,x2) -> red(x0,x2) {x0 -> n3, x1 -> n2, x2 -> n5}
% 3.62/1.30 === Backtracking. Learning clause 144:14:4:[6.0,143.6,135.7,74.4,11.1,74.4,27.2]:TopTopTopTop: less_than(x0,n4),green(n2,n6),less_than(n4,n6),less_than(n2,x0),less_than(n1,x1),less_than(x1,x0),less_than(n2,x2),less_than(x2,n5),red(x0,n6),less_than(n1,x3),less_than(x3,n5) -> red(n2,n5),red(n1,n5),red(n1,n6)
% 3.62/1.30 === Conflict found: 99:6:4:[12.2,9.3,74.4]:TopTopTopTop: green(x0,x1),less_than(x2,x1),less_than(x0,x3),less_than(x3,x2) -> red(x2,x1),red(x0,x2) {x0 -> n1, x1 -> n5, x2 -> n4, x3 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 147:16:6:[6.0,145.2,101.0,146.16,99.5,11.2,101.2,74.4,144.12,8.3,8.3,103.5,8.3,3.1,141.6,131.5,136.5]:TopTopTopTopTopTop: less_than(x0,n4),less_than(n2,x0),red(x0,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),red(n1,x1),less_than(x3,n4),less_than(n2,x3),green(n2,n6),less_than(n4,n6),red(n1,x4),less_than(n2,x4),less_than(x4,x5),less_than(x5,n6) -> red(n2,x3)
% 3.62/1.30 === Conflict found: 110:8:3:[101.1,99.6,31.1,12.1,9.3]:TopTopTop: green(n2,x0),less_than(n4,x0),less_than(n2,x1),less_than(x1,n4),green(n1,x2),less_than(n4,x2) -> red(n4,x0),red(n4,x2) {x0 -> n6, x1 -> n3, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 148:12:4:[110.7,142.6,74.4,101.2]:TopTopTopTop: green(n2,x0),less_than(n4,x0),less_than(x1,x2),less_than(x2,n4),less_than(n2,x2),green(n2,n6),less_than(n4,n6),red(x1,x0),less_than(n1,x3),less_than(x3,x0),red(n2,x0) -> red(x1,x2)
% 3.62/1.30 === Conflict found: 142:8:3:[141.1,131.5,11.1]:TopTopTop: less_than(x0,x1),less_than(x1,n4),less_than(n2,x1),green(n2,n6),less_than(n4,n6),red(n4,x2),red(x0,x2) -> red(x0,x1) {x0 -> n1, x1 -> n3, x2 -> n6}
% 3.62/1.30 === Backtracking. Learning clause 149:10:3:[142.6,110.7]:TopTopTop: less_than(x0,x1),less_than(x1,n4),less_than(n2,x1),green(n2,n6),less_than(n4,n6),red(x0,x2),green(n2,x2),green(n1,x2),less_than(n4,x2) -> red(x0,x1)
% 3.62/1.30 === Conflict found: 141:6:4:[73.3,8.3]:TopTopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x3),less_than(x3,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n4, x2 -> n1, x3 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 153:7:2:[8.2,150.4,5.0,151.5,4.0,152.6,141.6,101.2,8.3,8.3,3.1,141.6,131.5,147.7,139.6]:TopTop: less_than(x0,n4),less_than(x0,x1),less_than(x1,n5),less_than(n2,x0),green(n2,n6),less_than(n4,n6) -> red(n2,x0)
% 3.62/1.30 === Conflict found: 101:2:1:[11.1,97.1]:Top: red(n2,x0),red(n1,x0) -> {x0 -> n4}
% 3.62/1.30 === Backtracking. Learning clause 155:6:3:[136.0,154.6,101.2,141.6,99.6,140.5,8.3,3.1]:TopTopTop: green(n2,x0),less_than(x1,x0),green(x2,x1),less_than(x2,x1),red(n1,x0),less_than(n2,x2) ->
% 3.62/1.30 === Conflict found: 155:6:3:[136.0,154.6,101.2,141.6,99.6,140.5,8.3,3.1]:TopTopTop: green(n2,x0),less_than(x1,x0),green(x2,x1),less_than(x2,x1),red(n1,x0),less_than(n2,x2) -> {x0 -> n5, x1 -> n4, x2 -> n3}
% 3.62/1.30 === Backtracking. Learning clause 156:19:7:[155.1,74.4,144.13,8.3]:TopTopTopTopTopTopTop: less_than(x0,n5),green(x1,x0),less_than(x1,x0),less_than(n2,x1),less_than(n2,x2),less_than(x2,n5),less_than(x3,n4),green(n2,n6),less_than(n4,n6),less_than(n2,x3),less_than(n1,x4),less_than(x4,x3),less_than(n2,x5),red(x3,n6),less_than(n1,x5),less_than(x5,x6),less_than(x6,n5) -> red(n2,n5),red(n1,n6)
% 3.62/1.30 === Conflict found: 99:6:4:[12.2,9.3,74.4]:TopTopTopTop: green(x0,x1),less_than(x2,x1),less_than(x0,x3),less_than(x3,x2) -> red(x2,x1),red(x0,x2) {x0 -> n1, x1 -> n5, x2 -> n3, x3 -> n2}
% 3.62/1.30 === Backtracking. Learning clause 159:2:0:[6.0,157.0,5.0,158.1,99.5,11.2,74.4,8.3,101.2,156.18,8.3,139.6,8.3,3.1,155.5,131.5,101.2,153.7,4.1,8.3]:: green(n2,n6),less_than(n4,n6) ->
% 1.14/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n2, x1 -> n3, x2 -> n6}
% 1.14/1.30 === Backtracking. Learning clause 160:3:0:[74.1,4.1,20.2,159.1]:: less_than(n3,n5),less_than(n4,n6) -> red(n2,n6)
% 1.14/1.30 === Conflict found: 16:2:1:[8.2,5.1]:Top: less_than(x0,n3) -> less_than(x0,n4) {x0 -> n2}
% 1.14/1.30 === Backtracking. Learning clause 161:4:1:[16.1,4.1,137.1]:Top: red(n1,x0),less_than(n4,x0) -> red(n2,n4),red(n4,x0)
% 1.14/1.30 === Conflict found: 74:4:3:[9.1,8.3]:TopTopTop: less_than(x0,x1),less_than(x1,x2) -> red(x0,x2),green(x0,x2) {x0 -> n2, x1 -> n4, x2 -> n6}
% 1.14/1.30 === Backtracking. Learning clause 162:4:1:[74.4,159.1]:Top: less_than(n2,x0),less_than(x0,n6),less_than(n4,n6) -> red(n2,n6)
% 1.14/1.30 === Conflict found: 16:2:1:[8.2,5.1]:Top: less_than(x0,n3) -> less_than(x0,n4) {x0 -> n2}
% 1.14/1.30 === Backtracking. Learning clause 163:2:0:[16.1,4.1,162.1,101.1]:: less_than(n4,n6),red(n1,n6) ->
% 1.14/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n1, x1 -> n3, x2 -> n5}
% 1.14/1.30 === Backtracking. Learning clause 164:6:3:[11.2,137.5]:TopTopTop: red(x0,x1),red(x0,x2),less_than(n2,x1),red(n1,x2),less_than(x1,x2) -> red(n2,x1)
% 1.14/1.30 === Conflict found: 164:6:3:[11.2,137.5]:TopTopTop: red(x0,x1),red(x0,x2),less_than(n2,x1),red(n1,x2),less_than(x1,x2) -> red(n2,x1) {x0 -> n1, x1 -> n4, x2 -> n5}
% 1.14/1.30 === Backtracking. Learning clause 165:10:5:[164.1,99.6]:TopTopTopTopTop: red(x0,x1),less_than(n2,x2),red(n1,x1),less_than(x2,x1),green(x0,x3),less_than(x2,x3),less_than(x0,x4),less_than(x4,x2) -> red(n2,x2),red(x2,x3)
% 1.14/1.30 === Conflict found: 101:2:1:[11.1,97.1]:Top: red(n2,x0),red(n1,x0) -> {x0 -> n4}
% 1.14/1.30 === Backtracking. Learning clause 166:8:3:[101.2,99.6,165.9,24.2]:TopTopTop: less_than(n2,x0),red(n1,x1),less_than(x0,x1),less_than(x0,n6),less_than(n1,x2),less_than(x2,x0) -> red(x0,n6),red(n1,n6)
% 1.14/1.30 === Conflict found: 17:2:0:[9.1,5.1]:: -> red(n3,n4),green(n3,n4) {}
% 1.14/1.30 === Backtracking. Learning clause 168:8:1:[163.1,167.8,17.1,11.2,73.1,4.1,99.6,24.2]:Top: red(n1,n3),less_than(n2,n4),less_than(n4,n6),less_than(n1,x0),less_than(x0,n4) -> red(n2,n3),red(n2,n4),red(n4,n6)
% 1.14/1.30 === Conflict found: 99:6:4:[12.2,9.3,74.4]:TopTopTopTop: green(x0,x1),less_than(x2,x1),less_than(x0,x3),less_than(x3,x2) -> red(x2,x1),red(x0,x2) {x0 -> n1, x1 -> n6, x2 -> n4, x3 -> n2}
% 1.14/1.30 === Backtracking. Learning clause 171:6:1:[163.1,169.5,101.0,170.6,99.1,24.2,101.2,168.7]:Top: red(n1,n3),less_than(n2,n4),less_than(n4,n6),less_than(n1,x0),less_than(x0,n4) -> red(n4,n6)
% 1.14/1.30 === Conflict found: 136:5:3:[101.1,103.7]:TopTopTop: red(n1,x0),less_than(n2,x0),less_than(x0,x1),less_than(x1,x2),red(n1,x2) -> {x0 -> n3, x1 -> n4, x2 -> n5}
% 1.14/1.30 === Backtracking. Learning clause 173:3:1:[4.0,172.1,136.3,5.1]:Top: red(n1,n3),less_than(n4,x0),red(n1,x0) ->
% 1.14/1.30 === Conflict found: 116:16:7:[113.9,8.3]:TopTopTopTopTopTopTop: less_than(n2,x0),less_than(x0,n6),less_than(x1,n4),less_than(n4,n6),less_than(n2,x1),less_than(x1,x2),less_than(x2,n5),less_than(n4,x3),less_than(x4,x3),less_than(n2,x5),less_than(x5,x3),less_than(n1,x6),less_than(x6,x4) -> green(x1,n4),red(n1,x3),red(n2,x3) {x0 -> n3, x1 -> n3, x2 -> n4, x3 -> n5, x4 -> n3, x5 -> n4, x6 -> n2}
% 1.14/1.30 === Backtracking. Learning clause 176:12:5:[4.0,174.2,6.0,175.3,116.3,5.1,20.2]:TopTopTopTopTop: less_than(n2,x0),less_than(n4,n6),less_than(n4,x1),less_than(x2,x1),less_than(n2,x3),less_than(x3,x1),less_than(n1,x4),less_than(x4,x2),less_than(x0,n5) -> green(n3,n4),red(n1,x1),red(n2,x1)
% 1.14/1.30 === Conflict found: 105:12:4:[101.0,104.11,11.1,34.2,27.2,102.7,11.3,9.2,100.6]:TopTopTopTop: less_than(n2,x0),less_than(n2,x1),less_than(x1,n6),less_than(x0,x2),less_than(x2,n6),red(n1,x0),red(n1,x3),less_than(x3,n4),green(n1,n6),less_than(n4,n6) -> red(n1,n5),green(x3,n4) {x0 -> n3, x1 -> n4, x2 -> n4, x3 -> n3}
% 1.14/1.30 === Backtracking. Learning clause 179:4:0:[6.0,177.3,173.2,178.5,105.4,5.1,73.1,101.1,4.1,24.2,173.3]:: less_than(n4,n6),less_than(n2,n4),red(n1,n3) -> red(n2,n4)
% 1.14/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n2, x1 -> n4, x2 -> n6}
% 1.14/1.30 === Backtracking. Learning clause 181:5:1:[162.3,180.0,11.2,171.6,179.4]:Top: less_than(n1,x0),less_than(x0,n4),less_than(n4,n6),less_than(n2,n4),red(n1,n3) ->
% 1.14/1.30 === Conflict found: 164:6:3:[11.2,137.5]:TopTopTop: red(x0,x1),red(x0,x2),less_than(n2,x1),red(n1,x2),less_than(x1,x2) -> red(n2,x1) {x0 -> n3, x1 -> n4, x2 -> n5}
% 1.14/1.30 === Backtracking. Learning clause 183:7:1:[4.0,182.2,164.1,17.1,137.5]:Top: less_than(n2,n4),less_than(n4,x0),red(n1,x0),less_than(n3,x0) -> red(n2,n4),green(n3,n4),red(n2,n3)
% 1.14/1.30 === Conflict found: 166:8:3:[101.2,99.6,165.9,24.2]:TopTopTop: less_than(n2,x0),red(n1,x1),less_than(x0,x1),less_than(x0,n6),less_than(n1,x2),less_than(x2,x0) -> red(x0,n6),red(n1,n6) {x0 -> n3, x1 -> n5, x2 -> n2}
% 1.14/1.30 === Backtracking. Learning clause 186:8:2:[4.0,184.0,163.1,185.7,166.4,8.3,11.2,162.4,183.7,8.3,5.1]:TopTop: less_than(n1,x0),less_than(x0,n3),less_than(n4,n6),less_than(n2,n4),red(n1,x1),less_than(n4,x1) -> red(n2,n4),green(n3,n4)
% 1.14/1.30 === Conflict found: 166:8:3:[101.2,99.6,165.9,24.2]:TopTopTop: less_than(n2,x0),red(n1,x1),less_than(x0,x1),less_than(x0,n6),less_than(n1,x2),less_than(x2,x0) -> red(x0,n6),red(n1,n6) {x0 -> n3, x1 -> n5, x2 -> n2}
% 1.14/1.30 === Backtracking. Learning clause 189:5:1:[3.0,187.0,163.1,188.5,166.4,8.3,11.2,162.4,8.3,5.1,73.4,186.8,4.1]:Top: less_than(n4,n6),less_than(n2,n4),red(n1,x0),less_than(n4,x0) -> red(n2,n4)
% 1.14/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n3, x1 -> n5, x2 -> n6}
% 1.14/1.30 === Backtracking. Learning clause 191:13:4:[3.0,190.5,11.2,27.2,165.10,74.4,14.2,99.6]:TopTopTopTop: red(x0,n6),less_than(n2,x0),less_than(x0,x1),less_than(x0,n5),less_than(n3,n5),green(n1,x2),less_than(x1,x2),less_than(n1,x3),less_than(x3,x1) -> red(n1,n6),red(n2,x0),red(n1,n5),red(x1,x2)
% 1.14/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n3, x1 -> n4, x2 -> n6}
% 1.14/1.30 === Backtracking. Learning clause 196:5:0:[24.1,192.0,3.0,193.1,20.1,194.3,6.0,195.4,11.1,17.1,191.13,99.5,181.5,8.3,8.3,5.1,4.1]:: less_than(n2,n4) -> green(n3,n4),red(n1,n6),red(n2,n3),red(n1,n5)
% 1.14/1.30 === Conflict found: 73:5:3:[12.1,9.3,9.3]:TopTopTop: green(x0,x1),less_than(x2,x0),less_than(x2,x1) -> red(x2,x0),red(x2,x1) {x0 -> n3, x1 -> n4, x2 -> n2}
% 1.14/1.30 === Backtracking. Learning clause 197:5:0:[73.2,4.1,196.2]:: less_than(n2,n4) -> red(n2,n4),red(n1,n6),red(n2,n3),red(n1,n5)
% 1.14/1.30 === Conflict found: 11:3:3:[10.0,1.3]:TopTopTop: red(x0,x1),red(x1,x2),red(x0,x2) -> {x0 -> n2, x1 -> n3, x2 -> n6}
% 1.14/1.30 === Backtracking. Learning clause 201:3:0:[3.0,198.0,20.1,199.1,6.0,200.3,11.3,162.4,99.5,24.2,181.5,8.3,5.1,4.1,197.4,189.3]:: less_than(n2,n4) -> red(n1,n6),red(n2,n4)
% 1.14/1.30 === Conflict found: 99:6:4:[12.2,9.3,74.4]:TopTopTopTop: green(x0,x1),less_than(x2,x1),less_than(x0,x3),less_than(x3,x2) -> red(x2,x1),red(x0,x2) {x0 -> n1, x1 -> n6, x2 -> n4, x3 -> n2}
% 1.14/1.30 === Backtracking. Learning clause 203:2:0:[163.1,202.2,99.3,3.1,101.2,11.2,162.4,24.2,201.3]:: less_than(n4,n6),less_than(n2,n4) ->
% 1.14/1.30
% 1.14/1.30 SZS status Unsatisfiable
% 1.14/1.30
% 1.14/1.30 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.14/1.30
% 1.14/1.30 SPASS-SCL-FOL Statistics:
% 1.14/1.30 Number of learned clauses: 126
% 1.14/1.30 Number of propagations: 1759
% 1.14/1.30 Number of decisions: 493
% 1.14/1.30 Number of resolutions: 565
% 1.14/1.30 Number of condensations: 43
% 1.14/1.30 Number of sub resolutions: 67
% 1.14/1.30 Number of input literals (deduplicated): 9
% 1.14/1.30 Number of grows: 8
% 1.14/1.30 Number of considered ground atoms: 109
% 1.14/1.30
% 1.14/1.30 Needed: 0:00:00.75
% 1.14/1.30
%------------------------------------------------------------------------------