%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN891-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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.38s 0.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN891-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n015.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:50:32 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.38/0.91 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.91 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.91 Execution resolution_2 ended with status: unsatisfiable
% 0.38/0.91 Used heuristic: resolution_2
% 0.38/0.91
% 0.38/0.91 Input Clauses:
% 0.38/0.91
% 0.38/0.91 Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv16_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv15_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv14_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv13_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssPv17_4r1r1r1r1 ssPv20_1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ssPv18_3r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv19_2r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv11_10r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv12_9r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1
% 0.38/0.91 Fol Constants: skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19 skc16 skc17
% 0.38/0.91 Fol Functions:
% 0.38/0.91 Problem Properties:
% 0.38/0.91 This is a Bernays Schoenfinkel problem.
% 0.38/0.91
% 0.38/0.91 After reduction: Problem Properties:
% 0.38/0.91 This is a Bernays Schoenfinkel problem.
% 0.38/0.91
% 0.38/0.91
% 0.38/0.91 Reduced Input Clauses:
% 0.38/0.91 87:1:1:[1.0,2.0]:Top: -> ssNder1_1r1(x0)
% 0.38/0.91 89:1:2:[87.1,3.0,1.0,88.1]:TopTop: -> ssNder1_2r1r1(x0,x1)
% 0.38/0.91 92:1:3:[89.2,4.0,87.1,90.1,1.0,91.2]:TopTopTop: -> ssNder1_3r1r1r1(x0,x1,x2)
% 0.38/0.91 96:1:4:[92.3,5.0,89.2,93.1,87.1,94.2,1.0,95.3]:TopTopTopTop: -> ssNder1_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 100:1:4:[92.3,6.0,89.2,97.1,87.1,98.2,1.0,99.3]:TopTopTopTop: -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc30)
% 0.38/0.91 104:1:4:[92.3,7.1,89.2,101.2,87.1,102.3,1.0,103.4]:TopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,skc31) ->
% 0.38/0.91 109:1:5:[96.4,8.0,92.3,105.1,89.2,106.2,87.1,107.3,1.0,108.4]:TopTopTopTopTop: -> ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.38/0.91 114:1:5:[96.4,9.0,92.3,110.1,89.2,111.2,87.1,112.3,1.0,113.4]:TopTopTopTopTop: -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28)
% 0.38/0.91 119:1:5:[96.4,10.1,92.3,115.2,89.2,116.3,87.1,117.4,1.0,118.5]:TopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29) ->
% 0.38/0.91 125:1:6:[109.5,11.0,96.4,120.1,92.3,121.2,89.2,122.3,87.1,123.4,1.0,124.5]:TopTopTopTopTopTop: -> ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 131:1:6:[109.5,12.0,96.4,126.1,92.3,127.2,89.2,128.3,87.1,129.4,1.0,130.5]:TopTopTopTopTopTop: -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26)
% 0.38/0.91 137:1:6:[109.5,13.1,96.4,132.2,92.3,133.3,89.2,134.4,87.1,135.5,1.0,136.6]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27) ->
% 0.38/0.91 144:1:7:[125.6,14.0,109.5,138.1,96.4,139.2,92.3,140.3,89.2,141.4,87.1,142.5,1.0,143.6]:TopTopTopTopTopTopTop: -> ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.38/0.91 151:1:7:[125.6,15.0,109.5,145.1,96.4,146.2,92.3,147.3,89.2,148.4,87.1,149.5,1.0,150.6]:TopTopTopTopTopTopTop: -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24)
% 0.38/0.91 158:1:7:[125.6,16.1,109.5,152.2,96.4,153.3,92.3,154.4,89.2,155.5,87.1,156.6,1.0,157.7]:TopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25) ->
% 0.38/0.91 166:1:8:[144.7,17.0,125.6,159.1,109.5,160.2,96.4,161.3,92.3,162.4,89.2,163.5,87.1,164.6,1.0,165.7]:TopTopTopTopTopTopTopTop: -> ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.38/0.91 173:4:7:[125.6,18.0,109.5,167.2,96.4,168.4,92.3,169.5,89.2,170.6,87.1,171.7,1.0,172.8]:TopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0)
% 0.38/0.91 182:1:9:[166.8,19.0,144.7,174.1,125.6,175.2,109.5,176.3,96.4,177.4,92.3,178.5,89.2,179.6,87.1,180.7,1.0,181.8]:TopTopTopTopTopTopTopTopTop: -> ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.38/0.91 192:1:10:[182.9,20.0,166.8,183.1,144.7,184.2,125.6,185.3,109.5,186.4,96.4,187.5,92.3,188.6,89.2,189.7,87.1,190.8,1.0,191.9]:TopTopTopTopTopTopTopTopTopTop: -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 0.38/0.91 203:1:11:[192.10,21.0,182.9,193.1,166.8,194.2,144.7,195.3,125.6,196.4,109.5,197.5,96.4,198.6,92.3,199.7,89.2,200.8,87.1,201.9,1.0,202.10]:TopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.38/0.91 215:1:12:[203.11,22.0,192.10,204.1,182.9,205.2,166.8,206.3,144.7,207.4,125.6,208.5,109.5,209.6,96.4,210.7,92.3,211.8,89.2,212.9,87.1,213.10,1.0,214.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.91 227:1:12:[203.11,23.0,192.10,216.1,182.9,217.2,166.8,218.3,144.7,219.4,125.6,220.5,109.5,221.6,96.4,222.7,92.3,223.8,89.2,224.9,87.1,225.10,1.0,226.11]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22)
% 0.38/0.91 239:1:12:[203.11,24.1,192.10,228.2,182.9,229.3,166.8,230.4,144.7,231.5,125.6,232.6,109.5,233.7,96.4,234.8,92.3,235.9,89.2,236.10,87.1,237.11,1.0,238.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23) ->
% 0.38/0.91 250:4:11:[192.10,25.0,182.9,240.1,166.8,241.2,144.7,242.3,125.6,243.4,109.5,244.5,96.4,245.6,92.3,246.7,89.2,247.8,87.1,248.10,1.0,249.11]:TopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 261:4:11:[192.10,26.0,182.9,251.1,166.8,252.2,144.7,253.4,125.6,254.6,109.5,255.7,96.4,256.8,92.3,257.10,89.2,258.11,87.1,259.12,1.0,260.13]:TopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 0.38/0.91 274:1:13:[215.12,27.0,203.11,262.1,192.10,263.2,182.9,264.3,166.8,265.4,144.7,266.5,125.6,267.6,109.5,268.7,96.4,269.8,92.3,270.9,89.2,271.10,87.1,272.11,1.0,273.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.91 287:1:13:[215.12,28.0,203.11,275.1,192.10,276.2,182.9,277.3,166.8,278.4,144.7,279.5,125.6,280.6,109.5,281.7,96.4,282.8,92.3,283.9,89.2,284.10,87.1,285.11,1.0,286.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20)
% 0.38/0.91 300:1:13:[215.12,29.1,203.11,288.2,192.10,289.3,182.9,290.4,166.8,291.5,144.7,292.6,125.6,293.7,109.5,294.8,96.4,295.9,92.3,296.10,89.2,297.11,87.1,298.12,1.0,299.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21) ->
% 0.38/0.91 312:4:12:[203.11,30.0,192.10,301.2,182.9,302.3,166.8,303.4,144.7,304.5,125.6,305.7,109.5,306.8,96.4,307.9,92.3,308.10,89.2,309.12,87.1,310.13,1.0,311.14]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.38/0.91 325:4:13:[215.12,31.0,203.11,313.1,192.10,314.2,182.9,315.3,166.8,316.4,144.7,317.5,125.6,318.6,109.5,319.7,96.4,320.8,92.3,321.9,89.2,322.10,87.1,323.11,1.0,324.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0)
% 0.38/0.91 339:1:14:[274.13,32.0,215.12,326.1,203.11,327.2,192.10,328.3,182.9,329.4,166.8,330.5,144.7,331.6,125.6,332.7,109.5,333.8,96.4,334.9,92.3,335.10,89.2,336.11,87.1,337.12,1.0,338.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.91 353:1:14:[274.13,33.0,215.12,340.1,203.11,341.2,192.10,342.3,182.9,343.4,166.8,344.5,144.7,345.6,125.6,346.7,109.5,347.8,96.4,348.9,92.3,349.10,89.2,350.11,87.1,351.12,1.0,352.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18)
% 0.38/0.91 367:1:14:[274.13,34.1,215.12,354.2,203.11,355.3,192.10,356.4,182.9,357.5,166.8,358.6,144.7,359.7,125.6,360.8,109.5,361.9,96.4,362.10,92.3,363.11,89.2,364.12,87.1,365.13,1.0,366.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19) ->
% 0.38/0.91 380:4:13:[215.12,35.0,203.11,368.2,192.10,369.3,182.9,370.4,166.8,371.5,144.7,372.6,125.6,373.7,109.5,374.8,96.4,375.9,92.3,376.10,89.2,377.11,87.1,378.13,1.0,379.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 0.38/0.91 395:1:15:[339.14,36.0,274.13,381.1,215.12,382.2,203.11,383.3,192.10,384.4,182.9,385.5,166.8,386.6,144.7,387.7,125.6,388.8,109.5,389.9,96.4,390.10,92.3,391.11,89.2,392.12,87.1,393.13,1.0,394.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.38/0.91 410:1:15:[339.14,37.0,274.13,396.1,215.12,397.2,203.11,398.3,192.10,399.4,182.9,400.5,166.8,401.6,144.7,402.7,125.6,403.8,109.5,404.9,96.4,405.10,92.3,406.11,89.2,407.12,87.1,408.13,1.0,409.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16)
% 0.38/0.91 423:4:13:[215.12,38.1,203.11,411.3,192.10,412.5,182.9,413.6,166.8,414.7,144.7,415.8,125.6,416.9,109.5,417.10,96.4,418.11,92.3,419.12,89.2,420.13,87.1,421.14,1.0,422.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 437:4:14:[274.13,39.0,215.12,424.1,203.11,425.2,192.10,426.3,182.9,427.4,166.8,428.5,144.7,429.6,125.6,430.7,109.5,431.8,96.4,432.9,92.3,433.10,89.2,434.11,87.1,435.12,1.0,436.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0)
% 0.38/0.91 450:4:13:[215.12,40.0,203.11,438.3,192.10,439.4,182.9,440.5,166.8,441.6,144.7,442.7,125.6,443.9,109.5,444.10,96.4,445.11,92.3,446.12,89.2,447.13,87.1,448.14,1.0,449.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.91 465:1:15:[339.14,41.1,274.13,451.2,215.12,452.3,203.11,453.4,192.10,454.5,182.9,455.6,166.8,456.7,144.7,457.8,125.6,458.9,109.5,459.10,96.4,460.11,92.3,461.12,89.2,462.13,87.1,463.14,1.0,464.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc17) ->
% 0.38/0.91 479:4:14:[274.13,42.0,215.12,466.1,203.11,467.2,192.10,468.3,182.9,469.4,166.8,470.5,144.7,471.6,125.6,472.7,109.5,473.8,96.4,474.9,92.3,475.11,89.2,476.12,87.1,477.13,1.0,478.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv20_1r1(x0)
% 0.38/0.91 493:4:14:[274.13,43.0,215.12,480.2,203.11,481.3,192.10,482.4,182.9,483.5,166.8,484.6,144.7,485.7,125.6,486.8,109.5,487.9,96.4,488.10,92.3,489.11,89.2,490.12,87.1,491.13,1.0,492.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv19_2r1r1(x0,x1)
% 0.38/0.91 507:4:14:[274.13,44.0,215.12,494.1,203.11,495.2,192.10,496.3,182.9,497.4,166.8,498.5,144.7,499.6,125.6,500.7,109.5,501.8,96.4,502.9,92.3,503.10,89.2,504.11,87.1,505.12,1.0,506.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 523:1:16:[395.15,45.0,339.14,508.1,274.13,509.2,215.12,510.3,203.11,511.4,192.10,512.5,182.9,513.6,166.8,514.7,144.7,515.8,125.6,516.9,109.5,517.10,96.4,518.11,92.3,519.12,89.2,520.13,87.1,521.14,1.0,522.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.38/0.91 537:4:14:[274.13,46.0,215.12,524.2,203.11,525.4,192.10,526.5,182.9,527.7,166.8,528.8,144.7,529.9,125.6,530.10,109.5,531.11,96.4,532.12,92.3,533.13,89.2,534.14,87.1,535.15,1.0,536.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.91 552:4:15:[339.14,47.0,274.13,538.1,215.12,539.2,203.11,540.3,192.10,541.4,182.9,542.5,166.8,543.6,144.7,544.7,125.6,545.8,109.5,546.9,96.4,547.11,92.3,548.12,89.2,549.13,87.1,550.15,1.0,551.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv20_1r1(x0) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.38/0.91 567:4:15:[339.14,48.0,274.13,553.2,215.12,554.3,203.11,555.4,192.10,556.5,182.9,557.7,166.8,558.9,144.7,559.10,125.6,560.11,109.5,561.12,96.4,562.13,92.3,563.14,89.2,564.15,87.1,565.16,1.0,566.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv20_1r1(x0)
% 0.38/0.91 582:4:15:[339.14,49.0,274.13,568.1,215.12,569.3,203.11,570.4,192.10,571.5,182.9,572.6,166.8,573.7,144.7,574.8,125.6,575.9,109.5,576.10,96.4,577.11,92.3,578.12,89.2,579.13,87.1,580.15,1.0,581.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv20_1r1(x0) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 597:4:15:[339.14,50.0,274.13,583.2,215.12,584.3,203.11,585.4,192.10,586.5,182.9,587.6,166.8,588.7,144.7,589.8,125.6,590.9,109.5,591.10,96.4,592.11,92.3,593.12,89.2,594.13,87.1,595.14,1.0,596.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 612:4:15:[339.14,51.0,274.13,598.2,215.12,599.3,203.11,600.4,192.10,601.6,182.9,602.7,166.8,603.9,144.7,604.10,125.6,605.11,109.5,606.12,96.4,607.13,92.3,608.14,89.2,609.15,87.1,610.17,1.0,611.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) ->
% 0.38/0.91 629:1:17:[523.16,52.0,395.15,613.1,339.14,614.2,274.13,615.3,215.12,616.4,203.11,617.5,192.10,618.6,182.9,619.7,166.8,620.8,144.7,621.9,125.6,622.10,109.5,623.11,96.4,624.12,92.3,625.13,89.2,626.14,87.1,627.15,1.0,628.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.38/0.91 645:4:16:[395.15,53.0,339.14,630.2,274.13,631.3,215.12,632.4,203.11,633.5,192.10,634.6,182.9,635.7,166.8,636.8,144.7,637.9,125.6,638.11,109.5,639.12,96.4,640.13,92.3,641.14,89.2,642.15,87.1,643.16,1.0,644.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.91 661:4:16:[395.15,54.0,339.14,646.2,274.13,647.3,215.12,648.4,203.11,649.5,192.10,650.6,182.9,651.7,166.8,652.8,144.7,653.9,125.6,654.11,109.5,655.12,96.4,656.13,92.3,657.14,89.2,658.15,87.1,659.16,1.0,660.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 677:4:16:[395.15,55.0,339.14,662.2,274.13,663.3,215.12,664.4,203.11,665.5,192.10,666.6,182.9,667.8,166.8,668.9,144.7,669.10,125.6,670.11,109.5,671.12,96.4,672.13,92.3,673.14,89.2,674.15,87.1,675.16,1.0,676.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 693:4:16:[395.15,56.0,339.14,678.2,274.13,679.3,215.12,680.4,203.11,681.5,192.10,682.7,182.9,683.8,166.8,684.9,144.7,685.10,125.6,686.11,109.5,687.12,96.4,688.13,92.3,689.14,89.2,690.15,87.1,691.16,1.0,692.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 709:4:16:[395.15,57.0,339.14,694.2,274.13,695.3,215.12,696.4,203.11,697.5,192.10,698.7,182.9,699.9,166.8,700.10,144.7,701.11,125.6,702.12,109.5,703.13,96.4,704.14,92.3,705.15,89.2,706.16,87.1,707.17,1.0,708.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.91 726:4:17:[523.16,58.0,395.15,710.1,339.14,711.2,274.13,712.3,215.12,713.4,203.11,714.5,192.10,715.6,182.9,716.7,166.8,717.8,144.7,718.9,125.6,719.10,109.5,720.11,96.4,721.12,92.3,722.13,89.2,723.15,87.1,724.16,1.0,725.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 744:1:18:[629.17,59.0,523.16,727.1,395.15,728.2,339.14,729.3,274.13,730.4,215.12,731.5,203.11,732.6,192.10,733.7,182.9,734.8,166.8,735.9,144.7,736.10,125.6,737.11,109.5,738.12,96.4,739.13,92.3,740.14,89.2,741.15,87.1,742.16,1.0,743.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.38/0.91 760:4:16:[395.15,60.0,339.14,745.1,274.13,746.2,215.12,747.3,203.11,748.5,192.10,749.6,182.9,750.7,166.8,751.8,144.7,752.9,125.6,753.10,109.5,754.11,96.4,755.12,92.3,756.13,89.2,757.14,87.1,758.15,1.0,759.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.91 776:4:16:[395.15,61.0,339.14,761.2,274.13,762.3,215.12,763.5,203.11,764.7,192.10,765.8,182.9,766.9,166.8,767.10,144.7,768.11,125.6,769.12,109.5,770.13,96.4,771.14,92.3,772.15,89.2,773.16,87.1,774.17,1.0,775.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.38/0.91 793:4:17:[523.16,62.0,395.15,777.2,339.14,778.3,274.13,779.4,215.12,780.5,203.11,781.6,192.10,782.8,182.9,783.9,166.8,784.10,144.7,785.11,125.6,786.12,109.5,787.13,96.4,788.14,92.3,789.15,89.2,790.16,87.1,791.17,1.0,792.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 810:4:17:[523.16,63.1,395.15,794.3,339.14,795.4,274.13,796.5,215.12,797.6,203.11,798.7,192.10,799.8,182.9,800.9,166.8,801.10,144.7,802.11,125.6,803.12,109.5,804.13,96.4,805.14,92.3,806.15,89.2,807.17,87.1,808.18,1.0,809.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv19_2r1r1(x0,x1) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 827:4:17:[523.16,64.0,395.15,811.2,339.14,812.3,274.13,813.4,215.12,814.5,203.11,815.6,192.10,816.7,182.9,817.8,166.8,818.9,144.7,819.10,125.6,820.11,109.5,821.12,96.4,822.13,92.3,823.14,89.2,824.15,87.1,825.16,1.0,826.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.91 845:4:18:[629.17,65.0,523.16,828.1,395.15,829.2,339.14,830.3,274.13,831.4,215.12,832.5,203.11,833.6,192.10,834.7,182.9,835.8,166.8,836.9,144.7,837.10,125.6,838.11,109.5,839.13,96.4,840.14,92.3,841.15,89.2,842.16,87.1,843.17,1.0,844.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.91 864:1:19:[744.18,66.0,629.17,846.1,523.16,847.2,395.15,848.3,339.14,849.4,274.13,850.5,215.12,851.6,203.11,852.7,192.10,853.8,182.9,854.9,166.8,855.10,144.7,856.11,125.6,857.12,109.5,858.13,96.4,859.14,92.3,860.15,89.2,861.16,87.1,862.17,1.0,863.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.38/0.91 882:4:18:[629.17,67.0,523.16,865.2,395.15,866.3,339.14,867.4,274.13,868.6,215.12,869.7,203.11,870.8,192.10,871.9,182.9,872.10,166.8,873.11,144.7,874.12,125.6,875.13,109.5,876.14,96.4,877.15,92.3,878.16,89.2,879.17,87.1,880.18,1.0,881.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1)
% 0.38/0.91 900:4:18:[629.17,68.0,523.16,883.2,395.15,884.3,339.14,885.4,274.13,886.5,215.12,887.6,203.11,888.7,192.10,889.8,182.9,890.9,166.8,891.10,144.7,892.11,125.6,893.13,109.5,894.14,96.4,895.15,92.3,896.16,89.2,897.17,87.1,898.18,1.0,899.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv20_1r1(x0)
% 0.38/0.91 918:4:18:[629.17,69.0,523.16,901.2,395.15,902.3,339.14,903.4,274.13,904.5,215.12,905.6,203.11,906.7,192.10,907.8,182.9,908.9,166.8,909.10,144.7,910.11,125.6,911.12,109.5,912.13,96.4,913.14,92.3,914.15,89.2,915.16,87.1,916.17,1.0,917.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 936:4:18:[629.17,70.0,523.16,919.2,395.15,920.3,339.14,921.4,274.13,922.6,215.12,923.7,203.11,924.8,192.10,925.9,182.9,926.10,166.8,927.11,144.7,928.12,125.6,929.13,109.5,930.14,96.4,931.15,92.3,932.16,89.2,933.18,87.1,934.19,1.0,935.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.91 954:4:18:[629.17,71.0,523.16,937.2,395.15,938.3,339.14,939.4,274.13,940.6,215.12,941.7,203.11,942.8,192.10,943.9,182.9,944.10,166.8,945.12,144.7,946.13,125.6,947.14,109.5,948.15,96.4,949.16,92.3,950.17,89.2,951.18,87.1,952.19,1.0,953.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8)
% 0.38/0.91 973:4:19:[744.18,72.0,629.17,955.2,523.16,956.3,395.15,957.4,339.14,958.5,274.13,959.6,215.12,960.7,203.11,961.8,192.10,962.9,182.9,963.10,166.8,964.11,144.7,965.13,125.6,966.14,109.5,967.15,96.4,968.16,92.3,969.17,89.2,970.18,87.1,971.19,1.0,972.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1)
% 0.38/0.91 992:4:19:[744.18,73.0,629.17,974.2,523.16,975.3,395.15,976.4,339.14,977.5,274.13,978.6,215.12,979.7,203.11,980.8,192.10,981.9,182.9,982.10,166.8,983.11,144.7,984.13,125.6,985.14,109.5,986.15,96.4,987.17,92.3,988.18,89.2,989.19,87.1,990.20,1.0,991.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.38/0.91 1011:4:19:[744.18,74.0,629.17,993.2,523.16,994.3,395.15,995.4,339.14,996.5,274.13,997.6,215.12,998.7,203.11,999.8,192.10,1000.9,182.9,1001.10,166.8,1002.11,144.7,1003.12,125.6,1004.14,109.5,1005.15,96.4,1006.16,92.3,1007.17,89.2,1008.19,87.1,1009.20,1.0,1010.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.91 1030:4:19:[744.18,75.0,629.17,1012.1,523.16,1013.2,395.15,1014.3,339.14,1015.4,274.13,1016.5,215.12,1017.6,203.11,1018.7,192.10,1019.8,182.9,1020.9,166.8,1021.10,144.7,1022.11,125.6,1023.12,109.5,1024.13,96.4,1025.14,92.3,1026.15,89.2,1027.17,87.1,1028.18,1.0,1029.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.38/0.91 1049:4:19:[744.18,76.0,629.17,1031.2,523.16,1032.4,395.15,1033.5,339.14,1034.6,274.13,1035.7,215.12,1036.8,203.11,1037.9,192.10,1038.10,182.9,1039.11,166.8,1040.12,144.7,1041.14,125.6,1042.15,109.5,1043.16,96.4,1044.17,92.3,1045.18,89.2,1046.19,87.1,1047.20,1.0,1048.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv20_1r1(x0)
% 0.38/0.91 1067:4:18:[629.17,77.1,523.16,1050.2,395.15,1051.4,339.14,1052.6,274.13,1053.7,215.12,1054.8,203.11,1055.9,192.10,1056.10,182.9,1057.11,166.8,1058.12,144.7,1059.13,125.6,1060.14,109.5,1061.15,96.4,1062.16,92.3,1063.17,89.2,1064.18,87.1,1065.19,1.0,1066.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 0.38/0.91 1086:4:19:[744.18,78.0,629.17,1068.1,523.16,1069.2,395.15,1070.4,339.14,1071.5,274.13,1072.6,215.12,1073.7,203.11,1074.8,192.10,1075.9,182.9,1076.10,166.8,1077.11,144.7,1078.12,125.6,1079.13,109.5,1080.14,96.4,1081.15,92.3,1082.16,89.2,1083.17,87.1,1084.18,1.0,1085.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 0.38/0.91 1105:4:19:[744.18,79.0,629.17,1087.2,523.16,1088.3,395.15,1089.4,339.14,1090.5,274.13,1091.6,215.12,1092.7,203.11,1093.8,192.10,1094.9,182.9,1095.10,166.8,1096.11,144.7,1097.12,125.6,1098.13,109.5,1099.14,96.4,1100.15,92.3,1101.16,89.2,1102.17,87.1,1103.18,1.0,1104.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 1124:4:19:[744.18,80.0,629.17,1106.2,523.16,1107.3,395.15,1108.4,339.14,1109.6,274.13,1110.7,215.12,1111.8,203.11,1112.9,192.10,1113.10,182.9,1114.11,166.8,1115.12,144.7,1116.13,125.6,1117.14,109.5,1118.15,96.4,1119.16,92.3,1120.17,89.2,1121.18,87.1,1122.19,1.0,1123.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.91 1144:4:20:[864.19,81.0,744.18,1125.2,629.17,1126.3,523.16,1127.4,395.15,1128.5,339.14,1129.7,274.13,1130.8,215.12,1131.9,203.11,1132.10,192.10,1133.11,182.9,1134.12,166.8,1135.13,144.7,1136.15,125.6,1137.16,109.5,1138.17,96.4,1139.18,92.3,1140.20,89.2,1141.21,87.1,1142.22,1.0,1143.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv18_3r1r1r1(x0,x1,x2) ->
% 0.38/0.91 1164:4:20:[864.19,82.0,744.18,1145.1,629.17,1146.2,523.16,1147.3,395.15,1148.4,339.14,1149.5,274.13,1150.6,215.12,1151.7,203.11,1152.8,192.10,1153.9,182.9,1154.10,166.8,1155.12,144.7,1156.13,125.6,1157.14,109.5,1158.15,96.4,1159.16,92.3,1160.18,89.2,1161.19,87.1,1162.20,1.0,1163.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.38/0.91 1184:4:20:[864.19,83.0,744.18,1165.1,629.17,1166.2,523.16,1167.3,395.15,1168.4,339.14,1169.5,274.13,1170.6,215.12,1171.7,203.11,1172.8,192.10,1173.9,182.9,1174.10,166.8,1175.11,144.7,1176.13,125.6,1177.14,109.5,1178.16,96.4,1179.17,92.3,1180.18,89.2,1181.19,87.1,1182.20,1.0,1183.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.38/0.91 1204:4:20:[864.19,84.0,744.18,1185.2,629.17,1186.3,523.16,1187.4,395.15,1188.5,339.14,1189.6,274.13,1190.7,215.12,1191.8,203.11,1192.9,192.10,1193.10,182.9,1194.11,166.8,1195.12,144.7,1196.14,125.6,1197.16,109.5,1198.17,96.4,1199.18,92.3,1200.19,89.2,1201.20,87.1,1202.21,1.0,1203.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 0.38/0.91 1224:4:20:[864.19,85.0,744.18,1205.1,629.17,1206.2,523.16,1207.3,395.15,1208.5,339.14,1209.6,274.13,1210.7,215.12,1211.8,203.11,1212.9,192.10,1213.10,182.9,1214.12,166.8,1215.14,144.7,1216.15,125.6,1217.16,109.5,1218.17,96.4,1219.18,92.3,1220.19,89.2,1221.20,87.1,1222.21,1.0,1223.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.38/0.91 1244:4:20:[864.19,86.0,744.18,1225.2,629.17,1226.4,523.16,1227.5,395.15,1228.6,339.14,1229.8,274.13,1230.9,215.12,1231.10,203.11,1232.11,192.10,1233.12,182.9,1234.13,166.8,1235.15,144.7,1236.16,125.6,1237.17,109.5,1238.18,96.4,1239.19,92.3,1240.20,89.2,1241.21,87.1,1242.22,1.0,1243.23]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ->
% 0.38/0.91
% 0.38/0.91 Most General Atoms: ssNder1_0 ssNder1_1r1(x0) ssNder1_2r1r1(x0,x1) ssNder1_3r1r1r1(x0,x1,x2) ssNder1_4r1r1r1r1(x0,x1,x2,x3) ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv17_4r1r1r1r1(x0,x1,x2,x3) ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssPv20_1r1(x0) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv18_3r1r1r1(x0,x1,x2) ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ssPv19_2r1r1(x0,x1) ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssPv8_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) ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19)
% 0.38/0.91
% 0.38/0.91 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: resolution_2 ===
% 0.38/0.91
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 56
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 1184:4:20:[864.19,83.0,744.18,1165.1,629.17,1166.2,523.16,1167.3,395.15,1168.4,339.14,1169.5,274.13,1170.6,215.12,1171.7,203.11,1172.8,192.10,1173.9,182.9,1174.10,166.8,1175.11,144.7,1176.13,125.6,1177.14,109.5,1178.16,96.4,1179.17,92.3,1180.18,89.2,1181.19,87.1,1182.20,1.0,1183.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1245:3:19:[1184.2,100.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.38/0.91 === Conflict found: 845:4:18:[629.17,65.0,523.16,828.1,395.15,829.2,339.14,830.3,274.13,831.4,215.12,832.5,203.11,833.6,192.10,834.7,182.9,835.8,166.8,836.9,144.7,837.10,125.6,838.11,109.5,839.13,96.4,840.14,92.3,841.15,89.2,842.16,87.1,843.17,1.0,844.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1246:3:17:[845.1,100.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 63
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 1086:4:19:[744.18,78.0,629.17,1068.1,523.16,1069.2,395.15,1070.4,339.14,1071.5,274.13,1072.6,215.12,1073.7,203.11,1074.8,192.10,1075.9,182.9,1076.10,166.8,1077.11,144.7,1078.12,125.6,1079.13,109.5,1080.14,96.4,1081.15,92.3,1082.16,89.2,1083.17,87.1,1084.18,1.0,1085.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1247:5:14:[1086.4,104.1,1011.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4),ssPv19_2r1r1(x0,x1) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.91 === Conflict found: 312:4:12:[203.11,30.0,192.10,301.2,182.9,302.3,166.8,303.4,144.7,304.5,125.6,305.7,109.5,306.8,96.4,307.9,92.3,308.10,89.2,309.12,87.1,310.13,1.0,311.14]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1248:3:11:[312.4,104.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4),ssPv19_2r1r1(x0,x1) ->
% 0.38/0.91 === Conflict found: 1246:3:17:[845.1,100.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1249:6:30:[1246.1,954.1,645.2,567.2,325.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x19,x20,x21,x22,x23,x24) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x25,x26,x27,x28,x29),ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 77
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 1204:4:20:[864.19,84.0,744.18,1185.2,629.17,1186.3,523.16,1187.4,395.15,1188.5,339.14,1189.6,274.13,1190.7,215.12,1191.8,203.11,1192.9,192.10,1193.10,182.9,1194.11,166.8,1195.12,144.7,1196.14,125.6,1197.16,109.5,1198.17,96.4,1199.18,92.3,1200.19,89.2,1201.20,87.1,1202.21,1.0,1203.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1250:3:19:[1204.3,114.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.38/0.91 === Conflict found: 900:4:18:[629.17,68.0,523.16,883.2,395.15,884.3,339.14,885.4,274.13,886.5,215.12,887.6,203.11,888.7,192.10,889.8,182.9,890.9,166.8,891.10,144.7,892.11,125.6,893.13,109.5,894.14,96.4,895.15,92.3,896.16,89.2,897.17,87.1,898.18,1.0,899.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1251:3:17:[900.2,114.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 261:4:11:[192.10,26.0,182.9,251.1,166.8,252.2,144.7,253.4,125.6,254.6,109.5,255.7,96.4,256.8,92.3,257.10,89.2,258.11,87.1,259.12,1.0,260.13]:TopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1252:3:10:[261.2,114.1]:TopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9)
% 0.38/0.91 === Conflict found: 1248:3:11:[312.4,104.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc28, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1253:2:10:[1248.2,114.1]:TopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,skc28,x4,x5,x6,x7,x8,x9),ssPv19_2r1r1(x0,x1) ->
% 0.38/0.91 === Conflict found: 1245:3:19:[1184.2,100.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc31}
% 0.38/0.91 === Backtracking. Learning clause 1254:3:16:[1245.2,1204.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 90
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 1030:4:19:[744.18,75.0,629.17,1012.1,523.16,1013.2,395.15,1014.3,339.14,1015.4,274.13,1016.5,215.12,1017.6,203.11,1018.7,192.10,1019.8,182.9,1020.9,166.8,1021.10,144.7,1022.11,125.6,1023.12,109.5,1024.13,96.4,1025.14,92.3,1026.15,89.2,1027.17,87.1,1028.18,1.0,1029.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1255:6:16:[1030.2,1049.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 423:4:13:[215.12,38.1,203.11,411.3,192.10,412.5,182.9,413.6,166.8,414.7,144.7,415.8,125.6,416.9,109.5,417.10,96.4,418.11,92.3,419.12,89.2,420.13,87.1,421.14,1.0,422.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1256:3:12:[423.4,119.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8) ->
% 0.38/0.91 === Conflict found: 173:4:7:[125.6,18.0,109.5,167.2,96.4,168.4,92.3,169.5,89.2,170.6,87.1,171.7,1.0,172.8]:TopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1257:3:6:[173.3,119.1]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 1246:3:17:[845.1,100.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc29, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1258:2:16:[1246.2,119.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 154
% 0.38/0.91 === Conflict found: 423:4:13:[215.12,38.1,203.11,411.3,192.10,412.5,182.9,413.6,166.8,414.7,144.7,415.8,125.6,416.9,109.5,417.10,96.4,418.11,92.3,419.12,89.2,420.13,87.1,421.14,1.0,422.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1259:6:19:[423.2,479.2,1105.3,1011.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv18_3r1r1r1(x0,x1,x2),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv19_2r1r1(x0,x1) -> ssPv20_1r1(x0),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 161
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 1049:4:19:[744.18,76.0,629.17,1031.2,523.16,1032.4,395.15,1033.5,339.14,1034.6,274.13,1035.7,215.12,1036.8,203.11,1037.9,192.10,1038.10,182.9,1039.11,166.8,1040.12,144.7,1041.14,125.6,1042.15,109.5,1043.16,96.4,1044.17,92.3,1045.18,89.2,1046.19,87.1,1047.20,1.0,1048.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1260:3:18:[1049.3,131.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc26,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 261:4:11:[192.10,26.0,182.9,251.1,166.8,252.2,144.7,253.4,125.6,254.6,109.5,255.7,96.4,256.8,92.3,257.10,89.2,258.11,87.1,259.12,1.0,260.13]:TopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1261:2:9:[261.1,131.1,114.1]:TopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,skc26,x5,x6,x7,x8)
% 0.38/0.91 === Conflict found: 1245:3:19:[1184.2,100.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc28, x5 -> skc26, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1262:2:18:[1245.1,131.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc26,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,skc26,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 166
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 726:4:17:[523.16,58.0,395.15,710.1,339.14,711.2,274.13,712.3,215.12,713.4,203.11,714.5,192.10,715.6,182.9,716.7,166.8,717.8,144.7,718.9,125.6,719.10,109.5,720.11,96.4,721.12,92.3,722.13,89.2,723.15,87.1,724.16,1.0,725.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1263:3:16:[726.3,137.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 === Conflict found: 507:4:14:[274.13,44.0,215.12,494.1,203.11,495.2,192.10,496.3,182.9,497.4,166.8,498.5,144.7,499.6,125.6,500.7,109.5,501.8,96.4,502.9,92.3,503.10,89.2,504.11,87.1,505.12,1.0,506.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1264:3:13:[507.3,137.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 === Conflict found: 380:4:13:[215.12,35.0,203.11,368.2,192.10,369.3,182.9,370.4,166.8,371.5,144.7,372.6,125.6,373.7,109.5,374.8,96.4,375.9,92.3,376.10,89.2,377.11,87.1,378.13,1.0,379.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1265:3:12:[380.4,137.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11),ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9)
% 0.38/0.91 === Conflict found: 450:4:13:[215.12,40.0,203.11,438.3,192.10,439.4,182.9,440.5,166.8,441.6,144.7,442.7,125.6,443.9,109.5,444.10,96.4,445.11,92.3,446.12,89.2,447.13,87.1,448.14,1.0,449.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1266:4:16:[450.1,760.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 175
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 1224:4:20:[864.19,85.0,744.18,1205.1,629.17,1206.2,523.16,1207.3,395.15,1208.5,339.14,1209.6,274.13,1210.7,215.12,1211.8,203.11,1212.9,192.10,1213.10,182.9,1214.12,166.8,1215.14,144.7,1216.15,125.6,1217.16,109.5,1218.17,96.4,1219.18,92.3,1220.19,89.2,1221.20,87.1,1222.21,1.0,1223.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1267:3:19:[1224.3,151.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 0.38/0.91 === Conflict found: 450:4:13:[215.12,40.0,203.11,438.3,192.10,439.4,182.9,440.5,166.8,441.6,144.7,442.7,125.6,443.9,109.5,444.10,96.4,445.11,92.3,446.12,89.2,447.13,87.1,448.14,1.0,449.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 0.38/0.91 === Backtracking. Learning clause 1268:6:26:[450.4,776.2,380.3,1254.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x12,x13),ssPv20_1r1(x0),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x12,x13,x14,x15),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25)
% 0.38/0.91 === Conflict found: 645:4:16:[395.15,53.0,339.14,630.2,274.13,631.3,215.12,632.4,203.11,633.5,192.10,634.6,182.9,635.7,166.8,636.8,144.7,637.9,125.6,638.11,109.5,639.12,96.4,640.13,92.3,641.14,89.2,642.15,87.1,643.16,1.0,644.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1269:5:16:[645.3,709.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv18_3r1r1r1(x0,x1,x2),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 182
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 1030:4:19:[744.18,75.0,629.17,1012.1,523.16,1013.2,395.15,1014.3,339.14,1015.4,274.13,1016.5,215.12,1017.6,203.11,1018.7,192.10,1019.8,182.9,1020.9,166.8,1021.10,144.7,1022.11,125.6,1023.12,109.5,1024.13,96.4,1025.14,92.3,1026.15,89.2,1027.17,87.1,1028.18,1.0,1029.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1270:3:18:[1030.4,158.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11,x12)
% 0.38/0.91 === Conflict found: 793:4:17:[523.16,62.0,395.15,777.2,339.14,778.3,274.13,779.4,215.12,780.5,203.11,781.6,192.10,782.8,182.9,783.9,166.8,784.10,144.7,785.11,125.6,786.12,109.5,787.13,96.4,788.14,92.3,789.15,89.2,790.16,87.1,791.17,1.0,792.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1271:3:16:[793.3,158.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 === Conflict found: 250:4:11:[192.10,25.0,182.9,240.1,166.8,241.2,144.7,242.3,125.6,243.4,109.5,244.5,96.4,245.6,92.3,246.7,89.2,247.8,87.1,248.10,1.0,249.11]:TopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1272:3:10:[250.3,158.1]:TopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 0.38/0.91 === Conflict found: 1011:4:19:[744.18,74.0,629.17,993.2,523.16,994.3,395.15,995.4,339.14,996.5,274.13,997.6,215.12,998.7,203.11,999.8,192.10,1000.9,182.9,1001.10,166.8,1002.11,144.7,1003.12,125.6,1004.14,109.5,1005.15,96.4,1006.16,92.3,1007.17,89.2,1008.19,87.1,1009.20,1.0,1010.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1274:5:21:[137.0,1273.3,1011.1,1270.2,493.4,507.1,1265.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x13,x14,x15,x16,skc27,x17,x18,x19,x20)
% 0.38/0.91 === Conflict found: 1030:4:19:[744.18,75.0,629.17,1012.1,523.16,1013.2,395.15,1014.3,339.14,1015.4,274.13,1016.5,215.12,1017.6,203.11,1018.7,192.10,1019.8,182.9,1020.9,166.8,1021.10,144.7,1022.11,125.6,1023.12,109.5,1024.13,96.4,1025.14,92.3,1026.15,89.2,1027.17,87.1,1028.18,1.0,1029.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc25, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1275:4:14:[1030.2,1011.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.91 === Conflict found: 450:4:13:[215.12,40.0,203.11,438.3,192.10,439.4,182.9,440.5,166.8,441.6,144.7,442.7,125.6,443.9,109.5,444.10,96.4,445.11,92.3,446.12,89.2,447.13,87.1,448.14,1.0,449.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 0.38/0.91 === Backtracking. Learning clause 1276:5:17:[450.4,776.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x13,x14,x15,x16)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 246
% 0.38/0.91 === Conflict found: 827:4:17:[523.16,64.0,395.15,811.2,339.14,812.3,274.13,813.4,215.12,814.5,203.11,815.6,192.10,816.7,182.9,817.8,166.8,818.9,144.7,819.10,125.6,820.11,109.5,821.12,96.4,822.13,92.3,823.14,89.2,824.15,87.1,825.16,1.0,826.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1277:6:17:[827.1,552.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv20_1r1(x0) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 259
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 918:4:18:[629.17,69.0,523.16,901.2,395.15,902.3,339.14,903.4,274.13,904.5,215.12,905.6,203.11,906.7,192.10,907.8,182.9,908.9,166.8,909.10,144.7,910.11,125.6,911.12,109.5,912.13,96.4,913.14,92.3,914.15,89.2,915.16,87.1,916.17,1.0,917.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1278:3:17:[918.4,119.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7)
% 0.38/0.91 === Conflict found: 552:4:15:[339.14,47.0,274.13,538.1,215.12,539.2,203.11,540.3,192.10,541.4,182.9,542.5,166.8,543.6,144.7,544.7,125.6,545.8,109.5,546.9,96.4,547.11,92.3,548.12,89.2,549.13,87.1,550.15,1.0,551.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv20_1r1(x0) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc19}
% 0.38/0.91 === Backtracking. Learning clause 1279:4:11:[552.3,1276.3,367.1,465.1,227.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv20_1r1(x0),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ->
% 0.38/0.91 === Conflict found: 612:4:15:[339.14,51.0,274.13,598.2,215.12,599.3,203.11,600.4,192.10,601.6,182.9,602.7,166.8,603.9,144.7,604.10,125.6,605.11,109.5,606.12,96.4,607.13,92.3,608.14,89.2,609.15,87.1,610.17,1.0,611.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1280:4:14:[612.1,582.3,250.3,119.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10),ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x11,x12,x13)
% 0.38/0.91 === Conflict found: 493:4:14:[274.13,43.0,215.12,480.2,203.11,481.3,192.10,482.4,182.9,483.5,166.8,484.6,144.7,485.7,125.6,486.8,109.5,487.9,96.4,488.10,92.3,489.11,89.2,490.12,87.1,491.13,1.0,492.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1282:4:10:[137.0,1281.3,493.2,1265.1,507.1]:TopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv19_2r1r1(x0,x1),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 === Conflict found: 423:4:13:[215.12,38.1,203.11,411.3,192.10,412.5,182.9,413.6,166.8,414.7,144.7,415.8,125.6,416.9,109.5,417.10,96.4,418.11,92.3,419.12,89.2,420.13,87.1,421.14,1.0,422.15]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 0.38/0.91 === Backtracking. Learning clause 1283:2:11:[423.2,227.1,119.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8) ->
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 264
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 1249:6:30:[1246.1,954.1,645.2,567.2,325.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x12,x13,x14,x15,x16,x17,x18),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x19,x20,x21,x22,x23,x24) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x25,x26,x27,x28,x29),ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc23, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30, x20 -> skc30, x21 -> skc30, x22 -> skc30, x23 -> skc30, x24 -> skc30, x25 -> skc30, x26 -> skc30, x27 -> skc30, x28 -> skc30, x29 -> skc23}
% 0.38/0.91 === Backtracking. Learning clause 1284:6:19:[1249.4,239.1,693.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x12,x13,x14,x15,x16,x17,x18),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x12) -> ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 === Conflict found: 677:4:16:[395.15,55.0,339.14,662.2,274.13,663.3,215.12,664.4,203.11,665.5,192.10,666.6,182.9,667.8,166.8,668.9,144.7,669.10,125.6,670.11,109.5,671.12,96.4,672.13,92.3,673.14,89.2,674.15,87.1,675.16,1.0,676.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1285:3:15:[677.3,239.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 === Conflict found: 537:4:14:[274.13,46.0,215.12,524.2,203.11,525.4,192.10,526.5,182.9,527.7,166.8,528.8,144.7,529.9,125.6,530.10,109.5,531.11,96.4,532.12,92.3,533.13,89.2,534.14,87.1,535.15,1.0,536.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1286:3:13:[537.4,239.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ->
% 0.38/0.91 === Conflict found: 325:4:13:[215.12,31.0,203.11,313.1,192.10,314.2,182.9,315.3,166.8,316.4,144.7,317.5,125.6,318.6,109.5,319.7,96.4,320.8,92.3,321.9,89.2,322.10,87.1,323.11,1.0,324.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23}
% 0.38/0.91 === Backtracking. Learning clause 1287:3:8:[325.1,239.1]:TopTopTopTopTopTopTopTop: -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv18_3r1r1r1(x0,x1,x2),ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 882:4:18:[629.17,67.0,523.16,865.2,395.15,866.3,339.14,867.4,274.13,868.6,215.12,869.7,203.11,870.8,192.10,871.9,182.9,872.10,166.8,873.11,144.7,874.12,125.6,875.13,109.5,876.14,96.4,877.15,92.3,878.16,89.2,879.17,87.1,880.18,1.0,881.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1288:3:10:[882.3,137.1,1258.1]:TopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc29,skc27,x4,x5,x6,x7,x8,x9) -> ssPv19_2r1r1(x0,x1),ssPv18_3r1r1r1(x0,x1,x2)
% 0.38/0.91 === Conflict found: 1275:4:14:[1030.2,1011.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc28, x13 -> skc21}
% 0.38/0.91 === Backtracking. Learning clause 1289:3:8:[1275.4,300.1]:TopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 0.38/0.91 === Conflict found: 612:4:15:[339.14,51.0,274.13,598.2,215.12,599.3,203.11,600.4,192.10,601.6,182.9,602.7,166.8,603.9,144.7,604.10,125.6,605.11,109.5,606.12,96.4,607.13,92.3,608.14,89.2,609.15,87.1,610.17,1.0,611.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1290:5:14:[612.2,1247.4,1289.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4),ssPv19_2r1r1(x0,x1) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 271
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 537:4:14:[274.13,46.0,215.12,524.2,203.11,525.4,192.10,526.5,182.9,527.7,166.8,528.8,144.7,529.9,125.6,530.10,109.5,531.11,96.4,532.12,92.3,533.13,89.2,534.14,87.1,535.15,1.0,536.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc20}
% 0.38/0.91 === Backtracking. Learning clause 1291:2:11:[537.1,287.1,239.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ->
% 0.38/0.91 === Conflict found: 1257:3:6:[173.3,119.1]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc26}
% 0.38/0.91 === Backtracking. Learning clause 1292:6:27:[1257.1,131.1,1279.2,493.3,1289.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv15_6r1r1r1r1r1r1(x0,x1,x21,x22,x23,x24) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x21,x22,x23,x24,x25,x26)
% 0.38/0.91 === Conflict found: 1279:4:11:[552.3,1276.3,367.1,465.1,227.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv20_1r1(x0),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1293:3:14:[1279.3,114.1,1252.3,1288.3,131.1,227.1,1257.3,131.1,493.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1)
% 0.38/0.91 === Conflict found: 810:4:17:[523.16,63.1,395.15,794.3,339.14,795.4,274.13,796.5,215.12,797.6,203.11,798.7,192.10,799.8,182.9,800.9,166.8,801.10,144.7,802.11,125.6,803.12,109.5,804.13,96.4,805.14,92.3,806.15,89.2,807.17,87.1,808.18,1.0,809.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv19_2r1r1(x0,x1) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc20, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1295:6:13:[1293.2,1294.3,810.2,1245.3,760.2,1144.1,726.3,810.2,760.2]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4)
% 0.38/0.91 === Clause set with instances from active satisfied. Growing active. New size: 282
% 0.38/0.91 === Restarting.
% 0.38/0.91 === Conflict found: 597:4:15:[339.14,50.0,274.13,583.2,215.12,584.3,203.11,585.4,192.10,586.5,182.9,587.6,166.8,588.7,144.7,589.8,125.6,590.9,109.5,591.10,96.4,592.11,92.3,593.12,89.2,594.13,87.1,595.14,1.0,596.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18}
% 0.38/0.91 === Backtracking. Learning clause 1296:3:12:[597.1,353.1]:TopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 === Conflict found: 1257:3:6:[173.3,119.1]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc26}
% 0.38/0.91 === Backtracking. Learning clause 1297:2:11:[1257.1,131.1,1296.3,104.1]:TopTopTopTopTopTopTopTopTopTopTop: -> ssPv20_1r1(x0),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10)
% 0.38/0.91 === Conflict found: 567:4:15:[339.14,48.0,274.13,553.2,215.12,554.3,203.11,555.4,192.10,556.5,182.9,557.7,166.8,558.9,144.7,559.10,125.6,560.11,109.5,561.12,96.4,562.13,92.3,563.14,89.2,564.15,87.1,565.16,1.0,566.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18}
% 0.38/0.91 === Backtracking. Learning clause 1298:3:9:[567.1,353.1]:TopTopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 1224:4:20:[864.19,85.0,744.18,1205.1,629.17,1206.2,523.16,1207.3,395.15,1208.5,339.14,1209.6,274.13,1210.7,215.12,1211.8,203.11,1212.9,192.10,1213.10,182.9,1214.12,166.8,1215.14,144.7,1216.15,125.6,1217.16,109.5,1218.17,96.4,1219.18,92.3,1220.19,89.2,1221.20,87.1,1222.21,1.0,1223.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 0.38/0.91 === Backtracking. Learning clause 1299:2:18:[1224.1,353.1,151.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,skc18,x13,x14,x15,x16,x17)
% 0.38/0.91 === Conflict found: 567:4:15:[339.14,48.0,274.13,553.2,215.12,554.3,203.11,555.4,192.10,556.5,182.9,557.7,166.8,558.9,144.7,559.10,125.6,560.11,109.5,561.12,96.4,562.13,92.3,563.14,89.2,564.15,87.1,565.16,1.0,566.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc18}
% 0.38/0.91 === Backtracking. Learning clause 1300:3:14:[567.3,151.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7) -> ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 1289:3:8:[1275.4,300.1]:TopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc25}
% 0.38/0.91 === Backtracking. Learning clause 1301:2:6:[1289.3,158.1]:TopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) ->
% 0.38/0.91 === Conflict found: 1301:2:6:[1289.3,158.1]:TopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv19_2r1r1(x0,x1) -> {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28}
% 0.38/0.91 === Backtracking. Learning clause 1302:1:2:[1301.1,114.1]:TopTop: ssPv19_2r1r1(x0,x1) ->
% 0.38/0.91 === Conflict found: 1292:6:27:[1257.1,131.1,1279.2,493.3,1289.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x11,x12,x13,x14,x15,x16,x17,x18,x19,x20),ssPv15_6r1r1r1r1r1r1(x0,x1,x21,x22,x23,x24) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x21,x22,x23,x24,x25,x26) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc23, x20 -> skc20, x21 -> skc30, x22 -> skc30, x23 -> skc30, x24 -> skc30, x25 -> skc30, x26 -> skc25}
% 0.38/0.91 === Backtracking. Learning clause 1304:2:13:[114.0,1303.0,1292.3,287.1,1261.2,1287.2,158.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 1304:2:13:[114.0,1303.0,1292.3,287.1,1261.2,1287.2,158.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23}
% 0.38/0.91 === Backtracking. Learning clause 1305:1:1:[1304.1,239.1]:Top: -> ssPv20_1r1(x0)
% 0.38/0.91 === Conflict found: 493:4:14:[274.13,43.0,215.12,480.2,203.11,481.3,192.10,482.4,182.9,483.5,166.8,484.6,144.7,485.7,125.6,486.8,109.5,487.9,96.4,488.10,92.3,489.11,89.2,490.12,87.1,491.13,1.0,492.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc20}
% 0.38/0.91 === Backtracking. Learning clause 1307:2:13:[1302.0,1306.2,493.1,287.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 0.38/0.91 === Conflict found: 1293:3:14:[1279.3,114.1,1252.3,1288.3,131.1,227.1,1257.3,131.1,493.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc20}
% 0.38/0.91
% 0.38/0.91 SZS status Unsatisfiable
% 0.38/0.91
% 0.38/0.91 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.38/0.91
% 0.38/0.91 SPASS-SCL-FOL Statistics:
% 0.38/0.91 Number of learned clauses: 58
% 0.38/0.91 Number of propagations: 2276
% 0.38/0.91 Number of decisions: 908
% 0.38/0.91 Number of resolutions: 105
% 0.38/0.91 Number of condensations: 7
% 0.38/0.91 Number of sub resolutions: 1163
% 0.38/0.91 Number of input literals (deduplicated): 56
% 0.38/0.91 Number of grows: 14
% 0.38/0.91 Number of considered ground atoms: 282
% 0.38/0.91
% 0.38/0.91 Needed: 0:00:00.33
% 0.38/0.91
%------------------------------------------------------------------------------