%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT345+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 07:50:20 AM UTC 2026
% Result : Theorem 14.53s 2.55s
% Output : CNFRefutation 14.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 18
% Syntax : Number of formulae : 202 ( 59 unt; 0 def)
% Number of atoms : 601 ( 150 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 680 ( 281 ~; 324 |; 48 &)
% ( 2 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-3 aty)
% Number of variables : 178 ( 32 sgn 42 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v4_conlat_1,axiom,
! [A] :
( l2_conlat_1(A)
=> ( v4_conlat_1(A)
=> A = g2_conlat_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A)) ) ),
file('theBenchmark.p',abstractness_v4_conlat_1) ).
fof(abstractness_v6_conlat_1,axiom,
! [A,B] :
( ( l3_conlat_1(B,A)
& l1_conlat_1(A) )
=> ( v6_conlat_1(B,A)
=> B = g3_conlat_1(A,u4_conlat_1(A,B),u5_conlat_1(A,B)) ) ),
file('theBenchmark.p',abstractness_v6_conlat_1) ).
fof(cc1_relset_1,axiom,
! [A,B,C] :
( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))
=> v1_relat_1(C) ),
file('theBenchmark.p',cc1_relset_1) ).
fof(d7_conlat_2,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> k7_conlat_2(A) = g2_conlat_1(u2_conlat_1(A),u1_conlat_1(A),k6_relset_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A))) ),
file('theBenchmark.p',d7_conlat_2) ).
fof(d8_conlat_2,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( l3_conlat_1(B,A)
=> ! [C] :
( ( l3_conlat_1(C,k7_conlat_2(A))
& v6_conlat_1(C,k7_conlat_2(A)) )
=> ( C = k8_conlat_2(A,B)
<=> ( u5_conlat_1(k7_conlat_2(A),C) = u4_conlat_1(A,B)
& u4_conlat_1(k7_conlat_2(A),C) = u5_conlat_1(A,B) ) ) ) ) ),
file('theBenchmark.p',d8_conlat_2) ).
fof(dt_k6_relset_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> m2_relset_1(k6_relset_1(A,B,C),B,A) ),
file('theBenchmark.p',dt_k6_relset_1) ).
fof(dt_k7_conlat_2,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l2_conlat_1(k7_conlat_2(A))
& v4_conlat_1(k7_conlat_2(A))
& ~ v3_conlat_1(k7_conlat_2(A)) ) ),
file('theBenchmark.p',dt_k7_conlat_2) ).
fof(dt_k8_conlat_2,axiom,
! [A,B] :
( ( l3_conlat_1(B,A)
& l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
& v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A)) ) ),
file('theBenchmark.p',dt_k8_conlat_2) ).
fof(dt_k9_conlat_2,axiom,
! [A,B] :
( ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& v9_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& ~ v7_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
& v6_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A)) ) ),
file('theBenchmark.p',dt_k9_conlat_2) ).
fof(dt_l2_conlat_1,axiom,
! [A] :
( l2_conlat_1(A)
=> l1_conlat_1(A) ),
file('theBenchmark.p',dt_l2_conlat_1) ).
fof(dt_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ),
file('theBenchmark.p',dt_m2_relset_1) ).
fof(dt_u3_conlat_1,axiom,
! [A] :
( l2_conlat_1(A)
=> m2_relset_1(u3_conlat_1(A),u1_conlat_1(A),u2_conlat_1(A)) ),
file('theBenchmark.p',dt_u3_conlat_1) ).
fof(free_g2_conlat_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> ! [D,E,F] :
( g2_conlat_1(A,B,C) = g2_conlat_1(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('theBenchmark.p',free_g2_conlat_1) ).
fof(involutiveness_k4_relat_1,axiom,
! [A] :
( v1_relat_1(A)
=> k4_relat_1(k4_relat_1(A)) = A ),
file('theBenchmark.p',involutiveness_k4_relat_1) ).
fof(redefinition_k6_relset_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> k6_relset_1(A,B,C) = k4_relat_1(C) ),
file('theBenchmark.p',redefinition_k6_relset_1) ).
fof(redefinition_k9_conlat_2,axiom,
! [A,B] :
( ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> k9_conlat_2(A,B) = k8_conlat_2(A,B) ),
file('theBenchmark.p',redefinition_k9_conlat_2) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t20_conlat_2,conjecture,
! [A] :
( ( l2_conlat_1(A)
& v4_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& v6_conlat_1(B,A) )
=> k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B)) = B ) ),
file('theBenchmark.p',t20_conlat_2) ).
fof(t20_conlat_2_neg,negated_conjecture,
~ ! [A] :
( ( l2_conlat_1(A)
& v4_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& v6_conlat_1(B,A) )
=> k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B)) = B ) ),
inference(assume_negation,[status(cth)],[t20_conlat_2]) ).
cnf(c_70,plain,
( g2_conlat_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A)) = A
| ~ v4_conlat_1(A)
| ~ l2_conlat_1(A) ),
inference(clausify,[status(thm)],[abstractness_v4_conlat_1]) ).
cnf(c_71,plain,
( v4_conlat_1(k7_conlat_2(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k7_conlat_2]) ).
fof(nnf_68,plain,
? [A] :
( ? [B] :
( k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B)) != B
& l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& v6_conlat_1(B,A) )
& l2_conlat_1(A)
& v4_conlat_1(A)
& ~ v3_conlat_1(A) ),
inference(fof_nnf,[status(thm)],[t20_conlat_2_neg]) ).
fof(sk_t20_conlat_2_neg,plain,
( k9_conlat_2(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)) != sK1
& l3_conlat_1(sK1,sK0)
& v9_conlat_1(sK1,sK0)
& ~ v7_conlat_1(sK1,sK0)
& v6_conlat_1(sK1,sK0)
& l2_conlat_1(sK0)
& v4_conlat_1(sK0)
& ~ v3_conlat_1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_68]) ).
cnf(c_74,negated_conjecture,
v4_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t20_conlat_2_neg]) ).
cnf(c_96,plain,
( l1_conlat_1(A)
| ~ l2_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_l2_conlat_1]) ).
cnf(c_100,plain,
( g3_conlat_1(A,u4_conlat_1(A,B),u5_conlat_1(A,B)) = B
| ~ v6_conlat_1(B,A)
| ~ l3_conlat_1(B,A)
| ~ l1_conlat_1(A) ),
inference(clausify,[status(thm)],[abstractness_v6_conlat_1]) ).
cnf(c_101,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_104,plain,
( k4_relat_1(A) = k6_relset_1(B,C,A)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_k6_relset_1]) ).
cnf(c_106,plain,
( F = A
| g2_conlat_1(D,E,F) != g2_conlat_1(B,C,A)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[free_g2_conlat_1]) ).
cnf(c_107,plain,
( E = C
| g2_conlat_1(D,E,F) != g2_conlat_1(B,C,A)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[free_g2_conlat_1]) ).
cnf(c_108,plain,
( D = B
| g2_conlat_1(D,E,F) != g2_conlat_1(B,C,A)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[free_g2_conlat_1]) ).
cnf(c_110,plain,
( m2_relset_1(k6_relset_1(B,C,A),C,B)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[dt_k6_relset_1]) ).
cnf(c_116,negated_conjecture,
( g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = sK0
| ~ l2_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_74,c_70]) ).
cnf(c_119,plain,
( g2_conlat_1(u1_conlat_1(k7_conlat_2(A)),u2_conlat_1(k7_conlat_2(A)),u3_conlat_1(k7_conlat_2(A))) = k7_conlat_2(A)
| ~ l2_conlat_1(k7_conlat_2(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(resolve,[status(thm)],[c_71,c_70]) ).
cnf(c_120,negated_conjecture,
k9_conlat_2(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)) != sK1,
inference(split_conjunct,[status(thm)],[sk_t20_conlat_2_neg]) ).
cnf(c_121,negated_conjecture,
l3_conlat_1(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t20_conlat_2_neg]) ).
cnf(c_122,negated_conjecture,
v9_conlat_1(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t20_conlat_2_neg]) ).
cnf(c_123,negated_conjecture,
~ v7_conlat_1(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t20_conlat_2_neg]) ).
cnf(c_124,negated_conjecture,
v6_conlat_1(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t20_conlat_2_neg]) ).
cnf(c_125,negated_conjecture,
l2_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t20_conlat_2_neg]) ).
cnf(c_126,negated_conjecture,
~ v3_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t20_conlat_2_neg]) ).
cnf(c_134,plain,
( k8_conlat_2(A,B) = k9_conlat_2(A,B)
| ~ l3_conlat_1(B,A)
| ~ v9_conlat_1(B,A)
| v7_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[redefinition_k9_conlat_2]) ).
cnf(c_135,plain,
( k9_conlat_2(A,B) = k8_conlat_2(A,B)
| ~ l3_conlat_1(B,A)
| ~ v9_conlat_1(B,A)
| v7_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(copy,[status(thm)],[c_134]) ).
cnf(c_152,plain,
( k4_relat_1(k4_relat_1(A)) = A
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[involutiveness_k4_relat_1]) ).
cnf(c_159,plain,
( m2_relset_1(u3_conlat_1(A),u1_conlat_1(A),u2_conlat_1(A))
| ~ l2_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_u3_conlat_1]) ).
cnf(c_160,plain,
( m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C)))
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[dt_m2_relset_1]) ).
cnf(c_161,plain,
( l3_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ v9_conlat_1(B,A)
| v7_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k9_conlat_2]) ).
cnf(c_162,plain,
( v9_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ v9_conlat_1(B,A)
| v7_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k9_conlat_2]) ).
cnf(c_163,plain,
( ~ v7_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ v9_conlat_1(B,A)
| v7_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k9_conlat_2]) ).
cnf(c_164,plain,
( v6_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ v9_conlat_1(B,A)
| v7_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k9_conlat_2]) ).
cnf(c_165,plain,
( l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k8_conlat_2]) ).
cnf(c_166,plain,
( v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k8_conlat_2]) ).
cnf(c_167,plain,
( l2_conlat_1(k7_conlat_2(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k7_conlat_2]) ).
cnf(c_168,plain,
( ~ v3_conlat_1(k7_conlat_2(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k7_conlat_2]) ).
cnf(c_171,plain,
( u5_conlat_1(k7_conlat_2(A),C) = u4_conlat_1(A,B)
| k8_conlat_2(A,B) != C
| ~ l3_conlat_1(C,k7_conlat_2(A))
| ~ v6_conlat_1(C,k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[d8_conlat_2]) ).
cnf(c_172,plain,
( u5_conlat_1(A,B) = u4_conlat_1(k7_conlat_2(A),C)
| k8_conlat_2(A,B) != C
| ~ l3_conlat_1(C,k7_conlat_2(A))
| ~ v6_conlat_1(C,k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[d8_conlat_2]) ).
cnf(c_173,plain,
( g2_conlat_1(u2_conlat_1(A),u1_conlat_1(A),k6_relset_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A))) = k7_conlat_2(A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[d7_conlat_2]) ).
cnf(c_174,plain,
( v1_relat_1(A)
| ~ m1_subset_1(A,k1_zfmisc_1(k2_zfmisc_1(B,C))) ),
inference(clausify,[status(thm)],[cc1_relset_1]) ).
cnf(c_221,plain,
( ~ l2_conlat_1(B)
| g3_conlat_1(B,u4_conlat_1(B,A),u5_conlat_1(B,A)) = A
| ~ v6_conlat_1(A,B)
| ~ l3_conlat_1(A,B) ),
inference(resolve,[status(thm)],[c_100,c_96]) ).
cnf(c_224,plain,
( ~ m2_relset_1(A,B,C)
| k4_relat_1(A) = k6_relset_1(B,C,A) ),
inference(resolve,[status(thm)],[c_104,c_101]) ).
cnf(c_225,plain,
( ~ m2_relset_1(C,A,B)
| k6_relset_1(A,B,C) = k4_relat_1(C) ),
inference(copy,[status(thm)],[c_224]) ).
cnf(c_227,plain,
( ~ m2_relset_1(F,D,E)
| C = F
| g2_conlat_1(A,B,C) != g2_conlat_1(D,E,F) ),
inference(resolve,[status(thm)],[c_106,c_101]) ).
cnf(c_228,plain,
( ~ m2_relset_1(F,D,E)
| B = E
| g2_conlat_1(A,B,C) != g2_conlat_1(D,E,F) ),
inference(resolve,[status(thm)],[c_107,c_101]) ).
cnf(c_229,plain,
( ~ m2_relset_1(F,D,E)
| A = D
| g2_conlat_1(A,B,C) != g2_conlat_1(D,E,F) ),
inference(resolve,[status(thm)],[c_108,c_101]) ).
cnf(c_243,plain,
( ~ m2_relset_1(C,A,B)
| m2_relset_1(k6_relset_1(A,B,C),B,A) ),
inference(resolve,[status(thm)],[c_110,c_101]) ).
cnf(c_246,negated_conjecture,
g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = sK0,
inference(resolve,[status(thm)],[c_125,c_116]) ).
cnf(c_12256,negated_conjecture,
( g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0))) = k7_conlat_2(sK0)
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_125,c_119]) ).
cnf(c_253,negated_conjecture,
( g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0))) = k7_conlat_2(sK0)
| ~ l2_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_126,c_12256]) ).
cnf(c_12257,negated_conjecture,
( k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1)
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_135,c_122]) ).
cnf(c_12258,negated_conjecture,
( k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1)
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_126,c_12257]) ).
cnf(c_12259,negated_conjecture,
( k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1)
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_125,c_12258]) ).
cnf(c_12260,negated_conjecture,
( k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1)
| ~ l3_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_123,c_12259]) ).
cnf(c_256,negated_conjecture,
k9_conlat_2(sK0,sK1) = k8_conlat_2(sK0,sK1),
inference(resolve,[status(thm)],[c_121,c_12260]) ).
cnf(c_257,negated_conjecture,
k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) != sK1,
inference(paramod,[status(thm)],[c_256,c_120]) ).
cnf(c_307,plain,
m2_relset_1(u3_conlat_1(sK0),u1_conlat_1(sK0),u2_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_159,c_125]) ).
cnf(c_12261,negated_conjecture,
( l3_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_122]) ).
cnf(c_12262,negated_conjecture,
( l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12261]) ).
cnf(c_12263,negated_conjecture,
( l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_126,c_12262]) ).
cnf(c_12264,negated_conjecture,
( l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_125,c_12263]) ).
cnf(c_12265,negated_conjecture,
( l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_123,c_12264]) ).
cnf(c_313,negated_conjecture,
l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_121,c_12265]) ).
cnf(c_12266,negated_conjecture,
( v9_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_162,c_122]) ).
cnf(c_12267,negated_conjecture,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12266]) ).
cnf(c_12268,negated_conjecture,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_126,c_12267]) ).
cnf(c_12269,negated_conjecture,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_125,c_12268]) ).
cnf(c_12270,negated_conjecture,
( v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_123,c_12269]) ).
cnf(c_318,negated_conjecture,
v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_121,c_12270]) ).
cnf(c_12271,negated_conjecture,
( ~ v7_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_163,c_122]) ).
cnf(c_12272,negated_conjecture,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12271]) ).
cnf(c_12273,negated_conjecture,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_126,c_12272]) ).
cnf(c_12274,negated_conjecture,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_125,c_12273]) ).
cnf(c_12275,negated_conjecture,
( ~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_123,c_12274]) ).
cnf(c_323,negated_conjecture,
~ v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_121,c_12275]) ).
cnf(c_12276,negated_conjecture,
( v6_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_164,c_122]) ).
cnf(c_12277,negated_conjecture,
( v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12276]) ).
cnf(c_12278,negated_conjecture,
( v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_126,c_12277]) ).
cnf(c_12279,negated_conjecture,
( v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| v7_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_125,c_12278]) ).
cnf(c_12280,negated_conjecture,
( v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_123,c_12279]) ).
cnf(c_328,negated_conjecture,
v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_121,c_12280]) ).
cnf(c_12281,negated_conjecture,
( l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_167,c_125]) ).
cnf(c_340,negated_conjecture,
l2_conlat_1(k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_126,c_12281]) ).
cnf(c_342,negated_conjecture,
g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0))) = k7_conlat_2(sK0),
inference(resolve,[status(thm)],[c_340,c_253]) ).
cnf(c_12282,negated_conjecture,
( ~ v3_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_125]) ).
cnf(c_346,negated_conjecture,
~ v3_conlat_1(k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_126,c_12282]) ).
cnf(c_357,plain,
( u5_conlat_1(k7_conlat_2(A),k8_conlat_2(A,B)) = u4_conlat_1(A,B)
| ~ l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
| ~ v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(xxres,[status(thm)],[c_171]) ).
cnf(c_12283,plain,
( u5_conlat_1(A,B) = u4_conlat_1(k7_conlat_2(A),k8_conlat_2(A,B))
| ~ l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
| ~ v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(xxres,[status(thm)],[c_172]) ).
cnf(c_363,plain,
( u4_conlat_1(k7_conlat_2(A),k8_conlat_2(A,B)) = u5_conlat_1(A,B)
| ~ l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
| ~ v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(copy,[status(thm)],[c_12283]) ).
cnf(c_12284,negated_conjecture,
( g2_conlat_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0))) = k7_conlat_2(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_173,c_125]) ).
cnf(c_367,negated_conjecture,
g2_conlat_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0))) = k7_conlat_2(sK0),
inference(resolve,[status(thm)],[c_126,c_12284]) ).
cnf(c_12285,negated_conjecture,
( ~ l2_conlat_1(sK0)
| g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = sK1
| ~ v6_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_221,c_121]) ).
cnf(c_12286,negated_conjecture,
( ~ l2_conlat_1(sK0)
| g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = sK1 ),
inference(resolve,[status(thm)],[c_124,c_12285]) ).
cnf(c_587,negated_conjecture,
g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = sK1,
inference(resolve,[status(thm)],[c_125,c_12286]) ).
cnf(c_12287,plain,
( u5_conlat_1(A,B) = u4_conlat_1(k7_conlat_2(A),C)
| C != k8_conlat_2(A,B)
| ~ l3_conlat_1(C,k7_conlat_2(A))
| ~ v6_conlat_1(C,k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(copy,[status(thm)],[c_172]) ).
cnf(c_12288,plain,
( u5_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_256,c_12287]) ).
cnf(c_12289,plain,
( u5_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12288]) ).
cnf(c_12290,plain,
( u5_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12289]) ).
cnf(c_12291,plain,
( u5_conlat_1(sK0,sK1) = u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12290]) ).
cnf(c_12292,plain,
( u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(copy,[status(thm)],[c_12291]) ).
cnf(c_12293,negated_conjecture,
( u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_126,c_12292]) ).
cnf(c_12294,negated_conjecture,
( u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_125,c_12293]) ).
cnf(c_12295,negated_conjecture,
( u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_121,c_12294]) ).
cnf(c_12296,negated_conjecture,
( u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_328,c_12295]) ).
cnf(c_708,negated_conjecture,
u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u5_conlat_1(sK0,sK1),
inference(resolve,[status(thm)],[c_313,c_12296]) ).
cnf(c_12297,plain,
( u5_conlat_1(k7_conlat_2(A),C) = u4_conlat_1(A,B)
| C != k8_conlat_2(A,B)
| ~ l3_conlat_1(C,k7_conlat_2(A))
| ~ v6_conlat_1(C,k7_conlat_2(A))
| ~ l3_conlat_1(B,A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(copy,[status(thm)],[c_171]) ).
cnf(c_12298,plain,
( u5_conlat_1(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_256,c_12297]) ).
cnf(c_12299,plain,
( u5_conlat_1(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k9_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12298]) ).
cnf(c_12300,plain,
( u5_conlat_1(k7_conlat_2(sK0),k9_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12299]) ).
cnf(c_12301,plain,
( u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_256,c_12300]) ).
cnf(c_12302,negated_conjecture,
( u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0)
| ~ l2_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_126,c_12301]) ).
cnf(c_12303,negated_conjecture,
( u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l3_conlat_1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_125,c_12302]) ).
cnf(c_12304,negated_conjecture,
( u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ v6_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_121,c_12303]) ).
cnf(c_12305,negated_conjecture,
( u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_328,c_12304]) ).
cnf(c_709,negated_conjecture,
u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = u4_conlat_1(sK0,sK1),
inference(resolve,[status(thm)],[c_313,c_12305]) ).
cnf(c_12306,plain,
( g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0)))) = k7_conlat_2(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_340,c_173]) ).
cnf(c_776,plain,
g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0)))) = k7_conlat_2(k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_346,c_12306]) ).
cnf(c_12307,plain,
( l2_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_340,c_167]) ).
cnf(c_781,plain,
l2_conlat_1(k7_conlat_2(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_346,c_12307]) ).
cnf(c_788,plain,
m2_relset_1(u3_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_340,c_159]) ).
cnf(c_12308,plain,
( v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_313,c_166]) ).
cnf(c_12309,plain,
( v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_346,c_12308]) ).
cnf(c_1132,plain,
v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_340,c_12309]) ).
cnf(c_12310,plain,
( l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_313,c_165]) ).
cnf(c_12311,plain,
( l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_346,c_12310]) ).
cnf(c_1133,plain,
l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_340,c_12311]) ).
cnf(c_12312,plain,
( k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_313,c_135]) ).
cnf(c_12313,plain,
( k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| ~ l2_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_346,c_12312]) ).
cnf(c_12314,plain,
( k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0))
| v7_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_340,c_12313]) ).
cnf(c_12315,plain,
( k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ v9_conlat_1(k8_conlat_2(sK0,sK1),k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_323,c_12314]) ).
cnf(c_1138,plain,
k9_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),
inference(resolve,[status(thm)],[c_318,c_12315]) ).
cnf(c_1141,negated_conjecture,
k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) != sK1,
inference(paramod,[status(thm)],[c_1138,c_257]) ).
cnf(c_1183,plain,
m2_relset_1(k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_307,c_243]) ).
cnf(c_1185,plain,
k6_relset_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = k4_relat_1(u3_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_307,c_225]) ).
cnf(c_1186,plain,
m1_subset_1(u3_conlat_1(sK0),k1_zfmisc_1(k2_zfmisc_1(u1_conlat_1(sK0),u2_conlat_1(sK0)))),
inference(resolve,[status(thm)],[c_307,c_160]) ).
cnf(c_1188,plain,
m2_relset_1(k4_relat_1(u3_conlat_1(sK0)),u2_conlat_1(sK0),u1_conlat_1(sK0)),
inference(paramod,[status(thm)],[c_1185,c_1183]) ).
cnf(c_1189,negated_conjecture,
g2_conlat_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k4_relat_1(u3_conlat_1(sK0))) = k7_conlat_2(sK0),
inference(paramod,[status(thm)],[c_1185,c_367]) ).
cnf(c_12316,plain,
( ~ m2_relset_1(u3_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)))
| C = u3_conlat_1(k7_conlat_2(sK0))
| g2_conlat_1(A,B,C) != k7_conlat_2(sK0) ),
inference(paramod,[status(thm)],[c_342,c_227]) ).
cnf(c_12317,plain,
( ~ m2_relset_1(u3_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)))
| u3_conlat_1(k7_conlat_2(sK0)) = C
| g2_conlat_1(A,B,C) != k7_conlat_2(sK0) ),
inference(copy,[status(thm)],[c_12316]) ).
cnf(c_1276,plain,
( u3_conlat_1(k7_conlat_2(sK0)) = C
| g2_conlat_1(A,B,C) != k7_conlat_2(sK0) ),
inference(resolve,[status(thm)],[c_788,c_12317]) ).
cnf(c_12318,plain,
( ~ m2_relset_1(u3_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)))
| B = u2_conlat_1(k7_conlat_2(sK0))
| g2_conlat_1(A,B,C) != k7_conlat_2(sK0) ),
inference(paramod,[status(thm)],[c_342,c_228]) ).
cnf(c_12319,plain,
( ~ m2_relset_1(u3_conlat_1(k7_conlat_2(sK0)),u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)))
| u2_conlat_1(k7_conlat_2(sK0)) = B
| g2_conlat_1(A,B,C) != k7_conlat_2(sK0) ),
inference(copy,[status(thm)],[c_12318]) ).
cnf(c_1278,plain,
( u2_conlat_1(k7_conlat_2(sK0)) = B
| g2_conlat_1(A,B,C) != k7_conlat_2(sK0) ),
inference(resolve,[status(thm)],[c_788,c_12319]) ).
cnf(c_12320,plain,
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u4_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_357,c_313]) ).
cnf(c_12321,plain,
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(paramod,[status(thm)],[c_708,c_12320]) ).
cnf(c_12322,plain,
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_346,c_12321]) ).
cnf(c_12323,plain,
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_340,c_12322]) ).
cnf(c_12324,plain,
( u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u5_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_1132,c_12323]) ).
cnf(c_1512,plain,
u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u5_conlat_1(sK0,sK1),
inference(resolve,[status(thm)],[c_1133,c_12324]) ).
cnf(c_12325,plain,
( u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u5_conlat_1(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_363,c_313]) ).
cnf(c_12326,plain,
( u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0))
| v3_conlat_1(k7_conlat_2(sK0)) ),
inference(paramod,[status(thm)],[c_709,c_12325]) ).
cnf(c_12327,plain,
( u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ l2_conlat_1(k7_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_346,c_12326]) ).
cnf(c_12328,plain,
( u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0)))
| ~ v6_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_340,c_12327]) ).
cnf(c_12329,plain,
( u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u4_conlat_1(sK0,sK1)
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_1132,c_12328]) ).
cnf(c_1617,plain,
u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))) = u4_conlat_1(sK0,sK1),
inference(resolve,[status(thm)],[c_1133,c_12329]) ).
cnf(c_12330,plain,
( A = u2_conlat_1(sK0)
| g2_conlat_1(A,B,C) != g2_conlat_1(u2_conlat_1(sK0),u1_conlat_1(sK0),k4_relat_1(u3_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_1188,c_229]) ).
cnf(c_12331,plain,
( A = u2_conlat_1(sK0)
| g2_conlat_1(A,B,C) != k7_conlat_2(sK0) ),
inference(paramod,[status(thm)],[c_1189,c_12330]) ).
cnf(c_2566,plain,
( u2_conlat_1(sK0) = A
| g2_conlat_1(A,B,C) != k7_conlat_2(sK0) ),
inference(copy,[status(thm)],[c_12331]) ).
cnf(c_12332,plain,
u2_conlat_1(sK0) = u1_conlat_1(k7_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_2566,c_342]) ).
cnf(c_2574,plain,
u1_conlat_1(k7_conlat_2(sK0)) = u2_conlat_1(sK0),
inference(copy,[status(thm)],[c_12332]) ).
cnf(c_2585,plain,
m2_relset_1(u3_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(sK0),u2_conlat_1(k7_conlat_2(sK0))),
inference(paramod,[status(thm)],[c_2574,c_788]) ).
cnf(c_12333,plain,
g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(sK0),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0)))) = k7_conlat_2(k7_conlat_2(sK0)),
inference(paramod,[status(thm)],[c_2574,c_776]) ).
cnf(c_2586,plain,
g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(sK0),k6_relset_1(u2_conlat_1(sK0),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0)))) = k7_conlat_2(k7_conlat_2(sK0)),
inference(paramod,[status(thm)],[c_2574,c_12333]) ).
cnf(c_4181,plain,
k6_relset_1(u2_conlat_1(sK0),u2_conlat_1(k7_conlat_2(sK0)),u3_conlat_1(k7_conlat_2(sK0))) = k4_relat_1(u3_conlat_1(k7_conlat_2(sK0))),
inference(resolve,[status(thm)],[c_2585,c_225]) ).
cnf(c_4185,plain,
g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0)),u2_conlat_1(sK0),k4_relat_1(u3_conlat_1(k7_conlat_2(sK0)))) = k7_conlat_2(k7_conlat_2(sK0)),
inference(paramod,[status(thm)],[c_4181,c_2586]) ).
cnf(c_12334,plain,
( ~ l2_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))),u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)))) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
inference(resolve,[status(thm)],[c_1132,c_221]) ).
cnf(c_12335,plain,
( ~ l2_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(sK0,sK1),u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)))) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
inference(paramod,[status(thm)],[c_1617,c_12334]) ).
cnf(c_12336,plain,
( ~ l2_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1))
| ~ l3_conlat_1(k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),k7_conlat_2(k7_conlat_2(sK0))) ),
inference(paramod,[status(thm)],[c_1512,c_12335]) ).
cnf(c_12337,plain,
( ~ l2_conlat_1(k7_conlat_2(k7_conlat_2(sK0)))
| g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_1133,c_12336]) ).
cnf(c_11459,plain,
g3_conlat_1(k7_conlat_2(k7_conlat_2(sK0)),u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),
inference(resolve,[status(thm)],[c_781,c_12337]) ).
cnf(c_12158,plain,
v1_relat_1(u3_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_1186,c_174]) ).
cnf(c_12162,plain,
u2_conlat_1(k7_conlat_2(sK0)) = u1_conlat_1(sK0),
inference(resolve,[status(thm)],[c_1189,c_1278]) ).
cnf(c_12338,plain,
u3_conlat_1(k7_conlat_2(sK0)) = k4_relat_1(u3_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_1189,c_1276]) ).
cnf(c_12163,plain,
k4_relat_1(u3_conlat_1(sK0)) = u3_conlat_1(k7_conlat_2(sK0)),
inference(copy,[status(thm)],[c_12338]) ).
cnf(c_12200,plain,
g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),k4_relat_1(u3_conlat_1(k7_conlat_2(sK0)))) = k7_conlat_2(k7_conlat_2(sK0)),
inference(paramod,[status(thm)],[c_12162,c_4185]) ).
cnf(c_12339,plain,
k4_relat_1(k4_relat_1(u3_conlat_1(sK0))) = u3_conlat_1(sK0),
inference(resolve,[status(thm)],[c_12158,c_152]) ).
cnf(c_12247,plain,
k4_relat_1(u3_conlat_1(k7_conlat_2(sK0))) = u3_conlat_1(sK0),
inference(paramod,[status(thm)],[c_12163,c_12339]) ).
cnf(c_12340,plain,
g2_conlat_1(u1_conlat_1(sK0),u2_conlat_1(sK0),u3_conlat_1(sK0)) = k7_conlat_2(k7_conlat_2(sK0)),
inference(paramod,[status(thm)],[c_12247,c_12200]) ).
cnf(c_12341,plain,
sK0 = k7_conlat_2(k7_conlat_2(sK0)),
inference(paramod,[status(thm)],[c_246,c_12340]) ).
cnf(c_12250,plain,
k7_conlat_2(k7_conlat_2(sK0)) = sK0,
inference(copy,[status(thm)],[c_12341]) ).
cnf(c_12342,plain,
g3_conlat_1(sK0,u4_conlat_1(sK0,sK1),u5_conlat_1(sK0,sK1)) = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),
inference(paramod,[status(thm)],[c_12250,c_11459]) ).
cnf(c_12343,plain,
sK1 = k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)),
inference(paramod,[status(thm)],[c_587,c_12342]) ).
cnf(c_12344,plain,
k8_conlat_2(k7_conlat_2(sK0),k8_conlat_2(sK0,sK1)) = sK1,
inference(copy,[status(thm)],[c_12343]) ).
cnf(c_12255,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1141,c_12344]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT345+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n017.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 21:02:32 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 3157951 was started by sandbox on n017,
% 0.08/0.35 % Fri Sep 25 21:02:32 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.37
% 0.12/0.37 % From the command line: assign(max_seconds, 300).
% 14.53/2.55
% 14.53/2.55 % given #500 (F,wt=24): 2138 -r2_hidden(A,u4_conlat_1(c1,f1(c1))) | -v1_xboole_0(u1_conlat_1(c1)). [resolve(446,a,130,b)].
% 14.53/2.55
% 14.53/2.55 % given #1000 (T,wt=25): 2359 -r2_hidden(A,u4_conlat_1(c5,f5(c5))) | m1_subset_1(A,u1_conlat_1(c5)). [resolve(964,a,131,b)].
% 14.53/2.55
% 14.53/2.55 % given #1500 (T,wt=20): 9831 g3_conlat_1(c7,k1_xboole_0,k1_xboole_0) != f5(c2) | c7 = c2. [para(948(a,1),8930(a,2))].
% 14.53/2.55
% 14.53/2.55 % SZS status Theorem for theBenchmark
% 14.53/2.55
% 14.53/2.55 % Proof 1 at 1.71 (+ 0.41) seconds.
% 14.53/2.55 % Length of proof is 110.
% 14.53/2.55 % Level of proof is 13.
% 14.53/2.55 % Maximum clause weight is 51.000.
% 14.53/2.55 % Given clauses 1935.
% 14.53/2.55
% 14.53/2.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------