%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT291+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 : n009.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:03 AM UTC 2026
% Result : Theorem 3.24s 0.82s
% Output : CNFRefutation 3.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 7
% Syntax : Number of formulae : 46 ( 16 unt; 0 def)
% Number of atoms : 145 ( 33 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 160 ( 61 ~; 60 |; 31 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-4 aty)
% Number of variables : 24 ( 0 sgn 9 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k5_lattices,axiom,
! [A] :
( ( l1_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k5_lattices(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k5_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(t28_lopclset,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k4_xboole_0(k7_lopclset(A),k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B)) = k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k7_lattices(A,B)) ) ),
file('theBenchmark.p',t28_lopclset) ).
fof(t36_lopclset,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k5_lattices(A)) = k1_xboole_0 ),
file('theBenchmark.p',t36_lopclset) ).
fof(t37_lattice4,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k7_lattices(A,k5_lattices(A)) = k6_lattices(A) ),
file('theBenchmark.p',t37_lattice4) ).
fof(t3_boole,axiom,
! [A] : k4_xboole_0(A,k1_xboole_0) = A,
file('theBenchmark.p',t3_boole) ).
fof(t37_lopclset,conjecture,
! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A)) = k7_lopclset(A) ),
file('theBenchmark.p',t37_lopclset) ).
fof(t37_lopclset_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A)) = k7_lopclset(A) ),
inference(assume_negation,[status(cth)],[t37_lopclset]) ).
cnf(c_133,plain,
( k4_xboole_0(k7_lopclset(A),k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),B)) = k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k7_lattices(A,B))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t28_lopclset]) ).
cnf(c_134,plain,
( k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k5_lattices(A)) = k1_xboole_0
| ~ l3_lattices(A)
| v3_realset2(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t36_lopclset]) ).
cnf(c_135,plain,
( k7_lattices(A,k5_lattices(A)) = k6_lattices(A)
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t37_lattice4]) ).
fof(nnf_101,plain,
? [A] :
( k8_funct_2(u1_struct_0(A),k1_zfmisc_1(k7_lopclset(A)),k9_lopclset(A),k6_lattices(A)) != k7_lopclset(A)
& l3_lattices(A)
& ~ v3_realset2(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t37_lopclset_neg]) ).
fof(sk_t37_lopclset_neg,plain,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k6_lattices(sK0)) != k7_lopclset(sK0)
& l3_lattices(sK0)
& ~ v3_realset2(sK0)
& v17_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_101]) ).
cnf(c_136,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t37_lopclset_neg]) ).
cnf(c_185,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_187,plain,
( m1_subset_1(k5_lattices(A),u1_struct_0(A))
| ~ l1_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k5_lattices]) ).
cnf(c_265,plain,
( ~ l3_lattices(A)
| m1_subset_1(k5_lattices(A),u1_struct_0(A))
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_187,c_185]) ).
cnf(c_356,plain,
k4_xboole_0(A,k1_xboole_0) = A,
inference(clausify,[status(thm)],[t3_boole]) ).
cnf(c_363,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t37_lopclset_neg]) ).
cnf(c_364,negated_conjecture,
v17_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t37_lopclset_neg]) ).
cnf(c_365,negated_conjecture,
~ v3_realset2(sK0),
inference(split_conjunct,[status(thm)],[sk_t37_lopclset_neg]) ).
cnf(c_366,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t37_lopclset_neg]) ).
cnf(c_367,negated_conjecture,
k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k6_lattices(sK0)) != k7_lopclset(sK0),
inference(split_conjunct,[status(thm)],[sk_t37_lopclset_neg]) ).
cnf(c_412,negated_conjecture,
( k7_lattices(sK0,k5_lattices(sK0)) = k6_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_136,c_135]) ).
cnf(c_984,negated_conjecture,
( k6_lattices(sK0) = k7_lattices(sK0,k5_lattices(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_412]) ).
cnf(c_985,negated_conjecture,
( k6_lattices(sK0) = k7_lattices(sK0,k5_lattices(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_363,c_984]) ).
cnf(c_986,negated_conjecture,
( k6_lattices(sK0) = k7_lattices(sK0,k5_lattices(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_364,c_985]) ).
cnf(c_413,negated_conjecture,
k6_lattices(sK0) = k7_lattices(sK0,k5_lattices(sK0)),
inference(resolve,[status(thm)],[c_366,c_986]) ).
cnf(c_414,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k5_lattices(sK0)) = k1_xboole_0
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v17_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_136,c_134]) ).
cnf(c_987,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k5_lattices(sK0)) = k1_xboole_0
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_363,c_414]) ).
cnf(c_988,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k5_lattices(sK0)) = k1_xboole_0
| ~ l3_lattices(sK0)
| v3_realset2(sK0) ),
inference(resolve,[status(thm)],[c_364,c_987]) ).
cnf(c_989,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k5_lattices(sK0)) = k1_xboole_0
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_365,c_988]) ).
cnf(c_415,negated_conjecture,
k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k5_lattices(sK0)) = k1_xboole_0,
inference(resolve,[status(thm)],[c_366,c_989]) ).
cnf(c_416,negated_conjecture,
( k4_xboole_0(k7_lopclset(sK0),k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),A)) = k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v17_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_136,c_133]) ).
cnf(c_990,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,A)) = k4_xboole_0(k7_lopclset(sK0),k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v17_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_416]) ).
cnf(c_991,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,A)) = k4_xboole_0(k7_lopclset(sK0),k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0)
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_363,c_990]) ).
cnf(c_992,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,A)) = k4_xboole_0(k7_lopclset(sK0),k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v3_realset2(sK0) ),
inference(resolve,[status(thm)],[c_364,c_991]) ).
cnf(c_993,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,A)) = k4_xboole_0(k7_lopclset(sK0),k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_365,c_992]) ).
cnf(c_417,negated_conjecture,
( k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,A)) = k4_xboole_0(k7_lopclset(sK0),k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),A))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_366,c_993]) ).
cnf(c_586,negated_conjecture,
k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,k5_lattices(sK0))) != k7_lopclset(sK0),
inference(paramod,[status(thm)],[c_413,c_367]) ).
cnf(c_994,negated_conjecture,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_366,c_265]) ).
cnf(c_742,negated_conjecture,
m1_subset_1(k5_lattices(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_363,c_994]) ).
cnf(c_995,negated_conjecture,
k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,k5_lattices(sK0))) = k4_xboole_0(k7_lopclset(sK0),k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k5_lattices(sK0))),
inference(resolve,[status(thm)],[c_742,c_417]) ).
cnf(c_996,negated_conjecture,
k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,k5_lattices(sK0))) = k4_xboole_0(k7_lopclset(sK0),k1_xboole_0),
inference(paramod,[status(thm)],[c_415,c_995]) ).
cnf(c_997,negated_conjecture,
k8_funct_2(u1_struct_0(sK0),k1_zfmisc_1(k7_lopclset(sK0)),k9_lopclset(sK0),k7_lattices(sK0,k5_lattices(sK0))) = k7_lopclset(sK0),
inference(paramod,[status(thm)],[c_356,c_996]) ).
cnf(c_983,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_586,c_997]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT291+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.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 20:30:14 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.36 % Process 2472967 was started by sandbox on n009,
% 0.12/0.36 % Fri Sep 25 20:30:14 2026
% 0.12/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.38
% 0.12/0.38 % From the command line: assign(max_seconds, 300).
% 3.24/0.82
% 3.24/0.82 % SZS status Theorem for theBenchmark
% 3.24/0.82
% 3.24/0.82 % Proof 1 at 0.40 (+ 0.02) seconds.
% 3.24/0.82 % Length of proof is 29.
% 3.24/0.82 % Level of proof is 5.
% 3.24/0.82 % Maximum clause weight is 28.000.
% 3.24/0.82 % Given clauses 223.
% 3.24/0.82
% 3.24/0.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------