%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYO606+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 02:28:25 PM UTC 2026
% Result : Theorem 2.99s 1.12s
% Output : Refutation 3.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 54
% Syntax : Number of formulae : 395 ( 16 unt; 46 def)
% Number of atoms : 1499 ( 0 equ)
% Maximal formula atoms : 41 ( 3 avg)
% Number of connectives : 1911 ( 807 ~; 885 |; 172 &)
% ( 47 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 57 ( 56 usr; 46 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 9 con; 0-2 aty)
% Number of variables : 532 ( 0 sgn 385 !; 147 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ! [X0] :
( ! [X1] : g_false_only(X0,X1)
| ? [X1] : h_true_only(X0,X1) )
& ! [X0,X1] :
? [X2] :
( g_false_only(X0,X1)
| h_true_only(X0,X2) ) )
| ( ? [X0] :
( ( ? [X1] : g_true_only(X0,X1)
& ( ( ? [X1] : h_both(X0,X1)
& ~ ? [X1] : h_true_only(X0,X1) )
| ! [X1] : h_false_only(X0,X1) ) )
| ( ? [X1] : g_both(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ! [X1] : h_false_only(X0,X1) ) )
& ? [X0,X1] :
! [X2] :
( ( g_true_only(X0,X1)
& ( h_both(X0,X2)
| h_false_only(X0,X2) ) )
| ( g_both(X0,X1)
& h_false_only(X0,X2) ) ) )
| ( ? [X0] :
( ? [X1] : g_both(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ? [X1] : h_both(X0,X1)
& ~ ? [X1] : h_true_only(X0,X1) )
& ~ ? [X0] :
( ( ? [X1] : g_true_only(X0,X1)
& ( ( ? [X1] : h_both(X0,X1)
& ~ ? [X1] : h_true_only(X0,X1) )
| ! [X1] : h_false_only(X0,X1) ) )
| ( ? [X1] : g_both(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ! [X1] : h_false_only(X0,X1) ) )
& ? [X0] :
( ? [X1] :
( ? [X2] :
( g_both(X0,X1)
& h_both(X0,X2) )
& ~ ? [X2] :
( g_false_only(X0,X1)
| h_true_only(X0,X2) ) )
& ~ ? [X1] :
! [X2] :
( ( g_true_only(X0,X1)
& ( h_both(X0,X2)
| h_false_only(X0,X2) ) )
| ( g_both(X0,X1)
& h_false_only(X0,X2) ) ) )
& ~ ? [X0,X1] :
! [X2] :
( ( g_true_only(X0,X1)
& ( h_both(X0,X2)
| h_false_only(X0,X2) ) )
| ( g_both(X0,X1)
& h_false_only(X0,X2) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nc5) ).
fof(f2,negated_conjecture,
~ ( ( ! [X0] :
( ! [X1] : g_false_only(X0,X1)
| ? [X1] : h_true_only(X0,X1) )
& ! [X0,X1] :
? [X2] :
( g_false_only(X0,X1)
| h_true_only(X0,X2) ) )
| ( ? [X0] :
( ( ? [X1] : g_true_only(X0,X1)
& ( ( ? [X1] : h_both(X0,X1)
& ~ ? [X1] : h_true_only(X0,X1) )
| ! [X1] : h_false_only(X0,X1) ) )
| ( ? [X1] : g_both(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ! [X1] : h_false_only(X0,X1) ) )
& ? [X0,X1] :
! [X2] :
( ( g_true_only(X0,X1)
& ( h_both(X0,X2)
| h_false_only(X0,X2) ) )
| ( g_both(X0,X1)
& h_false_only(X0,X2) ) ) )
| ( ? [X0] :
( ? [X1] : g_both(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ? [X1] : h_both(X0,X1)
& ~ ? [X1] : h_true_only(X0,X1) )
& ~ ? [X0] :
( ( ? [X1] : g_true_only(X0,X1)
& ( ( ? [X1] : h_both(X0,X1)
& ~ ? [X1] : h_true_only(X0,X1) )
| ! [X1] : h_false_only(X0,X1) ) )
| ( ? [X1] : g_both(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ! [X1] : h_false_only(X0,X1) ) )
& ? [X0] :
( ? [X1] :
( ? [X2] :
( g_both(X0,X1)
& h_both(X0,X2) )
& ~ ? [X2] :
( g_false_only(X0,X1)
| h_true_only(X0,X2) ) )
& ~ ? [X1] :
! [X2] :
( ( g_true_only(X0,X1)
& ( h_both(X0,X2)
| h_false_only(X0,X2) ) )
| ( g_both(X0,X1)
& h_false_only(X0,X2) ) ) )
& ~ ? [X0,X1] :
! [X2] :
( ( g_true_only(X0,X1)
& ( h_both(X0,X2)
| h_false_only(X0,X2) ) )
| ( g_both(X0,X1)
& h_false_only(X0,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f4,axiom,
! [X0,X1] :
( g_both(X0,X1)
<=> ( g_true(X0,X1)
& g_false(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',both_g) ).
fof(f5,axiom,
! [X0,X1] :
( g_false_only(X0,X1)
<=> ( g_false(X0,X1)
& ~ g_true(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',false_only_g) ).
fof(f6,axiom,
! [X0,X1] :
( g_true_only(X0,X1)
| g_both(X0,X1)
| g_false_only(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exhaustion_g) ).
fof(f7,axiom,
! [X0,X1] :
( h_true_only(X0,X1)
<=> ( h_true(X0,X1)
& ~ h_false(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',true_only_h) ).
fof(f8,axiom,
! [X0,X1] :
( h_both(X0,X1)
<=> ( h_true(X0,X1)
& h_false(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',both_h) ).
fof(f9,axiom,
! [X0,X1] :
( h_false_only(X0,X1)
<=> ( h_false(X0,X1)
& ~ h_true(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',false_only_h) ).
fof(f10,axiom,
! [X0,X1] :
( h_true_only(X0,X1)
| h_both(X0,X1)
| h_false_only(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exhaustion_h) ).
fof(f11,plain,
~ ( ( ! [X0] :
( ! [X1] : g_false_only(X0,X1)
| ? [X2] : h_true_only(X0,X2) )
& ! [X3,X4] :
? [X5] :
( g_false_only(X3,X4)
| h_true_only(X3,X5) ) )
| ( ? [X6] :
( ( ? [X7] : g_true_only(X6,X7)
& ( ( ? [X8] : h_both(X6,X8)
& ~ ? [X9] : h_true_only(X6,X9) )
| ! [X10] : h_false_only(X6,X10) ) )
| ( ? [X11] : g_both(X6,X11)
& ~ ? [X12] : g_true_only(X6,X12)
& ! [X13] : h_false_only(X6,X13) ) )
& ? [X14,X15] :
! [X16] :
( ( g_true_only(X14,X15)
& ( h_both(X14,X16)
| h_false_only(X14,X16) ) )
| ( g_both(X14,X15)
& h_false_only(X14,X16) ) ) )
| ( ? [X17] :
( ? [X18] : g_both(X17,X18)
& ~ ? [X19] : g_true_only(X17,X19)
& ? [X20] : h_both(X17,X20)
& ~ ? [X21] : h_true_only(X17,X21) )
& ~ ? [X22] :
( ( ? [X23] : g_true_only(X22,X23)
& ( ( ? [X24] : h_both(X22,X24)
& ~ ? [X25] : h_true_only(X22,X25) )
| ! [X26] : h_false_only(X22,X26) ) )
| ( ? [X27] : g_both(X22,X27)
& ~ ? [X28] : g_true_only(X22,X28)
& ! [X29] : h_false_only(X22,X29) ) )
& ? [X30] :
( ? [X31] :
( ? [X32] :
( g_both(X30,X31)
& h_both(X30,X32) )
& ~ ? [X33] :
( g_false_only(X30,X31)
| h_true_only(X30,X33) ) )
& ~ ? [X34] :
! [X35] :
( ( g_true_only(X30,X34)
& ( h_both(X30,X35)
| h_false_only(X30,X35) ) )
| ( g_both(X30,X34)
& h_false_only(X30,X35) ) ) )
& ~ ? [X36,X37] :
! [X38] :
( ( g_true_only(X36,X37)
& ( h_both(X36,X38)
| h_false_only(X36,X38) ) )
| ( g_both(X36,X37)
& h_false_only(X36,X38) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f12,plain,
( ( ? [X0] :
( ? [X1] : ~ g_false_only(X0,X1)
& ! [X2] : ~ h_true_only(X0,X2) )
| ? [X3,X4] :
! [X5] :
( ~ g_false_only(X3,X4)
& ~ h_true_only(X3,X5) ) )
& ( ! [X6] :
( ( ! [X7] : ~ g_true_only(X6,X7)
| ( ( ! [X8] : ~ h_both(X6,X8)
| ? [X9] : h_true_only(X6,X9) )
& ? [X10] : ~ h_false_only(X6,X10) ) )
& ( ! [X11] : ~ g_both(X6,X11)
| ? [X12] : g_true_only(X6,X12)
| ? [X13] : ~ h_false_only(X6,X13) ) )
| ! [X14,X15] :
? [X16] :
( ( ~ g_true_only(X14,X15)
| ( ~ h_both(X14,X16)
& ~ h_false_only(X14,X16) ) )
& ( ~ g_both(X14,X15)
| ~ h_false_only(X14,X16) ) ) )
& ( ! [X17] :
( ! [X18] : ~ g_both(X17,X18)
| ? [X19] : g_true_only(X17,X19)
| ! [X20] : ~ h_both(X17,X20)
| ? [X21] : h_true_only(X17,X21) )
| ? [X22] :
( ( ? [X23] : g_true_only(X22,X23)
& ( ( ? [X24] : h_both(X22,X24)
& ! [X25] : ~ h_true_only(X22,X25) )
| ! [X26] : h_false_only(X22,X26) ) )
| ( ? [X27] : g_both(X22,X27)
& ! [X28] : ~ g_true_only(X22,X28)
& ! [X29] : h_false_only(X22,X29) ) )
| ! [X30] :
( ! [X31] :
( ! [X32] :
( ~ g_both(X30,X31)
| ~ h_both(X30,X32) )
| ? [X33] :
( g_false_only(X30,X31)
| h_true_only(X30,X33) ) )
| ? [X34] :
! [X35] :
( ( g_true_only(X30,X34)
& ( h_both(X30,X35)
| h_false_only(X30,X35) ) )
| ( g_both(X30,X34)
& h_false_only(X30,X35) ) ) )
| ? [X36,X37] :
! [X38] :
( ( g_true_only(X36,X37)
& ( h_both(X36,X38)
| h_false_only(X36,X38) ) )
| ( g_both(X36,X37)
& h_false_only(X36,X38) ) ) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f13,definition,
! [X22] :
( ( ? [X27] : g_both(X22,X27)
& ! [X28] : ~ g_true_only(X22,X28)
& ! [X29] : h_false_only(X22,X29) )
| ~ sP0(X22) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ? [X36,X37] :
! [X38] :
( ( g_true_only(X36,X37)
& ( h_both(X36,X38)
| h_false_only(X36,X38) ) )
| ( g_both(X36,X37)
& h_false_only(X36,X38) ) )
| ~ sP1 ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ! [X30] :
( ! [X31] :
( ! [X32] :
( ~ g_both(X30,X31)
| ~ h_both(X30,X32) )
| ? [X33] :
( g_false_only(X30,X31)
| h_true_only(X30,X33) ) )
| ? [X34] :
! [X35] :
( ( g_true_only(X30,X34)
& ( h_both(X30,X35)
| h_false_only(X30,X35) ) )
| ( g_both(X30,X34)
& h_false_only(X30,X35) ) ) )
| ~ sP2 ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ! [X14,X15] :
? [X16] :
( ( ~ g_true_only(X14,X15)
| ( ~ h_both(X14,X16)
& ~ h_false_only(X14,X16) ) )
& ( ~ g_both(X14,X15)
| ~ h_false_only(X14,X16) ) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f17,plain,
( ( ? [X0] :
( ? [X1] : ~ g_false_only(X0,X1)
& ! [X2] : ~ h_true_only(X0,X2) )
| ? [X3,X4] :
! [X5] :
( ~ g_false_only(X3,X4)
& ~ h_true_only(X3,X5) ) )
& ( ! [X6] :
( ( ! [X7] : ~ g_true_only(X6,X7)
| ( ( ! [X8] : ~ h_both(X6,X8)
| ? [X9] : h_true_only(X6,X9) )
& ? [X10] : ~ h_false_only(X6,X10) ) )
& ( ! [X11] : ~ g_both(X6,X11)
| ? [X12] : g_true_only(X6,X12)
| ? [X13] : ~ h_false_only(X6,X13) ) )
| sP3 )
& ( ! [X17] :
( ! [X18] : ~ g_both(X17,X18)
| ? [X19] : g_true_only(X17,X19)
| ! [X20] : ~ h_both(X17,X20)
| ? [X21] : h_true_only(X17,X21) )
| ? [X22] :
( ( ? [X23] : g_true_only(X22,X23)
& ( ( ? [X24] : h_both(X22,X24)
& ! [X25] : ~ h_true_only(X22,X25) )
| ! [X26] : h_false_only(X22,X26) ) )
| sP0(X22) )
| sP2
| sP1 ) ),
inference(definition_folding,[],[f12,f16,f15,f14,f13]) ).
fof(f18,plain,
( ! [X14,X15] :
? [X16] :
( ( ~ g_true_only(X14,X15)
| ( ~ h_both(X14,X16)
& ~ h_false_only(X14,X16) ) )
& ( ~ g_both(X14,X15)
| ~ h_false_only(X14,X16) ) )
| ~ sP3 ),
inference(nnf_transformation,[],[f16]) ).
fof(f19,plain,
( ! [X0,X1] :
? [X2] :
( ( ~ g_true_only(X0,X1)
| ( ~ h_both(X0,X2)
& ~ h_false_only(X0,X2) ) )
& ( ~ g_both(X0,X1)
| ~ h_false_only(X0,X2) ) )
| ~ sP3 ),
inference(rectify,[],[f18]) ).
fof(f20,plain,
( ! [X0,X1] :
( ( ~ g_true_only(X0,X1)
| ( ~ h_both(X0,sK4(X0,X1))
& ~ h_false_only(X0,sK4(X0,X1)) ) )
& ( ~ g_both(X0,X1)
| ~ h_false_only(X0,sK4(X0,X1)) ) )
| ~ sP3 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f19]) ).
fof(f21,plain,
( ! [X30] :
( ! [X31] :
( ! [X32] :
( ~ g_both(X30,X31)
| ~ h_both(X30,X32) )
| ? [X33] :
( g_false_only(X30,X31)
| h_true_only(X30,X33) ) )
| ? [X34] :
! [X35] :
( ( g_true_only(X30,X34)
& ( h_both(X30,X35)
| h_false_only(X30,X35) ) )
| ( g_both(X30,X34)
& h_false_only(X30,X35) ) ) )
| ~ sP2 ),
inference(nnf_transformation,[],[f15]) ).
fof(f22,plain,
( ! [X0] :
( ! [X1] :
( ! [X2] :
( ~ g_both(X0,X1)
| ~ h_both(X0,X2) )
| ? [X3] :
( g_false_only(X0,X1)
| h_true_only(X0,X3) ) )
| ? [X4] :
! [X5] :
( ( g_true_only(X0,X4)
& ( h_both(X0,X5)
| h_false_only(X0,X5) ) )
| ( g_both(X0,X4)
& h_false_only(X0,X5) ) ) )
| ~ sP2 ),
inference(rectify,[],[f21]) ).
fof(f23,plain,
( ! [X0] :
( ! [X1] :
( ! [X2] :
( ~ g_both(X0,X1)
| ~ h_both(X0,X2) )
| g_false_only(X0,X1)
| h_true_only(X0,sK5(X0,X1)) )
| ! [X5] :
( ( g_true_only(X0,sK6(X0))
& ( h_both(X0,X5)
| h_false_only(X0,X5) ) )
| ( g_both(X0,sK6(X0))
& h_false_only(X0,X5) ) ) )
| ~ sP2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X3,sK5(X0,X1)),skolemize(X4,sK6(X0))],[f22]) ).
fof(f24,plain,
( ? [X36,X37] :
! [X38] :
( ( g_true_only(X36,X37)
& ( h_both(X36,X38)
| h_false_only(X36,X38) ) )
| ( g_both(X36,X37)
& h_false_only(X36,X38) ) )
| ~ sP1 ),
inference(nnf_transformation,[],[f14]) ).
fof(f25,plain,
( ? [X0,X1] :
! [X2] :
( ( g_true_only(X0,X1)
& ( h_both(X0,X2)
| h_false_only(X0,X2) ) )
| ( g_both(X0,X1)
& h_false_only(X0,X2) ) )
| ~ sP1 ),
inference(rectify,[],[f24]) ).
fof(f26,plain,
( ! [X2] :
( ( g_true_only(sK7,sK8)
& ( h_both(sK7,X2)
| h_false_only(sK7,X2) ) )
| ( g_both(sK7,sK8)
& h_false_only(sK7,X2) ) )
| ~ sP1 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7),skolemize(X1,sK8)],[f25]) ).
fof(f27,plain,
! [X22] :
( ( ? [X27] : g_both(X22,X27)
& ! [X28] : ~ g_true_only(X22,X28)
& ! [X29] : h_false_only(X22,X29) )
| ~ sP0(X22) ),
inference(nnf_transformation,[],[f13]) ).
fof(f28,plain,
! [X0] :
( ( ? [X1] : g_both(X0,X1)
& ! [X2] : ~ g_true_only(X0,X2)
& ! [X3] : h_false_only(X0,X3) )
| ~ sP0(X0) ),
inference(rectify,[],[f27]) ).
fof(f29,plain,
! [X0] :
( ( g_both(X0,sK9(X0))
& ! [X2] : ~ g_true_only(X0,X2)
& ! [X3] : h_false_only(X0,X3) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X1,sK9(X0))],[f28]) ).
fof(f30,plain,
( ( ? [X0] :
( ? [X1] : ~ g_false_only(X0,X1)
& ! [X2] : ~ h_true_only(X0,X2) )
| ? [X3,X4] :
! [X5] :
( ~ g_false_only(X3,X4)
& ~ h_true_only(X3,X5) ) )
& ( ! [X6] :
( ( ! [X7] : ~ g_true_only(X6,X7)
| ( ( ! [X8] : ~ h_both(X6,X8)
| ? [X9] : h_true_only(X6,X9) )
& ? [X10] : ~ h_false_only(X6,X10) ) )
& ( ! [X11] : ~ g_both(X6,X11)
| ? [X12] : g_true_only(X6,X12)
| ? [X13] : ~ h_false_only(X6,X13) ) )
| sP3 )
& ( ! [X14] :
( ! [X15] : ~ g_both(X14,X15)
| ? [X16] : g_true_only(X14,X16)
| ! [X17] : ~ h_both(X14,X17)
| ? [X18] : h_true_only(X14,X18) )
| ? [X19] :
( ( ? [X20] : g_true_only(X19,X20)
& ( ( ? [X21] : h_both(X19,X21)
& ! [X22] : ~ h_true_only(X19,X22) )
| ! [X23] : h_false_only(X19,X23) ) )
| sP0(X19) )
| sP2
| sP1 ) ),
inference(rectify,[],[f17]) ).
fof(f31,plain,
( ( ( ~ g_false_only(sK10,sK11)
& ! [X2] : ~ h_true_only(sK10,X2) )
| ! [X5] :
( ~ g_false_only(sK12,sK13)
& ~ h_true_only(sK12,X5) ) )
& ( ! [X6] :
( ( ! [X7] : ~ g_true_only(X6,X7)
| ( ( ! [X8] : ~ h_both(X6,X8)
| h_true_only(X6,sK14(X6)) )
& ~ h_false_only(X6,sK15(X6)) ) )
& ( ! [X11] : ~ g_both(X6,X11)
| g_true_only(X6,sK16(X6))
| ~ h_false_only(X6,sK17(X6)) ) )
| sP3 )
& ( ! [X14] :
( ! [X15] : ~ g_both(X14,X15)
| g_true_only(X14,sK18(X14))
| ! [X17] : ~ h_both(X14,X17)
| h_true_only(X14,sK19(X14)) )
| ( g_true_only(sK20,sK21)
& ( ( h_both(sK20,sK22)
& ! [X22] : ~ h_true_only(sK20,X22) )
| ! [X23] : h_false_only(sK20,X23) ) )
| sP0(sK20)
| sP2
| sP1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X3,sK12),skolemize(X4,sK13),skolemize(X9,sK14(X6)),skolemize(X10,sK15(X6)),skolemize(X12,sK16(X6)),skolemize(X13,sK17(X6)),skolemize(X16,sK18(X14)),skolemize(X18,sK19(X14)),skolemize(X19,sK20),skolemize(X20,sK21),skolemize(X21,sK22)],[f30]) ).
fof(f34,plain,
! [X0,X1] :
( ( g_both(X0,X1)
| ~ g_true(X0,X1)
| ~ g_false(X0,X1) )
& ( ( g_true(X0,X1)
& g_false(X0,X1) )
| ~ g_both(X0,X1) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f35,plain,
! [X0,X1] :
( ( g_both(X0,X1)
| ~ g_true(X0,X1)
| ~ g_false(X0,X1) )
& ( ( g_true(X0,X1)
& g_false(X0,X1) )
| ~ g_both(X0,X1) ) ),
inference(flattening,[],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( ( g_false_only(X0,X1)
| ~ g_false(X0,X1)
| g_true(X0,X1) )
& ( ( g_false(X0,X1)
& ~ g_true(X0,X1) )
| ~ g_false_only(X0,X1) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f37,plain,
! [X0,X1] :
( ( g_false_only(X0,X1)
| ~ g_false(X0,X1)
| g_true(X0,X1) )
& ( ( g_false(X0,X1)
& ~ g_true(X0,X1) )
| ~ g_false_only(X0,X1) ) ),
inference(flattening,[],[f36]) ).
fof(f38,plain,
! [X0,X1] :
( ( h_true_only(X0,X1)
| ~ h_true(X0,X1)
| h_false(X0,X1) )
& ( ( h_true(X0,X1)
& ~ h_false(X0,X1) )
| ~ h_true_only(X0,X1) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f39,plain,
! [X0,X1] :
( ( h_true_only(X0,X1)
| ~ h_true(X0,X1)
| h_false(X0,X1) )
& ( ( h_true(X0,X1)
& ~ h_false(X0,X1) )
| ~ h_true_only(X0,X1) ) ),
inference(flattening,[],[f38]) ).
fof(f40,plain,
! [X0,X1] :
( ( h_both(X0,X1)
| ~ h_true(X0,X1)
| ~ h_false(X0,X1) )
& ( ( h_true(X0,X1)
& h_false(X0,X1) )
| ~ h_both(X0,X1) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f41,plain,
! [X0,X1] :
( ( h_both(X0,X1)
| ~ h_true(X0,X1)
| ~ h_false(X0,X1) )
& ( ( h_true(X0,X1)
& h_false(X0,X1) )
| ~ h_both(X0,X1) ) ),
inference(flattening,[],[f40]) ).
fof(f42,plain,
! [X0,X1] :
( ( h_false_only(X0,X1)
| ~ h_false(X0,X1)
| h_true(X0,X1) )
& ( ( h_false(X0,X1)
& ~ h_true(X0,X1) )
| ~ h_false_only(X0,X1) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f43,plain,
! [X0,X1] :
( ( h_false_only(X0,X1)
| ~ h_false(X0,X1)
| h_true(X0,X1) )
& ( ( h_false(X0,X1)
& ~ h_true(X0,X1) )
| ~ h_false_only(X0,X1) ) ),
inference(flattening,[],[f42]) ).
fof(f44,plain,
! [X0,X1] :
( ~ g_both(X0,X1)
| ~ h_false_only(X0,sK4(X0,X1))
| ~ sP3 ),
inference(cnf_transformation,[],[f20]) ).
fof(f45,plain,
! [X0,X1] :
( ~ g_true_only(X0,X1)
| ~ h_false_only(X0,sK4(X0,X1))
| ~ sP3 ),
inference(cnf_transformation,[],[f20]) ).
fof(f46,plain,
! [X0,X1] :
( ~ g_true_only(X0,X1)
| ~ h_both(X0,sK4(X0,X1))
| ~ sP3 ),
inference(cnf_transformation,[],[f20]) ).
fof(f49,plain,
! [X2,X0,X1,X5] :
( ~ g_both(X0,X1)
| ~ h_both(X0,X2)
| g_false_only(X0,X1)
| h_true_only(X0,sK5(X0,X1))
| g_true_only(X0,sK6(X0))
| h_false_only(X0,X5)
| ~ sP2 ),
inference(cnf_transformation,[],[f23]) ).
fof(f51,plain,
! [X2] :
( h_both(sK7,X2)
| h_false_only(sK7,X2)
| h_false_only(sK7,X2)
| ~ sP1 ),
inference(cnf_transformation,[],[f26]) ).
fof(f53,plain,
! [X2] :
( g_true_only(sK7,sK8)
| h_false_only(sK7,X2)
| ~ sP1 ),
inference(cnf_transformation,[],[f26]) ).
fof(f54,plain,
( g_true_only(sK7,sK8)
| g_both(sK7,sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f26]) ).
fof(f55,plain,
! [X3,X0] :
( ~ sP0(X0)
| h_false_only(X0,X3) ),
inference(cnf_transformation,[],[f29]) ).
fof(f57,plain,
! [X0] :
( ~ sP0(X0)
| g_both(X0,sK9(X0)) ),
inference(cnf_transformation,[],[f29]) ).
fof(f58,plain,
! [X14,X17,X15,X22,X23] :
( ~ g_both(X14,X15)
| g_true_only(X14,sK18(X14))
| ~ h_both(X14,X17)
| h_true_only(X14,sK19(X14))
| ~ h_true_only(sK20,X22)
| h_false_only(sK20,X23)
| sP0(sK20)
| sP2
| sP1 ),
inference(cnf_transformation,[],[f31]) ).
fof(f59,plain,
! [X14,X17,X15,X23] :
( ~ g_both(X14,X15)
| g_true_only(X14,sK18(X14))
| ~ h_both(X14,X17)
| h_true_only(X14,sK19(X14))
| h_both(sK20,sK22)
| h_false_only(sK20,X23)
| sP0(sK20)
| sP2
| sP1 ),
inference(cnf_transformation,[],[f31]) ).
fof(f60,plain,
! [X14,X17,X15] :
( ~ g_both(X14,X15)
| g_true_only(X14,sK18(X14))
| ~ h_both(X14,X17)
| h_true_only(X14,sK19(X14))
| g_true_only(sK20,sK21)
| sP0(sK20)
| sP2
| sP1 ),
inference(cnf_transformation,[],[f31]) ).
fof(f61,plain,
! [X11,X6] :
( ~ g_both(X6,X11)
| g_true_only(X6,sK16(X6))
| ~ h_false_only(X6,sK17(X6))
| sP3 ),
inference(cnf_transformation,[],[f31]) ).
fof(f62,plain,
! [X6,X7] :
( ~ g_true_only(X6,X7)
| ~ h_false_only(X6,sK15(X6))
| sP3 ),
inference(cnf_transformation,[],[f31]) ).
fof(f63,plain,
! [X8,X6,X7] :
( ~ g_true_only(X6,X7)
| ~ h_both(X6,X8)
| h_true_only(X6,sK14(X6))
| sP3 ),
inference(cnf_transformation,[],[f31]) ).
fof(f64,plain,
! [X2,X5] :
( ~ h_true_only(sK10,X2)
| ~ h_true_only(sK12,X5) ),
inference(cnf_transformation,[],[f31]) ).
fof(f65,plain,
! [X2] :
( ~ h_true_only(sK10,X2)
| ~ g_false_only(sK12,sK13) ),
inference(cnf_transformation,[],[f31]) ).
fof(f66,plain,
! [X5] :
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,X5) ),
inference(cnf_transformation,[],[f31]) ).
fof(f67,plain,
( ~ g_false_only(sK10,sK11)
| ~ g_false_only(sK12,sK13) ),
inference(cnf_transformation,[],[f31]) ).
fof(f71,plain,
! [X0,X1] :
( ~ g_both(X0,X1)
| g_false(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f73,plain,
! [X0,X1] :
( ~ g_false(X0,X1)
| ~ g_true(X0,X1)
| g_both(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f75,plain,
! [X0,X1] :
( ~ g_false_only(X0,X1)
| g_false(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f76,plain,
! [X0,X1] :
( ~ g_false(X0,X1)
| g_false_only(X0,X1)
| g_true(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f77,plain,
! [X0,X1] :
( g_true_only(X0,X1)
| g_both(X0,X1)
| g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f78,plain,
! [X0,X1] :
( ~ h_false(X0,X1)
| ~ h_true_only(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f81,plain,
! [X0,X1] :
( ~ h_both(X0,X1)
| h_false(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f83,plain,
! [X0,X1] :
( ~ h_false(X0,X1)
| ~ h_true(X0,X1)
| h_both(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f85,plain,
! [X0,X1] :
( ~ h_false_only(X0,X1)
| h_false(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f86,plain,
! [X0,X1] :
( h_true(X0,X1)
| ~ h_false(X0,X1)
| h_false_only(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f87,plain,
! [X0,X1] :
( h_true_only(X0,X1)
| h_both(X0,X1)
| h_false_only(X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
fof(f88,plain,
! [X2] :
( h_both(sK7,X2)
| h_false_only(sK7,X2)
| ~ sP1 ),
inference(duplicate_literal_removal,[],[f51]) ).
fof(f91,definition,
( spl23_1
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl23_1])],[avatar_definition]) ).
fof(f95,definition,
( spl23_2
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl23_2])],[avatar_definition]) ).
fof(f99,definition,
( spl23_3
<=> sP0(sK20) ),
introduced(definition,[new_symbols(definition,[spl23_3])],[avatar_definition]) ).
fof(f101,plain,
( sP0(sK20)
| ~ spl23_3 ),
inference(avatar_component_clause,[],[f99]) ).
fof(f103,definition,
( spl23_4
<=> ! [X23] : h_false_only(sK20,X23) ),
introduced(definition,[new_symbols(definition,[spl23_4])],[avatar_definition]) ).
fof(f104,plain,
( ! [X23] : h_false_only(sK20,X23)
| ~ spl23_4 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f106,definition,
( spl23_5
<=> ! [X22] : ~ h_true_only(sK20,X22) ),
introduced(definition,[new_symbols(definition,[spl23_5])],[avatar_definition]) ).
fof(f107,plain,
( ! [X22] : ~ h_true_only(sK20,X22)
| ~ spl23_5 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f109,definition,
( spl23_6
<=> ! [X17,X14,X15] :
( ~ g_both(X14,X15)
| h_true_only(X14,sK19(X14))
| ~ h_both(X14,X17)
| g_true_only(X14,sK18(X14)) ) ),
introduced(definition,[new_symbols(definition,[spl23_6])],[avatar_definition]) ).
fof(f110,plain,
( ! [X14,X17,X15] :
( g_true_only(X14,sK18(X14))
| h_true_only(X14,sK19(X14))
| ~ h_both(X14,X17)
| ~ g_both(X14,X15) )
| ~ spl23_6 ),
inference(avatar_component_clause,[],[f109]) ).
fof(f111,plain,
( spl23_1
| spl23_2
| spl23_3
| spl23_4
| spl23_5
| spl23_6 ),
inference(avatar_split_clause,[],[f58,f109,f106,f103,f99,f95,f91]) ).
fof(f113,definition,
( spl23_7
<=> h_both(sK20,sK22) ),
introduced(definition,[new_symbols(definition,[spl23_7])],[avatar_definition]) ).
fof(f115,plain,
( h_both(sK20,sK22)
| ~ spl23_7 ),
inference(avatar_component_clause,[],[f113]) ).
fof(f116,plain,
( spl23_1
| spl23_2
| spl23_3
| spl23_4
| spl23_7
| spl23_6 ),
inference(avatar_split_clause,[],[f59,f109,f113,f103,f99,f95,f91]) ).
fof(f118,definition,
( spl23_8
<=> g_true_only(sK20,sK21) ),
introduced(definition,[new_symbols(definition,[spl23_8])],[avatar_definition]) ).
fof(f120,plain,
( g_true_only(sK20,sK21)
| ~ spl23_8 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f121,plain,
( spl23_1
| spl23_2
| spl23_3
| spl23_8
| spl23_6 ),
inference(avatar_split_clause,[],[f60,f109,f118,f99,f95,f91]) ).
fof(f123,definition,
( spl23_9
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl23_9])],[avatar_definition]) ).
fof(f127,definition,
( spl23_10
<=> ! [X6,X11] :
( ~ g_both(X6,X11)
| ~ h_false_only(X6,sK17(X6))
| g_true_only(X6,sK16(X6)) ) ),
introduced(definition,[new_symbols(definition,[spl23_10])],[avatar_definition]) ).
fof(f128,plain,
( ! [X11,X6] :
( ~ h_false_only(X6,sK17(X6))
| ~ g_both(X6,X11)
| g_true_only(X6,sK16(X6)) )
| ~ spl23_10 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f129,plain,
( spl23_9
| spl23_10 ),
inference(avatar_split_clause,[],[f61,f127,f123]) ).
fof(f131,definition,
( spl23_11
<=> ! [X6,X7] :
( ~ g_true_only(X6,X7)
| ~ h_false_only(X6,sK15(X6)) ) ),
introduced(definition,[new_symbols(definition,[spl23_11])],[avatar_definition]) ).
fof(f132,plain,
( ! [X6,X7] :
( ~ h_false_only(X6,sK15(X6))
| ~ g_true_only(X6,X7) )
| ~ spl23_11 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f133,plain,
( spl23_9
| spl23_11 ),
inference(avatar_split_clause,[],[f62,f131,f123]) ).
fof(f135,definition,
( spl23_12
<=> ! [X6,X7,X8] :
( ~ g_true_only(X6,X7)
| h_true_only(X6,sK14(X6))
| ~ h_both(X6,X8) ) ),
introduced(definition,[new_symbols(definition,[spl23_12])],[avatar_definition]) ).
fof(f136,plain,
( ! [X8,X6,X7] :
( ~ h_both(X6,X8)
| h_true_only(X6,sK14(X6))
| ~ g_true_only(X6,X7) )
| ~ spl23_12 ),
inference(avatar_component_clause,[],[f135]) ).
fof(f137,plain,
( spl23_9
| spl23_12 ),
inference(avatar_split_clause,[],[f63,f135,f123]) ).
fof(f139,definition,
( spl23_13
<=> ! [X5] : ~ h_true_only(sK12,X5) ),
introduced(definition,[new_symbols(definition,[spl23_13])],[avatar_definition]) ).
fof(f140,plain,
( ! [X5] : ~ h_true_only(sK12,X5)
| ~ spl23_13 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,definition,
( spl23_14
<=> ! [X2] : ~ h_true_only(sK10,X2) ),
introduced(definition,[new_symbols(definition,[spl23_14])],[avatar_definition]) ).
fof(f143,plain,
( ! [X2] : ~ h_true_only(sK10,X2)
| ~ spl23_14 ),
inference(avatar_component_clause,[],[f142]) ).
fof(f144,plain,
( spl23_13
| spl23_14 ),
inference(avatar_split_clause,[],[f64,f142,f139]) ).
fof(f146,definition,
( spl23_15
<=> g_false_only(sK12,sK13) ),
introduced(definition,[new_symbols(definition,[spl23_15])],[avatar_definition]) ).
fof(f148,plain,
( ~ g_false_only(sK12,sK13)
| spl23_15 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f149,plain,
( ~ spl23_15
| spl23_14 ),
inference(avatar_split_clause,[],[f65,f142,f146]) ).
fof(f151,definition,
( spl23_16
<=> g_false_only(sK10,sK11) ),
introduced(definition,[new_symbols(definition,[spl23_16])],[avatar_definition]) ).
fof(f153,plain,
( ~ g_false_only(sK10,sK11)
| spl23_16 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,plain,
( spl23_13
| ~ spl23_16 ),
inference(avatar_split_clause,[],[f66,f151,f139]) ).
fof(f155,plain,
( ~ spl23_15
| ~ spl23_16 ),
inference(avatar_split_clause,[],[f67,f151,f146]) ).
fof(f157,definition,
( spl23_17
<=> ! [X2] :
( h_both(sK7,X2)
| h_false_only(sK7,X2) ) ),
introduced(definition,[new_symbols(definition,[spl23_17])],[avatar_definition]) ).
fof(f158,plain,
( ! [X2] :
( h_both(sK7,X2)
| h_false_only(sK7,X2) )
| ~ spl23_17 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f159,plain,
( ~ spl23_1
| spl23_17 ),
inference(avatar_split_clause,[],[f88,f157,f91]) ).
fof(f161,definition,
( spl23_18
<=> g_both(sK7,sK8) ),
introduced(definition,[new_symbols(definition,[spl23_18])],[avatar_definition]) ).
fof(f163,plain,
( g_both(sK7,sK8)
| ~ spl23_18 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f166,definition,
( spl23_19
<=> ! [X2] : h_false_only(sK7,X2) ),
introduced(definition,[new_symbols(definition,[spl23_19])],[avatar_definition]) ).
fof(f167,plain,
( ! [X2] : h_false_only(sK7,X2)
| ~ spl23_19 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,definition,
( spl23_20
<=> g_true_only(sK7,sK8) ),
introduced(definition,[new_symbols(definition,[spl23_20])],[avatar_definition]) ).
fof(f171,plain,
( g_true_only(sK7,sK8)
| ~ spl23_20 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f172,plain,
( ~ spl23_1
| spl23_19
| spl23_20 ),
inference(avatar_split_clause,[],[f53,f169,f166,f91]) ).
fof(f173,plain,
( ~ spl23_1
| spl23_18
| spl23_20 ),
inference(avatar_split_clause,[],[f54,f169,f161,f91]) ).
fof(f183,definition,
( spl23_23
<=> ! [X0,X5,X2,X1] :
( ~ g_both(X0,X1)
| h_false_only(X0,X5)
| g_true_only(X0,sK6(X0))
| h_true_only(X0,sK5(X0,X1))
| g_false_only(X0,X1)
| ~ h_both(X0,X2) ) ),
introduced(definition,[new_symbols(definition,[spl23_23])],[avatar_definition]) ).
fof(f184,plain,
( ! [X2,X0,X1,X5] :
( h_true_only(X0,sK5(X0,X1))
| h_false_only(X0,X5)
| g_true_only(X0,sK6(X0))
| ~ g_both(X0,X1)
| g_false_only(X0,X1)
| ~ h_both(X0,X2) )
| ~ spl23_23 ),
inference(avatar_component_clause,[],[f183]) ).
fof(f185,plain,
( ~ spl23_2
| spl23_23 ),
inference(avatar_split_clause,[],[f49,f183,f95]) ).
fof(f191,definition,
( spl23_25
<=> ! [X0,X1] :
( ~ g_both(X0,X1)
| ~ h_false_only(X0,sK4(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl23_25])],[avatar_definition]) ).
fof(f192,plain,
( ! [X0,X1] :
( ~ h_false_only(X0,sK4(X0,X1))
| ~ g_both(X0,X1) )
| ~ spl23_25 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f193,plain,
( ~ spl23_9
| spl23_25 ),
inference(avatar_split_clause,[],[f44,f191,f123]) ).
fof(f195,definition,
( spl23_26
<=> ! [X0,X1] :
( ~ g_true_only(X0,X1)
| ~ h_false_only(X0,sK4(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl23_26])],[avatar_definition]) ).
fof(f196,plain,
( ! [X0,X1] :
( ~ h_false_only(X0,sK4(X0,X1))
| ~ g_true_only(X0,X1) )
| ~ spl23_26 ),
inference(avatar_component_clause,[],[f195]) ).
fof(f197,plain,
( ~ spl23_9
| spl23_26 ),
inference(avatar_split_clause,[],[f45,f195,f123]) ).
fof(f199,definition,
( spl23_27
<=> ! [X0,X1] :
( ~ g_true_only(X0,X1)
| ~ h_both(X0,sK4(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl23_27])],[avatar_definition]) ).
fof(f200,plain,
( ! [X0,X1] :
( ~ h_both(X0,sK4(X0,X1))
| ~ g_true_only(X0,X1) )
| ~ spl23_27 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f201,plain,
( ~ spl23_9
| spl23_27 ),
inference(avatar_split_clause,[],[f46,f199,f123]) ).
fof(f202,plain,
( ! [X0] : h_false_only(sK20,X0)
| ~ spl23_3 ),
inference(resolution,[],[f55,f101]) ).
fof(f203,plain,
( spl23_4
| ~ spl23_3 ),
inference(avatar_split_clause,[],[f202,f99,f103]) ).
fof(f207,plain,
( ! [X0] :
( h_both(sK12,X0)
| h_false_only(sK12,X0) )
| ~ spl23_13 ),
inference(resolution,[],[f87,f140]) ).
fof(f209,plain,
( ! [X0,X1] :
( h_false_only(sK12,X0)
| h_true_only(sK12,sK14(sK12))
| ~ g_true_only(sK12,X1) )
| ~ spl23_12
| ~ spl23_13 ),
inference(resolution,[],[f207,f136]) ).
fof(f210,plain,
( ! [X0,X1] :
( h_false_only(sK12,X0)
| ~ g_true_only(sK12,X1) )
| ~ spl23_12
| ~ spl23_13 ),
inference(forward_subsumption_resolution,[],[f209,f140]) ).
fof(f213,definition,
( spl23_28
<=> ! [X1] : ~ g_true_only(sK12,X1) ),
introduced(definition,[new_symbols(definition,[spl23_28])],[avatar_definition]) ).
fof(f214,plain,
( ! [X1] : ~ g_true_only(sK12,X1)
| ~ spl23_28 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,definition,
( spl23_29
<=> ! [X0] : h_false_only(sK12,X0) ),
introduced(definition,[new_symbols(definition,[spl23_29])],[avatar_definition]) ).
fof(f217,plain,
( ! [X0] : h_false_only(sK12,X0)
| ~ spl23_29 ),
inference(avatar_component_clause,[],[f216]) ).
fof(f219,plain,
( ! [X0] :
( h_both(sK10,X0)
| h_false_only(sK10,X0) )
| ~ spl23_14 ),
inference(resolution,[],[f143,f87]) ).
fof(f220,plain,
( ! [X0] :
( h_false_only(sK10,X0)
| h_false(sK10,X0) )
| ~ spl23_14 ),
inference(resolution,[],[f219,f81]) ).
fof(f221,plain,
( ! [X0,X1] :
( h_false_only(sK10,X0)
| h_true_only(sK10,sK14(sK10))
| ~ g_true_only(sK10,X1) )
| ~ spl23_12
| ~ spl23_14 ),
inference(resolution,[],[f219,f136]) ).
fof(f222,plain,
( ! [X0,X1] :
( h_false_only(sK10,X0)
| ~ g_true_only(sK10,X1) )
| ~ spl23_12
| ~ spl23_14 ),
inference(forward_subsumption_resolution,[],[f221,f143]) ).
fof(f223,plain,
( ! [X0] : h_false(sK10,X0)
| ~ spl23_14 ),
inference(forward_subsumption_resolution,[],[f220,f85]) ).
fof(f225,definition,
( spl23_30
<=> ! [X1] : ~ g_true_only(sK10,X1) ),
introduced(definition,[new_symbols(definition,[spl23_30])],[avatar_definition]) ).
fof(f226,plain,
( ! [X1] : ~ g_true_only(sK10,X1)
| ~ spl23_30 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,definition,
( spl23_31
<=> ! [X0] : h_false_only(sK10,X0) ),
introduced(definition,[new_symbols(definition,[spl23_31])],[avatar_definition]) ).
fof(f229,plain,
( ! [X0] : h_false_only(sK10,X0)
| ~ spl23_31 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f230,plain,
( spl23_30
| spl23_31
| ~ spl23_12
| ~ spl23_14 ),
inference(avatar_split_clause,[],[f222,f142,f135,f228,f225]) ).
fof(f231,plain,
( ! [X0] :
( h_both(sK12,X0)
| h_false_only(sK12,X0) )
| ~ spl23_13 ),
inference(resolution,[],[f140,f87]) ).
fof(f239,plain,
( ! [X0] :
( ~ g_true_only(sK12,X0)
| h_false_only(sK12,sK4(sK12,X0)) )
| ~ spl23_13
| ~ spl23_27 ),
inference(resolution,[],[f200,f231]) ).
fof(f241,plain,
( ! [X0] : ~ g_true_only(sK12,X0)
| ~ spl23_13
| ~ spl23_26
| ~ spl23_27 ),
inference(forward_subsumption_resolution,[],[f239,f196]) ).
fof(f242,plain,
( spl23_28
| ~ spl23_13
| ~ spl23_26
| ~ spl23_27 ),
inference(avatar_split_clause,[],[f241,f199,f195,f139,f213]) ).
fof(f243,plain,
( ! [X0,X1] :
( h_true_only(sK12,sK19(sK12))
| ~ h_both(sK12,X0)
| ~ g_both(sK12,X1) )
| ~ spl23_6
| ~ spl23_28 ),
inference(resolution,[],[f214,f110]) ).
fof(f244,plain,
( ! [X0] :
( g_both(sK12,X0)
| g_false_only(sK12,X0) )
| ~ spl23_28 ),
inference(resolution,[],[f214,f77]) ).
fof(f246,plain,
( ! [X0,X1] :
( ~ h_both(sK12,X0)
| ~ g_both(sK12,X1) )
| ~ spl23_6
| ~ spl23_13
| ~ spl23_28 ),
inference(forward_subsumption_resolution,[],[f243,f140]) ).
fof(f248,definition,
( spl23_32
<=> ! [X1] : ~ g_both(sK12,X1) ),
introduced(definition,[new_symbols(definition,[spl23_32])],[avatar_definition]) ).
fof(f249,plain,
( ! [X1] : ~ g_both(sK12,X1)
| ~ spl23_32 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f251,definition,
( spl23_33
<=> ! [X0] : ~ h_both(sK12,X0) ),
introduced(definition,[new_symbols(definition,[spl23_33])],[avatar_definition]) ).
fof(f252,plain,
( ! [X0] : ~ h_both(sK12,X0)
| ~ spl23_33 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f253,plain,
( spl23_32
| spl23_33
| ~ spl23_6
| ~ spl23_13
| ~ spl23_28 ),
inference(avatar_split_clause,[],[f246,f213,f139,f109,f251,f248]) ).
fof(f254,plain,
( ! [X0] : g_false_only(sK12,X0)
| ~ spl23_28
| ~ spl23_32 ),
inference(forward_subsumption_resolution,[],[f244,f249]) ).
fof(f255,plain,
( $false
| spl23_15
| ~ spl23_28
| ~ spl23_32 ),
inference(resolution,[],[f254,f148]) ).
fof(f258,plain,
( spl23_15
| ~ spl23_28
| ~ spl23_32 ),
inference(avatar_contradiction_clause,[],[f255]) ).
fof(f260,plain,
( ! [X0] : h_false_only(sK12,X0)
| ~ spl23_13
| ~ spl23_33 ),
inference(resolution,[],[f252,f231]) ).
fof(f263,plain,
( spl23_29
| ~ spl23_13
| ~ spl23_33 ),
inference(avatar_split_clause,[],[f260,f251,f139,f216]) ).
fof(f270,plain,
( ! [X0] :
( h_false_only(sK7,X0)
| h_false(sK7,X0) )
| ~ spl23_17 ),
inference(resolution,[],[f158,f81]) ).
fof(f271,plain,
( ! [X0] :
( h_false_only(sK7,sK4(sK7,X0))
| ~ g_true_only(sK7,X0) )
| ~ spl23_17
| ~ spl23_27 ),
inference(resolution,[],[f158,f200]) ).
fof(f272,plain,
( ! [X0] : ~ g_true_only(sK7,X0)
| ~ spl23_17
| ~ spl23_26
| ~ spl23_27 ),
inference(forward_subsumption_resolution,[],[f271,f196]) ).
fof(f273,plain,
( ! [X0] : h_false(sK7,X0)
| ~ spl23_17 ),
inference(forward_subsumption_resolution,[],[f270,f85]) ).
fof(f274,plain,
( $false
| ~ spl23_17
| ~ spl23_20
| ~ spl23_26
| ~ spl23_27 ),
inference(resolution,[],[f272,f171]) ).
fof(f277,plain,
( ~ spl23_17
| ~ spl23_20
| ~ spl23_26
| ~ spl23_27 ),
inference(avatar_contradiction_clause,[],[f274]) ).
fof(f282,plain,
( ! [X0] : ~ g_both(sK7,X0)
| ~ spl23_19
| ~ spl23_25 ),
inference(resolution,[],[f167,f192]) ).
fof(f283,plain,
( ! [X0] : ~ g_true_only(sK7,X0)
| ~ spl23_11
| ~ spl23_19 ),
inference(resolution,[],[f167,f132]) ).
fof(f289,plain,
( ! [X0] : ~ h_true_only(sK7,X0)
| ~ spl23_17 ),
inference(resolution,[],[f273,f78]) ).
fof(f305,plain,
( $false
| ~ spl23_18
| ~ spl23_19
| ~ spl23_25 ),
inference(resolution,[],[f282,f163]) ).
fof(f306,plain,
( ~ spl23_18
| ~ spl23_19
| ~ spl23_25 ),
inference(avatar_contradiction_clause,[],[f305]) ).
fof(f307,plain,
( g_both(sK20,sK9(sK20))
| ~ spl23_3 ),
inference(resolution,[],[f101,f57]) ).
fof(f312,plain,
( ! [X0] : ~ g_true_only(sK20,X0)
| ~ spl23_4
| ~ spl23_26 ),
inference(resolution,[],[f104,f196]) ).
fof(f313,plain,
( ! [X0] : ~ g_both(sK20,X0)
| ~ spl23_4
| ~ spl23_25 ),
inference(resolution,[],[f104,f192]) ).
fof(f314,plain,
( ! [X0] : ~ g_true_only(sK20,X0)
| ~ spl23_4
| ~ spl23_11 ),
inference(resolution,[],[f104,f132]) ).
fof(f320,plain,
( ! [X0] :
( h_both(sK20,X0)
| h_false_only(sK20,X0) )
| ~ spl23_5 ),
inference(resolution,[],[f107,f87]) ).
fof(f337,plain,
( $false
| ~ spl23_3
| ~ spl23_4
| ~ spl23_25 ),
inference(forward_subsumption_resolution,[],[f307,f313]) ).
fof(f338,plain,
( ~ spl23_3
| ~ spl23_4
| ~ spl23_25 ),
inference(avatar_contradiction_clause,[],[f337]) ).
fof(f339,plain,
( $false
| ~ spl23_4
| ~ spl23_8
| ~ spl23_11 ),
inference(forward_subsumption_resolution,[],[f120,f314]) ).
fof(f340,plain,
( ~ spl23_4
| ~ spl23_8
| ~ spl23_11 ),
inference(avatar_contradiction_clause,[],[f339]) ).
fof(f341,plain,
( $false
| ~ spl23_4
| ~ spl23_8
| ~ spl23_26 ),
inference(resolution,[],[f312,f120]) ).
fof(f344,plain,
( ~ spl23_4
| ~ spl23_8
| ~ spl23_26 ),
inference(avatar_contradiction_clause,[],[f341]) ).
fof(f356,plain,
( ! [X2,X0,X1] :
( h_false_only(sK12,X0)
| g_true_only(sK12,sK6(sK12))
| ~ g_both(sK12,X1)
| g_false_only(sK12,X1)
| ~ h_both(sK12,X2) )
| ~ spl23_13
| ~ spl23_23 ),
inference(resolution,[],[f184,f140]) ).
fof(f358,plain,
( ! [X2,X0,X1] :
( h_false_only(sK12,X0)
| g_true_only(sK12,sK6(sK12))
| g_false_only(sK12,X1)
| ~ h_both(sK12,X2) )
| ~ spl23_13
| ~ spl23_23
| ~ spl23_28 ),
inference(forward_subsumption_resolution,[],[f356,f244]) ).
fof(f359,plain,
( ! [X2,X0,X1] :
( h_false_only(sK12,X0)
| g_false_only(sK12,X1)
| ~ h_both(sK12,X2) )
| ~ spl23_13
| ~ spl23_23
| ~ spl23_28 ),
inference(forward_subsumption_resolution,[],[f358,f214]) ).
fof(f361,definition,
( spl23_36
<=> ! [X1] : g_false_only(sK12,X1) ),
introduced(definition,[new_symbols(definition,[spl23_36])],[avatar_definition]) ).
fof(f362,plain,
( ! [X1] : g_false_only(sK12,X1)
| ~ spl23_36 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f364,plain,
( $false
| spl23_15
| ~ spl23_36 ),
inference(resolution,[],[f362,f148]) ).
fof(f367,plain,
( spl23_15
| ~ spl23_36 ),
inference(avatar_contradiction_clause,[],[f364]) ).
fof(f368,plain,
( ! [X0] :
( h_both(sK10,X0)
| h_false_only(sK10,X0) )
| ~ spl23_14 ),
inference(resolution,[],[f143,f87]) ).
fof(f369,plain,
( ! [X2,X0,X1] :
( h_false_only(sK10,X0)
| g_true_only(sK10,sK6(sK10))
| ~ g_both(sK10,X1)
| g_false_only(sK10,X1)
| ~ h_both(sK10,X2) )
| ~ spl23_14
| ~ spl23_23 ),
inference(resolution,[],[f143,f184]) ).
fof(f372,definition,
( spl23_37
<=> ! [X2] : ~ h_both(sK10,X2) ),
introduced(definition,[new_symbols(definition,[spl23_37])],[avatar_definition]) ).
fof(f373,plain,
( ! [X2] : ~ h_both(sK10,X2)
| ~ spl23_37 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f375,definition,
( spl23_38
<=> ! [X1] :
( ~ g_both(sK10,X1)
| g_false_only(sK10,X1) ) ),
introduced(definition,[new_symbols(definition,[spl23_38])],[avatar_definition]) ).
fof(f376,plain,
( ! [X1] :
( ~ g_both(sK10,X1)
| g_false_only(sK10,X1) )
| ~ spl23_38 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f378,definition,
( spl23_39
<=> ! [X0] :
( h_false_only(sK10,X0)
| h_both(sK10,X0) ) ),
introduced(definition,[new_symbols(definition,[spl23_39])],[avatar_definition]) ).
fof(f379,plain,
( ! [X0] :
( h_both(sK10,X0)
| h_false_only(sK10,X0) )
| ~ spl23_39 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f382,definition,
( spl23_40
<=> g_true_only(sK10,sK6(sK10)) ),
introduced(definition,[new_symbols(definition,[spl23_40])],[avatar_definition]) ).
fof(f384,plain,
( g_true_only(sK10,sK6(sK10))
| ~ spl23_40 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f385,plain,
( spl23_37
| spl23_38
| spl23_40
| spl23_31
| ~ spl23_14
| ~ spl23_23 ),
inference(avatar_split_clause,[],[f369,f183,f142,f228,f382,f375,f372]) ).
fof(f386,plain,
( spl23_39
| ~ spl23_14 ),
inference(avatar_split_clause,[],[f368,f142,f378]) ).
fof(f387,plain,
( ! [X0] :
( h_both(sK10,X0)
| ~ h_true(sK10,X0) )
| ~ spl23_14 ),
inference(resolution,[],[f223,f83]) ).
fof(f391,plain,
( ! [X0] : ~ h_true(sK10,X0)
| ~ spl23_14
| ~ spl23_37 ),
inference(resolution,[],[f373,f387]) ).
fof(f403,plain,
( ! [X0] :
( ~ h_false(sK10,X0)
| h_false_only(sK10,X0) )
| ~ spl23_14
| ~ spl23_37 ),
inference(resolution,[],[f391,f86]) ).
fof(f406,plain,
( ! [X0] : h_false_only(sK10,X0)
| ~ spl23_14
| ~ spl23_37 ),
inference(forward_subsumption_resolution,[],[f403,f223]) ).
fof(f407,plain,
( spl23_31
| ~ spl23_14
| ~ spl23_37 ),
inference(avatar_split_clause,[],[f406,f372,f142,f228]) ).
fof(f410,plain,
( ! [X0] :
( h_false_only(sK10,sK4(sK10,X0))
| ~ g_true_only(sK10,X0) )
| ~ spl23_27
| ~ spl23_39 ),
inference(resolution,[],[f379,f200]) ).
fof(f411,plain,
( ! [X0] : ~ g_true_only(sK10,X0)
| ~ spl23_26
| ~ spl23_27
| ~ spl23_39 ),
inference(forward_subsumption_resolution,[],[f410,f196]) ).
fof(f413,plain,
( spl23_30
| ~ spl23_26
| ~ spl23_27
| ~ spl23_39 ),
inference(avatar_split_clause,[],[f411,f378,f199,f195,f225]) ).
fof(f414,plain,
( ! [X0] :
( g_both(sK10,X0)
| g_false_only(sK10,X0) )
| ~ spl23_30 ),
inference(resolution,[],[f226,f77]) ).
fof(f416,plain,
( ! [X0] : g_false_only(sK10,X0)
| ~ spl23_30
| ~ spl23_38 ),
inference(forward_subsumption_resolution,[],[f414,f376]) ).
fof(f417,plain,
( $false
| spl23_16
| ~ spl23_30
| ~ spl23_38 ),
inference(resolution,[],[f416,f153]) ).
fof(f420,plain,
( spl23_16
| ~ spl23_30
| ~ spl23_38 ),
inference(avatar_contradiction_clause,[],[f417]) ).
fof(f421,plain,
( $false
| ~ spl23_30
| ~ spl23_40 ),
inference(forward_subsumption_resolution,[],[f384,f226]) ).
fof(f422,plain,
( ~ spl23_30
| ~ spl23_40 ),
inference(avatar_contradiction_clause,[],[f421]) ).
fof(f426,plain,
( ! [X0] : ~ g_both(sK10,X0)
| ~ spl23_25
| ~ spl23_31 ),
inference(resolution,[],[f229,f192]) ).
fof(f431,plain,
( ! [X0] :
( g_false_only(sK10,X0)
| g_false(sK10,X0) )
| ~ spl23_30 ),
inference(resolution,[],[f414,f71]) ).
fof(f432,plain,
( ! [X0] : g_false(sK10,X0)
| ~ spl23_30 ),
inference(forward_subsumption_resolution,[],[f431,f75]) ).
fof(f433,plain,
( ! [X0] :
( g_true(sK10,X0)
| g_false_only(sK10,X0) )
| ~ spl23_30 ),
inference(resolution,[],[f432,f76]) ).
fof(f434,plain,
( ! [X0] :
( ~ g_true(sK10,X0)
| g_both(sK10,X0) )
| ~ spl23_30 ),
inference(resolution,[],[f432,f73]) ).
fof(f441,plain,
( ! [X0] : ~ g_true(sK10,X0)
| ~ spl23_25
| ~ spl23_30
| ~ spl23_31 ),
inference(forward_subsumption_resolution,[],[f434,f426]) ).
fof(f442,plain,
( ! [X0] : g_false_only(sK10,X0)
| ~ spl23_25
| ~ spl23_30
| ~ spl23_31 ),
inference(resolution,[],[f441,f433]) ).
fof(f445,plain,
( $false
| spl23_16
| ~ spl23_25
| ~ spl23_30
| ~ spl23_31 ),
inference(resolution,[],[f442,f153]) ).
fof(f448,plain,
( spl23_16
| ~ spl23_25
| ~ spl23_30
| ~ spl23_31 ),
inference(avatar_contradiction_clause,[],[f445]) ).
fof(f468,plain,
( ! [X0] : ~ g_true_only(sK10,X0)
| ~ spl23_11
| ~ spl23_31 ),
inference(resolution,[],[f132,f229]) ).
fof(f469,plain,
( spl23_30
| ~ spl23_11
| ~ spl23_31 ),
inference(avatar_split_clause,[],[f468,f228,f131,f225]) ).
fof(f489,definition,
( spl23_45
<=> ! [X0] : ~ g_true_only(sK7,X0) ),
introduced(definition,[new_symbols(definition,[spl23_45])],[avatar_definition]) ).
fof(f490,plain,
( ! [X0] : ~ g_true_only(sK7,X0)
| ~ spl23_45 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f492,definition,
( spl23_46
<=> h_true_only(sK7,sK14(sK7)) ),
introduced(definition,[new_symbols(definition,[spl23_46])],[avatar_definition]) ).
fof(f494,plain,
( h_true_only(sK7,sK14(sK7))
| ~ spl23_46 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f496,plain,
( spl23_45
| ~ spl23_11
| ~ spl23_19 ),
inference(avatar_split_clause,[],[f283,f166,f131,f489]) ).
fof(f502,definition,
( spl23_48
<=> ! [X0] : ~ g_both(sK7,X0) ),
introduced(definition,[new_symbols(definition,[spl23_48])],[avatar_definition]) ).
fof(f503,plain,
( ! [X0] : ~ g_both(sK7,X0)
| ~ spl23_48 ),
inference(avatar_component_clause,[],[f502]) ).
fof(f510,plain,
( ! [X0] :
( ~ g_both(sK20,X0)
| g_true_only(sK20,sK16(sK20)) )
| ~ spl23_4
| ~ spl23_10 ),
inference(resolution,[],[f128,f104]) ).
fof(f511,plain,
( ! [X0] :
( ~ g_both(sK10,X0)
| g_true_only(sK10,sK16(sK10)) )
| ~ spl23_10
| ~ spl23_31 ),
inference(resolution,[],[f128,f229]) ).
fof(f513,definition,
( spl23_49
<=> g_true_only(sK10,sK16(sK10)) ),
introduced(definition,[new_symbols(definition,[spl23_49])],[avatar_definition]) ).
fof(f515,plain,
( g_true_only(sK10,sK16(sK10))
| ~ spl23_49 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f517,definition,
( spl23_50
<=> ! [X0] : ~ g_both(sK10,X0) ),
introduced(definition,[new_symbols(definition,[spl23_50])],[avatar_definition]) ).
fof(f518,plain,
( ! [X0] : ~ g_both(sK10,X0)
| ~ spl23_50 ),
inference(avatar_component_clause,[],[f517]) ).
fof(f519,plain,
( spl23_49
| spl23_50
| ~ spl23_10
| ~ spl23_31 ),
inference(avatar_split_clause,[],[f511,f228,f127,f517,f513]) ).
fof(f520,plain,
( ! [X0] : ~ g_both(sK20,X0)
| ~ spl23_4
| ~ spl23_10
| ~ spl23_11 ),
inference(forward_subsumption_resolution,[],[f510,f314]) ).
fof(f533,plain,
( ! [X0] :
( g_both(sK10,X0)
| g_false_only(sK10,X0) )
| ~ spl23_30 ),
inference(resolution,[],[f226,f77]) ).
fof(f550,plain,
( ! [X0] : g_false_only(sK10,X0)
| ~ spl23_30
| ~ spl23_50 ),
inference(forward_subsumption_resolution,[],[f533,f518]) ).
fof(f551,plain,
( $false
| spl23_16
| ~ spl23_30
| ~ spl23_50 ),
inference(resolution,[],[f550,f153]) ).
fof(f554,plain,
( spl23_16
| ~ spl23_30
| ~ spl23_50 ),
inference(avatar_contradiction_clause,[],[f551]) ).
fof(f555,plain,
( $false
| ~ spl23_30
| ~ spl23_49 ),
inference(forward_subsumption_resolution,[],[f515,f226]) ).
fof(f556,plain,
( ~ spl23_30
| ~ spl23_49 ),
inference(avatar_contradiction_clause,[],[f555]) ).
fof(f563,plain,
( ! [X0] : ~ g_true_only(sK12,X0)
| ~ spl23_11
| ~ spl23_29 ),
inference(resolution,[],[f217,f132]) ).
fof(f564,plain,
( ! [X0] :
( ~ g_both(sK12,X0)
| g_true_only(sK12,sK16(sK12)) )
| ~ spl23_10
| ~ spl23_29 ),
inference(resolution,[],[f217,f128]) ).
fof(f565,plain,
( ! [X0] : ~ g_both(sK12,X0)
| ~ spl23_10
| ~ spl23_28
| ~ spl23_29 ),
inference(forward_subsumption_resolution,[],[f564,f214]) ).
fof(f566,plain,
( spl23_32
| ~ spl23_10
| ~ spl23_28
| ~ spl23_29 ),
inference(avatar_split_clause,[],[f565,f216,f213,f127,f248]) ).
fof(f569,definition,
( spl23_51
<=> g_true_only(sK12,sK16(sK12)) ),
introduced(definition,[new_symbols(definition,[spl23_51])],[avatar_definition]) ).
fof(f571,plain,
( g_true_only(sK12,sK16(sK12))
| ~ spl23_51 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f572,plain,
( spl23_51
| spl23_32
| ~ spl23_10
| ~ spl23_29 ),
inference(avatar_split_clause,[],[f564,f216,f127,f248,f569]) ).
fof(f573,plain,
( spl23_28
| ~ spl23_11
| ~ spl23_29 ),
inference(avatar_split_clause,[],[f563,f216,f131,f213]) ).
fof(f587,definition,
( spl23_54
<=> ! [X0] : ~ g_both(sK20,X0) ),
introduced(definition,[new_symbols(definition,[spl23_54])],[avatar_definition]) ).
fof(f588,plain,
( ! [X0] : ~ g_both(sK20,X0)
| ~ spl23_54 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f591,plain,
( ! [X0,X1] :
( h_true_only(sK10,sK19(sK10))
| ~ h_both(sK10,X0)
| ~ g_both(sK10,X1) )
| ~ spl23_6
| ~ spl23_30 ),
inference(resolution,[],[f110,f226]) ).
fof(f593,plain,
( ! [X0,X1] :
( ~ h_both(sK10,X0)
| ~ g_both(sK10,X1) )
| ~ spl23_6
| ~ spl23_14
| ~ spl23_30 ),
inference(forward_subsumption_resolution,[],[f591,f143]) ).
fof(f594,plain,
( spl23_50
| spl23_37
| ~ spl23_6
| ~ spl23_14
| ~ spl23_30 ),
inference(avatar_split_clause,[],[f593,f225,f142,f109,f372,f517]) ).
fof(f599,plain,
( ! [X0] :
( h_true_only(sK20,sK14(sK20))
| ~ g_true_only(sK20,X0) )
| ~ spl23_7
| ~ spl23_12 ),
inference(resolution,[],[f115,f136]) ).
fof(f601,plain,
( ! [X0] : ~ g_true_only(sK20,X0)
| ~ spl23_5
| ~ spl23_7
| ~ spl23_12 ),
inference(forward_subsumption_resolution,[],[f599,f107]) ).
fof(f605,plain,
( $false
| ~ spl23_5
| ~ spl23_7
| ~ spl23_8
| ~ spl23_12 ),
inference(resolution,[],[f601,f120]) ).
fof(f608,plain,
( ~ spl23_5
| ~ spl23_7
| ~ spl23_8
| ~ spl23_12 ),
inference(avatar_contradiction_clause,[],[f605]) ).
fof(f645,plain,
( ! [X0] :
( ~ g_true_only(sK20,X0)
| h_false_only(sK20,sK4(sK20,X0)) )
| ~ spl23_5
| ~ spl23_27 ),
inference(resolution,[],[f200,f320]) ).
fof(f646,plain,
( ! [X0] : ~ g_true_only(sK20,X0)
| ~ spl23_5
| ~ spl23_26
| ~ spl23_27 ),
inference(forward_subsumption_resolution,[],[f645,f196]) ).
fof(f647,plain,
( $false
| ~ spl23_5
| ~ spl23_8
| ~ spl23_26
| ~ spl23_27 ),
inference(resolution,[],[f646,f120]) ).
fof(f650,plain,
( ~ spl23_5
| ~ spl23_8
| ~ spl23_26
| ~ spl23_27 ),
inference(avatar_contradiction_clause,[],[f647]) ).
fof(f658,plain,
( g_both(sK20,sK9(sK20))
| ~ spl23_3 ),
inference(resolution,[],[f101,f57]) ).
fof(f661,plain,
( $false
| ~ spl23_3
| ~ spl23_54 ),
inference(forward_subsumption_resolution,[],[f658,f588]) ).
fof(f662,plain,
( ~ spl23_3
| ~ spl23_54 ),
inference(avatar_contradiction_clause,[],[f661]) ).
fof(f666,plain,
( spl23_54
| ~ spl23_4
| ~ spl23_10
| ~ spl23_11 ),
inference(avatar_split_clause,[],[f520,f131,f127,f103,f587]) ).
fof(f676,plain,
( spl23_28
| spl23_29
| ~ spl23_12
| ~ spl23_13 ),
inference(avatar_split_clause,[],[f210,f139,f135,f216,f213]) ).
fof(f691,plain,
( spl23_33
| spl23_36
| spl23_29
| ~ spl23_13
| ~ spl23_23
| ~ spl23_28 ),
inference(avatar_split_clause,[],[f359,f213,f183,f139,f216,f361,f251]) ).
fof(f706,plain,
( ! [X0,X1] :
( h_true_only(sK7,sK14(sK7))
| ~ g_true_only(sK7,X0)
| h_false_only(sK7,X1) )
| ~ spl23_12
| ~ spl23_17 ),
inference(resolution,[],[f136,f158]) ).
fof(f712,plain,
( $false
| ~ spl23_28
| ~ spl23_51 ),
inference(resolution,[],[f214,f571]) ).
fof(f715,plain,
( ~ spl23_28
| ~ spl23_51 ),
inference(avatar_contradiction_clause,[],[f712]) ).
fof(f736,plain,
( ! [X0] : ~ g_both(sK12,X0)
| ~ spl23_25
| ~ spl23_29 ),
inference(resolution,[],[f192,f217]) ).
fof(f737,plain,
( spl23_32
| ~ spl23_25
| ~ spl23_29 ),
inference(avatar_split_clause,[],[f736,f216,f191,f248]) ).
fof(f739,plain,
( $false
| ~ spl23_20
| ~ spl23_45 ),
inference(forward_subsumption_resolution,[],[f171,f490]) ).
fof(f740,plain,
( ~ spl23_20
| ~ spl23_45 ),
inference(avatar_contradiction_clause,[],[f739]) ).
fof(f746,plain,
( spl23_19
| spl23_45
| spl23_46
| ~ spl23_12
| ~ spl23_17 ),
inference(avatar_split_clause,[],[f706,f157,f135,f492,f489,f166]) ).
fof(f793,plain,
( $false
| ~ spl23_17
| ~ spl23_46 ),
inference(resolution,[],[f289,f494]) ).
fof(f797,plain,
( ~ spl23_17
| ~ spl23_46 ),
inference(avatar_contradiction_clause,[],[f793]) ).
fof(f803,plain,
( $false
| ~ spl23_18
| ~ spl23_48 ),
inference(forward_subsumption_resolution,[],[f163,f503]) ).
fof(f804,plain,
( ~ spl23_18
| ~ spl23_48 ),
inference(avatar_contradiction_clause,[],[f803]) ).
fof(f833,plain,
( ! [X0] :
( ~ g_both(sK7,X0)
| g_true_only(sK7,sK16(sK7)) )
| ~ spl23_10
| ~ spl23_19 ),
inference(resolution,[],[f167,f128]) ).
fof(f834,plain,
( ! [X0] : ~ g_both(sK7,X0)
| ~ spl23_10
| ~ spl23_19
| ~ spl23_45 ),
inference(forward_subsumption_resolution,[],[f833,f490]) ).
fof(f835,plain,
( spl23_48
| ~ spl23_10
| ~ spl23_19
| ~ spl23_45 ),
inference(avatar_split_clause,[],[f834,f489,f166,f127,f502]) ).
cnf(s1,plain,
( spl23_1
| spl23_2
| spl23_3
| spl23_4
| spl23_5
| spl23_6 ),
inference(sat_conversion,[],[f111]) ).
cnf(s2,plain,
( spl23_1
| spl23_2
| spl23_3
| spl23_4
| spl23_6
| spl23_7 ),
inference(sat_conversion,[],[f116]) ).
cnf(s3,plain,
( spl23_1
| spl23_2
| spl23_3
| spl23_6
| spl23_8 ),
inference(sat_conversion,[],[f121]) ).
cnf(s4,plain,
( spl23_9
| spl23_10 ),
inference(sat_conversion,[],[f129]) ).
cnf(s5,plain,
( spl23_9
| spl23_11 ),
inference(sat_conversion,[],[f133]) ).
cnf(s6,plain,
( spl23_9
| spl23_12 ),
inference(sat_conversion,[],[f137]) ).
cnf(s7,plain,
( spl23_13
| spl23_14 ),
inference(sat_conversion,[],[f144]) ).
cnf(s8,plain,
( spl23_14
| ~ spl23_15 ),
inference(sat_conversion,[],[f149]) ).
cnf(s9,plain,
( spl23_13
| ~ spl23_16 ),
inference(sat_conversion,[],[f154]) ).
cnf(s10,plain,
( ~ spl23_15
| ~ spl23_16 ),
inference(sat_conversion,[],[f155]) ).
cnf(s11,plain,
( ~ spl23_1
| spl23_17 ),
inference(sat_conversion,[],[f159]) ).
cnf(s13,plain,
( ~ spl23_1
| spl23_19
| spl23_20 ),
inference(sat_conversion,[],[f172]) ).
cnf(s14,plain,
( ~ spl23_1
| spl23_18
| spl23_20 ),
inference(sat_conversion,[],[f173]) ).
cnf(s17,plain,
( ~ spl23_2
| spl23_23 ),
inference(sat_conversion,[],[f185]) ).
cnf(s19,plain,
( ~ spl23_9
| spl23_25 ),
inference(sat_conversion,[],[f193]) ).
cnf(s20,plain,
( ~ spl23_9
| spl23_26 ),
inference(sat_conversion,[],[f197]) ).
cnf(s21,plain,
( ~ spl23_9
| spl23_27 ),
inference(sat_conversion,[],[f201]) ).
cnf(s22,plain,
( ~ spl23_3
| spl23_4 ),
inference(sat_conversion,[],[f203]) ).
cnf(s24,plain,
( ~ spl23_12
| ~ spl23_14
| spl23_30
| spl23_31 ),
inference(sat_conversion,[],[f230]) ).
cnf(s25,plain,
( ~ spl23_13
| ~ spl23_26
| ~ spl23_27
| spl23_28 ),
inference(sat_conversion,[],[f242]) ).
cnf(s26,plain,
( ~ spl23_6
| ~ spl23_13
| ~ spl23_28
| spl23_32
| spl23_33 ),
inference(sat_conversion,[],[f253]) ).
cnf(s27,plain,
( spl23_15
| ~ spl23_28
| ~ spl23_32 ),
inference(sat_conversion,[],[f258]) ).
cnf(s28,plain,
( ~ spl23_13
| spl23_29
| ~ spl23_33 ),
inference(sat_conversion,[],[f263]) ).
cnf(s29,plain,
( ~ spl23_17
| ~ spl23_20
| ~ spl23_26
| ~ spl23_27 ),
inference(sat_conversion,[],[f277]) ).
cnf(s32,plain,
( ~ spl23_18
| ~ spl23_19
| ~ spl23_25 ),
inference(sat_conversion,[],[f306]) ).
cnf(s35,plain,
( ~ spl23_3
| ~ spl23_4
| ~ spl23_25 ),
inference(sat_conversion,[],[f338]) ).
cnf(s36,plain,
( ~ spl23_4
| ~ spl23_8
| ~ spl23_11 ),
inference(sat_conversion,[],[f340]) ).
cnf(s37,plain,
( ~ spl23_4
| ~ spl23_8
| ~ spl23_26 ),
inference(sat_conversion,[],[f344]) ).
cnf(s39,plain,
( spl23_15
| ~ spl23_36 ),
inference(sat_conversion,[],[f367]) ).
cnf(s41,plain,
( ~ spl23_14
| ~ spl23_23
| spl23_31
| spl23_37
| spl23_38
| spl23_40 ),
inference(sat_conversion,[],[f385]) ).
cnf(s42,plain,
( ~ spl23_14
| spl23_39 ),
inference(sat_conversion,[],[f386]) ).
cnf(s44,plain,
( ~ spl23_14
| spl23_31
| ~ spl23_37 ),
inference(sat_conversion,[],[f407]) ).
cnf(s45,plain,
( ~ spl23_26
| ~ spl23_27
| spl23_30
| ~ spl23_39 ),
inference(sat_conversion,[],[f413]) ).
cnf(s46,plain,
( spl23_16
| ~ spl23_30
| ~ spl23_38 ),
inference(sat_conversion,[],[f420]) ).
cnf(s47,plain,
( ~ spl23_30
| ~ spl23_40 ),
inference(sat_conversion,[],[f422]) ).
cnf(s49,plain,
( spl23_16
| ~ spl23_25
| ~ spl23_30
| ~ spl23_31 ),
inference(sat_conversion,[],[f448]) ).
cnf(s52,plain,
( ~ spl23_11
| spl23_30
| ~ spl23_31 ),
inference(sat_conversion,[],[f469]) ).
cnf(s56,plain,
( ~ spl23_11
| ~ spl23_19
| spl23_45 ),
inference(sat_conversion,[],[f496]) ).
cnf(s60,plain,
( ~ spl23_10
| ~ spl23_31
| spl23_49
| spl23_50 ),
inference(sat_conversion,[],[f519]) ).
cnf(s62,plain,
( spl23_16
| ~ spl23_30
| ~ spl23_50 ),
inference(sat_conversion,[],[f554]) ).
cnf(s63,plain,
( ~ spl23_30
| ~ spl23_49 ),
inference(sat_conversion,[],[f556]) ).
cnf(s64,plain,
( ~ spl23_10
| ~ spl23_28
| ~ spl23_29
| spl23_32 ),
inference(sat_conversion,[],[f566]) ).
cnf(s65,plain,
( ~ spl23_10
| ~ spl23_29
| spl23_32
| spl23_51 ),
inference(sat_conversion,[],[f572]) ).
cnf(s66,plain,
( ~ spl23_11
| spl23_28
| ~ spl23_29 ),
inference(sat_conversion,[],[f573]) ).
cnf(s75,plain,
( ~ spl23_6
| ~ spl23_14
| ~ spl23_30
| spl23_37
| spl23_50 ),
inference(sat_conversion,[],[f594]) ).
cnf(s81,plain,
( ~ spl23_5
| ~ spl23_7
| ~ spl23_8
| ~ spl23_12 ),
inference(sat_conversion,[],[f608]) ).
cnf(s83,plain,
( ~ spl23_5
| ~ spl23_8
| ~ spl23_26
| ~ spl23_27 ),
inference(sat_conversion,[],[f650]) ).
cnf(s87,plain,
( ~ spl23_3
| ~ spl23_54 ),
inference(sat_conversion,[],[f662]) ).
cnf(s89,plain,
( ~ spl23_4
| ~ spl23_10
| ~ spl23_11
| spl23_54 ),
inference(sat_conversion,[],[f666]) ).
cnf(s94,plain,
( ~ spl23_12
| ~ spl23_13
| spl23_28
| spl23_29 ),
inference(sat_conversion,[],[f676]) ).
cnf(s98,plain,
( ~ spl23_13
| ~ spl23_23
| ~ spl23_28
| spl23_29
| spl23_33
| spl23_36 ),
inference(sat_conversion,[],[f691]) ).
cnf(s108,plain,
( ~ spl23_28
| ~ spl23_51 ),
inference(sat_conversion,[],[f715]) ).
cnf(s112,plain,
( ~ spl23_25
| ~ spl23_29
| spl23_32 ),
inference(sat_conversion,[],[f737]) ).
cnf(s113,plain,
( ~ spl23_20
| ~ spl23_45 ),
inference(sat_conversion,[],[f740]) ).
cnf(s117,plain,
( ~ spl23_12
| ~ spl23_17
| spl23_19
| spl23_45
| spl23_46 ),
inference(sat_conversion,[],[f746]) ).
cnf(s124,plain,
( ~ spl23_17
| ~ spl23_46 ),
inference(sat_conversion,[],[f797]) ).
cnf(s126,plain,
( ~ spl23_18
| ~ spl23_48 ),
inference(sat_conversion,[],[f804]) ).
cnf(s137,plain,
( ~ spl23_10
| ~ spl23_19
| ~ spl23_45
| spl23_48 ),
inference(sat_conversion,[],[f835]) ).
cnf(s138,plain,
( spl23_30
| ~ spl23_14
| spl23_9 ),
inference(rat,[],[s24,s52,s6,s5]) ).
cnf(s139,plain,
( spl23_13
| spl23_9
| ~ spl23_6 ),
inference(rat,[],[s44,s60,s75,s62,s63,s138,s7,s9,s4]) ).
cnf(s140,plain,
( spl23_28
| ~ spl23_13
| ~ spl23_11
| ~ spl23_12 ),
inference(rat,[],[s66,s94]) ).
cnf(s141,plain,
( spl23_32
| spl23_9
| ~ spl23_6 ),
inference(rat,[],[s28,s26,s65,s4,s108,s140,s139,s5,s6]) ).
cnf(s142,plain,
( ~ spl23_14
| spl23_9
| ~ spl23_6 ),
inference(rat,[],[s44,s60,s75,s62,s63,s138,s4,s10,s27,s141,s140,s139,s5,s6]) ).
cnf(s143,plain,
( spl23_9
| ~ spl23_6 ),
inference(rat,[],[s8,s142,s27,s141,s140,s139,s5,s6]) ).
cnf(s145,plain,
( spl23_16
| ~ spl23_14
| ~ spl23_6 ),
inference(rat,[],[s44,s75,s49,s62,s19,s45,s42,s21,s20,s143]) ).
cnf(s146,plain,
( spl23_32
| ~ spl23_13
| ~ spl23_6 ),
inference(rat,[],[s28,s26,s112,s19,s25,s21,s20,s143]) ).
cnf(s147,plain,
( ~ spl23_15
| ~ spl23_6 ),
inference(rat,[],[s145,s8,s10]) ).
cnf(s148,plain,
( ~ spl23_13
| ~ spl23_6 ),
inference(rat,[],[s27,s146,s25,s21,s20,s143,s147]) ).
cnf(s149,plain,
~ spl23_6,
inference(rat,[],[s145,s7,s9,s148]) ).
cnf(s150,plain,
( ~ spl23_5
| ~ spl23_7
| ~ spl23_8 ),
inference(rat,[],[s83,s20,s21,s6,s81]) ).
cnf(s151,plain,
( spl23_4
| spl23_3
| spl23_2
| spl23_1 ),
inference(rat,[],[s150,s1,s2,s3,s149]) ).
cnf(s152,plain,
( ~ spl23_4
| ~ spl23_8 ),
inference(rat,[],[s5,s20,s36,s37]) ).
cnf(s153,plain,
( spl23_3
| spl23_2
| spl23_1 ),
inference(rat,[],[s152,s151,s3,s149]) ).
cnf(s154,plain,
~ spl23_3,
inference(rat,[],[s89,s4,s5,s19,s35,s22,s87]) ).
cnf(s155,plain,
( spl23_9
| spl23_28
| ~ spl23_13 ),
inference(rat,[],[s140,s5,s6]) ).
cnf(s156,plain,
( spl23_28
| ~ spl23_13 ),
inference(rat,[],[s25,s20,s21,s155]) ).
cnf(s157,plain,
( spl23_15
| ~ spl23_10
| ~ spl23_13
| ~ spl23_23 ),
inference(rat,[],[s98,s28,s64,s27,s39,s156]) ).
cnf(s158,plain,
( spl23_38
| spl23_40
| ~ spl23_14
| ~ spl23_23
| spl23_31 ),
inference(rat,[],[s44,s41]) ).
cnf(s159,plain,
( spl23_9
| ~ spl23_13
| ~ spl23_23 ),
inference(rat,[],[s158,s60,s46,s62,s47,s63,s138,s8,s10,s157,s4]) ).
cnf(s160,plain,
( spl23_15
| ~ spl23_13
| ~ spl23_23 ),
inference(rat,[],[s98,s28,s112,s27,s39,s156,s19,s159]) ).
cnf(s161,plain,
( ~ spl23_13
| ~ spl23_23 ),
inference(rat,[],[s158,s49,s46,s47,s45,s42,s8,s10,s160,s19,s20,s21,s159]) ).
cnf(s162,plain,
( spl23_9
| ~ spl23_23 ),
inference(rat,[],[s158,s60,s46,s62,s47,s63,s138,s4,s9,s7,s161]) ).
cnf(s163,plain,
~ spl23_23,
inference(rat,[],[s158,s46,s47,s49,s45,s19,s20,s21,s162,s42,s7,s9,s161]) ).
cnf(s164,plain,
~ spl23_2,
inference(rat,[],[s17,s163]) ).
cnf(s165,plain,
spl23_1,
inference(rat,[],[s153,s154,s164]) ).
cnf(s166,plain,
spl23_17,
inference(rat,[],[s11,s165]) ).
cnf(s167,plain,
~ spl23_46,
inference(rat,[],[s124,s166]) ).
cnf(s168,plain,
( spl23_45
| spl23_9 ),
inference(rat,[],[s117,s56,s6,s5,s166,s167]) ).
cnf(s169,plain,
spl23_9,
inference(rat,[],[s137,s126,s13,s14,s113,s168,s4,s165]) ).
cnf(s170,plain,
spl23_27,
inference(rat,[],[s21,s169]) ).
cnf(s171,plain,
spl23_26,
inference(rat,[],[s20,s169]) ).
cnf(s172,plain,
spl23_25,
inference(rat,[],[s19,s169]) ).
cnf(s174,plain,
~ spl23_20,
inference(rat,[],[s29,s170,s166,s171]) ).
cnf(s175,plain,
spl23_18,
inference(rat,[],[s14,s165,s174]) ).
cnf(s176,plain,
spl23_19,
inference(rat,[],[s13,s165,s174]) ).
cnf(s178,plain,
$false,
inference(rat,[],[s32,s172,s175,s176]) ).
fof(f836,plain,
$false,
inference(avatar_sat_refutation,[],[s178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO606+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n005.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 17:54:31 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.99/1.12 % (999288)Detected formulas, will run a generic FOF schedule.
% 2.99/1.12 % (999294)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=3474763110:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.99/1.12 % (999295)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=4040521336:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.99/1.12 % (999293)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=2349845348:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.99/1.12 % (999296)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=723057060:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.99/1.12 % (999298)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1530149293:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.99/1.12 % (999297)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=10787590:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.99/1.12 % (999299)dis-21_1_sil=8000:lcm=predicate:random_seed=880927847: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)
% 2.99/1.12 % (999296)Refutation not found, incomplete strategy
% 2.99/1.12 % (999296)------------------------------
% 2.99/1.12 % (999296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.99/1.12 % (999296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.99/1.12 % (999296)CaDiCaL version: 2.1.3
% 2.99/1.12 % (999296)Termination reason: Refutation not found, incomplete strategy
% 2.99/1.12 % (999296)Time elapsed: 0.006 s
% 2.99/1.12 % (999296)Peak memory usage: 88 MB
% 2.99/1.12 % (999296)Instructions burned: 7 (million)
% 2.99/1.12 % (999298)First to succeed.
% 2.99/1.12 % (999299)Also succeeded, but the first one will report.
% 2.99/1.12 % (999298)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-999288"
% 2.99/1.12 % (999297)Also succeeded, but the first one will report.
% 2.99/1.12 % (999296)------------------------------
% 2.99/1.12 % (999296)------------------------------
% 2.99/1.12 % (999298)Refutation found. Thanks to Tanya!
% 2.99/1.12 % SZS status Theorem for theBenchmark
% 2.99/1.12 % SZS output start Proof for theBenchmark
% See solution above
% 3.75/1.22 % (999298)------------------------------
% 3.75/1.22 % (999298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.75/1.22 % (999298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.75/1.22 % (999298)CaDiCaL version: 2.1.3
% 3.75/1.22 % (999298)Termination reason: Refutation
% 3.75/1.22 % (999298)Time elapsed: 0.018 s
% 3.75/1.22 % (999298)Peak memory usage: 89 MB
% 3.75/1.22 % (999298)Instructions burned: 25 (million)
% 3.75/1.22 % (999298)------------------------------
% 3.75/1.22 % (999298)------------------------------
% 3.75/1.22 % (999288)Success in time 0.449 s
% 3.75/1.22 % Vampire exiting
%------------------------------------------------------------------------------