%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN877-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 : n027.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 15.59s 3.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.30 % Problem : SYN877-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.31 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.53 % Computer : n027.cluster.edu
% 0.16/0.53 % Model : x86_64 x86_64
% 0.16/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.53 % Memory : 8042.1875MB
% 0.16/0.53 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.53 % CPULimit : 300
% 0.16/0.53 % WCLimit : 300
% 0.16/0.53 % DateTime : Thu May 7 13:50:06 EDT 2026
% 0.16/0.53 % CPUTime :
% 0.16/0.53 SPASS-SCL-FOL version:
% 0.20/0.62 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 15.13/3.80 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.13/3.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.13/3.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.13/3.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.13/3.80 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.13/3.80 Execution resolution_2 ended with status: unsatisfiable
% 15.13/3.80 Used heuristic: resolution_2
% 15.13/3.80
% 15.13/3.80 Input Clauses:
% 15.13/3.80
% 15.13/3.80 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 ssPv17_4r1r1r1r1 ssPv18_3r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ssPv12_9r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv11_10r1r1r1r1r1r1r1r1r1r1 ssPv20_1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv19_2r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 15.13/3.80 Fol Constants: skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19 skc16 skc17
% 15.13/3.80 Fol Functions:
% 15.13/3.80 Problem Properties:
% 15.13/3.80 This is a Bernays Schoenfinkel problem.
% 15.13/3.80
% 15.13/3.80 After reduction: Problem Properties:
% 15.13/3.80 This is a Bernays Schoenfinkel problem.
% 15.13/3.80
% 15.13/3.80
% 15.13/3.80 Reduced Input Clauses:
% 15.13/3.80 77:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 15.13/3.80 79:1:2:[77.1,3.0,1.0,78.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 15.13/3.80 82:1:3:[79.2,4.0,77.1,80.1,1.0,81.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 15.13/3.80 86:1:4:[82.3,5.0,79.2,83.1,77.1,84.2,1.0,85.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 90:1:4:[82.3,6.0,79.2,87.1,77.1,88.2,1.0,89.3]:TopTopTopTop: -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc30)
% 15.13/3.80 94:1:4:[82.3,7.1,79.2,91.2,77.1,92.3,1.0,93.4]:TopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc31) ->
% 15.13/3.80 99:1:5:[86.4,8.0,82.3,95.1,79.2,96.2,77.1,97.3,1.0,98.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.13/3.80 104:1:5:[86.4,9.0,82.3,100.1,79.2,101.2,77.1,102.3,1.0,103.4]:TopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28)
% 15.13/3.80 109:1:5:[86.4,10.1,82.3,105.2,79.2,106.3,77.1,107.4,1.0,108.5]:TopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29) ->
% 15.13/3.80 115:1:6:[99.5,11.0,86.4,110.1,82.3,111.2,79.2,112.3,77.1,113.4,1.0,114.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 15.13/3.80 121:1:6:[99.5,12.0,86.4,116.1,82.3,117.2,79.2,118.3,77.1,119.4,1.0,120.5]:TopTopTopTopTopTop: -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26)
% 15.13/3.80 127:1:6:[99.5,13.1,86.4,122.2,82.3,123.3,79.2,124.4,77.1,125.5,1.0,126.6]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27) ->
% 15.13/3.80 134:1:7:[115.6,14.0,99.5,128.1,86.4,129.2,82.3,130.3,79.2,131.4,77.1,132.5,1.0,133.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 15.13/3.80 141:1:7:[115.6,15.0,99.5,135.1,86.4,136.2,82.3,137.3,79.2,138.4,77.1,139.5,1.0,140.6]:TopTopTopTopTopTopTop: -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24)
% 15.13/3.80 148:1:7:[115.6,16.1,99.5,142.2,86.4,143.3,82.3,144.4,79.2,145.5,77.1,146.6,1.0,147.7]:TopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25) ->
% 15.13/3.80 156:1:8:[134.7,17.0,115.6,149.1,99.5,150.2,86.4,151.3,82.3,152.4,79.2,153.5,77.1,154.6,1.0,155.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 15.13/3.80 163:4:7:[115.6,18.0,99.5,157.2,86.4,158.4,82.3,159.6,79.2,160.7,77.1,161.8,1.0,162.9]:TopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.13/3.80 172:1:9:[156.8,19.0,134.7,164.1,115.6,165.2,99.5,166.3,86.4,167.4,82.3,168.5,79.2,169.6,77.1,170.7,1.0,171.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 15.13/3.80 182:1:10:[172.9,20.0,156.8,173.1,134.7,174.2,115.6,175.3,99.5,176.4,86.4,177.5,82.3,178.6,79.2,179.7,77.1,180.8,1.0,181.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 15.13/3.80 193:1:11:[182.10,21.0,172.9,183.1,156.8,184.2,134.7,185.3,115.6,186.4,99.5,187.5,86.4,188.6,82.3,189.7,79.2,190.8,77.1,191.9,1.0,192.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 15.13/3.80 205:1:12:[193.11,22.0,182.10,194.1,172.9,195.2,156.8,196.3,134.7,197.4,115.6,198.5,99.5,199.6,86.4,200.7,82.3,201.8,79.2,202.9,77.1,203.10,1.0,204.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 15.13/3.80 217:1:12:[193.11,23.0,182.10,206.1,172.9,207.2,156.8,208.3,134.7,209.4,115.6,210.5,99.5,211.6,86.4,212.7,82.3,213.8,79.2,214.9,77.1,215.10,1.0,216.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22)
% 15.13/3.80 229:1:12:[193.11,24.1,182.10,218.2,172.9,219.3,156.8,220.4,134.7,221.5,115.6,222.6,99.5,223.7,86.4,224.8,82.3,225.9,79.2,226.10,77.1,227.11,1.0,228.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23) ->
% 15.13/3.80 240:4:11:[182.10,25.0,172.9,230.1,156.8,231.2,134.7,232.3,115.6,233.4,99.5,234.5,86.4,235.6,82.3,236.7,79.2,237.8,77.1,238.9,1.0,239.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 251:4:11:[182.10,26.0,172.9,241.1,156.8,242.2,134.7,243.3,115.6,244.4,99.5,245.5,86.4,246.6,82.3,247.7,79.2,248.8,77.1,249.9,1.0,250.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.13/3.80 264:1:13:[205.12,27.0,193.11,252.1,182.10,253.2,172.9,254.3,156.8,255.4,134.7,256.5,115.6,257.6,99.5,258.7,86.4,259.8,82.3,260.9,79.2,261.10,77.1,262.11,1.0,263.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 15.13/3.80 277:1:13:[205.12,28.0,193.11,265.1,182.10,266.2,172.9,267.3,156.8,268.4,134.7,269.5,115.6,270.6,99.5,271.7,86.4,272.8,82.3,273.9,79.2,274.10,77.1,275.11,1.0,276.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20)
% 15.13/3.80 290:1:13:[205.12,29.1,193.11,278.2,182.10,279.3,172.9,280.4,156.8,281.5,134.7,282.6,115.6,283.7,99.5,284.8,86.4,285.9,82.3,286.10,79.2,287.11,77.1,288.12,1.0,289.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21) ->
% 15.13/3.80 302:4:12:[193.11,30.0,182.10,291.1,172.9,292.2,156.8,293.4,134.7,294.5,115.6,295.7,99.5,296.8,86.4,297.9,82.3,298.10,79.2,299.11,77.1,300.12,1.0,301.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 316:1:14:[264.13,31.0,205.12,303.1,193.11,304.2,182.10,305.3,172.9,306.4,156.8,307.5,134.7,308.6,115.6,309.7,99.5,310.8,86.4,311.9,82.3,312.10,79.2,313.11,77.1,314.12,1.0,315.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 15.13/3.80 330:1:14:[264.13,32.0,205.12,317.1,193.11,318.2,182.10,319.3,172.9,320.4,156.8,321.5,134.7,322.6,115.6,323.7,99.5,324.8,86.4,325.9,82.3,326.10,79.2,327.11,77.1,328.12,1.0,329.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18)
% 15.13/3.80 344:1:14:[264.13,33.1,205.12,331.2,193.11,332.3,182.10,333.4,172.9,334.5,156.8,335.6,134.7,336.7,115.6,337.8,99.5,338.9,86.4,339.10,82.3,340.11,79.2,341.12,77.1,342.13,1.0,343.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19) ->
% 15.13/3.80 357:4:13:[205.12,34.1,193.11,345.2,182.10,346.3,172.9,347.4,156.8,348.5,134.7,349.6,115.6,350.8,99.5,351.9,86.4,352.11,82.3,353.12,79.2,354.13,77.1,355.14,1.0,356.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 15.13/3.80 372:1:15:[316.14,35.0,264.13,358.1,205.12,359.2,193.11,360.3,182.10,361.4,172.9,362.5,156.8,363.6,134.7,364.7,115.6,365.8,99.5,366.9,86.4,367.10,82.3,368.11,79.2,369.12,77.1,370.13,1.0,371.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 15.13/3.80 387:1:15:[316.14,36.0,264.13,373.1,205.12,374.2,193.11,375.3,182.10,376.4,172.9,377.5,156.8,378.6,134.7,379.7,115.6,380.8,99.5,381.9,86.4,382.10,82.3,383.11,79.2,384.12,77.1,385.13,1.0,386.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16)
% 15.13/3.80 402:1:15:[316.14,37.1,264.13,388.2,205.12,389.3,193.11,390.4,182.10,391.5,172.9,392.6,156.8,393.7,134.7,394.8,115.6,395.9,99.5,396.10,86.4,397.11,82.3,398.12,79.2,399.13,77.1,400.14,1.0,401.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc17) ->
% 15.13/3.80 415:4:13:[205.12,38.0,193.11,403.3,182.10,404.4,172.9,405.5,156.8,406.6,134.7,407.7,115.6,408.8,99.5,409.9,86.4,410.10,82.3,411.11,79.2,412.12,77.1,413.13,1.0,414.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 15.13/3.80 429:4:14:[264.13,39.0,205.12,416.1,193.11,417.2,182.10,418.4,172.9,419.6,156.8,420.7,134.7,421.8,115.6,422.9,99.5,423.10,86.4,424.11,82.3,425.12,79.2,426.13,77.1,427.14,1.0,428.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 15.13/3.80 444:4:15:[316.14,40.0,264.13,430.1,205.12,431.2,193.11,432.3,182.10,433.4,172.9,434.5,156.8,435.7,134.7,436.8,115.6,437.9,99.5,438.10,86.4,439.11,82.3,440.12,79.2,441.13,77.1,442.15,1.0,443.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2)
% 15.13/3.80 460:1:16:[372.15,41.0,316.14,445.1,264.13,446.2,205.12,447.3,193.11,448.4,182.10,449.5,172.9,450.6,156.8,451.7,134.7,452.8,115.6,453.9,99.5,454.10,86.4,455.11,82.3,456.12,79.2,457.13,77.1,458.14,1.0,459.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 15.13/3.80 475:4:15:[316.14,42.0,264.13,461.1,205.12,462.2,193.11,463.3,182.10,464.4,172.9,465.5,156.8,466.6,134.7,467.7,115.6,468.9,99.5,469.10,86.4,470.11,82.3,471.12,79.2,472.13,77.1,473.15,1.0,474.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 15.13/3.80 490:4:15:[316.14,43.0,264.13,476.1,205.12,477.2,193.11,478.3,182.10,479.4,172.9,480.5,156.8,481.6,134.7,482.7,115.6,483.9,99.5,484.10,86.4,485.11,82.3,486.12,79.2,487.13,77.1,488.14,1.0,489.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 507:1:17:[460.16,44.0,372.15,491.1,316.14,492.2,264.13,493.3,205.12,494.4,193.11,495.5,182.10,496.6,172.9,497.7,156.8,498.8,134.7,499.9,115.6,500.10,99.5,501.11,86.4,502.12,82.3,503.13,79.2,504.14,77.1,505.15,1.0,506.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 15.13/3.80 522:4:15:[316.14,45.0,264.13,508.1,205.12,509.2,193.11,510.4,182.10,511.5,172.9,512.6,156.8,513.7,134.7,514.8,115.6,515.9,99.5,516.10,86.4,517.11,82.3,518.12,79.2,519.13,77.1,520.14,1.0,521.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 15.13/3.80 538:4:16:[372.15,46.0,316.14,523.2,264.13,524.4,205.12,525.5,193.11,526.6,182.10,527.7,172.9,528.8,156.8,529.9,134.7,530.10,115.6,531.11,99.5,532.12,86.4,533.13,82.3,534.14,79.2,535.15,77.1,536.16,1.0,537.17]: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) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv20_1r1(x0)
% 15.13/3.80 554:4:16:[372.15,47.0,316.14,539.2,264.13,540.3,205.12,541.4,193.11,542.5,182.10,543.6,172.9,544.7,156.8,545.8,134.7,546.9,115.6,547.10,99.5,548.11,86.4,549.12,82.3,550.14,79.2,551.15,77.1,552.16,1.0,553.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 15.13/3.80 570:4:16:[372.15,48.0,316.14,555.2,264.13,556.3,205.12,557.4,193.11,558.5,182.10,559.6,172.9,560.7,156.8,561.8,134.7,562.9,115.6,563.10,99.5,564.11,86.4,565.13,82.3,566.14,79.2,567.15,77.1,568.16,1.0,569.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 15.13/3.80 586:4:16:[372.15,49.0,316.14,571.2,264.13,572.4,205.12,573.6,193.11,574.7,182.10,575.8,172.9,576.9,156.8,577.10,134.7,578.11,115.6,579.12,99.5,580.13,86.4,581.15,82.3,582.16,79.2,583.17,77.1,584.18,1.0,585.19]: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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 15.13/3.80 604:1:18:[507.17,50.0,460.16,587.1,372.15,588.2,316.14,589.3,264.13,590.4,205.12,591.5,193.11,592.6,182.10,593.7,172.9,594.8,156.8,595.9,134.7,596.10,115.6,597.11,99.5,598.12,86.4,599.13,82.3,600.14,79.2,601.15,77.1,602.16,1.0,603.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 15.13/3.80 621:4:17:[460.16,51.0,372.15,605.2,316.14,606.3,264.13,607.4,205.12,608.5,193.11,609.6,182.10,610.7,172.9,611.8,156.8,612.9,134.7,613.10,115.6,614.11,99.5,615.13,86.4,616.14,82.3,617.15,79.2,618.16,77.1,619.17,1.0,620.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 638:4:17:[460.16,52.0,372.15,622.1,316.14,623.2,264.13,624.3,205.12,625.4,193.11,626.5,182.10,627.6,172.9,628.7,156.8,629.8,134.7,630.9,115.6,631.10,99.5,632.11,86.4,633.12,82.3,634.13,79.2,635.14,77.1,636.15,1.0,637.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.13/3.80 655:4:17:[460.16,53.0,372.15,639.1,316.14,640.2,264.13,641.3,205.12,642.4,193.11,643.5,182.10,644.6,172.9,645.7,156.8,646.8,134.7,647.9,115.6,648.10,99.5,649.11,86.4,650.13,82.3,651.14,79.2,652.15,77.1,653.16,1.0,654.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 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)
% 15.13/3.80 672:4:17:[460.16,54.0,372.15,656.1,316.14,657.2,264.13,658.3,205.12,659.4,193.11,660.5,182.10,661.6,172.9,662.7,156.8,663.8,134.7,664.9,115.6,665.11,99.5,666.12,86.4,667.13,82.3,668.14,79.2,669.15,77.1,670.16,1.0,671.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),ssPv20_1r1(x0)
% 15.13/3.80 689:4:17:[460.16,55.0,372.15,673.1,316.14,674.2,264.13,675.3,205.12,676.4,193.11,677.5,182.10,678.6,172.9,679.7,156.8,680.8,134.7,681.9,115.6,682.10,99.5,683.11,86.4,684.13,82.3,685.14,79.2,686.15,77.1,687.16,1.0,688.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 15.13/3.80 706:4:17:[460.16,56.0,372.15,690.2,316.14,691.3,264.13,692.4,205.12,693.5,193.11,694.6,182.10,695.7,172.9,696.8,156.8,697.9,134.7,698.10,115.6,699.11,99.5,700.12,86.4,701.13,82.3,702.14,79.2,703.15,77.1,704.16,1.0,705.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> 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),ssPv19_2r1r1(x0,x1)
% 15.13/3.80 723:4:17:[460.16,57.0,372.15,707.1,316.14,708.3,264.13,709.4,205.12,710.5,193.11,711.6,182.10,712.7,172.9,713.8,156.8,714.9,134.7,715.10,115.6,716.11,99.5,717.12,86.4,718.13,82.3,719.14,79.2,720.15,77.1,721.16,1.0,722.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv20_1r1(x0)
% 15.13/3.80 742:1:19:[604.18,58.0,507.17,724.1,460.16,725.2,372.15,726.3,316.14,727.4,264.13,728.5,205.12,729.6,193.11,730.7,182.10,731.8,172.9,732.9,156.8,733.10,134.7,734.11,115.6,735.12,99.5,736.13,86.4,737.14,82.3,738.15,79.2,739.16,77.1,740.17,1.0,741.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 15.13/3.80 760:4:18:[507.17,59.0,460.16,743.2,372.15,744.4,316.14,745.5,264.13,746.6,205.12,747.7,193.11,748.8,182.10,749.9,172.9,750.10,156.8,751.11,134.7,752.12,115.6,753.14,99.5,754.15,86.4,755.16,82.3,756.17,79.2,757.18,77.1,758.19,1.0,759.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv20_1r1(x0)
% 15.13/3.80 778:4:18:[507.17,60.1,460.16,761.3,372.15,762.4,316.14,763.5,264.13,764.6,205.12,765.7,193.11,766.8,182.10,767.9,172.9,768.10,156.8,769.11,134.7,770.12,115.6,771.13,99.5,772.14,86.4,773.15,82.3,774.16,79.2,775.17,77.1,776.18,1.0,777.19]: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) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.13/3.80 797:4:19:[604.18,61.0,507.17,779.1,460.16,780.2,372.15,781.3,316.14,782.4,264.13,783.5,205.12,784.6,193.11,785.7,182.10,786.9,172.9,787.10,156.8,788.11,134.7,789.12,115.6,790.13,99.5,791.14,86.4,792.15,82.3,793.16,79.2,794.17,77.1,795.18,1.0,796.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.13/3.80 816:4:19:[604.18,62.0,507.17,798.2,460.16,799.3,372.15,800.4,316.14,801.5,264.13,802.6,205.12,803.7,193.11,804.8,182.10,805.9,172.9,806.10,156.8,807.11,134.7,808.12,115.6,809.13,99.5,810.14,86.4,811.15,82.3,812.16,79.2,813.17,77.1,814.18,1.0,815.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.13/3.80 835:4:19:[604.18,63.0,507.17,817.2,460.16,818.3,372.15,819.4,316.14,820.6,264.13,821.7,205.12,822.8,193.11,823.9,182.10,824.10,172.9,825.11,156.8,826.12,134.7,827.14,115.6,828.15,99.5,829.16,86.4,830.17,82.3,831.18,79.2,832.19,77.1,833.21,1.0,834.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_1r1(x0) ->
% 15.13/3.80 854:4:19:[604.18,64.0,507.17,836.2,460.16,837.3,372.15,838.4,316.14,839.5,264.13,840.7,205.12,841.8,193.11,842.9,182.10,843.10,172.9,844.11,156.8,845.12,134.7,846.14,115.6,847.15,99.5,848.16,86.4,849.17,82.3,850.19,79.2,851.20,77.1,852.21,1.0,853.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv18_3r1r1r1(x0,x1,x2) ->
% 15.13/3.80 873:4:19:[604.18,65.0,507.17,855.2,460.16,856.3,372.15,857.4,316.14,858.5,264.13,859.6,205.12,860.7,193.11,861.8,182.10,862.9,172.9,863.10,156.8,864.11,134.7,865.12,115.6,866.13,99.5,867.14,86.4,868.15,82.3,869.16,79.2,870.17,77.1,871.18,1.0,872.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 15.13/3.80 892:4:19:[604.18,66.0,507.17,874.2,460.16,875.3,372.15,876.4,316.14,877.5,264.13,878.6,205.12,879.7,193.11,880.8,182.10,881.9,172.9,882.10,156.8,883.11,134.7,884.12,115.6,885.13,99.5,886.15,86.4,887.16,82.3,888.17,79.2,889.18,77.1,890.19,1.0,891.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 15.13/3.80 911:4:19:[604.18,67.1,507.17,893.3,460.16,894.4,372.15,895.5,316.14,896.6,264.13,897.7,205.12,898.8,193.11,899.9,182.10,900.10,172.9,901.11,156.8,902.12,134.7,903.14,115.6,904.15,99.5,905.17,86.4,906.18,82.3,907.19,79.2,908.20,77.1,909.21,1.0,910.22]: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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ->
% 15.13/3.80 930:4:19:[604.18,68.0,507.17,912.1,460.16,913.2,372.15,914.3,316.14,915.4,264.13,916.6,205.12,917.7,193.11,918.8,182.10,919.9,172.9,920.10,156.8,921.12,134.7,922.13,115.6,923.14,99.5,924.15,86.4,925.16,82.3,926.17,79.2,927.18,77.1,928.19,1.0,929.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 15.13/3.80 950:4:20:[742.19,69.0,604.18,931.1,507.17,932.2,460.16,933.3,372.15,934.4,316.14,935.5,264.13,936.6,205.12,937.7,193.11,938.8,182.10,939.9,172.9,940.10,156.8,941.12,134.7,942.13,115.6,943.14,99.5,944.15,86.4,945.16,82.3,946.17,79.2,947.18,77.1,948.20,1.0,949.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.13/3.80 970:4:20:[742.19,70.0,604.18,951.2,507.17,952.3,460.16,953.4,372.15,954.5,316.14,955.6,264.13,956.7,205.12,957.8,193.11,958.9,182.10,959.10,172.9,960.11,156.8,961.13,134.7,962.14,115.6,963.15,99.5,964.16,86.4,965.17,82.3,966.18,79.2,967.19,77.1,968.20,1.0,969.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 990:4:20:[742.19,71.0,604.18,971.2,507.17,972.3,460.16,973.4,372.15,974.5,316.14,975.6,264.13,976.7,205.12,977.8,193.11,978.9,182.10,979.10,172.9,980.11,156.8,981.13,134.7,982.14,115.6,983.15,99.5,984.16,86.4,985.17,82.3,986.18,79.2,987.19,77.1,988.20,1.0,989.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 15.13/3.80 1010:4:20:[742.19,72.0,604.18,991.2,507.17,992.3,460.16,993.4,372.15,994.6,316.14,995.7,264.13,996.9,205.12,997.10,193.11,998.11,182.10,999.12,172.9,1000.13,156.8,1001.14,134.7,1002.15,115.6,1003.16,99.5,1004.17,86.4,1005.18,82.3,1006.19,79.2,1007.20,77.1,1008.21,1.0,1009.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 1030:4:20:[742.19,73.1,604.18,1011.2,507.17,1012.3,460.16,1013.4,372.15,1014.5,316.14,1015.6,264.13,1016.7,205.12,1017.8,193.11,1018.9,182.10,1019.10,172.9,1020.11,156.8,1021.12,134.7,1022.13,115.6,1023.15,99.5,1024.16,86.4,1025.17,82.3,1026.18,79.2,1027.19,77.1,1028.20,1.0,1029.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 15.13/3.80 1050:4:20:[742.19,74.1,604.18,1031.2,507.17,1032.3,460.16,1033.4,372.15,1034.5,316.14,1035.6,264.13,1036.7,205.12,1037.8,193.11,1038.9,182.10,1039.10,172.9,1040.11,156.8,1041.12,134.7,1042.14,115.6,1043.15,99.5,1044.16,86.4,1045.17,82.3,1046.18,79.2,1047.19,77.1,1048.20,1.0,1049.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 15.13/3.80 1071:3:20:[742.19,75.1,604.18,1051.2,507.17,1052.3,460.16,1053.4,1050.23,1054.5,372.15,1055.6,316.14,1056.7,264.13,1057.8,205.12,1058.9,193.11,1059.10,182.10,1060.11,172.9,1061.12,156.8,1062.13,134.7,1063.15,115.6,1064.16,99.5,1065.17,86.4,1066.18,82.3,1067.19,79.2,1068.20,77.1,1069.21,1.0,1070.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 15.13/3.80 1091:4:20:[742.19,76.1,604.18,1072.3,507.17,1073.4,460.16,1074.5,372.15,1075.7,316.14,1076.8,264.13,1077.9,205.12,1078.10,193.11,1079.11,182.10,1080.12,172.9,1081.13,156.8,1082.14,134.7,1083.15,115.6,1084.16,99.5,1085.17,86.4,1086.18,82.3,1087.19,79.2,1088.20,77.1,1089.21,1.0,1090.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 15.13/3.80
% 15.13/3.80 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) ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv17_4r1r1r1r1(x0,x1,x2,x3) ssPv18_3r1r1r1(x0,x1,x2) ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) 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) ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssNder1_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) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv20_1r1(x0) ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssNder1_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) ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) 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) ssPv19_2r1r1(x0,x1) 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)
% 15.13/3.80
% 15.13/3.80 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: resolution_2 ===
% 15.13/3.80
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 56
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 911:4:19:[604.18,67.1,507.17,893.3,460.16,894.4,372.15,895.5,316.14,896.6,264.13,897.7,205.12,898.8,193.11,899.9,182.10,900.10,172.9,901.11,156.8,902.12,134.7,903.14,115.6,904.15,99.5,905.17,86.4,906.18,82.3,907.19,79.2,908.20,77.1,909.21,1.0,910.22]: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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> {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}
% 15.13/3.80 === Backtracking. Learning clause 1092:3:18:[911.4,90.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5) ->
% 15.13/3.80 === Conflict found: 892:4:19:[604.18,66.0,507.17,874.2,460.16,875.3,372.15,876.4,316.14,877.5,264.13,878.6,205.12,879.7,193.11,880.8,182.10,881.9,172.9,882.10,156.8,883.11,134.7,884.12,115.6,885.13,99.5,886.15,86.4,887.16,82.3,888.17,79.2,889.18,77.1,890.19,1.0,891.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {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}
% 15.13/3.80 === Backtracking. Learning clause 1093:3:18:[892.2,90.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10)
% 15.13/3.80 === Conflict found: 621:4:17:[460.16,51.0,372.15,605.2,316.14,606.3,264.13,607.4,205.12,608.5,193.11,609.6,182.10,610.7,172.9,611.8,156.8,612.9,134.7,613.10,115.6,614.11,99.5,615.13,86.4,616.14,82.3,617.15,79.2,618.16,77.1,619.17,1.0,620.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> 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, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1094:3:16:[621.2,90.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 66
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 797:4:19:[604.18,61.0,507.17,779.1,460.16,780.2,372.15,781.3,316.14,782.4,264.13,783.5,205.12,784.6,193.11,785.7,182.10,786.9,172.9,787.10,156.8,788.11,134.7,789.12,115.6,790.13,99.5,791.14,86.4,792.15,82.3,793.16,79.2,794.17,77.1,795.18,1.0,796.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {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}
% 15.13/3.80 === Backtracking. Learning clause 1095:3:18:[797.4,94.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4)
% 15.13/3.80 === Conflict found: 638:4:17:[460.16,52.0,372.15,622.1,316.14,623.2,264.13,624.3,205.12,625.4,193.11,626.5,182.10,627.6,172.9,628.7,156.8,629.8,134.7,630.9,115.6,631.10,99.5,632.11,86.4,633.12,82.3,634.13,79.2,635.14,77.1,636.15,1.0,637.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {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}
% 15.13/3.80 === Backtracking. Learning clause 1096:3:16:[638.4,94.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4)
% 15.13/3.80 === Conflict found: 251:4:11:[182.10,26.0,172.9,241.1,156.8,242.2,134.7,243.3,115.6,244.4,99.5,245.5,86.4,246.6,82.3,247.7,79.2,248.8,77.1,249.9,1.0,250.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1097:3:10:[251.4,94.1]:TopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4)
% 15.13/3.80 === Conflict found: 163:4:7:[115.6,18.0,99.5,157.2,86.4,158.4,82.3,159.6,79.2,160.7,77.1,161.8,1.0,162.9]:TopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1098:3:6:[163.4,94.1]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv18_3r1r1r1(x0,x1,x2) ->
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 77
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1030:4:20:[742.19,73.1,604.18,1011.2,507.17,1012.3,460.16,1013.4,372.15,1014.5,316.14,1015.6,264.13,1016.7,205.12,1017.8,193.11,1018.9,182.10,1019.10,172.9,1020.11,156.8,1021.12,134.7,1022.13,115.6,1023.15,99.5,1024.16,86.4,1025.17,82.3,1026.18,79.2,1027.19,77.1,1028.20,1.0,1029.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),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 -> 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, x19 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1099:3:19:[1030.2,104.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 15.13/3.80 === Conflict found: 475:4:15:[316.14,42.0,264.13,461.1,205.12,462.2,193.11,463.3,182.10,464.4,172.9,465.5,156.8,466.6,134.7,467.7,115.6,468.9,99.5,469.10,86.4,470.11,82.3,471.12,79.2,472.13,77.1,473.15,1.0,474.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),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}
% 15.13/3.80 === Backtracking. Learning clause 1100:3:14:[475.1,104.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8)
% 15.13/3.80 === Conflict found: 302:4:12:[193.11,30.0,182.10,291.1,172.9,292.2,156.8,293.4,134.7,294.5,115.6,295.7,99.5,296.8,86.4,297.9,82.3,298.10,79.2,299.11,77.1,300.12,1.0,301.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1101:3:11:[302.2,104.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 84
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1094:3:16:[621.2,90.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> 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, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1102:2:15:[1094.2,109.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 148
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 154
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1071:3:20:[742.19,75.1,604.18,1051.2,507.17,1052.3,460.16,1053.4,1050.23,1054.5,372.15,1055.6,316.14,1056.7,264.13,1057.8,205.12,1058.9,193.11,1059.10,182.10,1060.11,172.9,1061.12,156.8,1062.13,134.7,1063.15,115.6,1064.16,99.5,1065.17,86.4,1066.18,82.3,1067.19,79.2,1068.20,77.1,1069.21,1.0,1070.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) {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, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1103:2:19:[1071.2,121.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 163
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1091:4:20:[742.19,76.1,604.18,1072.3,507.17,1073.4,460.16,1074.5,372.15,1075.7,316.14,1076.8,264.13,1077.9,205.12,1078.10,193.11,1079.11,182.10,1080.12,172.9,1081.13,156.8,1082.14,134.7,1083.15,115.6,1084.16,99.5,1085.17,86.4,1086.18,82.3,1087.19,79.2,1088.20,77.1,1089.21,1.0,1090.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1104:3:19:[1091.4,127.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13) ->
% 15.13/3.80 === Conflict found: 655:4:17:[460.16,53.0,372.15,639.1,316.14,640.2,264.13,641.3,205.12,642.4,193.11,643.5,182.10,644.6,172.9,645.7,156.8,646.8,134.7,647.9,115.6,648.10,99.5,649.11,86.4,650.13,82.3,651.14,79.2,652.15,77.1,653.16,1.0,654.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 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) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1105:3:16:[655.4,127.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6)
% 15.13/3.80 === Conflict found: 429:4:14:[264.13,39.0,205.12,416.1,193.11,417.2,182.10,418.4,172.9,419.6,156.8,420.7,134.7,421.8,115.6,422.9,99.5,423.10,86.4,424.11,82.3,425.12,79.2,426.13,77.1,427.14,1.0,428.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1106:3:13:[429.4,127.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 171
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 930:4:19:[604.18,68.0,507.17,912.1,460.16,913.2,372.15,914.3,316.14,915.4,264.13,916.6,205.12,917.7,193.11,918.8,182.10,919.9,172.9,920.10,156.8,921.12,134.7,922.13,115.6,923.14,99.5,924.15,86.4,925.16,82.3,926.17,79.2,927.18,77.1,928.19,1.0,929.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1107:3:18:[930.2,141.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10)
% 15.13/3.80 === Conflict found: 444:4:15:[316.14,40.0,264.13,430.1,205.12,431.2,193.11,432.3,182.10,433.4,172.9,434.5,156.8,435.7,134.7,436.8,115.6,437.9,99.5,438.10,86.4,439.11,82.3,440.12,79.2,441.13,77.1,442.15,1.0,443.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1108:3:14:[444.1,141.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2)
% 15.13/3.80 === Conflict found: 302:4:12:[193.11,30.0,182.10,291.1,172.9,292.2,156.8,293.4,134.7,294.5,115.6,295.7,99.5,296.8,86.4,297.9,82.3,298.10,79.2,299.11,77.1,300.12,1.0,301.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1109:2:10:[302.1,141.1,104.1]:TopTopTopTopTopTopTopTopTopTop: -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,skc24,x6,x7,x8,x9),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Conflict found: 357:4:13:[205.12,34.1,193.11,345.2,182.10,346.3,172.9,347.4,156.8,348.5,134.7,349.6,115.6,350.8,99.5,351.9,86.4,352.11,82.3,353.12,79.2,354.13,77.1,355.14,1.0,356.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {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}
% 15.13/3.80 === Backtracking. Learning clause 1110:4:16:[357.4,586.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,x14,x15),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 179
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 415:4:13:[205.12,38.0,193.11,403.3,182.10,404.4,172.9,405.5,156.8,406.6,134.7,407.7,115.6,408.8,99.5,409.9,86.4,410.10,82.3,411.11,79.2,412.12,77.1,413.13,1.0,414.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1111:3:12:[415.4,148.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10)
% 15.13/3.80 === Conflict found: 1105:3:16:[655.4,127.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc25, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1112:2:15:[1105.3,148.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,skc25,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 243
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 251
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1010:4:20:[742.19,72.0,604.18,991.2,507.17,992.3,460.16,993.4,372.15,994.6,316.14,995.7,264.13,996.9,205.12,997.10,193.11,998.11,182.10,999.12,172.9,1000.13,156.8,1001.14,134.7,1002.15,115.6,1003.16,99.5,1004.17,86.4,1005.18,82.3,1006.19,79.2,1007.20,77.1,1008.21,1.0,1009.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3) {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 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1113:3:19:[1010.3,217.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Conflict found: 538:4:16:[372.15,46.0,316.14,523.2,264.13,524.4,205.12,525.5,193.11,526.6,182.10,527.7,172.9,528.8,156.8,529.9,134.7,530.10,115.6,531.11,99.5,532.12,86.4,533.13,82.3,534.14,79.2,535.15,77.1,536.16,1.0,537.17]: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) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),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 -> skc30, x15 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1114:3:15:[538.2,217.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x14) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv20_1r1(x0)
% 15.13/3.80 === Conflict found: 930:4:19:[604.18,68.0,507.17,912.1,460.16,913.2,372.15,914.3,316.14,915.4,264.13,916.6,205.12,917.7,193.11,918.8,182.10,919.9,172.9,920.10,156.8,921.12,134.7,922.13,115.6,923.14,99.5,924.15,86.4,925.16,82.3,926.17,79.2,927.18,77.1,928.19,1.0,929.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {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 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1115:2:17:[930.1,217.1,141.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,skc22,x11,x12,x13,x14,x15,x16),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 254
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 873:4:19:[604.18,65.0,507.17,855.2,460.16,856.3,372.15,857.4,316.14,858.5,264.13,859.6,205.12,860.7,193.11,861.8,182.10,862.9,172.9,863.10,156.8,864.11,134.7,865.12,115.6,866.13,99.5,867.14,86.4,868.15,82.3,869.16,79.2,870.17,77.1,871.18,1.0,872.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {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, x17 -> skc30, x18 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1116:3:18:[873.2,229.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15,x16,x17) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 15.13/3.80 === Conflict found: 554:4:16:[372.15,47.0,316.14,539.2,264.13,540.3,205.12,541.4,193.11,542.5,182.10,543.6,172.9,544.7,156.8,545.8,134.7,546.9,115.6,547.10,99.5,548.11,86.4,549.12,82.3,550.14,79.2,551.15,77.1,552.16,1.0,553.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc23, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1117:3:15:[554.3,229.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) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 15.13/3.80 === Conflict found: 522:4:15:[316.14,45.0,264.13,508.1,205.12,509.2,193.11,510.4,182.10,511.5,172.9,512.6,156.8,513.7,134.7,514.8,115.6,515.9,99.5,516.10,86.4,517.11,82.3,518.12,79.2,519.13,77.1,520.14,1.0,521.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,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 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1118:3:14:[522.3,229.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 15.13/3.80 === Conflict found: 930:4:19:[604.18,68.0,507.17,912.1,460.16,913.2,372.15,914.3,316.14,915.4,264.13,916.6,205.12,917.7,193.11,918.8,182.10,919.9,172.9,920.10,156.8,921.12,134.7,922.13,115.6,923.14,99.5,924.15,86.4,925.16,82.3,926.17,79.2,927.18,77.1,928.19,1.0,929.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {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 -> skc28}
% 15.13/3.80 === Backtracking. Learning clause 1119:6:23:[930.2,415.4,586.3,570.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x13,x14,x15,x16),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x13,x17,x18,x19,x20,x21,x22),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 257
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 723:4:17:[460.16,57.0,372.15,707.1,316.14,708.3,264.13,709.4,205.12,710.5,193.11,711.6,182.10,712.7,172.9,713.8,156.8,714.9,134.7,715.10,115.6,716.11,99.5,717.12,86.4,718.13,82.3,719.14,79.2,720.15,77.1,721.16,1.0,722.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,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 -> skc20, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1120:3:16:[723.1,277.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13),ssPv20_1r1(x0)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 261
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1106:3:13:[429.4,127.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12) {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}
% 15.13/3.80 === Backtracking. Learning clause 1121:2:9:[1106.3,290.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7) ->
% 15.13/3.80 === Conflict found: 1093:3:18:[892.2,90.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc27, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc21, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1122:2:17:[1093.2,290.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,skc21,x12,x13,x14,x15,x16) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 325
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 331
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 760:4:18:[507.17,59.0,460.16,743.2,372.15,744.4,316.14,745.5,264.13,746.6,205.12,747.7,193.11,748.8,182.10,749.9,172.9,750.10,156.8,751.11,134.7,752.12,115.6,753.14,99.5,754.15,86.4,755.16,82.3,756.17,79.2,757.18,77.1,758.19,1.0,759.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1123:3:17:[760.2,330.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15,x16),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv20_1r1(x0)
% 15.13/3.80 === Conflict found: 706:4:17:[460.16,56.0,372.15,690.2,316.14,691.3,264.13,692.4,205.12,693.5,193.11,694.6,182.10,695.7,172.9,696.8,156.8,697.9,134.7,698.10,115.6,699.11,99.5,700.12,86.4,701.13,82.3,702.14,79.2,703.15,77.1,704.16,1.0,705.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> 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),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1124:3:16:[706.1,330.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv19_2r1r1(x0,x1)
% 15.13/3.80 === Conflict found: 1104:3:19:[1091.4,127.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13) -> {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 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1125:2:18:[1104.3,330.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14,x15,x16),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14,x15,x16,x17) ->
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 340
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 522:4:15:[316.14,45.0,264.13,508.1,205.12,509.2,193.11,510.4,182.10,511.5,172.9,512.6,156.8,513.7,134.7,514.8,115.6,515.9,99.5,516.10,86.4,517.11,82.3,518.12,79.2,519.13,77.1,520.14,1.0,521.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc20, x14 -> skc19}
% 15.13/3.80 === Backtracking. Learning clause 1126:2:11:[522.2,344.1,229.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 15.13/3.80 === Conflict found: 1108:3:14:[444.1,141.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc23, x12 -> skc20, x13 -> skc19}
% 15.13/3.80 === Backtracking. Learning clause 1127:2:3:[1108.2,344.1]:TopTopTop: ssPv20_1r1(x0) -> ssPv18_3r1r1r1(x0,x1,x2)
% 15.13/3.80 === Conflict found: 1099:3:19:[1030.2,104.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc24, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc23, x12 -> skc20, x13 -> skc19, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1128:2:18:[1099.3,344.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,skc19,x13,x14,x15,x16) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,skc19,x13,x14,x15,x16,x17)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 342
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1110:4:16:[357.4,586.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,x14,x15),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),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, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc16}
% 15.13/3.80 === Backtracking. Learning clause 1129:3:12:[1110.2,387.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 15.13/3.80 === Conflict found: 586:4:16:[372.15,49.0,316.14,571.2,264.13,572.4,205.12,573.6,193.11,574.7,182.10,575.8,172.9,576.9,156.8,577.10,134.7,578.11,115.6,579.12,99.5,580.13,86.4,581.15,82.3,582.16,79.2,583.17,77.1,584.18,1.0,585.19]: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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),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, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc16}
% 15.13/3.80 === Backtracking. Learning clause 1130:3:13:[586.1,387.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 15.13/3.80 === Conflict found: 538:4:16:[372.15,46.0,316.14,523.2,264.13,524.4,205.12,525.5,193.11,526.6,182.10,527.7,172.9,528.8,156.8,529.9,134.7,530.10,115.6,531.11,99.5,532.12,86.4,533.13,82.3,534.14,79.2,535.15,77.1,536.16,1.0,537.17]: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) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),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 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc16}
% 15.13/3.80 === Backtracking. Learning clause 1131:2:9:[538.1,387.1,217.1]:TopTopTopTopTopTopTopTopTop: -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv20_1r1(x0)
% 15.13/3.80 === Conflict found: 490:4:15:[316.14,43.0,264.13,476.1,205.12,477.2,193.11,478.3,182.10,479.4,172.9,480.5,156.8,481.6,134.7,482.7,115.6,483.9,99.5,484.10,86.4,485.11,82.3,486.12,79.2,487.13,77.1,488.14,1.0,489.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),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, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc31, x14 -> skc19}
% 15.13/3.80 === Backtracking. Learning clause 1132:3:9:[490.2,344.1]:TopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 343
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 672:4:17:[460.16,54.0,372.15,656.1,316.14,657.2,264.13,658.3,205.12,659.4,193.11,660.5,182.10,661.6,172.9,662.7,156.8,663.8,134.7,664.9,115.6,665.11,99.5,666.12,86.4,667.13,82.3,668.14,79.2,669.15,77.1,670.16,1.0,671.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),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 -> skc17, x16 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1133:3:16:[672.2,402.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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,skc17,x15),ssPv20_1r1(x0)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 407
% 15.13/3.80 === Conflict found: 415:4:13:[205.12,38.0,193.11,403.3,182.10,404.4,172.9,405.5,156.8,406.6,134.7,407.7,115.6,408.8,99.5,409.9,86.4,410.10,82.3,411.11,79.2,412.12,77.1,413.13,1.0,414.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),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 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1134:4:13:[415.3,1130.2]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 15.13/3.80 === Conflict found: 1091:4:20:[742.19,76.1,604.18,1072.3,507.17,1073.4,460.16,1074.5,372.15,1075.7,316.14,1076.8,264.13,1077.9,205.12,1078.10,193.11,1079.11,182.10,1080.12,172.9,1081.13,156.8,1082.14,134.7,1083.15,115.6,1084.16,99.5,1085.17,86.4,1086.18,82.3,1087.19,79.2,1088.20,77.1,1089.21,1.0,1090.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {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, x19 -> skc28}
% 15.13/3.80 === Backtracking. Learning clause 1136:5:25:[1071.1,1135.4,1091.3,1030.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x20,x21,x22,x23),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x20,x21,x22,x23,x24)
% 15.13/3.80 === Conflict found: 950:4:20:[742.19,69.0,604.18,931.1,507.17,932.2,460.16,933.3,372.15,934.4,316.14,935.5,264.13,936.6,205.12,937.7,193.11,938.8,182.10,939.9,172.9,940.10,156.8,941.12,134.7,942.13,115.6,943.14,99.5,944.15,86.4,945.16,82.3,946.17,79.2,947.18,77.1,948.20,1.0,949.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {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, x19 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1137:6:19:[950.1,816.3,1091.2,475.3]: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),ssPv20_1r1(x0) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 414
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 706:4:17:[460.16,56.0,372.15,690.2,316.14,691.3,264.13,692.4,205.12,693.5,193.11,694.6,182.10,695.7,172.9,696.8,156.8,697.9,134.7,698.10,115.6,699.11,99.5,700.12,86.4,701.13,82.3,702.14,79.2,703.15,77.1,704.16,1.0,705.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> 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),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc27, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20, x14 -> skc18, x15 -> skc17, x16 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1138:4:13:[706.2,1102.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5),ssPv19_2r1r1(x0,x1),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 421
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1010:4:20:[742.19,72.0,604.18,991.2,507.17,992.3,460.16,993.4,372.15,994.6,316.14,995.7,264.13,996.9,205.12,997.10,193.11,998.11,182.10,999.12,172.9,1000.13,156.8,1001.14,134.7,1002.15,115.6,1003.16,99.5,1004.17,86.4,1005.18,82.3,1006.19,79.2,1007.20,77.1,1008.21,1.0,1009.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> 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 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1139:3:17:[1010.1,1103.2,217.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,skc22,x11,x12),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,skc22,x11,x12,x13,x14,x15,x16) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 421
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 302:4:12:[193.11,30.0,182.10,291.1,172.9,292.2,156.8,293.4,134.7,294.5,115.6,295.7,99.5,296.8,86.4,297.9,82.3,298.10,79.2,299.11,77.1,300.12,1.0,301.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1140:3:11:[302.1,141.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Conflict found: 1124:3:16:[706.1,330.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc27, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20, x14 -> skc17, x15 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1141:2:15:[1124.2,148.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11,x12,skc18,x13,x14),ssPv19_2r1r1(x0,x1)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 423
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1091:4:20:[742.19,76.1,604.18,1072.3,507.17,1073.4,460.16,1074.5,372.15,1075.7,316.14,1076.8,264.13,1077.9,205.12,1078.10,193.11,1079.11,182.10,1080.12,172.9,1081.13,156.8,1082.14,134.7,1083.15,115.6,1084.16,99.5,1085.17,86.4,1086.18,82.3,1087.19,79.2,1088.20,77.1,1089.21,1.0,1090.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {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, x19 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1142:5:19:[1091.4,1098.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv18_3r1r1r1(x0,x1,x2) ->
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 487
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 496
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 892:4:19:[604.18,66.0,507.17,874.2,460.16,875.3,372.15,876.4,316.14,877.5,264.13,878.6,205.12,879.7,193.11,880.8,182.10,881.9,172.9,882.10,156.8,883.11,134.7,884.12,115.6,885.13,99.5,886.15,86.4,887.16,82.3,888.17,79.2,889.18,77.1,890.19,1.0,891.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc21, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1143:1:10:[892.1,1115.1,90.1,290.1]:TopTopTopTopTopTopTopTopTopTop: -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,skc24,x6,x7,x8,x9)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 498
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1110:4:16:[357.4,586.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,x14,x15),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> {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 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1144:3:14:[1110.3,1143.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12,x13),ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 15.13/3.80 === Conflict found: 1129:3:12:[1110.2,387.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1145:2:5:[1129.2,1143.1]:TopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 15.13/3.80 === Conflict found: 1124:3:16:[706.1,330.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc27, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20, x14 -> skc17, x15 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1146:3:6:[1124.1,1102.1]:TopTopTopTopTopTop: -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5),ssPv19_2r1r1(x0,x1),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 508
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 554:4:16:[372.15,47.0,316.14,539.2,264.13,540.3,205.12,541.4,193.11,542.5,182.10,543.6,172.9,544.7,156.8,545.8,134.7,546.9,115.6,547.10,99.5,548.11,86.4,549.12,82.3,550.14,79.2,551.15,77.1,552.16,1.0,553.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1147:4:15:[554.4,1121.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11)
% 15.13/3.80 === Conflict found: 1117:3:15:[554.3,229.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) -> 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 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1148:3:14:[1117.3,1121.1,1127.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,skc23,x11,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7),ssPv20_1r1(x0) ->
% 15.13/3.80 === Conflict found: 1130:3:13:[586.1,387.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> {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}
% 15.13/3.80 === Backtracking. Learning clause 1149:2:12:[1130.1,217.1,1102.2,1141.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv19_2r1r1(x0,x1)
% 15.13/3.80 === Conflict found: 1130:3:13:[586.1,387.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> {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}
% 15.13/3.80 === Backtracking. Learning clause 1150:2:12:[1130.1,217.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 509
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 723:4:17:[460.16,57.0,372.15,707.1,316.14,708.3,264.13,709.4,205.12,710.5,193.11,711.6,182.10,712.7,172.9,713.8,156.8,714.9,134.7,715.10,115.6,716.11,99.5,717.12,86.4,718.13,82.3,719.14,79.2,720.15,77.1,721.16,1.0,722.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,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 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1151:5:21:[723.3,1113.2,970.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x14,x15,x16,x17,x18),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x19,x20),ssPv20_1r1(x0),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.13/3.80 === Conflict found: 1121:2:9:[1106.3,290.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30}
% 15.13/3.80 === Backtracking. Learning clause 1152:2:9:[1121.2,1131.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8) -> ssPv20_1r1(x0)
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 573
% 15.13/3.80 === Clause set with instances from active satisfied. Growing active. New size: 576
% 15.13/3.80 === Restarting.
% 15.13/3.80 === Conflict found: 1121:2:9:[1106.3,290.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1153:3:9:[1121.2,1132.2]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.59/3.80 === Conflict found: 251:4:11:[182.10,26.0,172.9,241.1,156.8,242.2,134.7,243.3,115.6,244.4,99.5,245.5,86.4,246.6,82.3,247.7,79.2,248.8,77.1,249.9,1.0,250.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1154:4:15:[251.3,490.1,1126.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 584
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 990:4:20:[742.19,71.0,604.18,971.2,507.17,972.3,460.16,973.4,372.15,974.5,316.14,975.6,264.13,976.7,205.12,977.8,193.11,978.9,182.10,979.10,172.9,980.11,156.8,981.13,134.7,982.14,115.6,983.15,99.5,984.16,86.4,985.17,82.3,986.18,79.2,987.19,77.1,988.20,1.0,989.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc19, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1155:3:16:[990.1,1128.2,127.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,x10,x11,skc19,x12,x13,x14,x15) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,x10,x11,skc19,x12,x13)
% 15.59/3.80 === Conflict found: 1132:3:9:[490.2,344.1]:TopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc27, x7 -> skc30, x8 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1156:2:8:[1132.1,104.1,1121.2]:TopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 585
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1145:2:5:[1129.2,1143.1]:TopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc28}
% 15.59/3.80 === Backtracking. Learning clause 1157:1:4:[1145.1,104.1]:TopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 588
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 970:4:20:[742.19,70.0,604.18,951.2,507.17,952.3,460.16,953.4,372.15,954.5,316.14,955.6,264.13,956.7,205.12,957.8,193.11,958.9,182.10,959.10,172.9,960.11,156.8,961.13,134.7,962.14,115.6,963.15,99.5,964.16,86.4,965.17,82.3,966.18,79.2,967.19,77.1,968.20,1.0,969.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),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, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1158:3:20:[970.4,1157.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 15.59/3.80 === Conflict found: 1139:3:17:[1010.1,1103.2,217.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,skc22,x11,x12),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,skc22,x11,x12,x13,x14,x15,x16) -> 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, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1159:2:17:[1139.3,1157.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,skc22,x11,x12),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,skc22,x11,x12,x13,x14,x15,x16) ->
% 15.59/3.80 === Conflict found: 1113:3:19:[1010.3,217.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13) -> 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, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1160:2:19:[1113.3,1157.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13) ->
% 15.59/3.80 === Conflict found: 1101:3:11:[302.2,104.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10),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, x10 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1161:2:11:[1101.3,1157.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10)
% 15.59/3.80 === Conflict found: 1094:3:16:[621.2,90.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),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, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1162:2:16:[1094.3,1157.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4)
% 15.59/3.80 === Conflict found: 1156:2:8:[1132.1,104.1,1121.2]:TopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1163:1:8:[1156.2,1157.1]:TopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 652
% 15.59/3.80 === Conflict found: 816:4:19:[604.18,62.0,507.17,798.2,460.16,799.3,372.15,800.4,316.14,801.5,264.13,802.6,205.12,803.7,193.11,804.8,182.10,805.9,172.9,806.10,156.8,807.11,134.7,808.12,115.6,809.13,99.5,810.14,86.4,811.15,82.3,812.16,79.2,813.17,77.1,814.18,1.0,815.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc19, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1164:3:17:[816.2,1163.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 652
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1149:2:12:[1130.1,217.1,1102.2,1141.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1165:1:2:[1149.1,1143.1]:TopTop: -> ssPv19_2r1r1(x0,x1)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 652
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1030:4:20:[742.19,73.1,604.18,1011.2,507.17,1012.3,460.16,1013.4,372.15,1014.5,316.14,1015.6,264.13,1016.7,205.12,1017.8,193.11,1018.9,182.10,1019.10,172.9,1020.11,156.8,1021.12,134.7,1022.13,115.6,1023.15,99.5,1024.16,86.4,1025.17,82.3,1026.18,79.2,1027.19,77.1,1028.20,1.0,1029.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),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 -> skc30, 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}
% 15.59/3.80 === Backtracking. Learning clause 1166:5:19:[1030.3,1158.1]: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),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv6_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)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 652
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1117:3:15:[554.3,229.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) -> 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 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1167:2:13:[1117.3,1163.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,skc23,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 652
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1100:3:14:[475.1,104.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc27, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1168:2:13:[1100.3,1163.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,x10,x11,x12)
% 15.59/3.80 === Conflict found: 1168:2:13:[1100.3,1163.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc22, x11 -> skc30, x12 -> skc19}
% 15.59/3.80 === Backtracking. Learning clause 1169:1:1:[1168.2,344.1]:Top: ssPv20_1r1(x0) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 716
% 15.59/3.80 === Conflict found: 873:4:19:[604.18,65.0,507.17,855.2,460.16,856.3,372.15,857.4,316.14,858.5,264.13,859.6,205.12,860.7,193.11,861.8,182.10,862.9,172.9,863.10,156.8,864.11,134.7,865.12,115.6,866.13,99.5,867.14,86.4,868.15,82.3,869.16,79.2,870.17,77.1,871.18,1.0,872.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc27, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20, x14 -> skc18, x15 -> skc17, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1171:3:18:[1169.0,1170.3,873.3,1152.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 717
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1153:3:9:[1121.2,1132.2]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),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}
% 15.59/3.80 === Backtracking. Learning clause 1172:2:9:[1153.3,1157.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ->
% 15.59/3.80 === Conflict found: 1152:2:9:[1121.2,1131.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1173:1:9:[1152.2,1169.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 717
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 554:4:16:[372.15,47.0,316.14,539.2,264.13,540.3,205.12,541.4,193.11,542.5,182.10,543.6,172.9,544.7,156.8,545.8,134.7,546.9,115.6,547.10,99.5,548.11,86.4,549.12,82.3,550.14,79.2,551.15,77.1,552.16,1.0,553.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1174:3:14:[554.4,1163.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,x10)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 726
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 797:4:19:[604.18,61.0,507.17,779.1,460.16,780.2,372.15,781.3,316.14,782.4,264.13,783.5,205.12,784.6,193.11,785.7,182.10,786.9,172.9,787.10,156.8,788.11,134.7,789.12,115.6,790.13,99.5,791.14,86.4,792.15,82.3,793.16,79.2,794.17,77.1,795.18,1.0,796.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc26, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1175:3:12:[797.2,1159.2,94.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,skc26,x5,x6,x7),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,skc26,x5,x6,x7,x8,x9,skc22,x10,x11) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 730
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1162:2:16:[1094.3,1157.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc29, x5 -> skc27, x6 -> skc25, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc20, x13 -> skc18, x14 -> skc17, x15 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1176:1:15:[1162.2,109.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 794
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 800
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 778:4:18:[507.17,60.1,460.16,761.3,372.15,762.4,316.14,763.5,264.13,764.6,205.12,765.7,193.11,766.8,182.10,767.9,172.9,768.10,156.8,769.11,134.7,770.12,115.6,771.13,99.5,772.14,86.4,773.15,82.3,774.16,79.2,775.17,77.1,776.18,1.0,777.19]: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) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {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}
% 15.59/3.80 === Backtracking. Learning clause 1178:5:18:[1169.0,1177.5,778.1,723.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 15.59/3.80 === Conflict found: 760:4:18:[507.17,59.0,460.16,743.2,372.15,744.4,316.14,745.5,264.13,746.6,205.12,747.7,193.11,748.8,182.10,749.9,172.9,750.10,156.8,751.11,134.7,752.12,115.6,753.14,99.5,754.15,86.4,755.16,82.3,756.17,79.2,757.18,77.1,758.19,1.0,759.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc21, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1180:1:16:[1169.0,1179.1,760.3,104.1,330.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,skc18,x13,x14,x15) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 800
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1131:2:9:[538.1,387.1,217.1]:TopTopTopTopTopTopTopTopTop: -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc24}
% 15.59/3.80 === Backtracking. Learning clause 1181:1:9:[1131.2,1169.1]:TopTopTopTopTopTopTopTopTop: -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 802
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 723:4:17:[460.16,57.0,372.15,707.1,316.14,708.3,264.13,709.4,205.12,710.5,193.11,711.6,182.10,712.7,172.9,713.8,156.8,714.9,134.7,715.10,115.6,716.11,99.5,717.12,86.4,718.13,82.3,719.14,79.2,720.15,77.1,721.16,1.0,722.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv20_1r1(x0) {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}
% 15.59/3.80 === Backtracking. Learning clause 1184:6:27:[1169.0,1182.5,1157.0,1183.7,723.1,892.3,1010.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x19,x20,x21,x22,x23,x24),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x19,x25,x26),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 15.59/3.80 === Conflict found: 760:4:18:[507.17,59.0,460.16,743.2,372.15,744.4,316.14,745.5,264.13,746.6,205.12,747.7,193.11,748.8,182.10,749.9,172.9,750.10,156.8,751.11,134.7,752.12,115.6,753.14,99.5,754.15,86.4,755.16,82.3,756.17,79.2,757.18,77.1,758.19,1.0,759.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1186:2:17:[1169.0,1185.2,760.3,104.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 812
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1171:3:18:[1169.0,1170.3,873.3,1152.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc25, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc20, x13 -> skc18, x14 -> skc17, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1187:2:17:[1171.3,109.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,skc27,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,skc27,x5,x6,x7,x8,x9,x10)
% 15.59/3.80 === Conflict found: 240:4:11:[182.10,25.0,172.9,230.1,156.8,231.2,134.7,232.3,115.6,233.4,99.5,234.5,86.4,235.6,82.3,236.7,79.2,237.8,77.1,238.9,1.0,239.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1189:2:10:[1157.0,1188.2,240.3,94.1]:TopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 876
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 878
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1167:2:13:[1117.3,1163.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc27,x5,x6,x7,x8,x9,skc23,x10,x11,x12),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 -> skc16}
% 15.59/3.80 === Backtracking. Learning clause 1190:1:3:[1167.1,387.1]:TopTopTop: ssPv18_3r1r1r1(x0,x1,x2) ->
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 879
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 723:4:17:[460.16,57.0,372.15,707.1,316.14,708.3,264.13,709.4,205.12,710.5,193.11,711.6,182.10,712.7,172.9,713.8,156.8,714.9,134.7,715.10,115.6,716.11,99.5,717.12,86.4,718.13,82.3,719.14,79.2,720.15,77.1,721.16,1.0,722.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,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 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1192:3:21:[1169.0,1191.3,723.1,1158.3,1160.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x14,x15,x16,x17,x18) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x19,x20)
% 15.59/3.80 === Conflict found: 1192:3:21:[1169.0,1191.3,723.1,1158.3,1160.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x14,x15,x16,x17,x18) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22,x12,x13,x19,x20) {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 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30, x20 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1193:3:18:[1192.3,1162.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,skc22,x11,x12,x13,x14,x15,x16,x17) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 879
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1158:3:20:[970.4,1157.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> 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 -> skc30, x5 -> skc28, x6 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc21, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1194:2:19:[1158.2,141.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 887
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1120:3:16:[723.1,277.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc19, x14 -> skc17, x15 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1195:2:16:[1120.3,1169.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 951
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 961
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1111:3:12:[415.4,148.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1196:3:11:[1111.2,1189.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc25,x6,x7,x8,x9,x10) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc25,x6,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 966
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1166:5:19:[1030.3,1158.1]: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),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv6_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) {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 -> skc30, x14 -> skc19, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1197:2:16:[1166.2,104.1,141.1,344.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,skc24,x6,x7,x8,x9,x10,x11,skc19,x12,x13,x14,x15) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,skc24,x6,x7,x8,x9,x10,x11)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 969
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1195:2:16:[1120.3,1169.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20,x13) {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}
% 15.59/3.80 === Backtracking. Learning clause 1198:1:12:[1195.1,1176.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,skc20,x11)
% 15.59/3.80 === Clause set with instances from active satisfied. Growing active. New size: 976
% 15.59/3.80 === Restarting.
% 15.59/3.80 === Conflict found: 1092:3:18:[911.4,90.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc29, x5 -> skc26, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc22, x12 -> skc20, x13 -> skc19, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 15.59/3.80 === Backtracking. Learning clause 1199:2:17:[1092.3,121.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc26,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc26,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ->
% 15.59/3.80 === Conflict found: 1198:1:12:[1195.1,1176.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,skc20,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc26, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc22, x11 -> skc19}
% 15.59/3.80
% 15.59/3.80 SZS status Unsatisfiable
% 15.59/3.80
% 15.59/3.80 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.59/3.80
% 15.59/3.80 SPASS-SCL-FOL Statistics:
% 15.59/3.80 Number of learned clauses: 99
% 15.59/3.80 Number of propagations: 21890
% 15.59/3.80 Number of decisions: 9771
% 15.59/3.80 Number of resolutions: 124
% 15.59/3.80 Number of condensations: 6
% 15.59/3.80 Number of sub resolutions: 1024
% 15.59/3.80 Number of input literals (deduplicated): 56
% 15.59/3.80 Number of grows: 59
% 15.59/3.80 Number of considered ground atoms: 976
% 15.59/3.80
% 15.59/3.80 Needed: 0:00:03.03
% 15.59/3.80
%------------------------------------------------------------------------------