%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX069+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:45:48 PM UTC 2026
% Result : Theorem 10.41s 3.52s
% Output : Refutation 19.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 70
% Syntax : Number of formulae : 888 ( 42 unt; 50 def)
% Number of atoms : 4326 ( 796 equ)
% Maximal formula atoms : 69 ( 4 avg)
% Number of connectives : 5503 (2065 ~;2842 |; 481 &)
% ( 46 <=>; 69 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 57 ( 55 usr; 32 prp; 0-3 aty)
% Number of functors : 51 ( 51 usr; 11 con; 0-3 aty)
% Number of variables : 1125 ( 0 sgn 909 !; 216 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
'1' != '0',
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id16) ).
fof(f25,axiom,
! [X0,X1] :
( p(X0) = p(X1)
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id25) ).
fof(f26,axiom,
! [X0,X1] : p(X0) != neg(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id26) ).
fof(f27,axiom,
! [X0,X1,X2] : p(X0) != and(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id27) ).
fof(f28,axiom,
! [X0,X1,X2] : p(X0) != or(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id28) ).
fof(f29,axiom,
! [X0,X1] :
( neg(X0) = neg(X1)
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id29) ).
fof(f30,axiom,
! [X0,X1,X2] : neg(X0) != and(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id30) ).
fof(f31,axiom,
! [X0,X1,X2] : neg(X0) != or(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id31) ).
fof(f32,axiom,
! [X0,X1,X2,X3] :
( and(X0,X1) = and(X2,X3)
=> X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id32) ).
fof(f33,axiom,
! [X0,X1,X2,X3] :
( and(X0,X1) = and(X2,X3)
=> X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id33) ).
fof(f34,axiom,
! [X0,X1,X2,X3] : and(X0,X1) != or(X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id34) ).
fof(f35,axiom,
! [X0,X1,X2,X3] :
( or(X0,X1) = or(X2,X3)
=> X1 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id35) ).
fof(f36,axiom,
! [X0,X1,X2,X3] :
( or(X0,X1) = or(X2,X3)
=> X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id36) ).
fof(f74,axiom,
! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
<=> ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& eval_succeeds(X4,X1,'0') )
| ? [X5,X6] :
( X0 = or(X5,X6)
& X2 = '1'
& eval_succeeds(X6,X1,'1') )
| ? [X7,X8] :
( X0 = or(X7,X8)
& X2 = '1'
& eval_succeeds(X7,X1,'1') )
| ? [X9,X10] :
( X0 = and(X9,X10)
& X2 = '0'
& eval_succeeds(X10,X1,'0') )
| ? [X11,X12] :
( X0 = and(X11,X12)
& X2 = '0'
& eval_succeeds(X11,X1,'0') )
| ? [X13,X14] :
( X0 = and(X13,X14)
& X2 = '1'
& eval_succeeds(X13,X1,'1')
& eval_succeeds(X14,X1,'1') )
| ? [X15] :
( X0 = neg(X15)
& X2 = '0'
& eval_succeeds(X15,X1,'1') )
| ? [X16] :
( X0 = neg(X16)
& X2 = '1'
& eval_succeeds(X16,X1,'0') )
| ? [X17] :
( X0 = p(X17)
& X2 = '0'
& member_succeeds(neg(p(X17)),X1) )
| ? [X18] :
( X0 = p(X18)
& X2 = '1'
& member_succeeds(p(X18),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id74) ).
fof(f104,axiom,
! [X0,X1] :
( member_succeeds(X0,X1)
<=> ( ? [X2,X3] :
( X1 = cons(X2,X3)
& member_succeeds(X0,X3) )
| ? [X4] : X1 = cons(X0,X4) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id104) ).
fof(f110,axiom,
! [X0,X1] :
( sub(X0,X1)
<=> ! [X2] :
( member_succeeds(X2,X0)
=> member_succeeds(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','sub/2') ).
fof(f119,axiom,
! [X0] :
( interpretation_succeeds(X0)
=> ( literal_list_succeeds(X0)
& ~ ? [X1] :
( member_succeeds(p(X1),X0)
& member_succeeds(neg(p(X1)),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(interpretation:elimination)') ).
fof(f141,axiom,
! [X0,X1,X2,X3] :
( ( eval_succeeds(X0,X1,X3)
& sub(X1,X2) )
=> eval_succeeds(X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','corollary-(eval:sub)') ).
fof(f144,axiom,
( ! [X0,X1,X2] :
( ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X3,X1,X5)
=> '0' = X5 ) )
& eval_succeeds(X4,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X4,X1,X5)
=> '0' = X5 ) ) )
| ? [X6,X7] :
( X0 = or(X6,X7)
& X2 = '1'
& eval_succeeds(X7,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X7,X1,X5)
=> '1' = X5 ) ) )
| ? [X8,X9] :
( X0 = or(X8,X9)
& X2 = '1'
& eval_succeeds(X8,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X8,X1,X5)
=> '1' = X5 ) ) )
| ? [X10,X11] :
( X0 = and(X10,X11)
& X2 = '0'
& eval_succeeds(X11,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X11,X1,X5)
=> '0' = X5 ) ) )
| ? [X12,X13] :
( X0 = and(X12,X13)
& X2 = '0'
& eval_succeeds(X12,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X12,X1,X5)
=> '0' = X5 ) ) )
| ? [X14,X15] :
( X0 = and(X14,X15)
& X2 = '1'
& eval_succeeds(X14,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X14,X1,X5)
=> '1' = X5 ) )
& eval_succeeds(X15,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X15,X1,X5)
=> '1' = X5 ) ) )
| ? [X16] :
( X0 = neg(X16)
& X2 = '0'
& eval_succeeds(X16,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X16,X1,X5)
=> '1' = X5 ) ) )
| ? [X17] :
( X0 = neg(X17)
& X2 = '1'
& eval_succeeds(X17,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X17,X1,X5)
=> '0' = X5 ) ) )
| ? [X18] :
( X0 = p(X18)
& X2 = '0'
& member_succeeds(neg(p(X18)),X1) )
| ? [X19] :
( X0 = p(X19)
& X2 = '1'
& member_succeeds(p(X19),X1) ) )
=> ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X0,X1,X5)
=> X2 = X5 ) ) )
=> ! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
=> ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X0,X1,X5)
=> X2 = X5 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',induction) ).
fof(f145,conjecture,
! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
=> ( interpretation_succeeds(X1)
=> ! [X3] :
( eval_succeeds(X0,X1,X3)
=> X2 = X3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(eval:function)') ).
fof(f146,negated_conjecture,
~ ! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
=> ( interpretation_succeeds(X1)
=> ! [X3] :
( eval_succeeds(X0,X1,X3)
=> X2 = X3 ) ) ),
inference(negated_conjecture,[status(cth)],[f145]) ).
fof(f165,plain,
( ! [X0,X1,X2] :
( ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X5] :
( eval_succeeds(X3,X1,X5)
=> '0' = X5 ) )
& eval_succeeds(X4,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X6] :
( eval_succeeds(X4,X1,X6)
=> '0' = X6 ) ) )
| ? [X7,X8] :
( or(X7,X8) = X0
& X2 = '1'
& eval_succeeds(X8,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X9] :
( eval_succeeds(X8,X1,X9)
=> '1' = X9 ) ) )
| ? [X10,X11] :
( or(X10,X11) = X0
& X2 = '1'
& eval_succeeds(X10,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X12] :
( eval_succeeds(X10,X1,X12)
=> '1' = X12 ) ) )
| ? [X13,X14] :
( and(X13,X14) = X0
& X2 = '0'
& eval_succeeds(X14,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X15] :
( eval_succeeds(X14,X1,X15)
=> '0' = X15 ) ) )
| ? [X16,X17] :
( and(X16,X17) = X0
& X2 = '0'
& eval_succeeds(X16,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X18] :
( eval_succeeds(X16,X1,X18)
=> '0' = X18 ) ) )
| ? [X19,X20] :
( and(X19,X20) = X0
& X2 = '1'
& eval_succeeds(X19,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X21] :
( eval_succeeds(X19,X1,X21)
=> '1' = X21 ) )
& eval_succeeds(X20,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X22] :
( eval_succeeds(X20,X1,X22)
=> '1' = X22 ) ) )
| ? [X23] :
( neg(X23) = X0
& X2 = '0'
& eval_succeeds(X23,X1,'1')
& ( interpretation_succeeds(X1)
=> ! [X24] :
( eval_succeeds(X23,X1,X24)
=> '1' = X24 ) ) )
| ? [X25] :
( neg(X25) = X0
& X2 = '1'
& eval_succeeds(X25,X1,'0')
& ( interpretation_succeeds(X1)
=> ! [X26] :
( eval_succeeds(X25,X1,X26)
=> '0' = X26 ) ) )
| ? [X27] :
( p(X27) = X0
& X2 = '0'
& member_succeeds(neg(p(X27)),X1) )
| ? [X28] :
( p(X28) = X0
& X2 = '1'
& member_succeeds(p(X28),X1) ) )
=> ( interpretation_succeeds(X1)
=> ! [X29] :
( eval_succeeds(X0,X1,X29)
=> X2 = X29 ) ) )
=> ! [X30,X31,X32] :
( eval_succeeds(X30,X31,X32)
=> ( interpretation_succeeds(X31)
=> ! [X33] :
( eval_succeeds(X30,X31,X33)
=> X32 = X33 ) ) ) ),
inference(rectify,[],[f144]) ).
fof(f169,plain,
! [X0,X1] :
( X0 = X1
| p(X0) != p(X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f170,plain,
! [X0,X1] :
( X0 = X1
| neg(X0) != neg(X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f171,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| and(X0,X1) != and(X2,X3) ),
inference(ennf_transformation,[],[f32]) ).
fof(f172,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| and(X0,X1) != and(X2,X3) ),
inference(ennf_transformation,[],[f33]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| or(X0,X1) != or(X2,X3) ),
inference(ennf_transformation,[],[f35]) ).
fof(f174,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| or(X0,X1) != or(X2,X3) ),
inference(ennf_transformation,[],[f36]) ).
fof(f216,plain,
! [X0,X1] :
( sub(X0,X1)
<=> ! [X2] :
( member_succeeds(X2,X1)
| ~ member_succeeds(X2,X0) ) ),
inference(ennf_transformation,[],[f110]) ).
fof(f226,plain,
! [X0] :
( ( literal_list_succeeds(X0)
& ! [X1] :
( ~ member_succeeds(p(X1),X0)
| ~ member_succeeds(neg(p(X1)),X0) ) )
| ~ interpretation_succeeds(X0) ),
inference(ennf_transformation,[],[f119]) ).
fof(f262,plain,
! [X0,X1,X2,X3] :
( eval_succeeds(X0,X2,X3)
| ~ eval_succeeds(X0,X1,X3)
| ~ sub(X1,X2) ),
inference(ennf_transformation,[],[f141]) ).
fof(f263,plain,
! [X0,X1,X2,X3] :
( eval_succeeds(X0,X2,X3)
| ~ eval_succeeds(X0,X1,X3)
| ~ sub(X1,X2) ),
inference(flattening,[],[f262]) ).
fof(f267,plain,
( ! [X30,X31,X32] :
( ! [X33] :
( X32 = X33
| ~ eval_succeeds(X30,X31,X33) )
| ~ interpretation_succeeds(X31)
| ~ eval_succeeds(X30,X31,X32) )
| ? [X0,X1,X2] :
( ? [X29] :
( X2 != X29
& eval_succeeds(X0,X1,X29) )
& interpretation_succeeds(X1)
& ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(X3,X1,X5) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X4,X1,'0')
& ( ! [X6] :
( '0' = X6
| ~ eval_succeeds(X4,X1,X6) )
| ~ interpretation_succeeds(X1) ) )
| ? [X7,X8] :
( or(X7,X8) = X0
& X2 = '1'
& eval_succeeds(X8,X1,'1')
& ( ! [X9] :
( '1' = X9
| ~ eval_succeeds(X8,X1,X9) )
| ~ interpretation_succeeds(X1) ) )
| ? [X10,X11] :
( or(X10,X11) = X0
& X2 = '1'
& eval_succeeds(X10,X1,'1')
& ( ! [X12] :
( '1' = X12
| ~ eval_succeeds(X10,X1,X12) )
| ~ interpretation_succeeds(X1) ) )
| ? [X13,X14] :
( and(X13,X14) = X0
& X2 = '0'
& eval_succeeds(X14,X1,'0')
& ( ! [X15] :
( '0' = X15
| ~ eval_succeeds(X14,X1,X15) )
| ~ interpretation_succeeds(X1) ) )
| ? [X16,X17] :
( and(X16,X17) = X0
& X2 = '0'
& eval_succeeds(X16,X1,'0')
& ( ! [X18] :
( '0' = X18
| ~ eval_succeeds(X16,X1,X18) )
| ~ interpretation_succeeds(X1) ) )
| ? [X19,X20] :
( and(X19,X20) = X0
& X2 = '1'
& eval_succeeds(X19,X1,'1')
& ( ! [X21] :
( '1' = X21
| ~ eval_succeeds(X19,X1,X21) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X20,X1,'1')
& ( ! [X22] :
( '1' = X22
| ~ eval_succeeds(X20,X1,X22) )
| ~ interpretation_succeeds(X1) ) )
| ? [X23] :
( neg(X23) = X0
& X2 = '0'
& eval_succeeds(X23,X1,'1')
& ( ! [X24] :
( '1' = X24
| ~ eval_succeeds(X23,X1,X24) )
| ~ interpretation_succeeds(X1) ) )
| ? [X25] :
( neg(X25) = X0
& X2 = '1'
& eval_succeeds(X25,X1,'0')
& ( ! [X26] :
( '0' = X26
| ~ eval_succeeds(X25,X1,X26) )
| ~ interpretation_succeeds(X1) ) )
| ? [X27] :
( p(X27) = X0
& X2 = '0'
& member_succeeds(neg(p(X27)),X1) )
| ? [X28] :
( p(X28) = X0
& X2 = '1'
& member_succeeds(p(X28),X1) ) ) ) ),
inference(ennf_transformation,[],[f165]) ).
fof(f268,plain,
( ! [X30,X31,X32] :
( ! [X33] :
( X32 = X33
| ~ eval_succeeds(X30,X31,X33) )
| ~ interpretation_succeeds(X31)
| ~ eval_succeeds(X30,X31,X32) )
| ? [X0,X1,X2] :
( ? [X29] :
( X2 != X29
& eval_succeeds(X0,X1,X29) )
& interpretation_succeeds(X1)
& ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(X3,X1,X5) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X4,X1,'0')
& ( ! [X6] :
( '0' = X6
| ~ eval_succeeds(X4,X1,X6) )
| ~ interpretation_succeeds(X1) ) )
| ? [X7,X8] :
( or(X7,X8) = X0
& X2 = '1'
& eval_succeeds(X8,X1,'1')
& ( ! [X9] :
( '1' = X9
| ~ eval_succeeds(X8,X1,X9) )
| ~ interpretation_succeeds(X1) ) )
| ? [X10,X11] :
( or(X10,X11) = X0
& X2 = '1'
& eval_succeeds(X10,X1,'1')
& ( ! [X12] :
( '1' = X12
| ~ eval_succeeds(X10,X1,X12) )
| ~ interpretation_succeeds(X1) ) )
| ? [X13,X14] :
( and(X13,X14) = X0
& X2 = '0'
& eval_succeeds(X14,X1,'0')
& ( ! [X15] :
( '0' = X15
| ~ eval_succeeds(X14,X1,X15) )
| ~ interpretation_succeeds(X1) ) )
| ? [X16,X17] :
( and(X16,X17) = X0
& X2 = '0'
& eval_succeeds(X16,X1,'0')
& ( ! [X18] :
( '0' = X18
| ~ eval_succeeds(X16,X1,X18) )
| ~ interpretation_succeeds(X1) ) )
| ? [X19,X20] :
( and(X19,X20) = X0
& X2 = '1'
& eval_succeeds(X19,X1,'1')
& ( ! [X21] :
( '1' = X21
| ~ eval_succeeds(X19,X1,X21) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X20,X1,'1')
& ( ! [X22] :
( '1' = X22
| ~ eval_succeeds(X20,X1,X22) )
| ~ interpretation_succeeds(X1) ) )
| ? [X23] :
( neg(X23) = X0
& X2 = '0'
& eval_succeeds(X23,X1,'1')
& ( ! [X24] :
( '1' = X24
| ~ eval_succeeds(X23,X1,X24) )
| ~ interpretation_succeeds(X1) ) )
| ? [X25] :
( neg(X25) = X0
& X2 = '1'
& eval_succeeds(X25,X1,'0')
& ( ! [X26] :
( '0' = X26
| ~ eval_succeeds(X25,X1,X26) )
| ~ interpretation_succeeds(X1) ) )
| ? [X27] :
( p(X27) = X0
& X2 = '0'
& member_succeeds(neg(p(X27)),X1) )
| ? [X28] :
( p(X28) = X0
& X2 = '1'
& member_succeeds(p(X28),X1) ) ) ) ),
inference(flattening,[],[f267]) ).
fof(f269,plain,
? [X0,X1,X2] :
( ? [X3] :
( X2 != X3
& eval_succeeds(X0,X1,X3) )
& interpretation_succeeds(X1)
& eval_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f146]) ).
fof(f270,plain,
? [X0,X1,X2] :
( ? [X3] :
( X2 != X3
& eval_succeeds(X0,X1,X3) )
& interpretation_succeeds(X1)
& eval_succeeds(X0,X1,X2) ),
inference(flattening,[],[f269]) ).
fof(f283,definition,
! [X0,X2,X1] :
( sP9(X0,X2,X1)
<=> ? [X13,X14] :
( X0 = and(X13,X14)
& X2 = '1'
& eval_succeeds(X13,X1,'1')
& eval_succeeds(X14,X1,'1') ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f284,definition,
! [X0,X2,X1] :
( sP10(X0,X2,X1)
<=> ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& eval_succeeds(X4,X1,'0') ) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f285,definition,
! [X0,X2,X1] :
( sP11(X0,X2,X1)
<=> ? [X18] :
( X0 = p(X18)
& X2 = '1'
& member_succeeds(p(X18),X1) ) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f286,definition,
! [X0,X2,X1] :
( sP12(X0,X2,X1)
<=> ? [X17] :
( X0 = p(X17)
& X2 = '0'
& member_succeeds(neg(p(X17)),X1) ) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f287,definition,
! [X0,X2,X1] :
( sP13(X0,X2,X1)
<=> ? [X16] :
( X0 = neg(X16)
& X2 = '1'
& eval_succeeds(X16,X1,'0') ) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f288,definition,
! [X0,X2,X1] :
( sP14(X0,X2,X1)
<=> ? [X15] :
( X0 = neg(X15)
& X2 = '0'
& eval_succeeds(X15,X1,'1') ) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f289,definition,
! [X0,X2,X1] :
( sP15(X0,X2,X1)
<=> ? [X11,X12] :
( X0 = and(X11,X12)
& X2 = '0'
& eval_succeeds(X11,X1,'0') ) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f290,definition,
! [X0,X2,X1] :
( sP16(X0,X2,X1)
<=> ? [X9,X10] :
( X0 = and(X9,X10)
& X2 = '0'
& eval_succeeds(X10,X1,'0') ) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f291,definition,
! [X0,X2,X1] :
( sP17(X0,X2,X1)
<=> ? [X7,X8] :
( X0 = or(X7,X8)
& X2 = '1'
& eval_succeeds(X7,X1,'1') ) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f292,definition,
! [X1,X2,X0] :
( sP18(X1,X2,X0)
<=> ( sP10(X0,X2,X1)
| ? [X5,X6] :
( X0 = or(X5,X6)
& X2 = '1'
& eval_succeeds(X6,X1,'1') )
| sP17(X0,X2,X1)
| sP16(X0,X2,X1)
| sP15(X0,X2,X1)
| sP9(X0,X2,X1)
| sP14(X0,X2,X1)
| sP13(X0,X2,X1)
| sP12(X0,X2,X1)
| sP11(X0,X2,X1) ) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f293,plain,
! [X0,X1,X2] :
( eval_succeeds(X0,X1,X2)
<=> sP18(X1,X2,X0) ),
inference(definition_folding,[],[f74,f292,f291,f290,f289,f288,f287,f286,f285,f284,f283]) ).
fof(f349,definition,
! [X0,X2,X1] :
( ? [X19,X20] :
( and(X19,X20) = X0
& X2 = '1'
& eval_succeeds(X19,X1,'1')
& ( ! [X21] :
( '1' = X21
| ~ eval_succeeds(X19,X1,X21) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X20,X1,'1')
& ( ! [X22] :
( '1' = X22
| ~ eval_succeeds(X20,X1,X22) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP63(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f350,definition,
! [X0,X2,X1] :
( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(X3,X1,X5) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X4,X1,'0')
& ( ! [X6] :
( '0' = X6
| ~ eval_succeeds(X4,X1,X6) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP64(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f351,definition,
! [X0,X2,X1] :
( ? [X25] :
( neg(X25) = X0
& X2 = '1'
& eval_succeeds(X25,X1,'0')
& ( ! [X26] :
( '0' = X26
| ~ eval_succeeds(X25,X1,X26) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP65(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f352,definition,
! [X0,X2,X1] :
( ? [X23] :
( neg(X23) = X0
& X2 = '0'
& eval_succeeds(X23,X1,'1')
& ( ! [X24] :
( '1' = X24
| ~ eval_succeeds(X23,X1,X24) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP66(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f353,definition,
! [X0,X2,X1] :
( ? [X16,X17] :
( and(X16,X17) = X0
& X2 = '0'
& eval_succeeds(X16,X1,'0')
& ( ! [X18] :
( '0' = X18
| ~ eval_succeeds(X16,X1,X18) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP67(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f354,definition,
! [X0,X2,X1] :
( ? [X13,X14] :
( and(X13,X14) = X0
& X2 = '0'
& eval_succeeds(X14,X1,'0')
& ( ! [X15] :
( '0' = X15
| ~ eval_succeeds(X14,X1,X15) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP68(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f355,definition,
! [X0,X2,X1] :
( ? [X10,X11] :
( or(X10,X11) = X0
& X2 = '1'
& eval_succeeds(X10,X1,'1')
& ( ! [X12] :
( '1' = X12
| ~ eval_succeeds(X10,X1,X12) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP69(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f356,definition,
! [X0,X2,X1] :
( ? [X7,X8] :
( or(X7,X8) = X0
& X2 = '1'
& eval_succeeds(X8,X1,'1')
& ( ! [X9] :
( '1' = X9
| ~ eval_succeeds(X8,X1,X9) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP70(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f357,definition,
! [X0,X2,X1] :
( ? [X28] :
( p(X28) = X0
& X2 = '1'
& member_succeeds(p(X28),X1) )
| ~ sP71(X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f358,plain,
( ! [X30,X31,X32] :
( ! [X33] :
( X32 = X33
| ~ eval_succeeds(X30,X31,X33) )
| ~ interpretation_succeeds(X31)
| ~ eval_succeeds(X30,X31,X32) )
| ? [X0,X1,X2] :
( ? [X29] :
( X2 != X29
& eval_succeeds(X0,X1,X29) )
& interpretation_succeeds(X1)
& ( sP64(X0,X2,X1)
| sP70(X0,X2,X1)
| sP69(X0,X2,X1)
| sP68(X0,X2,X1)
| sP67(X0,X2,X1)
| sP63(X0,X2,X1)
| sP66(X0,X2,X1)
| sP65(X0,X2,X1)
| ? [X27] :
( p(X27) = X0
& X2 = '0'
& member_succeeds(neg(p(X27)),X1) )
| sP71(X0,X2,X1) ) ) ),
inference(definition_folding,[],[f268,f357,f356,f355,f354,f353,f352,f351,f350,f349]) ).
fof(f400,plain,
! [X1,X2,X0] :
( ( sP18(X1,X2,X0)
| ( ~ sP10(X0,X2,X1)
& ! [X5,X6] :
( or(X5,X6) != X0
| '1' != X2
| ~ eval_succeeds(X6,X1,'1') )
& ~ sP17(X0,X2,X1)
& ~ sP16(X0,X2,X1)
& ~ sP15(X0,X2,X1)
& ~ sP9(X0,X2,X1)
& ~ sP14(X0,X2,X1)
& ~ sP13(X0,X2,X1)
& ~ sP12(X0,X2,X1)
& ~ sP11(X0,X2,X1) ) )
& ( sP10(X0,X2,X1)
| ? [X5,X6] :
( X0 = or(X5,X6)
& X2 = '1'
& eval_succeeds(X6,X1,'1') )
| sP17(X0,X2,X1)
| sP16(X0,X2,X1)
| sP15(X0,X2,X1)
| sP9(X0,X2,X1)
| sP14(X0,X2,X1)
| sP13(X0,X2,X1)
| sP12(X0,X2,X1)
| sP11(X0,X2,X1)
| ~ sP18(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f292]) ).
fof(f401,plain,
! [X1,X2,X0] :
( ( sP18(X1,X2,X0)
| ( ~ sP10(X0,X2,X1)
& ! [X5,X6] :
( or(X5,X6) != X0
| '1' != X2
| ~ eval_succeeds(X6,X1,'1') )
& ~ sP17(X0,X2,X1)
& ~ sP16(X0,X2,X1)
& ~ sP15(X0,X2,X1)
& ~ sP9(X0,X2,X1)
& ~ sP14(X0,X2,X1)
& ~ sP13(X0,X2,X1)
& ~ sP12(X0,X2,X1)
& ~ sP11(X0,X2,X1) ) )
& ( sP10(X0,X2,X1)
| ? [X5,X6] :
( X0 = or(X5,X6)
& X2 = '1'
& eval_succeeds(X6,X1,'1') )
| sP17(X0,X2,X1)
| sP16(X0,X2,X1)
| sP15(X0,X2,X1)
| sP9(X0,X2,X1)
| sP14(X0,X2,X1)
| sP13(X0,X2,X1)
| sP12(X0,X2,X1)
| sP11(X0,X2,X1)
| ~ sP18(X1,X2,X0) ) ),
inference(flattening,[],[f400]) ).
fof(f402,plain,
! [X0,X1,X2] :
( ( sP18(X0,X1,X2)
| ( ~ sP10(X2,X1,X0)
& ! [X3,X4] :
( or(X3,X4) != X2
| '1' != X1
| ~ eval_succeeds(X4,X0,'1') )
& ~ sP17(X2,X1,X0)
& ~ sP16(X2,X1,X0)
& ~ sP15(X2,X1,X0)
& ~ sP9(X2,X1,X0)
& ~ sP14(X2,X1,X0)
& ~ sP13(X2,X1,X0)
& ~ sP12(X2,X1,X0)
& ~ sP11(X2,X1,X0) ) )
& ( sP10(X2,X1,X0)
| ? [X5,X6] :
( or(X5,X6) = X2
& '1' = X1
& eval_succeeds(X6,X0,'1') )
| sP17(X2,X1,X0)
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP9(X2,X1,X0)
| sP14(X2,X1,X0)
| sP13(X2,X1,X0)
| sP12(X2,X1,X0)
| sP11(X2,X1,X0)
| ~ sP18(X0,X1,X2) ) ),
inference(rectify,[],[f401]) ).
fof(f403,plain,
! [X0,X1,X2] :
( ( sP18(X0,X1,X2)
| ( ~ sP10(X2,X1,X0)
& ! [X3,X4] :
( or(X3,X4) != X2
| '1' != X1
| ~ eval_succeeds(X4,X0,'1') )
& ~ sP17(X2,X1,X0)
& ~ sP16(X2,X1,X0)
& ~ sP15(X2,X1,X0)
& ~ sP9(X2,X1,X0)
& ~ sP14(X2,X1,X0)
& ~ sP13(X2,X1,X0)
& ~ sP12(X2,X1,X0)
& ~ sP11(X2,X1,X0) ) )
& ( sP10(X2,X1,X0)
| ( or(sK93(X0,X1,X2),sK94(X0,X1,X2)) = X2
& '1' = X1
& eval_succeeds(sK94(X0,X1,X2),X0,'1') )
| sP17(X2,X1,X0)
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP9(X2,X1,X0)
| sP14(X2,X1,X0)
| sP13(X2,X1,X0)
| sP12(X2,X1,X0)
| sP11(X2,X1,X0)
| ~ sP18(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK93,sK94]),skolemize(X5,sK93(X0,X1,X2)),skolemize(X6,sK94(X0,X1,X2))],[f402]) ).
fof(f404,plain,
! [X0,X2,X1] :
( ( sP17(X0,X2,X1)
| ! [X7,X8] :
( or(X7,X8) != X0
| '1' != X2
| ~ eval_succeeds(X7,X1,'1') ) )
& ( ? [X7,X8] :
( X0 = or(X7,X8)
& X2 = '1'
& eval_succeeds(X7,X1,'1') )
| ~ sP17(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f291]) ).
fof(f405,plain,
! [X0,X1,X2] :
( ( sP17(X0,X1,X2)
| ! [X3,X4] :
( or(X3,X4) != X0
| '1' != X1
| ~ eval_succeeds(X3,X2,'1') ) )
& ( ? [X5,X6] :
( or(X5,X6) = X0
& '1' = X1
& eval_succeeds(X5,X2,'1') )
| ~ sP17(X0,X1,X2) ) ),
inference(rectify,[],[f404]) ).
fof(f406,plain,
! [X0,X1,X2] :
( ( sP17(X0,X1,X2)
| ! [X3,X4] :
( or(X3,X4) != X0
| '1' != X1
| ~ eval_succeeds(X3,X2,'1') ) )
& ( ( or(sK95(X0,X1,X2),sK96(X0,X1,X2)) = X0
& '1' = X1
& eval_succeeds(sK95(X0,X1,X2),X2,'1') )
| ~ sP17(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK95,sK96]),skolemize(X5,sK95(X0,X1,X2)),skolemize(X6,sK96(X0,X1,X2))],[f405]) ).
fof(f407,plain,
! [X0,X2,X1] :
( ( sP16(X0,X2,X1)
| ! [X9,X10] :
( and(X9,X10) != X0
| '0' != X2
| ~ eval_succeeds(X10,X1,'0') ) )
& ( ? [X9,X10] :
( X0 = and(X9,X10)
& X2 = '0'
& eval_succeeds(X10,X1,'0') )
| ~ sP16(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f290]) ).
fof(f408,plain,
! [X0,X1,X2] :
( ( sP16(X0,X1,X2)
| ! [X3,X4] :
( and(X3,X4) != X0
| '0' != X1
| ~ eval_succeeds(X4,X2,'0') ) )
& ( ? [X5,X6] :
( and(X5,X6) = X0
& '0' = X1
& eval_succeeds(X6,X2,'0') )
| ~ sP16(X0,X1,X2) ) ),
inference(rectify,[],[f407]) ).
fof(f409,plain,
! [X0,X1,X2] :
( ( sP16(X0,X1,X2)
| ! [X3,X4] :
( and(X3,X4) != X0
| '0' != X1
| ~ eval_succeeds(X4,X2,'0') ) )
& ( ( and(sK97(X0,X1,X2),sK98(X0,X1,X2)) = X0
& '0' = X1
& eval_succeeds(sK98(X0,X1,X2),X2,'0') )
| ~ sP16(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK97,sK98]),skolemize(X5,sK97(X0,X1,X2)),skolemize(X6,sK98(X0,X1,X2))],[f408]) ).
fof(f410,plain,
! [X0,X2,X1] :
( ( sP15(X0,X2,X1)
| ! [X11,X12] :
( and(X11,X12) != X0
| '0' != X2
| ~ eval_succeeds(X11,X1,'0') ) )
& ( ? [X11,X12] :
( X0 = and(X11,X12)
& X2 = '0'
& eval_succeeds(X11,X1,'0') )
| ~ sP15(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f289]) ).
fof(f411,plain,
! [X0,X1,X2] :
( ( sP15(X0,X1,X2)
| ! [X3,X4] :
( and(X3,X4) != X0
| '0' != X1
| ~ eval_succeeds(X3,X2,'0') ) )
& ( ? [X5,X6] :
( and(X5,X6) = X0
& '0' = X1
& eval_succeeds(X5,X2,'0') )
| ~ sP15(X0,X1,X2) ) ),
inference(rectify,[],[f410]) ).
fof(f412,plain,
! [X0,X1,X2] :
( ( sP15(X0,X1,X2)
| ! [X3,X4] :
( and(X3,X4) != X0
| '0' != X1
| ~ eval_succeeds(X3,X2,'0') ) )
& ( ( and(sK99(X0,X1,X2),sK100(X0,X1,X2)) = X0
& '0' = X1
& eval_succeeds(sK99(X0,X1,X2),X2,'0') )
| ~ sP15(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK99,sK100]),skolemize(X5,sK99(X0,X1,X2)),skolemize(X6,sK100(X0,X1,X2))],[f411]) ).
fof(f413,plain,
! [X0,X2,X1] :
( ( sP14(X0,X2,X1)
| ! [X15] :
( neg(X15) != X0
| '0' != X2
| ~ eval_succeeds(X15,X1,'1') ) )
& ( ? [X15] :
( X0 = neg(X15)
& X2 = '0'
& eval_succeeds(X15,X1,'1') )
| ~ sP14(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f288]) ).
fof(f414,plain,
! [X0,X1,X2] :
( ( sP14(X0,X1,X2)
| ! [X3] :
( neg(X3) != X0
| '0' != X1
| ~ eval_succeeds(X3,X2,'1') ) )
& ( ? [X4] :
( neg(X4) = X0
& '0' = X1
& eval_succeeds(X4,X2,'1') )
| ~ sP14(X0,X1,X2) ) ),
inference(rectify,[],[f413]) ).
fof(f415,plain,
! [X0,X1,X2] :
( ( sP14(X0,X1,X2)
| ! [X3] :
( neg(X3) != X0
| '0' != X1
| ~ eval_succeeds(X3,X2,'1') ) )
& ( ( neg(sK101(X0,X1,X2)) = X0
& '0' = X1
& eval_succeeds(sK101(X0,X1,X2),X2,'1') )
| ~ sP14(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK101]),skolemize(X4,sK101(X0,X1,X2))],[f414]) ).
fof(f416,plain,
! [X0,X2,X1] :
( ( sP13(X0,X2,X1)
| ! [X16] :
( neg(X16) != X0
| '1' != X2
| ~ eval_succeeds(X16,X1,'0') ) )
& ( ? [X16] :
( X0 = neg(X16)
& X2 = '1'
& eval_succeeds(X16,X1,'0') )
| ~ sP13(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f287]) ).
fof(f417,plain,
! [X0,X1,X2] :
( ( sP13(X0,X1,X2)
| ! [X3] :
( neg(X3) != X0
| '1' != X1
| ~ eval_succeeds(X3,X2,'0') ) )
& ( ? [X4] :
( neg(X4) = X0
& '1' = X1
& eval_succeeds(X4,X2,'0') )
| ~ sP13(X0,X1,X2) ) ),
inference(rectify,[],[f416]) ).
fof(f418,plain,
! [X0,X1,X2] :
( ( sP13(X0,X1,X2)
| ! [X3] :
( neg(X3) != X0
| '1' != X1
| ~ eval_succeeds(X3,X2,'0') ) )
& ( ( neg(sK102(X0,X1,X2)) = X0
& '1' = X1
& eval_succeeds(sK102(X0,X1,X2),X2,'0') )
| ~ sP13(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK102]),skolemize(X4,sK102(X0,X1,X2))],[f417]) ).
fof(f419,plain,
! [X0,X2,X1] :
( ( sP12(X0,X2,X1)
| ! [X17] :
( p(X17) != X0
| '0' != X2
| ~ member_succeeds(neg(p(X17)),X1) ) )
& ( ? [X17] :
( X0 = p(X17)
& X2 = '0'
& member_succeeds(neg(p(X17)),X1) )
| ~ sP12(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f286]) ).
fof(f420,plain,
! [X0,X1,X2] :
( ( sP12(X0,X1,X2)
| ! [X3] :
( p(X3) != X0
| '0' != X1
| ~ member_succeeds(neg(p(X3)),X2) ) )
& ( ? [X4] :
( p(X4) = X0
& '0' = X1
& member_succeeds(neg(p(X4)),X2) )
| ~ sP12(X0,X1,X2) ) ),
inference(rectify,[],[f419]) ).
fof(f421,plain,
! [X0,X1,X2] :
( ( sP12(X0,X1,X2)
| ! [X3] :
( p(X3) != X0
| '0' != X1
| ~ member_succeeds(neg(p(X3)),X2) ) )
& ( ( p(sK103(X0,X1,X2)) = X0
& '0' = X1
& member_succeeds(neg(p(sK103(X0,X1,X2))),X2) )
| ~ sP12(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK103]),skolemize(X4,sK103(X0,X1,X2))],[f420]) ).
fof(f422,plain,
! [X0,X2,X1] :
( ( sP11(X0,X2,X1)
| ! [X18] :
( p(X18) != X0
| '1' != X2
| ~ member_succeeds(p(X18),X1) ) )
& ( ? [X18] :
( X0 = p(X18)
& X2 = '1'
& member_succeeds(p(X18),X1) )
| ~ sP11(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f285]) ).
fof(f423,plain,
! [X0,X1,X2] :
( ( sP11(X0,X1,X2)
| ! [X3] :
( p(X3) != X0
| '1' != X1
| ~ member_succeeds(p(X3),X2) ) )
& ( ? [X4] :
( p(X4) = X0
& '1' = X1
& member_succeeds(p(X4),X2) )
| ~ sP11(X0,X1,X2) ) ),
inference(rectify,[],[f422]) ).
fof(f424,plain,
! [X0,X1,X2] :
( ( sP11(X0,X1,X2)
| ! [X3] :
( p(X3) != X0
| '1' != X1
| ~ member_succeeds(p(X3),X2) ) )
& ( ( p(sK104(X0,X1,X2)) = X0
& '1' = X1
& member_succeeds(p(sK104(X0,X1,X2)),X2) )
| ~ sP11(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK104]),skolemize(X4,sK104(X0,X1,X2))],[f423]) ).
fof(f425,plain,
! [X0,X2,X1] :
( ( sP10(X0,X2,X1)
| ! [X3,X4] :
( or(X3,X4) != X0
| '0' != X2
| ~ eval_succeeds(X3,X1,'0')
| ~ eval_succeeds(X4,X1,'0') ) )
& ( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& eval_succeeds(X4,X1,'0') )
| ~ sP10(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f284]) ).
fof(f426,plain,
! [X0,X1,X2] :
( ( sP10(X0,X1,X2)
| ! [X3,X4] :
( or(X3,X4) != X0
| '0' != X1
| ~ eval_succeeds(X3,X2,'0')
| ~ eval_succeeds(X4,X2,'0') ) )
& ( ? [X5,X6] :
( or(X5,X6) = X0
& '0' = X1
& eval_succeeds(X5,X2,'0')
& eval_succeeds(X6,X2,'0') )
| ~ sP10(X0,X1,X2) ) ),
inference(rectify,[],[f425]) ).
fof(f427,plain,
! [X0,X1,X2] :
( ( sP10(X0,X1,X2)
| ! [X3,X4] :
( or(X3,X4) != X0
| '0' != X1
| ~ eval_succeeds(X3,X2,'0')
| ~ eval_succeeds(X4,X2,'0') ) )
& ( ( or(sK105(X0,X1,X2),sK106(X0,X1,X2)) = X0
& '0' = X1
& eval_succeeds(sK105(X0,X1,X2),X2,'0')
& eval_succeeds(sK106(X0,X1,X2),X2,'0') )
| ~ sP10(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK105,sK106]),skolemize(X5,sK105(X0,X1,X2)),skolemize(X6,sK106(X0,X1,X2))],[f426]) ).
fof(f428,plain,
! [X0,X2,X1] :
( ( sP9(X0,X2,X1)
| ! [X13,X14] :
( and(X13,X14) != X0
| '1' != X2
| ~ eval_succeeds(X13,X1,'1')
| ~ eval_succeeds(X14,X1,'1') ) )
& ( ? [X13,X14] :
( X0 = and(X13,X14)
& X2 = '1'
& eval_succeeds(X13,X1,'1')
& eval_succeeds(X14,X1,'1') )
| ~ sP9(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f283]) ).
fof(f429,plain,
! [X0,X1,X2] :
( ( sP9(X0,X1,X2)
| ! [X3,X4] :
( and(X3,X4) != X0
| '1' != X1
| ~ eval_succeeds(X3,X2,'1')
| ~ eval_succeeds(X4,X2,'1') ) )
& ( ? [X5,X6] :
( and(X5,X6) = X0
& '1' = X1
& eval_succeeds(X5,X2,'1')
& eval_succeeds(X6,X2,'1') )
| ~ sP9(X0,X1,X2) ) ),
inference(rectify,[],[f428]) ).
fof(f430,plain,
! [X0,X1,X2] :
( ( sP9(X0,X1,X2)
| ! [X3,X4] :
( and(X3,X4) != X0
| '1' != X1
| ~ eval_succeeds(X3,X2,'1')
| ~ eval_succeeds(X4,X2,'1') ) )
& ( ( and(sK107(X0,X1,X2),sK108(X0,X1,X2)) = X0
& '1' = X1
& eval_succeeds(sK107(X0,X1,X2),X2,'1')
& eval_succeeds(sK108(X0,X1,X2),X2,'1') )
| ~ sP9(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK107,sK108]),skolemize(X5,sK107(X0,X1,X2)),skolemize(X6,sK108(X0,X1,X2))],[f429]) ).
fof(f431,plain,
! [X0,X1,X2] :
( ( eval_succeeds(X0,X1,X2)
| ~ sP18(X1,X2,X0) )
& ( sP18(X1,X2,X0)
| ~ eval_succeeds(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f293]) ).
fof(f631,plain,
! [X0,X1] :
( ( member_succeeds(X0,X1)
| ( ! [X2,X3] :
( cons(X2,X3) != X1
| ~ member_succeeds(X0,X3) )
& ! [X4] : cons(X0,X4) != X1 ) )
& ( ? [X2,X3] :
( X1 = cons(X2,X3)
& member_succeeds(X0,X3) )
| ? [X4] : X1 = cons(X0,X4)
| ~ member_succeeds(X0,X1) ) ),
inference(nnf_transformation,[],[f104]) ).
fof(f632,plain,
! [X0,X1] :
( ( member_succeeds(X0,X1)
| ( ! [X2,X3] :
( cons(X2,X3) != X1
| ~ member_succeeds(X0,X3) )
& ! [X4] : cons(X0,X4) != X1 ) )
& ( ? [X2,X3] :
( X1 = cons(X2,X3)
& member_succeeds(X0,X3) )
| ? [X4] : X1 = cons(X0,X4)
| ~ member_succeeds(X0,X1) ) ),
inference(flattening,[],[f631]) ).
fof(f633,plain,
! [X0,X1] :
( ( member_succeeds(X0,X1)
| ( ! [X2,X3] :
( cons(X2,X3) != X1
| ~ member_succeeds(X0,X3) )
& ! [X4] : cons(X0,X4) != X1 ) )
& ( ? [X5,X6] :
( cons(X5,X6) = X1
& member_succeeds(X0,X6) )
| ? [X7] : cons(X0,X7) = X1
| ~ member_succeeds(X0,X1) ) ),
inference(rectify,[],[f632]) ).
fof(f634,plain,
! [X0,X1] :
( ( member_succeeds(X0,X1)
| ( ! [X2,X3] :
( cons(X2,X3) != X1
| ~ member_succeeds(X0,X3) )
& ! [X4] : cons(X0,X4) != X1 ) )
& ( ( cons(sK228(X0,X1),sK229(X0,X1)) = X1
& member_succeeds(X0,sK229(X0,X1)) )
| cons(X0,sK230(X0,X1)) = X1
| ~ member_succeeds(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK228,sK229,sK230]),skolemize(X5,sK228(X0,X1)),skolemize(X6,sK229(X0,X1)),skolemize(X7,sK230(X0,X1))],[f633]) ).
fof(f653,plain,
! [X0,X1] :
( ( sub(X0,X1)
| ? [X2] :
( ~ member_succeeds(X2,X1)
& member_succeeds(X2,X0) ) )
& ( ! [X2] :
( member_succeeds(X2,X1)
| ~ member_succeeds(X2,X0) )
| ~ sub(X0,X1) ) ),
inference(nnf_transformation,[],[f216]) ).
fof(f654,plain,
! [X0,X1] :
( ( sub(X0,X1)
| ? [X2] :
( ~ member_succeeds(X2,X1)
& member_succeeds(X2,X0) ) )
& ( ! [X3] :
( member_succeeds(X3,X1)
| ~ member_succeeds(X3,X0) )
| ~ sub(X0,X1) ) ),
inference(rectify,[],[f653]) ).
fof(f655,plain,
! [X0,X1] :
( ( sub(X0,X1)
| ( ~ member_succeeds(sK242(X0,X1),X1)
& member_succeeds(sK242(X0,X1),X0) ) )
& ( ! [X3] :
( member_succeeds(X3,X1)
| ~ member_succeeds(X3,X0) )
| ~ sub(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK242]),skolemize(X2,sK242(X0,X1))],[f654]) ).
fof(f657,plain,
! [X0,X2,X1] :
( ? [X28] :
( p(X28) = X0
& X2 = '1'
& member_succeeds(p(X28),X1) )
| ~ sP71(X0,X2,X1) ),
inference(nnf_transformation,[],[f357]) ).
fof(f658,plain,
! [X0,X1,X2] :
( ? [X3] :
( p(X3) = X0
& '1' = X1
& member_succeeds(p(X3),X2) )
| ~ sP71(X0,X1,X2) ),
inference(rectify,[],[f657]) ).
fof(f659,plain,
! [X0,X1,X2] :
( ( p(sK244(X0,X1,X2)) = X0
& '1' = X1
& member_succeeds(p(sK244(X0,X1,X2)),X2) )
| ~ sP71(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK244]),skolemize(X3,sK244(X0,X1,X2))],[f658]) ).
fof(f660,plain,
! [X0,X2,X1] :
( ? [X7,X8] :
( or(X7,X8) = X0
& X2 = '1'
& eval_succeeds(X8,X1,'1')
& ( ! [X9] :
( '1' = X9
| ~ eval_succeeds(X8,X1,X9) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP70(X0,X2,X1) ),
inference(nnf_transformation,[],[f356]) ).
fof(f661,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( or(X3,X4) = X0
& '1' = X1
& eval_succeeds(X4,X2,'1')
& ( ! [X5] :
( '1' = X5
| ~ eval_succeeds(X4,X2,X5) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP70(X0,X1,X2) ),
inference(rectify,[],[f660]) ).
fof(f662,plain,
! [X0,X1,X2] :
( ( or(sK245(X0,X1,X2),sK246(X0,X1,X2)) = X0
& '1' = X1
& eval_succeeds(sK246(X0,X1,X2),X2,'1')
& ( ! [X5] :
( '1' = X5
| ~ eval_succeeds(sK246(X0,X1,X2),X2,X5) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP70(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK245,sK246]),skolemize(X3,sK245(X0,X1,X2)),skolemize(X4,sK246(X0,X1,X2))],[f661]) ).
fof(f663,plain,
! [X0,X2,X1] :
( ? [X10,X11] :
( or(X10,X11) = X0
& X2 = '1'
& eval_succeeds(X10,X1,'1')
& ( ! [X12] :
( '1' = X12
| ~ eval_succeeds(X10,X1,X12) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP69(X0,X2,X1) ),
inference(nnf_transformation,[],[f355]) ).
fof(f664,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( or(X3,X4) = X0
& '1' = X1
& eval_succeeds(X3,X2,'1')
& ( ! [X5] :
( '1' = X5
| ~ eval_succeeds(X3,X2,X5) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP69(X0,X1,X2) ),
inference(rectify,[],[f663]) ).
fof(f665,plain,
! [X0,X1,X2] :
( ( or(sK247(X0,X1,X2),sK248(X0,X1,X2)) = X0
& '1' = X1
& eval_succeeds(sK247(X0,X1,X2),X2,'1')
& ( ! [X5] :
( '1' = X5
| ~ eval_succeeds(sK247(X0,X1,X2),X2,X5) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP69(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK247,sK248]),skolemize(X3,sK247(X0,X1,X2)),skolemize(X4,sK248(X0,X1,X2))],[f664]) ).
fof(f666,plain,
! [X0,X2,X1] :
( ? [X13,X14] :
( and(X13,X14) = X0
& X2 = '0'
& eval_succeeds(X14,X1,'0')
& ( ! [X15] :
( '0' = X15
| ~ eval_succeeds(X14,X1,X15) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP68(X0,X2,X1) ),
inference(nnf_transformation,[],[f354]) ).
fof(f667,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( and(X3,X4) = X0
& '0' = X1
& eval_succeeds(X4,X2,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(X4,X2,X5) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP68(X0,X1,X2) ),
inference(rectify,[],[f666]) ).
fof(f668,plain,
! [X0,X1,X2] :
( ( and(sK249(X0,X1,X2),sK250(X0,X1,X2)) = X0
& '0' = X1
& eval_succeeds(sK250(X0,X1,X2),X2,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(sK250(X0,X1,X2),X2,X5) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP68(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK249,sK250]),skolemize(X3,sK249(X0,X1,X2)),skolemize(X4,sK250(X0,X1,X2))],[f667]) ).
fof(f669,plain,
! [X0,X2,X1] :
( ? [X16,X17] :
( and(X16,X17) = X0
& X2 = '0'
& eval_succeeds(X16,X1,'0')
& ( ! [X18] :
( '0' = X18
| ~ eval_succeeds(X16,X1,X18) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP67(X0,X2,X1) ),
inference(nnf_transformation,[],[f353]) ).
fof(f670,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( and(X3,X4) = X0
& '0' = X1
& eval_succeeds(X3,X2,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(X3,X2,X5) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP67(X0,X1,X2) ),
inference(rectify,[],[f669]) ).
fof(f671,plain,
! [X0,X1,X2] :
( ( and(sK251(X0,X1,X2),sK252(X0,X1,X2)) = X0
& '0' = X1
& eval_succeeds(sK251(X0,X1,X2),X2,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(sK251(X0,X1,X2),X2,X5) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP67(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK251,sK252]),skolemize(X3,sK251(X0,X1,X2)),skolemize(X4,sK252(X0,X1,X2))],[f670]) ).
fof(f672,plain,
! [X0,X2,X1] :
( ? [X23] :
( neg(X23) = X0
& X2 = '0'
& eval_succeeds(X23,X1,'1')
& ( ! [X24] :
( '1' = X24
| ~ eval_succeeds(X23,X1,X24) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP66(X0,X2,X1) ),
inference(nnf_transformation,[],[f352]) ).
fof(f673,plain,
! [X0,X1,X2] :
( ? [X3] :
( neg(X3) = X0
& '0' = X1
& eval_succeeds(X3,X2,'1')
& ( ! [X4] :
( '1' = X4
| ~ eval_succeeds(X3,X2,X4) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP66(X0,X1,X2) ),
inference(rectify,[],[f672]) ).
fof(f674,plain,
! [X0,X1,X2] :
( ( neg(sK253(X0,X1,X2)) = X0
& '0' = X1
& eval_succeeds(sK253(X0,X1,X2),X2,'1')
& ( ! [X4] :
( '1' = X4
| ~ eval_succeeds(sK253(X0,X1,X2),X2,X4) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP66(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK253]),skolemize(X3,sK253(X0,X1,X2))],[f673]) ).
fof(f675,plain,
! [X0,X2,X1] :
( ? [X25] :
( neg(X25) = X0
& X2 = '1'
& eval_succeeds(X25,X1,'0')
& ( ! [X26] :
( '0' = X26
| ~ eval_succeeds(X25,X1,X26) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP65(X0,X2,X1) ),
inference(nnf_transformation,[],[f351]) ).
fof(f676,plain,
! [X0,X1,X2] :
( ? [X3] :
( neg(X3) = X0
& '1' = X1
& eval_succeeds(X3,X2,'0')
& ( ! [X4] :
( '0' = X4
| ~ eval_succeeds(X3,X2,X4) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP65(X0,X1,X2) ),
inference(rectify,[],[f675]) ).
fof(f677,plain,
! [X0,X1,X2] :
( ( neg(sK254(X0,X1,X2)) = X0
& '1' = X1
& eval_succeeds(sK254(X0,X1,X2),X2,'0')
& ( ! [X4] :
( '0' = X4
| ~ eval_succeeds(sK254(X0,X1,X2),X2,X4) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP65(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK254]),skolemize(X3,sK254(X0,X1,X2))],[f676]) ).
fof(f678,plain,
! [X0,X2,X1] :
( ? [X3,X4] :
( X0 = or(X3,X4)
& X2 = '0'
& eval_succeeds(X3,X1,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(X3,X1,X5) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X4,X1,'0')
& ( ! [X6] :
( '0' = X6
| ~ eval_succeeds(X4,X1,X6) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP64(X0,X2,X1) ),
inference(nnf_transformation,[],[f350]) ).
fof(f679,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( X0 = or(X3,X4)
& '0' = X1
& eval_succeeds(X3,X2,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(X3,X2,X5) )
| ~ interpretation_succeeds(X2) )
& eval_succeeds(X4,X2,'0')
& ( ! [X6] :
( '0' = X6
| ~ eval_succeeds(X4,X2,X6) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP64(X0,X1,X2) ),
inference(rectify,[],[f678]) ).
fof(f680,plain,
! [X0,X1,X2] :
( ( or(sK255(X0,X1,X2),sK256(X0,X1,X2)) = X0
& '0' = X1
& eval_succeeds(sK255(X0,X1,X2),X2,'0')
& ( ! [X5] :
( '0' = X5
| ~ eval_succeeds(sK255(X0,X1,X2),X2,X5) )
| ~ interpretation_succeeds(X2) )
& eval_succeeds(sK256(X0,X1,X2),X2,'0')
& ( ! [X6] :
( '0' = X6
| ~ eval_succeeds(sK256(X0,X1,X2),X2,X6) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP64(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK255,sK256]),skolemize(X3,sK255(X0,X1,X2)),skolemize(X4,sK256(X0,X1,X2))],[f679]) ).
fof(f681,plain,
! [X0,X2,X1] :
( ? [X19,X20] :
( and(X19,X20) = X0
& X2 = '1'
& eval_succeeds(X19,X1,'1')
& ( ! [X21] :
( '1' = X21
| ~ eval_succeeds(X19,X1,X21) )
| ~ interpretation_succeeds(X1) )
& eval_succeeds(X20,X1,'1')
& ( ! [X22] :
( '1' = X22
| ~ eval_succeeds(X20,X1,X22) )
| ~ interpretation_succeeds(X1) ) )
| ~ sP63(X0,X2,X1) ),
inference(nnf_transformation,[],[f349]) ).
fof(f682,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( and(X3,X4) = X0
& '1' = X1
& eval_succeeds(X3,X2,'1')
& ( ! [X5] :
( '1' = X5
| ~ eval_succeeds(X3,X2,X5) )
| ~ interpretation_succeeds(X2) )
& eval_succeeds(X4,X2,'1')
& ( ! [X6] :
( '1' = X6
| ~ eval_succeeds(X4,X2,X6) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP63(X0,X1,X2) ),
inference(rectify,[],[f681]) ).
fof(f683,plain,
! [X0,X1,X2] :
( ( and(sK257(X0,X1,X2),sK258(X0,X1,X2)) = X0
& '1' = X1
& eval_succeeds(sK257(X0,X1,X2),X2,'1')
& ( ! [X5] :
( '1' = X5
| ~ eval_succeeds(sK257(X0,X1,X2),X2,X5) )
| ~ interpretation_succeeds(X2) )
& eval_succeeds(sK258(X0,X1,X2),X2,'1')
& ( ! [X6] :
( '1' = X6
| ~ eval_succeeds(sK258(X0,X1,X2),X2,X6) )
| ~ interpretation_succeeds(X2) ) )
| ~ sP63(X0,X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK257,sK258]),skolemize(X3,sK257(X0,X1,X2)),skolemize(X4,sK258(X0,X1,X2))],[f682]) ).
fof(f684,plain,
( ! [X0,X1,X2] :
( ! [X3] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3) )
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2) )
| ? [X4,X5,X6] :
( ? [X7] :
( X6 != X7
& eval_succeeds(X4,X5,X7) )
& interpretation_succeeds(X5)
& ( sP64(X4,X6,X5)
| sP70(X4,X6,X5)
| sP69(X4,X6,X5)
| sP68(X4,X6,X5)
| sP67(X4,X6,X5)
| sP63(X4,X6,X5)
| sP66(X4,X6,X5)
| sP65(X4,X6,X5)
| ? [X8] :
( p(X8) = X4
& '0' = X6
& member_succeeds(neg(p(X8)),X5) )
| sP71(X4,X6,X5) ) ) ),
inference(rectify,[],[f358]) ).
fof(f685,plain,
( ! [X0,X1,X2] :
( ! [X3] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3) )
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2) )
| ( sK261 != sK262
& eval_succeeds(sK259,sK260,sK262)
& interpretation_succeeds(sK260)
& ( sP64(sK259,sK261,sK260)
| sP70(sK259,sK261,sK260)
| sP69(sK259,sK261,sK260)
| sP68(sK259,sK261,sK260)
| sP67(sK259,sK261,sK260)
| sP63(sK259,sK261,sK260)
| sP66(sK259,sK261,sK260)
| sP65(sK259,sK261,sK260)
| ( sK259 = p(sK263)
& '0' = sK261
& member_succeeds(neg(p(sK263)),sK260) )
| sP71(sK259,sK261,sK260) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK259,sK260,sK261,sK262,sK263]),skolemize(X4,sK259),skolemize(X5,sK260),skolemize(X6,sK261),skolemize(X7,sK262),skolemize(X8,sK263)],[f684]) ).
fof(f686,plain,
( sK266 != sK267
& eval_succeeds(sK264,sK265,sK267)
& interpretation_succeeds(sK265)
& eval_succeeds(sK264,sK265,sK266) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK264,sK265,sK266,sK267]),skolemize(X0,sK264),skolemize(X1,sK265),skolemize(X2,sK266),skolemize(X3,sK267)],[f270]) ).
fof(f702,plain,
'1' != '0',
inference(cnf_transformation,[],[f16]) ).
fof(f711,plain,
! [X0,X1] :
( p(X0) != p(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f169]) ).
fof(f712,plain,
! [X0,X1] : p(X0) != neg(X1),
inference(cnf_transformation,[],[f26]) ).
fof(f713,plain,
! [X2,X0,X1] : p(X0) != and(X1,X2),
inference(cnf_transformation,[],[f27]) ).
fof(f714,plain,
! [X2,X0,X1] : p(X0) != or(X1,X2),
inference(cnf_transformation,[],[f28]) ).
fof(f715,plain,
! [X0,X1] :
( neg(X0) != neg(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f170]) ).
fof(f716,plain,
! [X2,X0,X1] : neg(X0) != and(X1,X2),
inference(cnf_transformation,[],[f30]) ).
fof(f717,plain,
! [X2,X0,X1] : neg(X0) != or(X1,X2),
inference(cnf_transformation,[],[f31]) ).
fof(f718,plain,
! [X2,X3,X0,X1] :
( and(X0,X1) != and(X2,X3)
| X1 = X3 ),
inference(cnf_transformation,[],[f171]) ).
fof(f719,plain,
! [X2,X3,X0,X1] :
( and(X0,X1) != and(X2,X3)
| X0 = X2 ),
inference(cnf_transformation,[],[f172]) ).
fof(f720,plain,
! [X2,X3,X0,X1] : and(X0,X1) != or(X2,X3),
inference(cnf_transformation,[],[f34]) ).
fof(f721,plain,
! [X2,X3,X0,X1] :
( or(X0,X1) != or(X2,X3)
| X1 = X3 ),
inference(cnf_transformation,[],[f173]) ).
fof(f722,plain,
! [X2,X3,X0,X1] :
( or(X0,X1) != or(X2,X3)
| X0 = X2 ),
inference(cnf_transformation,[],[f174]) ).
fof(f836,plain,
! [X2,X0,X1] :
( eval_succeeds(sK94(X0,X1,X2),X0,'1')
| sP10(X2,X1,X0)
| sP17(X2,X1,X0)
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP9(X2,X1,X0)
| sP14(X2,X1,X0)
| sP13(X2,X1,X0)
| sP12(X2,X1,X0)
| sP11(X2,X1,X0)
| ~ sP18(X0,X1,X2) ),
inference(cnf_transformation,[],[f403]) ).
fof(f837,plain,
! [X2,X0,X1] :
( sP10(X2,X1,X0)
| '1' = X1
| sP17(X2,X1,X0)
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP9(X2,X1,X0)
| sP14(X2,X1,X0)
| sP13(X2,X1,X0)
| sP12(X2,X1,X0)
| sP11(X2,X1,X0)
| ~ sP18(X0,X1,X2) ),
inference(cnf_transformation,[],[f403]) ).
fof(f838,plain,
! [X2,X0,X1] :
( ~ sP18(X0,X1,X2)
| or(sK93(X0,X1,X2),sK94(X0,X1,X2)) = X2
| sP17(X2,X1,X0)
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP9(X2,X1,X0)
| sP14(X2,X1,X0)
| sP13(X2,X1,X0)
| sP12(X2,X1,X0)
| sP11(X2,X1,X0)
| sP10(X2,X1,X0) ),
inference(cnf_transformation,[],[f403]) ).
fof(f849,plain,
! [X2,X0,X1] :
( eval_succeeds(sK95(X0,X1,X2),X2,'1')
| ~ sP17(X0,X1,X2) ),
inference(cnf_transformation,[],[f406]) ).
fof(f850,plain,
! [X2,X0,X1] :
( ~ sP17(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f406]) ).
fof(f851,plain,
! [X2,X0,X1] :
( ~ sP17(X0,X1,X2)
| or(sK95(X0,X1,X2),sK96(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f406]) ).
fof(f853,plain,
! [X2,X0,X1] :
( eval_succeeds(sK98(X0,X1,X2),X2,'0')
| ~ sP16(X0,X1,X2) ),
inference(cnf_transformation,[],[f409]) ).
fof(f854,plain,
! [X2,X0,X1] :
( ~ sP16(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f409]) ).
fof(f855,plain,
! [X2,X0,X1] :
( ~ sP16(X0,X1,X2)
| and(sK97(X0,X1,X2),sK98(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f409]) ).
fof(f857,plain,
! [X2,X0,X1] :
( eval_succeeds(sK99(X0,X1,X2),X2,'0')
| ~ sP15(X0,X1,X2) ),
inference(cnf_transformation,[],[f412]) ).
fof(f858,plain,
! [X2,X0,X1] :
( ~ sP15(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f412]) ).
fof(f859,plain,
! [X2,X0,X1] :
( ~ sP15(X0,X1,X2)
| and(sK99(X0,X1,X2),sK100(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f412]) ).
fof(f861,plain,
! [X2,X0,X1] :
( eval_succeeds(sK101(X0,X1,X2),X2,'1')
| ~ sP14(X0,X1,X2) ),
inference(cnf_transformation,[],[f415]) ).
fof(f862,plain,
! [X2,X0,X1] :
( ~ sP14(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f415]) ).
fof(f863,plain,
! [X2,X0,X1] :
( ~ sP14(X0,X1,X2)
| neg(sK101(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f415]) ).
fof(f865,plain,
! [X2,X0,X1] :
( eval_succeeds(sK102(X0,X1,X2),X2,'0')
| ~ sP13(X0,X1,X2) ),
inference(cnf_transformation,[],[f418]) ).
fof(f866,plain,
! [X2,X0,X1] :
( ~ sP13(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f418]) ).
fof(f867,plain,
! [X2,X0,X1] :
( ~ sP13(X0,X1,X2)
| neg(sK102(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f418]) ).
fof(f869,plain,
! [X2,X0,X1] :
( member_succeeds(neg(p(sK103(X0,X1,X2))),X2)
| ~ sP12(X0,X1,X2) ),
inference(cnf_transformation,[],[f421]) ).
fof(f870,plain,
! [X2,X0,X1] :
( ~ sP12(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f421]) ).
fof(f871,plain,
! [X2,X0,X1] :
( ~ sP12(X0,X1,X2)
| p(sK103(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f421]) ).
fof(f873,plain,
! [X2,X0,X1] :
( member_succeeds(p(sK104(X0,X1,X2)),X2)
| ~ sP11(X0,X1,X2) ),
inference(cnf_transformation,[],[f424]) ).
fof(f874,plain,
! [X2,X0,X1] :
( ~ sP11(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f424]) ).
fof(f875,plain,
! [X2,X0,X1] :
( ~ sP11(X0,X1,X2)
| p(sK104(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f424]) ).
fof(f876,plain,
! [X2,X3,X0,X1] :
( sP11(X0,X1,X2)
| p(X3) != X0
| '1' != X1
| ~ member_succeeds(p(X3),X2) ),
inference(cnf_transformation,[],[f424]) ).
fof(f877,plain,
! [X2,X0,X1] :
( eval_succeeds(sK106(X0,X1,X2),X2,'0')
| ~ sP10(X0,X1,X2) ),
inference(cnf_transformation,[],[f427]) ).
fof(f878,plain,
! [X2,X0,X1] :
( eval_succeeds(sK105(X0,X1,X2),X2,'0')
| ~ sP10(X0,X1,X2) ),
inference(cnf_transformation,[],[f427]) ).
fof(f879,plain,
! [X2,X0,X1] :
( ~ sP10(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f427]) ).
fof(f880,plain,
! [X2,X0,X1] :
( ~ sP10(X0,X1,X2)
| or(sK105(X0,X1,X2),sK106(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f427]) ).
fof(f882,plain,
! [X2,X0,X1] :
( eval_succeeds(sK108(X0,X1,X2),X2,'1')
| ~ sP9(X0,X1,X2) ),
inference(cnf_transformation,[],[f430]) ).
fof(f883,plain,
! [X2,X0,X1] :
( eval_succeeds(sK107(X0,X1,X2),X2,'1')
| ~ sP9(X0,X1,X2) ),
inference(cnf_transformation,[],[f430]) ).
fof(f884,plain,
! [X2,X0,X1] :
( ~ sP9(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f430]) ).
fof(f885,plain,
! [X2,X0,X1] :
( ~ sP9(X0,X1,X2)
| and(sK107(X0,X1,X2),sK108(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f430]) ).
fof(f887,plain,
! [X2,X0,X1] :
( ~ eval_succeeds(X0,X1,X2)
| sP18(X1,X2,X0) ),
inference(cnf_transformation,[],[f431]) ).
fof(f1245,plain,
! [X0,X1,X4] :
( member_succeeds(X0,X1)
| cons(X0,X4) != X1 ),
inference(cnf_transformation,[],[f634]) ).
fof(f1266,plain,
! [X0,X1] :
( member_succeeds(sK242(X0,X1),X0)
| sub(X0,X1) ),
inference(cnf_transformation,[],[f655]) ).
fof(f1267,plain,
! [X0,X1] :
( ~ member_succeeds(sK242(X0,X1),X1)
| sub(X0,X1) ),
inference(cnf_transformation,[],[f655]) ).
fof(f1276,plain,
! [X0,X1] :
( ~ member_succeeds(neg(p(X1)),X0)
| ~ member_succeeds(p(X1),X0)
| ~ interpretation_succeeds(X0) ),
inference(cnf_transformation,[],[f226]) ).
fof(f1307,plain,
! [X2,X3,X0,X1] :
( ~ eval_succeeds(X0,X1,X3)
| eval_succeeds(X0,X2,X3)
| ~ sub(X1,X2) ),
inference(cnf_transformation,[],[f263]) ).
fof(f1311,plain,
! [X2,X0,X1] :
( member_succeeds(p(sK244(X0,X1,X2)),X2)
| ~ sP71(X0,X1,X2) ),
inference(cnf_transformation,[],[f659]) ).
fof(f1312,plain,
! [X2,X0,X1] :
( ~ sP71(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f659]) ).
fof(f1313,plain,
! [X2,X0,X1] :
( ~ sP71(X0,X1,X2)
| p(sK244(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f659]) ).
fof(f1314,plain,
! [X2,X0,X1,X5] :
( ~ eval_succeeds(sK246(X0,X1,X2),X2,X5)
| '1' = X5
| ~ interpretation_succeeds(X2)
| ~ sP70(X0,X1,X2) ),
inference(cnf_transformation,[],[f662]) ).
fof(f1316,plain,
! [X2,X0,X1] :
( ~ sP70(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f662]) ).
fof(f1317,plain,
! [X2,X0,X1] :
( ~ sP70(X0,X1,X2)
| or(sK245(X0,X1,X2),sK246(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f662]) ).
fof(f1318,plain,
! [X2,X0,X1,X5] :
( ~ eval_succeeds(sK247(X0,X1,X2),X2,X5)
| '1' = X5
| ~ interpretation_succeeds(X2)
| ~ sP69(X0,X1,X2) ),
inference(cnf_transformation,[],[f665]) ).
fof(f1320,plain,
! [X2,X0,X1] :
( ~ sP69(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f665]) ).
fof(f1321,plain,
! [X2,X0,X1] :
( ~ sP69(X0,X1,X2)
| or(sK247(X0,X1,X2),sK248(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f665]) ).
fof(f1322,plain,
! [X2,X0,X1,X5] :
( ~ eval_succeeds(sK250(X0,X1,X2),X2,X5)
| '0' = X5
| ~ interpretation_succeeds(X2)
| ~ sP68(X0,X1,X2) ),
inference(cnf_transformation,[],[f668]) ).
fof(f1324,plain,
! [X2,X0,X1] :
( ~ sP68(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f668]) ).
fof(f1325,plain,
! [X2,X0,X1] :
( ~ sP68(X0,X1,X2)
| and(sK249(X0,X1,X2),sK250(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f668]) ).
fof(f1326,plain,
! [X2,X0,X1,X5] :
( ~ eval_succeeds(sK251(X0,X1,X2),X2,X5)
| '0' = X5
| ~ interpretation_succeeds(X2)
| ~ sP67(X0,X1,X2) ),
inference(cnf_transformation,[],[f671]) ).
fof(f1328,plain,
! [X2,X0,X1] :
( ~ sP67(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f671]) ).
fof(f1329,plain,
! [X2,X0,X1] :
( ~ sP67(X0,X1,X2)
| and(sK251(X0,X1,X2),sK252(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f671]) ).
fof(f1330,plain,
! [X2,X0,X1,X4] :
( ~ eval_succeeds(sK253(X0,X1,X2),X2,X4)
| '1' = X4
| ~ interpretation_succeeds(X2)
| ~ sP66(X0,X1,X2) ),
inference(cnf_transformation,[],[f674]) ).
fof(f1332,plain,
! [X2,X0,X1] :
( ~ sP66(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f674]) ).
fof(f1333,plain,
! [X2,X0,X1] :
( ~ sP66(X0,X1,X2)
| neg(sK253(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f674]) ).
fof(f1334,plain,
! [X2,X0,X1,X4] :
( ~ eval_succeeds(sK254(X0,X1,X2),X2,X4)
| '0' = X4
| ~ interpretation_succeeds(X2)
| ~ sP65(X0,X1,X2) ),
inference(cnf_transformation,[],[f677]) ).
fof(f1336,plain,
! [X2,X0,X1] :
( ~ sP65(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f677]) ).
fof(f1337,plain,
! [X2,X0,X1] :
( ~ sP65(X0,X1,X2)
| neg(sK254(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f677]) ).
fof(f1338,plain,
! [X2,X0,X1,X6] :
( ~ eval_succeeds(sK256(X0,X1,X2),X2,X6)
| '0' = X6
| ~ interpretation_succeeds(X2)
| ~ sP64(X0,X1,X2) ),
inference(cnf_transformation,[],[f680]) ).
fof(f1340,plain,
! [X2,X0,X1,X5] :
( ~ eval_succeeds(sK255(X0,X1,X2),X2,X5)
| '0' = X5
| ~ interpretation_succeeds(X2)
| ~ sP64(X0,X1,X2) ),
inference(cnf_transformation,[],[f680]) ).
fof(f1342,plain,
! [X2,X0,X1] :
( ~ sP64(X0,X1,X2)
| '0' = X1 ),
inference(cnf_transformation,[],[f680]) ).
fof(f1343,plain,
! [X2,X0,X1] :
( ~ sP64(X0,X1,X2)
| or(sK255(X0,X1,X2),sK256(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f680]) ).
fof(f1344,plain,
! [X2,X0,X1,X6] :
( ~ eval_succeeds(sK258(X0,X1,X2),X2,X6)
| '1' = X6
| ~ interpretation_succeeds(X2)
| ~ sP63(X0,X1,X2) ),
inference(cnf_transformation,[],[f683]) ).
fof(f1346,plain,
! [X2,X0,X1,X5] :
( ~ eval_succeeds(sK257(X0,X1,X2),X2,X5)
| '1' = X5
| ~ interpretation_succeeds(X2)
| ~ sP63(X0,X1,X2) ),
inference(cnf_transformation,[],[f683]) ).
fof(f1348,plain,
! [X2,X0,X1] :
( ~ sP63(X0,X1,X2)
| '1' = X1 ),
inference(cnf_transformation,[],[f683]) ).
fof(f1349,plain,
! [X2,X0,X1] :
( ~ sP63(X0,X1,X2)
| and(sK257(X0,X1,X2),sK258(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f683]) ).
fof(f1350,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2)
| sP64(sK259,sK261,sK260)
| sP70(sK259,sK261,sK260)
| sP69(sK259,sK261,sK260)
| sP68(sK259,sK261,sK260)
| sP67(sK259,sK261,sK260)
| sP63(sK259,sK261,sK260)
| sP66(sK259,sK261,sK260)
| sP65(sK259,sK261,sK260)
| member_succeeds(neg(p(sK263)),sK260)
| sP71(sK259,sK261,sK260) ),
inference(cnf_transformation,[],[f685]) ).
fof(f1351,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2)
| sP64(sK259,sK261,sK260)
| sP70(sK259,sK261,sK260)
| sP69(sK259,sK261,sK260)
| sP68(sK259,sK261,sK260)
| sP67(sK259,sK261,sK260)
| sP63(sK259,sK261,sK260)
| sP66(sK259,sK261,sK260)
| sP65(sK259,sK261,sK260)
| '0' = sK261
| sP71(sK259,sK261,sK260) ),
inference(cnf_transformation,[],[f685]) ).
fof(f1352,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2)
| sP64(sK259,sK261,sK260)
| sP70(sK259,sK261,sK260)
| sP69(sK259,sK261,sK260)
| sP68(sK259,sK261,sK260)
| sP67(sK259,sK261,sK260)
| sP63(sK259,sK261,sK260)
| sP66(sK259,sK261,sK260)
| sP65(sK259,sK261,sK260)
| sK259 = p(sK263)
| sP71(sK259,sK261,sK260) ),
inference(cnf_transformation,[],[f685]) ).
fof(f1353,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2)
| interpretation_succeeds(sK260) ),
inference(cnf_transformation,[],[f685]) ).
fof(f1354,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2)
| eval_succeeds(sK259,sK260,sK262) ),
inference(cnf_transformation,[],[f685]) ).
fof(f1355,plain,
! [X2,X3,X0,X1] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X3)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X2)
| sK261 != sK262 ),
inference(cnf_transformation,[],[f685]) ).
fof(f1356,plain,
eval_succeeds(sK264,sK265,sK266),
inference(cnf_transformation,[],[f686]) ).
fof(f1357,plain,
interpretation_succeeds(sK265),
inference(cnf_transformation,[],[f686]) ).
fof(f1358,plain,
eval_succeeds(sK264,sK265,sK267),
inference(cnf_transformation,[],[f686]) ).
fof(f1359,plain,
sK266 != sK267,
inference(cnf_transformation,[],[f686]) ).
fof(f1391,plain,
! [X2,X3,X1] :
( sP11(p(X3),X1,X2)
| '1' != X1
| ~ member_succeeds(p(X3),X2) ),
inference(equality_resolution,[],[f876]) ).
fof(f1392,plain,
! [X2,X3] :
( sP11(p(X3),'1',X2)
| ~ member_succeeds(p(X3),X2) ),
inference(equality_resolution,[],[f1391]) ).
fof(f1511,plain,
! [X0,X4] : member_succeeds(X0,cons(X0,X4)),
inference(equality_resolution,[],[f1245]) ).
fof(f1521,definition,
( spl268_1
<=> sP71(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_1])],[avatar_definition]) ).
fof(f1523,plain,
( sP71(sK259,sK261,sK260)
| ~ spl268_1 ),
inference(avatar_component_clause,[],[f1521]) ).
fof(f1525,definition,
( spl268_2
<=> member_succeeds(neg(p(sK263)),sK260) ),
introduced(definition,[new_symbols(definition,[spl268_2])],[avatar_definition]) ).
fof(f1527,plain,
( member_succeeds(neg(p(sK263)),sK260)
| ~ spl268_2 ),
inference(avatar_component_clause,[],[f1525]) ).
fof(f1529,definition,
( spl268_3
<=> sP65(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_3])],[avatar_definition]) ).
fof(f1531,plain,
( sP65(sK259,sK261,sK260)
| ~ spl268_3 ),
inference(avatar_component_clause,[],[f1529]) ).
fof(f1533,definition,
( spl268_4
<=> sP66(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_4])],[avatar_definition]) ).
fof(f1535,plain,
( sP66(sK259,sK261,sK260)
| ~ spl268_4 ),
inference(avatar_component_clause,[],[f1533]) ).
fof(f1537,definition,
( spl268_5
<=> sP63(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_5])],[avatar_definition]) ).
fof(f1539,plain,
( sP63(sK259,sK261,sK260)
| ~ spl268_5 ),
inference(avatar_component_clause,[],[f1537]) ).
fof(f1541,definition,
( spl268_6
<=> sP67(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_6])],[avatar_definition]) ).
fof(f1543,plain,
( sP67(sK259,sK261,sK260)
| ~ spl268_6 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1545,definition,
( spl268_7
<=> sP68(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_7])],[avatar_definition]) ).
fof(f1547,plain,
( sP68(sK259,sK261,sK260)
| ~ spl268_7 ),
inference(avatar_component_clause,[],[f1545]) ).
fof(f1549,definition,
( spl268_8
<=> sP69(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_8])],[avatar_definition]) ).
fof(f1551,plain,
( sP69(sK259,sK261,sK260)
| ~ spl268_8 ),
inference(avatar_component_clause,[],[f1549]) ).
fof(f1553,definition,
( spl268_9
<=> sP70(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_9])],[avatar_definition]) ).
fof(f1555,plain,
( sP70(sK259,sK261,sK260)
| ~ spl268_9 ),
inference(avatar_component_clause,[],[f1553]) ).
fof(f1557,definition,
( spl268_10
<=> sP64(sK259,sK261,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_10])],[avatar_definition]) ).
fof(f1559,plain,
( sP64(sK259,sK261,sK260)
| ~ spl268_10 ),
inference(avatar_component_clause,[],[f1557]) ).
fof(f1561,definition,
( spl268_11
<=> ! [X0,X3,X2,X1] :
( X2 = X3
| ~ eval_succeeds(X0,X1,X2)
| ~ interpretation_succeeds(X1)
| ~ eval_succeeds(X0,X1,X3) ) ),
introduced(definition,[new_symbols(definition,[spl268_11])],[avatar_definition]) ).
fof(f1562,plain,
( ! [X2,X3,X0,X1] :
( ~ eval_succeeds(X0,X1,X3)
| ~ eval_succeeds(X0,X1,X2)
| ~ interpretation_succeeds(X1)
| X2 = X3 )
| ~ spl268_11 ),
inference(avatar_component_clause,[],[f1561]) ).
fof(f1563,plain,
( spl268_1
| spl268_2
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10
| spl268_11 ),
inference(avatar_split_clause,[],[f1350,f1561,f1557,f1553,f1549,f1545,f1541,f1537,f1533,f1529,f1525,f1521]) ).
fof(f1565,definition,
( spl268_12
<=> '0' = sK261 ),
introduced(definition,[new_symbols(definition,[spl268_12])],[avatar_definition]) ).
fof(f1566,plain,
( '0' != sK261
| spl268_12 ),
inference(avatar_component_clause,[],[f1565]) ).
fof(f1567,plain,
( '0' = sK261
| ~ spl268_12 ),
inference(avatar_component_clause,[],[f1565]) ).
fof(f1568,plain,
( spl268_1
| spl268_12
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10
| spl268_11 ),
inference(avatar_split_clause,[],[f1351,f1561,f1557,f1553,f1549,f1545,f1541,f1537,f1533,f1529,f1565,f1521]) ).
fof(f1570,definition,
( spl268_13
<=> sK259 = p(sK263) ),
introduced(definition,[new_symbols(definition,[spl268_13])],[avatar_definition]) ).
fof(f1572,plain,
( sK259 = p(sK263)
| ~ spl268_13 ),
inference(avatar_component_clause,[],[f1570]) ).
fof(f1573,plain,
( spl268_1
| spl268_13
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10
| spl268_11 ),
inference(avatar_split_clause,[],[f1352,f1561,f1557,f1553,f1549,f1545,f1541,f1537,f1533,f1529,f1570,f1521]) ).
fof(f1575,definition,
( spl268_14
<=> interpretation_succeeds(sK260) ),
introduced(definition,[new_symbols(definition,[spl268_14])],[avatar_definition]) ).
fof(f1577,plain,
( interpretation_succeeds(sK260)
| ~ spl268_14 ),
inference(avatar_component_clause,[],[f1575]) ).
fof(f1578,plain,
( spl268_14
| spl268_11 ),
inference(avatar_split_clause,[],[f1353,f1561,f1575]) ).
fof(f1580,definition,
( spl268_15
<=> eval_succeeds(sK259,sK260,sK262) ),
introduced(definition,[new_symbols(definition,[spl268_15])],[avatar_definition]) ).
fof(f1582,plain,
( eval_succeeds(sK259,sK260,sK262)
| ~ spl268_15 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1583,plain,
( spl268_15
| spl268_11 ),
inference(avatar_split_clause,[],[f1354,f1561,f1580]) ).
fof(f1585,definition,
( spl268_16
<=> sK261 = sK262 ),
introduced(definition,[new_symbols(definition,[spl268_16])],[avatar_definition]) ).
fof(f1587,plain,
( sK261 != sK262
| spl268_16 ),
inference(avatar_component_clause,[],[f1585]) ).
fof(f1588,plain,
( ~ spl268_16
| spl268_11 ),
inference(avatar_split_clause,[],[f1355,f1561,f1585]) ).
fof(f1593,plain,
! [X2,X0,X1] :
( sP10(X2,X1,X0)
| '1' = X1
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP9(X2,X1,X0)
| sP14(X2,X1,X0)
| sP13(X2,X1,X0)
| sP12(X2,X1,X0)
| sP11(X2,X1,X0)
| ~ sP18(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f837,f850]) ).
fof(f1597,plain,
! [X2,X0,X1] :
( sP10(X2,X1,X0)
| '1' = X1
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP14(X2,X1,X0)
| sP13(X2,X1,X0)
| sP12(X2,X1,X0)
| sP11(X2,X1,X0)
| ~ sP18(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1593,f884]) ).
fof(f1600,plain,
! [X2,X0,X1] :
( sP10(X2,X1,X0)
| '1' = X1
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP14(X2,X1,X0)
| sP12(X2,X1,X0)
| sP11(X2,X1,X0)
| ~ sP18(X0,X1,X2) ),
inference(forward_subsumption_resolution,[],[f1597,f866]) ).
fof(f1603,plain,
! [X2,X0,X1] :
( ~ sP18(X0,X1,X2)
| '1' = X1
| sP16(X2,X1,X0)
| sP15(X2,X1,X0)
| sP14(X2,X1,X0)
| sP12(X2,X1,X0)
| sP10(X2,X1,X0) ),
inference(forward_subsumption_resolution,[],[f1600,f874]) ).
fof(f1604,plain,
( ! [X0] :
( ~ eval_succeeds(sK264,sK265,X0)
| ~ interpretation_succeeds(sK265)
| sK267 = X0 )
| ~ spl268_11 ),
inference(resolution,[],[f1562,f1358]) ).
fof(f1607,plain,
( ! [X0] :
( ~ eval_succeeds(sK264,sK265,X0)
| sK267 = X0 )
| ~ spl268_11 ),
inference(forward_subsumption_resolution,[],[f1604,f1357]) ).
fof(f1609,plain,
( sK266 = sK267
| ~ spl268_11 ),
inference(resolution,[],[f1607,f1356]) ).
fof(f1610,plain,
( $false
| ~ spl268_11 ),
inference(forward_subsumption_resolution,[],[f1609,f1359]) ).
fof(f1611,plain,
~ spl268_11,
inference(avatar_contradiction_clause,[],[f1610]) ).
fof(f1614,plain,
( sP18(sK260,sK262,sK259)
| ~ spl268_15 ),
inference(resolution,[],[f887,f1582]) ).
fof(f1623,plain,
( sK259 = neg(sK254(sK259,sK261,sK260))
| ~ spl268_3 ),
inference(resolution,[],[f1337,f1531]) ).
fof(f1626,plain,
( ! [X0,X1] : or(X0,X1) != sK259
| ~ spl268_3 ),
inference(superposition,[],[f717,f1623]) ).
fof(f1632,plain,
( ! [X0] :
( eval_succeeds(sK259,X0,sK262)
| ~ sub(sK260,X0) )
| ~ spl268_15 ),
inference(resolution,[],[f1307,f1582]) ).
fof(f1634,plain,
( ! [X0] :
( sP18(X0,sK262,sK259)
| ~ sub(sK260,X0) )
| ~ spl268_15 ),
inference(resolution,[],[f1632,f887]) ).
fof(f1642,plain,
( '1' = sK261
| ~ spl268_3 ),
inference(resolution,[],[f1336,f1531]) ).
fof(f1644,plain,
( sP65(sK259,'1',sK260)
| ~ spl268_3 ),
inference(superposition,[],[f1531,f1642]) ).
fof(f1662,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| sP16(sK259,sK262,sK260)
| sP15(sK259,sK262,sK260)
| sP9(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| sP13(sK259,sK262,sK260)
| sP12(sK259,sK262,sK260)
| sP11(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15 ),
inference(resolution,[],[f838,f1614]) ).
fof(f1753,definition,
( spl268_37
<=> sP10(sK259,sK262,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_37])],[avatar_definition]) ).
fof(f1754,plain,
( ~ sP10(sK259,sK262,sK260)
| spl268_37 ),
inference(avatar_component_clause,[],[f1753]) ).
fof(f1755,plain,
( sP10(sK259,sK262,sK260)
| ~ spl268_37 ),
inference(avatar_component_clause,[],[f1753]) ).
fof(f1757,definition,
( spl268_38
<=> sP11(sK259,sK262,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_38])],[avatar_definition]) ).
fof(f1758,plain,
( ~ sP11(sK259,sK262,sK260)
| spl268_38 ),
inference(avatar_component_clause,[],[f1757]) ).
fof(f1759,plain,
( sP11(sK259,sK262,sK260)
| ~ spl268_38 ),
inference(avatar_component_clause,[],[f1757]) ).
fof(f1761,definition,
( spl268_39
<=> sP12(sK259,sK262,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_39])],[avatar_definition]) ).
fof(f1762,plain,
( ~ sP12(sK259,sK262,sK260)
| spl268_39 ),
inference(avatar_component_clause,[],[f1761]) ).
fof(f1763,plain,
( sP12(sK259,sK262,sK260)
| ~ spl268_39 ),
inference(avatar_component_clause,[],[f1761]) ).
fof(f1765,definition,
( spl268_40
<=> sP13(sK259,sK262,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_40])],[avatar_definition]) ).
fof(f1766,plain,
( ~ sP13(sK259,sK262,sK260)
| spl268_40 ),
inference(avatar_component_clause,[],[f1765]) ).
fof(f1767,plain,
( sP13(sK259,sK262,sK260)
| ~ spl268_40 ),
inference(avatar_component_clause,[],[f1765]) ).
fof(f1769,definition,
( spl268_41
<=> sP14(sK259,sK262,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_41])],[avatar_definition]) ).
fof(f1770,plain,
( ~ sP14(sK259,sK262,sK260)
| spl268_41 ),
inference(avatar_component_clause,[],[f1769]) ).
fof(f1771,plain,
( sP14(sK259,sK262,sK260)
| ~ spl268_41 ),
inference(avatar_component_clause,[],[f1769]) ).
fof(f1773,definition,
( spl268_42
<=> sP9(sK259,sK262,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_42])],[avatar_definition]) ).
fof(f1774,plain,
( ~ sP9(sK259,sK262,sK260)
| spl268_42 ),
inference(avatar_component_clause,[],[f1773]) ).
fof(f1775,plain,
( sP9(sK259,sK262,sK260)
| ~ spl268_42 ),
inference(avatar_component_clause,[],[f1773]) ).
fof(f1777,definition,
( spl268_43
<=> sP15(sK259,sK262,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_43])],[avatar_definition]) ).
fof(f1778,plain,
( ~ sP15(sK259,sK262,sK260)
| spl268_43 ),
inference(avatar_component_clause,[],[f1777]) ).
fof(f1779,plain,
( sP15(sK259,sK262,sK260)
| ~ spl268_43 ),
inference(avatar_component_clause,[],[f1777]) ).
fof(f1781,definition,
( spl268_44
<=> sP16(sK259,sK262,sK260) ),
introduced(definition,[new_symbols(definition,[spl268_44])],[avatar_definition]) ).
fof(f1782,plain,
( ~ sP16(sK259,sK262,sK260)
| spl268_44 ),
inference(avatar_component_clause,[],[f1781]) ).
fof(f1783,plain,
( sP16(sK259,sK262,sK260)
| ~ spl268_44 ),
inference(avatar_component_clause,[],[f1781]) ).
fof(f1793,plain,
( sK259 = or(sK105(sK259,sK262,sK260),sK106(sK259,sK262,sK260))
| ~ spl268_37 ),
inference(resolution,[],[f1755,f880]) ).
fof(f1795,plain,
( $false
| ~ spl268_3
| ~ spl268_37 ),
inference(forward_subsumption_resolution,[],[f1793,f1626]) ).
fof(f1796,plain,
( ~ spl268_3
| ~ spl268_37 ),
inference(avatar_contradiction_clause,[],[f1795]) ).
fof(f1797,plain,
( '0' = sK261
| ~ spl268_4 ),
inference(resolution,[],[f1535,f1332]) ).
fof(f1799,plain,
( spl268_12
| ~ spl268_4 ),
inference(avatar_split_clause,[],[f1797,f1533,f1565]) ).
fof(f1800,plain,
( '1' = sK261
| ~ spl268_5 ),
inference(resolution,[],[f1539,f1348]) ).
fof(f1801,plain,
( sK259 = and(sK257(sK259,sK261,sK260),sK258(sK259,sK261,sK260))
| ~ spl268_5 ),
inference(resolution,[],[f1539,f1349]) ).
fof(f1802,plain,
( sP63(sK259,'1',sK260)
| ~ spl268_5 ),
inference(superposition,[],[f1539,f1800]) ).
fof(f1803,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_37 ),
inference(superposition,[],[f714,f1793]) ).
fof(f1804,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_37 ),
inference(superposition,[],[f717,f1793]) ).
fof(f1805,plain,
( ! [X0,X1] : and(X0,X1) != sK259
| ~ spl268_37 ),
inference(superposition,[],[f720,f1793]) ).
fof(f1810,plain,
( sK259 = and(sK257(sK259,'1',sK260),sK258(sK259,'1',sK260))
| ~ spl268_5 ),
inference(superposition,[],[f1801,f1800]) ).
fof(f1811,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_5 ),
inference(superposition,[],[f713,f1801]) ).
fof(f1812,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_5 ),
inference(superposition,[],[f716,f1801]) ).
fof(f1818,plain,
( $false
| ~ spl268_5
| ~ spl268_37 ),
inference(forward_subsumption_resolution,[],[f1810,f1805]) ).
fof(f1819,plain,
( ~ spl268_5
| ~ spl268_37 ),
inference(avatar_contradiction_clause,[],[f1818]) ).
fof(f1831,plain,
( sK259 = p(sK103(sK259,sK262,sK260))
| ~ spl268_39 ),
inference(resolution,[],[f1763,f871]) ).
fof(f1833,plain,
( $false
| ~ spl268_5
| ~ spl268_39 ),
inference(forward_subsumption_resolution,[],[f1831,f1811]) ).
fof(f1834,plain,
( ~ spl268_5
| ~ spl268_39 ),
inference(avatar_contradiction_clause,[],[f1833]) ).
fof(f1839,plain,
( sK259 = neg(sK101(sK259,sK262,sK260))
| ~ spl268_41 ),
inference(resolution,[],[f1771,f863]) ).
fof(f1841,plain,
( $false
| ~ spl268_5
| ~ spl268_41 ),
inference(forward_subsumption_resolution,[],[f1839,f1812]) ).
fof(f1842,plain,
( ~ spl268_5
| ~ spl268_41 ),
inference(avatar_contradiction_clause,[],[f1841]) ).
fof(f1843,plain,
( sK259 = and(sK107(sK259,sK262,sK260),sK108(sK259,sK262,sK260))
| ~ spl268_42 ),
inference(resolution,[],[f1775,f885]) ).
fof(f1845,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_42 ),
inference(superposition,[],[f713,f1843]) ).
fof(f1846,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_42 ),
inference(superposition,[],[f716,f1843]) ).
fof(f1964,plain,
( '1' = sK262
| sP16(sK259,sK262,sK260)
| sP15(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| sP12(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15 ),
inference(resolution,[],[f1603,f1614]) ).
fof(f1967,plain,
( ! [X0] :
( '1' = sK262
| sP16(sK259,sK262,X0)
| sP15(sK259,sK262,X0)
| sP14(sK259,sK262,X0)
| sP12(sK259,sK262,X0)
| sP10(sK259,sK262,X0)
| ~ sub(sK260,X0) )
| ~ spl268_15 ),
inference(resolution,[],[f1603,f1634]) ).
fof(f1987,definition,
( spl268_50
<=> ! [X0] :
( sP16(sK259,sK262,X0)
| ~ sub(sK260,X0)
| sP10(sK259,sK262,X0)
| sP12(sK259,sK262,X0)
| sP14(sK259,sK262,X0)
| sP15(sK259,sK262,X0) ) ),
introduced(definition,[new_symbols(definition,[spl268_50])],[avatar_definition]) ).
fof(f1988,plain,
( ! [X0] :
( sP16(sK259,sK262,X0)
| ~ sub(sK260,X0)
| sP10(sK259,sK262,X0)
| sP12(sK259,sK262,X0)
| sP14(sK259,sK262,X0)
| sP15(sK259,sK262,X0) )
| ~ spl268_50 ),
inference(avatar_component_clause,[],[f1987]) ).
fof(f1990,definition,
( spl268_51
<=> '1' = sK262 ),
introduced(definition,[new_symbols(definition,[spl268_51])],[avatar_definition]) ).
fof(f1992,plain,
( '1' = sK262
| ~ spl268_51 ),
inference(avatar_component_clause,[],[f1990]) ).
fof(f1993,plain,
( spl268_50
| spl268_51
| ~ spl268_15 ),
inference(avatar_split_clause,[],[f1967,f1580,f1990,f1987]) ).
fof(f1994,plain,
( '1' = sK262
| sP16(sK259,sK262,sK260)
| sP15(sK259,sK262,sK260)
| sP12(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_41 ),
inference(forward_subsumption_resolution,[],[f1964,f1770]) ).
fof(f1995,plain,
( '1' = sK262
| sP16(sK259,sK262,sK260)
| sP15(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_39
| spl268_41 ),
inference(forward_subsumption_resolution,[],[f1994,f1762]) ).
fof(f1996,plain,
( '1' = sK262
| sP16(sK259,sK262,sK260)
| sP15(sK259,sK262,sK260)
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41 ),
inference(forward_subsumption_resolution,[],[f1995,f1754]) ).
fof(f1997,plain,
( spl268_43
| spl268_44
| spl268_51
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41 ),
inference(avatar_split_clause,[],[f1996,f1769,f1761,f1753,f1580,f1990,f1781,f1777]) ).
fof(f1998,plain,
( sK259 = and(sK99(sK259,sK262,sK260),sK100(sK259,sK262,sK260))
| ~ spl268_43 ),
inference(resolution,[],[f1779,f859]) ).
fof(f2000,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_43 ),
inference(superposition,[],[f713,f1998]) ).
fof(f2001,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_43 ),
inference(superposition,[],[f716,f1998]) ).
fof(f2026,plain,
( ! [X0] :
( sP15(sK259,sK262,X0)
| sP10(sK259,sK262,X0)
| sP12(sK259,sK262,X0)
| sP14(sK259,sK262,X0)
| ~ sub(sK260,X0)
| sK259 = and(sK97(sK259,sK262,X0),sK98(sK259,sK262,X0)) )
| ~ spl268_50 ),
inference(resolution,[],[f1988,f855]) ).
fof(f2096,plain,
( '0' = sK262
| ~ spl268_43 ),
inference(resolution,[],[f858,f1779]) ).
fof(f2106,plain,
( '0' != sK261
| spl268_16
| ~ spl268_43 ),
inference(superposition,[],[f1587,f2096]) ).
fof(f2117,plain,
( sP15(sK259,'0',sK260)
| ~ spl268_43 ),
inference(superposition,[],[f1779,f2096]) ).
fof(f2634,plain,
! [X0,X1] :
( ~ member_succeeds(p(X0),X1)
| p(X0) = p(sK104(p(X0),'1',X1)) ),
inference(resolution,[],[f1392,f875]) ).
fof(f2679,definition,
( spl268_66
<=> '0' = sK262 ),
introduced(definition,[new_symbols(definition,[spl268_66])],[avatar_definition]) ).
fof(f2680,plain,
( '0' != sK262
| spl268_66 ),
inference(avatar_component_clause,[],[f2679]) ).
fof(f2681,plain,
( '0' = sK262
| ~ spl268_66 ),
inference(avatar_component_clause,[],[f2679]) ).
fof(f2688,plain,
( '1' = sK261
| ~ spl268_1 ),
inference(resolution,[],[f1523,f1312]) ).
fof(f2689,plain,
( sK259 = p(sK244(sK259,sK261,sK260))
| ~ spl268_1 ),
inference(resolution,[],[f1523,f1313]) ).
fof(f2690,plain,
( sP71(sK259,'1',sK260)
| ~ spl268_1 ),
inference(superposition,[],[f1523,f2688]) ).
fof(f2694,plain,
( '0' != sK261
| spl268_16
| ~ spl268_66 ),
inference(superposition,[],[f1587,f2681]) ).
fof(f2699,plain,
( ~ sP10(sK259,'0',sK260)
| spl268_37
| ~ spl268_66 ),
inference(superposition,[],[f1754,f2681]) ).
fof(f2706,plain,
( '0' = sK262
| ~ spl268_41 ),
inference(resolution,[],[f1771,f862]) ).
fof(f2707,plain,
( sK259 = neg(sK101(sK259,sK262,sK260))
| ~ spl268_41 ),
inference(resolution,[],[f1771,f863]) ).
fof(f2709,plain,
( sP14(sK259,'0',sK260)
| ~ spl268_41
| ~ spl268_66 ),
inference(superposition,[],[f1771,f2681]) ).
fof(f2710,plain,
( sK259 = neg(sK101(sK259,'0',sK260))
| ~ spl268_41
| ~ spl268_66 ),
inference(forward_demodulation,[],[f2707,f2681]) ).
fof(f2711,plain,
( sK259 = p(sK244(sK259,'1',sK260))
| ~ spl268_1 ),
inference(superposition,[],[f2689,f2688]) ).
fof(f2716,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_1 ),
inference(superposition,[],[f712,f2689]) ).
fof(f2717,plain,
( ! [X0,X1] : and(X0,X1) != sK259
| ~ spl268_1 ),
inference(superposition,[],[f713,f2689]) ).
fof(f2745,plain,
( sK259 != sK259
| ~ spl268_1
| ~ spl268_41
| ~ spl268_66 ),
inference(superposition,[],[f2716,f2710]) ).
fof(f2746,plain,
( $false
| ~ spl268_1
| ~ spl268_41
| ~ spl268_66 ),
inference(trivial_inequality_removal,[],[f2745]) ).
fof(f2747,plain,
( ~ spl268_1
| ~ spl268_41
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f2746]) ).
fof(f2748,plain,
( ~ sP14(sK259,'0',sK260)
| spl268_41
| ~ spl268_66 ),
inference(forward_demodulation,[],[f1770,f2681]) ).
fof(f2750,plain,
( '1' = sK262
| sP16(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| sP12(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_43 ),
inference(forward_subsumption_resolution,[],[f1964,f1778]) ).
fof(f2754,plain,
( '1' = sK262
| sP16(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_39
| spl268_43 ),
inference(forward_subsumption_resolution,[],[f2750,f1762]) ).
fof(f2756,plain,
( '1' = sK262
| sP16(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_43 ),
inference(forward_subsumption_resolution,[],[f2754,f1754]) ).
fof(f2758,plain,
( '1' = '0'
| sP16(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_43
| ~ spl268_66 ),
inference(forward_demodulation,[],[f2756,f2681]) ).
fof(f2760,plain,
( sP16(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_43
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f2758,f702]) ).
fof(f2762,plain,
( sP16(sK259,'0',sK260)
| sP14(sK259,sK262,sK260)
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_43
| ~ spl268_66 ),
inference(forward_demodulation,[],[f2760,f2681]) ).
fof(f2764,plain,
( sP14(sK259,'0',sK260)
| sP16(sK259,'0',sK260)
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_43
| ~ spl268_66 ),
inference(forward_demodulation,[],[f2762,f2681]) ).
fof(f2766,plain,
( sP16(sK259,'0',sK260)
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f2764,f2748]) ).
fof(f2769,plain,
( sP10(sK259,'0',sK260)
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_demodulation,[],[f1755,f2681]) ).
fof(f2784,plain,
( sP10(sK259,sK262,sK260)
| sP12(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| ~ sub(sK260,sK260)
| sK259 = and(sK97(sK259,sK262,sK260),sK98(sK259,sK262,sK260))
| spl268_43
| ~ spl268_50 ),
inference(resolution,[],[f1778,f2026]) ).
fof(f2786,plain,
( sP10(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| ~ sub(sK260,sK260)
| sK259 = and(sK97(sK259,sK262,sK260),sK98(sK259,sK262,sK260))
| spl268_39
| spl268_43
| ~ spl268_50 ),
inference(forward_subsumption_resolution,[],[f2784,f1762]) ).
fof(f2809,plain,
( sK259 != sK259
| ~ spl268_1
| ~ spl268_37 ),
inference(superposition,[],[f1803,f2689]) ).
fof(f2813,plain,
( $false
| ~ spl268_1
| ~ spl268_37 ),
inference(trivial_inequality_removal,[],[f2809]) ).
fof(f2814,plain,
( ~ spl268_1
| ~ spl268_37 ),
inference(avatar_contradiction_clause,[],[f2813]) ).
fof(f2816,plain,
( sP12(sK259,'0',sK260)
| ~ spl268_39
| ~ spl268_66 ),
inference(forward_demodulation,[],[f1763,f2681]) ).
fof(f2834,plain,
( sK259 = p(sK103(sK259,'0',sK260))
| ~ spl268_39
| ~ spl268_66 ),
inference(resolution,[],[f2816,f871]) ).
fof(f2840,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_39
| ~ spl268_66 ),
inference(superposition,[],[f712,f2834]) ).
fof(f2979,plain,
( member_succeeds(sK259,sK260)
| ~ sP71(sK259,'1',sK260)
| ~ spl268_1 ),
inference(superposition,[],[f1311,f2711]) ).
fof(f2980,plain,
( member_succeeds(sK259,sK260)
| ~ spl268_1 ),
inference(forward_subsumption_resolution,[],[f2979,f2690]) ).
fof(f3243,plain,
( member_succeeds(neg(sK259),sK260)
| ~ sP12(sK259,'0',sK260)
| ~ spl268_39
| ~ spl268_66 ),
inference(superposition,[],[f869,f2834]) ).
fof(f3244,plain,
( member_succeeds(neg(sK259),sK260)
| ~ spl268_39
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3243,f2816]) ).
fof(f3369,plain,
! [X0] :
( sub(X0,X0)
| sub(X0,X0) ),
inference(resolution,[],[f1266,f1267]) ).
fof(f3372,plain,
! [X0] : sub(X0,X0),
inference(duplicate_literal_removal,[],[f3369]) ).
fof(f3541,plain,
( ! [X0] :
( ~ member_succeeds(neg(sK259),X0)
| ~ member_succeeds(sK259,X0)
| ~ interpretation_succeeds(X0) )
| ~ spl268_1 ),
inference(superposition,[],[f1276,f2711]) ).
fof(f3554,plain,
( ~ member_succeeds(sK259,sK260)
| ~ interpretation_succeeds(sK260)
| ~ spl268_1
| ~ spl268_39
| ~ spl268_66 ),
inference(resolution,[],[f3541,f3244]) ).
fof(f3559,plain,
( ~ interpretation_succeeds(sK260)
| ~ spl268_1
| ~ spl268_39
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3554,f2980]) ).
fof(f3560,plain,
( $false
| ~ spl268_1
| ~ spl268_14
| ~ spl268_39
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3559,f1577]) ).
fof(f3561,plain,
( ~ spl268_1
| ~ spl268_14
| ~ spl268_39
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f3560]) ).
fof(f3564,plain,
( sP10(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| sK259 = and(sK97(sK259,sK262,sK260),sK98(sK259,sK262,sK260))
| spl268_39
| spl268_43
| ~ spl268_50 ),
inference(forward_subsumption_resolution,[],[f2786,f3372]) ).
fof(f3570,plain,
( sP10(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| ~ spl268_1
| spl268_39
| spl268_43
| ~ spl268_50 ),
inference(forward_subsumption_resolution,[],[f3564,f2717]) ).
fof(f3574,plain,
( sP10(sK259,'0',sK260)
| sP14(sK259,sK262,sK260)
| ~ spl268_1
| spl268_39
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_demodulation,[],[f3570,f2681]) ).
fof(f3579,plain,
( sP14(sK259,sK262,sK260)
| ~ spl268_1
| spl268_37
| spl268_39
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3574,f2699]) ).
fof(f3583,plain,
( sP14(sK259,'0',sK260)
| ~ spl268_1
| spl268_37
| spl268_39
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_demodulation,[],[f3579,f2681]) ).
fof(f3586,plain,
( $false
| ~ spl268_1
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3583,f2748]) ).
fof(f3587,plain,
( ~ spl268_1
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f3586]) ).
fof(f3588,plain,
( ~ spl268_12
| spl268_16
| ~ spl268_66 ),
inference(avatar_split_clause,[],[f2694,f2679,f1585,f1565]) ).
fof(f3592,plain,
( sP10(sK259,'0',sK260)
| sP14(sK259,sK262,sK260)
| sK259 = and(sK97(sK259,sK262,sK260),sK98(sK259,sK262,sK260))
| spl268_39
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_demodulation,[],[f3564,f2681]) ).
fof(f3596,plain,
( sP14(sK259,sK262,sK260)
| sK259 = and(sK97(sK259,sK262,sK260),sK98(sK259,sK262,sK260))
| spl268_37
| spl268_39
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3592,f2699]) ).
fof(f3600,plain,
( sP14(sK259,'0',sK260)
| sK259 = and(sK97(sK259,sK262,sK260),sK98(sK259,sK262,sK260))
| spl268_37
| spl268_39
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_demodulation,[],[f3596,f2681]) ).
fof(f3604,plain,
( sK259 = and(sK97(sK259,sK262,sK260),sK98(sK259,sK262,sK260))
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3600,f2748]) ).
fof(f3608,plain,
( sK259 = and(sK97(sK259,'0',sK260),sK98(sK259,'0',sK260))
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_demodulation,[],[f3604,f2681]) ).
fof(f3614,plain,
( '0' = sK261
| ~ spl268_6 ),
inference(resolution,[],[f1543,f1328]) ).
fof(f3618,plain,
( '0' = sK261
| ~ spl268_7 ),
inference(resolution,[],[f1547,f1324]) ).
fof(f3620,plain,
( $false
| ~ spl268_7
| spl268_12 ),
inference(forward_subsumption_resolution,[],[f3618,f1566]) ).
fof(f3621,plain,
( ~ spl268_7
| spl268_12 ),
inference(avatar_contradiction_clause,[],[f3620]) ).
fof(f3624,plain,
( sK259 = neg(sK254(sK259,sK261,sK260))
| ~ spl268_3 ),
inference(resolution,[],[f1531,f1337]) ).
fof(f3625,plain,
( sK259 = neg(sK254(sK259,'1',sK260))
| ~ spl268_3 ),
inference(forward_demodulation,[],[f3624,f1642]) ).
fof(f3638,plain,
( ! [X0,X1] : and(X0,X1) != sK259
| ~ spl268_3 ),
inference(superposition,[],[f716,f3625]) ).
fof(f3667,plain,
( ! [X0,X1] : or(X0,X1) != sK259
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(superposition,[],[f720,f3608]) ).
fof(f3675,plain,
( sK259 != sK259
| ~ spl268_3
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(superposition,[],[f3638,f3608]) ).
fof(f3676,plain,
( $false
| ~ spl268_3
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(trivial_inequality_removal,[],[f3675]) ).
fof(f3677,plain,
( ~ spl268_3
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f3676]) ).
fof(f3678,plain,
( '0' = sK261
| ~ spl268_10 ),
inference(resolution,[],[f1559,f1342]) ).
fof(f3682,plain,
( $false
| ~ spl268_10
| spl268_12 ),
inference(forward_subsumption_resolution,[],[f3678,f1566]) ).
fof(f3683,plain,
( ~ spl268_10
| spl268_12 ),
inference(avatar_contradiction_clause,[],[f3682]) ).
fof(f3684,plain,
( '1' = sK261
| ~ spl268_8 ),
inference(resolution,[],[f1551,f1320]) ).
fof(f3685,plain,
( sK259 = or(sK247(sK259,sK261,sK260),sK248(sK259,sK261,sK260))
| ~ spl268_8 ),
inference(resolution,[],[f1551,f1321]) ).
fof(f3686,plain,
( $false
| ~ spl268_8
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3685,f3667]) ).
fof(f3687,plain,
( ~ spl268_8
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f3686]) ).
fof(f3688,plain,
( '1' = sK261
| ~ spl268_9 ),
inference(resolution,[],[f1555,f1316]) ).
fof(f3689,plain,
( sK259 = or(sK245(sK259,sK261,sK260),sK246(sK259,sK261,sK260))
| ~ spl268_9 ),
inference(resolution,[],[f1555,f1317]) ).
fof(f3690,plain,
( $false
| ~ spl268_9
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3689,f3667]) ).
fof(f3691,plain,
( ~ spl268_9
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f3690]) ).
fof(f3694,plain,
( sK259 = and(sK257(sK259,sK261,sK260),sK258(sK259,sK261,sK260))
| ~ spl268_5 ),
inference(resolution,[],[f1539,f1349]) ).
fof(f3695,plain,
( sK259 = and(sK257(sK259,'1',sK260),sK258(sK259,'1',sK260))
| ~ spl268_5 ),
inference(forward_demodulation,[],[f3694,f1800]) ).
fof(f3707,plain,
( ! [X0,X1] :
( and(X0,X1) != sK259
| sK258(sK259,'1',sK260) = X1 )
| ~ spl268_5 ),
inference(superposition,[],[f718,f3695]) ).
fof(f3709,plain,
( ! [X0,X1] :
( and(X0,X1) != sK259
| sK257(sK259,'1',sK260) = X0 )
| ~ spl268_5 ),
inference(superposition,[],[f719,f3695]) ).
fof(f3721,plain,
( sK259 != sK259
| sK258(sK259,'1',sK260) = sK98(sK259,'0',sK260)
| ~ spl268_5
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(superposition,[],[f3707,f3608]) ).
fof(f3722,plain,
( sK258(sK259,'1',sK260) = sK98(sK259,'0',sK260)
| ~ spl268_5
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(trivial_inequality_removal,[],[f3721]) ).
fof(f3846,plain,
( eval_succeeds(sK258(sK259,'1',sK260),sK260,'0')
| ~ sP16(sK259,'0',sK260)
| ~ spl268_5
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(superposition,[],[f853,f3722]) ).
fof(f3847,plain,
( eval_succeeds(sK258(sK259,'1',sK260),sK260,'0')
| ~ spl268_5
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3846,f2766]) ).
fof(f3848,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP63(sK259,'1',sK260)
| ~ spl268_5
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(resolution,[],[f3847,f1344]) ).
fof(f3851,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP63(sK259,'1',sK260)
| ~ spl268_5
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3848,f702]) ).
fof(f3852,plain,
( ~ sP63(sK259,'1',sK260)
| ~ spl268_5
| ~ spl268_14
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3851,f1577]) ).
fof(f3853,plain,
( $false
| ~ spl268_5
| ~ spl268_14
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f3852,f1802]) ).
fof(f3854,plain,
( ~ spl268_5
| ~ spl268_14
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f3853]) ).
fof(f3924,plain,
( sK259 = and(sK99(sK259,'0',sK260),sK100(sK259,'0',sK260))
| ~ spl268_43 ),
inference(resolution,[],[f2117,f859]) ).
fof(f3941,plain,
( ! [X0,X1] : or(X0,X1) != sK259
| ~ spl268_43 ),
inference(superposition,[],[f720,f3924]) ).
fof(f3952,plain,
( sK259 != sK259
| sK257(sK259,'1',sK260) = sK99(sK259,'0',sK260)
| ~ spl268_5
| ~ spl268_43 ),
inference(superposition,[],[f3709,f3924]) ).
fof(f3953,plain,
( sK257(sK259,'1',sK260) = sK99(sK259,'0',sK260)
| ~ spl268_5
| ~ spl268_43 ),
inference(trivial_inequality_removal,[],[f3952]) ).
fof(f3967,plain,
( eval_succeeds(sK257(sK259,'1',sK260),sK260,'0')
| ~ sP15(sK259,'0',sK260)
| ~ spl268_5
| ~ spl268_43 ),
inference(superposition,[],[f857,f3953]) ).
fof(f3968,plain,
( eval_succeeds(sK257(sK259,'1',sK260),sK260,'0')
| ~ spl268_5
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f3967,f2117]) ).
fof(f3975,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP63(sK259,'1',sK260)
| ~ spl268_5
| ~ spl268_43 ),
inference(resolution,[],[f3968,f1346]) ).
fof(f3978,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP63(sK259,'1',sK260)
| ~ spl268_5
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f3975,f702]) ).
fof(f3979,plain,
( ~ sP63(sK259,'1',sK260)
| ~ spl268_5
| ~ spl268_14
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f3978,f1577]) ).
fof(f3980,plain,
( $false
| ~ spl268_5
| ~ spl268_14
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f3979,f1802]) ).
fof(f3981,plain,
( ~ spl268_5
| ~ spl268_14
| ~ spl268_43 ),
inference(avatar_contradiction_clause,[],[f3980]) ).
fof(f3990,plain,
( sK259 = or(sK245(sK259,sK261,sK260),sK246(sK259,sK261,sK260))
| ~ spl268_9 ),
inference(resolution,[],[f1555,f1317]) ).
fof(f3991,plain,
( $false
| ~ spl268_9
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f3990,f3941]) ).
fof(f3992,plain,
( ~ spl268_9
| ~ spl268_43 ),
inference(avatar_contradiction_clause,[],[f3991]) ).
fof(f3995,plain,
( sK259 = neg(sK254(sK259,sK261,sK260))
| ~ spl268_3 ),
inference(resolution,[],[f1531,f1337]) ).
fof(f3996,plain,
( $false
| ~ spl268_3
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f3995,f2001]) ).
fof(f3997,plain,
( ~ spl268_3
| ~ spl268_43 ),
inference(avatar_contradiction_clause,[],[f3996]) ).
fof(f4000,plain,
( sK259 = or(sK247(sK259,sK261,sK260),sK248(sK259,sK261,sK260))
| ~ spl268_8 ),
inference(resolution,[],[f1551,f1321]) ).
fof(f4001,plain,
( $false
| ~ spl268_8
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f4000,f3941]) ).
fof(f4002,plain,
( ~ spl268_8
| ~ spl268_43 ),
inference(avatar_contradiction_clause,[],[f4001]) ).
fof(f4011,plain,
( sK259 = p(sK244(sK259,sK261,sK260))
| ~ spl268_1 ),
inference(resolution,[],[f1523,f1313]) ).
fof(f4012,plain,
( $false
| ~ spl268_1
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f4011,f2000]) ).
fof(f4013,plain,
( ~ spl268_1
| ~ spl268_43 ),
inference(avatar_contradiction_clause,[],[f4012]) ).
fof(f4014,plain,
( $false
| ~ spl268_13
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f1572,f2000]) ).
fof(f4015,plain,
( ~ spl268_13
| ~ spl268_43 ),
inference(avatar_contradiction_clause,[],[f4014]) ).
fof(f4018,plain,
( $false
| ~ spl268_12
| spl268_16
| ~ spl268_43 ),
inference(forward_subsumption_resolution,[],[f2106,f1567]) ).
fof(f4019,plain,
( ~ spl268_12
| spl268_16
| ~ spl268_43 ),
inference(avatar_contradiction_clause,[],[f4018]) ).
fof(f4031,plain,
( '0' = sK262
| ~ spl268_44 ),
inference(resolution,[],[f1783,f854]) ).
fof(f4034,plain,
( $false
| ~ spl268_44
| spl268_66 ),
inference(forward_subsumption_resolution,[],[f4031,f2680]) ).
fof(f4035,plain,
( ~ spl268_44
| spl268_66 ),
inference(avatar_contradiction_clause,[],[f4034]) ).
fof(f4045,definition,
( spl268_95
<=> sK259 = or(sK93(sK260,'1',sK259),sK94(sK260,'1',sK259)) ),
introduced(definition,[new_symbols(definition,[spl268_95])],[avatar_definition]) ).
fof(f4046,plain,
( sK259 != or(sK93(sK260,'1',sK259),sK94(sK260,'1',sK259))
| spl268_95 ),
inference(avatar_component_clause,[],[f4045]) ).
fof(f4047,plain,
( sK259 = or(sK93(sK260,'1',sK259),sK94(sK260,'1',sK259))
| ~ spl268_95 ),
inference(avatar_component_clause,[],[f4045]) ).
fof(f4049,definition,
( spl268_96
<=> sP17(sK259,'1',sK260) ),
introduced(definition,[new_symbols(definition,[spl268_96])],[avatar_definition]) ).
fof(f4050,plain,
( ~ sP17(sK259,'1',sK260)
| spl268_96 ),
inference(avatar_component_clause,[],[f4049]) ).
fof(f4051,plain,
( sP17(sK259,'1',sK260)
| ~ spl268_96 ),
inference(avatar_component_clause,[],[f4049]) ).
fof(f4053,plain,
( sP11(sK259,'1',sK260)
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_demodulation,[],[f1759,f1992]) ).
fof(f4058,plain,
( ~ member_succeeds(p(sK263),sK260)
| ~ interpretation_succeeds(sK260)
| ~ spl268_2 ),
inference(resolution,[],[f1527,f1276]) ).
fof(f4061,plain,
( ~ member_succeeds(p(sK263),sK260)
| ~ spl268_2
| ~ spl268_14 ),
inference(forward_subsumption_resolution,[],[f4058,f1577]) ).
fof(f4063,plain,
( ~ member_succeeds(sK259,sK260)
| ~ spl268_2
| ~ spl268_13
| ~ spl268_14 ),
inference(forward_demodulation,[],[f4061,f1572]) ).
fof(f4106,plain,
( ! [X0] :
( p(X0) != sK259
| sK263 = X0 )
| ~ spl268_13 ),
inference(superposition,[],[f711,f1572]) ).
fof(f4111,plain,
( ! [X0] :
( ~ member_succeeds(sK259,X0)
| sK259 = p(sK104(sK259,'1',X0)) )
| ~ spl268_13 ),
inference(superposition,[],[f2634,f1572]) ).
fof(f4123,plain,
( ! [X0] : ~ member_succeeds(sK259,X0)
| ~ spl268_13
| ~ spl268_37 ),
inference(forward_subsumption_resolution,[],[f4111,f1803]) ).
fof(f4131,plain,
( '1' != sK261
| spl268_16
| ~ spl268_51 ),
inference(superposition,[],[f1587,f1992]) ).
fof(f4132,plain,
( sP18(sK260,'1',sK259)
| ~ spl268_15
| ~ spl268_51 ),
inference(superposition,[],[f1614,f1992]) ).
fof(f4136,plain,
( ~ sP13(sK259,'1',sK260)
| spl268_40
| ~ spl268_51 ),
inference(superposition,[],[f1766,f1992]) ).
fof(f4137,plain,
( ~ sP9(sK259,'1',sK260)
| spl268_42
| ~ spl268_51 ),
inference(superposition,[],[f1774,f1992]) ).
fof(f4138,plain,
( ~ sP15(sK259,'1',sK260)
| spl268_43
| ~ spl268_51 ),
inference(superposition,[],[f1778,f1992]) ).
fof(f4139,plain,
( ~ sP16(sK259,'1',sK260)
| spl268_44
| ~ spl268_51 ),
inference(superposition,[],[f1782,f1992]) ).
fof(f4145,plain,
( ~ sP14(sK259,'1',sK260)
| spl268_41
| ~ spl268_51 ),
inference(superposition,[],[f1770,f1992]) ).
fof(f4146,plain,
( ~ sP12(sK259,'1',sK260)
| spl268_39
| ~ spl268_51 ),
inference(superposition,[],[f1762,f1992]) ).
fof(f4148,plain,
( $false
| ~ spl268_13
| ~ spl268_37 ),
inference(resolution,[],[f4123,f1511]) ).
fof(f4149,plain,
( ~ spl268_13
| ~ spl268_37 ),
inference(avatar_contradiction_clause,[],[f4148]) ).
fof(f4150,plain,
( ~ sP10(sK259,'1',sK260)
| spl268_37
| ~ spl268_51 ),
inference(forward_demodulation,[],[f1754,f1992]) ).
fof(f4181,plain,
( '0' = sK262
| ~ spl268_39 ),
inference(resolution,[],[f1763,f870]) ).
fof(f4194,plain,
( $false
| ~ spl268_41
| spl268_66 ),
inference(forward_subsumption_resolution,[],[f2706,f2680]) ).
fof(f4195,plain,
( ~ spl268_41
| spl268_66 ),
inference(avatar_contradiction_clause,[],[f4194]) ).
fof(f4199,plain,
( sK259 = p(sK104(sK259,sK262,sK260))
| ~ spl268_38 ),
inference(resolution,[],[f1759,f875]) ).
fof(f4201,plain,
( sK259 = p(sK104(sK259,'1',sK260))
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_demodulation,[],[f4199,f1992]) ).
fof(f4203,plain,
( '1' != sK261
| spl268_16
| ~ spl268_51 ),
inference(superposition,[],[f1587,f1992]) ).
fof(f4237,plain,
( sK259 != sK259
| sK263 = sK104(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_38
| ~ spl268_51 ),
inference(superposition,[],[f4106,f4201]) ).
fof(f4238,plain,
( sK263 = sK104(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_38
| ~ spl268_51 ),
inference(trivial_inequality_removal,[],[f4237]) ).
fof(f4247,plain,
( sK259 = or(sK93(sK260,'1',sK259),sK94(sK260,'1',sK259))
| sP17(sK259,'1',sK260)
| sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_15
| ~ spl268_51 ),
inference(resolution,[],[f4132,f838]) ).
fof(f4257,plain,
( ! [X0] : sK259 = p(sK104(sK259,'1',cons(sK259,X0)))
| ~ spl268_13 ),
inference(resolution,[],[f4111,f1511]) ).
fof(f4369,plain,
( ! [X1] : neg(X1) != sK259
| ~ spl268_13 ),
inference(superposition,[],[f712,f4257]) ).
fof(f4371,plain,
( ! [X2,X1] : or(X1,X2) != sK259
| ~ spl268_13 ),
inference(superposition,[],[f714,f4257]) ).
fof(f4479,plain,
( member_succeeds(p(sK263),sK260)
| ~ sP11(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_38
| ~ spl268_51 ),
inference(superposition,[],[f873,f4238]) ).
fof(f4487,plain,
( member_succeeds(p(sK263),sK260)
| ~ spl268_13
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4479,f4053]) ).
fof(f4493,plain,
( member_succeeds(sK259,sK260)
| ~ spl268_13
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_demodulation,[],[f4487,f1572]) ).
fof(f4495,plain,
( $false
| ~ spl268_2
| ~ spl268_13
| ~ spl268_14
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4493,f4063]) ).
fof(f4496,plain,
( ~ spl268_2
| ~ spl268_13
| ~ spl268_14
| ~ spl268_38
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f4495]) ).
fof(f4502,plain,
( ~ sP11(sK259,'1',sK260)
| spl268_38
| ~ spl268_51 ),
inference(forward_demodulation,[],[f1758,f1992]) ).
fof(f4580,plain,
( sK259 = or(sK95(sK259,'1',sK260),sK96(sK259,'1',sK260))
| ~ spl268_96 ),
inference(resolution,[],[f4051,f851]) ).
fof(f4582,plain,
( $false
| ~ spl268_13
| ~ spl268_96 ),
inference(forward_subsumption_resolution,[],[f4580,f4371]) ).
fof(f4583,plain,
( ~ spl268_13
| ~ spl268_96 ),
inference(avatar_contradiction_clause,[],[f4582]) ).
fof(f4584,plain,
( sP13(sK259,'1',sK260)
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_demodulation,[],[f1767,f1992]) ).
fof(f4585,plain,
( sP17(sK259,'1',sK260)
| sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4247,f4371]) ).
fof(f4599,plain,
( sK259 = neg(sK102(sK259,'1',sK260))
| ~ spl268_40
| ~ spl268_51 ),
inference(resolution,[],[f4584,f867]) ).
fof(f4601,plain,
( $false
| ~ spl268_13
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4599,f4369]) ).
fof(f4602,plain,
( ~ spl268_13
| ~ spl268_40
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f4601]) ).
fof(f4606,plain,
( sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4585,f4050]) ).
fof(f4608,plain,
( sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4606,f4139]) ).
fof(f4610,plain,
( sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4608,f4138]) ).
fof(f4613,plain,
( sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4610,f4137]) ).
fof(f4614,plain,
( sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4613,f4145]) ).
fof(f4615,plain,
( sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4614,f4136]) ).
fof(f4616,plain,
( sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4615,f4146]) ).
fof(f4617,plain,
( sP10(sK259,'1',sK260)
| ~ spl268_13
| ~ spl268_15
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4616,f4502]) ).
fof(f4618,plain,
( $false
| ~ spl268_13
| ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f4617,f4150]) ).
fof(f4619,plain,
( ~ spl268_13
| ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(avatar_contradiction_clause,[],[f4618]) ).
fof(f4620,plain,
( sP9(sK259,'1',sK260)
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_demodulation,[],[f1775,f1992]) ).
fof(f4631,plain,
( sK259 != sK259
| ~ spl268_13
| ~ spl268_42 ),
inference(superposition,[],[f1845,f1572]) ).
fof(f4635,plain,
( $false
| ~ spl268_13
| ~ spl268_42 ),
inference(trivial_inequality_removal,[],[f4631]) ).
fof(f4636,plain,
( ~ spl268_13
| ~ spl268_42 ),
inference(avatar_contradiction_clause,[],[f4635]) ).
fof(f4637,plain,
( sP66(sK259,'0',sK260)
| ~ spl268_4
| ~ spl268_12 ),
inference(forward_demodulation,[],[f1535,f1567]) ).
fof(f4656,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| sP15(sK259,sK262,sK260)
| sP9(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| sP13(sK259,sK262,sK260)
| sP12(sK259,sK262,sK260)
| sP11(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_44 ),
inference(forward_subsumption_resolution,[],[f1662,f1782]) ).
fof(f4657,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| sP9(sK259,sK262,sK260)
| sP14(sK259,sK262,sK260)
| sP13(sK259,sK262,sK260)
| sP12(sK259,sK262,sK260)
| sP11(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_43
| spl268_44 ),
inference(forward_subsumption_resolution,[],[f4656,f1778]) ).
fof(f4658,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| sP9(sK259,sK262,sK260)
| sP13(sK259,sK262,sK260)
| sP12(sK259,sK262,sK260)
| sP11(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_41
| spl268_43
| spl268_44 ),
inference(forward_subsumption_resolution,[],[f4657,f1770]) ).
fof(f4659,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| sP9(sK259,sK262,sK260)
| sP13(sK259,sK262,sK260)
| sP11(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_39
| spl268_41
| spl268_43
| spl268_44 ),
inference(forward_subsumption_resolution,[],[f4658,f1762]) ).
fof(f4663,plain,
( sK259 = neg(sK253(sK259,'0',sK260))
| ~ spl268_4
| ~ spl268_12 ),
inference(resolution,[],[f4637,f1333]) ).
fof(f4668,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_4
| ~ spl268_12 ),
inference(superposition,[],[f712,f4663]) ).
fof(f4670,plain,
( ! [X0] :
( neg(X0) != sK259
| sK253(sK259,'0',sK260) = X0 )
| ~ spl268_4
| ~ spl268_12 ),
inference(superposition,[],[f715,f4663]) ).
fof(f4672,plain,
( ! [X0,X1] : or(X0,X1) != sK259
| ~ spl268_4
| ~ spl268_12 ),
inference(superposition,[],[f717,f4663]) ).
fof(f4690,plain,
( ! [X0,X1] : and(X0,X1) != sK259
| ~ spl268_95 ),
inference(superposition,[],[f720,f4047]) ).
fof(f4705,plain,
( sK259 != sK259
| ~ spl268_4
| ~ spl268_12
| ~ spl268_95 ),
inference(superposition,[],[f4672,f4047]) ).
fof(f4706,plain,
( $false
| ~ spl268_4
| ~ spl268_12
| ~ spl268_95 ),
inference(trivial_inequality_removal,[],[f4705]) ).
fof(f4707,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_95 ),
inference(avatar_contradiction_clause,[],[f4706]) ).
fof(f4711,plain,
( sK259 = or(sK95(sK259,'1',sK260),sK96(sK259,'1',sK260))
| ~ spl268_96 ),
inference(resolution,[],[f4051,f851]) ).
fof(f4713,plain,
( $false
| ~ spl268_4
| ~ spl268_12
| ~ spl268_96 ),
inference(forward_subsumption_resolution,[],[f4711,f4672]) ).
fof(f4714,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_96 ),
inference(avatar_contradiction_clause,[],[f4713]) ).
fof(f4720,plain,
( sK259 = neg(sK102(sK259,'1',sK260))
| ~ spl268_40
| ~ spl268_51 ),
inference(resolution,[],[f4584,f867]) ).
fof(f4741,plain,
( sK259 != sK259
| sK102(sK259,'1',sK260) = sK253(sK259,'0',sK260)
| ~ spl268_4
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(superposition,[],[f4670,f4720]) ).
fof(f4742,plain,
( sK102(sK259,'1',sK260) = sK253(sK259,'0',sK260)
| ~ spl268_4
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(trivial_inequality_removal,[],[f4741]) ).
fof(f4755,plain,
( eval_succeeds(sK253(sK259,'0',sK260),sK260,'0')
| ~ sP13(sK259,'1',sK260)
| ~ spl268_4
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(superposition,[],[f865,f4742]) ).
fof(f4756,plain,
( eval_succeeds(sK253(sK259,'0',sK260),sK260,'0')
| ~ spl268_4
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4755,f4584]) ).
fof(f4758,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP66(sK259,'0',sK260)
| ~ spl268_4
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(resolution,[],[f4756,f1330]) ).
fof(f4761,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP66(sK259,'0',sK260)
| ~ spl268_4
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4758,f702]) ).
fof(f4762,plain,
( ~ sP66(sK259,'0',sK260)
| ~ spl268_4
| ~ spl268_12
| ~ spl268_14
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4761,f1577]) ).
fof(f4763,plain,
( $false
| ~ spl268_4
| ~ spl268_12
| ~ spl268_14
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4762,f4637]) ).
fof(f4764,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_14
| ~ spl268_40
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f4763]) ).
fof(f4770,plain,
( sK259 = p(sK104(sK259,'1',sK260))
| ~ spl268_38
| ~ spl268_51 ),
inference(resolution,[],[f4053,f875]) ).
fof(f4772,plain,
( $false
| ~ spl268_4
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4770,f4668]) ).
fof(f4773,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f4772]) ).
fof(f4776,plain,
( sK259 != sK259
| ~ spl268_4
| ~ spl268_12
| ~ spl268_42 ),
inference(superposition,[],[f1846,f4663]) ).
fof(f4777,plain,
( $false
| ~ spl268_4
| ~ spl268_12
| ~ spl268_42 ),
inference(trivial_inequality_removal,[],[f4776]) ).
fof(f4778,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_42 ),
inference(avatar_contradiction_clause,[],[f4777]) ).
fof(f4791,plain,
( sK259 != sK259
| ~ spl268_4
| ~ spl268_12
| ~ spl268_37 ),
inference(superposition,[],[f1804,f4663]) ).
fof(f4792,plain,
( $false
| ~ spl268_4
| ~ spl268_12
| ~ spl268_37 ),
inference(trivial_inequality_removal,[],[f4791]) ).
fof(f4793,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_37 ),
inference(avatar_contradiction_clause,[],[f4792]) ).
fof(f4815,plain,
( sP68(sK259,'0',sK260)
| ~ spl268_7
| ~ spl268_12 ),
inference(forward_demodulation,[],[f1547,f1567]) ).
fof(f4818,plain,
( sK259 = and(sK249(sK259,'0',sK260),sK250(sK259,'0',sK260))
| ~ spl268_7
| ~ spl268_12 ),
inference(resolution,[],[f4815,f1325]) ).
fof(f4823,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_7
| ~ spl268_12 ),
inference(superposition,[],[f713,f4818]) ).
fof(f4824,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_7
| ~ spl268_12 ),
inference(superposition,[],[f716,f4818]) ).
fof(f4829,plain,
( ! [X0,X1] : or(X0,X1) != sK259
| ~ spl268_7
| ~ spl268_12 ),
inference(superposition,[],[f720,f4818]) ).
fof(f4852,plain,
( '0' = sK262
| ~ spl268_37 ),
inference(resolution,[],[f1755,f879]) ).
fof(f4853,plain,
( sK259 = or(sK105(sK259,sK262,sK260),sK106(sK259,sK262,sK260))
| ~ spl268_37 ),
inference(resolution,[],[f1755,f880]) ).
fof(f4855,plain,
( $false
| ~ spl268_7
| ~ spl268_12
| ~ spl268_37 ),
inference(forward_subsumption_resolution,[],[f4853,f4829]) ).
fof(f4856,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_37 ),
inference(avatar_contradiction_clause,[],[f4855]) ).
fof(f4857,plain,
( $false
| ~ spl268_37
| spl268_66 ),
inference(forward_subsumption_resolution,[],[f4852,f2680]) ).
fof(f4858,plain,
( ~ spl268_37
| spl268_66 ),
inference(avatar_contradiction_clause,[],[f4857]) ).
fof(f4863,plain,
( sK259 = or(sK105(sK259,'0',sK260),sK106(sK259,'0',sK260))
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_demodulation,[],[f4853,f2681]) ).
fof(f4865,plain,
( sK259 = or(sK247(sK259,sK261,sK260),sK248(sK259,sK261,sK260))
| ~ spl268_8 ),
inference(resolution,[],[f1551,f1321]) ).
fof(f4866,plain,
( sK259 = or(sK247(sK259,'1',sK260),sK248(sK259,'1',sK260))
| ~ spl268_8 ),
inference(forward_demodulation,[],[f4865,f3684]) ).
fof(f4871,plain,
( sP69(sK259,'1',sK260)
| ~ spl268_8 ),
inference(superposition,[],[f1551,f3684]) ).
fof(f4889,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_8 ),
inference(superposition,[],[f714,f4866]) ).
fof(f4890,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_8 ),
inference(superposition,[],[f717,f4866]) ).
fof(f4895,plain,
( ! [X0,X1] :
( or(X0,X1) != sK259
| sK247(sK259,'1',sK260) = X0 )
| ~ spl268_8 ),
inference(superposition,[],[f722,f4866]) ).
fof(f4931,plain,
( sK259 != sK259
| sK105(sK259,'0',sK260) = sK247(sK259,'1',sK260)
| ~ spl268_8
| ~ spl268_37
| ~ spl268_66 ),
inference(superposition,[],[f4895,f4863]) ).
fof(f4932,plain,
( sK105(sK259,'0',sK260) = sK247(sK259,'1',sK260)
| ~ spl268_8
| ~ spl268_37
| ~ spl268_66 ),
inference(trivial_inequality_removal,[],[f4931]) ).
fof(f4942,plain,
( eval_succeeds(sK247(sK259,'1',sK260),sK260,'0')
| ~ sP10(sK259,'0',sK260)
| ~ spl268_8
| ~ spl268_37
| ~ spl268_66 ),
inference(superposition,[],[f878,f4932]) ).
fof(f4943,plain,
( eval_succeeds(sK247(sK259,'1',sK260),sK260,'0')
| ~ spl268_8
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f4942,f2769]) ).
fof(f4951,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP69(sK259,'1',sK260)
| ~ spl268_8
| ~ spl268_37
| ~ spl268_66 ),
inference(resolution,[],[f4943,f1318]) ).
fof(f4954,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP69(sK259,'1',sK260)
| ~ spl268_8
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f4951,f702]) ).
fof(f4955,plain,
( ~ sP69(sK259,'1',sK260)
| ~ spl268_8
| ~ spl268_14
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f4954,f1577]) ).
fof(f4956,plain,
( $false
| ~ spl268_8
| ~ spl268_14
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f4955,f4871]) ).
fof(f4957,plain,
( ~ spl268_8
| ~ spl268_14
| ~ spl268_37
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f4956]) ).
fof(f4963,plain,
( sK259 = or(sK245(sK259,sK261,sK260),sK246(sK259,sK261,sK260))
| ~ spl268_9 ),
inference(resolution,[],[f1555,f1317]) ).
fof(f4964,plain,
( sK259 = or(sK245(sK259,'1',sK260),sK246(sK259,'1',sK260))
| ~ spl268_9 ),
inference(forward_demodulation,[],[f4963,f3688]) ).
fof(f4970,plain,
( sP70(sK259,'1',sK260)
| ~ spl268_9 ),
inference(superposition,[],[f1555,f3688]) ).
fof(f4976,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_9 ),
inference(superposition,[],[f714,f4964]) ).
fof(f4977,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_9 ),
inference(superposition,[],[f717,f4964]) ).
fof(f4980,plain,
( ! [X0,X1] :
( or(X0,X1) != sK259
| sK246(sK259,'1',sK260) = X1 )
| ~ spl268_9 ),
inference(superposition,[],[f721,f4964]) ).
fof(f4993,plain,
( sK259 != sK259
| sK106(sK259,'0',sK260) = sK246(sK259,'1',sK260)
| ~ spl268_9
| ~ spl268_37
| ~ spl268_66 ),
inference(superposition,[],[f4980,f4863]) ).
fof(f4994,plain,
( sK106(sK259,'0',sK260) = sK246(sK259,'1',sK260)
| ~ spl268_9
| ~ spl268_37
| ~ spl268_66 ),
inference(trivial_inequality_removal,[],[f4993]) ).
fof(f4999,plain,
( eval_succeeds(sK246(sK259,'1',sK260),sK260,'0')
| ~ sP10(sK259,'0',sK260)
| ~ spl268_9
| ~ spl268_37
| ~ spl268_66 ),
inference(superposition,[],[f877,f4994]) ).
fof(f5000,plain,
( eval_succeeds(sK246(sK259,'1',sK260),sK260,'0')
| ~ spl268_9
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f4999,f2769]) ).
fof(f5008,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP70(sK259,'1',sK260)
| ~ spl268_9
| ~ spl268_37
| ~ spl268_66 ),
inference(resolution,[],[f5000,f1314]) ).
fof(f5011,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP70(sK259,'1',sK260)
| ~ spl268_9
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5008,f702]) ).
fof(f5012,plain,
( ~ sP70(sK259,'1',sK260)
| ~ spl268_9
| ~ spl268_14
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5011,f1577]) ).
fof(f5013,plain,
( $false
| ~ spl268_9
| ~ spl268_14
| ~ spl268_37
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5012,f4970]) ).
fof(f5014,plain,
( ~ spl268_9
| ~ spl268_14
| ~ spl268_37
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f5013]) ).
fof(f5017,plain,
( $false
| ~ spl268_8
| spl268_16
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4203,f3684]) ).
fof(f5018,plain,
( ~ spl268_8
| spl268_16
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f5017]) ).
fof(f5020,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| sP13(sK259,sK262,sK260)
| sP11(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_39
| spl268_41
| spl268_42
| spl268_43
| spl268_44 ),
inference(forward_subsumption_resolution,[],[f4659,f1774]) ).
fof(f5023,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| sP11(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44 ),
inference(forward_subsumption_resolution,[],[f5020,f1766]) ).
fof(f5024,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| sP10(sK259,sK262,sK260)
| ~ spl268_15
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44 ),
inference(forward_subsumption_resolution,[],[f5023,f1758]) ).
fof(f5025,plain,
( sK259 = or(sK93(sK260,sK262,sK259),sK94(sK260,sK262,sK259))
| sP17(sK259,sK262,sK260)
| ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44 ),
inference(forward_subsumption_resolution,[],[f5024,f1754]) ).
fof(f5026,plain,
( sK259 = or(sK93(sK260,'1',sK259),sK94(sK260,'1',sK259))
| sP17(sK259,sK262,sK260)
| ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51 ),
inference(forward_demodulation,[],[f5025,f1992]) ).
fof(f5027,plain,
( sP17(sK259,sK262,sK260)
| ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_95 ),
inference(forward_subsumption_resolution,[],[f5026,f4046]) ).
fof(f5028,plain,
( sP17(sK259,'1',sK260)
| ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_95 ),
inference(forward_demodulation,[],[f5027,f1992]) ).
fof(f5033,plain,
( $false
| ~ spl268_5
| spl268_16
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4203,f1800]) ).
fof(f5034,plain,
( ~ spl268_5
| spl268_16
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f5033]) ).
fof(f5040,plain,
( $false
| ~ spl268_9
| spl268_16
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4203,f3688]) ).
fof(f5041,plain,
( ~ spl268_9
| spl268_16
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f5040]) ).
fof(f5048,plain,
( $false
| ~ spl268_3
| spl268_16
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f4203,f1642]) ).
fof(f5049,plain,
( ~ spl268_3
| spl268_16
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f5048]) ).
fof(f5052,plain,
( spl268_66
| ~ spl268_39 ),
inference(avatar_split_clause,[],[f4181,f1761,f2679]) ).
fof(f5057,plain,
( sK259 = neg(sK254(sK259,sK261,sK260))
| ~ spl268_3 ),
inference(resolution,[],[f1531,f1337]) ).
fof(f5058,plain,
( $false
| ~ spl268_3
| ~ spl268_39
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5057,f2840]) ).
fof(f5059,plain,
( ~ spl268_3
| ~ spl268_39
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f5058]) ).
fof(f5087,plain,
( sK259 = p(sK103(sK259,sK262,sK260))
| ~ spl268_39 ),
inference(resolution,[],[f1763,f871]) ).
fof(f5090,plain,
( $false
| ~ spl268_8
| ~ spl268_39 ),
inference(forward_subsumption_resolution,[],[f5087,f4889]) ).
fof(f5091,plain,
( ~ spl268_8
| ~ spl268_39 ),
inference(avatar_contradiction_clause,[],[f5090]) ).
fof(f5097,plain,
( $false
| ~ spl268_9
| ~ spl268_39 ),
inference(forward_subsumption_resolution,[],[f5087,f4976]) ).
fof(f5098,plain,
( ~ spl268_9
| ~ spl268_39 ),
inference(avatar_contradiction_clause,[],[f5097]) ).
fof(f5415,plain,
( sK259 = neg(sK101(sK259,'0',sK260))
| ~ spl268_41
| ~ spl268_66 ),
inference(resolution,[],[f2709,f863]) ).
fof(f5417,plain,
( $false
| ~ spl268_8
| ~ spl268_41
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5415,f4890]) ).
fof(f5418,plain,
( ~ spl268_8
| ~ spl268_41
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f5417]) ).
fof(f5424,plain,
( $false
| ~ spl268_9
| ~ spl268_41
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5415,f4977]) ).
fof(f5425,plain,
( ~ spl268_9
| ~ spl268_41
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f5424]) ).
fof(f5435,plain,
( sK259 = neg(sK254(sK259,sK261,sK260))
| ~ spl268_3 ),
inference(resolution,[],[f1531,f1337]) ).
fof(f5436,plain,
( sK259 = neg(sK254(sK259,'1',sK260))
| ~ spl268_3 ),
inference(forward_demodulation,[],[f5435,f1642]) ).
fof(f5449,plain,
( ! [X0] :
( neg(X0) != sK259
| sK254(sK259,'1',sK260) = X0 )
| ~ spl268_3 ),
inference(superposition,[],[f715,f5436]) ).
fof(f5497,plain,
( sK259 != sK259
| sK254(sK259,'1',sK260) = sK101(sK259,'0',sK260)
| ~ spl268_3
| ~ spl268_41
| ~ spl268_66 ),
inference(superposition,[],[f5449,f5415]) ).
fof(f5498,plain,
( sK254(sK259,'1',sK260) = sK101(sK259,'0',sK260)
| ~ spl268_3
| ~ spl268_41
| ~ spl268_66 ),
inference(trivial_inequality_removal,[],[f5497]) ).
fof(f5511,plain,
( eval_succeeds(sK254(sK259,'1',sK260),sK260,'1')
| ~ sP14(sK259,'0',sK260)
| ~ spl268_3
| ~ spl268_41
| ~ spl268_66 ),
inference(superposition,[],[f861,f5498]) ).
fof(f5512,plain,
( eval_succeeds(sK254(sK259,'1',sK260),sK260,'1')
| ~ spl268_3
| ~ spl268_41
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5511,f2709]) ).
fof(f5514,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP65(sK259,'1',sK260)
| ~ spl268_3
| ~ spl268_41
| ~ spl268_66 ),
inference(resolution,[],[f5512,f1334]) ).
fof(f5518,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP65(sK259,'1',sK260)
| ~ spl268_3
| ~ spl268_41
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5514,f702]) ).
fof(f5519,plain,
( ~ sP65(sK259,'1',sK260)
| ~ spl268_3
| ~ spl268_14
| ~ spl268_41
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5518,f1577]) ).
fof(f5520,plain,
( $false
| ~ spl268_3
| ~ spl268_14
| ~ spl268_41
| ~ spl268_66 ),
inference(forward_subsumption_resolution,[],[f5519,f1644]) ).
fof(f5521,plain,
( ~ spl268_3
| ~ spl268_14
| ~ spl268_41
| ~ spl268_66 ),
inference(avatar_contradiction_clause,[],[f5520]) ).
fof(f5522,plain,
( spl268_12
| ~ spl268_6 ),
inference(avatar_split_clause,[],[f3614,f1541,f1565]) ).
fof(f5524,definition,
( spl268_130
<=> sP12(sK259,'1',sK260) ),
introduced(definition,[new_symbols(definition,[spl268_130])],[avatar_definition]) ).
fof(f5525,plain,
( ~ sP12(sK259,'1',sK260)
| spl268_130 ),
inference(avatar_component_clause,[],[f5524]) ).
fof(f5532,definition,
( spl268_131
<=> sP10(sK259,'1',sK260) ),
introduced(definition,[new_symbols(definition,[spl268_131])],[avatar_definition]) ).
fof(f5533,plain,
( ~ sP10(sK259,'1',sK260)
| spl268_131 ),
inference(avatar_component_clause,[],[f5532]) ).
fof(f5544,plain,
( ~ spl268_130
| spl268_39
| ~ spl268_51 ),
inference(avatar_split_clause,[],[f4146,f1990,f1761,f5524]) ).
fof(f5545,plain,
( ~ spl268_131
| spl268_37
| ~ spl268_51 ),
inference(avatar_split_clause,[],[f4150,f1990,f1753,f5532]) ).
fof(f5582,plain,
( sK259 = and(sK251(sK259,sK261,sK260),sK252(sK259,sK261,sK260))
| ~ spl268_6 ),
inference(resolution,[],[f1543,f1329]) ).
fof(f5583,plain,
( sK259 = and(sK251(sK259,'0',sK260),sK252(sK259,'0',sK260))
| ~ spl268_6
| ~ spl268_12 ),
inference(forward_demodulation,[],[f5582,f1567]) ).
fof(f5586,plain,
( sP67(sK259,'0',sK260)
| ~ spl268_6
| ~ spl268_12 ),
inference(superposition,[],[f1543,f1567]) ).
fof(f5591,plain,
( sK259 = and(sK107(sK259,sK262,sK260),sK108(sK259,sK262,sK260))
| ~ spl268_42 ),
inference(resolution,[],[f1775,f885]) ).
fof(f5593,plain,
( sK259 = and(sK107(sK259,'1',sK260),sK108(sK259,'1',sK260))
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_demodulation,[],[f5591,f1992]) ).
fof(f5615,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_6
| ~ spl268_12 ),
inference(superposition,[],[f713,f5583]) ).
fof(f5616,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_6
| ~ spl268_12 ),
inference(superposition,[],[f716,f5583]) ).
fof(f5620,plain,
( ! [X0,X1] :
( and(X0,X1) != sK259
| sK251(sK259,'0',sK260) = X0 )
| ~ spl268_6
| ~ spl268_12 ),
inference(superposition,[],[f719,f5583]) ).
fof(f5659,plain,
( sK259 = or(sK93(sK260,'1',sK259),sK94(sK260,'1',sK259))
| sP17(sK259,'1',sK260)
| sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_15
| ~ spl268_51 ),
inference(resolution,[],[f4132,f838]) ).
fof(f5685,plain,
( sK259 != sK259
| sK251(sK259,'0',sK260) = sK107(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(superposition,[],[f5620,f5593]) ).
fof(f5686,plain,
( sK251(sK259,'0',sK260) = sK107(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(trivial_inequality_removal,[],[f5685]) ).
fof(f5702,plain,
( eval_succeeds(sK251(sK259,'0',sK260),sK260,'1')
| ~ sP9(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(superposition,[],[f883,f5686]) ).
fof(f5703,plain,
( eval_succeeds(sK251(sK259,'0',sK260),sK260,'1')
| ~ spl268_6
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f5702,f4620]) ).
fof(f5706,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP67(sK259,'0',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(resolution,[],[f5703,f1326]) ).
fof(f5710,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP67(sK259,'0',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f5706,f702]) ).
fof(f5711,plain,
( ~ sP67(sK259,'0',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_14
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f5710,f1577]) ).
fof(f5712,plain,
( $false
| ~ spl268_6
| ~ spl268_12
| ~ spl268_14
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f5711,f5586]) ).
fof(f5713,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_14
| ~ spl268_42
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f5712]) ).
fof(f5733,plain,
( spl268_96
| ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_95 ),
inference(avatar_split_clause,[],[f5028,f4045,f1990,f1781,f1777,f1773,f1769,f1765,f1761,f1757,f1753,f1580,f4049]) ).
fof(f5795,plain,
( sP64(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12 ),
inference(forward_demodulation,[],[f1559,f1567]) ).
fof(f5942,plain,
( sK259 = and(sK251(sK259,'0',sK260),sK252(sK259,'0',sK260))
| ~ spl268_6
| ~ spl268_12 ),
inference(resolution,[],[f5586,f1329]) ).
fof(f5944,plain,
( sK259 = or(sK95(sK259,'1',sK260),sK96(sK259,'1',sK260))
| ~ spl268_96 ),
inference(resolution,[],[f4051,f851]) ).
fof(f5978,plain,
( ! [X0,X1] : or(X0,X1) != sK259
| ~ spl268_6
| ~ spl268_12 ),
inference(superposition,[],[f720,f5942]) ).
fof(f5989,plain,
( sK259 != sK259
| ~ spl268_6
| ~ spl268_12
| ~ spl268_96 ),
inference(superposition,[],[f5978,f5944]) ).
fof(f5990,plain,
( $false
| ~ spl268_6
| ~ spl268_12
| ~ spl268_96 ),
inference(trivial_inequality_removal,[],[f5989]) ).
fof(f5991,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_96 ),
inference(avatar_contradiction_clause,[],[f5990]) ).
fof(f6002,plain,
( sK259 = neg(sK102(sK259,'1',sK260))
| ~ spl268_40
| ~ spl268_51 ),
inference(resolution,[],[f4584,f867]) ).
fof(f6004,plain,
( $false
| ~ spl268_6
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6002,f5616]) ).
fof(f6005,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6004]) ).
fof(f6013,plain,
( sK259 = p(sK104(sK259,'1',sK260))
| ~ spl268_38
| ~ spl268_51 ),
inference(resolution,[],[f4053,f875]) ).
fof(f6015,plain,
( $false
| ~ spl268_6
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6013,f5615]) ).
fof(f6016,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6015]) ).
fof(f6021,plain,
( sP17(sK259,'1',sK260)
| sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f5659,f5978]) ).
fof(f6023,plain,
( sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f6021,f4050]) ).
fof(f6025,plain,
( sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f6023,f4139]) ).
fof(f6027,plain,
( sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f6025,f4138]) ).
fof(f6029,plain,
( sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f6027,f4137]) ).
fof(f6031,plain,
( sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f6029,f4145]) ).
fof(f6033,plain,
( sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(forward_subsumption_resolution,[],[f6031,f4136]) ).
fof(f6035,plain,
( sP11(sK259,'1',sK260)
| sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96
| spl268_130 ),
inference(forward_subsumption_resolution,[],[f6033,f5525]) ).
fof(f6037,plain,
( sP10(sK259,'1',sK260)
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96
| spl268_130 ),
inference(forward_subsumption_resolution,[],[f6035,f4502]) ).
fof(f6039,plain,
( $false
| ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96
| spl268_130
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6037,f5533]) ).
fof(f6040,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96
| spl268_130
| spl268_131 ),
inference(avatar_contradiction_clause,[],[f6039]) ).
fof(f6046,plain,
( sK259 = or(sK255(sK259,'0',sK260),sK256(sK259,'0',sK260))
| ~ spl268_10
| ~ spl268_12 ),
inference(resolution,[],[f5795,f1343]) ).
fof(f6051,plain,
( ! [X0] : p(X0) != sK259
| ~ spl268_10
| ~ spl268_12 ),
inference(superposition,[],[f714,f6046]) ).
fof(f6052,plain,
( ! [X0] : neg(X0) != sK259
| ~ spl268_10
| ~ spl268_12 ),
inference(superposition,[],[f717,f6046]) ).
fof(f6053,plain,
( ! [X0,X1] : and(X0,X1) != sK259
| ~ spl268_10
| ~ spl268_12 ),
inference(superposition,[],[f720,f6046]) ).
fof(f6055,plain,
( ! [X0,X1] :
( or(X0,X1) != sK259
| sK256(sK259,'0',sK260) = X1 )
| ~ spl268_10
| ~ spl268_12 ),
inference(superposition,[],[f721,f6046]) ).
fof(f6057,plain,
( ! [X0,X1] :
( or(X0,X1) != sK259
| sK255(sK259,'0',sK260) = X0 )
| ~ spl268_10
| ~ spl268_12 ),
inference(superposition,[],[f722,f6046]) ).
fof(f6092,plain,
( sK259 != sK259
| sK94(sK260,'1',sK259) = sK256(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_95 ),
inference(superposition,[],[f6055,f4047]) ).
fof(f6095,plain,
( sK94(sK260,'1',sK259) = sK256(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_95 ),
inference(trivial_inequality_removal,[],[f6092]) ).
fof(f6103,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP10(sK259,'1',sK260)
| sP17(sK259,'1',sK260)
| sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_95 ),
inference(superposition,[],[f836,f6095]) ).
fof(f6104,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP17(sK259,'1',sK260)
| sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_95
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6103,f5533]) ).
fof(f6107,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP16(sK259,'1',sK260)
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_95
| spl268_96
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6104,f4050]) ).
fof(f6109,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP15(sK259,'1',sK260)
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6107,f4139]) ).
fof(f6111,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP9(sK259,'1',sK260)
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6109,f4138]) ).
fof(f6113,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP14(sK259,'1',sK260)
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6111,f4137]) ).
fof(f6115,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP13(sK259,'1',sK260)
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6113,f4145]) ).
fof(f6117,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP12(sK259,'1',sK260)
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6115,f4136]) ).
fof(f6119,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| sP11(sK259,'1',sK260)
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6117,f5525]) ).
fof(f6121,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| ~ sP18(sK260,'1',sK259)
| ~ spl268_10
| ~ spl268_12
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6119,f4502]) ).
fof(f6123,plain,
( eval_succeeds(sK256(sK259,'0',sK260),sK260,'1')
| ~ spl268_10
| ~ spl268_12
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6121,f4132]) ).
fof(f6170,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP64(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(resolution,[],[f6123,f1338]) ).
fof(f6174,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP64(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6170,f702]) ).
fof(f6175,plain,
( ~ sP64(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_14
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6174,f1577]) ).
fof(f6176,plain,
( $false
| ~ spl268_10
| ~ spl268_12
| ~ spl268_14
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(forward_subsumption_resolution,[],[f6175,f5795]) ).
fof(f6177,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_14
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(avatar_contradiction_clause,[],[f6176]) ).
fof(f6247,plain,
( sK259 = and(sK107(sK259,'1',sK260),sK108(sK259,'1',sK260))
| ~ spl268_42
| ~ spl268_51 ),
inference(resolution,[],[f4620,f885]) ).
fof(f6252,plain,
( $false
| ~ spl268_10
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6247,f6053]) ).
fof(f6253,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6252]) ).
fof(f6269,plain,
( sK259 = p(sK104(sK259,'1',sK260))
| ~ spl268_38
| ~ spl268_51 ),
inference(resolution,[],[f4053,f875]) ).
fof(f6271,plain,
( $false
| ~ spl268_10
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6269,f6051]) ).
fof(f6272,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6271]) ).
fof(f6276,plain,
( sK259 = neg(sK102(sK259,'1',sK260))
| ~ spl268_40
| ~ spl268_51 ),
inference(resolution,[],[f4584,f867]) ).
fof(f6278,plain,
( $false
| ~ spl268_10
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6276,f6052]) ).
fof(f6279,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6278]) ).
fof(f6283,plain,
( sK259 = or(sK95(sK259,'1',sK260),sK96(sK259,'1',sK260))
| ~ spl268_96 ),
inference(resolution,[],[f4051,f851]) ).
fof(f6308,plain,
( sK259 != sK259
| sK95(sK259,'1',sK260) = sK255(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_96 ),
inference(superposition,[],[f6057,f6283]) ).
fof(f6309,plain,
( sK95(sK259,'1',sK260) = sK255(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_96 ),
inference(trivial_inequality_removal,[],[f6308]) ).
fof(f6327,plain,
( eval_succeeds(sK255(sK259,'0',sK260),sK260,'1')
| ~ sP17(sK259,'1',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_96 ),
inference(superposition,[],[f849,f6309]) ).
fof(f6328,plain,
( eval_succeeds(sK255(sK259,'0',sK260),sK260,'1')
| ~ spl268_10
| ~ spl268_12
| ~ spl268_96 ),
inference(forward_subsumption_resolution,[],[f6327,f4051]) ).
fof(f6331,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP64(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_96 ),
inference(resolution,[],[f6328,f1340]) ).
fof(f6335,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP64(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_96 ),
inference(forward_subsumption_resolution,[],[f6331,f702]) ).
fof(f6336,plain,
( ~ sP64(sK259,'0',sK260)
| ~ spl268_10
| ~ spl268_12
| ~ spl268_14
| ~ spl268_96 ),
inference(forward_subsumption_resolution,[],[f6335,f1577]) ).
fof(f6337,plain,
( $false
| ~ spl268_10
| ~ spl268_12
| ~ spl268_14
| ~ spl268_96 ),
inference(forward_subsumption_resolution,[],[f6336,f5795]) ).
fof(f6338,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_14
| ~ spl268_96 ),
inference(avatar_contradiction_clause,[],[f6337]) ).
fof(f6343,plain,
( sK259 = and(sK249(sK259,'0',sK260),sK250(sK259,'0',sK260))
| ~ spl268_7
| ~ spl268_12 ),
inference(resolution,[],[f4815,f1325]) ).
fof(f6344,plain,
( $false
| ~ spl268_7
| ~ spl268_12
| ~ spl268_95 ),
inference(forward_subsumption_resolution,[],[f6343,f4690]) ).
fof(f6345,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_95 ),
inference(avatar_contradiction_clause,[],[f6344]) ).
fof(f6356,plain,
( ! [X0,X1] :
( and(X0,X1) != sK259
| sK250(sK259,'0',sK260) = X1 )
| ~ spl268_7
| ~ spl268_12 ),
inference(superposition,[],[f718,f6343]) ).
fof(f6359,plain,
( ! [X0,X1] : or(X0,X1) != sK259
| ~ spl268_7
| ~ spl268_12 ),
inference(superposition,[],[f720,f6343]) ).
fof(f6371,plain,
( sK259 = or(sK95(sK259,'1',sK260),sK96(sK259,'1',sK260))
| ~ spl268_96 ),
inference(resolution,[],[f4051,f851]) ).
fof(f6373,plain,
( $false
| ~ spl268_7
| ~ spl268_12
| ~ spl268_96 ),
inference(forward_subsumption_resolution,[],[f6371,f6359]) ).
fof(f6374,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_96 ),
inference(avatar_contradiction_clause,[],[f6373]) ).
fof(f6392,plain,
( sK259 = p(sK104(sK259,'1',sK260))
| ~ spl268_38
| ~ spl268_51 ),
inference(resolution,[],[f4053,f875]) ).
fof(f6394,plain,
( $false
| ~ spl268_7
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6392,f4823]) ).
fof(f6395,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6394]) ).
fof(f6399,plain,
( sK259 = neg(sK102(sK259,'1',sK260))
| ~ spl268_40
| ~ spl268_51 ),
inference(resolution,[],[f4584,f867]) ).
fof(f6401,plain,
( $false
| ~ spl268_7
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6399,f4824]) ).
fof(f6402,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6401]) ).
fof(f6406,plain,
( sK259 = and(sK107(sK259,'1',sK260),sK108(sK259,'1',sK260))
| ~ spl268_42
| ~ spl268_51 ),
inference(resolution,[],[f4620,f885]) ).
fof(f6429,plain,
( sK259 != sK259
| sK250(sK259,'0',sK260) = sK108(sK259,'1',sK260)
| ~ spl268_7
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(superposition,[],[f6356,f6406]) ).
fof(f6432,plain,
( sK250(sK259,'0',sK260) = sK108(sK259,'1',sK260)
| ~ spl268_7
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(trivial_inequality_removal,[],[f6429]) ).
fof(f6441,plain,
( eval_succeeds(sK250(sK259,'0',sK260),sK260,'1')
| ~ sP9(sK259,'1',sK260)
| ~ spl268_7
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(superposition,[],[f882,f6432]) ).
fof(f6442,plain,
( eval_succeeds(sK250(sK259,'0',sK260),sK260,'1')
| ~ spl268_7
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6441,f4620]) ).
fof(f6445,plain,
( '1' = '0'
| ~ interpretation_succeeds(sK260)
| ~ sP68(sK259,'0',sK260)
| ~ spl268_7
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(resolution,[],[f6442,f1322]) ).
fof(f6449,plain,
( ~ interpretation_succeeds(sK260)
| ~ sP68(sK259,'0',sK260)
| ~ spl268_7
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6445,f702]) ).
fof(f6450,plain,
( ~ sP68(sK259,'0',sK260)
| ~ spl268_7
| ~ spl268_12
| ~ spl268_14
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6449,f1577]) ).
fof(f6451,plain,
( $false
| ~ spl268_7
| ~ spl268_12
| ~ spl268_14
| ~ spl268_42
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f6450,f4815]) ).
fof(f6452,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_14
| ~ spl268_42
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6451]) ).
fof(f6484,plain,
( $false
| ~ spl268_1
| spl268_16
| ~ spl268_51 ),
inference(forward_subsumption_resolution,[],[f2688,f4131]) ).
fof(f6485,plain,
( ~ spl268_1
| spl268_16
| ~ spl268_51 ),
inference(avatar_contradiction_clause,[],[f6484]) ).
cnf(s1,plain,
( spl268_1
| spl268_2
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10
| spl268_11 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s2,plain,
( spl268_1
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10
| spl268_11
| spl268_12 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s3,plain,
( spl268_1
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10
| spl268_11
| spl268_13 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s4,plain,
( spl268_11
| spl268_14 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s5,plain,
( spl268_11
| spl268_15 ),
inference(sat_conversion,[],[f1583]) ).
cnf(s6,plain,
( spl268_11
| ~ spl268_16 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s7,plain,
~ spl268_11,
inference(sat_conversion,[],[f1611]) ).
cnf(s11,plain,
( ~ spl268_3
| ~ spl268_37 ),
inference(sat_conversion,[],[f1796]) ).
cnf(s12,plain,
( ~ spl268_4
| spl268_12 ),
inference(sat_conversion,[],[f1799]) ).
cnf(s13,plain,
( ~ spl268_5
| ~ spl268_37 ),
inference(sat_conversion,[],[f1819]) ).
cnf(s16,plain,
( ~ spl268_5
| ~ spl268_39 ),
inference(sat_conversion,[],[f1834]) ).
cnf(s18,plain,
( ~ spl268_5
| ~ spl268_41 ),
inference(sat_conversion,[],[f1842]) ).
cnf(s21,plain,
( ~ spl268_15
| spl268_50
| spl268_51 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s22,plain,
( ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| spl268_44
| spl268_51 ),
inference(sat_conversion,[],[f1997]) ).
cnf(s70,plain,
( ~ spl268_1
| ~ spl268_41
| ~ spl268_66 ),
inference(sat_conversion,[],[f2747]) ).
cnf(s73,plain,
( ~ spl268_1
| ~ spl268_37 ),
inference(sat_conversion,[],[f2814]) ).
cnf(s91,plain,
( ~ spl268_1
| ~ spl268_14
| ~ spl268_39
| ~ spl268_66 ),
inference(sat_conversion,[],[f3561]) ).
cnf(s95,plain,
( ~ spl268_1
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(sat_conversion,[],[f3587]) ).
cnf(s96,plain,
( ~ spl268_12
| spl268_16
| ~ spl268_66 ),
inference(sat_conversion,[],[f3588]) ).
cnf(s98,plain,
( ~ spl268_7
| spl268_12 ),
inference(sat_conversion,[],[f3621]) ).
cnf(s99,plain,
( ~ spl268_3
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(sat_conversion,[],[f3677]) ).
cnf(s101,plain,
( ~ spl268_10
| spl268_12 ),
inference(sat_conversion,[],[f3683]) ).
cnf(s102,plain,
( ~ spl268_8
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(sat_conversion,[],[f3687]) ).
cnf(s103,plain,
( ~ spl268_9
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(sat_conversion,[],[f3691]) ).
cnf(s104,plain,
( ~ spl268_5
| ~ spl268_14
| ~ spl268_15
| spl268_37
| spl268_39
| spl268_41
| spl268_43
| ~ spl268_50
| ~ spl268_66 ),
inference(sat_conversion,[],[f3854]) ).
cnf(s106,plain,
( ~ spl268_5
| ~ spl268_14
| ~ spl268_43 ),
inference(sat_conversion,[],[f3981]) ).
cnf(s107,plain,
( ~ spl268_9
| ~ spl268_43 ),
inference(sat_conversion,[],[f3992]) ).
cnf(s108,plain,
( ~ spl268_3
| ~ spl268_43 ),
inference(sat_conversion,[],[f3997]) ).
cnf(s109,plain,
( ~ spl268_8
| ~ spl268_43 ),
inference(sat_conversion,[],[f4002]) ).
cnf(s111,plain,
( ~ spl268_1
| ~ spl268_43 ),
inference(sat_conversion,[],[f4013]) ).
cnf(s112,plain,
( ~ spl268_13
| ~ spl268_43 ),
inference(sat_conversion,[],[f4015]) ).
cnf(s114,plain,
( ~ spl268_12
| spl268_16
| ~ spl268_43 ),
inference(sat_conversion,[],[f4019]) ).
cnf(s115,plain,
( ~ spl268_44
| spl268_66 ),
inference(sat_conversion,[],[f4035]) ).
cnf(s120,plain,
( ~ spl268_13
| ~ spl268_37 ),
inference(sat_conversion,[],[f4149]) ).
cnf(s126,plain,
( ~ spl268_41
| spl268_66 ),
inference(sat_conversion,[],[f4195]) ).
cnf(s135,plain,
( ~ spl268_2
| ~ spl268_13
| ~ spl268_14
| ~ spl268_38
| ~ spl268_51 ),
inference(sat_conversion,[],[f4496]) ).
cnf(s148,plain,
( ~ spl268_13
| ~ spl268_96 ),
inference(sat_conversion,[],[f4583]) ).
cnf(s149,plain,
( ~ spl268_13
| ~ spl268_40
| ~ spl268_51 ),
inference(sat_conversion,[],[f4602]) ).
cnf(s152,plain,
( ~ spl268_13
| ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96 ),
inference(sat_conversion,[],[f4619]) ).
cnf(s154,plain,
( ~ spl268_13
| ~ spl268_42 ),
inference(sat_conversion,[],[f4636]) ).
cnf(s157,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_95 ),
inference(sat_conversion,[],[f4707]) ).
cnf(s158,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_96 ),
inference(sat_conversion,[],[f4714]) ).
cnf(s159,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_14
| ~ spl268_40
| ~ spl268_51 ),
inference(sat_conversion,[],[f4764]) ).
cnf(s160,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(sat_conversion,[],[f4773]) ).
cnf(s161,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_42 ),
inference(sat_conversion,[],[f4778]) ).
cnf(s162,plain,
( ~ spl268_4
| ~ spl268_12
| ~ spl268_37 ),
inference(sat_conversion,[],[f4793]) ).
cnf(s169,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_37 ),
inference(sat_conversion,[],[f4856]) ).
cnf(s170,plain,
( ~ spl268_37
| spl268_66 ),
inference(sat_conversion,[],[f4858]) ).
cnf(s171,plain,
( ~ spl268_8
| ~ spl268_14
| ~ spl268_37
| ~ spl268_66 ),
inference(sat_conversion,[],[f4957]) ).
cnf(s172,plain,
( ~ spl268_9
| ~ spl268_14
| ~ spl268_37
| ~ spl268_66 ),
inference(sat_conversion,[],[f5014]) ).
cnf(s174,plain,
( ~ spl268_8
| spl268_16
| ~ spl268_51 ),
inference(sat_conversion,[],[f5018]) ).
cnf(s176,plain,
( ~ spl268_5
| spl268_16
| ~ spl268_51 ),
inference(sat_conversion,[],[f5034]) ).
cnf(s178,plain,
( ~ spl268_9
| spl268_16
| ~ spl268_51 ),
inference(sat_conversion,[],[f5041]) ).
cnf(s180,plain,
( ~ spl268_3
| spl268_16
| ~ spl268_51 ),
inference(sat_conversion,[],[f5049]) ).
cnf(s181,plain,
( ~ spl268_39
| spl268_66 ),
inference(sat_conversion,[],[f5052]) ).
cnf(s182,plain,
( ~ spl268_3
| ~ spl268_39
| ~ spl268_66 ),
inference(sat_conversion,[],[f5059]) ).
cnf(s183,plain,
( ~ spl268_8
| ~ spl268_39 ),
inference(sat_conversion,[],[f5091]) ).
cnf(s184,plain,
( ~ spl268_9
| ~ spl268_39 ),
inference(sat_conversion,[],[f5098]) ).
cnf(s192,plain,
( ~ spl268_8
| ~ spl268_41
| ~ spl268_66 ),
inference(sat_conversion,[],[f5418]) ).
cnf(s193,plain,
( ~ spl268_9
| ~ spl268_41
| ~ spl268_66 ),
inference(sat_conversion,[],[f5425]) ).
cnf(s196,plain,
( ~ spl268_3
| ~ spl268_14
| ~ spl268_41
| ~ spl268_66 ),
inference(sat_conversion,[],[f5521]) ).
cnf(s197,plain,
( ~ spl268_6
| spl268_12 ),
inference(sat_conversion,[],[f5522]) ).
cnf(s206,plain,
( spl268_39
| ~ spl268_51
| ~ spl268_130 ),
inference(sat_conversion,[],[f5544]) ).
cnf(s207,plain,
( spl268_37
| ~ spl268_51
| ~ spl268_131 ),
inference(sat_conversion,[],[f5545]) ).
cnf(s209,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_14
| ~ spl268_42
| ~ spl268_51 ),
inference(sat_conversion,[],[f5713]) ).
cnf(s211,plain,
( ~ spl268_15
| spl268_37
| spl268_38
| spl268_39
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_95
| spl268_96 ),
inference(sat_conversion,[],[f5733]) ).
cnf(s228,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_96 ),
inference(sat_conversion,[],[f5991]) ).
cnf(s231,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(sat_conversion,[],[f6005]) ).
cnf(s232,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(sat_conversion,[],[f6016]) ).
cnf(s234,plain,
( ~ spl268_6
| ~ spl268_12
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| spl268_96
| spl268_130
| spl268_131 ),
inference(sat_conversion,[],[f6040]) ).
cnf(s237,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_14
| ~ spl268_15
| spl268_38
| spl268_40
| spl268_41
| spl268_42
| spl268_43
| spl268_44
| ~ spl268_51
| ~ spl268_95
| spl268_96
| spl268_130
| spl268_131 ),
inference(sat_conversion,[],[f6177]) ).
cnf(s244,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_42
| ~ spl268_51 ),
inference(sat_conversion,[],[f6253]) ).
cnf(s245,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(sat_conversion,[],[f6272]) ).
cnf(s246,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(sat_conversion,[],[f6279]) ).
cnf(s251,plain,
( ~ spl268_10
| ~ spl268_12
| ~ spl268_14
| ~ spl268_96 ),
inference(sat_conversion,[],[f6338]) ).
cnf(s255,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_95 ),
inference(sat_conversion,[],[f6345]) ).
cnf(s261,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_96 ),
inference(sat_conversion,[],[f6374]) ).
cnf(s266,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_38
| ~ spl268_51 ),
inference(sat_conversion,[],[f6395]) ).
cnf(s267,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_40
| ~ spl268_51 ),
inference(sat_conversion,[],[f6402]) ).
cnf(s268,plain,
( ~ spl268_7
| ~ spl268_12
| ~ spl268_14
| ~ spl268_42
| ~ spl268_51 ),
inference(sat_conversion,[],[f6452]) ).
cnf(s277,plain,
( ~ spl268_1
| spl268_16
| ~ spl268_51 ),
inference(sat_conversion,[],[f6485]) ).
cnf(s281,plain,
~ spl268_16,
inference(rat,[],[s6,s7]) ).
cnf(s282,plain,
spl268_15,
inference(rat,[],[s5,s7]) ).
cnf(s283,plain,
spl268_14,
inference(rat,[],[s4,s7]) ).
cnf(s284,plain,
( spl268_1
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10
| spl268_13 ),
inference(rat,[],[s3,s7]) ).
cnf(s285,plain,
( spl268_1
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10
| spl268_12 ),
inference(rat,[],[s2,s7]) ).
cnf(s286,plain,
( spl268_1
| spl268_2
| spl268_3
| spl268_4
| spl268_5
| spl268_6
| spl268_7
| spl268_8
| spl268_9
| spl268_10 ),
inference(rat,[],[s1,s7]) ).
cnf(s287,plain,
( ~ spl268_12
| ~ spl268_10 ),
inference(rat,[],[s211,s237,s244,s245,s246,s206,s207,s22,s115,s126,s170,s181,s96,s114,s251,s281,s283,s282]) ).
cnf(s288,plain,
~ spl268_10,
inference(rat,[],[s287,s101]) ).
cnf(s289,plain,
( spl268_41
| spl268_37
| ~ spl268_9 ),
inference(rat,[],[s115,s22,s103,s184,s107,s21,s178,s282,s281]) ).
cnf(s290,plain,
( ~ spl268_41
| ~ spl268_9 ),
inference(rat,[],[s126,s193]) ).
cnf(s291,plain,
( spl268_41
| ~ spl268_9 ),
inference(rat,[],[s172,s170,s289,s283]) ).
cnf(s292,plain,
~ spl268_9,
inference(rat,[],[s291,s290]) ).
cnf(s293,plain,
( spl268_66
| spl268_41
| ~ spl268_8 ),
inference(rat,[],[s22,s115,s170,s183,s174,s109,s282,s281]) ).
cnf(s294,plain,
( spl268_41
| ~ spl268_8 ),
inference(rat,[],[s102,s171,s293,s183,s109,s21,s174,s283,s282,s281]) ).
cnf(s295,plain,
( ~ spl268_41
| ~ spl268_8 ),
inference(rat,[],[s126,s192]) ).
cnf(s296,plain,
~ spl268_8,
inference(rat,[],[s295,s294]) ).
cnf(s297,plain,
( ~ spl268_12
| ~ spl268_7 ),
inference(rat,[],[s211,s266,s267,s268,s22,s115,s126,s181,s96,s114,s169,s255,s261,s281,s283,s282]) ).
cnf(s298,plain,
~ spl268_7,
inference(rat,[],[s297,s98]) ).
cnf(s299,plain,
( ~ spl268_12
| ~ spl268_6 ),
inference(rat,[],[s234,s209,s231,s232,s206,s207,s22,s115,s126,s170,s181,s96,s114,s228,s281,s283,s282]) ).
cnf(s300,plain,
~ spl268_6,
inference(rat,[],[s299,s197]) ).
cnf(s301,plain,
~ spl268_5,
inference(rat,[],[s115,s104,s22,s21,s13,s16,s18,s106,s176,s282,s283,s281]) ).
cnf(s302,plain,
( ~ spl268_12
| ~ spl268_4 ),
inference(rat,[],[s211,s159,s160,s22,s115,s126,s181,s96,s114,s157,s158,s161,s162,s281,s283,s282]) ).
cnf(s303,plain,
~ spl268_4,
inference(rat,[],[s302,s12]) ).
cnf(s304,plain,
( spl268_66
| spl268_41
| ~ spl268_3 ),
inference(rat,[],[s22,s115,s181,s180,s108,s11,s282,s281]) ).
cnf(s305,plain,
( ~ spl268_66
| spl268_41
| spl268_37
| ~ spl268_3
| spl268_43
| ~ spl268_50 ),
inference(rat,[],[s182,s99]) ).
cnf(s306,plain,
( spl268_41
| ~ spl268_3 ),
inference(rat,[],[s305,s304,s108,s11,s21,s180,s282,s281]) ).
cnf(s307,plain,
~ spl268_3,
inference(rat,[],[s196,s126,s306,s283]) ).
cnf(s308,plain,
spl268_1,
inference(rat,[],[s152,s135,s149,s22,s115,s126,s181,s96,s112,s120,s148,s154,s285,s284,s286,s282,s283,s281,s307,s301,s303,s298,s300,s292,s296,s288]) ).
cnf(s309,plain,
~ spl268_51,
inference(rat,[],[s277,s281,s308]) ).
cnf(s312,plain,
~ spl268_43,
inference(rat,[],[s111,s308]) ).
cnf(s313,plain,
~ spl268_37,
inference(rat,[],[s73,s308]) ).
cnf(s316,plain,
spl268_50,
inference(rat,[],[s21,s282,s309]) ).
cnf(s317,plain,
( spl268_66
| spl268_41 ),
inference(rat,[],[s22,s115,s181,s282,s309,s312,s313]) ).
cnf(s318,plain,
spl268_41,
inference(rat,[],[s95,s91,s317,s308,s313,s312,s316,s283]) ).
cnf(s319,plain,
spl268_66,
inference(rat,[],[s126,s318]) ).
cnf(s320,plain,
$false,
inference(rat,[],[s70,s308,s319,s318]) ).
fof(f6490,plain,
$false,
inference(avatar_sat_refutation,[],[s320]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX069+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.28 % Computer : n002.cluster.edu
% 0.23/0.28 % Model : x86_64 x86_64
% 0.23/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.28 % Memory : 8046.5625MB
% 0.23/0.28 % OS : Linux 6.8.0-71-generic
% 0.23/0.28 % CPULimit : 300
% 0.23/0.28 % WCLimit : 300
% 0.23/0.28 % DateTime : Mon Sep 28 15:00:23 UTC 2026
% 0.23/0.28 % CPUTime :
% 0.23/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.23/0.32 Running first-order theorem proving
% 0.23/0.32 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.41/3.52 % (415495)Detected formulas, will run a generic FOF schedule.
% 10.41/3.52 % (415509)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3623917939:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 10.41/3.52 % (415508)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2619725575:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 10.41/3.52 % (415512)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1929122539:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 10.41/3.52 % (415513)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2208809817:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 10.41/3.52 % (415510)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=507439418:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 10.41/3.52 % (415511)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1497759350:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 10.41/3.52 % (415514)dis-21_1_sil=8000:lcm=predicate:random_seed=2258467119:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 10.41/3.52 % (415511)Refutation not found, incomplete strategy
% 10.41/3.52 % (415511)------------------------------
% 10.41/3.52 % (415511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415511)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415511)Termination reason: Refutation not found, incomplete strategy
% 10.41/3.52 % (415511)Time elapsed: 0.045 s
% 10.41/3.52 % (415511)Peak memory usage: 89 MB
% 10.41/3.52 % (415511)Instructions burned: 43 (million)
% 10.41/3.52 % (415512)Instruction limit reached!
% 10.41/3.52 % (415512)------------------------------
% 10.41/3.52 % (415512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415512)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415512)Termination reason: Instruction limit
% 10.41/3.52 % (415512)Termination phase: Saturation
% 10.41/3.52 % (415512)Time elapsed: 0.110 s
% 10.41/3.52 % (415512)Peak memory usage: 89 MB
% 10.41/3.52 % (415512)Instructions burned: 119 (million)
% 10.41/3.52 % (415514)Instruction limit reached!
% 10.41/3.52 % (415514)------------------------------
% 10.41/3.52 % (415514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415514)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415514)Termination reason: Instruction limit
% 10.41/3.52 % (415514)Termination phase: Saturation
% 10.41/3.52 % (415514)Time elapsed: 0.109 s
% 10.41/3.52 % (415514)Peak memory usage: 90 MB
% 10.41/3.52 % (415514)Instructions burned: 129 (million)
% 10.41/3.52 % (415513)Instruction limit reached!
% 10.41/3.52 % (415513)------------------------------
% 10.41/3.52 % (415513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415513)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415513)Termination reason: Instruction limit
% 10.41/3.52 % (415513)Termination phase: Saturation
% 10.41/3.52 % (415513)Time elapsed: 0.143 s
% 10.41/3.52 % (415513)Peak memory usage: 90 MB
% 10.41/3.52 % (415513)Instructions burned: 140 (million)
% 10.41/3.52 % (415524)lrs+10_1_sil=8000:sp=occurrence:random_seed=2198557986:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 10.41/3.52 % (415525)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3772949527:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 10.41/3.52 % (415526)lrs+1011_1_sil=32000:sp=occurrence:random_seed=693465462:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 10.41/3.52 % (415511)------------------------------
% 10.41/3.52 % (415511)------------------------------
% 10.41/3.52 % (415525)Instruction limit reached!
% 10.41/3.52 % (415525)------------------------------
% 10.41/3.52 % (415525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415525)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415525)Termination reason: Instruction limit
% 10.41/3.52 % (415525)Termination phase: Saturation
% 10.41/3.52 % (415525)Time elapsed: 0.122 s
% 10.41/3.52 % (415525)Peak memory usage: 91 MB
% 10.41/3.52 % (415525)Instructions burned: 158 (million)
% 10.41/3.52 % (415524)Instruction limit reached!
% 10.41/3.52 % (415524)------------------------------
% 10.41/3.52 % (415524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415524)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415524)Termination reason: Instruction limit
% 10.41/3.52 % (415524)Termination phase: Saturation
% 10.41/3.52 % (415524)Time elapsed: 0.281 s
% 10.41/3.52 % (415524)Peak memory usage: 92 MB
% 10.41/3.52 % (415524)Instructions burned: 285 (million)
% 10.41/3.52 % (415530)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1173726799:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 10.41/3.52 % (415526)Instruction limit reached!
% 10.41/3.52 % (415526)------------------------------
% 10.41/3.52 % (415526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415526)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415526)Termination reason: Instruction limit
% 10.41/3.52 % (415526)Termination phase: Saturation
% 10.41/3.52 % (415526)Time elapsed: 0.323 s
% 10.41/3.52 % (415526)Peak memory usage: 91 MB
% 10.41/3.52 % (415526)Instructions burned: 326 (million)
% 10.41/3.52 % (415531)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2740415982:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 10.41/3.52 % (415532)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2807870748:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 10.41/3.52 % (415534)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1410671878:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 10.41/3.52 % (415530)Instruction limit reached!
% 10.41/3.52 % (415530)------------------------------
% 10.41/3.52 % (415530)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415530)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415530)Termination reason: Instruction limit
% 10.41/3.52 % (415530)Termination phase: Saturation
% 10.41/3.52 % (415530)Time elapsed: 0.247 s
% 10.41/3.52 % (415530)Peak memory usage: 93 MB
% 10.41/3.52 % (415530)Instructions burned: 249 (million)
% 10.41/3.52 % (415531)Instruction limit reached!
% 10.41/3.52 % (415531)------------------------------
% 10.41/3.52 % (415531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415531)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415531)Termination reason: Instruction limit
% 10.41/3.52 % (415531)Termination phase: Saturation
% 10.41/3.52 % (415531)Time elapsed: 0.212 s
% 10.41/3.52 % (415531)Peak memory usage: 89 MB
% 10.41/3.52 % (415531)Instructions burned: 294 (million)
% 10.41/3.52 % (415534)Instruction limit reached!
% 10.41/3.52 % (415534)------------------------------
% 10.41/3.52 % (415534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415534)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415534)Termination reason: Instruction limit
% 10.41/3.52 % (415534)Termination phase: Saturation
% 10.41/3.52 % (415534)Time elapsed: 0.111 s
% 10.41/3.52 % (415534)Peak memory usage: 91 MB
% 10.41/3.52 % (415534)Instructions burned: 113 (million)
% 10.41/3.52 % (415539)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3293097832:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 10.41/3.52 % (415538)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3684687640:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 10.41/3.52 % (415540)lrs+10_1_sil=8000:sp=occurrence:random_seed=728216130:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 10.41/3.52 % (415539)Instruction limit reached!
% 10.41/3.52 % (415539)------------------------------
% 10.41/3.52 % (415539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415539)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415539)Termination reason: Instruction limit
% 10.41/3.52 % (415539)Termination phase: Clausification
% 10.41/3.52 % (415539)Time elapsed: 0.143 s
% 10.41/3.52 % (415539)Peak memory usage: 127 MB
% 10.41/3.52 % (415539)Instructions burned: 115 (million)
% 10.41/3.52 % (415538)Instruction limit reached!
% 10.41/3.52 % (415538)------------------------------
% 10.41/3.52 % (415538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415538)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415538)Termination reason: Instruction limit
% 10.41/3.52 % (415538)Termination phase: Saturation
% 10.41/3.52 % (415538)Time elapsed: 0.114 s
% 10.41/3.52 % (415538)Peak memory usage: 90 MB
% 10.41/3.52 % (415538)Instructions burned: 127 (million)
% 10.41/3.52 % (415544)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2052760882:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 10.41/3.52 % (415544)Refutation not found, incomplete strategy
% 10.41/3.52 % (415544)------------------------------
% 10.41/3.52 % (415544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415544)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415544)Termination reason: Refutation not found, incomplete strategy
% 10.41/3.52 % (415544)Time elapsed: 0.024 s
% 10.41/3.52 % (415544)Peak memory usage: 90 MB
% 10.41/3.52 % (415544)Instructions burned: 38 (million)
% 10.41/3.52 % (415545)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3116628041:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 10.41/3.52 % (415544)------------------------------
% 10.41/3.52 % (415544)------------------------------
% 10.41/3.52 % (415508)First to succeed.
% 10.41/3.52 % (415508)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-415495"
% 10.41/3.52 % (415552)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1950502483:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2979 on theBenchmark for (2979ds/134Mi)
% 10.41/3.52 % (415540)Instruction limit reached!
% 10.41/3.52 % (415540)------------------------------
% 10.41/3.52 % (415540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415540)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415540)Termination reason: Instruction limit
% 10.41/3.52 % (415540)Termination phase: Saturation
% 10.41/3.52 % (415540)Time elapsed: 0.887 s
% 10.41/3.52 % (415540)Peak memory usage: 99 MB
% 10.41/3.52 % (415540)Instructions burned: 908 (million)
% 10.41/3.52 % (415552)Instruction limit reached!
% 10.41/3.52 % (415552)------------------------------
% 10.41/3.52 % (415552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.41/3.52 % (415552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.41/3.52 % (415552)CaDiCaL version: 2.1.3
% 10.41/3.52 % (415552)Termination reason: Instruction limit
% 10.41/3.52 % (415552)Termination phase: Saturation
% 10.41/3.52 % (415552)Time elapsed: 0.127 s
% 10.41/3.52 % (415552)Peak memory usage: 91 MB
% 10.41/3.52 % (415552)Instructions burned: 134 (million)
% 10.41/3.52 % (415554)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=893712538:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 10.41/3.52 % (415508)Refutation found. Thanks to Tanya!
% 10.41/3.52 % SZS status Theorem for theBenchmark
% 10.41/3.52 % SZS output start Proof for theBenchmark
% See solution above
% 19.29/3.77 % (415508)------------------------------
% 19.29/3.77 % (415508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.29/3.77 % (415508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.29/3.77 % (415508)CaDiCaL version: 2.1.3
% 19.29/3.77 % (415508)Termination reason: Refutation
% 19.29/3.77 % (415508)Time elapsed: 1.994 s
% 19.29/3.77 % (415508)Peak memory usage: 139 MB
% 19.29/3.77 % (415508)Instructions burned: 1986 (million)
% 19.29/3.77 % (415508)------------------------------
% 19.29/3.77 % (415508)------------------------------
% 19.29/3.77 % (415495)Success in time 2.608 s
% 19.29/3.77 % Vampire exiting
%------------------------------------------------------------------------------