%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SWV419-1.005 : TPTP v9.2.1. Released v3.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:14 PM UTC 2026
% Result : Unsatisfiable 31.41s 6.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : SWV419-1.005 : TPTP v9.2.1. Released v3.5.0.
% 0.00/0.07 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.25 % Computer : n012.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Thu May 7 13:28:16 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.25 SPASS-SCL-FOL version:
% 0.07/0.29 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 31.41/6.65 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.41/6.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.41/6.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.41/6.65 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.41/6.65 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.41/6.65 Execution resolution_1 ended with status: unsatisfiable
% 31.41/6.65 Used heuristic: resolution_1
% 31.41/6.65
% 31.41/6.65 Input Clauses:
% 31.41/6.65
% 31.41/6.65 Predicates: succ last trans loop m_cell_v_left m_cell_v_right m_cell_v_token m_mutex_h_half_v_inp m_user_v_req m_mutex_h_half_v_other_h_out m_mutex_h_half_v_out m_cell_v_req node1 m_and_h_gate_v_in1 m_and_h_gate_v_in2 m_cell_v_ack node2 m_user_v_ack m_c_h_element_v_in1 m_and_h_gate_v_out m_c_h_element_v_in2 m_or_h_gate_v_in1 m_or_h_gate_v_in2 m_or_h_gate_v_out m_c_h_element_v_out m_and_h_gate_h_init_v_out m_and_h_gate_h_init_v_in1 m_and_h_gate_h_init_v_in2 m_and_h_gate_h_init_v_init_h_out node3 node4 node5 node6 node7 node8 node9 node10 node11 node12 node13 node14 node15 node16 node17 node18 node19 node20 node21 node22 node23 node24 node25 node26 xuntil28 until27 until2p29 xuntil2p30
% 31.41/6.65 Fol Constants: s0 s1 s2 s3 s4 c_e_h_1 c_e_h_2 c_e_h_3 c_a c_u c_b c_c c_d c_e c_i c_f c_g c_h c_j c_l c_k c_m c_n c_p c_q c_r
% 31.41/6.65 Fol Functions:
% 31.41/6.65 Problem Properties:
% 31.41/6.65 This is a Bernays Schoenfinkel problem.
% 31.41/6.65
% 31.41/6.65 After reduction: Problem Properties:
% 31.41/6.65 This is a Bernays Schoenfinkel problem.
% 31.41/6.65
% 31.41/6.65
% 31.41/6.65 Reduced Input Clauses:
% 31.41/6.65
% 31.41/6.65 Most General Atoms: succ(x0,x1) trans(x0,x1) loop m_cell_v_right(c_e_h_1,c_e_h_3) m_cell_v_right(c_e_h_2,c_e_h_1) m_cell_v_right(c_e_h_3,c_e_h_2) m_cell_v_req(x2,x1) m_cell_v_left(x0,x1) node1(x0,x1,x2) node2(x0,x2,x1) m_cell_v_ack(x0,x1) m_cell_v_token(x0,x1) m_and_h_gate_h_init_v_init_h_out(x0,c_m,x1) m_and_h_gate_h_init_v_init_h_out(x0,c_n,x1) node3(x0,x1,x2) node4(x0,x1,x2) m_or_h_gate_v_out(x0,x1,x2) m_or_h_gate_v_in1(x0,x1,x3) m_or_h_gate_v_in2(x0,x1,x3) node5(x2,x3,x0,x1) node6(x2,x3,x0,x1) m_user_v_req(x0,x1,x2) m_user_v_ack(x0,x1,x3) node7(x2,x3,x0,x1) node8(x2,x3,x0,x1) m_and_h_gate_h_init_v_init_h_out(x0,x1,s0) m_and_h_gate_h_init_v_in1(x0,x1,x2) m_and_h_gate_h_init_v_in2(x0,x1,x2) m_and_h_gate_h_init_v_out(x0,x1,x2) node9(x0,x1,x3) node10(x2,x3,x0,x1) node11(x2,x3,x0,x1) m_mutex_h_half_v_inp(x0,x1,x3) node12(x2,x3,x0,x1) node13(x2,x3,x0,x1) m_mutex_h_half_v_out(x2,x3,x1) m_mutex_h_half_v_other_h_out(x2,x3,x1) m_c_h_element_v_out(x0,x1,x2) node14(x0,x1,x3,x2) m_c_h_element_v_in1(x0,x1,x3) node15(x0,x1,x3,x2) node16(x0,x1,x2) m_c_h_element_v_in2(x0,x1,x2) node17(x0,x1,x2) node18(x0,x1,x3,x2) node19(x2,x3,x0,x1) m_and_h_gate_v_in1(x0,x1,x2) m_and_h_gate_v_in2(x0,x1,x2) m_and_h_gate_v_out(x0,x1,x2) node20(x0,x1,x3) node21(x2,x3,x0,x1) node22(x2,x3,x0,x1) node23(x0) node24(x0) node25(x0) node26(x0) xuntil28(x0) until27(x1) last(x0) until2p29(x0) xuntil2p30(x0)
% 31.41/6.65
% 31.41/6.65 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_1 ===
% 31.41/6.65
% 31.41/6.65 === Backtracking. Learning clause 165:3:3:[21.2,23.2]:TopTopTop: m_cell_v_req(x0,x1),m_cell_v_left(x2,x0) -> m_mutex_h_half_v_inp(x2,c_b,x1)
% 31.41/6.65 === Backtracking. Learning clause 166:3:3:[28.1,30.2]:TopTopTop: m_cell_v_left(x0,x1) -> m_and_h_gate_v_in2(x0,c_c,x2),m_cell_v_ack(x1,x2)
% 31.41/6.65 === Backtracking. Learning clause 167:1:1:[53.2,98.1]:Top: -> m_and_h_gate_v_in2(x0,c_i,s0)
% 31.41/6.65 === Backtracking. Learning clause 168:1:1:[61.2,128.1]:Top: -> m_and_h_gate_v_in2(x0,c_k,s0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 118
% 31.41/6.65 === Restarting.
% 31.41/6.65 === Backtracking. Learning clause 169:2:0:[158.1,2.1]:: xuntil28(s1) -> until27(s2)
% 31.41/6.65 === Backtracking. Learning clause 170:1:1:[18.2,106.1]:Top: m_mutex_h_half_v_inp(x0,c_a,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 171:1:1:[25.2,121.1]:Top: m_mutex_h_half_v_other_h_out(x0,c_b,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 172:1:1:[20.2,121.1]:Top: m_mutex_h_half_v_other_h_out(x0,c_a,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 173:1:1:[36.2,142.1]:Top: m_c_h_element_v_in1(x0,c_e,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 174:1:1:[40.2,142.1]:Top: m_c_h_element_v_in1(x0,c_f,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 175:1:1:[64.2,142.1]:Top: m_and_h_gate_v_in1(x0,c_l,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 176:1:1:[80.2,142.1]:Top: m_and_h_gate_v_in1(x0,c_p,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 177:1:1:[92.2,142.1]:Top: m_cell_v_req(x0,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 178:1:1:[48.2,98.1]:Top: m_c_h_element_v_in1(x0,c_h,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 179:1:1:[60.2,98.1]:Top: m_and_h_gate_v_in1(x0,c_k,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 180:1:1:[50.2,98.1]:Top: m_c_h_element_v_in2(x0,c_h,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 181:2:2:[89.1,66.2]:TopTop: m_and_h_gate_v_in2(x0,c_l,x1) -> m_and_h_gate_v_in2(x0,c_r,x1)
% 31.41/6.65 === Backtracking. Learning clause 182:2:1:[113.2,72.1,66.2]:Top: m_and_h_gate_v_in2(x0,c_l,s0) -> m_cell_v_token(x0,s0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 128
% 31.41/6.65 === Restarting.
% 31.41/6.65 === Backtracking. Learning clause 183:2:0:[158.1,1.1]:: xuntil28(s0) -> until27(s1)
% 31.41/6.65 === Backtracking. Learning clause 184:2:0:[162.1,4.1]:: xuntil2p30(s3) -> until2p29(s4)
% 31.41/6.65 === Backtracking. Learning clause 185:3:3:[22.2,23.2]:TopTopTop: m_mutex_h_half_v_inp(x0,c_b,x1),m_cell_v_left(x0,x2) -> m_cell_v_req(x2,x1)
% 31.41/6.65 === Backtracking. Learning clause 186:2:1:[34.2,154.2]:Top: m_and_h_gate_v_in2(c_e_h_2,c_d,x0),node25(x0) ->
% 31.41/6.65 === Backtracking. Learning clause 187:1:1:[97.2,142.1,33.2]:Top: -> m_and_h_gate_v_in2(x0,c_d,s0)
% 31.41/6.65 === Conflict found: 186:2:1:[34.2,154.2]:Top: m_and_h_gate_v_in2(c_e_h_2,c_d,x0),node25(x0) -> {x0 -> s0}
% 31.41/6.65 === Backtracking. Learning clause 188:1:0:[186.1,187.1]:: node25(s0) ->
% 31.41/6.65 === Backtracking. Learning clause 189:1:1:[88.2,128.1]:Top: m_and_h_gate_v_in1(x0,c_r,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 190:1:1:[52.2,128.1]:Top: m_and_h_gate_v_in1(x0,c_i,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 191:2:2:[85.1,82.2]:TopTop: m_and_h_gate_v_in2(x0,c_p,x1) -> m_and_h_gate_v_in2(x0,c_q,x1)
% 31.41/6.65 === Backtracking. Learning clause 192:2:1:[113.2,78.1,82.2]:Top: m_cell_v_token(x0,s0),m_and_h_gate_v_in2(x0,c_p,s0) ->
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 130
% 31.41/6.65 === Restarting.
% 31.41/6.65 === Backtracking. Learning clause 193:4:2:[6.2,160.1]:TopTop: succ(x0,x1),last(x0),xuntil28(x0) -> until2p29(x1)
% 31.41/6.65 === Conflict found: 193:4:2:[6.2,160.1]:TopTop: succ(x0,x1),last(x0),xuntil28(x0) -> until2p29(x1) {x0 -> s0, x1 -> s1}
% 31.41/6.65 === Backtracking. Learning clause 194:3:0:[193.1,1.1]:: last(s0),xuntil28(s0) -> until2p29(s1)
% 31.41/6.65 === Backtracking. Learning clause 195:3:3:[29.3,30.2]:TopTopTop: m_and_h_gate_v_in2(x0,c_c,x1),m_cell_v_ack(x2,x1),m_cell_v_left(x0,x2) ->
% 31.41/6.65 === Backtracking. Learning clause 196:1:0:[34.2,150.2,187.1]:: node23(s0) ->
% 31.41/6.65 === Backtracking. Learning clause 197:1:0:[34.2,152.2,187.1]:: node24(s0) ->
% 31.41/6.65 === Backtracking. Learning clause 198:1:1:[84.2,128.1]:Top: m_and_h_gate_v_in1(x0,c_q,s0) ->
% 31.41/6.65 === Backtracking. Learning clause 199:2:2:[90.2,65.1]:TopTop: m_and_h_gate_v_in2(x0,c_r,x1) -> m_and_h_gate_v_in2(x0,c_l,x1)
% 31.41/6.65 === Backtracking. Learning clause 200:2:1:[112.1,77.1,81.1]:Top: -> m_cell_v_token(x0,s0),m_and_h_gate_v_in2(x0,c_p,s0)
% 31.41/6.65 === Backtracking. Learning clause 201:2:2:[94.2,95.2,142.1]:TopTop: m_cell_v_ack(x0,s0),m_cell_v_left(x1,x0) ->
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 133
% 31.41/6.65 === Restarting.
% 31.41/6.65 === Backtracking. Learning clause 202:2:0:[157.1,164.1,159.2,156.1,188.1,197.1,196.1]:: last(s0) -> loop
% 31.41/6.65 === Backtracking. Learning clause 203:2:0:[157.1,164.1]:: -> node26(s0),xuntil28(s0)
% 31.41/6.65 === Backtracking. Learning clause 204:2:2:[86.2,81.1]:TopTop: m_and_h_gate_v_in2(x0,c_q,x1) -> m_and_h_gate_v_in2(x0,c_p,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 197
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 261
% 31.41/6.65 === Backtracking. Learning clause 205:4:4:[149.2,146.2,148.2]:TopTopTopTop: trans(x0,x1),m_and_h_gate_v_out(x2,x3,x1) -> node20(x2,x3,x0),m_and_h_gate_v_out(x2,x3,x0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 325
% 31.41/6.65 === Backtracking. Learning clause 206:4:3:[97.2,205.2]:TopTopTop: m_user_v_ack(x0,c_u,x1),trans(x2,x1) -> node20(x0,c_r,x2),m_and_h_gate_v_out(x0,c_r,x2)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 389
% 31.41/6.65 === Backtracking. Learning clause 207:3:2:[143.2,189.1,205.3]:TopTop: trans(s0,x0),m_and_h_gate_v_out(x1,c_r,x0) -> m_and_h_gate_v_out(x1,c_r,s0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 453
% 31.41/6.65 === Backtracking. Learning clause 208:4:3:[120.2,117.2,119.2,69.2]:TopTopTop: trans(x0,x1) -> node9(x2,c_n,x0),m_and_h_gate_h_init_v_out(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 517
% 31.41/6.65 === Backtracking. Learning clause 209:2:2:[48.2,59.1]:TopTop: m_c_h_element_v_in1(x0,c_h,x1) -> m_and_h_gate_v_in1(x0,c_k,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 581
% 31.41/6.65 === Conflict found: 205:4:4:[149.2,146.2,148.2]:TopTopTopTop: trans(x0,x1),m_and_h_gate_v_out(x2,x3,x1) -> node20(x2,x3,x0),m_and_h_gate_v_out(x2,x3,x0) {x0 -> s1, x1 -> s2, x2 -> s0, x3 -> c_i}
% 31.41/6.65 === Backtracking. Learning clause 210:4:3:[205.2,42.2]:TopTopTop: trans(x0,x1),m_c_h_element_v_in2(x2,c_f,x1) -> node20(x2,c_i,x0),m_and_h_gate_v_out(x2,c_i,x0)
% 31.41/6.65 === Backtracking. Learning clause 211:5:4:[135.2,140.2,134.1,139.4,132.2,138.2]:TopTopTopTop: m_c_h_element_v_in2(x0,x1,x2),node19(x0,x1,x2,x3),m_c_h_element_v_out(x0,x1,x3) -> node14(x0,x1,x2,x3),m_c_h_element_v_out(x0,x1,x2)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 645
% 31.41/6.65 === Backtracking. Learning clause 212:2:2:[39.1,46.2]:TopTop: m_or_h_gate_v_in2(x0,c_g,x1) -> m_c_h_element_v_in1(x0,c_f,x1)
% 31.41/6.65 === Backtracking. Learning clause 213:3:3:[136.3,134.2]:TopTopTop: node17(x0,x1,x2),m_c_h_element_v_in1(x0,x1,x2),node16(x0,x1,x2) ->
% 31.41/6.65 === Backtracking. Learning clause 214:2:3:[135.1,133.3,213.2]:TopTopTop: node17(x0,x1,x2),node16(x0,x1,x2) ->
% 31.41/6.65 === Backtracking. Learning clause 215:6:2:[156.4,154.1,150.1,206.1,152.1,206.1,6.2]:TopTop: node26(x0),succ(x1,x0) -> node20(c_e_h_2,c_r,x1),m_and_h_gate_v_out(c_e_h_2,c_r,x1),node20(c_e_h_1,c_r,x1),m_and_h_gate_v_out(c_e_h_1,c_r,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 709
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 773
% 31.41/6.65 === Backtracking. Learning clause 216:5:4:[143.1,205.3,60.1,104.1]:TopTopTopTop: trans(x0,x1),m_and_h_gate_v_out(x2,c_k,x1),node6(x2,c_g,x3,x0) -> m_and_h_gate_v_out(x2,c_k,x0),m_or_h_gate_v_out(x2,c_g,x3)
% 31.41/6.65 === Backtracking. Learning clause 217:7:4:[105.2,102.2,216.3,60.2,143.2,205.3]:TopTopTopTop: trans(x0,x1),trans(x1,x2),m_and_h_gate_v_out(x3,c_k,x2) -> m_or_h_gate_v_in1(x3,c_g,x0),m_or_h_gate_v_in2(x3,c_g,x0),m_or_h_gate_v_out(x3,c_g,x0),m_and_h_gate_v_out(x3,c_k,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 837
% 31.41/6.65 === Backtracking. Learning clause 218:7:4:[80.2,217.3]:TopTopTopTop: m_and_h_gate_v_in1(x0,c_p,x1),trans(x2,x3),trans(x3,x1) -> m_or_h_gate_v_in1(x0,c_g,x2),m_or_h_gate_v_in2(x0,c_g,x2),m_or_h_gate_v_out(x0,c_g,x2),m_and_h_gate_v_out(x0,c_k,x3)
% 31.41/6.65 === Backtracking. Learning clause 219:4:4:[126.3,125.2,123.2]:TopTopTopTop: trans(x0,x1),m_mutex_h_half_v_out(x2,x3,x1) -> m_mutex_h_half_v_out(x2,x3,x0),m_mutex_h_half_v_inp(x2,x3,x0)
% 31.41/6.65 === Conflict found: 200:2:1:[112.1,77.1,81.1]:Top: -> m_cell_v_token(x0,s0),m_and_h_gate_v_in2(x0,c_p,s0) {x0 -> c_e_h_2}
% 31.41/6.65 === Backtracking. Learning clause 220:1:0:[200.2,191.1,13.1]:: -> m_and_h_gate_v_in2(c_e_h_2,c_q,s0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 901
% 31.41/6.65 === Conflict found: 210:4:3:[205.2,42.2]:TopTopTop: trans(x0,x1),m_c_h_element_v_in2(x2,c_f,x1) -> node20(x2,c_i,x0),m_and_h_gate_v_out(x2,c_i,x0) {x0 -> s2, x1 -> s3, x2 -> s0}
% 31.41/6.65 === Backtracking. Learning clause 221:4:3:[210.3,144.1,41.2,38.2]:TopTopTop: trans(x0,x1),m_c_h_element_v_in2(x2,c_e,x1) -> m_and_h_gate_v_out(x2,c_i,x0),m_and_h_gate_v_in2(x2,c_i,x0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 965
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1029
% 31.41/6.65 === Backtracking. Learning clause 222:5:3:[120.3,118.2,116.3,89.1]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_out(x2,c_m,x0),m_and_h_gate_h_init_v_in1(x2,c_m,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x0) -> m_and_h_gate_v_in2(x2,c_r,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1093
% 31.41/6.65 === Backtracking. Learning clause 224:1:0:[1.0,223.1,120.2,117.2,119.2,90.2,144.2,206.3,115.1,205.2,142.1,65.1,70.1,182.1,6.2,143.1,189.1,96.2,82.2,200.2,10.1,6.2,2.1]:: m_and_h_gate_v_out(c_e_h_1,c_r,s2) ->
% 31.41/6.65 === Backtracking. Learning clause 225:4:5:[116.2,115.2,114.2,117.3]:TopTopTopTopTop: node10(x0,x1,x2,x3),m_and_h_gate_h_init_v_out(x0,x1,x4),node10(x0,x1,x2,x4) -> m_and_h_gate_h_init_v_out(x0,x1,x3)
% 31.41/6.65 === Backtracking. Learning clause 226:9:3:[161.2,215.1,193.4]:TopTopTop: succ(x0,x1),succ(x2,x1),last(x2),xuntil28(x2) -> xuntil2p30(x1),node20(c_e_h_2,c_r,x0),m_and_h_gate_v_out(c_e_h_2,c_r,x0),node20(c_e_h_1,c_r,x0),m_and_h_gate_v_out(c_e_h_1,c_r,x0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1157
% 31.41/6.65 === Conflict found: 205:4:4:[149.2,146.2,148.2]:TopTopTopTop: trans(x0,x1),m_and_h_gate_v_out(x2,x3,x1) -> node20(x2,x3,x0),m_and_h_gate_v_out(x2,x3,x0) {x0 -> s3, x1 -> s4, x2 -> s0, x3 -> c_d}
% 31.41/6.65 === Backtracking. Learning clause 227:4:3:[205.3,144.1,40.2]:TopTopTop: trans(x0,x1),m_c_h_element_v_in1(x2,c_f,x1) -> m_and_h_gate_v_out(x2,c_d,x0),m_and_h_gate_v_in2(x2,c_d,x0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1221
% 31.41/6.65 === Backtracking. Learning clause 228:4:2:[152.2,206.1]:TopTop: node24(x0),trans(x1,x0) -> node20(c_e_h_1,c_r,x1),m_and_h_gate_v_out(c_e_h_1,c_r,x1)
% 31.41/6.65 === Backtracking. Learning clause 229:9:5:[139.2,130.2,132.2,52.2,143.2,205.3,210.4]:TopTopTopTopTop: node19(x0,c_h,x1,x2),trans(x2,x3),trans(x3,x4),m_c_h_element_v_in2(x0,c_f,x4) -> node16(x0,c_h,x1),m_c_h_element_v_in1(x0,c_h,x1),m_c_h_element_v_out(x0,c_h,x1),m_and_h_gate_v_out(x0,c_i,x2),node20(x0,c_i,x3)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1285
% 31.41/6.65 === Backtracking. Learning clause 231:6:4:[173.0,230.4,139.1,141.2,133.1,38.1,132.2,142.1,130.2,88.2,143.2,206.3,107.3]:TopTopTopTop: trans(s0,x0),trans(x0,x1),node7(x2,c_u,x1,x3) -> m_c_h_element_v_out(x2,c_e,s0),m_and_h_gate_v_out(x2,c_r,x0),m_user_v_req(x2,c_u,x3)
% 31.41/6.65 === Backtracking. Learning clause 232:5:3:[139.3,132.2,130.2,88.2,143.2]:TopTopTop: node19(x0,c_e,x1,x2),node20(x0,c_r,x2) -> node16(x0,c_e,x1),m_c_h_element_v_out(x0,c_e,x1),m_c_h_element_v_in1(x0,c_e,x1)
% 31.41/6.65 === Backtracking. Learning clause 233:5:3:[139.2,130.2,132.2,88.2]:TopTopTop: node19(x0,c_e,x1,x2),m_and_h_gate_v_in1(x0,c_r,x2) -> node16(x0,c_e,x1),m_c_h_element_v_in1(x0,c_e,x1),m_c_h_element_v_out(x0,c_e,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1349
% 31.41/6.65 === Backtracking. Learning clause 234:5:5:[146.2,149.2,148.3]:TopTopTopTopTop: trans(x0,x1),m_and_h_gate_v_out(x2,x3,x4),node22(x2,x3,x1,x4) -> node20(x2,x3,x0),node22(x2,x3,x0,x1)
% 31.41/6.65 === Backtracking. Learning clause 235:3:4:[145.1,143.2,144.2]:TopTopTopTop: node21(x0,x1,x2,x3),node20(x0,x1,x2) -> m_and_h_gate_v_out(x0,x1,x3)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1413
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1477
% 31.41/6.65 === Backtracking. Learning clause 236:4:3:[120.2,117.2,119.2,90.2,144.2]:TopTopTop: trans(x0,x1),node20(x2,c_r,x1) -> node9(x2,c_m,x0),m_and_h_gate_h_init_v_out(x2,c_m,x0)
% 31.41/6.65 === Backtracking. Learning clause 237:3:2:[133.2,173.1,38.1,142.1,139.4,141.2]:TopTop: trans(s0,x0) -> node14(x1,c_e,s0,x0),node15(x1,c_e,s0,x0)
% 31.41/6.65 === Conflict found: 232:5:3:[139.3,132.2,130.2,88.2,143.2]:TopTopTop: node19(x0,c_e,x1,x2),node20(x0,c_r,x2) -> node16(x0,c_e,x1),m_c_h_element_v_out(x0,c_e,x1),m_c_h_element_v_in1(x0,c_e,x1) {x0 -> s0, x1 -> s0, x2 -> s1}
% 31.41/6.65 === Backtracking. Learning clause 239:3:2:[173.0,238.3,232.4,128.1]:TopTop: node19(x0,c_e,s0,x1),node20(x0,c_r,x1) -> node16(x0,c_e,s0)
% 31.41/6.65 === Conflict found: 233:5:3:[139.2,130.2,132.2,88.2]:TopTopTop: node19(x0,c_e,x1,x2),m_and_h_gate_v_in1(x0,c_r,x2) -> node16(x0,c_e,x1),m_c_h_element_v_in1(x0,c_e,x1),m_c_h_element_v_out(x0,c_e,x1) {x0 -> s0, x1 -> s0, x2 -> s1}
% 31.41/6.65 === Backtracking. Learning clause 240:3:2:[233.5,128.1,133.1,173.1]:TopTop: node19(x0,c_e,s0,x1),m_and_h_gate_v_in1(x0,c_r,x1) -> m_c_h_element_v_in2(x0,c_e,s0)
% 31.41/6.65 === Backtracking. Learning clause 241:8:3:[161.2,215.1,162.3]:TopTopTop: succ(x0,x1),succ(x2,x1),xuntil2p30(x2) -> xuntil2p30(x1),node20(c_e_h_2,c_r,x0),m_and_h_gate_v_out(c_e_h_2,c_r,x0),node20(c_e_h_1,c_r,x0),m_and_h_gate_v_out(c_e_h_1,c_r,x0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1541
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1605
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1669
% 31.41/6.65 === Backtracking. Learning clause 242:8:3:[154.2,206.1,156.4,228.1]:TopTopTop: trans(x0,x1),node26(x1),trans(x2,x1) -> node20(c_e_h_2,c_r,x0),m_and_h_gate_v_out(c_e_h_2,c_r,x0),node23(x1),node20(c_e_h_1,c_r,x2),m_and_h_gate_v_out(c_e_h_1,c_r,x2)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1733
% 31.41/6.65 === Conflict found: 208:4:3:[120.2,117.2,119.2,69.2]:TopTopTop: trans(x0,x1) -> node9(x2,c_n,x0),m_and_h_gate_h_init_v_out(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) {x0 -> s3, x1 -> s4, x2 -> s0}
% 31.41/6.65 === Backtracking. Learning clause 243:4:3:[208.2,115.1]:TopTopTop: trans(x0,x1) -> m_and_h_gate_h_init_v_out(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1),m_and_h_gate_h_init_v_in2(x2,c_n,x0)
% 31.41/6.65 === Conflict found: 237:3:2:[133.2,173.1,38.1,142.1,139.4,141.2]:TopTop: trans(s0,x0) -> node14(x1,c_e,s0,x0),node15(x1,c_e,s0,x0) {x0 -> s1, x1 -> c_e_h_2}
% 31.41/6.65 === Backtracking. Learning clause 246:2:2:[173.0,244.2,128.0,245.3,237.2,130.2,132.2,88.2]:TopTop: trans(s0,x0),m_and_h_gate_v_in1(x1,c_r,x0) ->
% 31.41/6.65 === Backtracking. Learning clause 247:4:2:[71.1,77.2,112.1,222.2,69.1,112.1]:TopTop: trans(s0,x0),m_and_h_gate_h_init_v_in1(x1,c_m,s0) -> m_and_h_gate_v_in2(x1,c_r,x0),m_and_h_gate_h_init_v_out(x1,c_n,s0)
% 31.41/6.65 === Backtracking. Learning clause 248:5:3:[120.2,116.3,118.2,70.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in1(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_out(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) ->
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1797
% 31.41/6.65 === Conflict found: 219:4:4:[126.3,125.2,123.2]:TopTopTopTop: trans(x0,x1),m_mutex_h_half_v_out(x2,x3,x1) -> m_mutex_h_half_v_out(x2,x3,x0),m_mutex_h_half_v_inp(x2,x3,x0) {x0 -> s2, x1 -> c_e, x2 -> s0, x3 -> s0}
% 31.41/6.65 === Backtracking. Learning clause 249:4:4:[219.1,6.2]:TopTopTopTop: m_mutex_h_half_v_out(x0,x1,x2),succ(x3,x2) -> m_mutex_h_half_v_out(x0,x1,x3),m_mutex_h_half_v_inp(x0,x1,x3)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1861
% 31.41/6.65 === Backtracking. Learning clause 250:4:3:[6.2,206.2]:TopTopTop: succ(x0,x1),m_user_v_ack(x2,c_u,x1) -> node20(x2,c_r,x0),m_and_h_gate_v_out(x2,c_r,x0)
% 31.41/6.65 === Backtracking. Learning clause 251:5:3:[141.1,6.2,233.1]:TopTopTop: succ(x0,x1),m_and_h_gate_v_in1(x2,c_r,x1) -> node16(x2,c_e,x0),m_c_h_element_v_in1(x2,c_e,x0),m_c_h_element_v_out(x2,c_e,x0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1925
% 31.41/6.65 === Conflict found: 206:4:3:[97.2,205.2]:TopTopTop: m_user_v_ack(x0,c_u,x1),trans(x2,x1) -> node20(x0,c_r,x2),m_and_h_gate_v_out(x0,c_r,x2) {x0 -> c_e_h_2, x1 -> c_i, x2 -> s0}
% 31.41/6.65 === Backtracking. Learning clause 252:4:2:[206.1,151.2]:TopTop: trans(x0,x1),node23(x1) -> node20(c_e_h_2,c_r,x0),m_and_h_gate_v_out(c_e_h_2,c_r,x0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 1989
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2053
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2117
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2181
% 31.41/6.65 === Conflict found: 250:4:3:[6.2,206.2]:TopTopTop: succ(x0,x1),m_user_v_ack(x2,c_u,x1) -> node20(x2,c_r,x0),m_and_h_gate_v_out(x2,c_r,x0) {x0 -> c_a, x1 -> s3, x2 -> c_e_h_1}
% 31.41/6.65 === Backtracking. Learning clause 253:6:4:[250.3,236.2]:TopTopTopTop: succ(x0,x1),m_user_v_ack(x2,c_u,x1),trans(x3,x0) -> m_and_h_gate_v_out(x2,c_r,x0),node9(x2,c_m,x3),m_and_h_gate_h_init_v_out(x2,c_m,x3)
% 31.41/6.65 === Backtracking. Learning clause 254:8:4:[120.3,119.2,117.2,236.4,228.3]:TopTopTopTop: trans(x0,x1),trans(x1,x2),node24(x3),trans(x2,x3) -> m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x0),node9(c_e_h_1,c_m,x0),node9(c_e_h_1,c_m,x1),m_and_h_gate_v_out(c_e_h_1,c_r,x2)
% 31.41/6.65 === Conflict found: 242:8:3:[154.2,206.1,156.4,228.1]:TopTopTop: trans(x0,x1),node26(x1),trans(x2,x1) -> node20(c_e_h_2,c_r,x0),m_and_h_gate_v_out(c_e_h_2,c_r,x0),node23(x1),node20(c_e_h_1,c_r,x2),m_and_h_gate_v_out(c_e_h_1,c_r,x2) {x0 -> s2, x1 -> c_b, x2 -> s2}
% 31.41/6.65 === Backtracking. Learning clause 255:7:3:[242.6,252.2]:TopTopTop: node26(x0),trans(x1,x0),trans(x2,x0) -> node20(c_e_h_1,c_r,x1),m_and_h_gate_v_out(c_e_h_1,c_r,x1),node20(c_e_h_2,c_r,x2),m_and_h_gate_v_out(c_e_h_2,c_r,x2)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2245
% 31.41/6.65 === Conflict found: 254:8:4:[120.3,119.2,117.2,236.4,228.3]:TopTopTopTop: trans(x0,x1),trans(x1,x2),node24(x3),trans(x2,x3) -> m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x0),node9(c_e_h_1,c_m,x0),node9(c_e_h_1,c_m,x1),m_and_h_gate_v_out(c_e_h_1,c_r,x2) {x0 -> s1, x1 -> s2, x2 -> s3, x3 -> s4}
% 31.41/6.65 === Backtracking. Learning clause 256:10:5:[254.7,115.1,156.3,154.1,151.1,97.1,148.1]:TopTopTopTopTop: trans(x0,x1),trans(x1,x2),trans(x2,x3),node26(x3),node22(c_e_h_2,c_r,x4,x3) -> m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x0),node9(c_e_h_1,c_m,x0),m_and_h_gate_v_out(c_e_h_1,c_r,x2),m_and_h_gate_h_init_v_in2(c_e_h_1,c_m,x1),m_and_h_gate_v_out(c_e_h_2,c_r,x4)
% 31.41/6.65 === Backtracking. Learning clause 257:4:5:[102.3,99.1,100.1,101.3]:TopTopTopTopTop: m_or_h_gate_v_out(x0,x1,x2),node5(x0,x1,x3,x2),node5(x0,x1,x3,x4) -> m_or_h_gate_v_out(x0,x1,x4)
% 31.41/6.65 === Backtracking. Learning clause 262:12:1:[5.0,258.0,3.0,259.3,4.0,260.4,215.0,261.7,7.3,160.1,160.1,160.1,160.1,161.1,160.1,161.1,159.3,157.3,241.3,162.2,161.1,156.1,154.1,151.1,97.1]:Top: until27(s4),succ(x0,s3) -> until2p29(s1),until2p29(s0),node26(s2),node20(c_e_h_2,c_r,x0),m_and_h_gate_v_out(c_e_h_2,c_r,x0),node20(c_e_h_1,c_r,x0),m_and_h_gate_v_out(c_e_h_1,c_r,x0),xuntil2p30(s4),node24(s4),m_and_h_gate_v_out(c_e_h_2,c_r,s4)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2309
% 31.41/6.65 === Conflict found: 248:5:3:[120.2,116.3,118.2,70.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in1(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_out(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) -> {x0 -> c_a, x1 -> s3, x2 -> s0}
% 31.41/6.65 === Backtracking. Learning clause 263:5:3:[248.2,73.1,69.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) -> m_c_h_element_v_out(x2,c_e,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x0)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2373
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2437
% 31.41/6.65 === Backtracking. Learning clause 264:4:2:[147.2,149.3,97.2,150.2]:TopTop: trans(x0,x1),node23(x0) -> m_and_h_gate_v_out(c_e_h_1,c_r,x1),node21(c_e_h_1,c_r,x0,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2501
% 31.41/6.65 === Backtracking. Learning clause 265:12:5:[120.3,119.2,117.2,253.6,205.2,236.2,115.1,150.2,115.1,263.3,248.5]:TopTopTopTopTop: succ(x0,x1),trans(x2,x0),trans(x3,x2),node23(x1),m_and_h_gate_h_init_v_in2(c_e_h_1,c_n,x3),trans(x4,x3),m_and_h_gate_h_init_v_in1(c_e_h_1,c_n,x4),m_and_h_gate_h_init_v_in2(c_e_h_1,c_n,x4),m_and_h_gate_h_init_v_out(c_e_h_1,c_n,x4) -> m_and_h_gate_v_out(c_e_h_1,c_r,x2),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x3),m_c_h_element_v_out(c_e_h_1,c_e,x3)
% 31.41/6.65 === Backtracking. Learning clause 274:28:7:[5.0,266.0,1.0,267.5,2.0,268.7,3.0,269.8,4.0,270.12,215.0,271.20,215.0,272.25,154.0,273.26,7.3,160.1,160.1,160.1,160.1,160.1,159.3,157.3,158.3,157.3,158.3,157.3,158.3,157.3,161.1,241.3,161.1,241.3,161.1,162.2,161.1,156.1,151.1,254.3,162.2,161.1,156.1]:TopTopTopTopTopTopTop: succ(x0,s3),succ(x1,x0),until27(x1),succ(x2,s1),succ(x3,s2),trans(x4,x5),trans(x5,x6),trans(x6,s3) -> node26(x0),node26(x1),node26(s0),node20(c_e_h_2,c_r,x2),m_and_h_gate_v_out(c_e_h_2,c_r,x2),node20(c_e_h_1,c_r,x2),m_and_h_gate_v_out(c_e_h_1,c_r,x2),node20(c_e_h_2,c_r,x3),m_and_h_gate_v_out(c_e_h_2,c_r,x3),node20(c_e_h_1,c_r,x3),m_and_h_gate_v_out(c_e_h_1,c_r,x3),m_user_v_ack(c_e_h_2,c_u,s3),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x4),node9(c_e_h_1,c_m,x4),node9(c_e_h_1,c_m,x5),m_and_h_gate_v_out(c_e_h_1,c_r,x6),xuntil2p30(s4),node23(s4),node24(s4),node25(s4)
% 31.41/6.65 === Backtracking. Learning clause 275:4:4:[120.3,119.2,117.2]:TopTopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_out(x2,x3,x1) -> m_and_h_gate_h_init_v_out(x2,x3,x0),node9(x2,x3,x0)
% 31.41/6.65 === Backtracking. Learning clause 277:11:4:[246.1,276.11,148.3,142.1,149.3,146.2,255.7,161.2,207.2,236.2,143.1]:TopTopTopTop: trans(s0,x0),trans(x1,x2),trans(x0,x2),until2p29(x2),trans(s0,x1),trans(x3,x1) -> node20(c_e_h_2,c_r,s0),xuntil2p30(x2),m_and_h_gate_v_out(c_e_h_1,c_r,s0),node9(c_e_h_1,c_m,x3),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x3)
% 31.41/6.65 === Backtracking. Learning clause 278:2:0:[159.1,5.1]:: xuntil28(s4) -> loop
% 31.41/6.65 === Conflict found: 263:5:3:[248.2,73.1,69.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) -> m_c_h_element_v_out(x2,c_e,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x0) {x0 -> s0, x1 -> s1, x2 -> c_e_h_1}
% 31.41/6.65 === Backtracking. Learning clause 279:5:3:[263.4,128.1,75.1,115.2,117.3]:TopTopTop: trans(s0,x0),m_and_h_gate_h_init_v_out(x1,c_m,x2),node10(x1,c_m,x0,x2) -> m_and_h_gate_h_init_v_in2(x1,c_m,s0),m_and_h_gate_h_init_v_out(x1,c_m,s0)
% 31.41/6.65 === Conflict found: 253:6:4:[250.3,236.2]:TopTopTopTop: succ(x0,x1),m_user_v_ack(x2,c_u,x1),trans(x3,x0) -> m_and_h_gate_v_out(x2,c_r,x0),node9(x2,c_m,x3),m_and_h_gate_h_init_v_out(x2,c_m,x3) {x0 -> s3, x1 -> s4, x2 -> c_e_h_1, x3 -> s2}
% 31.41/6.65 === Backtracking. Learning clause 280:5:1:[253.4,205.2,6.2,3.1,4.1]:Top: m_user_v_ack(x0,c_u,s4) -> node9(x0,c_m,s2),m_and_h_gate_h_init_v_out(x0,c_m,s2),node20(x0,c_r,s2),m_and_h_gate_v_out(x0,c_r,s2)
% 31.41/6.65 === Conflict found: 263:5:3:[248.2,73.1,69.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) -> m_c_h_element_v_out(x2,c_e,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x0) {x0 -> s1, x1 -> s2, x2 -> c_e_h_1}
% 31.41/6.65 === Backtracking. Learning clause 281:11:4:[263.4,87.1,75.1,246.2,115.2,280.2,236.2,275.2,115.1,263.3,128.1,75.1,279.2]:TopTopTopTop: m_user_v_ack(x1,c_u,s4),trans(x0,s2),trans(x2,x0),trans(s0,x0),trans(s0,x3),node10(x1,c_m,x3,s2) -> m_and_h_gate_v_out(x1,c_r,s2),m_and_h_gate_h_init_v_out(x1,c_m,x2),node9(x1,c_m,x2),m_and_h_gate_h_init_v_in2(x1,c_m,s0),m_and_h_gate_h_init_v_out(x1,c_m,s0)
% 31.41/6.65 === Conflict found: 275:4:4:[120.3,119.2,117.2]:TopTopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_out(x2,x3,x1) -> m_and_h_gate_h_init_v_out(x2,x3,x0),node9(x2,x3,x0) {x0 -> s1, x1 -> s2, x2 -> c_e_h_1, x3 -> c_m}
% 31.41/6.65 === Backtracking. Learning clause 282:8:4:[275.3,275.2,115.1,263.3,75.1,128.1]:TopTopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_out(x2,c_m,x1),trans(x3,x0),trans(s0,x0) -> m_and_h_gate_h_init_v_out(x2,c_m,x3),node9(x2,c_m,x3),m_and_h_gate_h_init_v_in2(x2,c_m,s0),m_and_h_gate_h_init_v_out(x2,c_m,s0)
% 31.41/6.65 === Backtracking. Learning clause 284:4:0:[224.0,283.4,150.2,280.1]:: node23(s4) -> node9(c_e_h_1,c_m,s2),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s2),node20(c_e_h_1,c_r,s2)
% 31.41/6.65 === Backtracking. Learning clause 285:4:2:[161.3,163.2,162.3]:TopTop: last(x0),succ(x1,x0),xuntil2p30(x1) -> node26(x0)
% 31.41/6.65 === Backtracking. Learning clause 286:3:1:[161.3,163.2]:Top: until2p29(x0),last(x0) -> node26(x0)
% 31.41/6.65 === Backtracking. Learning clause 291:32:9:[203.1,287.12,5.0,288.15,150.0,289.25,13.0,290.31,115.1,253.5,248.5,275.2,115.1,274.20,70.1,73.1,75.1,65.1,128.1,255.1,205.2,182.1,82.2,183.2,215.1,143.1,246.2,163.2,152.1]:TopTopTopTopTopTopTopTopTop: succ(x0,s3),succ(x1,s3),succ(s1,x1),succ(x2,s1),succ(x3,s2),trans(x4,x5),trans(x5,x6),trans(x6,s3),trans(x7,s1),trans(x8,s1),trans(x3,x0),m_and_h_gate_v_in2(c_e_h_2,c_p,s0),succ(x3,x1),trans(s0,x3) -> node26(s0),node20(c_e_h_2,c_r,x2),m_and_h_gate_v_out(c_e_h_2,c_r,x2),node20(c_e_h_1,c_r,x2),m_and_h_gate_v_out(c_e_h_1,c_r,x2),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x4),node9(c_e_h_1,c_m,x4),node9(c_e_h_1,c_m,x5),m_and_h_gate_v_out(c_e_h_1,c_r,x6),node25(s4),node20(c_e_h_1,c_r,x7),m_and_h_gate_v_out(c_e_h_1,c_r,x7),node20(c_e_h_2,c_r,x8),m_and_h_gate_v_out(c_e_h_2,c_r,x8),m_and_h_gate_v_out(c_e_h_2,c_r,x3),node20(c_e_h_1,c_r,x3),m_and_h_gate_v_out(c_e_h_1,c_r,x3),m_user_v_ack(c_e_h_1,c_u,s4)
% 31.41/6.65 === Conflict found: 205:4:4:[149.2,146.2,148.2]:TopTopTopTop: trans(x0,x1),m_and_h_gate_v_out(x2,x3,x1) -> node20(x2,x3,x0),m_and_h_gate_v_out(x2,x3,x0) {x0 -> s0, x1 -> s1, x2 -> s0, x3 -> c_k}
% 31.41/6.65 === Backtracking. Learning clause 292:4:3:[205.2,80.2,143.1]:TopTopTop: trans(x0,x1),m_and_h_gate_v_in1(x2,c_p,x1) -> m_and_h_gate_v_out(x2,c_k,x0),m_and_h_gate_v_in1(x2,c_k,x0)
% 31.41/6.65 === Conflict found: 250:4:3:[6.2,206.2]:TopTopTop: succ(x0,x1),m_user_v_ack(x2,c_u,x1) -> node20(x2,c_r,x0),m_and_h_gate_v_out(x2,c_r,x0) {x0 -> s3, x1 -> s4, x2 -> c_e_h_2}
% 31.41/6.65 === Backtracking. Learning clause 293:4:3:[250.3,235.2,96.1]:TopTopTop: succ(x0,x1),m_user_v_ack(x2,c_u,x1),node21(x2,c_r,x0,x0) -> m_user_v_ack(x2,c_u,x0)
% 31.41/6.65 === Backtracking. Learning clause 294:7:4:[64.2,217.3,143.2]:TopTopTopTop: trans(x0,x1),trans(x1,x2),node20(x3,c_l,x2) -> m_or_h_gate_v_in1(x3,c_g,x0),m_or_h_gate_v_in2(x3,c_g,x0),m_or_h_gate_v_out(x3,c_g,x0),m_and_h_gate_v_out(x3,c_k,x1)
% 31.41/6.65 === Clause set with instances from active satisfied. Growing active. New size: 2565
% 31.41/6.65 === Backtracking. Learning clause 295:2:2:[66.1,144.2]:TopTop: node20(x0,c_l,x1) -> m_and_h_gate_h_init_v_out(x0,c_m,x1)
% 31.41/6.65 === Backtracking. Learning clause 296:4:1:[6.1,1.1,263.1]:Top: m_and_h_gate_h_init_v_in2(x0,c_n,s0),m_and_h_gate_h_init_v_in2(x0,c_m,s1) -> m_c_h_element_v_out(x0,c_e,s0),m_and_h_gate_h_init_v_in2(x0,c_m,s0)
% 31.41/6.65 === Backtracking. Learning clause 297:5:3:[117.3,115.1,120.2,119.2,6.2,1.1,275.3]:TopTopTop: trans(s1,x0),m_and_h_gate_h_init_v_out(x1,x2,x0) -> m_and_h_gate_h_init_v_in2(x1,x2,s0),m_and_h_gate_h_init_v_out(x1,x2,s0),node9(x1,x2,s1)
% 31.41/6.65 === Conflict found: 263:5:3:[248.2,73.1,69.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) -> m_c_h_element_v_out(x2,c_e,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x0) {x0 -> s1, x1 -> s2, x2 -> c_e_h_2}
% 31.41/6.65 === Backtracking. Learning clause 300:9:1:[246.1,298.5,224.0,299.7,263.3,115.2,75.1,253.5,297.2,96.1,253.2,275.2,115.1,70.1,115.1,248.5,82.2,200.2,75.1,65.1,182.1,13.1,87.1,205.2,207.2,142.1,6.2,3.1,4.1,154.2,73.1,128.1,156.4,152.1,280.1,284.1]:Top: trans(s1,s2),trans(s0,s1),trans(x0,s2),trans(s0,x0),node26(s4) -> node20(c_e_h_2,c_r,x0),node9(c_e_h_1,c_m,s2),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s2),node20(c_e_h_1,c_r,s2)
% 31.41/6.65 === Conflict found: 263:5:3:[248.2,73.1,69.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) -> m_c_h_element_v_out(x2,c_e,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x0) {x0 -> s1, x1 -> s2, x2 -> c_e_h_2}
% 31.41/6.65 === Backtracking. Learning clause 302:7:2:[246.1,301.6,263.2,75.1,115.2,253.5,282.2,96.1,253.2,115.1,275.2,115.1,70.1,248.5,82.2,200.2,75.1,65.1,182.1,13.1,87.1,205.2,207.2,142.1,6.2,3.1,4.1,151.2]:TopTop: trans(x0,s2),trans(s0,x0),m_and_h_gate_h_init_v_in1(c_e_h_2,c_n,s0),trans(x1,s2),trans(s0,x1),node23(s4) -> node20(c_e_h_2,c_r,x1)
% 31.41/6.65 === Conflict found: 263:5:3:[248.2,73.1,69.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) -> m_c_h_element_v_out(x2,c_e,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x0) {x0 -> s1, x1 -> s2, x2 -> c_e_h_1}
% 31.41/6.65 === Backtracking. Learning clause 303:10:1:[263.4,87.1,75.1,246.2,115.2,300.7,161.2,143.1,246.2]:Top: trans(x0,s2),trans(s0,x0),trans(s1,s2),trans(s0,s1),until2p29(s4) -> m_and_h_gate_h_init_v_in2(c_e_h_1,c_m,x0),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x0),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s2),node20(c_e_h_1,c_r,s2),xuntil2p30(s4)
% 31.41/6.65 === Conflict found: 286:3:1:[161.3,163.2]:Top: until2p29(x0),last(x0) -> node26(x0) {x0 -> s4}
% 31.41/6.65 === Backtracking. Learning clause 304:6:0:[286.2,5.1,300.5,236.2,115.1,70.1,82.2,200.2,65.1,182.1,13.1]:: until2p29(s4),trans(s1,s2),trans(s0,s1) -> node9(c_e_h_1,c_m,s2),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s2),node20(c_e_h_1,c_r,s2)
% 31.41/6.65 === Backtracking. Learning clause 305:4:1:[73.2,128.1,302.3]:Top: trans(x0,s2),trans(s0,x0),node23(s4) -> node20(c_e_h_2,c_r,x0)
% 31.41/6.65 === Backtracking. Learning clause 306:9:1:[87.2,246.2,263.4,75.1,115.2,304.4]:Top: trans(s0,x0),trans(x0,s2),until2p29(s4),trans(s1,s2),trans(s0,s1) -> m_and_h_gate_h_init_v_in2(c_e_h_1,c_m,x0),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x0),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s2),node20(c_e_h_1,c_r,s2)
% 31.41/6.65 === Conflict found: 291:32:9:[203.1,287.12,5.0,288.15,150.0,289.25,13.0,290.31,115.1,253.5,248.5,275.2,115.1,274.20,70.1,73.1,75.1,65.1,128.1,255.1,205.2,182.1,82.2,183.2,215.1,143.1,246.2,163.2,152.1]:TopTopTopTopTopTopTopTopTop: succ(x0,s3),succ(x1,s3),succ(s1,x1),succ(x2,s1),succ(x3,s2),trans(x4,x5),trans(x5,x6),trans(x6,s3),trans(x7,s1),trans(x8,s1),trans(x3,x0),m_and_h_gate_v_in2(c_e_h_2,c_p,s0),succ(x3,x1),trans(s0,x3) -> node26(s0),node20(c_e_h_2,c_r,x2),m_and_h_gate_v_out(c_e_h_2,c_r,x2),node20(c_e_h_1,c_r,x2),m_and_h_gate_v_out(c_e_h_1,c_r,x2),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x4),node9(c_e_h_1,c_m,x4),node9(c_e_h_1,c_m,x5),m_and_h_gate_v_out(c_e_h_1,c_r,x6),node25(s4),node20(c_e_h_1,c_r,x7),m_and_h_gate_v_out(c_e_h_1,c_r,x7),node20(c_e_h_2,c_r,x8),m_and_h_gate_v_out(c_e_h_2,c_r,x8),m_and_h_gate_v_out(c_e_h_2,c_r,x3),node20(c_e_h_1,c_r,x3),m_and_h_gate_v_out(c_e_h_1,c_r,x3),m_user_v_ack(c_e_h_1,c_u,s4) {x0 -> s2, x1 -> s2, x2 -> s0, x3 -> s1, x4 -> s0, x5 -> s1, x6 -> s2, x7 -> s0, x8 -> s0}
% 31.41/6.65 === Backtracking. Learning clause 312:12:3:[2.0,307.0,1.0,308.1,6.1,309.6,142.0,310.11,224.0,311.16,291.15,156.1,143.1,189.1,188.1,196.1,197.1,143.1,207.2,115.1,280.1,154.1,253.2,115.1,263.3,282.2,75.1,87.1,246.2,96.1,253.2,205.2,207.2,142.1,6.2,3.1,4.1,115.1,248.5,75.1,275.2,73.1,128.1,246.2,236.2,115.1,70.1,82.2,200.2,65.1,182.1,13.1]:TopTopTop: trans(x0,x1),trans(x1,s2),trans(s0,s1),succ(x2,s2),trans(s0,x2) -> node20(c_e_h_1,c_r,s0),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x0),node9(c_e_h_1,c_m,x1),m_and_h_gate_h_init_v_in2(c_e_h_1,c_m,x0),node9(c_e_h_1,c_m,s2),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s2),node20(c_e_h_1,c_r,s2)
% 31.41/6.65 === Conflict found: 263:5:3:[248.2,73.1,69.2]:TopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_in2(x2,c_n,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x1) -> m_c_h_element_v_out(x2,c_e,x0),m_and_h_gate_h_init_v_in2(x2,c_m,x0) {x0 -> s1, x1 -> s2, x2 -> c_e_h_1}
% 31.41/6.65 === Backtracking. Learning clause 313:17:5:[263.4,87.1,75.1,115.2,246.2,312.10,236.2]:TopTopTopTopTop: trans(x0,s2),trans(s0,x0),trans(x1,x2),trans(x2,s2),trans(s0,s1),succ(x3,s2),trans(s0,x3),trans(x4,s2) -> m_and_h_gate_h_init_v_in2(c_e_h_1,c_m,x0),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x0),node20(c_e_h_1,c_r,s0),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x1),node9(c_e_h_1,c_m,x2),m_and_h_gate_h_init_v_in2(c_e_h_1,c_m,x1),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s2),node9(c_e_h_1,c_m,x4),m_and_h_gate_h_init_v_out(c_e_h_1,c_m,x4)
% 31.41/6.65 === Conflict found: 275:4:4:[120.3,119.2,117.2]:TopTopTopTop: trans(x0,x1),m_and_h_gate_h_init_v_out(x2,x3,x1) -> m_and_h_gate_h_init_v_out(x2,x3,x0),node9(x2,x3,x0) {x0 -> s0, x1 -> s1, x2 -> c_e_h_1, x3 -> c_m}
% 31.41/6.65
% 31.41/6.65 SZS status Unsatisfiable
% 31.41/6.65
% 31.41/6.65 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.41/6.65
% 31.41/6.65 SPASS-SCL-FOL Statistics:
% 31.41/6.65 Number of learned clauses: 118
% 31.41/6.65 Number of propagations: 27843
% 31.41/6.65 Number of decisions: 15889
% 31.41/6.65 Number of resolutions: 480
% 31.41/6.65 Number of condensations: 10
% 31.41/6.65 Number of sub resolutions: 31
% 31.41/6.65 Number of input literals (deduplicated): 140
% 31.41/6.65 Number of grows: 42
% 31.41/6.65 Number of considered ground atoms: 2565
% 31.41/6.65
% 31.41/6.65 Needed: 0:00:06.28
% 31.41/6.65
%------------------------------------------------------------------------------