%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT301+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 : n016.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:06 AM UTC 2026
% Result : Theorem 233.48s 35.12s
% Output : CNFRefutation 233.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 9
% Syntax : Number of formulae : 55 ( 15 unt; 0 def)
% Number of atoms : 184 ( 6 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 205 ( 76 ~; 69 |; 41 &)
% ( 3 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-1 aty)
% Number of variables : 28 ( 0 sgn 15 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t12_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( ( l3_lattices(A)
& v14_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r2_hidden(k6_lattices(A),B) ) ) ),
file('theBenchmark.p',t12_filter_0) ).
fof(fc1_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc1_lattice2) ).
fof(fc6_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc6_lattice2) ).
fof(t63_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',t63_lattice2) ).
fof(dt_k1_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',dt_k1_lattice2) ).
fof(redefinition_m1_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('theBenchmark.p',redefinition_m1_filter_2) ).
fof(t78_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k5_lattices(A) = k6_lattices(k1_lattice2(A)) ),
file('theBenchmark.p',t78_lattice2) ).
fof(t21_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
<=> m1_filter_2(B,k1_lattice2(A)) ) ),
file('theBenchmark.p',t21_filter_2) ).
fof(t25_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
file('theBenchmark.p',t25_filter_2) ).
fof(t25_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
inference(assume_negation,[status(cth)],[t25_filter_2]) ).
cnf(c_2593,plain,
( k6_lattices(k1_lattice2(A)) = k5_lattices(A)
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t78_lattice2]) ).
cnf(c_3135,plain,
( m1_filter_2(B,k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t21_filter_2]) ).
cnf(c_3550,plain,
( r2_hidden(k6_lattices(A),B)
| ~ v14_lattices(A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t12_filter_0]) ).
cnf(c_3570,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_3581,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_3603,plain,
( v14_lattices(k1_lattice2(A))
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t63_lattice2]) ).
cnf(c_3617,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_3656,plain,
( m1_filter_0(B,A)
| ~ m1_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_m1_filter_2]) ).
fof(nnf_1109,plain,
? [A] :
( ? [B] :
( ~ r2_hidden(k5_lattices(A),B)
& v13_lattices(A)
& m2_filter_2(B,A) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t25_filter_2_neg]) ).
fof(sk_t25_filter_2_neg,plain,
( ~ r2_hidden(k5_lattices(sK0),sK1)
& v13_lattices(sK0)
& m2_filter_2(sK1,sK0)
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_1109]) ).
cnf(c_3721,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_3722,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_3723,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_3724,negated_conjecture,
m2_filter_2(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_3725,negated_conjecture,
v13_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_3726,negated_conjecture,
~ r2_hidden(k5_lattices(sK0),sK1),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_29918,negated_conjecture,
( k6_lattices(k1_lattice2(sK0)) = k5_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v13_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3722,c_2593]) ).
cnf(c_29919,negated_conjecture,
( k6_lattices(k1_lattice2(sK0)) = k5_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v13_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3721,c_29918]) ).
cnf(c_29920,negated_conjecture,
( k6_lattices(k1_lattice2(sK0)) = k5_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3725,c_29919]) ).
cnf(c_6619,negated_conjecture,
k6_lattices(k1_lattice2(sK0)) = k5_lattices(sK0),
inference(resolve,[status(thm)],[c_3723,c_29920]) ).
cnf(c_29921,negated_conjecture,
( m1_filter_2(sK1,k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3724,c_3135]) ).
cnf(c_29922,negated_conjecture,
( m1_filter_2(sK1,k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3721,c_29921]) ).
cnf(c_29923,negated_conjecture,
( m1_filter_2(sK1,k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3722,c_29922]) ).
cnf(c_6921,negated_conjecture,
m1_filter_2(sK1,k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_3723,c_29923]) ).
cnf(c_29924,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3570,c_3723]) ).
cnf(c_26464,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_3721,c_29924]) ).
cnf(c_29925,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3581,c_3722]) ).
cnf(c_29926,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3721,c_29925]) ).
cnf(c_26638,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_3723,c_29926]) ).
cnf(c_29927,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ v13_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3603,c_3722]) ).
cnf(c_29928,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ v13_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3721,c_29927]) ).
cnf(c_29929,negated_conjecture,
( v14_lattices(k1_lattice2(sK0))
| ~ v13_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3723,c_29928]) ).
cnf(c_27111,negated_conjecture,
v14_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_3725,c_29929]) ).
cnf(c_27826,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_3617,c_3723]) ).
cnf(c_29930,plain,
( m1_filter_0(sK1,k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_3656,c_6921]) ).
cnf(c_29931,plain,
( m1_filter_0(sK1,k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_26464,c_29930]) ).
cnf(c_29932,plain,
( m1_filter_0(sK1,k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_26638,c_29931]) ).
cnf(c_29518,plain,
m1_filter_0(sK1,k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_27826,c_29932]) ).
cnf(c_29933,plain,
( r2_hidden(k6_lattices(k1_lattice2(sK0)),sK1)
| ~ v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_29518,c_3550]) ).
cnf(c_29934,plain,
( r2_hidden(k5_lattices(sK0),sK1)
| ~ v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_6619,c_29933]) ).
cnf(c_29935,plain,
( r2_hidden(k5_lattices(sK0),sK1)
| ~ v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_26464,c_29934]) ).
cnf(c_29936,plain,
( r2_hidden(k5_lattices(sK0),sK1)
| ~ v14_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_26638,c_29935]) ).
cnf(c_29937,plain,
( r2_hidden(k5_lattices(sK0),sK1)
| ~ v14_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_27826,c_29936]) ).
cnf(c_29938,plain,
r2_hidden(k5_lattices(sK0),sK1),
inference(resolve,[status(thm)],[c_27111,c_29937]) ).
cnf(c_29917,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3726,c_29938]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT301+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.45 % Computer : n016.cluster.edu
% 0.08/0.45 % Model : x86_64 x86_64
% 0.08/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.45 % Memory : 8046.5625MB
% 0.08/0.45 % OS : Linux 6.8.0-71-generic
% 0.08/0.45 % CPULimit : 300
% 0.08/0.45 % WCLimit : 300
% 0.08/0.45 % DateTime : Fri Sep 25 20:42:31 UTC 2026
% 0.08/0.45 % CPUTime :
% 0.08/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.46 % Process 3234338 was started by sandbox on n016,
% 0.08/0.46 % Fri Sep 25 20:42:31 2026
% 0.08/0.46 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 233.48/35.12
% 233.48/35.12 % SInE (scan): 811 to sos (tol 1.5x), 307 to usable (tol 2.0x), 12489 zapped, of 13607 axioms (depth 3).
% 233.48/35.12
% 233.48/35.12 % From the command line: assign(max_seconds, 300).
% 233.48/35.12
% 233.48/35.12 % given #500 (F,wt=16): 19344 -v17_lattices(c6) | -v3_struct_0(k8_filter_1(c6,c6)). [factor(19137,d,e),unit_del(a,3397),unit_del(b,3405),unit_del(c,3396)].
% 233.48/35.12
% 233.48/35.12 % given #1000 (W,wt=13): 25880 l1_rlvect_1(f236(c7)). [resolve(22837,a,22838,a)].
% 233.48/35.12
% 233.48/35.12 % given #1500 (F,wt=20): 29214 -r2_hidden(k2_tarski(A,B),C) | -r2_hidden(k2_tarski(C,D),A). [resolve(22560,b,20336,a)].
% 233.48/35.12
% 233.48/35.12 % SZS status Theorem for theBenchmark
% 233.48/35.12
% 233.48/35.12 % Proof 1 at 31.14 (+ 2.19) seconds.
% 233.48/35.12 % Length of proof is 31.
% 233.48/35.12 % Level of proof is 4.
% 233.48/35.12 % Maximum clause weight is 125.000.
% 233.48/35.12 % Given clauses 1753.
% 233.48/35.12
% 233.48/35.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------