%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT094-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 01:02:12 PM UTC 2026
% Result : Unsatisfiable 223.85s 28.53s
% Output : CNFRefutation 223.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 2
% Syntax : Number of formulae : 101 ( 101 unt; 0 def)
% Number of atoms : 101 ( 100 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 6 avg)
% Maximal term depth : 20 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 459 ( 459 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D,E,F] : join(meet(join(meet(A,B),meet(B,join(A,B))),C),meet(join(meet(A,join(join(meet(B,D),meet(E,B)),B)),meet(join(meet(B,meet(meet(join(B,D),join(E,B)),B)),meet(F,join(B,meet(meet(join(B,D),join(E,B)),B)))),join(A,join(join(meet(B,D),meet(E,B)),B)))),join(join(meet(A,B),meet(B,join(A,B))),C))) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
join(a,a) != a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
join(a,a) != a,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f9,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,join(meet(X1,X2),meet(X2,join(X1,X2)))),meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(X0,join(meet(X1,X2),meet(X2,join(X1,X2)))))),X3),meet(join(meet(X0,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X4),meet(X5,join(meet(X1,X2),meet(X2,join(X1,X2))))),join(meet(X1,X2),meet(X2,join(X1,X2))))),meet(X2,join(X0,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X4),meet(X5,join(meet(X1,X2),meet(X2,join(X1,X2))))),join(meet(X1,X2),meet(X2,join(X1,X2))))))),join(join(meet(X0,join(meet(X1,X2),meet(X2,join(X1,X2)))),meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(X0,join(meet(X1,X2),meet(X2,join(X1,X2)))))),X3))) = join(meet(X1,X2),meet(X2,join(X1,X2))),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f33,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))))))),meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),join(X0,X2))),X6),meet(join(meet(X0,join(join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),X7),meet(X8,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))))),join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(X0,join(join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),X7),meet(X8,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))))),join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))))))),join(join(meet(X0,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))))))),meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),join(X0,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))))))))),X6))) = join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(join(meet(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)),meet(X5,join(X2,meet(meet(join(X2,X3),join(X4,X2)),X2)))),join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),
inference(paramodulation,[status(thm)],[f3,f9]) ).
fof(f83,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),join(X0,X1))),X6),meet(join(meet(X0,join(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),X7),meet(X8,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))),join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),X7),meet(X8,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))),join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))))))),meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),join(X0,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))))))))),X6))) = join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)),meet(X5,join(X1,meet(meet(join(X1,X3),join(X4,X1)),X1)))),join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f33]) ).
fof(f84,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),X7),meet(X8,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))))),join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),X7),meet(X8,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))))),join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))))))),meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),join(X0,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))))))))),X2))) = join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)),meet(X6,join(X1,meet(meet(join(X1,X4),join(X5,X1)),X1)))),join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f83]) ).
fof(f85,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f84]) ).
fof(f86,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f85]) ).
fof(f87,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f86]) ).
fof(f88,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(X1,X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f87]) ).
fof(f89,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(X1,X3),meet(X4,X1)),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f88]) ).
fof(f90,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f89]) ).
fof(f91,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f90]) ).
fof(f92,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f91]) ).
fof(f93,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f3,f92]) ).
fof(f94,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(join(meet(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)),meet(X8,join(X1,meet(meet(join(X1,X6),join(X7,X1)),X1)))),join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = X1,
inference(forward_demodulation,[status(thm)],[f3,f93]) ).
fof(f673,plain,
! [X0,X1,X2] : join(meet(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X1),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),X1))),X2),meet(X1,join(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X1),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),X1))),X2))) = X1,
inference(paramodulation,[status(thm)],[f3,f94]) ).
fof(f1066,plain,
! [X0,X1,X2] : join(meet(join(meet(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X1),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X1),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),X1))),X1))),X2),meet(X1,join(X1,X2))) = X1,
inference(paramodulation,[status(thm)],[f673,f673]) ).
fof(f1090,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(join(meet(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),X1),meet(X1,join(join(meet(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),X1))),X5),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(join(meet(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),X1),meet(X1,join(join(meet(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),X1))),X5))) = X1,
inference(paramodulation,[status(thm)],[f673,f3]) ).
fof(f1095,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2)))),meet(join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))),join(X0,join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2)))))),X3),meet(join(meet(X0,join(join(meet(join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))),X4),meet(X5,join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))))),join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))))),meet(X2,join(X0,join(join(meet(join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))),X4),meet(X5,join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))))),join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))))))),join(join(meet(X0,X2),meet(join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))),join(X0,join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2)))))),X3))) = join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2),meet(X2,join(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),X2),meet(X2,join(join(meet(X1,X2),meet(X2,join(X1,X2))),X2))),X2))),
inference(paramodulation,[status(thm)],[f673,f9]) ).
fof(f1180,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1)))))),X3),meet(join(meet(X0,join(join(meet(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),X4),meet(X5,join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))))),meet(X1,join(X0,join(join(meet(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),X4),meet(X5,join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))))))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1)))))),X3))) = join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1095]) ).
fof(f1181,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1)))))),X3),meet(join(meet(X0,join(join(meet(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),X4),meet(X5,join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))))),meet(X1,join(X0,join(join(meet(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),X4),meet(X5,join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))))))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1)))))),X3))) = join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),X1),meet(X1,join(join(meet(X2,X1),meet(X1,join(X2,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1180]) ).
fof(f1182,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1))),X4),meet(X5,join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1))))),meet(X1,join(X0,join(join(meet(join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1))),X4),meet(X5,join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1))))))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1)))))),X2))) = join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),X1),meet(X1,join(join(meet(X3,X1),meet(X1,join(X3,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1181]) ).
fof(f1183,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))),meet(X1,join(X0,join(join(meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),X3),meet(X4,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1)))))),X2))) = join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1182]) ).
fof(f1184,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))),meet(X1,join(X0,join(join(meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),X3),meet(X4,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1)))))),X2))) = join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1183]) ).
fof(f1185,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),X3),meet(X4,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1)))))),X2))) = join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1184]) ).
fof(f1186,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))),join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1)))))),X2))) = join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1185]) ).
fof(f1187,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,X1)),join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))))))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1)))))),X2))) = join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1186]) ).
fof(f1188,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),join(X0,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1)))))),X2))) = join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1187]) ).
fof(f1189,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1)))))),X2))) = join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1188]) ).
fof(f1190,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1),meet(X1,join(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),X1),meet(X1,join(join(meet(X5,X1),meet(X1,join(X5,X1))),X1))),X1))),
inference(forward_demodulation,[status(thm)],[f673,f1189]) ).
fof(f1191,plain,
! [X0,X1,X2,X3,X4] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = X1,
inference(forward_demodulation,[status(thm)],[f673,f1190]) ).
fof(f1251,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,join(X0,X1))) = X0,
inference(forward_demodulation,[status(thm)],[f673,f1066]) ).
fof(f1541,plain,
! [X0,X1,X2,X3,X4] : join(meet(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,X1),meet(X1,join(X0,X1)))),meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,X1),meet(X1,join(X0,X1)))))),X2),meet(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X3),meet(X4,join(meet(X0,X1),meet(X1,join(X0,X1))))),join(meet(X0,X1),meet(X1,join(X0,X1))))),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X3),meet(X4,join(meet(X0,X1),meet(X1,join(X0,X1))))),join(meet(X0,X1),meet(X1,join(X0,X1))))))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = join(meet(X0,X1),meet(X1,join(X0,X1))),
inference(paramodulation,[status(thm)],[f1251,f9]) ).
fof(f1586,plain,
! [X0,X1,X2,X3,X4] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X3),meet(X4,join(meet(X0,X1),meet(X1,join(X0,X1))))),join(meet(X0,X1),meet(X1,join(X0,X1))))),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X3),meet(X4,join(meet(X0,X1),meet(X1,join(X0,X1))))),join(meet(X0,X1),meet(X1,join(X0,X1))))))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = join(meet(X0,X1),meet(X1,join(X0,X1))),
inference(forward_demodulation,[status(thm)],[f1251,f1541]) ).
fof(f2343,plain,
! [X0,X1,X2,X3,X4] : join(meet(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X2),meet(X3,X1)),X1))))),meet(join(meet(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X2),meet(X3,X1)),X1))))))),X4),meet(X1,join(join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X2),meet(X3,X1)),X1))))),meet(join(meet(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)))),join(join(meet(X0,X1),meet(X1,join(X0,X1))),join(meet(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X2),meet(X3,X1)),X1))))))),X4))) = join(meet(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X2),meet(X3,X1)),X1)))),
inference(paramodulation,[status(thm)],[f1191,f1191]) ).
fof(f2371,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))))))),meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),join(X0,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))))))))),X5),meet(join(meet(X0,join(join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),X6),meet(X7,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))))),X2)),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(X0,join(join(meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),X6),meet(X7,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))))),join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))))))),join(join(meet(X0,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))))))),meet(join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),join(X0,join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))))))))),X5))) = join(meet(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))),meet(join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)))),join(join(meet(X1,X2),meet(X2,join(X1,X2))),join(meet(X1,join(join(meet(X2,X3),meet(X4,X2)),X2)),meet(X2,join(X1,join(join(meet(X2,X3),meet(X4,X2)),X2))))))),
inference(paramodulation,[status(thm)],[f1191,f9]) ).
fof(f2481,plain,
! [X0,X1,X2,X3,X4] : join(meet(X0,X1),meet(X0,join(join(meet(join(meet(X2,X0),meet(X0,join(X2,X0))),join(meet(X2,join(join(meet(X0,X3),meet(X4,X0)),X0)),meet(X0,join(X2,join(join(meet(X0,X3),meet(X4,X0)),X0))))),meet(join(meet(X2,join(join(meet(X0,X3),meet(X4,X0)),X0)),meet(X0,join(X2,join(join(meet(X0,X3),meet(X4,X0)),X0)))),join(join(meet(X2,X0),meet(X0,join(X2,X0))),join(meet(X2,join(join(meet(X0,X3),meet(X4,X0)),X0)),meet(X0,join(X2,join(join(meet(X0,X3),meet(X4,X0)),X0))))))),X1))) = join(meet(X2,join(join(meet(X0,X3),meet(X4,X0)),X0)),meet(X0,join(X2,join(join(meet(X0,X3),meet(X4,X0)),X0)))),
inference(forward_demodulation,[status(thm)],[f1191,f2343]) ).
fof(f2482,plain,
! [X0,X1,X2,X3,X4] : join(meet(X0,X1),meet(X0,join(X0,X1))) = join(meet(X2,join(join(meet(X0,X3),meet(X4,X0)),X0)),meet(X0,join(X2,join(join(meet(X0,X3),meet(X4,X0)),X0)))),
inference(forward_demodulation,[status(thm)],[f1191,f2481]) ).
fof(f2489,plain,
! [X0,X1,X2,X3] : X0 = join(meet(X1,join(join(meet(X0,X2),meet(X3,X0)),X0)),meet(X0,join(X1,join(join(meet(X0,X2),meet(X3,X0)),X0)))),
inference(forward_demodulation,[status(thm)],[f1251,f2482]) ).
fof(f2490,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),join(X0,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))))))))),X5),meet(join(meet(X0,join(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),X6),meet(X7,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))),X1)),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),X6),meet(X7,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))),join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))))))),meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),join(X0,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))))))))),X5))) = join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2371]) ).
fof(f2491,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(X1,join(X0,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))))))))),X5),meet(join(meet(X0,join(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),X6),meet(X7,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))),X1)),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),X6),meet(X7,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))),join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))))))),meet(join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),join(X0,join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))))))))),X5))) = join(meet(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))),meet(join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X2,X1),meet(X1,join(X2,X1))),join(meet(X2,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X2,join(join(meet(X1,X3),meet(X4,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2490]) ).
fof(f2492,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),X6),meet(X7,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))))),X1)),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),X6),meet(X7,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))))),join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))))))),meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),join(X0,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))))))))),X2))) = join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2491]) ).
fof(f2493,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2492]) ).
fof(f2494,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(X0,join(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2493]) ).
fof(f2495,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f2489,f2494]) ).
fof(f2496,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2495]) ).
fof(f2497,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,X1)),join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))))))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2496]) ).
fof(f2498,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(join(meet(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)),meet(X1,join(X0,join(join(meet(X1,X3),meet(X4,X1)),X1)))),join(join(meet(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))),meet(join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),join(X0,join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))))))))),X2))) = join(meet(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))),meet(join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)))),join(join(meet(X5,X1),meet(X1,join(X5,X1))),join(meet(X5,join(join(meet(X1,X6),meet(X7,X1)),X1)),meet(X1,join(X5,join(join(meet(X1,X6),meet(X7,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2497]) ).
fof(f2499,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(X1,join(join(meet(X0,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))))))),meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),join(X0,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))))))))),X2))) = join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f2489,f2498]) ).
fof(f2500,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(X1,join(join(meet(X0,X1),meet(join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),join(X0,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))))))))),X2))) = join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2499]) ).
fof(f2501,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))))))))),X2))) = join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2500]) ).
fof(f2502,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = join(meet(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))),meet(join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)))),join(join(meet(X3,X1),meet(X1,join(X3,X1))),join(meet(X3,join(join(meet(X1,X4),meet(X5,X1)),X1)),meet(X1,join(X3,join(join(meet(X1,X4),meet(X5,X1)),X1))))))),
inference(forward_demodulation,[status(thm)],[f1191,f2501]) ).
fof(f2512,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(join(meet(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),X1),meet(X1,join(join(meet(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),X1))),X5),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(join(meet(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(join(meet(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))),meet(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),join(X0,join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1))))))),X1),meet(X1,join(join(meet(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)),meet(X4,join(X1,meet(meet(join(X1,X2),join(X3,X1)),X1)))),X1))),X5))) = X1,
inference(backward_demodulation,[status(thm)],[f2531,f1090]) ).
fof(f2517,plain,
! [X0,X1,X2] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = join(meet(X0,X1),meet(X1,join(X0,X1))),
inference(backward_demodulation,[status(thm)],[f2531,f1586]) ).
fof(f2531,plain,
! [X0,X1,X2] : join(meet(join(meet(X0,X1),meet(X1,join(X0,X1))),X2),meet(X1,join(join(meet(X0,X1),meet(X1,join(X0,X1))),X2))) = X1,
inference(forward_demodulation,[status(thm)],[f1191,f2502]) ).
fof(f2632,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0),meet(X0,join(join(meet(join(meet(X4,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(X4,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(join(meet(X4,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(X4,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),X0))),X5),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(join(meet(join(meet(join(meet(X4,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(X4,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(join(meet(X4,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(X4,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),X0),meet(X0,join(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0))),X5))) = X0,
inference(forward_demodulation,[status(thm)],[f2531,f2512]) ).
fof(f2633,plain,
! [X0,X1,X2,X3,X4,X5] : join(meet(join(meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0),meet(X0,join(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0))),X4),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(join(meet(join(meet(join(meet(X5,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(join(meet(X5,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(X5,join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))))))),X0),meet(X0,join(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0))),X4))) = X0,
inference(forward_demodulation,[status(thm)],[f2531,f2632]) ).
fof(f2634,plain,
! [X0,X1,X2,X3,X4] : join(meet(join(meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0),meet(X0,join(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0))),X4),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(join(meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0),meet(X0,join(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0))),X4))) = X0,
inference(forward_demodulation,[status(thm)],[f2531,f2633]) ).
fof(f3028,plain,
! [X0,X1,X2,X3,X4] : join(meet(join(meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0),meet(X0,join(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),X0))),X4),meet(join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))),join(X0,X4))) = X0,
inference(backward_demodulation,[status(thm)],[f3058,f2634]) ).
fof(f3058,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,join(X1,X0))),
inference(forward_demodulation,[status(thm)],[f2531,f2517]) ).
fof(f3396,plain,
! [X0,X1,X2,X3,X4] : join(meet(X0,X1),meet(join(meet(X0,meet(meet(join(X0,X2),join(X3,X0)),X0)),meet(X4,join(X0,meet(meet(join(X0,X2),join(X3,X0)),X0)))),join(X0,X1))) = X0,
inference(forward_demodulation,[status(thm)],[f3058,f3028]) ).
fof(f3639,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(meet(meet(X1,X0),meet(X0,join(X1,X0))),meet(meet(X0,join(X1,X0)),X0)),
inference(paramodulation,[status(thm)],[f3058,f3058]) ).
fof(f3645,plain,
! [X0,X1] : join(meet(meet(X0,X1),meet(X1,join(X0,X1))),meet(meet(X0,X1),X1)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f3058,f1251]) ).
fof(f3888,plain,
! [X0,X1,X2,X3] : join(meet(X0,X1),meet(meet(meet(join(X0,X2),join(X3,X0)),X0),join(X0,X1))) = X0,
inference(paramodulation,[status(thm)],[f3058,f3396]) ).
fof(f3945,plain,
! [X0,X1,X2,X3] : join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)))) = X0,
inference(paramodulation,[status(thm)],[f3396,f2489]) ).
fof(f4093,plain,
! [X0,X1,X2] : meet(meet(join(X0,X1),join(X2,X0)),X0) = X0,
inference(paramodulation,[status(thm)],[f3058,f3888]) ).
fof(f4157,plain,
! [X0,X1,X2,X3] : join(meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0)),meet(X3,join(X0,X0))) = X0,
inference(backward_demodulation,[status(thm)],[f4093,f3945]) ).
fof(f4190,plain,
! [X0,X1] : join(meet(X0,X0),meet(X1,join(X0,X0))) = X0,
inference(forward_demodulation,[status(thm)],[f4093,f4157]) ).
fof(f4479,plain,
! [X0,X1,X2] : X0 = join(join(meet(X0,X1),meet(X2,X0)),X0),
inference(paramodulation,[status(thm)],[f2489,f4190]) ).
fof(f4712,plain,
! [X0,X1] : meet(meet(join(X0,X1),X0),X0) = X0,
inference(paramodulation,[status(thm)],[f4479,f4093]) ).
fof(f4884,plain,
! [X0,X1] : meet(meet(X0,meet(X1,X0)),meet(X1,X0)) = meet(X1,X0),
inference(paramodulation,[status(thm)],[f3058,f4712]) ).
fof(f4885,plain,
! [X0,X1] : meet(meet(X0,meet(X0,X1)),meet(X0,X1)) = meet(X0,X1),
inference(paramodulation,[status(thm)],[f1251,f4712]) ).
fof(f6108,plain,
! [X0,X1] : meet(meet(X0,meet(meet(join(X0,X1),X0),X0)),X0) = meet(meet(join(X0,X1),X0),X0),
inference(paramodulation,[status(thm)],[f4712,f4884]) ).
fof(f6180,plain,
! [X0,X1] : meet(meet(X0,X0),X0) = meet(meet(join(X0,X1),X0),X0),
inference(forward_demodulation,[status(thm)],[f4712,f6108]) ).
fof(f6199,plain,
! [X0] : meet(meet(X0,X0),X0) = X0,
inference(forward_demodulation,[status(thm)],[f4712,f6180]) ).
fof(f6263,plain,
! [X0] : meet(X0,join(meet(X0,X0),X0)) = join(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0)),
inference(paramodulation,[status(thm)],[f6199,f3639]) ).
fof(f6267,plain,
! [X0] : X0 = join(X0,meet(X0,join(meet(X0,X0),X0))),
inference(paramodulation,[status(thm)],[f6199,f3058]) ).
fof(f6375,plain,
! [X0,X1] : meet(meet(X0,join(X1,X0)),X0) = X0,
inference(paramodulation,[status(thm)],[f6267,f4093]) ).
fof(f6379,plain,
! [X0] : meet(meet(X0,join(meet(X0,X0),X0)),join(X0,meet(X0,join(meet(X0,X0),X0)))) = join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0)),meet(meet(meet(X0,join(meet(X0,X0),X0)),join(X0,meet(X0,join(meet(X0,X0),X0)))),meet(X0,join(meet(X0,X0),X0)))),
inference(paramodulation,[status(thm)],[f6267,f3639]) ).
fof(f6382,plain,
! [X0] : join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0)),meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(X0,join(meet(X0,X0),X0)))) = meet(X0,meet(X0,join(meet(X0,X0),X0))),
inference(paramodulation,[status(thm)],[f6267,f3645]) ).
fof(f6388,plain,
! [X0] : meet(meet(X0,join(meet(X0,X0),X0)),X0) = join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0)),meet(meet(meet(X0,join(meet(X0,X0),X0)),join(X0,meet(X0,join(meet(X0,X0),X0)))),meet(X0,join(meet(X0,X0),X0)))),
inference(forward_demodulation,[status(thm)],[f6267,f6379]) ).
fof(f6389,plain,
! [X0] : meet(meet(X0,join(meet(X0,X0),X0)),X0) = join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0)),meet(meet(meet(X0,join(meet(X0,X0),X0)),X0),meet(X0,join(meet(X0,X0),X0)))),
inference(forward_demodulation,[status(thm)],[f6267,f6388]) ).
fof(f6398,plain,
! [X0] : meet(meet(X0,join(meet(X0,X0),X0)),X0) = join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0)),meet(X0,meet(X0,join(meet(X0,X0),X0)))),
inference(backward_demodulation,[status(thm)],[f6375,f6389]) ).
fof(f6399,plain,
! [X0] : meet(X0,join(meet(X0,X0),X0)) = join(meet(X0,meet(X0,join(meet(X0,X0),X0))),X0),
inference(backward_demodulation,[status(thm)],[f6375,f6263]) ).
fof(f6413,plain,
! [X0] : X0 = join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0)),meet(X0,meet(X0,join(meet(X0,X0),X0)))),
inference(forward_demodulation,[status(thm)],[f6375,f6398]) ).
fof(f6414,plain,
! [X0] : X0 = join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),X0),meet(X0,meet(X0,join(meet(X0,X0),X0)))),
inference(forward_demodulation,[status(thm)],[f6375,f6413]) ).
fof(f6418,plain,
! [X0] : join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),X0),meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(X0,join(meet(X0,X0),X0)))) = meet(X0,meet(X0,join(meet(X0,X0),X0))),
inference(forward_demodulation,[status(thm)],[f6375,f6382]) ).
fof(f6419,plain,
! [X0] : join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),X0),meet(X0,join(meet(X0,X0),X0))) = meet(X0,meet(X0,join(meet(X0,X0),X0))),
inference(forward_demodulation,[status(thm)],[f4885,f6418]) ).
fof(f6463,plain,
! [X0,X1] : meet(meet(meet(X0,join(X1,X0)),X0),meet(X0,join(X1,X0))) = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f3058,f6375]) ).
fof(f6554,plain,
! [X0] : X0 = join(meet(meet(X0,meet(X0,join(meet(X0,X0),X0))),X0),meet(X0,join(meet(X0,X0),X0))),
inference(backward_demodulation,[status(thm)],[f6569,f6414]) ).
fof(f6556,plain,
! [X0] : meet(X0,join(meet(X0,X0),X0)) = join(meet(X0,join(meet(X0,X0),X0)),X0),
inference(backward_demodulation,[status(thm)],[f6569,f6399]) ).
fof(f6569,plain,
! [X0,X1] : meet(X0,meet(X0,join(X1,X0))) = meet(X0,join(X1,X0)),
inference(forward_demodulation,[status(thm)],[f6375,f6463]) ).
fof(f6646,plain,
! [X0] : X0 = meet(X0,meet(X0,join(meet(X0,X0),X0))),
inference(forward_demodulation,[status(thm)],[f6419,f6554]) ).
fof(f6649,plain,
! [X0] : meet(X0,join(meet(X0,X0),X0)) = join(X0,X0),
inference(backward_demodulation,[status(thm)],[f6652,f6556]) ).
fof(f6652,plain,
! [X0] : X0 = meet(X0,join(meet(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f6569,f6646]) ).
fof(f6653,plain,
a != a,
inference(backward_demodulation,[status(thm)],[f6679,f4]) ).
fof(f6679,plain,
! [X0] : X0 = join(X0,X0),
inference(forward_demodulation,[status(thm)],[f6652,f6649]) ).
fof(f7215,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f6653]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT094-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n012.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 23:11:21 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 223.85/28.53 % Refutation found
% 223.85/28.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 223.85/28.53 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.03/28.91 % Elapsed time: 28.551133 seconds
% 14.03/28.91 % CPU time: 225.064551 seconds
% 14.03/28.91 % Total memory used: 8.742 GB
% 14.03/28.91 % Net memory used: 8.692 GB
%------------------------------------------------------------------------------