%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT326+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art01.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 10:56:06 EST 2010
% Result : Theorem 3.65s
% Output : Solution 3.65s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP30659/LAT326+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP30659/LAT326+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP30659/LAT326+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 30755
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.93 CPU 2.03 WC
% # Preprocessing time : 0.022 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(10, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>r1_lattice2(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))),file('/tmp/SRASS.s.p', t40_lattice2)).
% fof(11, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>r1_lattice2(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1))),file('/tmp/SRASS.s.p', t41_lattice2)).
% fof(12, axiom,![X1]:(~(v1_xboole_0(X1))=>![X2]:((~(v1_xboole_0(X2))&m1_subset_1(X2,k1_zfmisc_1(X1)))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1))&m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1))=>![X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1))&m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1))=>![X5]:(((v1_funct_1(X5)&v1_funct_2(X5,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X5,k2_zfmisc_1(X2,X2),X2))=>![X6]:(((v1_funct_1(X6)&v1_funct_2(X6,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X6,k2_zfmisc_1(X2,X2),X2))=>(((X5=k1_realset1(X3,X2)&X6=k1_realset1(X4,X2))&r1_lattice2(X1,X3,X4))=>r1_lattice2(X2,X5,X6)))))))),file('/tmp/SRASS.s.p', t5_filter_2)).
% fof(13, axiom,![X1]:(~(v1_xboole_0(X1))=>![X2]:((~(v1_xboole_0(X2))&m1_subset_1(X2,k1_zfmisc_1(X1)))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1))&m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1))=>![X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))=>(X4=k1_realset1(X3,X2)=>(((v1_binop_1(X3,X1)=>v1_binop_1(X4,X2))&(v3_binop_1(X3,X1)=>v3_binop_1(X4,X2)))&(v2_binop_1(X3,X1)=>v2_binop_1(X4,X2)))))))),file('/tmp/SRASS.s.p', t1_filter_2)).
% fof(14, axiom,![X1]:(l1_lattices(X1)=>((v1_funct_1(u1_lattices(X1))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),file('/tmp/SRASS.s.p', dt_u1_lattices)).
% fof(15, axiom,![X1]:(l2_lattices(X1)=>((v1_funct_1(u2_lattices(X1))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),file('/tmp/SRASS.s.p', dt_u2_lattices)).
% fof(20, axiom,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m2_lattice4(X2,X1)=>m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))))),file('/tmp/SRASS.s.p', dt_m2_lattice4)).
% fof(22, axiom,![X1]:(((~(v3_struct_0(X1))&v4_lattices(X1))&l2_lattices(X1))=>((((v1_relat_1(u2_lattices(X1))&v1_funct_1(u2_lattices(X1)))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v1_binop_1(u2_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),file('/tmp/SRASS.s.p', fc2_lattice2)).
% fof(23, axiom,![X1]:(((~(v3_struct_0(X1))&v5_lattices(X1))&l2_lattices(X1))=>((((v1_relat_1(u2_lattices(X1))&v1_funct_1(u2_lattices(X1)))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v2_binop_1(u2_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),file('/tmp/SRASS.s.p', fc3_lattice2)).
% fof(24, axiom,![X1]:(((~(v3_struct_0(X1))&v6_lattices(X1))&l1_lattices(X1))=>((((v1_relat_1(u1_lattices(X1))&v1_funct_1(u1_lattices(X1)))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v1_binop_1(u1_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),file('/tmp/SRASS.s.p', fc4_lattice2)).
% fof(25, axiom,![X1]:(((~(v3_struct_0(X1))&v7_lattices(X1))&l1_lattices(X1))=>((((v1_relat_1(u1_lattices(X1))&v1_funct_1(u1_lattices(X1)))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v2_binop_1(u1_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),file('/tmp/SRASS.s.p', fc5_lattice2)).
% fof(39, axiom,![X1]:((~(v3_struct_0(X1))&l1_struct_0(X1))=>~(v1_xboole_0(u1_struct_0(X1)))),file('/tmp/SRASS.s.p', fc1_struct_0)).
% fof(49, axiom,![X1]:(l3_lattices(X1)=>(l1_lattices(X1)&l2_lattices(X1))),file('/tmp/SRASS.s.p', dt_l3_lattices)).
% fof(51, axiom,![X1]:(l3_lattices(X1)=>((~(v3_struct_0(X1))&v10_lattices(X1))=>((((((~(v3_struct_0(X1))&v4_lattices(X1))&v5_lattices(X1))&v6_lattices(X1))&v7_lattices(X1))&v8_lattices(X1))&v9_lattices(X1)))),file('/tmp/SRASS.s.p', cc1_lattices)).
% fof(57, axiom,![X1]:(l1_lattices(X1)=>l1_struct_0(X1)),file('/tmp/SRASS.s.p', dt_l1_lattices)).
% fof(67, conjecture,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:((~(v1_xboole_0(X2))&m2_lattice4(X2,X1))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2))=>![X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))=>((X3=k1_realset1(u2_lattices(X1),X2)&X4=k1_realset1(u1_lattices(X1),X2))=>(((((v1_binop_1(X3,X2)&v2_binop_1(X3,X2))&v1_binop_1(X4,X2))&v2_binop_1(X4,X2))&r1_lattice2(X2,X3,X4))&r1_lattice2(X2,X4,X3))))))),file('/tmp/SRASS.s.p', t62_filter_2)).
% fof(68, negated_conjecture,~(![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:((~(v1_xboole_0(X2))&m2_lattice4(X2,X1))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2))=>![X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))=>((X3=k1_realset1(u2_lattices(X1),X2)&X4=k1_realset1(u1_lattices(X1),X2))=>(((((v1_binop_1(X3,X2)&v2_binop_1(X3,X2))&v1_binop_1(X4,X2))&v2_binop_1(X4,X2))&r1_lattice2(X2,X3,X4))&r1_lattice2(X2,X4,X3)))))))),inference(assume_negation,[status(cth)],[67])).
% fof(73, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>r1_lattice2(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))),inference(fof_simplification,[status(thm)],[10,theory(equality)])).
% fof(74, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>r1_lattice2(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1))),inference(fof_simplification,[status(thm)],[11,theory(equality)])).
% fof(75, plain,![X1]:(~(v1_xboole_0(X1))=>![X2]:((~(v1_xboole_0(X2))&m1_subset_1(X2,k1_zfmisc_1(X1)))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1))&m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1))=>![X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1))&m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1))=>![X5]:(((v1_funct_1(X5)&v1_funct_2(X5,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X5,k2_zfmisc_1(X2,X2),X2))=>![X6]:(((v1_funct_1(X6)&v1_funct_2(X6,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X6,k2_zfmisc_1(X2,X2),X2))=>(((X5=k1_realset1(X3,X2)&X6=k1_realset1(X4,X2))&r1_lattice2(X1,X3,X4))=>r1_lattice2(X2,X5,X6)))))))),inference(fof_simplification,[status(thm)],[12,theory(equality)])).
% fof(76, plain,![X1]:(~(v1_xboole_0(X1))=>![X2]:((~(v1_xboole_0(X2))&m1_subset_1(X2,k1_zfmisc_1(X1)))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1))&m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1))=>![X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))=>(X4=k1_realset1(X3,X2)=>(((v1_binop_1(X3,X1)=>v1_binop_1(X4,X2))&(v3_binop_1(X3,X1)=>v3_binop_1(X4,X2)))&(v2_binop_1(X3,X1)=>v2_binop_1(X4,X2)))))))),inference(fof_simplification,[status(thm)],[13,theory(equality)])).
% fof(77, plain,![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:(m2_lattice4(X2,X1)=>m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))))),inference(fof_simplification,[status(thm)],[20,theory(equality)])).
% fof(78, plain,![X1]:(((~(v3_struct_0(X1))&v4_lattices(X1))&l2_lattices(X1))=>((((v1_relat_1(u2_lattices(X1))&v1_funct_1(u2_lattices(X1)))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v1_binop_1(u2_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_simplification,[status(thm)],[22,theory(equality)])).
% fof(79, plain,![X1]:(((~(v3_struct_0(X1))&v5_lattices(X1))&l2_lattices(X1))=>((((v1_relat_1(u2_lattices(X1))&v1_funct_1(u2_lattices(X1)))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v2_binop_1(u2_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_simplification,[status(thm)],[23,theory(equality)])).
% fof(80, plain,![X1]:(((~(v3_struct_0(X1))&v6_lattices(X1))&l1_lattices(X1))=>((((v1_relat_1(u1_lattices(X1))&v1_funct_1(u1_lattices(X1)))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v1_binop_1(u1_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_simplification,[status(thm)],[24,theory(equality)])).
% fof(81, plain,![X1]:(((~(v3_struct_0(X1))&v7_lattices(X1))&l1_lattices(X1))=>((((v1_relat_1(u1_lattices(X1))&v1_funct_1(u1_lattices(X1)))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v2_binop_1(u1_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_simplification,[status(thm)],[25,theory(equality)])).
% fof(84, plain,![X1]:((~(v3_struct_0(X1))&l1_struct_0(X1))=>~(v1_xboole_0(u1_struct_0(X1)))),inference(fof_simplification,[status(thm)],[39,theory(equality)])).
% fof(88, plain,![X1]:(l3_lattices(X1)=>((~(v3_struct_0(X1))&v10_lattices(X1))=>((((((~(v3_struct_0(X1))&v4_lattices(X1))&v5_lattices(X1))&v6_lattices(X1))&v7_lattices(X1))&v8_lattices(X1))&v9_lattices(X1)))),inference(fof_simplification,[status(thm)],[51,theory(equality)])).
% fof(90, negated_conjecture,~(![X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))=>![X2]:((~(v1_xboole_0(X2))&m2_lattice4(X2,X1))=>![X3]:(((v1_funct_1(X3)&v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2))=>![X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))=>((X3=k1_realset1(u2_lattices(X1),X2)&X4=k1_realset1(u1_lattices(X1),X2))=>(((((v1_binop_1(X3,X2)&v2_binop_1(X3,X2))&v1_binop_1(X4,X2))&v2_binop_1(X4,X2))&r1_lattice2(X2,X3,X4))&r1_lattice2(X2,X4,X3)))))))),inference(fof_simplification,[status(thm)],[68,theory(equality)])).
% fof(122, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|r1_lattice2(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))),inference(fof_nnf,[status(thm)],[73])).
% fof(123, plain,![X2]:(((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2)))|r1_lattice2(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2))),inference(variable_rename,[status(thm)],[122])).
% cnf(124,plain,(r1_lattice2(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[123])).
% fof(125, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|r1_lattice2(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1))),inference(fof_nnf,[status(thm)],[74])).
% fof(126, plain,![X2]:(((v3_struct_0(X2)|~(v10_lattices(X2)))|~(l3_lattices(X2)))|r1_lattice2(u1_struct_0(X2),u1_lattices(X2),u2_lattices(X2))),inference(variable_rename,[status(thm)],[125])).
% cnf(127,plain,(r1_lattice2(u1_struct_0(X1),u1_lattices(X1),u2_lattices(X1))|v3_struct_0(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[126])).
% fof(128, plain,![X1]:(v1_xboole_0(X1)|![X2]:((v1_xboole_0(X2)|~(m1_subset_1(X2,k1_zfmisc_1(X1))))|![X3]:(((~(v1_funct_1(X3))|~(v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)))|~(m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)))|![X4]:(((~(v1_funct_1(X4))|~(v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)))|~(m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)))|![X5]:(((~(v1_funct_1(X5))|~(v1_funct_2(X5,k2_zfmisc_1(X2,X2),X2)))|~(m2_relset_1(X5,k2_zfmisc_1(X2,X2),X2)))|![X6]:(((~(v1_funct_1(X6))|~(v1_funct_2(X6,k2_zfmisc_1(X2,X2),X2)))|~(m2_relset_1(X6,k2_zfmisc_1(X2,X2),X2)))|(((~(X5=k1_realset1(X3,X2))|~(X6=k1_realset1(X4,X2)))|~(r1_lattice2(X1,X3,X4)))|r1_lattice2(X2,X5,X6)))))))),inference(fof_nnf,[status(thm)],[75])).
% fof(129, plain,![X7]:(v1_xboole_0(X7)|![X8]:((v1_xboole_0(X8)|~(m1_subset_1(X8,k1_zfmisc_1(X7))))|![X9]:(((~(v1_funct_1(X9))|~(v1_funct_2(X9,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X9,k2_zfmisc_1(X7,X7),X7)))|![X10]:(((~(v1_funct_1(X10))|~(v1_funct_2(X10,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X10,k2_zfmisc_1(X7,X7),X7)))|![X11]:(((~(v1_funct_1(X11))|~(v1_funct_2(X11,k2_zfmisc_1(X8,X8),X8)))|~(m2_relset_1(X11,k2_zfmisc_1(X8,X8),X8)))|![X12]:(((~(v1_funct_1(X12))|~(v1_funct_2(X12,k2_zfmisc_1(X8,X8),X8)))|~(m2_relset_1(X12,k2_zfmisc_1(X8,X8),X8)))|(((~(X11=k1_realset1(X9,X8))|~(X12=k1_realset1(X10,X8)))|~(r1_lattice2(X7,X9,X10)))|r1_lattice2(X8,X11,X12)))))))),inference(variable_rename,[status(thm)],[128])).
% fof(130, plain,![X7]:![X8]:![X9]:![X10]:![X11]:![X12]:((((((((~(v1_funct_1(X12))|~(v1_funct_2(X12,k2_zfmisc_1(X8,X8),X8)))|~(m2_relset_1(X12,k2_zfmisc_1(X8,X8),X8)))|(((~(X11=k1_realset1(X9,X8))|~(X12=k1_realset1(X10,X8)))|~(r1_lattice2(X7,X9,X10)))|r1_lattice2(X8,X11,X12)))|((~(v1_funct_1(X11))|~(v1_funct_2(X11,k2_zfmisc_1(X8,X8),X8)))|~(m2_relset_1(X11,k2_zfmisc_1(X8,X8),X8))))|((~(v1_funct_1(X10))|~(v1_funct_2(X10,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X10,k2_zfmisc_1(X7,X7),X7))))|((~(v1_funct_1(X9))|~(v1_funct_2(X9,k2_zfmisc_1(X7,X7),X7)))|~(m2_relset_1(X9,k2_zfmisc_1(X7,X7),X7))))|(v1_xboole_0(X8)|~(m1_subset_1(X8,k1_zfmisc_1(X7)))))|v1_xboole_0(X7)),inference(shift_quantors,[status(thm)],[129])).
% cnf(131,plain,(v1_xboole_0(X1)|v1_xboole_0(X2)|r1_lattice2(X2,X5,X6)|~m1_subset_1(X2,k1_zfmisc_1(X1))|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X3)|~m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X4)|~m2_relset_1(X5,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X5,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(X5)|~r1_lattice2(X1,X3,X4)|X6!=k1_realset1(X4,X2)|X5!=k1_realset1(X3,X2)|~m2_relset_1(X6,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X6,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(X6)),inference(split_conjunct,[status(thm)],[130])).
% fof(132, plain,![X1]:(v1_xboole_0(X1)|![X2]:((v1_xboole_0(X2)|~(m1_subset_1(X2,k1_zfmisc_1(X1))))|![X3]:(((~(v1_funct_1(X3))|~(v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)))|~(m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)))|![X4]:(((~(v1_funct_1(X4))|~(v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)))|~(m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)))|(~(X4=k1_realset1(X3,X2))|(((~(v1_binop_1(X3,X1))|v1_binop_1(X4,X2))&(~(v3_binop_1(X3,X1))|v3_binop_1(X4,X2)))&(~(v2_binop_1(X3,X1))|v2_binop_1(X4,X2)))))))),inference(fof_nnf,[status(thm)],[76])).
% fof(133, plain,![X5]:(v1_xboole_0(X5)|![X6]:((v1_xboole_0(X6)|~(m1_subset_1(X6,k1_zfmisc_1(X5))))|![X7]:(((~(v1_funct_1(X7))|~(v1_funct_2(X7,k2_zfmisc_1(X5,X5),X5)))|~(m2_relset_1(X7,k2_zfmisc_1(X5,X5),X5)))|![X8]:(((~(v1_funct_1(X8))|~(v1_funct_2(X8,k2_zfmisc_1(X6,X6),X6)))|~(m2_relset_1(X8,k2_zfmisc_1(X6,X6),X6)))|(~(X8=k1_realset1(X7,X6))|(((~(v1_binop_1(X7,X5))|v1_binop_1(X8,X6))&(~(v3_binop_1(X7,X5))|v3_binop_1(X8,X6)))&(~(v2_binop_1(X7,X5))|v2_binop_1(X8,X6)))))))),inference(variable_rename,[status(thm)],[132])).
% fof(134, plain,![X5]:![X6]:![X7]:![X8]:((((((~(v1_funct_1(X8))|~(v1_funct_2(X8,k2_zfmisc_1(X6,X6),X6)))|~(m2_relset_1(X8,k2_zfmisc_1(X6,X6),X6)))|(~(X8=k1_realset1(X7,X6))|(((~(v1_binop_1(X7,X5))|v1_binop_1(X8,X6))&(~(v3_binop_1(X7,X5))|v3_binop_1(X8,X6)))&(~(v2_binop_1(X7,X5))|v2_binop_1(X8,X6)))))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,k2_zfmisc_1(X5,X5),X5)))|~(m2_relset_1(X7,k2_zfmisc_1(X5,X5),X5))))|(v1_xboole_0(X6)|~(m1_subset_1(X6,k1_zfmisc_1(X5)))))|v1_xboole_0(X5)),inference(shift_quantors,[status(thm)],[133])).
% fof(135, plain,![X5]:![X6]:![X7]:![X8]:((((((((~(v1_binop_1(X7,X5))|v1_binop_1(X8,X6))|~(X8=k1_realset1(X7,X6)))|((~(v1_funct_1(X8))|~(v1_funct_2(X8,k2_zfmisc_1(X6,X6),X6)))|~(m2_relset_1(X8,k2_zfmisc_1(X6,X6),X6))))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,k2_zfmisc_1(X5,X5),X5)))|~(m2_relset_1(X7,k2_zfmisc_1(X5,X5),X5))))|(v1_xboole_0(X6)|~(m1_subset_1(X6,k1_zfmisc_1(X5)))))|v1_xboole_0(X5))&((((((~(v3_binop_1(X7,X5))|v3_binop_1(X8,X6))|~(X8=k1_realset1(X7,X6)))|((~(v1_funct_1(X8))|~(v1_funct_2(X8,k2_zfmisc_1(X6,X6),X6)))|~(m2_relset_1(X8,k2_zfmisc_1(X6,X6),X6))))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,k2_zfmisc_1(X5,X5),X5)))|~(m2_relset_1(X7,k2_zfmisc_1(X5,X5),X5))))|(v1_xboole_0(X6)|~(m1_subset_1(X6,k1_zfmisc_1(X5)))))|v1_xboole_0(X5)))&((((((~(v2_binop_1(X7,X5))|v2_binop_1(X8,X6))|~(X8=k1_realset1(X7,X6)))|((~(v1_funct_1(X8))|~(v1_funct_2(X8,k2_zfmisc_1(X6,X6),X6)))|~(m2_relset_1(X8,k2_zfmisc_1(X6,X6),X6))))|((~(v1_funct_1(X7))|~(v1_funct_2(X7,k2_zfmisc_1(X5,X5),X5)))|~(m2_relset_1(X7,k2_zfmisc_1(X5,X5),X5))))|(v1_xboole_0(X6)|~(m1_subset_1(X6,k1_zfmisc_1(X5)))))|v1_xboole_0(X5))),inference(distribute,[status(thm)],[134])).
% cnf(136,plain,(v1_xboole_0(X1)|v1_xboole_0(X2)|v2_binop_1(X4,X2)|~m1_subset_1(X2,k1_zfmisc_1(X1))|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X3)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(X4)|X4!=k1_realset1(X3,X2)|~v2_binop_1(X3,X1)),inference(split_conjunct,[status(thm)],[135])).
% cnf(138,plain,(v1_xboole_0(X1)|v1_xboole_0(X2)|v1_binop_1(X4,X2)|~m1_subset_1(X2,k1_zfmisc_1(X1))|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X3)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(X4)|X4!=k1_realset1(X3,X2)|~v1_binop_1(X3,X1)),inference(split_conjunct,[status(thm)],[135])).
% fof(139, plain,![X1]:(~(l1_lattices(X1))|((v1_funct_1(u1_lattices(X1))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[14])).
% fof(140, plain,![X2]:(~(l1_lattices(X2))|((v1_funct_1(u1_lattices(X2))&v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))&m2_relset_1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[139])).
% fof(141, plain,![X2]:(((v1_funct_1(u1_lattices(X2))|~(l1_lattices(X2)))&(v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|~(l1_lattices(X2))))&(m2_relset_1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|~(l1_lattices(X2)))),inference(distribute,[status(thm)],[140])).
% cnf(142,plain,(m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))|~l1_lattices(X1)),inference(split_conjunct,[status(thm)],[141])).
% cnf(143,plain,(v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))|~l1_lattices(X1)),inference(split_conjunct,[status(thm)],[141])).
% cnf(144,plain,(v1_funct_1(u1_lattices(X1))|~l1_lattices(X1)),inference(split_conjunct,[status(thm)],[141])).
% fof(145, plain,![X1]:(~(l2_lattices(X1))|((v1_funct_1(u2_lattices(X1))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[15])).
% fof(146, plain,![X2]:(~(l2_lattices(X2))|((v1_funct_1(u2_lattices(X2))&v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))&m2_relset_1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[145])).
% fof(147, plain,![X2]:(((v1_funct_1(u2_lattices(X2))|~(l2_lattices(X2)))&(v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|~(l2_lattices(X2))))&(m2_relset_1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|~(l2_lattices(X2)))),inference(distribute,[status(thm)],[146])).
% cnf(148,plain,(m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))|~l2_lattices(X1)),inference(split_conjunct,[status(thm)],[147])).
% cnf(149,plain,(v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))|~l2_lattices(X1)),inference(split_conjunct,[status(thm)],[147])).
% cnf(150,plain,(v1_funct_1(u2_lattices(X1))|~l2_lattices(X1)),inference(split_conjunct,[status(thm)],[147])).
% fof(168, plain,![X1]:(((v3_struct_0(X1)|~(v10_lattices(X1)))|~(l3_lattices(X1)))|![X2]:(~(m2_lattice4(X2,X1))|m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1))))),inference(fof_nnf,[status(thm)],[77])).
% fof(169, plain,![X3]:(((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))|![X4]:(~(m2_lattice4(X4,X3))|m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3))))),inference(variable_rename,[status(thm)],[168])).
% fof(170, plain,![X3]:![X4]:((~(m2_lattice4(X4,X3))|m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X3))))|((v3_struct_0(X3)|~(v10_lattices(X3)))|~(l3_lattices(X3)))),inference(shift_quantors,[status(thm)],[169])).
% cnf(171,plain,(v3_struct_0(X1)|m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))|~l3_lattices(X1)|~v10_lattices(X1)|~m2_lattice4(X2,X1)),inference(split_conjunct,[status(thm)],[170])).
% fof(175, plain,![X1]:(((v3_struct_0(X1)|~(v4_lattices(X1)))|~(l2_lattices(X1)))|((((v1_relat_1(u2_lattices(X1))&v1_funct_1(u2_lattices(X1)))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v1_binop_1(u2_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[78])).
% fof(176, plain,![X2]:(((v3_struct_0(X2)|~(v4_lattices(X2)))|~(l2_lattices(X2)))|((((v1_relat_1(u2_lattices(X2))&v1_funct_1(u2_lattices(X2)))&v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))&v1_binop_1(u2_lattices(X2),u1_struct_0(X2)))&v1_partfun1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[175])).
% fof(177, plain,![X2]:(((((v1_relat_1(u2_lattices(X2))|((v3_struct_0(X2)|~(v4_lattices(X2)))|~(l2_lattices(X2))))&(v1_funct_1(u2_lattices(X2))|((v3_struct_0(X2)|~(v4_lattices(X2)))|~(l2_lattices(X2)))))&(v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|((v3_struct_0(X2)|~(v4_lattices(X2)))|~(l2_lattices(X2)))))&(v1_binop_1(u2_lattices(X2),u1_struct_0(X2))|((v3_struct_0(X2)|~(v4_lattices(X2)))|~(l2_lattices(X2)))))&(v1_partfun1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|((v3_struct_0(X2)|~(v4_lattices(X2)))|~(l2_lattices(X2))))),inference(distribute,[status(thm)],[176])).
% cnf(179,plain,(v3_struct_0(X1)|v1_binop_1(u2_lattices(X1),u1_struct_0(X1))|~l2_lattices(X1)|~v4_lattices(X1)),inference(split_conjunct,[status(thm)],[177])).
% fof(183, plain,![X1]:(((v3_struct_0(X1)|~(v5_lattices(X1)))|~(l2_lattices(X1)))|((((v1_relat_1(u2_lattices(X1))&v1_funct_1(u2_lattices(X1)))&v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v2_binop_1(u2_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[79])).
% fof(184, plain,![X2]:(((v3_struct_0(X2)|~(v5_lattices(X2)))|~(l2_lattices(X2)))|((((v1_relat_1(u2_lattices(X2))&v1_funct_1(u2_lattices(X2)))&v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))&v2_binop_1(u2_lattices(X2),u1_struct_0(X2)))&v1_partfun1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[183])).
% fof(185, plain,![X2]:(((((v1_relat_1(u2_lattices(X2))|((v3_struct_0(X2)|~(v5_lattices(X2)))|~(l2_lattices(X2))))&(v1_funct_1(u2_lattices(X2))|((v3_struct_0(X2)|~(v5_lattices(X2)))|~(l2_lattices(X2)))))&(v1_funct_2(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|((v3_struct_0(X2)|~(v5_lattices(X2)))|~(l2_lattices(X2)))))&(v2_binop_1(u2_lattices(X2),u1_struct_0(X2))|((v3_struct_0(X2)|~(v5_lattices(X2)))|~(l2_lattices(X2)))))&(v1_partfun1(u2_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|((v3_struct_0(X2)|~(v5_lattices(X2)))|~(l2_lattices(X2))))),inference(distribute,[status(thm)],[184])).
% cnf(187,plain,(v3_struct_0(X1)|v2_binop_1(u2_lattices(X1),u1_struct_0(X1))|~l2_lattices(X1)|~v5_lattices(X1)),inference(split_conjunct,[status(thm)],[185])).
% fof(191, plain,![X1]:(((v3_struct_0(X1)|~(v6_lattices(X1)))|~(l1_lattices(X1)))|((((v1_relat_1(u1_lattices(X1))&v1_funct_1(u1_lattices(X1)))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v1_binop_1(u1_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[80])).
% fof(192, plain,![X2]:(((v3_struct_0(X2)|~(v6_lattices(X2)))|~(l1_lattices(X2)))|((((v1_relat_1(u1_lattices(X2))&v1_funct_1(u1_lattices(X2)))&v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))&v1_binop_1(u1_lattices(X2),u1_struct_0(X2)))&v1_partfun1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[191])).
% fof(193, plain,![X2]:(((((v1_relat_1(u1_lattices(X2))|((v3_struct_0(X2)|~(v6_lattices(X2)))|~(l1_lattices(X2))))&(v1_funct_1(u1_lattices(X2))|((v3_struct_0(X2)|~(v6_lattices(X2)))|~(l1_lattices(X2)))))&(v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|((v3_struct_0(X2)|~(v6_lattices(X2)))|~(l1_lattices(X2)))))&(v1_binop_1(u1_lattices(X2),u1_struct_0(X2))|((v3_struct_0(X2)|~(v6_lattices(X2)))|~(l1_lattices(X2)))))&(v1_partfun1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|((v3_struct_0(X2)|~(v6_lattices(X2)))|~(l1_lattices(X2))))),inference(distribute,[status(thm)],[192])).
% cnf(195,plain,(v3_struct_0(X1)|v1_binop_1(u1_lattices(X1),u1_struct_0(X1))|~l1_lattices(X1)|~v6_lattices(X1)),inference(split_conjunct,[status(thm)],[193])).
% fof(199, plain,![X1]:(((v3_struct_0(X1)|~(v7_lattices(X1)))|~(l1_lattices(X1)))|((((v1_relat_1(u1_lattices(X1))&v1_funct_1(u1_lattices(X1)))&v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))&v2_binop_1(u1_lattices(X1),u1_struct_0(X1)))&v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[81])).
% fof(200, plain,![X2]:(((v3_struct_0(X2)|~(v7_lattices(X2)))|~(l1_lattices(X2)))|((((v1_relat_1(u1_lattices(X2))&v1_funct_1(u1_lattices(X2)))&v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))&v2_binop_1(u1_lattices(X2),u1_struct_0(X2)))&v1_partfun1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[199])).
% fof(201, plain,![X2]:(((((v1_relat_1(u1_lattices(X2))|((v3_struct_0(X2)|~(v7_lattices(X2)))|~(l1_lattices(X2))))&(v1_funct_1(u1_lattices(X2))|((v3_struct_0(X2)|~(v7_lattices(X2)))|~(l1_lattices(X2)))))&(v1_funct_2(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|((v3_struct_0(X2)|~(v7_lattices(X2)))|~(l1_lattices(X2)))))&(v2_binop_1(u1_lattices(X2),u1_struct_0(X2))|((v3_struct_0(X2)|~(v7_lattices(X2)))|~(l1_lattices(X2)))))&(v1_partfun1(u1_lattices(X2),k2_zfmisc_1(u1_struct_0(X2),u1_struct_0(X2)),u1_struct_0(X2))|((v3_struct_0(X2)|~(v7_lattices(X2)))|~(l1_lattices(X2))))),inference(distribute,[status(thm)],[200])).
% cnf(203,plain,(v3_struct_0(X1)|v2_binop_1(u1_lattices(X1),u1_struct_0(X1))|~l1_lattices(X1)|~v7_lattices(X1)),inference(split_conjunct,[status(thm)],[201])).
% fof(254, plain,![X1]:((v3_struct_0(X1)|~(l1_struct_0(X1)))|~(v1_xboole_0(u1_struct_0(X1)))),inference(fof_nnf,[status(thm)],[84])).
% fof(255, plain,![X2]:((v3_struct_0(X2)|~(l1_struct_0(X2)))|~(v1_xboole_0(u1_struct_0(X2)))),inference(variable_rename,[status(thm)],[254])).
% cnf(256,plain,(v3_struct_0(X1)|~v1_xboole_0(u1_struct_0(X1))|~l1_struct_0(X1)),inference(split_conjunct,[status(thm)],[255])).
% fof(285, plain,![X1]:(~(l3_lattices(X1))|(l1_lattices(X1)&l2_lattices(X1))),inference(fof_nnf,[status(thm)],[49])).
% fof(286, plain,![X2]:(~(l3_lattices(X2))|(l1_lattices(X2)&l2_lattices(X2))),inference(variable_rename,[status(thm)],[285])).
% fof(287, plain,![X2]:((l1_lattices(X2)|~(l3_lattices(X2)))&(l2_lattices(X2)|~(l3_lattices(X2)))),inference(distribute,[status(thm)],[286])).
% cnf(288,plain,(l2_lattices(X1)|~l3_lattices(X1)),inference(split_conjunct,[status(thm)],[287])).
% cnf(289,plain,(l1_lattices(X1)|~l3_lattices(X1)),inference(split_conjunct,[status(thm)],[287])).
% fof(293, plain,![X1]:(~(l3_lattices(X1))|((v3_struct_0(X1)|~(v10_lattices(X1)))|((((((~(v3_struct_0(X1))&v4_lattices(X1))&v5_lattices(X1))&v6_lattices(X1))&v7_lattices(X1))&v8_lattices(X1))&v9_lattices(X1)))),inference(fof_nnf,[status(thm)],[88])).
% fof(294, plain,![X2]:(~(l3_lattices(X2))|((v3_struct_0(X2)|~(v10_lattices(X2)))|((((((~(v3_struct_0(X2))&v4_lattices(X2))&v5_lattices(X2))&v6_lattices(X2))&v7_lattices(X2))&v8_lattices(X2))&v9_lattices(X2)))),inference(variable_rename,[status(thm)],[293])).
% fof(295, plain,![X2]:((((((((~(v3_struct_0(X2))|(v3_struct_0(X2)|~(v10_lattices(X2))))|~(l3_lattices(X2)))&((v4_lattices(X2)|(v3_struct_0(X2)|~(v10_lattices(X2))))|~(l3_lattices(X2))))&((v5_lattices(X2)|(v3_struct_0(X2)|~(v10_lattices(X2))))|~(l3_lattices(X2))))&((v6_lattices(X2)|(v3_struct_0(X2)|~(v10_lattices(X2))))|~(l3_lattices(X2))))&((v7_lattices(X2)|(v3_struct_0(X2)|~(v10_lattices(X2))))|~(l3_lattices(X2))))&((v8_lattices(X2)|(v3_struct_0(X2)|~(v10_lattices(X2))))|~(l3_lattices(X2))))&((v9_lattices(X2)|(v3_struct_0(X2)|~(v10_lattices(X2))))|~(l3_lattices(X2)))),inference(distribute,[status(thm)],[294])).
% cnf(298,plain,(v3_struct_0(X1)|v7_lattices(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[295])).
% cnf(299,plain,(v3_struct_0(X1)|v6_lattices(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[295])).
% cnf(300,plain,(v3_struct_0(X1)|v5_lattices(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[295])).
% cnf(301,plain,(v3_struct_0(X1)|v4_lattices(X1)|~l3_lattices(X1)|~v10_lattices(X1)),inference(split_conjunct,[status(thm)],[295])).
% fof(325, plain,![X1]:(~(l1_lattices(X1))|l1_struct_0(X1)),inference(fof_nnf,[status(thm)],[57])).
% fof(326, plain,![X2]:(~(l1_lattices(X2))|l1_struct_0(X2)),inference(variable_rename,[status(thm)],[325])).
% cnf(327,plain,(l1_struct_0(X1)|~l1_lattices(X1)),inference(split_conjunct,[status(thm)],[326])).
% fof(339, negated_conjecture,?[X1]:(((~(v3_struct_0(X1))&v10_lattices(X1))&l3_lattices(X1))&?[X2]:((~(v1_xboole_0(X2))&m2_lattice4(X2,X1))&?[X3]:(((v1_funct_1(X3)&v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2))&?[X4]:(((v1_funct_1(X4)&v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2))&m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2))&((X3=k1_realset1(u2_lattices(X1),X2)&X4=k1_realset1(u1_lattices(X1),X2))&(((((~(v1_binop_1(X3,X2))|~(v2_binop_1(X3,X2)))|~(v1_binop_1(X4,X2)))|~(v2_binop_1(X4,X2)))|~(r1_lattice2(X2,X3,X4)))|~(r1_lattice2(X2,X4,X3)))))))),inference(fof_nnf,[status(thm)],[90])).
% fof(340, negated_conjecture,?[X5]:(((~(v3_struct_0(X5))&v10_lattices(X5))&l3_lattices(X5))&?[X6]:((~(v1_xboole_0(X6))&m2_lattice4(X6,X5))&?[X7]:(((v1_funct_1(X7)&v1_funct_2(X7,k2_zfmisc_1(X6,X6),X6))&m2_relset_1(X7,k2_zfmisc_1(X6,X6),X6))&?[X8]:(((v1_funct_1(X8)&v1_funct_2(X8,k2_zfmisc_1(X6,X6),X6))&m2_relset_1(X8,k2_zfmisc_1(X6,X6),X6))&((X7=k1_realset1(u2_lattices(X5),X6)&X8=k1_realset1(u1_lattices(X5),X6))&(((((~(v1_binop_1(X7,X6))|~(v2_binop_1(X7,X6)))|~(v1_binop_1(X8,X6)))|~(v2_binop_1(X8,X6)))|~(r1_lattice2(X6,X7,X8)))|~(r1_lattice2(X6,X8,X7)))))))),inference(variable_rename,[status(thm)],[339])).
% fof(341, negated_conjecture,(((~(v3_struct_0(esk19_0))&v10_lattices(esk19_0))&l3_lattices(esk19_0))&((~(v1_xboole_0(esk20_0))&m2_lattice4(esk20_0,esk19_0))&(((v1_funct_1(esk21_0)&v1_funct_2(esk21_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0))&m2_relset_1(esk21_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0))&(((v1_funct_1(esk22_0)&v1_funct_2(esk22_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0))&m2_relset_1(esk22_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0))&((esk21_0=k1_realset1(u2_lattices(esk19_0),esk20_0)&esk22_0=k1_realset1(u1_lattices(esk19_0),esk20_0))&(((((~(v1_binop_1(esk21_0,esk20_0))|~(v2_binop_1(esk21_0,esk20_0)))|~(v1_binop_1(esk22_0,esk20_0)))|~(v2_binop_1(esk22_0,esk20_0)))|~(r1_lattice2(esk20_0,esk21_0,esk22_0)))|~(r1_lattice2(esk20_0,esk22_0,esk21_0)))))))),inference(skolemize,[status(esa)],[340])).
% cnf(342,negated_conjecture,(~r1_lattice2(esk20_0,esk22_0,esk21_0)|~r1_lattice2(esk20_0,esk21_0,esk22_0)|~v2_binop_1(esk22_0,esk20_0)|~v1_binop_1(esk22_0,esk20_0)|~v2_binop_1(esk21_0,esk20_0)|~v1_binop_1(esk21_0,esk20_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(343,negated_conjecture,(esk22_0=k1_realset1(u1_lattices(esk19_0),esk20_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(344,negated_conjecture,(esk21_0=k1_realset1(u2_lattices(esk19_0),esk20_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(345,negated_conjecture,(m2_relset_1(esk22_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(346,negated_conjecture,(v1_funct_2(esk22_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(347,negated_conjecture,(v1_funct_1(esk22_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(348,negated_conjecture,(m2_relset_1(esk21_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(349,negated_conjecture,(v1_funct_2(esk21_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(350,negated_conjecture,(v1_funct_1(esk21_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(351,negated_conjecture,(m2_lattice4(esk20_0,esk19_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(352,negated_conjecture,(~v1_xboole_0(esk20_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(353,negated_conjecture,(l3_lattices(esk19_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(354,negated_conjecture,(v10_lattices(esk19_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(355,negated_conjecture,(~v3_struct_0(esk19_0)),inference(split_conjunct,[status(thm)],[341])).
% cnf(360,negated_conjecture,(l1_lattices(esk19_0)),inference(pm,[status(thm)],[289,353,theory(equality)])).
% cnf(362,negated_conjecture,(l2_lattices(esk19_0)),inference(pm,[status(thm)],[288,353,theory(equality)])).
% cnf(399,negated_conjecture,(v4_lattices(esk19_0)|v3_struct_0(esk19_0)|~l3_lattices(esk19_0)),inference(pm,[status(thm)],[301,354,theory(equality)])).
% cnf(400,negated_conjecture,(v4_lattices(esk19_0)|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[399,353,theory(equality)])).
% cnf(401,negated_conjecture,(v4_lattices(esk19_0)|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[400,theory(equality)])).
% cnf(402,negated_conjecture,(v4_lattices(esk19_0)),inference(sr,[status(thm)],[401,355,theory(equality)])).
% cnf(403,negated_conjecture,(v5_lattices(esk19_0)|v3_struct_0(esk19_0)|~l3_lattices(esk19_0)),inference(pm,[status(thm)],[300,354,theory(equality)])).
% cnf(404,negated_conjecture,(v5_lattices(esk19_0)|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[403,353,theory(equality)])).
% cnf(405,negated_conjecture,(v5_lattices(esk19_0)|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[404,theory(equality)])).
% cnf(406,negated_conjecture,(v5_lattices(esk19_0)),inference(sr,[status(thm)],[405,355,theory(equality)])).
% cnf(407,negated_conjecture,(v6_lattices(esk19_0)|v3_struct_0(esk19_0)|~l3_lattices(esk19_0)),inference(pm,[status(thm)],[299,354,theory(equality)])).
% cnf(408,negated_conjecture,(v6_lattices(esk19_0)|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[407,353,theory(equality)])).
% cnf(409,negated_conjecture,(v6_lattices(esk19_0)|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[408,theory(equality)])).
% cnf(410,negated_conjecture,(v6_lattices(esk19_0)),inference(sr,[status(thm)],[409,355,theory(equality)])).
% cnf(411,negated_conjecture,(v7_lattices(esk19_0)|v3_struct_0(esk19_0)|~l3_lattices(esk19_0)),inference(pm,[status(thm)],[298,354,theory(equality)])).
% cnf(412,negated_conjecture,(v7_lattices(esk19_0)|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[411,353,theory(equality)])).
% cnf(413,negated_conjecture,(v7_lattices(esk19_0)|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[412,theory(equality)])).
% cnf(414,negated_conjecture,(v7_lattices(esk19_0)),inference(sr,[status(thm)],[413,355,theory(equality)])).
% cnf(474,negated_conjecture,(m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|v3_struct_0(esk19_0)|~v10_lattices(esk19_0)|~l3_lattices(esk19_0)),inference(pm,[status(thm)],[171,351,theory(equality)])).
% cnf(475,negated_conjecture,(m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|v3_struct_0(esk19_0)|$false|~l3_lattices(esk19_0)),inference(rw,[status(thm)],[474,354,theory(equality)])).
% cnf(476,negated_conjecture,(m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|v3_struct_0(esk19_0)|$false|$false),inference(rw,[status(thm)],[475,353,theory(equality)])).
% cnf(477,negated_conjecture,(m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[476,theory(equality)])).
% cnf(478,negated_conjecture,(m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))),inference(sr,[status(thm)],[477,355,theory(equality)])).
% cnf(479,negated_conjecture,(r1_lattice2(u1_struct_0(esk19_0),u2_lattices(esk19_0),u1_lattices(esk19_0))|v3_struct_0(esk19_0)|~l3_lattices(esk19_0)),inference(pm,[status(thm)],[124,354,theory(equality)])).
% cnf(480,negated_conjecture,(r1_lattice2(u1_struct_0(esk19_0),u2_lattices(esk19_0),u1_lattices(esk19_0))|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[479,353,theory(equality)])).
% cnf(481,negated_conjecture,(r1_lattice2(u1_struct_0(esk19_0),u2_lattices(esk19_0),u1_lattices(esk19_0))|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[480,theory(equality)])).
% cnf(482,negated_conjecture,(r1_lattice2(u1_struct_0(esk19_0),u2_lattices(esk19_0),u1_lattices(esk19_0))),inference(sr,[status(thm)],[481,355,theory(equality)])).
% cnf(485,negated_conjecture,(r1_lattice2(u1_struct_0(esk19_0),u1_lattices(esk19_0),u2_lattices(esk19_0))|v3_struct_0(esk19_0)|~l3_lattices(esk19_0)),inference(pm,[status(thm)],[127,354,theory(equality)])).
% cnf(486,negated_conjecture,(r1_lattice2(u1_struct_0(esk19_0),u1_lattices(esk19_0),u2_lattices(esk19_0))|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[485,353,theory(equality)])).
% cnf(487,negated_conjecture,(r1_lattice2(u1_struct_0(esk19_0),u1_lattices(esk19_0),u2_lattices(esk19_0))|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[486,theory(equality)])).
% cnf(488,negated_conjecture,(r1_lattice2(u1_struct_0(esk19_0),u1_lattices(esk19_0),u2_lattices(esk19_0))),inference(sr,[status(thm)],[487,355,theory(equality)])).
% cnf(491,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(esk22_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk22_0)|~v1_funct_1(X2)),inference(pm,[status(thm)],[138,346,theory(equality)])).
% cnf(492,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(esk21_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk21_0)|~v1_funct_1(X2)),inference(pm,[status(thm)],[138,349,theory(equality)])).
% cnf(493,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk22_0)|~v1_funct_1(X2)),inference(rw,[status(thm)],[491,345,theory(equality)])).
% cnf(494,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|$false|~v1_funct_1(X2)),inference(rw,[status(thm)],[493,347,theory(equality)])).
% cnf(495,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)),inference(cn,[status(thm)],[494,theory(equality)])).
% cnf(496,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)),inference(sr,[status(thm)],[495,352,theory(equality)])).
% cnf(497,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk21_0)|~v1_funct_1(X2)),inference(rw,[status(thm)],[492,348,theory(equality)])).
% cnf(498,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|$false|~v1_funct_1(X2)),inference(rw,[status(thm)],[497,350,theory(equality)])).
% cnf(499,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)),inference(cn,[status(thm)],[498,theory(equality)])).
% cnf(500,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v1_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)),inference(sr,[status(thm)],[499,352,theory(equality)])).
% cnf(511,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(esk22_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk22_0)|~v1_funct_1(X2)),inference(pm,[status(thm)],[136,346,theory(equality)])).
% cnf(512,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(esk21_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk21_0)|~v1_funct_1(X2)),inference(pm,[status(thm)],[136,349,theory(equality)])).
% cnf(513,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk22_0)|~v1_funct_1(X2)),inference(rw,[status(thm)],[511,345,theory(equality)])).
% cnf(514,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|$false|~v1_funct_1(X2)),inference(rw,[status(thm)],[513,347,theory(equality)])).
% cnf(515,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)),inference(cn,[status(thm)],[514,theory(equality)])).
% cnf(516,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)),inference(sr,[status(thm)],[515,352,theory(equality)])).
% cnf(517,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk21_0)|~v1_funct_1(X2)),inference(rw,[status(thm)],[512,348,theory(equality)])).
% cnf(518,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|$false|~v1_funct_1(X2)),inference(rw,[status(thm)],[517,350,theory(equality)])).
% cnf(519,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)),inference(cn,[status(thm)],[518,theory(equality)])).
% cnf(520,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|~v2_binop_1(X2,X1)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)),inference(sr,[status(thm)],[519,352,theory(equality)])).
% cnf(521,negated_conjecture,(r1_lattice2(esk20_0,X1,esk22_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk22_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|~m2_relset_1(esk22_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(esk22_0)|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(pm,[status(thm)],[131,346,theory(equality)])).
% cnf(522,negated_conjecture,(r1_lattice2(esk20_0,X1,esk21_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk21_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|~m2_relset_1(esk21_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(esk21_0)|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(pm,[status(thm)],[131,349,theory(equality)])).
% cnf(523,negated_conjecture,(r1_lattice2(esk20_0,X1,esk22_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk22_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|$false|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(esk22_0)|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(rw,[status(thm)],[521,345,theory(equality)])).
% cnf(524,negated_conjecture,(r1_lattice2(esk20_0,X1,esk22_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk22_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|$false|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|$false|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(rw,[status(thm)],[523,347,theory(equality)])).
% cnf(525,negated_conjecture,(r1_lattice2(esk20_0,X1,esk22_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk22_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(cn,[status(thm)],[524,theory(equality)])).
% cnf(526,negated_conjecture,(r1_lattice2(esk20_0,X1,esk22_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk22_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(sr,[status(thm)],[525,352,theory(equality)])).
% cnf(527,negated_conjecture,(r1_lattice2(esk20_0,X1,esk21_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk21_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|$false|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(esk21_0)|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(rw,[status(thm)],[522,348,theory(equality)])).
% cnf(528,negated_conjecture,(r1_lattice2(esk20_0,X1,esk21_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk21_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|$false|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|$false|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(rw,[status(thm)],[527,350,theory(equality)])).
% cnf(529,negated_conjecture,(r1_lattice2(esk20_0,X1,esk21_0)|v1_xboole_0(esk20_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk21_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(cn,[status(thm)],[528,theory(equality)])).
% cnf(530,negated_conjecture,(r1_lattice2(esk20_0,X1,esk21_0)|v1_xboole_0(X2)|k1_realset1(X3,esk20_0)!=esk21_0|k1_realset1(X4,esk20_0)!=X1|~v1_funct_2(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~v1_funct_2(X3,k2_zfmisc_1(X2,X2),X2)|~v1_funct_2(X4,k2_zfmisc_1(X2,X2),X2)|~m1_subset_1(esk20_0,k1_zfmisc_1(X2))|~r1_lattice2(X2,X4,X3)|~m2_relset_1(X1,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X3,k2_zfmisc_1(X2,X2),X2)|~m2_relset_1(X4,k2_zfmisc_1(X2,X2),X2)|~v1_funct_1(X1)|~v1_funct_1(X3)|~v1_funct_1(X4)),inference(sr,[status(thm)],[529,352,theory(equality)])).
% cnf(531,negated_conjecture,(l1_struct_0(esk19_0)),inference(pm,[status(thm)],[327,360,theory(equality)])).
% cnf(532,negated_conjecture,(v1_funct_1(u1_lattices(esk19_0))),inference(pm,[status(thm)],[144,360,theory(equality)])).
% cnf(533,negated_conjecture,(m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))),inference(pm,[status(thm)],[142,360,theory(equality)])).
% cnf(534,negated_conjecture,(v1_funct_2(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))),inference(pm,[status(thm)],[143,360,theory(equality)])).
% cnf(540,negated_conjecture,(v1_funct_1(u2_lattices(esk19_0))),inference(pm,[status(thm)],[150,362,theory(equality)])).
% cnf(541,negated_conjecture,(m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))),inference(pm,[status(thm)],[148,362,theory(equality)])).
% cnf(542,negated_conjecture,(v1_funct_2(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))),inference(pm,[status(thm)],[149,362,theory(equality)])).
% cnf(548,negated_conjecture,(v1_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)|~l2_lattices(esk19_0)),inference(pm,[status(thm)],[179,402,theory(equality)])).
% cnf(553,negated_conjecture,(v1_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[548,362,theory(equality)])).
% cnf(554,negated_conjecture,(v1_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[553,theory(equality)])).
% cnf(555,negated_conjecture,(v1_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))),inference(sr,[status(thm)],[554,355,theory(equality)])).
% cnf(560,negated_conjecture,(v2_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)|~l2_lattices(esk19_0)),inference(pm,[status(thm)],[187,406,theory(equality)])).
% cnf(565,negated_conjecture,(v2_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[560,362,theory(equality)])).
% cnf(566,negated_conjecture,(v2_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[565,theory(equality)])).
% cnf(567,negated_conjecture,(v2_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))),inference(sr,[status(thm)],[566,355,theory(equality)])).
% cnf(572,negated_conjecture,(v1_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)|~l1_lattices(esk19_0)),inference(pm,[status(thm)],[195,410,theory(equality)])).
% cnf(577,negated_conjecture,(v1_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[572,360,theory(equality)])).
% cnf(578,negated_conjecture,(v1_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[577,theory(equality)])).
% cnf(579,negated_conjecture,(v1_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))),inference(sr,[status(thm)],[578,355,theory(equality)])).
% cnf(584,negated_conjecture,(v2_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)|~l1_lattices(esk19_0)),inference(pm,[status(thm)],[203,414,theory(equality)])).
% cnf(589,negated_conjecture,(v2_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[584,360,theory(equality)])).
% cnf(590,negated_conjecture,(v2_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|v3_struct_0(esk19_0)),inference(cn,[status(thm)],[589,theory(equality)])).
% cnf(591,negated_conjecture,(v2_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))),inference(sr,[status(thm)],[590,355,theory(equality)])).
% cnf(1573,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|k1_realset1(X3,esk20_0)!=esk21_0|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~r1_lattice2(X1,X3,X2)|~m2_relset_1(esk21_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk21_0)|~v1_funct_1(X2)|~v1_funct_1(X3)),inference(pm,[status(thm)],[526,349,theory(equality)])).
% cnf(1577,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|k1_realset1(X3,esk20_0)!=esk21_0|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~r1_lattice2(X1,X3,X2)|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk21_0)|~v1_funct_1(X2)|~v1_funct_1(X3)),inference(rw,[status(thm)],[1573,348,theory(equality)])).
% cnf(1578,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|k1_realset1(X3,esk20_0)!=esk21_0|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~r1_lattice2(X1,X3,X2)|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|$false|~v1_funct_1(X2)|~v1_funct_1(X3)),inference(rw,[status(thm)],[1577,350,theory(equality)])).
% cnf(1579,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk22_0|k1_realset1(X3,esk20_0)!=esk21_0|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~r1_lattice2(X1,X3,X2)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_1(X3)),inference(cn,[status(thm)],[1578,theory(equality)])).
% cnf(1600,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|k1_realset1(X3,esk20_0)!=esk22_0|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~r1_lattice2(X1,X3,X2)|~m2_relset_1(esk22_0,k2_zfmisc_1(esk20_0,esk20_0),esk20_0)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk22_0)|~v1_funct_1(X2)|~v1_funct_1(X3)),inference(pm,[status(thm)],[530,346,theory(equality)])).
% cnf(1602,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|k1_realset1(X3,esk20_0)!=esk22_0|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~r1_lattice2(X1,X3,X2)|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(esk22_0)|~v1_funct_1(X2)|~v1_funct_1(X3)),inference(rw,[status(thm)],[1600,345,theory(equality)])).
% cnf(1603,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|k1_realset1(X3,esk20_0)!=esk22_0|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~r1_lattice2(X1,X3,X2)|$false|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|$false|~v1_funct_1(X2)|~v1_funct_1(X3)),inference(rw,[status(thm)],[1602,347,theory(equality)])).
% cnf(1604,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(X1)|k1_realset1(X2,esk20_0)!=esk21_0|k1_realset1(X3,esk20_0)!=esk22_0|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)|~m1_subset_1(esk20_0,k1_zfmisc_1(X1))|~r1_lattice2(X1,X3,X2)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_1(X3)),inference(cn,[status(thm)],[1603,theory(equality)])).
% cnf(1686,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(u1_lattices(esk19_0),esk20_0)!=esk22_0|~v1_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(pm,[status(thm)],[496,534,theory(equality)])).
% cnf(1688,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(u1_lattices(esk19_0),esk20_0)!=esk22_0|~v2_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(pm,[status(thm)],[516,534,theory(equality)])).
% cnf(1715,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|~v1_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[1686,343,theory(equality)])).
% cnf(1716,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[1715,579,theory(equality)])).
% cnf(1717,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[1716,478,theory(equality)])).
% cnf(1718,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[1717,533,theory(equality)])).
% cnf(1719,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[1718,532,theory(equality)])).
% cnf(1720,negated_conjecture,(v1_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))),inference(cn,[status(thm)],[1719,theory(equality)])).
% cnf(1726,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|~v2_binop_1(u1_lattices(esk19_0),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[1688,343,theory(equality)])).
% cnf(1727,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[1726,591,theory(equality)])).
% cnf(1728,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[1727,478,theory(equality)])).
% cnf(1729,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[1728,533,theory(equality)])).
% cnf(1730,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[1729,532,theory(equality)])).
% cnf(1731,negated_conjecture,(v2_binop_1(esk22_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))),inference(cn,[status(thm)],[1730,theory(equality)])).
% cnf(1921,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(u2_lattices(esk19_0),esk20_0)!=esk21_0|~v1_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(pm,[status(thm)],[500,542,theory(equality)])).
% cnf(1925,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(u2_lattices(esk19_0),esk20_0)!=esk21_0|~v2_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(pm,[status(thm)],[520,542,theory(equality)])).
% cnf(1945,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|~v1_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[1921,344,theory(equality)])).
% cnf(1946,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[1945,555,theory(equality)])).
% cnf(1947,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[1946,478,theory(equality)])).
% cnf(1948,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[1947,541,theory(equality)])).
% cnf(1949,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[1948,540,theory(equality)])).
% cnf(1950,negated_conjecture,(v1_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))),inference(cn,[status(thm)],[1949,theory(equality)])).
% cnf(1968,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|~v2_binop_1(u2_lattices(esk19_0),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[1925,344,theory(equality)])).
% cnf(1969,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[1968,567,theory(equality)])).
% cnf(1970,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[1969,478,theory(equality)])).
% cnf(1971,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[1970,541,theory(equality)])).
% cnf(1972,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false|$false),inference(rw,[status(thm)],[1971,540,theory(equality)])).
% cnf(1973,negated_conjecture,(v2_binop_1(esk21_0,esk20_0)|v1_xboole_0(u1_struct_0(esk19_0))),inference(cn,[status(thm)],[1972,theory(equality)])).
% cnf(1974,negated_conjecture,(v1_xboole_0(u1_struct_0(esk19_0))|~v2_binop_1(esk22_0,esk20_0)|~v1_binop_1(esk21_0,esk20_0)|~v1_binop_1(esk22_0,esk20_0)|~r1_lattice2(esk20_0,esk21_0,esk22_0)|~r1_lattice2(esk20_0,esk22_0,esk21_0)),inference(pm,[status(thm)],[342,1973,theory(equality)])).
% cnf(2093,negated_conjecture,(v1_xboole_0(u1_struct_0(esk19_0))|~v1_binop_1(esk21_0,esk20_0)|~v1_binop_1(esk22_0,esk20_0)|~r1_lattice2(esk20_0,esk21_0,esk22_0)|~r1_lattice2(esk20_0,esk22_0,esk21_0)),inference(pm,[status(thm)],[1974,1731,theory(equality)])).
% cnf(2094,negated_conjecture,(v1_xboole_0(u1_struct_0(esk19_0))|~v1_binop_1(esk22_0,esk20_0)|~r1_lattice2(esk20_0,esk21_0,esk22_0)|~r1_lattice2(esk20_0,esk22_0,esk21_0)),inference(pm,[status(thm)],[2093,1950,theory(equality)])).
% cnf(2095,negated_conjecture,(v1_xboole_0(u1_struct_0(esk19_0))|~r1_lattice2(esk20_0,esk21_0,esk22_0)|~r1_lattice2(esk20_0,esk22_0,esk21_0)),inference(pm,[status(thm)],[2094,1720,theory(equality)])).
% cnf(6643,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(u1_lattices(esk19_0),esk20_0)!=esk22_0|k1_realset1(X1,esk20_0)!=esk21_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~r1_lattice2(u1_struct_0(esk19_0),X1,u1_lattices(esk19_0))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))|~v1_funct_1(X1)),inference(pm,[status(thm)],[1579,534,theory(equality)])).
% cnf(6659,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|k1_realset1(X1,esk20_0)!=esk21_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~r1_lattice2(u1_struct_0(esk19_0),X1,u1_lattices(esk19_0))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))|~v1_funct_1(X1)),inference(rw,[status(thm)],[6643,343,theory(equality)])).
% cnf(6660,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|k1_realset1(X1,esk20_0)!=esk21_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|$false|~r1_lattice2(u1_struct_0(esk19_0),X1,u1_lattices(esk19_0))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))|~v1_funct_1(X1)),inference(rw,[status(thm)],[6659,478,theory(equality)])).
% cnf(6661,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|k1_realset1(X1,esk20_0)!=esk21_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|$false|~r1_lattice2(u1_struct_0(esk19_0),X1,u1_lattices(esk19_0))|$false|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))|~v1_funct_1(X1)),inference(rw,[status(thm)],[6660,533,theory(equality)])).
% cnf(6662,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|k1_realset1(X1,esk20_0)!=esk21_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|$false|~r1_lattice2(u1_struct_0(esk19_0),X1,u1_lattices(esk19_0))|$false|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|$false|~v1_funct_1(X1)),inference(rw,[status(thm)],[6661,532,theory(equality)])).
% cnf(6663,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(X1,esk20_0)!=esk21_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~r1_lattice2(u1_struct_0(esk19_0),X1,u1_lattices(esk19_0))|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(X1)),inference(cn,[status(thm)],[6662,theory(equality)])).
% cnf(7102,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(u2_lattices(esk19_0),esk20_0)!=esk21_0|k1_realset1(X1,esk20_0)!=esk22_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~r1_lattice2(u1_struct_0(esk19_0),X1,u2_lattices(esk19_0))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))|~v1_funct_1(X1)),inference(pm,[status(thm)],[1604,542,theory(equality)])).
% cnf(7126,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|k1_realset1(X1,esk20_0)!=esk22_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m1_subset_1(esk20_0,k1_zfmisc_1(u1_struct_0(esk19_0)))|~r1_lattice2(u1_struct_0(esk19_0),X1,u2_lattices(esk19_0))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))|~v1_funct_1(X1)),inference(rw,[status(thm)],[7102,344,theory(equality)])).
% cnf(7127,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|k1_realset1(X1,esk20_0)!=esk22_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|$false|~r1_lattice2(u1_struct_0(esk19_0),X1,u2_lattices(esk19_0))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))|~v1_funct_1(X1)),inference(rw,[status(thm)],[7126,478,theory(equality)])).
% cnf(7128,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|k1_realset1(X1,esk20_0)!=esk22_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|$false|~r1_lattice2(u1_struct_0(esk19_0),X1,u2_lattices(esk19_0))|$false|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))|~v1_funct_1(X1)),inference(rw,[status(thm)],[7127,541,theory(equality)])).
% cnf(7129,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|k1_realset1(X1,esk20_0)!=esk22_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|$false|~r1_lattice2(u1_struct_0(esk19_0),X1,u2_lattices(esk19_0))|$false|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|$false|~v1_funct_1(X1)),inference(rw,[status(thm)],[7128,540,theory(equality)])).
% cnf(7130,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(X1,esk20_0)!=esk22_0|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~r1_lattice2(u1_struct_0(esk19_0),X1,u2_lattices(esk19_0))|~m2_relset_1(X1,k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(X1)),inference(cn,[status(thm)],[7129,theory(equality)])).
% cnf(37040,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(u2_lattices(esk19_0),esk20_0)!=esk21_0|~r1_lattice2(u1_struct_0(esk19_0),u2_lattices(esk19_0),u1_lattices(esk19_0))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(pm,[status(thm)],[6663,542,theory(equality)])).
% cnf(37045,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|~r1_lattice2(u1_struct_0(esk19_0),u2_lattices(esk19_0),u1_lattices(esk19_0))|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[37040,344,theory(equality)])).
% cnf(37046,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|~m2_relset_1(u2_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[37045,482,theory(equality)])).
% cnf(37047,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|~v1_funct_1(u2_lattices(esk19_0))),inference(rw,[status(thm)],[37046,541,theory(equality)])).
% cnf(37048,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false),inference(rw,[status(thm)],[37047,540,theory(equality)])).
% cnf(37049,negated_conjecture,(r1_lattice2(esk20_0,esk21_0,esk22_0)|v1_xboole_0(u1_struct_0(esk19_0))),inference(cn,[status(thm)],[37048,theory(equality)])).
% cnf(37050,negated_conjecture,(v1_xboole_0(u1_struct_0(esk19_0))|~r1_lattice2(esk20_0,esk22_0,esk21_0)),inference(pm,[status(thm)],[2095,37049,theory(equality)])).
% cnf(37090,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|k1_realset1(u1_lattices(esk19_0),esk20_0)!=esk22_0|~r1_lattice2(u1_struct_0(esk19_0),u1_lattices(esk19_0),u2_lattices(esk19_0))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(pm,[status(thm)],[7130,534,theory(equality)])).
% cnf(37092,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|~r1_lattice2(u1_struct_0(esk19_0),u1_lattices(esk19_0),u2_lattices(esk19_0))|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[37090,343,theory(equality)])).
% cnf(37093,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|~m2_relset_1(u1_lattices(esk19_0),k2_zfmisc_1(u1_struct_0(esk19_0),u1_struct_0(esk19_0)),u1_struct_0(esk19_0))|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[37092,488,theory(equality)])).
% cnf(37094,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|~v1_funct_1(u1_lattices(esk19_0))),inference(rw,[status(thm)],[37093,533,theory(equality)])).
% cnf(37095,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))|$false|$false|$false|$false),inference(rw,[status(thm)],[37094,532,theory(equality)])).
% cnf(37096,negated_conjecture,(r1_lattice2(esk20_0,esk22_0,esk21_0)|v1_xboole_0(u1_struct_0(esk19_0))),inference(cn,[status(thm)],[37095,theory(equality)])).
% cnf(37101,negated_conjecture,(v1_xboole_0(u1_struct_0(esk19_0))),inference(pm,[status(thm)],[37050,37096,theory(equality)])).
% cnf(37146,negated_conjecture,(v3_struct_0(esk19_0)|~l1_struct_0(esk19_0)),inference(pm,[status(thm)],[256,37101,theory(equality)])).
% cnf(37206,negated_conjecture,(v3_struct_0(esk19_0)|$false),inference(rw,[status(thm)],[37146,531,theory(equality)])).
% cnf(37207,negated_conjecture,(v3_struct_0(esk19_0)),inference(cn,[status(thm)],[37206,theory(equality)])).
% cnf(37208,negated_conjecture,($false),inference(sr,[status(thm)],[37207,355,theory(equality)])).
% cnf(37209,negated_conjecture,($false),37208,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 6523
% # ...of these trivial : 7
% # ...subsumed : 2109
% # ...remaining for further processing: 4407
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 24
% # Backward-rewritten : 102
% # Generated clauses : 25299
% # ...of the previous two non-trivial : 18162
% # Contextual simplify-reflections : 0
% # Paramodulations : 25293
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 4281
% # Positive orientable unit clauses: 3185
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 24
% # Non-unit-clauses : 1072
% # Current number of unprocessed clauses: 11088
% # ...number of literals in the above : 25835
% # Clause-clause subsumption calls (NU) : 86497
% # Rec. Clause-clause subsumption calls : 57038
% # Unit Clause-clause subsumption calls : 385
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 547637
% # Indexed BW rewrite successes : 10
% # Backwards rewriting index: 931 leaves, 7.44+/-41.212 terms/leaf
% # Paramod-from index: 365 leaves, 9.46+/-54.159 terms/leaf
% # Paramod-into index: 771 leaves, 8.07+/-44.485 terms/leaf
% # -------------------------------------------------
% # User time : 1.979 s
% # System time : 0.058 s
% # Total time : 2.037 s
% # Maximum resident set size: 0 pages
% PrfWatch: 2.52 CPU 2.65 WC
% FINAL PrfWatch: 2.52 CPU 2.65 WC
% SZS output end Solution for /tmp/SystemOnTPTP30659/LAT326+1.tptp
%
%------------------------------------------------------------------------------