%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT210-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 : n005.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:16 AM UTC 2026
% Result : Unsatisfiable 28.74s 5.09s
% Output : Refutation 29.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 11
% Syntax : Number of formulae : 239 ( 227 unt; 0 def)
% Number of atoms : 254 ( 253 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 32 ( 17 ~; 15 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 7 ( 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 : 546 ( 546 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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,X2)) = meet(X0,join(X1,meet(X0,join(X2,meet(X0,X1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H68) ).
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,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X0,meet(X1,join(X2,meet(X0,X1))))),
inference(superposition,[],[f12,f5]) ).
fof(f18,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(X0,join(meet(X0,X1),X2)))),
inference(superposition,[],[f12,f6]) ).
fof(f19,plain,
! [X2,X0,X1] : meet(X0,join(join(X2,meet(X0,X1)),X1)) = meet(X0,join(join(X2,meet(X0,X1)),meet(X0,join(X1,X2)))),
inference(superposition,[],[f12,f12]) ).
fof(f20,plain,
! [X2,X0,X1] : meet(X0,join(join(X2,meet(X0,X1)),X1)) = meet(X0,join(meet(X0,join(X1,X2)),join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f19,f6]) ).
fof(f22,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,join(X1,X2)),join(X2,meet(X0,X1)))) = meet(X0,join(X1,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f20,f6]) ).
fof(f25,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f33,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f53,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f25,f4]) ).
fof(f55,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f33,f25]) ).
fof(f59,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f55,f6]) ).
fof(f61,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f53,f5]) ).
fof(f68,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f25]) ).
fof(f69,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f102,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f103,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f33]) ).
fof(f112,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f115,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(X2,join(X0,X1)))),
inference(superposition,[],[f33,f8]) ).
fof(f127,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f102,f6]) ).
fof(f148,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f150,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f151,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f200,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f202,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(complement(X0),meet(X0,join(X1,zero)))),
inference(superposition,[],[f12,f10]) ).
fof(f204,plain,
! [X0] : complement(X0) = join(complement(X0),zero),
inference(superposition,[],[f33,f10]) ).
fof(f206,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f207,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f204,f6]) ).
fof(f216,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f69,f5]) ).
fof(f260,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f150]) ).
fof(f264,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f33,f150]) ).
fof(f314,plain,
! [X0,X1] : meet(one,join(X0,X1)) = join(X0,meet(one,join(X1,meet(one,X0)))),
inference(superposition,[],[f12,f260]) ).
fof(f319,plain,
zero = complement(one),
inference(superposition,[],[f10,f260]) ).
fof(f322,plain,
! [X0,X1] : meet(one,join(X0,X1)) = join(X0,join(X1,meet(one,X0))),
inference(forward_demodulation,[],[f314,f260]) ).
fof(f330,plain,
! [X0,X1] : join(X0,join(X1,X0)) = meet(one,join(X0,X1)),
inference(forward_demodulation,[],[f322,f260]) ).
fof(f334,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f330,f260]) ).
fof(f511,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f200]) ).
fof(f540,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f33,f511]) ).
fof(f900,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X2,join(X3,join(X0,X1))),
inference(superposition,[],[f112,f8]) ).
fof(f1238,plain,
! [X0,X1] : one = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f151,f6]) ).
fof(f1264,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,f151]) ).
fof(f1273,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1264]) ).
fof(f1312,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f1273,f6]) ).
fof(f1410,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f103,f6]) ).
fof(f1773,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f68,f10]) ).
fof(f1823,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f1773,f540]) ).
fof(f1923,plain,
! [X0,X1] :
( one != join(one,X0)
| zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(superposition,[],[f11,f148]) ).
fof(f1949,plain,
! [X0,X1] :
( zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(forward_subsumption_resolution,[],[f1923,f264]) ).
fof(f2457,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f25,f334]) ).
fof(f2805,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(join(X1,X0),meet(X2,X0)))) = meet(X2,join(meet(X2,join(X0,X1)),join(join(X1,X0),meet(X2,X0)))),
inference(superposition,[],[f22,f334]) ).
fof(f2991,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(join(X1,X0),meet(X2,X0)))) = meet(X2,join(meet(X2,X0),join(meet(X2,join(X0,X1)),join(X1,X0)))),
inference(forward_demodulation,[],[f2805,f112]) ).
fof(f3074,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(join(X1,X0),meet(X2,X0)))) = meet(X2,join(X0,join(meet(X2,X0),join(meet(X2,join(X0,X1)),X1)))),
inference(forward_demodulation,[],[f2991,f900]) ).
fof(f3149,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(join(X1,X0),meet(X2,X0)))) = meet(X2,join(X0,join(meet(X2,join(X0,X1)),X1))),
inference(forward_demodulation,[],[f3074,f103]) ).
fof(f3207,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(join(X1,X0),meet(X2,X0)))) = meet(X2,join(X0,join(X1,meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f3149,f6]) ).
fof(f3247,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X0,join(join(X1,X0),meet(X2,X0)))),
inference(forward_demodulation,[],[f3207,f115]) ).
fof(f3271,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X0,join(X1,X0))),
inference(forward_demodulation,[],[f3247,f1410]) ).
fof(f3288,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f3271,f59]) ).
fof(f3360,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f3288,f8]) ).
fof(f3415,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f3288]) ).
fof(f3549,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X2,X3)) = meet(join(X1,X0),join(X3,X2)),
inference(superposition,[],[f3415,f3415]) ).
fof(f3731,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(complement(X1),meet(X1,X0))),
inference(superposition,[],[f202,f200]) ).
fof(f3744,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(complement(X1),meet(join(X0,zero),X1))),
inference(superposition,[],[f202,f5]) ).
fof(f3814,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f3744,f200]) ).
fof(f4094,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f3731,f206]) ).
fof(f4110,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(superposition,[],[f3731,f1823]) ).
fof(f4188,plain,
! [X0,X1] : meet(X0,join(zero,complement(X0))) = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f4110,f3288]) ).
fof(f4204,plain,
! [X0,X1] : meet(X0,join(zero,complement(X0))) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4094,f3288]) ).
fof(f4226,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f4188,f207]) ).
fof(f4233,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4204,f207]) ).
fof(f4244,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f4226,f10]) ).
fof(f4250,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4233,f10]) ).
fof(f5557,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(superposition,[],[f1312,f9]) ).
fof(f5589,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f5557,f319]) ).
fof(f5610,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f5589,f200]) ).
fof(f5625,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f5610,f5]) ).
fof(f5636,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(one)),
inference(forward_subsumption_resolution,[],[f5625,f10]) ).
fof(f5644,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f5636,f319]) ).
fof(f5651,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f5644,f200]) ).
fof(f5711,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))) ),
inference(superposition,[],[f1949,f4250]) ).
fof(f5712,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),complement(join(X1,X0))) ),
inference(superposition,[],[f1949,f4244]) ).
fof(f5724,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(trivial_inequality_removal,[],[f5712]) ).
fof(f5725,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(trivial_inequality_removal,[],[f5711]) ).
fof(f5755,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f5724,f6]) ).
fof(f5756,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f5724,f4]) ).
fof(f5757,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f5724,f33]) ).
fof(f5759,plain,
! [X0,X1] : complement(join(X1,X0)) = join(complement(join(X1,X0)),complement(join(X0,X1))),
inference(superposition,[],[f5724,f334]) ).
fof(f5787,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f25,f5724]) ).
fof(f5818,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f5787,f5]) ).
fof(f5835,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f5757,f6]) ).
fof(f5836,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f5756,f6]) ).
fof(f5929,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(X0),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f216,f5836]) ).
fof(f5992,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(X0,complement(join(X1,complement(X0)))),
inference(superposition,[],[f5818,f5651]) ).
fof(f5995,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f5818,f6]) ).
fof(f6039,plain,
! [X2,X0,X1] : join(complement(X1),X2) = join(complement(X1),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f127,f5818]) ).
fof(f6401,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f5755,f5651]) ).
fof(f7345,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f25,f6401]) ).
fof(f7399,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f7345,f5]) ).
fof(f7765,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f127,f5995]) ).
fof(f8159,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(meet(X1,complement(meet(X0,X1))),complement(X0)),
inference(superposition,[],[f25,f5725]) ).
fof(f8202,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f8159,f5]) ).
fof(f8254,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f8202,f5929]) ).
fof(f8300,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(superposition,[],[f8254,f5]) ).
fof(f8336,plain,
! [X2,X0,X1] : meet(complement(join(X2,X1)),X0) = meet(X0,complement(meet(X0,join(X1,X2)))),
inference(superposition,[],[f8254,f3415]) ).
fof(f8375,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X0,X1)))) = meet(X1,join(complement(X1),meet(complement(X0),X1))),
inference(superposition,[],[f3731,f8254]) ).
fof(f8399,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X0,X1)))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f8375,f3814]) ).
fof(f8447,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f8399,f5835]) ).
fof(f8478,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f8447,f8254]) ).
fof(f8515,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),X0)),
inference(superposition,[],[f8478,f5651]) ).
fof(f8696,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(X1,complement(X0)),
inference(superposition,[],[f8515,f5651]) ).
fof(f8718,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f8515,f112]) ).
fof(f9012,plain,
! [X0,X1] : meet(X0,complement(meet(X0,join(complement(X0),X1)))) = meet(complement(join(complement(X0),meet(X1,X0))),X0),
inference(superposition,[],[f8300,f3814]) ).
fof(f9016,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(join(complement(X1),X0)),X1),
inference(superposition,[],[f8300,f8515]) ).
fof(f9120,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f9016,f5]) ).
fof(f9124,plain,
! [X0,X1] : meet(X0,complement(meet(X0,join(complement(X0),X1)))) = meet(X0,complement(join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f9012,f5]) ).
fof(f9162,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f9120,f7399]) ).
fof(f9166,plain,
! [X0,X1] : meet(X0,complement(meet(X0,join(complement(X0),X1)))) = complement(join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f9124,f7399]) ).
fof(f9196,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f9162,f8254]) ).
fof(f9200,plain,
! [X0,X1] : complement(join(complement(X0),meet(X1,X0))) = meet(complement(join(X1,complement(X0))),X0),
inference(forward_demodulation,[],[f9166,f8336]) ).
fof(f9223,plain,
! [X0,X1] : complement(join(complement(X0),meet(X1,X0))) = meet(X0,complement(join(X1,complement(X0)))),
inference(forward_demodulation,[],[f9200,f5]) ).
fof(f9235,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = complement(join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f9223,f5992]) ).
fof(f9240,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(complement(meet(X1,X0)),X0),
inference(forward_demodulation,[],[f9235,f9196]) ).
fof(f9244,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = complement(join(X1,complement(X0))),
inference(forward_demodulation,[],[f9240,f5]) ).
fof(f9247,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(X1,complement(X0))),
inference(forward_demodulation,[],[f9244,f8254]) ).
fof(f9307,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(meet(complement(X0),join(X1,meet(X0,complement(X0)))),complement(X0)),
inference(superposition,[],[f15,f8696]) ).
fof(f9344,plain,
! [X0,X1] : meet(complement(X1),complement(meet(X0,complement(X1)))) = meet(complement(join(X1,X0)),complement(X1)),
inference(superposition,[],[f8300,f8696]) ).
fof(f9345,plain,
! [X0,X1] : meet(complement(X1),complement(join(X1,X0))) = meet(complement(X1),complement(meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f9344,f5]) ).
fof(f9371,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),meet(complement(X0),join(X1,meet(X0,complement(X0))))),
inference(forward_demodulation,[],[f9307,f5]) ).
fof(f9404,plain,
! [X0,X1] : meet(complement(X1),complement(join(X1,X0))) = meet(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f9345,f8254]) ).
fof(f9424,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X1,meet(X0,complement(X0)))),
inference(forward_demodulation,[],[f9371,f61]) ).
fof(f9449,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f9404,f5995]) ).
fof(f9465,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X1,zero)),
inference(forward_demodulation,[],[f9424,f10]) ).
fof(f9496,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f9465,f200]) ).
fof(f9619,plain,
! [X0,X1] : meet(complement(complement(X0)),join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),X1))),
inference(superposition,[],[f8254,f9496]) ).
fof(f9622,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f9619,f5651]) ).
fof(f9676,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f9622,f3]) ).
fof(f9769,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(X1,complement(X0))),
inference(superposition,[],[f9449,f5651]) ).
fof(f9813,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(X1)),
inference(superposition,[],[f5,f9449]) ).
fof(f10296,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f5651,f9247]) ).
fof(f10314,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(meet(complement(X0),X1),join(join(X0,complement(X1)),X2)),
inference(superposition,[],[f8696,f9247]) ).
fof(f10322,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(complement(X0),meet(X1,join(join(X0,complement(X1)),X2))),
inference(forward_demodulation,[],[f10314,f7]) ).
fof(f10374,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(complement(X0),meet(X1,join(X0,join(complement(X1),X2)))),
inference(forward_demodulation,[],[f10322,f8]) ).
fof(f10404,plain,
! [X2,X0,X1] : meet(complement(X0),meet(join(X2,X0),X1)) = meet(X2,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f10374,f8718]) ).
fof(f10433,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X1),X0))) = X1,
inference(superposition,[],[f9676,f6]) ).
fof(f10656,plain,
! [X0,X1] : meet(join(X0,X1),join(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f10433,f10296]) ).
fof(f10903,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = meet(one,join(join(X1,complement(join(X0,X1))),complement(X0))),
inference(superposition,[],[f10656,f151]) ).
fof(f10904,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = meet(one,join(join(X1,complement(join(X1,X0))),complement(X0))),
inference(superposition,[],[f10656,f1238]) ).
fof(f11043,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = meet(one,join(complement(X0),join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f10904,f3288]) ).
fof(f11044,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = meet(one,join(complement(X0),join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f10903,f3288]) ).
fof(f11091,plain,
! [X0,X1] : join(X1,complement(join(X1,X0))) = join(complement(X0),join(X1,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f11043,f260]) ).
fof(f11092,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f11044,f260]) ).
fof(f11118,plain,
! [X0,X1] : join(complement(X0),X1) = join(X1,complement(join(X1,X0))),
inference(forward_demodulation,[],[f11091,f6039]) ).
fof(f11119,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),X1),
inference(forward_demodulation,[],[f11092,f7765]) ).
fof(f11181,plain,
! [X0,X1] : join(complement(X1),meet(complement(X0),X1)) = join(complement(X0),complement(X1)),
inference(superposition,[],[f11119,f9247]) ).
fof(f11493,plain,
! [X0,X1] : join(complement(complement(X1)),X0) = join(X0,meet(complement(X0),X1)),
inference(superposition,[],[f11118,f9247]) ).
fof(f11608,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f11493,f5651]) ).
fof(f12204,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f5651,f9769]) ).
fof(f13996,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X0,X1)),
inference(superposition,[],[f11608,f5651]) ).
fof(f14434,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,X1)) = join(meet(join(X0,X2),X1),complement(X0)),
inference(superposition,[],[f13996,f69]) ).
fof(f14466,plain,
! [X0,X1] : join(complement(meet(X0,X1)),complement(X1)) = join(complement(X1),meet(complement(X0),X1)),
inference(superposition,[],[f13996,f8254]) ).
fof(f14550,plain,
! [X0,X1] : join(complement(meet(X1,X0)),complement(X1)) = join(complement(X1),complement(join(X0,complement(X1)))),
inference(superposition,[],[f11118,f13996]) ).
fof(f14551,plain,
! [X0,X1] : join(meet(X1,X0),complement(join(X0,complement(X1)))) = join(complement(complement(X1)),meet(X1,X0)),
inference(superposition,[],[f11119,f13996]) ).
fof(f14554,plain,
! [X0,X1] : join(X1,meet(X1,X0)) = join(meet(X1,X0),complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f14551,f5651]) ).
fof(f14555,plain,
! [X0,X1] : join(complement(meet(X1,X0)),complement(X1)) = join(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14550,f11119]) ).
fof(f14617,plain,
! [X0,X1] : join(complement(meet(X0,X1)),complement(X1)) = join(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14466,f11181]) ).
fof(f14645,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,X1)) = join(complement(X0),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f14434,f6]) ).
fof(f14648,plain,
! [X0,X1] : join(X1,meet(X1,X0)) = join(meet(X1,X0),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f14554,f9247]) ).
fof(f14649,plain,
! [X0,X1] : join(complement(X1),complement(meet(X1,X0))) = join(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14555,f6]) ).
fof(f14700,plain,
! [X0,X1] : join(complement(X1),complement(meet(X0,X1))) = join(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14617,f6]) ).
fof(f14727,plain,
! [X2,X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f14645,f13996]) ).
fof(f14730,plain,
! [X0,X1] : join(meet(X1,X0),meet(complement(X0),X1)) = X1,
inference(forward_demodulation,[],[f14648,f4]) ).
fof(f14731,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14649,f5836]) ).
fof(f14767,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14700,f5835]) ).
fof(f14949,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = join(complement(complement(meet(X0,X1))),complement(join(complement(X1),complement(X0)))),
inference(superposition,[],[f5759,f14767]) ).
fof(f14980,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = complement(meet(join(complement(X1),complement(X0)),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f14949,f14731]) ).
fof(f15053,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = join(meet(X0,X1),complement(join(complement(X1),complement(X0)))),
inference(forward_demodulation,[],[f14980,f12204]) ).
fof(f15096,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = join(meet(X0,X1),meet(complement(complement(X1)),X0)),
inference(forward_demodulation,[],[f15053,f9247]) ).
fof(f15128,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,X0)) = complement(complement(meet(X0,X1))),
inference(forward_demodulation,[],[f15096,f5651]) ).
fof(f15154,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X1,X0)),
inference(forward_demodulation,[],[f15128,f5651]) ).
fof(f15526,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(superposition,[],[f14767,f14731]) ).
fof(f16047,plain,
! [X2,X0,X1] : complement(join(X2,complement(meet(X0,X1)))) = meet(complement(X2),meet(X1,X0)),
inference(superposition,[],[f9247,f15526]) ).
fof(f16074,plain,
! [X2,X0,X1] : meet(complement(X2),meet(X0,X1)) = meet(complement(X2),meet(X1,X0)),
inference(forward_demodulation,[],[f16047,f9247]) ).
fof(f16764,plain,
! [X0,X1] : join(meet(X1,complement(X0)),meet(X0,X1)) = X1,
inference(superposition,[],[f14730,f5651]) ).
fof(f16970,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f16764,f6]) ).
fof(f17353,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(X0,X1),meet(meet(join(X2,X0),X1),complement(X0))),
inference(superposition,[],[f16970,f68]) ).
fof(f17599,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(X0,X1),meet(complement(X0),meet(join(X2,X0),X1))),
inference(forward_demodulation,[],[f17353,f5]) ).
fof(f17683,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(X0,X1),meet(X2,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f17599,f10404]) ).
fof(f18869,plain,
! [X2,X0,X1] : complement(meet(complement(X0),meet(X1,X2))) = complement(meet(meet(X2,X1),complement(X0))),
inference(superposition,[],[f15526,f16074]) ).
fof(f18873,plain,
! [X2,X0,X1] : complement(meet(complement(X0),meet(X1,X2))) = join(X0,complement(meet(X2,X1))),
inference(forward_demodulation,[],[f18869,f12204]) ).
fof(f18964,plain,
! [X2,X0,X1] : join(X0,complement(meet(X1,X2))) = join(X0,complement(meet(X2,X1))),
inference(forward_demodulation,[],[f18873,f10296]) ).
fof(f23174,plain,
! [X2,X0,X1] : join(X2,complement(meet(complement(X1),complement(X0)))) = join(X2,complement(complement(join(X0,X1)))),
inference(superposition,[],[f18964,f9813]) ).
fof(f23179,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,complement(meet(complement(X1),complement(X0)))),
inference(forward_demodulation,[],[f23174,f5651]) ).
fof(f23257,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f23179,f10296]) ).
fof(f23315,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f23257,f5651]) ).
fof(f23468,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f23315,f15154]) ).
fof(f23725,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f23468,f15154]) ).
fof(f23998,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f23725]) ).
fof(f24021,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(X3,join(meet(X2,X1),X0)),
inference(superposition,[],[f3288,f23725]) ).
fof(f24022,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(join(meet(X2,X1),X0),X3),
inference(superposition,[],[f3415,f23725]) ).
fof(f24483,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X1,X2)),join(X0,meet(X2,X1))),
inference(superposition,[],[f2457,f23998]) ).
fof(f39640,plain,
! [X2,X0,X1] : join(meet(join(X1,X2),X0),complement(join(X0,complement(X1)))) = join(complement(complement(X1)),meet(join(X1,X2),X0)),
inference(superposition,[],[f11119,f14727]) ).
fof(f39650,plain,
! [X2,X0,X1] : join(meet(join(X1,X2),X0),complement(join(X0,complement(X1)))) = join(X1,meet(join(X1,X2),X0)),
inference(forward_demodulation,[],[f39640,f5651]) ).
fof(f39788,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(meet(join(X1,X2),X0),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f39650,f9247]) ).
fof(f39888,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X2),X0)) = join(meet(complement(X0),X1),meet(join(X1,X2),X0)),
inference(forward_demodulation,[],[f39788,f6]) ).
fof(f92749,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X1,X2))) = join(meet(complement(join(complement(join(X1,X2)),X0)),X1),meet(X0,join(X1,X2))),
inference(superposition,[],[f39888,f8515]) ).
fof(f92827,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(complement(X2),X0)) = meet(join(meet(join(X0,X1),X2),meet(complement(X2),X0)),join(X0,meet(join(X0,X1),X2))),
inference(superposition,[],[f2457,f39888]) ).
fof(f92917,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(complement(X2),X0)) = meet(join(meet(X2,join(X0,X1)),X0),join(meet(join(X0,X1),X2),meet(complement(X2),X0))),
inference(forward_demodulation,[],[f92827,f24022]) ).
fof(f92978,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X1,X2))) = join(meet(X0,join(X1,X2)),meet(complement(join(complement(join(X1,X2)),X0)),X1)),
inference(forward_demodulation,[],[f92749,f6]) ).
fof(f93200,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(complement(X2),X0)) = meet(join(meet(X2,join(X0,X1)),X0),join(meet(X0,complement(X2)),meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f92917,f24021]) ).
fof(f93252,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X1,X2))) = join(meet(X0,join(X1,X2)),meet(X1,complement(join(complement(join(X1,X2)),X0)))),
inference(forward_demodulation,[],[f92978,f23725]) ).
fof(f93429,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(complement(X2),X0)) = meet(join(X0,meet(X2,join(X0,X1))),join(meet(join(X0,X1),X2),meet(X0,complement(X2)))),
inference(forward_demodulation,[],[f93200,f3549]) ).
fof(f93471,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X1,X2))) = join(meet(X0,join(X1,X2)),meet(X1,meet(complement(X0),join(X1,X2)))),
inference(forward_demodulation,[],[f93252,f9196]) ).
fof(f93597,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(complement(X2),X0)) = meet(join(X0,meet(X2,join(X0,X1))),join(meet(complement(X2),X0),meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f93429,f24021]) ).
fof(f93634,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X1,X2))) = meet(join(X1,X0),join(X1,X2)),
inference(forward_demodulation,[],[f93471,f17683]) ).
fof(f93736,plain,
! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(complement(X2),X0)) = meet(join(X0,meet(X2,join(X0,X1))),join(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f93597,f39888]) ).
fof(f93839,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X0,X1))) = join(meet(join(X0,X1),X2),meet(complement(X2),X0)),
inference(forward_demodulation,[],[f93736,f24483]) ).
fof(f93924,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X0,X1))) = join(meet(complement(X2),X0),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f93839,f6]) ).
fof(f93994,plain,
! [X2,X0,X1] : meet(join(X0,X2),join(X0,X1)) = join(meet(complement(X2),X0),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f93924,f93634]) ).
fof(f101953,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(join(X0,X2),X1)),
inference(superposition,[],[f39888,f93994]) ).
fof(f103799,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X2),X0) = join(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f101953,f14730]) ).
fof(f104336,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f103799,f5]) ).
fof(f107825,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X0,meet(X0,join(meet(X0,X1),X2))))),
inference(superposition,[],[f18,f104336]) ).
fof(f107873,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = join(meet(X0,X2),meet(X0,join(meet(X0,X1),X2))),
inference(superposition,[],[f334,f104336]) ).
fof(f108023,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(meet(X0,X2),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f107873,f104336]) ).
fof(f108061,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X0,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f107825,f61]) ).
fof(f108280,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(X2,join(meet(X0,X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f108023,f3360]) ).
fof(f108307,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f108061,f18]) ).
fof(f108455,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f108280,f103]) ).
fof(f108593,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f108455,f108307]) ).
fof(f109118,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(superposition,[],[f13,f108593]) ).
fof(f109252,plain,
$false,
inference(trivial_inequality_removal,[],[f109118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT210-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.13/0.40 % Computer : n005.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 14:06:02 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.46 Running first-order theorem proving
% 0.13/0.46 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.46/3.95 % (4018357)Input is clausal, will run a generic CNF schedule.
% 19.46/3.95 % (4018363)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3524079609:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 19.46/3.95 % (4018365)lrs+10_1_sil=8000:sp=occurrence:random_seed=1557368154:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 19.46/3.95 % (4018362)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=12698:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 19.46/3.95 % (4018368)dis-21_1_sil=8000:lcm=predicate:random_seed=762398070: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.46/3.95 % (4018367)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=871575107:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 19.46/3.95 % (4018364)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4258900692:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 19.46/3.95 % (4018366)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3468472904:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 19.46/3.95 % (4018368)Refutation not found, incomplete strategy
% 19.46/3.95 % (4018368)------------------------------
% 19.46/3.95 % (4018368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.95 % (4018368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.95 % (4018368)CaDiCaL version: 2.1.3
% 19.46/3.95 % (4018368)Termination reason: Refutation not found, incomplete strategy
% 19.46/3.95 % (4018368)Time elapsed: 0.003 s
% 19.46/3.95 % (4018368)Peak memory usage: 88 MB
% 19.46/3.95 % (4018368)Instructions burned: 1 (million)
% 19.46/3.95 % (4018365)Instruction limit reached!
% 19.46/3.95 % (4018365)------------------------------
% 19.46/3.95 % (4018365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.95 % (4018365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.95 % (4018365)CaDiCaL version: 2.1.3
% 19.46/3.95 % (4018365)Termination reason: Instruction limit
% 19.46/3.95 % (4018365)Termination phase: Saturation
% 19.46/3.95 % (4018365)Time elapsed: 0.104 s
% 19.46/3.95 % (4018365)Peak memory usage: 88 MB
% 19.46/3.95 % (4018365)Instructions burned: 107 (million)
% 19.46/3.95 % (4018366)Instruction limit reached!
% 19.46/3.95 % (4018366)------------------------------
% 19.46/3.95 % (4018366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.95 % (4018366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.95 % (4018366)CaDiCaL version: 2.1.3
% 19.46/3.95 % (4018366)Termination reason: Instruction limit
% 19.46/3.95 % (4018366)Termination phase: Saturation
% 19.46/3.95 % (4018366)Time elapsed: 0.111 s
% 19.46/3.95 % (4018366)Peak memory usage: 89 MB
% 19.46/3.95 % (4018366)Instructions burned: 114 (million)
% 19.46/3.95 % (4018367)Instruction limit reached!
% 19.46/3.95 % (4018367)------------------------------
% 19.46/3.95 % (4018367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.95 % (4018367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.95 % (4018367)CaDiCaL version: 2.1.3
% 19.46/3.95 % (4018367)Termination reason: Instruction limit
% 19.46/3.95 % (4018367)Termination phase: Saturation
% 19.46/3.95 % (4018367)Time elapsed: 0.163 s
% 19.46/3.95 % (4018367)Peak memory usage: 89 MB
% 19.46/3.95 % (4018367)Instructions burned: 180 (million)
% 19.46/3.95 % (4018376)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=616025990:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 19.46/3.95 % (4018376)Refutation not found, incomplete strategy
% 19.46/3.95 % (4018376)------------------------------
% 19.46/3.95 % (4018376)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.46/3.95 % (4018376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.46/3.95 % (4018376)CaDiCaL version: 2.1.3
% 19.46/3.95 % (4018376)Termination reason: Refutation not found, incomplete strategy
% 19.46/3.95 % (4018376)Time elapsed: 0.002 s
% 19.46/3.95 % (4018376)Peak memory usage: 88 MB
% 19.46/3.95 % (4018377)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1586472621: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)
% 28.74/5.09 % (4018377)Refutation not found, incomplete strategy
% 28.74/5.09 % (4018377)------------------------------
% 28.74/5.09 % (4018377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018377)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018377)Termination reason: Refutation not found, incomplete strategy
% 28.74/5.09 % (4018377)Time elapsed: 0.002 s
% 28.74/5.09 % (4018377)Peak memory usage: 88 MB
% 28.74/5.09 % (4018377)Instructions burned: 1 (million)
% 28.74/5.09 % (4018368)------------------------------
% 28.74/5.09 % (4018368)------------------------------
% 28.74/5.09 % (4018378)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1215052253:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 28.74/5.09 % (4018378)Refutation not found, incomplete strategy
% 28.74/5.09 % (4018378)------------------------------
% 28.74/5.09 % (4018378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018378)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018378)Termination reason: Refutation not found, incomplete strategy
% 28.74/5.09 % (4018378)Time elapsed: 0.002 s
% 28.74/5.09 % (4018378)Peak memory usage: 88 MB
% 28.74/5.09 % (4018376)------------------------------
% 28.74/5.09 % (4018376)------------------------------
% 28.74/5.09 % (4018381)lrs+10_64_to=lpo:sil=8000:random_seed=3576115511:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 28.74/5.09 % (4018377)------------------------------
% 28.74/5.09 % (4018377)------------------------------
% 28.74/5.09 % (4018381)Instruction limit reached!
% 28.74/5.09 % (4018381)------------------------------
% 28.74/5.09 % (4018381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018381)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018381)Termination reason: Instruction limit
% 28.74/5.09 % (4018381)Termination phase: Saturation
% 28.74/5.09 % (4018381)Time elapsed: 0.112 s
% 28.74/5.09 % (4018381)Peak memory usage: 88 MB
% 28.74/5.09 % (4018381)Instructions burned: 127 (million)
% 28.74/5.09 % (4018378)------------------------------
% 28.74/5.09 % (4018378)------------------------------
% 28.74/5.09 % (4018384)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1571601052:avsq=on:i=194:fgj=on:bd=preordered_2990 on theBenchmark for (2990ds/194Mi)
% 28.74/5.09 % (4018385)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2606421027:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 28.74/5.09 % (4018386)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2051662168:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 28.74/5.09 % (4018387)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=3235385411:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 28.74/5.09 % (4018384)Instruction limit reached!
% 28.74/5.09 % (4018384)------------------------------
% 28.74/5.09 % (4018384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018384)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018384)Termination reason: Instruction limit
% 28.74/5.09 % (4018384)Termination phase: Saturation
% 28.74/5.09 % (4018384)Time elapsed: 0.197 s
% 28.74/5.09 % (4018384)Peak memory usage: 90 MB
% 28.74/5.09 % (4018384)Instructions burned: 196 (million)
% 28.74/5.09 % (4018385)Instruction limit reached!
% 28.74/5.09 % (4018385)------------------------------
% 28.74/5.09 % (4018385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018385)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018385)Termination reason: Instruction limit
% 28.74/5.09 % (4018385)Termination phase: Saturation
% 28.74/5.09 % (4018385)Time elapsed: 0.154 s
% 28.74/5.09 % (4018385)Peak memory usage: 90 MB
% 28.74/5.09 % (4018385)Instructions burned: 157 (million)
% 28.74/5.09 % (4018387)Instruction limit reached!
% 28.74/5.09 % (4018387)------------------------------
% 28.74/5.09 % (4018387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018387)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018387)Termination reason: Instruction limit
% 28.74/5.09 % (4018387)Termination phase: Saturation
% 28.74/5.09 % (4018387)Time elapsed: 0.111 s
% 28.74/5.09 % (4018387)Peak memory usage: 89 MB
% 28.74/5.09 % (4018387)Instructions burned: 106 (million)
% 28.74/5.09 % (4018393)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4128570352:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2985 on theBenchmark for (2985ds/242Mi)
% 28.74/5.09 % (4018392)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3111578078:i=107_2985 on theBenchmark for (2985ds/107Mi)
% 28.74/5.09 % (4018392)Refutation not found, incomplete strategy
% 28.74/5.09 % (4018392)------------------------------
% 28.74/5.09 % (4018392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018392)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018392)Termination reason: Refutation not found, incomplete strategy
% 28.74/5.09 % (4018392)Time elapsed: 0.002 s
% 28.74/5.09 % (4018392)Peak memory usage: 87 MB
% 28.74/5.09 % (4018394)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=148050157:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 28.74/5.09 % (4018393)Instruction limit reached!
% 28.74/5.09 % (4018393)------------------------------
% 28.74/5.09 % (4018393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018393)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018393)Termination reason: Instruction limit
% 28.74/5.09 % (4018393)Termination phase: Saturation
% 28.74/5.09 % (4018393)Time elapsed: 0.229 s
% 28.74/5.09 % (4018393)Peak memory usage: 90 MB
% 28.74/5.09 % (4018393)Instructions burned: 242 (million)
% 28.74/5.09 % (4018392)------------------------------
% 28.74/5.09 % (4018392)------------------------------
% 28.74/5.09 % (4018398)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=4291024476:i=134:sd=2:doe=on:ss=axioms:sgt=14_2980 on theBenchmark for (2980ds/134Mi)
% 28.74/5.09 % (4018398)Instruction limit reached!
% 28.74/5.09 % (4018398)------------------------------
% 28.74/5.09 % (4018398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018398)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018398)Termination reason: Instruction limit
% 28.74/5.09 % (4018398)Termination phase: Saturation
% 28.74/5.09 % (4018398)Time elapsed: 0.135 s
% 28.74/5.09 % (4018398)Peak memory usage: 89 MB
% 28.74/5.09 % (4018398)Instructions burned: 134 (million)
% 28.74/5.09 % (4018399)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3170127655:i=499:bd=all_2978 on theBenchmark for (2978ds/499Mi)
% 28.74/5.09 % (4018401)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3094914914:i=191:fgj=on:bd=all_2976 on theBenchmark for (2976ds/191Mi)
% 28.74/5.09 % (4018401)Instruction limit reached!
% 28.74/5.09 % (4018401)------------------------------
% 28.74/5.09 % (4018401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018401)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018401)Termination reason: Instruction limit
% 28.74/5.09 % (4018401)Termination phase: Saturation
% 28.74/5.09 % (4018401)Time elapsed: 0.200 s
% 28.74/5.09 % (4018401)Peak memory usage: 91 MB
% 28.74/5.09 % (4018401)Instructions burned: 191 (million)
% 28.74/5.09 % (4018399)Instruction limit reached!
% 28.74/5.09 % (4018399)------------------------------
% 28.74/5.09 % (4018399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018399)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018399)Termination reason: Instruction limit
% 28.74/5.09 % (4018399)Termination phase: Saturation
% 28.74/5.09 % (4018399)Time elapsed: 0.499 s
% 28.74/5.09 % (4018399)Peak memory usage: 94 MB
% 28.74/5.09 % (4018399)Instructions burned: 499 (million)
% 28.74/5.09 % (4018404)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=847779210:i=264:kws=precedence:fsr=off_2971 on theBenchmark for (2971ds/264Mi)
% 28.74/5.09 % (4018405)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3049007895:cond=on:i=156:bs=on:gtg=exists_all:er=known_2971 on theBenchmark for (2971ds/156Mi)
% 28.74/5.09 % (4018405)Instruction limit reached!
% 28.74/5.09 % (4018405)------------------------------
% 28.74/5.09 % (4018405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018405)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018405)Termination reason: Instruction limit
% 28.74/5.09 % (4018405)Termination phase: Saturation
% 28.74/5.09 % (4018405)Time elapsed: 0.154 s
% 28.74/5.09 % (4018405)Peak memory usage: 89 MB
% 28.74/5.09 % (4018405)Instructions burned: 156 (million)
% 28.74/5.09 % (4018404)Instruction limit reached!
% 28.74/5.09 % (4018404)------------------------------
% 28.74/5.09 % (4018404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.74/5.09 % (4018404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.74/5.09 % (4018404)CaDiCaL version: 2.1.3
% 28.74/5.09 % (4018404)Termination reason: Instruction limit
% 28.74/5.09 % (4018404)Termination phase: Saturation
% 28.74/5.09 % (4018404)Time elapsed: 0.257 s
% 28.74/5.09 % (4018404)Peak memory usage: 92 MB
% 28.74/5.09 % (4018404)Instructions burned: 264 (million)
% 28.74/5.09 % (4018410)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=1906815142:i=3256:kws=precedence:bd=preordered:av=off_2966 on theBenchmark for (2966ds/3256Mi)
% 28.74/5.09 % (4018411)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3462361104:i=537:av=off:ss=included_2965 on theBenchmark for (2965ds/537Mi)
% 28.74/5.09 % (4018363)First to succeed.
% 28.74/5.09 % (4018363)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4018357"
% 28.74/5.09 % (4018363)Refutation found. Thanks to Tanya!
% 28.74/5.09 % SZS status Unsatisfiable for theBenchmark
% 28.74/5.09 % SZS output start Proof for theBenchmark
% See solution above
% 29.22/5.26 % (4018363)------------------------------
% 29.22/5.26 % (4018363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.22/5.26 % (4018363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.22/5.26 % (4018363)CaDiCaL version: 2.1.3
% 29.22/5.26 % (4018363)Termination reason: Refutation
% 29.22/5.26 % (4018363)Time elapsed: 3.578 s
% 29.22/5.26 % (4018363)Peak memory usage: 172 MB
% 29.22/5.26 % (4018363)Instructions burned: 6403 (million)
% 29.22/5.26 % (4018363)------------------------------
% 29.22/5.26 % (4018363)------------------------------
% 29.22/5.26 % (4018357)Success in time 4.037 s
% 29.22/5.26 % Vampire exiting
%------------------------------------------------------------------------------