%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT327+4 : 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 : n015.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 114.87s 35.17s
% Output : CNFRefutation 114.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 4
% Syntax : Number of formulae : 56 ( 14 unt; 0 def)
% Number of atoms : 245 ( 6 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 330 ( 141 ~; 141 |; 28 &)
% ( 3 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-3 aty)
% Number of variables : 49 ( 0 sgn 16 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(d3_boolealg,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))
=> ( r1_boolealg(A,B,C)
<=> ( r3_lattices(A,C,B)
& r3_lattices(A,B,C) ) ) ) ) ),
file('theBenchmark.p',d3_boolealg) ).
fof(redefinition_r1_boolealg,axiom,
! [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) )
=> ( r1_boolealg(A,B,C)
<=> B = C ) ),
file('theBenchmark.p',redefinition_r1_boolealg) ).
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_1356,plain,
( r3_lattices(A,C,B)
| ~ r1_boolealg(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(clausify,[status(thm)],[d3_boolealg]) ).
cnf(c_1416,plain,
( C != B
| r1_boolealg(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(clausify,[status(thm)],[redefinition_r1_boolealg]) ).
cnf(c_1674,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_442,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(sK2,k22_filter_2(sK0,sK1,sK2))
| ~ r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2)) )
& r3_lattices(sK0,sK1,sK2)
& m1_subset_1(sK2,u1_struct_0(sK0))
& m1_subset_1(sK1,u1_struct_0(sK0))
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_442]) ).
cnf(c_1675,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1676,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1677,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1678,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1679,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1680,negated_conjecture,
r3_lattices(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_1681,negated_conjecture,
( ~ r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2))
| ~ r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2)) ),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_21067,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_1674]) ).
cnf(c_1792,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_21067]) ).
cnf(c_21068,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_1674]) ).
cnf(c_1793,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_21068]) ).
cnf(c_21069,negated_conjecture,
( B != A
| r1_boolealg(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1676,c_1416]) ).
cnf(c_21070,negated_conjecture,
( B != A
| r1_boolealg(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1675,c_21069]) ).
cnf(c_2719,negated_conjecture,
( B != A
| r1_boolealg(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1677,c_21070]) ).
cnf(c_21071,plain,
( A != A
| r1_boolealg(sK0,A,A)
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(factor,[status(thm)],[c_2719]) ).
cnf(c_2904,plain,
( r1_boolealg(sK0,A,A)
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_21071]) ).
cnf(c_19675,plain,
r1_boolealg(sK0,sK2,sK2),
inference(resolve,[status(thm)],[c_2904,c_1679]) ).
cnf(c_19676,plain,
r1_boolealg(sK0,sK1,sK1),
inference(resolve,[status(thm)],[c_2904,c_1678]) ).
cnf(c_21072,plain,
( r3_lattices(sK0,sK2,sK2)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_19675,c_1356]) ).
cnf(c_21073,plain,
( r3_lattices(sK0,sK2,sK2)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_21072]) ).
cnf(c_21074,negated_conjecture,
( r3_lattices(sK0,sK2,sK2)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1675,c_21073]) ).
cnf(c_21075,negated_conjecture,
( r3_lattices(sK0,sK2,sK2)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1676,c_21074]) ).
cnf(c_21076,negated_conjecture,
( r3_lattices(sK0,sK2,sK2)
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1677,c_21075]) ).
cnf(c_19678,negated_conjecture,
r3_lattices(sK0,sK2,sK2),
inference(resolve,[status(thm)],[c_1679,c_21076]) ).
cnf(c_21077,plain,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_19676,c_1356]) ).
cnf(c_21078,plain,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_21077]) ).
cnf(c_21079,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1675,c_21078]) ).
cnf(c_21080,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1676,c_21079]) ).
cnf(c_21081,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1677,c_21080]) ).
cnf(c_19695,negated_conjecture,
r3_lattices(sK0,sK1,sK1),
inference(resolve,[status(thm)],[c_1678,c_21081]) ).
cnf(c_21082,negated_conjecture,
( ~ r3_lattices(sK0,sK1,sK1)
| r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1792,c_1680]) ).
cnf(c_21083,negated_conjecture,
( ~ r3_lattices(sK0,sK1,sK1)
| r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1675,c_21082]) ).
cnf(c_21084,negated_conjecture,
( ~ r3_lattices(sK0,sK1,sK1)
| r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1676,c_21083]) ).
cnf(c_21085,negated_conjecture,
( ~ r3_lattices(sK0,sK1,sK1)
| r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1677,c_21084]) ).
cnf(c_21086,negated_conjecture,
( ~ r3_lattices(sK0,sK1,sK1)
| r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1678,c_21085]) ).
cnf(c_21087,negated_conjecture,
( ~ r3_lattices(sK0,sK1,sK1)
| r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_1679,c_21086]) ).
cnf(c_21023,negated_conjecture,
r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_19695,c_21087]) ).
cnf(c_21024,negated_conjecture,
~ r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_21023,c_1681]) ).
cnf(c_21088,negated_conjecture,
( ~ r3_lattices(sK0,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1793,c_1680]) ).
cnf(c_21089,negated_conjecture,
( ~ r3_lattices(sK0,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1675,c_21088]) ).
cnf(c_21090,negated_conjecture,
( ~ r3_lattices(sK0,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1676,c_21089]) ).
cnf(c_21091,negated_conjecture,
( ~ r3_lattices(sK0,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1677,c_21090]) ).
cnf(c_21092,negated_conjecture,
( ~ r3_lattices(sK0,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2))
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1678,c_21091]) ).
cnf(c_21093,negated_conjecture,
( ~ r3_lattices(sK0,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_1679,c_21092]) ).
cnf(c_21094,negated_conjecture,
~ r3_lattices(sK0,sK2,sK2),
inference(resolve,[status(thm)],[c_21024,c_21093]) ).
cnf(c_21066,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_19678,c_21094]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT327+4 : 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.36 % Computer : n015.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 20:59:03 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 2191701 was started by sandbox on n015,
% 0.08/0.37 % Fri Sep 25 20:59:03 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 114.87/35.17
% 114.87/35.17 % SInE (scan): 308 to sos (tol 1.5x), 141 to usable (tol 2.0x), 34284 zapped, of 34733 axioms (depth 3).
% 114.87/35.17
% 114.87/35.17 % From the command line: assign(max_seconds, 300).
% 114.87/35.17
% 114.87/35.17 % given #500 (T,wt=14): 14148 m2_lattice4(f29(c10),c10). [resolve(1618,b,931,a),unit_del(a,923),unit_del(b,922)].
% 114.87/35.17
% 114.87/35.17 % given #1000 (F,wt=25): 11159 -r2_hidden(A,k1_tarski(c1)) | -r2_hidden(c1,f2(A,k1_tarski(c1))). [resolve(11119,a,1478,b)].
% 114.87/35.17
% 114.87/35.17 % SZS status Theorem for theBenchmark
% 114.87/35.18
% 114.87/35.18 % Proof 1 at 14.96 (+ 1.12) seconds.
% 114.87/35.18 % Length of proof is 25.
% 114.87/35.18 % Level of proof is 8.
% 114.87/35.18 % Maximum clause weight is 46.000.
% 114.87/35.18 % Given clauses 1192.
% 114.87/35.18
% 114.87/35.18 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------