%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV419-1.005 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 03:18:44 PM UTC 2026
% Result : Unsatisfiable 4.72s 7.07s
% Output : CNFRefutation 4.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 49
% Syntax : Number of formulae : 389 ( 39 unt; 0 def)
% Number of atoms : 998 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1143 ( 534 ~; 609 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 33 ( 32 usr; 2 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 16 con; 0-0 aty)
% Number of variables : 294 ( 0 sgn 294 !; 0 ?; 198 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
succ(s0,s1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound1) ).
fof(f2,axiom,
succ(s1,s2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound2) ).
fof(f3,axiom,
succ(s2,s3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound3) ).
fof(f4,axiom,
succ(s3,s4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound4) ).
fof(f5,axiom,
last(s4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound5) ).
fof(f6,axiom,
! [X0,X1] :
( trans(X0,X1)
| ~ succ(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound6) ).
fof(f7,axiom,
( trans(s4,s4)
| trans(s4,s3)
| trans(s4,s2)
| trans(s4,s1)
| trans(s4,s0)
| ~ loop ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bound7) ).
fof(f10,axiom,
! [X0] : ~ m_cell_v_token(c_e_h_1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_3) ).
fof(f13,axiom,
! [X0] : ~ m_cell_v_token(c_e_h_2,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_main_6) ).
fof(f36,axiom,
! [X0,X1] :
( m_and_h_gate_v_out(X0,c_c,X1)
| ~ m_c_h_element_v_in1(X0,c_e,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_20) ).
fof(f38,axiom,
! [X0,X1] :
( m_and_h_gate_v_out(X0,c_i,X1)
| ~ m_c_h_element_v_in2(X0,c_e,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_22) ).
fof(f48,axiom,
! [X0,X1] :
( m_or_h_gate_v_out(X0,c_g,X1)
| ~ m_c_h_element_v_in1(X0,c_h,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_32) ).
fof(f50,axiom,
! [X0,X1] :
( m_or_h_gate_v_out(X0,c_j,X1)
| ~ m_c_h_element_v_in2(X0,c_h,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_34) ).
fof(f52,axiom,
! [X0,X1] :
( m_c_h_element_v_out(X0,c_h,X1)
| ~ m_and_h_gate_v_in1(X0,c_i,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_36) ).
fof(f72,axiom,
! [X0,X1] :
( m_cell_v_token(X0,X1)
| ~ m_and_h_gate_h_init_v_init_h_out(X0,c_m,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_56) ).
fof(f88,axiom,
! [X0,X1] :
( m_c_h_element_v_out(X0,c_e,X1)
| ~ m_and_h_gate_v_in1(X0,c_r,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_72) ).
fof(f90,axiom,
! [X0,X1] :
( m_and_h_gate_h_init_v_out(X0,c_m,X1)
| ~ m_and_h_gate_v_in2(X0,c_r,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_74) ).
fof(f97,axiom,
! [X0,X1] :
( m_and_h_gate_v_out(X0,c_r,X1)
| ~ m_user_v_ack(X0,c_u,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_cell_81) ).
fof(f98,axiom,
! [X0,X1] : ~ m_or_h_gate_v_out(X0,X1,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_or_h_gate_1) ).
fof(f113,axiom,
! [X0,X1] :
( m_and_h_gate_h_init_v_init_h_out(X0,X1,s0)
| ~ m_and_h_gate_h_init_v_out(X0,X1,s0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_and_h_gate_h_init_2) ).
fof(f128,axiom,
! [X0,X1] : ~ m_c_h_element_v_out(X0,X1,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_1) ).
fof(f130,axiom,
! [X2,X3,X0,X1] :
( ~ node14(X0,X1,X3,X2)
| m_c_h_element_v_in1(X0,X1,X3)
| ~ m_c_h_element_v_out(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_3) ).
fof(f132,axiom,
! [X2,X3,X0,X1] :
( ~ node15(X0,X1,X3,X2)
| m_c_h_element_v_out(X0,X1,X3)
| ~ m_c_h_element_v_out(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_5) ).
fof(f133,axiom,
! [X2,X0,X1] :
( ~ node16(X0,X1,X2)
| m_c_h_element_v_in2(X0,X1,X2)
| m_c_h_element_v_in1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_6) ).
fof(f135,axiom,
! [X2,X0,X1] :
( ~ node17(X0,X1,X2)
| ~ m_c_h_element_v_in2(X0,X1,X2)
| m_c_h_element_v_in1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_8) ).
fof(f136,axiom,
! [X2,X0,X1] :
( ~ node17(X0,X1,X2)
| m_c_h_element_v_in2(X0,X1,X2)
| ~ m_c_h_element_v_in1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_9) ).
fof(f138,axiom,
! [X2,X3,X0,X1] :
( ~ node18(X0,X1,X3,X2)
| m_c_h_element_v_out(X0,X1,X3)
| ~ m_c_h_element_v_out(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_11) ).
fof(f139,axiom,
! [X2,X3,X0,X1] :
( ~ node19(X0,X1,X2,X3)
| node16(X0,X1,X2)
| node15(X0,X1,X2,X3)
| node14(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_12) ).
fof(f140,axiom,
! [X2,X3,X0,X1] :
( ~ node19(X0,X1,X2,X3)
| node18(X0,X1,X2,X3)
| node17(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_13) ).
fof(f141,axiom,
! [X2,X3,X0,X1] :
( node19(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_c_h_element_14) ).
fof(f142,axiom,
! [X0,X1] : ~ m_and_h_gate_v_out(X0,X1,s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_and_h_gate_1) ).
fof(f143,axiom,
! [X2,X0,X1] :
( ~ node20(X0,X1,X2)
| m_and_h_gate_v_in1(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_and_h_gate_2) ).
fof(f144,axiom,
! [X2,X0,X1] :
( ~ node20(X0,X1,X2)
| m_and_h_gate_v_in2(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_and_h_gate_3) ).
fof(f146,axiom,
! [X2,X3,X0,X1] :
( ~ node21(X0,X1,X3,X2)
| node20(X0,X1,X3)
| ~ m_and_h_gate_v_out(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_and_h_gate_5) ).
fof(f148,axiom,
! [X2,X3,X0,X1] :
( ~ node22(X0,X1,X3,X2)
| m_and_h_gate_v_out(X0,X1,X3)
| ~ m_and_h_gate_v_out(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_and_h_gate_7) ).
fof(f149,axiom,
! [X2,X3,X0,X1] :
( ~ trans(X2,X3)
| node22(X0,X1,X2,X3)
| node21(X0,X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_and_h_gate_8) ).
fof(f150,negated_conjecture,
! [X0] :
( ~ node23(X0)
| m_user_v_ack(c_e_h_1,c_u,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty1) ).
fof(f151,negated_conjecture,
! [X0] :
( ~ node23(X0)
| m_user_v_ack(c_e_h_2,c_u,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty2) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ node24(X0)
| m_user_v_ack(c_e_h_1,c_u,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty3) ).
fof(f154,negated_conjecture,
! [X0] :
( ~ node25(X0)
| m_user_v_ack(c_e_h_2,c_u,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty5) ).
fof(f156,negated_conjecture,
! [X0] :
( ~ node26(X0)
| node25(X0)
| node24(X0)
| node23(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty7) ).
fof(f157,negated_conjecture,
! [X0] :
( ~ until27(X0)
| xuntil28(X0)
| node26(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty8) ).
fof(f158,negated_conjecture,
! [X0,X1] :
( ~ xuntil28(X1)
| ~ succ(X1,X0)
| until27(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty9) ).
fof(f159,negated_conjecture,
! [X0] :
( ~ xuntil28(X0)
| ~ last(X0)
| loop ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty10) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( ~ xuntil28(X1)
| ~ last(X1)
| ~ trans(X1,X0)
| until2p29(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty11) ).
fof(f161,negated_conjecture,
! [X0] :
( ~ until2p29(X0)
| xuntil2p30(X0)
| node26(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty12) ).
fof(f162,negated_conjecture,
! [X0,X1] :
( ~ xuntil2p30(X1)
| ~ succ(X1,X0)
| until2p29(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty13) ).
fof(f163,negated_conjecture,
! [X0] :
( ~ xuntil2p30(X0)
| ~ last(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty14) ).
fof(f164,negated_conjecture,
until27(s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prpty15) ).
tcf(c_213,plain,
succ(s0,s1),
inference(cnf_transformation,[],[f1]) ).
tcf(c_214,plain,
succ(s1,s2),
inference(cnf_transformation,[],[f2]) ).
tcf(c_215,plain,
succ(s2,s3),
inference(cnf_transformation,[],[f3]) ).
tcf(c_216,plain,
succ(s3,s4),
inference(cnf_transformation,[],[f4]) ).
tcf(c_217,plain,
last(s4),
inference(cnf_transformation,[],[f5]) ).
tcf(c_218,plain,
! [X0: $i,X1: $i] :
( trans(X0,X1)
| ~ succ(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_219,plain,
( trans(s4,s4)
| trans(s4,s3)
| trans(s4,s2)
| trans(s4,s1)
| trans(s4,s0)
| ~ loop ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_221,plain,
! [X0: $i] : ~ m_cell_v_token(c_e_h_1,X0),
inference(cnf_transformation,[],[f10]) ).
tcf(c_223,plain,
! [X0: $i] : ~ m_cell_v_token(c_e_h_2,X0),
inference(cnf_transformation,[],[f13]) ).
tcf(c_245,plain,
! [X0: $i,X1: $i] :
( m_and_h_gate_v_out(X0,c_c,X1)
| ~ m_c_h_element_v_in1(X0,c_e,X1) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i] :
( m_and_h_gate_v_out(X0,c_i,X1)
| ~ m_c_h_element_v_in2(X0,c_e,X1) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_257,plain,
! [X0: $i,X1: $i] :
( m_or_h_gate_v_out(X0,c_g,X1)
| ~ m_c_h_element_v_in1(X0,c_h,X1) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i] :
( m_or_h_gate_v_out(X0,c_j,X1)
| ~ m_c_h_element_v_in2(X0,c_h,X1) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_261,plain,
! [X0: $i,X1: $i] :
( m_c_h_element_v_out(X0,c_h,X1)
| ~ m_and_h_gate_v_in1(X0,c_i,X1) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i] :
( m_cell_v_token(X0,X1)
| ~ m_and_h_gate_h_init_v_init_h_out(X0,c_m,X1) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_297,plain,
! [X0: $i,X1: $i] :
( m_c_h_element_v_out(X0,c_e,X1)
| ~ m_and_h_gate_v_in1(X0,c_r,X1) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_299,plain,
! [X0: $i,X1: $i] :
( m_and_h_gate_h_init_v_out(X0,c_m,X1)
| ~ m_and_h_gate_v_in2(X0,c_r,X1) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_306,plain,
! [X0: $i,X1: $i] :
( m_and_h_gate_v_out(X0,c_r,X1)
| ~ m_user_v_ack(X0,c_u,X1) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_307,plain,
! [X0: $i,X1: $i] : ~ m_or_h_gate_v_out(X0,X1,s0),
inference(cnf_transformation,[],[f98]) ).
tcf(c_322,plain,
! [X0: $i,X1: $i] :
( m_and_h_gate_h_init_v_init_h_out(X0,X1,s0)
| ~ m_and_h_gate_h_init_v_out(X0,X1,s0) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_337,plain,
! [X0: $i,X1: $i] : ~ m_c_h_element_v_out(X0,X1,s0),
inference(cnf_transformation,[],[f128]) ).
tcf(c_339,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m_c_h_element_v_in1(X0,X1,X2)
| ~ m_c_h_element_v_out(X0,X1,X3)
| ~ node14(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_341,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m_c_h_element_v_out(X0,X1,X2)
| ~ m_c_h_element_v_out(X0,X1,X3)
| ~ node15(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_342,plain,
! [X0: $i,X1: $i,X2: $i] :
( m_c_h_element_v_in2(X0,X1,X2)
| m_c_h_element_v_in1(X0,X1,X2)
| ~ node16(X0,X1,X2) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_344,plain,
! [X0: $i,X1: $i,X2: $i] :
( m_c_h_element_v_in1(X0,X1,X2)
| ~ node17(X0,X1,X2)
| ~ m_c_h_element_v_in2(X0,X1,X2) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_345,plain,
! [X0: $i,X1: $i,X2: $i] :
( m_c_h_element_v_in2(X0,X1,X2)
| ~ node17(X0,X1,X2)
| ~ m_c_h_element_v_in1(X0,X1,X2) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m_c_h_element_v_out(X0,X1,X2)
| ~ m_c_h_element_v_out(X0,X1,X3)
| ~ node18(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f138]) ).
tcf(c_348,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( node16(X0,X1,X2)
| node15(X0,X1,X2,X3)
| node14(X0,X1,X2,X3)
| ~ node19(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f139]) ).
tcf(c_349,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( node17(X0,X1,X2)
| node18(X0,X1,X2,X3)
| ~ node19(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_350,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( node19(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
inference(cnf_transformation,[],[f141]) ).
tcf(c_351,plain,
! [X0: $i,X1: $i] : ~ m_and_h_gate_v_out(X0,X1,s0),
inference(cnf_transformation,[],[f142]) ).
tcf(c_352,plain,
! [X0: $i,X1: $i,X2: $i] :
( m_and_h_gate_v_in1(X0,X1,X2)
| ~ node20(X0,X1,X2) ),
inference(cnf_transformation,[],[f143]) ).
tcf(c_353,plain,
! [X0: $i,X1: $i,X2: $i] :
( m_and_h_gate_v_in2(X0,X1,X2)
| ~ node20(X0,X1,X2) ),
inference(cnf_transformation,[],[f144]) ).
tcf(c_355,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( node20(X0,X1,X2)
| ~ m_and_h_gate_v_out(X0,X1,X3)
| ~ node21(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_357,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( m_and_h_gate_v_out(X0,X1,X2)
| ~ m_and_h_gate_v_out(X0,X1,X3)
| ~ node22(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_358,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( node22(X2,X3,X0,X1)
| node21(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
inference(cnf_transformation,[],[f149]) ).
tcf(c_359,negated_conjecture,
! [X0: $i] :
( m_user_v_ack(c_e_h_1,c_u,X0)
| ~ node23(X0) ),
inference(cnf_transformation,[],[f150]) ).
tcf(c_360,negated_conjecture,
! [X0: $i] :
( m_user_v_ack(c_e_h_2,c_u,X0)
| ~ node23(X0) ),
inference(cnf_transformation,[],[f151]) ).
tcf(c_361,negated_conjecture,
! [X0: $i] :
( m_user_v_ack(c_e_h_1,c_u,X0)
| ~ node24(X0) ),
inference(cnf_transformation,[],[f152]) ).
tcf(c_363,negated_conjecture,
! [X0: $i] :
( m_user_v_ack(c_e_h_2,c_u,X0)
| ~ node25(X0) ),
inference(cnf_transformation,[],[f154]) ).
tcf(c_365,negated_conjecture,
! [X0: $i] :
( node25(X0)
| node24(X0)
| node23(X0)
| ~ node26(X0) ),
inference(cnf_transformation,[],[f156]) ).
tcf(c_366,negated_conjecture,
! [X0: $i] :
( xuntil28(X0)
| node26(X0)
| ~ until27(X0) ),
inference(cnf_transformation,[],[f157]) ).
tcf(c_367,negated_conjecture,
! [X0: $i,X1: $i] :
( until27(X1)
| ~ xuntil28(X0)
| ~ succ(X0,X1) ),
inference(cnf_transformation,[],[f158]) ).
tcf(c_368,negated_conjecture,
! [X0: $i] :
( loop
| ~ xuntil28(X0)
| ~ last(X0) ),
inference(cnf_transformation,[],[f159]) ).
tcf(c_369,negated_conjecture,
! [X0: $i,X1: $i] :
( until2p29(X1)
| ~ xuntil28(X0)
| ~ last(X0)
| ~ trans(X0,X1) ),
inference(cnf_transformation,[],[f160]) ).
tcf(c_370,negated_conjecture,
! [X0: $i] :
( xuntil2p30(X0)
| node26(X0)
| ~ until2p29(X0) ),
inference(cnf_transformation,[],[f161]) ).
tcf(c_371,negated_conjecture,
! [X0: $i,X1: $i] :
( until2p29(X1)
| ~ xuntil2p30(X0)
| ~ succ(X0,X1) ),
inference(cnf_transformation,[],[f162]) ).
tcf(c_372,negated_conjecture,
! [X0: $i] :
( ~ xuntil2p30(X0)
| ~ last(X0) ),
inference(cnf_transformation,[],[f163]) ).
tcf(c_373,negated_conjecture,
until27(s0),
inference(cnf_transformation,[],[f164]) ).
tcf(c_511,plain,
( xuntil28(s0)
| node26(s0)
| ~ until27(s0) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_512,plain,
( trans(s0,s1)
| ~ succ(s0,s1) ),
inference(instantiation,[status(thm)],[c_218]) ).
tcf(c_513,plain,
( trans(s1,s2)
| ~ succ(s1,s2) ),
inference(instantiation,[status(thm)],[c_218]) ).
tcf(c_514,plain,
( trans(s2,s3)
| ~ succ(s2,s3) ),
inference(instantiation,[status(thm)],[c_218]) ).
tcf(c_515,plain,
( trans(s3,s4)
| ~ succ(s3,s4) ),
inference(instantiation,[status(thm)],[c_218]) ).
tcf(c_542,plain,
( node25(s0)
| node24(s0)
| node23(s0)
| ~ node26(s0) ),
inference(instantiation,[status(thm)],[c_365]) ).
tcf(c_543,plain,
! [X0: $i,X1: $i] :
( node22(X0,X1,s0,s1)
| node21(X0,X1,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_557,plain,
! [X0: $i,X1: $i] :
( node22(X0,X1,s1,s2)
| node21(X0,X1,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_576,plain,
! [X0: $i,X1: $i] :
( node19(X0,X1,s2,s3)
| ~ trans(s2,s3) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i] :
( node22(X0,X1,s3,s4)
| node21(X0,X1,s3,s4)
| ~ trans(s3,s4) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_625,plain,
~ m_cell_v_token(c_e_h_1,s0),
inference(instantiation,[status(thm)],[c_221]) ).
tcf(c_627,plain,
~ m_cell_v_token(c_e_h_2,s0),
inference(instantiation,[status(thm)],[c_223]) ).
tcf(c_633,plain,
! [X0: $i] :
( until27(X0)
| ~ xuntil28(s0)
| ~ succ(s0,X0) ),
inference(instantiation,[status(thm)],[c_367]) ).
tcf(c_656,plain,
! [X0: $i] :
( m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0)
| ~ m_and_h_gate_h_init_v_out(X0,c_m,s0) ),
inference(instantiation,[status(thm)],[c_322]) ).
tcf(c_657,plain,
! [X0: $i] :
( m_cell_v_token(X0,s0)
| ~ m_and_h_gate_h_init_v_init_h_out(X0,c_m,s0) ),
inference(instantiation,[status(thm)],[c_281]) ).
tcf(c_675,plain,
! [X0: $i,X1: $i] :
( node16(X0,X1,s2)
| node15(X0,X1,s2,s3)
| node14(X0,X1,s2,s3)
| ~ node19(X0,X1,s2,s3) ),
inference(instantiation,[status(thm)],[c_348]) ).
tcf(c_676,plain,
! [X0: $i,X1: $i] :
( node17(X0,X1,s2)
| node18(X0,X1,s2,s3)
| ~ node19(X0,X1,s2,s3) ),
inference(instantiation,[status(thm)],[c_349]) ).
tcf(c_720,plain,
( until27(s1)
| ~ xuntil28(s0)
| ~ succ(s0,s1) ),
inference(instantiation,[status(thm)],[c_633]) ).
tcf(c_750,plain,
! [X0: $i] :
( m_and_h_gate_h_init_v_out(X0,c_m,s0)
| ~ m_and_h_gate_v_in2(X0,c_r,s0) ),
inference(instantiation,[status(thm)],[c_299]) ).
tcf(c_758,plain,
( m_cell_v_token(c_e_h_1,s0)
| ~ m_and_h_gate_h_init_v_init_h_out(c_e_h_1,c_m,s0) ),
inference(instantiation,[status(thm)],[c_657]) ).
tcf(c_759,plain,
( m_cell_v_token(c_e_h_2,s0)
| ~ m_and_h_gate_h_init_v_init_h_out(c_e_h_2,c_m,s0) ),
inference(instantiation,[status(thm)],[c_657]) ).
tcf(c_835,plain,
( m_user_v_ack(c_e_h_2,c_u,s0)
| ~ node23(s0) ),
inference(instantiation,[status(thm)],[c_360]) ).
tcf(c_948,plain,
( m_user_v_ack(c_e_h_1,c_u,s0)
| ~ node24(s0) ),
inference(instantiation,[status(thm)],[c_361]) ).
tcf(c_1012,plain,
( m_user_v_ack(c_e_h_2,c_u,s0)
| ~ node25(s0) ),
inference(instantiation,[status(thm)],[c_363]) ).
tcf(c_1067,plain,
( xuntil28(s1)
| node26(s1)
| ~ until27(s1) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_1084,plain,
( m_and_h_gate_h_init_v_init_h_out(c_e_h_1,c_m,s0)
| ~ m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s0) ),
inference(instantiation,[status(thm)],[c_656]) ).
tcf(c_1085,plain,
( m_and_h_gate_h_init_v_init_h_out(c_e_h_2,c_m,s0)
| ~ m_and_h_gate_h_init_v_out(c_e_h_2,c_m,s0) ),
inference(instantiation,[status(thm)],[c_656]) ).
tcf(c_1159,plain,
( node25(s1)
| node24(s1)
| node23(s1)
| ~ node26(s1) ),
inference(instantiation,[status(thm)],[c_365]) ).
tcf(c_1170,plain,
( m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s0)
| ~ m_and_h_gate_v_in2(c_e_h_1,c_r,s0) ),
inference(instantiation,[status(thm)],[c_750]) ).
tcf(c_1175,plain,
( m_and_h_gate_h_init_v_out(c_e_h_2,c_m,s0)
| ~ m_and_h_gate_v_in2(c_e_h_2,c_r,s0) ),
inference(instantiation,[status(thm)],[c_750]) ).
tcf(c_1262,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s0)
| ~ m_user_v_ack(c_e_h_2,c_u,s0) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_1266,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s0)
| ~ m_user_v_ack(c_e_h_1,c_u,s0) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_1368,plain,
! [X0: $i] :
( until27(X0)
| ~ xuntil28(s1)
| ~ succ(s1,X0) ),
inference(instantiation,[status(thm)],[c_367]) ).
tcf(c_1401,plain,
( until27(s2)
| ~ xuntil28(s1)
| ~ succ(s1,s2) ),
inference(instantiation,[status(thm)],[c_1368]) ).
tcf(c_1464,plain,
! [X0: $i] : ~ m_c_h_element_v_out(X0,c_e,s0),
inference(instantiation,[status(thm)],[c_337]) ).
tcf(c_1471,plain,
( xuntil28(s2)
| node26(s2)
| ~ until27(s2) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_1514,plain,
! [X0: $i] :
( until27(X0)
| ~ xuntil28(s2)
| ~ succ(s2,X0) ),
inference(instantiation,[status(thm)],[c_367]) ).
tcf(c_1554,plain,
( until27(s3)
| ~ xuntil28(s2)
| ~ succ(s2,s3) ),
inference(instantiation,[status(thm)],[c_1514]) ).
tcf(c_1581,plain,
( xuntil28(s3)
| node26(s3)
| ~ until27(s3) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_1595,plain,
( node25(s3)
| node24(s3)
| node23(s3)
| ~ node26(s3) ),
inference(instantiation,[status(thm)],[c_365]) ).
tcf(c_1634,plain,
( m_user_v_ack(c_e_h_1,c_u,s3)
| ~ node23(s3) ),
inference(instantiation,[status(thm)],[c_359]) ).
tcf(c_1667,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| ~ m_user_v_ack(c_e_h_2,c_u,s3) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_1671,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s3)
| ~ m_user_v_ack(c_e_h_1,c_u,s3) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_1735,plain,
( m_user_v_ack(c_e_h_2,c_u,s1)
| ~ node23(s1) ),
inference(instantiation,[status(thm)],[c_360]) ).
tcf(c_1789,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| ~ m_user_v_ack(c_e_h_2,c_u,s1) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_1793,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s1)
| ~ m_user_v_ack(c_e_h_1,c_u,s1) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_1827,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_2,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| ~ node22(c_e_h_2,c_r,X0,s1) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_1828,plain,
! [X0: $i] :
( node20(c_e_h_2,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| ~ node21(c_e_h_2,c_r,X0,s1) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_1835,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_1,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s1)
| ~ node22(c_e_h_1,c_r,X0,s1) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_1836,plain,
! [X0: $i] :
( node20(c_e_h_1,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s1)
| ~ node21(c_e_h_1,c_r,X0,s1) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_1926,plain,
( node20(c_e_h_2,c_r,s0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| ~ node21(c_e_h_2,c_r,s0,s1) ),
inference(instantiation,[status(thm)],[c_1828]) ).
tcf(c_1927,plain,
( node22(c_e_h_2,c_r,s0,s1)
| node21(c_e_h_2,c_r,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_543]) ).
tcf(c_1928,plain,
( node20(c_e_h_1,c_r,s0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s1)
| ~ node21(c_e_h_1,c_r,s0,s1) ),
inference(instantiation,[status(thm)],[c_1836]) ).
tcf(c_1929,plain,
( node22(c_e_h_1,c_r,s0,s1)
| node21(c_e_h_1,c_r,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_543]) ).
tcf(c_1954,plain,
! [X0: $i,X1: $i] :
( m_c_h_element_v_out(X0,c_e,X1)
| ~ m_c_h_element_v_out(X0,c_e,s2)
| ~ node15(X0,c_e,X1,s2) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_1955,plain,
! [X0: $i,X1: $i] :
( m_c_h_element_v_in1(X0,c_e,X1)
| ~ m_c_h_element_v_out(X0,c_e,s2)
| ~ node14(X0,c_e,X1,s2) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_1965,plain,
( m_and_h_gate_v_in2(c_e_h_2,c_r,s0)
| ~ node20(c_e_h_2,c_r,s0) ),
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_1967,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| ~ node22(c_e_h_2,c_r,s0,s1) ),
inference(instantiation,[status(thm)],[c_1827]) ).
tcf(c_1968,plain,
( m_and_h_gate_v_in2(c_e_h_1,c_r,s0)
| ~ node20(c_e_h_1,c_r,s0) ),
inference(instantiation,[status(thm)],[c_353]) ).
tcf(c_1970,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s1)
| ~ node22(c_e_h_1,c_r,s0,s1) ),
inference(instantiation,[status(thm)],[c_1835]) ).
tcf(c_2043,plain,
! [X0: $i] :
( m_c_h_element_v_out(X0,c_e,s2)
| ~ m_and_h_gate_v_in1(X0,c_r,s2) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_2058,plain,
! [X0: $i] :
( m_c_h_element_v_in1(X0,c_e,s1)
| ~ m_c_h_element_v_out(X0,c_e,s2)
| ~ node14(X0,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_1955]) ).
tcf(c_2063,plain,
! [X0: $i] :
( node17(X0,c_e,s2)
| node18(X0,c_e,s2,s3)
| ~ node19(X0,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_676]) ).
tcf(c_2067,plain,
~ m_and_h_gate_v_out(c_e_h_2,c_r,s0),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_2072,plain,
~ m_and_h_gate_v_out(c_e_h_1,c_r,s0),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_2119,plain,
! [X0: $i] :
( node19(X0,c_e,s2,s3)
| ~ trans(s2,s3) ),
inference(instantiation,[status(thm)],[c_576]) ).
tcf(c_2125,plain,
! [X0: $i] :
( m_c_h_element_v_out(X0,c_e,s1)
| ~ m_c_h_element_v_out(X0,c_e,s2)
| ~ node15(X0,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_1954]) ).
tcf(c_2128,plain,
( m_user_v_ack(c_e_h_1,c_u,s1)
| ~ node24(s1) ),
inference(instantiation,[status(thm)],[c_361]) ).
tcf(c_2134,plain,
! [X0: $i] :
( m_c_h_element_v_in2(X0,c_e,s2)
| ~ node17(X0,c_e,s2)
| ~ m_c_h_element_v_in1(X0,c_e,s2) ),
inference(instantiation,[status(thm)],[c_345]) ).
tcf(c_2135,plain,
! [X0: $i] :
( m_c_h_element_v_in1(X0,c_e,s2)
| ~ node17(X0,c_e,s2)
| ~ m_c_h_element_v_in2(X0,c_e,s2) ),
inference(instantiation,[status(thm)],[c_344]) ).
tcf(c_2144,plain,
( m_user_v_ack(c_e_h_2,c_u,s1)
| ~ node25(s1) ),
inference(instantiation,[status(thm)],[c_363]) ).
tcf(c_2158,plain,
( node25(s2)
| node24(s2)
| node23(s2)
| ~ node26(s2) ),
inference(instantiation,[status(thm)],[c_365]) ).
tcf(c_2190,plain,
( m_user_v_ack(c_e_h_1,c_u,s2)
| ~ node23(s2) ),
inference(instantiation,[status(thm)],[c_359]) ).
tcf(c_2238,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| ~ m_user_v_ack(c_e_h_2,c_u,s2) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_2242,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s2)
| ~ m_user_v_ack(c_e_h_1,c_u,s2) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_2285,plain,
( m_user_v_ack(c_e_h_2,c_u,s2)
| ~ node25(s2) ),
inference(instantiation,[status(thm)],[c_363]) ).
tcf(c_2337,plain,
! [X0: $i] :
( until27(X0)
| ~ xuntil28(s3)
| ~ succ(s3,X0) ),
inference(instantiation,[status(thm)],[c_367]) ).
tcf(c_2385,plain,
( until27(s4)
| ~ xuntil28(s3)
| ~ succ(s3,s4) ),
inference(instantiation,[status(thm)],[c_2337]) ).
tcf(c_2409,plain,
( xuntil28(s4)
| node26(s4)
| ~ until27(s4) ),
inference(instantiation,[status(thm)],[c_366]) ).
tcf(c_2483,plain,
! [X0: $i] :
( until2p29(X0)
| ~ xuntil28(s4)
| ~ last(s4)
| ~ trans(s4,X0) ),
inference(instantiation,[status(thm)],[c_369]) ).
tcf(c_2485,plain,
( loop
| ~ xuntil28(s4)
| ~ last(s4) ),
inference(instantiation,[status(thm)],[c_368]) ).
tcf(c_2594,plain,
( node25(s4)
| node24(s4)
| node23(s4)
| ~ node26(s4) ),
inference(instantiation,[status(thm)],[c_365]) ).
tcf(c_2620,plain,
( m_user_v_ack(c_e_h_1,c_u,s4)
| ~ node24(s4) ),
inference(instantiation,[status(thm)],[c_361]) ).
tcf(c_2691,plain,
( until2p29(s0)
| ~ xuntil28(s4)
| ~ last(s4)
| ~ trans(s4,s0) ),
inference(instantiation,[status(thm)],[c_2483]) ).
tcf(c_2740,plain,
( xuntil2p30(s0)
| node26(s0)
| ~ until2p29(s0) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_2777,plain,
( until2p29(s1)
| ~ xuntil28(s4)
| ~ last(s4)
| ~ trans(s4,s1) ),
inference(instantiation,[status(thm)],[c_2483]) ).
tcf(c_2792,plain,
( xuntil2p30(s1)
| node26(s1)
| ~ until2p29(s1) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_2829,plain,
( until2p29(s4)
| ~ xuntil28(s4)
| ~ last(s4)
| ~ trans(s4,s4) ),
inference(instantiation,[status(thm)],[c_2483]) ).
tcf(c_2855,plain,
( xuntil2p30(s4)
| node26(s4)
| ~ until2p29(s4) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_2894,plain,
! [X0: $i] :
( until2p29(X0)
| ~ xuntil2p30(s1)
| ~ succ(s1,X0) ),
inference(instantiation,[status(thm)],[c_371]) ).
tcf(c_2927,plain,
( until2p29(s2)
| ~ xuntil2p30(s1)
| ~ succ(s1,s2) ),
inference(instantiation,[status(thm)],[c_2894]) ).
tcf(c_2951,plain,
( until2p29(s2)
| ~ xuntil28(s4)
| ~ last(s4)
| ~ trans(s4,s2) ),
inference(instantiation,[status(thm)],[c_2483]) ).
tcf(c_3002,plain,
( until2p29(s3)
| ~ xuntil28(s4)
| ~ last(s4)
| ~ trans(s4,s3) ),
inference(instantiation,[status(thm)],[c_2483]) ).
tcf(c_3039,plain,
( xuntil2p30(s3)
| node26(s3)
| ~ until2p29(s3) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_3080,plain,
( m_user_v_ack(c_e_h_2,c_u,s4)
| ~ node23(s4) ),
inference(instantiation,[status(thm)],[c_360]) ).
tcf(c_3096,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s4)
| ~ m_user_v_ack(c_e_h_2,c_u,s4) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_3101,plain,
( m_user_v_ack(c_e_h_2,c_u,s4)
| ~ node25(s4) ),
inference(instantiation,[status(thm)],[c_363]) ).
tcf(c_3141,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s4)
| ~ m_user_v_ack(c_e_h_1,c_u,s4) ),
inference(instantiation,[status(thm)],[c_306]) ).
tcf(c_3146,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_2,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s4)
| ~ node22(c_e_h_2,c_r,X0,s4) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_3147,plain,
! [X0: $i] :
( node20(c_e_h_2,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s4)
| ~ node21(c_e_h_2,c_r,X0,s4) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_3249,plain,
( node20(c_e_h_2,c_r,s3)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s4)
| ~ node21(c_e_h_2,c_r,s3,s4) ),
inference(instantiation,[status(thm)],[c_3147]) ).
tcf(c_3250,plain,
( node22(c_e_h_2,c_r,s3,s4)
| node21(c_e_h_2,c_r,s3,s4)
| ~ trans(s3,s4) ),
inference(instantiation,[status(thm)],[c_585]) ).
tcf(c_3323,plain,
( m_and_h_gate_v_in1(c_e_h_2,c_r,s3)
| ~ node20(c_e_h_2,c_r,s3) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_3409,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ m_and_h_gate_v_in1(c_e_h_2,c_r,s3) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_3501,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s4)
| ~ node22(c_e_h_2,c_r,s3,s4) ),
inference(instantiation,[status(thm)],[c_3146]) ).
tcf(c_3561,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_2,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ node18(c_e_h_2,c_e,X0,s3) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_3562,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_2,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ node15(c_e_h_2,c_e,X0,s3) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_3563,plain,
! [X0: $i] :
( m_c_h_element_v_in1(c_e_h_2,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ node14(c_e_h_2,c_e,X0,s3) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_3697,plain,
( m_c_h_element_v_in1(c_e_h_2,c_e,s2)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ node14(c_e_h_2,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_3563]) ).
tcf(c_3698,plain,
( node16(c_e_h_2,c_e,s2)
| node15(c_e_h_2,c_e,s2,s3)
| node14(c_e_h_2,c_e,s2,s3)
| ~ node19(c_e_h_2,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_675]) ).
tcf(c_3876,plain,
( node19(c_e_h_2,c_e,s2,s3)
| ~ trans(s2,s3) ),
inference(instantiation,[status(thm)],[c_2119]) ).
tcf(c_3968,plain,
( m_c_h_element_v_in2(c_e_h_2,c_e,s2)
| ~ node17(c_e_h_2,c_e,s2)
| ~ m_c_h_element_v_in1(c_e_h_2,c_e,s2) ),
inference(instantiation,[status(thm)],[c_2134]) ).
tcf(c_4050,plain,
( m_and_h_gate_v_out(c_e_h_2,c_i,s2)
| ~ m_c_h_element_v_in2(c_e_h_2,c_e,s2) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_4051,plain,
( m_c_h_element_v_in1(c_e_h_2,c_e,s2)
| ~ node17(c_e_h_2,c_e,s2)
| ~ m_c_h_element_v_in2(c_e_h_2,c_e,s2) ),
inference(instantiation,[status(thm)],[c_2135]) ).
tcf(c_4054,plain,
( m_c_h_element_v_in2(c_e_h_2,c_e,s2)
| m_c_h_element_v_in1(c_e_h_2,c_e,s2)
| ~ node16(c_e_h_2,c_e,s2) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_4141,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ node15(c_e_h_2,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_3562]) ).
tcf(c_4374,plain,
! [X0: $i,X1: $i] :
( m_and_h_gate_v_out(X0,c_i,X1)
| ~ m_and_h_gate_v_out(X0,c_i,s2)
| ~ node22(X0,c_i,X1,s2) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_4375,plain,
! [X0: $i,X1: $i] :
( node20(X0,c_i,X1)
| ~ m_and_h_gate_v_out(X0,c_i,s2)
| ~ node21(X0,c_i,X1,s2) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_4400,plain,
( node17(c_e_h_2,c_e,s2)
| node18(c_e_h_2,c_e,s2,s3)
| ~ node19(c_e_h_2,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_2063]) ).
tcf(c_4525,plain,
! [X0: $i] :
( m_and_h_gate_v_out(X0,c_i,s2)
| ~ m_c_h_element_v_in2(X0,c_e,s2) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_4535,plain,
! [X0: $i] :
( node20(X0,c_i,s1)
| ~ m_and_h_gate_v_out(X0,c_i,s2)
| ~ node21(X0,c_i,s1,s2) ),
inference(instantiation,[status(thm)],[c_4375]) ).
tcf(c_4536,plain,
! [X0: $i] :
( node22(X0,c_i,s1,s2)
| node21(X0,c_i,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_557]) ).
tcf(c_4552,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ node18(c_e_h_2,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_3561]) ).
tcf(c_4638,plain,
! [X0: $i] :
( m_and_h_gate_v_out(X0,c_i,s1)
| ~ m_and_h_gate_v_out(X0,c_i,s2)
| ~ node22(X0,c_i,s1,s2) ),
inference(instantiation,[status(thm)],[c_4374]) ).
tcf(c_4700,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s1)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ node15(c_e_h_2,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_2125]) ).
tcf(c_4879,plain,
! [X0: $i] :
( m_and_h_gate_v_in1(X0,c_i,s1)
| ~ node20(X0,c_i,s1) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_4910,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_1,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s4)
| ~ node22(c_e_h_1,c_r,X0,s4) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_4911,plain,
! [X0: $i] :
( node20(c_e_h_1,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s4)
| ~ node21(c_e_h_1,c_r,X0,s4) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_5033,plain,
( node20(c_e_h_1,c_r,s3)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s4)
| ~ node21(c_e_h_1,c_r,s3,s4) ),
inference(instantiation,[status(thm)],[c_4911]) ).
tcf(c_5034,plain,
( node22(c_e_h_1,c_r,s3,s4)
| node21(c_e_h_1,c_r,s3,s4)
| ~ trans(s3,s4) ),
inference(instantiation,[status(thm)],[c_585]) ).
tcf(c_5066,plain,
~ m_c_h_element_v_out(c_e_h_2,c_e,s0),
inference(instantiation,[status(thm)],[c_1464]) ).
tcf(c_5124,plain,
( m_and_h_gate_v_in1(c_e_h_1,c_r,s3)
| ~ node20(c_e_h_1,c_r,s3) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_5294,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s3)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s4)
| ~ node22(c_e_h_1,c_r,s3,s4) ),
inference(instantiation,[status(thm)],[c_4910]) ).
tcf(c_5419,plain,
( m_c_h_element_v_out(c_e_h_1,c_e,s3)
| ~ m_and_h_gate_v_in1(c_e_h_1,c_r,s3) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_5551,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_1,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s3)
| ~ node18(c_e_h_1,c_e,X0,s3) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_5553,plain,
! [X0: $i] :
( m_c_h_element_v_in1(c_e_h_1,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s3)
| ~ node14(c_e_h_1,c_e,X0,s3) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_5723,plain,
( m_c_h_element_v_out(c_e_h_1,c_e,s2)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s3)
| ~ node18(c_e_h_1,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_5551]) ).
tcf(c_5724,plain,
( node17(c_e_h_1,c_e,s2)
| node18(c_e_h_1,c_e,s2,s3)
| ~ node19(c_e_h_1,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_2063]) ).
tcf(c_5725,plain,
( m_c_h_element_v_in1(c_e_h_1,c_e,s2)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s3)
| ~ node14(c_e_h_1,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_5553]) ).
tcf(c_5726,plain,
( node16(c_e_h_1,c_e,s2)
| node15(c_e_h_1,c_e,s2,s3)
| node14(c_e_h_1,c_e,s2,s3)
| ~ node19(c_e_h_1,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_675]) ).
tcf(c_5889,plain,
( node19(c_e_h_1,c_e,s2,s3)
| ~ trans(s2,s3) ),
inference(instantiation,[status(thm)],[c_2119]) ).
tcf(c_5986,plain,
( m_c_h_element_v_in1(c_e_h_1,c_e,s2)
| ~ node17(c_e_h_1,c_e,s2)
| ~ m_c_h_element_v_in2(c_e_h_1,c_e,s2) ),
inference(instantiation,[status(thm)],[c_2135]) ).
tcf(c_5991,plain,
( m_c_h_element_v_in2(c_e_h_1,c_e,s2)
| ~ node17(c_e_h_1,c_e,s2)
| ~ m_c_h_element_v_in1(c_e_h_1,c_e,s2) ),
inference(instantiation,[status(thm)],[c_2134]) ).
tcf(c_6072,plain,
( m_and_h_gate_v_out(c_e_h_2,c_i,s1)
| ~ m_and_h_gate_v_out(c_e_h_2,c_i,s2)
| ~ node22(c_e_h_2,c_i,s1,s2) ),
inference(instantiation,[status(thm)],[c_4638]) ).
tcf(c_6138,plain,
( m_c_h_element_v_in2(c_e_h_1,c_e,s2)
| m_c_h_element_v_in1(c_e_h_1,c_e,s2)
| ~ node16(c_e_h_1,c_e,s2) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_6159,plain,
( node22(c_e_h_2,c_i,s1,s2)
| node21(c_e_h_2,c_i,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_4536]) ).
tcf(c_6260,plain,
( m_and_h_gate_v_out(c_e_h_1,c_i,s2)
| ~ m_c_h_element_v_in2(c_e_h_1,c_e,s2) ),
inference(instantiation,[status(thm)],[c_4525]) ).
tcf(c_6271,plain,
( m_c_h_element_v_out(c_e_h_1,c_e,s1)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s2)
| ~ node15(c_e_h_1,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_2125]) ).
tcf(c_6311,plain,
( node20(c_e_h_2,c_i,s1)
| ~ m_and_h_gate_v_out(c_e_h_2,c_i,s2)
| ~ node21(c_e_h_2,c_i,s1,s2) ),
inference(instantiation,[status(thm)],[c_4535]) ).
tcf(c_6492,plain,
( m_c_h_element_v_out(c_e_h_1,c_e,s2)
| ~ m_and_h_gate_v_in1(c_e_h_1,c_r,s2) ),
inference(instantiation,[status(thm)],[c_2043]) ).
tcf(c_6503,plain,
( m_and_h_gate_v_out(c_e_h_1,c_i,s1)
| ~ m_and_h_gate_v_out(c_e_h_1,c_i,s2)
| ~ node22(c_e_h_1,c_i,s1,s2) ),
inference(instantiation,[status(thm)],[c_4638]) ).
tcf(c_6509,plain,
( m_c_h_element_v_in1(c_e_h_1,c_e,s1)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s2)
| ~ node14(c_e_h_1,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_2058]) ).
tcf(c_6564,plain,
( m_and_h_gate_v_in1(c_e_h_2,c_i,s1)
| ~ node20(c_e_h_2,c_i,s1) ),
inference(instantiation,[status(thm)],[c_4879]) ).
tcf(c_6616,plain,
! [X0: $i,X1: $i] :
( node22(X0,X1,s0,s1)
| node21(X0,X1,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_6621,plain,
! [X0: $i,X1: $i] :
( node19(X0,X1,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_6622,plain,
! [X0: $i,X1: $i] :
( node22(X0,X1,s1,s2)
| node21(X0,X1,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_6627,plain,
! [X0: $i,X1: $i] :
( node19(X0,X1,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_350]) ).
tcf(c_6628,plain,
! [X0: $i,X1: $i] :
( node22(X0,X1,s2,s3)
| node21(X0,X1,s2,s3)
| ~ trans(s2,s3) ),
inference(instantiation,[status(thm)],[c_358]) ).
tcf(c_6678,plain,
! [X0: $i,X1: $i] :
( node16(X0,X1,s0)
| node15(X0,X1,s0,s1)
| node14(X0,X1,s0,s1)
| ~ node19(X0,X1,s0,s1) ),
inference(instantiation,[status(thm)],[c_348]) ).
tcf(c_6679,plain,
! [X0: $i,X1: $i] :
( node17(X0,X1,s0)
| node18(X0,X1,s0,s1)
| ~ node19(X0,X1,s0,s1) ),
inference(instantiation,[status(thm)],[c_349]) ).
tcf(c_6680,plain,
! [X0: $i,X1: $i] :
( node16(X0,X1,s1)
| node15(X0,X1,s1,s2)
| node14(X0,X1,s1,s2)
| ~ node19(X0,X1,s1,s2) ),
inference(instantiation,[status(thm)],[c_348]) ).
tcf(c_6681,plain,
! [X0: $i,X1: $i] :
( node17(X0,X1,s1)
| node18(X0,X1,s1,s2)
| ~ node19(X0,X1,s1,s2) ),
inference(instantiation,[status(thm)],[c_349]) ).
tcf(c_7393,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_1,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s3)
| ~ node15(c_e_h_1,c_e,X0,s3) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_7484,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_1,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s2)
| ~ node18(c_e_h_1,c_e,X0,s2) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_7526,plain,
( m_c_h_element_v_out(c_e_h_1,c_e,s1)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s2)
| ~ node18(c_e_h_1,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_7484]) ).
tcf(c_7527,plain,
( node17(c_e_h_1,c_e,s1)
| node18(c_e_h_1,c_e,s1,s2)
| ~ node19(c_e_h_1,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_6681]) ).
tcf(c_7529,plain,
( node16(c_e_h_1,c_e,s1)
| node15(c_e_h_1,c_e,s1,s2)
| node14(c_e_h_1,c_e,s1,s2)
| ~ node19(c_e_h_1,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_6680]) ).
tcf(c_7598,plain,
! [X0: $i] :
( node20(c_e_h_1,c_i,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_i,s2)
| ~ node21(c_e_h_1,c_i,X0,s2) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_7606,plain,
( node19(c_e_h_1,c_e,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_6627]) ).
tcf(c_7655,plain,
( m_c_h_element_v_in2(c_e_h_1,c_e,s1)
| ~ node17(c_e_h_1,c_e,s1)
| ~ m_c_h_element_v_in1(c_e_h_1,c_e,s1) ),
inference(instantiation,[status(thm)],[c_345]) ).
tcf(c_7656,plain,
( m_c_h_element_v_in1(c_e_h_1,c_e,s1)
| ~ node17(c_e_h_1,c_e,s1)
| ~ m_c_h_element_v_in2(c_e_h_1,c_e,s1) ),
inference(instantiation,[status(thm)],[c_344]) ).
tcf(c_7666,plain,
( node20(c_e_h_1,c_i,s1)
| ~ m_and_h_gate_v_out(c_e_h_1,c_i,s2)
| ~ node21(c_e_h_1,c_i,s1,s2) ),
inference(instantiation,[status(thm)],[c_7598]) ).
tcf(c_7667,plain,
( node22(c_e_h_1,c_i,s1,s2)
| node21(c_e_h_1,c_i,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_6622]) ).
tcf(c_7676,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_1,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s1)
| ~ node15(c_e_h_1,c_e,X0,s1) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_7677,plain,
! [X0: $i] :
( m_c_h_element_v_in1(c_e_h_1,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s1)
| ~ node14(c_e_h_1,c_e,X0,s1) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_7731,plain,
( m_and_h_gate_v_in1(c_e_h_1,c_i,s1)
| ~ node20(c_e_h_1,c_i,s1) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_7742,plain,
( m_c_h_element_v_in2(c_e_h_1,c_e,s1)
| m_c_h_element_v_in1(c_e_h_1,c_e,s1)
| ~ node16(c_e_h_1,c_e,s1) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_7779,plain,
( m_c_h_element_v_out(c_e_h_1,c_h,s1)
| ~ m_and_h_gate_v_in1(c_e_h_1,c_i,s1) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_7796,plain,
( m_c_h_element_v_out(c_e_h_1,c_e,s1)
| ~ m_and_h_gate_v_in1(c_e_h_1,c_r,s1) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_7803,plain,
( m_c_h_element_v_in1(c_e_h_1,c_e,s0)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s1)
| ~ node14(c_e_h_1,c_e,s0,s1) ),
inference(instantiation,[status(thm)],[c_7677]) ).
tcf(c_7804,plain,
( node16(c_e_h_1,c_e,s0)
| node15(c_e_h_1,c_e,s0,s1)
| node14(c_e_h_1,c_e,s0,s1)
| ~ node19(c_e_h_1,c_e,s0,s1) ),
inference(instantiation,[status(thm)],[c_6678]) ).
tcf(c_7851,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_2,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| ~ node22(c_e_h_2,c_r,X0,s3) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_7852,plain,
! [X0: $i] :
( node20(c_e_h_2,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| ~ node21(c_e_h_2,c_r,X0,s3) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_7879,plain,
( node19(c_e_h_1,c_e,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_6621]) ).
tcf(c_7884,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_1,c_i,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_i,s1)
| ~ node22(c_e_h_1,c_i,X0,s1) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_7885,plain,
! [X0: $i] :
( node20(c_e_h_1,c_i,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_i,s1)
| ~ node21(c_e_h_1,c_i,X0,s1) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_7936,plain,
( node22(c_e_h_1,c_r,s1,s2)
| node21(c_e_h_1,c_r,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_6622]) ).
tcf(c_7949,plain,
( node20(c_e_h_2,c_r,s2)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| ~ node21(c_e_h_2,c_r,s2,s3) ),
inference(instantiation,[status(thm)],[c_7852]) ).
tcf(c_7950,plain,
( node22(c_e_h_2,c_r,s2,s3)
| node21(c_e_h_2,c_r,s2,s3)
| ~ trans(s2,s3) ),
inference(instantiation,[status(thm)],[c_6628]) ).
tcf(c_7963,plain,
~ m_c_h_element_v_out(c_e_h_1,c_e,s0),
inference(instantiation,[status(thm)],[c_337]) ).
tcf(c_7970,plain,
( m_c_h_element_v_in2(c_e_h_1,c_e,s0)
| m_c_h_element_v_in1(c_e_h_1,c_e,s0)
| ~ node16(c_e_h_1,c_e,s0) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_7985,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_1,c_h,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_h,s1)
| ~ node18(c_e_h_1,c_h,X0,s1) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_7986,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_1,c_h,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_h,s1)
| ~ node15(c_e_h_1,c_h,X0,s1) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_7987,plain,
! [X0: $i] :
( m_c_h_element_v_in1(c_e_h_1,c_h,X0)
| ~ m_c_h_element_v_out(c_e_h_1,c_h,s1)
| ~ node14(c_e_h_1,c_h,X0,s1) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_8047,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| ~ node22(c_e_h_2,c_r,s2,s3) ),
inference(instantiation,[status(thm)],[c_7851]) ).
tcf(c_8051,plain,
( m_c_h_element_v_out(c_e_h_1,c_e,s0)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s1)
| ~ node15(c_e_h_1,c_e,s0,s1) ),
inference(instantiation,[status(thm)],[c_7676]) ).
tcf(c_8064,plain,
( m_c_h_element_v_out(c_e_h_1,c_h,s0)
| ~ m_c_h_element_v_out(c_e_h_1,c_h,s1)
| ~ node18(c_e_h_1,c_h,s0,s1) ),
inference(instantiation,[status(thm)],[c_7985]) ).
tcf(c_8065,plain,
( node17(c_e_h_1,c_h,s0)
| node18(c_e_h_1,c_h,s0,s1)
| ~ node19(c_e_h_1,c_h,s0,s1) ),
inference(instantiation,[status(thm)],[c_6679]) ).
tcf(c_8066,plain,
( m_c_h_element_v_in1(c_e_h_1,c_h,s0)
| ~ m_c_h_element_v_out(c_e_h_1,c_h,s1)
| ~ node14(c_e_h_1,c_h,s0,s1) ),
inference(instantiation,[status(thm)],[c_7987]) ).
tcf(c_8067,plain,
( node16(c_e_h_1,c_h,s0)
| node15(c_e_h_1,c_h,s0,s1)
| node14(c_e_h_1,c_h,s0,s1)
| ~ node19(c_e_h_1,c_h,s0,s1) ),
inference(instantiation,[status(thm)],[c_6678]) ).
tcf(c_8082,plain,
( m_and_h_gate_v_in1(c_e_h_2,c_r,s2)
| ~ node20(c_e_h_2,c_r,s2) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_8087,plain,
( m_and_h_gate_v_out(c_e_h_1,c_c,s0)
| ~ m_c_h_element_v_in1(c_e_h_1,c_e,s0) ),
inference(instantiation,[status(thm)],[c_245]) ).
tcf(c_8090,plain,
( m_and_h_gate_v_out(c_e_h_1,c_i,s0)
| ~ m_c_h_element_v_in2(c_e_h_1,c_e,s0) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_8118,plain,
( node19(c_e_h_1,c_h,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_6621]) ).
tcf(c_8130,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_2,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| ~ node22(c_e_h_2,c_r,X0,s2) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_8131,plain,
! [X0: $i] :
( node20(c_e_h_2,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| ~ node21(c_e_h_2,c_r,X0,s2) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_8138,plain,
~ m_and_h_gate_v_out(c_e_h_1,c_c,s0),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_8165,plain,
~ m_c_h_element_v_out(c_e_h_1,c_h,s0),
inference(instantiation,[status(thm)],[c_337]) ).
tcf(c_8172,plain,
( m_c_h_element_v_in2(c_e_h_1,c_h,s0)
| m_c_h_element_v_in1(c_e_h_1,c_h,s0)
| ~ node16(c_e_h_1,c_h,s0) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_8197,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_1,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s3)
| ~ node22(c_e_h_1,c_r,X0,s3) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_8198,plain,
! [X0: $i] :
( node20(c_e_h_1,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s3)
| ~ node21(c_e_h_1,c_r,X0,s3) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_8206,plain,
( node20(c_e_h_2,c_r,s1)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| ~ node21(c_e_h_2,c_r,s1,s2) ),
inference(instantiation,[status(thm)],[c_8131]) ).
tcf(c_8207,plain,
( node22(c_e_h_2,c_r,s1,s2)
| node21(c_e_h_2,c_r,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_6622]) ).
tcf(c_8273,plain,
( m_c_h_element_v_in2(c_e_h_1,c_h,s0)
| ~ node17(c_e_h_1,c_h,s0)
| ~ m_c_h_element_v_in1(c_e_h_1,c_h,s0) ),
inference(instantiation,[status(thm)],[c_345]) ).
tcf(c_8275,plain,
( m_or_h_gate_v_out(c_e_h_1,c_j,s0)
| ~ m_c_h_element_v_in2(c_e_h_1,c_h,s0) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_8288,plain,
( node20(c_e_h_1,c_r,s2)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s3)
| ~ node21(c_e_h_1,c_r,s2,s3) ),
inference(instantiation,[status(thm)],[c_8198]) ).
tcf(c_8289,plain,
( node22(c_e_h_1,c_r,s2,s3)
| node21(c_e_h_1,c_r,s2,s3)
| ~ trans(s2,s3) ),
inference(instantiation,[status(thm)],[c_6628]) ).
tcf(c_8301,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| ~ m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| ~ node22(c_e_h_2,c_r,s1,s2) ),
inference(instantiation,[status(thm)],[c_8130]) ).
tcf(c_8335,plain,
( m_c_h_element_v_out(c_e_h_1,c_h,s0)
| ~ m_c_h_element_v_out(c_e_h_1,c_h,s1)
| ~ node15(c_e_h_1,c_h,s0,s1) ),
inference(instantiation,[status(thm)],[c_7986]) ).
tcf(c_8349,plain,
( m_and_h_gate_v_in1(c_e_h_1,c_r,s2)
| ~ node20(c_e_h_1,c_r,s2) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_8354,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ m_and_h_gate_v_in1(c_e_h_2,c_r,s2) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_8377,plain,
( m_and_h_gate_v_out(c_e_h_1,c_i,s1)
| ~ m_c_h_element_v_in2(c_e_h_1,c_e,s1) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_8382,plain,
( node20(c_e_h_1,c_i,s0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_i,s1)
| ~ node21(c_e_h_1,c_i,s0,s1) ),
inference(instantiation,[status(thm)],[c_7885]) ).
tcf(c_8383,plain,
( node22(c_e_h_1,c_i,s0,s1)
| node21(c_e_h_1,c_i,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_6616]) ).
tcf(c_8408,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s2)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s3)
| ~ node22(c_e_h_1,c_r,s2,s3) ),
inference(instantiation,[status(thm)],[c_8197]) ).
tcf(c_8421,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_2,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ node18(c_e_h_2,c_e,X0,s2) ),
inference(instantiation,[status(thm)],[c_347]) ).
tcf(c_8423,plain,
! [X0: $i] :
( m_c_h_element_v_in1(c_e_h_2,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ node14(c_e_h_2,c_e,X0,s2) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_8438,plain,
( m_and_h_gate_v_in1(c_e_h_2,c_r,s1)
| ~ node20(c_e_h_2,c_r,s1) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_8469,plain,
( m_and_h_gate_v_in1(c_e_h_1,c_i,s0)
| ~ node20(c_e_h_1,c_i,s0) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_8548,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_1,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s2)
| ~ node22(c_e_h_1,c_r,X0,s2) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_8549,plain,
! [X0: $i] :
( node20(c_e_h_1,c_r,X0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s2)
| ~ node21(c_e_h_1,c_r,X0,s2) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_8559,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s1)
| ~ m_and_h_gate_v_in1(c_e_h_2,c_r,s1) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_8561,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s1)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ node18(c_e_h_2,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_8421]) ).
tcf(c_8562,plain,
( node17(c_e_h_2,c_e,s1)
| node18(c_e_h_2,c_e,s1,s2)
| ~ node19(c_e_h_2,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_6681]) ).
tcf(c_8563,plain,
( m_c_h_element_v_in1(c_e_h_2,c_e,s1)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ node14(c_e_h_2,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_8423]) ).
tcf(c_8564,plain,
( node16(c_e_h_2,c_e,s1)
| node15(c_e_h_2,c_e,s1,s2)
| node14(c_e_h_2,c_e,s1,s2)
| ~ node19(c_e_h_2,c_e,s1,s2) ),
inference(instantiation,[status(thm)],[c_6680]) ).
tcf(c_8573,plain,
( m_and_h_gate_v_out(c_e_h_1,c_i,s0)
| ~ m_and_h_gate_v_out(c_e_h_1,c_i,s1)
| ~ node22(c_e_h_1,c_i,s0,s1) ),
inference(instantiation,[status(thm)],[c_7884]) ).
tcf(c_8620,plain,
( m_and_h_gate_v_out(c_e_h_1,c_r,s1)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s2)
| ~ node22(c_e_h_1,c_r,s1,s2) ),
inference(instantiation,[status(thm)],[c_8548]) ).
tcf(c_8667,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_2,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s1)
| ~ node15(c_e_h_2,c_e,X0,s1) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_8668,plain,
! [X0: $i] :
( m_c_h_element_v_in1(c_e_h_2,c_e,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s1)
| ~ node14(c_e_h_2,c_e,X0,s1) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_8677,plain,
( node19(c_e_h_2,c_e,s1,s2)
| ~ trans(s1,s2) ),
inference(instantiation,[status(thm)],[c_6627]) ).
tcf(c_8697,plain,
( m_c_h_element_v_out(c_e_h_1,c_h,s0)
| ~ m_and_h_gate_v_in1(c_e_h_1,c_i,s0) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_8735,plain,
( m_c_h_element_v_in2(c_e_h_2,c_e,s1)
| ~ node17(c_e_h_2,c_e,s1)
| ~ m_c_h_element_v_in1(c_e_h_2,c_e,s1) ),
inference(instantiation,[status(thm)],[c_345]) ).
tcf(c_8738,plain,
( m_c_h_element_v_in2(c_e_h_2,c_e,s1)
| m_c_h_element_v_in1(c_e_h_2,c_e,s1)
| ~ node16(c_e_h_2,c_e,s1) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_8755,plain,
( m_c_h_element_v_in1(c_e_h_2,c_e,s0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s1)
| ~ node14(c_e_h_2,c_e,s0,s1) ),
inference(instantiation,[status(thm)],[c_8668]) ).
tcf(c_8756,plain,
( node16(c_e_h_2,c_e,s0)
| node15(c_e_h_2,c_e,s0,s1)
| node14(c_e_h_2,c_e,s0,s1)
| ~ node19(c_e_h_2,c_e,s0,s1) ),
inference(instantiation,[status(thm)],[c_6678]) ).
tcf(c_8760,plain,
( node20(c_e_h_1,c_r,s1)
| ~ m_and_h_gate_v_out(c_e_h_1,c_r,s2)
| ~ node21(c_e_h_1,c_r,s1,s2) ),
inference(instantiation,[status(thm)],[c_8549]) ).
tcf(c_8767,plain,
~ m_and_h_gate_v_out(c_e_h_1,c_i,s0),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_8785,plain,
( m_and_h_gate_v_in1(c_e_h_1,c_r,s1)
| ~ node20(c_e_h_1,c_r,s1) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_8851,plain,
( node19(c_e_h_2,c_e,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_6621]) ).
tcf(c_8858,plain,
( m_c_h_element_v_out(c_e_h_1,c_e,s2)
| ~ m_c_h_element_v_out(c_e_h_1,c_e,s3)
| ~ node15(c_e_h_1,c_e,s2,s3) ),
inference(instantiation,[status(thm)],[c_7393]) ).
tcf(c_8918,plain,
( m_c_h_element_v_in2(c_e_h_2,c_e,s0)
| m_c_h_element_v_in1(c_e_h_2,c_e,s0)
| ~ node16(c_e_h_2,c_e,s0) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_8937,plain,
( m_user_v_ack(c_e_h_1,c_u,s3)
| ~ node24(s3) ),
inference(instantiation,[status(thm)],[c_361]) ).
tcf(c_8941,plain,
( m_and_h_gate_v_out(c_e_h_2,c_c,s0)
| ~ m_c_h_element_v_in1(c_e_h_2,c_e,s0) ),
inference(instantiation,[status(thm)],[c_245]) ).
tcf(c_8944,plain,
( m_and_h_gate_v_out(c_e_h_2,c_i,s0)
| ~ m_c_h_element_v_in2(c_e_h_2,c_e,s0) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_8945,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s0)
| ~ m_c_h_element_v_out(c_e_h_2,c_e,s1)
| ~ node15(c_e_h_2,c_e,s0,s1) ),
inference(instantiation,[status(thm)],[c_8667]) ).
tcf(c_9000,plain,
( m_user_v_ack(c_e_h_2,c_u,s3)
| ~ node25(s3) ),
inference(instantiation,[status(thm)],[c_363]) ).
tcf(c_9041,plain,
~ m_and_h_gate_v_out(c_e_h_2,c_c,s0),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_9047,plain,
~ m_and_h_gate_v_out(c_e_h_2,c_i,s0),
inference(instantiation,[status(thm)],[c_351]) ).
tcf(c_9074,plain,
( m_c_h_element_v_out(c_e_h_2,c_h,s1)
| ~ m_and_h_gate_v_in1(c_e_h_2,c_i,s1) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_9099,plain,
( m_and_h_gate_v_out(c_e_h_2,c_i,s1)
| ~ m_c_h_element_v_in2(c_e_h_2,c_e,s1) ),
inference(instantiation,[status(thm)],[c_247]) ).
tcf(c_9130,plain,
( m_user_v_ack(c_e_h_1,c_u,s2)
| ~ node24(s2) ),
inference(instantiation,[status(thm)],[c_361]) ).
tcf(c_9136,plain,
! [X0: $i] :
( m_and_h_gate_v_out(c_e_h_2,c_i,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_i,s1)
| ~ node22(c_e_h_2,c_i,X0,s1) ),
inference(instantiation,[status(thm)],[c_357]) ).
tcf(c_9137,plain,
! [X0: $i] :
( node20(c_e_h_2,c_i,X0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_i,s1)
| ~ node21(c_e_h_2,c_i,X0,s1) ),
inference(instantiation,[status(thm)],[c_355]) ).
tcf(c_9173,plain,
( node20(c_e_h_2,c_i,s0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_i,s1)
| ~ node21(c_e_h_2,c_i,s0,s1) ),
inference(instantiation,[status(thm)],[c_9137]) ).
tcf(c_9174,plain,
( node22(c_e_h_2,c_i,s0,s1)
| node21(c_e_h_2,c_i,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_6616]) ).
tcf(c_9192,plain,
( m_and_h_gate_v_in1(c_e_h_2,c_i,s0)
| ~ node20(c_e_h_2,c_i,s0) ),
inference(instantiation,[status(thm)],[c_352]) ).
tcf(c_9193,plain,
( m_and_h_gate_v_out(c_e_h_2,c_i,s0)
| ~ m_and_h_gate_v_out(c_e_h_2,c_i,s1)
| ~ node22(c_e_h_2,c_i,s0,s1) ),
inference(instantiation,[status(thm)],[c_9136]) ).
tcf(c_9204,plain,
( m_c_h_element_v_out(c_e_h_2,c_h,s0)
| ~ m_and_h_gate_v_in1(c_e_h_2,c_i,s0) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_9220,plain,
! [X0: $i] :
( until2p29(X0)
| ~ xuntil2p30(s0)
| ~ succ(s0,X0) ),
inference(instantiation,[status(thm)],[c_371]) ).
tcf(c_9230,plain,
~ m_c_h_element_v_out(c_e_h_2,c_h,s0),
inference(instantiation,[status(thm)],[c_337]) ).
tcf(c_9246,plain,
! [X0: $i] :
( m_c_h_element_v_out(c_e_h_2,c_h,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_h,s1)
| ~ node15(c_e_h_2,c_h,X0,s1) ),
inference(instantiation,[status(thm)],[c_341]) ).
tcf(c_9247,plain,
! [X0: $i] :
( m_c_h_element_v_in1(c_e_h_2,c_h,X0)
| ~ m_c_h_element_v_out(c_e_h_2,c_h,s1)
| ~ node14(c_e_h_2,c_h,X0,s1) ),
inference(instantiation,[status(thm)],[c_339]) ).
tcf(c_9263,plain,
( until2p29(s1)
| ~ xuntil2p30(s0)
| ~ succ(s0,s1) ),
inference(instantiation,[status(thm)],[c_9220]) ).
tcf(c_9275,plain,
( m_c_h_element_v_in1(c_e_h_2,c_h,s0)
| ~ m_c_h_element_v_out(c_e_h_2,c_h,s1)
| ~ node14(c_e_h_2,c_h,s0,s1) ),
inference(instantiation,[status(thm)],[c_9247]) ).
tcf(c_9276,plain,
( node16(c_e_h_2,c_h,s0)
| node15(c_e_h_2,c_h,s0,s1)
| node14(c_e_h_2,c_h,s0,s1)
| ~ node19(c_e_h_2,c_h,s0,s1) ),
inference(instantiation,[status(thm)],[c_6678]) ).
tcf(c_9296,plain,
( node19(c_e_h_2,c_h,s0,s1)
| ~ trans(s0,s1) ),
inference(instantiation,[status(thm)],[c_6621]) ).
tcf(c_9311,plain,
( m_c_h_element_v_out(c_e_h_2,c_h,s0)
| ~ m_c_h_element_v_out(c_e_h_2,c_h,s1)
| ~ node15(c_e_h_2,c_h,s0,s1) ),
inference(instantiation,[status(thm)],[c_9246]) ).
tcf(c_9327,plain,
( m_c_h_element_v_in2(c_e_h_2,c_h,s0)
| m_c_h_element_v_in1(c_e_h_2,c_h,s0)
| ~ node16(c_e_h_2,c_h,s0) ),
inference(instantiation,[status(thm)],[c_342]) ).
tcf(c_9341,plain,
( xuntil2p30(s2)
| node26(s2)
| ~ until2p29(s2) ),
inference(instantiation,[status(thm)],[c_370]) ).
tcf(c_9343,plain,
( m_or_h_gate_v_out(c_e_h_2,c_g,s0)
| ~ m_c_h_element_v_in1(c_e_h_2,c_h,s0) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_9346,plain,
( m_or_h_gate_v_out(c_e_h_2,c_j,s0)
| ~ m_c_h_element_v_in2(c_e_h_2,c_h,s0) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_9373,plain,
! [X0: $i] :
( until2p29(X0)
| ~ xuntil2p30(s2)
| ~ succ(s2,X0) ),
inference(instantiation,[status(thm)],[c_371]) ).
tcf(c_9381,plain,
~ m_or_h_gate_v_out(c_e_h_2,c_g,s0),
inference(instantiation,[status(thm)],[c_307]) ).
tcf(c_9390,plain,
~ m_or_h_gate_v_out(c_e_h_2,c_j,s0),
inference(instantiation,[status(thm)],[c_307]) ).
tcf(c_9394,plain,
( until2p29(s3)
| ~ xuntil2p30(s2)
| ~ succ(s2,s3) ),
inference(instantiation,[status(thm)],[c_9373]) ).
tcf(c_9406,plain,
! [X0: $i] :
( until2p29(X0)
| ~ xuntil2p30(s3)
| ~ succ(s3,X0) ),
inference(instantiation,[status(thm)],[c_371]) ).
tcf(c_9409,plain,
( until2p29(s4)
| ~ xuntil2p30(s3)
| ~ succ(s3,s4) ),
inference(instantiation,[status(thm)],[c_9406]) ).
tcf(c_9412,plain,
( ~ xuntil2p30(s4)
| ~ last(s4) ),
inference(instantiation,[status(thm)],[c_372]) ).
tcf(c_9609,plain,
~ m_or_h_gate_v_out(c_e_h_1,c_j,s0),
inference(instantiation,[status(thm)],[c_307]) ).
tcf(c_9639,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_9609,c_9412,c_9409,c_9394,c_9390,c_9381,c_9346,c_9343,c_9341,c_9327,c_9311,c_9296,c_9276,c_9275,c_9263,c_9230,c_9204,c_9193,c_9192,c_9174,c_9173,c_9130,c_9099,c_9074,c_9047,c_9041,c_9000,c_8945,c_8944,c_8941,c_8937,c_8918,c_8858,c_8851,c_8785,c_8767,c_8760,c_8756,c_8755,c_8738,c_8735,c_8697,c_8677,c_8620,c_8573,c_8564,c_8563,c_8562,c_8561,c_8559,c_8469,c_8438,c_8408,c_8383,c_8382,c_8377,c_8354,c_8349,c_8335,c_8301,c_8289,c_8288,c_8275,c_8273,c_8207,c_8206,c_8172,c_8165,c_8138,c_8118,c_8090,c_8087,c_8082,c_8067,c_8066,c_8065,c_8064,c_8051,c_8047,c_7970,c_7963,c_7950,c_7949,c_7936,c_7879,c_7804,c_7803,c_7796,c_7779,c_7742,c_7731,c_7667,c_7666,c_7655,c_7656,c_7606,c_7529,c_7527,c_7526,c_6564,c_6509,c_6503,c_6492,c_6311,c_6271,c_6260,c_6159,c_6138,c_6072,c_5991,c_5986,c_5889,c_5726,c_5725,c_5724,c_5723,c_5419,c_5294,c_5124,c_5066,c_5034,c_5033,c_4700,c_4552,c_4400,c_4141,c_4054,c_4051,c_4050,c_3968,c_3876,c_3698,c_3697,c_3501,c_3409,c_3323,c_3250,c_3249,c_3141,c_3101,c_3096,c_3080,c_3039,c_3002,c_2951,c_2927,c_2855,c_2829,c_2792,c_2777,c_2740,c_2691,c_2620,c_2594,c_2485,c_2409,c_2385,c_2285,c_2242,c_2238,c_2190,c_2158,c_2144,c_2128,c_2072,c_2067,c_1970,c_1968,c_1967,c_1965,c_1929,c_1928,c_1927,c_1926,c_1793,c_1789,c_1735,c_1671,c_1667,c_1634,c_1595,c_1581,c_1554,c_1471,c_1401,c_1266,c_1262,c_1175,c_1170,c_1159,c_1085,c_1084,c_1067,c_1012,c_948,c_835,c_759,c_758,c_720,c_627,c_625,c_542,c_515,c_514,c_513,c_512,c_511,c_219,c_213,c_214,c_215,c_216,c_217,c_373]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV419-1.005 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.17/5.65 % Computer : n004.cluster.edu
% 0.17/5.65 % Model : x86_64 x86_64
% 0.17/5.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.65 % Memory : 8046.5625MB
% 0.17/5.65 % OS : Linux 6.8.0-71-generic
% 0.17/5.66 % CPULimit : 300
% 0.17/5.66 % WCLimit : 300
% 0.17/5.66 % DateTime : Thu Sep 24 19:33:43 UTC 2026
% 0.17/5.66 % CPUTime :
% 0.17/5.66 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.21/5.72 Running EPR theorem proving
% 0.21/5.72 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/5.74
% 0.21/5.74 % ======== iProver multi-core TPTP/SMT =========
% 0.21/5.74
% 0.21/5.74 % Detected problem language: tptp
% 0.21/5.76 % Proving...
% 4.72/7.07 % SZS status Started for theBenchmark.p
% 4.72/7.07 % SZS status Unsatisfiable for theBenchmark.p
% 4.72/7.07
% 4.72/7.07 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.72/7.07
% 4.72/7.07 % ------ iProver source info
% 4.72/7.07
% 4.72/7.07 % git: date: 2026-07-19 20:42:38 +0200
% 4.72/7.07 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.72/7.07 % git: non_committed_changes: false
% 4.72/7.07
% 4.72/7.07 % ------ Parsing...% successful
% 4.72/7.07
% 4.72/7.07
% 4.72/7.07 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 4.72/7.07 % ------ Proving...
% 4.72/7.07 % ------ Problem Properties
% 4.72/7.07
% 4.72/7.07 %
% 4.72/7.07 % clauses 161
% 4.72/7.07 % conjectures 15
% 4.72/7.07 % EPR 161
% 4.72/7.07 % Horn 137
% 4.72/7.07 % unary 17
% 4.72/7.07 % binary 92
% 4.72/7.07 % lits 366
% 4.72/7.07 % lits eq 0
% 4.72/7.07 % fd_pure 0
% 4.72/7.07 % fd_pseudo 0
% 4.72/7.07 % fd_cond 0
% 4.72/7.07 % fd_pseudo_cond 0
% 4.72/7.07 % AC symbols 0
% 4.72/7.07
% 4.72/7.07 % ------ Input Options Time Limit: Unbounded
% 4.72/7.07
% 4.72/7.07
% 4.72/7.07 % ------
% 4.72/7.07 % Current options:
% 4.72/7.07 % ------
% 4.72/7.07
% 4.72/7.07
% 4.72/7.07 %
% 4.72/7.07
% 4.72/7.07 % ------ Proving...
% 4.72/7.07 %
% 4.72/7.07
% 4.72/7.07 % SZS status Unsatisfiable for theBenchmark.p
% 4.72/7.07
% 4.72/7.07 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.72/7.08
% 4.72/7.08
%------------------------------------------------------------------------------