%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT199-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:13 AM UTC 2026
% Result : Unsatisfiable 36.19s 5.85s
% Output : Refutation 37.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 12
% Syntax : Number of formulae : 251 ( 239 unt; 0 def)
% Number of atoms : 266 ( 265 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 : 593 ( 593 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,join(meet(X0,X2),meet(X2,join(X1,X3))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H49) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f15,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f17,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f22,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f17,f3]) ).
fof(f24,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f22,f6]) ).
fof(f36,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f37,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f15]) ).
fof(f46,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f53,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f54,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f17]) ).
fof(f63,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f74,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f53,f6]) ).
fof(f95,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f97,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f98,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f106,plain,
! [X2,X3,X0,X1] : meet(X2,join(X1,meet(X3,join(X2,X0)))) = meet(X2,join(X1,join(meet(X2,X3),meet(X3,join(X0,X1))))),
inference(superposition,[],[f12,f6]) ).
fof(f110,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X1))))) = meet(X0,join(X1,join(meet(X0,X2),meet(X2,one)))),
inference(superposition,[],[f12,f9]) ).
fof(f119,plain,
! [X2,X3,X0,X1] : meet(X3,join(X1,meet(X0,join(X3,X2)))) = meet(X3,join(X1,join(meet(X0,join(X1,X2)),meet(X3,X0)))),
inference(superposition,[],[f12,f6]) ).
fof(f139,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X1))))) = meet(X0,join(X1,join(meet(X0,X2),X2))),
inference(forward_demodulation,[],[f110,f97]) ).
fof(f149,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X1))))) = meet(X0,join(X1,join(X2,meet(X0,X2)))),
inference(forward_demodulation,[],[f139,f6]) ).
fof(f152,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(X2,join(X0,complement(X1))))),
inference(forward_demodulation,[],[f149,f17]) ).
fof(f161,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f36,f5]) ).
fof(f188,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f191,plain,
! [X0] : complement(X0) = join(complement(X0),zero),
inference(superposition,[],[f17,f10]) ).
fof(f193,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f195,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f191,f6]) ).
fof(f202,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f97]) ).
fof(f205,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f97]) ).
fof(f245,plain,
zero = complement(one),
inference(superposition,[],[f10,f202]) ).
fof(f286,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(meet(X1,X2),meet(X2,X0)))) = meet(X1,join(X0,meet(X2,join(X1,zero)))),
inference(superposition,[],[f12,f188]) ).
fof(f287,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f15,f188]) ).
fof(f292,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(meet(X1,X2),meet(X2,X0)))) = meet(X1,join(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f286,f188]) ).
fof(f300,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f5,f287]) ).
fof(f454,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(join(X0,complement(X1)),X2))),
inference(superposition,[],[f152,f5]) ).
fof(f667,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f54,f6]) ).
fof(f739,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f37,f10]) ).
fof(f777,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f739,f300]) ).
fof(f1014,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,f98]) ).
fof(f1025,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1014]) ).
fof(f1067,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f1025,f6]) ).
fof(f1755,plain,
! [X0,X1] :
( one != join(one,X0)
| zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(superposition,[],[f11,f95]) ).
fof(f1784,plain,
! [X0,X1] :
( zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(forward_subsumption_resolution,[],[f1755,f205]) ).
fof(f2029,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X2,join(X1,zero)))) = meet(X1,join(X0,join(meet(X2,X0),meet(X1,X2)))),
inference(superposition,[],[f119,f188]) ).
fof(f2161,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X2,join(X1,zero)))) = meet(X1,join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f2029,f54]) ).
fof(f2210,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X2,X1))) = meet(X1,join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f2161,f188]) ).
fof(f2881,plain,
! [X2,X0,X1] : meet(X0,join(complement(X1),meet(X2,join(X0,X1)))) = meet(X0,join(complement(X1),join(meet(X0,X2),meet(X2,one)))),
inference(superposition,[],[f106,f9]) ).
fof(f2992,plain,
! [X2,X0,X1] : meet(X0,join(complement(X1),meet(X2,join(X0,X1)))) = meet(X0,join(complement(X1),join(meet(X0,X2),X2))),
inference(forward_demodulation,[],[f2881,f97]) ).
fof(f3047,plain,
! [X2,X0,X1] : meet(X0,join(complement(X1),meet(X2,join(X0,X1)))) = meet(X0,join(complement(X1),join(X2,meet(X0,X2)))),
inference(forward_demodulation,[],[f2992,f6]) ).
fof(f3081,plain,
! [X2,X0,X1] : meet(X0,join(complement(X1),X2)) = meet(X0,join(complement(X1),meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f3047,f17]) ).
fof(f4102,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X1,X0))) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f3081,f2]) ).
fof(f4245,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f4102,f5]) ).
fof(f4900,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(superposition,[],[f1067,f9]) ).
fof(f4930,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4900,f245]) ).
fof(f4950,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4930,f188]) ).
fof(f4964,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4950,f5]) ).
fof(f4975,plain,
! [X0] : join(X0,complement(one)) = complement(complement(X0)),
inference(forward_subsumption_resolution,[],[f4964,f10]) ).
fof(f4984,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f4975,f245]) ).
fof(f4990,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f4984,f188]) ).
fof(f5358,plain,
! [X0,X1] : meet(X0,join(X1,zero)) = meet(X0,join(X1,complement(join(X0,complement(X1))))),
inference(superposition,[],[f454,f10]) ).
fof(f5465,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,complement(X1))))),
inference(forward_demodulation,[],[f5358,f188]) ).
fof(f5536,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(X1,join(complement(X0),complement(join(X1,X0)))),
inference(superposition,[],[f5465,f4990]) ).
fof(f5543,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(complement(X0),X1)))),
inference(superposition,[],[f5465,f6]) ).
fof(f5556,plain,
! [X0,X1] : meet(X1,join(join(X0,complement(X1)),X0)) = meet(X1,join(join(X0,complement(X1)),meet(X0,X1))),
inference(superposition,[],[f152,f5465]) ).
fof(f5626,plain,
! [X0,X1] : meet(X1,join(join(X0,complement(X1)),X0)) = meet(X1,join(meet(X0,X1),join(X0,complement(X1)))),
inference(forward_demodulation,[],[f5556,f6]) ).
fof(f5653,plain,
! [X0,X1] : meet(X1,join(join(X0,complement(X1)),X0)) = meet(X1,join(complement(X1),join(meet(X0,X1),X0))),
inference(forward_demodulation,[],[f5626,f63]) ).
fof(f5667,plain,
! [X0,X1] : meet(X1,join(join(X0,complement(X1)),X0)) = meet(X1,join(complement(X1),join(X0,meet(X0,X1)))),
inference(forward_demodulation,[],[f5653,f6]) ).
fof(f5673,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(join(X0,complement(X1)),X0)),
inference(forward_demodulation,[],[f5667,f4]) ).
fof(f5675,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(X0,join(X0,complement(X1)))),
inference(forward_demodulation,[],[f5673,f6]) ).
fof(f5677,plain,
! [X0,X1] : meet(X1,join(X0,complement(X1))) = meet(X1,join(complement(X1),X0)),
inference(forward_demodulation,[],[f5675,f24]) ).
fof(f6524,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(X0,join(complement(meet(X1,X0)),complement(X0))),
inference(superposition,[],[f5536,f17]) ).
fof(f6637,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(X0,join(complement(X0),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f6524,f5677]) ).
fof(f6791,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,join(meet(X0,X1),join(meet(X1,X2),X2))),
inference(superposition,[],[f292,f63]) ).
fof(f6877,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,join(meet(X0,X1),join(X2,meet(X1,X2)))),
inference(forward_demodulation,[],[f6791,f6]) ).
fof(f6998,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f6877,f17]) ).
fof(f7228,plain,
! [X2,X3,X0,X1] : meet(X1,join(join(X3,X0),meet(X2,X1))) = meet(X1,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f6998,f63]) ).
fof(f7486,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,join(meet(X1,X2),X3))) = meet(X1,join(X3,join(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f7228,f8]) ).
fof(f7715,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f4245,f193]) ).
fof(f7745,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(superposition,[],[f4245,f777]) ).
fof(f7859,plain,
! [X0,X1] : meet(X0,join(zero,complement(X0))) = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f7745,f5677]) ).
fof(f7889,plain,
! [X0,X1] : meet(X0,join(zero,complement(X0))) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f7715,f5677]) ).
fof(f7914,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f7859,f195]) ).
fof(f7922,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f7889,f195]) ).
fof(f7933,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f7914,f10]) ).
fof(f7937,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f7922,f10]) ).
fof(f7981,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),complement(join(X1,X0))) ),
inference(superposition,[],[f1784,f7933]) ).
fof(f8028,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(trivial_inequality_removal,[],[f7981]) ).
fof(f8172,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(superposition,[],[f8028,f4990]) ).
fof(f8175,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f8028,f6]) ).
fof(f8176,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f8028,f4]) ).
fof(f8177,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f8028,f17]) ).
fof(f8211,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f15,f8028]) ).
fof(f8257,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f8211,f5]) ).
fof(f8278,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f8177,f6]) ).
fof(f8279,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f8176,f6]) ).
fof(f8403,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(X0),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f161,f8279]) ).
fof(f8473,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f8257,f6]) ).
fof(f8475,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f8257,f17]) ).
fof(f8513,plain,
! [X2,X0,X1] : join(complement(X1),X2) = join(complement(X1),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f74,f8257]) ).
fof(f8564,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f8475,f5]) ).
fof(f8684,plain,
! [X2,X0,X1] : meet(X1,join(complement(meet(X2,X0)),meet(complement(X0),X1))) = meet(X1,join(complement(meet(X2,X0)),join(meet(X1,complement(X0)),complement(X0)))),
inference(superposition,[],[f292,f8564]) ).
fof(f8698,plain,
! [X2,X0,X1] : meet(X1,join(complement(meet(X2,X0)),meet(complement(X0),X1))) = meet(X1,join(complement(X0),join(complement(meet(X2,X0)),meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f8684,f7486]) ).
fof(f8747,plain,
! [X2,X0,X1] : meet(X1,join(complement(meet(X2,X0)),meet(complement(X0),X1))) = meet(X1,join(complement(X0),complement(meet(X2,X0)))),
inference(forward_demodulation,[],[f8698,f74]) ).
fof(f8764,plain,
! [X2,X0,X1] : meet(X1,join(complement(meet(X2,X0)),meet(complement(X0),X1))) = meet(X1,complement(meet(X2,X0))),
inference(forward_demodulation,[],[f8747,f8278]) ).
fof(f8780,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f8175,f4990]) ).
fof(f9334,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f15,f8780]) ).
fof(f9400,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f9334,f5]) ).
fof(f9729,plain,
! [X2,X0,X1] : join(X2,X0) = join(X0,join(complement(join(X1,complement(X0))),X2)),
inference(superposition,[],[f63,f8172]) ).
fof(f10482,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),complement(meet(X2,X1))) = meet(complement(join(X0,X1)),join(complement(meet(X2,X1)),complement(join(X0,X1)))),
inference(superposition,[],[f8764,f8257]) ).
fof(f10678,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(meet(X2,X1))),
inference(forward_demodulation,[],[f10482,f15]) ).
fof(f10899,plain,
! [X2,X0,X1] : complement(meet(X2,X1)) = join(complement(meet(X2,X1)),complement(join(X0,X1))),
inference(superposition,[],[f17,f10678]) ).
fof(f11111,plain,
! [X2,X0,X1] : complement(meet(X2,X0)) = join(complement(meet(X2,X0)),complement(join(X0,X1))),
inference(superposition,[],[f10899,f6]) ).
fof(f12014,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))) ),
inference(superposition,[],[f1784,f7937]) ).
fof(f12070,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(trivial_inequality_removal,[],[f12014]) ).
fof(f12380,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(meet(X1,complement(meet(X0,X1))),complement(X0)),
inference(superposition,[],[f15,f12070]) ).
fof(f12441,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f12380,f5]) ).
fof(f12506,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f12441,f8403]) ).
fof(f12556,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(superposition,[],[f12506,f5]) ).
fof(f12654,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X0,X1)))) = meet(X1,join(complement(X1),meet(complement(X0),X1))),
inference(superposition,[],[f4245,f12506]) ).
fof(f12693,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X0,X1)))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f12654,f4102]) ).
fof(f12758,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f12693,f6637]) ).
fof(f12789,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f12758,f12506]) ).
fof(f12847,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(complement(join(X1,complement(join(complement(X1),X0)))),X0),
inference(superposition,[],[f12556,f5543]) ).
fof(f13008,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,complement(join(X1,complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f12847,f5]) ).
fof(f13073,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,complement(X1)),
inference(forward_demodulation,[],[f13008,f8780]) ).
fof(f13182,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),X0)),
inference(superposition,[],[f12789,f4990]) ).
fof(f13275,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(complement(X0),join(X1,complement(X2))))) = meet(X1,join(X2,join(complement(join(X1,complement(X2))),complement(X0)))),
inference(superposition,[],[f454,f12789]) ).
fof(f13291,plain,
! [X2,X0,X1] : meet(X1,join(complement(X0),X2)) = meet(X1,join(X2,meet(complement(X0),join(X1,complement(X2))))),
inference(forward_demodulation,[],[f13275,f9729]) ).
fof(f13346,plain,
! [X2,X0,X1] : meet(X1,join(X2,complement(X0))) = meet(X1,join(complement(X0),X2)),
inference(forward_demodulation,[],[f13291,f152]) ).
fof(f13411,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(superposition,[],[f13182,f4990]) ).
fof(f13431,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f13182,f63]) ).
fof(f13498,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(meet(join(X0,complement(complement(X0))),X1),X0),
inference(superposition,[],[f454,f13182]) ).
fof(f13550,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(join(complement(X1),X0)),X1),
inference(superposition,[],[f12556,f13182]) ).
fof(f13575,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f13550,f5]) ).
fof(f13604,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,meet(join(X0,complement(complement(X0))),X1)),
inference(forward_demodulation,[],[f13498,f5]) ).
fof(f13671,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f13575,f9400]) ).
fof(f13693,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f13604,f36]) ).
fof(f13748,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f13671,f12506]) ).
fof(f13892,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(meet(join(complement(X0),complement(X0)),X1),complement(X0)),
inference(superposition,[],[f454,f13411]) ).
fof(f13950,plain,
! [X0,X1] : meet(complement(X1),complement(meet(X0,complement(X1)))) = meet(complement(join(X1,X0)),complement(X1)),
inference(superposition,[],[f12556,f13411]) ).
fof(f13951,plain,
! [X0,X1] : meet(complement(X1),complement(join(X1,X0))) = meet(complement(X1),complement(meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f13950,f5]) ).
fof(f13991,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),meet(join(complement(X0),complement(X0)),X1)),
inference(forward_demodulation,[],[f13892,f5]) ).
fof(f14045,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(X1),complement(join(X1,X0))),
inference(forward_demodulation,[],[f13951,f12506]) ).
fof(f14076,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f13991,f37]) ).
fof(f14122,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(X1)),
inference(forward_demodulation,[],[f14045,f8473]) ).
fof(f14225,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(X1,complement(X0))),
inference(superposition,[],[f14122,f4990]) ).
fof(f14586,plain,
! [X0,X1] : meet(complement(complement(X0)),join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),X1))),
inference(superposition,[],[f12506,f14076]) ).
fof(f14589,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f14586,f4990]) ).
fof(f14681,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f14589,f3]) ).
fof(f14881,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f4990,f14225]) ).
fof(f15060,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X1),X0))) = X1,
inference(superposition,[],[f14681,f6]) ).
fof(f15097,plain,
! [X0,X1] : meet(join(X1,join(X1,X0)),complement(meet(X0,complement(X1)))) = X1,
inference(superposition,[],[f14681,f13411]) ).
fof(f15306,plain,
! [X0,X1] : meet(join(X1,join(X1,X0)),join(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f15097,f14881]) ).
fof(f15396,plain,
! [X0,X1] : meet(join(X1,complement(X0)),join(X1,join(X1,X0))) = X1,
inference(forward_demodulation,[],[f15306,f5]) ).
fof(f15463,plain,
! [X0,X1] : meet(join(X1,complement(X0)),join(X1,X0)) = X1,
inference(forward_demodulation,[],[f15396,f24]) ).
fof(f15507,plain,
! [X0,X1] : meet(join(X1,X0),join(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f15463,f5]) ).
fof(f15623,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f4990,f13748]) ).
fof(f17496,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(X0)),
inference(superposition,[],[f13073,f5]) ).
fof(f19131,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(X1)),
inference(superposition,[],[f14881,f4990]) ).
fof(f19134,plain,
! [X2,X0,X1] : complement(meet(X2,meet(complement(X0),X1))) = join(join(complement(X1),X0),complement(X2)),
inference(superposition,[],[f14881,f13748]) ).
fof(f19143,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(meet(X0,X1),complement(X1)),
inference(superposition,[],[f14881,f12506]) ).
fof(f19146,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(meet(X1,X0),complement(X1)),
inference(superposition,[],[f14881,f12556]) ).
fof(f19321,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(X1),meet(X1,X0)),
inference(forward_demodulation,[],[f19146,f6]) ).
fof(f19324,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f19143,f6]) ).
fof(f19332,plain,
! [X2,X0,X1] : complement(meet(X2,meet(complement(X0),X1))) = join(complement(X1),join(X0,complement(X2))),
inference(forward_demodulation,[],[f19134,f8]) ).
fof(f19382,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X1,X0)),
inference(forward_demodulation,[],[f19321,f15623]) ).
fof(f19384,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f19324,f15623]) ).
fof(f19530,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X0,X1))) = join(complement(complement(X0)),complement(X1)),
inference(superposition,[],[f19384,f14122]) ).
fof(f19555,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,X0),X2)) = join(X2,join(complement(X0),X1)),
inference(superposition,[],[f63,f19384]) ).
fof(f19634,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(complement(complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f19530,f19131]) ).
fof(f19726,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = complement(meet(join(X0,X1),complement(X0))),
inference(forward_demodulation,[],[f19634,f19131]) ).
fof(f19805,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(X0))),
inference(forward_demodulation,[],[f19726,f14881]) ).
fof(f19863,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f19805,f14881]) ).
fof(f20270,plain,
! [X2,X0,X1] : complement(meet(X2,X0)) = complement(meet(join(X0,X1),meet(X2,X0))),
inference(superposition,[],[f11111,f19131]) ).
fof(f20407,plain,
! [X2,X0,X1] : complement(meet(X2,X0)) = complement(meet(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f20270,f46]) ).
fof(f20483,plain,
! [X2,X0] : complement(meet(X0,X2)) = complement(meet(X2,X0)),
inference(forward_demodulation,[],[f20407,f36]) ).
fof(f20648,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,join(meet(X0,X2),meet(X2,X1)))) = join(complement(X0),meet(X0,join(X1,meet(X2,X0)))),
inference(superposition,[],[f19382,f292]) ).
fof(f20655,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,join(X1,meet(X2,X0)))) = join(complement(X0),join(meet(X0,X2),X1)),
inference(superposition,[],[f19382,f6998]) ).
fof(f20681,plain,
! [X0,X1] : join(complement(join(X0,X1)),X0) = join(complement(join(X0,X1)),complement(meet(complement(X0),X1))),
inference(superposition,[],[f19382,f14681]) ).
fof(f20731,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),X1)) = join(complement(X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f63,f19382]) ).
fof(f20737,plain,
! [X2,X3,X0,X1] : meet(X2,join(complement(X0),join(meet(X3,join(complement(X0),X1)),meet(X2,X3)))) = meet(X2,join(complement(X0),meet(X3,join(X2,meet(X0,X1))))),
inference(superposition,[],[f119,f19382]) ).
fof(f20788,plain,
! [X2,X3,X0,X1] : meet(X2,join(complement(X0),meet(X3,join(X2,X1)))) = meet(X2,join(complement(X0),meet(X3,join(X2,meet(X0,X1))))),
inference(forward_demodulation,[],[f20737,f119]) ).
fof(f20834,plain,
! [X0,X1] : join(complement(join(X0,X1)),X0) = complement(meet(meet(complement(X0),X1),join(X0,X1))),
inference(forward_demodulation,[],[f20681,f19131]) ).
fof(f20859,plain,
! [X2,X0,X1] : join(X1,join(complement(X0),X2)) = join(complement(X0),meet(X0,join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f20655,f20731]) ).
fof(f20866,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,join(meet(X0,X2),meet(X2,X1)))) = join(complement(X0),join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f20648,f19382]) ).
fof(f20934,plain,
! [X0,X1] : join(complement(join(X0,X1)),X0) = complement(meet(join(X0,X1),meet(complement(X0),X1))),
inference(forward_demodulation,[],[f20834,f20483]) ).
fof(f20950,plain,
! [X2,X0,X1] : join(X1,join(complement(X0),X2)) = join(complement(X0),join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f20859,f19382]) ).
fof(f20952,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,meet(X0,X2))) = join(complement(X0),join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f20866,f667]) ).
fof(f20996,plain,
! [X0,X1] : join(complement(join(X0,X1)),X0) = join(complement(X1),join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f20934,f19332]) ).
fof(f21005,plain,
! [X2,X0,X1] : join(X1,join(complement(X0),X2)) = join(complement(X0),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f20952,f20950]) ).
fof(f21030,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(join(X0,X1)),X0),
inference(forward_demodulation,[],[f20996,f8513]) ).
fof(f21051,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f21030,f6]) ).
fof(f21129,plain,
! [X2,X0,X1] : join(complement(X1),join(X2,meet(complement(X0),X1))) = join(X2,join(complement(X1),complement(meet(X1,X0)))),
inference(superposition,[],[f21005,f12556]) ).
fof(f21177,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f13693,f21005]) ).
fof(f21282,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f21177,f13431]) ).
fof(f21317,plain,
! [X2,X0,X1] : join(X2,complement(meet(X1,X0))) = join(complement(X1),join(X2,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f21129,f8279]) ).
fof(f21427,plain,
! [X2,X0,X1] : join(X2,complement(meet(X1,X0))) = join(X2,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f21317,f20950]) ).
fof(f21498,plain,
! [X2,X0,X1] : join(X2,complement(meet(X1,X0))) = join(X2,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f21427,f19131]) ).
fof(f25221,plain,
! [X2,X0,X1] : join(X2,complement(complement(join(X0,X1)))) = join(X2,complement(meet(complement(X0),complement(X1)))),
inference(superposition,[],[f21498,f14122]) ).
fof(f25409,plain,
! [X2,X0,X1] : join(complement(complement(meet(X2,X1))),X0) = join(X0,complement(join(X0,complement(meet(X1,X2))))),
inference(superposition,[],[f21051,f21498]) ).
fof(f25449,plain,
! [X2,X0,X1] : join(complement(complement(meet(X2,X1))),X0) = join(X0,complement(complement(meet(X1,X2)))),
inference(forward_demodulation,[],[f25409,f19863]) ).
fof(f25571,plain,
! [X2,X0,X1] : join(X2,complement(complement(join(X0,X1)))) = join(X2,join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f25221,f14881]) ).
fof(f25596,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(complement(complement(meet(X2,X1))),X0),
inference(forward_demodulation,[],[f25449,f4990]) ).
fof(f25682,plain,
! [X2,X0,X1] : join(X2,join(X1,X0)) = join(X2,complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f25571,f4990]) ).
fof(f25698,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(forward_demodulation,[],[f25596,f4990]) ).
fof(f25764,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f25682,f4990]) ).
fof(f27409,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(superposition,[],[f6,f25698]) ).
fof(f28289,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(complement(X0),join(X1,X2))),
inference(superposition,[],[f13693,f25764]) ).
fof(f28295,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(X0,join(X2,X1)),
inference(forward_demodulation,[],[f28289,f13182]) ).
fof(f32378,plain,
! [X2,X0,X1] : complement(join(meet(X0,X1),complement(X2))) = meet(X2,complement(meet(X1,X0))),
inference(superposition,[],[f14225,f27409]) ).
fof(f32417,plain,
! [X2,X0,X1] : meet(X2,complement(meet(X0,X1))) = meet(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f32378,f14225]) ).
fof(f34314,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(complement(meet(X1,X0)),X0))) = meet(X0,join(X2,join(meet(X0,complement(X1)),meet(complement(meet(X1,X0)),X2)))),
inference(superposition,[],[f292,f17496]) ).
fof(f34407,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,complement(X1)))) = meet(X0,join(X2,meet(complement(meet(X1,X0)),X0))),
inference(forward_demodulation,[],[f34314,f667]) ).
fof(f34532,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,complement(X1)))) = meet(X0,join(X2,meet(X0,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f34407,f2210]) ).
fof(f34623,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,complement(X1)))) = meet(join(complement(meet(X1,X0)),X2),X0),
inference(forward_demodulation,[],[f34532,f21282]) ).
fof(f34685,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X1,X0)),X2)) = meet(X0,join(X2,meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f34623,f5]) ).
fof(f34730,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X1,X0)),X2)) = meet(join(complement(X1),X2),X0),
inference(forward_demodulation,[],[f34685,f21282]) ).
fof(f34976,plain,
! [X2,X0,X1] : meet(X2,join(complement(meet(X0,X2)),X1)) = meet(join(complement(X0),meet(X1,join(X2,meet(X0,X2)))),X2),
inference(superposition,[],[f3081,f34730]) ).
fof(f35162,plain,
! [X2,X0,X1] : meet(X2,join(complement(meet(X0,X2)),X1)) = meet(X2,join(complement(X0),meet(X1,join(X2,meet(X0,X2))))),
inference(forward_demodulation,[],[f34976,f5]) ).
fof(f35375,plain,
! [X2,X0,X1] : meet(X2,join(complement(meet(X0,X2)),X1)) = meet(X2,join(complement(X0),meet(X1,join(X2,X2)))),
inference(forward_demodulation,[],[f35162,f20788]) ).
fof(f35547,plain,
! [X2,X0,X1] : meet(X2,join(complement(meet(X0,X2)),X1)) = meet(X2,join(complement(X0),meet(X1,X2))),
inference(forward_demodulation,[],[f35375,f2]) ).
fof(f35683,plain,
! [X2,X0,X1] : meet(join(complement(X0),X1),X2) = meet(X2,join(complement(X0),meet(X1,X2))),
inference(forward_demodulation,[],[f35547,f34730]) ).
fof(f35907,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f35683,f4990]) ).
fof(f36678,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,join(meet(X2,X1),X0)),
inference(superposition,[],[f6998,f35907]) ).
fof(f44642,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),complement(meet(complement(join(meet(X2,X0),X1)),X0))),
inference(superposition,[],[f15060,f54]) ).
fof(f45075,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),complement(meet(X0,complement(join(meet(X2,X0),X1))))),
inference(forward_demodulation,[],[f44642,f32417]) ).
fof(f45262,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(join(meet(X2,X0),X1),complement(X0))),
inference(forward_demodulation,[],[f45075,f14881]) ).
fof(f45419,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(complement(X0),join(meet(X2,X0),X1))),
inference(forward_demodulation,[],[f45262,f13346]) ).
fof(f45551,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(X1,join(complement(X0),X2))),
inference(forward_demodulation,[],[f45419,f19555]) ).
fof(f51754,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(join(X0,complement(X1)),join(X0,X1)))) = meet(join(X0,X1),join(X2,join(X0,meet(join(X0,complement(X1)),X2)))),
inference(superposition,[],[f292,f15507]) ).
fof(f51844,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = meet(join(X0,X1),join(X2,meet(join(X0,complement(X1)),join(X0,X1)))),
inference(forward_demodulation,[],[f51754,f667]) ).
fof(f51967,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = meet(join(X0,X1),join(X2,meet(join(X0,X1),join(X0,complement(X1))))),
inference(forward_demodulation,[],[f51844,f2210]) ).
fof(f52039,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = meet(join(join(X0,complement(X1)),X2),join(X0,X1)),
inference(forward_demodulation,[],[f51967,f21282]) ).
fof(f52087,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = meet(join(X1,X0),join(join(X0,complement(X1)),X2)),
inference(forward_demodulation,[],[f52039,f28295]) ).
fof(f52122,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = meet(join(X1,X0),join(X0,join(complement(X1),X2))),
inference(forward_demodulation,[],[f52087,f8]) ).
fof(f52144,plain,
! [X2,X0,X1] : join(meet(X2,X1),X0) = meet(join(X0,X1),join(X2,X0)),
inference(forward_demodulation,[],[f52122,f45551]) ).
fof(f52245,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(join(meet(X0,X2),X1),X0),
inference(superposition,[],[f52144,f4]) ).
fof(f52601,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f52245,f5]) ).
fof(f52782,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f52601,f36678]) ).
fof(f53283,plain,
meet(a,join(b,c)) != meet(join(b,c),a),
inference(superposition,[],[f13,f52782]) ).
fof(f53489,plain,
$false,
inference(forward_subsumption_resolution,[],[f53283,f5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT199-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n017.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:01:05 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.01/2.56 % (2579008)Input is clausal, will run a generic CNF schedule.
% 13.01/2.56 % (2579080)dis-21_1_sil=8000:lcm=predicate:random_seed=1902535237: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)
% 13.01/2.56 % (2579080)Refutation not found, incomplete strategy
% 13.01/2.56 % (2579080)------------------------------
% 13.01/2.56 % (2579080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.56 % (2579080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.56 % (2579080)CaDiCaL version: 2.1.3
% 13.01/2.56 % (2579080)Termination reason: Refutation not found, incomplete strategy
% 13.01/2.56 % (2579080)Time elapsed: 0.001 s
% 13.01/2.56 % (2579080)Peak memory usage: 88 MB
% 13.01/2.56 % (2579080)Instructions burned: 1 (million)
% 13.01/2.56 % (2579079)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2252139929:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.01/2.56 % (2579074)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=1370406630:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.01/2.56 % (2579076)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=997201582:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.01/2.56 % (2579075)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4217863638:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.01/2.56 % (2579078)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=4098246847:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.01/2.56 % (2579077)lrs+10_1_sil=8000:sp=occurrence:random_seed=2046363671:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.01/2.56 % (2579078)Instruction limit reached!
% 13.01/2.56 % (2579078)------------------------------
% 13.01/2.56 % (2579078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.56 % (2579078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.56 % (2579078)CaDiCaL version: 2.1.3
% 13.01/2.56 % (2579078)Termination reason: Instruction limit
% 13.01/2.56 % (2579078)Termination phase: Saturation
% 13.01/2.56 % (2579078)Time elapsed: 0.069 s
% 13.01/2.56 % (2579078)Peak memory usage: 89 MB
% 13.01/2.56 % (2579078)Instructions burned: 114 (million)
% 13.01/2.56 % (2579077)Instruction limit reached!
% 13.01/2.56 % (2579077)------------------------------
% 13.01/2.56 % (2579077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.56 % (2579077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.56 % (2579077)CaDiCaL version: 2.1.3
% 13.01/2.56 % (2579077)Termination reason: Instruction limit
% 13.01/2.56 % (2579077)Termination phase: Saturation
% 13.01/2.56 % (2579077)Time elapsed: 0.064 s
% 13.01/2.56 % (2579077)Peak memory usage: 88 MB
% 13.01/2.56 % (2579077)Instructions burned: 108 (million)
% 13.01/2.56 % (2579079)Instruction limit reached!
% 13.01/2.56 % (2579079)------------------------------
% 13.01/2.56 % (2579079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.56 % (2579079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.56 % (2579079)CaDiCaL version: 2.1.3
% 13.01/2.56 % (2579079)Termination reason: Instruction limit
% 13.01/2.56 % (2579079)Termination phase: Saturation
% 13.01/2.56 % (2579079)Time elapsed: 0.099 s
% 13.01/2.56 % (2579079)Peak memory usage: 89 MB
% 13.01/2.56 % (2579079)Instructions burned: 181 (million)
% 13.01/2.56 % (2579080)------------------------------
% 13.01/2.56 % (2579080)------------------------------
% 13.01/2.56 % (2579107)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=4027008336:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 13.01/2.56 % (2579107)Refutation not found, incomplete strategy
% 13.01/2.56 % (2579107)------------------------------
% 13.01/2.56 % (2579107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.56 % (2579107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.56 % (2579107)CaDiCaL version: 2.1.3
% 13.01/2.56 % (2579107)Termination reason: Refutation not found, incomplete strategy
% 13.01/2.56 % (2579107)Time elapsed: 0.002 s
% 13.01/2.56 % (2579107)Peak memory usage: 88 MB
% 33.08/5.38 % (2579108)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1390555654:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 33.08/5.38 % (2579110)lrs+10_64_to=lpo:sil=8000:random_seed=1226646181:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 33.08/5.38 % (2579108)Refutation not found, incomplete strategy
% 33.08/5.38 % (2579108)------------------------------
% 33.08/5.38 % (2579108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.08/5.38 % (2579108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.08/5.38 % (2579108)CaDiCaL version: 2.1.3
% 33.08/5.38 % (2579108)Termination reason: Refutation not found, incomplete strategy
% 33.08/5.38 % (2579108)Time elapsed: 0.002 s
% 33.08/5.38 % (2579108)Peak memory usage: 88 MB
% 33.08/5.38 % (2579108)Instructions burned: 1 (million)
% 33.08/5.38 % (2579109)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3657794607:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 33.08/5.38 % (2579109)Refutation not found, incomplete strategy
% 33.08/5.38 % (2579109)------------------------------
% 33.08/5.38 % (2579109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.08/5.38 % (2579109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.08/5.38 % (2579109)CaDiCaL version: 2.1.3
% 33.08/5.38 % (2579109)Termination reason: Refutation not found, incomplete strategy
% 33.08/5.38 % (2579109)Time elapsed: 0.001 s
% 33.08/5.38 % (2579109)Peak memory usage: 88 MB
% 33.08/5.38 % (2579110)Instruction limit reached!
% 33.08/5.38 % (2579110)------------------------------
% 33.08/5.38 % (2579110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.08/5.38 % (2579110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.08/5.38 % (2579110)CaDiCaL version: 2.1.3
% 33.08/5.38 % (2579110)Termination reason: Instruction limit
% 33.08/5.38 % (2579110)Termination phase: Saturation
% 33.08/5.38 % (2579110)Time elapsed: 0.040 s
% 33.08/5.38 % (2579110)Peak memory usage: 88 MB
% 33.08/5.38 % (2579110)Instructions burned: 130 (million)
% 33.08/5.38 % (2579128)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=691043443:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 33.08/5.38 % (2579128)Instruction limit reached!
% 33.08/5.38 % (2579128)------------------------------
% 33.08/5.38 % (2579128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.08/5.38 % (2579128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.08/5.38 % (2579128)CaDiCaL version: 2.1.3
% 33.08/5.38 % (2579128)Termination reason: Instruction limit
% 33.08/5.38 % (2579128)Termination phase: Saturation
% 33.08/5.38 % (2579128)Time elapsed: 0.064 s
% 33.08/5.38 % (2579128)Peak memory usage: 90 MB
% 33.08/5.38 % (2579128)Instructions burned: 196 (million)
% 33.08/5.38 % (2579107)------------------------------
% 33.08/5.38 % (2579107)------------------------------
% 33.08/5.38 % (2579108)------------------------------
% 33.08/5.38 % (2579108)------------------------------
% 33.08/5.38 % (2579109)------------------------------
% 33.08/5.38 % (2579109)------------------------------
% 33.08/5.38 % (2579130)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1770058366:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 33.08/5.38 % (2579131)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1242128777:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 33.08/5.38 % (2579132)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=3349072874:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 33.08/5.38 % (2579130)Instruction limit reached!
% 33.08/5.38 % (2579130)------------------------------
% 33.08/5.38 % (2579130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.08/5.38 % (2579130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.08/5.38 % (2579130)CaDiCaL version: 2.1.3
% 33.08/5.38 % (2579130)Termination reason: Instruction limit
% 33.08/5.38 % (2579130)Termination phase: Saturation
% 33.08/5.38 % (2579130)Time elapsed: 0.053 s
% 33.08/5.38 % (2579130)Peak memory usage: 90 MB
% 33.08/5.38 % (2579130)Instructions burned: 158 (million)
% 33.08/5.38 % (2579133)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2142049522:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 36.19/5.85 % (2579133)Refutation not found, incomplete strategy
% 36.19/5.85 % (2579133)------------------------------
% 36.19/5.85 % (2579133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579133)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579133)Termination reason: Refutation not found, incomplete strategy
% 36.19/5.85 % (2579133)Time elapsed: 0.001 s
% 36.19/5.85 % (2579133)Peak memory usage: 87 MB
% 36.19/5.85 % (2579132)Instruction limit reached!
% 36.19/5.85 % (2579132)------------------------------
% 36.19/5.85 % (2579132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579132)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579132)Termination reason: Instruction limit
% 36.19/5.85 % (2579132)Termination phase: Saturation
% 36.19/5.85 % (2579132)Time elapsed: 0.067 s
% 36.19/5.85 % (2579132)Peak memory usage: 89 MB
% 36.19/5.85 % (2579132)Instructions burned: 107 (million)
% 36.19/5.85 % (2579137)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1373845087:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 36.19/5.85 % (2579137)Instruction limit reached!
% 36.19/5.85 % (2579137)------------------------------
% 36.19/5.85 % (2579137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579137)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579137)Termination reason: Instruction limit
% 36.19/5.85 % (2579137)Termination phase: Saturation
% 36.19/5.85 % (2579137)Time elapsed: 0.075 s
% 36.19/5.85 % (2579137)Peak memory usage: 90 MB
% 36.19/5.85 % (2579137)Instructions burned: 242 (million)
% 36.19/5.85 % (2579139)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3172729937:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 36.19/5.85 % (2579133)------------------------------
% 36.19/5.85 % (2579133)------------------------------
% 36.19/5.85 % (2579141)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3578375509:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 36.19/5.85 % (2579141)Instruction limit reached!
% 36.19/5.85 % (2579141)------------------------------
% 36.19/5.85 % (2579141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579141)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579141)Termination reason: Instruction limit
% 36.19/5.85 % (2579141)Termination phase: Saturation
% 36.19/5.85 % (2579141)Time elapsed: 0.071 s
% 36.19/5.85 % (2579141)Peak memory usage: 89 MB
% 36.19/5.85 % (2579141)Instructions burned: 135 (million)
% 36.19/5.85 % (2579151)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2780303243:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 36.19/5.85 % (2579160)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3380855136:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 36.19/5.85 % (2579160)Instruction limit reached!
% 36.19/5.85 % (2579160)------------------------------
% 36.19/5.85 % (2579160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579160)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579160)Termination reason: Instruction limit
% 36.19/5.85 % (2579160)Termination phase: Saturation
% 36.19/5.85 % (2579160)Time elapsed: 0.103 s
% 36.19/5.85 % (2579160)Peak memory usage: 91 MB
% 36.19/5.85 % (2579160)Instructions burned: 191 (million)
% 36.19/5.85 % (2579168)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=721359192:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 36.19/5.85 % (2579151)Instruction limit reached!
% 36.19/5.85 % (2579151)------------------------------
% 36.19/5.85 % (2579151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579151)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579151)Termination reason: Instruction limit
% 36.19/5.85 % (2579151)Termination phase: Saturation
% 36.19/5.85 % (2579151)Time elapsed: 0.506 s
% 36.19/5.85 % (2579151)Peak memory usage: 94 MB
% 36.19/5.85 % (2579151)Instructions burned: 499 (million)
% 36.19/5.85 % (2579168)Instruction limit reached!
% 36.19/5.85 % (2579168)------------------------------
% 36.19/5.85 % (2579168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579168)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579168)Termination reason: Instruction limit
% 36.19/5.85 % (2579168)Termination phase: Saturation
% 36.19/5.85 % (2579168)Time elapsed: 0.143 s
% 36.19/5.85 % (2579168)Peak memory usage: 91 MB
% 36.19/5.85 % (2579168)Instructions burned: 265 (million)
% 36.19/5.85 % (2579175)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2665580462:cond=on:i=156:bs=on:gtg=exists_all:er=known_2980 on theBenchmark for (2980ds/156Mi)
% 36.19/5.85 % (2579178)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=4154450884:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 36.19/5.85 % (2579175)Instruction limit reached!
% 36.19/5.85 % (2579175)------------------------------
% 36.19/5.85 % (2579175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579175)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579175)Termination reason: Instruction limit
% 36.19/5.85 % (2579175)Termination phase: Saturation
% 36.19/5.85 % (2579175)Time elapsed: 0.142 s
% 36.19/5.85 % (2579175)Peak memory usage: 89 MB
% 36.19/5.85 % (2579175)Instructions burned: 157 (million)
% 36.19/5.85 % (2579187)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=809848138:i=537:av=off:ss=included_2976 on theBenchmark for (2976ds/537Mi)
% 36.19/5.85 % (2579187)Instruction limit reached!
% 36.19/5.85 % (2579187)------------------------------
% 36.19/5.85 % (2579187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579187)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579187)Termination reason: Instruction limit
% 36.19/5.85 % (2579187)Termination phase: Saturation
% 36.19/5.85 % (2579187)Time elapsed: 0.371 s
% 36.19/5.85 % (2579187)Peak memory usage: 93 MB
% 36.19/5.85 % (2579187)Instructions burned: 538 (million)
% 36.19/5.85 % (2579198)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3982392042:i=180:bd=preordered:av=off_2969 on theBenchmark for (2969ds/180Mi)
% 36.19/5.85 % (2579198)Instruction limit reached!
% 36.19/5.85 % (2579198)------------------------------
% 36.19/5.85 % (2579198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579198)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579198)Termination reason: Instruction limit
% 36.19/5.85 % (2579198)Termination phase: Saturation
% 36.19/5.85 % (2579198)Time elapsed: 0.158 s
% 36.19/5.85 % (2579198)Peak memory usage: 88 MB
% 36.19/5.85 % (2579198)Instructions burned: 181 (million)
% 36.19/5.85 % (2579202)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=4169549773:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2965 on theBenchmark for (2965ds/10307Mi)
% 36.19/5.85 % (2579131)Instruction limit reached!
% 36.19/5.85 % (2579131)------------------------------
% 36.19/5.85 % (2579131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579131)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579131)Termination reason: Instruction limit
% 36.19/5.85 % (2579131)Termination phase: Saturation
% 36.19/5.85 % (2579131)Time elapsed: 3.256 s
% 36.19/5.85 % (2579131)Peak memory usage: 152 MB
% 36.19/5.85 % (2579131)Instructions burned: 3395 (million)
% 36.19/5.85 % (2579210)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=1627443068:i=412:gtgl=4:gtg=exists_all_2959 on theBenchmark for (2959ds/412Mi)
% 36.19/5.85 % (2579210)Instruction limit reached!
% 36.19/5.85 % (2579210)------------------------------
% 36.19/5.85 % (2579210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.19/5.85 % (2579210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.19/5.85 % (2579210)CaDiCaL version: 2.1.3
% 36.19/5.85 % (2579210)Termination reason: Instruction limit
% 36.19/5.85 % (2579210)Termination phase: Saturation
% 36.19/5.85 % (2579210)Time elapsed: 0.408 s
% 36.19/5.85 % (2579210)Peak memory usage: 94 MB
% 36.19/5.85 % (2579210)Instructions burned: 412 (million)
% 36.19/5.85 % (2579075)First to succeed.
% 36.19/5.85 % (2579075)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2579008"
% 36.19/5.85 % (2579214)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=1263133049:s2pl=no:i=8478:s2at=4:nm=6_2952 on theBenchmark for (2952ds/8478Mi)
% 36.19/5.85 % (2579075)Refutation found. Thanks to Tanya!
% 36.19/5.85 % SZS status Unsatisfiable for theBenchmark
% 36.19/5.85 % SZS output start Proof for theBenchmark
% See solution above
% 37.11/6.08 % (2579075)------------------------------
% 37.11/6.08 % (2579075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.11/6.08 % (2579075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.11/6.08 % (2579075)CaDiCaL version: 2.1.3
% 37.11/6.08 % (2579075)Termination reason: Refutation
% 37.11/6.08 % (2579075)Time elapsed: 4.611 s
% 37.11/6.08 % (2579075)Peak memory usage: 166 MB
% 37.11/6.08 % (2579075)Instructions burned: 5156 (million)
% 37.11/6.08 % (2579075)------------------------------
% 37.11/6.08 % (2579075)------------------------------
% 37.11/6.08 % (2579008)Success in time 5.204 s
% 37.11/6.08 % Vampire exiting
%------------------------------------------------------------------------------