%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN917+1 : TPTP v9.2.1. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:24 PM UTC 2026
% Result : Theorem 105.32s 21.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYN917+1 : TPTP v9.2.1. Released v3.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.32 % Computer : n015.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Thu May 7 13:50:47 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.18/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 105.32/21.66 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 105.32/21.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 105.32/21.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 105.32/21.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 105.32/21.66 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 105.32/21.66 Execution resolution_1 ended with status: unsatisfiable
% 105.32/21.66 Used heuristic: resolution_1
% 105.32/21.66
% 105.32/21.66 Input Clauses:
% 105.32/21.67
% 105.32/21.67 Predicates: f g h r p q c ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40
% 105.32/21.67 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 skc21 skc22 skc23 skc24 skc25 skc26 skc27 skc28 skc29 skc30 skc31 skc32 skc33 skc34 skc35 skc36 skc38
% 105.32/21.67 Fol Functions: skf37
% 105.32/21.67 Problem Properties:
% 105.32/21.67 This is a full first-order problem without equality.
% 105.32/21.67
% 105.32/21.67 After reduction: Problem Properties:
% 105.32/21.67 This is a full first-order problem without equality.
% 105.32/21.67
% 105.32/21.67
% 105.32/21.67 Reduced Input Clauses:
% 105.32/21.67 130:2:2:[25.0,23.1]:TopTop: p(x0) -> ren8(x0,x1)
% 105.32/21.67 131:1:1:[54.0,55.0]:Top: -> ren18(x0)
% 105.32/21.67 132:1:0:[57.0,56.0]:: -> ren19
% 105.32/21.67 133:1:0:[58.0,59.0]:: -> ren20
% 105.32/21.67 136:17:2:[131.1,129.9,132.1,134.10,133.1,135.11]:TopTop: ren3,ren4,ren7,ren8(skf37(x0),x0),ren11,ren12,ren15,ren16(x1),ren17,ren23,ren26,ren27,ren28,ren31,ren34,ren37,ren40 ->
% 105.32/21.67 137:1:0:[84.0,83.0]:: -> ren27
% 105.32/21.67 138:1:0:[88.0,87.0]:: -> ren28
% 105.32/21.67
% 105.32/21.67 Most General Atoms: ren1(x0) g(x0) ren2(x0) ren3 f(x1) h(x1) ren4 r(x0,x2) ren5(x0) ren6(x0) ren7 p(x0) ren8(x1,x0) ren9(x0) ren10 ren11 q(x1) ren12 ren13(x0) ren14 ren15 ren17 ren18(x0) ren19 ren20 ren40 ren39 ren21(x0) c ren22 ren23 ren24(x0) ren25 ren26 ren16(x1) ren27 ren28 ren31 ren34 ren37 ren38(x0) ren29(x0) ren30 ren32(x0) ren33 ren35(x0) ren36
% 105.32/21.67
% 105.32/21.67 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_1 ===
% 105.32/21.67
% 105.32/21.67 === Backtracking. Learning clause 139:2:0:[51.1,43.1]:: -> ren17,ren14
% 105.32/21.67 === Backtracking. Learning clause 140:2:0:[36.2,44.1,43.1]:: -> ren12,ren14
% 105.32/21.67 === Backtracking. Learning clause 141:3:1:[53.2,36.2,51.1]:Top: -> p(x0),ren12,ren17
% 105.32/21.67 === Conflict found: 141:3:1:[53.2,36.2,51.1]:Top: -> p(x0),ren12,ren17 {x0 -> skc10}
% 105.32/21.67 === Backtracking. Learning clause 142:2:0:[141.1,37.1]:: -> ren17,ren12
% 105.32/21.67 === Backtracking. Learning clause 144:3:1:[29.0,143.1,31.2,36.2]:Top: p(skc6) -> p(x0),ren12
% 105.32/21.67 === Backtracking. Learning clause 145:2:1:[36.2,38.1]:Top: -> p(x0),ren12
% 105.32/21.67 === Conflict found: 144:3:1:[29.0,143.1,31.2,36.2]:Top: p(skc6) -> p(x0),ren12 {x0 -> skc10}
% 105.32/21.67 === Backtracking. Learning clause 146:1:0:[144.2,37.1,145.1]:: -> ren12
% 105.32/21.67 === Backtracking. Learning clause 147:2:0:[6.2,4.1,1.2]:: -> ren3,f(skc1)
% 105.32/21.67 === Backtracking. Learning clause 148:5:1:[6.2,5.1,3.2,22.3]:Top: g(skc1),f(x0),g(x0) -> ren3,ren7
% 105.32/21.67 === Backtracking. Learning clause 149:2:0:[21.2,7.4,148.1,147.2]:: -> ren7,ren3
% 105.32/21.67 === Backtracking. Learning clause 150:4:1:[6.2,5.1,3.2,9.3]:Top: g(skc1),f(x0),g(x0) -> ren3
% 105.32/21.67 === Backtracking. Learning clause 151:1:0:[8.2,7.4,150.1,147.2]:: -> ren3
% 105.32/21.67 === Backtracking. Learning clause 152:3:0:[19.2,17.1]:: ren5(skc4) -> ren7,f(skc5)
% 105.32/21.67 === Backtracking. Learning clause 153:2:1:[11.3,13.1,10.2]:Top: r(x0,skc2) -> ren4
% 105.32/21.67 === Clause set with instances from active satisfied. Growing active. New size: 107
% 105.32/21.67 === Restarting.
% 105.32/21.67 === Backtracking. Learning clause 154:3:0:[64.2,43.1]:: ren22 -> c,ren14
% 105.32/21.67 === Backtracking. Learning clause 155:2:0:[123.1,43.1]:: -> ren39,ren14
% 105.32/21.67 === Backtracking. Learning clause 156:3:0:[27.1,35.1,44.1]:: -> ren10,ren11,ren14
% 105.32/21.67 === Backtracking. Learning clause 157:3:0:[102.2,64.2]:: ren33,ren22 -> c
% 105.32/21.67 === Backtracking. Learning clause 158:3:0:[62.2,69.1,64.2]:: ren22 -> ren23,c
% 105.32/21.67 === Backtracking. Learning clause 160:2:0:[75.0,159.0,80.1,72.1]:: -> ren26,c
% 105.32/21.67 === Backtracking. Learning clause 162:2:0:[93.1,161.0,97.1,90.2]:: -> ren31,c
% 105.32/21.67 === Backtracking. Learning clause 164:3:0:[157.0,163.1,99.1,108.1,64.2]:: ren22 -> ren34,c
% 105.32/21.67 === Backtracking. Learning clause 166:2:0:[113.1,165.0,117.1,110.2]:: -> ren37,c
% 105.32/21.67 === Clause set with instances from active satisfied. Growing active. New size: 162
% 105.32/21.67 === Backtracking. Learning clause 167:3:1:[50.1,64.2]:Top: ren22 -> ren16(x0),c
% 105.32/21.67 === Clause set with instances from active satisfied. Growing active. New size: 226
% 105.32/21.67 === Clause set with instances from active satisfied. Growing active. New size: 290
% 105.32/21.67 === Backtracking. Learning clause 168:1:0:[10.2,153.1,12.1]:: -> ren4
% 105.32/21.67 === Clause set with instances from active satisfied. Growing active. New size: 354
% 105.32/21.67 === Conflict found: 136:17:2:[131.1,129.9,132.1,134.10,133.1,135.11]:TopTop: ren3,ren4,ren7,ren8(skf37(x0),x0),ren11,ren12,ren15,ren16(x1),ren17,ren23,ren26,ren27,ren28,ren31,ren34,ren37,ren40 -> {x0 -> skc2, x1 -> skc31}
% 105.32/21.67 === Backtracking. Learning clause 174:12:2:[151.0,169.0,168.0,170.1,145.1,171.4,137.0,172.9,138.0,173.10,136.8,49.2,25.2]:TopTop: ren7,ren11,ren15,ren17,ren23,ren26,ren31,ren34,ren37,ren40,q(x0) -> p(x1)
% 105.32/21.67 === Backtracking. Learning clause 177:12:3:[53.2,175.2,29.0,176.13,20.4,21.2,174.1,35.3,27.1,31.2]:TopTopTop: f(x0),ren15,ren23,ren26,ren31,ren34,ren37,ren40,q(x1),p(skc6) -> g(x0),p(x2)
% 105.32/21.67 === Backtracking. Learning clause 179:11:2:[29.0,178.10,35.1,26.1,174.2]:TopTop: ren7,ren15,ren17,ren23,ren26,ren31,ren34,ren37,ren40,q(x0) -> p(x1)
% 105.32/21.67 === Conflict found: 177:12:3:[53.2,175.2,29.0,176.13,20.4,21.2,174.1,35.3,27.1,31.2]:TopTopTop: f(x0),ren15,ren23,ren26,ren31,ren34,ren37,ren40,q(x1),p(skc6) -> g(x0),p(x2) {x0 -> skc5, x1 -> skc2, x2 -> skc28}
% 105.32/21.67 === Backtracking. Learning clause 180:11:3:[177.1,17.2,18.2]:TopTopTop: ren15,ren23,ren26,ren31,ren34,ren37,ren40,q(x0),p(skc6),ren6(x1) -> p(x2)
% 105.32/21.67 === Backtracking. Learning clause 181:11:2:[22.2,15.1,16.1,14.1,19.1,180.10]:TopTop: ren15,ren23,ren26,ren31,ren34,ren37,ren40,q(x0),p(skc6) -> ren7,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 182:2:1:[21.2,20.4,17.2,18.2]:Top: ren6(x0) -> ren7
% 105.32/21.67 === Backtracking. Learning clause 183:11:3:[22.3,16.1,14.1,15.1,19.1,182.1,179.1,127.3,53.3]:TopTopTop: ren15,ren23,ren26,ren31,ren34,ren37,ren38(skc36),ren39,p(x0),q(x1) -> p(x2)
% 105.32/21.67 === Clause set with instances from active satisfied. Growing active. New size: 418
% 105.32/21.67 === Backtracking. Learning clause 189:12:2:[151.0,184.0,168.0,185.1,145.1,186.4,137.0,187.10,138.0,188.11,24.2,136.4]:TopTop: ren7,ren11,ren15,ren16(x0),ren17,ren23,ren26,ren31,ren34,ren37,ren40 -> p(x1)
% 105.32/21.67 === Backtracking. Learning clause 191:11:3:[29.0,190.10,52.1,183.10,189.5,49.2,35.3,26.1,127.3,182.2]:TopTopTop: p(x0),ren15,ren23,ren26,ren31,ren34,ren37,ren38(skc36),ren39,ren6(x1) -> p(x2)
% 105.32/21.67 === Backtracking. Learning clause 193:11:2:[29.0,192.10,52.1,183.10,189.5,49.2,35.3,26.1,127.3]:TopTop: p(x0),ren7,ren15,ren23,ren26,ren31,ren34,ren37,ren38(skc36),ren39 -> p(x1)
% 105.32/21.67 === Backtracking. Learning clause 196:7:3:[124.1,194.4,110.0,195.6,22.3,16.1,15.1,14.1,19.1,191.10,193.2,121.2,79.3,73.3,114.1,118.3,112.1,76.3]:TopTopTop: ren15,ren23,ren31,ren34,p(x0) -> ren35(x1),p(x2)
% 105.32/21.67 === Backtracking. Learning clause 197:3:1:[63.1,110.1,69.1,65.2,120.1]:Top: -> ren35(x0),ren23,ren38(skc19)
% 105.32/21.67 === Backtracking. Learning clause 198:3:1:[112.2,110.1,31.1,27.2,35.1,114.2,26.2,35.1]:Top: -> ren35(x0),ren10,ren11
% 105.32/21.67 === Backtracking. Learning clause 199:6:3:[69.3,196.2,66.2,63.2,110.1]:TopTopTop: ren15,ren31,ren34,p(x0) -> p(x1),ren35(x2)
% 105.32/21.67 === Backtracking. Learning clause 204:8:2:[160.0,200.3,162.0,201.4,166.0,202.6,64.0,203.9,70.1,61.1,179.4]:TopTop: ren7,ren15,ren17,ren34,ren40,q(x0) -> c,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 206:3:1:[64.0,205.0,70.1,61.1]:Top: -> ren23,p(x0),c
% 105.32/21.67 === Backtracking. Learning clause 208:8:1:[66.0,207.5,53.3,204.3,27.2,35.1,65.1]:Top: p(x0),ren7,ren15,ren34,ren40 -> ren10,ren11,ren22
% 105.32/21.67 === Backtracking. Learning clause 209:4:2:[128.1,119.1,122.1,61.2]:TopTop: p(x0),ren21(x1) -> ren40,c
% 105.32/21.67 === Backtracking. Learning clause 211:7:3:[29.0,210.6,53.3,204.3,27.2,35.1,209.3,112.2,114.2,26.2,35.1]:TopTopTop: ren7,ren15,ren34,p(x0),ren21(x1) -> p(x2),ren11
% 105.32/21.67 === Conflict found: 189:12:2:[151.0,184.0,168.0,185.1,145.1,186.4,137.0,187.10,138.0,188.11,24.2,136.4]:TopTop: ren7,ren11,ren15,ren16(x0),ren17,ren23,ren26,ren31,ren34,ren37,ren40 -> p(x1) {x0 -> skc31, x1 -> skc31}
% 105.32/21.67 === Backtracking. Learning clause 214:8:1:[206.0,212.4,162.0,213.5,189.7,160.1,166.1,49.2]:Top: ren7,ren11,ren15,ren17,ren34,ren40 -> c,p(x0)
% 105.32/21.67 === Backtracking. Learning clause 216:2:1:[160.1,215.1,79.2,76.3,73.3]:Top: p(x0) -> ren26
% 105.32/21.67 === Backtracking. Learning clause 219:8:3:[53.2,217.1,29.0,218.8,47.3,204.2,40.2,26.2,35.1,43.2]:TopTopTop: ren7,ren34,ren40,q(x0),p(x1) -> c,p(x2),ren11
% 105.32/21.67 === Backtracking. Learning clause 221:5:2:[29.0,220.4,22.2,15.1,16.1,14.1,19.1,182.1,219.1,112.2,114.2,27.2,35.1,26.2,35.1]:TopTop: ren34,ren40,p(x0) -> p(x1),ren11
% 105.32/21.67 === Backtracking. Learning clause 223:7:3:[219.7,222.1,40.2,47.1,123.1,122.1,214.3,43.2,53.3]:TopTopTop: ren7,ren34,ren40,p(x0),q(x1) -> c,p(x2)
% 105.32/21.67 === Backtracking. Learning clause 225:7:2:[221.4,224.1,40.2,47.1,123.1,122.1,214.3,43.2]:TopTop: ren7,ren17,ren34,ren40,p(x0) -> c,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 226:6:2:[52.1,223.5,225.2]:TopTop: ren7,ren34,ren40,p(x0) -> c,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 228:3:1:[113.0,227.0,118.1,109.1]:Top: -> ren36,ren37,p(x0)
% 105.32/21.67 === Backtracking. Learning clause 232:9:1:[53.2,229.2,216.1,230.3,63.1,231.8,97.2,94.2,179.6,91.2,69.3,66.2,31.1]:Top: ren7,ren15,ren34,ren37,ren40,p(x0),c,q(skc7) -> ren10
% 105.32/21.67 === Backtracking. Learning clause 234:2:1:[44.1,233.1,41.2,47.1]:Top: q(x0) -> ren15
% 105.32/21.67 === Conflict found: 228:3:1:[113.0,227.0,118.1,109.1]:Top: -> ren36,ren37,p(x0) {x0 -> skc31}
% 105.32/21.67 === Backtracking. Learning clause 237:6:2:[223.5,235.5,29.0,236.6,228.2,232.4,114.1,112.1,234.2]:TopTop: ren7,ren34,ren40,p(x0),q(skc7) -> p(x1)
% 105.32/21.67 === Backtracking. Learning clause 240:7:2:[221.4,238.1,225.5,239.7,97.2,94.2,91.2,189.8,49.2,69.3,63.2,216.2,66.2,228.2,114.1,112.1]:TopTop: ren7,ren15,ren17,ren34,ren40,p(x0) -> p(x1)
% 105.32/21.67 === Backtracking. Learning clause 242:2:1:[43.1,241.1,40.2,47.1]:Top: p(x0) -> ren15
% 105.32/21.67 === Conflict found: 199:6:3:[69.3,196.2,66.2,63.2,110.1]:TopTopTop: ren15,ren31,ren34,p(x0) -> p(x1),ren35(x2) {x0 -> skc1, x1 -> skc15, x2 -> skc6}
% 105.32/21.67 === Backtracking. Learning clause 244:4:2:[242.1,243.0,199.6,109.1,97.3,94.2,91.2,113.1]:TopTop: ren34,p(x0) -> p(x1),ren36
% 105.32/21.67 === Backtracking. Learning clause 248:6:3:[234.1,245.2,53.2,246.3,122.0,247.6,62.2,209.2,123.1,204.5]:TopTopTop: p(x0),ren7,ren34,q(x1) -> c,p(x2)
% 105.32/21.67 === Backtracking. Learning clause 249:5:3:[22.1,14.1,15.1,16.1,19.1,182.1,248.2]:TopTopTop: p(x0),ren34,q(x1) -> c,p(x2)
% 105.32/21.67 === Backtracking. Learning clause 250:5:2:[62.2,209.2,123.1,122.1,226.3]:TopTop: ren7,ren34,p(x0) -> c,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 251:3:2:[22.2,15.1,14.1,16.1,19.1,182.1,250.1,112.2,244.4,49.1]:TopTop: ren34 -> p(x0),ren16(x1)
% 105.32/21.67 === Backtracking. Learning clause 254:4:0:[93.0,252.0,94.0,253.4,89.1,98.1,244.2]:: ren34 -> ren30,ren31,ren36
% 105.32/21.67 === Backtracking. Learning clause 255:4:2:[26.2,244.2]:TopTop: ren9(x0),ren34 -> p(x1),ren36
% 105.32/21.67 === Backtracking. Learning clause 260:8:2:[234.1,256.1,228.1,257.5,66.1,258.8,113.0,259.9,71.2,244.2,80.1,74.1,244.2,179.5,69.3,63.2]:TopTop: ren7,ren17,ren31,ren34,ren40,q(x0) -> ren36,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 262:2:0:[63.1,261.0,69.2,66.2]:: c -> ren23
% 105.32/21.67 === Backtracking. Learning clause 264:3:0:[216.0,263.2,71.2,244.2,80.1,74.1,244.2]:: ren34 -> ren26,ren36
% 105.32/21.67 === Backtracking. Learning clause 269:8:2:[113.0,265.0,234.1,266.2,264.1,267.5,228.1,268.7,92.3,244.2,254.2,179.6]:TopTop: ren7,ren17,ren23,ren34,ren40,q(x0) -> ren36,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 272:7:2:[124.1,270.0,113.0,271.1,127.1,121.2,269.5]:TopTop: ren7,ren17,ren23,ren34,q(x0) -> ren36,p(x1)
% 105.32/21.67 === Conflict found: 189:12:2:[151.0,184.0,168.0,185.1,145.1,186.4,137.0,187.10,138.0,188.11,24.2,136.4]:TopTop: ren7,ren11,ren15,ren16(x0),ren17,ren23,ren26,ren31,ren34,ren37,ren40 -> p(x1) {x0 -> skc31, x1 -> skc22}
% 105.32/21.67 === Backtracking. Learning clause 274:11:2:[29.0,273.11,189.4,251.3,35.3]:TopTop: ren7,ren15,ren17,ren23,ren26,ren31,ren37,ren40,ren34 -> p(x0),ren9(x1)
% 105.32/21.67 === Backtracking. Learning clause 275:5:2:[39.2,244.2]:TopTop: ren13(x0),ren34 -> q(x0),p(x1),ren36
% 105.32/21.67 === Conflict found: 274:11:2:[29.0,273.11,189.4,251.3,35.3]:TopTop: ren7,ren15,ren17,ren23,ren26,ren31,ren37,ren40,ren34 -> p(x0),ren9(x1) {x0 -> skc34, x1 -> skc7}
% 105.32/21.67 === Backtracking. Learning clause 279:8:0:[264.1,276.4,228.1,277.5,94.0,278.8,274.11,255.1,254.3]:: ren7,ren15,ren17,ren23,ren40,ren34 -> ren30,ren36
% 105.32/21.67 === Backtracking. Learning clause 281:8:1:[113.0,280.0,92.3,244.2,279.7]:Top: ren7,ren15,ren17,ren23,ren40,ren34 -> p(x0),ren36
% 105.32/21.67 === Backtracking. Learning clause 282:7:1:[48.1,39.1,42.1,272.5,244.2,272.5,244.2,281.2]:Top: ren7,ren17,ren23,ren40,ren34 -> p(x0),ren36
% 105.32/21.67 === Backtracking. Learning clause 284:6:1:[113.0,283.0,127.1,121.2,124.2,282.4]:Top: ren7,ren17,ren23,ren34 -> p(x0),ren36
% 105.32/21.67 === Backtracking. Learning clause 285:4:1:[51.1,244.2,284.2,262.2,113.1]:Top: ren7,ren34 -> p(x0),ren36
% 105.32/21.67 === Backtracking. Learning clause 287:7:1:[29.0,286.5,35.3,214.2,27.1,204.6]:Top: ren7,ren15,ren17,ren34,ren40 -> c,p(x0)
% 105.32/21.67 === Backtracking. Learning clause 289:5:1:[285.3,288.4,51.1,226.4,287.3,112.2]:Top: ren7,ren15,ren34,ren40 -> p(x0)
% 105.32/21.67 === Backtracking. Learning clause 290:4:1:[39.3,234.1,48.1,42.1,234.1,242.1,242.1,289.2]:Top: ren7,ren34,ren40 -> p(x0)
% 105.32/21.67 === Backtracking. Learning clause 292:2:1:[29.0,291.0,35.1,26.1]:Top: -> ren11,p(x0)
% 105.32/21.67 === Backtracking. Learning clause 294:6:2:[234.1,293.1,107.1,100.2,103.2,204.4]:TopTop: ren7,ren17,ren40,q(x0) -> c,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 295:5:2:[22.3,16.1,14.1,15.1,19.1,182.1,294.1]:TopTop: ren17,ren40,q(x0) -> c,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 297:6:1:[292.0,296.1,107.1,100.2,103.2,214.5]:Top: ren7,ren15,ren17,ren40 -> c,p(x0)
% 105.32/21.67 === Backtracking. Learning clause 298:5:1:[22.2,15.1,14.1,16.1,19.1,182.1,297.1]:Top: ren15,ren17,ren40 -> c,p(x0)
% 105.32/21.67 === Backtracking. Learning clause 299:5:1:[107.1,101.2,103.2,289.3]:Top: c,ren7,ren15,ren40 -> p(x0)
% 105.32/21.67 === Backtracking. Learning clause 300:4:1:[22.1,14.1,16.1,15.1,19.1,182.1,299.2,298.4]:Top: ren15,ren17,ren40 -> p(x0)
% 105.32/21.67 === Backtracking. Learning clause 301:6:3:[26.2,248.1]:TopTopTop: ren9(x0),ren7,ren34,q(x1) -> c,p(x2)
% 105.32/21.67 === Backtracking. Learning clause 302:6:4:[24.1,248.1]:TopTopTopTop: ren7,ren34,q(x0) -> ren8(x1,x2),c,p(x3)
% 105.32/21.67 === Backtracking. Learning clause 304:5:2:[103.1,303.2,120.1,248.1,127.1,123.2,249.1,107.3,100.2]:TopTop: ren7,q(x0) -> ren40,c,p(x1)
% 105.32/21.67 === Backtracking. Learning clause 305:4:1:[120.1,250.3,127.1,123.2,250.3,107.3,103.2,100.2]:Top: ren7 -> ren40,c,p(x0)
% 105.32/21.67 === Backtracking. Learning clause 306:3:1:[127.1,121.2,124.2,305.3]:Top: ren7 -> ren40,p(x0)
% 105.32/21.67 === Backtracking. Learning clause 307:3:1:[22.2,15.1,16.1,14.1,19.1,182.1,306.1,300.3]:Top: ren15,ren17 -> p(x0)
% 105.32/21.67 === Backtracking. Learning clause 308:2:1:[53.2,52.1,51.1,307.2]:Top: ren15 -> p(x0)
% 105.32/21.67 === Backtracking. Learning clause 309:2:1:[107.2,103.2,100.2,290.2,242.1,308.1,306.2]:Top: ren7 -> p(x0)
% 105.32/21.67 === Backtracking. Learning clause 310:1:1:[22.3,16.1,14.1,15.1,19.1,182.1,309.1]:Top: -> p(x0)
% 105.32/21.67 === Backtracking. Learning clause 311:2:1:[119.2,310.1]:Top: ren38(x0) -> c
% 105.32/21.67 === Backtracking. Learning clause 312:2:1:[65.1,310.1,164.1,101.1]:Top: -> ren34,ren32(x0)
% 105.32/21.67 === Backtracking. Learning clause 314:1:0:[310.0,313.0,104.2,107.2,99.3,312.2]:: -> ren34
% 105.32/21.67 === Backtracking. Learning clause 315:2:0:[65.1,310.1,157.2]:: ren33 -> c
% 105.32/21.67 === Backtracking. Learning clause 317:2:0:[292.1,316.0,28.2,30.2,34.1,31.3,310.1]:: q(skc7) -> ren11
% 105.32/21.67 === Conflict found: 136:17:2:[131.1,129.9,132.1,134.10,133.1,135.11]:TopTop: ren3,ren4,ren7,ren8(skf37(x0),x0),ren11,ren12,ren15,ren16(x1),ren17,ren23,ren26,ren27,ren28,ren31,ren34,ren37,ren40 -> {x0 -> skc3, x1 -> skc10}
% 105.32/21.67 === Backtracking. Learning clause 322:7:0:[158.1,318.3,160.0,319.4,162.0,320.5,164.1,321.6,136.13,138.1,25.2,167.2,137.1,30.2,146.1,151.1,168.1,31.3,310.1,166.1,317.2,27.2]:: ren7,ren15,ren17,ren40,ren22,ren9(skc7) -> c
% 105.32/21.67 === Backtracking. Learning clause 323:2:1:[30.1,35.2,317.1]:Top: -> ren9(x0),ren11
% 105.32/21.67 === Backtracking. Learning clause 324:2:0:[31.1,310.1]:: q(skc7) -> ren10
% 105.32/21.67 === Conflict found: 130:2:2:[25.0,23.1]:TopTop: p(x0) -> ren8(x0,x1) {x0 -> skf37(skc1), x1 -> skc1}
% 105.32/21.67 === Backtracking. Learning clause 327:5:0:[314.0,325.0,297.5,326.1,130.1,310.1,136.4,216.2,162.1,158.2,138.1,167.2,137.1,146.1,151.1,168.1,166.1,323.2,322.6,65.2,310.1]:: ren7,ren15,ren17,ren40 -> c
% 105.32/21.67 === Conflict found: 323:2:1:[30.1,35.2,317.1]:Top: -> ren9(x0),ren11 {x0 -> skc7}
% 105.32/21.67 === Backtracking. Learning clause 328:2:1:[323.1,27.1]:Top: -> ren11,q(x0)
% 105.32/21.67 === Backtracking. Learning clause 330:4:0:[308.1,329.0,52.1,53.2,327.3]:: ren7,ren15,ren40 -> c
% 105.32/21.67 === Conflict found: 317:2:0:[292.1,316.0,28.2,30.2,34.1,31.3,310.1]:: q(skc7) -> ren11 {}
% 105.32/21.67 === Backtracking. Learning clause 331:1:0:[317.1,328.2]:: -> ren11
% 105.32/21.67 === Conflict found: 327:5:0:[314.0,325.0,297.5,326.1,130.1,310.1,136.4,216.2,162.1,158.2,138.1,167.2,137.1,146.1,151.1,168.1,166.1,323.2,322.6,65.2,310.1]:: ren7,ren15,ren17,ren40 -> c {}
% 105.32/21.67 === Backtracking. Learning clause 332:5:2:[327.2,234.2,101.1]:TopTop: ren7,ren17,ren40,q(x0) -> ren32(x1)
% 105.32/21.67 === Backtracking. Learning clause 333:2:0:[91.1,310.1,97.1]:: ren30 -> ren31
% 105.32/21.67 === Backtracking. Learning clause 334:1:0:[111.1,310.1,117.1,114.2,310.1]:: -> ren37
% 105.32/21.67 === Backtracking. Learning clause 336:4:0:[307.2,335.0,128.2,122.1,311.1,327.4]:: ren7,ren15,ren17 -> c
% 105.32/21.67 === Backtracking. Learning clause 337:2:1:[22.2,15.1,14.1,16.1,19.1,182.1,336.1,53.3,310.1,234.2]:Top: q(x0) -> c
% 105.32/21.67 === Backtracking. Learning clause 338:2:0:[128.2,122.1,311.1,330.3,242.2,310.1]:: ren7 -> c
% 105.32/21.67 === Backtracking. Learning clause 339:1:1:[22.3,16.1,15.1,14.1,19.1,182.1,338.1,101.1]:Top: -> ren32(x0)
% 105.32/21.67 === Backtracking. Learning clause 341:2:1:[310.0,340.1,97.2,94.2]:Top: ren29(x0) -> ren31
% 105.32/21.67 === Backtracking. Learning clause 346:3:1:[331.0,342.1,234.1,343.2,337.1,344.4,309.1,345.5,50.1,310.1,136.8,130.2,310.1,341.2,91.2,310.1,216.2,262.2,138.1,137.1,146.1,151.1,168.1,314.1,334.1,53.3]:Top: ren7,ren40,q(x0) ->
% 105.32/21.67 === Backtracking. Learning clause 347:1:0:[91.1,310.1,341.1]:: -> ren31
% 105.32/21.67 === Backtracking. Learning clause 349:2:1:[337.1,348.0,127.2,124.2,121.2,346.2]:Top: ren7,q(x0) ->
% 105.32/21.67 === Backtracking. Learning clause 355:3:0:[331.0,350.1,242.1,351.2,347.0,352.4,309.1,353.6,338.1,354.7,50.1,310.1,136.8,130.2,310.1,216.2,262.2,137.1,138.1,146.1,151.1,168.1,314.1,334.1]:: ren7,ren17,ren40 ->
% 105.32/21.67 === Backtracking. Learning clause 356:2:0:[52.1,349.2,355.2]:: ren7,ren40 ->
% 105.32/21.67 === Backtracking. Learning clause 357:1:0:[127.2,124.2,121.2,338.2,356.2]:: ren7 ->
% 105.32/21.67
% 105.32/21.67 SZS status Unsatisfiable
% 105.32/21.67
% 105.32/21.67 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 105.32/21.67
% 105.32/21.67 SPASS-SCL-FOL Statistics:
% 105.32/21.67 Number of learned clauses: 121
% 105.32/21.67 Number of propagations: 5218
% 105.32/21.67 Number of decisions: 894
% 105.32/21.67 Number of resolutions: 467
% 105.32/21.67 Number of condensations: 41
% 105.32/21.67 Number of sub resolutions: 107
% 105.32/21.67 Number of input literals (deduplicated): 84
% 105.32/21.67 Number of grows: 6
% 105.32/21.67 Number of considered ground atoms: 418
% 105.32/21.67
% 105.32/21.67 Needed: 0:0:21.14
% 105.32/21.67
%------------------------------------------------------------------------------