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

%------------------------------------------------------------------------------
% File     : SPASS-SCL---0.1
% Problem  : SWV424-1.050 : TPTP v9.2.1. Released v3.5.0.
% Transfm  : none
% Format   : tptp
% Command  : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n022.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:37:17 PM UTC 2026

% Result   : Unsatisfiable 15.63s 3.69s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : SWV424-1.050 : TPTP v9.2.1. Released v3.5.0.
% 0.12/0.13  % Command  : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34  % Computer : n022.cluster.edu
% 0.16/0.34  % Model    : x86_64 x86_64
% 0.16/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34  % Memory   : 8042.1875MB
% 0.16/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34  % CPULimit : 300
% 0.16/0.34  % WCLimit  : 300
% 0.16/0.34  % DateTime : Thu May  7 13:28:52 EDT 2026
% 0.16/0.34  % CPUTime  : 
% 0.16/0.34  SPASS-SCL-FOL version:
% 0.19/0.43  SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 15.63/3.69  Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.63/3.69  Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.63/3.69  Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.63/3.69  Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.63/3.69  Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.63/3.69  Execution resolution_1 ended with status: unsatisfiable
% 15.63/3.69  Used heuristic: resolution_1
% 15.63/3.69  
% 15.63/3.69   Input Clauses:
% 15.63/3.69  
% 15.63/3.69   Predicates: succ last trans loop m_main_v_state node1 m_main_v_request node2 always3 node4 xuntil6 until5 until2p7 xuntil2p8 
% 15.63/3.69   Fol Constants: s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 s22 s23 s24 s25 s26 s27 s28 s29 s30 s31 s32 s33 s34 s35 s36 s37 s38 s39 s40 s41 s42 s43 s44 s45 s46 s47 s48 s49 c_ready c_busy 
% 15.63/3.69   Fol Functions: 
% 15.63/3.69   Problem Properties:
% 15.63/3.69   This is a Bernays Schoenfinkel problem.
% 15.63/3.69  
% 15.63/3.69   After reduction:  Problem Properties:
% 15.63/3.69   This is a Bernays Schoenfinkel problem.
% 15.63/3.69  
% 15.63/3.69  
% 15.63/3.69   Reduced Input Clauses:
% 15.63/3.69  
% 15.63/3.69   Most General Atoms: succ(x0,x1) trans(x0,x1) loop m_main_v_state(x0,c_ready) node1(x0) m_main_v_request(x0) node2(x0,x1) m_main_v_state(x1,c_busy) always3(x1) last(x0) node4(x0) xuntil6(x0) until5(x1) until2p7(x0) xuntil2p8(x0) 
% 15.63/3.69  
% 15.63/3.69  === Starting SPASS-SCL-FOL A Little Less Naive, considering 59 atoms initially, heuristics mode: resolution_1 ===
% 15.63/3.69  
% 15.63/3.69  === Backtracking. Learning clause 74:3:1:[58.3,60.2,61.1,55.1,51.2]:Top: m_main_v_request(s0),always3(x0),succ(s0,x0) -> 
% 15.63/3.69  === Backtracking. Learning clause 75:3:1:[58.3,60.2,61.1,55.1]:Top: m_main_v_request(s0),trans(s0,x0),always3(x0) -> 
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 208
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Backtracking. Learning clause 76:2:0:[66.1,73.1]::  -> node4(s0),xuntil6(s0)
% 15.63/3.69  === Backtracking. Learning clause 77:2:0:[67.1,3.1]:: xuntil6(s2) -> until5(s3)
% 15.63/3.69  === Backtracking. Learning clause 78:2:0:[67.1,4.1]:: xuntil6(s3) -> until5(s4)
% 15.63/3.69  === Backtracking. Learning clause 79:2:0:[67.1,12.1]:: xuntil6(s11) -> until5(s12)
% 15.63/3.69  === Backtracking. Learning clause 80:2:0:[67.1,15.1]:: xuntil6(s14) -> until5(s15)
% 15.63/3.69  === Backtracking. Learning clause 81:2:0:[67.1,16.1]:: xuntil6(s15) -> until5(s16)
% 15.63/3.69  === Backtracking. Learning clause 82:2:0:[67.1,20.1]:: xuntil6(s19) -> until5(s20)
% 15.63/3.69  === Backtracking. Learning clause 83:2:0:[67.1,21.1]:: xuntil6(s20) -> until5(s21)
% 15.63/3.69  === Backtracking. Learning clause 84:2:0:[67.1,22.1]:: xuntil6(s21) -> until5(s22)
% 15.63/3.69  === Backtracking. Learning clause 85:2:0:[67.1,25.1]:: xuntil6(s24) -> until5(s25)
% 15.63/3.69  === Backtracking. Learning clause 86:2:0:[67.1,26.1]:: xuntil6(s25) -> until5(s26)
% 15.63/3.69  === Backtracking. Learning clause 87:2:0:[67.1,29.1]:: xuntil6(s28) -> until5(s29)
% 15.63/3.69  === Backtracking. Learning clause 88:2:0:[67.1,30.1]:: xuntil6(s29) -> until5(s30)
% 15.63/3.69  === Backtracking. Learning clause 89:2:0:[67.1,36.1]:: xuntil6(s35) -> until5(s36)
% 15.63/3.69  === Backtracking. Learning clause 90:2:0:[67.1,43.1]:: xuntil6(s42) -> until5(s43)
% 15.63/3.69  === Backtracking. Learning clause 91:2:0:[67.1,45.1]:: xuntil6(s44) -> until5(s45)
% 15.63/3.69  === Backtracking. Learning clause 92:2:0:[67.1,48.1]:: xuntil6(s47) -> until5(s48)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 310
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Backtracking. Learning clause 93:2:0:[67.1,5.1]:: xuntil6(s4) -> until5(s5)
% 15.63/3.69  === Backtracking. Learning clause 94:2:0:[71.1,11.1]:: xuntil2p8(s10) -> until2p7(s11)
% 15.63/3.69  === Backtracking. Learning clause 95:2:0:[71.1,12.1]:: xuntil2p8(s11) -> until2p7(s12)
% 15.63/3.69  === Backtracking. Learning clause 96:2:0:[67.1,13.1]:: xuntil6(s12) -> until5(s13)
% 15.63/3.69  === Backtracking. Learning clause 97:2:0:[71.1,14.1]:: xuntil2p8(s13) -> until2p7(s14)
% 15.63/3.69  === Backtracking. Learning clause 98:2:0:[71.1,15.1]:: xuntil2p8(s14) -> until2p7(s15)
% 15.63/3.69  === Backtracking. Learning clause 99:2:0:[71.1,17.1]:: xuntil2p8(s16) -> until2p7(s17)
% 15.63/3.69  === Backtracking. Learning clause 100:2:0:[67.1,17.1]:: xuntil6(s16) -> until5(s17)
% 15.63/3.69  === Backtracking. Learning clause 101:2:0:[67.1,19.1]:: xuntil6(s18) -> until5(s19)
% 15.63/3.69  === Backtracking. Learning clause 102:2:0:[67.1,31.1]:: xuntil6(s30) -> until5(s31)
% 15.63/3.69  === Backtracking. Learning clause 103:2:0:[71.1,32.1]:: xuntil2p8(s31) -> until2p7(s32)
% 15.63/3.69  === Backtracking. Learning clause 104:2:0:[67.1,32.1]:: xuntil6(s31) -> until5(s32)
% 15.63/3.69  === Backtracking. Learning clause 105:2:0:[71.1,34.1]:: xuntil2p8(s33) -> until2p7(s34)
% 15.63/3.69  === Backtracking. Learning clause 106:2:0:[67.1,34.1]:: xuntil6(s33) -> until5(s34)
% 15.63/3.69  === Backtracking. Learning clause 107:2:0:[71.1,38.1]:: xuntil2p8(s37) -> until2p7(s38)
% 15.63/3.69  === Backtracking. Learning clause 108:2:0:[71.1,41.1]:: xuntil2p8(s40) -> until2p7(s41)
% 15.63/3.69  === Backtracking. Learning clause 109:2:0:[67.1,41.1]:: xuntil6(s40) -> until5(s41)
% 15.63/3.69  === Backtracking. Learning clause 110:2:0:[71.1,42.1]:: xuntil2p8(s41) -> until2p7(s42)
% 15.63/3.69  === Backtracking. Learning clause 111:2:0:[67.1,42.1]:: xuntil6(s41) -> until5(s42)
% 15.63/3.69  === Backtracking. Learning clause 112:2:0:[71.1,44.1]:: xuntil2p8(s43) -> until2p7(s44)
% 15.63/3.69  === Backtracking. Learning clause 113:2:0:[67.1,44.1]:: xuntil6(s43) -> until5(s44)
% 15.63/3.69  === Backtracking. Learning clause 114:2:0:[71.1,45.1]:: xuntil2p8(s44) -> until2p7(s45)
% 15.63/3.69  === Backtracking. Learning clause 115:2:0:[67.1,47.1]:: xuntil6(s46) -> until5(s47)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 344
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Backtracking. Learning clause 116:3:0:[66.1,79.2]:: xuntil6(s11) -> node4(s12),xuntil6(s12)
% 15.63/3.69  === Backtracking. Learning clause 117:3:0:[66.1,81.2]:: xuntil6(s15) -> node4(s16),xuntil6(s16)
% 15.63/3.69  === Backtracking. Learning clause 118:3:0:[66.1,84.2]:: xuntil6(s21) -> node4(s22),xuntil6(s22)
% 15.63/3.69  === Backtracking. Learning clause 119:3:0:[66.1,89.2]:: xuntil6(s35) -> node4(s36),xuntil6(s36)
% 15.63/3.69  === Backtracking. Learning clause 120:3:0:[66.1,90.2]:: xuntil6(s42) -> node4(s43),xuntil6(s43)
% 15.63/3.69  === Backtracking. Learning clause 121:3:0:[66.1,115.2]:: xuntil6(s46) -> node4(s47),xuntil6(s47)
% 15.63/3.69  === Conflict found: 105:2:0:[71.1,34.1]:: xuntil2p8(s33) -> until2p7(s34) {}
% 15.63/3.69  === Backtracking. Learning clause 122:3:0:[105.1,70.3]:: until2p7(s33) -> until2p7(s34),node4(s33)
% 15.63/3.69  === Backtracking. Learning clause 123:2:0:[67.1,2.1]:: xuntil6(s1) -> until5(s2)
% 15.63/3.69  === Backtracking. Learning clause 124:2:0:[71.1,3.1]:: xuntil2p8(s2) -> until2p7(s3)
% 15.63/3.69  === Backtracking. Learning clause 125:2:0:[71.1,6.1]:: xuntil2p8(s5) -> until2p7(s6)
% 15.63/3.69  === Backtracking. Learning clause 126:2:0:[71.1,9.1]:: xuntil2p8(s8) -> until2p7(s9)
% 15.63/3.69  === Backtracking. Learning clause 127:2:0:[71.1,10.1]:: xuntil2p8(s9) -> until2p7(s10)
% 15.63/3.69  === Backtracking. Learning clause 128:2:0:[67.1,11.1]:: xuntil6(s10) -> until5(s11)
% 15.63/3.69  === Backtracking. Learning clause 129:3:0:[71.1,13.1,70.3]:: until2p7(s12) -> until2p7(s13),node4(s12)
% 15.63/3.69  === Backtracking. Learning clause 130:2:0:[67.1,14.1]:: xuntil6(s13) -> until5(s14)
% 15.63/3.69  === Backtracking. Learning clause 131:2:0:[71.1,18.1]:: xuntil2p8(s17) -> until2p7(s18)
% 15.63/3.69  === Backtracking. Learning clause 132:2:0:[71.1,21.1]:: xuntil2p8(s20) -> until2p7(s21)
% 15.63/3.69  === Backtracking. Learning clause 133:3:0:[71.1,23.1,70.3]:: until2p7(s22) -> until2p7(s23),node4(s22)
% 15.63/3.69  === Backtracking. Learning clause 134:2:0:[67.1,23.1]:: xuntil6(s22) -> until5(s23)
% 15.63/3.69  === Backtracking. Learning clause 135:2:0:[71.1,26.1]:: xuntil2p8(s25) -> until2p7(s26)
% 15.63/3.69  === Backtracking. Learning clause 136:2:0:[71.1,28.1]:: xuntil2p8(s27) -> until2p7(s28)
% 15.63/3.69  === Backtracking. Learning clause 137:2:0:[71.1,30.1]:: xuntil2p8(s29) -> until2p7(s30)
% 15.63/3.69  === Backtracking. Learning clause 138:2:0:[67.1,33.1]:: xuntil6(s32) -> until5(s33)
% 15.63/3.69  === Backtracking. Learning clause 139:3:0:[71.1,37.1,70.3]:: until2p7(s36) -> until2p7(s37),node4(s36)
% 15.63/3.69  === Backtracking. Learning clause 140:2:0:[67.1,37.1]:: xuntil6(s36) -> until5(s37)
% 15.63/3.69  === Backtracking. Learning clause 141:2:0:[67.1,38.1]:: xuntil6(s37) -> until5(s38)
% 15.63/3.69  === Backtracking. Learning clause 142:2:0:[67.1,40.1]:: xuntil6(s39) -> until5(s40)
% 15.63/3.69  === Backtracking. Learning clause 143:3:0:[71.1,43.1,70.3]:: until2p7(s42) -> until2p7(s43),node4(s42)
% 15.63/3.69  === Conflict found: 112:2:0:[71.1,44.1]:: xuntil2p8(s43) -> until2p7(s44) {}
% 15.63/3.69  === Backtracking. Learning clause 144:3:0:[112.1,70.3]:: until2p7(s43) -> until2p7(s44),node4(s43)
% 15.63/3.69  === Backtracking. Learning clause 145:2:0:[71.1,47.1]:: xuntil2p8(s46) -> until2p7(s47)
% 15.63/3.69  === Backtracking. Learning clause 146:2:0:[71.1,49.1]:: xuntil2p8(s48) -> until2p7(s49)
% 15.63/3.69  === Backtracking. Learning clause 147:2:0:[67.1,49.1]:: xuntil6(s48) -> until5(s49)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 358
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Backtracking. Learning clause 148:3:0:[66.1,80.2]:: xuntil6(s14) -> node4(s15),xuntil6(s15)
% 15.63/3.69  === Backtracking. Learning clause 149:3:0:[66.1,85.2]:: xuntil6(s24) -> node4(s25),xuntil6(s25)
% 15.63/3.69  === Backtracking. Learning clause 150:3:0:[66.1,86.2]:: xuntil6(s25) -> node4(s26),xuntil6(s26)
% 15.63/3.69  === Conflict found: 135:2:0:[71.1,26.1]:: xuntil2p8(s25) -> until2p7(s26) {}
% 15.63/3.69  === Backtracking. Learning clause 151:3:0:[135.1,70.3]:: until2p7(s25) -> until2p7(s26),node4(s25)
% 15.63/3.69  === Backtracking. Learning clause 152:3:1:[70.3,72.2]:Top: until2p7(x0),last(x0) -> node4(x0)
% 15.63/3.69  === Conflict found: 110:2:0:[71.1,42.1]:: xuntil2p8(s41) -> until2p7(s42) {}
% 15.63/3.69  === Backtracking. Learning clause 153:3:0:[110.1,70.3]:: until2p7(s41) -> until2p7(s42),node4(s41)
% 15.63/3.69  === Conflict found: 74:3:1:[58.3,60.2,61.1,55.1,51.2]:Top: m_main_v_request(s0),always3(x0),succ(s0,x0) ->  {x0 -> s1}
% 15.63/3.69  === Backtracking. Learning clause 154:2:0:[74.3,1.1]:: m_main_v_request(s0),always3(s1) -> 
% 15.63/3.69  === Backtracking. Learning clause 155:2:0:[67.1,1.1]:: xuntil6(s0) -> until5(s1)
% 15.63/3.69  === Backtracking. Learning clause 156:3:0:[71.1,4.1,70.3]:: until2p7(s3) -> until2p7(s4),node4(s3)
% 15.63/3.69  === Backtracking. Learning clause 157:2:0:[67.1,7.1]:: xuntil6(s6) -> until5(s7)
% 15.63/3.69  === Backtracking. Learning clause 158:2:0:[71.1,8.1]:: xuntil2p8(s7) -> until2p7(s8)
% 15.63/3.69  === Backtracking. Learning clause 159:2:0:[71.1,16.1]:: xuntil2p8(s15) -> until2p7(s16)
% 15.63/3.69  === Backtracking. Learning clause 160:2:0:[71.1,19.1]:: xuntil2p8(s18) -> until2p7(s19)
% 15.63/3.69  === Backtracking. Learning clause 161:3:0:[71.1,24.1,70.3]:: until2p7(s23) -> until2p7(s24),node4(s23)
% 15.63/3.69  === Backtracking. Learning clause 162:3:0:[71.1,27.1,70.3]:: until2p7(s26) -> until2p7(s27),node4(s26)
% 15.63/3.69  === Conflict found: 136:2:0:[71.1,28.1]:: xuntil2p8(s27) -> until2p7(s28) {}
% 15.63/3.69  === Backtracking. Learning clause 163:3:0:[136.1,70.3]:: until2p7(s27) -> until2p7(s28),node4(s27)
% 15.63/3.69  === Backtracking. Learning clause 164:2:0:[67.1,27.1]:: xuntil6(s26) -> until5(s27)
% 15.63/3.69  === Backtracking. Learning clause 165:3:0:[71.1,35.1,70.3]:: until2p7(s34) -> until2p7(s35),node4(s34)
% 15.63/3.69  === Backtracking. Learning clause 166:2:0:[71.1,36.1]:: xuntil2p8(s35) -> until2p7(s36)
% 15.63/3.69  === Backtracking. Learning clause 167:3:0:[71.1,39.1,70.3]:: until2p7(s38) -> until2p7(s39),node4(s38)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 380
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Backtracking. Learning clause 168:3:0:[66.1,155.2]:: xuntil6(s0) -> node4(s1),xuntil6(s1)
% 15.63/3.69  === Backtracking. Learning clause 169:3:0:[66.1,134.2]:: xuntil6(s22) -> node4(s23),xuntil6(s23)
% 15.63/3.69  === Backtracking. Learning clause 170:3:0:[66.1,138.2]:: xuntil6(s32) -> node4(s33),xuntil6(s33)
% 15.63/3.69  === Backtracking. Learning clause 171:3:0:[66.1,106.2]:: xuntil6(s33) -> node4(s34),xuntil6(s34)
% 15.63/3.69  === Backtracking. Learning clause 172:3:0:[66.1,113.2]:: xuntil6(s43) -> node4(s44),xuntil6(s44)
% 15.63/3.69  === Conflict found: 133:3:0:[71.1,23.1,70.3]:: until2p7(s22) -> until2p7(s23),node4(s22) {}
% 15.63/3.69  === Backtracking. Learning clause 173:4:0:[133.2,152.1]:: until2p7(s22),last(s23) -> node4(s22),node4(s23)
% 15.63/3.69  === Conflict found: 166:2:0:[71.1,36.1]:: xuntil2p8(s35) -> until2p7(s36) {}
% 15.63/3.69  === Backtracking. Learning clause 174:6:0:[166.1,70.3,152.1,165.2,122.2]:: last(s36),until2p7(s33) -> node4(s35),node4(s36),node4(s34),node4(s33)
% 15.63/3.69  === Conflict found: 166:2:0:[71.1,36.1]:: xuntil2p8(s35) -> until2p7(s36) {}
% 15.63/3.69  === Backtracking. Learning clause 175:5:0:[166.1,70.3,152.1,165.2]:: last(s36),until2p7(s34) -> node4(s35),node4(s36),node4(s34)
% 15.63/3.69  === Conflict found: 146:2:0:[71.1,49.1]:: xuntil2p8(s48) -> until2p7(s49) {}
% 15.63/3.69  === Backtracking. Learning clause 177:3:0:[50.0,176.1,146.1,70.3,152.1]:: until2p7(s48) -> node4(s48),node4(s49)
% 15.63/3.69  === Backtracking. Learning clause 178:2:0:[71.1,1.1]:: xuntil2p8(s0) -> until2p7(s1)
% 15.63/3.69  === Backtracking. Learning clause 179:2:0:[67.1,6.1]:: xuntil6(s5) -> until5(s6)
% 15.63/3.69  === Backtracking. Learning clause 180:2:0:[71.1,13.1]:: xuntil2p8(s12) -> until2p7(s13)
% 15.63/3.69  === Backtracking. Learning clause 181:3:0:[67.1,18.1,66.1]:: xuntil6(s17) -> node4(s18),xuntil6(s18)
% 15.63/3.69  === Backtracking. Learning clause 182:3:0:[66.1,101.2]:: xuntil6(s18) -> node4(s19),xuntil6(s19)
% 15.63/3.69  === Backtracking. Learning clause 183:2:0:[67.1,18.1]:: xuntil6(s17) -> until5(s18)
% 15.63/3.69  === Backtracking. Learning clause 184:2:0:[71.1,22.1]:: xuntil2p8(s21) -> until2p7(s22)
% 15.63/3.69  === Backtracking. Learning clause 185:2:0:[71.1,23.1]:: xuntil2p8(s22) -> until2p7(s23)
% 15.63/3.69  === Backtracking. Learning clause 186:3:0:[67.1,24.1,66.1]:: xuntil6(s23) -> node4(s24),xuntil6(s24)
% 15.63/3.69  === Backtracking. Learning clause 187:2:0:[67.1,28.1]:: xuntil6(s27) -> until5(s28)
% 15.63/3.69  === Backtracking. Learning clause 188:7:0:[71.1,33.1,70.3,174.2]:: until2p7(s32),last(s36) -> node4(s32),node4(s35),node4(s36),node4(s34),node4(s33)
% 15.63/3.69  === Backtracking. Learning clause 189:2:0:[71.1,33.1]:: xuntil2p8(s32) -> until2p7(s33)
% 15.63/3.69  === Backtracking. Learning clause 190:2:0:[71.1,35.1]:: xuntil2p8(s34) -> until2p7(s35)
% 15.63/3.69  === Backtracking. Learning clause 191:3:0:[67.1,35.1,66.1]:: xuntil6(s34) -> node4(s35),xuntil6(s35)
% 15.63/3.69  === Backtracking. Learning clause 192:2:0:[71.1,39.1]:: xuntil2p8(s38) -> until2p7(s39)
% 15.63/3.69  === Backtracking. Learning clause 193:3:0:[67.1,39.1,66.1]:: xuntil6(s38) -> node4(s39),xuntil6(s39)
% 15.63/3.69  === Backtracking. Learning clause 194:3:0:[66.1,142.2]:: xuntil6(s39) -> node4(s40),xuntil6(s40)
% 15.63/3.69  === Backtracking. Learning clause 195:2:0:[67.1,39.1]:: xuntil6(s38) -> until5(s39)
% 15.63/3.69  === Backtracking. Learning clause 196:3:0:[71.1,46.1,70.3]:: until2p7(s45) -> until2p7(s46),node4(s45)
% 15.63/3.69  === Backtracking. Learning clause 197:2:0:[67.1,46.1]:: xuntil6(s45) -> until5(s46)
% 15.63/3.69  === Backtracking. Learning clause 198:2:0:[71.1,48.1]:: xuntil2p8(s47) -> until2p7(s48)
% 15.63/3.69  === Backtracking. Learning clause 199:2:0:[58.3,60.2,54.2,55.1,51.2]:: m_main_v_request(s0),succ(s0,s0) -> 
% 15.63/3.69  === Backtracking. Learning clause 200:2:0:[58.3,60.2,54.2,55.1]:: m_main_v_request(s0),trans(s0,s0) -> 
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 387
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Conflict found: 182:3:0:[66.1,101.2]:: xuntil6(s18) -> node4(s19),xuntil6(s19) {}
% 15.63/3.69  === Backtracking. Learning clause 201:5:0:[182.3,68.2,181.3]:: last(s19),xuntil6(s17) -> node4(s19),loop,node4(s18)
% 15.63/3.69  === Conflict found: 150:3:0:[66.1,86.2]:: xuntil6(s25) -> node4(s26),xuntil6(s26) {}
% 15.63/3.69  === Backtracking. Learning clause 202:4:0:[150.3,68.2]:: xuntil6(s25),last(s26) -> node4(s26),loop
% 15.63/3.69  === Backtracking. Learning clause 203:3:0:[66.1,78.2]:: xuntil6(s3) -> node4(s4),xuntil6(s4)
% 15.63/3.69  === Backtracking. Learning clause 204:5:0:[66.1,96.2,68.2,116.3]:: last(s13),xuntil6(s11) -> node4(s13),loop,node4(s12)
% 15.63/3.69  === Backtracking. Learning clause 206:3:0:[50.0,205.1,66.1,147.2,68.2]:: xuntil6(s48) -> node4(s49),loop
% 15.63/3.69  === Conflict found: 94:2:0:[71.1,11.1]:: xuntil2p8(s10) -> until2p7(s11) {}
% 15.63/3.69  === Backtracking. Learning clause 207:3:0:[94.1,70.3]:: until2p7(s10) -> until2p7(s11),node4(s10)
% 15.63/3.69  === Conflict found: 95:2:0:[71.1,12.1]:: xuntil2p8(s11) -> until2p7(s12) {}
% 15.63/3.69  === Backtracking. Learning clause 208:3:0:[95.1,70.3]:: until2p7(s11) -> until2p7(s12),node4(s11)
% 15.63/3.69  === Conflict found: 129:3:0:[71.1,13.1,70.3]:: until2p7(s12) -> until2p7(s13),node4(s12) {}
% 15.63/3.69  === Backtracking. Learning clause 209:6:0:[129.2,152.1,208.2,207.2]:: last(s13),until2p7(s10) -> node4(s12),node4(s13),node4(s11),node4(s10)
% 15.63/3.69  === Conflict found: 127:2:0:[71.1,10.1]:: xuntil2p8(s9) -> until2p7(s10) {}
% 15.63/3.69  === Backtracking. Learning clause 210:7:0:[127.1,70.3,209.2]:: until2p7(s9),last(s13) -> node4(s9),node4(s12),node4(s13),node4(s11),node4(s10)
% 15.63/3.69  === Conflict found: 160:2:0:[71.1,19.1]:: xuntil2p8(s18) -> until2p7(s19) {}
% 15.63/3.69  === Backtracking. Learning clause 211:4:0:[160.1,70.3,152.1]:: until2p7(s18),last(s19) -> node4(s18),node4(s19)
% 15.63/3.69  === Conflict found: 189:2:0:[71.1,33.1]:: xuntil2p8(s32) -> until2p7(s33) {}
% 15.63/3.69  === Backtracking. Learning clause 212:3:0:[189.1,70.3]:: until2p7(s32) -> until2p7(s33),node4(s32)
% 15.63/3.69  === Conflict found: 145:2:0:[71.1,47.1]:: xuntil2p8(s46) -> until2p7(s47) {}
% 15.63/3.69  === Backtracking. Learning clause 213:3:0:[145.1,70.3]:: until2p7(s46) -> until2p7(s47),node4(s46)
% 15.63/3.69  === Conflict found: 198:2:0:[71.1,48.1]:: xuntil2p8(s47) -> until2p7(s48) {}
% 15.63/3.69  === Backtracking. Learning clause 214:3:0:[198.1,70.3]:: until2p7(s47) -> until2p7(s48),node4(s47)
% 15.63/3.69  === Backtracking. Learning clause 215:2:0:[67.1,9.1]:: xuntil6(s8) -> until5(s9)
% 15.63/3.69  === Backtracking. Learning clause 216:3:0:[67.1,10.1,66.1]:: xuntil6(s9) -> node4(s10),xuntil6(s10)
% 15.63/3.69  === Backtracking. Learning clause 217:7:0:[66.1,128.2,204.2,216.3]:: last(s13),xuntil6(s9) -> node4(s11),node4(s13),loop,node4(s12),node4(s10)
% 15.63/3.69  === Backtracking. Learning clause 218:8:0:[66.1,215.2,217.2]:: xuntil6(s8),last(s13) -> node4(s9),node4(s11),node4(s13),loop,node4(s12),node4(s10)
% 15.63/3.69  === Backtracking. Learning clause 219:2:0:[71.1,29.1]:: xuntil2p8(s28) -> until2p7(s29)
% 15.63/3.69  === Backtracking. Learning clause 220:2:0:[71.1,37.1]:: xuntil2p8(s36) -> until2p7(s37)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 390
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Conflict found: 181:3:0:[67.1,18.1,66.1]:: xuntil6(s17) -> node4(s18),xuntil6(s18) {}
% 15.63/3.69  === Backtracking. Learning clause 221:4:0:[181.3,68.2]:: xuntil6(s17),last(s18) -> node4(s18),loop
% 15.63/3.69  === Backtracking. Learning clause 222:3:0:[66.1,77.2]:: xuntil6(s2) -> node4(s3),xuntil6(s3)
% 15.63/3.69  === Conflict found: 203:3:0:[66.1,78.2]:: xuntil6(s3) -> node4(s4),xuntil6(s4) {}
% 15.63/3.69  === Backtracking. Learning clause 223:5:0:[203.3,68.2,222.3]:: last(s4),xuntil6(s2) -> node4(s4),loop,node4(s3)
% 15.63/3.69  === Backtracking. Learning clause 224:3:0:[66.1,215.2]:: xuntil6(s8) -> node4(s9),xuntil6(s9)
% 15.63/3.69  === Backtracking. Learning clause 225:3:0:[66.1,96.2]:: xuntil6(s12) -> node4(s13),xuntil6(s13)
% 15.63/3.69  === Backtracking. Learning clause 226:3:0:[66.1,130.2]:: xuntil6(s13) -> node4(s14),xuntil6(s14)
% 15.63/3.69  === Backtracking. Learning clause 227:3:0:[66.1,82.2]:: xuntil6(s19) -> node4(s20),xuntil6(s20)
% 15.63/3.69  === Backtracking. Learning clause 228:3:0:[66.1,88.2]:: xuntil6(s29) -> node4(s30),xuntil6(s30)
% 15.63/3.69  === Conflict found: 153:3:0:[110.1,70.3]:: until2p7(s41) -> until2p7(s42),node4(s41) {}
% 15.63/3.69  === Backtracking. Learning clause 229:4:0:[153.2,152.1]:: until2p7(s41),last(s42) -> node4(s41),node4(s42)
% 15.63/3.69  === Conflict found: 196:3:0:[71.1,46.1,70.3]:: until2p7(s45) -> until2p7(s46),node4(s45) {}
% 15.63/3.69  === Backtracking. Learning clause 230:4:0:[196.2,152.1]:: until2p7(s45),last(s46) -> node4(s45),node4(s46)
% 15.63/3.69  === Conflict found: 178:2:0:[71.1,1.1]:: xuntil2p8(s0) -> until2p7(s1) {}
% 15.63/3.69  === Backtracking. Learning clause 231:3:0:[178.1,70.3]:: until2p7(s0) -> until2p7(s1),node4(s0)
% 15.63/3.69  === Backtracking. Learning clause 232:2:0:[71.1,7.1]:: xuntil2p8(s6) -> until2p7(s7)
% 15.63/3.69  === Backtracking. Learning clause 233:2:0:[71.1,20.1]:: xuntil2p8(s19) -> until2p7(s20)
% 15.63/3.69  === Backtracking. Learning clause 234:3:0:[71.1,31.1,70.3]:: until2p7(s30) -> until2p7(s31),node4(s30)
% 15.63/3.69  === Backtracking. Learning clause 235:2:0:[71.1,46.1]:: xuntil2p8(s45) -> until2p7(s46)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 396
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Conflict found: 76:2:0:[66.1,73.1]::  -> node4(s0),xuntil6(s0) {}
% 15.63/3.69  === Backtracking. Learning clause 236:2:0:[76.2,68.2,65.1,63.1]:: last(s0) -> loop
% 15.63/3.69  === Conflict found: 171:3:0:[66.1,106.2]:: xuntil6(s33) -> node4(s34),xuntil6(s34) {}
% 15.63/3.69  === Backtracking. Learning clause 237:5:0:[171.3,68.2,170.3]:: last(s34),xuntil6(s32) -> node4(s34),loop,node4(s33)
% 15.63/3.69  === Backtracking. Learning clause 238:6:0:[66.1,123.2,223.2]:: xuntil6(s1),last(s4) -> node4(s2),node4(s4),loop,node4(s3)
% 15.63/3.69  === Backtracking. Learning clause 239:4:0:[66.1,111.2,68.2]:: xuntil6(s41),last(s42) -> node4(s42),loop
% 15.63/3.69  === Backtracking. Learning clause 240:5:0:[66.1,109.2,239.1]:: xuntil6(s40),last(s42) -> node4(s41),node4(s42),loop
% 15.63/3.69  === Conflict found: 122:3:0:[105.1,70.3]:: until2p7(s33) -> until2p7(s34),node4(s33) {}
% 15.63/3.69  === Backtracking. Learning clause 241:4:0:[122.2,152.1]:: until2p7(s33),last(s34) -> node4(s33),node4(s34)
% 15.63/3.69  === Conflict found: 108:2:0:[71.1,41.1]:: xuntil2p8(s40) -> until2p7(s41) {}
% 15.63/3.69  === Backtracking. Learning clause 242:5:0:[108.1,70.3,229.1]:: until2p7(s40),last(s42) -> node4(s40),node4(s41),node4(s42)
% 15.63/3.69  === Backtracking. Learning clause 243:3:0:[71.1,2.1,70.3]:: until2p7(s1) -> until2p7(s2),node4(s1)
% 15.63/3.69  === Conflict found: 124:2:0:[71.1,3.1]:: xuntil2p8(s2) -> until2p7(s3) {}
% 15.63/3.69  === Backtracking. Learning clause 244:5:0:[124.1,70.3,152.1,243.2]:: last(s3),until2p7(s1) -> node4(s2),node4(s3),node4(s1)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 397
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Conflict found: 168:3:0:[66.1,155.2]:: xuntil6(s0) -> node4(s1),xuntil6(s1) {}
% 15.63/3.69  === Backtracking. Learning clause 245:4:0:[168.3,68.2]:: xuntil6(s0),last(s1) -> node4(s1),loop
% 15.63/3.69  === Conflict found: 216:3:0:[67.1,10.1,66.1]:: xuntil6(s9) -> node4(s10),xuntil6(s10) {}
% 15.63/3.69  === Backtracking. Learning clause 246:4:0:[216.3,68.2]:: xuntil6(s9),last(s10) -> node4(s10),loop
% 15.63/3.69  === Conflict found: 226:3:0:[66.1,130.2]:: xuntil6(s13) -> node4(s14),xuntil6(s14) {}
% 15.63/3.69  === Backtracking. Learning clause 247:4:0:[226.3,68.2]:: xuntil6(s13),last(s14) -> node4(s14),loop
% 15.63/3.69  === Conflict found: 172:3:0:[66.1,113.2]:: xuntil6(s43) -> node4(s44),xuntil6(s44) {}
% 15.63/3.69  === Backtracking. Learning clause 248:5:0:[172.3,68.2,120.3]:: last(s44),xuntil6(s42) -> node4(s44),loop,node4(s43)
% 15.63/3.69  === Backtracking. Learning clause 249:3:0:[66.1,104.2]:: xuntil6(s31) -> node4(s32),xuntil6(s32)
% 15.63/3.69  === Conflict found: 170:3:0:[66.1,138.2]:: xuntil6(s32) -> node4(s33),xuntil6(s33) {}
% 15.63/3.69  === Backtracking. Learning clause 250:5:0:[170.3,68.2,249.3]:: last(s33),xuntil6(s31) -> node4(s33),loop,node4(s32)
% 15.63/3.69  === Conflict found: 212:3:0:[189.1,70.3]:: until2p7(s32) -> until2p7(s33),node4(s32) {}
% 15.63/3.69  === Backtracking. Learning clause 251:4:0:[212.2,152.1]:: until2p7(s32),last(s33) -> node4(s32),node4(s33)
% 15.63/3.69  === Conflict found: 144:3:0:[112.1,70.3]:: until2p7(s43) -> until2p7(s44),node4(s43) {}
% 15.63/3.69  === Backtracking. Learning clause 252:4:0:[144.2,152.1]:: until2p7(s43),last(s44) -> node4(s43),node4(s44)
% 15.63/3.69  === Conflict found: 158:2:0:[71.1,8.1]:: xuntil2p8(s7) -> until2p7(s8) {}
% 15.63/3.69  === Backtracking. Learning clause 253:3:0:[158.1,70.3]:: until2p7(s7) -> until2p7(s8),node4(s7)
% 15.63/3.69  === Conflict found: 127:2:0:[71.1,10.1]:: xuntil2p8(s9) -> until2p7(s10) {}
% 15.63/3.69  === Backtracking. Learning clause 254:4:0:[127.1,70.3,152.1]:: until2p7(s9),last(s10) -> node4(s9),node4(s10)
% 15.63/3.69  === Conflict found: 126:2:0:[71.1,9.1]:: xuntil2p8(s8) -> until2p7(s9) {}
% 15.63/3.69  === Backtracking. Learning clause 255:6:0:[126.1,70.3,254.1,253.2]:: last(s10),until2p7(s7) -> node4(s8),node4(s9),node4(s10),node4(s7)
% 15.63/3.69  === Conflict found: 97:2:0:[71.1,14.1]:: xuntil2p8(s13) -> until2p7(s14) {}
% 15.63/3.69  === Backtracking. Learning clause 256:4:0:[97.1,70.3,152.1]:: until2p7(s13),last(s14) -> node4(s13),node4(s14)
% 15.63/3.69  === Conflict found: 160:2:0:[71.1,19.1]:: xuntil2p8(s18) -> until2p7(s19) {}
% 15.63/3.69  === Backtracking. Learning clause 257:3:0:[160.1,70.3]:: until2p7(s18) -> until2p7(s19),node4(s18)
% 15.63/3.69  === Conflict found: 137:2:0:[71.1,30.1]:: xuntil2p8(s29) -> until2p7(s30) {}
% 15.63/3.69  === Backtracking. Learning clause 258:3:0:[137.1,70.3]:: until2p7(s29) -> until2p7(s30),node4(s29)
% 15.63/3.69  === Conflict found: 107:2:0:[71.1,38.1]:: xuntil2p8(s37) -> until2p7(s38) {}
% 15.63/3.69  === Backtracking. Learning clause 259:3:0:[107.1,70.3]:: until2p7(s37) -> until2p7(s38),node4(s37)
% 15.63/3.69  === Backtracking. Learning clause 260:2:0:[71.1,40.1]:: xuntil2p8(s39) -> until2p7(s40)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 400
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Conflict found: 149:3:0:[66.1,85.2]:: xuntil6(s24) -> node4(s25),xuntil6(s25) {}
% 15.63/3.69  === Backtracking. Learning clause 261:6:0:[149.3,202.1,186.3]:: last(s26),xuntil6(s23) -> node4(s25),node4(s26),loop,node4(s24)
% 15.63/3.69  === Conflict found: 149:3:0:[66.1,85.2]:: xuntil6(s24) -> node4(s25),xuntil6(s25) {}
% 15.63/3.69  === Backtracking. Learning clause 262:5:0:[149.3,202.1]:: xuntil6(s24),last(s26) -> node4(s25),node4(s26),loop
% 15.63/3.69  === Conflict found: 228:3:0:[66.1,88.2]:: xuntil6(s29) -> node4(s30),xuntil6(s30) {}
% 15.63/3.69  === Backtracking. Learning clause 263:4:0:[228.3,68.2]:: xuntil6(s29),last(s30) -> node4(s30),loop
% 15.63/3.69  === Conflict found: 172:3:0:[66.1,113.2]:: xuntil6(s43) -> node4(s44),xuntil6(s44) {}
% 15.63/3.69  === Backtracking. Learning clause 264:4:0:[172.3,68.2]:: xuntil6(s43),last(s44) -> node4(s44),loop
% 15.63/3.69  === Backtracking. Learning clause 265:3:0:[66.1,123.2]:: xuntil6(s1) -> node4(s2),xuntil6(s2)
% 15.63/3.69  === Conflict found: 222:3:0:[66.1,77.2]:: xuntil6(s2) -> node4(s3),xuntil6(s3) {}
% 15.63/3.69  === Backtracking. Learning clause 266:5:0:[222.3,68.2,265.3]:: last(s3),xuntil6(s1) -> node4(s3),loop,node4(s2)
% 15.63/3.69  === Conflict found: 151:3:0:[135.1,70.3]:: until2p7(s25) -> until2p7(s26),node4(s25) {}
% 15.63/3.69  === Backtracking. Learning clause 267:4:0:[151.2,152.1]:: until2p7(s25),last(s26) -> node4(s25),node4(s26)
% 15.63/3.69  === Conflict found: 124:2:0:[71.1,3.1]:: xuntil2p8(s2) -> until2p7(s3) {}
% 15.63/3.69  === Backtracking. Learning clause 268:4:0:[124.1,70.3,152.1]:: until2p7(s2),last(s3) -> node4(s2),node4(s3)
% 15.63/3.69  === Conflict found: 232:2:0:[71.1,7.1]:: xuntil2p8(s6) -> until2p7(s7) {}
% 15.63/3.69  === Backtracking. Learning clause 269:3:0:[232.1,70.3]:: until2p7(s6) -> until2p7(s7),node4(s6)
% 15.63/3.69  === Conflict found: 253:3:0:[158.1,70.3]:: until2p7(s7) -> until2p7(s8),node4(s7) {}
% 15.63/3.69  === Backtracking. Learning clause 270:5:0:[253.2,152.1,269.2]:: last(s8),until2p7(s6) -> node4(s7),node4(s8),node4(s6)
% 15.63/3.69  === Backtracking. Learning clause 271:4:0:[67.1,8.1,66.1,68.2]:: xuntil6(s7),last(s8) -> node4(s8),loop
% 15.63/3.69  === Backtracking. Learning clause 272:5:0:[66.1,157.2,271.1]:: xuntil6(s6),last(s8) -> node4(s7),node4(s8),loop
% 15.63/3.69  === Backtracking. Learning clause 273:5:0:[71.1,25.1,70.3,267.1]:: until2p7(s24),last(s26) -> node4(s24),node4(s25),node4(s26)
% 15.63/3.69  === Backtracking. Learning clause 274:2:0:[71.1,25.1]:: xuntil2p8(s24) -> until2p7(s25)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 401
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Backtracking. Learning clause 275:3:0:[66.1,100.2]:: xuntil6(s16) -> node4(s17),xuntil6(s17)
% 15.63/3.69  === Backtracking. Learning clause 276:3:0:[66.1,141.2]:: xuntil6(s37) -> node4(s38),xuntil6(s38)
% 15.63/3.69  === Backtracking. Learning clause 277:3:0:[66.1,92.2]:: xuntil6(s47) -> node4(s48),xuntil6(s48)
% 15.63/3.69  === Conflict found: 124:2:0:[71.1,3.1]:: xuntil2p8(s2) -> until2p7(s3) {}
% 15.63/3.69  === Backtracking. Learning clause 278:3:0:[124.1,70.3]:: until2p7(s2) -> until2p7(s3),node4(s2)
% 15.63/3.69  === Conflict found: 131:2:0:[71.1,18.1]:: xuntil2p8(s17) -> until2p7(s18) {}
% 15.63/3.69  === Backtracking. Learning clause 279:3:0:[131.1,70.3]:: until2p7(s17) -> until2p7(s18),node4(s17)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 402
% 15.63/3.69  === Restarting.
% 15.63/3.69  === Backtracking. Learning clause 280:4:0:[66.1,197.2,68.2]:: xuntil6(s45),last(s46) -> node4(s46),loop
% 15.63/3.69  === Backtracking. Learning clause 281:5:0:[66.1,91.2,280.1]:: xuntil6(s44),last(s46) -> node4(s45),node4(s46),loop
% 15.63/3.69  === Conflict found: 208:3:0:[95.1,70.3]:: until2p7(s11) -> until2p7(s12),node4(s11) {}
% 15.63/3.69  === Backtracking. Learning clause 282:4:0:[208.2,152.1]:: until2p7(s11),last(s12) -> node4(s11),node4(s12)
% 15.63/3.69  === Conflict found: 279:3:0:[131.1,70.3]:: until2p7(s17) -> until2p7(s18),node4(s17) {}
% 15.63/3.69  === Backtracking. Learning clause 283:4:0:[279.2,152.1]:: until2p7(s17),last(s18) -> node4(s17),node4(s18)
% 15.63/3.69  === Conflict found: 260:2:0:[71.1,40.1]:: xuntil2p8(s39) -> until2p7(s40) {}
% 15.63/3.69  === Backtracking. Learning clause 284:3:0:[260.1,70.3]:: until2p7(s39) -> until2p7(s40),node4(s39)
% 15.63/3.69  === Backtracking. Learning clause 285:2:0:[71.1,43.1]:: xuntil2p8(s42) -> until2p7(s43)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 448
% 15.63/3.69  === Backtracking. Learning clause 286:3:1:[65.2,63.1]:Top: node4(x0),last(x0) -> loop
% 15.63/3.69  === Conflict found: 74:3:1:[58.3,60.2,61.1,55.1,51.2]:Top: m_main_v_request(s0),always3(x0),succ(s0,x0) ->  {x0 -> s1}
% 15.63/3.69  === Backtracking. Learning clause 288:3:1:[73.0,287.2,74.1,64.2,62.3,65.2,66.2]:Top: succ(s0,x0),trans(s0,x0) -> xuntil6(s0)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 512
% 15.63/3.69  === Backtracking. Learning clause 289:3:2:[62.1,51.2]:TopTop: always3(x0),succ(x0,x1) -> always3(x1)
% 15.63/3.69  === Conflict found: 289:3:2:[62.1,51.2]:TopTop: always3(x0),succ(x0,x1) -> always3(x1) {x0 -> s0, x1 -> s1}
% 15.63/3.69  === Backtracking. Learning clause 290:1:0:[289.2,1.1,154.2,64.2,65.2,76.1]::  -> xuntil6(s0)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 576
% 15.63/3.69  === Backtracking. Learning clause 291:5:2:[58.3,60.2,64.2,66.2]:TopTop: m_main_v_state(x0,c_ready),trans(x0,x1),until5(x0) -> m_main_v_state(x1,c_busy),xuntil6(x0)
% 15.63/3.69  === Clause set with instances from active satisfied. Growing active. New size: 640
% 15.63/3.69  === Backtracking. Learning clause 292:4:2:[58.3,60.2,64.2]:TopTop: m_main_v_state(x0,c_ready),trans(x0,x1),node4(x0) -> m_main_v_state(x1,c_busy)
% 15.63/3.69  === Backtracking. Learning clause 294:2:2:[60.1,293.0,61.1,58.4,62.3,53.1,61.1,65.2,64.2]:TopTop: trans(x0,x1),node4(x0) -> 
% 15.63/3.69  === Conflict found: 294:2:2:[60.1,293.0,61.1,58.4,62.3,53.1,61.1,65.2,64.2]:TopTop: trans(x0,x1),node4(x0) ->  {x0 -> s7, x1 -> s8}
% 15.63/3.69  === Backtracking. Learning clause 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) -> 
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s7, x1 -> s8}
% 15.63/3.69  === Backtracking. Learning clause 296:1:0:[295.2,8.1]:: node4(s7) -> 
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s1, x1 -> s2}
% 15.63/3.69  === Backtracking. Learning clause 298:1:0:[290.0,297.0,295.2,2.1,168.2]::  -> xuntil6(s1)
% 15.63/3.69  === Backtracking. Learning clause 299:4:2:[62.3,289.1,62.3,51.2,62.3,289.3,51.2,51.2,5.1,3.1,4.1,6.1,7.1,62.3,289.3]:TopTop: trans(x0,s2),always3(x1),succ(x1,x0) -> always3(s7)
% 15.63/3.69  === Backtracking. Learning clause 300:3:1:[62.2,289.3,289.1,51.2,289.3,289.1,5.1,3.1,4.1,6.1,7.1,62.3]:Top: trans(x0,s2),always3(x0) -> always3(s7)
% 15.63/3.69  === Backtracking. Learning clause 306:34:30:[11.0,301.4,31.0,302.9,37.0,303.10,298.0,304.17,295.0,305.37,67.2,66.3,66.1,169.1,186.1,149.1,150.1,67.2,66.1,67.2,67.3,227.3,182.3,181.3,275.3,117.3,148.3,226.3,225.3,116.3,66.3,67.3,216.3,224.3,66.3,67.3,66.3,67.3,66.3,67.3,66.3,66.1,67.2,66.1,228.1,67.2,66.1,249.1,170.1,171.1,191.1,119.1,67.2,66.1,276.1,295.1,193.1,194.1,67.2,66.1,67.2,66.1,120.1,172.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,67.3,203.3,222.3,265.3,295.1,67.2,66.1,67.2,66.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,12.1,15.1,17.1,32.1,34.1,45.1,41.1,42.1,44.1,67.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(x2,s29),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s42,x9),succ(s25,x10),succ(s4,x5),succ(s2,x11),succ(s45,x12),succ(s3,x13),succ(s35,x14),succ(s39,x15),succ(s17,x16),succ(s34,x17),succ(s24,x18),succ(s15,x19),succ(s23,x20),succ(s9,x21),succ(s22,x22),succ(s38,x23),succ(s18,x24),succ(s13,x25),succ(s19,x26),succ(s29,x27),succ(s32,x28),succ(x12,x29) -> until5(x29)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s10, x1 -> s11}
% 15.63/3.69  === Backtracking. Learning clause 307:9:0:[295.2,11.1,216.2,128.1,66.1,116.1,225.1,226.1,148.1,117.1,275.1]:: xuntil6(s9) -> node4(s11),node4(s12),node4(s13),node4(s14),node4(s15),node4(s16),node4(s17),xuntil6(s17)
% 15.63/3.69  === Backtracking. Learning clause 308:2:2:[60.1,51.2]:TopTop: succ(x0,x1) -> node2(x0,x1)
% 15.63/3.69  === Conflict found: 289:3:2:[62.1,51.2]:TopTop: always3(x0),succ(x0,x1) -> always3(x1) {x0 -> s1, x1 -> s2}
% 15.63/3.69  === Backtracking. Learning clause 309:2:0:[289.2,2.1]:: always3(s1) -> always3(s2)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s9, x1 -> s10}
% 15.63/3.69  === Backtracking. Learning clause 310:2:0:[295.2,10.1,224.2]:: xuntil6(s8) -> xuntil6(s9)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s8, x1 -> s9}
% 15.63/3.69  === Backtracking. Learning clause 311:3:0:[295.2,9.1,66.2,310.1,216.1]:: until5(s8) -> node4(s10),xuntil6(s10)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s15, x1 -> s16}
% 15.63/3.69  === Backtracking. Learning clause 312:2:0:[295.2,16.1,148.2]:: xuntil6(s14) -> xuntil6(s15)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s17, x1 -> s18}
% 15.63/3.69  === Backtracking. Learning clause 313:3:0:[295.2,18.1,275.2,117.3,312.2]:: xuntil6(s14) -> xuntil6(s17),node4(s16)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s13, x1 -> s14}
% 15.63/3.69  === Backtracking. Learning clause 314:2:0:[295.2,14.1,225.2]:: xuntil6(s12) -> xuntil6(s13)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s12, x1 -> s13}
% 15.63/3.69  === Backtracking. Learning clause 316:5:0:[11.0,315.0,295.2,13.1,116.2,66.3,67.3,314.1,226.1,216.3,310.2]:: xuntil6(s8) -> node4(s11),node4(s14),xuntil6(s14),node4(s10)
% 15.63/3.69  === Backtracking. Learning clause 321:8:4:[295.0,317.6,295.0,318.7,295.0,319.8,295.0,320.9,66.3,67.2,67.3,203.3,222.3,295.1,66.1,67.2,66.1,67.2,311.1]:TopTopTopTop: succ(x0,x1),succ(s4,x0),xuntil6(s2),succ(s3,x2),succ(x1,x3),succ(x3,s8) -> node4(s10),xuntil6(s10)
% 15.63/3.69  === Backtracking. Learning clause 322:3:2:[66.2,295.1]:TopTop: until5(x0),succ(x0,x1) -> xuntil6(x0)
% 15.63/3.69  === Conflict found: 203:3:0:[66.1,78.2]:: xuntil6(s3) -> node4(s4),xuntil6(s4) {}
% 15.63/3.69  === Backtracking. Learning clause 323:5:3:[203.2,295.1,67.2,322.1,67.2,322.1,67.2]:TopTopTop: xuntil6(s3),succ(s4,x0),succ(x0,x1),succ(x1,x2) -> until5(x2)
% 15.63/3.69  === Conflict found: 307:9:0:[295.2,11.1,216.2,128.1,66.1,116.1,225.1,226.1,148.1,117.1,275.1]:: xuntil6(s9) -> node4(s11),node4(s12),node4(s13),node4(s14),node4(s15),node4(s16),node4(s17),xuntil6(s17) {}
% 15.63/3.69  === Backtracking. Learning clause 324:5:3:[307.5,295.1,295.1,295.1,16.1,295.1,18.1,295.1,14.1,295.1,13.1,295.1,310.2]:TopTopTop: succ(s14,x0),succ(s16,x1),succ(s11,x2),xuntil6(s8) -> xuntil6(s17)
% 15.63/3.69  === Conflict found: 117:3:0:[66.1,81.2]:: xuntil6(s15) -> node4(s16),xuntil6(s16) {}
% 15.63/3.69  === Backtracking. Learning clause 325:6:2:[117.2,295.1,148.3,226.3,295.1,225.3]:TopTop: succ(s16,x0),succ(s14,x1),xuntil6(s12) -> xuntil6(s16),node4(s15),node4(s13)
% 15.63/3.69  === Conflict found: 265:3:0:[66.1,123.2]:: xuntil6(s1) -> node4(s2),xuntil6(s2) {}
% 15.63/3.69  === Backtracking. Learning clause 327:8:5:[298.0,326.0,265.2,295.1,321.3]:TopTopTopTopTop: succ(s2,x0),succ(x1,x2),succ(s4,x1),succ(s3,x3),succ(x2,x4),succ(x4,s8) -> node4(s10),xuntil6(s10)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s16, x1 -> s17}
% 15.63/3.69  === Backtracking. Learning clause 328:1:0:[295.2,17.1]:: node4(s16) -> 
% 15.63/3.69  === Conflict found: 322:3:2:[66.2,295.1]:TopTop: until5(x0),succ(x0,x1) -> xuntil6(x0) {x0 -> s6, x1 -> s7}
% 15.63/3.69  === Backtracking. Learning clause 329:2:0:[322.2,7.1]:: until5(s6) -> xuntil6(s6)
% 15.63/3.69  === Conflict found: 322:3:2:[66.2,295.1]:TopTop: until5(x0),succ(x0,x1) -> xuntil6(x0) {x0 -> s5, x1 -> s6}
% 15.63/3.69  === Backtracking. Learning clause 330:2:0:[322.2,6.1,93.2]:: xuntil6(s4) -> xuntil6(s5)
% 15.63/3.69  === Conflict found: 322:3:2:[66.2,295.1]:TopTop: until5(x0),succ(x0,x1) -> xuntil6(x0) {x0 -> s5, x1 -> s6}
% 15.63/3.69  === Backtracking. Learning clause 331:2:0:[322.2,6.1]:: until5(s5) -> xuntil6(s5)
% 15.63/3.69  === Conflict found: 265:3:0:[66.1,123.2]:: xuntil6(s1) -> node4(s2),xuntil6(s2) {}
% 15.63/3.69  === Backtracking. Learning clause 332:1:0:[265.1,298.1,222.1,323.1,5.1,295.1,3.1,295.1,4.1,7.1,6.1]::  -> until5(s7)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s10, x1 -> s11}
% 15.63/3.69  === Backtracking. Learning clause 333:2:0:[295.2,11.1,216.2,310.2]:: xuntil6(s8) -> xuntil6(s10)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s10, x1 -> s11}
% 15.63/3.69  === Backtracking. Learning clause 334:2:0:[295.2,11.1,216.2]:: xuntil6(s9) -> xuntil6(s10)
% 15.63/3.69  === Backtracking. Learning clause 336:1:0:[332.0,335.0,67.1,8.1,311.1,66.3,296.1,295.1,11.1]::  -> xuntil6(s10)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s14, x1 -> s15}
% 15.63/3.69  === Backtracking. Learning clause 337:2:0:[295.2,15.1,226.2,312.1]:: xuntil6(s13) -> xuntil6(s15)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s14, x1 -> s15}
% 15.63/3.69  === Backtracking. Learning clause 338:1:0:[295.2,15.1]:: node4(s14) -> 
% 15.63/3.69  === Conflict found: 322:3:2:[66.2,295.1]:TopTop: until5(x0),succ(x0,x1) -> xuntil6(x0) {x0 -> s11, x1 -> s12}
% 15.63/3.69  === Backtracking. Learning clause 340:1:0:[336.0,339.0,322.2,12.1,116.1,295.1,13.1,128.2,314.1,337.1]::  -> xuntil6(s15)
% 15.63/3.69  === Conflict found: 322:3:2:[66.2,295.1]:TopTop: until5(x0),succ(x0,x1) -> xuntil6(x0) {x0 -> s11, x1 -> s12}
% 15.63/3.69  === Backtracking. Learning clause 341:2:0:[322.2,12.1]:: until5(s11) -> xuntil6(s11)
% 15.63/3.69  === Backtracking. Learning clause 343:4:1:[50.0,342.1,69.3,66.3,214.1,177.1,294.2,295.1]:Top: trans(s49,s47),until5(s49),succ(s47,x0) -> node4(s48)
% 15.63/3.69  === Backtracking. Learning clause 346:20:18:[29.0,344.4,46.0,345.10,69.3,66.3,177.1,294.2,295.1,50.1,67.3,322.3,67.3,322.3,306.34,21.1,26.1,30.1,38.1,47.1,49.1,19.1,36.1,27.1,22.1,23.1,28.1,24.1,48.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: trans(s49,s48),succ(x0,s8),succ(x1,x0),succ(x2,x1),succ(s12,x3),succ(s8,x4),succ(s42,x5),succ(s4,x2),succ(s2,x6),succ(s3,x7),succ(s39,x8),succ(s17,x9),succ(s34,x10),succ(s24,x11),succ(s15,x12),succ(s9,x13),succ(s38,x14),succ(s13,x15),succ(s19,x16),succ(s32,x17) -> 
% 15.63/3.69  === Backtracking. Learning clause 348:5:0:[50.0,347.0,52.10,294.1,294.1,294.1,294.1,286.3,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,177.3]:: until2p7(s48) -> trans(s49,s7),trans(s49,s47),trans(s49,s48),node4(s48)
% 15.63/3.69  === Backtracking. Learning clause 364:51:0:[68.2,349.0,5.0,350.1,6.0,351.2,9.0,352.3,10.0,353.4,14.0,354.5,15.0,355.6,16.0,356.7,17.0,357.8,20.0,358.9,21.0,359.10,50.0,360.11,296.0,361.47,338.0,362.54,328.0,363.56,69.4,278.1,52.4,69.1,156.1,69.1,70.1,71.2,69.1,70.1,71.2,69.1,269.1,253.1,69.1,70.1,71.2,69.1,70.1,71.2,69.1,207.1,69.1,208.1,69.1,129.1,69.1,70.1,71.2,69.1,70.1,71.2,69.1,70.1,71.2,69.1,70.1,71.2,69.1,279.1,69.1,257.1,69.1,70.1,71.2,69.1,70.1,69.1,231.1,71.2,69.1,70.1,69.1,70.1]:: xuntil6(s49) -> node4(s2),trans(s49,s7),trans(s49,s22),trans(s49,s23),trans(s49,s24),trans(s49,s25),trans(s49,s26),trans(s49,s27),trans(s49,s28),trans(s49,s29),trans(s49,s30),trans(s49,s31),trans(s49,s32),trans(s49,s33),trans(s49,s34),trans(s49,s35),trans(s49,s36),trans(s49,s37),trans(s49,s38),trans(s49,s39),trans(s49,s40),trans(s49,s41),trans(s49,s42),trans(s49,s43),trans(s49,s44),trans(s49,s45),trans(s49,s46),trans(s49,s47),trans(s49,s48),trans(s49,s49),node4(s3),node4(s4),node4(s5),node4(s6),node4(s8),node4(s9),node4(s10),node4(s11),node4(s12),node4(s13),node4(s15),node4(s17),node4(s18),node4(s19),node4(s20),node4(s0),node4(s21),xuntil2p8(s21),node4(s1),xuntil2p8(s1)
% 15.63/3.69  === Backtracking. Learning clause 385:53:16:[20.0,365.8,21.0,366.9,2.0,367.10,22.0,368.11,25.0,369.12,29.0,370.13,32.0,371.14,36.0,372.15,41.0,373.16,45.0,374.17,50.0,375.18,295.0,376.31,295.0,377.32,295.0,378.33,296.0,379.34,295.0,380.35,295.0,381.36,295.0,382.42,295.0,383.45,295.0,384.50,71.3,70.1,70.3,71.3,70.3,129.2,208.2,207.2,71.3,70.3,71.3,70.3,253.2,269.2,71.3,70.3,71.3,70.3,71.2,70.1,71.2,279.1,257.1,70.1,71.2,70.1,71.2,70.1,156.2,278.2,71.3,364.51,71.2,69.1,133.1,69.1,161.1,69.1,70.1,71.2,69.1,151.1,69.1,162.1,69.1,163.1,69.1,70.1,71.2,69.1,258.1,69.1,234.1,69.1,70.1,71.2,69.1,212.1,69.1,122.1,69.1,165.1,69.1,70.1,71.2,69.1,139.1,69.1,259.1,69.1,167.1,69.1,284.1,69.1,70.1,71.2,69.1,153.1,69.1,143.1,69.1,144.1,69.1,70.1,71.2,69.1,152.1,69.1,196.1,69.1,213.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,214.1,295.1,66.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,x1),succ(s13,x0),succ(x2,s10),succ(s8,x2),succ(x3,s6),succ(s4,x3),succ(x1,x4),succ(x4,s17),succ(s46,x5),succ(s23,x6),succ(s25,x7),succ(s29,x8),succ(s27,x9),succ(s18,x10),succ(s22,x11),succ(s37,x12),succ(s26,x13),succ(s32,x14),succ(s47,x15),until5(s49) -> node4(s2),trans(s49,s7),trans(s49,s47),trans(s49,s48),node4(s3),node4(s5),node4(s6),node4(s9),node4(s10),node4(s11),node4(s12),node4(s15),node4(s17),node4(s19),node4(s0),node4(s1),node4(s24),node4(s28),node4(s30),node4(s31),node4(s33),node4(s34),node4(s36),node4(s38),node4(s39),node4(s40),node4(s41),node4(s42),node4(s43),node4(s44),node4(s45),until2p7(s48),node4(s49)
% 15.63/3.69  === Conflict found: 258:3:0:[137.1,70.3]:: until2p7(s29) -> until2p7(s30),node4(s29) {}
% 15.63/3.69  === Backtracking. Learning clause 389:18:1:[29.0,386.0,32.0,387.1,36.0,388.2,258.1,71.3,234.1,70.1,71.2,212.1,122.1,165.1,70.1,71.2,139.1,259.1,70.3,163.2,162.2,167.1,284.1,151.2,71.3]:Top: succ(x0,s25),xuntil2p8(x0) -> node4(s29),node4(s30),node4(s31),node4(s32),node4(s33),node4(s34),node4(s35),node4(s36),node4(s37),node4(s28),node4(s27),node4(s26),node4(s38),until2p7(s40),node4(s39),node4(s25)
% 15.63/3.69  === Backtracking. Learning clause 403:45:20:[45.0,390.0,41.0,391.1,25.0,392.2,295.0,393.43,295.0,394.45,295.0,395.46,295.0,396.47,295.0,397.48,295.0,398.52,295.0,399.53,296.0,400.54,295.0,401.56,295.0,402.57,70.3,71.2,144.2,143.2,153.2,71.3,70.3,389.16,70.3,161.2,133.2,71.3,70.3,196.1,213.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,71.3,70.3,295.1,71.3,70.3,257.2,295.1,279.2,71.3,70.3,71.3,70.3,71.3,70.3,71.3,70.3,129.2,208.2,207.2,71.3,70.3,71.3,70.3,253.2,269.2,71.3,70.3,71.3,70.3,71.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s37,x1),succ(s26,x2),succ(s22,x3),succ(s27,x4),succ(s35,x5),succ(s23,x6),succ(s25,x7),succ(s29,x8),succ(s46,x9),succ(s32,x10),succ(x11,x0),succ(s19,x11),succ(s18,x12),succ(x13,s17),succ(x14,x13),succ(x15,x14),succ(s13,x15),succ(x16,s10),succ(s8,x16),succ(x17,s6),succ(x18,x17),succ(x19,x18),xuntil2p8(x19) -> node4(s44),node4(s43),node4(s42),node4(s41),node4(s40),node4(s30),node4(s31),node4(s33),node4(s34),node4(s36),node4(s28),node4(s38),node4(s39),node4(s24),node4(s45),until2p7(s47),node4(s17),node4(s12),node4(s11),node4(s10),node4(s6)
% 15.63/3.69  === Backtracking. Learning clause 404:34:20:[52.1,286.3,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,385.53,348.1,343.1,50.1,346.1,295.1,67.3,322.3,67.3,322.3,306.34,21.1,26.1,30.1,38.1,47.1,49.1,19.1,36.1,27.1,22.1,23.1,28.1,24.1,48.1,33.1,295.1,35.1,295.1,39.1,295.1,29.1,295.1,37.1,295.1,20.1,295.1,31.1,295.1,46.1,295.1,40.1,295.1,43.1,295.1,25.1,295.1,1.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,32.1,34.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,x1),succ(s13,x0),succ(x2,s10),succ(s8,x2),succ(x3,s6),succ(s4,x3),succ(x1,x4),succ(x4,s17),succ(x5,s8),succ(x6,x5),succ(x7,x6),succ(s12,x8),succ(s4,x7),succ(s2,x9),succ(s3,x10),succ(s17,x11),succ(s15,x12),succ(s9,x13),succ(s6,x14),succ(s40,x15),succ(s41,x16),succ(s44,x17),succ(s5,x18),succ(s43,x19) -> node4(s2),node4(s3),node4(s9),node4(s10),node4(s11),node4(s12),node4(s15),node4(s17),node4(s1),trans(s49,s7)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s48, x1 -> s49}
% 15.63/3.69  === Backtracking. Learning clause 405:2:0:[295.1,177.2,49.1]:: until2p7(s48) -> node4(s49)
% 15.63/3.69  === Backtracking. Learning clause 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0)
% 15.63/3.69  === Conflict found: 269:3:0:[232.1,70.3]:: until2p7(s6) -> until2p7(s7),node4(s6) {}
% 15.63/3.69  === Backtracking. Learning clause 408:5:3:[269.3,295.1,71.3,407.4]:TopTopTop: succ(s6,x0),succ(x1,s6),succ(x2,x1),until2p7(x2) -> until2p7(s7)
% 15.63/3.69  === Backtracking. Learning clause 409:3:2:[70.2,295.1]:TopTop: until2p7(x0),succ(x0,x1) -> xuntil2p8(x0)
% 15.63/3.69  === Conflict found: 306:34:30:[11.0,301.4,31.0,302.9,37.0,303.10,298.0,304.17,295.0,305.37,67.2,66.3,66.1,169.1,186.1,149.1,150.1,67.2,66.1,67.2,67.3,227.3,182.3,181.3,275.3,117.3,148.3,226.3,225.3,116.3,66.3,67.3,216.3,224.3,66.3,67.3,66.3,67.3,66.3,67.3,66.3,66.1,67.2,66.1,228.1,67.2,66.1,249.1,170.1,171.1,191.1,119.1,67.2,66.1,276.1,295.1,193.1,194.1,67.2,66.1,67.2,66.1,120.1,172.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,67.3,203.3,222.3,265.3,295.1,67.2,66.1,67.2,66.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,12.1,15.1,17.1,32.1,34.1,45.1,41.1,42.1,44.1,67.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(x2,s29),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s42,x9),succ(s25,x10),succ(s4,x5),succ(s2,x11),succ(s45,x12),succ(s3,x13),succ(s35,x14),succ(s39,x15),succ(s17,x16),succ(s34,x17),succ(s24,x18),succ(s15,x19),succ(s23,x20),succ(s9,x21),succ(s22,x22),succ(s38,x23),succ(s18,x24),succ(s13,x25),succ(s19,x26),succ(s29,x27),succ(s32,x28),succ(x12,x29) -> until5(x29) {x0 -> s21, x1 -> s27, x2 -> s28, x3 -> s7, x4 -> s6, x5 -> s5, x6 -> s13, x7 -> s9, x8 -> s38, x9 -> s43, x10 -> s26, x11 -> s3, x12 -> s46, x13 -> s4, x14 -> s36, x15 -> s40, x16 -> s18, x17 -> s35, x18 -> s25, x19 -> s16, x20 -> s24, x21 -> s10, x22 -> s23, x23 -> s39, x24 -> s19, x25 -> s14, x26 -> s20, x27 -> s30, x28 -> s33, x29 -> s47}
% 15.63/3.69  === Backtracking. Learning clause 413:28:23:[47.0,410.23,295.0,411.28,294.1,412.29,306.32,33.1,35.1,39.1,29.1,20.1,46.1,40.1,43.1,25.1,322.1,277.1,67.2,66.1,69.3]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,s28),succ(s20,x0),succ(x2,s8),succ(x3,x2),succ(x4,x3),succ(s12,x5),succ(s8,x6),succ(s37,x7),succ(s25,x8),succ(s4,x4),succ(s2,x9),succ(s3,x10),succ(s35,x11),succ(s17,x12),succ(s15,x13),succ(s23,x14),succ(s9,x15),succ(s22,x16),succ(s18,x17),succ(s13,x18),succ(s29,x19),succ(s47,x20),succ(s48,x21),trans(x21,x22),last(x21) -> until2p7(x22)
% 15.63/3.69  === Conflict found: 214:3:0:[198.1,70.3]:: until2p7(s47) -> until2p7(s48),node4(s47) {}
% 15.63/3.69  === Backtracking. Learning clause 414:29:22:[214.3,295.1,213.2,413.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,s28),succ(s20,x0),succ(x2,s8),succ(x3,x2),succ(x4,x3),succ(s12,x5),succ(s8,x6),succ(s37,x7),succ(s25,x8),succ(s4,x4),succ(s2,x9),succ(s3,x10),succ(s35,x11),succ(s17,x12),succ(s15,x13),succ(s23,x14),succ(s9,x15),succ(s22,x16),succ(s18,x17),succ(s13,x18),succ(s29,x19),succ(s47,x20),succ(s48,x21),trans(x21,s46),last(x21) -> until2p7(s48),node4(s46)
% 15.63/3.69  === Conflict found: 284:3:0:[260.1,70.3]:: until2p7(s39) -> until2p7(s40),node4(s39) {}
% 15.63/3.69  === Backtracking. Learning clause 415:29:23:[284.3,295.1,413.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(s39,x0),succ(x1,s22),succ(s26,x2),succ(x2,s28),succ(s20,x1),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s25,x9),succ(s4,x5),succ(s2,x10),succ(s3,x11),succ(s35,x12),succ(s17,x13),succ(s15,x14),succ(s23,x15),succ(s9,x16),succ(s22,x17),succ(s18,x18),succ(s13,x19),succ(s29,x20),succ(s47,x21),succ(s48,x22),trans(x22,s39),last(x22) -> until2p7(s40)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s36, x1 -> s37}
% 15.63/3.69  === Backtracking. Learning clause 416:31:23:[295.2,37.1,139.3,71.3,407.4,122.2,413.28]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s36),succ(s34,x0),succ(x1,s22),succ(s26,x2),succ(x2,s28),succ(s20,x1),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s25,x9),succ(s4,x5),succ(s2,x10),succ(s3,x11),succ(s35,x12),succ(s17,x13),succ(s15,x14),succ(s23,x15),succ(s9,x16),succ(s22,x17),succ(s18,x18),succ(s13,x19),succ(s29,x20),succ(s47,x21),succ(s48,x22),trans(x22,s33),last(x22) -> until2p7(s37),node4(s33)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s31, x1 -> s32, x2 -> s30}
% 15.63/3.69  === Backtracking. Learning clause 417:8:3:[407.2,31.1,71.2,212.1,122.1,407.3,71.2,139.1,295.1,37.1,295.1,259.1,167.1,295.1,32.1,34.1,284.1,295.1]:TopTopTop: until2p7(s30),succ(s34,x0),succ(x0,s36),succ(s38,x1),succ(s39,x2) -> node4(s32),node4(s37),until2p7(s40)
% 15.63/3.69  === Conflict found: 196:3:0:[71.1,46.1,70.3]:: until2p7(s45) -> until2p7(s46),node4(s45) {}
% 15.63/3.69  === Backtracking. Learning clause 424:27:11:[41.0,418.3,36.0,419.4,28.0,420.5,24.0,421.6,19.0,422.9,296.0,423.30,196.3,295.1,71.3,407.4,143.2,153.2,295.1,295.1,71.3,409.3,417.8,258.2,71.3,407.4,162.2,151.2,71.3,407.4,133.2,71.3,407.4,295.1,33.1,35.1,39.1,29.1,71.3,407.4,20.1,46.1,40.1,43.1,25.1,279.2,71.3,407.4,71.3,407.4,129.2,208.2,207.2,71.3,407.4,253.2,408.5,213.1,214.1,295.1]:TopTopTopTopTopTopTopTopTopTopTop: succ(x0,s45),succ(s43,x0),succ(s41,x1),succ(x2,s22),succ(s20,x2),succ(x3,s17),succ(x4,x3),succ(x5,x4),succ(s13,x5),succ(x6,s10),succ(s8,x6),succ(s6,x7),succ(x8,s6),succ(x9,x8),until2p7(x9),succ(s47,x10) -> node4(s37),node4(s29),node4(s26),node4(s25),node4(s22),node4(s17),node4(s12),node4(s11),node4(s10),node4(s46),until2p7(s48)
% 15.63/3.69  === Conflict found: 167:3:0:[71.1,39.1,70.3]:: until2p7(s38) -> until2p7(s39),node4(s38) {}
% 15.63/3.69  === Backtracking. Learning clause 425:7:3:[167.3,295.1,259.2,139.2,71.3,407.4]:TopTopTop: succ(s38,x0),succ(x1,s36),succ(x2,x1),until2p7(x2) -> until2p7(s39),node4(s37),node4(s36)
% 15.63/3.69  === Conflict found: 167:3:0:[71.1,39.1,70.3]:: until2p7(s38) -> until2p7(s39),node4(s38) {}
% 15.63/3.69  === Backtracking. Learning clause 426:6:2:[167.3,295.1,259.2,139.2,71.3]:TopTop: succ(s38,x0),succ(x1,s36),xuntil2p8(x1) -> until2p7(s39),node4(s37),node4(s36)
% 15.63/3.69  === Conflict found: 167:3:0:[71.1,39.1,70.3]:: until2p7(s38) -> until2p7(s39),node4(s38) {}
% 15.63/3.69  === Backtracking. Learning clause 427:5:1:[167.3,295.1,259.2,139.2]:Top: succ(s38,x0),until2p7(s36) -> until2p7(s39),node4(s37),node4(s36)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s35, x1 -> s36, x2 -> s34}
% 15.63/3.69  === Backtracking. Learning clause 428:3:1:[407.2,35.1]:Top: succ(s35,x0),until2p7(s34) -> xuntil2p8(s35)
% 15.63/3.69  === Conflict found: 269:3:0:[232.1,70.3]:: until2p7(s6) -> until2p7(s7),node4(s6) {}
% 15.63/3.69  === Backtracking. Learning clause 430:4:2:[295.0,429.4,269.3,295.1,71.3,70.3]:TopTop: succ(s6,x0),succ(x1,s6),until2p7(x1) -> until2p7(s7)
% 15.63/3.69  === Backtracking. Learning clause 431:3:1:[69.2,50.1]:Top: trans(s49,x0),xuntil6(s49) -> until2p7(x0)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s33, x1 -> s34}
% 15.63/3.69  === Backtracking. Learning clause 432:3:0:[295.1,122.3,34.1,431.3]:: trans(s49,s33),xuntil6(s49) -> until2p7(s34)
% 15.63/3.69  === Conflict found: 431:3:1:[69.2,50.1]:Top: trans(s49,x0),xuntil6(s49) -> until2p7(x0) {x0 -> s7}
% 15.63/3.69  === Backtracking. Learning clause 451:39:26:[49.0,433.8,47.0,434.25,19.0,435.32,24.0,436.35,28.0,437.36,36.0,438.37,295.0,439.38,295.0,440.39,295.0,441.40,295.0,442.41,296.0,443.46,295.0,444.49,295.0,445.50,295.0,446.51,295.0,447.52,295.0,448.53,295.0,449.54,295.0,450.55,431.1,404.34,66.3,67.3,277.3,66.3,306.34,253.1,407.3,71.2,207.1,208.1,129.1,407.3,71.2,407.3,71.2,279.1,407.3,71.2,407.3,71.2,133.1,407.3,71.2,151.1,162.1,407.3,71.2,258.1,417.1,295.1,33.1,35.1,39.1,29.1,20.1,46.1,40.1,43.1,25.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s6),succ(s4,x0),succ(s6,x1),succ(s40,x2),succ(s41,x3),succ(s44,x4),succ(s5,x5),succ(s43,x6),succ(s26,x7),succ(x7,s28),succ(x8,s8),succ(x9,x8),succ(x10,x9),succ(s12,x11),succ(s37,x12),succ(s25,x13),succ(s4,x10),succ(s2,x14),succ(s3,x15),succ(s17,x16),succ(s15,x17),succ(s9,x18),succ(s22,x19),succ(s29,x20),succ(s8,x21),succ(x21,s10),succ(s13,x22),succ(x22,x23),succ(x23,x24),succ(x24,s17),succ(s20,x25),succ(x25,s22) -> node4(s1),node4(s49),node4(s48),node4(s47),node4(s10),node4(s11),until2p7(s40)
% 15.63/3.69  === Conflict found: 143:3:0:[71.1,43.1,70.3]:: until2p7(s42) -> until2p7(s43),node4(s42) {}
% 15.63/3.69  === Backtracking. Learning clause 453:28:19:[41.0,452.2,143.3,295.1,407.3,71.2,196.1,295.1,153.2,295.1,71.3,409.3,213.1,214.1,46.1,43.1,451.39,295.1,21.1,26.1,30.1,38.1,295.1,47.1,27.1,22.1,23.1,28.1,48.1,295.1,49.1,405.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(s43,x0),succ(x0,s45),succ(x1,s6),succ(s4,x1),succ(s6,x2),succ(s41,x3),succ(s44,x4),succ(s5,x5),succ(x6,s8),succ(x7,x6),succ(x8,x7),succ(s12,x9),succ(s4,x8),succ(s2,x10),succ(s3,x11),succ(s17,x12),succ(s15,x13),succ(s9,x14),succ(s8,x15),succ(x15,s10),succ(s13,x16),succ(x16,x17),succ(x17,x18),succ(x18,s17) -> node4(s1),node4(s10),node4(s11),node4(s49)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s47, x1 -> s48}
% 15.63/3.69  === Backtracking. Learning clause 454:1:0:[295.2,48.1]:: node4(s47) -> 
% 15.63/3.69  === Conflict found: 284:3:0:[260.1,70.3]:: until2p7(s39) -> until2p7(s40),node4(s39) {}
% 15.63/3.69  === Backtracking. Learning clause 455:4:1:[284.3,295.1,167.2]:Top: succ(s39,x0),until2p7(s38) -> until2p7(s40),node4(s38)
% 15.63/3.69  === Conflict found: 258:3:0:[137.1,70.3]:: until2p7(s29) -> until2p7(s30),node4(s29) {}
% 15.63/3.69  === Backtracking. Learning clause 456:3:1:[258.3,295.1]:Top: until2p7(s29),succ(s29,x0) -> until2p7(s30)
% 15.63/3.69  === Conflict found: 151:3:0:[135.1,70.3]:: until2p7(s25) -> until2p7(s26),node4(s25) {}
% 15.63/3.69  === Backtracking. Learning clause 457:3:1:[151.3,295.1]:Top: until2p7(s25),succ(s25,x0) -> until2p7(s26)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s37, x1 -> s38}
% 15.63/3.69  === Backtracking. Learning clause 458:2:0:[295.1,259.3,38.1]:: until2p7(s37) -> until2p7(s38)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s36, x1 -> s37}
% 15.63/3.69  === Backtracking. Learning clause 459:2:0:[295.2,37.1,139.3,458.1,455.2,295.1,39.1,40.1]:: until2p7(s36) -> until2p7(s40)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s38, x1 -> s39}
% 15.63/3.69  === Backtracking. Learning clause 460:2:0:[295.2,39.1,455.4,40.1,458.2]:: until2p7(s37) -> until2p7(s40)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s38, x1 -> s39}
% 15.63/3.69  === Backtracking. Learning clause 461:2:0:[295.2,39.1,455.4,40.1]:: until2p7(s38) -> until2p7(s40)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s38, x1 -> s39}
% 15.63/3.69  === Backtracking. Learning clause 462:1:0:[295.2,39.1]:: node4(s38) -> 
% 15.63/3.69  === Conflict found: 456:3:1:[258.3,295.1]:Top: until2p7(s29),succ(s29,x0) -> until2p7(s30) {x0 -> s30}
% 15.63/3.69  === Backtracking. Learning clause 463:2:0:[456.2,30.1]:: until2p7(s29) -> until2p7(s30)
% 15.63/3.69  === Conflict found: 457:3:1:[151.3,295.1]:Top: until2p7(s25),succ(s25,x0) -> until2p7(s26) {x0 -> s26}
% 15.63/3.69  === Backtracking. Learning clause 464:3:1:[457.2,26.1,71.3]:Top: succ(x0,s25),xuntil2p8(x0) -> until2p7(s26)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s24, x1 -> s25, x2 -> s23}
% 15.63/3.69  === Backtracking. Learning clause 465:3:1:[407.2,24.1]:Top: succ(s24,x0),until2p7(s23) -> xuntil2p8(s24)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s22, x1 -> s23}
% 15.63/3.69  === Backtracking. Learning clause 466:2:0:[295.1,133.3,23.1]:: until2p7(s22) -> until2p7(s23)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s21, x1 -> s22, x2 -> s20}
% 15.63/3.69  === Backtracking. Learning clause 467:3:1:[407.1,22.1,21.1,71.3]:Top: succ(x0,s20),xuntil2p8(x0) -> xuntil2p8(s21)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s19, x1 -> s20, x2 -> s18}
% 15.63/3.69  === Backtracking. Learning clause 468:3:1:[407.2,19.1]:Top: succ(s19,x0),until2p7(s18) -> xuntil2p8(s19)
% 15.63/3.69  === Conflict found: 409:3:2:[70.2,295.1]:TopTop: until2p7(x0),succ(x0,x1) -> xuntil2p8(x0) {x0 -> s5, x1 -> s6}
% 15.63/3.69  === Backtracking. Learning clause 469:2:0:[409.2,6.1,125.1]:: until2p7(s5) -> until2p7(s6)
% 15.63/3.69  === Conflict found: 409:3:2:[70.2,295.1]:TopTop: until2p7(x0),succ(x0,x1) -> xuntil2p8(x0) {x0 -> s5, x1 -> s6}
% 15.63/3.69  === Backtracking. Learning clause 470:2:0:[409.2,6.1]:: until2p7(s5) -> xuntil2p8(s5)
% 15.63/3.69  === Conflict found: 430:4:2:[295.0,429.4,269.3,295.1,71.3,70.3]:TopTop: succ(s6,x0),succ(x1,s6),until2p7(x1) -> until2p7(s7) {x0 -> s7, x1 -> s5}
% 15.63/3.69  === Backtracking. Learning clause 471:3:1:[430.1,7.1]:Top: succ(x0,s6),until2p7(x0) -> until2p7(s7)
% 15.63/3.69  === Conflict found: 409:3:2:[70.2,295.1]:TopTop: until2p7(x0),succ(x0,x1) -> xuntil2p8(x0) {x0 -> s4, x1 -> s5}
% 15.63/3.69  === Backtracking. Learning clause 472:2:0:[409.2,5.1]:: until2p7(s4) -> xuntil2p8(s4)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s11, x1 -> s12}
% 15.63/3.69  === Backtracking. Learning clause 473:2:0:[295.1,208.3,12.1]:: until2p7(s11) -> until2p7(s12)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s10, x1 -> s11}
% 15.63/3.69  === Backtracking. Learning clause 474:2:0:[295.2,11.1,207.3,127.2]:: xuntil2p8(s9) -> until2p7(s11)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s10, x1 -> s11}
% 15.63/3.69  === Backtracking. Learning clause 475:2:0:[295.2,11.1,207.3]:: until2p7(s10) -> until2p7(s11)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s17, x1 -> s18}
% 15.63/3.69  === Backtracking. Learning clause 476:2:0:[295.2,18.1,279.3]:: until2p7(s17) -> until2p7(s18)
% 15.63/3.69  === Backtracking. Learning clause 477:2:0:[71.1,5.1,472.2]:: until2p7(s4) -> until2p7(s5)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s12, x1 -> s13}
% 15.63/3.69  === Backtracking. Learning clause 478:2:0:[295.2,13.1,129.3]:: until2p7(s12) -> until2p7(s13)
% 15.63/3.69  === Conflict found: 471:3:1:[430.1,7.1]:Top: succ(x0,s6),until2p7(x0) -> until2p7(s7) {x0 -> s5}
% 15.63/3.69  === Backtracking. Learning clause 479:2:0:[471.1,6.1]:: until2p7(s5) -> until2p7(s7)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s14, x1 -> s15, x2 -> s13}
% 15.63/3.69  === Backtracking. Learning clause 480:2:0:[407.2,14.1,15.1,98.1]:: until2p7(s13) -> until2p7(s15)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s14, x1 -> s15, x2 -> s13}
% 15.63/3.69  === Backtracking. Learning clause 481:2:0:[407.2,14.1,15.1]:: until2p7(s13) -> xuntil2p8(s14)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s15, x1 -> s16, x2 -> s14}
% 15.63/3.69  === Backtracking. Learning clause 482:2:0:[407.1,16.1,159.1,70.1,328.1,71.3,409.3,99.1,14.1,15.1,478.2,473.2,475.2]:: until2p7(s10) -> until2p7(s17)
% 15.63/3.69  === Conflict found: 407:4:3:[295.0,406.4,70.2,295.1,71.3,70.3]:TopTopTop: succ(x0,x1),succ(x2,x0),until2p7(x2) -> xuntil2p8(x0) {x0 -> s9, x1 -> s10, x2 -> s8}
% 15.63/3.69  === Backtracking. Learning clause 483:2:0:[407.2,9.1,10.1]:: until2p7(s8) -> xuntil2p8(s9)
% 15.63/3.69  === Conflict found: 306:34:30:[11.0,301.4,31.0,302.9,37.0,303.10,298.0,304.17,295.0,305.37,67.2,66.3,66.1,169.1,186.1,149.1,150.1,67.2,66.1,67.2,67.3,227.3,182.3,181.3,275.3,117.3,148.3,226.3,225.3,116.3,66.3,67.3,216.3,224.3,66.3,67.3,66.3,67.3,66.3,67.3,66.3,66.1,67.2,66.1,228.1,67.2,66.1,249.1,170.1,171.1,191.1,119.1,67.2,66.1,276.1,295.1,193.1,194.1,67.2,66.1,67.2,66.1,120.1,172.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,67.3,203.3,222.3,265.3,295.1,67.2,66.1,67.2,66.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,12.1,15.1,17.1,32.1,34.1,45.1,41.1,42.1,44.1,67.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(x2,s29),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s42,x9),succ(s25,x10),succ(s4,x5),succ(s2,x11),succ(s45,x12),succ(s3,x13),succ(s35,x14),succ(s39,x15),succ(s17,x16),succ(s34,x17),succ(s24,x18),succ(s15,x19),succ(s23,x20),succ(s9,x21),succ(s22,x22),succ(s38,x23),succ(s18,x24),succ(s13,x25),succ(s19,x26),succ(s29,x27),succ(s32,x28),succ(x12,x29) -> until5(x29) {x0 -> s21, x1 -> s27, x2 -> s28, x3 -> s7, x4 -> s6, x5 -> s5, x6 -> s13, x7 -> s9, x8 -> s38, x9 -> s43, x10 -> s26, x11 -> s3, x12 -> s46, x13 -> s4, x14 -> s36, x15 -> s40, x16 -> s18, x17 -> s35, x18 -> s25, x19 -> s16, x20 -> s24, x21 -> s10, x22 -> s23, x23 -> s39, x24 -> s19, x25 -> s14, x26 -> s20, x27 -> s30, x28 -> s33, x29 -> s47}
% 15.63/3.69  === Backtracking. Learning clause 484:35:28:[306.17,4.1,8.1,3.1,322.1,277.1,67.2,66.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s7),succ(x4,x3),succ(x2,s29),succ(s12,x5),succ(s8,x6),succ(s37,x7),succ(s42,x8),succ(s25,x9),succ(s4,x4),succ(s45,x10),succ(s35,x11),succ(s39,x12),succ(s17,x13),succ(s34,x14),succ(s24,x15),succ(s15,x16),succ(s23,x17),succ(s9,x18),succ(s22,x19),succ(s38,x20),succ(s18,x21),succ(s13,x22),succ(s19,x23),succ(s29,x24),succ(s32,x25),succ(x10,s47),succ(s47,x26),succ(s48,x27) -> node4(s48),node4(x27),xuntil6(x27)
% 15.63/3.69  === Conflict found: 234:3:0:[71.1,31.1,70.3]:: until2p7(s30) -> until2p7(s31),node4(s30) {}
% 15.63/3.69  === Backtracking. Learning clause 485:3:1:[234.3,295.1]:Top: until2p7(s30),succ(s30,x0) -> until2p7(s31)
% 15.63/3.69  === Conflict found: 306:34:30:[11.0,301.4,31.0,302.9,37.0,303.10,298.0,304.17,295.0,305.37,67.2,66.3,66.1,169.1,186.1,149.1,150.1,67.2,66.1,67.2,67.3,227.3,182.3,181.3,275.3,117.3,148.3,226.3,225.3,116.3,66.3,67.3,216.3,224.3,66.3,67.3,66.3,67.3,66.3,67.3,66.3,66.1,67.2,66.1,228.1,67.2,66.1,249.1,170.1,171.1,191.1,119.1,67.2,66.1,276.1,295.1,193.1,194.1,67.2,66.1,67.2,66.1,120.1,172.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,67.3,203.3,222.3,265.3,295.1,67.2,66.1,67.2,66.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,12.1,15.1,17.1,32.1,34.1,45.1,41.1,42.1,44.1,67.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(x2,s29),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s42,x9),succ(s25,x10),succ(s4,x5),succ(s2,x11),succ(s45,x12),succ(s3,x13),succ(s35,x14),succ(s39,x15),succ(s17,x16),succ(s34,x17),succ(s24,x18),succ(s15,x19),succ(s23,x20),succ(s9,x21),succ(s22,x22),succ(s38,x23),succ(s18,x24),succ(s13,x25),succ(s19,x26),succ(s29,x27),succ(s32,x28),succ(x12,x29) -> until5(x29) {x0 -> s21, x1 -> s27, x2 -> s28, x3 -> s7, x4 -> s6, x5 -> s5, x6 -> s13, x7 -> s9, x8 -> s38, x9 -> s43, x10 -> s26, x11 -> s3, x12 -> s46, x13 -> s4, x14 -> s36, x15 -> s40, x16 -> s18, x17 -> s35, x18 -> s25, x19 -> s16, x20 -> s24, x21 -> s10, x22 -> s23, x23 -> s39, x24 -> s19, x25 -> s14, x26 -> s20, x27 -> s30, x28 -> s33, x29 -> s47}
% 15.63/3.69  === Backtracking. Learning clause 486:37:30:[306.18,36.1,322.1,277.1,67.2,66.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(x2,s29),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s42,x9),succ(s25,x10),succ(s4,x5),succ(s2,x11),succ(s45,x12),succ(s3,x13),succ(s39,x14),succ(s17,x15),succ(s34,x16),succ(s24,x17),succ(s15,x18),succ(s23,x19),succ(s9,x20),succ(s22,x21),succ(s38,x22),succ(s18,x23),succ(s13,x24),succ(s19,x25),succ(s29,x26),succ(s32,x27),succ(x12,s47),succ(s47,x28),succ(s48,x29) -> node4(s48),node4(x29),xuntil6(x29)
% 15.63/3.69  === Conflict found: 306:34:30:[11.0,301.4,31.0,302.9,37.0,303.10,298.0,304.17,295.0,305.37,67.2,66.3,66.1,169.1,186.1,149.1,150.1,67.2,66.1,67.2,67.3,227.3,182.3,181.3,275.3,117.3,148.3,226.3,225.3,116.3,66.3,67.3,216.3,224.3,66.3,67.3,66.3,67.3,66.3,67.3,66.3,66.1,67.2,66.1,228.1,67.2,66.1,249.1,170.1,171.1,191.1,119.1,67.2,66.1,276.1,295.1,193.1,194.1,67.2,66.1,67.2,66.1,120.1,172.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,67.3,203.3,222.3,265.3,295.1,67.2,66.1,67.2,66.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,12.1,15.1,17.1,32.1,34.1,45.1,41.1,42.1,44.1,67.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(x2,s29),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s42,x9),succ(s25,x10),succ(s4,x5),succ(s2,x11),succ(s45,x12),succ(s3,x13),succ(s35,x14),succ(s39,x15),succ(s17,x16),succ(s34,x17),succ(s24,x18),succ(s15,x19),succ(s23,x20),succ(s9,x21),succ(s22,x22),succ(s38,x23),succ(s18,x24),succ(s13,x25),succ(s19,x26),succ(s29,x27),succ(s32,x28),succ(x12,x29) -> until5(x29) {x0 -> s21, x1 -> s27, x2 -> s28, x3 -> s7, x4 -> s6, x5 -> s5, x6 -> s13, x7 -> s9, x8 -> s38, x9 -> s43, x10 -> s26, x11 -> s3, x12 -> s46, x13 -> s4, x14 -> s36, x15 -> s40, x16 -> s18, x17 -> s35, x18 -> s25, x19 -> s16, x20 -> s24, x21 -> s10, x22 -> s23, x23 -> s39, x24 -> s19, x25 -> s14, x26 -> s20, x27 -> s30, x28 -> s33, x29 -> s47}
% 15.63/3.69  === Backtracking. Learning clause 487:33:29:[306.18,36.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(x2,s29),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s42,x9),succ(s25,x10),succ(s4,x5),succ(s2,x11),succ(s45,x12),succ(s3,x13),succ(s39,x14),succ(s17,x15),succ(s34,x16),succ(s24,x17),succ(s15,x18),succ(s23,x19),succ(s9,x20),succ(s22,x21),succ(s38,x22),succ(s18,x23),succ(s13,x24),succ(s19,x25),succ(s29,x26),succ(s32,x27),succ(x12,x28) -> until5(x28)
% 15.63/3.69  === Backtracking. Learning clause 489:5:1:[328.0,488.5,69.1,51.2,181.3,313.2]:Top: last(s18),succ(s18,x0),xuntil6(s14) -> until2p7(x0),node4(s18)
% 15.63/3.69  === Conflict found: 404:34:20:[52.1,286.3,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,385.53,348.1,343.1,50.1,346.1,295.1,67.3,322.3,67.3,322.3,306.34,21.1,26.1,30.1,38.1,47.1,49.1,19.1,36.1,27.1,22.1,23.1,28.1,24.1,48.1,33.1,295.1,35.1,295.1,39.1,295.1,29.1,295.1,37.1,295.1,20.1,295.1,31.1,295.1,46.1,295.1,40.1,295.1,43.1,295.1,25.1,295.1,1.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,32.1,34.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,x1),succ(s13,x0),succ(x2,s10),succ(s8,x2),succ(x3,s6),succ(s4,x3),succ(x1,x4),succ(x4,s17),succ(x5,s8),succ(x6,x5),succ(x7,x6),succ(s12,x8),succ(s4,x7),succ(s2,x9),succ(s3,x10),succ(s17,x11),succ(s15,x12),succ(s9,x13),succ(s6,x14),succ(s40,x15),succ(s41,x16),succ(s44,x17),succ(s5,x18),succ(s43,x19) -> node4(s2),node4(s3),node4(s9),node4(s10),node4(s11),node4(s12),node4(s15),node4(s17),node4(s1),trans(s49,s7) {x0 -> s14, x1 -> s15, x2 -> s9, x3 -> s5, x4 -> s16, x5 -> s7, x6 -> s6, x7 -> s5, x8 -> s13, x9 -> s3, x10 -> s4, x11 -> s18, x12 -> s16, x13 -> s10, x14 -> s7, x15 -> s41, x16 -> s42, x17 -> s45, x18 -> s6, x19 -> s44}
% 15.63/3.69  === Backtracking. Learning clause 493:13:10:[6.0,490.2,29.0,491.3,46.0,492.6,404.24,44.1,41.1,42.1,45.1,295.1,295.1,2.1,17.1,295.1,295.1,295.1,431.1,486.37,3.1,8.1,4.1,24.1,295.1,19.1,7.1,295.1,18.1,12.1,47.1,27.1,28.1,295.1,13.1,16.1,10.1,9.1,30.1,26.1,295.1,49.1,23.1,22.1,21.1,5.1,295.1,11.1]:TopTopTopTopTopTopTopTopTopTop: succ(x0,s15),succ(s13,x0),succ(s37,x1),succ(s42,x2),succ(s39,x3),succ(s34,x4),succ(s24,x5),succ(s38,x6),succ(s19,x7),succ(s32,x8),succ(s47,x9) -> until2p7(s7),node4(s49)
% 15.63/3.69  === Conflict found: 306:34:30:[11.0,301.4,31.0,302.9,37.0,303.10,298.0,304.17,295.0,305.37,67.2,66.3,66.1,169.1,186.1,149.1,150.1,67.2,66.1,67.2,67.3,227.3,182.3,181.3,275.3,117.3,148.3,226.3,225.3,116.3,66.3,67.3,216.3,224.3,66.3,67.3,66.3,67.3,66.3,67.3,66.3,66.1,67.2,66.1,228.1,67.2,66.1,249.1,170.1,171.1,191.1,119.1,67.2,66.1,276.1,295.1,193.1,194.1,67.2,66.1,67.2,66.1,120.1,172.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,67.3,203.3,222.3,265.3,295.1,67.2,66.1,67.2,66.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,12.1,15.1,17.1,32.1,34.1,45.1,41.1,42.1,44.1,67.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,s22),succ(s26,x1),succ(x1,x2),succ(s20,x0),succ(x3,s8),succ(x4,x3),succ(x5,x4),succ(x2,s29),succ(s12,x6),succ(s8,x7),succ(s37,x8),succ(s42,x9),succ(s25,x10),succ(s4,x5),succ(s2,x11),succ(s45,x12),succ(s3,x13),succ(s35,x14),succ(s39,x15),succ(s17,x16),succ(s34,x17),succ(s24,x18),succ(s15,x19),succ(s23,x20),succ(s9,x21),succ(s22,x22),succ(s38,x23),succ(s18,x24),succ(s13,x25),succ(s19,x26),succ(s29,x27),succ(s32,x28),succ(x12,x29) -> until5(x29) {x0 -> s21, x1 -> s27, x2 -> s28, x3 -> s7, x4 -> s6, x5 -> s5, x6 -> s13, x7 -> s9, x8 -> s38, x9 -> s43, x10 -> s26, x11 -> s3, x12 -> s46, x13 -> s4, x14 -> s36, x15 -> s40, x16 -> s18, x17 -> s35, x18 -> s25, x19 -> s16, x20 -> s24, x21 -> s10, x22 -> s23, x23 -> s39, x24 -> s19, x25 -> s14, x26 -> s20, x27 -> s30, x28 -> s33, x29 -> s47}
% 15.63/3.69  === Backtracking. Learning clause 496:10:9:[29.0,494.0,46.0,495.3,306.7,6.1,24.1,7.1,19.1,18.1,47.1,13.1,28.1,27.1,9.1,10.1,16.1,30.1,26.1,23.1,8.1,3.1,22.1,21.1,4.1,5.1,36.1]:TopTopTopTopTopTopTopTopTop: succ(s37,x0),succ(s42,x1),succ(s39,x2),succ(s34,x3),succ(s24,x4),succ(s38,x5),succ(s13,x6),succ(s19,x7),succ(s32,x8) -> until5(s47)
% 15.63/3.69  === Conflict found: 295:2:2:[294.1,51.2]:TopTop: node4(x0),succ(x0,x1) ->  {x0 -> s48, x1 -> s49}
% 15.63/3.69  === Backtracking. Learning clause 497:3:0:[295.2,49.1,277.2,147.1,66.1]:: xuntil6(s47) -> node4(s49),xuntil6(s49)
% 15.63/3.69  === Conflict found: 453:28:19:[41.0,452.2,143.3,295.1,407.3,71.2,196.1,295.1,153.2,295.1,71.3,409.3,213.1,214.1,46.1,43.1,451.39,295.1,21.1,26.1,30.1,38.1,295.1,47.1,27.1,22.1,23.1,28.1,48.1,295.1,49.1,405.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(s43,x0),succ(x0,s45),succ(x1,s6),succ(s4,x1),succ(s6,x2),succ(s41,x3),succ(s44,x4),succ(s5,x5),succ(x6,s8),succ(x7,x6),succ(x8,x7),succ(s12,x9),succ(s4,x8),succ(s2,x10),succ(s3,x11),succ(s17,x12),succ(s15,x13),succ(s9,x14),succ(s8,x15),succ(x15,s10),succ(s13,x16),succ(x16,x17),succ(x17,x18),succ(x18,s17) -> node4(s1),node4(s10),node4(s11),node4(s49) {x0 -> s44, x1 -> s5, x2 -> s7, x3 -> s42, x4 -> s45, x5 -> s6, x6 -> s7, x7 -> s6, x8 -> s5, x9 -> s13, x10 -> s3, x11 -> s4, x12 -> s18, x13 -> s16, x14 -> s10, x15 -> s9, x16 -> s14, x17 -> s15, x18 -> s16}
% 15.63/3.69  === Backtracking. Learning clause 498:1:1:[453.6,42.1,45.1,44.1,295.1,2.1,17.1,295.1,12.1,295.1,11.1,6.1,7.1,18.1,13.1,16.1,10.1,9.1,4.1,8.1,3.1,5.1,14.1,15.1,294.2]:Top: trans(s49,x0) -> 
% 15.63/3.69  === Conflict found: 404:34:20:[52.1,286.3,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,294.1,385.53,348.1,343.1,50.1,346.1,295.1,67.3,322.3,67.3,322.3,306.34,21.1,26.1,30.1,38.1,47.1,49.1,19.1,36.1,27.1,22.1,23.1,28.1,24.1,48.1,33.1,295.1,35.1,295.1,39.1,295.1,29.1,295.1,37.1,295.1,20.1,295.1,31.1,295.1,46.1,295.1,40.1,295.1,43.1,295.1,25.1,295.1,1.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,295.1,32.1,34.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: succ(x0,x1),succ(s13,x0),succ(x2,s10),succ(s8,x2),succ(x3,s6),succ(s4,x3),succ(x1,x4),succ(x4,s17),succ(x5,s8),succ(x6,x5),succ(x7,x6),succ(s12,x8),succ(s4,x7),succ(s2,x9),succ(s3,x10),succ(s17,x11),succ(s15,x12),succ(s9,x13),succ(s6,x14),succ(s40,x15),succ(s41,x16),succ(s44,x17),succ(s5,x18),succ(s43,x19) -> node4(s2),node4(s3),node4(s9),node4(s10),node4(s11),node4(s12),node4(s15),node4(s17),node4(s1),trans(s49,s7) {x0 -> s14, x1 -> s15, x2 -> s9, x3 -> s5, x4 -> s16, x5 -> s7, x6 -> s6, x7 -> s5, x8 -> s13, x9 -> s3, x10 -> s4, x11 -> s18, x12 -> s16, x13 -> s10, x14 -> s7, x15 -> s41, x16 -> s42, x17 -> s45, x18 -> s6, x19 -> s44}
% 15.63/3.69  
% 15.63/3.69  SZS status Unsatisfiable
% 15.63/3.69  
% 15.63/3.69  Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.63/3.69  
% 15.63/3.69  SPASS-SCL-FOL Statistics:
% 15.63/3.69  Number of learned clauses: 316
% 15.63/3.69  Number of propagations: 19524
% 15.63/3.69  Number of decisions: 17792
% 15.63/3.69  Number of resolutions: 1368
% 15.63/3.69  Number of condensations: 16
% 15.63/3.69  Number of sub resolutions: 109
% 15.63/3.69  Number of input literals (deduplicated): 117
% 15.63/3.69  Number of grows: 16
% 15.63/3.69  Number of considered ground atoms: 640
% 15.63/3.69  
% 15.63/3.69   Needed:       0:00:03.15
% 15.63/3.69  
%------------------------------------------------------------------------------