%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT183-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:46:10 AM UTC 2026
% Result : Unsatisfiable 104.62s 18.10s
% Output : Refutation 122.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 118
% Number of leaves : 12
% Syntax : Number of formulae : 512 ( 489 unt; 0 def)
% Number of atoms : 538 ( 537 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 54 ( 28 ~; 26 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 1376 (1376 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
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,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H7) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f15,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f17,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f25,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,meet(X1,join(meet(X1,X0),meet(X2,join(X0,X1)))))),
inference(superposition,[],[f12,f6]) ).
fof(f30,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X0,join(meet(X0,X1),meet(join(X0,X1),X2))))),
inference(superposition,[],[f12,f5]) ).
fof(f46,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f15,f3]) ).
fof(f51,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f46,f6]) ).
fof(f54,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f17,f4]) ).
fof(f55,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f17,f15]) ).
fof(f57,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f15,f17]) ).
fof(f61,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f57,f6]) ).
fof(f63,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f55,f5]) ).
fof(f64,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f54,f5]) ).
fof(f69,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f70,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f72,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f17]) ).
fof(f81,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f83,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f84,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(meet(X0,X1),X2))),
inference(superposition,[],[f3,f7]) ).
fof(f87,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f17,f7]) ).
fof(f88,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),X3))) = meet(meet(X0,X1),join(X2,meet(X0,meet(X1,join(meet(meet(X0,X1),X2),meet(X3,join(meet(X0,X1),X2))))))),
inference(superposition,[],[f12,f7]) ).
fof(f89,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),X3))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(meet(X0,X1),X2),meet(X3,join(meet(X0,X1),X2)))))))),
inference(forward_demodulation,[],[f88,f7]) ).
fof(f95,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),X3))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(X0,meet(X1,X2)),meet(X3,join(meet(X0,X1),X2)))))))),
inference(forward_demodulation,[],[f89,f7]) ).
fof(f100,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(X0,meet(X1,X2)),meet(X3,join(meet(X0,X1),X2)))))))) = meet(X0,meet(X1,join(X2,meet(meet(X0,X1),X3)))),
inference(forward_demodulation,[],[f95,f7]) ).
fof(f104,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(X0,meet(X1,X2)),meet(X3,join(meet(X0,X1),X2)))))))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,X3))))),
inference(forward_demodulation,[],[f100,f7]) ).
fof(f110,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f111,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f15]) ).
fof(f119,plain,
! [X2,X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))),
inference(superposition,[],[f3,f8]) ).
fof(f121,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f122,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f4,f8]) ).
fof(f123,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,X1),meet(X2,X3))) = meet(X2,join(X0,join(X1,meet(X2,join(meet(X2,join(X0,X1)),meet(X3,join(X2,join(X0,X1)))))))),
inference(superposition,[],[f12,f8]) ).
fof(f124,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(X2,join(X0,X1)))),
inference(superposition,[],[f15,f8]) ).
fof(f125,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,join(X1,meet(X2,join(meet(X2,join(X0,X1)),meet(X3,join(X2,join(X0,X1)))))))) = meet(X2,join(X0,join(X1,meet(X2,X3)))),
inference(forward_demodulation,[],[f123,f8]) ).
fof(f135,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f110,f6]) ).
fof(f141,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f17,f110]) ).
fof(f147,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f141,f5]) ).
fof(f164,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f70,f5]) ).
fof(f173,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f15,f70]) ).
fof(f177,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f173,f6]) ).
fof(f189,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,one),
inference(superposition,[],[f110,f9]) ).
fof(f190,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f191,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f193,plain,
! [X0] : complement(X0) = meet(complement(X0),one),
inference(superposition,[],[f17,f9]) ).
fof(f194,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(one,X1)),
inference(superposition,[],[f70,f9]) ).
fof(f195,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f196,plain,
! [X0] : complement(X0) = meet(one,complement(X0)),
inference(forward_demodulation,[],[f193,f5]) ).
fof(f200,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f204,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(zero,X1)),
inference(superposition,[],[f110,f10]) ).
fof(f205,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f223,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f190]) ).
fof(f226,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f15,f190]) ).
fof(f238,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f226]) ).
fof(f275,plain,
zero = complement(one),
inference(superposition,[],[f10,f223]) ).
fof(f305,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f200]) ).
fof(f331,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f15,f305]) ).
fof(f416,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f83,f17]) ).
fof(f438,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X3,X0)) = meet(X1,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f70,f83]) ).
fof(f507,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f111,f6]) ).
fof(f512,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X1,X0))),
inference(superposition,[],[f111,f9]) ).
fof(f534,plain,
! [X0,X1] : one = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f512,f238]) ).
fof(f600,plain,
! [X2,X3,X0,X1] : meet(X1,X3) = meet(X1,meet(join(X0,join(X1,X2)),X3)),
inference(superposition,[],[f70,f121]) ).
fof(f601,plain,
! [X2,X3,X0,X1] : join(X2,join(X3,X0)) = join(X2,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f111,f121]) ).
fof(f602,plain,
! [X2,X3,X0,X1] : join(X1,join(X3,X0)) = join(X1,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f110,f121]) ).
fof(f616,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X2,join(X3,join(X0,X1))),
inference(superposition,[],[f8,f121]) ).
fof(f680,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f72,f5]) ).
fof(f684,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X3,X0)) = meet(X2,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f72,f83]) ).
fof(f688,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f72,f10]) ).
fof(f718,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f688,f331]) ).
fof(f792,plain,
! [X0,X1] : one = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f195,f6]) ).
fof(f818,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(superposition,[],[f11,f195]) ).
fof(f829,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f818]) ).
fof(f873,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f829,f6]) ).
fof(f937,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f205,f5]) ).
fof(f1045,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X1,X0)),meet(X0,X2))) = meet(X0,join(complement(meet(X1,X0)),meet(X0,join(meet(X0,complement(meet(X1,X0))),meet(X2,one))))),
inference(superposition,[],[f12,f534]) ).
fof(f1065,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X1,X0)),meet(X0,X2))) = meet(X0,join(complement(meet(X1,X0)),meet(X0,join(meet(X0,complement(meet(X1,X0))),X2)))),
inference(forward_demodulation,[],[f1045,f190]) ).
fof(f1347,plain,
! [X2,X0,X1] : meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),join(X1,meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X0))) = meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),join(X1,meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),join(meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X1),meet(X0,join(X1,meet(X0,X2))))))),
inference(superposition,[],[f25,f12]) ).
fof(f1414,plain,
! [X2,X0,X1] : meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),join(X1,meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X0))) = meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),join(meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X1),meet(X0,join(X1,meet(X0,X2)))))))),
inference(forward_demodulation,[],[f1347,f7]) ).
fof(f1459,plain,
! [X2,X0,X1] : meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),join(X1,meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X0))) = meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X1),meet(X0,join(X1,meet(X0,X2))))))))),
inference(forward_demodulation,[],[f1414,f7]) ).
fof(f1491,plain,
! [X2,X0,X1] : meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),join(X1,meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X0))) = meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(meet(X0,join(X1,meet(X0,X2))),meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X1))))))),
inference(forward_demodulation,[],[f1459,f6]) ).
fof(f1514,plain,
! [X2,X0,X1] : meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),join(X1,meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X0))) = meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(meet(X0,join(X1,meet(X0,X2))),meet(X1,meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1))))))))))),
inference(forward_demodulation,[],[f1491,f5]) ).
fof(f1526,plain,
! [X2,X0,X1] : meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(meet(X0,join(X1,meet(X0,X2))),meet(X1,meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1))))))))))) = meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))),X0)))),
inference(forward_demodulation,[],[f1514,f7]) ).
fof(f1531,plain,
! [X2,X0,X1] : meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(meet(X0,join(X1,meet(X0,X2))),meet(X1,meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1))))))))))) = meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))))))),
inference(forward_demodulation,[],[f1526,f5]) ).
fof(f1535,plain,
! [X2,X0,X1] : meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(meet(X0,join(X1,meet(X0,X2))),meet(X1,meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1))))))))))) = meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1))))))),
inference(forward_demodulation,[],[f1531,f64]) ).
fof(f1538,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(X2,join(X0,X1))),join(meet(X0,join(X1,meet(X0,X2))),meet(X1,meet(X0,join(meet(X0,X1),meet(X2,join(X0,X1))))))))))),
inference(forward_demodulation,[],[f1535,f87]) ).
fof(f1836,plain,
! [X2,X0,X1] : join(one,join(X2,X0)) = join(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f191,f121]) ).
fof(f1895,plain,
! [X2,X0,X1] : one = join(X1,join(X0,join(complement(X1),X2))),
inference(forward_demodulation,[],[f1836,f226]) ).
fof(f2521,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(superposition,[],[f718,f6]) ).
fof(f2713,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),X3) = meet(X0,meet(meet(X1,join(X0,X2)),X3)),
inference(superposition,[],[f7,f164]) ).
fof(f2748,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),X3) = meet(X0,meet(X1,meet(join(X0,X2),X3))),
inference(forward_demodulation,[],[f2713,f7]) ).
fof(f2770,plain,
! [X3,X0,X1] : meet(meet(X0,X1),X3) = meet(X0,meet(X3,X1)),
inference(forward_demodulation,[],[f2748,f438]) ).
fof(f3205,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),X3))) = meet(X0,meet(X1,join(X2,meet(meet(X0,X1),join(meet(meet(X0,X1),X2),meet(join(meet(X0,X1),X2),X3)))))),
inference(superposition,[],[f7,f30]) ).
fof(f3215,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),X3))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(meet(X0,X1),X2),meet(join(meet(X0,X1),X2),X3))))))),
inference(forward_demodulation,[],[f3205,f7]) ).
fof(f3307,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),X3))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(X0,meet(X1,X2)),meet(join(meet(X0,X1),X2),X3))))))),
inference(forward_demodulation,[],[f3215,f7]) ).
fof(f3363,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,meet(meet(X0,X1),X3)))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(X0,meet(X1,X2)),meet(join(meet(X0,X1),X2),X3))))))),
inference(forward_demodulation,[],[f3307,f7]) ).
fof(f3397,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,X3))))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(X0,meet(X1,X2)),meet(join(meet(X0,X1),X2),X3))))))),
inference(forward_demodulation,[],[f3363,f7]) ).
fof(f3597,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(join(X1,meet(X0,X2)),X3)),
inference(superposition,[],[f8,f135]) ).
fof(f3643,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(X1,join(meet(X0,X2),X3))),
inference(forward_demodulation,[],[f3597,f8]) ).
fof(f3669,plain,
! [X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(X3,X1)),
inference(forward_demodulation,[],[f3643,f602]) ).
fof(f3695,plain,
! [X0,X1] :
( zero != meet(join(X0,complement(join(X0,X1))),join(X1,complement(one)))
| join(X1,complement(one)) = complement(join(X0,complement(join(X0,X1)))) ),
inference(superposition,[],[f873,f792]) ).
fof(f3696,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(superposition,[],[f873,f9]) ).
fof(f3725,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f3696,f275]) ).
fof(f3726,plain,
! [X0,X1] :
( zero != meet(join(X1,complement(one)),join(X0,complement(join(X0,X1))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f3695,f5]) ).
fof(f3743,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f3725,f200]) ).
fof(f3744,plain,
! [X0,X1] :
( zero != meet(join(X1,zero),join(X0,complement(join(X0,X1))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f3726,f275]) ).
fof(f3755,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f3743,f5]) ).
fof(f3756,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f3744,f200]) ).
fof(f3764,plain,
! [X0] : join(X0,complement(one)) = complement(complement(X0)),
inference(forward_subsumption_resolution,[],[f3755,f10]) ).
fof(f3765,plain,
! [X0,X1] :
( join(X1,zero) = complement(join(X0,complement(join(X0,X1))))
| zero != meet(X1,join(X0,complement(join(X0,X1)))) ),
inference(forward_demodulation,[],[f3756,f275]) ).
fof(f3771,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f3764,f275]) ).
fof(f3772,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(join(X0,complement(join(X0,X1)))) = X1 ),
inference(forward_demodulation,[],[f3765,f200]) ).
fof(f3776,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f3771,f200]) ).
fof(f4160,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(one,X1))),
inference(superposition,[],[f194,f83]) ).
fof(f4274,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f4160,f194]) ).
fof(f4418,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f5,f4274]) ).
fof(f4999,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X1,meet(X2,X0)),join(X0,X1)),
inference(superposition,[],[f17,f507]) ).
fof(f5044,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f4999,f5]) ).
fof(f5231,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(meet(X1,X0),X2))),
inference(superposition,[],[f3,f69]) ).
fof(f5504,plain,
! [X0,X1] : meet(X0,join(complement(meet(X1,X0)),meet(X0,one))) = meet(X0,join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0))))))),
inference(superposition,[],[f1065,f9]) ).
fof(f5609,plain,
! [X0,X1] : meet(X0,join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0))))))) = meet(X0,join(meet(X0,one),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f5504,f6]) ).
fof(f5694,plain,
! [X0,X1] : meet(X0,join(X0,complement(meet(X1,X0)))) = meet(X0,join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0))))))),
inference(forward_demodulation,[],[f5609,f190]) ).
fof(f5758,plain,
! [X0,X1] : meet(X0,join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0))))))) = X0,
inference(forward_demodulation,[],[f5694,f3]) ).
fof(f5961,plain,
! [X0,X1] : join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))) = join(join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))),X0),
inference(superposition,[],[f15,f5758]) ).
fof(f6012,plain,
! [X0,X1] : join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))) = join(X0,join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0))))))),
inference(forward_demodulation,[],[f5961,f6]) ).
fof(f6071,plain,
! [X0,X1] : join(X0,complement(meet(X1,X0))) = join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f6012,f135]) ).
fof(f6112,plain,
! [X0,X1] : one = join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f6071,f534]) ).
fof(f6176,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(unit_resulting_resolution,[],[f11,f937,f6112]) ).
fof(f6179,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f6112,f5]) ).
fof(f6318,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f6176,f3776]) ).
fof(f6920,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f81,f63]) ).
fof(f7491,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),X0)),
inference(superposition,[],[f177,f5]) ).
fof(f7507,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(join(X0,X1),join(X0,X2))),
inference(superposition,[],[f177,f3]) ).
fof(f7819,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X0,X1),join(meet(X1,X2),X0)),
inference(superposition,[],[f147,f6]) ).
fof(f7820,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f147,f4]) ).
fof(f8190,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f119,f61]) ).
fof(f8458,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(join(X0,X1),meet(join(X1,X0),X2)),
inference(superposition,[],[f83,f8190]) ).
fof(f8475,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f4274,f8190]) ).
fof(f8477,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f4418,f8190]) ).
fof(f8484,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(join(X0,X1),X2),
inference(forward_demodulation,[],[f8477,f8190]) ).
fof(f8486,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f8475,f8190]) ).
fof(f8650,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X2,join(X0,X1))),
inference(superposition,[],[f8486,f8]) ).
fof(f8754,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X2,X1),X3)) = meet(X3,meet(X0,join(X1,X2))),
inference(superposition,[],[f83,f8486]) ).
fof(f8872,plain,
! [X2,X0,X1] : join(X2,join(X1,X0)) = join(X2,join(X0,join(zero,X1))),
inference(superposition,[],[f204,f121]) ).
fof(f9007,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f8872,f204]) ).
fof(f9078,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f9007,f6920]) ).
fof(f9172,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f6,f9007]) ).
fof(f9269,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(X2,meet(X0,X1)),
inference(forward_demodulation,[],[f9078,f6920]) ).
fof(f9347,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X0,meet(X2,X1))),
inference(superposition,[],[f9269,f4418]) ).
fof(f9348,plain,
! [X2,X3,X0,X1] : join(X3,meet(X2,meet(X0,X1))) = join(X3,meet(X0,meet(X1,X2))),
inference(superposition,[],[f9269,f7]) ).
fof(f9430,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f9269]) ).
fof(f9676,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(superposition,[],[f6,f9430]) ).
fof(f9757,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(X3,join(X0,meet(X2,X1))),
inference(superposition,[],[f8486,f9430]) ).
fof(f10232,plain,
! [X0,X1] : one = join(meet(X0,X1),complement(meet(X1,X0))),
inference(superposition,[],[f9,f9676]) ).
fof(f11300,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X0,join(X2,X1))),
inference(superposition,[],[f8486,f9172]) ).
fof(f11645,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(unit_resulting_resolution,[],[f11,f937,f6179]) ).
fof(f11799,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f11645,f3776]) ).
fof(f12055,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(meet(X0,X1),meet(X0,X2)),X3)) = meet(X3,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f83,f7820]) ).
fof(f12354,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X2,join(X1,meet(X0,meet(X2,X3))))) = meet(X0,meet(X2,join(X1,meet(X0,meet(X2,join(meet(X0,meet(X1,X2)),meet(X3,join(meet(X0,X2),X1)))))))),
inference(superposition,[],[f104,f4274]) ).
fof(f12385,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),join(meet(X0,meet(meet(X1,join(X2,X0)),X3)),meet(X4,join(meet(X0,X1),X3)))))))),
inference(superposition,[],[f104,f680]) ).
fof(f12719,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(X1,meet(join(X2,X0),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),join(meet(X0,meet(meet(X1,join(X2,X0)),X3)),meet(X4,join(meet(X0,X1),X3))))))))),
inference(forward_demodulation,[],[f12385,f7]) ).
fof(f12902,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(join(X3,meet(X0,meet(meet(X1,join(X2,X0)),join(meet(X0,meet(meet(X1,join(X2,X0)),X3)),meet(X4,join(meet(X0,X1),X3)))))),X1)),
inference(forward_demodulation,[],[f12719,f684]) ).
fof(f13048,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(meet(X1,join(X2,X0)),join(meet(X0,meet(meet(X1,join(X2,X0)),X3)),meet(X4,join(meet(X0,X1),X3)))))))),
inference(forward_demodulation,[],[f12902,f4274]) ).
fof(f13163,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(X1,meet(join(X2,X0),join(meet(X0,meet(meet(X1,join(X2,X0)),X3)),meet(X4,join(meet(X0,X1),X3))))))))),
inference(forward_demodulation,[],[f13048,f7]) ).
fof(f13256,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(join(meet(X0,meet(meet(X1,join(X2,X0)),X3)),meet(X4,join(meet(X0,X1),X3))),X1))))),
inference(forward_demodulation,[],[f13163,f684]) ).
fof(f13304,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(X1,join(meet(X0,meet(meet(X1,join(X2,X0)),X3)),meet(X4,join(meet(X0,X1),X3)))))))),
inference(forward_demodulation,[],[f13256,f9347]) ).
fof(f13334,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(X1,join(meet(X0,meet(X1,meet(join(X2,X0),X3))),meet(X4,join(meet(X0,X1),X3)))))))),
inference(forward_demodulation,[],[f13304,f7]) ).
fof(f13359,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(X1,join(meet(X0,meet(X3,X1)),meet(X4,join(meet(X0,X1),X3)))))))),
inference(forward_demodulation,[],[f13334,f684]) ).
fof(f13381,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(meet(X1,join(X2,X0)),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(X1,X4))))),
inference(forward_demodulation,[],[f13359,f12354]) ).
fof(f13399,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(X1,join(X3,meet(X0,meet(X1,X4))))) = meet(X0,meet(X1,meet(join(X2,X0),join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4)))))),
inference(forward_demodulation,[],[f13381,f7]) ).
fof(f13416,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(X1,join(X3,meet(X0,meet(X1,X4))))) = meet(X0,meet(join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))),X1)),
inference(forward_demodulation,[],[f13399,f684]) ).
fof(f13429,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(X1,join(X3,meet(X0,meet(X1,X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(meet(X1,join(X2,X0)),X4))))),
inference(forward_demodulation,[],[f13416,f4274]) ).
fof(f13435,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(X1,join(X3,meet(X0,meet(X1,X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(X1,meet(join(X2,X0),X4)))))),
inference(forward_demodulation,[],[f13429,f7]) ).
fof(f13440,plain,
! [X3,X0,X1,X4] : meet(X0,meet(X1,join(X3,meet(X0,meet(X1,X4))))) = meet(X0,meet(X1,join(X3,meet(X0,meet(X4,X1))))),
inference(forward_demodulation,[],[f13435,f684]) ).
fof(f13450,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X2),X1) = join(meet(X0,X1),meet(join(meet(X0,X1),X2),X1)),
inference(superposition,[],[f7491,f63]) ).
fof(f13546,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,join(X1,X2))),
inference(superposition,[],[f7491,f5]) ).
fof(f13595,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = join(meet(X2,X0),meet(X2,join(X0,X1))),
inference(superposition,[],[f9269,f7491]) ).
fof(f13741,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X2),X1) = join(meet(X0,X1),meet(X1,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f13450,f9269]) ).
fof(f13827,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X1,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f13741,f5]) ).
fof(f14037,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,X2)),X3) = meet(X3,join(X0,meet(X2,X1))),
inference(superposition,[],[f8484,f9430]) ).
fof(f14073,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f5,f8484]) ).
fof(f14117,plain,
! [X2,X3,X0,X1] : join(X3,meet(join(X0,X1),X2)) = join(X3,meet(join(X1,X0),X2)),
inference(superposition,[],[f9269,f8484]) ).
fof(f14205,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(X4,X3)))))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(meet(X0,meet(X1,X2)),meet(join(meet(X0,X1),X2),join(X3,X4)))))))),
inference(superposition,[],[f104,f8484]) ).
fof(f14211,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(X4,X3)))))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,join(X3,X4)))))),
inference(forward_demodulation,[],[f14205,f3397]) ).
fof(f14480,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,X2)),X3) = meet(join(X0,meet(X2,X1)),X3),
inference(superposition,[],[f14073,f9430]) ).
fof(f15071,plain,
! [X0,X1] :
( one != one
| zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(superposition,[],[f11,f10232]) ).
fof(f15106,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f15071]) ).
fof(f15132,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f15106,f7]) ).
fof(f15228,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f15132,f937]) ).
fof(f15432,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f15228,f8190]) ).
fof(f15496,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f15432,f8190]) ).
fof(f16562,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X2),join(X0,meet(X1,X2))),
inference(superposition,[],[f7819,f9430]) ).
fof(f16572,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(join(X0,meet(X1,X2)),X1),join(X0,meet(X1,X2))),
inference(superposition,[],[f7819,f61]) ).
fof(f16716,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X2,X1)),join(join(X0,meet(X1,X2)),X1)),
inference(forward_demodulation,[],[f16572,f14037]) ).
fof(f16803,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X2,X1)),join(X1,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f16716,f8486]) ).
fof(f16865,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X2,X1)),join(X1,X0)),
inference(forward_demodulation,[],[f16803,f135]) ).
fof(f16905,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X1),join(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f16865,f8484]) ).
fof(f17025,plain,
! [X2,X0,X1] : join(X1,meet(join(X2,X0),X0)) = meet(join(X1,join(X2,X0)),join(X1,X0)),
inference(superposition,[],[f16905,f17]) ).
fof(f17229,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,join(X2,X0))) = join(X1,meet(join(X2,X0),X0)),
inference(forward_demodulation,[],[f17025,f8484]) ).
fof(f17349,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,join(X2,X0))) = join(X1,meet(X0,join(X2,X0))),
inference(forward_demodulation,[],[f17229,f9269]) ).
fof(f17420,plain,
! [X2,X0,X1] : join(X1,X0) = meet(join(X0,X1),join(X1,join(X2,X0))),
inference(forward_demodulation,[],[f17349,f17]) ).
fof(f17736,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(join(X0,X1),complement(X0)))) = X0,
inference(superposition,[],[f6318,f3]) ).
fof(f17742,plain,
! [X0,X1] : meet(join(X1,X0),complement(meet(join(X1,X0),complement(X0)))) = X0,
inference(superposition,[],[f6318,f17]) ).
fof(f17775,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(superposition,[],[f6318,f15228]) ).
fof(f17931,plain,
! [X0,X1] : meet(join(X1,X0),complement(meet(complement(X0),join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f17742,f15228]) ).
fof(f17937,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f17736,f15228]) ).
fof(f18851,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(meet(X0,X2),X1),join(X1,X0)),
inference(superposition,[],[f17420,f4]) ).
fof(f18852,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(meet(X2,X0),X1),join(X1,X0)),
inference(superposition,[],[f17420,f15]) ).
fof(f19089,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f18852,f8484]) ).
fof(f19090,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f18851,f8484]) ).
fof(f19398,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(meet(X0,X2),meet(X1,X0))),
inference(superposition,[],[f19090,f15]) ).
fof(f22003,plain,
! [X0,X1] : complement(X0) = meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1)))),
inference(superposition,[],[f17937,f3776]) ).
fof(f23445,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X1,X2)) = join(X1,meet(join(X0,X1),join(X1,X2))),
inference(superposition,[],[f7507,f8484]) ).
fof(f24839,plain,
! [X2,X3,X0,X1] : join(X1,join(meet(X0,X1),X2)) = join(X1,join(X2,meet(X3,join(meet(X0,X1),X2)))),
inference(superposition,[],[f111,f124]) ).
fof(f24844,plain,
! [X2,X3,X0,X1] : join(join(X2,meet(X3,join(meet(X0,X1),X2))),meet(X0,X1)) = meet(join(X1,join(X2,meet(X3,join(meet(X0,X1),X2)))),join(meet(X0,X1),X2)),
inference(superposition,[],[f19089,f124]) ).
fof(f24865,plain,
! [X2,X3,X0,X1] : join(join(X2,meet(X3,join(meet(X0,X1),X2))),meet(X0,X1)) = meet(join(X2,meet(X0,X1)),join(X1,join(X2,meet(X3,join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f24844,f8484]) ).
fof(f24867,plain,
! [X2,X3,X0,X1] : join(X1,X2) = join(X1,join(X2,meet(X3,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f24839,f111]) ).
fof(f24982,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),join(X2,meet(X3,join(meet(X0,X1),X2)))) = meet(join(X2,meet(X0,X1)),join(X1,join(X2,meet(X3,join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f24865,f6]) ).
fof(f25031,plain,
! [X2,X3,X0,X1] : meet(join(X2,meet(X0,X1)),join(X1,X2)) = join(meet(X0,X1),join(X2,meet(X3,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f24982,f24867]) ).
fof(f25049,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,meet(X0,X1)),join(X1,X2)),
inference(forward_demodulation,[],[f25031,f124]) ).
fof(f25058,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,X1),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f25049,f8484]) ).
fof(f25919,plain,
! [X0,X1] : complement(X1) = meet(join(X0,complement(X1)),complement(meet(X1,join(X0,complement(X1))))),
inference(superposition,[],[f22003,f61]) ).
fof(f25965,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(X1,complement(meet(X0,join(complement(X0),X1)))),
inference(superposition,[],[f72,f22003]) ).
fof(f38020,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(meet(X1,X0)),X1),
inference(superposition,[],[f17775,f17775]) ).
fof(f38213,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f38020,f5]) ).
fof(f38571,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f15,f38213]) ).
fof(f62675,plain,
! [X2,X0,X1] : zero = meet(meet(X0,X1),complement(meet(X0,join(X1,X2)))),
inference(superposition,[],[f2521,f13546]) ).
fof(f62739,plain,
! [X2,X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f62675,f7]) ).
fof(f68483,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(meet(X0,join(X1,zero)),meet(X1,meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1))))))))))),
inference(superposition,[],[f1538,f10]) ).
fof(f69515,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(meet(X0,join(X1,zero)),meet(X0,X1))))))),
inference(forward_demodulation,[],[f68483,f5231]) ).
fof(f70059,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(meet(X0,X1),meet(X0,join(X1,zero)))))))),
inference(forward_demodulation,[],[f69515,f14211]) ).
fof(f70577,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(X0,meet(join(meet(X0,X1),meet(X0,join(X1,zero))),join(meet(X0,X1),meet(complement(X0),join(X0,X1)))))))),
inference(forward_demodulation,[],[f70059,f13440]) ).
fof(f71084,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(meet(X0,X1),meet(X0,join(X1,zero))))))),
inference(forward_demodulation,[],[f70577,f12055]) ).
fof(f71578,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(join(meet(X0,X1),meet(X0,join(X1,zero))),join(meet(X0,X1),meet(complement(X0),join(X0,X1))))))),
inference(forward_demodulation,[],[f71084,f9757]) ).
fof(f72069,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(meet(join(X1,zero),X0),join(meet(X0,X1),meet(complement(X0),join(X0,X1))))))),
inference(forward_demodulation,[],[f71578,f13595]) ).
fof(f72554,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(join(X1,zero),meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))))))),
inference(forward_demodulation,[],[f72069,f7]) ).
fof(f73015,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),join(X1,meet(X1,meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))))))),
inference(forward_demodulation,[],[f72554,f200]) ).
fof(f73462,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(complement(X0),join(X0,X1))),X1)),
inference(forward_demodulation,[],[f73015,f4]) ).
fof(f73845,plain,
! [X0,X1] : meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) = meet(X0,meet(X1,join(meet(X0,X1),meet(complement(X0),join(X0,X1))))),
inference(forward_demodulation,[],[f73462,f4274]) ).
fof(f74169,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f73845,f84]) ).
fof(f75641,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,complement(meet(X0,complement(meet(X0,X1)))))))),
inference(superposition,[],[f74169,f11799]) ).
fof(f75642,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(meet(X0,X1),meet(complement(X1),join(X1,complement(meet(X1,complement(meet(X1,X0)))))))),
inference(superposition,[],[f74169,f17775]) ).
fof(f75668,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,meet(complement(join(X0,X1)),join(join(X0,X1),complement(meet(complement(X0),join(X0,X1))))))) = X0,
inference(superposition,[],[f74169,f17937]) ).
fof(f75669,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,meet(complement(join(X1,X0)),join(join(X1,X0),complement(meet(complement(X0),join(X1,X0))))))) = X0,
inference(superposition,[],[f74169,f17931]) ).
fof(f76102,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,meet(complement(join(X1,X0)),one))) = X0,
inference(forward_demodulation,[],[f75669,f534]) ).
fof(f76103,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,meet(complement(join(X0,X1)),one))) = X0,
inference(forward_demodulation,[],[f75668,f534]) ).
fof(f76123,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(meet(X0,X1),meet(complement(X1),join(X1,one)))),
inference(forward_demodulation,[],[f75642,f189]) ).
fof(f76124,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),meet(complement(X0),join(X0,one)))),
inference(forward_demodulation,[],[f75641,f189]) ).
fof(f76308,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,meet(one,complement(join(X1,X0))))) = X0,
inference(forward_demodulation,[],[f76102,f9757]) ).
fof(f76309,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,meet(one,complement(join(X0,X1))))) = X0,
inference(forward_demodulation,[],[f76103,f9757]) ).
fof(f76318,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(meet(X0,X1),meet(complement(X1),one))),
inference(forward_demodulation,[],[f76123,f238]) ).
fof(f76319,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),meet(complement(X0),one))),
inference(forward_demodulation,[],[f76124,f238]) ).
fof(f76427,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f76308,f196]) ).
fof(f76428,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f76309,f196]) ).
fof(f76437,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(meet(X0,X1),meet(one,complement(X1)))),
inference(forward_demodulation,[],[f76318,f9757]) ).
fof(f76438,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),meet(one,complement(X0)))),
inference(forward_demodulation,[],[f76319,f9757]) ).
fof(f76515,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(meet(X0,X1),complement(X1))),
inference(forward_demodulation,[],[f76437,f196]) ).
fof(f76516,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),complement(X0))),
inference(forward_demodulation,[],[f76438,f196]) ).
fof(f76561,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f76515,f8486]) ).
fof(f76562,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f76516,f8486]) ).
fof(f76777,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X1,X2)) = meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,X2)))),
inference(superposition,[],[f76562,f19398]) ).
fof(f76986,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),meet(join(complement(X0),meet(X0,X1)),complement(meet(join(complement(X0),meet(X0,X1)),X0)))),
inference(superposition,[],[f38571,f76562]) ).
fof(f77034,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),meet(join(complement(X0),meet(X0,X1)),complement(meet(X0,join(complement(X0),meet(X0,X1)))))),
inference(forward_demodulation,[],[f76986,f38213]) ).
fof(f77179,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(forward_demodulation,[],[f77034,f22003]) ).
fof(f77275,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f77179,f6]) ).
fof(f77624,plain,
! [X2,X0,X1] : meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,X2)))) = meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,join(meet(X0,X1),meet(X2,join(X1,join(complement(X1),meet(X0,X1))))))))),
inference(superposition,[],[f125,f76561]) ).
fof(f77732,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),meet(join(complement(X1),meet(X0,X1)),complement(meet(join(complement(X1),meet(X0,X1)),X1)))),
inference(superposition,[],[f38571,f76561]) ).
fof(f77779,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),meet(join(complement(X1),meet(X0,X1)),complement(meet(X1,join(complement(X1),meet(X0,X1)))))),
inference(forward_demodulation,[],[f77732,f38213]) ).
fof(f77852,plain,
! [X2,X0,X1] : meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,X2)))) = join(meet(X0,X1),meet(X1,join(meet(X0,X1),meet(X2,join(X1,join(complement(X1),meet(X0,X1))))))),
inference(forward_demodulation,[],[f77624,f76777]) ).
fof(f77958,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X1)),
inference(forward_demodulation,[],[f77779,f22003]) ).
fof(f78013,plain,
! [X2,X0,X1] : meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,X2)))) = meet(X1,join(meet(X0,X1),meet(X2,join(X1,join(complement(X1),meet(X0,X1)))))),
inference(forward_demodulation,[],[f77852,f13827]) ).
fof(f78092,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f77958,f6]) ).
fof(f78122,plain,
! [X2,X0,X1] : meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,X2)))) = meet(X1,join(meet(X0,X1),meet(X2,join(X1,complement(X1))))),
inference(forward_demodulation,[],[f78013,f507]) ).
fof(f78172,plain,
! [X2,X0,X1] : meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,X2)))) = meet(X1,join(meet(X0,X1),meet(X2,one))),
inference(forward_demodulation,[],[f78122,f9]) ).
fof(f78204,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,X2)))),
inference(forward_demodulation,[],[f78172,f190]) ).
fof(f78399,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f72,f76428]) ).
fof(f78524,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(join(X0,complement(join(X0,X1))),complement(meet(join(X0,complement(join(X0,X1))),join(X0,X1))))),
inference(superposition,[],[f38571,f76428]) ).
fof(f78542,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(join(X0,complement(join(X0,X1))),complement(meet(join(X0,X1),join(X0,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f78524,f38213]) ).
fof(f78680,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f78542,f25919]) ).
fof(f78977,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f78399,f15496]) ).
fof(f79698,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f78680,f3776]) ).
fof(f79766,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f78680,f15496]) ).
fof(f79779,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f17,f78680]) ).
fof(f79817,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f3669,f78680]) ).
fof(f79903,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f79779,f5]) ).
fof(f80018,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f79903,f3776]) ).
fof(f80086,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f79903,f15496]) ).
fof(f80792,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(superposition,[],[f77275,f3776]) ).
fof(f80924,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(superposition,[],[f3,f77275]) ).
fof(f81153,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,complement(meet(X1,complement(X0)))),
inference(superposition,[],[f78092,f3776]) ).
fof(f81657,plain,
! [X2,X0,X1] : join(X1,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(join(X1,meet(join(X0,X1),X2)),complement(join(X0,X1)))),
inference(superposition,[],[f76427,f122]) ).
fof(f81728,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),join(X0,meet(X2,join(join(X1,X0),join(X0,complement(join(X1,X0)))))))))),
inference(superposition,[],[f125,f76427]) ).
fof(f81953,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),join(X0,meet(X2,join(X0,join(complement(join(X1,X0)),join(X1,X0))))))))),
inference(forward_demodulation,[],[f81728,f8650]) ).
fof(f81991,plain,
! [X2,X0,X1] : join(X1,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(complement(join(X0,X1)),join(X1,meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f81657,f8486]) ).
fof(f82076,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),join(X0,meet(X2,join(X0,join(join(X1,X0),complement(join(X1,X0)))))))))),
inference(forward_demodulation,[],[f81953,f11300]) ).
fof(f82104,plain,
! [X2,X0,X1] : join(X1,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X1,join(meet(join(X0,X1),X2),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f81991,f8650]) ).
fof(f82151,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),join(X0,meet(X2,join(X0,one))))))),
inference(forward_demodulation,[],[f82076,f9]) ).
fof(f82171,plain,
! [X2,X0,X1] : join(X1,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X1,join(complement(join(X0,X1)),meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f82104,f11300]) ).
fof(f82199,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),join(X0,meet(X2,one)))))),
inference(forward_demodulation,[],[f82151,f238]) ).
fof(f82223,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),X2)))) = join(X0,meet(join(X1,X0),join(X0,meet(X2,one)))),
inference(forward_demodulation,[],[f82199,f82171]) ).
fof(f82240,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,meet(X2,one))) = meet(join(X1,X0),join(X0,join(complement(join(X1,X0)),meet(join(X1,X0),X2)))),
inference(forward_demodulation,[],[f82223,f23445]) ).
fof(f82254,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(X0,meet(X2,one))),
inference(forward_demodulation,[],[f82240,f82171]) ).
fof(f82266,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(X0,X2)),
inference(forward_demodulation,[],[f82254,f190]) ).
fof(f82290,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = meet(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f82266,f6]) ).
fof(f82291,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f82266,f4]) ).
fof(f82341,plain,
! [X2,X3,X0,X1] : join(X1,meet(join(X0,join(X1,X2)),X3)) = meet(join(X0,join(X1,X2)),join(X1,X3)),
inference(superposition,[],[f82266,f3669]) ).
fof(f82371,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X1,X2))) = meet(join(X2,X1),join(X1,X0)),
inference(superposition,[],[f82266,f8484]) ).
fof(f82394,plain,
! [X2,X3,X0,X1] : join(X2,meet(X0,meet(join(X1,X2),X3))) = meet(join(X1,X2),join(X2,meet(X3,X0))),
inference(superposition,[],[f82266,f83]) ).
fof(f82489,plain,
! [X2,X0,X1] : join(X1,meet(X2,join(X0,X1))) = meet(join(X0,X1),join(X1,X2)),
inference(superposition,[],[f9269,f82266]) ).
fof(f83490,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(meet(X0,X2),join(complement(X0),meet(X0,X1)))),
inference(superposition,[],[f82291,f76562]) ).
fof(f83498,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X0,X1)) = meet(X1,join(meet(X1,X2),join(complement(X1),meet(X0,X1)))),
inference(superposition,[],[f82291,f76561]) ).
fof(f83599,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,meet(X0,join(meet(X0,X1),X2))),
inference(superposition,[],[f111,f82291]) ).
fof(f83908,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X0,X1)) = meet(X1,join(complement(X1),join(meet(X0,X1),meet(X1,X2)))),
inference(forward_demodulation,[],[f83498,f8650]) ).
fof(f83916,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X0,X1),meet(X0,X2)))) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f83490,f8650]) ).
fof(f84136,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = join(meet(X1,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f83908,f78204]) ).
fof(f84141,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f83916,f82291]) ).
fof(f84280,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(complement(X0),meet(X0,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f84141,f82291]) ).
fof(f84366,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f84280,f76562]) ).
fof(f88523,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(join(X0,X1))),
inference(superposition,[],[f80924,f17420]) ).
fof(f90232,plain,
! [X2,X3,X0,X1] : join(X2,meet(X0,meet(X1,join(X2,X3)))) = meet(join(X2,X3),join(X2,meet(X0,X1))),
inference(superposition,[],[f82290,f83]) ).
fof(f90233,plain,
! [X2,X3,X0,X1] : join(X1,meet(X0,meet(join(X1,X2),X3))) = meet(join(X1,X2),join(X1,meet(X3,X0))),
inference(superposition,[],[f82290,f83]) ).
fof(f90430,plain,
! [X2,X0,X1] : meet(X0,join(meet(join(meet(X0,X1),X2),X0),X1)) = meet(join(meet(X0,X1),X2),join(meet(X0,X1),X0)),
inference(superposition,[],[f84136,f82290]) ).
fof(f90515,plain,
! [X2,X0,X1] : meet(X0,join(meet(join(meet(X0,X1),X2),X0),X1)) = meet(join(meet(X0,X1),X2),join(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f90430,f8486]) ).
fof(f90774,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X2),X0) = meet(X0,join(meet(join(meet(X0,X1),X2),X0),X1)),
inference(forward_demodulation,[],[f90515,f4]) ).
fof(f90925,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X2),X0) = meet(X0,join(X1,meet(join(meet(X0,X1),X2),X0))),
inference(forward_demodulation,[],[f90774,f8486]) ).
fof(f91021,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X2),X0) = meet(X0,join(X1,meet(X0,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f90925,f9757]) ).
fof(f91086,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(join(meet(X0,X1),X2),X0),
inference(forward_demodulation,[],[f91021,f83599]) ).
fof(f91128,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f91086,f5]) ).
fof(f91414,plain,
! [X2,X0,X1] : meet(X1,complement(join(X2,X0))) = meet(complement(join(X2,X0)),meet(complement(X0),X1)),
inference(superposition,[],[f416,f79766]) ).
fof(f91456,plain,
! [X2,X0,X1] : join(meet(X1,complement(join(X2,X0))),complement(X0)) = meet(complement(X0),join(complement(X0),meet(X1,complement(join(X2,X0))))),
inference(superposition,[],[f25058,f79766]) ).
fof(f91460,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),join(complement(join(X1,X0)),complement(complement(X0)))),
inference(superposition,[],[f76427,f79766]) ).
fof(f91469,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),join(complement(complement(X0)),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f91460,f8486]) ).
fof(f91472,plain,
! [X2,X0,X1] : complement(X0) = join(meet(X1,complement(join(X2,X0))),complement(X0)),
inference(forward_demodulation,[],[f91456,f3]) ).
fof(f91501,plain,
! [X2,X0,X1] : meet(X1,complement(join(X2,X0))) = meet(complement(X0),meet(X1,complement(join(X2,X0)))),
inference(forward_demodulation,[],[f91414,f83]) ).
fof(f91566,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f91469,f3776]) ).
fof(f91567,plain,
! [X2,X0,X1] : complement(X0) = join(complement(X0),meet(X1,complement(join(X2,X0)))),
inference(forward_demodulation,[],[f91472,f6]) ).
fof(f91809,plain,
! [X2,X0,X1] : join(X2,X0) = meet(join(X2,X0),join(X2,complement(meet(complement(X0),X1)))),
inference(superposition,[],[f119,f80792]) ).
fof(f105574,plain,
! [X2,X0,X1] : meet(X1,X2) = meet(X1,meet(X2,complement(meet(X0,complement(meet(X1,X2)))))),
inference(superposition,[],[f84,f81153]) ).
fof(f112132,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,join(X1,complement(join(X0,X1))))),
inference(superposition,[],[f2770,f78977]) ).
fof(f112329,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f112132,f7]) ).
fof(f127079,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,meet(complement(join(X1,X0)),complement(join(X0,X1)))),
inference(superposition,[],[f4274,f88523]) ).
fof(f127255,plain,
! [X2,X0,X1] : meet(X2,complement(join(X1,X0))) = meet(X2,complement(join(X0,X1))),
inference(forward_demodulation,[],[f127079,f88523]) ).
fof(f128961,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f80086,f127255]) ).
fof(f130333,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f128961,f3776]) ).
fof(f153472,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),complement(meet(complement(X0),complement(X1)))),
inference(superposition,[],[f91809,f81153]) ).
fof(f154435,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(X1),meet(complement(X0),complement(join(X0,X1)))),
inference(superposition,[],[f105574,f153472]) ).
fof(f154690,plain,
! [X0,X1] : meet(complement(X0),complement(join(X0,X1))) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f154435,f91501]) ).
fof(f154863,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f154690,f79903]) ).
fof(f155411,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(X1,complement(X0))),
inference(superposition,[],[f154863,f3776]) ).
fof(f155418,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(superposition,[],[f154863,f3776]) ).
fof(f156291,plain,
! [X2,X0,X1] : meet(complement(X2),join(complement(X1),X0)) = complement(join(meet(complement(X0),X1),X2)),
inference(superposition,[],[f155418,f155418]) ).
fof(f156332,plain,
! [X2,X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(meet(complement(X0),X2),X1)),X0),
inference(superposition,[],[f155418,f110]) ).
fof(f156340,plain,
! [X2,X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(X1,meet(X2,complement(X0)))),X0),
inference(superposition,[],[f155418,f507]) ).
fof(f156560,plain,
! [X2,X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(X1,meet(X2,complement(X0))))),
inference(forward_demodulation,[],[f156340,f5]) ).
fof(f156566,plain,
! [X2,X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(meet(complement(X0),X2),X1))),
inference(forward_demodulation,[],[f156332,f5]) ).
fof(f156677,plain,
! [X2,X0,X1] : meet(complement(X1),X0) = meet(X0,complement(join(X1,meet(X2,complement(X0))))),
inference(forward_demodulation,[],[f156560,f155418]) ).
fof(f156680,plain,
! [X2,X0,X1] : complement(join(complement(X0),X1)) = meet(X0,meet(complement(X1),join(complement(X2),X0))),
inference(forward_demodulation,[],[f156566,f156291]) ).
fof(f156750,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(forward_demodulation,[],[f156680,f680]) ).
fof(f156821,plain,
! [X2,X0,X1] : meet(join(X1,complement(X0)),complement(X2)) = complement(join(X2,meet(X0,complement(X1)))),
inference(superposition,[],[f155411,f155411]) ).
fof(f156924,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f3776,f155411]) ).
fof(f157354,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f3776,f156750]) ).
fof(f157688,plain,
! [X2,X0,X1] : complement(meet(X2,join(complement(X0),X1))) = join(complement(X2),meet(X0,complement(X1))),
inference(superposition,[],[f157354,f157354]) ).
fof(f157694,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X1),complement(X0)),
inference(superposition,[],[f157354,f3776]) ).
fof(f158160,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(superposition,[],[f157694,f3776]) ).
fof(f159026,plain,
! [X0,X1] : complement(meet(complement(X0),complement(X1))) = join(X0,complement(complement(meet(X1,join(complement(X1),complement(X0)))))),
inference(superposition,[],[f158160,f25965]) ).
fof(f159261,plain,
! [X0,X1] : complement(meet(complement(X0),complement(X1))) = join(X0,meet(X1,join(complement(X1),complement(X0)))),
inference(forward_demodulation,[],[f159026,f3776]) ).
fof(f159442,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X1,X0)))) = complement(meet(complement(X0),complement(X1))),
inference(forward_demodulation,[],[f159261,f157694]) ).
fof(f159580,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X1,X0)))) = join(X1,complement(complement(X0))),
inference(forward_demodulation,[],[f159442,f156924]) ).
fof(f159685,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f159580,f3776]) ).
fof(f160272,plain,
! [X0,X1] :
( zero != meet(meet(X0,complement(meet(X0,X1))),join(X1,complement(join(X0,X1))))
| join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(superposition,[],[f873,f159685]) ).
fof(f160479,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1)))))
| join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f160272,f7]) ).
fof(f160761,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X0,X1))))
| join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f160479,f112329]) ).
fof(f160976,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f160761,f205]) ).
fof(f161136,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(meet(X0,X1),complement(X0)),
inference(forward_demodulation,[],[f160976,f156924]) ).
fof(f161249,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f161136,f6]) ).
fof(f161767,plain,
! [X0,X1] : join(complement(X1),meet(X1,complement(join(X0,X1)))) = join(complement(join(X0,X1)),complement(join(complement(X0),meet(X0,X1)))),
inference(superposition,[],[f161249,f161249]) ).
fof(f161979,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(complement(complement(join(X0,X1))),join(complement(join(X0,X1)),complement(join(complement(X0),meet(X0,X1))))),
inference(superposition,[],[f91566,f161249]) ).
fof(f162021,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,complement(X1)))) = meet(X1,complement(join(complement(X0),meet(X0,complement(X1))))),
inference(superposition,[],[f80018,f161249]) ).
fof(f162040,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(join(X1,X0))))) = X1,
inference(superposition,[],[f79698,f161249]) ).
fof(f162043,plain,
! [X0,X1] : meet(X1,complement(join(X0,complement(join(X1,X0))))) = complement(join(meet(X1,X0),complement(X1))),
inference(superposition,[],[f130333,f161249]) ).
fof(f162065,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(complement(X1),join(X0,complement(join(X1,X0)))),
inference(superposition,[],[f51,f161249]) ).
fof(f162100,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),join(complement(X1),complement(join(X0,complement(join(X1,X0))))))
| meet(X1,X0) = complement(join(complement(X1),complement(join(X0,complement(join(X1,X0)))))) ),
inference(superposition,[],[f3772,f161249]) ).
fof(f162115,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(join(X1,X0)))) = join(join(meet(X1,X0),complement(X1)),X2),
inference(superposition,[],[f9172,f161249]) ).
fof(f162206,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(join(X1,X0)))) = join(meet(X1,X0),join(complement(X1),X2)),
inference(forward_demodulation,[],[f162115,f8]) ).
fof(f162220,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(complement(X1),complement(join(X0,complement(join(X1,X0)))))))
| meet(X1,X0) = complement(join(complement(X1),complement(join(X0,complement(join(X1,X0)))))) ),
inference(forward_demodulation,[],[f162100,f7]) ).
fof(f162246,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f162065,f79817]) ).
fof(f162264,plain,
! [X0,X1] : complement(join(complement(X1),meet(X1,X0))) = meet(X1,complement(join(X0,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f162043,f15496]) ).
fof(f162267,plain,
! [X0,X1] : join(X1,meet(join(X1,X0),complement(X0))) = X1,
inference(forward_demodulation,[],[f162040,f155411]) ).
fof(f162277,plain,
! [X0,X1] : meet(complement(complement(X0)),X1) = complement(join(complement(X0),meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f162021,f156677]) ).
fof(f162308,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(complement(complement(join(X0,X1))),complement(meet(join(X0,X1),join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f161979,f157694]) ).
fof(f162457,plain,
! [X0,X1] : join(complement(X1),meet(X1,complement(join(X0,X1)))) = complement(meet(join(X0,X1),join(complement(X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f161767,f157694]) ).
fof(f162537,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(join(X1,X0)))) = join(complement(X1),join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f162206,f121]) ).
fof(f162548,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X1,join(X0,complement(join(X1,X0)))))))
| meet(X1,X0) = complement(join(complement(X1),complement(join(X0,complement(join(X1,X0)))))) ),
inference(forward_demodulation,[],[f162220,f157694]) ).
fof(f162582,plain,
! [X0,X1] : complement(join(complement(X1),meet(X1,X0))) = meet(X1,meet(join(X1,X0),complement(X0))),
inference(forward_demodulation,[],[f162264,f155411]) ).
fof(f162585,plain,
! [X0,X1] : join(X1,meet(complement(X0),join(X1,X0))) = X1,
inference(forward_demodulation,[],[f162267,f9269]) ).
fof(f162593,plain,
! [X0,X1] : meet(complement(complement(X0)),X1) = meet(join(X1,complement(X0)),complement(complement(X0))),
inference(forward_demodulation,[],[f162277,f156821]) ).
fof(f162618,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = complement(join(meet(join(X0,X1),join(complement(X0),meet(X0,X1))),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f162308,f154863]) ).
fof(f162739,plain,
! [X0,X1] : join(complement(X1),meet(X1,complement(join(X0,X1)))) = join(complement(join(X0,X1)),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f162457,f157688]) ).
fof(f162812,plain,
! [X2,X0,X1] : join(X2,join(complement(X1),X0)) = join(complement(X1),join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f162537,f162246]) ).
fof(f162821,plain,
! [X0,X1] : meet(X1,X0) = complement(join(complement(X1),complement(join(X0,complement(join(X1,X0)))))),
inference(forward_subsumption_resolution,[],[f162548,f62739]) ).
fof(f162845,plain,
! [X0,X1] : complement(join(complement(X1),meet(X1,X0))) = meet(X1,meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f162582,f4274]) ).
fof(f162848,plain,
! [X0,X1] : meet(join(X0,X1),join(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f162585,f82371]) ).
fof(f162855,plain,
! [X0,X1] : meet(complement(complement(X0)),X1) = meet(complement(complement(X0)),join(X1,complement(X0))),
inference(forward_demodulation,[],[f162593,f5]) ).
fof(f162879,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = complement(join(complement(join(X0,X1)),meet(join(X0,X1),join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f162618,f15496]) ).
fof(f162980,plain,
! [X0,X1] : complement(X1) = join(complement(join(X0,X1)),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f162739,f91567]) ).
fof(f163046,plain,
! [X0,X1] : meet(X1,X0) = meet(join(X0,complement(join(X1,X0))),complement(complement(X1))),
inference(forward_demodulation,[],[f162821,f155411]) ).
fof(f163063,plain,
! [X0,X1] : meet(X1,complement(X0)) = complement(join(complement(X1),meet(X1,X0))),
inference(forward_demodulation,[],[f162845,f164]) ).
fof(f163071,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f162855,f3776]) ).
fof(f163088,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(complement(meet(join(X0,X1),join(complement(X0),meet(X0,X1)))),join(X0,X1)),
inference(forward_demodulation,[],[f162879,f155418]) ).
fof(f163211,plain,
! [X0,X1] : meet(X1,X0) = meet(complement(complement(X1)),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f163046,f5]) ).
fof(f163224,plain,
! [X0,X1] : meet(complement(meet(X1,X0)),X1) = meet(X1,complement(X0)),
inference(forward_demodulation,[],[f163063,f155418]) ).
fof(f163238,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(join(X1,X0),complement(meet(join(X0,X1),join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f163088,f8484]) ).
fof(f163319,plain,
! [X0,X1] : meet(X1,X0) = meet(complement(complement(X1)),join(complement(X1),X0)),
inference(forward_demodulation,[],[f163211,f162246]) ).
fof(f163330,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(X1,complement(X0)),
inference(forward_demodulation,[],[f163224,f5]) ).
fof(f163343,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(join(X1,X0),join(complement(join(X0,X1)),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f163238,f157688]) ).
fof(f163399,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(complement(X1),X0)),
inference(forward_demodulation,[],[f163319,f3776]) ).
fof(f163418,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(join(X1,X0),complement(X1)),
inference(forward_demodulation,[],[f163343,f162980]) ).
fof(f163473,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f163418,f5]) ).
fof(f163520,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f163473,f155418]) ).
fof(f163554,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f163520,f5]) ).
fof(f163578,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f163554,f163330]) ).
fof(f165300,plain,
! [X0,X1] : meet(complement(complement(X0)),complement(meet(X0,X1))) = meet(complement(X1),complement(complement(X0))),
inference(superposition,[],[f163578,f157694]) ).
fof(f165721,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(complement(X0)),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f165300,f154863]) ).
fof(f165937,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = complement(join(meet(X0,X1),complement(X0))),
inference(forward_demodulation,[],[f165721,f154863]) ).
fof(f166107,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = complement(join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f165937,f15496]) ).
fof(f166218,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = complement(join(complement(X0),X1)),
inference(forward_demodulation,[],[f166107,f155418]) ).
fof(f166297,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(meet(X0,X1)),X0),
inference(forward_demodulation,[],[f166218,f155418]) ).
fof(f166353,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f166297,f5]) ).
fof(f167481,plain,
! [X0,X1] : meet(join(complement(X0),X1),complement(complement(X0))) = meet(complement(complement(meet(X0,join(complement(X0),X1)))),join(complement(X0),X1)),
inference(superposition,[],[f166353,f22003]) ).
fof(f167919,plain,
! [X0,X1] : meet(join(complement(X0),X1),complement(complement(X0))) = meet(join(X1,complement(X0)),complement(complement(meet(X0,join(complement(X0),X1))))),
inference(forward_demodulation,[],[f167481,f8484]) ).
fof(f168181,plain,
! [X0,X1] : meet(join(complement(X0),X1),complement(complement(X0))) = meet(join(X1,complement(X0)),meet(X0,join(complement(X0),X1))),
inference(forward_demodulation,[],[f167919,f3776]) ).
fof(f168379,plain,
! [X0,X1] : meet(join(complement(X0),X1),complement(complement(X0))) = meet(X0,meet(join(X1,complement(X0)),join(X1,complement(X0)))),
inference(forward_demodulation,[],[f168181,f8754]) ).
fof(f168518,plain,
! [X0,X1] : meet(X0,join(X1,complement(X0))) = meet(join(complement(X0),X1),complement(complement(X0))),
inference(forward_demodulation,[],[f168379,f1]) ).
fof(f168614,plain,
! [X0,X1] : meet(X0,join(X1,complement(X0))) = meet(complement(complement(X0)),join(complement(X0),X1)),
inference(forward_demodulation,[],[f168518,f5]) ).
fof(f168673,plain,
! [X0,X1] : meet(X0,join(X1,complement(X0))) = meet(X1,complement(complement(X0))),
inference(forward_demodulation,[],[f168614,f163578]) ).
fof(f168719,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f168673,f3776]) ).
fof(f170673,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(join(X1,meet(X0,X2)),complement(X0))),
inference(superposition,[],[f162848,f135]) ).
fof(f170814,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),join(X0,meet(X2,join(join(X1,X0),join(X0,complement(X1))))))))),
inference(superposition,[],[f125,f162848]) ).
fof(f171107,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),join(X0,meet(X2,join(complement(X1),join(join(X1,X0),X0)))))))),
inference(forward_demodulation,[],[f170814,f8650]) ).
fof(f171202,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(complement(X0),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f170673,f8486]) ).
fof(f171328,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),join(X0,meet(X2,join(complement(X1),join(X0,join(X1,X0))))))))),
inference(forward_demodulation,[],[f171107,f11300]) ).
fof(f171394,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X1,join(complement(X0),X2))),
inference(forward_demodulation,[],[f171202,f162812]) ).
fof(f171481,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),join(X0,meet(X2,join(X1,join(X0,join(complement(X1),X0))))))))),
inference(forward_demodulation,[],[f171328,f616]) ).
fof(f171583,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = join(X0,meet(X1,meet(join(X1,X0),join(X0,meet(X2,join(X1,join(X0,join(complement(X1),X0)))))))),
inference(forward_demodulation,[],[f171481,f171394]) ).
fof(f171650,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X0,meet(X2,join(X1,join(X0,join(complement(X1),X0))))),join(X0,meet(X1,join(X1,X0)))),
inference(forward_demodulation,[],[f171583,f90232]) ).
fof(f171694,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X0,meet(join(X1,X0),X1)),join(X0,meet(X2,join(X1,join(X0,join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f171650,f14037]) ).
fof(f171728,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X0,meet(X1,join(X1,X0))),join(X0,meet(X2,join(X1,join(X0,join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f171694,f14480]) ).
fof(f171751,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X0,meet(X1,join(X1,X0))),join(X0,meet(X2,one))),
inference(forward_demodulation,[],[f171728,f1895]) ).
fof(f171770,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X0,meet(X1,join(X1,X0))),join(X0,X2)),
inference(forward_demodulation,[],[f171751,f190]) ).
fof(f171788,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(meet(join(X1,X0),join(X0,X1)),join(X0,X2)),
inference(forward_demodulation,[],[f171770,f82489]) ).
fof(f171804,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))) = meet(join(X1,X0),meet(join(X0,X1),join(X0,X2))),
inference(forward_demodulation,[],[f171788,f7]) ).
fof(f171818,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X1,X0)) = meet(join(X1,X0),join(X0,join(complement(X1),meet(join(X1,X0),X2)))),
inference(forward_demodulation,[],[f171804,f8458]) ).
fof(f171831,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X1,X0)) = join(X0,meet(X1,meet(join(X1,X0),X2))),
inference(forward_demodulation,[],[f171818,f171394]) ).
fof(f171841,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X1,X0)) = meet(join(X1,X0),join(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f171831,f82394]) ).
fof(f171849,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X1,X0)) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f171841,f5044]) ).
fof(f171917,plain,
! [X2,X3,X0,X1] : join(X1,meet(join(X2,X0),X3)) = meet(join(X0,join(X1,X2)),join(X3,X1)),
inference(superposition,[],[f171849,f121]) ).
fof(f172060,plain,
! [X2,X3,X0,X1] : meet(join(X1,X3),join(X0,join(X1,X2))) = join(X1,meet(X3,join(X0,X2))),
inference(superposition,[],[f171849,f3669]) ).
fof(f172131,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(join(X2,X0),X1),
inference(superposition,[],[f416,f171849]) ).
fof(f172157,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f8486,f171849]) ).
fof(f172170,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(meet(join(X0,X1),X0),X2)) = join(X0,meet(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f84366,f171849]) ).
fof(f172488,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,meet(X2,X1))) = meet(join(X0,X1),join(meet(join(X0,X1),X0),X2)),
inference(forward_demodulation,[],[f172170,f90233]) ).
fof(f172838,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,meet(join(X0,X1),X2))) = meet(join(X0,X1),join(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f172488,f91128]) ).
fof(f173095,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,meet(join(X0,X1),X2))) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f172838,f16562]) ).
fof(f173286,plain,
! [X2,X0,X1] : meet(join(X2,X0),join(X0,X1)) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f173095,f172131]) ).
fof(f174316,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),join(join(X0,meet(X1,X2)),meet(X3,join(join(X1,X0),join(X0,X2))))))),
inference(superposition,[],[f12,f173286]) ).
fof(f174627,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = meet(join(join(join(X0,meet(X1,X2)),meet(X3,join(join(X1,X0),join(X0,X2)))),join(X0,X2)),join(X1,X0)),
inference(forward_demodulation,[],[f174316,f172131]) ).
fof(f175006,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = meet(join(X0,X1),join(join(join(X0,meet(X1,X2)),meet(X3,join(join(X1,X0),join(X0,X2)))),join(X0,X2))),
inference(forward_demodulation,[],[f174627,f8484]) ).
fof(f175285,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = meet(join(X0,X1),join(X2,join(join(join(X0,meet(X1,X2)),meet(X3,join(join(X1,X0),join(X0,X2)))),X0))),
inference(forward_demodulation,[],[f175006,f8650]) ).
fof(f175490,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = meet(join(X0,X1),join(X2,join(X0,join(join(X0,meet(X1,X2)),meet(X3,join(join(X1,X0),join(X0,X2))))))),
inference(forward_demodulation,[],[f175285,f11300]) ).
fof(f175639,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,join(X2,join(join(X0,meet(X1,X2)),meet(X3,join(join(X1,X0),join(X0,X2))))))),
inference(forward_demodulation,[],[f175490,f172060]) ).
fof(f175751,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,join(X2,join(X0,join(meet(X1,X2),meet(X3,join(join(X1,X0),join(X0,X2)))))))),
inference(forward_demodulation,[],[f175639,f8]) ).
fof(f175839,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,join(X2,join(meet(X3,join(join(X1,X0),join(X0,X2))),X0)))),
inference(forward_demodulation,[],[f175751,f601]) ).
fof(f175915,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,join(X2,join(X0,meet(X3,join(join(X1,X0),join(X0,X2))))))),
inference(forward_demodulation,[],[f175839,f11300]) ).
fof(f175978,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,join(X2,join(X0,meet(X3,join(X0,join(X2,join(X1,X0)))))))),
inference(forward_demodulation,[],[f175915,f8650]) ).
fof(f176022,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,join(X2,meet(join(join(X2,join(X1,X0)),X0),join(X0,X3))))),
inference(forward_demodulation,[],[f175978,f82371]) ).
fof(f176057,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,join(X2,meet(join(X0,join(X2,join(X1,X0))),join(X0,X3))))),
inference(forward_demodulation,[],[f176022,f14117]) ).
fof(f176088,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,meet(join(X0,join(X2,join(X1,X0))),join(X2,join(X0,X3))))),
inference(forward_demodulation,[],[f176057,f82341]) ).
fof(f176112,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = meet(join(X0,join(X2,join(X1,X0))),join(X0,meet(join(X2,join(X0,X3)),X1))),
inference(forward_demodulation,[],[f176088,f90233]) ).
fof(f176131,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(join(X2,join(X1,X0)),meet(join(X2,join(X0,X3)),X1))),
inference(forward_demodulation,[],[f176112,f172157]) ).
fof(f176149,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,meet(join(X2,join(X1,X0)),join(X2,join(X0,X3))))),
inference(forward_demodulation,[],[f176131,f9348]) ).
fof(f176166,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),meet(join(X1,X0),X3))) = join(X0,meet(X1,join(X2,join(X0,X3)))),
inference(forward_demodulation,[],[f176149,f600]) ).
fof(f176181,plain,
! [X2,X3,X0,X1] : meet(join(X3,join(X0,X2)),join(X1,X0)) = join(X0,meet(X1,join(X2,join(X0,X3)))),
inference(forward_demodulation,[],[f176166,f172131]) ).
fof(f176195,plain,
! [X2,X3,X0,X1] : join(X0,meet(join(X2,X3),X1)) = join(X0,meet(X1,join(X2,join(X0,X3)))),
inference(forward_demodulation,[],[f176181,f171917]) ).
fof(f183023,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f163399,f121]) ).
fof(f186922,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(X1,join(X0,join(complement(X1),meet(X1,join(meet(X0,X1),meet(X2,join(X1,join(X0,complement(X1))))))))),
inference(superposition,[],[f125,f168719]) ).
fof(f187294,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(X1,join(meet(X1,join(meet(X0,X1),meet(X2,join(X1,join(X0,complement(X1)))))),X0)),
inference(forward_demodulation,[],[f186922,f183023]) ).
fof(f187464,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(X1,join(X0,meet(X1,join(meet(X0,X1),meet(X2,join(X1,join(X0,complement(X1)))))))),
inference(forward_demodulation,[],[f187294,f8486]) ).
fof(f187569,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(join(join(meet(X0,X1),meet(X2,join(X1,join(X0,complement(X1))))),X0),X1),
inference(forward_demodulation,[],[f187464,f172131]) ).
fof(f187642,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(X1,join(join(meet(X0,X1),meet(X2,join(X1,join(X0,complement(X1))))),X0)),
inference(forward_demodulation,[],[f187569,f5]) ).
fof(f187700,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(X1,join(X0,join(meet(X0,X1),meet(X2,join(X1,join(X0,complement(X1))))))),
inference(forward_demodulation,[],[f187642,f8486]) ).
fof(f187747,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(X1,join(X0,meet(X2,join(X1,join(X0,complement(X1)))))),
inference(forward_demodulation,[],[f187700,f110]) ).
fof(f187787,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(X1,join(X0,meet(join(X1,complement(X1)),X2))),
inference(forward_demodulation,[],[f187747,f176195]) ).
fof(f187821,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),meet(X1,X2)))) = meet(X1,join(X0,meet(one,X2))),
inference(forward_demodulation,[],[f187787,f9]) ).
fof(f187850,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X0,join(complement(X1),meet(X1,X2)))),
inference(forward_demodulation,[],[f187821,f223]) ).
fof(f187873,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(meet(X1,X2),X0)),
inference(forward_demodulation,[],[f187850,f183023]) ).
fof(f188192,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,join(meet(X1,X2),X3))) = meet(X1,join(join(X3,X0),X2)),
inference(superposition,[],[f187873,f121]) ).
fof(f188799,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,join(meet(X1,X2),X3))) = meet(X1,join(X3,join(X0,X2))),
inference(forward_demodulation,[],[f188192,f8]) ).
fof(f208184,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(meet(X0,X2),join(X1,complement(X0)))),
inference(superposition,[],[f82291,f163071]) ).
fof(f208328,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(complement(X0),join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f208184,f8650]) ).
fof(f208528,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(X1,join(complement(X0),X2))),
inference(forward_demodulation,[],[f208328,f188799]) ).
fof(f208673,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f208528,f183023]) ).
fof(f209513,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(superposition,[],[f13,f208673]) ).
fof(f209746,plain,
$false,
inference(trivial_inequality_removal,[],[f209513]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT183-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n018.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 14:07:08 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 19.51/3.64 % (2379045)Input is clausal, will run a generic CNF schedule.
% 19.51/3.64 % (2379099)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2554019671:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 19.51/3.64 % (2379096)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3909633288:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 19.51/3.64 % (2379099)Instruction limit reached!
% 19.51/3.64 % (2379099)------------------------------
% 19.51/3.64 % (2379099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.64 % (2379099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.64 % (2379099)CaDiCaL version: 2.1.3
% 19.51/3.64 % (2379099)Termination reason: Instruction limit
% 19.51/3.64 % (2379099)Termination phase: Saturation
% 19.51/3.64 % (2379099)Time elapsed: 0.061 s
% 19.51/3.64 % (2379099)Peak memory usage: 89 MB
% 19.51/3.64 % (2379099)Instructions burned: 116 (million)
% 19.51/3.64 % (2379095)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3960417926:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 19.51/3.64 % (2379097)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3429711489:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 19.51/3.64 % (2379100)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1397982903:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 19.51/3.64 % (2379101)dis-21_1_sil=8000:lcm=predicate:random_seed=2583493490:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 19.51/3.64 % (2379098)lrs+10_1_sil=8000:sp=occurrence:random_seed=2451975330:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 19.51/3.64 % (2379101)Refutation not found, incomplete strategy
% 19.51/3.64 % (2379101)------------------------------
% 19.51/3.64 % (2379101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.64 % (2379101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.64 % (2379101)CaDiCaL version: 2.1.3
% 19.51/3.64 % (2379101)Termination reason: Refutation not found, incomplete strategy
% 19.51/3.64 % (2379101)Time elapsed: 0.003 s
% 19.51/3.64 % (2379101)Peak memory usage: 88 MB
% 19.51/3.64 % (2379101)Instructions burned: 1 (million)
% 19.51/3.64 % (2379098)Instruction limit reached!
% 19.51/3.64 % (2379098)------------------------------
% 19.51/3.64 % (2379098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.64 % (2379098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.64 % (2379098)CaDiCaL version: 2.1.3
% 19.51/3.64 % (2379098)Termination reason: Instruction limit
% 19.51/3.64 % (2379098)Termination phase: Saturation
% 19.51/3.64 % (2379098)Time elapsed: 0.105 s
% 19.51/3.64 % (2379098)Peak memory usage: 88 MB
% 19.51/3.64 % (2379098)Instructions burned: 108 (million)
% 19.51/3.64 % (2379100)Instruction limit reached!
% 19.51/3.64 % (2379100)------------------------------
% 19.51/3.64 % (2379100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.64 % (2379100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.64 % (2379100)CaDiCaL version: 2.1.3
% 19.51/3.64 % (2379100)Termination reason: Instruction limit
% 19.51/3.64 % (2379100)Termination phase: Saturation
% 19.51/3.64 % (2379100)Time elapsed: 0.145 s
% 19.51/3.64 % (2379100)Peak memory usage: 89 MB
% 19.51/3.64 % (2379100)Instructions burned: 180 (million)
% 19.51/3.64 % (2379109)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3975276406:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 19.51/3.64 % (2379109)Refutation not found, incomplete strategy
% 19.51/3.64 % (2379109)------------------------------
% 19.51/3.64 % (2379109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.51/3.64 % (2379109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.51/3.64 % (2379109)CaDiCaL version: 2.1.3
% 19.51/3.64 % (2379109)Termination reason: Refutation not found, incomplete strategy
% 19.51/3.64 % (2379109)Time elapsed: 0.001 s
% 19.51/3.64 % (2379109)Peak memory usage: 88 MB
% 19.51/3.64 % (2379115)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3934961937:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 33.70/5.61 % (2379115)Refutation not found, incomplete strategy
% 33.70/5.61 % (2379115)------------------------------
% 33.70/5.61 % (2379115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.70/5.61 % (2379115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.70/5.61 % (2379115)CaDiCaL version: 2.1.3
% 33.70/5.61 % (2379115)Termination reason: Refutation not found, incomplete strategy
% 33.70/5.61 % (2379115)Time elapsed: 0.003 s
% 33.70/5.61 % (2379115)Peak memory usage: 88 MB
% 33.70/5.61 % (2379115)Instructions burned: 1 (million)
% 33.70/5.61 % (2379101)------------------------------
% 33.70/5.61 % (2379101)------------------------------
% 33.70/5.61 % (2379117)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1237922279:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 33.70/5.61 % (2379117)Refutation not found, incomplete strategy
% 33.70/5.61 % (2379117)------------------------------
% 33.70/5.61 % (2379117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.70/5.61 % (2379117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.70/5.61 % (2379117)CaDiCaL version: 2.1.3
% 33.70/5.61 % (2379117)Termination reason: Refutation not found, incomplete strategy
% 33.70/5.61 % (2379117)Time elapsed: 0.001 s
% 33.70/5.61 % (2379117)Peak memory usage: 88 MB
% 33.70/5.61 % (2379109)------------------------------
% 33.70/5.61 % (2379109)------------------------------
% 33.70/5.61 % (2379129)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=906620064:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 33.70/5.61 % (2379125)lrs+10_64_to=lpo:sil=8000:random_seed=1838030209:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 33.70/5.61 % (2379115)------------------------------
% 33.70/5.61 % (2379115)------------------------------
% 33.70/5.61 % (2379129)Instruction limit reached!
% 33.70/5.61 % (2379129)------------------------------
% 33.70/5.61 % (2379129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.70/5.61 % (2379129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.70/5.61 % (2379129)CaDiCaL version: 2.1.3
% 33.70/5.61 % (2379129)Termination reason: Instruction limit
% 33.70/5.61 % (2379129)Termination phase: Saturation
% 33.70/5.61 % (2379129)Time elapsed: 0.104 s
% 33.70/5.61 % (2379129)Peak memory usage: 89 MB
% 33.70/5.61 % (2379129)Instructions burned: 195 (million)
% 33.70/5.61 % (2379125)Instruction limit reached!
% 33.70/5.61 % (2379125)------------------------------
% 33.70/5.61 % (2379125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.70/5.61 % (2379125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.70/5.61 % (2379125)CaDiCaL version: 2.1.3
% 33.70/5.61 % (2379125)Termination reason: Instruction limit
% 33.70/5.61 % (2379125)Termination phase: Saturation
% 33.70/5.61 % (2379125)Time elapsed: 0.117 s
% 33.70/5.61 % (2379125)Peak memory usage: 88 MB
% 33.70/5.61 % (2379125)Instructions burned: 127 (million)
% 33.70/5.61 % (2379117)------------------------------
% 33.70/5.61 % (2379117)------------------------------
% 33.70/5.61 % (2379133)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=928899983:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 33.70/5.62 % (2379132)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=284659227:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 33.70/5.62 % (2379134)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1923639067:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 33.70/5.62 % (2379135)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3249551527:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 33.70/5.62 % (2379135)Refutation not found, incomplete strategy
% 33.70/5.62 % (2379135)------------------------------
% 33.70/5.62 % (2379135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.70/5.62 % (2379135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.70/5.62 % (2379135)CaDiCaL version: 2.1.3
% 33.70/5.62 % (2379135)Termination reason: Refutation not found, incomplete strategy
% 33.70/5.62 % (2379135)Time elapsed: 0.002 s
% 49.85/7.95 % (2379135)Peak memory usage: 87 MB
% 49.85/7.95 % (2379134)Instruction limit reached!
% 49.85/7.95 % (2379134)------------------------------
% 49.85/7.95 % (2379134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.85/7.95 % (2379134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.85/7.95 % (2379134)CaDiCaL version: 2.1.3
% 49.85/7.95 % (2379134)Termination reason: Instruction limit
% 49.85/7.95 % (2379134)Termination phase: Saturation
% 49.85/7.95 % (2379134)Time elapsed: 0.110 s
% 49.85/7.95 % (2379134)Peak memory usage: 89 MB
% 49.85/7.95 % (2379134)Instructions burned: 106 (million)
% 49.85/7.95 % (2379132)Instruction limit reached!
% 49.85/7.95 % (2379132)------------------------------
% 49.85/7.95 % (2379132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.85/7.95 % (2379132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.85/7.95 % (2379132)CaDiCaL version: 2.1.3
% 49.85/7.95 % (2379132)Termination reason: Instruction limit
% 49.85/7.95 % (2379132)Termination phase: Saturation
% 49.85/7.95 % (2379132)Time elapsed: 0.158 s
% 49.85/7.95 % (2379132)Peak memory usage: 90 MB
% 49.85/7.95 % (2379132)Instructions burned: 157 (million)
% 49.85/7.95 % (2379145)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=529150130:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2985 on theBenchmark for (2985ds/242Mi)
% 49.85/7.95 % (2379135)------------------------------
% 49.85/7.95 % (2379135)------------------------------
% 49.85/7.95 % (2379147)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3260790495:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 49.85/7.95 % (2379145)Instruction limit reached!
% 49.85/7.95 % (2379145)------------------------------
% 49.85/7.95 % (2379145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.85/7.95 % (2379145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.85/7.95 % (2379145)CaDiCaL version: 2.1.3
% 49.85/7.95 % (2379145)Termination reason: Instruction limit
% 49.85/7.95 % (2379145)Termination phase: Saturation
% 49.85/7.95 % (2379145)Time elapsed: 0.242 s
% 49.85/7.95 % (2379145)Peak memory usage: 90 MB
% 49.85/7.95 % (2379145)Instructions burned: 242 (million)
% 49.85/7.95 % (2379152)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1244550906:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 49.85/7.95 % (2379152)Instruction limit reached!
% 49.85/7.95 % (2379152)------------------------------
% 49.85/7.95 % (2379152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.85/7.95 % (2379152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.85/7.95 % (2379152)CaDiCaL version: 2.1.3
% 49.85/7.95 % (2379152)Termination reason: Instruction limit
% 49.85/7.95 % (2379152)Termination phase: Saturation
% 49.85/7.95 % (2379152)Time elapsed: 0.127 s
% 49.85/7.95 % (2379152)Peak memory usage: 89 MB
% 49.85/7.95 % (2379152)Instructions burned: 135 (million)
% 49.85/7.95 % (2379153)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=536270593:i=499:bd=all_2980 on theBenchmark for (2980ds/499Mi)
% 49.85/7.95 % (2379157)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=306280895:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 49.85/7.95 % (2379157)Instruction limit reached!
% 49.85/7.95 % (2379157)------------------------------
% 49.85/7.95 % (2379157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.85/7.95 % (2379157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.85/7.95 % (2379157)CaDiCaL version: 2.1.3
% 49.85/7.95 % (2379157)Termination reason: Instruction limit
% 49.85/7.95 % (2379157)Termination phase: Saturation
% 49.85/7.95 % (2379157)Time elapsed: 0.190 s
% 49.85/7.95 % (2379157)Peak memory usage: 91 MB
% 49.85/7.95 % (2379157)Instructions burned: 191 (million)
% 49.85/7.95 % (2379153)Instruction limit reached!
% 49.85/7.95 % (2379153)------------------------------
% 49.85/7.95 % (2379153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.85/7.95 % (2379153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.85/7.95 % (2379153)CaDiCaL version: 2.1.3
% 49.85/7.95 % (2379153)Termination reason: Instruction limit
% 49.85/7.95 % (2379153)Termination phase: Saturation
% 49.85/7.95 % (2379153)Time elapsed: 0.516 s
% 49.85/7.95 % (2379153)Peak memory usage: 94 MB
% 49.85/7.95 % (2379153)Instructions burned: 500 (million)
% 88.30/13.39 % (2379160)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3536575027:i=264:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/264Mi)
% 88.30/13.39 % (2379161)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=308091568:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi)
% 88.30/13.39 % (2379133)Instruction limit reached!
% 88.30/13.39 % (2379133)------------------------------
% 88.30/13.39 % (2379133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.30/13.39 % (2379133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.30/13.39 % (2379133)CaDiCaL version: 2.1.3
% 88.30/13.39 % (2379133)Termination reason: Instruction limit
% 88.30/13.39 % (2379133)Termination phase: Saturation
% 88.30/13.39 % (2379133)Time elapsed: 1.910 s
% 88.30/13.39 % (2379133)Peak memory usage: 149 MB
% 88.30/13.39 % (2379133)Instructions burned: 3395 (million)
% 88.30/13.39 % (2379161)Instruction limit reached!
% 88.30/13.39 % (2379161)------------------------------
% 88.30/13.39 % (2379161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.30/13.39 % (2379161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.30/13.39 % (2379161)CaDiCaL version: 2.1.3
% 88.30/13.39 % (2379161)Termination reason: Instruction limit
% 88.30/13.39 % (2379161)Termination phase: Saturation
% 88.30/13.39 % (2379161)Time elapsed: 0.158 s
% 88.30/13.39 % (2379161)Peak memory usage: 89 MB
% 88.30/13.39 % (2379161)Instructions burned: 156 (million)
% 88.30/13.39 % (2379160)Instruction limit reached!
% 88.30/13.39 % (2379160)------------------------------
% 88.30/13.39 % (2379160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.30/13.39 % (2379160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.30/13.39 % (2379160)CaDiCaL version: 2.1.3
% 88.30/13.39 % (2379160)Termination reason: Instruction limit
% 88.30/13.39 % (2379160)Termination phase: Saturation
% 88.30/13.39 % (2379160)Time elapsed: 0.250 s
% 88.30/13.39 % (2379160)Peak memory usage: 92 MB
% 88.30/13.39 % (2379160)Instructions burned: 264 (million)
% 88.30/13.39 % (2379164)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1659074355:i=3256:kws=precedence:bd=preordered:av=off_2968 on theBenchmark for (2968ds/3256Mi)
% 88.30/13.39 % (2379166)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1280686453:i=180:bd=preordered:av=off_2967 on theBenchmark for (2967ds/180Mi)
% 88.30/13.39 % (2379165)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=950957744:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi)
% 88.30/13.39 % (2379166)Instruction limit reached!
% 88.30/13.39 % (2379166)------------------------------
% 88.30/13.39 % (2379166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.30/13.39 % (2379166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.30/13.39 % (2379166)CaDiCaL version: 2.1.3
% 88.30/13.39 % (2379166)Termination reason: Instruction limit
% 88.30/13.39 % (2379166)Termination phase: Saturation
% 88.30/13.39 % (2379166)Time elapsed: 0.170 s
% 88.30/13.39 % (2379166)Peak memory usage: 88 MB
% 88.30/13.39 % (2379166)Instructions burned: 180 (million)
% 88.30/13.39 % (2379172)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3378790978:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2963 on theBenchmark for (2963ds/10307Mi)
% 88.30/13.39 % (2379165)Instruction limit reached!
% 88.30/13.39 % (2379165)------------------------------
% 88.30/13.39 % (2379165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.30/13.39 % (2379165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.30/13.39 % (2379165)CaDiCaL version: 2.1.3
% 88.30/13.39 % (2379165)Termination reason: Instruction limit
% 88.30/13.39 % (2379165)Termination phase: Saturation
% 88.30/13.39 % (2379165)Time elapsed: 0.512 s
% 88.30/13.39 % (2379165)Peak memory usage: 93 MB
% 88.30/13.39 % (2379165)Instructions burned: 538 (million)
% 88.30/13.39 % (2379174)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=1387425472:i=412:gtgl=4:gtg=exists_all_2960 on theBenchmark for (2960ds/412Mi)
% 88.30/13.39 % (2379174)Instruction limit reached!
% 88.30/13.39 % (2379174)------------------------------
% 88.30/13.39 % (2379174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.48/17.49 % (2379174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.49 % (2379174)CaDiCaL version: 2.1.3
% 117.48/17.49 % (2379174)Termination reason: Instruction limit
% 117.48/17.49 % (2379174)Termination phase: Saturation
% 117.48/17.49 % (2379174)Time elapsed: 0.412 s
% 117.48/17.49 % (2379174)Peak memory usage: 94 MB
% 117.48/17.49 % (2379174)Instructions burned: 412 (million)
% 117.48/17.49 % (2379176)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=245884908:s2pl=no:i=8478:s2at=4:nm=6_2952 on theBenchmark for (2952ds/8478Mi)
% 117.48/17.49 % (2379164)Instruction limit reached!
% 117.48/17.49 % (2379164)------------------------------
% 117.48/17.49 % (2379164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.48/17.49 % (2379164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.49 % (2379164)CaDiCaL version: 2.1.3
% 117.48/17.49 % (2379164)Termination reason: Instruction limit
% 117.48/17.49 % (2379164)Termination phase: Saturation
% 117.48/17.49 % (2379164)Time elapsed: 1.864 s
% 117.48/17.49 % (2379164)Peak memory usage: 148 MB
% 117.48/17.49 % (2379164)Instructions burned: 3256 (million)
% 117.48/17.49 % (2379178)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2719337993:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2947 on theBenchmark for (2947ds/303Mi)
% 117.48/17.49 % (2379178)Refutation not found, incomplete strategy
% 117.48/17.49 % (2379178)------------------------------
% 117.48/17.49 % (2379178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.48/17.49 % (2379178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.49 % (2379178)CaDiCaL version: 2.1.3
% 117.48/17.49 % (2379178)Termination reason: Refutation not found, incomplete strategy
% 117.48/17.49 % (2379178)Time elapsed: 0.001 s
% 117.48/17.49 % (2379178)Peak memory usage: 88 MB
% 117.48/17.49 % (2379178)Instructions burned: 1 (million)
% 117.48/17.49 % (2379178)------------------------------
% 117.48/17.49 % (2379178)------------------------------
% 117.48/17.49 % (2379180)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1980756338:st=4:i=720:sd=3:fsr=off:ss=axioms_2942 on theBenchmark for (2942ds/720Mi)
% 117.48/17.49 % (2379180)Refutation not found, incomplete strategy
% 117.48/17.49 % (2379180)------------------------------
% 117.48/17.49 % (2379180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.48/17.49 % (2379180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.49 % (2379180)CaDiCaL version: 2.1.3
% 117.48/17.49 % (2379180)Termination reason: Refutation not found, incomplete strategy
% 117.48/17.49 % (2379180)Time elapsed: 0.001 s
% 117.48/17.49 % (2379180)Peak memory usage: 88 MB
% 117.48/17.49 % (2379180)------------------------------
% 117.48/17.49 % (2379180)------------------------------
% 117.48/17.49 % (2379184)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1129537504:i=598:bs=on:bd=preordered:av=off:ss=axioms_2938 on theBenchmark for (2938ds/598Mi)
% 117.48/17.49 % (2379184)Instruction limit reached!
% 117.48/17.49 % (2379184)------------------------------
% 117.48/17.49 % (2379184)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.48/17.49 % (2379184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.49 % (2379184)CaDiCaL version: 2.1.3
% 117.48/17.49 % (2379184)Termination reason: Instruction limit
% 117.48/17.49 % (2379184)Termination phase: Saturation
% 117.48/17.49 % (2379184)Time elapsed: 0.333 s
% 117.48/17.49 % (2379184)Peak memory usage: 95 MB
% 117.48/17.49 % (2379184)Instructions burned: 598 (million)
% 117.48/17.49 % (2379186)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4251645470:i=2989:sd=3:ss=axioms:sgt=60_2932 on theBenchmark for (2932ds/2989Mi)
% 117.48/17.49 % (2379147)Instruction limit reached!
% 117.48/17.49 % (2379147)------------------------------
% 117.48/17.49 % (2379147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 117.48/17.49 % (2379147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.48/17.49 % (2379147)CaDiCaL version: 2.1.3
% 117.48/17.49 % (2379147)Termination reason: Instruction limit
% 117.48/17.49 % (2379147)Termination phase: Saturation
% 117.48/17.49 % (2379147)Time elapsed: 5.280 s
% 117.48/17.49 % (2379147)Peak memory usage: 167 MB
% 104.62/18.10 % (2379147)Instructions burned: 5209 (million)
% 104.62/18.10 % (2379188)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1988749888:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2929 on theBenchmark for (2929ds/1997Mi)
% 104.62/18.10 % (2379186)Instruction limit reached!
% 104.62/18.10 % (2379186)------------------------------
% 104.62/18.10 % (2379186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379186)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379186)Termination reason: Instruction limit
% 104.62/18.10 % (2379186)Termination phase: Saturation
% 104.62/18.10 % (2379186)Time elapsed: 1.647 s
% 104.62/18.10 % (2379186)Peak memory usage: 147 MB
% 104.62/18.10 % (2379186)Instructions burned: 2991 (million)
% 104.62/18.10 % (2379198)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=713318883:i=2088:bd=preordered:av=off_2913 on theBenchmark for (2913ds/2088Mi)
% 104.62/18.10 % (2379188)Instruction limit reached!
% 104.62/18.10 % (2379188)------------------------------
% 104.62/18.10 % (2379188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379188)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379188)Termination reason: Instruction limit
% 104.62/18.10 % (2379188)Termination phase: Saturation
% 104.62/18.10 % (2379188)Time elapsed: 1.689 s
% 104.62/18.10 % (2379188)Peak memory usage: 138 MB
% 104.62/18.10 % (2379188)Instructions burned: 1998 (million)
% 104.62/18.10 % (2379200)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2568489023:i=1098:nicw=on_2909 on theBenchmark for (2909ds/1098Mi)
% 104.62/18.10 % (2379200)Instruction limit reached!
% 104.62/18.10 % (2379200)------------------------------
% 104.62/18.10 % (2379200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379200)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379200)Termination reason: Instruction limit
% 104.62/18.10 % (2379200)Termination phase: Saturation
% 104.62/18.10 % (2379200)Time elapsed: 0.584 s
% 104.62/18.10 % (2379200)Peak memory usage: 101 MB
% 104.62/18.10 % (2379200)Instructions burned: 1098 (million)
% 104.62/18.10 % (2379202)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3313320406:i=433:bd=preordered_2901 on theBenchmark for (2901ds/433Mi)
% 104.62/18.10 % (2379202)Refutation not found, incomplete strategy
% 104.62/18.10 % (2379202)------------------------------
% 104.62/18.10 % (2379202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379202)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379202)Termination reason: Refutation not found, incomplete strategy
% 104.62/18.10 % (2379202)Time elapsed: 0.002 s
% 104.62/18.10 % (2379202)Peak memory usage: 88 MB
% 104.62/18.10 % (2379202)Instructions burned: 1 (million)
% 104.62/18.10 % (2379202)------------------------------
% 104.62/18.10 % (2379202)------------------------------
% 104.62/18.10 % (2379204)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2623962151:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2896 on theBenchmark for (2896ds/2942Mi)
% 104.62/18.10 % (2379198)Instruction limit reached!
% 104.62/18.10 % (2379198)------------------------------
% 104.62/18.10 % (2379198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379198)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379198)Termination reason: Instruction limit
% 104.62/18.10 % (2379198)Termination phase: Saturation
% 104.62/18.10 % (2379198)Time elapsed: 2.161 s
% 104.62/18.10 % (2379198)Peak memory usage: 139 MB
% 104.62/18.10 % (2379198)Instructions burned: 2088 (million)
% 104.62/18.10 % (2379208)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3228802502:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2888 on theBenchmark for (2888ds/6922Mi)
% 104.62/18.10 % (2379204)Instruction limit reached!
% 104.62/18.10 % (2379204)------------------------------
% 104.62/18.10 % (2379204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379204)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379204)Termination reason: Instruction limit
% 104.62/18.10 % (2379204)Termination phase: Saturation
% 104.62/18.10 % (2379204)Time elapsed: 1.923 s
% 104.62/18.10 % (2379204)Peak memory usage: 139 MB
% 104.62/18.10 % (2379204)Instructions burned: 2942 (million)
% 104.62/18.10 % (2379212)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1599253471:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2875 on theBenchmark for (2875ds/596Mi)
% 104.62/18.10 % (2379212)Refutation not found, incomplete strategy
% 104.62/18.10 % (2379212)------------------------------
% 104.62/18.10 % (2379212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379212)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379212)Termination reason: Refutation not found, incomplete strategy
% 104.62/18.10 % (2379212)Time elapsed: 0.001 s
% 104.62/18.10 % (2379212)Peak memory usage: 88 MB
% 104.62/18.10 % (2379212)Instructions burned: 1 (million)
% 104.62/18.10 % (2379212)------------------------------
% 104.62/18.10 % (2379212)------------------------------
% 104.62/18.10 % (2379216)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=63349851:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2870 on theBenchmark for (2870ds/4123Mi)
% 104.62/18.10 % (2379176)Instruction limit reached!
% 104.62/18.10 % (2379176)------------------------------
% 104.62/18.10 % (2379176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379176)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379176)Termination reason: Instruction limit
% 104.62/18.10 % (2379176)Termination phase: Saturation
% 104.62/18.10 % (2379176)Time elapsed: 9.298 s
% 104.62/18.10 % (2379176)Peak memory usage: 193 MB
% 104.62/18.10 % (2379176)Instructions burned: 8478 (million)
% 104.62/18.10 % (2379172)Instruction limit reached!
% 104.62/18.10 % (2379172)------------------------------
% 104.62/18.10 % (2379172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379172)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379172)Termination reason: Instruction limit
% 104.62/18.10 % (2379172)Termination phase: Saturation
% 104.62/18.10 % (2379172)Time elapsed: 10.563 s
% 104.62/18.10 % (2379172)Peak memory usage: 205 MB
% 104.62/18.10 % (2379172)Instructions burned: 10307 (million)
% 104.62/18.10 % (2379220)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=774977936:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2856 on theBenchmark for (2856ds/16411Mi)
% 104.62/18.10 % (2379221)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3816100986:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2854 on theBenchmark for (2854ds/1670Mi)
% 104.62/18.10 % (2379216)Instruction limit reached!
% 104.62/18.10 % (2379216)------------------------------
% 104.62/18.10 % (2379216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379216)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379216)Termination reason: Instruction limit
% 104.62/18.10 % (2379216)Termination phase: Saturation
% 104.62/18.10 % (2379216)Time elapsed: 2.267 s
% 104.62/18.10 % (2379216)Peak memory usage: 161 MB
% 104.62/18.10 % (2379216)Instructions burned: 4124 (million)
% 104.62/18.10 % (2379225)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=3790887215:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2845 on theBenchmark for (2845ds/1722Mi)
% 104.62/18.10 % (2379225)Instruction limit reached!
% 104.62/18.10 % (2379225)------------------------------
% 104.62/18.10 % (2379225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379225)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379225)Termination reason: Instruction limit
% 104.62/18.10 % (2379225)Termination phase: Saturation
% 104.62/18.10 % (2379225)Time elapsed: 0.935 s
% 104.62/18.10 % (2379225)Peak memory usage: 134 MB
% 104.62/18.10 % (2379225)Instructions burned: 1722 (million)
% 104.62/18.10 % (2379221)Instruction limit reached!
% 104.62/18.10 % (2379221)------------------------------
% 104.62/18.10 % (2379221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 104.62/18.10 % (2379221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 104.62/18.10 % (2379221)CaDiCaL version: 2.1.3
% 104.62/18.10 % (2379221)Termination reason: Instruction limit
% 104.62/18.10 % (2379221)Termination phase: Saturation
% 104.62/18.10 % (2379221)Time elapsed: 1.761 s
% 104.62/18.10 % (2379221)Peak memory usage: 135 MB
% 104.62/18.10 % (2379221)Instructions burned: 1670 (million)
% 104.62/18.10 % (2379096)First to succeed.
% 104.62/18.10 % (2379096)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2379045"
% 104.62/18.10 % (2379227)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3267606337:cts=off:cond=on:i=9530:bs=on:fsd=on_2834 on theBenchmark for (2834ds/9530Mi)
% 104.62/18.10 % (2379228)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2607902232:st=2:i=4495:sd=10:ss=included_2833 on theBenchmark for (2833ds/4495Mi)
% 104.62/18.10 % (2379096)Refutation found. Thanks to Tanya!
% 104.62/18.10 % SZS status Unsatisfiable for theBenchmark
% 104.62/18.10 % SZS output start Proof for theBenchmark
% See solution above
% 122.46/18.33 % (2379096)------------------------------
% 122.46/18.33 % (2379096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 122.46/18.33 % (2379096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 122.46/18.33 % (2379096)CaDiCaL version: 2.1.3
% 122.46/18.33 % (2379096)Termination reason: Refutation
% 122.46/18.33 % (2379096)Time elapsed: 16.515 s
% 122.46/18.33 % (2379096)Peak memory usage: 244 MB
% 122.46/18.33 % (2379096)Instructions burned: 16065 (million)
% 122.46/18.33 % (2379096)------------------------------
% 122.46/18.33 % (2379096)------------------------------
% 122.46/18.33 % (2379045)Success in time 17.193 s
% 122.46/18.33 % Vampire exiting
%------------------------------------------------------------------------------