%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN871-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:21 PM UTC 2026
% Result : Unsatisfiable 6.93s 2.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : SYN871-1 : TPTP v9.2.1. Released v2.5.0.
% 0.13/0.14 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.36 % Computer : n009.cluster.edu
% 0.19/0.36 % Model : x86_64 x86_64
% 0.19/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.36 % Memory : 8042.1875MB
% 0.19/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.19/0.36 % CPULimit : 300
% 0.19/0.36 % WCLimit : 300
% 0.19/0.36 % DateTime : Thu May 7 13:49:56 EDT 2026
% 0.19/0.37 % CPUTime :
% 0.19/0.37 SPASS-SCL-FOL version:
% 0.28/0.45 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 6.93/2.20 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.93/2.20 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.93/2.20 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.93/2.20 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.93/2.20 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.93/2.20 Execution resolution_2 ended with status: unsatisfiable
% 6.93/2.20 Used heuristic: resolution_2
% 6.93/2.20
% 6.93/2.20 Input Clauses:
% 6.93/2.21
% 6.93/2.21 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv16_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv15_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv14_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv13_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssPv12_9r1r1r1r1r1r1r1r1r1 ssPv19_2r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssPv11_10r1r1r1r1r1r1r1r1r1r1 ssPv17_4r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv20_1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv18_3r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 6.93/2.21 Fol Constants: skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19 skc16 skc17
% 6.93/2.21 Fol Functions:
% 6.93/2.21 Problem Properties:
% 6.93/2.21 This is a Bernays Schoenfinkel problem.
% 6.93/2.21
% 6.93/2.21 After reduction: Problem Properties:
% 6.93/2.21 This is a Bernays Schoenfinkel problem.
% 6.93/2.21
% 6.93/2.21
% 6.93/2.21 Reduced Input Clauses:
% 6.93/2.21 57:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 6.93/2.21 59:1:2:[57.1,3.0,1.0,58.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 6.93/2.21 62:1:3:[59.2,4.0,57.1,60.1,1.0,61.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 6.93/2.21 66:1:4:[62.3,5.0,59.2,63.1,57.1,64.2,1.0,65.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 6.93/2.21 70:1:4:[62.3,6.0,59.2,67.1,57.1,68.2,1.0,69.3]:TopTopTopTop: -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc30)
% 6.93/2.21 74:1:4:[62.3,7.1,59.2,71.2,57.1,72.3,1.0,73.4]:TopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc31) ->
% 6.93/2.21 79:1:5:[66.4,8.0,62.3,75.1,59.2,76.2,57.1,77.3,1.0,78.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 6.93/2.21 84:1:5:[66.4,9.0,62.3,80.1,59.2,81.2,57.1,82.3,1.0,83.4]:TopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28)
% 6.93/2.21 89:1:5:[66.4,10.1,62.3,85.2,59.2,86.3,57.1,87.4,1.0,88.5]:TopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29) ->
% 6.93/2.21 95:1:6:[79.5,11.0,66.4,90.1,62.3,91.2,59.2,92.3,57.1,93.4,1.0,94.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 6.93/2.21 101:1:6:[79.5,12.0,66.4,96.1,62.3,97.2,59.2,98.3,57.1,99.4,1.0,100.5]:TopTopTopTopTopTop: -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26)
% 6.93/2.21 107:1:6:[79.5,13.1,66.4,102.2,62.3,103.3,59.2,104.4,57.1,105.5,1.0,106.6]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27) ->
% 6.93/2.21 114:1:7:[95.6,14.0,79.5,108.1,66.4,109.2,62.3,110.3,59.2,111.4,57.1,112.5,1.0,113.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 6.93/2.21 121:1:7:[95.6,15.0,79.5,115.1,66.4,116.2,62.3,117.3,59.2,118.4,57.1,119.5,1.0,120.6]:TopTopTopTopTopTopTop: -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24)
% 6.93/2.21 128:1:7:[95.6,16.1,79.5,122.2,66.4,123.3,62.3,124.4,59.2,125.5,57.1,126.6,1.0,127.7]:TopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25) ->
% 6.93/2.21 136:1:8:[114.7,17.0,95.6,129.1,79.5,130.2,66.4,131.3,62.3,132.4,59.2,133.5,57.1,134.6,1.0,135.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 6.93/2.21 145:1:9:[136.8,18.0,114.7,137.1,95.6,138.2,79.5,139.3,66.4,140.4,62.3,141.5,59.2,142.6,57.1,143.7,1.0,144.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 6.93/2.21 155:1:10:[145.9,19.0,136.8,146.1,114.7,147.2,95.6,148.3,79.5,149.4,66.4,150.5,62.3,151.6,59.2,152.7,57.1,153.8,1.0,154.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 6.93/2.21 164:4:9:[136.8,20.0,114.7,156.2,95.6,157.3,79.5,158.5,66.4,159.6,62.3,160.7,59.2,161.8,57.1,162.9,1.0,163.10]:TopTopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 175:1:11:[155.10,21.0,145.9,165.1,136.8,166.2,114.7,167.3,95.6,168.4,79.5,169.5,66.4,170.6,62.3,171.7,59.2,172.8,57.1,173.9,1.0,174.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 6.93/2.21 185:4:10:[145.9,22.0,136.8,176.1,114.7,177.2,95.6,178.3,79.5,179.5,66.4,180.6,62.3,181.7,59.2,182.8,57.1,183.9,1.0,184.10]:TopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 6.93/2.21 197:1:12:[175.11,23.0,155.10,186.1,145.9,187.2,136.8,188.3,114.7,189.4,95.6,190.5,79.5,191.6,66.4,192.7,62.3,193.8,59.2,194.9,57.1,195.10,1.0,196.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 6.93/2.21 209:1:12:[175.11,24.0,155.10,198.1,145.9,199.2,136.8,200.3,114.7,201.4,95.6,202.5,79.5,203.6,66.4,204.7,62.3,205.8,59.2,206.9,57.1,207.10,1.0,208.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22)
% 6.93/2.21 221:1:12:[175.11,25.1,155.10,210.2,145.9,211.3,136.8,212.4,114.7,213.5,95.6,214.6,79.5,215.7,66.4,216.8,62.3,217.9,59.2,218.10,57.1,219.11,1.0,220.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23) ->
% 6.93/2.21 232:4:11:[155.10,26.0,145.9,222.2,136.8,223.3,114.7,224.4,95.6,225.5,79.5,226.6,66.4,227.7,62.3,228.8,59.2,229.9,57.1,230.10,1.0,231.11]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 6.93/2.21 245:1:13:[197.12,27.0,175.11,233.1,155.10,234.2,145.9,235.3,136.8,236.4,114.7,237.5,95.6,238.6,79.5,239.7,66.4,240.8,62.3,241.9,59.2,242.10,57.1,243.11,1.0,244.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 6.93/2.21 258:1:13:[197.12,28.0,175.11,246.1,155.10,247.2,145.9,248.3,136.8,249.4,114.7,250.5,95.6,251.6,79.5,252.7,66.4,253.8,62.3,254.9,59.2,255.10,57.1,256.11,1.0,257.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20)
% 6.93/2.21 271:1:13:[197.12,29.1,175.11,259.2,155.10,260.3,145.9,261.4,136.8,262.5,114.7,263.6,95.6,264.7,79.5,265.8,66.4,266.9,62.3,267.10,59.2,268.11,57.1,269.12,1.0,270.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21) ->
% 6.93/2.21 285:1:14:[245.13,30.0,197.12,272.1,175.11,273.2,155.10,274.3,145.9,275.4,136.8,276.5,114.7,277.6,95.6,278.7,79.5,279.8,66.4,280.9,62.3,281.10,59.2,282.11,57.1,283.12,1.0,284.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 6.93/2.21 299:1:14:[245.13,31.0,197.12,286.1,175.11,287.2,155.10,288.3,145.9,289.4,136.8,290.5,114.7,291.6,95.6,292.7,79.5,293.8,66.4,294.9,62.3,295.10,59.2,296.11,57.1,297.12,1.0,298.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18)
% 6.93/2.21 313:1:14:[245.13,32.1,197.12,300.2,175.11,301.3,155.10,302.4,145.9,303.5,136.8,304.6,114.7,305.7,95.6,306.8,79.5,307.9,66.4,308.10,62.3,309.11,59.2,310.12,57.1,311.13,1.0,312.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19) ->
% 6.93/2.21 328:1:15:[285.14,33.0,245.13,314.1,197.12,315.2,175.11,316.3,155.10,317.4,145.9,318.5,136.8,319.6,114.7,320.7,95.6,321.8,79.5,322.9,66.4,323.10,62.3,324.11,59.2,325.12,57.1,326.13,1.0,327.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 6.93/2.21 343:1:15:[285.14,34.0,245.13,329.1,197.12,330.2,175.11,331.3,155.10,332.4,145.9,333.5,136.8,334.6,114.7,335.7,95.6,336.8,79.5,337.9,66.4,338.10,62.3,339.11,59.2,340.12,57.1,341.13,1.0,342.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16)
% 6.93/2.21 358:1:15:[285.14,35.1,245.13,344.2,197.12,345.3,175.11,346.4,155.10,347.5,145.9,348.6,136.8,349.7,114.7,350.8,95.6,351.9,79.5,352.10,66.4,353.11,62.3,354.12,59.2,355.13,57.1,356.14,1.0,357.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc17) ->
% 6.93/2.21 372:4:14:[245.13,36.0,197.12,359.1,175.11,360.2,155.10,361.3,145.9,362.4,136.8,363.5,114.7,364.6,95.6,365.7,79.5,366.8,66.4,367.10,62.3,368.11,59.2,369.12,57.1,370.13,1.0,371.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 6.93/2.21 388:1:16:[328.15,37.0,285.14,373.1,245.13,374.2,197.12,375.3,175.11,376.4,155.10,377.5,145.9,378.6,136.8,379.7,114.7,380.8,95.6,381.9,79.5,382.10,66.4,383.11,62.3,384.12,59.2,385.13,57.1,386.14,1.0,387.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 6.93/2.21 404:4:16:[328.15,38.0,285.14,389.1,245.13,390.2,197.12,391.3,175.11,392.4,155.10,393.5,145.9,394.6,136.8,395.7,114.7,396.8,95.6,397.10,79.5,398.11,66.4,399.12,62.3,400.13,59.2,401.14,57.1,402.16,1.0,403.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 420:4:16:[328.15,39.0,285.14,405.1,245.13,406.2,197.12,407.3,175.11,408.4,155.10,409.5,145.9,410.6,136.8,411.7,114.7,412.9,95.6,413.10,79.5,414.11,66.4,415.12,62.3,416.13,59.2,417.15,57.1,418.16,1.0,419.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 6.93/2.21 437:1:17:[388.16,40.0,328.15,421.1,285.14,422.2,245.13,423.3,197.12,424.4,175.11,425.5,155.10,426.6,145.9,427.7,136.8,428.8,114.7,429.9,95.6,430.10,79.5,431.11,66.4,432.12,62.3,433.13,59.2,434.14,57.1,435.15,1.0,436.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 6.93/2.21 453:4:16:[328.15,41.0,285.14,438.1,245.13,439.2,197.12,440.3,175.11,441.4,155.10,442.5,145.9,443.6,136.8,444.7,114.7,445.8,95.6,446.9,79.5,447.10,66.4,448.11,62.3,449.12,59.2,450.13,57.1,451.14,1.0,452.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 469:4:16:[328.15,42.0,285.14,454.2,245.13,455.4,197.12,456.5,175.11,457.6,155.10,458.7,145.9,459.8,136.8,460.9,114.7,461.10,95.6,462.11,79.5,463.12,66.4,464.13,62.3,465.14,59.2,466.15,57.1,467.17,1.0,468.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) -> ssPv18_3r1r1r1(x0,x1,x2)
% 6.93/2.21 485:4:16:[328.15,43.0,285.14,470.1,245.13,471.2,197.12,472.3,175.11,473.4,155.10,474.5,145.9,475.6,136.8,476.7,114.7,477.8,95.6,478.9,79.5,479.10,66.4,480.11,62.3,481.12,59.2,482.13,57.1,483.14,1.0,484.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0)
% 6.93/2.21 503:1:18:[437.17,44.0,388.16,486.1,328.15,487.2,285.14,488.3,245.13,489.4,197.12,490.5,175.11,491.6,155.10,492.7,145.9,493.8,136.8,494.9,114.7,495.10,95.6,496.11,79.5,497.12,66.4,498.13,62.3,499.14,59.2,500.15,57.1,501.16,1.0,502.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 6.93/2.21 520:4:17:[388.16,45.0,328.15,504.2,285.14,505.3,245.13,506.4,197.12,507.5,175.11,508.6,155.10,509.7,145.9,510.8,136.8,511.10,114.7,512.12,95.6,513.13,79.5,514.14,66.4,515.15,62.3,516.16,59.2,517.18,57.1,518.19,1.0,519.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) ->
% 6.93/2.21 537:4:17:[388.16,46.0,328.15,521.2,285.14,522.3,245.13,523.4,197.12,524.5,175.11,525.6,155.10,526.7,145.9,527.8,136.8,528.9,114.7,529.10,95.6,530.11,79.5,531.12,66.4,532.13,62.3,533.14,59.2,534.15,57.1,535.16,1.0,536.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 554:4:17:[388.16,47.0,328.15,538.1,285.14,539.2,245.13,540.3,197.12,541.4,175.11,542.5,155.10,543.6,145.9,544.7,136.8,545.8,114.7,546.9,95.6,547.11,79.5,548.12,66.4,549.13,62.3,550.14,59.2,551.15,57.1,552.16,1.0,553.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 6.93/2.21 571:4:17:[388.16,48.0,328.15,555.1,285.14,556.3,245.13,557.4,197.12,558.5,175.11,559.6,155.10,560.8,145.9,561.9,136.8,562.11,114.7,563.12,95.6,564.13,79.5,565.14,66.4,566.15,62.3,567.16,59.2,568.17,57.1,569.18,1.0,570.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 6.93/2.21 590:1:19:[503.18,49.0,437.17,572.1,388.16,573.2,328.15,574.3,285.14,575.4,245.13,576.5,197.12,577.6,175.11,578.7,155.10,579.8,145.9,580.9,136.8,581.10,114.7,582.11,95.6,583.12,79.5,584.13,66.4,585.14,62.3,586.15,59.2,587.16,57.1,588.17,1.0,589.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 6.93/2.21 608:4:18:[437.17,50.1,388.16,591.3,328.15,592.4,285.14,593.5,245.13,594.6,197.12,595.7,175.11,596.8,155.10,597.9,145.9,598.10,136.8,599.12,114.7,600.13,95.6,601.14,79.5,602.15,66.4,603.16,62.3,604.17,59.2,605.18,57.1,606.19,1.0,607.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 6.93/2.21 627:4:19:[503.18,51.0,437.17,609.1,388.16,610.2,328.15,611.4,285.14,612.5,245.13,613.6,197.12,614.7,175.11,615.8,155.10,616.9,145.9,617.10,136.8,618.11,114.7,619.12,95.6,620.13,79.5,621.14,66.4,622.15,62.3,623.16,59.2,624.17,57.1,625.18,1.0,626.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 645:4:18:[437.17,52.1,388.16,628.4,328.15,629.5,285.14,630.6,245.13,631.7,197.12,632.8,175.11,633.9,155.10,634.10,145.9,635.11,136.8,636.12,114.7,637.13,95.6,638.14,79.5,639.15,66.4,640.16,62.3,641.17,59.2,642.18,57.1,643.19,1.0,644.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 6.93/2.21 664:4:19:[503.18,53.0,437.17,646.2,388.16,647.4,328.15,648.5,285.14,649.6,245.13,650.7,197.12,651.8,175.11,652.9,155.10,653.10,145.9,654.11,136.8,655.12,114.7,656.13,95.6,657.15,79.5,658.16,66.4,659.17,62.3,660.18,59.2,661.19,57.1,662.20,1.0,663.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 6.93/2.21 683:4:19:[503.18,54.0,437.17,665.1,388.16,666.3,328.15,667.5,285.14,668.6,245.13,669.7,197.12,670.8,175.11,671.10,155.10,672.11,145.9,673.12,136.8,674.13,114.7,675.14,95.6,676.15,79.5,677.16,66.4,678.17,62.3,679.18,59.2,680.19,57.1,681.20,1.0,682.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 6.93/2.21 702:4:19:[503.18,55.1,437.17,684.3,388.16,685.4,328.15,686.5,285.14,687.6,245.13,688.7,197.12,689.8,175.11,690.9,155.10,691.10,145.9,692.11,136.8,693.12,114.7,694.13,95.6,695.14,79.5,696.15,66.4,697.16,62.3,698.17,59.2,699.18,57.1,700.19,1.0,701.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 6.93/2.21 722:4:20:[590.19,56.0,503.18,703.2,437.17,704.3,388.16,705.5,328.15,706.6,285.14,707.7,245.13,708.8,197.12,709.9,175.11,710.10,155.10,711.11,145.9,712.12,136.8,713.14,114.7,714.15,95.6,715.16,79.5,716.17,66.4,717.18,62.3,718.19,59.2,719.20,57.1,720.21,1.0,721.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv20_1r1(x0)
% 6.93/2.21
% 6.93/2.21 Most General Atoms: ssNder1_0 ssNder1_1r1(x0) ssNder1_2r1r1(x0,x1) ssNder1_3r1r1r1(x0,x1,x2) ssNder1_4r1r1r1r1(x0,x1,x2,x3) ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv19_2r1r1(x0,x1) ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv17_4r1r1r1r1(x0,x1,x2,x3) ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssPv20_1r1(x0) ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv18_3r1r1r1(x0,x1,x2) ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 6.93/2.21
% 6.93/2.21 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_2 ===
% 6.93/2.21
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 55
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 185:4:10:[145.9,22.0,136.8,176.1,114.7,177.2,95.6,178.3,79.5,179.5,66.4,180.6,62.3,181.7,59.2,182.8,57.1,183.9,1.0,184.10]:TopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 723:3:9:[185.1,70.1]:TopTopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 6.93/2.21 === Conflict found: 164:4:9:[136.8,20.0,114.7,156.2,95.6,157.3,79.5,158.5,66.4,159.6,62.3,160.7,59.2,161.8,57.1,162.9,1.0,163.10]:TopTopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 724:3:8:[164.2,70.1]:TopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Conflict found: 664:4:19:[503.18,53.0,437.17,646.2,388.16,647.4,328.15,648.5,285.14,649.6,245.13,650.7,197.12,651.8,175.11,652.9,155.10,653.10,145.9,654.11,136.8,655.12,114.7,656.13,95.6,657.15,79.5,658.16,66.4,659.17,62.3,660.18,59.2,661.19,57.1,662.20,1.0,663.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 725:5:17:[664.1,683.4,554.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 57
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 627:4:19:[503.18,51.0,437.17,609.1,388.16,610.2,328.15,611.4,285.14,612.5,245.13,613.6,197.12,614.7,175.11,615.8,155.10,616.9,145.9,617.10,136.8,618.11,114.7,619.12,95.6,620.13,79.5,621.14,66.4,622.15,62.3,623.16,59.2,624.17,57.1,625.18,1.0,626.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 726:3:18:[627.3,74.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 63
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 725:5:17:[664.1,683.4,554.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 727:4:16:[725.3,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8)
% 6.93/2.21 === Conflict found: 554:4:17:[388.16,47.0,328.15,538.1,285.14,539.2,245.13,540.3,197.12,541.4,175.11,542.5,155.10,543.6,145.9,544.7,136.8,545.8,114.7,546.9,95.6,547.11,79.5,548.12,66.4,549.13,62.3,550.14,59.2,551.15,57.1,552.16,1.0,553.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 728:3:16:[554.1,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8)
% 6.93/2.21 === Conflict found: 404:4:16:[328.15,38.0,285.14,389.1,245.13,390.2,197.12,391.3,175.11,392.4,155.10,393.5,145.9,394.6,136.8,395.7,114.7,396.8,95.6,397.10,79.5,398.11,66.4,399.12,62.3,400.13,59.2,401.14,57.1,402.16,1.0,403.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 729:3:15:[404.1,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 68
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 232:4:11:[155.10,26.0,145.9,222.2,136.8,223.3,114.7,224.4,95.6,225.5,79.5,226.6,66.4,227.7,62.3,228.8,59.2,229.9,57.1,230.10,1.0,231.11]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 730:3:10:[232.4,89.1]:TopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6)
% 6.93/2.21 === Conflict found: 723:3:9:[185.1,70.1]:TopTopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc29, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 731:2:8:[723.2,89.1]:TopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 132
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 135
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 520:4:17:[388.16,45.0,328.15,504.2,285.14,505.3,245.13,506.4,197.12,507.5,175.11,508.6,155.10,509.7,145.9,510.8,136.8,511.10,114.7,512.12,95.6,513.13,79.5,514.14,66.4,515.15,62.3,516.16,59.2,517.18,57.1,518.19,1.0,519.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 732:3:16:[520.3,101.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6),ssPv19_2r1r1(x0,x1) ->
% 6.93/2.21 === Conflict found: 420:4:16:[328.15,39.0,285.14,405.1,245.13,406.2,197.12,407.3,175.11,408.4,155.10,409.5,145.9,410.6,136.8,411.7,114.7,412.9,95.6,413.10,79.5,414.11,66.4,415.12,62.3,416.13,59.2,417.15,57.1,418.16,1.0,419.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 733:3:15:[420.1,101.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 136
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 724:3:8:[164.2,70.1]:TopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc27, x6 -> skc30, x7 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 734:2:7:[724.2,107.1]:TopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc27,x5,x6) -> ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 143
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 722:4:20:[590.19,56.0,503.18,703.2,437.17,704.3,388.16,705.5,328.15,706.6,285.14,707.7,245.13,708.8,197.12,709.9,175.11,710.10,155.10,711.11,145.9,712.12,136.8,713.14,114.7,714.15,95.6,715.16,79.5,716.17,66.4,717.18,62.3,718.19,59.2,719.20,57.1,720.21,1.0,721.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc26, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 735:3:19:[722.3,121.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_1r1(x0)
% 6.93/2.21 === Conflict found: 608:4:18:[437.17,50.1,388.16,591.3,328.15,592.4,285.14,593.5,245.13,594.6,197.12,595.7,175.11,596.8,155.10,597.9,145.9,598.10,136.8,599.12,114.7,600.13,95.6,601.14,79.5,602.15,66.4,603.16,62.3,604.17,59.2,605.18,57.1,606.19,1.0,607.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc26, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 736:3:17:[608.3,121.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 6.93/2.21 === Conflict found: 732:3:16:[520.3,101.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc24, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 737:2:15:[732.2,121.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,skc24,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) ->
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 147
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 730:3:10:[232.4,89.1]:TopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc25, x7 -> skc30, x8 -> skc30, x9 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 738:2:9:[730.3,128.1]:TopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7,x8) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 211
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 212
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 469:4:16:[328.15,42.0,285.14,454.2,245.13,455.4,197.12,456.5,175.11,457.6,155.10,458.7,145.9,459.8,136.8,460.9,114.7,461.10,95.6,462.11,79.5,463.12,66.4,464.13,62.3,465.14,59.2,466.15,57.1,467.17,1.0,468.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) -> ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 739:3:15:[469.2,209.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x14),ssPv20_1r1(x0) -> ssPv18_3r1r1r1(x0,x1,x2)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 215
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 537:4:17:[388.16,46.0,328.15,521.2,285.14,522.3,245.13,523.4,197.12,524.5,175.11,525.6,155.10,526.7,145.9,527.8,136.8,528.9,114.7,529.10,95.6,530.11,79.5,531.12,66.4,532.13,62.3,533.14,59.2,534.15,57.1,535.16,1.0,536.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 740:3:16:[537.3,221.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Conflict found: 453:4:16:[328.15,41.0,285.14,438.1,245.13,439.2,197.12,440.3,175.11,441.4,155.10,442.5,145.9,443.6,136.8,444.7,114.7,445.8,95.6,446.9,79.5,447.10,66.4,448.11,62.3,449.12,59.2,450.13,57.1,451.14,1.0,452.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 741:3:15:[453.2,221.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 216
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 571:4:17:[388.16,48.0,328.15,555.1,285.14,556.3,245.13,557.4,197.12,558.5,175.11,559.6,155.10,560.8,145.9,561.9,136.8,562.11,114.7,563.12,95.6,564.13,79.5,565.14,66.4,566.15,62.3,567.16,59.2,568.17,57.1,569.18,1.0,570.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 742:3:16:[571.1,258.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13,x14,x15)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 221
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 372:4:14:[245.13,36.0,197.12,359.1,175.11,360.2,155.10,361.3,145.9,362.4,136.8,363.5,114.7,364.6,95.6,365.7,79.5,366.8,66.4,367.10,62.3,368.11,59.2,369.12,57.1,370.13,1.0,371.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc21}
% 6.93/2.21 === Backtracking. Learning clause 743:3:11:[372.2,271.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 6.93/2.21 === Conflict found: 740:3:16:[537.3,221.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc21, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 744:2:15:[740.2,271.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,skc21,x12,x13,x14) -> ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 285
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 291
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 725:5:17:[664.1,683.4,554.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 745:3:15:[725.1,299.1,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8)
% 6.93/2.21 === Conflict found: 683:4:19:[503.18,54.0,437.17,665.1,388.16,666.3,328.15,667.5,285.14,668.6,245.13,669.7,197.12,670.8,175.11,671.10,155.10,672.11,145.9,673.12,136.8,674.13,114.7,675.14,95.6,676.15,79.5,677.16,66.4,678.17,62.3,679.18,59.2,680.19,57.1,681.20,1.0,682.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 746:3:18:[683.2,299.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15,x16,x17)
% 6.93/2.21 === Conflict found: 726:3:18:[627.3,74.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc28, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc18, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 747:2:17:[726.1,299.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14,x15,x16),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Conflict found: 554:4:17:[388.16,47.0,328.15,538.1,285.14,539.2,245.13,540.3,197.12,541.4,175.11,542.5,155.10,543.6,145.9,544.7,136.8,545.8,114.7,546.9,95.6,547.11,79.5,548.12,66.4,549.13,62.3,550.14,59.2,551.15,57.1,552.16,1.0,553.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 748:4:19:[554.2,664.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 294
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 485:4:16:[328.15,43.0,285.14,470.1,245.13,471.2,197.12,472.3,175.11,473.4,155.10,474.5,145.9,475.6,136.8,476.7,114.7,477.8,95.6,478.9,79.5,479.10,66.4,480.11,62.3,481.12,59.2,482.13,57.1,483.14,1.0,484.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 749:3:15:[485.1,313.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 302
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 683:4:19:[503.18,54.0,437.17,665.1,388.16,666.3,328.15,667.5,285.14,668.6,245.13,669.7,197.12,670.8,175.11,671.10,155.10,672.11,145.9,673.12,136.8,674.13,114.7,675.14,95.6,676.15,79.5,677.16,66.4,678.17,62.3,679.18,59.2,680.19,57.1,681.20,1.0,682.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc18, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 750:2:17:[683.1,343.1,299.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,skc16,x14,x15,x16)
% 6.93/2.21 === Conflict found: 735:3:19:[722.3,121.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc22, x12 -> skc30, x13 -> skc18, x14 -> skc16, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 751:2:18:[735.2,343.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,skc16,x14,x15,x16,x17) -> ssPv20_1r1(x0)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 311
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 453:4:16:[328.15,41.0,285.14,438.1,245.13,439.2,197.12,440.3,175.11,441.4,155.10,442.5,145.9,443.6,136.8,444.7,114.7,445.8,95.6,446.9,79.5,447.10,66.4,448.11,62.3,449.12,59.2,450.13,57.1,451.14,1.0,452.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc19, x15 -> skc17}
% 6.93/2.21 === Backtracking. Learning clause 752:2:3:[453.1,358.1,221.1]:TopTopTop: -> ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Conflict found: 729:3:15:[404.1,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc26, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc23, x12 -> skc30, x13 -> skc19, x14 -> skc17}
% 6.93/2.21 === Backtracking. Learning clause 753:2:2:[729.2,358.1]:TopTop: ssPv20_1r1(x0) -> ssPv19_2r1r1(x0,x1)
% 6.93/2.21 === Conflict found: 728:3:16:[554.1,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc26, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc23, x12 -> skc30, x13 -> skc19, x14 -> skc17, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 754:2:15:[728.1,358.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc17,x14),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 375
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 377
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 571:4:17:[388.16,48.0,328.15,555.1,285.14,556.3,245.13,557.4,197.12,558.5,175.11,559.6,155.10,560.8,145.9,561.9,136.8,562.11,114.7,563.12,95.6,564.13,79.5,565.14,66.4,566.15,62.3,567.16,59.2,568.17,57.1,569.18,1.0,570.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 755:4:15:[571.2,731.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 6.93/2.21 === Conflict found: 742:3:16:[571.1,258.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13,x14,x15) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 756:3:14:[742.1,731.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,skc20,x11,x12,x13),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 385
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 728:3:16:[554.1,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc26, x6 -> skc24, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc20, x13 -> skc18, x14 -> skc17, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 757:2:7:[728.2,737.1,358.1]:TopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc26,skc24,x5,x6)
% 6.93/2.21 === Conflict found: 571:4:17:[388.16,48.0,328.15,555.1,285.14,556.3,245.13,557.4,197.12,558.5,175.11,559.6,155.10,560.8,145.9,561.9,136.8,562.11,114.7,563.12,95.6,564.13,79.5,565.14,66.4,566.15,62.3,567.16,59.2,568.17,57.1,569.18,1.0,570.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc26, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20, x14 -> skc18, x15 -> skc17, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 758:1:2:[571.3,121.1,258.1,737.1,757.2]:TopTop: ssPv19_2r1r1(x0,x1) ->
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 386
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 537:4:17:[388.16,46.0,328.15,521.2,285.14,522.3,245.13,523.4,197.12,524.5,175.11,525.6,155.10,526.7,145.9,527.8,136.8,528.9,114.7,529.10,95.6,530.11,79.5,531.12,66.4,532.13,62.3,533.14,59.2,534.15,57.1,535.16,1.0,536.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 759:3:17:[537.4,758.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 6.93/2.21 === Conflict found: 740:3:16:[537.3,221.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 760:2:16:[740.3,758.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12)
% 6.93/2.21 === Conflict found: 744:2:15:[740.2,271.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,skc21,x12,x13,x14) -> ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 761:1:15:[744.2,758.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,skc21,x12,x13,x14) ->
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 391
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 728:3:16:[554.1,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc23, x12 -> skc21, x13 -> skc18, x14 -> skc17, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 762:1:9:[728.2,761.1,358.1]:TopTopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 455
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 457
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 571:4:17:[388.16,48.0,328.15,555.1,285.14,556.3,245.13,557.4,197.12,558.5,175.11,559.6,155.10,560.8,145.9,561.9,136.8,562.11,114.7,563.12,95.6,564.13,79.5,565.14,66.4,566.15,62.3,567.16,59.2,568.17,57.1,569.18,1.0,570.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 763:3:16:[571.2,762.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 6.93/2.21 === Conflict found: 742:3:16:[571.1,258.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13,x14,x15) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 764:2:15:[742.1,762.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,skc20,x12,x13,x14)
% 6.93/2.21 === Conflict found: 232:4:11:[155.10,26.0,145.9,222.2,136.8,223.3,114.7,224.4,95.6,225.5,79.5,226.6,66.4,227.7,62.3,228.8,59.2,229.9,57.1,230.10,1.0,231.11]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 765:4:10:[232.1,743.2]:TopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 460
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 485:4:16:[328.15,43.0,285.14,470.1,245.13,471.2,197.12,472.3,175.11,473.4,155.10,474.5,145.9,475.6,136.8,476.7,114.7,477.8,95.6,478.9,79.5,479.10,66.4,480.11,62.3,481.12,59.2,482.13,57.1,483.14,1.0,484.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 766:4:14:[485.3,738.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7,x8,x9,x10,x11,x12),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7,x8,x9,x10,x11,x12,x13),ssPv20_1r1(x0),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7)
% 6.93/2.21 === Conflict found: 749:3:15:[485.1,313.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 767:3:13:[749.2,738.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7,x8,x9,x10,x11,skc19,x12),ssPv20_1r1(x0),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7)
% 6.93/2.21 === Conflict found: 753:2:2:[729.2,358.1]:TopTop: ssPv20_1r1(x0) -> ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 768:2:13:[753.1,767.2,758.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7,x8,x9,x10,x11,skc19,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,skc25,x6,x7)
% 6.93/2.21 === Conflict found: 743:3:11:[372.2,271.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 769:2:12:[743.3,128.1,731.2,738.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x8,skc29,x9,skc25,x10,x11)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 460
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 722:4:20:[590.19,56.0,503.18,703.2,437.17,704.3,388.16,705.5,328.15,706.6,285.14,707.7,245.13,708.8,197.12,709.9,175.11,710.10,155.10,711.11,145.9,712.12,136.8,713.14,114.7,714.15,95.6,715.16,79.5,716.17,66.4,717.18,62.3,718.19,59.2,719.20,57.1,720.21,1.0,721.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc18, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 771:3:20:[758.0,770.3,722.4,753.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ->
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 466
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 702:4:19:[503.18,55.1,437.17,684.3,388.16,685.4,328.15,686.5,285.14,687.6,245.13,688.7,197.12,689.8,175.11,690.9,155.10,691.10,145.9,692.11,136.8,693.12,114.7,694.13,95.6,695.14,79.5,696.15,66.4,697.16,62.3,698.17,59.2,699.18,57.1,700.19,1.0,701.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 773:3:16:[758.0,772.3,702.2,747.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14,x15) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 6.93/2.21 === Conflict found: 554:4:17:[388.16,47.0,328.15,538.1,285.14,539.2,245.13,540.3,197.12,541.4,175.11,542.5,155.10,543.6,145.9,544.7,136.8,545.8,114.7,546.9,95.6,547.11,79.5,548.12,66.4,549.13,62.3,550.14,59.2,551.15,57.1,552.16,1.0,553.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 774:7:24:[554.1,185.3,571.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x14,x15,x16,x17,x18,x19),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x14,x15,x16,x17,x18,x19,x20),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x21,x22,x23)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 530
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 534
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 748:4:19:[554.2,664.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 775:4:15:[748.1,750.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,skc16,x14)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 534
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 753:2:2:[729.2,358.1]:TopTop: ssPv20_1r1(x0) -> ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 776:1:1:[753.2,758.1]:Top: ssPv20_1r1(x0) ->
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 537
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 485:4:16:[328.15,43.0,285.14,470.1,245.13,471.2,197.12,472.3,175.11,473.4,155.10,474.5,145.9,475.6,136.8,476.7,114.7,477.8,95.6,478.9,79.5,479.10,66.4,480.11,62.3,481.12,59.2,482.13,57.1,483.14,1.0,484.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 777:3:16:[485.4,776.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 6.93/2.21 === Conflict found: 749:3:15:[485.1,313.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 778:2:15:[749.3,776.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 6.93/2.21 === Conflict found: 735:3:19:[722.3,121.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 779:2:19:[735.3,776.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14) ->
% 6.93/2.21 === Conflict found: 751:2:18:[735.2,343.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,skc16,x14,x15,x16,x17) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 780:1:18:[751.2,776.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,skc16,x14,x15,x16,x17) ->
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 543
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 607
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 612
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 752:2:3:[453.1,358.1,221.1]:TopTopTop: -> ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc31}
% 6.93/2.21 === Backtracking. Learning clause 781:1:3:[752.2,758.1]:TopTopTop: -> ssPv18_3r1r1r1(x0,x1,x2)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 617
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 645:4:18:[437.17,52.1,388.16,628.4,328.15,629.5,285.14,630.6,245.13,631.7,197.12,632.8,175.11,633.9,155.10,634.10,145.9,635.11,136.8,636.12,114.7,637.13,95.6,638.14,79.5,639.15,66.4,640.16,62.3,641.17,59.2,642.18,57.1,643.19,1.0,644.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc26, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc20, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 782:4:16:[645.1,764.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,skc20,x12,x13,x14,x15),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,skc20,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,skc20,x12)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 624
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 627:4:19:[503.18,51.0,437.17,609.1,388.16,610.2,328.15,611.4,285.14,612.5,245.13,613.6,197.12,614.7,175.11,615.8,155.10,616.9,145.9,617.10,136.8,618.11,114.7,619.12,95.6,620.13,79.5,621.14,66.4,622.15,62.3,623.16,59.2,624.17,57.1,625.18,1.0,626.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 783:3:19:[627.4,758.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 6.93/2.21 === Conflict found: 747:2:17:[726.1,299.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14,x15,x16),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 784:1:17:[747.2,758.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14,x15,x16)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 624
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 748:4:19:[554.2,664.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 785:3:15:[748.1,784.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14)
% 6.93/2.21 === Conflict found: 664:4:19:[503.18,53.0,437.17,646.2,388.16,647.4,328.15,648.5,285.14,649.6,245.13,650.7,197.12,651.8,175.11,652.9,155.10,653.10,145.9,654.11,136.8,655.12,114.7,656.13,95.6,657.15,79.5,658.16,66.4,659.17,62.3,660.18,59.2,661.19,57.1,662.20,1.0,663.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 786:3:15:[664.1,784.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14)
% 6.93/2.21 === Conflict found: 749:3:15:[485.1,313.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc17}
% 6.93/2.21 === Backtracking. Learning clause 788:1:11:[776.0,787.1,749.1,358.1]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 688
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 694
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 683:4:19:[503.18,54.0,437.17,665.1,388.16,666.3,328.15,667.5,285.14,668.6,245.13,669.7,197.12,670.8,175.11,671.10,155.10,672.11,145.9,673.12,136.8,674.13,114.7,675.14,95.6,676.15,79.5,677.16,66.4,678.17,62.3,679.18,59.2,680.19,57.1,681.20,1.0,682.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 789:3:19:[683.3,788.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 6.93/2.21 === Conflict found: 746:3:18:[683.2,299.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15,x16,x17) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 790:2:18:[746.2,788.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15,x16,x17)
% 6.93/2.21 === Conflict found: 750:2:17:[683.1,343.1,299.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,skc16,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 791:1:17:[750.1,788.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,skc16,x14,x15,x16)
% 6.93/2.21 === Conflict found: 765:4:10:[232.1,743.2]:TopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc31}
% 6.93/2.21 === Backtracking. Learning clause 792:6:16:[765.1,185.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x5,x6),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x5,x6,x7,x8),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x11)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 694
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 748:4:19:[554.2,664.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 793:3:15:[748.1,791.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,skc16,x14)
% 6.93/2.21 === Conflict found: 664:4:19:[503.18,53.0,437.17,646.2,388.16,647.4,328.15,648.5,285.14,649.6,245.13,650.7,197.12,651.8,175.11,652.9,155.10,653.10,145.9,654.11,136.8,655.12,114.7,656.13,95.6,657.15,79.5,658.16,66.4,659.17,62.3,660.18,59.2,661.19,57.1,662.20,1.0,663.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 795:2:15:[343.0,794.0,664.1,791.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,skc16,x14)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 695
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 792:6:16:[765.1,185.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x5,x6),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x5,x6,x7,x8),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc29, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc29}
% 6.93/2.21 === Backtracking. Learning clause 796:4:19:[792.3,795.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x10,x11,x12,x13,x14,x15,x16,x17,skc18,skc16,x18)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 704
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 768
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 772
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 748:4:19:[554.2,664.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 798:3:16:[554.1,797.1,748.1,790.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15)
% 6.93/2.21 === Conflict found: 664:4:19:[503.18,53.0,437.17,646.2,388.16,647.4,328.15,648.5,285.14,649.6,245.13,650.7,197.12,651.8,175.11,652.9,155.10,653.10,145.9,654.11,136.8,655.12,114.7,656.13,95.6,657.15,79.5,658.16,66.4,659.17,62.3,660.18,59.2,661.19,57.1,662.20,1.0,663.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 799:3:16:[664.1,790.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15)
% 6.93/2.21 === Clause set with instances from active satisfied. Growing active. New size: 778
% 6.93/2.21 === Restarting.
% 6.93/2.21 === Conflict found: 795:2:15:[343.0,794.0,664.1,791.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,skc16,x14) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc26, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc21, x14 -> skc30}
% 6.93/2.21 === Backtracking. Learning clause 800:1:6:[795.2,761.1]:TopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ->
% 6.93/2.21 === Conflict found: 800:1:6:[795.2,761.1]:TopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28}
% 6.93/2.21
% 6.93/2.21 SZS status Unsatisfiable
% 6.93/2.21
% 6.93/2.21 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.93/2.21
% 6.93/2.21 SPASS-SCL-FOL Statistics:
% 6.93/2.21 Number of learned clauses: 73
% 6.93/2.21 Number of propagations: 14073
% 6.93/2.21 Number of decisions: 4744
% 6.93/2.21 Number of resolutions: 87
% 6.93/2.21 Number of condensations: 3
% 6.93/2.21 Number of sub resolutions: 671
% 6.93/2.21 Number of input literals (deduplicated): 55
% 6.93/2.21 Number of grows: 47
% 6.93/2.21 Number of considered ground atoms: 778
% 6.93/2.21
% 6.93/2.21 Needed: 0:00:01.62
% 6.93/2.21
%------------------------------------------------------------------------------