%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT203-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 35.20s 6.29s
% Output : Refutation 36.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 104
% Number of leaves : 12
% Syntax : Number of formulae : 383 ( 363 unt; 0 def)
% Number of atoms : 405 ( 404 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 46 ( 24 ~; 22 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 9 ( 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 : 906 ( 906 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,join(X1,X2)))) = meet(X0,join(X1,meet(join(X0,X1),join(X2,meet(X0,X1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H57) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f15,plain,
! [X0,X1] : 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(f27,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f15,f4]) ).
fof(f28,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f15,f17]) ).
fof(f29,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f17,f15]) ).
fof(f31,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f29,f6]) ).
fof(f32,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f28,f5]) ).
fof(f33,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f27,f5]) ).
fof(f35,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
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(f44,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f46,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f52,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,join(X0,X2)))) = meet(X1,join(X0,meet(join(X0,X1),join(X2,meet(X1,X0))))),
inference(superposition,[],[f12,f6]) ).
fof(f64,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,join(X1,X2)))) = meet(X0,join(X1,meet(join(X0,X1),join(meet(X0,X1),X2)))),
inference(superposition,[],[f12,f6]) ).
fof(f106,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f107,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f17]) ).
fof(f117,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f133,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f106,f6]) ).
fof(f172,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f17,f36]) ).
fof(f176,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f172,f6]) ).
fof(f189,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f190,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f191,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,join(complement(X0),X1)))) = meet(X0,join(complement(X0),meet(one,join(X1,meet(X0,complement(X0)))))),
inference(superposition,[],[f12,f9]) ).
fof(f193,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(one,X1)),
inference(superposition,[],[f36,f9]) ).
fof(f194,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f196,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,join(complement(X0),X1)))) = meet(X0,join(complement(X0),meet(one,join(X1,zero)))),
inference(forward_demodulation,[],[f191,f10]) ).
fof(f198,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f199,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f201,plain,
! [X0] : complement(X0) = join(complement(X0),zero),
inference(superposition,[],[f17,f10]) ).
fof(f202,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(zero,X1)),
inference(superposition,[],[f106,f10]) ).
fof(f203,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f205,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f201,f6]) ).
fof(f221,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f189]) ).
fof(f224,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f189]) ).
fof(f236,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f224]) ).
fof(f277,plain,
zero = complement(one),
inference(superposition,[],[f10,f221]) ).
fof(f300,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f198]) ).
fof(f304,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f15,f198]) ).
fof(f325,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f17,f300]) ).
fof(f489,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(join(X1,X0),join(X0,X2)),
inference(superposition,[],[f107,f15]) ).
fof(f498,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f107,f6]) ).
fof(f532,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X0,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f489,f117]) ).
fof(f540,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(X0,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f532,f8]) ).
fof(f593,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f203,f5]) ).
fof(f681,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f37,f5]) ).
fof(f690,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f37,f10]) ).
fof(f727,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f690,f325]) ).
fof(f1151,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,f194]) ).
fof(f1162,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1151]) ).
fof(f1205,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f1162,f6]) ).
fof(f1703,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X1,X0)),meet(X0,join(complement(join(X1,X0)),X2)))) = meet(X0,join(complement(join(X1,X0)),meet(join(X0,complement(join(X1,X0))),join(X2,zero)))),
inference(superposition,[],[f12,f727]) ).
fof(f1728,plain,
! [X2,X0,X1] : meet(X0,join(complement(join(X1,X0)),meet(X0,join(complement(join(X1,X0)),X2)))) = meet(X0,join(complement(join(X1,X0)),meet(join(X0,complement(join(X1,X0))),X2))),
inference(forward_demodulation,[],[f1703,f198]) ).
fof(f3569,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(superposition,[],[f1205,f9]) ).
fof(f3598,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f3569,f277]) ).
fof(f3616,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f3598,f198]) ).
fof(f3628,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f3616,f5]) ).
fof(f3637,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(one)),
inference(forward_subsumption_resolution,[],[f3628,f10]) ).
fof(f3644,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f3637,f277]) ).
fof(f3649,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f3644,f198]) ).
fof(f4671,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(one,X1))),
inference(superposition,[],[f193,f46]) ).
fof(f4681,plain,
! [X2,X0,X1] : meet(X2,meet(one,join(X0,meet(one,join(X0,X1))))) = meet(X2,join(X0,meet(join(X0,one),join(X1,meet(one,X0))))),
inference(superposition,[],[f193,f52]) ).
fof(f4781,plain,
! [X2,X0,X1] : meet(X2,meet(one,join(X0,meet(one,join(X0,X1))))) = meet(X2,join(X0,meet(join(X0,one),join(X1,X0)))),
inference(forward_demodulation,[],[f4681,f221]) ).
fof(f4789,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f4671,f193]) ).
fof(f4803,plain,
! [X2,X0,X1] : meet(X2,meet(one,join(X0,meet(one,join(X0,X1))))) = meet(X2,join(X0,meet(one,join(X1,X0)))),
inference(forward_demodulation,[],[f4781,f236]) ).
fof(f4812,plain,
! [X2,X0,X1] : meet(X2,meet(one,join(X0,meet(one,join(X0,X1))))) = meet(X2,join(X0,join(X1,X0))),
inference(forward_demodulation,[],[f4803,f221]) ).
fof(f4816,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,meet(one,join(X0,meet(one,join(X0,X1))))),
inference(forward_demodulation,[],[f4812,f31]) ).
fof(f4819,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,meet(one,join(X0,X1)))),
inference(forward_demodulation,[],[f4816,f193]) ).
fof(f4822,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,join(X0,X1))),
inference(forward_demodulation,[],[f4819,f221]) ).
fof(f4825,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f4822,f24]) ).
fof(f4848,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f4825,f8]) ).
fof(f4908,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f1,f4825]) ).
fof(f4911,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f4825]) ).
fof(f4914,plain,
! [X2,X0,X1] : join(X2,X1) = join(join(X2,X1),meet(X0,join(X1,X2))),
inference(superposition,[],[f17,f4825]) ).
fof(f4960,plain,
! [X2,X0,X1] : join(X2,X1) = join(X2,join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f4914,f8]) ).
fof(f5084,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f5,f4911]) ).
fof(f5398,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f5,f4789]) ).
fof(f6013,plain,
! [X2,X0,X1] : join(join(X1,meet(X0,X2)),X0) = meet(join(join(X1,meet(X0,X2)),X0),join(X0,X1)),
inference(superposition,[],[f4908,f133]) ).
fof(f6087,plain,
! [X2,X0,X1] : join(join(X1,meet(X0,X2)),X0) = meet(join(X1,X0),join(join(X1,meet(X0,X2)),X0)),
inference(forward_demodulation,[],[f6013,f4911]) ).
fof(f6123,plain,
! [X2,X0,X1] : join(join(X1,meet(X0,X2)),X0) = meet(join(X1,X0),join(X0,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f6087,f4825]) ).
fof(f6152,plain,
! [X2,X0,X1] : join(join(X1,meet(X0,X2)),X0) = meet(join(X1,X0),join(X0,X1)),
inference(forward_demodulation,[],[f6123,f133]) ).
fof(f6167,plain,
! [X2,X0,X1] : join(X1,X0) = join(join(X1,meet(X0,X2)),X0),
inference(forward_demodulation,[],[f6152,f4908]) ).
fof(f6179,plain,
! [X2,X0,X1] : join(X1,X0) = join(X0,join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f6167,f6]) ).
fof(f6238,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(X1,X2)),X3) = meet(join(X2,join(X0,X1)),X3),
inference(superposition,[],[f5084,f8]) ).
fof(f6832,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(join(X0,X1),join(X0,X2))),
inference(superposition,[],[f176,f3]) ).
fof(f6833,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(join(X0,X1),join(X2,X0))),
inference(superposition,[],[f176,f15]) ).
fof(f7159,plain,
! [X2,X0,X1] : join(X2,join(X1,X0)) = join(X2,join(X0,join(zero,X1))),
inference(superposition,[],[f202,f117]) ).
fof(f7296,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f7159,f202]) ).
fof(f7462,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f6,f7296]) ).
fof(f7706,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f44,f32]) ).
fof(f8068,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f7296,f7706]) ).
fof(f8069,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f8068,f7706]) ).
fof(f8313,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,X2))) = join(X3,meet(X0,join(X2,X1))),
inference(superposition,[],[f8069,f4911]) ).
fof(f8399,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f8069]) ).
fof(f8411,plain,
! [X2,X3,X0,X1] : join(X0,join(meet(X2,X1),X3)) = join(X3,join(X0,meet(X1,X2))),
inference(superposition,[],[f117,f8069]) ).
fof(f8640,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(superposition,[],[f6,f8399]) ).
fof(f9203,plain,
! [X0,X1] : one = join(meet(X0,X1),complement(meet(X1,X0))),
inference(superposition,[],[f9,f8640]) ).
fof(f10733,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X0,join(X2,X1))),
inference(superposition,[],[f4825,f7462]) ).
fof(f10740,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(X1,X2)),X3) = meet(join(X0,join(X2,X1)),X3),
inference(superposition,[],[f5084,f7462]) ).
fof(f14110,plain,
! [X0,X1] : meet(X0,join(complement(join(X1,X0)),zero)) = meet(X0,join(complement(join(X1,X0)),meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))))),
inference(superposition,[],[f1728,f10]) ).
fof(f14232,plain,
! [X0,X1] : meet(X0,join(complement(join(X1,X0)),meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))))) = meet(X0,join(zero,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f14110,f4825]) ).
fof(f14338,plain,
! [X0,X1] : meet(X0,complement(join(X1,X0))) = meet(X0,join(complement(join(X1,X0)),meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))))),
inference(forward_demodulation,[],[f14232,f205]) ).
fof(f14405,plain,
! [X0,X1] : zero = meet(X0,join(complement(join(X1,X0)),meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))))),
inference(forward_demodulation,[],[f14338,f727]) ).
fof(f14581,plain,
! [X0,X1] : meet(meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))),X0) = meet(meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))),zero),
inference(superposition,[],[f681,f14405]) ).
fof(f14674,plain,
! [X0,X1] : meet(meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))),X0) = meet(zero,meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f14581,f5]) ).
fof(f14753,plain,
! [X0,X1] : zero = meet(meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))),X0),
inference(forward_demodulation,[],[f14674,f304]) ).
fof(f14808,plain,
! [X0,X1] : zero = meet(X0,meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))))),
inference(forward_demodulation,[],[f14753,f5]) ).
fof(f14845,plain,
! [X0,X1] : zero = meet(X0,join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0)))))),
inference(forward_demodulation,[],[f14808,f33]) ).
fof(f15036,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))) ),
inference(superposition,[],[f1162,f14845]) ).
fof(f15090,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(join(X0,complement(join(X1,X0))))),
inference(trivial_inequality_removal,[],[f15036]) ).
fof(f15344,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X0,X1)),complement(join(meet(X1,X0),complement(meet(X0,X1))))),
inference(superposition,[],[f15090,f7706]) ).
fof(f15374,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f3,f15090]) ).
fof(f15379,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f24,f15090]) ).
fof(f15452,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f15379,f6]) ).
fof(f15456,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f15374,f5]) ).
fof(f15473,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X0,X1)),complement(one)),
inference(forward_demodulation,[],[f15344,f9203]) ).
fof(f15543,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(one),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f15473,f6]) ).
fof(f15585,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(zero,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f15543,f277]) ).
fof(f15609,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_demodulation,[],[f15585,f205]) ).
fof(f15771,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f15456,f4]) ).
fof(f15847,plain,
! [X2,X0,X1] : join(X2,complement(X1)) = join(complement(X1),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f6179,f15456]) ).
fof(f15897,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f15771,f5]) ).
fof(f16015,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f17,f15897]) ).
fof(f16018,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(meet(X0,X1)),meet(complement(X0),X2)),
inference(superposition,[],[f35,f15897]) ).
fof(f16027,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(meet(X0,X1)),join(complement(X0),X2)),
inference(superposition,[],[f107,f15897]) ).
fof(f16060,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(X0),join(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f16027,f117]) ).
fof(f16064,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(X0),meet(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f16018,f46]) ).
fof(f16066,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f16015,f6]) ).
fof(f16164,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f16066,f15609]) ).
fof(f16342,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f16164,f3]) ).
fof(f16488,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f16342,f6]) ).
fof(f16576,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f16488,f3649]) ).
fof(f17063,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f15,f16576]) ).
fof(f17155,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f17063,f5]) ).
fof(f17302,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f44,f17155]) ).
fof(f17995,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f17302,f15456]) ).
fof(f18308,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),complement(join(complement(X1),complement(X0)))),
inference(superposition,[],[f17995,f3649]) ).
fof(f18980,plain,
! [X0,X1] : complement(complement(join(complement(X1),complement(X0)))) = join(complement(complement(join(complement(X1),complement(X0)))),complement(meet(X0,X1))),
inference(superposition,[],[f15452,f18308]) ).
fof(f18984,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,[],[f18980,f6]) ).
fof(f19064,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X0,X1)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f18984,f3649]) ).
fof(f19120,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(meet(X0,X1)),complement(X1))),
inference(forward_demodulation,[],[f19064,f117]) ).
fof(f19162,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f19120,f7296]) ).
fof(f19195,plain,
! [X0,X1] : join(complement(meet(X0,X1)),complement(X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f19162,f16060]) ).
fof(f19224,plain,
! [X0,X1] : join(complement(X1),complement(meet(X0,X1))) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f19195,f6]) ).
fof(f19242,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f19224,f16164]) ).
fof(f19273,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(X1,complement(X0))),
inference(superposition,[],[f19242,f3649]) ).
fof(f19278,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f19242,f3649]) ).
fof(f19381,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X0,X1))),complement(join(complement(X0),complement(complement(meet(X0,X1)))))),
inference(superposition,[],[f15090,f19242]) ).
fof(f19388,plain,
! [X0,X1] : complement(complement(X0)) = complement(meet(join(complement(X0),complement(complement(meet(X0,X1)))),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f19381,f19242]) ).
fof(f19472,plain,
! [X0,X1] : complement(complement(X0)) = complement(meet(complement(meet(X0,X1)),join(complement(X0),complement(complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f19388,f15609]) ).
fof(f19511,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(join(complement(X0),complement(complement(meet(X0,X1))))),meet(X0,X1)),
inference(forward_demodulation,[],[f19472,f19278]) ).
fof(f19535,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),complement(join(complement(X0),complement(complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f19511,f6]) ).
fof(f19553,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),complement(complement(meet(complement(meet(X0,X1)),X0)))),
inference(forward_demodulation,[],[f19535,f19242]) ).
fof(f19567,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),meet(complement(meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f19553,f3649]) ).
fof(f19574,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f19567,f8069]) ).
fof(f19580,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f19574,f3649]) ).
fof(f19597,plain,
! [X2,X0,X1] : join(complement(X2),meet(complement(X1),X0)) = complement(meet(join(complement(X0),X1),X2)),
inference(superposition,[],[f19278,f19278]) ).
fof(f19613,plain,
! [X2,X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(join(complement(X0),X2),X1)),X0),
inference(superposition,[],[f19278,f36]) ).
fof(f19633,plain,
! [X2,X0,X1] : join(complement(join(X1,X0)),X2) = complement(meet(join(X0,X1),complement(X2))),
inference(superposition,[],[f19278,f4911]) ).
fof(f19676,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(superposition,[],[f3649,f19278]) ).
fof(f19734,plain,
! [X2,X0,X1] : join(complement(join(X1,X0)),X2) = join(X2,complement(join(X0,X1))),
inference(forward_demodulation,[],[f19633,f19273]) ).
fof(f19751,plain,
! [X2,X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(join(complement(X0),X2),X1))),
inference(forward_demodulation,[],[f19613,f6]) ).
fof(f19809,plain,
! [X2,X0,X1] : complement(meet(complement(X0),X1)) = join(X0,join(complement(X1),meet(complement(X2),X0))),
inference(forward_demodulation,[],[f19751,f19597]) ).
fof(f19845,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(forward_demodulation,[],[f19809,f498]) ).
fof(f19993,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(superposition,[],[f3649,f19845]) ).
fof(f20695,plain,
! [X2,X0,X1] : meet(complement(X2),meet(X1,complement(X0))) = complement(join(X2,join(X0,complement(X1)))),
inference(superposition,[],[f19993,f19273]) ).
fof(f20697,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f19993,f3649]) ).
fof(f20716,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),X2) = complement(join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f19993,f8]) ).
fof(f20717,plain,
! [X0,X1] : complement(complement(X0)) = meet(complement(complement(join(X1,X0))),join(X0,complement(join(X1,X0)))),
inference(superposition,[],[f19993,f15090]) ).
fof(f20828,plain,
! [X0,X1] : complement(complement(X0)) = meet(join(X1,X0),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f20717,f3649]) ).
fof(f20842,plain,
! [X2,X0,X1] : meet(complement(join(X2,X0)),X1) = meet(complement(X2),meet(X1,complement(X0))),
inference(forward_demodulation,[],[f20695,f20716]) ).
fof(f20875,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f20828,f3649]) ).
fof(f20969,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f5,f20697]) ).
fof(f21699,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),complement(X0))),
inference(superposition,[],[f20875,f4]) ).
fof(f21769,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X1,X0)))),
inference(superposition,[],[f36,f20875]) ).
fof(f21908,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f21699,f4825]) ).
fof(f22054,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f21769,f6]) ).
fof(f22109,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(X0,join(complement(X1),meet(complement(X0),X1))),
inference(superposition,[],[f21769,f19993]) ).
fof(f22930,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f107,f19580]) ).
fof(f23263,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f22930,f15609]) ).
fof(f25486,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(meet(join(X1,complement(join(X1,X0))),X0),X2),
inference(superposition,[],[f5398,f22054]) ).
fof(f25556,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(join(X1,complement(join(X1,X0))),meet(X0,X2)),
inference(forward_demodulation,[],[f25486,f7]) ).
fof(f25650,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X0,meet(X2,join(X1,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f25556,f46]) ).
fof(f25962,plain,
! [X0,X1] :
( zero != meet(meet(X1,complement(meet(X0,X1))),join(X0,complement(join(X0,X1))))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X0,X1)))) ),
inference(superposition,[],[f1205,f23263]) ).
fof(f26046,plain,
! [X0,X1] :
( zero != meet(X1,meet(complement(meet(X0,X1)),join(X0,complement(join(X0,X1)))))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f25962,f7]) ).
fof(f26162,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),meet(X1,X0))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f26046,f25650]) ).
fof(f26244,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),complement(meet(X0,X1)))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f26162,f5]) ).
fof(f26294,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X0,X1))))
| join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f26244,f7]) ).
fof(f26321,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f26294,f593]) ).
fof(f26344,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(meet(X0,X1),complement(X1)),
inference(forward_demodulation,[],[f26321,f19273]) ).
fof(f26363,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f26344,f6]) ).
fof(f26411,plain,
! [X0,X1] : join(complement(X1),complement(complement(meet(X0,X1)))) = join(complement(complement(X0)),meet(complement(X1),complement(X0))),
inference(superposition,[],[f26363,f19242]) ).
fof(f26456,plain,
! [X0,X1] : join(X0,complement(join(X0,meet(X1,complement(meet(X1,X0)))))) = join(complement(meet(X1,complement(meet(X1,X0)))),zero),
inference(superposition,[],[f26363,f593]) ).
fof(f26511,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(X1,X0))) = X1,
inference(superposition,[],[f3,f26363]) ).
fof(f26516,plain,
! [X0,X1] : join(complement(X0),meet(X1,X0)) = join(X1,join(complement(X0),meet(X1,X0))),
inference(superposition,[],[f24,f26363]) ).
fof(f26550,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),meet(X1,X0))) = join(join(complement(join(X1,X0)),X1),X2),
inference(superposition,[],[f7462,f26363]) ).
fof(f26575,plain,
! [X0,X1] : meet(X1,join(complement(X1),meet(one,join(complement(join(complement(X1),X0)),zero)))) = meet(X1,join(complement(X1),meet(X1,join(complement(X0),meet(complement(X1),X0))))),
inference(superposition,[],[f196,f26363]) ).
fof(f26590,plain,
! [X0,X1] : complement(join(X0,complement(join(X0,X1)))) = meet(X1,complement(join(X0,complement(join(X0,X1))))),
inference(superposition,[],[f17155,f26363]) ).
fof(f26608,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f24,f26363]) ).
fof(f26629,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(meet(X0,X1),complement(join(X0,complement(join(X0,X1))))))
| complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(join(X0,X1))))) ),
inference(superposition,[],[f1162,f26363]) ).
fof(f26642,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(join(X0,X1)))) = join(join(meet(X0,X1),complement(X1)),X2),
inference(superposition,[],[f7462,f26363]) ).
fof(f26651,plain,
! [X0,X1] : meet(complement(X1),meet(X0,X1)) = meet(complement(X1),join(meet(X0,X1),complement(join(X0,complement(join(X0,X1)))))),
inference(superposition,[],[f21769,f26363]) ).
fof(f26656,plain,
! [X0,X1] : meet(complement(X1),meet(X0,X1)) = meet(complement(X1),join(meet(X0,X1),meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f26651,f19993]) ).
fof(f26665,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(join(X0,X1)))) = join(meet(X0,X1),join(complement(X1),X2)),
inference(forward_demodulation,[],[f26642,f8]) ).
fof(f26676,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(meet(X0,X1),meet(complement(X0),join(X0,X1))))
| complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(join(X0,X1))))) ),
inference(forward_demodulation,[],[f26629,f19993]) ).
fof(f26690,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(X0,complement(X1)),
inference(forward_demodulation,[],[f26608,f15847]) ).
fof(f26704,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(X1,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f26590,f19993]) ).
fof(f26714,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(complement(X1),X0))) = meet(X1,join(complement(X1),meet(one,join(complement(join(complement(X1),X0)),zero)))),
inference(forward_demodulation,[],[f26575,f21908]) ).
fof(f26738,plain,
! [X2,X0,X1] : join(complement(join(X1,X0)),join(X1,X2)) = join(X2,join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f26550,f8]) ).
fof(f26761,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[],[f26516,f133]) ).
fof(f26808,plain,
! [X0,X1] : join(X0,complement(join(X0,meet(X1,complement(meet(X1,X0)))))) = join(zero,complement(meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f26456,f6]) ).
fof(f26839,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X1,X0))) = join(complement(X1),complement(complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f26411,f20697]) ).
fof(f26853,plain,
! [X0,X1] : meet(X1,meet(complement(X1),X0)) = meet(complement(X1),join(meet(X0,X1),meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f26656,f46]) ).
fof(f26861,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(join(X0,X1)))) = join(complement(X1),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f26665,f117]) ).
fof(f26867,plain,
! [X0,X1] :
( complement(complement(X1)) = join(meet(X0,X1),meet(complement(X0),join(X0,X1)))
| zero != meet(complement(X1),join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) ),
inference(forward_demodulation,[],[f26676,f19993]) ).
fof(f26884,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f26704,f681]) ).
fof(f26892,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(complement(X1),X0))) = meet(X1,join(complement(X1),meet(one,join(zero,complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f26714,f8313]) ).
fof(f26909,plain,
! [X2,X0,X1] : join(X1,join(X2,complement(join(X1,X0)))) = join(X2,join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f26738,f117]) ).
fof(f26968,plain,
! [X0,X1] : complement(meet(X1,complement(meet(X1,X0)))) = join(X0,complement(join(X0,meet(X1,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f26808,f205]) ).
fof(f26989,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X1,X0))) = complement(meet(complement(meet(X0,X1)),X1)),
inference(forward_demodulation,[],[f26839,f19242]) ).
fof(f26996,plain,
! [X0,X1] : meet(zero,X0) = meet(complement(X1),join(meet(X0,X1),meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f26853,f199]) ).
fof(f27002,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(X1))) = join(complement(X1),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f26861,f26690]) ).
fof(f27008,plain,
! [X0,X1] :
( join(meet(X0,X1),meet(complement(X0),join(X0,X1))) = X1
| zero != meet(complement(X1),join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) ),
inference(forward_demodulation,[],[f26867,f3649]) ).
fof(f27025,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(complement(X1),X0))) = meet(X1,join(complement(X1),join(zero,complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f26892,f221]) ).
fof(f27038,plain,
! [X2,X0,X1] : join(X1,join(X2,complement(join(X1,X0)))) = join(X2,join(X1,complement(X0))),
inference(forward_demodulation,[],[f26909,f26761]) ).
fof(f27084,plain,
! [X0,X1] : complement(meet(X1,complement(meet(X1,X0)))) = join(X0,complement(meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f26968,f26690]) ).
fof(f27097,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X1,X0))) = complement(meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f26989,f15609]) ).
fof(f27103,plain,
! [X0,X1] : meet(zero,X0) = meet(complement(X1),join(meet(X0,X1),meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f26996,f26884]) ).
fof(f27112,plain,
! [X0,X1] :
( join(meet(X0,X1),meet(X1,complement(X0))) = X1
| zero != meet(complement(X1),join(meet(X0,X1),meet(complement(X0),join(X0,X1)))) ),
inference(forward_demodulation,[],[f27008,f26884]) ).
fof(f27127,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(complement(X1),X0))) = meet(X1,join(zero,join(complement(join(complement(X1),X0)),complement(X1)))),
inference(forward_demodulation,[],[f27025,f4848]) ).
fof(f27173,plain,
! [X0,X1] : join(meet(X1,X0),complement(X1)) = join(X0,join(meet(X1,X0),complement(X1))),
inference(forward_demodulation,[],[f27084,f19273]) ).
fof(f27179,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X1,X0))) = join(meet(X0,X1),complement(X1)),
inference(forward_demodulation,[],[f27097,f19273]) ).
fof(f27183,plain,
! [X0,X1] : zero = meet(complement(X1),join(meet(X0,X1),meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f27103,f304]) ).
fof(f27191,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(meet(X0,X1),meet(X1,complement(X0))))
| join(meet(X0,X1),meet(X1,complement(X0))) = X1 ),
inference(forward_demodulation,[],[f27112,f26884]) ).
fof(f27202,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(complement(X1),X0))) = meet(X1,join(zero,join(complement(X1),complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f27127,f10733]) ).
fof(f27236,plain,
! [X0,X1] : join(meet(X1,X0),complement(X1)) = join(X0,join(complement(X1),meet(X1,X0))),
inference(forward_demodulation,[],[f27173,f7296]) ).
fof(f27240,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(complement(complement(X0)),complement(join(X1,X0))),
inference(forward_demodulation,[],[f27179,f6]) ).
fof(f27248,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(X0))) = X1,
inference(forward_subsumption_resolution,[],[f27191,f27183]) ).
fof(f27254,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(complement(X1),X0))) = meet(X1,join(complement(X1),complement(join(complement(X1),X0)))),
inference(forward_demodulation,[],[f27202,f300]) ).
fof(f27277,plain,
! [X0,X1] : join(X0,complement(X1)) = join(meet(X1,X0),complement(X1)),
inference(forward_demodulation,[],[f27236,f498]) ).
fof(f27281,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = complement(meet(join(X1,X0),complement(X0))),
inference(forward_demodulation,[],[f27240,f19242]) ).
fof(f27291,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(X0))) = meet(X1,join(complement(X0),meet(complement(X1),X0))),
inference(forward_demodulation,[],[f27254,f26690]) ).
fof(f27309,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),meet(X1,X0)),
inference(forward_demodulation,[],[f27277,f6]) ).
fof(f27312,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = complement(meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f27281,f15609]) ).
fof(f27319,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f27291,f22109]) ).
fof(f27334,plain,
! [X0,X1] : join(complement(join(X1,X0)),X0) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f27312,f19278]) ).
fof(f27339,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(X0)),
inference(forward_demodulation,[],[f27319,f19242]) ).
fof(f27350,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(join(X1,X0)),X0),
inference(forward_demodulation,[],[f27334,f26761]) ).
fof(f27363,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(X0,complement(X1)),
inference(forward_demodulation,[],[f27350,f6]) ).
fof(f27414,plain,
! [X0,X1] : meet(meet(X0,complement(meet(X1,X0))),complement(X1)) = meet(meet(X0,complement(meet(X1,X0))),complement(zero)),
inference(superposition,[],[f27339,f203]) ).
fof(f27451,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = meet(complement(X0),complement(complement(X1))),
inference(superposition,[],[f27339,f20969]) ).
fof(f27452,plain,
! [X0,X1] : meet(complement(X1),complement(complement(join(X0,X1)))) = meet(complement(X1),complement(complement(X0))),
inference(superposition,[],[f27339,f20697]) ).
fof(f27458,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,complement(complement(X1))),
inference(superposition,[],[f27339,f19278]) ).
fof(f27606,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f27458,f3649]) ).
fof(f27610,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(complement(X1),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f27452,f20697]) ).
fof(f27611,plain,
! [X0,X1] : complement(join(X0,complement(X1))) = meet(complement(X0),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f27451,f20697]) ).
fof(f27643,plain,
! [X0,X1] : meet(complement(zero),meet(X0,complement(meet(X1,X0)))) = meet(meet(X0,complement(meet(X1,X0))),complement(X1)),
inference(forward_demodulation,[],[f27414,f5]) ).
fof(f27697,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = complement(join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f27610,f20697]) ).
fof(f27698,plain,
! [X0,X1] : complement(join(X0,complement(join(X0,X1)))) = complement(join(X0,complement(X1))),
inference(forward_demodulation,[],[f27611,f20697]) ).
fof(f27725,plain,
! [X0,X1] : meet(complement(zero),meet(X0,complement(meet(X1,X0)))) = meet(complement(X1),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f27643,f5]) ).
fof(f27766,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(complement(X1),join(X0,X1)),
inference(forward_demodulation,[],[f27697,f19993]) ).
fof(f27767,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f27698,f19993]) ).
fof(f27790,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(zero),meet(X0,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f27725,f16064]) ).
fof(f27821,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X0,X1)),
inference(forward_demodulation,[],[f27766,f19993]) ).
fof(f27822,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f27767,f19993]) ).
fof(f27839,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(join(zero,meet(X1,X0))),X0),
inference(forward_demodulation,[],[f27790,f20842]) ).
fof(f27868,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(join(zero,meet(X1,X0)))),
inference(forward_demodulation,[],[f27839,f5]) ).
fof(f27883,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f27868,f300]) ).
fof(f28482,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(superposition,[],[f23263,f27883]) ).
fof(f28896,plain,
! [X0,X1] : meet(complement(meet(X1,complement(meet(X0,X1)))),join(X0,X1)) = meet(complement(meet(X1,complement(meet(X0,X1)))),X0),
inference(superposition,[],[f27821,f23263]) ).
fof(f29010,plain,
! [X0,X1] : join(X1,X0) = join(meet(complement(X0),X1),meet(join(X1,X0),complement(complement(X0)))),
inference(superposition,[],[f27248,f27821]) ).
fof(f29012,plain,
! [X0,X1] : meet(complement(complement(X0)),join(X1,X0)) = meet(join(X1,X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f27883,f27821]) ).
fof(f29013,plain,
! [X0,X1] : meet(complement(complement(X0)),join(X1,X0)) = meet(join(X1,X0),join(complement(X1),X0)),
inference(forward_demodulation,[],[f29012,f19278]) ).
fof(f29015,plain,
! [X0,X1] : join(X1,X0) = join(meet(complement(X0),X1),meet(join(X1,X0),X0)),
inference(forward_demodulation,[],[f29010,f3649]) ).
fof(f29092,plain,
! [X0,X1] : meet(complement(meet(X1,complement(meet(X0,X1)))),join(X0,X1)) = meet(X0,complement(meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f28896,f5]) ).
fof(f29100,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = meet(join(X1,X0),join(complement(X1),X0)),
inference(forward_demodulation,[],[f29013,f3649]) ).
fof(f29102,plain,
! [X0,X1] : join(X1,X0) = join(meet(complement(X0),X1),meet(X0,join(X1,X0))),
inference(forward_demodulation,[],[f29015,f8069]) ).
fof(f29162,plain,
! [X0,X1] : meet(join(meet(X0,X1),complement(X1)),join(X0,X1)) = meet(X0,join(meet(X0,X1),complement(X1))),
inference(forward_demodulation,[],[f29092,f19273]) ).
fof(f29169,plain,
! [X0,X1] : meet(join(X1,X0),join(complement(X1),X0)) = X0,
inference(forward_demodulation,[],[f29100,f15]) ).
fof(f29171,plain,
! [X0,X1] : join(X1,X0) = join(meet(complement(X0),X1),X0),
inference(forward_demodulation,[],[f29102,f15]) ).
fof(f29215,plain,
! [X0,X1] : meet(X0,join(complement(X1),meet(X0,X1))) = meet(join(meet(X0,X1),complement(X1)),join(X0,X1)),
inference(forward_demodulation,[],[f29162,f4825]) ).
fof(f29219,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f29171,f6]) ).
fof(f29249,plain,
! [X0,X1] : meet(X0,join(complement(X1),meet(X0,X1))) = meet(join(X1,X0),join(meet(X0,X1),complement(X1))),
inference(forward_demodulation,[],[f29215,f4911]) ).
fof(f29272,plain,
! [X0,X1] : meet(join(X1,X0),join(complement(X1),meet(X0,X1))) = meet(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f29249,f4825]) ).
fof(f29289,plain,
! [X0,X1] : meet(join(X1,X0),join(complement(X1),meet(X0,X1))) = X0,
inference(forward_demodulation,[],[f29272,f26511]) ).
fof(f29301,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(X1))) = X0,
inference(forward_demodulation,[],[f29289,f26761]) ).
fof(f29810,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(superposition,[],[f27822,f106]) ).
fof(f29939,plain,
! [X0,X1] : meet(complement(complement(X0)),join(X0,X1)) = meet(join(X0,X1),complement(meet(complement(X0),X1))),
inference(superposition,[],[f27883,f27822]) ).
fof(f29940,plain,
! [X0,X1] : meet(complement(complement(X0)),join(X0,X1)) = meet(join(X0,X1),join(complement(X1),X0)),
inference(forward_demodulation,[],[f29939,f19278]) ).
fof(f30024,plain,
! [X2,X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f29810,f26884]) ).
fof(f30040,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = meet(join(X0,X1),join(complement(X1),X0)),
inference(forward_demodulation,[],[f29940,f3649]) ).
fof(f30109,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(X1),X0)) = X0,
inference(forward_demodulation,[],[f30040,f3]) ).
fof(f31364,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),X1),meet(X0,join(join(complement(X0),X1),X2)))) = meet(X0,join(join(complement(X0),X1),meet(join(X0,join(complement(X0),X1)),join(meet(X0,X1),X2)))),
inference(superposition,[],[f64,f27606]) ).
fof(f31471,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),X1),meet(X0,join(join(complement(X0),X1),X2)))) = meet(X0,join(complement(X0),join(X1,meet(join(X0,join(complement(X0),X1)),join(meet(X0,X1),X2))))),
inference(forward_demodulation,[],[f31364,f8]) ).
fof(f31579,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),X1),meet(X0,join(join(complement(X0),X1),X2)))) = meet(X0,join(X1,meet(join(X0,join(complement(X0),X1)),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f31471,f27606]) ).
fof(f31639,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),X1),meet(X0,join(join(complement(X0),X1),X2)))) = meet(X0,join(X1,meet(join(one,X1),join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f31579,f190]) ).
fof(f31677,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),X1),meet(X0,join(join(complement(X0),X1),X2)))) = meet(X0,join(X1,meet(one,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f31639,f224]) ).
fof(f31699,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(meet(X0,X1),X2))) = meet(X0,join(join(complement(X0),X1),meet(X0,join(join(complement(X0),X1),X2)))),
inference(forward_demodulation,[],[f31677,f221]) ).
fof(f31704,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(meet(X0,X1),X2))) = meet(X0,join(complement(X0),join(X1,meet(X0,join(join(complement(X0),X1),X2))))),
inference(forward_demodulation,[],[f31699,f8]) ).
fof(f31707,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(meet(X0,X1),X2))) = meet(X0,join(X1,meet(X0,join(join(complement(X0),X1),X2)))),
inference(forward_demodulation,[],[f31704,f27606]) ).
fof(f31710,plain,
! [X2,X0,X1] : meet(X0,join(X1,join(meet(X0,X1),X2))) = meet(X0,join(X1,meet(X0,join(complement(X0),join(X1,X2))))),
inference(forward_demodulation,[],[f31707,f8]) ).
fof(f31713,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,join(X1,X2)))) = meet(X0,join(X1,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f31710,f27606]) ).
fof(f31716,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f31713,f107]) ).
fof(f32240,plain,
! [X2,X0,X1] : join(join(X1,meet(X2,join(X1,X0))),complement(join(X0,X1))) = join(join(X1,meet(X2,join(X1,X0))),complement(X0)),
inference(superposition,[],[f27363,f4960]) ).
fof(f32497,plain,
! [X2,X0,X1] : join(join(X1,meet(X2,join(X1,X0))),complement(join(X0,X1))) = join(complement(X0),join(X1,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f32240,f6]) ).
fof(f32592,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,meet(X2,join(X1,X0)))) = join(complement(join(X1,X0)),join(X1,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f32497,f19734]) ).
fof(f32666,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,meet(X2,join(X1,X0)))) = join(X1,join(meet(join(X1,X0),X2),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f32592,f8411]) ).
fof(f32721,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,meet(X2,join(X1,X0)))) = join(X1,join(complement(join(X1,X0)),meet(join(X1,X0),X2))),
inference(forward_demodulation,[],[f32666,f7296]) ).
fof(f32762,plain,
! [X2,X0,X1] : join(X1,join(X2,complement(join(X1,X0)))) = join(complement(X0),join(X1,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f32721,f27309]) ).
fof(f32784,plain,
! [X2,X0,X1] : join(X2,join(X1,complement(X0))) = join(complement(X0),join(X1,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f32762,f27038]) ).
fof(f32818,plain,
! [X2,X0,X1] : join(X2,join(complement(X1),X0)) = join(join(complement(X1),X0),meet(meet(complement(X0),X1),X2)),
inference(superposition,[],[f29219,f19676]) ).
fof(f32845,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,meet(X1,complement(X2)))),
inference(superposition,[],[f29219,f46]) ).
fof(f33106,plain,
! [X2,X0,X1] : join(X2,join(complement(X1),X0)) = join(complement(X1),join(X0,meet(meet(complement(X0),X1),X2))),
inference(forward_demodulation,[],[f32818,f8]) ).
fof(f33202,plain,
! [X2,X0,X1] : join(X2,join(complement(X1),X0)) = join(complement(X1),join(X0,meet(complement(X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f33106,f7]) ).
fof(f33261,plain,
! [X2,X0,X1] : join(complement(X1),join(X0,meet(X1,X2))) = join(X2,join(complement(X1),X0)),
inference(forward_demodulation,[],[f33202,f28482]) ).
fof(f33365,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,X1)) = join(meet(join(X0,X2),X1),complement(X0)),
inference(superposition,[],[f27309,f36]) ).
fof(f33631,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,X1)) = join(complement(X0),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f33365,f6]) ).
fof(f33732,plain,
! [X2,X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f33631,f27309]) ).
fof(f35134,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(join(X1,meet(X0,X2)),complement(X0))),
inference(superposition,[],[f29301,f133]) ).
fof(f35135,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(join(X1,meet(X2,X0)),complement(X0))),
inference(superposition,[],[f29301,f498]) ).
fof(f35136,plain,
! [X2,X0,X1] : join(X1,meet(X2,join(X1,X0))) = meet(join(X0,X1),join(join(X1,meet(X2,join(X1,X0))),complement(X0))),
inference(superposition,[],[f29301,f4960]) ).
fof(f35412,plain,
! [X2,X0,X1] : join(X1,meet(X2,join(X1,X0))) = meet(join(X0,X1),join(complement(X0),join(X1,meet(X2,join(X1,X0))))),
inference(forward_demodulation,[],[f35136,f4825]) ).
fof(f35413,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(complement(X0),join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f35135,f4825]) ).
fof(f35414,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(complement(X0),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f35134,f4825]) ).
fof(f35507,plain,
! [X2,X0,X1] : join(X1,meet(X2,join(X1,X0))) = meet(join(X0,X1),join(X2,join(X1,complement(X0)))),
inference(forward_demodulation,[],[f35412,f32784]) ).
fof(f35508,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(X1,join(X2,complement(X0)))),
inference(forward_demodulation,[],[f35413,f27002]) ).
fof(f35509,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X2,join(complement(X0),X1))),
inference(forward_demodulation,[],[f35414,f33261]) ).
fof(f44121,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(join(complement(X1),X0),meet(join(join(X1,X0),join(complement(X1),X0)),join(X2,X0)))),
inference(superposition,[],[f12,f29169]) ).
fof(f44132,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(join(complement(X1),X0),meet(join(join(X1,X0),join(complement(X1),X0)),join(X0,X2)))),
inference(superposition,[],[f64,f29169]) ).
fof(f44226,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),join(X0,meet(join(join(X1,X0),join(complement(X1),X0)),join(X0,X2))))),
inference(forward_demodulation,[],[f44132,f8]) ).
fof(f44236,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),join(X0,meet(join(join(X1,X0),join(complement(X1),X0)),join(X2,X0))))),
inference(forward_demodulation,[],[f44121,f8]) ).
fof(f44382,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),join(X0,meet(join(X0,join(join(X1,X0),complement(X1))),join(X0,X2))))),
inference(forward_demodulation,[],[f44226,f6238]) ).
fof(f44385,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),join(X0,meet(join(X0,join(join(X1,X0),complement(X1))),join(X2,X0))))),
inference(forward_demodulation,[],[f44236,f6238]) ).
fof(f44483,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),meet(join(X0,join(join(X1,X0),complement(X1))),join(X0,X2)))),
inference(forward_demodulation,[],[f44382,f6832]) ).
fof(f44486,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),meet(join(X0,join(join(X1,X0),complement(X1))),join(X2,X0)))),
inference(forward_demodulation,[],[f44385,f6833]) ).
fof(f44548,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),meet(join(X0,join(complement(X1),join(X1,X0))),join(X0,X2)))),
inference(forward_demodulation,[],[f44483,f10740]) ).
fof(f44551,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),meet(join(X0,join(complement(X1),join(X1,X0))),join(X2,X0)))),
inference(forward_demodulation,[],[f44486,f10740]) ).
fof(f44585,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),meet(join(X1,join(X0,complement(X1))),join(X0,X2)))),
inference(forward_demodulation,[],[f44548,f540]) ).
fof(f44588,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(complement(X1),meet(join(X1,join(X0,complement(X1))),join(X2,X0)))),
inference(forward_demodulation,[],[f44551,f540]) ).
fof(f44600,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(join(X0,X2),complement(X1))),
inference(forward_demodulation,[],[f44585,f33732]) ).
fof(f44603,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(join(X2,X0),complement(X1))),
inference(forward_demodulation,[],[f44588,f33732]) ).
fof(f44605,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(X0,join(X2,complement(X1)))),
inference(forward_demodulation,[],[f44600,f8]) ).
fof(f44608,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))) = meet(join(X1,X0),join(X2,join(X0,complement(X1)))),
inference(forward_demodulation,[],[f44603,f8]) ).
fof(f44610,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))),
inference(forward_demodulation,[],[f44605,f35508]) ).
fof(f44613,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X0,X1))) = meet(join(X1,X0),join(join(complement(X1),X0),meet(join(X1,X0),join(join(complement(X1),X0),X2)))),
inference(forward_demodulation,[],[f44608,f35507]) ).
fof(f44614,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = meet(join(X1,X0),join(join(complement(X1),X0),X2)),
inference(forward_demodulation,[],[f44610,f31716]) ).
fof(f44617,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X0,X1))) = meet(join(X1,X0),join(join(complement(X1),X0),X2)),
inference(forward_demodulation,[],[f44613,f31716]) ).
fof(f44618,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = meet(join(X1,X0),join(complement(X1),join(X0,X2))),
inference(forward_demodulation,[],[f44614,f8]) ).
fof(f44621,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X0,X1))) = meet(join(X1,X0),join(complement(X1),join(X0,X2))),
inference(forward_demodulation,[],[f44617,f8]) ).
fof(f44623,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = join(X0,meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f44621,f44618]) ).
fof(f102721,plain,
! [X2,X0,X1] : meet(join(meet(X1,X2),X0),complement(meet(X0,complement(X1)))) = meet(complement(complement(X1)),join(meet(X1,X2),X0)),
inference(superposition,[],[f27883,f30024]) ).
fof(f102748,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(join(meet(X1,X2),X0),complement(meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f102721,f3649]) ).
fof(f102962,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(join(meet(X1,X2),X0),join(X1,complement(X0))),
inference(forward_demodulation,[],[f102748,f19273]) ).
fof(f103118,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(join(complement(X0),X1),join(meet(X1,X2),X0)),
inference(forward_demodulation,[],[f102962,f4911]) ).
fof(f105673,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(join(complement(meet(complement(meet(X0,X1)),X2)),X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f103118,f28482]) ).
fof(f105945,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(join(X2,meet(X0,X1)),join(complement(meet(complement(meet(X0,X1)),X2)),X0)),
inference(forward_demodulation,[],[f105673,f4911]) ).
fof(f106208,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(join(X2,meet(X0,X1)),join(X0,complement(meet(complement(meet(X0,X1)),X2)))),
inference(forward_demodulation,[],[f105945,f4825]) ).
fof(f106419,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(join(X2,meet(X0,X1)),join(X0,join(complement(X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f106208,f19278]) ).
fof(f106580,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X2,X0)),
inference(forward_demodulation,[],[f106419,f35509]) ).
fof(f108341,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(X2,join(X0,X1))),
inference(superposition,[],[f106580,f30109]) ).
fof(f108884,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f108341,f44623]) ).
fof(f109920,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X2),join(X1,X0)),
inference(superposition,[],[f4825,f108884]) ).
fof(f109921,plain,
! [X2,X0,X1] : meet(X1,join(X0,X2)) = meet(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f681,f108884]) ).
fof(f112427,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X2,meet(X0,complement(meet(X0,X1))))),
inference(superposition,[],[f109920,f19580]) ).
fof(f113019,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X2,X0),meet(X0,X1)),
inference(forward_demodulation,[],[f112427,f32845]) ).
fof(f113282,plain,
! [X2,X0,X1] : join(meet(X2,X0),meet(X0,X1)) = meet(X0,join(X2,X1)),
inference(forward_demodulation,[],[f113019,f109921]) ).
fof(f114011,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X2),meet(X0,X1)),
inference(superposition,[],[f8399,f113282]) ).
fof(f121241,plain,
meet(a,join(b,c)) != meet(a,join(c,b)),
inference(superposition,[],[f13,f114011]) ).
fof(f121523,plain,
$false,
inference(forward_subsumption_resolution,[],[f121241,f4825]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT203-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.49 % Computer : n009.cluster.edu
% 0.20/0.49 % Model : x86_64 x86_64
% 0.20/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.49 % Memory : 8046.5625MB
% 0.20/0.49 % OS : Linux 6.8.0-71-generic
% 0.20/0.49 % CPULimit : 300
% 0.20/0.49 % WCLimit : 300
% 0.20/0.49 % DateTime : Sun Sep 27 14:06:00 UTC 2026
% 0.20/0.49 % CPUTime :
% 0.20/0.49 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.55 Running first-order theorem proving
% 0.25/0.55 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.04/4.52 % (2065288)Input is clausal, will run a generic CNF schedule.
% 23.04/4.52 % (2065294)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=892088792:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 23.04/4.52 % (2065293)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=3908901304:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 23.04/4.52 % (2065295)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=211712886:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 23.04/4.52 % (2065296)lrs+10_1_sil=8000:sp=occurrence:random_seed=2659023851:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 23.04/4.52 % (2065297)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2996287232:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 23.04/4.52 % (2065299)dis-21_1_sil=8000:lcm=predicate:random_seed=4251045324: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)
% 23.04/4.52 % (2065298)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2294290687:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 23.04/4.52 % (2065299)Refutation not found, incomplete strategy
% 23.04/4.52 % (2065299)------------------------------
% 23.04/4.52 % (2065299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.52 % (2065299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.52 % (2065299)CaDiCaL version: 2.1.3
% 23.04/4.52 % (2065299)Termination reason: Refutation not found, incomplete strategy
% 23.04/4.52 % (2065299)Time elapsed: 0.003 s
% 23.04/4.52 % (2065299)Peak memory usage: 88 MB
% 23.04/4.52 % (2065299)Instructions burned: 1 (million)
% 23.04/4.52 % (2065296)Instruction limit reached!
% 23.04/4.52 % (2065296)------------------------------
% 23.04/4.52 % (2065296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.52 % (2065296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.52 % (2065296)CaDiCaL version: 2.1.3
% 23.04/4.52 % (2065296)Termination reason: Instruction limit
% 23.04/4.52 % (2065296)Termination phase: Saturation
% 23.04/4.52 % (2065296)Time elapsed: 0.104 s
% 23.04/4.52 % (2065296)Peak memory usage: 88 MB
% 23.04/4.52 % (2065296)Instructions burned: 107 (million)
% 23.04/4.52 % (2065297)Instruction limit reached!
% 23.04/4.52 % (2065297)------------------------------
% 23.04/4.52 % (2065297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.52 % (2065297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.52 % (2065297)CaDiCaL version: 2.1.3
% 23.04/4.52 % (2065297)Termination reason: Instruction limit
% 23.04/4.52 % (2065297)Termination phase: Saturation
% 23.04/4.52 % (2065297)Time elapsed: 0.110 s
% 23.04/4.52 % (2065297)Peak memory usage: 88 MB
% 23.04/4.52 % (2065297)Instructions burned: 114 (million)
% 23.04/4.52 % (2065298)Instruction limit reached!
% 23.04/4.52 % (2065298)------------------------------
% 23.04/4.52 % (2065298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.52 % (2065298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.52 % (2065298)CaDiCaL version: 2.1.3
% 23.04/4.52 % (2065298)Termination reason: Instruction limit
% 23.04/4.52 % (2065298)Termination phase: Saturation
% 23.04/4.52 % (2065298)Time elapsed: 0.176 s
% 23.04/4.52 % (2065298)Peak memory usage: 89 MB
% 23.04/4.52 % (2065298)Instructions burned: 180 (million)
% 23.04/4.52 % (2065308)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2128836297:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 23.04/4.52 % (2065308)Refutation not found, incomplete strategy
% 23.04/4.52 % (2065308)------------------------------
% 23.04/4.52 % (2065308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.04/4.52 % (2065299)------------------------------
% 23.04/4.52 % (2065299)------------------------------
% 23.04/4.52 % (2065308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.04/4.52 % (2065308)CaDiCaL version: 2.1.3
% 23.04/4.52 % (2065308)Termination reason: Refutation not found, incomplete strategy
% 23.04/4.52 % (2065308)Time elapsed: 0.003 s
% 35.20/6.29 % (2065308)Peak memory usage: 88 MB
% 35.20/6.29 % (2065308)Instructions burned: 1 (million)
% 35.20/6.29 % (2065307)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=125220400:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 35.20/6.29 % (2065307)Refutation not found, incomplete strategy
% 35.20/6.29 % (2065307)------------------------------
% 35.20/6.29 % (2065307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065307)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065307)Termination reason: Refutation not found, incomplete strategy
% 35.20/6.29 % (2065307)Time elapsed: 0.002 s
% 35.20/6.29 % (2065307)Peak memory usage: 88 MB
% 35.20/6.29 % (2065309)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3282549830:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 35.20/6.29 % (2065309)Refutation not found, incomplete strategy
% 35.20/6.29 % (2065309)------------------------------
% 35.20/6.29 % (2065309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065309)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065309)Termination reason: Refutation not found, incomplete strategy
% 35.20/6.29 % (2065309)Time elapsed: 0.002 s
% 35.20/6.29 % (2065309)Peak memory usage: 87 MB
% 35.20/6.29 % (2065312)lrs+10_64_to=lpo:sil=8000:random_seed=2821202300:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 35.20/6.29 % (2065308)------------------------------
% 35.20/6.29 % (2065308)------------------------------
% 35.20/6.29 % (2065307)------------------------------
% 35.20/6.29 % (2065307)------------------------------
% 35.20/6.29 % (2065312)Instruction limit reached!
% 35.20/6.29 % (2065312)------------------------------
% 35.20/6.29 % (2065312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065312)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065312)Termination reason: Instruction limit
% 35.20/6.29 % (2065312)Termination phase: Saturation
% 35.20/6.29 % (2065312)Time elapsed: 0.125 s
% 35.20/6.29 % (2065312)Peak memory usage: 88 MB
% 35.20/6.29 % (2065312)Instructions burned: 126 (million)
% 35.20/6.29 % (2065309)------------------------------
% 35.20/6.29 % (2065309)------------------------------
% 35.20/6.29 % (2065315)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=138249710:avsq=on:i=194:fgj=on:bd=preordered_2988 on theBenchmark for (2988ds/194Mi)
% 35.20/6.29 % (2065316)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3104698900:i=157:gtg=all_2988 on theBenchmark for (2988ds/157Mi)
% 35.20/6.29 % (2065317)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2863404938:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 35.20/6.29 % (2065318)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=3650026290:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 35.20/6.29 % (2065316)Instruction limit reached!
% 35.20/6.29 % (2065316)------------------------------
% 35.20/6.29 % (2065316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065316)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065316)Termination reason: Instruction limit
% 35.20/6.29 % (2065316)Termination phase: Saturation
% 35.20/6.29 % (2065316)Time elapsed: 0.162 s
% 35.20/6.29 % (2065316)Peak memory usage: 90 MB
% 35.20/6.29 % (2065316)Instructions burned: 158 (million)
% 35.20/6.29 % (2065315)Instruction limit reached!
% 35.20/6.29 % (2065315)------------------------------
% 35.20/6.29 % (2065315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065315)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065315)Termination reason: Instruction limit
% 35.20/6.29 % (2065315)Termination phase: Saturation
% 35.20/6.29 % (2065315)Time elapsed: 0.198 s
% 35.20/6.29 % (2065315)Peak memory usage: 90 MB
% 35.20/6.29 % (2065315)Instructions burned: 195 (million)
% 35.20/6.29 % (2065318)Instruction limit reached!
% 35.20/6.29 % (2065318)------------------------------
% 35.20/6.29 % (2065318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065318)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065318)Termination reason: Instruction limit
% 35.20/6.29 % (2065318)Termination phase: Saturation
% 35.20/6.29 % (2065318)Time elapsed: 0.111 s
% 35.20/6.29 % (2065318)Peak memory usage: 89 MB
% 35.20/6.29 % (2065318)Instructions burned: 106 (million)
% 35.20/6.29 % (2065324)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=534790382:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2984 on theBenchmark for (2984ds/242Mi)
% 35.20/6.29 % (2065323)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2019607195:i=107_2984 on theBenchmark for (2984ds/107Mi)
% 35.20/6.29 % (2065323)Refutation not found, incomplete strategy
% 35.20/6.29 % (2065323)------------------------------
% 35.20/6.29 % (2065323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065323)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065323)Termination reason: Refutation not found, incomplete strategy
% 35.20/6.29 % (2065323)Time elapsed: 0.002 s
% 35.20/6.29 % (2065323)Peak memory usage: 87 MB
% 35.20/6.29 % (2065325)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2766483249:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 35.20/6.29 % (2065324)Instruction limit reached!
% 35.20/6.29 % (2065324)------------------------------
% 35.20/6.29 % (2065324)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065324)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065324)Termination reason: Instruction limit
% 35.20/6.29 % (2065324)Termination phase: Saturation
% 35.20/6.29 % (2065324)Time elapsed: 0.241 s
% 35.20/6.29 % (2065324)Peak memory usage: 90 MB
% 35.20/6.29 % (2065324)Instructions burned: 242 (million)
% 35.20/6.29 % (2065323)------------------------------
% 35.20/6.29 % (2065323)------------------------------
% 35.20/6.29 % (2065329)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3604724843:i=134:sd=2:doe=on:ss=axioms:sgt=14_2978 on theBenchmark for (2978ds/134Mi)
% 35.20/6.29 % (2065329)Instruction limit reached!
% 35.20/6.29 % (2065329)------------------------------
% 35.20/6.29 % (2065329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065329)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065329)Termination reason: Instruction limit
% 35.20/6.29 % (2065329)Termination phase: Saturation
% 35.20/6.29 % (2065329)Time elapsed: 0.131 s
% 35.20/6.29 % (2065329)Peak memory usage: 89 MB
% 35.20/6.29 % (2065329)Instructions burned: 135 (million)
% 35.20/6.29 % (2065330)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1918947785:i=499:bd=all_2977 on theBenchmark for (2977ds/499Mi)
% 35.20/6.29 % (2065332)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2161426712:i=191:fgj=on:bd=all_2974 on theBenchmark for (2974ds/191Mi)
% 35.20/6.29 % (2065332)Instruction limit reached!
% 35.20/6.29 % (2065332)------------------------------
% 35.20/6.29 % (2065332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065332)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065332)Termination reason: Instruction limit
% 35.20/6.29 % (2065332)Termination phase: Saturation
% 35.20/6.29 % (2065332)Time elapsed: 0.200 s
% 35.20/6.29 % (2065332)Peak memory usage: 91 MB
% 35.20/6.29 % (2065332)Instructions burned: 192 (million)
% 35.20/6.29 % (2065330)Instruction limit reached!
% 35.20/6.29 % (2065330)------------------------------
% 35.20/6.29 % (2065330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065330)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065330)Termination reason: Instruction limit
% 35.20/6.29 % (2065330)Termination phase: Saturation
% 35.20/6.29 % (2065330)Time elapsed: 0.558 s
% 35.20/6.29 % (2065330)Peak memory usage: 93 MB
% 35.20/6.29 % (2065330)Instructions burned: 499 (million)
% 35.20/6.29 % (2065335)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=615193810:i=264:kws=precedence:fsr=off_2969 on theBenchmark for (2969ds/264Mi)
% 35.20/6.29 % (2065336)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4280593404:cond=on:i=156:bs=on:gtg=exists_all:er=known_2968 on theBenchmark for (2968ds/156Mi)
% 35.20/6.29 % (2065336)Instruction limit reached!
% 35.20/6.29 % (2065336)------------------------------
% 35.20/6.29 % (2065336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065336)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065336)Termination reason: Instruction limit
% 35.20/6.29 % (2065336)Termination phase: Saturation
% 35.20/6.29 % (2065336)Time elapsed: 0.157 s
% 35.20/6.29 % (2065336)Peak memory usage: 89 MB
% 35.20/6.29 % (2065336)Instructions burned: 156 (million)
% 35.20/6.29 % (2065335)Instruction limit reached!
% 35.20/6.29 % (2065335)------------------------------
% 35.20/6.29 % (2065335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065335)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065335)Termination reason: Instruction limit
% 35.20/6.29 % (2065335)Termination phase: Saturation
% 35.20/6.29 % (2065335)Time elapsed: 0.267 s
% 35.20/6.29 % (2065335)Peak memory usage: 91 MB
% 35.20/6.29 % (2065335)Instructions burned: 264 (million)
% 35.20/6.29 % (2065339)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=3654567941:i=3256:kws=precedence:bd=preordered:av=off_2963 on theBenchmark for (2963ds/3256Mi)
% 35.20/6.29 % (2065340)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=374313784:i=537:av=off:ss=included_2963 on theBenchmark for (2963ds/537Mi)
% 35.20/6.29 % (2065340)Instruction limit reached!
% 35.20/6.29 % (2065340)------------------------------
% 35.20/6.29 % (2065340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065340)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065340)Termination reason: Instruction limit
% 35.20/6.29 % (2065340)Termination phase: Saturation
% 35.20/6.29 % (2065340)Time elapsed: 0.503 s
% 35.20/6.29 % (2065340)Peak memory usage: 93 MB
% 35.20/6.29 % (2065340)Instructions burned: 538 (million)
% 35.20/6.29 % (2065294)First to succeed.
% 35.20/6.29 % (2065294)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2065288"
% 35.20/6.29 % (2065343)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3900862117:i=180:bd=preordered:av=off_2955 on theBenchmark for (2955ds/180Mi)
% 35.20/6.29 % (2065317)Instruction limit reached!
% 35.20/6.29 % (2065317)------------------------------
% 35.20/6.29 % (2065317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065317)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065317)Termination reason: Instruction limit
% 35.20/6.29 % (2065317)Termination phase: Saturation
% 35.20/6.29 % (2065317)Time elapsed: 3.448 s
% 35.20/6.29 % (2065317)Peak memory usage: 148 MB
% 35.20/6.29 % (2065317)Instructions burned: 3394 (million)
% 35.20/6.29 % (2065343)Instruction limit reached!
% 35.20/6.29 % (2065343)------------------------------
% 35.20/6.29 % (2065343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/6.29 % (2065343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/6.29 % (2065343)CaDiCaL version: 2.1.3
% 35.20/6.29 % (2065343)Termination reason: Instruction limit
% 35.20/6.29 % (2065343)Termination phase: Saturation
% 35.20/6.29 % (2065343)Time elapsed: 0.171 s
% 35.20/6.29 % (2065343)Peak memory usage: 88 MB
% 35.20/6.29 % (2065343)Instructions burned: 181 (million)
% 35.20/6.29 % (2065294)Refutation found. Thanks to Tanya!
% 35.20/6.29 % SZS status Unsatisfiable for theBenchmark
% 35.20/6.29 % SZS output start Proof for theBenchmark
% See solution above
% 36.10/6.67 % (2065294)------------------------------
% 36.10/6.67 % (2065294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.10/6.67 % (2065294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.10/6.67 % (2065294)CaDiCaL version: 2.1.3
% 36.10/6.67 % (2065294)Termination reason: Refutation
% 36.10/6.67 % (2065294)Time elapsed: 4.462 s
% 36.10/6.67 % (2065294)Peak memory usage: 181 MB
% 36.10/6.67 % (2065294)Instructions burned: 7663 (million)
% 36.10/6.67 % (2065294)------------------------------
% 36.10/6.67 % (2065294)------------------------------
% 36.10/6.67 % (2065288)Success in time 4.961 s
% 36.10/6.67 % Vampire exiting
%------------------------------------------------------------------------------