%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO604+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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:32:02 PM UTC 2026
% Result : Theorem 0.19s 0.35s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 44
% Syntax : Number of formulae : 414 ( 20 unt; 39 def)
% Number of atoms : 1657 ( 0 equ)
% Maximal formula atoms : 59 ( 4 avg)
% Number of connectives : 2075 ( 832 ~;1062 |; 139 &)
% ( 42 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 51 ( 50 usr; 40 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 1 con; 0-1 aty)
% Number of variables : 383 ( 0 sgn 310 !; 73 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ! [X0] :
? [X1] :
( ( g_true_only(X1,X0)
& ( ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) )
| ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) )
| ( g_both(X1,X0)
& ( ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) )
| ( g_false_only(X1,X0)
& ( ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) ) ) )
| ( ? [X0] :
( ? [X1] :
( g_both(X1,X0)
& ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) )
& ~ ? [X1] :
( ( g_true_only(X1,X0)
& ( ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) )
| ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) )
| ( g_both(X1,X0)
& ( ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) )
| ( g_false_only(X1,X0)
& ( ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) ) ) ) )
& ~ ? [X0] :
! [X1] :
( ( g_true_only(X1,X0)
& ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) ) )
| ( g_false_only(X1,X0)
& ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nc3) ).
fof(f2,negated_conjecture,
~ ( ! [X0] :
? [X1] :
( ( g_true_only(X1,X0)
& ( ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) )
| ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) )
| ( g_both(X1,X0)
& ( ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) )
| ( g_false_only(X1,X0)
& ( ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) ) ) )
| ( ? [X0] :
( ? [X1] :
( g_both(X1,X0)
& ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) )
& ~ ? [X1] :
( ( g_true_only(X1,X0)
& ( ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) )
| ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) )
| ( g_both(X1,X0)
& ( ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) )
| ( g_false_only(X1,X0)
& ( ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) ) ) ) )
& ~ ? [X0] :
! [X1] :
( ( g_true_only(X1,X0)
& ! [X2] :
( g_false_only(X1,X2)
| g_false_only(X2,X1) ) )
| ( g_false_only(X1,X0)
& ? [X2] :
( g_true_only(X1,X2)
& g_true_only(X2,X1) ) ) ) ) ),
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/sandbox/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/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,plain,
~ ( ! [X0] :
? [X1] :
( ( g_true_only(X1,X0)
& ( ( ? [X2] :
( ( g_both(X1,X2)
| g_both(X2,X1) )
& ~ g_false_only(X1,X2)
& ~ g_false_only(X2,X1) )
& ~ ? [X3] :
( g_true_only(X1,X3)
& g_true_only(X3,X1) ) )
| ? [X4] :
( g_true_only(X1,X4)
& g_true_only(X4,X1) ) ) )
| ( g_both(X1,X0)
& ( ! [X5] :
( g_false_only(X1,X5)
| g_false_only(X5,X1) )
| ? [X6] :
( g_true_only(X1,X6)
& g_true_only(X6,X1) ) ) )
| ( g_false_only(X1,X0)
& ( ! [X7] :
( g_false_only(X1,X7)
| g_false_only(X7,X1) )
| ( ? [X8] :
( ( g_both(X1,X8)
| g_both(X8,X1) )
& ~ g_false_only(X1,X8)
& ~ g_false_only(X8,X1) )
& ~ ? [X9] :
( g_true_only(X1,X9)
& g_true_only(X9,X1) ) ) ) ) )
| ( ? [X10] :
( ? [X11] :
( g_both(X11,X10)
& ? [X12] :
( ( g_both(X11,X12)
| g_both(X12,X11) )
& ~ g_false_only(X11,X12)
& ~ g_false_only(X12,X11) )
& ~ ? [X13] :
( g_true_only(X11,X13)
& g_true_only(X13,X11) ) )
& ~ ? [X14] :
( ( g_true_only(X14,X10)
& ( ( ? [X15] :
( ( g_both(X14,X15)
| g_both(X15,X14) )
& ~ g_false_only(X14,X15)
& ~ g_false_only(X15,X14) )
& ~ ? [X16] :
( g_true_only(X14,X16)
& g_true_only(X16,X14) ) )
| ? [X17] :
( g_true_only(X14,X17)
& g_true_only(X17,X14) ) ) )
| ( g_both(X14,X10)
& ( ! [X18] :
( g_false_only(X14,X18)
| g_false_only(X18,X14) )
| ? [X19] :
( g_true_only(X14,X19)
& g_true_only(X19,X14) ) ) )
| ( g_false_only(X14,X10)
& ( ! [X20] :
( g_false_only(X14,X20)
| g_false_only(X20,X14) )
| ( ? [X21] :
( ( g_both(X14,X21)
| g_both(X21,X14) )
& ~ g_false_only(X14,X21)
& ~ g_false_only(X21,X14) )
& ~ ? [X22] :
( g_true_only(X14,X22)
& g_true_only(X22,X14) ) ) ) ) ) )
& ~ ? [X23] :
! [X24] :
( ( g_true_only(X24,X23)
& ! [X25] :
( g_false_only(X24,X25)
| g_false_only(X25,X24) ) )
| ( g_false_only(X24,X23)
& ? [X26] :
( g_true_only(X24,X26)
& g_true_only(X26,X24) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f8,plain,
( ? [X0] :
! [X1] :
( ( ~ g_true_only(X1,X0)
| ( ( ! [X2] :
( ( ~ g_both(X1,X2)
& ~ g_both(X2,X1) )
| g_false_only(X1,X2)
| g_false_only(X2,X1) )
| ? [X3] :
( g_true_only(X1,X3)
& g_true_only(X3,X1) ) )
& ! [X4] :
( ~ g_true_only(X1,X4)
| ~ g_true_only(X4,X1) ) ) )
& ( ~ g_both(X1,X0)
| ( ? [X5] :
( ~ g_false_only(X1,X5)
& ~ g_false_only(X5,X1) )
& ! [X6] :
( ~ g_true_only(X1,X6)
| ~ g_true_only(X6,X1) ) ) )
& ( ~ g_false_only(X1,X0)
| ( ? [X7] :
( ~ g_false_only(X1,X7)
& ~ g_false_only(X7,X1) )
& ( ! [X8] :
( ( ~ g_both(X1,X8)
& ~ g_both(X8,X1) )
| g_false_only(X1,X8)
| g_false_only(X8,X1) )
| ? [X9] :
( g_true_only(X1,X9)
& g_true_only(X9,X1) ) ) ) ) )
& ( ! [X10] :
( ! [X11] :
( ~ g_both(X11,X10)
| ! [X12] :
( ( ~ g_both(X11,X12)
& ~ g_both(X12,X11) )
| g_false_only(X11,X12)
| g_false_only(X12,X11) )
| ? [X13] :
( g_true_only(X11,X13)
& g_true_only(X13,X11) ) )
| ? [X14] :
( ( g_true_only(X14,X10)
& ( ( ? [X15] :
( ( g_both(X14,X15)
| g_both(X15,X14) )
& ~ g_false_only(X14,X15)
& ~ g_false_only(X15,X14) )
& ! [X16] :
( ~ g_true_only(X14,X16)
| ~ g_true_only(X16,X14) ) )
| ? [X17] :
( g_true_only(X14,X17)
& g_true_only(X17,X14) ) ) )
| ( g_both(X14,X10)
& ( ! [X18] :
( g_false_only(X14,X18)
| g_false_only(X18,X14) )
| ? [X19] :
( g_true_only(X14,X19)
& g_true_only(X19,X14) ) ) )
| ( g_false_only(X14,X10)
& ( ! [X20] :
( g_false_only(X14,X20)
| g_false_only(X20,X14) )
| ( ? [X21] :
( ( g_both(X14,X21)
| g_both(X21,X14) )
& ~ g_false_only(X14,X21)
& ~ g_false_only(X21,X14) )
& ! [X22] :
( ~ g_true_only(X14,X22)
| ~ g_true_only(X22,X14) ) ) ) ) ) )
| ? [X23] :
! [X24] :
( ( g_true_only(X24,X23)
& ! [X25] :
( g_false_only(X24,X25)
| g_false_only(X25,X24) ) )
| ( g_false_only(X24,X23)
& ? [X26] :
( g_true_only(X24,X26)
& g_true_only(X26,X24) ) ) ) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
! [X10,X14] :
( g_true_only(sK16(X14),X14)
| g_both(sK18(X14),X14)
| g_both(X14,sK18(X14))
| ~ sP4(X14,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f10,plain,
! [X10,X14] :
( g_true_only(X14,sK16(X14))
| g_both(sK18(X14),X14)
| g_both(X14,sK18(X14))
| ~ sP4(X14,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f11,plain,
! [X14,X20] :
( g_both(sK17(X14),X14)
| g_both(X14,sK17(X14))
| g_false_only(X20,X14)
| g_false_only(X14,X20)
| ~ sP10(X14) ),
inference(cnf_transformation,[],[f8]) ).
fof(f12,plain,
! [X10,X14] :
( g_true_only(X14,sK16(X14))
| ~ g_false_only(sK18(X14),X14)
| ~ sP4(X14,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f13,plain,
! [X10,X14] :
( g_true_only(X14,sK16(X14))
| ~ g_false_only(X14,sK18(X14))
| ~ sP4(X14,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
! [X10,X14] :
( g_true_only(sK16(X14),X14)
| ~ g_false_only(sK18(X14),X14)
| ~ sP4(X14,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f15,plain,
! [X10,X14] :
( g_true_only(sK16(X14),X14)
| ~ g_false_only(X14,sK18(X14))
| ~ sP4(X14,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f18,plain,
! [X14,X20] :
( ~ g_false_only(sK17(X14),X14)
| g_false_only(X20,X14)
| g_false_only(X14,X20)
| ~ sP10(X14) ),
inference(cnf_transformation,[],[f8]) ).
fof(f19,plain,
! [X14,X20] :
( ~ g_false_only(X14,sK17(X14))
| g_false_only(X20,X14)
| g_false_only(X14,X20)
| ~ sP10(X14) ),
inference(cnf_transformation,[],[f8]) ).
fof(f20,plain,
! [X14,X22,X20] :
( ~ g_true_only(X22,X14)
| ~ g_true_only(X14,X22)
| g_false_only(X20,X14)
| g_false_only(X14,X20)
| ~ sP10(X14) ),
inference(cnf_transformation,[],[f8]) ).
fof(f21,plain,
! [X18,X14] :
( g_true_only(X14,sK15(X14))
| g_false_only(X18,X14)
| g_false_only(X14,X18)
| ~ sP11(X14) ),
inference(cnf_transformation,[],[f8]) ).
fof(f22,plain,
! [X18,X14] :
( g_true_only(sK15(X14),X14)
| g_false_only(X18,X14)
| g_false_only(X14,X18)
| ~ sP11(X14) ),
inference(cnf_transformation,[],[f8]) ).
fof(f23,plain,
! [X2,X1] :
( g_true_only(sK14(X1),X1)
| g_false_only(X2,X1)
| g_false_only(X1,X2)
| ~ g_both(X2,X1)
| ~ g_true_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f24,plain,
! [X2,X1] :
( g_true_only(sK14(X1),X1)
| g_false_only(X2,X1)
| g_false_only(X1,X2)
| ~ g_both(X1,X2)
| ~ g_true_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f25,plain,
! [X2,X1] :
( g_true_only(X1,sK14(X1))
| g_false_only(X2,X1)
| g_false_only(X1,X2)
| ~ g_both(X2,X1)
| ~ g_true_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f26,plain,
! [X2,X1] :
( g_true_only(X1,sK14(X1))
| g_false_only(X2,X1)
| g_false_only(X1,X2)
| ~ g_both(X1,X2)
| ~ g_true_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f27,plain,
! [X1,X8] :
( g_true_only(sK13(X1),X1)
| g_false_only(X8,X1)
| g_false_only(X1,X8)
| ~ g_both(X8,X1)
| ~ g_false_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f28,plain,
! [X1,X8] :
( g_true_only(sK13(X1),X1)
| g_false_only(X8,X1)
| g_false_only(X1,X8)
| ~ g_both(X1,X8)
| ~ g_false_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
! [X1,X8] :
( g_true_only(X1,sK13(X1))
| g_false_only(X8,X1)
| g_false_only(X1,X8)
| ~ g_both(X8,X1)
| ~ g_false_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
! [X1,X8] :
( g_true_only(X1,sK13(X1))
| g_false_only(X8,X1)
| g_false_only(X1,X8)
| ~ g_both(X1,X8)
| ~ g_false_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f31,plain,
! [X11,X12] :
( g_false_only(X12,X11)
| g_false_only(X11,X12)
| ~ g_both(X12,X11)
| ~ sP6(X11) ),
inference(cnf_transformation,[],[f8]) ).
fof(f33,plain,
! [X11] :
( g_true_only(sK12(X11),X11)
| ~ sP5(X11) ),
inference(cnf_transformation,[],[f8]) ).
fof(f34,plain,
! [X11] :
( g_true_only(X11,sK12(X11))
| ~ sP5(X11) ),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
! [X24,X25] :
( g_false_only(X25,X24)
| g_false_only(X24,X25)
| ~ sP9(X25,X24) ),
inference(cnf_transformation,[],[f8]) ).
fof(f36,plain,
! [X1,X4] :
( ~ g_true_only(X4,X1)
| ~ g_true_only(X1,X4)
| ~ g_true_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f37,plain,
! [X1] :
( ~ g_false_only(sK8(X1),X1)
| ~ g_both(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f38,plain,
! [X1] :
( ~ g_false_only(X1,sK8(X1))
| ~ g_both(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
! [X1,X6] :
( ~ g_true_only(X6,X1)
| ~ g_true_only(X1,X6)
| ~ g_both(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f40,plain,
! [X1] :
( ~ g_false_only(sK7(X1),X1)
| ~ g_false_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f41,plain,
! [X1] :
( ~ g_false_only(X1,sK7(X1))
| ~ g_false_only(X1,sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f42,plain,
! [X10,X14] :
( g_true_only(X14,X10)
| ~ sP4(X14,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f51,plain,
! [X10,X11,X24,X25] :
( g_true_only(sK3(X24),X24)
| sP9(X25,X24)
| sP10(sK2(X10))
| g_both(sK2(X10),X10)
| sP4(sK2(X10),X10)
| sP5(X11)
| sP6(X11)
| ~ g_both(X11,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f52,plain,
! [X10,X11,X24,X25] :
( g_true_only(X24,sK3(X24))
| sP9(X25,X24)
| sP10(sK2(X10))
| g_both(sK2(X10),X10)
| sP4(sK2(X10),X10)
| sP5(X11)
| sP6(X11)
| ~ g_both(X11,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f55,plain,
! [X10,X11,X24,X25] :
( g_true_only(sK3(X24),X24)
| sP9(X25,X24)
| g_false_only(sK2(X10),X10)
| g_both(sK2(X10),X10)
| sP4(sK2(X10),X10)
| sP5(X11)
| sP6(X11)
| ~ g_both(X11,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f56,plain,
! [X10,X11,X24,X25] :
( g_true_only(X24,sK3(X24))
| sP9(X25,X24)
| g_false_only(sK2(X10),X10)
| g_both(sK2(X10),X10)
| sP4(sK2(X10),X10)
| sP5(X11)
| sP6(X11)
| ~ g_both(X11,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f57,plain,
! [X10,X11,X24,X25] :
( g_true_only(sK3(X24),X24)
| sP9(X25,X24)
| g_false_only(sK2(X10),X10)
| sP11(sK2(X10))
| sP4(sK2(X10),X10)
| sP5(X11)
| sP6(X11)
| ~ g_both(X11,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f58,plain,
! [X10,X11,X24,X25] :
( g_true_only(X24,sK3(X24))
| sP9(X25,X24)
| g_false_only(sK2(X10),X10)
| sP11(sK2(X10))
| sP4(sK2(X10),X10)
| sP5(X11)
| sP6(X11)
| ~ g_both(X11,X10) ),
inference(cnf_transformation,[],[f8]) ).
fof(f67,plain,
! [X0,X1] :
( ~ g_false(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f3]) ).
fof(f71,plain,
! [X0,X1] :
( g_true(X0,X1)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f73,plain,
! [X0,X1] :
( ~ g_true(X0,X1)
| ~ g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f74,plain,
! [X0,X1] :
( g_false(X0,X1)
| ~ g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f5]) ).
fof(f76,plain,
! [X0,X1] :
( g_false_only(X0,X1)
| g_both(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f85,plain,
! [X10,X11,X24,X25] :
( ~ g_true_only(X24,sK3(X24))
| sP9(X25,X24)
| ~ g_false_only(sK2(X10),X10)
| ~ sP11(sK2(X10))
| sP4(sK2(X10),X10)
| ~ sP5(X11)
| ~ sP6(X11)
| ~ g_both(X11,X10) ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f86,plain,
! [X10,X11,X24,X25] :
( ~ g_true_only(sK3(X24),X24)
| sP9(X25,X24)
| ~ g_false_only(sK2(X10),X10)
| ~ sP11(sK2(X10))
| sP4(sK2(X10),X10)
| ~ sP5(X11)
| ~ sP6(X11)
| ~ g_both(X11,X10) ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f87,plain,
! [X10,X11,X24,X25] :
( ~ g_true_only(X24,sK3(X24))
| sP9(X25,X24)
| ~ g_false_only(sK2(X10),X10)
| g_both(sK2(X10),X10)
| sP4(sK2(X10),X10)
| ~ sP5(X11)
| ~ sP6(X11)
| ~ g_both(X11,X10) ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f88,plain,
! [X10,X11,X24,X25] :
( ~ g_true_only(sK3(X24),X24)
| sP9(X25,X24)
| ~ g_false_only(sK2(X10),X10)
| g_both(sK2(X10),X10)
| sP4(sK2(X10),X10)
| ~ sP5(X11)
| ~ sP6(X11)
| ~ g_both(X11,X10) ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f91,plain,
! [X10,X11,X24,X25] :
( ~ g_true_only(X24,sK3(X24))
| sP9(X25,X24)
| sP10(sK2(X10))
| g_both(sK2(X10),X10)
| sP4(sK2(X10),X10)
| ~ sP5(X11)
| ~ sP6(X11)
| ~ g_both(X11,X10) ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f92,plain,
! [X10,X11,X24,X25] :
( ~ g_true_only(sK3(X24),X24)
| sP9(X25,X24)
| sP10(sK2(X10))
| g_both(sK2(X10),X10)
| sP4(sK2(X10),X10)
| ~ sP5(X11)
| ~ sP6(X11)
| ~ g_both(X11,X10) ),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f101,plain,
! [X10,X14] :
( ~ sP4(X14,X10)
| ~ g_true_only(X14,X10) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f102,plain,
! [X1] :
( g_false_only(X1,sK7(X1))
| g_false_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f103,plain,
! [X1] :
( g_false_only(sK7(X1),X1)
| g_false_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f104,plain,
! [X1,X6] :
( ~ g_both(X1,sK0)
| g_true_only(X1,X6)
| g_true_only(X6,X1) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f105,plain,
! [X1] :
( g_false_only(X1,sK8(X1))
| ~ g_both(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f106,plain,
! [X1] :
( ~ g_both(X1,sK0)
| g_false_only(sK8(X1),X1) ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f107,plain,
! [X1,X4] :
( g_true_only(X4,X1)
| g_true_only(X1,X4)
| g_true_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f108,plain,
! [X24,X25] :
( ~ sP9(X25,X24)
| ~ g_false_only(X24,X25)
| ~ g_false_only(X25,X24) ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f109,plain,
! [X11] :
( ~ g_true_only(X11,sK12(X11))
| sP5(X11) ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f110,plain,
! [X11] :
( ~ g_true_only(sK12(X11),X11)
| sP5(X11) ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f112,plain,
! [X11,X12] :
( ~ g_both(X12,X11)
| ~ g_false_only(X11,X12)
| ~ g_false_only(X12,X11)
| sP6(X11) ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f113,plain,
! [X1,X8] :
( ~ g_both(X1,X8)
| ~ g_false_only(X8,X1)
| ~ g_false_only(X1,X8)
| ~ g_true_only(X1,sK13(X1))
| g_false_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f114,plain,
! [X1,X8] :
( ~ g_both(X8,X1)
| ~ g_false_only(X8,X1)
| ~ g_false_only(X1,X8)
| ~ g_true_only(X1,sK13(X1))
| g_false_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f115,plain,
! [X1,X8] :
( ~ g_both(X1,X8)
| ~ g_false_only(X8,X1)
| ~ g_false_only(X1,X8)
| ~ g_true_only(sK13(X1),X1)
| g_false_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f116,plain,
! [X1,X8] :
( ~ g_both(X8,X1)
| ~ g_false_only(X8,X1)
| ~ g_false_only(X1,X8)
| ~ g_true_only(sK13(X1),X1)
| g_false_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f117,plain,
! [X2,X1] :
( ~ g_both(X1,X2)
| ~ g_false_only(X2,X1)
| ~ g_false_only(X1,X2)
| ~ g_true_only(X1,sK14(X1))
| g_true_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f118,plain,
! [X2,X1] :
( ~ g_both(X2,X1)
| ~ g_false_only(X2,X1)
| ~ g_false_only(X1,X2)
| ~ g_true_only(X1,sK14(X1))
| g_true_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f119,plain,
! [X2,X1] :
( ~ g_both(X1,X2)
| ~ g_false_only(X2,X1)
| ~ g_false_only(X1,X2)
| ~ g_true_only(sK14(X1),X1)
| g_true_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f24]) ).
fof(f120,plain,
! [X2,X1] :
( ~ g_both(X2,X1)
| ~ g_false_only(X2,X1)
| ~ g_false_only(X1,X2)
| ~ g_true_only(sK14(X1),X1)
| g_true_only(X1,sK0) ),
inference(consistent_polarity_flipping,[],[f23]) ).
fof(f121,plain,
! [X18,X14] :
( ~ g_true_only(sK15(X14),X14)
| ~ g_false_only(X18,X14)
| ~ g_false_only(X14,X18)
| sP11(X14) ),
inference(consistent_polarity_flipping,[],[f22]) ).
fof(f122,plain,
! [X18,X14] :
( ~ g_true_only(X14,sK15(X14))
| ~ g_false_only(X18,X14)
| ~ g_false_only(X14,X18)
| sP11(X14) ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f123,plain,
! [X14,X22,X20] :
( ~ sP10(X14)
| g_true_only(X14,X22)
| ~ g_false_only(X20,X14)
| ~ g_false_only(X14,X20)
| g_true_only(X22,X14) ),
inference(consistent_polarity_flipping,[],[f20]) ).
fof(f124,plain,
! [X14,X20] :
( ~ sP10(X14)
| ~ g_false_only(X20,X14)
| ~ g_false_only(X14,X20)
| g_false_only(X14,sK17(X14)) ),
inference(consistent_polarity_flipping,[],[f19]) ).
fof(f125,plain,
! [X14,X20] :
( ~ sP10(X14)
| ~ g_false_only(X20,X14)
| ~ g_false_only(X14,X20)
| g_false_only(sK17(X14),X14) ),
inference(consistent_polarity_flipping,[],[f18]) ).
fof(f128,plain,
! [X10,X14] :
( ~ sP4(X14,X10)
| g_false_only(X14,sK18(X14))
| ~ g_true_only(sK16(X14),X14) ),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f129,plain,
! [X10,X14] :
( ~ sP4(X14,X10)
| g_false_only(sK18(X14),X14)
| ~ g_true_only(sK16(X14),X14) ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f130,plain,
! [X10,X14] :
( ~ sP4(X14,X10)
| g_false_only(X14,sK18(X14))
| ~ g_true_only(X14,sK16(X14)) ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f131,plain,
! [X10,X14] :
( ~ sP4(X14,X10)
| g_false_only(sK18(X14),X14)
| ~ g_true_only(X14,sK16(X14)) ),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f132,plain,
! [X14,X20] :
( ~ sP10(X14)
| g_both(X14,sK17(X14))
| ~ g_false_only(X20,X14)
| ~ g_false_only(X14,X20)
| g_both(sK17(X14),X14) ),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f133,plain,
! [X10,X14] :
( ~ sP4(X14,X10)
| g_both(sK18(X14),X14)
| g_both(X14,sK18(X14))
| ~ g_true_only(X14,sK16(X14)) ),
inference(consistent_polarity_flipping,[],[f10]) ).
fof(f134,plain,
! [X10,X14] :
( ~ sP4(X14,X10)
| g_both(sK18(X14),X14)
| g_both(X14,sK18(X14))
| ~ g_true_only(sK16(X14),X14) ),
inference(consistent_polarity_flipping,[],[f9]) ).
fof(f137,plain,
! [X0,X1] :
( ~ g_false(X0,X1)
| g_true_only(X0,X1) ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f139,plain,
! [X0,X1] :
( g_false(X0,X1)
| g_false_only(X0,X1) ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f140,plain,
! [X0,X1] :
( ~ g_true(X0,X1)
| g_false_only(X0,X1) ),
inference(consistent_polarity_flipping,[],[f73]) ).
fof(f141,plain,
! [X0,X1] :
( ~ g_false_only(X0,X1)
| g_both(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f143,definition,
( spl19_1
<=> ! [X11,X10] :
( sP10(sK2(X10))
| ~ sP5(X11)
| ~ g_both(X11,X10)
| ~ sP6(X11)
| sP4(sK2(X10),X10)
| g_both(sK2(X10),X10) ) ),
introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition]) ).
fof(f144,plain,
( ! [X10,X11] :
( ~ sP6(X11)
| ~ sP5(X11)
| ~ g_both(X11,X10)
| sP10(sK2(X10))
| sP4(sK2(X10),X10)
| g_both(sK2(X10),X10) )
| ~ spl19_1 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f159,definition,
( spl19_5
<=> ! [X11,X10] :
( ~ g_false_only(sK2(X10),X10)
| ~ sP5(X11)
| ~ g_both(X11,X10)
| ~ sP6(X11)
| sP4(sK2(X10),X10)
| g_both(sK2(X10),X10) ) ),
introduced(definition,[new_symbols(definition,[spl19_5])],[avatar_definition]) ).
fof(f160,plain,
( ! [X10,X11] :
( ~ sP6(X11)
| ~ sP5(X11)
| ~ g_both(X11,X10)
| ~ g_false_only(sK2(X10),X10)
| sP4(sK2(X10),X10)
| g_both(sK2(X10),X10) )
| ~ spl19_5 ),
inference(avatar_component_clause,[],[f159]) ).
fof(f164,definition,
( spl19_6
<=> ! [X11,X10] :
( ~ g_false_only(sK2(X10),X10)
| ~ sP5(X11)
| ~ g_both(X11,X10)
| ~ sP6(X11)
| sP4(sK2(X10),X10)
| ~ sP11(sK2(X10)) ) ),
introduced(definition,[new_symbols(definition,[spl19_6])],[avatar_definition]) ).
fof(f165,plain,
( ! [X10,X11] :
( ~ sP11(sK2(X10))
| ~ sP5(X11)
| ~ g_both(X11,X10)
| ~ sP6(X11)
| sP4(sK2(X10),X10)
| ~ g_false_only(sK2(X10),X10) )
| ~ spl19_6 ),
inference(avatar_component_clause,[],[f164]) ).
fof(f169,definition,
( spl19_7
<=> ! [X25,X24] :
( ~ g_true_only(sK3(X24),X24)
| sP9(X25,X24) ) ),
introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition]) ).
fof(f170,plain,
( ! [X24,X25] :
( ~ g_true_only(sK3(X24),X24)
| sP9(X25,X24) )
| ~ spl19_7 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f171,plain,
( spl19_1
| spl19_7 ),
inference(avatar_split_clause,[],[f92,f169,f143]) ).
fof(f173,definition,
( spl19_8
<=> ! [X25,X24] :
( ~ g_true_only(X24,sK3(X24))
| sP9(X25,X24) ) ),
introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition]) ).
fof(f174,plain,
( ! [X24,X25] :
( ~ g_true_only(X24,sK3(X24))
| sP9(X25,X24) )
| ~ spl19_8 ),
inference(avatar_component_clause,[],[f173]) ).
fof(f175,plain,
( spl19_1
| spl19_8 ),
inference(avatar_split_clause,[],[f91,f173,f143]) ).
fof(f178,plain,
( spl19_5
| spl19_7 ),
inference(avatar_split_clause,[],[f88,f169,f159]) ).
fof(f179,plain,
( spl19_5
| spl19_8 ),
inference(avatar_split_clause,[],[f87,f173,f159]) ).
fof(f180,plain,
( spl19_6
| spl19_7 ),
inference(avatar_split_clause,[],[f86,f169,f164]) ).
fof(f181,plain,
( spl19_6
| spl19_8 ),
inference(avatar_split_clause,[],[f85,f173,f164]) ).
fof(f217,plain,
! [X0] :
( g_true_only(X0,sK12(X0))
| g_true_only(sK12(X0),sK0)
| sP5(X0) ),
inference(resolution,[],[f107,f110]) ).
fof(f222,plain,
( g_true_only(sK0,sK0)
| g_true_only(sK0,sK0) ),
inference(factoring,[],[f107]) ).
fof(f223,plain,
! [X0] :
( g_true_only(sK0,X0)
| g_true_only(X0,sK0) ),
inference(factoring,[],[f107]) ).
fof(f224,plain,
g_true_only(sK0,sK0),
inference(duplicate_literal_removal,[],[f222]) ).
fof(f226,definition,
( spl19_14
<=> sP5(sK0) ),
introduced(definition,[new_symbols(definition,[spl19_14])],[avatar_definition]) ).
fof(f228,plain,
( sP5(sK0)
| ~ spl19_14 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f242,definition,
( spl19_18
<=> ! [X1] : sP9(X1,sK0) ),
introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition]) ).
fof(f243,plain,
( ! [X1] : sP9(X1,sK0)
| ~ spl19_18 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f245,plain,
! [X0] :
( g_true_only(sK12(X0),sK0)
| sP5(X0) ),
inference(forward_subsumption_resolution,[],[f217,f109]) ).
fof(f273,plain,
( ! [X0] :
( ~ g_false_only(sK0,X0)
| ~ g_false_only(X0,sK0) )
| ~ spl19_18 ),
inference(resolution,[],[f243,f108]) ).
fof(f286,definition,
( spl19_24
<=> ! [X0] :
( ~ g_false_only(X0,sK0)
| ~ g_false_only(sK0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl19_24])],[avatar_definition]) ).
fof(f287,plain,
( ! [X0] :
( ~ g_false_only(sK0,X0)
| ~ g_false_only(X0,sK0) )
| ~ spl19_24 ),
inference(avatar_component_clause,[],[f286]) ).
fof(f296,plain,
( ! [X0] :
( g_true_only(sK0,sK3(sK0))
| sP9(X0,sK0) )
| ~ spl19_7 ),
inference(resolution,[],[f223,f170]) ).
fof(f302,plain,
( ! [X0] : sP9(X0,sK0)
| ~ spl19_7
| ~ spl19_8 ),
inference(forward_subsumption_resolution,[],[f296,f174]) ).
fof(f304,plain,
! [X0,X1] :
( g_true_only(X0,X1)
| g_false_only(X0,X1) ),
inference(resolution,[],[f139,f137]) ).
fof(f306,plain,
! [X0,X1] :
( ~ g_both(X0,X1)
| g_false_only(X0,X1) ),
inference(resolution,[],[f140,f71]) ).
fof(f307,plain,
( sP5(sK0)
| sP5(sK0) ),
inference(resolution,[],[f245,f110]) ).
fof(f308,plain,
sP5(sK0),
inference(duplicate_literal_removal,[],[f307]) ).
fof(f319,plain,
( spl19_24
| ~ spl19_18 ),
inference(avatar_split_clause,[],[f273,f242,f286]) ).
fof(f320,plain,
( spl19_18
| ~ spl19_7
| ~ spl19_8 ),
inference(avatar_split_clause,[],[f302,f173,f169,f242]) ).
fof(f330,plain,
! [X0] :
( ~ g_true_only(X0,sK7(X0))
| g_both(X0,sK7(X0))
| g_false_only(X0,sK0) ),
inference(resolution,[],[f141,f102]) ).
fof(f332,plain,
! [X0] :
( ~ g_true_only(sK7(X0),X0)
| g_both(sK7(X0),X0)
| g_false_only(X0,sK0) ),
inference(resolution,[],[f141,f103]) ).
fof(f335,plain,
( ~ g_false_only(sK7(sK0),sK0)
| g_false_only(sK0,sK0)
| ~ spl19_24 ),
inference(resolution,[],[f287,f102]) ).
fof(f336,plain,
( ~ g_false_only(sK8(sK0),sK0)
| ~ g_both(sK0,sK0)
| ~ spl19_24 ),
inference(resolution,[],[f287,f105]) ).
fof(f337,plain,
( ~ g_both(sK0,sK0)
| ~ spl19_24 ),
inference(forward_subsumption_resolution,[],[f336,f106]) ).
fof(f338,plain,
( g_false_only(sK0,sK0)
| ~ spl19_24 ),
inference(forward_subsumption_resolution,[],[f335,f103]) ).
fof(f358,plain,
( g_both(sK0,sK0)
| ~ g_true_only(sK0,sK0)
| ~ spl19_24 ),
inference(resolution,[],[f338,f141]) ).
fof(f359,plain,
( ~ g_true_only(sK0,sK0)
| ~ spl19_24 ),
inference(forward_subsumption_resolution,[],[f358,f337]) ).
fof(f362,plain,
( $false
| ~ spl19_24 ),
inference(forward_subsumption_resolution,[],[f359,f224]) ).
fof(f363,plain,
~ spl19_24,
inference(avatar_contradiction_clause,[],[f362]) ).
fof(f369,definition,
( spl19_27
<=> g_false_only(sK0,sK0) ),
introduced(definition,[new_symbols(definition,[spl19_27])],[avatar_definition]) ).
fof(f371,plain,
( g_false_only(sK0,sK0)
| ~ spl19_27 ),
inference(avatar_component_clause,[],[f369]) ).
fof(f373,definition,
( spl19_28
<=> g_true_only(sK13(sK0),sK0) ),
introduced(definition,[new_symbols(definition,[spl19_28])],[avatar_definition]) ).
fof(f375,plain,
( ~ g_true_only(sK13(sK0),sK0)
| spl19_28 ),
inference(avatar_component_clause,[],[f373]) ).
fof(f382,definition,
( spl19_30
<=> g_true_only(sK0,sK13(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_30])],[avatar_definition]) ).
fof(f387,definition,
( spl19_31
<=> sP6(sK0) ),
introduced(definition,[new_symbols(definition,[spl19_31])],[avatar_definition]) ).
fof(f389,plain,
( sP6(sK0)
| ~ spl19_31 ),
inference(avatar_component_clause,[],[f387]) ).
fof(f426,plain,
! [X0] :
( g_both(sK7(X0),X0)
| g_false_only(X0,sK0)
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0) ),
inference(resolution,[],[f332,f107]) ).
fof(f452,definition,
( spl19_41
<=> g_both(sK7(sK0),sK0) ),
introduced(definition,[new_symbols(definition,[spl19_41])],[avatar_definition]) ).
fof(f454,plain,
( g_both(sK7(sK0),sK0)
| ~ spl19_41 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f488,plain,
( g_both(sK0,sK0)
| ~ g_true_only(sK0,sK0)
| ~ spl19_27 ),
inference(resolution,[],[f371,f141]) ).
fof(f489,plain,
( g_both(sK0,sK0)
| ~ spl19_27 ),
inference(forward_subsumption_resolution,[],[f488,f224]) ).
fof(f495,plain,
( ~ g_false_only(sK0,sK0)
| ~ g_false_only(sK0,sK0)
| sP6(sK0)
| ~ spl19_27 ),
inference(resolution,[],[f489,f112]) ).
fof(f531,plain,
! [X0,X1] :
( ~ g_false_only(X0,X1)
| ~ g_false_only(X1,X0)
| g_false_only(X0,sK15(X0))
| sP11(X0) ),
inference(resolution,[],[f304,f122]) ).
fof(f537,plain,
! [X0,X1] :
( ~ g_false_only(X0,X1)
| ~ g_false_only(X1,X0)
| g_false_only(sK15(X0),X0)
| sP11(X0) ),
inference(resolution,[],[f304,f121]) ).
fof(f549,plain,
( ~ g_false_only(sK7(sK0),sK0)
| ~ g_false_only(sK0,sK7(sK0))
| ~ g_true_only(sK0,sK13(sK0))
| g_false_only(sK0,sK0)
| ~ spl19_41 ),
inference(resolution,[],[f454,f114]) ).
fof(f551,plain,
( ~ g_false_only(sK7(sK0),sK0)
| ~ g_false_only(sK0,sK7(sK0))
| ~ g_true_only(sK13(sK0),sK0)
| g_false_only(sK0,sK0)
| ~ spl19_41 ),
inference(resolution,[],[f454,f116]) ).
fof(f560,plain,
( ~ g_false_only(sK0,sK7(sK0))
| ~ g_true_only(sK13(sK0),sK0)
| g_false_only(sK0,sK0)
| ~ spl19_41 ),
inference(forward_subsumption_resolution,[],[f551,f103]) ).
fof(f561,plain,
( ~ g_false_only(sK0,sK7(sK0))
| ~ g_true_only(sK0,sK13(sK0))
| g_false_only(sK0,sK0)
| ~ spl19_41 ),
inference(forward_subsumption_resolution,[],[f549,f103]) ).
fof(f587,definition,
( spl19_52
<=> g_true_only(sK7(sK0),sK0) ),
introduced(definition,[new_symbols(definition,[spl19_52])],[avatar_definition]) ).
fof(f589,plain,
( g_true_only(sK7(sK0),sK0)
| ~ spl19_52 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f600,plain,
( ~ g_true_only(sK13(sK0),sK0)
| g_false_only(sK0,sK0)
| ~ spl19_41 ),
inference(forward_subsumption_resolution,[],[f560,f102]) ).
fof(f601,plain,
( ~ g_true_only(sK0,sK13(sK0))
| g_false_only(sK0,sK0)
| ~ spl19_41 ),
inference(forward_subsumption_resolution,[],[f561,f102]) ).
fof(f656,plain,
( g_true_only(sK0,sK13(sK0))
| spl19_28 ),
inference(resolution,[],[f375,f223]) ).
fof(f661,plain,
( spl19_30
| spl19_28 ),
inference(avatar_split_clause,[],[f656,f373,f382]) ).
fof(f663,plain,
( ~ g_false_only(sK0,sK0)
| sP6(sK0)
| ~ spl19_27 ),
inference(duplicate_literal_removal,[],[f495]) ).
fof(f674,plain,
( spl19_31
| ~ spl19_27
| ~ spl19_27 ),
inference(avatar_split_clause,[],[f663,f369,f369,f387]) ).
fof(f679,plain,
( spl19_27
| ~ spl19_28
| ~ spl19_41 ),
inference(avatar_split_clause,[],[f600,f452,f373,f369]) ).
fof(f680,plain,
( spl19_27
| ~ spl19_30
| ~ spl19_41 ),
inference(avatar_split_clause,[],[f601,f452,f382,f369]) ).
fof(f685,plain,
( ! [X0] :
( ~ sP5(sK0)
| ~ g_both(sK0,X0)
| ~ g_false_only(sK2(X0),X0)
| sP4(sK2(X0),X0)
| g_both(sK2(X0),X0) )
| ~ spl19_5
| ~ spl19_31 ),
inference(resolution,[],[f389,f160]) ).
fof(f686,plain,
( ! [X0] :
( ~ sP5(sK0)
| ~ g_both(sK0,X0)
| sP10(sK2(X0))
| sP4(sK2(X0),X0)
| g_both(sK2(X0),X0) )
| ~ spl19_1
| ~ spl19_31 ),
inference(resolution,[],[f389,f144]) ).
fof(f687,plain,
( ! [X0] :
( ~ g_both(sK0,X0)
| sP10(sK2(X0))
| sP4(sK2(X0),X0)
| g_both(sK2(X0),X0) )
| ~ spl19_1
| ~ spl19_14
| ~ spl19_31 ),
inference(forward_subsumption_resolution,[],[f686,f228]) ).
fof(f688,plain,
( ! [X0] :
( ~ g_false_only(sK2(X0),X0)
| ~ g_both(sK0,X0)
| sP4(sK2(X0),X0)
| g_both(sK2(X0),X0) )
| ~ spl19_5
| ~ spl19_14
| ~ spl19_31 ),
inference(forward_subsumption_resolution,[],[f685,f228]) ).
fof(f745,plain,
! [X0] :
( ~ g_false_only(sK8(X0),X0)
| g_false_only(X0,sK15(X0))
| sP11(X0)
| ~ g_both(X0,sK0) ),
inference(resolution,[],[f531,f105]) ).
fof(f760,plain,
! [X0] :
( ~ g_both(X0,sK0)
| sP11(X0)
| g_false_only(X0,sK15(X0)) ),
inference(forward_subsumption_resolution,[],[f745,f106]) ).
fof(f795,plain,
! [X0] :
( ~ g_false_only(sK8(X0),X0)
| g_false_only(sK15(X0),X0)
| sP11(X0)
| ~ g_both(X0,sK0) ),
inference(resolution,[],[f537,f105]) ).
fof(f810,plain,
! [X0] :
( ~ g_both(X0,sK0)
| sP11(X0)
| g_false_only(sK15(X0),X0) ),
inference(forward_subsumption_resolution,[],[f795,f106]) ).
fof(f821,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_false_only(sK7(X0),X0)
| ~ g_true_only(sK7(X0),sK14(sK7(X0)))
| g_true_only(sK7(X0),sK0) ),
inference(resolution,[],[f426,f117]) ).
fof(f823,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_false_only(sK7(X0),X0)
| ~ g_true_only(sK14(sK7(X0)),sK7(X0))
| g_true_only(sK7(X0),sK0) ),
inference(resolution,[],[f426,f119]) ).
fof(f827,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_false_only(sK7(X0),X0)
| ~ g_true_only(sK14(sK7(X0)),sK7(X0)) ),
inference(duplicate_literal_removal,[],[f823]) ).
fof(f828,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_false_only(sK7(X0),X0)
| ~ g_true_only(sK7(X0),sK14(sK7(X0))) ),
inference(duplicate_literal_removal,[],[f821]) ).
fof(f832,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_true_only(sK14(sK7(X0)),sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f827,f103]) ).
fof(f834,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_true_only(sK7(X0),sK14(sK7(X0))) ),
inference(forward_subsumption_resolution,[],[f828,f103]) ).
fof(f842,plain,
! [X0] :
( ~ g_true_only(sK14(sK7(X0)),sK7(X0))
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| g_false_only(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f832,f304]) ).
fof(f844,plain,
! [X0] :
( ~ g_true_only(sK7(X0),sK14(sK7(X0)))
| g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| g_false_only(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f834,f304]) ).
fof(f907,plain,
( g_both(sK7(sK0),sK0)
| g_false_only(sK0,sK0)
| ~ spl19_52 ),
inference(resolution,[],[f589,f332]) ).
fof(f1281,plain,
! [X0] :
( g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK14(sK7(X0)))
| g_true_only(sK7(X0),sK0) ),
inference(resolution,[],[f842,f107]) ).
fof(f1282,plain,
! [X0] :
( g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK14(sK7(X0))) ),
inference(duplicate_literal_removal,[],[f1281]) ).
fof(f1684,plain,
( sP10(sK2(sK0))
| sP4(sK2(sK0),sK0)
| g_both(sK2(sK0),sK0)
| ~ spl19_1
| ~ spl19_14
| ~ spl19_27
| ~ spl19_31 ),
inference(resolution,[],[f687,f489]) ).
fof(f1687,definition,
( spl19_140
<=> g_both(sK2(sK0),sK0) ),
introduced(definition,[new_symbols(definition,[spl19_140])],[avatar_definition]) ).
fof(f1689,plain,
( g_both(sK2(sK0),sK0)
| ~ spl19_140 ),
inference(avatar_component_clause,[],[f1687]) ).
fof(f1691,definition,
( spl19_141
<=> sP4(sK2(sK0),sK0) ),
introduced(definition,[new_symbols(definition,[spl19_141])],[avatar_definition]) ).
fof(f1693,plain,
( sP4(sK2(sK0),sK0)
| ~ spl19_141 ),
inference(avatar_component_clause,[],[f1691]) ).
fof(f1695,definition,
( spl19_142
<=> sP10(sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_142])],[avatar_definition]) ).
fof(f1696,plain,
( ~ sP10(sK2(sK0))
| spl19_142 ),
inference(avatar_component_clause,[],[f1695]) ).
fof(f1697,plain,
( sP10(sK2(sK0))
| ~ spl19_142 ),
inference(avatar_component_clause,[],[f1695]) ).
fof(f1710,plain,
( sP11(sK2(sK0))
| g_false_only(sK15(sK2(sK0)),sK2(sK0))
| ~ spl19_140 ),
inference(resolution,[],[f1689,f810]) ).
fof(f1713,plain,
( ! [X0] :
( g_true_only(sK2(sK0),X0)
| g_true_only(X0,sK2(sK0)) )
| ~ spl19_140 ),
inference(resolution,[],[f1689,f104]) ).
fof(f1726,plain,
( g_false_only(sK2(sK0),sK0)
| ~ spl19_140 ),
inference(resolution,[],[f1689,f306]) ).
fof(f1738,definition,
( spl19_145
<=> g_false_only(sK2(sK0),sK0) ),
introduced(definition,[new_symbols(definition,[spl19_145])],[avatar_definition]) ).
fof(f1739,plain,
( g_false_only(sK2(sK0),sK0)
| ~ spl19_145 ),
inference(avatar_component_clause,[],[f1738]) ).
fof(f1740,plain,
( ~ g_false_only(sK2(sK0),sK0)
| spl19_145 ),
inference(avatar_component_clause,[],[f1738]) ).
fof(f1752,definition,
( spl19_148
<=> g_false_only(sK2(sK0),sK15(sK2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_148])],[avatar_definition]) ).
fof(f1754,plain,
( g_false_only(sK2(sK0),sK15(sK2(sK0)))
| ~ spl19_148 ),
inference(avatar_component_clause,[],[f1752]) ).
fof(f1756,definition,
( spl19_149
<=> sP11(sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_149])],[avatar_definition]) ).
fof(f1758,plain,
( sP11(sK2(sK0))
| ~ spl19_149 ),
inference(avatar_component_clause,[],[f1756]) ).
fof(f1761,definition,
( spl19_150
<=> g_false_only(sK15(sK2(sK0)),sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_150])],[avatar_definition]) ).
fof(f1763,plain,
( g_false_only(sK15(sK2(sK0)),sK2(sK0))
| ~ spl19_150 ),
inference(avatar_component_clause,[],[f1761]) ).
fof(f1766,definition,
( spl19_151
<=> g_true_only(sK2(sK0),sK0) ),
introduced(definition,[new_symbols(definition,[spl19_151])],[avatar_definition]) ).
fof(f1767,plain,
( ~ g_true_only(sK2(sK0),sK0)
| spl19_151 ),
inference(avatar_component_clause,[],[f1766]) ).
fof(f1770,definition,
( spl19_152
<=> g_true_only(sK14(sK2(sK0)),sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_152])],[avatar_definition]) ).
fof(f1772,plain,
( ~ g_true_only(sK14(sK2(sK0)),sK2(sK0))
| spl19_152 ),
inference(avatar_component_clause,[],[f1770]) ).
fof(f1775,definition,
( spl19_153
<=> g_true_only(sK2(sK0),sK14(sK2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_153])],[avatar_definition]) ).
fof(f1788,plain,
( ! [X0] :
( g_both(sK2(sK0),sK17(sK2(sK0)))
| ~ g_false_only(X0,sK2(sK0))
| ~ g_false_only(sK2(sK0),X0)
| g_both(sK17(sK2(sK0)),sK2(sK0)) )
| ~ spl19_142 ),
inference(resolution,[],[f1697,f132]) ).
fof(f1793,definition,
( spl19_154
<=> g_false_only(sK2(sK0),sK17(sK2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_154])],[avatar_definition]) ).
fof(f1795,plain,
( g_false_only(sK2(sK0),sK17(sK2(sK0)))
| ~ spl19_154 ),
inference(avatar_component_clause,[],[f1793]) ).
fof(f1797,definition,
( spl19_155
<=> ! [X0] :
( ~ g_false_only(X0,sK2(sK0))
| ~ g_false_only(sK2(sK0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl19_155])],[avatar_definition]) ).
fof(f1798,plain,
( ! [X0] :
( ~ g_false_only(X0,sK2(sK0))
| ~ g_false_only(sK2(sK0),X0) )
| ~ spl19_155 ),
inference(avatar_component_clause,[],[f1797]) ).
fof(f1801,definition,
( spl19_156
<=> g_false_only(sK17(sK2(sK0)),sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_156])],[avatar_definition]) ).
fof(f1803,plain,
( g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ spl19_156 ),
inference(avatar_component_clause,[],[f1801]) ).
fof(f1806,definition,
( spl19_157
<=> ! [X0] :
( g_true_only(sK2(sK0),X0)
| g_true_only(X0,sK2(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl19_157])],[avatar_definition]) ).
fof(f1807,plain,
( ! [X0] :
( g_true_only(sK2(sK0),X0)
| g_true_only(X0,sK2(sK0)) )
| ~ spl19_157 ),
inference(avatar_component_clause,[],[f1806]) ).
fof(f1810,definition,
( spl19_158
<=> g_both(sK17(sK2(sK0)),sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_158])],[avatar_definition]) ).
fof(f1812,plain,
( g_both(sK17(sK2(sK0)),sK2(sK0))
| ~ spl19_158 ),
inference(avatar_component_clause,[],[f1810]) ).
fof(f1814,definition,
( spl19_159
<=> g_both(sK2(sK0),sK17(sK2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_159])],[avatar_definition]) ).
fof(f1816,plain,
( g_both(sK2(sK0),sK17(sK2(sK0)))
| ~ spl19_159 ),
inference(avatar_component_clause,[],[f1814]) ).
fof(f1883,plain,
( ~ g_true_only(sK2(sK0),sK0)
| ~ spl19_141 ),
inference(resolution,[],[f1693,f101]) ).
fof(f1893,definition,
( spl19_163
<=> g_true_only(sK16(sK2(sK0)),sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_163])],[avatar_definition]) ).
fof(f1895,plain,
( ~ g_true_only(sK16(sK2(sK0)),sK2(sK0))
| spl19_163 ),
inference(avatar_component_clause,[],[f1893]) ).
fof(f1897,definition,
( spl19_164
<=> g_both(sK2(sK0),sK18(sK2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_164])],[avatar_definition]) ).
fof(f1899,plain,
( g_both(sK2(sK0),sK18(sK2(sK0)))
| ~ spl19_164 ),
inference(avatar_component_clause,[],[f1897]) ).
fof(f1901,definition,
( spl19_165
<=> g_both(sK18(sK2(sK0)),sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_165])],[avatar_definition]) ).
fof(f1903,plain,
( g_both(sK18(sK2(sK0)),sK2(sK0))
| ~ spl19_165 ),
inference(avatar_component_clause,[],[f1901]) ).
fof(f1906,definition,
( spl19_166
<=> g_true_only(sK2(sK0),sK16(sK2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_166])],[avatar_definition]) ).
fof(f1911,definition,
( spl19_167
<=> g_false_only(sK18(sK2(sK0)),sK2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl19_167])],[avatar_definition]) ).
fof(f1916,definition,
( spl19_168
<=> g_false_only(sK2(sK0),sK18(sK2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_168])],[avatar_definition]) ).
fof(f1924,plain,
( ~ spl19_151
| ~ spl19_141 ),
inference(avatar_split_clause,[],[f1883,f1691,f1766]) ).
fof(f1958,plain,
! [X0] :
( g_true_only(X0,sK7(X0))
| g_true_only(sK7(X0),sK0)
| g_false_only(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f1282,f844]) ).
fof(f1959,plain,
! [X0] :
( g_true_only(sK7(X0),sK0)
| g_false_only(X0,sK0)
| g_both(X0,sK7(X0))
| g_false_only(X0,sK0) ),
inference(resolution,[],[f1958,f330]) ).
fof(f1963,plain,
! [X0] :
( g_both(X0,sK7(X0))
| g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK0) ),
inference(duplicate_literal_removal,[],[f1959]) ).
fof(f1992,plain,
( ! [X0] :
( g_true_only(X0,sK2(sK0))
| g_true_only(sK2(sK0),X0) )
| spl19_151 ),
inference(resolution,[],[f1767,f107]) ).
fof(f1996,plain,
( spl19_157
| spl19_151 ),
inference(avatar_split_clause,[],[f1992,f1766,f1806]) ).
fof(f2078,plain,
( ~ g_both(sK0,sK0)
| sP4(sK2(sK0),sK0)
| g_both(sK2(sK0),sK0)
| ~ spl19_5
| ~ spl19_14
| ~ spl19_31
| ~ spl19_145 ),
inference(resolution,[],[f1739,f688]) ).
fof(f2115,plain,
( g_true_only(sK2(sK0),sK16(sK2(sK0)))
| g_true_only(sK2(sK0),sK0)
| spl19_163 ),
inference(resolution,[],[f1895,f107]) ).
fof(f2123,plain,
( spl19_150
| spl19_149
| ~ spl19_140 ),
inference(avatar_split_clause,[],[f1710,f1687,f1756,f1761]) ).
fof(f2126,plain,
( spl19_157
| ~ spl19_140 ),
inference(avatar_split_clause,[],[f1713,f1687,f1806]) ).
fof(f2135,plain,
( spl19_158
| spl19_155
| spl19_159
| ~ spl19_142 ),
inference(avatar_split_clause,[],[f1788,f1695,f1814,f1797,f1810]) ).
fof(f2139,plain,
( spl19_151
| spl19_166
| spl19_163 ),
inference(avatar_split_clause,[],[f2115,f1893,f1906,f1766]) ).
fof(f2148,plain,
spl19_14,
inference(avatar_split_clause,[],[f308,f226]) ).
fof(f2161,plain,
( ! [X0,X1] :
( g_true_only(sK2(sK0),X0)
| ~ g_false_only(X1,sK2(sK0))
| ~ g_false_only(sK2(sK0),X1)
| g_true_only(X0,sK2(sK0)) )
| ~ spl19_142 ),
inference(resolution,[],[f1697,f123]) ).
fof(f2162,plain,
( ! [X0] :
( ~ g_false_only(X0,sK2(sK0))
| ~ g_false_only(sK2(sK0),X0)
| g_false_only(sK17(sK2(sK0)),sK2(sK0)) )
| ~ spl19_142 ),
inference(resolution,[],[f1697,f125]) ).
fof(f2163,plain,
( ! [X0] :
( ~ g_false_only(X0,sK2(sK0))
| ~ g_false_only(sK2(sK0),X0)
| g_false_only(sK2(sK0),sK17(sK2(sK0))) )
| ~ spl19_142 ),
inference(resolution,[],[f1697,f124]) ).
fof(f2164,plain,
( spl19_154
| spl19_155
| ~ spl19_142 ),
inference(avatar_split_clause,[],[f2163,f1695,f1797,f1793]) ).
fof(f2165,plain,
( spl19_156
| spl19_155
| ~ spl19_142 ),
inference(avatar_split_clause,[],[f2162,f1695,f1797,f1801]) ).
fof(f2166,plain,
( spl19_155
| spl19_157
| ~ spl19_142 ),
inference(avatar_split_clause,[],[f2161,f1695,f1806,f1797]) ).
fof(f2518,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(sK7(X0),X0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_true_only(X0,sK13(X0))
| g_false_only(X0,sK0) ),
inference(resolution,[],[f1963,f113]) ).
fof(f2520,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(sK7(X0),X0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_true_only(sK13(X0),X0)
| g_false_only(X0,sK0) ),
inference(resolution,[],[f1963,f115]) ).
fof(f2533,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(sK7(X0),X0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_true_only(sK13(X0),X0) ),
inference(duplicate_literal_removal,[],[f2520]) ).
fof(f2534,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(sK7(X0),X0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_true_only(X0,sK13(X0)) ),
inference(duplicate_literal_removal,[],[f2518]) ).
fof(f2540,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_true_only(sK13(X0),X0) ),
inference(forward_subsumption_resolution,[],[f2533,f103]) ).
fof(f2542,plain,
! [X0] :
( g_false_only(X0,sK0)
| g_true_only(sK7(X0),sK0)
| ~ g_false_only(X0,sK7(X0))
| ~ g_true_only(X0,sK13(X0)) ),
inference(forward_subsumption_resolution,[],[f2534,f103]) ).
fof(f2545,plain,
! [X0] :
( ~ g_true_only(sK13(X0),X0)
| g_true_only(sK7(X0),sK0)
| g_false_only(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f2540,f102]) ).
fof(f2546,plain,
! [X0] :
( ~ g_true_only(X0,sK13(X0))
| g_true_only(sK7(X0),sK0)
| g_false_only(X0,sK0) ),
inference(forward_subsumption_resolution,[],[f2542,f102]) ).
fof(f2968,definition,
( spl19_269
<=> g_true_only(sK2(sK0),sK13(sK2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl19_269])],[avatar_definition]) ).
fof(f3047,plain,
( ~ g_false_only(sK2(sK0),sK7(sK2(sK0)))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_155 ),
inference(resolution,[],[f1798,f103]) ).
fof(f3050,plain,
( ~ g_false_only(sK2(sK0),sK15(sK2(sK0)))
| ~ spl19_150
| ~ spl19_155 ),
inference(resolution,[],[f1798,f1763]) ).
fof(f3054,plain,
( $false
| ~ spl19_148
| ~ spl19_150
| ~ spl19_155 ),
inference(forward_subsumption_resolution,[],[f3050,f1754]) ).
fof(f3055,plain,
( ~ spl19_148
| ~ spl19_150
| ~ spl19_155 ),
inference(avatar_contradiction_clause,[],[f3054]) ).
fof(f3058,plain,
( g_false_only(sK2(sK0),sK0)
| ~ spl19_155 ),
inference(forward_subsumption_resolution,[],[f3047,f102]) ).
fof(f3061,plain,
( $false
| spl19_145
| ~ spl19_155 ),
inference(forward_subsumption_resolution,[],[f3058,f1740]) ).
fof(f3062,plain,
( spl19_145
| ~ spl19_155 ),
inference(avatar_contradiction_clause,[],[f3061]) ).
fof(f3120,plain,
( ~ g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK17(sK2(sK0)))
| ~ g_true_only(sK2(sK0),sK13(sK2(sK0)))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_159 ),
inference(resolution,[],[f1816,f113]) ).
fof(f3122,plain,
( ~ g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK17(sK2(sK0)))
| ~ g_true_only(sK13(sK2(sK0)),sK2(sK0))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_159 ),
inference(resolution,[],[f1816,f115]) ).
fof(f3185,plain,
( ! [X0] :
( g_true_only(sK2(sK0),sK15(sK2(sK0)))
| ~ g_false_only(X0,sK2(sK0))
| ~ g_false_only(sK2(sK0),X0)
| sP11(sK2(sK0)) )
| ~ spl19_157 ),
inference(resolution,[],[f1807,f121]) ).
fof(f3204,plain,
( ~ g_false_only(sK2(sK0),sK17(sK2(sK0)))
| ~ g_true_only(sK13(sK2(sK0)),sK2(sK0))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_156
| ~ spl19_159 ),
inference(forward_subsumption_resolution,[],[f3122,f1803]) ).
fof(f3208,plain,
( ~ g_true_only(sK13(sK2(sK0)),sK2(sK0))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_154
| ~ spl19_156
| ~ spl19_159 ),
inference(forward_subsumption_resolution,[],[f3204,f1795]) ).
fof(f3209,plain,
( ~ g_true_only(sK13(sK2(sK0)),sK2(sK0))
| spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_159 ),
inference(forward_subsumption_resolution,[],[f3208,f1740]) ).
fof(f3358,plain,
( g_true_only(sK7(sK0),sK0)
| g_false_only(sK0,sK0)
| g_true_only(sK0,sK13(sK0)) ),
inference(resolution,[],[f2545,f223]) ).
fof(f3451,plain,
( g_true_only(sK2(sK0),sK13(sK2(sK0)))
| spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_157
| ~ spl19_159 ),
inference(resolution,[],[f3209,f1807]) ).
fof(f3462,plain,
( ~ g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK17(sK2(sK0)))
| ~ g_true_only(sK2(sK0),sK13(sK2(sK0)))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_158 ),
inference(resolution,[],[f1812,f114]) ).
fof(f3464,plain,
( ~ g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK17(sK2(sK0)))
| ~ g_true_only(sK13(sK2(sK0)),sK2(sK0))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_158 ),
inference(resolution,[],[f1812,f116]) ).
fof(f3474,plain,
( ~ g_false_only(sK2(sK0),sK17(sK2(sK0)))
| ~ g_true_only(sK13(sK2(sK0)),sK2(sK0))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_156
| ~ spl19_158 ),
inference(forward_subsumption_resolution,[],[f3464,f1803]) ).
fof(f3480,plain,
( ~ g_true_only(sK13(sK2(sK0)),sK2(sK0))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_154
| ~ spl19_156
| ~ spl19_158 ),
inference(forward_subsumption_resolution,[],[f3474,f1795]) ).
fof(f3486,plain,
( ~ g_true_only(sK13(sK2(sK0)),sK2(sK0))
| spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_158 ),
inference(forward_subsumption_resolution,[],[f3480,f1740]) ).
fof(f3553,plain,
( g_true_only(sK2(sK0),sK13(sK2(sK0)))
| spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_157
| ~ spl19_158 ),
inference(resolution,[],[f3486,f1807]) ).
fof(f3569,definition,
( spl19_320
<=> ! [X0] :
( ~ sP5(X0)
| ~ sP6(X0)
| ~ g_both(X0,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl19_320])],[avatar_definition]) ).
fof(f3570,plain,
( ! [X0] :
( ~ sP6(X0)
| ~ sP5(X0)
| ~ g_both(X0,sK0) )
| ~ spl19_320 ),
inference(avatar_component_clause,[],[f3569]) ).
fof(f3584,plain,
( spl19_269
| spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_157
| ~ spl19_158 ),
inference(avatar_split_clause,[],[f3553,f1810,f1806,f1801,f1793,f1738,f2968]) ).
fof(f3587,plain,
( ~ g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ g_true_only(sK2(sK0),sK13(sK2(sK0)))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_154
| ~ spl19_158 ),
inference(forward_subsumption_resolution,[],[f3462,f1795]) ).
fof(f3624,plain,
( ~ g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ g_true_only(sK2(sK0),sK13(sK2(sK0)))
| spl19_145
| ~ spl19_154
| ~ spl19_158 ),
inference(forward_subsumption_resolution,[],[f3587,f1740]) ).
fof(f3631,plain,
( ~ spl19_269
| ~ spl19_156
| spl19_145
| ~ spl19_154
| ~ spl19_158 ),
inference(avatar_split_clause,[],[f3624,f1810,f1793,f1738,f1801,f2968]) ).
fof(f3642,plain,
( ~ g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ g_true_only(sK2(sK0),sK13(sK2(sK0)))
| g_false_only(sK2(sK0),sK0)
| ~ spl19_154
| ~ spl19_159 ),
inference(forward_subsumption_resolution,[],[f3120,f1795]) ).
fof(f3661,plain,
( spl19_269
| spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_157
| ~ spl19_159 ),
inference(avatar_split_clause,[],[f3451,f1814,f1806,f1801,f1793,f1738,f2968]) ).
fof(f3670,plain,
( ~ g_false_only(sK17(sK2(sK0)),sK2(sK0))
| ~ g_true_only(sK2(sK0),sK13(sK2(sK0)))
| spl19_145
| ~ spl19_154
| ~ spl19_159 ),
inference(forward_subsumption_resolution,[],[f3642,f1740]) ).
fof(f3677,plain,
( ~ spl19_269
| ~ spl19_156
| spl19_145
| ~ spl19_154
| ~ spl19_159 ),
inference(avatar_split_clause,[],[f3670,f1814,f1793,f1738,f1801,f2968]) ).
fof(f3688,plain,
( spl19_27
| spl19_41
| ~ spl19_52 ),
inference(avatar_split_clause,[],[f907,f587,f452,f369]) ).
fof(f3732,plain,
( g_true_only(sK7(sK0),sK0)
| g_false_only(sK0,sK0) ),
inference(forward_subsumption_resolution,[],[f3358,f2546]) ).
fof(f3749,plain,
( spl19_27
| spl19_52 ),
inference(avatar_split_clause,[],[f3732,f587,f369]) ).
fof(f3787,plain,
( spl19_145
| ~ spl19_140 ),
inference(avatar_split_clause,[],[f1726,f1687,f1738]) ).
fof(f3808,definition,
( spl19_336
<=> g_both(sK0,sK0) ),
introduced(definition,[new_symbols(definition,[spl19_336])],[avatar_definition]) ).
fof(f3809,plain,
( g_both(sK0,sK0)
| ~ spl19_336 ),
inference(avatar_component_clause,[],[f3808]) ).
fof(f3822,plain,
( g_both(sK0,sK0)
| ~ g_true_only(sK0,sK0)
| ~ spl19_27 ),
inference(resolution,[],[f371,f141]) ).
fof(f3823,plain,
( g_both(sK0,sK0)
| ~ spl19_27 ),
inference(forward_subsumption_resolution,[],[f3822,f224]) ).
fof(f3827,plain,
( spl19_336
| ~ spl19_27 ),
inference(avatar_split_clause,[],[f3823,f369,f3808]) ).
fof(f3922,plain,
( sP11(sK2(sK0))
| g_false_only(sK2(sK0),sK15(sK2(sK0)))
| ~ spl19_140 ),
inference(resolution,[],[f1689,f760]) ).
fof(f4146,plain,
( ~ sP5(sK0)
| ~ g_both(sK0,sK0)
| ~ spl19_31
| ~ spl19_320 ),
inference(resolution,[],[f3570,f389]) ).
fof(f4152,plain,
( ~ g_both(sK0,sK0)
| ~ spl19_14
| ~ spl19_31
| ~ spl19_320 ),
inference(forward_subsumption_resolution,[],[f4146,f228]) ).
fof(f4155,plain,
( $false
| ~ spl19_14
| ~ spl19_31
| ~ spl19_320
| ~ spl19_336 ),
inference(forward_subsumption_resolution,[],[f4152,f3809]) ).
fof(f4156,plain,
( ~ spl19_14
| ~ spl19_31
| ~ spl19_320
| ~ spl19_336 ),
inference(avatar_contradiction_clause,[],[f4155]) ).
fof(f4179,plain,
( spl19_148
| spl19_149
| ~ spl19_140 ),
inference(avatar_split_clause,[],[f3922,f1687,f1756,f1752]) ).
fof(f4203,plain,
( ! [X0] :
( ~ g_false_only(X0,sK2(sK0))
| ~ g_false_only(sK2(sK0),X0)
| sP11(sK2(sK0)) )
| ~ spl19_157 ),
inference(forward_subsumption_resolution,[],[f3185,f122]) ).
fof(f4209,plain,
( spl19_149
| spl19_155
| ~ spl19_157 ),
inference(avatar_split_clause,[],[f4203,f1806,f1797,f1756]) ).
fof(f4225,plain,
( sP4(sK2(sK0),sK0)
| g_both(sK2(sK0),sK0)
| ~ spl19_1
| ~ spl19_14
| ~ spl19_27
| ~ spl19_31
| spl19_142 ),
inference(forward_subsumption_resolution,[],[f1684,f1696]) ).
fof(f4228,plain,
( sP4(sK2(sK0),sK0)
| g_both(sK2(sK0),sK0)
| ~ spl19_5
| ~ spl19_14
| ~ spl19_31
| ~ spl19_145
| ~ spl19_336 ),
inference(forward_subsumption_resolution,[],[f2078,f3809]) ).
fof(f4244,plain,
( spl19_140
| spl19_141
| ~ spl19_1
| ~ spl19_14
| ~ spl19_27
| ~ spl19_31
| spl19_142 ),
inference(avatar_split_clause,[],[f4225,f1695,f387,f369,f226,f143,f1691,f1687]) ).
fof(f4246,plain,
( spl19_140
| spl19_141
| ~ spl19_5
| ~ spl19_14
| ~ spl19_31
| ~ spl19_145
| ~ spl19_336 ),
inference(avatar_split_clause,[],[f4228,f3808,f1738,f387,f226,f159,f1691,f1687]) ).
fof(f4249,plain,
( ! [X0] :
( ~ sP5(X0)
| ~ g_both(X0,sK0)
| ~ sP6(X0)
| sP4(sK2(sK0),sK0)
| ~ g_false_only(sK2(sK0),sK0) )
| ~ spl19_6
| ~ spl19_149 ),
inference(resolution,[],[f1758,f165]) ).
fof(f4252,plain,
( ! [X0] :
( ~ sP5(X0)
| ~ g_both(X0,sK0)
| ~ sP6(X0)
| sP4(sK2(sK0),sK0) )
| ~ spl19_6
| ~ spl19_145
| ~ spl19_149 ),
inference(forward_subsumption_resolution,[],[f4249,f1739]) ).
fof(f4254,plain,
( spl19_141
| spl19_320
| ~ spl19_6
| ~ spl19_145
| ~ spl19_149 ),
inference(avatar_split_clause,[],[f4252,f1756,f1738,f164,f3569,f1691]) ).
fof(f4382,plain,
( g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK16(sK2(sK0)),sK2(sK0))
| ~ spl19_141 ),
inference(resolution,[],[f1693,f128]) ).
fof(f4383,plain,
( g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_true_only(sK16(sK2(sK0)),sK2(sK0))
| ~ spl19_141 ),
inference(resolution,[],[f1693,f129]) ).
fof(f4384,plain,
( g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK2(sK0),sK16(sK2(sK0)))
| ~ spl19_141 ),
inference(resolution,[],[f1693,f130]) ).
fof(f4385,plain,
( g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_true_only(sK2(sK0),sK16(sK2(sK0)))
| ~ spl19_141 ),
inference(resolution,[],[f1693,f131]) ).
fof(f4386,plain,
( g_both(sK18(sK2(sK0)),sK2(sK0))
| g_both(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK2(sK0),sK16(sK2(sK0)))
| ~ spl19_141 ),
inference(resolution,[],[f1693,f133]) ).
fof(f4387,plain,
( g_both(sK18(sK2(sK0)),sK2(sK0))
| g_both(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK16(sK2(sK0)),sK2(sK0))
| ~ spl19_141 ),
inference(resolution,[],[f1693,f134]) ).
fof(f4497,plain,
( g_true_only(sK2(sK0),sK14(sK2(sK0)))
| spl19_152
| ~ spl19_157 ),
inference(resolution,[],[f1772,f1807]) ).
fof(f4507,plain,
( spl19_153
| spl19_152
| ~ spl19_157 ),
inference(avatar_split_clause,[],[f4497,f1806,f1770,f1775]) ).
fof(f4533,plain,
( ~ g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK2(sK0),sK14(sK2(sK0)))
| g_true_only(sK2(sK0),sK0)
| ~ spl19_164 ),
inference(resolution,[],[f1899,f117]) ).
fof(f4535,plain,
( ~ g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK14(sK2(sK0)),sK2(sK0))
| g_true_only(sK2(sK0),sK0)
| ~ spl19_164 ),
inference(resolution,[],[f1899,f119]) ).
fof(f4583,plain,
( ~ g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK2(sK0),sK14(sK2(sK0)))
| g_true_only(sK2(sK0),sK0)
| ~ spl19_165 ),
inference(resolution,[],[f1903,f118]) ).
fof(f4585,plain,
( ~ g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK14(sK2(sK0)),sK2(sK0))
| g_true_only(sK2(sK0),sK0)
| ~ spl19_165 ),
inference(resolution,[],[f1903,f120]) ).
fof(f4599,plain,
( ~ spl19_166
| spl19_167
| ~ spl19_141 ),
inference(avatar_split_clause,[],[f4385,f1691,f1911,f1906]) ).
fof(f4600,plain,
( ~ spl19_166
| spl19_168
| ~ spl19_141 ),
inference(avatar_split_clause,[],[f4384,f1691,f1916,f1906]) ).
fof(f4603,plain,
( ~ spl19_163
| spl19_167
| ~ spl19_141 ),
inference(avatar_split_clause,[],[f4383,f1691,f1911,f1893]) ).
fof(f4604,plain,
( ~ spl19_163
| spl19_168
| ~ spl19_141 ),
inference(avatar_split_clause,[],[f4382,f1691,f1916,f1893]) ).
fof(f4605,plain,
( ~ g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK2(sK0),sK14(sK2(sK0)))
| spl19_151
| ~ spl19_165 ),
inference(forward_subsumption_resolution,[],[f4583,f1767]) ).
fof(f4606,plain,
( ~ g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK14(sK2(sK0)),sK2(sK0))
| spl19_151
| ~ spl19_165 ),
inference(forward_subsumption_resolution,[],[f4585,f1767]) ).
fof(f4607,plain,
( ~ spl19_153
| ~ spl19_168
| ~ spl19_167
| spl19_151
| ~ spl19_165 ),
inference(avatar_split_clause,[],[f4605,f1901,f1766,f1911,f1916,f1775]) ).
fof(f4608,plain,
( ~ spl19_152
| ~ spl19_168
| ~ spl19_167
| spl19_151
| ~ spl19_165 ),
inference(avatar_split_clause,[],[f4606,f1901,f1766,f1911,f1916,f1770]) ).
fof(f4612,plain,
( ~ g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK2(sK0),sK14(sK2(sK0)))
| spl19_151
| ~ spl19_164 ),
inference(forward_subsumption_resolution,[],[f4533,f1767]) ).
fof(f4614,plain,
( ~ g_false_only(sK18(sK2(sK0)),sK2(sK0))
| ~ g_false_only(sK2(sK0),sK18(sK2(sK0)))
| ~ g_true_only(sK14(sK2(sK0)),sK2(sK0))
| spl19_151
| ~ spl19_164 ),
inference(forward_subsumption_resolution,[],[f4535,f1767]) ).
fof(f4617,plain,
( ~ spl19_166
| spl19_164
| spl19_165
| ~ spl19_141 ),
inference(avatar_split_clause,[],[f4386,f1691,f1901,f1897,f1906]) ).
fof(f4619,plain,
( ~ spl19_163
| spl19_164
| spl19_165
| ~ spl19_141 ),
inference(avatar_split_clause,[],[f4387,f1691,f1901,f1897,f1893]) ).
fof(f4620,plain,
( ~ spl19_153
| ~ spl19_168
| ~ spl19_167
| spl19_151
| ~ spl19_164 ),
inference(avatar_split_clause,[],[f4612,f1897,f1766,f1911,f1916,f1775]) ).
fof(f4621,plain,
( ~ spl19_152
| ~ spl19_168
| ~ spl19_167
| spl19_151
| ~ spl19_164 ),
inference(avatar_split_clause,[],[f4614,f1897,f1766,f1911,f1916,f1770]) ).
cnf(s9,plain,
( spl19_1
| spl19_7 ),
inference(sat_conversion,[],[f171]) ).
cnf(s10,plain,
( spl19_1
| spl19_8 ),
inference(sat_conversion,[],[f175]) ).
cnf(s13,plain,
( spl19_5
| spl19_7 ),
inference(sat_conversion,[],[f178]) ).
cnf(s14,plain,
( spl19_5
| spl19_8 ),
inference(sat_conversion,[],[f179]) ).
cnf(s15,plain,
( spl19_6
| spl19_7 ),
inference(sat_conversion,[],[f180]) ).
cnf(s16,plain,
( spl19_6
| spl19_8 ),
inference(sat_conversion,[],[f181]) ).
cnf(s36,plain,
( ~ spl19_18
| spl19_24 ),
inference(sat_conversion,[],[f319]) ).
cnf(s37,plain,
( ~ spl19_7
| ~ spl19_8
| spl19_18 ),
inference(sat_conversion,[],[f320]) ).
cnf(s42,plain,
~ spl19_24,
inference(sat_conversion,[],[f363]) ).
cnf(s72,plain,
( spl19_28
| spl19_30 ),
inference(sat_conversion,[],[f661]) ).
cnf(s77,plain,
( ~ spl19_27
| ~ spl19_27
| spl19_31 ),
inference(sat_conversion,[],[f674]) ).
cnf(s78,plain,
( ~ spl19_27
| spl19_31 ),
inference(rat,[],[s77]) ).
cnf(s80,plain,
( spl19_27
| ~ spl19_28
| ~ spl19_41 ),
inference(sat_conversion,[],[f679]) ).
cnf(s81,plain,
( spl19_27
| ~ spl19_30
| ~ spl19_41 ),
inference(sat_conversion,[],[f680]) ).
cnf(s190,plain,
( ~ spl19_141
| ~ spl19_151 ),
inference(sat_conversion,[],[f1924]) ).
cnf(s192,plain,
( spl19_151
| spl19_157 ),
inference(sat_conversion,[],[f1996]) ).
cnf(s208,plain,
( ~ spl19_140
| spl19_149
| spl19_150 ),
inference(sat_conversion,[],[f2123]) ).
cnf(s211,plain,
( ~ spl19_140
| spl19_157 ),
inference(sat_conversion,[],[f2126]) ).
cnf(s217,plain,
( ~ spl19_142
| spl19_155
| spl19_158
| spl19_159 ),
inference(sat_conversion,[],[f2135]) ).
cnf(s221,plain,
( spl19_151
| spl19_163
| spl19_166 ),
inference(sat_conversion,[],[f2139]) ).
cnf(s225,plain,
spl19_14,
inference(sat_conversion,[],[f2148]) ).
cnf(s232,plain,
( ~ spl19_142
| spl19_154
| spl19_155 ),
inference(sat_conversion,[],[f2164]) ).
cnf(s233,plain,
( ~ spl19_142
| spl19_155
| spl19_156 ),
inference(sat_conversion,[],[f2165]) ).
cnf(s234,plain,
( ~ spl19_142
| spl19_155
| spl19_157 ),
inference(sat_conversion,[],[f2166]) ).
cnf(s344,plain,
( ~ spl19_148
| ~ spl19_150
| ~ spl19_155 ),
inference(sat_conversion,[],[f3055]) ).
cnf(s347,plain,
( spl19_145
| ~ spl19_155 ),
inference(sat_conversion,[],[f3062]) ).
cnf(s418,plain,
( spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_157
| ~ spl19_158
| spl19_269 ),
inference(sat_conversion,[],[f3584]) ).
cnf(s435,plain,
( spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_158
| ~ spl19_269 ),
inference(sat_conversion,[],[f3631]) ).
cnf(s450,plain,
( spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_157
| ~ spl19_159
| spl19_269 ),
inference(sat_conversion,[],[f3661]) ).
cnf(s467,plain,
( spl19_145
| ~ spl19_154
| ~ spl19_156
| ~ spl19_159
| ~ spl19_269 ),
inference(sat_conversion,[],[f3677]) ).
cnf(s474,plain,
( spl19_27
| spl19_41
| ~ spl19_52 ),
inference(sat_conversion,[],[f3688]) ).
cnf(s495,plain,
( spl19_27
| spl19_52 ),
inference(sat_conversion,[],[f3749]) ).
cnf(s501,plain,
( ~ spl19_140
| spl19_145 ),
inference(sat_conversion,[],[f3787]) ).
cnf(s516,plain,
( ~ spl19_27
| spl19_336 ),
inference(sat_conversion,[],[f3827]) ).
cnf(s534,plain,
( ~ spl19_14
| ~ spl19_31
| ~ spl19_320
| ~ spl19_336 ),
inference(sat_conversion,[],[f4156]) ).
cnf(s544,plain,
( ~ spl19_140
| spl19_148
| spl19_149 ),
inference(sat_conversion,[],[f4179]) ).
cnf(s572,plain,
( spl19_149
| spl19_155
| ~ spl19_157 ),
inference(sat_conversion,[],[f4209]) ).
cnf(s593,plain,
( ~ spl19_1
| ~ spl19_14
| ~ spl19_27
| ~ spl19_31
| spl19_140
| spl19_141
| spl19_142 ),
inference(sat_conversion,[],[f4244]) ).
cnf(s595,plain,
( ~ spl19_5
| ~ spl19_14
| ~ spl19_31
| spl19_140
| spl19_141
| ~ spl19_145
| ~ spl19_336 ),
inference(sat_conversion,[],[f4246]) ).
cnf(s599,plain,
( ~ spl19_6
| spl19_141
| ~ spl19_145
| ~ spl19_149
| spl19_320 ),
inference(sat_conversion,[],[f4254]) ).
cnf(s632,plain,
( spl19_152
| spl19_153
| ~ spl19_157 ),
inference(sat_conversion,[],[f4507]) ).
cnf(s659,plain,
( ~ spl19_141
| ~ spl19_166
| spl19_167 ),
inference(sat_conversion,[],[f4599]) ).
cnf(s660,plain,
( ~ spl19_141
| ~ spl19_166
| spl19_168 ),
inference(sat_conversion,[],[f4600]) ).
cnf(s663,plain,
( ~ spl19_141
| ~ spl19_163
| spl19_167 ),
inference(sat_conversion,[],[f4603]) ).
cnf(s664,plain,
( ~ spl19_141
| ~ spl19_163
| spl19_168 ),
inference(sat_conversion,[],[f4604]) ).
cnf(s665,plain,
( spl19_151
| ~ spl19_153
| ~ spl19_165
| ~ spl19_167
| ~ spl19_168 ),
inference(sat_conversion,[],[f4607]) ).
cnf(s666,plain,
( spl19_151
| ~ spl19_152
| ~ spl19_165
| ~ spl19_167
| ~ spl19_168 ),
inference(sat_conversion,[],[f4608]) ).
cnf(s674,plain,
( ~ spl19_141
| spl19_164
| spl19_165
| ~ spl19_166 ),
inference(sat_conversion,[],[f4617]) ).
cnf(s676,plain,
( ~ spl19_141
| ~ spl19_163
| spl19_164
| spl19_165 ),
inference(sat_conversion,[],[f4619]) ).
cnf(s677,plain,
( spl19_151
| ~ spl19_153
| ~ spl19_164
| ~ spl19_167
| ~ spl19_168 ),
inference(sat_conversion,[],[f4620]) ).
cnf(s678,plain,
( spl19_151
| ~ spl19_152
| ~ spl19_164
| ~ spl19_167
| ~ spl19_168 ),
inference(sat_conversion,[],[f4621]) ).
cnf(s681,plain,
~ spl19_18,
inference(rat,[],[s36,s42]) ).
cnf(s686,plain,
spl19_1,
inference(rat,[],[s37,s9,s10,s681]) ).
cnf(s687,plain,
( spl19_27
| ~ spl19_41 ),
inference(rat,[],[s72,s80,s81]) ).
cnf(s688,plain,
( spl19_27
| ~ spl19_52 ),
inference(rat,[],[s687,s474]) ).
cnf(s689,plain,
spl19_27,
inference(rat,[],[s688,s495]) ).
cnf(s690,plain,
spl19_336,
inference(rat,[],[s516,s689]) ).
cnf(s692,plain,
spl19_31,
inference(rat,[],[s78,s689]) ).
cnf(s694,plain,
~ spl19_320,
inference(rat,[],[s534,s690,s225,s692]) ).
cnf(s696,plain,
( ~ spl19_159
| ~ spl19_154
| ~ spl19_156
| ~ spl19_157
| spl19_145 ),
inference(rat,[],[s450,s467]) ).
cnf(s697,plain,
( spl19_141
| spl19_140
| ~ spl19_5 ),
inference(rat,[],[s418,s435,s217,s696,s232,s233,s234,s347,s595,s593,s225,s692,s690,s686,s689]) ).
cnf(s698,plain,
( ~ spl19_166
| ~ spl19_153
| ~ spl19_141 ),
inference(rat,[],[s674,s665,s677,s659,s660,s190]) ).
cnf(s699,plain,
( ~ spl19_153
| ~ spl19_141 ),
inference(rat,[],[s676,s665,s677,s663,s664,s221,s698,s190]) ).
cnf(s700,plain,
( ~ spl19_166
| ~ spl19_141 ),
inference(rat,[],[s674,s666,s678,s659,s660,s632,s699,s192,s190]) ).
cnf(s701,plain,
~ spl19_141,
inference(rat,[],[s676,s666,s678,s663,s664,s221,s700,s632,s699,s192,s190]) ).
cnf(s703,plain,
spl19_6,
inference(rat,[],[s37,s15,s16,s681]) ).
cnf(s704,plain,
~ spl19_140,
inference(rat,[],[s344,s544,s208,s572,s599,s211,s501,s703,s701,s694]) ).
cnf(s705,plain,
~ spl19_5,
inference(rat,[],[s697,s701,s704]) ).
cnf(s709,plain,
spl19_8,
inference(rat,[],[s14,s705]) ).
cnf(s710,plain,
spl19_7,
inference(rat,[],[s13,s705]) ).
cnf(s712,plain,
$false,
inference(rat,[],[s37,s681,s709,s710]) ).
fof(f4622,plain,
$false,
inference(avatar_sat_refutation,[],[s712]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO604+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n005.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 17:54:17 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.23 Running first-order model finding
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.35 % (998868)Will run a generic schedule for satisfiability detection.
% 0.19/0.35 % (998878)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2151683208:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.35 % (998874)% WARNING: option uhcvi not known.
% 0.19/0.35 % (998873)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=181393306_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.35 % (998876)dis+10_1_sil=32000:sp=arity:random_seed=944438299:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.35 % (998879)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=992190236:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.35 % (998877)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1933407450:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.35 % (998874)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2248620751:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.35 % (998875)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1898419214:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.35 % TRYING [1]
% 0.19/0.35 % TRYING [2]
% 0.19/0.35 % TRYING [3]
% 0.19/0.35 % TRYING [4]
% 0.19/0.35 % (998878)Instruction limit reached!
% 0.19/0.35 % (998878)------------------------------
% 0.19/0.35 % (998878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (998878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (998878)CaDiCaL version: 2.1.3
% 0.19/0.35 % (998878)Termination reason: Instruction limit
% 0.19/0.35 % (998878)Termination phase: Saturation
% 0.19/0.35 % (998878)Time elapsed: 0.040 s
% 0.19/0.35 % (998878)Peak memory usage: 12 MB
% 0.19/0.35 % (998878)Instructions burned: 131 (million)
% 0.19/0.35 % (998887)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2402666639:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.19/0.35 % TRYING [1]
% 0.19/0.35 % TRYING [2]
% 0.19/0.35 % TRYING [3]
% 0.19/0.35 % TRYING [4]
% 0.19/0.35 % TRYING [5]
% 0.19/0.35 % (998877)Instruction limit reached!
% 0.19/0.35 % (998877)------------------------------
% 0.19/0.35 % (998877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (998877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (998877)CaDiCaL version: 2.1.3
% 0.19/0.35 % (998877)Termination reason: Instruction limit
% 0.19/0.35 % (998877)Termination phase: Saturation
% 0.19/0.35 % (998877)Time elapsed: 0.064 s
% 0.19/0.35 % (998877)Peak memory usage: 12 MB
% 0.19/0.35 % (998877)Instructions burned: 120 (million)
% 0.19/0.35 % (998876)Instruction limit reached!
% 0.19/0.35 % (998876)------------------------------
% 0.19/0.35 % (998876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.35 % (998876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.35 % (998876)CaDiCaL version: 2.1.3
% 0.19/0.35 % (998876)Termination reason: Instruction limit
% 0.19/0.35 % (998876)Termination phase: Saturation
% 0.19/0.35 % (998876)Time elapsed: 0.065 s
% 0.19/0.35 % (998876)Peak memory usage: 12 MB
% 0.19/0.35 % (998876)Instructions burned: 107 (million)
% 0.19/0.35 % (998874) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-998868-998874"...
% 0.19/0.35 % TRYING [5]
% 0.19/0.35 % (998874)...printing done.
% 0.19/0.35 % (998889)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4058592050:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.35 % (998890)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2550978085:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.19/0.35 % (998874)Refutation found. Thanks to Tanya!
% 0.19/0.35 % SZS status Theorem for theBenchmark
% 0.19/0.35 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.36 % (998874)------------------------------
% 0.19/0.36 % (998874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.36 % (998874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.36 % (998874)CaDiCaL version: 2.1.3
% 0.19/0.36 % (998874)Termination reason: Refutation
% 0.19/0.36 % (998874)Time elapsed: 0.082 s
% 0.19/0.36 % (998874)Peak memory usage: 14 MB
% 0.19/0.36 % (998874)Instructions burned: 129 (million)
% 0.19/0.36 % (998868)Success in time 0.115 s
% 0.19/0.36 % Vampire exiting
%------------------------------------------------------------------------------