%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV419-1.005 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:50:45 PM UTC 2026
% Result : Unsatisfiable 7.67s 1.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV419-1.005 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n004.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 08:45:35 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 7.67/1.40 % Refutation found
% 7.67/1.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 7.67/1.40 % SZS output start CNFRefutation for theBenchmark
% 7.67/1.40 fof(f1,axiom,(
% 7.67/1.40 succ(s0,s1) ),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f2,axiom,(
% 7.67/1.40 succ(s1,s2) ),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f3,axiom,(
% 7.67/1.40 succ(s2,s3) ),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f4,axiom,(
% 7.67/1.40 succ(s3,s4) ),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f5,axiom,(
% 7.67/1.40 last(s4) ),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f6,axiom,(
% 7.67/1.40 (![X,Y]: (( ~ succ(X,Y)| trans(X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f7,axiom,(
% 7.67/1.40 ( ~ loop| trans(s4,s0)| trans(s4,s1)| trans(s4,s2)| trans(s4,s3)| trans(s4,s4) ) ),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f10,axiom,(
% 7.67/1.40 (![X]: (~ m_cell_v_token(c_e_h_1,X) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f11,axiom,(
% 7.67/1.40 m_cell_v_left(c_e_h_2,c_e_h_3) ),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f13,axiom,(
% 7.67/1.40 (![X]: (~ m_cell_v_token(c_e_h_2,X) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f33,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_v_in2(I0,c_d,X)| m_user_v_ack(I0,c_u,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f34,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_and_h_gate_v_in2(I0,c_d,X)| ~ m_user_v_ack(I0,c_u,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f38,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_c_h_element_v_in2(I0,c_e,X)| m_and_h_gate_v_out(I0,c_i,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f65,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_v_in2(I0,c_l,X)| ~ m_and_h_gate_h_init_v_out(I0,c_m,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f66,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_and_h_gate_v_in2(I0,c_l,X)| m_and_h_gate_h_init_v_out(I0,c_m,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f67,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_h_init_v_in1(I0,c_m,X)| m_c_h_element_v_out(I0,c_f,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f69,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_h_init_v_in2(I0,c_m,X)| m_and_h_gate_h_init_v_out(I0,c_n,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f70,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_and_h_gate_h_init_v_in2(I0,c_m,X)| ~ m_and_h_gate_h_init_v_out(I0,c_n,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f71,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_h_init_v_init_h_out(I0,c_m,X)| ~ m_cell_v_token(I0,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f72,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_and_h_gate_h_init_v_init_h_out(I0,c_m,X)| m_cell_v_token(I0,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f73,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_h_init_v_in1(I0,c_n,X)| m_c_h_element_v_out(I0,c_e,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f75,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_h_init_v_in2(I0,c_n,X)| m_and_h_gate_h_init_v_out(I0,c_m,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f77,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_h_init_v_init_h_out(I0,c_n,X)| m_cell_v_token(I0,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f78,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_and_h_gate_h_init_v_init_h_out(I0,c_n,X)| ~ m_cell_v_token(I0,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f85,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_v_in2(I0,c_q,X)| ~ m_and_h_gate_h_init_v_out(I0,c_n,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f86,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_and_h_gate_v_in2(I0,c_q,X)| m_and_h_gate_h_init_v_out(I0,c_n,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f88,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_and_h_gate_v_in1(I0,c_r,X)| m_c_h_element_v_out(I0,c_e,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f89,axiom,(
% 7.67/1.40 (![I0,X]: (( m_and_h_gate_v_in2(I0,c_r,X)| ~ m_and_h_gate_h_init_v_out(I0,c_m,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f90,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_and_h_gate_v_in2(I0,c_r,X)| m_and_h_gate_h_init_v_out(I0,c_m,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f94,axiom,(
% 7.67/1.40 (![J0,X,I0]: (( ~ m_cell_v_ack(J0,X)| m_and_h_gate_v_out(I0,c_q,X)| ~ node3(I0,J0,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f95,axiom,(
% 7.67/1.40 (![I0,J0,X]: (( ~ m_cell_v_left(I0,J0)| node3(I0,J0,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f96,axiom,(
% 7.67/1.40 (![I0,X]: (( m_user_v_ack(I0,c_u,X)| ~ m_and_h_gate_v_out(I0,c_r,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f97,axiom,(
% 7.67/1.40 (![I0,X]: (( ~ m_user_v_ack(I0,c_u,X)| m_and_h_gate_v_out(I0,c_r,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f112,axiom,(
% 7.67/1.40 (![I0,I1]: (( m_and_h_gate_h_init_v_out(I0,I1,s0)| ~ m_and_h_gate_h_init_v_init_h_out(I0,I1,s0) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f113,axiom,(
% 7.67/1.40 (![I0,I1]: (( ~ m_and_h_gate_h_init_v_out(I0,I1,s0)| m_and_h_gate_h_init_v_init_h_out(I0,I1,s0) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f115,axiom,(
% 7.67/1.40 (![I0,I1,X]: (( m_and_h_gate_h_init_v_in2(I0,I1,X)| ~ node9(I0,I1,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f116,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( m_and_h_gate_h_init_v_out(I0,I1,Y)| ~ m_and_h_gate_h_init_v_in1(I0,I1,X)| ~ m_and_h_gate_h_init_v_in2(I0,I1,X)| ~ node10(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f117,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( ~ m_and_h_gate_h_init_v_out(I0,I1,Y)| node9(I0,I1,X)| ~ node10(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f118,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( m_and_h_gate_h_init_v_out(I0,I1,Y)| ~ m_and_h_gate_h_init_v_out(I0,I1,X)| ~ node11(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f119,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( ~ m_and_h_gate_h_init_v_out(I0,I1,Y)| m_and_h_gate_h_init_v_out(I0,I1,X)| ~ node11(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f120,axiom,(
% 7.67/1.40 (![I0,I1,X,Y]: (( node10(I0,I1,X,Y)| node11(I0,I1,X,Y)| ~ trans(X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f128,axiom,(
% 7.67/1.40 (![I0,I1]: (~ m_c_h_element_v_out(I0,I1,s0) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f130,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( ~ m_c_h_element_v_out(I0,I1,Y)| m_c_h_element_v_in1(I0,I1,X)| ~ node14(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f132,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( ~ m_c_h_element_v_out(I0,I1,Y)| m_c_h_element_v_out(I0,I1,X)| ~ node15(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f133,axiom,(
% 7.67/1.40 (![I0,I1,X]: (( m_c_h_element_v_in1(I0,I1,X)| m_c_h_element_v_in2(I0,I1,X)| ~ node16(I0,I1,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f136,axiom,(
% 7.67/1.40 (![I0,I1,X]: (( ~ m_c_h_element_v_in1(I0,I1,X)| m_c_h_element_v_in2(I0,I1,X)| ~ node17(I0,I1,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f138,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( ~ m_c_h_element_v_out(I0,I1,Y)| m_c_h_element_v_out(I0,I1,X)| ~ node18(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f139,axiom,(
% 7.67/1.40 (![I0,I1,X,Y]: (( node14(I0,I1,X,Y)| node15(I0,I1,X,Y)| node16(I0,I1,X)| ~ node19(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f140,axiom,(
% 7.67/1.40 (![I0,I1,X,Y]: (( node17(I0,I1,X)| node18(I0,I1,X,Y)| ~ node19(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f141,axiom,(
% 7.67/1.40 (![X,Y,I0,I1]: (( ~ trans(X,Y)| node19(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f142,axiom,(
% 7.67/1.40 (![I0,I1]: (~ m_and_h_gate_v_out(I0,I1,s0) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f144,axiom,(
% 7.67/1.40 (![I0,I1,X]: (( m_and_h_gate_v_in2(I0,I1,X)| ~ node20(I0,I1,X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f146,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( ~ m_and_h_gate_v_out(I0,I1,Y)| node20(I0,I1,X)| ~ node21(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f148,axiom,(
% 7.67/1.40 (![I0,I1,Y,X]: (( ~ m_and_h_gate_v_out(I0,I1,Y)| m_and_h_gate_v_out(I0,I1,X)| ~ node22(I0,I1,X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f149,axiom,(
% 7.67/1.40 (![I0,I1,X,Y]: (( node21(I0,I1,X,Y)| node22(I0,I1,X,Y)| ~ trans(X,Y) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f150,negated_conjecture,(
% 7.67/1.40 (![X]: (( m_user_v_ack(c_e_h_1,c_u,X)| ~ node23(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f151,negated_conjecture,(
% 7.67/1.40 (![X]: (( m_user_v_ack(c_e_h_2,c_u,X)| ~ node23(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f152,negated_conjecture,(
% 7.67/1.40 (![X]: (( m_user_v_ack(c_e_h_1,c_u,X)| ~ node24(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f154,negated_conjecture,(
% 7.67/1.40 (![X]: (( m_user_v_ack(c_e_h_2,c_u,X)| ~ node25(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f156,negated_conjecture,(
% 7.67/1.40 (![X]: (( node23(X)| node24(X)| node25(X)| ~ node26(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f157,negated_conjecture,(
% 7.67/1.40 (![X]: (( node26(X)| xuntil28(X)| ~ until27(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f158,negated_conjecture,(
% 7.67/1.40 (![Y,X]: (( until27(Y)| ~ succ(X,Y)| ~ xuntil28(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f159,negated_conjecture,(
% 7.67/1.40 (![X]: (( loop| ~ last(X)| ~ xuntil28(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f160,negated_conjecture,(
% 7.67/1.40 (![Y,X]: (( until2p29(Y)| ~ trans(X,Y)| ~ last(X)| ~ xuntil28(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f161,negated_conjecture,(
% 7.67/1.40 (![X]: (( node26(X)| xuntil2p30(X)| ~ until2p29(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f162,negated_conjecture,(
% 7.67/1.40 (![Y,X]: (( until2p29(Y)| ~ succ(X,Y)| ~ xuntil2p30(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f163,negated_conjecture,(
% 7.67/1.40 (![X]: (( ~ last(X)| ~ xuntil2p30(X) ) ))),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f164,negated_conjecture,(
% 7.67/1.40 until27(s0) ),
% 7.67/1.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.67/1.40 fof(f165,plain,(
% 7.67/1.40 succ(s0,s1)),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f1])).
% 7.67/1.40 fof(f166,plain,(
% 7.67/1.40 succ(s1,s2)),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f2])).
% 7.67/1.40 fof(f167,plain,(
% 7.67/1.40 succ(s2,s3)),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f3])).
% 7.67/1.40 fof(f168,plain,(
% 7.67/1.40 succ(s3,s4)),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f4])).
% 7.67/1.40 fof(f169,plain,(
% 7.67/1.40 last(s4)),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f5])).
% 7.67/1.40 fof(f170,plain,(
% 7.67/1.40 ![X0,X1]: (~succ(X0,X1)|trans(X0,X1))),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f6])).
% 7.67/1.40 fof(f171,plain,(
% 7.67/1.40 ~loop|trans(s4,s0)|trans(s4,s1)|trans(s4,s2)|trans(s4,s3)|trans(s4,s4)),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f7])).
% 7.67/1.40 fof(f174,plain,(
% 7.67/1.40 ![X0]: (~m_cell_v_token(c_e_h_1,X0))),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f10])).
% 7.67/1.40 fof(f175,plain,(
% 7.67/1.40 m_cell_v_left(c_e_h_2,c_e_h_3)),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f11])).
% 7.67/1.40 fof(f177,plain,(
% 7.67/1.40 ![X0]: (~m_cell_v_token(c_e_h_2,X0))),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f13])).
% 7.67/1.40 fof(f199,plain,(
% 7.67/1.40 ![X0,X1]: (m_and_h_gate_v_in2(X0,c_d,X1)|m_user_v_ack(X0,c_u,X1))),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f33])).
% 7.67/1.40 fof(f200,plain,(
% 7.67/1.40 ![X0,X1]: (~m_and_h_gate_v_in2(X0,c_d,X1)|~m_user_v_ack(X0,c_u,X1))),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f34])).
% 7.67/1.40 fof(f204,plain,(
% 7.67/1.40 ![X0,X1]: (~m_c_h_element_v_in2(X0,c_e,X1)|m_and_h_gate_v_out(X0,c_i,X1))),
% 7.67/1.40 inference(cnf_transformation,[status(thm)],[f38])).
% 7.67/1.41 fof(f231,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_v_in2(X0,c_l,X1)|~m_and_h_gate_h_init_v_out(X0,c_m,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f65])).
% 7.67/1.41 fof(f232,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_v_in2(X0,c_l,X1)|m_and_h_gate_h_init_v_out(X0,c_m,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f66])).
% 7.67/1.41 fof(f233,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_in1(X0,c_m,X1)|m_c_h_element_v_out(X0,c_f,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f67])).
% 7.67/1.41 fof(f235,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_in2(X0,c_m,X1)|m_and_h_gate_h_init_v_out(X0,c_n,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f69])).
% 7.67/1.41 fof(f236,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_h_init_v_in2(X0,c_m,X1)|~m_and_h_gate_h_init_v_out(X0,c_n,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f70])).
% 7.67/1.41 fof(f237,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_init_h_out(X0,c_m,X1)|~m_cell_v_token(X0,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f71])).
% 7.67/1.41 fof(f238,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_h_init_v_init_h_out(X0,c_m,X1)|m_cell_v_token(X0,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f72])).
% 7.67/1.41 fof(f239,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_in1(X0,c_n,X1)|m_c_h_element_v_out(X0,c_e,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f73])).
% 7.67/1.41 fof(f241,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_in2(X0,c_n,X1)|m_and_h_gate_h_init_v_out(X0,c_m,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f75])).
% 7.67/1.41 fof(f243,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_init_h_out(X0,c_n,X1)|m_cell_v_token(X0,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f77])).
% 7.67/1.41 fof(f244,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_h_init_v_init_h_out(X0,c_n,X1)|~m_cell_v_token(X0,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f78])).
% 7.67/1.41 fof(f251,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_v_in2(X0,c_q,X1)|~m_and_h_gate_h_init_v_out(X0,c_n,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f85])).
% 7.67/1.41 fof(f252,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_v_in2(X0,c_q,X1)|m_and_h_gate_h_init_v_out(X0,c_n,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f86])).
% 7.67/1.41 fof(f254,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_v_in1(X0,c_r,X1)|m_c_h_element_v_out(X0,c_e,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f88])).
% 7.67/1.41 fof(f255,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_v_in2(X0,c_r,X1)|~m_and_h_gate_h_init_v_out(X0,c_m,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f89])).
% 7.67/1.41 fof(f256,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_v_in2(X0,c_r,X1)|m_and_h_gate_h_init_v_out(X0,c_m,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f90])).
% 7.67/1.41 fof(f260,plain,(
% 7.67/1.41 ![X0,X1,X2]: (~m_cell_v_ack(X0,X1)|m_and_h_gate_v_out(X2,c_q,X1)|~node3(X2,X0,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f94])).
% 7.67/1.41 fof(f261,plain,(
% 7.67/1.41 ![I0,J0]: (~m_cell_v_left(I0,J0)|(![X]: node3(I0,J0,X)))),
% 7.67/1.41 inference(miniscoping,[status(thm)],[f95])).
% 7.67/1.41 fof(f262,plain,(
% 7.67/1.41 ![X0,X1,X2]: (~m_cell_v_left(X0,X1)|node3(X0,X1,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f261])).
% 7.67/1.41 fof(f263,plain,(
% 7.67/1.41 ![X0,X1]: (m_user_v_ack(X0,c_u,X1)|~m_and_h_gate_v_out(X0,c_r,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f96])).
% 7.67/1.41 fof(f264,plain,(
% 7.67/1.41 ![X0,X1]: (~m_user_v_ack(X0,c_u,X1)|m_and_h_gate_v_out(X0,c_r,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f97])).
% 7.67/1.41 fof(f281,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_out(X0,X1,s0)|~m_and_h_gate_h_init_v_init_h_out(X0,X1,s0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f112])).
% 7.67/1.41 fof(f282,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_h_init_v_out(X0,X1,s0)|m_and_h_gate_h_init_v_init_h_out(X0,X1,s0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f113])).
% 7.67/1.41 fof(f284,plain,(
% 7.67/1.41 ![X0,X1,X2]: (m_and_h_gate_h_init_v_in2(X0,X1,X2)|~node9(X0,X1,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f115])).
% 7.67/1.41 fof(f285,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (m_and_h_gate_h_init_v_out(X0,X1,X2)|~m_and_h_gate_h_init_v_in1(X0,X1,X3)|~m_and_h_gate_h_init_v_in2(X0,X1,X3)|~node10(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f116])).
% 7.67/1.41 fof(f286,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (~m_and_h_gate_h_init_v_out(X0,X1,X2)|node9(X0,X1,X3)|~node10(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f117])).
% 7.67/1.41 fof(f287,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (m_and_h_gate_h_init_v_out(X0,X1,X2)|~m_and_h_gate_h_init_v_out(X0,X1,X3)|~node11(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f118])).
% 7.67/1.41 fof(f288,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (~m_and_h_gate_h_init_v_out(X0,X1,X2)|m_and_h_gate_h_init_v_out(X0,X1,X3)|~node11(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f119])).
% 7.67/1.41 fof(f289,plain,(
% 7.67/1.41 ![X,Y]: ((![I0,I1]: (node10(I0,I1,X,Y)|node11(I0,I1,X,Y)))|~trans(X,Y))),
% 7.67/1.41 inference(miniscoping,[status(thm)],[f120])).
% 7.67/1.41 fof(f290,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (node10(X0,X1,X2,X3)|node11(X0,X1,X2,X3)|~trans(X2,X3))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f289])).
% 7.67/1.41 fof(f300,plain,(
% 7.67/1.41 ![X0,X1]: (~m_c_h_element_v_out(X0,X1,s0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f128])).
% 7.67/1.41 fof(f302,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (~m_c_h_element_v_out(X0,X1,X2)|m_c_h_element_v_in1(X0,X1,X3)|~node14(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f130])).
% 7.67/1.41 fof(f304,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (~m_c_h_element_v_out(X0,X1,X2)|m_c_h_element_v_out(X0,X1,X3)|~node15(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f132])).
% 7.67/1.41 fof(f305,plain,(
% 7.67/1.41 ![X0,X1,X2]: (m_c_h_element_v_in1(X0,X1,X2)|m_c_h_element_v_in2(X0,X1,X2)|~node16(X0,X1,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f133])).
% 7.67/1.41 fof(f308,plain,(
% 7.67/1.41 ![X0,X1,X2]: (~m_c_h_element_v_in1(X0,X1,X2)|m_c_h_element_v_in2(X0,X1,X2)|~node17(X0,X1,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f136])).
% 7.67/1.41 fof(f310,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (~m_c_h_element_v_out(X0,X1,X2)|m_c_h_element_v_out(X0,X1,X3)|~node18(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f138])).
% 7.67/1.41 fof(f311,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (node14(X0,X1,X2,X3)|node15(X0,X1,X2,X3)|node16(X0,X1,X2)|~node19(X0,X1,X2,X3))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f139])).
% 7.67/1.41 fof(f312,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (node17(X0,X1,X2)|node18(X0,X1,X2,X3)|~node19(X0,X1,X2,X3))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f140])).
% 7.67/1.41 fof(f313,plain,(
% 7.67/1.41 ![X,Y]: (~trans(X,Y)|(![I0,I1]: node19(I0,I1,X,Y)))),
% 7.67/1.41 inference(miniscoping,[status(thm)],[f141])).
% 7.67/1.41 fof(f314,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (~trans(X0,X1)|node19(X2,X3,X0,X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f313])).
% 7.67/1.41 fof(f315,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_v_out(X0,X1,s0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f142])).
% 7.67/1.41 fof(f317,plain,(
% 7.67/1.41 ![X0,X1,X2]: (m_and_h_gate_v_in2(X0,X1,X2)|~node20(X0,X1,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f144])).
% 7.67/1.41 fof(f319,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (~m_and_h_gate_v_out(X0,X1,X2)|node20(X0,X1,X3)|~node21(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f146])).
% 7.67/1.41 fof(f321,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (~m_and_h_gate_v_out(X0,X1,X2)|m_and_h_gate_v_out(X0,X1,X3)|~node22(X0,X1,X3,X2))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f148])).
% 7.67/1.41 fof(f322,plain,(
% 7.67/1.41 ![X,Y]: ((![I0,I1]: (node21(I0,I1,X,Y)|node22(I0,I1,X,Y)))|~trans(X,Y))),
% 7.67/1.41 inference(miniscoping,[status(thm)],[f149])).
% 7.67/1.41 fof(f323,plain,(
% 7.67/1.41 ![X0,X1,X2,X3]: (node21(X0,X1,X2,X3)|node22(X0,X1,X2,X3)|~trans(X2,X3))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f322])).
% 7.67/1.41 fof(f324,plain,(
% 7.67/1.41 ![X0]: (m_user_v_ack(c_e_h_1,c_u,X0)|~node23(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f150])).
% 7.67/1.41 fof(f325,plain,(
% 7.67/1.41 ![X0]: (m_user_v_ack(c_e_h_2,c_u,X0)|~node23(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f151])).
% 7.67/1.41 fof(f326,plain,(
% 7.67/1.41 ![X0]: (m_user_v_ack(c_e_h_1,c_u,X0)|~node24(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f152])).
% 7.67/1.41 fof(f328,plain,(
% 7.67/1.41 ![X0]: (m_user_v_ack(c_e_h_2,c_u,X0)|~node25(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f154])).
% 7.67/1.41 fof(f330,plain,(
% 7.67/1.41 ![X0]: (node23(X0)|node24(X0)|node25(X0)|~node26(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f156])).
% 7.67/1.41 fof(f331,plain,(
% 7.67/1.41 ![X0]: (node26(X0)|xuntil28(X0)|~until27(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f157])).
% 7.67/1.41 fof(f332,plain,(
% 7.67/1.41 ![X]: ((![Y]: (until27(Y)|~succ(X,Y)))|~xuntil28(X))),
% 7.67/1.41 inference(miniscoping,[status(thm)],[f158])).
% 7.67/1.41 fof(f333,plain,(
% 7.67/1.41 ![X0,X1]: (until27(X0)|~succ(X1,X0)|~xuntil28(X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f332])).
% 7.67/1.41 fof(f334,plain,(
% 7.67/1.41 ![X0]: (loop|~last(X0)|~xuntil28(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f159])).
% 7.67/1.41 fof(f335,plain,(
% 7.67/1.41 ![X]: (((![Y]: (until2p29(Y)|~trans(X,Y)))|~last(X))|~xuntil28(X))),
% 7.67/1.41 inference(miniscoping,[status(thm)],[f160])).
% 7.67/1.41 fof(f336,plain,(
% 7.67/1.41 ![X0,X1]: (until2p29(X0)|~trans(X1,X0)|~last(X1)|~xuntil28(X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f335])).
% 7.67/1.41 fof(f337,plain,(
% 7.67/1.41 ![X0]: (node26(X0)|xuntil2p30(X0)|~until2p29(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f161])).
% 7.67/1.41 fof(f338,plain,(
% 7.67/1.41 ![X]: ((![Y]: (until2p29(Y)|~succ(X,Y)))|~xuntil2p30(X))),
% 7.67/1.41 inference(miniscoping,[status(thm)],[f162])).
% 7.67/1.41 fof(f339,plain,(
% 7.67/1.41 ![X0,X1]: (until2p29(X0)|~succ(X1,X0)|~xuntil2p30(X1))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f338])).
% 7.67/1.41 fof(f340,plain,(
% 7.67/1.41 ![X0]: (~last(X0)|~xuntil2p30(X0))),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f163])).
% 7.67/1.41 fof(f341,plain,(
% 7.67/1.41 until27(s0)),
% 7.67/1.41 inference(cnf_transformation,[status(thm)],[f164])).
% 7.67/1.41 fof(f342,definition,(
% 7.67/1.41 sQ0_spl <=> (loop)),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f345,definition,(
% 7.67/1.41 sQ1_spl <=> (trans(s4,s0))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f346,plain,(
% 7.67/1.41 trans(s4,s0)|~sQ1_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f345])).
% 7.67/1.41 fof(f348,definition,(
% 7.67/1.41 sQ2_spl <=> (trans(s4,s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f349,plain,(
% 7.67/1.41 trans(s4,s1)|~sQ2_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f348])).
% 7.67/1.41 fof(f351,definition,(
% 7.67/1.41 sQ3_spl <=> (trans(s4,s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f352,plain,(
% 7.67/1.41 trans(s4,s2)|~sQ3_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f351])).
% 7.67/1.41 fof(f354,definition,(
% 7.67/1.41 sQ4_spl <=> (trans(s4,s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f355,plain,(
% 7.67/1.41 trans(s4,s3)|~sQ4_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f354])).
% 7.67/1.41 fof(f357,definition,(
% 7.67/1.41 sQ5_spl <=> (trans(s4,s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f358,plain,(
% 7.67/1.41 trans(s4,s4)|~sQ5_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f357])).
% 7.67/1.41 fof(f360,plain,(
% 7.67/1.41 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ4_spl|sQ5_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f171,f342,f345,f348,f351,f354,f357])).
% 7.67/1.41 fof(f361,definition,(
% 7.67/1.41 ![X0]: (sQ6_spl <=> (~last(X0)|~xuntil28(X0)))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f362,plain,(
% 7.67/1.41 ![X0]: (~last(X0)|~xuntil28(X0)|~sQ6_spl)),
% 7.67/1.41 inference(component_clause,[status(thm)],[f361])).
% 7.67/1.41 fof(f364,plain,(
% 7.67/1.41 sQ0_spl|sQ6_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f334,f342,f361])).
% 7.67/1.41 fof(f366,plain,(
% 7.67/1.41 trans(s0,s1)),
% 7.67/1.41 inference(resolution,[status(thm)],[f165,f170])).
% 7.67/1.41 fof(f367,plain,(
% 7.67/1.41 trans(s1,s2)),
% 7.67/1.41 inference(resolution,[status(thm)],[f166,f170])).
% 7.67/1.41 fof(f368,plain,(
% 7.67/1.41 trans(s2,s3)),
% 7.67/1.41 inference(resolution,[status(thm)],[f167,f170])).
% 7.67/1.41 fof(f369,plain,(
% 7.67/1.41 trans(s3,s4)),
% 7.67/1.41 inference(resolution,[status(thm)],[f168,f170])).
% 7.67/1.41 fof(f370,plain,(
% 7.67/1.41 node26(s0)|xuntil28(s0)),
% 7.67/1.41 inference(resolution,[status(thm)],[f331,f341])).
% 7.67/1.41 fof(f371,definition,(
% 7.67/1.41 sQ7_spl <=> (node26(s0))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f372,plain,(
% 7.67/1.41 node26(s0)|~sQ7_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f371])).
% 7.67/1.41 fof(f374,definition,(
% 7.67/1.41 sQ8_spl <=> (xuntil28(s0))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f377,plain,(
% 7.67/1.41 sQ7_spl|sQ8_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f370,f371,f374])).
% 7.67/1.41 fof(f379,plain,(
% 7.67/1.41 until27(s4)|~xuntil28(s3)),
% 7.67/1.41 inference(resolution,[status(thm)],[f333,f168])).
% 7.67/1.41 fof(f380,plain,(
% 7.67/1.41 until27(s3)|~xuntil28(s2)),
% 7.67/1.41 inference(resolution,[status(thm)],[f333,f167])).
% 7.67/1.41 fof(f381,plain,(
% 7.67/1.41 until27(s2)|~xuntil28(s1)),
% 7.67/1.41 inference(resolution,[status(thm)],[f333,f166])).
% 7.67/1.41 fof(f382,plain,(
% 7.67/1.41 until27(s1)|~xuntil28(s0)),
% 7.67/1.41 inference(resolution,[status(thm)],[f333,f165])).
% 7.67/1.41 fof(f383,definition,(
% 7.67/1.41 sQ9_spl <=> (until27(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f384,plain,(
% 7.67/1.41 until27(s4)|~sQ9_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f383])).
% 7.67/1.41 fof(f386,definition,(
% 7.67/1.41 sQ10_spl <=> (xuntil28(s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f389,plain,(
% 7.67/1.41 sQ9_spl|~sQ10_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f379,f383,f386])).
% 7.67/1.41 fof(f390,definition,(
% 7.67/1.41 sQ11_spl <=> (until27(s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f391,plain,(
% 7.67/1.41 until27(s3)|~sQ11_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f390])).
% 7.67/1.41 fof(f393,definition,(
% 7.67/1.41 sQ12_spl <=> (xuntil28(s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f396,plain,(
% 7.67/1.41 sQ11_spl|~sQ12_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f380,f390,f393])).
% 7.67/1.41 fof(f397,definition,(
% 7.67/1.41 sQ13_spl <=> (until27(s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f398,plain,(
% 7.67/1.41 until27(s2)|~sQ13_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f397])).
% 7.67/1.41 fof(f400,definition,(
% 7.67/1.41 sQ14_spl <=> (xuntil28(s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f403,plain,(
% 7.67/1.41 sQ13_spl|~sQ14_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f381,f397,f400])).
% 7.67/1.41 fof(f404,definition,(
% 7.67/1.41 sQ15_spl <=> (until27(s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f405,plain,(
% 7.67/1.41 until27(s1)|~sQ15_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f404])).
% 7.67/1.41 fof(f407,plain,(
% 7.67/1.41 sQ15_spl|~sQ8_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f382,f404,f374])).
% 7.67/1.41 fof(f408,plain,(
% 7.67/1.41 until2p29(s4)|~xuntil2p30(s3)),
% 7.67/1.41 inference(resolution,[status(thm)],[f339,f168])).
% 7.67/1.41 fof(f409,plain,(
% 7.67/1.41 until2p29(s3)|~xuntil2p30(s2)),
% 7.67/1.41 inference(resolution,[status(thm)],[f339,f167])).
% 7.67/1.41 fof(f410,plain,(
% 7.67/1.41 until2p29(s2)|~xuntil2p30(s1)),
% 7.67/1.41 inference(resolution,[status(thm)],[f339,f166])).
% 7.67/1.41 fof(f411,plain,(
% 7.67/1.41 until2p29(s1)|~xuntil2p30(s0)),
% 7.67/1.41 inference(resolution,[status(thm)],[f339,f165])).
% 7.67/1.41 fof(f412,definition,(
% 7.67/1.41 sQ16_spl <=> (until2p29(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f413,plain,(
% 7.67/1.41 until2p29(s4)|~sQ16_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f412])).
% 7.67/1.41 fof(f415,definition,(
% 7.67/1.41 sQ17_spl <=> (xuntil2p30(s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f418,plain,(
% 7.67/1.41 sQ16_spl|~sQ17_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f408,f412,f415])).
% 7.67/1.41 fof(f419,definition,(
% 7.67/1.41 sQ18_spl <=> (until2p29(s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f420,plain,(
% 7.67/1.41 until2p29(s3)|~sQ18_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f419])).
% 7.67/1.41 fof(f422,definition,(
% 7.67/1.41 sQ19_spl <=> (xuntil2p30(s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f425,plain,(
% 7.67/1.41 sQ18_spl|~sQ19_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f409,f419,f422])).
% 7.67/1.41 fof(f426,definition,(
% 7.67/1.41 sQ20_spl <=> (until2p29(s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f427,plain,(
% 7.67/1.41 until2p29(s2)|~sQ20_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f426])).
% 7.67/1.41 fof(f429,definition,(
% 7.67/1.41 sQ21_spl <=> (xuntil2p30(s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f432,plain,(
% 7.67/1.41 sQ20_spl|~sQ21_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f410,f426,f429])).
% 7.67/1.41 fof(f433,definition,(
% 7.67/1.41 sQ22_spl <=> (until2p29(s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f434,plain,(
% 7.67/1.41 until2p29(s1)|~sQ22_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f433])).
% 7.67/1.41 fof(f436,definition,(
% 7.67/1.41 sQ23_spl <=> (xuntil2p30(s0))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f439,plain,(
% 7.67/1.41 sQ22_spl|~sQ23_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f411,f433,f436])).
% 7.67/1.41 fof(f440,plain,(
% 7.67/1.41 node23(s0)|node24(s0)|node25(s0)|~sQ7_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f372,f330])).
% 7.67/1.41 fof(f441,definition,(
% 7.67/1.41 sQ24_spl <=> (node23(s0))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f442,plain,(
% 7.67/1.41 node23(s0)|~sQ24_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f441])).
% 7.67/1.41 fof(f444,definition,(
% 7.67/1.41 sQ25_spl <=> (node24(s0))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f445,plain,(
% 7.67/1.41 node24(s0)|~sQ25_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f444])).
% 7.67/1.41 fof(f447,definition,(
% 7.67/1.41 sQ26_spl <=> (node25(s0))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f448,plain,(
% 7.67/1.41 node25(s0)|~sQ26_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f447])).
% 7.67/1.41 fof(f450,plain,(
% 7.67/1.41 sQ24_spl|sQ25_spl|sQ26_spl|~sQ7_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f440,f441,f444,f447,f371])).
% 7.67/1.41 fof(f451,plain,(
% 7.67/1.41 node26(s1)|xuntil28(s1)|~sQ15_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f405,f331])).
% 7.67/1.41 fof(f452,definition,(
% 7.67/1.41 sQ27_spl <=> (node26(s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f453,plain,(
% 7.67/1.41 node26(s1)|~sQ27_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f452])).
% 7.67/1.41 fof(f455,plain,(
% 7.67/1.41 sQ27_spl|sQ14_spl|~sQ15_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f451,f452,f400,f404])).
% 7.67/1.41 fof(f456,plain,(
% 7.67/1.41 node26(s2)|xuntil28(s2)|~sQ13_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f398,f331])).
% 7.67/1.41 fof(f457,definition,(
% 7.67/1.41 sQ28_spl <=> (node26(s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f458,plain,(
% 7.67/1.41 node26(s2)|~sQ28_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f457])).
% 7.67/1.41 fof(f460,plain,(
% 7.67/1.41 sQ28_spl|sQ12_spl|~sQ13_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f456,f457,f393,f397])).
% 7.67/1.41 fof(f461,plain,(
% 7.67/1.41 node26(s3)|xuntil28(s3)|~sQ11_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f391,f331])).
% 7.67/1.41 fof(f462,definition,(
% 7.67/1.41 sQ29_spl <=> (node26(s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f463,plain,(
% 7.67/1.41 node26(s3)|~sQ29_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f462])).
% 7.67/1.41 fof(f465,plain,(
% 7.67/1.41 sQ29_spl|sQ10_spl|~sQ11_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f461,f462,f386,f390])).
% 7.67/1.41 fof(f466,plain,(
% 7.67/1.41 node26(s4)|xuntil28(s4)|~sQ9_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f384,f331])).
% 7.67/1.41 fof(f467,definition,(
% 7.67/1.41 sQ30_spl <=> (node26(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f468,plain,(
% 7.67/1.41 node26(s4)|~sQ30_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f467])).
% 7.67/1.41 fof(f470,definition,(
% 7.67/1.41 sQ31_spl <=> (xuntil28(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f471,plain,(
% 7.67/1.41 xuntil28(s4)|~sQ31_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f470])).
% 7.67/1.41 fof(f473,plain,(
% 7.67/1.41 sQ30_spl|sQ31_spl|~sQ9_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f466,f467,f470,f383])).
% 7.67/1.41 fof(f474,plain,(
% 7.67/1.41 node26(s1)|xuntil2p30(s1)|~sQ22_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f434,f337])).
% 7.67/1.41 fof(f475,plain,(
% 7.67/1.41 sQ27_spl|sQ21_spl|~sQ22_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f474,f452,f429,f433])).
% 7.67/1.41 fof(f476,plain,(
% 7.67/1.41 node26(s2)|xuntil2p30(s2)|~sQ20_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f427,f337])).
% 7.67/1.41 fof(f477,plain,(
% 7.67/1.41 sQ28_spl|sQ19_spl|~sQ20_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f476,f457,f422,f426])).
% 7.67/1.41 fof(f478,plain,(
% 7.67/1.41 node26(s3)|xuntil2p30(s3)|~sQ18_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f420,f337])).
% 7.67/1.41 fof(f479,plain,(
% 7.67/1.41 sQ29_spl|sQ17_spl|~sQ18_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f478,f462,f415,f419])).
% 7.67/1.41 fof(f480,plain,(
% 7.67/1.41 node26(s4)|xuntil2p30(s4)|~sQ16_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f413,f337])).
% 7.67/1.41 fof(f481,definition,(
% 7.67/1.41 sQ32_spl <=> (xuntil2p30(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f482,plain,(
% 7.67/1.41 xuntil2p30(s4)|~sQ32_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f481])).
% 7.67/1.41 fof(f484,plain,(
% 7.67/1.41 sQ30_spl|sQ32_spl|~sQ16_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f480,f467,f481,f412])).
% 7.67/1.41 fof(f486,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_2,c_u,s0)|~sQ26_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f448,f328])).
% 7.67/1.41 fof(f488,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_1,c_u,s0)|~sQ25_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f445,f326])).
% 7.67/1.41 fof(f490,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_1,c_u,s0)|~sQ24_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f442,f324])).
% 7.67/1.41 fof(f491,plain,(
% 7.67/1.41 node23(s1)|node24(s1)|node25(s1)|~sQ27_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f453,f330])).
% 7.67/1.41 fof(f492,definition,(
% 7.67/1.41 sQ33_spl <=> (node23(s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f493,plain,(
% 7.67/1.41 node23(s1)|~sQ33_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f492])).
% 7.67/1.41 fof(f495,definition,(
% 7.67/1.41 sQ34_spl <=> (node24(s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f496,plain,(
% 7.67/1.41 node24(s1)|~sQ34_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f495])).
% 7.67/1.41 fof(f498,definition,(
% 7.67/1.41 sQ35_spl <=> (node25(s1))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f499,plain,(
% 7.67/1.41 node25(s1)|~sQ35_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f498])).
% 7.67/1.41 fof(f501,plain,(
% 7.67/1.41 sQ33_spl|sQ34_spl|sQ35_spl|~sQ27_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f491,f492,f495,f498,f452])).
% 7.67/1.41 fof(f502,plain,(
% 7.67/1.41 node23(s2)|node24(s2)|node25(s2)|~sQ28_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f458,f330])).
% 7.67/1.41 fof(f503,definition,(
% 7.67/1.41 sQ36_spl <=> (node23(s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f504,plain,(
% 7.67/1.41 node23(s2)|~sQ36_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f503])).
% 7.67/1.41 fof(f506,definition,(
% 7.67/1.41 sQ37_spl <=> (node24(s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f507,plain,(
% 7.67/1.41 node24(s2)|~sQ37_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f506])).
% 7.67/1.41 fof(f509,definition,(
% 7.67/1.41 sQ38_spl <=> (node25(s2))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f510,plain,(
% 7.67/1.41 node25(s2)|~sQ38_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f509])).
% 7.67/1.41 fof(f512,plain,(
% 7.67/1.41 sQ36_spl|sQ37_spl|sQ38_spl|~sQ28_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f502,f503,f506,f509,f457])).
% 7.67/1.41 fof(f513,plain,(
% 7.67/1.41 node23(s3)|node24(s3)|node25(s3)|~sQ29_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f463,f330])).
% 7.67/1.41 fof(f514,definition,(
% 7.67/1.41 sQ39_spl <=> (node23(s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f515,plain,(
% 7.67/1.41 node23(s3)|~sQ39_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f514])).
% 7.67/1.41 fof(f517,definition,(
% 7.67/1.41 sQ40_spl <=> (node24(s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f518,plain,(
% 7.67/1.41 node24(s3)|~sQ40_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f517])).
% 7.67/1.41 fof(f520,definition,(
% 7.67/1.41 sQ41_spl <=> (node25(s3))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f521,plain,(
% 7.67/1.41 node25(s3)|~sQ41_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f520])).
% 7.67/1.41 fof(f523,plain,(
% 7.67/1.41 sQ39_spl|sQ40_spl|sQ41_spl|~sQ29_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f513,f514,f517,f520,f462])).
% 7.67/1.41 fof(f524,plain,(
% 7.67/1.41 node23(s4)|node24(s4)|node25(s4)|~sQ30_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f468,f330])).
% 7.67/1.41 fof(f525,definition,(
% 7.67/1.41 sQ42_spl <=> (node23(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f526,plain,(
% 7.67/1.41 node23(s4)|~sQ42_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f525])).
% 7.67/1.41 fof(f528,definition,(
% 7.67/1.41 sQ43_spl <=> (node24(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f529,plain,(
% 7.67/1.41 node24(s4)|~sQ43_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f528])).
% 7.67/1.41 fof(f531,definition,(
% 7.67/1.41 sQ44_spl <=> (node25(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f532,plain,(
% 7.67/1.41 node25(s4)|~sQ44_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f531])).
% 7.67/1.41 fof(f534,plain,(
% 7.67/1.41 sQ42_spl|sQ43_spl|sQ44_spl|~sQ30_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f524,f525,f528,f531,f467])).
% 7.67/1.41 fof(f535,plain,(
% 7.67/1.41 ~last(s4)|~sQ31_spl|~sQ6_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f471,f362])).
% 7.67/1.41 fof(f536,plain,(
% 7.67/1.41 $false|~sQ31_spl|~sQ6_spl),
% 7.67/1.41 inference(forward_subsumption_resolution,[status(thm)],[f535,f169])).
% 7.67/1.41 fof(f537,plain,(
% 7.67/1.41 ~sQ31_spl|~sQ6_spl),
% 7.67/1.41 inference(contradiction_clause,[status(thm)],[f536])).
% 7.67/1.41 fof(f538,plain,(
% 7.67/1.41 ~last(s4)|~sQ32_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f482,f340])).
% 7.67/1.41 fof(f539,plain,(
% 7.67/1.41 $false|~sQ32_spl),
% 7.67/1.41 inference(forward_subsumption_resolution,[status(thm)],[f538,f169])).
% 7.67/1.41 fof(f540,plain,(
% 7.67/1.41 ~sQ32_spl),
% 7.67/1.41 inference(contradiction_clause,[status(thm)],[f539])).
% 7.67/1.41 fof(f542,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_2,c_u,s1)|~sQ35_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f499,f328])).
% 7.67/1.41 fof(f544,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_1,c_u,s1)|~sQ34_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f496,f326])).
% 7.67/1.41 fof(f546,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_1,c_u,s1)|~sQ33_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f493,f324])).
% 7.67/1.41 fof(f548,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_2,c_u,s2)|~sQ38_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f510,f328])).
% 7.67/1.41 fof(f550,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_1,c_u,s2)|~sQ37_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f507,f326])).
% 7.67/1.41 fof(f551,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_2,c_u,s2)|~sQ36_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f504,f325])).
% 7.67/1.41 fof(f554,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_2,c_u,s3)|~sQ41_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f521,f328])).
% 7.67/1.41 fof(f556,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_1,c_u,s3)|~sQ40_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f518,f326])).
% 7.67/1.41 fof(f557,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_2,c_u,s3)|~sQ39_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f515,f325])).
% 7.67/1.41 fof(f560,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_2,c_u,s4)|~sQ44_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f532,f328])).
% 7.67/1.41 fof(f562,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_1,c_u,s4)|~sQ43_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f529,f326])).
% 7.67/1.41 fof(f563,plain,(
% 7.67/1.41 m_user_v_ack(c_e_h_2,c_u,s4)|~sQ42_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f526,f325])).
% 7.67/1.41 fof(f566,plain,(
% 7.67/1.41 until2p29(s4)|~last(s4)|~xuntil28(s4)|~sQ5_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f358,f336])).
% 7.67/1.41 fof(f572,definition,(
% 7.67/1.41 sQ45_spl <=> (last(s4))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f574,plain,(
% 7.67/1.41 ~last(s4)|sQ45_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f572])).
% 7.67/1.41 fof(f575,plain,(
% 7.67/1.41 sQ16_spl|~sQ45_spl|~sQ31_spl|~sQ5_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f566,f412,f572,f470,f357])).
% 7.67/1.41 fof(f576,plain,(
% 7.67/1.41 $false|sQ45_spl),
% 7.67/1.41 inference(forward_subsumption_resolution,[status(thm)],[f574,f169])).
% 7.67/1.41 fof(f577,plain,(
% 7.67/1.41 sQ45_spl),
% 7.67/1.41 inference(contradiction_clause,[status(thm)],[f576])).
% 7.67/1.41 fof(f578,plain,(
% 7.67/1.41 until2p29(s3)|~last(s4)|~xuntil28(s4)|~sQ4_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f355,f336])).
% 7.67/1.41 fof(f584,plain,(
% 7.67/1.41 sQ18_spl|~sQ45_spl|~sQ31_spl|~sQ4_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f578,f419,f572,f470,f354])).
% 7.67/1.41 fof(f586,plain,(
% 7.67/1.41 ![X0,X1]: (node21(X0,X1,s0,s1)|node22(X0,X1,s0,s1))),
% 7.67/1.41 inference(resolution,[status(thm)],[f366,f323])).
% 7.67/1.41 fof(f588,plain,(
% 7.67/1.41 ![X0,X1]: (node10(X0,X1,s0,s1)|node11(X0,X1,s0,s1))),
% 7.67/1.41 inference(resolution,[status(thm)],[f366,f290])).
% 7.67/1.41 fof(f599,plain,(
% 7.67/1.41 until2p29(s2)|~last(s4)|~xuntil28(s4)|~sQ3_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f352,f336])).
% 7.67/1.41 fof(f605,plain,(
% 7.67/1.41 sQ20_spl|~sQ45_spl|~sQ31_spl|~sQ3_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f599,f426,f572,f470,f351])).
% 7.67/1.41 fof(f606,plain,(
% 7.67/1.41 until2p29(s1)|~last(s4)|~xuntil28(s4)|~sQ2_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f349,f336])).
% 7.67/1.41 fof(f612,plain,(
% 7.67/1.41 sQ22_spl|~sQ45_spl|~sQ31_spl|~sQ2_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f606,f433,f572,f470,f348])).
% 7.67/1.41 fof(f613,plain,(
% 7.67/1.41 until2p29(s0)|~last(s4)|~xuntil28(s4)|~sQ1_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f346,f336])).
% 7.67/1.41 fof(f619,definition,(
% 7.67/1.41 sQ47_spl <=> (until2p29(s0))),
% 7.67/1.41 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 7.67/1.41 fof(f620,plain,(
% 7.67/1.41 until2p29(s0)|~sQ47_spl),
% 7.67/1.41 inference(component_clause,[status(thm)],[f619])).
% 7.67/1.41 fof(f622,plain,(
% 7.67/1.41 sQ47_spl|~sQ45_spl|~sQ31_spl|~sQ1_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f613,f619,f572,f470,f345])).
% 7.67/1.41 fof(f623,plain,(
% 7.67/1.41 node26(s0)|xuntil2p30(s0)|~sQ47_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f620,f337])).
% 7.67/1.41 fof(f624,plain,(
% 7.67/1.41 sQ7_spl|sQ23_spl|~sQ47_spl),
% 7.67/1.41 inference(split_clause,[status(thm)],[f623,f371,f436,f619])).
% 7.67/1.41 fof(f629,plain,(
% 7.67/1.41 ![X0,X1]: (node21(X0,X1,s1,s2)|node22(X0,X1,s1,s2))),
% 7.67/1.41 inference(resolution,[status(thm)],[f367,f323])).
% 7.67/1.41 fof(f631,plain,(
% 7.67/1.41 ![X0,X1]: (node10(X0,X1,s1,s2)|node11(X0,X1,s1,s2))),
% 7.67/1.41 inference(resolution,[status(thm)],[f367,f290])).
% 7.67/1.41 fof(f639,plain,(
% 7.67/1.41 ![X0,X1]: (node21(X0,X1,s2,s3)|node22(X0,X1,s2,s3))),
% 7.67/1.41 inference(resolution,[status(thm)],[f368,f323])).
% 7.67/1.41 fof(f641,plain,(
% 7.67/1.41 ![X0,X1]: (node10(X0,X1,s2,s3)|node11(X0,X1,s2,s3))),
% 7.67/1.41 inference(resolution,[status(thm)],[f368,f290])).
% 7.67/1.41 fof(f649,plain,(
% 7.67/1.41 ![X0,X1]: (node21(X0,X1,s3,s4)|node22(X0,X1,s3,s4))),
% 7.67/1.41 inference(resolution,[status(thm)],[f369,f323])).
% 7.67/1.41 fof(f671,plain,(
% 7.67/1.41 ~m_and_h_gate_v_in2(c_e_h_1,c_d,s3)|~sQ40_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f200,f556])).
% 7.67/1.41 fof(f673,plain,(
% 7.67/1.41 ~m_and_h_gate_v_in2(c_e_h_1,c_d,s1)|~sQ34_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f200,f544])).
% 7.67/1.41 fof(f678,plain,(
% 7.67/1.41 ~m_and_h_gate_v_in2(c_e_h_2,c_d,s1)|~sQ35_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f200,f542])).
% 7.67/1.41 fof(f694,plain,(
% 7.67/1.41 ![X0]: (node3(c_e_h_2,c_e_h_3,X0))),
% 7.67/1.41 inference(resolution,[status(thm)],[f262,f175])).
% 7.67/1.41 fof(f711,plain,(
% 7.67/1.41 ![X0,X1]: (node19(X0,X1,s0,s1))),
% 7.67/1.41 inference(resolution,[status(thm)],[f314,f366])).
% 7.67/1.41 fof(f718,plain,(
% 7.67/1.41 ![X0]: (~m_cell_v_ack(c_e_h_3,X0)|m_and_h_gate_v_out(c_e_h_2,c_q,X0))),
% 7.67/1.41 inference(resolution,[status(thm)],[f260,f694])).
% 7.67/1.41 fof(f722,plain,(
% 7.67/1.41 m_and_h_gate_v_out(c_e_h_1,c_r,s2)|~sQ37_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f264,f550])).
% 7.67/1.41 fof(f724,plain,(
% 7.67/1.41 m_and_h_gate_v_out(c_e_h_1,c_r,s0)|~sQ25_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f264,f488])).
% 7.67/1.41 fof(f729,plain,(
% 7.67/1.41 m_and_h_gate_v_out(c_e_h_2,c_r,s0)|~sQ26_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f264,f486])).
% 7.67/1.41 fof(f735,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_v_out(X0,c_r,X1)|m_and_h_gate_v_in2(X0,c_d,X1))),
% 7.67/1.41 inference(resolution,[status(thm)],[f264,f199])).
% 7.67/1.41 fof(f736,plain,(
% 7.67/1.41 $false|~sQ25_spl),
% 7.67/1.41 inference(forward_subsumption_resolution,[status(thm)],[f724,f315])).
% 7.67/1.41 fof(f737,plain,(
% 7.67/1.41 ~sQ25_spl),
% 7.67/1.41 inference(contradiction_clause,[status(thm)],[f736])).
% 7.67/1.41 fof(f738,plain,(
% 7.67/1.41 $false|~sQ26_spl),
% 7.67/1.41 inference(forward_subsumption_resolution,[status(thm)],[f729,f315])).
% 7.67/1.41 fof(f739,plain,(
% 7.67/1.41 ~sQ26_spl),
% 7.67/1.41 inference(contradiction_clause,[status(thm)],[f738])).
% 7.67/1.41 fof(f879,plain,(
% 7.67/1.41 m_and_h_gate_v_out(c_e_h_1,c_r,s0)|~sQ24_spl),
% 7.67/1.41 inference(resolution,[status(thm)],[f490,f264])).
% 7.67/1.41 fof(f881,plain,(
% 7.67/1.41 $false|~sQ24_spl),
% 7.67/1.41 inference(forward_subsumption_resolution,[status(thm)],[f879,f315])).
% 7.67/1.41 fof(f882,plain,(
% 7.67/1.41 ~sQ24_spl),
% 7.67/1.41 inference(contradiction_clause,[status(thm)],[f881])).
% 7.67/1.41 fof(f905,plain,(
% 7.67/1.41 ![X0]: (m_and_h_gate_h_init_v_out(X0,c_n,s0)|m_cell_v_token(X0,s0))),
% 7.67/1.41 inference(resolution,[status(thm)],[f281,f243])).
% 7.67/1.41 fof(f963,plain,(
% 7.67/1.41 ![X0,X1]: (node17(X0,X1,s0)|node18(X0,X1,s0,s1))),
% 7.67/1.41 inference(resolution,[status(thm)],[f711,f312])).
% 7.67/1.41 fof(f964,plain,(
% 7.67/1.41 ![X0,X1]: (node14(X0,X1,s0,s1)|node15(X0,X1,s0,s1)|node16(X0,X1,s0))),
% 7.67/1.41 inference(resolution,[status(thm)],[f711,f311])).
% 7.67/1.41 fof(f1024,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_out(X0,X1,s2)|~m_and_h_gate_h_init_v_out(X0,X1,s1)|node10(X0,X1,s1,s2))),
% 7.67/1.41 inference(resolution,[status(thm)],[f287,f631])).
% 7.67/1.41 fof(f1026,plain,(
% 7.67/1.41 ![X0,X1]: (m_and_h_gate_h_init_v_out(X0,X1,s1)|~m_and_h_gate_h_init_v_out(X0,X1,s0)|node10(X0,X1,s0,s1))),
% 7.67/1.41 inference(resolution,[status(thm)],[f287,f588])).
% 7.67/1.41 fof(f1028,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_h_init_v_out(X0,X1,s3)|m_and_h_gate_h_init_v_out(X0,X1,s2)|node10(X0,X1,s2,s3))),
% 7.67/1.41 inference(resolution,[status(thm)],[f288,f641])).
% 7.67/1.41 fof(f1029,plain,(
% 7.67/1.41 ![X0,X1]: (~m_and_h_gate_h_init_v_out(X0,X1,s2)|m_and_h_gate_h_init_v_out(X0,X1,s1)|node10(X0,X1,s1,s2))),
% 7.67/1.41 inference(resolution,[status(thm)],[f288,f631])).
% 7.67/1.42 fof(f1031,plain,(
% 7.67/1.42 ![X0,X1]: (~m_and_h_gate_h_init_v_out(X0,X1,s1)|m_and_h_gate_h_init_v_out(X0,X1,s0)|node10(X0,X1,s0,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f288,f588])).
% 7.67/1.42 fof(f1067,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_h_init_v_out(X0,c_n,s1)|node10(X0,c_n,s0,s1)|m_cell_v_token(X0,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1026,f905])).
% 7.67/1.42 fof(f1093,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_h_init_v_out(X0,c_n,s1)|m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s1)|~m_and_h_gate_h_init_v_in1(X0,c_n,s0)|~m_and_h_gate_h_init_v_in2(X0,c_n,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1067,f285])).
% 7.67/1.42 fof(f1094,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_h_init_v_out(X0,c_n,s1)|m_cell_v_token(X0,s0)|~m_and_h_gate_h_init_v_in1(X0,c_n,s0)|~m_and_h_gate_h_init_v_in2(X0,c_n,s0))),
% 7.67/1.42 inference(duplicate_literals_removal,[status(thm)],[f1093])).
% 7.67/1.42 fof(f1107,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_h_init_v_out(X0,c_n,s1)|m_cell_v_token(X0,s0)|~m_and_h_gate_h_init_v_in1(X0,c_n,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1094,f241])).
% 7.67/1.42 fof(f1118,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_h_init_v_out(X0,c_n,s1)|m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_c_h_element_v_out(X0,c_e,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1107,f239])).
% 7.67/1.42 fof(f1119,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_h_init_v_out(X0,c_n,s1)|m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1118,f300])).
% 7.67/1.42 fof(f1120,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_v_in2(X0,c_q,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1119,f251])).
% 7.67/1.42 fof(f1124,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|node10(X0,c_n,s1,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1119,f1024])).
% 7.67/1.42 fof(f1128,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1120,f282])).
% 7.67/1.42 fof(f1129,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1128,f237])).
% 7.67/1.42 fof(f1130,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_cell_v_token(X0,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1129,f238])).
% 7.67/1.42 fof(f1131,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1129,f281])).
% 7.67/1.42 fof(f1132,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1130,f252])).
% 7.67/1.42 fof(f1137,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|node10(X0,c_n,s1,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1132,f1024])).
% 7.67/1.42 fof(f1177,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|~m_and_h_gate_h_init_v_in1(X0,c_n,s1)|~m_and_h_gate_h_init_v_in2(X0,c_n,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1124,f285])).
% 7.67/1.42 fof(f1178,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|~m_and_h_gate_h_init_v_in1(X0,c_n,s1)|~m_and_h_gate_h_init_v_in2(X0,c_n,s1))),
% 7.67/1.42 inference(duplicate_literals_removal,[status(thm)],[f1177])).
% 7.67/1.42 fof(f1257,plain,(
% 7.67/1.42 ![X0,X1]: (~m_c_h_element_v_out(X0,X1,s1)|m_c_h_element_v_out(X0,X1,s0)|node14(X0,X1,s0,s1)|node16(X0,X1,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f304,f964])).
% 7.67/1.42 fof(f1261,plain,(
% 7.67/1.42 ![X0,X1]: (~m_c_h_element_v_out(X0,X1,s1)|node14(X0,X1,s0,s1)|node16(X0,X1,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1257,f300])).
% 7.67/1.42 fof(f1267,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_v_in2(X0,c_l,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1131,f231])).
% 7.67/1.42 fof(f1268,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|node10(X0,c_m,s0,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1131,f1026])).
% 7.67/1.42 fof(f1272,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_l,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1267,f252])).
% 7.67/1.42 fof(f1312,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|~m_and_h_gate_h_init_v_in1(X0,c_n,s1)|~m_and_h_gate_h_init_v_in2(X0,c_n,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1137,f285])).
% 7.67/1.42 fof(f1313,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|~m_and_h_gate_h_init_v_in1(X0,c_n,s1)|~m_and_h_gate_h_init_v_in2(X0,c_n,s1))),
% 7.67/1.42 inference(duplicate_literals_removal,[status(thm)],[f1312])).
% 7.67/1.42 fof(f1325,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_in1(X0,c_m,s0)|~m_and_h_gate_h_init_v_in2(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1268,f285])).
% 7.67/1.42 fof(f1326,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_in1(X0,c_m,s0)|~m_and_h_gate_h_init_v_in2(X0,c_m,s0))),
% 7.67/1.42 inference(duplicate_literals_removal,[status(thm)],[f1325])).
% 7.67/1.42 fof(f1408,plain,(
% 7.67/1.42 ![X0,X1]: (~m_c_h_element_v_out(X0,X1,s1)|m_c_h_element_v_out(X0,X1,s0)|node17(X0,X1,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f310,f963])).
% 7.67/1.42 fof(f1412,plain,(
% 7.67/1.42 ![X0,X1]: (~m_c_h_element_v_out(X0,X1,s1)|node17(X0,X1,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1408,f300])).
% 7.67/1.42 fof(f1417,plain,(
% 7.67/1.42 ![X0,X1]: (~m_and_h_gate_v_out(X0,X1,s4)|m_and_h_gate_v_out(X0,X1,s3)|node21(X0,X1,s3,s4))),
% 7.67/1.42 inference(resolution,[status(thm)],[f321,f649])).
% 7.67/1.42 fof(f1418,plain,(
% 7.67/1.42 ![X0,X1]: (~m_and_h_gate_v_out(X0,X1,s3)|m_and_h_gate_v_out(X0,X1,s2)|node21(X0,X1,s2,s3))),
% 7.67/1.42 inference(resolution,[status(thm)],[f321,f639])).
% 7.67/1.42 fof(f1419,plain,(
% 7.67/1.42 ![X0,X1]: (~m_and_h_gate_v_out(X0,X1,s2)|m_and_h_gate_v_out(X0,X1,s1)|node21(X0,X1,s1,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f321,f629])).
% 7.67/1.42 fof(f1420,plain,(
% 7.67/1.42 ![X0,X1]: (~m_and_h_gate_v_out(X0,X1,s1)|m_and_h_gate_v_out(X0,X1,s0)|node21(X0,X1,s0,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f321,f586])).
% 7.67/1.42 fof(f1421,plain,(
% 7.67/1.42 ![X0,X1]: (~m_and_h_gate_v_out(X0,X1,s1)|node21(X0,X1,s0,s1))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1420,f315])).
% 7.67/1.42 fof(f1503,definition,(
% 7.67/1.42 sQ77_spl <=> (m_and_h_gate_v_out(c_e_h_2,c_r,s2))),
% 7.67/1.42 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 7.67/1.42 fof(f1504,plain,(
% 7.67/1.42 m_and_h_gate_v_out(c_e_h_2,c_r,s2)|~sQ77_spl),
% 7.67/1.42 inference(component_clause,[status(thm)],[f1503])).
% 7.67/1.42 fof(f1510,definition,(
% 7.67/1.42 sQ79_spl <=> (m_and_h_gate_v_out(c_e_h_1,c_r,s2))),
% 7.67/1.42 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 7.67/1.42 fof(f1511,plain,(
% 7.67/1.42 m_and_h_gate_v_out(c_e_h_1,c_r,s2)|~sQ79_spl),
% 7.67/1.42 inference(component_clause,[status(thm)],[f1510])).
% 7.67/1.42 fof(f1566,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s3)|node21(X0,c_r,s3,s4)|m_and_h_gate_v_in2(X0,c_d,s4))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1417,f735])).
% 7.67/1.42 fof(f1567,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s2)|node21(X0,c_r,s2,s3)|m_and_h_gate_v_in2(X0,c_d,s3))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1418,f735])).
% 7.67/1.42 fof(f1568,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s1)|node21(X0,c_r,s1,s2)|m_and_h_gate_v_in2(X0,c_d,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1419,f735])).
% 7.67/1.42 fof(f1610,plain,(
% 7.67/1.42 m_and_h_gate_v_out(c_e_h_2,c_r,s2)|~sQ36_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f551,f264])).
% 7.67/1.42 fof(f1668,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s3)|m_and_h_gate_v_in2(X0,c_d,s4)|~m_and_h_gate_v_out(X0,c_r,s4)|node20(X0,c_r,s3))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1566,f319])).
% 7.67/1.42 fof(f1670,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s3)|m_and_h_gate_v_in2(X0,c_d,s4)|node20(X0,c_r,s3))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1668,f735])).
% 7.67/1.42 fof(f1671,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s2)|m_and_h_gate_v_in2(X0,c_d,s3)|~m_and_h_gate_v_out(X0,c_r,s3)|node20(X0,c_r,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1567,f319])).
% 7.67/1.42 fof(f1673,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s2)|m_and_h_gate_v_in2(X0,c_d,s3)|node20(X0,c_r,s2))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1671,f735])).
% 7.67/1.42 fof(f1674,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s1)|m_and_h_gate_v_in2(X0,c_d,s2)|~m_and_h_gate_v_out(X0,c_r,s2)|node20(X0,c_r,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1568,f319])).
% 7.67/1.42 fof(f1676,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s1)|m_and_h_gate_v_in2(X0,c_d,s2)|node20(X0,c_r,s1))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1674,f735])).
% 7.67/1.42 fof(f1696,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s3)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1670,f317])).
% 7.67/1.42 fof(f1698,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s2)|m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1673,f317])).
% 7.67/1.42 fof(f1700,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_out(X0,c_r,s1)|m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1676,f317])).
% 7.67/1.42 fof(f1712,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|m_user_v_ack(X0,c_u,s3))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1696,f263])).
% 7.67/1.42 fof(f1713,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|m_and_h_gate_v_out(X0,c_r,s2)|node21(X0,c_r,s2,s3))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1696,f1418])).
% 7.67/1.42 fof(f1756,plain,(
% 7.67/1.42 ~m_and_h_gate_v_in2(c_e_h_1,c_d,s1)|~sQ33_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f546,f200])).
% 7.67/1.42 fof(f1757,plain,(
% 7.67/1.42 m_user_v_ack(c_e_h_1,c_u,s2)|~sQ79_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f1511,f263])).
% 7.67/1.42 fof(f1781,plain,(
% 7.67/1.42 m_user_v_ack(c_e_h_2,c_u,s2)|~sQ77_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f1504,f263])).
% 7.67/1.42 fof(f1849,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_v_out(X0,c_r,s1)|node21(X0,c_r,s1,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1698,f1419])).
% 7.67/1.42 fof(f1854,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s1)|m_user_v_ack(X0,c_u,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1700,f263])).
% 7.67/1.42 fof(f1859,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|~m_and_h_gate_v_in2(X0,c_d,s3))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1712,f200])).
% 7.67/1.42 fof(f1867,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s1)|~m_and_h_gate_v_in2(X0,c_d,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1854,f200])).
% 7.67/1.42 fof(f1885,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|m_and_h_gate_v_out(X0,c_r,s2)|~m_and_h_gate_v_out(X0,c_r,s3)|node20(X0,c_r,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1713,f319])).
% 7.67/1.42 fof(f1887,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|m_and_h_gate_v_out(X0,c_r,s2)|node20(X0,c_r,s2))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1885,f1696])).
% 7.67/1.42 fof(f1924,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_v_out(X0,c_r,s1)|~m_and_h_gate_v_out(X0,c_r,s2)|node20(X0,c_r,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1849,f319])).
% 7.67/1.42 fof(f1926,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_v_out(X0,c_r,s1)|node20(X0,c_r,s1))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f1924,f1698])).
% 7.67/1.42 fof(f2007,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|m_and_h_gate_v_out(X0,c_r,s2)|m_and_h_gate_v_in2(X0,c_r,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1887,f317])).
% 7.67/1.42 fof(f2100,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_v_out(X0,c_r,s1)|m_and_h_gate_v_in2(X0,c_r,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1926,f317])).
% 7.67/1.42 fof(f2187,plain,(
% 7.67/1.42 ![X0]: (node21(X0,c_r,s0,s1)|m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1421,f1700])).
% 7.67/1.42 fof(f2188,plain,(
% 7.67/1.42 ![X0]: (node21(X0,c_r,s0,s1)|m_and_h_gate_v_in2(X0,c_d,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1421,f735])).
% 7.67/1.42 fof(f2236,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|~m_and_h_gate_v_out(X0,c_r,s1)|node20(X0,c_r,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2188,f319])).
% 7.67/1.42 fof(f2238,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|node20(X0,c_r,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f2236,f735])).
% 7.67/1.42 fof(f2239,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_v_in2(X0,c_r,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2238,f317])).
% 7.67/1.42 fof(f2241,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2239,f256])).
% 7.67/1.42 fof(f2247,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|node10(X0,c_m,s0,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2241,f1026])).
% 7.67/1.42 fof(f2248,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2241,f282])).
% 7.67/1.42 fof(f2250,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_cell_v_token(X0,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2248,f238])).
% 7.67/1.42 fof(f2428,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s1)|~m_and_h_gate_v_out(X0,c_r,s1)|node20(X0,c_r,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2187,f319])).
% 7.67/1.42 fof(f2430,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s1)|node20(X0,c_r,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f2428,f1700])).
% 7.67/1.42 fof(f2439,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_in1(X0,c_m,s0)|~m_and_h_gate_h_init_v_in2(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2247,f285])).
% 7.67/1.42 fof(f2440,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_in1(X0,c_m,s0)|~m_and_h_gate_h_init_v_in2(X0,c_m,s0))),
% 7.67/1.42 inference(duplicate_literals_removal,[status(thm)],[f2439])).
% 7.67/1.42 fof(f2451,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s1)|m_and_h_gate_v_in2(X0,c_r,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2430,f317])).
% 7.67/1.42 fof(f2457,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|~m_and_h_gate_h_init_v_in1(X0,c_n,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1178,f241])).
% 7.67/1.42 fof(f2513,plain,(
% 7.67/1.42 m_and_h_gate_v_out(c_e_h_2,c_r,s2)|~sQ38_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f548,f264])).
% 7.67/1.42 fof(f2541,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|m_user_v_ack(X0,c_u,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2007,f263])).
% 7.67/1.42 fof(f2560,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_v_in2(X0,c_r,s1)|m_user_v_ack(X0,c_u,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2100,f263])).
% 7.67/1.42 fof(f2573,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2451,f256])).
% 7.67/1.42 fof(f2733,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node10(X0,c_m,s0,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2573,f1031])).
% 7.67/1.42 fof(f2735,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node10(X0,c_m,s0,s1))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f2733,f256])).
% 7.67/1.42 fof(f2780,definition,(
% 7.67/1.42 sQ101_spl <=> (m_and_h_gate_v_in1(c_e_h_2,c_r,s0))),
% 7.67/1.42 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 7.67/1.42 fof(f2781,plain,(
% 7.67/1.42 m_and_h_gate_v_in1(c_e_h_2,c_r,s0)|~sQ101_spl),
% 7.67/1.42 inference(component_clause,[status(thm)],[f2780])).
% 7.67/1.42 fof(f2787,definition,(
% 7.67/1.42 sQ103_spl <=> (m_cell_v_token(c_e_h_2,s0))),
% 7.67/1.42 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 7.67/1.42 fof(f2788,plain,(
% 7.67/1.42 m_cell_v_token(c_e_h_2,s0)|~sQ103_spl),
% 7.67/1.42 inference(component_clause,[status(thm)],[f2787])).
% 7.67/1.42 fof(f2791,plain,(
% 7.67/1.42 $false|~sQ103_spl),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f2788,f177])).
% 7.67/1.42 fof(f2792,plain,(
% 7.67/1.42 ~sQ103_spl),
% 7.67/1.42 inference(contradiction_clause,[status(thm)],[f2791])).
% 7.67/1.42 fof(f2962,plain,(
% 7.67/1.42 ~m_and_h_gate_v_in2(c_e_h_2,c_d,s2)|~sQ77_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f1781,f200])).
% 7.67/1.42 fof(f3013,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_in1(X0,c_m,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2440,f235])).
% 7.67/1.42 fof(f3035,plain,(
% 7.67/1.42 m_cell_v_token(c_e_h_2,s0)|~sQ35_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f678,f2250])).
% 7.67/1.42 fof(f3037,plain,(
% 7.67/1.42 sQ103_spl|~sQ35_spl),
% 7.67/1.42 inference(split_clause,[status(thm)],[f3035,f2787,f498])).
% 7.67/1.42 fof(f3195,plain,(
% 7.67/1.42 ~m_and_h_gate_v_in2(c_e_h_1,c_d,s2)|~sQ79_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f1757,f200])).
% 7.67/1.42 fof(f3475,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_c_h_element_v_out(X0,c_e,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2457,f239])).
% 7.67/1.42 fof(f3492,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|~m_and_h_gate_v_in2(X0,c_d,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2541,f200])).
% 7.67/1.42 fof(f3552,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_v_in2(X0,c_r,s1)|~m_and_h_gate_v_in2(X0,c_d,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2560,f200])).
% 7.67/1.42 fof(f3601,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|~m_and_h_gate_h_init_v_out(X0,c_m,s1)|node9(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f2735,f286])).
% 7.67/1.42 fof(f3623,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_out(X0,c_n,s0)|m_c_h_element_v_out(X0,c_f,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3013,f233])).
% 7.67/1.42 fof(f3624,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_out(X0,c_n,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3623,f300])).
% 7.67/1.42 fof(f3659,plain,(
% 7.67/1.42 ~m_and_h_gate_v_in2(c_e_h_2,c_d,s3)|~sQ39_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f557,f200])).
% 7.67/1.42 fof(f3679,plain,(
% 7.67/1.42 ~m_and_h_gate_v_in2(c_e_h_2,c_d,s4)|~sQ42_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f563,f200])).
% 7.67/1.42 fof(f3700,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_init_h_out(X0,c_n,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3624,f282])).
% 7.67/1.42 fof(f3709,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_cell_v_token(X0,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3700,f244])).
% 7.67/1.42 fof(f3711,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3709,f2250])).
% 7.67/1.42 fof(f3735,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s1)|m_and_h_gate_v_in2(X0,c_r,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3711,f255])).
% 7.67/1.42 fof(f3739,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_v_in2(X0,c_r,s1))),
% 7.67/1.42 inference(backward_subsumption_resolution,[status(thm)],[f1867,f3735])).
% 7.67/1.42 fof(f3743,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3739,f256])).
% 7.67/1.42 fof(f3755,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3475,f251])).
% 7.67/1.42 fof(f3789,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|~m_and_h_gate_h_init_v_in1(X0,c_n,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1313,f241])).
% 7.67/1.42 fof(f3795,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_v_in2(X0,c_r,s1))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3552,f3735])).
% 7.67/1.42 fof(f3797,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3795,f256])).
% 7.67/1.42 fof(f3820,plain,(
% 7.67/1.42 m_cell_v_token(c_e_h_1,s0)|~sQ33_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f1756,f2250])).
% 7.67/1.42 fof(f3822,plain,(
% 7.67/1.42 $false|~sQ33_spl),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3820,f174])).
% 7.67/1.42 fof(f3823,plain,(
% 7.67/1.42 ~sQ33_spl),
% 7.67/1.42 inference(contradiction_clause,[status(thm)],[f3822])).
% 7.67/1.42 fof(f3832,definition,(
% 7.67/1.42 sQ124_spl <=> (m_cell_v_token(c_e_h_1,s0))),
% 7.67/1.42 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 7.67/1.42 fof(f3833,plain,(
% 7.67/1.42 m_cell_v_token(c_e_h_1,s0)|~sQ124_spl),
% 7.67/1.42 inference(component_clause,[status(thm)],[f3832])).
% 7.67/1.42 fof(f3842,definition,(
% 7.67/1.42 sQ127_spl <=> (m_and_h_gate_v_in1(c_e_h_1,c_r,s0))),
% 7.67/1.42 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 7.67/1.42 fof(f3843,plain,(
% 7.67/1.42 m_and_h_gate_v_in1(c_e_h_1,c_r,s0)|~sQ127_spl),
% 7.67/1.42 inference(component_clause,[status(thm)],[f3842])).
% 7.67/1.42 fof(f3846,plain,(
% 7.67/1.42 $false|~sQ124_spl),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3833,f174])).
% 7.67/1.42 fof(f3847,plain,(
% 7.67/1.42 ~sQ124_spl),
% 7.67/1.42 inference(contradiction_clause,[status(thm)],[f3846])).
% 7.67/1.42 fof(f3851,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s1)|m_and_h_gate_v_in2(X0,c_l,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3797,f231])).
% 7.67/1.42 fof(f3852,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_r,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|node10(X0,c_m,s1,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3797,f1029])).
% 7.67/1.42 fof(f3854,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|node10(X0,c_m,s1,s2))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3852,f256])).
% 7.67/1.42 fof(f3859,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3851,f256])).
% 7.67/1.42 fof(f3878,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s2)|m_and_h_gate_v_in2(X0,c_l,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3859,f231])).
% 7.67/1.42 fof(f3882,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3878,f232])).
% 7.67/1.42 fof(f3890,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_out(X0,c_m,s2)|node9(X0,c_m,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3854,f286])).
% 7.67/1.42 fof(f3905,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_in1(X0,c_m,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f1326,f235])).
% 7.67/1.42 fof(f3917,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node9(X0,c_m,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3601,f3743])).
% 7.67/1.42 fof(f3918,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_in2(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3917,f284])).
% 7.67/1.42 fof(f3927,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|~m_and_h_gate_h_init_v_out(X0,c_n,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3918,f236])).
% 7.67/1.42 fof(f3930,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_cell_v_token(X0,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3927,f905])).
% 7.67/1.42 fof(f3934,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3930,f282])).
% 7.67/1.42 fof(f3935,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3934,f237])).
% 7.67/1.42 fof(f3936,plain,(
% 7.67/1.42 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s2)|m_cell_v_token(X0,s0))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3935,f238])).
% 7.67/1.42 fof(f3941,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3)|m_and_h_gate_v_in2(X0,c_r,s2))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3936,f3492])).
% 7.67/1.42 fof(f4014,plain,(
% 7.67/1.42 m_c_h_element_v_out(c_e_h_2,c_e,s0)|~sQ101_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f2781,f254])).
% 7.67/1.42 fof(f4015,plain,(
% 7.67/1.42 $false|~sQ101_spl),
% 7.67/1.42 inference(forward_subsumption_resolution,[status(thm)],[f4014,f300])).
% 7.67/1.42 fof(f4016,plain,(
% 7.67/1.42 ~sQ101_spl),
% 7.67/1.42 inference(contradiction_clause,[status(thm)],[f4015])).
% 7.67/1.42 fof(f4017,plain,(
% 7.67/1.42 m_cell_v_token(c_e_h_2,s0)|~sQ77_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f2962,f3936])).
% 7.67/1.42 fof(f4019,plain,(
% 7.67/1.42 sQ103_spl|~sQ77_spl),
% 7.67/1.42 inference(split_clause,[status(thm)],[f4017,f2787,f1503])).
% 7.67/1.42 fof(f4163,plain,(
% 7.67/1.42 ~m_and_h_gate_v_in2(c_e_h_2,c_d,s3)|~sQ41_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f554,f200])).
% 7.67/1.42 fof(f4344,plain,(
% 7.67/1.42 m_cell_v_token(c_e_h_1,s0)|~sQ79_spl),
% 7.67/1.42 inference(resolution,[status(thm)],[f3195,f3936])).
% 7.67/1.42 fof(f4346,plain,(
% 7.67/1.42 sQ124_spl|~sQ79_spl),
% 7.67/1.42 inference(split_clause,[status(thm)],[f4344,f3832,f1510])).
% 7.67/1.42 fof(f4504,plain,(
% 7.67/1.42 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_c_h_element_v_out(X0,c_e,s1))),
% 7.67/1.42 inference(resolution,[status(thm)],[f3789,f239])).
% 7.67/1.42 fof(f4521,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s3))),
% 7.67/1.43 inference(resolution,[status(thm)],[f3941,f256])).
% 7.67/1.43 fof(f4609,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2))),
% 7.67/1.43 inference(resolution,[status(thm)],[f4504,f251])).
% 7.67/1.43 fof(f4726,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node10(X0,c_m,s0,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f3755,f1031])).
% 7.67/1.43 fof(f4728,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|node10(X0,c_m,s0,s1))),
% 7.67/1.43 inference(duplicate_literals_removal,[status(thm)],[f4726])).
% 7.67/1.43 fof(f4745,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s2)|m_and_h_gate_h_init_v_out(X0,c_m,s2)|node10(X0,c_m,s2,s3))),
% 7.67/1.43 inference(resolution,[status(thm)],[f4521,f1028])).
% 7.67/1.43 fof(f4747,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s2)|node10(X0,c_m,s2,s3))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f4745,f256])).
% 7.67/1.43 fof(f5052,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|node9(X0,c_m,s1)|m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f3890,f3882])).
% 7.67/1.43 fof(f5058,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|node9(X0,c_m,s1)|m_and_h_gate_v_in2(X0,c_l,s1))),
% 7.67/1.43 inference(duplicate_literals_removal,[status(thm)],[f5052])).
% 7.67/1.43 fof(f5059,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|node9(X0,c_m,s1)|m_and_h_gate_v_in2(X0,c_l,s1))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5058,f231])).
% 7.67/1.43 fof(f5063,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s1)|m_and_h_gate_h_init_v_in2(X0,c_m,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5059,f284])).
% 7.67/1.43 fof(f5070,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s1)|~m_and_h_gate_h_init_v_out(X0,c_n,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5063,f236])).
% 7.67/1.43 fof(f5099,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s1)|m_and_h_gate_v_in2(X0,c_l,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5070,f1272])).
% 7.67/1.43 fof(f5109,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5099,f232])).
% 7.67/1.43 fof(f5113,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node10(X0,c_m,s0,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5109,f1031])).
% 7.67/1.43 fof(f5115,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node10(X0,c_m,s0,s1))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5113,f232])).
% 7.67/1.43 fof(f5147,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_out(X0,c_n,s0)|m_c_h_element_v_out(X0,c_f,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f3905,f233])).
% 7.67/1.43 fof(f5149,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_out(X0,c_n,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5147,f300])).
% 7.67/1.43 fof(f5188,plain,(
% 7.67/1.43 m_c_h_element_v_out(c_e_h_1,c_e,s0)|~sQ127_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f3843,f254])).
% 7.67/1.43 fof(f5189,plain,(
% 7.67/1.43 $false|~sQ127_spl),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5188,f300])).
% 7.67/1.43 fof(f5190,plain,(
% 7.67/1.43 ~sQ127_spl),
% 7.67/1.43 inference(contradiction_clause,[status(thm)],[f5189])).
% 7.67/1.43 fof(f5194,definition,(
% 7.67/1.43 sQ148_spl <=> (m_and_h_gate_v_in1(c_e_h_3,c_r,s0))),
% 7.67/1.43 introduced(definition,[new_symbols(definition,[sQ148_spl])],[split_symbol_definition])).
% 7.67/1.43 fof(f5195,plain,(
% 7.67/1.43 m_and_h_gate_v_in1(c_e_h_3,c_r,s0)|~sQ148_spl),
% 7.67/1.43 inference(component_clause,[status(thm)],[f5194])).
% 7.67/1.43 fof(f5201,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_init_h_out(X0,c_n,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5149,f282])).
% 7.67/1.43 fof(f5226,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_cell_v_token(X0,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5201,f244])).
% 7.67/1.43 fof(f5228,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5226,f1130])).
% 7.67/1.43 fof(f5230,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s1)|m_and_h_gate_v_in2(X0,c_l,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5228,f231])).
% 7.67/1.43 fof(f5234,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_l,s1)|m_and_h_gate_h_init_v_out(X0,c_n,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5230,f252])).
% 7.67/1.43 fof(f5235,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_v_in2(X0,c_l,s1))),
% 7.67/1.43 inference(backward_subsumption_resolution,[status(thm)],[f5070,f5234])).
% 7.67/1.43 fof(f5241,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5235,f232])).
% 7.67/1.43 fof(f5331,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|~m_and_h_gate_h_init_v_out(X0,c_m,s1)|node9(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5115,f286])).
% 7.67/1.43 fof(f5333,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node9(X0,c_m,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5331,f5241])).
% 7.67/1.43 fof(f5334,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_in2(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5333,f284])).
% 7.67/1.43 fof(f5336,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|~m_and_h_gate_h_init_v_out(X0,c_n,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5334,f236])).
% 7.67/1.43 fof(f5338,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_cell_v_token(X0,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5336,f905])).
% 7.67/1.43 fof(f5342,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5338,f282])).
% 7.67/1.43 fof(f5343,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5342,f237])).
% 7.67/1.43 fof(f5360,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|~m_and_h_gate_h_init_v_out(X0,c_m,s1)|node9(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f4728,f286])).
% 7.67/1.43 fof(f5362,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|node9(X0,c_m,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5360,f4609])).
% 7.67/1.43 fof(f5466,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s3)|m_cell_v_token(X0,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5343,f238])).
% 7.67/1.43 fof(f5469,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_v_in2(X0,c_r,s3))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5466,f1859])).
% 7.67/1.43 fof(f5504,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s3))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5469,f256])).
% 7.67/1.43 fof(f5567,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s2)|~m_and_h_gate_h_init_v_out(X0,c_m,s3)|node9(X0,c_m,s2))),
% 7.67/1.43 inference(resolution,[status(thm)],[f4747,f286])).
% 7.67/1.43 fof(f5569,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s2)|node9(X0,c_m,s2))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5567,f5504])).
% 7.67/1.43 fof(f5640,plain,(
% 7.67/1.43 m_cell_v_token(c_e_h_2,s0)|~sQ39_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f3659,f5466])).
% 7.67/1.43 fof(f5642,plain,(
% 7.67/1.43 sQ103_spl|~sQ39_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f5640,f2787,f514])).
% 7.67/1.43 fof(f5824,plain,(
% 7.67/1.43 m_cell_v_token(c_e_h_2,s0)|~sQ41_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f4163,f5466])).
% 7.67/1.43 fof(f5826,plain,(
% 7.67/1.43 sQ103_spl|~sQ41_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f5824,f2787,f520])).
% 7.67/1.43 fof(f5985,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s2)|m_and_h_gate_h_init_v_in2(X0,c_m,s2))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5569,f284])).
% 7.67/1.43 fof(f5994,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s2)|~m_and_h_gate_h_init_v_out(X0,c_n,s2))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5985,f236])).
% 7.67/1.43 fof(f6006,definition,(
% 7.67/1.43 sQ168_spl <=> (m_cell_v_ack(c_e_h_3,s0))),
% 7.67/1.43 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 7.67/1.43 fof(f6007,plain,(
% 7.67/1.43 m_cell_v_ack(c_e_h_3,s0)|~sQ168_spl),
% 7.67/1.43 inference(component_clause,[status(thm)],[f6006])).
% 7.67/1.43 fof(f6080,plain,(
% 7.67/1.43 m_and_h_gate_v_out(c_e_h_2,c_q,s0)|~sQ168_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f6007,f718])).
% 7.67/1.43 fof(f6082,plain,(
% 7.67/1.43 $false|~sQ168_spl),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f6080,f315])).
% 7.67/1.43 fof(f6083,plain,(
% 7.67/1.43 ~sQ168_spl),
% 7.67/1.43 inference(contradiction_clause,[status(thm)],[f6082])).
% 7.67/1.43 fof(f6112,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|m_and_h_gate_h_init_v_in2(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f5362,f284])).
% 7.67/1.43 fof(f6627,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|~m_and_h_gate_h_init_v_out(X0,c_n,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f6112,f236])).
% 7.67/1.43 fof(f6628,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f6627,f905])).
% 7.67/1.43 fof(f6642,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f6628,f282])).
% 7.67/1.43 fof(f6643,plain,(
% 7.67/1.43 ![X0]: (m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f6642,f237])).
% 7.67/1.43 fof(f6644,plain,(
% 7.67/1.43 ![X0]: (m_c_h_element_v_out(X0,c_e,s1)|m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f6643,f238])).
% 7.67/1.43 fof(f6647,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|node17(X0,c_e,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f6644,f1412])).
% 7.67/1.43 fof(f6648,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|node14(X0,c_e,s0,s1)|node16(X0,c_e,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f6644,f1261])).
% 7.67/1.43 fof(f6652,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|~m_c_h_element_v_in1(X0,c_e,s0)|m_c_h_element_v_in2(X0,c_e,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f6647,f308])).
% 7.67/1.43 fof(f6806,plain,(
% 7.67/1.43 m_cell_v_token(c_e_h_1,s0)|~sQ34_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f673,f2250])).
% 7.67/1.43 fof(f6808,plain,(
% 7.67/1.43 sQ124_spl|~sQ34_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f6806,f3832,f495])).
% 7.67/1.43 fof(f6818,plain,(
% 7.67/1.43 sQ79_spl|~sQ37_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f722,f1510,f506])).
% 7.67/1.43 fof(f6825,plain,(
% 7.67/1.43 sQ77_spl|~sQ36_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f1610,f1503,f503])).
% 7.67/1.43 fof(f6826,plain,(
% 7.67/1.43 sQ77_spl|~sQ38_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f2513,f1503,f509])).
% 7.67/1.43 fof(f7226,plain,(
% 7.67/1.43 m_cell_v_token(c_e_h_1,s0)|~sQ40_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f671,f5466])).
% 7.67/1.43 fof(f7228,plain,(
% 7.67/1.43 sQ124_spl|~sQ40_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f7226,f3832,f517])).
% 7.67/1.43 fof(f7642,plain,(
% 7.67/1.43 m_c_h_element_v_out(c_e_h_3,c_e,s0)|~sQ148_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f5195,f254])).
% 7.67/1.43 fof(f7643,plain,(
% 7.67/1.43 $false|~sQ148_spl),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f7642,f300])).
% 7.67/1.43 fof(f7644,plain,(
% 7.67/1.43 ~sQ148_spl),
% 7.67/1.43 inference(contradiction_clause,[status(thm)],[f7643])).
% 7.67/1.43 fof(f8421,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|node16(X0,c_e,s0)|~m_c_h_element_v_out(X0,c_e,s1)|m_c_h_element_v_in1(X0,c_e,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f6648,f302])).
% 7.67/1.43 fof(f8423,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|node16(X0,c_e,s0)|m_c_h_element_v_in1(X0,c_e,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f8421,f6644])).
% 7.67/1.43 fof(f8425,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|m_c_h_element_v_in1(X0,c_e,s0)|m_c_h_element_v_in1(X0,c_e,s0)|m_c_h_element_v_in2(X0,c_e,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f8423,f305])).
% 7.67/1.43 fof(f8426,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|m_c_h_element_v_in1(X0,c_e,s0)|m_c_h_element_v_in2(X0,c_e,s0))),
% 7.67/1.43 inference(duplicate_literals_removal,[status(thm)],[f8425])).
% 7.67/1.43 fof(f8427,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|m_c_h_element_v_in2(X0,c_e,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f8426,f6652])).
% 7.67/1.43 fof(f8434,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0)|m_and_h_gate_v_out(X0,c_i,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f8427,f204])).
% 7.67/1.43 fof(f8438,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_q,s2)|m_cell_v_token(X0,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f8434,f315])).
% 7.67/1.43 fof(f8439,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_h_init_v_out(X0,c_n,s2))),
% 7.67/1.43 inference(resolution,[status(thm)],[f8438,f252])).
% 7.67/1.43 fof(f8440,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s2))),
% 7.67/1.43 inference(backward_subsumption_resolution,[status(thm)],[f5994,f8439])).
% 7.67/1.43 fof(f8449,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|node10(X0,c_m,s1,s2))),
% 7.67/1.43 inference(resolution,[status(thm)],[f8440,f1029])).
% 7.67/1.43 fof(f9071,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_out(X0,c_m,s2)|node9(X0,c_m,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f8449,f286])).
% 7.67/1.43 fof(f9073,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|node9(X0,c_m,s1))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f9071,f8440])).
% 7.67/1.43 fof(f9074,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|m_and_h_gate_h_init_v_in2(X0,c_m,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f9073,f284])).
% 7.67/1.43 fof(f9080,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s1)|~m_and_h_gate_h_init_v_out(X0,c_n,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f9074,f236])).
% 7.67/1.43 fof(f9081,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s1))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f9080,f1132])).
% 7.67/1.43 fof(f9084,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node10(X0,c_m,s0,s1))),
% 7.67/1.43 inference(resolution,[status(thm)],[f9081,f1031])).
% 7.67/1.43 fof(f9643,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|~m_and_h_gate_h_init_v_out(X0,c_m,s1)|node9(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f9084,f286])).
% 7.67/1.43 fof(f9645,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|node9(X0,c_m,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f9643,f9081])).
% 7.67/1.43 fof(f9646,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|m_and_h_gate_h_init_v_in2(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f9645,f284])).
% 7.67/1.43 fof(f9648,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s0)|~m_and_h_gate_h_init_v_out(X0,c_n,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f9646,f236])).
% 7.67/1.43 fof(f9649,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_out(X0,c_m,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f9648,f905])).
% 7.67/1.43 fof(f9662,plain,(
% 7.67/1.43 ![X0]: (m_cell_v_token(X0,s0)|m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f9649,f282])).
% 7.67/1.43 fof(f9663,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0))),
% 7.67/1.43 inference(forward_subsumption_resolution,[status(thm)],[f9662,f237])).
% 7.67/1.43 fof(f9664,plain,(
% 7.67/1.43 ![X0]: (m_and_h_gate_v_in2(X0,c_d,s4)|m_cell_v_token(X0,s0))),
% 7.67/1.43 inference(resolution,[status(thm)],[f9663,f238])).
% 7.67/1.43 fof(f9667,plain,(
% 7.67/1.43 m_cell_v_token(c_e_h_2,s0)|~sQ42_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f9664,f3679])).
% 7.67/1.43 fof(f9669,plain,(
% 7.67/1.43 sQ103_spl|~sQ42_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f9667,f2787,f525])).
% 7.67/1.43 fof(f9783,plain,(
% 7.67/1.43 ~m_and_h_gate_v_in2(c_e_h_2,c_d,s4)|~sQ44_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f560,f200])).
% 7.67/1.43 fof(f9863,plain,(
% 7.67/1.43 m_cell_v_token(c_e_h_2,s0)|~sQ44_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f9783,f9664])).
% 7.67/1.43 fof(f9865,plain,(
% 7.67/1.43 sQ103_spl|~sQ44_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f9863,f2787,f531])).
% 7.67/1.43 fof(f10075,plain,(
% 7.67/1.43 ~m_and_h_gate_v_in2(c_e_h_1,c_d,s4)|~sQ43_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f562,f200])).
% 7.67/1.43 fof(f10084,plain,(
% 7.67/1.43 m_cell_v_token(c_e_h_1,s0)|~sQ43_spl),
% 7.67/1.43 inference(resolution,[status(thm)],[f10075,f9664])).
% 7.67/1.43 fof(f10086,plain,(
% 7.67/1.43 sQ124_spl|~sQ43_spl),
% 7.67/1.43 inference(split_clause,[status(thm)],[f10084,f3832,f528])).
% 7.67/1.43 fof(f10088,plain,(
% 7.67/1.43 $false),
% 7.67/1.43 inference(sat_refutation,[status(thm)],[f360,f364,f377,f389,f396,f403,f407,f418,f425,f432,f439,f450,f455,f460,f465,f473,f475,f477,f479,f484,f501,f512,f523,f534,f537,f540,f575,f577,f584,f605,f612,f622,f624,f737,f739,f882,f2792,f3037,f3823,f3847,f4016,f4019,f4346,f5190,f5642,f5826,f6083,f6808,f6818,f6825,f6826,f7228,f7644,f9669,f9865,f10086])).
% 7.67/1.43 % SZS output end CNFRefutation for theBenchmark.p
% 6.71/1.46 % Elapsed time: 1.081667 seconds
% 6.71/1.46 % CPU time: 8.177418 seconds
% 6.71/1.46 % Total memory used: 80.160 MB
% 6.71/1.46 % Net memory used: 75.085 MB
%------------------------------------------------------------------------------