%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV419-1.005 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 : Sun Sep 27 09:02:18 AM UTC 2026
% Result : Unsatisfiable 115.86s 29.61s
% Output : CNFRefutation 115.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 132
% Number of leaves : 55
% Syntax : Number of clauses : 668 ( 52 unt; 491 nHn; 649 RR)
% Number of literals : 2715 ( 0 equ;1053 neg)
% Maximal clause size : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 37 ( 36 usr; 2 prp; 0-4 aty)
% Number of functors : 14 ( 14 usr; 14 con; 0-0 aty)
% Number of variables : 558 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(bound1,axiom,
succ(s0,s1) ).
cnf(bound2,axiom,
succ(s1,s2) ).
cnf(bound3,axiom,
succ(s2,s3) ).
cnf(bound4,axiom,
succ(s3,s4) ).
cnf(bound5,axiom,
last(s4) ).
cnf(bound6,axiom,
( trans(X0,X1)
| ~ succ(X0,X1) ) ).
cnf(bound7,axiom,
( trans(s4,s4)
| trans(s4,s3)
| trans(s4,s2)
| trans(s4,s1)
| trans(s4,s0)
| ~ loop ) ).
cnf(m_main_3,axiom,
~ 'm$ucell$uv$utoken'('c$ue$uh$u1',X0) ).
cnf(m_main_6,axiom,
~ 'm$ucell$uv$utoken'('c$ue$uh$u2',X0) ).
cnf(m_cell_20,axiom,
( 'm$uand$uh$ugate$uv$uout'(X0,'c$uc',X1)
| ~ 'm$uc$uh$uelement$uv$uin1'(X0,'c$ue',X1) ) ).
cnf(m_cell_54,axiom,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,'c$un',X1)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X0,'c$um',X1) ) ).
cnf(m_cell_56,axiom,
( 'm$ucell$uv$utoken'(X0,X1)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'(X0,'c$um',X1) ) ).
cnf(m_cell_57,axiom,
( 'm$uc$uh$uelement$uv$uout'(X0,'c$ue',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uin1'(X0,'c$un',X1) ) ).
cnf(m_cell_59,axiom,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,'c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X0,'c$un',X1) ) ).
cnf(m_cell_61,axiom,
( 'm$ucell$uv$utoken'(X0,X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'(X0,'c$un',X1) ) ).
cnf(m_cell_72,axiom,
( 'm$uc$uh$uelement$uv$uout'(X0,'c$ue',X1)
| ~ 'm$uand$uh$ugate$uv$uin1'(X0,'c$ur',X1) ) ).
cnf(m_cell_74,axiom,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,'c$um',X1)
| ~ 'm$uand$uh$ugate$uv$uin2'(X0,'c$ur',X1) ) ).
cnf(m_cell_81,axiom,
( 'm$uand$uh$ugate$uv$uout'(X0,'c$ur',X1)
| ~ 'm$uuser$uv$uack'(X0,'c$uu',X1) ) ).
cnf(m_and_h_gate_h_init_1,axiom,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'(X0,X1,s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,s0) ) ).
cnf(m_and_h_gate_h_init_2,axiom,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'(X0,X1,s0)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,s0) ) ).
cnf(m_and_h_gate_h_init_4,axiom,
( ~ node9(X0,X1,X2)
| 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X0,X1,X2) ) ).
cnf(m_and_h_gate_h_init_5,axiom,
( ~ node10(X0,X1,X3,X2)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uin1'(X0,X1,X3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X2) ) ).
cnf(m_and_h_gate_h_init_6,axiom,
( ~ node10(X0,X1,X3,X2)
| node9(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X2) ) ).
cnf(m_and_h_gate_h_init_7,axiom,
( ~ node11(X0,X1,X3,X2)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X2) ) ).
cnf(m_and_h_gate_h_init_8,axiom,
( ~ node11(X0,X1,X3,X2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X2) ) ).
cnf(m_and_h_gate_h_init_9,axiom,
( ~ trans(X2,X3)
| node11(X0,X1,X2,X3)
| node10(X0,X1,X2,X3) ) ).
cnf(m_c_h_element_1,axiom,
~ 'm$uc$uh$uelement$uv$uout'(X0,X1,s0) ).
cnf(m_c_h_element_3,axiom,
( ~ node14(X0,X1,X3,X2)
| 'm$uc$uh$uelement$uv$uin1'(X0,X1,X3)
| ~ 'm$uc$uh$uelement$uv$uout'(X0,X1,X2) ) ).
cnf(m_c_h_element_5,axiom,
( ~ node15(X0,X1,X3,X2)
| 'm$uc$uh$uelement$uv$uout'(X0,X1,X3)
| ~ 'm$uc$uh$uelement$uv$uout'(X0,X1,X2) ) ).
cnf(m_c_h_element_6,axiom,
( ~ node16(X0,X1,X2)
| 'm$uc$uh$uelement$uv$uin2'(X0,X1,X2)
| 'm$uc$uh$uelement$uv$uin1'(X0,X1,X2) ) ).
cnf(m_c_h_element_8,axiom,
( ~ node17(X0,X1,X2)
| ~ 'm$uc$uh$uelement$uv$uin2'(X0,X1,X2)
| 'm$uc$uh$uelement$uv$uin1'(X0,X1,X2) ) ).
cnf(m_c_h_element_11,axiom,
( ~ node18(X0,X1,X3,X2)
| 'm$uc$uh$uelement$uv$uout'(X0,X1,X3)
| ~ 'm$uc$uh$uelement$uv$uout'(X0,X1,X2) ) ).
cnf(m_c_h_element_12,axiom,
( ~ node19(X0,X1,X2,X3)
| node16(X0,X1,X2)
| node15(X0,X1,X2,X3)
| node14(X0,X1,X2,X3) ) ).
cnf(m_c_h_element_13,axiom,
( ~ node19(X0,X1,X2,X3)
| node18(X0,X1,X2,X3)
| node17(X0,X1,X2) ) ).
cnf(m_c_h_element_14,axiom,
( node19(X2,X3,X0,X1)
| ~ trans(X0,X1) ) ).
cnf(m_and_h_gate_1,axiom,
~ 'm$uand$uh$ugate$uv$uout'(X0,X1,s0) ).
cnf(m_and_h_gate_2,axiom,
( ~ node20(X0,X1,X2)
| 'm$uand$uh$ugate$uv$uin1'(X0,X1,X2) ) ).
cnf(m_and_h_gate_3,axiom,
( ~ node20(X0,X1,X2)
| 'm$uand$uh$ugate$uv$uin2'(X0,X1,X2) ) ).
cnf(m_and_h_gate_5,axiom,
( ~ node21(X0,X1,X3,X2)
| node20(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uv$uout'(X0,X1,X2) ) ).
cnf(m_and_h_gate_7,axiom,
( ~ node22(X0,X1,X3,X2)
| 'm$uand$uh$ugate$uv$uout'(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uv$uout'(X0,X1,X2) ) ).
cnf(m_and_h_gate_8,axiom,
( ~ trans(X2,X3)
| node22(X0,X1,X2,X3)
| node21(X0,X1,X2,X3) ) ).
cnf(prpty2,negated_conjecture,
( ~ node23(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u2','c$uu',X0) ) ).
cnf(prpty3,negated_conjecture,
( ~ node24(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u1','c$uu',X0) ) ).
cnf(prpty4,negated_conjecture,
( ~ node24(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u3','c$uu',X0) ) ).
cnf(prpty5,negated_conjecture,
( ~ node25(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u2','c$uu',X0) ) ).
cnf(prpty6,negated_conjecture,
( ~ node25(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u3','c$uu',X0) ) ).
cnf(prpty7,negated_conjecture,
( ~ node26(X0)
| node25(X0)
| node24(X0)
| node23(X0) ) ).
cnf(prpty8,negated_conjecture,
( ~ until27(X0)
| xuntil28(X0)
| node26(X0) ) ).
cnf(prpty9,negated_conjecture,
( ~ xuntil28(X1)
| ~ succ(X1,X0)
| until27(X0) ) ).
cnf(prpty10,negated_conjecture,
( ~ xuntil28(X0)
| ~ last(X0)
| loop ) ).
cnf(prpty11,negated_conjecture,
( ~ xuntil28(X1)
| ~ last(X1)
| ~ trans(X1,X0)
| until2p29(X0) ) ).
cnf(prpty12,negated_conjecture,
( ~ until2p29(X0)
| xuntil2p30(X0)
| node26(X0) ) ).
cnf(prpty13,negated_conjecture,
( ~ xuntil2p30(X1)
| ~ succ(X1,X0)
| until2p29(X0) ) ).
cnf(prpty14,negated_conjecture,
( ~ xuntil2p30(X0)
| ~ last(X0) ) ).
cnf(prpty15,negated_conjecture,
until27(s0) ).
cnf(c0,plain,
succ(s0,s1),
inference(clausification,[status(esa)],[bound1]) ).
cnf(c1,plain,
succ(s1,s2),
inference(clausification,[status(esa)],[bound2]) ).
cnf(c2,plain,
succ(s2,s3),
inference(clausification,[status(esa)],[bound3]) ).
cnf(c3,plain,
succ(s3,s4),
inference(clausification,[status(esa)],[bound4]) ).
cnf(c4,plain,
last(s4),
inference(clausification,[status(esa)],[bound5]) ).
cnf(c5,plain,
( trans(X0,X1)
| ~ succ(X0,X1) ),
inference(clausification,[status(esa)],[bound6]) ).
cnf(c6,plain,
( ~ loop
| trans(s4,s3)
| trans(s4,s4)
| trans(s4,s2)
| trans(s4,s1)
| trans(s4,s0) ),
inference(clausification,[status(esa)],[bound7]) ).
cnf(c9,plain,
~ 'm$ucell$uv$utoken'('c$ue$uh$u1',X0),
inference(clausification,[status(esa)],[m_main_3]) ).
cnf(c12,plain,
~ 'm$ucell$uv$utoken'('c$ue$uh$u2',X0),
inference(clausification,[status(esa)],[m_main_6]) ).
cnf(c35,plain,
( 'm$uand$uh$ugate$uv$uout'(X0,'c$uc',X1)
| ~ 'm$uc$uh$uelement$uv$uin1'(X0,'c$ue',X1) ),
inference(clausification,[status(esa)],[m_cell_20]) ).
cnf(c69,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,'c$un',X1)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X0,'c$um',X1) ),
inference(clausification,[status(esa)],[m_cell_54]) ).
cnf(c71,plain,
( 'm$ucell$uv$utoken'(X0,X1)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'(X0,'c$um',X1) ),
inference(clausification,[status(esa)],[m_cell_56]) ).
cnf(c72,plain,
( 'm$uc$uh$uelement$uv$uout'(X0,'c$ue',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uin1'(X0,'c$un',X1) ),
inference(clausification,[status(esa)],[m_cell_57]) ).
cnf(c74,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,'c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X0,'c$un',X1) ),
inference(clausification,[status(esa)],[m_cell_59]) ).
cnf(c76,plain,
( 'm$ucell$uv$utoken'(X0,X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'(X0,'c$un',X1) ),
inference(clausification,[status(esa)],[m_cell_61]) ).
cnf(c87,plain,
( 'm$uc$uh$uelement$uv$uout'(X0,'c$ue',X1)
| ~ 'm$uand$uh$ugate$uv$uin1'(X0,'c$ur',X1) ),
inference(clausification,[status(esa)],[m_cell_72]) ).
cnf(c89,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,'c$um',X1)
| ~ 'm$uand$uh$ugate$uv$uin2'(X0,'c$ur',X1) ),
inference(clausification,[status(esa)],[m_cell_74]) ).
cnf(c96,plain,
( 'm$uand$uh$ugate$uv$uout'(X0,'c$ur',X1)
| ~ 'm$uuser$uv$uack'(X0,'c$uu',X1) ),
inference(clausification,[status(esa)],[m_cell_81]) ).
cnf(c111,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'(X0,X1,s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,s0) ),
inference(clausification,[status(esa)],[m_and_h_gate_h_init_1]) ).
cnf(c112,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'(X0,X1,s0)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,s0) ),
inference(clausification,[status(esa)],[m_and_h_gate_h_init_2]) ).
cnf(c114,plain,
( ~ node9(X0,X1,X2)
| 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_h_init_4]) ).
cnf(c115,plain,
( ~ node10(X0,X1,X3,X2)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uin1'(X0,X1,X3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_h_init_5]) ).
cnf(c116,plain,
( ~ node10(X0,X1,X3,X2)
| node9(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_h_init_6]) ).
cnf(c117,plain,
( ~ node11(X0,X1,X3,X2)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_h_init_7]) ).
cnf(c118,plain,
( ~ node11(X0,X1,X3,X2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_h_init_8]) ).
cnf(c119,plain,
( ~ trans(X2,X3)
| node11(X0,X1,X2,X3)
| node10(X0,X1,X2,X3) ),
inference(clausification,[status(esa)],[m_and_h_gate_h_init_9]) ).
cnf(c127,plain,
~ 'm$uc$uh$uelement$uv$uout'(X0,X1,s0),
inference(clausification,[status(esa)],[m_c_h_element_1]) ).
cnf(c129,plain,
( ~ node14(X0,X1,X3,X2)
| 'm$uc$uh$uelement$uv$uin1'(X0,X1,X3)
| ~ 'm$uc$uh$uelement$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_c_h_element_3]) ).
cnf(c131,plain,
( ~ node15(X0,X1,X3,X2)
| 'm$uc$uh$uelement$uv$uout'(X0,X1,X3)
| ~ 'm$uc$uh$uelement$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_c_h_element_5]) ).
cnf(c132,plain,
( ~ node16(X0,X1,X2)
| 'm$uc$uh$uelement$uv$uin2'(X0,X1,X2)
| 'm$uc$uh$uelement$uv$uin1'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_c_h_element_6]) ).
cnf(c134,plain,
( ~ node17(X0,X1,X2)
| ~ 'm$uc$uh$uelement$uv$uin2'(X0,X1,X2)
| 'm$uc$uh$uelement$uv$uin1'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_c_h_element_8]) ).
cnf(c137,plain,
( ~ node18(X0,X1,X3,X2)
| 'm$uc$uh$uelement$uv$uout'(X0,X1,X3)
| ~ 'm$uc$uh$uelement$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_c_h_element_11]) ).
cnf(c138,plain,
( ~ node19(X0,X1,X2,X3)
| node16(X0,X1,X2)
| node15(X0,X1,X2,X3)
| node14(X0,X1,X2,X3) ),
inference(clausification,[status(esa)],[m_c_h_element_12]) ).
cnf(c139,plain,
( ~ node19(X0,X1,X2,X3)
| node18(X0,X1,X2,X3)
| node17(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_c_h_element_13]) ).
cnf(c140,plain,
( node19(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
inference(clausification,[status(esa)],[m_c_h_element_14]) ).
cnf(c141,plain,
~ 'm$uand$uh$ugate$uv$uout'(X0,X1,s0),
inference(clausification,[status(esa)],[m_and_h_gate_1]) ).
cnf(c142,plain,
( ~ node20(X0,X1,X2)
| 'm$uand$uh$ugate$uv$uin1'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_2]) ).
cnf(c143,plain,
( ~ node20(X0,X1,X2)
| 'm$uand$uh$ugate$uv$uin2'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_3]) ).
cnf(c145,plain,
( ~ node21(X0,X1,X3,X2)
| node20(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_5]) ).
cnf(c147,plain,
( ~ node22(X0,X1,X3,X2)
| 'm$uand$uh$ugate$uv$uout'(X0,X1,X3)
| ~ 'm$uand$uh$ugate$uv$uout'(X0,X1,X2) ),
inference(clausification,[status(esa)],[m_and_h_gate_7]) ).
cnf(c148,plain,
( ~ trans(X2,X3)
| node22(X0,X1,X2,X3)
| node21(X0,X1,X2,X3) ),
inference(clausification,[status(esa)],[m_and_h_gate_8]) ).
cnf(c150,plain,
( ~ node23(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u2','c$uu',X0) ),
inference(clausification,[status(esa)],[prpty2]) ).
cnf(c151,plain,
( ~ node24(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u1','c$uu',X0) ),
inference(clausification,[status(esa)],[prpty3]) ).
cnf(c152,plain,
( ~ node24(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u3','c$uu',X0) ),
inference(clausification,[status(esa)],[prpty4]) ).
cnf(c153,plain,
( ~ node25(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u2','c$uu',X0) ),
inference(clausification,[status(esa)],[prpty5]) ).
cnf(c154,plain,
( ~ node25(X0)
| 'm$uuser$uv$uack'('c$ue$uh$u3','c$uu',X0) ),
inference(clausification,[status(esa)],[prpty6]) ).
cnf(c155,plain,
( ~ node26(X0)
| node25(X0)
| node24(X0)
| node23(X0) ),
inference(clausification,[status(esa)],[prpty7]) ).
cnf(c156,plain,
( ~ until27(X0)
| xuntil28(X0)
| node26(X0) ),
inference(clausification,[status(esa)],[prpty8]) ).
cnf(c157,plain,
( ~ xuntil28(X1)
| ~ succ(X1,X0)
| until27(X0) ),
inference(clausification,[status(esa)],[prpty9]) ).
cnf(c158,plain,
( ~ xuntil28(X0)
| ~ last(X0)
| loop ),
inference(clausification,[status(esa)],[prpty10]) ).
cnf(c159,plain,
( ~ xuntil28(X1)
| ~ last(X1)
| ~ trans(X1,X0)
| until2p29(X0) ),
inference(clausification,[status(esa)],[prpty11]) ).
cnf(c160,plain,
( ~ until2p29(X0)
| xuntil2p30(X0)
| node26(X0) ),
inference(clausification,[status(esa)],[prpty12]) ).
cnf(c161,plain,
( ~ xuntil2p30(X1)
| ~ succ(X1,X0)
| until2p29(X0) ),
inference(clausification,[status(esa)],[prpty13]) ).
cnf(c162,plain,
( ~ xuntil2p30(X0)
| ~ last(X0) ),
inference(clausification,[status(esa)],[prpty14]) ).
cnf(c163,plain,
until27(s0),
inference(clausification,[status(esa)],[prpty15]) ).
cnf(d0,plain,
( ~ xuntil2p30(s3)
| until2p29(s4) ),
inference(resolution,[status(thm)],[c161,c3]) ).
cnf(d1,plain,
( ~ xuntil2p30(s2)
| until2p29(s3) ),
inference(resolution,[status(thm)],[c161,c2]) ).
cnf(d2,plain,
( ~ xuntil2p30(s1)
| until2p29(s2) ),
inference(resolution,[status(thm)],[c161,c1]) ).
cnf(d3,plain,
( ~ xuntil2p30(s0)
| until2p29(s1) ),
inference(resolution,[status(thm)],[c161,c0]) ).
cnf(d4,plain,
( ~ loop
| trans(s4,s4)
| trans(s4,s2)
| trans(s4,s1)
| trans(s4,s0)
| until2p29(s3)
| ~ xuntil28(s4)
| ~ last(s4) ),
inference(resolution,[status(thm)],[c159,c6]) ).
cnf(d5,plain,
( until2p29(s3)
| ~ xuntil28(s4)
| ~ loop
| trans(s4,s4)
| trans(s4,s2)
| trans(s4,s1)
| trans(s4,s0) ),
inference(resolution,[status(thm)],[c4,d4]) ).
cnf(d6,plain,
( until2p29(s2)
| ~ xuntil28(s4)
| ~ last(s4)
| until2p29(s3)
| ~ xuntil28(s4)
| ~ loop
| trans(s4,s4)
| trans(s4,s1)
| trans(s4,s0) ),
inference(resolution,[status(thm)],[d5,c159]) ).
cnf(d7,plain,
( until2p29(s3)
| until2p29(s2)
| ~ xuntil28(s4)
| ~ loop
| trans(s4,s4)
| trans(s4,s1)
| trans(s4,s0) ),
inference(resolution,[status(thm)],[c4,d6]) ).
cnf(d8,plain,
( until2p29(s1)
| ~ xuntil28(s4)
| ~ last(s4)
| until2p29(s3)
| until2p29(s2)
| ~ xuntil28(s4)
| ~ loop
| trans(s4,s4)
| trans(s4,s0) ),
inference(resolution,[status(thm)],[d7,c159]) ).
cnf(d9,plain,
( until2p29(s3)
| until2p29(s2)
| until2p29(s1)
| ~ xuntil28(s4)
| ~ loop
| trans(s4,s4)
| trans(s4,s0) ),
inference(resolution,[status(thm)],[c4,d8]) ).
cnf(d10,plain,
( until2p29(s4)
| ~ xuntil28(s4)
| ~ last(s4)
| until2p29(s3)
| until2p29(s2)
| until2p29(s1)
| ~ xuntil28(s4)
| ~ loop
| trans(s4,s0) ),
inference(resolution,[status(thm)],[d9,c159]) ).
cnf(d11,plain,
( until2p29(s4)
| until2p29(s3)
| until2p29(s2)
| until2p29(s1)
| ~ xuntil28(s4)
| ~ loop
| trans(s4,s0) ),
inference(resolution,[status(thm)],[c4,d10]) ).
cnf(d12,plain,
( until2p29(s0)
| ~ xuntil28(s4)
| ~ last(s4)
| until2p29(s4)
| until2p29(s3)
| until2p29(s2)
| until2p29(s1)
| ~ xuntil28(s4)
| ~ loop ),
inference(resolution,[status(thm)],[d11,c159]) ).
cnf(d13,plain,
( until2p29(s4)
| until2p29(s3)
| until2p29(s2)
| until2p29(s1)
| until2p29(s0)
| ~ xuntil28(s4)
| ~ loop ),
inference(resolution,[status(thm)],[c4,d12]) ).
cnf(d14,plain,
( ~ xuntil28(s3)
| until27(s4) ),
inference(resolution,[status(thm)],[c157,c3]) ).
cnf(d15,plain,
( ~ xuntil28(s2)
| until27(s3) ),
inference(resolution,[status(thm)],[c157,c2]) ).
cnf(d16,plain,
( ~ xuntil28(s1)
| until27(s2) ),
inference(resolution,[status(thm)],[c157,c1]) ).
cnf(d17,plain,
( ~ xuntil28(s0)
| until27(s1) ),
inference(resolution,[status(thm)],[c157,c0]) ).
cnf(d18,plain,
( xuntil28(s0)
| node26(s0) ),
inference(resolution,[status(thm)],[c156,c163]) ).
cnf(d19,plain,
( xuntil28(s0)
| node25(s0)
| node24(s0)
| node23(s0) ),
inference(resolution,[status(thm)],[c155,d18]) ).
cnf(d20,plain,
( ~ node24(X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u3','c$ur',X0) ),
inference(resolution,[status(thm)],[c96,c152]) ).
cnf(d21,plain,
~ node24(s0),
inference(resolution,[status(thm)],[d20,c141]) ).
cnf(d22,plain,
( xuntil28(s0)
| node25(s0)
| node23(s0) ),
inference(resolution,[status(thm)],[d21,d19]) ).
cnf(d23,plain,
( ~ node25(X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u3','c$ur',X0) ),
inference(resolution,[status(thm)],[c96,c154]) ).
cnf(d24,plain,
~ node25(s0),
inference(resolution,[status(thm)],[d23,c141]) ).
cnf(d25,plain,
( xuntil28(s0)
| node23(s0) ),
inference(resolution,[status(thm)],[d24,d22]) ).
cnf(d26,plain,
( ~ node23(X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0) ),
inference(resolution,[status(thm)],[c96,c150]) ).
cnf(d27,plain,
~ node23(s0),
inference(resolution,[status(thm)],[d26,c141]) ).
cnf(d28,plain,
xuntil28(s0),
inference(resolution,[status(thm)],[d27,d25]) ).
cnf(d29,plain,
until27(s1),
inference(resolution,[status(thm)],[d28,d17]) ).
cnf(d30,plain,
( xuntil28(s1)
| node26(s1) ),
inference(resolution,[status(thm)],[d29,c156]) ).
cnf(d31,plain,
( node25(s1)
| node24(s1)
| node23(s1)
| xuntil28(s1) ),
inference(resolution,[status(thm)],[d30,c155]) ).
cnf(d32,plain,
trans(s0,s1),
inference(resolution,[status(thm)],[c5,c0]) ).
cnf(d33,plain,
( ~ 'm$uand$uh$ugate$uv$uout'(X2,X3,X1)
| 'm$uand$uh$ugate$uv$uout'(X2,X3,X0)
| node21(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[c148,c147]) ).
cnf(d34,plain,
( node20(X2,X3,X0)
| ~ 'm$uand$uh$ugate$uv$uout'(X2,X3,X1)
| 'm$uand$uh$ugate$uv$uout'(X2,X3,X0)
| ~ 'm$uand$uh$ugate$uv$uout'(X2,X3,X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d33,c145]) ).
cnf(d35,plain,
( ~ node25(X1)
| node20('c$ue$uh$u3','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u3','c$ur',X0)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d34,d23]) ).
cnf(d36,plain,
( ~ node25(s1)
| node20('c$ue$uh$u3','c$ur',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u3','c$ur',s0) ),
inference(resolution,[status(thm)],[d35,d32]) ).
cnf(d37,plain,
( ~ node25(s1)
| node20('c$ue$uh$u3','c$ur',s0) ),
inference(resolution,[status(thm)],[c141,d36]) ).
cnf(d38,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u3','c$ur',s0)
| ~ node25(s1) ),
inference(resolution,[status(thm)],[d37,c142]) ).
cnf(d39,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u3','c$ue',s0)
| ~ node25(s1) ),
inference(resolution,[status(thm)],[d38,c87]) ).
cnf(d40,plain,
~ node25(s1),
inference(resolution,[status(thm)],[c127,d39]) ).
cnf(d41,plain,
( xuntil28(s1)
| node24(s1)
| node23(s1) ),
inference(resolution,[status(thm)],[d40,d31]) ).
cnf(d42,plain,
( ~ node24(X1)
| node20('c$ue$uh$u3','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u3','c$ur',X0)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d34,d20]) ).
cnf(d43,plain,
( ~ node24(s1)
| node20('c$ue$uh$u3','c$ur',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u3','c$ur',s0) ),
inference(resolution,[status(thm)],[d42,d32]) ).
cnf(d44,plain,
( ~ node24(s1)
| node20('c$ue$uh$u3','c$ur',s0) ),
inference(resolution,[status(thm)],[c141,d43]) ).
cnf(d45,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u3','c$ur',s0)
| ~ node24(s1) ),
inference(resolution,[status(thm)],[d44,c142]) ).
cnf(d46,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u3','c$ue',s0)
| ~ node24(s1) ),
inference(resolution,[status(thm)],[d45,c87]) ).
cnf(d47,plain,
~ node24(s1),
inference(resolution,[status(thm)],[c127,d46]) ).
cnf(d48,plain,
( xuntil28(s1)
| node23(s1) ),
inference(resolution,[status(thm)],[d47,d41]) ).
cnf(d49,plain,
( ~ node23(X1)
| node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d34,d26]) ).
cnf(d50,plain,
( ~ node23(s1)
| node20('c$ue$uh$u2','c$ur',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0) ),
inference(resolution,[status(thm)],[d49,d32]) ).
cnf(d51,plain,
( ~ node23(s1)
| node20('c$ue$uh$u2','c$ur',s0) ),
inference(resolution,[status(thm)],[c141,d50]) ).
cnf(d52,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u2','c$ur',s0)
| ~ node23(s1) ),
inference(resolution,[status(thm)],[d51,c142]) ).
cnf(d53,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s0)
| ~ node23(s1) ),
inference(resolution,[status(thm)],[d52,c87]) ).
cnf(d54,plain,
~ node23(s1),
inference(resolution,[status(thm)],[c127,d53]) ).
cnf(d55,plain,
xuntil28(s1),
inference(resolution,[status(thm)],[d54,d48]) ).
cnf(d56,plain,
until27(s2),
inference(resolution,[status(thm)],[d55,d16]) ).
cnf(d57,plain,
( xuntil28(s2)
| node26(s2) ),
inference(resolution,[status(thm)],[d56,c156]) ).
cnf(d58,plain,
( node25(s2)
| node24(s2)
| node23(s2)
| xuntil28(s2) ),
inference(resolution,[status(thm)],[d57,c155]) ).
cnf(d59,plain,
( 'm$ucell$uv$utoken'(X0,s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X0,'c$un',s0) ),
inference(resolution,[status(thm)],[c111,c76]) ).
cnf(d60,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X0)
| node10(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[c119,c118]) ).
cnf(d61,plain,
( node9(X2,X3,X0)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X0)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d60,c116]) ).
cnf(d62,plain,
trans(s1,s2),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(d63,plain,
( ~ node23(s2)
| node20('c$ue$uh$u2','c$ur',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d49,d62]) ).
cnf(d64,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',s1)
| ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d63,c143]) ).
cnf(d65,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d64,c89]) ).
cnf(d66,plain,
( node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ trans(X0,s1)
| ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d65,d61]) ).
cnf(d67,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d66,c114]) ).
cnf(d68,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d67,c69]) ).
cnf(d69,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d68,d59]) ).
cnf(d70,plain,
( ~ node23(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d69]) ).
cnf(d71,plain,
( ~ node23(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d70]) ).
cnf(d72,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d71,c112]) ).
cnf(d73,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d72,c71]) ).
cnf(d74,plain,
( ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[c12,d73]) ).
cnf(d75,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1)
| ~ node23(s2) ),
inference(resolution,[status(thm)],[d74,d34]) ).
cnf(d76,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u2','c$ur',X0)
| ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d75,c142]) ).
cnf(d77,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d76,c87]) ).
cnf(d78,plain,
( ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d77,c127]) ).
cnf(d79,plain,
( ~ node23(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d78]) ).
cnf(d80,plain,
~ node23(s2),
inference(resolution,[status(thm)],[c141,d79]) ).
cnf(d81,plain,
( xuntil28(s2)
| node25(s2)
| node24(s2) ),
inference(resolution,[status(thm)],[d80,d58]) ).
cnf(d82,plain,
( ~ node25(X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0) ),
inference(resolution,[status(thm)],[c96,c153]) ).
cnf(d83,plain,
( ~ node25(X1)
| node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d34,d82]) ).
cnf(d84,plain,
( ~ node25(s2)
| node20('c$ue$uh$u2','c$ur',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d83,d62]) ).
cnf(d85,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',s1)
| ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d84,c143]) ).
cnf(d86,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d85,c89]) ).
cnf(d87,plain,
( node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ trans(X0,s1)
| ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d86,d61]) ).
cnf(d88,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d87,c114]) ).
cnf(d89,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d88,c69]) ).
cnf(d90,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d89,d59]) ).
cnf(d91,plain,
( ~ node25(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d90]) ).
cnf(d92,plain,
( ~ node25(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d91]) ).
cnf(d93,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d92,c112]) ).
cnf(d94,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d93,c71]) ).
cnf(d95,plain,
( ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[c12,d94]) ).
cnf(d96,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1)
| ~ node25(s2) ),
inference(resolution,[status(thm)],[d95,d34]) ).
cnf(d97,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u2','c$ur',X0)
| ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d96,c142]) ).
cnf(d98,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d97,c87]) ).
cnf(d99,plain,
( ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d98,c127]) ).
cnf(d100,plain,
( ~ node25(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d99]) ).
cnf(d101,plain,
~ node25(s2),
inference(resolution,[status(thm)],[c141,d100]) ).
cnf(d102,plain,
( xuntil28(s2)
| node24(s2) ),
inference(resolution,[status(thm)],[d101,d81]) ).
cnf(d103,plain,
( ~ node24(X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0) ),
inference(resolution,[status(thm)],[c96,c151]) ).
cnf(d104,plain,
( ~ node24(X1)
| node20('c$ue$uh$u1','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d34,d103]) ).
cnf(d105,plain,
( ~ node24(s2)
| node20('c$ue$uh$u1','c$ur',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d104,d62]) ).
cnf(d106,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u1','c$ur',s1)
| ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d105,c143]) ).
cnf(d107,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d106,c89]) ).
cnf(d108,plain,
( node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| ~ trans(X0,s1)
| ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d107,d61]) ).
cnf(d109,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d108,c114]) ).
cnf(d110,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d109,c69]) ).
cnf(d111,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d110,d59]) ).
cnf(d112,plain,
( ~ node24(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c9,d111]) ).
cnf(d113,plain,
( ~ node24(s2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d112]) ).
cnf(d114,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u1','c$um',s0)
| ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d113,c112]) ).
cnf(d115,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d114,c71]) ).
cnf(d116,plain,
( ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[c9,d115]) ).
cnf(d117,plain,
( node20('c$ue$uh$u1','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1)
| ~ node24(s2) ),
inference(resolution,[status(thm)],[d116,d34]) ).
cnf(d118,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u1','c$ur',X0)
| ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d117,c142]) ).
cnf(d119,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d118,c87]) ).
cnf(d120,plain,
( ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d119,c127]) ).
cnf(d121,plain,
( ~ node24(s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d120]) ).
cnf(d122,plain,
~ node24(s2),
inference(resolution,[status(thm)],[c141,d121]) ).
cnf(d123,plain,
xuntil28(s2),
inference(resolution,[status(thm)],[d122,d102]) ).
cnf(d124,plain,
until27(s3),
inference(resolution,[status(thm)],[d123,d15]) ).
cnf(d125,plain,
( xuntil28(s3)
| node26(s3) ),
inference(resolution,[status(thm)],[d124,c156]) ).
cnf(d126,plain,
( node25(s3)
| node24(s3)
| node23(s3)
| xuntil28(s3) ),
inference(resolution,[status(thm)],[d125,c155]) ).
cnf(d127,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X1)
| node10(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[c119,c117]) ).
cnf(d128,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uin2'(X2,X3,X0)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uin1'(X2,X3,X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X1)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,X3,X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d127,c115]) ).
cnf(d129,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,'c$um',X0)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uin1'(X2,'c$un',X0)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,'c$un',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,'c$un',X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d128,c74]) ).
cnf(d130,plain,
( 'm$uc$uh$uelement$uv$uout'(X2,'c$ue',X0)
| ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,'c$un',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,'c$un',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X2,'c$um',X0)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d129,c72]) ).
cnf(d131,plain,
( 'm$ucell$uv$utoken'(X1,s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$un',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$um',s0)
| 'm$uc$uh$uelement$uv$uout'(X1,'c$ue',s0)
| ~ trans(s0,X0) ),
inference(resolution,[status(thm)],[d130,d59]) ).
cnf(d132,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$un',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$um',s0)
| 'm$ucell$uv$utoken'(X1,s0)
| ~ trans(s0,X0) ),
inference(resolution,[status(thm)],[c127,d131]) ).
cnf(d133,plain,
trans(s2,s3),
inference(resolution,[status(thm)],[c5,c2]) ).
cnf(d134,plain,
( ~ node23(s3)
| node20('c$ue$uh$u2','c$ur',s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d49,d133]) ).
cnf(d135,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',s2)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d134,c143]) ).
cnf(d136,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s2)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d135,c89]) ).
cnf(d137,plain,
( node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ trans(X0,s2)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d136,d61]) ).
cnf(d138,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d137,c114]) ).
cnf(d139,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d138,c69]) ).
cnf(d140,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ trans(s0,X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d139,d132]) ).
cnf(d141,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d140]) ).
cnf(d142,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d141,c112]) ).
cnf(d143,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d142,c71]) ).
cnf(d144,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d143]) ).
cnf(d145,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d144,d61]) ).
cnf(d146,plain,
( ~ node23(s3)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s1,s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d145,d32]) ).
cnf(d147,plain,
( ~ node23(s3)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d62,d146]) ).
cnf(d148,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d147,c114]) ).
cnf(d149,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d148,c69]) ).
cnf(d150,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d149,d59]) ).
cnf(d151,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d150]) ).
cnf(d152,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d32,d151]) ).
cnf(d153,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d152,c112]) ).
cnf(d154,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d153,c71]) ).
cnf(d155,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[c12,d154]) ).
cnf(d156,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2)
| ~ node23(s3) ),
inference(resolution,[status(thm)],[d155,d34]) ).
cnf(d157,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d156,c143]) ).
cnf(d158,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d157,c89]) ).
cnf(d159,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d158,d61]) ).
cnf(d160,plain,
( ~ node23(s3)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d159,d62]) ).
cnf(d161,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d160,c114]) ).
cnf(d162,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d161,c69]) ).
cnf(d163,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d162,d59]) ).
cnf(d164,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d163]) ).
cnf(d165,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d164]) ).
cnf(d166,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d165,c112]) ).
cnf(d167,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d166,c71]) ).
cnf(d168,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[c12,d167]) ).
cnf(d169,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1)
| ~ node23(s3) ),
inference(resolution,[status(thm)],[d168,d34]) ).
cnf(d170,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u2','c$ur',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d169,c142]) ).
cnf(d171,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d170,c87]) ).
cnf(d172,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d171,c127]) ).
cnf(d173,plain,
( ~ node23(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d172]) ).
cnf(d174,plain,
~ node23(s3),
inference(resolution,[status(thm)],[c141,d173]) ).
cnf(d175,plain,
( xuntil28(s3)
| node25(s3)
| node24(s3) ),
inference(resolution,[status(thm)],[d174,d126]) ).
cnf(d176,plain,
( ~ node25(s3)
| node20('c$ue$uh$u2','c$ur',s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d83,d133]) ).
cnf(d177,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',s2)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d176,c143]) ).
cnf(d178,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s2)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d177,c89]) ).
cnf(d179,plain,
( node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ trans(X0,s2)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d178,d61]) ).
cnf(d180,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d179,c114]) ).
cnf(d181,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d180,c69]) ).
cnf(d182,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ trans(s0,X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d181,d132]) ).
cnf(d183,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d182]) ).
cnf(d184,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d183,c112]) ).
cnf(d185,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d184,c71]) ).
cnf(d186,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d185]) ).
cnf(d187,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d186,d61]) ).
cnf(d188,plain,
( ~ node25(s3)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s1,s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d187,d32]) ).
cnf(d189,plain,
( ~ node25(s3)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d62,d188]) ).
cnf(d190,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d189,c114]) ).
cnf(d191,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d190,c69]) ).
cnf(d192,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d191,d59]) ).
cnf(d193,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d192]) ).
cnf(d194,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d32,d193]) ).
cnf(d195,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d194,c112]) ).
cnf(d196,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d195,c71]) ).
cnf(d197,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[c12,d196]) ).
cnf(d198,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2)
| ~ node25(s3) ),
inference(resolution,[status(thm)],[d197,d34]) ).
cnf(d199,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d198,c143]) ).
cnf(d200,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d199,c89]) ).
cnf(d201,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d200,d61]) ).
cnf(d202,plain,
( ~ node25(s3)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d201,d62]) ).
cnf(d203,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d202,c114]) ).
cnf(d204,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d203,c69]) ).
cnf(d205,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d204,d59]) ).
cnf(d206,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d205]) ).
cnf(d207,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d206]) ).
cnf(d208,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d207,c112]) ).
cnf(d209,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d208,c71]) ).
cnf(d210,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[c12,d209]) ).
cnf(d211,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1)
| ~ node25(s3) ),
inference(resolution,[status(thm)],[d210,d34]) ).
cnf(d212,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u2','c$ur',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d211,c142]) ).
cnf(d213,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d212,c87]) ).
cnf(d214,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d213,c127]) ).
cnf(d215,plain,
( ~ node25(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d214]) ).
cnf(d216,plain,
~ node25(s3),
inference(resolution,[status(thm)],[c141,d215]) ).
cnf(d217,plain,
( xuntil28(s3)
| node24(s3) ),
inference(resolution,[status(thm)],[d216,d175]) ).
cnf(d218,plain,
( ~ node24(s3)
| node20('c$ue$uh$u1','c$ur',s2)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d104,d133]) ).
cnf(d219,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u1','c$ur',s2)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d218,c143]) ).
cnf(d220,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s2)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d219,c89]) ).
cnf(d221,plain,
( node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| ~ trans(X0,s2)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d220,d61]) ).
cnf(d222,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d221,c114]) ).
cnf(d223,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d222,c69]) ).
cnf(d224,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ trans(s0,X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d223,d132]) ).
cnf(d225,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c9,d224]) ).
cnf(d226,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u1','c$um',s0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d225,c112]) ).
cnf(d227,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d226,c71]) ).
cnf(d228,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c9,d227]) ).
cnf(d229,plain,
( node9('c$ue$uh$u1','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X1)
| ~ trans(X1,X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d228,d61]) ).
cnf(d230,plain,
( ~ node24(s3)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s1,s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d229,d32]) ).
cnf(d231,plain,
( ~ node24(s3)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d62,d230]) ).
cnf(d232,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d231,c114]) ).
cnf(d233,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d232,c69]) ).
cnf(d234,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d233,d59]) ).
cnf(d235,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c9,d234]) ).
cnf(d236,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d32,d235]) ).
cnf(d237,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u1','c$um',s0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d236,c112]) ).
cnf(d238,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d237,c71]) ).
cnf(d239,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[c9,d238]) ).
cnf(d240,plain,
( node20('c$ue$uh$u1','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s2)
| ~ node24(s3) ),
inference(resolution,[status(thm)],[d239,d34]) ).
cnf(d241,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u1','c$ur',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d240,c143]) ).
cnf(d242,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d241,c89]) ).
cnf(d243,plain,
( node9('c$ue$uh$u1','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X1)
| ~ trans(X1,X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d242,d61]) ).
cnf(d244,plain,
( ~ node24(s3)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d243,d62]) ).
cnf(d245,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d244,c114]) ).
cnf(d246,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d245,c69]) ).
cnf(d247,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d246,d59]) ).
cnf(d248,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c9,d247]) ).
cnf(d249,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d248]) ).
cnf(d250,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u1','c$um',s0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d249,c112]) ).
cnf(d251,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d250,c71]) ).
cnf(d252,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[c9,d251]) ).
cnf(d253,plain,
( node20('c$ue$uh$u1','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1)
| ~ node24(s3) ),
inference(resolution,[status(thm)],[d252,d34]) ).
cnf(d254,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u1','c$ur',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d253,c142]) ).
cnf(d255,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d254,c87]) ).
cnf(d256,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d255,c127]) ).
cnf(d257,plain,
( ~ node24(s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d256]) ).
cnf(d258,plain,
~ node24(s3),
inference(resolution,[status(thm)],[c141,d257]) ).
cnf(d259,plain,
xuntil28(s3),
inference(resolution,[status(thm)],[d258,d217]) ).
cnf(d260,plain,
until27(s4),
inference(resolution,[status(thm)],[d259,d14]) ).
cnf(d261,plain,
( xuntil28(s4)
| node26(s4) ),
inference(resolution,[status(thm)],[d260,c156]) ).
cnf(d262,plain,
( node25(s4)
| node24(s4)
| node23(s4)
| xuntil28(s4) ),
inference(resolution,[status(thm)],[d261,c155]) ).
cnf(d263,plain,
( ~ trans(X2,X3)
| node18(X0,X1,X2,X3)
| node17(X0,X1,X2) ),
inference(resolution,[status(thm)],[c139,c140]) ).
cnf(d264,plain,
( ~ 'm$uc$uh$uelement$uv$uout'(X2,X3,X1)
| 'm$uc$uh$uelement$uv$uout'(X2,X3,X0)
| node17(X2,X3,X0)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d263,c137]) ).
cnf(d265,plain,
trans(s3,s4),
inference(resolution,[status(thm)],[c5,c3]) ).
cnf(d266,plain,
( ~ node25(s4)
| node20('c$ue$uh$u2','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d83,d265]) ).
cnf(d267,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',s3)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d266,c143]) ).
cnf(d268,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s3)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d267,c89]) ).
cnf(d269,plain,
( node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ trans(X0,s3)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d268,d61]) ).
cnf(d270,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d269,c114]) ).
cnf(d271,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d270,c69]) ).
cnf(d272,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$un',X2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$um',X0)
| 'm$uc$uh$uelement$uv$uout'(X1,'c$ue',X0)
| ~ trans(X0,X2)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$um',s0)
| 'm$ucell$uv$utoken'(X1,s0)
| ~ trans(s0,X0) ),
inference(resolution,[status(thm)],[d132,d130]) ).
cnf(d273,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$un',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'(X1,'c$um',s1)
| 'm$uc$uh$uelement$uv$uout'(X1,'c$ue',s1)
| 'm$ucell$uv$utoken'(X1,s0)
| ~ trans(s1,X0) ),
inference(resolution,[status(thm)],[d272,d32]) ).
cnf(d274,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ trans(s1,X0) ),
inference(resolution,[status(thm)],[d273,d271]) ).
cnf(d275,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s1,X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[c12,d274]) ).
cnf(d276,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s1,X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d275,d61]) ).
cnf(d277,plain,
( ~ node25(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s2,s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d276,d62]) ).
cnf(d278,plain,
( ~ node25(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d133,d277]) ).
cnf(d279,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d278,c114]) ).
cnf(d280,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d279,c69]) ).
cnf(d281,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ trans(s0,X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d280,d132]) ).
cnf(d282,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d281]) ).
cnf(d283,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s0,s1)
| ~ trans(s1,s2) ),
inference(factoring,[status(thm)],[d282]) ).
cnf(d284,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s1,s2) ),
inference(resolution,[status(thm)],[d32,d283]) ).
cnf(d285,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d62,d284]) ).
cnf(d286,plain,
( node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ trans(X0,s1)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d285,d61]) ).
cnf(d287,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d286,c114]) ).
cnf(d288,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d287,c69]) ).
cnf(d289,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d288,d59]) ).
cnf(d290,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d289]) ).
cnf(d291,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d32,d290]) ).
cnf(d292,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node25(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d291,c112]) ).
cnf(d293,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d292,c71]) ).
cnf(d294,plain,
( ~ node25(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[c12,d293]) ).
cnf(d295,plain,
( node17('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| ~ trans(X0,s1)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d294,d264]) ).
cnf(d296,plain,
( ~ 'm$uc$uh$uelement$uv$uin2'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| ~ node25(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d295,c134]) ).
cnf(d297,plain,
( ~ trans(X2,X3)
| node16(X0,X1,X2)
| node15(X0,X1,X2,X3)
| node14(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[c138,c140]) ).
cnf(d298,plain,
( 'm$uc$uh$uelement$uv$uout'(X2,X3,X0)
| ~ 'm$uc$uh$uelement$uv$uout'(X2,X3,X1)
| node16(X2,X3,X0)
| node14(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d297,c131]) ).
cnf(d299,plain,
( ~ 'm$uc$uh$uelement$uv$uout'(X2,X3,X1)
| 'm$uc$uh$uelement$uv$uin1'(X2,X3,X0)
| node16(X2,X3,X0)
| 'm$uc$uh$uelement$uv$uout'(X2,X3,X0)
| ~ 'm$uc$uh$uelement$uv$uout'(X2,X3,X1)
| ~ trans(X0,X1) ),
inference(resolution,[status(thm)],[d298,c129]) ).
cnf(d300,plain,
( node16('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| ~ trans(X0,s1)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d294,d299]) ).
cnf(d301,plain,
( 'm$uc$uh$uelement$uv$uin2'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| ~ node25(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d300,c132]) ).
cnf(d302,plain,
( ~ node25(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1)
| ~ node25(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d301,d296]) ).
cnf(d303,plain,
( 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$uc',X0)
| ~ node25(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d302,c35]) ).
cnf(d304,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$uc',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d303,c127]) ).
cnf(d305,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$uc',s0) ),
inference(resolution,[status(thm)],[d32,d304]) ).
cnf(d306,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[c141,d305]) ).
cnf(d307,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s3)
| ~ node25(s4) ),
inference(resolution,[status(thm)],[d306,d34]) ).
cnf(d308,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d307,c143]) ).
cnf(d309,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d308,c89]) ).
cnf(d310,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d309,d61]) ).
cnf(d311,plain,
( ~ node25(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d310,d133]) ).
cnf(d312,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d311,c114]) ).
cnf(d313,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d312,c69]) ).
cnf(d314,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ trans(s0,X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d313,d132]) ).
cnf(d315,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d314]) ).
cnf(d316,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d315,c112]) ).
cnf(d317,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d316,c71]) ).
cnf(d318,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d317]) ).
cnf(d319,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d318,d61]) ).
cnf(d320,plain,
( ~ node25(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s1,s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d319,d32]) ).
cnf(d321,plain,
( ~ node25(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d62,d320]) ).
cnf(d322,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d321,c114]) ).
cnf(d323,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d322,c69]) ).
cnf(d324,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d323,d59]) ).
cnf(d325,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d324]) ).
cnf(d326,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d32,d325]) ).
cnf(d327,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d326,c112]) ).
cnf(d328,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d327,c71]) ).
cnf(d329,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[c12,d328]) ).
cnf(d330,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2)
| ~ node25(s4) ),
inference(resolution,[status(thm)],[d329,d34]) ).
cnf(d331,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d330,c143]) ).
cnf(d332,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d331,c89]) ).
cnf(d333,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d332,d61]) ).
cnf(d334,plain,
( ~ node25(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d333,d62]) ).
cnf(d335,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d334,c114]) ).
cnf(d336,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d335,c69]) ).
cnf(d337,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d336,d59]) ).
cnf(d338,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d337]) ).
cnf(d339,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d338]) ).
cnf(d340,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d339,c112]) ).
cnf(d341,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d340,c71]) ).
cnf(d342,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[c12,d341]) ).
cnf(d343,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1)
| ~ node25(s4) ),
inference(resolution,[status(thm)],[d342,d34]) ).
cnf(d344,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u2','c$ur',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d343,c142]) ).
cnf(d345,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d344,c87]) ).
cnf(d346,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d345,c127]) ).
cnf(d347,plain,
( ~ node25(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d346]) ).
cnf(d348,plain,
~ node25(s4),
inference(resolution,[status(thm)],[c141,d347]) ).
cnf(d349,plain,
( xuntil28(s4)
| node24(s4)
| node23(s4) ),
inference(resolution,[status(thm)],[d348,d262]) ).
cnf(d350,plain,
( ~ node23(s4)
| node20('c$ue$uh$u2','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d49,d265]) ).
cnf(d351,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',s3)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d350,c143]) ).
cnf(d352,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s3)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d351,c89]) ).
cnf(d353,plain,
( node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ trans(X0,s3)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d352,d61]) ).
cnf(d354,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d353,c114]) ).
cnf(d355,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d354,c69]) ).
cnf(d356,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ trans(s1,X0) ),
inference(resolution,[status(thm)],[d273,d355]) ).
cnf(d357,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s1,X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[c12,d356]) ).
cnf(d358,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s1,X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d357,d61]) ).
cnf(d359,plain,
( ~ node23(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s2,s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d358,d62]) ).
cnf(d360,plain,
( ~ node23(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d133,d359]) ).
cnf(d361,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d360,c114]) ).
cnf(d362,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d361,c69]) ).
cnf(d363,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ trans(s0,X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d362,d132]) ).
cnf(d364,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d363]) ).
cnf(d365,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s0,s1)
| ~ trans(s1,s2) ),
inference(factoring,[status(thm)],[d364]) ).
cnf(d366,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s1,s2) ),
inference(resolution,[status(thm)],[d32,d365]) ).
cnf(d367,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d62,d366]) ).
cnf(d368,plain,
( node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ trans(X0,s1)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d367,d61]) ).
cnf(d369,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d368,c114]) ).
cnf(d370,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d369,c69]) ).
cnf(d371,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d370,d59]) ).
cnf(d372,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d371]) ).
cnf(d373,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d32,d372]) ).
cnf(d374,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node23(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d373,c112]) ).
cnf(d375,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d374,c71]) ).
cnf(d376,plain,
( ~ node23(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[c12,d375]) ).
cnf(d377,plain,
( node17('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| ~ trans(X0,s1)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d376,d264]) ).
cnf(d378,plain,
( ~ 'm$uc$uh$uelement$uv$uin2'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| ~ node23(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d377,c134]) ).
cnf(d379,plain,
( node16('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| ~ trans(X0,s1)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[d376,d299]) ).
cnf(d380,plain,
( 'm$uc$uh$uelement$uv$uin2'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| ~ node23(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d379,c132]) ).
cnf(d381,plain,
( ~ node23(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1)
| ~ node23(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d380,d378]) ).
cnf(d382,plain,
( 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$uc',X0)
| ~ node23(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d381,c35]) ).
cnf(d383,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$uc',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d382,c127]) ).
cnf(d384,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$uc',s0) ),
inference(resolution,[status(thm)],[d32,d383]) ).
cnf(d385,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s3) ),
inference(resolution,[status(thm)],[c141,d384]) ).
cnf(d386,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s3)
| ~ node23(s4) ),
inference(resolution,[status(thm)],[d385,d34]) ).
cnf(d387,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d386,c143]) ).
cnf(d388,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d387,c89]) ).
cnf(d389,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d388,d61]) ).
cnf(d390,plain,
( ~ node23(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d389,d133]) ).
cnf(d391,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d390,c114]) ).
cnf(d392,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d391,c69]) ).
cnf(d393,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ trans(s0,X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d392,d132]) ).
cnf(d394,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d393]) ).
cnf(d395,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d394,c112]) ).
cnf(d396,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d395,c71]) ).
cnf(d397,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c12,d396]) ).
cnf(d398,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d397,d61]) ).
cnf(d399,plain,
( ~ node23(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s1,s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d398,d32]) ).
cnf(d400,plain,
( ~ node23(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d62,d399]) ).
cnf(d401,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d400,c114]) ).
cnf(d402,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d401,c69]) ).
cnf(d403,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d402,d59]) ).
cnf(d404,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d403]) ).
cnf(d405,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d32,d404]) ).
cnf(d406,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d405,c112]) ).
cnf(d407,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[d406,c71]) ).
cnf(d408,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s2) ),
inference(resolution,[status(thm)],[c12,d407]) ).
cnf(d409,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2)
| ~ node23(s4) ),
inference(resolution,[status(thm)],[d408,d34]) ).
cnf(d410,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u2','c$ur',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d409,c143]) ).
cnf(d411,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d410,c89]) ).
cnf(d412,plain,
( node9('c$ue$uh$u2','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X1)
| ~ trans(X1,X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d411,d61]) ).
cnf(d413,plain,
( ~ node23(s4)
| node9('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d412,d62]) ).
cnf(d414,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u2','c$um',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d413,c114]) ).
cnf(d415,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$un',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d414,c69]) ).
cnf(d416,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d415,d59]) ).
cnf(d417,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c12,d416]) ).
cnf(d418,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u2','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d417]) ).
cnf(d419,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u2','c$um',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d418,c112]) ).
cnf(d420,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u2',s0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[d419,c71]) ).
cnf(d421,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s1) ),
inference(resolution,[status(thm)],[c12,d420]) ).
cnf(d422,plain,
( node20('c$ue$uh$u2','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1)
| ~ node23(s4) ),
inference(resolution,[status(thm)],[d421,d34]) ).
cnf(d423,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u2','c$ur',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d422,c142]) ).
cnf(d424,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u2','c$ue',X0)
| ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d423,c87]) ).
cnf(d425,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d424,c127]) ).
cnf(d426,plain,
( ~ node23(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u2','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d425]) ).
cnf(d427,plain,
~ node23(s4),
inference(resolution,[status(thm)],[c141,d426]) ).
cnf(d428,plain,
( xuntil28(s4)
| node24(s4) ),
inference(resolution,[status(thm)],[d427,d349]) ).
cnf(d429,plain,
( ~ node24(s4)
| node20('c$ue$uh$u1','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d104,d265]) ).
cnf(d430,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u1','c$ur',s3)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d429,c143]) ).
cnf(d431,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s3)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d430,c89]) ).
cnf(d432,plain,
( node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| ~ trans(X0,s3)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d431,d61]) ).
cnf(d433,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d432,c114]) ).
cnf(d434,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d433,c69]) ).
cnf(d435,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s3)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ trans(s1,X0) ),
inference(resolution,[status(thm)],[d273,d434]) ).
cnf(d436,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(s1,X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[c9,d435]) ).
cnf(d437,plain,
( node9('c$ue$uh$u1','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X1)
| ~ trans(X1,X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(s1,X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d436,d61]) ).
cnf(d438,plain,
( ~ node24(s4)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(s2,s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d437,d62]) ).
cnf(d439,plain,
( ~ node24(s4)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d133,d438]) ).
cnf(d440,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d439,c114]) ).
cnf(d441,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d440,c69]) ).
cnf(d442,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ trans(s0,X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d441,d132]) ).
cnf(d443,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c9,d442]) ).
cnf(d444,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(s0,s1)
| ~ trans(s1,s2) ),
inference(factoring,[status(thm)],[d443]) ).
cnf(d445,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(s1,s2) ),
inference(resolution,[status(thm)],[d32,d444]) ).
cnf(d446,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d62,d445]) ).
cnf(d447,plain,
( node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| ~ trans(X0,s1)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d446,d61]) ).
cnf(d448,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d447,c114]) ).
cnf(d449,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d448,c69]) ).
cnf(d450,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d449,d59]) ).
cnf(d451,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c9,d450]) ).
cnf(d452,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d32,d451]) ).
cnf(d453,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u1','c$um',s0)
| ~ node24(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d452,c112]) ).
cnf(d454,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d453,c71]) ).
cnf(d455,plain,
( ~ node24(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',s1)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[c9,d454]) ).
cnf(d456,plain,
( node17('c$ue$uh$u1','c$ue',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| ~ trans(X0,s1)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d455,d264]) ).
cnf(d457,plain,
( ~ 'm$uc$uh$uelement$uv$uin2'('c$ue$uh$u1','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u1','c$ue',X0)
| ~ node24(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d456,c134]) ).
cnf(d458,plain,
( node16('c$ue$uh$u1','c$ue',X0)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u1','c$ue',X0)
| ~ trans(X0,s1)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[d455,d299]) ).
cnf(d459,plain,
( 'm$uc$uh$uelement$uv$uin2'('c$ue$uh$u1','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u1','c$ue',X0)
| ~ node24(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u1','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d458,c132]) ).
cnf(d460,plain,
( ~ node24(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u1','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s1)
| ~ node24(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| 'm$uc$uh$uelement$uv$uin1'('c$ue$uh$u1','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d459,d457]) ).
cnf(d461,plain,
( 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$uc',X0)
| ~ node24(s4)
| 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d460,c35]) ).
cnf(d462,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$uc',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d461,c127]) ).
cnf(d463,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$uc',s0) ),
inference(resolution,[status(thm)],[d32,d462]) ).
cnf(d464,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s3) ),
inference(resolution,[status(thm)],[c141,d463]) ).
cnf(d465,plain,
( node20('c$ue$uh$u1','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s3)
| ~ node24(s4) ),
inference(resolution,[status(thm)],[d464,d34]) ).
cnf(d466,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u1','c$ur',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d465,c143]) ).
cnf(d467,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d466,c89]) ).
cnf(d468,plain,
( node9('c$ue$uh$u1','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X1)
| ~ trans(X1,X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s3) ),
inference(resolution,[status(thm)],[d467,d61]) ).
cnf(d469,plain,
( ~ node24(s4)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d468,d133]) ).
cnf(d470,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d469,c114]) ).
cnf(d471,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d470,c69]) ).
cnf(d472,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ trans(s0,X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d471,d132]) ).
cnf(d473,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c9,d472]) ).
cnf(d474,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u1','c$um',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d473,c112]) ).
cnf(d475,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d474,c71]) ).
cnf(d476,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[c9,d475]) ).
cnf(d477,plain,
( node9('c$ue$uh$u1','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X1)
| ~ trans(X1,X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d476,d61]) ).
cnf(d478,plain,
( ~ node24(s4)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s1,s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d477,d32]) ).
cnf(d479,plain,
( ~ node24(s4)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d62,d478]) ).
cnf(d480,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d479,c114]) ).
cnf(d481,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d480,c69]) ).
cnf(d482,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d481,d59]) ).
cnf(d483,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c9,d482]) ).
cnf(d484,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d32,d483]) ).
cnf(d485,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u1','c$um',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d484,c112]) ).
cnf(d486,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[d485,c71]) ).
cnf(d487,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s2) ),
inference(resolution,[status(thm)],[c9,d486]) ).
cnf(d488,plain,
( node20('c$ue$uh$u1','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s2)
| ~ node24(s4) ),
inference(resolution,[status(thm)],[d487,d34]) ).
cnf(d489,plain,
( 'm$uand$uh$ugate$uv$uin2'('c$ue$uh$u1','c$ur',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d488,c143]) ).
cnf(d490,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d489,c89]) ).
cnf(d491,plain,
( node9('c$ue$uh$u1','c$um',X1)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X1)
| ~ trans(X1,X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s2) ),
inference(resolution,[status(thm)],[d490,d61]) ).
cnf(d492,plain,
( ~ node24(s4)
| node9('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d491,d62]) ).
cnf(d493,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uin2'('c$ue$uh$u1','c$um',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d492,c114]) ).
cnf(d494,plain,
( ~ 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$un',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d493,c69]) ).
cnf(d495,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d494,d59]) ).
cnf(d496,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[c9,d495]) ).
cnf(d497,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uh$uinit$uv$uout'('c$ue$uh$u1','c$um',s0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d32,d496]) ).
cnf(d498,plain,
( 'm$uand$uh$ugate$uh$uinit$uv$uinit$uh$uout'('c$ue$uh$u1','c$um',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d497,c112]) ).
cnf(d499,plain,
( 'm$ucell$uv$utoken'('c$ue$uh$u1',s0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[d498,c71]) ).
cnf(d500,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s1) ),
inference(resolution,[status(thm)],[c9,d499]) ).
cnf(d501,plain,
( node20('c$ue$uh$u1','c$ur',X0)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1)
| ~ node24(s4) ),
inference(resolution,[status(thm)],[d500,d34]) ).
cnf(d502,plain,
( 'm$uand$uh$ugate$uv$uin1'('c$ue$uh$u1','c$ur',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d501,c142]) ).
cnf(d503,plain,
( 'm$uc$uh$uelement$uv$uout'('c$ue$uh$u1','c$ue',X0)
| ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',X0)
| ~ trans(X0,s1) ),
inference(resolution,[status(thm)],[d502,c87]) ).
cnf(d504,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s0)
| ~ trans(s0,s1) ),
inference(resolution,[status(thm)],[d503,c127]) ).
cnf(d505,plain,
( ~ node24(s4)
| 'm$uand$uh$ugate$uv$uout'('c$ue$uh$u1','c$ur',s0) ),
inference(resolution,[status(thm)],[d32,d504]) ).
cnf(d506,plain,
~ node24(s4),
inference(resolution,[status(thm)],[c141,d505]) ).
cnf(d507,plain,
xuntil28(s4),
inference(resolution,[status(thm)],[d506,d428]) ).
cnf(d508,plain,
( until2p29(s4)
| until2p29(s3)
| until2p29(s2)
| until2p29(s1)
| until2p29(s0)
| ~ loop ),
inference(resolution,[status(thm)],[d507,d13]) ).
cnf(d509,plain,
( loop
| ~ last(s4) ),
inference(resolution,[status(thm)],[d507,c158]) ).
cnf(d510,plain,
loop,
inference(resolution,[status(thm)],[c4,d509]) ).
cnf(d511,plain,
( until2p29(s4)
| until2p29(s3)
| until2p29(s2)
| until2p29(s1)
| until2p29(s0) ),
inference(resolution,[status(thm)],[d510,d508]) ).
cnf(d512,plain,
( xuntil2p30(s3)
| node26(s3)
| until2p29(s4)
| until2p29(s2)
| until2p29(s1)
| until2p29(s0) ),
inference(resolution,[status(thm)],[d511,c160]) ).
cnf(d513,plain,
( until2p29(s4)
| until2p29(s4)
| until2p29(s2)
| until2p29(s1)
| until2p29(s0)
| node26(s3) ),
inference(resolution,[status(thm)],[d512,d0]) ).
cnf(d514,plain,
( xuntil2p30(s2)
| node26(s2)
| until2p29(s4)
| until2p29(s1)
| until2p29(s0)
| node26(s3) ),
inference(resolution,[status(thm)],[d513,c160]) ).
cnf(d515,plain,
( until2p29(s3)
| until2p29(s4)
| until2p29(s1)
| until2p29(s0)
| node26(s3)
| node26(s2) ),
inference(resolution,[status(thm)],[d514,d1]) ).
cnf(d516,plain,
( xuntil2p30(s3)
| node26(s3)
| until2p29(s4)
| until2p29(s1)
| until2p29(s0)
| node26(s3)
| node26(s2) ),
inference(resolution,[status(thm)],[d515,c160]) ).
cnf(d517,plain,
( until2p29(s4)
| until2p29(s4)
| until2p29(s1)
| until2p29(s0)
| node26(s3)
| node26(s2) ),
inference(resolution,[status(thm)],[d516,d0]) ).
cnf(d518,plain,
( xuntil2p30(s1)
| node26(s1)
| until2p29(s4)
| until2p29(s0)
| node26(s3)
| node26(s2) ),
inference(resolution,[status(thm)],[d517,c160]) ).
cnf(d519,plain,
( until2p29(s2)
| until2p29(s4)
| until2p29(s0)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[d518,d2]) ).
cnf(d520,plain,
( xuntil2p30(s2)
| node26(s2)
| until2p29(s4)
| until2p29(s0)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[d519,c160]) ).
cnf(d521,plain,
( until2p29(s3)
| until2p29(s4)
| until2p29(s0)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[d520,d1]) ).
cnf(d522,plain,
( xuntil2p30(s3)
| node26(s3)
| until2p29(s4)
| until2p29(s0)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[d521,c160]) ).
cnf(d523,plain,
( until2p29(s4)
| until2p29(s4)
| until2p29(s0)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[d522,d0]) ).
cnf(d524,plain,
( xuntil2p30(s4)
| node26(s4)
| until2p29(s0)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[d523,c160]) ).
cnf(d525,plain,
( ~ last(s4)
| until2p29(s0)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[d524,c162]) ).
cnf(d526,plain,
( until2p29(s0)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[c4,d525]) ).
cnf(d527,plain,
( xuntil2p30(s0)
| node26(s0)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1) ),
inference(resolution,[status(thm)],[d526,c160]) ).
cnf(d528,plain,
( until2p29(s1)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d527,d3]) ).
cnf(d529,plain,
( xuntil2p30(s1)
| node26(s1)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d528,c160]) ).
cnf(d530,plain,
( until2p29(s2)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d529,d2]) ).
cnf(d531,plain,
( xuntil2p30(s2)
| node26(s2)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d530,c160]) ).
cnf(d532,plain,
( until2p29(s3)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d531,d1]) ).
cnf(d533,plain,
( xuntil2p30(s3)
| node26(s3)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d532,c160]) ).
cnf(d534,plain,
( until2p29(s4)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d533,d0]) ).
cnf(d535,plain,
( xuntil2p30(s4)
| node26(s4)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d534,c160]) ).
cnf(d536,plain,
( ~ last(s4)
| node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d535,c162]) ).
cnf(d537,plain,
( node26(s4)
| node26(s3)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[c4,d536]) ).
cnf(d538,plain,
( node25(s3)
| node24(s3)
| node23(s3)
| node26(s4)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d537,c155]) ).
cnf(d539,plain,
( node26(s4)
| node26(s2)
| node26(s1)
| node26(s0)
| node25(s3)
| node24(s3) ),
inference(resolution,[status(thm)],[d174,d538]) ).
cnf(d540,plain,
( node26(s4)
| node26(s2)
| node26(s1)
| node26(s0)
| node24(s3) ),
inference(resolution,[status(thm)],[d216,d539]) ).
cnf(d541,plain,
( node26(s4)
| node26(s2)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d258,d540]) ).
cnf(d542,plain,
( node25(s2)
| node24(s2)
| node23(s2)
| node26(s4)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d541,c155]) ).
cnf(d543,plain,
( node26(s4)
| node26(s1)
| node26(s0)
| node25(s2)
| node24(s2) ),
inference(resolution,[status(thm)],[d80,d542]) ).
cnf(d544,plain,
( node26(s4)
| node26(s1)
| node26(s0)
| node24(s2) ),
inference(resolution,[status(thm)],[d101,d543]) ).
cnf(d545,plain,
( node26(s4)
| node26(s1)
| node26(s0) ),
inference(resolution,[status(thm)],[d122,d544]) ).
cnf(d546,plain,
( node25(s1)
| node24(s1)
| node23(s1)
| node26(s4)
| node26(s0) ),
inference(resolution,[status(thm)],[d545,c155]) ).
cnf(d547,plain,
( node26(s4)
| node26(s0)
| node24(s1)
| node23(s1) ),
inference(resolution,[status(thm)],[d40,d546]) ).
cnf(d548,plain,
( node26(s4)
| node26(s0)
| node23(s1) ),
inference(resolution,[status(thm)],[d47,d547]) ).
cnf(d549,plain,
( node26(s4)
| node26(s0) ),
inference(resolution,[status(thm)],[d54,d548]) ).
cnf(d550,plain,
( node25(s4)
| node24(s4)
| node23(s4)
| node26(s0) ),
inference(resolution,[status(thm)],[d549,c155]) ).
cnf(d551,plain,
( node26(s0)
| node24(s4)
| node23(s4) ),
inference(resolution,[status(thm)],[d348,d550]) ).
cnf(d552,plain,
( node26(s0)
| node24(s4) ),
inference(resolution,[status(thm)],[d427,d551]) ).
cnf(d553,plain,
node26(s0),
inference(resolution,[status(thm)],[d506,d552]) ).
cnf(d554,plain,
( node25(s0)
| node24(s0)
| node23(s0) ),
inference(resolution,[status(thm)],[d553,c155]) ).
cnf(d555,plain,
( node25(s0)
| node23(s0) ),
inference(resolution,[status(thm)],[d21,d554]) ).
cnf(d556,plain,
node23(s0),
inference(resolution,[status(thm)],[d24,d555]) ).
cnf(d557,plain,
$false,
inference(resolution,[status(thm)],[d27,d556]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV419-1.005 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n009.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sat Sep 26 13:43:29 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 115.86/29.61 % SZS status Unsatisfiable for theBenchmark.p
% 115.86/29.61 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------