%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SYO605+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 : n002.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 26.54s 31.86s
% Output : Proof 26.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 5
% Syntax : Number of formulae : 321 ( 140 unt; 0 def)
% Number of atoms : 1757 ( 0 equ)
% Maximal formula atoms : 114 ( 5 avg)
% Number of connectives : 2100 ( 664 ~; 889 |; 544 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 48 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-2 aty)
% Number of variables : 592 ( 0 sgn 364 !; 149 ?)
% Comments :
%------------------------------------------------------------------------------
fof(nc4,conjecture,
( ( ~ ? [B] :
! [A] :
? [C] :
( ( ( g_both(C,B)
| g_false_only(C,B) )
& g_false_only(C,A) )
| ( ( g_true_only(C,B)
| g_false_only(C,B) )
& g_both(C,A) )
| ( ( g_true_only(C,B)
| g_both(C,B) )
& g_true_only(C,A) ) )
& ? [B] :
( ~ ? [A] :
! [C] :
( ( g_true_only(C,B)
& g_false_only(C,A) )
| ( g_false_only(C,B)
& g_true_only(C,A) ) )
& ? [A] :
( ~ ? [C] :
( ( ( g_both(C,B)
| g_false_only(C,B) )
& g_false_only(C,A) )
| ( ( g_true_only(C,B)
| g_false_only(C,B) )
& g_both(C,A) )
| ( ( g_true_only(C,B)
| g_both(C,B) )
& g_true_only(C,A) ) )
& ? [C] :
( g_both(C,B)
& g_both(C,A) ) ) )
& ~ ? [A] :
! [B] :
( ( g_false_only(B,B)
& g_false_only(B,A) )
| ( g_true_only(B,B)
& g_true_only(B,A) ) )
& ? [A] :
( ~ ? [B] :
( ( ( g_both(B,B)
| g_true_only(B,B) )
& g_false_only(B,A) )
| ( ( g_false_only(B,B)
| g_true_only(B,B) )
& g_both(B,A) )
| ( ( g_false_only(B,B)
| g_both(B,B) )
& g_true_only(B,A) ) )
& ? [B] :
( g_both(B,B)
& g_both(B,A) ) ) )
| ? [B] :
! [A] :
? [C] :
( ( ( g_both(C,B)
| g_false_only(C,B) )
& g_false_only(C,A) )
| ( ( g_true_only(C,B)
| g_false_only(C,B) )
& g_both(C,A) )
| ( ( g_true_only(C,B)
| g_both(C,B) )
& g_true_only(C,A) ) )
| ! [A] :
? [B] :
( ( ( g_both(B,B)
| g_true_only(B,B) )
& g_false_only(B,A) )
| ( ( g_false_only(B,B)
| g_true_only(B,B) )
& g_both(B,A) )
| ( ( g_false_only(B,B)
| g_both(B,B) )
& g_true_only(B,A) ) ) ),
file('theBenchmark.p',nc4) ).
fof(true_only_g,axiom,
! [X_2,X_1] :
( g_true_only(X_2,X_1)
<=> ( ~ g_false(X_2,X_1)
& g_true(X_2,X_1) ) ),
file('theBenchmark.p',true_only_g) ).
fof(both_g,axiom,
! [X_2,X_1] :
( g_both(X_2,X_1)
<=> ( g_false(X_2,X_1)
& g_true(X_2,X_1) ) ),
file('theBenchmark.p',both_g) ).
fof(false_only_g,axiom,
! [X_2,X_1] :
( g_false_only(X_2,X_1)
<=> ( ~ g_true(X_2,X_1)
& g_false(X_2,X_1) ) ),
file('theBenchmark.p',false_only_g) ).
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,
~ ( ( ~ ? [B] :
! [A] :
? [C] :
( ( ( g_both(C,B)
| g_false_only(C,B) )
& g_false_only(C,A) )
| ( ( g_true_only(C,B)
| g_false_only(C,B) )
& g_both(C,A) )
| ( ( g_true_only(C,B)
| g_both(C,B) )
& g_true_only(C,A) ) )
& ? [B] :
( ~ ? [A] :
! [C] :
( ( g_true_only(C,B)
& g_false_only(C,A) )
| ( g_false_only(C,B)
& g_true_only(C,A) ) )
& ? [A] :
( ~ ? [C] :
( ( ( g_both(C,B)
| g_false_only(C,B) )
& g_false_only(C,A) )
| ( ( g_true_only(C,B)
| g_false_only(C,B) )
& g_both(C,A) )
| ( ( g_true_only(C,B)
| g_both(C,B) )
& g_true_only(C,A) ) )
& ? [C] :
( g_both(C,B)
& g_both(C,A) ) ) )
& ~ ? [A] :
! [B] :
( ( g_false_only(B,B)
& g_false_only(B,A) )
| ( g_true_only(B,B)
& g_true_only(B,A) ) )
& ? [A] :
( ~ ? [B] :
( ( ( g_both(B,B)
| g_true_only(B,B) )
& g_false_only(B,A) )
| ( ( g_false_only(B,B)
| g_true_only(B,B) )
& g_both(B,A) )
| ( ( g_false_only(B,B)
| g_both(B,B) )
& g_true_only(B,A) ) )
& ? [B] :
( g_both(B,B)
& g_both(B,A) ) ) )
| ? [B] :
! [A] :
? [C] :
( ( ( g_both(C,B)
| g_false_only(C,B) )
& g_false_only(C,A) )
| ( ( g_true_only(C,B)
| g_false_only(C,B) )
& g_both(C,A) )
| ( ( g_true_only(C,B)
| g_both(C,B) )
& g_true_only(C,A) ) )
| ! [A] :
? [B] :
( ( ( g_both(B,B)
| g_true_only(B,B) )
& g_false_only(B,A) )
| ( ( g_false_only(B,B)
| g_true_only(B,B) )
& g_both(B,A) )
| ( ( g_false_only(B,B)
| g_both(B,B) )
& g_true_only(B,A) ) ) ),
inference(negate,[status(cth)],[nc4]) ).
fof(f_1_2,negated_conjecture,
( ( ? [B] :
! [A] :
? [C] :
( ( ( g_both(C,B)
| g_false_only(C,B) )
& g_false_only(C,A) )
| ( ( g_true_only(C,B)
| g_false_only(C,B) )
& g_both(C,A) )
| ( ( g_true_only(C,B)
| g_both(C,B) )
& g_true_only(C,A) ) )
| ! [B] :
( ? [A] :
! [C] :
( ( g_true_only(C,B)
& g_false_only(C,A) )
| ( g_false_only(C,B)
& g_true_only(C,A) ) )
| ! [A] :
( ? [C] :
( ( ( g_both(C,B)
| g_false_only(C,B) )
& g_false_only(C,A) )
| ( ( g_true_only(C,B)
| g_false_only(C,B) )
& g_both(C,A) )
| ( ( g_true_only(C,B)
| g_both(C,B) )
& g_true_only(C,A) ) )
| ! [C] :
( ~ g_both(C,B)
| ~ g_both(C,A) ) ) )
| ? [A] :
! [B] :
( ( g_false_only(B,B)
& g_false_only(B,A) )
| ( g_true_only(B,B)
& g_true_only(B,A) ) )
| ! [A] :
( ? [B] :
( ( ( g_both(B,B)
| g_true_only(B,B) )
& g_false_only(B,A) )
| ( ( g_false_only(B,B)
| g_true_only(B,B) )
& g_both(B,A) )
| ( ( g_false_only(B,B)
| g_both(B,B) )
& g_true_only(B,A) ) )
| ! [B] :
( ~ g_both(B,B)
| ~ g_both(B,A) ) ) )
& ! [B] :
? [A] :
! [C] :
( ( ( ~ g_both(C,B)
& ~ g_false_only(C,B) )
| ~ g_false_only(C,A) )
& ( ( ~ g_true_only(C,B)
& ~ g_false_only(C,B) )
| ~ g_both(C,A) )
& ( ( ~ g_true_only(C,B)
& ~ g_both(C,B) )
| ~ g_true_only(C,A) ) )
& ? [A] :
! [B] :
( ( ( ~ g_both(B,B)
& ~ g_true_only(B,B) )
| ~ g_false_only(B,A) )
& ( ( ~ g_false_only(B,B)
& ~ g_true_only(B,B) )
| ~ g_both(B,A) )
& ( ( ~ g_false_only(B,B)
& ~ g_both(B,B) )
| ~ g_true_only(B,A) ) ) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
? [U_16] :
( ( ( g_both(U_16,U_18)
| g_false_only(U_16,U_18) )
& g_false_only(U_16,U_17) )
| ( ( g_true_only(U_16,U_18)
| g_false_only(U_16,U_18) )
& g_both(U_16,U_17) )
| ( ( g_true_only(U_16,U_18)
| g_both(U_16,U_18) )
& g_true_only(U_16,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_11] :
( ( ( g_both(U_11,U_15)
| g_false_only(U_11,U_15) )
& g_false_only(U_11,U_12) )
| ( ( g_true_only(U_11,U_15)
| g_false_only(U_11,U_15) )
& g_both(U_11,U_12) )
| ( ( g_true_only(U_11,U_15)
| g_both(U_11,U_15) )
& g_true_only(U_11,U_12) ) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ? [U_9] :
! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,U_9) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,U_9) ) )
| ! [U_7] :
( ? [U_6] :
( ( ( g_both(U_6,U_6)
| g_true_only(U_6,U_6) )
& g_false_only(U_6,U_7) )
| ( ( g_false_only(U_6,U_6)
| g_true_only(U_6,U_6) )
& g_both(U_6,U_7) )
| ( ( g_false_only(U_6,U_6)
| g_both(U_6,U_6) )
& g_true_only(U_6,U_7) ) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
? [U_3] :
! [U_2] :
( ( ( ~ g_both(U_2,U_4)
& ~ g_false_only(U_2,U_4) )
| ~ g_false_only(U_2,U_3) )
& ( ( ~ g_true_only(U_2,U_4)
& ~ g_false_only(U_2,U_4) )
| ~ g_both(U_2,U_3) )
& ( ( ~ g_true_only(U_2,U_4)
& ~ g_both(U_2,U_4) )
| ~ g_true_only(U_2,U_3) ) )
& ? [U_1] :
! [U_0] :
( ( ( ~ g_both(U_0,U_0)
& ~ g_true_only(U_0,U_0) )
| ~ g_false_only(U_0,U_1) )
& ( ( ~ g_false_only(U_0,U_0)
& ~ g_true_only(U_0,U_0) )
| ~ g_both(U_0,U_1) )
& ( ( ~ g_false_only(U_0,U_0)
& ~ g_both(U_0,U_0) )
| ~ g_true_only(U_0,U_1) ) ) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ? [U_29] :
( ( g_true_only(U_29,U_15)
| g_false_only(U_29,U_15) )
& g_both(U_29,U_12) )
| ? [U_28] :
( ( g_true_only(U_28,U_15)
| g_both(U_28,U_15) )
& g_true_only(U_28,U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ? [U_9] :
! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,U_9) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,U_9) ) )
| ! [U_7] :
( ? [U_27] :
( ( g_both(U_27,U_27)
| g_true_only(U_27,U_27) )
& g_false_only(U_27,U_7) )
| ? [U_26] :
( ( g_false_only(U_26,U_26)
| g_true_only(U_26,U_26) )
& g_both(U_26,U_7) )
| ? [U_25] :
( ( g_false_only(U_25,U_25)
| g_both(U_25,U_25) )
& g_true_only(U_25,U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
? [U_3] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,U_3) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,U_3) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,U_3) ) )
& ? [U_1] :
( ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,U_1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,U_1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,U_1) ) ) ),
inference(miniscope,[status(thm)],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ? [U_29] :
( ( g_true_only(U_29,U_15)
| g_false_only(U_29,U_15) )
& g_both(U_29,U_12) )
| ? [U_28] :
( ( g_true_only(U_28,U_15)
| g_both(U_28,U_15) )
& g_true_only(U_28,U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ? [U_9] :
! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,U_9) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,U_9) ) )
| ! [U_7] :
( ? [U_27] :
( ( g_both(U_27,U_27)
| g_true_only(U_27,U_27) )
& g_false_only(U_27,U_7) )
| ? [U_26] :
( ( g_false_only(U_26,U_26)
| g_true_only(U_26,U_26) )
& g_both(U_26,U_7) )
| ? [U_25] :
( ( g_false_only(U_25,U_25)
| g_both(U_25,U_25) )
& g_true_only(U_25,U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
? [U_3] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,U_3) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,U_3) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,U_3) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_1,sK1)],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ? [U_29] :
( ( g_true_only(U_29,U_15)
| g_false_only(U_29,U_15) )
& g_both(U_29,U_12) )
| ? [U_28] :
( ( g_true_only(U_28,U_15)
| g_both(U_28,U_15) )
& g_true_only(U_28,U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ? [U_9] :
! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,U_9) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,U_9) ) )
| ! [U_7] :
( ? [U_27] :
( ( g_both(U_27,U_27)
| g_true_only(U_27,U_27) )
& g_false_only(U_27,U_7) )
| ? [U_26] :
( ( g_false_only(U_26,U_26)
| g_true_only(U_26,U_26) )
& g_both(U_26,U_7) )
| ? [U_25] :
( ( g_false_only(U_25,U_25)
| g_both(U_25,U_25) )
& g_true_only(U_25,U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_3,sK2(U_4))],[f_1_5]) ).
fof(f_1_7,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ? [U_29] :
( ( g_true_only(U_29,U_15)
| g_false_only(U_29,U_15) )
& g_both(U_29,U_12) )
| ? [U_28] :
( ( g_true_only(U_28,U_15)
| g_both(U_28,U_15) )
& g_true_only(U_28,U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ? [U_9] :
! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,U_9) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,U_9) ) )
| ! [U_7] :
( ? [U_27] :
( ( g_both(U_27,U_27)
| g_true_only(U_27,U_27) )
& g_false_only(U_27,U_7) )
| ? [U_26] :
( ( g_false_only(U_26,U_26)
| g_true_only(U_26,U_26) )
& g_both(U_26,U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_25,sK3(U_7))],[f_1_6]) ).
fof(f_1_8,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ? [U_29] :
( ( g_true_only(U_29,U_15)
| g_false_only(U_29,U_15) )
& g_both(U_29,U_12) )
| ? [U_28] :
( ( g_true_only(U_28,U_15)
| g_both(U_28,U_15) )
& g_true_only(U_28,U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ? [U_9] :
! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,U_9) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,U_9) ) )
| ! [U_7] :
( ? [U_27] :
( ( g_both(U_27,U_27)
| g_true_only(U_27,U_27) )
& g_false_only(U_27,U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_26,sK4(U_7))],[f_1_7]) ).
fof(f_1_9,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ? [U_29] :
( ( g_true_only(U_29,U_15)
| g_false_only(U_29,U_15) )
& g_both(U_29,U_12) )
| ? [U_28] :
( ( g_true_only(U_28,U_15)
| g_both(U_28,U_15) )
& g_true_only(U_28,U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ? [U_9] :
! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,U_9) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,U_9) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_27,sK5(U_7))],[f_1_8]) ).
fof(f_1_10,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ? [U_29] :
( ( g_true_only(U_29,U_15)
| g_false_only(U_29,U_15) )
& g_both(U_29,U_12) )
| ? [U_28] :
( ( g_true_only(U_28,U_15)
| g_both(U_28,U_15) )
& g_true_only(U_28,U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_9,sK6)],[f_1_9]) ).
fof(f_1_11,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ? [U_29] :
( ( g_true_only(U_29,U_15)
| g_false_only(U_29,U_15) )
& g_both(U_29,U_12) )
| ( ( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15) )
& g_true_only(sK7(U_15,U_12),U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_28,sK7(U_15,U_12))],[f_1_10]) ).
fof(f_1_12,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ? [U_30] :
( ( g_both(U_30,U_15)
| g_false_only(U_30,U_15) )
& g_false_only(U_30,U_12) )
| ( ( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15) )
& g_both(sK8(U_15,U_12),U_12) )
| ( ( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15) )
& g_true_only(sK7(U_15,U_12),U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_29,sK8(U_15,U_12))],[f_1_11]) ).
fof(f_1_13,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ? [U_14] :
! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,U_14) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,U_14) ) )
| ! [U_12] :
( ( ( g_both(sK9(U_15,U_12),U_15)
| g_false_only(sK9(U_15,U_12),U_15) )
& g_false_only(sK9(U_15,U_12),U_12) )
| ( ( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15) )
& g_both(sK8(U_15,U_12),U_12) )
| ( ( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15) )
& g_true_only(sK7(U_15,U_12),U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_30,sK9(U_15,U_12))],[f_1_12]) ).
fof(f_1_14,negated_conjecture,
( ( ? [U_18] :
! [U_17] :
( ? [U_33] :
( ( g_both(U_33,U_18)
| g_false_only(U_33,U_18) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,U_18)
| g_false_only(U_32,U_18) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,U_18)
| g_both(U_31,U_18) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,sK10(U_15)) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,sK10(U_15)) ) )
| ! [U_12] :
( ( ( g_both(sK9(U_15,U_12),U_15)
| g_false_only(sK9(U_15,U_12),U_15) )
& g_false_only(sK9(U_15,U_12),U_12) )
| ( ( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15) )
& g_both(sK8(U_15,U_12),U_12) )
| ( ( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15) )
& g_true_only(sK7(U_15,U_12),U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_14,sK10(U_15))],[f_1_13]) ).
fof(f_1_15,negated_conjecture,
( ( ! [U_17] :
( ? [U_33] :
( ( g_both(U_33,sK11)
| g_false_only(U_33,sK11) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,sK11)
| g_false_only(U_32,sK11) )
& g_both(U_32,U_17) )
| ? [U_31] :
( ( g_true_only(U_31,sK11)
| g_both(U_31,sK11) )
& g_true_only(U_31,U_17) ) )
| ! [U_15] :
( ! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,sK10(U_15)) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,sK10(U_15)) ) )
| ! [U_12] :
( ( ( g_both(sK9(U_15,U_12),U_15)
| g_false_only(sK9(U_15,U_12),U_15) )
& g_false_only(sK9(U_15,U_12),U_12) )
| ( ( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15) )
& g_both(sK8(U_15,U_12),U_12) )
| ( ( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15) )
& g_true_only(sK7(U_15,U_12),U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_18,sK11)],[f_1_14]) ).
fof(f_1_16,negated_conjecture,
( ( ! [U_17] :
( ? [U_33] :
( ( g_both(U_33,sK11)
| g_false_only(U_33,sK11) )
& g_false_only(U_33,U_17) )
| ? [U_32] :
( ( g_true_only(U_32,sK11)
| g_false_only(U_32,sK11) )
& g_both(U_32,U_17) )
| ( ( g_true_only(sK12(U_17),sK11)
| g_both(sK12(U_17),sK11) )
& g_true_only(sK12(U_17),U_17) ) )
| ! [U_15] :
( ! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,sK10(U_15)) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,sK10(U_15)) ) )
| ! [U_12] :
( ( ( g_both(sK9(U_15,U_12),U_15)
| g_false_only(sK9(U_15,U_12),U_15) )
& g_false_only(sK9(U_15,U_12),U_12) )
| ( ( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15) )
& g_both(sK8(U_15,U_12),U_12) )
| ( ( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15) )
& g_true_only(sK7(U_15,U_12),U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_31,sK12(U_17))],[f_1_15]) ).
fof(f_1_17,negated_conjecture,
( ( ! [U_17] :
( ? [U_33] :
( ( g_both(U_33,sK11)
| g_false_only(U_33,sK11) )
& g_false_only(U_33,U_17) )
| ( ( g_true_only(sK13(U_17),sK11)
| g_false_only(sK13(U_17),sK11) )
& g_both(sK13(U_17),U_17) )
| ( ( g_true_only(sK12(U_17),sK11)
| g_both(sK12(U_17),sK11) )
& g_true_only(sK12(U_17),U_17) ) )
| ! [U_15] :
( ! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,sK10(U_15)) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,sK10(U_15)) ) )
| ! [U_12] :
( ( ( g_both(sK9(U_15,U_12),U_15)
| g_false_only(sK9(U_15,U_12),U_15) )
& g_false_only(sK9(U_15,U_12),U_12) )
| ( ( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15) )
& g_both(sK8(U_15,U_12),U_12) )
| ( ( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15) )
& g_true_only(sK7(U_15,U_12),U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_32,sK13(U_17))],[f_1_16]) ).
fof(f_1_18,negated_conjecture,
( ( ! [U_17] :
( ( ( g_both(sK14(U_17),sK11)
| g_false_only(sK14(U_17),sK11) )
& g_false_only(sK14(U_17),U_17) )
| ( ( g_true_only(sK13(U_17),sK11)
| g_false_only(sK13(U_17),sK11) )
& g_both(sK13(U_17),U_17) )
| ( ( g_true_only(sK12(U_17),sK11)
| g_both(sK12(U_17),sK11) )
& g_true_only(sK12(U_17),U_17) ) )
| ! [U_15] :
( ! [U_13] :
( ( g_true_only(U_13,U_15)
& g_false_only(U_13,sK10(U_15)) )
| ( g_false_only(U_13,U_15)
& g_true_only(U_13,sK10(U_15)) ) )
| ! [U_12] :
( ( ( g_both(sK9(U_15,U_12),U_15)
| g_false_only(sK9(U_15,U_12),U_15) )
& g_false_only(sK9(U_15,U_12),U_12) )
| ( ( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15) )
& g_both(sK8(U_15,U_12),U_12) )
| ( ( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15) )
& g_true_only(sK7(U_15,U_12),U_12) )
| ! [U_10] :
( ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12) ) ) )
| ! [U_8] :
( ( g_false_only(U_8,U_8)
& g_false_only(U_8,sK6) )
| ( g_true_only(U_8,U_8)
& g_true_only(U_8,sK6) ) )
| ! [U_7] :
( ( ( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7)) )
& g_false_only(sK5(U_7),U_7) )
| ( ( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7)) )
& g_both(sK4(U_7),U_7) )
| ( ( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7)) )
& g_true_only(sK3(U_7),U_7) )
| ! [U_5] :
( ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ) ) )
& ! [U_4] :
( ! [U_24] :
( ( ~ g_both(U_24,U_4)
& ~ g_false_only(U_24,U_4) )
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_23] :
( ( ~ g_true_only(U_23,U_4)
& ~ g_false_only(U_23,U_4) )
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_22] :
( ( ~ g_true_only(U_22,U_4)
& ~ g_both(U_22,U_4) )
| ~ g_true_only(U_22,sK2(U_4)) ) )
& ! [U_21] :
( ( ~ g_both(U_21,U_21)
& ~ g_true_only(U_21,U_21) )
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( ( ~ g_false_only(U_20,U_20)
& ~ g_true_only(U_20,U_20) )
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( ( ~ g_false_only(U_19,U_19)
& ~ g_both(U_19,U_19) )
| ~ g_true_only(U_19,sK1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_33,sK14(U_17))],[f_1_17]) ).
fof(f_1_19,negated_conjecture,
( ! [U_17] :
( g_both(sK14(U_17),sK11)
| g_false_only(sK14(U_17),sK11)
| ~ sP18(U_17) )
& ! [U_17] :
( g_false_only(sK14(U_17),U_17)
| ~ sP18(U_17) )
& ! [U_17] :
( g_true_only(sK13(U_17),sK11)
| g_false_only(sK13(U_17),sK11)
| ~ sP17(U_17) )
& ! [U_17] :
( g_both(sK13(U_17),U_17)
| ~ sP17(U_17) )
& ! [U_17] :
( g_true_only(sK12(U_17),sK11)
| g_both(sK12(U_17),sK11)
| ~ sP16(U_17) )
& ! [U_17] :
( g_true_only(sK12(U_17),U_17)
| ~ sP16(U_17) )
& ! [U_13,U_15] :
( g_true_only(U_13,U_15)
| ~ sP15(U_13,U_15) )
& ! [U_13,U_15] :
( g_false_only(U_13,sK10(U_15))
| ~ sP15(U_13,U_15) )
& ! [U_13,U_15] :
( g_false_only(U_13,U_15)
| ~ sP14(U_13,U_15) )
& ! [U_13,U_15] :
( g_true_only(U_13,sK10(U_15))
| ~ sP14(U_13,U_15) )
& ! [U_12,U_15] :
( g_both(sK9(U_15,U_12),U_15)
| g_false_only(sK9(U_15,U_12),U_15)
| ~ sP13(U_12,U_15) )
& ! [U_12,U_15] :
( g_false_only(sK9(U_15,U_12),U_12)
| ~ sP13(U_12,U_15) )
& ! [U_12,U_15] :
( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15)
| ~ sP12(U_12,U_15) )
& ! [U_12,U_15] :
( g_both(sK8(U_15,U_12),U_12)
| ~ sP12(U_12,U_15) )
& ! [U_12,U_15] :
( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15)
| ~ sP11(U_12,U_15) )
& ! [U_12,U_15] :
( g_true_only(sK7(U_15,U_12),U_12)
| ~ sP11(U_12,U_15) )
& ! [U_8] :
( g_false_only(U_8,U_8)
| ~ sP10(U_8) )
& ! [U_8] :
( g_false_only(U_8,sK6)
| ~ sP10(U_8) )
& ! [U_8] :
( g_true_only(U_8,U_8)
| ~ sP9(U_8) )
& ! [U_8] :
( g_true_only(U_8,sK6)
| ~ sP9(U_8) )
& ! [U_7] :
( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7))
| ~ sP8(U_7) )
& ! [U_7] :
( g_false_only(sK5(U_7),U_7)
| ~ sP8(U_7) )
& ! [U_7] :
( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7))
| ~ sP7(U_7) )
& ! [U_7] :
( g_both(sK4(U_7),U_7)
| ~ sP7(U_7) )
& ! [U_7] :
( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7))
| ~ sP6(U_7) )
& ! [U_7] :
( g_true_only(sK3(U_7),U_7)
| ~ sP6(U_7) )
& ! [U_4,U_24] :
( ~ g_both(U_24,U_4)
| ~ sP5(U_4,U_24) )
& ! [U_4,U_24] :
( ~ g_false_only(U_24,U_4)
| ~ sP5(U_4,U_24) )
& ! [U_4,U_23] :
( ~ g_true_only(U_23,U_4)
| ~ sP4(U_4,U_23) )
& ! [U_4,U_23] :
( ~ g_false_only(U_23,U_4)
| ~ sP4(U_4,U_23) )
& ! [U_4,U_22] :
( ~ g_true_only(U_22,U_4)
| ~ sP3(U_4,U_22) )
& ! [U_4,U_22] :
( ~ g_both(U_22,U_4)
| ~ sP3(U_4,U_22) )
& ! [U_21] :
( ~ g_both(U_21,U_21)
| ~ sP2(U_21) )
& ! [U_21] :
( ~ g_true_only(U_21,U_21)
| ~ sP2(U_21) )
& ! [U_20] :
( ~ g_false_only(U_20,U_20)
| ~ sP1(U_20) )
& ! [U_20] :
( ~ g_true_only(U_20,U_20)
| ~ sP1(U_20) )
& ! [U_19] :
( ~ g_false_only(U_19,U_19)
| ~ sP0(U_19) )
& ! [U_19] :
( ~ g_both(U_19,U_19)
| ~ sP0(U_19) )
& ! [U_5,U_13,U_7,U_8,U_17,U_10,U_12,U_15] :
( sP18(U_17)
| sP17(U_17)
| sP16(U_17)
| sP15(U_13,U_15)
| sP14(U_13,U_15)
| sP13(U_12,U_15)
| sP12(U_12,U_15)
| sP11(U_12,U_15)
| ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12)
| sP10(U_8)
| sP9(U_8)
| sP8(U_7)
| sP7(U_7)
| sP6(U_7)
| ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) )
& ! [U_4,U_24] :
( sP5(U_4,U_24)
| ~ g_false_only(U_24,sK2(U_4)) )
& ! [U_4,U_23] :
( sP4(U_4,U_23)
| ~ g_both(U_23,sK2(U_4)) )
& ! [U_4,U_22] :
( sP3(U_4,U_22)
| ~ g_true_only(U_22,sK2(U_4)) )
& ! [U_21] :
( sP2(U_21)
| ~ g_false_only(U_21,sK1) )
& ! [U_20] :
( sP1(U_20)
| ~ g_both(U_20,sK1) )
& ! [U_19] :
( sP0(U_19)
| ~ g_true_only(U_19,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,sP18])],[f_1_18]) ).
cnf(f_1_20,negated_conjecture,
( sP0(U_19)
| ~ g_true_only(U_19,sK1) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_21,negated_conjecture,
( sP1(U_20)
| ~ g_both(U_20,sK1) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_22,negated_conjecture,
( sP2(U_21)
| ~ g_false_only(U_21,sK1) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_23,negated_conjecture,
( sP3(U_4,U_22)
| ~ g_true_only(U_22,sK2(U_4)) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_24,negated_conjecture,
( sP4(U_4,U_23)
| ~ g_both(U_23,sK2(U_4)) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_25,negated_conjecture,
( sP5(U_4,U_24)
| ~ g_false_only(U_24,sK2(U_4)) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_26,negated_conjecture,
( sP18(U_17)
| sP17(U_17)
| sP16(U_17)
| sP15(U_13,U_15)
| sP14(U_13,U_15)
| sP13(U_12,U_15)
| sP12(U_12,U_15)
| sP11(U_12,U_15)
| ~ g_both(U_10,U_15)
| ~ g_both(U_10,U_12)
| sP10(U_8)
| sP9(U_8)
| sP8(U_7)
| sP7(U_7)
| sP6(U_7)
| ~ g_both(U_5,U_5)
| ~ g_both(U_5,U_7) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_27,negated_conjecture,
( ~ g_both(U_19,U_19)
| ~ sP0(U_19) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_28,negated_conjecture,
( ~ g_false_only(U_19,U_19)
| ~ sP0(U_19) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_29,negated_conjecture,
( ~ g_true_only(U_20,U_20)
| ~ sP1(U_20) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_30,negated_conjecture,
( ~ g_false_only(U_20,U_20)
| ~ sP1(U_20) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_31,negated_conjecture,
( ~ g_true_only(U_21,U_21)
| ~ sP2(U_21) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_32,negated_conjecture,
( ~ g_both(U_21,U_21)
| ~ sP2(U_21) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_33,negated_conjecture,
( ~ g_both(U_22,U_4)
| ~ sP3(U_4,U_22) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_34,negated_conjecture,
( ~ g_true_only(U_22,U_4)
| ~ sP3(U_4,U_22) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_35,negated_conjecture,
( ~ g_false_only(U_23,U_4)
| ~ sP4(U_4,U_23) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_36,negated_conjecture,
( ~ g_true_only(U_23,U_4)
| ~ sP4(U_4,U_23) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_37,negated_conjecture,
( ~ g_false_only(U_24,U_4)
| ~ sP5(U_4,U_24) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_38,negated_conjecture,
( ~ g_both(U_24,U_4)
| ~ sP5(U_4,U_24) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_39,negated_conjecture,
( g_true_only(sK3(U_7),U_7)
| ~ sP6(U_7) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_40,negated_conjecture,
( g_false_only(sK3(U_7),sK3(U_7))
| g_both(sK3(U_7),sK3(U_7))
| ~ sP6(U_7) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_41,negated_conjecture,
( g_both(sK4(U_7),U_7)
| ~ sP7(U_7) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_42,negated_conjecture,
( g_false_only(sK4(U_7),sK4(U_7))
| g_true_only(sK4(U_7),sK4(U_7))
| ~ sP7(U_7) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_43,negated_conjecture,
( g_false_only(sK5(U_7),U_7)
| ~ sP8(U_7) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_44,negated_conjecture,
( g_both(sK5(U_7),sK5(U_7))
| g_true_only(sK5(U_7),sK5(U_7))
| ~ sP8(U_7) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_46,negated_conjecture,
( g_true_only(U_8,U_8)
| ~ sP9(U_8) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_48,negated_conjecture,
( g_false_only(U_8,U_8)
| ~ sP10(U_8) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_49,negated_conjecture,
( g_true_only(sK7(U_15,U_12),U_12)
| ~ sP11(U_12,U_15) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_50,negated_conjecture,
( g_true_only(sK7(U_15,U_12),U_15)
| g_both(sK7(U_15,U_12),U_15)
| ~ sP11(U_12,U_15) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_51,negated_conjecture,
( g_both(sK8(U_15,U_12),U_12)
| ~ sP12(U_12,U_15) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_52,negated_conjecture,
( g_true_only(sK8(U_15,U_12),U_15)
| g_false_only(sK8(U_15,U_12),U_15)
| ~ sP12(U_12,U_15) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_53,negated_conjecture,
( g_false_only(sK9(U_15,U_12),U_12)
| ~ sP13(U_12,U_15) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_54,negated_conjecture,
( g_both(sK9(U_15,U_12),U_15)
| g_false_only(sK9(U_15,U_12),U_15)
| ~ sP13(U_12,U_15) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_56,negated_conjecture,
( g_false_only(U_13,U_15)
| ~ sP14(U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_58,negated_conjecture,
( g_true_only(U_13,U_15)
| ~ sP15(U_13,U_15) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_59,negated_conjecture,
( g_true_only(sK12(U_17),U_17)
| ~ sP16(U_17) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_60,negated_conjecture,
( g_true_only(sK12(U_17),sK11)
| g_both(sK12(U_17),sK11)
| ~ sP16(U_17) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_61,negated_conjecture,
( g_both(sK13(U_17),U_17)
| ~ sP17(U_17) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_62,negated_conjecture,
( g_true_only(sK13(U_17),sK11)
| g_false_only(sK13(U_17),sK11)
| ~ sP17(U_17) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_63,negated_conjecture,
( g_false_only(sK14(U_17),U_17)
| ~ sP18(U_17) ),
inference(clausify,[status(thm)],[f_1_19]) ).
cnf(f_1_64,negated_conjecture,
( g_both(sK14(U_17),sK11)
| g_false_only(sK14(U_17),sK11)
| ~ sP18(U_17) ),
inference(clausify,[status(thm)],[f_1_19]) ).
fof(f_2_1,plain,
! [X_2,X_1] :
( ( g_true_only(X_2,X_1)
| g_false(X_2,X_1)
| ~ g_true(X_2,X_1) )
& ( ( ~ g_false(X_2,X_1)
& g_true(X_2,X_1) )
| ~ g_true_only(X_2,X_1) ) ),
inference(fof_nnf,[status(thm)],[true_only_g]) ).
fof(f_2_2,plain,
! [U_35,U_34] :
( ( g_true_only(U_35,U_34)
| g_false(U_35,U_34)
| ~ g_true(U_35,U_34) )
& ( ( ~ g_false(U_35,U_34)
& g_true(U_35,U_34) )
| ~ g_true_only(U_35,U_34) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_39,U_37] :
( g_true_only(U_39,U_37)
| g_false(U_39,U_37)
| ~ g_true(U_39,U_37) )
& ! [U_38,U_36] :
( ( ~ g_false(U_38,U_36)
& g_true(U_38,U_36) )
| ~ g_true_only(U_38,U_36) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
cnf(f_2_4,plain,
( g_true(U_38,U_36)
| ~ g_true_only(U_38,U_36) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_5,plain,
( ~ g_false(U_38,U_36)
| ~ g_true_only(U_38,U_36) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_6,plain,
( g_true_only(U_39,U_37)
| g_false(U_39,U_37)
| ~ g_true(U_39,U_37) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
! [X_2,X_1] :
( ( g_both(X_2,X_1)
| ~ g_false(X_2,X_1)
| ~ g_true(X_2,X_1) )
& ( ( g_false(X_2,X_1)
& g_true(X_2,X_1) )
| ~ g_both(X_2,X_1) ) ),
inference(fof_nnf,[status(thm)],[both_g]) ).
fof(f_3_2,plain,
! [U_41,U_40] :
( ( g_both(U_41,U_40)
| ~ g_false(U_41,U_40)
| ~ g_true(U_41,U_40) )
& ( ( g_false(U_41,U_40)
& g_true(U_41,U_40) )
| ~ g_both(U_41,U_40) ) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_45,U_43] :
( g_both(U_45,U_43)
| ~ g_false(U_45,U_43)
| ~ g_true(U_45,U_43) )
& ! [U_44,U_42] :
( ( g_false(U_44,U_42)
& g_true(U_44,U_42) )
| ~ g_both(U_44,U_42) ) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
cnf(f_3_4,plain,
( g_true(U_44,U_42)
| ~ g_both(U_44,U_42) ),
inference(clausify,[status(thm)],[f_3_3]) ).
cnf(f_3_5,plain,
( g_false(U_44,U_42)
| ~ g_both(U_44,U_42) ),
inference(clausify,[status(thm)],[f_3_3]) ).
fof(f_4_1,plain,
! [X_2,X_1] :
( ( g_false_only(X_2,X_1)
| g_true(X_2,X_1)
| ~ g_false(X_2,X_1) )
& ( ( ~ g_true(X_2,X_1)
& g_false(X_2,X_1) )
| ~ g_false_only(X_2,X_1) ) ),
inference(fof_nnf,[status(thm)],[false_only_g]) ).
fof(f_4_2,plain,
! [U_47,U_46] :
( ( g_false_only(U_47,U_46)
| g_true(U_47,U_46)
| ~ g_false(U_47,U_46) )
& ( ( ~ g_true(U_47,U_46)
& g_false(U_47,U_46) )
| ~ g_false_only(U_47,U_46) ) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_51,U_49] :
( g_false_only(U_51,U_49)
| g_true(U_51,U_49)
| ~ g_false(U_51,U_49) )
& ! [U_50,U_48] :
( ( ~ g_true(U_50,U_48)
& g_false(U_50,U_48) )
| ~ g_false_only(U_50,U_48) ) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
( g_false(U_50,U_48)
| ~ g_false_only(U_50,U_48) ),
inference(clausify,[status(thm)],[f_4_3]) ).
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_53,U_52] :
( g_false_only(U_53,U_52)
| g_both(U_53,U_52)
| g_true_only(U_53,U_52) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( g_false_only(U_53,U_52)
| g_both(U_53,U_52)
| g_true_only(U_53,U_52) ),
inference(clausify,[status(thm)],[f_5_2]) ).
cnf(t1,plain,
( ~ g_false(sK2(sK1),sK1)
| ~ g_true_only(sK2(sK1),sK1) ),
inference(start,[status(thm),parent(0:0)],[f_2_5]) ).
cnf(t2,plain,
( g_both(sK2(sK1),sK1)
| g_false_only(sK2(sK1),sK1)
| g_true_only(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t1:1)],[f_5_3]) ).
cnf(t3,plain,
$false,
inference(connection,[status(thm),parent(t2:1)],[t2:1,t1:1]) ).
cnf(t4,plain,
( ~ sP5(sK1,sK2(sK1))
| ~ g_false_only(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t2:2)],[f_1_37]) ).
cnf(t5,plain,
$false,
inference(connection,[status(thm),parent(t4:1)],[t4:1,t2:2]) ).
cnf(t6,plain,
( ~ g_false_only(sK2(sK1),sK2(sK1))
| sP5(sK1,sK2(sK1)) ),
inference(extension,[status(thm),parent(t4:2)],[f_1_25]) ).
cnf(t7,plain,
$false,
inference(connection,[status(thm),parent(t6:1)],[t6:1,t4:2]) ).
cnf(t8,plain,
( g_both(sK2(sK1),sK2(sK1))
| g_true_only(sK2(sK1),sK2(sK1))
| g_false_only(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t6:2)],[f_5_3]) ).
cnf(t9,plain,
$false,
inference(connection,[status(thm),parent(t8:1)],[t8:1,t6:2]) ).
cnf(t10,plain,
( ~ sP2(sK2(sK1))
| ~ g_true_only(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t8:2)],[f_1_31]) ).
cnf(t11,plain,
$false,
inference(connection,[status(thm),parent(t10:1)],[t10:1,t8:2]) ).
cnf(t12,plain,
( ~ g_false_only(sK2(sK1),sK1)
| sP2(sK2(sK1)) ),
inference(extension,[status(thm),parent(t10:2)],[f_1_22]) ).
cnf(t13,plain,
$false,
inference(connection,[status(thm),parent(t12:1)],[t12:1,t10:2]) ).
cnf(t14,plain,
$false,
inference(reduction,[status(thm),parent(t12:2)],[t12:2,t2:2]) ).
cnf(t15,plain,
( ~ sP2(sK2(sK1))
| ~ g_both(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t8:3)],[f_1_32]) ).
cnf(t16,plain,
$false,
inference(connection,[status(thm),parent(t15:1)],[t15:1,t8:3]) ).
cnf(t17,plain,
( ~ g_false_only(sK2(sK1),sK1)
| sP2(sK2(sK1)) ),
inference(extension,[status(thm),parent(t15:2)],[f_1_22]) ).
cnf(t18,plain,
$false,
inference(connection,[status(thm),parent(t17:1)],[t17:1,t15:2]) ).
cnf(t19,plain,
$false,
inference(reduction,[status(thm),parent(t17:2)],[t17:2,t2:2]) ).
cnf(l2,lemma,
~ g_false_only(sK2(sK1),sK1),
inference(lemma,[status(cth),parent(t2:2),below(t1:1)],[t2:2]) ).
cnf(t20,plain,
( ~ g_both(sK2(sK1),sK2(sK1))
| sP6(sK1)
| sP7(sK1)
| sP8(sK1)
| sP9(sK2(sK1))
| sP10(sK2(sK1))
| ~ g_both(sK2(sK1),sK2(sK1))
| sP18(sK2(sK11))
| sP11(sK2(sK1),sK1)
| sP12(sK2(sK1),sK1)
| sP13(sK2(sK1),sK1)
| sP14(sK2(sK1),sK1)
| sP15(sK2(sK1),sK1)
| sP16(sK2(sK11))
| sP17(sK2(sK11))
| ~ g_both(sK2(sK1),sK1)
| ~ g_both(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t2:3)],[f_1_26]) ).
cnf(t21,plain,
$false,
inference(connection,[status(thm),parent(t20:1)],[t20:1,t2:3]) ).
cnf(t22,plain,
$false,
inference(reduction,[status(thm),parent(t20:2)],[t20:2,t2:3]) ).
cnf(l12,lemma,
g_both(sK2(sK1),sK1),
inference(lemma,[status(cth),parent(t20:2),below(t2:3)],[t20:2]) ).
cnf(t23,plain,
( g_false_only(sK13(sK2(sK11)),sK11)
| g_true_only(sK13(sK2(sK11)),sK11)
| ~ sP17(sK2(sK11)) ),
inference(extension,[status(thm),parent(t20:3)],[f_1_62]) ).
cnf(t24,plain,
$false,
inference(connection,[status(thm),parent(t23:1)],[t23:1,t20:3]) ).
cnf(t25,plain,
( ~ sP4(sK11,sK13(sK2(sK11)))
| ~ g_true_only(sK13(sK2(sK11)),sK11) ),
inference(extension,[status(thm),parent(t23:2)],[f_1_36]) ).
cnf(t26,plain,
$false,
inference(connection,[status(thm),parent(t25:1)],[t25:1,t23:2]) ).
cnf(t27,plain,
( ~ g_both(sK13(sK2(sK11)),sK2(sK11))
| sP4(sK11,sK13(sK2(sK11))) ),
inference(extension,[status(thm),parent(t25:2)],[f_1_24]) ).
cnf(t28,plain,
$false,
inference(connection,[status(thm),parent(t27:1)],[t27:1,t25:2]) ).
cnf(t29,plain,
( ~ sP17(sK2(sK11))
| g_both(sK13(sK2(sK11)),sK2(sK11)) ),
inference(extension,[status(thm),parent(t27:2)],[f_1_61]) ).
cnf(t30,plain,
$false,
inference(connection,[status(thm),parent(t29:1)],[t29:1,t27:2]) ).
cnf(t31,plain,
$false,
inference(reduction,[status(thm),parent(t29:2)],[t29:2,t20:3]) ).
cnf(t32,plain,
( ~ sP4(sK11,sK13(sK2(sK11)))
| ~ g_false_only(sK13(sK2(sK11)),sK11) ),
inference(extension,[status(thm),parent(t23:3)],[f_1_35]) ).
cnf(t33,plain,
$false,
inference(connection,[status(thm),parent(t32:1)],[t32:1,t23:3]) ).
cnf(t34,plain,
( ~ g_both(sK13(sK2(sK11)),sK2(sK11))
| sP4(sK11,sK13(sK2(sK11))) ),
inference(extension,[status(thm),parent(t32:2)],[f_1_24]) ).
cnf(t35,plain,
$false,
inference(connection,[status(thm),parent(t34:1)],[t34:1,t32:2]) ).
cnf(t36,plain,
( ~ sP17(sK2(sK11))
| g_both(sK13(sK2(sK11)),sK2(sK11)) ),
inference(extension,[status(thm),parent(t34:2)],[f_1_61]) ).
cnf(t37,plain,
$false,
inference(connection,[status(thm),parent(t36:1)],[t36:1,t34:2]) ).
cnf(t38,plain,
$false,
inference(reduction,[status(thm),parent(t36:2)],[t36:2,t20:3]) ).
cnf(t39,plain,
( g_both(sK12(sK2(sK11)),sK11)
| g_true_only(sK12(sK2(sK11)),sK11)
| ~ sP16(sK2(sK11)) ),
inference(extension,[status(thm),parent(t20:4)],[f_1_60]) ).
cnf(t40,plain,
$false,
inference(connection,[status(thm),parent(t39:1)],[t39:1,t20:4]) ).
cnf(t41,plain,
( ~ sP3(sK11,sK12(sK2(sK11)))
| ~ g_true_only(sK12(sK2(sK11)),sK11) ),
inference(extension,[status(thm),parent(t39:2)],[f_1_34]) ).
cnf(t42,plain,
$false,
inference(connection,[status(thm),parent(t41:1)],[t41:1,t39:2]) ).
cnf(t43,plain,
( ~ g_true_only(sK12(sK2(sK11)),sK2(sK11))
| sP3(sK11,sK12(sK2(sK11))) ),
inference(extension,[status(thm),parent(t41:2)],[f_1_23]) ).
cnf(t44,plain,
$false,
inference(connection,[status(thm),parent(t43:1)],[t43:1,t41:2]) ).
cnf(t45,plain,
( ~ sP16(sK2(sK11))
| g_true_only(sK12(sK2(sK11)),sK2(sK11)) ),
inference(extension,[status(thm),parent(t43:2)],[f_1_59]) ).
cnf(t46,plain,
$false,
inference(connection,[status(thm),parent(t45:1)],[t45:1,t43:2]) ).
cnf(t47,plain,
$false,
inference(reduction,[status(thm),parent(t45:2)],[t45:2,t20:4]) ).
cnf(t48,plain,
( ~ sP3(sK11,sK12(sK2(sK11)))
| ~ g_both(sK12(sK2(sK11)),sK11) ),
inference(extension,[status(thm),parent(t39:3)],[f_1_33]) ).
cnf(t49,plain,
$false,
inference(connection,[status(thm),parent(t48:1)],[t48:1,t39:3]) ).
cnf(t50,plain,
( ~ g_true_only(sK12(sK2(sK11)),sK2(sK11))
| sP3(sK11,sK12(sK2(sK11))) ),
inference(extension,[status(thm),parent(t48:2)],[f_1_23]) ).
cnf(t51,plain,
$false,
inference(connection,[status(thm),parent(t50:1)],[t50:1,t48:2]) ).
cnf(t52,plain,
( ~ sP16(sK2(sK11))
| g_true_only(sK12(sK2(sK11)),sK2(sK11)) ),
inference(extension,[status(thm),parent(t50:2)],[f_1_59]) ).
cnf(t53,plain,
$false,
inference(connection,[status(thm),parent(t52:1)],[t52:1,t50:2]) ).
cnf(t54,plain,
$false,
inference(reduction,[status(thm),parent(t52:2)],[t52:2,t20:4]) ).
cnf(t55,plain,
( g_true_only(sK2(sK1),sK1)
| ~ sP15(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t20:5)],[f_1_58]) ).
cnf(t56,plain,
$false,
inference(connection,[status(thm),parent(t55:1)],[t55:1,t20:5]) ).
cnf(t57,plain,
$false,
inference(reduction,[status(thm),parent(t55:2)],[t55:2,t1:1]) ).
cnf(t58,plain,
( g_false_only(sK2(sK1),sK1)
| ~ sP14(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t20:6)],[f_1_56]) ).
cnf(t59,plain,
$false,
inference(connection,[status(thm),parent(t58:1)],[t58:1,t20:6]) ).
cnf(t60,plain,
~ g_false_only(sK2(sK1),sK1),
inference(lemma_extension,[status(thm),parent(t58:2)],[l2:1]) ).
cnf(t61,plain,
$false,
inference(connection,[status(thm),parent(t60:1)],[t60:1,t58:2]) ).
cnf(t62,plain,
( g_false_only(sK9(sK1,sK2(sK1)),sK1)
| g_both(sK9(sK1,sK2(sK1)),sK1)
| ~ sP13(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t20:7)],[f_1_54]) ).
cnf(t63,plain,
$false,
inference(connection,[status(thm),parent(t62:1)],[t62:1,t20:7]) ).
cnf(t64,plain,
( ~ sP5(sK1,sK9(sK1,sK2(sK1)))
| ~ g_both(sK9(sK1,sK2(sK1)),sK1) ),
inference(extension,[status(thm),parent(t62:2)],[f_1_38]) ).
cnf(t65,plain,
$false,
inference(connection,[status(thm),parent(t64:1)],[t64:1,t62:2]) ).
cnf(t66,plain,
( ~ g_false_only(sK9(sK1,sK2(sK1)),sK2(sK1))
| sP5(sK1,sK9(sK1,sK2(sK1))) ),
inference(extension,[status(thm),parent(t64:2)],[f_1_25]) ).
cnf(t67,plain,
$false,
inference(connection,[status(thm),parent(t66:1)],[t66:1,t64:2]) ).
cnf(t68,plain,
( ~ sP13(sK2(sK1),sK1)
| g_false_only(sK9(sK1,sK2(sK1)),sK2(sK1)) ),
inference(extension,[status(thm),parent(t66:2)],[f_1_53]) ).
cnf(t69,plain,
$false,
inference(connection,[status(thm),parent(t68:1)],[t68:1,t66:2]) ).
cnf(t70,plain,
$false,
inference(reduction,[status(thm),parent(t68:2)],[t68:2,t20:7]) ).
cnf(t71,plain,
( ~ sP5(sK1,sK9(sK1,sK2(sK1)))
| ~ g_false_only(sK9(sK1,sK2(sK1)),sK1) ),
inference(extension,[status(thm),parent(t62:3)],[f_1_37]) ).
cnf(t72,plain,
$false,
inference(connection,[status(thm),parent(t71:1)],[t71:1,t62:3]) ).
cnf(t73,plain,
( ~ g_false_only(sK9(sK1,sK2(sK1)),sK2(sK1))
| sP5(sK1,sK9(sK1,sK2(sK1))) ),
inference(extension,[status(thm),parent(t71:2)],[f_1_25]) ).
cnf(t74,plain,
$false,
inference(connection,[status(thm),parent(t73:1)],[t73:1,t71:2]) ).
cnf(t75,plain,
( ~ sP13(sK2(sK1),sK1)
| g_false_only(sK9(sK1,sK2(sK1)),sK2(sK1)) ),
inference(extension,[status(thm),parent(t73:2)],[f_1_53]) ).
cnf(t76,plain,
$false,
inference(connection,[status(thm),parent(t75:1)],[t75:1,t73:2]) ).
cnf(t77,plain,
$false,
inference(reduction,[status(thm),parent(t75:2)],[t75:2,t20:7]) ).
cnf(t78,plain,
( g_false_only(sK8(sK1,sK2(sK1)),sK1)
| g_true_only(sK8(sK1,sK2(sK1)),sK1)
| ~ sP12(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t20:8)],[f_1_52]) ).
cnf(t79,plain,
$false,
inference(connection,[status(thm),parent(t78:1)],[t78:1,t20:8]) ).
cnf(t80,plain,
( ~ sP4(sK1,sK8(sK1,sK2(sK1)))
| ~ g_true_only(sK8(sK1,sK2(sK1)),sK1) ),
inference(extension,[status(thm),parent(t78:2)],[f_1_36]) ).
cnf(t81,plain,
$false,
inference(connection,[status(thm),parent(t80:1)],[t80:1,t78:2]) ).
cnf(t82,plain,
( ~ g_both(sK8(sK1,sK2(sK1)),sK2(sK1))
| sP4(sK1,sK8(sK1,sK2(sK1))) ),
inference(extension,[status(thm),parent(t80:2)],[f_1_24]) ).
cnf(t83,plain,
$false,
inference(connection,[status(thm),parent(t82:1)],[t82:1,t80:2]) ).
cnf(t84,plain,
( ~ sP12(sK2(sK1),sK1)
| g_both(sK8(sK1,sK2(sK1)),sK2(sK1)) ),
inference(extension,[status(thm),parent(t82:2)],[f_1_51]) ).
cnf(t85,plain,
$false,
inference(connection,[status(thm),parent(t84:1)],[t84:1,t82:2]) ).
cnf(t86,plain,
$false,
inference(reduction,[status(thm),parent(t84:2)],[t84:2,t20:8]) ).
cnf(t87,plain,
( ~ sP4(sK1,sK8(sK1,sK2(sK1)))
| ~ g_false_only(sK8(sK1,sK2(sK1)),sK1) ),
inference(extension,[status(thm),parent(t78:3)],[f_1_35]) ).
cnf(t88,plain,
$false,
inference(connection,[status(thm),parent(t87:1)],[t87:1,t78:3]) ).
cnf(t89,plain,
( ~ g_both(sK8(sK1,sK2(sK1)),sK2(sK1))
| sP4(sK1,sK8(sK1,sK2(sK1))) ),
inference(extension,[status(thm),parent(t87:2)],[f_1_24]) ).
cnf(t90,plain,
$false,
inference(connection,[status(thm),parent(t89:1)],[t89:1,t87:2]) ).
cnf(t91,plain,
( ~ sP12(sK2(sK1),sK1)
| g_both(sK8(sK1,sK2(sK1)),sK2(sK1)) ),
inference(extension,[status(thm),parent(t89:2)],[f_1_51]) ).
cnf(t92,plain,
$false,
inference(connection,[status(thm),parent(t91:1)],[t91:1,t89:2]) ).
cnf(t93,plain,
$false,
inference(reduction,[status(thm),parent(t91:2)],[t91:2,t20:8]) ).
cnf(t94,plain,
( g_both(sK7(sK1,sK2(sK1)),sK1)
| g_true_only(sK7(sK1,sK2(sK1)),sK1)
| ~ sP11(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t20:9)],[f_1_50]) ).
cnf(t95,plain,
$false,
inference(connection,[status(thm),parent(t94:1)],[t94:1,t20:9]) ).
cnf(t96,plain,
( ~ sP3(sK1,sK7(sK1,sK2(sK1)))
| ~ g_true_only(sK7(sK1,sK2(sK1)),sK1) ),
inference(extension,[status(thm),parent(t94:2)],[f_1_34]) ).
cnf(t97,plain,
$false,
inference(connection,[status(thm),parent(t96:1)],[t96:1,t94:2]) ).
cnf(t98,plain,
( ~ g_true_only(sK7(sK1,sK2(sK1)),sK2(sK1))
| sP3(sK1,sK7(sK1,sK2(sK1))) ),
inference(extension,[status(thm),parent(t96:2)],[f_1_23]) ).
cnf(t99,plain,
$false,
inference(connection,[status(thm),parent(t98:1)],[t98:1,t96:2]) ).
cnf(t100,plain,
( ~ sP11(sK2(sK1),sK1)
| g_true_only(sK7(sK1,sK2(sK1)),sK2(sK1)) ),
inference(extension,[status(thm),parent(t98:2)],[f_1_49]) ).
cnf(t101,plain,
$false,
inference(connection,[status(thm),parent(t100:1)],[t100:1,t98:2]) ).
cnf(t102,plain,
$false,
inference(reduction,[status(thm),parent(t100:2)],[t100:2,t20:9]) ).
cnf(t103,plain,
( ~ sP3(sK1,sK7(sK1,sK2(sK1)))
| ~ g_both(sK7(sK1,sK2(sK1)),sK1) ),
inference(extension,[status(thm),parent(t94:3)],[f_1_33]) ).
cnf(t104,plain,
$false,
inference(connection,[status(thm),parent(t103:1)],[t103:1,t94:3]) ).
cnf(t105,plain,
( ~ g_true_only(sK7(sK1,sK2(sK1)),sK2(sK1))
| sP3(sK1,sK7(sK1,sK2(sK1))) ),
inference(extension,[status(thm),parent(t103:2)],[f_1_23]) ).
cnf(t106,plain,
$false,
inference(connection,[status(thm),parent(t105:1)],[t105:1,t103:2]) ).
cnf(t107,plain,
( ~ sP11(sK2(sK1),sK1)
| g_true_only(sK7(sK1,sK2(sK1)),sK2(sK1)) ),
inference(extension,[status(thm),parent(t105:2)],[f_1_49]) ).
cnf(t108,plain,
$false,
inference(connection,[status(thm),parent(t107:1)],[t107:1,t105:2]) ).
cnf(t109,plain,
$false,
inference(reduction,[status(thm),parent(t107:2)],[t107:2,t20:9]) ).
cnf(t110,plain,
( g_false_only(sK14(sK2(sK11)),sK11)
| g_both(sK14(sK2(sK11)),sK11)
| ~ sP18(sK2(sK11)) ),
inference(extension,[status(thm),parent(t20:10)],[f_1_64]) ).
cnf(t111,plain,
$false,
inference(connection,[status(thm),parent(t110:1)],[t110:1,t20:10]) ).
cnf(t112,plain,
( ~ sP5(sK11,sK14(sK2(sK11)))
| ~ g_both(sK14(sK2(sK11)),sK11) ),
inference(extension,[status(thm),parent(t110:2)],[f_1_38]) ).
cnf(t113,plain,
$false,
inference(connection,[status(thm),parent(t112:1)],[t112:1,t110:2]) ).
cnf(t114,plain,
( ~ g_false_only(sK14(sK2(sK11)),sK2(sK11))
| sP5(sK11,sK14(sK2(sK11))) ),
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,
( ~ sP18(sK2(sK11))
| g_false_only(sK14(sK2(sK11)),sK2(sK11)) ),
inference(extension,[status(thm),parent(t114:2)],[f_1_63]) ).
cnf(t117,plain,
$false,
inference(connection,[status(thm),parent(t116:1)],[t116:1,t114:2]) ).
cnf(t118,plain,
$false,
inference(reduction,[status(thm),parent(t116:2)],[t116:2,t20:10]) ).
cnf(t119,plain,
( ~ sP5(sK11,sK14(sK2(sK11)))
| ~ g_false_only(sK14(sK2(sK11)),sK11) ),
inference(extension,[status(thm),parent(t110:3)],[f_1_37]) ).
cnf(t120,plain,
$false,
inference(connection,[status(thm),parent(t119:1)],[t119:1,t110:3]) ).
cnf(t121,plain,
( ~ g_false_only(sK14(sK2(sK11)),sK2(sK11))
| sP5(sK11,sK14(sK2(sK11))) ),
inference(extension,[status(thm),parent(t119:2)],[f_1_25]) ).
cnf(t122,plain,
$false,
inference(connection,[status(thm),parent(t121:1)],[t121:1,t119:2]) ).
cnf(t123,plain,
( ~ sP18(sK2(sK11))
| g_false_only(sK14(sK2(sK11)),sK2(sK11)) ),
inference(extension,[status(thm),parent(t121:2)],[f_1_63]) ).
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,t20:10]) ).
cnf(t126,plain,
( g_false_only(sK2(sK1),sK2(sK1))
| g_true_only(sK2(sK1),sK2(sK1))
| g_both(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t20:11)],[f_5_3]) ).
cnf(t127,plain,
$false,
inference(connection,[status(thm),parent(t126:1)],[t126:1,t20:11]) ).
cnf(t128,plain,
( ~ sP1(sK2(sK1))
| ~ g_true_only(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t126:2)],[f_1_29]) ).
cnf(t129,plain,
$false,
inference(connection,[status(thm),parent(t128:1)],[t128:1,t126:2]) ).
cnf(t130,plain,
( ~ g_both(sK2(sK1),sK1)
| sP1(sK2(sK1)) ),
inference(extension,[status(thm),parent(t128:2)],[f_1_21]) ).
cnf(t131,plain,
$false,
inference(connection,[status(thm),parent(t130:1)],[t130:1,t128:2]) ).
cnf(t132,plain,
g_both(sK2(sK1),sK1),
inference(lemma_extension,[status(thm),parent(t130:2)],[l12:1]) ).
cnf(t133,plain,
$false,
inference(connection,[status(thm),parent(t132:1)],[t132:1,t130:2]) ).
cnf(t134,plain,
( ~ sP1(sK2(sK1))
| ~ g_false_only(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t126:3)],[f_1_30]) ).
cnf(t135,plain,
$false,
inference(connection,[status(thm),parent(t134:1)],[t134:1,t126:3]) ).
cnf(t136,plain,
( ~ g_both(sK2(sK1),sK1)
| sP1(sK2(sK1)) ),
inference(extension,[status(thm),parent(t134:2)],[f_1_21]) ).
cnf(t137,plain,
$false,
inference(connection,[status(thm),parent(t136:1)],[t136:1,t134:2]) ).
cnf(t138,plain,
g_both(sK2(sK1),sK1),
inference(lemma_extension,[status(thm),parent(t136:2)],[l12:1]) ).
cnf(t139,plain,
$false,
inference(connection,[status(thm),parent(t138:1)],[t138:1,t136:2]) ).
cnf(l70,lemma,
g_both(sK2(sK1),sK2(sK1)),
inference(lemma,[status(cth),parent(t20:11),below(t2:3)],[t20:11]) ).
cnf(t140,plain,
( g_false_only(sK2(sK1),sK2(sK1))
| ~ sP10(sK2(sK1)) ),
inference(extension,[status(thm),parent(t20:12)],[f_1_48]) ).
cnf(t141,plain,
$false,
inference(connection,[status(thm),parent(t140:1)],[t140:1,t20:12]) ).
cnf(t142,plain,
( ~ sP1(sK2(sK1))
| ~ g_false_only(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t140:2)],[f_1_30]) ).
cnf(t143,plain,
$false,
inference(connection,[status(thm),parent(t142:1)],[t142:1,t140:2]) ).
cnf(t144,plain,
( ~ g_both(sK2(sK1),sK1)
| sP1(sK2(sK1)) ),
inference(extension,[status(thm),parent(t142:2)],[f_1_21]) ).
cnf(t145,plain,
$false,
inference(connection,[status(thm),parent(t144:1)],[t144:1,t142:2]) ).
cnf(t146,plain,
$false,
inference(reduction,[status(thm),parent(t144:2)],[t144:2,t2:3]) ).
cnf(t147,plain,
( g_true_only(sK2(sK1),sK2(sK1))
| ~ sP9(sK2(sK1)) ),
inference(extension,[status(thm),parent(t20:13)],[f_1_46]) ).
cnf(t148,plain,
$false,
inference(connection,[status(thm),parent(t147:1)],[t147:1,t20:13]) ).
cnf(t149,plain,
( ~ g_false(sK2(sK1),sK2(sK1))
| ~ g_true_only(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t147:2)],[f_2_5]) ).
cnf(t150,plain,
$false,
inference(connection,[status(thm),parent(t149:1)],[t149:1,t147:2]) ).
cnf(t151,plain,
( ~ g_both(sK2(sK1),sK2(sK1))
| g_false(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t149:2)],[f_3_5]) ).
cnf(t152,plain,
$false,
inference(connection,[status(thm),parent(t151:1)],[t151:1,t149:2]) ).
cnf(t153,plain,
g_both(sK2(sK1),sK2(sK1)),
inference(lemma_extension,[status(thm),parent(t151:2)],[l70:1]) ).
cnf(t154,plain,
$false,
inference(connection,[status(thm),parent(t153:1)],[t153:1,t151:2]) ).
cnf(t155,plain,
( g_true_only(sK5(sK1),sK5(sK1))
| g_both(sK5(sK1),sK5(sK1))
| ~ sP8(sK1) ),
inference(extension,[status(thm),parent(t20:14)],[f_1_44]) ).
cnf(t156,plain,
$false,
inference(connection,[status(thm),parent(t155:1)],[t155:1,t20:14]) ).
cnf(t157,plain,
( ~ sP2(sK5(sK1))
| ~ g_both(sK5(sK1),sK5(sK1)) ),
inference(extension,[status(thm),parent(t155:2)],[f_1_32]) ).
cnf(t158,plain,
$false,
inference(connection,[status(thm),parent(t157:1)],[t157:1,t155:2]) ).
cnf(t159,plain,
( ~ g_false_only(sK5(sK1),sK1)
| sP2(sK5(sK1)) ),
inference(extension,[status(thm),parent(t157:2)],[f_1_22]) ).
cnf(t160,plain,
$false,
inference(connection,[status(thm),parent(t159:1)],[t159:1,t157:2]) ).
cnf(t161,plain,
( ~ sP8(sK1)
| g_false_only(sK5(sK1),sK1) ),
inference(extension,[status(thm),parent(t159:2)],[f_1_43]) ).
cnf(t162,plain,
$false,
inference(connection,[status(thm),parent(t161:1)],[t161:1,t159:2]) ).
cnf(t163,plain,
$false,
inference(reduction,[status(thm),parent(t161:2)],[t161:2,t20:14]) ).
cnf(t164,plain,
( ~ sP2(sK5(sK1))
| ~ g_true_only(sK5(sK1),sK5(sK1)) ),
inference(extension,[status(thm),parent(t155:3)],[f_1_31]) ).
cnf(t165,plain,
$false,
inference(connection,[status(thm),parent(t164:1)],[t164:1,t155:3]) ).
cnf(t166,plain,
( ~ g_false_only(sK5(sK1),sK1)
| sP2(sK5(sK1)) ),
inference(extension,[status(thm),parent(t164:2)],[f_1_22]) ).
cnf(t167,plain,
$false,
inference(connection,[status(thm),parent(t166:1)],[t166:1,t164:2]) ).
cnf(t168,plain,
( ~ sP8(sK1)
| g_false_only(sK5(sK1),sK1) ),
inference(extension,[status(thm),parent(t166:2)],[f_1_43]) ).
cnf(t169,plain,
$false,
inference(connection,[status(thm),parent(t168:1)],[t168:1,t166:2]) ).
cnf(t170,plain,
$false,
inference(reduction,[status(thm),parent(t168:2)],[t168:2,t20:14]) ).
cnf(t171,plain,
( g_true_only(sK4(sK1),sK4(sK1))
| g_false_only(sK4(sK1),sK4(sK1))
| ~ sP7(sK1) ),
inference(extension,[status(thm),parent(t20:15)],[f_1_42]) ).
cnf(t172,plain,
$false,
inference(connection,[status(thm),parent(t171:1)],[t171:1,t20:15]) ).
cnf(t173,plain,
( ~ sP1(sK4(sK1))
| ~ g_false_only(sK4(sK1),sK4(sK1)) ),
inference(extension,[status(thm),parent(t171:2)],[f_1_30]) ).
cnf(t174,plain,
$false,
inference(connection,[status(thm),parent(t173:1)],[t173:1,t171:2]) ).
cnf(t175,plain,
( ~ g_both(sK4(sK1),sK1)
| sP1(sK4(sK1)) ),
inference(extension,[status(thm),parent(t173:2)],[f_1_21]) ).
cnf(t176,plain,
$false,
inference(connection,[status(thm),parent(t175:1)],[t175:1,t173:2]) ).
cnf(t177,plain,
( ~ sP7(sK1)
| g_both(sK4(sK1),sK1) ),
inference(extension,[status(thm),parent(t175:2)],[f_1_41]) ).
cnf(t178,plain,
$false,
inference(connection,[status(thm),parent(t177:1)],[t177:1,t175:2]) ).
cnf(t179,plain,
$false,
inference(reduction,[status(thm),parent(t177:2)],[t177:2,t20:15]) ).
cnf(t180,plain,
( ~ sP1(sK4(sK1))
| ~ g_true_only(sK4(sK1),sK4(sK1)) ),
inference(extension,[status(thm),parent(t171:3)],[f_1_29]) ).
cnf(t181,plain,
$false,
inference(connection,[status(thm),parent(t180:1)],[t180:1,t171:3]) ).
cnf(t182,plain,
( ~ g_both(sK4(sK1),sK1)
| sP1(sK4(sK1)) ),
inference(extension,[status(thm),parent(t180:2)],[f_1_21]) ).
cnf(t183,plain,
$false,
inference(connection,[status(thm),parent(t182:1)],[t182:1,t180:2]) ).
cnf(t184,plain,
( ~ sP7(sK1)
| g_both(sK4(sK1),sK1) ),
inference(extension,[status(thm),parent(t182:2)],[f_1_41]) ).
cnf(t185,plain,
$false,
inference(connection,[status(thm),parent(t184:1)],[t184:1,t182:2]) ).
cnf(t186,plain,
$false,
inference(reduction,[status(thm),parent(t184:2)],[t184:2,t20:15]) ).
cnf(t187,plain,
( g_both(sK3(sK1),sK3(sK1))
| g_false_only(sK3(sK1),sK3(sK1))
| ~ sP6(sK1) ),
inference(extension,[status(thm),parent(t20:16)],[f_1_40]) ).
cnf(t188,plain,
$false,
inference(connection,[status(thm),parent(t187:1)],[t187:1,t20:16]) ).
cnf(t189,plain,
( ~ sP0(sK3(sK1))
| ~ g_false_only(sK3(sK1),sK3(sK1)) ),
inference(extension,[status(thm),parent(t187:2)],[f_1_28]) ).
cnf(t190,plain,
$false,
inference(connection,[status(thm),parent(t189:1)],[t189:1,t187:2]) ).
cnf(t191,plain,
( ~ g_true_only(sK3(sK1),sK1)
| sP0(sK3(sK1)) ),
inference(extension,[status(thm),parent(t189:2)],[f_1_20]) ).
cnf(t192,plain,
$false,
inference(connection,[status(thm),parent(t191:1)],[t191:1,t189:2]) ).
cnf(t193,plain,
( ~ sP6(sK1)
| g_true_only(sK3(sK1),sK1) ),
inference(extension,[status(thm),parent(t191:2)],[f_1_39]) ).
cnf(t194,plain,
$false,
inference(connection,[status(thm),parent(t193:1)],[t193:1,t191:2]) ).
cnf(t195,plain,
$false,
inference(reduction,[status(thm),parent(t193:2)],[t193:2,t20:16]) ).
cnf(t196,plain,
( ~ sP0(sK3(sK1))
| ~ g_both(sK3(sK1),sK3(sK1)) ),
inference(extension,[status(thm),parent(t187:3)],[f_1_27]) ).
cnf(t197,plain,
$false,
inference(connection,[status(thm),parent(t196:1)],[t196:1,t187:3]) ).
cnf(t198,plain,
( ~ g_true_only(sK3(sK1),sK1)
| sP0(sK3(sK1)) ),
inference(extension,[status(thm),parent(t196:2)],[f_1_20]) ).
cnf(t199,plain,
$false,
inference(connection,[status(thm),parent(t198:1)],[t198:1,t196:2]) ).
cnf(t200,plain,
( ~ sP6(sK1)
| g_true_only(sK3(sK1),sK1) ),
inference(extension,[status(thm),parent(t198:2)],[f_1_39]) ).
cnf(t201,plain,
$false,
inference(connection,[status(thm),parent(t200:1)],[t200:1,t198:2]) ).
cnf(t202,plain,
$false,
inference(reduction,[status(thm),parent(t200:2)],[t200:2,t20:16]) ).
cnf(t203,plain,
g_both(sK2(sK1),sK2(sK1)),
inference(lemma_extension,[status(thm),parent(t20:17)],[l70:1]) ).
cnf(t204,plain,
$false,
inference(connection,[status(thm),parent(t203:1)],[t203:1,t20:17]) ).
cnf(l1,lemma,
g_true_only(sK2(sK1),sK1),
inference(lemma,[status(cth),parent(t1:1),below(0:0)],[t1:1]) ).
cnf(t205,plain,
( g_true_only(sK2(sK1),sK1)
| ~ g_true(sK2(sK1),sK1)
| g_false(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t1:2)],[f_2_6]) ).
cnf(t206,plain,
$false,
inference(connection,[status(thm),parent(t205:1)],[t205:1,t1:2]) ).
cnf(t207,plain,
( ~ g_both(sK2(sK1),sK1)
| g_true(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t205:2)],[f_3_4]) ).
cnf(t208,plain,
$false,
inference(connection,[status(thm),parent(t207:1)],[t207:1,t205:2]) ).
cnf(t209,plain,
( g_false_only(sK2(sK1),sK1)
| g_true_only(sK2(sK1),sK1)
| g_both(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t207:2)],[f_5_3]) ).
cnf(t210,plain,
$false,
inference(connection,[status(thm),parent(t209:1)],[t209:1,t207:2]) ).
cnf(t211,plain,
( g_true(sK2(sK1),sK1)
| ~ g_true_only(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t209:2)],[f_2_4]) ).
cnf(t212,plain,
$false,
inference(connection,[status(thm),parent(t211:1)],[t211:1,t209:2]) ).
cnf(t213,plain,
$false,
inference(reduction,[status(thm),parent(t211:2)],[t211:2,t205:2]) ).
cnf(t214,plain,
( g_false(sK2(sK1),sK1)
| ~ g_false_only(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t209:3)],[f_4_4]) ).
cnf(t215,plain,
$false,
inference(connection,[status(thm),parent(t214:1)],[t214:1,t209:3]) ).
cnf(t216,plain,
$false,
inference(reduction,[status(thm),parent(t214:2)],[t214:2,t1:2]) ).
cnf(t217,plain,
( ~ sP4(sK1,sK2(sK1))
| ~ g_true_only(sK2(sK1),sK1) ),
inference(extension,[status(thm),parent(t205:3)],[f_1_36]) ).
cnf(t218,plain,
$false,
inference(connection,[status(thm),parent(t217:1)],[t217:1,t205:3]) ).
cnf(t219,plain,
( ~ g_both(sK2(sK1),sK2(sK1))
| sP4(sK1,sK2(sK1)) ),
inference(extension,[status(thm),parent(t217:2)],[f_1_24]) ).
cnf(t220,plain,
$false,
inference(connection,[status(thm),parent(t219:1)],[t219:1,t217:2]) ).
cnf(t221,plain,
( g_false_only(sK2(sK1),sK2(sK1))
| g_true_only(sK2(sK1),sK2(sK1))
| g_both(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t219:2)],[f_5_3]) ).
cnf(t222,plain,
$false,
inference(connection,[status(thm),parent(t221:1)],[t221:1,t219:2]) ).
cnf(t223,plain,
( sP3(sK1,sK2(sK1))
| ~ g_true_only(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t221:2)],[f_1_23]) ).
cnf(t224,plain,
$false,
inference(connection,[status(thm),parent(t223:1)],[t223:1,t221:2]) ).
cnf(t225,plain,
( ~ g_true_only(sK2(sK1),sK1)
| ~ sP3(sK1,sK2(sK1)) ),
inference(extension,[status(thm),parent(t223:2)],[f_1_34]) ).
cnf(t226,plain,
$false,
inference(connection,[status(thm),parent(t225:1)],[t225:1,t223:2]) ).
cnf(t227,plain,
g_true_only(sK2(sK1),sK1),
inference(lemma_extension,[status(thm),parent(t225:2)],[l1:1]) ).
cnf(t228,plain,
$false,
inference(connection,[status(thm),parent(t227:1)],[t227:1,t225:2]) ).
cnf(t229,plain,
( ~ sP0(sK2(sK1))
| ~ g_false_only(sK2(sK1),sK2(sK1)) ),
inference(extension,[status(thm),parent(t221:3)],[f_1_28]) ).
cnf(t230,plain,
$false,
inference(connection,[status(thm),parent(t229:1)],[t229:1,t221:3]) ).
cnf(t231,plain,
( ~ g_true_only(sK2(sK1),sK1)
| sP0(sK2(sK1)) ),
inference(extension,[status(thm),parent(t229:2)],[f_1_20]) ).
cnf(t232,plain,
$false,
inference(connection,[status(thm),parent(t231:1)],[t231:1,t229:2]) ).
cnf(t233,plain,
g_true_only(sK2(sK1),sK1),
inference(lemma_extension,[status(thm),parent(t231:2)],[l1:1]) ).
cnf(t234,plain,
$false,
inference(connection,[status(thm),parent(t233:1)],[t233:1,t231:2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO605+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 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.09/5.39 % Computer : n002.cluster.edu
% 0.09/5.39 % Model : x86_64 x86_64
% 0.09/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.39 % Memory : 8046.5625MB
% 0.09/5.39 % OS : Linux 6.8.0-71-generic
% 0.09/5.39 % CPULimit : 300
% 0.09/5.39 % WCLimit : 300
% 0.09/5.39 % DateTime : Sun Sep 20 07:39:07 UTC 2026
% 0.09/5.39 % CPUTime :
% 26.54/31.86 % SZS status Theorem for theBenchmark
% 26.54/31.86 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------