%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYO607+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Sun Sep 27 09:51:05 AM UTC 2026
% Result : Theorem 14.03s 2.17s
% Output : CNFRefutation 14.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 4
% Syntax : Number of formulae : 225 ( 7 unt; 0 def)
% Number of atoms : 1538 ( 0 equ)
% Maximal formula atoms : 33 ( 6 avg)
% Number of connectives : 1401 ( 88 ~;1278 |; 33 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-1 aty)
% Number of variables : 844 ( 475 sgn 55 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(nc6,conjecture,
( ( ~ ? [A] :
! [B] : g_true_only(A,B)
& ? [A] :
( ~ ? [B] : g_false_only(A,B)
& ? [B] : g_both(A,B) )
& ~ ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) )
& ? [A] :
( ~ ! [B] : g_true_only(A,B)
& ~ g_true_only(a,A)
& ( ( ~ ? [B] : g_false_only(A,B)
& ? [B] : g_both(A,B) )
| g_both(a,A) ) ) )
| ? [A] :
! [B] : g_true_only(A,B)
| ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) ) ),
file('theBenchmark.p',nc6) ).
fof(nc6_neg,negated_conjecture,
~ ( ( ~ ? [A] :
! [B] : g_true_only(A,B)
& ? [A] :
( ~ ? [B] : g_false_only(A,B)
& ? [B] : g_both(A,B) )
& ~ ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) )
& ? [A] :
( ~ ! [B] : g_true_only(A,B)
& ~ g_true_only(a,A)
& ( ( ~ ? [B] : g_false_only(A,B)
& ? [B] : g_both(A,B) )
| g_both(a,A) ) ) )
| ? [A] :
! [B] : g_true_only(A,B)
| ? [A] :
( ? [B] : g_false_only(A,B)
& g_false_only(a,A) ) ),
inference(assume_negation,[status(cth)],[nc6]) ).
cnf(c_7,plain,
( g_true(A,B)
| ~ g_true_only(A,B) ),
inference(clausify,[status(thm)],[true_only_g]) ).
cnf(c_10,plain,
( ~ g_true(A,B)
| ~ g_false_only(A,B) ),
inference(clausify,[status(thm)],[false_only_g]) ).
cnf(c_14,plain,
( ~ g_true_only(A,B)
| ~ g_false_only(A,B) ),
inference(resolve,[status(thm)],[c_10,c_7]) ).
fof(nnf_5,plain,
( ( ? [A] :
! [B] : g_true_only(A,B)
| ! [X10] :
( ? [X12] : g_false_only(X10,X12)
| ! [X11] : ~ g_both(X10,X11) )
| ? [X8] :
( ? [X9] : g_false_only(X8,X9)
& g_false_only(a,X8) )
| ! [X4] :
( ! [X7] : g_true_only(X4,X7)
| g_true_only(a,X4)
| ( ( ? [X6] : g_false_only(X4,X6)
| ! [X5] : ~ g_both(X4,X5) )
& ~ g_both(a,X4) ) ) )
& ! [X2] :
? [X3] : ~ g_true_only(X2,X3)
& ! [X0] :
( ! [X1] : ~ g_false_only(X0,X1)
| ~ g_false_only(a,X0) ) ),
inference(fof_nnf,[status(thm)],[nc6_neg]) ).
fof(sk_nc6_neg_sk,plain,
( ( ! [B] : g_true_only(sK4,B)
| ! [X10] :
( g_false_only(X10,sK3(X10))
| ! [X11] : ~ g_both(X10,X11) )
| ( g_false_only(sK1,sK2)
& g_false_only(a,sK1) )
| ! [X4] :
( ! [X7] : g_true_only(X4,X7)
| g_true_only(a,X4)
| ( ( g_false_only(X4,sK0(X4))
| ! [X5] : ~ g_both(X4,X5) )
& ~ g_both(a,X4) ) ) )
& ! [X2] : ~ g_true_only(X2,sK5(X2))
& ! [X0] :
( ! [X1] : ~ g_false_only(X0,X1)
| ~ g_false_only(a,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK0,sK1,sK2,sK3,sK4]),skolemize(X3,sK5(X2)),skolemize(X6,sK0(X4)),skolemize(X8,sK1),skolemize(X9,sK2),skolemize(X12,sK3(X10)),skolemize(A,sK4)],[nnf_5]) ).
fof(sk_nc6_neg,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( g_true_only(sK4,VAR_5)
| g_false_only(VAR_3,sK3(VAR_3))
| ~ g_both(VAR_3,VAR_4)
| g_false_only(sK1,sK2)
| g_true_only(VAR_0,VAR_2)
| g_true_only(a,VAR_0)
| g_false_only(VAR_0,sK0(VAR_0))
| ~ g_both(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( g_true_only(sK4,VAR_5)
| g_false_only(VAR_3,sK3(VAR_3))
| ~ g_both(VAR_3,VAR_4)
| g_false_only(a,sK1)
| g_true_only(VAR_0,VAR_2)
| g_true_only(a,VAR_0)
| g_false_only(VAR_0,sK0(VAR_0))
| ~ g_both(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( g_true_only(sK4,VAR_4)
| g_false_only(VAR_2,sK3(VAR_2))
| ~ g_both(VAR_2,VAR_3)
| g_false_only(sK1,sK2)
| g_true_only(VAR_0,VAR_1)
| g_true_only(a,VAR_0)
| ~ g_both(a,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( g_true_only(sK4,VAR_4)
| g_false_only(VAR_2,sK3(VAR_2))
| ~ g_both(VAR_2,VAR_3)
| g_false_only(a,sK1)
| g_true_only(VAR_0,VAR_1)
| g_true_only(a,VAR_0)
| ~ g_both(a,VAR_0) )
& ! [VAR_0] : ~ g_true_only(VAR_0,sK5(VAR_0))
& ! [VAR_0,VAR_1] :
( ~ g_false_only(VAR_0,VAR_1)
| ~ g_false_only(a,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_nc6_neg_sk]) ).
cnf(c_17,negated_conjecture,
( g_true_only(sK4,F)
| g_false_only(D,sK3(D))
| ~ g_both(D,E)
| g_false_only(sK1,sK2)
| g_true_only(A,C)
| g_true_only(a,A)
| g_false_only(A,sK0(A))
| ~ g_both(A,B) ),
inference(split_conjunct,[status(thm)],[sk_nc6_neg]) ).
cnf(c_18,negated_conjecture,
( g_true_only(sK4,F)
| g_false_only(D,sK3(D))
| ~ g_both(D,E)
| g_false_only(a,sK1)
| g_true_only(A,C)
| g_true_only(a,A)
| g_false_only(A,sK0(A))
| ~ g_both(A,B) ),
inference(split_conjunct,[status(thm)],[sk_nc6_neg]) ).
cnf(c_19,negated_conjecture,
( g_true_only(sK4,E)
| g_false_only(C,sK3(C))
| ~ g_both(C,D)
| g_false_only(sK1,sK2)
| g_true_only(A,B)
| g_true_only(a,A)
| ~ g_both(a,A) ),
inference(split_conjunct,[status(thm)],[sk_nc6_neg]) ).
cnf(c_20,negated_conjecture,
( g_true_only(sK4,E)
| g_false_only(C,sK3(C))
| ~ g_both(C,D)
| g_false_only(a,sK1)
| g_true_only(A,B)
| g_true_only(a,A)
| ~ g_both(a,A) ),
inference(split_conjunct,[status(thm)],[sk_nc6_neg]) ).
cnf(c_21,negated_conjecture,
~ g_true_only(A,sK5(A)),
inference(split_conjunct,[status(thm)],[sk_nc6_neg]) ).
cnf(c_22,negated_conjecture,
( ~ g_false_only(A,B)
| ~ g_false_only(a,A) ),
inference(split_conjunct,[status(thm)],[sk_nc6_neg]) ).
cnf(c_23,plain,
( g_false_only(A,B)
| g_both(A,B)
| g_true_only(A,B) ),
inference(clausify,[status(thm)],[exhaustion_g]) ).
cnf(c_27,plain,
( g_true_only(sK4,D)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(A,C)
| g_true_only(a,A)
| g_false_only(A,sK0(A))
| ~ g_both(A,B) ),
inference(factor,[status(thm)],[c_17]) ).
cnf(c_30,plain,
( g_true_only(sK4,D)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(A,C)
| g_true_only(a,A)
| g_false_only(A,sK0(A))
| ~ g_both(A,B) ),
inference(factor,[status(thm)],[c_18]) ).
cnf(c_33,plain,
( g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_false_only(sK1,sK2)
| g_true_only(A,B)
| g_true_only(a,A)
| ~ g_both(a,A) ),
inference(factor,[status(thm)],[c_19]) ).
cnf(c_36,plain,
( g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_false_only(a,sK1)
| g_true_only(A,B)
| g_true_only(a,A)
| ~ g_both(a,A) ),
inference(factor,[status(thm)],[c_20]) ).
cnf(c_48,plain,
( g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| ~ g_both(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_23,c_20]) ).
cnf(c_50,plain,
( g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(C,D)
| g_true_only(a,C)
| ~ g_both(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_23,c_19]) ).
cnf(c_52,plain,
( g_true_only(sK4,F)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,E)
| g_true_only(a,C)
| g_false_only(C,sK0(C))
| ~ g_both(C,D)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_23,c_18]) ).
cnf(c_54,plain,
( g_true_only(sK4,F)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(C,E)
| g_true_only(a,C)
| g_false_only(C,sK0(C))
| ~ g_both(C,D)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_23,c_17]) ).
cnf(c_136,plain,
( g_false_only(A,D)
| g_true_only(A,D)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(A,B)
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(resolve,[status(thm)],[c_27,c_23]) ).
cnf(c_141,plain,
( g_false_only(A,B)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(A,B)
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(factor,[status(thm)],[c_136]) ).
cnf(c_153,plain,
( g_false_only(A,D)
| g_true_only(A,D)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(A,B)
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(resolve,[status(thm)],[c_30,c_23]) ).
cnf(c_154,plain,
( g_true_only(A,sK0(A))
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(A,B)
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(factor,[status(thm)],[c_153]) ).
cnf(c_158,plain,
( g_false_only(A,B)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(A,B)
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(factor,[status(thm)],[c_153]) ).
cnf(c_161,plain,
( g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(A,sK0(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(factor,[status(thm)],[c_154]) ).
cnf(c_6070,plain,
( g_false_only(a,A)
| g_true_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_false_only(sK1,sK2)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(resolve,[status(thm)],[c_33,c_23]) ).
cnf(c_168,plain,
( g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_false_only(sK1,sK2)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6070]) ).
cnf(c_171,plain,
( g_true_only(sK4,B)
| g_false_only(a,sK3(a))
| g_false_only(sK1,sK2)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(factor,[status(thm)],[c_168]) ).
cnf(c_6071,plain,
( g_false_only(a,A)
| g_true_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_false_only(a,sK1)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(resolve,[status(thm)],[c_36,c_23]) ).
cnf(c_172,plain,
( g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_false_only(a,sK1)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6071]) ).
cnf(c_175,plain,
( g_true_only(sK4,B)
| g_false_only(a,sK3(a))
| g_false_only(a,sK1)
| g_true_only(sK1,A)
| g_true_only(a,sK1) ),
inference(factor,[status(thm)],[c_172]) ).
cnf(c_176,plain,
( g_true_only(sK4,B)
| g_false_only(a,sK3(a))
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(factor,[status(thm)],[c_172]) ).
cnf(c_6072,plain,
( g_false_only(a,C)
| g_true_only(a,C)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_48,c_23]) ).
cnf(c_177,plain,
( g_false_only(a,C)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6072]) ).
cnf(c_6073,plain,
( g_false_only(a,C)
| g_true_only(a,C)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_50,c_23]) ).
cnf(c_197,plain,
( g_false_only(a,C)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6073]) ).
cnf(c_198,plain,
( g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_197]) ).
cnf(c_205,plain,
( g_false_only(a,A)
| g_true_only(sK4,B)
| g_false_only(sK1,sK2)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_198]) ).
cnf(c_220,plain,
( g_false_only(C,F)
| g_true_only(C,F)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(C,sK0(C))
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_52,c_23]) ).
cnf(c_223,plain,
( g_false_only(B,E)
| g_true_only(B,E)
| g_true_only(sK4,D)
| g_false_only(a,sK1)
| g_true_only(B,C)
| g_true_only(a,B)
| g_false_only(B,sK0(B))
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_220]) ).
cnf(c_226,plain,
( g_false_only(C,D)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(C,sK0(C))
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_220]) ).
cnf(c_235,plain,
( g_false_only(B,C)
| g_true_only(sK4,D)
| g_false_only(a,sK1)
| g_true_only(B,C)
| g_true_only(a,B)
| g_false_only(B,sK0(B))
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_223]) ).
cnf(c_252,plain,
( g_false_only(C,F)
| g_true_only(C,F)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(C,sK0(C))
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_54,c_23]) ).
cnf(c_255,plain,
( g_false_only(B,E)
| g_true_only(B,E)
| g_true_only(sK4,D)
| g_false_only(sK1,sK2)
| g_true_only(B,C)
| g_true_only(a,B)
| g_false_only(B,sK0(B))
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_252]) ).
cnf(c_269,plain,
( g_false_only(B,C)
| g_true_only(sK4,D)
| g_false_only(sK1,sK2)
| g_true_only(B,C)
| g_true_only(a,B)
| g_false_only(B,sK0(B))
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_255]) ).
cnf(c_303,plain,
( ~ g_false_only(sK3(a),C)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK1,A)
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_175,c_22]) ).
cnf(c_378,plain,
( ~ g_false_only(a,sK1)
| g_true_only(sK4,B)
| g_false_only(a,sK3(a))
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(resolve,[status(thm)],[c_171,c_22]) ).
cnf(c_381,plain,
( ~ g_false_only(sK3(a),C)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(resolve,[status(thm)],[c_176,c_22]) ).
cnf(c_383,plain,
( ~ g_false_only(a,sK1)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(resolve,[status(thm)],[c_168,c_22]) ).
cnf(c_402,plain,
( ~ g_false_only(a,sK1)
| g_false_only(A,B)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_true_only(A,B)
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(resolve,[status(thm)],[c_141,c_22]) ).
cnf(c_413,plain,
( ~ g_true_only(A,sK3(A))
| g_false_only(A,B)
| g_true_only(sK4,C)
| g_false_only(sK1,sK2)
| g_true_only(A,B)
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(resolve,[status(thm)],[c_141,c_14]) ).
cnf(c_453,plain,
( ~ g_true_only(sK1,sK3(sK1))
| g_true_only(sK4,A)
| g_false_only(sK1,sK2)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1)
| g_false_only(sK1,sK0(sK1)) ),
inference(factor,[status(thm)],[c_413]) ).
cnf(c_6074,plain,
( g_true_only(sK4,D)
| g_false_only(a,sK1)
| g_true_only(sK3(a),C)
| g_true_only(a,sK3(a))
| g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a))
| g_false_only(sK3(a),sK0(sK3(a))) ),
inference(resolve,[status(thm)],[c_158,c_381]) ).
cnf(c_6075,plain,
( g_true_only(sK4,D)
| g_false_only(a,sK1)
| g_true_only(sK3(a),C)
| g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a))
| g_false_only(sK3(a),sK0(sK3(a))) ),
inference(copy,[status(thm)],[c_6074]) ).
cnf(c_502,plain,
( g_true_only(sK4,D)
| g_true_only(sK3(a),C)
| g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a))
| g_false_only(sK3(a),sK0(sK3(a))) ),
inference(copy,[status(thm)],[c_6075]) ).
cnf(c_548,plain,
( g_true_only(sK4,C)
| g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a))
| g_false_only(sK3(a),sK0(sK3(a))) ),
inference(factor,[status(thm)],[c_502]) ).
cnf(c_600,plain,
( g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a))
| g_false_only(sK3(a),sK0(sK3(a))) ),
inference(factor,[status(thm)],[c_548]) ).
cnf(c_6076,plain,
( g_true_only(sK4,F)
| g_false_only(a,sK1)
| g_true_only(sK1,E)
| g_true_only(a,sK1)
| g_false_only(a,B)
| g_true_only(sK4,D)
| g_false_only(sK3(a),sK3(sK3(a)))
| g_false_only(a,sK1)
| g_true_only(B,C)
| g_true_only(a,B)
| g_true_only(sK3(a),A) ),
inference(resolve,[status(thm)],[c_177,c_303]) ).
cnf(c_669,plain,
( g_true_only(sK4,F)
| g_true_only(sK1,E)
| g_true_only(a,sK1)
| g_false_only(a,B)
| g_true_only(sK4,D)
| g_false_only(sK3(a),sK3(sK3(a)))
| g_false_only(a,sK1)
| g_true_only(B,C)
| g_true_only(a,B)
| g_true_only(sK3(a),A) ),
inference(copy,[status(thm)],[c_6076]) ).
cnf(c_676,plain,
( g_true_only(sK4,V6)
| g_false_only(a,sK3(a))
| g_true_only(sK3(a),F)
| g_true_only(a,sK3(a))
| g_false_only(a,C)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_177,c_378]) ).
cnf(c_681,plain,
( ~ g_false_only(sK1,F)
| g_false_only(a,C)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_177,c_22]) ).
cnf(c_694,plain,
( ~ g_false_only(C,F)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_177,c_22]) ).
cnf(c_6077,plain,
( g_true_only(sK4,D)
| g_true_only(a,sK1)
| g_false_only(a,sK1)
| g_true_only(sK4,C)
| g_false_only(sK3(a),sK3(sK3(a)))
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(factor,[status(thm)],[c_669]) ).
cnf(c_6078,plain,
( g_true_only(sK4,D)
| g_true_only(a,sK1)
| g_true_only(sK4,C)
| g_false_only(sK3(a),sK3(sK3(a)))
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(copy,[status(thm)],[c_6077]) ).
cnf(c_706,plain,
( g_true_only(sK4,D)
| g_true_only(sK4,C)
| g_false_only(sK3(a),sK3(sK3(a)))
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(copy,[status(thm)],[c_6078]) ).
cnf(c_6079,plain,
( g_true_only(sK4,E)
| g_false_only(a,sK3(a))
| g_true_only(sK3(a),D)
| g_true_only(a,sK3(a))
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_false_only(a,A)
| g_true_only(a,A) ),
inference(factor,[status(thm)],[c_676]) ).
cnf(c_6080,plain,
( g_true_only(sK4,E)
| g_false_only(a,sK3(a))
| g_true_only(sK3(a),D)
| g_true_only(a,sK3(a))
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_false_only(a,A)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6079]) ).
cnf(c_733,plain,
( g_true_only(sK4,E)
| g_true_only(sK3(a),D)
| g_true_only(a,sK3(a))
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_false_only(a,A)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6080]) ).
cnf(c_817,plain,
( g_true_only(sK4,C)
| g_false_only(sK3(a),sK3(sK3(a)))
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(factor,[status(thm)],[c_706]) ).
cnf(c_6081,plain,
( g_true_only(sK4,C)
| g_true_only(a,sK3(a))
| g_true_only(sK4,B)
| g_false_only(a,sK3(a))
| g_true_only(sK3(a),A)
| g_false_only(a,sK3(a))
| g_true_only(a,sK3(a)) ),
inference(factor,[status(thm)],[c_733]) ).
cnf(c_6082,plain,
( g_true_only(sK4,C)
| g_true_only(a,sK3(a))
| g_true_only(sK4,B)
| g_true_only(sK3(a),A)
| g_false_only(a,sK3(a))
| g_true_only(a,sK3(a)) ),
inference(copy,[status(thm)],[c_6081]) ).
cnf(c_838,plain,
( g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_true_only(sK3(a),A)
| g_false_only(a,sK3(a))
| g_true_only(a,sK3(a)) ),
inference(copy,[status(thm)],[c_6082]) ).
cnf(c_909,plain,
( g_true_only(sK4,B)
| g_true_only(sK3(a),A)
| g_false_only(a,sK3(a))
| g_true_only(a,sK3(a)) ),
inference(factor,[status(thm)],[c_838]) ).
cnf(c_964,plain,
( ~ g_false_only(sK3(a),C)
| g_true_only(sK4,B)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(resolve,[status(thm)],[c_909,c_22]) ).
cnf(c_1089,plain,
( ~ g_true_only(A,sK3(A))
| g_false_only(a,C)
| g_true_only(sK4,E)
| g_false_only(sK1,sK2)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_197,c_14]) ).
cnf(c_2569,plain,
( g_false_only(a,F)
| g_true_only(sK4,V7)
| g_false_only(D,sK3(D))
| g_true_only(F,V6)
| g_true_only(a,F)
| g_false_only(D,E)
| g_true_only(D,E)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(resolve,[status(thm)],[c_383,c_177]) ).
cnf(c_6083,plain,
( g_false_only(a,D)
| g_true_only(sK4,F)
| g_false_only(a,sK3(a))
| g_true_only(D,E)
| g_true_only(a,D)
| g_false_only(a,A)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(factor,[status(thm)],[c_2569]) ).
cnf(c_6084,plain,
( g_false_only(a,D)
| g_true_only(sK4,F)
| g_false_only(a,sK3(a))
| g_true_only(D,E)
| g_true_only(a,D)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6083]) ).
cnf(c_2609,plain,
( g_false_only(a,D)
| g_true_only(sK4,F)
| g_true_only(D,E)
| g_true_only(a,D)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6084]) ).
cnf(c_6085,plain,
( g_false_only(a,A)
| g_true_only(sK4,D)
| g_true_only(a,A)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(factor,[status(thm)],[c_2609]) ).
cnf(c_6086,plain,
( g_false_only(a,A)
| g_true_only(sK4,D)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6085]) ).
cnf(c_2652,plain,
( g_true_only(sK4,D)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6086]) ).
cnf(c_2667,plain,
( g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(factor,[status(thm)],[c_2652]) ).
cnf(c_2669,plain,
( ~ g_false_only(sK3(a),D)
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(resolve,[status(thm)],[c_2667,c_22]) ).
cnf(c_2677,plain,
( ~ g_false_only(A,D)
| g_true_only(sK4,C)
| g_false_only(a,sK3(a))
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(resolve,[status(thm)],[c_2667,c_22]) ).
cnf(c_2735,plain,
( g_true_only(sK4,E)
| g_false_only(D,sK3(D))
| g_true_only(D,sK0(D))
| g_true_only(a,D)
| g_false_only(D,sK0(D))
| g_false_only(A,B)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_true_only(A,B)
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(resolve,[status(thm)],[c_402,c_161]) ).
cnf(c_6087,plain,
( g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A))
| g_false_only(A,sK0(A))
| g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_true_only(A,sK0(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(factor,[status(thm)],[c_2735]) ).
cnf(c_6088,plain,
( g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A))
| g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_true_only(A,sK0(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(copy,[status(thm)],[c_6087]) ).
cnf(c_6089,plain,
( g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_true_only(a,A)
| g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_true_only(A,sK0(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(copy,[status(thm)],[c_6088]) ).
cnf(c_6090,plain,
( g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_true_only(A,sK0(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(copy,[status(thm)],[c_6089]) ).
cnf(c_2788,plain,
( g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_true_only(A,sK0(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(copy,[status(thm)],[c_6090]) ).
cnf(c_2826,plain,
( g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_true_only(A,sK0(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(factor,[status(thm)],[c_2788]) ).
cnf(c_3662,plain,
( ~ g_true_only(A,sK3(A))
| g_true_only(sK4,B)
| g_true_only(A,sK0(A))
| g_true_only(a,A)
| g_false_only(A,sK0(A)) ),
inference(resolve,[status(thm)],[c_2826,c_14]) ).
cnf(c_6091,plain,
( g_true_only(sK4,D)
| g_true_only(sK3(a),C)
| g_true_only(a,sK3(a))
| g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(resolve,[status(thm)],[c_600,c_964]) ).
cnf(c_3699,plain,
( g_true_only(sK4,D)
| g_true_only(sK3(a),C)
| g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(copy,[status(thm)],[c_6091]) ).
cnf(c_3710,plain,
( g_true_only(sK4,C)
| g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(factor,[status(thm)],[c_3699]) ).
cnf(c_3718,plain,
( g_false_only(sK3(a),A)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(factor,[status(thm)],[c_3710]) ).
cnf(c_3793,plain,
( g_false_only(a,F)
| g_true_only(sK4,V6)
| g_true_only(a,F)
| g_false_only(F,sK3(F))
| g_true_only(F,sK3(F))
| g_false_only(a,C)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_681,c_205]) ).
cnf(c_3827,plain,
( g_false_only(a,D)
| g_true_only(sK4,E)
| g_true_only(a,D)
| g_false_only(D,sK3(D))
| g_true_only(D,sK3(D))
| g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_3793]) ).
cnf(c_6092,plain,
( g_false_only(a,A)
| g_true_only(sK4,C)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_false_only(a,A)
| g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_3827]) ).
cnf(c_6093,plain,
( g_false_only(a,A)
| g_true_only(sK4,C)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_false_only(a,A)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6092]) ).
cnf(c_6094,plain,
( g_false_only(a,A)
| g_true_only(sK4,C)
| g_true_only(a,A)
| g_false_only(a,A)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6093]) ).
cnf(c_6095,plain,
( g_false_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,A)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6094]) ).
cnf(c_3903,plain,
( g_true_only(sK4,C)
| g_false_only(a,A)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6095]) ).
cnf(c_3957,plain,
( g_false_only(a,A)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_3903]) ).
cnf(c_3998,plain,
( ~ g_false_only(A,C)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(resolve,[status(thm)],[c_3957,c_22]) ).
cnf(c_6096,plain,
( g_false_only(C,V6)
| g_true_only(sK4,V7)
| g_false_only(a,sK1)
| g_true_only(C,V6)
| g_true_only(a,C)
| g_false_only(F,sK3(F))
| g_true_only(F,sK3(F))
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_694,c_235]) ).
cnf(c_6097,plain,
( g_false_only(C,V6)
| g_true_only(sK4,V7)
| g_false_only(a,sK1)
| g_true_only(C,V6)
| g_false_only(F,sK3(F))
| g_true_only(F,sK3(F))
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6096]) ).
cnf(c_4038,plain,
( g_false_only(C,V6)
| g_true_only(sK4,V7)
| g_true_only(C,V6)
| g_false_only(F,sK3(F))
| g_true_only(F,sK3(F))
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6097]) ).
cnf(c_6098,plain,
( g_false_only(C,V7)
| g_true_only(sK4,V8)
| g_false_only(F,sK3(F))
| g_false_only(a,sK1)
| g_true_only(C,V7)
| g_true_only(a,C)
| g_false_only(F,V6)
| g_true_only(F,V6)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_694,c_226]) ).
cnf(c_6099,plain,
( g_false_only(C,V7)
| g_true_only(sK4,V8)
| g_false_only(F,sK3(F))
| g_false_only(a,sK1)
| g_true_only(C,V7)
| g_false_only(F,V6)
| g_true_only(F,V6)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6098]) ).
cnf(c_4042,plain,
( g_false_only(C,V7)
| g_true_only(sK4,V8)
| g_false_only(F,sK3(F))
| g_true_only(C,V7)
| g_false_only(F,V6)
| g_true_only(F,V6)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(C,D)
| g_true_only(a,C)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6099]) ).
cnf(c_4130,plain,
( g_false_only(A,E)
| g_true_only(sK4,F)
| g_true_only(A,E)
| g_false_only(D,sK3(D))
| g_true_only(D,sK3(D))
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_4038]) ).
cnf(c_4143,plain,
( g_false_only(A,F)
| g_true_only(sK4,V6)
| g_false_only(D,sK3(D))
| g_true_only(A,F)
| g_false_only(D,E)
| g_true_only(D,E)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_4042]) ).
cnf(c_6100,plain,
( g_false_only(A,C)
| g_true_only(sK4,D)
| g_true_only(A,C)
| g_false_only(A,sK3(A))
| g_true_only(sK4,B)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_4130]) ).
cnf(c_6101,plain,
( g_false_only(A,C)
| g_true_only(sK4,D)
| g_true_only(A,C)
| g_false_only(A,sK3(A))
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6100]) ).
cnf(c_4243,plain,
( g_false_only(A,C)
| g_true_only(sK4,D)
| g_true_only(A,C)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6101]) ).
cnf(c_6102,plain,
( g_false_only(A,D)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_true_only(A,D)
| g_false_only(A,B)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_4143]) ).
cnf(c_6103,plain,
( g_false_only(A,D)
| g_true_only(sK4,E)
| g_false_only(A,sK3(A))
| g_true_only(A,D)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6102]) ).
cnf(c_4256,plain,
( g_false_only(A,D)
| g_true_only(sK4,E)
| g_true_only(A,D)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6103]) ).
cnf(c_6104,plain,
( g_false_only(A,sK3(A))
| g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_4243]) ).
cnf(c_4318,plain,
( g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6104]) ).
cnf(c_6105,plain,
( g_false_only(A,B)
| g_true_only(sK4,D)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_4256]) ).
cnf(c_4327,plain,
( g_true_only(sK4,D)
| g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6105]) ).
cnf(c_4339,plain,
( g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_4318]) ).
cnf(c_4340,plain,
( g_true_only(sK4,C)
| g_false_only(A,sK3(A))
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_4327]) ).
cnf(c_6106,plain,
( g_false_only(A,D)
| g_true_only(sK4,E)
| g_false_only(sK1,sK2)
| g_true_only(A,D)
| g_true_only(a,A)
| g_false_only(C,sK3(C))
| g_true_only(C,sK3(C))
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(resolve,[status(thm)],[c_3998,c_269]) ).
cnf(c_4384,plain,
( g_false_only(A,D)
| g_true_only(sK4,E)
| g_false_only(sK1,sK2)
| g_true_only(A,D)
| g_false_only(C,sK3(C))
| g_true_only(C,sK3(C))
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6106]) ).
cnf(c_4396,plain,
( g_false_only(A,D)
| g_false_only(sK1,sK2)
| g_true_only(A,D)
| g_false_only(C,sK3(C))
| g_true_only(C,sK3(C))
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_4384]) ).
cnf(c_6107,plain,
( g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A))
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_4396]) ).
cnf(c_6108,plain,
( g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_false_only(A,sK3(A))
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6107]) ).
cnf(c_6109,plain,
( g_false_only(A,sK3(A))
| g_false_only(sK1,sK2)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6108]) ).
cnf(c_4403,plain,
( g_false_only(sK1,sK2)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6109]) ).
cnf(c_4424,plain,
( ~ g_false_only(sK1,C)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(resolve,[status(thm)],[c_4339,c_22]) ).
cnf(c_4476,plain,
( g_true_only(sK4,D)
| g_true_only(a,C)
| g_false_only(C,sK3(C))
| g_true_only(C,sK3(C))
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(resolve,[status(thm)],[c_4424,c_4403]) ).
cnf(c_6110,plain,
( g_true_only(sK4,C)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_4476]) ).
cnf(c_6111,plain,
( g_true_only(sK4,C)
| g_true_only(a,A)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6110]) ).
cnf(c_4479,plain,
( g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(copy,[status(thm)],[c_6111]) ).
cnf(c_4483,plain,
( g_true_only(sK4,B)
| g_true_only(a,A)
| g_false_only(A,sK3(A))
| g_true_only(A,sK3(A)) ),
inference(factor,[status(thm)],[c_4479]) ).
cnf(c_4490,plain,
( ~ g_false_only(a,A)
| g_true_only(sK4,B)
| g_true_only(a,A)
| g_true_only(A,sK3(A)) ),
inference(resolve,[status(thm)],[c_4483,c_22]) ).
cnf(c_6112,plain,
( g_true_only(sK4,D)
| g_true_only(sK3(a),C)
| g_true_only(a,sK3(a))
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(resolve,[status(thm)],[c_3718,c_964]) ).
cnf(c_4552,plain,
( g_true_only(sK4,D)
| g_true_only(sK3(a),C)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(copy,[status(thm)],[c_6112]) ).
cnf(c_4563,plain,
( g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(factor,[status(thm)],[c_4552]) ).
cnf(c_4568,plain,
( g_true_only(sK4,B)
| g_false_only(a,sK1)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(factor,[status(thm)],[c_4563]) ).
cnf(c_4582,plain,
( ~ g_true_only(a,sK1)
| g_true_only(sK4,B)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(resolve,[status(thm)],[c_4568,c_14]) ).
cnf(c_4597,plain,
( g_false_only(a,D)
| g_true_only(sK4,F)
| g_true_only(D,E)
| g_true_only(a,D)
| g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(resolve,[status(thm)],[c_817,c_2669]) ).
cnf(c_6113,plain,
( g_false_only(a,sK1)
| g_true_only(sK4,D)
| g_true_only(a,sK1)
| g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(factor,[status(thm)],[c_4597]) ).
cnf(c_6114,plain,
( g_false_only(a,sK1)
| g_true_only(sK4,D)
| g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(copy,[status(thm)],[c_6113]) ).
cnf(c_4609,plain,
( g_true_only(sK4,D)
| g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(copy,[status(thm)],[c_6114]) ).
cnf(c_4616,plain,
( g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(factor,[status(thm)],[c_4609]) ).
cnf(c_6115,plain,
( g_true_only(sK4,D)
| g_true_only(a,sK1)
| g_true_only(sK1,sK3(sK1))
| g_true_only(sK4,C)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(resolve,[status(thm)],[c_4616,c_4490]) ).
cnf(c_4726,plain,
( g_true_only(sK4,D)
| g_true_only(sK1,sK3(sK1))
| g_true_only(sK4,C)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(copy,[status(thm)],[c_6115]) ).
cnf(c_4736,plain,
( ~ g_false_only(sK1,D)
| g_true_only(sK4,C)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(resolve,[status(thm)],[c_4616,c_22]) ).
cnf(c_4737,plain,
( g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_true_only(sK1,sK3(sK1))
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(factor,[status(thm)],[c_4726]) ).
cnf(c_4755,plain,
( g_true_only(sK4,B)
| g_true_only(sK1,sK3(sK1))
| g_true_only(a,sK1)
| g_true_only(sK3(a),A) ),
inference(factor,[status(thm)],[c_4737]) ).
cnf(c_4764,plain,
( g_true_only(sK4,A)
| g_true_only(sK1,sK3(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4755,c_21]) ).
cnf(c_4766,plain,
( g_true_only(sK1,sK3(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4764,c_21]) ).
cnf(c_6116,plain,
( g_true_only(sK4,A)
| g_true_only(sK1,sK0(sK1))
| g_true_only(a,sK1)
| g_false_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4766,c_3662]) ).
cnf(c_4767,plain,
( g_true_only(sK4,A)
| g_true_only(sK1,sK0(sK1))
| g_false_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(copy,[status(thm)],[c_6116]) ).
cnf(c_6117,plain,
( g_true_only(sK4,A)
| g_false_only(sK1,sK2)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1)
| g_false_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4766,c_453]) ).
cnf(c_4772,plain,
( g_true_only(sK4,A)
| g_false_only(sK1,sK2)
| g_true_only(sK1,sK2)
| g_false_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(copy,[status(thm)],[c_6117]) ).
cnf(c_6118,plain,
( g_false_only(sK1,A)
| g_true_only(sK4,B)
| g_false_only(sK1,sK2)
| g_true_only(sK1,A)
| g_true_only(a,sK1)
| g_false_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4766,c_413]) ).
cnf(c_4773,plain,
( g_false_only(sK1,A)
| g_true_only(sK4,B)
| g_false_only(sK1,sK2)
| g_true_only(sK1,A)
| g_false_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(copy,[status(thm)],[c_6118]) ).
cnf(c_4778,plain,
( ~ g_false_only(a,sK1)
| g_true_only(sK4,A)
| g_true_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4767,c_22]) ).
cnf(c_6119,plain,
( g_true_only(sK4,D)
| g_true_only(sK1,C)
| g_true_only(a,sK1)
| g_true_only(sK3(a),B)
| g_true_only(sK4,A)
| g_true_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4778,c_4616]) ).
cnf(c_4783,plain,
( g_true_only(sK4,D)
| g_true_only(sK1,C)
| g_true_only(sK3(a),B)
| g_true_only(sK4,A)
| g_true_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(copy,[status(thm)],[c_6119]) ).
cnf(c_4784,plain,
( g_true_only(sK4,C)
| g_true_only(sK3(a),B)
| g_true_only(sK4,A)
| g_true_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(factor,[status(thm)],[c_4783]) ).
cnf(c_4786,plain,
( g_true_only(sK3(a),B)
| g_true_only(sK4,A)
| g_true_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(factor,[status(thm)],[c_4784]) ).
cnf(c_4788,plain,
( g_true_only(sK4,A)
| g_true_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4786,c_21]) ).
cnf(c_4789,plain,
( g_true_only(sK1,sK0(sK1))
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4788,c_21]) ).
cnf(c_5109,plain,
( ~ g_true_only(sK1,sK0(sK1))
| g_true_only(sK4,A)
| g_false_only(sK1,sK2)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4772,c_14]) ).
cnf(c_6120,plain,
( g_true_only(a,sK1)
| g_true_only(sK4,A)
| g_false_only(sK1,sK2)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_5109,c_4789]) ).
cnf(c_5236,plain,
( g_true_only(sK4,A)
| g_false_only(sK1,sK2)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(copy,[status(thm)],[c_6120]) ).
cnf(c_5246,plain,
( g_true_only(a,sK1)
| g_false_only(a,B)
| g_true_only(sK4,D)
| g_false_only(sK1,sK2)
| g_true_only(B,C)
| g_true_only(a,B)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(resolve,[status(thm)],[c_1089,c_4766]) ).
cnf(c_6121,plain,
( g_true_only(sK4,D)
| g_true_only(sK1,C)
| g_true_only(a,sK1)
| g_true_only(sK3(a),B)
| g_true_only(sK4,A)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_5236,c_4736]) ).
cnf(c_5250,plain,
( g_true_only(sK4,D)
| g_true_only(sK1,C)
| g_true_only(sK3(a),B)
| g_true_only(sK4,A)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(copy,[status(thm)],[c_6121]) ).
cnf(c_5261,plain,
( g_true_only(sK4,C)
| g_true_only(sK3(a),B)
| g_true_only(sK4,A)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(factor,[status(thm)],[c_5250]) ).
cnf(c_5275,plain,
( g_true_only(sK3(a),B)
| g_true_only(sK4,A)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(factor,[status(thm)],[c_5261]) ).
cnf(c_5282,plain,
( g_true_only(sK4,A)
| g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_5275,c_21]) ).
cnf(c_5283,plain,
( g_true_only(sK1,sK2)
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_5282,c_21]) ).
cnf(c_6122,plain,
( g_true_only(sK4,E)
| g_false_only(a,sK3(a))
| g_true_only(A,D)
| g_true_only(a,A)
| g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_4340,c_2677]) ).
cnf(c_5718,plain,
( g_true_only(sK4,E)
| g_false_only(a,sK3(a))
| g_true_only(A,D)
| g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(copy,[status(thm)],[c_6122]) ).
cnf(c_5736,plain,
( g_true_only(sK4,D)
| g_false_only(a,sK3(a))
| g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_5718]) ).
cnf(c_5747,plain,
( g_false_only(a,sK3(a))
| g_true_only(sK4,C)
| g_false_only(a,sK1)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(factor,[status(thm)],[c_5736]) ).
cnf(c_5754,plain,
( ~ g_false_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK4,B)
| g_false_only(sK1,sK2)
| g_true_only(sK1,A)
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_4773,c_22]) ).
cnf(c_6123,plain,
( g_false_only(sK1,D)
| g_true_only(sK4,E)
| g_false_only(sK1,sK2)
| g_true_only(sK1,D)
| g_true_only(a,sK1)
| g_true_only(a,sK1)
| g_true_only(sK4,C)
| g_false_only(sK1,sK2)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(resolve,[status(thm)],[c_5246,c_5754]) ).
cnf(c_6124,plain,
( g_false_only(sK1,D)
| g_true_only(sK4,E)
| g_false_only(sK1,sK2)
| g_true_only(sK1,D)
| g_true_only(a,sK1)
| g_true_only(sK4,C)
| g_false_only(sK1,sK2)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(copy,[status(thm)],[c_6123]) ).
cnf(c_6125,plain,
( g_false_only(sK1,D)
| g_true_only(sK4,E)
| g_false_only(sK1,sK2)
| g_true_only(sK1,D)
| g_true_only(sK4,C)
| g_false_only(sK1,sK2)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(copy,[status(thm)],[c_6124]) ).
cnf(c_5784,plain,
( g_false_only(sK1,D)
| g_true_only(sK4,E)
| g_true_only(sK1,D)
| g_true_only(sK4,C)
| g_false_only(sK1,sK2)
| g_true_only(sK1,B)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(copy,[status(thm)],[c_6125]) ).
cnf(c_5797,plain,
( g_false_only(sK1,C)
| g_true_only(sK4,D)
| g_true_only(sK1,C)
| g_true_only(sK4,B)
| g_false_only(sK1,sK2)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(factor,[status(thm)],[c_5784]) ).
cnf(c_6126,plain,
( g_false_only(sK1,A)
| g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_false_only(sK1,sK2)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(factor,[status(thm)],[c_5797]) ).
cnf(c_5812,plain,
( g_true_only(sK4,C)
| g_true_only(sK4,B)
| g_false_only(sK1,sK2)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(copy,[status(thm)],[c_6126]) ).
cnf(c_5819,plain,
( g_true_only(sK4,B)
| g_false_only(sK1,sK2)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(factor,[status(thm)],[c_5812]) ).
cnf(c_5836,plain,
( ~ g_true_only(sK1,sK2)
| g_true_only(sK4,B)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(resolve,[status(thm)],[c_5819,c_14]) ).
cnf(c_6127,plain,
( g_true_only(a,sK1)
| g_true_only(sK4,B)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(resolve,[status(thm)],[c_5836,c_5283]) ).
cnf(c_5877,plain,
( g_true_only(sK4,B)
| g_true_only(a,sK1)
| g_false_only(sK1,A)
| g_true_only(sK1,A) ),
inference(copy,[status(thm)],[c_6127]) ).
cnf(c_6128,plain,
( g_true_only(sK4,E)
| g_true_only(sK1,D)
| g_true_only(a,sK1)
| g_true_only(sK3(a),C)
| g_true_only(sK4,B)
| g_true_only(a,sK1)
| g_true_only(sK1,A) ),
inference(resolve,[status(thm)],[c_5877,c_4736]) ).
cnf(c_5878,plain,
( g_true_only(sK4,E)
| g_true_only(sK1,D)
| g_true_only(sK3(a),C)
| g_true_only(sK4,B)
| g_true_only(a,sK1)
| g_true_only(sK1,A) ),
inference(copy,[status(thm)],[c_6128]) ).
cnf(c_5886,plain,
( g_true_only(sK4,D)
| g_true_only(sK3(a),C)
| g_true_only(sK4,B)
| g_true_only(a,sK1)
| g_true_only(sK1,A) ),
inference(factor,[status(thm)],[c_5878]) ).
cnf(c_5897,plain,
( g_true_only(sK3(a),C)
| g_true_only(sK4,B)
| g_true_only(a,sK1)
| g_true_only(sK1,A) ),
inference(factor,[status(thm)],[c_5886]) ).
cnf(c_5906,plain,
( g_true_only(sK4,B)
| g_true_only(a,sK1)
| g_true_only(sK1,A) ),
inference(resolve,[status(thm)],[c_5897,c_21]) ).
cnf(c_5907,plain,
( g_true_only(sK4,A)
| g_true_only(a,sK1) ),
inference(resolve,[status(thm)],[c_5906,c_21]) ).
cnf(c_5909,plain,
g_true_only(a,sK1),
inference(resolve,[status(thm)],[c_5907,c_21]) ).
cnf(c_5911,plain,
( g_true_only(sK4,B)
| g_true_only(sK3(a),A)
| g_true_only(a,sK3(a)) ),
inference(resolve,[status(thm)],[c_5909,c_4582]) ).
cnf(c_5919,plain,
~ g_false_only(a,sK1),
inference(resolve,[status(thm)],[c_14,c_5909]) ).
cnf(c_5921,plain,
( g_false_only(a,sK3(a))
| g_true_only(sK4,C)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_5919,c_5747]) ).
cnf(c_6016,plain,
( g_true_only(sK4,A)
| g_true_only(a,sK3(a)) ),
inference(resolve,[status(thm)],[c_5911,c_21]) ).
cnf(c_6018,plain,
g_true_only(a,sK3(a)),
inference(resolve,[status(thm)],[c_6016,c_21]) ).
cnf(c_6023,plain,
~ g_false_only(a,sK3(a)),
inference(resolve,[status(thm)],[c_14,c_6018]) ).
cnf(c_6026,plain,
( g_true_only(sK4,C)
| g_true_only(a,A)
| g_false_only(A,B)
| g_true_only(A,B) ),
inference(resolve,[status(thm)],[c_6023,c_5921]) ).
cnf(c_6027,plain,
( ~ g_false_only(A,D)
| g_true_only(sK4,C)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(resolve,[status(thm)],[c_6023,c_2677]) ).
cnf(c_6129,plain,
( g_true_only(sK4,E)
| g_true_only(a,A)
| g_true_only(A,D)
| g_true_only(sK4,C)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(resolve,[status(thm)],[c_6027,c_6026]) ).
cnf(c_6058,plain,
( g_true_only(sK4,E)
| g_true_only(A,D)
| g_true_only(sK4,C)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(copy,[status(thm)],[c_6129]) ).
cnf(c_6060,plain,
( g_true_only(sK4,D)
| g_true_only(sK4,C)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(factor,[status(thm)],[c_6058]) ).
cnf(c_6062,plain,
( g_true_only(sK4,C)
| g_true_only(A,B)
| g_true_only(a,A) ),
inference(factor,[status(thm)],[c_6060]) ).
cnf(c_6064,plain,
( g_true_only(sK4,B)
| g_true_only(sK5(a),A) ),
inference(resolve,[status(thm)],[c_6062,c_21]) ).
cnf(c_6068,plain,
g_true_only(sK4,A),
inference(resolve,[status(thm)],[c_6064,c_21]) ).
cnf(c_6069,plain,
$false,
inference(resolve,[status(thm)],[c_6068,c_21]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO607+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 19:37:18 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 2031708 was started by sandbox on n019,
% 0.09/0.35 % Sat Sep 26 19:37:18 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.36
% 0.09/0.36 % From the command line: assign(max_seconds, 300).
% 14.03/2.17
% 14.03/2.17 % given #500 (T,wt=26): 4342 g_true_only(c3,A) | g_true_only(a,c3) | g_false_only(a,c1) | g_false_only(c3,f3(c3)) | g_false(c3,A). [resolve(4337,b,24,a)].
% 14.03/2.17
% 14.03/2.17 % SZS status Theorem for theBenchmark
% 14.03/2.17
% 14.03/2.17 % Proof 1 at 1.44 (+ 0.26) seconds.
% 14.03/2.17 % Length of proof is 161.
% 14.03/2.17 % Level of proof is 53.
% 14.03/2.17 % Maximum clause weight is 51.000.
% 14.03/2.17 % Given clauses 825.
% 14.03/2.17
% 14.03/2.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------