%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN067-1 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 7.27s 2.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN067-1 : TPTP v9.2.1. Released v1.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n016.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:52 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 7.27/2.02 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.27/2.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.27/2.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.27/2.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.27/2.02 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.27/2.02 Execution normal ended with status: unsatisfiable
% 7.27/2.02 Used heuristic: normal
% 7.27/2.02
% 7.27/2.02 Input Clauses:
% 7.27/2.02
% 7.27/2.02 Predicates: big_p big_r
% 7.27/2.02 Fol Constants: a c3 c4 c2 c1
% 7.27/2.02 Fol Functions: f2 f4 f3 f6 f5 f1
% 7.27/2.02 Problem Properties:
% 7.27/2.02 This is a full first-order problem without equality.
% 7.27/2.02
% 7.27/2.02 After reduction: Problem Properties:
% 7.27/2.02 This is a full first-order problem without equality.
% 7.27/2.02
% 7.27/2.02
% 7.27/2.02 Reduced Input Clauses:
% 7.27/2.02 85:4:2:[37.0,1.0]:TopTop: -> big_p(x0),big_p(f2(x0)),big_p(x1),big_p(f4(x1))
% 7.27/2.02 86:4:2:[37.0,2.0]:TopTop: -> big_p(x0),big_p(f2(x0)),big_p(x1),big_r(x1,f3(x1))
% 7.27/2.02 87:4:2:[37.0,3.0]:TopTop: -> big_p(x0),big_p(f2(x0)),big_p(x1),big_r(f3(x1),f4(x1))
% 7.27/2.02 88:5:3:[37.0,4.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(f2(x2)),big_p(f6(x1))
% 7.27/2.02 89:5:3:[37.0,5.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(f2(x2)),big_r(x1,f5(x1))
% 7.27/2.02 90:5:3:[37.0,6.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_p(f2(x2)),big_r(f5(x1),f6(x1))
% 7.27/2.02 91:4:2:[37.0,7.0]:TopTop: -> big_p(x0),big_r(x0,f1(x0)),big_p(x1),big_p(f4(x1))
% 7.27/2.02 92:4:2:[37.0,8.0]:TopTop: -> big_p(x0),big_r(x0,f1(x0)),big_p(x1),big_r(x1,f3(x1))
% 7.27/2.02 93:4:2:[37.0,9.0]:TopTop: -> big_p(x0),big_r(x0,f1(x0)),big_p(x1),big_r(f3(x1),f4(x1))
% 7.27/2.02 94:5:3:[37.0,10.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,f1(x2)),big_p(f6(x1))
% 7.27/2.02 95:5:3:[37.0,11.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,f1(x2)),big_r(x1,f5(x1))
% 7.27/2.02 96:5:3:[37.0,12.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(x2,f1(x2)),big_r(f5(x1),f6(x1))
% 7.27/2.02 97:4:2:[37.0,13.0]:TopTop: -> big_p(x0),big_r(f1(x0),f2(x0)),big_p(x1),big_p(f4(x1))
% 7.27/2.02 98:4:2:[37.0,14.0]:TopTop: -> big_p(x0),big_r(f1(x0),f2(x0)),big_p(x1),big_r(x1,f3(x1))
% 7.27/2.02 99:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_r(f1(x0),f2(x0)),big_p(x1),big_r(f3(x1),f4(x1))
% 7.27/2.02 100:5:3:[37.0,16.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(f1(x2),f2(x2)),big_p(f6(x1))
% 7.27/2.02 101:5:3:[37.0,17.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(f1(x2),f2(x2)),big_r(x1,f5(x1))
% 7.27/2.02 102:5:3:[37.0,18.0]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(x2),big_r(f1(x2),f2(x2)),big_r(f5(x1),f6(x1))
% 7.27/2.02 103:5:3:[37.0,19.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(f2(x1)),big_p(x2),big_p(f4(x2))
% 7.27/2.02 104:5:3:[37.0,20.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(f2(x1)),big_p(x2),big_r(x2,f3(x2))
% 7.27/2.02 105:5:3:[37.0,21.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_p(f2(x1)),big_p(x2),big_r(f3(x2),f4(x2))
% 7.27/2.02 106:6:4:[37.0,22.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_p(f6(x3))
% 7.27/2.02 107:6:4:[37.0,23.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(x3,f5(x3))
% 7.27/2.02 108:6:4:[37.0,24.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(f5(x3),f6(x3))
% 7.27/2.02 109:5:3:[37.0,25.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(x1,f1(x1)),big_p(x2),big_p(f4(x2))
% 7.27/2.02 110:5:3:[37.0,26.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(x1,f1(x1)),big_p(x2),big_r(x2,f3(x2))
% 7.27/2.02 111:5:3:[37.0,27.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(x1,f1(x1)),big_p(x2),big_r(f3(x2),f4(x2))
% 7.27/2.02 112:6:4:[37.0,28.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_p(f6(x3))
% 7.27/2.02 113:6:4:[37.0,29.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(x3,f5(x3))
% 7.27/2.02 114:6:4:[37.0,30.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(f5(x3),f6(x3))
% 7.27/2.02 115:5:3:[37.0,31.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(f1(x1),f2(x1)),big_p(x2),big_p(f4(x2))
% 7.27/2.02 116:5:3:[37.0,32.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(f1(x1),f2(x1)),big_p(x2),big_r(x2,f3(x2))
% 7.27/2.02 117:5:3:[37.0,33.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(f1(x1),f2(x1)),big_p(x2),big_r(f3(x2),f4(x2))
% 7.27/2.02 118:6:4:[37.0,34.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_p(f6(x3))
% 7.27/2.02 119:6:4:[37.0,35.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_r(x3,f5(x3))
% 7.27/2.02 120:6:4:[37.0,36.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_r(f5(x3),f6(x3))
% 7.27/2.02
% 7.27/2.02 Most General Atoms: big_p(x2) big_r(x3,x2)
% 7.27/2.02
% 7.27/2.02 === Starting SPASS-SCL-FOL A Little Less Naive, considering 46 atoms initially, heuristics mode: normal ===
% 7.27/2.02
% 7.27/2.02 === Clause set with instances from active satisfied. Growing active. New size: 110
% 7.27/2.02 === Backtracking. Learning clause 121:4:1:[84.2,92.2,98.2,86.2,86.2,98.2,92.2]:Top: -> big_p(c2),big_p(c4),big_p(x0),big_r(x0,f3(x0))
% 7.27/2.02 === Backtracking. Learning clause 122:6:3:[84.3,87.4,87.4,85.4,85.4]:TopTopTop: big_r(c2,f3(x0)),big_r(c4,f3(x1)) -> big_p(x1),big_p(x2),big_p(f2(x2)),big_p(x0)
% 7.27/2.02 === Backtracking. Learning clause 123:8:4:[84.6,97.2,91.2,84.4]:TopTopTopTop: big_p(f2(c4)),big_p(x0),big_r(c2,x1),big_r(x1,x0),big_r(c4,x2),big_r(x2,f4(x3)) -> big_p(c4),big_p(x3)
% 7.27/2.02 === Conflict found: 123:8:4:[84.6,97.2,91.2,84.4]:TopTopTopTop: big_p(f2(c4)),big_p(x0),big_r(c2,x1),big_r(x1,x0),big_r(c4,x2),big_r(x2,f4(x3)) -> big_p(c4),big_p(x3) {x0 -> f2(c2), x1 -> f1(c2), x2 -> f3(c4), x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 124:10:3:[123.3,93.2,99.2,123.4]:TopTopTop: big_p(f2(c2)),big_p(f2(c4)),big_p(f4(x0)),big_r(c2,f3(x0)),big_r(c4,x1),big_r(x1,f4(x2)) -> big_p(c2),big_p(x0),big_p(c4),big_p(x2)
% 7.27/2.02 === Backtracking. Learning clause 125:9:2:[84.5,93.2,99.2,99.2,93.2,124.6]:TopTop: big_p(f2(c2)),big_p(f2(c4)),big_p(f4(x0)),big_r(c2,f3(x0)),big_r(c4,f3(x1)) -> big_p(c2),big_p(x0),big_p(c4),big_p(x1)
% 7.27/2.02 === Backtracking. Learning clause 126:2:0:[84.6,97.2,91.2,91.2,97.2,125.3,122.5,122.5,121.4,121.4]:: -> big_p(c2),big_p(c4)
% 7.27/2.02 === Backtracking. Learning clause 128:6:2:[126.0,127.0,84.2,113.6,112.6,114.6,72.5,60.5,85.4,86.4]:TopTop: big_r(f3(c4),f4(x0)) -> big_r(c2,f1(c2)),big_p(x0),big_p(x1),big_p(f2(x1)),big_p(c4)
% 7.27/2.02 === Conflict found: 123:8:4:[84.6,97.2,91.2,84.4]:TopTopTopTop: big_p(f2(c4)),big_p(x0),big_r(c2,x1),big_r(x1,x0),big_r(c4,x2),big_r(x2,f4(x3)) -> big_p(c4),big_p(x3) {x0 -> f6(c2), x1 -> f5(c2), x2 -> f3(c4), x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 130:6:2:[126.0,129.0,123.4,114.6,112.6,113.6,110.5,72.5,60.5,128.5]:TopTop: big_r(c4,x0),big_r(x0,f2(c4)),big_r(f3(c4),f4(x1)) -> big_r(c2,f1(c2)),big_p(x1),big_p(c4)
% 7.27/2.02 === Conflict found: 111:5:3:[37.0,27.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(x1,f1(x1)),big_p(x2),big_r(f3(x2),f4(x2)) {x0 -> c1, x1 -> c2, x2 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 131:4:1:[111.2,72.5,60.5,126.1,87.2,130.3]:Top: big_r(c4,x0),big_r(x0,f2(c4)) -> big_r(c2,f1(c2)),big_p(c4)
% 7.27/2.02 === Backtracking. Learning clause 132:7:3:[60.2,97.4]:TopTopTop: big_p(c2),big_r(c4,x0),big_r(x0,f4(x1)) -> big_p(c1),big_p(x2),big_r(f1(x2),f2(x2)),big_p(x1)
% 7.27/2.02 === Conflict found: 123:8:4:[84.6,97.2,91.2,84.4]:TopTopTopTop: big_p(f2(c4)),big_p(x0),big_r(c2,x1),big_r(x1,x0),big_r(c4,x2),big_r(x2,f4(x3)) -> big_p(c4),big_p(x3) {x0 -> f6(c2), x1 -> f5(c2), x2 -> f3(c4), x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 133:3:0:[123.2,100.5,102.5,101.5,72.5,97.4,132.4,126.1,98.4,128.5,99.4,131.2]:: big_r(c4,f1(c4)) -> big_r(c2,f1(c2)),big_p(c4)
% 7.27/2.02 === Conflict found: 87:4:2:[37.0,3.0]:TopTop: -> big_p(x0),big_p(f2(x0)),big_p(x1),big_r(f3(x1),f4(x1)) {x0 -> c4, x1 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 134:4:1:[87.4,128.1]:Top: -> big_r(c2,f1(c2)),big_p(x0),big_p(f2(x0)),big_p(c4)
% 7.27/2.02 === Backtracking. Learning clause 135:5:1:[60.1,126.1,91.4,92.4,133.1]:Top: big_r(f3(c4),f4(x0)) -> big_p(c1),big_p(x0),big_r(c2,f1(c2)),big_p(c4)
% 7.27/2.02 === Conflict found: 123:8:4:[84.6,97.2,91.2,84.4]:TopTopTopTop: big_p(f2(c4)),big_p(x0),big_r(c2,x1),big_r(x1,x0),big_r(c4,x2),big_r(x2,f4(x3)) -> big_p(c4),big_p(x3) {x0 -> f6(c2), x1 -> f5(c2), x2 -> f3(c4), x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 136:5:1:[123.2,94.5,95.5,96.5,72.5,126.1,92.4,91.4,133.1,135.2]:Top: big_p(f2(c4)),big_r(f3(c4),f4(x0)) -> big_p(x0),big_r(c2,f1(c2)),big_p(c4)
% 7.27/2.02 === Conflict found: 93:4:2:[37.0,9.0]:TopTop: -> big_p(x0),big_r(x0,f1(x0)),big_p(x1),big_r(f3(x1),f4(x1)) {x0 -> c4, x1 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 137:2:0:[93.2,133.1,136.2,134.3]:: -> big_r(c2,f1(c2)),big_p(c4)
% 7.27/2.02 === Backtracking. Learning clause 138:6:2:[60.1,126.1,86.4,85.4]:TopTop: big_r(f3(c4),f4(x0)) -> big_p(c1),big_p(c4),big_p(x1),big_p(f2(x1)),big_p(x0)
% 7.27/2.02 === Backtracking. Learning clause 140:5:1:[126.0,139.1,60.4,98.2,92.2,60.3]:Top: big_p(f2(c4)),big_p(x0),big_r(f3(c4),x0) -> big_p(c4),big_p(c1)
% 7.27/2.02 === Backtracking. Learning clause 141:4:1:[60.4,97.2,126.1,91.2,140.2,138.5]:Top: big_r(f3(c4),f4(x0)) -> big_p(c1),big_p(c4),big_p(x0)
% 7.27/2.02 === Backtracking. Learning clause 142:6:2:[84.1,88.5,89.5,90.5,72.5,126.1,86.4]:TopTop: big_p(c1),big_p(x0),big_r(f3(c4),x0) -> big_p(x1),big_p(f2(x1)),big_p(c4)
% 7.27/2.02 === Backtracking. Learning clause 145:4:1:[121.0,143.1,86.1,144.2,84.1,104.3,116.3,137.1,72.5,98.2,92.2]:Top: big_p(c1) -> big_p(c4),big_p(x0),big_r(x0,f3(x0))
% 7.27/2.02 === Backtracking. Learning clause 146:9:6:[84.1,106.5,118.5]:TopTopTopTopTopTop: big_r(c2,f1(x0)),big_p(x1),big_r(c4,x2),big_r(x2,x1),big_p(x3),big_r(x0,x3),big_p(x4),big_r(x5,x4) -> big_p(f6(x5))
% 7.27/2.02 === Backtracking. Learning clause 147:10:6:[84.3,108.6,107.6,84.1]:TopTopTopTopTopTop: big_p(f6(c2)),big_p(x0),big_r(x1,x0),big_p(x2),big_r(c2,x2),big_r(c2,x3),big_r(x3,f2(x1)),big_p(x4),big_r(c4,x5),big_r(x5,x4) ->
% 7.27/2.02 === Backtracking. Learning clause 148:6:3:[84.2,119.6,120.6,147.7,146.9,137.1]:TopTopTop: big_p(x0),big_r(c4,x1),big_r(x1,x0),big_p(x2),big_r(c2,x2) -> big_p(c4)
% 7.27/2.02 === Backtracking. Learning clause 149:5:2:[72.5,148.5,126.1,145.4,141.2]:TopTop: big_p(x0),big_r(f3(c4),x0),big_r(f3(c4),f4(x1)) -> big_p(c4),big_p(x1)
% 7.27/2.02 === Conflict found: 145:4:1:[121.0,143.1,86.1,144.2,84.1,104.3,116.3,137.1,72.5,98.2,92.2]:Top: big_p(c1) -> big_p(c4),big_p(x0),big_r(x0,f3(x0)) {x0 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 150:5:2:[145.1,141.2]:TopTop: big_r(f3(c4),f4(x0)) -> big_p(x1),big_r(x1,f3(x1)),big_p(c4),big_p(x0)
% 7.27/2.02 === Backtracking. Learning clause 151:3:1:[72.5,148.5,97.2,91.2,85.2,126.1,149.1,141.2]:Top: big_r(f3(c4),f4(x0)) -> big_p(c4),big_p(x0)
% 7.27/2.02 === Backtracking. Learning clause 153:3:1:[121.0,152.0,60.4,98.2,92.2,86.2,145.1]:Top: -> big_p(c4),big_p(x0),big_r(x0,f3(x0))
% 7.27/2.02 === Conflict found: 87:4:2:[37.0,3.0]:TopTop: -> big_p(x0),big_p(f2(x0)),big_p(x1),big_r(f3(x1),f4(x1)) {x0 -> c4, x1 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 154:3:1:[87.4,151.1]:Top: -> big_p(x0),big_p(f2(x0)),big_p(c4)
% 7.27/2.02 === Conflict found: 99:4:2:[37.0,15.0]:TopTop: -> big_p(x0),big_r(f1(x0),f2(x0)),big_p(x1),big_r(f3(x1),f4(x1)) {x0 -> c4, x1 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 157:4:1:[126.0,155.0,154.1,156.1,99.4,151.1,60.4]:Top: big_r(c4,f1(x0)) -> big_p(x0),big_p(c4),big_p(c1)
% 7.27/2.02 === Conflict found: 93:4:2:[37.0,9.0]:TopTop: -> big_p(x0),big_r(x0,f1(x0)),big_p(x1),big_r(f3(x1),f4(x1)) {x0 -> c4, x1 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 158:2:0:[93.4,151.1,157.1]:: -> big_p(c4),big_p(c1)
% 7.27/2.02 === Backtracking. Learning clause 159:1:0:[72.5,148.5,126.1,99.2,154.2,93.2,151.1,158.2]:: -> big_p(c4)
% 7.27/2.02 === Backtracking. Learning clause 161:3:1:[126.1,160.0,84.6,96.5,95.5,94.5,78.5,79.5,92.4,93.4,91.4]:Top: -> big_p(x0),big_r(x0,f1(x0)),big_p(c2)
% 7.27/2.02 === Backtracking. Learning clause 163:4:2:[159.0,162.3,84.5,107.6,106.6,108.6,78.5,79.5]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(f2(c4))
% 7.27/2.02 === Conflict found: 163:4:2:[159.0,162.3,84.5,107.6,106.6,108.6,78.5,79.5]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(f2(c4)) {x0 -> f4(c2), x1 -> f3(c2)}
% 7.27/2.02 === Backtracking. Learning clause 164:5:1:[163.2,98.4,99.4,97.4,163.3]:Top: big_p(f2(x0)),big_r(c2,f1(x0)) -> big_p(x0),big_p(c2),big_p(f2(c4))
% 7.27/2.02 === Conflict found: 163:4:2:[159.0,162.3,84.5,107.6,106.6,108.6,78.5,79.5]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(f2(c4)) {x0 -> f4(c2), x1 -> f3(c2)}
% 7.27/2.02 === Backtracking. Learning clause 165:2:0:[163.2,86.4,87.4,85.4,164.1,161.2]:: -> big_p(f2(c4)),big_p(c2)
% 7.27/2.02 === Backtracking. Learning clause 166:2:0:[60.3,107.6,108.6,106.6,55.4,54.4,159.1,165.2]:: -> big_p(c1),big_p(f2(c4))
% 7.27/2.02 === Backtracking. Learning clause 167:7:3:[84.2,98.4,99.4,97.4,84.3]:TopTopTop: big_p(f2(x0)),big_r(c2,f1(x0)),big_p(x1),big_r(c4,x2),big_r(x2,x1) -> big_p(x0),big_p(c2)
% 7.27/2.02 === Backtracking. Learning clause 168:4:2:[84.2,86.4,87.4,85.4,167.1,161.2]:TopTop: big_p(x0),big_r(c4,x1),big_r(x1,x0) -> big_p(c2)
% 7.27/2.02 === Conflict found: 116:5:3:[37.0,32.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(f1(x1),f2(x1)),big_p(x2),big_r(x2,f3(x2)) {x0 -> c3, x1 -> c4, x2 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 170:5:2:[86.1,169.0,116.2,79.5,78.5,159.1,98.2]:TopTop: big_r(c2,f1(x0)) -> big_r(f1(c4),f2(c4)),big_p(x0),big_p(x1),big_r(x1,f3(x1))
% 7.27/2.02 === Conflict found: 168:4:2:[84.2,86.4,87.4,85.4,167.1,161.2]:TopTop: big_p(x0),big_r(c4,x1),big_r(x1,x0) -> big_p(c2) {x0 -> f6(c4), x1 -> f5(c4)}
% 7.27/2.02 === Backtracking. Learning clause 171:5:2:[168.1,118.6,119.6,120.6,78.5,79.5,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c2),big_r(f1(c4),f2(c4))
% 7.27/2.02 === Conflict found: 171:5:2:[168.1,118.6,119.6,120.6,78.5,79.5,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c2),big_r(f1(c4),f2(c4)) {x0 -> f4(c2), x1 -> f3(c2)}
% 7.27/2.02 === Backtracking. Learning clause 172:3:0:[171.1,97.4,99.4,171.3,170.5,161.2]:: big_p(f2(c2)) -> big_r(f1(c4),f2(c4)),big_p(c2)
% 7.27/2.02 === Conflict found: 171:5:2:[168.1,118.6,119.6,120.6,78.5,79.5,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c2),big_r(f1(c4),f2(c4)) {x0 -> f4(c2), x1 -> f3(c2)}
% 7.27/2.02 === Backtracking. Learning clause 174:2:0:[165.0,173.0,171.1,85.4,86.4,87.4,172.1,168.3]:: big_r(c4,f1(c4)) -> big_p(c2)
% 7.27/2.02 === Conflict found: 163:4:2:[159.0,162.3,84.5,107.6,106.6,108.6,78.5,79.5]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(f2(c4)) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 178:3:0:[55.2,175.0,165.1,176.1,137.1,177.2,163.1,112.6,114.6,113.6,67.3]:: -> big_p(f2(c4)),big_r(c2,f1(c2)),big_r(c4,c3)
% 7.27/2.02 === Conflict found: 163:4:2:[159.0,162.3,84.5,107.6,106.6,108.6,78.5,79.5]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(f2(c4)) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 182:3:0:[54.2,179.0,165.1,180.1,137.1,181.2,163.1,112.6,114.6,113.6,66.3]:: -> big_p(f2(c4)),big_r(c2,f1(c2)),big_p(c3)
% 7.27/2.02 === Conflict found: 163:4:2:[159.0,162.3,84.5,107.6,106.6,108.6,78.5,79.5]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(f2(c4)) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 183:9:5:[163.1,112.6,114.6,107.6]:TopTopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2),big_p(x4),big_r(c2,x4) -> big_p(f2(c4)),big_r(x1,f1(x1)),big_p(f2(x3))
% 7.27/2.02 === Conflict found: 183:9:5:[163.1,112.6,114.6,107.6]:TopTopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2),big_p(x4),big_r(c2,x4) -> big_p(f2(c4)),big_r(x1,f1(x1)),big_p(f2(x3)) {x0 -> c1, x1 -> c2, x2 -> c3, x3 -> c4, x4 -> c1}
% 7.27/2.02 === Backtracking. Learning clause 184:7:3:[183.1,166.1]:TopTopTop: big_r(x0,c1),big_p(x1),big_r(x2,x1),big_r(c2,c1) -> big_r(x0,f1(x0)),big_p(f2(x2)),big_p(f2(c4))
% 7.27/2.02 === Backtracking. Learning clause 186:3:1:[165.1,185.0,72.4,108.6,107.6,106.6,184.1,178.3,182.3,163.2]:Top: big_p(x0),big_r(f1(c2),x0) -> big_p(f2(c4))
% 7.27/2.02 === Backtracking. Learning clause 187:6:2:[84.1,112.6,114.6,113.6,60.5,84.2,186.3]:TopTop: big_r(c2,c1),big_p(c2),big_r(c4,x0),big_r(x0,f2(c4)),big_p(x1),big_r(f1(c2),x1) ->
% 7.27/2.02 === Backtracking. Learning clause 188:5:2:[72.2,186.3,187.1]:TopTop: big_p(c2),big_r(c4,x0),big_r(x0,f2(c4)),big_p(x1),big_r(f1(c2),x1) ->
% 7.27/2.02 === Conflict found: 163:4:2:[159.0,162.3,84.5,107.6,106.6,108.6,78.5,79.5]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(f2(c4)) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 190:5:1:[165.1,189.1,163.1,118.6,120.6,119.6,188.5,166.1]:Top: big_r(c2,c1),big_r(c4,x0),big_r(x0,f2(c4)),big_p(f2(c2)) -> big_p(f2(c4))
% 7.27/2.02 === Backtracking. Learning clause 191:5:1:[84.1,118.6,119.6,120.6,188.5,60.5,190.5]:Top: big_p(c2),big_r(c2,c1),big_r(c4,x0),big_r(x0,f2(c4)),big_p(f2(c2)) ->
% 7.27/2.02 === Backtracking. Learning clause 193:3:0:[165.1,192.0,72.3,107.6,106.6,108.6,178.3,182.3]:: -> big_r(c2,c1),big_p(f2(c4)),big_r(c2,f1(c2))
% 7.27/2.02 === Backtracking. Learning clause 194:3:0:[66.2,159.1]:: big_p(c2) -> big_r(c2,c1),big_p(c3)
% 7.27/2.02 === Backtracking. Learning clause 195:3:0:[67.2,159.1]:: big_p(c2) -> big_r(c2,c1),big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 196:4:1:[72.2,106.6,108.6,107.6,194.3,195.3,72.2,191.2]:Top: big_p(c2),big_r(c4,x0),big_r(x0,f2(c4)),big_p(f2(c2)) ->
% 7.27/2.02 === Conflict found: 163:4:2:[159.0,162.3,84.5,107.6,106.6,108.6,78.5,79.5]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(f2(c4)) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 197:3:0:[163.1,118.6,119.6,120.6,186.2,166.1]:: big_r(c2,c1),big_p(f2(c2)) -> big_p(f2(c4))
% 7.27/2.02 === Backtracking. Learning clause 198:3:0:[54.2,159.1]:: big_p(c2) -> big_p(c1),big_p(c3)
% 7.27/2.02 === Backtracking. Learning clause 200:6:3:[108.4,199.0,78.2,114.5,159.1,120.5]:TopTopTop: big_p(x0),big_r(c2,x0),big_p(x1),big_r(x2,x1) -> big_p(c3),big_r(f5(x2),f6(x2))
% 7.27/2.02 === Backtracking. Learning clause 202:9:4:[159.0,201.7,79.1,112.6,113.6,78.2]:TopTopTopTop: big_r(f5(c2),f6(x0)),big_p(x1),big_r(x0,x1),big_p(x2),big_r(c2,x2),big_p(x3),big_r(f1(c2),x3) -> big_r(c4,c3),big_p(c3)
% 7.27/2.02 === Backtracking. Learning clause 204:4:0:[194.1,203.1,79.4,159.1,118.6,119.6,202.7,200.6,198.2]:: big_p(f2(c2)),big_p(c2) -> big_r(c4,c3),big_p(c3)
% 7.27/2.02 === Conflict found: 112:6:4:[37.0,28.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_p(f6(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 206:8:4:[159.0,205.6,112.5,79.2]:TopTopTopTop: big_p(x0),big_r(c2,x0),big_p(x1),big_r(x2,x1),big_p(x3),big_r(f1(c2),x3) -> big_p(f6(x2)),big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 208:4:1:[195.1,207.0,79.3,114.6,113.6,79.2,206.7,55.3,159.1]:Top: big_p(x0),big_r(f1(c2),x0),big_p(c2) -> big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 209:6:2:[55.2,159.1,118.1]:TopTop: big_p(c2),big_r(x0,c1),big_r(x1,c1) -> big_r(c4,c3),big_r(f1(x0),f2(x0)),big_p(f6(x1))
% 7.27/2.02 === Backtracking. Learning clause 211:3:0:[195.1,210.0,79.3,120.6,119.6,55.3,159.1,209.6,208.2]:: big_p(f2(c2)),big_p(c2) -> big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 214:3:0:[158.0,212.1,174.1,213.3,60.2,118.6,120.6,119.6,196.3,54.4,211.3]:: big_r(c4,f1(c4)),big_p(f2(c2)) -> big_p(c1)
% 7.27/2.02 === Conflict found: 204:4:0:[194.1,203.1,79.4,159.1,118.6,119.6,202.7,200.6,198.2]:: big_p(f2(c2)),big_p(c2) -> big_r(c4,c3),big_p(c3) {}
% 7.27/2.02 === Backtracking. Learning clause 215:4:0:[204.2,174.2]:: big_p(f2(c2)),big_r(c4,f1(c4)) -> big_r(c4,c3),big_p(c3)
% 7.27/2.02 === Conflict found: 195:3:0:[67.2,159.1]:: big_p(c2) -> big_r(c2,c1),big_r(c4,c3) {}
% 7.27/2.02 === Backtracking. Learning clause 216:3:0:[195.1,174.2]:: big_r(c4,f1(c4)) -> big_r(c2,c1),big_r(c4,c3)
% 7.27/2.02 === Conflict found: 194:3:0:[66.2,159.1]:: big_p(c2) -> big_r(c2,c1),big_p(c3) {}
% 7.27/2.02 === Backtracking. Learning clause 217:3:0:[194.1,174.2]:: big_r(c4,f1(c4)) -> big_r(c2,c1),big_p(c3)
% 7.27/2.02 === Backtracking. Learning clause 218:5:0:[72.2,118.6,120.6,119.6,72.4,174.2,216.3,217.3,112.2]:: big_p(f2(c4)),big_r(c4,f1(c4)),big_p(c1) -> big_r(c2,f1(c2)),big_p(f6(c2))
% 7.27/2.02 === Backtracking. Learning clause 221:6:1:[159.0,219.2,186.2,220.3,78.2,218.4]:Top: big_p(x0),big_r(f1(c2),x0),big_r(c4,f1(c4)),big_p(c1) -> big_p(c3),big_p(f6(c2))
% 7.27/2.02 === Conflict found: 208:4:1:[195.1,207.0,79.3,114.6,113.6,79.2,206.7,55.3,159.1]:Top: big_p(x0),big_r(f1(c2),x0),big_p(c2) -> big_r(c4,c3) {x0 -> f2(c2)}
% 7.27/2.02 === Backtracking. Learning clause 222:4:1:[208.3,174.2]:Top: big_p(x0),big_r(f1(c2),x0),big_r(c4,f1(c4)) -> big_r(c4,c3)
% 7.27/2.02 === Conflict found: 218:5:0:[72.2,118.6,120.6,119.6,72.4,174.2,216.3,217.3,112.2]:: big_p(f2(c4)),big_r(c4,f1(c4)),big_p(c1) -> big_r(c2,f1(c2)),big_p(f6(c2)) {}
% 7.27/2.02 === Backtracking. Learning clause 223:6:1:[218.1,186.3]:Top: big_r(c4,f1(c4)),big_p(c1),big_p(x0),big_r(f1(c2),x0) -> big_r(c2,f1(c2)),big_p(f6(c2))
% 7.27/2.02 === Backtracking. Learning clause 224:5:1:[84.6,120.6,118.6,119.6,188.3,174.2,222.4,223.5,221.5]:Top: big_p(x0),big_r(f1(c2),x0),big_r(c4,f1(c4)),big_p(c1) -> big_p(f6(c2))
% 7.27/2.02 === Conflict found: 218:5:0:[72.2,118.6,120.6,119.6,72.4,174.2,216.3,217.3,112.2]:: big_p(f2(c4)),big_r(c4,f1(c4)),big_p(c1) -> big_r(c2,f1(c2)),big_p(f6(c2)) {}
% 7.27/2.02 === Backtracking. Learning clause 225:5:0:[218.1,182.1]:: big_r(c4,f1(c4)),big_p(c1) -> big_p(f6(c2)),big_r(c2,f1(c2)),big_p(c3)
% 7.27/2.02 === Conflict found: 118:6:4:[37.0,34.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_p(f6(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 227:4:0:[214.2,226.2,118.2,217.2,224.2]:: big_p(f2(c2)),big_r(c4,f1(c4)) -> big_p(c3),big_p(f6(c2))
% 7.27/2.02 === Conflict found: 193:3:0:[165.1,192.0,72.3,107.6,106.6,108.6,178.3,182.3]:: -> big_r(c2,c1),big_p(f2(c4)),big_r(c2,f1(c2)) {}
% 7.27/2.02 === Backtracking. Learning clause 228:4:0:[193.1,112.2,218.1]:: big_r(c4,f1(c4)),big_p(c1) -> big_r(c2,f1(c2)),big_p(f6(c2))
% 7.27/2.02 === Backtracking. Learning clause 229:7:3:[72.3,107.6,106.6,108.6]:TopTopTop: big_p(c2),big_p(x0),big_r(x1,x0),big_p(x2),big_r(c4,x2) -> big_r(c2,c1),big_p(f2(x1))
% 7.27/2.02 === Conflict found: 120:6:4:[37.0,36.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_r(f5(x3),f6(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 232:6:3:[174.1,230.4,114.4,231.5,120.5,196.3]:TopTopTop: big_p(x0),big_r(c4,x0),big_p(x1),big_r(x2,x1),big_p(f2(c2)) -> big_r(f5(x2),f6(x2))
% 7.27/2.02 === Conflict found: 229:7:3:[72.3,107.6,106.6,108.6]:TopTopTop: big_p(c2),big_p(x0),big_r(x1,x0),big_p(x2),big_r(c4,x2) -> big_r(c2,c1),big_p(f2(x1)) {x0 -> c3, x1 -> c4, x2 -> c3}
% 7.27/2.02 === Backtracking. Learning clause 233:7:3:[229.1,174.2]:TopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(c4,x2),big_r(c4,f1(c4)) -> big_r(c2,c1),big_p(f2(x1))
% 7.27/2.02 === Backtracking. Learning clause 235:3:0:[214.2,234.0,72.3,119.6,118.6,72.4,232.6,174.2,233.7,216.3,118.2,224.2,227.3]:: big_p(f2(c2)),big_r(c4,f1(c4)) -> big_p(f6(c2))
% 7.27/2.02 === Conflict found: 194:3:0:[66.2,159.1]:: big_p(c2) -> big_r(c2,c1),big_p(c3) {}
% 7.27/2.02 === Backtracking. Learning clause 237:3:0:[165.1,236.0,194.2,197.1]:: big_p(f2(c2)) -> big_p(c3),big_p(f2(c4))
% 7.27/2.02 === Conflict found: 229:7:3:[72.3,107.6,106.6,108.6]:TopTopTop: big_p(c2),big_p(x0),big_r(x1,x0),big_p(x2),big_r(c4,x2) -> big_r(c2,c1),big_p(f2(x1)) {x0 -> c3, x1 -> c4, x2 -> c3}
% 7.27/2.02 === Backtracking. Learning clause 239:2:0:[165.1,238.0,229.3,211.3,197.1,237.2]:: big_p(f2(c2)) -> big_p(f2(c4))
% 7.27/2.02 === Backtracking. Learning clause 241:5:1:[217.1,240.1,78.3,200.6,113.6,159.1,214.3,235.3]:Top: big_r(x0,c1),big_p(f2(c2)),big_r(c4,f1(c4)) -> big_p(c3),big_r(x0,f1(x0))
% 7.27/2.02 === Backtracking. Learning clause 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3)
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 243:3:0:[242.3,120.6,119.6,214.3,235.3,242.3,241.5,217.2]:: big_p(f2(c2)),big_r(c4,f1(c4)) -> big_p(c3)
% 7.27/2.02 === Backtracking. Learning clause 246:7:2:[235.2,244.0,241.3,245.3,84.4,112.6,113.6,232.6,113.6,232.6,214.3,222.4]:TopTop: big_r(x0,c1),big_r(c2,c1),big_p(f2(c2)),big_p(x1),big_r(f1(c2),x1),big_r(c4,f1(c4)) -> big_r(x0,f1(x0))
% 7.27/2.02 === Conflict found: 211:3:0:[195.1,210.0,79.3,120.6,119.6,55.3,159.1,209.6,208.2]:: big_p(f2(c2)),big_p(c2) -> big_r(c4,c3) {}
% 7.27/2.02 === Backtracking. Learning clause 247:3:0:[211.2,174.2]:: big_p(f2(c2)),big_r(c4,f1(c4)) -> big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 248:11:4:[72.3,119.6,118.6,72.4,232.6,174.2,246.1]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(f2(x1)),big_r(c4,f1(x1)),big_p(x2),big_r(c4,x2),big_p(f2(c2)),big_p(x3),big_r(f1(c2),x3),big_r(c4,f1(c4)) -> big_r(c2,f1(c2))
% 7.27/2.02 === Backtracking. Learning clause 249:10:4:[84.5,119.6,118.6,84.6,232.6,248.11]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(f2(x1)),big_r(c4,f1(x1)),big_p(x2),big_r(c4,x2),big_p(f2(c2)),big_p(x3),big_r(f1(c2),x3),big_r(c4,f1(c4)) ->
% 7.27/2.02 === Backtracking. Learning clause 250:10:4:[84.3,114.6,113.6,235.3,113.6,112.6,214.3]:TopTopTopTop: big_r(f5(c4),f6(x0)),big_r(c2,c1),big_p(x1),big_r(c4,x1),big_r(x2,c1),big_p(x3),big_r(x0,x3),big_r(c4,f1(c4)),big_p(f2(c2)) -> big_r(x2,f1(x2))
% 7.27/2.02 === Backtracking. Learning clause 252:8:4:[106.4,251.0,72.4,118.5,174.2]:TopTopTopTop: big_r(c4,f1(x0)),big_p(x1),big_r(x0,x1),big_p(x2),big_r(x3,x2),big_r(c4,f1(c4)) -> big_r(c2,c1),big_p(f6(x3))
% 7.27/2.02 === Conflict found: 119:6:4:[37.0,35.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_r(x3,f5(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 253:9:3:[119.5,72.4,72.3,174.2,252.8,250.2,232.6]:TopTopTop: big_p(x0),big_r(x1,x0),big_p(f2(x1)),big_r(c4,f1(x1)),big_r(c4,f1(c4)),big_p(x2),big_r(c4,x2),big_p(f2(c2)) -> big_r(c2,f1(c2))
% 7.27/2.02 === Conflict found: 118:6:4:[37.0,34.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_p(f6(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 256:6:3:[174.1,254.4,112.4,255.5,118.5,196.3]:TopTopTop: big_p(x0),big_r(c4,x0),big_p(x1),big_r(x2,x1),big_p(f2(c2)) -> big_p(f6(x2))
% 7.27/2.02 === Conflict found: 250:10:4:[84.3,114.6,113.6,235.3,113.6,112.6,214.3]:TopTopTopTop: big_r(f5(c4),f6(x0)),big_r(c2,c1),big_p(x1),big_r(c4,x1),big_r(x2,c1),big_p(x3),big_r(x0,x3),big_r(c4,f1(c4)),big_p(f2(c2)) -> big_r(x2,f1(x2)) {x0 -> c4, x1 -> c3, x2 -> c2, x3 -> c3}
% 7.27/2.02 === Backtracking. Learning clause 259:6:1:[174.1,257.1,256.5,258.2,250.2,72.5,232.6]:Top: big_r(c4,f1(c4)),big_r(c4,f5(c4)),big_p(x0),big_r(c4,x0),big_p(f2(c2)) -> big_r(c2,f1(c2))
% 7.27/2.02 === Backtracking. Learning clause 260:2:0:[84.3,120.6,119.6,235.3,214.3,72.5,232.6,119.6,196.3,174.2,256.6,247.3,243.3]:: big_p(f2(c2)),big_r(c4,f1(c4)) ->
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 263:3:0:[194.1,261.0,174.1,262.2,242.3,200.6,113.6,225.3,198.2]:: big_r(c4,f1(c4)) -> big_r(c2,f1(c2)),big_p(c3)
% 7.27/2.02 === Conflict found: 178:3:0:[55.2,175.0,165.1,176.1,137.1,177.2,163.1,112.6,114.6,113.6,67.3]:: -> big_p(f2(c4)),big_r(c2,f1(c2)),big_r(c4,c3) {}
% 7.27/2.02 === Backtracking. Learning clause 264:6:1:[178.1,60.2]:Top: big_p(c2),big_r(c4,x0),big_r(x0,f2(c4)) -> big_r(c2,f1(c2)),big_r(c4,c3),big_p(c1)
% 7.27/2.02 === Conflict found: 108:6:4:[37.0,24.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(f5(x3),f6(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 266:6:1:[198.2,265.0,108.5,60.2,264.5]:Top: big_p(c2),big_r(c4,x0),big_r(x0,f2(c4)) -> big_r(f5(c4),f6(c4)),big_r(c2,f1(c2)),big_p(c1)
% 7.27/2.02 === Backtracking. Learning clause 267:8:1:[84.3,114.6,113.6,178.1,112.6,112.4,266.6]:Top: big_r(c2,c1),big_p(c3),big_p(c2),big_r(c4,x0),big_r(x0,f2(c4)) -> big_p(f6(c4)),big_r(f5(c4),f6(c4)),big_r(c2,f1(c2))
% 7.27/2.02 === Backtracking. Learning clause 268:3:0:[55.2,159.1]:: big_p(c2) -> big_p(c1),big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 270:5:0:[174.1,269.1,79.4,159.1,114.6,113.6,112.6,268.2,118.2,267.5,263.3]:: big_r(c2,c1),big_r(c4,f1(c4)) -> big_p(f6(c4)),big_r(f5(c4),f6(c4)),big_r(c2,f1(c2))
% 7.27/2.02 === Backtracking. Learning clause 271:4:1:[60.2,166.2]:Top: big_p(c2),big_r(c4,x0),big_r(x0,f2(c4)) -> big_p(c1)
% 7.27/2.02 === Conflict found: 120:6:4:[37.0,36.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_r(f5(x3),f6(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 273:3:0:[174.1,272.0,120.1,198.3,268.3,271.3]:: big_r(c4,f1(c4)) -> big_r(f5(c4),f6(c4)),big_p(c1)
% 7.27/2.02 === Conflict found: 106:6:4:[37.0,22.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_p(f6(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 274:6:3:[106.5,260.1]:TopTopTop: big_p(x0),big_r(c2,x0),big_p(x1),big_r(x2,x1),big_r(c4,f1(c4)) -> big_p(f6(x2))
% 7.27/2.02 === Conflict found: 107:6:4:[37.0,23.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(x3,f5(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 275:5:1:[107.5,260.1,242.2,200.6]:Top: big_r(c4,f1(c4)),big_p(f6(c2)),big_p(x0),big_r(c2,x0) -> big_p(c3)
% 7.27/2.02 === Conflict found: 108:6:4:[37.0,24.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(f5(x3),f6(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 276:6:3:[108.5,260.1]:TopTopTop: big_p(x0),big_r(c2,x0),big_p(x1),big_r(x2,x1),big_r(c4,f1(c4)) -> big_r(f5(x2),f6(x2))
% 7.27/2.02 === Backtracking. Learning clause 277:5:3:[84.4,163.4]:TopTopTop: big_r(c4,x0),big_r(x0,f2(c4)),big_p(x1),big_r(c2,x2),big_r(x2,x1) ->
% 7.27/2.02 === Conflict found: 107:6:4:[37.0,23.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(x3,f5(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 278:8:4:[107.5,260.1,277.4,274.6]:TopTopTopTop: big_r(c4,x0),big_r(x0,f2(c4)),big_r(f5(c2),f6(x1)),big_p(x2),big_r(c2,x2),big_p(x3),big_r(x1,x3),big_r(c4,f1(c4)) ->
% 7.27/2.02 === Backtracking. Learning clause 279:9:3:[79.4,159.1,120.2,275.5]:TopTopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0),big_r(c4,f1(c4)),big_p(f6(c2)),big_p(x2),big_r(c2,x2) -> big_r(f1(c4),f2(c4)),big_r(f5(c4),f6(c4))
% 7.27/2.02 === Conflict found: 107:6:4:[37.0,23.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(x3,f5(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 280:3:0:[107.5,260.1,279.2,274.6,278.2,276.6,273.3]:: big_r(c2,c1),big_r(c4,f1(c4)) -> big_r(f5(c4),f6(c4))
% 7.27/2.02 === Backtracking. Learning clause 281:3:0:[54.1,174.2,159.1]:: big_r(c4,f1(c4)) -> big_p(c1),big_p(c3)
% 7.27/2.02 === Backtracking. Learning clause 282:3:0:[55.1,174.2,159.1]:: big_r(c4,f1(c4)) -> big_p(c1),big_r(c4,c3)
% 7.27/2.02 === Conflict found: 271:4:1:[60.2,166.2]:Top: big_p(c2),big_r(c4,x0),big_r(x0,f2(c4)) -> big_p(c1) {x0 -> f1(c4)}
% 7.27/2.02 === Backtracking. Learning clause 283:4:1:[271.1,174.2]:Top: big_r(c4,x0),big_r(x0,f2(c4)),big_r(c4,f1(c4)) -> big_p(c1)
% 7.27/2.02 === Conflict found: 276:6:3:[108.5,260.1]:TopTopTop: big_p(x0),big_r(c2,x0),big_p(x1),big_r(x2,x1),big_r(c4,f1(c4)) -> big_r(f5(x2),f6(x2)) {x0 -> c1, x1 -> c1, x2 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 284:4:1:[276.6,278.3,283.4]:Top: big_r(c2,c1),big_r(c4,x0),big_r(x0,f2(c4)),big_r(c4,f1(c4)) ->
% 7.27/2.02 === Conflict found: 118:6:4:[37.0,34.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_p(f6(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 285:4:0:[118.1,281.3,282.3]:: big_r(c4,f1(c4)) -> big_r(f1(c4),f2(c4)),big_p(f6(c4)),big_p(c1)
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 286:8:4:[242.1,274.6]:TopTopTopTop: big_r(c2,x0),big_r(x0,f6(x1)),big_p(x2),big_r(c2,x2),big_p(x3),big_r(x1,x3),big_r(c4,f1(c4)) -> big_p(c3)
% 7.27/2.02 === Conflict found: 275:5:1:[107.5,260.1,242.2,200.6]:Top: big_r(c4,f1(c4)),big_p(f6(c2)),big_p(x0),big_r(c2,x0) -> big_p(c3) {x0 -> c1}
% 7.27/2.02 === Backtracking. Learning clause 287:4:1:[275.2,274.6]:Top: big_p(x0),big_r(c2,x0),big_r(c4,f1(c4)) -> big_p(c3)
% 7.27/2.02 === Backtracking. Learning clause 289:7:3:[274.5,288.0,79.4,159.1,276.6]:TopTopTop: big_r(c2,f5(x0)),big_p(x1),big_r(c2,x1),big_p(x2),big_r(x0,x2),big_r(c4,f1(c4)) -> big_r(c4,c3)
% 7.27/2.02 === Conflict found: 107:6:4:[37.0,23.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(x3,f5(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 290:3:0:[107.5,260.1,289.1,118.2,287.4,285.4,284.3]:: big_r(c2,c1),big_r(c4,f1(c4)) -> big_p(f6(c4))
% 7.27/2.02 === Conflict found: 283:4:1:[271.1,174.2]:Top: big_r(c4,x0),big_r(x0,f2(c4)),big_r(c4,f1(c4)) -> big_p(c1) {x0 -> f1(c4)}
% 7.27/2.02 === Backtracking. Learning clause 291:3:0:[283.2,285.2]:: big_r(c4,f1(c4)) -> big_p(f6(c4)),big_p(c1)
% 7.27/2.02 === Backtracking. Learning clause 292:3:0:[67.3,290.1,174.2,159.1]:: big_r(c4,f1(c4)) -> big_r(c4,c3),big_p(f6(c4))
% 7.27/2.02 === Backtracking. Learning clause 293:3:0:[66.3,290.1,174.2,159.1]:: big_r(c4,f1(c4)) -> big_p(c3),big_p(f6(c4))
% 7.27/2.02 === Conflict found: 252:8:4:[106.4,251.0,72.4,118.5,174.2]:TopTopTopTop: big_r(c4,f1(x0)),big_p(x1),big_r(x0,x1),big_p(x2),big_r(x3,x2),big_r(c4,f1(c4)) -> big_r(c2,c1),big_p(f6(x3)) {x0 -> c4, x1 -> c3, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 294:2:0:[252.7,290.1,292.2,293.2]:: big_r(c4,f1(c4)) -> big_p(f6(c4))
% 7.27/2.02 === Conflict found: 287:4:1:[275.2,274.6]:Top: big_p(x0),big_r(c2,x0),big_r(c4,f1(c4)) -> big_p(c3) {x0 -> c1}
% 7.27/2.02 === Backtracking. Learning clause 295:2:0:[287.2,217.2,281.2]:: big_r(c4,f1(c4)) -> big_p(c3)
% 7.27/2.02 === Backtracking. Learning clause 297:2:0:[281.2,296.0,60.3,119.6,273.2,294.2,174.2,283.2,282.3]:: big_r(c4,f1(c4)) -> big_p(c1)
% 7.27/2.02 === Conflict found: 107:6:4:[37.0,23.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(x3,f5(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 299:2:0:[282.1,298.0,107.5,260.1,289.1,216.2]:: big_r(c4,f1(c4)) -> big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 300:6:2:[84.5,119.6,276.6,294.2,276.6,274.6,119.6,284.3]:TopTop: big_p(x0),big_r(c4,x0),big_p(x1),big_r(c2,x1),big_r(c2,c1),big_r(c4,f1(c4)) ->
% 7.27/2.02 === Backtracking. Learning clause 301:8:4:[72.2,233.7,174.2]:TopTopTopTop: big_r(c4,x0),big_r(x0,f2(x1)),big_p(x2),big_r(x1,x2),big_p(x3),big_r(c4,x3),big_r(c4,f1(c4)) -> big_r(c2,c1)
% 7.27/2.02 === Backtracking. Learning clause 302:1:0:[72.3,119.6,120.6,294.2,174.2,301.2,300.4,295.2,297.2,299.2]:: big_r(c4,f1(c4)) ->
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f4(c2), x1 -> f3(c2)}
% 7.27/2.02 === Backtracking. Learning clause 305:3:0:[126.1,303.1,204.1,304.4,242.1,97.4,98.4,99.4,79.3,161.2]:: big_p(f2(c2)) -> big_p(c3),big_r(c4,c3)
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f4(c2), x1 -> f3(c2)}
% 7.27/2.02 === Backtracking. Learning clause 306:3:0:[242.1,85.4,86.4,87.4,305.1]:: -> big_p(c2),big_p(c3),big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 308:2:0:[211.1,307.2,79.1,97.4,98.4,99.4,79.3,161.2,159.1]:: big_p(f2(c2)) -> big_r(c4,c3)
% 7.27/2.02 === Conflict found: 198:3:0:[54.2,159.1]:: big_p(c2) -> big_p(c1),big_p(c3) {}
% 7.27/2.02 === Backtracking. Learning clause 309:3:0:[198.1,306.1]:: -> big_p(c1),big_p(c3),big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 310:2:0:[78.3,200.6,106.6,159.1,107.6,308.1,195.2,306.1,309.1]:: -> big_p(c3),big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 311:2:0:[79.1,85.4,86.4,87.4,159.1,308.1,268.1]:: -> big_p(c1),big_r(c4,c3)
% 7.27/2.02 === Backtracking. Learning clause 313:5:2:[154.2,312.0,79.3,90.5,88.5,89.5]:TopTop: big_p(x0),big_r(c2,x0) -> big_r(c4,c3),big_p(x1),big_p(f2(x1))
% 7.27/2.02 === Backtracking. Learning clause 314:4:1:[79.1,85.4,86.4,87.4,159.1]:Top: -> big_r(c4,c3),big_p(x0),big_p(f2(x0)),big_p(c2)
% 7.27/2.02 === Backtracking. Learning clause 315:1:0:[79.3,108.6,106.6,159.1,107.6,195.2,314.2,308.1,311.1]:: -> big_r(c4,c3)
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f2(c2), x1 -> f1(c2)}
% 7.27/2.02 === Backtracking. Learning clause 317:4:1:[86.1,316.0,242.3,98.2,161.2]:Top: -> big_p(c3),big_p(x0),big_r(x0,f3(x0)),big_p(c2)
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f4(c2), x1 -> f3(c2)}
% 7.27/2.02 === Backtracking. Learning clause 318:3:0:[242.1,97.4,99.4,242.3,161.2,317.3]:: big_p(f2(c2)) -> big_p(c3),big_p(c2)
% 7.27/2.02 === Conflict found: 110:5:3:[37.0,26.2]:TopTopTop: big_p(x0),big_r(x1,x0) -> big_r(x1,f1(x1)),big_p(x2),big_r(x2,f3(x2)) {x0 -> c3, x1 -> c4, x2 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 319:4:2:[110.3,302.1]:TopTop: big_p(x0),big_r(c4,x0) -> big_p(x1),big_r(x1,f3(x1))
% 7.27/2.02 === Conflict found: 113:6:4:[37.0,29.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(x3,f5(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 320:6:3:[113.5,302.1,84.5,232.6,256.6]:TopTopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0),big_p(x2),big_r(c4,x2),big_p(f2(c2)) ->
% 7.27/2.02 === Conflict found: 320:6:3:[113.5,302.1,84.5,232.6,256.6]:TopTopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0),big_p(x2),big_r(c4,x2),big_p(f2(c2)) -> {x0 -> f2(c2), x1 -> f1(c2), x2 -> c3}
% 7.27/2.02 === Backtracking. Learning clause 321:7:2:[320.3,99.2,161.2,320.3]:TopTop: big_p(f4(x0)),big_r(c2,f3(x0)),big_p(x1),big_r(c4,x1),big_p(f2(c2)) -> big_p(x0),big_p(c2)
% 7.27/2.02 === Conflict found: 320:6:3:[113.5,302.1,84.5,232.6,256.6]:TopTopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0),big_p(x2),big_r(c4,x2),big_p(f2(c2)) -> {x0 -> f2(c2), x1 -> f1(c2), x2 -> c3}
% 7.27/2.02 === Backtracking. Learning clause 323:2:0:[308.1,322.0,320.3,97.2,161.2,321.1,319.4,318.2]:: big_p(f2(c2)) -> big_p(c2)
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f4(c2), x1 -> f3(c2)}
% 7.27/2.02 === Backtracking. Learning clause 325:5:2:[85.3,324.0,242.3,87.4]:TopTop: big_r(c2,f3(x0)) -> big_p(c3),big_p(x1),big_p(f2(x1)),big_p(x0)
% 7.27/2.02 === Backtracking. Learning clause 326:1:0:[84.5,89.5,90.5,88.5,315.1,87.4,325.2,86.4,85.4,323.1]:: -> big_p(c2)
% 7.27/2.02 === Backtracking. Learning clause 328:6:3:[159.0,327.0,78.3,200.6,112.6,113.6]:TopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(c2,x2) -> big_p(c3),big_r(x1,f1(x1))
% 7.27/2.02 === Conflict found: 118:6:4:[37.0,34.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(f1(x1),f2(x1)),big_p(f6(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 330:9:5:[159.0,329.8,118.5,242.3,78.1]:TopTopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2),big_p(f2(x1)),big_r(c2,f1(x1)),big_r(c2,x4),big_r(x4,f6(x3)) -> big_p(c3)
% 7.27/2.02 === Conflict found: 330:9:5:[159.0,329.8,118.5,242.3,78.1]:TopTopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2),big_p(f2(x1)),big_r(c2,f1(x1)),big_r(c2,x4),big_r(x4,f6(x3)) -> big_p(c3) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2, x4 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 333:2:0:[198.1,331.1,318.2,332.2,330.8,200.6,119.6,242.3,328.6,194.2]:: big_p(f2(c2)) -> big_p(c3)
% 7.27/2.02 === Conflict found: 328:6:3:[159.0,327.0,78.3,200.6,112.6,113.6]:TopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(c2,x2) -> big_p(c3),big_r(x1,f1(x1)) {x0 -> c1, x1 -> c2, x2 -> c1}
% 7.27/2.02 === Backtracking. Learning clause 336:3:1:[194.1,334.1,326.0,335.2,328.1,198.2]:Top: big_r(x0,c1) -> big_r(x0,f1(x0)),big_p(c3)
% 7.27/2.02 === Conflict found: 242:4:2:[78.4,159.1]:TopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0) -> big_p(c3) {x0 -> f6(c2), x1 -> f5(c2)}
% 7.27/2.02 === Backtracking. Learning clause 338:2:0:[333.0,337.1,242.1,106.6,200.6,198.2,194.2,326.1]:: big_r(c2,f5(c2)) -> big_p(c3)
% 7.27/2.02 === Conflict found: 107:6:4:[37.0,23.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_p(f2(x1)),big_r(x3,f5(x3)) {x0 -> c1, x1 -> c2, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 339:1:0:[107.2,194.2,333.1,198.2,326.1,338.1]:: -> big_p(c3)
% 7.27/2.02 === Conflict found: 113:6:4:[37.0,29.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(x3,f5(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 342:2:0:[323.1,340.0,333.1,341.1,113.5,302.1,60.3,232.6,256.6,315.1]:: big_p(f2(c2)) -> big_p(c1)
% 7.27/2.02 === Conflict found: 112:6:4:[37.0,28.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_p(f6(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 343:5:3:[112.5,302.1]:TopTopTop: big_p(x0),big_r(c4,x0),big_p(x1),big_r(x2,x1) -> big_p(f6(x2))
% 7.27/2.02 === Backtracking. Learning clause 346:1:0:[326.0,344.0,339.0,345.1,60.3,113.6,114.6,302.1,343.5,315.1]:: -> big_p(c1)
% 7.27/2.02 === Conflict found: 320:6:3:[113.5,302.1,84.5,232.6,256.6]:TopTopTop: big_p(x0),big_r(c2,x1),big_r(x1,x0),big_p(x2),big_r(c4,x2),big_p(f2(c2)) -> {x0 -> f6(c2), x1 -> f5(c2), x2 -> c3}
% 7.27/2.02 === Backtracking. Learning clause 347:6:3:[320.1,256.6,232.6]:TopTopTop: big_r(c2,f5(x0)),big_p(x1),big_r(c4,x1),big_p(x2),big_r(x0,x2),big_p(f2(c2)) ->
% 7.27/2.02 === Conflict found: 113:6:4:[37.0,29.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(x3,f5(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 351:2:0:[323.1,348.0,333.1,349.2,342.1,350.3,113.6,72.3,302.1,232.6,256.6,347.5,315.1]:: big_r(c2,f5(c2)),big_p(f2(c2)) ->
% 7.27/2.02 === Backtracking. Learning clause 353:6:4:[339.0,352.5,84.5,107.6,108.6,106.6,108.6,106.6,315.1]:TopTopTopTop: big_r(c2,f5(x0)),big_p(x1),big_r(x0,x1),big_p(x2),big_r(x3,x2) -> big_p(f2(x3))
% 7.27/2.02 === Conflict found: 114:6:4:[37.0,30.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(f5(x3),f6(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 354:5:3:[114.5,302.1]:TopTopTop: big_p(x0),big_r(c4,x0),big_p(x1),big_r(x2,x1) -> big_r(f5(x2),f6(x2))
% 7.27/2.02 === Conflict found: 113:6:4:[37.0,29.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(x3,f5(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 358:1:0:[326.0,355.0,338.1,356.1,346.0,357.2,113.6,72.3,302.1,343.5,354.5,315.1,353.3,351.2]:: big_r(c2,f5(c2)) ->
% 7.27/2.02 === Conflict found: 256:6:3:[174.1,254.4,112.4,255.5,118.5,196.3]:TopTopTop: big_p(x0),big_r(c4,x0),big_p(x1),big_r(x2,x1),big_p(f2(c2)) -> big_p(f6(x2)) {x0 -> c3, x1 -> c3, x2 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 360:3:1:[308.1,359.0,256.1,339.1]:Top: big_r(x0,c3),big_p(f2(c2)) -> big_p(f6(x0))
% 7.27/2.02 === Conflict found: 232:6:3:[174.1,230.4,114.4,231.5,120.5,196.3]:TopTopTop: big_p(x0),big_r(c4,x0),big_p(x1),big_r(x2,x1),big_p(f2(c2)) -> big_r(f5(x2),f6(x2)) {x0 -> c3, x1 -> c3, x2 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 362:3:1:[308.1,361.0,232.1,339.1]:Top: big_r(x0,c3),big_p(f2(c2)) -> big_r(f5(x0),f6(x0))
% 7.27/2.02 === Conflict found: 114:6:4:[37.0,30.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(f5(x3),f6(x3)) {x0 -> c3, x1 -> c4, x2 -> c3, x3 -> c4}
% 7.27/2.02 === Backtracking. Learning clause 363:4:2:[114.1,339.1]:TopTop: big_r(x0,c3),big_r(x1,c3) -> big_r(x0,f1(x0)),big_r(f5(x1),f6(x1))
% 7.27/2.02 === Conflict found: 113:6:4:[37.0,29.2]:TopTopTopTop: big_p(x0),big_r(x1,x0),big_p(x2),big_r(x3,x2) -> big_r(x1,f1(x1)),big_r(x3,f5(x3)) {x0 -> c3, x1 -> c4, x2 -> c1, x3 -> c2}
% 7.27/2.02 === Backtracking. Learning clause 364:1:0:[113.3,346.1,339.1,302.1,358.1,315.1]:: big_r(c2,c1) ->
% 7.27/2.02
% 7.27/2.02 SZS status Unsatisfiable
% 7.27/2.02
% 7.27/2.02 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.27/2.02
% 7.27/2.02 SPASS-SCL-FOL Statistics:
% 7.27/2.02 Number of learned clauses: 164
% 7.27/2.02 Number of propagations: 969
% 7.27/2.02 Number of decisions: 495
% 7.27/2.02 Number of resolutions: 642
% 7.27/2.02 Number of condensations: 62
% 7.27/2.02 Number of sub resolutions: 116
% 7.27/2.02 Number of input literals (deduplicated): 20
% 7.27/2.02 Number of grows: 1
% 7.27/2.02 Number of considered ground atoms: 110
% 7.27/2.02
% 7.27/2.02 Needed: 0:00:01.50
% 7.27/2.02
%------------------------------------------------------------------------------