SPASS-SCL---0.1.CSA-Ass.s

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

% Computer : n020.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:39:49 PM UTC 2026

% Result   : CounterSatisfiable 98.14s 25.03s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : SYN446+1 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.12  % Command  : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.33  % Computer : n020.cluster.edu
% 0.16/0.33  % Model    : x86_64 x86_64
% 0.16/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33  % Memory   : 8042.1875MB
% 0.16/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33  % CPULimit : 300
% 0.16/0.33  % WCLimit  : 300
% 0.16/0.33  % DateTime : Thu May  7 13:44:35 EDT 2026
% 0.16/0.34  % CPUTime  : 
% 0.16/0.34  SPASS-SCL-FOL version:
% 0.19/0.42  SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 98.14/25.03  Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.14/25.03  Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.14/25.03  Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.14/25.03  Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.14/25.03  Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.14/25.03  Execution resolution_3 ended with status: satisfiable
% 98.14/25.03  Used heuristic: resolution_3
% 98.14/25.03  
% 98.14/25.03   Input Clauses:
% 98.14/25.03  
% 98.14/25.03   Predicates: hskp0 ndr1_0 c1_1 c0_1 c2_1 hskp1 c3_1 hskp2 hskp3 hskp4 hskp5 hskp6 hskp7 hskp8 hskp9 hskp10 hskp11 hskp12 hskp13 hskp14 hskp15 hskp16 hskp17 hskp18 hskp19 hskp20 hskp21 hskp22 hskp23 hskp24 hskp25 hskp26 hskp27 hskp28 hskp29 hskp30 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 
% 98.14/25.03   Fol Constants: a375 a376 a377 a378 a379 a380 a381 a384 a385 a387 a392 a394 a395 a396 a398 a399 a400 a401 a404 a407 a409 a411 a418 a420 a424 a425 a427 a374 a386 a390 a397 
% 98.14/25.03   Fol Functions: 
% 98.14/25.03   Problem Properties:
% 98.14/25.03   This is a Bernays Schoenfinkel problem.
% 98.14/25.03  
% 98.14/25.03   After reduction:  Problem Properties:
% 98.14/25.03   This is a Bernays Schoenfinkel problem.
% 98.14/25.03  
% 98.14/25.03  
% 98.14/25.03   Reduced Input Clauses:
% 98.14/25.03  216:7:2:[200.1,162.5]:TopTop: c3_1(x0),ndr1_0,c2_1(x1) -> c0_1(x0),c1_1(x0),c3_1(x1),hskp6
% 98.14/25.03  
% 98.14/25.03   Most General Atoms: ren1 ndr1_0 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 hskp0 hskp1 hskp2 hskp3 hskp4 hskp5 hskp6 hskp7 hskp8 hskp9 hskp10 hskp11 hskp12 hskp13 hskp14 hskp15 hskp16 hskp17 hskp18 hskp19 hskp20 hskp21 hskp22 hskp23 hskp24 hskp25 hskp26 hskp27 hskp28 hskp29 hskp30 c1_1(x2) c2_1(x2) c3_1(x0) c0_1(x2) 
% 98.14/25.03  
% 98.14/25.03  === Starting SPASS-SCL-FOL A Little Less Naive, considering 51 atoms initially, heuristics mode: resolution_3 ===
% 98.14/25.03  
% 98.14/25.03  === Backtracking. Learning clause 217:2:0:[1.1,125.2]:: hskp0 -> ndr1_0
% 98.14/25.03  === Clause set with instances from active satisfied. Growing active. New size: 127
% 98.14/25.03  === Restarting.
% 98.14/25.03  === Clause set with instances from active satisfied. Growing active. New size: 168
% 98.14/25.03  === Restarting.
% 98.14/25.03  === Backtracking. Learning clause 221:7:1:[70.1,218.0,9.1,219.1,11.1,220.8,166.9,12.2,71.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren3,ren18 -> c0_1(a377),c0_1(a401)
% 98.14/25.03  === Conflict found: 221:7:1:[70.1,218.0,9.1,219.1,11.1,220.8,166.9,12.2,71.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren3,ren18 -> c0_1(a377),c0_1(a401) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 223:6:0:[114.1,222.1,221.3,115.2]:: c0_1(a386),ren3,ren18,ren29 -> c0_1(a377),c0_1(a401)
% 98.14/25.03  === Backtracking. Learning clause 228:9:0:[9.1,224.0,22.1,225.5,23.1,226.6,31.1,227.9,164.6,39.2,30.2,24.2,38.2,221.3]:: c0_1(a387),ren8,ren6,ren10,ren3,ren18 -> c1_1(a384),c0_1(a377),c0_1(a401)
% 98.14/25.03  === Backtracking. Learning clause 232:7:1:[9.1,229.2,70.1,230.4,11.1,231.8,166.9,12.2,71.2]:Top: c1_1(x0),c2_1(x0),c0_1(a401),ren3,ren18 -> c0_1(a377),c0_1(x0)
% 98.14/25.03  === Backtracking. Learning clause 236:5:0:[6.1,233.0,5.1,234.1,31.1,235.6,164.6,39.2,30.2,8.2,38.2,7.2]:: c0_1(a387),ren8,ren10,ren2 -> c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 240:7:1:[37.1,237.1,40.1,238.6,55.1,239.7,161.8,56.2,39.2]:Top: c2_1(a396),c0_1(x0),ren14,ren10 -> c0_1(a387),c1_1(x0),c2_1(x0)
% 98.14/25.03  === Backtracking. Learning clause 244:7:1:[114.1,241.1,57.1,242.2,59.1,243.9,169.10,60.2,115.2]:Top: c1_1(x0),c2_1(a398),ren15,ren29 -> c0_1(x0),c2_1(x0),c0_1(a386)
% 98.14/25.03  === Backtracking. Learning clause 250:12:0:[54.1,245.0,114.1,246.1,5.1,247.2,6.1,248.4,55.1,249.11,169.10,68.2,115.2,67.2,240.1,7.2,223.1]:: ren17,ren14,ren10,ren2,ren3,ren18,ren29 -> c1_1(a400),c0_1(a387),c1_1(a376),c0_1(a377),c0_1(a401)
% 98.14/25.03  === Backtracking. Learning clause 254:14:0:[5.1,251.0,54.1,252.1,40.1,253.11,160.3,79.2,56.2,232.2,38.2,78.2,250.12,55.2,236.1]:: ren20,ren17,ren3,ren18,ren29,ren14,ren8,ren10,ren2 -> c1_1(a407),c1_1(a400),c1_1(a376),c0_1(a377),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 259:6:0:[122.1,255.0,23.1,256.1,13.1,257.3,14.1,258.4,194.10,24.2,15.2,123.2]:: c2_1(a380),c2_1(a378),ren6,ren4,ren31 -> c1_1(a397)
% 98.14/25.03  === Backtracking. Learning clause 265:9:0:[70.1,260.0,5.1,261.1,114.1,262.3,6.1,263.6,55.1,264.10,166.9,56.2,115.2,71.2,240.1,7.2]:: c0_1(a386),ren29,ren18,ren14,ren10,ren2 -> c0_1(a401),c0_1(a387),c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0)
% 98.14/25.03  === Backtracking. Learning clause 274:10:0:[54.1,269.0,114.1,270.1,5.1,271.2,6.1,272.4,55.1,273.10,169.10,68.2,115.2,67.2,240.1,7.2,265.1]:: ren17,ren29,ren18,ren14,ren10,ren2 -> c1_1(a400),c0_1(a401),c0_1(a387),c1_1(a376)
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a378, x1 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 276:11:2:[70.1,275.3,268.5,71.2,240.1]:TopTop: c1_1(x0),c2_1(x0),c0_1(a401),ren18,c0_1(x1),ren14,ren10 -> c0_1(x0),c0_1(a387),c1_1(x1),c2_1(x1)
% 98.14/25.03  === Backtracking. Learning clause 280:8:0:[5.1,277.0,54.1,278.1,40.1,279.7,160.3,79.2,56.2,240.1,38.2,7.2,78.2,236.1,6.2]:: ren14,ren20,ren8,ren10,ren2 -> c1_1(a407),c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 284:6:0:[5.1,281.0,6.1,282.1,40.1,283.6,161.8,84.2,39.2,82.2,7.2]:: ren10,ren21,ren2 -> c0_1(a387),c0_1(a409),c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 286:7:0:[5.1,285.0,175.7,92.2,8.2,90.2,82.2,91.2,284.5,236.1,6.2,83.2]:: ren23,ren8,ren10,ren2,ren21 -> c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 290:6:0:[10.1,287.1,9.1,288.2,31.1,289.7,168.6,39.2,12.2,38.2,32.2]:: c1_1(a384),c0_1(a387),ren3,ren10,ren8 -> c0_1(a377)
% 98.14/25.03  === Backtracking. Learning clause 295:13:0:[5.1,291.0,54.1,292.1,254.13,293.8,40.1,294.12,160.3,79.2,56.2,232.2,38.2,78.2,250.12,55.2,290.2]:: ren20,ren17,ren2,ren18,ren29,ren14,ren3,ren10,ren8 -> c1_1(a407),c1_1(a400),c1_1(a376),c0_1(a377)
% 98.14/25.03  === Backtracking. Learning clause 300:6:1:[9.1,296.2,10.1,297.3,40.1,298.8,11.1,299.9,160.3,39.2,12.2]:Top: c2_1(x0),c0_1(a387),ren10,ren3 -> c0_1(x0),c1_1(x0)
% 98.14/25.03  === Conflict found: 300:6:1:[9.1,296.2,10.1,297.3,40.1,298.8,11.1,299.9,160.3,39.2,12.2]:Top: c2_1(x0),c0_1(a387),ren10,ren3 -> c0_1(x0),c1_1(x0) {x0 -> a409}
% 98.14/25.03  === Backtracking. Learning clause 302:5:0:[83.1,301.5,300.1,82.2]:: c0_1(a387),ren10,ren3,ren21 -> c0_1(a409)
% 98.14/25.03  === Conflict found: 300:6:1:[9.1,296.2,10.1,297.3,40.1,298.8,11.1,299.9,160.3,39.2,12.2]:Top: c2_1(x0),c0_1(a387),ren10,ren3 -> c0_1(x0),c1_1(x0) {x0 -> a411}
% 98.14/25.03  === Backtracking. Learning clause 303:5:0:[300.1,86.2,88.2]:: c0_1(a387),ren10,ren3,ren22 -> c1_1(a411)
% 98.14/25.03  === Backtracking. Learning clause 307:13:0:[5.1,304.0,54.1,305.1,40.1,306.11,160.3,79.2,56.2,276.2,38.2,7.2,78.2,274.8,55.2,303.1,6.2]:: ren20,ren17,ren29,ren18,ren14,ren10,ren3,ren22,ren2 -> c1_1(a407),c1_1(a400),c1_1(a376),c1_1(a411)
% 98.14/25.03  === Conflict found: 300:6:1:[9.1,296.2,10.1,297.3,40.1,298.8,11.1,299.9,160.3,39.2,12.2]:Top: c2_1(x0),c0_1(a387),ren10,ren3 -> c0_1(x0),c1_1(x0) {x0 -> a418}
% 98.14/25.03  === Backtracking. Learning clause 308:5:0:[300.1,90.2,91.2]:: c0_1(a387),ren10,ren3,ren23 -> c1_1(a418)
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a411, x1 -> a380}
% 98.14/25.03  === Backtracking. Learning clause 313:12:2:[276.7,309.1,54.1,310.5,88.1,311.11,55.1,312.12,268.2,86.2,276.2]:TopTop: c1_1(a411),c1_1(x0),c2_1(x0),ren22,c0_1(a401),ren18,c0_1(x1),ren14,ren10 -> c0_1(a387),c1_1(x1),c2_1(x1)
% 98.14/25.03  === Conflict found: 313:12:2:[276.7,309.1,54.1,310.5,88.1,311.11,55.1,312.12,268.2,86.2,276.2]:TopTop: c1_1(a411),c1_1(x0),c2_1(x0),ren22,c0_1(a401),ren18,c0_1(x1),ren14,ren10 -> c0_1(a387),c1_1(x1),c2_1(x1) {x0 -> a401, x1 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 315:13:0:[70.1,314.1,313.3,71.2,7.2,274.8,308.1,6.2]:: c1_1(a411),ren22,ren17,ren29,ren18,ren14,ren10,ren3,ren23,ren2 -> c1_1(a400),c1_1(a376),c1_1(a418)
% 98.14/25.03  === Backtracking. Learning clause 318:6:0:[9.1,316.1,47.1,317.7,164.1,46.2,39.2,12.2,38.2,11.2]:: c0_1(a377),c0_1(a387),ren12,ren10,ren3 -> c0_1(a394)
% 98.14/25.03  === Backtracking. Learning clause 323:6:0:[54.1,319.1,13.1,320.3,14.1,321.4,83.1,322.9,194.10,56.2,15.2,82.2]:: c0_1(a409),c2_1(a396),c2_1(a378),ren14,ren4,ren21 -> 
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a411, x1 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 326:9:0:[114.1,324.2,88.1,325.10,268.5,115.2,86.2,323.2]:: c1_1(a411),c0_1(a386),ren29,ren22,c0_1(a409),c2_1(a378),ren14,ren4,ren21 -> 
% 98.14/25.03  === Backtracking. Learning clause 330:5:0:[54.1,327.1,29.1,328.2,31.1,329.7,168.10,56.2,39.2,38.2,32.2,55.2]:: c1_1(a384),c0_1(a387),ren10,ren8,ren14 -> 
% 98.14/25.03  === Conflict found: 313:12:2:[276.7,309.1,54.1,310.5,88.1,311.11,55.1,312.12,268.2,86.2,276.2]:TopTop: c1_1(a411),c1_1(x0),c2_1(x0),ren22,c0_1(a401),ren18,c0_1(x1),ren14,ren10 -> c0_1(a387),c1_1(x1),c2_1(x1) {x0 -> a401, x1 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 333:13:0:[70.1,331.0,280.7,332.1,313.3,71.2,7.2,274.8,330.2,6.2,307.13]:: ren8,ren20,ren17,ren29,ren18,ren14,ren10,ren3,ren22,ren2 -> c1_1(a407),c1_1(a400),c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 335:7:0:[5.1,334.0,175.7,92.2,8.2,90.2,82.2,91.2,284.5,330.2,6.2,83.2,286.7]:: ren14,ren23,ren8,ren10,ren2,ren21 -> c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 342:11:0:[54.1,336.0,114.1,337.1,9.1,338.2,50.1,339.4,55.1,340.11,51.1,341.14,169.10,68.2,115.2,67.2,240.1,52.2,223.1]:: ren17,ren14,ren10,ren13,ren3,ren18,ren29 -> c1_1(a400),c0_1(a387),c0_1(a377),c0_1(a401)
% 98.14/25.03  === Backtracking. Learning clause 346:7:1:[78.1,343.1,5.1,344.2,7.1,345.9,160.3,79.2,8.2]:Top: c2_1(x0),c1_1(a376),ren20,ren2 -> c0_1(x0),c1_1(x0),c1_1(a407)
% 98.14/25.03  === Conflict found: 346:7:1:[78.1,343.1,5.1,344.2,7.1,345.9,160.3,79.2,8.2]:Top: c2_1(x0),c1_1(a376),ren20,ren2 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 348:7:0:[40.1,347.5,346.1,38.2,236.1]:: c1_1(a376),ren20,ren8,ren10,ren2 -> c1_1(a407),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 353:5:0:[37.1,349.0,50.1,350.1,40.1,351.6,51.1,352.8,161.8,84.2,39.2,82.2,52.2]:: ren10,ren21,ren13 -> c0_1(a387),c0_1(a409)
% 98.14/25.03  === Backtracking. Learning clause 355:7:0:[5.1,354.0,175.7,92.2,84.2,90.2,82.2,91.2,353.5,236.1,83.2]:: ren23,ren13,ren8,ren10,ren2,ren21 -> c1_1(a384)
% 98.14/25.03  === Conflict found: 346:7:1:[78.1,343.1,5.1,344.2,7.1,345.9,160.3,79.2,8.2]:Top: c2_1(x0),c1_1(a376),ren20,ren2 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 358:7:0:[348.6,356.3,40.1,357.7,346.1,38.2,330.2]:: c1_1(a376),ren20,ren2,ren10,ren8,ren14 -> c1_1(a407)
% 98.14/25.03  === Backtracking. Learning clause 359:8:0:[175.7,92.2,84.2,90.2,82.2,91.2,353.5,330.2,83.2,355.7,147.2,145.2,138.2,137.2,134.2,132.2,126.2]:: ndr1_0,hskp22,hskp20,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Backtracking. Learning clause 362:14:0:[9.1,360.0,54.1,361.2,197.5,79.2,56.2,232.2,78.2,342.11,55.2,330.2]:: c1_1(a407),ren20,ren17,ren13,ren3,ren18,ren29,c1_1(a384),ren10,ren8,ren14 -> hskp22,c1_1(a400),c0_1(a377)
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a401, x1 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 365:9:0:[70.1,363.0,114.1,364.2,268.5,115.2,71.2,323.2]:: c0_1(a386),ren29,ren18,c0_1(a409),c2_1(a378),ren14,ren4,ren21 -> c0_1(a401)
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a401, x1 -> a380}
% 98.14/25.03  === Backtracking. Learning clause 369:9:1:[70.1,366.0,50.1,367.5,51.1,368.11,268.2,71.2,240.1,52.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren18,ren14,ren10,ren13 -> c0_1(a401),c0_1(a387)
% 98.14/25.03  === Conflict found: 369:9:1:[70.1,366.0,50.1,367.5,51.1,368.11,268.2,71.2,240.1,52.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren18,ren14,ren10,ren13 -> c0_1(a401),c0_1(a387) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 371:8:0:[114.1,370.1,369.3,115.2]:: c0_1(a386),ren18,ren14,ren10,ren13,ren29 -> c0_1(a401),c0_1(a387)
% 98.14/25.03  === Backtracking. Learning clause 375:6:0:[70.1,372.1,29.1,373.2,31.1,374.6,169.10,68.2,71.2,67.2,32.2]:: c1_1(a384),ren18,ren17,ren8 -> c0_1(a401),c1_1(a400)
% 98.14/25.03  === Conflict found: 276:11:2:[70.1,275.3,268.5,71.2,240.1]:TopTop: c1_1(x0),c2_1(x0),c0_1(a401),ren18,c0_1(x1),ren14,ren10 -> c0_1(x0),c0_1(a387),c1_1(x1),c2_1(x1) {x0 -> a378, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 378:9:1:[50.1,376.4,51.1,377.10,276.11,52.2]:Top: c1_1(x0),c2_1(x0),c0_1(a401),ren18,ren14,ren10,ren13 -> c0_1(x0),c0_1(a387)
% 98.14/25.03  === Backtracking. Learning clause 381:12:0:[5.1,379.0,54.1,380.1,197.5,79.2,56.2,378.2,78.2,375.5,55.2,330.2,358.7]:: ren13,ren18,ren17,c1_1(a384),c1_1(a376),ren20,ren2,ren10,ren8,ren14 -> hskp22,c1_1(a400)
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a378, x1 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 383:10:1:[66.1,382.2,268.5,67.2,323.2]:Top: c1_1(x0),c2_1(x0),c1_1(a400),ren17,c0_1(a409),c2_1(a378),ren14,ren4,ren21 -> c0_1(x0)
% 98.14/25.03  === Conflict found: 369:9:1:[70.1,366.0,50.1,367.5,51.1,368.11,268.2,71.2,240.1,52.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren18,ren14,ren10,ren13 -> c0_1(a401),c0_1(a387) {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 385:8:0:[66.1,384.0,369.3,67.2]:: c1_1(a400),ren18,ren14,ren10,ren13,ren17 -> c0_1(a401),c0_1(a387)
% 98.14/25.03  === Backtracking. Learning clause 388:13:0:[9.1,386.0,54.1,387.2,197.5,79.2,56.2,232.2,78.2,385.7,55.2,330.2]:: c1_1(a407),ren3,ren20,c1_1(a400),ren18,ren13,ren17,c1_1(a384),ren10,ren8,ren14 -> hskp22,c0_1(a377)
% 98.14/25.03  === Backtracking. Learning clause 390:11:0:[5.1,389.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,358.7,381.12,54.2,355.7,335.7]:: ren18,ren17,ren20,ren13,ren14,ren23,ren8,ren10,ren2,ren21 -> hskp22
% 98.14/25.03  === Backtracking. Learning clause 394:14:0:[5.1,391.0,254.9,392.1,54.1,393.2,197.5,79.2,56.2,232.2,78.2,250.12,55.2,236.1]:: ren20,ren17,ren3,ren18,ren29,ren14,ren8,ren10,ren2 -> hskp22,c1_1(a400),c1_1(a376),c0_1(a377),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 397:13:0:[5.1,395.0,54.1,396.1,197.5,79.2,56.2,378.2,78.2,274.8,55.2,236.1,280.6]:: ren13,ren17,ren29,ren18,ren14,ren20,ren8,ren10,ren2 -> hskp22,c1_1(a400),c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 401:13:0:[5.1,398.0,54.1,399.2,388.7,400.15,197.5,79.2,56.2,232.2,78.2,385.7,55.2,236.1]:: c1_1(a407),ren3,ren20,c1_1(a400),ren18,ren13,ren17,ren14,ren8,ren10,ren2 -> hskp22,c0_1(a377)
% 98.14/25.03  === Backtracking. Learning clause 403:12:0:[5.1,402.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,236.1,280.6,397.11,54.2]:: ren13,ren17,ren29,ren18,ren20,ren8,ren10,ren2,ren14 -> hskp22,c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 407:14:0:[5.1,404.0,54.1,405.1,397.12,406.3,197.5,79.2,56.2,378.2,78.2,375.5,55.2,330.2,333.11]:: ren13,ren8,ren20,ren17,ren29,ren18,ren14,ren10,ren3,ren22,ren2 -> hskp22,c1_1(a400),c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 411:12:0:[9.1,408.0,54.1,409.1,40.1,410.12,160.3,79.2,56.2,232.2,38.2,78.2,385.7,55.2,330.2]:: ren3,ren20,c1_1(a400),ren18,ren13,ren17,c1_1(a384),ren10,ren8,ren14 -> c1_1(a407),c0_1(a377)
% 98.14/25.03  === Backtracking. Learning clause 415:10:0:[29.1,412.0,54.1,413.1,40.1,414.11,160.3,79.2,56.2,378.2,38.2,78.2,385.7,55.2,330.2]:: ren20,c1_1(a400),ren18,ren13,ren17,c1_1(a384),ren10,ren8,ren14 -> c1_1(a407)
% 98.14/25.03  === Backtracking. Learning clause 417:13:0:[5.1,416.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,415.10,407.13,54.2,403.12]:: ren3,ren22,ren13,ren17,ren29,ren18,ren20,ren8,ren10,ren2,ren14 -> hskp22,c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 421:14:0:[5.1,418.0,54.1,419.2,401.3,420.14,197.5,79.2,56.2,232.2,78.2,342.11,55.2,236.1]:: c1_1(a407),ren20,ren17,ren13,ren3,ren18,ren29,ren14,ren8,ren10,ren2 -> hskp22,c0_1(a377),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 426:9:0:[54.1,422.0,114.1,423.1,13.1,424.2,55.1,425.10,169.10,68.2,115.2,67.2,323.2]:: ren29,ren17,c0_1(a409),c2_1(a378),ren14,ren4,ren21 -> c0_1(a386),c1_1(a400)
% 98.14/25.03  === Backtracking. Learning clause 432:10:0:[14.1,427.0,114.1,428.1,13.1,429.2,16.1,430.11,385.0,431.12,169.10,68.2,115.2,67.2,426.4,371.1,353.5]:: ren17,ren4,ren18,ren14,ren29,ren10,ren21,ren13 -> c0_1(a401),c0_1(a387)
% 98.14/25.03  === Backtracking. Learning clause 435:13:0:[5.1,433.0,403.10,434.7,197.5,79.2,56.2,378.2,78.2,432.9,55.2,236.1,358.7,54.2]:: ren17,ren4,ren18,ren29,ren21,ren13,ren20,ren2,ren10,ren8,ren14 -> hskp22,c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 437:14:0:[359.1,436.14,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,358.7,381.12,54.2,435.13,417.13,153.2,146.2,145.2,144.2,142.2,141.2,138.2,137.2,134.2,132.2,128.2,127.2,126.2]:: ndr1_0,hskp28,hskp21,hskp20,hskp19,hskp17,hskp16,hskp13,hskp12,hskp9,hskp7,hskp3,hskp2,hskp1 -> 
% 98.14/25.03  === Backtracking. Learning clause 439:14:0:[5.1,438.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,358.7,381.12,54.2,435.13,417.13]:: ren4,ren21,ren3,ren22,ren13,ren17,ren29,ren18,ren20,ren8,ren10,ren2,ren14 -> hskp22
% 98.14/25.03  === Backtracking. Learning clause 443:7:1:[70.1,440.1,57.1,441.2,59.1,442.9,169.10,60.2,71.2]:Top: c1_1(x0),c2_1(a398),ren15,ren18 -> c0_1(x0),c2_1(x0),c0_1(a401)
% 98.14/25.03  === Backtracking. Learning clause 449:9:0:[54.1,444.0,70.1,445.1,5.1,446.2,6.1,447.5,55.1,448.9,169.10,68.2,71.2,67.2,240.1,7.2]:: ren18,ren17,ren14,ren10,ren2 -> c0_1(a401),c1_1(a400),c0_1(a387),c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 453:13:0:[5.1,450.0,280.5,451.1,54.1,452.2,197.5,79.2,56.2,232.2,78.2,449.6,55.2,236.1]:: ren3,ren20,ren18,ren17,ren14,ren8,ren10,ren2 -> hskp22,c0_1(a377),c1_1(a400),c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 456:12:0:[5.1,454.0,54.1,455.1,197.5,79.2,56.2,378.2,78.2,449.6,55.2,236.1,280.6]:: ren13,ren18,ren17,ren14,ren20,ren8,ren10,ren2 -> hskp22,c1_1(a400),c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 458:11:0:[5.1,457.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,236.1,280.6,456.10,54.2]:: ren13,ren18,ren17,ren20,ren8,ren10,ren2,ren14 -> hskp22,c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 462:11:0:[9.1,459.0,54.1,460.1,40.1,461.10,160.3,79.2,56.2,232.2,38.2,78.2,375.5,55.2,330.2]:: ren3,ren20,ren18,ren17,c1_1(a384),ren10,ren8,ren14 -> c1_1(a407),c0_1(a377),c1_1(a400)
% 98.14/25.03  === Backtracking. Learning clause 467:9:0:[29.1,463.0,54.1,464.1,40.1,465.10,415.1,466.12,160.3,79.2,56.2,378.2,38.2,78.2,375.5,55.2,330.2]:: ren13,ren20,ren18,ren17,c1_1(a384),ren10,ren8,ren14 -> c1_1(a407)
% 98.14/25.03  === Backtracking. Learning clause 470:11:0:[9.1,468.0,54.1,469.2,197.5,79.2,56.2,232.2,78.2,375.5,55.2]:: c1_1(a407),ren3,ren20,c1_1(a384),ren18,ren17,ren8,ren14 -> hskp22,c0_1(a377),c1_1(a400)
% 98.14/25.03  === Backtracking. Learning clause 473:10:0:[29.1,471.0,54.1,472.1,197.5,79.2,56.2,378.2,78.2,375.5,55.2,330.2,467.9]:: ren13,ren20,ren18,ren17,c1_1(a384),ren10,ren8,ren14 -> hskp22,c1_1(a400)
% 98.14/25.03  === Backtracking. Learning clause 475:10:0:[5.1,474.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,467.9,473.10,54.2,458.11]:: ren13,ren18,ren17,ren20,ren8,ren10,ren2,ren14 -> hskp22,c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 480:9:0:[54.1,476.0,70.1,477.1,13.1,478.2,55.1,479.10,169.10,68.2,71.2,67.2,323.2]:: ren18,ren17,c0_1(a409),c2_1(a378),ren14,ren4,ren21 -> c0_1(a401),c1_1(a400)
% 98.14/25.03  === Backtracking. Learning clause 486:9:0:[14.1,481.0,70.1,482.1,13.1,483.2,16.1,484.10,385.0,485.12,169.10,68.2,71.2,67.2,480.4,353.5]:: ren18,ren17,ren14,ren4,ren10,ren21,ren13 -> c0_1(a401),c0_1(a387)
% 98.14/25.03  === Backtracking. Learning clause 489:15:0:[5.1,487.0,54.1,488.2,197.5,79.2,56.2,232.2,78.2,486.8,55.2,236.1]:: c1_1(a407),ren3,ren20,ren18,ren17,ren4,ren21,ren13,ren14,ren8,ren10,ren2 -> hskp22,c0_1(a377),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 492:12:0:[5.1,490.0,458.9,491.6,197.5,79.2,56.2,378.2,78.2,486.8,55.2,236.1,358.7,54.2]:: ren18,ren17,ren4,ren21,ren13,ren20,ren2,ren10,ren8,ren14 -> hskp22,c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 493:11:0:[197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,358.7,381.12,54.2,492.12,475.10,145.2,144.2,142.2,141.2,138.2,137.2,134.2,132.2,128.2,126.2,359.2]:: hskp19,hskp17,hskp16,hskp3,ndr1_0,hskp20,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Backtracking. Learning clause 495:9:0:[5.1,494.0,189.6,60.2,80.2,78.2,58.2,358.7,59.2,335.7,147.2]:: ren20,ren15,ren14,ren8,ren10,ren2,ren21,hskp22 -> hskp20
% 98.14/25.03  === Backtracking. Learning clause 497:8:0:[5.1,496.0,189.6,8.2,80.2,78.2,6.2,280.6]:: ren14,ren20,ren8,ren10,ren2 -> hskp20,c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 499:10:0:[5.1,498.0,189.6,8.2,80.2,78.2,6.2,467.9,497.8]:: ren13,ren18,ren17,ren14,ren20,ren8,ren10,ren2 -> hskp20,c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 500:11:0:[189.6,60.2,80.2,78.2,58.2,358.7,59.2,499.10,144.2,142.2,141.2,139.2,138.2,137.2,134.2,132.2,126.2,493.6]:: hskp14,hskp19,hskp17,hskp16,hskp3,ndr1_0,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Conflict found: 439:14:0:[5.1,438.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,358.7,381.12,54.2,435.13,417.13]:: ren4,ren21,ren3,ren22,ren13,ren17,ren29,ren18,ren20,ren8,ren10,ren2,ren14 -> hskp22 {}
% 98.14/25.03  === Backtracking. Learning clause 501:14:0:[439.7,153.2,146.2,145.2]:: ren4,ren3,ren13,ren17,ren18,ren20,ren8,ren10,ren2,ren14,hskp28,hskp21,hskp20 -> hskp22
% 98.14/25.03  === Backtracking. Learning clause 503:9:0:[5.1,502.0,187.1,46.2,82.2,48.2,353.5,330.2,83.2,47.2,355.7]:: ren14,ren12,ren23,ren13,ren8,ren10,ren2,ren21 -> hskp19
% 98.14/25.03  === Backtracking. Learning clause 505:7:0:[5.1,504.0,187.1,30.2,82.2,32.2,284.5,236.1,83.2]:: ren8,ren10,ren2,ren21 -> hskp19,c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 507:8:0:[5.1,506.0,187.1,46.2,82.2,48.2,284.5,330.2,83.2,47.2,505.7]:: ren14,ren12,ren8,ren10,ren2,ren21 -> hskp19,c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 509:7:0:[5.1,508.0,187.1,30.2,82.2,32.2,353.5,236.1,83.2]:: ren13,ren8,ren10,ren2,ren21 -> hskp19,c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 510:9:0:[187.1,46.2,82.2,48.2,353.5,330.2,83.2,47.2,509.7,145.2,138.2,137.2,136.2,134.2,132.2,126.2]:: ndr1_0,hskp20,hskp13,hskp12,hskp11,hskp9,hskp7,hskp1 -> hskp19
% 98.14/25.03  === Backtracking. Learning clause 513:6:1:[29.1,511.0,32.1,512.5,187.1,30.2]:Top: c0_1(x0),c2_1(x0),ren8 -> c1_1(a384),c1_1(x0),hskp19
% 98.14/25.03  === Conflict found: 513:6:1:[29.1,511.0,32.1,512.5,187.1,30.2]:Top: c0_1(x0),c2_1(x0),ren8 -> c1_1(a384),c1_1(x0),hskp19 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 514:5:0:[513.2,67.2,66.2]:: ren8,ren17 -> c1_1(a384),c1_1(a400),hskp19
% 98.14/25.03  === Conflict found: 513:6:1:[29.1,511.0,32.1,512.5,187.1,30.2]:Top: c0_1(x0),c2_1(x0),ren8 -> c1_1(a384),c1_1(x0),hskp19 {x0 -> a397}
% 98.14/25.03  === Backtracking. Learning clause 515:5:0:[513.2,123.2,122.2]:: ren8,ren31 -> c1_1(a384),c1_1(a397),hskp19
% 98.14/25.03  === Backtracking. Learning clause 517:10:0:[5.1,516.0,189.6,60.2,80.2,78.2,58.2,358.7,59.2,499.10]:: ren15,ren13,ren18,ren17,ren14,ren20,ren8,ren10,ren2 -> hskp20
% 98.14/25.03  === Conflict found: 503:9:0:[5.1,502.0,187.1,46.2,82.2,48.2,353.5,330.2,83.2,47.2,355.7]:: ren14,ren12,ren23,ren13,ren8,ren10,ren2,ren21 -> hskp19 {}
% 98.14/25.03  === Backtracking. Learning clause 518:9:0:[503.3,147.2]:: ren14,ren12,ren13,ren8,ren10,ren2,ren21,hskp22 -> hskp19
% 98.14/25.03  === Backtracking. Learning clause 520:4:0:[5.1,519.0,189.6,8.2,44.2,42.2,6.2,43.2]:: ren2,ren11 -> c1_1(a376),hskp20
% 98.14/25.03  === Backtracking. Learning clause 521:12:0:[189.6,60.2,7.2,58.2,6.2,59.2,520.3,139.2,135.2,126.2,510.2,500.2]:: hskp10,hskp11,hskp14,hskp17,hskp16,hskp3,ndr1_0,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Conflict found: 501:14:0:[439.7,153.2,146.2,145.2]:: ren4,ren3,ren13,ren17,ren18,ren20,ren8,ren10,ren2,ren14,hskp28,hskp21,hskp20 -> hskp22 {}
% 98.14/25.03  === Backtracking. Learning clause 522:14:0:[501.6,144.2]:: ren4,ren3,ren13,ren17,ren18,ren8,ren10,ren2,ren14,hskp28,hskp21,hskp20,hskp19 -> hskp22
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a378, x1 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 524:10:1:[114.1,523.3,268.5,115.2,323.2]:Top: c1_1(x0),c2_1(x0),c0_1(a386),ren29,c0_1(a409),c2_1(a378),ren14,ren4,ren21 -> c0_1(x0)
% 98.14/25.03  === Backtracking. Learning clause 526:9:0:[5.1,525.0,197.5,79.2,56.2,240.1,52.2,78.2,50.2,330.2,358.7,54.2,51.2,355.7,335.7]:: ren20,ren13,ren14,ren23,ren8,ren10,ren2,ren21 -> hskp22
% 98.14/25.03  === Backtracking. Learning clause 528:8:0:[5.1,527.0,197.5,79.2,56.2,240.1,7.2,78.2,236.1,6.2,280.6,54.2]:: ren20,ren8,ren10,ren2,ren14 -> hskp22,c1_1(a376),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407)
% 98.14/25.03  === Conflict found: 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 535:7:0:[40.1,534.6,533.1,38.2,330.2]:: ren20,ren3,c1_1(a384),ren10,ren8,ren14 -> c1_1(a407)
% 98.14/25.03  === Backtracking. Learning clause 537:8:0:[5.1,536.0,197.5,79.2,56.2,240.1,7.2,78.2,330.2,6.2,535.7,54.2,528.8]:: ren3,ren20,ren8,ren10,ren2,ren14 -> hskp22,c1_1(a376)
% 98.14/25.03  === Backtracking. Learning clause 540:8:0:[5.1,538.0,528.6,539.1,197.5,79.2,56.2,240.1,52.2,78.2,50.2,236.1,358.7,54.2,51.2]:: ren20,ren2,ren10,ren8,ren14,ren13 -> hskp22,c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 541:9:0:[197.5,79.2,56.2,240.1,52.2,78.2,50.2,330.2,358.7,54.2,51.2,540.8,537.8,144.2,138.2,137.2,134.2,132.2,127.2,126.2,359.2]:: hskp19,hskp2,ndr1_0,hskp20,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Conflict found: 517:10:0:[5.1,516.0,189.6,60.2,80.2,78.2,58.2,358.7,59.2,499.10]:: ren15,ren13,ren18,ren17,ren14,ren20,ren8,ren10,ren2 -> hskp20 {}
% 98.14/25.03  === Backtracking. Learning clause 542:10:0:[517.6,144.2]:: ren15,ren13,ren18,ren17,ren14,ren8,ren10,ren2,hskp19 -> hskp20
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a378, x1 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 546:9:1:[114.1,543.3,50.1,544.5,51.1,545.11,268.5,115.2,240.1,52.2]:Top: c1_1(x0),c2_1(x0),c0_1(a386),ren29,ren14,ren10,ren13 -> c0_1(x0),c0_1(a387)
% 98.14/25.03  === Backtracking. Learning clause 547:10:0:[189.6,60.2,80.2,78.2,58.2,358.7,59.2,520.3,144.2,139.2,138.2,135.2,134.2,132.2,126.2,541.4]:: hskp14,hskp10,hskp19,hskp2,ndr1_0,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Backtracking. Learning clause 548:10:0:[189.6,60.2,7.2,58.2,6.2,59.2,520.3,139.2,135.2,126.2,510.2,547.3]:: hskp11,hskp14,hskp10,hskp2,ndr1_0,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Conflict found: 542:10:0:[517.6,144.2]:: ren15,ren13,ren18,ren17,ren14,ren8,ren10,ren2,hskp19 -> hskp20 {}
% 98.14/25.03  === Backtracking. Learning clause 549:10:0:[542.3,142.2,141.2]:: ren15,ren13,ren14,ren8,ren10,ren2,hskp19,hskp17,hskp16 -> hskp20
% 98.14/25.03  === Backtracking. Learning clause 552:5:0:[21.1,550.0,22.1,551.1,191.6,68.2,24.2,67.2]:: c2_1(a380),ren6,ren17 -> c1_1(a400),hskp14
% 98.14/25.03  === Backtracking. Learning clause 554:3:0:[65.1,553.0,191.6,68.2,67.2,66.2]:: ren17 -> c1_1(a400),hskp14
% 98.14/25.03  === Backtracking. Learning clause 556:10:0:[5.1,555.0,191.6,84.2,72.2,82.2,71.2,385.7,330.2,83.2,554.2,355.7,147.2]:: ren18,ren14,ren17,ren13,ren8,ren10,ren2,ren21,hskp22 -> hskp14
% 98.14/25.03  === Backtracking. Learning clause 559:11:0:[5.1,557.0,554.1,558.2,191.6,92.2,72.2,90.2,71.2,385.7,236.1]:: ren23,ren18,ren14,ren13,ren17,ren8,ren10,ren2 -> c1_1(a418),hskp14,c1_1(a384)
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a418, x1 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 561:13:0:[54.1,560.1,268.2,90.2,67.2,232.2,91.2,385.7,66.2,55.2,236.1]:: c1_1(a418),ren3,ren23,c1_1(a400),ren18,ren13,ren17,ren14,ren8,ren10,ren2 -> c0_1(a377),c1_1(a384)
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a418, x1 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 562:10:0:[268.2,90.2,67.2,378.2,91.2,385.7,66.2,55.2,236.1,559.9,554.2,54.2]:: ren23,ren18,ren13,ren8,ren10,ren2,ren17,ren14 -> c1_1(a384),hskp14
% 98.14/25.03  === Backtracking. Learning clause 565:10:0:[29.1,563.0,554.1,564.2,191.6,92.2,72.2,90.2,71.2,385.7,330.2]:: ren23,ren18,ren13,ren17,c1_1(a384),ren10,ren8,ren14 -> c1_1(a418),hskp14
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a418, x1 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 567:12:0:[54.1,566.1,268.2,90.2,67.2,232.2,91.2,385.7,66.2,55.2,330.2]:: c1_1(a418),ren3,ren23,c1_1(a400),ren18,ren13,ren17,c1_1(a384),ren10,ren8,ren14 -> c0_1(a377)
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a418, x1 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 568:9:0:[268.2,90.2,67.2,378.2,91.2,385.7,66.2,55.2,330.2,565.9,554.2,54.2,562.9,147.2,142.2,141.2,138.2,137.2,134.2,132.2,126.2]:: hskp22,hskp17,hskp16,hskp13,hskp12,hskp9,hskp7,hskp1 -> hskp14
% 98.14/25.03  === Conflict found: 439:14:0:[5.1,438.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,358.7,381.12,54.2,435.13,417.13]:: ren4,ren21,ren3,ren22,ren13,ren17,ren29,ren18,ren20,ren8,ren10,ren2,ren14 -> hskp22 {}
% 98.14/25.03  === Backtracking. Learning clause 569:14:0:[439.7,153.2,146.2]:: ren4,ren21,ren3,ren13,ren17,ren18,ren20,ren8,ren10,ren2,ren14,hskp28,hskp21 -> hskp22
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a418, x1 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 570:11:0:[268.2,90.2,67.2,378.2,91.2,385.7,66.2,55.2,330.2,565.9,554.2,54.2,540.8]:: ren23,ren18,ren17,ren20,ren2,ren10,ren8,ren14,ren13 -> hskp14,hskp22
% 98.14/25.03  === Backtracking. Learning clause 572:11:0:[500.0,571.11,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,358.7,554.2,54.2,540.8,520.3,144.2,142.2,141.2,138.2,137.2,135.2,134.2,132.2,126.2,568.1,493.6]:: hskp10,hskp19,hskp17,hskp16,hskp3,ndr1_0,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Backtracking. Learning clause 574:8:0:[5.1,573.0,187.1,46.2,82.2,48.2,353.5,330.2,83.2,47.2,509.7]:: ren14,ren12,ren13,ren8,ren10,ren2,ren21 -> hskp19
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a418, x1 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 575:9:0:[268.2,90.2,67.2,378.2,91.2,385.7,66.2,55.2,330.2,565.9,554.2,54.2,562.9]:: ren23,ren18,ren13,ren8,ren10,ren2,ren17,ren14 -> hskp14
% 98.14/25.03  === Backtracking. Learning clause 577:4:0:[5.1,576.0,189.6,60.2,7.2,58.2,6.2,59.2,520.3]:: ren15,ren2,ren11 -> hskp20
% 98.14/25.03  === Backtracking. Learning clause 580:4:0:[45.1,578.0,47.1,579.3,187.1,46.2,123.2,48.2,122.2]:: ren12,ren31 -> c1_1(a397),hskp19
% 98.14/25.03  === Backtracking. Learning clause 582:12:0:[5.1,581.0,197.5,79.2,56.2,378.2,78.2,385.7,55.2,330.2,358.7,554.2,54.2,540.8,520.3]:: ren18,ren17,ren20,ren10,ren8,ren14,ren13,ren2,ren11 -> hskp14,hskp22,hskp20
% 98.14/25.03  === Backtracking. Learning clause 586:5:0:[69.1,583.1,71.1,584.3,107.1,585.6,191.6,108.2,72.2]:: c2_1(a427),c0_1(a401),ren27,ren18 -> hskp14
% 98.14/25.03  === Backtracking. Learning clause 591:4:0:[6.1,587.0,5.1,588.1,103.1,589.6,104.1,590.7,164.6,116.2,102.2,8.2,115.2,7.2]:: c0_1(a386),ren26,ren29,ren2 -> 
% 98.14/25.03  === Conflict found: 378:9:1:[50.1,376.4,51.1,377.10,276.11,52.2]:Top: c1_1(x0),c2_1(x0),c0_1(a401),ren18,ren14,ren10,ren13 -> c0_1(x0),c0_1(a387) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 592:11:0:[378.2,115.2,591.1,385.7,236.1,114.2,554.2]:: ren26,ren18,ren14,ren13,ren8,ren10,ren2,ren29,ren17 -> c1_1(a384),hskp14
% 98.14/25.03  === Conflict found: 378:9:1:[50.1,376.4,51.1,377.10,276.11,52.2]:Top: c1_1(x0),c2_1(x0),c0_1(a401),ren18,ren14,ren10,ren13 -> c0_1(x0),c0_1(a387) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 593:10:0:[378.2,115.2,591.1,385.7,330.2,114.2,554.2,592.10,153.2,150.2,142.2,141.2,138.2,137.2,134.2,132.2,126.2]:: hskp28,hskp25,hskp17,hskp16,hskp13,hskp12,hskp9,hskp7,hskp1 -> hskp14
% 98.14/25.03  === Conflict found: 378:9:1:[50.1,376.4,51.1,377.10,276.11,52.2]:Top: c1_1(x0),c2_1(x0),c0_1(a401),ren18,ren14,ren10,ren13 -> c0_1(x0),c0_1(a387) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 594:10:0:[378.2,115.2,591.1,385.7,330.2,114.2,554.2,592.10]:: ren26,ren18,ren14,ren13,ren8,ren10,ren2,ren29,ren17 -> hskp14
% 98.14/25.03  === Backtracking. Learning clause 597:11:3:[5.1,595.3,7.1,596.9,160.3,189.6,8.2]:TopTopTop: c2_1(x0),c1_1(a376),c0_1(x1),c0_1(x2),c1_1(x2),ren2 -> c0_1(x0),c1_1(x0),c1_1(x1),c2_1(x2),hskp20
% 98.14/25.03  === Conflict found: 597:11:3:[5.1,595.3,7.1,596.9,160.3,189.6,8.2]:TopTopTop: c2_1(x0),c1_1(a376),c0_1(x1),c0_1(x2),c1_1(x2),ren2 -> c0_1(x0),c1_1(x0),c1_1(x1),c2_1(x2),hskp20 {x0 -> a387, x1 -> a386, x2 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 601:7:0:[600.1,50.2,236.1,51.2]:: c1_1(a376),ren8,ren10,ren2,ren13 -> hskp20,c1_1(a384)
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 602:11:0:[600.1,50.2,330.2,51.2,601.7,520.3,138.2,137.2,135.2,134.2,132.2,126.2,510.2,572.2]:: hskp11,hskp10,hskp17,hskp16,hskp3,ndr1_0,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Conflict found: 575:9:0:[268.2,90.2,67.2,378.2,91.2,385.7,66.2,55.2,330.2,565.9,554.2,54.2,562.9]:: ren23,ren18,ren13,ren8,ren10,ren2,ren17,ren14 -> hskp14 {}
% 98.14/25.03  === Backtracking. Learning clause 603:9:0:[575.1,147.2]:: ren18,ren13,ren8,ren10,ren2,ren17,ren14,hskp22 -> hskp14
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 604:9:0:[600.1,50.2,330.2,51.2,355.7,520.3,147.2]:: ren14,ren13,ren8,ren10,ren21,ren2,ren11,hskp22 -> hskp20
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 605:9:0:[600.1,50.2,330.2,51.2,601.7,520.3,138.2,137.2,135.2,134.2,132.2,126.2,541.4]:: hskp10,hskp19,hskp2,ndr1_0,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 606:9:0:[600.1,50.2,330.2,51.2,601.7,520.3,138.2,137.2,135.2,134.2,132.2,126.2,510.2,605.2]:: hskp11,hskp10,hskp2,ndr1_0,hskp13,hskp12,hskp9,hskp7,hskp1 -> 
% 98.14/25.03  === Conflict found: 378:9:1:[50.1,376.4,51.1,377.10,276.11,52.2]:Top: c1_1(x0),c2_1(x0),c0_1(a401),ren18,ren14,ren10,ren13 -> c0_1(x0),c0_1(a387) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 607:11:0:[378.2,115.2,591.1,375.5,330.2,114.2]:: ren13,ren26,ren2,ren18,ren17,c1_1(a384),ren10,ren8,ren14,ren29 -> c1_1(a400)
% 98.14/25.03  === Conflict found: 378:9:1:[50.1,376.4,51.1,377.10,276.11,52.2]:Top: c1_1(x0),c2_1(x0),c0_1(a401),ren18,ren14,ren10,ren13 -> c0_1(x0),c0_1(a387) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 608:11:0:[378.2,115.2,591.1,385.7,330.2,114.2,607.11,355.7,153.2,150.2,147.2,145.2,142.2,141.2]:: ren14,ren13,ren8,ren10,ren2,hskp28,hskp25,hskp22,hskp20,hskp17,hskp16 -> 
% 98.14/25.03  === Conflict found: 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 610:6:0:[40.1,609.4,533.1,38.2,303.1]:: ren20,ren10,ren3,ren22 -> c1_1(a407),c1_1(a411)
% 98.14/25.03  === Conflict found: 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 612:6:0:[40.1,611.4,533.1,38.2,308.1]:: ren20,ren10,ren3,ren23 -> c1_1(a407),c1_1(a418)
% 98.14/25.03  === Conflict found: 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 614:7:0:[40.1,613.5,533.1,38.2,290.2]:: ren20,c1_1(a384),ren3,ren10,ren8 -> c1_1(a407),c0_1(a377)
% 98.14/25.03  === Backtracking. Learning clause 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1)
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a375, x1 -> a378, x2 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 618:9:2:[69.1,616.3,70.1,617.5,615.7,71.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),c0_1(a401),ren18 -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1)
% 98.14/25.03  === Conflict found: 618:9:2:[69.1,616.3,70.1,617.5,615.7,71.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),c0_1(a401),ren18 -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a375, x1 -> a411}
% 98.14/25.03  === Backtracking. Learning clause 620:12:0:[2.1,619.0,618.3,86.2,4.2,88.2,375.5,3.2,610.6]:: c1_1(a384),ren18,ren17,ren8,ren1,ren20,ren10,ren3,ren22 -> hskp13,c1_1(a400),c1_1(a407)
% 98.14/25.03  === Conflict found: 618:9:2:[69.1,616.3,70.1,617.5,615.7,71.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),c0_1(a401),ren18 -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a375, x1 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 622:10:0:[2.1,621.0,618.3,115.2,4.2,591.1,375.5,3.2,114.2]:: ren26,ren2,c1_1(a384),ren18,ren17,ren8,ren1,ren29 -> hskp13,c1_1(a400)
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a378, x2 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 626:8:1:[29.1,623.3,66.1,624.4,31.1,625.9,615.7,67.2,32.2]:Top: c1_1(a384),c1_1(x0),c2_1(x0),c1_1(a400),ren17,ren8 -> hskp13,c0_1(x0)
% 98.14/25.03  === Conflict found: 626:8:1:[29.1,623.3,66.1,624.4,31.1,625.9,615.7,67.2,32.2]:Top: c1_1(a384),c1_1(x0),c2_1(x0),c1_1(a400),ren17,ren8 -> hskp13,c0_1(x0) {x0 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 629:6:0:[70.1,627.1,375.5,628.2,626.3,71.2]:: c1_1(a384),ren17,ren8,ren18 -> hskp13,c0_1(a401)
% 98.14/25.03  === Conflict found: 626:8:1:[29.1,623.3,66.1,624.4,31.1,625.9,615.7,67.2,32.2]:Top: c1_1(a384),c1_1(x0),c2_1(x0),c1_1(a400),ren17,ren8 -> hskp13,c0_1(x0) {x0 -> a411}
% 98.14/25.03  === Backtracking. Learning clause 630:10:0:[626.3,86.2,88.2,610.6]:: c1_1(a384),c1_1(a400),ren17,ren8,ren20,ren10,ren3,ren22 -> hskp13,c1_1(a407)
% 98.14/25.03  === Conflict found: 626:8:1:[29.1,623.3,66.1,624.4,31.1,625.9,615.7,67.2,32.2]:Top: c1_1(a384),c1_1(x0),c2_1(x0),c1_1(a400),ren17,ren8 -> hskp13,c0_1(x0) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 631:12:0:[626.3,115.2,591.1,114.2,622.10,355.7,153.2,150.2,147.2,145.2,142.2,141.2,137.2,134.2,132.2,126.2,125.2]:: hskp28,hskp25,hskp22,hskp20,hskp17,hskp16,hskp12,hskp9,hskp7,hskp1,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a396, x1 -> a386, x2 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 633:12:0:[5.1,632.0,615.3,115.2,71.2,626.3,591.1,629.6,55.2,114.2,70.2,607.11,54.2,355.7]:: ren26,ren18,ren17,ren29,ren14,ren23,ren13,ren8,ren10,ren2,ren21 -> hskp13
% 98.14/25.03  === Backtracking. Learning clause 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 638:10:0:[637.3,71.2,629.6,70.2,355.7,147.2,145.2,142.2,141.2,137.2,134.2,132.2,128.2,126.2]:: hskp22,hskp20,hskp17,hskp16,hskp12,hskp9,hskp7,hskp3,hskp1 -> hskp13
% 98.14/25.03  === Conflict found: 522:14:0:[501.6,144.2]:: ren4,ren3,ren13,ren17,ren18,ren8,ren10,ren2,ren14,hskp28,hskp21,hskp20,hskp19 -> hskp22 {}
% 98.14/25.03  === Backtracking. Learning clause 639:14:0:[522.5,142.2,141.2]:: ren4,ren3,ren13,ren8,ren10,ren2,ren14,hskp28,hskp21,hskp20,hskp19,hskp17,hskp16 -> hskp22
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 640:13:0:[637.3,67.2,66.2,622.10,355.7,153.2,150.2]:: ren4,ren18,ren17,ren1,ren23,ren13,ren8,ren10,ren2,ren21,hskp28,hskp25 -> hskp13
% 98.14/25.03  === Conflict found: 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 642:7:0:[40.1,641.5,533.1,38.2,236.1]:: ren20,ren3,ren8,ren10,ren2 -> c1_1(a407),c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 645:6:0:[2.1,643.0,1.1,644.1,169.10,68.2,115.2,67.2,4.2,591.1,3.2,114.2]:: ren17,ren26,ren2,ren1,ren29 -> c1_1(a400)
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 646:7:0:[637.3,67.2,66.2,645.6,153.2,150.2,141.2,128.2,126.2,125.2]:: hskp28,hskp25,hskp16,hskp3,hskp1,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 647:11:0:[637.3,67.2,66.2,381.12,540.8,475.10,144.2,142.2,141.2]:: ren4,ren13,ren8,ren10,ren2,ren14,hskp19,hskp17,hskp16 -> hskp13,hskp22
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 648:7:0:[637.3,67.2,66.2,645.6]:: ren4,ren17,ren26,ren2,ren1,ren29 -> hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 649:10:0:[637.3,71.2,629.6,70.2,355.7]:: ren4,ren17,ren18,ren23,ren13,ren8,ren10,ren2,ren21 -> hskp13
% 98.14/25.03  === Backtracking. Learning clause 652:7:1:[74.1,650.0,65.1,651.3,169.10,68.2,76.2,67.2]:Top: c1_1(x0),c2_1(x0),ren19,ren17 -> c0_1(a404),c0_1(x0),c1_1(a400)
% 98.14/25.03  === Conflict found: 652:7:1:[74.1,650.0,65.1,651.3,169.10,68.2,76.2,67.2]:Top: c1_1(x0),c2_1(x0),ren19,ren17 -> c0_1(a404),c0_1(x0),c1_1(a400) {x0 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 654:6:0:[70.1,653.0,652.2,71.2]:: ren19,ren17,ren18 -> c0_1(a404),c0_1(a401),c1_1(a400)
% 98.14/25.03  === Backtracking. Learning clause 656:8:2:[65.1,655.3,169.10,68.2,67.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),ren17 -> c0_1(x0),c2_1(x0),c0_1(x1),c1_1(a400)
% 98.14/25.03  === Conflict found: 656:8:2:[65.1,655.3,169.10,68.2,67.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),ren17 -> c0_1(x0),c2_1(x0),c0_1(x1),c1_1(a400) {x0 -> a375, x1 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 660:5:0:[2.1,657.0,70.1,658.1,3.1,659.5,656.3,71.2,4.2]:: ren17,ren18,ren1 -> c0_1(a401),c1_1(a400)
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a401}
% 98.14/25.03  === Backtracking. Learning clause 661:6:0:[637.3,71.2,660.4,70.2]:: ren4,ren17,ren1,ren18 -> hskp13,c1_1(a400)
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 662:5:0:[637.3,67.2,66.2,661.6,142.2,141.2,128.2,125.2]:: hskp17,hskp16,hskp3,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 649:10:0:[637.3,71.2,629.6,70.2,355.7]:: ren4,ren17,ren18,ren23,ren13,ren8,ren10,ren2,ren21 -> hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 663:10:0:[649.4,147.2,145.2]:: ren4,ren17,ren18,ren13,ren8,ren10,ren2,hskp22,hskp20 -> hskp13
% 98.14/25.03  === Backtracking. Learning clause 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 668:7:0:[667.9,52.2,38.2,50.2,330.2,51.2,40.2,355.7,147.2,145.2]:: ren14,ren13,ren8,ren10,ren2,hskp22,hskp20 -> 
% 98.14/25.03  === Conflict found: 652:7:1:[74.1,650.0,65.1,651.3,169.10,68.2,76.2,67.2]:Top: c1_1(x0),c2_1(x0),ren19,ren17 -> c0_1(a404),c0_1(x0),c1_1(a400) {x0 -> a411}
% 98.14/25.03  === Backtracking. Learning clause 669:6:0:[652.2,86.2,88.2]:: c1_1(a411),ren19,ren17,ren22 -> c0_1(a404),c1_1(a400)
% 98.14/25.03  === Conflict found: 656:8:2:[65.1,655.3,169.10,68.2,67.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),ren17 -> c0_1(x0),c2_1(x0),c0_1(x1),c1_1(a400) {x0 -> a375, x1 -> a411}
% 98.14/25.03  === Backtracking. Learning clause 671:8:0:[2.1,670.0,656.3,86.2,4.2,88.2,3.2,610.6]:: ren17,ren1,ren20,ren10,ren3,ren22 -> c1_1(a400),c1_1(a407)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 673:7:0:[40.1,672.5,667.1,38.2,7.2,303.1,6.2]:: ren23,ren10,ren3,ren22,ren2 -> c1_1(a376),c1_1(a411)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 675:6:0:[40.1,674.4,667.1,38.2,7.2,308.1,6.2]:: ren10,ren3,ren23,ren2 -> c1_1(a376),c1_1(a418)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 678:8:0:[6.1,676.0,40.1,677.7,667.1,38.2,7.2,290.2]:: ren23,ren2,c1_1(a384),ren3,ren10,ren8 -> c1_1(a376),c0_1(a377)
% 98.14/25.03  === Conflict found: 656:8:2:[65.1,655.3,169.10,68.2,67.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),ren17 -> c0_1(x0),c2_1(x0),c0_1(x1),c1_1(a400) {x0 -> a375, x1 -> a411}
% 98.14/25.03  === Backtracking. Learning clause 680:9:0:[2.1,679.0,656.3,86.2,4.2,88.2,3.2,673.7]:: ren17,ren1,ren23,ren10,ren3,ren22,ren2 -> c1_1(a400),c1_1(a376)
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 681:10:0:[637.3,67.2,66.2,680.8]:: ren4,ren17,ren1,ren23,ren10,ren3,ren22,ren2 -> hskp13,c1_1(a376)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 684:6:0:[40.1,682.5,51.1,683.6,667.9,52.2,38.2,50.2,303.1]:: ren23,ren13,ren10,ren3,ren22 -> c1_1(a411)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 687:5:0:[40.1,685.4,51.1,686.5,667.9,52.2,38.2,50.2,308.1]:: ren13,ren10,ren3,ren23 -> c1_1(a418)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 690:7:0:[40.1,688.6,51.1,689.7,667.9,52.2,38.2,50.2,290.2]:: ren23,ren13,c1_1(a384),ren3,ren10,ren8 -> c0_1(a377)
% 98.14/25.03  === Conflict found: 656:8:2:[65.1,655.3,169.10,68.2,67.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),ren17 -> c0_1(x0),c2_1(x0),c0_1(x1),c1_1(a400) {x0 -> a375, x1 -> a411}
% 98.14/25.03  === Backtracking. Learning clause 692:8:0:[2.1,691.0,656.3,86.2,4.2,88.2,3.2,684.6]:: ren17,ren1,ren23,ren13,ren10,ren3,ren22 -> c1_1(a400)
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 693:9:0:[637.3,67.2,66.2,692.8,147.2,146.2,141.2,137.2,134.2,128.2,127.2,125.2]:: hskp22,hskp21,hskp16,hskp12,hskp9,hskp3,hskp2,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 694:5:0:[637.3,67.2,66.2,661.6]:: ren4,ren17,ren1,ren18 -> hskp13
% 98.14/25.03  === Backtracking. Learning clause 698:8:0:[53.1,695.0,54.1,696.3,55.1,697.9,197.5,79.2,56.2,652.2,78.2]:: c1_1(a407),ren14,ren19,ren17,ren20 -> hskp22,c0_1(a404),c1_1(a400)
% 98.14/25.03  === Backtracking. Learning clause 700:10:0:[5.1,699.0,197.5,75.2,8.2,7.2,698.7,358.7,74.2]:: ren17,c1_1(a376),ren20,ren2,ren10,ren8,ren14,ren19 -> hskp22,c1_1(a400)
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 701:11:0:[637.3,67.2,66.2,700.10,537.8,144.2,143.2,141.2]:: ren4,ren3,ren8,ren10,ren2,ren14,hskp19,hskp18,hskp16 -> hskp13,hskp22
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 702:9:0:[637.3,67.2,66.2,692.8]:: ren4,ren17,ren1,ren23,ren13,ren10,ren3,ren22 -> hskp13
% 98.14/25.03  === Backtracking. Learning clause 705:10:0:[5.1,703.0,23.1,704.1,197.5,79.2,24.2,637.3,78.2,22.2,642.6]:: ren4,ren6,ren20,ren3,ren8,ren10,ren2 -> hskp22,hskp13,c1_1(a384)
% 98.14/25.03  === Backtracking. Learning clause 708:11:0:[1.1,706.0,23.1,707.1,197.5,79.2,24.2,637.3,78.2,22.2,671.8]:: ren4,ren6,ren17,ren1,ren20,ren10,ren3,ren22 -> hskp22,hskp13,c1_1(a400)
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 709:10:0:[637.3,67.2,66.2,708.11,146.2,144.2,141.2,134.2,130.2,128.2,127.2,125.2,693.1]:: hskp19,hskp5,hskp21,hskp16,hskp12,hskp9,hskp3,hskp2,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 702:9:0:[637.3,67.2,66.2,692.8]:: ren4,ren17,ren1,ren23,ren13,ren10,ren3,ren22 -> hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 710:9:0:[702.4,147.2]:: ren4,ren17,ren1,ren13,ren10,ren3,ren22,hskp22 -> hskp13
% 98.14/25.03  === Conflict found: 652:7:1:[74.1,650.0,65.1,651.3,169.10,68.2,76.2,67.2]:Top: c1_1(x0),c2_1(x0),ren19,ren17 -> c0_1(a404),c0_1(x0),c1_1(a400) {x0 -> a418}
% 98.14/25.03  === Backtracking. Learning clause 711:6:0:[652.2,90.2,91.2]:: c1_1(a418),ren19,ren17,ren23 -> c0_1(a404),c1_1(a400)
% 98.14/25.03  === Conflict found: 656:8:2:[65.1,655.3,169.10,68.2,67.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),ren17 -> c0_1(x0),c2_1(x0),c0_1(x1),c1_1(a400) {x0 -> a375, x1 -> a418}
% 98.14/25.03  === Backtracking. Learning clause 713:7:0:[2.1,712.0,656.3,90.2,4.2,91.2,3.2,687.5]:: ren17,ren1,ren13,ren10,ren3,ren23 -> c1_1(a400)
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 714:8:0:[637.3,67.2,66.2,713.7,147.2,141.2,137.2,134.2,128.2,127.2,125.2]:: hskp22,hskp16,hskp12,hskp9,hskp3,hskp2,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 715:10:0:[637.3,67.2,66.2,708.11]:: ren4,ren6,ren17,ren1,ren20,ren10,ren3,ren22 -> hskp22,hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 716:8:0:[637.3,67.2,66.2,713.7]:: ren4,ren17,ren1,ren13,ren10,ren3,ren23 -> hskp13
% 98.14/25.03  === Backtracking. Learning clause 720:7:2:[101.1,717.1,103.1,718.6,104.1,719.7,164.1,102.2]:TopTop: c0_1(x0),c0_1(x1),c2_1(x1),c3_1(x1),ren26 -> c2_1(x0),c3_1(x0)
% 98.14/25.03  === Conflict found: 720:7:2:[101.1,717.1,103.1,718.6,104.1,719.7,164.1,102.2]:TopTop: c0_1(x0),c0_1(x1),c2_1(x1),c3_1(x1),ren26 -> c2_1(x0),c3_1(x0) {x0 -> a376, x1 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 722:4:0:[6.1,721.0,720.4,39.2,8.2,38.2,7.2]:: c0_1(a387),ren26,ren10,ren2 -> 
% 98.14/25.03  === Conflict found: 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 724:6:0:[40.1,723.5,533.1,38.2,722.1]:: ren20,ren3,ren26,ren10,ren2 -> c1_1(a407)
% 98.14/25.03  === Backtracking. Learning clause 725:10:0:[197.5,79.2,24.2,637.3,78.2,22.2,724.6,23.2,150.2,144.2,134.2,130.2,128.2,127.2,126.2]:: ndr1_0,hskp25,hskp19,hskp9,hskp5,hskp3,hskp2,hskp1 -> hskp22,hskp13
% 98.14/25.03  === Conflict found: 648:7:0:[637.3,67.2,66.2,645.6]:: ren4,ren17,ren26,ren2,ren1,ren29 -> hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 726:7:0:[648.6,153.2]:: ren4,ren17,ren26,ren2,ren1,hskp28 -> hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 728:4:0:[114.1,727.1,637.3,115.2]:: c0_1(a386),ren4,ren29 -> hskp13
% 98.14/25.03  === Conflict found: 652:7:1:[74.1,650.0,65.1,651.3,169.10,68.2,76.2,67.2]:Top: c1_1(x0),c2_1(x0),ren19,ren17 -> c0_1(a404),c0_1(x0),c1_1(a400) {x0 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 730:7:0:[114.1,729.0,652.2,115.2,728.1]:: ren19,ren17,ren4,ren29 -> c0_1(a404),c1_1(a400),hskp13
% 98.14/25.03  === Conflict found: 656:8:2:[65.1,655.3,169.10,68.2,67.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),ren17 -> c0_1(x0),c2_1(x0),c0_1(x1),c1_1(a400) {x0 -> a384, x1 -> a386}
% 98.14/25.03  === Backtracking. Learning clause 731:7:0:[656.3,115.2,32.2,728.1,31.2,114.2]:: c1_1(a384),ren17,ren4,ren8,ren29 -> c1_1(a400),hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 732:11:0:[637.3,67.2,66.2,731.6,705.10,153.2,144.2,141.2,134.2,132.2,130.2,128.2,127.2,126.2]:: hskp28,hskp19,hskp16,hskp9,hskp7,hskp5,hskp3,hskp2,hskp1 -> hskp22,hskp13
% 98.14/25.03  === Backtracking. Learning clause 734:9:0:[5.1,733.0,197.5,79.2,24.2,637.3,78.2,22.2,724.6,23.2]:: ren4,ren20,ren3,ren26,ren10,ren2,ren6 -> hskp22,hskp13
% 98.14/25.03  === Conflict found: 637:5:1:[14.1,634.0,13.1,635.1,16.1,636.6,179.2,15.2]:Top: c0_1(x0),c1_1(x0),c2_1(x0),ren4 -> hskp13 {x0 -> a400}
% 98.14/25.03  === Backtracking. Learning clause 735:11:0:[637.3,67.2,66.2,731.6,705.10]:: ren17,ren29,ren4,ren6,ren20,ren3,ren8,ren10,ren2 -> hskp22,hskp13
% 98.14/25.03  === Backtracking. Learning clause 736:4:0:[197.5,120.2,12.2,11.2,118.2,119.2,10.2,154.2,127.2]:: ndr1_0,hskp29,hskp2 -> hskp22
% 98.14/25.03  === Backtracking. Learning clause 738:3:0:[9.1,737.0,197.5,120.2,12.2,11.2,118.2,119.2,10.2]:: ren30,ren3 -> hskp22
% 98.14/25.03  === Clause set with instances from active satisfied. Growing active. New size: 180
% 98.14/25.03  === Restarting.
% 98.14/25.03  === Conflict found: 652:7:1:[74.1,650.0,65.1,651.3,169.10,68.2,76.2,67.2]:Top: c1_1(x0),c2_1(x0),ren19,ren17 -> c0_1(a404),c0_1(x0),c1_1(a400) {x0 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 741:5:0:[26.1,739.0,28.1,740.5,652.2,27.2]:: ren19,ren17,ren7 -> c0_1(a404),c1_1(a400)
% 98.14/25.03  === Conflict found: 656:8:2:[65.1,655.3,169.10,68.2,67.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),ren17 -> c0_1(x0),c2_1(x0),c0_1(x1),c1_1(a400) {x0 -> a375, x1 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 744:4:0:[2.1,742.0,26.1,743.1,656.3,27.2,4.2,28.2,3.2]:: ren17,ren7,ren1 -> c1_1(a400)
% 98.14/25.03  === Conflict found: 626:8:1:[29.1,623.3,66.1,624.4,31.1,625.9,615.7,67.2,32.2]:Top: c1_1(a384),c1_1(x0),c2_1(x0),c1_1(a400),ren17,ren8 -> hskp13,c0_1(x0) {x0 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 745:12:0:[626.3,27.2,28.2,744.4,705.10,26.2,144.2,141.2,134.2,132.2,131.2,130.2,128.2,127.2,126.2,125.2,714.1]:: hskp19,hskp7,hskp6,hskp5,hskp1,hskp16,hskp12,hskp9,hskp3,hskp2,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 574:8:0:[5.1,573.0,187.1,46.2,82.2,48.2,353.5,330.2,83.2,47.2,509.7]:: ren14,ren12,ren13,ren8,ren10,ren2,ren21 -> hskp19 {}
% 98.14/25.03  === Backtracking. Learning clause 746:8:0:[574.7,145.2]:: ren14,ren12,ren13,ren8,ren10,ren2,hskp20 -> hskp19
% 98.14/25.03  === Conflict found: 715:10:0:[637.3,67.2,66.2,708.11]:: ren4,ren6,ren17,ren1,ren20,ren10,ren3,ren22 -> hskp22,hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 747:10:0:[715.8,146.2]:: ren4,ren6,ren17,ren1,ren20,ren10,ren3,hskp21 -> hskp22,hskp13
% 98.14/25.03  === Conflict found: 626:8:1:[29.1,623.3,66.1,624.4,31.1,625.9,615.7,67.2,32.2]:Top: c1_1(a384),c1_1(x0),c2_1(x0),c1_1(a400),ren17,ren8 -> hskp13,c0_1(x0) {x0 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 748:10:0:[626.3,27.2,28.2,744.4,509.7,26.2,145.2,141.2,137.2,134.2,132.2,131.2,126.2,125.2]:: hskp20,hskp16,hskp12,hskp9,hskp7,hskp6,hskp1,hskp0 -> hskp13,hskp19
% 98.14/25.03  === Conflict found: 577:4:0:[5.1,576.0,189.6,60.2,7.2,58.2,6.2,59.2,520.3]:: ren15,ren2,ren11 -> hskp20 {}
% 98.14/25.03  === Backtracking. Learning clause 749:13:0:[577.1,139.2,135.2,126.2,748.1,745.1]:: hskp14,hskp10,hskp7,hskp6,hskp5,hskp1,hskp16,hskp12,hskp9,hskp3,hskp2,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 694:5:0:[637.3,67.2,66.2,661.6]:: ren4,ren17,ren1,ren18 -> hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 750:5:0:[694.4,142.2]:: ren4,ren17,ren1,hskp17 -> hskp13
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 751:5:0:[667.1,38.2,7.2,722.1,6.2,40.2]:: ren23,ren26,ren2,ren10 -> c1_1(a376)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 752:5:0:[667.9,52.2,38.2,50.2,722.1,51.2,40.2,150.2,147.2,137.2,134.2,126.2]:: hskp25,hskp22,hskp12,hskp9,hskp1 -> 
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 753:5:0:[667.9,52.2,38.2,50.2,722.1,51.2,40.2]:: ren23,ren26,ren2,ren13,ren10 -> 
% 98.14/25.03  === Conflict found: 300:6:1:[9.1,296.2,10.1,297.3,40.1,298.8,11.1,299.9,160.3,39.2,12.2]:Top: c2_1(x0),c0_1(a387),ren10,ren3 -> c0_1(x0),c1_1(x0) {x0 -> a424}
% 98.14/25.03  === Backtracking. Learning clause 755:4:0:[100.1,754.4,300.1,98.2,99.2]:: c0_1(a387),ren10,ren3,ren25 -> 
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 756:6:0:[667.1,38.2,7.2,755.1,6.2,40.2]:: ren23,ren3,ren25,ren2,ren10 -> c1_1(a376)
% 98.14/25.03  === Conflict found: 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 758:5:0:[40.1,757.4,533.1,38.2,755.1]:: ren20,ren10,ren3,ren25 -> c1_1(a407)
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 759:5:0:[667.9,52.2,38.2,50.2,755.1,51.2,40.2,149.2,147.2,137.2,134.2,127.2]:: hskp24,hskp22,hskp12,hskp9,hskp2 -> 
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 760:5:0:[667.9,52.2,38.2,50.2,755.1,51.2,40.2]:: ren23,ren3,ren25,ren13,ren10 -> 
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a418, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 762:9:0:[359.3,761.9,615.7,112.2,90.2,32.2,110.2,91.2,31.2,111.2,687.5,355.7,152.2,147.2,145.2,137.2,134.2,132.2,127.2,126.2]:: ndr1_0,hskp27,hskp22,hskp20,hskp12,hskp9,hskp7,hskp2,hskp1 -> 
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a418, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 764:9:0:[5.1,763.0,615.7,112.2,90.2,32.2,110.2,91.2,31.2,111.2,687.5,355.7]:: ren28,ren3,ren23,ren13,ren8,ren10,ren2,ren21 -> hskp13
% 98.14/25.03  === Backtracking. Learning clause 769:6:1:[70.1,765.2,71.1,766.3,13.1,767.4,14.1,768.5,194.10,72.2,15.2]:Top: c0_1(x0),c2_1(x0),c2_1(a378),ren18,ren4 -> c1_1(x0)
% 98.14/25.03  === Conflict found: 769:6:1:[70.1,765.2,71.1,766.3,13.1,767.4,14.1,768.5,194.10,72.2,15.2]:Top: c0_1(x0),c2_1(x0),c2_1(a378),ren18,ren4 -> c1_1(x0) {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 772:4:0:[34.1,770.0,36.1,771.5,769.2,35.2]:: c2_1(a378),ren18,ren4,ren9 -> 
% 98.14/25.03  === Backtracking. Learning clause 778:4:0:[58.1,773.0,33.1,774.1,34.1,775.2,59.1,776.7,36.1,777.8,175.7,72.2,60.2,71.2,35.2]:: ren15,ren18,ren9 -> c0_1(a401)
% 98.14/25.03  === Conflict found: 618:9:2:[69.1,616.3,70.1,617.5,615.7,71.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),c0_1(a401),ren18 -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a375, x1 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 779:6:0:[618.3,27.2,4.2,778.4,28.2,3.2,26.2,2.2,142.2,139.2,133.2,131.2,125.2]:: hskp17,hskp14,hskp8,hskp6,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 710:9:0:[702.4,147.2]:: ren4,ren17,ren1,ren13,ren10,ren3,ren22,hskp22 -> hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 780:9:0:[710.7,146.2]:: ren4,ren17,ren1,ren13,ren10,ren3,hskp22,hskp21 -> hskp13
% 98.14/25.03  === Conflict found: 618:9:2:[69.1,616.3,70.1,617.5,615.7,71.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),c0_1(a401),ren18 -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a375, x1 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 781:6:0:[618.3,27.2,4.2,778.4,28.2,3.2,26.2,2.2]:: ren15,ren18,ren9,ren7,ren1 -> hskp13
% 98.14/25.03  === Backtracking. Learning clause 783:6:0:[9.1,782.0,201.4,84.2,82.2,302.5]:: c0_1(a387),ren10,ren3,ren21 -> hskp24,hskp25
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a376}
% 98.14/25.03  === Backtracking. Learning clause 784:8:0:[667.1,38.2,7.2,783.1,6.2,40.2]:: ren23,ren3,ren21,ren2,ren10 -> c1_1(a376),hskp24,hskp25
% 98.14/25.03  === Conflict found: 533:6:1:[78.1,529.1,9.1,530.2,10.1,531.3,11.1,532.9,160.3,79.2,12.2]:Top: c2_1(x0),ren20,ren3 -> c0_1(x0),c1_1(x0),c1_1(a407) {x0 -> a387}
% 98.14/25.03  === Backtracking. Learning clause 786:7:0:[40.1,785.4,533.1,38.2,783.1]:: ren20,ren10,ren3,ren21 -> c1_1(a407),hskp24,hskp25
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 787:6:0:[667.9,52.2,38.2,50.2,783.1,51.2,40.2,147.2,145.2,137.2,134.2,127.2,752.1,759.1]:: hskp20,hskp1,hskp22,hskp12,hskp9,hskp2 -> 
% 98.14/25.03  === Conflict found: 747:10:0:[715.8,146.2]:: ren4,ren6,ren17,ren1,ren20,ren10,ren3,hskp21 -> hskp22,hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 788:10:0:[747.5,144.2]:: ren4,ren6,ren17,ren1,ren10,ren3,hskp21,hskp19 -> hskp22,hskp13
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a381, x1 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 793:7:0:[26.1,789.0,110.1,790.1,111.1,791.2,28.1,792.10,268.5,112.2,323.2,27.2]:: ren28,c0_1(a409),c2_1(a378),ren14,ren4,ren21,ren7 -> 
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a381, x1 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 794:7:0:[268.5,112.2,240.1,52.2,27.2,110.2,50.2,755.1,28.2,111.2,51.2,26.2,152.2,149.2]:: ren14,ren10,ren3,ren13,ren7,hskp27,hskp24 -> 
% 98.14/25.03  === Conflict found: 760:5:0:[667.9,52.2,38.2,50.2,755.1,51.2,40.2]:: ren23,ren3,ren25,ren13,ren10 ->  {}
% 98.14/25.03  === Backtracking. Learning clause 795:5:0:[760.3,149.2]:: ren23,ren3,ren13,ren10,hskp24 -> 
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a377, x1 -> a381, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 800:5:0:[10.1,796.0,26.1,797.1,9.1,798.2,111.1,799.3,615.7,112.2,27.2,11.2,110.2,28.2]:: ren3,ren28,ren7 -> hskp13,c0_1(a377)
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a404, x1 -> a381, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 806:5:0:[74.1,801.0,26.1,802.1,25.1,803.2,111.1,804.3,28.1,805.9,615.7,112.2,76.2,27.2,110.2]:: ren19,ren7,ren28 -> hskp13,c0_1(a404)
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a381, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 807:12:0:[615.7,112.2,32.2,27.2,110.2,31.2,28.2,111.2,705.10,26.2,152.2,144.2,134.2,132.2,131.2,130.2,128.2,127.2,126.2]:: ndr1_0,hskp27,hskp19,hskp9,hskp7,hskp6,hskp5,hskp3,hskp2,hskp1 -> hskp22,hskp13
% 98.14/25.03  === Conflict found: 268:8:2:[53.1,266.2,55.1,267.7,166.9,56.2]:TopTop: c1_1(x0),c2_1(x0),c0_1(x1),c1_1(x1),c2_1(x1),ren14 -> c2_1(a396),c0_1(x0) {x0 -> a381, x1 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 808:7:0:[268.5,112.2,240.1,52.2,27.2,110.2,50.2,755.1,28.2,111.2,51.2,26.2]:: ren14,ren10,ren3,ren25,ren28,ren13,ren7 -> 
% 98.14/25.03  === Backtracking. Learning clause 811:5:0:[10.1,809.0,9.1,810.1,173.6,12.2,80.2,78.2]:: c1_1(a407),ren3,ren20 -> c0_1(a377),hskp29
% 98.14/25.03  === Backtracking. Learning clause 813:6:0:[9.1,812.0,173.6,56.2,11.2,55.2,811.4,758.5,54.2,10.2,149.2,144.2]:: ren10,ren14,ren3,hskp24,hskp19 -> hskp29
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a381, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 815:11:0:[5.1,814.0,615.7,112.2,32.2,27.2,110.2,31.2,28.2,111.2,705.10,26.2]:: ren28,ren4,ren6,ren20,ren3,ren8,ren10,ren2,ren7 -> hskp22,hskp13
% 98.14/25.03  === Backtracking. Learning clause 816:9:0:[197.5,79.2,24.2,637.3,78.2,22.2,758.5,23.2,149.2,144.2,134.2,130.2,128.2,127.2]:: ndr1_0,hskp24,hskp19,hskp9,hskp5,hskp3,hskp2 -> hskp22,hskp13
% 98.14/25.03  === Backtracking. Learning clause 819:7:0:[9.1,817.0,813.3,818.7,173.6,56.2,11.2,55.2,811.4,786.5,54.2,10.2,145.2,144.2]:: ren10,ren14,ren3,hskp20,hskp19 -> hskp29,hskp25
% 98.14/25.03  === Conflict found: 667:9:2:[37.1,664.1,91.1,665.6,40.1,666.8,161.8,92.2,161.8,39.2,90.2]:TopTop: c2_1(x0),c0_1(x1),ren10,ren23 -> c1_1(x0),c0_1(a387),c0_1(x0),c1_1(x1),c2_1(x1) {x0 -> a387, x1 -> a395}
% 98.14/25.03  === Backtracking. Learning clause 821:6:0:[795.4,820.5,667.9,52.2,38.2,50.2,783.1,51.2,40.2]:: ren23,ren3,ren21,ren13,ren10 -> hskp25
% 98.14/25.03  === Backtracking. Learning clause 822:10:0:[197.5,79.2,24.2,637.3,78.2,22.2,786.5,23.2,145.2,144.2,134.2,130.2,128.2,127.2,725.2,816.2,787.3]:: ndr1_0,hskp19,hskp5,hskp3,hskp20,hskp1,hskp12,hskp9,hskp2 -> hskp13
% 98.14/25.03  === Conflict found: 577:4:0:[5.1,576.0,189.6,60.2,7.2,58.2,6.2,59.2,520.3]:: ren15,ren2,ren11 -> hskp20 {}
% 98.14/25.03  === Backtracking. Learning clause 823:11:0:[577.1,139.2,135.2,126.2,822.5]:: hskp14,hskp10,ndr1_0,hskp19,hskp5,hskp3,hskp1,hskp12,hskp9,hskp2 -> hskp13
% 98.14/25.03  === Conflict found: 726:7:0:[648.6,153.2]:: ren4,ren17,ren26,ren2,ren1,hskp28 -> hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 824:7:0:[726.3,150.2]:: ren4,ren17,ren2,ren1,hskp28,hskp25 -> hskp13
% 98.14/25.03  === Conflict found: 734:9:0:[5.1,733.0,197.5,79.2,24.2,637.3,78.2,22.2,724.6,23.2]:: ren4,ren20,ren3,ren26,ren10,ren2,ren6 -> hskp22,hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 825:9:0:[734.4,150.2]:: ren4,ren20,ren3,ren10,ren2,ren6,hskp25 -> hskp22,hskp13
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a381, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 826:10:0:[615.7,112.2,32.2,27.2,110.2,31.2,28.2,111.2,509.7,26.2,152.2,145.2,137.2,134.2,132.2,131.2,126.2]:: ndr1_0,hskp27,hskp20,hskp12,hskp9,hskp7,hskp6,hskp1 -> hskp13,hskp19
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a381, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 828:9:0:[5.1,827.0,615.7,112.2,32.2,27.2,110.2,31.2,28.2,111.2,509.7,26.2]:: ren28,ren13,ren8,ren10,ren2,ren21,ren7 -> hskp13,hskp19
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a404, x1 -> a386, x2 -> a397}
% 98.14/25.03  === Backtracking. Learning clause 832:8:0:[74.1,829.0,114.1,830.1,5.1,831.2,615.7,123.2,115.2,76.2,122.2,591.1]:: c1_1(a397),ren19,ren31,ren26,ren29,ren2 -> hskp13,c0_1(a404)
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a386, x2 -> a397}
% 98.14/25.03  === Backtracking. Learning clause 834:11:0:[510.2,833.10,615.7,123.2,115.2,32.2,122.2,591.1,31.2,580.3,114.2,509.7,155.2,153.2,150.2,145.2,137.2,136.2,134.2,132.2,126.2]:: ndr1_0,hskp30,hskp28,hskp25,hskp20,hskp12,hskp11,hskp9,hskp7,hskp1 -> hskp19
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a386, x2 -> a397}
% 98.14/25.03  === Backtracking. Learning clause 836:11:0:[5.1,835.0,615.7,123.2,115.2,32.2,122.2,591.1,31.2,580.3,114.2,509.7]:: ren26,ren12,ren31,ren29,ren13,ren8,ren10,ren2,ren21 -> hskp13,hskp19
% 98.14/25.03  === Backtracking. Learning clause 839:7:1:[10.1,837.0,9.1,838.1,173.6,12.2,637.3]:Top: ren3,c0_1(x0),c1_1(x0),ren4 -> c0_1(a377),hskp29,hskp13
% 98.14/25.03  === Conflict found: 839:7:1:[10.1,837.0,9.1,838.1,173.6,12.2,637.3]:Top: ren3,c0_1(x0),c1_1(x0),ren4 -> c0_1(a377),hskp29,hskp13 {x0 -> a380}
% 98.14/25.03  === Backtracking. Learning clause 841:6:0:[23.1,840.1,839.2,22.2]:: ren3,ren4,ren6 -> c0_1(a377),hskp29,hskp13
% 98.14/25.03  === Backtracking. Learning clause 845:5:1:[45.1,842.0,47.1,843.4,48.1,844.5,187.1,46.2]:Top: c0_1(x0),c2_1(x0),ren12 -> c1_1(x0),hskp19
% 98.14/25.03  === Conflict found: 845:5:1:[45.1,842.0,47.1,843.4,48.1,844.5,187.1,46.2]:Top: c0_1(x0),c2_1(x0),ren12 -> c1_1(x0),hskp19 {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 846:12:0:[845.2,35.2,34.2,36.2,136.2,133.2,823.4]:: hskp11,hskp8,hskp14,hskp10,ndr1_0,hskp5,hskp3,hskp1,hskp12,hskp9,hskp2 -> hskp13
% 98.14/25.03  === Conflict found: 828:9:0:[5.1,827.0,615.7,112.2,32.2,27.2,110.2,31.2,28.2,111.2,509.7,26.2]:: ren28,ren13,ren8,ren10,ren2,ren21,ren7 -> hskp13,hskp19 {}
% 98.14/25.03  === Backtracking. Learning clause 847:9:0:[828.1,152.2]:: ren13,ren8,ren10,ren2,ren21,ren7,hskp27 -> hskp13,hskp19
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 848:7:0:[600.5,755.1,34.2,36.2,520.3,149.2,135.2,134.2,133.2,127.2,126.2]:: hskp24,hskp10,hskp9,hskp8,hskp2,hskp1 -> hskp20
% 98.14/25.03  === Conflict found: 808:7:0:[268.5,112.2,240.1,52.2,27.2,110.2,50.2,755.1,28.2,111.2,51.2,26.2]:: ren14,ren10,ren3,ren25,ren28,ren13,ren7 ->  {}
% 98.14/25.03  === Backtracking. Learning clause 849:7:0:[808.5,152.2]:: ren14,ren10,ren3,ren25,ren13,ren7,hskp27 -> 
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 850:6:0:[600.5,722.1,34.2,36.2,520.3,150.2,135.2,134.2,133.2,126.2]:: hskp25,hskp10,hskp9,hskp8,hskp1 -> hskp20
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 851:8:0:[600.5,330.2,34.2,36.2,601.7,520.3]:: ren14,ren9,ren8,ren10,ren13,ren2,ren11 -> hskp20
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 852:7:0:[600.5,755.1,34.2,36.2,520.3]:: ren10,ren3,ren25,ren9,ren2,ren11 -> hskp20
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 854:8:0:[36.1,853.6,600.5,303.1,34.2]:: c1_1(a376),ren2,ren10,ren3,ren22,ren9 -> hskp20,c1_1(a411)
% 98.14/25.03  === Conflict found: 626:8:1:[29.1,623.3,66.1,624.4,31.1,625.9,615.7,67.2,32.2]:Top: c1_1(a384),c1_1(x0),c2_1(x0),c1_1(a400),ren17,ren8 -> hskp13,c0_1(x0) {x0 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 856:12:0:[749.0,855.11,626.3,27.2,28.2,554.2,601.7,26.2,520.3,141.2,137.2,135.2,134.2,132.2,131.2,126.2,748.1,745.1]:: hskp10,hskp7,hskp6,hskp5,hskp1,hskp16,hskp12,hskp9,hskp3,hskp2,hskp0 -> hskp13
% 98.14/25.03  === Conflict found: 821:6:0:[795.4,820.5,667.9,52.2,38.2,50.2,783.1,51.2,40.2]:: ren23,ren3,ren21,ren13,ren10 -> hskp25 {}
% 98.14/25.03  === Backtracking. Learning clause 857:6:0:[821.1,147.2]:: ren3,ren21,ren13,ren10,hskp22 -> hskp25
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a418, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 859:10:0:[762.3,858.10,615.7,112.2,90.2,32.2,110.2,91.2,31.2,111.2,687.5,601.7,520.3,152.2,147.2,137.2,135.2,134.2,132.2,127.2,126.2]:: ndr1_0,hskp27,hskp22,hskp12,hskp10,hskp9,hskp7,hskp2,hskp1 -> hskp13
% 98.14/25.03  === Conflict found: 615:11:3:[179.2,166.9]:TopTopTop: c1_1(x0),c1_1(x1),c2_1(x1),ndr1_0,c0_1(x2),c1_1(x2),c2_1(x2) -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a384, x1 -> a418, x2 -> a374}
% 98.14/25.03  === Backtracking. Learning clause 861:10:0:[5.1,860.0,615.7,112.2,90.2,32.2,110.2,91.2,31.2,111.2,687.5,601.7,520.3]:: ren28,ren3,ren23,ren8,ren10,ren13,ren2,ren11 -> hskp13,hskp20
% 98.14/25.03  === Backtracking. Learning clause 866:6:0:[14.1,862.0,70.1,863.1,13.1,864.2,16.1,865.8,168.10,72.2,39.2,38.2,772.1]:: c0_1(a387),ren10,ren18,ren4,ren9 -> c0_1(a401)
% 98.14/25.03  === Conflict found: 618:9:2:[69.1,616.3,70.1,617.5,615.7,71.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),c0_1(a401),ren18 -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a375, x1 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 868:13:0:[217.1,867.5,618.3,27.2,4.2,866.6,600.5,34.2,28.2,3.2,36.2,26.2,520.3,2.2,142.2,135.2,134.2,133.2,131.2,128.2,126.2,125.2,822.5]:: hskp17,hskp10,hskp8,hskp6,hskp0,hskp19,hskp5,hskp3,hskp1,hskp12,hskp9,hskp2 -> hskp13
% 98.14/25.03  === Conflict found: 781:6:0:[618.3,27.2,4.2,778.4,28.2,3.2,26.2,2.2]:: ren15,ren18,ren9,ren7,ren1 -> hskp13 {}
% 98.14/25.03  === Backtracking. Learning clause 869:6:0:[781.2,142.2]:: ren15,ren9,ren7,ren1,hskp17 -> hskp13
% 98.14/25.03  === Conflict found: 845:5:1:[45.1,842.0,47.1,843.4,48.1,844.5,187.1,46.2]:Top: c0_1(x0),c2_1(x0),ren12 -> c1_1(x0),hskp19 {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 870:13:0:[845.2,35.2,34.2,36.2,136.2,133.2,868.6]:: hskp11,hskp17,hskp10,hskp8,hskp6,hskp0,hskp5,hskp3,hskp1,hskp12,hskp9,hskp2 -> hskp13
% 98.14/25.03  === Conflict found: 618:9:2:[69.1,616.3,70.1,617.5,615.7,71.2]:TopTop: c1_1(x0),c1_1(x1),c2_1(x1),c0_1(a401),ren18 -> hskp13,c0_1(x0),c2_1(x0),c0_1(x1) {x0 -> a375, x1 -> a381}
% 98.14/25.03  === Backtracking. Learning clause 871:10:0:[618.3,27.2,4.2,866.6,600.5,34.2,28.2,3.2,36.2,26.2,520.3,2.2]:: ren18,ren4,ren10,ren9,ren7,ren2,ren11,ren1 -> hskp13,hskp20
% 98.14/25.03  === Backtracking. Learning clause 875:7:1:[90.1,872.3,13.1,873.4,14.1,874.5,194.10,92.2,15.2]:Top: c0_1(x0),c2_1(x0),c1_1(a418),c2_1(a378),ren23,ren4 -> c1_1(x0)
% 98.14/25.03  === Conflict found: 875:7:1:[90.1,872.3,13.1,873.4,14.1,874.5,194.10,92.2,15.2]:Top: c0_1(x0),c2_1(x0),c1_1(a418),c2_1(a378),ren23,ren4 -> c1_1(x0) {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 878:5:0:[34.1,876.0,36.1,877.6,875.2,35.2]:: c1_1(a418),c2_1(a378),ren23,ren4,ren9 -> 
% 98.14/25.03  === Backtracking. Learning clause 882:7:1:[90.1,879.3,85.1,880.4,86.1,881.6,194.10,92.2,87.2]:Top: c0_1(x0),c2_1(x0),c1_1(a418),c1_1(a411),ren23,ren22 -> c1_1(x0)
% 98.14/25.03  === Conflict found: 882:7:1:[90.1,879.3,85.1,880.4,86.1,881.6,194.10,92.2,87.2]:Top: c0_1(x0),c2_1(x0),c1_1(a418),c1_1(a411),ren23,ren22 -> c1_1(x0) {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 883:6:0:[882.2,35.2,34.2,687.5,684.6,36.2,147.2,146.2,137.2,134.2,133.2,127.2]:: hskp22,hskp21,hskp12,hskp9,hskp8,hskp2 -> 
% 98.14/25.03  === Conflict found: 600:7:1:[6.1,598.1,40.1,599.6,597.1,38.2,7.2]:Top: c0_1(x0),c1_1(a376),ren10,ren2 -> c0_1(a387),c1_1(x0),hskp20 {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 884:9:0:[600.5,783.1,34.2,36.2,520.3]:: ren10,ren3,ren21,ren9,ren2,ren11 -> hskp24,hskp25,hskp20
% 98.14/25.03  === Conflict found: 882:7:1:[90.1,879.3,85.1,880.4,86.1,881.6,194.10,92.2,87.2]:Top: c0_1(x0),c2_1(x0),c1_1(a418),c1_1(a411),ren23,ren22 -> c1_1(x0) {x0 -> a385}
% 98.14/25.03  === Backtracking. Learning clause 885:6:0:[882.2,35.2,34.2,687.5,684.6,36.2]:: ren23,ren13,ren10,ren3,ren22,ren9 -> 
% 98.14/25.03  === Clause set with instances from active satisfied. Growing active. New size: 187
% 98.14/25.03  
% 98.14/25.03  Linear Model Building succeeded.
% 98.14/25.03  SZS status Satisfiable
% 98.14/25.03  
% 98.14/25.03  Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.14/25.03  
% 98.14/25.03  SPASS-SCL-FOL Statistics:
% 98.14/25.03  Number of learned clauses: 290
% 98.14/25.03  Number of propagations: 17297
% 98.14/25.03  Number of decisions: 4629
% 98.14/25.03  Number of resolutions: 1788
% 98.14/25.03  Number of condensations: 2
% 98.14/25.03  Number of sub resolutions: 380
% 98.14/25.03  Number of input literals (deduplicated): 160
% 98.14/25.03  Number of grows: 4
% 98.14/25.03  Number of considered ground atoms: 187
% 98.14/25.03  
% 98.14/25.03   Needed:       0:0:24.50
% 98.14/25.03  
%------------------------------------------------------------------------------