%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYO606+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n014.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 : Fri Sep 25 03:51:32 PM UTC 2026
% Result : Theorem 4.39s 6.30s
% Output : CNFRefutation 4.39s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f89ERROR: Could not build tree for root c_11464ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ~ ? [X0,X1] :
! [X2] :
( ( h_false_only(X0,X2)
& g_both(X0,X1) )
| ( ( h_false_only(X0,X2)
| h_both(X0,X2) )
& g_true_only(X0,X1) ) )
& ? [X0] :
( ~ ? [X1] :
! [X2] :
( ( h_false_only(X0,X2)
& g_both(X0,X1) )
| ( ( h_false_only(X0,X2)
| h_both(X0,X2) )
& g_true_only(X0,X1) ) )
& ? [X1] :
( ~ ? [X2] :
( h_true_only(X0,X2)
| g_false_only(X0,X1) )
& ? [X2] :
( h_both(X0,X2)
& g_both(X0,X1) ) ) )
& ~ ? [X0] :
( ( ! [X1] : h_false_only(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ? [X1] : g_both(X0,X1) )
| ( ( ! [X1] : h_false_only(X0,X1)
| ( ~ ? [X1] : h_true_only(X0,X1)
& ? [X1] : h_both(X0,X1) ) )
& ? [X1] : g_true_only(X0,X1) ) )
& ? [X0] :
( ~ ? [X1] : h_true_only(X0,X1)
& ? [X1] : h_both(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ? [X1] : g_both(X0,X1) ) )
| ( ? [X0,X1] :
! [X2] :
( ( h_false_only(X0,X2)
& g_both(X0,X1) )
| ( ( h_false_only(X0,X2)
| h_both(X0,X2) )
& g_true_only(X0,X1) ) )
& ? [X0] :
( ( ! [X1] : h_false_only(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ? [X1] : g_both(X0,X1) )
| ( ( ! [X1] : h_false_only(X0,X1)
| ( ~ ? [X1] : h_true_only(X0,X1)
& ? [X1] : h_both(X0,X1) ) )
& ? [X1] : g_true_only(X0,X1) ) ) )
| ( ! [X0,X1] :
? [X2] :
( h_true_only(X0,X2)
| g_false_only(X0,X1) )
& ! [X0] :
( ? [X1] : h_true_only(X0,X1)
| ! [X1] : g_false_only(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nc5) ).
fof(f2,negated_conjecture,
~ ( ( ~ ? [X0,X1] :
! [X2] :
( ( h_false_only(X0,X2)
& g_both(X0,X1) )
| ( ( h_false_only(X0,X2)
| h_both(X0,X2) )
& g_true_only(X0,X1) ) )
& ? [X0] :
( ~ ? [X1] :
! [X2] :
( ( h_false_only(X0,X2)
& g_both(X0,X1) )
| ( ( h_false_only(X0,X2)
| h_both(X0,X2) )
& g_true_only(X0,X1) ) )
& ? [X1] :
( ~ ? [X2] :
( h_true_only(X0,X2)
| g_false_only(X0,X1) )
& ? [X2] :
( h_both(X0,X2)
& g_both(X0,X1) ) ) )
& ~ ? [X0] :
( ( ! [X1] : h_false_only(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ? [X1] : g_both(X0,X1) )
| ( ( ! [X1] : h_false_only(X0,X1)
| ( ~ ? [X1] : h_true_only(X0,X1)
& ? [X1] : h_both(X0,X1) ) )
& ? [X1] : g_true_only(X0,X1) ) )
& ? [X0] :
( ~ ? [X1] : h_true_only(X0,X1)
& ? [X1] : h_both(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ? [X1] : g_both(X0,X1) ) )
| ( ? [X0,X1] :
! [X2] :
( ( h_false_only(X0,X2)
& g_both(X0,X1) )
| ( ( h_false_only(X0,X2)
| h_both(X0,X2) )
& g_true_only(X0,X1) ) )
& ? [X0] :
( ( ! [X1] : h_false_only(X0,X1)
& ~ ? [X1] : g_true_only(X0,X1)
& ? [X1] : g_both(X0,X1) )
| ( ( ! [X1] : h_false_only(X0,X1)
| ( ~ ? [X1] : h_true_only(X0,X1)
& ? [X1] : h_both(X0,X1) ) )
& ? [X1] : g_true_only(X0,X1) ) ) )
| ( ! [X0,X1] :
? [X2] :
( h_true_only(X0,X2)
| g_false_only(X0,X1) )
& ! [X0] :
( ? [X1] : h_true_only(X0,X1)
| ! [X1] : g_false_only(X0,X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [X0,X1] :
( g_true_only(X0,X1)
<=> ( ~ g_false(X0,X1)
& g_true(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',true_only_g) ).
fof(f4,axiom,
! [X0,X1] :
( g_both(X0,X1)
<=> ( g_false(X0,X1)
& g_true(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',both_g) ).
fof(f5,axiom,
! [X0,X1] :
( g_false_only(X0,X1)
<=> ( ~ g_true(X0,X1)
& g_false(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',false_only_g) ).
fof(f6,axiom,
! [X0,X1] :
( g_false_only(X0,X1)
| g_both(X0,X1)
| g_true_only(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exhaustion_g) ).
fof(f7,axiom,
! [X0,X1] :
( h_true_only(X0,X1)
<=> ( ~ h_false(X0,X1)
& h_true(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',true_only_h) ).
fof(f8,axiom,
! [X0,X1] :
( h_both(X0,X1)
<=> ( h_false(X0,X1)
& h_true(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',both_h) ).
fof(f9,axiom,
! [X0,X1] :
( h_false_only(X0,X1)
<=> ( ~ h_true(X0,X1)
& h_false(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',false_only_h) ).
fof(f10,axiom,
! [X0,X1] :
( h_false_only(X0,X1)
| h_both(X0,X1)
| h_true_only(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exhaustion_h) ).
fof(f11,plain,
~ ( ( ~ ? [X36,X37] :
! [X38] :
( ( h_false_only(X36,X38)
& g_both(X36,X37) )
| ( ( h_false_only(X36,X38)
| h_both(X36,X38) )
& g_true_only(X36,X37) ) )
& ? [X30] :
( ~ ? [X34] :
! [X35] :
( ( h_false_only(X30,X35)
& g_both(X30,X34) )
| ( ( h_false_only(X30,X35)
| h_both(X30,X35) )
& g_true_only(X30,X34) ) )
& ? [X31] :
( ~ ? [X33] :
( h_true_only(X30,X33)
| g_false_only(X30,X31) )
& ? [X32] :
( h_both(X30,X32)
& g_both(X30,X31) ) ) )
& ~ ? [X22] :
( ( ! [X29] : h_false_only(X22,X29)
& ~ ? [X28] : g_true_only(X22,X28)
& ? [X27] : g_both(X22,X27) )
| ( ( ! [X26] : h_false_only(X22,X26)
| ( ~ ? [X25] : h_true_only(X22,X25)
& ? [X24] : h_both(X22,X24) ) )
& ? [X23] : g_true_only(X22,X23) ) )
& ? [X17] :
( ~ ? [X21] : h_true_only(X17,X21)
& ? [X20] : h_both(X17,X20)
& ~ ? [X19] : g_true_only(X17,X19)
& ? [X18] : g_both(X17,X18) ) )
| ( ? [X14,X15] :
! [X16] :
( ( h_false_only(X14,X16)
& g_both(X14,X15) )
| ( ( h_false_only(X14,X16)
| h_both(X14,X16) )
& g_true_only(X14,X15) ) )
& ? [X6] :
( ( ! [X13] : h_false_only(X6,X13)
& ~ ? [X12] : g_true_only(X6,X12)
& ? [X11] : g_both(X6,X11) )
| ( ( ! [X10] : h_false_only(X6,X10)
| ( ~ ? [X9] : h_true_only(X6,X9)
& ? [X8] : h_both(X6,X8) ) )
& ? [X7] : g_true_only(X6,X7) ) ) )
| ( ! [X3,X4] :
? [X5] :
( h_true_only(X3,X5)
| g_false_only(X3,X4) )
& ! [X0] :
( ? [X2] : h_true_only(X0,X2)
| ! [X1] : g_false_only(X0,X1) ) ) ),
inference(rectify,[],[f2]) ).
fof(f12,plain,
( ( ? [X36,X37] :
! [X38] :
( ( h_false_only(X36,X38)
& g_both(X36,X37) )
| ( ( h_false_only(X36,X38)
| h_both(X36,X38) )
& g_true_only(X36,X37) ) )
| ! [X30] :
( ? [X34] :
! [X35] :
( ( h_false_only(X30,X35)
& g_both(X30,X34) )
| ( ( h_false_only(X30,X35)
| h_both(X30,X35) )
& g_true_only(X30,X34) ) )
| ! [X31] :
( ? [X33] :
( h_true_only(X30,X33)
| g_false_only(X30,X31) )
| ! [X32] :
( ~ h_both(X30,X32)
| ~ g_both(X30,X31) ) ) )
| ? [X22] :
( ( ! [X29] : h_false_only(X22,X29)
& ! [X28] : ~ g_true_only(X22,X28)
& ? [X27] : g_both(X22,X27) )
| ( ( ! [X26] : h_false_only(X22,X26)
| ( ! [X25] : ~ h_true_only(X22,X25)
& ? [X24] : h_both(X22,X24) ) )
& ? [X23] : g_true_only(X22,X23) ) )
| ! [X17] :
( ? [X21] : h_true_only(X17,X21)
| ! [X20] : ~ h_both(X17,X20)
| ? [X19] : g_true_only(X17,X19)
| ! [X18] : ~ g_both(X17,X18) ) )
& ( ! [X14,X15] :
? [X16] :
( ( ~ h_false_only(X14,X16)
| ~ g_both(X14,X15) )
& ( ( ~ h_false_only(X14,X16)
& ~ h_both(X14,X16) )
| ~ g_true_only(X14,X15) ) )
| ! [X6] :
( ( ? [X13] : ~ h_false_only(X6,X13)
| ? [X12] : g_true_only(X6,X12)
| ! [X11] : ~ g_both(X6,X11) )
& ( ( ? [X10] : ~ h_false_only(X6,X10)
& ( ? [X9] : h_true_only(X6,X9)
| ! [X8] : ~ h_both(X6,X8) ) )
| ! [X7] : ~ g_true_only(X6,X7) ) ) )
& ( ? [X3,X4] :
! [X5] :
( ~ h_true_only(X3,X5)
& ~ g_false_only(X3,X4) )
| ? [X0] :
( ! [X2] : ~ h_true_only(X0,X2)
& ? [X1] : ~ g_false_only(X0,X1) ) ) ),
inference(ennf_transformation,[],[f11]) ).
fof(f18,plain,
( ~ sP3
| ! [X14,X15] :
? [X16] :
( ( ~ h_false_only(X14,X16)
| ~ g_both(X14,X15) )
& ( ( ~ h_false_only(X14,X16)
& ~ h_both(X14,X16) )
| ~ g_true_only(X14,X15) ) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f19,plain,
( ~ sP3
| ! [X0,X1] :
? [X2] :
( ( ~ h_false_only(X0,X2)
| ~ g_both(X0,X1) )
& ( ( ~ h_false_only(X0,X2)
& ~ h_both(X0,X2) )
| ~ g_true_only(X0,X1) ) ) ),
inference(rectify,[],[f18]) ).
fof(f20,plain,
( ~ sP3
| ! [X0,X1] :
( ( ~ h_false_only(X0,sK4(X0,X1))
| ~ g_both(X0,X1) )
& ( ( ~ h_false_only(X0,sK4(X0,X1))
& ~ h_both(X0,sK4(X0,X1)) )
| ~ g_true_only(X0,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X2,sK4(X0,X1))],[f19]) ).
fof(f21,plain,
( ~ sP2
| ! [X30] :
( ? [X34] :
! [X35] :
( ( h_false_only(X30,X35)
& g_both(X30,X34) )
| ( ( h_false_only(X30,X35)
| h_both(X30,X35) )
& g_true_only(X30,X34) ) )
| ! [X31] :
( ? [X33] :
( h_true_only(X30,X33)
| g_false_only(X30,X31) )
| ! [X32] :
( ~ h_both(X30,X32)
| ~ g_both(X30,X31) ) ) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f22,plain,
( ~ sP2
| ! [X0] :
( ? [X4] :
! [X5] :
( ( h_false_only(X0,X5)
& g_both(X0,X4) )
| ( ( h_false_only(X0,X5)
| h_both(X0,X5) )
& g_true_only(X0,X4) ) )
| ! [X1] :
( ? [X3] :
( h_true_only(X0,X3)
| g_false_only(X0,X1) )
| ! [X2] :
( ~ h_both(X0,X2)
| ~ g_both(X0,X1) ) ) ) ),
inference(rectify,[],[f21]) ).
fof(f23,plain,
( ~ sP2
| ! [X0] :
( ! [X5] :
( ( h_false_only(X0,X5)
& g_both(X0,sK6(X0)) )
| ( ( h_false_only(X0,X5)
| h_both(X0,X5) )
& g_true_only(X0,sK6(X0)) ) )
| ! [X1] :
( h_true_only(X0,sK5(X0,X1))
| g_false_only(X0,X1)
| ! [X2] :
( ~ h_both(X0,X2)
| ~ g_both(X0,X1) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6]),skolemize(X3,sK5(X0,X1)),skolemize(X4,sK6(X0))],[f22]) ).
fof(f24,plain,
( ~ sP1
| ? [X36,X37] :
! [X38] :
( ( h_false_only(X36,X38)
& g_both(X36,X37) )
| ( ( h_false_only(X36,X38)
| h_both(X36,X38) )
& g_true_only(X36,X37) ) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f25,plain,
( ~ sP1
| ? [X0,X1] :
! [X2] :
( ( h_false_only(X0,X2)
& g_both(X0,X1) )
| ( ( h_false_only(X0,X2)
| h_both(X0,X2) )
& g_true_only(X0,X1) ) ) ),
inference(rectify,[],[f24]) ).
fof(f26,plain,
( ~ sP1
| ! [X2] :
( ( h_false_only(sK7,X2)
& g_both(sK7,sK8) )
| ( ( h_false_only(sK7,X2)
| h_both(sK7,X2) )
& g_true_only(sK7,sK8) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7),skolemize(X1,sK8)],[f25]) ).
fof(f30,plain,
( ( sP1
| sP2
| ? [X19] :
( sP0(X19)
| ( ( ! [X23] : h_false_only(X19,X23)
| ( ! [X22] : ~ h_true_only(X19,X22)
& ? [X21] : h_both(X19,X21) ) )
& ? [X20] : g_true_only(X19,X20) ) )
| ! [X14] :
( ? [X18] : h_true_only(X14,X18)
| ! [X17] : ~ h_both(X14,X17)
| ? [X16] : g_true_only(X14,X16)
| ! [X15] : ~ g_both(X14,X15) ) )
& ( sP3
| ! [X6] :
( ( ? [X13] : ~ h_false_only(X6,X13)
| ? [X12] : g_true_only(X6,X12)
| ! [X11] : ~ g_both(X6,X11) )
& ( ( ? [X10] : ~ h_false_only(X6,X10)
& ( ? [X9] : h_true_only(X6,X9)
| ! [X8] : ~ h_both(X6,X8) ) )
| ! [X7] : ~ g_true_only(X6,X7) ) ) )
& ( ? [X3,X4] :
! [X5] :
( ~ h_true_only(X3,X5)
& ~ g_false_only(X3,X4) )
| ? [X0] :
( ! [X2] : ~ h_true_only(X0,X2)
& ? [X1] : ~ g_false_only(X0,X1) ) ) ),
inference(rectify,[],[f17]) ).
fof(f31,plain,
( ( sP1
| sP2
| sP0(sK20)
| ( ( ! [X23] : h_false_only(sK20,X23)
| ( ! [X22] : ~ h_true_only(sK20,X22)
& h_both(sK20,sK22) ) )
& g_true_only(sK20,sK21) )
| ! [X14] :
( h_true_only(X14,sK19(X14))
| ! [X17] : ~ h_both(X14,X17)
| g_true_only(X14,sK18(X14))
| ! [X15] : ~ g_both(X14,X15) ) )
& ( sP3
| ! [X6] :
( ( ~ h_false_only(X6,sK17(X6))
| g_true_only(X6,sK16(X6))
| ! [X11] : ~ g_both(X6,X11) )
& ( ( ~ h_false_only(X6,sK15(X6))
& ( h_true_only(X6,sK14(X6))
| ! [X8] : ~ h_both(X6,X8) ) )
| ! [X7] : ~ g_true_only(X6,X7) ) ) )
& ( ! [X5] :
( ~ h_true_only(sK12,X5)
& ~ g_false_only(sK12,sK13) )
| ( ! [X2] : ~ h_true_only(sK10,X2)
& ~ g_false_only(sK10,sK11) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X3,sK12),skolemize(X4,sK13),skolemize(X9,sK14(X6)),skolemize(X10,sK15(X6)),skolemize(X12,sK16(X6)),skolemize(X13,sK17(X6)),skolemize(X16,sK18(X14)),skolemize(X18,sK19(X14)),skolemize(X19,sK20),skolemize(X20,sK21),skolemize(X21,sK22)],[f30]) ).
fof(f32,plain,
! [X0,X1] :
( ( ~ g_true_only(X0,X1)
| ( ~ g_false(X0,X1)
& g_true(X0,X1) ) )
& ( g_false(X0,X1)
| ~ g_true(X0,X1)
| g_true_only(X0,X1) ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f33,plain,
! [X0,X1] :
( ( ~ g_true_only(X0,X1)
| ( ~ g_false(X0,X1)
& g_true(X0,X1) ) )
& ( g_false(X0,X1)
| ~ g_true(X0,X1)
| g_true_only(X0,X1) ) ),
inference(flattening,[],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( ( ~ g_both(X0,X1)
| ( g_false(X0,X1)
& g_true(X0,X1) ) )
& ( ~ g_false(X0,X1)
| ~ g_true(X0,X1)
| g_both(X0,X1) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f35,plain,
! [X0,X1] :
( ( ~ g_both(X0,X1)
| ( g_false(X0,X1)
& g_true(X0,X1) ) )
& ( ~ g_false(X0,X1)
| ~ g_true(X0,X1)
| g_both(X0,X1) ) ),
inference(flattening,[],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( ( ~ g_false_only(X0,X1)
| ( ~ g_true(X0,X1)
& g_false(X0,X1) ) )
& ( g_true(X0,X1)
| ~ g_false(X0,X1)
| g_false_only(X0,X1) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f37,plain,
! [X0,X1] :
( ( ~ g_false_only(X0,X1)
| ( ~ g_true(X0,X1)
& g_false(X0,X1) ) )
& ( g_true(X0,X1)
| ~ g_false(X0,X1)
| g_false_only(X0,X1) ) ),
inference(flattening,[],[f36]) ).
fof(f38,plain,
! [X0,X1] :
( ( ~ h_true_only(X0,X1)
| ( ~ h_false(X0,X1)
& h_true(X0,X1) ) )
& ( h_false(X0,X1)
| ~ h_true(X0,X1)
| h_true_only(X0,X1) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f39,plain,
! [X0,X1] :
( ( ~ h_true_only(X0,X1)
| ( ~ h_false(X0,X1)
& h_true(X0,X1) ) )
& ( h_false(X0,X1)
| ~ h_true(X0,X1)
| h_true_only(X0,X1) ) ),
inference(flattening,[],[f38]) ).
fof(f40,plain,
! [X0,X1] :
( ( ~ h_both(X0,X1)
| ( h_false(X0,X1)
& h_true(X0,X1) ) )
& ( ~ h_false(X0,X1)
| ~ h_true(X0,X1)
| h_both(X0,X1) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f41,plain,
! [X0,X1] :
( ( ~ h_both(X0,X1)
| ( h_false(X0,X1)
& h_true(X0,X1) ) )
& ( ~ h_false(X0,X1)
| ~ h_true(X0,X1)
| h_both(X0,X1) ) ),
inference(flattening,[],[f40]) ).
fof(f42,plain,
! [X0,X1] :
( ( ~ h_false_only(X0,X1)
| ( ~ h_true(X0,X1)
& h_false(X0,X1) ) )
& ( h_true(X0,X1)
| ~ h_false(X0,X1)
| h_false_only(X0,X1) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f43,plain,
! [X0,X1] :
( ( ~ h_false_only(X0,X1)
| ( ~ h_true(X0,X1)
& h_false(X0,X1) ) )
& ( h_true(X0,X1)
| ~ h_false(X0,X1)
| h_false_only(X0,X1) ) ),
inference(flattening,[],[f42]) ).
fof(f44,plain,
! [X0,X1] :
( ~ sP3
| ~ h_false_only(X0,sK4(X0,X1))
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f45,plain,
! [X0,X1] :
( ~ sP3
| ~ h_false_only(X0,sK4(X0,X1))
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f46,plain,
! [X0,X1] :
( ~ sP3
| ~ h_both(X0,sK4(X0,X1))
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f49,plain,
! [X2,X0,X1,X5] :
( ~ sP2
| h_false_only(X0,X5)
| g_true_only(X0,sK6(X0))
| h_true_only(X0,sK5(X0,X1))
| g_false_only(X0,X1)
| ~ h_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f52,plain,
! [X2] :
( ~ sP1
| g_both(sK7,sK8)
| h_false_only(sK7,X2)
| h_both(sK7,X2) ),
inference(cnf_transformation,[],[f26]) ).
fof(f53,plain,
! [X2] :
( ~ sP1
| h_false_only(sK7,X2)
| g_true_only(sK7,sK8) ),
inference(cnf_transformation,[],[f26]) ).
fof(f54,plain,
( ~ sP1
| g_both(sK7,sK8)
| g_true_only(sK7,sK8) ),
inference(cnf_transformation,[],[f26]) ).
fof(f58,plain,
! [X14,X17,X15,X22,X23] :
( sP1
| sP2
| sP0(sK20)
| h_false_only(sK20,X23)
| ~ h_true_only(sK20,X22)
| h_true_only(X14,sK19(X14))
| ~ h_both(X14,X17)
| g_true_only(X14,sK18(X14))
| ~ g_both(X14,X15) ),
inference(cnf_transformation,[],[f31]) ).
fof(f59,plain,
! [X14,X17,X15,X23] :
( sP1
| sP2
| sP0(sK20)
| h_false_only(sK20,X23)
| h_both(sK20,sK22)
| h_true_only(X14,sK19(X14))
| ~ h_both(X14,X17)
| g_true_only(X14,sK18(X14))
| ~ g_both(X14,X15) ),
inference(cnf_transformation,[],[f31]) ).
fof(f60,plain,
! [X14,X17,X15] :
( sP1
| sP2
| sP0(sK20)
| g_true_only(sK20,sK21)
| h_true_only(X14,sK19(X14))
| ~ h_both(X14,X17)
| g_true_only(X14,sK18(X14))
| ~ g_both(X14,X15) ),
inference(cnf_transformation,[],[f31]) ).
fof(f61,plain,
! [X11,X6] :
( sP3
| ~ h_false_only(X6,sK17(X6))
| g_true_only(X6,sK16(X6))
| ~ g_both(X6,X11) ),
inference(cnf_transformation,[],[f31]) ).
fof(f62,plain,
! [X6,X7] :
( sP3
| ~ h_false_only(X6,sK15(X6))
| ~ g_true_only(X6,X7) ),
inference(cnf_transformation,[],[f31]) ).
fof(f63,plain,
! [X8,X6,X7] :
( sP3
| h_true_only(X6,sK14(X6))
| ~ h_both(X6,X8)
| ~ g_true_only(X6,X7) ),
inference(cnf_transformation,[],[f31]) ).
fof(f64,plain,
! [X2,X5] :
( ~ h_true_only(sK12,X5)
| ~ h_true_only(sK10,X2) ),
inference(cnf_transformation,[],[f31]) ).
fof(f65,plain,
! [X2] :
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,X2) ),
inference(cnf_transformation,[],[f31]) ).
fof(f66,plain,
! [X5] :
( ~ h_true_only(sK12,X5)
| ~ g_false_only(sK10,sK11) ),
inference(cnf_transformation,[],[f31]) ).
fof(f67,plain,
( ~ g_false_only(sK12,sK13)
| ~ g_false_only(sK10,sK11) ),
inference(cnf_transformation,[],[f31]) ).
fof(f68,plain,
! [X0,X1] :
( ~ g_true_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f69,plain,
! [X0,X1] :
( ~ g_true_only(X0,X1)
| g_true(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f70,plain,
! [X0,X1] :
( g_false(X0,X1)
| ~ g_true(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f72,plain,
! [X0,X1] :
( ~ g_both(X0,X1)
| g_true(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
fof(f74,plain,
! [X0,X1] :
( ~ g_false_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f75,plain,
! [X0,X1] :
( ~ g_false_only(X0,X1)
| g_false(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f76,plain,
! [X0,X1] :
( g_true(X0,X1)
| ~ g_false(X0,X1)
| g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f37]) ).
fof(f77,plain,
! [X0,X1] :
( g_false_only(X0,X1)
| g_both(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f78,plain,
! [X0,X1] :
( ~ h_true_only(X0,X1)
| ~ h_false(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f79,plain,
! [X0,X1] :
( ~ h_true_only(X0,X1)
| h_true(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f80,plain,
! [X0,X1] :
( h_false(X0,X1)
| ~ h_true(X0,X1)
| h_true_only(X0,X1) ),
inference(cnf_transformation,[],[f39]) ).
fof(f81,plain,
! [X0,X1] :
( ~ h_both(X0,X1)
| h_false(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f82,plain,
! [X0,X1] :
( ~ h_both(X0,X1)
| h_true(X0,X1) ),
inference(cnf_transformation,[],[f41]) ).
fof(f84,plain,
! [X0,X1] :
( ~ h_false_only(X0,X1)
| ~ h_true(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f85,plain,
! [X0,X1] :
( ~ h_false_only(X0,X1)
| h_false(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f86,plain,
! [X0,X1] :
( h_true(X0,X1)
| ~ h_false(X0,X1)
| h_false_only(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f87,plain,
! [X0,X1] :
( h_false_only(X0,X1)
| h_both(X0,X1)
| h_true_only(X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] :
( ~ sP3
| ~ g_true_only(X0,X1)
| ~ h_both(X0,sK4(X0,X1)) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i] :
( ~ sP3
| ~ g_true_only(X0,X1)
| ~ h_false_only(X0,sK4(X0,X1)) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i] :
( ~ sP3
| ~ g_both(X0,X1)
| ~ h_false_only(X0,sK4(X0,X1)) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( g_false_only(X0,X2)
| h_false_only(X0,X3)
| g_true_only(X0,sK6(X0))
| h_true_only(X0,sK5(X0,X2))
| ~ sP2
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_56,plain,
( g_both(sK7,sK8)
| g_true_only(sK7,sK8)
| ~ sP1 ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_57,plain,
! [X0: $i] :
( g_true_only(sK7,sK8)
| h_false_only(sK7,X0)
| ~ sP1 ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_58,plain,
! [X0: $i] :
( g_both(sK7,sK8)
| h_false_only(sK7,X0)
| h_both(sK7,X0)
| ~ sP1 ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_59,plain,
! [X0: $i] :
( h_false_only(sK7,X0)
| h_both(sK7,X0)
| ~ sP1 ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_63,negated_conjecture,
( ~ g_false_only(sK12,sK13)
| ~ g_false_only(sK10,sK11) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_64,negated_conjecture,
! [X0: $i] :
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,X0) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_65,negated_conjecture,
! [X0: $i] :
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,X0) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_66,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ h_true_only(sK12,X1)
| ~ h_true_only(sK10,X0) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_67,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP3
| h_true_only(X0,sK14(X0))
| ~ h_both(X0,X2)
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_68,negated_conjecture,
! [X0: $i,X1: $i] :
( sP3
| ~ g_true_only(X0,X1)
| ~ h_false_only(X0,sK15(X0)) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_69,negated_conjecture,
! [X0: $i,X1: $i] :
( sP3
| g_true_only(X0,sK16(X0))
| ~ g_both(X0,X1)
| ~ h_false_only(X0,sK17(X0)) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_70,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP1
| sP2
| sP0(sK20)
| g_true_only(sK20,sK21)
| h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_71,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1
| sP2
| sP0(sK20)
| h_both(sK20,sK22)
| h_false_only(sK20,X3)
| h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_72,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP1
| sP2
| sP0(sK20)
| h_false_only(sK20,X4)
| h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ h_true_only(sK20,X3)
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| g_true_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i] :
( ~ g_false(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_77,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_false_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] :
( ~ g_true(X0,X1)
| ~ g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i] :
( g_false_only(X0,X1)
| g_both(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i] :
( h_false(X0,X1)
| h_true_only(X0,X1)
| ~ h_true(X0,X1) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i] :
( h_true(X0,X1)
| ~ h_true_only(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i] :
( ~ h_false(X0,X1)
| ~ h_true_only(X0,X1) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_87,plain,
! [X0: $i,X1: $i] :
( h_true(X0,X1)
| ~ h_both(X0,X1) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] :
( h_false(X0,X1)
| ~ h_both(X0,X1) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i] :
( h_true(X0,X1)
| h_false_only(X0,X1)
| ~ h_false(X0,X1) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i] :
( h_false(X0,X1)
| ~ h_false_only(X0,X1) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] :
( ~ h_true(X0,X1)
| ~ h_false_only(X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] :
( h_true_only(X0,X1)
| h_false_only(X0,X1)
| h_both(X0,X1) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] :
( h_true(X0,X1)
| h_false_only(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_89,c_87,c_84,c_92]) ).
tcf(c_135,plain,
! [X0: $i,X1: $i] :
( h_false(X0,X1)
| h_true_only(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_83,c_90,c_88,c_92]) ).
tcf(c_138,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_false_only(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_79,c_77,c_74,c_82]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| g_true_only(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_73,c_80,c_73,c_138]) ).
tcf(c_144,plain,
! [X0: $i] :
( ~ sP1
| h_both(sK7,X0)
| h_false_only(sK7,X0) ),
inference(global_subsumption_just,[status(thm)],[c_58,c_59]) ).
tcf(c_145,plain,
! [X0: $i] :
( h_false_only(sK7,X0)
| h_both(sK7,X0)
| ~ sP1 ),
inference(renaming,[status(thm)],[c_144]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i] :
( ~ g_true_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_75]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i] :
( ~ g_false(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(renaming,[status(thm)],[c_148]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i] :
( g_true_only(X0,X1)
| g_false(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_141]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| g_true_only(X0,X1) ),
inference(renaming,[status(thm)],[c_150]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i] :
( ~ g_false_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_81]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( ~ g_true(X0,X1)
| ~ g_false_only(X0,X1) ),
inference(renaming,[status(thm)],[c_152]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i] :
( g_false_only(X0,X1)
| g_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_138]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_false_only(X0,X1) ),
inference(renaming,[status(thm)],[c_154]) ).
tcf(c_156,plain,
! [X0: $i,X1: $i] :
( ~ h_false_only(X0,X1)
| ~ h_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_91]) ).
tcf(c_157,plain,
! [X0: $i,X1: $i] :
( ~ h_true(X0,X1)
| ~ h_false_only(X0,X1) ),
inference(renaming,[status(thm)],[c_156]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i] :
( h_false_only(X0,X1)
| h_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_132]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i] :
( h_true(X0,X1)
| h_false_only(X0,X1) ),
inference(renaming,[status(thm)],[c_158]) ).
tcf(c_160,plain,
! [X0: $i,X1: $i] :
( ~ h_true_only(X0,X1)
| ~ h_false(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_85]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i] :
( ~ h_false(X0,X1)
| ~ h_true_only(X0,X1) ),
inference(renaming,[status(thm)],[c_160]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_both(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_77]) ).
tcf(c_168,plain,
! [X0: $i,X1: $i] :
( h_true(X0,X1)
| ~ h_both(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_87]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i] :
( h_false(X0,X1)
| ~ h_both(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_88]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i] :
( h_false(X0,X1)
| h_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_84,c_135]) ).
tcf(c_283,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ sP3
| ~ h_both(X0,sK4(X0,X1)) ),
inference(bin_hyper_res,[status(thm)],[c_49,c_151]) ).
tcf(c_284,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ sP3
| ~ h_false_only(X0,sK4(X0,X1)) ),
inference(bin_hyper_res,[status(thm)],[c_50,c_151]) ).
tcf(c_285,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP3
| g_false(X0,X2)
| h_true_only(X0,sK14(X0))
| ~ h_both(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_67,c_151]) ).
tcf(c_286,negated_conjecture,
! [X0: $i,X1: $i] :
( sP3
| g_false(X0,X1)
| ~ h_false_only(X0,sK15(X0)) ),
inference(bin_hyper_res,[status(thm)],[c_68,c_151]) ).
tcf(c_287,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| ~ g_false(X0,X1)
| ~ g_true(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_82,c_153,c_149]) ).
tcf(c_554,plain,
! [X0: $i,X1: $i] :
( g_false_only(X0,X1)
| g_both(X0,X1)
| ~ g_false(X0,X1) ),
inference(resolution,[status(thm)],[c_155,c_287]) ).
tcf(c_565,plain,
! [X0: $i,X1: $i] :
( ~ g_false_only(X0,X1)
| ~ g_both(X0,X1) ),
inference(resolution,[status(thm)],[c_164,c_153]) ).
tcf(c_582,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( h_false_only(X0,X3)
| g_true_only(X0,sK6(X0))
| h_true_only(X0,sK5(X0,X2))
| ~ sP2
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_53,c_565]) ).
tcf(c_587,plain,
! [X0: $i,X1: $i] :
( h_true(X0,X1)
| ~ h_true_only(X0,X1) ),
inference(resolution,[status(thm)],[c_208,c_161]) ).
tcf(c_607,plain,
! [X0: $i,X1: $i] :
( ~ h_true_only(X0,X1)
| ~ h_both(X0,X1) ),
inference(resolution,[status(thm)],[c_170,c_161]) ).
tcf(c_649,plain,
! [X0: $i,X1: $i] :
( ~ h_false_only(X0,X1)
| ~ h_both(X0,X1) ),
inference(resolution,[status(thm)],[c_168,c_157]) ).
tcf(c_666,plain,
! [X0: $i,X1: $i] :
( ~ h_true_only(X0,X1)
| ~ h_false_only(X0,X1) ),
inference(resolution,[status(thm)],[c_587,c_157]) ).
tcf(c_1986,plain,
! [X0: $i] :
( g_false(sK7,X0)
| h_both(sK7,sK4(sK7,X0))
| ~ sP1
| ~ sP3 ),
inference(resolution,[status(thm)],[c_284,c_145]) ).
tcf(c_1996,plain,
! [X0: $i] :
( g_false(sK7,X0)
| ~ sP1
| ~ sP3 ),
inference(forward_subsumption_resolution,[status(thm)],[c_1986,c_283]) ).
tcf(c_2016,plain,
! [X0: $i] :
( g_true_only(sK7,sK8)
| ~ sP1
| ~ sP3
| ~ g_both(sK7,X0) ),
inference(resolution,[status(thm)],[c_51,c_57]) ).
tcf(c_2348,plain,
! [X0: $i] :
( sP3
| g_false(sK7,X0)
| h_both(sK7,sK15(sK7))
| ~ sP1 ),
inference(resolution,[status(thm)],[c_145,c_286]) ).
tcf(c_2350,plain,
! [X0: $i] :
( ~ sP1
| h_both(sK7,sK15(sK7))
| g_false(sK7,X0) ),
inference(global_subsumption_just,[status(thm)],[c_2348,c_1996,c_2348]) ).
tcf(c_2351,plain,
! [X0: $i] :
( g_false(sK7,X0)
| h_both(sK7,sK15(sK7))
| ~ sP1 ),
inference(renaming,[status(thm)],[c_2350]) ).
tcf(c_2376,plain,
! [X0: $i] :
( sP3
| h_both(sK7,sK17(sK7))
| g_true_only(sK7,sK16(sK7))
| ~ sP1
| ~ g_both(sK7,X0) ),
inference(resolution,[status(thm)],[c_145,c_69]) ).
tcf(c_2393,plain,
! [X0: $i] :
( sP3
| g_true_only(sK7,sK8)
| g_true_only(sK7,sK16(sK7))
| ~ sP1
| ~ g_both(sK7,X0) ),
inference(resolution,[status(thm)],[c_57,c_69]) ).
tcf(c_2395,plain,
! [X0: $i] :
( ~ g_both(sK7,X0)
| ~ sP1
| g_true_only(sK7,sK16(sK7))
| g_true_only(sK7,sK8) ),
inference(global_subsumption_just,[status(thm)],[c_2393,c_2016,c_2393]) ).
tcf(c_2396,plain,
! [X0: $i] :
( g_true_only(sK7,sK8)
| g_true_only(sK7,sK16(sK7))
| ~ sP1
| ~ g_both(sK7,X0) ),
inference(renaming,[status(thm)],[c_2395]) ).
tcf(c_4124,plain,
! [X0: $i,X1: $i] :
( ~ g_false_only(X0,X1)
| ~ g_both(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_565]) ).
tcf(c_4132,plain,
! [X0: $i,X1: $i] :
( ~ h_true_only(X0,X1)
| ~ h_both(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_607]) ).
tcf(c_4134,plain,
! [X0: $i,X1: $i] :
( ~ h_false_only(X0,X1)
| ~ h_both(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_649]) ).
tcf(c_4148,plain,
! [X0: $i,X1: $i] :
( ~ h_true_only(X0,X1)
| ~ h_false_only(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_666]) ).
tcf(c_6255,negated_conjecture,
( iPr_def_11
| sP1
| sP2
| sP0(sK20)
| g_true_only(sK20,sK21) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_70]) ).
tcf(c_6256,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ~ h_true_only(sK12,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_66]) ).
tcf(c_6257,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ~ h_true_only(sK10,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_66]) ).
tcf(c_6258,negated_conjecture,
( iPr_def_14
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_66]) ).
tcf(c_6259,plain,
! [X0: $i] :
( ~ iPr_def_15
| h_false_only(sK7,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_57]) ).
tcf(c_6260,plain,
( iPr_def_15
| g_true_only(sK7,sK8)
| ~ sP1 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_57]) ).
tcf(c_6267,negated_conjecture,
! [X0: $i,X1: $i] :
( sP3
| g_false(X0,X1)
| ~ h_false_only(X0,sK15(X0)) ),
inference(demodulation,[status(thm)],[c_286]) ).
tcf(c_6268,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( sP3
| g_false(X0,X2)
| h_true_only(X0,sK14(X0))
| ~ h_both(X0,X1) ),
inference(demodulation,[status(thm)],[c_285]) ).
tcf(c_6269,negated_conjecture,
( iPr_def_11
| sP1
| sP2
| sP0(sK20)
| g_true_only(sK20,sK21) ),
inference(demodulation,[status(thm)],[c_6255]) ).
tcf(c_6271,negated_conjecture,
! [X0: $i,X1: $i] :
( sP3
| g_true_only(X0,sK16(X0))
| ~ g_both(X0,X1)
| ~ h_false_only(X0,sK17(X0)) ),
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_6272,negated_conjecture,
( iPr_def_14
| iPr_def_13 ),
inference(demodulation,[status(thm)],[c_6258]) ).
tcf(c_6273,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ~ h_true_only(sK10,X0) ),
inference(demodulation,[status(thm)],[c_6257]) ).
tcf(c_6274,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ~ h_true_only(sK12,X0) ),
inference(demodulation,[status(thm)],[c_6256]) ).
tcf(c_6275,negated_conjecture,
! [X0: $i] :
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,X0) ),
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_6276,negated_conjecture,
! [X0: $i] :
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,X0) ),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_6284,plain,
( g_false_only(sK10,sK11)
| g_both(sK10,sK11)
| ~ g_false(sK10,sK11) ),
inference(instantiation,[status(thm)],[c_554]) ).
tcf(c_6285,plain,
( g_false_only(sK12,sK13)
| g_both(sK12,sK13)
| ~ g_false(sK12,sK13) ),
inference(instantiation,[status(thm)],[c_554]) ).
tcf(c_6286,plain,
( ~ g_false_only(sK10,sK11)
| ~ g_both(sK10,sK11) ),
inference(instantiation,[status(thm)],[c_4124]) ).
tcf(c_6287,plain,
( sP3
| g_true_only(sK10,sK16(sK10))
| ~ g_both(sK10,sK11)
| ~ h_false_only(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_6271]) ).
tcf(c_6289,plain,
( sP3
| g_true_only(sK12,sK16(sK12))
| ~ g_both(sK12,sK13)
| ~ h_false_only(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_6271]) ).
tcf(c_6290,plain,
( ~ g_false(sK10,sK16(sK10))
| ~ g_true_only(sK10,sK16(sK10)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_6291,plain,
( ~ g_false(sK12,sK16(sK12))
| ~ g_true_only(sK12,sK16(sK12)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_6298,plain,
( sP3
| g_false(sK10,sK11)
| ~ h_false_only(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_6267]) ).
tcf(c_6299,plain,
! [X0: $i] :
( sP3
| g_false(sK10,sK11)
| h_true_only(sK10,sK14(sK10))
| ~ h_both(sK10,X0) ),
inference(instantiation,[status(thm)],[c_6268]) ).
tcf(c_6305,plain,
( sP3
| g_false(sK12,sK13)
| ~ h_false_only(sK12,sK15(sK12)) ),
inference(instantiation,[status(thm)],[c_6267]) ).
tcf(c_6306,plain,
! [X0: $i] :
( sP3
| g_false(sK12,sK13)
| h_true_only(sK12,sK14(sK12))
| ~ h_both(sK12,X0) ),
inference(instantiation,[status(thm)],[c_6268]) ).
tcf(c_6312,plain,
! [X0: $i,X1: $i] :
( h_false_only(sK10,sK17(sK10))
| g_true_only(sK10,sK6(sK10))
| h_true_only(sK10,sK5(sK10,X1))
| ~ sP2
| ~ g_both(sK10,X1)
| ~ h_both(sK10,X0) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_6315,plain,
( h_true_only(sK10,sK17(sK10))
| h_false_only(sK10,sK17(sK10))
| h_both(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_6324,plain,
( ~ g_false(sK10,sK6(sK10))
| ~ g_true_only(sK10,sK6(sK10)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_6329,plain,
( ~ sP3
| ~ g_both(sK10,sK11)
| ~ h_false_only(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_6331,plain,
! [X0: $i,X1: $i] :
( g_true_only(sK10,sK6(sK10))
| h_false_only(sK10,sK4(sK10,sK11))
| h_true_only(sK10,sK5(sK10,X1))
| ~ sP2
| ~ g_both(sK10,X1)
| ~ h_both(sK10,X0) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_6334,plain,
( h_true_only(sK10,sK4(sK10,sK11))
| h_false_only(sK10,sK4(sK10,sK11))
| h_both(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_6343,plain,
! [X0: $i] :
( g_true_only(sK10,sK6(sK10))
| h_false_only(sK10,sK4(sK10,sK11))
| h_true_only(sK10,sK5(sK10,X0))
| ~ sP2
| ~ g_both(sK10,X0)
| ~ h_both(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_6331]) ).
tcf(c_6350,plain,
( ~ sP3
| ~ g_both(sK12,sK13)
| ~ h_false_only(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_6355,plain,
! [X0: $i,X1: $i] :
( g_true_only(sK12,sK6(sK12))
| h_false_only(sK12,sK4(sK12,sK13))
| h_true_only(sK12,sK5(sK12,X1))
| ~ sP2
| ~ g_both(sK12,X1)
| ~ h_both(sK12,X0) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_6358,plain,
( h_true_only(sK12,sK4(sK12,sK13))
| h_false_only(sK12,sK4(sK12,sK13))
| h_both(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_6367,plain,
! [X0: $i] :
( g_true_only(sK12,sK6(sK12))
| h_false_only(sK12,sK4(sK12,sK13))
| h_true_only(sK12,sK5(sK12,X0))
| ~ sP2
| ~ g_both(sK12,X0)
| ~ h_both(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_6355]) ).
tcf(c_6376,plain,
( g_true_only(sK12,sK6(sK12))
| h_true_only(sK12,sK5(sK12,sK13))
| h_false_only(sK12,sK4(sK12,sK13))
| ~ sP2
| ~ g_both(sK12,sK13)
| ~ h_both(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_6367]) ).
tcf(c_6378,plain,
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,sK5(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_6276]) ).
tcf(c_6379,plain,
( ~ iPr_def_13
| ~ h_true_only(sK12,sK5(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_6274]) ).
tcf(c_6381,plain,
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_6276]) ).
tcf(c_6382,plain,
( ~ iPr_def_13
| ~ h_true_only(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_6274]) ).
tcf(c_6385,plain,
( g_false(sK10,sK11)
| ~ sP3
| ~ h_false_only(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_6386,plain,
( g_false(sK10,sK11)
| ~ sP3
| ~ h_both(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_6417,plain,
( ~ iPr_def_14
| ~ h_true_only(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_6273]) ).
tcf(c_6418,plain,
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_6275]) ).
tcf(c_6458,plain,
( g_true_only(sK10,sK6(sK10))
| h_true_only(sK10,sK5(sK10,sK11))
| h_false_only(sK10,sK4(sK10,sK11))
| ~ sP2
| ~ g_both(sK10,sK11)
| ~ h_both(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_6343]) ).
tcf(c_6467,plain,
( ~ iPr_def_14
| ~ h_true_only(sK10,sK5(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_6273]) ).
tcf(c_6468,plain,
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,sK5(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_6275]) ).
tcf(c_6476,plain,
( g_false(sK10,sK6(sK10))
| ~ sP3
| ~ h_false_only(sK10,sK4(sK10,sK6(sK10))) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_6477,plain,
( g_false(sK10,sK6(sK10))
| ~ sP3
| ~ h_both(sK10,sK4(sK10,sK6(sK10))) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_6482,plain,
( sP3
| g_false(sK10,sK6(sK10))
| ~ h_false_only(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_6267]) ).
tcf(c_6483,plain,
! [X0: $i] :
( sP3
| g_false(sK10,sK6(sK10))
| h_true_only(sK10,sK14(sK10))
| ~ h_both(sK10,X0) ),
inference(instantiation,[status(thm)],[c_6268]) ).
tcf(c_6495,plain,
( h_true_only(sK10,sK4(sK10,sK6(sK10)))
| h_false_only(sK10,sK4(sK10,sK6(sK10)))
| h_both(sK10,sK4(sK10,sK6(sK10))) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_6519,plain,
( ~ iPr_def_14
| ~ h_true_only(sK10,sK4(sK10,sK6(sK10))) ),
inference(instantiation,[status(thm)],[c_6273]) ).
tcf(c_6520,plain,
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,sK4(sK10,sK6(sK10))) ),
inference(instantiation,[status(thm)],[c_6275]) ).
tcf(c_6560,plain,
( ~ g_false(sK10,sK18(sK10))
| ~ g_true_only(sK10,sK18(sK10)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_6570,plain,
( ~ iPr_def_14
| ~ h_true_only(sK10,sK19(sK10)) ),
inference(instantiation,[status(thm)],[c_6273]) ).
tcf(c_6571,plain,
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,sK19(sK10)) ),
inference(instantiation,[status(thm)],[c_6275]) ).
tcf(c_6589,plain,
( g_false(sK10,sK18(sK10))
| ~ sP3
| ~ h_false_only(sK10,sK4(sK10,sK18(sK10))) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_6590,plain,
( g_false(sK10,sK18(sK10))
| ~ sP3
| ~ h_both(sK10,sK4(sK10,sK18(sK10))) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_6596,plain,
! [X0: $i] :
( sP3
| g_false(sK10,sK18(sK10))
| h_true_only(sK10,sK14(sK10))
| ~ h_both(sK10,X0) ),
inference(instantiation,[status(thm)],[c_6268]) ).
tcf(c_6614,plain,
( h_true_only(sK10,sK4(sK10,sK18(sK10)))
| h_false_only(sK10,sK4(sK10,sK18(sK10)))
| h_both(sK10,sK4(sK10,sK18(sK10))) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_6631,plain,
( ~ iPr_def_14
| ~ h_true_only(sK10,sK4(sK10,sK18(sK10))) ),
inference(instantiation,[status(thm)],[c_6273]) ).
tcf(c_6632,plain,
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,sK4(sK10,sK18(sK10))) ),
inference(instantiation,[status(thm)],[c_6275]) ).
tcf(c_6833,plain,
( ~ g_false(sK7,sK8)
| ~ g_true_only(sK7,sK8) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_6835,plain,
( g_false(sK7,sK8)
| ~ sP3
| ~ h_false_only(sK7,sK4(sK7,sK8)) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_6836,plain,
( g_false(sK7,sK8)
| ~ sP3
| ~ h_both(sK7,sK4(sK7,sK8)) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_6841,plain,
( sP3
| g_false(sK7,sK8)
| ~ h_false_only(sK7,sK15(sK7)) ),
inference(instantiation,[status(thm)],[c_6267]) ).
tcf(c_6893,plain,
! [X0: $i] :
( sP3
| g_true_only(sK7,sK16(sK7))
| ~ iPr_def_15
| ~ g_both(sK7,X0) ),
inference(superposition,[status(thm)],[c_6259,c_6271]) ).
tcf(c_6918,plain,
! [X0: $i] :
( sP3
| g_true_only(sK7,sK16(sK7))
| ~ iPr_def_15
| ~ g_both(sK7,X0) ),
inference(superposition,[status(thm)],[c_6259,c_6271]) ).
tcf(c_6945,plain,
( h_false_only(sK7,sK4(sK7,sK8))
| h_both(sK7,sK4(sK7,sK8))
| ~ sP1 ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_6950,plain,
( ~ g_false(sK20,sK21)
| ~ g_true_only(sK20,sK21) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_6966,plain,
( g_false(sK20,sK21)
| ~ sP3
| ~ h_false_only(sK20,sK4(sK20,sK21)) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_6967,plain,
( g_false(sK20,sK21)
| ~ sP3
| ~ h_both(sK20,sK4(sK20,sK21)) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_7066,plain,
( h_true_only(sK20,sK4(sK20,sK21))
| h_false_only(sK20,sK4(sK20,sK21))
| h_both(sK20,sK4(sK20,sK21)) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_7165,plain,
( ~ sP3
| ~ g_both(sK7,sK8)
| ~ h_false_only(sK7,sK4(sK7,sK8)) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_7173,plain,
( h_false_only(sK7,sK4(sK7,sK8))
| ~ iPr_def_15 ),
inference(instantiation,[status(thm)],[c_6259]) ).
tcf(c_7184,plain,
( sP3
| g_true_only(sK7,sK8)
| g_true_only(sK7,sK16(sK7))
| ~ iPr_def_15
| ~ sP1 ),
inference(superposition,[status(thm)],[c_56,c_6893]) ).
tcf(c_7256,plain,
( sP3
| g_true_only(sK7,sK8)
| g_true_only(sK7,sK16(sK7))
| ~ iPr_def_15
| ~ sP1 ),
inference(superposition,[status(thm)],[c_56,c_6918]) ).
tcf(c_7290,plain,
( ~ g_false(sK12,sK18(sK12))
| ~ g_true_only(sK12,sK18(sK12)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_7293,plain,
( g_false(sK12,sK18(sK12))
| ~ sP3
| ~ h_false_only(sK12,sK4(sK12,sK18(sK12))) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_7294,plain,
( g_false(sK12,sK18(sK12))
| ~ sP3
| ~ h_both(sK12,sK4(sK12,sK18(sK12))) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_7300,plain,
! [X0: $i] :
( sP3
| g_false(sK12,sK18(sK12))
| h_true_only(sK12,sK14(sK12))
| ~ h_both(sK12,X0) ),
inference(instantiation,[status(thm)],[c_6268]) ).
tcf(c_7308,plain,
! [X0: $i] :
( sP3
| g_false(sK7,X0)
| h_both(sK7,sK15(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_59,c_6267]) ).
tcf(c_7309,plain,
! [X0: $i] :
( sP3
| h_both(sK7,sK17(sK7))
| g_true_only(sK7,sK16(sK7))
| ~ sP1
| ~ g_both(sK7,X0) ),
inference(superposition,[status(thm)],[c_59,c_6271]) ).
tcf(c_7325,plain,
! [X0: $i] :
( sP3
| g_false(sK7,X0)
| h_both(sK7,sK15(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_59,c_6267]) ).
tcf(c_7340,plain,
( h_true_only(sK12,sK4(sK12,sK18(sK12)))
| h_false_only(sK12,sK4(sK12,sK18(sK12)))
| h_both(sK12,sK4(sK12,sK18(sK12))) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_7358,plain,
! [X0: $i] :
( ~ sP1
| h_both(sK7,sK15(sK7))
| g_false(sK7,X0) ),
inference(global_subsumption_just,[status(thm)],[c_7308,c_1996,c_2348]) ).
tcf(c_7359,plain,
! [X0: $i] :
( g_false(sK7,X0)
| h_both(sK7,sK15(sK7))
| ~ sP1 ),
inference(renaming,[status(thm)],[c_7358]) ).
tcf(c_7367,plain,
! [X0: $i,X1: $i] :
( sP3
| g_false(sK7,X1)
| g_false(sK7,X0)
| h_true_only(sK7,sK14(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_7359,c_6268]) ).
tcf(c_7385,plain,
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,sK4(sK12,sK18(sK12))) ),
inference(instantiation,[status(thm)],[c_6276]) ).
tcf(c_7386,plain,
( ~ iPr_def_13
| ~ h_true_only(sK12,sK4(sK12,sK18(sK12))) ),
inference(instantiation,[status(thm)],[c_6274]) ).
tcf(c_7423,plain,
! [X0: $i] :
( ~ sP1
| h_both(sK7,sK15(sK7))
| g_false(sK7,X0) ),
inference(global_subsumption_just,[status(thm)],[c_7325,c_2351]) ).
tcf(c_7424,plain,
! [X0: $i] :
( g_false(sK7,X0)
| h_both(sK7,sK15(sK7))
| ~ sP1 ),
inference(renaming,[status(thm)],[c_7423]) ).
tcf(c_7433,plain,
! [X0: $i,X1: $i] :
( sP3
| g_false(sK7,X1)
| g_false(sK7,X0)
| h_true_only(sK7,sK14(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_7424,c_6268]) ).
tcf(c_7457,plain,
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,sK19(sK12)) ),
inference(instantiation,[status(thm)],[c_6276]) ).
tcf(c_7458,plain,
( ~ iPr_def_13
| ~ h_true_only(sK12,sK19(sK12)) ),
inference(instantiation,[status(thm)],[c_6274]) ).
tcf(c_7518,plain,
( g_false(sK12,sK13)
| ~ sP3
| ~ h_false_only(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_7519,plain,
( g_false(sK12,sK13)
| ~ sP3
| ~ h_both(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_7526,plain,
! [X0: $i,X1: $i] :
( ~ sP1
| h_true_only(sK7,sK14(sK7))
| g_false(sK7,X0)
| g_false(sK7,X1) ),
inference(global_subsumption_just,[status(thm)],[c_7367,c_1996,c_7367]) ).
tcf(c_7527,plain,
! [X0: $i,X1: $i] :
( g_false(sK7,X1)
| g_false(sK7,X0)
| h_true_only(sK7,sK14(sK7))
| ~ sP1 ),
inference(renaming,[status(thm)],[c_7526]) ).
tcf(c_7538,plain,
! [X0: $i] :
( g_false(sK7,X0)
| h_true_only(sK7,sK14(sK7))
| ~ sP1 ),
inference(equality_factoring,[status(thm)],[c_7527]) ).
tcf(c_7543,plain,
! [X0: $i] :
( g_false(sK7,X0)
| h_true_only(sK7,sK14(sK7))
| ~ sP1 ),
inference(global_subsumption_just,[status(thm)],[c_7433,c_7538]) ).
tcf(c_7552,plain,
! [X0: $i] :
( ~ g_both(sK7,X0)
| ~ sP1
| g_true_only(sK7,sK16(sK7))
| h_both(sK7,sK17(sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_7309,c_2376,c_2396,c_6833,c_6836,c_6835,c_6945]) ).
tcf(c_7553,plain,
! [X0: $i] :
( h_both(sK7,sK17(sK7))
| g_true_only(sK7,sK16(sK7))
| ~ sP1
| ~ g_both(sK7,X0) ),
inference(renaming,[status(thm)],[c_7552]) ).
tcf(c_7563,plain,
( g_true_only(sK7,sK8)
| h_both(sK7,sK17(sK7))
| g_true_only(sK7,sK16(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_56,c_7553]) ).
tcf(c_7660,plain,
( ~ sP1
| g_true_only(sK7,sK16(sK7))
| g_true_only(sK7,sK8) ),
inference(global_subsumption_just,[status(thm)],[c_7256,c_56,c_6260,c_7165,c_7173,c_7184]) ).
tcf(c_7661,plain,
( g_true_only(sK7,sK8)
| g_true_only(sK7,sK16(sK7))
| ~ sP1 ),
inference(renaming,[status(thm)],[c_7660]) ).
tcf(c_7681,plain,
( iPr_def_15
| ~ sP1
| ~ g_false(sK7,sK8) ),
inference(superposition,[status(thm)],[c_6260,c_75]) ).
tcf(c_7683,plain,
( iPr_def_11
| sP1
| sP2
| sP0(sK20)
| ~ g_false(sK20,sK21) ),
inference(superposition,[status(thm)],[c_6269,c_75]) ).
tcf(c_7684,plain,
( g_true_only(sK7,sK8)
| ~ sP1
| ~ g_false(sK7,sK16(sK7)) ),
inference(superposition,[status(thm)],[c_7661,c_75]) ).
tcf(c_7701,plain,
( g_true_only(sK7,sK8)
| ~ sP1
| g_true_only(sK7,sK16(sK7)) ),
inference(global_subsumption_just,[status(thm)],[c_7563,c_7661]) ).
tcf(c_7702,plain,
( g_true_only(sK7,sK8)
| g_true_only(sK7,sK16(sK7))
| ~ sP1 ),
inference(renaming,[status(thm)],[c_7701]) ).
tcf(c_7720,plain,
( iPr_def_15
| ~ sP1
| ~ g_false(sK7,sK8) ),
inference(superposition,[status(thm)],[c_6260,c_75]) ).
tcf(c_7722,plain,
( iPr_def_11
| sP1
| sP2
| sP0(sK20)
| ~ g_false(sK20,sK21) ),
inference(superposition,[status(thm)],[c_6269,c_75]) ).
tcf(c_7723,plain,
( g_true_only(sK7,sK8)
| ~ sP1
| ~ g_false(sK7,sK16(sK7)) ),
inference(superposition,[status(thm)],[c_7702,c_75]) ).
tcf(c_7764,plain,
( ~ g_false(sK12,sK6(sK12))
| ~ g_true_only(sK12,sK6(sK12)) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_7939,plain,
! [X0: $i] :
( g_false(sK7,X0)
| ~ sP1
| ~ h_false_only(sK7,sK15(sK7)) ),
inference(superposition,[status(thm)],[c_7359,c_4134]) ).
tcf(c_7989,plain,
( g_false(sK12,sK6(sK12))
| ~ sP3
| ~ h_false_only(sK12,sK4(sK12,sK6(sK12))) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_7990,plain,
( g_false(sK12,sK6(sK12))
| ~ sP3
| ~ h_both(sK12,sK4(sK12,sK6(sK12))) ),
inference(instantiation,[status(thm)],[c_283]) ).
tcf(c_7996,plain,
! [X0: $i] :
( sP3
| g_false(sK12,sK6(sK12))
| h_true_only(sK12,sK14(sK12))
| ~ h_both(sK12,X0) ),
inference(instantiation,[status(thm)],[c_6268]) ).
tcf(c_8016,plain,
( iPr_def_15
| h_true_only(sK7,sK14(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_7543,c_7681]) ).
tcf(c_8017,plain,
( iPr_def_15
| h_both(sK7,sK15(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_7424,c_7681]) ).
tcf(c_8046,plain,
( iPr_def_15
| h_true_only(sK7,sK14(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_7538,c_7720]) ).
tcf(c_8140,plain,
( h_true_only(sK12,sK4(sK12,sK6(sK12)))
| h_false_only(sK12,sK4(sK12,sK6(sK12)))
| h_both(sK12,sK4(sK12,sK6(sK12))) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_8204,plain,
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,sK4(sK12,sK6(sK12))) ),
inference(instantiation,[status(thm)],[c_6276]) ).
tcf(c_8205,plain,
( ~ iPr_def_13
| ~ h_true_only(sK12,sK4(sK12,sK6(sK12))) ),
inference(instantiation,[status(thm)],[c_6274]) ).
tcf(c_8246,plain,
( iPr_def_15
| ~ sP1
| ~ h_true_only(sK7,sK15(sK7)) ),
inference(superposition,[status(thm)],[c_8017,c_4132]) ).
tcf(c_8275,plain,
! [X0: $i,X1: $i] :
( h_false_only(sK12,sK17(sK12))
| g_true_only(sK12,sK6(sK12))
| h_true_only(sK12,sK5(sK12,X1))
| ~ sP2
| ~ g_both(sK12,X1)
| ~ h_both(sK12,X0) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_8278,plain,
( h_true_only(sK12,sK17(sK12))
| h_false_only(sK12,sK17(sK12))
| h_both(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_8287,plain,
! [X0: $i] :
( g_false(sK7,X0)
| ~ iPr_def_15
| ~ sP1 ),
inference(superposition,[status(thm)],[c_6259,c_7939]) ).
tcf(c_8301,plain,
( iPr_def_15
| ~ sP1
| ~ h_false_only(sK7,sK14(sK7)) ),
inference(superposition,[status(thm)],[c_8046,c_4148]) ).
tcf(c_8318,plain,
( h_false_only(sK7,sK15(sK7))
| ~ iPr_def_15 ),
inference(instantiation,[status(thm)],[c_6259]) ).
tcf(c_8402,plain,
! [X0: $i] :
( ~ iPr_def_15
| ~ sP3
| ~ g_both(sK7,X0) ),
inference(superposition,[status(thm)],[c_6259,c_51]) ).
tcf(c_8473,plain,
( h_true_only(sK12,sK15(sK12))
| h_false_only(sK12,sK15(sK12))
| h_both(sK12,sK15(sK12)) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_8525,plain,
( sP3
| g_false(sK12,sK6(sK12))
| h_true_only(sK12,sK14(sK12))
| ~ h_both(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_7996]) ).
tcf(c_8655,plain,
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,sK14(sK12)) ),
inference(instantiation,[status(thm)],[c_6276]) ).
tcf(c_8656,plain,
( ~ iPr_def_13
| ~ h_true_only(sK12,sK14(sK12)) ),
inference(instantiation,[status(thm)],[c_6274]) ).
tcf(c_8667,plain,
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_6276]) ).
tcf(c_8668,plain,
( ~ iPr_def_13
| ~ h_true_only(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_6274]) ).
tcf(c_8706,plain,
( sP3
| g_false(sK12,sK16(sK12))
| ~ h_false_only(sK12,sK15(sK12)) ),
inference(instantiation,[status(thm)],[c_6267]) ).
tcf(c_8707,plain,
! [X0: $i] :
( sP3
| g_false(sK12,sK16(sK12))
| h_true_only(sK12,sK14(sK12))
| ~ h_both(sK12,X0) ),
inference(instantiation,[status(thm)],[c_6268]) ).
tcf(c_8846,plain,
( ~ g_false_only(sK10,sK11)
| ~ h_true_only(sK12,sK15(sK12)) ),
inference(instantiation,[status(thm)],[c_6276]) ).
tcf(c_8847,plain,
( ~ iPr_def_13
| ~ h_true_only(sK12,sK15(sK12)) ),
inference(instantiation,[status(thm)],[c_6274]) ).
tcf(c_8932,plain,
! [X0: $i] :
( h_false_only(sK12,sK17(sK12))
| g_true_only(sK12,sK6(sK12))
| h_true_only(sK12,sK5(sK12,X0))
| ~ sP2
| ~ g_both(sK12,X0)
| ~ h_both(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_8275]) ).
tcf(c_9117,plain,
( iPr_def_15
| h_both(sK7,sK14(sK7))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_59,c_8301]) ).
tcf(c_9129,plain,
( iPr_def_15
| ~ sP1
| ~ h_true_only(sK7,sK14(sK7)) ),
inference(superposition,[status(thm)],[c_9117,c_4132]) ).
tcf(c_9216,plain,
( iPr_def_15
| ~ sP1 ),
inference(global_subsumption_just,[status(thm)],[c_8246,c_8016,c_9129]) ).
tcf(c_9264,plain,
( g_true_only(sK7,sK8)
| ~ iPr_def_15
| ~ sP1
| ~ sP3 ),
inference(superposition,[status(thm)],[c_56,c_8402]) ).
tcf(c_9286,plain,
( ~ sP1
| ~ sP3 ),
inference(global_subsumption_just,[status(thm)],[c_9264,c_6833,c_6835,c_7173,c_8016,c_9129,c_9264]) ).
tcf(c_9365,plain,
( h_false_only(sK12,sK17(sK12))
| g_true_only(sK12,sK6(sK12))
| h_true_only(sK12,sK5(sK12,sK13))
| ~ sP2
| ~ g_both(sK12,sK13)
| ~ h_both(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_8932]) ).
tcf(c_9492,plain,
( sP3
| g_false(sK12,sK16(sK12))
| h_true_only(sK12,sK14(sK12))
| ~ h_both(sK12,sK15(sK12)) ),
inference(instantiation,[status(thm)],[c_8707]) ).
tcf(c_9604,plain,
( h_true_only(sK10,sK15(sK10))
| h_false_only(sK10,sK15(sK10))
| h_both(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_9681,plain,
( sP3
| g_false(sK10,sK11)
| h_true_only(sK10,sK14(sK10))
| ~ h_both(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_6299]) ).
tcf(c_9750,plain,
( ~ iPr_def_14
| ~ h_true_only(sK10,sK14(sK10)) ),
inference(instantiation,[status(thm)],[c_6273]) ).
tcf(c_9751,plain,
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,sK14(sK10)) ),
inference(instantiation,[status(thm)],[c_6275]) ).
tcf(c_9802,plain,
( ~ iPr_def_14
| ~ h_true_only(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_6273]) ).
tcf(c_9803,plain,
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_6275]) ).
tcf(c_9841,plain,
( ~ iPr_def_14
| ~ h_true_only(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_6273]) ).
tcf(c_9842,plain,
( ~ g_false_only(sK12,sK13)
| ~ h_true_only(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_6275]) ).
tcf(c_9865,plain,
! [X0: $i] :
( h_false_only(sK10,sK17(sK10))
| g_true_only(sK10,sK6(sK10))
| h_true_only(sK10,sK5(sK10,X0))
| ~ sP2
| ~ g_both(sK10,X0)
| ~ h_both(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_6312]) ).
tcf(c_9926,plain,
( iPr_def_15
| ~ sP1 ),
inference(global_subsumption_just,[status(thm)],[c_9129,c_8016,c_9129]) ).
tcf(c_9932,plain,
! [X0: $i] :
( g_false(sK7,X0)
| ~ sP1 ),
inference(backward_subsumption_resolution,[status(thm)],[c_8287,c_9926]) ).
tcf(c_9995,plain,
( ~ g_false(sK7,sK16(sK7))
| ~ sP1 ),
inference(global_subsumption_just,[status(thm)],[c_7723,c_6833,c_6841,c_7684,c_8318,c_9216,c_9286]) ).
tcf(c_9996,plain,
( ~ sP1
| ~ g_false(sK7,sK16(sK7)) ),
inference(renaming,[status(thm)],[c_9995]) ).
tcf(c_9999,plain,
~ sP1,
inference(forward_subsumption_resolution,[status(thm)],[c_9996,c_9932]) ).
tcf(c_10447,plain,
( h_false_only(sK10,sK17(sK10))
| g_true_only(sK10,sK6(sK10))
| h_true_only(sK10,sK5(sK10,sK11))
| ~ sP2
| ~ g_both(sK10,sK11)
| ~ h_both(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_9865]) ).
tcf(c_10493,plain,
( sP3
| g_false(sK10,sK16(sK10))
| ~ h_false_only(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_6267]) ).
tcf(c_10494,plain,
! [X0: $i] :
( sP3
| g_false(sK10,sK16(sK10))
| h_true_only(sK10,sK14(sK10))
| ~ h_both(sK10,X0) ),
inference(instantiation,[status(thm)],[c_6268]) ).
tcf(c_10504,plain,
( sP3
| g_false(sK10,sK16(sK10))
| h_true_only(sK10,sK14(sK10))
| ~ h_both(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_10494]) ).
tcf(c_10590,plain,
( sP3
| g_false(sK10,sK6(sK10))
| h_true_only(sK10,sK14(sK10))
| ~ h_both(sK10,sK15(sK10)) ),
inference(instantiation,[status(thm)],[c_6483]) ).
tcf(c_10891,plain,
( sP3
| g_false(sK12,sK13)
| h_true_only(sK12,sK14(sK12))
| ~ h_both(sK12,sK15(sK12)) ),
inference(instantiation,[status(thm)],[c_6306]) ).
tcf(c_11336,plain,
( sP3
| g_false(sK10,sK18(sK10))
| h_true_only(sK10,sK14(sK10))
| ~ h_both(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_6596]) ).
tcf(c_11431,plain,
( sP3
| g_false(sK12,sK18(sK12))
| h_true_only(sK12,sK14(sK12))
| ~ h_both(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_7300]) ).
fof(f13,definition,
! [X22] :
( ~ sP0(X22)
| ( ! [X29] : h_false_only(X22,X29)
& ! [X28] : ~ g_true_only(X22,X28)
& ? [X27] : g_both(X22,X27) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f14,definition,
( ~ sP1
| ? [X36,X37] :
! [X38] :
( ( h_false_only(X36,X38)
& g_both(X36,X37) )
| ( ( h_false_only(X36,X38)
| h_both(X36,X38) )
& g_true_only(X36,X37) ) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f15,definition,
( ~ sP2
| ! [X30] :
( ? [X34] :
! [X35] :
( ( h_false_only(X30,X35)
& g_both(X30,X34) )
| ( ( h_false_only(X30,X35)
| h_both(X30,X35) )
& g_true_only(X30,X34) ) )
| ! [X31] :
( ? [X33] :
( h_true_only(X30,X33)
| g_false_only(X30,X31) )
| ! [X32] :
( ~ h_both(X30,X32)
| ~ g_both(X30,X31) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f16,definition,
( ~ sP3
| ! [X14,X15] :
? [X16] :
( ( ~ h_false_only(X14,X16)
| ~ g_both(X14,X15) )
& ( ( ~ h_false_only(X14,X16)
& ~ h_both(X14,X16) )
| ~ g_true_only(X14,X15) ) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f17,plain,
( ( sP1
| sP2
| ? [X22] :
( sP0(X22)
| ( ( ! [X26] : h_false_only(X22,X26)
| ( ! [X25] : ~ h_true_only(X22,X25)
& ? [X24] : h_both(X22,X24) ) )
& ? [X23] : g_true_only(X22,X23) ) )
| ! [X17] :
( ? [X21] : h_true_only(X17,X21)
| ! [X20] : ~ h_both(X17,X20)
| ? [X19] : g_true_only(X17,X19)
| ! [X18] : ~ g_both(X17,X18) ) )
& ( sP3
| ! [X6] :
( ( ? [X13] : ~ h_false_only(X6,X13)
| ? [X12] : g_true_only(X6,X12)
| ! [X11] : ~ g_both(X6,X11) )
& ( ( ? [X10] : ~ h_false_only(X6,X10)
& ( ? [X9] : h_true_only(X6,X9)
| ! [X8] : ~ h_both(X6,X8) ) )
| ! [X7] : ~ g_true_only(X6,X7) ) ) )
& ( ? [X3,X4] :
! [X5] :
( ~ h_true_only(X3,X5)
& ~ g_false_only(X3,X4) )
| ? [X0] :
( ! [X2] : ~ h_true_only(X0,X2)
& ? [X1] : ~ g_false_only(X0,X1) ) ) ),
inference(definition_folding,[],[f12,f16,f15,f14,f13]) ).
fof(f27,plain,
! [X22] :
( ~ sP0(X22)
| ( ! [X29] : h_false_only(X22,X29)
& ! [X28] : ~ g_true_only(X22,X28)
& ? [X27] : g_both(X22,X27) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f28,plain,
! [X0] :
( ~ sP0(X0)
| ( ! [X3] : h_false_only(X0,X3)
& ! [X2] : ~ g_true_only(X0,X2)
& ? [X1] : g_both(X0,X1) ) ),
inference(rectify,[],[f27]) ).
fof(f29,plain,
! [X0] :
( ~ sP0(X0)
| ( ! [X3] : h_false_only(X0,X3)
& ! [X2] : ~ g_true_only(X0,X2)
& g_both(X0,sK9(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X1,sK9(X0))],[f28]) ).
fof(f55,plain,
! [X3,X0] :
( ~ sP0(X0)
| h_false_only(X0,X3) ),
inference(cnf_transformation,[],[f29]) ).
fof(f56,plain,
! [X2,X0] :
( ~ sP0(X0)
| ~ g_true_only(X0,X2) ),
inference(cnf_transformation,[],[f29]) ).
fof(f57,plain,
! [X0] :
( ~ sP0(X0)
| g_both(X0,sK9(X0)) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_60,plain,
! [X0: $i] :
( g_both(X0,sK9(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0)
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i] :
( h_false_only(X0,X1)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ sP0(X0) ),
inference(prop_impl_just,[status(thm)],[c_80,c_61,c_73,c_138]) ).
tcf(c_176,plain,
! [X0: $i,X1: $i] :
( ~ h_true(X0,X1)
| ~ sP0(X0) ),
inference(prop_impl_just,[status(thm)],[c_62,c_91]) ).
tcf(c_177,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0)
| ~ h_true(X0,X1) ),
inference(renaming,[status(thm)],[c_176]) ).
tcf(c_632,plain,
! [X0: $i,X1: $i] :
( h_false_only(X0,X1)
| ~ sP0(X0) ),
inference(resolution,[status(thm)],[c_159,c_177]) ).
tcf(c_641,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0)
| ~ h_both(X0,X1) ),
inference(resolution,[status(thm)],[c_168,c_177]) ).
tcf(c_675,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1
| sP2
| h_both(sK20,sK22)
| h_false_only(sK20,X3)
| h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_71,c_632]) ).
tcf(c_676,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP1
| sP2
| h_false_only(sK20,X4)
| h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ h_true_only(sK20,X3)
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_72,c_632]) ).
tcf(c_2061,plain,
! [X0: $i,X1: $i] :
( ~ sP3
| ~ sP0(X0)
| ~ g_both(X0,X1) ),
inference(resolution,[status(thm)],[c_51,c_632]) ).
tcf(c_2442,plain,
! [X0: $i,X1: $i] :
( sP3
| g_true_only(X0,sK16(X0))
| ~ sP0(X0)
| ~ g_both(X0,X1) ),
inference(resolution,[status(thm)],[c_632,c_69]) ).
tcf(c_2444,plain,
! [X0: $i,X1: $i] :
( ~ g_both(X0,X1)
| ~ sP0(X0)
| g_true_only(X0,sK16(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_2442,c_2061,c_2442]) ).
tcf(c_2445,plain,
! [X0: $i,X1: $i] :
( g_true_only(X0,sK16(X0))
| ~ sP0(X0)
| ~ g_both(X0,X1) ),
inference(renaming,[status(thm)],[c_2444]) ).
tcf(c_2456,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1
| sP2
| h_both(sK20,sK22)
| h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ h_true_only(sK20,X3)
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(resolution,[status(thm)],[c_666,c_675]) ).
tcf(c_2534,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP1
| sP2
| h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ h_true_only(sK20,X4)
| ~ h_both(sK20,X3)
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(resolution,[status(thm)],[c_649,c_676]) ).
tcf(c_2554,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP1
| sP2
| h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ h_true_only(sK20,X3)
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2456,c_2534]) ).
tcf(c_4130,plain,
! [X0: $i,X1: $i] :
( ~ sP0(X0)
| ~ h_both(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_641]) ).
tcf(c_4142,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ sP0(X0) ),
inference(prop_impl_just,[status(thm)],[c_174]) ).
tcf(c_6250,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ h_true_only(sK20,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_2554]) ).
tcf(c_6251,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ iPr_def_11
| g_true_only(X0,sK18(X0))
| ~ h_both(X0,X2)
| ~ g_both(X0,X1)
| h_true_only(X0,sK19(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_2554]) ).
tcf(c_6252,plain,
( iPr_def_11
| iPr_def_10
| sP1
| sP2 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_2554]) ).
tcf(c_6253,plain,
! [X0: $i] :
( ~ iPr_def_12
| h_false_only(sK20,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_675]) ).
tcf(c_6254,plain,
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| h_both(sK20,sK22) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_675]) ).
tcf(c_6261,plain,
( iPr_def_11
| iPr_def_10
| sP1
| sP2 ),
inference(demodulation,[status(thm)],[c_6252]) ).
tcf(c_6263,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ h_true_only(sK20,X0) ),
inference(demodulation,[status(thm)],[c_6250]) ).
tcf(c_6264,plain,
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| h_both(sK20,sK22) ),
inference(demodulation,[status(thm)],[c_6254]) ).
tcf(c_6266,plain,
! [X0: $i] :
( h_false_only(sK20,X0)
| ~ iPr_def_12 ),
inference(demodulation,[status(thm)],[c_6253]) ).
tcf(c_6270,plain,
! [X0: $i,X1: $i,X2: $i] :
( h_true_only(X0,sK19(X0))
| g_true_only(X0,sK18(X0))
| ~ iPr_def_11
| ~ g_both(X0,X2)
| ~ h_both(X0,X1) ),
inference(demodulation,[status(thm)],[c_6251]) ).
tcf(c_6541,plain,
! [X0: $i] :
( h_true_only(sK10,sK19(sK10))
| g_true_only(sK10,sK18(sK10))
| ~ iPr_def_11
| ~ g_both(sK10,X0)
| ~ h_both(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_6270]) ).
tcf(c_6567,plain,
( h_true_only(sK10,sK19(sK10))
| g_true_only(sK10,sK18(sK10))
| ~ iPr_def_11
| ~ g_both(sK10,sK11)
| ~ h_both(sK10,sK4(sK10,sK11)) ),
inference(instantiation,[status(thm)],[c_6541]) ).
tcf(c_6857,plain,
! [X0: $i] :
( sP3
| g_false(sK20,X0)
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_6266,c_6267]) ).
tcf(c_6894,plain,
! [X0: $i,X1: $i] :
( sP3
| g_true_only(X0,sK16(X0))
| ~ sP0(X0)
| ~ g_both(X0,X1) ),
inference(superposition,[status(thm)],[c_62,c_6271]) ).
tcf(c_7068,plain,
! [X0: $i,X1: $i] :
( ~ g_both(X0,X1)
| ~ sP0(X0)
| g_true_only(X0,sK16(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_6894,c_2445]) ).
tcf(c_7069,plain,
! [X0: $i,X1: $i] :
( g_true_only(X0,sK16(X0))
| ~ sP0(X0)
| ~ g_both(X0,X1) ),
inference(renaming,[status(thm)],[c_7068]) ).
tcf(c_7076,plain,
! [X0: $i] :
( g_true_only(X0,sK16(X0))
| ~ sP0(X0) ),
inference(superposition,[status(thm)],[c_60,c_7069]) ).
tcf(c_7098,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| sP3
| g_false(sK20,X0)
| h_true_only(sK20,sK14(sK20)) ),
inference(superposition,[status(thm)],[c_6264,c_6268]) ).
tcf(c_7115,plain,
( ~ iPr_def_10
| ~ h_true_only(sK20,sK4(sK20,sK21)) ),
inference(instantiation,[status(thm)],[c_6263]) ).
tcf(c_7130,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| sP3
| g_false(sK20,X0)
| h_true_only(sK20,sK14(sK20)) ),
inference(superposition,[status(thm)],[c_6264,c_6268]) ).
tcf(c_7147,plain,
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| ~ sP0(sK20) ),
inference(superposition,[status(thm)],[c_6264,c_4130]) ).
tcf(c_7240,plain,
! [X0: $i] :
( h_true_only(sK12,sK19(sK12))
| g_true_only(sK12,sK18(sK12))
| ~ iPr_def_11
| ~ g_both(sK12,X0)
| ~ h_both(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_6270]) ).
tcf(c_7291,plain,
( h_true_only(sK12,sK19(sK12))
| g_true_only(sK12,sK18(sK12))
| ~ iPr_def_11
| ~ g_both(sK12,sK13)
| ~ h_both(sK12,sK4(sK12,sK13)) ),
inference(instantiation,[status(thm)],[c_7240]) ).
tcf(c_7460,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| h_true_only(sK20,sK14(sK20))
| g_false(sK20,X0) ),
inference(global_subsumption_just,[status(thm)],[c_7098,c_6261,c_6269,c_6950,c_6967,c_6966,c_7066,c_7098,c_7115,c_7147]) ).
tcf(c_7461,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| g_false(sK20,X0)
| h_true_only(sK20,sK14(sK20)) ),
inference(renaming,[status(thm)],[c_7460]) ).
tcf(c_7476,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| g_false(sK20,X0)
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_7461,c_6263]) ).
tcf(c_7500,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| g_false(sK20,X0) ),
inference(global_subsumption_just,[status(thm)],[c_7130,c_6261,c_7476]) ).
tcf(c_7721,plain,
! [X0: $i] :
( ~ sP0(X0)
| ~ g_false(X0,sK16(X0)) ),
inference(superposition,[status(thm)],[c_7076,c_75]) ).
tcf(c_8095,plain,
( iPr_def_12
| iPr_def_11
| sP1
| sP2
| sP0(sK20) ),
inference(superposition,[status(thm)],[c_7500,c_7683]) ).
tcf(c_8096,plain,
( iPr_def_11
| sP1
| sP2
| sP3
| sP0(sK20)
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_6857,c_7683]) ).
tcf(c_8156,plain,
( iPr_def_11
| sP1
| sP2
| sP0(sK20) ),
inference(global_subsumption_just,[status(thm)],[c_7722,c_6261,c_6967,c_6966,c_7066,c_7115,c_7683,c_8095,c_8096]) ).
tcf(c_8519,plain,
! [X0: $i] :
( h_true_only(sK12,sK19(sK12))
| g_true_only(sK12,sK18(sK12))
| ~ iPr_def_11
| ~ g_both(sK12,X0)
| ~ h_both(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_6270]) ).
tcf(c_8720,plain,
! [X0: $i] : ~ sP0(X0),
inference(forward_subsumption_resolution,[status(thm)],[c_7721,c_4142]) ).
tcf(c_8721,plain,
( iPr_def_11
| sP1
| sP2 ),
inference(backward_subsumption_resolution,[status(thm)],[c_8156,c_8720]) ).
tcf(c_9860,plain,
! [X0: $i] :
( h_true_only(sK10,sK19(sK10))
| g_true_only(sK10,sK18(sK10))
| ~ iPr_def_11
| ~ g_both(sK10,X0)
| ~ h_both(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_6270]) ).
tcf(c_10000,plain,
( iPr_def_11
| sP2 ),
inference(backward_subsumption_resolution,[status(thm)],[c_8721,c_9999]) ).
tcf(c_11246,plain,
( h_true_only(sK10,sK19(sK10))
| g_true_only(sK10,sK18(sK10))
| ~ iPr_def_11
| ~ g_both(sK10,sK11)
| ~ h_both(sK10,sK17(sK10)) ),
inference(instantiation,[status(thm)],[c_9860]) ).
tcf(c_11402,plain,
( h_true_only(sK12,sK19(sK12))
| g_true_only(sK12,sK18(sK12))
| ~ iPr_def_11
| ~ g_both(sK12,sK13)
| ~ h_both(sK12,sK17(sK12)) ),
inference(instantiation,[status(thm)],[c_8519]) ).
tcf(c_11464,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_11431,c_11402,c_11336,c_11246,c_10891,c_10590,c_10504,c_10493,c_10447,c_10000,c_9841,c_9842,c_9802,c_9803,c_9750,c_9751,c_9681,c_9604,c_9492,c_9365,c_8846,c_8847,c_8706,c_8667,c_8668,c_8655,c_8656,c_8525,c_8473,c_8278,c_8204,c_8205,c_8140,c_7989,c_7990,c_7764,c_7518,c_7519,c_7457,c_7458,c_7385,c_7386,c_7340,c_7293,c_7294,c_7291,c_7290,c_6631,c_6632,c_6614,c_6589,c_6590,c_6570,c_6571,c_6567,c_6560,c_6519,c_6520,c_6495,c_6476,c_6477,c_6482,c_6467,c_6468,c_6458,c_6417,c_6418,c_6385,c_6386,c_6381,c_6382,c_6378,c_6379,c_6376,c_6358,c_6350,c_6334,c_6329,c_6324,c_6315,c_6305,c_6298,c_6291,c_6290,c_6289,c_6286,c_6287,c_6285,c_6284,c_6272,c_63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO606+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/5.38 % Computer : n014.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Fri Sep 25 03:13:52 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/5.42 Running first-order theorem proving
% 0.14/5.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.43
% 0.14/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.43
% 0.14/5.44 % Detected problem language: tptp
% 0.14/5.45 % Proving...
% 4.39/6.30 % SZS status Started for theBenchmark.p
% 4.39/6.30 % SZS status Theorem for theBenchmark.p
% 4.39/6.30
% 4.39/6.30 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.39/6.30
% 4.39/6.30 % ------ iProver source info
% 4.39/6.30
% 4.39/6.30 % git: date: 2026-07-19 20:42:38 +0200
% 4.39/6.30 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.39/6.30 % git: non_committed_changes: false
% 4.39/6.30
% 4.39/6.30 % ------ Parsing...
% 4.39/6.30 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.39/6.30
% 4.39/6.30 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 4.39/6.30
% 4.39/6.30 % ------ Preprocessing... gs_s sp: 8 0s gs_e snvd_s sp: 0 0s snvd_e
% 4.39/6.30 % ------ Proving...
% 4.39/6.30 % ------ Problem Properties
% 4.39/6.30
% 4.39/6.30 %
% 4.39/6.30 % clauses 40
% 4.39/6.30 % conjectures 10
% 4.39/6.30 % EPR 29
% 4.39/6.30 % Horn 23
% 4.39/6.30 % unary 0
% 4.39/6.30 % binary 22
% 4.39/6.30 % lits 116
% 4.39/6.30 % lits eq 0
% 4.39/6.30 % fd_pure 0
% 4.39/6.30 % fd_pseudo 0
% 4.39/6.30 % fd_cond 0
% 4.39/6.30 % fd_pseudo_cond 0
% 4.39/6.30 % AC symbols 0
% 4.39/6.30
% 4.39/6.30 % ------ Schedule dynamic 5 is on
% 4.39/6.30
% 4.39/6.30 % ------ no equalities: superposition off
% 4.39/6.30
% 4.39/6.30 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 4.39/6.30
% 4.39/6.30
% 4.39/6.30 % ------
% 4.39/6.30 % Current options:
% 4.39/6.30 % ------
% 4.39/6.30
% 4.39/6.30
% 4.39/6.30 %
% 4.39/6.30
% 4.39/6.30 % ------ Proving...
% 4.39/6.30 %
% 4.39/6.30
% 4.39/6.30 % SZS status Theorem for theBenchmark.p
% 4.39/6.30
% 4.39/6.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.39/6.31
% 4.39/6.31
%------------------------------------------------------------------------------