%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT327+3 : 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 : 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 07:50:15 AM UTC 2026
% Result : Theorem 79.02s 12.19s
% Output : CNFRefutation 79.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 5
% Syntax : Number of formulae : 65 ( 19 unt; 0 def)
% Number of atoms : 261 ( 0 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 335 ( 139 ~; 145 |; 34 &)
% ( 1 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 47 ( 1 sgn 17 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(existence_m1_subset_1,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('theBenchmark.p',existence_m1_subset_1) ).
fof(cc1_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc1_lattices) ).
fof(t63_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r2_hidden(D,k22_filter_2(A,B,C))
<=> ( r3_lattices(A,D,C)
& r3_lattices(A,B,D) ) ) ) ) ) ) ),
file('theBenchmark.p',t63_filter_2) ).
fof(reflexivity_r3_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> r3_lattices(A,B,B) ),
file('theBenchmark.p',reflexivity_r3_lattices) ).
fof(t64_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r2_hidden(C,k22_filter_2(A,B,C))
& r2_hidden(B,k22_filter_2(A,B,C)) ) ) ) ) ),
file('theBenchmark.p',t64_filter_2) ).
fof(t64_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r2_hidden(C,k22_filter_2(A,B,C))
& r2_hidden(B,k22_filter_2(A,B,C)) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t64_filter_2]) ).
cnf(c_669,plain,
( r3_lattices(A,B,B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[reflexivity_r3_lattices]) ).
fof(nnf_20,plain,
! [A] :
? [B] : m1_subset_1(B,A),
inference(fof_nnf,[status(thm)],[existence_m1_subset_1]) ).
fof(sk_existence_m1_subset_1,plain,
! [A] : m1_subset_1(sK0(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B,sK0(A))],[nnf_20]) ).
cnf(c_971,plain,
m1_subset_1(sK0(A),A),
inference(split_conjunct,[status(thm)],[sk_existence_m1_subset_1]) ).
cnf(c_1002,plain,
( v6_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_1004,plain,
( v8_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_1005,plain,
( v9_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_1183,plain,
( ~ r3_lattices(A,D,C)
| ~ r3_lattices(A,B,D)
| r2_hidden(D,k22_filter_2(A,B,C))
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(D,u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t63_filter_2]) ).
fof(nnf_347,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ r2_hidden(C,k22_filter_2(A,B,C))
| ~ r2_hidden(B,k22_filter_2(A,B,C)) )
& r3_lattices(A,B,C)
& m1_subset_1(C,u1_struct_0(A)) )
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t64_filter_2_neg]) ).
fof(sk_t64_filter_2_neg,plain,
( ( ~ r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3))
| ~ r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3)) )
& r3_lattices(sK1,sK2,sK3)
& m1_subset_1(sK3,u1_struct_0(sK1))
& m1_subset_1(sK2,u1_struct_0(sK1))
& l3_lattices(sK1)
& v10_lattices(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(A,sK1),skolemize(B,sK2),skolemize(C,sK3)],[nnf_347]) ).
cnf(c_1184,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1185,negated_conjecture,
v10_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1186,negated_conjecture,
l3_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1187,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK1)),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1188,negated_conjecture,
m1_subset_1(sK3,u1_struct_0(sK1)),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1189,negated_conjecture,
r3_lattices(sK1,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1190,negated_conjecture,
( ~ r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3))
| ~ r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3)) ),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_35331,plain,
( ~ r3_lattices(A,B,C)
| ~ r3_lattices(A,B,B)
| r2_hidden(B,k22_filter_2(A,B,C))
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(factor,[status(thm)],[c_1183]) ).
cnf(c_1282,plain,
( ~ r3_lattices(A,B,B)
| r2_hidden(B,k22_filter_2(A,B,C))
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35331]) ).
cnf(c_35332,plain,
( ~ r3_lattices(A,C,C)
| ~ r3_lattices(A,B,C)
| r2_hidden(C,k22_filter_2(A,B,C))
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(factor,[status(thm)],[c_1183]) ).
cnf(c_1283,plain,
( ~ r3_lattices(A,C,C)
| r2_hidden(C,k22_filter_2(A,B,C))
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_35332]) ).
cnf(c_1470,plain,
( r3_lattices(A,B,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_971,c_669]) ).
cnf(c_35333,negated_conjecture,
( v6_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1002,c_1185]) ).
cnf(c_35334,negated_conjecture,
( v6_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1186,c_35333]) ).
cnf(c_8252,negated_conjecture,
v6_lattices(sK1),
inference(resolve,[status(thm)],[c_1184,c_35334]) ).
cnf(c_35335,negated_conjecture,
( v8_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1004,c_1185]) ).
cnf(c_35336,negated_conjecture,
( v8_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1186,c_35335]) ).
cnf(c_8753,negated_conjecture,
v8_lattices(sK1),
inference(resolve,[status(thm)],[c_1184,c_35336]) ).
cnf(c_35337,negated_conjecture,
( v9_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1005,c_1185]) ).
cnf(c_35338,negated_conjecture,
( v9_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1186,c_35337]) ).
cnf(c_9020,negated_conjecture,
v9_lattices(sK1),
inference(resolve,[status(thm)],[c_1184,c_35338]) ).
cnf(c_35339,negated_conjecture,
( ~ r3_lattices(sK1,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1282,c_1189]) ).
cnf(c_35340,negated_conjecture,
( ~ r3_lattices(sK1,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1184,c_35339]) ).
cnf(c_35341,negated_conjecture,
( ~ r3_lattices(sK1,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1185,c_35340]) ).
cnf(c_35342,negated_conjecture,
( ~ r3_lattices(sK1,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_1186,c_35341]) ).
cnf(c_35343,negated_conjecture,
( ~ r3_lattices(sK1,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_1187,c_35342]) ).
cnf(c_28708,negated_conjecture,
( ~ r3_lattices(sK1,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3)) ),
inference(resolve,[status(thm)],[c_1188,c_35343]) ).
cnf(c_35344,negated_conjecture,
( ~ r3_lattices(sK1,sK3,sK3)
| r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1283,c_1189]) ).
cnf(c_35345,negated_conjecture,
( ~ r3_lattices(sK1,sK3,sK3)
| r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1184,c_35344]) ).
cnf(c_35346,negated_conjecture,
( ~ r3_lattices(sK1,sK3,sK3)
| r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1185,c_35345]) ).
cnf(c_35347,negated_conjecture,
( ~ r3_lattices(sK1,sK3,sK3)
| r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1))
| ~ m1_subset_1(sK2,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_1186,c_35346]) ).
cnf(c_35348,negated_conjecture,
( ~ r3_lattices(sK1,sK3,sK3)
| r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3))
| ~ m1_subset_1(sK3,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_1187,c_35347]) ).
cnf(c_28756,negated_conjecture,
( ~ r3_lattices(sK1,sK3,sK3)
| r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3)) ),
inference(resolve,[status(thm)],[c_1188,c_35348]) ).
cnf(c_35349,negated_conjecture,
( r3_lattices(sK1,sK3,sK3)
| ~ l3_lattices(sK1)
| ~ v9_lattices(sK1)
| ~ v8_lattices(sK1)
| ~ v6_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1470,c_1188]) ).
cnf(c_35350,negated_conjecture,
( r3_lattices(sK1,sK3,sK3)
| ~ l3_lattices(sK1)
| ~ v9_lattices(sK1)
| ~ v8_lattices(sK1)
| ~ v6_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1184,c_35349]) ).
cnf(c_35351,negated_conjecture,
( r3_lattices(sK1,sK3,sK3)
| ~ l3_lattices(sK1)
| ~ v9_lattices(sK1)
| ~ v8_lattices(sK1) ),
inference(resolve,[status(thm)],[c_8252,c_35350]) ).
cnf(c_35352,negated_conjecture,
( r3_lattices(sK1,sK3,sK3)
| ~ l3_lattices(sK1)
| ~ v9_lattices(sK1) ),
inference(resolve,[status(thm)],[c_8753,c_35351]) ).
cnf(c_35353,negated_conjecture,
( r3_lattices(sK1,sK3,sK3)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_9020,c_35352]) ).
cnf(c_35315,negated_conjecture,
r3_lattices(sK1,sK3,sK3),
inference(resolve,[status(thm)],[c_1186,c_35353]) ).
cnf(c_35354,negated_conjecture,
( r3_lattices(sK1,sK2,sK2)
| ~ l3_lattices(sK1)
| ~ v9_lattices(sK1)
| ~ v8_lattices(sK1)
| ~ v6_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_1470,c_1187]) ).
cnf(c_35355,negated_conjecture,
( r3_lattices(sK1,sK2,sK2)
| ~ l3_lattices(sK1)
| ~ v9_lattices(sK1)
| ~ v8_lattices(sK1)
| ~ v6_lattices(sK1) ),
inference(resolve,[status(thm)],[c_1184,c_35354]) ).
cnf(c_35356,negated_conjecture,
( r3_lattices(sK1,sK2,sK2)
| ~ l3_lattices(sK1)
| ~ v9_lattices(sK1)
| ~ v8_lattices(sK1) ),
inference(resolve,[status(thm)],[c_8252,c_35355]) ).
cnf(c_35357,negated_conjecture,
( r3_lattices(sK1,sK2,sK2)
| ~ l3_lattices(sK1)
| ~ v9_lattices(sK1) ),
inference(resolve,[status(thm)],[c_8753,c_35356]) ).
cnf(c_35358,negated_conjecture,
( r3_lattices(sK1,sK2,sK2)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_9020,c_35357]) ).
cnf(c_35316,negated_conjecture,
r3_lattices(sK1,sK2,sK2),
inference(resolve,[status(thm)],[c_1186,c_35358]) ).
cnf(c_35324,negated_conjecture,
r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3)),
inference(resolve,[status(thm)],[c_35315,c_28756]) ).
cnf(c_35327,negated_conjecture,
r2_hidden(sK2,k22_filter_2(sK1,sK2,sK3)),
inference(resolve,[status(thm)],[c_35316,c_28708]) ).
cnf(c_35359,negated_conjecture,
~ r2_hidden(sK3,k22_filter_2(sK1,sK2,sK3)),
inference(resolve,[status(thm)],[c_35327,c_1190]) ).
cnf(c_35330,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_35324,c_35359]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT327+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.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 : Fri Sep 25 20:55:05 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 3672612 was started by sandbox on n019,
% 0.09/0.36 % Fri Sep 25 20:55:05 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 79.02/12.19
% 79.02/12.19 % SInE (scan): 201 to sos (tol 1.5x), 147 to usable (tol 2.0x), 13310 zapped, of 13658 axioms (depth 3).
% 79.02/12.19
% 79.02/12.19 % From the command line: assign(max_seconds, 300).
% 79.02/12.19
% 79.02/12.19 % given #500 (F,wt=9): 10176 -r2_hidden(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(c15))),A) | -r2_hidden(A,c17). [resolve(10140,a,6334,a)].
% 79.02/12.19
% 79.02/12.19 % given #1000 (W,wt=4): 17035 -v3_struct_0(k8_filter_1(c15,c8)). [resolve(1369,b,1035,a),unit_del(a,1036)].
% 79.02/12.19
% 79.02/12.19 % given #1500 (F,wt=7): 20306 -v3_struct_0(k1_lattice2(k8_filter_1(c15,k8_filter_1(c15,c13)))). [resolve(1102,b,17259,a),unit_del(a,17232)].
% 79.02/12.19
% 79.02/12.19 % given #2000 (T,wt=6): 21763 r2_hidden(k5_lattices(k1_lattice2(c8)),f22(c8)). [back_rewrite(20285),rewrite([21702(2)])].
% 79.02/12.19
% 79.02/12.19 % given #2500 (F,wt=6): 26085 -r2_hidden(k1_zfmisc_1(u1_struct_0(c15)),f99(c15)). [resolve(25188,a,940,b)].
% 79.02/12.19
% 79.02/12.19 % given #3000 (T,wt=7): 24525 m1_subset_1(f22(k1_lattice2(c14)),k1_zfmisc_1(u1_struct_0(c14))). [resolve(22640,a,1100,d),rewrite([20979(15)]),unit_del(a,20350),unit_del(b,20577),unit_del(c,22459)].
% 79.02/12.19
% 79.02/12.19 % given #3500 (F,wt=7): 30358 -r2_hidden(u1_struct_0(c13),f34(k1_zfmisc_1(f23(c13)))). [resolve(30144,a,429,b)].
% 79.02/12.19
% 79.02/12.19 % given #4000 (T,wt=5): 32530 v7_lattices(k1_lattice2(k8_filter_1(c12,c15))). [resolve(32407,a,1107,b),unit_del(a,16552),unit_del(b,15968)].
% 79.02/12.19
% 79.02/12.19 % given #4500 (A,wt=20): 1437 v3_struct_0(A) | -v10_lattices(A) | -l3_lattices(A) | m1_subset_1(f90(A,f7(u1_struct_0(A))),u1_struct_0(A)) | f7(u1_struct_0(A)) = k5_lattices(A). [resolve(971,a,786,d),flip(e)].
% 79.02/12.19
% 79.02/12.19 % SZS status Theorem for theBenchmark
% 79.02/12.19
% 79.02/12.19 % Proof 1 at 10.49 (+ 0.99) seconds.
% 79.02/12.19 % Length of proof is 31.
% 79.02/12.19 % Level of proof is 5.
% 79.02/12.19 % Maximum clause weight is 108.000.
% 79.02/12.19 % Given clauses 4863.
% 79.02/12.19
% 79.02/12.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------