%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN894-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 : n011.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:22 PM UTC 2026
% Result : Unsatisfiable 0.41s 0.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SYN894-1 : TPTP v9.2.1. Released v2.5.0.
% 0.09/0.15 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.37 % Computer : n011.cluster.edu
% 0.17/0.37 % Model : x86_64 x86_64
% 0.17/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.37 % Memory : 8042.1875MB
% 0.17/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.37 % CPULimit : 300
% 0.17/0.37 % WCLimit : 300
% 0.17/0.37 % DateTime : Thu May 7 13:50:03 EDT 2026
% 0.17/0.37 % CPUTime :
% 0.17/0.37 SPASS-SCL-FOL version:
% 0.28/0.47 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.41/0.79 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.41/0.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.41/0.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.41/0.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.41/0.79 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.41/0.79 Execution resolution_3 ended with status: unsatisfiable
% 0.41/0.79 Used heuristic: resolution_3
% 0.41/0.79
% 0.41/0.79 Input Clauses:
% 0.41/0.79
% 0.41/0.79 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv24_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv23_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv22_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv21_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv27_2r1r1 ssPv26_3r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv25_4r1r1r1r1 ssPv20_9r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv19_10r1r1r1r1r1r1r1r1r1r1 ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv18_11r1r1r1r1r1r1r1r1r1r1r1 ssPv28_1r1 ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 0.41/0.79 Fol Constants: skc46 skc47 skc44 skc45 skc42 skc43 skc40 skc41 skc38 skc39 skc36 skc37 skc34 skc35 skc32 skc33 skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25
% 0.41/0.79 Fol Functions:
% 0.41/0.79 Problem Properties:
% 0.41/0.79 This is a Bernays Schoenfinkel problem.
% 0.41/0.79
% 0.41/0.79 After reduction: Problem Properties:
% 0.41/0.79 This is a Bernays Schoenfinkel problem.
% 0.41/0.79
% 0.41/0.79
% 0.41/0.79 Reduced Input Clauses:
% 0.41/0.79 103:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 0.41/0.79 105:1:2:[103.1,3.0,1.0,104.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 0.41/0.79 108:1:3:[105.2,4.0,103.1,106.1,1.0,107.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 0.41/0.79 112:1:4:[108.3,5.0,105.2,109.1,103.1,110.2,1.0,111.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 116:1:4:[108.3,6.0,105.2,113.1,103.1,114.2,1.0,115.3]:TopTopTopTop: -> ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,skc46)
% 0.41/0.79 120:1:4:[108.3,7.1,105.2,117.2,103.1,118.3,1.0,119.4]:TopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,skc47) ->
% 0.41/0.79 125:1:5:[112.4,8.0,108.3,121.1,105.2,122.2,103.1,123.3,1.0,124.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.41/0.79 130:1:5:[112.4,9.0,108.3,126.1,105.2,127.2,103.1,128.3,1.0,129.4]:TopTopTopTopTop: -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc44)
% 0.41/0.79 135:1:5:[112.4,10.1,108.3,131.2,105.2,132.3,103.1,133.4,1.0,134.5]:TopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc45) ->
% 0.41/0.79 141:1:6:[125.5,11.0,112.4,136.1,108.3,137.2,105.2,138.3,103.1,139.4,1.0,140.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.41/0.79 147:1:6:[125.5,12.0,112.4,142.1,108.3,143.2,105.2,144.3,103.1,145.4,1.0,146.5]:TopTopTopTopTopTop: -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc42)
% 0.41/0.79 153:1:6:[125.5,13.1,112.4,148.2,108.3,149.3,105.2,150.4,103.1,151.5,1.0,152.6]:TopTopTopTopTopTop: ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc43) ->
% 0.41/0.79 160:1:7:[141.6,14.0,125.5,154.1,112.4,155.2,108.3,156.3,105.2,157.4,103.1,158.5,1.0,159.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 167:1:7:[141.6,15.0,125.5,161.1,112.4,162.2,108.3,163.3,105.2,164.4,103.1,165.5,1.0,166.6]:TopTopTopTopTopTopTop: -> ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc40)
% 0.41/0.79 174:1:7:[141.6,16.1,125.5,168.2,112.4,169.3,108.3,170.4,105.2,171.5,103.1,172.6,1.0,173.7]:TopTopTopTopTopTopTop: ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc41) ->
% 0.41/0.79 182:1:8:[160.7,17.0,141.6,175.1,125.5,176.2,112.4,177.3,108.3,178.4,105.2,179.5,103.1,180.6,1.0,181.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 191:1:9:[182.8,18.0,160.7,183.1,141.6,184.2,125.5,185.3,112.4,186.4,108.3,187.5,105.2,188.6,103.1,189.7,1.0,190.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.41/0.79 201:1:10:[191.9,19.0,182.8,192.1,160.7,193.2,141.6,194.3,125.5,195.4,112.4,196.5,108.3,197.6,105.2,198.7,103.1,199.8,1.0,200.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.41/0.79 212:1:11:[201.10,20.0,191.9,202.1,182.8,203.2,160.7,204.3,141.6,205.4,125.5,206.5,112.4,207.6,108.3,208.7,105.2,209.8,103.1,210.9,1.0,211.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.41/0.79 224:1:12:[212.11,21.0,201.10,213.1,191.9,214.2,182.8,215.3,160.7,216.4,141.6,217.5,125.5,218.6,112.4,219.7,108.3,220.8,105.2,221.9,103.1,222.10,1.0,223.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.41/0.79 236:1:12:[212.11,22.0,201.10,225.1,191.9,226.2,182.8,227.3,160.7,228.4,141.6,229.5,125.5,230.6,112.4,231.7,108.3,232.8,105.2,233.9,103.1,234.10,1.0,235.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc38)
% 0.41/0.79 248:1:12:[212.11,23.1,201.10,237.2,191.9,238.3,182.8,239.4,160.7,240.5,141.6,241.6,125.5,242.7,112.4,243.8,108.3,244.9,105.2,245.10,103.1,246.11,1.0,247.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc39) ->
% 0.41/0.79 261:1:13:[224.12,24.0,212.11,249.1,201.10,250.2,191.9,251.3,182.8,252.4,160.7,253.5,141.6,254.6,125.5,255.7,112.4,256.8,108.3,257.9,105.2,258.10,103.1,259.11,1.0,260.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 274:1:13:[224.12,25.0,212.11,262.1,201.10,263.2,191.9,264.3,182.8,265.4,160.7,266.5,141.6,267.6,125.5,268.7,112.4,269.8,108.3,270.9,105.2,271.10,103.1,272.11,1.0,273.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc36)
% 0.41/0.79 287:1:13:[224.12,26.1,212.11,275.2,201.10,276.3,191.9,277.4,182.8,278.5,160.7,279.6,141.6,280.7,125.5,281.8,112.4,282.9,108.3,283.10,105.2,284.11,103.1,285.12,1.0,286.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc37) ->
% 0.41/0.79 301:1:14:[261.13,27.0,224.12,288.1,212.11,289.2,201.10,290.3,191.9,291.4,182.8,292.5,160.7,293.6,141.6,294.7,125.5,295.8,112.4,296.9,108.3,297.10,105.2,298.11,103.1,299.12,1.0,300.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.41/0.79 315:1:14:[261.13,28.0,224.12,302.1,212.11,303.2,201.10,304.3,191.9,305.4,182.8,306.5,160.7,307.6,141.6,308.7,125.5,309.8,112.4,310.9,108.3,311.10,105.2,312.11,103.1,313.12,1.0,314.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc34)
% 0.41/0.79 329:1:14:[261.13,29.1,224.12,316.2,212.11,317.3,201.10,318.4,191.9,319.5,182.8,320.6,160.7,321.7,141.6,322.8,125.5,323.9,112.4,324.10,108.3,325.11,105.2,326.12,103.1,327.13,1.0,328.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc35) ->
% 0.41/0.79 344:1:15:[301.14,30.0,261.13,330.1,224.12,331.2,212.11,332.3,201.10,333.4,191.9,334.5,182.8,335.6,160.7,336.7,141.6,337.8,125.5,338.9,112.4,339.10,108.3,340.11,105.2,341.12,103.1,342.13,1.0,343.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.41/0.79 359:1:15:[301.14,31.0,261.13,345.1,224.12,346.2,212.11,347.3,201.10,348.4,191.9,349.5,182.8,350.6,160.7,351.7,141.6,352.8,125.5,353.9,112.4,354.10,108.3,355.11,105.2,356.12,103.1,357.13,1.0,358.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc32)
% 0.41/0.79 374:1:15:[301.14,32.1,261.13,360.2,224.12,361.3,212.11,362.4,201.10,363.5,191.9,364.6,182.8,365.7,160.7,366.8,141.6,367.9,125.5,368.10,112.4,369.11,108.3,370.12,105.2,371.13,103.1,372.14,1.0,373.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc33) ->
% 0.41/0.79 389:4:15:[301.14,33.0,261.13,375.1,224.12,376.2,212.11,377.3,201.10,378.4,191.9,379.5,182.8,380.6,160.7,381.7,141.6,382.9,125.5,383.10,112.4,384.11,108.3,385.12,105.2,386.14,103.1,387.15,1.0,388.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) -> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 405:1:16:[344.15,34.0,301.14,390.1,261.13,391.2,224.12,392.3,212.11,393.4,201.10,394.5,191.9,395.6,182.8,396.7,160.7,397.8,141.6,398.9,125.5,399.10,112.4,400.11,108.3,401.12,105.2,402.13,103.1,403.14,1.0,404.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.41/0.79 422:1:17:[405.16,35.0,344.15,406.1,301.14,407.2,261.13,408.3,224.12,409.4,212.11,410.5,201.10,411.6,191.9,412.7,182.8,413.8,160.7,414.9,141.6,415.10,125.5,416.11,112.4,417.12,108.3,418.13,105.2,419.14,103.1,420.15,1.0,421.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.41/0.79 438:4:16:[344.15,36.0,301.14,423.2,261.13,424.3,224.12,425.4,212.11,426.5,201.10,427.6,191.9,428.7,182.8,429.8,160.7,430.9,141.6,431.10,125.5,432.11,112.4,433.12,108.3,434.13,105.2,435.15,103.1,436.16,1.0,437.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv27_2r1r1(x0,x1) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 456:1:18:[422.17,37.0,405.16,439.1,344.15,440.2,301.14,441.3,261.13,442.4,224.12,443.5,212.11,444.6,201.10,445.7,191.9,446.8,182.8,447.9,160.7,448.10,141.6,449.11,125.5,450.12,112.4,451.13,108.3,452.14,105.2,453.15,103.1,454.16,1.0,455.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.41/0.79 473:4:17:[405.16,38.0,344.15,457.2,301.14,458.3,261.13,459.4,224.12,460.5,212.11,461.6,201.10,462.7,191.9,463.8,182.8,464.9,160.7,465.10,141.6,466.11,125.5,467.13,112.4,468.14,108.3,469.15,105.2,470.16,103.1,471.17,1.0,472.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 490:4:17:[405.16,39.0,344.15,474.1,301.14,475.2,261.13,476.3,224.12,477.4,212.11,478.5,201.10,479.6,191.9,480.8,182.8,481.9,160.7,482.10,141.6,483.11,125.5,484.12,112.4,485.13,108.3,486.14,105.2,487.15,103.1,488.16,1.0,489.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 509:1:19:[456.18,40.0,422.17,491.1,405.16,492.2,344.15,493.3,301.14,494.4,261.13,495.5,224.12,496.6,212.11,497.7,201.10,498.8,191.9,499.9,182.8,500.10,160.7,501.11,141.6,502.12,125.5,503.13,112.4,504.14,108.3,505.15,105.2,506.16,103.1,507.17,1.0,508.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.41/0.79 527:4:18:[422.17,41.0,405.16,510.1,344.15,511.2,301.14,512.3,261.13,513.4,224.12,514.5,212.11,515.6,201.10,516.7,191.9,517.8,182.8,518.9,160.7,519.10,141.6,520.11,125.5,521.13,112.4,522.14,108.3,523.15,105.2,524.16,103.1,525.17,1.0,526.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 547:1:20:[509.19,42.0,456.18,528.1,422.17,529.2,405.16,530.3,344.15,531.4,301.14,532.5,261.13,533.6,224.12,534.7,212.11,535.8,201.10,536.9,191.9,537.10,182.8,538.11,160.7,539.12,141.6,540.13,125.5,541.14,112.4,542.15,108.3,543.16,105.2,544.17,103.1,545.18,1.0,546.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.41/0.79 567:1:20:[509.19,43.0,456.18,548.1,422.17,549.2,405.16,550.3,344.15,551.4,301.14,552.5,261.13,553.6,224.12,554.7,212.11,555.8,201.10,556.9,191.9,557.10,182.8,558.11,160.7,559.12,141.6,560.13,125.5,561.14,112.4,562.15,108.3,563.16,105.2,564.17,103.1,565.18,1.0,566.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,skc30)
% 0.41/0.79 587:1:20:[509.19,44.1,456.18,568.2,422.17,569.3,405.16,570.4,344.15,571.5,301.14,572.6,261.13,573.7,224.12,574.8,212.11,575.9,201.10,576.10,191.9,577.11,182.8,578.12,160.7,579.13,141.6,580.14,125.5,581.15,112.4,582.16,108.3,583.17,105.2,584.18,103.1,585.19,1.0,586.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,skc31) ->
% 0.41/0.79 606:4:19:[456.18,45.0,422.17,588.2,405.16,589.3,344.15,590.4,301.14,591.5,261.13,592.6,224.12,593.7,212.11,594.8,201.10,595.9,191.9,596.10,182.8,597.11,160.7,598.12,141.6,599.14,125.5,600.15,112.4,601.16,108.3,602.17,105.2,603.18,103.1,604.19,1.0,605.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 625:4:19:[456.18,46.0,422.17,607.2,405.16,608.3,344.15,609.4,301.14,610.5,261.13,611.6,224.12,612.7,212.11,613.8,201.10,614.10,191.9,615.11,182.8,616.12,160.7,617.13,141.6,618.14,125.5,619.16,112.4,620.17,108.3,621.18,105.2,622.19,103.1,623.20,1.0,624.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.41/0.79 644:4:19:[456.18,47.0,422.17,626.2,405.16,627.3,344.15,628.4,301.14,629.6,261.13,630.7,224.12,631.8,212.11,632.9,201.10,633.10,191.9,634.11,182.8,635.12,160.7,636.13,141.6,637.14,125.5,638.15,112.4,639.16,108.3,640.17,105.2,641.18,103.1,642.19,1.0,643.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 664:4:20:[509.19,48.0,456.18,645.2,422.17,646.3,405.16,647.4,344.15,648.5,301.14,649.6,261.13,650.7,224.12,651.8,212.11,652.9,201.10,653.10,191.9,654.11,182.8,655.12,160.7,656.14,141.6,657.16,125.5,658.17,112.4,659.18,108.3,660.19,105.2,661.21,103.1,662.22,1.0,663.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) ->
% 0.41/0.79 685:1:21:[547.20,49.0,509.19,665.1,456.18,666.2,422.17,667.3,405.16,668.4,344.15,669.5,301.14,670.6,261.13,671.7,224.12,672.8,212.11,673.9,201.10,674.10,191.9,675.11,182.8,676.12,160.7,677.13,141.6,678.14,125.5,679.15,112.4,680.16,108.3,681.17,105.2,682.18,103.1,683.19,1.0,684.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 0.41/0.79 706:1:21:[547.20,50.0,509.19,686.1,456.18,687.2,422.17,688.3,405.16,689.4,344.15,690.5,301.14,691.6,261.13,692.7,224.12,693.8,212.11,694.9,201.10,695.10,191.9,696.11,182.8,697.12,160.7,698.13,141.6,699.14,125.5,700.15,112.4,701.16,108.3,702.17,105.2,703.18,103.1,704.19,1.0,705.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc28)
% 0.41/0.79 727:1:21:[547.20,51.1,509.19,707.2,456.18,708.3,422.17,709.4,405.16,710.5,344.15,711.6,301.14,712.7,261.13,713.8,224.12,714.9,212.11,715.10,201.10,716.11,191.9,717.12,182.8,718.13,160.7,719.14,141.6,720.15,125.5,721.16,112.4,722.17,108.3,723.18,105.2,724.19,103.1,725.20,1.0,726.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,skc29) ->
% 0.41/0.79 747:4:20:[509.19,52.0,456.18,728.1,422.17,729.2,405.16,730.3,344.15,731.4,301.14,732.5,261.13,733.6,224.12,734.7,212.11,735.8,201.10,736.9,191.9,737.11,182.8,738.12,160.7,739.13,141.6,740.14,125.5,741.16,112.4,742.17,108.3,743.18,105.2,744.19,103.1,745.20,1.0,746.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 767:4:20:[509.19,53.0,456.18,748.2,422.17,749.3,405.16,750.4,344.15,751.5,301.14,752.6,261.13,753.7,224.12,754.8,212.11,755.9,201.10,756.10,191.9,757.11,182.8,758.13,160.7,759.14,141.6,760.15,125.5,761.16,112.4,762.17,108.3,763.18,105.2,764.19,103.1,765.20,1.0,766.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 789:1:22:[685.21,54.0,547.20,768.1,509.19,769.2,456.18,770.3,422.17,771.4,405.16,772.5,344.15,773.6,301.14,774.7,261.13,775.8,224.12,776.9,212.11,777.10,201.10,778.11,191.9,779.12,182.8,780.13,160.7,781.14,141.6,782.15,125.5,783.16,112.4,784.17,108.3,785.18,105.2,786.19,103.1,787.20,1.0,788.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
% 0.41/0.79 810:4:21:[547.20,55.0,509.19,790.2,456.18,791.3,422.17,792.4,405.16,793.5,344.15,794.6,301.14,795.7,261.13,796.8,224.12,797.9,212.11,798.10,201.10,799.11,191.9,800.12,182.8,801.13,160.7,802.14,141.6,803.15,125.5,804.17,112.4,805.19,108.3,806.20,105.2,807.21,103.1,808.22,1.0,809.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.41/0.79 832:1:22:[685.21,56.0,547.20,811.1,509.19,812.2,456.18,813.3,422.17,814.4,405.16,815.5,344.15,816.6,301.14,817.7,261.13,818.8,224.12,819.9,212.11,820.10,201.10,821.11,191.9,822.12,182.8,823.13,160.7,824.14,141.6,825.15,125.5,826.16,112.4,827.17,108.3,828.18,105.2,829.19,103.1,830.20,1.0,831.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,skc26)
% 0.41/0.79 854:1:22:[685.21,57.1,547.20,833.2,509.19,834.3,456.18,835.4,422.17,836.5,405.16,837.6,344.15,838.7,301.14,839.8,261.13,840.9,224.12,841.10,212.11,842.11,201.10,843.12,191.9,844.13,182.8,845.14,160.7,846.15,141.6,847.16,125.5,848.17,112.4,849.18,108.3,850.19,105.2,851.20,103.1,852.21,1.0,853.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,skc27) ->
% 0.41/0.79 875:4:21:[547.20,58.0,509.19,855.1,456.18,856.2,422.17,857.3,405.16,858.4,344.15,859.5,301.14,860.6,261.13,861.7,224.12,862.8,212.11,863.9,201.10,864.10,191.9,865.11,182.8,866.12,160.7,867.13,141.6,868.14,125.5,869.15,112.4,870.16,108.3,871.17,105.2,872.18,103.1,873.19,1.0,874.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 896:4:21:[547.20,59.0,509.19,876.2,456.18,877.3,422.17,878.4,405.16,879.5,344.15,880.7,301.14,881.8,261.13,882.9,224.12,883.10,212.11,884.11,201.10,885.12,191.9,886.13,182.8,887.14,160.7,888.15,141.6,889.16,125.5,890.17,112.4,891.18,108.3,892.19,105.2,893.20,103.1,894.21,1.0,895.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 917:4:21:[547.20,60.1,509.19,897.2,456.18,898.3,422.17,899.4,405.16,900.5,344.15,901.6,301.14,902.7,261.13,903.8,224.12,904.9,212.11,905.10,201.10,906.11,191.9,907.12,182.8,908.13,160.7,909.14,141.6,910.16,125.5,911.17,112.4,912.18,108.3,913.19,105.2,914.21,103.1,915.22,1.0,916.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 0.41/0.79 938:4:21:[547.20,61.0,509.19,918.1,456.18,919.2,422.17,920.3,405.16,921.4,344.15,922.5,301.14,923.6,261.13,924.7,224.12,925.8,212.11,926.9,201.10,927.11,191.9,928.12,182.8,929.14,160.7,930.15,141.6,931.16,125.5,932.17,112.4,933.18,108.3,934.19,105.2,935.20,103.1,936.21,1.0,937.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.41/0.79 960:4:22:[685.21,62.0,547.20,939.2,509.19,940.3,456.18,941.4,422.17,942.5,405.16,943.6,344.15,944.7,301.14,945.8,261.13,946.9,224.12,947.10,212.11,948.11,201.10,949.12,191.9,950.13,182.8,951.14,160.7,952.15,141.6,953.16,125.5,954.17,112.4,955.18,108.3,956.19,105.2,957.20,103.1,958.21,1.0,959.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv26_3r1r1r1(x0,x1,x2),ssPv28_1r1(x0)
% 0.41/0.79 983:1:23:[789.22,63.0,685.21,961.1,547.20,962.2,509.19,963.3,456.18,964.4,422.17,965.5,405.16,966.6,344.15,967.7,301.14,968.8,261.13,969.9,224.12,970.10,212.11,971.11,201.10,972.12,191.9,973.13,182.8,974.14,160.7,975.15,141.6,976.16,125.5,977.17,112.4,978.18,108.3,979.19,105.2,980.20,103.1,981.21,1.0,982.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22)
% 0.41/0.79 1006:1:23:[789.22,64.0,685.21,984.1,547.20,985.2,509.19,986.3,456.18,987.4,422.17,988.5,405.16,989.6,344.15,990.7,301.14,991.8,261.13,992.9,224.12,993.10,212.11,994.11,201.10,995.12,191.9,996.13,182.8,997.14,160.7,998.15,141.6,999.16,125.5,1000.17,112.4,1001.18,108.3,1002.19,105.2,1003.20,103.1,1004.21,1.0,1005.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,skc24)
% 0.41/0.79 1029:1:23:[789.22,65.1,685.21,1007.2,547.20,1008.3,509.19,1009.4,456.18,1010.5,422.17,1011.6,405.16,1012.7,344.15,1013.8,301.14,1014.9,261.13,1015.10,224.12,1016.11,212.11,1017.12,201.10,1018.13,191.9,1019.14,182.8,1020.15,160.7,1021.16,141.6,1022.17,125.5,1023.18,112.4,1024.19,108.3,1025.20,105.2,1026.21,103.1,1027.22,1.0,1028.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,skc25) ->
% 0.41/0.79 1052:4:23:[789.22,66.0,685.21,1030.2,547.20,1031.3,509.19,1032.4,456.18,1033.5,422.17,1034.6,405.16,1035.7,344.15,1036.8,301.14,1037.9,261.13,1038.11,224.12,1039.12,212.11,1040.13,201.10,1041.14,191.9,1042.15,182.8,1043.16,160.7,1044.17,141.6,1045.18,125.5,1046.19,112.4,1047.20,108.3,1048.22,105.2,1049.23,103.1,1050.24,1.0,1051.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 1076:1:24:[983.23,67.0,789.22,1053.1,685.21,1054.2,547.20,1055.3,509.19,1056.4,456.18,1057.5,422.17,1058.6,405.16,1059.7,344.15,1060.8,301.14,1061.9,261.13,1062.10,224.12,1063.11,212.11,1064.12,201.10,1065.13,191.9,1066.14,182.8,1067.15,160.7,1068.16,141.6,1069.17,125.5,1070.18,112.4,1071.19,108.3,1072.20,105.2,1073.21,103.1,1074.22,1.0,1075.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23)
% 0.41/0.79 1099:4:23:[789.22,68.0,685.21,1077.2,547.20,1078.3,509.19,1079.4,456.18,1080.5,422.17,1081.6,405.16,1082.7,344.15,1083.8,301.14,1084.9,261.13,1085.10,224.12,1086.11,212.11,1087.12,201.10,1088.13,191.9,1089.14,182.8,1090.15,160.7,1091.16,141.6,1092.17,125.5,1093.18,112.4,1094.19,108.3,1095.20,105.2,1096.21,103.1,1097.22,1.0,1098.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 1122:4:23:[789.22,69.0,685.21,1100.1,547.20,1101.2,509.19,1102.3,456.18,1103.5,422.17,1104.6,405.16,1105.7,344.15,1106.8,301.14,1107.9,261.13,1108.10,224.12,1109.11,212.11,1110.12,201.10,1111.13,191.9,1112.14,182.8,1113.15,160.7,1114.16,141.6,1115.17,125.5,1116.18,112.4,1117.19,108.3,1118.20,105.2,1119.22,103.1,1120.23,1.0,1121.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 1145:4:23:[789.22,70.0,685.21,1123.2,547.20,1124.3,509.19,1125.4,456.18,1126.5,422.17,1127.7,405.16,1128.8,344.15,1129.9,301.14,1130.10,261.13,1131.11,224.12,1132.12,212.11,1133.13,201.10,1134.14,191.9,1135.15,182.8,1136.16,160.7,1137.17,141.6,1138.18,125.5,1139.19,112.4,1140.21,108.3,1141.22,105.2,1142.23,103.1,1143.24,1.0,1144.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.41/0.79 1168:4:23:[789.22,71.0,685.21,1146.2,547.20,1147.4,509.19,1148.5,456.18,1149.6,422.17,1150.7,405.16,1151.8,344.15,1152.9,301.14,1153.10,261.13,1154.11,224.12,1155.12,212.11,1156.13,201.10,1157.14,191.9,1158.15,182.8,1159.16,160.7,1160.17,141.6,1161.18,125.5,1162.19,112.4,1163.20,108.3,1164.22,105.2,1165.23,103.1,1166.24,1.0,1167.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.41/0.79 1191:4:23:[789.22,72.0,685.21,1169.1,547.20,1170.2,509.19,1171.4,456.18,1172.5,422.17,1173.6,405.16,1174.7,344.15,1175.8,301.14,1176.9,261.13,1177.10,224.12,1178.11,212.11,1179.12,201.10,1180.13,191.9,1181.15,182.8,1182.16,160.7,1183.17,141.6,1184.18,125.5,1185.19,112.4,1186.20,108.3,1187.21,105.2,1188.22,103.1,1189.23,1.0,1190.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.41/0.79 1216:1:25:[1076.24,73.0,983.23,1192.1,789.22,1193.2,685.21,1194.3,547.20,1195.4,509.19,1196.5,456.18,1197.6,422.17,1198.7,405.16,1199.8,344.15,1200.9,301.14,1201.10,261.13,1202.11,224.12,1203.12,212.11,1204.13,201.10,1205.14,191.9,1206.15,182.8,1207.16,160.7,1208.17,141.6,1209.18,125.5,1210.19,112.4,1211.20,108.3,1212.21,105.2,1213.22,103.1,1214.23,1.0,1215.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24)
% 0.41/0.79 1240:4:24:[983.23,74.0,789.22,1217.2,685.21,1218.3,547.20,1219.4,509.19,1220.5,456.18,1221.6,422.17,1222.7,405.16,1223.8,344.15,1224.10,301.14,1225.11,261.13,1226.12,224.12,1227.13,212.11,1228.14,201.10,1229.15,191.9,1230.16,182.8,1231.17,160.7,1232.18,141.6,1233.19,125.5,1234.20,112.4,1235.21,108.3,1236.22,105.2,1237.23,103.1,1238.24,1.0,1239.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 1264:4:24:[983.23,75.0,789.22,1241.3,685.21,1242.4,547.20,1243.5,509.19,1244.6,456.18,1245.7,422.17,1246.8,405.16,1247.9,344.15,1248.10,301.14,1249.11,261.13,1250.12,224.12,1251.13,212.11,1252.14,201.10,1253.15,191.9,1254.16,182.8,1255.17,160.7,1256.18,141.6,1257.19,125.5,1258.20,112.4,1259.21,108.3,1260.22,105.2,1261.23,103.1,1262.24,1.0,1263.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv28_1r1(x0)
% 0.41/0.79 1290:1:26:[1216.25,76.0,1076.24,1265.1,983.23,1266.2,789.22,1267.3,685.21,1268.4,547.20,1269.5,509.19,1270.6,456.18,1271.7,422.17,1272.8,405.16,1273.9,344.15,1274.10,301.14,1275.11,261.13,1276.12,224.12,1277.13,212.11,1278.14,201.10,1279.15,191.9,1280.16,182.8,1281.17,160.7,1282.18,141.6,1283.19,125.5,1284.20,112.4,1285.21,108.3,1286.22,105.2,1287.23,103.1,1288.24,1.0,1289.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25)
% 0.41/0.79 1315:4:25:[1076.24,77.0,983.23,1291.2,789.22,1292.3,685.21,1293.4,547.20,1294.5,509.19,1295.6,456.18,1296.7,422.17,1297.8,405.16,1298.9,344.15,1299.10,301.14,1300.11,261.13,1301.12,224.12,1302.13,212.11,1303.14,201.10,1304.15,191.9,1305.16,182.8,1306.17,160.7,1307.19,141.6,1308.20,125.5,1309.21,112.4,1310.22,108.3,1311.23,105.2,1312.25,103.1,1313.26,1.0,1314.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv27_2r1r1(x0,x1) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20)
% 0.41/0.79 1340:4:25:[1076.24,78.0,983.23,1316.2,789.22,1317.3,685.21,1318.4,547.20,1319.5,509.19,1320.6,456.18,1321.7,422.17,1322.8,405.16,1323.9,344.15,1324.10,301.14,1325.11,261.13,1326.12,224.12,1327.13,212.11,1328.14,201.10,1329.15,191.9,1330.16,182.8,1331.17,160.7,1332.18,141.6,1333.19,125.5,1334.20,112.4,1335.22,108.3,1336.23,105.2,1337.24,103.1,1338.25,1.0,1339.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.41/0.79 1365:4:25:[1076.24,79.0,983.23,1341.2,789.22,1342.3,685.21,1343.5,547.20,1344.6,509.19,1345.7,456.18,1346.8,422.17,1347.9,405.16,1348.10,344.15,1349.11,301.14,1350.12,261.13,1351.14,224.12,1352.15,212.11,1353.16,201.10,1354.17,191.9,1355.18,182.8,1356.19,160.7,1357.20,141.6,1358.21,125.5,1359.22,112.4,1360.24,108.3,1361.25,105.2,1362.26,103.1,1363.27,1.0,1364.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3) ->
% 0.41/0.79 1390:4:25:[1076.24,80.0,983.23,1366.2,789.22,1367.3,685.21,1368.4,547.20,1369.5,509.19,1370.6,456.18,1371.7,422.17,1372.8,405.16,1373.9,344.15,1374.10,301.14,1375.11,261.13,1376.12,224.12,1377.13,212.11,1378.15,201.10,1379.16,191.9,1380.17,182.8,1381.18,160.7,1382.19,141.6,1383.20,125.5,1384.21,112.4,1385.22,108.3,1386.23,105.2,1387.24,103.1,1388.25,1.0,1389.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 1417:1:27:[1290.26,81.0,1216.25,1391.1,1076.24,1392.2,983.23,1393.3,789.22,1394.4,685.21,1395.5,547.20,1396.6,509.19,1397.7,456.18,1398.8,422.17,1399.9,405.16,1400.10,344.15,1401.11,301.14,1402.12,261.13,1403.13,224.12,1404.14,212.11,1405.15,201.10,1406.16,191.9,1407.17,182.8,1408.18,160.7,1409.19,141.6,1410.20,125.5,1411.21,112.4,1412.22,108.3,1413.23,105.2,1414.24,103.1,1415.25,1.0,1416.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26)
% 0.41/0.79 1443:4:26:[1216.25,82.0,1076.24,1418.1,983.23,1419.2,789.22,1420.3,685.21,1421.4,547.20,1422.5,509.19,1423.6,456.18,1424.7,422.17,1425.8,405.16,1426.10,344.15,1427.11,301.14,1428.12,261.13,1429.13,224.12,1430.14,212.11,1431.15,201.10,1432.16,191.9,1433.17,182.8,1434.18,160.7,1435.19,141.6,1436.20,125.5,1437.21,112.4,1438.22,108.3,1439.23,105.2,1440.24,103.1,1441.25,1.0,1442.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.41/0.79 1469:4:26:[1216.25,83.0,1076.24,1444.2,983.23,1445.4,789.22,1446.5,685.21,1447.6,547.20,1448.7,509.19,1449.8,456.18,1450.9,422.17,1451.10,405.16,1452.11,344.15,1453.12,301.14,1454.13,261.13,1455.14,224.12,1456.15,212.11,1457.16,201.10,1458.18,191.9,1459.19,182.8,1460.20,160.7,1461.21,141.6,1462.23,125.5,1463.24,112.4,1464.25,108.3,1465.26,105.2,1466.27,103.1,1467.28,1.0,1468.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ->
% 0.41/0.79 1495:4:26:[1216.25,84.0,1076.24,1470.2,983.23,1471.3,789.22,1472.4,685.21,1473.5,547.20,1474.6,509.19,1475.7,456.18,1476.8,422.17,1477.9,405.16,1478.10,344.15,1479.11,301.14,1480.12,261.13,1481.13,224.12,1482.14,212.11,1483.15,201.10,1484.16,191.9,1485.17,182.8,1486.18,160.7,1487.19,141.6,1488.20,125.5,1489.21,112.4,1490.22,108.3,1491.23,105.2,1492.24,103.1,1493.25,1.0,1494.26]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.41/0.79 1522:4:27:[1290.26,85.0,1216.25,1496.2,1076.24,1497.4,983.23,1498.5,789.22,1499.6,685.21,1500.7,547.20,1501.8,509.19,1502.9,456.18,1503.10,422.17,1504.11,405.16,1505.12,344.15,1506.13,301.14,1507.14,261.13,1508.15,224.12,1509.16,212.11,1510.17,201.10,1511.18,191.9,1512.19,182.8,1513.20,160.7,1514.21,141.6,1515.22,125.5,1516.23,112.4,1517.24,108.3,1518.25,105.2,1519.27,103.1,1520.28,1.0,1521.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv27_2r1r1(x0,x1) -> ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.41/0.79 1549:4:27:[1290.26,86.1,1216.25,1523.3,1076.24,1524.4,983.23,1525.5,789.22,1526.6,685.21,1527.7,547.20,1528.8,509.19,1529.9,456.18,1530.10,422.17,1531.11,405.16,1532.12,344.15,1533.13,301.14,1534.14,261.13,1535.15,224.12,1536.16,212.11,1537.17,201.10,1538.18,191.9,1539.19,182.8,1540.20,160.7,1541.21,141.6,1542.22,125.5,1543.24,112.4,1544.25,108.3,1545.26,105.2,1546.27,103.1,1547.28,1.0,1548.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25),ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 1576:4:27:[1290.26,87.0,1216.25,1550.2,1076.24,1551.3,983.23,1552.5,789.22,1553.6,685.21,1554.7,547.20,1555.8,509.19,1556.9,456.18,1557.10,422.17,1558.11,405.16,1559.12,344.15,1560.14,301.14,1561.15,261.13,1562.16,224.12,1563.17,212.11,1564.18,201.10,1565.19,191.9,1566.20,182.8,1567.21,160.7,1568.22,141.6,1569.23,125.5,1570.24,112.4,1571.25,108.3,1572.26,105.2,1573.27,103.1,1574.28,1.0,1575.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 1603:4:27:[1290.26,88.0,1216.25,1577.2,1076.24,1578.3,983.23,1579.4,789.22,1580.5,685.21,1581.6,547.20,1582.7,509.19,1583.8,456.18,1584.10,422.17,1585.11,405.16,1586.12,344.15,1587.13,301.14,1588.14,261.13,1589.15,224.12,1590.16,212.11,1591.17,201.10,1592.18,191.9,1593.19,182.8,1594.20,160.7,1595.21,141.6,1596.22,125.5,1597.23,112.4,1598.24,108.3,1599.25,105.2,1600.26,103.1,1601.27,1.0,1602.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 1630:4:27:[1290.26,89.0,1216.25,1604.2,1076.24,1605.3,983.23,1606.4,789.22,1607.5,685.21,1608.6,547.20,1609.7,509.19,1610.8,456.18,1611.9,422.17,1612.10,405.16,1613.11,344.15,1614.12,301.14,1615.13,261.13,1616.14,224.12,1617.15,212.11,1618.17,201.10,1619.18,191.9,1620.19,182.8,1621.20,160.7,1622.21,141.6,1623.22,125.5,1624.23,112.4,1625.24,108.3,1626.25,105.2,1627.26,103.1,1628.27,1.0,1629.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.41/0.79 1658:4:28:[1417.27,90.0,1290.26,1631.1,1216.25,1632.2,1076.24,1633.3,983.23,1634.4,789.22,1635.5,685.21,1636.6,547.20,1637.7,509.19,1638.8,456.18,1639.9,422.17,1640.10,405.16,1641.11,344.15,1642.12,301.14,1643.13,261.13,1644.14,224.12,1645.15,212.11,1646.16,201.10,1647.17,191.9,1648.18,182.8,1649.19,160.7,1650.20,141.6,1651.21,125.5,1652.23,112.4,1653.24,108.3,1654.25,105.2,1655.26,103.1,1656.27,1.0,1657.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 1686:4:28:[1417.27,91.0,1290.26,1659.1,1216.25,1660.2,1076.24,1661.3,983.23,1662.4,789.22,1663.5,685.21,1664.6,547.20,1665.7,509.19,1666.8,456.18,1667.9,422.17,1668.10,405.16,1669.11,344.15,1670.12,301.14,1671.14,261.13,1672.15,224.12,1673.16,212.11,1674.17,201.10,1675.18,191.9,1676.19,182.8,1677.20,160.7,1678.21,141.6,1679.22,125.5,1680.23,112.4,1681.24,108.3,1682.25,105.2,1683.26,103.1,1684.27,1.0,1685.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.41/0.79 1714:4:28:[1417.27,92.0,1290.26,1687.1,1216.25,1688.2,1076.24,1689.3,983.23,1690.4,789.22,1691.5,685.21,1692.6,547.20,1693.7,509.19,1694.8,456.18,1695.9,422.17,1696.10,405.16,1697.11,344.15,1698.12,301.14,1699.13,261.13,1700.14,224.12,1701.15,212.11,1702.16,201.10,1703.17,191.9,1704.18,182.8,1705.19,160.7,1706.20,141.6,1707.21,125.5,1708.22,112.4,1709.23,108.3,1710.25,105.2,1711.26,103.1,1712.27,1.0,1713.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv26_3r1r1r1(x0,x1,x2) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 1742:4:28:[1417.27,93.0,1290.26,1715.1,1216.25,1716.2,1076.24,1717.3,983.23,1718.5,789.22,1719.6,685.21,1720.7,547.20,1721.8,509.19,1722.9,456.18,1723.10,422.17,1724.11,405.16,1725.12,344.15,1726.13,301.14,1727.14,261.13,1728.15,224.12,1729.16,212.11,1730.17,201.10,1731.18,191.9,1732.19,182.8,1733.20,160.7,1734.21,141.6,1735.22,125.5,1736.24,112.4,1737.25,108.3,1738.27,105.2,1739.28,103.1,1740.29,1.0,1741.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27)
% 0.41/0.79 1770:4:28:[1417.27,94.0,1290.26,1743.1,1216.25,1744.2,1076.24,1745.3,983.23,1746.5,789.22,1747.6,685.21,1748.7,547.20,1749.8,509.19,1750.9,456.18,1751.10,422.17,1752.11,405.16,1753.12,344.15,1754.13,301.14,1755.14,261.13,1756.15,224.12,1757.16,212.11,1758.17,201.10,1759.18,191.9,1760.20,182.8,1761.21,160.7,1762.22,141.6,1763.23,125.5,1764.25,112.4,1765.26,108.3,1766.27,105.2,1767.28,103.1,1768.29,1.0,1769.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27)
% 0.41/0.79 1798:4:28:[1417.27,95.0,1290.26,1771.2,1216.25,1772.3,1076.24,1773.4,983.23,1774.5,789.22,1775.6,685.21,1776.7,547.20,1777.8,509.19,1778.9,456.18,1779.10,422.17,1780.11,405.16,1781.12,344.15,1782.13,301.14,1783.14,261.13,1784.15,224.12,1785.16,212.11,1786.17,201.10,1787.19,191.9,1788.20,182.8,1789.21,160.7,1790.22,141.6,1791.23,125.5,1792.24,112.4,1793.25,108.3,1794.26,105.2,1795.27,103.1,1796.28,1.0,1797.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 1826:4:28:[1417.27,96.0,1290.26,1799.1,1216.25,1800.2,1076.24,1801.3,983.23,1802.4,789.22,1803.5,685.21,1804.6,547.20,1805.7,509.19,1806.8,456.18,1807.9,422.17,1808.10,405.16,1809.12,344.15,1810.13,301.14,1811.14,261.13,1812.15,224.12,1813.16,212.11,1814.17,201.10,1815.18,191.9,1816.19,182.8,1817.20,160.7,1818.21,141.6,1819.22,125.5,1820.23,112.4,1821.24,108.3,1822.25,105.2,1823.27,103.1,1824.28,1.0,1825.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv27_2r1r1(x0,x1) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23)
% 0.41/0.79 1854:4:28:[1417.27,97.0,1290.26,1827.1,1216.25,1828.2,1076.24,1829.3,983.23,1830.4,789.22,1831.6,685.21,1832.8,547.20,1833.9,509.19,1834.10,456.18,1835.11,422.17,1836.12,405.16,1837.13,344.15,1838.14,301.14,1839.15,261.13,1840.16,224.12,1841.17,212.11,1842.18,201.10,1843.19,191.9,1844.20,182.8,1845.21,160.7,1846.22,141.6,1847.23,125.5,1848.24,112.4,1849.25,108.3,1850.27,105.2,1851.28,103.1,1852.29,1.0,1853.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27)
% 0.41/0.79 1882:4:28:[1417.27,98.0,1290.26,1855.2,1216.25,1856.3,1076.24,1857.4,983.23,1858.5,789.22,1859.6,685.21,1860.7,547.20,1861.8,509.19,1862.9,456.18,1863.10,422.17,1864.12,405.16,1865.14,344.15,1866.15,301.14,1867.16,261.13,1868.17,224.12,1869.18,212.11,1870.19,201.10,1871.20,191.9,1872.21,182.8,1873.22,160.7,1874.23,141.6,1875.24,125.5,1876.25,112.4,1877.26,108.3,1878.27,105.2,1879.28,103.1,1880.29,1.0,1881.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21)
% 0.41/0.79 1910:4:28:[1417.27,99.0,1290.26,1883.2,1216.25,1884.3,1076.24,1885.4,983.23,1886.5,789.22,1887.7,685.21,1888.8,547.20,1889.9,509.19,1890.10,456.18,1891.12,422.17,1892.13,405.16,1893.14,344.15,1894.15,301.14,1895.17,261.13,1896.18,224.12,1897.19,212.11,1898.20,201.10,1899.21,191.9,1900.22,182.8,1901.23,160.7,1902.24,141.6,1903.25,125.5,1904.26,112.4,1905.27,108.3,1906.28,105.2,1907.29,103.1,1908.30,1.0,1909.31]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ->
% 0.41/0.79 1938:4:28:[1417.27,100.0,1290.26,1911.1,1216.25,1912.2,1076.24,1913.3,983.23,1914.4,789.22,1915.5,685.21,1916.6,547.20,1917.7,509.19,1918.8,456.18,1919.9,422.17,1920.10,405.16,1921.11,344.15,1922.12,301.14,1923.13,261.13,1924.14,224.12,1925.15,212.11,1926.16,201.10,1927.17,191.9,1928.18,182.8,1929.19,160.7,1930.20,141.6,1931.21,125.5,1932.22,112.4,1933.23,108.3,1934.24,105.2,1935.25,103.1,1936.26,1.0,1937.27]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.41/0.79 1966:4:28:[1417.27,101.0,1290.26,1939.2,1216.25,1940.3,1076.24,1941.5,983.23,1942.6,789.22,1943.7,685.21,1944.9,547.20,1945.10,509.19,1946.11,456.18,1947.12,422.17,1948.13,405.16,1949.14,344.15,1950.15,301.14,1951.16,261.13,1952.17,224.12,1953.18,212.11,1954.19,201.10,1955.20,191.9,1956.21,182.8,1957.22,160.7,1958.23,141.6,1959.24,125.5,1960.25,112.4,1961.26,108.3,1962.27,105.2,1963.28,103.1,1964.29,1.0,1965.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) -> ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.41/0.79 1994:4:28:[1417.27,102.1,1290.26,1967.3,1216.25,1968.4,1076.24,1969.5,983.23,1970.6,789.22,1971.7,685.21,1972.8,547.20,1973.9,509.19,1974.10,456.18,1975.11,422.17,1976.12,405.16,1977.13,344.15,1978.14,301.14,1979.15,261.13,1980.16,224.12,1981.17,212.11,1982.18,201.10,1983.19,191.9,1984.20,182.8,1985.21,160.7,1986.22,141.6,1987.23,125.5,1988.24,112.4,1989.25,108.3,1990.26,105.2,1991.27,103.1,1992.28,1.0,1993.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.41/0.79
% 0.41/0.79 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) 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) ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv27_2r1r1(x0,x1) ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssPv26_3r1r1r1(x0,x1,x2) ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv13_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) ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssPv25_4r1r1r1r1(x0,x1,x2,x3) ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssNder1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) ssNder1_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ssNder1_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) ssPv28_1r1(x0) ssNder1_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) ssNder1_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23) ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssNder1_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23) ssNder1_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) ssPv4_25r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24) ssNder1_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26) ssPv3_26r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25) ssPv2_27r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26) ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27)
% 0.41/0.79
% 0.41/0.79 === Starting SPASS-SCL-FOL A Little Less Naive, considering 35 atoms initially, heuristics mode: resolution_3 ===
% 0.41/0.79
% 0.41/0.79 === Conflict found: 389:4:15:[301.14,33.0,261.13,375.1,224.12,376.2,212.11,377.3,201.10,378.4,191.9,379.5,182.8,380.6,160.7,381.7,141.6,382.9,125.5,383.10,112.4,384.11,108.3,385.12,105.2,386.14,103.1,387.15,1.0,388.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) -> ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv26_3r1r1r1(x0,x1,x2) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc35}
% 0.41/0.79 === Backtracking. Learning clause 1995:3:6:[389.3,329.1]:TopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) -> ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 === Conflict found: 438:4:16:[344.15,36.0,301.14,423.2,261.13,424.3,224.12,425.4,212.11,426.5,201.10,427.6,191.9,428.7,182.8,429.8,160.7,430.9,141.6,431.10,125.5,432.11,112.4,433.12,108.3,434.13,105.2,435.15,103.1,436.16,1.0,437.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv27_2r1r1(x0,x1) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv26_3r1r1r1(x0,x1,x2) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc33}
% 0.41/0.79 === Backtracking. Learning clause 1996:3:14:[438.3,374.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv27_2r1r1(x0,x1) -> ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 === Conflict found: 473:4:17:[405.16,38.0,344.15,457.2,301.14,458.3,261.13,459.4,224.12,460.5,212.11,461.6,201.10,462.7,191.9,463.8,182.8,464.9,160.7,465.10,141.6,466.11,125.5,467.13,112.4,468.14,108.3,469.15,105.2,470.16,103.1,471.17,1.0,472.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 1997:6:16:[473.1,490.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 1997:6:16:[473.1,490.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc33}
% 0.41/0.79 === Backtracking. Learning clause 1998:6:9:[1997.3,374.1,1996.1]:TopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv27_2r1r1(x0,x1) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 === Conflict found: 896:4:21:[547.20,59.0,509.19,876.2,456.18,877.3,422.17,878.4,405.16,879.5,344.15,880.7,301.14,881.8,261.13,882.9,224.12,883.10,212.11,884.11,201.10,885.12,191.9,886.13,182.8,887.14,160.7,888.15,141.6,889.16,125.5,890.17,112.4,891.18,108.3,892.19,105.2,893.20,103.1,894.21,1.0,895.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 1999:5:15:[896.1,875.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 875:4:21:[547.20,58.0,509.19,855.1,456.18,856.2,422.17,857.3,405.16,858.4,344.15,859.5,301.14,860.6,261.13,861.7,224.12,862.8,212.11,863.9,201.10,864.10,191.9,865.11,182.8,866.12,160.7,867.13,141.6,868.14,125.5,869.15,112.4,870.16,108.3,871.17,105.2,872.18,103.1,873.19,1.0,874.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc31}
% 0.41/0.79 === Backtracking. Learning clause 2000:4:11:[875.1,587.1,1996.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv25_4r1r1r1r1(x0,x1,x2,x3),ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 === Conflict found: 896:4:21:[547.20,59.0,509.19,876.2,456.18,877.3,422.17,878.4,405.16,879.5,344.15,880.7,301.14,881.8,261.13,882.9,224.12,883.10,212.11,884.11,201.10,885.12,191.9,886.13,182.8,887.14,160.7,888.15,141.6,889.16,125.5,890.17,112.4,891.18,108.3,892.19,105.2,893.20,103.1,894.21,1.0,895.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc30}
% 0.41/0.79 === Backtracking. Learning clause 2001:3:15:[896.1,567.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 960:4:22:[685.21,62.0,547.20,939.2,509.19,940.3,456.18,941.4,422.17,942.5,405.16,943.6,344.15,944.7,301.14,945.8,261.13,946.9,224.12,947.10,212.11,948.11,201.10,949.12,191.9,950.13,182.8,951.14,160.7,952.15,141.6,953.16,125.5,954.17,112.4,955.18,108.3,956.19,105.2,957.20,103.1,958.21,1.0,959.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv26_3r1r1r1(x0,x1,x2),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc28}
% 0.41/0.79 === Backtracking. Learning clause 2002:3:3:[960.1,706.1,1996.1]:TopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv28_1r1(x0),ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 === Conflict found: 917:4:21:[547.20,60.1,509.19,897.2,456.18,898.3,422.17,899.4,405.16,900.5,344.15,901.6,301.14,902.7,261.13,903.8,224.12,904.9,212.11,905.10,201.10,906.11,191.9,907.12,182.8,908.13,160.7,909.14,141.6,910.16,125.5,911.17,112.4,912.18,108.3,913.19,105.2,914.21,103.1,915.22,1.0,916.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc31}
% 0.41/0.79 === Backtracking. Learning clause 2003:5:9:[917.4,587.1,747.3]:TopTopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 917:4:21:[547.20,60.1,509.19,897.2,456.18,898.3,422.17,899.4,405.16,900.5,344.15,901.6,301.14,902.7,261.13,903.8,224.12,904.9,212.11,905.10,201.10,906.11,191.9,907.12,182.8,908.13,160.7,909.14,141.6,910.16,125.5,911.17,112.4,912.18,108.3,913.19,105.2,914.21,103.1,915.22,1.0,916.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) -> ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc31}
% 0.41/0.79 === Backtracking. Learning clause 2004:3:20:[917.4,587.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) ->
% 0.41/0.79 === Conflict found: 1122:4:23:[789.22,69.0,685.21,1100.1,547.20,1101.2,509.19,1102.3,456.18,1103.5,422.17,1104.6,405.16,1105.7,344.15,1106.8,301.14,1107.9,261.13,1108.10,224.12,1109.11,212.11,1110.12,201.10,1111.13,191.9,1112.14,182.8,1113.15,160.7,1114.16,141.6,1115.17,125.5,1116.18,112.4,1117.19,108.3,1118.20,105.2,1119.22,103.1,1120.23,1.0,1121.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 2005:6:13:[1122.3,1099.1,527.2]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 1122:4:23:[789.22,69.0,685.21,1100.1,547.20,1101.2,509.19,1102.3,456.18,1103.5,422.17,1104.6,405.16,1105.7,344.15,1106.8,301.14,1107.9,261.13,1108.10,224.12,1109.11,212.11,1110.12,201.10,1111.13,191.9,1112.14,182.8,1113.15,160.7,1114.16,141.6,1115.17,125.5,1116.18,112.4,1117.19,108.3,1118.20,105.2,1119.22,103.1,1120.23,1.0,1121.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 2006:5:18:[1122.3,1099.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 1099:4:23:[789.22,68.0,685.21,1077.2,547.20,1078.3,509.19,1079.4,456.18,1080.5,422.17,1081.6,405.16,1082.7,344.15,1083.8,301.14,1084.9,261.13,1085.10,224.12,1086.11,212.11,1087.12,201.10,1088.13,191.9,1089.14,182.8,1090.15,160.7,1091.16,141.6,1092.17,125.5,1093.18,112.4,1094.19,108.3,1095.20,105.2,1096.21,103.1,1097.22,1.0,1098.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22) -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc26}
% 0.41/0.79 === Backtracking. Learning clause 2007:3:12:[1099.1,832.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 1122:4:23:[789.22,69.0,685.21,1100.1,547.20,1101.2,509.19,1102.3,456.18,1103.5,422.17,1104.6,405.16,1105.7,344.15,1106.8,301.14,1107.9,261.13,1108.10,224.12,1109.11,212.11,1110.12,201.10,1111.13,191.9,1112.14,182.8,1113.15,160.7,1114.16,141.6,1115.17,125.5,1116.18,112.4,1117.19,108.3,1118.20,105.2,1119.22,103.1,1120.23,1.0,1121.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc27}
% 0.41/0.79 === Backtracking. Learning clause 2008:5:13:[1122.3,854.1,527.2]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 1122:4:23:[789.22,69.0,685.21,1100.1,547.20,1101.2,509.19,1102.3,456.18,1103.5,422.17,1104.6,405.16,1105.7,344.15,1106.8,301.14,1107.9,261.13,1108.10,224.12,1109.11,212.11,1110.12,201.10,1111.13,191.9,1112.14,182.8,1113.15,160.7,1114.16,141.6,1115.17,125.5,1116.18,112.4,1117.19,108.3,1118.20,105.2,1119.22,103.1,1120.23,1.0,1121.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 2009:6:18:[1122.3,1052.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 1052:4:23:[789.22,66.0,685.21,1030.2,547.20,1031.3,509.19,1032.4,456.18,1033.5,422.17,1034.6,405.16,1035.7,344.15,1036.8,301.14,1037.9,261.13,1038.11,224.12,1039.12,212.11,1040.13,201.10,1041.14,191.9,1042.15,182.8,1043.16,160.7,1044.17,141.6,1045.18,125.5,1046.19,112.4,1047.20,108.3,1048.22,105.2,1049.23,103.1,1050.24,1.0,1051.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc26}
% 0.41/0.79 === Backtracking. Learning clause 2010:5:7:[1052.1,832.1,2008.4]:TopTopTopTopTopTopTop: ssPv26_3r1r1r1(x0,x1,x2),ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 1264:4:24:[983.23,75.0,789.22,1241.3,685.21,1242.4,547.20,1243.5,509.19,1244.6,456.18,1245.7,422.17,1246.8,405.16,1247.9,344.15,1248.10,301.14,1249.11,261.13,1250.12,224.12,1251.13,212.11,1252.14,201.10,1253.15,191.9,1254.16,182.8,1255.17,160.7,1256.18,141.6,1257.19,125.5,1258.20,112.4,1259.21,108.3,1260.22,105.2,1261.23,103.1,1262.24,1.0,1263.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46, x23 -> skc24}
% 0.41/0.79 === Backtracking. Learning clause 2011:3:22:[1264.1,1006.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv28_1r1(x0)
% 0.41/0.79 === Conflict found: 2011:3:22:[1264.1,1006.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc28}
% 0.41/0.79 === Backtracking. Learning clause 2012:4:16:[2011.1,706.1,473.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 2012:4:16:[2011.1,706.1,473.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc33}
% 0.41/0.79 === Backtracking. Learning clause 2013:2:4:[2012.3,374.1,116.1]:TopTopTopTop: -> ssPv28_1r1(x0),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 606:4:19:[456.18,45.0,422.17,588.2,405.16,589.3,344.15,590.4,301.14,591.5,261.13,592.6,224.12,593.7,212.11,594.8,201.10,595.9,191.9,596.10,182.8,597.11,160.7,598.12,141.6,599.14,125.5,600.15,112.4,601.16,108.3,602.17,105.2,603.18,103.1,604.19,1.0,605.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 2014:6:17:[606.3,644.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 2011:3:22:[1264.1,1006.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc28}
% 0.41/0.79 === Backtracking. Learning clause 2015:6:14:[2011.1,706.1,2014.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 606:4:19:[456.18,45.0,422.17,588.2,405.16,589.3,344.15,590.4,301.14,591.5,261.13,592.6,224.12,593.7,212.11,594.8,201.10,595.9,191.9,596.10,182.8,597.11,160.7,598.12,141.6,599.14,125.5,600.15,112.4,601.16,108.3,602.17,105.2,603.18,103.1,604.19,1.0,605.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv10_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 2016:6:17:[606.3,625.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.41/0.79 === Conflict found: 2011:3:22:[1264.1,1006.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc28}
% 0.41/0.79 === Backtracking. Learning clause 2017:7:10:[2011.1,706.1,2016.1,2015.2]:TopTopTopTopTopTopTopTopTopTop: ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 810:4:21:[547.20,55.0,509.19,790.2,456.18,791.3,422.17,792.4,405.16,793.5,344.15,794.6,301.14,795.7,261.13,796.8,224.12,797.9,212.11,798.10,201.10,799.11,191.9,800.12,182.8,801.13,160.7,802.14,141.6,803.15,125.5,804.17,112.4,805.19,108.3,806.20,105.2,807.21,103.1,808.22,1.0,809.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc30}
% 0.41/0.79 === Backtracking. Learning clause 2019:6:8:[2013.1,2018.0,810.1,567.1,2017.1,2003.3]:TopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 1122:4:23:[789.22,69.0,685.21,1100.1,547.20,1101.2,509.19,1102.3,456.18,1103.5,422.17,1104.6,405.16,1105.7,344.15,1106.8,301.14,1107.9,261.13,1108.10,224.12,1109.11,212.11,1110.12,201.10,1111.13,191.9,1112.14,182.8,1113.15,160.7,1114.16,141.6,1115.17,125.5,1116.18,112.4,1117.19,108.3,1118.20,105.2,1119.22,103.1,1120.23,1.0,1121.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1) -> ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc27}
% 0.41/0.79 === Backtracking. Learning clause 2020:3:18:[1122.3,854.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv27_2r1r1(x0,x1) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 === Conflict found: 1742:4:28:[1417.27,93.0,1290.26,1715.1,1216.25,1716.2,1076.24,1717.3,983.23,1718.5,789.22,1719.6,685.21,1720.7,547.20,1721.8,509.19,1722.9,456.18,1723.10,422.17,1724.11,405.16,1725.12,344.15,1726.13,301.14,1727.14,261.13,1728.15,224.12,1729.16,212.11,1730.17,201.10,1731.18,191.9,1732.19,182.8,1733.20,160.7,1734.21,141.6,1735.22,125.5,1736.24,112.4,1737.25,108.3,1738.27,105.2,1739.28,103.1,1740.29,1.0,1741.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46, x23 -> skc46, x24 -> skc46, x25 -> skc46, x26 -> skc46, x27 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 2021:6:23:[1742.4,1798.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 === Conflict found: 2021:6:23:[1742.4,1798.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc26}
% 0.41/0.79 === Backtracking. Learning clause 2022:5:16:[2021.1,832.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 === Conflict found: 2022:5:16:[2021.1,832.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc33}
% 0.41/0.79 === Backtracking. Learning clause 2023:4:13:[2022.4,374.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 === Clause set with instances from active satisfied. Growing active. New size: 41
% 0.41/0.79 === Restarting.
% 0.41/0.79 === Conflict found: 2019:6:8:[2013.1,2018.0,810.1,567.1,2017.1,2003.3]:TopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc41}
% 0.41/0.79 === Backtracking. Learning clause 2024:5:7:[2019.6,174.1]:TopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 === Conflict found: 2024:5:7:[2019.6,174.1]:TopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc43}
% 0.41/0.79 === Backtracking. Learning clause 2025:4:6:[2024.5,153.1]:TopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0)
% 0.41/0.79 === Conflict found: 2025:4:6:[2024.5,153.1]:TopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc44}
% 0.41/0.79 === Backtracking. Learning clause 2026:2:2:[2025.1,130.1,116.1]:TopTop: ssPv27_2r1r1(x0,x1) -> ssPv28_1r1(x0)
% 0.41/0.79 === Conflict found: 1770:4:28:[1417.27,94.0,1290.26,1743.1,1216.25,1744.2,1076.24,1745.3,983.23,1746.5,789.22,1747.6,685.21,1748.7,547.20,1749.8,509.19,1750.9,456.18,1751.10,422.17,1752.11,405.16,1753.12,344.15,1754.13,301.14,1755.14,261.13,1756.15,224.12,1757.16,212.11,1758.17,201.10,1759.18,191.9,1760.20,182.8,1761.21,160.7,1762.22,141.6,1763.23,125.5,1764.25,112.4,1765.26,108.3,1766.27,105.2,1767.28,103.1,1768.29,1.0,1769.30]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46, x23 -> skc46, x24 -> skc46, x25 -> skc46, x26 -> skc46, x27 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 2027:6:23:[1770.4,1798.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 === Conflict found: 2027:6:23:[1770.4,1798.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_23r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc26}
% 0.41/0.79 === Backtracking. Learning clause 2028:5:16:[2027.1,832.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 === Conflict found: 2028:5:16:[2027.1,832.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc33}
% 0.41/0.79 === Backtracking. Learning clause 2029:4:13:[2028.4,374.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.41/0.79 === Conflict found: 2029:4:13:[2028.4,374.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc39}
% 0.41/0.79 === Backtracking. Learning clause 2030:3:10:[2029.4,248.1]:TopTopTopTopTopTopTopTopTopTop: ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ->
% 0.41/0.79 === Conflict found: 810:4:21:[547.20,55.0,509.19,790.2,456.18,791.3,422.17,792.4,405.16,793.5,344.15,794.6,301.14,795.7,261.13,796.8,224.12,797.9,212.11,798.10,201.10,799.11,191.9,800.12,182.8,801.13,160.7,802.14,141.6,803.15,125.5,804.17,112.4,805.19,108.3,806.20,105.2,807.21,103.1,808.22,1.0,809.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc30}
% 0.41/0.79 === Backtracking. Learning clause 2031:3:9:[810.1,567.1,2030.3]:TopTopTopTopTopTopTopTopTop: ssPv25_4r1r1r1r1(x0,x1,x2,x3),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) ->
% 0.41/0.79 === Conflict found: 2015:6:14:[2011.1,706.1,2014.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.41/0.79 === Backtracking. Learning clause 2033:5:8:[2013.1,2032.1,2015.2,274.1,2031.2]:TopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 2033:5:8:[2013.1,2032.1,2015.2,274.1,2031.2]:TopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc41}
% 0.41/0.79 === Backtracking. Learning clause 2034:4:7:[2033.5,174.1]:TopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 === Conflict found: 2034:4:7:[2033.5,174.1]:TopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc43}
% 0.41/0.79 === Backtracking. Learning clause 2035:3:6:[2034.4,153.1]:TopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0)
% 0.41/0.79 === Conflict found: 2035:3:6:[2034.4,153.1]:TopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv28_1r1(x0) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc44}
% 0.41/0.79 === Backtracking. Learning clause 2036:1:1:[2035.1,130.1,116.1]:Top: -> ssPv28_1r1(x0)
% 0.41/0.79 === Conflict found: 1995:3:6:[389.3,329.1]:TopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv27_2r1r1(x0,x1) -> ssPv26_3r1r1r1(x0,x1,x2) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc44}
% 0.41/0.79 === Backtracking. Learning clause 2037:2:3:[1995.1,130.1]:TopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 === Conflict found: 2010:5:7:[1052.1,832.1,2008.4]:TopTopTopTopTopTopTop: ssPv26_3r1r1r1(x0,x1,x2),ssPv27_2r1r1(x0,x1),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc43}
% 0.41/0.79 === Backtracking. Learning clause 2039:2:4:[2037.1,2038.0,2010.4,153.1,116.1]:TopTopTopTop: ssPv27_2r1r1(x0,x1) -> ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 2023:4:13:[2022.4,374.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc39}
% 0.41/0.79 === Backtracking. Learning clause 2040:3:10:[2023.4,248.1]:TopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv26_3r1r1r1(x0,x1,x2),ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ->
% 0.41/0.79 === Conflict found: 810:4:21:[547.20,55.0,509.19,790.2,456.18,791.3,422.17,792.4,405.16,793.5,344.15,794.6,301.14,795.7,261.13,796.8,224.12,797.9,212.11,798.10,201.10,799.11,191.9,800.12,182.8,801.13,160.7,802.14,141.6,803.15,125.5,804.17,112.4,805.19,108.3,806.20,105.2,807.21,103.1,808.22,1.0,809.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc30}
% 0.41/0.79 === Backtracking. Learning clause 2041:1:2:[810.1,567.1,2040.3,116.1,2039.2,2037.2]:TopTop: ssPv27_2r1r1(x0,x1) ->
% 0.41/0.79 === Conflict found: 1240:4:24:[983.23,74.0,789.22,1217.2,685.21,1218.3,547.20,1219.4,509.19,1220.5,456.18,1221.6,422.17,1222.7,405.16,1223.8,344.15,1224.10,301.14,1225.11,261.13,1226.12,224.12,1227.13,212.11,1228.14,201.10,1229.15,191.9,1230.16,182.8,1231.17,160.7,1232.18,141.6,1233.19,125.5,1234.20,112.4,1235.21,108.3,1236.22,105.2,1237.23,103.1,1238.24,1.0,1239.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv26_3r1r1r1(x0,x1,x2) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46, x23 -> skc24}
% 0.41/0.79 === Backtracking. Learning clause 2042:5:16:[1240.1,1006.1,473.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 2042:5:16:[1240.1,1006.1,473.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc33}
% 0.41/0.79 === Backtracking. Learning clause 2043:4:15:[2042.4,374.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 2043:4:15:[2042.4,374.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc34}
% 0.41/0.79 === Backtracking. Learning clause 2044:2:4:[2043.1,315.1,116.1]:TopTopTopTop: -> ssPv26_3r1r1r1(x0,x1,x2),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 1240:4:24:[983.23,74.0,789.22,1217.2,685.21,1218.3,547.20,1219.4,509.19,1220.5,456.18,1221.6,422.17,1222.7,405.16,1223.8,344.15,1224.10,301.14,1225.11,261.13,1226.12,224.12,1227.13,212.11,1228.14,201.10,1229.15,191.9,1230.16,182.8,1231.17,160.7,1232.18,141.6,1233.19,125.5,1234.20,112.4,1235.21,108.3,1236.22,105.2,1237.23,103.1,1238.24,1.0,1239.25]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_24r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23),ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv12_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv26_3r1r1r1(x0,x1,x2) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46, x23 -> skc24}
% 0.41/0.79 === Backtracking. Learning clause 2045:7:15:[1240.1,1006.1,2014.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 2045:7:15:[1240.1,1006.1,2014.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc34}
% 0.41/0.79 === Backtracking. Learning clause 2046:6:14:[2045.1,315.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 2046:6:14:[2045.1,315.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv20_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.41/0.79 === Backtracking. Learning clause 2048:5:8:[2044.1,2047.1,2046.2,274.1,2031.2]:TopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.41/0.79 === Conflict found: 2048:5:8:[2044.1,2047.1,2046.2,274.1,2031.2]:TopTopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv21_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc41}
% 0.41/0.79 === Backtracking. Learning clause 2049:4:7:[2048.5,174.1]:TopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.41/0.79 === Conflict found: 2049:4:7:[2048.5,174.1]:TopTopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2),ssPv22_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc43}
% 0.41/0.79 === Backtracking. Learning clause 2050:3:6:[2049.4,153.1]:TopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 === Conflict found: 2050:3:6:[2049.4,153.1]:TopTopTopTopTopTop: ssPv23_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv26_3r1r1r1(x0,x1,x2) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc44}
% 0.41/0.79 === Backtracking. Learning clause 2051:1:3:[2050.1,130.1,116.1]:TopTopTop: -> ssPv26_3r1r1r1(x0,x1,x2)
% 0.41/0.79 === Conflict found: 1910:4:28:[1417.27,99.0,1290.26,1883.2,1216.25,1884.3,1076.24,1885.4,983.23,1886.5,789.22,1887.7,685.21,1888.8,547.20,1889.9,509.19,1890.10,456.18,1891.12,422.17,1892.13,405.16,1893.14,344.15,1894.15,301.14,1895.17,261.13,1896.18,224.12,1897.19,212.11,1898.20,201.10,1899.21,191.9,1900.22,182.8,1901.23,160.7,1902.24,141.6,1903.25,125.5,1904.26,112.4,1905.27,108.3,1906.28,105.2,1907.29,103.1,1908.30,1.0,1909.31]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_28r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26,x27),ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc46, x22 -> skc46, x23 -> skc46, x24 -> skc46, x25 -> skc46, x26 -> skc46, x27 -> skc46}
% 0.41/0.79 === Backtracking. Learning clause 2053:4:22:[2051.0,2052.4,1910.1,1854.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ->
% 0.41/0.79 === Conflict found: 2053:4:22:[2051.0,2052.4,1910.1,1854.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv7_22r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20,x21),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) -> {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc46, x21 -> skc28}
% 0.41/0.79 === Backtracking. Learning clause 2054:3:21:[2053.3,706.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) ->
% 0.41/0.79 === Conflict found: 2054:3:21:[2053.3,706.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) -> {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc30}
% 0.41/0.79 === Backtracking. Learning clause 2055:4:14:[2054.3,567.1,527.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 2055:4:14:[2054.3,567.1,527.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc36}
% 0.41/0.79 === Backtracking. Learning clause 2056:3:13:[2055.1,274.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 2056:3:13:[2055.1,274.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv25_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc39}
% 0.41/0.79 === Backtracking. Learning clause 2057:1:4:[2056.2,248.1,116.1]:TopTopTopTop: -> ssPv25_4r1r1r1r1(x0,x1,x2,x3)
% 0.41/0.79 === Conflict found: 2054:3:21:[2053.3,706.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20) -> {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc30}
% 0.41/0.79 === Backtracking. Learning clause 2058:2:18:[2054.3,567.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ->
% 0.41/0.79 === Conflict found: 810:4:21:[547.20,55.0,509.19,790.2,456.18,791.3,422.17,792.4,405.16,793.5,344.15,794.6,301.14,795.7,261.13,796.8,224.12,797.9,212.11,798.10,201.10,799.11,191.9,800.12,182.8,801.13,160.7,802.14,141.6,803.15,125.5,804.17,112.4,805.19,108.3,806.20,105.2,807.21,103.1,808.22,1.0,809.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_21r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv24_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv25_4r1r1r1r1(x0,x1,x2,x3) -> ssPv19_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc46, x1 -> skc46, x2 -> skc46, x3 -> skc46, x4 -> skc46, x5 -> skc46, x6 -> skc46, x7 -> skc46, x8 -> skc46, x9 -> skc46, x10 -> skc46, x11 -> skc46, x12 -> skc46, x13 -> skc46, x14 -> skc46, x15 -> skc46, x16 -> skc46, x17 -> skc46, x18 -> skc46, x19 -> skc46, x20 -> skc30}
% 0.41/0.79
% 0.41/0.79 SZS status Unsatisfiable
% 0.41/0.79
% 0.41/0.79 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.41/0.79
% 0.41/0.79 SPASS-SCL-FOL Statistics:
% 0.41/0.79 Number of learned clauses: 59
% 0.41/0.79 Number of propagations: 521
% 0.41/0.79 Number of decisions: 354
% 0.41/0.79 Number of resolutions: 94
% 0.41/0.79 Number of condensations: 0
% 0.41/0.79 Number of sub resolutions: 1897
% 0.41/0.79 Number of input literals (deduplicated): 80
% 0.41/0.79 Number of grows: 1
% 0.41/0.79 Number of considered ground atoms: 41
% 0.41/0.79
% 0.41/0.79 Needed: 0:00:00.15
% 0.41/0.79
%------------------------------------------------------------------------------