%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT202-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:14 AM UTC 2026
% Result : Unsatisfiable 30.21s 6.62s
% Output : Refutation 38.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 79
% Number of leaves : 11
% Syntax : Number of formulae : 281 ( 266 unt; 0 def)
% Number of atoms : 299 ( 298 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 38 ( 20 ~; 18 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 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 : 643 ( 643 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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,X0,X1] : join(X0,meet(X1,join(X0,X2))) = join(X0,meet(X1,join(X2,meet(X0,join(X2,X1))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H55) ).
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,
! [X2,X0,X1] : join(X1,meet(meet(X0,X2),join(X1,X0))) = join(X1,meet(meet(X0,X2),join(X0,meet(X1,X0)))),
inference(superposition,[],[f12,f4]) ).
fof(f25,plain,
! [X2,X0,X1] : join(X2,meet(X1,join(X2,X0))) = join(X2,meet(X1,join(X0,meet(join(X0,X1),X2)))),
inference(superposition,[],[f12,f5]) ).
fof(f34,plain,
! [X2,X0,X1] : join(X1,meet(meet(X0,X2),join(X1,X0))) = join(X1,meet(X0,meet(X2,join(X0,meet(X1,X0))))),
inference(forward_demodulation,[],[f22,f7]) ).
fof(f37,plain,
! [X2,X0,X1] : join(X1,meet(meet(X0,X2),join(X1,X0))) = join(X1,meet(X0,meet(X2,X0))),
inference(forward_demodulation,[],[f34,f17]) ).
fof(f39,plain,
! [X2,X0,X1] : join(X1,meet(X0,meet(X2,X0))) = join(X1,meet(X0,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f37,f7]) ).
fof(f83,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f84,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f85,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f15]) ).
fof(f91,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f93,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f97,plain,
! [X2,X3,X0,X1] : join(X3,meet(meet(X0,X1),join(X3,X2))) = join(X3,meet(X0,meet(X1,join(X2,meet(X3,join(X2,meet(X0,X1))))))),
inference(superposition,[],[f12,f7]) ).
fof(f101,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,join(X2,meet(X3,join(X2,meet(X0,X1))))))) = join(X3,meet(X0,meet(X1,join(X3,X2)))),
inference(forward_demodulation,[],[f97,f7]) ).
fof(f106,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f17,f3]) ).
fof(f107,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f17,f15]) ).
fof(f110,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f15,f17]) ).
fof(f114,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f110,f5]) ).
fof(f115,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f107,f6]) ).
fof(f116,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f106,f6]) ).
fof(f121,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f124,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f17]) ).
fof(f134,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f139,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X2,join(X0,X1)))) = join(X2,meet(X3,join(X0,join(X1,meet(X2,join(join(X0,X1),X3)))))),
inference(superposition,[],[f12,f8]) ).
fof(f146,plain,
! [X2,X3,X0,X1] : join(X2,meet(X3,join(X2,join(X0,X1)))) = join(X2,meet(X3,join(X0,join(X1,meet(X2,join(X0,join(X1,X3))))))),
inference(forward_demodulation,[],[f139,f8]) ).
fof(f164,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f121,f6]) ).
fof(f194,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f199,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f208,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(one,X1)),
inference(superposition,[],[f84,f9]) ).
fof(f234,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f235,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f236,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f253,plain,
! [X0,X1] : join(complement(join(X0,X1)),meet(X1,join(complement(join(X0,X1)),X0))) = join(complement(join(X0,X1)),meet(X1,join(X0,zero))),
inference(superposition,[],[f25,f10]) ).
fof(f285,plain,
! [X0,X1] : join(complement(join(X0,X1)),meet(X1,join(complement(join(X0,X1)),X0))) = join(complement(join(X0,X1)),meet(X1,X0)),
inference(forward_demodulation,[],[f253,f235]) ).
fof(f302,plain,
! [X0,X1] : join(complement(join(X0,X1)),meet(X1,join(complement(join(X0,X1)),X0))) = join(meet(X1,X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f285,f6]) ).
fof(f315,plain,
! [X0,X1] : join(meet(X1,X0),complement(join(X0,X1))) = join(complement(join(X0,X1)),meet(X1,join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f302,f6]) ).
fof(f355,plain,
! [X0,X1] : meet(X0,join(X1,complement(join(X1,X0)))) = meet(meet(X0,join(X1,complement(join(X1,X0)))),join(meet(X0,X1),complement(join(X1,X0)))),
inference(superposition,[],[f15,f315]) ).
fof(f360,plain,
! [X0,X1] : meet(X0,join(X1,complement(join(X1,X0)))) = meet(join(meet(X0,X1),complement(join(X1,X0))),meet(X0,join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f355,f5]) ).
fof(f376,plain,
! [X0,X1] : meet(X0,join(X1,complement(join(X1,X0)))) = meet(join(X1,complement(join(X1,X0))),meet(join(meet(X0,X1),complement(join(X1,X0))),X0)),
inference(forward_demodulation,[],[f360,f93]) ).
fof(f387,plain,
! [X0,X1] : meet(X0,join(X1,complement(join(X1,X0)))) = meet(X0,meet(join(X1,complement(join(X1,X0))),join(meet(X0,X1),complement(join(X1,X0))))),
inference(forward_demodulation,[],[f376,f93]) ).
fof(f424,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f194]) ).
fof(f428,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f194]) ).
fof(f444,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f424]) ).
fof(f500,plain,
! [X0,X1] : join(X1,meet(one,join(X1,X0))) = join(X1,join(X0,meet(join(X0,one),X1))),
inference(superposition,[],[f25,f428]) ).
fof(f502,plain,
zero = complement(one),
inference(superposition,[],[f10,f428]) ).
fof(f504,plain,
! [X0,X1] : join(X1,meet(one,join(X1,X0))) = join(X1,join(X0,meet(one,X1))),
inference(forward_demodulation,[],[f500,f444]) ).
fof(f511,plain,
! [X0,X1] : join(X1,meet(one,join(X1,X0))) = join(X1,join(X0,X1)),
inference(forward_demodulation,[],[f504,f428]) ).
fof(f515,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(one,join(X1,X0))),
inference(forward_demodulation,[],[f511,f115]) ).
fof(f517,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X1,X0)),
inference(forward_demodulation,[],[f515,f428]) ).
fof(f606,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f235]) ).
fof(f610,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f15,f235]) ).
fof(f636,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f5,f610]) ).
fof(f790,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f236,f5]) ).
fof(f985,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f124,f3]) ).
fof(f1039,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f985,f134]) ).
fof(f1049,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f1039,f8]) ).
fof(f1128,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f85,f5]) ).
fof(f1132,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X3,X0)) = meet(X2,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f85,f93]) ).
fof(f1136,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f85,f10]) ).
fof(f1176,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f1136,f636]) ).
fof(f1278,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,f199]) ).
fof(f1291,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1278]) ).
fof(f1340,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f1291,f6]) ).
fof(f1549,plain,
! [X2,X0,X1] : meet(X1,meet(zero,X0)) = meet(X1,meet(complement(join(X1,X2)),X0)),
inference(superposition,[],[f84,f234]) ).
fof(f1552,plain,
! [X2,X0,X1] : meet(X1,zero) = meet(X1,meet(complement(join(X1,X2)),X0)),
inference(forward_demodulation,[],[f1549,f610]) ).
fof(f1583,plain,
! [X2,X0,X1] : zero = meet(X1,meet(complement(join(X1,X2)),X0)),
inference(forward_demodulation,[],[f1552,f636]) ).
fof(f2500,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f15,f517]) ).
fof(f2718,plain,
! [X0,X1] : zero = meet(join(X1,X0),complement(join(X0,X1))),
inference(superposition,[],[f1176,f517]) ).
fof(f2750,plain,
! [X0,X1] : meet(X0,join(complement(join(X1,X0)),complement(join(complement(join(X1,X0)),X0)))) = meet(X0,meet(join(complement(join(X1,X0)),complement(join(complement(join(X1,X0)),X0))),join(zero,complement(join(complement(join(X1,X0)),X0))))),
inference(superposition,[],[f387,f1176]) ).
fof(f2768,plain,
! [X0,X1] : meet(X0,join(complement(join(X1,X0)),complement(join(complement(join(X1,X0)),X0)))) = meet(X0,meet(join(zero,complement(join(complement(join(X1,X0)),X0))),join(complement(join(X1,X0)),complement(join(complement(join(X1,X0)),X0))))),
inference(forward_demodulation,[],[f2750,f5]) ).
fof(f2793,plain,
! [X0,X1] : meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))) = meet(X0,meet(join(zero,complement(join(X0,complement(join(X1,X0))))),join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f2768,f6]) ).
fof(f2804,plain,
! [X0,X1] : meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))) = meet(X0,meet(complement(join(X0,complement(join(X1,X0)))),join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f2793,f606]) ).
fof(f2807,plain,
! [X0,X1] : zero = meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f2804,f1583]) ).
fof(f4061,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(join(X1,X0),join(join(X0,X1),X2)),
inference(superposition,[],[f124,f2500]) ).
fof(f4072,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X1,join(X0,join(join(X0,X1),X2))),
inference(forward_demodulation,[],[f4061,f8]) ).
fof(f4118,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X1,join(X0,join(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f4072,f8]) ).
fof(f4158,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X1,join(X0,join(X1,X2))),
inference(forward_demodulation,[],[f4118,f116]) ).
fof(f4178,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X1,join(X2,X0)),
inference(forward_demodulation,[],[f4158,f1049]) ).
fof(f4199,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(superposition,[],[f1340,f9]) ).
fof(f4234,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4199,f502]) ).
fof(f4259,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4234,f235]) ).
fof(f4273,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f4259,f5]) ).
fof(f4282,plain,
! [X0] : join(X0,complement(one)) = complement(complement(X0)),
inference(forward_subsumption_resolution,[],[f4273,f10]) ).
fof(f4289,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f4282,f502]) ).
fof(f4294,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f4289,f235]) ).
fof(f5694,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X2,meet(X1,X0)))),
inference(superposition,[],[f15,f83]) ).
fof(f5868,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X0,meet(X1,X0))),
inference(superposition,[],[f39,f1128]) ).
fof(f5886,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X1,meet(X2,join(X0,X1))),X3)) = join(join(X0,meet(X1,meet(X2,X1))),X3),
inference(superposition,[],[f8,f39]) ).
fof(f5889,plain,
! [X2,X0,X1] : meet(X1,meet(X2,join(X0,X1))) = meet(meet(X1,meet(X2,join(X0,X1))),join(X0,meet(X1,meet(X2,X1)))),
inference(superposition,[],[f15,f39]) ).
fof(f5948,plain,
! [X2,X0,X1] : meet(X1,meet(X2,join(X0,X1))) = meet(join(X0,meet(X1,meet(X2,X1))),meet(X1,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f5889,f5]) ).
fof(f5951,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X1,meet(X2,join(X0,X1))),X3)) = join(X0,join(meet(X1,meet(X2,X1)),X3)),
inference(forward_demodulation,[],[f5886,f8]) ).
fof(f5964,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f5868,f114]) ).
fof(f6032,plain,
! [X2,X0,X1] : meet(X1,meet(X2,join(X0,X1))) = meet(meet(X2,join(X0,X1)),meet(join(X0,meet(X1,meet(X2,X1))),X1)),
inference(forward_demodulation,[],[f5948,f93]) ).
fof(f6035,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X2,X1),X3)) = join(X0,join(meet(X1,meet(X2,join(X0,X1))),X3)),
inference(forward_demodulation,[],[f5951,f114]) ).
fof(f6104,plain,
! [X2,X0,X1] : meet(X1,meet(X2,join(X0,X1))) = meet(X1,meet(meet(X2,join(X0,X1)),join(X0,meet(X1,meet(X2,X1))))),
inference(forward_demodulation,[],[f6032,f93]) ).
fof(f6107,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X1,X2),X3)) = join(X0,join(meet(X2,X1),X3)),
inference(forward_demodulation,[],[f6035,f1128]) ).
fof(f6149,plain,
! [X2,X0,X1] : meet(X1,meet(X2,join(X0,X1))) = meet(X1,meet(X2,meet(join(X0,X1),join(X0,meet(X1,meet(X2,X1)))))),
inference(forward_demodulation,[],[f6104,f7]) ).
fof(f6172,plain,
! [X2,X0,X1] : meet(X1,meet(X2,join(X0,X1))) = meet(X1,meet(join(X0,meet(X1,meet(X2,X1))),X2)),
inference(forward_demodulation,[],[f6149,f1132]) ).
fof(f6190,plain,
! [X2,X0,X1] : meet(X1,meet(X2,join(X0,X1))) = meet(X1,meet(X2,join(X0,meet(X1,meet(X2,X1))))),
inference(forward_demodulation,[],[f6172,f5]) ).
fof(f6205,plain,
! [X2,X0,X1] : meet(X1,meet(X2,join(X0,X1))) = meet(X1,meet(X2,join(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f6190,f114]) ).
fof(f6216,plain,
! [X2,X0,X1] : meet(X2,X1) = meet(X1,meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f6205,f5694]) ).
fof(f6263,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f5964,f2500]) ).
fof(f6335,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f5964]) ).
fof(f6416,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f6263,f2500]) ).
fof(f6935,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(zero,join(meet(X0,X1),X2)),
inference(superposition,[],[f606,f6107]) ).
fof(f6936,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(forward_demodulation,[],[f6935,f606]) ).
fof(f7336,plain,
! [X2,X0,X1] : meet(X1,X0) = join(meet(X0,X1),meet(X2,meet(X1,X0))),
inference(superposition,[],[f17,f6936]) ).
fof(f7338,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X1,X0),meet(X3,X2)),
inference(superposition,[],[f5964,f6936]) ).
fof(f7367,plain,
! [X0,X1] : one = join(meet(X0,X1),complement(meet(X1,X0))),
inference(superposition,[],[f9,f6936]) ).
fof(f8579,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X0,meet(X2,join(X0,X1))),
inference(superposition,[],[f6216,f6]) ).
fof(f8825,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(one,X1))),
inference(superposition,[],[f208,f93]) ).
fof(f8969,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f8825,f208]) ).
fof(f9057,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f8969,f2500]) ).
fof(f9258,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,X1)),
inference(forward_demodulation,[],[f9057,f2500]) ).
fof(f9431,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f9258]) ).
fof(f9452,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,X2))) = join(X3,meet(join(X2,X1),X0)),
inference(superposition,[],[f5964,f9258]) ).
fof(f9455,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,X2))) = join(meet(join(X2,X1),X0),X3),
inference(superposition,[],[f6335,f9258]) ).
fof(f9666,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f5,f9431]) ).
fof(f11295,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(join(X2,X0),X1),meet(X0,X1)),
inference(superposition,[],[f7336,f1128]) ).
fof(f11402,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X1,X0),meet(join(X2,X0),X1)),
inference(forward_demodulation,[],[f11295,f6335]) ).
fof(f11950,plain,
! [X0,X1] :
( one != one
| zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(superposition,[],[f11,f7367]) ).
fof(f11984,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f11950]) ).
fof(f12010,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f11984,f7]) ).
fof(f12083,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f12010,f790]) ).
fof(f12276,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f12083,f2500]) ).
fof(f12338,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f12276,f2500]) ).
fof(f19481,plain,
! [X2,X0,X1] : join(X0,meet(complement(X1),join(X0,join(X2,X1)))) = join(X0,meet(complement(X1),join(X2,join(X1,meet(X0,join(X2,one)))))),
inference(superposition,[],[f146,f9]) ).
fof(f19804,plain,
! [X2,X0,X1] : join(X0,meet(complement(X1),join(X0,join(X2,X1)))) = join(X0,meet(complement(X1),join(X2,join(X1,meet(X0,one))))),
inference(forward_demodulation,[],[f19481,f444]) ).
fof(f19924,plain,
! [X2,X0,X1] : join(X0,meet(complement(X1),join(X0,join(X2,X1)))) = join(X0,meet(complement(X1),join(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f19804,f194]) ).
fof(f23370,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))) ),
inference(superposition,[],[f1291,f2807]) ).
fof(f23434,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))),
inference(trivial_inequality_removal,[],[f23370]) ).
fof(f23855,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f3,f23434]) ).
fof(f23866,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f116,f23434]) ).
fof(f23949,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f23866,f6]) ).
fof(f23956,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f23855,f5]) ).
fof(f24184,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f23949,f4]) ).
fof(f24185,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f23949,f17]) ).
fof(f24254,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f23949,f12338]) ).
fof(f24392,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f24185,f6]) ).
fof(f24393,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f24184,f6]) ).
fof(f24595,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(X0),join(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f4178,f24393]) ).
fof(f24827,plain,
! [X2,X0,X1] : meet(complement(X1),meet(X2,complement(meet(X0,X1)))) = meet(X2,complement(X1)),
inference(superposition,[],[f8579,f24392]) ).
fof(f25058,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f23956,f12338]) ).
fof(f25477,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f24254,f4294]) ).
fof(f25848,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f15,f25477]) ).
fof(f25962,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f25848,f5]) ).
fof(f26142,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f91,f25962]) ).
fof(f26820,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f26142,f23956]) ).
fof(f27150,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),complement(join(complement(X1),complement(X0)))),
inference(superposition,[],[f26820,f4294]) ).
fof(f27949,plain,
! [X0,X1] : complement(complement(join(complement(X1),complement(X0)))) = join(complement(complement(join(complement(X1),complement(X0)))),complement(meet(X0,X1))),
inference(superposition,[],[f23949,f27150]) ).
fof(f27953,plain,
! [X0,X1] : complement(complement(join(complement(X1),complement(X0)))) = join(complement(meet(X0,X1)),complement(complement(join(complement(X1),complement(X0))))),
inference(forward_demodulation,[],[f27949,f6]) ).
fof(f28037,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X0,X1)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f27953,f4294]) ).
fof(f28096,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(meet(X0,X1)),complement(X1))),
inference(forward_demodulation,[],[f28037,f134]) ).
fof(f28139,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f28096,f6416]) ).
fof(f28173,plain,
! [X0,X1] : join(complement(meet(X0,X1)),complement(X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f28139,f24595]) ).
fof(f28200,plain,
! [X0,X1] : join(complement(X1),complement(meet(X0,X1))) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f28173,f6]) ).
fof(f28219,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f28200,f24392]) ).
fof(f28242,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(X1,complement(X0))),
inference(superposition,[],[f28219,f4294]) ).
fof(f28249,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(X1),X0),
inference(superposition,[],[f28219,f4294]) ).
fof(f28368,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X0,X1))),complement(join(complement(X0),complement(complement(meet(X0,X1)))))),
inference(superposition,[],[f23434,f28219]) ).
fof(f28375,plain,
! [X0,X1] : complement(complement(X0)) = complement(meet(join(complement(X0),complement(complement(meet(X0,X1)))),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f28368,f28219]) ).
fof(f28475,plain,
! [X0,X1] : complement(complement(X0)) = complement(meet(complement(meet(X0,X1)),join(complement(X0),complement(complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f28375,f12083]) ).
fof(f28529,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(join(complement(X0),complement(complement(meet(X0,X1))))),meet(X0,X1)),
inference(forward_demodulation,[],[f28475,f28249]) ).
fof(f28562,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X1,X0),complement(join(complement(X0),complement(complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f28529,f6335]) ).
fof(f28585,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X1,X0),complement(complement(meet(complement(meet(X0,X1)),X0)))),
inference(forward_demodulation,[],[f28562,f28219]) ).
fof(f28603,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X1,X0),meet(complement(meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f28585,f4294]) ).
fof(f28614,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f28603,f5964]) ).
fof(f28620,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f28614,f4294]) ).
fof(f28661,plain,
! [X2,X0,X1] : join(complement(join(X1,X0)),X2) = complement(meet(join(X0,X1),complement(X2))),
inference(superposition,[],[f28249,f9431]) ).
fof(f28685,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f12083,f28249]) ).
fof(f28701,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(superposition,[],[f4294,f28249]) ).
fof(f28762,plain,
! [X2,X0,X1] : join(complement(join(X1,X0)),X2) = join(X2,complement(join(X0,X1))),
inference(forward_demodulation,[],[f28661,f28242]) ).
fof(f28922,plain,
! [X2,X0,X1] : join(X2,complement(join(X1,X0))) = complement(meet(join(X0,X1),complement(X2))),
inference(superposition,[],[f28242,f9666]) ).
fof(f28959,plain,
! [X0,X1] : meet(X1,complement(X0)) = complement(join(X0,complement(X1))),
inference(superposition,[],[f4294,f28242]) ).
fof(f29022,plain,
! [X2,X0,X1] : join(X2,complement(join(X1,X0))) = join(X2,complement(join(X0,X1))),
inference(forward_demodulation,[],[f28922,f28242]) ).
fof(f29480,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f28701,f4294]) ).
fof(f29487,plain,
! [X0,X1] : complement(complement(X0)) = meet(complement(complement(join(X0,complement(join(X1,X0))))),join(X1,X0)),
inference(superposition,[],[f28701,f23434]) ).
fof(f29525,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),X2) = complement(join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f28701,f134]) ).
fof(f29706,plain,
! [X0,X1] : complement(complement(X0)) = meet(join(X1,X0),complement(complement(join(X0,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f29487,f5]) ).
fof(f29781,plain,
! [X0,X1] : complement(complement(X0)) = meet(join(X1,X0),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f29706,f4294]) ).
fof(f29826,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f29781,f4294]) ).
fof(f31869,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X1,X0)))),
inference(superposition,[],[f84,f29826]) ).
fof(f33880,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f121,f28620]) ).
fof(f34686,plain,
! [X0,X1] :
( zero != meet(X0,join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1))))
| complement(X0) = join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1))) ),
inference(superposition,[],[f1291,f33880]) ).
fof(f34713,plain,
! [X0,X1] : meet(X0,meet(X1,complement(meet(X1,X0)))) = meet(X0,join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1)))),
inference(superposition,[],[f31869,f33880]) ).
fof(f34753,plain,
! [X0,X1] : meet(X0,meet(X1,complement(meet(X1,X0)))) = meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f34713,f9258]) ).
fof(f34775,plain,
! [X0,X1] :
( zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X1,X0)))))
| complement(X0) = join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1))) ),
inference(forward_demodulation,[],[f34686,f9258]) ).
fof(f34867,plain,
! [X0,X1] : zero = meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f34753,f790]) ).
fof(f34883,plain,
! [X0,X1] :
( complement(X0) = join(complement(join(X1,X0)),meet(X1,complement(meet(X1,X0))))
| zero != meet(X0,join(complement(join(X0,X1)),meet(X1,complement(meet(X1,X0))))) ),
inference(forward_demodulation,[],[f34775,f28762]) ).
fof(f34959,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),meet(X1,complement(meet(X1,X0)))),
inference(forward_subsumption_resolution,[],[f34883,f34867]) ).
fof(f49427,plain,
! [X0,X1] : complement(join(X1,complement(join(X0,X1)))) = join(complement(join(X0,join(X1,complement(join(X0,X1))))),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f34959,f31869]) ).
fof(f49455,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(join(complement(X1),complement(join(X0,X1)))),meet(complement(X1),complement(complement(join(X0,X1))))),
inference(superposition,[],[f34959,f23956]) ).
fof(f49456,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(join(complement(X0),complement(join(X0,X1)))),meet(complement(X0),complement(complement(join(X0,X1))))),
inference(superposition,[],[f34959,f25058]) ).
fof(f49500,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(meet(X1,complement(meet(X1,X0))),complement(X0)),
inference(superposition,[],[f15,f34959]) ).
fof(f49557,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(meet(X1,complement(meet(X1,X0))),complement(complement(X0)))),
inference(superposition,[],[f29826,f34959]) ).
fof(f49574,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(complement(complement(X0)),meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f49557,f9258]) ).
fof(f49626,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f49500,f5]) ).
fof(f49665,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(join(X0,X1))),complement(X0)),complement(join(complement(X0),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f49456,f6335]) ).
fof(f49666,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(join(X0,X1))),complement(X1)),complement(join(complement(X1),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f49455,f6335]) ).
fof(f49694,plain,
! [X0,X1] : complement(join(X1,complement(join(X0,X1)))) = join(meet(complement(meet(X0,X1)),X0),complement(join(X0,join(X1,complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f49427,f6335]) ).
fof(f49795,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(X0,meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f49574,f4294]) ).
fof(f49835,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(X1,complement(X0)),
inference(forward_demodulation,[],[f49626,f24827]) ).
fof(f49864,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X0),complement(complement(join(X0,X1)))),complement(join(complement(X0),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f49665,f6936]) ).
fof(f49865,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X1),complement(complement(join(X0,X1)))),complement(join(complement(X1),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f49666,f6936]) ).
fof(f49887,plain,
! [X0,X1] : complement(join(X1,complement(join(X0,X1)))) = join(meet(X0,complement(meet(X0,X1))),complement(join(X0,join(X1,complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f49694,f6936]) ).
fof(f49975,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f49795,f33880]) ).
fof(f50024,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X0),complement(complement(join(X0,X1)))),meet(join(X0,X1),complement(complement(X0)))),
inference(forward_demodulation,[],[f49864,f28959]) ).
fof(f50025,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X1),complement(complement(join(X0,X1)))),meet(join(X0,X1),complement(complement(X1)))),
inference(forward_demodulation,[],[f49865,f28959]) ).
fof(f50047,plain,
! [X0,X1] : complement(join(X1,complement(join(X0,X1)))) = join(meet(X0,complement(meet(X0,X1))),meet(complement(join(X0,X1)),join(X0,X1))),
inference(forward_demodulation,[],[f49887,f29525]) ).
fof(f50123,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f49975,f49835]) ).
fof(f50167,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X0)),join(X0,X1)),meet(complement(X0),complement(complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50024,f6335]) ).
fof(f50168,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X1)),join(X0,X1)),meet(complement(X1),complement(complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50025,f6335]) ).
fof(f50189,plain,
! [X0,X1] : complement(join(X1,complement(join(X0,X1)))) = join(meet(X0,complement(meet(X0,X1))),meet(join(X1,X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f50047,f9452]) ).
fof(f50290,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X0)),join(X0,X1)),complement(join(complement(join(X0,X1)),X0))),
inference(forward_demodulation,[],[f50167,f29480]) ).
fof(f50291,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X1)),join(X0,X1)),complement(join(complement(join(X0,X1)),X1))),
inference(forward_demodulation,[],[f50168,f29480]) ).
fof(f50310,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),zero) = complement(join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f50189,f2718]) ).
fof(f50397,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X0)),join(X0,X1)),complement(join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50290,f29022]) ).
fof(f50398,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X1)),join(X0,X1)),complement(join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f50291,f29022]) ).
fof(f50417,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),zero) = meet(join(X0,X1),complement(X1)),
inference(forward_demodulation,[],[f50310,f28959]) ).
fof(f50488,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X0)),join(X0,X1)),meet(join(X0,X1),complement(X0))),
inference(forward_demodulation,[],[f50397,f28959]) ).
fof(f50489,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X1)),join(X0,X1)),meet(join(X0,X1),complement(X1))),
inference(forward_demodulation,[],[f50398,f28959]) ).
fof(f50503,plain,
! [X0,X1] : meet(complement(X1),join(X0,X1)) = join(meet(X0,complement(meet(X0,X1))),zero),
inference(forward_demodulation,[],[f50417,f5]) ).
fof(f50559,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X0)),join(X0,X1)),meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f50488,f5964]) ).
fof(f50560,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(complement(X1)),join(X0,X1)),meet(complement(X1),join(X0,X1))),
inference(forward_demodulation,[],[f50489,f5964]) ).
fof(f50572,plain,
! [X0,X1] : meet(complement(X1),join(X0,X1)) = join(zero,meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f50503,f6]) ).
fof(f50622,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(join(X1,X0),complement(X0)),meet(complement(complement(X0)),join(X0,X1))),
inference(forward_demodulation,[],[f50559,f9455]) ).
fof(f50623,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(join(X1,X0),complement(X1)),meet(complement(complement(X1)),join(X0,X1))),
inference(forward_demodulation,[],[f50560,f9455]) ).
fof(f50634,plain,
! [X0,X1] : meet(complement(X1),join(X0,X1)) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f50572,f606]) ).
fof(f50678,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X0),join(X1,X0)),meet(join(X0,X1),complement(complement(X0)))),
inference(forward_demodulation,[],[f50622,f7338]) ).
fof(f50679,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X1),join(X1,X0)),meet(join(X0,X1),complement(complement(X1)))),
inference(forward_demodulation,[],[f50623,f7338]) ).
fof(f50688,plain,
! [X0,X1] : meet(complement(X1),join(X0,X1)) = meet(X0,complement(X1)),
inference(forward_demodulation,[],[f50634,f49835]) ).
fof(f50725,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X0),join(X1,X0)),meet(join(X0,X1),X0)),
inference(forward_demodulation,[],[f50678,f4294]) ).
fof(f50726,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X1),join(X1,X0)),meet(join(X0,X1),X1)),
inference(forward_demodulation,[],[f50679,f4294]) ).
fof(f50760,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X0),join(X1,X0)),meet(X0,join(X0,X1))),
inference(forward_demodulation,[],[f50725,f5964]) ).
fof(f50761,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X1),join(X1,X0)),meet(X1,join(X0,X1))),
inference(forward_demodulation,[],[f50726,f5964]) ).
fof(f50790,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(join(X1,X0),X0),meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f50760,f9455]) ).
fof(f50791,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(join(X1,X0),X1),meet(complement(X1),join(X1,X0))),
inference(forward_demodulation,[],[f50761,f9455]) ).
fof(f50816,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(X0,join(X1,X0)),meet(join(X1,X0),complement(X0))),
inference(forward_demodulation,[],[f50790,f7338]) ).
fof(f50817,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(X1,join(X1,X0)),meet(join(X1,X0),complement(X1))),
inference(forward_demodulation,[],[f50791,f7338]) ).
fof(f50839,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(X0,join(X1,X0)),meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f50816,f5964]) ).
fof(f50840,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(X1,join(X1,X0)),meet(complement(X1),join(X1,X0))),
inference(forward_demodulation,[],[f50817,f5964]) ).
fof(f50860,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(X0,join(X1,X0)),meet(X1,complement(X0))),
inference(forward_demodulation,[],[f50839,f50688]) ).
fof(f50861,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(X1,join(X1,X0)),meet(X0,complement(X1))),
inference(forward_demodulation,[],[f50840,f50123]) ).
fof(f50875,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X0),X1),meet(X0,join(X1,X0))),
inference(forward_demodulation,[],[f50860,f6335]) ).
fof(f50876,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X1),X0),meet(X1,join(X1,X0))),
inference(forward_demodulation,[],[f50861,f6335]) ).
fof(f50887,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X0),X1),X0),
inference(forward_demodulation,[],[f50875,f15]) ).
fof(f50888,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(meet(complement(X1),X0),X1),
inference(forward_demodulation,[],[f50876,f3]) ).
fof(f50899,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f50887,f6]) ).
fof(f50900,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(X1,meet(complement(X1),X0)),
inference(forward_demodulation,[],[f50888,f6]) ).
fof(f50908,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f50899,f4294]) ).
fof(f50909,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(complement(X1),X0)),
inference(forward_demodulation,[],[f50900,f4294]) ).
fof(f50984,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,complement(complement(X1))),
inference(superposition,[],[f49835,f28685]) ).
fof(f51168,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f50984,f4294]) ).
fof(f55267,plain,
! [X2,X0,X1] : meet(complement(X1),join(X0,join(X1,X2))) = meet(join(X0,X2),complement(X1)),
inference(superposition,[],[f50688,f4178]) ).
fof(f65387,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(X1,meet(complement(X0),X2))),
inference(superposition,[],[f51168,f164]) ).
fof(f65662,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,join(X1,meet(complement(X0),X2))),
inference(forward_demodulation,[],[f65387,f51168]) ).
fof(f68138,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,meet(X2,join(X1,meet(complement(X2),X0))))),X2) = join(X2,meet(complement(X2),meet(X0,join(X2,X1)))),
inference(superposition,[],[f101,f50909]) ).
fof(f68357,plain,
! [X2,X0,X1] : join(X2,meet(X0,join(X2,X1))) = join(meet(X0,join(X1,meet(X2,join(X1,meet(complement(X2),X0))))),X2),
inference(forward_demodulation,[],[f68138,f50908]) ).
fof(f68514,plain,
! [X2,X0,X1] : join(X2,meet(X0,join(X2,X1))) = join(X2,meet(X0,join(X1,meet(X2,join(X1,meet(complement(X2),X0)))))),
inference(forward_demodulation,[],[f68357,f6]) ).
fof(f68621,plain,
! [X2,X0,X1] : join(X2,meet(X0,join(X2,X1))) = join(X2,meet(X0,join(X1,meet(X2,X1)))),
inference(forward_demodulation,[],[f68514,f65662]) ).
fof(f68684,plain,
! [X2,X0,X1] : join(X2,meet(X0,join(X2,X1))) = join(X2,meet(X0,X1)),
inference(forward_demodulation,[],[f68621,f17]) ).
fof(f70211,plain,
! [X2,X0,X1] : join(meet(complement(X0),X1),meet(complement(X0),join(meet(complement(X0),X1),join(X2,X0)))) = join(meet(complement(X0),X1),meet(complement(X0),join(X2,join(X0,X1)))),
inference(superposition,[],[f19924,f50908]) ).
fof(f70306,plain,
! [X2,X0,X1] : join(meet(complement(X0),X1),meet(complement(X0),join(meet(complement(X0),X1),join(X2,X0)))) = join(meet(complement(X0),X1),meet(join(X2,X1),complement(X0))),
inference(forward_demodulation,[],[f70211,f55267]) ).
fof(f70473,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,X1)) = join(meet(complement(X0),X1),meet(complement(X0),join(meet(complement(X0),X1),join(X2,X0)))),
inference(forward_demodulation,[],[f70306,f11402]) ).
fof(f70573,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,X1)) = join(meet(complement(X0),X1),meet(complement(X0),join(X2,X0))),
inference(forward_demodulation,[],[f70473,f68684]) ).
fof(f70632,plain,
! [X2,X0,X1] : meet(complement(X0),join(X2,X1)) = join(meet(complement(X0),X1),meet(X2,complement(X0))),
inference(forward_demodulation,[],[f70573,f50688]) ).
fof(f81724,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X2),meet(X1,X0)),
inference(superposition,[],[f70632,f4294]) ).
fof(f82750,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f6335,f81724]) ).
fof(f99157,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(superposition,[],[f13,f82750]) ).
fof(f99327,plain,
$false,
inference(trivial_inequality_removal,[],[f99157]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT202-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.22/0.49 % Computer : n018.cluster.edu
% 0.22/0.49 % Model : x86_64 x86_64
% 0.22/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.49 % Memory : 8046.5625MB
% 0.22/0.49 % OS : Linux 6.8.0-71-generic
% 0.22/0.49 % CPULimit : 300
% 0.22/0.49 % WCLimit : 300
% 0.22/0.49 % DateTime : Sun Sep 27 14:08:08 UTC 2026
% 0.22/0.49 % CPUTime :
% 0.22/0.49 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.55 Running first-order theorem proving
% 0.25/0.55 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
% 20.76/4.19 % (2380073)Input is clausal, will run a generic CNF schedule.
% 20.76/4.19 % (2380083)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3841082459:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 20.76/4.19 % (2380083)Instruction limit reached!
% 20.76/4.19 % (2380083)------------------------------
% 20.76/4.19 % (2380083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.76/4.19 % (2380083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.76/4.19 % (2380083)CaDiCaL version: 2.1.3
% 20.76/4.19 % (2380083)Termination reason: Instruction limit
% 20.76/4.19 % (2380083)Termination phase: Saturation
% 20.76/4.19 % (2380083)Time elapsed: 0.059 s
% 20.76/4.19 % (2380083)Peak memory usage: 89 MB
% 20.76/4.19 % (2380083)Instructions burned: 114 (million)
% 20.76/4.19 % (2380080)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4292624659:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 20.76/4.19 % (2380079)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=3729256995:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 20.76/4.19 % (2380081)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2648124858:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 20.76/4.19 % (2380085)dis-21_1_sil=8000:lcm=predicate:random_seed=2916851042: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)
% 20.76/4.19 % (2380084)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2271006187:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 20.76/4.19 % (2380082)lrs+10_1_sil=8000:sp=occurrence:random_seed=3891364166:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 20.76/4.19 % (2380085)Refutation not found, incomplete strategy
% 20.76/4.19 % (2380085)------------------------------
% 20.76/4.19 % (2380085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.76/4.19 % (2380085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.76/4.19 % (2380085)CaDiCaL version: 2.1.3
% 20.76/4.19 % (2380085)Termination reason: Refutation not found, incomplete strategy
% 20.76/4.19 % (2380085)Time elapsed: 0.003 s
% 20.76/4.19 % (2380085)Peak memory usage: 88 MB
% 20.76/4.19 % (2380085)Instructions burned: 1 (million)
% 20.76/4.19 % (2380082)Instruction limit reached!
% 20.76/4.19 % (2380082)------------------------------
% 20.76/4.19 % (2380082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.76/4.19 % (2380082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.76/4.19 % (2380082)CaDiCaL version: 2.1.3
% 20.76/4.19 % (2380082)Termination reason: Instruction limit
% 20.76/4.19 % (2380082)Termination phase: Saturation
% 20.76/4.19 % (2380082)Time elapsed: 0.104 s
% 20.76/4.19 % (2380082)Peak memory usage: 88 MB
% 20.76/4.19 % (2380082)Instructions burned: 107 (million)
% 20.76/4.19 % (2380084)Instruction limit reached!
% 20.76/4.19 % (2380084)------------------------------
% 20.76/4.19 % (2380084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.76/4.19 % (2380084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.76/4.19 % (2380084)CaDiCaL version: 2.1.3
% 20.76/4.19 % (2380084)Termination reason: Instruction limit
% 20.76/4.19 % (2380084)Termination phase: Saturation
% 20.76/4.19 % (2380084)Time elapsed: 0.169 s
% 20.76/4.19 % (2380084)Peak memory usage: 89 MB
% 20.76/4.19 % (2380084)Instructions burned: 181 (million)
% 20.76/4.19 % (2380087)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=1916786187:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 20.76/4.19 % (2380087)Refutation not found, incomplete strategy
% 20.76/4.19 % (2380087)------------------------------
% 20.76/4.19 % (2380087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.76/4.19 % (2380087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.76/4.19 % (2380087)CaDiCaL version: 2.1.3
% 20.76/4.19 % (2380087)Termination reason: Refutation not found, incomplete strategy
% 20.76/4.19 % (2380087)Time elapsed: 0.001 s
% 20.76/4.19 % (2380087)Peak memory usage: 88 MB
% 20.76/4.19 % (2380085)------------------------------
% 20.76/4.19 % (2380085)------------------------------
% 30.21/6.62 % (2380094)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2337634276: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)
% 30.21/6.62 % (2380094)Refutation not found, incomplete strategy
% 30.21/6.62 % (2380094)------------------------------
% 30.21/6.62 % (2380094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380094)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380094)Termination reason: Refutation not found, incomplete strategy
% 30.21/6.62 % (2380094)Time elapsed: 0.003 s
% 30.21/6.62 % (2380094)Peak memory usage: 88 MB
% 30.21/6.62 % (2380094)Instructions burned: 1 (million)
% 30.21/6.62 % (2380087)------------------------------
% 30.21/6.62 % (2380087)------------------------------
% 30.21/6.62 % (2380095)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=789293943:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 30.21/6.62 % (2380095)Refutation not found, incomplete strategy
% 30.21/6.62 % (2380095)------------------------------
% 30.21/6.62 % (2380095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380095)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380095)Termination reason: Refutation not found, incomplete strategy
% 30.21/6.62 % (2380095)Time elapsed: 0.002 s
% 30.21/6.62 % (2380095)Peak memory usage: 88 MB
% 30.21/6.62 % (2380100)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2691881829:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 30.21/6.62 % (2380097)lrs+10_64_to=lpo:sil=8000:random_seed=2785726151:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 30.21/6.62 % (2380100)Instruction limit reached!
% 30.21/6.62 % (2380100)------------------------------
% 30.21/6.62 % (2380100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380100)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380100)Termination reason: Instruction limit
% 30.21/6.62 % (2380100)Termination phase: Saturation
% 30.21/6.62 % (2380100)Time elapsed: 0.105 s
% 30.21/6.62 % (2380100)Peak memory usage: 90 MB
% 30.21/6.62 % (2380100)Instructions burned: 197 (million)
% 30.21/6.62 % (2380097)Instruction limit reached!
% 30.21/6.62 % (2380097)------------------------------
% 30.21/6.62 % (2380097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380097)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380097)Termination reason: Instruction limit
% 30.21/6.62 % (2380097)Termination phase: Saturation
% 30.21/6.62 % (2380097)Time elapsed: 0.128 s
% 30.21/6.62 % (2380097)Peak memory usage: 88 MB
% 30.21/6.62 % (2380097)Instructions burned: 126 (million)
% 30.21/6.62 % (2380094)------------------------------
% 30.21/6.62 % (2380094)------------------------------
% 30.21/6.62 % (2380095)------------------------------
% 30.21/6.62 % (2380095)------------------------------
% 30.21/6.62 % (2380104)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3950045059:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 30.21/6.62 % (2380105)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3009789889:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 30.21/6.62 % (2380107)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=947626611:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 30.21/6.62 % (2380108)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1322007504:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 30.21/6.62 % (2380108)Refutation not found, incomplete strategy
% 30.21/6.62 % (2380108)------------------------------
% 30.21/6.62 % (2380108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380108)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380108)Termination reason: Refutation not found, incomplete strategy
% 30.21/6.62 % (2380108)Time elapsed: 0.002 s
% 30.21/6.62 % (2380108)Peak memory usage: 87 MB
% 30.21/6.62 % (2380107)Instruction limit reached!
% 30.21/6.62 % (2380107)------------------------------
% 30.21/6.62 % (2380107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380107)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380107)Termination reason: Instruction limit
% 30.21/6.62 % (2380107)Termination phase: Saturation
% 30.21/6.62 % (2380107)Time elapsed: 0.108 s
% 30.21/6.62 % (2380107)Peak memory usage: 89 MB
% 30.21/6.62 % (2380107)Instructions burned: 106 (million)
% 30.21/6.62 % (2380104)Instruction limit reached!
% 30.21/6.62 % (2380104)------------------------------
% 30.21/6.62 % (2380104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380104)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380104)Termination reason: Instruction limit
% 30.21/6.62 % (2380104)Termination phase: Saturation
% 30.21/6.62 % (2380104)Time elapsed: 0.162 s
% 30.21/6.62 % (2380104)Peak memory usage: 90 MB
% 30.21/6.62 % (2380104)Instructions burned: 157 (million)
% 30.21/6.62 % (2380113)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4281896741:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2985 on theBenchmark for (2985ds/242Mi)
% 30.21/6.62 % (2380114)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=458547633:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 30.21/6.62 % (2380108)------------------------------
% 30.21/6.62 % (2380108)------------------------------
% 30.21/6.62 % (2380113)Instruction limit reached!
% 30.21/6.62 % (2380113)------------------------------
% 30.21/6.62 % (2380113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380113)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380113)Termination reason: Instruction limit
% 30.21/6.62 % (2380113)Termination phase: Saturation
% 30.21/6.62 % (2380113)Time elapsed: 0.238 s
% 30.21/6.62 % (2380113)Peak memory usage: 90 MB
% 30.21/6.62 % (2380113)Instructions burned: 242 (million)
% 30.21/6.62 % (2380117)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2521185380:i=134:sd=2:doe=on:ss=axioms:sgt=14_2981 on theBenchmark for (2981ds/134Mi)
% 30.21/6.62 % (2380117)Instruction limit reached!
% 30.21/6.62 % (2380117)------------------------------
% 30.21/6.62 % (2380117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380117)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380117)Termination reason: Instruction limit
% 30.21/6.62 % (2380117)Termination phase: Saturation
% 30.21/6.62 % (2380117)Time elapsed: 0.131 s
% 30.21/6.62 % (2380117)Peak memory usage: 89 MB
% 30.21/6.62 % (2380117)Instructions burned: 134 (million)
% 30.21/6.62 % (2380118)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=640401759:i=499:bd=all_2979 on theBenchmark for (2979ds/499Mi)
% 30.21/6.62 % (2380120)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=960483179:i=191:fgj=on:bd=all_2977 on theBenchmark for (2977ds/191Mi)
% 30.21/6.62 % (2380120)Instruction limit reached!
% 30.21/6.62 % (2380120)------------------------------
% 30.21/6.62 % (2380120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380120)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380120)Termination reason: Instruction limit
% 30.21/6.62 % (2380120)Termination phase: Saturation
% 30.21/6.62 % (2380120)Time elapsed: 0.203 s
% 30.21/6.62 % (2380120)Peak memory usage: 91 MB
% 30.21/6.62 % (2380120)Instructions burned: 191 (million)
% 30.21/6.62 % (2380118)Instruction limit reached!
% 30.21/6.62 % (2380118)------------------------------
% 30.21/6.62 % (2380118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380118)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380118)Termination reason: Instruction limit
% 30.21/6.62 % (2380118)Termination phase: Saturation
% 30.21/6.62 % (2380118)Time elapsed: 0.523 s
% 30.21/6.62 % (2380118)Peak memory usage: 94 MB
% 30.21/6.62 % (2380118)Instructions burned: 499 (million)
% 30.21/6.62 % (2380123)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3355074801:i=264:kws=precedence:fsr=off_2972 on theBenchmark for (2972ds/264Mi)
% 30.21/6.62 % (2380124)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=377594181:cond=on:i=156:bs=on:gtg=exists_all:er=known_2971 on theBenchmark for (2971ds/156Mi)
% 30.21/6.62 % (2380124)Instruction limit reached!
% 30.21/6.62 % (2380124)------------------------------
% 30.21/6.62 % (2380124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380124)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380124)Termination reason: Instruction limit
% 30.21/6.62 % (2380124)Termination phase: Saturation
% 30.21/6.62 % (2380124)Time elapsed: 0.156 s
% 30.21/6.62 % (2380124)Peak memory usage: 89 MB
% 30.21/6.62 % (2380124)Instructions burned: 156 (million)
% 30.21/6.62 % (2380123)Instruction limit reached!
% 30.21/6.62 % (2380123)------------------------------
% 30.21/6.62 % (2380123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380123)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380123)Termination reason: Instruction limit
% 30.21/6.62 % (2380123)Termination phase: Saturation
% 30.21/6.62 % (2380123)Time elapsed: 0.282 s
% 30.21/6.62 % (2380123)Peak memory usage: 92 MB
% 30.21/6.62 % (2380123)Instructions burned: 265 (million)
% 30.21/6.62 % (2380127)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=1427918067:i=3256:kws=precedence:bd=preordered:av=off_2966 on theBenchmark for (2966ds/3256Mi)
% 30.21/6.62 % (2380128)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2658262511:i=537:av=off:ss=included_2966 on theBenchmark for (2966ds/537Mi)
% 30.21/6.62 % (2380128)Instruction limit reached!
% 30.21/6.62 % (2380128)------------------------------
% 30.21/6.62 % (2380128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380128)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380128)Termination reason: Instruction limit
% 30.21/6.62 % (2380128)Termination phase: Saturation
% 30.21/6.62 % (2380128)Time elapsed: 0.498 s
% 30.21/6.62 % (2380128)Peak memory usage: 93 MB
% 30.21/6.62 % (2380128)Instructions burned: 538 (million)
% 30.21/6.62 % (2380131)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2524381699:i=180:bd=preordered:av=off_2958 on theBenchmark for (2958ds/180Mi)
% 30.21/6.62 % (2380131)Instruction limit reached!
% 30.21/6.62 % (2380131)------------------------------
% 30.21/6.62 % (2380131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380131)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380131)Termination reason: Instruction limit
% 30.21/6.62 % (2380131)Termination phase: Saturation
% 30.21/6.62 % (2380131)Time elapsed: 0.172 s
% 30.21/6.62 % (2380131)Peak memory usage: 88 MB
% 30.21/6.62 % (2380131)Instructions burned: 180 (million)
% 30.21/6.62 % (2380133)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=1890945378:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2953 on theBenchmark for (2953ds/10307Mi)
% 30.21/6.62 % (2380105)Instruction limit reached!
% 30.21/6.62 % (2380105)------------------------------
% 30.21/6.62 % (2380105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.21/6.62 % (2380105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.21/6.62 % (2380105)CaDiCaL version: 2.1.3
% 30.21/6.62 % (2380105)Termination reason: Instruction limit
% 30.21/6.62 % (2380105)Termination phase: Saturation
% 30.21/6.62 % (2380105)Time elapsed: 3.594 s
% 30.21/6.62 % (2380105)Peak memory usage: 151 MB
% 30.21/6.62 % (2380105)Instructions burned: 3394 (million)
% 30.21/6.62 % (2380080)First to succeed.
% 30.21/6.62 % (2380080)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2380073"
% 30.21/6.62 % (2380080)Refutation found. Thanks to Tanya!
% 30.21/6.62 % SZS status Unsatisfiable for theBenchmark
% 30.21/6.62 % SZS output start Proof for theBenchmark
% See solution above
% 38.40/7.01 % (2380080)------------------------------
% 38.40/7.01 % (2380080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.40/7.01 % (2380080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.40/7.01 % (2380080)CaDiCaL version: 2.1.3
% 38.40/7.01 % (2380080)Termination reason: Refutation
% 38.40/7.01 % (2380080)Time elapsed: 4.712 s
% 38.40/7.01 % (2380080)Peak memory usage: 187 MB
% 38.40/7.01 % (2380080)Instructions burned: 7503 (million)
% 38.40/7.01 % (2380080)------------------------------
% 38.40/7.01 % (2380080)------------------------------
% 38.40/7.01 % (2380073)Success in time 5.293 s
% 38.40/7.01 % Vampire exiting
%------------------------------------------------------------------------------