%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LAT007-1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sun Jul 17 06:48:33 EDT 2022
% Result : Unsatisfiable 26.68s 26.91s
% Output : Refutation 26.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 3
% Syntax : Number of clauses : 193 ( 193 unt; 0 nHn; 193 RR)
% Number of literals : 193 ( 0 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(meet(u,join(u,v)),u),
file('LAT007-1.p',unknown),
[] ).
cnf(2,axiom,
equal(join(meet(u,v),meet(w,v)),meet(v,join(w,u))),
file('LAT007-1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(join(join(a,b),c),join(a,join(b,c))),
file('LAT007-1.p',unknown),
[] ).
cnf(5,plain,
equal(meet(meet(u,v),meet(v,join(w,u))),meet(u,v)),
inference(spr,[status(thm),theory(equality)],[2,1]),
[iquote('0:SpR:2.0,1.0')] ).
cnf(7,plain,
equal(meet(join(u,v),join(u,w)),join(meet(w,join(u,v)),u)),
inference(spr,[status(thm),theory(equality)],[1,2]),
[iquote('0:SpR:1.0,2.0')] ).
cnf(8,plain,
equal(meet(join(u,v),join(w,u)),join(u,meet(w,join(u,v)))),
inference(spr,[status(thm),theory(equality)],[1,2]),
[iquote('0:SpR:1.0,2.0')] ).
cnf(9,plain,
equal(meet(meet(u,join(v,w)),join(meet(w,u),x)),join(meet(x,meet(u,join(v,w))),meet(w,u))),
inference(spr,[status(thm),theory(equality)],[5,2]),
[iquote('0:SpR:5.0,2.0')] ).
cnf(10,plain,
equal(meet(meet(u,join(v,w)),join(x,meet(w,u))),join(meet(w,u),meet(x,meet(u,join(v,w))))),
inference(spr,[status(thm),theory(equality)],[5,2]),
[iquote('0:SpR:5.0,2.0')] ).
cnf(14,plain,
equal(meet(meet(u,v),v),meet(u,v)),
inference(spr,[status(thm),theory(equality)],[1,5]),
[iquote('0:SpR:1.0,5.0')] ).
cnf(20,plain,
equal(join(meet(u,join(v,w)),join(meet(w,join(v,x)),v)),meet(join(v,w),join(join(v,x),u))),
inference(spr,[status(thm),theory(equality)],[7,2]),
[iquote('0:SpR:7.0,2.0')] ).
cnf(26,plain,
equal(meet(u,join(meet(v,u),w)),join(meet(w,u),meet(v,u))),
inference(spr,[status(thm),theory(equality)],[14,2]),
[iquote('0:SpR:14.0,2.0')] ).
cnf(27,plain,
equal(meet(u,join(v,meet(w,u))),join(meet(w,u),meet(v,u))),
inference(spr,[status(thm),theory(equality)],[14,2]),
[iquote('0:SpR:14.0,2.0')] ).
cnf(34,plain,
equal(meet(u,join(meet(v,u),w)),meet(u,join(v,w))),
inference(rew,[status(thm),theory(equality)],[2,26]),
[iquote('0:Rew:2.0,26.0')] ).
cnf(35,plain,
equal(meet(u,join(v,meet(w,u))),meet(u,join(v,w))),
inference(rew,[status(thm),theory(equality)],[2,27]),
[iquote('0:Rew:2.0,27.0')] ).
cnf(48,plain,
equal(meet(u,meet(u,join(v,w))),meet(u,join(w,meet(v,u)))),
inference(spr,[status(thm),theory(equality)],[2,34]),
[iquote('0:SpR:2.0,34.0')] ).
cnf(49,plain,
equal(meet(u,meet(u,join(v,w))),meet(u,join(w,v))),
inference(rew,[status(thm),theory(equality)],[35,48]),
[iquote('0:Rew:35.0,48.0')] ).
cnf(59,plain,
equal(meet(join(u,meet(v,w)),join(meet(w,join(u,v)),x)),meet(join(u,meet(v,w)),join(w,x))),
inference(spr,[status(thm),theory(equality)],[35,34]),
[iquote('0:SpR:35.0,34.0')] ).
cnf(80,plain,
equal(meet(u,join(v,u)),meet(u,u)),
inference(spr,[status(thm),theory(equality)],[1,49]),
[iquote('0:SpR:1.0,49.0')] ).
cnf(88,plain,
equal(join(u,meet(join(u,v),join(u,v))),join(u,v)),
inference(spr,[status(thm),theory(equality)],[8,1]),
[iquote('0:SpR:8.0,1.0')] ).
cnf(94,plain,
equal(join(meet(u,join(v,w)),join(w,meet(v,join(w,x)))),meet(join(v,w),join(join(w,x),u))),
inference(spr,[status(thm),theory(equality)],[8,2]),
[iquote('0:SpR:8.0,2.0')] ).
cnf(95,plain,
equal(join(join(u,meet(v,join(u,w))),meet(x,join(v,u))),meet(join(v,u),join(x,join(u,w)))),
inference(spr,[status(thm),theory(equality)],[8,2]),
[iquote('0:SpR:8.0,2.0')] ).
cnf(100,plain,
equal(join(meet(u,v),meet(meet(w,v),join(meet(u,v),x))),meet(join(meet(u,v),x),meet(v,join(u,w)))),
inference(spr,[status(thm),theory(equality)],[2,8]),
[iquote('0:SpR:2.0,8.0')] ).
cnf(102,plain,
equal(join(u,join(meet(v,join(u,v)),u)),join(u,v)),
inference(rew,[status(thm),theory(equality)],[7,88]),
[iquote('0:Rew:7.0,88.0')] ).
cnf(103,plain,
equal(join(u,join(meet(v,v),u)),join(u,v)),
inference(rew,[status(thm),theory(equality)],[80,102]),
[iquote('0:Rew:80.0,102.0')] ).
cnf(108,plain,
equal(meet(u,u),u),
inference(spr,[status(thm),theory(equality)],[80,1]),
[iquote('0:SpR:80.0,1.0')] ).
cnf(114,plain,
equal(join(meet(u,join(v,w)),meet(w,w)),meet(join(v,w),join(w,u))),
inference(spr,[status(thm),theory(equality)],[80,2]),
[iquote('0:SpR:80.0,2.0')] ).
cnf(115,plain,
equal(join(meet(u,u),meet(v,join(w,u))),meet(join(w,u),join(v,u))),
inference(spr,[status(thm),theory(equality)],[80,2]),
[iquote('0:SpR:80.0,2.0')] ).
cnf(121,plain,
equal(meet(u,join(v,u)),u),
inference(rew,[status(thm),theory(equality)],[108,80]),
[iquote('0:Rew:108.0,80.0')] ).
cnf(123,plain,
equal(join(u,join(v,u)),join(u,v)),
inference(rew,[status(thm),theory(equality)],[108,103]),
[iquote('0:Rew:108.0,103.0')] ).
cnf(131,plain,
equal(meet(join(u,v),join(v,w)),join(meet(w,join(u,v)),v)),
inference(rew,[status(thm),theory(equality)],[108,114]),
[iquote('0:Rew:108.0,114.0')] ).
cnf(133,plain,
equal(meet(join(u,v),join(w,v)),join(v,meet(w,join(u,v)))),
inference(rew,[status(thm),theory(equality)],[108,115]),
[iquote('0:Rew:108.0,115.0')] ).
cnf(138,plain,
equal(join(meet(u,join(v,u)),v),join(v,u)),
inference(spr,[status(thm),theory(equality)],[108,7]),
[iquote('0:SpR:108.0,7.0')] ).
cnf(142,plain,
equal(meet(u,join(u,v)),join(meet(v,u),u)),
inference(spr,[status(thm),theory(equality)],[108,2]),
[iquote('0:SpR:108.0,2.0')] ).
cnf(150,plain,
equal(join(u,v),join(v,u)),
inference(rew,[status(thm),theory(equality)],[121,138]),
[iquote('0:Rew:121.0,138.0')] ).
cnf(151,plain,
equal(meet(join(u,v),join(u,w)),join(u,meet(w,join(u,v)))),
inference(rew,[status(thm),theory(equality)],[150,7]),
[iquote('0:Rew:150.0,7.0')] ).
cnf(152,plain,
~ equal(join(c,join(a,b)),join(a,join(b,c))),
inference(rew,[status(thm),theory(equality)],[150,3]),
[iquote('0:Rew:150.0,3.0')] ).
cnf(154,plain,
equal(meet(join(u,v),join(v,w)),join(v,meet(w,join(u,v)))),
inference(rew,[status(thm),theory(equality)],[150,131]),
[iquote('0:Rew:150.0,131.0')] ).
cnf(162,plain,
equal(join(meet(u,join(v,w)),join(v,meet(w,join(v,x)))),meet(join(v,w),join(join(v,x),u))),
inference(rew,[status(thm),theory(equality)],[150,20]),
[iquote('0:Rew:150.0,20.0')] ).
cnf(165,plain,
equal(meet(meet(u,join(v,w)),join(meet(w,u),x)),join(meet(w,u),meet(x,meet(u,join(v,w))))),
inference(rew,[status(thm),theory(equality)],[150,9]),
[iquote('0:Rew:150.0,9.0')] ).
cnf(168,plain,
equal(join(meet(u,v),v),v),
inference(rew,[status(thm),theory(equality)],[1,142]),
[iquote('0:Rew:1.0,142.0')] ).
cnf(169,plain,
equal(join(u,meet(v,u)),u),
inference(rew,[status(thm),theory(equality)],[150,168]),
[iquote('0:Rew:150.0,168.0')] ).
cnf(198,plain,
equal(join(meet(u,v),meet(w,v)),meet(v,join(u,w))),
inference(spr,[status(thm),theory(equality)],[150,2]),
[iquote('0:SpR:150.0,2.0')] ).
cnf(215,plain,
equal(meet(u,join(v,w)),meet(u,join(w,v))),
inference(rew,[status(thm),theory(equality)],[2,198]),
[iquote('0:Rew:2.0,198.0')] ).
cnf(229,plain,
equal(meet(u,meet(u,v)),meet(u,join(meet(w,v),v))),
inference(spr,[status(thm),theory(equality)],[169,49]),
[iquote('0:SpR:169.0,49.0')] ).
cnf(240,plain,
equal(join(u,u),u),
inference(spr,[status(thm),theory(equality)],[108,169]),
[iquote('0:SpR:108.0,169.0')] ).
cnf(246,plain,
equal(meet(u,meet(u,v)),meet(u,v)),
inference(rew,[status(thm),theory(equality)],[169,229,150]),
[iquote('0:Rew:169.0,229.0,150.0,229.0')] ).
cnf(255,plain,
equal(meet(meet(u,v),meet(v,u)),meet(u,v)),
inference(spr,[status(thm),theory(equality)],[240,5]),
[iquote('0:SpR:240.0,5.0')] ).
cnf(257,plain,
equal(meet(u,join(v,v)),meet(v,u)),
inference(spr,[status(thm),theory(equality)],[240,2]),
[iquote('0:SpR:240.0,2.0')] ).
cnf(262,plain,
equal(meet(u,v),meet(v,u)),
inference(rew,[status(thm),theory(equality)],[240,257]),
[iquote('0:Rew:240.0,257.0')] ).
cnf(263,plain,
equal(meet(u,meet(v,u)),meet(v,u)),
inference(rew,[status(thm),theory(equality)],[262,14]),
[iquote('0:Rew:262.0,14.0')] ).
cnf(278,plain,
equal(meet(join(u,v),join(v,w)),join(v,meet(u,join(v,w)))),
inference(spr,[status(thm),theory(equality)],[262,8]),
[iquote('0:SpR:262.0,8.0')] ).
cnf(279,plain,
equal(join(meet(u,v),meet(v,w)),meet(v,join(w,u))),
inference(spr,[status(thm),theory(equality)],[262,2]),
[iquote('0:SpR:262.0,2.0')] ).
cnf(280,plain,
equal(join(meet(u,v),meet(w,u)),meet(u,join(w,v))),
inference(spr,[status(thm),theory(equality)],[262,2]),
[iquote('0:SpR:262.0,2.0')] ).
cnf(283,plain,
equal(meet(u,join(meet(u,v),w)),meet(u,join(v,w))),
inference(spr,[status(thm),theory(equality)],[262,34]),
[iquote('0:SpR:262.0,34.0')] ).
cnf(284,plain,
equal(join(u,meet(u,v)),u),
inference(spr,[status(thm),theory(equality)],[262,169]),
[iquote('0:SpR:262.0,169.0')] ).
cnf(286,plain,
equal(meet(u,join(v,meet(u,w))),meet(u,join(v,w))),
inference(spr,[status(thm),theory(equality)],[262,35]),
[iquote('0:SpR:262.0,35.0')] ).
cnf(306,plain,
equal(join(u,meet(v,join(w,u))),join(u,meet(w,join(u,v)))),
inference(rew,[status(thm),theory(equality)],[154,278]),
[iquote('0:Rew:154.0,278.0')] ).
cnf(314,plain,
equal(join(meet(u,v),meet(u,join(meet(u,v),w))),meet(join(meet(u,v),w),u)),
inference(spr,[status(thm),theory(equality)],[284,8]),
[iquote('0:SpR:284.0,8.0')] ).
cnf(334,plain,
equal(join(meet(u,v),meet(u,join(meet(u,v),w))),meet(u,join(meet(u,v),w))),
inference(rew,[status(thm),theory(equality)],[262,314]),
[iquote('0:Rew:262.0,314.0')] ).
cnf(335,plain,
equal(join(meet(u,v),meet(u,join(v,w))),meet(u,join(v,w))),
inference(rew,[status(thm),theory(equality)],[283,334]),
[iquote('0:Rew:283.0,334.0')] ).
cnf(385,plain,
equal(join(join(u,v),join(v,u)),join(join(u,v),v)),
inference(spr,[status(thm),theory(equality)],[123]),
[iquote('0:SpR:123.0,123.0')] ).
cnf(393,plain,
equal(join(join(u,v),join(v,u)),join(v,u)),
inference(rew,[status(thm),theory(equality)],[123,385,150]),
[iquote('0:Rew:123.0,385.0,150.0,385.0')] ).
cnf(429,plain,
equal(meet(meet(u,v),meet(meet(u,v),join(w,u))),meet(u,v)),
inference(spr,[status(thm),theory(equality)],[246,5]),
[iquote('0:SpR:246.0,5.0')] ).
cnf(446,plain,
equal(meet(meet(u,v),join(w,u)),meet(u,v)),
inference(rew,[status(thm),theory(equality)],[246,429]),
[iquote('0:Rew:246.0,429.0')] ).
cnf(458,plain,
equal(join(meet(u,meet(v,w)),meet(v,w)),meet(meet(v,w),join(w,u))),
inference(spr,[status(thm),theory(equality)],[263,2]),
[iquote('0:SpR:263.0,2.0')] ).
cnf(460,plain,
equal(meet(meet(u,v),meet(meet(u,v),join(w,v))),meet(u,v)),
inference(spr,[status(thm),theory(equality)],[263,5]),
[iquote('0:SpR:263.0,5.0')] ).
cnf(483,plain,
equal(meet(meet(u,v),join(w,v)),meet(u,v)),
inference(rew,[status(thm),theory(equality)],[246,460]),
[iquote('0:Rew:246.0,460.0')] ).
cnf(484,plain,
equal(meet(meet(u,v),join(v,w)),meet(u,v)),
inference(rew,[status(thm),theory(equality)],[169,458,150]),
[iquote('0:Rew:169.0,458.0,150.0,458.0')] ).
cnf(587,plain,
equal(meet(u,join(v,w)),meet(join(w,v),u)),
inference(spr,[status(thm),theory(equality)],[215,262]),
[iquote('0:SpR:215.0,262.0')] ).
cnf(592,plain,
equal(join(join(u,v),meet(w,join(v,u))),join(u,v)),
inference(spr,[status(thm),theory(equality)],[215,169]),
[iquote('0:SpR:215.0,169.0')] ).
cnf(917,plain,
equal(meet(meet(u,join(v,w)),join(x,meet(v,u))),join(meet(v,u),meet(x,meet(u,join(v,w))))),
inference(spr,[status(thm),theory(equality)],[215,10]),
[iquote('0:SpR:215.0,10.0')] ).
cnf(1046,plain,
equal(join(join(u,v),meet(w,v)),join(u,v)),
inference(spr,[status(thm),theory(equality)],[483,169]),
[iquote('0:SpR:483.0,169.0')] ).
cnf(1062,plain,
equal(meet(u,join(v,join(u,w))),u),
inference(spr,[status(thm),theory(equality)],[1,483]),
[iquote('0:SpR:1.0,483.0')] ).
cnf(1070,plain,
equal(meet(u,join(v,join(w,u))),u),
inference(spr,[status(thm),theory(equality)],[121,483]),
[iquote('0:SpR:121.0,483.0')] ).
cnf(1104,plain,
equal(meet(u,join(join(u,v),w)),u),
inference(spr,[status(thm),theory(equality)],[1062,215]),
[iquote('0:SpR:1062.0,215.0')] ).
cnf(1109,plain,
equal(meet(join(u,join(v,w)),join(v,x)),join(meet(x,join(u,join(v,w))),v)),
inference(spr,[status(thm),theory(equality)],[1062,2]),
[iquote('0:SpR:1062.0,2.0')] ).
cnf(1150,plain,
equal(meet(join(u,join(v,w)),join(v,x)),join(v,meet(x,join(u,join(v,w))))),
inference(rew,[status(thm),theory(equality)],[150,1109]),
[iquote('0:Rew:150.0,1109.0')] ).
cnf(1159,plain,
equal(meet(u,join(join(v,u),w)),u),
inference(spr,[status(thm),theory(equality)],[1070,215]),
[iquote('0:SpR:1070.0,215.0')] ).
cnf(1250,plain,
equal(join(join(u,meet(v,join(u,w))),join(u,meet(v,join(u,x)))),meet(join(v,u),join(join(u,x),join(u,w)))),
inference(spr,[status(thm),theory(equality)],[8,95]),
[iquote('0:SpR:8.0,95.0')] ).
cnf(1262,plain,
equal(join(join(u,meet(v,join(u,w))),meet(join(v,u),x)),meet(join(v,u),join(x,join(u,w)))),
inference(spr,[status(thm),theory(equality)],[262,95]),
[iquote('0:SpR:262.0,95.0')] ).
cnf(1391,plain,
equal(join(join(join(u,v),w),u),join(join(u,v),w)),
inference(spr,[status(thm),theory(equality)],[1104,169]),
[iquote('0:SpR:1104.0,169.0')] ).
cnf(1419,plain,
equal(join(u,join(join(u,v),w)),join(join(u,v),w)),
inference(rew,[status(thm),theory(equality)],[150,1391]),
[iquote('0:Rew:150.0,1391.0')] ).
cnf(1538,plain,
equal(join(join(u,v),meet(w,u)),join(u,v)),
inference(spr,[status(thm),theory(equality)],[484,169]),
[iquote('0:SpR:484.0,169.0')] ).
cnf(1551,plain,
equal(meet(meet(u,meet(v,w)),meet(w,join(x,v))),meet(u,meet(v,w))),
inference(spr,[status(thm),theory(equality)],[2,484]),
[iquote('0:SpR:2.0,484.0')] ).
cnf(1610,plain,
equal(meet(join(meet(u,v),w),meet(v,join(x,u))),join(meet(u,v),meet(w,meet(v,join(x,u))))),
inference(spr,[status(thm),theory(equality)],[587,10]),
[iquote('0:SpR:587.0,10.0')] ).
cnf(1758,plain,
equal(join(meet(u,join(v,join(w,x))),join(join(w,x),meet(v,join(x,w)))),meet(join(v,join(w,x)),join(join(x,w),u))),
inference(spr,[status(thm),theory(equality)],[393,94]),
[iquote('0:SpR:393.0,94.0')] ).
cnf(1785,plain,
equal(join(meet(u,v),join(meet(v,w),meet(v,join(meet(v,w),x)))),meet(v,join(join(meet(v,w),x),u))),
inference(spr,[status(thm),theory(equality)],[284,94]),
[iquote('0:SpR:284.0,94.0')] ).
cnf(1798,plain,
equal(join(meet(join(u,v),w),join(u,meet(v,join(u,x)))),meet(join(v,u),join(join(u,x),w))),
inference(spr,[status(thm),theory(equality)],[587,94]),
[iquote('0:SpR:587.0,94.0')] ).
cnf(1809,plain,
equal(meet(join(u,v),join(join(v,w),meet(x,v))),join(meet(x,v),join(v,meet(u,join(v,w))))),
inference(spr,[status(thm),theory(equality)],[483,94]),
[iquote('0:SpR:483.0,94.0')] ).
cnf(1812,plain,
equal(join(meet(join(u,v),w),join(v,meet(u,join(v,x)))),meet(join(u,v),join(join(v,x),w))),
inference(spr,[status(thm),theory(equality)],[262,94]),
[iquote('0:SpR:262.0,94.0')] ).
cnf(1834,plain,
equal(join(meet(u,v),join(v,meet(w,join(v,x)))),join(v,meet(x,join(w,v)))),
inference(rew,[status(thm),theory(equality)],[154,1809,1538]),
[iquote('0:Rew:154.0,1809.0,1538.0,1809.0')] ).
cnf(1848,plain,
equal(meet(u,join(join(meet(u,v),w),x)),meet(u,join(join(v,w),x))),
inference(rew,[status(thm),theory(equality)],[279,1785,335,283]),
[iquote('0:Rew:279.0,1785.0,335.0,1785.0,283.0,1785.0')] ).
cnf(1880,plain,
equal(meet(join(u,join(v,w)),join(join(w,v),x)),join(meet(x,join(u,join(v,w))),join(v,w))),
inference(rew,[status(thm),theory(equality)],[592,1758]),
[iquote('0:Rew:592.0,1758.0')] ).
cnf(1881,plain,
equal(meet(join(u,join(v,w)),join(join(w,v),x)),join(join(v,w),meet(x,join(u,join(v,w))))),
inference(rew,[status(thm),theory(equality)],[150,1880]),
[iquote('0:Rew:150.0,1880.0')] ).
cnf(2462,plain,
equal(meet(join(u,v),join(join(u,w),v)),join(v,join(u,meet(v,join(u,w))))),
inference(spr,[status(thm),theory(equality)],[121,162]),
[iquote('0:SpR:121.0,162.0')] ).
cnf(2468,plain,
equal(meet(join(u,v),join(join(u,w),meet(x,u))),join(meet(x,u),join(u,meet(v,join(u,w))))),
inference(spr,[status(thm),theory(equality)],[484,162]),
[iquote('0:SpR:484.0,162.0')] ).
cnf(2484,plain,
equal(join(u,meet(v,join(u,join(v,w)))),join(u,join(v,meet(u,join(v,w))))),
inference(rew,[status(thm),theory(equality)],[306,2462,133]),
[iquote('0:Rew:306.0,2462.0,133.0,2462.0')] ).
cnf(2485,plain,
equal(join(u,join(v,meet(u,join(v,w)))),join(u,v)),
inference(rew,[status(thm),theory(equality)],[1062,2484]),
[iquote('0:Rew:1062.0,2484.0')] ).
cnf(2497,plain,
equal(meet(join(u,v),join(u,w)),join(u,meet(w,join(v,u)))),
inference(rew,[status(thm),theory(equality)],[1538,2468,1834]),
[iquote('0:Rew:1538.0,2468.0,1834.0,2468.0')] ).
cnf(2498,plain,
equal(join(u,meet(v,join(u,w))),join(u,meet(v,join(w,u)))),
inference(rew,[status(thm),theory(equality)],[151,2497]),
[iquote('0:Rew:151.0,2497.0')] ).
cnf(3499,plain,
equal(join(join(u,meet(v,w)),meet(w,v)),join(u,meet(v,w))),
inference(spr,[status(thm),theory(equality)],[255,1046]),
[iquote('0:SpR:255.0,1046.0')] ).
cnf(3540,plain,
equal(join(meet(u,v),join(w,meet(v,u))),join(w,meet(v,u))),
inference(rew,[status(thm),theory(equality)],[150,3499]),
[iquote('0:Rew:150.0,3499.0')] ).
cnf(4807,plain,
equal(meet(join(meet(u,v),meet(w,meet(x,v))),meet(v,join(u,x))),join(meet(u,v),meet(meet(x,v),join(meet(u,v),w)))),
inference(spr,[status(thm),theory(equality)],[35,100]),
[iquote('0:SpR:35.0,100.0')] ).
cnf(4908,plain,
equal(meet(meet(u,join(v,w)),join(meet(x,meet(w,u)),meet(v,u))),meet(join(meet(v,u),x),meet(u,join(v,w)))),
inference(rew,[status(thm),theory(equality)],[587,4807,100]),
[iquote('0:Rew:587.0,4807.0,100.0,4807.0')] ).
cnf(4909,plain,
equal(meet(join(meet(u,v),w),meet(v,join(u,x))),join(meet(u,v),meet(w,meet(x,v)))),
inference(rew,[status(thm),theory(equality)],[1551,4908,917]),
[iquote('0:Rew:1551.0,4908.0,917.0,4908.0')] ).
cnf(4910,plain,
equal(join(meet(u,v),meet(meet(w,v),join(meet(u,v),x))),join(meet(u,v),meet(x,meet(w,v)))),
inference(rew,[status(thm),theory(equality)],[4909,100]),
[iquote('0:Rew:4909.0,100.0')] ).
cnf(5766,plain,
equal(meet(join(meet(u,v),w),join(meet(u,v),meet(w,meet(x,v)))),meet(join(meet(u,v),w),join(meet(u,v),meet(x,v)))),
inference(spr,[status(thm),theory(equality)],[4910,35]),
[iquote('0:SpR:4910.0,35.0')] ).
cnf(6010,plain,
equal(meet(join(meet(u,v),w),meet(v,join(x,u))),join(meet(u,v),meet(w,meet(x,v)))),
inference(rew,[status(thm),theory(equality)],[446,5766,151,2]),
[iquote('0:Rew:446.0,5766.0,151.0,5766.0,2.0,5766.0')] ).
cnf(6011,plain,
equal(join(meet(u,v),meet(w,meet(v,join(x,u)))),join(meet(u,v),meet(w,meet(x,v)))),
inference(rew,[status(thm),theory(equality)],[1610,6010]),
[iquote('0:Rew:1610.0,6010.0')] ).
cnf(6012,plain,
equal(meet(meet(u,join(v,w)),join(x,meet(w,u))),join(meet(w,u),meet(x,meet(v,u)))),
inference(rew,[status(thm),theory(equality)],[6011,10]),
[iquote('0:Rew:6011.0,10.0')] ).
cnf(6013,plain,
equal(meet(meet(u,join(v,w)),join(meet(w,u),x)),join(meet(w,u),meet(x,meet(v,u)))),
inference(rew,[status(thm),theory(equality)],[6011,165]),
[iquote('0:Rew:6011.0,165.0')] ).
cnf(7179,plain,
equal(join(meet(u,join(v,u)),meet(w,meet(v,join(v,u)))),meet(join(v,u),join(w,meet(u,join(v,u))))),
inference(spr,[status(thm),theory(equality)],[108,6012]),
[iquote('0:SpR:108.0,6012.0')] ).
cnf(7254,plain,
equal(meet(join(u,v),join(w,v)),join(v,meet(w,u))),
inference(rew,[status(thm),theory(equality)],[1,7179,121]),
[iquote('0:Rew:1.0,7179.0,121.0,7179.0')] ).
cnf(7255,plain,
equal(join(u,meet(v,join(w,u))),join(u,meet(v,w))),
inference(rew,[status(thm),theory(equality)],[133,7254]),
[iquote('0:Rew:133.0,7254.0')] ).
cnf(7258,plain,
equal(join(u,meet(v,join(u,w))),join(u,meet(w,v))),
inference(rew,[status(thm),theory(equality)],[7255,306]),
[iquote('0:Rew:7255.0,306.0')] ).
cnf(7260,plain,
equal(join(u,meet(v,join(u,w))),join(u,meet(v,w))),
inference(rew,[status(thm),theory(equality)],[7255,2498]),
[iquote('0:Rew:7255.0,2498.0')] ).
cnf(7265,plain,
equal(meet(join(u,v),join(w,v)),join(v,meet(w,u))),
inference(rew,[status(thm),theory(equality)],[7255,133]),
[iquote('0:Rew:7255.0,133.0')] ).
cnf(7266,plain,
equal(meet(join(u,v),join(v,w)),join(v,meet(w,u))),
inference(rew,[status(thm),theory(equality)],[7255,154]),
[iquote('0:Rew:7255.0,154.0')] ).
cnf(7268,plain,
equal(meet(join(u,join(v,w)),join(join(w,v),x)),join(join(v,w),meet(x,u))),
inference(rew,[status(thm),theory(equality)],[7255,1881]),
[iquote('0:Rew:7255.0,1881.0')] ).
cnf(7271,plain,
equal(join(meet(u,join(v,w)),join(w,meet(x,v))),meet(join(v,w),join(join(w,x),u))),
inference(rew,[status(thm),theory(equality)],[7258,94]),
[iquote('0:Rew:7258.0,94.0')] ).
cnf(7272,plain,
equal(join(join(u,meet(v,w)),meet(x,join(w,u))),meet(join(w,u),join(x,join(u,v)))),
inference(rew,[status(thm),theory(equality)],[7258,95]),
[iquote('0:Rew:7258.0,95.0')] ).
cnf(7274,plain,
equal(meet(join(u,v),join(w,u)),join(u,meet(v,w))),
inference(rew,[status(thm),theory(equality)],[7258,8]),
[iquote('0:Rew:7258.0,8.0')] ).
cnf(7275,plain,
equal(meet(join(u,v),join(u,w)),join(u,meet(v,w))),
inference(rew,[status(thm),theory(equality)],[7258,151]),
[iquote('0:Rew:7258.0,151.0')] ).
cnf(7308,plain,
equal(join(u,join(v,meet(w,u))),join(u,v)),
inference(rew,[status(thm),theory(equality)],[7258,2485]),
[iquote('0:Rew:7258.0,2485.0')] ).
cnf(7316,plain,
equal(join(meet(join(u,v),w),join(v,meet(x,u))),meet(join(u,v),join(join(v,x),w))),
inference(rew,[status(thm),theory(equality)],[7258,1812]),
[iquote('0:Rew:7258.0,1812.0')] ).
cnf(7328,plain,
equal(join(join(u,meet(v,join(u,w))),join(u,meet(x,v))),meet(join(v,u),join(join(u,x),join(u,w)))),
inference(rew,[status(thm),theory(equality)],[7258,1250]),
[iquote('0:Rew:7258.0,1250.0')] ).
cnf(7329,plain,
equal(join(meet(join(u,v),w),join(u,meet(x,v))),meet(join(v,u),join(join(u,x),w))),
inference(rew,[status(thm),theory(equality)],[7258,1798]),
[iquote('0:Rew:7258.0,1798.0')] ).
cnf(7357,plain,
equal(join(join(u,meet(v,w)),meet(join(w,u),x)),meet(join(w,u),join(x,join(u,v)))),
inference(rew,[status(thm),theory(equality)],[7258,1262]),
[iquote('0:Rew:7258.0,1262.0')] ).
cnf(7433,plain,
equal(join(u,meet(v,w)),join(u,meet(w,v))),
inference(rew,[status(thm),theory(equality)],[7258,7260]),
[iquote('0:Rew:7258.0,7260.0')] ).
cnf(7493,plain,
equal(join(join(u,meet(v,w)),join(u,meet(x,w))),meet(join(w,u),join(join(u,x),join(u,v)))),
inference(rew,[status(thm),theory(equality)],[7258,7328]),
[iquote('0:Rew:7258.0,7328.0')] ).
cnf(9535,plain,
equal(join(join(join(u,v),w),join(x,v)),join(join(join(u,v),w),x)),
inference(spr,[status(thm),theory(equality)],[1159,7308]),
[iquote('0:SpR:1159.0,7308.0')] ).
cnf(9552,plain,
equal(join(u,join(v,meet(u,w))),join(u,v)),
inference(spr,[status(thm),theory(equality)],[262,7308]),
[iquote('0:SpR:262.0,7308.0')] ).
cnf(9557,plain,
equal(join(meet(u,v),join(w,meet(v,u))),join(meet(u,v),w)),
inference(spr,[status(thm),theory(equality)],[255,7308]),
[iquote('0:SpR:255.0,7308.0')] ).
cnf(9567,plain,
equal(join(u,join(meet(v,u),w)),join(u,w)),
inference(spr,[status(thm),theory(equality)],[150,7308]),
[iquote('0:SpR:150.0,7308.0')] ).
cnf(9621,plain,
equal(join(u,meet(v,w)),join(meet(w,v),u)),
inference(rew,[status(thm),theory(equality)],[3540,9557]),
[iquote('0:Rew:3540.0,9557.0')] ).
cnf(9810,plain,
equal(join(u,meet(v,join(w,x))),join(u,meet(join(x,w),v))),
inference(spr,[status(thm),theory(equality)],[215,7433]),
[iquote('0:SpR:215.0,7433.0')] ).
cnf(9918,plain,
equal(meet(join(join(u,meet(v,w)),x),join(v,u)),join(join(u,meet(v,w)),meet(x,v))),
inference(spr,[status(thm),theory(equality)],[9552,7274]),
[iquote('0:SpR:9552.0,7274.0')] ).
cnf(10035,plain,
equal(meet(join(u,v),join(w,join(v,meet(u,x)))),join(join(v,meet(u,x)),meet(w,u))),
inference(rew,[status(thm),theory(equality)],[587,9918]),
[iquote('0:Rew:587.0,9918.0')] ).
cnf(10217,plain,
equal(meet(join(u,meet(v,w)),join(meet(w,join(u,v)),x)),join(meet(w,join(u,v)),meet(x,meet(u,join(u,v))))),
inference(spr,[status(thm),theory(equality)],[7275,6013]),
[iquote('0:SpR:7275.0,6013.0')] ).
cnf(10322,plain,
equal(meet(join(u,meet(v,w)),join(meet(w,join(u,v)),x)),join(meet(w,join(u,v)),meet(x,u))),
inference(rew,[status(thm),theory(equality)],[1,10217]),
[iquote('0:Rew:1.0,10217.0')] ).
cnf(10323,plain,
equal(meet(join(u,meet(v,w)),join(w,x)),join(meet(w,join(u,v)),meet(x,u))),
inference(rew,[status(thm),theory(equality)],[59,10322]),
[iquote('0:Rew:59.0,10322.0')] ).
cnf(10469,plain,
equal(join(join(u,v),join(u,w)),join(join(u,v),w)),
inference(spr,[status(thm),theory(equality)],[1,9567]),
[iquote('0:SpR:1.0,9567.0')] ).
cnf(10546,plain,
equal(join(join(u,meet(v,w)),join(u,meet(x,w))),meet(join(w,u),join(join(u,x),v))),
inference(rew,[status(thm),theory(equality)],[10469,7493]),
[iquote('0:Rew:10469.0,7493.0')] ).
cnf(10598,plain,
equal(join(join(u,meet(v,w)),meet(x,w)),meet(join(w,u),join(join(u,x),v))),
inference(rew,[status(thm),theory(equality)],[10469,10546]),
[iquote('0:Rew:10469.0,10546.0')] ).
cnf(11478,plain,
equal(join(join(u,meet(v,w)),meet(join(w,u),join(join(u,v),x))),join(join(u,meet(v,w)),meet(x,join(w,u)))),
inference(spr,[status(thm),theory(equality)],[7271,123]),
[iquote('0:SpR:7271.0,123.0')] ).
cnf(11760,plain,
equal(meet(join(u,v),join(w,join(v,x))),join(v,meet(join(join(v,x),w),u))),
inference(rew,[status(thm),theory(equality)],[7265,11478,9535,7357,7272]),
[iquote('0:Rew:7265.0,11478.0,9535.0,11478.0,7357.0,11478.0,7272.0,11478.0')] ).
cnf(11775,plain,
equal(join(u,meet(join(join(u,meet(v,w)),x),v)),join(join(u,meet(v,w)),meet(x,v))),
inference(rew,[status(thm),theory(equality)],[11760,10035]),
[iquote('0:Rew:11760.0,10035.0')] ).
cnf(11791,plain,
equal(join(join(u,meet(v,w)),meet(x,join(w,u))),join(u,meet(join(join(u,v),x),w))),
inference(rew,[status(thm),theory(equality)],[11760,7272]),
[iquote('0:Rew:11760.0,7272.0')] ).
cnf(11823,plain,
equal(join(u,meet(v,join(w,join(u,meet(v,x))))),join(join(u,meet(v,x)),meet(w,v))),
inference(rew,[status(thm),theory(equality)],[587,11775]),
[iquote('0:Rew:587.0,11775.0')] ).
cnf(16599,plain,
equal(join(meet(join(u,v),w),join(v,meet(x,u))),join(v,meet(join(join(v,x),w),u))),
inference(spr,[status(thm),theory(equality)],[11791,9621]),
[iquote('0:SpR:11791.0,9621.0')] ).
cnf(16603,plain,
equal(join(u,join(v,meet(join(join(v,w),u),x))),join(u,join(v,meet(w,x)))),
inference(spr,[status(thm),theory(equality)],[11791,9552]),
[iquote('0:SpR:11791.0,9552.0')] ).
cnf(16655,plain,
equal(join(u,meet(join(join(u,v),w),join(x,w))),join(join(u,meet(v,join(x,w))),w)),
inference(spr,[status(thm),theory(equality)],[1159,11791]),
[iquote('0:SpR:1159.0,11791.0')] ).
cnf(16753,plain,
equal(join(u,meet(join(join(u,v),w),join(x,w))),join(w,join(u,meet(v,join(x,w))))),
inference(rew,[status(thm),theory(equality)],[150,16655]),
[iquote('0:Rew:150.0,16655.0')] ).
cnf(16754,plain,
equal(join(u,join(v,meet(w,join(u,x)))),join(v,join(u,meet(x,join(w,v))))),
inference(rew,[status(thm),theory(equality)],[7265,16753]),
[iquote('0:Rew:7265.0,16753.0')] ).
cnf(16757,plain,
equal(meet(join(u,v),join(join(v,w),x)),join(v,meet(join(join(v,w),x),u))),
inference(rew,[status(thm),theory(equality)],[7316,16599]),
[iquote('0:Rew:7316.0,16599.0')] ).
cnf(16781,plain,
equal(join(join(u,meet(v,w)),meet(x,w)),join(u,meet(join(join(u,x),v),w))),
inference(rew,[status(thm),theory(equality)],[16757,10598]),
[iquote('0:Rew:16757.0,10598.0')] ).
cnf(16791,plain,
equal(join(meet(join(u,v),w),join(u,meet(x,v))),join(u,meet(join(join(u,x),w),v))),
inference(rew,[status(thm),theory(equality)],[16757,7329]),
[iquote('0:Rew:16757.0,7329.0')] ).
cnf(18868,plain,
equal(join(meet(join(u,v),w),join(u,meet(x,v))),meet(join(u,v),join(join(u,x),w))),
inference(spr,[status(thm),theory(equality)],[7275,280]),
[iquote('0:SpR:7275.0,280.0')] ).
cnf(19126,plain,
equal(meet(join(u,v),join(join(u,w),x)),join(u,meet(join(join(u,w),x),v))),
inference(rew,[status(thm),theory(equality)],[16791,18868]),
[iquote('0:Rew:16791.0,18868.0')] ).
cnf(19289,plain,
equal(meet(join(u,v),join(join(u,meet(v,w)),x)),meet(join(u,v),join(join(u,w),x))),
inference(spr,[status(thm),theory(equality)],[7275,283]),
[iquote('0:SpR:7275.0,283.0')] ).
cnf(19461,plain,
equal(join(join(u,meet(v,w)),meet(x,v)),join(u,meet(join(join(u,w),x),v))),
inference(rew,[status(thm),theory(equality)],[11823,19289,9810,19126]),
[iquote('0:Rew:11823.0,19289.0,9810.0,19289.0,19126.0,19289.0,19126.0,19289.0')] ).
cnf(19509,plain,
equal(meet(u,join(v,join(w,meet(u,x)))),join(meet(u,join(w,x)),meet(v,u))),
inference(spr,[status(thm),theory(equality)],[286,280]),
[iquote('0:SpR:286.0,280.0')] ).
cnf(19681,plain,
equal(meet(u,join(v,join(w,meet(u,x)))),meet(u,join(v,join(w,x)))),
inference(rew,[status(thm),theory(equality)],[280,19509]),
[iquote('0:Rew:280.0,19509.0')] ).
cnf(19685,plain,
equal(join(u,meet(v,join(w,join(u,x)))),join(join(u,meet(v,x)),meet(w,v))),
inference(rew,[status(thm),theory(equality)],[19681,11823]),
[iquote('0:Rew:19681.0,11823.0')] ).
cnf(21668,plain,
equal(meet(u,join(v,join(join(meet(u,v),w),x))),meet(u,join(join(meet(u,v),w),x))),
inference(spr,[status(thm),theory(equality)],[1419,283]),
[iquote('0:SpR:1419.0,283.0')] ).
cnf(21794,plain,
equal(meet(u,join(v,join(join(meet(u,v),w),x))),meet(u,join(join(v,w),x))),
inference(rew,[status(thm),theory(equality)],[1848,21668]),
[iquote('0:Rew:1848.0,21668.0')] ).
cnf(23909,plain,
equal(join(meet(join(u,v),join(w,v)),meet(x,w)),meet(join(w,v),join(join(u,v),x))),
inference(spr,[status(thm),theory(equality)],[121,10323]),
[iquote('0:SpR:121.0,10323.0')] ).
cnf(24172,plain,
equal(join(join(u,meet(v,w)),meet(x,v)),meet(join(v,u),join(join(w,u),x))),
inference(rew,[status(thm),theory(equality)],[7265,23909]),
[iquote('0:Rew:7265.0,23909.0')] ).
cnf(29245,plain,
equal(join(join(meet(u,v),meet(w,u)),meet(x,u)),meet(u,join(join(join(meet(u,v),x),w),v))),
inference(spr,[status(thm),theory(equality)],[16781,280]),
[iquote('0:SpR:16781.0,280.0')] ).
cnf(29354,plain,
equal(join(u,meet(join(join(u,v),w),join(w,x))),join(join(u,w),meet(v,join(w,x)))),
inference(spr,[status(thm),theory(equality)],[1,16781]),
[iquote('0:SpR:1.0,16781.0')] ).
cnf(29606,plain,
equal(join(u,join(v,meet(w,join(u,x)))),join(join(u,v),meet(x,join(v,w)))),
inference(rew,[status(thm),theory(equality)],[7266,29354]),
[iquote('0:Rew:7266.0,29354.0')] ).
cnf(29662,plain,
equal(meet(u,join(v,join(join(meet(u,v),w),x))),meet(u,join(w,join(x,v)))),
inference(rew,[status(thm),theory(equality)],[280,29245,150]),
[iquote('0:Rew:280.0,29245.0,280.0,29245.0,150.0,29245.0')] ).
cnf(29663,plain,
equal(meet(u,join(join(v,w),x)),meet(u,join(w,join(x,v)))),
inference(rew,[status(thm),theory(equality)],[21794,29662]),
[iquote('0:Rew:21794.0,29662.0')] ).
cnf(29811,plain,
equal(join(join(u,meet(v,w)),meet(x,v)),meet(join(v,u),join(u,join(x,w)))),
inference(rew,[status(thm),theory(equality)],[29663,24172]),
[iquote('0:Rew:29663.0,24172.0')] ).
cnf(29840,plain,
equal(meet(join(u,join(v,w)),join(v,join(x,w))),join(join(v,w),meet(x,u))),
inference(rew,[status(thm),theory(equality)],[29663,7268]),
[iquote('0:Rew:29663.0,7268.0')] ).
cnf(30070,plain,
equal(join(join(u,meet(v,w)),meet(x,v)),join(u,meet(join(x,w),v))),
inference(rew,[status(thm),theory(equality)],[7266,29811]),
[iquote('0:Rew:7266.0,29811.0')] ).
cnf(30085,plain,
equal(join(u,meet(v,join(w,join(u,x)))),join(u,meet(join(w,x),v))),
inference(rew,[status(thm),theory(equality)],[30070,19685]),
[iquote('0:Rew:30070.0,19685.0')] ).
cnf(30086,plain,
equal(join(u,meet(join(join(u,v),w),x)),join(u,meet(join(w,v),x))),
inference(rew,[status(thm),theory(equality)],[30070,19461]),
[iquote('0:Rew:30070.0,19461.0')] ).
cnf(30096,plain,
equal(meet(join(u,join(v,w)),join(v,x)),join(v,meet(join(u,w),x))),
inference(rew,[status(thm),theory(equality)],[30085,1150]),
[iquote('0:Rew:30085.0,1150.0')] ).
cnf(30100,plain,
equal(join(join(u,meet(v,w)),meet(x,join(w,u))),join(u,meet(join(x,v),w))),
inference(rew,[status(thm),theory(equality)],[30086,11791]),
[iquote('0:Rew:30086.0,11791.0')] ).
cnf(30172,plain,
equal(join(u,join(v,meet(join(u,w),x))),join(u,join(v,meet(w,x)))),
inference(rew,[status(thm),theory(equality)],[30086,16603]),
[iquote('0:Rew:30086.0,16603.0')] ).
cnf(30305,plain,
equal(join(join(u,v),meet(w,x)),join(u,join(v,meet(w,x)))),
inference(rew,[status(thm),theory(equality)],[7265,29840,30096]),
[iquote('0:Rew:7265.0,29840.0,30096.0,29840.0')] ).
cnf(30495,plain,
equal(join(u,join(v,meet(w,join(u,x)))),join(u,join(v,meet(x,join(v,w))))),
inference(rew,[status(thm),theory(equality)],[30305,29606]),
[iquote('0:Rew:30305.0,29606.0')] ).
cnf(30695,plain,
equal(join(u,join(meet(v,w),meet(x,join(w,u)))),join(u,meet(join(x,v),w))),
inference(rew,[status(thm),theory(equality)],[30305,30100]),
[iquote('0:Rew:30305.0,30100.0')] ).
cnf(30739,plain,
equal(join(u,join(v,meet(w,join(u,x)))),join(u,join(v,meet(w,x)))),
inference(rew,[status(thm),theory(equality)],[7258,30495]),
[iquote('0:Rew:7258.0,30495.0')] ).
cnf(30748,plain,
equal(join(u,join(v,meet(w,join(x,u)))),join(v,join(u,meet(x,w)))),
inference(rew,[status(thm),theory(equality)],[30739,16754]),
[iquote('0:Rew:30739.0,16754.0')] ).
cnf(30768,plain,
equal(join(meet(u,v),join(w,meet(v,x))),join(w,meet(join(x,u),v))),
inference(rew,[status(thm),theory(equality)],[30748,30695]),
[iquote('0:Rew:30748.0,30695.0')] ).
cnf(33375,plain,
equal(join(u,join(v,meet(join(u,w),x))),join(v,meet(join(x,u),join(u,w)))),
inference(spr,[status(thm),theory(equality)],[1,30768]),
[iquote('0:SpR:1.0,30768.0')] ).
cnf(33523,plain,
equal(join(u,join(v,meet(w,x))),join(v,join(u,meet(w,x)))),
inference(rew,[status(thm),theory(equality)],[30172,33375,7266]),
[iquote('0:Rew:30172.0,33375.0,7266.0,33375.0')] ).
cnf(35347,plain,
equal(join(u,join(v,w)),join(v,join(u,w))),
inference(spr,[status(thm),theory(equality)],[1,33523]),
[iquote('0:SpR:1.0,33523.0')] ).
cnf(35506,plain,
~ equal(join(a,join(c,b)),join(a,join(b,c))),
inference(rew,[status(thm),theory(equality)],[35347,152]),
[iquote('0:Rew:35347.0,152.0')] ).
cnf(35586,plain,
~ equal(join(a,join(b,c)),join(a,join(b,c))),
inference(rew,[status(thm),theory(equality)],[150,35506]),
[iquote('0:Rew:150.0,35506.0')] ).
cnf(35587,plain,
$false,
inference(obv,[status(thm),theory(equality)],[35586]),
[iquote('0:Obv:35586.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : LAT007-1 : TPTP v8.1.0. Released v2.2.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n026.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Tue Jun 28 22:36:17 EDT 2022
% 0.14/0.34 % CPUTime :
% 26.68/26.91
% 26.68/26.91 SPASS V 3.9
% 26.68/26.91 SPASS beiseite: Proof found.
% 26.68/26.91 % SZS status Theorem
% 26.68/26.91 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.68/26.91 SPASS derived 22995 clauses, backtracked 0 clauses, performed 0 splits and kept 4972 clauses.
% 26.68/26.91 SPASS allocated 98511 KBytes.
% 26.68/26.91 SPASS spent 0:0:26.53 on the problem.
% 26.68/26.91 0:00:00.03 for the input.
% 26.68/26.91 0:00:00.00 for the FLOTTER CNF translation.
% 26.68/26.91 0:00:00.15 for inferences.
% 26.68/26.91 0:00:00.00 for the backtracking.
% 26.68/26.91 0:0:26.31 for the reduction.
% 26.68/26.91
% 26.68/26.91
% 26.68/26.91 Here is a proof with depth 11, length 193 :
% 26.68/26.91 % SZS output start Refutation
% See solution above
% 26.96/27.12 Formulae used in the proof : absorption distribution prove_associativity_of_join
% 26.96/27.12
%------------------------------------------------------------------------------