%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : LAT326+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 10:34:28 PM UTC 2025
% Result : Theorem 247.11s 31.38s
% Output : CNFRefutation 247.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 17
% Syntax : Number of formulae : 366 ( 212 unt; 0 def)
% Number of atoms : 907 ( 29 equ)
% Maximal formula atoms : 19 ( 2 avg)
% Number of connectives : 952 ( 411 ~; 414 |; 88 &)
% ( 0 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 84 ( 1 sgn 36 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(t62_filter_2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( ( ~ v1_xboole_0(B)
& m2_lattice4(B,A) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,k2_zfmisc_1(B,B),B)
& m2_relset_1(C,k2_zfmisc_1(B,B),B) )
=> ! [D] :
( ( v1_funct_1(D)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& m2_relset_1(D,k2_zfmisc_1(B,B),B) )
=> ( ( C = k1_realset1(u2_lattices(A),B)
& D = k1_realset1(u1_lattices(A),B) )
=> ( v1_binop_1(C,B)
& v2_binop_1(C,B)
& v1_binop_1(D,B)
& v2_binop_1(D,B)
& r1_lattice2(B,C,D)
& r1_lattice2(B,D,C) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t62_filter_2) ).
fof(t62_filter_2_negated,plain,
~ ! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( ( ~ v1_xboole_0(B)
& m2_lattice4(B,A) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,k2_zfmisc_1(B,B),B)
& m2_relset_1(C,k2_zfmisc_1(B,B),B) )
=> ! [D] :
( ( v1_funct_1(D)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& m2_relset_1(D,k2_zfmisc_1(B,B),B) )
=> ( ( C = k1_realset1(u2_lattices(A),B)
& D = k1_realset1(u1_lattices(A),B) )
=> ( v1_binop_1(C,B)
& v2_binop_1(C,B)
& v1_binop_1(D,B)
& v2_binop_1(D,B)
& r1_lattice2(B,C,D)
& r1_lattice2(B,D,C) ) ) ) ) ) ),
inference(negate_conjecture,[status(cth)],[t62_filter_2]) ).
cnf(13,plain,
( ~ v1_binop_1(sK3,sK2)
| ~ v1_binop_1(sK4,sK2)
| ~ v2_binop_1(sK3,sK2)
| ~ v2_binop_1(sK4,sK2)
| ~ r1_lattice2(sK2,sK3,sK4)
| ~ r1_lattice2(sK2,sK4,sK3) ),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l0,plain,
( ~ v1_binop_1(sK3,sK2)
| ~ v1_binop_1(sK4,sK2)
| ~ v2_binop_1(sK3,sK2)
| ~ v2_binop_1(sK4,sK2)
| ~ r1_lattice2(sK2,sK3,sK4)
| ~ r1_lattice2(sK2,sK4,sK3) ),
inference(instantiation,[status(thm)],[13]) ).
fof(t1_filter_2,plain,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( ~ v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& m2_relset_1(C,k2_zfmisc_1(A,A),A) )
=> ! [D] :
( ( v1_funct_1(D)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& m2_relset_1(D,k2_zfmisc_1(B,B),B) )
=> ( D = k1_realset1(C,B)
=> ( ( v1_binop_1(C,A)
=> v1_binop_1(D,B) )
& ( v3_binop_1(C,A)
=> v3_binop_1(D,B) )
& ( v2_binop_1(C,A)
=> v2_binop_1(D,B) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_filter_2) ).
cnf(101,plain,
( ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X3,X3),X3)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X2,k2_zfmisc_1(X3,X3),X3)
| X2 != k1_realset1(X0,X3)
| ~ v2_binop_1(X0,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| v2_binop_1(X2,X3)
| v1_xboole_0(X1)
| v1_xboole_0(X3) ),
inference(cnf,[status(esa)],[t1_filter_2]) ).
cnf(l2189,plain,
( ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2)
| ~ m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2)
| sK4 != k1_realset1(u1_lattices(sK1),sK2)
| ~ v2_binop_1(u1_lattices(sK1),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_1(sK4)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v2_binop_1(sK4,sK2)
| v1_xboole_0(u1_struct_0(sK1))
| v1_xboole_0(sK2) ),
inference(instantiation,[status(thm)],[101]) ).
fof(fc4_lattice2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v6_lattices(A)
& l1_lattices(A) )
=> ( v1_relat_1(u1_lattices(A))
& v1_funct_1(u1_lattices(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_binop_1(u1_lattices(A),u1_struct_0(A))
& v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_lattice2) ).
cnf(67,plain,
( ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc4_lattice2]) ).
cnf(l2199,plain,
( ~ l1_lattices(sK1)
| ~ v6_lattices(sK1)
| v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[67]) ).
cnf(10,plain,
m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l3207,plain,
m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(l2212,plain,
( ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2)
| ~ m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2)
| sK3 != k1_realset1(u2_lattices(sK1),sK2)
| ~ v2_binop_1(u2_lattices(sK1),u1_struct_0(sK1))
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_1(sK3)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v2_binop_1(sK3,sK2)
| v1_xboole_0(u1_struct_0(sK1))
| v1_xboole_0(sK2) ),
inference(instantiation,[status(thm)],[101]) ).
fof(dt_l3_lattices,plain,
! [A] :
( l3_lattices(A)
=> ( l1_lattices(A)
& l2_lattices(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
cnf(29,plain,
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf,[status(esa)],[dt_l3_lattices]) ).
cnf(l2520,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(5,plain,
v1_funct_1(sK3),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2327,plain,
v1_funct_1(sK3),
inference(instantiation,[status(thm)],[5]) ).
fof(fc3_lattice2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v5_lattices(A)
& l2_lattices(A) )
=> ( v1_relat_1(u2_lattices(A))
& v1_funct_1(u2_lattices(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u2_lattices(A),u1_struct_0(A))
& v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_lattice2) ).
cnf(60,plain,
( ~ l2_lattices(X0)
| ~ v5_lattices(X0)
| v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc3_lattice2]) ).
cnf(l2308,plain,
( ~ l2_lattices(sK1)
| ~ v5_lattices(sK1)
| v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[60]) ).
fof(dt_u1_lattices,plain,
! [A] :
( l1_lattices(A)
=> ( v1_funct_1(u1_lattices(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_lattices) ).
cnf(35,plain,
( ~ l1_lattices(X0)
| m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf,[status(esa)],[dt_u1_lattices]) ).
cnf(l2272,plain,
( ~ l1_lattices(sK1)
| m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[35]) ).
fof(fc5_lattice2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v7_lattices(A)
& l1_lattices(A) )
=> ( v1_relat_1(u1_lattices(A))
& v1_funct_1(u1_lattices(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u1_lattices(A),u1_struct_0(A))
& v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_lattice2) ).
cnf(74,plain,
( ~ l1_lattices(X0)
| ~ v7_lattices(X0)
| v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc5_lattice2]) ).
cnf(l3204,plain,
( ~ l1_lattices(sK1)
| ~ v7_lattices(sK1)
| v2_binop_1(u1_lattices(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[74]) ).
cnf(9,plain,
v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2381,plain,
v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[9]) ).
fof(t5_filter_2,plain,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( ~ v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) )
=> ! [C] :
( ( v1_funct_1(C)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& m2_relset_1(C,k2_zfmisc_1(A,A),A) )
=> ! [D] :
( ( v1_funct_1(D)
& v1_funct_2(D,k2_zfmisc_1(A,A),A)
& m2_relset_1(D,k2_zfmisc_1(A,A),A) )
=> ! [E] :
( ( v1_funct_1(E)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& m2_relset_1(E,k2_zfmisc_1(B,B),B) )
=> ! [F] :
( ( v1_funct_1(F)
& v1_funct_2(F,k2_zfmisc_1(B,B),B)
& m2_relset_1(F,k2_zfmisc_1(B,B),B) )
=> ( ( E = k1_realset1(C,B)
& F = k1_realset1(D,B)
& r1_lattice2(A,C,D) )
=> r1_lattice2(B,E,F) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_filter_2) ).
cnf(109,plain,
( ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X3,k2_zfmisc_1(X4,X4),X4)
| ~ v1_funct_2(X5,k2_zfmisc_1(X4,X4),X4)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X4,X4),X4)
| ~ m2_relset_1(X5,k2_zfmisc_1(X4,X4),X4)
| X3 != k1_realset1(X0,X4)
| X5 != k1_realset1(X2,X4)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X2)
| ~ v1_funct_1(X3)
| ~ v1_funct_1(X5)
| ~ r1_lattice2(X1,X0,X2)
| ~ m1_subset_1(X4,k1_zfmisc_1(X1))
| v1_xboole_0(X1)
| v1_xboole_0(X4)
| r1_lattice2(X4,X3,X5) ),
inference(cnf,[status(esa)],[t5_filter_2]) ).
cnf(l2201,plain,
( ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2)
| ~ v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2)
| ~ m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2)
| ~ m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2)
| sK4 != k1_realset1(u1_lattices(sK1),sK2)
| sK3 != k1_realset1(u2_lattices(sK1),sK2)
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_1(sK4)
| ~ v1_funct_1(sK3)
| ~ r1_lattice2(u1_struct_0(sK1),u1_lattices(sK1),u2_lattices(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(u1_struct_0(sK1))
| v1_xboole_0(sK2)
| r1_lattice2(sK2,sK4,sK3) ),
inference(instantiation,[status(thm)],[109]) ).
cnf(0,plain,
~ v3_struct_0(sK1),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2473,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(t41_lattice2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> r1_lattice2(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t41_lattice2) ).
cnf(107,plain,
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)) ),
inference(cnf,[status(esa)],[t41_lattice2]) ).
cnf(l2209,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| r1_lattice2(u1_struct_0(sK1),u1_lattices(sK1),u2_lattices(sK1)) ),
inference(instantiation,[status(thm)],[107]) ).
cnf(8,plain,
v1_funct_1(sK4),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2203,plain,
v1_funct_1(sK4),
inference(instantiation,[status(thm)],[8]) ).
cnf(2,plain,
l3_lattices(sK1),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2587,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(61,plain,
( ~ l2_lattices(X0)
| ~ v5_lattices(X0)
| v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc3_lattice2]) ).
cnf(l2262,plain,
( ~ l2_lattices(sK1)
| ~ v5_lattices(sK1)
| v2_binop_1(u2_lattices(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[61]) ).
fof(fc2_lattice2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v4_lattices(A)
& l2_lattices(A) )
=> ( v1_relat_1(u2_lattices(A))
& v1_funct_1(u2_lattices(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_binop_1(u2_lattices(A),u1_struct_0(A))
& v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_lattice2) ).
cnf(52,plain,
( ~ l2_lattices(X0)
| ~ v4_lattices(X0)
| v3_struct_0(X0)
| v1_funct_1(u2_lattices(X0)) ),
inference(cnf,[status(esa)],[fc2_lattice2]) ).
cnf(l2227,plain,
( ~ l2_lattices(sK1)
| ~ v4_lattices(sK1)
| v3_struct_0(sK1)
| v1_funct_1(u2_lattices(sK1)) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(3,plain,
~ v1_xboole_0(sK2),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2221,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(6,plain,
v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2234,plain,
v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2265,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2564,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(99,plain,
( ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X3,X3),X3)
| ~ m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X2,k2_zfmisc_1(X3,X3),X3)
| X2 != k1_realset1(X0,X3)
| ~ v1_binop_1(X0,X1)
| ~ v1_funct_1(X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(X1))
| v1_binop_1(X2,X3)
| v1_xboole_0(X1)
| v1_xboole_0(X3) ),
inference(cnf,[status(esa)],[t1_filter_2]) ).
cnf(l2184,plain,
( ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2)
| ~ m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2)
| sK4 != k1_realset1(u1_lattices(sK1),sK2)
| ~ v1_binop_1(u1_lattices(sK1),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_1(sK4)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_binop_1(sK4,sK2)
| v1_xboole_0(u1_struct_0(sK1))
| v1_xboole_0(sK2) ),
inference(instantiation,[status(thm)],[99]) ).
cnf(30,plain,
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf,[status(esa)],[dt_l3_lattices]) ).
cnf(l2237,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3228,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(12,plain,
sK4 = k1_realset1(u1_lattices(sK1),sK2),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l3202,plain,
sK4 = k1_realset1(u1_lattices(sK1),sK2),
inference(instantiation,[status(thm)],[12]) ).
fof(dt_u2_lattices,plain,
! [A] :
( l2_lattices(A)
=> ( v1_funct_1(u2_lattices(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u2_lattices) ).
cnf(38,plain,
( ~ l2_lattices(X0)
| m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf,[status(esa)],[dt_u2_lattices]) ).
cnf(l2490,plain,
( ~ l2_lattices(sK1)
| m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l2277,plain,
( ~ l1_lattices(sK1)
| ~ v6_lattices(sK1)
| v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[67]) ).
cnf(36,plain,
( ~ l2_lattices(X0)
| v1_funct_1(u2_lattices(X0)) ),
inference(cnf,[status(esa)],[dt_u2_lattices]) ).
cnf(l2477,plain,
( ~ l2_lattices(sK1)
| v1_funct_1(u2_lattices(sK1)) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l3210,plain,
v1_funct_1(sK4),
inference(instantiation,[status(thm)],[8]) ).
cnf(l2518,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
fof(cc1_lattices,plain,
! [A] :
( l3_lattices(A)
=> ( ( ~ v3_struct_0(A)
& v10_lattices(A) )
=> ( ~ v3_struct_0(A)
& v4_lattices(A)
& v5_lattices(A)
& v6_lattices(A)
& v7_lattices(A)
& v8_lattices(A)
& v9_lattices(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattices) ).
cnf(17,plain,
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| v5_lattices(X0) ),
inference(cnf,[status(esa)],[cc1_lattices]) ).
cnf(l2481,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v5_lattices(sK1) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(18,plain,
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| v6_lattices(X0) ),
inference(cnf,[status(esa)],[cc1_lattices]) ).
cnf(l2521,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v6_lattices(sK1) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3206,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2266,plain,
( ~ l1_lattices(sK1)
| m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2231,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(33,plain,
( ~ l1_lattices(X0)
| v1_funct_1(u1_lattices(X0)) ),
inference(cnf,[status(esa)],[dt_u1_lattices]) ).
cnf(l3219,plain,
( ~ l1_lattices(sK1)
| v1_funct_1(u1_lattices(sK1)) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l3203,plain,
v1_funct_1(sK4),
inference(instantiation,[status(thm)],[8]) ).
cnf(11,plain,
sK3 = k1_realset1(u2_lattices(sK1),sK2),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2271,plain,
sK3 = k1_realset1(u2_lattices(sK1),sK2),
inference(instantiation,[status(thm)],[11]) ).
fof(dt_m2_lattice4,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
cnf(31,plain,
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(cnf,[status(esa)],[dt_m2_lattice4]) ).
cnf(l3201,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2220,plain,
( ~ l2_lattices(sK1)
| m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l3238,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2592,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2491,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3884,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2615,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v6_lattices(sK1) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3221,plain,
m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(7,plain,
m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l2264,plain,
m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3298,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2276,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l2617,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2341,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v5_lattices(sK1) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(1,plain,
v10_lattices(sK1),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l3387,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2289,plain,
( ~ l1_lattices(sK1)
| ~ v6_lattices(sK1)
| v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[67]) ).
cnf(l2475,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3239,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2280,plain,
v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[9]) ).
cnf(l3044,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3979,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2251,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(66,plain,
( ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0)
| v1_funct_1(u1_lattices(X0)) ),
inference(cnf,[status(esa)],[fc4_lattice2]) ).
cnf(l2216,plain,
( ~ l1_lattices(sK1)
| ~ v6_lattices(sK1)
| v3_struct_0(sK1)
| v1_funct_1(u1_lattices(sK1)) ),
inference(instantiation,[status(thm)],[66]) ).
cnf(l3473,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2748,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v6_lattices(sK1) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(72,plain,
( ~ l1_lattices(X0)
| ~ v7_lattices(X0)
| v3_struct_0(X0)
| v1_funct_1(u1_lattices(X0)) ),
inference(cnf,[status(esa)],[fc5_lattice2]) ).
cnf(l3213,plain,
( ~ l1_lattices(sK1)
| ~ v7_lattices(sK1)
| v3_struct_0(sK1)
| v1_funct_1(u1_lattices(sK1)) ),
inference(instantiation,[status(thm)],[72]) ).
cnf(4,plain,
m2_lattice4(sK2,sK1),
inference(cnf,[status(esa)],[t62_filter_2_negated]) ).
cnf(l3459,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2183,plain,
( ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2)
| ~ v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2)
| ~ m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2)
| ~ m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2)
| sK3 != k1_realset1(u2_lattices(sK1),sK2)
| sK4 != k1_realset1(u1_lattices(sK1),sK2)
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_1(u1_lattices(sK1))
| ~ v1_funct_1(sK3)
| ~ v1_funct_1(sK4)
| ~ r1_lattice2(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK1))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(u1_struct_0(sK1))
| v1_xboole_0(sK2)
| r1_lattice2(sK2,sK3,sK4) ),
inference(instantiation,[status(thm)],[109]) ).
fof(t5_subset,plain,
! [A,B,C] :
~ ( r2_hidden(A,B)
& m1_subset_1(B,k1_zfmisc_1(C))
& v1_xboole_0(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
cnf(110,plain,
( ~ v1_xboole_0(X0)
| ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf,[status(esa)],[t5_subset]) ).
cnf(l2222,plain,
( ~ v1_xboole_0(u1_struct_0(sK1))
| ~ r2_hidden(sK10(sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[110]) ).
cnf(l2322,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2186,plain,
v1_funct_1(sK4),
inference(instantiation,[status(thm)],[8]) ).
cnf(l3498,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3189,plain,
sK4 = k1_realset1(u1_lattices(sK1),sK2),
inference(instantiation,[status(thm)],[12]) ).
cnf(16,plain,
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| v4_lattices(X0) ),
inference(cnf,[status(esa)],[cc1_lattices]) ).
cnf(l2295,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v4_lattices(sK1) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2506,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2307,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3358,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2529,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2337,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3469,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3394,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2240,plain,
( ~ l1_lattices(sK1)
| v1_funct_1(u1_lattices(sK1)) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l2193,plain,
sK3 = k1_realset1(u2_lattices(sK1),sK2),
inference(instantiation,[status(thm)],[11]) ).
cnf(l2187,plain,
v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[6]) ).
cnf(l2749,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2210,plain,
sK4 = k1_realset1(u1_lattices(sK1),sK2),
inference(instantiation,[status(thm)],[12]) ).
cnf(73,plain,
( ~ l1_lattices(X0)
| ~ v7_lattices(X0)
| v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc5_lattice2]) ).
cnf(l2252,plain,
( ~ l1_lattices(sK1)
| ~ v7_lattices(sK1)
| v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[73]) ).
cnf(l2324,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2246,plain,
v1_funct_1(sK3),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2599,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3422,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3405,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2621,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3639,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2320,plain,
( ~ l1_lattices(sK1)
| m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2217,plain,
sK3 = k1_realset1(u2_lattices(sK1),sK2),
inference(instantiation,[status(thm)],[11]) ).
cnf(l2545,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(19,plain,
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| v7_lattices(X0) ),
inference(cnf,[status(esa)],[cc1_lattices]) ).
cnf(l3214,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v7_lattices(sK1) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l2313,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2652,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2908,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2655,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l1,plain,
( ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2)
| ~ m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2)
| sK3 != k1_realset1(u2_lattices(sK1),sK2)
| ~ v1_binop_1(u2_lattices(sK1),u1_struct_0(sK1))
| ~ v1_funct_1(u2_lattices(sK1))
| ~ v1_funct_1(sK3)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_binop_1(sK3,sK2)
| v1_xboole_0(u1_struct_0(sK1))
| v1_xboole_0(sK2) ),
inference(instantiation,[status(thm)],[99]) ).
cnf(l2495,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3740,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2524,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2947,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l38,plain,
v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1070,plain,
( ~ v1_xboole_0(u1_struct_0(sK1))
| ~ r2_hidden(sK10(sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[110]) ).
cnf(l2608,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2213,plain,
( ~ l1_lattices(sK1)
| m2_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2775,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3,plain,
( ~ l2_lattices(sK1)
| m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(59,plain,
( ~ l2_lattices(X0)
| ~ v5_lattices(X0)
| v3_struct_0(X0)
| v1_funct_1(u2_lattices(X0)) ),
inference(cnf,[status(esa)],[fc3_lattice2]) ).
cnf(l795,plain,
( ~ l2_lattices(sK1)
| ~ v5_lattices(sK1)
| v3_struct_0(sK1)
| v1_funct_1(u2_lattices(sK1)) ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l2949,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2202,plain,
v1_funct_2(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[6]) ).
fof(t2_subset,plain,
! [A,B] :
( m1_subset_1(A,B)
=> ( v1_xboole_0(B)
| r2_hidden(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
cnf(103,plain,
( ~ m1_subset_1(X0,X1)
| v1_xboole_0(X1)
| r2_hidden(X0,X1) ),
inference(cnf,[status(esa)],[t2_subset]) ).
cnf(l1071,plain,
( ~ m1_subset_1(sK10(sK2),sK2)
| v1_xboole_0(sK2)
| r2_hidden(sK10(sK2),sK2) ),
inference(instantiation,[status(thm)],[103]) ).
cnf(l1121,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2211,plain,
m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[7]) ).
cnf(l798,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2323,plain,
( ~ m1_subset_1(sK10(sK2),sK2)
| v1_xboole_0(sK2)
| r2_hidden(sK10(sK2),sK2) ),
inference(instantiation,[status(thm)],[103]) ).
cnf(l2208,plain,
sK4 = k1_realset1(u1_lattices(sK1),sK2),
inference(instantiation,[status(thm)],[12]) ).
cnf(l2247,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3211,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2424,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3424,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l797,plain,
v1_funct_1(sK3),
inference(instantiation,[status(thm)],[5]) ).
cnf(l3217,plain,
( ~ v1_xboole_0(u1_struct_0(sK1))
| ~ r2_hidden(sK10(sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[110]) ).
cnf(l3457,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2229,plain,
( ~ l2_lattices(sK1)
| m2_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[38]) ).
fof(existence_m1_subset_1,plain,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
cnf(44,plain,
m1_subset_1(sK10(X0),X0),
inference(cnf,[status(esa)],[existence_m1_subset_1]) ).
cnf(l1144,plain,
m1_subset_1(sK10(sK2),sK2),
inference(instantiation,[status(thm)],[44]) ).
cnf(l3458,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1032,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1048,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3407,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2253,plain,
v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[9]) ).
cnf(l1067,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3901,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3225,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v7_lattices(sK1) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3460,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2268,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2751,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(37,plain,
( ~ l2_lattices(X0)
| v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)) ),
inference(cnf,[status(esa)],[dt_u2_lattices]) ).
cnf(l2206,plain,
( ~ l2_lattices(sK1)
| v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1902,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l134,plain,
m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[7]) ).
cnf(l2309,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1109,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2236,plain,
m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(l2228,plain,
v1_funct_1(sK3),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2296,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2509,plain,
m1_subset_1(sK10(sK2),sK2),
inference(instantiation,[status(thm)],[44]) ).
cnf(l2793,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3359,plain,
( ~ v1_xboole_0(u1_struct_0(sK1))
| ~ r2_hidden(sK10(sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[110]) ).
cnf(l1069,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l494,plain,
sK3 = k1_realset1(u2_lattices(sK1),sK2),
inference(instantiation,[status(thm)],[11]) ).
cnf(l4025,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(54,plain,
( ~ l2_lattices(X0)
| ~ v4_lattices(X0)
| v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc2_lattice2]) ).
cnf(l796,plain,
( ~ l2_lattices(sK1)
| ~ v4_lattices(sK1)
| v1_binop_1(u2_lattices(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l2513,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
fof(t40_lattice2,plain,
! [A] :
( ( ~ v3_struct_0(A)
& v10_lattices(A)
& l3_lattices(A) )
=> r1_lattice2(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t40_lattice2) ).
cnf(106,plain,
( ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
inference(cnf,[status(esa)],[t40_lattice2]) ).
cnf(l2194,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| r1_lattice2(u1_struct_0(sK1),u2_lattices(sK1),u1_lattices(sK1)) ),
inference(instantiation,[status(thm)],[106]) ).
cnf(l3423,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2675,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(68,plain,
( ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc4_lattice2]) ).
cnf(l3205,plain,
( ~ l1_lattices(sK1)
| ~ v6_lattices(sK1)
| v1_binop_1(u1_lattices(sK1),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[68]) ).
cnf(l1578,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2293,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l121,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l3272,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v6_lattices(sK1) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l3218,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l2455,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2218,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l800,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1127,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2367,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3903,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l4391,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3467,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4314,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l4026,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2,plain,
( ~ l2_lattices(sK1)
| ~ v5_lattices(sK1)
| v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[60]) ).
cnf(l3233,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2500,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2275,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2686,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3888,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2241,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l3961,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2230,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l179,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2283,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2661,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(53,plain,
( ~ l2_lattices(X0)
| ~ v4_lattices(X0)
| v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| v3_struct_0(X0) ),
inference(cnf,[status(esa)],[fc2_lattice2]) ).
cnf(l2214,plain,
( ~ l2_lattices(sK1)
| ~ v4_lattices(sK1)
| v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l3488,plain,
( ~ m1_subset_1(sK10(sK2),sK2)
| v1_xboole_0(sK2)
| r2_hidden(sK10(sK2),sK2) ),
inference(instantiation,[status(thm)],[103]) ).
cnf(l2290,plain,
( ~ l2_lattices(sK1)
| ~ v5_lattices(sK1)
| v3_struct_0(sK1)
| v1_funct_1(u2_lattices(sK1)) ),
inference(instantiation,[status(thm)],[59]) ).
cnf(l2260,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l144,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v5_lattices(sK1) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1106,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2286,plain,
( ~ v1_xboole_0(u1_struct_0(sK1))
| ~ r2_hidden(sK10(sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[110]) ).
cnf(l3489,plain,
m1_subset_1(sK10(sK2),sK2),
inference(instantiation,[status(thm)],[44]) ).
cnf(l2483,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l805,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2226,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l3695,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3190,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l2263,plain,
m2_relset_1(sK3,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[7]) ).
cnf(l3904,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2606,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l2270,plain,
m2_relset_1(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[10]) ).
cnf(l2314,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l5,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l2445,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2716,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2551,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3133,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2285,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l804,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v5_lattices(sK1) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l126,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2805,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3079,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2343,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1215,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l2238,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2585,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2258,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3299,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l1096,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3520,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2932,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2380,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2340,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v7_lattices(sK1) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l3053,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l3870,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1135,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3696,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l811,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l810,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l165,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l4324,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2243,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2594,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2474,plain,
( ~ m1_subset_1(sK10(sK2),sK2)
| v1_xboole_0(sK2)
| r2_hidden(sK10(sK2),sK2) ),
inference(instantiation,[status(thm)],[103]) ).
cnf(l2350,plain,
( ~ l3_lattices(sK1)
| l2_lattices(sK1) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l14,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3712,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2542,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3483,plain,
m1_subset_1(sK10(sK2),sK2),
inference(instantiation,[status(thm)],[44]) ).
cnf(l3154,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l4675,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l4231,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1149,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2225,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l4253,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2356,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2273,plain,
( ~ v1_xboole_0(u1_struct_0(sK1))
| ~ r2_hidden(sK10(sK2),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[110]) ).
cnf(l2300,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ m2_lattice4(sK2,sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l808,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v4_lattices(sK1) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2576,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2460,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l812,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2188,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3718,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3420,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3163,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2393,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2449,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2378,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2567,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l155,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3101,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3859,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3356,plain,
( ~ l3_lattices(sK1)
| l1_lattices(sK1) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l2899,plain,
m2_lattice4(sK2,sK1),
inference(instantiation,[status(thm)],[4]) ).
cnf(l2197,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l3962,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3737,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l806,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2348,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v5_lattices(sK1) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l3476,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l3058,plain,
( ~ m1_subset_1(sK10(sK2),sK2)
| v1_xboole_0(sK2)
| r2_hidden(sK10(sK2),sK2) ),
inference(instantiation,[status(thm)],[103]) ).
cnf(l2185,plain,
v1_funct_2(sK4,k2_zfmisc_1(sK2,sK2),sK2),
inference(instantiation,[status(thm)],[9]) ).
cnf(l814,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3282,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v6_lattices(sK1) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l195,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2526,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2900,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3059,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(l809,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3834,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2361,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2362,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l3093,plain,
m1_subset_1(sK10(sK2),sK2),
inference(instantiation,[status(thm)],[44]) ).
cnf(l3505,plain,
( ~ m1_subset_1(sK10(sK2),sK2)
| v1_xboole_0(sK2)
| r2_hidden(sK10(sK2),sK2) ),
inference(instantiation,[status(thm)],[103]) ).
cnf(l3531,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2332,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3526,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l3626,plain,
m1_subset_1(sK10(sK2),sK2),
inference(instantiation,[status(thm)],[44]) ).
cnf(l3724,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2427,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2239,plain,
( ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| v4_lattices(sK1) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l2248,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2432,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l2580,plain,
v10_lattices(sK1),
inference(instantiation,[status(thm)],[1]) ).
cnf(l2579,plain,
l3_lattices(sK1),
inference(instantiation,[status(thm)],[2]) ).
cnf(l827,plain,
~ v3_struct_0(sK1),
inference(instantiation,[status(thm)],[0]) ).
cnf(l4350,plain,
~ v1_xboole_0(sK2),
inference(instantiation,[status(thm)],[3]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l2189,l2199,l3207,l2212,l2520,l2327,l2308,l2272,l3204,l2381,l2201,l2473,l2209,l2203,l2587,l2262,l2227,l2221,l2234,l2265,l2564,l2184,l2237,l3228,l3202,l2490,l2277,l2477,l3210,l2518,l2481,l2521,l3206,l2266,l2231,l3219,l3203,l2271,l3201,l2220,l3238,l2592,l2491,l3884,l2615,l3221,l2264,l3298,l2276,l2617,l2341,l3387,l2289,l2475,l3239,l2280,l3044,l3979,l2251,l2216,l3473,l2748,l3213,l3459,l2183,l2222,l2322,l2186,l3498,l3189,l2295,l2506,l2307,l3358,l2529,l2337,l3469,l3394,l2240,l2193,l2187,l2749,l2210,l2252,l2324,l2246,l2599,l3422,l3405,l2621,l3639,l2320,l2217,l2545,l3214,l2313,l2652,l2908,l2655,l1,l2495,l3740,l2524,l2947,l38,l1070,l2608,l2213,l2775,l3,l795,l2949,l2202,l1071,l1121,l2211,l798,l2323,l2208,l2247,l3211,l2424,l3424,l797,l3217,l3457,l2229,l1144,l3458,l1032,l1048,l3407,l2253,l1067,l3901,l3225,l3460,l2268,l2751,l2206,l1902,l134,l2309,l1109,l2236,l2228,l2296,l2509,l2793,l3359,l1069,l494,l4025,l796,l2513,l2194,l3423,l2675,l3205,l1578,l2293,l121,l3272,l3218,l2455,l2218,l800,l1127,l2367,l3903,l4391,l3467,l4314,l4026,l2,l3233,l2500,l2275,l2686,l3888,l2241,l3961,l2230,l179,l2283,l2661,l2214,l3488,l2290,l2260,l144,l1106,l2286,l3489,l2483,l805,l2226,l3695,l3190,l2263,l3904,l2606,l2270,l2314,l5,l2445,l2716,l2551,l3133,l2285,l804,l126,l2805,l3079,l2343,l1215,l2238,l2585,l2258,l3299,l1096,l3520,l2932,l2380,l2340,l3053,l3870,l1135,l3696,l811,l810,l165,l4324,l2243,l2594,l2474,l2350,l14,l3712,l2542,l3483,l3154,l4675,l4231,l1149,l2225,l4253,l2356,l2273,l2300,l808,l2576,l2460,l812,l2188,l3718,l3420,l3163,l2393,l2449,l2378,l2567,l155,l3101,l3859,l3356,l2899,l2197,l3962,l3737,l806,l2348,l3476,l3058,l2185,l814,l3282,l195,l2526,l2900,l3059,l809,l3834,l2361,l2362,l3093,l3505,l3531,l2332,l3526,l3626,l3724,l2427,l2239,l2248,l2432,l2580,l2579,l827,l4350]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : LAT326+1 : TPTP v9.0.0. Released v3.4.0.
% 0.03/0.11 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.32 % Computer : n027.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Mon Jul 21 00:41:49 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.11/0.32 % launching worker at depth: 1
% 0.11/0.32 % launching worker at depth: 2
% 0.11/0.32 % launching worker at depth: 3
% 0.11/0.32 % launching worker at depth: 4
% 0.11/0.32 % launching worker at depth: 7
% 0.11/0.32 % launching worker at depth: 5
% 0.11/0.32 % launching worker at depth: 6
% 0.11/0.32 % launching worker at depth: 8
% 0.11/0.33 % launching worker at depth: 9
% 0.17/0.36 % launching worker at depth: 10
% 2.05/0.63 % launching worker at depth: 11
% 247.11/31.38 % SZS status Theorem for theBenchmark
% 247.11/31.38 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------