%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT327+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:14 AM UTC 2026
% Result : Theorem 0.02s 0.34s
% Output : CNFRefutation 0.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 4
% Syntax : Number of formulae : 58 ( 15 unt; 0 def)
% Number of atoms : 233 ( 0 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 299 ( 124 ~; 124 |; 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 : 5 ( 5 usr; 3 con; 0-3 aty)
% Number of variables : 46 ( 1 sgn 14 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(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_52,plain,
( v6_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_54,plain,
( v8_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_55,plain,
( v9_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_58,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_42,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_42]) ).
cnf(c_59,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_114,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]) ).
cnf(c_119,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_120,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_121,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_122,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_123,negated_conjecture,
r3_lattices(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t64_filter_2_neg]) ).
cnf(c_124,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_125,negated_conjecture,
( ~ r3_lattices(sK0,C,B)
| ~ r3_lattices(sK0,A,C)
| r2_hidden(C,k22_filter_2(sK0,A,B))
| ~ r3_lattices(sK0,A,B)
| ~ m1_subset_1(C,u1_struct_0(sK0))
| ~ 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_59,c_58]) ).
cnf(c_252,negated_conjecture,
( ~ r3_lattices(sK0,C,B)
| ~ r3_lattices(sK0,A,C)
| r2_hidden(C,k22_filter_2(sK0,A,B))
| ~ r3_lattices(sK0,A,B)
| ~ m1_subset_1(C,u1_struct_0(sK0))
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_119,c_125]) ).
cnf(c_126,negated_conjecture,
( ~ r3_lattices(sK0,C,B)
| ~ r3_lattices(sK0,A,C)
| r2_hidden(C,k22_filter_2(sK0,A,B))
| ~ r3_lattices(sK0,A,B)
| ~ m1_subset_1(C,u1_struct_0(sK0))
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_120,c_252]) ).
cnf(c_131,negated_conjecture,
( v9_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_59,c_55]) ).
cnf(c_253,negated_conjecture,
( v9_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_120,c_131]) ).
cnf(c_132,negated_conjecture,
v9_lattices(sK0),
inference(resolve,[status(thm)],[c_119,c_253]) ).
cnf(c_133,negated_conjecture,
( v8_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_59,c_54]) ).
cnf(c_254,negated_conjecture,
( v8_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_120,c_133]) ).
cnf(c_134,negated_conjecture,
v8_lattices(sK0),
inference(resolve,[status(thm)],[c_119,c_254]) ).
cnf(c_137,negated_conjecture,
( v6_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_59,c_52]) ).
cnf(c_255,negated_conjecture,
( v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_120,c_137]) ).
cnf(c_138,negated_conjecture,
v6_lattices(sK0),
inference(resolve,[status(thm)],[c_119,c_255]) ).
cnf(c_169,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(factor,[status(thm)],[c_114]) ).
cnf(c_256,plain,
( ~ r3_lattices(sK0,A,B)
| ~ r3_lattices(sK0,A,A)
| r2_hidden(A,k22_filter_2(sK0,A,B))
| ~ r3_lattices(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(factor,[status(thm)],[c_126]) ).
cnf(c_171,plain,
( ~ r3_lattices(sK0,A,A)
| r2_hidden(A,k22_filter_2(sK0,A,B))
| ~ r3_lattices(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_256]) ).
cnf(c_257,plain,
( ~ r3_lattices(sK0,B,B)
| ~ r3_lattices(sK0,A,B)
| r2_hidden(B,k22_filter_2(sK0,A,B))
| ~ r3_lattices(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(factor,[status(thm)],[c_126]) ).
cnf(c_172,plain,
( ~ r3_lattices(sK0,B,B)
| r2_hidden(B,k22_filter_2(sK0,A,B))
| ~ r3_lattices(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_257]) ).
cnf(c_258,negated_conjecture,
( r3_lattices(sK0,sK2,sK2)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_169,c_122]) ).
cnf(c_259,negated_conjecture,
( r3_lattices(sK0,sK2,sK2)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0) ),
inference(resolve,[status(thm)],[c_119,c_258]) ).
cnf(c_260,negated_conjecture,
( r3_lattices(sK0,sK2,sK2)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0) ),
inference(resolve,[status(thm)],[c_138,c_259]) ).
cnf(c_261,negated_conjecture,
( r3_lattices(sK0,sK2,sK2)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0) ),
inference(resolve,[status(thm)],[c_134,c_260]) ).
cnf(c_262,negated_conjecture,
( r3_lattices(sK0,sK2,sK2)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_132,c_261]) ).
cnf(c_244,negated_conjecture,
r3_lattices(sK0,sK2,sK2),
inference(resolve,[status(thm)],[c_120,c_262]) ).
cnf(c_263,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_169,c_121]) ).
cnf(c_264,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0) ),
inference(resolve,[status(thm)],[c_119,c_263]) ).
cnf(c_265,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0) ),
inference(resolve,[status(thm)],[c_138,c_264]) ).
cnf(c_266,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0) ),
inference(resolve,[status(thm)],[c_134,c_265]) ).
cnf(c_267,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_132,c_266]) ).
cnf(c_245,negated_conjecture,
r3_lattices(sK0,sK1,sK1),
inference(resolve,[status(thm)],[c_120,c_267]) ).
cnf(c_268,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_171,c_123]) ).
cnf(c_269,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_121,c_268]) ).
cnf(c_270,negated_conjecture,
( ~ r3_lattices(sK0,sK1,sK1)
| r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_122,c_269]) ).
cnf(c_249,negated_conjecture,
r2_hidden(sK1,k22_filter_2(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_245,c_270]) ).
cnf(c_250,negated_conjecture,
~ r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_249,c_124]) ).
cnf(c_271,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_172,c_123]) ).
cnf(c_272,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_121,c_271]) ).
cnf(c_273,negated_conjecture,
( ~ r3_lattices(sK0,sK2,sK2)
| r2_hidden(sK2,k22_filter_2(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_122,c_272]) ).
cnf(c_274,negated_conjecture,
~ r3_lattices(sK0,sK2,sK2),
inference(resolve,[status(thm)],[c_250,c_273]) ).
cnf(c_251,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_244,c_274]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT327+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Fri Sep 25 20:54:20 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.02/0.30 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.30 % Process 2998634 was started by sandbox2 on n012,
% 0.02/0.30 % Fri Sep 25 20:54:20 2026
% 0.02/0.30 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.02/0.31
% 0.02/0.31 % From the command line: assign(max_seconds, 300).
% 0.02/0.34
% 0.02/0.34 % SZS status Theorem for theBenchmark
% 0.02/0.34
% 0.02/0.34 % Proof 1 at 0.02 (+ 0.00) seconds.
% 0.02/0.34 % Length of proof is 32.
% 0.02/0.34 % Level of proof is 7.
% 0.02/0.34 % Maximum clause weight is 30.000.
% 0.02/0.34 % Given clauses 60.
% 0.02/0.34
% 0.02/0.34 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------