%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYO605+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 : n011.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 10.93s 27.38s
% Output : CNFRefutation 10.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 9
% Syntax : Number of formulae : 400 ( 25 unt; 4 def)
% Number of atoms : 1652 ( 0 equ)
% Maximal formula atoms : 57 ( 4 avg)
% Number of connectives : 1694 ( 563 ~; 921 |; 207 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 12 usr; 6 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-1 aty)
% Number of variables : 553 ( 0 sgn 482 !; 71 ?; 332 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ( ~ ? [X1] :
! [X0] :
? [X2] :
( ( ( g_both(X2,X1)
| g_false_only(X2,X1) )
& g_false_only(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_false_only(X2,X1) )
& g_both(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_both(X2,X1) )
& g_true_only(X2,X0) ) )
& ? [X1] :
( ~ ? [X0] :
! [X2] :
( ( g_true_only(X2,X1)
& g_false_only(X2,X0) )
| ( g_false_only(X2,X1)
& g_true_only(X2,X0) ) )
& ? [X0] :
( ~ ? [X2] :
( ( ( g_both(X2,X1)
| g_false_only(X2,X1) )
& g_false_only(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_false_only(X2,X1) )
& g_both(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_both(X2,X1) )
& g_true_only(X2,X0) ) )
& ? [X2] :
( g_both(X2,X1)
& g_both(X2,X0) ) ) )
& ~ ? [X0] :
! [X1] :
( ( g_false_only(X1,X1)
& g_false_only(X1,X0) )
| ( g_true_only(X1,X1)
& g_true_only(X1,X0) ) )
& ? [X0] :
( ~ ? [X1] :
( ( ( g_both(X1,X1)
| g_true_only(X1,X1) )
& g_false_only(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_true_only(X1,X1) )
& g_both(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_both(X1,X1) )
& g_true_only(X1,X0) ) )
& ? [X1] :
( g_both(X1,X1)
& g_both(X1,X0) ) ) )
| ? [X1] :
! [X0] :
? [X2] :
( ( ( g_both(X2,X1)
| g_false_only(X2,X1) )
& g_false_only(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_false_only(X2,X1) )
& g_both(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_both(X2,X1) )
& g_true_only(X2,X0) ) )
| ! [X0] :
? [X1] :
( ( ( g_both(X1,X1)
| g_true_only(X1,X1) )
& g_false_only(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_true_only(X1,X1) )
& g_both(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_both(X1,X1) )
& g_true_only(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nc4) ).
fof(f2,negated_conjecture,
~ ( ( ~ ? [X1] :
! [X0] :
? [X2] :
( ( ( g_both(X2,X1)
| g_false_only(X2,X1) )
& g_false_only(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_false_only(X2,X1) )
& g_both(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_both(X2,X1) )
& g_true_only(X2,X0) ) )
& ? [X1] :
( ~ ? [X0] :
! [X2] :
( ( g_true_only(X2,X1)
& g_false_only(X2,X0) )
| ( g_false_only(X2,X1)
& g_true_only(X2,X0) ) )
& ? [X0] :
( ~ ? [X2] :
( ( ( g_both(X2,X1)
| g_false_only(X2,X1) )
& g_false_only(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_false_only(X2,X1) )
& g_both(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_both(X2,X1) )
& g_true_only(X2,X0) ) )
& ? [X2] :
( g_both(X2,X1)
& g_both(X2,X0) ) ) )
& ~ ? [X0] :
! [X1] :
( ( g_false_only(X1,X1)
& g_false_only(X1,X0) )
| ( g_true_only(X1,X1)
& g_true_only(X1,X0) ) )
& ? [X0] :
( ~ ? [X1] :
( ( ( g_both(X1,X1)
| g_true_only(X1,X1) )
& g_false_only(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_true_only(X1,X1) )
& g_both(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_both(X1,X1) )
& g_true_only(X1,X0) ) )
& ? [X1] :
( g_both(X1,X1)
& g_both(X1,X0) ) ) )
| ? [X1] :
! [X0] :
? [X2] :
( ( ( g_both(X2,X1)
| g_false_only(X2,X1) )
& g_false_only(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_false_only(X2,X1) )
& g_both(X2,X0) )
| ( ( g_true_only(X2,X1)
| g_both(X2,X1) )
& g_true_only(X2,X0) ) )
| ! [X0] :
? [X1] :
( ( ( g_both(X1,X1)
| g_true_only(X1,X1) )
& g_false_only(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_true_only(X1,X1) )
& g_both(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_both(X1,X1) )
& g_true_only(X1,X0) ) ) ),
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,plain,
~ ( ( ~ ? [X16] :
! [X17] :
? [X18] :
( ( ( g_both(X18,X16)
| g_false_only(X18,X16) )
& g_false_only(X18,X17) )
| ( ( g_true_only(X18,X16)
| g_false_only(X18,X16) )
& g_both(X18,X17) )
| ( ( g_true_only(X18,X16)
| g_both(X18,X16) )
& g_true_only(X18,X17) ) )
& ? [X10] :
( ~ ? [X14] :
! [X15] :
( ( g_true_only(X15,X10)
& g_false_only(X15,X14) )
| ( g_false_only(X15,X10)
& g_true_only(X15,X14) ) )
& ? [X11] :
( ~ ? [X13] :
( ( ( g_both(X13,X10)
| g_false_only(X13,X10) )
& g_false_only(X13,X11) )
| ( ( g_true_only(X13,X10)
| g_false_only(X13,X10) )
& g_both(X13,X11) )
| ( ( g_true_only(X13,X10)
| g_both(X13,X10) )
& g_true_only(X13,X11) ) )
& ? [X12] :
( g_both(X12,X10)
& g_both(X12,X11) ) ) )
& ~ ? [X8] :
! [X9] :
( ( g_false_only(X9,X9)
& g_false_only(X9,X8) )
| ( g_true_only(X9,X9)
& g_true_only(X9,X8) ) )
& ? [X5] :
( ~ ? [X7] :
( ( ( g_both(X7,X7)
| g_true_only(X7,X7) )
& g_false_only(X7,X5) )
| ( ( g_false_only(X7,X7)
| g_true_only(X7,X7) )
& g_both(X7,X5) )
| ( ( g_false_only(X7,X7)
| g_both(X7,X7) )
& g_true_only(X7,X5) ) )
& ? [X6] :
( g_both(X6,X6)
& g_both(X6,X5) ) ) )
| ? [X2] :
! [X3] :
? [X4] :
( ( ( g_both(X4,X2)
| g_false_only(X4,X2) )
& g_false_only(X4,X3) )
| ( ( g_true_only(X4,X2)
| g_false_only(X4,X2) )
& g_both(X4,X3) )
| ( ( g_true_only(X4,X2)
| g_both(X4,X2) )
& g_true_only(X4,X3) ) )
| ! [X0] :
? [X1] :
( ( ( g_both(X1,X1)
| g_true_only(X1,X1) )
& g_false_only(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_true_only(X1,X1) )
& g_both(X1,X0) )
| ( ( g_false_only(X1,X1)
| g_both(X1,X1) )
& g_true_only(X1,X0) ) ) ),
inference(rectify,[],[f2]) ).
fof(f8,plain,
( ( ? [X16] :
! [X17] :
? [X18] :
( ( ( g_both(X18,X16)
| g_false_only(X18,X16) )
& g_false_only(X18,X17) )
| ( ( g_true_only(X18,X16)
| g_false_only(X18,X16) )
& g_both(X18,X17) )
| ( ( g_true_only(X18,X16)
| g_both(X18,X16) )
& g_true_only(X18,X17) ) )
| ! [X10] :
( ? [X14] :
! [X15] :
( ( g_true_only(X15,X10)
& g_false_only(X15,X14) )
| ( g_false_only(X15,X10)
& g_true_only(X15,X14) ) )
| ! [X11] :
( ? [X13] :
( ( ( g_both(X13,X10)
| g_false_only(X13,X10) )
& g_false_only(X13,X11) )
| ( ( g_true_only(X13,X10)
| g_false_only(X13,X10) )
& g_both(X13,X11) )
| ( ( g_true_only(X13,X10)
| g_both(X13,X10) )
& g_true_only(X13,X11) ) )
| ! [X12] :
( ~ g_both(X12,X10)
| ~ g_both(X12,X11) ) ) )
| ? [X8] :
! [X9] :
( ( g_false_only(X9,X9)
& g_false_only(X9,X8) )
| ( g_true_only(X9,X9)
& g_true_only(X9,X8) ) )
| ! [X5] :
( ? [X7] :
( ( ( g_both(X7,X7)
| g_true_only(X7,X7) )
& g_false_only(X7,X5) )
| ( ( g_false_only(X7,X7)
| g_true_only(X7,X7) )
& g_both(X7,X5) )
| ( ( g_false_only(X7,X7)
| g_both(X7,X7) )
& g_true_only(X7,X5) ) )
| ! [X6] :
( ~ g_both(X6,X6)
| ~ g_both(X6,X5) ) ) )
& ! [X2] :
? [X3] :
! [X4] :
( ( ( ~ g_both(X4,X2)
& ~ g_false_only(X4,X2) )
| ~ g_false_only(X4,X3) )
& ( ( ~ g_true_only(X4,X2)
& ~ g_false_only(X4,X2) )
| ~ g_both(X4,X3) )
& ( ( ~ g_true_only(X4,X2)
& ~ g_both(X4,X2) )
| ~ g_true_only(X4,X3) ) )
& ? [X0] :
! [X1] :
( ( ( ~ g_both(X1,X1)
& ~ g_true_only(X1,X1) )
| ~ g_false_only(X1,X0) )
& ( ( ~ g_false_only(X1,X1)
& ~ g_true_only(X1,X1) )
| ~ g_both(X1,X0) )
& ( ( ~ g_false_only(X1,X1)
& ~ g_both(X1,X1) )
| ~ g_true_only(X1,X0) ) ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f14,plain,
( ~ sP3
| ! [X10] :
( ? [X14] :
! [X15] :
( ( g_true_only(X15,X10)
& g_false_only(X15,X14) )
| ( g_false_only(X15,X10)
& g_true_only(X15,X14) ) )
| sP0(X10) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f15,plain,
( ~ sP3
| ! [X0] :
( ? [X1] :
! [X2] :
( ( g_true_only(X2,X0)
& g_false_only(X2,X1) )
| ( g_false_only(X2,X0)
& g_true_only(X2,X1) ) )
| sP0(X0) ) ),
inference(rectify,[],[f14]) ).
fof(f16,plain,
( ~ sP3
| ! [X0] :
( ! [X2] :
( ( g_true_only(X2,X0)
& g_false_only(X2,sK4(X0)) )
| ( g_false_only(X2,X0)
& g_true_only(X2,sK4(X0)) ) )
| sP0(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X1,sK4(X0))],[f15]) ).
fof(f17,plain,
( ~ sP2
| ! [X5] :
( ? [X7] :
( ( ( g_both(X7,X7)
| g_true_only(X7,X7) )
& g_false_only(X7,X5) )
| ( ( g_false_only(X7,X7)
| g_true_only(X7,X7) )
& g_both(X7,X5) )
| ( ( g_false_only(X7,X7)
| g_both(X7,X7) )
& g_true_only(X7,X5) ) )
| ! [X6] :
( ~ g_both(X6,X6)
| ~ g_both(X6,X5) ) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f18,plain,
( ~ sP2
| ! [X0] :
( ? [X2] :
( ( ( g_both(X2,X2)
| g_true_only(X2,X2) )
& g_false_only(X2,X0) )
| ( ( g_false_only(X2,X2)
| g_true_only(X2,X2) )
& g_both(X2,X0) )
| ( ( g_false_only(X2,X2)
| g_both(X2,X2) )
& g_true_only(X2,X0) ) )
| ! [X1] :
( ~ g_both(X1,X1)
| ~ g_both(X1,X0) ) ) ),
inference(rectify,[],[f17]) ).
fof(f19,plain,
( ~ sP2
| ! [X0] :
( ( ( g_both(sK5(X0),sK5(X0))
| g_true_only(sK5(X0),sK5(X0)) )
& g_false_only(sK5(X0),X0) )
| ( ( g_false_only(sK5(X0),sK5(X0))
| g_true_only(sK5(X0),sK5(X0)) )
& g_both(sK5(X0),X0) )
| ( ( g_false_only(sK5(X0),sK5(X0))
| g_both(sK5(X0),sK5(X0)) )
& g_true_only(sK5(X0),X0) )
| ! [X1] :
( ~ g_both(X1,X1)
| ~ g_both(X1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X2,sK5(X0))],[f18]) ).
fof(f20,plain,
( ~ sP1
| ? [X16] :
! [X17] :
? [X18] :
( ( ( g_both(X18,X16)
| g_false_only(X18,X16) )
& g_false_only(X18,X17) )
| ( ( g_true_only(X18,X16)
| g_false_only(X18,X16) )
& g_both(X18,X17) )
| ( ( g_true_only(X18,X16)
| g_both(X18,X16) )
& g_true_only(X18,X17) ) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f21,plain,
( ~ sP1
| ? [X0] :
! [X1] :
? [X2] :
( ( ( g_both(X2,X0)
| g_false_only(X2,X0) )
& g_false_only(X2,X1) )
| ( ( g_true_only(X2,X0)
| g_false_only(X2,X0) )
& g_both(X2,X1) )
| ( ( g_true_only(X2,X0)
| g_both(X2,X0) )
& g_true_only(X2,X1) ) ) ),
inference(rectify,[],[f20]) ).
fof(f22,plain,
( ~ sP1
| ! [X1] :
( ( ( g_both(sK7(X1),sK6)
| g_false_only(sK7(X1),sK6) )
& g_false_only(sK7(X1),X1) )
| ( ( g_true_only(sK7(X1),sK6)
| g_false_only(sK7(X1),sK6) )
& g_both(sK7(X1),X1) )
| ( ( g_true_only(sK7(X1),sK6)
| g_both(sK7(X1),sK6) )
& g_true_only(sK7(X1),X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X0,sK6),skolemize(X2,sK7(X1))],[f21]) ).
fof(f26,plain,
( ( sP1
| sP3
| ? [X5] :
! [X6] :
( ( g_false_only(X6,X6)
& g_false_only(X6,X5) )
| ( g_true_only(X6,X6)
& g_true_only(X6,X5) ) )
| sP2 )
& ! [X2] :
? [X3] :
! [X4] :
( ( ( ~ g_both(X4,X2)
& ~ g_false_only(X4,X2) )
| ~ g_false_only(X4,X3) )
& ( ( ~ g_true_only(X4,X2)
& ~ g_false_only(X4,X2) )
| ~ g_both(X4,X3) )
& ( ( ~ g_true_only(X4,X2)
& ~ g_both(X4,X2) )
| ~ g_true_only(X4,X3) ) )
& ? [X0] :
! [X1] :
( ( ( ~ g_both(X1,X1)
& ~ g_true_only(X1,X1) )
| ~ g_false_only(X1,X0) )
& ( ( ~ g_false_only(X1,X1)
& ~ g_true_only(X1,X1) )
| ~ g_both(X1,X0) )
& ( ( ~ g_false_only(X1,X1)
& ~ g_both(X1,X1) )
| ~ g_true_only(X1,X0) ) ) ),
inference(rectify,[],[f13]) ).
fof(f27,plain,
( ( sP1
| sP3
| ! [X6] :
( ( g_false_only(X6,X6)
& g_false_only(X6,sK11) )
| ( g_true_only(X6,X6)
& g_true_only(X6,sK11) ) )
| sP2 )
& ! [X2,X4] :
( ( ( ~ g_both(X4,X2)
& ~ g_false_only(X4,X2) )
| ~ g_false_only(X4,sK10(X2)) )
& ( ( ~ g_true_only(X4,X2)
& ~ g_false_only(X4,X2) )
| ~ g_both(X4,sK10(X2)) )
& ( ( ~ g_true_only(X4,X2)
& ~ g_both(X4,X2) )
| ~ g_true_only(X4,sK10(X2)) ) )
& ! [X1] :
( ( ( ~ g_both(X1,X1)
& ~ g_true_only(X1,X1) )
| ~ g_false_only(X1,sK9) )
& ( ( ~ g_false_only(X1,X1)
& ~ g_true_only(X1,X1) )
| ~ g_both(X1,sK9) )
& ( ( ~ g_false_only(X1,X1)
& ~ g_both(X1,X1) )
| ~ g_true_only(X1,sK9) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X0,sK9),skolemize(X3,sK10(X2)),skolemize(X5,sK11)],[f26]) ).
fof(f28,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(f29,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,[],[f28]) ).
fof(f30,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(f31,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,[],[f30]) ).
fof(f32,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(f33,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,[],[f32]) ).
fof(f34,plain,
! [X2,X0] :
( ~ sP3
| g_true_only(X2,X0)
| g_false_only(X2,X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f16]) ).
fof(f41,plain,
! [X0,X1] :
( ~ sP2
| g_false_only(sK5(X0),X0)
| g_both(sK5(X0),X0)
| g_false_only(sK5(X0),sK5(X0))
| g_both(sK5(X0),sK5(X0))
| ~ g_both(X1,X1)
| ~ g_both(X1,X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f43,plain,
! [X0,X1] :
( ~ sP2
| g_false_only(sK5(X0),X0)
| g_false_only(sK5(X0),sK5(X0))
| g_true_only(sK5(X0),sK5(X0))
| g_true_only(sK5(X0),X0)
| ~ g_both(X1,X1)
| ~ g_both(X1,X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f44,plain,
! [X0,X1] :
( ~ sP2
| g_both(sK5(X0),sK5(X0))
| g_true_only(sK5(X0),sK5(X0))
| g_both(sK5(X0),X0)
| g_true_only(sK5(X0),X0)
| ~ g_both(X1,X1)
| ~ g_both(X1,X0) ),
inference(cnf_transformation,[],[f19]) ).
fof(f49,plain,
! [X1] :
( ~ sP1
| g_false_only(sK7(X1),X1)
| g_both(sK7(X1),X1)
| g_true_only(sK7(X1),sK6)
| g_both(sK7(X1),sK6) ),
inference(cnf_transformation,[],[f22]) ).
fof(f51,plain,
! [X1] :
( ~ sP1
| g_false_only(sK7(X1),X1)
| g_true_only(sK7(X1),sK6)
| g_false_only(sK7(X1),sK6)
| g_true_only(sK7(X1),X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f52,plain,
! [X1] :
( ~ sP1
| g_both(sK7(X1),sK6)
| g_false_only(sK7(X1),sK6)
| g_both(sK7(X1),X1)
| g_true_only(sK7(X1),X1) ),
inference(cnf_transformation,[],[f22]) ).
fof(f62,plain,
! [X6] :
( sP1
| sP3
| g_false_only(X6,X6)
| g_true_only(X6,X6)
| sP2 ),
inference(cnf_transformation,[],[f27]) ).
fof(f63,plain,
! [X6] :
( sP1
| sP3
| g_false_only(X6,sK11)
| g_true_only(X6,X6)
| sP2 ),
inference(cnf_transformation,[],[f27]) ).
fof(f66,plain,
! [X2,X4] :
( ~ g_both(X4,X2)
| ~ g_false_only(X4,sK10(X2)) ),
inference(cnf_transformation,[],[f27]) ).
fof(f67,plain,
! [X2,X4] :
( ~ g_false_only(X4,X2)
| ~ g_false_only(X4,sK10(X2)) ),
inference(cnf_transformation,[],[f27]) ).
fof(f68,plain,
! [X2,X4] :
( ~ g_true_only(X4,X2)
| ~ g_both(X4,sK10(X2)) ),
inference(cnf_transformation,[],[f27]) ).
fof(f69,plain,
! [X2,X4] :
( ~ g_false_only(X4,X2)
| ~ g_both(X4,sK10(X2)) ),
inference(cnf_transformation,[],[f27]) ).
fof(f70,plain,
! [X2,X4] :
( ~ g_true_only(X4,X2)
| ~ g_true_only(X4,sK10(X2)) ),
inference(cnf_transformation,[],[f27]) ).
fof(f71,plain,
! [X2,X4] :
( ~ g_both(X4,X2)
| ~ g_true_only(X4,sK10(X2)) ),
inference(cnf_transformation,[],[f27]) ).
fof(f72,plain,
! [X1] :
( ~ g_both(X1,X1)
| ~ g_false_only(X1,sK9) ),
inference(cnf_transformation,[],[f27]) ).
fof(f73,plain,
! [X1] :
( ~ g_true_only(X1,X1)
| ~ g_false_only(X1,sK9) ),
inference(cnf_transformation,[],[f27]) ).
fof(f74,plain,
! [X1] :
( ~ g_false_only(X1,X1)
| ~ g_both(X1,sK9) ),
inference(cnf_transformation,[],[f27]) ).
fof(f75,plain,
! [X1] :
( ~ g_true_only(X1,X1)
| ~ g_both(X1,sK9) ),
inference(cnf_transformation,[],[f27]) ).
fof(f76,plain,
! [X1] :
( ~ g_false_only(X1,X1)
| ~ g_true_only(X1,sK9) ),
inference(cnf_transformation,[],[f27]) ).
fof(f77,plain,
! [X1] :
( ~ g_both(X1,X1)
| ~ g_true_only(X1,sK9) ),
inference(cnf_transformation,[],[f27]) ).
fof(f78,plain,
! [X0,X1] :
( g_false_only(X0,X1)
| g_both(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
fof(f79,plain,
! [X0,X1] :
( ~ g_true_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f80,plain,
! [X0,X1] :
( ~ g_true_only(X0,X1)
| g_true(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f81,plain,
! [X0,X1] :
( g_false(X0,X1)
| ~ g_true(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f82,plain,
! [X0,X1] :
( ~ g_both(X0,X1)
| g_false(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
fof(f83,plain,
! [X0,X1] :
( ~ g_both(X0,X1)
| g_true(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
fof(f84,plain,
! [X0,X1] :
( ~ g_false(X0,X1)
| ~ g_true(X0,X1)
| g_both(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
fof(f85,plain,
! [X0,X1] :
( ~ g_false_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f86,plain,
! [X0,X1] :
( ~ g_false_only(X0,X1)
| g_false(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f87,plain,
! [X0,X1] :
( g_true(X0,X1)
| ~ g_false(X0,X1)
| g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| g_false_only(X0,X1)
| g_true_only(X0,X1)
| ~ sP3 ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( g_both(sK5(X1),X1)
| g_true_only(sK5(X1),X1)
| g_both(sK5(X1),sK5(X1))
| g_true_only(sK5(X1),sK5(X1))
| ~ sP2
| ~ g_both(X0,X1)
| ~ g_both(X0,X0) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i] :
( g_false_only(sK5(X1),X1)
| g_true_only(sK5(X1),X1)
| g_false_only(sK5(X1),sK5(X1))
| g_true_only(sK5(X1),sK5(X1))
| ~ sP2
| ~ g_both(X0,X1)
| ~ g_both(X0,X0) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( g_both(sK5(X1),X1)
| g_false_only(sK5(X1),X1)
| g_both(sK5(X1),sK5(X1))
| g_false_only(sK5(X1),sK5(X1))
| ~ sP2
| ~ g_both(X0,X1)
| ~ g_both(X0,X0) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_62,plain,
! [X0: $i] :
( g_both(sK7(X0),sK6)
| g_false_only(sK7(X0),sK6)
| g_both(sK7(X0),X0)
| g_true_only(sK7(X0),X0)
| ~ sP1 ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_63,plain,
! [X0: $i] :
( g_false_only(sK7(X0),sK6)
| g_true_only(sK7(X0),sK6)
| g_false_only(sK7(X0),X0)
| g_true_only(sK7(X0),X0)
| ~ sP1 ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_65,plain,
! [X0: $i] :
( g_both(sK7(X0),sK6)
| g_true_only(sK7(X0),sK6)
| g_both(sK7(X0),X0)
| g_false_only(sK7(X0),X0)
| ~ sP1 ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_77,negated_conjecture,
! [X0: $i] :
( ~ g_true_only(X0,sK9)
| ~ g_both(X0,X0) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_78,negated_conjecture,
! [X0: $i] :
( ~ g_true_only(X0,sK9)
| ~ g_false_only(X0,X0) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_79,negated_conjecture,
! [X0: $i] :
( ~ g_both(X0,sK9)
| ~ g_true_only(X0,X0) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_80,negated_conjecture,
! [X0: $i] :
( ~ g_both(X0,sK9)
| ~ g_false_only(X0,X0) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_81,negated_conjecture,
! [X0: $i] :
( ~ g_false_only(X0,sK9)
| ~ g_true_only(X0,X0) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_82,negated_conjecture,
! [X0: $i] :
( ~ g_false_only(X0,sK9)
| ~ g_both(X0,X0) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_83,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ g_both(X0,X1)
| ~ g_true_only(X0,sK10(X1)) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_84,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ g_true_only(X0,X1)
| ~ g_true_only(X0,sK10(X1)) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_85,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ g_false_only(X0,X1)
| ~ g_both(X0,sK10(X1)) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_86,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ g_true_only(X0,X1)
| ~ g_both(X0,sK10(X1)) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_87,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ g_false_only(X0,X1)
| ~ g_false_only(X0,sK10(X1)) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_88,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ g_both(X0,X1)
| ~ g_false_only(X0,sK10(X1)) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_91,negated_conjecture,
! [X0: $i] :
( sP1
| sP2
| sP3
| g_false_only(X0,sK11)
| g_true_only(X0,X0) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_92,negated_conjecture,
! [X0: $i] :
( sP1
| sP2
| sP3
| g_false_only(X0,X0)
| g_true_only(X0,X0) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_false_only(X0,X1)
| g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| g_true_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i] :
( ~ g_false(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| ~ g_false(X0,X1)
| ~ g_true(X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_false_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i] :
( ~ g_true(X0,X1)
| ~ g_false_only(X0,X1) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_false_only(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_100,c_98,c_95,c_93]) ).
tcf(c_148,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| g_true_only(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_94,c_101,c_98,c_95,c_93,c_94]) ).
tcf(c_169,plain,
! [X0: $i,X1: $i] :
( ~ g_true_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_96]) ).
tcf(c_170,plain,
! [X0: $i,X1: $i] :
( ~ g_false(X0,X1)
| ~ g_true_only(X0,X1) ),
inference(renaming,[status(thm)],[c_169]) ).
tcf(c_173,plain,
! [X0: $i,X1: $i] :
( ~ g_false_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_102]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i] :
( ~ g_true(X0,X1)
| ~ g_false_only(X0,X1) ),
inference(renaming,[status(thm)],[c_173]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_both(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_98]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ g_true_only(X0,sK10(X1)) ),
inference(prop_impl_just,[status(thm)],[c_84,c_148]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_both(X0,sK10(X1)) ),
inference(prop_impl_just,[status(thm)],[c_98,c_95,c_85,c_93]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ g_both(X0,sK10(X1)) ),
inference(prop_impl_just,[status(thm)],[c_101,c_98,c_95,c_86,c_93,c_94]) ).
tcf(c_219,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_false_only(X0,sK10(X1)) ),
inference(prop_impl_just,[status(thm)],[c_87,c_145]) ).
tcf(c_227,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| g_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_101,c_98,c_95,c_93,c_94]) ).
tcf(c_295,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| ~ sP3
| ~ g_false(X0,X1)
| ~ g_true(X0,X1) ),
inference(bin_hyper_res,[status(thm)],[c_52,c_174,c_170]) ).
tcf(c_767,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| ~ sP3
| ~ g_false(X0,X1)
| ~ g_both(X0,X1) ),
inference(resolution,[status(thm)],[c_181,c_295]) ).
tcf(c_769,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| ~ sP3
| ~ g_both(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_767,c_99,c_767]) ).
tcf(c_4081,plain,
! [X0: $i,X1: $i] :
( g_true_only(X0,X1)
| g_false(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_148]) ).
tcf(c_4082,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| g_true_only(X0,X1) ),
inference(renaming,[status(thm)],[c_4081]) ).
tcf(c_4085,plain,
! [X0: $i,X1: $i] :
( g_false_only(X0,X1)
| g_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_145]) ).
tcf(c_4086,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_false_only(X0,X1) ),
inference(renaming,[status(thm)],[c_4085]) ).
tcf(c_4121,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ g_true_only(X0,sK10(X1)) ),
inference(prop_impl_just,[status(thm)],[c_211]) ).
tcf(c_4123,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_both(X0,sK10(X1)) ),
inference(prop_impl_just,[status(thm)],[c_213]) ).
tcf(c_4125,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| ~ g_both(X0,sK10(X1)) ),
inference(prop_impl_just,[status(thm)],[c_215]) ).
tcf(c_4129,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_false_only(X0,sK10(X1)) ),
inference(prop_impl_just,[status(thm)],[c_219]) ).
tcf(c_4137,plain,
! [X0: $i,X1: $i] :
( g_false(X0,X1)
| g_true(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_227]) ).
tcf(c_6851,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| g_true_only(X0,X0)
| g_false_only(X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_92]) ).
tcf(c_6852,negated_conjecture,
( iPr_def_10
| sP1
| sP2
| sP3 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_92]) ).
tcf(c_6853,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| g_true_only(X0,X0)
| g_false_only(X0,sK11) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_91]) ).
tcf(c_6863,plain,
! [X0: $i] :
( g_true(X0,sK9)
| g_false_only(X0,sK9) ),
inference(instantiation,[status(thm)],[c_4086]) ).
tcf(c_6865,plain,
! [X0: $i,X1: $i] :
( g_true(X0,sK10(X1))
| g_false_only(X0,sK10(X1)) ),
inference(instantiation,[status(thm)],[c_4086]) ).
tcf(c_6867,plain,
! [X0: $i] :
( g_both(X0,sK9)
| ~ g_false(X0,sK9)
| ~ g_true(X0,sK9) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_6868,plain,
! [X0: $i] :
( ~ g_true(X0,sK9)
| ~ g_false_only(X0,sK9) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_6871,plain,
! [X0: $i,X1: $i] :
( g_both(X0,sK10(X1))
| ~ g_false(X0,sK10(X1))
| ~ g_true(X0,sK10(X1)) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_6876,plain,
! [X0: $i] :
( g_false(X0,sK9)
| g_true_only(X0,sK9) ),
inference(instantiation,[status(thm)],[c_4082]) ).
tcf(c_6878,plain,
! [X0: $i,X1: $i] :
( g_false(X0,sK10(X1))
| g_true_only(X0,sK10(X1)) ),
inference(instantiation,[status(thm)],[c_4082]) ).
tcf(c_6892,plain,
! [X0: $i] :
( g_false(sK10(X0),sK10(X0))
| g_true_only(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_6878]) ).
tcf(c_6908,plain,
! [X0: $i] :
( g_true(sK10(X0),sK9)
| g_false_only(sK10(X0),sK9) ),
inference(instantiation,[status(thm)],[c_6863]) ).
tcf(c_6922,plain,
! [X0: $i] :
( g_both(sK10(X0),sK9)
| ~ g_false(sK10(X0),sK9)
| ~ g_true(sK10(X0),sK9) ),
inference(instantiation,[status(thm)],[c_6867]) ).
tcf(c_6939,plain,
! [X0: $i] :
( g_true(sK10(X0),sK9)
| ~ g_both(sK10(X0),sK9) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_6952,plain,
! [X0: $i] :
( g_true(sK10(sK10(X0)),sK10(X0))
| g_false_only(sK10(sK10(X0)),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_6865]) ).
tcf(c_6999,plain,
! [X0: $i] :
( ~ g_false(sK7(X0),sK6)
| ~ g_true_only(sK7(X0),sK6) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_7005,plain,
! [X0: $i] :
( ~ g_both(sK7(sK10(X0)),X0)
| ~ g_true_only(sK7(sK10(X0)),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_7026,plain,
( ~ g_true(sK5(sK9),sK9)
| ~ g_false_only(sK5(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_6868]) ).
tcf(c_7027,plain,
( ~ g_false_only(sK5(sK9),sK9)
| ~ g_both(sK5(sK9),sK5(sK9)) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_7039,plain,
! [X0: $i] :
( ~ g_both(sK5(X0),sK9)
| ~ g_true_only(sK5(X0),sK5(X0)) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_7040,plain,
! [X0: $i] :
( ~ g_false_only(sK5(X0),sK9)
| ~ g_true_only(sK5(X0),sK5(X0)) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_7116,plain,
! [X0: $i] :
( g_false(sK7(X0),sK6)
| ~ g_both(sK7(X0),sK6) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_7199,plain,
! [X0: $i] :
( g_false(sK7(sK10(X0)),X0)
| g_true(sK7(sK10(X0)),X0) ),
inference(instantiation,[status(thm)],[c_4137]) ).
tcf(c_7200,plain,
! [X0: $i] :
( g_true(sK7(sK10(X0)),X0)
| ~ g_both(sK7(sK10(X0)),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_4123]) ).
tcf(c_7202,plain,
! [X0: $i] :
( g_true(sK7(sK10(X0)),X0)
| ~ g_both(sK7(sK10(X0)),X0) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_7203,plain,
( g_true(sK7(sK10(sK6)),sK6)
| ~ g_both(sK7(sK10(sK6)),sK6) ),
inference(instantiation,[status(thm)],[c_7202]) ).
tcf(c_7206,plain,
( g_false(sK7(sK10(sK6)),sK6)
| g_true(sK7(sK10(sK6)),sK6) ),
inference(instantiation,[status(thm)],[c_7199]) ).
tcf(c_7226,plain,
! [X0: $i] :
( g_true(sK10(sK10(sK10(X0))),sK10(sK10(X0)))
| g_false_only(sK10(sK10(sK10(X0))),sK10(sK10(X0))) ),
inference(instantiation,[status(thm)],[c_6952]) ).
tcf(c_7260,plain,
! [X0: $i] :
( g_true(sK10(X0),sK10(X0))
| g_false_only(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_6865]) ).
tcf(c_7351,plain,
( g_false(sK7(sK10(sK6)),sK6)
| ~ g_both(sK7(sK10(sK6)),sK6) ),
inference(instantiation,[status(thm)],[c_7116]) ).
tcf(c_7392,plain,
! [X0: $i] :
( g_both(sK5(X0),sK9)
| ~ g_false(sK5(X0),sK9)
| ~ g_true(sK5(X0),sK9) ),
inference(instantiation,[status(thm)],[c_6867]) ).
tcf(c_7422,plain,
! [X0: $i] :
( g_false(sK7(sK10(X0)),X0)
| ~ g_both(sK7(sK10(X0)),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_4125]) ).
tcf(c_7494,plain,
! [X0: $i] :
( g_both(sK10(X0),sK10(X0))
| ~ g_false(sK10(X0),sK10(X0))
| ~ g_true(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_6871]) ).
tcf(c_7715,plain,
! [X0: $i,X1: $i] :
( ~ g_false(sK8(X0,X1),X0)
| ~ g_true_only(sK8(X0,X1),X0) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_7824,plain,
! [X0: $i] :
( g_false(sK5(X0),X0)
| g_true(sK5(X0),X0) ),
inference(instantiation,[status(thm)],[c_4137]) ).
tcf(c_7827,plain,
! [X0: $i] :
( g_true(sK5(X0),X0)
| ~ g_both(sK5(X0),X0) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_7899,plain,
! [X0: $i] :
( ~ g_both(sK10(X0),X0)
| ~ g_false_only(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_7918,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| ~ iPr_def_11
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_6853,c_83]) ).
tcf(c_7927,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| ~ iPr_def_11
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_6853,c_83]) ).
tcf(c_7932,plain,
( g_true(sK5(sK9),sK9)
| g_false_only(sK5(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_6863]) ).
tcf(c_7948,plain,
! [X0: $i] :
( g_true_only(sK10(X0),sK10(X0))
| ~ iPr_def_10
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_6851,c_88]) ).
tcf(c_8067,plain,
! [X0: $i] :
( ~ g_true(sK7(sK10(X0)),X0)
| ~ g_false_only(sK7(sK10(X0)),X0) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_8068,plain,
( ~ g_true(sK7(sK10(sK6)),sK6)
| ~ g_false_only(sK7(sK10(sK6)),sK6) ),
inference(instantiation,[status(thm)],[c_8067]) ).
tcf(c_8177,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| ~ g_false_only(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_4129]) ).
tcf(c_8193,plain,
! [X0: $i] :
( g_false(sK10(X0),sK9)
| ~ g_both(sK10(X0),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_4125]) ).
tcf(c_8207,plain,
! [X0: $i] :
( ~ g_both(sK10(sK10(X0)),X0)
| ~ g_false_only(sK10(sK10(X0)),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_8266,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| g_false(sK10(X0),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_6853,c_4121]) ).
tcf(c_8275,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| g_false(sK10(X0),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_6853,c_4121]) ).
tcf(c_8340,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| g_true_only(sK10(X0),sK10(X0))
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_6851,c_4129]) ).
tcf(c_8354,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| g_true_only(sK10(X0),sK10(X0))
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_6851,c_4129]) ).
tcf(c_8791,plain,
( g_both(sK5(sK9),sK9)
| ~ g_false(sK5(sK9),sK9)
| ~ g_true(sK5(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_7392]) ).
tcf(c_8873,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_false_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(superposition,[status(thm)],[c_4086,c_97]) ).
tcf(c_8889,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_false_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(superposition,[status(thm)],[c_4086,c_97]) ).
tcf(c_9011,plain,
! [X0: $i,X1: $i] :
( g_false(sK8(X0,X1),X0)
| ~ g_true_only(sK8(X0,X1),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_4121]) ).
tcf(c_9012,plain,
! [X0: $i,X1: $i] :
( g_false(sK8(X0,X1),X0)
| g_true(sK8(X0,X1),X0) ),
inference(instantiation,[status(thm)],[c_4137]) ).
tcf(c_9013,plain,
! [X0: $i,X1: $i] :
( g_false(sK8(X0,X1),X0)
| ~ g_both(sK8(X0,X1),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_4125]) ).
tcf(c_9015,plain,
! [X0: $i,X1: $i] :
( g_false(sK8(X0,X1),X0)
| ~ g_both(sK8(X0,X1),X0) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_9021,plain,
! [X0: $i] :
( ~ g_false(sK8(sK9,X0),sK9)
| ~ g_true_only(sK8(sK9,X0),sK9) ),
inference(instantiation,[status(thm)],[c_7715]) ).
tcf(c_9192,plain,
! [X0: $i] :
( g_both(sK7(sK10(X0)),sK6)
| g_false_only(sK7(sK10(X0)),sK6)
| g_false(sK7(sK10(X0)),X0)
| g_both(sK7(sK10(X0)),sK10(X0))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_62,c_4121]) ).
tcf(c_9325,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| ~ g_both(sK10(X0),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_4123]) ).
tcf(c_9352,plain,
( g_true(sK5(sK9),sK9)
| ~ g_both(sK5(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_7827]) ).
tcf(c_9354,plain,
( g_false(sK5(sK9),sK9)
| g_true(sK5(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_7824]) ).
tcf(c_9395,plain,
( g_both(sK10(sK9),sK9)
| ~ g_false(sK10(sK9),sK9)
| ~ g_true(sK10(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_6922]) ).
tcf(c_9396,plain,
( ~ g_both(sK10(sK9),sK9)
| ~ g_false_only(sK10(sK9),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_7899]) ).
tcf(c_9531,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| g_true_only(sK10(X0),sK10(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_8340,c_6892,c_7260,c_7494,c_8177,c_9325]) ).
tcf(c_9539,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| ~ g_false_only(sK10(X0),sK9) ),
inference(superposition,[status(thm)],[c_9531,c_81]) ).
tcf(c_9540,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| ~ g_both(sK10(X0),sK9) ),
inference(superposition,[status(thm)],[c_9531,c_79]) ).
tcf(c_9558,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| g_true_only(sK10(X0),sK10(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_8354,c_9531]) ).
tcf(c_9565,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| ~ g_false_only(sK10(X0),sK9) ),
inference(superposition,[status(thm)],[c_9558,c_81]) ).
tcf(c_9777,plain,
! [X0: $i] :
( g_false_only(sK7(sK10(X0)),sK6)
| g_true_only(sK7(sK10(X0)),sK6)
| g_true_only(sK7(sK10(X0)),sK10(X0))
| ~ sP1
| ~ g_both(sK7(sK10(X0)),X0) ),
inference(superposition,[status(thm)],[c_63,c_88]) ).
tcf(c_10099,plain,
! [X0: $i] :
( g_both(sK7(sK10(X0)),sK6)
| g_true_only(sK7(sK10(X0)),sK6)
| g_true(sK7(sK10(X0)),X0)
| g_both(sK7(sK10(X0)),sK10(X0))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_65,c_4129]) ).
tcf(c_10208,plain,
! [X0: $i] :
( g_false(sK5(X0),X0)
| ~ g_both(sK5(X0),X0) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_10373,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ g_both(sK10(X0),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7948,c_83]) ).
tcf(c_10860,plain,
! [X0: $i] :
( ~ g_false(sK5(X0),X0)
| ~ g_true_only(sK5(X0),X0) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_11032,plain,
( ~ g_true_only(sK5(sK9),sK9)
| ~ g_false_only(sK5(sK9),sK5(sK9)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_11033,plain,
( ~ g_true_only(sK5(sK9),sK9)
| ~ g_both(sK5(sK9),sK5(sK9)) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_11150,plain,
( g_true(sK10(sK9),sK9)
| ~ g_both(sK10(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_6939]) ).
tcf(c_11182,plain,
( ~ g_false(sK5(sK9),sK9)
| ~ g_true_only(sK5(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_10860]) ).
tcf(c_11183,plain,
( g_false(sK5(sK9),sK9)
| g_true_only(sK5(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_6876]) ).
tcf(c_11552,plain,
! [X0: $i] :
( g_false_only(sK7(sK10(X0)),sK6)
| g_true_only(sK7(sK10(X0)),sK6)
| ~ g_both(sK7(sK10(X0)),X0)
| ~ sP1 ),
inference(global_subsumption_just,[status(thm)],[c_9777,c_7005,c_9777]) ).
tcf(c_11553,plain,
! [X0: $i] :
( g_false_only(sK7(sK10(X0)),sK6)
| g_true_only(sK7(sK10(X0)),sK6)
| ~ sP1
| ~ g_both(sK7(sK10(X0)),X0) ),
inference(renaming,[status(thm)],[c_11552]) ).
tcf(c_11554,plain,
( g_false_only(sK7(sK10(sK6)),sK6)
| g_true_only(sK7(sK10(sK6)),sK6)
| ~ sP1
| ~ g_both(sK7(sK10(sK6)),sK6) ),
inference(instantiation,[status(thm)],[c_11553]) ).
tcf(c_12219,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_false_only(X0,X1)
| g_true_only(X0,X1) ),
inference(superposition,[status(thm)],[c_4082,c_8889]) ).
tcf(c_12221,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| g_both(sK10(X0),X0)
| g_false_only(sK10(X0),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_8275,c_8889]) ).
tcf(c_12338,plain,
( g_true(sK10(sK10(sK10(sK9))),sK10(sK10(sK9)))
| g_false_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK9))) ),
inference(instantiation,[status(thm)],[c_7226]) ).
tcf(c_12345,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_false_only(X0,X1)
| g_true_only(X0,X1) ),
inference(superposition,[status(thm)],[c_4082,c_8873]) ).
tcf(c_12347,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| g_both(sK10(X0),X0)
| g_false_only(sK10(X0),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_8266,c_8873]) ).
tcf(c_12461,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_true_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(superposition,[status(thm)],[c_12219,c_102]) ).
tcf(c_12462,plain,
! [X0: $i] :
( g_both(X0,X0)
| g_true_only(X0,X0)
| ~ g_both(X0,sK9) ),
inference(superposition,[status(thm)],[c_12219,c_80]) ).
tcf(c_12464,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_both(X0,sK10(X1))
| g_true_only(X0,sK10(X1)) ),
inference(superposition,[status(thm)],[c_12219,c_4129]) ).
tcf(c_12465,plain,
! [X0: $i,X1: $i] :
( g_both(X0,sK10(X1))
| g_true_only(X0,sK10(X1))
| ~ g_both(X0,X1) ),
inference(superposition,[status(thm)],[c_12219,c_88]) ).
tcf(c_12466,plain,
! [X0: $i] :
( g_both(sK10(X0),sK9)
| g_true_only(sK10(X0),sK9)
| g_true(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_12219,c_9565]) ).
tcf(c_12586,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_true_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(superposition,[status(thm)],[c_12345,c_102]) ).
tcf(c_12587,plain,
! [X0: $i] :
( g_both(X0,X0)
| g_true_only(X0,X0)
| ~ g_both(X0,sK9) ),
inference(superposition,[status(thm)],[c_12345,c_80]) ).
tcf(c_12589,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_both(X0,sK10(X1))
| g_true_only(X0,sK10(X1)) ),
inference(superposition,[status(thm)],[c_12345,c_4129]) ).
tcf(c_12590,plain,
! [X0: $i,X1: $i] :
( g_both(X0,sK10(X1))
| g_true_only(X0,sK10(X1))
| ~ g_both(X0,X1) ),
inference(superposition,[status(thm)],[c_12345,c_88]) ).
tcf(c_12591,plain,
! [X0: $i] :
( g_both(sK10(X0),sK9)
| g_true_only(sK10(X0),sK9)
| g_true(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_12345,c_9539]) ).
tcf(c_12675,plain,
! [X0: $i] :
( g_both(X0,X0)
| ~ g_both(X0,sK9) ),
inference(global_subsumption_just,[status(thm)],[c_12462,c_79,c_12462]) ).
tcf(c_12692,plain,
! [X0: $i] :
( g_both(X0,X0)
| ~ g_both(X0,sK9) ),
inference(global_subsumption_just,[status(thm)],[c_12587,c_12675]) ).
tcf(c_12726,plain,
! [X0: $i,X1: $i] :
( g_both(X0,sK10(X1))
| ~ g_both(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_12465,c_83,c_12465]) ).
tcf(c_12741,plain,
! [X0: $i] :
( ~ g_false_only(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_12726,c_82]) ).
tcf(c_12742,plain,
! [X0: $i] :
( ~ g_true_only(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_12726,c_77]) ).
tcf(c_12748,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| ~ iPr_def_11
| ~ g_both(sK10(sK10(X0)),X0) ),
inference(superposition,[status(thm)],[c_12726,c_7927]) ).
tcf(c_13032,plain,
! [X0: $i,X1: $i] :
( g_both(X0,sK10(X1))
| ~ g_both(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_12590,c_83,c_12465]) ).
tcf(c_13044,plain,
! [X0: $i,X1: $i] :
( g_false(X0,sK10(X1))
| ~ g_both(X0,X1) ),
inference(superposition,[status(thm)],[c_13032,c_99]) ).
tcf(c_13046,plain,
! [X0: $i] :
( ~ g_false_only(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_13032,c_82]) ).
tcf(c_13053,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| ~ iPr_def_11
| ~ g_both(sK10(sK10(X0)),X0) ),
inference(superposition,[status(thm)],[c_13032,c_7918]) ).
tcf(c_13564,plain,
! [X0: $i] :
( g_both(sK10(X0),sK9)
| g_true_only(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_12219,c_12741]) ).
tcf(c_13573,plain,
! [X0: $i] :
( g_both(sK10(X0),sK9)
| g_true_only(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_12345,c_13046]) ).
tcf(c_13830,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_true_only(X0,sK10(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_12464,c_213,c_12464]) ).
tcf(c_13837,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_false(X0,sK10(X1)) ),
inference(superposition,[status(thm)],[c_13830,c_96]) ).
tcf(c_13885,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| g_true(sK10(sK10(X0)),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_8275,c_13837]) ).
tcf(c_13944,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| g_true_only(sK10(X0),sK9) ),
inference(global_subsumption_just,[status(thm)],[c_12466,c_9540,c_12466]) ).
tcf(c_13945,plain,
! [X0: $i] :
( g_true_only(sK10(X0),sK9)
| g_true(sK10(X0),X0) ),
inference(renaming,[status(thm)],[c_13944]) ).
tcf(c_13951,plain,
! [X0: $i] :
( g_true_only(sK10(X0),sK9)
| g_both(sK10(X0),X0)
| g_true_only(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_13945,c_12461]) ).
tcf(c_14009,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| g_true_only(sK10(X0),sK9) ),
inference(global_subsumption_just,[status(thm)],[c_12591,c_9540,c_12466]) ).
tcf(c_14010,plain,
! [X0: $i] :
( g_true_only(sK10(X0),sK9)
| g_true(sK10(X0),X0) ),
inference(renaming,[status(thm)],[c_14009]) ).
tcf(c_14015,plain,
! [X0: $i] :
( g_true_only(sK10(X0),sK9)
| g_both(sK10(X0),X0)
| g_true_only(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_14010,c_12586]) ).
tcf(c_14093,plain,
( ~ g_both(sK5(sK9),sK9)
| ~ g_false_only(sK5(sK9),sK5(sK9)) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_14099,plain,
( ~ g_both(sK5(sK9),sK9)
| ~ g_true_only(sK5(sK9),sK5(sK9)) ),
inference(instantiation,[status(thm)],[c_7039]) ).
tcf(c_14100,plain,
( g_false(sK5(sK9),sK9)
| ~ g_both(sK5(sK9),sK9) ),
inference(instantiation,[status(thm)],[c_10208]) ).
tcf(c_14575,plain,
( ~ g_false(sK7(sK10(sK6)),sK6)
| ~ g_true_only(sK7(sK10(sK6)),sK6) ),
inference(instantiation,[status(thm)],[c_6999]) ).
tcf(c_15058,plain,
( g_false(sK10(sK9),sK9)
| ~ g_both(sK10(sK9),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_8193]) ).
tcf(c_15291,plain,
( ~ g_both(sK10(sK10(sK10(sK9))),sK10(sK9))
| ~ g_false_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK9))) ),
inference(instantiation,[status(thm)],[c_8207]) ).
tcf(c_15310,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_true_only(X0,sK10(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_12589,c_13830]) ).
tcf(c_15316,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| ~ g_false(X0,sK10(X1)) ),
inference(superposition,[status(thm)],[c_15310,c_96]) ).
tcf(c_15330,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| g_true(sK10(sK10(X0)),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_8266,c_15316]) ).
tcf(c_15912,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| g_both(sK10(sK10(X0)),X0)
| ~ iPr_def_11
| ~ g_false(sK10(sK10(X0)),X0) ),
inference(superposition,[status(thm)],[c_13885,c_97]) ).
tcf(c_16759,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| g_both(sK10(sK10(X0)),X0)
| ~ iPr_def_11
| ~ g_false(sK10(sK10(X0)),X0) ),
inference(superposition,[status(thm)],[c_15330,c_97]) ).
tcf(c_16933,plain,
! [X0: $i] :
( g_both(sK10(X0),X0)
| g_true_only(sK10(X0),X0)
| ~ g_false(sK10(X0),sK9) ),
inference(superposition,[status(thm)],[c_13951,c_96]) ).
tcf(c_16941,plain,
( g_both(sK10(sK9),sK9)
| g_true_only(sK10(sK9),sK9) ),
inference(equality_factoring,[status(thm)],[c_13951]) ).
tcf(c_17212,plain,
( g_both(sK10(sK9),sK9)
| ~ g_false(sK10(sK9),sK9) ),
inference(superposition,[status(thm)],[c_16941,c_96]) ).
tcf(c_17213,plain,
( g_both(sK10(sK9),sK9)
| ~ g_false_only(sK10(sK9),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_16941,c_78]) ).
tcf(c_17280,plain,
( g_true(sK10(sK9),sK9)
| g_both(sK10(sK9),sK9) ),
inference(superposition,[status(thm)],[c_4137,c_17212]) ).
tcf(c_17287,plain,
~ g_false_only(sK10(sK9),sK10(sK9)),
inference(global_subsumption_just,[status(thm)],[c_17213,c_9396,c_17213]) ).
tcf(c_17289,plain,
( g_both(sK10(sK9),sK10(sK9))
| g_true_only(sK10(sK9),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_12219,c_17287]) ).
tcf(c_17522,plain,
! [X0: $i] :
( g_both(sK10(X0),X0)
| g_true_only(sK10(X0),X0)
| ~ g_false(sK10(X0),sK9) ),
inference(superposition,[status(thm)],[c_14015,c_96]) ).
tcf(c_17530,plain,
( g_both(sK10(sK9),sK9)
| g_true_only(sK10(sK9),sK9) ),
inference(equality_factoring,[status(thm)],[c_14015]) ).
tcf(c_17736,plain,
g_true(sK10(sK9),sK9),
inference(global_subsumption_just,[status(thm)],[c_17280,c_11150,c_17280]) ).
tcf(c_17857,plain,
( g_false(sK10(sK9),sK9)
| g_both(sK10(sK9),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_17289,c_4121]) ).
tcf(c_17876,plain,
g_false(sK10(sK9),sK9),
inference(global_subsumption_just,[status(thm)],[c_17857,c_15058,c_17857]) ).
tcf(c_17878,plain,
g_both(sK10(sK9),sK9),
inference(backward_subsumption_resolution,[status(thm)],[c_17212,c_17876]) ).
tcf(c_17880,plain,
( g_both(sK5(sK9),sK9)
| g_false_only(sK5(sK9),sK9)
| g_both(sK5(sK9),sK5(sK9))
| g_false_only(sK5(sK9),sK5(sK9))
| ~ sP2
| ~ g_both(sK10(sK9),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_17878,c_57]) ).
tcf(c_17881,plain,
( g_false_only(sK5(sK9),sK9)
| g_true_only(sK5(sK9),sK9)
| g_false_only(sK5(sK9),sK5(sK9))
| g_true_only(sK5(sK9),sK5(sK9))
| ~ sP2
| ~ g_both(sK10(sK9),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_17878,c_55]) ).
tcf(c_17882,plain,
( g_both(sK5(sK9),sK9)
| g_true_only(sK5(sK9),sK9)
| g_both(sK5(sK9),sK5(sK9))
| g_true_only(sK5(sK9),sK5(sK9))
| ~ sP2
| ~ g_both(sK10(sK9),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_17878,c_54]) ).
tcf(c_17888,plain,
g_both(sK10(sK9),sK10(sK9)),
inference(superposition,[status(thm)],[c_17878,c_12675]) ).
tcf(c_17894,plain,
( g_both(sK5(sK9),sK9)
| g_true_only(sK5(sK9),sK9)
| g_both(sK5(sK9),sK5(sK9))
| g_true_only(sK5(sK9),sK5(sK9))
| ~ sP2 ),
inference(forward_subsumption_resolution,[status(thm)],[c_17882,c_17888]) ).
tcf(c_17900,plain,
( g_false_only(sK5(sK9),sK9)
| g_true_only(sK5(sK9),sK9)
| g_false_only(sK5(sK9),sK5(sK9))
| g_true_only(sK5(sK9),sK5(sK9))
| ~ sP2 ),
inference(forward_subsumption_resolution,[status(thm)],[c_17881,c_17888]) ).
tcf(c_17906,plain,
( g_both(sK5(sK9),sK9)
| g_false_only(sK5(sK9),sK9)
| g_both(sK5(sK9),sK5(sK9))
| g_false_only(sK5(sK9),sK5(sK9))
| ~ sP2 ),
inference(forward_subsumption_resolution,[status(thm)],[c_17880,c_17888]) ).
tcf(c_17962,plain,
( ~ g_false_only(sK5(sK9),sK9)
| ~ g_true_only(sK5(sK9),sK5(sK9)) ),
inference(instantiation,[status(thm)],[c_7040]) ).
tcf(c_17964,plain,
g_both(sK10(sK9),sK9),
inference(global_subsumption_just,[status(thm)],[c_17530,c_9395,c_17736,c_17876]) ).
tcf(c_17967,plain,
( g_false_only(sK5(sK9),sK9)
| g_true_only(sK5(sK9),sK9)
| g_false_only(sK5(sK9),sK5(sK9))
| g_true_only(sK5(sK9),sK5(sK9))
| ~ sP2
| ~ g_both(sK10(sK9),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_17964,c_55]) ).
tcf(c_17974,plain,
g_both(sK10(sK9),sK10(sK9)),
inference(superposition,[status(thm)],[c_17964,c_12692]) ).
tcf(c_17979,plain,
~ iPr_def_10,
inference(superposition,[status(thm)],[c_17964,c_10373]) ).
tcf(c_17992,plain,
( g_false_only(sK5(sK9),sK9)
| g_true_only(sK5(sK9),sK9)
| g_false_only(sK5(sK9),sK5(sK9))
| g_true_only(sK5(sK9),sK5(sK9))
| ~ sP2 ),
inference(forward_subsumption_resolution,[status(thm)],[c_17967,c_17974]) ).
tcf(c_18022,plain,
( sP1
| sP2
| sP3 ),
inference(backward_subsumption_resolution,[status(thm)],[c_6852,c_17979]) ).
tcf(c_18459,plain,
( g_false_only(sK5(sK9),sK9)
| g_true_only(sK5(sK9),sK9)
| ~ sP2 ),
inference(global_subsumption_just,[status(thm)],[c_17992,c_7027,c_7026,c_7932,c_8791,c_9354,c_9352,c_11033,c_11032,c_11182,c_11183,c_14093,c_14099,c_14100,c_17906,c_17900,c_17894,c_17962]) ).
tcf(c_18461,plain,
( g_false_only(sK5(sK9),sK9)
| ~ sP2 ),
inference(global_subsumption_just,[status(thm)],[c_18459,c_7027,c_7026,c_9354,c_9352,c_11033,c_11032,c_11182,c_14100,c_17906,c_17894,c_17962,c_18459]) ).
tcf(c_18463,plain,
~ sP2,
inference(global_subsumption_just,[status(thm)],[c_18461,c_7027,c_7026,c_9354,c_9352,c_11182,c_17894,c_17962,c_18461]) ).
tcf(c_18465,plain,
( sP1
| sP3 ),
inference(backward_subsumption_resolution,[status(thm)],[c_18022,c_18463]) ).
tcf(c_18557,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(sK10(X0))),sK11)
| ~ iPr_def_11
| ~ g_both(sK10(sK10(sK10(X0))),X0) ),
inference(superposition,[status(thm)],[c_13032,c_13053]) ).
tcf(c_18562,plain,
! [X0: $i] :
( g_both(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_13573,c_12742,c_13564]) ).
tcf(c_19264,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| ~ iPr_def_11
| g_false_only(sK10(X0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_12347,c_7918,c_12221]) ).
tcf(c_19265,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| g_false_only(sK10(X0),X0)
| ~ iPr_def_11 ),
inference(renaming,[status(thm)],[c_19264]) ).
tcf(c_19849,plain,
! [X0: $i] :
( g_true(sK10(X0),sK9)
| g_both(sK10(X0),X0)
| g_true_only(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_4137,c_16933]) ).
tcf(c_19894,plain,
! [X0: $i] :
( g_true(sK10(X0),sK9)
| g_true_only(sK10(X0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_19849,c_6908,c_12741,c_19849]) ).
tcf(c_19905,plain,
! [X0: $i] :
( g_true(sK10(sK10(X0)),sK9)
| g_false(sK10(sK10(X0)),X0) ),
inference(superposition,[status(thm)],[c_19894,c_4121]) ).
tcf(c_20329,plain,
! [X0: $i] :
( g_true(sK10(X0),sK9)
| g_both(sK10(X0),X0)
| g_true_only(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_4137,c_17522]) ).
tcf(c_20437,plain,
! [X0: $i] :
( g_true(sK10(X0),sK9)
| g_true_only(sK10(X0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_20329,c_6908,c_12741,c_19849]) ).
tcf(c_20448,plain,
! [X0: $i] :
( g_true(sK10(sK10(X0)),sK9)
| g_false(sK10(sK10(X0)),X0) ),
inference(superposition,[status(thm)],[c_20437,c_4121]) ).
tcf(c_20463,plain,
! [X0: $i] :
( g_true(sK10(sK10(sK10(X0))),sK9)
| g_true(sK10(sK10(sK10(X0))),X0) ),
inference(superposition,[status(thm)],[c_19905,c_13837]) ).
tcf(c_20963,plain,
! [X0: $i] :
( g_true(sK10(sK10(sK10(X0))),sK9)
| g_true(sK10(sK10(sK10(X0))),X0) ),
inference(superposition,[status(thm)],[c_20448,c_15316]) ).
tcf(c_21364,plain,
g_true(sK10(sK10(sK10(sK9))),sK9),
inference(equality_factoring,[status(thm)],[c_20463]) ).
tcf(c_22054,plain,
g_true(sK10(sK10(sK10(sK9))),sK9),
inference(equality_factoring,[status(thm)],[c_20963]) ).
tcf(c_22649,plain,
( g_both(sK10(sK10(sK10(sK9))),sK9)
| g_true_only(sK10(sK10(sK10(sK9))),sK9) ),
inference(superposition,[status(thm)],[c_22054,c_12586]) ).
tcf(c_22650,plain,
( g_both(sK10(sK10(sK10(sK9))),sK9)
| ~ g_false(sK10(sK10(sK10(sK9))),sK9) ),
inference(superposition,[status(thm)],[c_22054,c_97]) ).
tcf(c_22761,plain,
( g_both(sK10(sK10(sK10(sK9))),sK9)
| ~ g_false_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9)))) ),
inference(superposition,[status(thm)],[c_22649,c_78]) ).
tcf(c_22797,plain,
( g_both(sK10(sK10(sK10(sK9))),sK9)
| g_true_only(sK10(sK10(sK10(sK9))),sK9) ),
inference(superposition,[status(thm)],[c_21364,c_12461]) ).
tcf(c_22840,plain,
~ g_false_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9)))),
inference(forward_subsumption_resolution,[status(thm)],[c_22761,c_80]) ).
tcf(c_22841,plain,
( g_both(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9))))
| g_true_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9)))) ),
inference(superposition,[status(thm)],[c_12345,c_22840]) ).
tcf(c_22859,plain,
( g_both(sK10(sK10(sK10(sK9))),sK9)
| ~ g_false_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9)))) ),
inference(superposition,[status(thm)],[c_22797,c_78]) ).
tcf(c_22978,plain,
~ g_false_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9)))),
inference(forward_subsumption_resolution,[status(thm)],[c_22859,c_80]) ).
tcf(c_22979,plain,
( g_both(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9))))
| g_true_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9)))) ),
inference(superposition,[status(thm)],[c_12219,c_22978]) ).
tcf(c_23928,plain,
( g_false(sK10(sK10(sK10(sK9))),sK10(sK10(sK9)))
| g_both(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9)))) ),
inference(superposition,[status(thm)],[c_22841,c_4121]) ).
tcf(c_24123,plain,
( ~ g_false(sK8(sK9,sK10(sK9)),sK9)
| ~ g_true_only(sK8(sK9,sK10(sK9)),sK9) ),
inference(instantiation,[status(thm)],[c_9021]) ).
tcf(c_24554,plain,
( g_false(sK10(sK10(sK10(sK9))),sK10(sK10(sK9)))
| g_both(sK10(sK10(sK10(sK9))),sK10(sK10(sK10(sK9)))) ),
inference(superposition,[status(thm)],[c_22979,c_4121]) ).
tcf(c_27171,plain,
g_false(sK10(sK10(sK10(sK9))),sK10(sK10(sK9))),
inference(forward_subsumption_resolution,[status(thm)],[c_23928,c_4125]) ).
tcf(c_27172,plain,
( g_both(sK10(sK10(sK10(sK9))),sK10(sK10(sK9)))
| g_false_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK9))) ),
inference(superposition,[status(thm)],[c_27171,c_8873]) ).
tcf(c_27173,plain,
g_true(sK10(sK10(sK10(sK9))),sK10(sK9)),
inference(superposition,[status(thm)],[c_27171,c_15316]) ).
tcf(c_27200,plain,
( g_both(sK10(sK10(sK10(sK9))),sK10(sK9))
| ~ g_false(sK10(sK10(sK10(sK9))),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_27173,c_97]) ).
tcf(c_27789,plain,
g_false(sK10(sK10(sK10(sK9))),sK10(sK10(sK9))),
inference(forward_subsumption_resolution,[status(thm)],[c_24554,c_4125]) ).
tcf(c_27791,plain,
g_true(sK10(sK10(sK10(sK9))),sK10(sK9)),
inference(superposition,[status(thm)],[c_27789,c_13837]) ).
tcf(c_27852,plain,
( g_both(sK10(sK10(sK10(sK9))),sK10(sK9))
| g_true_only(sK10(sK10(sK10(sK9))),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_27791,c_12461]) ).
tcf(c_28499,plain,
( g_both(sK10(sK10(sK10(sK9))),sK10(sK9))
| ~ g_both(sK10(sK10(sK10(sK9))),sK9) ),
inference(superposition,[status(thm)],[c_13044,c_27200]) ).
tcf(c_28791,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| ~ g_false(sK10(sK10(X0)),X0)
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_16759,c_12748,c_15912]) ).
tcf(c_28792,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| ~ iPr_def_11
| ~ g_false(sK10(sK10(X0)),X0) ),
inference(renaming,[status(thm)],[c_28791]) ).
tcf(c_28800,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| g_true_only(sK10(sK10(X0)),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_4082,c_28792]) ).
tcf(c_29073,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(sK10(X0))),sK11)
| g_false(sK10(sK10(sK10(X0))),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_28800,c_4121]) ).
tcf(c_29591,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(sK10(X0))),sK11)
| g_both(sK10(sK10(sK10(X0))),X0)
| g_false_only(sK10(sK10(sK10(X0))),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_29073,c_8873]) ).
tcf(c_34093,plain,
( g_false(sK10(sK10(sK10(sK9))),sK9)
| g_both(sK10(sK10(sK10(sK9))),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_27852,c_4121]) ).
tcf(c_34097,plain,
g_both(sK10(sK10(sK10(sK9))),sK10(sK9)),
inference(global_subsumption_just,[status(thm)],[c_34093,c_22650,c_28499,c_34093]) ).
tcf(c_36769,plain,
( g_false(sK8(sK9,sK10(sK9)),sK9)
| g_true(sK8(sK9,sK10(sK9)),sK9) ),
inference(instantiation,[status(thm)],[c_9012]) ).
tcf(c_36770,plain,
( g_false(sK8(sK9,sK10(sK9)),sK9)
| ~ g_true_only(sK8(sK9,sK10(sK9)),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_9011]) ).
tcf(c_36771,plain,
( g_false(sK8(sK9,sK10(sK9)),sK9)
| ~ g_both(sK8(sK9,sK10(sK9)),sK9) ),
inference(instantiation,[status(thm)],[c_9015]) ).
tcf(c_36773,plain,
( g_false(sK8(sK9,sK10(sK9)),sK9)
| ~ g_both(sK8(sK9,sK10(sK9)),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_9013]) ).
tcf(c_46101,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| g_false(sK10(X0),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_6853,c_4121]) ).
tcf(c_46203,plain,
! [X0: $i] :
( g_both(sK7(sK10(X0)),sK6)
| g_false_only(sK7(sK10(X0)),sK6)
| g_false(sK7(sK10(X0)),X0)
| g_both(sK7(sK10(X0)),sK10(X0))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_62,c_4121]) ).
tcf(c_46291,plain,
! [X0: $i] :
( g_both(sK7(sK10(X0)),sK6)
| g_false_only(sK7(sK10(X0)),sK6)
| g_false(sK7(sK10(X0)),X0)
| ~ sP1 ),
inference(global_subsumption_just,[status(thm)],[c_46203,c_7422,c_9192]) ).
tcf(c_46469,plain,
! [X0: $i] :
( g_both(sK7(sK10(X0)),sK6)
| g_true_only(sK7(sK10(X0)),sK6)
| g_true(sK7(sK10(X0)),X0)
| g_both(sK7(sK10(X0)),sK10(X0))
| ~ sP1 ),
inference(superposition,[status(thm)],[c_65,c_4129]) ).
tcf(c_46670,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_false_only(X0,X1)
| ~ g_false(X0,X1) ),
inference(superposition,[status(thm)],[c_4086,c_97]) ).
tcf(c_46693,plain,
! [X0: $i] :
( g_both(sK7(sK10(X0)),sK6)
| g_true_only(sK7(sK10(X0)),sK6)
| g_true(sK7(sK10(X0)),X0)
| ~ sP1 ),
inference(global_subsumption_just,[status(thm)],[c_46469,c_7200,c_10099]) ).
tcf(c_46695,plain,
( g_true(sK7(sK10(sK6)),sK6)
| g_both(sK7(sK10(sK6)),sK6)
| g_true_only(sK7(sK10(sK6)),sK6)
| ~ sP1 ),
inference(instantiation,[status(thm)],[c_46693]) ).
tcf(c_46846,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_false_only(X0,X1)
| g_true_only(X0,X1) ),
inference(superposition,[status(thm)],[c_4082,c_46670]) ).
tcf(c_46849,plain,
! [X0: $i] :
( g_both(sK7(sK10(X0)),sK6)
| g_false_only(sK7(sK10(X0)),sK6)
| g_both(sK7(sK10(X0)),X0)
| g_false_only(sK7(sK10(X0)),X0)
| ~ sP1 ),
inference(superposition,[status(thm)],[c_46291,c_46670]) ).
tcf(c_46851,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| g_both(sK10(X0),X0)
| g_false_only(sK10(X0),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_46101,c_46670]) ).
tcf(c_46873,plain,
( g_both(sK7(sK10(sK6)),sK6)
| g_false_only(sK7(sK10(sK6)),sK6)
| ~ sP1 ),
inference(instantiation,[status(thm)],[c_46849]) ).
tcf(c_46876,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| ~ iPr_def_11
| g_false_only(sK10(X0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_46851,c_19265]) ).
tcf(c_46877,plain,
! [X0: $i] :
( g_false_only(sK10(X0),sK11)
| g_false_only(sK10(X0),X0)
| ~ iPr_def_11 ),
inference(renaming,[status(thm)],[c_46876]) ).
tcf(c_46887,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| g_true(sK10(sK10(X0)),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_46877,c_4129]) ).
tcf(c_46927,plain,
! [X0: $i,X1: $i] :
( g_both(X0,X1)
| g_true_only(X0,X1)
| ~ g_true(X0,X1) ),
inference(superposition,[status(thm)],[c_46846,c_102]) ).
tcf(c_46930,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_both(X0,sK10(X1))
| g_true_only(X0,sK10(X1)) ),
inference(superposition,[status(thm)],[c_46846,c_4129]) ).
tcf(c_46931,plain,
! [X0: $i,X1: $i] :
( g_both(X0,sK10(X1))
| g_true_only(X0,sK10(X1))
| ~ g_both(X0,X1) ),
inference(superposition,[status(thm)],[c_46846,c_88]) ).
tcf(c_46967,plain,
! [X0: $i,X1: $i] :
( g_both(X0,sK10(X1))
| ~ g_both(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_46931,c_83,c_12465]) ).
tcf(c_46975,plain,
! [X0: $i] :
( ~ g_false_only(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_46967,c_82]) ).
tcf(c_47001,plain,
! [X0: $i] :
( g_both(sK10(X0),sK9)
| g_true_only(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(superposition,[status(thm)],[c_46846,c_46975]) ).
tcf(c_47046,plain,
! [X0: $i] :
( g_both(sK10(X0),sK9)
| ~ g_both(sK10(X0),X0) ),
inference(global_subsumption_just,[status(thm)],[c_47001,c_18562]) ).
tcf(c_47113,plain,
! [X0: $i,X1: $i] :
( g_true(X0,X1)
| g_true_only(X0,sK10(X1)) ),
inference(global_subsumption_just,[status(thm)],[c_46930,c_213,c_12464]) ).
tcf(c_47120,plain,
! [X0: $i] :
( g_true(sK10(X0),X0)
| ~ g_false_only(sK10(X0),sK9) ),
inference(superposition,[status(thm)],[c_47113,c_81]) ).
tcf(c_47558,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| g_both(sK10(sK10(X0)),X0)
| g_true_only(sK10(sK10(X0)),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_46887,c_46927]) ).
tcf(c_47666,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| ~ iPr_def_11
| g_true_only(sK10(sK10(X0)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_47558,c_28800]) ).
tcf(c_47667,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(X0)),sK11)
| g_true_only(sK10(sK10(X0)),X0)
| ~ iPr_def_11 ),
inference(renaming,[status(thm)],[c_47666]) ).
tcf(c_47677,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(sK10(X0))),sK11)
| g_false(sK10(sK10(sK10(X0))),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_47667,c_4121]) ).
tcf(c_47842,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(sK10(X0))),sK11)
| g_both(sK10(sK10(sK10(X0))),X0)
| g_false_only(sK10(sK10(sK10(X0))),X0)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_47677,c_46670]) ).
tcf(c_47890,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(sK10(X0))),sK11)
| ~ iPr_def_11
| g_false_only(sK10(sK10(sK10(X0))),X0) ),
inference(global_subsumption_just,[status(thm)],[c_47842,c_18557,c_29591]) ).
tcf(c_47891,plain,
! [X0: $i] :
( g_false_only(sK10(sK10(sK10(X0))),sK11)
| g_false_only(sK10(sK10(sK10(X0))),X0)
| ~ iPr_def_11 ),
inference(renaming,[status(thm)],[c_47890]) ).
tcf(c_47904,plain,
( g_false_only(sK10(sK10(sK10(sK9))),sK11)
| g_true(sK10(sK10(sK10(sK9))),sK10(sK10(sK9)))
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_47891,c_47120]) ).
tcf(c_47930,plain,
g_true(sK10(sK10(sK10(sK9))),sK10(sK10(sK9))),
inference(global_subsumption_just,[status(thm)],[c_47904,c_12338,c_15291,c_34097]) ).
tcf(c_47932,plain,
( g_both(sK10(sK10(sK10(sK9))),sK10(sK10(sK9)))
| g_true_only(sK10(sK10(sK10(sK9))),sK10(sK10(sK9))) ),
inference(superposition,[status(thm)],[c_47930,c_46927]) ).
tcf(c_47993,plain,
g_both(sK10(sK10(sK10(sK9))),sK10(sK10(sK9))),
inference(global_subsumption_just,[status(thm)],[c_47932,c_15291,c_27172,c_34097]) ).
tcf(c_47997,plain,
g_false(sK10(sK10(sK10(sK9))),sK10(sK9)),
inference(superposition,[status(thm)],[c_47993,c_4125]) ).
tcf(c_47998,plain,
g_true(sK10(sK10(sK10(sK9))),sK10(sK9)),
inference(superposition,[status(thm)],[c_47993,c_4123]) ).
tcf(c_47999,plain,
g_both(sK10(sK10(sK10(sK9))),sK9),
inference(superposition,[status(thm)],[c_47993,c_47046]) ).
tcf(c_48010,plain,
( g_both(sK10(sK10(sK10(sK9))),sK10(sK9))
| ~ g_false(sK10(sK10(sK10(sK9))),sK10(sK9)) ),
inference(superposition,[status(thm)],[c_47998,c_97]) ).
tcf(c_48013,plain,
g_both(sK10(sK10(sK10(sK9))),sK10(sK9)),
inference(forward_subsumption_resolution,[status(thm)],[c_48010,c_47997]) ).
tcf(c_54428,plain,
! [X0: $i,X1: $i] :
( g_true(sK8(X0,sK10(X1)),X1)
| ~ g_false_only(sK8(X0,sK10(X1)),sK10(X1)) ),
inference(instantiation,[status(thm)],[c_4129]) ).
tcf(c_54441,plain,
! [X0: $i,X1: $i] :
( g_both(sK8(X0,sK10(X1)),X1)
| ~ g_false(sK8(X0,sK10(X1)),X1)
| ~ g_true(sK8(X0,sK10(X1)),X1) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_54442,plain,
! [X0: $i,X1: $i] :
( ~ g_true(sK8(X0,sK10(X1)),X1)
| ~ g_false_only(sK8(X0,sK10(X1)),X1) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_54450,plain,
! [X0: $i,X1: $i] :
( g_true(sK8(X0,sK10(X1)),X1)
| ~ g_both(sK8(X0,sK10(X1)),sK10(X1)) ),
inference(instantiation,[status(thm)],[c_4123]) ).
tcf(c_54513,plain,
! [X0: $i] :
( g_both(sK8(X0,sK10(sK9)),sK9)
| ~ g_false(sK8(X0,sK10(sK9)),sK9)
| ~ g_true(sK8(X0,sK10(sK9)),sK9) ),
inference(instantiation,[status(thm)],[c_54441]) ).
tcf(c_54535,plain,
! [X0: $i] :
( g_true(sK8(X0,sK10(sK9)),sK9)
| ~ g_both(sK8(X0,sK10(sK9)),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_54450]) ).
tcf(c_54536,plain,
! [X0: $i] :
( g_true(sK8(X0,sK10(sK9)),sK9)
| ~ g_false_only(sK8(X0,sK10(sK9)),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_54428]) ).
tcf(c_54712,plain,
! [X0: $i,X1: $i] :
( g_true(sK8(X0,sK10(X1)),X0)
| ~ g_both(sK8(X0,sK10(X1)),X0) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_54713,plain,
! [X0: $i,X1: $i] :
( ~ g_both(sK8(X0,sK10(X1)),X0)
| ~ g_false_only(sK8(X0,sK10(X1)),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_54714,plain,
! [X0: $i,X1: $i] :
( ~ g_both(sK8(X0,sK10(X1)),X0)
| ~ g_true_only(sK8(X0,sK10(X1)),sK10(X0)) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_54926,plain,
! [X0: $i] :
( ~ g_true(sK8(X0,sK10(sK9)),sK9)
| ~ g_false_only(sK8(X0,sK10(sK9)),sK9) ),
inference(instantiation,[status(thm)],[c_54442]) ).
tcf(c_55445,plain,
( ~ g_true(sK8(sK9,sK10(sK9)),sK9)
| ~ g_false_only(sK8(sK9,sK10(sK9)),sK9) ),
inference(instantiation,[status(thm)],[c_54926]) ).
tcf(c_60065,plain,
( g_both(sK8(sK9,sK10(sK9)),sK9)
| ~ g_false(sK8(sK9,sK10(sK9)),sK9)
| ~ g_true(sK8(sK9,sK10(sK9)),sK9) ),
inference(instantiation,[status(thm)],[c_54513]) ).
tcf(c_60066,plain,
( g_true(sK8(sK9,sK10(sK9)),sK9)
| ~ g_both(sK8(sK9,sK10(sK9)),sK9) ),
inference(instantiation,[status(thm)],[c_54712]) ).
tcf(c_60067,plain,
( ~ g_both(sK8(sK9,sK10(sK9)),sK9)
| ~ g_true_only(sK8(sK9,sK10(sK9)),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_54714]) ).
tcf(c_60536,plain,
( g_true(sK8(sK9,sK10(sK9)),sK9)
| ~ g_both(sK8(sK9,sK10(sK9)),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_54535]) ).
tcf(c_63293,plain,
( g_true(sK8(sK9,sK10(sK9)),sK9)
| ~ g_false_only(sK8(sK9,sK10(sK9)),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_54536]) ).
tcf(c_63587,plain,
( ~ g_both(sK8(sK9,sK10(sK9)),sK9)
| ~ g_false_only(sK8(sK9,sK10(sK9)),sK10(sK9)) ),
inference(instantiation,[status(thm)],[c_54713]) ).
fof(f9,definition,
! [X10] :
( ~ sP0(X10)
| ! [X11] :
( ? [X13] :
( ( ( g_both(X13,X10)
| g_false_only(X13,X10) )
& g_false_only(X13,X11) )
| ( ( g_true_only(X13,X10)
| g_false_only(X13,X10) )
& g_both(X13,X11) )
| ( ( g_true_only(X13,X10)
| g_both(X13,X10) )
& g_true_only(X13,X11) ) )
| ! [X12] :
( ~ g_both(X12,X10)
| ~ g_both(X12,X11) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f10,definition,
( ~ sP1
| ? [X16] :
! [X17] :
? [X18] :
( ( ( g_both(X18,X16)
| g_false_only(X18,X16) )
& g_false_only(X18,X17) )
| ( ( g_true_only(X18,X16)
| g_false_only(X18,X16) )
& g_both(X18,X17) )
| ( ( g_true_only(X18,X16)
| g_both(X18,X16) )
& g_true_only(X18,X17) ) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f11,definition,
( ~ sP2
| ! [X5] :
( ? [X7] :
( ( ( g_both(X7,X7)
| g_true_only(X7,X7) )
& g_false_only(X7,X5) )
| ( ( g_false_only(X7,X7)
| g_true_only(X7,X7) )
& g_both(X7,X5) )
| ( ( g_false_only(X7,X7)
| g_both(X7,X7) )
& g_true_only(X7,X5) ) )
| ! [X6] :
( ~ g_both(X6,X6)
| ~ g_both(X6,X5) ) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f12,definition,
( ~ sP3
| ! [X10] :
( ? [X14] :
! [X15] :
( ( g_true_only(X15,X10)
& g_false_only(X15,X14) )
| ( g_false_only(X15,X10)
& g_true_only(X15,X14) ) )
| sP0(X10) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f13,plain,
( ( sP1
| sP3
| ? [X8] :
! [X9] :
( ( g_false_only(X9,X9)
& g_false_only(X9,X8) )
| ( g_true_only(X9,X9)
& g_true_only(X9,X8) ) )
| sP2 )
& ! [X2] :
? [X3] :
! [X4] :
( ( ( ~ g_both(X4,X2)
& ~ g_false_only(X4,X2) )
| ~ g_false_only(X4,X3) )
& ( ( ~ g_true_only(X4,X2)
& ~ g_false_only(X4,X2) )
| ~ g_both(X4,X3) )
& ( ( ~ g_true_only(X4,X2)
& ~ g_both(X4,X2) )
| ~ g_true_only(X4,X3) ) )
& ? [X0] :
! [X1] :
( ( ( ~ g_both(X1,X1)
& ~ g_true_only(X1,X1) )
| ~ g_false_only(X1,X0) )
& ( ( ~ g_false_only(X1,X1)
& ~ g_true_only(X1,X1) )
| ~ g_both(X1,X0) )
& ( ( ~ g_false_only(X1,X1)
& ~ g_both(X1,X1) )
| ~ g_true_only(X1,X0) ) ) ),
inference(definition_folding,[],[f8,f12,f11,f10,f9]) ).
fof(f23,plain,
! [X10] :
( ~ sP0(X10)
| ! [X11] :
( ? [X13] :
( ( ( g_both(X13,X10)
| g_false_only(X13,X10) )
& g_false_only(X13,X11) )
| ( ( g_true_only(X13,X10)
| g_false_only(X13,X10) )
& g_both(X13,X11) )
| ( ( g_true_only(X13,X10)
| g_both(X13,X10) )
& g_true_only(X13,X11) ) )
| ! [X12] :
( ~ g_both(X12,X10)
| ~ g_both(X12,X11) ) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f24,plain,
! [X0] :
( ~ sP0(X0)
| ! [X1] :
( ? [X3] :
( ( ( g_both(X3,X0)
| g_false_only(X3,X0) )
& g_false_only(X3,X1) )
| ( ( g_true_only(X3,X0)
| g_false_only(X3,X0) )
& g_both(X3,X1) )
| ( ( g_true_only(X3,X0)
| g_both(X3,X0) )
& g_true_only(X3,X1) ) )
| ! [X2] :
( ~ g_both(X2,X0)
| ~ g_both(X2,X1) ) ) ),
inference(rectify,[],[f23]) ).
fof(f25,plain,
! [X0] :
( ~ sP0(X0)
| ! [X1] :
( ( ( g_both(sK8(X0,X1),X0)
| g_false_only(sK8(X0,X1),X0) )
& g_false_only(sK8(X0,X1),X1) )
| ( ( g_true_only(sK8(X0,X1),X0)
| g_false_only(sK8(X0,X1),X0) )
& g_both(sK8(X0,X1),X1) )
| ( ( g_true_only(sK8(X0,X1),X0)
| g_both(sK8(X0,X1),X0) )
& g_true_only(sK8(X0,X1),X1) )
| ! [X2] :
( ~ g_both(X2,X0)
| ~ g_both(X2,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X3,sK8(X0,X1))],[f24]) ).
fof(f57,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| g_false_only(sK8(X0,X1),X1)
| g_both(sK8(X0,X1),X1)
| g_true_only(sK8(X0,X1),X0)
| g_both(sK8(X0,X1),X0)
| ~ g_both(X2,X0)
| ~ g_both(X2,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f59,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| g_false_only(sK8(X0,X1),X1)
| g_true_only(sK8(X0,X1),X0)
| g_false_only(sK8(X0,X1),X0)
| g_true_only(sK8(X0,X1),X1)
| ~ g_both(X2,X0)
| ~ g_both(X2,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f60,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| g_both(sK8(X0,X1),X0)
| g_false_only(sK8(X0,X1),X0)
| g_both(sK8(X0,X1),X1)
| g_true_only(sK8(X0,X1),X1)
| ~ g_both(X2,X0)
| ~ g_both(X2,X1) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] :
( g_both(sK8(X1,X2),X2)
| g_both(sK8(X1,X2),X1)
| g_false_only(sK8(X1,X2),X1)
| g_true_only(sK8(X1,X2),X2)
| ~ sP0(X1)
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] :
( g_false_only(sK8(X1,X2),X2)
| g_false_only(sK8(X1,X2),X1)
| g_true_only(sK8(X1,X2),X2)
| g_true_only(sK8(X1,X2),X1)
| ~ sP0(X1)
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i] :
( g_both(sK8(X1,X2),X2)
| g_both(sK8(X1,X2),X1)
| g_false_only(sK8(X1,X2),X2)
| g_true_only(sK8(X1,X2),X1)
| ~ sP0(X1)
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_2159,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( g_both(sK8(X1,X2),X2)
| g_both(sK8(X1,X2),X1)
| g_false_only(sK8(X1,X2),X2)
| g_true_only(sK8(X1,X2),X1)
| ~ sP3
| ~ g_false(X3,X1)
| ~ g_true(X3,X1)
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(resolution,[status(thm)],[c_295,c_73]) ).
tcf(c_2160,plain,
! [X0: $i,X1: $i,X2: $i] :
( g_both(sK8(X1,X2),X2)
| g_both(sK8(X1,X2),X1)
| g_false_only(sK8(X1,X2),X2)
| g_true_only(sK8(X1,X2),X1)
| ~ sP3
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2159,c_99,c_73,c_767]) ).
tcf(c_2183,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( g_false_only(sK8(X1,X2),X2)
| g_false_only(sK8(X1,X2),X1)
| g_true_only(sK8(X1,X2),X2)
| g_true_only(sK8(X1,X2),X1)
| ~ sP3
| ~ g_false(X3,X1)
| ~ g_true(X3,X1)
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(resolution,[status(thm)],[c_295,c_71]) ).
tcf(c_2185,plain,
! [X0: $i,X1: $i,X2: $i] :
( g_false_only(sK8(X1,X2),X2)
| g_false_only(sK8(X1,X2),X1)
| g_true_only(sK8(X1,X2),X2)
| g_true_only(sK8(X1,X2),X1)
| ~ sP3
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2183,c_99,c_71,c_767]) ).
tcf(c_2209,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( g_both(sK8(X1,X2),X2)
| g_both(sK8(X1,X2),X1)
| g_false_only(sK8(X1,X2),X1)
| g_true_only(sK8(X1,X2),X2)
| ~ sP3
| ~ g_false(X3,X1)
| ~ g_true(X3,X1)
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(resolution,[status(thm)],[c_295,c_70]) ).
tcf(c_2210,plain,
! [X0: $i,X1: $i,X2: $i] :
( g_both(sK8(X1,X2),X2)
| g_both(sK8(X1,X2),X1)
| g_false_only(sK8(X1,X2),X1)
| g_true_only(sK8(X1,X2),X2)
| ~ sP3
| ~ g_both(X0,X2)
| ~ g_both(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_2209,c_70,c_769]) ).
tcf(c_49574,plain,
! [X0: $i] :
( g_both(sK8(sK9,X0),sK9)
| g_true_only(sK8(sK9,X0),sK9)
| g_both(sK8(sK9,X0),X0)
| g_false_only(sK8(sK9,X0),X0)
| ~ sP3
| ~ g_both(sK10(sK10(sK10(sK9))),X0) ),
inference(superposition,[status(thm)],[c_47999,c_2160]) ).
tcf(c_49621,plain,
( g_both(sK8(sK9,sK10(sK9)),sK9)
| g_true_only(sK8(sK9,sK10(sK9)),sK9)
| g_both(sK8(sK9,sK10(sK9)),sK10(sK9))
| g_false_only(sK8(sK9,sK10(sK9)),sK10(sK9))
| ~ sP3 ),
inference(superposition,[status(thm)],[c_48013,c_49574]) ).
tcf(c_50069,plain,
! [X0: $i] :
( g_false_only(sK8(sK9,X0),sK9)
| g_true_only(sK8(sK9,X0),sK9)
| g_false_only(sK8(sK9,X0),X0)
| g_true_only(sK8(sK9,X0),X0)
| ~ sP3
| ~ g_both(sK10(sK10(sK10(sK9))),X0) ),
inference(superposition,[status(thm)],[c_47999,c_2185]) ).
tcf(c_50116,plain,
( g_false_only(sK8(sK9,sK10(sK9)),sK9)
| g_true_only(sK8(sK9,sK10(sK9)),sK9)
| g_false_only(sK8(sK9,sK10(sK9)),sK10(sK9))
| g_true_only(sK8(sK9,sK10(sK9)),sK10(sK9))
| ~ sP3 ),
inference(superposition,[status(thm)],[c_48013,c_50069]) ).
tcf(c_50842,plain,
! [X0: $i] :
( g_both(sK8(sK9,X0),sK9)
| g_false_only(sK8(sK9,X0),sK9)
| g_both(sK8(sK9,X0),X0)
| g_true_only(sK8(sK9,X0),X0)
| ~ sP3
| ~ g_both(sK10(sK10(sK10(sK9))),X0) ),
inference(superposition,[status(thm)],[c_47999,c_2210]) ).
tcf(c_50962,plain,
( g_both(sK8(sK9,sK10(sK9)),sK9)
| g_false_only(sK8(sK9,sK10(sK9)),sK9)
| g_both(sK8(sK9,sK10(sK9)),sK10(sK9))
| g_true_only(sK8(sK9,sK10(sK9)),sK10(sK9))
| ~ sP3 ),
inference(superposition,[status(thm)],[c_48013,c_50842]) ).
tcf(c_66466,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_63587,c_63293,c_60536,c_60066,c_60067,c_60065,c_55445,c_50962,c_50116,c_49621,c_46873,c_46695,c_36769,c_36770,c_36771,c_36773,c_24123,c_18465,c_14575,c_11554,c_8068,c_7351,c_7206,c_7203]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYO605+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/25.46 % CPULimit : 300
% 0.10/25.46 % WCLimit : 300
% 0.10/25.46 % DateTime : Fri Sep 25 03:15:04 UTC 2026
% 0.10/25.46 % CPUTime :
% 0.10/25.46 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.36/25.50 Running first-order theorem proving
% 0.36/25.50 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.36/25.51
% 0.36/25.51 % ======== iProver multi-core TPTP/SMT =========
% 0.36/25.51
% 0.36/25.51 % Detected problem language: tptp
% 0.36/25.53 % Proving...
% 10.93/27.38 % SZS status Started for theBenchmark.p
% 10.93/27.38 % SZS status Theorem for theBenchmark.p
% 10.93/27.38
% 10.93/27.38 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.93/27.38
% 10.93/27.38 % ------ iProver source info
% 10.93/27.38
% 10.93/27.38 % git: date: 2026-07-19 20:42:38 +0200
% 10.93/27.38 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.93/27.38 % git: non_committed_changes: false
% 10.93/27.38
% 10.93/27.38 % ------ Parsing...
% 10.93/27.38 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 10.93/27.38
% 10.93/27.38 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 10.93/27.38
% 10.93/27.38 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e
% 10.93/27.38 % ------ Proving...
% 10.93/27.38 % ------ Problem Properties
% 10.93/27.38
% 10.93/27.38 %
% 10.93/27.38 % clauses 43
% 10.93/27.38 % conjectures 16
% 10.93/27.38 % EPR 22
% 10.93/27.38 % Horn 17
% 10.93/27.38 % unary 0
% 10.93/27.38 % binary 19
% 10.93/27.38 % lits 158
% 10.93/27.38 % lits eq 0
% 10.93/27.38 % fd_pure 0
% 10.93/27.38 % fd_pseudo 0
% 10.93/27.38 % fd_cond 0
% 10.93/27.38 % fd_pseudo_cond 0
% 10.93/27.38 % AC symbols 0
% 10.93/27.38
% 10.93/27.38 % ------ Schedule dynamic 5 is on
% 10.93/27.38
% 10.93/27.38 % ------ no equalities: superposition off
% 10.93/27.38
% 10.93/27.38 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 10.93/27.38
% 10.93/27.38
% 10.93/27.38 % ------
% 10.93/27.38 % Current options:
% 10.93/27.38 % ------
% 10.93/27.38
% 10.93/27.38
% 10.93/27.38 %
% 10.93/27.38
% 10.93/27.38 % ------ Proving...
% 10.93/27.38 %
% 10.93/27.38
% 10.93/27.38 % SZS status Theorem for theBenchmark.p
% 10.93/27.38
% 10.93/27.38 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.93/27.39
% 10.93/27.39
%------------------------------------------------------------------------------