SPASS-SCL---0.1.UNS-Ass.s

%------------------------------------------------------------------------------
% File     : SPASS-SCL---0.1
% Problem  : SYN890-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm  : none
% Format   : tptp
% Command  : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n009.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu May  7 07:40:22 PM UTC 2026

% Result   : Unsatisfiable 16.86s 4.02s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.15  % Problem  : SYN890-1 : TPTP v9.2.1. Released v2.5.0.
% 0.10/0.16  % Command  : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.37  % Computer : n009.cluster.edu
% 0.18/0.37  % Model    : x86_64 x86_64
% 0.18/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.37  % Memory   : 8042.1875MB
% 0.18/0.37  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.18/0.37  % CPULimit : 300
% 0.18/0.37  % WCLimit  : 300
% 0.18/0.37  % DateTime : Thu May  7 13:50:11 EDT 2026
% 0.18/0.37  % CPUTime  : 
% 0.18/0.37  SPASS-SCL-FOL version:
% 0.30/0.47  SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 16.86/4.02  Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.86/4.02  Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.86/4.02  Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.86/4.02  Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.86/4.02  Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.86/4.02  Execution resolution_2 ended with status: unsatisfiable
% 16.86/4.02  Used heuristic: resolution_2
% 16.86/4.02  
% 16.86/4.02   Input Clauses:
% 16.86/4.02  
% 16.86/4.02   Predicates: ssNder1_0 ssNder1_1r1 ssNder1_2r1r1 ssNder1_3r1r1r1 ssNder1_4r1r1r1r1 ssPv16_5r1r1r1r1r1 ssNder1_5r1r1r1r1r1 ssPv15_6r1r1r1r1r1r1 ssNder1_6r1r1r1r1r1r1 ssPv14_7r1r1r1r1r1r1r1 ssNder1_7r1r1r1r1r1r1r1 ssPv13_8r1r1r1r1r1r1r1r1 ssNder1_8r1r1r1r1r1r1r1r1 ssPv19_2r1r1 ssPv17_4r1r1r1r1 ssNder1_9r1r1r1r1r1r1r1r1r1 ssPv20_1r1 ssNder1_10r1r1r1r1r1r1r1r1r1r1 ssPv12_9r1r1r1r1r1r1r1r1r1 ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ssPv11_10r1r1r1r1r1r1r1r1r1r1 ssPv18_3r1r1r1 ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 
% 16.86/4.02   Fol Constants: skc30 skc31 skc28 skc29 skc26 skc27 skc24 skc25 skc22 skc23 skc20 skc21 skc18 skc19 skc16 skc17 
% 16.86/4.02   Fol Functions: 
% 16.86/4.02   Problem Properties:
% 16.86/4.02   This is a Bernays Schoenfinkel problem.
% 16.86/4.02  
% 16.86/4.02   After reduction:  Problem Properties:
% 16.86/4.02   This is a Bernays Schoenfinkel problem.
% 16.86/4.02  
% 16.86/4.02  
% 16.86/4.02   Reduced Input Clauses:
% 16.86/4.02  87:1:1:[1.0,2.0]:Top:  -> ssNder1_1r1(x0)
% 16.86/4.02  89:1:2:[87.1,3.0,1.0,88.1]:TopTop:  -> ssNder1_2r1r1(x0,x1)
% 16.86/4.02  92:1:3:[89.2,4.0,87.1,90.1,1.0,91.2]:TopTopTop:  -> ssNder1_3r1r1r1(x0,x1,x2)
% 16.86/4.02  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)
% 16.86/4.02  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)
% 16.86/4.02  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) -> 
% 16.86/4.02  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)
% 16.86/4.02  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)
% 16.86/4.02  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) -> 
% 16.86/4.02  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)
% 16.86/4.02  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)
% 16.86/4.02  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) -> 
% 16.86/4.02  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)
% 16.86/4.02  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)
% 16.86/4.02  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) -> 
% 16.86/4.02  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)
% 16.86/4.02  173:4:7:[125.6,18.0,109.5,167.2,96.4,168.3,92.3,169.4,89.2,170.6,87.1,171.7,1.0,172.8]:TopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 16.86/4.02  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)
% 16.86/4.02  190:4:8:[144.7,20.0,125.6,183.2,109.5,184.3,96.4,185.4,92.3,186.5,89.2,187.6,87.1,188.7,1.0,189.8]:TopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1),ssPv20_1r1(x0)
% 16.86/4.02  200:1:10:[182.9,21.0,166.8,191.1,144.7,192.2,125.6,193.3,109.5,194.4,96.4,195.5,92.3,196.6,89.2,197.7,87.1,198.8,1.0,199.9]:TopTopTopTopTopTopTopTopTopTop:  -> ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 16.86/4.02  209:4:9:[166.8,22.0,144.7,201.2,125.6,202.4,109.5,203.6,96.4,204.7,92.3,205.8,89.2,206.9,87.1,207.11,1.0,208.12]:TopTopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> 
% 16.86/4.02  218:4:9:[166.8,23.0,144.7,210.1,125.6,211.2,109.5,212.4,96.4,213.5,92.3,214.6,89.2,215.7,87.1,216.8,1.0,217.9]:TopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 16.86/4.02  229:1:11:[200.10,24.0,182.9,219.1,166.8,220.2,144.7,221.3,125.6,222.4,109.5,223.5,96.4,224.6,92.3,225.7,89.2,226.8,87.1,227.9,1.0,228.10]:TopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10)
% 16.86/4.02  239:4:10:[182.9,25.0,166.8,230.2,144.7,231.3,125.6,232.4,109.5,233.5,96.4,234.6,92.3,235.7,89.2,236.8,87.1,237.10,1.0,238.11]:TopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv20_1r1(x0) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 16.86/4.02  249:4:10:[182.9,26.0,166.8,240.3,144.7,241.4,125.6,242.5,109.5,243.6,96.4,244.7,92.3,245.8,89.2,246.9,87.1,247.10,1.0,248.11]:TopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  261:1:12:[229.11,27.0,200.10,250.1,182.9,251.2,166.8,252.3,144.7,253.4,125.6,254.5,109.5,255.6,96.4,256.7,92.3,257.8,89.2,258.9,87.1,259.10,1.0,260.11]:TopTopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 16.86/4.02  273:1:12:[229.11,28.0,200.10,262.1,182.9,263.2,166.8,264.3,144.7,265.4,125.6,266.5,109.5,267.6,96.4,268.7,92.3,269.8,89.2,270.9,87.1,271.10,1.0,272.11]:TopTopTopTopTopTopTopTopTopTopTopTop:  -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc22)
% 16.86/4.02  285:1:12:[229.11,29.1,200.10,274.2,182.9,275.3,166.8,276.4,144.7,277.5,125.6,278.6,109.5,279.7,96.4,280.8,92.3,281.9,89.2,282.10,87.1,283.11,1.0,284.12]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23) -> 
% 16.86/4.02  296:4:11:[200.10,30.0,182.9,286.1,166.8,287.3,144.7,288.4,125.6,289.5,109.5,290.6,96.4,291.7,92.3,292.8,89.2,293.9,87.1,294.11,1.0,295.12]:TopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  309:1:13:[261.12,31.0,229.11,297.1,200.10,298.2,182.9,299.3,166.8,300.4,144.7,301.5,125.6,302.6,109.5,303.7,96.4,304.8,92.3,305.9,89.2,306.10,87.1,307.11,1.0,308.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12)
% 16.86/4.02  322:1:13:[261.12,32.0,229.11,310.1,200.10,311.2,182.9,312.3,166.8,313.4,144.7,314.5,125.6,315.6,109.5,316.7,96.4,317.8,92.3,318.9,89.2,319.10,87.1,320.11,1.0,321.12]:TopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc20)
% 16.86/4.02  335:1:13:[261.12,33.1,229.11,323.2,200.10,324.3,182.9,325.4,166.8,326.5,144.7,327.6,125.6,328.7,109.5,329.8,96.4,330.9,92.3,331.10,89.2,332.11,87.1,333.12,1.0,334.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21) -> 
% 16.86/4.02  347:4:12:[229.11,34.0,200.10,336.2,182.9,337.3,166.8,338.4,144.7,339.6,125.6,340.7,109.5,341.9,96.4,342.10,92.3,343.11,89.2,344.12,87.1,345.13,1.0,346.14]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv20_1r1(x0)
% 16.86/4.02  359:4:12:[229.11,35.0,200.10,348.2,182.9,349.3,166.8,350.5,144.7,351.7,125.6,352.8,109.5,353.9,96.4,354.10,92.3,355.11,89.2,356.12,87.1,357.13,1.0,358.14]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv20_1r1(x0)
% 16.86/4.02  373:1:14:[309.13,36.0,261.12,360.1,229.11,361.2,200.10,362.3,182.9,363.4,166.8,364.5,144.7,365.6,125.6,366.7,109.5,367.8,96.4,368.9,92.3,369.10,89.2,370.11,87.1,371.12,1.0,372.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 16.86/4.02  386:4:13:[261.12,37.0,229.11,374.2,200.10,375.3,182.9,376.4,166.8,377.5,144.7,378.7,125.6,379.8,109.5,380.9,96.4,381.10,92.3,382.11,89.2,383.13,87.1,384.15,1.0,385.16]:TopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv20_1r1(x0) -> 
% 16.86/4.02  400:1:14:[309.13,38.0,261.12,387.1,229.11,388.2,200.10,389.3,182.9,390.4,166.8,391.5,144.7,392.6,125.6,393.7,109.5,394.8,96.4,395.9,92.3,396.10,89.2,397.11,87.1,398.12,1.0,399.13]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc18)
% 16.86/4.02  414:1:14:[309.13,39.1,261.12,401.2,229.11,402.3,200.10,403.4,182.9,404.5,166.8,405.6,144.7,406.7,125.6,407.8,109.5,408.9,96.4,409.10,92.3,410.11,89.2,411.12,87.1,412.13,1.0,413.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc19) -> 
% 16.86/4.02  427:4:13:[261.12,40.0,229.11,415.2,200.10,416.3,182.9,417.4,166.8,418.5,144.7,419.6,125.6,420.7,109.5,421.8,96.4,422.9,92.3,423.10,89.2,424.11,87.1,425.13,1.0,426.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 16.86/4.02  440:4:13:[261.12,41.0,229.11,428.3,200.10,429.4,182.9,430.5,166.8,431.6,144.7,432.8,125.6,433.9,109.5,434.10,96.4,435.11,92.3,436.12,89.2,437.14,87.1,438.15,1.0,439.16]: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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> 
% 16.86/4.02  453:4:13:[261.12,42.0,229.11,441.2,200.10,442.3,182.9,443.4,166.8,444.5,144.7,445.6,125.6,446.7,109.5,447.8,96.4,448.9,92.3,449.10,89.2,450.11,87.1,451.12,1.0,452.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 16.86/4.02  468:1:15:[373.14,43.0,309.13,454.1,261.12,455.2,229.11,456.3,200.10,457.4,182.9,458.5,166.8,459.6,144.7,460.7,125.6,461.8,109.5,462.9,96.4,463.10,92.3,464.11,89.2,465.12,87.1,466.13,1.0,467.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14)
% 16.86/4.02  483:1:15:[373.14,44.0,309.13,469.1,261.12,470.2,229.11,471.3,200.10,472.4,182.9,473.5,166.8,474.6,144.7,475.7,125.6,476.8,109.5,477.9,96.4,478.10,92.3,479.11,89.2,480.12,87.1,481.13,1.0,482.14]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16)
% 16.86/4.02  498:1:15:[373.14,45.1,309.13,484.2,261.12,485.3,229.11,486.4,200.10,487.5,182.9,488.6,166.8,489.7,144.7,490.8,125.6,491.9,109.5,492.10,96.4,493.11,92.3,494.12,89.2,495.13,87.1,496.14,1.0,497.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc17) -> 
% 16.86/4.02  512:4:14:[309.13,46.0,261.12,499.2,229.11,500.3,200.10,501.4,182.9,502.6,166.8,503.7,144.7,504.8,125.6,505.9,109.5,506.10,96.4,507.11,92.3,508.12,89.2,509.14,87.1,510.15,1.0,511.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv19_2r1r1(x0,x1) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 16.86/4.02  527:4:15:[373.14,47.0,309.13,513.1,261.12,514.2,229.11,515.3,200.10,516.4,182.9,517.5,166.8,518.6,144.7,519.7,125.6,520.8,109.5,521.10,96.4,522.11,92.3,523.12,89.2,524.13,87.1,525.14,1.0,526.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1)
% 16.86/4.02  543:1:16:[468.15,48.0,373.14,528.1,309.13,529.2,261.12,530.3,229.11,531.4,200.10,532.5,182.9,533.6,166.8,534.7,144.7,535.8,125.6,536.9,109.5,537.10,96.4,538.11,92.3,539.12,89.2,540.13,87.1,541.14,1.0,542.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 16.86/4.02  558:4:15:[373.14,49.0,309.13,544.1,261.12,545.2,229.11,546.4,200.10,547.5,182.9,548.6,166.8,549.7,144.7,550.8,125.6,551.9,109.5,552.10,96.4,553.11,92.3,554.12,89.2,555.13,87.1,556.14,1.0,557.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 16.86/4.02  573:4:15:[373.14,50.0,309.13,559.2,261.12,560.3,229.11,561.4,200.10,562.5,182.9,563.6,166.8,564.7,144.7,565.8,125.6,566.9,109.5,567.10,96.4,568.11,92.3,569.12,89.2,570.14,87.1,571.15,1.0,572.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 16.86/4.02  590:1:17:[543.16,51.0,468.15,574.1,373.14,575.2,309.13,576.3,261.12,577.4,229.11,578.5,200.10,579.6,182.9,580.7,166.8,581.8,144.7,582.9,125.6,583.10,109.5,584.11,96.4,585.12,92.3,586.13,89.2,587.14,87.1,588.15,1.0,589.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 16.86/4.02  606:4:16:[468.15,52.0,373.14,591.1,309.13,592.2,261.12,593.3,229.11,594.4,200.10,595.5,182.9,596.6,166.8,597.7,144.7,598.8,125.6,599.10,109.5,600.11,96.4,601.12,92.3,602.13,89.2,603.14,87.1,604.16,1.0,605.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 16.86/4.02  622:4:16:[468.15,53.0,373.14,607.1,309.13,608.2,261.12,609.3,229.11,610.4,200.10,611.6,182.9,612.7,166.8,613.8,144.7,614.9,125.6,615.10,109.5,616.11,96.4,617.12,92.3,618.13,89.2,619.14,87.1,620.15,1.0,621.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv20_1r1(x0)
% 16.86/4.02  638:4:16:[468.15,54.0,373.14,623.2,309.13,624.3,261.12,625.4,229.11,626.5,200.10,627.6,182.9,628.7,166.8,629.8,144.7,630.9,125.6,631.10,109.5,632.11,96.4,633.12,92.3,634.14,89.2,635.15,87.1,636.16,1.0,637.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) -> 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)
% 16.86/4.02  655:4:17:[543.16,55.0,468.15,639.1,373.14,640.2,309.13,641.3,261.12,642.4,229.11,643.5,200.10,644.6,182.9,645.7,166.8,646.9,144.7,647.10,125.6,648.11,109.5,649.13,96.4,650.14,92.3,651.15,89.2,652.16,87.1,653.18,1.0,654.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16)
% 16.86/4.02  673:1:18:[590.17,56.0,543.16,656.1,468.15,657.2,373.14,658.3,309.13,659.4,261.12,660.5,229.11,661.6,200.10,662.7,182.9,663.8,166.8,664.9,144.7,665.10,125.6,666.11,109.5,667.12,96.4,668.13,92.3,669.14,89.2,670.15,87.1,671.16,1.0,672.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17)
% 16.86/4.02  689:4:16:[468.15,57.0,373.14,674.2,309.13,675.3,261.12,676.4,229.11,677.6,200.10,678.8,182.9,679.9,166.8,680.10,144.7,681.11,125.6,682.12,109.5,683.13,96.4,684.14,92.3,685.15,89.2,686.16,87.1,687.17,1.0,688.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15)
% 16.86/4.02  706:4:17:[543.16,58.0,468.15,690.2,373.14,691.3,309.13,692.4,261.12,693.5,229.11,694.6,200.10,695.7,182.9,696.8,166.8,697.9,144.7,698.10,125.6,699.11,109.5,700.12,96.4,701.13,92.3,702.14,89.2,703.15,87.1,704.16,1.0,705.17]: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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 16.86/4.02  723:4:17:[543.16,59.0,468.15,707.1,373.14,708.2,309.13,709.3,261.12,710.4,229.11,711.5,200.10,712.6,182.9,713.7,166.8,714.8,144.7,715.10,125.6,716.11,109.5,717.12,96.4,718.13,92.3,719.14,89.2,720.16,87.1,721.17,1.0,722.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> 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)
% 16.86/4.02  740:4:17:[543.16,60.0,468.15,724.1,373.14,725.2,309.13,726.3,261.12,727.4,229.11,728.5,200.10,729.6,182.9,730.7,166.8,731.9,144.7,732.10,125.6,733.11,109.5,734.12,96.4,735.13,92.3,736.14,89.2,737.15,87.1,738.16,1.0,739.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  757:4:17:[543.16,61.0,468.15,741.1,373.14,742.2,309.13,743.3,261.12,744.4,229.11,745.5,200.10,746.6,182.9,747.7,166.8,748.8,144.7,749.9,125.6,750.10,109.5,751.11,96.4,752.12,92.3,753.13,89.2,754.14,87.1,755.15,1.0,756.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> 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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  774:4:17:[543.16,62.0,468.15,758.2,373.14,759.3,309.13,760.5,261.12,761.6,229.11,762.7,200.10,763.8,182.9,764.9,166.8,765.10,144.7,766.11,125.6,767.12,109.5,768.13,96.4,769.15,92.3,770.16,89.2,771.17,87.1,772.18,1.0,773.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 16.86/4.02  791:4:17:[543.16,63.0,468.15,775.3,373.14,776.4,309.13,777.5,261.12,778.6,229.11,779.7,200.10,780.8,182.9,781.9,166.8,782.10,144.7,783.11,125.6,784.12,109.5,785.13,96.4,786.14,92.3,787.15,89.2,788.16,87.1,789.17,1.0,790.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 16.86/4.02  810:1:19:[673.18,64.0,590.17,792.1,543.16,793.2,468.15,794.3,373.14,795.4,309.13,796.5,261.12,797.6,229.11,798.7,200.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.16,87.1,808.17,1.0,809.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 16.86/4.02  828:4:18:[590.17,65.0,543.16,811.2,468.15,812.3,373.14,813.4,309.13,814.5,261.12,815.6,229.11,816.7,200.10,817.8,182.9,818.9,166.8,819.11,144.7,820.12,125.6,821.14,109.5,822.15,96.4,823.16,92.3,824.17,89.2,825.18,87.1,826.19,1.0,827.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  845:4:17:[543.16,66.0,468.15,829.2,373.14,830.3,309.13,831.4,261.12,832.5,229.11,833.6,200.10,834.7,182.9,835.9,166.8,836.10,144.7,837.11,125.6,838.12,109.5,839.13,96.4,840.14,92.3,841.15,89.2,842.16,87.1,843.17,1.0,844.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> 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)
% 16.86/4.02  863:4:18:[590.17,67.0,543.16,846.2,468.15,847.3,373.14,848.5,309.13,849.6,261.12,850.7,229.11,851.8,200.10,852.9,182.9,853.10,166.8,854.11,144.7,855.12,125.6,856.13,109.5,857.14,96.4,858.15,92.3,859.16,89.2,860.17,87.1,861.18,1.0,862.19]: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) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 16.86/4.02  881:4:18:[590.17,68.0,543.16,864.2,468.15,865.3,373.14,866.4,309.13,867.5,261.12,868.6,229.11,869.7,200.10,870.8,182.9,871.9,166.8,872.10,144.7,873.11,125.6,874.12,109.5,875.13,96.4,876.14,92.3,877.15,89.2,878.17,87.1,879.18,1.0,880.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv19_2r1r1(x0,x1) -> 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)
% 16.86/4.02  899:4:18:[590.17,69.0,543.16,882.2,468.15,883.4,373.14,884.5,309.13,885.6,261.12,886.7,229.11,887.8,200.10,888.9,182.9,889.10,166.8,890.11,144.7,891.12,125.6,892.13,109.5,893.14,96.4,894.15,92.3,895.16,89.2,896.17,87.1,897.18,1.0,898.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv20_1r1(x0)
% 16.86/4.02  917:4:18:[590.17,70.0,543.16,900.2,468.15,901.3,373.14,902.4,309.13,903.5,261.12,904.6,229.11,905.7,200.10,906.8,182.9,907.9,166.8,908.10,144.7,909.11,125.6,910.12,109.5,911.13,96.4,912.14,92.3,913.16,89.2,914.17,87.1,915.18,1.0,916.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv18_3r1r1r1(x0,x1,x2) -> 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)
% 16.86/4.02  935:4:18:[590.17,71.0,543.16,918.1,468.15,919.3,373.14,920.4,309.13,921.5,261.12,922.6,229.11,923.7,200.10,924.8,182.9,925.9,166.8,926.11,144.7,927.12,125.6,928.13,109.5,929.14,96.4,930.15,92.3,931.16,89.2,932.17,87.1,933.18,1.0,934.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11)
% 16.86/4.02  953:4:18:[590.17,72.0,543.16,936.2,468.15,937.4,373.14,938.5,309.13,939.6,261.12,940.8,229.11,941.9,200.10,942.10,182.9,943.11,166.8,944.13,144.7,945.14,125.6,946.15,109.5,947.16,96.4,948.17,92.3,949.18,89.2,950.19,87.1,951.20,1.0,952.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> 
% 16.86/4.02  972:4:19:[673.18,73.0,590.17,954.2,543.16,955.3,468.15,956.4,373.14,957.5,309.13,958.6,261.12,959.7,229.11,960.8,200.10,961.9,182.9,962.11,166.8,963.13,144.7,964.14,125.6,965.15,109.5,966.16,96.4,967.17,92.3,968.18,89.2,969.19,87.1,970.20,1.0,971.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  991:4:19:[673.18,74.0,590.17,973.1,543.16,974.2,468.15,975.3,373.14,976.4,309.13,977.5,261.12,978.6,229.11,979.7,200.10,980.8,182.9,981.9,166.8,982.10,144.7,983.11,125.6,984.12,109.5,985.13,96.4,986.14,92.3,987.15,89.2,988.17,87.1,989.18,1.0,990.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),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)
% 16.86/4.02  1010:4:19:[673.18,75.0,590.17,992.1,543.16,993.2,468.15,994.3,373.14,995.4,309.13,996.6,261.12,997.7,229.11,998.8,200.10,999.9,182.9,1000.10,166.8,1001.11,144.7,1002.12,125.6,1003.13,109.5,1004.14,96.4,1005.15,92.3,1006.16,89.2,1007.17,87.1,1008.18,1.0,1009.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  1029:4:19:[673.18,76.0,590.17,1011.1,543.16,1012.3,468.15,1013.4,373.14,1014.5,309.13,1015.7,261.12,1016.8,229.11,1017.9,200.10,1018.10,182.9,1019.11,166.8,1020.12,144.7,1021.13,125.6,1022.14,109.5,1023.15,96.4,1024.16,92.3,1025.18,89.2,1026.19,87.1,1027.20,1.0,1028.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 16.86/4.02  1048:4:19:[673.18,77.0,590.17,1030.2,543.16,1031.3,468.15,1032.4,373.14,1033.5,309.13,1034.6,261.12,1035.7,229.11,1036.8,200.10,1037.10,182.9,1038.11,166.8,1039.12,144.7,1040.13,125.6,1041.14,109.5,1042.15,96.4,1043.16,92.3,1044.17,89.2,1045.18,87.1,1046.19,1.0,1047.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 16.86/4.02  1067:4:19:[673.18,78.0,590.17,1049.2,543.16,1050.4,468.15,1051.5,373.14,1052.7,309.13,1053.8,261.12,1054.9,229.11,1055.10,200.10,1056.11,182.9,1057.12,166.8,1058.13,144.7,1059.14,125.6,1060.15,109.5,1061.16,96.4,1062.17,92.3,1063.19,89.2,1064.20,87.1,1065.21,1.0,1066.22]: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),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) -> 
% 16.86/4.02  1086:4:19:[673.18,79.0,590.17,1068.1,543.16,1069.3,468.15,1070.5,373.14,1071.6,309.13,1072.7,261.12,1073.8,229.11,1074.9,200.10,1075.10,182.9,1076.11,166.8,1077.12,144.7,1078.13,125.6,1079.14,109.5,1080.15,96.4,1081.17,92.3,1082.18,89.2,1083.19,87.1,1084.20,1.0,1085.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 16.86/4.02  1106:4:20:[810.19,80.0,673.18,1087.1,590.17,1088.2,543.16,1089.3,468.15,1090.5,373.14,1091.6,309.13,1092.7,261.12,1093.8,229.11,1094.9,200.10,1095.10,182.9,1096.11,166.8,1097.12,144.7,1098.13,125.6,1099.14,109.5,1100.15,96.4,1101.16,92.3,1102.17,89.2,1103.18,87.1,1104.19,1.0,1105.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 16.86/4.02  1126:4:20:[810.19,81.0,673.18,1107.2,590.17,1108.3,543.16,1109.4,468.15,1110.5,373.14,1111.6,309.13,1112.7,261.12,1113.8,229.11,1114.9,200.10,1115.10,182.9,1116.11,166.8,1117.12,144.7,1118.13,125.6,1119.14,109.5,1120.15,96.4,1121.16,92.3,1122.17,89.2,1123.18,87.1,1124.19,1.0,1125.20]: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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 16.86/4.02  1146:4:20:[810.19,82.0,673.18,1127.1,590.17,1128.2,543.16,1129.4,468.15,1130.5,373.14,1131.6,309.13,1132.7,261.12,1133.8,229.11,1134.9,200.10,1135.10,182.9,1136.11,166.8,1137.12,144.7,1138.13,125.6,1139.14,109.5,1140.15,96.4,1141.16,92.3,1142.17,89.2,1143.18,87.1,1144.19,1.0,1145.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 16.86/4.02  1165:4:19:[673.18,83.0,590.17,1147.2,543.16,1148.3,468.15,1149.4,373.14,1150.6,309.13,1151.8,261.12,1152.9,229.11,1153.10,200.10,1154.11,182.9,1155.12,166.8,1156.13,144.7,1157.14,125.6,1158.15,109.5,1159.16,96.4,1160.17,92.3,1161.18,89.2,1162.19,87.1,1163.20,1.0,1164.21]: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),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 16.86/4.02  1185:4:20:[810.19,84.0,673.18,1166.2,590.17,1167.3,543.16,1168.5,468.15,1169.6,373.14,1170.7,309.13,1171.8,261.12,1172.9,229.11,1173.10,200.10,1174.11,182.9,1175.12,166.8,1176.13,144.7,1177.14,125.6,1178.15,109.5,1179.16,96.4,1180.17,92.3,1181.18,89.2,1182.20,87.1,1183.21,1.0,1184.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv19_2r1r1(x0,x1) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 16.86/4.02  1205:4:20:[810.19,85.0,673.18,1186.2,590.17,1187.3,543.16,1188.4,468.15,1189.5,373.14,1190.6,309.13,1191.7,261.12,1192.8,229.11,1193.9,200.10,1194.10,182.9,1195.11,166.8,1196.12,144.7,1197.13,125.6,1198.14,109.5,1199.15,96.4,1200.16,92.3,1201.17,89.2,1202.19,87.1,1203.20,1.0,1204.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv19_2r1r1(x0,x1) -> 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)
% 16.86/4.02  1225:4:20:[810.19,86.0,673.18,1206.2,590.17,1207.3,543.16,1208.4,468.15,1209.6,373.14,1210.7,309.13,1211.8,261.12,1212.9,229.11,1213.10,200.10,1214.11,182.9,1215.12,166.8,1216.13,144.7,1217.15,125.6,1218.16,109.5,1219.17,96.4,1220.18,92.3,1221.19,89.2,1222.20,87.1,1223.21,1.0,1224.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 16.86/4.02  
% 16.86/4.02   Most General Atoms: ssNder1_0 ssNder1_1r1(x0) ssNder1_2r1r1(x0,x1) ssNder1_3r1r1r1(x0,x1,x2) ssNder1_4r1r1r1r1(x0,x1,x2,x3) ssNder1_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssNder1_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssNder1_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) ssPv19_2r1r1(x0,x1) ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) ssPv17_4r1r1r1r1(x0,x1,x2,x3) ssNder1_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) ssPv20_1r1(x0) ssNder1_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ssPv18_3r1r1r1(x0,x1,x2) 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) 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) ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) 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) ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) 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) ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17) ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19) 
% 16.86/4.02  
% 16.86/4.02  === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: resolution_2 ===
% 16.86/4.02  
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 56
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 527:4:15:[373.14,47.0,309.13,513.1,261.12,514.2,229.11,515.3,200.10,516.4,182.9,517.5,166.8,518.6,144.7,519.7,125.6,520.8,109.5,521.10,96.4,522.11,92.3,523.12,89.2,524.13,87.1,525.14,1.0,526.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1226:3:14:[527.1,100.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1)
% 16.86/4.02  === Conflict found: 209:4:9:[166.8,22.0,144.7,201.2,125.6,202.4,109.5,203.6,96.4,204.7,92.3,205.8,89.2,206.9,87.1,207.11,1.0,208.12]:TopTopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1227:3:8:[209.3,100.1]:TopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv20_1r1(x0) -> 
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 69
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 972:4:19:[673.18,73.0,590.17,954.2,543.16,955.3,468.15,956.4,373.14,957.5,309.13,958.6,261.12,959.7,229.11,960.8,200.10,961.9,182.9,962.11,166.8,963.13,144.7,964.14,125.6,965.15,109.5,966.16,96.4,967.17,92.3,968.18,89.2,969.19,87.1,970.20,1.0,971.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> 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}
% 16.86/4.02  === Backtracking. Learning clause 1228:3:18:[972.4,104.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6) -> 
% 16.86/4.02  === Conflict found: 249:4:10:[182.9,26.0,166.8,240.3,144.7,241.4,125.6,242.5,109.5,243.6,96.4,244.7,92.3,245.8,89.2,246.9,87.1,247.10,1.0,248.11]:TopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1229:3:9:[249.3,104.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6) -> ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  === Conflict found: 173:4:7:[125.6,18.0,109.5,167.2,96.4,168.3,92.3,169.4,89.2,170.6,87.1,171.7,1.0,172.8]:TopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> 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}
% 16.86/4.02  === Backtracking. Learning clause 1230:3:6:[173.3,104.1]:TopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5),ssPv19_2r1r1(x0,x1) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 16.86/4.02  === Conflict found: 453:4:13:[261.12,42.0,229.11,441.2,200.10,442.3,182.9,443.4,166.8,444.5,144.7,445.6,125.6,446.7,109.5,447.8,96.4,448.9,92.3,449.10,89.2,450.11,87.1,451.12,1.0,452.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23}
% 16.86/4.02  === Backtracking. Learning clause 1231:6:19:[453.3,689.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x11,x12,x13,x14),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x11) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x15,x16),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x11,x12,x13,x14,x17,x18)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 74
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 828:4:18:[590.17,65.0,543.16,811.2,468.15,812.3,373.14,813.4,309.13,814.5,261.12,815.6,229.11,816.7,200.10,817.8,182.9,818.9,166.8,819.11,144.7,820.12,125.6,821.14,109.5,822.15,96.4,823.16,92.3,824.17,89.2,825.18,87.1,826.19,1.0,827.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5) -> ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1232:3:17:[828.3,114.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6) -> ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  === Conflict found: 606:4:16:[468.15,52.0,373.14,591.1,309.13,592.2,261.12,593.3,229.11,594.4,200.10,595.5,182.9,596.6,166.8,597.7,144.7,598.8,125.6,599.10,109.5,600.11,96.4,601.12,92.3,602.13,89.2,603.14,87.1,604.16,1.0,605.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1233:3:15:[606.1,114.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10)
% 16.86/4.02  === Conflict found: 1227:3:8:[209.3,100.1]:TopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4),ssPv20_1r1(x0) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc28, x5 -> skc30, x6 -> skc30, x7 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1234:2:7:[1227.2,114.1]:TopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,skc28,x4,x5,x6),ssPv20_1r1(x0) -> 
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 82
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1185:4:20:[810.19,84.0,673.18,1166.2,590.17,1167.3,543.16,1168.5,468.15,1169.6,373.14,1170.7,309.13,1171.8,261.12,1172.9,229.11,1173.10,200.10,1174.11,182.9,1175.12,166.8,1176.13,144.7,1177.14,125.6,1178.15,109.5,1179.16,96.4,1180.17,92.3,1181.18,89.2,1182.20,87.1,1183.21,1.0,1184.22]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv19_2r1r1(x0,x1) -> 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, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1235:3:19:[1185.4,119.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) -> 
% 16.86/4.02  === Conflict found: 881:4:18:[590.17,68.0,543.16,864.2,468.15,865.3,373.14,866.4,309.13,867.5,261.12,868.6,229.11,869.7,200.10,870.8,182.9,871.9,166.8,872.10,144.7,873.11,125.6,874.12,109.5,875.13,96.4,876.14,92.3,877.15,89.2,878.17,87.1,879.18,1.0,880.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv19_2r1r1(x0,x1) -> 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) {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}
% 16.86/4.02  === Backtracking. Learning clause 1236:3:17:[881.4,119.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv19_2r1r1(x0,x1) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13)
% 16.86/4.02  === Conflict found: 427:4:13:[261.12,40.0,229.11,415.2,200.10,416.3,182.9,417.4,166.8,418.5,144.7,419.6,125.6,420.7,109.5,421.8,96.4,422.9,92.3,423.10,89.2,424.11,87.1,425.13,1.0,426.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) -> 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 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1237:3:12:[427.4,119.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11),ssPv20_1r1(x0) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7)
% 16.86/4.02  === Conflict found: 218:4:9:[166.8,23.0,144.7,210.1,125.6,211.2,109.5,212.4,96.4,213.5,92.3,214.6,89.2,215.7,87.1,216.8,1.0,217.9]:TopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1238:3:8:[218.3,119.1]:TopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 146
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 155
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 173:4:7:[125.6,18.0,109.5,167.2,96.4,168.3,92.3,169.4,89.2,170.6,87.1,171.7,1.0,172.8]:TopTopTopTopTopTopTop: ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> 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 -> skc26}
% 16.86/4.02  === Backtracking. Learning clause 1239:2:4:[173.1,131.1,104.1]:TopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 164
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 512:4:14:[309.13,46.0,261.12,499.2,229.11,500.3,200.10,501.4,182.9,502.6,166.8,503.7,144.7,504.8,125.6,505.9,109.5,506.10,96.4,507.11,92.3,508.12,89.2,509.14,87.1,510.15,1.0,511.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv19_2r1r1(x0,x1) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1240:3:13:[512.4,137.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7),ssPv19_2r1r1(x0,x1) -> 
% 16.86/4.02  === Conflict found: 239:4:10:[182.9,25.0,166.8,230.2,144.7,231.3,125.6,232.4,109.5,233.5,96.4,234.6,92.3,235.7,89.2,236.8,87.1,237.10,1.0,238.11]:TopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv20_1r1(x0) -> 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}
% 16.86/4.02  === Backtracking. Learning clause 1241:3:9:[239.3,137.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7,x8),ssPv20_1r1(x0) -> ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 16.86/4.02  === Conflict found: 991:4:19:[673.18,74.0,590.17,973.1,543.16,974.2,468.15,975.3,373.14,976.4,309.13,977.5,261.12,978.6,229.11,979.7,200.10,980.8,182.9,981.9,166.8,982.10,144.7,983.11,125.6,984.12,109.5,985.13,96.4,986.14,92.3,987.15,89.2,988.17,87.1,989.18,1.0,990.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),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) {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}
% 16.86/4.02  === Backtracking. Learning clause 1243:4:19:[1239.1,1242.2,991.3,1086.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 174
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 190:4:8:[144.7,20.0,125.6,183.2,109.5,184.3,96.4,185.4,92.3,186.5,89.2,187.6,87.1,188.7,1.0,189.8]:TopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc24}
% 16.86/4.02  === Backtracking. Learning clause 1244:3:5:[190.1,151.1]:TopTopTopTopTop:  -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1),ssPv20_1r1(x0)
% 16.86/4.02  === Conflict found: 1232:3:17:[828.3,114.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6) -> ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc24, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1245:2:16:[1232.2,151.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,skc24,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  === Conflict found: 1229:3:9:[249.3,104.1]:TopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6) -> ssPv18_3r1r1r1(x0,x1,x2) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc28, x5 -> skc30, x6 -> skc24, x7 -> skc30, x8 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1246:2:8:[1229.2,151.1]:TopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7) -> ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  === Conflict found: 1228:3:18:[972.4,104.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6,x7),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,x6) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc28, x5 -> skc30, x6 -> skc24, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1247:2:17:[1228.3,151.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6) -> 
% 16.86/4.02  === Conflict found: 527:4:15:[373.14,47.0,309.13,513.1,261.12,514.2,229.11,515.3,200.10,516.4,182.9,517.5,166.8,518.6,144.7,519.7,125.6,520.8,109.5,521.10,96.4,522.11,92.3,523.12,89.2,524.13,87.1,525.14,1.0,526.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc31, x14 -> skc19}
% 16.86/4.02  === Backtracking. Learning clause 1248:2:5:[527.2,414.1,100.1,1239.1]:TopTopTopTopTop:  -> ssPv18_3r1r1r1(x0,x1,x2),ssPv17_4r1r1r1r1(x0,x1,x3,x4)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 181
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 706:4:17:[543.16,58.0,468.15,690.2,373.14,691.3,309.13,692.4,261.12,693.5,229.11,694.6,200.10,695.7,182.9,696.8,166.8,697.9,144.7,698.10,125.6,699.11,109.5,700.12,96.4,701.13,92.3,702.14,89.2,703.15,87.1,704.16,1.0,705.17]: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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {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}
% 16.86/4.02  === Backtracking. Learning clause 1249:3:16:[706.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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 16.86/4.02  === Conflict found: 573:4:15:[373.14,50.0,309.13,559.2,261.12,560.3,229.11,561.4,200.10,562.5,182.9,563.6,166.8,564.7,144.7,565.8,125.6,566.9,109.5,567.10,96.4,568.11,92.3,569.12,89.2,570.14,87.1,571.15,1.0,572.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),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}
% 16.86/4.02  === Backtracking. Learning clause 1250:3:14:[573.4,158.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7,x8,x9,x10,x11,x12,x13),ssPv19_2r1r1(x0,x1) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 245
% 16.86/4.02  === Conflict found: 1029:4:19:[673.18,76.0,590.17,1011.1,543.16,1012.3,468.15,1013.4,373.14,1014.5,309.13,1015.7,261.12,1016.8,229.11,1017.9,200.10,1018.10,182.9,1019.11,166.8,1020.12,144.7,1021.13,125.6,1022.14,109.5,1023.15,96.4,1024.16,92.3,1025.18,89.2,1026.19,87.1,1027.20,1.0,1028.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1251:7:23:[1029.2,757.2,991.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) -> ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x17,x18,x19,x20,x21,x22),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 251
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 440:4:13:[261.12,41.0,229.11,428.3,200.10,429.4,182.9,430.5,166.8,431.6,144.7,432.8,125.6,433.9,109.5,434.10,96.4,435.11,92.3,436.12,89.2,437.14,87.1,438.15,1.0,439.16]: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),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 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 16.86/4.02  === Backtracking. Learning clause 1252:3:11:[440.1,273.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) -> 
% 16.86/4.02  === Conflict found: 427:4:13:[261.12,40.0,229.11,415.2,200.10,416.3,182.9,417.4,166.8,418.5,144.7,419.6,125.6,420.7,109.5,421.8,96.4,422.9,92.3,423.10,89.2,424.11,87.1,425.13,1.0,426.14]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv20_1r1(x0) -> 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 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22}
% 16.86/4.02  === Backtracking. Learning clause 1253:2:8:[427.1,273.1,119.1]:TopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 256
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1205:4:20:[810.19,85.0,673.18,1186.2,590.17,1187.3,543.16,1188.4,468.15,1189.5,373.14,1190.6,309.13,1191.7,261.12,1192.8,229.11,1193.9,200.10,1194.10,182.9,1195.11,166.8,1196.12,144.7,1197.13,125.6,1198.14,109.5,1199.15,96.4,1200.16,92.3,1201.17,89.2,1202.19,87.1,1203.20,1.0,1204.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv19_2r1r1(x0,x1) -> 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) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1254:5:21:[1205.4,285.1,638.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15,x16,x17,x18),ssPv19_2r1r1(x0,x1),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x19,x20),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 16.86/4.02  === Conflict found: 917:4:18:[590.17,70.0,543.16,900.2,468.15,901.3,373.14,902.4,309.13,903.5,261.12,904.6,229.11,905.7,200.10,906.8,182.9,907.9,166.8,908.10,144.7,909.11,125.6,910.12,109.5,911.13,96.4,912.14,92.3,913.16,89.2,914.17,87.1,915.18,1.0,916.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv18_3r1r1r1(x0,x1,x2) -> 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) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1255:3:17:[917.4,285.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15,x16),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14)
% 16.86/4.02  === Conflict found: 845:4:17:[543.16,66.0,468.15,829.2,373.14,830.3,309.13,831.4,261.12,832.5,229.11,833.6,200.10,834.7,182.9,835.9,166.8,836.10,144.7,837.11,125.6,838.12,109.5,839.13,96.4,840.14,92.3,841.15,89.2,842.16,87.1,843.17,1.0,844.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> 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) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1256:3:16:[845.4,285.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14)
% 16.86/4.02  === Conflict found: 453:4:13:[261.12,42.0,229.11,441.2,200.10,442.3,182.9,443.4,166.8,444.5,144.7,445.6,125.6,446.7,109.5,447.8,96.4,448.9,92.3,449.10,89.2,450.11,87.1,451.12,1.0,452.13]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc23}
% 16.86/4.02  === Backtracking. Learning clause 1257:3:11:[453.2,285.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 16.86/4.02  === Conflict found: 1067:4:19:[673.18,78.0,590.17,1049.2,543.16,1050.4,468.15,1051.5,373.14,1052.7,309.13,1053.8,261.12,1054.9,229.11,1055.10,200.10,1056.11,182.9,1057.12,166.8,1058.13,144.7,1059.14,125.6,1060.15,109.5,1061.16,96.4,1062.17,92.3,1063.19,89.2,1064.20,87.1,1065.21,1.0,1066.22]: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),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) ->  {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}
% 16.86/4.02  === Backtracking. Learning clause 1258:7:14:[1067.1,1086.4,689.4,558.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),ssPv17_4r1r1r1r1(x0,x1,x2,x3),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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1)
% 16.86/4.02  === Conflict found: 1048:4:19:[673.18,77.0,590.17,1030.2,543.16,1031.3,468.15,1032.4,373.14,1033.5,309.13,1034.6,261.12,1035.7,229.11,1036.8,200.10,1037.10,182.9,1038.11,166.8,1039.12,144.7,1040.13,125.6,1041.14,109.5,1042.15,96.4,1043.16,92.3,1044.17,89.2,1045.18,87.1,1046.19,1.0,1047.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {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}
% 16.86/4.02  === Backtracking. Learning clause 1259:5:19:[1048.3,1067.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 16.86/4.02  === Conflict found: 1029:4:19:[673.18,76.0,590.17,1011.1,543.16,1012.3,468.15,1013.4,373.14,1014.5,309.13,1015.7,261.12,1016.8,229.11,1017.9,200.10,1018.10,182.9,1019.11,166.8,1020.12,144.7,1021.13,125.6,1022.14,109.5,1023.15,96.4,1024.16,92.3,1025.18,89.2,1026.19,87.1,1027.20,1.0,1028.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1260:6:14:[1029.4,1259.2,689.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 16.86/4.02  === Conflict found: 1029:4:19:[673.18,76.0,590.17,1011.1,543.16,1012.3,468.15,1013.4,373.14,1014.5,309.13,1015.7,261.12,1016.8,229.11,1017.9,200.10,1018.10,182.9,1019.11,166.8,1020.12,144.7,1021.13,125.6,1022.14,109.5,1023.15,96.4,1024.16,92.3,1025.18,89.2,1026.19,87.1,1027.20,1.0,1028.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc22, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1261:5:14:[1029.4,1067.1,638.3,1260.5]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 16.86/4.02  === Conflict found: 1106:4:20:[810.19,80.0,673.18,1087.1,590.17,1088.2,543.16,1089.3,468.15,1090.5,373.14,1091.6,309.13,1092.7,261.12,1093.8,229.11,1094.9,200.10,1095.10,182.9,1096.11,166.8,1097.12,144.7,1098.13,125.6,1099.14,109.5,1100.15,96.4,1101.16,92.3,1102.17,89.2,1103.18,87.1,1104.19,1.0,1105.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc26, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1262:5:15:[1106.2,1225.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9)
% 16.86/4.02  === Conflict found: 655:4:17:[543.16,55.0,468.15,639.1,373.14,640.2,309.13,641.3,261.12,642.4,229.11,643.5,200.10,644.6,182.9,645.7,166.8,646.9,144.7,647.10,125.6,648.11,109.5,649.13,96.4,650.14,92.3,651.15,89.2,652.16,87.1,653.18,1.0,654.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> 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}
% 16.86/4.02  === Backtracking. Learning clause 1263:9:20:[655.1,1261.5,774.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0),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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x14,x15,x16,x17,x18),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x14,x15,x16,x17,x18,x19)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 261
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 512:4:14:[309.13,46.0,261.12,499.2,229.11,500.3,200.10,501.4,182.9,502.6,166.8,503.7,144.7,504.8,125.6,505.9,109.5,506.10,96.4,507.11,92.3,508.12,89.2,509.14,87.1,510.15,1.0,511.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv19_2r1r1(x0,x1) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc20}
% 16.86/4.02  === Backtracking. Learning clause 1264:2:8:[512.1,322.1,137.1]:TopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7),ssPv19_2r1r1(x0,x1) -> 
% 16.86/4.02  === Conflict found: 1257:3:11:[453.2,285.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1265:6:19:[1257.3,1262.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,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),ssPv19_2r1r1(x0,x1),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x11,x12,x13)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 266
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 899:4:18:[590.17,69.0,543.16,882.2,468.15,883.4,373.14,884.5,309.13,885.6,261.12,886.7,229.11,887.8,200.10,888.9,182.9,889.10,166.8,890.11,144.7,891.12,125.6,892.13,109.5,893.14,96.4,894.15,92.3,895.16,89.2,896.17,87.1,897.18,1.0,898.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),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 -> skc21, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1266:3:17:[899.3,335.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21,x13,x14,x15,x16),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21,x13) -> ssPv20_1r1(x0)
% 16.86/4.02  === Conflict found: 774:4:17:[543.16,62.0,468.15,758.2,373.14,759.3,309.13,760.5,261.12,761.6,229.11,762.7,200.10,763.8,182.9,764.9,166.8,765.10,144.7,766.11,125.6,767.12,109.5,768.13,96.4,769.15,92.3,770.16,89.2,771.17,87.1,772.18,1.0,773.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc21, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1267:3:16:[774.4,335.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 
% 16.86/4.02  === Conflict found: 622:4:16:[468.15,53.0,373.14,607.1,309.13,608.2,261.12,609.3,229.11,610.4,200.10,611.6,182.9,612.7,166.8,613.8,144.7,614.9,125.6,615.10,109.5,616.11,96.4,617.12,92.3,618.13,89.2,619.14,87.1,620.15,1.0,621.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),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 -> skc21, x14 -> skc30, x15 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1268:3:15:[622.3,335.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21,x13,x14),ssPv20_1r1(x0)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 330
% 16.86/4.02  === Conflict found: 774:4:17:[543.16,62.0,468.15,758.2,373.14,759.3,309.13,760.5,261.12,761.6,229.11,762.7,200.10,763.8,182.9,764.9,166.8,765.10,144.7,766.11,125.6,767.12,109.5,768.13,96.4,769.15,92.3,770.16,89.2,771.17,87.1,772.18,1.0,773.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1269:6:19:[774.4,689.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x17,x18)
% 16.86/4.02  === Conflict found: 638:4:16:[468.15,54.0,373.14,623.2,309.13,624.3,261.12,625.4,229.11,626.5,200.10,627.6,182.9,628.7,166.8,629.8,144.7,630.9,125.6,631.10,109.5,632.11,96.4,633.12,92.3,634.14,89.2,635.15,87.1,636.16,1.0,637.17]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) -> 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) {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 -> skc20, x14 -> skc30, x15 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1270:4:19:[638.3,1067.2,1259.1]: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),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 337
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 573:4:15:[373.14,50.0,309.13,559.2,261.12,560.3,229.11,561.4,200.10,562.5,182.9,563.6,166.8,564.7,144.7,565.8,125.6,566.9,109.5,567.10,96.4,568.11,92.3,569.12,89.2,570.14,87.1,571.15,1.0,572.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),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 -> skc21, x14 -> skc18}
% 16.86/4.02  === Backtracking. Learning clause 1271:2:8:[573.1,400.1,158.1]:TopTopTopTopTopTopTopTop: ssPv19_2r1r1(x0,x1) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc25,x7)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 340
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1086:4:19:[673.18,79.0,590.17,1068.1,543.16,1069.3,468.15,1070.5,373.14,1071.6,309.13,1072.7,261.12,1073.8,229.11,1074.9,200.10,1075.10,182.9,1076.11,166.8,1077.12,144.7,1078.13,125.6,1079.14,109.5,1080.15,96.4,1081.17,92.3,1082.18,89.2,1083.19,87.1,1084.20,1.0,1085.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1272:3:18:[1086.1,483.1,1239.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16,x15,x16,x17)
% 16.86/4.02  === Conflict found: 1029:4:19:[673.18,76.0,590.17,1011.1,543.16,1012.3,468.15,1013.4,373.14,1014.5,309.13,1015.7,261.12,1016.8,229.11,1017.9,200.10,1018.10,182.9,1019.11,166.8,1020.12,144.7,1021.13,125.6,1022.14,109.5,1023.15,96.4,1024.16,92.3,1025.18,89.2,1026.19,87.1,1027.20,1.0,1028.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1273:3:18:[1029.1,483.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16,x15,x16,x17)
% 16.86/4.02  === Conflict found: 1235:3:19:[1185.4,119.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc16, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1274:2:18:[1235.2,483.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,skc16,x14,x15,x16,x17),ssPv19_2r1r1(x0,x1) -> 
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 351
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1233:3:15:[606.1,114.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc23, x12 -> skc21, x13 -> skc30, x14 -> skc17}
% 16.86/4.02  === Backtracking. Learning clause 1275:2:11:[1233.2,498.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,x6,x7,x8,x9,x10)
% 16.86/4.02  === Conflict found: 512:4:14:[309.13,46.0,261.12,499.2,229.11,500.3,200.10,501.4,182.9,502.6,166.8,503.7,144.7,504.8,125.6,505.9,109.5,506.10,96.4,507.11,92.3,508.12,89.2,509.14,87.1,510.15,1.0,511.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv19_2r1r1(x0,x1) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc28, x13 -> skc20}
% 16.86/4.02  === Backtracking. Learning clause 1276:2:2:[512.2,427.3,322.1,386.2,273.1,1227.2,1271.2]:TopTop: ssPv20_1r1(x0),ssPv19_2r1r1(x0,x1) -> 
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 355
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 863:4:18:[590.17,67.0,543.16,846.2,468.15,847.3,373.14,848.5,309.13,849.6,261.12,850.7,229.11,851.8,200.10,852.9,182.9,853.10,166.8,854.11,144.7,855.12,125.6,856.13,109.5,857.14,96.4,858.15,92.3,859.16,89.2,860.17,87.1,861.18,1.0,862.19]: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) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1278:4:24:[1239.0,1277.2,863.2,1126.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x18,x19,x20,x21,x22,x23) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 419
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 423
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 935:4:18:[590.17,71.0,543.16,918.1,468.15,919.3,373.14,920.4,309.13,921.5,261.12,922.6,229.11,923.7,200.10,924.8,182.9,925.9,166.8,926.11,144.7,927.12,125.6,928.13,109.5,929.14,96.4,930.15,92.3,931.16,89.2,932.17,87.1,933.18,1.0,934.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1280:3:13:[151.0,1279.1,935.3,1245.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,skc24,x6,x7,x8,x9,x10,x11,x12) -> ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc28,x5,skc24,x6,x7,x8,x9),ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  === Conflict found: 527:4:15:[373.14,47.0,309.13,513.1,261.12,514.2,229.11,515.3,200.10,516.4,182.9,517.5,166.8,518.6,144.7,519.7,125.6,520.8,109.5,521.10,96.4,522.11,92.3,523.12,89.2,524.13,87.1,525.14,1.0,526.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc31, x14 -> skc19}
% 16.86/4.02  === Backtracking. Learning clause 1281:2:3:[527.2,414.1,100.1]:TopTopTop:  -> ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 434
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1257:3:11:[453.2,285.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1282:3:9:[1257.2,1246.1]:TopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5),ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  === Conflict found: 1252:3:11:[440.1,273.1]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),ssPv19_2r1r1(x0,x1) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1283:2:9:[1252.2,1282.2,1281.2]:TopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8) -> ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 438
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 774:4:17:[543.16,62.0,468.15,758.2,373.14,759.3,309.13,760.5,261.12,761.6,229.11,762.7,200.10,763.8,182.9,764.9,166.8,765.10,144.7,766.11,125.6,767.12,109.5,768.13,96.4,769.15,92.3,770.16,89.2,771.17,87.1,772.18,1.0,773.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc16, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1284:5:17:[774.3,1239.2,512.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv19_2r1r1(x0,x1) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6)
% 16.86/4.02  === Conflict found: 1272:3:18:[1086.1,483.1,1239.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv19_2r1r1(x0,x1) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16,x15,x16,x17) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1285:3:13:[1272.3,1247.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6) -> 
% 16.86/4.02  === Conflict found: 1086:4:19:[673.18,79.0,590.17,1068.1,543.16,1069.3,468.15,1070.5,373.14,1071.6,309.13,1072.7,261.12,1073.8,229.11,1074.9,200.10,1075.10,182.9,1076.11,166.8,1077.12,144.7,1078.13,125.6,1079.14,109.5,1080.15,96.4,1081.17,92.3,1082.18,89.2,1083.19,87.1,1084.20,1.0,1085.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1286:3:13:[1086.1,483.1,1247.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6) -> 
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 438
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1285:3:13:[1272.3,1247.1]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12),ssPv19_2r1r1(x0,x1),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1287:3:14:[1285.2,1281.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6) -> ssPv18_3r1r1r1(x0,x1,x13)
% 16.86/4.02  === Conflict found: 1267:3:16:[774.4,335.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21,x13,x14,x15),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 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1288:3:17:[1267.3,1248.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,skc21,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv18_3r1r1r1(x0,x1,x16)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 502
% 16.86/4.02  === Conflict found: 935:4:18:[590.17,71.0,543.16,918.1,468.15,919.3,373.14,920.4,309.13,921.5,261.12,922.6,229.11,923.7,200.10,924.8,182.9,925.9,166.8,926.11,144.7,927.12,125.6,928.13,109.5,929.14,96.4,930.15,92.3,931.16,89.2,932.17,87.1,933.18,1.0,934.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),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 -> 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}
% 16.86/4.02  === Backtracking. Learning clause 1289:5:15:[935.4,359.1,899.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6),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),ssPv20_1r1(x0)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 511
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 845:4:17:[543.16,66.0,468.15,829.2,373.14,830.3,309.13,831.4,261.12,832.5,229.11,833.6,200.10,834.7,182.9,835.9,166.8,836.10,144.7,837.11,125.6,838.12,109.5,839.13,96.4,840.14,92.3,841.15,89.2,842.16,87.1,843.17,1.0,844.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> 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) {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, x15 -> skc30, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1290:4:16:[845.2,1253.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,x11)
% 16.86/4.02  === Conflict found: 1256:3:16:[845.4,285.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14,x15),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,skc23,x12,x13,x14) {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, x15 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1291:3:15:[1256.2,1253.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,skc23,x11,x12,x13,x14),ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9,x10,skc23,x11,x12,x13)
% 16.86/4.02  === Conflict found: 1029:4:19:[673.18,76.0,590.17,1011.1,543.16,1012.3,468.15,1013.4,373.14,1014.5,309.13,1015.7,261.12,1016.8,229.11,1017.9,200.10,1018.10,182.9,1019.11,166.8,1020.12,144.7,1021.13,125.6,1022.14,109.5,1023.15,96.4,1024.16,92.3,1025.18,89.2,1026.19,87.1,1027.20,1.0,1028.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1292:5:14:[1029.4,1067.1,689.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> 
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 515
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1264:2:8:[512.1,322.1,137.1]:TopTopTopTopTopTopTopTop: ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,skc27,x6,x7),ssPv19_2r1r1(x0,x1) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc29, x6 -> skc25, x7 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1293:1:2:[1264.1,1271.2]:TopTop: ssPv19_2r1r1(x0,x1) -> 
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 515
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 527:4:15:[373.14,47.0,309.13,513.1,261.12,514.2,229.11,515.3,200.10,516.4,182.9,517.5,166.8,518.6,144.7,519.7,125.6,520.8,109.5,521.10,96.4,522.11,92.3,523.12,89.2,524.13,87.1,525.14,1.0,526.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1294:2:14:[527.4,1293.1,100.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc30,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2)
% 16.86/4.02  === Conflict found: 1244:3:5:[190.1,151.1]:TopTopTopTopTop:  -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1),ssPv20_1r1(x0) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31}
% 16.86/4.02  === Backtracking. Learning clause 1296:1:8:[1293.0,1295.0,1244.1,104.1,1253.1]:TopTopTopTopTopTopTopTop:  -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7)
% 16.86/4.02  === Conflict found: 558:4:15:[373.14,49.0,309.13,544.1,261.12,545.2,229.11,546.4,200.10,547.5,182.9,548.6,166.8,549.7,144.7,550.8,125.6,551.9,109.5,552.10,96.4,553.11,92.3,554.12,89.2,555.13,87.1,556.14,1.0,557.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1299:4:18:[1244.2,1297.2,1293.0,1298.3,558.2,1086.2,296.3,151.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  === Conflict found: 1067:4:19:[673.18,78.0,590.17,1049.2,543.16,1050.4,468.15,1051.5,373.14,1052.7,309.13,1053.8,261.12,1054.9,229.11,1055.10,200.10,1056.11,182.9,1057.12,166.8,1058.13,144.7,1059.14,125.6,1060.15,109.5,1061.16,96.4,1062.17,92.3,1063.19,89.2,1064.20,87.1,1065.21,1.0,1066.22]: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),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1304:3:13:[1281.0,1300.0,151.0,1301.3,1244.2,1302.4,1293.0,1303.5,1067.1,1299.3,638.3,1258.4,296.3]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  === Conflict found: 1086:4:19:[673.18,79.0,590.17,1068.1,543.16,1069.3,468.15,1070.5,373.14,1071.6,309.13,1072.7,261.12,1073.8,229.11,1074.9,200.10,1075.10,182.9,1076.11,166.8,1077.12,144.7,1078.13,125.6,1079.14,109.5,1080.15,96.4,1081.17,92.3,1082.18,89.2,1083.19,87.1,1084.20,1.0,1085.21]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc16, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1307:3:17:[1244.2,1305.1,1293.0,1306.3,1086.1,483.1,558.2,296.3,151.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,skc16,x14,x15,x16),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  === Conflict found: 296:4:11:[200.10,30.0,182.9,286.1,166.8,287.3,144.7,288.4,125.6,289.5,109.5,290.6,96.4,291.7,92.3,292.8,89.2,293.9,87.1,294.11,1.0,295.12]:TopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7),ssPv20_1r1(x0) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1309:4:15:[1293.0,1308.4,296.2,1244.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv16_5r1r1r1r1r1(x0,x11,x12,x13,x14)
% 16.86/4.02  === Conflict found: 1048:4:19:[673.18,77.0,590.17,1030.2,543.16,1031.3,468.15,1032.4,373.14,1033.5,309.13,1034.6,261.12,1035.7,229.11,1036.8,200.10,1037.10,182.9,1038.11,166.8,1039.12,144.7,1040.13,125.6,1041.14,109.5,1042.15,96.4,1043.16,92.3,1044.17,89.2,1045.18,87.1,1046.19,1.0,1047.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) {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}
% 16.86/4.02  === Backtracking. Learning clause 1311:8:30:[1293.0,1310.8,1048.2,1257.2,953.4,558.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x19),ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x20,x21,x22,x23,x24,x25,x26,x27,x28,x29),ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x20,x21,x22,x23),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x20,x21,x22) -> 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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 526
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1304:3:13:[1281.0,1300.0,151.0,1301.3,1244.2,1302.4,1293.0,1303.5,1067.1,1299.3,638.3,1258.4,296.3]:TopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1312:2:12:[1304.3,104.1]:TopTopTopTopTopTopTopTopTopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11) -> 
% 16.86/4.02  === Conflict found: 1309:4:15:[1293.0,1308.4,296.2,1244.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv16_5r1r1r1r1r1(x0,x11,x12,x13,x14) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc28, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc31}
% 16.86/4.02  === Backtracking. Learning clause 1313:4:15:[1309.1,151.1,689.2,638.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14)
% 16.86/4.02  === Conflict found: 1313:4:15:[1309.1,151.1,689.2,638.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,skc24,x7,x8,x9,x10,x11,x12,x13,x14) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc27, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1314:2:17:[1313.4,1067.2,1281.1,104.1,1293.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11) -> 
% 16.86/4.02  === Conflict found: 1247:2:17:[1228.3,151.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc29, x5 -> skc27, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1315:1:16:[1247.2,1296.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,skc29,x4,skc24,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) -> 
% 16.86/4.02  === Conflict found: 1165:4:19:[673.18,83.0,590.17,1147.2,543.16,1148.3,468.15,1149.4,373.14,1150.6,309.13,1151.8,261.12,1152.9,229.11,1153.10,200.10,1154.11,182.9,1155.12,166.8,1156.13,144.7,1157.14,125.6,1158.15,109.5,1159.16,96.4,1160.17,92.3,1161.18,89.2,1162.19,87.1,1163.20,1.0,1164.21]: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),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18) {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, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1316:5:17:[1165.4,1270.1,774.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv18_3r1r1r1(x0,x1,x2),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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv13_8r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7)
% 16.86/4.02  === Conflict found: 774:4:17:[543.16,62.0,468.15,758.2,373.14,759.3,309.13,760.5,261.12,761.6,229.11,762.7,200.10,763.8,182.9,764.9,166.8,765.10,144.7,766.11,125.6,767.12,109.5,768.13,96.4,769.15,92.3,770.16,89.2,771.17,87.1,772.18,1.0,773.19]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1317:6:21:[774.2,845.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16),ssPv17_4r1r1r1r1(x0,x1,x2,x3),ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x17,x18,x19,x20),ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8) -> ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x17,x18,x19)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 590
% 16.86/4.02  === Conflict found: 706:4:17:[543.16,58.0,468.15,690.2,373.14,691.3,309.13,692.4,261.12,693.5,229.11,694.6,200.10,695.7,182.9,696.8,166.8,697.9,144.7,698.10,125.6,699.11,109.5,700.12,96.4,701.13,92.3,702.14,89.2,703.15,87.1,704.16,1.0,705.17]: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),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) {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, x15 -> skc30, x16 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1320:4:22:[137.0,1318.3,119.0,1319.4,706.2,1241.1,655.1,1291.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,skc27,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv20_1r1(x0) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,skc27,x5,x15,x16,x17,x18,skc23,x19,x20,x21)
% 16.86/4.02  === Conflict found: 558:4:15:[373.14,49.0,309.13,544.1,261.12,545.2,229.11,546.4,200.10,547.5,182.9,548.6,166.8,549.7,144.7,550.8,125.6,551.9,109.5,552.10,96.4,553.11,92.3,554.12,89.2,555.13,87.1,556.14,1.0,557.15]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc27, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1324:1:4:[1244.2,1321.0,1293.0,1322.2,104.0,1323.3,558.1,296.3,1286.1,151.1,1296.1]:TopTopTopTop: ssPv17_4r1r1r1r1(x0,x1,x2,x3) -> 
% 16.86/4.02  === Conflict found: 1126:4:20:[810.19,81.0,673.18,1107.2,590.17,1108.3,543.16,1109.4,468.15,1110.5,373.14,1111.6,309.13,1112.7,261.12,1113.8,229.11,1114.9,200.10,1115.10,182.9,1116.11,166.8,1117.12,144.7,1118.13,125.6,1119.14,109.5,1120.15,96.4,1121.16,92.3,1122.17,89.2,1123.18,87.1,1124.19,1.0,1125.20]: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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1328:4:20:[1248.0,1325.3,1324.0,1326.4,1293.0,1327.6,1126.1,1106.2,1067.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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,x15,x16,x17,x18,x19),ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x15,x16) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 599
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 1273:3:18:[1029.1,483.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12),ssPv18_3r1r1r1(x0,x1,x2) -> ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,skc16,x15,x16,x17) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1329:2:10:[1273.3,1315.1]:TopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,skc29,x4,skc24,x5,x6,x7,x8,x9),ssPv18_3r1r1r1(x0,x1,x2) -> 
% 16.86/4.02  === Conflict found: 1281:2:3:[527.2,414.1,100.1]:TopTopTop:  -> ssPv18_3r1r1r1(x0,x1,x2),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1330:1:10:[1281.1,1329.2,1293.1]:TopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,skc29,x4,skc24,x5,x6,x7,x8,x9) -> 
% 16.86/4.02  === Conflict found: 757:4:17:[543.16,61.0,468.15,741.1,373.14,742.2,309.13,743.3,261.12,744.4,229.11,745.5,200.10,746.6,182.9,747.7,166.8,748.8,144.7,749.9,125.6,750.10,109.5,751.11,96.4,752.12,92.3,753.13,89.2,754.14,87.1,755.15,1.0,756.16]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop:  -> 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),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),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}
% 16.86/4.02  === Backtracking. Learning clause 1332:9:32:[1309.0,1331.6,757.1,706.1,1029.2,638.3,1225.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13),ssPv18_3r1r1r1(x0,x1,x2),ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x14,x15,x16,x17,x18,x19,x20,x21,x22,x23,x24,x25,x26),ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x14,x15,x16,x17,x18,x19,x20,x21) -> ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x27,x28,x29,x30,x31),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x14,x15,x16)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 599
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 218:4:9:[166.8,23.0,144.7,210.1,125.6,211.2,109.5,212.4,96.4,213.5,92.3,214.6,89.2,215.7,87.1,216.8,1.0,217.9]:TopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1333:3:9:[218.4,1324.1]:TopTopTopTopTopTopTopTopTop: ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4) -> ssPv12_9r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8),ssPv15_6r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5)
% 16.86/4.02  === Conflict found: 1106:4:20:[810.19,80.0,673.18,1087.1,590.17,1088.2,543.16,1089.3,468.15,1090.5,373.14,1091.6,309.13,1092.7,261.12,1093.8,229.11,1094.9,200.10,1095.10,182.9,1096.11,166.8,1097.12,144.7,1098.13,125.6,1099.14,109.5,1100.15,96.4,1101.16,92.3,1102.17,89.2,1103.18,87.1,1104.19,1.0,1105.20]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14) -> ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,x17,x18,x19),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> 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}
% 16.86/4.02  === Backtracking. Learning clause 1337:1:17:[1324.0,1334.1,1293.0,1335.2,104.0,1336.3,1106.2,1126.1,558.2,296.3,151.1,1244.3,1314.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,x4,x5,skc24,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16) -> 
% 16.86/4.02  === Conflict found: 1126:4:20:[810.19,81.0,673.18,1107.2,590.17,1108.3,543.16,1109.4,468.15,1110.5,373.14,1111.6,309.13,1112.7,261.12,1113.8,229.11,1114.9,200.10,1115.10,182.9,1116.11,166.8,1117.12,144.7,1118.13,125.6,1119.14,109.5,1120.15,96.4,1121.16,92.3,1122.17,89.2,1123.18,87.1,1124.19,1.0,1125.20]: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),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv17_4r1r1r1r1(x0,x1,x2,x3) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30, x16 -> skc30, x17 -> skc30, x18 -> skc30, x19 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1341:3:16:[1248.0,1338.2,1324.0,1339.3,1293.0,1340.5,1126.1,1146.2,1067.3,1029.4]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15),ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  === Clause set with instances from active satisfied. Growing active. New size: 608
% 16.86/4.02  === Restarting.
% 16.86/4.02  === Conflict found: 689:4:16:[468.15,57.0,373.14,674.2,309.13,675.3,261.12,676.4,229.11,677.6,200.10,678.8,182.9,679.9,166.8,680.10,144.7,681.11,125.6,682.12,109.5,683.13,96.4,684.14,92.3,685.15,89.2,686.16,87.1,687.17,1.0,688.18]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) -> ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30, x15 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1342:4:16:[689.3,1257.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: 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) -> 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)
% 16.86/4.02  === Conflict found: 239:4:10:[182.9,25.0,166.8,230.2,144.7,231.3,125.6,232.4,109.5,233.5,96.4,234.6,92.3,235.7,89.2,236.8,87.1,237.10,1.0,238.11]:TopTopTopTopTopTopTopTopTopTop: ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv20_1r1(x0) -> 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 -> skc31, x5 -> skc29, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1343:3:10:[239.4,119.1,1257.2]:TopTopTopTopTopTopTopTopTopTop: ssPv20_1r1(x0),ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5,x6,x7,x8,x9) -> ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,skc29,x5)
% 16.86/4.02  === Conflict found: 1262:5:15:[1106.2,1225.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14),ssPv14_7r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6) -> ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4),ssPv19_2r1r1(x0,x1),ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc31, x5 -> skc29, x6 -> skc30, x7 -> skc24, x8 -> skc30, x9 -> skc30, x10 -> skc30, x11 -> skc30, x12 -> skc30, x13 -> skc30, x14 -> skc30}
% 16.86/4.02  === Backtracking. Learning clause 1346:3:11:[1257.2,1344.0,1293.0,1345.4,1262.1,558.2]:TopTopTopTopTopTopTopTopTopTopTop: ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) -> ssPv11_10r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9),ssPv16_5r1r1r1r1r1(x0,x1,x2,x3,x4)
% 16.86/4.02  === Conflict found: 1330:1:10:[1281.1,1329.2,1293.1]:TopTopTopTopTopTopTopTopTopTop: ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(x0,x1,x2,x3,skc31,skc29,x4,skc24,x5,x6,x7,x8,x9) ->  {x0 -> skc30, x1 -> skc30, x2 -> skc30, x3 -> skc30, x4 -> skc30, x5 -> skc30, x6 -> skc30, x7 -> skc30, x8 -> skc30, x9 -> skc22}
% 16.86/4.02  
% 16.86/4.02  SZS status Unsatisfiable
% 16.86/4.02  
% 16.86/4.02  Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.86/4.02  
% 16.86/4.02  SPASS-SCL-FOL Statistics:
% 16.86/4.02  Number of learned clauses: 90
% 16.86/4.02  Number of propagations: 9495
% 16.86/4.02  Number of decisions: 3919
% 16.86/4.02  Number of resolutions: 154
% 16.86/4.02  Number of condensations: 12
% 16.86/4.02  Number of sub resolutions: 1170
% 16.86/4.02  Number of input literals (deduplicated): 56
% 16.86/4.02  Number of grows: 33
% 16.86/4.02  Number of considered ground atoms: 608
% 16.86/4.02  
% 16.86/4.02   Needed:       0:00:03.41
% 16.86/4.02  
%------------------------------------------------------------------------------