%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT399-2 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n004.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 203.62s 30.98s
% Output : CNFRefutation 203.62s
% 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/sandbox/benchmark/theBenchmark.p',commutativity) ).
fof(f2,axiom,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity) ).
fof(f3,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_001) ).
fof(f4,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_002) ).
fof(f5,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption) ).
fof(f6,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption_003) ).
fof(f7,axiom,
! [X2,X0,X1] : upme(X0,X1,X2) = meet(X0,join(X1,X2)),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',definition_of_lome) ).
fof(f11,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/sandbox/benchmark/theBenchmark.p',conjecture) ).
fof(f12,negated_conjecture,
upme(meet(a,z1),z2,z3) != lome(meet(a,z1),z2,z3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture_1) ).
fof(f13,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,[],[f11,f7]) ).
fof(f14,plain,
meet(meet(a,z1),join(z2,z3)) != join(meet(meet(a,z1),z2),meet(meet(a,z1),z3)),
inference(definition_unfolding,[],[f12,f7,f8]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : meet(X0,X1) = meet(X1,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[],[f3]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i] : join(X0,meet(X0,X1)) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] : meet(X0,join(X0,X1)) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_67,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,[],[f13]) ).
tcf(c_68,negated_conjecture,
join(meet(meet(a,z1),z2),meet(meet(a,z1),z3)) != meet(meet(a,z1),join(z2,z3)),
inference(cnf_transformation,[],[f14]) ).
tcf(c_76,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_67,c_64,c_63,c_62,c_61]) ).
tcf(c_77,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_68,c_64,c_63,c_62,c_61]) ).
tcf(c_99,definition,
iPr_def_10 = meet(z1,z2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_100,definition,
iPr_def_11 = meet(a,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_101,definition,
iPr_def_12 = meet(z1,z3),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_102,definition,
iPr_def_13 = meet(a,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_103,definition,
iPr_def_14 = join(iPr_def_11,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_104,definition,
iPr_def_15 = join(z2,z3),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_105,definition,
iPr_def_16 = meet(z1,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_106,definition,
iPr_def_17 = meet(a,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_107,negated_conjecture,
iPr_def_14 != iPr_def_17,
inference(demodulation,[status(thm)],[c_77,c_104,c_105,c_106,c_101,c_102,c_99,c_100,c_103]) ).
tcf(c_108,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_76]) ).
tcf(c_109,definition,
iPr_def_18 = join(z2,z3),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_110,definition,
iPr_def_19 = meet(z1,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_111,definition,
iPr_def_20 = meet(a,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_112,definition,
iPr_def_21 = meet(z1,z3),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_113,definition,
iPr_def_22 = meet(a,iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_114,definition,
iPr_def_23 = meet(z1,z2),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_115,definition,
iPr_def_24 = meet(a,iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_116,definition,
iPr_def_25 = join(iPr_def_11,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_117,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_108]) ).
tcf(c_118,negated_conjecture,
iPr_def_14 != iPr_def_17,
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_119,plain,
iPr_def_15 = iPr_def_18,
inference(demodulation,[status(thm)],[c_104,c_109]) ).
tcf(c_120,plain,
iPr_def_16 = iPr_def_19,
inference(demodulation,[status(thm)],[c_105,c_110]) ).
tcf(c_121,plain,
iPr_def_17 = iPr_def_20,
inference(demodulation,[status(thm)],[c_106,c_111]) ).
tcf(c_122,plain,
iPr_def_12 = iPr_def_21,
inference(demodulation,[status(thm)],[c_101,c_112]) ).
tcf(c_123,plain,
iPr_def_13 = iPr_def_22,
inference(demodulation,[status(thm)],[c_102,c_113]) ).
tcf(c_124,plain,
iPr_def_10 = iPr_def_23,
inference(demodulation,[status(thm)],[c_99,c_114]) ).
tcf(c_125,plain,
iPr_def_11 = iPr_def_24,
inference(demodulation,[status(thm)],[c_100,c_115]) ).
tcf(c_126,plain,
iPr_def_14 = iPr_def_25,
inference(demodulation,[status(thm)],[c_103,c_116]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i] : meet(X0,join(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] : join(X0,meet(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i,X2: $i] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] : join(X0,X1) = join(X1,X0),
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_131,plain,
! [X0: $i,X1: $i,X2: $i] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
inference(demodulation,[status(thm)],[c_62]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] : meet(X0,X1) = meet(X1,X0),
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_222,plain,
meet(a,iPr_def_12) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_113,c_123]) ).
tcf(c_223,plain,
meet(iPr_def_12,a) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_222,c_131,c_132,c_129,c_130]) ).
tcf(c_266,plain,
! [X0: $i,X1: $i] : join(X0,meet(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_132,c_128]) ).
tcf(c_300,plain,
! [X0: $i] : meet(iPr_def_12,meet(a,X0)) = meet(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_223,c_131]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,meet(X1,meet(X2,X0))) = X0,
inference(superposition,[status(thm)],[c_131,c_266]) ).
tcf(c_1654,plain,
! [X0: $i] : meet(X0,X0) = X0,
inference(superposition,[status(thm)],[c_128,c_127]) ).
tcf(c_1655,plain,
join(z2,z3) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_109,c_119]) ).
tcf(c_1656,plain,
meet(z2,iPr_def_15) = z2,
inference(superposition,[status(thm)],[c_1655,c_127]) ).
tcf(c_1657,plain,
meet(z1,iPr_def_15) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_110,c_120]) ).
tcf(c_1658,plain,
meet(iPr_def_15,z1) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_1657,c_131,c_132,c_129,c_130]) ).
tcf(c_1659,plain,
join(iPr_def_15,iPr_def_16) = iPr_def_15,
inference(superposition,[status(thm)],[c_1658,c_128]) ).
tcf(c_1660,plain,
meet(iPr_def_15,z2) = z2,
inference(theory_normalisation,[status(thm)],[c_1656,c_131,c_132,c_129,c_130]) ).
tcf(c_1661,plain,
meet(a,iPr_def_16) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_111,c_121]) ).
tcf(c_1662,plain,
meet(iPr_def_16,a) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_1661,c_131,c_132,c_129,c_130]) ).
tcf(c_1663,plain,
join(iPr_def_16,iPr_def_17) = iPr_def_16,
inference(superposition,[status(thm)],[c_1662,c_128]) ).
tcf(c_1664,plain,
meet(z1,z3) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_112,c_122]) ).
tcf(c_1665,plain,
join(z1,iPr_def_12) = z1,
inference(superposition,[status(thm)],[c_1664,c_128]) ).
tcf(c_1666,plain,
join(iPr_def_12,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_1665,c_131,c_132,c_129,c_130]) ).
tcf(c_1667,plain,
meet(a,iPr_def_12) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_113,c_123]) ).
tcf(c_1668,plain,
meet(iPr_def_12,a) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_1667,c_131,c_132,c_129,c_130]) ).
tcf(c_1669,plain,
join(iPr_def_12,iPr_def_13) = iPr_def_12,
inference(superposition,[status(thm)],[c_1668,c_128]) ).
tcf(c_1670,plain,
meet(z1,z2) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_114,c_124]) ).
tcf(c_1671,plain,
join(z1,iPr_def_10) = z1,
inference(superposition,[status(thm)],[c_1670,c_128]) ).
tcf(c_1672,plain,
join(iPr_def_10,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_1671,c_131,c_132,c_129,c_130]) ).
tcf(c_1673,plain,
meet(a,iPr_def_10) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_115,c_125]) ).
tcf(c_1674,plain,
meet(iPr_def_10,a) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_1673,c_131,c_132,c_129,c_130]) ).
tcf(c_1675,plain,
join(iPr_def_10,iPr_def_11) = iPr_def_10,
inference(superposition,[status(thm)],[c_1674,c_128]) ).
tcf(c_1678,plain,
! [X0: $i] : join(z2,join(z3,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_1655,c_129]) ).
tcf(c_1680,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(X1,meet(join(X0,X1),X2))) = join(X0,X1),
inference(superposition,[status(thm)],[c_129,c_128]) ).
tcf(c_1681,plain,
join(iPr_def_11,iPr_def_13) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_116,c_126]) ).
tcf(c_1682,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_13,X0)) = join(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_1681,c_129]) ).
tcf(c_1684,plain,
! [X0: $i] : join(iPr_def_15,join(iPr_def_16,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_1659,c_129]) ).
tcf(c_1686,plain,
join(iPr_def_15,z2) = iPr_def_15,
inference(superposition,[status(thm)],[c_1660,c_128]) ).
tcf(c_1695,plain,
meet(iPr_def_12,z1) = iPr_def_12,
inference(superposition,[status(thm)],[c_1666,c_127]) ).
tcf(c_1698,plain,
! [X0: $i,X1: $i] : meet(X0,join(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_130,c_127]) ).
tcf(c_1700,plain,
! [X0: $i] : join(iPr_def_10,join(z1,X0)) = join(z1,X0),
inference(superposition,[status(thm)],[c_1672,c_129]) ).
tcf(c_1701,plain,
meet(iPr_def_10,z1) = iPr_def_10,
inference(superposition,[status(thm)],[c_1672,c_127]) ).
tcf(c_1705,plain,
! [X0: $i] : join(iPr_def_15,join(z2,X0)) = join(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_1686,c_129]) ).
tcf(c_1709,plain,
! [X0: $i,X1: $i] : join(X0,meet(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_132,c_128]) ).
tcf(c_1713,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,join(X1,join(X2,X0))) = X0,
inference(superposition,[status(thm)],[c_129,c_1698]) ).
tcf(c_1716,plain,
meet(iPr_def_13,iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_1681,c_1698]) ).
tcf(c_1718,plain,
meet(iPr_def_16,iPr_def_15) = iPr_def_16,
inference(superposition,[status(thm)],[c_1659,c_1698]) ).
tcf(c_1719,plain,
meet(iPr_def_17,iPr_def_16) = iPr_def_17,
inference(superposition,[status(thm)],[c_1663,c_1698]) ).
tcf(c_1721,plain,
meet(iPr_def_13,iPr_def_12) = iPr_def_13,
inference(superposition,[status(thm)],[c_1669,c_1698]) ).
tcf(c_1723,plain,
meet(iPr_def_11,iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_1675,c_1698]) ).
tcf(c_1727,plain,
meet(iPr_def_10,iPr_def_11) = iPr_def_11,
inference(theory_normalisation,[status(thm)],[c_1723,c_131,c_132,c_129,c_130]) ).
tcf(c_1728,plain,
meet(iPr_def_12,iPr_def_13) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_1721,c_131,c_132,c_129,c_130]) ).
tcf(c_1729,plain,
meet(iPr_def_16,iPr_def_17) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_1719,c_131,c_132,c_129,c_130]) ).
tcf(c_1730,plain,
meet(iPr_def_15,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_1718,c_131,c_132,c_129,c_130]) ).
tcf(c_1740,plain,
! [X0: $i] : meet(iPr_def_15,meet(z1,X0)) = meet(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_1658,c_131]) ).
tcf(c_1742,plain,
! [X0: $i] : meet(iPr_def_16,meet(a,X0)) = meet(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_1662,c_131]) ).
tcf(c_1744,plain,
! [X0: $i] : meet(iPr_def_10,meet(a,X0)) = meet(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_1674,c_131]) ).
tcf(c_1752,plain,
! [X0: $i,X1: $i,X2: $i] : meet(X0,meet(X1,join(X2,meet(X0,X1)))) = meet(X0,X1),
inference(superposition,[status(thm)],[c_131,c_1698]) ).
tcf(c_1761,plain,
! [X0: $i] : meet(iPr_def_15,meet(iPr_def_16,X0)) = meet(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_1730,c_131]) ).
tcf(c_1774,plain,
join(z2,iPr_def_10) = z2,
inference(superposition,[status(thm)],[c_1670,c_1709]) ).
tcf(c_1775,plain,
join(z3,iPr_def_12) = z3,
inference(superposition,[status(thm)],[c_1664,c_1709]) ).
tcf(c_1777,plain,
join(z1,iPr_def_16) = z1,
inference(superposition,[status(thm)],[c_1658,c_1709]) ).
tcf(c_1780,plain,
join(a,iPr_def_13) = a,
inference(superposition,[status(thm)],[c_1668,c_1709]) ).
tcf(c_1781,plain,
join(a,iPr_def_11) = a,
inference(superposition,[status(thm)],[c_1674,c_1709]) ).
tcf(c_1786,plain,
join(iPr_def_14,iPr_def_13) = iPr_def_14,
inference(superposition,[status(thm)],[c_1716,c_1709]) ).
tcf(c_1792,plain,
! [X0: $i,X1: $i,X2: $i] : join(X0,join(meet(X1,X0),X2)) = join(X0,X2),
inference(superposition,[status(thm)],[c_1709,c_129]) ).
tcf(c_1796,plain,
join(iPr_def_13,iPr_def_14) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_1786,c_131,c_132,c_129,c_130]) ).
tcf(c_1800,plain,
join(iPr_def_11,a) = a,
inference(theory_normalisation,[status(thm)],[c_1781,c_131,c_132,c_129,c_130]) ).
tcf(c_1801,plain,
join(iPr_def_13,a) = a,
inference(theory_normalisation,[status(thm)],[c_1780,c_131,c_132,c_129,c_130]) ).
tcf(c_1803,plain,
join(iPr_def_16,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_1777,c_131,c_132,c_129,c_130]) ).
tcf(c_1804,plain,
join(iPr_def_12,z3) = z3,
inference(theory_normalisation,[status(thm)],[c_1775,c_131,c_132,c_129,c_130]) ).
tcf(c_1805,plain,
join(iPr_def_10,z2) = z2,
inference(theory_normalisation,[status(thm)],[c_1774,c_131,c_132,c_129,c_130]) ).
tcf(c_1829,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_1674,c_117]) ).
tcf(c_1851,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_1664,c_117]) ).
tcf(c_1866,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_1730,c_117]) ).
tcf(c_1878,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_1866,c_131,c_132,c_129,c_130]) ).
tcf(c_1879,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_1878,c_1662]) ).
tcf(c_1908,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_1851,c_131,c_132,c_129,c_130]) ).
tcf(c_1909,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_1908,c_1668]) ).
tcf(c_1932,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_1829,c_131,c_132,c_129,c_130]) ).
tcf(c_1933,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_1932,c_132,c_1744,c_329]) ).
tcf(c_1988,plain,
meet(iPr_def_11,a) = iPr_def_11,
inference(superposition,[status(thm)],[c_1800,c_127]) ).
tcf(c_1993,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_1933,c_1988]) ).
tcf(c_2013,plain,
meet(iPr_def_16,z1) = iPr_def_16,
inference(superposition,[status(thm)],[c_1803,c_127]) ).
tcf(c_2016,plain,
meet(iPr_def_12,z3) = iPr_def_12,
inference(superposition,[status(thm)],[c_1804,c_127]) ).
tcf(c_2018,plain,
! [X0: $i] : join(iPr_def_10,join(z2,X0)) = join(z2,X0),
inference(superposition,[status(thm)],[c_1805,c_129]) ).
tcf(c_2019,plain,
meet(iPr_def_10,z2) = iPr_def_10,
inference(superposition,[status(thm)],[c_1805,c_127]) ).
tcf(c_2022,plain,
! [X0: $i] : meet(iPr_def_12,meet(X0,a)) = meet(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_132,c_300]) ).
tcf(c_2047,plain,
! [X0: $i] : meet(iPr_def_11,meet(a,X0)) = meet(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_1988,c_131]) ).
tcf(c_2173,plain,
! [X0: $i] : join(z1,meet(X0,iPr_def_12)) = z1,
inference(superposition,[status(thm)],[c_1695,c_329]) ).
tcf(c_2175,plain,
! [X0: $i] : join(z1,meet(X0,iPr_def_10)) = z1,
inference(superposition,[status(thm)],[c_1701,c_329]) ).
tcf(c_2187,plain,
! [X0: $i] : join(z1,meet(X0,iPr_def_16)) = z1,
inference(superposition,[status(thm)],[c_2013,c_329]) ).
tcf(c_2188,plain,
! [X0: $i] : join(z3,meet(X0,iPr_def_12)) = z3,
inference(superposition,[status(thm)],[c_2016,c_329]) ).
tcf(c_2189,plain,
! [X0: $i] : join(z2,meet(X0,iPr_def_10)) = z2,
inference(superposition,[status(thm)],[c_2019,c_329]) ).
tcf(c_2268,plain,
! [X0: $i] : join(z1,meet(iPr_def_12,X0)) = z1,
inference(superposition,[status(thm)],[c_132,c_2173]) ).
tcf(c_2278,plain,
! [X0: $i] : join(z1,meet(iPr_def_10,X0)) = z1,
inference(superposition,[status(thm)],[c_132,c_2175]) ).
tcf(c_2419,plain,
! [X0: $i] : join(z1,meet(iPr_def_16,X0)) = z1,
inference(superposition,[status(thm)],[c_132,c_2187]) ).
tcf(c_2430,plain,
! [X0: $i] : join(z3,meet(iPr_def_12,X0)) = z3,
inference(superposition,[status(thm)],[c_132,c_2188]) ).
tcf(c_2440,plain,
! [X0: $i] : join(z2,meet(iPr_def_10,X0)) = z2,
inference(superposition,[status(thm)],[c_132,c_2189]) ).
tcf(c_2474,plain,
join(z1,iPr_def_13) = z1,
inference(superposition,[status(thm)],[c_1728,c_2268]) ).
tcf(c_2481,plain,
join(iPr_def_13,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_2474,c_131,c_132,c_129,c_130]) ).
tcf(c_2611,plain,
join(z1,iPr_def_11) = z1,
inference(superposition,[status(thm)],[c_1727,c_2278]) ).
tcf(c_2619,plain,
join(iPr_def_11,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_2611,c_131,c_132,c_129,c_130]) ).
tcf(c_2728,plain,
join(z1,iPr_def_17) = z1,
inference(superposition,[status(thm)],[c_1729,c_2419]) ).
tcf(c_2736,plain,
join(iPr_def_17,z1) = z1,
inference(theory_normalisation,[status(thm)],[c_2728,c_131,c_132,c_129,c_130]) ).
tcf(c_2817,plain,
meet(iPr_def_17,z1) = iPr_def_17,
inference(superposition,[status(thm)],[c_2736,c_127]) ).
tcf(c_2851,plain,
join(z3,iPr_def_13) = z3,
inference(superposition,[status(thm)],[c_1728,c_2430]) ).
tcf(c_2860,plain,
join(iPr_def_13,z3) = z3,
inference(theory_normalisation,[status(thm)],[c_2851,c_131,c_132,c_129,c_130]) ).
tcf(c_2898,plain,
join(z2,iPr_def_11) = z2,
inference(superposition,[status(thm)],[c_1727,c_2440]) ).
tcf(c_2906,plain,
join(iPr_def_11,z2) = z2,
inference(theory_normalisation,[status(thm)],[c_2898,c_131,c_132,c_129,c_130]) ).
tcf(c_2909,plain,
meet(iPr_def_11,z2) = iPr_def_11,
inference(superposition,[status(thm)],[c_2906,c_127]) ).
tcf(c_2923,plain,
! [X0: $i] : join(z2,meet(X0,iPr_def_11)) = z2,
inference(superposition,[status(thm)],[c_2909,c_329]) ).
tcf(c_2945,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_12,X0)) = join(z2,z3),
inference(superposition,[status(thm)],[c_2430,c_1678]) ).
tcf(c_2951,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_12,X0)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_2945,c_1655]) ).
tcf(c_3058,plain,
! [X0: $i] : join(z2,meet(iPr_def_11,X0)) = z2,
inference(superposition,[status(thm)],[c_132,c_2923]) ).
tcf(c_3271,plain,
join(iPr_def_15,iPr_def_12) = iPr_def_15,
inference(superposition,[status(thm)],[c_2016,c_2951]) ).
tcf(c_3281,plain,
join(iPr_def_12,iPr_def_15) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_3271,c_131,c_132,c_129,c_130]) ).
tcf(c_3287,plain,
meet(iPr_def_12,iPr_def_15) = iPr_def_12,
inference(superposition,[status(thm)],[c_3281,c_127]) ).
tcf(c_3653,plain,
join(iPr_def_11,a) = join(iPr_def_14,a),
inference(superposition,[status(thm)],[c_1801,c_1682]) ).
tcf(c_3654,plain,
join(iPr_def_11,z1) = join(iPr_def_14,z1),
inference(superposition,[status(thm)],[c_2481,c_1682]) ).
tcf(c_3655,plain,
join(iPr_def_11,z3) = join(iPr_def_14,z3),
inference(superposition,[status(thm)],[c_2860,c_1682]) ).
tcf(c_3667,plain,
join(iPr_def_14,z1) = z1,
inference(demodulation,[status(thm)],[c_3654,c_2619]) ).
tcf(c_3668,plain,
join(iPr_def_14,a) = a,
inference(demodulation,[status(thm)],[c_3653,c_1800]) ).
tcf(c_3682,plain,
meet(iPr_def_14,z1) = iPr_def_14,
inference(superposition,[status(thm)],[c_3667,c_127]) ).
tcf(c_3691,plain,
meet(iPr_def_14,a) = iPr_def_14,
inference(superposition,[status(thm)],[c_3668,c_127]) ).
tcf(c_3700,plain,
! [X0: $i] : meet(iPr_def_14,meet(z1,X0)) = meet(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_3682,c_131]) ).
tcf(c_3719,plain,
! [X0: $i] : meet(iPr_def_14,meet(a,X0)) = meet(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_3691,c_131]) ).
tcf(c_3803,plain,
meet(iPr_def_14,join(iPr_def_11,z3)) = iPr_def_14,
inference(superposition,[status(thm)],[c_3655,c_127]) ).
tcf(c_3816,plain,
join(iPr_def_15,iPr_def_16) = join(iPr_def_15,iPr_def_17),
inference(superposition,[status(thm)],[c_1663,c_1684]) ).
tcf(c_3832,plain,
join(iPr_def_15,iPr_def_17) = iPr_def_15,
inference(demodulation,[status(thm)],[c_3816,c_1659]) ).
tcf(c_3848,plain,
meet(iPr_def_17,iPr_def_15) = iPr_def_17,
inference(superposition,[status(thm)],[c_3832,c_1698]) ).
tcf(c_3854,plain,
meet(iPr_def_15,iPr_def_17) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_3848,c_131,c_132,c_129,c_130]) ).
tcf(c_4529,plain,
! [X0: $i] : meet(iPr_def_10,join(z1,X0)) = iPr_def_10,
inference(superposition,[status(thm)],[c_1700,c_127]) ).
tcf(c_4782,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_10,X0)) = join(iPr_def_15,z2),
inference(superposition,[status(thm)],[c_2440,c_1705]) ).
tcf(c_4783,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_11,X0)) = join(iPr_def_15,z2),
inference(superposition,[status(thm)],[c_3058,c_1705]) ).
tcf(c_4797,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_11,X0)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_4783,c_1686]) ).
tcf(c_4798,plain,
! [X0: $i] : join(iPr_def_15,meet(iPr_def_10,X0)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_4782,c_1686]) ).
tcf(c_4863,plain,
join(iPr_def_15,iPr_def_11) = iPr_def_15,
inference(superposition,[status(thm)],[c_1654,c_4797]) ).
tcf(c_4883,plain,
join(iPr_def_11,iPr_def_15) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_4863,c_131,c_132,c_129,c_130]) ).
tcf(c_4912,plain,
meet(iPr_def_11,iPr_def_15) = iPr_def_11,
inference(superposition,[status(thm)],[c_4883,c_127]) ).
tcf(c_4954,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_4912,c_117]) ).
tcf(c_4975,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_4954,c_131,c_132,c_129,c_130]) ).
tcf(c_4976,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_4975,c_132,c_1988,c_2047,c_4797]) ).
tcf(c_4988,plain,
join(iPr_def_15,iPr_def_10) = iPr_def_15,
inference(superposition,[status(thm)],[c_4529,c_4798]) ).
tcf(c_5002,plain,
join(iPr_def_10,iPr_def_15) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_4988,c_131,c_132,c_129,c_130]) ).
tcf(c_5040,plain,
! [X0: $i] : meet(iPr_def_13,join(X0,iPr_def_12)) = iPr_def_13,
inference(superposition,[status(thm)],[c_1669,c_1713]) ).
tcf(c_5042,plain,
! [X0: $i] : meet(iPr_def_11,join(X0,iPr_def_10)) = iPr_def_11,
inference(superposition,[status(thm)],[c_1675,c_1713]) ).
tcf(c_5269,plain,
meet(iPr_def_10,iPr_def_15) = iPr_def_10,
inference(superposition,[status(thm)],[c_5002,c_127]) ).
tcf(c_5715,plain,
! [X0: $i] : meet(iPr_def_13,join(iPr_def_12,X0)) = iPr_def_13,
inference(superposition,[status(thm)],[c_130,c_5040]) ).
tcf(c_5748,plain,
! [X0: $i] : meet(iPr_def_11,join(iPr_def_10,X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_130,c_5042]) ).
tcf(c_7015,plain,
! [X0: $i] : meet(iPr_def_15,meet(X0,z1)) = meet(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_132,c_1740]) ).
tcf(c_7019,plain,
meet(iPr_def_15,iPr_def_10) = meet(iPr_def_16,z2),
inference(superposition,[status(thm)],[c_1670,c_1740]) ).
tcf(c_7020,plain,
meet(iPr_def_15,iPr_def_12) = meet(iPr_def_16,z3),
inference(superposition,[status(thm)],[c_1664,c_1740]) ).
tcf(c_7040,plain,
meet(iPr_def_12,iPr_def_15) = meet(iPr_def_16,z3),
inference(theory_normalisation,[status(thm)],[c_7020,c_131,c_132,c_129,c_130]) ).
tcf(c_7041,plain,
meet(iPr_def_16,z3) = iPr_def_12,
inference(demodulation,[status(thm)],[c_7040,c_3287]) ).
tcf(c_7042,plain,
meet(iPr_def_10,iPr_def_15) = meet(iPr_def_16,z2),
inference(theory_normalisation,[status(thm)],[c_7019,c_131,c_132,c_129,c_130]) ).
tcf(c_7043,plain,
meet(iPr_def_16,z2) = iPr_def_10,
inference(demodulation,[status(thm)],[c_7042,c_5269]) ).
tcf(c_7064,plain,
join(iPr_def_16,iPr_def_12) = iPr_def_16,
inference(superposition,[status(thm)],[c_7041,c_128]) ).
tcf(c_7076,plain,
join(iPr_def_12,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_7064,c_131,c_132,c_129,c_130]) ).
tcf(c_7087,plain,
join(iPr_def_16,iPr_def_10) = iPr_def_16,
inference(superposition,[status(thm)],[c_7043,c_128]) ).
tcf(c_7099,plain,
join(iPr_def_10,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_7087,c_131,c_132,c_129,c_130]) ).
tcf(c_7117,plain,
meet(iPr_def_13,iPr_def_16) = iPr_def_13,
inference(superposition,[status(thm)],[c_7076,c_5715]) ).
tcf(c_7180,plain,
meet(iPr_def_11,iPr_def_16) = iPr_def_11,
inference(superposition,[status(thm)],[c_7099,c_5748]) ).
tcf(c_7211,plain,
join(iPr_def_16,iPr_def_13) = iPr_def_16,
inference(superposition,[status(thm)],[c_7117,c_1709]) ).
tcf(c_7229,plain,
join(iPr_def_13,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_7211,c_131,c_132,c_129,c_130]) ).
tcf(c_7243,plain,
join(iPr_def_16,iPr_def_11) = iPr_def_16,
inference(superposition,[status(thm)],[c_7180,c_1709]) ).
tcf(c_7255,plain,
! [X0: $i] : join(iPr_def_16,meet(X0,iPr_def_11)) = iPr_def_16,
inference(superposition,[status(thm)],[c_7180,c_329]) ).
tcf(c_7261,plain,
join(iPr_def_11,iPr_def_16) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_7243,c_131,c_132,c_129,c_130]) ).
tcf(c_7280,plain,
join(iPr_def_11,iPr_def_16) = join(iPr_def_14,iPr_def_16),
inference(superposition,[status(thm)],[c_7229,c_1682]) ).
tcf(c_7283,plain,
join(iPr_def_14,iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_7280,c_7261]) ).
tcf(c_7302,plain,
meet(iPr_def_14,iPr_def_16) = iPr_def_14,
inference(superposition,[status(thm)],[c_7283,c_127]) ).
tcf(c_7369,plain,
! [X0: $i] : join(iPr_def_16,meet(X0,iPr_def_14)) = iPr_def_16,
inference(superposition,[status(thm)],[c_7302,c_329]) ).
tcf(c_7531,plain,
! [X0: $i] : join(iPr_def_16,meet(iPr_def_11,X0)) = iPr_def_16,
inference(superposition,[status(thm)],[c_132,c_7255]) ).
tcf(c_7590,plain,
! [X0: $i] : meet(iPr_def_11,join(a,X0)) = meet(iPr_def_10,a),
inference(superposition,[status(thm)],[c_127,c_1744]) ).
tcf(c_7612,plain,
! [X0: $i] : meet(iPr_def_11,join(a,X0)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7590,c_1674]) ).
tcf(c_7627,plain,
! [X0: $i] : meet(a,join(iPr_def_11,X0)) = join(meet(a,X0),iPr_def_11),
inference(demodulation,[status(thm)],[c_1993,c_7612]) ).
tcf(c_7628,plain,
! [X0: $i] : meet(a,join(iPr_def_11,X0)) = join(iPr_def_11,meet(a,X0)),
inference(theory_normalisation,[status(thm)],[c_7627,c_131,c_132,c_129,c_130]) ).
tcf(c_7676,plain,
! [X0: $i] : join(iPr_def_16,meet(iPr_def_14,X0)) = iPr_def_16,
inference(superposition,[status(thm)],[c_132,c_7369]) ).
tcf(c_10538,plain,
! [X0: $i] : join(iPr_def_16,join(iPr_def_11,X0)) = join(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_7180,c_1792]) ).
tcf(c_10632,plain,
! [X0: $i] : join(iPr_def_11,join(X0,iPr_def_16)) = join(iPr_def_16,X0),
inference(theory_normalisation,[status(thm)],[c_10538,c_131,c_132,c_129,c_130]) ).
tcf(c_13154,plain,
! [X0: $i] : meet(iPr_def_11,join(z2,X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_2018,c_5748]) ).
tcf(c_14232,plain,
! [X0: $i] : meet(iPr_def_11,join(iPr_def_15,X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_1678,c_13154]) ).
tcf(c_14307,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_4976,c_14232]) ).
tcf(c_14310,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_14307,c_131,c_132,c_129,c_130]) ).
tcf(c_15552,plain,
meet(iPr_def_12,iPr_def_17) = meet(iPr_def_13,iPr_def_16),
inference(superposition,[status(thm)],[c_1662,c_2022]) ).
tcf(c_15597,plain,
meet(iPr_def_12,iPr_def_17) = iPr_def_13,
inference(demodulation,[status(thm)],[c_15552,c_7117]) ).
tcf(c_15707,plain,
join(iPr_def_17,iPr_def_13) = iPr_def_17,
inference(superposition,[status(thm)],[c_15597,c_1709]) ).
tcf(c_15729,plain,
join(iPr_def_13,iPr_def_17) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_15707,c_131,c_132,c_129,c_130]) ).
tcf(c_15762,plain,
join(iPr_def_11,iPr_def_17) = join(iPr_def_14,iPr_def_17),
inference(superposition,[status(thm)],[c_15729,c_1682]) ).
tcf(c_17979,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_7180,c_1879]) ).
tcf(c_17992,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_7283,c_1879]) ).
tcf(c_18013,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_17992,c_131,c_132,c_129,c_130]) ).
tcf(c_18014,plain,
meet(iPr_def_16,join(iPr_def_11,iPr_def_17)) = join(iPr_def_11,iPr_def_17),
inference(demodulation,[status(thm)],[c_18013,c_132,c_1662,c_1761,c_7302,c_7676,c_15762]) ).
tcf(c_18027,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_17979,c_131,c_132,c_129,c_130]) ).
tcf(c_18028,plain,
meet(iPr_def_16,join(iPr_def_11,iPr_def_17)) = iPr_def_17,
inference(demodulation,[status(thm)],[c_18027,c_132,c_130,c_1662,c_3854,c_7261,c_7531,c_7628,c_10632,c_14310]) ).
tcf(c_18131,plain,
join(iPr_def_11,iPr_def_17) = iPr_def_17,
inference(superposition,[status(thm)],[c_18014,c_18028]) ).
tcf(c_18234,plain,
! [X0: $i] : join(iPr_def_11,join(iPr_def_17,X0)) = join(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_18131,c_129]) ).
tcf(c_23871,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_1655,c_1909]) ).
tcf(c_23876,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_3655,c_1909]) ).
tcf(c_23903,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_23871,c_131,c_132,c_129,c_130]) ).
tcf(c_23904,plain,
meet(join(iPr_def_11,z3),join(iPr_def_13,z2)) = join(iPr_def_17,meet(z2,z3)),
inference(demodulation,[status(thm)],[c_23903,c_132,c_130,c_1662,c_1670,c_1674,c_7015]) ).
tcf(c_23913,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_23876,c_131,c_132,c_129,c_130]) ).
tcf(c_23914,plain,
join(meet(iPr_def_14,z3),meet(a,meet(z1,join(iPr_def_11,z3)))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_23913,c_130,c_1796,c_3719,c_3655,c_3682,c_3803]) ).
tcf(c_26427,plain,
join(iPr_def_11,join(z3,join(iPr_def_17,meet(z2,z3)))) = join(iPr_def_11,z3),
inference(superposition,[status(thm)],[c_23904,c_1680]) ).
tcf(c_26434,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_26427,c_131,c_132,c_129,c_130]) ).
tcf(c_26435,plain,
join(iPr_def_11,z3) = join(iPr_def_17,z3),
inference(demodulation,[status(thm)],[c_26434,c_1709,c_18234]) ).
tcf(c_26580,plain,
meet(iPr_def_17,join(iPr_def_11,z3)) = iPr_def_17,
inference(superposition,[status(thm)],[c_26435,c_127]) ).
tcf(c_27081,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_23914,c_1752]) ).
tcf(c_27096,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_27081,c_131,c_132,c_129,c_130]) ).
tcf(c_27097,plain,
meet(a,meet(z1,join(iPr_def_11,z3))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_27096,c_3719,c_3700,c_3803]) ).
tcf(c_27396,plain,
meet(iPr_def_17,meet(z1,join(iPr_def_11,z3))) = meet(iPr_def_16,iPr_def_14),
inference(superposition,[status(thm)],[c_27097,c_1742]) ).
tcf(c_27420,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_27396,c_131,c_132,c_129,c_130]) ).
tcf(c_27421,plain,
meet(iPr_def_17,meet(z1,join(iPr_def_11,z3))) = iPr_def_14,
inference(demodulation,[status(thm)],[c_27420,c_7302]) ).
tcf(c_27422,plain,
meet(join(iPr_def_11,z3),iPr_def_17) = iPr_def_14,
inference(ac_demodulation,[status(thm)],[c_27421,c_2817,c_131,c_132,c_129,c_130]) ).
tcf(c_27478,plain,
meet(iPr_def_17,join(iPr_def_11,z3)) = iPr_def_14,
inference(theory_normalisation,[status(thm)],[c_27422,c_131,c_132,c_129,c_130]) ).
tcf(c_27510,plain,
iPr_def_14 = iPr_def_17,
inference(superposition,[status(thm)],[c_27478,c_26580]) ).
tcf(c_28175,plain,
iPr_def_14 != iPr_def_14,
inference(demodulation,[status(thm)],[c_118,c_27510]) ).
tcf(c_28177,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_28175]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT399-2 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n004.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 21:33:07 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/0.42 Running UEQ theorem proving
% 0.16/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43
% 0.16/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.16/0.43
% 0.16/0.43 % Detected problem language: tptp
% 0.16/0.44 % Proving...
% 203.62/30.98 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 203.62/30.98 % SZS status Started for theBenchmark.p
% 203.62/30.98 % SZS status Unsatisfiable for theBenchmark.p
% 203.62/30.98
% 203.62/30.98 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 203.62/30.98
% 203.62/30.98 % ------ iProver source info
% 203.62/30.98
% 203.62/30.98 % git: date: 2026-07-19 20:42:38 +0200
% 203.62/30.98 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 203.62/30.98 % git: non_committed_changes: false
% 203.62/30.98
% 203.62/30.98 % ------ Parsing...% successful
% 203.62/30.98
% 203.62/30.98
% 203.62/30.98 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 203.62/30.98
% 203.62/30.98 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 203.62/30.98
% 203.62/30.98 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 203.62/30.98
% 203.62/30.98 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 203.62/30.98 % ------ Proving...
% 203.62/30.98 % ------ Problem Properties
% 203.62/30.98
% 203.62/30.98 %
% 203.62/30.98 % clauses 24
% 203.62/30.98 % conjectures 2
% 203.62/30.98 % EPR 9
% 203.62/30.98 % Horn 24
% 203.62/30.98 % unary 24
% 203.62/30.98 % binary 0
% 203.62/30.98 % lits 24
% 203.62/30.98 % lits eq 24
% 203.62/30.98 % fd_pure 0
% 203.62/30.98 % fd_pseudo 0
% 203.62/30.98 % fd_cond 0
% 203.62/30.98 % fd_pseudo_cond 0
% 203.62/30.98 % AC symbols 2
% 203.62/30.98
% 203.62/30.98 % ------ Input Options Time Limit: Unbounded
% 203.62/30.98
% 203.62/30.98
% 203.62/30.98 % ------
% 203.62/30.98 % Current options:
% 203.62/30.98 % ------
% 203.62/30.98
% 203.62/30.98
% 203.62/30.98 %
% 203.62/30.98
% 203.62/30.98 % ------ Proving...
% 203.62/30.98 %
% 203.62/30.98
% 203.62/30.98 % SZS status Unsatisfiable for theBenchmark.p
% 203.62/30.98
% 203.62/30.98 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 203.62/30.99
% 203.62/30.99
%------------------------------------------------------------------------------