%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT337+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n007.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 : Fri Sep 25 01:59:23 PM UTC 2026
% Result : Theorem 4.20s 1.28s
% Output : CNFRefutation 4.20s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f458ERROR: Could not build tree for root c_11206ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( l3_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( r3_lattices(X0,X1,X2)
& l3_lattices(X0)
& v17_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0) )
=> ( l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t87_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( l3_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( r3_lattices(X0,X1,X2)
& l3_lattices(X0)
& v17_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0) )
=> ( l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
& ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f12,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( v17_lattices(X0)
& ~ v3_struct_0(X0) )
=> ( v16_lattices(X0)
& v15_lattices(X0)
& v14_lattices(X0)
& v13_lattices(X0)
& v11_lattices(X0)
& ~ v3_struct_0(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc5_lattices) ).
fof(f13,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( v16_lattices(X0)
& v15_lattices(X0)
& v11_lattices(X0)
& ~ v3_struct_0(X0) )
=> ( v17_lattices(X0)
& ~ v3_struct_0(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc6_lattices) ).
fof(f14,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( v11_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0) )
=> ( v12_lattices(X0)
& v10_lattices(X0)
& v9_lattices(X0)
& v8_lattices(X0)
& v7_lattices(X0)
& v6_lattices(X0)
& v5_lattices(X0)
& v4_lattices(X0)
& ~ v3_struct_0(X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc7_lattices) ).
fof(f18,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X2,u1_struct_0(X0))
& m1_subset_1(X1,u1_struct_0(X0))
& l3_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0) )
=> ( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
& ~ v1_xboole_0(k22_filter_2(X0,X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k22_filter_2) ).
fof(f81,axiom,
! [X0] :
( ( l3_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0) )
=> ! [X1] :
( ( m2_lattice4(X1,X0)
& ~ v1_xboole_0(X1) )
=> ( v11_lattices(X0)
=> v11_lattices(k23_filter_2(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t78_filter_2) ).
fof(f97,plain,
? [X0] :
( l3_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
& ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& r3_lattices(X0,X1,X2)
& l3_lattices(X0)
& v17_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0)
& ( ~ l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f98,plain,
? [X0] :
( l3_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0)
& ? [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
& ? [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
& r3_lattices(X0,X1,X2)
& l3_lattices(X0)
& v17_lattices(X0)
& v10_lattices(X0)
& ~ v3_struct_0(X0)
& ( ~ l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v17_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ) ) ) ),
inference(flattening,[],[f97]) ).
fof(f114,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| ( v16_lattices(X0)
& v15_lattices(X0)
& v14_lattices(X0)
& v13_lattices(X0)
& v11_lattices(X0)
& ~ v3_struct_0(X0) ) ),
inference(ennf_transformation,[],[f12]) ).
fof(f115,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| ( v16_lattices(X0)
& v15_lattices(X0)
& v14_lattices(X0)
& v13_lattices(X0)
& v11_lattices(X0)
& ~ v3_struct_0(X0) ) ),
inference(flattening,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v11_lattices(X0)
| v3_struct_0(X0)
| ( v17_lattices(X0)
& ~ v3_struct_0(X0) ) ),
inference(ennf_transformation,[],[f13]) ).
fof(f117,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v11_lattices(X0)
| v3_struct_0(X0)
| ( v17_lattices(X0)
& ~ v3_struct_0(X0) ) ),
inference(flattening,[],[f116]) ).
fof(f118,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v11_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ( v12_lattices(X0)
& v10_lattices(X0)
& v9_lattices(X0)
& v8_lattices(X0)
& v7_lattices(X0)
& v6_lattices(X0)
& v5_lattices(X0)
& v4_lattices(X0)
& ~ v3_struct_0(X0) ) ),
inference(ennf_transformation,[],[f14]) ).
fof(f119,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v11_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ( v12_lattices(X0)
& v10_lattices(X0)
& v9_lattices(X0)
& v8_lattices(X0)
& v7_lattices(X0)
& v6_lattices(X0)
& v5_lattices(X0)
& v4_lattices(X0)
& ~ v3_struct_0(X0) ) ),
inference(flattening,[],[f118]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
& ~ v1_xboole_0(k22_filter_2(X0,X1,X2)) ) ),
inference(ennf_transformation,[],[f18]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ( m2_lattice4(k22_filter_2(X0,X1,X2),X0)
& ~ v1_xboole_0(k22_filter_2(X0,X1,X2)) ) ),
inference(flattening,[],[f122]) ).
fof(f177,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ v11_lattices(X0)
| v11_lattices(k23_filter_2(X0,X1)) ) ),
inference(ennf_transformation,[],[f81]) ).
fof(f178,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ! [X1] :
( ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ v11_lattices(X0)
| v11_lattices(k23_filter_2(X0,X1)) ) ),
inference(flattening,[],[f177]) ).
fof(f189,plain,
( l3_lattices(sK3)
& v10_lattices(sK3)
& ~ v3_struct_0(sK3)
& m1_subset_1(sK4,u1_struct_0(sK3))
& m1_subset_1(sK5,u1_struct_0(sK3))
& r3_lattices(sK3,sK4,sK5)
& l3_lattices(sK3)
& v17_lattices(sK3)
& v10_lattices(sK3)
& ~ v3_struct_0(sK3)
& ( ~ l3_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v17_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5)],[f98]) ).
fof(f223,plain,
l3_lattices(sK3),
inference(cnf_transformation,[],[f189]) ).
fof(f224,plain,
v10_lattices(sK3),
inference(cnf_transformation,[],[f189]) ).
fof(f225,plain,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f189]) ).
fof(f226,plain,
m1_subset_1(sK4,u1_struct_0(sK3)),
inference(cnf_transformation,[],[f189]) ).
fof(f227,plain,
m1_subset_1(sK5,u1_struct_0(sK3)),
inference(cnf_transformation,[],[f189]) ).
fof(f228,plain,
r3_lattices(sK3,sK4,sK5),
inference(cnf_transformation,[],[f189]) ).
fof(f230,plain,
v17_lattices(sK3),
inference(cnf_transformation,[],[f189]) ).
fof(f233,plain,
( ~ l3_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v17_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ),
inference(cnf_transformation,[],[f189]) ).
fof(f254,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v16_lattices(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f255,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v15_lattices(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f258,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| v3_struct_0(X0)
| v11_lattices(X0) ),
inference(cnf_transformation,[],[f115]) ).
fof(f260,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ v11_lattices(X0)
| v3_struct_0(X0)
| v17_lattices(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f271,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v11_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f184]) ).
fof(f274,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_lattice4(k22_filter_2(X0,X1,X2),X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f275,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(k22_filter_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f446,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ v11_lattices(X0)
| v11_lattices(k23_filter_2(X0,X1)) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_49,negated_conjecture,
( v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ l3_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v17_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ),
inference(cnf_transformation,[],[f233]) ).
tcf(c_52,negated_conjecture,
v17_lattices(sK3),
inference(cnf_transformation,[],[f230]) ).
tcf(c_54,negated_conjecture,
r3_lattices(sK3,sK4,sK5),
inference(cnf_transformation,[],[f228]) ).
tcf(c_55,negated_conjecture,
m1_subset_1(sK5,u1_struct_0(sK3)),
inference(cnf_transformation,[],[f227]) ).
tcf(c_56,negated_conjecture,
m1_subset_1(sK4,u1_struct_0(sK3)),
inference(cnf_transformation,[],[f226]) ).
tcf(c_57,negated_conjecture,
~ v3_struct_0(sK3),
inference(cnf_transformation,[],[f225]) ).
tcf(c_58,negated_conjecture,
v10_lattices(sK3),
inference(cnf_transformation,[],[f224]) ).
tcf(c_59,negated_conjecture,
l3_lattices(sK3),
inference(cnf_transformation,[],[f223]) ).
tcf(c_74,plain,
! [X0: $i] :
( v11_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v17_lattices(X0) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_77,plain,
! [X0: $i] :
( v15_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v17_lattices(X0) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_78,plain,
! [X0: $i] :
( v16_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v17_lattices(X0) ),
inference(cnf_transformation,[],[f254]) ).
tcf(c_79,plain,
! [X0: $i] :
( v17_lattices(X0)
| v3_struct_0(X0)
| ~ v16_lattices(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f260]) ).
tcf(c_89,plain,
! [X0: $i] :
( sP0(X0)
| v3_struct_0(X0)
| ~ v11_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v1_xboole_0(k22_filter_2(X0,X1,X2)) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X1)
| m2_lattice4(k22_filter_2(X1,X0,X2),X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X0,u1_struct_0(X1)) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_264,plain,
! [X0: $i,X1: $i] :
( v1_xboole_0(X0)
| v3_struct_0(X1)
| v11_lattices(k23_filter_2(X1,X0))
| ~ v11_lattices(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X1)
| ~ m2_lattice4(X0,X1) ),
inference(cnf_transformation,[],[f446]) ).
tcf(c_266,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2)
| ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2))) ),
inference(cnf_transformation,[],[f454]) ).
tcf(c_267,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f455]) ).
tcf(c_268,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f456]) ).
tcf(c_269,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f457]) ).
tcf(c_270,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r3_lattices(X0,X1,X2) ),
inference(cnf_transformation,[],[f458]) ).
tcf(c_328,plain,
( v16_lattices(sK3)
| v3_struct_0(sK3)
| ~ l3_lattices(sK3)
| ~ v17_lattices(sK3) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_329,plain,
( v15_lattices(sK3)
| v3_struct_0(sK3)
| ~ l3_lattices(sK3)
| ~ v17_lattices(sK3) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_332,plain,
( v11_lattices(sK3)
| v3_struct_0(sK3)
| ~ l3_lattices(sK3)
| ~ v17_lattices(sK3) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_359,plain,
( sP0(sK3)
| v3_struct_0(sK3)
| ~ v11_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_3801,plain,
! [X0: $i] :
( v3_struct_0(X0)
| v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v16_lattices(X0)
| ~ v11_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ l3_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ( k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_49,c_79]) ).
tcf(c_3802,plain,
( v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v16_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v11_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v15_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ l3_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ),
inference(unflattening,[status(thm)],[c_3801]) ).
tcf(c_3848,plain,
! [X0: $i] :
( v11_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_52,c_74]) ).
tcf(c_3849,plain,
( v11_lattices(sK3)
| v3_struct_0(sK3)
| ~ l3_lattices(sK3) ),
inference(unflattening,[status(thm)],[c_3848]) ).
tcf(c_3850,plain,
v11_lattices(sK3),
inference(global_subsumption_just,[status(thm)],[c_3849,c_59,c_52,c_57,c_332]) ).
tcf(c_5497,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| l3_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ( X2 != sK5 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_270]) ).
tcf(c_5498,plain,
( v3_struct_0(sK3)
| l3_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v12_lattices(sK3)
| ~ v16_lattices(sK3)
| ~ v15_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,u1_struct_0(sK3)) ),
inference(unflattening,[status(thm)],[c_5497]) ).
tcf(c_5504,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v16_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ( X2 != sK5 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_269]) ).
tcf(c_5505,plain,
( v3_struct_0(sK3)
| v16_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v12_lattices(sK3)
| ~ v16_lattices(sK3)
| ~ v15_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,u1_struct_0(sK3)) ),
inference(unflattening,[status(thm)],[c_5504]) ).
tcf(c_5511,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v15_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ( X2 != sK5 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_268]) ).
tcf(c_5512,plain,
( v3_struct_0(sK3)
| v15_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v12_lattices(sK3)
| ~ v16_lattices(sK3)
| ~ v15_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,u1_struct_0(sK3)) ),
inference(unflattening,[status(thm)],[c_5511]) ).
tcf(c_5518,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| v10_lattices(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ( X2 != sK5 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_267]) ).
tcf(c_5519,plain,
( v3_struct_0(sK3)
| v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v12_lattices(sK3)
| ~ v16_lattices(sK3)
| ~ v15_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,u1_struct_0(sK3)) ),
inference(unflattening,[status(thm)],[c_5518]) ).
tcf(c_5525,plain,
! [X0: $i,X1: $i,X2: $i] :
( v3_struct_0(X0)
| ~ v12_lattices(X0)
| ~ v16_lattices(X0)
| ~ v15_lattices(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v3_struct_0(k23_filter_2(X0,k22_filter_2(X0,X1,X2)))
| ( X2 != sK5 )
| ( X1 != sK4 )
| ( X0 != sK3 ) ),
inference(resolution_lifted,[status(thm)],[c_54,c_266]) ).
tcf(c_5526,plain,
( v3_struct_0(sK3)
| ~ v12_lattices(sK3)
| ~ v16_lattices(sK3)
| ~ v15_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,u1_struct_0(sK3))
| ~ v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ),
inference(unflattening,[status(thm)],[c_5525]) ).
tcf(c_8444,definition,
iPr_def_10 = k22_filter_2(sK3,sK4,sK5),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_8445,definition,
iPr_def_11 = k23_filter_2(sK3,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_8446,definition,
iPr_def_12 = u1_struct_0(sK3),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_8455,plain,
v11_lattices(sK3),
inference(demodulation,[status(thm)],[c_3850]) ).
tcf(c_8458,negated_conjecture,
m1_subset_1(sK4,iPr_def_12),
inference(demodulation,[status(thm)],[c_56,c_8446]) ).
tcf(c_8459,negated_conjecture,
m1_subset_1(sK5,iPr_def_12),
inference(demodulation,[status(thm)],[c_55]) ).
tcf(c_8460,negated_conjecture,
l3_lattices(sK3),
inference(demodulation,[status(thm)],[c_59]) ).
tcf(c_8461,negated_conjecture,
v10_lattices(sK3),
inference(demodulation,[status(thm)],[c_58]) ).
tcf(c_8462,negated_conjecture,
~ v3_struct_0(sK3),
inference(demodulation,[status(thm)],[c_57]) ).
tcf(c_11022,plain,
( v11_lattices(iPr_def_11)
| v1_xboole_0(iPr_def_10)
| v3_struct_0(sK3)
| ~ v11_lattices(sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m2_lattice4(iPr_def_10,sK3) ),
inference(superposition,[status(thm)],[c_8445,c_264]) ).
tcf(c_11179,plain,
( v3_struct_0(sK3)
| ~ v1_xboole_0(iPr_def_10)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,u1_struct_0(sK3)) ),
inference(superposition,[status(thm)],[c_8444,c_92]) ).
tcf(c_11180,plain,
( v3_struct_0(sK3)
| ~ v1_xboole_0(iPr_def_10)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_11179,c_8446]) ).
tcf(c_11181,plain,
~ v1_xboole_0(iPr_def_10),
inference(forward_subsumption_resolution,[status(thm)],[c_11180,c_8462,c_8460,c_8461,c_8459,c_8458]) ).
tcf(c_11195,plain,
( v3_struct_0(sK3)
| m2_lattice4(iPr_def_10,sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,u1_struct_0(sK3))
| ~ m1_subset_1(sK4,u1_struct_0(sK3)) ),
inference(superposition,[status(thm)],[c_8444,c_93]) ).
tcf(c_11197,plain,
( v3_struct_0(sK3)
| m2_lattice4(iPr_def_10,sK3)
| ~ l3_lattices(sK3)
| ~ v10_lattices(sK3)
| ~ m1_subset_1(sK5,iPr_def_12)
| ~ m1_subset_1(sK4,iPr_def_12) ),
inference(light_normalisation,[status(thm)],[c_11195,c_8446]) ).
tcf(c_11198,plain,
m2_lattice4(iPr_def_10,sK3),
inference(forward_subsumption_resolution,[status(thm)],[c_11197,c_8462,c_8460,c_8461,c_8459,c_8458]) ).
fof(f183,definition,
! [X0] :
( ~ sP0(X0)
| ( v12_lattices(X0)
& v10_lattices(X0)
& v9_lattices(X0)
& v8_lattices(X0)
& v7_lattices(X0)
& v6_lattices(X0)
& v5_lattices(X0)
& v4_lattices(X0)
& ~ v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f184,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v11_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP0(X0) ),
inference(definition_folding,[],[f119,f183]) ).
fof(f190,plain,
! [X0] :
( ~ sP0(X0)
| ( v12_lattices(X0)
& v10_lattices(X0)
& v9_lattices(X0)
& v8_lattices(X0)
& v7_lattices(X0)
& v6_lattices(X0)
& v5_lattices(X0)
& v4_lattices(X0)
& ~ v3_struct_0(X0) ) ),
inference(nnf_transformation,[],[f183]) ).
fof(f262,plain,
! [X0] :
( ~ sP0(X0)
| v12_lattices(X0) ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_88,plain,
! [X0: $i] :
( v12_lattices(X0)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f262]) ).
tcf(c_281,plain,
( v12_lattices(sK3)
| ~ sP0(sK3) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_5499,plain,
l3_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))),
inference(global_subsumption_just,[status(thm)],[c_5498,c_59,c_58,c_52,c_57,c_56,c_55,c_281,c_328,c_329,c_332,c_359,c_5498]) ).
tcf(c_5506,plain,
v16_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))),
inference(global_subsumption_just,[status(thm)],[c_5505,c_59,c_58,c_52,c_57,c_56,c_55,c_281,c_328,c_329,c_332,c_359,c_5505]) ).
tcf(c_5513,plain,
v15_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))),
inference(global_subsumption_just,[status(thm)],[c_5512,c_59,c_58,c_52,c_57,c_56,c_55,c_281,c_328,c_329,c_332,c_359,c_5512]) ).
tcf(c_5520,plain,
v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))),
inference(global_subsumption_just,[status(thm)],[c_5519,c_59,c_58,c_52,c_57,c_56,c_55,c_281,c_328,c_329,c_332,c_359,c_5519]) ).
tcf(c_5527,plain,
~ v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))),
inference(global_subsumption_just,[status(thm)],[c_5526,c_59,c_58,c_52,c_57,c_56,c_55,c_281,c_328,c_329,c_332,c_359,c_5526]) ).
tcf(c_5720,plain,
( v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v16_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v11_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v15_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3802,c_5499]) ).
tcf(c_5722,plain,
( v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v11_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v15_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5720,c_5506]) ).
tcf(c_5724,plain,
( v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v11_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v10_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5722,c_5513]) ).
tcf(c_5728,plain,
( v3_struct_0(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5)))
| ~ v11_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5724,c_5520]) ).
tcf(c_5730,plain,
~ v11_lattices(k23_filter_2(sK3,k22_filter_2(sK3,sK4,sK5))),
inference(backward_subsumption_resolution,[status(thm)],[c_5728,c_5527]) ).
tcf(c_8449,plain,
~ v11_lattices(iPr_def_11),
inference(demodulation,[status(thm)],[c_5730]) ).
tcf(c_11023,plain,
( v1_xboole_0(iPr_def_10)
| ~ m2_lattice4(iPr_def_10,sK3) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11022,c_8449,c_8462,c_8455,c_8460,c_8461]) ).
tcf(c_11206,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_11198,c_11181,c_11023]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT337+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 21:09:07 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 4.20/1.28 % SZS status Started for theBenchmark.p
% 4.20/1.28 % SZS status Theorem for theBenchmark.p
% 4.20/1.28
% 4.20/1.28 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.20/1.28
% 4.20/1.28 % ------ iProver source info
% 4.20/1.28
% 4.20/1.28 % git: date: 2026-07-19 20:42:38 +0200
% 4.20/1.28 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.20/1.28 % git: non_committed_changes: false
% 4.20/1.28
% 4.20/1.28 % ------ Parsing...
% 4.20/1.28 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.20/1.28
% 4.20/1.28 % ------ Preprocessing... sup_sim: 0 sf_s rm: 10 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 0 sf_s rm: 16 0s sf_e pe_s pe_e %
% 4.20/1.28
% 4.20/1.28 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.20/1.28
% 4.20/1.28 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 4.20/1.28 % ------ Proving...
% 4.20/1.28 % ------ Problem Properties
% 4.20/1.28
% 4.20/1.28 %
% 4.20/1.28 % clauses 148
% 4.20/1.28 % conjectures 5
% 4.20/1.28 % EPR 72
% 4.20/1.28 % Horn 125
% 4.20/1.28 % unary 81
% 4.20/1.28 % binary 32
% 4.20/1.28 % lits 339
% 4.20/1.28 % lits eq 14
% 4.20/1.28 % fd_pure 0
% 4.20/1.28 % fd_pseudo 0
% 4.20/1.28 % fd_cond 1
% 4.20/1.28 % fd_pseudo_cond 4
% 4.20/1.28 % AC symbols 0
% 4.20/1.28
% 4.20/1.28 % ------ Schedule dynamic 5 is on
% 4.20/1.28
% 4.20/1.28 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 4.20/1.28
% 4.20/1.28
% 4.20/1.28 % ------
% 4.20/1.28 % Current options:
% 4.20/1.28 % ------
% 4.20/1.28
% 4.20/1.28
% 4.20/1.28 %
% 4.20/1.28
% 4.20/1.28 % ------ Proving...
% 4.20/1.28 %
% 4.20/1.28
% 4.20/1.28 % SZS status Theorem for theBenchmark.p
% 4.20/1.28
% 4.20/1.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.20/1.28
% 4.20/1.28
%------------------------------------------------------------------------------