%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN875-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 : n021.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 22.11s 6.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN875-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n021.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:50:58 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.21/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 22.11/6.02 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.11/6.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.11/6.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.11/6.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.11/6.02 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.11/6.02 Execution resolution_2 ended with status: unsatisfiable
% 22.11/6.02 Used heuristic: resolution_2
% 22.11/6.02
% 22.11/6.02 Input Clauses:
% 22.11/6.02
% 22.11/6.02 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv16_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv15_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv14_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv13_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssPv11_10r1r1r1r1r1r1r1r1r1r1 ssPv20_1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv12_9r1r1r1r1r1r1r1r1r1 ssPv18_3r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv17_4r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ssPv19_2r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 22.11/6.02 Fol Constants: skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19 skc16 skc17
% 22.11/6.02 Fol Functions:
% 22.11/6.02 Problem Properties:
% 22.11/6.02 This is a Bernays Schoenfinkel problem.
% 22.11/6.02
% 22.11/6.02 After reduction: Problem Properties:
% 22.11/6.02 This is a Bernays Schoenfinkel problem.
% 22.11/6.02
% 22.11/6.02
% 22.11/6.02 Reduced Input Clauses:
% 22.11/6.02 67:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 22.11/6.02 69:1:2:[67.1,3.0,1.0,68.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 22.11/6.02 72:1:3:[69.2,4.0,67.1,70.1,1.0,71.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 22.11/6.02 76:1:4:[72.3,5.0,69.2,73.1,67.1,74.2,1.0,75.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 80:1:4:[72.3,6.0,69.2,77.1,67.1,78.2,1.0,79.3]:TopTopTopTop: -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc30)
% 22.11/6.02 84:1:4:[72.3,7.1,69.2,81.2,67.1,82.3,1.0,83.4]:TopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc31) ->
% 22.11/6.02 89:1:5:[76.4,8.0,72.3,85.1,69.2,86.2,67.1,87.3,1.0,88.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 22.11/6.02 94:1:5:[76.4,9.0,72.3,90.1,69.2,91.2,67.1,92.3,1.0,93.4]:TopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28)
% 22.11/6.02 99:1:5:[76.4,10.1,72.3,95.2,69.2,96.3,67.1,97.4,1.0,98.5]:TopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29) ->
% 22.11/6.02 105:1:6:[89.5,11.0,76.4,100.1,72.3,101.2,69.2,102.3,67.1,103.4,1.0,104.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 22.11/6.02 111:1:6:[89.5,12.0,76.4,106.1,72.3,107.2,69.2,108.3,67.1,109.4,1.0,110.5]:TopTopTopTopTopTop: -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26)
% 22.11/6.02 117:1:6:[89.5,13.1,76.4,112.2,72.3,113.3,69.2,114.4,67.1,115.5,1.0,116.6]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27) ->
% 22.11/6.02 124:1:7:[105.6,14.0,89.5,118.1,76.4,119.2,72.3,120.3,69.2,121.4,67.1,122.5,1.0,123.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 22.11/6.02 131:1:7:[105.6,15.0,89.5,125.1,76.4,126.2,72.3,127.3,69.2,128.4,67.1,129.5,1.0,130.6]:TopTopTopTopTopTopTop: -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24)
% 22.11/6.02 138:1:7:[105.6,16.1,89.5,132.2,76.4,133.3,72.3,134.4,69.2,135.5,67.1,136.6,1.0,137.7]:TopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25) ->
% 22.11/6.02 146:1:8:[124.7,17.0,105.6,139.1,89.5,140.2,76.4,141.3,72.3,142.4,69.2,143.5,67.1,144.6,1.0,145.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 22.11/6.02 155:1:9:[146.8,18.0,124.7,147.1,105.6,148.2,89.5,149.3,76.4,150.4,72.3,151.5,69.2,152.6,67.1,153.7,1.0,154.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 22.11/6.02 165:1:10:[155.9,19.0,146.8,156.1,124.7,157.2,105.6,158.3,89.5,159.4,76.4,160.5,72.3,161.6,69.2,162.7,67.1,163.8,1.0,164.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 22.11/6.02 176:1:11:[165.10,20.0,155.9,166.1,146.8,167.2,124.7,168.3,105.6,169.4,89.5,170.5,76.4,171.6,72.3,172.7,69.2,173.8,67.1,174.9,1.0,175.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 22.11/6.02 186:4:10:[155.9,21.0,146.8,177.1,124.7,178.2,105.6,179.3,89.5,180.4,76.4,181.5,72.3,182.6,69.2,183.7,67.1,184.8,1.0,185.9]:TopTopTopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0)
% 22.11/6.02 198:1:12:[176.11,22.0,165.10,187.1,155.9,188.2,146.8,189.3,124.7,190.4,105.6,191.5,89.5,192.6,76.4,193.7,72.3,194.8,69.2,195.9,67.1,196.10,1.0,197.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 22.11/6.02 210:1:12:[176.11,23.0,165.10,199.1,155.9,200.2,146.8,201.3,124.7,202.4,105.6,203.5,89.5,204.6,76.4,205.7,72.3,206.8,69.2,207.9,67.1,208.10,1.0,209.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22)
% 22.11/6.02 222:1:12:[176.11,24.1,165.10,211.2,155.9,212.3,146.8,213.4,124.7,214.5,105.6,215.6,89.5,216.7,76.4,217.8,72.3,218.9,69.2,219.10,67.1,220.11,1.0,221.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23) ->
% 22.11/6.02 235:1:13:[198.12,25.0,176.11,223.1,165.10,224.2,155.9,225.3,146.8,226.4,124.7,227.5,105.6,228.6,89.5,229.7,76.4,230.8,72.3,231.9,69.2,232.10,67.1,233.11,1.0,234.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 22.11/6.02 248:1:13:[198.12,26.0,176.11,236.1,165.10,237.2,155.9,238.3,146.8,239.4,124.7,240.5,105.6,241.6,89.5,242.7,76.4,243.8,72.3,244.9,69.2,245.10,67.1,246.11,1.0,247.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20)
% 22.11/6.02 261:1:13:[198.12,27.1,176.11,249.2,165.10,250.3,155.9,251.4,146.8,252.5,124.7,253.6,105.6,254.7,89.5,255.8,76.4,256.9,72.3,257.10,69.2,258.11,67.1,259.12,1.0,260.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21) ->
% 22.11/6.02 273:4:12:[176.11,28.0,165.10,262.2,155.9,263.3,146.8,264.4,124.7,265.5,105.6,266.6,89.5,267.8,76.4,268.9,72.3,269.10,69.2,270.11,67.1,271.12,1.0,272.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 22.11/6.02 287:1:14:[235.13,29.0,198.12,274.1,176.11,275.2,165.10,276.3,155.9,277.4,146.8,278.5,124.7,279.6,105.6,280.7,89.5,281.8,76.4,282.9,72.3,283.10,69.2,284.11,67.1,285.12,1.0,286.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 22.11/6.02 301:1:14:[235.13,30.0,198.12,288.1,176.11,289.2,165.10,290.3,155.9,291.4,146.8,292.5,124.7,293.6,105.6,294.7,89.5,295.8,76.4,296.9,72.3,297.10,69.2,298.11,67.1,299.12,1.0,300.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18)
% 22.11/6.02 315:1:14:[235.13,31.1,198.12,302.2,176.11,303.3,165.10,304.4,155.9,305.5,146.8,306.6,124.7,307.7,105.6,308.8,89.5,309.9,76.4,310.10,72.3,311.11,69.2,312.12,67.1,313.13,1.0,314.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19) ->
% 22.11/6.02 328:4:13:[198.12,32.0,176.11,316.1,165.10,317.2,155.9,318.3,146.8,319.4,124.7,320.6,105.6,321.7,89.5,322.8,76.4,323.9,72.3,324.10,69.2,325.11,67.1,326.12,1.0,327.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> 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),ssPv18_3r1r1r1(x0,x1,x2)
% 22.11/6.02 341:4:13:[198.12,33.0,176.11,329.2,165.10,330.3,155.9,331.4,146.8,332.5,124.7,333.6,105.6,334.8,89.5,335.9,76.4,336.10,72.3,337.12,69.2,338.13,67.1,339.14,1.0,340.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 22.11/6.02 356:1:15:[287.14,34.0,235.13,342.1,198.12,343.2,176.11,344.3,165.10,345.4,155.9,346.5,146.8,347.6,124.7,348.7,105.6,349.8,89.5,350.9,76.4,351.10,72.3,352.11,69.2,353.12,67.1,354.13,1.0,355.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 22.11/6.02 369:4:13:[198.12,35.1,176.11,357.3,165.10,358.4,155.9,359.5,146.8,360.6,124.7,361.7,105.6,362.9,89.5,363.10,76.4,364.11,72.3,365.12,69.2,366.13,67.1,367.14,1.0,368.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 22.11/6.02 384:1:15:[287.14,36.0,235.13,370.1,198.12,371.2,176.11,372.3,165.10,373.4,155.9,374.5,146.8,375.6,124.7,376.7,105.6,377.8,89.5,378.9,76.4,379.10,72.3,380.11,69.2,381.12,67.1,382.13,1.0,383.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16)
% 22.11/6.02 399:1:15:[287.14,37.1,235.13,385.2,198.12,386.3,176.11,387.4,165.10,388.5,155.9,389.6,146.8,390.7,124.7,391.8,105.6,392.9,89.5,393.10,76.4,394.11,72.3,395.12,69.2,396.13,67.1,397.14,1.0,398.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc17) ->
% 22.11/6.02 413:4:14:[235.13,38.0,198.12,400.1,176.11,401.2,165.10,402.3,155.9,403.4,146.8,404.6,124.7,405.7,105.6,406.8,89.5,407.9,76.4,408.11,72.3,409.12,69.2,410.13,67.1,411.14,1.0,412.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 22.11/6.02 427:4:14:[235.13,39.1,198.12,414.3,176.11,415.4,165.10,416.6,155.9,417.7,146.8,418.8,124.7,419.9,105.6,420.10,89.5,421.11,76.4,422.12,72.3,423.13,69.2,424.14,67.1,425.16,1.0,426.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv20_1r1(x0) ->
% 22.11/6.02 441:4:14:[235.13,40.0,198.12,428.2,176.11,429.3,165.10,430.4,155.9,431.5,146.8,432.6,124.7,433.7,105.6,434.8,89.5,435.9,76.4,436.11,72.3,437.12,69.2,438.13,67.1,439.14,1.0,440.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 22.11/6.02 457:1:16:[356.15,41.0,287.14,442.1,235.13,443.2,198.12,444.3,176.11,445.4,165.10,446.5,155.9,447.6,146.8,448.7,124.7,449.8,105.6,450.9,89.5,451.10,76.4,452.11,72.3,453.12,69.2,454.13,67.1,455.14,1.0,456.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 22.11/6.02 471:4:14:[235.13,42.1,198.12,458.2,176.11,459.3,165.10,460.4,155.9,461.6,146.8,462.7,124.7,463.8,105.6,464.9,89.5,465.10,76.4,466.11,72.3,467.12,69.2,468.13,67.1,469.14,1.0,470.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 22.11/6.02 486:4:15:[287.14,43.0,235.13,472.1,198.12,473.2,176.11,474.4,165.10,475.5,155.9,476.6,146.8,477.7,124.7,478.8,105.6,479.9,89.5,480.10,76.4,481.11,72.3,482.12,69.2,483.13,67.1,484.14,1.0,485.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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 22.11/6.02 501:4:15:[287.14,44.0,235.13,487.2,198.12,488.3,176.11,489.4,165.10,490.5,155.9,491.6,146.8,492.7,124.7,493.8,105.6,494.10,89.5,495.11,76.4,496.12,72.3,497.14,69.2,498.15,67.1,499.16,1.0,500.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 22.11/6.02 516:4:15:[287.14,45.0,235.13,502.2,198.12,503.3,176.11,504.4,165.10,505.5,155.9,506.6,146.8,507.7,124.7,508.8,105.6,509.10,89.5,510.11,76.4,511.13,72.3,512.14,69.2,513.15,67.1,514.16,1.0,515.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 22.11/6.02 531:4:15:[287.14,46.0,235.13,517.3,198.12,518.5,176.11,519.6,165.10,520.7,155.9,521.8,146.8,522.9,124.7,523.10,105.6,524.11,89.5,525.12,76.4,526.13,72.3,527.14,69.2,528.16,67.1,529.17,1.0,530.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv19_2r1r1(x0,x1) ->
% 22.11/6.02 548:1:17:[457.16,47.0,356.15,532.1,287.14,533.2,235.13,534.3,198.12,535.4,176.11,536.5,165.10,537.6,155.9,538.7,146.8,539.8,124.7,540.9,105.6,541.10,89.5,542.11,76.4,543.12,72.3,544.13,69.2,545.14,67.1,546.15,1.0,547.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 22.11/6.02 564:4:16:[356.15,48.0,287.14,549.2,235.13,550.3,198.12,551.4,176.11,552.5,165.10,553.6,155.9,554.7,146.8,555.8,124.7,556.9,105.6,557.10,89.5,558.11,76.4,559.12,72.3,560.13,69.2,561.14,67.1,562.15,1.0,563.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_1r1(x0)
% 22.11/6.02 580:4:16:[356.15,49.0,287.14,565.1,235.13,566.2,198.12,567.3,176.11,568.4,165.10,569.6,155.9,570.7,146.8,571.8,124.7,572.9,105.6,573.10,89.5,574.11,76.4,575.12,72.3,576.13,69.2,577.14,67.1,578.15,1.0,579.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0)
% 22.11/6.02 596:4:16:[356.15,50.0,287.14,581.2,235.13,582.3,198.12,583.4,176.11,584.5,165.10,585.6,155.9,586.7,146.8,587.8,124.7,588.9,105.6,589.10,89.5,590.11,76.4,591.12,72.3,592.14,69.2,593.15,67.1,594.16,1.0,595.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) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 22.11/6.02 614:1:18:[548.17,51.0,457.16,597.1,356.15,598.2,287.14,599.3,235.13,600.4,198.12,601.5,176.11,602.6,165.10,603.7,155.9,604.8,146.8,605.9,124.7,606.10,105.6,607.11,89.5,608.12,76.4,609.13,72.3,610.14,69.2,611.15,67.1,612.16,1.0,613.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 22.11/6.02 631:4:17:[457.16,52.0,356.15,615.2,287.14,616.3,235.13,617.4,198.12,618.5,176.11,619.6,165.10,620.7,155.9,621.8,146.8,622.9,124.7,623.11,105.6,624.13,89.5,625.14,76.4,626.15,72.3,627.16,69.2,628.17,67.1,629.18,1.0,630.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 648:4:17:[457.16,53.0,356.15,632.2,287.14,633.3,235.13,634.4,198.12,635.5,176.11,636.6,165.10,637.7,155.9,638.8,146.8,639.9,124.7,640.10,105.6,641.11,89.5,642.12,76.4,643.13,72.3,644.14,69.2,645.15,67.1,646.16,1.0,647.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_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),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 665:4:17:[457.16,54.0,356.15,649.2,287.14,650.3,235.13,651.4,198.12,652.5,176.11,653.6,165.10,654.7,155.9,655.8,146.8,656.9,124.7,657.10,105.6,658.11,89.5,659.12,76.4,660.13,72.3,661.14,69.2,662.15,67.1,663.16,1.0,664.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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 22.11/6.02 683:4:18:[548.17,55.0,457.16,666.2,356.15,667.3,287.14,668.4,235.13,669.5,198.12,670.6,176.11,671.7,165.10,672.8,155.9,673.9,146.8,674.11,124.7,675.12,105.6,676.13,89.5,677.14,76.4,678.15,72.3,679.16,69.2,680.17,67.1,681.18,1.0,682.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0)
% 22.11/6.02 701:4:18:[548.17,56.0,457.16,684.1,356.15,685.2,287.14,686.3,235.13,687.4,198.12,688.5,176.11,689.6,165.10,690.7,155.9,691.8,146.8,692.9,124.7,693.10,105.6,694.11,89.5,695.13,76.4,696.14,72.3,697.15,69.2,698.16,67.1,699.17,1.0,700.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 720:1:19:[614.18,57.0,548.17,702.1,457.16,703.2,356.15,704.3,287.14,705.4,235.13,706.5,198.12,707.6,176.11,708.7,165.10,709.8,155.9,710.9,146.8,711.10,124.7,712.11,105.6,713.12,89.5,714.13,76.4,715.14,72.3,716.15,69.2,717.16,67.1,718.17,1.0,719.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 22.11/6.02 738:4:18:[548.17,58.0,457.16,721.1,356.15,722.2,287.14,723.3,235.13,724.4,198.12,725.5,176.11,726.6,165.10,727.7,155.9,728.8,146.8,729.9,124.7,730.10,105.6,731.11,89.5,732.12,76.4,733.13,72.3,734.14,69.2,735.15,67.1,736.16,1.0,737.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 756:4:18:[548.17,59.0,457.16,739.1,356.15,740.3,287.14,741.4,235.13,742.5,198.12,743.6,176.11,744.7,165.10,745.8,155.9,746.9,146.8,747.10,124.7,748.11,105.6,749.12,89.5,750.13,76.4,751.14,72.3,752.15,69.2,753.16,67.1,754.17,1.0,755.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 774:4:18:[548.17,60.0,457.16,757.2,356.15,758.3,287.14,759.4,235.13,760.5,198.12,761.6,176.11,762.7,165.10,763.8,155.9,764.9,146.8,765.11,124.7,766.12,105.6,767.14,89.5,768.15,76.4,769.16,72.3,770.17,69.2,771.18,67.1,772.19,1.0,773.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 22.11/6.02 792:4:18:[548.17,61.0,457.16,775.2,356.15,776.4,287.14,777.5,235.13,778.6,198.12,779.7,176.11,780.8,165.10,781.9,155.9,782.11,146.8,783.12,124.7,784.13,105.6,785.14,89.5,786.15,76.4,787.16,72.3,788.17,69.2,789.18,67.1,790.19,1.0,791.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),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 22.11/6.02 810:4:18:[548.17,62.0,457.16,793.2,356.15,794.4,287.14,795.5,235.13,796.6,198.12,797.7,176.11,798.8,165.10,799.9,155.9,800.10,146.8,801.11,124.7,802.12,105.6,803.13,89.5,804.14,76.4,805.15,72.3,806.16,69.2,807.17,67.1,808.18,1.0,809.19]: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) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 22.11/6.02 829:4:19:[614.18,63.0,548.17,811.2,457.16,812.3,356.15,813.4,287.14,814.5,235.13,815.6,198.12,816.7,176.11,817.8,165.10,818.9,155.9,819.10,146.8,820.11,124.7,821.12,105.6,822.13,89.5,823.14,76.4,824.15,72.3,825.16,69.2,826.17,67.1,827.18,1.0,828.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_1r1(x0)
% 22.11/6.02 849:4:20:[720.19,64.0,614.18,830.1,548.17,831.2,457.16,832.3,356.15,833.5,287.14,834.6,235.13,835.8,198.12,836.10,176.11,837.11,165.10,838.12,155.9,839.13,146.8,840.14,124.7,841.15,105.6,842.16,89.5,843.17,76.4,844.18,72.3,845.19,69.2,846.20,67.1,847.21,1.0,848.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 22.11/6.02 869:4:20:[720.19,65.0,614.18,850.1,548.17,851.2,457.16,852.4,356.15,853.5,287.14,854.6,235.13,855.8,198.12,856.9,176.11,857.10,165.10,858.11,155.9,859.12,146.8,860.13,124.7,861.14,105.6,862.15,89.5,863.16,76.4,864.17,72.3,865.18,69.2,866.19,67.1,867.20,1.0,868.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> 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)
% 22.11/6.02 889:4:20:[720.19,66.0,614.18,870.1,548.17,871.3,457.16,872.5,356.15,873.7,287.14,874.8,235.13,875.9,198.12,876.10,176.11,877.11,165.10,878.12,155.9,879.13,146.8,880.14,124.7,881.15,105.6,882.16,89.5,883.17,76.4,884.18,72.3,885.19,69.2,886.20,67.1,887.21,1.0,888.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_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),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 22.11/6.02
% 22.11/6.02 Most General Atoms: ssNder1_0 ssNder1_1r1(x0) ssNder1_2r1r1(x0,x1) ssNder1_3r1r1r1(x0,x1,x2) ssNder1_4r1r1r1r1(x0,x1,x2,x3) ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv20_1r1(x0) ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) 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) ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssPv18_3r1r1r1(x0,x1,x2) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv17_4r1r1r1r1(x0,x1,x2,x3) ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) 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) ssPv19_2r1r1(x0,x1) 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) ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) 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)
% 22.11/6.02
% 22.11/6.02 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: resolution_2 ===
% 22.11/6.02
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 56
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 701:4:18:[548.17,56.0,457.16,684.1,356.15,685.2,287.14,686.3,235.13,687.4,198.12,688.5,176.11,689.6,165.10,690.7,155.9,691.8,146.8,692.9,124.7,693.10,105.6,694.11,89.5,695.13,76.4,696.14,72.3,697.15,69.2,698.16,67.1,699.17,1.0,700.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),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}
% 22.11/6.02 === Backtracking. Learning clause 890:3:17:[701.1,80.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 === Conflict found: 273:4:12:[176.11,28.0,165.10,262.2,155.9,263.3,146.8,264.4,124.7,265.5,105.6,266.6,89.5,267.8,76.4,268.9,72.3,269.10,69.2,270.11,67.1,271.12,1.0,272.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,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 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 891:3:11:[273.2,80.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 60
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 683:4:18:[548.17,55.0,457.16,666.2,356.15,667.3,287.14,668.4,235.13,669.5,198.12,670.6,176.11,671.7,165.10,672.8,155.9,673.9,146.8,674.11,124.7,675.12,105.6,676.13,89.5,677.14,76.4,678.15,72.3,679.16,69.2,680.17,67.1,681.18,1.0,682.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) {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}
% 22.11/6.02 === Backtracking. Learning clause 892:3:17:[683.3,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6) -> ssPv20_1r1(x0)
% 22.11/6.02 === Conflict found: 486:4:15:[287.14,43.0,235.13,472.1,198.12,473.2,176.11,474.4,165.10,475.5,155.9,476.6,146.8,477.7,124.7,478.8,105.6,479.9,89.5,480.10,76.4,481.11,72.3,482.12,69.2,483.13,67.1,484.14,1.0,485.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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 893:3:14:[486.3,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv19_2r1r1(x0,x1)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 69
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 501:4:15:[287.14,44.0,235.13,487.2,198.12,488.3,176.11,489.4,165.10,490.5,155.9,491.6,146.8,492.7,124.7,493.8,105.6,494.10,89.5,495.11,76.4,496.12,72.3,497.14,69.2,498.15,67.1,499.16,1.0,500.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 894:3:14:[501.2,94.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8)
% 22.11/6.02 === Conflict found: 341:4:13:[198.12,33.0,176.11,329.2,165.10,330.3,155.9,331.4,146.8,332.5,124.7,333.6,105.6,334.8,89.5,335.9,76.4,336.10,72.3,337.12,69.2,338.13,67.1,339.14,1.0,340.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> 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 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 895:3:12:[341.2,94.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 78
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 648:4:17:[457.16,53.0,356.15,632.2,287.14,633.3,235.13,634.4,198.12,635.5,176.11,636.6,165.10,637.7,155.9,638.8,146.8,639.9,124.7,640.10,105.6,641.11,89.5,642.12,76.4,643.13,72.3,644.14,69.2,645.15,67.1,646.16,1.0,647.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_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),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 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 896:3:16:[648.3,99.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 === Conflict found: 273:4:12:[176.11,28.0,165.10,262.2,155.9,263.3,146.8,264.4,124.7,265.5,105.6,266.6,89.5,267.8,76.4,268.9,72.3,269.10,69.2,270.11,67.1,271.12,1.0,272.13]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,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 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 897:2:10:[273.4,99.1,80.1]:TopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 142
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 145
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 631:4:17:[457.16,52.0,356.15,615.2,287.14,616.3,235.13,617.4,198.12,618.5,176.11,619.6,165.10,620.7,155.9,621.8,146.8,622.9,124.7,623.11,105.6,624.13,89.5,625.14,76.4,626.15,72.3,627.16,69.2,628.17,67.1,629.18,1.0,630.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 898:3:16:[631.2,111.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 === Conflict found: 328:4:13:[198.12,32.0,176.11,316.1,165.10,317.2,155.9,318.3,146.8,319.4,124.7,320.6,105.6,321.7,89.5,322.8,76.4,323.9,72.3,324.10,69.2,325.11,67.1,326.12,1.0,327.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> 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),ssPv18_3r1r1r1(x0,x1,x2) {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}
% 22.11/6.02 === Backtracking. Learning clause 899:3:12:[328.1,111.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7),ssPv18_3r1r1r1(x0,x1,x2)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 152
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 829:4:19:[614.18,63.0,548.17,811.2,457.16,812.3,356.15,813.4,287.14,814.5,235.13,815.6,198.12,816.7,176.11,817.8,165.10,818.9,155.9,819.10,146.8,820.11,124.7,821.12,105.6,822.13,89.5,823.14,76.4,824.15,72.3,825.16,69.2,826.17,67.1,827.18,1.0,828.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),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 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 900:3:18:[829.3,117.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6),ssPv20_1r1(x0)
% 22.11/6.02 === Conflict found: 564:4:16:[356.15,48.0,287.14,549.2,235.13,550.3,198.12,551.4,176.11,552.5,165.10,553.6,155.9,554.7,146.8,555.8,124.7,556.9,105.6,557.10,89.5,558.11,76.4,559.12,72.3,560.13,69.2,561.14,67.1,562.15,1.0,563.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),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 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 901:3:15:[564.3,117.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9),ssPv20_1r1(x0)
% 22.11/6.02 === Conflict found: 186:4:10:[155.9,21.0,146.8,177.1,124.7,178.2,105.6,179.3,89.5,180.4,76.4,181.5,72.3,182.6,69.2,183.7,67.1,184.8,1.0,185.9]:TopTopTopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),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}
% 22.11/6.02 === Backtracking. Learning clause 902:3:9:[186.2,117.1]:TopTopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 158
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 413:4:14:[235.13,38.0,198.12,400.1,176.11,401.2,165.10,402.3,155.9,403.4,146.8,404.6,124.7,405.7,105.6,406.8,89.5,407.9,76.4,408.11,72.3,409.12,69.2,410.13,67.1,411.14,1.0,412.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 903:3:13:[413.1,131.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7)
% 22.11/6.02 === Conflict found: 892:3:17:[683.3,84.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc24, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 904:2:16:[892.2,131.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv20_1r1(x0)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 164
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 580:4:16:[356.15,49.0,287.14,565.1,235.13,566.2,198.12,567.3,176.11,568.4,165.10,569.6,155.9,570.7,146.8,571.8,124.7,572.9,105.6,573.10,89.5,574.11,76.4,575.12,72.3,576.13,69.2,577.14,67.1,578.15,1.0,579.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 905:3:15:[580.3,138.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11,x12,x13,x14),ssPv20_1r1(x0)
% 22.11/6.02 === Conflict found: 900:3:18:[829.3,117.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6),ssPv20_1r1(x0) {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, x16 -> skc30, x17 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 906:2:17:[900.2,138.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,skc25,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv20_1r1(x0)
% 22.11/6.02 === Conflict found: 890:3:17:[701.1,80.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc27, x6 -> skc25, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 907:2:16:[890.2,138.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,skc25,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 228
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 234
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 369:4:13:[198.12,35.1,176.11,357.3,165.10,358.4,155.9,359.5,146.8,360.6,124.7,361.7,105.6,362.9,89.5,363.10,76.4,364.11,72.3,365.12,69.2,366.13,67.1,367.14,1.0,368.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> 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 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 22.11/6.02 === Backtracking. Learning clause 908:3:12:[369.2,210.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 22.11/6.02 === Conflict found: 341:4:13:[198.12,33.0,176.11,329.2,165.10,330.3,155.9,331.4,146.8,332.5,124.7,333.6,105.6,334.8,89.5,335.9,76.4,336.10,72.3,337.12,69.2,338.13,67.1,339.14,1.0,340.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> 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 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 22.11/6.02 === Backtracking. Learning clause 909:2:8:[341.1,210.1,94.1]:TopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 237
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 328:4:13:[198.12,32.0,176.11,316.1,165.10,317.2,155.9,318.3,146.8,319.4,124.7,320.6,105.6,321.7,89.5,322.8,76.4,323.9,72.3,324.10,69.2,325.11,67.1,326.12,1.0,327.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> 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),ssPv18_3r1r1r1(x0,x1,x2) {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 -> skc23}
% 22.11/6.02 === Backtracking. Learning clause 910:2:8:[328.2,222.1,111.1]:TopTopTopTopTopTopTopTop: -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7),ssPv18_3r1r1r1(x0,x1,x2)
% 22.11/6.02 === Conflict found: 427:4:14:[235.13,39.1,198.12,414.3,176.11,415.4,165.10,416.6,155.9,417.7,146.8,418.8,124.7,419.9,105.6,420.10,89.5,421.11,76.4,422.12,72.3,423.13,69.2,424.14,67.1,425.16,1.0,426.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),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 -> skc28, x13 -> skc20}
% 22.11/6.02 === Backtracking. Learning clause 911:7:18:[427.3,501.4,441.3,516.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv20_1r1(x0),ssPv18_3r1r1r1(x0,x1,x2),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x14,x15,x16),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x17)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 237
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 911:7:18:[427.3,501.4,441.3,516.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv20_1r1(x0),ssPv18_3r1r1r1(x0,x1,x2),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x14,x15,x16),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x17) {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, x17 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 913:6:16:[501.3,912.5,911.1,248.1,427.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),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),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x15),ssPv20_1r1(x0) ->
% 22.11/6.02 === Conflict found: 427:4:14:[235.13,39.1,198.12,414.3,176.11,415.4,165.10,416.6,155.9,417.7,146.8,418.8,124.7,419.9,105.6,420.10,89.5,421.11,76.4,422.12,72.3,423.13,69.2,424.14,67.1,425.16,1.0,426.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),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}
% 22.11/6.02 === Backtracking. Learning clause 914:3:13:[427.2,248.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv20_1r1(x0) ->
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 244
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 903:3:13:[413.1,131.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc21}
% 22.11/6.02 === Backtracking. Learning clause 915:2:8:[903.2,261.1]:TopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 308
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 314
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 913:6:16:[501.3,912.5,911.1,248.1,427.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),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),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x15),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 -> skc18, x15 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 916:7:28:[913.2,301.1,564.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),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),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv14_7r1r1r1r1r1r1r1(x0,x13,x14,x15,x16,x17,x18)
% 22.11/6.02 === Conflict found: 516:4:15:[287.14,45.0,235.13,502.2,198.12,503.3,176.11,504.4,165.10,505.5,155.9,506.6,146.8,507.7,124.7,508.8,105.6,509.10,89.5,510.11,76.4,511.13,72.3,512.14,69.2,513.15,67.1,514.16,1.0,515.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 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 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18}
% 22.11/6.02 === Backtracking. Learning clause 917:3:12:[516.1,301.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 22.11/6.02 === Conflict found: 501:4:15:[287.14,44.0,235.13,487.2,198.12,488.3,176.11,489.4,165.10,490.5,155.9,491.6,146.8,492.7,124.7,493.8,105.6,494.10,89.5,495.11,76.4,496.12,72.3,497.14,69.2,498.15,67.1,499.16,1.0,500.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18}
% 22.11/6.02 === Backtracking. Learning clause 918:2:9:[501.1,301.1,94.1]:TopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8)
% 22.11/6.02 === Conflict found: 914:3:13:[427.2,248.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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 -> skc22}
% 22.11/6.02 === Backtracking. Learning clause 919:2:3:[914.1,210.1,918.2]:TopTopTop: ssPv20_1r1(x0),ssPv18_3r1r1r1(x0,x1,x2) ->
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 315
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 486:4:15:[287.14,43.0,235.13,472.1,198.12,473.2,176.11,474.4,165.10,475.5,155.9,476.6,146.8,477.7,124.7,478.8,105.6,479.9,89.5,480.10,76.4,481.11,72.3,482.12,69.2,483.13,67.1,484.14,1.0,485.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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 22.11/6.02 === Backtracking. Learning clause 920:2:10:[486.2,315.1,84.1]:TopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9) -> ssPv19_2r1r1(x0,x1)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 320
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 596:4:16:[356.15,50.0,287.14,581.2,235.13,582.3,198.12,583.4,176.11,584.5,165.10,585.6,155.9,586.7,146.8,587.8,124.7,588.9,105.6,589.10,89.5,590.11,76.4,591.12,72.3,592.14,69.2,593.15,67.1,594.16,1.0,595.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) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc16}
% 22.11/6.02 === Backtracking. Learning clause 921:3:11:[596.1,384.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 22.11/6.02 === Conflict found: 564:4:16:[356.15,48.0,287.14,549.2,235.13,550.3,198.12,551.4,176.11,552.5,165.10,553.6,155.9,554.7,146.8,555.8,124.7,556.9,105.6,557.10,89.5,558.11,76.4,559.12,72.3,560.13,69.2,561.14,67.1,562.15,1.0,563.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),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 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc16}
% 22.11/6.02 === Backtracking. Learning clause 922:2:10:[564.1,384.1,117.1]:TopTopTopTopTopTopTopTopTopTop: -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9),ssPv20_1r1(x0)
% 22.11/6.02 === Conflict found: 441:4:14:[235.13,40.0,198.12,428.2,176.11,429.3,165.10,430.4,155.9,431.5,146.8,432.6,124.7,433.7,105.6,434.8,89.5,435.9,76.4,436.11,72.3,437.12,69.2,438.13,67.1,439.14,1.0,440.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc21}
% 22.11/6.02 === Backtracking. Learning clause 923:5:16:[441.3,531.2,516.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x15)
% 22.11/6.02 === Conflict found: 889:4:20:[720.19,66.0,614.18,870.1,548.17,871.3,457.16,872.5,356.15,873.7,287.14,874.8,235.13,875.9,198.12,876.10,176.11,877.11,165.10,878.12,155.9,879.13,146.8,880.14,124.7,881.15,105.6,882.16,89.5,883.17,76.4,884.18,72.3,885.19,69.2,886.20,67.1,887.21,1.0,888.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_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),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> 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 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 924:5:20:[889.1,665.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 324
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 580:4:16:[356.15,49.0,287.14,565.1,235.13,566.2,198.12,567.3,176.11,568.4,165.10,569.6,155.9,570.7,146.8,571.8,124.7,572.9,105.6,573.10,89.5,574.11,76.4,575.12,72.3,576.13,69.2,577.14,67.1,578.15,1.0,579.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc17}
% 22.11/6.02 === Backtracking. Learning clause 925:2:9:[580.2,399.1,138.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8) -> ssPv20_1r1(x0)
% 22.11/6.02 === Conflict found: 896:3:16:[648.3,99.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {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 -> skc17, x15 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 926:2:15:[896.2,399.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc17,x14) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 388
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 391
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 849:4:20:[720.19,64.0,614.18,830.1,548.17,831.2,457.16,832.3,356.15,833.5,287.14,834.6,235.13,835.8,198.12,836.10,176.11,837.11,165.10,838.12,155.9,839.13,146.8,840.14,124.7,841.15,105.6,842.16,89.5,843.17,76.4,844.18,72.3,845.19,69.2,846.20,67.1,847.21,1.0,848.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) -> 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 -> skc29, 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}
% 22.11/6.02 === Backtracking. Learning clause 927:4:18:[849.3,897.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 22.11/6.02 === Conflict found: 902:3:9:[186.2,117.1]:TopTopTopTopTopTopTopTopTop: -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc25, x7 -> skc30, x8 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 928:2:6:[902.1,925.1]:TopTopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 392
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 756:4:18:[548.17,59.0,457.16,739.1,356.15,740.3,287.14,741.4,235.13,742.5,198.12,743.6,176.11,744.7,165.10,745.8,155.9,746.9,146.8,747.10,124.7,748.11,105.6,749.12,89.5,750.13,76.4,751.14,72.3,752.15,69.2,753.16,67.1,754.17,1.0,755.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),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 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 930:3:13:[84.0,929.1,756.2,904.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv20_1r1(x0)
% 22.11/6.02 === Conflict found: 928:2:6:[902.1,925.1]:TopTopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29}
% 22.11/6.02 === Backtracking. Learning clause 931:1:1:[928.1,99.1]:Top: -> ssPv20_1r1(x0)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 392
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 913:6:16:[501.3,912.5,911.1,248.1,427.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),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),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x15),ssPv20_1r1(x0) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 932:5:16:[913.6,931.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),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),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x15) ->
% 22.11/6.02 === Conflict found: 427:4:14:[235.13,39.1,198.12,414.3,176.11,415.4,165.10,416.6,155.9,417.7,146.8,418.8,124.7,419.9,105.6,420.10,89.5,421.11,76.4,422.12,72.3,423.13,69.2,424.14,67.1,425.16,1.0,426.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),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}
% 22.11/6.02 === Backtracking. Learning clause 933:3:14:[427.4,931.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ->
% 22.11/6.02 === Conflict found: 914:3:13:[427.2,248.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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}
% 22.11/6.02 === Backtracking. Learning clause 934:2:13:[914.3,931.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: 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) ->
% 22.11/6.02 === Conflict found: 919:2:3:[914.1,210.1,918.2]:TopTopTop: ssPv20_1r1(x0),ssPv18_3r1r1r1(x0,x1,x2) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 935:1:3:[919.1,931.1]:TopTopTop: ssPv18_3r1r1r1(x0,x1,x2) ->
% 22.11/6.02 === Conflict found: 441:4:14:[235.13,40.0,198.12,428.2,176.11,429.3,165.10,430.4,155.9,431.5,146.8,432.6,124.7,433.7,105.6,434.8,89.5,435.9,76.4,436.11,72.3,437.12,69.2,438.13,67.1,439.14,1.0,440.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc28, x13 -> skc21}
% 22.11/6.02 === Backtracking. Learning clause 936:3:12:[441.4,261.1,934.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ->
% 22.11/6.02 === Conflict found: 917:3:12:[516.1,301.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 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}
% 22.11/6.02 === Backtracking. Learning clause 937:2:9:[917.1,891.3,936.1]:TopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8) ->
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 392
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 328:4:13:[198.12,32.0,176.11,316.1,165.10,317.2,155.9,318.3,146.8,319.4,124.7,320.6,105.6,321.7,89.5,322.8,76.4,323.9,72.3,324.10,69.2,325.11,67.1,326.12,1.0,327.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> 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),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 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 938:3:13:[328.4,935.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> 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)
% 22.11/6.02 === Conflict found: 899:3:12:[328.1,111.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7),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}
% 22.11/6.02 === Backtracking. Learning clause 939:2:12:[899.3,935.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7)
% 22.11/6.02 === Conflict found: 910:2:8:[328.2,222.1,111.1]:TopTopTopTopTopTopTopTop: -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 940:1:8:[910.2,935.1]:TopTopTopTopTopTopTopTop: -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 456
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 460
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 792:4:18:[548.17,61.0,457.16,775.2,356.15,776.4,287.14,777.5,235.13,778.6,198.12,779.7,176.11,780.8,165.10,781.9,155.9,782.11,146.8,783.12,124.7,784.13,105.6,785.14,89.5,786.15,76.4,787.16,72.3,788.17,69.2,789.18,67.1,790.19,1.0,791.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),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {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}
% 22.11/6.02 === Backtracking. Learning clause 941:3:17:[792.3,940.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 22.11/6.02 === Conflict found: 471:4:14:[235.13,42.1,198.12,458.2,176.11,459.3,165.10,460.4,155.9,461.6,146.8,462.7,124.7,463.8,105.6,464.9,89.5,465.10,76.4,466.11,72.3,467.12,69.2,468.13,67.1,469.14,1.0,470.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) {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}
% 22.11/6.02 === Backtracking. Learning clause 942:3:13:[471.2,940.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 462
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 934:2:13:[914.3,931.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: 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 -> skc31, x12 -> skc22}
% 22.11/6.02 === Backtracking. Learning clause 943:1:10:[934.1,210.1]:TopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ->
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 464
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 469
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 792:4:18:[548.17,61.0,457.16,775.2,356.15,776.4,287.14,777.5,235.13,778.6,198.12,779.7,176.11,780.8,165.10,781.9,155.9,782.11,146.8,783.12,124.7,784.13,105.6,785.14,89.5,786.15,76.4,787.16,72.3,788.17,69.2,789.18,67.1,790.19,1.0,791.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),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc26, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 22.11/6.02 === Backtracking. Learning clause 944:3:12:[792.1,907.1,940.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc26,skc25,x5,x6,x7,x8,x9,x10,x11) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 533
% 22.11/6.02 === Clause set with instances from active satisfied. Growing active. New size: 533
% 22.11/6.02 === Restarting.
% 22.11/6.02 === Conflict found: 792:4:18:[548.17,61.0,457.16,775.2,356.15,776.4,287.14,777.5,235.13,778.6,198.12,779.7,176.11,780.8,165.10,781.9,155.9,782.11,146.8,783.12,124.7,784.13,105.6,785.14,89.5,786.15,76.4,787.16,72.3,788.17,69.2,789.18,67.1,790.19,1.0,791.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),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> 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 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc27}
% 22.11/6.02 === Backtracking. Learning clause 945:6:30:[792.4,774.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x18,x19) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x18,x19,x20,x21,x22,x23)
% 22.11/6.03 === Conflict found: 915:2:8:[903.2,261.1]:TopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 946:3:20:[915.1,896.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x16,x17,x18,skc24,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 22.11/6.03 === Conflict found: 516:4:15:[287.14,45.0,235.13,502.2,198.12,503.3,176.11,504.4,165.10,505.5,155.9,506.6,146.8,507.7,124.7,508.8,105.6,509.10,89.5,510.11,76.4,511.13,72.3,512.14,69.2,513.15,67.1,514.16,1.0,515.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 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 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 947:6:28:[516.4,369.1,896.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x16,skc29,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x16,skc29,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26)
% 22.11/6.03 === Conflict found: 516:4:15:[287.14,45.0,235.13,502.2,198.12,503.3,176.11,504.4,165.10,505.5,155.9,506.6,146.8,507.7,124.7,508.8,105.6,509.10,89.5,510.11,76.4,511.13,72.3,512.14,69.2,513.15,67.1,514.16,1.0,515.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 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 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 948:5:16:[516.4,369.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 533
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 774:4:18:[548.17,60.0,457.16,757.2,356.15,758.3,287.14,759.4,235.13,760.5,198.12,761.6,176.11,762.7,165.10,763.8,155.9,764.9,146.8,765.11,124.7,766.12,105.6,767.14,89.5,768.15,76.4,769.16,72.3,770.17,69.2,771.18,67.1,772.19,1.0,773.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> 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}
% 22.11/6.03 === Backtracking. Learning clause 949:5:29:[774.3,941.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x18,x19,x20,x21,x22,x23,x24,x25) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 534
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 471:4:14:[235.13,42.1,198.12,458.2,176.11,459.3,165.10,460.4,155.9,461.6,146.8,462.7,124.7,463.8,105.6,464.9,89.5,465.10,76.4,466.11,72.3,467.12,69.2,468.13,67.1,469.14,1.0,470.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) {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}
% 22.11/6.03 === Backtracking. Learning clause 950:4:13:[471.2,915.2]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9)
% 22.11/6.03 === Conflict found: 945:6:30:[792.4,774.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x18,x19) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x18,x19,x20,x21,x22,x23) {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, x21 -> skc30, x22 -> skc30, x23 -> skc30, x24 -> skc30, x25 -> skc30, x26 -> skc30, x27 -> skc30, x28 -> skc30, x29 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 951:6:29:[945.3,915.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18,x19,x20,x21,x22)
% 22.11/6.03 === Conflict found: 792:4:18:[548.17,61.0,457.16,775.2,356.15,776.4,287.14,777.5,235.13,778.6,198.12,779.7,176.11,780.8,165.10,781.9,155.9,782.11,146.8,783.12,124.7,784.13,105.6,785.14,89.5,786.15,76.4,787.16,72.3,788.17,69.2,789.18,67.1,790.19,1.0,791.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),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {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}
% 22.11/6.03 === Backtracking. Learning clause 952:4:17:[792.3,915.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 534
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 648:4:17:[457.16,53.0,356.15,632.2,287.14,633.3,235.13,634.4,198.12,635.5,176.11,636.6,165.10,637.7,155.9,638.8,146.8,639.9,124.7,640.10,105.6,641.11,89.5,642.12,76.4,643.13,72.3,644.14,69.2,645.15,67.1,646.16,1.0,647.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_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),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}
% 22.11/6.03 === Backtracking. Learning clause 953:7:32:[648.2,889.2,774.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x29,x30,x31),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18,x19,x20,x21,x22)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 598
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 609
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 924:5:20:[889.1,665.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc27, 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}
% 22.11/6.03 === Backtracking. Learning clause 954:5:19:[924.4,920.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4),ssPv19_2r1r1(x0,x1)
% 22.11/6.03 === Conflict found: 665:4:17:[457.16,54.0,356.15,649.2,287.14,650.3,235.13,651.4,198.12,652.5,176.11,653.6,165.10,654.7,155.9,655.8,146.8,656.9,124.7,657.10,105.6,658.11,89.5,659.12,76.4,660.13,72.3,661.14,69.2,662.15,67.1,663.16,1.0,664.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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 955:4:16:[665.3,920.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4),ssPv19_2r1r1(x0,x1)
% 22.11/6.03 === Conflict found: 471:4:14:[235.13,42.1,198.12,458.2,176.11,459.3,165.10,460.4,155.9,461.6,146.8,462.7,124.7,463.8,105.6,464.9,89.5,465.10,76.4,466.11,72.3,467.12,69.2,468.13,67.1,469.14,1.0,470.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 956:4:13:[471.4,920.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1)
% 22.11/6.03 === Conflict found: 441:4:14:[235.13,40.0,198.12,428.2,176.11,429.3,165.10,430.4,155.9,431.5,146.8,432.6,124.7,433.7,105.6,434.8,89.5,435.9,76.4,436.11,72.3,437.12,69.2,438.13,67.1,439.14,1.0,440.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),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 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc21}
% 22.11/6.03 === Backtracking. Learning clause 957:2:6:[441.3,222.1,261.1,917.3]:TopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 611
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 774:4:18:[548.17,60.0,457.16,757.2,356.15,758.3,287.14,759.4,235.13,760.5,198.12,761.6,176.11,762.7,165.10,763.8,155.9,764.9,146.8,765.11,124.7,766.12,105.6,767.14,89.5,768.15,76.4,769.16,72.3,770.17,69.2,771.18,67.1,772.19,1.0,773.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> 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 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 958:4:18:[774.4,908.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 614
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 665:4:17:[457.16,54.0,356.15,649.2,287.14,650.3,235.13,651.4,198.12,652.5,176.11,653.6,165.10,654.7,155.9,655.8,146.8,656.9,124.7,657.10,105.6,658.11,89.5,659.12,76.4,660.13,72.3,661.14,69.2,662.15,67.1,663.16,1.0,664.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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc17, x16 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 960:3:13:[99.0,959.1,665.2,926.1,920.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv19_2r1r1(x0,x1)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 614
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 957:2:6:[441.3,222.1,261.1,917.3]:TopTopTopTopTopTop: 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 -> skc28}
% 22.11/6.03 === Backtracking. Learning clause 961:1:4:[957.1,94.1]:TopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) ->
% 22.11/6.03 === Conflict found: 756:4:18:[548.17,59.0,457.16,739.1,356.15,740.3,287.14,741.4,235.13,742.5,198.12,743.6,176.11,744.7,165.10,745.8,155.9,746.9,146.8,747.10,124.7,748.11,105.6,749.12,89.5,750.13,76.4,751.14,72.3,752.15,69.2,753.16,67.1,754.17,1.0,755.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),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 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 963:4:15:[961.0,962.2,756.2,810.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 678
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 680
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 896:3:16:[648.3,99.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),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}
% 22.11/6.03 === Backtracking. Learning clause 964:2:16:[896.3,961.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 22.11/6.03 === Conflict found: 926:2:15:[896.2,399.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc17,x14) -> 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}
% 22.11/6.03 === Backtracking. Learning clause 965:1:15:[926.2,961.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc17,x14) ->
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 680
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 955:4:16:[665.3,920.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4),ssPv19_2r1r1(x0,x1) {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 -> skc17, x15 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 967:2:13:[99.0,966.1,955.2,965.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv19_2r1r1(x0,x1)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 691
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 810:4:18:[548.17,62.0,457.16,793.2,356.15,794.4,287.14,795.5,235.13,796.6,198.12,797.7,176.11,798.8,165.10,799.9,155.9,800.10,146.8,801.11,124.7,802.12,105.6,803.13,89.5,804.14,76.4,805.15,72.3,806.16,69.2,807.17,67.1,808.18,1.0,809.19]: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) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, 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}
% 22.11/6.03 === Backtracking. Learning clause 968:4:17:[810.3,920.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5),ssPv19_2r1r1(x0,x1)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 693
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 665:4:17:[457.16,54.0,356.15,649.2,287.14,650.3,235.13,651.4,198.12,652.5,176.11,653.6,165.10,654.7,155.9,655.8,146.8,656.9,124.7,657.10,105.6,658.11,89.5,659.12,76.4,660.13,72.3,661.14,69.2,662.15,67.1,663.16,1.0,664.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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 970:3:15:[99.0,969.2,665.2,964.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 757
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 758
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 967:2:13:[99.0,966.1,955.2,965.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc18}
% 22.11/6.03 === Backtracking. Learning clause 971:1:2:[967.1,301.1]:TopTop: -> ssPv19_2r1r1(x0,x1)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 758
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 531:4:15:[287.14,46.0,235.13,517.3,198.12,518.5,176.11,519.6,165.10,520.7,155.9,521.8,146.8,522.9,124.7,523.10,105.6,524.11,89.5,525.12,76.4,526.13,72.3,527.14,69.2,528.16,67.1,529.17,1.0,530.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 972:3:15:[531.4,971.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ->
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 763
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 701:4:18:[548.17,56.0,457.16,684.1,356.15,685.2,287.14,686.3,235.13,687.4,198.12,688.5,176.11,689.6,165.10,690.7,155.9,691.8,146.8,692.9,124.7,693.10,105.6,694.11,89.5,695.13,76.4,696.14,72.3,697.15,69.2,698.16,67.1,699.17,1.0,700.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {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}
% 22.11/6.03 === Backtracking. Learning clause 974:7:27:[961.0,973.6,701.2,945.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x15,x16) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x15,x16,x17,x18,x19,x20)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 763
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 827
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 827
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 972:3:15:[531.4,971.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),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 -> skc26, x14 -> skc18}
% 22.11/6.03 === Backtracking. Learning clause 975:2:13:[972.1,301.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) ->
% 22.11/6.03 === Conflict found: 975:2:13:[972.1,301.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) -> {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}
% 22.11/6.03 === Backtracking. Learning clause 976:1:12:[975.1,210.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ->
% 22.11/6.03 === Conflict found: 810:4:18:[548.17,62.0,457.16,793.2,356.15,794.4,287.14,795.5,235.13,796.6,198.12,797.7,176.11,798.8,165.10,799.9,155.9,800.10,146.8,801.11,124.7,802.12,105.6,803.13,89.5,804.14,76.4,805.15,72.3,806.16,69.2,807.17,67.1,808.18,1.0,809.19]: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) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 978:3:14:[961.0,977.3,810.4,117.1,756.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 831
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 953:7:32:[648.2,889.2,774.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x29,x30,x31),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18,x19,x20,x21,x22) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30, x20 -> skc30, x21 -> skc30, x22 -> skc30, x23 -> skc30, x24 -> skc30, x25 -> skc30, x26 -> skc30, x27 -> skc30, x28 -> skc30, x29 -> skc30, x30 -> skc30, x31 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 980:5:32:[961.0,979.4,953.7,976.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27,x28),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x17,x18) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x29,x30,x31)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 842
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 774:4:18:[548.17,60.0,457.16,757.2,356.15,758.3,287.14,759.4,235.13,760.5,198.12,761.6,176.11,762.7,165.10,763.8,155.9,764.9,146.8,765.11,124.7,766.12,105.6,767.14,89.5,768.15,76.4,769.16,72.3,770.17,69.2,771.18,67.1,772.19,1.0,773.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 981:3:18:[774.4,976.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ->
% 22.11/6.03 === Conflict found: 981:3:18:[774.4,976.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, 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}
% 22.11/6.03 === Backtracking. Learning clause 982:1:16:[981.2,131.1,94.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,skc24,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ->
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 845
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 898:3:16:[631.2,111.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc24, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc19, x14 -> skc30, x15 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 984:1:15:[961.0,983.1,898.2,94.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc26,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ->
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 909
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 912
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 701:4:18:[548.17,56.0,457.16,684.1,356.15,685.2,287.14,686.3,235.13,687.4,198.12,688.5,176.11,689.6,165.10,690.7,155.9,691.8,146.8,692.9,124.7,693.10,105.6,694.11,89.5,695.13,76.4,696.14,72.3,697.15,69.2,698.16,67.1,699.17,1.0,700.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 985:3:18:[701.4,961.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 912
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 907:2:16:[890.2,138.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,skc25,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc26, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 22.11/6.03 === Backtracking. Learning clause 986:1:16:[907.2,961.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,skc25,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 912
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 944:3:12:[792.1,907.1,940.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc26,skc25,x5,x6,x7,x8,x9,x10,x11) -> 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}
% 22.11/6.03 === Backtracking. Learning clause 987:2:12:[944.3,961.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc26,skc25,x5,x6,x7,x8,x9,x10,x11) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4)
% 22.11/6.03 === Clause set with instances from active satisfied. Growing active. New size: 913
% 22.11/6.03 === Restarting.
% 22.11/6.03 === Conflict found: 987:2:12:[944.3,961.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc26,skc25,x5,x6,x7,x8,x9,x10,x11) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc18}
% 22.11/6.03 === Backtracking. Learning clause 988:1:5:[987.1,301.1]:TopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4)
% 22.11/6.03 === Conflict found: 988:1:5:[987.1,301.1]:TopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc29}
% 22.11/6.03
% 22.11/6.03 SZS status Unsatisfiable
% 22.11/6.03
% 22.11/6.03 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.11/6.03
% 22.11/6.03 SPASS-SCL-FOL Statistics:
% 22.11/6.03 Number of learned clauses: 89
% 22.11/6.03 Number of propagations: 20776
% 22.11/6.03 Number of decisions: 8527
% 22.11/6.03 Number of resolutions: 113
% 22.11/6.03 Number of condensations: 3
% 22.11/6.03 Number of sub resolutions: 833
% 22.11/6.03 Number of input literals (deduplicated): 56
% 22.11/6.03 Number of grows: 59
% 22.11/6.03 Number of considered ground atoms: 913
% 22.11/6.03
% 22.11/6.03 Needed: 0:00:05.43
% 22.11/6.03
%------------------------------------------------------------------------------