%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO606+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:32:02 PM UTC 2026
% Result : Theorem 0.19s 0.27s
% Output : Refutation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% 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/sandbox2/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(f3,axiom,
! [X0,X1] :
( g_true_only(X0,X1)
<=> ( g_true(X0,X1)
& ~ g_false(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',true_only_g) ).
fof(f4,axiom,
! [X0,X1] :
( g_both(X0,X1)
<=> ( g_true(X0,X1)
& g_false(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',both_g) ).
fof(f6,axiom,
! [X0,X1] :
( g_true_only(X0,X1)
| g_both(X0,X1)
| g_false_only(X0,X1) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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(f15,plain,
! [X31,X32,X30] :
( g_false_only(X30,X31)
| h_true_only(X30,sK19(X30,X31))
| ~ h_both(X30,X32)
| ~ g_both(X30,X31)
| ~ sP13(X31,X30) ),
inference(cnf_transformation,[],[f12]) ).
fof(f17,plain,
! [X34,X35,X30] :
( ~ sP12(X34,X30)
| g_true_only(X30,X34)
| h_false_only(X30,X35) ),
inference(cnf_transformation,[],[f12]) ).
fof(f18,plain,
! [X38,X36,X37] :
( ~ sP11(X38,X37,X36)
| h_both(X36,X38)
| h_false_only(X36,X38) ),
inference(cnf_transformation,[],[f12]) ).
fof(f19,plain,
! [X8,X6,X7,X14,X15] :
( ~ h_false_only(X14,sK6(X14,X15))
| ~ g_both(X14,X15)
| h_true_only(X6,sK21(X6))
| ~ h_both(X6,X8)
| ~ g_true_only(X6,X7) ),
inference(cnf_transformation,[],[f12]) ).
fof(f20,plain,
! [X8,X6,X7,X14,X15] :
( ~ h_both(X14,sK6(X14,X15))
| ~ g_true_only(X14,X15)
| h_true_only(X6,sK21(X6))
| ~ h_both(X6,X8)
| ~ g_true_only(X6,X7) ),
inference(cnf_transformation,[],[f12]) ).
fof(f21,plain,
! [X8,X6,X7,X14,X15] :
( ~ h_false_only(X14,sK6(X14,X15))
| ~ g_true_only(X14,X15)
| h_true_only(X6,sK21(X6))
| ~ h_both(X6,X8)
| ~ g_true_only(X6,X7) ),
inference(cnf_transformation,[],[f12]) ).
fof(f24,plain,
! [X6,X7,X14,X15] :
( ~ h_false_only(X14,sK6(X14,X15))
| ~ g_true_only(X14,X15)
| ~ h_false_only(X6,sK18(X6))
| ~ g_true_only(X6,X7) ),
inference(cnf_transformation,[],[f12]) ).
fof(f25,plain,
! [X6,X7,X14,X15] :
( ~ h_both(X14,sK6(X14,X15))
| ~ g_true_only(X14,X15)
| ~ h_false_only(X6,sK18(X6))
| ~ g_true_only(X6,X7) ),
inference(cnf_transformation,[],[f12]) ).
fof(f26,plain,
! [X31,X38,X29,X18,X26,X17,X25,X30,X20] :
( h_false_only(sK0,X38)
| sP11(X38,sK1,sK0)
| sP12(sK7(X30),X30)
| sP13(X31,X30)
| h_false_only(sK2,X29)
| h_false_only(sK2,X26)
| ~ h_true_only(sK2,X25)
| h_true_only(X17,sK8(X17))
| ~ h_both(X17,X20)
| g_true_only(X17,sK9(X17))
| ~ g_both(X17,X18) ),
inference(cnf_transformation,[],[f12]) ).
fof(f28,plain,
! [X31,X38,X29,X18,X26,X17,X25,X30,X20] :
( g_both(sK0,sK1)
| sP11(X38,sK1,sK0)
| sP12(sK7(X30),X30)
| sP13(X31,X30)
| h_false_only(sK2,X29)
| h_false_only(sK2,X26)
| ~ h_true_only(sK2,X25)
| h_true_only(X17,sK8(X17))
| ~ h_both(X17,X20)
| g_true_only(X17,sK9(X17))
| ~ g_both(X17,X18) ),
inference(cnf_transformation,[],[f12]) ).
fof(f29,plain,
! [X31,X38,X29,X18,X26,X17,X30,X20] :
( g_both(sK0,sK1)
| sP11(X38,sK1,sK0)
| sP12(sK7(X30),X30)
| sP13(X31,X30)
| h_false_only(sK2,X29)
| h_false_only(sK2,X26)
| h_both(sK2,sK20)
| h_true_only(X17,sK8(X17))
| ~ h_both(X17,X20)
| g_true_only(X17,sK9(X17))
| ~ g_both(X17,X18) ),
inference(cnf_transformation,[],[f12]) ).
fof(f38,plain,
! [X38,X36,X37] :
( ~ sP11(X38,X37,X36)
| g_true_only(X36,X37) ),
inference(cnf_transformation,[],[f12]) ).
fof(f39,plain,
! [X6,X7,X14,X15] :
( ~ h_false_only(X14,sK6(X14,X15))
| ~ g_both(X14,X15)
| ~ h_false_only(X6,sK18(X6))
| ~ g_true_only(X6,X7) ),
inference(cnf_transformation,[],[f12]) ).
fof(f40,plain,
! [X11,X6,X14,X15] :
( ~ h_false_only(X14,sK6(X14,X15))
| ~ g_both(X14,X15)
| ~ h_false_only(X6,sK16(X6))
| g_true_only(X6,sK17(X6))
| ~ g_both(X6,X11) ),
inference(cnf_transformation,[],[f12]) ).
fof(f41,plain,
! [X31,X38,X29,X18,X17,X30,X20] :
( h_false_only(sK0,X38)
| sP11(X38,sK1,sK0)
| sP12(sK7(X30),X30)
| sP13(X31,X30)
| h_false_only(sK2,X29)
| g_true_only(sK2,sK15)
| h_true_only(X17,sK8(X17))
| ~ h_both(X17,X20)
| g_true_only(X17,sK9(X17))
| ~ g_both(X17,X18) ),
inference(cnf_transformation,[],[f12]) ).
fof(f42,plain,
! [X31,X38,X29,X18,X17,X30,X20] :
( g_both(sK0,sK1)
| sP11(X38,sK1,sK0)
| sP12(sK7(X30),X30)
| sP13(X31,X30)
| h_false_only(sK2,X29)
| g_true_only(sK2,sK15)
| h_true_only(X17,sK8(X17))
| ~ h_both(X17,X20)
| g_true_only(X17,sK9(X17))
| ~ g_both(X17,X18) ),
inference(cnf_transformation,[],[f12]) ).
fof(f45,plain,
! [X31,X38,X18,X17,X30,X20] :
( h_false_only(sK0,X38)
| sP11(X38,sK1,sK0)
| sP12(sK7(X30),X30)
| sP13(X31,X30)
| g_both(sK2,sK14)
| g_true_only(sK2,sK15)
| h_true_only(X17,sK8(X17))
| ~ h_both(X17,X20)
| g_true_only(X17,sK9(X17))
| ~ g_both(X17,X18) ),
inference(cnf_transformation,[],[f12]) ).
fof(f46,plain,
! [X31,X38,X18,X17,X30,X20] :
( g_both(sK0,sK1)
| sP11(X38,sK1,sK0)
| sP12(sK7(X30),X30)
| sP13(X31,X30)
| g_both(sK2,sK14)
| g_true_only(sK2,sK15)
| h_true_only(X17,sK8(X17))
| ~ h_both(X17,X20)
| g_true_only(X17,sK9(X17))
| ~ g_both(X17,X18) ),
inference(cnf_transformation,[],[f12]) ).
fof(f47,plain,
! [X5] :
( ~ h_true_only(sK3,X5)
| ~ g_false_only(sK5,sK10) ),
inference(cnf_transformation,[],[f12]) ).
fof(f48,plain,
( ~ g_false_only(sK3,sK4)
| ~ g_false_only(sK5,sK10) ),
inference(cnf_transformation,[],[f12]) ).
fof(f49,plain,
! [X2,X5] :
( ~ h_true_only(sK3,X5)
| ~ h_true_only(sK5,X2) ),
inference(cnf_transformation,[],[f12]) ).
fof(f50,plain,
! [X2] :
( ~ g_false_only(sK3,sK4)
| ~ h_true_only(sK5,X2) ),
inference(cnf_transformation,[],[f12]) ).
fof(f51,plain,
! [X0,X1] :
( ~ g_false(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f54,plain,
! [X0,X1] :
( g_false(X0,X1)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f60,plain,
! [X0,X1] :
( g_false_only(X0,X1)
| g_both(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f61,plain,
! [X0,X1] :
( ~ h_false(X0,X1)
| ~ h_true_only(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f62,plain,
! [X0,X1] :
( h_true(X0,X1)
| ~ h_true_only(X0,X1) ),
inference(cnf_transformation,[],[f7]) ).
fof(f64,plain,
! [X0,X1] :
( h_false(X0,X1)
| ~ h_both(X0,X1) ),
inference(cnf_transformation,[],[f8]) ).
fof(f67,plain,
! [X0,X1] :
( ~ h_true(X0,X1)
| ~ h_false_only(X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
fof(f70,plain,
! [X0,X1] :
( h_true_only(X0,X1)
| h_both(X0,X1)
| h_false_only(X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
fof(f72,definition,
( spl22_1
<=> ! [X6,X7,X8] :
( h_true_only(X6,sK21(X6))
| ~ g_true_only(X6,X7)
| ~ h_both(X6,X8) ) ),
introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition]) ).
fof(f73,plain,
( ! [X8,X6,X7] :
( h_true_only(X6,sK21(X6))
| ~ g_true_only(X6,X7)
| ~ h_both(X6,X8) )
| ~ spl22_1 ),
inference(avatar_component_clause,[],[f72]) ).
fof(f75,definition,
( spl22_2
<=> ! [X14,X15] :
( ~ h_false_only(X14,sK6(X14,X15))
| ~ g_both(X14,X15) ) ),
introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).
fof(f76,plain,
( ! [X14,X15] :
( ~ g_both(X14,X15)
| ~ h_false_only(X14,sK6(X14,X15)) )
| ~ spl22_2 ),
inference(avatar_component_clause,[],[f75]) ).
fof(f77,plain,
( spl22_1
| spl22_2 ),
inference(avatar_split_clause,[],[f19,f75,f72]) ).
fof(f79,definition,
( spl22_3
<=> ! [X14,X15] :
( ~ h_both(X14,sK6(X14,X15))
| ~ g_true_only(X14,X15) ) ),
introduced(definition,[new_symbols(definition,[spl22_3])],[avatar_definition]) ).
fof(f80,plain,
( ! [X14,X15] :
( ~ h_both(X14,sK6(X14,X15))
| ~ g_true_only(X14,X15) )
| ~ spl22_3 ),
inference(avatar_component_clause,[],[f79]) ).
fof(f81,plain,
( spl22_1
| spl22_3 ),
inference(avatar_split_clause,[],[f20,f79,f72]) ).
fof(f83,definition,
( spl22_4
<=> ! [X14,X15] :
( ~ h_false_only(X14,sK6(X14,X15))
| ~ g_true_only(X14,X15) ) ),
introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition]) ).
fof(f84,plain,
( ! [X14,X15] :
( ~ h_false_only(X14,sK6(X14,X15))
| ~ g_true_only(X14,X15) )
| ~ spl22_4 ),
inference(avatar_component_clause,[],[f83]) ).
fof(f85,plain,
( spl22_1
| spl22_4 ),
inference(avatar_split_clause,[],[f21,f83,f72]) ).
fof(f87,definition,
( spl22_5
<=> ! [X6,X11] :
( ~ h_false_only(X6,sK16(X6))
| ~ g_both(X6,X11)
| g_true_only(X6,sK17(X6)) ) ),
introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition]) ).
fof(f88,plain,
( ! [X11,X6] :
( ~ g_both(X6,X11)
| ~ h_false_only(X6,sK16(X6))
| g_true_only(X6,sK17(X6)) )
| ~ spl22_5 ),
inference(avatar_component_clause,[],[f87]) ).
fof(f92,definition,
( spl22_6
<=> ! [X6,X7] :
( ~ h_false_only(X6,sK18(X6))
| ~ g_true_only(X6,X7) ) ),
introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition]) ).
fof(f93,plain,
( ! [X6,X7] :
( ~ h_false_only(X6,sK18(X6))
| ~ g_true_only(X6,X7) )
| ~ spl22_6 ),
inference(avatar_component_clause,[],[f92]) ).
fof(f94,plain,
( spl22_6
| spl22_4 ),
inference(avatar_split_clause,[],[f24,f83,f92]) ).
fof(f95,plain,
( spl22_6
| spl22_3 ),
inference(avatar_split_clause,[],[f25,f79,f92]) ).
fof(f97,definition,
( spl22_7
<=> ! [X20,X18,X17] :
( h_true_only(X17,sK8(X17))
| ~ g_both(X17,X18)
| g_true_only(X17,sK9(X17))
| ~ h_both(X17,X20) ) ),
introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition]) ).
fof(f98,plain,
( ! [X18,X17,X20] :
( h_true_only(X17,sK8(X17))
| ~ g_both(X17,X18)
| g_true_only(X17,sK9(X17))
| ~ h_both(X17,X20) )
| ~ spl22_7 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,definition,
( spl22_8
<=> ! [X25] : ~ h_true_only(sK2,X25) ),
introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition]) ).
fof(f101,plain,
( ! [X25] : ~ h_true_only(sK2,X25)
| ~ spl22_8 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f103,definition,
( spl22_9
<=> ! [X26] : h_false_only(sK2,X26) ),
introduced(definition,[new_symbols(definition,[spl22_9])],[avatar_definition]) ).
fof(f104,plain,
( ! [X26] : h_false_only(sK2,X26)
| ~ spl22_9 ),
inference(avatar_component_clause,[],[f103]) ).
fof(f106,definition,
( spl22_10
<=> ! [X30,X31] :
( sP12(sK7(X30),X30)
| sP13(X31,X30) ) ),
introduced(definition,[new_symbols(definition,[spl22_10])],[avatar_definition]) ).
fof(f107,plain,
( ! [X31,X30] :
( sP13(X31,X30)
| sP12(sK7(X30),X30) )
| ~ spl22_10 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f109,definition,
( spl22_11
<=> ! [X38] :
( h_false_only(sK0,X38)
| sP11(X38,sK1,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl22_11])],[avatar_definition]) ).
fof(f110,plain,
( ! [X38] :
( sP11(X38,sK1,sK0)
| h_false_only(sK0,X38) )
| ~ spl22_11 ),
inference(avatar_component_clause,[],[f109]) ).
fof(f111,plain,
( spl22_7
| spl22_8
| spl22_9
| spl22_9
| spl22_10
| spl22_11 ),
inference(avatar_split_clause,[],[f26,f109,f106,f103,f103,f100,f97]) ).
fof(f113,definition,
( spl22_12
<=> h_both(sK2,sK20) ),
introduced(definition,[new_symbols(definition,[spl22_12])],[avatar_definition]) ).
fof(f115,plain,
( h_both(sK2,sK20)
| ~ spl22_12 ),
inference(avatar_component_clause,[],[f113]) ).
fof(f118,definition,
( spl22_13
<=> ! [X38] : sP11(X38,sK1,sK0) ),
introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).
fof(f119,plain,
( ! [X38] : sP11(X38,sK1,sK0)
| ~ spl22_13 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f121,definition,
( spl22_14
<=> g_both(sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl22_14])],[avatar_definition]) ).
fof(f123,plain,
( g_both(sK0,sK1)
| ~ spl22_14 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f124,plain,
( spl22_7
| spl22_8
| spl22_9
| spl22_9
| spl22_10
| spl22_13
| spl22_14 ),
inference(avatar_split_clause,[],[f28,f121,f118,f106,f103,f103,f100,f97]) ).
fof(f125,plain,
( spl22_7
| spl22_12
| spl22_9
| spl22_9
| spl22_10
| spl22_13
| spl22_14 ),
inference(avatar_split_clause,[],[f29,f121,f118,f106,f103,f103,f113,f97]) ).
fof(f127,definition,
( spl22_15
<=> ! [X28] : ~ g_true_only(sK2,X28) ),
introduced(definition,[new_symbols(definition,[spl22_15])],[avatar_definition]) ).
fof(f128,plain,
( ! [X28] : ~ g_true_only(sK2,X28)
| ~ spl22_15 ),
inference(avatar_component_clause,[],[f127]) ).
fof(f134,definition,
( spl22_16
<=> g_both(sK2,sK14) ),
introduced(definition,[new_symbols(definition,[spl22_16])],[avatar_definition]) ).
fof(f136,plain,
( g_both(sK2,sK14)
| ~ spl22_16 ),
inference(avatar_component_clause,[],[f134]) ).
fof(f141,plain,
( spl22_6
| spl22_2 ),
inference(avatar_split_clause,[],[f39,f75,f92]) ).
fof(f142,plain,
( spl22_5
| spl22_2 ),
inference(avatar_split_clause,[],[f40,f75,f87]) ).
fof(f144,definition,
( spl22_17
<=> g_true_only(sK2,sK15) ),
introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition]) ).
fof(f146,plain,
( g_true_only(sK2,sK15)
| ~ spl22_17 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f147,plain,
( spl22_7
| spl22_17
| spl22_9
| spl22_10
| spl22_11 ),
inference(avatar_split_clause,[],[f41,f109,f106,f103,f144,f97]) ).
fof(f148,plain,
( spl22_7
| spl22_17
| spl22_9
| spl22_10
| spl22_13
| spl22_14 ),
inference(avatar_split_clause,[],[f42,f121,f118,f106,f103,f144,f97]) ).
fof(f151,plain,
( spl22_7
| spl22_17
| spl22_16
| spl22_10
| spl22_11 ),
inference(avatar_split_clause,[],[f45,f109,f106,f134,f144,f97]) ).
fof(f152,plain,
( spl22_7
| spl22_17
| spl22_16
| spl22_10
| spl22_13
| spl22_14 ),
inference(avatar_split_clause,[],[f46,f121,f118,f106,f134,f144,f97]) ).
fof(f154,definition,
( spl22_18
<=> g_false_only(sK5,sK10) ),
introduced(definition,[new_symbols(definition,[spl22_18])],[avatar_definition]) ).
fof(f156,plain,
( ~ g_false_only(sK5,sK10)
| spl22_18 ),
inference(avatar_component_clause,[],[f154]) ).
fof(f158,definition,
( spl22_19
<=> ! [X5] : ~ h_true_only(sK3,X5) ),
introduced(definition,[new_symbols(definition,[spl22_19])],[avatar_definition]) ).
fof(f159,plain,
( ! [X5] : ~ h_true_only(sK3,X5)
| ~ spl22_19 ),
inference(avatar_component_clause,[],[f158]) ).
fof(f160,plain,
( ~ spl22_18
| spl22_19 ),
inference(avatar_split_clause,[],[f47,f158,f154]) ).
fof(f162,definition,
( spl22_20
<=> g_false_only(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl22_20])],[avatar_definition]) ).
fof(f164,plain,
( ~ g_false_only(sK3,sK4)
| spl22_20 ),
inference(avatar_component_clause,[],[f162]) ).
fof(f165,plain,
( ~ spl22_18
| ~ spl22_20 ),
inference(avatar_split_clause,[],[f48,f162,f154]) ).
fof(f167,definition,
( spl22_21
<=> ! [X2] : ~ h_true_only(sK5,X2) ),
introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition]) ).
fof(f168,plain,
( ! [X2] : ~ h_true_only(sK5,X2)
| ~ spl22_21 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f169,plain,
( spl22_21
| spl22_19 ),
inference(avatar_split_clause,[],[f49,f158,f167]) ).
fof(f170,plain,
( spl22_21
| ~ spl22_20 ),
inference(avatar_split_clause,[],[f50,f162,f167]) ).
fof(f171,plain,
( ! [X0,X1] :
( ~ g_both(sK3,X0)
| g_true_only(sK3,sK9(sK3))
| ~ h_both(sK3,X1) )
| ~ spl22_7
| ~ spl22_19 ),
inference(resolution,[],[f98,f159]) ).
fof(f173,definition,
( spl22_22
<=> ! [X1] : ~ h_both(sK3,X1) ),
introduced(definition,[new_symbols(definition,[spl22_22])],[avatar_definition]) ).
fof(f174,plain,
( ! [X1] : ~ h_both(sK3,X1)
| ~ spl22_22 ),
inference(avatar_component_clause,[],[f173]) ).
fof(f176,definition,
( spl22_23
<=> g_true_only(sK3,sK9(sK3)) ),
introduced(definition,[new_symbols(definition,[spl22_23])],[avatar_definition]) ).
fof(f178,plain,
( g_true_only(sK3,sK9(sK3))
| ~ spl22_23 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f180,definition,
( spl22_24
<=> ! [X0] : ~ g_both(sK3,X0) ),
introduced(definition,[new_symbols(definition,[spl22_24])],[avatar_definition]) ).
fof(f181,plain,
( ! [X0] : ~ g_both(sK3,X0)
| ~ spl22_24 ),
inference(avatar_component_clause,[],[f180]) ).
fof(f183,plain,
( ! [X0] :
( h_true_only(sK3,sK19(sK3,sK4))
| ~ h_both(sK3,X0)
| ~ g_both(sK3,sK4)
| ~ sP13(sK4,sK3) )
| spl22_20 ),
inference(resolution,[],[f15,f164]) ).
fof(f184,plain,
( ! [X0] :
( ~ h_both(sK3,X0)
| ~ g_both(sK3,sK4)
| ~ sP13(sK4,sK3) )
| ~ spl22_19
| spl22_20 ),
inference(forward_subsumption_resolution,[],[f183,f159]) ).
fof(f186,definition,
( spl22_25
<=> sP13(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl22_25])],[avatar_definition]) ).
fof(f188,plain,
( ~ sP13(sK4,sK3)
| spl22_25 ),
inference(avatar_component_clause,[],[f186]) ).
fof(f190,definition,
( spl22_26
<=> g_both(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl22_26])],[avatar_definition]) ).
fof(f191,plain,
( g_both(sK3,sK4)
| ~ spl22_26 ),
inference(avatar_component_clause,[],[f190]) ).
fof(f193,plain,
( ~ spl22_25
| ~ spl22_26
| spl22_22
| ~ spl22_19
| spl22_20 ),
inference(avatar_split_clause,[],[f184,f162,f158,f173,f190,f186]) ).
fof(f194,plain,
( sP12(sK7(sK3),sK3)
| ~ spl22_10
| spl22_25 ),
inference(resolution,[],[f188,f107]) ).
fof(f195,plain,
( ! [X0] :
( g_true_only(sK3,sK7(sK3))
| h_false_only(sK3,X0) )
| ~ spl22_10
| spl22_25 ),
inference(resolution,[],[f194,f17]) ).
fof(f203,definition,
( spl22_28
<=> g_true_only(sK3,sK7(sK3)) ),
introduced(definition,[new_symbols(definition,[spl22_28])],[avatar_definition]) ).
fof(f205,plain,
( g_true_only(sK3,sK7(sK3))
| ~ spl22_28 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f208,definition,
( spl22_29
<=> ! [X0] : h_false_only(sK3,X0) ),
introduced(definition,[new_symbols(definition,[spl22_29])],[avatar_definition]) ).
fof(f209,plain,
( ! [X0] : h_false_only(sK3,X0)
| ~ spl22_29 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f211,plain,
( ! [X0] :
( h_both(sK0,X0)
| h_false_only(sK0,X0) )
| ~ spl22_13 ),
inference(resolution,[],[f119,f18]) ).
fof(f212,plain,
( g_true_only(sK0,sK1)
| ~ spl22_13 ),
inference(resolution,[],[f119,f38]) ).
fof(f213,plain,
( ! [X0] :
( h_false_only(sK0,X0)
| h_both(sK0,X0)
| h_false_only(sK0,X0) )
| ~ spl22_11 ),
inference(resolution,[],[f110,f18]) ).
fof(f215,plain,
( ! [X0] :
( h_both(sK0,X0)
| h_false_only(sK0,X0) )
| ~ spl22_11 ),
inference(duplicate_literal_removal,[],[f213]) ).
fof(f216,plain,
( ! [X0] :
( h_false_only(sK0,sK6(sK0,X0))
| ~ g_true_only(sK0,X0) )
| ~ spl22_3
| ~ spl22_13 ),
inference(resolution,[],[f211,f80]) ).
fof(f217,plain,
( ! [X0] : ~ g_true_only(sK0,X0)
| ~ spl22_3
| ~ spl22_4
| ~ spl22_13 ),
inference(forward_subsumption_resolution,[],[f216,f84]) ).
fof(f218,plain,
! [X0,X1] :
( ~ g_both(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(resolution,[],[f54,f51]) ).
fof(f219,plain,
( $false
| ~ spl22_3
| ~ spl22_4
| ~ spl22_13 ),
inference(resolution,[],[f217,f212]) ).
fof(f220,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_13 ),
inference(avatar_contradiction_clause,[],[f219]) ).
fof(f222,definition,
( spl22_30
<=> g_true_only(sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl22_30])],[avatar_definition]) ).
fof(f223,plain,
( ~ g_true_only(sK0,sK1)
| spl22_30 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f224,plain,
( g_true_only(sK0,sK1)
| ~ spl22_30 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f226,definition,
( spl22_31
<=> ! [X0] : h_false_only(sK0,X0) ),
introduced(definition,[new_symbols(definition,[spl22_31])],[avatar_definition]) ).
fof(f227,plain,
( ! [X0] : h_false_only(sK0,X0)
| ~ spl22_31 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f229,plain,
( ~ h_false_only(sK0,sK6(sK0,sK1))
| ~ spl22_2
| ~ spl22_14 ),
inference(resolution,[],[f123,f76]) ).
fof(f230,plain,
( ! [X0] :
( h_true_only(sK5,sK19(sK5,sK10))
| ~ h_both(sK5,X0)
| ~ g_both(sK5,sK10)
| ~ sP13(sK10,sK5) )
| spl22_18 ),
inference(resolution,[],[f156,f15]) ).
fof(f231,plain,
( ! [X0] :
( ~ h_both(sK5,X0)
| ~ g_both(sK5,sK10)
| ~ sP13(sK10,sK5) )
| spl22_18
| ~ spl22_21 ),
inference(forward_subsumption_resolution,[],[f230,f168]) ).
fof(f233,definition,
( spl22_32
<=> sP13(sK10,sK5) ),
introduced(definition,[new_symbols(definition,[spl22_32])],[avatar_definition]) ).
fof(f235,plain,
( ~ sP13(sK10,sK5)
| spl22_32 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f237,definition,
( spl22_33
<=> g_both(sK5,sK10) ),
introduced(definition,[new_symbols(definition,[spl22_33])],[avatar_definition]) ).
fof(f238,plain,
( g_both(sK5,sK10)
| ~ spl22_33 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f241,definition,
( spl22_34
<=> ! [X0] : ~ h_both(sK5,X0) ),
introduced(definition,[new_symbols(definition,[spl22_34])],[avatar_definition]) ).
fof(f242,plain,
( ! [X0] : ~ h_both(sK5,X0)
| ~ spl22_34 ),
inference(avatar_component_clause,[],[f241]) ).
fof(f243,plain,
( ~ spl22_32
| ~ spl22_33
| spl22_34
| spl22_18
| ~ spl22_21 ),
inference(avatar_split_clause,[],[f231,f167,f154,f241,f237,f233]) ).
fof(f246,definition,
( spl22_35
<=> g_true_only(sK5,sK9(sK5)) ),
introduced(definition,[new_symbols(definition,[spl22_35])],[avatar_definition]) ).
fof(f248,plain,
( g_true_only(sK5,sK9(sK5))
| ~ spl22_35 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f250,definition,
( spl22_36
<=> ! [X0] : ~ g_both(sK5,X0) ),
introduced(definition,[new_symbols(definition,[spl22_36])],[avatar_definition]) ).
fof(f251,plain,
( ! [X0] : ~ g_both(sK5,X0)
| ~ spl22_36 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f253,plain,
( spl22_22
| spl22_23
| spl22_24
| ~ spl22_7
| ~ spl22_19 ),
inference(avatar_split_clause,[],[f171,f158,f97,f180,f176,f173]) ).
fof(f258,plain,
! [X0,X1] :
( ~ h_true_only(X0,X1)
| ~ h_both(X0,X1) ),
inference(resolution,[],[f64,f61]) ).
fof(f260,plain,
! [X0,X1] :
( ~ h_true_only(X0,X1)
| ~ h_false_only(X0,X1) ),
inference(resolution,[],[f67,f62]) ).
fof(f262,plain,
( ~ g_true_only(sK0,sK1)
| ~ spl22_14 ),
inference(resolution,[],[f218,f123]) ).
fof(f263,plain,
( ~ spl22_30
| ~ spl22_14 ),
inference(avatar_split_clause,[],[f262,f121,f222]) ).
fof(f274,plain,
( g_both(sK3,sK4)
| g_true_only(sK3,sK4)
| spl22_20 ),
inference(resolution,[],[f60,f164]) ).
fof(f275,plain,
( g_both(sK5,sK10)
| g_true_only(sK5,sK10)
| spl22_18 ),
inference(resolution,[],[f60,f156]) ).
fof(f278,definition,
( spl22_37
<=> g_true_only(sK5,sK10) ),
introduced(definition,[new_symbols(definition,[spl22_37])],[avatar_definition]) ).
fof(f280,plain,
( g_true_only(sK5,sK10)
| ~ spl22_37 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f281,plain,
( spl22_37
| spl22_33
| spl22_18 ),
inference(avatar_split_clause,[],[f275,f154,f237,f278]) ).
fof(f283,definition,
( spl22_38
<=> g_true_only(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl22_38])],[avatar_definition]) ).
fof(f285,plain,
( g_true_only(sK3,sK4)
| ~ spl22_38 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
( spl22_38
| spl22_26
| spl22_20 ),
inference(avatar_split_clause,[],[f274,f162,f190,f283]) ).
fof(f291,plain,
( ~ h_false_only(sK3,sK6(sK3,sK4))
| ~ spl22_2
| ~ spl22_26 ),
inference(resolution,[],[f191,f76]) ).
fof(f300,plain,
( ! [X0] :
( h_both(sK3,X0)
| h_false_only(sK3,X0) )
| ~ spl22_19 ),
inference(resolution,[],[f70,f159]) ).
fof(f301,plain,
( ! [X0] : h_false_only(sK3,X0)
| ~ spl22_19
| ~ spl22_22 ),
inference(forward_subsumption_resolution,[],[f300,f174]) ).
fof(f302,plain,
( spl22_29
| ~ spl22_19
| ~ spl22_22 ),
inference(avatar_split_clause,[],[f301,f173,f158,f208]) ).
fof(f303,plain,
( ! [X0] : ~ g_true_only(sK3,X0)
| ~ spl22_4
| ~ spl22_29 ),
inference(resolution,[],[f209,f84]) ).
fof(f310,plain,
( $false
| ~ spl22_2
| ~ spl22_26
| ~ spl22_29 ),
inference(resolution,[],[f291,f209]) ).
fof(f311,plain,
( ~ spl22_2
| ~ spl22_26
| ~ spl22_29 ),
inference(avatar_contradiction_clause,[],[f310]) ).
fof(f312,plain,
( $false
| ~ spl22_4
| ~ spl22_29
| ~ spl22_38 ),
inference(forward_subsumption_resolution,[],[f285,f303]) ).
fof(f313,plain,
( ~ spl22_4
| ~ spl22_29
| ~ spl22_38 ),
inference(avatar_contradiction_clause,[],[f312]) ).
fof(f316,plain,
( ! [X0] :
( h_false_only(sK3,sK6(sK3,X0))
| ~ g_true_only(sK3,X0) )
| ~ spl22_3
| ~ spl22_19 ),
inference(resolution,[],[f300,f80]) ).
fof(f318,plain,
( ! [X0] : ~ g_true_only(sK3,X0)
| ~ spl22_3
| ~ spl22_4
| ~ spl22_19 ),
inference(forward_subsumption_resolution,[],[f316,f84]) ).
fof(f319,plain,
( $false
| ~ spl22_3
| ~ spl22_4
| ~ spl22_19
| ~ spl22_23 ),
inference(resolution,[],[f318,f178]) ).
fof(f320,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_19
| ~ spl22_23 ),
inference(avatar_contradiction_clause,[],[f319]) ).
fof(f321,plain,
( ! [X0] :
( h_both(sK2,X0)
| h_false_only(sK2,X0) )
| ~ spl22_8 ),
inference(resolution,[],[f101,f70]) ).
fof(f323,plain,
( ! [X0] :
( h_false_only(sK2,sK6(sK2,X0))
| ~ g_true_only(sK2,X0) )
| ~ spl22_3
| ~ spl22_8 ),
inference(resolution,[],[f321,f80]) ).
fof(f325,plain,
( ! [X0] : ~ g_true_only(sK2,X0)
| ~ spl22_3
| ~ spl22_4
| ~ spl22_8 ),
inference(forward_subsumption_resolution,[],[f323,f84]) ).
fof(f326,plain,
( spl22_15
| ~ spl22_3
| ~ spl22_4
| ~ spl22_8 ),
inference(avatar_split_clause,[],[f325,f100,f83,f79,f127]) ).
fof(f328,plain,
( $false
| ~ spl22_2
| ~ spl22_14
| ~ spl22_31 ),
inference(resolution,[],[f227,f229]) ).
fof(f330,plain,
( ~ spl22_2
| ~ spl22_14
| ~ spl22_31 ),
inference(avatar_contradiction_clause,[],[f328]) ).
fof(f335,plain,
( $false
| ~ spl22_24
| ~ spl22_26 ),
inference(resolution,[],[f181,f191]) ).
fof(f336,plain,
( ~ spl22_24
| ~ spl22_26 ),
inference(avatar_contradiction_clause,[],[f335]) ).
fof(f337,plain,
( ! [X0] : h_false_only(sK3,X0)
| ~ spl22_3
| ~ spl22_4
| ~ spl22_10
| ~ spl22_19
| spl22_25 ),
inference(forward_subsumption_resolution,[],[f195,f318]) ).
fof(f340,plain,
( spl22_29
| ~ spl22_3
| ~ spl22_4
| ~ spl22_10
| ~ spl22_19
| spl22_25 ),
inference(avatar_split_clause,[],[f337,f186,f158,f106,f83,f79,f208]) ).
fof(f341,plain,
( ! [X0] : ~ g_true_only(sK2,X0)
| ~ spl22_4
| ~ spl22_9 ),
inference(resolution,[],[f104,f84]) ).
fof(f344,plain,
( spl22_15
| ~ spl22_4
| ~ spl22_9 ),
inference(avatar_split_clause,[],[f341,f103,f83,f127]) ).
fof(f348,plain,
( ! [X0] :
( h_both(sK5,X0)
| h_false_only(sK5,X0) )
| ~ spl22_21 ),
inference(resolution,[],[f168,f70]) ).
fof(f349,plain,
( ! [X0] : h_false_only(sK5,X0)
| ~ spl22_21
| ~ spl22_34 ),
inference(forward_subsumption_resolution,[],[f348,f242]) ).
fof(f351,plain,
( ! [X0,X1] :
( ~ g_both(sK5,X0)
| g_true_only(sK5,sK9(sK5))
| ~ h_both(sK5,X1) )
| ~ spl22_7
| ~ spl22_21 ),
inference(resolution,[],[f98,f168]) ).
fof(f353,plain,
( ~ h_false_only(sK5,sK6(sK5,sK10))
| ~ spl22_2
| ~ spl22_33 ),
inference(resolution,[],[f238,f76]) ).
fof(f354,plain,
( $false
| ~ spl22_2
| ~ spl22_21
| ~ spl22_33
| ~ spl22_34 ),
inference(forward_subsumption_resolution,[],[f353,f349]) ).
fof(f355,plain,
( ~ spl22_2
| ~ spl22_21
| ~ spl22_33
| ~ spl22_34 ),
inference(avatar_contradiction_clause,[],[f354]) ).
fof(f356,plain,
( $false
| ~ spl22_33
| ~ spl22_36 ),
inference(resolution,[],[f251,f238]) ).
fof(f357,plain,
( ~ spl22_33
| ~ spl22_36 ),
inference(avatar_contradiction_clause,[],[f356]) ).
fof(f358,plain,
( ! [X0] :
( h_false_only(sK5,sK6(sK5,X0))
| ~ g_true_only(sK5,X0) )
| ~ spl22_3
| ~ spl22_21 ),
inference(resolution,[],[f348,f80]) ).
fof(f360,plain,
( ! [X0] : ~ g_true_only(sK5,X0)
| ~ spl22_3
| ~ spl22_4
| ~ spl22_21 ),
inference(forward_subsumption_resolution,[],[f358,f84]) ).
fof(f361,plain,
( $false
| ~ spl22_3
| ~ spl22_4
| ~ spl22_21
| ~ spl22_37 ),
inference(resolution,[],[f360,f280]) ).
fof(f362,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_21
| ~ spl22_37 ),
inference(avatar_contradiction_clause,[],[f361]) ).
fof(f365,plain,
( ! [X0,X1] :
( ~ g_both(sK5,X0)
| ~ h_both(sK5,X1) )
| ~ spl22_3
| ~ spl22_4
| ~ spl22_7
| ~ spl22_21 ),
inference(forward_subsumption_resolution,[],[f351,f360]) ).
fof(f366,plain,
( spl22_34
| spl22_36
| ~ spl22_3
| ~ spl22_4
| ~ spl22_7
| ~ spl22_21 ),
inference(avatar_split_clause,[],[f365,f167,f97,f83,f79,f250,f241]) ).
fof(f368,plain,
( $false
| ~ spl22_15
| ~ spl22_17 ),
inference(resolution,[],[f128,f146]) ).
fof(f369,plain,
( ~ spl22_15
| ~ spl22_17 ),
inference(avatar_contradiction_clause,[],[f368]) ).
fof(f372,plain,
( ! [X2,X0,X1] :
( ~ h_both(X0,X2)
| ~ h_both(X0,sK21(X0))
| ~ g_true_only(X0,X1) )
| ~ spl22_1 ),
inference(resolution,[],[f73,f258]) ).
fof(f375,definition,
( spl22_39
<=> ! [X0] : ~ g_true_only(sK5,X0) ),
introduced(definition,[new_symbols(definition,[spl22_39])],[avatar_definition]) ).
fof(f376,plain,
( ! [X0] : ~ g_true_only(sK5,X0)
| ~ spl22_39 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f379,plain,
( ~ h_false_only(sK5,sK16(sK5))
| g_true_only(sK5,sK17(sK5))
| ~ spl22_5
| ~ spl22_33 ),
inference(resolution,[],[f88,f238]) ).
fof(f390,plain,
( $false
| ~ spl22_35
| ~ spl22_39 ),
inference(resolution,[],[f248,f376]) ).
fof(f391,plain,
( ~ spl22_35
| ~ spl22_39 ),
inference(avatar_contradiction_clause,[],[f390]) ).
fof(f393,definition,
( spl22_42
<=> g_true_only(sK5,sK17(sK5)) ),
introduced(definition,[new_symbols(definition,[spl22_42])],[avatar_definition]) ).
fof(f395,plain,
( g_true_only(sK5,sK17(sK5))
| ~ spl22_42 ),
inference(avatar_component_clause,[],[f393]) ).
fof(f397,definition,
( spl22_43
<=> h_false_only(sK5,sK16(sK5)) ),
introduced(definition,[new_symbols(definition,[spl22_43])],[avatar_definition]) ).
fof(f399,plain,
( ~ h_false_only(sK5,sK16(sK5))
| spl22_43 ),
inference(avatar_component_clause,[],[f397]) ).
fof(f400,plain,
( spl22_42
| ~ spl22_43
| ~ spl22_5
| ~ spl22_33 ),
inference(avatar_split_clause,[],[f379,f237,f87,f397,f393]) ).
fof(f405,definition,
( spl22_44
<=> ! [X0] : ~ g_true_only(sK3,X0) ),
introduced(definition,[new_symbols(definition,[spl22_44])],[avatar_definition]) ).
fof(f406,plain,
( ! [X0] : ~ g_true_only(sK3,X0)
| ~ spl22_44 ),
inference(avatar_component_clause,[],[f405]) ).
fof(f408,plain,
( $false
| ~ spl22_23
| ~ spl22_44 ),
inference(resolution,[],[f406,f178]) ).
fof(f409,plain,
( ~ spl22_23
| ~ spl22_44 ),
inference(avatar_contradiction_clause,[],[f408]) ).
fof(f410,plain,
( $false
| ~ spl22_38
| ~ spl22_44 ),
inference(forward_subsumption_resolution,[],[f285,f406]) ).
fof(f411,plain,
( ~ spl22_38
| ~ spl22_44 ),
inference(avatar_contradiction_clause,[],[f410]) ).
fof(f413,plain,
( spl22_34
| spl22_35
| spl22_36
| ~ spl22_7
| ~ spl22_21 ),
inference(avatar_split_clause,[],[f351,f167,f97,f250,f246,f241]) ).
fof(f419,plain,
( ! [X0,X1] :
( ~ g_true_only(sK5,X0)
| ~ h_both(sK5,X1) )
| ~ spl22_1
| ~ spl22_21 ),
inference(resolution,[],[f168,f73]) ).
fof(f420,plain,
( $false
| ~ spl22_37
| ~ spl22_39 ),
inference(resolution,[],[f376,f280]) ).
fof(f421,plain,
( ~ spl22_37
| ~ spl22_39 ),
inference(avatar_contradiction_clause,[],[f420]) ).
fof(f422,plain,
( ! [X0] : ~ g_true_only(sK5,X0)
| ~ spl22_4
| ~ spl22_21
| ~ spl22_34 ),
inference(resolution,[],[f349,f84]) ).
fof(f423,plain,
( ! [X0] : ~ g_true_only(sK5,X0)
| ~ spl22_6
| ~ spl22_21
| ~ spl22_34 ),
inference(resolution,[],[f349,f93]) ).
fof(f424,plain,
( spl22_39
| ~ spl22_6
| ~ spl22_21
| ~ spl22_34 ),
inference(avatar_split_clause,[],[f423,f241,f167,f92,f375]) ).
fof(f425,plain,
( spl22_39
| ~ spl22_4
| ~ spl22_21
| ~ spl22_34 ),
inference(avatar_split_clause,[],[f422,f241,f167,f83,f375]) ).
fof(f427,plain,
( spl22_44
| ~ spl22_3
| ~ spl22_4
| ~ spl22_19 ),
inference(avatar_split_clause,[],[f318,f158,f83,f79,f405]) ).
fof(f429,plain,
( spl22_39
| ~ spl22_3
| ~ spl22_4
| ~ spl22_21 ),
inference(avatar_split_clause,[],[f360,f167,f83,f79,f375]) ).
fof(f436,plain,
( ! [X0,X1] :
( ~ g_true_only(sK3,X0)
| ~ h_both(sK3,X1) )
| ~ spl22_1
| ~ spl22_19 ),
inference(resolution,[],[f73,f159]) ).
fof(f438,plain,
( ! [X0] : ~ g_true_only(sK3,X0)
| ~ spl22_6
| ~ spl22_29 ),
inference(resolution,[],[f209,f93]) ).
fof(f439,plain,
( spl22_44
| ~ spl22_6
| ~ spl22_29 ),
inference(avatar_split_clause,[],[f438,f208,f92,f405]) ).
fof(f442,plain,
( ~ h_false_only(sK3,sK16(sK3))
| g_true_only(sK3,sK17(sK3))
| ~ spl22_5
| ~ spl22_26 ),
inference(resolution,[],[f191,f88]) ).
fof(f451,plain,
( g_true_only(sK3,sK17(sK3))
| ~ spl22_5
| ~ spl22_26
| ~ spl22_29 ),
inference(forward_subsumption_resolution,[],[f442,f209]) ).
fof(f454,plain,
( $false
| ~ spl22_5
| ~ spl22_26
| ~ spl22_29
| ~ spl22_44 ),
inference(forward_subsumption_resolution,[],[f451,f406]) ).
fof(f455,plain,
( ~ spl22_5
| ~ spl22_26
| ~ spl22_29
| ~ spl22_44 ),
inference(avatar_contradiction_clause,[],[f454]) ).
fof(f462,plain,
( spl22_34
| spl22_39
| ~ spl22_1
| ~ spl22_21 ),
inference(avatar_split_clause,[],[f419,f167,f72,f375,f241]) ).
fof(f468,plain,
( ~ h_false_only(sK5,sK16(sK5))
| g_true_only(sK5,sK17(sK5))
| ~ spl22_5
| ~ spl22_33 ),
inference(resolution,[],[f238,f88]) ).
fof(f473,plain,
( ! [X2,X0,X1] :
( ~ h_both(X0,X2)
| ~ g_true_only(X0,X1)
| ~ h_false_only(X0,sK21(X0)) )
| ~ spl22_1 ),
inference(resolution,[],[f260,f73]) ).
fof(f476,plain,
( $false
| ~ spl22_39
| ~ spl22_42 ),
inference(forward_subsumption_resolution,[],[f395,f376]) ).
fof(f477,plain,
( ~ spl22_39
| ~ spl22_42 ),
inference(avatar_contradiction_clause,[],[f476]) ).
fof(f481,plain,
( g_true_only(sK5,sK17(sK5))
| ~ spl22_5
| ~ spl22_21
| ~ spl22_33
| ~ spl22_34 ),
inference(forward_subsumption_resolution,[],[f468,f349]) ).
fof(f484,plain,
( $false
| ~ spl22_5
| ~ spl22_21
| ~ spl22_33
| ~ spl22_34
| ~ spl22_39 ),
inference(forward_subsumption_resolution,[],[f481,f376]) ).
fof(f485,plain,
( ~ spl22_5
| ~ spl22_21
| ~ spl22_33
| ~ spl22_34
| ~ spl22_39 ),
inference(avatar_contradiction_clause,[],[f484]) ).
fof(f486,plain,
( ! [X0] : ~ g_true_only(sK2,X0)
| ~ spl22_6
| ~ spl22_9 ),
inference(resolution,[],[f104,f93]) ).
fof(f487,plain,
( spl22_15
| ~ spl22_6
| ~ spl22_9 ),
inference(avatar_split_clause,[],[f486,f103,f92,f127]) ).
fof(f488,plain,
( ~ h_false_only(sK2,sK16(sK2))
| g_true_only(sK2,sK17(sK2))
| ~ spl22_5
| ~ spl22_16 ),
inference(resolution,[],[f136,f88]) ).
fof(f490,plain,
( g_true_only(sK2,sK17(sK2))
| ~ spl22_5
| ~ spl22_9
| ~ spl22_16 ),
inference(forward_subsumption_resolution,[],[f488,f104]) ).
fof(f491,plain,
( $false
| ~ spl22_5
| ~ spl22_9
| ~ spl22_15
| ~ spl22_16 ),
inference(forward_subsumption_resolution,[],[f490,f128]) ).
fof(f492,plain,
( ~ spl22_5
| ~ spl22_9
| ~ spl22_15
| ~ spl22_16 ),
inference(avatar_contradiction_clause,[],[f491]) ).
fof(f494,plain,
( g_true_only(sK0,sK1)
| ~ spl22_13 ),
inference(resolution,[],[f119,f38]) ).
fof(f496,plain,
( ! [X0] :
( h_false_only(sK0,X0)
| g_true_only(sK0,sK1) )
| ~ spl22_11 ),
inference(resolution,[],[f110,f38]) ).
fof(f506,plain,
( ! [X0,X1] :
( ~ h_both(sK0,X0)
| ~ g_true_only(sK0,X1)
| h_false_only(sK0,sK21(sK0)) )
| ~ spl22_1
| ~ spl22_11 ),
inference(resolution,[],[f372,f215]) ).
fof(f509,plain,
( ! [X0,X1] :
( ~ h_both(sK0,X0)
| ~ g_true_only(sK0,X1) )
| ~ spl22_1
| ~ spl22_11 ),
inference(forward_subsumption_resolution,[],[f506,f473]) ).
fof(f511,definition,
( spl22_45
<=> ! [X1] : ~ g_true_only(sK0,X1) ),
introduced(definition,[new_symbols(definition,[spl22_45])],[avatar_definition]) ).
fof(f512,plain,
( ! [X1] : ~ g_true_only(sK0,X1)
| ~ spl22_45 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f519,definition,
( spl22_47
<=> ! [X0] : ~ h_both(sK0,X0) ),
introduced(definition,[new_symbols(definition,[spl22_47])],[avatar_definition]) ).
fof(f520,plain,
( ! [X0] : ~ h_both(sK0,X0)
| ~ spl22_47 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f521,plain,
( spl22_45
| spl22_47
| ~ spl22_1
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f509,f109,f72,f519,f511]) ).
fof(f529,plain,
( ! [X0] : h_false_only(sK0,X0)
| ~ spl22_11
| ~ spl22_47 ),
inference(resolution,[],[f520,f215]) ).
fof(f530,plain,
( spl22_31
| ~ spl22_11
| ~ spl22_47 ),
inference(avatar_split_clause,[],[f529,f519,f109,f226]) ).
fof(f531,plain,
( $false
| ~ spl22_30
| ~ spl22_45 ),
inference(resolution,[],[f512,f224]) ).
fof(f532,plain,
( ~ spl22_30
| ~ spl22_45 ),
inference(avatar_contradiction_clause,[],[f531]) ).
fof(f533,plain,
( ! [X0] : ~ g_true_only(sK0,X0)
| ~ spl22_6
| ~ spl22_31 ),
inference(resolution,[],[f227,f93]) ).
fof(f534,plain,
( spl22_45
| ~ spl22_6
| ~ spl22_31 ),
inference(avatar_split_clause,[],[f533,f226,f92,f511]) ).
fof(f537,plain,
( ! [X0] :
( h_both(sK2,X0)
| h_false_only(sK2,X0) )
| ~ spl22_8 ),
inference(resolution,[],[f101,f70]) ).
fof(f538,plain,
( ! [X0,X1] :
( ~ g_true_only(sK2,X0)
| ~ h_both(sK2,X1) )
| ~ spl22_1
| ~ spl22_8 ),
inference(resolution,[],[f101,f73]) ).
fof(f540,definition,
( spl22_49
<=> ! [X1] : ~ h_both(sK2,X1) ),
introduced(definition,[new_symbols(definition,[spl22_49])],[avatar_definition]) ).
fof(f541,plain,
( ! [X1] : ~ h_both(sK2,X1)
| ~ spl22_49 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f542,plain,
( spl22_49
| spl22_15
| ~ spl22_1
| ~ spl22_8 ),
inference(avatar_split_clause,[],[f538,f100,f72,f127,f540]) ).
fof(f550,plain,
( $false
| ~ spl22_12
| ~ spl22_49 ),
inference(resolution,[],[f541,f115]) ).
fof(f551,plain,
( ~ spl22_12
| ~ spl22_49 ),
inference(avatar_contradiction_clause,[],[f550]) ).
fof(f553,plain,
( sP12(sK7(sK5),sK5)
| ~ spl22_10
| spl22_32 ),
inference(resolution,[],[f107,f235]) ).
fof(f555,plain,
( ! [X0] : h_false_only(sK2,X0)
| ~ spl22_8
| ~ spl22_49 ),
inference(resolution,[],[f537,f541]) ).
fof(f560,plain,
( spl22_9
| ~ spl22_8
| ~ spl22_49 ),
inference(avatar_split_clause,[],[f555,f540,f100,f103]) ).
fof(f561,plain,
( ! [X0] :
( g_true_only(sK5,sK7(sK5))
| h_false_only(sK5,X0) )
| ~ spl22_10
| spl22_32 ),
inference(resolution,[],[f553,f17]) ).
fof(f565,plain,
( ! [X0] : h_false_only(sK5,X0)
| ~ spl22_10
| spl22_32
| ~ spl22_39 ),
inference(forward_subsumption_resolution,[],[f561,f376]) ).
fof(f566,plain,
( $false
| ~ spl22_10
| spl22_32
| ~ spl22_39
| spl22_43 ),
inference(resolution,[],[f565,f399]) ).
fof(f568,plain,
( ~ spl22_10
| spl22_32
| ~ spl22_39
| spl22_43 ),
inference(avatar_contradiction_clause,[],[f566]) ).
fof(f572,plain,
( spl22_30
| spl22_31
| ~ spl22_11 ),
inference(avatar_split_clause,[],[f496,f109,f226,f222]) ).
fof(f573,plain,
( ~ h_false_only(sK0,sK16(sK0))
| g_true_only(sK0,sK17(sK0))
| ~ spl22_5
| ~ spl22_14 ),
inference(resolution,[],[f123,f88]) ).
fof(f575,plain,
( g_true_only(sK0,sK17(sK0))
| ~ spl22_5
| ~ spl22_14
| ~ spl22_31 ),
inference(forward_subsumption_resolution,[],[f573,f227]) ).
fof(f576,plain,
( $false
| ~ spl22_5
| ~ spl22_14
| ~ spl22_31
| ~ spl22_45 ),
inference(forward_subsumption_resolution,[],[f575,f512]) ).
fof(f577,plain,
( ~ spl22_5
| ~ spl22_14
| ~ spl22_31
| ~ spl22_45 ),
inference(avatar_contradiction_clause,[],[f576]) ).
fof(f580,plain,
( $false
| ~ spl22_13
| spl22_30 ),
inference(forward_subsumption_resolution,[],[f494,f223]) ).
fof(f581,plain,
( ~ spl22_13
| spl22_30 ),
inference(avatar_contradiction_clause,[],[f580]) ).
fof(f588,plain,
( ~ h_false_only(sK2,sK6(sK2,sK14))
| ~ spl22_2
| ~ spl22_16 ),
inference(resolution,[],[f76,f136]) ).
fof(f589,plain,
( $false
| ~ spl22_2
| ~ spl22_9
| ~ spl22_16 ),
inference(forward_subsumption_resolution,[],[f588,f104]) ).
fof(f590,plain,
( ~ spl22_2
| ~ spl22_9
| ~ spl22_16 ),
inference(avatar_contradiction_clause,[],[f589]) ).
fof(f602,plain,
( $false
| ~ spl22_2
| ~ spl22_10
| spl22_32
| ~ spl22_33
| ~ spl22_39 ),
inference(resolution,[],[f353,f565]) ).
fof(f603,plain,
( ~ spl22_2
| ~ spl22_10
| spl22_32
| ~ spl22_33
| ~ spl22_39 ),
inference(avatar_contradiction_clause,[],[f602]) ).
fof(f607,plain,
( spl22_22
| spl22_44
| ~ spl22_1
| ~ spl22_19 ),
inference(avatar_split_clause,[],[f436,f158,f72,f405,f173]) ).
fof(f608,plain,
( spl22_29
| spl22_28
| ~ spl22_10
| spl22_25 ),
inference(avatar_split_clause,[],[f195,f186,f106,f203,f208]) ).
fof(f638,plain,
( $false
| ~ spl22_28
| ~ spl22_44 ),
inference(resolution,[],[f205,f406]) ).
fof(f639,plain,
( ~ spl22_28
| ~ spl22_44 ),
inference(avatar_contradiction_clause,[],[f638]) ).
cnf(s1,plain,
( spl22_1
| spl22_2 ),
inference(sat_conversion,[],[f77]) ).
cnf(s2,plain,
( spl22_1
| spl22_3 ),
inference(sat_conversion,[],[f81]) ).
cnf(s3,plain,
( spl22_1
| spl22_4 ),
inference(sat_conversion,[],[f85]) ).
cnf(s6,plain,
( spl22_4
| spl22_6 ),
inference(sat_conversion,[],[f94]) ).
cnf(s7,plain,
( spl22_3
| spl22_6 ),
inference(sat_conversion,[],[f95]) ).
cnf(s8,plain,
( spl22_9
| spl22_8
| spl22_7
| spl22_9
| spl22_10
| spl22_11 ),
inference(sat_conversion,[],[f111]) ).
cnf(s9,plain,
( spl22_7
| spl22_8
| spl22_9
| spl22_10
| spl22_11 ),
inference(rat,[],[s8]) ).
cnf(s12,plain,
( spl22_9
| spl22_8
| spl22_7
| spl22_9
| spl22_10
| spl22_13
| spl22_14 ),
inference(sat_conversion,[],[f124]) ).
cnf(s13,plain,
( spl22_7
| spl22_8
| spl22_9
| spl22_10
| spl22_13
| spl22_14 ),
inference(rat,[],[s12]) ).
cnf(s14,plain,
( spl22_9
| spl22_7
| spl22_9
| spl22_10
| spl22_12
| spl22_13
| spl22_14 ),
inference(sat_conversion,[],[f125]) ).
cnf(s15,plain,
( spl22_7
| spl22_9
| spl22_10
| spl22_12
| spl22_13
| spl22_14 ),
inference(rat,[],[s14]) ).
cnf(s24,plain,
( spl22_2
| spl22_6 ),
inference(sat_conversion,[],[f141]) ).
cnf(s25,plain,
( spl22_2
| spl22_5 ),
inference(sat_conversion,[],[f142]) ).
cnf(s26,plain,
( spl22_7
| spl22_9
| spl22_10
| spl22_11
| spl22_17 ),
inference(sat_conversion,[],[f147]) ).
cnf(s27,plain,
( spl22_7
| spl22_9
| spl22_10
| spl22_13
| spl22_14
| spl22_17 ),
inference(sat_conversion,[],[f148]) ).
cnf(s30,plain,
( spl22_7
| spl22_10
| spl22_11
| spl22_16
| spl22_17 ),
inference(sat_conversion,[],[f151]) ).
cnf(s31,plain,
( spl22_7
| spl22_10
| spl22_13
| spl22_14
| spl22_16
| spl22_17 ),
inference(sat_conversion,[],[f152]) ).
cnf(s32,plain,
( ~ spl22_18
| spl22_19 ),
inference(sat_conversion,[],[f160]) ).
cnf(s33,plain,
( ~ spl22_18
| ~ spl22_20 ),
inference(sat_conversion,[],[f165]) ).
cnf(s34,plain,
( spl22_19
| spl22_21 ),
inference(sat_conversion,[],[f169]) ).
cnf(s35,plain,
( ~ spl22_20
| spl22_21 ),
inference(sat_conversion,[],[f170]) ).
cnf(s37,plain,
( ~ spl22_19
| spl22_20
| spl22_22
| ~ spl22_25
| ~ spl22_26 ),
inference(sat_conversion,[],[f193]) ).
cnf(s40,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_13 ),
inference(sat_conversion,[],[f220]) ).
cnf(s42,plain,
( spl22_18
| ~ spl22_21
| ~ spl22_32
| ~ spl22_33
| spl22_34 ),
inference(sat_conversion,[],[f243]) ).
cnf(s44,plain,
( ~ spl22_7
| ~ spl22_19
| spl22_22
| spl22_23
| spl22_24 ),
inference(sat_conversion,[],[f253]) ).
cnf(s45,plain,
( ~ spl22_14
| ~ spl22_30 ),
inference(sat_conversion,[],[f263]) ).
cnf(s46,plain,
( spl22_18
| spl22_33
| spl22_37 ),
inference(sat_conversion,[],[f281]) ).
cnf(s47,plain,
( spl22_20
| spl22_26
| spl22_38 ),
inference(sat_conversion,[],[f286]) ).
cnf(s50,plain,
( ~ spl22_19
| ~ spl22_22
| spl22_29 ),
inference(sat_conversion,[],[f302]) ).
cnf(s52,plain,
( ~ spl22_2
| ~ spl22_26
| ~ spl22_29 ),
inference(sat_conversion,[],[f311]) ).
cnf(s53,plain,
( ~ spl22_4
| ~ spl22_29
| ~ spl22_38 ),
inference(sat_conversion,[],[f313]) ).
cnf(s55,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_19
| ~ spl22_23 ),
inference(sat_conversion,[],[f320]) ).
cnf(s56,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_8
| spl22_15 ),
inference(sat_conversion,[],[f326]) ).
cnf(s57,plain,
( ~ spl22_2
| ~ spl22_14
| ~ spl22_31 ),
inference(sat_conversion,[],[f330]) ).
cnf(s58,plain,
( ~ spl22_24
| ~ spl22_26 ),
inference(sat_conversion,[],[f336]) ).
cnf(s60,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_10
| ~ spl22_19
| spl22_25
| spl22_29 ),
inference(sat_conversion,[],[f340]) ).
cnf(s62,plain,
( ~ spl22_4
| ~ spl22_9
| spl22_15 ),
inference(sat_conversion,[],[f344]) ).
cnf(s64,plain,
( ~ spl22_2
| ~ spl22_21
| ~ spl22_33
| ~ spl22_34 ),
inference(sat_conversion,[],[f355]) ).
cnf(s65,plain,
( ~ spl22_33
| ~ spl22_36 ),
inference(sat_conversion,[],[f357]) ).
cnf(s66,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_21
| ~ spl22_37 ),
inference(sat_conversion,[],[f362]) ).
cnf(s68,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_7
| ~ spl22_21
| spl22_34
| spl22_36 ),
inference(sat_conversion,[],[f366]) ).
cnf(s70,plain,
( ~ spl22_15
| ~ spl22_17 ),
inference(sat_conversion,[],[f369]) ).
cnf(s73,plain,
( ~ spl22_35
| ~ spl22_39 ),
inference(sat_conversion,[],[f391]) ).
cnf(s74,plain,
( ~ spl22_5
| ~ spl22_33
| spl22_42
| ~ spl22_43 ),
inference(sat_conversion,[],[f400]) ).
cnf(s76,plain,
( ~ spl22_23
| ~ spl22_44 ),
inference(sat_conversion,[],[f409]) ).
cnf(s77,plain,
( ~ spl22_38
| ~ spl22_44 ),
inference(sat_conversion,[],[f411]) ).
cnf(s79,plain,
( ~ spl22_7
| ~ spl22_21
| spl22_34
| spl22_35
| spl22_36 ),
inference(sat_conversion,[],[f413]) ).
cnf(s81,plain,
( ~ spl22_37
| ~ spl22_39 ),
inference(sat_conversion,[],[f421]) ).
cnf(s82,plain,
( ~ spl22_6
| ~ spl22_21
| ~ spl22_34
| spl22_39 ),
inference(sat_conversion,[],[f424]) ).
cnf(s83,plain,
( ~ spl22_4
| ~ spl22_21
| ~ spl22_34
| spl22_39 ),
inference(sat_conversion,[],[f425]) ).
cnf(s84,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_19
| spl22_44 ),
inference(sat_conversion,[],[f427]) ).
cnf(s85,plain,
( ~ spl22_3
| ~ spl22_4
| ~ spl22_21
| spl22_39 ),
inference(sat_conversion,[],[f429]) ).
cnf(s90,plain,
( ~ spl22_6
| ~ spl22_29
| spl22_44 ),
inference(sat_conversion,[],[f439]) ).
cnf(s96,plain,
( ~ spl22_5
| ~ spl22_26
| ~ spl22_29
| ~ spl22_44 ),
inference(sat_conversion,[],[f455]) ).
cnf(s100,plain,
( ~ spl22_1
| ~ spl22_21
| spl22_34
| spl22_39 ),
inference(sat_conversion,[],[f462]) ).
cnf(s105,plain,
( ~ spl22_39
| ~ spl22_42 ),
inference(sat_conversion,[],[f477]) ).
cnf(s108,plain,
( ~ spl22_5
| ~ spl22_21
| ~ spl22_33
| ~ spl22_34
| ~ spl22_39 ),
inference(sat_conversion,[],[f485]) ).
cnf(s109,plain,
( ~ spl22_6
| ~ spl22_9
| spl22_15 ),
inference(sat_conversion,[],[f487]) ).
cnf(s110,plain,
( ~ spl22_5
| ~ spl22_9
| ~ spl22_15
| ~ spl22_16 ),
inference(sat_conversion,[],[f492]) ).
cnf(s112,plain,
( ~ spl22_1
| ~ spl22_11
| spl22_45
| spl22_47 ),
inference(sat_conversion,[],[f521]) ).
cnf(s114,plain,
( ~ spl22_11
| spl22_31
| ~ spl22_47 ),
inference(sat_conversion,[],[f530]) ).
cnf(s115,plain,
( ~ spl22_30
| ~ spl22_45 ),
inference(sat_conversion,[],[f532]) ).
cnf(s116,plain,
( ~ spl22_6
| ~ spl22_31
| spl22_45 ),
inference(sat_conversion,[],[f534]) ).
cnf(s118,plain,
( ~ spl22_1
| ~ spl22_8
| spl22_15
| spl22_49 ),
inference(sat_conversion,[],[f542]) ).
cnf(s120,plain,
( ~ spl22_12
| ~ spl22_49 ),
inference(sat_conversion,[],[f551]) ).
cnf(s121,plain,
( ~ spl22_8
| spl22_9
| ~ spl22_49 ),
inference(sat_conversion,[],[f560]) ).
cnf(s122,plain,
( ~ spl22_10
| spl22_32
| ~ spl22_39
| spl22_43 ),
inference(sat_conversion,[],[f568]) ).
cnf(s125,plain,
( ~ spl22_11
| spl22_30
| spl22_31 ),
inference(sat_conversion,[],[f572]) ).
cnf(s129,plain,
( ~ spl22_5
| ~ spl22_14
| ~ spl22_31
| ~ spl22_45 ),
inference(sat_conversion,[],[f577]) ).
cnf(s131,plain,
( ~ spl22_13
| spl22_30 ),
inference(sat_conversion,[],[f581]) ).
cnf(s134,plain,
( ~ spl22_2
| ~ spl22_9
| ~ spl22_16 ),
inference(sat_conversion,[],[f590]) ).
cnf(s135,plain,
( ~ spl22_2
| ~ spl22_10
| spl22_32
| ~ spl22_33
| ~ spl22_39 ),
inference(sat_conversion,[],[f603]) ).
cnf(s137,plain,
( ~ spl22_1
| ~ spl22_19
| spl22_22
| spl22_44 ),
inference(sat_conversion,[],[f607]) ).
cnf(s138,plain,
( ~ spl22_10
| spl22_25
| spl22_28
| spl22_29 ),
inference(sat_conversion,[],[f608]) ).
cnf(s147,plain,
( ~ spl22_28
| ~ spl22_44 ),
inference(sat_conversion,[],[f639]) ).
cnf(s148,plain,
( spl22_10
| spl22_9
| spl22_8
| spl22_7
| spl22_1 ),
inference(rat,[],[s125,s45,s57,s13,s9,s1,s40,s3,s2]) ).
cnf(s149,plain,
( ~ spl22_14
| ~ spl22_11
| ~ spl22_2 ),
inference(rat,[],[s125,s45,s57]) ).
cnf(s150,plain,
( ~ spl22_21
| spl22_18
| ~ spl22_10
| spl22_1 ),
inference(rat,[],[s42,s135,s64,s46,s66,s85,s3,s2,s1]) ).
cnf(s151,plain,
( spl22_21
| ~ spl22_10
| spl22_1 ),
inference(rat,[],[s37,s60,s50,s52,s47,s77,s84,s34,s35,s3,s2,s1]) ).
cnf(s152,plain,
( ~ spl22_10
| spl22_1 ),
inference(rat,[],[s37,s60,s50,s52,s47,s77,s84,s32,s33,s150,s151,s3,s2,s1]) ).
cnf(s153,plain,
( ~ spl22_9
| spl22_7
| spl22_1 ),
inference(rat,[],[s149,s31,s30,s70,s62,s134,s1,s40,s3,s2,s152]) ).
cnf(s154,plain,
( spl22_7
| spl22_1 ),
inference(rat,[],[s149,s26,s27,s70,s56,s148,s153,s1,s40,s3,s2,s152]) ).
cnf(s155,plain,
( ~ spl22_21
| spl22_18
| spl22_1 ),
inference(rat,[],[s68,s64,s65,s46,s66,s3,s2,s1,s154]) ).
cnf(s156,plain,
( spl22_21
| spl22_1 ),
inference(rat,[],[s50,s44,s52,s58,s47,s77,s55,s84,s34,s35,s3,s2,s1,s154]) ).
cnf(s157,plain,
spl22_1,
inference(rat,[],[s50,s44,s52,s58,s47,s77,s55,s84,s32,s33,s155,s156,s154,s1,s2,s3]) ).
cnf(s158,plain,
( ~ spl22_21
| spl22_18
| ~ spl22_10
| ~ spl22_3
| ~ spl22_4
| ~ spl22_2 ),
inference(rat,[],[s42,s135,s64,s46,s66,s85]) ).
cnf(s159,plain,
( spl22_21
| ~ spl22_10
| ~ spl22_3
| ~ spl22_4
| ~ spl22_2 ),
inference(rat,[],[s37,s60,s50,s52,s47,s77,s84,s34,s35]) ).
cnf(s160,plain,
( ~ spl22_21
| ~ spl22_10
| ~ spl22_2
| ~ spl22_3
| ~ spl22_4 ),
inference(rat,[],[s37,s60,s50,s52,s47,s77,s84,s32,s33,s158]) ).
cnf(s161,plain,
( ~ spl22_10
| ~ spl22_3
| ~ spl22_2
| ~ spl22_4 ),
inference(rat,[],[s160,s159]) ).
cnf(s162,plain,
( spl22_9
| spl22_8
| spl22_10
| spl22_13
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s149,s13,s9]) ).
cnf(s163,plain,
( ~ spl22_9
| ~ spl22_3
| ~ spl22_4
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s149,s31,s30,s70,s62,s134,s40,s161]) ).
cnf(s164,plain,
( ~ spl22_3
| ~ spl22_4
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s149,s26,s27,s70,s56,s162,s163,s161,s40]) ).
cnf(s165,plain,
( ~ spl22_33
| spl22_18
| ~ spl22_21
| ~ spl22_10
| ~ spl22_2 ),
inference(rat,[],[s135,s100,s42,s64,s157]) ).
cnf(s166,plain,
( spl22_39
| ~ spl22_21
| ~ spl22_4 ),
inference(rat,[],[s100,s83,s157]) ).
cnf(s167,plain,
( spl22_18
| spl22_37
| ~ spl22_21
| ~ spl22_10
| ~ spl22_2 ),
inference(rat,[],[s46,s165]) ).
cnf(s168,plain,
( spl22_22
| ~ spl22_18
| ~ spl22_10
| ~ spl22_2 ),
inference(rat,[],[s138,s37,s52,s47,s77,s147,s137,s33,s32,s157]) ).
cnf(s169,plain,
( ~ spl22_18
| ~ spl22_10
| ~ spl22_4
| ~ spl22_2 ),
inference(rat,[],[s47,s52,s53,s50,s168,s32,s33]) ).
cnf(s170,plain,
( ~ spl22_21
| ~ spl22_10
| ~ spl22_4
| ~ spl22_2 ),
inference(rat,[],[s81,s167,s166,s169]) ).
cnf(s171,plain,
( spl22_22
| ~ spl22_19
| spl22_20
| ~ spl22_10
| ~ spl22_2 ),
inference(rat,[],[s138,s37,s52,s47,s77,s147,s137,s157]) ).
cnf(s172,plain,
( ~ spl22_10
| ~ spl22_4
| ~ spl22_2 ),
inference(rat,[],[s47,s52,s53,s50,s171,s34,s35,s170]) ).
cnf(s173,plain,
( spl22_9
| spl22_8
| ~ spl22_4
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s114,s116,s112,s115,s131,s9,s162,s7,s164,s172,s157]) ).
cnf(s174,plain,
( ~ spl22_9
| ~ spl22_4
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s114,s116,s112,s115,s131,s31,s149,s30,s70,s62,s134,s7,s164,s172,s157]) ).
cnf(s175,plain,
( ~ spl22_4
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s114,s116,s112,s115,s131,s27,s149,s26,s70,s118,s121,s173,s174,s172,s7,s164,s157]) ).
cnf(s176,plain,
( spl22_9
| spl22_8
| spl22_10
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s114,s116,s112,s115,s131,s9,s162,s6,s175,s157]) ).
cnf(s177,plain,
( ~ spl22_9
| spl22_10
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s114,s116,s112,s115,s131,s31,s149,s30,s70,s109,s134,s6,s175,s157]) ).
cnf(s178,plain,
( spl22_10
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s114,s116,s112,s115,s131,s27,s149,s26,s70,s118,s121,s176,s177,s6,s175,s157]) ).
cnf(s179,plain,
( spl22_45
| ~ spl22_11
| ~ spl22_6 ),
inference(rat,[],[s114,s116,s112,s157]) ).
cnf(s180,plain,
( spl22_39
| ~ spl22_21
| ~ spl22_6 ),
inference(rat,[],[s82,s100,s157]) ).
cnf(s181,plain,
( ~ spl22_18
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s47,s77,s52,s90,s50,s168,s32,s33,s6,s175,s178]) ).
cnf(s182,plain,
( ~ spl22_21
| spl22_7
| ~ spl22_2 ),
inference(rat,[],[s81,s167,s180,s6,s175,s178,s181]) ).
cnf(s183,plain,
( spl22_7
| ~ spl22_2 ),
inference(rat,[],[s47,s77,s52,s90,s50,s171,s34,s35,s182,s178,s6,s175]) ).
cnf(s184,plain,
( ~ spl22_33
| spl22_35
| ~ spl22_21
| ~ spl22_2 ),
inference(rat,[],[s79,s64,s65,s183]) ).
cnf(s185,plain,
( spl22_22
| ~ spl22_18
| ~ spl22_7 ),
inference(rat,[],[s58,s44,s47,s76,s77,s137,s33,s32,s157]) ).
cnf(s186,plain,
( ~ spl22_18
| ~ spl22_4
| ~ spl22_2 ),
inference(rat,[],[s47,s52,s53,s50,s185,s32,s33,s183]) ).
cnf(s187,plain,
( ~ spl22_21
| ~ spl22_4
| ~ spl22_2 ),
inference(rat,[],[s184,s46,s73,s81,s166,s186]) ).
cnf(s188,plain,
( spl22_22
| spl22_21
| ~ spl22_7 ),
inference(rat,[],[s58,s44,s47,s76,s77,s137,s35,s34,s157]) ).
cnf(s189,plain,
( ~ spl22_4
| ~ spl22_2 ),
inference(rat,[],[s47,s52,s53,s50,s188,s34,s35,s187,s183]) ).
cnf(s190,plain,
( ~ spl22_18
| ~ spl22_2 ),
inference(rat,[],[s77,s47,s90,s52,s50,s185,s32,s33,s183,s6,s189]) ).
cnf(s191,plain,
( ~ spl22_21
| ~ spl22_2 ),
inference(rat,[],[s184,s46,s73,s81,s180,s6,s189,s190]) ).
cnf(s192,plain,
~ spl22_2,
inference(rat,[],[s77,s47,s90,s52,s50,s188,s34,s35,s191,s6,s189,s183]) ).
cnf(s193,plain,
spl22_5,
inference(rat,[],[s25,s192]) ).
cnf(s194,plain,
spl22_6,
inference(rat,[],[s24,s192]) ).
cnf(s196,plain,
( spl22_9
| spl22_13
| spl22_7
| spl22_10
| spl22_14 ),
inference(rat,[],[s118,s70,s120,s27,s13,s15,s157]) ).
cnf(s199,plain,
( spl22_9
| spl22_11
| spl22_10
| spl22_7 ),
inference(rat,[],[s118,s70,s121,s26,s9,s157]) ).
cnf(s201,plain,
( spl22_18
| ~ spl22_10
| ~ spl22_21 ),
inference(rat,[],[s122,s74,s42,s108,s46,s105,s81,s180,s193,s194]) ).
cnf(s202,plain,
( spl22_22
| ~ spl22_19
| spl22_20
| ~ spl22_10 ),
inference(rat,[],[s138,s37,s96,s47,s77,s147,s137,s193,s157]) ).
cnf(s204,plain,
( spl22_16
| spl22_17
| spl22_7
| spl22_10 ),
inference(rat,[],[s129,s31,s125,s131,s115,s179,s30,s194,s193]) ).
cnf(s205,plain,
( ~ spl22_9
| spl22_10
| spl22_7 ),
inference(rat,[],[s204,s110,s70,s109,s193,s194]) ).
cnf(s206,plain,
( spl22_9
| spl22_10
| spl22_7 ),
inference(rat,[],[s129,s196,s125,s131,s115,s179,s199,s194,s193]) ).
cnf(s207,plain,
( spl22_10
| spl22_7 ),
inference(rat,[],[s206,s205]) ).
cnf(s208,plain,
( ~ spl22_19
| ~ spl22_10
| spl22_20 ),
inference(rat,[],[s47,s96,s77,s90,s50,s202,s194,s193]) ).
cnf(s209,plain,
( ~ spl22_10
| ~ spl22_21 ),
inference(rat,[],[s208,s32,s33,s201]) ).
cnf(s210,plain,
( ~ spl22_33
| ~ spl22_21 ),
inference(rat,[],[s79,s108,s65,s73,s180,s207,s209,s193,s194]) ).
cnf(s211,plain,
~ spl22_21,
inference(rat,[],[s47,s77,s96,s90,s50,s185,s32,s33,s46,s210,s207,s209,s81,s180,s193,s194]) ).
cnf(s212,plain,
~ spl22_20,
inference(rat,[],[s35,s211]) ).
cnf(s213,plain,
spl22_19,
inference(rat,[],[s34,s211]) ).
cnf(s214,plain,
~ spl22_10,
inference(rat,[],[s208,s212,s213]) ).
cnf(s215,plain,
spl22_7,
inference(rat,[],[s207,s214]) ).
cnf(s216,plain,
spl22_22,
inference(rat,[],[s188,s211,s215]) ).
cnf(s217,plain,
spl22_29,
inference(rat,[],[s50,s213,s216]) ).
cnf(s219,plain,
spl22_44,
inference(rat,[],[s90,s194,s217]) ).
cnf(s222,plain,
~ spl22_38,
inference(rat,[],[s77,s219]) ).
cnf(s224,plain,
~ spl22_26,
inference(rat,[],[s96,s217,s193,s219]) ).
cnf(s225,plain,
$false,
inference(rat,[],[s47,s212,s222,s224]) ).
fof(f640,plain,
$false,
inference(avatar_sat_refutation,[],[s225]) ).
%------------------------------------------------------------------------------
%----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/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n007.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 17:52:40 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.27 % (2638279)Will run a generic schedule for satisfiability detection.
% 0.19/0.27 % (2638288)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1943494095:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.27 % (2638285)% WARNING: option uhcvi not known.
% 0.19/0.27 % (2638284)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3462269773_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.27 % (2638285)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1321850442:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.27 % (2638286)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=66249733:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.27 % (2638287)dis+10_1_sil=32000:sp=arity:random_seed=1509040184:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.27 % (2638289)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=384863492:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.27 % (2638290)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3341463814:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.27 % (2638288) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2638279-2638288"...
% 0.19/0.27 % TRYING [1]
% 0.19/0.27 % (2638288)...printing done.
% 0.19/0.27 % TRYING [2]
% 0.19/0.27 % (2638288)Refutation found. Thanks to Tanya!
% 0.19/0.27 % SZS status Theorem for theBenchmark
% 0.19/0.27 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.27 % (2638288)------------------------------
% 0.19/0.27 % (2638288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.27 % (2638288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.27 % (2638288)CaDiCaL version: 2.1.3
% 0.19/0.27 % (2638288)Termination reason: Refutation
% 0.19/0.27 % (2638288)Time elapsed: 0.011 s
% 0.19/0.27 % (2638288)Peak memory usage: 12 MB
% 0.19/0.27 % (2638288)Instructions burned: 33 (million)
% 0.19/0.27 % (2638279)Success in time 0.034 s
% 0.19/0.28 % Vampire exiting
%------------------------------------------------------------------------------