%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN723+1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n023.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:40:12 PM UTC 2026
% Result : Theorem 15.30s 4.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN723+1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n023.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 13:48:24 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 15.30/4.31 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.30/4.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.30/4.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.30/4.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.30/4.31 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.30/4.31 Execution resolution_3 ended with status: unsatisfiable
% 15.30/4.31 Used heuristic: resolution_3
% 15.30/4.31
% 15.30/4.31 Input Clauses:
% 15.30/4.31
% 15.30/4.31 Predicates: p q r s ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14
% 15.30/4.31 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc10 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 skc22 skc24 skc26 skc28 skc30
% 15.30/4.31 Fol Functions: skf9 skf11 skf21 skf23 skf25 skf27 skf29
% 15.30/4.31 Problem Properties:
% 15.30/4.31 This is a full first-order problem without equality.
% 15.30/4.31
% 15.30/4.31 After reduction: Problem Properties:
% 15.30/4.31 This is a full first-order problem without equality.
% 15.30/4.31
% 15.30/4.31
% 15.30/4.31 Reduced Input Clauses:
% 15.30/4.31
% 15.30/4.31 Most General Atoms: ren1(x0,x1) p(x1) ren2 r(x0) ren3(x0,x1) q(x1) ren4 s(x0) ren5 ren6(x0,x1) ren7 ren8(x0,x1) ren9 ren10 ren11 ren12 ren13 ren14
% 15.30/4.31
% 15.30/4.31 === Starting SPASS-SCL-FOL A Little Less Naive, considering 53 atoms initially, heuristics mode: resolution_3 ===
% 15.30/4.31
% 15.30/4.31 === Backtracking. Learning clause 59:3:1:[34.2,33.3]:Top: ren9,p(x0) -> p(skc18)
% 15.30/4.31 === Backtracking. Learning clause 60:6:2:[13.3,25.2,5.3,33.3]:TopTop: ren4,ren7,ren2,ren9,p(x0) -> p(x1)
% 15.30/4.31 === Clause set with instances from active satisfied. Growing active. New size: 74
% 15.30/4.31 === Restarting.
% 15.30/4.31 === Backtracking. Learning clause 61:6:1:[3.3,57.1,60.6]:Top: ren14,ren4,ren7,ren2,ren9,p(x0) ->
% 15.30/4.31 === Backtracking. Learning clause 62:3:1:[6.2,5.3]:Top: ren2,q(x0) -> q(skc2)
% 15.30/4.31 === Backtracking. Learning clause 63:5:2:[13.3,25.2,5.3]:TopTop: ren4,ren7,ren2,q(x0) -> p(x1)
% 15.30/4.31 === Backtracking. Learning clause 64:4:2:[13.3,25.2]:TopTop: ren4,r(x0),ren7 -> p(x1)
% 15.30/4.31 === Backtracking. Learning clause 65:6:0:[4.3,57.1,61.6,61.6,55.3,51.3]:: ren4,ren7,ren9,ren2,ren5,ren12 ->
% 15.30/4.31 === Backtracking. Learning clause 66:5:1:[23.3,47.1,5.3,5.3,33.3]:Top: ren11,ren2,ren9,p(x0) -> ren12
% 15.30/4.31 === Backtracking. Learning clause 67:6:0:[24.3,47.1,64.2,64.2,66.4,65.6,43.3]:: ren4,ren9,ren2,ren5,ren7,ren10 ->
% 15.30/4.31 === Backtracking. Learning clause 68:5:1:[31.3,39.1,13.3,13.3,5.3,33.3]:Top: ren4,ren2,ren9,p(x0) -> ren10
% 15.30/4.31 === Backtracking. Learning clause 69:5:0:[32.3,39.1,25.2,25.2,68.4,67.6]:: ren4,ren9,ren2,ren5,ren7 ->
% 15.30/4.31 === Backtracking. Learning clause 70:5:0:[36.2,63.4]:: ren4,ren7,ren2 -> p(skc20),ren9
% 15.30/4.31 === Backtracking. Learning clause 71:3:1:[25.2,26.3]:Top: ren7,p(skc13) -> p(x0)
% 15.30/4.31 === Backtracking. Learning clause 72:3:0:[3.3,57.1,71.3]:: ren14,ren7,p(skc13) ->
% 15.30/4.31 === Backtracking. Learning clause 73:3:1:[3.3,57.1]:Top: p(x0),p(skf29(x0)),ren14 ->
% 15.30/4.31 === Backtracking. Learning clause 74:6:0:[32.3,37.2,25.2,25.2,72.3,55.3,51.3]:: ren10,ren7,ren2,ren5,ren12 -> ren9
% 15.30/4.31 === Backtracking. Learning clause 75:4:1:[23.3,47.1,5.3,5.3]:Top: ren11,ren2,q(x0) -> ren12
% 15.30/4.31 === Backtracking. Learning clause 76:3:1:[14.2,13.3]:Top: ren4,r(x0) -> r(skc6)
% 15.30/4.31 === Backtracking. Learning clause 77:4:1:[31.3,37.2,13.3,13.3]:Top: ren10,ren4,r(x0) -> ren9
% 15.30/4.31 === Backtracking. Learning clause 79:5:0:[67.1,78.5,24.3,47.1,77.3,77.3,74.5,43.3]:: ren4,ren2,ren5,ren7,ren10 ->
% 15.30/4.31 === Backtracking. Learning clause 80:6:0:[24.3,45.2,64.2,64.2,72.3,55.3,51.3]:: ren4,ren7,ren2,ren5,ren12 -> ren11
% 15.30/4.31 === Clause set with instances from active satisfied. Growing active. New size: 128
% 15.30/4.31 === Clause set with instances from active satisfied. Growing active. New size: 192
% 15.30/4.31 === Backtracking. Learning clause 81:4:1:[9.1,18.3]:Top: q(skc10),ren5,ren4 -> q(x0)
% 15.30/4.31 === Backtracking. Learning clause 82:4:2:[10.1,18.3,81.1]:TopTop: q(x0),ren5,ren4 -> q(x1)
% 15.30/4.31 === Conflict found: 82:4:2:[10.1,18.3,81.1]:TopTop: q(x0),ren5,ren4 -> q(x1) {x0 -> skc5, x1 -> skc19}
% 15.30/4.31 === Backtracking. Learning clause 83:5:2:[82.4,35.2,82.4]:TopTop: p(x0),q(x1),ren5,ren4 -> ren9
% 15.30/4.31 === Backtracking. Learning clause 84:6:1:[6.3,83.2]:Top: ren2,r(skc1),p(x0),ren5,ren4 -> ren9
% 15.30/4.31 === Clause set with instances from active satisfied. Growing active. New size: 256
% 15.30/4.31 === Clause set with instances from active satisfied. Growing active. New size: 320
% 15.30/4.31 === Backtracking. Learning clause 85:5:0:[22.1,48.1,14.3]:: ren4,s(skc5) -> r(skc28),ren11,ren12
% 15.30/4.31 === Clause set with instances from active satisfied. Growing active. New size: 384
% 15.30/4.31 === Backtracking. Learning clause 86:7:2:[29.1,40.1,85.2,21.2,48.1,30.3,40.1]:TopTop: ren4,s(x0) -> r(x1),ren11,ren12,ren9,ren10
% 15.30/4.31 === Backtracking. Learning clause 88:7:1:[44.0,87.0,26.3,86.2]:Top: p(skc13),ren4 -> r(x0),ren11,ren12,ren9,ren10
% 15.30/4.31 === Backtracking. Learning clause 89:4:3:[2.3,1.2,58.1,58.1,1.3]:TopTopTop: ren1(x0,x1),p(x0) -> p(x2),ren14
% 15.30/4.31 === Conflict found: 89:4:3:[2.3,1.2,58.1,58.1,1.3]:TopTopTop: ren1(x0,x1),p(x0) -> p(x2),ren14 {x0 -> skc1, x1 -> skc1, x2 -> skc30}
% 15.30/4.31 === Backtracking. Learning clause 91:8:1:[68.2,90.8,89.1,3.3,89.2,58.1,3.2,89.1,88.1,84.2]:Top: ren2,p(x0),ren5,ren4 -> ren14,ren11,ren12,ren10
% 15.30/4.31 === Conflict found: 91:8:1:[68.2,90.8,89.1,3.3,89.2,58.1,3.2,89.1,88.1,84.2]:Top: ren2,p(x0),ren5,ren4 -> ren14,ren11,ren12,ren10 {x0 -> skc20}
% 15.30/4.31 === Backtracking. Learning clause 92:4:0:[91.2,70.4,53.1,49.1,80.5,41.1,79.5,69.2]:: ren4,ren2,ren5,ren7 ->
% 15.30/4.31 === Backtracking. Learning clause 93:6:1:[23.2,5.3,45.2,42.1,92.4,68.5,33.3,84.6]:Top: ren12,ren2,r(skc1),p(x0),ren5,ren4 ->
% 15.30/4.31 === Backtracking. Learning clause 94:6:2:[1.3,27.2,58.1,2.3,58.1,53.1,49.1,92.4]:TopTop: s(x0),p(x1),ren4,ren2,ren5 -> ren12
% 15.30/4.31 === Conflict found: 94:6:2:[1.3,27.2,58.1,2.3,58.1,53.1,49.1,92.4]:TopTop: s(x0),p(x1),ren4,ren2,ren5 -> ren12 {x0 -> skc1, x1 -> skf29(skc1)}
% 15.30/4.31 === Backtracking. Learning clause 96:5:1:[13.2,95.0,94.6,93.1]:Top: ren2,r(skc1),p(x0),ren5,ren4 ->
% 15.30/4.31 === Backtracking. Learning clause 98:5:0:[96.2,97.5,4.1,96.3,57.1,55.3,51.3]:: r(skc1),ren4,ren2,ren5,ren12 ->
% 15.30/4.31 === Backtracking. Learning clause 100:5:1:[5.2,99.3,34.2,82.4,96.3]:Top: ren9,q(x0),ren2,ren5,ren4 ->
% 15.30/4.31 === Conflict found: 82:4:2:[10.1,18.3,81.1]:TopTop: q(x0),ren5,ren4 -> q(x1) {x0 -> skc2, x1 -> skc17}
% 15.30/4.31 === Backtracking. Learning clause 101:5:0:[82.1,6.3,100.2,77.4]:: r(skc1),ren2,ren5,ren10,ren4 ->
% 15.30/4.31 === Conflict found: 75:4:1:[23.3,47.1,5.3,5.3]:Top: ren11,ren2,q(x0) -> ren12 {x0 -> skc17}
% 15.30/4.31 === Backtracking. Learning clause 103:6:1:[92.3,102.5,75.1,44.3,82.4]:Top: ren2,q(x0),ren5,ren4 -> ren12,ren10
% 15.30/4.31 === Conflict found: 82:4:2:[10.1,18.3,81.1]:TopTop: q(x0),ren5,ren4 -> q(x1) {x0 -> skc2, x1 -> skc17}
% 15.30/4.31 === Backtracking. Learning clause 104:4:0:[82.1,6.3,103.2,101.4,98.5]:: r(skc1),ren4,ren2,ren5 ->
% 15.30/4.31 === Backtracking. Learning clause 106:7:2:[5.1,105.7,24.3,45.2,77.3,42.1,92.4,33.1]:TopTop: ren12,ren10,ren4,ren2,ren5,p(x0) -> r(x1)
% 15.30/4.31 === Backtracking. Learning clause 107:5:2:[22.3,21.2,46.3,46.3,76.3]:TopTop: ren12,ren11,ren4,r(x0) -> r(x1)
% 15.30/4.31 === Clause set with instances from active satisfied. Growing active. New size: 448
% 15.30/4.31 === Backtracking. Learning clause 108:4:1:[30.1,40.1]:Top: s(x0) -> s(skc24),ren9,ren10
% 15.30/4.31 === Conflict found: 108:4:1:[30.1,40.1]:Top: s(x0) -> s(skc24),ren9,ren10 {x0 -> skc16}
% 15.30/4.31 === Backtracking. Learning clause 110:7:2:[5.1,109.6,108.1,28.1,29.2,40.1,14.2,107.4,73.1,44.3,92.4,33.1,106.2]:TopTop: p(skf29(x0)),ren14,ren12,ren4,ren2,ren5 -> r(x1)
% 15.30/4.31 === Backtracking. Learning clause 112:7:1:[106.5,111.6,4.3,57.1,106.6]:Top: ren14,ren12,ren10,ren4,ren2,ren5 -> r(x0)
% 15.30/4.31 === Conflict found: 108:4:1:[30.1,40.1]:Top: s(x0) -> s(skc24),ren9,ren10 {x0 -> skc16}
% 15.30/4.31 === Backtracking. Learning clause 114:5:1:[5.1,113.4,108.1,28.1,29.2,40.1,14.2,107.4,33.1,4.1,57.1,44.3,92.4,110.1,112.3,55.3,51.3]:Top: ren4,ren2,ren5,ren12 -> r(x0)
% 15.30/4.31 === Backtracking. Learning clause 115:4:2:[33.3,5.2]:TopTop: ren9,p(x0),ren2 -> r(x1)
% 15.30/4.31 === Backtracking. Learning clause 117:6:2:[106.0,116.5,32.2,94.1,37.2,94.1,115.1]:TopTop: ren10,ren4,ren5,p(x0),ren2 -> r(x1)
% 15.30/4.31 === Backtracking. Learning clause 118:4:2:[30.1,38.3,29.2,38.3]:TopTop: s(x0),ren10,ren9 -> s(x1)
% 15.30/4.31 === Conflict found: 118:4:2:[30.1,38.3,29.2,38.3]:TopTop: s(x0),ren10,ren9 -> s(x1) {x0 -> skc16, x1 -> skc24}
% 15.30/4.31 === Backtracking. Learning clause 119:6:1:[118.1,28.1,118.1,14.2]:Top: ren10,ren9,ren4 -> p(x0),ren7,r(skc6)
% 15.30/4.31 === Backtracking. Learning clause 121:6:1:[115.1,120.6,21.1,48.1,85.3,13.3,114.4,119.6,42.1,92.4]:Top: ren9,ren10,ren4,ren2,ren5 -> r(x0)
% 15.30/4.31 === Backtracking. Learning clause 122:5:1:[36.1,117.4,5.2,121.1]:Top: ren10,ren4,ren2,ren5 -> r(x0)
% 15.30/4.31 === Backtracking. Learning clause 123:4:0:[24.2,76.2,47.1]:: ren4,ren11 -> r(skc6),ren12
% 15.30/4.31 === Backtracking. Learning clause 124:5:1:[31.2,13.3,39.1,13.3,123.3,114.4,44.3,92.4,122.1]:Top: ren9,ren4,ren2,ren5 -> r(x0)
% 15.30/4.31 === Conflict found: 123:4:0:[24.2,76.2,47.1]:: ren4,ren11 -> r(skc6),ren12 {}
% 15.30/4.31 === Backtracking. Learning clause 126:4:0:[122.0,125.4,123.4,114.4,44.3,92.4]:: ren4,ren2,ren5 -> r(skc6)
% 15.30/4.31 === Backtracking. Learning clause 127:5:1:[33.3,100.2]:Top: p(x0),ren9,ren2,ren5,ren4 ->
% 15.30/4.31 === Backtracking. Learning clause 128:6:1:[55.3,57.2,51.3,4.3,127.1]:Top: ren12,ren9,ren2,ren5,ren4 -> p(skf29(x0))
% 15.30/4.31 === Conflict found: 121:6:1:[115.1,120.6,21.1,48.1,85.3,13.3,114.4,119.6,42.1,92.4]:Top: ren9,ren10,ren4,ren2,ren5 -> r(x0) {x0 -> skc1}
% 15.30/4.31 === Backtracking. Learning clause 129:5:0:[121.6,104.1]:: ren9,ren10,ren4,ren2,ren5 ->
% 15.30/4.31 === Conflict found: 128:6:1:[55.3,57.2,51.3,4.3,127.1]:Top: ren12,ren9,ren2,ren5,ren4 -> p(skf29(x0)) {x0 -> skc1}
% 15.30/4.31 === Backtracking. Learning clause 130:5:0:[128.6,127.1]:: ren12,ren9,ren2,ren5,ren4 ->
% 15.30/4.31 === Conflict found: 124:5:1:[31.2,13.3,39.1,13.3,123.3,114.4,44.3,92.4,122.1]:Top: ren9,ren4,ren2,ren5 -> r(x0) {x0 -> skc1}
% 15.30/4.31 === Backtracking. Learning clause 131:4:0:[124.5,104.1]:: ren9,ren4,ren2,ren5 ->
% 15.30/4.31 === Conflict found: 107:5:2:[22.3,21.2,46.3,46.3,76.3]:TopTop: ren12,ren11,ren4,r(x0) -> r(x1) {x0 -> skc6, x1 -> skc1}
% 15.30/4.31 === Backtracking. Learning clause 133:5:0:[114.4,132.1,107.5,104.1,44.3,92.4]:: ren12,ren4,ren2,ren5 -> ren10
% 15.30/4.31 === Conflict found: 94:6:2:[1.3,27.2,58.1,2.3,58.1,53.1,49.1,92.4]:TopTop: s(x0),p(x1),ren4,ren2,ren5 -> ren12 {x0 -> skc5, x1 -> skf29(skc1)}
% 15.30/4.31 === Backtracking. Learning clause 134:6:2:[94.1,13.3]:TopTop: p(x0),ren2,ren5,ren4,r(x1) -> ren12
% 15.30/4.31 === Backtracking. Learning clause 135:3:0:[36.1,134.1,103.2,133.1,77.1,126.4,131.1]:: ren4,ren2,ren5 ->
% 15.30/4.31 === Backtracking. Learning clause 136:3:3:[12.2,5.2,5.2]:TopTopTop: ren2 -> ren3(x0,x1),r(x2)
% 15.30/4.31 === Backtracking. Learning clause 137:3:1:[19.1,136.2,135.3]:Top: ren4,ren2 -> r(x0)
% 15.30/4.31 === Backtracking. Learning clause 138:4:1:[11.2,33.3,19.1,33.3,135.3]:Top: ren9,p(x0),ren4,ren2 ->
% 15.30/4.31 === Backtracking. Learning clause 139:5:0:[23.3,45.2,137.3,137.3,42.1]:: ren12,ren4,ren2,ren10 -> ren7
% 15.30/4.31 === Backtracking. Learning clause 141:4:0:[137.2,140.1,31.2,13.3,39.1,13.3,139.4,64.3,138.2]:: ren12,ren9,ren4,ren2 ->
% 15.30/4.31 === Conflict found: 89:4:3:[2.3,1.2,58.1,58.1,1.3]:TopTopTop: ren1(x0,x1),p(x0) -> p(x2),ren14 {x0 -> skc1, x1 -> skf29(skc1), x2 -> skc15}
% 15.30/4.31 === Backtracking. Learning clause 142:4:2:[89.3,27.2,3.3]:TopTop: s(x0),p(x1) -> ren14,ren7
% 15.30/4.31 === Conflict found: 73:3:1:[3.3,57.1]:Top: p(x0),p(skf29(x0)),ren14 -> {x0 -> skc1}
% 15.30/4.31 === Backtracking. Learning clause 143:4:2:[73.3,142.3]:TopTop: p(x0),p(skf29(x0)),s(x1) -> ren7
% 15.30/4.31 === Backtracking. Learning clause 145:6:1:[137.2,144.2,53.3,50.1,142.3,13.3,135.3,41.2]:Top: ren12,p(x0),ren4,ren2,ren11 -> ren10
% 15.30/4.31 === Backtracking. Learning clause 146:5:1:[23.3,45.2,137.3,137.3,145.5]:Top: ren12,p(x0),ren4,ren2 -> ren10
% 15.30/4.31 === Backtracking. Learning clause 148:3:0:[137.2,147.0,11.3,19.1,36.2,36.2,146.2,135.3,77.1,141.2]:: ren12,ren4,ren2 ->
% 15.30/4.31 === Conflict found: 64:4:2:[13.3,25.2]:TopTop: ren4,r(x0),ren7 -> p(x1) {x0 -> skc1, x1 -> skf29(skc1)}
% 15.30/4.31 === Backtracking. Learning clause 149:5:1:[64.2,137.3,42.3]:Top: ren4,ren2,ren11,ren10 -> p(x0)
% 15.30/4.31 === Backtracking. Learning clause 151:3:0:[141.0,150.3,55.2,52.3,57.2,4.3,138.2,135.3,138.2]:: ren9,ren4,ren2 ->
% 15.30/4.31 === Backtracking. Learning clause 152:3:0:[12.2,75.3,19.1,75.3,135.3,148.1]:: ren11,ren4,ren2 ->
% 15.30/4.31 === Backtracking. Learning clause 157:3:1:[135.2,153.3,148.0,154.4,152.0,155.5,138.0,156.6,55.2,52.3,73.3,64.4,44.1,77.1,137.3]:Top: p(skf29(x0)),ren4,ren2 ->
% 15.30/4.31 === Backtracking. Learning clause 158:2:0:[44.1,64.3,77.1,137.3,151.1,152.1,157.1]:: ren4,ren2 ->
% 15.30/4.31 === Backtracking. Learning clause 159:4:1:[11.3,17.2,33.3,33.3,158.1]:Top: ren5,ren9,p(x0),ren2 ->
% 15.30/4.31 === Backtracking. Learning clause 161:3:3:[33.2,160.0,11.1,33.3]:TopTopTop: ren9,p(x0) -> ren3(x1,x2)
% 15.30/4.31 === Conflict found: 118:4:2:[30.1,38.3,29.2,38.3]:TopTop: s(x0),ren10,ren9 -> s(x1) {x0 -> skc15, x1 -> skc7}
% 15.30/4.32 === Backtracking. Learning clause 162:5:2:[118.4,15.2,118.4]:TopTop: r(x0),s(x1),ren10,ren9 -> ren4
% 15.30/4.32 === Backtracking. Learning clause 164:6:1:[115.3,163.1,26.3,162.2,89.3,158.1,3.3]:Top: ren7,ren10,ren9,ren2,p(x0) -> ren14
% 15.30/4.32 === Conflict found: 73:3:1:[3.3,57.1]:Top: p(x0),p(skf29(x0)),ren14 -> {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 165:6:1:[73.3,164.6]:Top: p(x0),p(skf29(x0)),ren7,ren10,ren9,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 167:5:1:[43.2,166.0,50.1,53.3,66.5,164.6,159.1]:Top: ren7,ren10,ren9,p(x0),ren2 ->
% 15.30/4.32 === Conflict found: 136:3:3:[12.2,5.2,5.2]:TopTopTop: ren2 -> ren3(x0,x1),r(x2) {x0 -> skc1, x1 -> skf9(skc1), x2 -> skc6}
% 15.30/4.32 === Backtracking. Learning clause 169:3:1:[135.0,168.3,136.2,17.2]:Top: ren2,ren5 -> r(x0)
% 15.30/4.32 === Backtracking. Learning clause 171:5:0:[43.2,170.0,12.1,75.3,75.3,17.2,158.1,74.5]:: ren10,ren7,ren2,ren5 -> ren9
% 15.30/4.32 === Backtracking. Learning clause 172:3:1:[5.2,6.3]:Top: ren2,r(skc1) -> r(x0)
% 15.30/4.32 === Backtracking. Learning clause 173:5:2:[9.1,20.1,10.3,20.1,35.2]:TopTop: q(x0),p(x1) -> ren4,ren5,ren9
% 15.30/4.32 === Backtracking. Learning clause 174:7:2:[22.1,46.3,16.1,21.2,46.3,31.2,37.2]:TopTop: ren12,ren11,s(x0),ren10 -> ren4,r(x1),ren9
% 15.30/4.32 === Backtracking. Learning clause 175:6:1:[32.2,174.3,37.2,174.3]:Top: ren12,ren11,ren10 -> ren4,r(x0),ren9
% 15.30/4.32 === Backtracking. Learning clause 176:7:1:[6.3,173.1,175.5,158.1]:Top: p(x0),ren12,ren11,ren10,ren2 -> ren5,ren9
% 15.30/4.32 === Backtracking. Learning clause 178:5:1:[25.2,177.1,55.2,52.3,73.3,25.3]:Top: ren2,ren7,s(x0) -> ren5,ren12
% 15.30/4.32 === Backtracking. Learning clause 179:4:1:[32.2,178.3,37.2,178.3,176.2,171.4,167.3,42.3]:Top: p(x0),ren2,ren11,ren10 ->
% 15.30/4.32 === Backtracking. Learning clause 180:5:2:[29.1,40.1,108.2,15.2,158.1,169.3,179.4,159.2]:TopTop: s(x0),ren11,ren5,p(x1),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 181:5:2:[53.3,50.1,142.3,41.2,179.4,180.3]:TopTop: ren12,s(x0),ren11,p(x1),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 183:5:1:[179.3,182.5,28.1,181.2,73.1,55.3,51.3,41.2]:Top: p(skf29(x0)),ren2,ren5,ren12,ren11 ->
% 15.30/4.32 === Backtracking. Learning clause 186:5:2:[66.4,184.0,179.3,185.6,32.2,181.2,39.1]:TopTop: ren11,p(x0),ren2,ren9 -> s(x1)
% 15.30/4.32 === Backtracking. Learning clause 188:5:1:[158.0,187.3,6.3,173.1]:Top: ren2,r(skc1),p(x0) -> ren5,ren9
% 15.30/4.32 === Backtracking. Learning clause 189:4:1:[22.1,46.3,16.1,21.2,46.3,158.1,188.2,186.4,181.2,183.3]:Top: p(skf29(x0)),ren2,ren12,ren11 ->
% 15.30/4.32 === Conflict found: 75:4:1:[23.3,47.1,5.3,5.3]:Top: ren11,ren2,q(x0) -> ren12 {x0 -> skc2}
% 15.30/4.32 === Backtracking. Learning clause 190:4:1:[75.3,6.3,189.3,169.3]:Top: p(skf29(x0)),ren11,ren2,ren5 ->
% 15.30/4.32 === Backtracking. Learning clause 193:5:3:[181.0,191.5,115.0,192.6,24.2,15.1,47.1,29.3,40.1,108.2,158.1,179.4]:TopTopTop: s(x0),p(x1),ren2,ren11 -> r(x2)
% 15.30/4.32 === Backtracking. Learning clause 194:3:1:[28.1,193.1,73.1,55.3,52.3,41.2,179.4,188.2,66.3,189.3,190.4]:Top: p(skf29(x0)),ren11,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 196:4:1:[169.2,195.0,23.3,45.2,169.3,194.2]:Top: ren12,ren5,p(skf29(x0)),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 197:6:2:[53.3,49.1,142.3]:TopTop: ren2,ren5,s(x0),p(x1) -> ren12,ren7
% 15.30/4.32 === Backtracking. Learning clause 199:5:1:[159.1,198.5,32.2,197.3,37.2,197.3,171.2]:Top: p(x0),ren10,ren2,ren5 -> ren12
% 15.30/4.32 === Backtracking. Learning clause 200:5:2:[29.1,40.1,108.2,15.2,158.1,159.2,169.3]:TopTop: s(x0),p(x1),ren2,ren5 -> ren10
% 15.30/4.32 === Backtracking. Learning clause 201:6:1:[26.3,200.1,89.3,3.3]:Top: ren7,ren2,ren5,p(x0) -> ren10,ren14
% 15.30/4.32 === Backtracking. Learning clause 202:3:1:[44.3,194.2,201.1,53.1,49.1,199.2,196.1]:Top: ren5,p(skf29(x0)),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 204:5:2:[196.1,203.5,43.3,194.2,142.4,53.1,50.1]:TopTop: ren10,p(skf29(x0)),s(x1),ren2,ren12 ->
% 15.30/4.32 === Backtracking. Learning clause 205:4:0:[23.3,45.2,172.3]:: ren12,ren2,r(skc1) -> ren11
% 15.30/4.32 === Backtracking. Learning clause 206:4:2:[29.1,40.1,15.2,24.2,45.2,108.2,158.1,115.1,205.3,194.2,204.1]:TopTop: p(skf29(x0)),s(x1),ren2,ren12 ->
% 15.30/4.32 === Conflict found: 162:5:2:[118.4,15.2,118.4]:TopTop: r(x0),s(x1),ren10,ren9 -> ren4 {x0 -> skc1, x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 207:6:2:[162.5,158.1,188.5]:TopTop: s(x0),ren10,ren2,r(skc1),p(x1) -> ren5
% 15.30/4.32 === Backtracking. Learning clause 208:4:0:[16.1,15.1,31.2,37.2]:: s(skc7),ren10 -> ren4,ren9
% 15.30/4.32 === Backtracking. Learning clause 209:4:2:[22.1,48.1,21.2,48.1]:TopTop: r(x0) -> r(x1),ren11,ren12
% 15.30/4.32 === Backtracking. Learning clause 212:4:2:[204.4,210.4,202.0,211.5,16.1,209.1,208.1,194.2,158.1,115.1,207.4]:TopTop: p(skf29(x0)),s(x1),ren10,ren2 ->
% 15.30/4.32 === Conflict found: 178:5:1:[25.2,177.1,55.2,52.3,73.3,25.3]:Top: ren2,ren7,s(x0) -> ren5,ren12 {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 214:3:2:[202.0,213.3,178.2,44.1,206.4,194.2,212.3]:TopTop: p(skf29(x0)),s(x1),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 216:4:1:[179.2,215.4,28.1,214.2,73.1,55.3,52.3,202.1,43.1,205.1]:Top: p(skf29(x0)),ren10,ren2,r(skc1) ->
% 15.30/4.32 === Backtracking. Learning clause 217:3:1:[32.2,214.2,37.2,214.2,115.1,216.4]:Top: p(skf29(x0)),ren10,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 220:3:1:[214.1,218.3,217.1,219.4,32.2,214.2,39.1]:Top: p(skf29(x0)),ren2,ren9 ->
% 15.30/4.32 === Conflict found: 188:5:1:[158.0,187.3,6.3,173.1]:Top: ren2,r(skc1),p(x0) -> ren5,ren9 {x0 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 222:3:1:[220.2,221.3,188.4,202.1]:Top: r(skc1),p(skf29(x0)),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 223:4:1:[26.3,214.2,89.3,3.3]:Top: ren7,p(skf29(x0)),ren2 -> ren14
% 15.30/4.32 === Backtracking. Learning clause 225:4:1:[196.1,224.4,53.3,50.1,223.4]:Top: ren12,ren7,p(skf29(x0)),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 226:2:1:[16.1,209.1,214.2,158.1,225.1,44.1,194.2,217.2,222.1]:Top: p(skf29(x0)),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 227:5:0:[4.2,226.1,57.1,179.1,55.3,51.3]:: ren11,ren10,ren2,ren5,ren12 ->
% 15.30/4.32 === Backtracking. Learning clause 228:5:2:[9.1,20.1,11.1]:TopTop: q(skc12),q(x0) -> ren4,ren5,ren3(x1,x0)
% 15.30/4.32 === Conflict found: 228:5:2:[9.1,20.1,11.1]:TopTop: q(skc12),q(x0) -> ren4,ren5,ren3(x1,x0) {x0 -> skc10, x1 -> skc17}
% 15.30/4.32 === Backtracking. Learning clause 229:6:0:[228.5,10.1,9.3,10.3,20.1,34.2,179.1,20.1,6.3,158.1]:: ren9,ren11,ren10,r(skc1),ren2 -> ren5
% 15.30/4.32 === Backtracking. Learning clause 230:4:0:[32.2,25.2,37.2,25.2,179.1,42.3,229.1,227.4,205.4]:: ren10,ren12,ren2,r(skc1) ->
% 15.30/4.32 === Conflict found: 75:4:1:[23.3,47.1,5.3,5.3]:Top: ren11,ren2,q(x0) -> ren12 {x0 -> skc2}
% 15.30/4.32 === Backtracking. Learning clause 232:4:0:[230.1,231.4,75.3,6.3,43.3]:: ren2,r(skc1),ren7,ren10 ->
% 15.30/4.32 === Backtracking. Learning clause 235:6:0:[169.2,233.0,129.2,234.6,28.1,162.2,199.1]:: ren9,ren10,ren2,ren5 -> ren7,ren12
% 15.30/4.32 === Backtracking. Learning clause 236:5:1:[28.2,226.1,162.2,158.1]:Top: r(x0),ren10,ren9,ren2 -> ren7
% 15.30/4.32 === Backtracking. Learning clause 238:5:0:[135.0,237.5,11.1,36.2,36.2,199.1,17.2]:: ren10,ren2,ren5 -> ren9,ren12
% 15.30/4.32 === Backtracking. Learning clause 239:3:0:[4.3,57.1,226.1,55.3,52.3,188.3,238.3,236.3,232.3,230.2]:: ren10,ren2,r(skc1) ->
% 15.30/4.32 === Backtracking. Learning clause 241:4:0:[230.0,240.4,41.1,205.4]:: ren7,ren12,ren2,r(skc1) ->
% 15.30/4.32 === Backtracking. Learning clause 242:4:0:[4.3,57.1,226.1,55.3,51.3,159.3]:: ren12,ren5,ren9,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 244:4:0:[169.2,243.1,32.3,39.1,25.2,25.2,239.1,159.3]:: ren7,ren5,ren9,ren2 ->
% 15.30/4.32 === Conflict found: 75:4:1:[23.3,47.1,5.3,5.3]:Top: ren11,ren2,q(x0) -> ren12 {x0 -> skc2}
% 15.30/4.32 === Backtracking. Learning clause 246:3:0:[169.2,245.0,75.3,6.3,44.3,239.1,242.1,244.1]:: ren5,ren9,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 248:5:1:[199.1,247.5,53.3,49.1,201.6]:Top: ren7,ren2,ren5,p(x0) -> ren12
% 15.30/4.32 === Backtracking. Learning clause 251:3:0:[169.2,249.3,244.2,250.4,11.1,36.2,36.2,248.4,17.2,158.1,241.2]:: ren5,ren7,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 253:4:1:[251.1,252.4,28.1,180.1,226.1]:Top: ren11,ren5,p(x0),ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 255:3:0:[169.2,254.3,4.3,57.1,226.1,55.3,51.3,253.3,205.4]:: ren5,ren12,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 258:3:1:[169.2,256.0,251.1,257.4,44.2,239.1,253.1]:Top: ren5,p(x0),ren2 ->
% 15.30/4.32 === Conflict found: 75:4:1:[23.3,47.1,5.3,5.3]:Top: ren11,ren2,q(x0) -> ren12 {x0 -> skc2}
% 15.30/4.32 === Backtracking. Learning clause 260:2:0:[169.2,259.0,75.3,6.3,44.3,239.1,251.2,255.2]:: ren5,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 261:4:1:[41.3,179.4]:Top: ren7,p(x0),ren2,ren11 ->
% 15.30/4.32 === Conflict found: 115:4:2:[33.3,5.2]:TopTop: ren9,p(x0),ren2 -> r(x1) {x0 -> skc1, x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 262:5:1:[115.4,241.4]:Top: ren9,p(x0),ren7,ren12,ren2 ->
% 15.30/4.32 === Conflict found: 89:4:3:[2.3,1.2,58.1,58.1,1.3]:TopTopTop: ren1(x0,x1),p(x0) -> p(x2),ren14 {x0 -> skc1, x1 -> skc1, x2 -> skc30}
% 15.30/4.32 === Backtracking. Learning clause 263:3:1:[89.1,3.3,89.2,58.1,226.1,53.1,50.1,260.1]:Top: p(x0),ren12,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 265:4:0:[179.0,264.4,22.1,46.3,21.2,46.3,16.1,25.2,158.1,239.3,42.3]:: ren12,ren2,ren11,ren10 ->
% 15.30/4.32 === Backtracking. Learning clause 268:4:0:[141.2,266.4,242.1,267.5,10.1,228.5,9.3,10.3,20.1,34.2,263.1,20.1,6.3]:: ren9,ren12,ren2,r(skc1) ->
% 15.30/4.32 === Backtracking. Learning clause 269:7:2:[31.3,39.1,16.2,22.2,46.3,21.2,46.3]:TopTop: s(x0),ren9,ren12,ren11 -> ren10,ren4,r(x1)
% 15.30/4.32 === Backtracking. Learning clause 272:4:0:[265.3,270.4,141.2,271.5,22.1,46.3,21.2,46.3,16.1,269.1,268.4]:: ren11,ren9,ren12,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 274:4:1:[239.0,273.4,29.1,40.1,108.2,15.2,158.1,172.3]:Top: s(x0),ren2,r(skc1) -> ren9
% 15.30/4.32 === Conflict found: 274:4:1:[239.0,273.4,29.1,40.1,108.2,15.2,158.1,172.3]:Top: s(x0),ren2,r(skc1) -> ren9 {x0 -> skc16}
% 15.30/4.32 === Backtracking. Learning clause 275:5:1:[274.1,28.1]:Top: ren2,r(skc1) -> ren9,p(x0),ren7
% 15.30/4.32 === Backtracking. Learning clause 277:3:0:[263.0,276.3,36.1,263.1,5.2,275.2,272.2,41.2,265.4]:: ren12,ren2,ren11 ->
% 15.30/4.32 === Backtracking. Learning clause 280:5:1:[44.1,278.1,272.0,279.5,24.3,45.2,236.1]:Top: ren12,ren9,ren2 -> r(x0),ren7
% 15.30/4.32 === Backtracking. Learning clause 282:4:1:[265.2,281.4,36.1,263.1,5.2,280.2,43.1]:Top: ren12,ren2,ren10 -> r(x0)
% 15.30/4.32 === Backtracking. Learning clause 283:5:0:[32.3,39.1,25.2,25.2,263.1]:: ren9,ren7,ren12,ren2 -> ren10
% 15.30/4.32 === Backtracking. Learning clause 284:2:0:[36.1,263.1,5.2,283.1,44.1,282.3,205.3,277.3]:: ren12,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 285:3:0:[4.3,57.1,226.1,55.3,52.3,260.1,284.1,115.2,239.3]:: ren9,ren10,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 287:3:0:[285.1,286.3,32.2,178.3,39.1,178.3,260.1,284.1]:: ren9,ren7,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 288:2:0:[4.3,57.1,226.1,55.3,52.3,260.1,66.4,44.3,284.1,287.2,285.2]:: ren9,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 290:3:0:[284.0,289.3,4.3,57.1,226.1,55.3,52.3,260.1,261.2,43.3]:: ren2,ren7,ren10 ->
% 15.30/4.32 === Conflict found: 208:4:0:[16.1,15.1,31.2,37.2]:: s(skc7),ren10 -> ren4,ren9 {}
% 15.30/4.32 === Backtracking. Learning clause 293:2:0:[285.0,291.2,284.0,292.3,208.1,16.2,158.1,209.1,239.3,42.1,290.2]:: ren2,ren10 ->
% 15.30/4.32 === Backtracking. Learning clause 297:2:0:[284.0,294.2,260.0,295.3,288.0,296.4,4.3,57.1,226.1,55.3,52.3,188.3]:: ren2,r(skc1) ->
% 15.30/4.32 === Backtracking. Learning clause 299:2:0:[290.2,298.2,16.3,158.1,209.1,178.3,260.1,284.1,41.1,297.2]:: ren7,ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 301:4:2:[261.0,300.3,28.1,193.1,226.1]:TopTop: p(x0),ren11,ren2 -> r(x1)
% 15.30/4.32 === Backtracking. Learning clause 302:1:0:[57.1,4.3,55.3,52.3,226.1,260.1,284.1,301.1,44.3,293.2,297.2,299.1]:: ren2 ->
% 15.30/4.32 === Backtracking. Learning clause 303:7:3:[7.2,107.5,33.3,302.1,162.5]:TopTopTop: ren12,ren11,p(x0),r(x1),s(x2),ren10,ren9 ->
% 15.30/4.32 === Backtracking. Learning clause 304:7:2:[17.2,161.3,13.1,303.5]:TopTop: ren5,ren12,ren11,p(x0),r(x1),ren10,ren9 ->
% 15.30/4.32 === Backtracking. Learning clause 306:6:1:[265.1,305.4,7.2,175.5]:Top: q(x0),ren12,ren11,ren10 -> ren4,ren9
% 15.30/4.32 === Backtracking. Learning clause 307:6:2:[12.1,306.1,17.2,306.1,77.2,304.7]:TopTop: ren5,ren12,ren11,p(x0),r(x1),ren10 ->
% 15.30/4.32 === Backtracking. Learning clause 308:3:1:[56.1,302.1,73.3]:Top: p(x0),p(skf29(x0)) -> ren13
% 15.30/4.32 === Backtracking. Learning clause 309:5:2:[21.1,46.3,22.3,46.3,7.2,302.1,33.3]:TopTop: r(x0),ren12,ren11,ren9,p(x1) ->
% 15.30/4.32 === Conflict found: 308:3:1:[56.1,302.1,73.3]:Top: p(x0),p(skf29(x0)) -> ren13 {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 310:4:1:[308.3,50.1]:Top: p(x0),p(skf29(x0)),ren12 -> ren5
% 15.30/4.32 === Backtracking. Learning clause 312:5:2:[42.2,311.0,32.3,37.2,25.2,25.2,310.2,307.1,309.4]:TopTop: ren10,r(x0),ren12,ren11,p(x1) ->
% 15.30/4.32 === Backtracking. Learning clause 313:4:1:[49.1,308.3]:Top: ren5,p(x0),p(skf29(x0)) -> ren12
% 15.30/4.32 === Backtracking. Learning clause 314:6:3:[19.1,161.3,162.5]:TopTopTop: p(x0),r(x1),s(x2),ren10,ren9 -> ren5
% 15.30/4.32 === Backtracking. Learning clause 316:6:2:[42.2,315.0,26.3,314.3,89.3,3.3,73.3,313.1,312.3]:TopTop: ren9,p(x0),p(skf29(x0)),ren10,r(x1),ren11 ->
% 15.30/4.32 === Backtracking. Learning clause 317:6:3:[17.2,161.3,64.1]:TopTopTop: ren5,ren9,p(x0),r(x1),ren7 -> p(x2)
% 15.30/4.32 === Backtracking. Learning clause 318:2:0:[54.3,302.1]:: ren14,ren13 ->
% 15.30/4.32 === Conflict found: 89:4:3:[2.3,1.2,58.1,58.1,1.3]:TopTopTop: ren1(x0,x1),p(x0) -> p(x2),ren14 {x0 -> skc1, x1 -> skc1, x2 -> skc13}
% 15.30/4.32 === Backtracking. Learning clause 320:5:2:[42.2,319.0,89.1,3.3,71.2,318.1,52.3,312.3,317.1,316.3]:TopTop: ren9,p(x0),ren10,r(x1),ren11 ->
% 15.30/4.32 === Conflict found: 313:4:1:[49.1,308.3]:Top: ren5,p(x0),p(skf29(x0)) -> ren12 {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 321:6:2:[313.4,312.3]:TopTop: ren5,p(x0),p(skf29(x0)),ren10,r(x1),ren11 ->
% 15.30/4.32 === Backtracking. Learning clause 323:5:2:[42.2,322.0,32.3,37.2,25.2,25.2,320.1,321.3]:TopTop: ren5,p(x0),ren10,r(x1),ren11 ->
% 15.30/4.32 === Backtracking. Learning clause 325:4:2:[323.0,324.4,8.1,173.1,23.2,47.1,302.1,77.2,312.3,320.1]:TopTop: p(x0),ren10,r(x1),ren11 ->
% 15.30/4.32 === Conflict found: 77:4:1:[31.3,37.2,13.3,13.3]:Top: ren10,ren4,r(x0) -> ren9 {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 326:5:1:[77.1,41.3]:Top: ren4,r(x0),ren11,ren7 -> ren9
% 15.30/4.32 === Conflict found: 307:6:2:[12.1,306.1,17.2,306.1,77.2,304.7]:TopTop: ren5,ren12,ren11,p(x0),r(x1),ren10 -> {x0 -> skc1, x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 327:6:2:[307.6,41.3,313.4]:TopTop: r(x0),ren11,ren7,ren5,p(x1),p(skf29(x1)) ->
% 15.30/4.32 === Conflict found: 325:4:2:[323.0,324.4,8.1,173.1,23.2,47.1,302.1,77.2,312.3,320.1]:TopTop: p(x0),ren10,r(x1),ren11 -> {x0 -> skf29(skc1), x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 328:4:2:[325.2,41.3]:TopTop: p(x0),r(x1),ren11,ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 329:4:2:[43.3,328.3]:TopTop: ren10,p(x0),r(x1),ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 330:4:1:[31.2,13.3,39.1,13.3]:Top: ren9,ren4,r(x0) -> ren10
% 15.30/4.32 === Backtracking. Learning clause 331:5:2:[17.2,161.3,330.2]:TopTop: ren5,p(x0),ren9,r(x1) -> ren10
% 15.30/4.32 === Backtracking. Learning clause 333:6:1:[64.3,332.3,23.3,45.2,8.2,83.2,302.1,328.3]:Top: ren12,ren5,ren4,r(x0),ren7 -> ren9
% 15.30/4.32 === Backtracking. Learning clause 334:5:2:[29.1,40.1,108.2,15.2]:TopTop: s(x0),r(x1) -> ren9,ren10,ren4
% 15.30/4.32 === Backtracking. Learning clause 335:5:2:[26.3,334.1,89.3,3.3,73.3,333.3,331.3,329.1,313.4]:TopTop: r(x0),ren7,ren5,p(x1),p(skf29(x1)) ->
% 15.30/4.32 === Backtracking. Learning clause 338:4:1:[64.3,336.3,64.3,337.4,12.2,7.1,7.1,19.1,86.3,302.1,328.3,13.3,330.1,329.1,310.3]:Top: ren4,r(x0),ren7 -> ren5
% 15.30/4.32 === Backtracking. Learning clause 339:5:2:[7.1,33.3,209.2,302.1,328.3]:TopTop: ren9,p(x0),r(x1),ren7 -> ren12
% 15.30/4.32 === Backtracking. Learning clause 340:4:2:[26.3,334.1,89.3,3.3,73.3,329.1,339.1,310.3,338.1,335.3]:TopTop: r(x0),ren7,p(x1),p(skf29(x1)) ->
% 15.30/4.32 === Conflict found: 330:4:1:[31.2,13.3,39.1,13.3]:Top: ren9,ren4,r(x0) -> ren10 {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 342:4:1:[64.3,341.2,330.4,329.1]:Top: ren9,ren4,r(x0),ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 343:4:2:[32.3,39.1,25.2,25.2,340.4,329.1]:TopTop: ren9,p(x0),r(x1),ren7 ->
% 15.30/4.32 === Conflict found: 64:4:2:[13.3,25.2]:TopTop: ren4,r(x0),ren7 -> p(x1) {x0 -> skc1, x1 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 345:3:1:[64.3,344.3,64.4,340.4]:Top: ren4,r(x0),ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 347:3:0:[255.2,346.3,54.2,51.3]:: ren14,ren5,ren12 ->
% 15.30/4.32 === Backtracking. Learning clause 349:2:2:[302.0,348.2,12.1,7.1,7.1]:TopTop: r(skc3) -> ren3(x0,x1)
% 15.30/4.32 === Backtracking. Learning clause 351:5:1:[345.0,350.5,21.1,46.3,22.3,46.3,349.1,17.2,43.3]:Top: r(x0),ren12,ren5,ren7,ren10 ->
% 15.30/4.32 === Backtracking. Learning clause 352:5:2:[4.1,343.2,57.1]:TopTop: ren9,r(x0),ren7,ren14 -> p(skf29(x1))
% 15.30/4.32 === Backtracking. Learning clause 353:5:1:[56.2,49.1,302.1,351.2]:Top: r(x0),ren5,ren7,ren10 -> ren14
% 15.30/4.32 === Backtracking. Learning clause 354:3:0:[56.2,50.1,302.1]:: ren12 -> ren14,ren5
% 15.30/4.32 === Backtracking. Learning clause 356:3:0:[302.0,355.3,23.2,8.2,47.1,7.1]:: ren11,r(skc3) -> ren12
% 15.30/4.32 === Conflict found: 228:5:2:[9.1,20.1,11.1]:TopTop: q(skc12),q(x0) -> ren4,ren5,ren3(x1,x0) {x0 -> skc10, x1 -> skc17}
% 15.30/4.32 === Backtracking. Learning clause 358:5:2:[338.0,357.4,228.5,10.1,9.3,10.3,20.1,34.2,343.2,20.1]:TopTop: q(x0),ren9,r(x1),ren7 -> ren5
% 15.30/4.32 === Backtracking. Learning clause 359:5:2:[8.1,358.1,356.2,43.3,302.1,354.1,353.2,352.4]:TopTop: ren10,ren9,r(x0),ren7 -> p(skf29(x1))
% 15.30/4.32 === Conflict found: 349:2:2:[302.0,348.2,12.1,7.1,7.1]:TopTop: r(skc3) -> ren3(x0,x1) {x0 -> skc1, x1 -> skf9(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 360:3:0:[349.2,17.2]:: r(skc3),ren5 -> ren4
% 15.30/4.32 === Backtracking. Learning clause 361:3:1:[32.3,39.1,25.2,25.2,359.1,343.2]:Top: ren9,r(x0),ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 362:5:2:[4.1,329.2,57.1,354.2,351.3]:TopTop: r(x0),ren12,ren7,ren10 -> p(skf29(x1))
% 15.30/4.32 === Backtracking. Learning clause 363:5:2:[4.1,329.2,57.1,353.5]:TopTop: r(x0),ren5,ren7,ren10 -> p(skf29(x1))
% 15.30/4.32 === Conflict found: 356:3:0:[302.0,355.3,23.2,8.2,47.1,7.1]:: ren11,r(skc3) -> ren12 {}
% 15.30/4.32 === Backtracking. Learning clause 364:4:0:[356.1,43.3]:: r(skc3),ren7,ren10 -> ren12
% 15.30/4.32 === Backtracking. Learning clause 365:5:2:[4.1,329.2,57.1]:TopTop: ren10,r(x0),ren7,ren14 -> p(skf29(x1))
% 15.30/4.32 === Backtracking. Learning clause 367:3:1:[361.0,366.3,32.2,25.2,37.2,25.2,329.2]:Top: ren10,r(x0),ren7 ->
% 15.30/4.32 === Conflict found: 209:4:2:[22.1,48.1,21.2,48.1]:TopTop: r(x0) -> r(x1),ren11,ren12 {x0 -> skc1, x1 -> skc3}
% 15.30/4.32 === Backtracking. Learning clause 369:4:1:[367.0,368.4,209.3,41.1,360.1,345.1,347.3]:Top: r(x0),ren7,ren14,ren5 ->
% 15.30/4.32 === Backtracking. Learning clause 370:7:2:[23.3,45.2,8.2,173.1,302.1]:TopTop: r(x0),ren12,p(x1) -> ren11,ren4,ren5,ren9
% 15.30/4.32 === Backtracking. Learning clause 373:4:1:[354.1,371.1,367.0,372.5,4.1,370.3,370.3,361.1,57.1,41.1,345.1]:Top: ren12,r(x0),ren7 -> ren5
% 15.30/4.32 === Backtracking. Learning clause 374:3:1:[52.3,318.2,373.1,369.4]:Top: r(x0),ren7,ren14 ->
% 15.30/4.32 === Backtracking. Learning clause 376:4:2:[369.2,375.4,2.3,89.2,58.1,335.4]:TopTop: r(x0),ren7,ren5,p(skf29(x1)) ->
% 15.30/4.32 === Backtracking. Learning clause 377:3:2:[3.3,89.1]:TopTop: p(x0) -> p(x1),ren14
% 15.30/4.32 === Backtracking. Learning clause 378:3:1:[11.1,36.2,36.2,377.1,17.2,361.1,345.1,374.3,376.4,373.4]:Top: ren12,r(x0),ren7 ->
% 15.30/4.32 === Conflict found: 377:3:2:[3.3,89.1]:TopTop: p(x0) -> p(x1),ren14 {x0 -> skf29(skc1), x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 380:3:2:[374.2,379.3,377.2,340.3]:TopTop: r(x0),ren7,p(skf29(x1)) ->
% 15.30/4.32 === Backtracking. Learning clause 382:3:1:[378.0,381.3,41.3,367.1,209.3,360.1,345.1]:Top: ren5,r(x0),ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 383:2:1:[36.1,377.1,7.1,302.1,361.1,209.2,41.1,367.1,374.3,378.1,380.3]:Top: r(x0),ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 384:5:1:[14.2,118.4,383.1]:Top: ren4,s(x0),ren10,ren9,ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 385:6:1:[26.3,384.2,377.2]:Top: ren4,ren10,ren9,ren7,p(x0) -> ren14
% 15.30/4.32 === Backtracking. Learning clause 387:6:1:[329.2,386.5,8.1,83.2,302.1,385.3]:Top: ren5,ren4,ren10,ren7,p(x0) -> ren14
% 15.30/4.32 === Conflict found: 161:3:3:[33.2,160.0,11.1,33.3]:TopTopTop: ren9,p(x0) -> ren3(x1,x2) {x0 -> skf29(skc1), x1 -> skc1, x2 -> skf9(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 390:5:1:[354.2,388.1,328.1,389.5,161.3,17.2,175.6,387.2,41.3]:Top: ren12,p(x0),ren11,ren7 -> ren14
% 15.30/4.32 === Backtracking. Learning clause 391:4:1:[24.3,45.2,383.1,383.1,390.3,347.1]:Top: p(x0),ren7,ren5,ren12 ->
% 15.30/4.32 === Backtracking. Learning clause 392:4:1:[19.1,161.3]:Top: ren4,ren9,p(x0) -> ren5
% 15.30/4.32 === Backtracking. Learning clause 394:4:1:[391.2,393.4,16.1,383.1,25.2,310.1,392.1]:Top: ren7,p(skf29(x0)),ren12,ren9 ->
% 15.30/4.32 === Backtracking. Learning clause 395:4:1:[32.3,37.2,25.2,25.2,41.3]:Top: ren11,ren7 -> ren9,p(x0)
% 15.30/4.32 === Backtracking. Learning clause 396:3:1:[24.3,45.2,383.1,383.1,395.1,310.1,391.3,394.4]:Top: ren7,p(skf29(x0)),ren12 ->
% 15.30/4.32 === Conflict found: 123:4:0:[24.2,76.2,47.1]:: ren4,ren11 -> r(skc6),ren12 {}
% 15.30/4.32 === Backtracking. Learning clause 397:4:1:[123.3,383.1,396.3]:Top: ren4,ren11,ren7,p(skf29(x0)) ->
% 15.30/4.32 === Backtracking. Learning clause 398:4:1:[17.2,161.3]:Top: ren5,ren9,p(x0) -> ren4
% 15.30/4.32 === Backtracking. Learning clause 399:3:1:[24.3,47.1,383.1,383.1,396.3]:Top: ren11,ren7,p(skf29(x0)) ->
% 15.30/4.32 === Backtracking. Learning clause 402:4:1:[397.1,400.4,394.2,401.5,32.3,39.1,25.2,25.2,43.2,313.2,392.4]:Top: ren7,p(skf29(x0)),ren4,ren9 ->
% 15.30/4.32 === Backtracking. Learning clause 403:5:1:[8.1,83.2,302.1,383.1]:Top: p(x0),ren5,ren4,ren7 -> ren9
% 15.30/4.32 === Conflict found: 377:3:2:[3.3,89.1]:TopTop: p(x0) -> p(x1),ren14 {x0 -> skc20, x1 -> skc13}
% 15.30/4.32 === Backtracking. Learning clause 405:7:1:[44.0,404.3,377.2,88.1,377.2,73.3,383.1]:Top: ren4,p(x0),p(skf29(x0)) -> ren11,ren12,ren9,ren10
% 15.30/4.32 === Backtracking. Learning clause 408:3:1:[396.2,406.3,397.1,407.4,54.2,52.3,302.1,377.3,405.2,43.2,403.2,402.4]:Top: ren7,p(skf29(x0)),ren4 ->
% 15.30/4.32 === Conflict found: 313:4:1:[49.1,308.3]:Top: ren5,p(x0),p(skf29(x0)) -> ren12 {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 409:4:1:[313.4,396.3]:Top: ren5,p(x0),p(skf29(x0)),ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 410:3:1:[16.1,383.1,25.2,408.3,409.2]:Top: ren5,p(skf29(x0)),ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 411:5:1:[31.3,39.1,16.2,383.1]:Top: s(x0),ren9,ren7 -> ren10,ren4
% 15.30/4.32 === Backtracking. Learning clause 413:3:1:[402.2,412.3,16.1,383.1,411.1,43.2,399.1]:Top: ren9,ren7,p(skf29(x0)) ->
% 15.30/4.32 === Backtracking. Learning clause 414:2:1:[8.1,173.1,302.1,383.1,408.3,413.1,410.1]:Top: p(skf29(x0)),ren7 ->
% 15.30/4.32 === Conflict found: 123:4:0:[24.2,76.2,47.1]:: ren4,ren11 -> r(skc6),ren12 {}
% 15.30/4.32 === Backtracking. Learning clause 415:4:0:[123.3,383.1]:: ren4,ren11,ren7 -> ren12
% 15.30/4.32 === Backtracking. Learning clause 417:4:1:[403.4,416.0,32.3,39.1,25.2,25.2,414.1,43.2,415.2,391.4]:Top: ren4,p(x0),ren7,ren5 ->
% 15.30/4.32 === Backtracking. Learning clause 418:4:0:[34.3,417.2,82.4,8.1,302.1,383.1]:: ren9,ren5,ren4,ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 419:3:0:[16.1,383.1,25.2,398.3,418.3]:: ren9,ren5,ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 421:3:0:[378.1,420.2,24.3,45.2,383.1]:: ren12,ren7 -> ren11
% 15.30/4.32 === Backtracking. Learning clause 422:3:1:[57.1,4.3]:Top: ren14 -> p(x0),p(skf29(x0))
% 15.30/4.32 === Backtracking. Learning clause 424:3:0:[418.0,423.3,56.2,49.1,422.1,414.1,302.1,421.1,395.1,403.1]:: ren5,ren4,ren7 ->
% 15.30/4.32 === Conflict found: 395:4:1:[32.3,37.2,25.2,25.2,41.3]:Top: ren11,ren7 -> ren9,p(x0) {x0 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 425:3:0:[395.4,414.1]:: ren11,ren7 -> ren9
% 15.30/4.32 === Backtracking. Learning clause 426:2:0:[16.1,383.1,25.2,414.1,424.2]:: ren5,ren7 ->
% 15.30/4.32 === Conflict found: 392:4:1:[19.1,161.3]:Top: ren4,ren9,p(x0) -> ren5 {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 428:4:1:[417.3,427.4,392.2,425.3]:Top: ren4,p(x0),ren11,ren7 ->
% 15.30/4.32 === Conflict found: 354:3:0:[56.2,50.1,302.1]:: ren12 -> ren14,ren5 {}
% 15.30/4.32 === Backtracking. Learning clause 431:3:0:[424.0,429.3,428.1,430.4,354.2,422.1,415.4,428.2]:: ren4,ren11,ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 432:3:1:[54.2,52.3,302.1,377.3,414.1,426.1,421.1]:Top: p(x0),ren7 -> ren11
% 15.30/4.32 === Backtracking. Learning clause 434:3:0:[432.0,433.3,32.3,39.1,25.2,43.2,25.2]:: ren9,ren7 -> ren11
% 15.30/4.32 === Backtracking. Learning clause 435:2:0:[11.2,36.2,36.2,19.1,432.1,426.1,434.1,431.2]:: ren4,ren7 ->
% 15.30/4.32 === Backtracking. Learning clause 436:1:0:[16.1,383.1,25.2,414.1,435.1]:: ren7 ->
% 15.30/4.32 === Conflict found: 142:4:2:[89.3,27.2,3.3]:TopTop: s(x0),p(x1) -> ren14,ren7 {x0 -> skc1, x1 -> skc20}
% 15.30/4.32 === Backtracking. Learning clause 437:3:2:[142.4,436.1,377.2]:TopTop: s(x0),p(x1) -> ren14
% 15.30/4.32 === Backtracking. Learning clause 438:2:0:[42.3,436.1]:: ren11,ren10 ->
% 15.30/4.32 === Backtracking. Learning clause 439:4:1:[32.3,39.1,437.1,437.1,73.3,438.2]:Top: ren9,p(x0),p(skf29(x0)),ren11 ->
% 15.30/4.32 === Backtracking. Learning clause 440:4:1:[31.3,39.1]:Top: s(x0),s(skf23(x0)),ren9 -> ren10
% 15.30/4.32 === Conflict found: 123:4:0:[24.2,76.2,47.1]:: ren4,ren11 -> r(skc6),ren12 {}
% 15.30/4.32 === Backtracking. Learning clause 441:4:1:[123.3,331.4,347.3,377.3,438.2,392.4,439.3]:Top: ren4,ren9,p(x0),ren11 ->
% 15.30/4.32 === Backtracking. Learning clause 442:5:2:[8.1,83.2,13.2,302.1]:TopTop: p(x0),ren5,ren4 -> ren9,s(x1)
% 15.30/4.32 === Conflict found: 123:4:0:[24.2,76.2,47.1]:: ren4,ren11 -> r(skc6),ren12 {}
% 15.30/4.32 === Backtracking. Learning clause 444:4:1:[439.0,443.4,123.3,13.2,354.1,442.2,437.1,73.3]:Top: ren11,ren4,p(x0),p(skf29(x0)) ->
% 15.30/4.32 === Backtracking. Learning clause 445:5:2:[8.2,356.2,83.2,302.1,441.2,347.3,377.3]:TopTop: ren4,ren11,ren5,p(x0) -> p(x1)
% 15.30/4.32 === Conflict found: 349:2:2:[302.0,348.2,12.1,7.1,7.1]:TopTop: r(skc3) -> ren3(x0,x1) {x0 -> skc10, x1 -> skf11(skc10)}
% 15.30/4.32 === Backtracking. Learning clause 447:3:0:[158.1,446.3,349.2,19.1,8.2]:: ren4 -> ren5,q(skc4)
% 15.30/4.32 === Backtracking. Learning clause 448:3:2:[11.2,36.2,36.2]:TopTop: -> ren3(x0,x1),p(skc20),ren9
% 15.30/4.32 === Backtracking. Learning clause 451:6:1:[438.1,449.5,148.2,450.6,29.1,40.1,108.2,14.2,107.4,7.2,447.3]:Top: s(x0),ren12,ren11,ren4 -> ren9,ren5
% 15.30/4.32 === Backtracking. Learning clause 452:6:1:[28.1,451.1,436.1]:Top: ren12,ren11,ren4 -> p(x0),ren9,ren5
% 15.30/4.32 === Backtracking. Learning clause 453:3:1:[52.3,318.2,452.1,441.2,377.3,445.3,444.4]:Top: ren11,ren4,p(x0) ->
% 15.30/4.32 === Backtracking. Learning clause 454:4:1:[24.3,45.2,13.2,13.2,453.1,437.1,347.1]:Top: ren4,p(x0),ren5,ren12 ->
% 15.30/4.32 === Backtracking. Learning clause 456:4:0:[438.0,455.3,24.3,45.2,77.3,77.3]:: ren12,ren10,ren4 -> ren9
% 15.30/4.32 === Backtracking. Learning clause 457:3:1:[44.1,436.1,456.2,453.1,392.2,454.3]:Top: ren4,p(x0),ren12 ->
% 15.30/4.32 === Conflict found: 209:4:2:[22.1,48.1,21.2,48.1]:TopTop: r(x0) -> r(x1),ren11,ren12 {x0 -> skc1, x1 -> skc3}
% 15.30/4.32 === Backtracking. Learning clause 459:4:2:[302.0,458.4,209.2,7.2]:TopTop: r(x0),q(x1) -> ren11,ren12
% 15.30/4.32 === Conflict found: 119:6:1:[118.1,28.1,118.1,14.2]:Top: ren10,ren9,ren4 -> p(x0),ren7,r(skc6) {x0 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 462:5:2:[438.0,460.5,457.2,461.6,119.6,459.1,436.1,33.3]:TopTop: ren10,ren4,ren9,p(x0) -> p(x1)
% 15.30/4.32 === Backtracking. Learning clause 464:4:2:[441.3,463.3,44.1,436.1,462.1]:TopTop: ren4,ren9,p(x0) -> p(x1)
% 15.30/4.32 === Backtracking. Learning clause 465:5:1:[8.3,302.1,77.3,83.2]:Top: ren10,p(x0),ren5,ren4 -> ren9
% 15.30/4.32 === Backtracking. Learning clause 467:3:1:[454.3,466.3,44.1,436.1,465.1,464.2,313.3,453.1]:Top: ren5,ren4,p(x0) ->
% 15.30/4.32 === Backtracking. Learning clause 468:3:0:[54.2,52.3,302.1]:: ren14 -> ren5,ren12
% 15.30/4.32 === Backtracking. Learning clause 469:3:1:[32.3,37.2,142.1,142.1,468.1,436.1,457.3,392.2,467.1]:Top: ren10,ren4,p(x0) ->
% 15.30/4.32 === Backtracking. Learning clause 470:2:1:[44.3,453.1,436.1,469.1]:Top: ren4,p(x0) ->
% 15.30/4.32 === Backtracking. Learning clause 471:3:0:[23.2,8.2,45.2,8.2,302.1]:: ren12 -> ren11,q(skc4)
% 15.30/4.32 === Backtracking. Learning clause 473:4:0:[456.3,472.0,34.2,82.4,470.2,471.3,438.1]:: ren5,ren4,ren12,ren10 ->
% 15.30/4.32 === Conflict found: 422:3:1:[57.1,4.3]:Top: ren14 -> p(x0),p(skf29(x0)) {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 474:2:0:[422.2,470.2,470.2]:: ren14,ren4 ->
% 15.30/4.32 === Backtracking. Learning clause 475:3:0:[56.2,49.1,302.1,474.1,473.3]:: ren5,ren4,ren10 ->
% 15.30/4.32 === Conflict found: 119:6:1:[118.1,28.1,118.1,14.2]:Top: ren10,ren9,ren4 -> p(x0),ren7,r(skc6) {x0 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 477:5:1:[435.1,476.4,119.6,459.1,470.2,438.1]:Top: ren9,q(x0),ren4,ren10 -> ren12
% 15.30/4.32 === Conflict found: 448:3:2:[11.2,36.2,36.2]:TopTop: -> ren3(x0,x1),p(skc20),ren9 {x0 -> skc10, x1 -> skf11(skc10)}
% 15.30/4.32 === Backtracking. Learning clause 478:2:0:[448.1,19.1,470.2,477.1,447.3,354.1,474.1,475.1]:: ren4,ren10 ->
% 15.30/4.32 === Backtracking. Learning clause 480:3:0:[478.1,479.3,8.2,330.3,302.1]:: ren9,ren4 -> q(skc4)
% 15.30/4.32 === Backtracking. Learning clause 481:3:0:[34.2,82.4,470.2,480.3]:: ren5,ren9,ren4 ->
% 15.30/4.32 === Backtracking. Learning clause 482:3:1:[36.1,470.2]:Top: ren4 -> q(x0),ren9
% 15.30/4.32 === Conflict found: 107:5:2:[22.3,21.2,46.3,46.3,76.3]:TopTop: ren12,ren11,ren4,r(x0) -> r(x1) {x0 -> skc1, x1 -> skc3}
% 15.30/4.32 === Backtracking. Learning clause 484:5:2:[148.2,483.5,107.5,7.2]:TopTop: ren12,ren11,ren4,r(x0),q(x1) ->
% 15.30/4.32 === Backtracking. Learning clause 486:4:1:[478.1,485.3,29.2,108.2,40.1,14.2]:Top: s(x0),ren4 -> ren9,r(skc6)
% 15.30/4.32 === Conflict found: 108:4:1:[30.1,40.1]:Top: s(x0) -> s(skc24),ren9,ren10 {x0 -> skc16}
% 15.30/4.32 === Backtracking. Learning clause 489:3:0:[482.1,487.1,456.1,488.4,108.1,28.1,486.1,484.4,470.2,44.3,436.1]:: ren12,ren4 -> ren9
% 15.30/4.32 === Backtracking. Learning clause 490:2:0:[56.2,49.1,302.1,474.1,489.1,481.2]:: ren5,ren4 ->
% 15.30/4.32 === Conflict found: 354:3:0:[56.2,50.1,302.1]:: ren12 -> ren14,ren5 {}
% 15.30/4.32 === Backtracking. Learning clause 492:2:0:[490.0,491.2,354.2,474.1]:: ren12,ren4 ->
% 15.30/4.32 === Conflict found: 123:4:0:[24.2,76.2,47.1]:: ren4,ren11 -> r(skc6),ren12 {}
% 15.30/4.32 === Backtracking. Learning clause 495:2:0:[492.0,493.2,478.1,494.3,123.3,330.3,44.3,436.1]:: ren9,ren4 ->
% 15.30/4.32 === Conflict found: 448:3:2:[11.2,36.2,36.2]:TopTop: -> ren3(x0,x1),p(skc20),ren9 {x0 -> skc10, x1 -> skf11(skc10)}
% 15.30/4.32 === Backtracking. Learning clause 496:1:0:[448.1,19.1,470.2,490.1,495.1]:: ren4 ->
% 15.30/4.32 === Conflict found: 398:4:1:[17.2,161.3]:Top: ren5,ren9,p(x0) -> ren4 {x0 -> skc20}
% 15.30/4.32 === Backtracking. Learning clause 497:4:1:[398.4,496.1,377.2]:Top: ren5,ren9,p(x0) -> ren14
% 15.30/4.32 === Conflict found: 118:4:2:[30.1,38.3,29.2,38.3]:TopTop: s(x0),ren10,ren9 -> s(x1) {x0 -> skc16, x1 -> skc24}
% 15.30/4.32 === Backtracking. Learning clause 500:4:2:[361.2,498.4,478.0,499.5,118.1,28.1,162.2]:TopTop: r(x0),ren10,ren9 -> p(x1)
% 15.30/4.32 === Backtracking. Learning clause 502:4:1:[436.0,501.4,24.3,45.2,500.1,500.1,42.1]:Top: ren12,ren9,ren10 -> p(x0)
% 15.30/4.32 === Conflict found: 360:3:0:[349.2,17.2]:: r(skc3),ren5 -> ren4 {}
% 15.30/4.32 === Backtracking. Learning clause 503:2:0:[360.1,8.2,496.1,302.1]:: ren5 -> q(skc4)
% 15.30/4.32 === Conflict found: 502:4:1:[436.0,501.4,24.3,45.2,500.1,500.1,42.1]:Top: ren12,ren9,ren10 -> p(x0) {x0 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 505:4:0:[354.2,504.2,502.4,497.3]:: ren12,ren10,ren9 -> ren14
% 15.30/4.32 === Conflict found: 269:7:2:[31.3,39.1,16.2,22.2,46.3,21.2,46.3]:TopTop: s(x0),ren9,ren12,ren11 -> ren10,ren4,r(x1) {x0 -> skc16, x1 -> skc6}
% 15.30/4.32 === Backtracking. Learning clause 510:4:2:[44.2,506.2,502.2,507.3,492.1,508.4,436.0,509.7,269.1,28.1]:TopTop: ren9,ren12 -> r(x0),p(x1)
% 15.30/4.32 === Backtracking. Learning clause 511:3:0:[7.2,510.3,302.1,497.3,347.1,503.2]:: ren9,ren12,ren5 ->
% 15.30/4.32 === Conflict found: 310:4:1:[308.3,50.1]:Top: p(x0),p(skf29(x0)),ren12 -> ren5 {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 513:3:0:[511.2,512.3,310.1,502.4,502.4]:: ren12,ren9,ren10 ->
% 15.30/4.32 === Conflict found: 510:4:2:[44.2,506.2,502.2,507.3,492.1,508.4,436.0,509.7,269.1,28.1]:TopTop: ren9,ren12 -> r(x0),p(x1) {x0 -> skc1, x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 516:3:1:[511.2,514.3,513.2,515.4,510.4,310.1,309.1,44.3,436.1]:Top: p(skf29(x0)),ren12,ren9 ->
% 15.30/4.32 === Conflict found: 309:5:2:[21.1,46.3,22.3,46.3,7.2,302.1,33.3]:TopTop: r(x0),ren12,ren11,ren9,p(x1) -> {x0 -> skc3, x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 517:2:0:[309.5,422.2,510.3,44.3,436.1,354.2,511.3,513.3,516.1]:: ren12,ren9 ->
% 15.30/4.32 === Conflict found: 398:4:1:[17.2,161.3]:Top: ren5,ren9,p(x0) -> ren4 {x0 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 518:3:1:[398.4,496.1]:Top: ren5,ren9,p(x0) ->
% 15.30/4.32 === Backtracking. Learning clause 520:3:1:[518.0,519.3,16.1,459.1,437.1,496.1,33.3,468.1,517.1,438.1]:Top: p(x0),ren9,ren10 ->
% 15.30/4.32 === Conflict found: 439:4:1:[32.3,39.1,437.1,437.1,73.3,438.2]:Top: ren9,p(x0),p(skf29(x0)),ren11 -> {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 521:4:1:[439.2,377.2]:Top: ren9,p(skf29(x0)),ren11 -> ren14
% 15.30/4.32 === Backtracking. Learning clause 522:2:1:[44.1,436.1,521.3,468.1,517.1,518.1,520.3]:Top: p(skf29(x0)),ren9 ->
% 15.30/4.32 === Conflict found: 422:3:1:[57.1,4.3]:Top: ren14 -> p(x0),p(skf29(x0)) {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 524:3:0:[522.0,523.3,422.2,518.3]:: ren14,ren5,ren9 ->
% 15.30/4.32 === Backtracking. Learning clause 526:2:0:[511.1,525.2,56.2,49.1,302.1,524.1]:: ren5,ren9 ->
% 15.30/4.32 === Conflict found: 468:3:0:[54.2,52.3,302.1]:: ren14 -> ren5,ren12 {}
% 15.30/4.32 === Backtracking. Learning clause 528:2:0:[524.1,527.2,468.3,517.1]:: ren14,ren9 ->
% 15.30/4.32 === Conflict found: 228:5:2:[9.1,20.1,11.1]:TopTop: q(skc12),q(x0) -> ren4,ren5,ren3(x1,x0) {x0 -> skc4, x1 -> skc17}
% 15.30/4.32 === Backtracking. Learning clause 532:3:1:[526.0,529.2,528.0,530.4,517.0,531.5,228.1,10.3,10.1,20.1,34.2,377.1,8.1,356.2,496.1,302.1]:Top: ren9,ren11 -> p(x0)
% 15.30/4.32 === Conflict found: 228:5:2:[9.1,20.1,11.1]:TopTop: q(skc12),q(x0) -> ren4,ren5,ren3(x1,x0) {x0 -> skc4, x1 -> skc17}
% 15.30/4.32 === Backtracking. Learning clause 536:2:0:[526.0,533.2,528.0,534.3,520.0,535.4,228.1,10.3,10.1,20.1,34.2,377.1,8.1,500.1,496.1,302.1]:: ren10,ren9 ->
% 15.30/4.32 === Conflict found: 532:3:1:[526.0,529.2,528.0,530.4,517.0,531.5,228.1,10.3,10.1,20.1,34.2,377.1,8.1,356.2,496.1,302.1]:Top: ren9,ren11 -> p(x0) {x0 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 537:2:0:[532.3,522.1]:: ren11,ren9 ->
% 15.30/4.32 === Backtracking. Learning clause 538:1:0:[44.1,436.1,536.1,537.1]:: ren9 ->
% 15.30/4.32 === Conflict found: 448:3:2:[11.2,36.2,36.2]:TopTop: -> ren3(x0,x1),p(skc20),ren9 {x0 -> skc1, x1 -> skf9(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 541:2:0:[526.1,539.2,490.1,540.3,448.1,17.2]:: ren5 -> p(skc20)
% 15.30/4.32 === Backtracking. Learning clause 545:4:1:[44.2,542.0,467.1,543.5,410.2,544.6,24.3,47.1,334.2,334.2,28.1,538.1,73.1,347.3]:Top: p(skf29(x0)),ren14,ren5 -> ren10
% 15.30/4.32 === Conflict found: 334:5:2:[29.1,40.1,108.2,15.2]:TopTop: s(x0),r(x1) -> ren9,ren10,ren4 {x0 -> skc16, x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 547:3:1:[226.1,546.2,334.1,28.1,8.2,436.1,173.1,496.1,538.1,73.1,545.3]:Top: p(skf29(x0)),ren14 -> ren10
% 15.30/4.32 === Backtracking. Learning clause 549:4:1:[438.1,548.3,24.3,47.1,334.2,334.2,28.1,436.1,496.1,538.1,347.3]:Top: ren11,ren14,ren5 -> p(x0)
% 15.30/4.32 === Backtracking. Learning clause 551:2:0:[438.1,550.2,8.3,302.1,334.2,28.1,173.1,422.2,436.1,496.1,538.1,549.3,547.1]:: ren11,ren14 ->
% 15.30/4.32 === Backtracking. Learning clause 553:3:2:[538.0,552.3,9.3,35.2]:TopTop: ren3(x0,skc19),q(x0),p(x1) ->
% 15.30/4.32 === Backtracking. Learning clause 554:4:2:[21.2,22.3,46.3,46.3]:TopTop: r(x0),ren12,ren11 -> r(x1)
% 15.30/4.32 === Conflict found: 554:4:2:[21.2,22.3,46.3,46.3]:TopTop: r(x0),ren12,ren11 -> r(x1) {x0 -> skc1, x1 -> skc3}
% 15.30/4.32 === Backtracking. Learning clause 556:4:1:[490.1,555.4,554.4,360.1]:Top: r(x0),ren12,ren11,ren5 ->
% 15.30/4.32 === Backtracking. Learning clause 559:3:1:[453.1,557.3,551.1,558.4,16.1,556.1,437.1,313.4,377.2]:Top: ren11,ren5,p(skf29(x0)) ->
% 15.30/4.32 === Conflict found: 142:4:2:[89.3,27.2,3.3]:TopTop: s(x0),p(x1) -> ren14,ren7 {x0 -> skc16, x1 -> skc20}
% 15.30/4.32 === Backtracking. Learning clause 560:2:0:[142.2,541.2,551.2,28.1,436.1,559.3]:: ren11,ren5 ->
% 15.30/4.32 === Backtracking. Learning clause 562:2:1:[560.1,561.2,8.2,356.2,302.1,173.1,496.1,538.1,377.2,354.1,551.2]:Top: p(x0),ren11 ->
% 15.30/4.32 === Conflict found: 334:5:2:[29.1,40.1,108.2,15.2]:TopTop: s(x0),r(x1) -> ren9,ren10,ren4 {x0 -> skc16, x1 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 565:3:2:[537.1,563.3,496.0,564.4,334.4,438.2]:TopTop: s(x0),r(x1),ren11 ->
% 15.30/4.32 === Backtracking. Learning clause 566:1:0:[24.3,47.1,565.2,565.2,28.1,436.1,562.1,354.1,551.2,560.2]:: ren11 ->
% 15.30/4.32 === Conflict found: 459:4:2:[302.0,458.4,209.2,7.2]:TopTop: r(x0),q(x1) -> ren11,ren12 {x0 -> skc1, x1 -> skc4}
% 15.30/4.32 === Backtracking. Learning clause 567:3:1:[459.2,503.2,566.1]:Top: r(x0),ren5 -> ren12
% 15.30/4.32 === Backtracking. Learning clause 569:2:0:[426.1,568.2,31.3,37.2,16.2,16.2,567.1,44.2,496.1,538.1,566.1,347.3]:: ren14,ren5 ->
% 15.30/4.32 === Backtracking. Learning clause 571:3:1:[520.1,570.2,32.3,37.2,437.1,437.1]:Top: ren10,p(x0) -> ren14
% 15.30/4.32 === Conflict found: 142:4:2:[89.3,27.2,3.3]:TopTop: s(x0),p(x1) -> ren14,ren7 {x0 -> skc16, x1 -> skc20}
% 15.30/4.32 === Backtracking. Learning clause 573:1:0:[426.1,572.1,142.2,541.2,28.1,571.2,44.2,566.1,569.1]:: ren5 ->
% 15.30/4.32 === Conflict found: 370:7:2:[23.3,45.2,8.2,173.1,302.1]:TopTop: r(x0),ren12,p(x1) -> ren11,ren4,ren5,ren9 {x0 -> skc1, x1 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 577:3:2:[562.1,574.3,573.0,575.4,517.1,576.5,370.5,496.1]:TopTop: r(x0),ren12,p(x1) ->
% 15.30/4.32 === Conflict found: 173:5:2:[9.1,20.1,10.3,20.1,35.2]:TopTop: q(x0),p(x1) -> ren4,ren5,ren9 {x0 -> skc4, x1 -> skf29(skc1)}
% 15.30/4.32 === Backtracking. Learning clause 580:2:1:[551.0,578.2,569.1,579.3,173.1,471.3,538.1,496.1,468.3]:Top: p(x0),ren14 ->
% 15.30/4.32 === Backtracking. Learning clause 582:1:1:[562.1,581.1,44.1,436.1,571.1,580.2]:Top: p(x0) ->
% 15.30/4.32 === Conflict found: 422:3:1:[57.1,4.3]:Top: ren14 -> p(x0),p(skf29(x0)) {x0 -> skc1}
% 15.30/4.32 === Backtracking. Learning clause 584:1:0:[580.0,583.1,422.2,582.1]:: ren14 ->
% 15.30/4.32 === Backtracking. Learning clause 587:2:1:[538.0,585.1,566.0,586.2,36.1,582.1,459.2]:Top: r(x0) -> ren12
% 15.30/4.32 === Backtracking. Learning clause 589:1:1:[538.0,588.1,36.1,582.1]:Top: -> q(x0)
% 15.30/4.32 === Conflict found: 354:3:0:[56.2,50.1,302.1]:: ren12 -> ren14,ren5 {}
% 15.30/4.32 === Backtracking. Learning clause 591:1:1:[584.0,590.1,354.3,573.1,587.2]:Top: r(x0) ->
% 15.30/4.32
% 15.30/4.32 SZS status Unsatisfiable
% 15.30/4.32
% 15.30/4.32 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.30/4.32
% 15.30/4.32 SPASS-SCL-FOL Statistics:
% 15.30/4.32 Number of learned clauses: 343
% 15.30/4.32 Number of propagations: 9864
% 15.30/4.32 Number of decisions: 905
% 15.30/4.32 Number of resolutions: 1343
% 15.30/4.32 Number of condensations: 116
% 15.30/4.32 Number of sub resolutions: 190
% 15.30/4.32 Number of input literals (deduplicated): 48
% 15.30/4.32 Number of grows: 7
% 15.30/4.32 Number of considered ground atoms: 448
% 15.30/4.32
% 15.30/4.32 Needed: 0:00:03.72
% 15.30/4.32
%------------------------------------------------------------------------------