%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : TOP047+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 : n014.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:53:05 AM UTC 2026
% Result : Theorem 49.68s 6.79s
% Output : CNFRefutation 49.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 12
% Syntax : Number of formulae : 149 ( 47 unt; 0 def)
% Number of atoms : 647 ( 86 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 872 ( 374 ~; 398 |; 75 &)
% ( 3 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-2 aty)
% Number of variables : 88 ( 2 sgn 25 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v1_pre_topc,axiom,
! [A] :
( l1_pre_topc(A)
=> ( v1_pre_topc(A)
=> A = g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) ) ),
file('theBenchmark.p',abstractness_v1_pre_topc) ).
fof(cc2_lattice3,axiom,
! [A] :
( l1_orders_2(A)
=> ( v2_lattice3(A)
=> ~ v3_struct_0(A) ) ),
file('theBenchmark.p',cc2_lattice3) ).
fof(d10_xboole_0,axiom,
! [A,B] :
( A = B
<=> ( r1_tarski(B,A)
& r1_tarski(A,B) ) ),
file('theBenchmark.p',d10_xboole_0) ).
fof(d27_yellow_6,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m4_yellow_6(B,A)
=> ! [C] :
( ( l1_pre_topc(C)
& v1_pre_topc(C) )
=> ( C = k14_yellow_6(A,B)
<=> ( u1_pre_topc(C) = a_2_1_yellow_6(A,B)
& u1_struct_0(C) = u1_struct_0(A) ) ) ) ) ),
file('theBenchmark.p',d27_yellow_6) ).
fof(dt_k14_yellow_6,axiom,
! [A,B] :
( ( m4_yellow_6(B,A)
& l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ( l1_pre_topc(k14_yellow_6(A,B))
& v1_pre_topc(k14_yellow_6(A,B)) ) ),
file('theBenchmark.p',dt_k14_yellow_6) ).
fof(dt_k3_waybel28,axiom,
! [A] :
( ( l1_orders_2(A)
& ~ v3_struct_0(A) )
=> m4_yellow_6(k3_waybel28(A),A) ),
file('theBenchmark.p',dt_k3_waybel28) ).
fof(dt_l1_orders_2,axiom,
! [A] :
( l1_orders_2(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_orders_2) ).
fof(dt_u1_orders_2,axiom,
! [A] :
( l1_orders_2(A)
=> m2_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_u1_orders_2) ).
fof(free_g1_orders_2,axiom,
! [A,B] :
( m1_relset_1(B,A,A)
=> ! [C,D] :
( g1_orders_2(A,B) = g1_orders_2(C,D)
=> ( B = D
& A = C ) ) ),
file('theBenchmark.p',free_g1_orders_2) ).
fof(l12_waybel33,axiom,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v25_waybel_0(A)
& v24_waybel_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v25_waybel_0(B)
& v24_waybel_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ( g1_orders_2(u1_struct_0(A),u1_orders_2(A)) = g1_orders_2(u1_struct_0(B),u1_orders_2(B))
=> r1_tarski(u1_pre_topc(k14_yellow_6(A,k3_waybel28(A))),u1_pre_topc(k14_yellow_6(B,k3_waybel28(B)))) ) ) ),
file('theBenchmark.p',l12_waybel33) ).
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(t8_waybel33,conjecture,
! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v25_waybel_0(A)
& v24_waybel_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v25_waybel_0(B)
& v24_waybel_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ( g1_orders_2(u1_struct_0(A),u1_orders_2(A)) = g1_orders_2(u1_struct_0(B),u1_orders_2(B))
=> k14_yellow_6(A,k3_waybel28(A)) = k14_yellow_6(B,k3_waybel28(B)) ) ) ),
file('theBenchmark.p',t8_waybel33) ).
fof(t8_waybel33_neg,negated_conjecture,
~ ! [A] :
( ( l1_orders_2(A)
& v2_lattice3(A)
& v25_waybel_0(A)
& v24_waybel_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) )
=> ! [B] :
( ( l1_orders_2(B)
& v2_lattice3(B)
& v25_waybel_0(B)
& v24_waybel_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
=> ( g1_orders_2(u1_struct_0(A),u1_orders_2(A)) = g1_orders_2(u1_struct_0(B),u1_orders_2(B))
=> k14_yellow_6(A,k3_waybel28(A)) = k14_yellow_6(B,k3_waybel28(B)) ) ) ),
inference(assume_negation,[status(cth)],[t8_waybel33]) ).
cnf(c_137,plain,
( l1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k14_yellow_6]) ).
cnf(c_140,plain,
( a_2_1_yellow_6(A,B) = u1_pre_topc(C)
| k14_yellow_6(A,B) != C
| ~ l1_pre_topc(C)
| ~ v1_pre_topc(C)
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d27_yellow_6]) ).
cnf(c_141,plain,
( u1_struct_0(C) = u1_struct_0(A)
| k14_yellow_6(A,B) != C
| ~ l1_pre_topc(C)
| ~ v1_pre_topc(C)
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d27_yellow_6]) ).
cnf(c_156,plain,
( g1_pre_topc(u1_struct_0(A),u1_pre_topc(A)) = A
| ~ v1_pre_topc(A)
| ~ l1_pre_topc(A) ),
inference(clausify,[status(thm)],[abstractness_v1_pre_topc]) ).
cnf(c_167,plain,
( m2_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A))
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_u1_orders_2]) ).
cnf(c_170,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_181,plain,
( ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A)
| g1_pre_topc(u1_struct_0(k14_yellow_6(A,B)),u1_pre_topc(k14_yellow_6(A,B))) = k14_yellow_6(A,B)
| ~ v1_pre_topc(k14_yellow_6(A,B)) ),
inference(resolve,[status(thm)],[c_156,c_137]) ).
cnf(c_208,plain,
( ~ m4_yellow_6(D,C)
| ~ l1_struct_0(C)
| v3_struct_0(C)
| u1_struct_0(k14_yellow_6(C,D)) = u1_struct_0(A)
| k14_yellow_6(A,B) != k14_yellow_6(C,D)
| ~ v1_pre_topc(k14_yellow_6(C,D))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_141,c_137]) ).
cnf(c_212,plain,
( ~ m4_yellow_6(D,C)
| ~ l1_struct_0(C)
| v3_struct_0(C)
| a_2_1_yellow_6(A,B) = u1_pre_topc(k14_yellow_6(C,D))
| k14_yellow_6(A,B) != k14_yellow_6(C,D)
| ~ v1_pre_topc(k14_yellow_6(C,D))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_140,c_137]) ).
cnf(c_283,plain,
( ~ v3_struct_0(A)
| ~ v2_lattice3(A)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[cc2_lattice3]) ).
cnf(c_287,plain,
( ~ r1_tarski(A,B)
| ~ r1_tarski(B,A)
| A = B ),
inference(clausify,[status(thm)],[d10_xboole_0]) ).
cnf(c_292,plain,
( v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k14_yellow_6]) ).
cnf(c_293,plain,
( m4_yellow_6(k3_waybel28(A),A)
| ~ l1_orders_2(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k3_waybel28]) ).
cnf(c_294,plain,
( l1_struct_0(A)
| ~ l1_orders_2(A) ),
inference(clausify,[status(thm)],[dt_l1_orders_2]) ).
cnf(c_321,plain,
( C = B
| g1_orders_2(C,D) != g1_orders_2(B,A)
| ~ m1_relset_1(A,B,B) ),
inference(clausify,[status(thm)],[free_g1_orders_2]) ).
cnf(c_325,plain,
( r1_tarski(u1_pre_topc(k14_yellow_6(A,k3_waybel28(A))),u1_pre_topc(k14_yellow_6(B,k3_waybel28(B))))
| g1_orders_2(u1_struct_0(B),u1_orders_2(B)) != g1_orders_2(u1_struct_0(A),u1_orders_2(A))
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v25_waybel_0(B)
| ~ v24_waybel_0(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v25_waybel_0(A)
| ~ v24_waybel_0(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(clausify,[status(thm)],[l12_waybel33]) ).
fof(nnf_102,plain,
? [A] :
( ? [B] :
( k14_yellow_6(B,k3_waybel28(B)) != k14_yellow_6(A,k3_waybel28(A))
& g1_orders_2(u1_struct_0(B),u1_orders_2(B)) = g1_orders_2(u1_struct_0(A),u1_orders_2(A))
& l1_orders_2(B)
& v2_lattice3(B)
& v25_waybel_0(B)
& v24_waybel_0(B)
& v4_orders_2(B)
& v3_orders_2(B)
& v2_orders_2(B) )
& l1_orders_2(A)
& v2_lattice3(A)
& v25_waybel_0(A)
& v24_waybel_0(A)
& v4_orders_2(A)
& v3_orders_2(A)
& v2_orders_2(A) ),
inference(fof_nnf,[status(thm)],[t8_waybel33_neg]) ).
fof(sk_t8_waybel33_neg,plain,
( k14_yellow_6(sK1,k3_waybel28(sK1)) != k14_yellow_6(sK0,k3_waybel28(sK0))
& g1_orders_2(u1_struct_0(sK1),u1_orders_2(sK1)) = g1_orders_2(u1_struct_0(sK0),u1_orders_2(sK0))
& l1_orders_2(sK1)
& v2_lattice3(sK1)
& v25_waybel_0(sK1)
& v24_waybel_0(sK1)
& v4_orders_2(sK1)
& v3_orders_2(sK1)
& v2_orders_2(sK1)
& l1_orders_2(sK0)
& v2_lattice3(sK0)
& v25_waybel_0(sK0)
& v24_waybel_0(sK0)
& v4_orders_2(sK0)
& v3_orders_2(sK0)
& v2_orders_2(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_102]) ).
cnf(c_367,negated_conjecture,
v2_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_368,negated_conjecture,
v3_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_369,negated_conjecture,
v4_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_370,negated_conjecture,
v24_waybel_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_371,negated_conjecture,
v25_waybel_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_372,negated_conjecture,
v2_lattice3(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_373,negated_conjecture,
l1_orders_2(sK0),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_374,negated_conjecture,
v2_orders_2(sK1),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_375,negated_conjecture,
v3_orders_2(sK1),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_376,negated_conjecture,
v4_orders_2(sK1),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_377,negated_conjecture,
v24_waybel_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_378,negated_conjecture,
v25_waybel_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_379,negated_conjecture,
v2_lattice3(sK1),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_380,negated_conjecture,
l1_orders_2(sK1),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_381,negated_conjecture,
g1_orders_2(u1_struct_0(sK1),u1_orders_2(sK1)) = g1_orders_2(u1_struct_0(sK0),u1_orders_2(sK0)),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_382,negated_conjecture,
k14_yellow_6(sK1,k3_waybel28(sK1)) != k14_yellow_6(sK0,k3_waybel28(sK0)),
inference(split_conjunct,[status(thm)],[sk_t8_waybel33_neg]) ).
cnf(c_389,plain,
( ~ l1_orders_2(A)
| m1_relset_1(u1_orders_2(A),u1_struct_0(A),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_170,c_167]) ).
cnf(c_35164,plain,
( ~ l1_struct_0(A)
| v3_struct_0(A)
| u1_struct_0(k14_yellow_6(A,B)) = u1_struct_0(A)
| k14_yellow_6(A,B) != k14_yellow_6(A,B)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(factor,[status(thm)],[c_208]) ).
cnf(c_35165,plain,
( ~ l1_struct_0(A)
| v3_struct_0(A)
| u1_struct_0(k14_yellow_6(A,B)) = u1_struct_0(A)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35164]) ).
cnf(c_35166,plain,
( ~ l1_struct_0(A)
| u1_struct_0(k14_yellow_6(A,B)) = u1_struct_0(A)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35165]) ).
cnf(c_393,plain,
( u1_struct_0(k14_yellow_6(A,B)) = u1_struct_0(A)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35166]) ).
cnf(c_35167,plain,
( ~ l1_struct_0(A)
| v3_struct_0(A)
| a_2_1_yellow_6(A,B) = u1_pre_topc(k14_yellow_6(A,B))
| k14_yellow_6(A,B) != k14_yellow_6(A,B)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(factor,[status(thm)],[c_212]) ).
cnf(c_35168,plain,
( ~ l1_struct_0(A)
| v3_struct_0(A)
| u1_pre_topc(k14_yellow_6(A,B)) = a_2_1_yellow_6(A,B)
| k14_yellow_6(A,B) != k14_yellow_6(A,B)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35167]) ).
cnf(c_35169,plain,
( ~ l1_struct_0(A)
| v3_struct_0(A)
| u1_pre_topc(k14_yellow_6(A,B)) = a_2_1_yellow_6(A,B)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35168]) ).
cnf(c_35170,plain,
( ~ l1_struct_0(A)
| u1_pre_topc(k14_yellow_6(A,B)) = a_2_1_yellow_6(A,B)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35169]) ).
cnf(c_395,plain,
( u1_pre_topc(k14_yellow_6(A,B)) = a_2_1_yellow_6(A,B)
| ~ v1_pre_topc(k14_yellow_6(A,B))
| ~ m4_yellow_6(B,A)
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35170]) ).
cnf(c_35171,negated_conjecture,
( ~ v3_struct_0(sK0)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_372,c_283]) ).
cnf(c_1231,negated_conjecture,
~ v3_struct_0(sK0),
inference(resolve,[status(thm)],[c_373,c_35171]) ).
cnf(c_1232,plain,
l1_struct_0(sK0),
inference(resolve,[status(thm)],[c_373,c_294]) ).
cnf(c_35172,negated_conjecture,
( m4_yellow_6(k3_waybel28(sK0),sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_373,c_293]) ).
cnf(c_1233,negated_conjecture,
m4_yellow_6(k3_waybel28(sK0),sK0),
inference(resolve,[status(thm)],[c_1231,c_35172]) ).
cnf(c_35173,negated_conjecture,
( ~ v3_struct_0(sK1)
| ~ l1_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_379,c_283]) ).
cnf(c_1236,negated_conjecture,
~ v3_struct_0(sK1),
inference(resolve,[status(thm)],[c_380,c_35173]) ).
cnf(c_1237,plain,
l1_struct_0(sK1),
inference(resolve,[status(thm)],[c_380,c_294]) ).
cnf(c_35174,negated_conjecture,
( m4_yellow_6(k3_waybel28(sK1),sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_380,c_293]) ).
cnf(c_1238,negated_conjecture,
m4_yellow_6(k3_waybel28(sK1),sK1),
inference(resolve,[status(thm)],[c_1236,c_35174]) ).
cnf(c_35175,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_381,c_325]) ).
cnf(c_35176,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_367,c_35175]) ).
cnf(c_35177,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_368,c_35176]) ).
cnf(c_35178,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0) ),
inference(resolve,[status(thm)],[c_369,c_35177]) ).
cnf(c_35179,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0) ),
inference(resolve,[status(thm)],[c_370,c_35178]) ).
cnf(c_35180,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_371,c_35179]) ).
cnf(c_35181,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1)
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_372,c_35180]) ).
cnf(c_35182,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_373,c_35181]) ).
cnf(c_35183,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_374,c_35182]) ).
cnf(c_35184,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_375,c_35183]) ).
cnf(c_35185,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1) ),
inference(resolve,[status(thm)],[c_376,c_35184]) ).
cnf(c_35186,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1) ),
inference(resolve,[status(thm)],[c_377,c_35185]) ).
cnf(c_35187,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1) ),
inference(resolve,[status(thm)],[c_378,c_35186]) ).
cnf(c_35188,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))))
| ~ l1_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_379,c_35187]) ).
cnf(c_1239,negated_conjecture,
r1_tarski(u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))),
inference(resolve,[status(thm)],[c_380,c_35188]) ).
cnf(c_35189,plain,
( r1_tarski(u1_pre_topc(k14_yellow_6(A,k3_waybel28(A))),u1_pre_topc(k14_yellow_6(B,k3_waybel28(B))))
| g1_orders_2(u1_struct_0(A),u1_orders_2(A)) != g1_orders_2(u1_struct_0(B),u1_orders_2(B))
| ~ l1_orders_2(B)
| ~ v2_lattice3(B)
| ~ v25_waybel_0(B)
| ~ v24_waybel_0(B)
| ~ v4_orders_2(B)
| ~ v3_orders_2(B)
| ~ v2_orders_2(B)
| ~ l1_orders_2(A)
| ~ v2_lattice3(A)
| ~ v25_waybel_0(A)
| ~ v24_waybel_0(A)
| ~ v4_orders_2(A)
| ~ v3_orders_2(A)
| ~ v2_orders_2(A) ),
inference(copy,[status(thm)],[c_325]) ).
cnf(c_35190,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1)
| ~ v2_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_381,c_35189]) ).
cnf(c_35191,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1)
| ~ v3_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_374,c_35190]) ).
cnf(c_35192,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1)
| ~ v4_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_375,c_35191]) ).
cnf(c_35193,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1)
| ~ v24_waybel_0(sK1) ),
inference(resolve,[status(thm)],[c_376,c_35192]) ).
cnf(c_35194,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1)
| ~ v25_waybel_0(sK1) ),
inference(resolve,[status(thm)],[c_377,c_35193]) ).
cnf(c_35195,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK1)
| ~ v2_lattice3(sK1) ),
inference(resolve,[status(thm)],[c_378,c_35194]) ).
cnf(c_35196,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0)
| ~ l1_orders_2(sK1) ),
inference(resolve,[status(thm)],[c_379,c_35195]) ).
cnf(c_35197,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0)
| ~ v2_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_380,c_35196]) ).
cnf(c_35198,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0)
| ~ v3_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_367,c_35197]) ).
cnf(c_35199,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0)
| ~ v4_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_368,c_35198]) ).
cnf(c_35200,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0)
| ~ v24_waybel_0(sK0) ),
inference(resolve,[status(thm)],[c_369,c_35199]) ).
cnf(c_35201,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0)
| ~ v25_waybel_0(sK0) ),
inference(resolve,[status(thm)],[c_370,c_35200]) ).
cnf(c_35202,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0)
| ~ v2_lattice3(sK0) ),
inference(resolve,[status(thm)],[c_371,c_35201]) ).
cnf(c_35203,negated_conjecture,
( r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))))
| ~ l1_orders_2(sK0) ),
inference(resolve,[status(thm)],[c_372,c_35202]) ).
cnf(c_1242,negated_conjecture,
r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))),
inference(resolve,[status(thm)],[c_373,c_35203]) ).
cnf(c_35204,plain,
( C = B
| g1_orders_2(B,A) != g1_orders_2(C,D)
| ~ m1_relset_1(A,B,B) ),
inference(copy,[status(thm)],[c_321]) ).
cnf(c_35205,negated_conjecture,
( u1_struct_0(sK0) = u1_struct_0(sK1)
| ~ m1_relset_1(u1_orders_2(sK1),u1_struct_0(sK1),u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_381,c_35204]) ).
cnf(c_1244,negated_conjecture,
( u1_struct_0(sK1) = u1_struct_0(sK0)
| ~ m1_relset_1(u1_orders_2(sK1),u1_struct_0(sK1),u1_struct_0(sK1)) ),
inference(copy,[status(thm)],[c_35205]) ).
cnf(c_1260,plain,
m1_relset_1(u1_orders_2(sK1),u1_struct_0(sK1),u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_389,c_380]) ).
cnf(c_1264,negated_conjecture,
u1_struct_0(sK1) = u1_struct_0(sK0),
inference(resolve,[status(thm)],[c_1260,c_1244]) ).
cnf(c_35206,plain,
( u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))) = a_2_1_yellow_6(sK0,k3_waybel28(sK0))
| ~ v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))
| ~ l1_struct_0(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1233,c_395]) ).
cnf(c_35207,plain,
( u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))) = a_2_1_yellow_6(sK0,k3_waybel28(sK0))
| ~ v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))
| ~ l1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1231,c_35206]) ).
cnf(c_2514,plain,
( u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))) = a_2_1_yellow_6(sK0,k3_waybel28(sK0))
| ~ v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))) ),
inference(resolve,[status(thm)],[c_1232,c_35207]) ).
cnf(c_35208,plain,
( u1_struct_0(k14_yellow_6(sK0,k3_waybel28(sK0))) = u1_struct_0(sK0)
| ~ v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))
| ~ l1_struct_0(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1233,c_393]) ).
cnf(c_35209,plain,
( u1_struct_0(k14_yellow_6(sK0,k3_waybel28(sK0))) = u1_struct_0(sK0)
| ~ v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))
| ~ l1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1231,c_35208]) ).
cnf(c_2517,plain,
( u1_struct_0(k14_yellow_6(sK0,k3_waybel28(sK0))) = u1_struct_0(sK0)
| ~ v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))) ),
inference(resolve,[status(thm)],[c_1232,c_35209]) ).
cnf(c_35210,plain,
( v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))
| ~ l1_struct_0(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1233,c_292]) ).
cnf(c_35211,plain,
( v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))
| ~ l1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1231,c_35210]) ).
cnf(c_2528,plain,
v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))),
inference(resolve,[status(thm)],[c_1232,c_35211]) ).
cnf(c_35212,plain,
( ~ l1_struct_0(sK0)
| v3_struct_0(sK0)
| g1_pre_topc(u1_struct_0(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))) = k14_yellow_6(sK0,k3_waybel28(sK0))
| ~ v1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))) ),
inference(resolve,[status(thm)],[c_1233,c_181]) ).
cnf(c_35213,plain,
( ~ l1_struct_0(sK0)
| v3_struct_0(sK0)
| g1_pre_topc(u1_struct_0(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))) = k14_yellow_6(sK0,k3_waybel28(sK0)) ),
inference(resolve,[status(thm)],[c_2528,c_35212]) ).
cnf(c_35214,plain,
( ~ l1_struct_0(sK0)
| g1_pre_topc(u1_struct_0(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))) = k14_yellow_6(sK0,k3_waybel28(sK0)) ),
inference(resolve,[status(thm)],[c_1231,c_35213]) ).
cnf(c_2569,plain,
g1_pre_topc(u1_struct_0(k14_yellow_6(sK0,k3_waybel28(sK0))),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))) = k14_yellow_6(sK0,k3_waybel28(sK0)),
inference(resolve,[status(thm)],[c_1232,c_35214]) ).
cnf(c_2571,plain,
u1_struct_0(k14_yellow_6(sK0,k3_waybel28(sK0))) = u1_struct_0(sK0),
inference(resolve,[status(thm)],[c_2528,c_2517]) ).
cnf(c_2573,plain,
u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0))) = a_2_1_yellow_6(sK0,k3_waybel28(sK0)),
inference(resolve,[status(thm)],[c_2528,c_2514]) ).
cnf(c_35215,plain,
g1_pre_topc(u1_struct_0(sK0),u1_pre_topc(k14_yellow_6(sK0,k3_waybel28(sK0)))) = k14_yellow_6(sK0,k3_waybel28(sK0)),
inference(paramod,[status(thm)],[c_2571,c_2569]) ).
cnf(c_2576,plain,
g1_pre_topc(u1_struct_0(sK0),a_2_1_yellow_6(sK0,k3_waybel28(sK0))) = k14_yellow_6(sK0,k3_waybel28(sK0)),
inference(paramod,[status(thm)],[c_2573,c_35215]) ).
cnf(c_2595,negated_conjecture,
r1_tarski(u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),a_2_1_yellow_6(sK0,k3_waybel28(sK0))),
inference(paramod,[status(thm)],[c_2573,c_1242]) ).
cnf(c_2596,negated_conjecture,
r1_tarski(a_2_1_yellow_6(sK0,k3_waybel28(sK0)),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))),
inference(paramod,[status(thm)],[c_2573,c_1239]) ).
cnf(c_35216,plain,
( u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))) = a_2_1_yellow_6(sK1,k3_waybel28(sK1))
| ~ v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))
| ~ l1_struct_0(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1238,c_395]) ).
cnf(c_35217,plain,
( u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))) = a_2_1_yellow_6(sK1,k3_waybel28(sK1))
| ~ v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))
| ~ l1_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1236,c_35216]) ).
cnf(c_2605,plain,
( u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))) = a_2_1_yellow_6(sK1,k3_waybel28(sK1))
| ~ v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))) ),
inference(resolve,[status(thm)],[c_1237,c_35217]) ).
cnf(c_35218,plain,
( u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))) = u1_struct_0(sK1)
| ~ v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))
| ~ l1_struct_0(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1238,c_393]) ).
cnf(c_35219,plain,
( u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))) = u1_struct_0(sK0)
| ~ v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))
| ~ l1_struct_0(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_1264,c_35218]) ).
cnf(c_35220,plain,
( u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))) = u1_struct_0(sK0)
| ~ v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))
| ~ l1_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1236,c_35219]) ).
cnf(c_2608,plain,
( u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))) = u1_struct_0(sK0)
| ~ v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))) ),
inference(resolve,[status(thm)],[c_1237,c_35220]) ).
cnf(c_35221,plain,
( v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))
| ~ l1_struct_0(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1238,c_292]) ).
cnf(c_35222,plain,
( v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))
| ~ l1_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1236,c_35221]) ).
cnf(c_2619,plain,
v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))),
inference(resolve,[status(thm)],[c_1237,c_35222]) ).
cnf(c_35223,plain,
( ~ l1_struct_0(sK1)
| v3_struct_0(sK1)
| g1_pre_topc(u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))) = k14_yellow_6(sK1,k3_waybel28(sK1))
| ~ v1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))) ),
inference(resolve,[status(thm)],[c_1238,c_181]) ).
cnf(c_35224,plain,
( ~ l1_struct_0(sK1)
| v3_struct_0(sK1)
| g1_pre_topc(u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))) = k14_yellow_6(sK1,k3_waybel28(sK1)) ),
inference(resolve,[status(thm)],[c_2619,c_35223]) ).
cnf(c_35225,plain,
( ~ l1_struct_0(sK1)
| g1_pre_topc(u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))) = k14_yellow_6(sK1,k3_waybel28(sK1)) ),
inference(resolve,[status(thm)],[c_1236,c_35224]) ).
cnf(c_2660,plain,
g1_pre_topc(u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))) = k14_yellow_6(sK1,k3_waybel28(sK1)),
inference(resolve,[status(thm)],[c_1237,c_35225]) ).
cnf(c_2662,plain,
u1_struct_0(k14_yellow_6(sK1,k3_waybel28(sK1))) = u1_struct_0(sK0),
inference(resolve,[status(thm)],[c_2619,c_2608]) ).
cnf(c_2664,plain,
u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1))) = a_2_1_yellow_6(sK1,k3_waybel28(sK1)),
inference(resolve,[status(thm)],[c_2619,c_2605]) ).
cnf(c_35226,plain,
g1_pre_topc(u1_struct_0(sK0),u1_pre_topc(k14_yellow_6(sK1,k3_waybel28(sK1)))) = k14_yellow_6(sK1,k3_waybel28(sK1)),
inference(paramod,[status(thm)],[c_2662,c_2660]) ).
cnf(c_2667,plain,
g1_pre_topc(u1_struct_0(sK0),a_2_1_yellow_6(sK1,k3_waybel28(sK1))) = k14_yellow_6(sK1,k3_waybel28(sK1)),
inference(paramod,[status(thm)],[c_2664,c_35226]) ).
cnf(c_2686,negated_conjecture,
r1_tarski(a_2_1_yellow_6(sK0,k3_waybel28(sK0)),a_2_1_yellow_6(sK1,k3_waybel28(sK1))),
inference(paramod,[status(thm)],[c_2664,c_2596]) ).
cnf(c_2687,negated_conjecture,
r1_tarski(a_2_1_yellow_6(sK1,k3_waybel28(sK1)),a_2_1_yellow_6(sK0,k3_waybel28(sK0))),
inference(paramod,[status(thm)],[c_2664,c_2595]) ).
cnf(c_35227,plain,
( ~ r1_tarski(a_2_1_yellow_6(sK1,k3_waybel28(sK1)),a_2_1_yellow_6(sK0,k3_waybel28(sK0)))
| a_2_1_yellow_6(sK0,k3_waybel28(sK0)) = a_2_1_yellow_6(sK1,k3_waybel28(sK1)) ),
inference(resolve,[status(thm)],[c_2686,c_287]) ).
cnf(c_35228,plain,
( ~ r1_tarski(a_2_1_yellow_6(sK1,k3_waybel28(sK1)),a_2_1_yellow_6(sK0,k3_waybel28(sK0)))
| a_2_1_yellow_6(sK1,k3_waybel28(sK1)) = a_2_1_yellow_6(sK0,k3_waybel28(sK0)) ),
inference(copy,[status(thm)],[c_35227]) ).
cnf(c_35162,plain,
a_2_1_yellow_6(sK1,k3_waybel28(sK1)) = a_2_1_yellow_6(sK0,k3_waybel28(sK0)),
inference(resolve,[status(thm)],[c_2687,c_35228]) ).
cnf(c_35229,plain,
g1_pre_topc(u1_struct_0(sK0),a_2_1_yellow_6(sK0,k3_waybel28(sK0))) = k14_yellow_6(sK1,k3_waybel28(sK1)),
inference(paramod,[status(thm)],[c_35162,c_2667]) ).
cnf(c_35230,plain,
k14_yellow_6(sK0,k3_waybel28(sK0)) = k14_yellow_6(sK1,k3_waybel28(sK1)),
inference(paramod,[status(thm)],[c_2576,c_35229]) ).
cnf(c_35231,plain,
k14_yellow_6(sK1,k3_waybel28(sK1)) = k14_yellow_6(sK0,k3_waybel28(sK0)),
inference(copy,[status(thm)],[c_35230]) ).
cnf(c_35163,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_382,c_35231]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : TOP047+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 20:47:46 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 4070457 was started by sandbox on n014,
% 0.09/0.36 % Sat Sep 26 20:47:46 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.39
% 0.14/0.39 % From the command line: assign(max_seconds, 300).
% 49.68/6.79
% 49.68/6.79 % given #500 (F,wt=35): 3998 -m4_yellow_6(A,k14_yellow_6(c11,f5(c11))) | -v3_struct_0(k14_yellow_6(k14_yellow_6(c11,f5(c11)),A)). [resolve(2203,a,306,b),unit_del(a,2201)].
% 49.68/6.79
% 49.68/6.79 % given #1000 (F,wt=22): 10249 -m1_subset_1(a_2_1_yellow_6(c15,k3_waybel28(c15)),k1_zfmisc_1(k1_xboole_0)). [resolve(10222,a,1150,a)].
% 49.68/6.79
% 49.68/6.79 % given #1500 (T,wt=22): 21489 v1_finset_1(k2_zfmisc_1(f9(c4),f4(c4,c4))). [resolve(3218,a,3381,a)].
% 49.68/6.79
% 49.68/6.79 % given #2000 (T,wt=22): 23471 v1_finset_1(f2(k1_tarski(A),f4(c4,k1_xboole_0))). [resolve(23236,a,8412,a)].
% 49.68/6.79
% 49.68/6.79 % given #2500 (A,wt=35): 895 -v2_pre_topc(g1_pre_topc(A,f13(A))) | v2_tops_1(f20(g1_pre_topc(A,f13(A))),g1_pre_topc(A,f13(A))). [resolve(335,a,220,a)].
% 49.68/6.79
% 49.68/6.79 % SZS status Theorem for theBenchmark
% 49.68/6.79
% 49.68/6.79 % Proof 1 at 4.23 (+ 1.95) seconds.
% 49.68/6.79 % Length of proof is 78.
% 49.68/6.79 % Level of proof is 9.
% 49.68/6.79 % Maximum clause weight is 70.000.
% 49.68/6.79 % Given clauses 2845.
% 49.68/6.79
% 49.68/6.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------