%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT010-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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 : Tue Sep 29 11:45:49 AM UTC 2026
% Result : Unsatisfiable 18.34s 3.23s
% Output : Refutation 18.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 13
% Syntax : Number of formulae : 407 ( 407 unt; 1 def)
% Number of atoms : 407 ( 378 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 1299 (1299 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,X3)))) = join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),meet(X2,X3)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n5_1) ).
fof(f10,axiom,
! [X2,X3,X0,X1] : join(X0,meet(X1,join(X2,meet(X0,X3)))) = meet(join(X0,meet(X1,join(X0,X2))),join(X0,meet(join(X0,X1),join(X2,X3)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',n5_2) ).
fof(f11,axiom,
! [X2,X0,X1] : meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))) = join(meet(X2,join(X0,meet(X1,X2))),meet(X0,join(X1,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nr_3) ).
fof(f12,negated_conjecture,
meet(a,meet(join(b,c),join(b,d))) != meet(meet(a,meet(join(b,c),join(b,d))),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f13,definition,
~ sP0(meet(a,meet(join(b,c),join(b,d)))),
introduced(definition,[new_symbols(definition,[sP0])],[inequality_splitting_name_introduction]) ).
fof(f14,plain,
sP0(meet(meet(a,meet(join(b,c),join(b,d))),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d))))),
inference(inequality_splitting,[],[f12,f13]) ).
fof(f15,plain,
sP0(meet(a,meet(meet(join(b,c),join(b,d)),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d)))))),
inference(forward_demodulation,[],[f14,f7]) ).
fof(f16,plain,
! [X2,X0,X1] : meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))) = join(meet(X0,join(X1,X2)),meet(X2,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f11,f6]) ).
fof(f17,plain,
sP0(meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d))))))),
inference(forward_demodulation,[],[f15,f7]) ).
fof(f24,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(X1,meet(X2,join(X0,X3))))),
inference(superposition,[],[f3,f9]) ).
fof(f25,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,meet(join(X1,meet(X0,X2)),meet(X0,join(X1,meet(X2,join(X0,X3)))))),
inference(forward_demodulation,[],[f24,f7]) ).
fof(f93,plain,
! [X0,X1] : meet(join(X0,meet(X0,X1)),join(X1,meet(X0,X0))) = join(X0,meet(X1,join(X0,meet(X0,X1)))),
inference(superposition,[],[f16,f3]) ).
fof(f94,plain,
! [X2,X3,X0,X1] : meet(join(join(X0,meet(X1,join(X0,X2))),meet(X0,meet(join(X0,X1),join(X2,X3)))),join(meet(join(X0,X1),join(X2,X3)),meet(join(X0,meet(X1,join(X0,X2))),X0))) = join(join(X0,meet(X1,join(X2,meet(X0,X3)))),meet(meet(join(X0,X1),join(X2,X3)),join(join(X0,meet(X1,join(X0,X2))),meet(X0,meet(join(X0,X1),join(X2,X3)))))),
inference(superposition,[],[f16,f10]) ).
fof(f95,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(X1,X0))) = join(meet(X1,join(X0,join(X0,X2))),meet(join(X0,X2),join(X1,X0))),
inference(superposition,[],[f16,f3]) ).
fof(f102,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,X2),meet(X2,join(X0,join(X0,meet(X1,X2)))))) = join(meet(X0,join(join(X1,X2),meet(X0,X2))),meet(X0,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))),
inference(superposition,[],[f9,f16]) ).
fof(f111,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,X2),meet(X2,join(X0,join(X0,meet(X1,X2)))))) = join(meet(X0,join(X1,join(X2,meet(X0,X2)))),meet(X0,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f102,f8]) ).
fof(f118,plain,
! [X2,X0,X1] : join(meet(X1,join(X0,join(X0,X2))),meet(join(X0,X2),join(X1,X0))) = meet(join(X1,X0),join(X0,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f95,f8]) ).
fof(f119,plain,
! [X2,X3,X0,X1] : meet(join(join(X0,meet(X1,join(X0,X2))),meet(X0,meet(join(X0,X1),join(X2,X3)))),join(meet(join(X0,X1),join(X2,X3)),meet(join(X0,meet(X1,join(X0,X2))),X0))) = join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(meet(join(X0,X1),join(X2,X3)),join(join(X0,meet(X1,join(X0,X2))),meet(X0,meet(join(X0,X1),join(X2,X3))))))),
inference(forward_demodulation,[],[f94,f8]) ).
fof(f120,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = meet(X0,join(X1,meet(X0,X0))),
inference(forward_demodulation,[],[f93,f4]) ).
fof(f125,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,join(X2,meet(X0,X2)))),meet(X0,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))) = meet(X0,join(X1,join(X2,meet(X2,join(X0,join(X0,meet(X1,X2))))))),
inference(forward_demodulation,[],[f111,f8]) ).
fof(f132,plain,
! [X2,X3,X0,X1] : meet(join(join(X0,meet(X1,join(X0,X2))),meet(X0,meet(join(X0,X1),join(X2,X3)))),join(meet(join(X0,X1),join(X2,X3)),meet(join(X0,meet(X1,join(X0,X2))),X0))) = join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(join(X0,meet(X1,join(X0,X2))),meet(X0,meet(join(X0,X1),join(X2,X3)))))))),
inference(forward_demodulation,[],[f119,f7]) ).
fof(f133,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f120,f1]) ).
fof(f137,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,join(X2,meet(X0,X2)))),meet(X0,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f125,f4]) ).
fof(f143,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3))))),join(meet(join(X0,X1),join(X2,X3)),meet(join(X0,meet(X1,join(X0,X2))),X0))) = join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3))))))))),
inference(forward_demodulation,[],[f132,f8]) ).
fof(f147,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,meet(X2,join(X0,X2)))),meet(X0,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f137,f133]) ).
fof(f153,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3))))))))) = meet(join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3))))),join(meet(join(X0,X1),join(X2,X3)),meet(X0,join(X0,meet(X1,join(X0,X2)))))),
inference(forward_demodulation,[],[f143,f5]) ).
fof(f157,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3))))))))) = meet(join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3))))),join(meet(join(X0,X1),join(X2,X3)),X0)),
inference(forward_demodulation,[],[f153,f3]) ).
fof(f159,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3))))))))) = meet(join(meet(join(X0,X1),join(X2,X3)),X0),join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3)))))),
inference(forward_demodulation,[],[f157,f5]) ).
fof(f161,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3))))))))) = meet(join(X0,meet(join(X0,X1),join(X2,X3))),join(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(join(X0,X1),join(X2,X3)))))),
inference(forward_demodulation,[],[f159,f6]) ).
fof(f177,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,X1)),join(X1,meet(X2,X0))) = join(meet(join(X0,X1),X2),meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f16,f5]) ).
fof(f179,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f180,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,meet(X2,join(X1,X3)))) = join(meet(X1,join(X0,meet(X1,X2))),meet(X1,join(meet(X0,X1),meet(X2,X3)))),
inference(superposition,[],[f9,f5]) ).
fof(f182,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X1,join(X2,X0)))) = join(meet(X2,join(X3,meet(X2,X1))),meet(X2,join(meet(X2,X3),meet(X0,X1)))),
inference(superposition,[],[f9,f5]) ).
fof(f183,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,X1)),join(X0,meet(X2,X1))) = join(meet(X2,join(X1,X0)),meet(X0,join(X2,meet(X0,X1)))),
inference(superposition,[],[f16,f5]) ).
fof(f184,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(join(X2,meet(X3,join(X2,X0))),join(X2,meet(join(X0,X1),join(X2,X3)))),
inference(superposition,[],[f10,f5]) ).
fof(f185,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = X0,
inference(backward_demodulation,[],[f133,f179]) ).
fof(f187,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,X2)),meet(X0,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))),
inference(backward_demodulation,[],[f147,f185]) ).
fof(f200,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,join(X2,meet(X1,X3)))) = meet(join(X1,meet(X0,join(X1,X2))),join(X1,meet(join(X0,X1),join(X2,X3)))),
inference(superposition,[],[f10,f6]) ).
fof(f201,plain,
! [X2,X3,X0,X1] : join(X1,meet(X2,join(X0,meet(X1,X3)))) = meet(join(X1,meet(X2,join(X0,X1))),join(X1,meet(join(X1,X2),join(X0,X3)))),
inference(superposition,[],[f10,f6]) ).
fof(f202,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X1,meet(X2,X0)))) = meet(join(X2,meet(X3,join(X2,X1))),join(X2,meet(join(X2,X3),join(X0,X1)))),
inference(superposition,[],[f10,f6]) ).
fof(f206,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X0,join(X2,X1)))) = join(meet(X2,join(X3,meet(X2,X0))),meet(X2,join(meet(X0,X1),meet(X2,X3)))),
inference(superposition,[],[f9,f6]) ).
fof(f209,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f225,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f238,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,join(meet(X1,join(X0,X2)),meet(X0,join(X2,X3)))))))) = meet(join(X0,meet(join(X0,X1),join(X2,X3))),join(X0,join(meet(X1,join(X0,X2)),meet(X0,join(X2,X3))))),
inference(backward_demodulation,[],[f161,f209]) ).
fof(f239,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,X2)),meet(X0,join(X2,meet(X0,X1)))),
inference(backward_demodulation,[],[f187,f209]) ).
fof(f253,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f179,f3]) ).
fof(f257,plain,
! [X2,X0,X1] : join(X2,meet(X0,meet(X1,X2))) = X2,
inference(superposition,[],[f179,f7]) ).
fof(f259,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X0,join(X1,X2)))) = join(meet(X1,X0),meet(X1,join(meet(X1,X0),meet(X0,X2)))),
inference(superposition,[],[f9,f179]) ).
fof(f260,plain,
! [X2,X0,X1] : join(join(X0,X1),meet(X2,join(X0,meet(join(X0,X1),X1)))) = meet(join(join(X0,X1),meet(X2,join(join(X0,X1),X0))),join(X0,X1)),
inference(superposition,[],[f10,f179]) ).
fof(f266,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,meet(X0,X1))))) = join(meet(X0,join(X1,meet(X0,X2))),meet(X0,meet(X0,X1))),
inference(superposition,[],[f9,f179]) ).
fof(f267,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,meet(X0,X1))))) = join(meet(X0,meet(X0,X1)),meet(X0,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f266,f6]) ).
fof(f271,plain,
! [X2,X0,X1] : join(join(X0,X1),meet(X2,join(X0,meet(join(X0,X1),X1)))) = meet(join(X0,X1),join(join(X0,X1),meet(X2,join(join(X0,X1),X0)))),
inference(forward_demodulation,[],[f260,f5]) ).
fof(f272,plain,
! [X2,X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X1,join(meet(X1,X0),meet(X0,X2)))),
inference(forward_demodulation,[],[f259,f4]) ).
fof(f277,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f253,f6]) ).
fof(f278,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = join(meet(X0,meet(X0,X1)),meet(X0,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f267,f4]) ).
fof(f281,plain,
! [X2,X0,X1] : join(X0,X1) = join(join(X0,X1),meet(X2,join(X0,meet(join(X0,X1),X1)))),
inference(forward_demodulation,[],[f271,f3]) ).
fof(f288,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(X2,meet(X1,X0)))) = join(meet(X1,join(X0,X2)),meet(join(X0,X2),join(X1,X0))),
inference(backward_demodulation,[],[f118,f277]) ).
fof(f291,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(X2,join(X0,meet(join(X0,X1),X1))))),
inference(forward_demodulation,[],[f281,f8]) ).
fof(f297,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(X2,join(X0,meet(X1,join(X0,X1)))))),
inference(forward_demodulation,[],[f291,f5]) ).
fof(f300,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f297,f185]) ).
fof(f302,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f314,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f349,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f185,f4]) ).
fof(f351,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f185,f179]) ).
fof(f354,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(X1,X2))) = X2,
inference(superposition,[],[f185,f8]) ).
fof(f357,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X0,meet(X1,X2)))) = meet(join(X1,X0),join(X1,meet(join(X1,X0),join(X0,X2)))),
inference(superposition,[],[f10,f185]) ).
fof(f360,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f185]) ).
fof(f365,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f179,f185]) ).
fof(f369,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f365,f6]) ).
fof(f376,plain,
! [X2,X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X1,meet(join(X1,X0),join(X0,X2)))),
inference(forward_demodulation,[],[f357,f3]) ).
fof(f379,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f351,f5]) ).
fof(f381,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f349,f5]) ).
fof(f395,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = join(meet(X0,X1),meet(X0,join(X1,meet(X0,X2)))),
inference(backward_demodulation,[],[f278,f381]) ).
fof(f423,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,join(X1,X2))),
inference(superposition,[],[f369,f8]) ).
fof(f431,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(join(X0,X1),X2)),
inference(superposition,[],[f8,f369]) ).
fof(f441,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,join(X1,X2))),
inference(forward_demodulation,[],[f431,f8]) ).
fof(f462,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f381,f7]) ).
fof(f472,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(X3,meet(X2,X0))),meet(X2,join(meet(X2,X3),meet(X0,X1)))) = meet(X2,join(X3,meet(X0,join(X2,meet(X0,X1))))),
inference(superposition,[],[f9,f381]) ).
fof(f478,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X0,join(X2,X1)))) = meet(X2,join(X3,meet(X0,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f472,f9]) ).
fof(f482,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(meet(X1,X2),meet(X0,X1))),
inference(forward_demodulation,[],[f462,f225]) ).
fof(f485,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(meet(X1,X2),X0))),
inference(forward_demodulation,[],[f482,f225]) ).
fof(f487,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f485,f7]) ).
fof(f488,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f487,f381]) ).
fof(f499,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),join(X1,meet(X0,X2)))) = meet(join(X0,join(X0,X1)),join(X0,meet(join(X0,join(X0,X1)),join(X1,X2)))),
inference(superposition,[],[f10,f1]) ).
fof(f504,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,meet(join(X0,X1),join(X1,X2)))) = join(X0,meet(join(X0,X1),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f499,f277]) ).
fof(f512,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f504,f376]) ).
fof(f548,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X1,join(X0,X2)))) = join(meet(X0,meet(X0,X1)),meet(X0,join(meet(X0,meet(X0,X1)),meet(X1,X2)))),
inference(superposition,[],[f9,f2]) ).
fof(f553,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,join(meet(X0,X1),meet(X1,X2)))) = meet(X0,join(meet(X0,X1),meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f548,f381]) ).
fof(f561,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f553,f272]) ).
fof(f589,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f302,f6]) ).
fof(f622,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(join(X0,X1),join(X2,X3))),join(X0,meet(X1,join(X0,X2)))) = join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,meet(X1,join(X0,X2))))))),
inference(backward_demodulation,[],[f238,f589]) ).
fof(f631,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,join(X0,X2))),join(X0,meet(join(X0,X1),join(X2,X3)))) = join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,meet(X1,join(X0,X2))))))),
inference(forward_demodulation,[],[f622,f5]) ).
fof(f634,plain,
! [X2,X3,X0,X1] : join(X0,meet(X1,join(X2,meet(X0,X3)))) = join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X0,X1),meet(join(X2,X3),join(X0,meet(X1,join(X0,X2))))))),
inference(forward_demodulation,[],[f631,f10]) ).
fof(f651,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f209,f5]) ).
fof(f655,plain,
! [X2,X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X2,join(X0,X1))),
inference(superposition,[],[f209,f185]) ).
fof(f674,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(X0,X1))) = X0,
inference(forward_demodulation,[],[f655,f3]) ).
fof(f882,plain,
! [X2,X0,X1] : join(X1,meet(X2,join(X0,X1))) = meet(join(X1,meet(X2,join(X0,X1))),join(X0,X1)),
inference(superposition,[],[f185,f300]) ).
fof(f892,plain,
! [X2,X0,X1] : join(X1,meet(X2,join(X0,X1))) = meet(join(X0,X1),join(X1,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f882,f5]) ).
fof(f962,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X1,meet(X0,X2)),meet(X0,join(X0,X1)))) = join(meet(X0,join(join(X0,X1),join(X1,meet(X0,X2)))),meet(join(X1,meet(X0,X2)),join(X0,X1))),
inference(superposition,[],[f16,f512]) ).
fof(f988,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X1,meet(X0,X2)),meet(X0,join(X0,X1)))) = join(meet(join(X1,meet(X0,X2)),join(X0,X1)),meet(X0,join(join(X0,X1),join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f962,f6]) ).
fof(f1015,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X1,meet(X0,X2)),meet(X0,join(X0,X1)))) = join(meet(join(X1,meet(X0,X2)),join(X0,X1)),meet(X0,join(X1,join(meet(X0,X2),join(X0,X1))))),
inference(forward_demodulation,[],[f988,f314]) ).
fof(f1027,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X1,meet(X0,X2)),meet(X0,join(X0,X1)))) = join(meet(join(X1,meet(X0,X2)),join(X0,X1)),meet(X0,join(meet(X0,X2),join(X0,X1)))),
inference(forward_demodulation,[],[f1015,f423]) ).
fof(f1033,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X1,meet(X0,X2)),meet(X0,join(X0,X1)))) = join(meet(join(X1,meet(X0,X2)),join(X0,X1)),X0),
inference(forward_demodulation,[],[f1027,f674]) ).
fof(f1037,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(join(X1,meet(X0,X2)),meet(X0,join(X0,X1)))) = join(X0,meet(join(X1,meet(X0,X2)),join(X0,X1))),
inference(forward_demodulation,[],[f1033,f6]) ).
fof(f1039,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),join(X1,meet(X0,X2)))) = meet(join(X0,X1),join(join(X1,meet(X0,X2)),meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f1037,f5]) ).
fof(f1040,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),join(X1,meet(X0,X2)))) = meet(join(X0,X1),join(X1,join(meet(X0,X2),meet(X0,join(X0,X1))))),
inference(forward_demodulation,[],[f1039,f8]) ).
fof(f1041,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),join(X1,meet(X0,X2)))) = meet(join(X0,X1),join(X1,join(meet(X0,X2),X0))),
inference(forward_demodulation,[],[f1040,f3]) ).
fof(f1042,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),join(X1,meet(X0,X2)))) = meet(join(X0,X1),join(X1,join(X0,meet(X0,X2)))),
inference(forward_demodulation,[],[f1041,f6]) ).
fof(f1043,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),join(X1,meet(X0,X2)))) = meet(join(X0,X1),join(X1,X0)),
inference(forward_demodulation,[],[f1042,f4]) ).
fof(f1044,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(forward_demodulation,[],[f1043,f512]) ).
fof(f1074,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(X1,X0))) = join(meet(join(X0,join(X0,X2)),X1),meet(join(X0,X2),join(X1,X0))),
inference(superposition,[],[f177,f3]) ).
fof(f1092,plain,
! [X2,X0,X1] : join(join(X1,X2),meet(X2,join(X0,meet(X1,X2)))) = join(join(X1,X2),meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1)))),
inference(superposition,[],[f302,f177]) ).
fof(f1097,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(meet(join(X1,X2),X0),meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1)))),
inference(superposition,[],[f3,f177]) ).
fof(f1104,plain,
! [X2,X3,X0,X1] : meet(meet(join(X1,X2),X0),X3) = meet(meet(join(X1,X2),X0),meet(meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))),X3)),
inference(superposition,[],[f209,f177]) ).
fof(f1110,plain,
! [X2,X3,X0,X1] : meet(meet(join(X1,X2),X0),X3) = meet(join(X1,X2),meet(X0,meet(meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))),X3))),
inference(forward_demodulation,[],[f1104,f7]) ).
fof(f1116,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(join(X1,X2),meet(X0,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f1097,f7]) ).
fof(f1121,plain,
! [X2,X0,X1] : join(join(X1,X2),meet(X2,join(X0,meet(X1,X2)))) = join(X1,join(X2,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f1092,f8]) ).
fof(f1137,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(X1,X0))) = join(meet(join(X0,X2),join(X1,X0)),meet(join(X0,join(X0,X2)),X1)),
inference(forward_demodulation,[],[f1074,f6]) ).
fof(f1159,plain,
! [X2,X3,X0,X1] : meet(meet(join(X1,X2),X0),X3) = meet(join(X1,X2),meet(X0,meet(join(X0,meet(X1,X2)),meet(join(X2,meet(X0,X1)),X3)))),
inference(forward_demodulation,[],[f1110,f7]) ).
fof(f1163,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(join(X1,X2),meet(X0,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f1116,f209]) ).
fof(f1168,plain,
! [X2,X0,X1] : join(X1,join(X2,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))) = join(X1,join(X2,meet(X2,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f1121,f8]) ).
fof(f1182,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(X1,X0))) = join(meet(join(X0,X2),join(X1,X0)),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f1137,f277]) ).
fof(f1200,plain,
! [X2,X3,X0,X1] : meet(meet(join(X1,X2),X0),X3) = meet(join(X1,X2),meet(X0,meet(join(X2,meet(X0,X1)),X3))),
inference(forward_demodulation,[],[f1159,f209]) ).
fof(f1206,plain,
! [X2,X0,X1] : join(X1,X2) = join(X1,join(X2,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f1168,f4]) ).
fof(f1220,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(X1,X0))) = join(meet(join(X0,X2),X1),meet(join(X0,X2),join(X1,X0))),
inference(forward_demodulation,[],[f1182,f6]) ).
fof(f1236,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),meet(X0,X3)) = meet(join(X1,X2),meet(X0,meet(join(X2,meet(X0,X1)),X3))),
inference(forward_demodulation,[],[f1200,f7]) ).
fof(f1255,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(X2,meet(X1,X0)))) = join(meet(join(X0,X2),X1),meet(join(X0,X2),join(X1,X0))),
inference(forward_demodulation,[],[f1220,f8]) ).
fof(f1414,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X2,meet(X1,join(X0,X1))))) = meet(join(X1,meet(X0,join(X1,X2))),join(X1,join(X0,X1))),
inference(superposition,[],[f200,f185]) ).
fof(f1464,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X2,meet(X1,join(X0,X1))))) = meet(join(X1,join(X0,X1)),join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f1414,f5]) ).
fof(f1527,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X2,meet(X1,join(X0,X1))))) = meet(join(X0,X1),join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f1464,f369]) ).
fof(f1570,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X2,X1))) = meet(join(X0,X1),join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f1527,f185]) ).
fof(f1691,plain,
! [X2,X3,X0,X1,X4] : join(X0,meet(join(meet(X0,X2),X1),join(X3,meet(X0,X4)))) = meet(join(X0,meet(join(meet(X0,X2),X1),join(X3,X0))),join(X0,meet(join(X0,X1),join(X3,X4)))),
inference(superposition,[],[f201,f302]) ).
fof(f1699,plain,
! [X2,X3,X0,X1] : join(X1,meet(X2,join(X0,meet(X1,meet(X3,X0))))) = meet(join(X1,meet(X2,join(X0,X1))),join(X1,meet(join(X1,X2),X0))),
inference(superposition,[],[f201,f179]) ).
fof(f1710,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,meet(X0,join(X0,X1))))) = meet(join(X0,meet(X1,join(X2,X0))),join(X0,join(X0,X1))),
inference(superposition,[],[f201,f185]) ).
fof(f1713,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(join(X2,meet(X3,join(X0,X2))),join(X2,meet(join(X0,X1),join(X2,X3)))),
inference(superposition,[],[f201,f5]) ).
fof(f1764,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,meet(X0,join(X0,X1))))) = meet(join(X0,join(X0,X1)),join(X0,meet(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f1710,f5]) ).
fof(f1773,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X1,meet(X2,join(X0,X1))),join(X1,meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f1699,f257]) ).
fof(f1830,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,meet(X0,join(X0,X1))))) = meet(join(X0,X1),join(X0,meet(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f1764,f277]) ).
fof(f1878,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X2,X0))) = meet(join(X0,X1),join(X0,meet(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f1830,f3]) ).
fof(f2001,plain,
! [X2,X3,X0,X1] : join(X1,meet(X2,join(join(X0,X1),meet(X1,X3)))) = meet(join(X1,meet(X2,join(X0,X1))),join(X1,meet(join(X1,X2),join(X3,join(X0,X1))))),
inference(superposition,[],[f202,f369]) ).
fof(f2140,plain,
! [X2,X3,X0,X1] : join(X1,meet(X2,join(X0,join(X1,meet(X1,X3))))) = meet(join(X1,meet(X2,join(X0,X1))),join(X1,meet(join(X1,X2),join(X3,join(X0,X1))))),
inference(forward_demodulation,[],[f2001,f8]) ).
fof(f2199,plain,
! [X2,X3,X0,X1] : join(X1,meet(X2,join(X0,X1))) = meet(join(X1,meet(X2,join(X0,X1))),join(X1,meet(join(X1,X2),join(X3,join(X0,X1))))),
inference(forward_demodulation,[],[f2140,f4]) ).
fof(f2336,plain,
! [X2,X0,X1] : meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X0,X1)))),
inference(superposition,[],[f561,f369]) ).
fof(f2355,plain,
! [X2,X0,X1] : meet(join(X0,meet(meet(X0,X1),meet(X1,join(X0,X2)))),join(meet(X1,join(X0,X2)),meet(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(meet(X1,join(X0,X2)),join(X0,meet(meet(X0,X1),meet(X1,join(X0,X2)))))),
inference(superposition,[],[f16,f561]) ).
fof(f2376,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,join(meet(join(X0,X1),X2),meet(X1,meet(X2,join(join(X0,X1),X3)))))) = meet(join(X1,meet(X0,join(X1,meet(join(X0,X1),X2)))),join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f200,f561]) ).
fof(f2383,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,join(meet(join(X0,X1),X2),meet(X1,meet(X2,join(join(X0,X1),X3)))))) = meet(join(X1,meet(join(X0,X1),X2)),join(X1,meet(X0,join(X1,meet(join(X0,X1),X2))))),
inference(forward_demodulation,[],[f2376,f5]) ).
fof(f2399,plain,
! [X2,X0,X1] : meet(join(X0,meet(meet(X0,X1),meet(X1,join(X0,X2)))),join(meet(X1,join(X0,X2)),meet(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(X1,meet(join(X0,X2),join(X0,meet(meet(X0,X1),meet(X1,join(X0,X2))))))),
inference(forward_demodulation,[],[f2355,f7]) ).
fof(f2428,plain,
! [X2,X3,X0,X1] : meet(join(X1,meet(join(X0,X1),X2)),join(X1,meet(X0,join(X1,meet(join(X0,X1),X2))))) = join(X1,meet(X0,join(meet(join(X0,X1),X2),meet(X1,meet(X2,join(X0,join(X1,X3))))))),
inference(forward_demodulation,[],[f2383,f8]) ).
fof(f2438,plain,
! [X2,X0,X1] : meet(join(X0,meet(X1,meet(join(X0,X2),meet(X0,X1)))),join(meet(X1,join(X0,X2)),meet(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(X1,meet(join(X0,X2),join(X0,meet(X1,meet(join(X0,X2),meet(X0,X1))))))),
inference(forward_demodulation,[],[f2399,f225]) ).
fof(f2458,plain,
! [X2,X0,X1] : meet(join(X0,meet(X1,meet(join(X0,X2),X0))),join(meet(X1,join(X0,X2)),meet(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(X1,meet(join(X0,X2),join(X0,meet(X1,meet(join(X0,X2),X0)))))),
inference(forward_demodulation,[],[f2438,f488]) ).
fof(f2469,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(X1,meet(join(X0,X2),X0))),
inference(forward_demodulation,[],[f2458,f257]) ).
fof(f2477,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(X1,meet(X0,join(X0,X2)))),
inference(forward_demodulation,[],[f2469,f5]) ).
fof(f2481,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X0)) = meet(X0,join(meet(X1,join(X0,X2)),meet(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f2477,f3]) ).
fof(f2484,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X0)) = meet(X0,join(meet(X1,join(X0,X2)),meet(X0,X1))),
inference(forward_demodulation,[],[f2481,f381]) ).
fof(f2487,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X1,join(X0,X2)))) = join(meet(X0,X1),meet(X1,X0)),
inference(forward_demodulation,[],[f2484,f6]) ).
fof(f2490,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X1,X0)),
inference(forward_demodulation,[],[f2487,f561]) ).
fof(f2578,plain,
! [X2,X3,X0,X1] : join(X0,meet(join(X2,X3),join(X0,X1))) = join(X0,join(meet(join(X2,X3),join(X0,X1)),join(X0,meet(X1,join(X2,meet(X0,X3)))))),
inference(superposition,[],[f300,f184]) ).
fof(f2604,plain,
! [X2,X3,X0,X1] : join(X0,meet(join(X2,X3),join(X0,X1))) = join(meet(join(X2,X3),join(X0,X1)),join(X0,meet(X1,join(X2,meet(X0,X3))))),
inference(forward_demodulation,[],[f2578,f441]) ).
fof(f2684,plain,
! [X2,X3,X0,X1] : join(X0,meet(join(X2,X3),join(X0,X1))) = join(X0,join(meet(X1,join(X2,meet(X0,X3))),meet(join(X2,X3),join(X0,X1)))),
inference(forward_demodulation,[],[f2604,f314]) ).
fof(f2970,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(meet(X0,X1),meet(X2,meet(X1,X0))))) = meet(join(X2,meet(X3,join(meet(X0,X1),X2))),join(X2,meet(join(X2,X3),meet(X0,X1)))),
inference(superposition,[],[f201,f2490]) ).
fof(f2983,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,meet(X0,X1))) = join(X2,meet(X3,join(meet(X0,X1),meet(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f2970,f1773]) ).
fof(f3156,plain,
! [X2,X3,X0,X1] : join(meet(X0,X2),meet(X0,join(X2,meet(X0,X1)))) = meet(X0,join(X2,meet(join(meet(X0,X1),meet(X1,join(X0,X3))),X0))),
inference(superposition,[],[f395,f561]) ).
fof(f3252,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(X0,join(meet(X0,X1),meet(X1,join(X0,X3)))))) = join(meet(X0,X2),meet(X0,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f3156,f5]) ).
fof(f3303,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,join(X2,meet(X0,join(meet(X0,X1),meet(X1,join(X0,X3)))))),
inference(forward_demodulation,[],[f3252,f395]) ).
fof(f3347,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f3303,f561]) ).
fof(f3445,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,join(X3,X0))))) = join(meet(X1,join(X2,meet(X1,X0))),meet(X1,join(X0,meet(X1,X2)))),
inference(superposition,[],[f206,f185]) ).
fof(f3449,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,meet(X2,join(X1,X3)))) = join(meet(X1,join(X0,meet(X1,X2))),meet(X1,join(meet(X2,X3),meet(X0,X1)))),
inference(superposition,[],[f206,f5]) ).
fof(f3503,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X2,X3),meet(X0,X1))) = meet(meet(X0,join(meet(X2,X3),meet(X0,X1))),meet(X0,join(X1,meet(X2,join(X0,X3))))),
inference(superposition,[],[f185,f206]) ).
fof(f3509,plain,
! [X2,X3,X0,X1,X4,X5] : meet(join(X4,meet(X5,join(meet(X0,join(X1,meet(X0,X2))),X4))),join(X4,meet(join(X4,X5),meet(X0,join(X1,meet(X2,join(X0,X3))))))) = join(X4,meet(X5,join(meet(X0,join(X1,meet(X0,X2))),meet(X4,meet(X0,join(meet(X2,X3),meet(X0,X1))))))),
inference(superposition,[],[f201,f206]) ).
fof(f3528,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X2,X3),meet(X0,X1))) = meet(join(X1,meet(X2,join(X0,X3))),meet(meet(X0,join(meet(X2,X3),meet(X0,X1))),X0)),
inference(forward_demodulation,[],[f3503,f225]) ).
fof(f3579,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X1,join(X2,meet(X1,X0))),meet(X1,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f3445,f354]) ).
fof(f3623,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X2,X3),meet(X0,X1))) = meet(X0,meet(join(X1,meet(X2,join(X0,X3))),meet(X0,join(meet(X2,X3),meet(X0,X1))))),
inference(forward_demodulation,[],[f3528,f225]) ).
fof(f3687,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X2,X3),meet(X0,X1))) = meet(X0,meet(X0,meet(join(meet(X2,X3),meet(X0,X1)),join(X1,meet(X2,join(X0,X3)))))),
inference(forward_demodulation,[],[f3623,f225]) ).
fof(f3739,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X2,X3),meet(X0,X1))) = meet(X0,meet(join(meet(X2,X3),meet(X0,X1)),join(X1,meet(X2,join(X0,X3))))),
inference(forward_demodulation,[],[f3687,f381]) ).
fof(f3884,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(meet(X0,X1),join(X0,X3)))) = join(meet(X0,join(X2,meet(X0,X1))),meet(X0,join(meet(X2,X0),meet(meet(X0,X1),X3)))),
inference(superposition,[],[f180,f381]) ).
fof(f4090,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(meet(X0,X1),join(X0,X3)))) = join(meet(X0,join(X2,meet(X0,X1))),meet(X0,join(meet(X2,X0),meet(X0,meet(X1,X3))))),
inference(forward_demodulation,[],[f3884,f7]) ).
fof(f4155,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(X0,meet(X1,join(X0,X3))))) = join(meet(X0,join(X2,meet(X0,X1))),meet(X0,join(meet(X2,X0),meet(X0,meet(X1,X3))))),
inference(forward_demodulation,[],[f4090,f7]) ).
fof(f4209,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,join(X2,meet(X0,X1))),meet(X0,join(meet(X2,X0),meet(X0,meet(X1,X3))))),
inference(forward_demodulation,[],[f4155,f651]) ).
fof(f4818,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(join(X1,X2),X0),meet(join(X0,meet(X1,X2)),join(X2,X3)))) = join(meet(X2,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1)))),meet(X2,join(meet(X2,meet(join(X1,X2),X0)),meet(X3,join(X0,meet(X1,X2)))))),
inference(superposition,[],[f182,f177]) ).
fof(f4820,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),meet(join(X0,meet(X1,X2)),join(X2,X3)))) = join(meet(X2,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1)))),meet(X2,join(meet(X2,meet(X0,join(X1,X2))),meet(X3,join(X0,meet(X1,X2)))))),
inference(superposition,[],[f182,f16]) ).
fof(f4995,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),meet(join(X0,meet(X1,X2)),join(X2,X3)))) = join(meet(X2,join(X0,meet(X1,X2))),meet(X2,join(meet(X2,meet(X0,join(X1,X2))),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f4820,f651]) ).
fof(f4997,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(join(X1,X2),X0),meet(join(X0,meet(X1,X2)),join(X2,X3)))) = join(meet(X2,meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1)))),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f4818,f360]) ).
fof(f5079,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(join(X1,X2),X0),meet(join(X0,meet(X1,X2)),join(X2,X3)))) = join(meet(X2,join(X0,meet(X1,X2))),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f4997,f651]) ).
fof(f5515,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(join(meet(X0,X1),X2),meet(X0,join(X2,meet(X1,join(X0,X3)))))),
inference(superposition,[],[f25,f6]) ).
fof(f5534,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X2,meet(X1,X3)),meet(X1,join(X2,meet(X3,join(X0,X1)))))),
inference(superposition,[],[f25,f369]) ).
fof(f5543,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,meet(join(X2,meet(X1,X0)),meet(X1,join(X2,X0)))),
inference(superposition,[],[f25,f185]) ).
fof(f5554,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),meet(X2,X0))) = meet(X2,meet(join(meet(X0,join(X1,X2)),meet(X2,X0)),meet(X2,meet(X0,join(X1,X2))))),
inference(superposition,[],[f25,f239]) ).
fof(f5655,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),meet(X2,X0))) = meet(X2,meet(meet(X2,meet(X0,join(X1,X2))),join(meet(X0,join(X1,X2)),meet(X2,X0)))),
inference(forward_demodulation,[],[f5554,f5]) ).
fof(f5666,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,meet(meet(X1,join(X2,X0)),join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f5543,f5]) ).
fof(f5673,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(X1,meet(join(X2,meet(X3,join(X0,X1))),join(X2,meet(X1,X3))))),
inference(forward_demodulation,[],[f5534,f225]) ).
fof(f5691,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(X0,meet(join(X2,meet(X1,join(X0,X3))),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f5515,f225]) ).
fof(f5770,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),meet(X2,X0))) = meet(X2,meet(X2,meet(meet(X0,join(X1,X2)),join(meet(X0,join(X1,X2)),meet(X2,X0))))),
inference(forward_demodulation,[],[f5655,f7]) ).
fof(f5781,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,meet(X1,meet(join(X2,X0),join(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f5666,f7]) ).
fof(f5788,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X2,meet(X3,join(X0,X1))),join(X2,meet(X1,X3)))),
inference(forward_demodulation,[],[f5673,f381]) ).
fof(f5806,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(join(X2,meet(X1,join(X0,X3))),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f5691,f381]) ).
fof(f5873,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),meet(X2,X0))) = meet(X2,meet(meet(X0,join(X1,X2)),join(meet(X0,join(X1,X2)),meet(X2,X0)))),
inference(forward_demodulation,[],[f5770,f381]) ).
fof(f5884,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,meet(join(X2,X0),join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f5781,f381]) ).
fof(f5891,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X2,meet(X1,X3)),join(X2,meet(X3,join(X0,X1))))),
inference(forward_demodulation,[],[f5788,f5]) ).
fof(f5906,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(join(meet(X0,X1),X2),join(X2,meet(X1,join(X0,X3))))),
inference(forward_demodulation,[],[f5806,f5]) ).
fof(f5966,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,X2))) = meet(X2,join(meet(X0,join(X1,X2)),meet(X2,X0))),
inference(forward_demodulation,[],[f5873,f3]) ).
fof(f6039,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,X2))) = meet(X2,join(meet(X2,X0),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f5966,f6]) ).
fof(f6091,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f6039,f2336]) ).
fof(f6138,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),meet(join(X0,meet(X1,X2)),join(X2,X3)))) = join(meet(X2,join(X0,meet(X1,X2))),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(backward_demodulation,[],[f4995,f6091]) ).
fof(f6260,plain,
! [X2,X3,X0,X1] : meet(meet(X0,join(X2,meet(X0,X1))),X3) = meet(meet(X0,join(X2,meet(X0,X1))),meet(X3,meet(X0,join(X1,X2)))),
inference(superposition,[],[f6091,f239]) ).
fof(f6263,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(meet(X1,X0),meet(X2,X0)),
inference(superposition,[],[f6091,f179]) ).
fof(f6286,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),X3) = meet(X0,meet(meet(X1,join(X2,X0)),X3)),
inference(superposition,[],[f7,f6091]) ).
fof(f6318,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X0,X1),X2)) = meet(X0,meet(X2,join(X3,join(X0,X1)))),
inference(superposition,[],[f209,f6091]) ).
fof(f6319,plain,
! [X2,X3,X0,X1] : meet(X0,X2) = meet(X0,meet(X2,join(X3,join(X0,X1)))),
inference(forward_demodulation,[],[f6318,f209]) ).
fof(f6343,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),X3) = meet(X0,meet(X1,meet(join(X2,X0),X3))),
inference(forward_demodulation,[],[f6286,f7]) ).
fof(f6361,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X0,meet(meet(X1,X0),X2)),
inference(forward_demodulation,[],[f6263,f225]) ).
fof(f6364,plain,
! [X2,X3,X0,X1] : meet(meet(X0,join(X2,meet(X0,X1))),X3) = meet(meet(X0,join(X1,X2)),meet(meet(X0,join(X2,meet(X0,X1))),X3)),
inference(forward_demodulation,[],[f6260,f225]) ).
fof(f6370,plain,
! [X2,X0,X1] : meet(join(X1,meet(join(X0,X1),X2)),join(X1,meet(X0,join(X1,meet(join(X0,X1),X2))))) = join(X1,meet(X0,join(meet(join(X0,X1),X2),meet(X1,X2)))),
inference(backward_demodulation,[],[f2428,f6319]) ).
fof(f6384,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,X3)) = meet(X0,meet(X1,meet(join(X2,X0),X3))),
inference(forward_demodulation,[],[f6343,f7]) ).
fof(f6395,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f6361,f7]) ).
fof(f6398,plain,
! [X2,X3,X0,X1] : meet(meet(X0,join(X2,meet(X0,X1))),X3) = meet(X0,meet(join(X1,X2),meet(meet(X0,join(X2,meet(X0,X1))),X3))),
inference(forward_demodulation,[],[f6364,f7]) ).
fof(f6405,plain,
! [X2,X0,X1] : meet(join(X1,meet(join(X0,X1),X2)),join(X1,meet(X0,join(X1,meet(join(X0,X1),X2))))) = join(X1,meet(X0,join(meet(X1,X2),meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f6370,f6]) ).
fof(f6423,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X2,meet(X0,X1)),X3)) = meet(X0,meet(join(X1,X2),meet(X0,meet(join(X2,meet(X0,X1)),X3)))),
inference(forward_demodulation,[],[f6398,f7]) ).
fof(f6436,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X2,meet(X0,X1)),X3)) = meet(join(X1,X2),meet(X0,meet(join(X2,meet(X0,X1)),X3))),
inference(forward_demodulation,[],[f6423,f6395]) ).
fof(f6444,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),meet(X0,X3)) = meet(X0,meet(join(X2,meet(X0,X1)),X3)),
inference(forward_demodulation,[],[f6436,f1236]) ).
fof(f6513,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X1,X3))) = meet(join(X3,X2),meet(X1,join(X2,meet(X3,join(X0,X1))))),
inference(backward_demodulation,[],[f5891,f6444]) ).
fof(f6541,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X2,X3),meet(X0,X1))) = meet(join(X1,meet(X2,X3)),meet(X0,join(X1,meet(X2,join(X0,X3))))),
inference(backward_demodulation,[],[f3739,f6444]) ).
fof(f6654,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X0,X1),meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f1044]) ).
fof(f7055,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X0,meet(X1,X2)))) = join(X1,join(meet(X0,join(X0,meet(X1,X2))),meet(join(X1,X0),meet(join(X0,X2),join(X1,X0))))),
inference(superposition,[],[f634,f185]) ).
fof(f7154,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X0,meet(X1,X2)))) = join(X1,join(meet(X0,join(X0,meet(X1,X2))),meet(join(X0,X2),join(X1,X0)))),
inference(forward_demodulation,[],[f7055,f379]) ).
fof(f7265,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X0,meet(X1,X2)))) = join(X1,meet(join(X0,X2),join(X1,X0))),
inference(forward_demodulation,[],[f7154,f2684]) ).
fof(f7345,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,meet(join(X0,X2),join(X1,X0))),
inference(forward_demodulation,[],[f7265,f3]) ).
fof(f7573,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),join(X1,X2))),
inference(superposition,[],[f7345,f5]) ).
fof(f7596,plain,
! [X2,X0,X1] : meet(join(X1,X2),join(X0,meet(join(X0,X1),join(X1,X2)))) = join(meet(join(X1,X2),X0),meet(join(X1,X2),join(X0,X1))),
inference(superposition,[],[f395,f7345]) ).
fof(f7671,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,join(X2,meet(X0,X1)))) = meet(join(X1,X2),join(X0,meet(join(X0,X1),join(X1,X2)))),
inference(forward_demodulation,[],[f7596,f1255]) ).
fof(f7737,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,join(X2,meet(X0,X1)))) = meet(join(X1,X2),join(X0,X1)),
inference(forward_demodulation,[],[f7671,f7573]) ).
fof(f7774,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X1,X0)) = join(meet(X1,join(X0,X2)),meet(join(X0,X2),join(X1,X0))),
inference(backward_demodulation,[],[f288,f7737]) ).
fof(f7901,plain,
! [X2,X3,X0,X1,X4] : join(X3,meet(X4,join(meet(X2,join(X0,X1)),meet(X3,meet(join(X0,X1),join(X2,X0)))))) = meet(join(X3,meet(X4,join(meet(X2,join(X0,X1)),X3))),join(X3,meet(join(X3,X4),meet(join(X0,X1),join(X2,X0))))),
inference(superposition,[],[f201,f7774]) ).
fof(f8203,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X2,X1))) = join(meet(join(X1,meet(X0,X1)),X2),meet(meet(X0,X1),join(X2,meet(X0,X1)))),
inference(superposition,[],[f177,f379]) ).
fof(f8243,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X2,X1))) = join(meet(join(X1,meet(X0,X1)),X2),meet(X0,X1)),
inference(forward_demodulation,[],[f8203,f185]) ).
fof(f8270,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X2,X1))) = join(meet(X0,X1),meet(join(X1,meet(X0,X1)),X2)),
inference(forward_demodulation,[],[f8243,f6]) ).
fof(f8284,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(join(X2,meet(X0,X1)),join(meet(X0,X1),meet(X2,X1))),
inference(forward_demodulation,[],[f8270,f179]) ).
fof(f8346,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,X1)),join(X1,meet(X2,meet(X0,X1)))) = join(meet(X2,join(meet(X0,X1),X1)),meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f183,f379]) ).
fof(f8347,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,meet(X1,join(X0,X2)))) = join(meet(X1,join(join(X0,X2),X0)),meet(X0,join(X1,X0))),
inference(superposition,[],[f183,f3]) ).
fof(f8408,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(meet(X1,join(X0,meet(X1,X2))),meet(join(X0,meet(X1,X2)),join(X1,meet(X0,X2)))),
inference(superposition,[],[f185,f183]) ).
fof(f8451,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(join(X1,meet(X0,X2)),meet(meet(X1,join(X0,meet(X1,X2))),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f8408,f225]) ).
fof(f8509,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,meet(X1,join(X0,X2)))) = join(meet(X0,join(X1,X0)),meet(X1,join(join(X0,X2),X0))),
inference(forward_demodulation,[],[f8347,f6]) ).
fof(f8510,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,X1)),join(X1,meet(X2,meet(X0,X1)))) = join(meet(X2,join(X1,meet(X0,X1))),meet(X1,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f8346,f6]) ).
fof(f8560,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(join(X1,meet(X0,X2)),meet(join(X0,meet(X1,X2)),meet(X1,join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f8451,f5]) ).
fof(f8610,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,meet(X1,join(X0,X2)))) = join(meet(X0,join(X1,X0)),meet(X1,join(X0,join(X0,X2)))),
inference(forward_demodulation,[],[f8509,f6]) ).
fof(f8611,plain,
! [X2,X0,X1] : meet(join(X2,meet(X0,X1)),join(X1,meet(X2,meet(X0,X1)))) = join(meet(X2,X1),meet(X1,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f8510,f179]) ).
fof(f8656,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(join(X1,meet(X0,X2)),meet(X1,meet(join(X0,meet(X1,X2)),join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f8560,f225]) ).
fof(f8704,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,meet(X1,join(X0,X2)))) = join(meet(X0,join(X1,X0)),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f8610,f277]) ).
fof(f8705,plain,
! [X2,X0,X1] : join(meet(X2,X1),meet(X1,join(X2,meet(X0,X1)))) = meet(join(X2,meet(X0,X1)),X1),
inference(forward_demodulation,[],[f8611,f257]) ).
fof(f8743,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,meet(meet(join(X0,meet(X1,X2)),join(X0,meet(X1,X2))),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f8656,f225]) ).
fof(f8785,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X0,X2))) = meet(join(X1,X0),join(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f8704,f185]) ).
fof(f8786,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = join(meet(X2,X1),meet(X1,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f8705,f5]) ).
fof(f8818,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,meet(join(X0,meet(X1,X2)),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f8743,f651]) ).
fof(f8883,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(join(X2,X0),meet(X1,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f8818,f6444]) ).
fof(f8939,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(join(X2,X0),X1),
inference(forward_demodulation,[],[f8883,f1163]) ).
fof(f8997,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X0,join(X2,X1)))) = meet(X2,join(X3,meet(join(X1,X2),X0))),
inference(backward_demodulation,[],[f478,f8939]) ).
fof(f9040,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(X0,join(X2,meet(X1,X0))),
inference(backward_demodulation,[],[f3347,f8939]) ).
fof(f9044,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,meet(X2,join(X1,X3)))) = join(meet(join(X2,X0),X1),meet(X1,join(meet(X2,X3),meet(X0,X1)))),
inference(backward_demodulation,[],[f3449,f8939]) ).
fof(f9048,plain,
! [X2,X3,X0,X1,X4,X5] : meet(join(X4,meet(X5,join(meet(join(X2,X1),X0),X4))),join(X4,meet(join(X4,X5),meet(X0,join(X1,meet(X2,join(X0,X3))))))) = join(X4,meet(X5,join(meet(join(X2,X1),X0),meet(X4,meet(X0,join(meet(X2,X3),meet(X0,X1))))))),
inference(backward_demodulation,[],[f3509,f8939]) ).
fof(f9052,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(join(X0,X2),X1),meet(X1,join(X0,meet(X1,X2)))),
inference(backward_demodulation,[],[f3579,f8939]) ).
fof(f9073,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),X0) = join(meet(join(X1,X2),X0),meet(X0,join(meet(X2,X0),meet(X0,meet(X1,X3))))),
inference(backward_demodulation,[],[f4209,f8939]) ).
fof(f9107,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = meet(X1,meet(join(X2,X0),join(X2,meet(X1,X0)))),
inference(backward_demodulation,[],[f5884,f8939]) ).
fof(f9152,plain,
! [X2,X3,X0,X1] : meet(join(X3,X2),meet(X1,join(X2,meet(X3,join(X0,X1))))) = meet(join(X3,X2),X1),
inference(backward_demodulation,[],[f6513,f8939]) ).
fof(f9295,plain,
! [X2,X3,X0,X1] : meet(join(X1,meet(X2,X3)),meet(X0,join(X1,meet(X2,join(X0,X3))))) = meet(join(X1,meet(X2,X3)),X0),
inference(backward_demodulation,[],[f6541,f8939]) ).
fof(f9467,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),X0) = join(meet(join(X1,X2),X0),meet(join(meet(X1,X3),meet(X2,X0)),X0)),
inference(forward_demodulation,[],[f9073,f8939]) ).
fof(f9474,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(join(X0,X2),X1),meet(join(X2,X0),X1)),
inference(forward_demodulation,[],[f9052,f8939]) ).
fof(f9478,plain,
! [X2,X3,X0,X1,X4,X5] : meet(join(X4,meet(X5,join(meet(join(X2,X1),X0),X4))),join(X4,meet(join(X4,X5),meet(X0,join(X1,meet(X2,join(X0,X3))))))) = join(X4,meet(X5,join(meet(join(X2,X1),X0),meet(X4,meet(join(X1,meet(X2,X3)),X0))))),
inference(forward_demodulation,[],[f9048,f8939]) ).
fof(f9558,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(join(X1,X2),X0),meet(join(X0,meet(X1,X2)),join(X2,X3)))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(backward_demodulation,[],[f5079,f9040]) ).
fof(f9569,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),meet(join(X0,meet(X1,X2)),join(X2,X3)))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(backward_demodulation,[],[f6138,f9040]) ).
fof(f9589,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X2,X1),meet(join(X0,X2),X1)),
inference(backward_demodulation,[],[f8786,f9040]) ).
fof(f9610,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,meet(X2,join(X1,X3)))) = join(meet(join(X2,X0),X1),meet(join(X0,meet(X2,X3)),X1)),
inference(backward_demodulation,[],[f9044,f9040]) ).
fof(f9618,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,meet(join(X0,X1),X2))) = join(X1,meet(X0,join(meet(X1,X2),meet(join(X0,X1),X2)))),
inference(backward_demodulation,[],[f6405,f9040]) ).
fof(f9619,plain,
! [X2,X0,X1] : join(X1,meet(X2,join(X0,X1))) = meet(join(X2,X1),join(X0,X1)),
inference(backward_demodulation,[],[f892,f9040]) ).
fof(f9704,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),X0) = join(meet(join(X1,X2),X0),meet(X0,join(meet(X1,X3),meet(X2,X0)))),
inference(forward_demodulation,[],[f9467,f5]) ).
fof(f9726,plain,
! [X2,X3,X0,X1,X4] : join(X0,meet(join(meet(X0,X2),X1),join(X3,meet(X0,X4)))) = meet(meet(join(join(meet(X0,X2),X1),X0),join(X3,X0)),join(X0,meet(join(X0,X1),join(X3,X4)))),
inference(backward_demodulation,[],[f1691,f9619]) ).
fof(f9738,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X1)) = meet(join(X0,X1),join(X1,meet(X0,join(X1,X2)))),
inference(backward_demodulation,[],[f1570,f9619]) ).
fof(f9741,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(meet(join(X3,X2),join(X0,X2)),join(X2,meet(join(X0,X1),join(X2,X3)))),
inference(backward_demodulation,[],[f1713,f9619]) ).
fof(f9746,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(meet(join(X2,X1),join(X0,X1)),join(X1,meet(join(X1,X2),X0))),
inference(backward_demodulation,[],[f1773,f9619]) ).
fof(f9748,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X2,X0)) = meet(join(X0,X1),meet(join(X1,X0),join(X2,X0))),
inference(backward_demodulation,[],[f1878,f9619]) ).
fof(f9761,plain,
! [X2,X3,X0,X1] : meet(join(X2,X1),join(X0,X1)) = meet(meet(join(X2,X1),join(X0,X1)),join(X1,meet(join(X1,X2),join(X3,join(X0,X1))))),
inference(backward_demodulation,[],[f2199,f9619]) ).
fof(f9799,plain,
! [X2,X3,X0,X1,X4] : join(X3,meet(X4,join(meet(X2,join(X0,X1)),meet(X3,meet(join(X0,X1),join(X2,X0)))))) = meet(meet(join(X4,X3),join(meet(X2,join(X0,X1)),X3)),join(X3,meet(join(X3,X4),meet(join(X0,X1),join(X2,X0))))),
inference(backward_demodulation,[],[f7901,f9619]) ).
fof(f9800,plain,
! [X2,X3,X0,X1,X4,X5] : join(X4,meet(X5,join(meet(join(X2,X1),X0),meet(X4,meet(join(X1,meet(X2,X3)),X0))))) = meet(meet(join(X5,X4),join(meet(join(X2,X1),X0),X4)),join(X4,meet(join(X4,X5),meet(X0,join(X1,meet(X2,join(X0,X3))))))),
inference(backward_demodulation,[],[f9478,f9619]) ).
fof(f9803,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,X1)) = join(X1,meet(X0,join(meet(X1,X2),meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f9618,f8939]) ).
fof(f9886,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),X0) = join(meet(join(X1,X2),X0),meet(join(X2,meet(X1,X3)),X0)),
inference(forward_demodulation,[],[f9704,f9040]) ).
fof(f9893,plain,
! [X2,X3,X0,X1,X4,X5] : join(X4,meet(X5,join(meet(join(X2,X1),X0),meet(X4,meet(join(X1,meet(X2,X3)),X0))))) = meet(join(X5,X4),meet(join(meet(join(X2,X1),X0),X4),join(X4,meet(join(X4,X5),meet(X0,join(X1,meet(X2,join(X0,X3)))))))),
inference(forward_demodulation,[],[f9800,f7]) ).
fof(f9894,plain,
! [X2,X3,X0,X1,X4] : join(X3,meet(X4,join(meet(X2,join(X0,X1)),meet(X3,meet(join(X0,X1),join(X2,X0)))))) = meet(join(X4,X3),meet(join(meet(X2,join(X0,X1)),X3),join(X3,meet(join(X3,X4),meet(join(X0,X1),join(X2,X0)))))),
inference(forward_demodulation,[],[f9799,f7]) ).
fof(f9919,plain,
! [X2,X3,X0,X1] : meet(join(X2,X1),join(X0,X1)) = meet(join(X2,X1),meet(join(X0,X1),join(X1,meet(join(X1,X2),join(X3,join(X0,X1)))))),
inference(forward_demodulation,[],[f9761,f7]) ).
fof(f9926,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = meet(join(X1,X0),join(X2,X0)),
inference(forward_demodulation,[],[f9748,f6654]) ).
fof(f9928,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X2,X1),meet(join(X0,X1),join(X1,meet(join(X1,X2),X0)))),
inference(forward_demodulation,[],[f9746,f7]) ).
fof(f9933,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(join(X3,X2),meet(join(X0,X2),join(X2,meet(join(X0,X1),join(X2,X3))))),
inference(forward_demodulation,[],[f9741,f7]) ).
fof(f9936,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X0,X2))) = meet(join(X1,X0),join(X2,X0)),
inference(backward_demodulation,[],[f8785,f9738]) ).
fof(f9943,plain,
! [X2,X3,X0,X1,X4] : join(X0,meet(join(meet(X0,X2),X1),join(X3,meet(X0,X4)))) = meet(join(join(meet(X0,X2),X1),X0),meet(join(X3,X0),join(X0,meet(join(X0,X1),join(X3,X4))))),
inference(forward_demodulation,[],[f9726,f7]) ).
fof(f9948,plain,
! [X2,X0,X1] : meet(join(X2,X1),join(X0,X1)) = join(X1,meet(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f9803,f9589]) ).
fof(f9985,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,meet(X2,join(X1,X3)))) = meet(join(X2,X0),X1),
inference(backward_demodulation,[],[f9610,f9886]) ).
fof(f10079,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(join(X3,X2),meet(join(X0,X2),meet(join(join(X0,X1),X2),join(X3,X2)))),
inference(backward_demodulation,[],[f9933,f9936]) ).
fof(f10087,plain,
! [X2,X0,X1] : join(X1,X2) = join(X1,meet(join(join(X0,meet(X1,X2)),X2),join(meet(X0,X1),X2))),
inference(backward_demodulation,[],[f1206,f9936]) ).
fof(f10287,plain,
! [X2,X3,X0,X1,X4] : join(X0,meet(join(meet(X0,X2),X1),join(X3,meet(X0,X4)))) = meet(join(X0,join(meet(X0,X2),X1)),meet(join(X3,X0),join(X0,meet(join(X0,X1),join(X3,X4))))),
inference(forward_demodulation,[],[f9943,f6]) ).
fof(f10292,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X2,X1),join(X0,X1)),
inference(forward_demodulation,[],[f9948,f209]) ).
fof(f10334,plain,
! [X2,X3,X0,X1] : meet(join(X0,X3),X2) = meet(X2,join(X3,meet(join(X1,X2),X0))),
inference(backward_demodulation,[],[f8997,f9985]) ).
fof(f10386,plain,
! [X2,X3,X0,X1] : meet(join(X1,meet(X2,X3)),X0) = meet(join(X1,meet(X2,X3)),meet(join(X2,X1),X0)),
inference(backward_demodulation,[],[f9295,f9985]) ).
fof(f10401,plain,
! [X2,X3,X0,X1,X4,X5] : join(X4,meet(X5,join(meet(join(X2,X1),X0),meet(X4,meet(join(X1,meet(X2,X3)),X0))))) = meet(join(X5,X4),meet(join(meet(join(X2,X1),X0),X4),join(X4,meet(join(X4,X5),meet(join(X2,X1),X0))))),
inference(backward_demodulation,[],[f9893,f9985]) ).
fof(f10437,plain,
! [X2,X3,X0,X1] : join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))) = meet(join(join(X0,meet(X1,X2)),meet(X0,join(X1,X2))),X2),
inference(backward_demodulation,[],[f9569,f9985]) ).
fof(f10446,plain,
! [X2,X3,X0,X1] : join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))) = meet(join(join(X0,meet(X1,X2)),meet(join(X1,X2),X0)),X2),
inference(backward_demodulation,[],[f9558,f9985]) ).
fof(f10649,plain,
! [X2,X0,X1] : join(X1,X2) = join(X1,meet(join(meet(X0,X1),X2),join(join(X0,meet(X1,X2)),X2))),
inference(forward_demodulation,[],[f10087,f5]) ).
fof(f10657,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(join(X3,X2),meet(join(X0,X2),join(join(X0,X1),X2))),
inference(forward_demodulation,[],[f10079,f488]) ).
fof(f10696,plain,
! [X2,X3,X0,X1,X4] : join(X0,meet(join(meet(X0,X2),X1),join(X3,meet(X0,X4)))) = meet(join(X0,X1),meet(join(X3,X0),join(X0,meet(join(X0,X1),join(X3,X4))))),
inference(forward_demodulation,[],[f10287,f302]) ).
fof(f10726,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X2,X1),meet(join(X0,X1),join(X1,meet(join(X1,X2),join(X3,join(X0,X1)))))),
inference(backward_demodulation,[],[f9919,f10292]) ).
fof(f10728,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = meet(join(X0,X1),join(X2,X0)),
inference(backward_demodulation,[],[f9926,f10292]) ).
fof(f10782,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,meet(X1,X2)),meet(join(X1,X2),X0))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f10446,f5]) ).
fof(f10791,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,meet(X1,X2)),meet(X0,join(X1,X2)))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f10437,f5]) ).
fof(f10828,plain,
! [X2,X3,X0,X1,X4,X5] : join(X4,meet(X5,join(meet(join(X2,X1),X0),meet(X4,meet(join(X1,meet(X2,X3)),X0))))) = join(X4,meet(X5,meet(join(X2,X1),X0))),
inference(forward_demodulation,[],[f10401,f9928]) ).
fof(f10834,plain,
! [X2,X3,X0,X1] : meet(join(X1,meet(X2,X3)),X0) = meet(join(X2,X1),meet(X0,join(X1,meet(X2,X3)))),
inference(forward_demodulation,[],[f10386,f225]) ).
fof(f10994,plain,
! [X2,X0,X1] : join(X1,X2) = join(X1,join(X2,meet(join(X0,meet(X1,X2)),meet(X0,X1)))),
inference(forward_demodulation,[],[f10649,f10292]) ).
fof(f11002,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(join(X3,X2),join(X2,meet(join(X0,X1),X0))),
inference(forward_demodulation,[],[f10657,f10292]) ).
fof(f11069,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X1,join(X2,meet(X0,X1)))),
inference(backward_demodulation,[],[f7737,f10728]) ).
fof(f11094,plain,
! [X2,X3,X0,X1,X4] : join(X3,meet(X4,join(meet(X2,join(X0,X1)),meet(X3,join(X0,meet(X2,X1)))))) = meet(join(X4,X3),meet(join(meet(X2,join(X0,X1)),X3),join(X3,meet(join(X3,X4),join(X0,meet(X2,X1)))))),
inference(backward_demodulation,[],[f9894,f10728]) ).
fof(f11126,plain,
! [X2,X3,X0,X1] : join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))) = meet(join(X0,join(X0,meet(X1,X2))),X2),
inference(forward_demodulation,[],[f10782,f10334]) ).
fof(f11128,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X0,join(X1,X2)),join(X0,meet(X1,X2)))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f10791,f6]) ).
fof(f11165,plain,
! [X2,X3,X0,X1] : meet(join(X3,X2),X1) = meet(join(X2,meet(X3,join(X0,X1))),X1),
inference(backward_demodulation,[],[f9152,f10834]) ).
fof(f11265,plain,
! [X2,X0,X1] : join(X1,X2) = join(X1,join(X2,meet(meet(X0,X1),join(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f10994,f5]) ).
fof(f11273,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(join(X3,X2),join(X2,meet(X0,join(X0,X1)))),
inference(forward_demodulation,[],[f11002,f5]) ).
fof(f11363,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,join(X0,meet(X1,X2)))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f11126,f5]) ).
fof(f11365,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X1,X2),join(meet(X0,join(X1,X2)),X0))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f11128,f314]) ).
fof(f11379,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X3,join(X0,X1)))) = meet(join(X3,X2),X1),
inference(forward_demodulation,[],[f11165,f5]) ).
fof(f11440,plain,
! [X2,X0,X1] : join(X1,X2) = join(X1,join(X2,meet(X0,meet(X1,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f11265,f7]) ).
fof(f11446,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X0,meet(X2,X1)))) = meet(join(X3,X2),join(X2,X0)),
inference(forward_demodulation,[],[f11273,f3]) ).
fof(f11492,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,meet(X1,X2))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f11363,f277]) ).
fof(f11494,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X1,X2),join(X0,meet(X0,join(X1,X2))))) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f11365,f6]) ).
fof(f11525,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X2,X1),meet(join(join(X1,X2),X1),join(X0,X1))),
inference(backward_demodulation,[],[f10726,f11379]) ).
fof(f11584,plain,
! [X2,X0,X1] : join(X1,X2) = join(X1,join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f11440,f651]) ).
fof(f11600,plain,
! [X2,X3,X0,X1,X4] : meet(join(X0,X1),meet(join(X3,X0),join(X0,meet(join(X0,X1),join(X3,X4))))) = meet(join(join(meet(X0,X2),X1),X0),join(X0,X3)),
inference(backward_demodulation,[],[f10696,f11446]) ).
fof(f11605,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,meet(X0,X1))) = meet(join(X3,X2),join(X2,meet(X0,X1))),
inference(backward_demodulation,[],[f2983,f11446]) ).
fof(f11623,plain,
! [X2,X0,X1,X4,X5] : join(X4,meet(X5,meet(join(X2,X1),X0))) = meet(join(X5,X4),join(X4,meet(join(X2,X1),X0))),
inference(backward_demodulation,[],[f10828,f11446]) ).
fof(f11646,plain,
! [X2,X3,X0,X1,X4] : meet(join(X4,X3),meet(join(meet(X2,join(X0,X1)),X3),join(X3,meet(join(X3,X4),join(X0,meet(X2,X1)))))) = meet(join(X4,X3),join(X3,meet(X2,join(X0,X1)))),
inference(backward_demodulation,[],[f11094,f11446]) ).
fof(f11816,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),X2) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f11492,f9040]) ).
fof(f11818,plain,
! [X2,X3,X0,X1] : meet(X2,join(meet(X1,X2),X0)) = join(meet(join(X1,X0),X2),meet(X2,join(meet(X2,X0),meet(X3,join(X0,meet(X1,X2)))))),
inference(forward_demodulation,[],[f11494,f4]) ).
fof(f11839,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X2,X1),join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f11525,f10292]) ).
fof(f11872,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X1,X2)),
inference(backward_demodulation,[],[f11069,f11584]) ).
fof(f11950,plain,
! [X2,X3,X0,X1,X4] : meet(join(X4,X3),join(X3,meet(X2,join(X0,X1)))) = meet(join(X4,X3),join(X3,meet(meet(X2,join(X0,X1)),meet(join(X3,X4),join(X0,meet(X2,X1)))))),
inference(backward_demodulation,[],[f11646,f11623]) ).
fof(f11967,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = join(meet(X0,X1),meet(X2,meet(X2,X1))),
inference(backward_demodulation,[],[f8284,f11605]) ).
fof(f11991,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(meet(X0,X1),meet(X1,join(X0,X3))))),
inference(backward_demodulation,[],[f5906,f11605]) ).
fof(f11999,plain,
! [X2,X3,X0,X1,X4] : meet(join(X0,X1),meet(join(X3,X0),join(X0,meet(join(X0,X1),join(X3,X4))))) = meet(join(X0,join(meet(X0,X2),X1)),join(X0,X3)),
inference(forward_demodulation,[],[f11600,f6]) ).
fof(f12124,plain,
! [X2,X0,X1] : meet(X2,join(meet(X1,X2),X0)) = meet(join(X1,X0),X2),
inference(forward_demodulation,[],[f11818,f11816]) ).
fof(f12138,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,meet(X2,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f11839,f11605]) ).
fof(f12298,plain,
! [X2,X3,X0,X1,X4] : meet(join(X4,X3),join(X3,meet(X2,join(X0,X1)))) = join(X3,meet(X4,meet(meet(X2,join(X0,X1)),meet(join(X3,X4),join(X0,meet(X2,X1)))))),
inference(forward_demodulation,[],[f11950,f11872]) ).
fof(f12334,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(X1,meet(join(X0,X3),meet(X0,X1))))),
inference(forward_demodulation,[],[f11991,f225]) ).
fof(f12351,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X0,X1),meet(X1,X2)),
inference(forward_demodulation,[],[f11967,f381]) ).
fof(f12354,plain,
! [X3,X0,X1,X4] : meet(join(X0,X1),join(X0,X3)) = meet(join(X0,X1),meet(join(X3,X0),join(X0,meet(join(X0,X1),join(X3,X4))))),
inference(forward_demodulation,[],[f11999,f302]) ).
fof(f12479,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,meet(X2,X0)),
inference(forward_demodulation,[],[f12138,f6091]) ).
fof(f12583,plain,
! [X2,X3,X0,X1,X4] : meet(join(X4,X3),join(X3,meet(X2,join(X0,X1)))) = join(X3,meet(X4,meet(meet(X2,join(X0,X1)),join(X0,meet(X2,X1))))),
inference(forward_demodulation,[],[f12298,f6384]) ).
fof(f12619,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(X1,meet(join(X0,X3),X0)))),
inference(forward_demodulation,[],[f12334,f488]) ).
fof(f12630,plain,
! [X3,X0,X1,X4] : meet(join(X0,X1),join(X0,X3)) = meet(join(X0,X1),join(X0,meet(X3,meet(join(X0,X1),join(X3,X4))))),
inference(forward_demodulation,[],[f12354,f11872]) ).
fof(f12768,plain,
! [X2,X3,X0,X1,X4] : meet(join(X4,X3),join(X3,meet(X2,join(X0,X1)))) = join(X3,meet(X4,meet(X2,meet(join(X0,X1),join(X0,meet(X2,X1)))))),
inference(forward_demodulation,[],[f12583,f7]) ).
fof(f12804,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(X1,meet(X0,join(X0,X3))))),
inference(forward_demodulation,[],[f12619,f5]) ).
fof(f12810,plain,
! [X3,X0,X1] : meet(join(X0,X1),join(X0,X3)) = meet(join(X0,X1),join(X0,meet(X3,join(X0,X1)))),
inference(forward_demodulation,[],[f12630,f651]) ).
fof(f12908,plain,
! [X2,X3,X0,X1,X4] : join(X3,meet(X4,meet(join(X1,X0),X2))) = meet(join(X4,X3),join(X3,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f12768,f9107]) ).
fof(f12934,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f12804,f3]) ).
fof(f12939,plain,
! [X3,X0,X1] : meet(join(X0,X1),join(X0,X3)) = meet(join(X3,X0),join(X0,X1)),
inference(forward_demodulation,[],[f12810,f9040]) ).
fof(f13063,plain,
! [X2,X3,X0,X1,X4] : join(X3,meet(X4,meet(join(X1,X0),X2))) = join(X3,meet(X4,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f12908,f11872]) ).
fof(f13083,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(join(X1,X2),X0),
inference(forward_demodulation,[],[f12934,f9040]) ).
fof(f13087,plain,
! [X3,X0,X1] : join(X0,meet(X3,X1)) = meet(join(X0,X1),join(X0,X3)),
inference(forward_demodulation,[],[f12939,f11872]) ).
fof(f13304,plain,
~ sP0(meet(a,join(b,meet(d,c)))),
inference(backward_demodulation,[],[f13,f13087]) ).
fof(f13678,plain,
~ sP0(meet(a,join(b,meet(c,d)))),
inference(forward_demodulation,[],[f13304,f12479]) ).
fof(f14738,plain,
! [X2,X3,X0,X1] : join(X2,meet(join(X0,X1),X3)) = meet(join(X2,X3),join(X0,join(X1,X2))),
inference(superposition,[],[f10728,f8]) ).
fof(f14739,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(join(meet(X0,X1),X2),X0),
inference(superposition,[],[f10728,f4]) ).
fof(f14740,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(join(meet(X1,X0),X2),X0),
inference(superposition,[],[f10728,f179]) ).
fof(f14755,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,X2)),X3) = meet(join(X0,X2),meet(join(X1,X0),X3)),
inference(superposition,[],[f7,f10728]) ).
fof(f14806,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),X2)) = join(meet(X1,X0),meet(X0,X2)),
inference(forward_demodulation,[],[f14740,f5]) ).
fof(f14807,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f14739,f5]) ).
fof(f14850,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X1,X0),meet(X0,X2)),
inference(forward_demodulation,[],[f14806,f12124]) ).
fof(f14851,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f14807,f13083]) ).
fof(f14886,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = meet(join(X0,X2),X1),
inference(backward_demodulation,[],[f12351,f14850]) ).
fof(f14974,plain,
sP0(meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,join(b,meet(c,d))),meet(join(c,d),a)))))),
inference(backward_demodulation,[],[f17,f14851]) ).
fof(f15054,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(join(join(X0,X2),join(X2,X0)),X1),
inference(backward_demodulation,[],[f9474,f14886]) ).
fof(f15094,plain,
sP0(meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,join(b,meet(c,d))),meet(a,join(c,d))))))),
inference(forward_demodulation,[],[f14974,f12479]) ).
fof(f15209,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(join(X0,join(join(X0,X2),X2)),X1),
inference(forward_demodulation,[],[f15054,f314]) ).
fof(f15234,plain,
sP0(meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,join(c,d)),meet(a,join(b,meet(c,d)))))))),
inference(forward_demodulation,[],[f15094,f6]) ).
fof(f15321,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(join(X0,join(X2,join(X0,X2))),X1),
inference(forward_demodulation,[],[f15209,f6]) ).
fof(f15347,plain,
sP0(meet(a,meet(join(b,c),meet(join(b,d),meet(join(join(c,d),join(b,meet(c,d))),a))))),
inference(forward_demodulation,[],[f15234,f14851]) ).
fof(f15422,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(join(X2,join(X0,X2)),X1),
inference(forward_demodulation,[],[f15321,f441]) ).
fof(f15446,plain,
sP0(meet(a,meet(join(b,c),meet(a,meet(join(b,d),join(join(c,d),join(b,meet(c,d)))))))),
inference(forward_demodulation,[],[f15347,f225]) ).
fof(f15505,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(join(X0,X2),X1),
inference(forward_demodulation,[],[f15422,f369]) ).
fof(f15526,plain,
sP0(meet(join(b,c),meet(a,meet(join(b,d),join(join(c,d),join(b,meet(c,d))))))),
inference(forward_demodulation,[],[f15446,f6395]) ).
fof(f15595,plain,
sP0(meet(a,meet(meet(join(b,d),join(join(c,d),join(b,meet(c,d)))),join(b,c)))),
inference(forward_demodulation,[],[f15526,f225]) ).
fof(f15644,plain,
sP0(meet(a,meet(join(c,b),meet(join(b,d),join(join(c,d),join(b,meet(c,d))))))),
inference(forward_demodulation,[],[f15595,f15505]) ).
fof(f15680,plain,
sP0(meet(a,meet(join(b,d),meet(join(join(c,d),join(b,meet(c,d))),join(c,b))))),
inference(forward_demodulation,[],[f15644,f225]) ).
fof(f15694,plain,
sP0(meet(a,meet(join(b,d),meet(join(b,c),join(join(c,d),join(b,meet(c,d))))))),
inference(forward_demodulation,[],[f15680,f15505]) ).
fof(f15706,plain,
sP0(meet(a,meet(join(b,c),meet(join(join(c,d),join(b,meet(c,d))),join(b,d))))),
inference(forward_demodulation,[],[f15694,f225]) ).
fof(f15717,plain,
sP0(meet(a,meet(join(b,c),meet(join(d,b),join(join(c,d),join(b,meet(c,d))))))),
inference(forward_demodulation,[],[f15706,f15505]) ).
fof(f15726,plain,
sP0(meet(a,meet(join(b,meet(d,c)),join(join(c,d),join(b,meet(c,d)))))),
inference(forward_demodulation,[],[f15717,f14755]) ).
fof(f15737,plain,
sP0(meet(a,meet(join(b,meet(d,c)),join(meet(c,d),join(join(c,d),b))))),
inference(forward_demodulation,[],[f15726,f314]) ).
fof(f15740,plain,
sP0(meet(a,join(b,meet(join(meet(c,d),join(c,d)),meet(d,c))))),
inference(forward_demodulation,[],[f15737,f14738]) ).
fof(f15742,plain,
sP0(meet(a,join(b,meet(meet(d,c),join(meet(c,d),join(c,d)))))),
inference(forward_demodulation,[],[f15740,f12479]) ).
fof(f15743,plain,
sP0(meet(a,join(b,meet(d,meet(c,join(meet(c,d),join(c,d))))))),
inference(forward_demodulation,[],[f15742,f7]) ).
fof(f15744,plain,
sP0(meet(a,join(b,meet(c,meet(join(meet(c,d),join(c,d)),d))))),
inference(forward_demodulation,[],[f15743,f225]) ).
fof(f15745,plain,
sP0(meet(a,join(b,meet(c,meet(d,join(join(c,d),meet(c,d))))))),
inference(forward_demodulation,[],[f15744,f13063]) ).
fof(f15746,plain,
sP0(meet(a,join(b,meet(c,meet(join(c,join(c,d)),d))))),
inference(forward_demodulation,[],[f15745,f9040]) ).
fof(f15747,plain,
sP0(meet(a,join(b,meet(c,meet(d,join(join(c,d),c)))))),
inference(forward_demodulation,[],[f15746,f13063]) ).
fof(f15748,plain,
sP0(meet(a,join(b,meet(c,d)))),
inference(forward_demodulation,[],[f15747,f6091]) ).
fof(f15749,plain,
$false,
inference(forward_subsumption_resolution,[],[f15748,f13678]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT010-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.40 % Computer : n015.cluster.edu
% 0.11/0.40 % Model : x86_64 x86_64
% 0.11/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.40 % Memory : 8046.5625MB
% 0.11/0.40 % OS : Linux 6.8.0-71-generic
% 0.11/0.40 % CPULimit : 300
% 0.11/0.40 % WCLimit : 300
% 0.11/0.40 % DateTime : Sun Sep 27 13:59:46 UTC 2026
% 0.11/0.41 % CPUTime :
% 0.11/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.44 Running first-order theorem proving
% 0.11/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.34/3.23 % (1689036)Detected a unit-equality problem, will run specialized UEQ schedule.
% 18.34/3.23 % (1689046)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1721288484:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 18.34/3.23 % (1689043)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3148071035:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 18.34/3.23 % (1689045)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=587522399:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 18.34/3.23 % (1689047)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=367329137:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 18.34/3.23 % (1689042)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3695580648:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 18.34/3.23 % (1689041)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=3852642727:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 18.34/3.23 % (1689044)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3927989274:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 18.34/3.23 % (1689046)Instruction limit reached!
% 18.34/3.23 % (1689046)------------------------------
% 18.34/3.23 % (1689046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.23 % (1689046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.23 % (1689046)CaDiCaL version: 2.1.3
% 18.34/3.23 % (1689046)Termination reason: Instruction limit
% 18.34/3.23 % (1689046)Termination phase: Saturation
% 18.34/3.23 % (1689046)Time elapsed: 0.087 s
% 18.34/3.23 % (1689046)Peak memory usage: 90 MB
% 18.34/3.23 % (1689046)Instructions burned: 258 (million)
% 18.34/3.23 % (1689044)Instruction limit reached!
% 18.34/3.23 % (1689044)------------------------------
% 18.34/3.23 % (1689044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.23 % (1689044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.23 % (1689044)CaDiCaL version: 2.1.3
% 18.34/3.23 % (1689044)Termination reason: Instruction limit
% 18.34/3.23 % (1689044)Termination phase: Saturation
% 18.34/3.23 % (1689044)Time elapsed: 0.082 s
% 18.34/3.23 % (1689044)Peak memory usage: 89 MB
% 18.34/3.23 % (1689044)Instructions burned: 136 (million)
% 18.34/3.23 % (1689045)Instruction limit reached!
% 18.34/3.23 % (1689045)------------------------------
% 18.34/3.23 % (1689045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.23 % (1689045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.23 % (1689045)CaDiCaL version: 2.1.3
% 18.34/3.23 % (1689045)Termination reason: Instruction limit
% 18.34/3.23 % (1689045)Termination phase: Saturation
% 18.34/3.23 % (1689045)Time elapsed: 0.103 s
% 18.34/3.23 % (1689045)Peak memory usage: 90 MB
% 18.34/3.23 % (1689045)Instructions burned: 183 (million)
% 18.34/3.23 % (1689056)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2729007591:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 18.34/3.23 % (1689055)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3709316996:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 18.34/3.23 % (1689057)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3031856955:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 18.34/3.23 % (1689057)Instruction limit reached!
% 18.34/3.23 % (1689057)------------------------------
% 18.34/3.23 % (1689057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.23 % (1689057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.23 % (1689057)CaDiCaL version: 2.1.3
% 18.34/3.23 % (1689057)Termination reason: Instruction limit
% 18.34/3.23 % (1689057)Termination phase: Saturation
% 18.34/3.23 % (1689057)Time elapsed: 0.118 s
% 18.34/3.23 % (1689057)Peak memory usage: 91 MB
% 18.34/3.23 % (1689057)Instructions burned: 215 (million)
% 18.34/3.23 % (1689061)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=3455749106:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 18.34/3.23 % (1689047)Instruction limit reached!
% 18.34/3.23 % (1689047)------------------------------
% 18.34/3.23 % (1689047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.23 % (1689047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.23 % (1689047)CaDiCaL version: 2.1.3
% 18.34/3.23 % (1689047)Termination reason: Instruction limit
% 18.34/3.23 % (1689047)Termination phase: Saturation
% 18.34/3.23 % (1689047)Time elapsed: 0.601 s
% 18.34/3.23 % (1689047)Peak memory usage: 97 MB
% 18.34/3.23 % (1689047)Instructions burned: 1187 (million)
% 18.34/3.23 % (1689061)Instruction limit reached!
% 18.34/3.23 % (1689061)------------------------------
% 18.34/3.23 % (1689061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.23 % (1689061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.23 % (1689061)CaDiCaL version: 2.1.3
% 18.34/3.23 % (1689061)Termination reason: Instruction limit
% 18.34/3.23 % (1689061)Termination phase: Saturation
% 18.34/3.23 % (1689061)Time elapsed: 0.187 s
% 18.34/3.23 % (1689061)Peak memory usage: 94 MB
% 18.34/3.23 % (1689061)Instructions burned: 317 (million)
% 18.34/3.23 % (1689063)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=1548291775:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 18.34/3.23 % (1689064)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3585663754:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2992 on theBenchmark for (2992ds/2836Mi)
% 18.34/3.23 % (1689055)Instruction limit reached!
% 18.34/3.23 % (1689055)------------------------------
% 18.34/3.23 % (1689055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.34/3.23 % (1689055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.34/3.23 % (1689055)CaDiCaL version: 2.1.3
% 18.34/3.23 % (1689055)Termination reason: Instruction limit
% 18.34/3.23 % (1689055)Termination phase: Saturation
% 18.34/3.23 % (1689055)Time elapsed: 0.688 s
% 18.34/3.23 % (1689055)Peak memory usage: 138 MB
% 18.34/3.23 % (1689055)Instructions burned: 2053 (million)
% 18.34/3.23 % (1689067)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3301060162:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 18.34/3.23 % (1689067)First to succeed.
% 18.34/3.23 % (1689067)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1689036"
% 18.34/3.23 % (1689067)Refutation found. Thanks to Tanya!
% 18.34/3.23 % SZS status Unsatisfiable for theBenchmark
% 18.34/3.23 % SZS output start Proof for theBenchmark
% See solution above
% 18.65/3.32 % (1689067)------------------------------
% 18.65/3.32 % (1689067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.65/3.32 % (1689067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.65/3.32 % (1689067)CaDiCaL version: 2.1.3
% 18.65/3.32 % (1689067)Termination reason: Refutation
% 18.65/3.32 % (1689067)Time elapsed: 1.288 s
% 18.65/3.32 % (1689067)Peak memory usage: 152 MB
% 18.65/3.32 % (1689067)Instructions burned: 4084 (million)
% 18.65/3.32 % (1689067)------------------------------
% 18.65/3.32 % (1689067)------------------------------
% 18.65/3.32 % (1689036)Success in time 2.59 s
% 18.65/3.32 % Vampire exiting
%------------------------------------------------------------------------------