%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT399-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:59:48 PM UTC 2026
% Result : Unsatisfiable 108.91s 26.99s
% Output : CNFRefutation 108.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 26
% Syntax : Number of formulae : 269 ( 269 unt; 16 def)
% Number of atoms : 833 ( 268 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 16 usr; 17 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 155 ( 0 sgn 155 !; 0 ?; 129 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity) ).
fof(f2,axiom,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity) ).
fof(f3,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_001) ).
fof(f4,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_002) ).
fof(f5,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption) ).
fof(f6,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption_003) ).
fof(f7,axiom,
! [X2,X0,X1] : upme(X0,X1,X2) = meet(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_upme) ).
fof(f8,axiom,
! [X2,X0,X1] : lome(X0,X1,X2) = join(meet(X0,X1),meet(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_lome) ).
fof(f9,negated_conjecture,
! [X2,X0,X1] : join(upme(meet(a,X0),X1,X2),meet(X1,X2)) = meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture) ).
fof(f10,negated_conjecture,
upme(meet(a,z1),z2,z3) != lome(meet(a,z1),z2,z3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture_1) ).
fof(f11,plain,
! [X2,X0,X1] : meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)) = join(meet(meet(a,X0),join(X1,X2)),meet(X1,X2)),
inference(definition_unfolding,[],[f9,f7]) ).
fof(f12,plain,
meet(meet(a,z1),join(z2,z3)) != join(meet(meet(a,z1),z2),meet(meet(a,z1),z3)),
inference(definition_unfolding,[],[f10,f7,f8]) ).
tcf(c_59,plain,
! [X0: $i,X1: $i] : meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_60,plain,
! [X0: $i,X1: $i,X2: $i] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f3]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] : join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_65,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)) = join(meet(meet(a,X0),join(X1,X2)),meet(X1,X2)),
inference(cnf_transformation,[],[f11]) ).
tcf(c_66,negated_conjecture,
join(meet(meet(a,z1),z2),meet(meet(a,z1),z3)) != meet(meet(a,z1),join(z2,z3)),
inference(cnf_transformation,[],[f12]) ).
tcf(c_74,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : meet(join(meet(a,meet(X0,X1)),X2),join(meet(a,meet(X0,X2)),X1)) = join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))),
inference(theory_normalisation,[status(thm)],[c_65,c_62,c_61,c_60,c_59]) ).
tcf(c_75,negated_conjecture,
join(meet(a,meet(z1,z2)),meet(a,meet(z1,z3))) != meet(a,meet(z1,join(z2,z3))),
inference(theory_normalisation,[status(thm)],[c_66,c_62,c_61,c_60,c_59]) ).
tcf(c_97,definition,
iPr_def_10 = meet(z1,z2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_98,definition,
iPr_def_11 = meet(a,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_99,definition,
iPr_def_12 = meet(z1,z3),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_100,definition,
iPr_def_13 = meet(a,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_101,definition,
iPr_def_14 = join(iPr_def_11,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_102,definition,
iPr_def_15 = join(z2,z3),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_103,definition,
iPr_def_16 = meet(z1,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_104,definition,
iPr_def_17 = meet(a,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_105,negated_conjecture,
iPr_def_14 != iPr_def_17,
inference(demodulation,[status(thm)],[c_75,c_102,c_103,c_104,c_99,c_100,c_97,c_98,c_101]) ).
tcf(c_106,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : meet(join(meet(a,meet(X0,X1)),X2),join(meet(a,meet(X0,X2)),X1)) = join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))),
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_107,definition,
iPr_def_18 = join(z2,z3),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_108,definition,
iPr_def_19 = meet(z1,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_109,definition,
iPr_def_20 = meet(a,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_110,definition,
iPr_def_21 = meet(z1,z3),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_111,definition,
iPr_def_22 = meet(a,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_112,definition,
iPr_def_23 = meet(z1,z2),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_113,definition,
iPr_def_24 = meet(a,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_114,definition,
iPr_def_25 = join(iPr_def_11,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_115,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : meet(join(meet(a,meet(X0,X1)),X2),join(meet(a,meet(X0,X2)),X1)) = join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_116,negated_conjecture,
iPr_def_14 != iPr_def_17,
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_117,plain,
iPr_def_15 = iPr_def_18,
inference(demodulation,[status(thm)],[c_102,c_107]) ).
tcf(c_118,plain,
iPr_def_16 = iPr_def_19,
inference(demodulation,[status(thm)],[c_103,c_108]) ).
tcf(c_119,plain,
iPr_def_17 = iPr_def_20,
inference(demodulation,[status(thm)],[c_104,c_109]) ).
tcf(c_120,plain,
iPr_def_12 = iPr_def_21,
inference(demodulation,[status(thm)],[c_99,c_110]) ).
tcf(c_121,plain,
iPr_def_13 = iPr_def_22,
inference(demodulation,[status(thm)],[c_100,c_111]) ).
tcf(c_122,plain,
iPr_def_10 = iPr_def_23,
inference(demodulation,[status(thm)],[c_97,c_112]) ).
tcf(c_123,plain,
iPr_def_11 = iPr_def_24,
inference(demodulation,[status(thm)],[c_98,c_113]) ).
tcf(c_124,plain,
iPr_def_14 = iPr_def_25,
inference(demodulation,[status(thm)],[c_101,c_114]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i] : meet(X0,join(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i] : join(X0,meet(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(demodulation,[status(thm)],[c_62]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(demodulation,[status(thm)],[c_60]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] : meet(X0,X1) = meet(X1,X0),
inference(demodulation,[status(thm)],[c_59]) ).
tcf(c_220,plain,
meet(a,iPr_def_12) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_111,c_121]) ).
tcf(c_221,plain,
meet(iPr_def_12,a) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_220,c_129,c_130,c_127,c_128]) ).
tcf(c_264,plain,
! [X0: $i,X1: $i] : join(X0,meet(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_130,c_126]) ).
tcf(c_298,plain,
! [X0: $i] : meet(iPr_def_12,meet(a,X0)) = meet(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_221,c_129]) ).
tcf(c_327,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,meet(X1,meet(X2,X0))) = X0,
inference(superposition,[status(thm)],[c_129,c_264]) ).
tcf(c_1679,plain,
! [X0: $i] : meet(X0,X0) = X0,
inference(superposition,[status(thm)],[c_126,c_125]) ).
tcf(c_1680,plain,
join(z2,z3) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_107,c_117]) ).
tcf(c_1681,plain,
meet(z2,iPr_def_15) = z2,
inference(superposition,[status(thm)],[c_1680,c_125]) ).
tcf(c_1682,plain,
meet(z1,iPr_def_15) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_108,c_118]) ).
tcf(c_1683,plain,
meet(iPr_def_15,z1) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_1682,c_129,c_130,c_127,c_128]) ).
tcf(c_1684,plain,
join(iPr_def_15,iPr_def_16) = iPr_def_15,
inference(superposition,[status(thm)],[c_1683,c_126]) ).
tcf(c_1685,plain,
meet(iPr_def_15,z2) = z2,
inference(theory_normalisation,[status(thm)],[c_1681,c_129,c_130,c_127,c_128]) ).
tcf(c_1686,plain,
meet(a,iPr_def_16) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_109,c_119]) ).
tcf(c_1687,plain,
meet(iPr_def_16,a) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_1686,c_129,c_130,c_127,c_128]) ).
tcf(c_1688,plain,
join(iPr_def_16,iPr_def_17) = iPr_def_16,
inference(superposition,[status(thm)],[c_1687,c_126]) ).
tcf(c_1689,plain,
meet(z1,z3) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_110,c_120]) ).
tcf(c_1690,plain,
join(z1,iPr_def_12) = z1,
inference(superposition,[status(thm)],[c_1689,c_126]) ).
tcf(c_1691,plain,
join(iPr_def_12,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_1690,c_129,c_130,c_127,c_128]) ).
tcf(c_1692,plain,
meet(a,iPr_def_12) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_111,c_121]) ).
tcf(c_1693,plain,
meet(iPr_def_12,a) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_1692,c_129,c_130,c_127,c_128]) ).
tcf(c_1694,plain,
join(iPr_def_12,iPr_def_13) = iPr_def_12,
inference(superposition,[status(thm)],[c_1693,c_126]) ).
tcf(c_1695,plain,
meet(z1,z2) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_112,c_122]) ).
tcf(c_1696,plain,
join(z1,iPr_def_10) = z1,
inference(superposition,[status(thm)],[c_1695,c_126]) ).
tcf(c_1697,plain,
join(iPr_def_10,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_1696,c_129,c_130,c_127,c_128]) ).
tcf(c_1698,plain,
meet(a,iPr_def_10) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_113,c_123]) ).
tcf(c_1699,plain,
meet(iPr_def_10,a) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_1698,c_129,c_130,c_127,c_128]) ).
tcf(c_1700,plain,
join(iPr_def_10,iPr_def_11) = iPr_def_10,
inference(superposition,[status(thm)],[c_1699,c_126]) ).
tcf(c_1703,plain,
! [X0: $i] : join(z2,join(z3,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_1680,c_127]) ).
tcf(c_1705,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,meet(join(X0,X1),X2))) = join(X0,X1),
inference(superposition,[status(thm)],[c_127,c_126]) ).
tcf(c_1706,plain,
join(iPr_def_11,iPr_def_13) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_114,c_124]) ).
tcf(c_1707,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_13,X0)) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_1706,c_127]) ).
tcf(c_1709,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_16,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_1684,c_127]) ).
tcf(c_1711,plain,
join(iPr_def_15,z2) = iPr_def_15,
inference(superposition,[status(thm)],[c_1685,c_126]) ).
tcf(c_1720,plain,
meet(iPr_def_12,z1) = iPr_def_12,
inference(superposition,[status(thm)],[c_1691,c_125]) ).
tcf(c_1723,plain,
! [X0: $i,X1: $i] : meet(X0,join(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_128,c_125]) ).
tcf(c_1725,plain,
! [X0: $i] : join(iPr_def_10,join(z1,X0)) = join(z1,X0),
inference(superposition,[status(thm)],[c_1697,c_127]) ).
tcf(c_1726,plain,
meet(iPr_def_10,z1) = iPr_def_10,
inference(superposition,[status(thm)],[c_1697,c_125]) ).
tcf(c_1730,plain,
! [X0: $i] : join(iPr_def_15,join(z2,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_1711,c_127]) ).
tcf(c_1734,plain,
! [X0: $i,X1: $i] : join(X0,meet(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_130,c_126]) ).
tcf(c_1738,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,join(X1,join(X2,X0))) = X0,
inference(superposition,[status(thm)],[c_127,c_1723]) ).
tcf(c_1741,plain,
meet(iPr_def_13,iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_1706,c_1723]) ).
tcf(c_1743,plain,
meet(iPr_def_16,iPr_def_15) = iPr_def_16,
inference(superposition,[status(thm)],[c_1684,c_1723]) ).
tcf(c_1744,plain,
meet(iPr_def_17,iPr_def_16) = iPr_def_17,
inference(superposition,[status(thm)],[c_1688,c_1723]) ).
tcf(c_1746,plain,
meet(iPr_def_13,iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_1694,c_1723]) ).
tcf(c_1748,plain,
meet(iPr_def_11,iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_1700,c_1723]) ).
tcf(c_1752,plain,
meet(iPr_def_10,iPr_def_11) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_1748,c_129,c_130,c_127,c_128]) ).
tcf(c_1753,plain,
meet(iPr_def_12,iPr_def_13) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_1746,c_129,c_130,c_127,c_128]) ).
tcf(c_1754,plain,
meet(iPr_def_16,iPr_def_17) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_1744,c_129,c_130,c_127,c_128]) ).
tcf(c_1755,plain,
meet(iPr_def_15,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_1743,c_129,c_130,c_127,c_128]) ).
tcf(c_1765,plain,
! [X0: $i] : meet(iPr_def_15,meet(z1,X0)) = meet(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_1683,c_129]) ).
tcf(c_1767,plain,
! [X0: $i] : meet(iPr_def_16,meet(a,X0)) = meet(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_1687,c_129]) ).
tcf(c_1769,plain,
! [X0: $i] : meet(iPr_def_10,meet(a,X0)) = meet(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_1699,c_129]) ).
tcf(c_1777,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,meet(X1,join(X2,meet(X0,X1)))) = meet(X0,X1),
inference(superposition,[status(thm)],[c_129,c_1723]) ).
tcf(c_1786,plain,
! [X0: $i] : meet(iPr_def_15,meet(iPr_def_16,X0)) = meet(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_1755,c_129]) ).
tcf(c_1799,plain,
join(z2,iPr_def_10) = z2,
inference(superposition,[status(thm)],[c_1695,c_1734]) ).
tcf(c_1800,plain,
join(z3,iPr_def_12) = z3,
inference(superposition,[status(thm)],[c_1689,c_1734]) ).
tcf(c_1802,plain,
join(z1,iPr_def_16) = z1,
inference(superposition,[status(thm)],[c_1683,c_1734]) ).
tcf(c_1805,plain,
join(a,iPr_def_13) = a,
inference(superposition,[status(thm)],[c_1693,c_1734]) ).
tcf(c_1806,plain,
join(a,iPr_def_11) = a,
inference(superposition,[status(thm)],[c_1699,c_1734]) ).
tcf(c_1811,plain,
join(iPr_def_14,iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_1741,c_1734]) ).
tcf(c_1817,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(meet(X1,X0),X2)) = join(X0,X2),
inference(superposition,[status(thm)],[c_1734,c_127]) ).
tcf(c_1821,plain,
join(iPr_def_13,iPr_def_14) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_1811,c_129,c_130,c_127,c_128]) ).
tcf(c_1825,plain,
join(iPr_def_11,a) = a,
inference(theory_normalisation,[status(thm)],[c_1806,c_129,c_130,c_127,c_128]) ).
tcf(c_1826,plain,
join(iPr_def_13,a) = a,
inference(theory_normalisation,[status(thm)],[c_1805,c_129,c_130,c_127,c_128]) ).
tcf(c_1828,plain,
join(iPr_def_16,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_1802,c_129,c_130,c_127,c_128]) ).
tcf(c_1829,plain,
join(iPr_def_12,z3) = z3,
inference(theory_normalisation,[status(thm)],[c_1800,c_129,c_130,c_127,c_128]) ).
tcf(c_1830,plain,
join(iPr_def_10,z2) = z2,
inference(theory_normalisation,[status(thm)],[c_1799,c_129,c_130,c_127,c_128]) ).
tcf(c_1854,plain,
! [X0: $i] : meet(join(meet(a,iPr_def_11),X0),join(meet(a,meet(iPr_def_10,X0)),a)) = join(meet(a,X0),meet(a,meet(iPr_def_10,join(a,X0)))),
inference(superposition,[status(thm)],[c_1699,c_115]) ).
tcf(c_1876,plain,
! [X0: $i] : meet(join(meet(a,meet(z1,X0)),z3),join(meet(a,iPr_def_12),X0)) = join(meet(X0,z3),meet(a,meet(z1,join(X0,z3)))),
inference(superposition,[status(thm)],[c_1689,c_115]) ).
tcf(c_1891,plain,
! [X0: $i] : meet(join(meet(a,meet(iPr_def_15,X0)),iPr_def_16),join(meet(a,iPr_def_16),X0)) = join(meet(X0,iPr_def_16),meet(a,meet(iPr_def_15,join(X0,iPr_def_16)))),
inference(superposition,[status(thm)],[c_1755,c_115]) ).
tcf(c_1903,plain,
! [X0: $i] : meet(join(meet(iPr_def_16,a),X0),join(iPr_def_16,meet(iPr_def_15,meet(X0,a)))) = join(meet(X0,iPr_def_16),meet(iPr_def_15,meet(a,join(X0,iPr_def_16)))),
inference(theory_normalisation,[status(thm)],[c_1891,c_129,c_130,c_127,c_128]) ).
tcf(c_1904,plain,
! [X0: $i] : meet(join(iPr_def_17,X0),join(iPr_def_16,meet(iPr_def_15,meet(X0,a)))) = join(meet(X0,iPr_def_16),meet(iPr_def_15,meet(a,join(X0,iPr_def_16)))),
inference(demodulation,[status(thm)],[c_1903,c_1687]) ).
tcf(c_1933,plain,
! [X0: $i] : meet(join(meet(iPr_def_12,a),X0),join(z3,meet(a,meet(z1,X0)))) = join(meet(X0,z3),meet(a,meet(z1,join(X0,z3)))),
inference(theory_normalisation,[status(thm)],[c_1876,c_129,c_130,c_127,c_128]) ).
tcf(c_1934,plain,
! [X0: $i] : meet(join(iPr_def_13,X0),join(z3,meet(a,meet(z1,X0)))) = join(meet(X0,z3),meet(a,meet(z1,join(X0,z3)))),
inference(demodulation,[status(thm)],[c_1933,c_1693]) ).
tcf(c_1957,plain,
! [X0: $i] : meet(join(meet(iPr_def_11,a),X0),join(a,meet(iPr_def_10,meet(X0,a)))) = join(meet(a,X0),meet(iPr_def_10,meet(a,join(a,X0)))),
inference(theory_normalisation,[status(thm)],[c_1854,c_129,c_130,c_127,c_128]) ).
tcf(c_1958,plain,
! [X0: $i] : join(meet(a,X0),meet(iPr_def_11,join(a,X0))) = meet(a,join(meet(iPr_def_11,a),X0)),
inference(demodulation,[status(thm)],[c_1957,c_130,c_1769,c_327]) ).
tcf(c_2013,plain,
meet(iPr_def_11,a) = iPr_def_11,
inference(superposition,[status(thm)],[c_1825,c_125]) ).
tcf(c_2018,plain,
! [X0: $i] : join(meet(a,X0),meet(iPr_def_11,join(a,X0))) = meet(a,join(iPr_def_11,X0)),
inference(demodulation,[status(thm)],[c_1958,c_2013]) ).
tcf(c_2038,plain,
meet(iPr_def_16,z1) = iPr_def_16,
inference(superposition,[status(thm)],[c_1828,c_125]) ).
tcf(c_2041,plain,
meet(iPr_def_12,z3) = iPr_def_12,
inference(superposition,[status(thm)],[c_1829,c_125]) ).
tcf(c_2043,plain,
! [X0: $i] : join(iPr_def_10,join(z2,X0)) = join(z2,X0),
inference(superposition,[status(thm)],[c_1830,c_127]) ).
tcf(c_2044,plain,
meet(iPr_def_10,z2) = iPr_def_10,
inference(superposition,[status(thm)],[c_1830,c_125]) ).
tcf(c_2047,plain,
! [X0: $i] : meet(iPr_def_12,meet(X0,a)) = meet(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_130,c_298]) ).
tcf(c_2072,plain,
! [X0: $i] : meet(iPr_def_11,meet(a,X0)) = meet(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_2013,c_129]) ).
tcf(c_2198,plain,
! [X0: $i] : join(z1,meet(X0,iPr_def_12)) = z1,
inference(superposition,[status(thm)],[c_1720,c_327]) ).
tcf(c_2200,plain,
! [X0: $i] : join(z1,meet(X0,iPr_def_10)) = z1,
inference(superposition,[status(thm)],[c_1726,c_327]) ).
tcf(c_2212,plain,
! [X0: $i] : join(z1,meet(X0,iPr_def_16)) = z1,
inference(superposition,[status(thm)],[c_2038,c_327]) ).
tcf(c_2213,plain,
! [X0: $i] : join(z3,meet(X0,iPr_def_12)) = z3,
inference(superposition,[status(thm)],[c_2041,c_327]) ).
tcf(c_2214,plain,
! [X0: $i] : join(z2,meet(X0,iPr_def_10)) = z2,
inference(superposition,[status(thm)],[c_2044,c_327]) ).
tcf(c_2293,plain,
! [X0: $i] : join(z1,meet(iPr_def_12,X0)) = z1,
inference(superposition,[status(thm)],[c_130,c_2198]) ).
tcf(c_2303,plain,
! [X0: $i] : join(z1,meet(iPr_def_10,X0)) = z1,
inference(superposition,[status(thm)],[c_130,c_2200]) ).
tcf(c_2444,plain,
! [X0: $i] : join(z1,meet(iPr_def_16,X0)) = z1,
inference(superposition,[status(thm)],[c_130,c_2212]) ).
tcf(c_2455,plain,
! [X0: $i] : join(z3,meet(iPr_def_12,X0)) = z3,
inference(superposition,[status(thm)],[c_130,c_2213]) ).
tcf(c_2465,plain,
! [X0: $i] : join(z2,meet(iPr_def_10,X0)) = z2,
inference(superposition,[status(thm)],[c_130,c_2214]) ).
tcf(c_2499,plain,
join(z1,iPr_def_13) = z1,
inference(superposition,[status(thm)],[c_1753,c_2293]) ).
tcf(c_2506,plain,
join(iPr_def_13,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_2499,c_129,c_130,c_127,c_128]) ).
tcf(c_2636,plain,
join(z1,iPr_def_11) = z1,
inference(superposition,[status(thm)],[c_1752,c_2303]) ).
tcf(c_2644,plain,
join(iPr_def_11,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_2636,c_129,c_130,c_127,c_128]) ).
tcf(c_2753,plain,
join(z1,iPr_def_17) = z1,
inference(superposition,[status(thm)],[c_1754,c_2444]) ).
tcf(c_2761,plain,
join(iPr_def_17,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_2753,c_129,c_130,c_127,c_128]) ).
tcf(c_2842,plain,
meet(iPr_def_17,z1) = iPr_def_17,
inference(superposition,[status(thm)],[c_2761,c_125]) ).
tcf(c_2876,plain,
join(z3,iPr_def_13) = z3,
inference(superposition,[status(thm)],[c_1753,c_2455]) ).
tcf(c_2885,plain,
join(iPr_def_13,z3) = z3,
inference(theory_normalisation,[status(thm)],[c_2876,c_129,c_130,c_127,c_128]) ).
tcf(c_2923,plain,
join(z2,iPr_def_11) = z2,
inference(superposition,[status(thm)],[c_1752,c_2465]) ).
tcf(c_2931,plain,
join(iPr_def_11,z2) = z2,
inference(theory_normalisation,[status(thm)],[c_2923,c_129,c_130,c_127,c_128]) ).
tcf(c_2934,plain,
meet(iPr_def_11,z2) = iPr_def_11,
inference(superposition,[status(thm)],[c_2931,c_125]) ).
tcf(c_2948,plain,
! [X0: $i] : join(z2,meet(X0,iPr_def_11)) = z2,
inference(superposition,[status(thm)],[c_2934,c_327]) ).
tcf(c_2970,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_12,X0)) = join(z2,z3),
inference(superposition,[status(thm)],[c_2455,c_1703]) ).
tcf(c_2976,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_12,X0)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2970,c_1680]) ).
tcf(c_3083,plain,
! [X0: $i] : join(z2,meet(iPr_def_11,X0)) = z2,
inference(superposition,[status(thm)],[c_130,c_2948]) ).
tcf(c_3296,plain,
join(iPr_def_15,iPr_def_12) = iPr_def_15,
inference(superposition,[status(thm)],[c_2041,c_2976]) ).
tcf(c_3306,plain,
join(iPr_def_12,iPr_def_15) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_3296,c_129,c_130,c_127,c_128]) ).
tcf(c_3312,plain,
meet(iPr_def_12,iPr_def_15) = iPr_def_12,
inference(superposition,[status(thm)],[c_3306,c_125]) ).
tcf(c_3678,plain,
join(iPr_def_11,a) = join(iPr_def_14,a),
inference(superposition,[status(thm)],[c_1826,c_1707]) ).
tcf(c_3679,plain,
join(iPr_def_11,z1) = join(iPr_def_14,z1),
inference(superposition,[status(thm)],[c_2506,c_1707]) ).
tcf(c_3680,plain,
join(iPr_def_11,z3) = join(iPr_def_14,z3),
inference(superposition,[status(thm)],[c_2885,c_1707]) ).
tcf(c_3692,plain,
join(iPr_def_14,z1) = z1,
inference(demodulation,[status(thm)],[c_3679,c_2644]) ).
tcf(c_3693,plain,
join(iPr_def_14,a) = a,
inference(demodulation,[status(thm)],[c_3678,c_1825]) ).
tcf(c_3707,plain,
meet(iPr_def_14,z1) = iPr_def_14,
inference(superposition,[status(thm)],[c_3692,c_125]) ).
tcf(c_3716,plain,
meet(iPr_def_14,a) = iPr_def_14,
inference(superposition,[status(thm)],[c_3693,c_125]) ).
tcf(c_3725,plain,
! [X0: $i] : meet(iPr_def_14,meet(z1,X0)) = meet(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_3707,c_129]) ).
tcf(c_3744,plain,
! [X0: $i] : meet(iPr_def_14,meet(a,X0)) = meet(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_3716,c_129]) ).
tcf(c_3828,plain,
meet(iPr_def_14,join(iPr_def_11,z3)) = iPr_def_14,
inference(superposition,[status(thm)],[c_3680,c_125]) ).
tcf(c_3841,plain,
join(iPr_def_15,iPr_def_16) = join(iPr_def_15,iPr_def_17),
inference(superposition,[status(thm)],[c_1688,c_1709]) ).
tcf(c_3857,plain,
join(iPr_def_15,iPr_def_17) = iPr_def_15,
inference(demodulation,[status(thm)],[c_3841,c_1684]) ).
tcf(c_3873,plain,
meet(iPr_def_17,iPr_def_15) = iPr_def_17,
inference(superposition,[status(thm)],[c_3857,c_1723]) ).
tcf(c_3879,plain,
meet(iPr_def_15,iPr_def_17) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_3873,c_129,c_130,c_127,c_128]) ).
tcf(c_4553,plain,
! [X0: $i] : meet(iPr_def_10,join(z1,X0)) = iPr_def_10,
inference(superposition,[status(thm)],[c_1725,c_125]) ).
tcf(c_4806,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_10,X0)) = join(iPr_def_15,z2),
inference(superposition,[status(thm)],[c_2465,c_1730]) ).
tcf(c_4807,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_11,X0)) = join(iPr_def_15,z2),
inference(superposition,[status(thm)],[c_3083,c_1730]) ).
tcf(c_4821,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_11,X0)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_4807,c_1711]) ).
tcf(c_4822,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_10,X0)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_4806,c_1711]) ).
tcf(c_4887,plain,
join(iPr_def_15,iPr_def_11) = iPr_def_15,
inference(superposition,[status(thm)],[c_1679,c_4821]) ).
tcf(c_4907,plain,
join(iPr_def_11,iPr_def_15) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_4887,c_129,c_130,c_127,c_128]) ).
tcf(c_4936,plain,
meet(iPr_def_11,iPr_def_15) = iPr_def_11,
inference(superposition,[status(thm)],[c_4907,c_125]) ).
tcf(c_4978,plain,
! [X0: $i] : meet(join(meet(a,iPr_def_11),X0),join(meet(a,meet(iPr_def_11,X0)),iPr_def_15)) = join(meet(iPr_def_15,X0),meet(a,meet(iPr_def_11,join(iPr_def_15,X0)))),
inference(superposition,[status(thm)],[c_4936,c_115]) ).
tcf(c_4999,plain,
! [X0: $i] : meet(join(meet(iPr_def_11,a),X0),join(iPr_def_15,meet(iPr_def_11,meet(X0,a)))) = join(meet(iPr_def_15,X0),meet(iPr_def_11,meet(a,join(iPr_def_15,X0)))),
inference(theory_normalisation,[status(thm)],[c_4978,c_129,c_130,c_127,c_128]) ).
tcf(c_5000,plain,
! [X0: $i] : join(meet(iPr_def_15,X0),meet(iPr_def_11,join(iPr_def_15,X0))) = meet(iPr_def_15,join(iPr_def_11,X0)),
inference(demodulation,[status(thm)],[c_4999,c_130,c_2013,c_2072,c_4821]) ).
tcf(c_5012,plain,
join(iPr_def_15,iPr_def_10) = iPr_def_15,
inference(superposition,[status(thm)],[c_4553,c_4822]) ).
tcf(c_5026,plain,
join(iPr_def_10,iPr_def_15) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_5012,c_129,c_130,c_127,c_128]) ).
tcf(c_5064,plain,
! [X0: $i] : meet(iPr_def_13,join(X0,iPr_def_12)) = iPr_def_13,
inference(superposition,[status(thm)],[c_1694,c_1738]) ).
tcf(c_5066,plain,
! [X0: $i] : meet(iPr_def_11,join(X0,iPr_def_10)) = iPr_def_11,
inference(superposition,[status(thm)],[c_1700,c_1738]) ).
tcf(c_5293,plain,
meet(iPr_def_10,iPr_def_15) = iPr_def_10,
inference(superposition,[status(thm)],[c_5026,c_125]) ).
tcf(c_5739,plain,
! [X0: $i] : meet(iPr_def_13,join(iPr_def_12,X0)) = iPr_def_13,
inference(superposition,[status(thm)],[c_128,c_5064]) ).
tcf(c_5772,plain,
! [X0: $i] : meet(iPr_def_11,join(iPr_def_10,X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_128,c_5066]) ).
tcf(c_7039,plain,
! [X0: $i] : meet(iPr_def_15,meet(X0,z1)) = meet(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_130,c_1765]) ).
tcf(c_7043,plain,
meet(iPr_def_15,iPr_def_10) = meet(iPr_def_16,z2),
inference(superposition,[status(thm)],[c_1695,c_1765]) ).
tcf(c_7044,plain,
meet(iPr_def_15,iPr_def_12) = meet(iPr_def_16,z3),
inference(superposition,[status(thm)],[c_1689,c_1765]) ).
tcf(c_7064,plain,
meet(iPr_def_12,iPr_def_15) = meet(iPr_def_16,z3),
inference(theory_normalisation,[status(thm)],[c_7044,c_129,c_130,c_127,c_128]) ).
tcf(c_7065,plain,
meet(iPr_def_16,z3) = iPr_def_12,
inference(demodulation,[status(thm)],[c_7064,c_3312]) ).
tcf(c_7066,plain,
meet(iPr_def_10,iPr_def_15) = meet(iPr_def_16,z2),
inference(theory_normalisation,[status(thm)],[c_7043,c_129,c_130,c_127,c_128]) ).
tcf(c_7067,plain,
meet(iPr_def_16,z2) = iPr_def_10,
inference(demodulation,[status(thm)],[c_7066,c_5293]) ).
tcf(c_7088,plain,
join(iPr_def_16,iPr_def_12) = iPr_def_16,
inference(superposition,[status(thm)],[c_7065,c_126]) ).
tcf(c_7100,plain,
join(iPr_def_12,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_7088,c_129,c_130,c_127,c_128]) ).
tcf(c_7111,plain,
join(iPr_def_16,iPr_def_10) = iPr_def_16,
inference(superposition,[status(thm)],[c_7067,c_126]) ).
tcf(c_7123,plain,
join(iPr_def_10,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_7111,c_129,c_130,c_127,c_128]) ).
tcf(c_7141,plain,
meet(iPr_def_13,iPr_def_16) = iPr_def_13,
inference(superposition,[status(thm)],[c_7100,c_5739]) ).
tcf(c_7204,plain,
meet(iPr_def_11,iPr_def_16) = iPr_def_11,
inference(superposition,[status(thm)],[c_7123,c_5772]) ).
tcf(c_7235,plain,
join(iPr_def_16,iPr_def_13) = iPr_def_16,
inference(superposition,[status(thm)],[c_7141,c_1734]) ).
tcf(c_7253,plain,
join(iPr_def_13,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_7235,c_129,c_130,c_127,c_128]) ).
tcf(c_7267,plain,
join(iPr_def_16,iPr_def_11) = iPr_def_16,
inference(superposition,[status(thm)],[c_7204,c_1734]) ).
tcf(c_7279,plain,
! [X0: $i] : join(iPr_def_16,meet(X0,iPr_def_11)) = iPr_def_16,
inference(superposition,[status(thm)],[c_7204,c_327]) ).
tcf(c_7285,plain,
join(iPr_def_11,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_7267,c_129,c_130,c_127,c_128]) ).
tcf(c_7304,plain,
join(iPr_def_11,iPr_def_16) = join(iPr_def_14,iPr_def_16),
inference(superposition,[status(thm)],[c_7253,c_1707]) ).
tcf(c_7307,plain,
join(iPr_def_14,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_7304,c_7285]) ).
tcf(c_7326,plain,
meet(iPr_def_14,iPr_def_16) = iPr_def_14,
inference(superposition,[status(thm)],[c_7307,c_125]) ).
tcf(c_7393,plain,
! [X0: $i] : join(iPr_def_16,meet(X0,iPr_def_14)) = iPr_def_16,
inference(superposition,[status(thm)],[c_7326,c_327]) ).
tcf(c_7555,plain,
! [X0: $i] : join(iPr_def_16,meet(iPr_def_11,X0)) = iPr_def_16,
inference(superposition,[status(thm)],[c_130,c_7279]) ).
tcf(c_7614,plain,
! [X0: $i] : meet(iPr_def_11,join(a,X0)) = meet(iPr_def_10,a),
inference(superposition,[status(thm)],[c_125,c_1769]) ).
tcf(c_7636,plain,
! [X0: $i] : meet(iPr_def_11,join(a,X0)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7614,c_1699]) ).
tcf(c_7651,plain,
! [X0: $i] : meet(a,join(iPr_def_11,X0)) = join(meet(a,X0),iPr_def_11),
inference(demodulation,[status(thm)],[c_2018,c_7636]) ).
tcf(c_7652,plain,
! [X0: $i] : meet(a,join(iPr_def_11,X0)) = join(iPr_def_11,meet(a,X0)),
inference(theory_normalisation,[status(thm)],[c_7651,c_129,c_130,c_127,c_128]) ).
tcf(c_7700,plain,
! [X0: $i] : join(iPr_def_16,meet(iPr_def_14,X0)) = iPr_def_16,
inference(superposition,[status(thm)],[c_130,c_7393]) ).
tcf(c_10562,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_11,X0)) = join(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_7204,c_1817]) ).
tcf(c_10656,plain,
! [X0: $i] : join(iPr_def_11,join(X0,iPr_def_16)) = join(iPr_def_16,X0),
inference(theory_normalisation,[status(thm)],[c_10562,c_129,c_130,c_127,c_128]) ).
tcf(c_13157,plain,
! [X0: $i] : meet(iPr_def_11,join(z2,X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_2043,c_5772]) ).
tcf(c_14235,plain,
! [X0: $i] : meet(iPr_def_11,join(iPr_def_15,X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_1703,c_13157]) ).
tcf(c_14310,plain,
! [X0: $i] : meet(iPr_def_15,join(iPr_def_11,X0)) = join(meet(iPr_def_15,X0),iPr_def_11),
inference(demodulation,[status(thm)],[c_5000,c_14235]) ).
tcf(c_14313,plain,
! [X0: $i] : meet(iPr_def_15,join(iPr_def_11,X0)) = join(iPr_def_11,meet(iPr_def_15,X0)),
inference(theory_normalisation,[status(thm)],[c_14310,c_129,c_130,c_127,c_128]) ).
tcf(c_15519,plain,
meet(iPr_def_12,iPr_def_17) = meet(iPr_def_13,iPr_def_16),
inference(superposition,[status(thm)],[c_1687,c_2047]) ).
tcf(c_15564,plain,
meet(iPr_def_12,iPr_def_17) = iPr_def_13,
inference(demodulation,[status(thm)],[c_15519,c_7141]) ).
tcf(c_15674,plain,
join(iPr_def_17,iPr_def_13) = iPr_def_17,
inference(superposition,[status(thm)],[c_15564,c_1734]) ).
tcf(c_15696,plain,
join(iPr_def_13,iPr_def_17) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_15674,c_129,c_130,c_127,c_128]) ).
tcf(c_15729,plain,
join(iPr_def_11,iPr_def_17) = join(iPr_def_14,iPr_def_17),
inference(superposition,[status(thm)],[c_15696,c_1707]) ).
tcf(c_18016,plain,
meet(join(iPr_def_17,iPr_def_11),join(iPr_def_16,meet(iPr_def_15,meet(iPr_def_11,a)))) = join(iPr_def_11,meet(iPr_def_15,meet(a,join(iPr_def_11,iPr_def_16)))),
inference(superposition,[status(thm)],[c_7204,c_1904]) ).
tcf(c_18029,plain,
meet(join(iPr_def_17,iPr_def_14),join(iPr_def_16,meet(iPr_def_15,meet(iPr_def_14,a)))) = join(meet(iPr_def_14,iPr_def_16),meet(iPr_def_15,meet(a,iPr_def_16))),
inference(superposition,[status(thm)],[c_7307,c_1904]) ).
tcf(c_18050,plain,
meet(join(iPr_def_14,iPr_def_17),join(iPr_def_16,meet(iPr_def_14,meet(iPr_def_15,a)))) = join(meet(iPr_def_14,iPr_def_16),meet(iPr_def_15,meet(iPr_def_16,a))),
inference(theory_normalisation,[status(thm)],[c_18029,c_129,c_130,c_127,c_128]) ).
tcf(c_18051,plain,
meet(iPr_def_16,join(iPr_def_11,iPr_def_17)) = join(iPr_def_11,iPr_def_17),
inference(demodulation,[status(thm)],[c_18050,c_130,c_1687,c_1786,c_7326,c_7700,c_15729]) ).
tcf(c_18064,plain,
meet(join(iPr_def_11,iPr_def_17),join(iPr_def_16,meet(iPr_def_11,meet(iPr_def_15,a)))) = join(iPr_def_11,meet(iPr_def_15,meet(a,join(iPr_def_11,iPr_def_16)))),
inference(theory_normalisation,[status(thm)],[c_18016,c_129,c_130,c_127,c_128]) ).
tcf(c_18065,plain,
meet(iPr_def_16,join(iPr_def_11,iPr_def_17)) = iPr_def_17,
inference(demodulation,[status(thm)],[c_18064,c_130,c_128,c_1687,c_3879,c_7285,c_7555,c_7652,c_10656,c_14313]) ).
tcf(c_18291,plain,
join(iPr_def_11,iPr_def_17) = iPr_def_17,
inference(superposition,[status(thm)],[c_18051,c_18065]) ).
tcf(c_18394,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_17,X0)) = join(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_18291,c_127]) ).
tcf(c_23861,plain,
meet(join(iPr_def_13,z2),join(z3,meet(a,meet(z1,z2)))) = join(meet(z2,z3),meet(a,meet(z1,iPr_def_15))),
inference(superposition,[status(thm)],[c_1680,c_1934]) ).
tcf(c_23866,plain,
meet(join(iPr_def_13,iPr_def_14),join(z3,meet(a,meet(z1,iPr_def_14)))) = join(meet(iPr_def_14,z3),meet(a,meet(z1,join(iPr_def_11,z3)))),
inference(superposition,[status(thm)],[c_3680,c_1934]) ).
tcf(c_23893,plain,
meet(join(iPr_def_13,z2),join(z3,meet(a,meet(z1,z2)))) = join(meet(z2,z3),meet(iPr_def_15,meet(a,z1))),
inference(theory_normalisation,[status(thm)],[c_23861,c_129,c_130,c_127,c_128]) ).
tcf(c_23894,plain,
meet(join(iPr_def_11,z3),join(iPr_def_13,z2)) = join(iPr_def_17,meet(z2,z3)),
inference(demodulation,[status(thm)],[c_23893,c_130,c_128,c_1687,c_1695,c_1699,c_7039]) ).
tcf(c_23903,plain,
meet(join(iPr_def_13,iPr_def_14),join(z3,meet(iPr_def_14,meet(a,z1)))) = join(meet(iPr_def_14,z3),meet(a,meet(z1,join(iPr_def_11,z3)))),
inference(theory_normalisation,[status(thm)],[c_23866,c_129,c_130,c_127,c_128]) ).
tcf(c_23904,plain,
join(meet(iPr_def_14,z3),meet(a,meet(z1,join(iPr_def_11,z3)))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_23903,c_128,c_1821,c_3744,c_3680,c_3707,c_3828]) ).
tcf(c_26381,plain,
join(iPr_def_11,join(z3,join(iPr_def_17,meet(z2,z3)))) = join(iPr_def_11,z3),
inference(superposition,[status(thm)],[c_23894,c_1705]) ).
tcf(c_26388,plain,
join(iPr_def_11,join(iPr_def_17,join(z3,meet(z2,z3)))) = join(iPr_def_11,z3),
inference(theory_normalisation,[status(thm)],[c_26381,c_129,c_130,c_127,c_128]) ).
tcf(c_26389,plain,
join(iPr_def_11,z3) = join(iPr_def_17,z3),
inference(demodulation,[status(thm)],[c_26388,c_1734,c_18394]) ).
tcf(c_26534,plain,
meet(iPr_def_17,join(iPr_def_11,z3)) = iPr_def_17,
inference(superposition,[status(thm)],[c_26389,c_125]) ).
tcf(c_27034,plain,
meet(a,meet(meet(z1,join(iPr_def_11,z3)),iPr_def_14)) = meet(a,meet(z1,join(iPr_def_11,z3))),
inference(superposition,[status(thm)],[c_23904,c_1777]) ).
tcf(c_27049,plain,
meet(iPr_def_14,meet(a,meet(z1,join(iPr_def_11,z3)))) = meet(a,meet(z1,join(iPr_def_11,z3))),
inference(theory_normalisation,[status(thm)],[c_27034,c_129,c_130,c_127,c_128]) ).
tcf(c_27050,plain,
meet(a,meet(z1,join(iPr_def_11,z3))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_27049,c_3744,c_3725,c_3828]) ).
tcf(c_27130,plain,
meet(iPr_def_17,meet(z1,join(iPr_def_11,z3))) = meet(iPr_def_16,iPr_def_14),
inference(superposition,[status(thm)],[c_27050,c_1767]) ).
tcf(c_27154,plain,
meet(iPr_def_17,meet(z1,join(iPr_def_11,z3))) = meet(iPr_def_14,iPr_def_16),
inference(theory_normalisation,[status(thm)],[c_27130,c_129,c_130,c_127,c_128]) ).
tcf(c_27155,plain,
meet(iPr_def_17,meet(z1,join(iPr_def_11,z3))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_27154,c_7326]) ).
tcf(c_27156,plain,
meet(join(iPr_def_11,z3),iPr_def_17) = iPr_def_14,
inference(ac_demodulation,[status(thm)],[c_27155,c_2842,c_129,c_130,c_127,c_128]) ).
tcf(c_27212,plain,
meet(iPr_def_17,join(iPr_def_11,z3)) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_27156,c_129,c_130,c_127,c_128]) ).
tcf(c_27244,plain,
iPr_def_14 = iPr_def_17,
inference(superposition,[status(thm)],[c_27212,c_26534]) ).
tcf(c_27903,plain,
iPr_def_14 != iPr_def_14,
inference(demodulation,[status(thm)],[c_116,c_27244]) ).
tcf(c_27905,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_27903]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT399-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 21:35:04 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.40 Running UEQ theorem proving
% 0.03/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.41
% 0.03/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.03/0.41
% 0.03/0.41 % Detected problem language: tptp
% 0.03/0.43 % Proving...
% 108.91/26.99 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 108.91/26.99 % SZS status Started for theBenchmark.p
% 108.91/26.99 % SZS status Unsatisfiable for theBenchmark.p
% 108.91/26.99
% 108.91/26.99 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 108.91/26.99
% 108.91/26.99 % ------ iProver source info
% 108.91/26.99
% 108.91/26.99 % git: date: 2026-07-19 20:42:38 +0200
% 108.91/26.99 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 108.91/26.99 % git: non_committed_changes: false
% 108.91/26.99
% 108.91/26.99 % ------ Parsing...% successful
% 108.91/26.99
% 108.91/26.99
% 108.91/26.99 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 108.91/26.99
% 108.91/26.99 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 108.91/26.99
% 108.91/26.99 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 108.91/26.99
% 108.91/26.99 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 108.91/26.99 % ------ Proving...
% 108.91/26.99 % ------ Problem Properties
% 108.91/26.99
% 108.91/26.99 %
% 108.91/26.99 % clauses 24
% 108.91/26.99 % conjectures 2
% 108.91/26.99 % EPR 9
% 108.91/26.99 % Horn 24
% 108.91/26.99 % unary 24
% 108.91/26.99 % binary 0
% 108.91/26.99 % lits 24
% 108.91/26.99 % lits eq 24
% 108.91/26.99 % fd_pure 0
% 108.91/26.99 % fd_pseudo 0
% 108.91/26.99 % fd_cond 0
% 108.91/26.99 % fd_pseudo_cond 0
% 108.91/26.99 % AC symbols 2
% 108.91/26.99
% 108.91/26.99 % ------ Input Options Time Limit: Unbounded
% 108.91/26.99
% 108.91/26.99
% 108.91/26.99 % ------
% 108.91/26.99 % Current options:
% 108.91/26.99 % ------
% 108.91/26.99
% 108.91/26.99
% 108.91/26.99 %
% 108.91/26.99
% 108.91/26.99 % ------ Proving...
% 108.91/26.99 %
% 108.91/26.99
% 108.91/26.99 % SZS status Unsatisfiable for theBenchmark.p
% 108.91/26.99
% 108.91/26.99 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 108.91/27.00
% 108.91/27.00
%------------------------------------------------------------------------------