%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN475+1 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:51 PM UTC 2026
% Result : Theorem 6.94s 2.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN475+1 : TPTP v9.2.1. Released v2.1.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n018.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:43:02 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 6.94/2.21 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.94/2.21 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.94/2.21 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.94/2.21 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.94/2.21 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.94/2.21 Execution resolution_2 ended with status: unsatisfiable
% 6.94/2.21 Used heuristic: resolution_2
% 6.94/2.21
% 6.94/2.21 Input Clauses:
% 6.94/2.21
% 6.94/2.21 Predicates: hskp0 ndr1_0 c0_1 c2_1 c3_1 hskp1 c1_1 hskp2 hskp3 hskp4 hskp5 hskp6 hskp7 hskp8 hskp9 hskp10 hskp11 hskp12 hskp13 hskp14 hskp15 hskp16 hskp17 hskp18 hskp19 hskp20 hskp21 hskp22 hskp23 hskp24 hskp25 hskp26 hskp27 hskp28 hskp29 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
% 6.94/2.21 Fol Constants: a1000 a1001 a1002 a1003 a1004 a1005 a1006 a1008 a1010 a1011 a1012 a1015 a1019 a1023 a1025 a1026 a1030 a1032 a1036 a1037 a1038 a1041 a1043 a1044 a1045 a1048 a1052 a1029 a1033 a1040
% 6.94/2.21 Fol Functions:
% 6.94/2.21 Problem Properties:
% 6.94/2.21 This is a Bernays Schoenfinkel problem.
% 6.94/2.21
% 6.94/2.21 After reduction: Problem Properties:
% 6.94/2.21 This is a Bernays Schoenfinkel problem.
% 6.94/2.21
% 6.94/2.21
% 6.94/2.21 Reduced Input Clauses:
% 6.94/2.21
% 6.94/2.21 Most General Atoms: ren1 ndr1_0 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 hskp0 hskp1 hskp2 hskp3 hskp4 hskp5 hskp6 hskp7 hskp8 hskp9 hskp10 hskp11 hskp12 hskp13 hskp14 hskp15 hskp16 hskp17 hskp18 hskp19 hskp20 hskp21 hskp22 hskp23 hskp24 hskp25 hskp26 hskp27 hskp28 hskp29 c0_1(x1) c2_1(x1) c1_1(x1) c3_1(x2)
% 6.94/2.21
% 6.94/2.21 === Starting SPASS-SCL-FOL A Little Less Naive, considering 181 atoms initially, heuristics mode: resolution_2 ===
% 6.94/2.21
% 6.94/2.21 === Backtracking. Learning clause 223:4:0:[213.3,205.4,117.2,118.2,120.2,150.2,216.1,147.1,107.1]:: c0_1(a1052) -> hskp19,hskp23,hskp3
% 6.94/2.21 === Backtracking. Learning clause 224:7:1:[162.7,52.2,50.2,51.2,133.2,215.2,180.3,105.2,147.2,216.3,150.1,118.1]:Top: c1_1(x0),c3_1(x0) -> hskp0,hskp5,c0_1(x0),hskp3,c0_1(a1040)
% 6.94/2.21 === Backtracking. Learning clause 225:6:1:[205.4,213.3,117.2,150.2,216.1,147.1]:Top: c0_1(x0),c3_1(x0) -> hskp23,hskp19,hskp3,ren27
% 6.94/2.21 === Backtracking. Learning clause 226:10:1:[197.3,35.2,34.2,36.2,129.2,165.8,31.2,32.2,30.2,128.2,211.5,205.2,205.4,105.2,225.6,224.5]:Top: c1_1(x0),c3_1(x0),c1_1(a1040),c3_1(a1040) -> c2_1(x0),hskp23,hskp19,hskp0,hskp5,hskp3
% 6.94/2.21 === Backtracking. Learning clause 227:2:0:[150.2,117.1,216.1,147.1,105.1]:: -> hskp3,ndr1_0
% 6.94/2.21 === Backtracking. Learning clause 228:10:1:[120.2,226.4,150.2,216.1,147.1]:Top: c1_1(x0),c3_1(x0),c1_1(a1040) -> c2_1(x0),hskp23,hskp19,hskp0,hskp5,hskp3,ren27
% 6.94/2.21 === Backtracking. Learning clause 230:9:2:[227.1,229.3,197.3,35.2,34.2,36.2,129.2,165.8,32.2,30.2,31.2,128.2,211.5,168.5,205.2]:TopTop: c2_1(x0),c1_1(x0),c1_1(x1),c3_1(x1) -> c3_1(x0),hskp11,c2_1(x1),hskp23,hskp3
% 6.94/2.21 === Backtracking. Learning clause 231:6:1:[197.4,36.2,34.2,35.2,129.2,167.5,128.1,32.1]:Top: ndr1_0,c1_1(x0),c3_1(a1008) -> hskp23,c0_1(x0),c2_1(x0)
% 6.94/2.21 === Backtracking. Learning clause 233:7:1:[231.2,232.4,165.3,30.2,31.2,128.2,167.6,129.1,36.1,197.4]:Top: c1_1(x0),ndr1_0,c0_1(a1010),c3_1(a1010) -> c0_1(x0),c2_1(x0),hskp23
% 6.94/2.21 === Backtracking. Learning clause 235:6:1:[231.2,234.3,165.6,31.2,30.2,128.2,167.6,129.1,35.1,233.4]:Top: c1_1(x0),ndr1_0,c0_1(a1010) -> c0_1(x0),c2_1(x0),hskp23
% 6.94/2.21 === Backtracking. Learning clause 236:5:1:[165.7,231.3,30.2,31.2,128.2,167.6,129.1,34.1,235.3,205.2,227.2,124.1,15.1]:Top: c1_1(x0),c3_1(x0),c0_1(a1003) -> c2_1(x0),hskp23
% 6.94/2.21 === Backtracking. Learning clause 237:2:0:[197.1,33.2,36.2,35.2,34.2,129.2]:: hskp8 -> hskp23
% 6.94/2.21 === Backtracking. Learning clause 238:4:1:[124.2,13.1,227.1,197.1]:Top: c0_1(x0),c3_1(x0) -> c1_1(x0),hskp23
% 6.94/2.21 === Backtracking. Learning clause 239:1:0:[124.2,13.1,227.1]:: -> ndr1_0
% 6.94/2.21 === Backtracking. Learning clause 241:5:1:[13.1,240.0,165.1,14.2,16.2,15.2]:Top: c2_1(x0),ren4 -> c1_1(x0),c3_1(x0),hskp8
% 6.94/2.21 === Backtracking. Learning clause 244:10:2:[120.1,242.1,117.1,243.4,165.5,180.3,180.4,62.2,63.2,64.2,136.2,181.8,100.2,98.2,99.2,145.2,212.5,119.2]:TopTop: c2_1(a1040),c0_1(x0),c3_1(x0),c0_1(x1),c2_1(x1),c3_1(x1),ren30 -> hskp8,c1_1(x0),hskp3
% 6.94/2.21 === Backtracking. Learning clause 246:6:1:[227.1,245.0,203.3,119.2,244.1,120.2,118.2,150.2,216.1,147.1]:Top: c0_1(x0),c3_1(x0) -> hskp8,c1_1(x0),hskp3,ren27
% 6.94/2.21 === Conflict found: 244:10:2:[120.1,242.1,117.1,243.4,165.5,180.3,180.4,62.2,63.2,64.2,136.2,181.8,100.2,98.2,99.2,145.2,212.5,119.2]:TopTop: c2_1(a1040),c0_1(x0),c3_1(x0),c0_1(x1),c2_1(x1),c3_1(x1),ren30 -> hskp8,c1_1(x0),hskp3 {x0 -> a1010, x1 -> a1040}
% 6.94/2.21 === Backtracking. Learning clause 247:7:1:[244.6,120.2,118.2,150.2]:Top: c0_1(x0),c3_1(x0),c2_1(a1040),hskp29 -> hskp8,c1_1(x0),hskp3
% 6.94/2.21 === Backtracking. Learning clause 249:7:2:[105.1,248.2,157.8,108.2,106.2,107.2,180.1]:TopTop: c2_1(x0),ren27,c2_1(x1),c3_1(x1) -> c1_1(x0),c3_1(x0),c0_1(x1)
% 6.94/2.21 === Backtracking. Learning clause 251:11:3:[105.1,250.3,151.5,165.1,171.5,106.2,108.2,107.2]:TopTopTop: c1_1(x0),c0_1(x1),c3_1(x1),c2_1(x2),ren27 -> c1_1(x2),hskp8,c0_1(x0),c3_1(x0),c1_1(x1),c3_1(x2)
% 6.94/2.21 === Backtracking. Learning clause 253:10:3:[105.1,252.0,157.6,165.1,106.2,108.2,107.2,251.1,249.4]:TopTopTop: c0_1(x0),c3_1(x0),c2_1(x1),ren27,c2_1(x2) -> hskp8,c1_1(x0),c1_1(x1),c3_1(x1),c0_1(x2)
% 6.94/2.21 === Backtracking. Learning clause 255:7:2:[239.0,254.1,165.5,180.3]:TopTop: c2_1(x0),c1_1(x1),c3_1(x1) -> c1_1(x0),c3_1(x0),hskp8,c0_1(x1)
% 6.94/2.21 === Backtracking. Learning clause 257:5:1:[239.0,256.0,157.6,255.2,108.2,106.2,107.2,246.6,124.1,241.2,32.2,31.2,30.2,128.2]:Top: c0_1(x0),c3_1(x0),hskp7 -> c1_1(x0),hskp8
% 6.94/2.21 === Backtracking. Learning clause 260:5:1:[239.0,258.0,257.2,259.4,167.4,16.2,14.2,15.2,124.2,246.5,107.1]:Top: c0_1(x0),c3_1(x0),c0_1(a1052) -> hskp8,c1_1(x0)
% 6.94/2.21 === Backtracking. Learning clause 262:5:1:[13.1,261.0,167.4,16.2,14.2,15.2,257.3]:Top: ren4,c0_1(x0),c3_1(x0) -> c1_1(x0),hskp8
% 6.94/2.21 === Backtracking. Learning clause 264:4:1:[239.0,263.0,211.4,116.2,114.2,115.2,149.2,188.5,167.2,108.2,106.2,246.6,124.1,257.3,260.3,262.1]:Top: c0_1(x0),c3_1(x0) -> c1_1(x0),hskp8
% 6.94/2.21 === Backtracking. Learning clause 266:3:0:[13.1,265.0,165.7,32.2,31.2,30.2,14.2,16.2,128.2,15.2]:: hskp7,ren4 -> hskp8
% 6.94/2.21 === Backtracking. Learning clause 268:2:0:[13.1,267.0,167.4,16.2,14.2,15.2,266.1]:: ren4 -> hskp8
% 6.94/2.21 === Backtracking. Learning clause 270:5:1:[239.0,269.0,203.6,147.1]:Top: c0_1(x0),c1_1(x0) -> c2_1(x0),hskp8,ren27
% 6.94/2.21 === Backtracking. Learning clause 271:3:0:[150.1,216.1,118.1]:: -> hskp3,hskp26,c0_1(a1040)
% 6.94/2.21 === Conflict found: 255:7:2:[239.0,254.1,165.5,180.3]:TopTop: c2_1(x0),c1_1(x1),c3_1(x1) -> c1_1(x0),c3_1(x0),hskp8,c0_1(x1) {x0 -> a1008, x1 -> a1045}
% 6.94/2.21 === Backtracking. Learning clause 273:8:2:[227.1,272.1,255.7,100.2,98.2,99.2,145.2,212.5,270.3,264.3]:TopTop: c2_1(x0),c0_1(x1),c3_1(x1) -> c1_1(x0),c3_1(x0),hskp3,ren27,hskp8
% 6.94/2.21 === Conflict found: 271:3:0:[150.1,216.1,118.1]:: -> hskp3,hskp26,c0_1(a1040) {}
% 6.94/2.21 === Backtracking. Learning clause 274:3:0:[271.2,147.1]:: -> hskp3,c0_1(a1040),ren27
% 6.94/2.21 === Conflict found: 273:8:2:[227.1,272.1,255.7,100.2,98.2,99.2,145.2,212.5,270.3,264.3]:TopTop: c2_1(x0),c0_1(x1),c3_1(x1) -> c1_1(x0),c3_1(x0),hskp3,ren27,hskp8 {x0 -> a1008, x1 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 275:6:1:[273.5,32.2,30.2,31.2,128.2]:Top: c0_1(x0),c3_1(x0),hskp7 -> hskp3,ren27,hskp8
% 6.94/2.21 === Backtracking. Learning clause 276:4:0:[120.2,275.2,150.2,216.1,147.1,274.2,107.1]:: hskp7,c0_1(a1052) -> hskp8,hskp3
% 6.94/2.21 === Backtracking. Learning clause 279:4:0:[227.1,277.0,276.1,278.3,157.6,255.2,32.2,30.2,31.2,128.2,108.2,106.2,274.3]:: hskp7 -> hskp8,hskp3,c0_1(a1040)
% 6.94/2.21 === Backtracking. Learning clause 283:4:0:[279.3,280.0,29.1,281.1,128.1,282.4,120.2,275.2,150.2,216.1,147.1,249.2,157.8,255.2,32.2,276.2,30.2,31.2]:: c3_1(a1052),hskp7 -> hskp8,hskp3
% 6.94/2.21 === Backtracking. Learning clause 285:2:0:[266.1,284.2,120.2,275.2,150.2,216.1,147.1,279.4,106.1,283.1,124.1]:: hskp7 -> hskp8
% 6.94/2.21 === Conflict found: 264:4:1:[239.0,263.0,211.4,116.2,114.2,115.2,149.2,188.5,167.2,108.2,106.2,246.6,124.1,257.3,260.3,262.1]:Top: c0_1(x0),c3_1(x0) -> c1_1(x0),hskp8 {x0 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 287:5:1:[239.0,286.1,264.3,203.3]:Top: c3_1(x0),c0_1(x0) -> c2_1(x0),hskp8,hskp26
% 6.94/2.21 === Backtracking. Learning clause 288:3:0:[124.1,274.1,268.1]:: -> c0_1(a1040),ren27,hskp8
% 6.94/2.21 === Backtracking. Learning clause 292:5:1:[227.1,289.0,275.2,290.3,147.0,291.4,211.4,287.3,246.4]:Top: c0_1(x0),c3_1(x0) -> hskp8,hskp3,ren27
% 6.94/2.21 === Backtracking. Learning clause 293:2:0:[120.2,292.2,150.2,216.1,124.1,268.1,147.1,288.1]:: -> ren27,hskp8
% 6.94/2.21 === Backtracking. Learning clause 295:4:1:[239.0,294.0,211.4,116.2,115.2,114.2,149.2,188.5,285.1]:Top: c3_1(x0) -> c1_1(x0),c2_1(x0),hskp8
% 6.94/2.21 === Backtracking. Learning clause 297:1:0:[239.0,296.0,167.6,285.1,295.2,108.2,106.2,107.2,293.1,129.1]:: -> ren9
% 6.94/2.21 === Backtracking. Learning clause 299:12:4:[239.0,298.5,157.1,46.2,47.2,48.2,132.2,175.8,157.1,154.2,64.2,62.2,63.2,136.2,181.8,196.7]:TopTopTopTop: c2_1(x0),c0_1(x1),c3_1(x1),c0_1(x2),c1_1(x2),c1_1(x3),c3_1(x3) -> c3_1(x0),c0_1(x3),c1_1(x0),c1_1(x1),c2_1(x2)
% 6.94/2.21 === Backtracking. Learning clause 301:17:6:[239.0,300.9,199.10,196.8,154.9]:TopTopTopTopTopTop: c2_1(x0),c3_1(x0),c0_1(x1),c3_1(x1),c0_1(x2),c3_1(x2),c2_1(x3),c0_1(x4),c2_1(x4),c0_1(x5),c1_1(x5) -> c1_1(x0),c2_1(x1),c1_1(x2),c0_1(x3),c1_1(x3),c2_1(x5)
% 6.94/2.21 === Conflict found: 299:12:4:[239.0,298.5,157.1,46.2,47.2,48.2,132.2,175.8,157.1,154.2,64.2,62.2,63.2,136.2,181.8,196.7]:TopTopTopTop: c2_1(x0),c0_1(x1),c3_1(x1),c0_1(x2),c1_1(x2),c1_1(x3),c3_1(x3) -> c3_1(x0),c0_1(x3),c1_1(x0),c1_1(x1),c2_1(x2) {x0 -> a1008, x1 -> a1052, x2 -> a1033, x3 -> a1045}
% 6.94/2.21 === Backtracking. Learning clause 303:10:3:[239.0,302.3,299.7,99.2,98.2,100.2,145.2,198.5,136.1,63.1]:TopTopTop: c2_1(x0),c0_1(x1),c1_1(x1),c0_1(x2),c3_1(x2),c0_1(a1026) -> c3_1(x0),c1_1(x0),c2_1(x1),c1_1(x2)
% 6.94/2.21 === Backtracking. Learning clause 305:4:1:[239.0,304.0,181.6,100.2,99.2,98.2,145.2,198.5,136.1]:Top: c0_1(x0),c3_1(x0) -> c1_1(x0),ren16
% 6.94/2.21 === Backtracking. Learning clause 306:7:2:[181.3,239.1]:TopTop: c1_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c0_1(x0),c1_1(x1),hskp15
% 6.94/2.21 === Backtracking. Learning clause 307:5:1:[181.1,98.2,100.2,145.2,198.5,239.1]:Top: c3_1(a1045),c0_1(x0),c3_1(x0) -> c1_1(x0),hskp15
% 6.94/2.21 === Backtracking. Learning clause 308:4:1:[198.1,239.1,145.1,99.1,307.1]:Top: c0_1(x0),c3_1(x0) -> c1_1(x0),hskp15
% 6.94/2.21 === Backtracking. Learning clause 311:11:4:[157.7,309.2,239.0,310.5,157.8,180.3,180.6,157.8]:TopTopTopTop: c1_1(x0),c3_1(x0),c3_1(x1),c3_1(x2),c2_1(x3) -> c0_1(x0),c0_1(x1),c0_1(x2),c1_1(x2),c1_1(x3),c3_1(x3)
% 6.94/2.21 === Conflict found: 311:11:4:[157.7,309.2,239.0,310.5,157.8,180.3,180.6,157.8]:TopTopTopTop: c1_1(x0),c3_1(x0),c3_1(x1),c3_1(x2),c2_1(x3) -> c0_1(x0),c0_1(x1),c0_1(x2),c1_1(x2),c1_1(x3),c3_1(x3) {x0 -> a1045, x1 -> a1015, x2 -> a1015, x3 -> a1008}
% 6.94/2.21 === Backtracking. Learning clause 314:8:2:[61.1,312.0,305.3,313.5,311.9,48.2,46.2,47.2,132.2,175.8,62.2,311.3,64.2,32.2,31.2,30.2,128.2]:TopTop: c0_1(x0),c3_1(x0),c1_1(x1),c3_1(x1),hskp7 -> c1_1(x0),c0_1(x1),c0_1(a1026)
% 6.94/2.21 === Backtracking. Learning clause 318:10:3:[61.1,315.5,63.1,316.10,64.1,317.11,180.8,199.10,62.2]:TopTopTop: c1_1(x0),c3_1(x0),c3_1(a1026),c0_1(x1),c3_1(x1),c1_1(x2),c2_1(x2),ren16 -> c0_1(x0),c2_1(x1)
% 6.94/2.21 === Backtracking. Learning clause 320:12:3:[61.1,319.0,163.5,318.7]:TopTopTop: c3_1(x0),c1_1(x1),c3_1(x1),c3_1(a1026),c0_1(x2),c3_1(x2),ren16 -> c1_1(x0),c2_1(x0),hskp7,c0_1(x1),c2_1(x2)
% 6.94/2.21 === Backtracking. Learning clause 322:17:5:[239.0,321.8,170.3,151.6,80.2,79.2,78.2,140.2,213.6,180.3,180.8]:TopTopTopTopTop: c2_1(x0),c0_1(x1),c2_1(x1),c3_1(x1),c1_1(x2),c3_1(x2),c2_1(x3),c3_1(x3),c1_1(x4),c2_1(x4) -> c0_1(x4),hskp7,c0_1(x0),c1_1(x0),hskp26,c0_1(x2),c0_1(x3)
% 6.94/2.21 === Backtracking. Learning clause 324:17:5:[239.0,323.1,151.6,311.5,79.2,78.2,80.2,140.2,213.6,180.3,322.9]:TopTopTopTopTop: c3_1(x0),c2_1(x1),c0_1(x2),c2_1(x2),c3_1(x2),c1_1(x3),c3_1(x3),c2_1(x4),c3_1(x4) -> c0_1(x0),c1_1(x0),hskp7,c0_1(x1),c1_1(x1),hskp26,c0_1(x3),c0_1(x4)
% 6.94/2.21 === Conflict found: 322:17:5:[239.0,321.8,170.3,151.6,80.2,79.2,78.2,140.2,213.6,180.3,180.8]:TopTopTopTopTop: c2_1(x0),c0_1(x1),c2_1(x1),c3_1(x1),c1_1(x2),c3_1(x2),c2_1(x3),c3_1(x3),c1_1(x4),c2_1(x4) -> c0_1(x4),hskp7,c0_1(x0),c1_1(x0),hskp26,c0_1(x2),c0_1(x3) {x0 -> a1026, x1 -> a1052, x2 -> a1045, x3 -> a1026, x4 -> a1040}
% 6.94/2.21 === Backtracking. Learning clause 328:12:3:[318.9,325.1,64.1,326.11,63.1,327.14,322.1,62.2]:TopTopTop: c0_1(x0),c3_1(x0),c1_1(x1),c3_1(x1),c3_1(a1026),c1_1(x2),c2_1(x2),ren16 -> c0_1(x2),hskp7,hskp26,c0_1(x1)
% 6.94/2.21 === Conflict found: 324:17:5:[239.0,323.1,151.6,311.5,79.2,78.2,80.2,140.2,213.6,180.3,322.9]:TopTopTopTopTop: c3_1(x0),c2_1(x1),c0_1(x2),c2_1(x2),c3_1(x2),c1_1(x3),c3_1(x3),c2_1(x4),c3_1(x4) -> c0_1(x0),c1_1(x0),hskp7,c0_1(x1),c1_1(x1),hskp26,c0_1(x3),c0_1(x4) {x0 -> a1026, x1 -> a1026, x2 -> a1052, x3 -> a1045, x4 -> a1026}
% 6.94/2.21 === Backtracking. Learning clause 331:10:2:[305.3,329.5,314.4,330.10,324.4,320.9,62.2]:TopTop: c1_1(x0),c3_1(x0),c3_1(a1026),c0_1(x1),c3_1(x1) -> c1_1(a1026),hskp26,c0_1(a1026),c1_1(x1),c0_1(x0)
% 6.94/2.21 === Backtracking. Learning clause 333:7:2:[239.0,332.2,180.2,170.5]:TopTop: c2_1(x0),c1_1(x0),c2_1(x1) -> c0_1(x0),c1_1(x1),c3_1(x1),hskp7
% 6.94/2.21 === Conflict found: 311:11:4:[157.7,309.2,239.0,310.5,157.8,180.3,180.6,157.8]:TopTopTopTop: c1_1(x0),c3_1(x0),c3_1(x1),c3_1(x2),c2_1(x3) -> c0_1(x0),c0_1(x1),c0_1(x2),c1_1(x2),c1_1(x3),c3_1(x3) {x0 -> a1045, x1 -> a1045, x2 -> a1015, x3 -> a1040}
% 6.94/2.21 === Backtracking. Learning clause 336:12:4:[239.0,334.1,311.7,335.2,311.9,48.2,46.2,47.2,132.2,175.8,311.4,333.2]:TopTopTopTop: c2_1(x0),c3_1(x1),c1_1(x2),c3_1(x2),c2_1(x3) -> c0_1(x0),c3_1(x0),c1_1(x1),c0_1(x2),c1_1(x3),c3_1(x3),hskp7
% 6.94/2.21 === Backtracking. Learning clause 339:13:3:[239.0,337.5,314.4,338.8,170.7,331.3,180.2]:TopTopTop: c2_1(a1026),c1_1(x0),c3_1(x0),c0_1(x1),c3_1(x1),c1_1(x2),c2_1(x2) -> c1_1(a1026),hskp26,c0_1(a1026),c1_1(x1),c0_1(x0),c0_1(x2)
% 6.94/2.21 === Conflict found: 336:12:4:[239.0,334.1,311.7,335.2,311.9,48.2,46.2,47.2,132.2,175.8,311.4,333.2]:TopTopTopTop: c2_1(x0),c3_1(x1),c1_1(x2),c3_1(x2),c2_1(x3) -> c0_1(x0),c3_1(x0),c1_1(x1),c0_1(x2),c1_1(x3),c3_1(x3),hskp7 {x0 -> a1026, x1 -> a1052, x2 -> a1040, x3 -> a1026}
% 6.94/2.21 === Backtracking. Learning clause 341:10:2:[314.4,340.5,336.7,331.3]:TopTop: c2_1(a1026),c1_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c1_1(a1026),hskp26,c0_1(a1026),c1_1(x1),c0_1(x0)
% 6.94/2.21 === Conflict found: 341:10:2:[314.4,340.5,336.7,331.3]:TopTop: c2_1(a1026),c1_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c1_1(a1026),hskp26,c0_1(a1026),c1_1(x1),c0_1(x0) {x0 -> a1040, x1 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 343:9:2:[305.3,342.4,341.1,62.2]:TopTop: c1_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c1_1(a1026),hskp26,c0_1(a1026),c1_1(x1),c0_1(x0)
% 6.94/2.21 === Conflict found: 324:17:5:[239.0,323.1,151.6,311.5,79.2,78.2,80.2,140.2,213.6,180.3,322.9]:TopTopTopTopTop: c3_1(x0),c2_1(x1),c0_1(x2),c2_1(x2),c3_1(x2),c1_1(x3),c3_1(x3),c2_1(x4),c3_1(x4) -> c0_1(x0),c1_1(x0),hskp7,c0_1(x1),c1_1(x1),hskp26,c0_1(x3),c0_1(x4) {x0 -> a1026, x1 -> a1026, x2 -> a1052, x3 -> a1045, x4 -> a1026}
% 6.94/2.21 === Backtracking. Learning clause 346:9:2:[62.1,344.0,305.3,345.2,324.11,64.2,320.9,314.5]:TopTop: c3_1(a1026),c0_1(x0),c3_1(x0),c1_1(x1),c3_1(x1) -> hskp26,c1_1(x0),c0_1(x1),c0_1(a1026)
% 6.94/2.21 === Conflict found: 336:12:4:[239.0,334.1,311.7,335.2,311.9,48.2,46.2,47.2,132.2,175.8,311.4,333.2]:TopTopTopTop: c2_1(x0),c3_1(x1),c1_1(x2),c3_1(x2),c2_1(x3) -> c0_1(x0),c3_1(x0),c1_1(x1),c0_1(x2),c1_1(x3),c3_1(x3),hskp7 {x0 -> a1026, x1 -> a1052, x2 -> a1045, x3 -> a1026}
% 6.94/2.21 === Backtracking. Learning clause 348:5:1:[99.1,347.0,336.10,64.2,314.5,62.2,346.1,63.2,305.4,147.1,98.2,100.2]:Top: c0_1(x0),c3_1(x0),ren25 -> c1_1(x0),ren27
% 6.94/2.21 === Backtracking. Learning clause 349:7:2:[63.2,314.8,305.4]:TopTop: c1_1(x0),c3_1(x0),hskp7,c0_1(x1),c3_1(x1) -> c0_1(x0),c1_1(x1)
% 6.94/2.21 === Conflict found: 322:17:5:[239.0,321.8,170.3,151.6,80.2,79.2,78.2,140.2,213.6,180.3,180.8]:TopTopTopTopTop: c2_1(x0),c0_1(x1),c2_1(x1),c3_1(x1),c1_1(x2),c3_1(x2),c2_1(x3),c3_1(x3),c1_1(x4),c2_1(x4) -> c0_1(x4),hskp7,c0_1(x0),c1_1(x0),hskp26,c0_1(x2),c0_1(x3) {x0 -> a1026, x1 -> a1052, x2 -> a1040, x3 -> a1040, x4 -> a1040}
% 6.94/2.21 === Backtracking. Learning clause 351:15:4:[349.2,350.13,322.15,147.1,63.2,320.9,64.2,305.4]:TopTopTopTop: c2_1(a1026),c2_1(x0),c3_1(x0),c1_1(x1),c2_1(x1),c1_1(x2),c3_1(x2),c3_1(a1026),c0_1(x3),c3_1(x3) -> c0_1(x1),c0_1(x0),ren27,c0_1(x2),c1_1(x3)
% 6.94/2.21 === Conflict found: 343:9:2:[305.3,342.4,341.1,62.2]:TopTop: c1_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c1_1(a1026),hskp26,c0_1(a1026),c1_1(x1),c0_1(x0) {x0 -> a1040, x1 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 352:7:2:[343.6,147.1,63.2,64.2,305.4]:TopTop: c1_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c0_1(x0),ren27,c1_1(x1)
% 6.94/2.21 === Backtracking. Learning clause 353:9:3:[199.5,239.1]:TopTopTop: c2_1(x0),c3_1(x0),c0_1(x1),c3_1(x1),c1_1(x2),c2_1(x2) -> c1_1(x0),c2_1(x1),c3_1(x2)
% 6.94/2.21 === Backtracking. Learning clause 354:12:4:[199.3,26.2,27.2,28.2,127.2,172.8,239.1,353.8]:TopTopTopTop: c1_1(x0),c2_1(x1),c3_1(x1),c0_1(x2),c3_1(x2),c1_1(x3),c2_1(x3) -> c1_1(x2),c0_1(x0),c3_1(x0),c1_1(x1),c3_1(x3)
% 6.94/2.21 === Conflict found: 353:9:3:[199.5,239.1]:TopTopTop: c2_1(x0),c3_1(x0),c0_1(x1),c3_1(x1),c1_1(x2),c2_1(x2) -> c1_1(x0),c2_1(x1),c3_1(x2) {x0 -> a1026, x1 -> a1052, x2 -> a1004}
% 6.94/2.21 === Backtracking. Learning clause 355:9:3:[353.6,19.2,18.2,20.2,125.2,156.8,239.1]:TopTopTop: c2_1(x0),c3_1(x0),c2_1(x1),c0_1(x2),c3_1(x2) -> c1_1(x0),c0_1(x1),c1_1(x1),c2_1(x2)
% 6.94/2.21 === Conflict found: 355:9:3:[353.6,19.2,18.2,20.2,125.2,156.8,239.1]:TopTopTop: c2_1(x0),c3_1(x0),c2_1(x1),c0_1(x2),c3_1(x2) -> c1_1(x0),c0_1(x1),c1_1(x1),c2_1(x2) {x0 -> a1026, x1 -> a1026, x2 -> a1006}
% 6.94/2.21 === Backtracking. Learning clause 356:7:2:[355.5,27.2,26.2,28.2,127.2,172.8,239.1,355.9,62.2,63.2,64.2,305.4,352.2]:TopTop: c3_1(a1026),c1_1(x0),c0_1(x1),c3_1(x1) -> c0_1(x0),ren27,c1_1(x1)
% 6.94/2.21 === Conflict found: 355:9:3:[353.6,19.2,18.2,20.2,125.2,156.8,239.1]:TopTopTop: c2_1(x0),c3_1(x0),c2_1(x1),c0_1(x2),c3_1(x2) -> c1_1(x0),c0_1(x1),c1_1(x1),c2_1(x2) {x0 -> a1026, x1 -> a1026, x2 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 357:7:2:[355.1,62.2,63.2,64.2,305.4]:TopTop: c3_1(a1026),c0_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c2_1(x0),c1_1(x1)
% 6.94/2.21 === Conflict found: 357:7:2:[355.1,62.2,63.2,64.2,305.4]:TopTop: c3_1(a1026),c0_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c2_1(x0),c1_1(x1) {x0 -> a1006, x1 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 358:4:1:[357.6,28.2,26.2,27.2,127.2,194.8,239.1,357.6]:Top: c3_1(a1026),c0_1(x0),c3_1(x0) -> c1_1(x0)
% 6.94/2.21 === Conflict found: 355:9:3:[353.6,19.2,18.2,20.2,125.2,156.8,239.1]:TopTopTop: c2_1(x0),c3_1(x0),c2_1(x1),c0_1(x2),c3_1(x2) -> c1_1(x0),c0_1(x1),c1_1(x1),c2_1(x2) {x0 -> a1040, x1 -> a1040, x2 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 360:12:4:[239.0,359.3,355.1,151.6,352.1]:TopTopTopTop: c0_1(x0),c3_1(x0),c2_1(x1),c3_1(x2),c0_1(x3),c3_1(x3) -> c2_1(x0),c0_1(x1),c1_1(x1),c0_1(x2),ren27,c1_1(x3)
% 6.94/2.21 === Conflict found: 360:12:4:[239.0,359.3,355.1,151.6,352.1]:TopTopTopTop: c0_1(x0),c3_1(x0),c2_1(x1),c3_1(x2),c0_1(x3),c3_1(x3) -> c2_1(x0),c0_1(x1),c1_1(x1),c0_1(x2),ren27,c1_1(x3) {x0 -> a1052, x1 -> a1026, x2 -> a1015, x3 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 361:7:2:[360.4,46.2,47.2,132.2,175.8,358.1,62.2,63.2,64.2,305.4,239.1]:TopTop: c0_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c2_1(x0),ren27,c1_1(x1)
% 6.94/2.21 === Conflict found: 361:7:2:[360.4,46.2,47.2,132.2,175.8,358.1,62.2,63.2,64.2,305.4,239.1]:TopTop: c0_1(x0),c3_1(x0),c0_1(x1),c3_1(x1) -> c2_1(x0),ren27,c1_1(x1) {x0 -> a1006, x1 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 362:4:1:[361.2,27.2,26.2,28.2,127.2,194.8,239.1,361.5]:Top: c0_1(x0),c3_1(x0) -> ren27,c1_1(x0)
% 6.94/2.21 === Backtracking. Learning clause 364:10:3:[239.0,363.2,174.1,161.5,78.2,80.2,140.2,190.8,31.2,32.2,30.2,128.2]:TopTopTop: c0_1(x0),c0_1(x1),c0_1(x2),c2_1(x2),hskp7 -> c2_1(x0),c3_1(x0),c1_1(x1),c3_1(x1),c1_1(x2)
% 6.94/2.21 === Backtracking. Learning clause 367:12:4:[239.0,365.2,362.1,366.10,161.5,174.1,80.2,78.2,140.2,190.8,362.2]:TopTopTopTop: c2_1(x0),c0_1(x1),c0_1(x2),c2_1(x2),c0_1(x3) -> c1_1(x0),c3_1(x0),c2_1(x3),c1_1(x1),c1_1(x2),ren27,c1_1(x3)
% 6.94/2.21 === Backtracking. Learning clause 370:11:4:[157.5,368.0,239.0,369.5,180.6,157.6]:TopTopTopTop: c3_1(x0),c2_1(x1),c3_1(x1),c3_1(x2),c2_1(x3) -> c0_1(x0),c0_1(x1),c0_1(x2),c2_1(x2),c1_1(x3),c3_1(x3)
% 6.94/2.21 === Conflict found: 362:4:1:[361.2,27.2,26.2,28.2,127.2,194.8,239.1,361.5]:Top: c0_1(x0),c3_1(x0) -> ren27,c1_1(x0) {x0 -> a1010}
% 6.94/2.21 === Backtracking. Learning clause 371:1:0:[362.1,34.2,36.2,35.2,297.1]:: -> ren27
% 6.94/2.21 === Conflict found: 305:4:1:[239.0,304.0,181.6,100.2,99.2,98.2,145.2,198.5,136.1]:Top: c0_1(x0),c3_1(x0) -> c1_1(x0),ren16 {x0 -> a1010}
% 6.94/2.21 === Backtracking. Learning clause 372:1:0:[305.1,34.2,36.2,35.2,297.1]:: -> ren16
% 6.94/2.21 === Conflict found: 358:4:1:[357.6,28.2,26.2,27.2,127.2,194.8,239.1,357.6]:Top: c3_1(a1026),c0_1(x0),c3_1(x0) -> c1_1(x0) {x0 -> a1010}
% 6.94/2.21 === Backtracking. Learning clause 373:1:0:[358.2,34.2,36.2,35.2,297.1]:: c3_1(a1026) ->
% 6.94/2.21 === Conflict found: 314:8:2:[61.1,312.0,305.3,313.5,311.9,48.2,46.2,47.2,132.2,175.8,62.2,311.3,64.2,32.2,31.2,30.2,128.2]:TopTop: c0_1(x0),c3_1(x0),c1_1(x1),c3_1(x1),hskp7 -> c1_1(x0),c0_1(x1),c0_1(a1026) {x0 -> a1010, x1 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 377:12:3:[106.1,374.2,105.1,375.5,362.2,376.7,314.3,151.5,107.2]:TopTopTop: c0_1(x0),c3_1(x0),hskp7,c2_1(x1),c3_1(x2) -> c1_1(x0),c0_1(a1026),c2_1(a1052),c0_1(x1),c1_1(x1),c0_1(x2),c2_1(x2)
% 6.94/2.21 === Conflict found: 377:12:3:[106.1,374.2,105.1,375.5,362.2,376.7,314.3,151.5,107.2]:TopTopTop: c0_1(x0),c3_1(x0),hskp7,c2_1(x1),c3_1(x2) -> c1_1(x0),c0_1(a1026),c2_1(a1052),c0_1(x1),c1_1(x1),c0_1(x2),c2_1(x2) {x0 -> a1010, x1 -> a1026, x2 -> a1052}
% 6.94/2.21 === Backtracking. Learning clause 378:9:2:[377.11,107.2,106.2,371.1]:TopTop: c0_1(x0),c3_1(x0),hskp7,c2_1(x1) -> c1_1(x0),c0_1(a1026),c0_1(x1),c1_1(x1),c2_1(a1052)
% 6.94/2.21 === Backtracking. Learning clause 379:1:0:[151.5,336.3,107.2,106.2,371.1,378.3,34.2,36.2,35.2,297.1,63.2,64.2,62.2,373.1,239.1,372.1]:: -> c2_1(a1052)
% 6.94/2.21
% 6.94/2.21 SZS status Unsatisfiable
% 6.94/2.21
% 6.94/2.21 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.94/2.21
% 6.94/2.21 SPASS-SCL-FOL Statistics:
% 6.94/2.21 Number of learned clauses: 86
% 6.94/2.21 Number of propagations: 1053
% 6.94/2.21 Number of decisions: 311
% 6.94/2.21 Number of resolutions: 478
% 6.94/2.21 Number of condensations: 36
% 6.94/2.21 Number of sub resolutions: 71
% 6.94/2.21 Number of input literals (deduplicated): 155
% 6.94/2.21 Number of grows: 0
% 6.94/2.21 Number of considered ground atoms: 181
% 6.94/2.21
% 6.94/2.21 Needed: 0:00:01.61
% 6.94/2.21
%------------------------------------------------------------------------------