%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV419-1.005 : TPTP v9.3.1. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 : Tue Sep 29 01:21:54 PM UTC 2026
% Result : Unsatisfiable 2.11s 0.62s
% Output : Refutation 2.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 108
% Syntax : Number of formulae : 580 ( 105 unt; 51 def)
% Number of atoms : 1523 ( 0 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 1606 ( 663 ~; 892 |; 0 &)
% ( 51 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 89 ( 88 usr; 53 prp; 0-4 aty)
% Number of functors : 17 ( 17 usr; 17 con; 0-0 aty)
% Number of variables : 367 ( 0 sgn 367 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
succ(s0,s1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound1) ).
fof(f2,axiom,
succ(s1,s2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound2) ).
fof(f3,axiom,
succ(s2,s3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound3) ).
fof(f4,axiom,
succ(s3,s4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound4) ).
fof(f5,axiom,
last(s4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound5) ).
fof(f6,axiom,
! [X0,X1] :
( ~ succ(X0,X1)
| trans(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound6) ).
fof(f7,axiom,
( ~ loop
| trans(s4,s0)
| trans(s4,s1)
| trans(s4,s2)
| trans(s4,s3)
| trans(s4,s4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bound7) ).
fof(f10,axiom,
! [X0] : ~ m_cell_v_token(c_e_h_1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_3) ).
fof(f13,axiom,
! [X0] : ~ m_cell_v_token(c_e_h_2,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_main_6) ).
fof(f18,axiom,
! [X0,X1] :
( ~ m_mutex_h_half_v_inp(X0,c_a,X1)
| m_user_v_req(X0,c_u,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_2) ).
fof(f27,axiom,
! [X0,X1] :
( ~ m_and_h_gate_v_in1(X0,c_c,X1)
| m_mutex_h_half_v_out(X0,c_a,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_11) ).
fof(f36,axiom,
! [X0,X1] :
( ~ m_c_h_element_v_in1(X0,c_e,X1)
| m_and_h_gate_v_out(X0,c_c,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_20) ).
fof(f38,axiom,
! [X0,X1] :
( ~ m_c_h_element_v_in2(X0,c_e,X1)
| m_and_h_gate_v_out(X0,c_i,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_22) ).
fof(f48,axiom,
! [X0,X1] :
( ~ m_c_h_element_v_in1(X0,c_h,X1)
| m_or_h_gate_v_out(X0,c_g,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_32) ).
fof(f52,axiom,
! [X0,X1] :
( ~ m_and_h_gate_v_in1(X0,c_i,X1)
| m_c_h_element_v_out(X0,c_h,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_36) ).
fof(f72,axiom,
! [X0,X1] :
( ~ m_and_h_gate_h_init_v_init_h_out(X0,c_m,X1)
| m_cell_v_token(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_56) ).
fof(f88,axiom,
! [X0,X1] :
( ~ m_and_h_gate_v_in1(X0,c_r,X1)
| m_c_h_element_v_out(X0,c_e,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_72) ).
fof(f90,axiom,
! [X0,X1] :
( ~ m_and_h_gate_v_in2(X0,c_r,X1)
| m_and_h_gate_h_init_v_out(X0,c_m,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_74) ).
fof(f97,axiom,
! [X0,X1] :
( ~ m_user_v_ack(X0,c_u,X1)
| m_and_h_gate_v_out(X0,c_r,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_cell_81) ).
fof(f98,axiom,
! [X0,X1] : ~ m_or_h_gate_v_out(X0,X1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_or_h_gate_1) ).
fof(f106,axiom,
! [X0,X1] : ~ m_user_v_req(X0,X1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_user_1) ).
fof(f113,axiom,
! [X0,X1] :
( ~ m_and_h_gate_h_init_v_out(X0,X1,s0)
| m_and_h_gate_h_init_v_init_h_out(X0,X1,s0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_and_h_gate_h_init_2) ).
fof(f121,axiom,
! [X0,X1] : ~ m_mutex_h_half_v_out(X0,X1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_mutex_h_half_1) ).
fof(f123,axiom,
! [X2,X3,X0,X1] :
( ~ m_mutex_h_half_v_out(X0,X1,X2)
| m_mutex_h_half_v_inp(X0,X1,X3)
| ~ node12(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_mutex_h_half_3) ).
fof(f125,axiom,
! [X2,X3,X0,X1] :
( ~ m_mutex_h_half_v_out(X0,X1,X2)
| m_mutex_h_half_v_out(X0,X1,X3)
| ~ node13(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_mutex_h_half_5) ).
fof(f126,axiom,
! [X2,X3,X0,X1] :
( node12(X0,X1,X2,X3)
| node13(X0,X1,X2,X3)
| ~ trans(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_mutex_h_half_6) ).
fof(f128,axiom,
! [X0,X1] : ~ m_c_h_element_v_out(X0,X1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_1) ).
fof(f130,axiom,
! [X2,X3,X0,X1] :
( ~ m_c_h_element_v_out(X0,X1,X2)
| m_c_h_element_v_in1(X0,X1,X3)
| ~ node14(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_3) ).
fof(f132,axiom,
! [X2,X3,X0,X1] :
( ~ m_c_h_element_v_out(X0,X1,X2)
| m_c_h_element_v_out(X0,X1,X3)
| ~ node15(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_5) ).
fof(f133,axiom,
! [X2,X0,X1] :
( m_c_h_element_v_in1(X0,X1,X2)
| m_c_h_element_v_in2(X0,X1,X2)
| ~ node16(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_6) ).
fof(f135,axiom,
! [X2,X0,X1] :
( m_c_h_element_v_in1(X0,X1,X2)
| ~ m_c_h_element_v_in2(X0,X1,X2)
| ~ node17(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_8) ).
fof(f136,axiom,
! [X2,X0,X1] :
( ~ m_c_h_element_v_in1(X0,X1,X2)
| m_c_h_element_v_in2(X0,X1,X2)
| ~ node17(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_9) ).
fof(f138,axiom,
! [X2,X3,X0,X1] :
( ~ m_c_h_element_v_out(X0,X1,X2)
| m_c_h_element_v_out(X0,X1,X3)
| ~ node18(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_11) ).
fof(f139,axiom,
! [X2,X3,X0,X1] :
( node14(X0,X1,X2,X3)
| node15(X0,X1,X2,X3)
| node16(X0,X1,X2)
| ~ node19(X0,X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_12) ).
fof(f140,axiom,
! [X2,X3,X0,X1] :
( ~ node19(X0,X1,X2,X3)
| node18(X0,X1,X2,X3)
| node17(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_13) ).
fof(f141,axiom,
! [X2,X3,X0,X1] :
( node19(X2,X3,X0,X1)
| ~ trans(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_c_h_element_14) ).
fof(f142,axiom,
! [X0,X1] : ~ m_and_h_gate_v_out(X0,X1,s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_and_h_gate_1) ).
fof(f143,axiom,
! [X2,X0,X1] :
( m_and_h_gate_v_in1(X0,X1,X2)
| ~ node20(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_and_h_gate_2) ).
fof(f144,axiom,
! [X2,X0,X1] :
( m_and_h_gate_v_in2(X0,X1,X2)
| ~ node20(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_and_h_gate_3) ).
fof(f146,axiom,
! [X2,X3,X0,X1] :
( ~ m_and_h_gate_v_out(X0,X1,X2)
| node20(X0,X1,X3)
| ~ node21(X0,X1,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_and_h_gate_5) ).
fof(f148,axiom,
! [X2,X3,X0,X1] :
( ~ node22(X0,X1,X3,X2)
| m_and_h_gate_v_out(X0,X1,X3)
| ~ m_and_h_gate_v_out(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_and_h_gate_7) ).
fof(f149,axiom,
! [X2,X3,X0,X1] :
( node21(X0,X1,X2,X3)
| node22(X0,X1,X2,X3)
| ~ trans(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_and_h_gate_8) ).
fof(f150,negated_conjecture,
! [X0] :
( m_user_v_ack(c_e_h_1,c_u,X0)
| ~ node23(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty1) ).
fof(f151,negated_conjecture,
! [X0] :
( m_user_v_ack(c_e_h_2,c_u,X0)
| ~ node23(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty2) ).
fof(f152,negated_conjecture,
! [X0] :
( m_user_v_ack(c_e_h_1,c_u,X0)
| ~ node24(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty3) ).
fof(f153,negated_conjecture,
! [X0] :
( m_user_v_ack(c_e_h_3,c_u,X0)
| ~ node24(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty4) ).
fof(f154,negated_conjecture,
! [X0] :
( m_user_v_ack(c_e_h_2,c_u,X0)
| ~ node25(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty5) ).
fof(f155,negated_conjecture,
! [X0] :
( m_user_v_ack(c_e_h_3,c_u,X0)
| ~ node25(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty6) ).
fof(f156,negated_conjecture,
! [X0] :
( node23(X0)
| node24(X0)
| node25(X0)
| ~ node26(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty7) ).
fof(f157,negated_conjecture,
! [X0] :
( node26(X0)
| xuntil28(X0)
| ~ until27(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty8) ).
fof(f158,negated_conjecture,
! [X0,X1] :
( until27(X0)
| ~ succ(X1,X0)
| ~ xuntil28(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty9) ).
fof(f159,negated_conjecture,
! [X0] :
( loop
| ~ last(X0)
| ~ xuntil28(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty10) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( until2p29(X0)
| ~ trans(X1,X0)
| ~ last(X1)
| ~ xuntil28(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty11) ).
fof(f161,negated_conjecture,
! [X0] :
( ~ until2p29(X0)
| xuntil2p30(X0)
| node26(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty12) ).
fof(f162,negated_conjecture,
! [X0,X1] :
( ~ xuntil2p30(X1)
| ~ succ(X1,X0)
| until2p29(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty13) ).
fof(f163,negated_conjecture,
! [X0] :
( ~ last(X0)
| ~ xuntil2p30(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty14) ).
fof(f164,negated_conjecture,
until27(s0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prpty15) ).
fof(f165,plain,
~ last(s4),
inference(consistent_polarity_flipping,[],[f5]) ).
fof(f166,plain,
! [X0] : m_cell_v_token(c_e_h_1,X0),
inference(consistent_polarity_flipping,[],[f10]) ).
fof(f167,plain,
! [X0] : m_cell_v_token(c_e_h_2,X0),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f170,plain,
! [X0,X1] :
( ~ m_user_v_req(X0,c_u,X1)
| ~ m_mutex_h_half_v_inp(X0,c_a,X1) ),
inference(consistent_polarity_flipping,[],[f18]) ).
fof(f178,plain,
! [X0,X1] :
( ~ m_and_h_gate_v_in1(X0,c_c,X1)
| ~ m_mutex_h_half_v_out(X0,c_a,X1) ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f186,plain,
! [X0,X1] :
( m_c_h_element_v_in1(X0,c_e,X1)
| m_and_h_gate_v_out(X0,c_c,X1) ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f192,plain,
! [X0,X1] :
( m_c_h_element_v_in1(X0,c_h,X1)
| m_or_h_gate_v_out(X0,c_g,X1) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f194,plain,
! [X0,X1] :
( ~ m_c_h_element_v_out(X0,c_h,X1)
| ~ m_and_h_gate_v_in1(X0,c_i,X1) ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f208,plain,
! [X0,X1] :
( m_and_h_gate_h_init_v_init_h_out(X0,c_m,X1)
| ~ m_cell_v_token(X0,X1) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f222,plain,
! [X0,X1] :
( ~ m_c_h_element_v_out(X0,c_e,X1)
| ~ m_and_h_gate_v_in1(X0,c_r,X1) ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f224,plain,
! [X0,X1] :
( ~ m_and_h_gate_h_init_v_out(X0,c_m,X1)
| m_and_h_gate_v_in2(X0,c_r,X1) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f231,plain,
! [X0,X1] :
( m_user_v_ack(X0,c_u,X1)
| m_and_h_gate_v_out(X0,c_r,X1) ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f237,plain,
! [X0,X1] : m_user_v_req(X0,X1,s0),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f244,plain,
! [X0,X1] :
( ~ m_and_h_gate_h_init_v_init_h_out(X0,X1,s0)
| m_and_h_gate_h_init_v_out(X0,X1,s0) ),
inference(consistent_polarity_flipping,[],[f113]) ).
fof(f251,plain,
! [X0,X1] : m_mutex_h_half_v_out(X0,X1,s0),
inference(consistent_polarity_flipping,[],[f121]) ).
fof(f253,plain,
! [X2,X3,X0,X1] :
( node12(X0,X1,X3,X2)
| m_mutex_h_half_v_inp(X0,X1,X3)
| m_mutex_h_half_v_out(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f255,plain,
! [X2,X3,X0,X1] :
( ~ node13(X0,X1,X3,X2)
| ~ m_mutex_h_half_v_out(X0,X1,X3)
| m_mutex_h_half_v_out(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f256,plain,
! [X2,X3,X0,X1] :
( node13(X0,X1,X2,X3)
| ~ node12(X0,X1,X2,X3)
| ~ trans(X2,X3) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f258,plain,
! [X0,X1] : m_c_h_element_v_out(X0,X1,s0),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f260,plain,
! [X2,X3,X0,X1] :
( node14(X0,X1,X3,X2)
| ~ m_c_h_element_v_in1(X0,X1,X3)
| m_c_h_element_v_out(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f262,plain,
! [X2,X3,X0,X1] :
( node15(X0,X1,X3,X2)
| ~ m_c_h_element_v_out(X0,X1,X3)
| m_c_h_element_v_out(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f263,plain,
! [X2,X0,X1] :
( node16(X0,X1,X2)
| m_c_h_element_v_in2(X0,X1,X2)
| ~ m_c_h_element_v_in1(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f133]) ).
fof(f265,plain,
! [X2,X0,X1] :
( ~ node17(X0,X1,X2)
| ~ m_c_h_element_v_in2(X0,X1,X2)
| ~ m_c_h_element_v_in1(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f266,plain,
! [X2,X0,X1] :
( ~ node17(X0,X1,X2)
| m_c_h_element_v_in2(X0,X1,X2)
| m_c_h_element_v_in1(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f268,plain,
! [X2,X3,X0,X1] :
( ~ node18(X0,X1,X3,X2)
| ~ m_c_h_element_v_out(X0,X1,X3)
| m_c_h_element_v_out(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f269,plain,
! [X2,X3,X0,X1] :
( ~ node19(X0,X1,X2,X3)
| ~ node15(X0,X1,X2,X3)
| ~ node16(X0,X1,X2)
| ~ node14(X0,X1,X2,X3) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f270,plain,
! [X2,X0,X1] :
( node20(X0,X1,X2)
| m_and_h_gate_v_in1(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f271,plain,
! [X2,X0,X1] :
( node20(X0,X1,X2)
| ~ m_and_h_gate_v_in2(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f273,plain,
! [X2,X3,X0,X1] :
( node21(X0,X1,X3,X2)
| ~ node20(X0,X1,X3)
| ~ m_and_h_gate_v_out(X0,X1,X2) ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f274,plain,
! [X2,X3,X0,X1] :
( ~ node21(X0,X1,X2,X3)
| node22(X0,X1,X2,X3)
| ~ trans(X2,X3) ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f275,plain,
! [X0] :
( ~ m_user_v_ack(c_e_h_1,c_u,X0)
| node23(X0) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f276,plain,
! [X0] :
( ~ m_user_v_ack(c_e_h_2,c_u,X0)
| node23(X0) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f277,plain,
! [X0] :
( ~ m_user_v_ack(c_e_h_1,c_u,X0)
| node24(X0) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f278,plain,
! [X0] :
( ~ m_user_v_ack(c_e_h_3,c_u,X0)
| node24(X0) ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f279,plain,
! [X0] :
( ~ m_user_v_ack(c_e_h_2,c_u,X0)
| node25(X0) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f280,plain,
! [X0] :
( ~ m_user_v_ack(c_e_h_3,c_u,X0)
| node25(X0) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f281,plain,
! [X0] :
( ~ node25(X0)
| ~ node24(X0)
| ~ node23(X0)
| ~ node26(X0) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f282,plain,
! [X0] :
( until27(X0)
| xuntil28(X0)
| node26(X0) ),
inference(consistent_polarity_flipping,[],[f157]) ).
fof(f283,plain,
! [X0,X1] :
( ~ xuntil28(X1)
| ~ succ(X1,X0)
| ~ until27(X0) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f284,plain,
! [X0] :
( loop
| last(X0)
| ~ xuntil28(X0) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f285,plain,
! [X0,X1] :
( ~ xuntil28(X1)
| ~ trans(X1,X0)
| last(X1)
| until2p29(X0) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f286,plain,
! [X0] :
( ~ xuntil2p30(X0)
| last(X0) ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f287,plain,
~ until27(s0),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f290,definition,
( spl0_1
<=> ! [X0] :
( last(X0)
| ~ xuntil28(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f291,plain,
( ! [X0] :
( ~ xuntil28(X0)
| last(X0) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f293,definition,
( spl0_2
<=> loop ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f296,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f284,f293,f290]) ).
fof(f298,definition,
( spl0_3
<=> trans(s4,s4) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f300,plain,
( trans(s4,s4)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f298]) ).
fof(f302,definition,
( spl0_4
<=> trans(s4,s3) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f304,plain,
( trans(s4,s3)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f306,definition,
( spl0_5
<=> trans(s4,s2) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f308,plain,
( trans(s4,s2)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f310,definition,
( spl0_6
<=> trans(s4,s1) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f312,plain,
( trans(s4,s1)
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f314,definition,
( spl0_7
<=> trans(s4,s0) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f316,plain,
( trans(s4,s0)
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f314]) ).
fof(f317,plain,
( spl0_3
| spl0_4
| spl0_5
| spl0_6
| spl0_7
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f7,f293,f314,f310,f306,f302,f298]) ).
fof(f318,plain,
( xuntil28(s0)
| node26(s0) ),
inference(resolution,[],[f282,f287]) ).
fof(f320,definition,
( spl0_8
<=> node26(s0) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f321,plain,
( ~ node26(s0)
| spl0_8 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f324,definition,
( spl0_9
<=> xuntil28(s0) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f326,plain,
( xuntil28(s0)
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f324]) ).
fof(f327,plain,
( spl0_8
| spl0_9 ),
inference(avatar_split_clause,[],[f318,f324,f320]) ).
fof(f328,plain,
trans(s0,s1),
inference(resolution,[],[f6,f1]) ).
fof(f329,plain,
trans(s1,s2),
inference(resolution,[],[f6,f2]) ).
fof(f330,plain,
trans(s2,s3),
inference(resolution,[],[f6,f3]) ).
fof(f331,plain,
trans(s3,s4),
inference(resolution,[],[f6,f4]) ).
fof(f340,plain,
! [X0] : ~ m_mutex_h_half_v_inp(X0,c_a,s0),
inference(resolution,[],[f170,f237]) ).
fof(f356,plain,
! [X0] : ~ m_and_h_gate_v_in1(X0,c_i,s0),
inference(resolution,[],[f194,f258]) ).
fof(f366,plain,
! [X0] : ~ m_and_h_gate_v_in1(X0,c_r,s0),
inference(resolution,[],[f222,f258]) ).
fof(f367,plain,
! [X0] :
( m_and_h_gate_v_out(c_e_h_1,c_r,X0)
| node24(X0) ),
inference(resolution,[],[f231,f277]) ).
fof(f368,plain,
! [X0] :
( m_and_h_gate_v_out(c_e_h_1,c_r,X0)
| node23(X0) ),
inference(resolution,[],[f231,f275]) ).
fof(f369,plain,
! [X0] :
( m_and_h_gate_v_out(c_e_h_2,c_r,X0)
| node25(X0) ),
inference(resolution,[],[f231,f279]) ).
fof(f370,plain,
! [X0] :
( m_and_h_gate_v_out(c_e_h_2,c_r,X0)
| node23(X0) ),
inference(resolution,[],[f231,f276]) ).
fof(f371,plain,
! [X0] :
( m_and_h_gate_v_out(c_e_h_3,c_r,X0)
| node25(X0) ),
inference(resolution,[],[f231,f280]) ).
fof(f372,plain,
! [X0] :
( m_and_h_gate_v_out(c_e_h_3,c_r,X0)
| node24(X0) ),
inference(resolution,[],[f231,f278]) ).
fof(f374,plain,
! [X0] :
( ~ m_cell_v_token(X0,s0)
| m_and_h_gate_h_init_v_out(X0,c_m,s0) ),
inference(resolution,[],[f244,f208]) ).
fof(f377,plain,
node24(s0),
inference(resolution,[],[f367,f142]) ).
fof(f380,plain,
node23(s0),
inference(resolution,[],[f368,f142]) ).
fof(f387,plain,
node25(s0),
inference(resolution,[],[f369,f142]) ).
fof(f388,plain,
( ~ node24(s0)
| ~ node23(s0)
| ~ node26(s0) ),
inference(resolution,[],[f387,f281]) ).
fof(f389,plain,
( ~ node23(s0)
| ~ node26(s0) ),
inference(forward_subsumption_resolution,[],[f388,f377]) ).
fof(f390,plain,
~ node26(s0),
inference(forward_subsumption_resolution,[],[f389,f380]) ).
fof(f393,plain,
~ spl0_8,
inference(avatar_split_clause,[],[f390,f320]) ).
fof(f395,plain,
( ! [X0] :
( ~ until27(X0)
| ~ succ(s0,X0) )
| ~ spl0_9 ),
inference(resolution,[],[f326,f283]) ).
fof(f406,plain,
( ! [X0] :
( ~ succ(s0,X0)
| xuntil28(X0)
| node26(X0) )
| ~ spl0_9 ),
inference(resolution,[],[f395,f282]) ).
fof(f413,plain,
! [X2,X3,X0,X1] :
( ~ node12(X0,X1,X2,X3)
| ~ trans(X2,X3)
| ~ m_mutex_h_half_v_out(X0,X1,X2)
| m_mutex_h_half_v_out(X0,X1,X3) ),
inference(resolution,[],[f256,f255]) ).
fof(f415,plain,
( xuntil28(s1)
| node26(s1)
| ~ spl0_9 ),
inference(resolution,[],[f406,f1]) ).
fof(f417,definition,
( spl0_12
<=> node26(s1) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f418,plain,
( ~ node26(s1)
| spl0_12 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f421,definition,
( spl0_13
<=> xuntil28(s1) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f423,plain,
( xuntil28(s1)
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f424,plain,
( spl0_12
| spl0_13
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f415,f324,f421,f417]) ).
fof(f426,plain,
m_and_h_gate_h_init_v_out(c_e_h_1,c_m,s0),
inference(resolution,[],[f374,f166]) ).
fof(f427,plain,
m_and_h_gate_h_init_v_out(c_e_h_2,c_m,s0),
inference(resolution,[],[f374,f167]) ).
fof(f428,plain,
! [X2,X3,X0,X1] :
( ~ node20(X0,X1,X2)
| ~ trans(X2,X3)
| node22(X0,X1,X2,X3)
| ~ m_and_h_gate_v_out(X0,X1,X3) ),
inference(resolution,[],[f274,f273]) ).
fof(f429,plain,
! [X2,X3,X0,X1] :
( node18(X0,X1,X2,X3)
| node17(X0,X1,X2)
| ~ trans(X2,X3) ),
inference(resolution,[],[f140,f141]) ).
fof(f431,plain,
m_and_h_gate_v_in2(c_e_h_1,c_r,s0),
inference(resolution,[],[f426,f224]) ).
fof(f437,plain,
m_and_h_gate_v_in2(c_e_h_2,c_r,s0),
inference(resolution,[],[f427,f224]) ).
fof(f441,plain,
! [X2,X3,X0,X1] :
( ~ node16(X0,X1,X2)
| ~ node15(X0,X1,X2,X3)
| ~ node14(X0,X1,X2,X3)
| ~ trans(X2,X3) ),
inference(resolution,[],[f269,f141]) ).
fof(f464,plain,
! [X2,X3,X0,X1] :
( ~ m_c_h_element_v_out(X0,X1,X2)
| ~ trans(X2,X3)
| node17(X0,X1,X2)
| m_c_h_element_v_out(X0,X1,X3) ),
inference(resolution,[],[f429,f268]) ).
fof(f468,plain,
! [X2,X3,X0,X1] :
( ~ trans(X0,X1)
| ~ m_mutex_h_half_v_out(X2,X3,X0)
| m_mutex_h_half_v_out(X2,X3,X1)
| m_mutex_h_half_v_inp(X2,X3,X0)
| m_mutex_h_half_v_out(X2,X3,X1) ),
inference(resolution,[],[f413,f253]) ).
fof(f470,plain,
! [X2,X3,X0,X1] :
( ~ trans(X0,X1)
| ~ m_mutex_h_half_v_out(X2,X3,X0)
| m_mutex_h_half_v_out(X2,X3,X1)
| m_mutex_h_half_v_inp(X2,X3,X0) ),
inference(duplicate_literal_removal,[],[f468]) ).
fof(f474,plain,
! [X2,X3,X0,X1] :
( node22(X2,X3,X0,X1)
| ~ trans(X0,X1)
| ~ m_and_h_gate_v_out(X2,X3,X1)
| ~ m_and_h_gate_v_in2(X2,X3,X0) ),
inference(resolution,[],[f428,f271]) ).
fof(f475,plain,
! [X2,X3,X0,X1] :
( node22(X2,X3,X0,X1)
| ~ trans(X0,X1)
| ~ m_and_h_gate_v_out(X2,X3,X1)
| m_and_h_gate_v_in1(X2,X3,X0) ),
inference(resolution,[],[f428,f270]) ).
fof(f477,plain,
! [X2,X3,X0,X1] :
( ~ node15(X0,X1,X2,X3)
| ~ node14(X0,X1,X2,X3)
| ~ trans(X2,X3)
| m_c_h_element_v_in2(X0,X1,X2)
| ~ m_c_h_element_v_in1(X0,X1,X2) ),
inference(resolution,[],[f441,f263]) ).
fof(f502,plain,
! [X2,X0,X1] :
( ~ trans(s0,X0)
| node17(X1,X2,s0)
| m_c_h_element_v_out(X1,X2,X0) ),
inference(resolution,[],[f464,f258]) ).
fof(f504,plain,
! [X0,X1] :
( ~ m_mutex_h_half_v_out(X0,X1,s0)
| m_mutex_h_half_v_out(X0,X1,s1)
| m_mutex_h_half_v_inp(X0,X1,s0) ),
inference(resolution,[],[f470,f328]) ).
fof(f509,plain,
! [X0,X1] :
( m_mutex_h_half_v_inp(X0,X1,s0)
| m_mutex_h_half_v_out(X0,X1,s1) ),
inference(forward_subsumption_resolution,[],[f504,f251]) ).
fof(f514,plain,
! [X2,X3,X0,X1] :
( ~ trans(X0,X1)
| ~ m_and_h_gate_v_out(X2,X3,X1)
| ~ m_and_h_gate_v_in2(X2,X3,X0)
| m_and_h_gate_v_out(X2,X3,X0)
| ~ m_and_h_gate_v_out(X2,X3,X1) ),
inference(resolution,[],[f474,f148]) ).
fof(f516,plain,
! [X2,X3,X0,X1] :
( ~ trans(X0,X1)
| ~ m_and_h_gate_v_out(X2,X3,X1)
| ~ m_and_h_gate_v_in2(X2,X3,X0)
| m_and_h_gate_v_out(X2,X3,X0) ),
inference(duplicate_literal_removal,[],[f514]) ).
fof(f517,plain,
! [X2,X3,X0,X1] :
( ~ trans(X0,X1)
| ~ m_and_h_gate_v_out(X2,X3,X1)
| m_and_h_gate_v_in1(X2,X3,X0)
| m_and_h_gate_v_out(X2,X3,X0)
| ~ m_and_h_gate_v_out(X2,X3,X1) ),
inference(resolution,[],[f475,f148]) ).
fof(f519,plain,
! [X2,X3,X0,X1] :
( ~ trans(X0,X1)
| ~ m_and_h_gate_v_out(X2,X3,X1)
| m_and_h_gate_v_in1(X2,X3,X0)
| m_and_h_gate_v_out(X2,X3,X0) ),
inference(duplicate_literal_removal,[],[f517]) ).
fof(f526,plain,
! [X2,X3,X0,X1] :
( ~ node14(X0,X1,X2,X3)
| ~ trans(X2,X3)
| m_c_h_element_v_in2(X0,X1,X2)
| ~ m_c_h_element_v_in1(X0,X1,X2)
| ~ m_c_h_element_v_out(X0,X1,X2)
| m_c_h_element_v_out(X0,X1,X3) ),
inference(resolution,[],[f477,f262]) ).
fof(f528,plain,
! [X2,X3,X0,X1] :
( ~ m_c_h_element_v_out(X0,X1,X2)
| m_c_h_element_v_in2(X0,X1,X2)
| ~ m_c_h_element_v_in1(X0,X1,X2)
| ~ trans(X2,X3)
| m_c_h_element_v_out(X0,X1,X3) ),
inference(forward_subsumption_resolution,[],[f526,f260]) ).
fof(f529,plain,
! [X0] : m_mutex_h_half_v_out(X0,c_a,s1),
inference(resolution,[],[f509,f340]) ).
fof(f550,plain,
! [X0,X1] :
( node17(X0,X1,s0)
| m_c_h_element_v_out(X0,X1,s1) ),
inference(resolution,[],[f502,f328]) ).
fof(f648,plain,
! [X0,X1] :
( ~ m_and_h_gate_v_out(X0,X1,s1)
| ~ m_and_h_gate_v_in2(X0,X1,s0)
| m_and_h_gate_v_out(X0,X1,s0) ),
inference(resolution,[],[f516,f328]) ).
fof(f653,plain,
! [X0,X1] :
( ~ m_and_h_gate_v_out(X0,X1,s1)
| ~ m_and_h_gate_v_in2(X0,X1,s0) ),
inference(forward_subsumption_resolution,[],[f648,f142]) ).
fof(f654,plain,
! [X0,X1] :
( ~ m_and_h_gate_v_out(X0,X1,s1)
| m_and_h_gate_v_in1(X0,X1,s0)
| m_and_h_gate_v_out(X0,X1,s0) ),
inference(resolution,[],[f519,f328]) ).
fof(f655,plain,
! [X0,X1] :
( m_and_h_gate_v_in1(X0,X1,s1)
| ~ m_and_h_gate_v_out(X0,X1,s2)
| m_and_h_gate_v_out(X0,X1,s1) ),
inference(resolution,[],[f519,f329]) ).
fof(f656,plain,
! [X0,X1] :
( m_and_h_gate_v_in1(X0,X1,s2)
| ~ m_and_h_gate_v_out(X0,X1,s3)
| m_and_h_gate_v_out(X0,X1,s2) ),
inference(resolution,[],[f519,f330]) ).
fof(f657,plain,
! [X0,X1] :
( m_and_h_gate_v_in1(X0,X1,s3)
| ~ m_and_h_gate_v_out(X0,X1,s4)
| m_and_h_gate_v_out(X0,X1,s3) ),
inference(resolution,[],[f519,f331]) ).
fof(f659,plain,
! [X0,X1] :
( ~ m_and_h_gate_v_out(X0,X1,s1)
| m_and_h_gate_v_in1(X0,X1,s0) ),
inference(forward_subsumption_resolution,[],[f654,f142]) ).
fof(f673,plain,
! [X2,X0,X1] :
( ~ trans(s0,X2)
| ~ m_c_h_element_v_in1(X0,X1,s0)
| m_c_h_element_v_in2(X0,X1,s0)
| m_c_h_element_v_out(X0,X1,X2) ),
inference(resolution,[],[f528,f258]) ).
fof(f679,plain,
! [X0,X1] :
( ~ m_c_h_element_v_in2(X0,X1,s0)
| m_c_h_element_v_out(X0,X1,s1)
| ~ m_c_h_element_v_in1(X0,X1,s0) ),
inference(resolution,[],[f550,f265]) ).
fof(f684,plain,
( ~ m_and_h_gate_v_in2(c_e_h_1,c_r,s0)
| node24(s1) ),
inference(resolution,[],[f653,f367]) ).
fof(f685,plain,
( ~ m_and_h_gate_v_in2(c_e_h_2,c_r,s0)
| node23(s1) ),
inference(resolution,[],[f653,f370]) ).
fof(f686,plain,
( ~ m_and_h_gate_v_in2(c_e_h_2,c_r,s0)
| node25(s1) ),
inference(resolution,[],[f653,f369]) ).
fof(f690,definition,
( spl0_29
<=> node25(s1) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f692,plain,
( node25(s1)
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f690]) ).
fof(f699,definition,
( spl0_31
<=> node24(s1) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f701,plain,
( node24(s1)
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f699]) ).
fof(f703,plain,
node25(s1),
inference(forward_subsumption_resolution,[],[f686,f437]) ).
fof(f704,plain,
node23(s1),
inference(forward_subsumption_resolution,[],[f685,f437]) ).
fof(f705,plain,
node24(s1),
inference(forward_subsumption_resolution,[],[f684,f431]) ).
fof(f707,plain,
spl0_29,
inference(avatar_split_clause,[],[f703,f690]) ).
fof(f708,plain,
spl0_31,
inference(avatar_split_clause,[],[f705,f699]) ).
fof(f722,plain,
( ~ node24(s1)
| ~ node23(s1)
| ~ node26(s1)
| ~ spl0_29 ),
inference(resolution,[],[f692,f281]) ).
fof(f725,definition,
( spl0_32
<=> node23(s1) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f742,plain,
spl0_32,
inference(avatar_split_clause,[],[f704,f725]) ).
fof(f743,plain,
( ~ node23(s1)
| ~ node26(s1)
| ~ spl0_29
| ~ spl0_31 ),
inference(forward_subsumption_resolution,[],[f722,f701]) ).
fof(f744,plain,
( ~ spl0_12
| ~ spl0_32
| ~ spl0_29
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f743,f699,f690,f725,f417]) ).
fof(f746,plain,
( ! [X0] :
( ~ until27(X0)
| ~ succ(s1,X0) )
| ~ spl0_13 ),
inference(resolution,[],[f423,f283]) ).
fof(f776,definition,
( spl0_39
<=> node25(s2) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f778,plain,
( node25(s2)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f780,definition,
( spl0_40
<=> m_and_h_gate_v_out(c_e_h_3,c_r,s1) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f781,plain,
( ~ m_and_h_gate_v_out(c_e_h_3,c_r,s1)
| spl0_40 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f782,plain,
( m_and_h_gate_v_out(c_e_h_3,c_r,s1)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f780]) ).
fof(f789,definition,
( spl0_42
<=> node24(s2) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f791,plain,
( node24(s2)
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f789]) ).
fof(f794,definition,
( spl0_43
<=> m_and_h_gate_v_out(c_e_h_2,c_r,s1) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f795,plain,
( ~ m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| spl0_43 ),
inference(avatar_component_clause,[],[f794]) ).
fof(f796,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f794]) ).
fof(f803,definition,
( spl0_45
<=> node23(s2) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f805,plain,
( node23(s2)
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f825,definition,
( spl0_48
<=> node25(s3) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f827,plain,
( node25(s3)
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f825]) ).
fof(f829,definition,
( spl0_49
<=> m_and_h_gate_v_out(c_e_h_3,c_r,s2) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f830,plain,
( ~ m_and_h_gate_v_out(c_e_h_3,c_r,s2)
| spl0_49 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f831,plain,
( m_and_h_gate_v_out(c_e_h_3,c_r,s2)
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f829]) ).
fof(f838,definition,
( spl0_51
<=> node24(s3) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f843,definition,
( spl0_52
<=> m_and_h_gate_v_out(c_e_h_2,c_r,s2) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f844,plain,
( ~ m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| spl0_52 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f845,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f852,definition,
( spl0_54
<=> node23(s3) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f874,definition,
( spl0_57
<=> node25(s4) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f876,plain,
( node25(s4)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f874]) ).
fof(f878,definition,
( spl0_58
<=> m_and_h_gate_v_out(c_e_h_3,c_r,s3) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f879,plain,
( ~ m_and_h_gate_v_out(c_e_h_3,c_r,s3)
| spl0_58 ),
inference(avatar_component_clause,[],[f878]) ).
fof(f887,definition,
( spl0_60
<=> node24(s4) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f892,definition,
( spl0_61
<=> m_and_h_gate_v_out(c_e_h_2,c_r,s3) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f893,plain,
( ~ m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| spl0_61 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f901,definition,
( spl0_63
<=> node23(s4) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f903,plain,
( node23(s4)
| ~ spl0_63 ),
inference(avatar_component_clause,[],[f901]) ).
fof(f915,plain,
! [X0] :
( ~ m_and_h_gate_v_out(X0,c_c,s2)
| m_and_h_gate_v_out(X0,c_c,s1)
| ~ m_mutex_h_half_v_out(X0,c_a,s1) ),
inference(resolution,[],[f655,f178]) ).
fof(f921,plain,
! [X0] :
( ~ m_and_h_gate_v_out(X0,c_c,s2)
| m_and_h_gate_v_out(X0,c_c,s1) ),
inference(forward_subsumption_resolution,[],[f915,f529]) ).
fof(f939,plain,
! [X0,X1] :
( ~ m_c_h_element_v_in1(X0,X1,s0)
| m_c_h_element_v_in2(X0,X1,s0)
| m_c_h_element_v_out(X0,X1,s1) ),
inference(resolution,[],[f673,f328]) ).
fof(f962,definition,
( spl0_69
<=> m_c_h_element_v_out(c_e_h_3,c_e,s2) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f963,plain,
( ~ m_c_h_element_v_out(c_e_h_3,c_e,s2)
| spl0_69 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f964,plain,
( m_c_h_element_v_out(c_e_h_3,c_e,s2)
| ~ spl0_69 ),
inference(avatar_component_clause,[],[f962]) ).
fof(f973,plain,
( node24(s2)
| spl0_49 ),
inference(resolution,[],[f830,f372]) ).
fof(f976,plain,
( spl0_42
| spl0_49 ),
inference(avatar_split_clause,[],[f973,f829,f789]) ).
fof(f977,plain,
( ~ node24(s2)
| ~ node23(s2)
| ~ node26(s2)
| ~ spl0_39 ),
inference(resolution,[],[f778,f281]) ).
fof(f979,definition,
( spl0_70
<=> node26(s2) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f981,plain,
( ~ node26(s2)
| spl0_70 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f985,definition,
( spl0_71
<=> m_c_h_element_v_out(c_e_h_2,c_e,s2) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f986,plain,
( ~ m_c_h_element_v_out(c_e_h_2,c_e,s2)
| spl0_71 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f987,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s2)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f989,plain,
( node23(s2)
| spl0_52 ),
inference(resolution,[],[f844,f370]) ).
fof(f993,plain,
( spl0_45
| spl0_52 ),
inference(avatar_split_clause,[],[f989,f843,f803]) ).
fof(f1004,definition,
( spl0_73
<=> m_c_h_element_v_out(c_e_h_3,c_e,s3) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f1006,plain,
( m_c_h_element_v_out(c_e_h_3,c_e,s3)
| ~ spl0_73 ),
inference(avatar_component_clause,[],[f1004]) ).
fof(f1008,definition,
( spl0_74
<=> m_and_h_gate_v_out(c_e_h_3,c_r,s4) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f1009,plain,
( ~ m_and_h_gate_v_out(c_e_h_3,c_r,s4)
| spl0_74 ),
inference(avatar_component_clause,[],[f1008]) ).
fof(f1012,plain,
( node24(s3)
| spl0_58 ),
inference(resolution,[],[f879,f372]) ).
fof(f1013,plain,
( node25(s3)
| spl0_58 ),
inference(resolution,[],[f879,f371]) ).
fof(f1014,plain,
( spl0_48
| spl0_58 ),
inference(avatar_split_clause,[],[f1013,f878,f825]) ).
fof(f1015,plain,
( spl0_51
| spl0_58 ),
inference(avatar_split_clause,[],[f1012,f878,f838]) ).
fof(f1016,plain,
( ~ node24(s3)
| ~ node23(s3)
| ~ node26(s3)
| ~ spl0_48 ),
inference(resolution,[],[f827,f281]) ).
fof(f1018,definition,
( spl0_75
<=> node26(s3) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f1020,plain,
( ~ node26(s3)
| spl0_75 ),
inference(avatar_component_clause,[],[f1018]) ).
fof(f1021,plain,
( ~ spl0_75
| ~ spl0_54
| ~ spl0_51
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f1016,f825,f838,f852,f1018]) ).
fof(f1024,definition,
( spl0_76
<=> m_c_h_element_v_out(c_e_h_2,c_e,s3) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f1026,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f1024]) ).
fof(f1028,definition,
( spl0_77
<=> m_and_h_gate_v_out(c_e_h_2,c_r,s4) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f1029,plain,
( ~ m_and_h_gate_v_out(c_e_h_2,c_r,s4)
| spl0_77 ),
inference(avatar_component_clause,[],[f1028]) ).
fof(f1030,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s4)
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f1028]) ).
fof(f1032,plain,
( node23(s3)
| spl0_61 ),
inference(resolution,[],[f893,f370]) ).
fof(f1036,plain,
( spl0_54
| spl0_61 ),
inference(avatar_split_clause,[],[f1032,f892,f852]) ).
fof(f1049,plain,
( ! [X0] :
( ~ succ(s1,X0)
| xuntil28(X0)
| node26(X0) )
| ~ spl0_13 ),
inference(resolution,[],[f746,f282]) ).
fof(f1128,plain,
( xuntil28(s2)
| node26(s2)
| ~ spl0_13 ),
inference(resolution,[],[f1049,f2]) ).
fof(f1129,plain,
( xuntil28(s2)
| ~ spl0_13
| spl0_70 ),
inference(forward_subsumption_resolution,[],[f1128,f981]) ).
fof(f1155,plain,
( ! [X0] :
( ~ until27(X0)
| ~ succ(s2,X0) )
| ~ spl0_13
| spl0_70 ),
inference(resolution,[],[f1129,f283]) ).
fof(f1185,plain,
( m_and_h_gate_v_in1(c_e_h_2,c_r,s0)
| ~ spl0_43 ),
inference(resolution,[],[f796,f659]) ).
fof(f1189,plain,
( $false
| ~ spl0_43 ),
inference(forward_subsumption_resolution,[],[f1185,f366]) ).
fof(f1190,plain,
~ spl0_43,
inference(avatar_contradiction_clause,[],[f1189]) ).
fof(f1248,plain,
! [X0,X1] :
( ~ m_c_h_element_v_in1(X0,X1,s0)
| m_c_h_element_v_out(X0,X1,s1) ),
inference(forward_subsumption_resolution,[],[f939,f679]) ).
fof(f1250,plain,
! [X0] :
( m_c_h_element_v_out(X0,c_e,s1)
| m_and_h_gate_v_out(X0,c_c,s0) ),
inference(resolution,[],[f1248,f186]) ).
fof(f1252,plain,
! [X0] :
( m_c_h_element_v_out(X0,c_h,s1)
| m_or_h_gate_v_out(X0,c_g,s0) ),
inference(resolution,[],[f1248,f192]) ).
fof(f1253,plain,
! [X0] : m_c_h_element_v_out(X0,c_h,s1),
inference(forward_subsumption_resolution,[],[f1252,f98]) ).
fof(f1255,plain,
! [X0] : m_c_h_element_v_out(X0,c_e,s1),
inference(forward_subsumption_resolution,[],[f1250,f142]) ).
fof(f1360,plain,
! [X0] : ~ m_and_h_gate_v_in1(X0,c_i,s1),
inference(resolution,[],[f1253,f194]) ).
fof(f1370,plain,
! [X0] : ~ m_and_h_gate_v_in1(X0,c_r,s1),
inference(resolution,[],[f1255,f222]) ).
fof(f1372,plain,
! [X0,X1] :
( ~ m_c_h_element_v_in1(X0,c_e,s1)
| m_c_h_element_v_in2(X0,c_e,s1)
| ~ trans(s1,X1)
| m_c_h_element_v_out(X0,c_e,X1) ),
inference(resolution,[],[f1255,f528]) ).
fof(f1374,plain,
! [X0,X1] :
( ~ trans(s1,X0)
| node17(X1,c_e,s1)
| m_c_h_element_v_out(X1,c_e,X0) ),
inference(resolution,[],[f1255,f464]) ).
fof(f1604,plain,
! [X0] :
( ~ m_and_h_gate_v_out(X0,c_i,s2)
| m_and_h_gate_v_out(X0,c_i,s1) ),
inference(resolution,[],[f1360,f655]) ).
fof(f1608,plain,
! [X0] :
( ~ m_and_h_gate_v_out(X0,c_r,s2)
| m_and_h_gate_v_out(X0,c_r,s1) ),
inference(resolution,[],[f1370,f655]) ).
fof(f1677,plain,
! [X0] :
( node17(X0,c_e,s1)
| m_c_h_element_v_out(X0,c_e,s2) ),
inference(resolution,[],[f1374,f329]) ).
fof(f1711,plain,
( m_and_h_gate_v_in1(c_e_h_3,c_r,s0)
| ~ spl0_40 ),
inference(resolution,[],[f782,f659]) ).
fof(f1714,plain,
( $false
| ~ spl0_40 ),
inference(forward_subsumption_resolution,[],[f1711,f366]) ).
fof(f1715,plain,
~ spl0_40,
inference(avatar_contradiction_clause,[],[f1714]) ).
fof(f1733,plain,
! [X0,X1] :
( ~ trans(s1,X1)
| m_c_h_element_v_in2(X0,c_e,s1)
| m_c_h_element_v_out(X0,c_e,X1)
| m_and_h_gate_v_out(X0,c_c,s1) ),
inference(resolution,[],[f1372,f186]) ).
fof(f1822,plain,
( ~ m_and_h_gate_v_in1(c_e_h_3,c_r,s2)
| ~ spl0_69 ),
inference(resolution,[],[f964,f222]) ).
fof(f1824,plain,
( ! [X0] :
( m_c_h_element_v_in2(c_e_h_3,c_e,s2)
| ~ m_c_h_element_v_in1(c_e_h_3,c_e,s2)
| ~ trans(s2,X0)
| m_c_h_element_v_out(c_e_h_3,c_e,X0) )
| ~ spl0_69 ),
inference(resolution,[],[f964,f528]) ).
fof(f1832,definition,
( spl0_145
<=> ! [X0] :
( ~ trans(s2,X0)
| m_c_h_element_v_out(c_e_h_3,c_e,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1833,plain,
( ! [X0] :
( ~ trans(s2,X0)
| m_c_h_element_v_out(c_e_h_3,c_e,X0) )
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f1832]) ).
fof(f1836,definition,
( spl0_146
<=> m_c_h_element_v_in1(c_e_h_3,c_e,s2) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1838,plain,
( ~ m_c_h_element_v_in1(c_e_h_3,c_e,s2)
| spl0_146 ),
inference(avatar_component_clause,[],[f1836]) ).
fof(f1840,definition,
( spl0_147
<=> m_c_h_element_v_in2(c_e_h_3,c_e,s2) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1842,plain,
( m_c_h_element_v_in2(c_e_h_3,c_e,s2)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f1840]) ).
fof(f1843,plain,
( spl0_145
| ~ spl0_146
| spl0_147
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f1824,f962,f1840,f1836,f1832]) ).
fof(f1844,plain,
( ~ m_and_h_gate_v_out(c_e_h_3,c_r,s3)
| m_and_h_gate_v_out(c_e_h_3,c_r,s2)
| ~ spl0_69 ),
inference(resolution,[],[f1822,f656]) ).
fof(f1852,plain,
( m_c_h_element_v_out(c_e_h_3,c_e,s3)
| ~ spl0_145 ),
inference(resolution,[],[f1833,f330]) ).
fof(f1853,plain,
( spl0_73
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f1852,f1832,f1004]) ).
fof(f1854,plain,
( m_and_h_gate_v_out(c_e_h_3,c_c,s2)
| spl0_146 ),
inference(resolution,[],[f1838,f186]) ).
fof(f1855,plain,
( m_and_h_gate_v_out(c_e_h_3,c_i,s2)
| ~ spl0_147 ),
inference(resolution,[],[f1842,f38]) ).
fof(f1866,plain,
( m_and_h_gate_v_out(c_e_h_3,c_c,s1)
| spl0_146 ),
inference(resolution,[],[f1854,f921]) ).
fof(f1870,definition,
( spl0_148
<=> m_and_h_gate_v_out(c_e_h_3,c_c,s1) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1871,plain,
( ~ m_and_h_gate_v_out(c_e_h_3,c_c,s1)
| spl0_148 ),
inference(avatar_component_clause,[],[f1870]) ).
fof(f1872,plain,
( m_and_h_gate_v_out(c_e_h_3,c_c,s1)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f1870]) ).
fof(f1878,plain,
( spl0_148
| spl0_146 ),
inference(avatar_split_clause,[],[f1866,f1836,f1870]) ).
fof(f1887,definition,
( spl0_150
<=> m_and_h_gate_v_out(c_e_h_3,c_i,s1) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1889,plain,
( m_and_h_gate_v_out(c_e_h_3,c_i,s1)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f1887]) ).
fof(f1919,plain,
( m_and_h_gate_v_in1(c_e_h_3,c_c,s0)
| ~ spl0_148 ),
inference(resolution,[],[f1872,f659]) ).
fof(f2011,plain,
( ~ m_mutex_h_half_v_out(c_e_h_3,c_a,s0)
| ~ spl0_148 ),
inference(resolution,[],[f1919,f178]) ).
fof(f2013,plain,
( $false
| ~ spl0_148 ),
inference(forward_subsumption_resolution,[],[f2011,f251]) ).
fof(f2014,plain,
~ spl0_148,
inference(avatar_contradiction_clause,[],[f2013]) ).
fof(f2015,plain,
( ~ m_and_h_gate_v_in1(c_e_h_3,c_r,s3)
| ~ spl0_73 ),
inference(resolution,[],[f1006,f222]) ).
fof(f2039,plain,
( ~ m_and_h_gate_v_out(c_e_h_3,c_r,s4)
| m_and_h_gate_v_out(c_e_h_3,c_r,s3)
| ~ spl0_73 ),
inference(resolution,[],[f2015,f657]) ).
fof(f2043,plain,
( node24(s4)
| spl0_74 ),
inference(resolution,[],[f1009,f372]) ).
fof(f2044,plain,
( node25(s4)
| spl0_74 ),
inference(resolution,[],[f1009,f371]) ).
fof(f2045,plain,
( spl0_57
| spl0_74 ),
inference(avatar_split_clause,[],[f2044,f1008,f874]) ).
fof(f2046,plain,
( spl0_60
| spl0_74 ),
inference(avatar_split_clause,[],[f2043,f1008,f887]) ).
fof(f2047,plain,
( spl0_58
| ~ spl0_74
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f2039,f1004,f1008,f878]) ).
fof(f2057,definition,
( spl0_171
<=> node26(s4) ),
introduced(definition,[new_symbols(definition,[spl0_171])],[avatar_definition]) ).
fof(f2059,plain,
( ~ node26(s4)
| spl0_171 ),
inference(avatar_component_clause,[],[f2057]) ).
fof(f2129,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s1)
| ~ spl0_52 ),
inference(resolution,[],[f1608,f845]) ).
fof(f2132,plain,
( m_and_h_gate_v_out(c_e_h_3,c_r,s1)
| ~ spl0_49 ),
inference(resolution,[],[f1608,f831]) ).
fof(f2134,plain,
( m_and_h_gate_v_out(c_e_h_3,c_r,s1)
| node25(s2) ),
inference(resolution,[],[f1608,f371]) ).
fof(f2135,plain,
( node25(s2)
| spl0_40 ),
inference(forward_subsumption_resolution,[],[f2134,f781]) ).
fof(f2136,plain,
( $false
| spl0_40
| ~ spl0_49 ),
inference(forward_subsumption_resolution,[],[f2132,f781]) ).
fof(f2137,plain,
( spl0_40
| ~ spl0_49 ),
inference(avatar_contradiction_clause,[],[f2136]) ).
fof(f2139,plain,
( $false
| spl0_43
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f2129,f795]) ).
fof(f2140,plain,
( spl0_43
| ~ spl0_52 ),
inference(avatar_contradiction_clause,[],[f2139]) ).
fof(f2145,plain,
( ~ node23(s2)
| ~ node26(s2)
| ~ spl0_39
| ~ spl0_42 ),
inference(forward_subsumption_resolution,[],[f977,f791]) ).
fof(f2148,plain,
( spl0_39
| spl0_40 ),
inference(avatar_split_clause,[],[f2135,f780,f776]) ).
fof(f2150,plain,
( ~ node26(s2)
| ~ spl0_39
| ~ spl0_42
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f2145,f805]) ).
fof(f2151,plain,
( ~ spl0_70
| ~ spl0_39
| ~ spl0_42
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f2150,f803,f789,f776,f979]) ).
fof(f2163,plain,
( ! [X0] :
( ~ succ(s2,X0)
| xuntil28(X0)
| node26(X0) )
| ~ spl0_13
| spl0_70 ),
inference(resolution,[],[f1155,f282]) ).
fof(f2179,plain,
! [X0] :
( ~ m_c_h_element_v_in1(X0,c_e,s1)
| ~ m_c_h_element_v_in2(X0,c_e,s1)
| m_c_h_element_v_out(X0,c_e,s2) ),
inference(resolution,[],[f1677,f265]) ).
fof(f2253,plain,
! [X0] :
( m_c_h_element_v_in2(X0,c_e,s1)
| m_c_h_element_v_out(X0,c_e,s2)
| m_and_h_gate_v_out(X0,c_c,s1) ),
inference(resolution,[],[f1733,f329]) ).
fof(f2334,plain,
( xuntil28(s3)
| node26(s3)
| ~ spl0_13
| spl0_70 ),
inference(resolution,[],[f2163,f3]) ).
fof(f2335,plain,
( xuntil28(s3)
| ~ spl0_13
| spl0_70
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f2334,f1020]) ).
fof(f2343,plain,
( ! [X0] :
( ~ until27(X0)
| ~ succ(s3,X0) )
| ~ spl0_13
| spl0_70
| spl0_75 ),
inference(resolution,[],[f2335,f283]) ).
fof(f2357,plain,
( ~ m_and_h_gate_v_out(c_e_h_3,c_r,s3)
| spl0_49
| ~ spl0_69 ),
inference(forward_subsumption_resolution,[],[f1844,f830]) ).
fof(f2359,plain,
( ~ spl0_58
| spl0_49
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f2357,f962,f829,f878]) ).
fof(f2579,plain,
( ! [X0] :
( ~ succ(s3,X0)
| xuntil28(X0)
| node26(X0) )
| ~ spl0_13
| spl0_70
| spl0_75 ),
inference(resolution,[],[f2343,f282]) ).
fof(f2611,definition,
( spl0_214
<=> xuntil2p30(s4) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f2612,plain,
( ~ xuntil2p30(s4)
| spl0_214 ),
inference(avatar_component_clause,[],[f2611]) ).
fof(f2613,plain,
( xuntil2p30(s4)
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f2611]) ).
fof(f2616,plain,
( last(s4)
| ~ spl0_214 ),
inference(resolution,[],[f2613,f286]) ).
fof(f2617,plain,
( $false
| ~ spl0_214 ),
inference(forward_subsumption_resolution,[],[f2616,f165]) ).
fof(f2618,plain,
~ spl0_214,
inference(avatar_contradiction_clause,[],[f2617]) ).
fof(f2818,definition,
( spl0_227
<=> xuntil28(s4) ),
introduced(definition,[new_symbols(definition,[spl0_227])],[avatar_definition]) ).
fof(f2820,plain,
( xuntil28(s4)
| ~ spl0_227 ),
inference(avatar_component_clause,[],[f2818]) ).
fof(f2879,plain,
( ! [X0] :
( ~ trans(s4,X0)
| last(s4)
| until2p29(X0) )
| ~ spl0_227 ),
inference(resolution,[],[f2820,f285]) ).
fof(f2881,plain,
( ! [X0] :
( ~ trans(s4,X0)
| until2p29(X0) )
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f2879,f165]) ).
fof(f2949,plain,
( until2p29(s0)
| ~ spl0_7
| ~ spl0_227 ),
inference(resolution,[],[f2881,f316]) ).
fof(f2954,plain,
( xuntil2p30(s0)
| node26(s0)
| ~ spl0_7
| ~ spl0_227 ),
inference(resolution,[],[f2949,f161]) ).
fof(f2955,plain,
( xuntil2p30(s0)
| ~ spl0_7
| spl0_8
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f2954,f321]) ).
fof(f2957,plain,
( ! [X0] :
( ~ succ(s0,X0)
| until2p29(X0) )
| ~ spl0_7
| spl0_8
| ~ spl0_227 ),
inference(resolution,[],[f2955,f162]) ).
fof(f2961,plain,
( until2p29(s1)
| ~ spl0_7
| spl0_8
| ~ spl0_227 ),
inference(resolution,[],[f2957,f1]) ).
fof(f2962,plain,
( xuntil2p30(s1)
| node26(s1)
| ~ spl0_7
| spl0_8
| ~ spl0_227 ),
inference(resolution,[],[f2961,f161]) ).
fof(f2963,plain,
( xuntil2p30(s1)
| ~ spl0_7
| spl0_8
| spl0_12
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f2962,f418]) ).
fof(f2964,plain,
( ! [X0] :
( ~ succ(s1,X0)
| until2p29(X0) )
| ~ spl0_7
| spl0_8
| spl0_12
| ~ spl0_227 ),
inference(resolution,[],[f2963,f162]) ).
fof(f2966,plain,
( until2p29(s2)
| ~ spl0_7
| spl0_8
| spl0_12
| ~ spl0_227 ),
inference(resolution,[],[f2964,f2]) ).
fof(f2971,plain,
( xuntil2p30(s2)
| node26(s2)
| ~ spl0_7
| spl0_8
| spl0_12
| ~ spl0_227 ),
inference(resolution,[],[f2966,f161]) ).
fof(f2972,plain,
( xuntil2p30(s2)
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f2971,f981]) ).
fof(f3001,plain,
( ! [X0] :
( ~ succ(s2,X0)
| until2p29(X0) )
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f2972,f162]) ).
fof(f3019,plain,
( until2p29(s3)
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f3001,f3]) ).
fof(f3020,plain,
( xuntil2p30(s3)
| node26(s3)
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f3019,f161]) ).
fof(f3021,plain,
( xuntil2p30(s3)
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3020,f1020]) ).
fof(f3022,plain,
( ! [X0] :
( ~ succ(s3,X0)
| until2p29(X0) )
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3021,f162]) ).
fof(f3031,plain,
( until2p29(s4)
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3022,f4]) ).
fof(f3032,plain,
( xuntil2p30(s4)
| node26(s4)
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3031,f161]) ).
fof(f3033,plain,
( node26(s4)
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| spl0_75
| spl0_214
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3032,f2612]) ).
fof(f3034,plain,
( $false
| ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3033,f2059]) ).
fof(f3035,plain,
( ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(avatar_contradiction_clause,[],[f3034]) ).
fof(f3043,plain,
( until2p29(s1)
| ~ spl0_6
| ~ spl0_227 ),
inference(resolution,[],[f312,f2881]) ).
fof(f3064,plain,
( xuntil2p30(s1)
| node26(s1)
| ~ spl0_6
| ~ spl0_227 ),
inference(resolution,[],[f3043,f161]) ).
fof(f3065,plain,
( xuntil2p30(s1)
| ~ spl0_6
| spl0_12
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3064,f418]) ).
fof(f3098,plain,
( ! [X0] :
( ~ succ(s1,X0)
| until2p29(X0) )
| ~ spl0_6
| spl0_12
| ~ spl0_227 ),
inference(resolution,[],[f3065,f162]) ).
fof(f3104,plain,
( until2p29(s2)
| ~ spl0_6
| spl0_12
| ~ spl0_227 ),
inference(resolution,[],[f3098,f2]) ).
fof(f3106,plain,
( xuntil2p30(s2)
| node26(s2)
| ~ spl0_6
| spl0_12
| ~ spl0_227 ),
inference(resolution,[],[f3104,f161]) ).
fof(f3107,plain,
( xuntil2p30(s2)
| ~ spl0_6
| spl0_12
| spl0_70
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3106,f981]) ).
fof(f3108,plain,
( ! [X0] :
( ~ succ(s2,X0)
| until2p29(X0) )
| ~ spl0_6
| spl0_12
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f3107,f162]) ).
fof(f3110,plain,
( until2p29(s3)
| ~ spl0_6
| spl0_12
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f3108,f3]) ).
fof(f3111,plain,
( xuntil2p30(s3)
| node26(s3)
| ~ spl0_6
| spl0_12
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f3110,f161]) ).
fof(f3112,plain,
( xuntil2p30(s3)
| ~ spl0_6
| spl0_12
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3111,f1020]) ).
fof(f3117,plain,
( ! [X0] :
( ~ succ(s3,X0)
| until2p29(X0) )
| ~ spl0_6
| spl0_12
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3112,f162]) ).
fof(f3119,plain,
( until2p29(s4)
| ~ spl0_6
| spl0_12
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3117,f4]) ).
fof(f3120,plain,
( xuntil2p30(s4)
| node26(s4)
| ~ spl0_6
| spl0_12
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3119,f161]) ).
fof(f3121,plain,
( node26(s4)
| ~ spl0_6
| spl0_12
| spl0_70
| spl0_75
| spl0_214
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3120,f2612]) ).
fof(f3122,plain,
( $false
| ~ spl0_6
| spl0_12
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3121,f2059]) ).
fof(f3123,plain,
( ~ spl0_6
| spl0_12
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(avatar_contradiction_clause,[],[f3122]) ).
fof(f3126,plain,
( until2p29(s4)
| ~ spl0_3
| ~ spl0_227 ),
inference(resolution,[],[f300,f2881]) ).
fof(f3140,plain,
( xuntil2p30(s4)
| node26(s4)
| ~ spl0_3
| ~ spl0_227 ),
inference(resolution,[],[f3126,f161]) ).
fof(f3141,plain,
( node26(s4)
| ~ spl0_3
| spl0_214
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3140,f2612]) ).
fof(f3142,plain,
( $false
| ~ spl0_3
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3141,f2059]) ).
fof(f3143,plain,
( ~ spl0_3
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(avatar_contradiction_clause,[],[f3142]) ).
fof(f3147,plain,
( until2p29(s2)
| ~ spl0_5
| ~ spl0_227 ),
inference(resolution,[],[f308,f2881]) ).
fof(f3232,plain,
( xuntil2p30(s2)
| node26(s2)
| ~ spl0_5
| ~ spl0_227 ),
inference(resolution,[],[f3147,f161]) ).
fof(f3233,plain,
( xuntil2p30(s2)
| ~ spl0_5
| spl0_70
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3232,f981]) ).
fof(f3234,plain,
( ! [X0] :
( ~ succ(s2,X0)
| until2p29(X0) )
| ~ spl0_5
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f3233,f162]) ).
fof(f3325,plain,
( until2p29(s3)
| ~ spl0_5
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f3234,f3]) ).
fof(f3326,plain,
( xuntil2p30(s3)
| node26(s3)
| ~ spl0_5
| spl0_70
| ~ spl0_227 ),
inference(resolution,[],[f3325,f161]) ).
fof(f3327,plain,
( xuntil2p30(s3)
| ~ spl0_5
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3326,f1020]) ).
fof(f3357,plain,
( ! [X0] :
( ~ succ(s3,X0)
| until2p29(X0) )
| ~ spl0_5
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3327,f162]) ).
fof(f3368,plain,
( until2p29(s4)
| ~ spl0_5
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3357,f4]) ).
fof(f3370,plain,
( xuntil2p30(s4)
| node26(s4)
| ~ spl0_5
| spl0_70
| spl0_75
| ~ spl0_227 ),
inference(resolution,[],[f3368,f161]) ).
fof(f3371,plain,
( node26(s4)
| ~ spl0_5
| spl0_70
| spl0_75
| spl0_214
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3370,f2612]) ).
fof(f3372,plain,
( $false
| ~ spl0_5
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3371,f2059]) ).
fof(f3373,plain,
( ~ spl0_5
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(avatar_contradiction_clause,[],[f3372]) ).
fof(f3375,definition,
( spl0_255
<=> xuntil2p30(s3) ),
introduced(definition,[new_symbols(definition,[spl0_255])],[avatar_definition]) ).
fof(f3377,plain,
( xuntil2p30(s3)
| ~ spl0_255 ),
inference(avatar_component_clause,[],[f3375]) ).
fof(f3465,plain,
( ~ m_and_h_gate_v_in1(c_e_h_2,c_r,s3)
| ~ spl0_76 ),
inference(resolution,[],[f1026,f222]) ).
fof(f3516,plain,
( node23(s4)
| spl0_77 ),
inference(resolution,[],[f1029,f370]) ).
fof(f3518,plain,
( ~ m_and_h_gate_v_out(c_e_h_2,c_r,s4)
| m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| ~ spl0_76 ),
inference(resolution,[],[f3465,f657]) ).
fof(f3549,definition,
( spl0_262
<=> node17(c_e_h_2,c_e,s2) ),
introduced(definition,[new_symbols(definition,[spl0_262])],[avatar_definition]) ).
fof(f3551,plain,
( node17(c_e_h_2,c_e,s2)
| ~ spl0_262 ),
inference(avatar_component_clause,[],[f3549]) ).
fof(f3553,plain,
( ~ m_and_h_gate_v_in1(c_e_h_2,c_r,s2)
| ~ spl0_71 ),
inference(resolution,[],[f987,f222]) ).
fof(f3557,plain,
( ! [X0] :
( ~ trans(s2,X0)
| node17(c_e_h_2,c_e,s2)
| m_c_h_element_v_out(c_e_h_2,c_e,X0) )
| ~ spl0_71 ),
inference(resolution,[],[f987,f464]) ).
fof(f3559,definition,
( spl0_263
<=> ! [X0] :
( ~ trans(s2,X0)
| m_c_h_element_v_out(c_e_h_2,c_e,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_263])],[avatar_definition]) ).
fof(f3560,plain,
( ! [X0] :
( ~ trans(s2,X0)
| m_c_h_element_v_out(c_e_h_2,c_e,X0) )
| ~ spl0_263 ),
inference(avatar_component_clause,[],[f3559]) ).
fof(f3561,plain,
( spl0_262
| spl0_263
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f3557,f985,f3559,f3549]) ).
fof(f3563,definition,
( spl0_264
<=> m_c_h_element_v_in1(c_e_h_2,c_e,s2) ),
introduced(definition,[new_symbols(definition,[spl0_264])],[avatar_definition]) ).
fof(f3567,definition,
( spl0_265
<=> m_c_h_element_v_in2(c_e_h_2,c_e,s2) ),
introduced(definition,[new_symbols(definition,[spl0_265])],[avatar_definition]) ).
fof(f3568,plain,
( ~ m_c_h_element_v_in2(c_e_h_2,c_e,s2)
| spl0_265 ),
inference(avatar_component_clause,[],[f3567]) ).
fof(f3569,plain,
( m_c_h_element_v_in2(c_e_h_2,c_e,s2)
| ~ spl0_265 ),
inference(avatar_component_clause,[],[f3567]) ).
fof(f3571,plain,
( ~ m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| m_and_h_gate_v_out(c_e_h_2,c_r,s2)
| ~ spl0_71 ),
inference(resolution,[],[f3553,f656]) ).
fof(f3577,plain,
( ~ m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| spl0_52
| ~ spl0_71 ),
inference(forward_subsumption_resolution,[],[f3571,f844]) ).
fof(f3578,plain,
( ~ spl0_61
| spl0_52
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f3577,f985,f843,f892]) ).
fof(f3581,plain,
( until2p29(s3)
| ~ spl0_4
| ~ spl0_227 ),
inference(resolution,[],[f304,f2881]) ).
fof(f3612,plain,
( last(s4)
| ~ spl0_1
| ~ spl0_227 ),
inference(resolution,[],[f291,f2820]) ).
fof(f3613,plain,
( $false
| ~ spl0_1
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3612,f165]) ).
fof(f3614,plain,
( ~ spl0_1
| ~ spl0_227 ),
inference(avatar_contradiction_clause,[],[f3613]) ).
fof(f3656,plain,
( xuntil2p30(s3)
| node26(s3)
| ~ spl0_4
| ~ spl0_227 ),
inference(resolution,[],[f3581,f161]) ).
fof(f3657,plain,
( xuntil2p30(s3)
| ~ spl0_4
| spl0_75
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3656,f1020]) ).
fof(f3658,plain,
( spl0_255
| ~ spl0_4
| spl0_75
| ~ spl0_227 ),
inference(avatar_split_clause,[],[f3657,f2818,f1018,f302,f3375]) ).
fof(f3673,plain,
( spl0_63
| spl0_77 ),
inference(avatar_split_clause,[],[f3516,f1028,f901]) ).
fof(f3746,plain,
( m_c_h_element_v_in2(c_e_h_2,c_e,s2)
| m_c_h_element_v_in1(c_e_h_2,c_e,s2)
| ~ spl0_262 ),
inference(resolution,[],[f3551,f266]) ).
fof(f3792,plain,
( xuntil28(s4)
| node26(s4)
| ~ spl0_13
| spl0_70
| spl0_75 ),
inference(resolution,[],[f2579,f4]) ).
fof(f4166,plain,
( ! [X0] :
( m_c_h_element_v_in2(c_e_h_2,c_e,s2)
| ~ m_c_h_element_v_in1(c_e_h_2,c_e,s2)
| ~ trans(s2,X0)
| m_c_h_element_v_out(c_e_h_2,c_e,X0) )
| ~ spl0_71 ),
inference(resolution,[],[f987,f528]) ).
fof(f4177,plain,
( m_c_h_element_v_out(c_e_h_2,c_e,s3)
| ~ spl0_263 ),
inference(resolution,[],[f3560,f330]) ).
fof(f4217,plain,
( m_and_h_gate_v_out(c_e_h_2,c_r,s3)
| ~ spl0_76
| ~ spl0_77 ),
inference(forward_subsumption_resolution,[],[f3518,f1030]) ).
fof(f4225,plain,
( spl0_61
| ~ spl0_76
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f4217,f1028,f1024,f892]) ).
fof(f4486,plain,
! [X0] :
( ~ m_c_h_element_v_in2(X0,c_e,s1)
| m_c_h_element_v_out(X0,c_e,s2)
| m_and_h_gate_v_out(X0,c_c,s1) ),
inference(resolution,[],[f2179,f186]) ).
fof(f5048,plain,
! [X0] :
( m_c_h_element_v_out(X0,c_e,s2)
| m_and_h_gate_v_out(X0,c_c,s1) ),
inference(forward_subsumption_resolution,[],[f4486,f2253]) ).
fof(f5056,plain,
( m_and_h_gate_v_out(c_e_h_2,c_c,s1)
| spl0_71 ),
inference(resolution,[],[f5048,f986]) ).
fof(f5059,plain,
( m_and_h_gate_v_in1(c_e_h_2,c_c,s0)
| spl0_71 ),
inference(resolution,[],[f5056,f659]) ).
fof(f5073,plain,
( ~ m_mutex_h_half_v_out(c_e_h_2,c_a,s0)
| spl0_71 ),
inference(resolution,[],[f5059,f178]) ).
fof(f5075,plain,
( $false
| spl0_71 ),
inference(forward_subsumption_resolution,[],[f5073,f251]) ).
fof(f5076,plain,
spl0_71,
inference(avatar_contradiction_clause,[],[f5075]) ).
fof(f5081,plain,
( ! [X0] :
( ~ m_c_h_element_v_in1(c_e_h_2,c_e,s2)
| ~ trans(s2,X0)
| m_c_h_element_v_out(c_e_h_2,c_e,X0) )
| ~ spl0_71
| spl0_265 ),
inference(forward_subsumption_resolution,[],[f4166,f3568]) ).
fof(f5118,plain,
( m_c_h_element_v_in1(c_e_h_2,c_e,s2)
| ~ spl0_262
| spl0_265 ),
inference(forward_subsumption_resolution,[],[f3746,f3568]) ).
fof(f5134,plain,
( spl0_264
| ~ spl0_262
| spl0_265 ),
inference(avatar_split_clause,[],[f5118,f3567,f3549,f3563]) ).
fof(f5189,plain,
( m_and_h_gate_v_out(c_e_h_2,c_i,s2)
| ~ spl0_265 ),
inference(resolution,[],[f3569,f38]) ).
fof(f5194,plain,
( m_and_h_gate_v_out(c_e_h_2,c_i,s1)
| ~ spl0_265 ),
inference(resolution,[],[f5189,f1604]) ).
fof(f5200,definition,
( spl0_348
<=> m_and_h_gate_v_out(c_e_h_2,c_i,s1) ),
introduced(definition,[new_symbols(definition,[spl0_348])],[avatar_definition]) ).
fof(f5202,plain,
( m_and_h_gate_v_out(c_e_h_2,c_i,s1)
| ~ spl0_348 ),
inference(avatar_component_clause,[],[f5200]) ).
fof(f5221,plain,
( spl0_348
| ~ spl0_265 ),
inference(avatar_split_clause,[],[f5194,f3567,f5200]) ).
fof(f5233,plain,
( m_and_h_gate_v_in1(c_e_h_2,c_i,s0)
| ~ spl0_348 ),
inference(resolution,[],[f5202,f659]) ).
fof(f5235,plain,
( $false
| ~ spl0_348 ),
inference(forward_subsumption_resolution,[],[f5233,f356]) ).
fof(f5236,plain,
~ spl0_348,
inference(avatar_contradiction_clause,[],[f5235]) ).
fof(f5257,plain,
( spl0_76
| ~ spl0_263 ),
inference(avatar_split_clause,[],[f4177,f3559,f1024]) ).
fof(f5261,plain,
( spl0_263
| ~ spl0_264
| ~ spl0_71
| spl0_265 ),
inference(avatar_split_clause,[],[f5081,f3567,f985,f3563,f3559]) ).
fof(f5288,plain,
( ~ node24(s4)
| ~ node23(s4)
| ~ node26(s4)
| ~ spl0_57 ),
inference(resolution,[],[f876,f281]) ).
fof(f5293,plain,
( m_and_h_gate_v_out(c_e_h_3,c_c,s1)
| spl0_69 ),
inference(resolution,[],[f963,f5048]) ).
fof(f5294,plain,
( $false
| spl0_69
| spl0_148 ),
inference(forward_subsumption_resolution,[],[f5293,f1871]) ).
fof(f5295,plain,
( spl0_69
| spl0_148 ),
inference(avatar_contradiction_clause,[],[f5294]) ).
fof(f5302,plain,
( spl0_171
| spl0_227
| ~ spl0_13
| spl0_70
| spl0_75 ),
inference(avatar_split_clause,[],[f3792,f1018,f979,f421,f2818,f2057]) ).
fof(f5304,plain,
( ~ node24(s4)
| ~ node26(s4)
| ~ spl0_57
| ~ spl0_63 ),
inference(forward_subsumption_resolution,[],[f5288,f903]) ).
fof(f5310,plain,
( ~ spl0_171
| ~ spl0_60
| ~ spl0_57
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f5304,f901,f874,f887,f2057]) ).
fof(f5427,plain,
( ! [X0] :
( ~ succ(s3,X0)
| until2p29(X0) )
| ~ spl0_255 ),
inference(resolution,[],[f3377,f162]) ).
fof(f5470,plain,
( m_and_h_gate_v_out(c_e_h_3,c_i,s1)
| ~ spl0_147 ),
inference(resolution,[],[f1855,f1604]) ).
fof(f5476,plain,
( spl0_150
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f5470,f1840,f1887]) ).
fof(f5490,plain,
( m_and_h_gate_v_in1(c_e_h_3,c_i,s0)
| ~ spl0_150 ),
inference(resolution,[],[f1889,f659]) ).
fof(f5492,plain,
( $false
| ~ spl0_150 ),
inference(forward_subsumption_resolution,[],[f5490,f356]) ).
fof(f5493,plain,
~ spl0_150,
inference(avatar_contradiction_clause,[],[f5492]) ).
fof(f5961,plain,
( until2p29(s4)
| ~ spl0_255 ),
inference(resolution,[],[f5427,f4]) ).
fof(f5968,plain,
( xuntil2p30(s4)
| node26(s4)
| ~ spl0_255 ),
inference(resolution,[],[f5961,f161]) ).
fof(f5969,plain,
( node26(s4)
| spl0_214
| ~ spl0_255 ),
inference(forward_subsumption_resolution,[],[f5968,f2612]) ).
fof(f5970,plain,
( $false
| spl0_171
| spl0_214
| ~ spl0_255 ),
inference(forward_subsumption_resolution,[],[f5969,f2059]) ).
fof(f5971,plain,
( spl0_171
| spl0_214
| ~ spl0_255 ),
inference(avatar_contradiction_clause,[],[f5970]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f296]) ).
cnf(s2,plain,
( ~ spl0_2
| spl0_3
| spl0_4
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f317]) ).
cnf(s3,plain,
( spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f327]) ).
cnf(s5,plain,
~ spl0_8,
inference(sat_conversion,[],[f393]) ).
cnf(s7,plain,
( ~ spl0_9
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f424]) ).
cnf(s16,plain,
spl0_29,
inference(sat_conversion,[],[f707]) ).
cnf(s17,plain,
spl0_31,
inference(sat_conversion,[],[f708]) ).
cnf(s24,plain,
spl0_32,
inference(sat_conversion,[],[f742]) ).
cnf(s25,plain,
( ~ spl0_12
| ~ spl0_29
| ~ spl0_31
| ~ spl0_32 ),
inference(sat_conversion,[],[f744]) ).
cnf(s54,plain,
( spl0_42
| spl0_49 ),
inference(sat_conversion,[],[f976]) ).
cnf(s58,plain,
( spl0_45
| spl0_52 ),
inference(sat_conversion,[],[f993]) ).
cnf(s61,plain,
( spl0_48
| spl0_58 ),
inference(sat_conversion,[],[f1014]) ).
cnf(s62,plain,
( spl0_51
| spl0_58 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s63,plain,
( ~ spl0_48
| ~ spl0_51
| ~ spl0_54
| ~ spl0_75 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s66,plain,
( spl0_54
| spl0_61 ),
inference(sat_conversion,[],[f1036]) ).
cnf(s83,plain,
~ spl0_43,
inference(sat_conversion,[],[f1190]) ).
cnf(s137,plain,
~ spl0_40,
inference(sat_conversion,[],[f1715]) ).
cnf(s153,plain,
( ~ spl0_69
| spl0_145
| ~ spl0_146
| spl0_147 ),
inference(sat_conversion,[],[f1843]) ).
cnf(s156,plain,
( spl0_73
| ~ spl0_145 ),
inference(sat_conversion,[],[f1853]) ).
cnf(s159,plain,
( spl0_146
| spl0_148 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s172,plain,
~ spl0_148,
inference(sat_conversion,[],[f2014]) ).
cnf(s177,plain,
( spl0_57
| spl0_74 ),
inference(sat_conversion,[],[f2045]) ).
cnf(s178,plain,
( spl0_60
| spl0_74 ),
inference(sat_conversion,[],[f2046]) ).
cnf(s179,plain,
( spl0_58
| ~ spl0_73
| ~ spl0_74 ),
inference(sat_conversion,[],[f2047]) ).
cnf(s192,plain,
( spl0_40
| ~ spl0_49 ),
inference(sat_conversion,[],[f2137]) ).
cnf(s193,plain,
( spl0_43
| ~ spl0_52 ),
inference(sat_conversion,[],[f2140]) ).
cnf(s200,plain,
( spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f2148]) ).
cnf(s202,plain,
( ~ spl0_39
| ~ spl0_42
| ~ spl0_45
| ~ spl0_70 ),
inference(sat_conversion,[],[f2151]) ).
cnf(s222,plain,
( spl0_49
| ~ spl0_58
| ~ spl0_69 ),
inference(sat_conversion,[],[f2359]) ).
cnf(s252,plain,
~ spl0_214,
inference(sat_conversion,[],[f2618]) ).
cnf(s290,plain,
( ~ spl0_7
| spl0_8
| spl0_12
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s292,plain,
( ~ spl0_6
| spl0_12
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(sat_conversion,[],[f3123]) ).
cnf(s293,plain,
( ~ spl0_3
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(sat_conversion,[],[f3143]) ).
cnf(s314,plain,
( ~ spl0_5
| spl0_70
| spl0_75
| spl0_171
| spl0_214
| ~ spl0_227 ),
inference(sat_conversion,[],[f3373]) ).
cnf(s330,plain,
( ~ spl0_71
| spl0_262
| spl0_263 ),
inference(sat_conversion,[],[f3561]) ).
cnf(s335,plain,
( spl0_52
| ~ spl0_61
| ~ spl0_71 ),
inference(sat_conversion,[],[f3578]) ).
cnf(s337,plain,
( ~ spl0_1
| ~ spl0_227 ),
inference(sat_conversion,[],[f3614]) ).
cnf(s342,plain,
( ~ spl0_4
| spl0_75
| ~ spl0_227
| spl0_255 ),
inference(sat_conversion,[],[f3658]) ).
cnf(s346,plain,
( spl0_63
| spl0_77 ),
inference(sat_conversion,[],[f3673]) ).
cnf(s446,plain,
( spl0_61
| ~ spl0_76
| ~ spl0_77 ),
inference(sat_conversion,[],[f4225]) ).
cnf(s550,plain,
spl0_71,
inference(sat_conversion,[],[f5076]) ).
cnf(s580,plain,
( ~ spl0_262
| spl0_264
| spl0_265 ),
inference(sat_conversion,[],[f5134]) ).
cnf(s599,plain,
( ~ spl0_265
| spl0_348 ),
inference(sat_conversion,[],[f5221]) ).
cnf(s601,plain,
~ spl0_348,
inference(sat_conversion,[],[f5236]) ).
cnf(s608,plain,
( spl0_76
| ~ spl0_263 ),
inference(sat_conversion,[],[f5257]) ).
cnf(s615,plain,
( ~ spl0_71
| spl0_263
| ~ spl0_264
| spl0_265 ),
inference(sat_conversion,[],[f5261]) ).
cnf(s633,plain,
( spl0_69
| spl0_148 ),
inference(sat_conversion,[],[f5295]) ).
cnf(s639,plain,
( ~ spl0_13
| spl0_70
| spl0_75
| spl0_171
| spl0_227 ),
inference(sat_conversion,[],[f5302]) ).
cnf(s645,plain,
( ~ spl0_57
| ~ spl0_60
| ~ spl0_63
| ~ spl0_171 ),
inference(sat_conversion,[],[f5310]) ).
cnf(s666,plain,
( ~ spl0_147
| spl0_150 ),
inference(sat_conversion,[],[f5476]) ).
cnf(s668,plain,
~ spl0_150,
inference(sat_conversion,[],[f5493]) ).
cnf(s719,plain,
( spl0_171
| spl0_214
| ~ spl0_255 ),
inference(sat_conversion,[],[f5971]) ).
cnf(s720,plain,
~ spl0_147,
inference(rat,[],[s666,s668]) ).
cnf(s723,plain,
~ spl0_265,
inference(rat,[],[s599,s601]) ).
cnf(s732,plain,
( ~ spl0_262
| spl0_264 ),
inference(rat,[],[s580,s723]) ).
cnf(s739,plain,
( spl0_52
| ~ spl0_61 ),
inference(rat,[],[s335,s550]) ).
cnf(s742,plain,
( spl0_262
| spl0_263 ),
inference(rat,[],[s330,s550]) ).
cnf(s757,plain,
spl0_69,
inference(rat,[],[s633,s172]) ).
cnf(s760,plain,
spl0_146,
inference(rat,[],[s159,s172]) ).
cnf(s761,plain,
spl0_145,
inference(rat,[],[s153,s720,s760,s757]) ).
cnf(s762,plain,
spl0_73,
inference(rat,[],[s156,s761]) ).
cnf(s770,plain,
spl0_39,
inference(rat,[],[s200,s137]) ).
cnf(s771,plain,
~ spl0_49,
inference(rat,[],[s192,s137]) ).
cnf(s773,plain,
~ spl0_58,
inference(rat,[],[s222,s757,s771]) ).
cnf(s775,plain,
~ spl0_74,
inference(rat,[],[s179,s762,s773]) ).
cnf(s776,plain,
spl0_60,
inference(rat,[],[s178,s775]) ).
cnf(s777,plain,
spl0_57,
inference(rat,[],[s177,s775]) ).
cnf(s792,plain,
~ spl0_52,
inference(rat,[],[s193,s83]) ).
cnf(s793,plain,
~ spl0_61,
inference(rat,[],[s739,s792]) ).
cnf(s795,plain,
spl0_54,
inference(rat,[],[s66,s793]) ).
cnf(s796,plain,
( ~ spl0_48
| ~ spl0_51
| ~ spl0_75 ),
inference(rat,[],[s63,s795]) ).
cnf(s797,plain,
spl0_51,
inference(rat,[],[s62,s773]) ).
cnf(s798,plain,
spl0_48,
inference(rat,[],[s61,s773]) ).
cnf(s799,plain,
~ spl0_75,
inference(rat,[],[s796,s797,s798]) ).
cnf(s800,plain,
spl0_45,
inference(rat,[],[s58,s792]) ).
cnf(s802,plain,
spl0_42,
inference(rat,[],[s54,s771]) ).
cnf(s803,plain,
~ spl0_70,
inference(rat,[],[s202,s800,s770,s802]) ).
cnf(s806,plain,
~ spl0_12,
inference(rat,[],[s25,s24,s17,s16]) ).
cnf(s807,plain,
( ~ spl0_9
| spl0_13 ),
inference(rat,[],[s7,s806]) ).
cnf(s808,plain,
spl0_9,
inference(rat,[],[s3,s5]) ).
cnf(s809,plain,
spl0_13,
inference(rat,[],[s807,s808]) ).
cnf(s814,plain,
spl0_263,
inference(rat,[],[s732,s742,s615,s550,s723]) ).
cnf(s815,plain,
spl0_76,
inference(rat,[],[s608,s814]) ).
cnf(s816,plain,
~ spl0_77,
inference(rat,[],[s446,s793,s815]) ).
cnf(s818,plain,
spl0_63,
inference(rat,[],[s346,s816]) ).
cnf(s819,plain,
~ spl0_171,
inference(rat,[],[s645,s777,s776,s818]) ).
cnf(s820,plain,
~ spl0_255,
inference(rat,[],[s719,s252,s819]) ).
cnf(s822,plain,
spl0_227,
inference(rat,[],[s639,s809,s803,s799,s819]) ).
cnf(s823,plain,
~ spl0_5,
inference(rat,[],[s314,s822,s252,s803,s799,s819]) ).
cnf(s824,plain,
~ spl0_6,
inference(rat,[],[s292,s822,s252,s806,s799,s803,s819]) ).
cnf(s826,plain,
~ spl0_4,
inference(rat,[],[s342,s820,s799,s822]) ).
cnf(s827,plain,
~ spl0_7,
inference(rat,[],[s290,s819,s252,s5,s799,s803,s806,s822]) ).
cnf(s828,plain,
~ spl0_3,
inference(rat,[],[s293,s819,s252,s822]) ).
cnf(s829,plain,
~ spl0_2,
inference(rat,[],[s2,s823,s826,s828,s827,s824]) ).
cnf(s830,plain,
~ spl0_1,
inference(rat,[],[s337,s822]) ).
cnf(s831,plain,
$false,
inference(rat,[],[s1,s829,s830]) ).
fof(f5972,plain,
$false,
inference(avatar_sat_refutation,[],[s831]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV419-1.005 : TPTP v9.3.1. Released v3.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.25 % Computer : n008.cluster.edu
% 0.12/0.25 % Model : x86_64 x86_64
% 0.12/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.25 % Memory : 8046.5625MB
% 0.12/0.25 % OS : Linux 6.8.0-71-generic
% 0.12/0.25 % CPULimit : 300
% 0.12/0.25 % WCLimit : 300
% 0.12/0.25 % DateTime : Mon Sep 28 10:56:25 UTC 2026
% 0.12/0.25 % CPUTime :
% 0.12/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.30 Running first-order model finding
% 0.25/0.30 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.11/0.62 % (2170928)Will run a generic schedule for satisfiability detection.
% 2.11/0.62 % (2170934)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3911961738_2999 on theBenchmark for (2999ds/0Mi)
% 2.11/0.62 % (2170940)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=267230517:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.11/0.62 % Detected minimum model sizes of [1]
% 2.11/0.62 % Detected maximum model sizes of [26]
% 2.11/0.62 % TRYING [1]
% 2.11/0.62 % TRYING [2]
% 2.11/0.62 % (2170935)% WARNING: option uhcvi not known.
% 2.11/0.62 % (2170936)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1416572213:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.11/0.62 % TRYING [3]
% 2.11/0.62 % (2170935)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3968372449:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.11/0.62 % (2170937)dis+10_1_sil=32000:sp=arity:random_seed=3715115582:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.11/0.62 % (2170939)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2061583783:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.11/0.62 % (2170938)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2127172444:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.11/0.62 % TRYING [4]
% 2.11/0.62 % TRYING [5]
% 2.11/0.62 % TRYING [6]
% 2.11/0.62 % (2170938)Instruction limit reached!
% 2.11/0.62 % (2170938)------------------------------
% 2.11/0.62 % (2170938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.62 % (2170938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.62 % (2170938)CaDiCaL version: 2.1.3
% 2.11/0.62 % (2170938)Termination reason: Instruction limit
% 2.11/0.62 % (2170938)Termination phase: Saturation
% 2.11/0.62 % (2170938)Time elapsed: 0.090 s
% 2.11/0.62 % (2170938)Peak memory usage: 12 MB
% 2.11/0.62 % (2170938)Instructions burned: 117 (million)
% 2.11/0.62 % (2170948)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=880627112:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 2.11/0.62 % Detected minimum model sizes of [1]
% 2.11/0.62 % TRYING [7]
% 2.11/0.62 % Detected maximum model sizes of [26]
% 2.11/0.62 % TRYING [1]
% 2.11/0.62 % TRYING [2]
% 2.11/0.62 % TRYING [3]
% 2.11/0.62 % (2170939)Instruction limit reached!
% 2.11/0.62 % (2170939)------------------------------
% 2.11/0.62 % (2170939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.62 % (2170939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.62 % (2170939)CaDiCaL version: 2.1.3
% 2.11/0.62 % (2170939)Termination reason: Instruction limit
% 2.11/0.62 % (2170939)Termination phase: Saturation
% 2.11/0.62 % (2170939)Time elapsed: 0.128 s
% 2.11/0.62 % (2170939)Peak memory usage: 12 MB
% 2.11/0.62 % (2170939)Instructions burned: 131 (million)
% 2.11/0.62 % (2170940)Instruction limit reached!
% 2.11/0.62 % (2170940)------------------------------
% 2.11/0.62 % (2170940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.62 % (2170940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.62 % (2170940)CaDiCaL version: 2.1.3
% 2.11/0.62 % (2170940)Termination reason: Instruction limit
% 2.11/0.62 % (2170940)Termination phase: Saturation
% 2.11/0.62 % (2170940)Time elapsed: 0.143 s
% 2.11/0.62 % (2170940)Peak memory usage: 13 MB
% 2.11/0.62 % (2170940)Instructions burned: 159 (million)
% 2.11/0.62 % (2170937)Instruction limit reached!
% 2.11/0.62 % (2170937)------------------------------
% 2.11/0.62 % (2170937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.62 % (2170937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.62 % (2170937)CaDiCaL version: 2.1.3
% 2.11/0.62 % (2170937)Termination reason: Instruction limit
% 2.11/0.62 % (2170937)Termination phase: Saturation
% 2.11/0.62 % (2170937)Time elapsed: 0.134 s
% 2.11/0.62 % (2170937)Peak memory usage: 12 MB
% 2.11/0.62 % (2170937)Instructions burned: 104 (million)
% 2.11/0.62 % TRYING [4]
% 2.11/0.62 % (2170951)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=500038989:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 2.11/0.62 % (2170952)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3225947081:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.11/0.62 % (2170953)ott-21_1_sil=16000:fs=off:random_seed=3472419611:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.11/0.62 % TRYING [8]
% 2.11/0.62 % TRYING [5]
% 2.11/0.62 % TRYING [6]
% 2.11/0.62 % TRYING [9]
% 2.11/0.62 % (2170935) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2170928-2170935"...
% 2.11/0.62 % (2170935)...printing done.
% 2.11/0.62 % (2170935)Refutation found. Thanks to Tanya!
% 2.11/0.62 % SZS status Unsatisfiable for theBenchmark
% 2.11/0.62 % SZS output start Proof for theBenchmark
% See solution above
% 2.11/0.63 % (2170935)------------------------------
% 2.11/0.63 % (2170935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.63 % (2170935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.63 % (2170935)CaDiCaL version: 2.1.3
% 2.11/0.63 % (2170935)Termination reason: Refutation
% 2.11/0.63 % (2170935)Time elapsed: 0.268 s
% 2.11/0.63 % (2170935)Peak memory usage: 15 MB
% 2.11/0.63 % (2170935)Instructions burned: 244 (million)
% 2.11/0.63 % (2170928)Success in time 0.313 s
% 2.11/0.63 % Vampire exiting
%------------------------------------------------------------------------------