%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO604+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:12:10 AM UTC 2026
% Result : Theorem 48.09s 48.56s
% Output : Proof 48.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 2
% Syntax : Number of formulae : 276 ( 128 unt; 0 def)
% Number of atoms : 1752 ( 0 equ)
% Maximal formula atoms : 120 ( 6 avg)
% Number of connectives : 2230 ( 754 ~; 854 |; 622 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 50 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 2 con; 0-2 aty)
% Number of variables : 697 ( 43 sgn 401 !; 186 ?)
% Comments :
%------------------------------------------------------------------------------
fof(nc3,conjecture,
( ( ~ ? [A] :
! [B] :
( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& g_false_only(B,A) )
| ( ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) )
& g_true_only(B,A) ) )
& ? [A] :
( ~ ? [B] :
( ( ( ( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_false_only(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_both(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) ) )
& g_true_only(B,A) ) )
& ? [B] :
( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) )
& g_both(B,A) ) ) )
| ! [A] :
? [B] :
( ( ( ( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_false_only(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_both(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) ) )
& g_true_only(B,A) ) ) ),
file('theBenchmark.p',nc3) ).
fof(exhaustion_g,axiom,
! [X_2,X_1] :
( g_false_only(X_2,X_1)
| g_both(X_2,X_1)
| g_true_only(X_2,X_1) ),
file('theBenchmark.p',exhaustion_g) ).
fof(f_1_1,negated_conjecture,
~ ( ( ~ ? [A] :
! [B] :
( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& g_false_only(B,A) )
| ( ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) )
& g_true_only(B,A) ) )
& ? [A] :
( ~ ? [B] :
( ( ( ( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_false_only(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_both(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) ) )
& g_true_only(B,A) ) )
& ? [B] :
( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) )
& g_both(B,A) ) ) )
| ! [A] :
? [B] :
( ( ( ( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_false_only(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_both(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ( ~ ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) ) )
& g_true_only(B,A) ) ) ),
inference(negate,[status(cth)],[nc3]) ).
fof(f_1_2,negated_conjecture,
( ( ? [A] :
! [B] :
( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
& g_false_only(B,A) )
| ( ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) )
& g_true_only(B,A) ) )
| ! [A] :
( ? [B] :
( ( ( ( ! [C] :
( ~ g_true_only(C,B)
| ~ g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_false_only(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C) ) )
& g_both(B,A) )
| ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ( ! [C] :
( ~ g_true_only(C,B)
| ~ g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C)
& ( g_both(C,B)
| g_both(B,C) ) ) ) )
& g_true_only(B,A) ) )
| ! [B] :
( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C)
| ( ~ g_both(C,B)
& ~ g_both(B,C) ) )
| ~ g_both(B,A) ) ) )
& ? [A] :
! [B] :
( ( ( ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C)
| ( ~ g_both(C,B)
& ~ g_both(B,C) ) ) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C) ) )
| ~ g_false_only(B,A) )
& ( ( ! [C] :
( ~ g_true_only(C,B)
| ~ g_true_only(B,C) )
& ? [C] :
( ~ g_false_only(C,B)
& ~ g_false_only(B,C) ) )
| ~ g_both(B,A) )
& ( ( ! [C] :
( ~ g_true_only(C,B)
| ~ g_true_only(B,C) )
& ( ? [C] :
( g_true_only(C,B)
& g_true_only(B,C) )
| ! [C] :
( g_false_only(C,B)
| g_false_only(B,C)
| ( ~ g_both(C,B)
& ~ g_both(B,C) ) ) ) )
| ~ g_true_only(B,A) ) ) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_21] :
( ( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_21)
| ~ g_true_only(U_21,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_21)
& ~ g_false_only(U_21,U_19)
& ( g_both(U_19,U_21)
| g_both(U_21,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_21)
| g_false_only(U_21,U_18) ) )
& g_false_only(U_21,U_22) )
| ( ( ? [U_17] :
( g_true_only(U_17,U_21)
& g_true_only(U_21,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_21)
| g_false_only(U_21,U_16) ) )
& g_both(U_21,U_22) )
| ( ( ? [U_15] :
( g_true_only(U_15,U_21)
& g_true_only(U_21,U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,U_21)
| ~ g_true_only(U_21,U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,U_21)
& ~ g_false_only(U_21,U_13)
& ( g_both(U_13,U_21)
| g_both(U_21,U_13) ) ) ) )
& g_true_only(U_21,U_22) ) )
| ! [U_12] :
( ? [U_11] :
( g_true_only(U_11,U_12)
& g_true_only(U_12,U_11) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ? [U_9] :
! [U_8] :
( ( ( ( ? [U_7] :
( g_true_only(U_7,U_8)
& g_true_only(U_8,U_7) )
| ! [U_6] :
( g_false_only(U_6,U_8)
| g_false_only(U_8,U_6)
| ( ~ g_both(U_6,U_8)
& ~ g_both(U_8,U_6) ) ) )
& ? [U_5] :
( ~ g_false_only(U_5,U_8)
& ~ g_false_only(U_8,U_5) ) )
| ~ g_false_only(U_8,U_9) )
& ( ( ! [U_4] :
( ~ g_true_only(U_4,U_8)
| ~ g_true_only(U_8,U_4) )
& ? [U_3] :
( ~ g_false_only(U_3,U_8)
& ~ g_false_only(U_8,U_3) ) )
| ~ g_both(U_8,U_9) )
& ( ( ! [U_2] :
( ~ g_true_only(U_2,U_8)
| ~ g_true_only(U_8,U_2) )
& ( ? [U_1] :
( g_true_only(U_1,U_8)
& g_true_only(U_8,U_1) )
| ! [U_0] :
( g_false_only(U_0,U_8)
| g_false_only(U_8,U_0)
| ( ~ g_both(U_0,U_8)
& ~ g_both(U_8,U_0) ) ) ) )
| ~ g_true_only(U_8,U_9) ) ) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ? [U_30] :
( ( ? [U_15] :
( g_true_only(U_15,U_30)
& g_true_only(U_30,U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,U_30)
| ~ g_true_only(U_30,U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,U_30)
& ~ g_false_only(U_30,U_13)
& ( g_both(U_13,U_30)
| g_both(U_30,U_13) ) ) ) )
& g_true_only(U_30,U_22) )
| ! [U_12] :
( ? [U_11] :
( g_true_only(U_11,U_12)
& g_true_only(U_12,U_11) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ? [U_9] :
( ! [U_29] :
( ( ( ? [U_7] :
( g_true_only(U_7,U_29)
& g_true_only(U_29,U_7) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ? [U_5] :
( ~ g_false_only(U_5,U_29)
& ~ g_false_only(U_29,U_5) ) )
| ~ g_false_only(U_29,U_9) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ? [U_3] :
( ~ g_false_only(U_3,U_28)
& ~ g_false_only(U_28,U_3) ) )
| ~ g_both(U_28,U_9) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ? [U_1] :
( g_true_only(U_1,U_27)
& g_true_only(U_27,U_1) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,U_9) ) ) ),
inference(miniscope,[status(thm)],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ? [U_30] :
( ( ? [U_15] :
( g_true_only(U_15,U_30)
& g_true_only(U_30,U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,U_30)
| ~ g_true_only(U_30,U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,U_30)
& ~ g_false_only(U_30,U_13)
& ( g_both(U_13,U_30)
| g_both(U_30,U_13) ) ) ) )
& g_true_only(U_30,U_22) )
| ! [U_12] :
( ? [U_11] :
( g_true_only(U_11,U_12)
& g_true_only(U_12,U_11) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ? [U_7] :
( g_true_only(U_7,U_29)
& g_true_only(U_29,U_7) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ? [U_5] :
( ~ g_false_only(U_5,U_29)
& ~ g_false_only(U_29,U_5) ) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ? [U_3] :
( ~ g_false_only(U_3,U_28)
& ~ g_false_only(U_28,U_3) ) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ? [U_1] :
( g_true_only(U_1,U_27)
& g_true_only(U_27,U_1) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_9,sK1)],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ? [U_30] :
( ( ? [U_15] :
( g_true_only(U_15,U_30)
& g_true_only(U_30,U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,U_30)
| ~ g_true_only(U_30,U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,U_30)
& ~ g_false_only(U_30,U_13)
& ( g_both(U_13,U_30)
| g_both(U_30,U_13) ) ) ) )
& g_true_only(U_30,U_22) )
| ! [U_12] :
( ? [U_11] :
( g_true_only(U_11,U_12)
& g_true_only(U_12,U_11) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ? [U_7] :
( g_true_only(U_7,U_29)
& g_true_only(U_29,U_7) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ? [U_5] :
( ~ g_false_only(U_5,U_29)
& ~ g_false_only(U_29,U_5) ) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ? [U_3] :
( ~ g_false_only(U_3,U_28)
& ~ g_false_only(U_28,U_3) ) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_1,sK2(U_27))],[f_1_5]) ).
fof(f_1_7,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ? [U_30] :
( ( ? [U_15] :
( g_true_only(U_15,U_30)
& g_true_only(U_30,U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,U_30)
| ~ g_true_only(U_30,U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,U_30)
& ~ g_false_only(U_30,U_13)
& ( g_both(U_13,U_30)
| g_both(U_30,U_13) ) ) ) )
& g_true_only(U_30,U_22) )
| ! [U_12] :
( ? [U_11] :
( g_true_only(U_11,U_12)
& g_true_only(U_12,U_11) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ? [U_7] :
( g_true_only(U_7,U_29)
& g_true_only(U_29,U_7) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ? [U_5] :
( ~ g_false_only(U_5,U_29)
& ~ g_false_only(U_29,U_5) ) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_3,sK3(U_28))],[f_1_6]) ).
fof(f_1_8,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ? [U_30] :
( ( ? [U_15] :
( g_true_only(U_15,U_30)
& g_true_only(U_30,U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,U_30)
| ~ g_true_only(U_30,U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,U_30)
& ~ g_false_only(U_30,U_13)
& ( g_both(U_13,U_30)
| g_both(U_30,U_13) ) ) ) )
& g_true_only(U_30,U_22) )
| ! [U_12] :
( ? [U_11] :
( g_true_only(U_11,U_12)
& g_true_only(U_12,U_11) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ? [U_7] :
( g_true_only(U_7,U_29)
& g_true_only(U_29,U_7) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_5,sK4(U_29))],[f_1_7]) ).
fof(f_1_9,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ? [U_30] :
( ( ? [U_15] :
( g_true_only(U_15,U_30)
& g_true_only(U_30,U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,U_30)
| ~ g_true_only(U_30,U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,U_30)
& ~ g_false_only(U_30,U_13)
& ( g_both(U_13,U_30)
| g_both(U_30,U_13) ) ) ) )
& g_true_only(U_30,U_22) )
| ! [U_12] :
( ? [U_11] :
( g_true_only(U_11,U_12)
& g_true_only(U_12,U_11) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_7,sK5(U_29))],[f_1_8]) ).
fof(f_1_10,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ? [U_30] :
( ( ? [U_15] :
( g_true_only(U_15,U_30)
& g_true_only(U_30,U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,U_30)
| ~ g_true_only(U_30,U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,U_30)
& ~ g_false_only(U_30,U_13)
& ( g_both(U_13,U_30)
| g_both(U_30,U_13) ) ) ) )
& g_true_only(U_30,U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_11,sK6(U_22,U_12))],[f_1_9]) ).
fof(f_1_11,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ( ( ? [U_15] :
( g_true_only(U_15,sK7(U_22))
& g_true_only(sK7(U_22),U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ? [U_13] :
( ~ g_false_only(U_13,sK7(U_22))
& ~ g_false_only(sK7(U_22),U_13)
& ( g_both(U_13,sK7(U_22))
| g_both(sK7(U_22),U_13) ) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_30,sK7(U_22))],[f_1_10]) ).
fof(f_1_12,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ( ( ? [U_15] :
( g_true_only(U_15,sK7(U_22))
& g_true_only(sK7(U_22),U_15) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ~ g_false_only(sK8(U_22),sK7(U_22))
& ~ g_false_only(sK7(U_22),sK8(U_22))
& ( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22)) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_13,sK8(U_22))],[f_1_11]) ).
fof(f_1_13,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ? [U_31] :
( ( ? [U_17] :
( g_true_only(U_17,U_31)
& g_true_only(U_31,U_17) )
| ! [U_16] :
( g_false_only(U_16,U_31)
| g_false_only(U_31,U_16) ) )
& g_both(U_31,U_22) )
| ( ( ( g_true_only(sK9(U_22),sK7(U_22))
& g_true_only(sK7(U_22),sK9(U_22)) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ~ g_false_only(sK8(U_22),sK7(U_22))
& ~ g_false_only(sK7(U_22),sK8(U_22))
& ( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22)) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_15,sK9(U_22))],[f_1_12]) ).
fof(f_1_14,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ( ( ? [U_17] :
( g_true_only(U_17,sK10(U_22))
& g_true_only(sK10(U_22),U_17) )
| ! [U_16] :
( g_false_only(U_16,sK10(U_22))
| g_false_only(sK10(U_22),U_16) ) )
& g_both(sK10(U_22),U_22) )
| ( ( ( g_true_only(sK9(U_22),sK7(U_22))
& g_true_only(sK7(U_22),sK9(U_22)) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ~ g_false_only(sK8(U_22),sK7(U_22))
& ~ g_false_only(sK7(U_22),sK8(U_22))
& ( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22)) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_31,sK10(U_22))],[f_1_13]) ).
fof(f_1_15,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ? [U_32] :
( ( ( ! [U_20] :
( ~ g_true_only(U_20,U_32)
| ~ g_true_only(U_32,U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,U_32)
& ~ g_false_only(U_32,U_19)
& ( g_both(U_19,U_32)
| g_both(U_32,U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,U_32)
| g_false_only(U_32,U_18) ) )
& g_false_only(U_32,U_22) )
| ( ( ( g_true_only(sK11(U_22),sK10(U_22))
& g_true_only(sK10(U_22),sK11(U_22)) )
| ! [U_16] :
( g_false_only(U_16,sK10(U_22))
| g_false_only(sK10(U_22),U_16) ) )
& g_both(sK10(U_22),U_22) )
| ( ( ( g_true_only(sK9(U_22),sK7(U_22))
& g_true_only(sK7(U_22),sK9(U_22)) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ~ g_false_only(sK8(U_22),sK7(U_22))
& ~ g_false_only(sK7(U_22),sK8(U_22))
& ( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22)) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_17,sK11(U_22))],[f_1_14]) ).
fof(f_1_16,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ( ( ( ! [U_20] :
( ~ g_true_only(U_20,sK12(U_22))
| ~ g_true_only(sK12(U_22),U_20) )
& ? [U_19] :
( ~ g_false_only(U_19,sK12(U_22))
& ~ g_false_only(sK12(U_22),U_19)
& ( g_both(U_19,sK12(U_22))
| g_both(sK12(U_22),U_19) ) ) )
| ! [U_18] :
( g_false_only(U_18,sK12(U_22))
| g_false_only(sK12(U_22),U_18) ) )
& g_false_only(sK12(U_22),U_22) )
| ( ( ( g_true_only(sK11(U_22),sK10(U_22))
& g_true_only(sK10(U_22),sK11(U_22)) )
| ! [U_16] :
( g_false_only(U_16,sK10(U_22))
| g_false_only(sK10(U_22),U_16) ) )
& g_both(sK10(U_22),U_22) )
| ( ( ( g_true_only(sK9(U_22),sK7(U_22))
& g_true_only(sK7(U_22),sK9(U_22)) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ~ g_false_only(sK8(U_22),sK7(U_22))
& ~ g_false_only(sK7(U_22),sK8(U_22))
& ( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22)) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_32,sK12(U_22))],[f_1_15]) ).
fof(f_1_17,negated_conjecture,
( ( ? [U_26] :
! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,U_26) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,U_26) ) )
| ! [U_22] :
( ( ( ( ! [U_20] :
( ~ g_true_only(U_20,sK12(U_22))
| ~ g_true_only(sK12(U_22),U_20) )
& ~ g_false_only(sK13(U_22),sK12(U_22))
& ~ g_false_only(sK12(U_22),sK13(U_22))
& ( g_both(sK13(U_22),sK12(U_22))
| g_both(sK12(U_22),sK13(U_22)) ) )
| ! [U_18] :
( g_false_only(U_18,sK12(U_22))
| g_false_only(sK12(U_22),U_18) ) )
& g_false_only(sK12(U_22),U_22) )
| ( ( ( g_true_only(sK11(U_22),sK10(U_22))
& g_true_only(sK10(U_22),sK11(U_22)) )
| ! [U_16] :
( g_false_only(U_16,sK10(U_22))
| g_false_only(sK10(U_22),U_16) ) )
& g_both(sK10(U_22),U_22) )
| ( ( ( g_true_only(sK9(U_22),sK7(U_22))
& g_true_only(sK7(U_22),sK9(U_22)) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ~ g_false_only(sK8(U_22),sK7(U_22))
& ~ g_false_only(sK7(U_22),sK8(U_22))
& ( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22)) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_19,sK13(U_22))],[f_1_16]) ).
fof(f_1_18,negated_conjecture,
( ( ! [U_25] :
( ( ? [U_24] :
( g_true_only(U_24,U_25)
& g_true_only(U_25,U_24) )
& g_false_only(U_25,sK14) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,sK14) ) )
| ! [U_22] :
( ( ( ( ! [U_20] :
( ~ g_true_only(U_20,sK12(U_22))
| ~ g_true_only(sK12(U_22),U_20) )
& ~ g_false_only(sK13(U_22),sK12(U_22))
& ~ g_false_only(sK12(U_22),sK13(U_22))
& ( g_both(sK13(U_22),sK12(U_22))
| g_both(sK12(U_22),sK13(U_22)) ) )
| ! [U_18] :
( g_false_only(U_18,sK12(U_22))
| g_false_only(sK12(U_22),U_18) ) )
& g_false_only(sK12(U_22),U_22) )
| ( ( ( g_true_only(sK11(U_22),sK10(U_22))
& g_true_only(sK10(U_22),sK11(U_22)) )
| ! [U_16] :
( g_false_only(U_16,sK10(U_22))
| g_false_only(sK10(U_22),U_16) ) )
& g_both(sK10(U_22),U_22) )
| ( ( ( g_true_only(sK9(U_22),sK7(U_22))
& g_true_only(sK7(U_22),sK9(U_22)) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ~ g_false_only(sK8(U_22),sK7(U_22))
& ~ g_false_only(sK7(U_22),sK8(U_22))
& ( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22)) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_26,sK14)],[f_1_17]) ).
fof(f_1_19,negated_conjecture,
( ( ! [U_25] :
( ( g_true_only(sK15(U_25),U_25)
& g_true_only(U_25,sK15(U_25))
& g_false_only(U_25,sK14) )
| ( ! [U_23] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23) )
& g_true_only(U_25,sK14) ) )
| ! [U_22] :
( ( ( ( ! [U_20] :
( ~ g_true_only(U_20,sK12(U_22))
| ~ g_true_only(sK12(U_22),U_20) )
& ~ g_false_only(sK13(U_22),sK12(U_22))
& ~ g_false_only(sK12(U_22),sK13(U_22))
& ( g_both(sK13(U_22),sK12(U_22))
| g_both(sK12(U_22),sK13(U_22)) ) )
| ! [U_18] :
( g_false_only(U_18,sK12(U_22))
| g_false_only(sK12(U_22),U_18) ) )
& g_false_only(sK12(U_22),U_22) )
| ( ( ( g_true_only(sK11(U_22),sK10(U_22))
& g_true_only(sK10(U_22),sK11(U_22)) )
| ! [U_16] :
( g_false_only(U_16,sK10(U_22))
| g_false_only(sK10(U_22),U_16) ) )
& g_both(sK10(U_22),U_22) )
| ( ( ( g_true_only(sK9(U_22),sK7(U_22))
& g_true_only(sK7(U_22),sK9(U_22)) )
| ( ! [U_14] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14) )
& ~ g_false_only(sK8(U_22),sK7(U_22))
& ~ g_false_only(sK7(U_22),sK8(U_22))
& ( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22)) ) ) )
& g_true_only(sK7(U_22),U_22) )
| ! [U_12] :
( ( g_true_only(sK6(U_22,U_12),U_12)
& g_true_only(U_12,sK6(U_22,U_12)) )
| ! [U_10] :
( g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| ( ~ g_both(U_10,U_12)
& ~ g_both(U_12,U_10) ) )
| ~ g_both(U_12,U_22) ) ) )
& ! [U_29] :
( ( ( ( g_true_only(sK5(U_29),U_29)
& g_true_only(U_29,sK5(U_29)) )
| ! [U_6] :
( g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| ( ~ g_both(U_6,U_29)
& ~ g_both(U_29,U_6) ) ) )
& ~ g_false_only(sK4(U_29),U_29)
& ~ g_false_only(U_29,sK4(U_29)) )
| ~ g_false_only(U_29,sK1) )
& ! [U_28] :
( ( ! [U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4) )
& ~ g_false_only(sK3(U_28),U_28)
& ~ g_false_only(U_28,sK3(U_28)) )
| ~ g_both(U_28,sK1) )
& ! [U_27] :
( ( ! [U_2] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2) )
& ( ( g_true_only(sK2(U_27),U_27)
& g_true_only(U_27,sK2(U_27)) )
| ! [U_0] :
( g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| ( ~ g_both(U_0,U_27)
& ~ g_both(U_27,U_0) ) ) ) )
| ~ g_true_only(U_27,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_24,sK15(U_25))],[f_1_18]) ).
fof(f_1_20,negated_conjecture,
( ! [U_25] :
( g_true_only(sK15(U_25),U_25)
| ~ sP17(U_25) )
& ! [U_25] :
( g_true_only(U_25,sK15(U_25))
| ~ sP17(U_25) )
& ! [U_25] :
( g_false_only(U_25,sK14)
| ~ sP17(U_25) )
& ! [U_23,U_25] :
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23)
| ~ sP16(U_23,U_25) )
& ! [U_23,U_25] :
( g_true_only(U_25,sK14)
| ~ sP16(U_23,U_25) )
& ! [U_20,U_22] :
( ~ g_true_only(U_20,sK12(U_22))
| ~ g_true_only(sK12(U_22),U_20)
| ~ sP14(U_20,U_22) )
& ! [U_20,U_22] :
( ~ g_false_only(sK13(U_22),sK12(U_22))
| ~ sP14(U_20,U_22) )
& ! [U_20,U_22] :
( ~ g_false_only(sK12(U_22),sK13(U_22))
| ~ sP14(U_20,U_22) )
& ! [U_20,U_22] :
( g_both(sK13(U_22),sK12(U_22))
| g_both(sK12(U_22),sK13(U_22))
| ~ sP14(U_20,U_22) )
& ! [U_20,U_18,U_22] :
( sP14(U_20,U_22)
| g_false_only(U_18,sK12(U_22))
| g_false_only(sK12(U_22),U_18)
| ~ sP15(U_20,U_18,U_22) )
& ! [U_20,U_18,U_22] :
( g_false_only(sK12(U_22),U_22)
| ~ sP15(U_20,U_18,U_22) )
& ! [U_22] :
( g_true_only(sK11(U_22),sK10(U_22))
| ~ sP12(U_22) )
& ! [U_22] :
( g_true_only(sK10(U_22),sK11(U_22))
| ~ sP12(U_22) )
& ! [U_16,U_22] :
( sP12(U_22)
| g_false_only(U_16,sK10(U_22))
| g_false_only(sK10(U_22),U_16)
| ~ sP13(U_16,U_22) )
& ! [U_16,U_22] :
( g_both(sK10(U_22),U_22)
| ~ sP13(U_16,U_22) )
& ! [U_22] :
( g_true_only(sK9(U_22),sK7(U_22))
| ~ sP10(U_22) )
& ! [U_22] :
( g_true_only(sK7(U_22),sK9(U_22))
| ~ sP10(U_22) )
& ! [U_14,U_22] :
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14)
| ~ sP9(U_14,U_22) )
& ! [U_14,U_22] :
( ~ g_false_only(sK8(U_22),sK7(U_22))
| ~ sP9(U_14,U_22) )
& ! [U_14,U_22] :
( ~ g_false_only(sK7(U_22),sK8(U_22))
| ~ sP9(U_14,U_22) )
& ! [U_14,U_22] :
( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22))
| ~ sP9(U_14,U_22) )
& ! [U_14,U_22] :
( sP10(U_22)
| sP9(U_14,U_22)
| ~ sP11(U_14,U_22) )
& ! [U_14,U_22] :
( g_true_only(sK7(U_22),U_22)
| ~ sP11(U_14,U_22) )
& ! [U_12,U_22] :
( g_true_only(sK6(U_22,U_12),U_12)
| ~ sP8(U_12,U_22) )
& ! [U_12,U_22] :
( g_true_only(U_12,sK6(U_22,U_12))
| ~ sP8(U_12,U_22) )
& ! [U_12,U_10] :
( ~ g_both(U_10,U_12)
| ~ sP7(U_12,U_10) )
& ! [U_12,U_10] :
( ~ g_both(U_12,U_10)
| ~ sP7(U_12,U_10) )
& ! [U_29] :
( g_true_only(sK5(U_29),U_29)
| ~ sP5(U_29) )
& ! [U_29] :
( g_true_only(U_29,sK5(U_29))
| ~ sP5(U_29) )
& ! [U_29,U_6] :
( ~ g_both(U_6,U_29)
| ~ sP4(U_29,U_6) )
& ! [U_29,U_6] :
( ~ g_both(U_29,U_6)
| ~ sP4(U_29,U_6) )
& ! [U_29,U_6] :
( sP5(U_29)
| g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| sP4(U_29,U_6)
| ~ sP6(U_29,U_6) )
& ! [U_29,U_6] :
( ~ g_false_only(sK4(U_29),U_29)
| ~ sP6(U_29,U_6) )
& ! [U_29,U_6] :
( ~ g_false_only(U_29,sK4(U_29))
| ~ sP6(U_29,U_6) )
& ! [U_28,U_4] :
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4)
| ~ sP3(U_28,U_4) )
& ! [U_28,U_4] :
( ~ g_false_only(sK3(U_28),U_28)
| ~ sP3(U_28,U_4) )
& ! [U_28,U_4] :
( ~ g_false_only(U_28,sK3(U_28))
| ~ sP3(U_28,U_4) )
& ! [U_27] :
( g_true_only(sK2(U_27),U_27)
| ~ sP1(U_27) )
& ! [U_27] :
( g_true_only(U_27,sK2(U_27))
| ~ sP1(U_27) )
& ! [U_0,U_27] :
( ~ g_both(U_0,U_27)
| ~ sP0(U_0,U_27) )
& ! [U_0,U_27] :
( ~ g_both(U_27,U_0)
| ~ sP0(U_0,U_27) )
& ! [U_2,U_0,U_27] :
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2)
| ~ sP2(U_2,U_0,U_27) )
& ! [U_2,U_0,U_27] :
( sP1(U_27)
| g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| sP0(U_0,U_27)
| ~ sP2(U_2,U_0,U_27) )
& ! [U_20,U_23,U_16,U_18,U_12,U_14,U_22,U_10,U_25] :
( sP17(U_25)
| sP16(U_23,U_25)
| sP15(U_20,U_18,U_22)
| sP13(U_16,U_22)
| sP11(U_14,U_22)
| sP8(U_12,U_22)
| g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| sP7(U_12,U_10)
| ~ g_both(U_12,U_22) )
& ! [U_29,U_6] :
( sP6(U_29,U_6)
| ~ g_false_only(U_29,sK1) )
& ! [U_28,U_4] :
( sP3(U_28,U_4)
| ~ g_both(U_28,sK1) )
& ! [U_2,U_0,U_27] :
( sP2(U_2,U_0,U_27)
| ~ g_true_only(U_27,sK1) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2,sP3,sP4,sP5,sP6,sP7,sP8,sP9,sP10,sP11,sP12,sP13,sP14,sP15,sP16,sP17])],[f_1_19]) ).
cnf(f_1_21,negated_conjecture,
( sP2(U_2,U_0,U_27)
| ~ g_true_only(U_27,sK1) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_22,negated_conjecture,
( sP3(U_28,U_4)
| ~ g_both(U_28,sK1) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_23,negated_conjecture,
( sP6(U_29,U_6)
| ~ g_false_only(U_29,sK1) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_24,negated_conjecture,
( sP17(U_25)
| sP16(U_23,U_25)
| sP15(U_20,U_18,U_22)
| sP13(U_16,U_22)
| sP11(U_14,U_22)
| sP8(U_12,U_22)
| g_false_only(U_10,U_12)
| g_false_only(U_12,U_10)
| sP7(U_12,U_10)
| ~ g_both(U_12,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_25,negated_conjecture,
( sP1(U_27)
| g_false_only(U_0,U_27)
| g_false_only(U_27,U_0)
| sP0(U_0,U_27)
| ~ sP2(U_2,U_0,U_27) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_26,negated_conjecture,
( ~ g_true_only(U_2,U_27)
| ~ g_true_only(U_27,U_2)
| ~ sP2(U_2,U_0,U_27) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_27,negated_conjecture,
( ~ g_both(U_27,U_0)
| ~ sP0(U_0,U_27) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_28,negated_conjecture,
( ~ g_both(U_0,U_27)
| ~ sP0(U_0,U_27) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_29,negated_conjecture,
( g_true_only(U_27,sK2(U_27))
| ~ sP1(U_27) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_30,negated_conjecture,
( g_true_only(sK2(U_27),U_27)
| ~ sP1(U_27) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_31,negated_conjecture,
( ~ g_false_only(U_28,sK3(U_28))
| ~ sP3(U_28,U_4) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_32,negated_conjecture,
( ~ g_false_only(sK3(U_28),U_28)
| ~ sP3(U_28,U_4) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_33,negated_conjecture,
( ~ g_true_only(U_4,U_28)
| ~ g_true_only(U_28,U_4)
| ~ sP3(U_28,U_4) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_34,negated_conjecture,
( ~ g_false_only(U_29,sK4(U_29))
| ~ sP6(U_29,U_6) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_35,negated_conjecture,
( ~ g_false_only(sK4(U_29),U_29)
| ~ sP6(U_29,U_6) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_36,negated_conjecture,
( sP5(U_29)
| g_false_only(U_6,U_29)
| g_false_only(U_29,U_6)
| sP4(U_29,U_6)
| ~ sP6(U_29,U_6) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_37,negated_conjecture,
( ~ g_both(U_29,U_6)
| ~ sP4(U_29,U_6) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_38,negated_conjecture,
( ~ g_both(U_6,U_29)
| ~ sP4(U_29,U_6) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_39,negated_conjecture,
( g_true_only(U_29,sK5(U_29))
| ~ sP5(U_29) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_40,negated_conjecture,
( g_true_only(sK5(U_29),U_29)
| ~ sP5(U_29) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_42,negated_conjecture,
( ~ g_both(U_10,U_12)
| ~ sP7(U_12,U_10) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_43,negated_conjecture,
( g_true_only(U_12,sK6(U_22,U_12))
| ~ sP8(U_12,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_44,negated_conjecture,
( g_true_only(sK6(U_22,U_12),U_12)
| ~ sP8(U_12,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_45,negated_conjecture,
( g_true_only(sK7(U_22),U_22)
| ~ sP11(U_14,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_46,negated_conjecture,
( sP10(U_22)
| sP9(U_14,U_22)
| ~ sP11(U_14,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_47,negated_conjecture,
( g_both(sK8(U_22),sK7(U_22))
| g_both(sK7(U_22),sK8(U_22))
| ~ sP9(U_14,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_48,negated_conjecture,
( ~ g_false_only(sK7(U_22),sK8(U_22))
| ~ sP9(U_14,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_49,negated_conjecture,
( ~ g_false_only(sK8(U_22),sK7(U_22))
| ~ sP9(U_14,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_50,negated_conjecture,
( ~ g_true_only(U_14,sK7(U_22))
| ~ g_true_only(sK7(U_22),U_14)
| ~ sP9(U_14,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_51,negated_conjecture,
( g_true_only(sK7(U_22),sK9(U_22))
| ~ sP10(U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_52,negated_conjecture,
( g_true_only(sK9(U_22),sK7(U_22))
| ~ sP10(U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_53,negated_conjecture,
( g_both(sK10(U_22),U_22)
| ~ sP13(U_16,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_54,negated_conjecture,
( sP12(U_22)
| g_false_only(U_16,sK10(U_22))
| g_false_only(sK10(U_22),U_16)
| ~ sP13(U_16,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_55,negated_conjecture,
( g_true_only(sK10(U_22),sK11(U_22))
| ~ sP12(U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_56,negated_conjecture,
( g_true_only(sK11(U_22),sK10(U_22))
| ~ sP12(U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_57,negated_conjecture,
( g_false_only(sK12(U_22),U_22)
| ~ sP15(U_20,U_18,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_58,negated_conjecture,
( sP14(U_20,U_22)
| g_false_only(U_18,sK12(U_22))
| g_false_only(sK12(U_22),U_18)
| ~ sP15(U_20,U_18,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_59,negated_conjecture,
( g_both(sK13(U_22),sK12(U_22))
| g_both(sK12(U_22),sK13(U_22))
| ~ sP14(U_20,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_60,negated_conjecture,
( ~ g_false_only(sK12(U_22),sK13(U_22))
| ~ sP14(U_20,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_61,negated_conjecture,
( ~ g_false_only(sK13(U_22),sK12(U_22))
| ~ sP14(U_20,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_62,negated_conjecture,
( ~ g_true_only(U_20,sK12(U_22))
| ~ g_true_only(sK12(U_22),U_20)
| ~ sP14(U_20,U_22) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_64,negated_conjecture,
( g_false_only(U_23,U_25)
| g_false_only(U_25,U_23)
| ~ sP16(U_23,U_25) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_66,negated_conjecture,
( g_true_only(U_25,sK15(U_25))
| ~ sP17(U_25) ),
inference(clausify,[status(thm)],[f_1_20]) ).
cnf(f_1_67,negated_conjecture,
( g_true_only(sK15(U_25),U_25)
| ~ sP17(U_25) ),
inference(clausify,[status(thm)],[f_1_20]) ).
fof(f_5_1,plain,
! [X_2,X_1] :
( g_false_only(X_2,X_1)
| g_both(X_2,X_1)
| g_true_only(X_2,X_1) ),
inference(fof_nnf,[status(thm)],[exhaustion_g]) ).
fof(f_5_2,plain,
! [U_52,U_51] :
( g_false_only(U_52,U_51)
| g_both(U_52,U_51)
| g_true_only(U_52,U_51) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_51,U_52] :
( g_false_only(U_52,U_51)
| g_both(U_52,U_51)
| g_true_only(U_52,U_51) ),
inference(definitional_conversion,[status(esa)],[f_5_2]) ).
cnf(f_5_4,plain,
( g_false_only(U_52,U_51)
| g_both(U_52,U_51)
| g_true_only(U_52,U_51) ),
inference(clausify,[status(thm)],[f_5_3]) ).
cnf(t1,plain,
( sP6(sK1,sK4(sK1))
| ~ g_false_only(sK1,sK1) ),
inference(start,[status(thm),parent(0:0)],[f_1_23]) ).
cnf(t2,plain,
( sP7(sK1,sK1)
| g_false_only(sK1,sK1)
| sP17(sK1)
| sP8(sK1,sK1)
| sP11(sK2(sK7(sK1)),sK1)
| sP13(sK3(sK10(sK1)),sK1)
| sP15(sK5(sK12(sK1)),sK4(sK12(sK1)),sK1)
| sP16(sK1,sK1)
| ~ g_both(sK1,sK1)
| g_false_only(sK1,sK1) ),
inference(extension,[status(thm),parent(t1:1)],[f_1_24]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( g_false_only(sK1,sK1)
| g_true_only(sK1,sK1)
| g_both(sK1,sK1) ),
inference(extension,[status(thm),parent(t2:2)],[f_5_4]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ g_true_only(sK1,sK1)
| ~ sP3(sK1,sK1)
| ~ g_true_only(sK1,sK1) ),
inference(extension,[status(thm),parent(t4:2)],[f_1_33]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( ~ g_both(sK1,sK1)
| sP3(sK1,sK1) ),
inference(extension,[status(thm),parent(t6:2)],[f_1_22]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( g_false_only(sK1,sK1)
| g_true_only(sK1,sK1)
| g_both(sK1,sK1) ),
inference(extension,[status(thm),parent(t8:2)],[f_5_4]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( ~ g_true_only(sK1,sK1)
| ~ sP2(sK1,U_705,sK1)
| ~ g_true_only(sK1,sK1) ),
inference(extension,[status(thm),parent(t10:2)],[f_1_26]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
( ~ g_true_only(sK1,sK1)
| sP2(sK1,U_705,sK1) ),
inference(extension,[status(thm),parent(t12:2)],[f_1_21]) ).
cnf(t15,plain,
$false,
inference(connection,[status(thm),parent(t14:1)],[t14:1,t12:2]) ).
cnf(t16,plain,
$false,
inference(reduction,[status(thm),parent(t14:2)],[t14:2,t10:2]) ).
cnf(t17,plain,
$false,
inference(reduction,[status(thm),parent(t12:3)],[t12:3,t10:2]) ).
cnf(t18,plain,
$false,
inference(reduction,[status(thm),parent(t10:3)],[t10:3,t1:1]) ).
cnf(t19,plain,
$false,
inference(reduction,[status(thm),parent(t6:3)],[t6:3,t4:2]) ).
cnf(t20,plain,
$false,
inference(reduction,[status(thm),parent(t4:3)],[t4:3,t1:1]) ).
cnf(l2,lemma,
g_both(sK1,sK1),
inference(lemma,[status(cth),parent(t2:2),below(t1:1)],[t2:2]) ).
cnf(t21,plain,
( g_false_only(sK1,sK1)
| g_false_only(sK1,sK1)
| ~ sP16(sK1,sK1) ),
inference(extension,[status(thm),parent(t2:3)],[f_1_64]) ).
cnf(t22,plain,
$false,
inference(connection,[status(thm),parent(t21:1)],[t21:1,t2:3]) ).
cnf(t23,plain,
$false,
inference(reduction,[status(thm),parent(t21:2)],[t21:2,t1:1]) ).
cnf(l14,lemma,
~ g_false_only(sK1,sK1),
inference(lemma,[status(cth),parent(t21:2),below(t2:3)],[t21:2]) ).
cnf(t24,plain,
~ g_false_only(sK1,sK1),
inference(lemma_extension,[status(thm),parent(t21:3)],[l14:1]) ).
cnf(t25,plain,
$false,
inference(connection,[status(thm),parent(t24:1)],[t24:1,t21:3]) ).
cnf(t26,plain,
( g_false_only(sK12(sK1),sK4(sK12(sK1)))
| g_false_only(sK4(sK12(sK1)),sK12(sK1))
| sP14(sK5(sK12(sK1)),sK1)
| ~ sP15(sK5(sK12(sK1)),sK4(sK12(sK1)),sK1) ),
inference(extension,[status(thm),parent(t2:4)],[f_1_58]) ).
cnf(t27,plain,
$false,
inference(connection,[status(thm),parent(t26:1)],[t26:1,t2:4]) ).
cnf(t28,plain,
( ~ g_false_only(sK13(sK1),sK12(sK1))
| ~ sP14(sK5(sK12(sK1)),sK1) ),
inference(extension,[status(thm),parent(t26:2)],[f_1_61]) ).
cnf(t29,plain,
$false,
inference(connection,[status(thm),parent(t28:1)],[t28:1,t26:2]) ).
cnf(t30,plain,
( sP4(sK12(sK1),sK13(sK1))
| g_false_only(sK12(sK1),sK13(sK1))
| sP5(sK12(sK1))
| ~ sP6(sK12(sK1),sK13(sK1))
| g_false_only(sK13(sK1),sK12(sK1)) ),
inference(extension,[status(thm),parent(t28:2)],[f_1_36]) ).
cnf(t31,plain,
$false,
inference(connection,[status(thm),parent(t30:1)],[t30:1,t28:2]) ).
cnf(t32,plain,
( ~ g_false_only(sK12(sK1),sK1)
| sP6(sK12(sK1),sK13(sK1)) ),
inference(extension,[status(thm),parent(t30:2)],[f_1_23]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t30:2]) ).
cnf(t34,plain,
( ~ sP15(sK5(sK12(sK1)),sK4(sK12(sK1)),sK1)
| g_false_only(sK12(sK1),sK1) ),
inference(extension,[status(thm),parent(t32:2)],[f_1_57]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t32:2]) ).
cnf(t36,plain,
$false,
inference(reduction,[status(thm),parent(t34:2)],[t34:2,t2:4]) ).
cnf(t37,plain,
( g_true_only(sK5(sK12(sK1)),sK12(sK1))
| ~ sP5(sK12(sK1)) ),
inference(extension,[status(thm),parent(t30:3)],[f_1_40]) ).
cnf(t38,plain,
$false,
inference(connection,[status(thm),parent(t37:1)],[t37:1,t30:3]) ).
cnf(t39,plain,
( ~ g_true_only(sK12(sK1),sK5(sK12(sK1)))
| ~ sP14(sK5(sK12(sK1)),sK1)
| ~ g_true_only(sK5(sK12(sK1)),sK12(sK1)) ),
inference(extension,[status(thm),parent(t37:2)],[f_1_62]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t37:2]) ).
cnf(t41,plain,
$false,
inference(reduction,[status(thm),parent(t39:2)],[t39:2,t26:2]) ).
cnf(t42,plain,
( ~ sP5(sK12(sK1))
| g_true_only(sK12(sK1),sK5(sK12(sK1))) ),
inference(extension,[status(thm),parent(t39:3)],[f_1_39]) ).
cnf(t43,plain,
$false,
inference(connection,[status(thm),parent(t42:1)],[t42:1,t39:3]) ).
cnf(t44,plain,
$false,
inference(reduction,[status(thm),parent(t42:2)],[t42:2,t30:3]) ).
cnf(t45,plain,
( ~ sP14(sK5(sK12(sK1)),sK1)
| ~ g_false_only(sK12(sK1),sK13(sK1)) ),
inference(extension,[status(thm),parent(t30:4)],[f_1_60]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t30:4]) ).
cnf(t47,plain,
$false,
inference(reduction,[status(thm),parent(t45:2)],[t45:2,t26:2]) ).
cnf(t48,plain,
( ~ g_both(sK13(sK1),sK12(sK1))
| ~ sP4(sK12(sK1),sK13(sK1)) ),
inference(extension,[status(thm),parent(t30:5)],[f_1_38]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t30:5]) ).
cnf(t50,plain,
( g_both(sK12(sK1),sK13(sK1))
| ~ sP14(sK5(sK12(sK1)),sK1)
| g_both(sK13(sK1),sK12(sK1)) ),
inference(extension,[status(thm),parent(t48:2)],[f_1_59]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t48:2]) ).
cnf(t52,plain,
$false,
inference(reduction,[status(thm),parent(t50:2)],[t50:2,t26:2]) ).
cnf(t53,plain,
( ~ sP4(sK12(sK1),sK13(sK1))
| ~ g_both(sK12(sK1),sK13(sK1)) ),
inference(extension,[status(thm),parent(t50:3)],[f_1_37]) ).
cnf(t54,plain,
$false,
inference(connection,[status(thm),parent(t53:1)],[t53:1,t50:3]) ).
cnf(t55,plain,
$false,
inference(reduction,[status(thm),parent(t53:2)],[t53:2,t30:5]) ).
cnf(t56,plain,
( ~ sP6(sK12(sK1),U_735)
| ~ g_false_only(sK4(sK12(sK1)),sK12(sK1)) ),
inference(extension,[status(thm),parent(t26:3)],[f_1_35]) ).
cnf(t57,plain,
$false,
inference(connection,[status(thm),parent(t56:1)],[t56:1,t26:3]) ).
cnf(t58,plain,
( ~ g_false_only(sK12(sK1),sK1)
| sP6(sK12(sK1),U_735) ),
inference(extension,[status(thm),parent(t56:2)],[f_1_23]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t56:2]) ).
cnf(t60,plain,
( ~ sP15(sK5(sK12(sK1)),sK4(sK12(sK1)),sK1)
| g_false_only(sK12(sK1),sK1) ),
inference(extension,[status(thm),parent(t58:2)],[f_1_57]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
$false,
inference(reduction,[status(thm),parent(t60:2)],[t60:2,t2:4]) ).
cnf(t63,plain,
( ~ sP6(sK12(sK1),U_742)
| ~ g_false_only(sK12(sK1),sK4(sK12(sK1))) ),
inference(extension,[status(thm),parent(t26:4)],[f_1_34]) ).
cnf(t64,plain,
$false,
inference(connection,[status(thm),parent(t63:1)],[t63:1,t26:4]) ).
cnf(t65,plain,
( ~ g_false_only(sK12(sK1),sK1)
| sP6(sK12(sK1),U_742) ),
inference(extension,[status(thm),parent(t63:2)],[f_1_23]) ).
cnf(t66,plain,
$false,
inference(connection,[status(thm),parent(t65:1)],[t65:1,t63:2]) ).
cnf(t67,plain,
( ~ sP15(sK5(sK12(sK1)),sK4(sK12(sK1)),sK1)
| g_false_only(sK12(sK1),sK1) ),
inference(extension,[status(thm),parent(t65:2)],[f_1_57]) ).
cnf(t68,plain,
$false,
inference(connection,[status(thm),parent(t67:1)],[t67:1,t65:2]) ).
cnf(t69,plain,
$false,
inference(reduction,[status(thm),parent(t67:2)],[t67:2,t2:4]) ).
cnf(t70,plain,
( g_false_only(sK10(sK1),sK3(sK10(sK1)))
| g_false_only(sK3(sK10(sK1)),sK10(sK1))
| sP12(sK1)
| ~ sP13(sK3(sK10(sK1)),sK1) ),
inference(extension,[status(thm),parent(t2:5)],[f_1_54]) ).
cnf(t71,plain,
$false,
inference(connection,[status(thm),parent(t70:1)],[t70:1,t2:5]) ).
cnf(t72,plain,
( g_true_only(sK11(sK1),sK10(sK1))
| ~ sP12(sK1) ),
inference(extension,[status(thm),parent(t70:2)],[f_1_56]) ).
cnf(t73,plain,
$false,
inference(connection,[status(thm),parent(t72:1)],[t72:1,t70:2]) ).
cnf(t74,plain,
( ~ g_true_only(sK10(sK1),sK11(sK1))
| ~ sP3(sK10(sK1),sK11(sK1))
| ~ g_true_only(sK11(sK1),sK10(sK1)) ),
inference(extension,[status(thm),parent(t72:2)],[f_1_33]) ).
cnf(t75,plain,
$false,
inference(connection,[status(thm),parent(t74:1)],[t74:1,t72:2]) ).
cnf(t76,plain,
( ~ g_both(sK10(sK1),sK1)
| sP3(sK10(sK1),sK11(sK1)) ),
inference(extension,[status(thm),parent(t74:2)],[f_1_22]) ).
cnf(t77,plain,
$false,
inference(connection,[status(thm),parent(t76:1)],[t76:1,t74:2]) ).
cnf(t78,plain,
( ~ sP13(sK3(sK10(sK1)),sK1)
| g_both(sK10(sK1),sK1) ),
inference(extension,[status(thm),parent(t76:2)],[f_1_53]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t76:2]) ).
cnf(t80,plain,
$false,
inference(reduction,[status(thm),parent(t78:2)],[t78:2,t2:5]) ).
cnf(t81,plain,
( ~ sP12(sK1)
| g_true_only(sK10(sK1),sK11(sK1)) ),
inference(extension,[status(thm),parent(t74:3)],[f_1_55]) ).
cnf(t82,plain,
$false,
inference(connection,[status(thm),parent(t81:1)],[t81:1,t74:3]) ).
cnf(t83,plain,
$false,
inference(reduction,[status(thm),parent(t81:2)],[t81:2,t70:2]) ).
cnf(t84,plain,
( ~ sP3(sK10(sK1),U_759)
| ~ g_false_only(sK3(sK10(sK1)),sK10(sK1)) ),
inference(extension,[status(thm),parent(t70:3)],[f_1_32]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t70:3]) ).
cnf(t86,plain,
( ~ g_both(sK10(sK1),sK1)
| sP3(sK10(sK1),U_759) ),
inference(extension,[status(thm),parent(t84:2)],[f_1_22]) ).
cnf(t87,plain,
$false,
inference(connection,[status(thm),parent(t86:1)],[t86:1,t84:2]) ).
cnf(t88,plain,
( ~ sP13(sK3(sK10(sK1)),sK1)
| g_both(sK10(sK1),sK1) ),
inference(extension,[status(thm),parent(t86:2)],[f_1_53]) ).
cnf(t89,plain,
$false,
inference(connection,[status(thm),parent(t88:1)],[t88:1,t86:2]) ).
cnf(t90,plain,
$false,
inference(reduction,[status(thm),parent(t88:2)],[t88:2,t2:5]) ).
cnf(t91,plain,
( ~ sP3(sK10(sK1),U_765)
| ~ g_false_only(sK10(sK1),sK3(sK10(sK1))) ),
inference(extension,[status(thm),parent(t70:4)],[f_1_31]) ).
cnf(t92,plain,
$false,
inference(connection,[status(thm),parent(t91:1)],[t91:1,t70:4]) ).
cnf(t93,plain,
( ~ g_both(sK10(sK1),sK1)
| sP3(sK10(sK1),U_765) ),
inference(extension,[status(thm),parent(t91:2)],[f_1_22]) ).
cnf(t94,plain,
$false,
inference(connection,[status(thm),parent(t93:1)],[t93:1,t91:2]) ).
cnf(t95,plain,
( ~ sP13(sK3(sK10(sK1)),sK1)
| g_both(sK10(sK1),sK1) ),
inference(extension,[status(thm),parent(t93:2)],[f_1_53]) ).
cnf(t96,plain,
$false,
inference(connection,[status(thm),parent(t95:1)],[t95:1,t93:2]) ).
cnf(t97,plain,
$false,
inference(reduction,[status(thm),parent(t95:2)],[t95:2,t2:5]) ).
cnf(t98,plain,
( sP9(sK2(sK7(sK1)),sK1)
| sP10(sK1)
| ~ sP11(sK2(sK7(sK1)),sK1) ),
inference(extension,[status(thm),parent(t2:6)],[f_1_46]) ).
cnf(t99,plain,
$false,
inference(connection,[status(thm),parent(t98:1)],[t98:1,t2:6]) ).
cnf(t100,plain,
( g_true_only(sK9(sK1),sK7(sK1))
| ~ sP10(sK1) ),
inference(extension,[status(thm),parent(t98:2)],[f_1_52]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t98:2]) ).
cnf(t102,plain,
( ~ g_true_only(sK7(sK1),sK9(sK1))
| ~ sP2(sK9(sK1),U_776,sK7(sK1))
| ~ g_true_only(sK9(sK1),sK7(sK1)) ),
inference(extension,[status(thm),parent(t100:2)],[f_1_26]) ).
cnf(t103,plain,
$false,
inference(connection,[status(thm),parent(t102:1)],[t102:1,t100:2]) ).
cnf(t104,plain,
( ~ g_true_only(sK7(sK1),sK1)
| sP2(sK9(sK1),U_776,sK7(sK1)) ),
inference(extension,[status(thm),parent(t102:2)],[f_1_21]) ).
cnf(t105,plain,
$false,
inference(connection,[status(thm),parent(t104:1)],[t104:1,t102:2]) ).
cnf(t106,plain,
( ~ sP11(sK2(sK7(sK1)),sK1)
| g_true_only(sK7(sK1),sK1) ),
inference(extension,[status(thm),parent(t104:2)],[f_1_45]) ).
cnf(t107,plain,
$false,
inference(connection,[status(thm),parent(t106:1)],[t106:1,t104:2]) ).
cnf(t108,plain,
$false,
inference(reduction,[status(thm),parent(t106:2)],[t106:2,t2:6]) ).
cnf(t109,plain,
( ~ sP10(sK1)
| g_true_only(sK7(sK1),sK9(sK1)) ),
inference(extension,[status(thm),parent(t102:3)],[f_1_51]) ).
cnf(t110,plain,
$false,
inference(connection,[status(thm),parent(t109:1)],[t109:1,t102:3]) ).
cnf(t111,plain,
$false,
inference(reduction,[status(thm),parent(t109:2)],[t109:2,t98:2]) ).
cnf(t112,plain,
( ~ g_false_only(sK8(sK1),sK7(sK1))
| ~ sP9(sK2(sK7(sK1)),sK1) ),
inference(extension,[status(thm),parent(t98:3)],[f_1_49]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t98:3]) ).
cnf(t114,plain,
( sP0(sK8(sK1),sK7(sK1))
| g_false_only(sK7(sK1),sK8(sK1))
| sP1(sK7(sK1))
| ~ sP2(U_786,sK8(sK1),sK7(sK1))
| g_false_only(sK8(sK1),sK7(sK1)) ),
inference(extension,[status(thm),parent(t112:2)],[f_1_25]) ).
cnf(t115,plain,
$false,
inference(connection,[status(thm),parent(t114:1)],[t114:1,t112:2]) ).
cnf(t116,plain,
( ~ g_true_only(sK7(sK1),sK1)
| sP2(U_786,sK8(sK1),sK7(sK1)) ),
inference(extension,[status(thm),parent(t114:2)],[f_1_21]) ).
cnf(t117,plain,
$false,
inference(connection,[status(thm),parent(t116:1)],[t116:1,t114:2]) ).
cnf(t118,plain,
( ~ sP11(sK2(sK7(sK1)),sK1)
| g_true_only(sK7(sK1),sK1) ),
inference(extension,[status(thm),parent(t116:2)],[f_1_45]) ).
cnf(t119,plain,
$false,
inference(connection,[status(thm),parent(t118:1)],[t118:1,t116:2]) ).
cnf(t120,plain,
$false,
inference(reduction,[status(thm),parent(t118:2)],[t118:2,t2:6]) ).
cnf(t121,plain,
( g_true_only(sK2(sK7(sK1)),sK7(sK1))
| ~ sP1(sK7(sK1)) ),
inference(extension,[status(thm),parent(t114:3)],[f_1_30]) ).
cnf(t122,plain,
$false,
inference(connection,[status(thm),parent(t121:1)],[t121:1,t114:3]) ).
cnf(t123,plain,
( ~ g_true_only(sK7(sK1),sK2(sK7(sK1)))
| ~ sP9(sK2(sK7(sK1)),sK1)
| ~ g_true_only(sK2(sK7(sK1)),sK7(sK1)) ),
inference(extension,[status(thm),parent(t121:2)],[f_1_50]) ).
cnf(t124,plain,
$false,
inference(connection,[status(thm),parent(t123:1)],[t123:1,t121:2]) ).
cnf(t125,plain,
$false,
inference(reduction,[status(thm),parent(t123:2)],[t123:2,t98:3]) ).
cnf(t126,plain,
( ~ sP1(sK7(sK1))
| g_true_only(sK7(sK1),sK2(sK7(sK1))) ),
inference(extension,[status(thm),parent(t123:3)],[f_1_29]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t123:3]) ).
cnf(t128,plain,
$false,
inference(reduction,[status(thm),parent(t126:2)],[t126:2,t114:3]) ).
cnf(t129,plain,
( ~ sP9(sK2(sK7(sK1)),sK1)
| ~ g_false_only(sK7(sK1),sK8(sK1)) ),
inference(extension,[status(thm),parent(t114:4)],[f_1_48]) ).
cnf(t130,plain,
$false,
inference(connection,[status(thm),parent(t129:1)],[t129:1,t114:4]) ).
cnf(t131,plain,
$false,
inference(reduction,[status(thm),parent(t129:2)],[t129:2,t98:3]) ).
cnf(t132,plain,
( ~ g_both(sK8(sK1),sK7(sK1))
| ~ sP0(sK8(sK1),sK7(sK1)) ),
inference(extension,[status(thm),parent(t114:5)],[f_1_28]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t114:5]) ).
cnf(t134,plain,
( g_both(sK7(sK1),sK8(sK1))
| ~ sP9(sK2(sK7(sK1)),sK1)
| g_both(sK8(sK1),sK7(sK1)) ),
inference(extension,[status(thm),parent(t132:2)],[f_1_47]) ).
cnf(t135,plain,
$false,
inference(connection,[status(thm),parent(t134:1)],[t134:1,t132:2]) ).
cnf(t136,plain,
$false,
inference(reduction,[status(thm),parent(t134:2)],[t134:2,t98:3]) ).
cnf(t137,plain,
( ~ sP0(sK8(sK1),sK7(sK1))
| ~ g_both(sK7(sK1),sK8(sK1)) ),
inference(extension,[status(thm),parent(t134:3)],[f_1_27]) ).
cnf(t138,plain,
$false,
inference(connection,[status(thm),parent(t137:1)],[t137:1,t134:3]) ).
cnf(t139,plain,
$false,
inference(reduction,[status(thm),parent(t137:2)],[t137:2,t114:5]) ).
cnf(t140,plain,
( g_true_only(sK6(sK1,sK1),sK1)
| ~ sP8(sK1,sK1) ),
inference(extension,[status(thm),parent(t2:7)],[f_1_44]) ).
cnf(t141,plain,
$false,
inference(connection,[status(thm),parent(t140:1)],[t140:1,t2:7]) ).
cnf(t142,plain,
( ~ g_true_only(sK1,sK6(sK1,sK1))
| ~ sP3(sK1,sK6(sK1,sK1))
| ~ g_true_only(sK6(sK1,sK1),sK1) ),
inference(extension,[status(thm),parent(t140:2)],[f_1_33]) ).
cnf(t143,plain,
$false,
inference(connection,[status(thm),parent(t142:1)],[t142:1,t140:2]) ).
cnf(t144,plain,
( ~ g_both(sK1,sK1)
| sP3(sK1,sK6(sK1,sK1)) ),
inference(extension,[status(thm),parent(t142:2)],[f_1_22]) ).
cnf(t145,plain,
$false,
inference(connection,[status(thm),parent(t144:1)],[t144:1,t142:2]) ).
cnf(t146,plain,
g_both(sK1,sK1),
inference(lemma_extension,[status(thm),parent(t144:2)],[l2:1]) ).
cnf(t147,plain,
$false,
inference(connection,[status(thm),parent(t146:1)],[t146:1,t144:2]) ).
cnf(t148,plain,
( ~ sP8(sK1,sK1)
| g_true_only(sK1,sK6(sK1,sK1)) ),
inference(extension,[status(thm),parent(t142:3)],[f_1_43]) ).
cnf(t149,plain,
$false,
inference(connection,[status(thm),parent(t148:1)],[t148:1,t142:3]) ).
cnf(t150,plain,
$false,
inference(reduction,[status(thm),parent(t148:2)],[t148:2,t2:7]) ).
cnf(t151,plain,
( g_true_only(sK15(sK1),sK1)
| ~ sP17(sK1) ),
inference(extension,[status(thm),parent(t2:8)],[f_1_67]) ).
cnf(t152,plain,
$false,
inference(connection,[status(thm),parent(t151:1)],[t151:1,t2:8]) ).
cnf(t153,plain,
( ~ g_true_only(sK1,sK15(sK1))
| ~ sP3(sK1,sK15(sK1))
| ~ g_true_only(sK15(sK1),sK1) ),
inference(extension,[status(thm),parent(t151:2)],[f_1_33]) ).
cnf(t154,plain,
$false,
inference(connection,[status(thm),parent(t153:1)],[t153:1,t151:2]) ).
cnf(t155,plain,
( ~ g_both(sK1,sK1)
| sP3(sK1,sK15(sK1)) ),
inference(extension,[status(thm),parent(t153:2)],[f_1_22]) ).
cnf(t156,plain,
$false,
inference(connection,[status(thm),parent(t155:1)],[t155:1,t153:2]) ).
cnf(t157,plain,
g_both(sK1,sK1),
inference(lemma_extension,[status(thm),parent(t155:2)],[l2:1]) ).
cnf(t158,plain,
$false,
inference(connection,[status(thm),parent(t157:1)],[t157:1,t155:2]) ).
cnf(t159,plain,
( ~ sP17(sK1)
| g_true_only(sK1,sK15(sK1)) ),
inference(extension,[status(thm),parent(t153:3)],[f_1_66]) ).
cnf(t160,plain,
$false,
inference(connection,[status(thm),parent(t159:1)],[t159:1,t153:3]) ).
cnf(t161,plain,
$false,
inference(reduction,[status(thm),parent(t159:2)],[t159:2,t2:8]) ).
cnf(t162,plain,
$false,
inference(reduction,[status(thm),parent(t2:9)],[t2:9,t1:1]) ).
cnf(t163,plain,
( ~ g_both(sK1,sK1)
| ~ sP7(sK1,sK1) ),
inference(extension,[status(thm),parent(t2:10)],[f_1_42]) ).
cnf(t164,plain,
$false,
inference(connection,[status(thm),parent(t163:1)],[t163:1,t2:10]) ).
cnf(t165,plain,
g_both(sK1,sK1),
inference(lemma_extension,[status(thm),parent(t163:2)],[l2:1]) ).
cnf(t166,plain,
$false,
inference(connection,[status(thm),parent(t165:1)],[t165:1,t163:2]) ).
cnf(t167,plain,
( sP4(sK1,sK4(sK1))
| g_false_only(sK1,sK4(sK1))
| g_false_only(sK4(sK1),sK1)
| sP5(sK1)
| ~ sP6(sK1,sK4(sK1)) ),
inference(extension,[status(thm),parent(t1:2)],[f_1_36]) ).
cnf(t168,plain,
$false,
inference(connection,[status(thm),parent(t167:1)],[t167:1,t1:2]) ).
cnf(t169,plain,
( g_true_only(sK5(sK1),sK1)
| ~ sP5(sK1) ),
inference(extension,[status(thm),parent(t167:2)],[f_1_40]) ).
cnf(t170,plain,
$false,
inference(connection,[status(thm),parent(t169:1)],[t169:1,t167:2]) ).
cnf(t171,plain,
( ~ g_true_only(sK1,sK5(sK1))
| ~ sP2(sK1,U_826,sK5(sK1))
| ~ g_true_only(sK5(sK1),sK1) ),
inference(extension,[status(thm),parent(t169:2)],[f_1_26]) ).
cnf(t172,plain,
$false,
inference(connection,[status(thm),parent(t171:1)],[t171:1,t169:2]) ).
cnf(t173,plain,
( ~ g_true_only(sK5(sK1),sK1)
| sP2(sK1,U_826,sK5(sK1)) ),
inference(extension,[status(thm),parent(t171:2)],[f_1_21]) ).
cnf(t174,plain,
$false,
inference(connection,[status(thm),parent(t173:1)],[t173:1,t171:2]) ).
cnf(t175,plain,
$false,
inference(reduction,[status(thm),parent(t173:2)],[t173:2,t169:2]) ).
cnf(t176,plain,
( ~ sP5(sK1)
| g_true_only(sK1,sK5(sK1)) ),
inference(extension,[status(thm),parent(t171:3)],[f_1_39]) ).
cnf(t177,plain,
$false,
inference(connection,[status(thm),parent(t176:1)],[t176:1,t171:3]) ).
cnf(t178,plain,
$false,
inference(reduction,[status(thm),parent(t176:2)],[t176:2,t167:2]) ).
cnf(t179,plain,
( ~ sP6(sK1,sK4(sK1))
| ~ g_false_only(sK4(sK1),sK1) ),
inference(extension,[status(thm),parent(t167:3)],[f_1_35]) ).
cnf(t180,plain,
$false,
inference(connection,[status(thm),parent(t179:1)],[t179:1,t167:3]) ).
cnf(t181,plain,
$false,
inference(reduction,[status(thm),parent(t179:2)],[t179:2,t1:2]) ).
cnf(l101,lemma,
~ g_false_only(sK4(sK1),sK1),
inference(lemma,[status(cth),parent(t167:3),below(t1:2)],[t167:3]) ).
cnf(t182,plain,
( ~ sP6(sK1,sK4(sK1))
| ~ g_false_only(sK1,sK4(sK1)) ),
inference(extension,[status(thm),parent(t167:4)],[f_1_34]) ).
cnf(t183,plain,
$false,
inference(connection,[status(thm),parent(t182:1)],[t182:1,t167:4]) ).
cnf(t184,plain,
$false,
inference(reduction,[status(thm),parent(t182:2)],[t182:2,t1:2]) ).
cnf(l103,lemma,
~ g_false_only(sK1,sK4(sK1)),
inference(lemma,[status(cth),parent(t167:4),below(t1:2)],[t167:4]) ).
cnf(t185,plain,
( ~ g_both(sK4(sK1),sK1)
| ~ sP4(sK1,sK4(sK1)) ),
inference(extension,[status(thm),parent(t167:5)],[f_1_38]) ).
cnf(t186,plain,
$false,
inference(connection,[status(thm),parent(t185:1)],[t185:1,t167:5]) ).
cnf(t187,plain,
( g_false_only(sK4(sK1),sK1)
| g_true_only(sK4(sK1),sK1)
| g_both(sK4(sK1),sK1) ),
inference(extension,[status(thm),parent(t185:2)],[f_5_4]) ).
cnf(t188,plain,
$false,
inference(connection,[status(thm),parent(t187:1)],[t187:1,t185:2]) ).
cnf(t189,plain,
( ~ g_true_only(sK1,sK4(sK1))
| ~ sP2(sK1,U_841,sK4(sK1))
| ~ g_true_only(sK4(sK1),sK1) ),
inference(extension,[status(thm),parent(t187:2)],[f_1_26]) ).
cnf(t190,plain,
$false,
inference(connection,[status(thm),parent(t189:1)],[t189:1,t187:2]) ).
cnf(t191,plain,
( ~ g_true_only(sK4(sK1),sK1)
| sP2(sK1,U_841,sK4(sK1)) ),
inference(extension,[status(thm),parent(t189:2)],[f_1_21]) ).
cnf(t192,plain,
$false,
inference(connection,[status(thm),parent(t191:1)],[t191:1,t189:2]) ).
cnf(t193,plain,
$false,
inference(reduction,[status(thm),parent(t191:2)],[t191:2,t187:2]) ).
cnf(t194,plain,
( g_both(sK1,sK4(sK1))
| g_false_only(sK1,sK4(sK1))
| g_true_only(sK1,sK4(sK1)) ),
inference(extension,[status(thm),parent(t189:3)],[f_5_4]) ).
cnf(t195,plain,
$false,
inference(connection,[status(thm),parent(t194:1)],[t194:1,t189:3]) ).
cnf(t196,plain,
~ g_false_only(sK1,sK4(sK1)),
inference(lemma_extension,[status(thm),parent(t194:2)],[l103:1]) ).
cnf(t197,plain,
$false,
inference(connection,[status(thm),parent(t196:1)],[t196:1,t194:2]) ).
cnf(t198,plain,
( ~ sP4(sK1,sK4(sK1))
| ~ g_both(sK1,sK4(sK1)) ),
inference(extension,[status(thm),parent(t194:3)],[f_1_37]) ).
cnf(t199,plain,
$false,
inference(connection,[status(thm),parent(t198:1)],[t198:1,t194:3]) ).
cnf(t200,plain,
$false,
inference(reduction,[status(thm),parent(t198:2)],[t198:2,t167:5]) ).
cnf(t201,plain,
~ g_false_only(sK4(sK1),sK1),
inference(lemma_extension,[status(thm),parent(t187:3)],[l101:1]) ).
cnf(t202,plain,
$false,
inference(connection,[status(thm),parent(t201:1)],[t201:1,t187:3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO604+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.54 % Computer : n007.cluster.edu
% 0.12/0.54 % Model : x86_64 x86_64
% 0.12/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.54 % Memory : 8046.5625MB
% 0.12/0.54 % OS : Linux 6.8.0-71-generic
% 0.12/0.54 % CPULimit : 300
% 0.12/0.54 % WCLimit : 300
% 0.12/0.54 % DateTime : Sun Sep 20 07:34:21 UTC 2026
% 0.12/0.54 % CPUTime :
% 48.09/48.56 % SZS status Theorem for theBenchmark
% 48.09/48.56 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------