%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN067-3 : TPTP v9.2.1. Released v1.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:39:13 PM UTC 2026
% Result : Unsatisfiable 25.04s 6.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN067-3 : TPTP v9.2.1. Released v1.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n008.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:39:29 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 30.72/6.70 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.72/6.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.72/6.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.72/6.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.72/6.70 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.72/6.70 Execution resolution_2 ended with status: unsatisfiable
% 30.72/6.70 Used heuristic: resolution_2
% 30.72/6.70
% 30.72/6.70 Input Clauses:
% 30.72/6.70
% 30.72/6.70 Predicates: big_p big_r
% 30.72/6.70 Fol Constants: a sk10 sk8 sk7 sk9
% 30.72/6.70 Fol Functions: sk1 sk3 sk4 sk2 sk5 sk6
% 30.72/6.70 Problem Properties:
% 30.72/6.70 This is a full first-order problem without equality.
% 30.72/6.70
% 30.72/6.70 After reduction: Problem Properties:
% 30.72/6.70 This is a full first-order problem without equality.
% 30.72/6.70
% 30.72/6.70
% 30.72/6.70 Reduced Input Clauses:
% 30.72/6.70 47:4:2:[37.0,1.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_p(sk3(x0))
% 30.72/6.70 48:4:2:[37.0,2.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_r(x0,sk4(x0))
% 30.72/6.70 49:4:2:[37.0,3.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_r(sk4(x0),sk3(x0))
% 30.72/6.70 50:4:2:[37.0,4.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(x1,sk2(x1))
% 30.72/6.70 51:4:2:[37.0,5.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x0,sk4(x0)),big_r(x1,sk2(x1))
% 30.72/6.70 52:4:2:[37.0,6.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x1,sk2(x1)),big_r(sk4(x0),sk3(x0))
% 30.72/6.70 53:5:3:[37.0,7.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x2)),big_p(sk5(x1))
% 30.72/6.70 54:5:3:[37.0,8.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x2)),big_r(x1,sk6(x1))
% 30.72/6.70 55:5:3:[37.0,9.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x2)),big_r(sk6(x1),sk5(x1))
% 30.72/6.70 56:5:3:[37.0,10.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk5(x1)),big_r(x2,sk2(x2))
% 30.72/6.70 57:5:3:[37.0,11.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x1,sk6(x1)),big_r(x2,sk2(x2))
% 30.72/6.70 58:5:3:[37.0,12.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,sk2(x2)),big_r(sk6(x1),sk5(x1))
% 30.72/6.70 59:4:2:[37.0,13.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(sk2(x1),sk1(x1))
% 30.72/6.70 60:4:2:[37.0,14.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x0,sk4(x0)),big_r(sk2(x1),sk1(x1))
% 30.72/6.70 61:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1)),big_r(sk4(x0),sk3(x0))
% 30.72/6.70 62:5:3:[37.0,16.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x1)),big_p(sk3(x2))
% 30.72/6.70 63:5:3:[37.0,17.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk3(x2)),big_r(x1,sk2(x1))
% 30.72/6.70 64:5:3:[37.0,18.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x1)),big_r(x2,sk4(x2))
% 30.72/6.70 65:5:3:[37.0,19.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,sk4(x2)),big_r(x1,sk2(x1))
% 30.72/6.70 66:5:3:[37.0,20.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk3(x2)),big_r(sk2(x1),sk1(x1))
% 30.72/6.70 67:5:3:[37.0,21.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,sk4(x2)),big_r(sk2(x1),sk1(x1))
% 30.72/6.70 68:5:3:[37.0,22.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x1)),big_r(sk4(x2),sk3(x2))
% 30.72/6.70 69:5:3:[37.0,23.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x1,sk2(x1)),big_r(sk4(x2),sk3(x2))
% 30.72/6.70 70:5:3:[37.0,24.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(sk2(x1),sk1(x1)),big_r(sk4(x2),sk3(x2))
% 30.72/6.70 71:5:3:[37.0,25.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk5(x1)),big_r(sk2(x2),sk1(x2))
% 30.72/6.70 72:5:3:[37.0,26.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x1,sk6(x1)),big_r(sk2(x2),sk1(x2))
% 30.72/6.70 73:5:3:[37.0,27.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(sk2(x2),sk1(x2)),big_r(sk6(x1),sk5(x1))
% 30.72/6.70 74:6:4:[37.0,28.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk1(x3)),big_p(sk5(x2))
% 30.72/6.70 75:6:4:[37.0,29.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk5(x2)),big_r(x3,sk2(x3))
% 30.72/6.70 76:6:4:[37.0,30.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk1(x3)),big_r(x2,sk6(x2))
% 30.72/6.70 77:6:4:[37.0,31.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(x2,sk6(x2)),big_r(x3,sk2(x3))
% 30.72/6.70 78:6:4:[37.0,32.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk5(x2)),big_r(sk2(x3),sk1(x3))
% 30.72/6.70 79:6:4:[37.0,33.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(x2,sk6(x2)),big_r(sk2(x3),sk1(x3))
% 30.72/6.70 80:6:4:[37.0,34.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk1(x3)),big_r(sk6(x2),sk5(x2))
% 30.72/6.70 81:6:4:[37.0,35.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(x3,sk2(x3)),big_r(sk6(x2),sk5(x2))
% 30.72/6.70 82:6:4:[37.0,36.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(sk2(x3),sk1(x3)),big_r(sk6(x2),sk5(x2))
% 30.72/6.70
% 30.72/6.70 Most General Atoms: big_p(x2) big_r(x3,x1)
% 30.72/6.70
% 30.72/6.70 === Starting SPASS-SCL-FOL A Little Less Naive, considering 46 atoms initially, heuristics mode: resolution_2 ===
% 30.72/6.70
% 30.72/6.70 === Clause set with instances from active satisfied. Growing active. New size: 46
% 30.72/6.70 === Restarting.
% 30.72/6.70 === Conflict found: 81:6:4:[37.0,35.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(x3,sk2(x3)),big_r(sk6(x2),sk5(x2)) {x0 -> a, x1 -> a, x2 -> a, x3 -> a}
% 30.72/6.70 === Backtracking. Learning clause 83:4:2:[81.1,37.1]:TopTop: big_r(x0,a),big_r(x1,a) -> big_r(x1,sk2(x1)),big_r(sk6(x0),sk5(x0))
% 30.72/6.70 === Conflict found: 80:6:4:[37.0,34.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk1(x3)),big_r(sk6(x2),sk5(x2)) {x0 -> a, x1 -> a, x2 -> a, x3 -> a}
% 30.72/6.70 === Backtracking. Learning clause 84:4:2:[80.1,37.1]:TopTop: big_r(x0,a),big_r(x1,a) -> big_p(sk1(x1)),big_r(sk6(x0),sk5(x0))
% 30.72/6.70 === Backtracking. Learning clause 85:4:1:[42.1,37.1]:Top: big_p(sk7),big_r(x0,a),big_r(sk9,x0) -> big_p(sk8)
% 30.72/6.70 === Clause set with instances from active satisfied. Growing active. New size: 52
% 30.72/6.70 === Restarting.
% 30.72/6.70 === Conflict found: 61:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk9, x1 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 86:5:0:[61.1,38.2]:: big_p(sk7) -> big_r(sk2(sk9),sk1(sk9)),big_r(sk4(sk9),sk3(sk9)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 87:4:0:[42.1,49.3,52.3,86.2,38.2]:: big_p(sk7) -> big_r(sk4(sk9),sk3(sk9)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 88:7:2:[42.4,60.3,59.3]:TopTop: big_p(sk7),big_r(sk4(sk9),sk3(x0)) -> big_p(sk8),big_p(sk9),big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1))
% 30.72/6.70 === Backtracking. Learning clause 89:7:2:[42.1,47.3,50.4]:TopTop: big_p(sk7),big_r(sk2(sk9),sk1(x0)) -> big_p(sk8),big_p(x0),big_p(x1),big_p(sk9),big_p(sk3(x1))
% 30.72/6.70 === Backtracking. Learning clause 90:3:0:[42.1,48.3,51.4,42.4,89.7,88.7,87.2,38.2]:: big_p(sk7) -> big_p(sk10),big_p(sk8)
% 30.72/6.70 === Clause set with instances from active satisfied. Growing active. New size: 59
% 30.72/6.70 === Restarting.
% 30.72/6.70 === Conflict found: 61:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk7, x1 -> sk7}
% 30.72/6.70 === Backtracking. Learning clause 91:4:0:[61.1,90.1]:: -> big_r(sk2(sk7),sk1(sk7)),big_r(sk4(sk7),sk3(sk7)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 92:6:0:[44.1,47.3,52.3,91.1,90.1,59.1]:: -> big_p(sk3(sk7)),big_r(sk4(sk7),sk3(sk7)),big_p(sk10),big_p(sk8),big_p(sk3(sk9)),big_r(sk2(sk9),sk1(sk9))
% 30.72/6.70 === Backtracking. Learning clause 93:5:0:[44.1,47.3,52.3,91.1,61.2,90.1]:: -> big_p(sk3(sk7)),big_r(sk2(sk9),sk1(sk9)),big_r(sk4(sk7),sk3(sk7)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 94:10:4:[46.2,47.3,52.3,50.4,47.3]:TopTopTopTop: big_r(sk2(sk9),sk1(x0)),big_r(sk2(sk7),sk1(x1)) -> big_p(x1),big_p(x2),big_p(sk7),big_r(sk4(x2),sk3(x2)),big_p(sk9),big_p(x3),big_p(x0),big_p(sk3(x3))
% 30.72/6.70 === Backtracking. Learning clause 95:4:0:[44.4,52.3,47.3,94.7,91.1,90.1,93.2]:: -> big_p(sk3(sk7)),big_r(sk4(sk7),sk3(sk7)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 96:4:0:[46.6,50.4,47.3,59.4,50.4,47.3,59.4,90.1]:: -> big_p(sk9),big_p(sk3(sk7)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 97:3:0:[44.3,59.4,47.3,50.4,90.1,96.1]:: -> big_p(sk3(sk7)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 99:5:1:[90.0,98.0,46.5,48.4,49.4,49.4,48.4,97.1,47.4]:Top: -> big_p(sk10),big_p(sk8),big_p(sk9),big_p(x0),big_p(sk1(x0))
% 30.72/6.70 === Conflict found: 99:5:1:[90.0,98.0,46.5,48.4,49.4,49.4,48.4,97.1,47.4]:Top: -> big_p(sk10),big_p(sk8),big_p(sk9),big_p(x0),big_p(sk1(x0)) {x0 -> sk7}
% 30.72/6.70 === Backtracking. Learning clause 100:4:0:[99.4,90.1]:: -> big_p(sk9),big_p(sk1(sk7)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 102:5:1:[90.0,101.0,46.5,51.3,52.4,52.4,97.1,51.3,50.3]:Top: -> big_p(sk10),big_p(sk8),big_p(sk9),big_p(x0),big_r(x0,sk2(x0))
% 30.72/6.70 === Backtracking. Learning clause 104:4:0:[90.0,103.0,46.5,60.3,91.2,61.4,60.3,97.1,59.3]:: -> big_r(sk2(sk7),sk1(sk7)),big_p(sk10),big_p(sk8),big_p(sk9)
% 30.72/6.70 === Backtracking. Learning clause 106:7:3:[44.1,105.6,46.1,99.5,102.5,59.4]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1) -> big_p(sk10),big_p(sk8),big_p(x2),big_p(sk3(x2))
% 30.72/6.70 === Backtracking. Learning clause 107:3:0:[46.3,61.4,60.3,46.3,99.5,102.5,106.7,102.5,90.1,104.1,100.2]:: -> big_p(sk9),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 110:4:1:[99.2,108.0,90.0,109.1,44.4,48.4,49.4,97.1]:Top: -> big_p(x0),big_p(sk1(x0)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Conflict found: 110:4:1:[99.2,108.0,90.0,109.1,44.4,48.4,49.4,97.1]:Top: -> big_p(x0),big_p(sk1(x0)),big_p(sk10),big_p(sk8) {x0 -> sk7}
% 30.72/6.70 === Backtracking. Learning clause 111:3:0:[110.1,90.1]:: -> big_p(sk1(sk7)),big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 113:5:1:[50.2,112.0,44.4,51.3,52.4]:Top: big_p(sk9) -> big_p(sk10),big_p(sk7),big_p(x0),big_r(x0,sk2(x0))
% 30.72/6.70 === Backtracking. Learning clause 114:2:0:[44.1,97.1,60.3,91.2,44.3,113.5,107.1,90.1,111.1]:: -> big_p(sk10),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 115:4:1:[46.3,52.4,51.3,50.3,50.3,51.3,52.4,113.1]:Top: -> big_p(sk10),big_p(sk7),big_p(x0),big_r(x0,sk2(x0))
% 30.72/6.70 === Conflict found: 62:5:3:[37.0,16.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x1)),big_p(sk3(x2)) {x0 -> sk8, x1 -> sk7, x2 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 117:5:1:[47.1,116.0,62.2,43.5,114.2,47.3,50.4,59.4]:Top: -> big_p(sk1(sk7)),big_p(sk10),big_p(x0),big_p(sk9),big_p(sk3(x0))
% 30.72/6.70 === Clause set with instances from active satisfied. Growing active. New size: 65
% 30.72/6.70 === Restarting.
% 30.72/6.70 === Conflict found: 80:6:4:[37.0,34.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk1(x3)),big_r(sk6(x2),sk5(x2)) {x0 -> sk10, x1 -> a, x2 -> sk9, x3 -> a}
% 30.72/6.70 === Backtracking. Learning clause 119:7:2:[38.2,118.0,80.3,39.4]:TopTop: big_p(x0),big_r(x1,x0),big_p(sk7),big_p(sk9) -> big_p(sk1(x1)),big_r(sk6(sk9),sk5(sk9)),big_p(sk8)
% 30.72/6.70 === Conflict found: 119:7:2:[38.2,118.0,80.3,39.4]:TopTop: big_p(x0),big_r(x1,x0),big_p(sk7),big_p(sk9) -> big_p(sk1(x1)),big_r(sk6(sk9),sk5(sk9)),big_p(sk8) {x0 -> sk10, x1 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 121:5:0:[38.2,120.0,119.2,39.4]:: big_p(sk7),big_p(sk9) -> big_p(sk1(sk9)),big_r(sk6(sk9),sk5(sk9)),big_p(sk8)
% 30.72/6.70 === Conflict found: 77:6:4:[37.0,31.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(x2,sk6(x2)),big_r(x3,sk2(x3)) {x0 -> sk10, x1 -> sk9, x2 -> sk9, x3 -> sk7}
% 30.72/6.70 === Backtracking. Learning clause 123:7:2:[38.2,122.0,77.3,39.4]:TopTop: big_p(x0),big_r(x1,x0),big_p(sk7),big_p(sk9) -> big_r(sk9,sk6(sk9)),big_r(x1,sk2(x1)),big_p(sk8)
% 30.72/6.70 === Conflict found: 76:6:4:[37.0,30.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk1(x3)),big_r(x2,sk6(x2)) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 125:5:0:[38.2,124.0,76.3,39.4]:: big_p(sk7),big_p(sk9) -> big_p(sk1(sk9)),big_r(sk9,sk6(sk9)),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 126:5:0:[43.4,39.4,37.1]:: big_r(sk10,a),big_p(sk7),big_p(sk9) -> big_r(sk7,sk8),big_p(sk8)
% 30.72/6.70 === Conflict found: 85:4:1:[42.1,37.1]:Top: big_p(sk7),big_r(x0,a),big_r(sk9,x0) -> big_p(sk8) {x0 -> sk10}
% 30.72/6.70 === Backtracking. Learning clause 127:4:0:[85.3,39.4]:: big_r(sk10,a),big_p(sk7),big_p(sk9) -> big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 129:7:1:[39.3,128.0,43.4,125.4,121.4,75.5,38.3]:Top: big_r(x0,sk10),big_p(sk7),big_p(sk9) -> big_r(sk7,sk8),big_p(sk1(sk9)),big_r(x0,sk2(x0)),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 131:6:1:[39.3,130.0,42.1,75.5,121.4,125.4,38.3]:Top: big_r(x0,sk10),big_p(sk7),big_p(sk9) -> big_r(x0,sk2(x0)),big_p(sk1(sk9)),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 133:4:0:[39.3,132.0,42.4,125.4,74.6,121.4,38.3]:: big_p(sk7),big_p(sk9) -> big_p(sk1(sk9)),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 134:8:3:[42.1,75.5,81.6,123.5]:TopTopTop: big_p(x0),big_r(sk9,x0),big_p(x1),big_r(x2,x1),big_p(sk7),big_p(sk9) -> big_r(x2,sk2(x2)),big_p(sk8)
% 30.72/6.70 === Conflict found: 82:6:4:[37.0,36.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(sk2(x3),sk1(x3)),big_r(sk6(x2),sk5(x2)) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 136:8:4:[80.4,135.4,82.5,42.3]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1),big_p(sk7),big_r(sk9,sk2(x3)) -> big_r(sk6(x2),sk5(x2)),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 137:3:0:[42.4,79.5,78.5,42.3,136.7,134.7,38.3,39.4,133.3]:: big_p(sk7),big_p(sk9) -> big_p(sk8)
% 30.72/6.70 === Clause set with instances from active satisfied. Growing active. New size: 129
% 30.72/6.70 === Backtracking. Learning clause 139:4:0:[39.2,138.0,45.1,75.5,81.6,77.5,41.3]:: big_p(sk7),big_p(sk9) -> big_r(sk7,sk2(sk7)),big_r(sk9,sk10)
% 30.72/6.70 === Backtracking. Learning clause 140:8:3:[45.4,79.5,82.6,78.5,45.3]:TopTopTop: big_p(x0),big_p(x1),big_r(sk7,x0),big_r(x2,x1),big_p(sk1(x2)),big_p(sk9),big_r(sk7,sk2(x2)) -> big_r(sk9,sk10)
% 30.72/6.70 === Backtracking. Learning clause 141:3:0:[45.3,80.6,74.6,76.6,140.5,137.3,41.3,139.3]:: big_p(sk7),big_p(sk9) -> big_r(sk9,sk10)
% 30.72/6.70 === Backtracking. Learning clause 142:7:2:[44.3,81.6,75.5,77.5,137.3,40.4,80.1]:TopTop: big_p(sk7),big_p(sk9),big_r(x0,sk10),big_r(x1,sk10) -> big_r(sk7,sk2(sk7)),big_p(sk1(x1)),big_r(sk6(x0),sk5(x0))
% 30.72/6.70 === Backtracking. Learning clause 144:6:1:[41.3,143.2,43.3,82.5,81.5,40.3]:Top: big_p(sk1(sk9)),big_r(x0,sk10),big_p(sk7),big_p(sk9) -> big_r(sk6(x0),sk5(x0)),big_r(sk7,sk8)
% 30.72/6.70 === Backtracking. Learning clause 146:5:1:[139.3,145.3,44.4,77.5,75.5,81.6,81.1,137.3,144.6,142.6]:Top: big_p(sk7),big_p(sk9),big_r(x0,sk10) -> big_r(sk7,sk2(sk7)),big_r(sk6(x0),sk5(x0))
% 30.72/6.70 === Backtracking. Learning clause 147:10:5:[43.4,76.6,74.6]:TopTopTopTopTop: big_p(sk7),big_r(sk6(sk9),sk5(x0)),big_p(x1),big_r(sk9,x1),big_p(x2),big_p(x3),big_r(x0,x2),big_r(x4,x3) -> big_r(sk7,sk8),big_p(sk1(x4))
% 30.72/6.70 === Backtracking. Learning clause 148:10:5:[43.4,77.5,75.5]:TopTopTopTopTop: big_p(sk7),big_r(sk6(sk9),sk5(x0)),big_p(x1),big_r(sk9,x1),big_p(x2),big_p(x3),big_r(x0,x2),big_r(x4,x3) -> big_r(sk7,sk8),big_r(x4,sk2(x4))
% 30.72/6.70 === Conflict found: 79:6:4:[37.0,33.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(x2,sk6(x2)),big_r(sk2(x3),sk1(x3)) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 150:8:4:[76.4,149.4,79.6,43.3]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1),big_p(sk7),big_r(sk9,sk2(x3)) -> big_r(x2,sk6(x2)),big_r(sk7,sk8)
% 30.72/6.70 === Conflict found: 78:6:4:[37.0,32.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk5(x2)),big_r(sk2(x3),sk1(x3)) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 152:4:0:[41.3,151.0,78.6,43.3,43.1,150.7,148.10,147.10,146.5,40.3]:: big_p(sk7),big_p(sk9) -> big_r(sk7,sk2(sk7)),big_r(sk7,sk8)
% 30.72/6.70 === Backtracking. Learning clause 153:9:3:[44.3,81.6,75.5,77.5,137.3,76.1]:TopTopTop: big_r(sk7,sk8),big_r(x0,sk8),big_p(sk7),big_p(sk9),big_r(x1,sk10),big_r(x2,sk10) -> big_r(x0,sk2(x0)),big_p(sk1(x2)),big_r(x1,sk6(x1))
% 30.72/6.70 === Conflict found: 77:6:4:[37.0,31.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(x2,sk6(x2)),big_r(x3,sk2(x3)) {x0 -> sk10, x1 -> sk8, x2 -> sk9, x3 -> sk7}
% 30.72/6.70 === Backtracking. Learning clause 154:7:3:[77.2,137.3]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(x2,sk8),big_p(sk7),big_p(sk9) -> big_r(x1,sk6(x1)),big_r(x2,sk2(x2))
% 30.72/6.70 === Backtracking. Learning clause 155:7:2:[44.3,81.6,75.5,154.6,137.3,154.1]:TopTop: big_r(sk7,sk8),big_r(x0,sk10),big_r(x1,sk8),big_p(sk7),big_p(sk9) -> big_r(x0,sk6(x0)),big_r(x1,sk2(x1))
% 30.72/6.70 === Backtracking. Learning clause 158:5:1:[152.3,156.2,139.3,157.3,46.3,146.5,75.5,154.6,81.6,75.5,137.3,155.6]:Top: big_p(x0),big_r(sk9,x0),big_p(sk7),big_p(sk9) -> big_r(sk7,sk2(sk7))
% 30.72/6.70 === Conflict found: 153:9:3:[44.3,81.6,75.5,77.5,137.3,76.1]:TopTopTop: big_r(sk7,sk8),big_r(x0,sk8),big_p(sk7),big_p(sk9),big_r(x1,sk10),big_r(x2,sk10) -> big_r(x0,sk2(x0)),big_p(sk1(x2)),big_r(x1,sk6(x1)) {x0 -> sk7, x1 -> sk9, x2 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 159:7:2:[153.1,152.4]:TopTop: big_r(x0,sk10),big_r(x1,sk10),big_p(sk7),big_p(sk9) -> big_p(sk1(x1)),big_r(x0,sk6(x0)),big_r(sk7,sk2(sk7))
% 30.72/6.70 === Conflict found: 155:7:2:[44.3,81.6,75.5,154.6,137.3,154.1]:TopTop: big_r(sk7,sk8),big_r(x0,sk10),big_r(x1,sk8),big_p(sk7),big_p(sk9) -> big_r(x0,sk6(x0)),big_r(x1,sk2(x1)) {x0 -> sk9, x1 -> sk7}
% 30.72/6.70 === Backtracking. Learning clause 160:5:1:[155.1,152.4]:Top: big_r(x0,sk10),big_p(sk7),big_p(sk9) -> big_r(x0,sk6(x0)),big_r(sk7,sk2(sk7))
% 30.72/6.70 === Backtracking. Learning clause 162:3:0:[139.3,161.0,44.1,75.5,81.6,154.6,137.3,152.4,158.1]:: big_p(sk7),big_p(sk9) -> big_r(sk7,sk2(sk7))
% 30.72/6.70 === Conflict found: 81:6:4:[37.0,35.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_r(x3,sk2(x3)),big_r(sk6(x2),sk5(x2)) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 163:5:0:[81.3,141.3]:: big_p(sk10),big_p(sk7),big_p(sk9) -> big_r(sk9,sk2(sk9)),big_r(sk6(sk9),sk5(sk9))
% 30.72/6.70 === Conflict found: 150:8:4:[76.4,149.4,79.6,43.3]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1),big_p(sk7),big_r(sk9,sk2(x3)) -> big_r(x2,sk6(x2)),big_r(sk7,sk8) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 165:5:0:[40.2,164.0,150.3,141.3,163.4]:: big_p(sk7),big_p(sk9) -> big_r(sk9,sk6(sk9)),big_r(sk7,sk8),big_r(sk6(sk9),sk5(sk9))
% 30.72/6.70 === Conflict found: 148:10:5:[43.4,77.5,75.5]:TopTopTopTopTop: big_p(sk7),big_r(sk6(sk9),sk5(x0)),big_p(x1),big_r(sk9,x1),big_p(x2),big_p(x3),big_r(x0,x2),big_r(x4,x3) -> big_r(sk7,sk8),big_r(x4,sk2(x4)) {x0 -> sk9, x1 -> sk10, x2 -> sk10, x3 -> sk10, x4 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 168:4:0:[163.4,166.0,40.2,167.1,148.4,141.3]:: big_p(sk7),big_p(sk9) -> big_r(sk7,sk8),big_r(sk9,sk2(sk9))
% 30.72/6.70 === Conflict found: 150:8:4:[76.4,149.4,79.6,43.3]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1),big_p(sk7),big_r(sk9,sk2(x3)) -> big_r(x2,sk6(x2)),big_r(sk7,sk8) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 170:4:0:[40.2,169.0,150.3,141.3,168.4]:: big_p(sk7),big_p(sk9) -> big_r(sk9,sk6(sk9)),big_r(sk7,sk8)
% 30.72/6.70 === Backtracking. Learning clause 172:4:0:[137.2,171.0,46.4,79.6,76.5,162.3,79.6,76.5,77.6,141.3,170.4]:: big_p(sk10),big_p(sk7),big_p(sk9) -> big_r(sk9,sk6(sk9))
% 30.72/6.70 === Backtracking. Learning clause 173:9:4:[46.1,75.5,81.6,77.5,81.6,75.5,137.3,168.3]:TopTopTopTop: big_r(sk9,sk6(x0)),big_p(x1),big_r(x0,x1),big_p(x2),big_r(x3,x2),big_p(sk7),big_p(sk9) -> big_r(x3,sk2(x3)),big_r(sk9,sk2(sk9))
% 30.72/6.70 === Conflict found: 147:10:5:[43.4,76.6,74.6]:TopTopTopTopTop: big_p(sk7),big_r(sk6(sk9),sk5(x0)),big_p(x1),big_r(sk9,x1),big_p(x2),big_p(x3),big_r(x0,x2),big_r(x4,x3) -> big_r(sk7,sk8),big_p(sk1(x4)) {x0 -> sk9, x1 -> sk10, x2 -> sk10, x3 -> sk10, x4 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 174:7:3:[147.2,80.6]:TopTopTop: big_p(sk7),big_p(x0),big_p(x1),big_r(sk9,x0),big_r(x2,x1) -> big_r(sk7,sk8),big_p(sk1(x2))
% 30.72/6.70 === Conflict found: 78:6:4:[37.0,32.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk5(x2)),big_r(sk2(x3),sk1(x3)) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 176:9:3:[168.3,175.2,78.6,43.3,43.1,144.5,174.7]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk9,sk6(x1)),big_r(x1,sk10),big_p(sk9),big_p(sk7),big_p(x2),big_r(sk9,x2) -> big_r(sk7,sk8)
% 30.72/6.70 === Backtracking. Learning clause 177:9:4:[46.2,74.6,76.6,80.6,74.6,137.3,80.6]:TopTopTopTop: big_r(sk9,sk6(x0)),big_r(sk7,sk8),big_p(sk7),big_p(sk9),big_p(x1),big_p(x2),big_r(x0,x1),big_r(x3,x2) -> big_p(sk1(x3))
% 30.72/6.70 === Backtracking. Learning clause 179:9:4:[80.4,178.0,46.4,82.5,80.5,162.3,82.5,137.3]:TopTopTopTop: big_r(sk9,sk2(x0)),big_r(sk7,sk8),big_p(x1),big_p(x2),big_r(x3,x1),big_r(x0,x2),big_p(sk7),big_p(sk9) -> big_r(sk6(x3),sk5(x3))
% 30.72/6.70 === Backtracking. Learning clause 181:14:7:[74.4,180.0,46.4,78.6,177.9,162.3,78.6]:TopTopTopTopTopTopTop: big_r(sk9,sk2(x0)),big_r(sk9,sk6(x1)),big_r(sk7,sk8),big_p(x2),big_p(x3),big_r(x1,x2),big_r(sk7,x3),big_p(sk7),big_p(sk9),big_p(x4),big_p(x5),big_r(x6,x4),big_r(x0,x5) -> big_p(sk5(x6))
% 30.72/6.70 === Backtracking. Learning clause 182:3:0:[46.4,79.6,177.9,162.3,46.5,181.14,179.9,181.14,137.3,179.9,173.8,176.9,172.4,141.3]:: big_p(sk10),big_p(sk7),big_p(sk9) ->
% 30.72/6.70 === Backtracking. Learning clause 183:3:0:[40.3,182.1]:: big_p(sk7),big_p(sk9) -> big_r(sk7,sk8)
% 30.72/6.70 === Backtracking. Learning clause 184:8:4:[44.3,78.6,74.5]:TopTopTopTop: big_p(sk9),big_r(sk7,sk2(x0)),big_p(x1),big_p(x2),big_r(x3,x1),big_r(x0,x2) -> big_p(sk10),big_p(sk5(x3))
% 30.72/6.70 === Backtracking. Learning clause 185:9:3:[44.4,79.5,82.6,44.3]:TopTopTop: big_p(sk5(sk7)),big_p(x0),big_p(x1),big_r(sk7,x0),big_r(x2,x1),big_p(sk1(x2)),big_p(sk9),big_r(sk7,sk2(x2)) -> big_p(sk10)
% 30.72/6.70 === Backtracking. Learning clause 186:2:0:[44.3,80.6,76.6,185.6,184.8,162.3,182.1,137.3,183.3]:: big_p(sk7),big_p(sk9) ->
% 30.72/6.70 === Conflict found: 88:7:2:[42.4,60.3,59.3]:TopTop: big_p(sk7),big_r(sk4(sk9),sk3(x0)) -> big_p(sk8),big_p(sk9),big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1)) {x0 -> sk9, x1 -> sk9}
% 30.72/6.70 === Backtracking. Learning clause 187:3:0:[88.2,61.4,186.2]:: big_p(sk7) -> big_p(sk8),big_r(sk2(sk9),sk1(sk9))
% 30.72/6.70 === Backtracking. Learning clause 188:3:0:[42.4,48.4,47.4,49.4,186.2]:: big_p(sk7) -> big_p(sk8),big_p(sk1(sk9))
% 30.72/6.70 === Backtracking. Learning clause 189:3:0:[42.4,51.3,50.3,52.4,186.2,43.4,187.3,188.3]:: big_p(sk7) -> big_r(sk7,sk8),big_p(sk8)
% 30.72/6.70 === Backtracking. Learning clause 190:3:0:[43.4,60.3,59.3,61.4,186.2]:: big_p(sk7) -> big_r(sk7,sk8),big_r(sk2(sk9),sk1(sk9))
% 30.72/6.70 === Backtracking. Learning clause 192:4:1:[183.1,191.2,43.4,48.4,47.4,49.4]:Top: big_p(sk7) -> big_r(sk7,sk8),big_p(x0),big_p(sk1(x0))
% 30.72/6.70 === Backtracking. Learning clause 193:2:0:[43.4,51.3,50.3,52.4,43.4,192.4,186.2,190.3]:: big_p(sk7) -> big_r(sk7,sk8)
% 30.72/6.70 === Backtracking. Learning clause 194:5:1:[46.2,53.5,60.3,73.5,72.4,59.3,61.4,186.2]:Top: big_p(x0),big_r(sk7,x0),big_p(sk7) -> big_p(sk1(sk9)),big_r(sk2(sk9),sk1(sk9))
% 30.72/6.70 === Backtracking. Learning clause 196:2:0:[193.1,195.0,46.2,53.5,48.4,54.5,55.5,47.4,49.4,186.2,188.2]:: big_p(sk7) -> big_p(sk1(sk9))
% 30.72/6.70 === Backtracking. Learning clause 199:5:2:[193.1,197.0,186.1,198.4,46.2,71.4,73.5,72.4,88.3,60.3,59.3]:TopTop: big_p(sk7),big_r(sk4(sk9),sk3(x0)) -> big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1))
% 30.72/6.70 === Backtracking. Learning clause 201:6:2:[137.1,200.5,42.4,51.4]:TopTop: big_p(x0),big_p(sk7),big_r(sk2(sk9),x0) -> big_p(sk8),big_p(x1),big_r(x1,sk4(x1))
% 30.72/6.70 === Backtracking. Learning clause 204:5:2:[193.1,202.0,186.1,203.4,46.5,65.5,67.5,64.4,51.4,201.4]:TopTop: big_p(x0),big_p(sk7),big_r(sk2(sk9),x0) -> big_p(x1),big_r(x1,sk4(x1))
% 30.72/6.70 === Backtracking. Learning clause 206:7:3:[137.1,205.7,42.1,89.7]:TopTopTop: big_r(x0,sk3(x1)),big_r(sk9,x0),big_p(sk7),big_r(sk2(sk9),sk1(x2)) -> big_p(sk8),big_p(x2),big_p(x1)
% 30.72/6.70 === Backtracking. Learning clause 207:7:4:[46.2,56.4,57.4,58.5]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_r(sk9,x1),big_p(x2),big_r(sk7,x2) -> big_p(x3),big_r(x3,sk2(x3))
% 25.04/6.70 === Backtracking. Learning clause 208:9:6:[46.5,75.6,78.6,74.5,46.2]:TopTopTopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(sk7,x1),big_p(x3),big_r(x4,x3),big_r(x5,sk5(x2)),big_r(sk7,x5),big_r(sk9,x4) ->
% 25.04/6.70 === Backtracking. Learning clause 209:8:5:[46.5,77.6,79.6,76.5,208.8]:TopTopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(sk7,x1),big_p(x3),big_r(x4,x3),big_r(sk6(sk7),sk5(x2)),big_r(sk9,x4) ->
% 25.04/6.70 === Backtracking. Learning clause 210:8:4:[46.5,81.5,82.5,80.5,207.7,209.7]:TopTopTopTop: big_p(x0),big_r(sk2(sk9),x0),big_p(x1),big_r(sk7,x1),big_p(x2),big_r(x3,x2),big_r(sk9,x3) -> big_p(sk9)
% 25.04/6.70 === Conflict found: 50:4:2:[37.0,4.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(x1,sk2(x1)) {x0 -> sk9, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 214:3:1:[193.1,211.0,196.1,212.1,186.1,213.5,50.3,210.5,210.7,206.5,204.5,199.5]:Top: big_p(sk7),big_r(sk4(sk9),sk3(x0)) -> big_p(x0)
% 25.04/6.70 === Conflict found: 52:4:2:[37.0,6.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x1,sk2(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk9, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 216:3:1:[186.1,215.3,52.4,214.2]:Top: big_p(sk7) -> big_p(x0),big_r(x0,sk2(x0))
% 25.04/6.70 === Conflict found: 61:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk9, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 218:5:1:[137.1,217.5,61.3,42.3,214.2]:Top: big_p(sk1(x0)),big_r(sk9,sk2(x0)),big_p(sk7) -> big_p(x0),big_p(sk8)
% 25.04/6.70 === Conflict found: 75:6:4:[37.0,29.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk5(x2)),big_r(x3,sk2(x3)) {x0 -> sk8, x1 -> sk8, x2 -> sk7, x3 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 220:7:3:[42.4,219.0,75.3,193.2,46.5]:TopTopTop: big_p(sk7),big_p(x0),big_p(x1),big_r(x2,x0),big_r(sk2(sk7),x1),big_r(sk9,x2) -> big_p(sk5(sk7))
% 25.04/6.70 === Conflict found: 74:6:4:[37.0,28.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk1(x3)),big_p(sk5(x2)) {x0 -> sk8, x1 -> sk8, x2 -> sk7, x3 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 222:6:2:[42.4,221.0,74.3,193.2,220.3]:TopTop: big_p(sk7),big_p(x0),big_r(x1,x0),big_r(sk2(sk7),sk1(sk7)),big_r(sk9,x1) -> big_p(sk5(sk7))
% 25.04/6.70 === Conflict found: 78:6:4:[37.0,32.2]:TopTopTopTop: big_p(x0),big_p(x1),big_r(x2,x0),big_r(x3,x1) -> big_p(sk5(x2)),big_r(sk2(x3),sk1(x3)) {x0 -> sk8, x1 -> sk8, x2 -> sk7, x3 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 224:6:3:[42.4,223.0,78.3,193.2,222.4,46.2]:TopTopTop: big_p(sk7),big_p(x0),big_r(x1,x0),big_r(x2,sk5(sk7)),big_r(sk7,x2),big_r(sk9,x1) ->
% 25.04/6.70 === Conflict found: 210:8:4:[46.5,81.5,82.5,80.5,207.7,209.7]:TopTopTopTop: big_p(x0),big_r(sk2(sk9),x0),big_p(x1),big_r(sk7,x1),big_p(x2),big_r(x3,x2),big_r(sk9,x3) -> big_p(sk9) {x0 -> sk1(sk9), x1 -> sk8, x2 -> sk1(sk9), x3 -> sk2(sk9)}
% 25.04/6.70 === Backtracking. Learning clause 225:1:0:[210.4,193.2,61.3,214.2,218.5,216.3,186.2,196.2]:: big_p(sk7) ->
% 25.04/6.70 === Backtracking. Learning clause 228:4:1:[113.1,226.1,186.0,227.2,45.1,50.3,51.3,52.4,58.2]:Top: big_p(sk9) -> big_p(x0),big_r(x0,sk2(x0)),big_r(sk6(sk9),sk5(sk9))
% 25.04/6.70 === Backtracking. Learning clause 230:4:1:[141.0,229.2,45.1,50.3,51.3,52.4]:Top: big_p(sk9) -> big_r(sk9,sk10),big_p(x0),big_r(x0,sk2(x0))
% 25.04/6.70 === Backtracking. Learning clause 231:4:0:[46.6,57.4,56.4,50.3,51.3,52.4,228.4,230.2,225.1,114.1,51.1]:: -> big_r(sk7,sk2(sk7)),big_p(sk8),big_r(sk9,sk4(sk9)),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 230:4:1:[141.0,229.2,45.1,50.3,51.3,52.4]:Top: big_p(sk9) -> big_r(sk9,sk10),big_p(x0),big_r(x0,sk2(x0)) {x0 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 232:3:0:[230.3,225.1]:: big_p(sk9) -> big_r(sk9,sk10),big_r(sk7,sk2(sk7))
% 25.04/6.70 === Backtracking. Learning clause 233:5:1:[46.2,50.3,51.3,52.4,225.1,231.3]:Top: big_p(x0),big_r(sk4(sk9),x0) -> big_r(sk7,sk2(sk7)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 62:5:3:[37.0,16.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x1)),big_p(sk3(x2)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 234:5:2:[62.1,114.1]:TopTop: big_r(x0,sk10) -> big_p(x1),big_p(sk1(x0)),big_p(sk3(x1)),big_p(sk8)
% 25.04/6.70 === Conflict found: 66:5:3:[37.0,20.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk3(x2)),big_r(sk2(x1),sk1(x1)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 235:5:2:[66.1,114.1]:TopTop: big_r(x0,sk10) -> big_p(x1),big_p(sk3(x1)),big_r(sk2(x0),sk1(x0)),big_p(sk8)
% 25.04/6.70 === Backtracking. Learning clause 236:7:2:[46.6,77.5,75.5,81.6,65.4,70.5,63.4,225.1,114.1,45.5,51.1,46.6,233.3]:TopTop: big_p(x0),big_r(sk2(sk7),x0),big_p(x1),big_r(sk4(sk9),x1) -> big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Backtracking. Learning clause 238:6:1:[114.0,237.0,46.6,79.5,78.5,82.6,65.4,70.5,235.3,225.1,45.5,51.1,231.1]:Top: big_p(x0),big_r(sk2(sk7),x0) -> big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk4(sk9)),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 50:4:2:[37.0,4.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(x1,sk2(x1)) {x0 -> sk9, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 239:12:4:[50.3,236.3,45.2]:TopTopTopTop: big_p(x0),big_r(sk2(sk7),x0),big_r(sk4(sk9),sk3(sk9)),big_p(x1),big_r(x2,x1),big_r(sk7,x2) -> big_p(x3),big_r(x3,sk2(x3)),big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Backtracking. Learning clause 241:8:2:[187.0,240.6,46.6,77.5,75.5,228.4,114.1,235.2,236.3,239.12,51.3,52.4,50.3]:TopTop: big_p(x0),big_r(sk2(sk7),x0),big_r(sk4(sk9),sk3(sk9)) -> big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9)),big_p(x1),big_r(x1,sk2(x1))
% 25.04/6.70 === Conflict found: 232:3:0:[230.3,225.1]:: big_p(sk9) -> big_r(sk9,sk10),big_r(sk7,sk2(sk7)) {}
% 25.04/6.70 === Backtracking. Learning clause 242:4:1:[232.3,45.4]:Top: big_p(x0),big_p(sk9),big_r(sk2(sk7),x0) -> big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 63:5:3:[37.0,17.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk3(x2)),big_r(x1,sk2(x1)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 243:4:1:[63.3,225.1,114.1]:Top: big_r(x0,sk10) -> big_p(sk3(sk7)),big_r(x0,sk2(x0)),big_p(sk8)
% 25.04/6.70 === Conflict found: 241:8:2:[187.0,240.6,46.6,77.5,75.5,228.4,114.1,235.2,236.3,239.12,51.3,52.4,50.3]:TopTop: big_p(x0),big_r(sk2(sk7),x0),big_r(sk4(sk9),sk3(sk9)) -> big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9)),big_p(x1),big_r(x1,sk2(x1)) {x0 -> sk1(sk7), x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 244:7:1:[241.7,225.1]:Top: big_p(x0),big_r(sk2(sk7),x0),big_r(sk4(sk9),sk3(sk9)) -> big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9)),big_r(sk7,sk2(sk7))
% 25.04/6.70 === Backtracking. Learning clause 245:10:3:[45.2,241.7]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_p(x2),big_r(sk2(sk7),x2),big_r(sk4(sk9),sk3(sk9)) -> big_r(sk9,sk10),big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Backtracking. Learning clause 246:6:1:[46.6,77.5,75.5,81.6,67.4,69.5,114.1,225.1,243.2,245.7,244.7]:Top: big_p(x0),big_r(sk2(sk7),x0),big_r(sk4(sk9),sk3(sk9)) -> big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 50:4:2:[37.0,4.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(x1,sk2(x1)) {x0 -> sk9, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 247:5:0:[50.3,233.1,232.1,225.1]:: big_r(sk4(sk9),sk3(sk9)) -> big_p(sk8),big_r(sk9,sk2(sk9)),big_r(sk9,sk10),big_r(sk7,sk2(sk7))
% 25.04/6.70 === Conflict found: 49:4:2:[37.0,3.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 248:8:2:[49.3,246.1]:TopTop: big_r(sk2(sk7),sk1(x0)),big_r(sk4(sk9),sk3(sk9)) -> big_p(x1),big_p(x0),big_r(sk4(x1),sk3(x1)),big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 47:4:2:[37.0,1.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_p(sk3(x0)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 249:8:2:[47.3,246.1]:TopTop: big_r(sk2(sk7),sk1(x0)),big_r(sk4(sk9),sk3(sk9)) -> big_p(x1),big_p(x0),big_p(sk3(x1)),big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 48:4:2:[37.0,2.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_r(x0,sk4(x0)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 251:10:2:[39.0,250.5,48.4,45.4,246.1]:TopTop: big_p(x0),big_p(sk9),big_r(sk4(sk7),x0),big_r(sk2(sk7),sk1(x1)),big_r(sk4(sk9),sk3(sk9)) -> big_p(x1),big_r(sk9,sk10),big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Backtracking. Learning clause 252:6:0:[46.6,60.3,59.3,60.3,251.2,248.5,249.5,225.1]:: big_r(sk2(sk7),sk1(sk7)),big_r(sk4(sk9),sk3(sk9)) -> big_r(sk9,sk10),big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Backtracking. Learning clause 255:11:3:[230.1,253.2,137.0,254.10,46.6,54.5,53.5,228.4,114.1,246.1,51.3]:TopTopTop: big_p(x0),big_r(sk4(sk7),x0),big_p(sk9),big_r(sk2(sk7),sk1(x1)),big_r(sk4(sk9),sk3(sk9)) -> big_p(x1),big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9)),big_p(x2),big_r(x2,sk2(x2))
% 25.04/6.70 === Backtracking. Learning clause 256:5:0:[46.6,54.5,53.5,55.5,114.1,48.4,246.1,248.5,225.1,243.2,252.3]:: big_r(sk2(sk7),sk1(sk7)),big_r(sk4(sk9),sk3(sk9)) -> big_r(sk2(sk9),sk1(sk9)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Backtracking. Learning clause 257:7:3:[45.1,47.3,50.2]:TopTopTop: big_r(x0,sk1(x1)),big_r(sk7,x0) -> big_r(sk9,sk10),big_p(x1),big_p(x2),big_p(sk3(x2)),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Backtracking. Learning clause 259:6:2:[141.0,258.4,45.3,49.4,48.4,45.1]:TopTop: big_p(sk3(sk7)),big_p(sk9),big_r(x0,sk1(x1)),big_r(sk7,x0) -> big_p(x1),big_r(sk9,sk10)
% 25.04/6.70 === Backtracking. Learning clause 261:6:1:[225.0,260.3,46.6,51.3,50.3,52.4,51.3,259.2,257.6,247.5]:Top: big_r(sk2(sk7),sk1(x0)),big_r(sk4(sk9),sk3(sk9)) -> big_p(x0),big_p(sk8),big_r(sk9,sk2(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 69:5:3:[37.0,23.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x1,sk2(x1)),big_r(sk4(x2),sk3(x2)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 262:5:2:[69.1,114.1]:TopTop: big_r(x0,sk10) -> big_p(x1),big_r(x0,sk2(x0)),big_r(sk4(x1),sk3(x1)),big_p(sk8)
% 25.04/6.70 === Backtracking. Learning clause 263:7:3:[46.6,77.5,75.5,81.6,114.1]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_r(sk9,sk10),big_r(x2,sk10) -> big_r(x2,sk2(x2)),big_p(sk8)
% 25.04/6.70 === Conflict found: 65:5:3:[37.0,19.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,sk4(x2)),big_r(x1,sk2(x1)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 264:4:0:[65.1,114.1,263.3,243.2,262.4,261.6,225.1]:: big_r(sk2(sk7),sk1(sk7)),big_r(sk4(sk9),sk3(sk9)) -> big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 47:4:2:[37.0,1.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_p(sk3(x0)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 265:4:0:[47.1,225.1,242.1]:: big_p(sk9),big_r(sk2(sk7),sk1(sk7)) -> big_p(sk3(sk7)),big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 50:4:2:[37.0,4.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(x1,sk2(x1)) {x0 -> sk7, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 266:4:0:[50.1,225.1,265.1,243.1]:: big_r(sk2(sk7),sk1(sk7)) -> big_p(sk3(sk7)),big_r(sk9,sk2(sk9)),big_p(sk8)
% 25.04/6.70 === Conflict found: 49:4:2:[37.0,3.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 267:7:2:[49.3,242.1,45.3]:TopTop: big_r(sk2(sk7),sk1(x0)),big_p(sk3(x1)),big_p(sk9),big_r(sk7,sk4(x1)) -> big_p(x1),big_p(x0),big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 262:5:2:[69.1,114.1]:TopTop: big_r(x0,sk10) -> big_p(x1),big_r(x0,sk2(x0)),big_r(sk4(x1),sk3(x1)),big_p(sk8) {x0 -> sk9, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 268:8:2:[262.4,263.2,267.7]:TopTop: big_r(sk2(sk7),sk1(x0)),big_p(sk3(x1)),big_p(sk9),big_r(sk7,sk4(x1)) -> big_r(sk9,sk2(sk9)),big_p(sk8),big_p(x1),big_p(x0)
% 25.04/6.70 === Conflict found: 242:4:1:[232.3,45.4]:Top: big_p(x0),big_p(sk9),big_r(sk2(sk7),x0) -> big_r(sk9,sk10) {x0 -> sk1(sk7)}
% 25.04/6.70 === Backtracking. Learning clause 269:6:2:[242.1,48.3]:TopTop: big_p(sk9),big_r(sk2(sk7),sk1(x0)) -> big_r(sk9,sk10),big_p(x1),big_p(x0),big_r(x1,sk4(x1))
% 25.04/6.70 === Conflict found: 65:5:3:[37.0,19.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,sk4(x2)),big_r(x1,sk2(x1)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 271:4:0:[266.1,270.1,65.1,114.1,269.3,268.4,225.1]:: big_r(sk2(sk7),sk1(sk7)),big_p(sk9) -> big_r(sk9,sk2(sk9)),big_p(sk8)
% 25.04/6.70 === Conflict found: 52:4:2:[37.0,6.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x1,sk2(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk9, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 273:3:0:[271.1,272.1,52.4,264.2]:: big_r(sk2(sk7),sk1(sk7)) -> big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 61:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 275:4:1:[225.0,274.1,61.3,273.1]:Top: -> big_p(x0),big_r(sk4(x0),sk3(x0)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 275:4:1:[225.0,274.1,61.3,273.1]:Top: -> big_p(x0),big_r(sk4(x0),sk3(x0)),big_p(sk8),big_r(sk9,sk2(sk9)) {x0 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 276:3:0:[275.1,225.1]:: -> big_r(sk4(sk7),sk3(sk7)),big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 59:4:2:[37.0,13.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 278:7:2:[39.0,277.4,59.4,273.1,45.1]:TopTop: big_p(sk9),big_r(x0,sk3(x1)),big_r(sk7,x0) -> big_p(x1),big_p(sk8),big_r(sk9,sk2(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 233:5:1:[46.2,50.3,51.3,52.4,225.1,231.3]:Top: big_p(x0),big_r(sk4(sk9),x0) -> big_r(sk7,sk2(sk7)),big_p(sk8),big_r(sk9,sk2(sk9)) {x0 -> sk3(sk9)}
% 25.04/6.70 === Backtracking. Learning clause 279:4:0:[233.2,52.4,50.3]:: -> big_r(sk7,sk2(sk7)),big_p(sk8),big_r(sk9,sk2(sk9)),big_p(sk9)
% 25.04/6.70 === Backtracking. Learning clause 280:6:2:[46.6,51.3,52.4,50.3,50.3,278.1]:TopTop: big_r(x0,sk3(x1)),big_r(sk7,x0) -> big_p(x1),big_p(sk8),big_r(sk9,sk2(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 60:4:2:[37.0,14.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x0,sk4(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 282:3:0:[276.0,281.0,60.4,273.1,280.2,225.1]:: -> big_p(sk8),big_r(sk9,sk2(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 263:7:3:[46.6,77.5,75.5,81.6,114.1]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_r(sk9,sk10),big_r(x2,sk10) -> big_r(x2,sk2(x2)),big_p(sk8) {x0 -> sk3(sk7), x1 -> sk4(sk7), x2 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 283:6:2:[263.1,243.2]:TopTop: big_r(x0,sk3(sk7)),big_r(sk7,x0),big_r(sk9,sk10),big_r(x1,sk10) -> big_r(x1,sk2(x1)),big_p(sk8)
% 25.04/6.70 === Conflict found: 65:5:3:[37.0,19.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,sk4(x2)),big_r(x1,sk2(x1)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 284:2:0:[65.1,114.1,225.1,283.2,276.1,282.3]:: -> big_p(sk8),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 242:4:1:[232.3,45.4]:Top: big_p(x0),big_p(sk9),big_r(sk2(sk7),x0) -> big_r(sk9,sk10) {x0 -> sk1(sk7)}
% 25.04/6.70 === Backtracking. Learning clause 286:4:1:[141.0,285.3,242.3,61.3,49.3]:Top: big_p(sk9) -> big_r(sk9,sk10),big_p(x0),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Conflict found: 94:10:4:[46.2,47.3,52.3,50.4,47.3]:TopTopTopTop: big_r(sk2(sk9),sk1(x0)),big_r(sk2(sk7),sk1(x1)) -> big_p(x1),big_p(x2),big_p(sk7),big_r(sk4(x2),sk3(x2)),big_p(sk9),big_p(x3),big_p(x0),big_p(sk3(x3)) {x0 -> sk9, x1 -> sk7, x2 -> sk7, x3 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 288:5:2:[225.0,287.4,94.1,61.3,61.3]:TopTop: -> big_p(x0),big_p(sk3(x0)),big_p(sk9),big_p(x1),big_r(sk4(x1),sk3(x1))
% 25.04/6.70 === Backtracking. Learning clause 290:4:1:[225.0,289.1,46.1,49.3,284.2,61.3,52.3,61.3,49.3,286.1]:Top: -> big_p(sk8),big_r(sk9,sk10),big_p(x0),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Conflict found: 290:4:1:[225.0,289.1,46.1,49.3,284.2,61.3,52.3,61.3,49.3,286.1]:Top: -> big_p(sk8),big_r(sk9,sk10),big_p(x0),big_r(sk4(x0),sk3(x0)) {x0 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 291:3:0:[290.3,225.1]:: -> big_p(sk8),big_r(sk9,sk10),big_r(sk4(sk7),sk3(sk7))
% 25.04/6.70 === Conflict found: 59:4:2:[37.0,13.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 293:4:1:[141.0,292.3,59.4,265.2,45.1]:Top: big_p(sk9),big_r(x0,sk3(sk7)),big_r(sk7,x0) -> big_r(sk9,sk10)
% 25.04/6.70 === Backtracking. Learning clause 295:4:1:[225.0,294.3,46.1,47.3,284.2,59.4,50.4,47.3,59.4]:Top: -> big_p(sk8),big_p(sk9),big_p(x0),big_p(sk3(x0))
% 25.04/6.70 === Conflict found: 295:4:1:[225.0,294.3,46.1,47.3,284.2,59.4,50.4,47.3,59.4]:Top: -> big_p(sk8),big_p(sk9),big_p(x0),big_p(sk3(x0)) {x0 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 296:3:0:[295.3,225.1]:: -> big_p(sk8),big_p(sk9),big_p(sk3(sk7))
% 25.04/6.70 === Backtracking. Learning clause 298:7:3:[45.1,297.7,46.6,51.3,290.4,295.4]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1) -> big_p(x2),big_r(x2,sk2(x2)),big_r(sk9,sk10),big_p(sk8)
% 25.04/6.70 === Backtracking. Learning clause 300:5:2:[45.1,299.5,46.1,48.3,60.4,46.6,284.2,290.4,295.4]:TopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1) -> big_r(sk9,sk10),big_p(sk8)
% 25.04/6.70 === Conflict found: 296:3:0:[295.3,225.1]:: -> big_p(sk8),big_p(sk9),big_p(sk3(sk7)) {}
% 25.04/6.70 === Backtracking. Learning clause 301:3:0:[296.2,293.1,300.1,291.3]:: big_r(sk7,sk4(sk7)) -> big_p(sk8),big_r(sk9,sk10)
% 25.04/6.70 === Backtracking. Learning clause 302:3:0:[46.1,234.3,284.2,235.4,50.4,59.4,47.3,225.1,301.3]:: big_r(sk7,sk4(sk7)) -> big_p(sk3(sk7)),big_p(sk8)
% 25.04/6.70 === Conflict found: 70:5:3:[37.0,24.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(sk2(x1),sk1(x1)),big_r(sk4(x2),sk3(x2)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 303:5:2:[70.1,114.1]:TopTop: big_r(x0,sk10) -> big_p(x1),big_r(sk2(x0),sk1(x0)),big_r(sk4(x1),sk3(x1)),big_p(sk8)
% 25.04/6.70 === Conflict found: 68:5:3:[37.0,22.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x1)),big_r(sk4(x2),sk3(x2)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 307:3:1:[49.2,304.0,290.1,305.1,225.0,306.4,68.4,46.1,114.1,284.2,303.3,52.3,61.3]:Top: -> big_p(sk8),big_p(x0),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Backtracking. Learning clause 308:2:0:[46.1,234.3,284.2,47.3,235.4,265.4,50.4,59.4,225.1,296.2]:: -> big_p(sk8),big_p(sk3(sk7))
% 25.04/6.70 === Backtracking. Learning clause 311:8:3:[230.1,309.2,137.0,310.7,46.6,79.5,78.5,228.4,114.1,51.3]:TopTopTop: big_p(x0),big_r(sk4(sk7),x0),big_r(x1,sk10),big_p(sk9) -> big_r(sk2(x1),sk1(x1)),big_p(sk8),big_p(x2),big_r(x2,sk2(x2))
% 25.04/6.70 === Backtracking. Learning clause 313:5:1:[137.0,312.4,46.6,57.4,56.4,228.4,114.1,51.3,232.2]:Top: big_p(x0),big_r(sk4(sk7),x0),big_p(sk9) -> big_p(sk8),big_r(sk7,sk2(sk7))
% 25.04/6.70 === Conflict found: 298:7:3:[45.1,297.7,46.6,51.3,290.4,295.4]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1) -> big_p(x2),big_r(x2,sk2(x2)),big_r(sk9,sk10),big_p(sk8) {x0 -> sk3(sk7), x1 -> sk4(sk7), x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 315:6:2:[216.0,314.4,298.3,51.3]:TopTop: big_p(x0),big_r(sk4(sk7),x0) -> big_r(sk9,sk10),big_p(sk8),big_p(x1),big_r(x1,sk2(x1))
% 25.04/6.70 === Backtracking. Learning clause 317:6:3:[300.3,316.3,46.6,79.5,78.5,82.6,114.1]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_r(x2,sk10) -> big_r(sk2(x2),sk1(x2)),big_p(sk8)
% 25.04/6.70 === Backtracking. Learning clause 319:5:2:[216.0,318.2,46.6,57.4,56.4,58.5,114.1,51.3,315.3]:TopTop: big_p(x0),big_r(sk4(sk7),x0) -> big_p(sk8),big_p(x1),big_r(x1,sk2(x1))
% 25.04/6.70 === Conflict found: 259:6:2:[141.0,258.4,45.3,49.4,48.4,45.1]:TopTop: big_p(sk3(sk7)),big_p(sk9),big_r(x0,sk1(x1)),big_r(sk7,x0) -> big_p(x1),big_r(sk9,sk10) {x0 -> sk2(sk7), x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 320:7:2:[259.3,60.4,60.2]:TopTop: big_p(sk3(sk7)),big_r(sk7,sk2(x0)) -> big_r(sk9,sk10),big_p(x0),big_p(x1),big_r(x1,sk4(x1)),big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Conflict found: 300:5:2:[45.1,299.5,46.1,48.3,60.4,46.6,284.2,290.4,295.4]:TopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1) -> big_r(sk9,sk10),big_p(sk8) {x0 -> sk1(sk7), x1 -> sk2(sk7)}
% 25.04/6.70 === Backtracking. Learning clause 322:4:1:[225.0,321.2,300.1,48.3,60.4,319.5,300.3]:Top: big_p(x0),big_r(sk4(sk7),x0) -> big_r(sk9,sk10),big_p(sk8)
% 25.04/6.70 === Backtracking. Learning clause 323:9:5:[46.6,76.6,74.6,80.6,46.1,284.2]:TopTopTopTopTop: big_p(x0),big_p(x1),big_r(sk9,x0),big_r(x2,x1),big_p(x3),big_r(sk2(sk9),sk1(x2)),big_r(x4,x3),big_r(sk7,x4) -> big_p(sk8)
% 25.04/6.70 === Conflict found: 323:9:5:[46.6,76.6,74.6,80.6,46.1,284.2]:TopTopTopTopTop: big_p(x0),big_p(x1),big_r(sk9,x0),big_r(x2,x1),big_p(x3),big_r(sk2(sk9),sk1(x2)),big_r(x4,x3),big_r(sk7,x4) -> big_p(sk8) {x0 -> sk10, x1 -> sk10, x2 -> sk9, x3 -> sk3(sk7), x4 -> sk4(sk7)}
% 25.04/6.70 === Backtracking. Learning clause 325:4:2:[300.3,324.3,323.1,114.1,317.5]:TopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1) -> big_p(sk8)
% 25.04/6.70 === Conflict found: 325:4:2:[300.3,324.3,323.1,114.1,317.5]:TopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1) -> big_p(sk8) {x0 -> sk1(sk7), x1 -> sk2(sk7)}
% 25.04/6.70 === Backtracking. Learning clause 326:1:0:[325.3,319.5,48.3,60.4,325.3,307.3,225.1,308.2]:: -> big_p(sk8)
% 25.04/6.70 === Conflict found: 50:4:2:[37.0,4.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(x1,sk2(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 327:2:0:[50.1,225.1]:: -> big_p(sk3(sk7)),big_r(sk7,sk2(sk7))
% 25.04/6.70 === Backtracking. Learning clause 328:5:1:[46.6,51.3,52.4,50.3,52.4,242.2,225.1,327.1]:Top: big_r(sk7,sk4(sk7)),big_p(x0),big_r(sk2(sk7),x0) -> big_r(sk9,sk10),big_r(sk7,sk2(sk7))
% 25.04/6.70 === Conflict found: 59:4:2:[37.0,13.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 329:6:2:[59.2,242.2]:TopTop: big_p(x0),big_r(sk2(sk7),x0) -> big_p(x1),big_p(sk3(x1)),big_r(sk2(sk9),sk1(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Backtracking. Learning clause 330:5:1:[46.6,320.6,61.4,59.3,61.4,242.2,329.4,225.1,328.5]:Top: big_r(sk7,sk4(sk7)),big_p(x0),big_r(sk2(sk7),x0) -> big_r(sk2(sk9),sk1(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 59:4:2:[37.0,13.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 331:4:0:[59.1,225.1,265.1]:: big_r(sk2(sk7),sk1(sk7)) -> big_r(sk2(sk9),sk1(sk9)),big_p(sk3(sk7)),big_r(sk9,sk10)
% 25.04/6.70 === Backtracking. Learning clause 332:4:0:[46.6,60.3,61.4,59.3,61.4,267.3,225.1,331.3]:: big_r(sk7,sk4(sk7)),big_r(sk2(sk7),sk1(sk7)) -> big_r(sk2(sk9),sk1(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Backtracking. Learning clause 333:4:0:[44.5,66.1,47.3,332.4,327.2,59.2,225.1]:: big_r(sk7,sk4(sk7)),big_r(sk2(sk7),sk1(sk7)) -> big_p(sk3(sk7)),big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Backtracking. Learning clause 337:5:2:[50.2,334.0,230.1,335.2,186.0,336.4,46.6,57.4,56.4,228.4,113.2,52.4]:TopTop: big_r(sk7,sk4(x0)),big_p(sk9) -> big_p(x0),big_p(x1),big_r(x1,sk2(x1))
% 25.04/6.70 === Backtracking. Learning clause 338:8:4:[44.5,70.1,49.3]:TopTopTopTop: big_p(sk9),big_r(x0,sk1(x1)),big_r(sk7,x0),big_r(x2,sk10) -> big_r(sk2(x2),sk1(x2)),big_p(x3),big_p(x1),big_r(sk4(x3),sk3(x3))
% 25.04/6.70 === Backtracking. Learning clause 340:7:1:[186.0,339.7,46.6,79.5,78.5,82.6,44.5,338.8,332.4,337.5]:Top: big_p(sk3(x0)),big_r(sk7,sk4(x0)),big_r(sk7,sk4(sk7)),big_r(sk2(sk7),sk1(sk7)),big_p(sk9) -> big_p(x0),big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Backtracking. Learning clause 343:7:3:[51.2,341.3,216.0,342.6,46.6,79.5,78.5,82.6,332.4,115.1]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_r(sk2(sk7),sk1(sk7)) -> big_r(sk2(sk9),sk1(sk9)),big_p(x2),big_r(x2,sk2(x2))
% 25.04/6.70 === Backtracking. Learning clause 344:7:4:[46.6,72.4,71.4,73.5]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_p(x2),big_r(sk9,x2) -> big_p(x3),big_r(sk2(x3),sk1(x3))
% 25.04/6.70 === Conflict found: 344:7:4:[46.6,72.4,71.4,73.5]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_p(x2),big_r(sk9,x2) -> big_p(x3),big_r(sk2(x3),sk1(x3)) {x0 -> sk3(sk7), x1 -> sk4(sk7), x2 -> sk10, x3 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 345:9:3:[344.5,332.4]:TopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_p(sk10),big_r(sk7,sk4(sk7)),big_r(sk2(sk7),sk1(sk7)) -> big_p(x2),big_r(sk2(x2),sk1(x2)),big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Backtracking. Learning clause 346:3:0:[46.6,60.3,61.4,59.3,61.4,340.5,225.1,333.3]:: big_r(sk7,sk4(sk7)),big_r(sk2(sk7),sk1(sk7)) -> big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Conflict found: 286:4:1:[141.0,285.3,242.3,61.3,49.3]:Top: big_p(sk9) -> big_r(sk9,sk10),big_p(x0),big_r(sk4(x0),sk3(x0)) {x0 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 347:5:0:[286.4,293.2,66.2,225.1]:: big_p(sk9),big_r(sk7,sk4(sk7)),big_p(sk10) -> big_p(sk3(sk7)),big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Conflict found: 286:4:1:[141.0,285.3,242.3,61.3,49.3]:Top: big_p(sk9) -> big_r(sk9,sk10),big_p(x0),big_r(sk4(x0),sk3(x0)) {x0 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 349:4:1:[61.1,348.0,286.2,70.2]:Top: big_p(sk10) -> big_p(x0),big_r(sk2(sk9),sk1(sk9)),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Backtracking. Learning clause 350:4:0:[46.6,79.5,78.5,82.6,45.5,349.4,225.1,347.4]:: big_p(sk9),big_r(sk7,sk4(sk7)),big_p(sk10) -> big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Conflict found: 61:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk7, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 351:4:0:[61.1,225.1,350.1]:: big_r(sk7,sk4(sk7)),big_p(sk10) -> big_r(sk4(sk7),sk3(sk7)),big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Backtracking. Learning clause 352:3:0:[46.6,60.3,349.4,59.3,59.3,225.1,350.1,351.3]:: big_r(sk7,sk4(sk7)),big_p(sk10) -> big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Conflict found: 61:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_p(x1),big_r(sk2(x1),sk1(x1)),big_r(sk4(x0),sk3(x0)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 353:3:0:[61.3,346.2,225.1]:: big_r(sk7,sk4(sk7)) -> big_r(sk4(sk7),sk3(sk7)),big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Conflict found: 59:4:2:[37.0,13.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 355:4:1:[225.0,354.2,59.4,346.2]:Top: big_r(sk7,sk4(sk7)) -> big_p(x0),big_p(sk3(x0)),big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Backtracking. Learning clause 356:6:2:[44.5,352.2]:TopTop: big_p(x0),big_p(sk9),big_r(x1,x0),big_r(sk7,x1),big_r(sk7,sk4(sk7)) -> big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Backtracking. Learning clause 357:2:0:[46.6,60.3,61.4,59.3,356.2,355.3,225.1,353.2]:: big_r(sk7,sk4(sk7)) -> big_r(sk2(sk9),sk1(sk9))
% 25.04/6.70 === Backtracking. Learning clause 359:7:3:[225.0,358.6,46.1,62.4,63.5,357.2,49.3,61.3,52.3]:TopTopTop: big_p(x0),big_r(sk9,x0),big_r(sk7,sk4(sk7)) -> big_p(x1),big_p(sk3(x1)),big_p(x2),big_r(sk4(x2),sk3(x2))
% 25.04/6.70 === Conflict found: 359:7:3:[225.0,358.6,46.1,62.4,63.5,357.2,49.3,61.3,52.3]:TopTopTop: big_p(x0),big_r(sk9,x0),big_r(sk7,sk4(sk7)) -> big_p(x1),big_p(sk3(x1)),big_p(x2),big_r(sk4(x2),sk3(x2)) {x0 -> sk10, x1 -> sk7, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 361:6:2:[288.2,360.2,359.2,286.2]:TopTop: big_p(sk10),big_r(sk7,sk4(sk7)) -> big_p(x0),big_p(sk3(x0)),big_p(x1),big_r(sk4(x1),sk3(x1))
% 25.04/6.70 === Backtracking. Learning clause 364:5:2:[288.2,362.0,225.0,363.2,44.1,49.3,61.3,52.3,361.1]:TopTop: big_r(sk7,sk4(sk7)) -> big_p(x0),big_p(sk3(x0)),big_p(x1),big_r(sk4(x1),sk3(x1))
% 25.04/6.70 === Backtracking. Learning clause 366:5:1:[182.1,365.3,46.1,68.4,69.4,357.2,49.3,61.3,52.3,286.2]:Top: big_p(sk10),big_r(sk7,sk4(sk7)),big_p(sk9) -> big_p(x0),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Backtracking. Learning clause 368:4:1:[225.0,367.2,46.1,49.3,52.3,357.2,49.3,61.3,52.3,366.3]:Top: big_p(sk10),big_r(sk7,sk4(sk7)) -> big_p(x0),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Backtracking. Learning clause 370:4:1:[186.0,369.3,44.1,49.3,61.3,52.3]:Top: big_p(sk9) -> big_p(sk10),big_p(x0),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Backtracking. Learning clause 372:3:1:[225.0,371.1,46.1,49.3,115.4,357.2,49.3,61.3,52.3,370.1,368.1]:Top: big_r(sk7,sk4(sk7)) -> big_p(x0),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Backtracking. Learning clause 373:8:4:[46.1,62.4,63.5,357.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_p(x2),big_r(sk9,x2),big_r(sk7,sk4(sk7)) -> big_p(x3),big_p(sk3(x3))
% 25.04/6.70 === Backtracking. Learning clause 374:8:5:[46.6,77.5,75.5,81.6]:TopTopTopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_p(x2),big_p(x3),big_r(sk9,x2),big_r(x4,x3) -> big_r(x4,sk2(x4))
% 25.04/6.70 === Backtracking. Learning clause 376:10:5:[44.4,375.5,46.6,76.6,74.6,80.6,46.1,374.8,357.2,373.8,293.4]:TopTopTopTopTop: big_r(x0,sk3(x1)),big_r(sk7,x0),big_p(x2),big_r(x3,x2),big_r(sk7,x3),big_r(sk7,sk4(sk7)),big_p(sk9),big_r(x4,sk3(sk7)),big_r(sk7,x4) -> big_p(x1)
% 25.04/6.70 === Conflict found: 376:10:5:[44.4,375.5,46.6,76.6,74.6,80.6,46.1,374.8,357.2,373.8,293.4]:TopTopTopTopTop: big_r(x0,sk3(x1)),big_r(sk7,x0),big_p(x2),big_r(x3,x2),big_r(sk7,x3),big_r(sk7,sk4(sk7)),big_p(sk9),big_r(x4,sk3(sk7)),big_r(sk7,x4) -> big_p(x1) {x0 -> sk4(sk7), x1 -> sk7, x2 -> sk1(sk7), x3 -> sk2(sk7), x4 -> sk4(sk7)}
% 25.04/6.70 === Backtracking. Learning clause 378:2:0:[186.0,377.2,376.4,59.4,47.3,376.3,372.3,337.5]:: big_r(sk7,sk4(sk7)),big_p(sk9) ->
% 25.04/6.70 === Conflict found: 368:4:1:[225.0,367.2,46.1,49.3,52.3,357.2,49.3,61.3,52.3,366.3]:Top: big_p(sk10),big_r(sk7,sk4(sk7)) -> big_p(x0),big_r(sk4(x0),sk3(x0)) {x0 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 379:3:0:[368.3,225.1]:: big_p(sk10),big_r(sk7,sk4(sk7)) -> big_r(sk4(sk7),sk3(sk7))
% 25.04/6.70 === Conflict found: 94:10:4:[46.2,47.3,52.3,50.4,47.3]:TopTopTopTop: big_r(sk2(sk9),sk1(x0)),big_r(sk2(sk7),sk1(x1)) -> big_p(x1),big_p(x2),big_p(sk7),big_r(sk4(x2),sk3(x2)),big_p(sk9),big_p(x3),big_p(x0),big_p(sk3(x3)) {x0 -> sk9, x1 -> sk7, x2 -> sk7, x3 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 381:4:0:[378.1,380.3,94.3,225.1,357.2]:: big_r(sk2(sk7),sk1(sk7)),big_r(sk7,sk4(sk7)) -> big_r(sk4(sk7),sk3(sk7)),big_p(sk3(sk7))
% 25.04/6.70 === Backtracking. Learning clause 383:5:2:[378.1,382.4,46.1,47.3,50.4,225.1,357.2]:TopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_r(sk7,sk4(sk7)) -> big_p(sk3(sk7))
% 25.04/6.70 === Conflict found: 59:4:2:[37.0,13.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk3(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 385:3:0:[327.1,384.1,59.1,225.1,383.2]:: big_p(sk1(sk7)),big_r(sk7,sk4(sk7)) -> big_p(sk3(sk7))
% 25.04/6.70 === Conflict found: 47:4:2:[37.0,1.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_p(sk3(x0)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 386:2:0:[47.3,385.1,225.1]:: big_r(sk7,sk4(sk7)) -> big_p(sk3(sk7))
% 25.04/6.70 === Backtracking. Learning clause 387:10:4:[46.6,57.4,56.4,58.5,328.4]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_p(sk10),big_r(sk7,sk4(sk7)),big_p(x2),big_r(sk2(sk7),x2) -> big_p(x3),big_r(x3,sk2(x3)),big_r(sk7,sk2(sk7))
% 25.04/6.70 === Backtracking. Learning clause 389:9:4:[45.1,388.8,46.6,51.3,372.3,257.6]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_r(sk7,sk4(sk7)),big_r(x2,sk1(x3)),big_r(sk7,x2) -> big_r(sk9,sk10),big_p(x3),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Backtracking. Learning clause 391:10:5:[45.1,390.7,46.6,48.4,372.3,47.4,46.1,389.9]:TopTopTopTopTop: big_r(sk2(sk9),sk1(x0)),big_p(x1),big_r(x2,x1),big_r(sk7,x2),big_r(sk7,sk4(sk7)),big_r(x3,sk1(x4)),big_r(sk7,x3) -> big_p(x0),big_r(sk9,sk10),big_p(x4)
% 25.04/6.70 === Backtracking. Learning clause 393:11:5:[225.0,392.11,46.6,54.5,53.5,55.5,46.1,374.8,391.9,387.9]:TopTopTopTopTop: big_r(sk2(sk9),sk1(x0)),big_r(sk2(sk7),sk1(x1)),big_p(x2),big_r(x3,x2),big_r(sk7,x3),big_p(sk10),big_r(sk7,sk4(sk7)),big_p(x4),big_r(sk2(sk7),x4) -> big_p(x0),big_p(x1)
% 25.04/6.70 === Conflict found: 115:4:1:[46.3,52.4,51.3,50.3,50.3,51.3,52.4,113.1]:Top: -> big_p(sk10),big_p(sk7),big_p(x0),big_r(x0,sk2(x0)) {x0 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 396:11:6:[51.2,394.5,216.0,395.8,115.1,393.6]:TopTopTopTopTopTop: big_r(sk2(sk9),sk1(x0)),big_r(sk2(sk7),sk1(x1)),big_p(x2),big_r(x3,x2),big_r(sk7,x3),big_p(x4),big_r(sk2(sk7),x4) -> big_p(x5),big_r(x5,sk2(x5)),big_p(x0),big_p(x1)
% 25.04/6.70 === Backtracking. Learning clause 398:8:3:[378.1,397.6,46.6,48.4,372.3,47.4,46.1,396.9,357.2,372.3]:TopTopTop: big_r(sk2(sk7),sk1(x0)),big_p(sk3(x1)),big_r(sk7,sk4(x1)),big_p(x2),big_r(sk2(sk7),x2),big_r(sk7,sk4(sk7)) -> big_p(x0),big_p(x1)
% 25.04/6.70 === Backtracking. Learning clause 401:5:2:[50.2,399.0,337.1,400.3,46.6,51.3,372.3,50.3,372.3]:TopTop: big_r(sk7,sk4(x0)),big_r(sk7,sk4(sk7)) -> big_p(x1),big_r(x1,sk2(x1)),big_p(x0)
% 25.04/6.70 === Conflict found: 115:4:1:[46.3,52.4,51.3,50.3,50.3,51.3,52.4,113.1]:Top: -> big_p(sk10),big_p(sk7),big_p(x0),big_r(x0,sk2(x0)) {x0 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 403:7:3:[225.0,402.5,115.3,378.2,374.4,389.7,386.2]:TopTopTop: big_r(x0,sk3(sk7)),big_r(sk7,x0),big_r(x1,sk1(x2)),big_r(sk7,x1),big_r(sk7,sk4(sk7)) -> big_p(x2),big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 401:5:2:[50.2,399.0,337.1,400.3,46.6,51.3,372.3,50.3,372.3]:TopTop: big_r(sk7,sk4(x0)),big_r(sk7,sk4(sk7)) -> big_p(x1),big_r(x1,sk2(x1)),big_p(x0) {x0 -> sk7, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 404:4:1:[401.3,378.2]:Top: big_r(sk7,sk4(x0)),big_r(sk7,sk4(sk7)) -> big_r(sk9,sk2(sk9)),big_p(x0)
% 25.04/6.70 === Backtracking. Learning clause 406:9:4:[378.1,405.7,46.6,48.4,372.3,47.4,398.4]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_r(sk7,x1),big_p(sk3(x2)),big_r(sk7,sk4(x2)),big_r(sk2(sk7),sk1(x3)),big_r(sk7,sk4(sk7)) -> big_p(x3),big_p(x2)
% 25.04/6.70 === Backtracking. Learning clause 407:1:0:[46.6,60.3,372.3,59.3,406.6,386.2,372.3,378.2,225.1]:: big_r(sk7,sk4(sk7)) ->
% 25.04/6.70 === Conflict found: 69:5:3:[37.0,23.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x1,sk2(x1)),big_r(sk4(x2),sk3(x2)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 409:3:1:[52.1,408.0,69.2,286.2,370.2]:Top: -> big_r(sk9,sk2(sk9)),big_p(x0),big_r(sk4(x0),sk3(x0))
% 25.04/6.70 === Conflict found: 259:6:2:[141.0,258.4,45.3,49.4,48.4,45.1]:TopTop: big_p(sk3(sk7)),big_p(sk9),big_r(x0,sk1(x1)),big_r(sk7,x0) -> big_p(x1),big_r(sk9,sk10) {x0 -> sk2(sk7), x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 411:3:0:[141.0,410.2,259.4,230.4,265.3]:: big_p(sk9),big_r(sk2(sk7),sk1(sk7)) -> big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 64:5:3:[37.0,18.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(sk1(x1)),big_r(x2,sk4(x2)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 413:3:2:[225.0,412.2,64.5,407.1]:TopTop: big_p(x0),big_r(x1,x0) -> big_p(sk1(x1))
% 25.04/6.70 === Conflict found: 65:5:3:[37.0,19.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,sk4(x2)),big_r(x1,sk2(x1)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 415:4:0:[182.1,414.3,65.4,407.1,411.3]:: big_p(sk10),big_p(sk9),big_r(sk2(sk7),sk1(sk7)) -> big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 48:4:2:[37.0,2.0]:TopTop: -> big_p(x0),big_p(x1),big_p(sk1(x1)),big_r(x0,sk4(x0)) {x0 -> sk7, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 417:2:1:[225.0,416.0,48.4,407.1]:Top: -> big_p(x0),big_p(sk1(x0))
% 25.04/6.70 === Conflict found: 51:4:2:[37.0,5.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x0,sk4(x0)),big_r(x1,sk2(x1)) {x0 -> sk7, x1 -> sk9}
% 25.04/6.70 === Backtracking. Learning clause 419:3:0:[225.0,418.1,51.3,407.1,411.1]:: big_r(sk2(sk7),sk1(sk7)) -> big_r(sk9,sk2(sk9)),big_r(sk9,sk10)
% 25.04/6.70 === Conflict found: 370:4:1:[186.0,369.3,44.1,49.3,61.3,52.3]:Top: big_p(sk9) -> big_p(sk10),big_p(x0),big_r(sk4(x0),sk3(x0)) {x0 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 420:3:0:[370.3,225.1]:: big_p(sk9) -> big_p(sk10),big_r(sk4(sk7),sk3(sk7))
% 25.04/6.70 === Backtracking. Learning clause 421:3:0:[44.1,417.2,115.4,225.1,415.1]:: big_p(sk9),big_r(sk2(sk7),sk1(sk7)) -> big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 65:5:3:[37.0,19.1]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,sk4(x2)),big_r(x1,sk2(x1)) {x0 -> sk10, x1 -> sk9, x2 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 422:2:0:[65.4,407.1,115.1,225.1,419.3,421.1]:: big_r(sk2(sk7),sk1(sk7)) -> big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 60:4:2:[37.0,14.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x0,sk4(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 423:1:0:[60.3,407.1,422.1,225.1]:: -> big_r(sk9,sk2(sk9))
% 25.04/6.70 === Conflict found: 60:4:2:[37.0,14.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x0,sk4(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70 === Backtracking. Learning clause 425:2:0:[141.0,424.1,60.3,407.1,411.2]:: big_p(sk9) -> big_r(sk9,sk10)
% 25.04/6.70 === Backtracking. Learning clause 427:7:4:[225.0,426.5,46.3,67.5,417.2,51.4,64.4]:TopTopTopTop: big_r(sk2(sk7),sk1(x0)),big_r(sk9,sk2(x1)),big_p(x2),big_r(x1,x2) -> big_p(x0),big_p(x3),big_r(x3,sk4(x3))
% 25.04/6.70 === Backtracking. Learning clause 429:1:0:[186.0,428.1,44.1,417.2,51.4,427.3,423.1,60.4,407.1,425.2]:: big_p(sk9) ->
% 25.04/6.70 === Backtracking. Learning clause 432:1:0:[429.0,430.1,407.0,431.2,46.3,60.4,417.2,48.3,51.4,225.1,423.1]:: big_r(sk2(sk7),sk1(sk7)) ->
% 25.04/6.70 === Conflict found: 60:4:2:[37.0,14.0]:TopTop: -> big_p(x0),big_p(x1),big_r(x0,sk4(x0)),big_r(sk2(x1),sk1(x1)) {x0 -> sk7, x1 -> sk7}
% 25.04/6.70
% 25.04/6.70 SZS status Unsatisfiable
% 25.04/6.70
% 25.04/6.70 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.04/6.70
% 25.04/6.70 SPASS-SCL-FOL Statistics:
% 25.04/6.70 Number of learned clauses: 227
% 25.04/6.70 Number of propagations: 1354
% 25.04/6.70 Number of decisions: 876
% 25.04/6.70 Number of resolutions: 884
% 25.04/6.70 Number of condensations: 94
% 25.04/6.70 Number of sub resolutions: 159
% 25.04/6.70 Number of input literals (deduplicated): 20
% 25.04/6.70 Number of grows: 5
% 25.04/6.70 Number of considered ground atoms: 129
% 25.04/6.70
% 25.04/6.70 Needed: 0:00:06.16
% 25.04/6.70
%------------------------------------------------------------------------------