%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT201-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 : n006.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 99.14s 17.59s
% Output : Refutation 116.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 96
% Number of leaves : 12
% Syntax : Number of formulae : 359 ( 335 unt; 0 def)
% Number of atoms : 387 ( 386 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 58 ( 30 ~; 28 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 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 : 895 ( 895 !; 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,X3,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,join(meet(X0,X2),meet(X2,X3)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H51) ).
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(f27,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f33,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f35,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f42,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f15,f17]) ).
fof(f44,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f15]) ).
fof(f49,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f42,f5]) ).
fof(f52,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,X3)))) = meet(X1,join(X2,join(meet(X0,X1),meet(X0,X3)))),
inference(superposition,[],[f12,f5]) ).
fof(f58,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X1,join(X2,X0)))) = meet(X2,join(X3,join(meet(X2,X1),meet(X0,X1)))),
inference(superposition,[],[f12,f5]) ).
fof(f63,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,join(X0,meet(X0,X1))))) = meet(X0,join(X2,meet(X0,X1))),
inference(superposition,[],[f12,f17]) ).
fof(f65,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X0,join(X2,X1)))) = meet(X2,join(X3,join(meet(X0,X1),meet(X2,X0)))),
inference(superposition,[],[f12,f6]) ).
fof(f81,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f63,f4]) ).
fof(f94,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f8,f6]) ).
fof(f95,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f96,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f17]) ).
fof(f105,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f119,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f95,f6]) ).
fof(f126,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f15,f95]) ).
fof(f130,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f126,f5]) ).
fof(f147,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f27,f5]) ).
fof(f157,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f17,f27]) ).
fof(f161,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f157,f6]) ).
fof(f177,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(one,X1)),
inference(superposition,[],[f27,f9]) ).
fof(f178,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f180,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f181,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f183,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f185,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,X2)))) = meet(X0,join(X1,join(zero,meet(complement(X0),X2)))),
inference(superposition,[],[f12,f10]) ).
fof(f186,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(X1,join(meet(X0,X2),zero))),
inference(superposition,[],[f12,f10]) ).
fof(f188,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(zero,X1)),
inference(superposition,[],[f95,f10]) ).
fof(f189,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f190,plain,
! [X0,X1] : meet(X0,complement(join(X0,X1))) = meet(X0,zero),
inference(superposition,[],[f27,f10]) ).
fof(f192,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(X1,join(zero,meet(X0,X2)))),
inference(forward_demodulation,[],[f186,f6]) ).
fof(f193,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,X2)))) = meet(X0,join(X1,meet(complement(X0),X2))),
inference(forward_demodulation,[],[f185,f188]) ).
fof(f194,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X0,complement(X2))))),
inference(forward_demodulation,[],[f192,f188]) ).
fof(f196,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(complement(X1),X0))) = meet(X1,join(X2,meet(complement(X1),join(X0,X1)))),
inference(superposition,[],[f193,f6]) ).
fof(f200,plain,
! [X0,X1] : meet(X0,join(X1,meet(complement(X0),complement(X0)))) = meet(X0,join(X1,meet(complement(X0),one))),
inference(superposition,[],[f193,f9]) ).
fof(f208,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(complement(X0),X1))) = meet(X0,join(meet(complement(X0),join(X0,X1)),X2)),
inference(superposition,[],[f193,f6]) ).
fof(f231,plain,
! [X0,X1] : meet(X0,join(X1,meet(complement(X0),complement(X0)))) = meet(X0,join(X1,meet(one,complement(X0)))),
inference(forward_demodulation,[],[f200,f5]) ).
fof(f240,plain,
! [X0,X1] : meet(X0,join(X1,complement(X0))) = meet(X0,join(X1,meet(one,complement(X0)))),
inference(forward_demodulation,[],[f231,f1]) ).
fof(f257,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f180]) ).
fof(f261,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f180]) ).
fof(f275,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f261]) ).
fof(f309,plain,
zero = complement(one),
inference(superposition,[],[f10,f257]) ).
fof(f351,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f183]) ).
fof(f354,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f15,f183]) ).
fof(f372,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f5,f354]) ).
fof(f403,plain,
! [X0,X1] : meet(X0,join(zero,meet(complement(X0),X1))) = meet(X0,meet(complement(X0),join(X0,X1))),
inference(superposition,[],[f193,f351]) ).
fof(f404,plain,
! [X2,X0,X1] : meet(X0,join(zero,meet(X1,join(X0,X2)))) = meet(X0,join(meet(X0,X1),meet(X1,X2))),
inference(superposition,[],[f12,f351]) ).
fof(f407,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X1,X2))),
inference(forward_demodulation,[],[f404,f351]) ).
fof(f408,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(zero,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f403,f147]) ).
fof(f411,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),meet(X1,X2))),
inference(forward_demodulation,[],[f407,f147]) ).
fof(f412,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f408,f351]) ).
fof(f414,plain,
! [X0,X1] : zero = meet(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f412,f10]) ).
fof(f526,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f189,f5]) ).
fof(f672,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f96,f6]) ).
fof(f677,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X1,X0))),
inference(superposition,[],[f96,f9]) ).
fof(f701,plain,
! [X0,X1] : one = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f677,f275]) ).
fof(f752,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f44,f5]) ).
fof(f762,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f44,f10]) ).
fof(f802,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f762,f372]) ).
fof(f837,plain,
! [X0,X1] : one = join(join(X0,X1),complement(X0)),
inference(superposition,[],[f701,f3]) ).
fof(f871,plain,
! [X0,X1] : one = join(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f837,f6]) ).
fof(f878,plain,
! [X0,X1] : one = join(X0,join(X1,complement(X0))),
inference(forward_demodulation,[],[f871,f105]) ).
fof(f1131,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,f181]) ).
fof(f1137,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),one))) = meet(X0,join(X1,meet(complement(X0),join(X2,complement(join(X0,X2)))))),
inference(superposition,[],[f193,f181]) ).
fof(f1142,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1131]) ).
fof(f1147,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(one,complement(X0)))) = meet(X0,join(X1,meet(complement(X0),join(X2,complement(join(X0,X2)))))),
inference(forward_demodulation,[],[f1137,f5]) ).
fof(f1170,plain,
! [X2,X0,X1] : meet(X0,join(X1,complement(X0))) = meet(X0,join(X1,meet(complement(X0),join(X2,complement(join(X0,X2)))))),
inference(forward_demodulation,[],[f1147,f240]) ).
fof(f1183,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f1142,f6]) ).
fof(f1361,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,join(X2,meet(X0,join(complement(X0),X1)))),
inference(superposition,[],[f194,f6]) ).
fof(f1539,plain,
! [X0,X1] :
( one != join(one,X0)
| zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(superposition,[],[f11,f178]) ).
fof(f1564,plain,
! [X0,X1] :
( zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(forward_subsumption_resolution,[],[f1539,f261]) ).
fof(f2006,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,complement(join(X0,X3)))))) = meet(X1,join(X2,join(meet(X1,X0),meet(X0,zero)))),
inference(superposition,[],[f12,f190]) ).
fof(f2035,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,complement(join(X0,X3)))))) = meet(X1,join(X2,meet(X0,join(X1,zero)))),
inference(forward_demodulation,[],[f2006,f12]) ).
fof(f2062,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = meet(X1,join(X2,meet(X0,join(X1,complement(join(X0,X3)))))),
inference(forward_demodulation,[],[f2035,f183]) ).
fof(f2581,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,meet(X0,join(complement(X0),X2)))) = meet(complement(X0),join(X1,join(zero,meet(X0,X2)))),
inference(superposition,[],[f52,f10]) ).
fof(f2609,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(X1,join(meet(X2,X0),zero))),
inference(superposition,[],[f52,f10]) ).
fof(f2695,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(X1,join(zero,meet(X2,X0)))),
inference(forward_demodulation,[],[f2609,f6]) ).
fof(f2719,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,meet(X0,join(complement(X0),X2)))) = meet(complement(X0),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f2581,f188]) ).
fof(f2756,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,meet(X2,join(X0,complement(X2))))),
inference(forward_demodulation,[],[f2695,f188]) ).
fof(f2942,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,X2)))) = meet(X0,join(X1,join(zero,meet(X2,complement(X0))))),
inference(superposition,[],[f58,f10]) ).
fof(f3085,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),join(X0,X2)))) = meet(X0,join(X1,meet(X2,complement(X0)))),
inference(forward_demodulation,[],[f2942,f188]) ).
fof(f3828,plain,
! [X0,X1] :
( zero != meet(join(X0,complement(join(X1,X0))),join(X1,complement(one)))
| join(X1,complement(one)) = complement(join(X0,complement(join(X1,X0)))) ),
inference(superposition,[],[f1183,f181]) ).
fof(f3830,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(superposition,[],[f1183,f9]) ).
fof(f3860,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f3830,f309]) ).
fof(f3862,plain,
! [X0,X1] :
( zero != meet(join(X1,complement(one)),join(X0,complement(join(X1,X0))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f3828,f5]) ).
fof(f3880,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f3860,f183]) ).
fof(f3882,plain,
! [X0,X1] :
( zero != meet(join(X1,zero),join(X0,complement(join(X1,X0))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f3862,f309]) ).
fof(f3894,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = join(X0,complement(one)) ),
inference(forward_demodulation,[],[f3880,f5]) ).
fof(f3896,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X1,X0))))
| join(X1,complement(one)) = complement(join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f3882,f183]) ).
fof(f3905,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(one)),
inference(forward_subsumption_resolution,[],[f3894,f10]) ).
fof(f3907,plain,
! [X0,X1] :
( join(X1,zero) = complement(join(X0,complement(join(X1,X0))))
| zero != meet(X1,join(X0,complement(join(X1,X0)))) ),
inference(forward_demodulation,[],[f3896,f309]) ).
fof(f3914,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f3905,f309]) ).
fof(f3916,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X1,X0))))
| complement(join(X0,complement(join(X1,X0)))) = X1 ),
inference(forward_demodulation,[],[f3907,f183]) ).
fof(f3920,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f3914,f183]) ).
fof(f3995,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X1,meet(X0,X2)),join(X0,X1)),
inference(superposition,[],[f15,f119]) ).
fof(f4032,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f3995,f5]) ).
fof(f4094,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X0,X2))) = meet(X2,join(X3,meet(X0,join(complement(join(X0,X1)),X2)))),
inference(superposition,[],[f2062,f6]) ).
fof(f4263,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(complement(X1),join(X0,X1)))) = meet(X1,join(X2,meet(X0,complement(X1)))),
inference(superposition,[],[f3085,f6]) ).
fof(f4792,plain,
! [X0,X1] : meet(X0,join(X1,complement(X0))) = meet(X0,join(meet(one,complement(X0)),X1)),
inference(superposition,[],[f240,f6]) ).
fof(f4865,plain,
! [X0,X1] : meet(X0,join(X1,complement(X0))) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f4792,f257]) ).
fof(f5180,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f81,f6]) ).
fof(f5201,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = meet(X1,join(X2,meet(X1,X0))),
inference(superposition,[],[f81,f6]) ).
fof(f5730,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(one,X1))),
inference(superposition,[],[f177,f35]) ).
fof(f5883,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f5730,f177]) ).
fof(f7115,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = meet(X1,join(meet(X1,X0),X2)),
inference(superposition,[],[f5180,f6]) ).
fof(f7299,plain,
! [X2,X0,X1] : meet(X2,meet(one,join(X0,meet(X1,one)))) = meet(X2,join(meet(one,X1),X0)),
inference(superposition,[],[f177,f5180]) ).
fof(f7304,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,meet(one,join(X0,meet(X1,one)))),
inference(forward_demodulation,[],[f7299,f257]) ).
fof(f7486,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,meet(X1,one))),
inference(forward_demodulation,[],[f7304,f177]) ).
fof(f7598,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f7486,f180]) ).
fof(f7704,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f7598,f8]) ).
fof(f7830,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f1,f7598]) ).
fof(f7833,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f7598]) ).
fof(f7863,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X3,meet(join(X2,X1),X0)),
inference(superposition,[],[f5883,f7598]) ).
fof(f9210,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f33,f49]) ).
fof(f10804,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f130,f4]) ).
fof(f10805,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f130,f17]) ).
fof(f11418,plain,
! [X2,X0,X1] : join(X2,join(X1,X0)) = join(X2,join(X0,join(zero,X1))),
inference(superposition,[],[f188,f105]) ).
fof(f11564,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f11418,f188]) ).
fof(f11639,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f11564,f9210]) ).
fof(f11746,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f6,f11564]) ).
fof(f11863,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f11639,f9210]) ).
fof(f12047,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f11863]) ).
fof(f12313,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X1,X0),meet(X3,X2)),
inference(superposition,[],[f12047,f12047]) ).
fof(f12442,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X2,X1))) = meet(X3,join(X0,meet(X1,X2))),
inference(superposition,[],[f7598,f12047]) ).
fof(f12775,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,meet(X0,one))) = meet(complement(X0),join(X1,meet(X0,complement(meet(X2,complement(X0)))))),
inference(superposition,[],[f2719,f701]) ).
fof(f12954,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,X0)) = meet(complement(X0),join(X1,meet(X0,complement(meet(X2,complement(X0)))))),
inference(forward_demodulation,[],[f12775,f180]) ).
fof(f13120,plain,
! [X0,X1] : meet(complement(X1),join(complement(meet(X0,complement(X1))),X1)) = meet(complement(X1),complement(meet(X0,complement(X1)))),
inference(superposition,[],[f12954,f17]) ).
fof(f13228,plain,
! [X0,X1] : meet(complement(X1),complement(meet(X0,complement(X1)))) = meet(complement(X1),join(X1,complement(meet(X0,complement(X1))))),
inference(forward_demodulation,[],[f13120,f7598]) ).
fof(f13391,plain,
! [X2,X0,X1] : join(X0,one) = join(X0,join(X1,complement(meet(X0,X2)))),
inference(superposition,[],[f95,f878]) ).
fof(f13405,plain,
! [X2,X0,X1] : one = join(X0,join(X1,complement(meet(X0,X2)))),
inference(forward_demodulation,[],[f13391,f275]) ).
fof(f13873,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(meet(X1,X0),complement(meet(X0,X1)))),
inference(superposition,[],[f7115,f9]) ).
fof(f14213,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f13873,f180]) ).
fof(f14591,plain,
! [X0,X1] : join(meet(X1,X0),complement(meet(X0,X1))) = join(join(meet(X1,X0),complement(meet(X0,X1))),X0),
inference(superposition,[],[f17,f14213]) ).
fof(f14667,plain,
! [X0,X1] : join(meet(X1,X0),complement(meet(X0,X1))) = join(X0,join(meet(X1,X0),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f14591,f6]) ).
fof(f14803,plain,
! [X0,X1] : one = join(meet(X1,X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f14667,f13405]) ).
fof(f15182,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,f14803]) ).
fof(f15215,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f15182]) ).
fof(f15237,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f15215,f7]) ).
fof(f15356,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f15237,f526]) ).
fof(f15599,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f15356,f7830]) ).
fof(f15689,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f15599,f7830]) ).
fof(f17943,plain,
! [X2,X0,X1] : meet(X2,join(meet(X0,join(complement(join(X0,X1)),X2)),meet(X2,join(X0,X1)))) = meet(X2,meet(join(X0,X1),join(complement(join(X0,X1)),X2))),
inference(superposition,[],[f1361,f161]) ).
fof(f18094,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(meet(X0,join(complement(join(X0,X1)),X2)),meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f17943,f752]) ).
fof(f18172,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(meet(join(X0,X1),X2),meet(X0,join(complement(join(X0,X1)),X2)))),
inference(forward_demodulation,[],[f18094,f5201]) ).
fof(f18224,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(meet(join(X0,X1),X2),meet(X0,X2))),
inference(forward_demodulation,[],[f18172,f4094]) ).
fof(f18257,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(meet(X2,X0),meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f18224,f5180]) ).
fof(f18284,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,X0),meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f18257,f10805]) ).
fof(f18539,plain,
! [X2,X0,X1] : meet(X0,join(meet(join(X0,complement(join(X1,X2))),X1),meet(join(X1,X2),X0))) = meet(X0,meet(join(X0,complement(join(X1,X2))),join(X1,X2))),
inference(superposition,[],[f2756,f18284]) ).
fof(f18622,plain,
! [X2,X0,X1] : meet(X0,join(meet(join(X0,complement(join(X1,X2))),X1),meet(join(X1,X2),X0))) = meet(X0,meet(join(X2,X1),join(X0,complement(join(X1,X2))))),
inference(forward_demodulation,[],[f18539,f7863]) ).
fof(f18791,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(meet(join(X0,complement(join(X1,X2))),X1),meet(join(X1,X2),X0))),
inference(forward_demodulation,[],[f18622,f147]) ).
fof(f18919,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(meet(X0,join(X1,X2)),meet(join(X0,complement(join(X1,X2))),X1))),
inference(forward_demodulation,[],[f18791,f5180]) ).
fof(f19001,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(meet(X0,join(X1,X2)),meet(X1,join(X0,complement(join(X1,X2)))))),
inference(forward_demodulation,[],[f18919,f12442]) ).
fof(f19048,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(meet(X0,join(X1,X2)),meet(X1,X0))),
inference(forward_demodulation,[],[f19001,f2062]) ).
fof(f19088,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(meet(X0,X1),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f19048,f5180]) ).
fof(f19117,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = join(meet(X0,X1),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f19088,f10804]) ).
fof(f21941,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(X0,join(complement(X0),complement(meet(X1,X0)))),
inference(superposition,[],[f13228,f3920]) ).
fof(f22151,plain,
! [X0,X1] : meet(join(X0,X1),complement(X0)) = meet(join(X0,X1),join(complement(join(X0,X1)),complement(X0))),
inference(superposition,[],[f21941,f3]) ).
fof(f22356,plain,
! [X0,X1] : meet(join(X0,X1),complement(X0)) = meet(join(X0,X1),join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f22151,f7598]) ).
fof(f22426,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(join(X0,X1),join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f22356,f5]) ).
fof(f22572,plain,
! [X0,X1] : meet(X0,meet(complement(X0),join(X0,X1))) = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(superposition,[],[f27,f22426]) ).
fof(f22675,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f22572,f147]) ).
fof(f22729,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f22675,f10]) ).
fof(f22855,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),complement(join(X0,X1))) ),
inference(superposition,[],[f1564,f22729]) ).
fof(f22924,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(trivial_inequality_removal,[],[f22855]) ).
fof(f23189,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f22924,f15689]) ).
fof(f23202,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f15,f22924]) ).
fof(f23209,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(join(X0,X1)),join(complement(X0),X2)),
inference(superposition,[],[f94,f22924]) ).
fof(f23260,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f23209,f105]) ).
fof(f23263,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f23202,f5]) ).
fof(f23328,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f23263,f3920]) ).
fof(f23379,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f23263,f15689]) ).
fof(f23513,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(superposition,[],[f23189,f3920]) ).
fof(f23519,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f23189,f4]) ).
fof(f23520,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f23189,f17]) ).
fof(f23668,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f23520,f6]) ).
fof(f23669,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f23519,f6]) ).
fof(f23833,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(meet(X0,X1)),join(complement(X0),X2)),
inference(superposition,[],[f94,f23669]) ).
fof(f23888,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(X0),join(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f23833,f105]) ).
fof(f24286,plain,
! [X2,X0,X1] : meet(complement(X1),X2) = meet(complement(X1),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f147,f23668]) ).
fof(f24517,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f33,f23328]) ).
fof(f26727,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f24517,f23379]) ).
fof(f26999,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),complement(join(complement(X1),complement(X0)))),
inference(superposition,[],[f26727,f3920]) ).
fof(f27658,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(join(complement(X1),complement(X0)),complement(meet(X0,X1))),
inference(superposition,[],[f23513,f26999]) ).
fof(f27735,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X0,X1)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f27658,f6]) ).
fof(f27825,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(meet(X0,X1)),complement(X1))),
inference(forward_demodulation,[],[f27735,f105]) ).
fof(f27875,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f27825,f11564]) ).
fof(f27907,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X0,X1)),complement(X1)),
inference(forward_demodulation,[],[f27875,f23888]) ).
fof(f27935,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X1),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f27907,f6]) ).
fof(f27960,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f27935,f23668]) ).
fof(f27993,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(X1,complement(X0))),
inference(superposition,[],[f27960,f3920]) ).
fof(f28000,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f27960,f3920]) ).
fof(f28072,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = join(complement(X0),join(X2,complement(X1))),
inference(superposition,[],[f105,f27960]) ).
fof(f28103,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = join(X2,join(complement(X0),complement(X1))),
inference(superposition,[],[f11564,f27960]) ).
fof(f28129,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f28103,f27960]) ).
fof(f28307,plain,
! [X2,X0,X1] : join(complement(X2),meet(complement(X1),X0)) = complement(meet(join(complement(X0),X1),X2)),
inference(superposition,[],[f28000,f28000]) ).
fof(f28330,plain,
! [X2,X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(join(complement(X0),X2),X1)),X0),
inference(superposition,[],[f28000,f27]) ).
fof(f28335,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = complement(meet(X0,meet(X1,complement(X2)))),
inference(superposition,[],[f28000,f35]) ).
fof(f28336,plain,
! [X2,X0,X1] : join(complement(meet(X2,X0)),X1) = complement(meet(X0,meet(complement(X1),X2))),
inference(superposition,[],[f28000,f35]) ).
fof(f28343,plain,
! [X2,X0,X1] : join(complement(join(X1,X0)),X2) = complement(meet(join(X0,X1),complement(X2))),
inference(superposition,[],[f28000,f7833]) ).
fof(f28372,plain,
! [X0,X1] : complement(meet(complement(X0),join(X1,complement(complement(X0))))) = join(complement(join(complement(complement(X0)),X1)),X0),
inference(superposition,[],[f28000,f4865]) ).
fof(f28398,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f15356,f28000]) ).
fof(f28425,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(superposition,[],[f3920,f28000]) ).
fof(f28511,plain,
! [X0,X1] : complement(meet(complement(X0),join(X1,complement(complement(X0))))) = join(X0,complement(join(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f28372,f6]) ).
fof(f28540,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(complement(join(X1,X0)),X2),
inference(forward_demodulation,[],[f28343,f27993]) ).
fof(f28551,plain,
! [X2,X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(join(complement(X0),X2),X1))),
inference(forward_demodulation,[],[f28330,f6]) ).
fof(f28614,plain,
! [X0,X1] : complement(meet(complement(X0),join(X1,complement(complement(X0))))) = join(X0,meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f28511,f28425]) ).
fof(f28648,plain,
! [X2,X0,X1] : complement(meet(complement(X0),X1)) = join(X0,join(complement(X1),meet(complement(X2),X0))),
inference(forward_demodulation,[],[f28551,f28307]) ).
fof(f28684,plain,
! [X0,X1] : join(complement(join(X1,complement(complement(X0)))),X0) = join(X0,meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f28614,f28000]) ).
fof(f28712,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(forward_demodulation,[],[f28648,f672]) ).
fof(f28729,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(complement(X0))))) = join(X0,meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f28684,f6]) ).
fof(f28749,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(X0,meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f28729,f3920]) ).
fof(f28760,plain,
! [X2,X0,X1] : complement(meet(X2,join(complement(X0),X1))) = join(complement(X2),meet(X0,complement(X1))),
inference(superposition,[],[f28398,f28398]) ).
fof(f28831,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(superposition,[],[f3920,f28398]) ).
fof(f29068,plain,
! [X0,X1] : complement(meet(complement(X0),join(complement(complement(X0)),X1))) = join(X0,complement(join(X1,complement(complement(X0))))),
inference(superposition,[],[f28712,f4865]) ).
fof(f29131,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(superposition,[],[f3920,f28712]) ).
fof(f29232,plain,
! [X0,X1] : complement(meet(complement(X0),join(complement(complement(X0)),X1))) = join(X0,meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f29068,f29131]) ).
fof(f29335,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = complement(meet(complement(X0),join(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f29232,f28749]) ).
fof(f29376,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(complement(complement(X0)),meet(complement(X0),complement(X1))),
inference(forward_demodulation,[],[f29335,f28760]) ).
fof(f29397,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(X0,meet(complement(X0),complement(X1))),
inference(forward_demodulation,[],[f29376,f3920]) ).
fof(f29681,plain,
! [X2,X0,X1] : complement(join(X2,join(X0,complement(X1)))) = meet(complement(X2),meet(complement(X0),X1)),
inference(superposition,[],[f29131,f28712]) ).
fof(f29688,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f29131,f3920]) ).
fof(f29710,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),X2) = complement(join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f29131,f8]) ).
fof(f29867,plain,
! [X2,X0,X1] : meet(complement(join(X2,X0)),X1) = meet(complement(X2),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f29681,f29710]) ).
fof(f30049,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,meet(complement(X1),complement(X0))),
inference(superposition,[],[f5883,f29688]) ).
fof(f30107,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f30049,f29688]) ).
fof(f32198,plain,
! [X2,X0,X1] : complement(join(X2,X1)) = join(complement(join(X2,X1)),meet(X0,complement(join(X1,X2)))),
inference(superposition,[],[f17,f30107]) ).
fof(f33866,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(meet(complement(X0),complement(X1)),join(X0,complement(join(X1,X0)))),
inference(superposition,[],[f15,f29397]) ).
fof(f33981,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(X0),meet(complement(X1),join(X0,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f33866,f7]) ).
fof(f34072,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(join(X0,X1)),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f33981,f29867]) ).
fof(f34127,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f34072,f29688]) ).
fof(f35066,plain,
! [X0,X1] : meet(complement(join(X0,X1)),join(complement(join(X1,X0)),X0)) = join(meet(complement(join(X0,X1)),X0),complement(join(X0,X1))),
inference(superposition,[],[f19117,f34127]) ).
fof(f35113,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(X2,join(X0,complement(join(X1,X0))))) = join(complement(join(X0,X1)),meet(complement(join(X0,X1)),join(join(X0,complement(join(X1,X0))),X2))),
inference(superposition,[],[f19117,f34127]) ).
fof(f35124,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),join(X2,join(X0,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f35113,f4]) ).
fof(f35156,plain,
! [X0,X1] : meet(complement(join(X0,X1)),join(complement(join(X1,X0)),X0)) = join(complement(join(X1,X0)),meet(complement(join(X0,X1)),X0)),
inference(forward_demodulation,[],[f35066,f28540]) ).
fof(f35300,plain,
! [X0,X1] : meet(complement(join(X0,X1)),join(complement(join(X1,X0)),X0)) = join(complement(join(X1,X0)),meet(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f35156,f11863]) ).
fof(f35407,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X0,X1)),join(complement(join(X1,X0)),X0)),
inference(forward_demodulation,[],[f35300,f32198]) ).
fof(f35485,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X0,X1)),join(X0,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f35407,f7598]) ).
fof(f35882,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(complement(join(X1,X0)),join(X2,join(X1,complement(join(X0,X1))))))) = meet(X2,join(X3,join(complement(join(X0,X1)),meet(X2,complement(join(X1,X0)))))),
inference(superposition,[],[f65,f35485]) ).
fof(f35953,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,complement(join(X0,X1)))) = meet(X2,join(X3,meet(complement(join(X1,X0)),join(X2,join(X1,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f35882,f32198]) ).
fof(f36122,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,complement(join(X0,X1)))) = meet(X2,join(X3,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f35953,f35124]) ).
fof(f36805,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,complement(meet(X0,X1)))) = meet(X2,join(X3,complement(join(meet(X1,X0),meet(X0,X1))))),
inference(superposition,[],[f36122,f9210]) ).
fof(f37263,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,complement(meet(X0,X1)))) = meet(X2,join(X3,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f36805,f9210]) ).
fof(f76616,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f411,f5]) ).
fof(f79672,plain,
! [X2,X0,X1] : zero = meet(X0,join(meet(complement(X0),X1),meet(complement(X0),X2))),
inference(superposition,[],[f414,f10804]) ).
fof(f81387,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X0),X2))) = meet(X0,join(meet(complement(X0),join(X2,X0)),X1)),
inference(superposition,[],[f7598,f196]) ).
fof(f93779,plain,
! [X2,X0,X1] : meet(X0,join(meet(complement(X0),join(X0,X2)),meet(X1,complement(X0)))) = meet(X0,join(meet(complement(X0),join(X1,X0)),meet(complement(X0),X2))),
inference(superposition,[],[f4263,f208]) ).
fof(f94035,plain,
! [X2,X0,X1] : meet(X0,join(meet(complement(X0),join(X0,X2)),meet(X1,complement(X0)))) = meet(X0,join(meet(complement(X0),X2),meet(complement(X0),X1))),
inference(forward_demodulation,[],[f93779,f81387]) ).
fof(f94226,plain,
! [X2,X0,X1] : zero = meet(X0,join(meet(complement(X0),join(X0,X2)),meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f94035,f79672]) ).
fof(f94353,plain,
! [X2,X0,X1] : zero = meet(X0,join(meet(X1,complement(X0)),meet(complement(X0),X2))),
inference(forward_demodulation,[],[f94226,f208]) ).
fof(f114828,plain,
! [X0,X1] : meet(X1,join(X0,complement(join(X1,X0)))) = meet(X1,join(join(X0,complement(join(X1,X0))),complement(X1))),
inference(superposition,[],[f1170,f17]) ).
fof(f115170,plain,
! [X0,X1] : meet(X1,join(X0,complement(join(X1,X0)))) = meet(X1,join(complement(X1),join(X0,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f114828,f4865]) ).
fof(f115383,plain,
! [X0,X1] : meet(X1,join(X0,complement(join(X1,X0)))) = meet(X1,join(complement(X1),X0)),
inference(forward_demodulation,[],[f115170,f23260]) ).
fof(f168095,plain,
! [X0,X1] :
( zero != meet(X0,join(meet(complement(X1),complement(X0)),complement(join(X0,complement(join(X1,X0))))))
| complement(join(meet(complement(X1),complement(X0)),complement(join(X0,complement(join(X1,X0)))))) = X0 ),
inference(superposition,[],[f3916,f28749]) ).
fof(f168333,plain,
! [X0,X1] :
( zero != meet(X0,join(meet(complement(X1),complement(X0)),meet(complement(X0),join(X1,X0))))
| complement(join(meet(complement(X1),complement(X0)),complement(join(X0,complement(join(X1,X0)))))) = X0 ),
inference(forward_demodulation,[],[f168095,f29131]) ).
fof(f168447,plain,
! [X0,X1] : complement(join(meet(complement(X1),complement(X0)),complement(join(X0,complement(join(X1,X0)))))) = X0,
inference(forward_subsumption_resolution,[],[f168333,f94353]) ).
fof(f168542,plain,
! [X0,X1] : meet(complement(meet(complement(X1),complement(X0))),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f168447,f29131]) ).
fof(f168614,plain,
! [X0,X1] : meet(join(X0,complement(complement(X1))),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f168542,f27993]) ).
fof(f168680,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f168614,f3920]) ).
fof(f169083,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X1,X0)))),
inference(superposition,[],[f44,f168680]) ).
fof(f173536,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f115383,f169083]) ).
fof(f174469,plain,
! [X2,X0,X1] : meet(meet(complement(X0),X1),X2) = meet(meet(complement(X0),X1),join(join(X0,complement(X1)),X2)),
inference(superposition,[],[f173536,f28712]) ).
fof(f174480,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(superposition,[],[f173536,f3920]) ).
fof(f174526,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X0,join(X1,complement(X2)))),
inference(superposition,[],[f173536,f105]) ).
fof(f174527,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f173536,f105]) ).
fof(f175170,plain,
! [X2,X0,X1] : meet(meet(complement(X0),X1),X2) = meet(complement(X0),meet(X1,join(join(X0,complement(X1)),X2))),
inference(forward_demodulation,[],[f174469,f7]) ).
fof(f175346,plain,
! [X2,X0,X1] : meet(meet(complement(X0),X1),X2) = meet(complement(X0),meet(X1,join(X0,join(complement(X1),X2)))),
inference(forward_demodulation,[],[f175170,f8]) ).
fof(f175443,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,join(X2,X0))) = meet(meet(complement(X0),X1),X2),
inference(forward_demodulation,[],[f175346,f174527]) ).
fof(f175502,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,join(X2,X0))) = meet(complement(X0),meet(X1,X2)),
inference(forward_demodulation,[],[f175443,f7]) ).
fof(f175603,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(meet(X2,X0),X1)),
inference(superposition,[],[f174480,f96]) ).
fof(f175776,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(join(X0,X1))),
inference(superposition,[],[f28712,f174480]) ).
fof(f175795,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = join(meet(complement(X0),X0),meet(complement(X0),X1)),
inference(superposition,[],[f19117,f174480]) ).
fof(f176126,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = join(meet(X0,complement(X0)),meet(X1,complement(X0))),
inference(forward_demodulation,[],[f175795,f12313]) ).
fof(f176134,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f175776,f28000]) ).
fof(f176261,plain,
! [X2,X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f175603,f174480]) ).
fof(f176386,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = join(zero,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f176126,f10]) ).
fof(f176542,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f176386,f351]) ).
fof(f177048,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f28712,f176542]) ).
fof(f177146,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(meet(X0,complement(X1)),complement(meet(join(X0,X1),complement(X1))))),
inference(superposition,[],[f14213,f176542]) ).
fof(f177262,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(meet(X0,complement(X1)),complement(meet(complement(X1),join(X0,X1))))),
inference(forward_demodulation,[],[f177146,f37263]) ).
fof(f177330,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(forward_demodulation,[],[f177048,f27993]) ).
fof(f177465,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(meet(X0,complement(X1)),join(complement(join(X0,X1)),X1))),
inference(forward_demodulation,[],[f177262,f28000]) ).
fof(f177608,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,join(meet(X0,complement(X1)),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f177465,f7704]) ).
fof(f177700,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f177608,f174526]) ).
fof(f177766,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(X0,complement(X1))),
inference(forward_demodulation,[],[f177700,f4032]) ).
fof(f177881,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),X1)) = join(join(complement(X0),X1),meet(X2,meet(X0,complement(X1)))),
inference(superposition,[],[f177766,f28831]) ).
fof(f177883,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X1,X0)),
inference(superposition,[],[f177766,f3920]) ).
fof(f177907,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,meet(X1,complement(X2)))),
inference(superposition,[],[f177766,f7]) ).
fof(f178279,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),X1)) = join(complement(X0),join(X1,meet(X2,meet(X0,complement(X1))))),
inference(forward_demodulation,[],[f177881,f8]) ).
fof(f178386,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),X1)) = join(complement(X0),join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f178279,f177907]) ).
fof(f178759,plain,
! [X2,X0,X1] : join(complement(meet(X1,complement(meet(X2,X0)))),meet(complement(X0),X1)) = join(complement(X0),complement(meet(X1,complement(meet(X2,X0))))),
inference(superposition,[],[f177883,f24286]) ).
fof(f178881,plain,
! [X0,X1] :
( zero != meet(complement(X1),join(meet(X0,X1),complement(join(X0,complement(X1)))))
| complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(X1)))) ),
inference(superposition,[],[f1142,f177883]) ).
fof(f178907,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(X1))) = join(join(meet(X0,X1),complement(X1)),X2),
inference(superposition,[],[f11746,f177883]) ).
fof(f178960,plain,
! [X0,X1] : complement(X1) = meet(join(X0,complement(X1)),join(complement(X1),complement(join(meet(X0,X1),complement(X1))))),
inference(superposition,[],[f168680,f177883]) ).
fof(f178969,plain,
! [X0,X1] : complement(X1) = meet(join(X0,complement(X1)),join(complement(X1),complement(join(complement(X1),meet(X0,X1))))),
inference(forward_demodulation,[],[f178960,f36122]) ).
fof(f179007,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(X1))) = join(meet(X0,X1),join(complement(X1),X2)),
inference(forward_demodulation,[],[f178907,f8]) ).
fof(f179028,plain,
! [X0,X1] :
( zero != meet(complement(X1),complement(join(X0,complement(X1))))
| complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(X1)))) ),
inference(forward_demodulation,[],[f178881,f176261]) ).
fof(f179100,plain,
! [X2,X0,X1] : join(complement(meet(X1,complement(meet(X2,X0)))),meet(complement(X0),X1)) = complement(meet(meet(X1,complement(meet(X2,X0))),X0)),
inference(forward_demodulation,[],[f178759,f27960]) ).
fof(f179231,plain,
! [X0,X1] : complement(X1) = meet(join(X0,complement(X1)),join(complement(meet(X0,X1)),complement(X1))),
inference(forward_demodulation,[],[f178969,f176134]) ).
fof(f179266,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(X1))) = join(complement(X1),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f179007,f105]) ).
fof(f179282,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X0,X1),complement(join(X0,complement(X1)))),
inference(forward_subsumption_resolution,[],[f179028,f802]) ).
fof(f179328,plain,
! [X2,X0,X1] : complement(meet(X0,meet(X1,complement(meet(X2,X0))))) = join(complement(meet(X1,complement(meet(X2,X0)))),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f179100,f15356]) ).
fof(f179423,plain,
! [X0,X1] : complement(X1) = meet(join(X0,complement(X1)),join(complement(X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f179231,f7598]) ).
fof(f179463,plain,
! [X0,X1] : complement(complement(X1)) = join(meet(X0,X1),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f179282,f29131]) ).
fof(f179496,plain,
! [X2,X0,X1] : complement(meet(X0,meet(X1,complement(meet(X2,X0))))) = join(meet(complement(X0),X1),complement(meet(X1,complement(meet(X2,X0))))),
inference(forward_demodulation,[],[f179328,f6]) ).
fof(f179562,plain,
! [X0,X1] : complement(X1) = meet(join(X0,complement(X1)),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f179423,f23668]) ).
fof(f179588,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X0),X1)) = X1,
inference(forward_demodulation,[],[f179463,f3920]) ).
fof(f179608,plain,
! [X2,X0,X1] : complement(meet(X0,meet(X1,complement(meet(X2,X0))))) = join(meet(complement(X0),X1),join(meet(X2,X0),complement(X1))),
inference(forward_demodulation,[],[f179496,f27993]) ).
fof(f179687,plain,
! [X2,X0,X1] : complement(meet(X0,meet(X1,complement(meet(X2,X0))))) = join(complement(X1),join(meet(complement(X0),X1),meet(X2,X0))),
inference(forward_demodulation,[],[f179608,f105]) ).
fof(f179750,plain,
! [X2,X0,X1] : complement(meet(X0,meet(X1,complement(meet(X2,X0))))) = join(complement(X0),join(complement(X1),meet(X2,X0))),
inference(forward_demodulation,[],[f179687,f178386]) ).
fof(f179791,plain,
! [X2,X0,X1] : join(complement(X1),join(X2,complement(X0))) = complement(meet(X0,meet(X1,complement(meet(X2,X0))))),
inference(forward_demodulation,[],[f179750,f179266]) ).
fof(f179816,plain,
! [X2,X0,X1] : join(complement(X1),join(X2,complement(X0))) = join(complement(meet(X0,X1)),meet(X2,X0)),
inference(forward_demodulation,[],[f179791,f28335]) ).
fof(f179835,plain,
! [X2,X0,X1] : join(X2,complement(meet(X1,X0))) = join(complement(meet(X0,X1)),meet(X2,X0)),
inference(forward_demodulation,[],[f179816,f28072]) ).
fof(f179884,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(complement(X0),meet(X1,join(X2,X0)))),
inference(superposition,[],[f179588,f752]) ).
fof(f180815,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(complement(X0),meet(X1,X2))),
inference(forward_demodulation,[],[f179884,f175502]) ).
fof(f250978,plain,
! [X2,X0,X1] : join(join(X1,complement(X0)),complement(meet(X2,complement(meet(X1,X0))))) = join(complement(meet(complement(meet(X1,X0)),X2)),complement(X0)),
inference(superposition,[],[f179835,f179562]) ).
fof(f251563,plain,
! [X2,X0,X1] : join(complement(X0),complement(meet(complement(meet(X1,X0)),X2))) = join(join(X1,complement(X0)),complement(meet(X2,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f250978,f6]) ).
fof(f252085,plain,
! [X2,X0,X1] : join(complement(X0),complement(meet(complement(meet(X1,X0)),X2))) = join(X1,join(complement(X0),complement(meet(X2,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f251563,f8]) ).
fof(f252530,plain,
! [X2,X0,X1] : join(complement(X0),complement(meet(complement(meet(X1,X0)),X2))) = join(X1,complement(meet(meet(X2,complement(meet(X1,X0))),X0))),
inference(forward_demodulation,[],[f252085,f27960]) ).
fof(f252906,plain,
! [X2,X0,X1] : join(complement(X0),complement(meet(complement(meet(X1,X0)),X2))) = join(X1,complement(meet(X0,meet(X2,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f252530,f28129]) ).
fof(f253161,plain,
! [X2,X0,X1] : join(complement(X0),complement(meet(complement(meet(X1,X0)),X2))) = join(X1,join(complement(meet(X0,X2)),meet(X1,X0))),
inference(forward_demodulation,[],[f252906,f28335]) ).
fof(f253347,plain,
! [X2,X0,X1] : join(X1,complement(meet(X0,X2))) = join(complement(X0),complement(meet(complement(meet(X1,X0)),X2))),
inference(forward_demodulation,[],[f253161,f119]) ).
fof(f253478,plain,
! [X2,X0,X1] : join(X1,complement(meet(X0,X2))) = complement(meet(meet(complement(meet(X1,X0)),X2),X0)),
inference(forward_demodulation,[],[f253347,f27960]) ).
fof(f253565,plain,
! [X2,X0,X1] : join(X1,complement(meet(X0,X2))) = complement(meet(X0,meet(complement(meet(X1,X0)),X2))),
inference(forward_demodulation,[],[f253478,f15356]) ).
fof(f253619,plain,
! [X2,X0,X1] : join(X1,complement(meet(X0,X2))) = join(complement(meet(X2,X0)),meet(X1,X0)),
inference(forward_demodulation,[],[f253565,f28336]) ).
fof(f254373,plain,
! [X2,X0,X1] : join(meet(X0,X1),complement(join(X0,complement(meet(X1,X2))))) = join(meet(X0,X1),complement(complement(meet(X2,X1)))),
inference(superposition,[],[f177330,f253619]) ).
fof(f254394,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X0,X1),complement(join(X0,complement(meet(X1,X2))))),
inference(forward_demodulation,[],[f254373,f3920]) ).
fof(f254976,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X0,X1),meet(complement(X0),meet(X1,X2))),
inference(forward_demodulation,[],[f254394,f29131]) ).
fof(f255412,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(X2,X1)),
inference(forward_demodulation,[],[f254976,f180815]) ).
fof(f256614,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(X2,join(X0,X1))),
inference(superposition,[],[f255412,f3]) ).
fof(f256822,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(meet(X2,join(X0,X1)),X0),
inference(superposition,[],[f255412,f3]) ).
fof(f257072,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f119,f255412]) ).
fof(f257079,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(X1,X2)),
inference(superposition,[],[f12047,f255412]) ).
fof(f257650,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(X2,join(X0,X1))),
inference(forward_demodulation,[],[f256822,f6]) ).
fof(f257805,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X1),join(X2,X0)),
inference(forward_demodulation,[],[f256614,f257072]) ).
fof(f258084,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X1),join(X0,X2)),
inference(forward_demodulation,[],[f257650,f257072]) ).
fof(f258938,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X2,meet(X0,join(meet(X0,X1),X2)))),
inference(superposition,[],[f76616,f257805]) ).
fof(f259280,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f258938,f752]) ).
fof(f259699,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f259280,f257079]) ).
fof(f260764,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X2),join(X1,X0)),
inference(superposition,[],[f7833,f258084]) ).
fof(f269233,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(join(meet(X0,X1),X2),X0),
inference(superposition,[],[f260764,f4]) ).
fof(f269995,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f269233,f5]) ).
fof(f270399,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(forward_demodulation,[],[f269995,f259699]) ).
fof(f271602,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(superposition,[],[f13,f270399]) ).
fof(f271864,plain,
$false,
inference(trivial_inequality_removal,[],[f271602]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT201-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 % Computer : n006.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 14:05:41 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.46 Running first-order theorem proving
% 0.17/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.25/4.37 % (3002020)Input is clausal, will run a generic CNF schedule.
% 22.25/4.37 % (3002026)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=1566165592:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 22.25/4.37 % (3002029)lrs+10_1_sil=8000:sp=occurrence:random_seed=3807270752:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 22.25/4.37 % (3002027)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2000979865:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 22.25/4.37 % (3002028)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=286493090:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 22.25/4.37 % (3002030)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=872750195:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 22.25/4.37 % (3002032)dis-21_1_sil=8000:lcm=predicate:random_seed=4194232514: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)
% 22.25/4.37 % (3002031)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=622072321:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 22.25/4.37 % (3002032)Refutation not found, incomplete strategy
% 22.25/4.37 % (3002032)------------------------------
% 22.25/4.37 % (3002032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.25/4.37 % (3002032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.25/4.37 % (3002032)CaDiCaL version: 2.1.3
% 22.25/4.37 % (3002032)Termination reason: Refutation not found, incomplete strategy
% 22.25/4.37 % (3002032)Time elapsed: 0.003 s
% 22.25/4.37 % (3002032)Peak memory usage: 88 MB
% 22.25/4.37 % (3002032)Instructions burned: 1 (million)
% 22.25/4.37 % (3002029)Instruction limit reached!
% 22.25/4.37 % (3002029)------------------------------
% 22.25/4.37 % (3002029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.25/4.37 % (3002029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.25/4.37 % (3002029)CaDiCaL version: 2.1.3
% 22.25/4.37 % (3002029)Termination reason: Instruction limit
% 22.25/4.37 % (3002029)Termination phase: Saturation
% 22.25/4.37 % (3002029)Time elapsed: 0.107 s
% 22.25/4.37 % (3002029)Peak memory usage: 88 MB
% 22.25/4.37 % (3002029)Instructions burned: 107 (million)
% 22.25/4.37 % (3002030)Instruction limit reached!
% 22.25/4.37 % (3002030)------------------------------
% 22.25/4.37 % (3002030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.25/4.37 % (3002030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.25/4.37 % (3002030)CaDiCaL version: 2.1.3
% 22.25/4.37 % (3002030)Termination reason: Instruction limit
% 22.25/4.37 % (3002030)Termination phase: Saturation
% 22.25/4.37 % (3002030)Time elapsed: 0.112 s
% 22.25/4.37 % (3002030)Peak memory usage: 89 MB
% 22.25/4.37 % (3002030)Instructions burned: 114 (million)
% 22.25/4.37 % (3002031)Instruction limit reached!
% 22.25/4.37 % (3002031)------------------------------
% 22.25/4.37 % (3002031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.25/4.37 % (3002031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.25/4.37 % (3002031)CaDiCaL version: 2.1.3
% 22.25/4.37 % (3002031)Termination reason: Instruction limit
% 22.25/4.37 % (3002031)Termination phase: Saturation
% 22.25/4.37 % (3002031)Time elapsed: 0.172 s
% 22.25/4.37 % (3002031)Peak memory usage: 89 MB
% 22.25/4.37 % (3002031)Instructions burned: 180 (million)
% 22.25/4.37 % (3002032)------------------------------
% 22.25/4.37 % (3002032)------------------------------
% 22.25/4.37 % (3002041)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3733885357: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)
% 22.25/4.37 % (3002040)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=3985100155:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 22.25/4.37 % (3002041)Refutation not found, incomplete strategy
% 22.25/4.37 % (3002041)------------------------------
% 22.25/4.37 % (3002041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.25/4.37 % (3002040)Refutation not found, incomplete strategy
% 39.38/6.98 % (3002040)------------------------------
% 39.38/6.98 % (3002040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.38/6.98 % (3002040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.38/6.98 % (3002040)CaDiCaL version: 2.1.3
% 39.38/6.98 % (3002040)Termination reason: Refutation not found, incomplete strategy
% 39.38/6.98 % (3002040)Time elapsed: 0.002 s
% 39.38/6.98 % (3002040)Peak memory usage: 88 MB
% 39.38/6.98 % (3002041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.38/6.98 % (3002041)CaDiCaL version: 2.1.3
% 39.38/6.98 % (3002041)Termination reason: Refutation not found, incomplete strategy
% 39.38/6.98 % (3002041)Time elapsed: 0.003 s
% 39.38/6.98 % (3002041)Peak memory usage: 88 MB
% 39.38/6.98 % (3002041)Instructions burned: 1 (million)
% 39.38/6.98 % (3002042)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=925997971:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 39.38/6.98 % (3002042)Refutation not found, incomplete strategy
% 39.38/6.98 % (3002042)------------------------------
% 39.38/6.98 % (3002042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.38/6.98 % (3002042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.38/6.98 % (3002042)CaDiCaL version: 2.1.3
% 39.38/6.98 % (3002042)Termination reason: Refutation not found, incomplete strategy
% 39.38/6.98 % (3002042)Time elapsed: 0.002 s
% 39.38/6.98 % (3002042)Peak memory usage: 88 MB
% 39.38/6.98 % (3002045)lrs+10_64_to=lpo:sil=8000:random_seed=3483962210:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 39.38/6.98 % (3002041)------------------------------
% 39.38/6.98 % (3002041)------------------------------
% 39.38/6.98 % (3002040)------------------------------
% 39.38/6.98 % (3002040)------------------------------
% 39.38/6.98 % (3002045)Instruction limit reached!
% 39.38/6.98 % (3002045)------------------------------
% 39.38/6.98 % (3002045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.38/6.98 % (3002045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.38/6.98 % (3002045)CaDiCaL version: 2.1.3
% 39.38/6.98 % (3002045)Termination reason: Instruction limit
% 39.38/6.98 % (3002045)Termination phase: Saturation
% 39.38/6.98 % (3002045)Time elapsed: 0.125 s
% 39.38/6.98 % (3002045)Peak memory usage: 88 MB
% 39.38/6.98 % (3002045)Instructions burned: 127 (million)
% 39.38/6.98 % (3002042)------------------------------
% 39.38/6.98 % (3002042)------------------------------
% 39.38/6.98 % (3002048)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=366829743:avsq=on:i=194:fgj=on:bd=preordered_2988 on theBenchmark for (2988ds/194Mi)
% 39.38/6.98 % (3002049)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3362285486:i=157:gtg=all_2988 on theBenchmark for (2988ds/157Mi)
% 39.38/6.98 % (3002050)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=59211406:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 39.38/6.98 % (3002051)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=1810575561:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 39.38/6.98 % (3002049)Instruction limit reached!
% 39.38/6.98 % (3002049)------------------------------
% 39.38/6.98 % (3002049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.38/6.98 % (3002049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.38/6.98 % (3002049)CaDiCaL version: 2.1.3
% 39.38/6.98 % (3002049)Termination reason: Instruction limit
% 39.38/6.98 % (3002049)Termination phase: Saturation
% 39.38/6.98 % (3002049)Time elapsed: 0.162 s
% 39.38/6.98 % (3002049)Peak memory usage: 90 MB
% 39.38/6.98 % (3002049)Instructions burned: 158 (million)
% 39.38/6.98 % (3002048)Instruction limit reached!
% 39.38/6.98 % (3002048)------------------------------
% 39.38/6.98 % (3002048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.38/6.98 % (3002048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.38/6.98 % (3002048)CaDiCaL version: 2.1.3
% 39.38/6.98 % (3002048)Termination reason: Instruction limit
% 39.38/6.98 % (3002048)Termination phase: Saturation
% 39.38/6.98 % (3002048)Time elapsed: 0.195 s
% 39.38/6.98 % (3002048)Peak memory usage: 90 MB
% 39.38/6.98 % (3002048)Instructions burned: 194 (million)
% 39.38/6.98 % (3002051)Instruction limit reached!
% 39.38/6.98 % (3002051)------------------------------
% 64.03/10.22 % (3002051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.03/10.22 % (3002051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.03/10.22 % (3002051)CaDiCaL version: 2.1.3
% 64.03/10.22 % (3002051)Termination reason: Instruction limit
% 64.03/10.22 % (3002051)Termination phase: Saturation
% 64.03/10.22 % (3002051)Time elapsed: 0.115 s
% 64.03/10.22 % (3002051)Peak memory usage: 89 MB
% 64.03/10.22 % (3002051)Instructions burned: 106 (million)
% 64.03/10.22 % (3002056)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2530503598:i=107_2984 on theBenchmark for (2984ds/107Mi)
% 64.03/10.22 % (3002056)Refutation not found, incomplete strategy
% 64.03/10.22 % (3002056)------------------------------
% 64.03/10.22 % (3002056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.03/10.22 % (3002056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.03/10.22 % (3002056)CaDiCaL version: 2.1.3
% 64.03/10.22 % (3002056)Termination reason: Refutation not found, incomplete strategy
% 64.03/10.22 % (3002056)Time elapsed: 0.002 s
% 64.03/10.22 % (3002056)Peak memory usage: 87 MB
% 64.03/10.22 % (3002057)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3036172074:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2984 on theBenchmark for (2984ds/242Mi)
% 64.03/10.22 % (3002058)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1307127418:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 64.03/10.22 % (3002057)Instruction limit reached!
% 64.03/10.22 % (3002057)------------------------------
% 64.03/10.22 % (3002057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.03/10.22 % (3002057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.03/10.22 % (3002057)CaDiCaL version: 2.1.3
% 64.03/10.22 % (3002057)Termination reason: Instruction limit
% 64.03/10.22 % (3002057)Termination phase: Saturation
% 64.03/10.22 % (3002057)Time elapsed: 0.242 s
% 64.03/10.22 % (3002057)Peak memory usage: 90 MB
% 64.03/10.22 % (3002057)Instructions burned: 242 (million)
% 64.03/10.22 % (3002056)------------------------------
% 64.03/10.22 % (3002056)------------------------------
% 64.03/10.22 % (3002062)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=485838577:i=134:sd=2:doe=on:ss=axioms:sgt=14_2978 on theBenchmark for (2978ds/134Mi)
% 64.03/10.22 % (3002063)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3620287677:i=499:bd=all_2977 on theBenchmark for (2977ds/499Mi)
% 64.03/10.22 % (3002062)Instruction limit reached!
% 64.03/10.22 % (3002062)------------------------------
% 64.03/10.22 % (3002062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.03/10.22 % (3002062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.03/10.22 % (3002062)CaDiCaL version: 2.1.3
% 64.03/10.22 % (3002062)Termination reason: Instruction limit
% 64.03/10.22 % (3002062)Termination phase: Saturation
% 64.03/10.22 % (3002062)Time elapsed: 0.137 s
% 64.03/10.22 % (3002062)Peak memory usage: 89 MB
% 64.03/10.22 % (3002062)Instructions burned: 134 (million)
% 64.03/10.22 % (3002066)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=270847561:i=191:fgj=on:bd=all_2974 on theBenchmark for (2974ds/191Mi)
% 64.03/10.22 % (3002063)Instruction limit reached!
% 64.03/10.22 % (3002063)------------------------------
% 64.03/10.22 % (3002063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.03/10.22 % (3002063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.03/10.22 % (3002063)CaDiCaL version: 2.1.3
% 64.03/10.22 % (3002063)Termination reason: Instruction limit
% 64.03/10.22 % (3002063)Termination phase: Saturation
% 64.03/10.22 % (3002063)Time elapsed: 0.524 s
% 64.03/10.22 % (3002063)Peak memory usage: 93 MB
% 64.03/10.22 % (3002063)Instructions burned: 499 (million)
% 64.03/10.22 % (3002066)Instruction limit reached!
% 64.03/10.22 % (3002066)------------------------------
% 64.03/10.22 % (3002066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.03/10.22 % (3002066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.03/10.22 % (3002066)CaDiCaL version: 2.1.3
% 64.03/10.22 % (3002066)Termination reason: Instruction limit
% 64.03/10.22 % (3002066)Termination phase: Saturation
% 64.03/10.22 % (3002066)Time elapsed: 0.206 s
% 64.03/10.22 % (3002066)Peak memory usage: 91 MB
% 64.03/10.22 % (3002066)Instructions burned: 191 (million)
% 113.47/17.24 % (3002068)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=422989345:i=264:kws=precedence:fsr=off_2969 on theBenchmark for (2969ds/264Mi)
% 113.47/17.24 % (3002069)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1650732375:cond=on:i=156:bs=on:gtg=exists_all:er=known_2968 on theBenchmark for (2968ds/156Mi)
% 113.47/17.24 % (3002069)Instruction limit reached!
% 113.47/17.24 % (3002069)------------------------------
% 113.47/17.24 % (3002069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.47/17.24 % (3002069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.47/17.24 % (3002069)CaDiCaL version: 2.1.3
% 113.47/17.24 % (3002069)Termination reason: Instruction limit
% 113.47/17.24 % (3002069)Termination phase: Saturation
% 113.47/17.24 % (3002069)Time elapsed: 0.159 s
% 113.47/17.24 % (3002069)Peak memory usage: 89 MB
% 113.47/17.24 % (3002069)Instructions burned: 157 (million)
% 113.47/17.24 % (3002068)Instruction limit reached!
% 113.47/17.24 % (3002068)------------------------------
% 113.47/17.24 % (3002068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.47/17.24 % (3002068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.47/17.24 % (3002068)CaDiCaL version: 2.1.3
% 113.47/17.24 % (3002068)Termination reason: Instruction limit
% 113.47/17.24 % (3002068)Termination phase: Saturation
% 113.47/17.24 % (3002068)Time elapsed: 0.271 s
% 113.47/17.24 % (3002068)Peak memory usage: 92 MB
% 113.47/17.24 % (3002068)Instructions burned: 264 (million)
% 113.47/17.24 % (3002072)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=1618103855:i=3256:kws=precedence:bd=preordered:av=off_2964 on theBenchmark for (2964ds/3256Mi)
% 113.47/17.24 % (3002073)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1649452295:i=537:av=off:ss=included_2963 on theBenchmark for (2963ds/537Mi)
% 113.47/17.24 % (3002073)Instruction limit reached!
% 113.47/17.24 % (3002073)------------------------------
% 113.47/17.24 % (3002073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.47/17.24 % (3002073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.47/17.24 % (3002073)CaDiCaL version: 2.1.3
% 113.47/17.24 % (3002073)Termination reason: Instruction limit
% 113.47/17.24 % (3002073)Termination phase: Saturation
% 113.47/17.24 % (3002073)Time elapsed: 0.510 s
% 113.47/17.24 % (3002073)Peak memory usage: 93 MB
% 113.47/17.24 % (3002073)Instructions burned: 537 (million)
% 113.47/17.24 % (3002076)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1120957621:i=180:bd=preordered:av=off_2955 on theBenchmark for (2955ds/180Mi)
% 113.47/17.24 % (3002076)Instruction limit reached!
% 113.47/17.24 % (3002076)------------------------------
% 113.47/17.24 % (3002076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.47/17.24 % (3002076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.47/17.24 % (3002076)CaDiCaL version: 2.1.3
% 113.47/17.24 % (3002076)Termination reason: Instruction limit
% 113.47/17.24 % (3002076)Termination phase: Saturation
% 113.47/17.24 % (3002076)Time elapsed: 0.173 s
% 113.47/17.24 % (3002076)Peak memory usage: 88 MB
% 113.47/17.24 % (3002076)Instructions burned: 180 (million)
% 113.47/17.24 % (3002050)Instruction limit reached!
% 113.47/17.24 % (3002050)------------------------------
% 113.47/17.24 % (3002050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 113.47/17.24 % (3002050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 113.47/17.24 % (3002050)CaDiCaL version: 2.1.3
% 113.47/17.24 % (3002050)Termination reason: Instruction limit
% 113.47/17.24 % (3002050)Termination phase: Saturation
% 113.47/17.24 % (3002050)Time elapsed: 3.581 s
% 113.47/17.24 % (3002050)Peak memory usage: 149 MB
% 113.47/17.24 % (3002050)Instructions burned: 3394 (million)
% 113.47/17.24 % (3002078)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=2472395139:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2950 on theBenchmark for (2950ds/10307Mi)
% 113.47/17.24 % (3002079)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2433897754:i=412:gtgl=4:gtg=exists_all_2949 on theBenchmark for (2949ds/412Mi)
% 113.47/17.24 % (3002079)Instruction limit reached!
% 113.47/17.24 % (3002079)------------------------------
% 113.47/17.24 % (3002079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002079)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002079)Termination reason: Instruction limit
% 99.14/17.59 % (3002079)Termination phase: Saturation
% 99.14/17.59 % (3002079)Time elapsed: 0.415 s
% 99.14/17.59 % (3002079)Peak memory usage: 94 MB
% 99.14/17.59 % (3002079)Instructions burned: 412 (million)
% 99.14/17.59 % (3002082)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1812211403:s2pl=no:i=8478:s2at=4:nm=6_2942 on theBenchmark for (2942ds/8478Mi)
% 99.14/17.59 % (3002058)Instruction limit reached!
% 99.14/17.59 % (3002058)------------------------------
% 99.14/17.59 % (3002058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002058)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002058)Termination reason: Instruction limit
% 99.14/17.59 % (3002058)Termination phase: Saturation
% 99.14/17.59 % (3002058)Time elapsed: 5.382 s
% 99.14/17.59 % (3002058)Peak memory usage: 170 MB
% 99.14/17.59 % (3002058)Instructions burned: 5208 (million)
% 99.14/17.59 % (3002072)Instruction limit reached!
% 99.14/17.59 % (3002072)------------------------------
% 99.14/17.59 % (3002072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002072)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002072)Termination reason: Instruction limit
% 99.14/17.59 % (3002072)Termination phase: Saturation
% 99.14/17.59 % (3002072)Time elapsed: 3.497 s
% 99.14/17.59 % (3002072)Peak memory usage: 149 MB
% 99.14/17.59 % (3002072)Instructions burned: 3256 (million)
% 99.14/17.59 % (3002084)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3854650567:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2926 on theBenchmark for (2926ds/303Mi)
% 99.14/17.59 % (3002084)Refutation not found, incomplete strategy
% 99.14/17.59 % (3002084)------------------------------
% 99.14/17.59 % (3002084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002084)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002084)Termination reason: Refutation not found, incomplete strategy
% 99.14/17.59 % (3002084)Time elapsed: 0.003 s
% 99.14/17.59 % (3002084)Peak memory usage: 88 MB
% 99.14/17.59 % (3002084)Instructions burned: 1 (million)
% 99.14/17.59 % (3002085)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2842934963:st=4:i=720:sd=3:fsr=off:ss=axioms_2926 on theBenchmark for (2926ds/720Mi)
% 99.14/17.59 % (3002085)Refutation not found, incomplete strategy
% 99.14/17.59 % (3002085)------------------------------
% 99.14/17.59 % (3002085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002085)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002085)Termination reason: Refutation not found, incomplete strategy
% 99.14/17.59 % (3002085)Time elapsed: 0.002 s
% 99.14/17.59 % (3002085)Peak memory usage: 88 MB
% 99.14/17.59 % (3002084)------------------------------
% 99.14/17.59 % (3002084)------------------------------
% 99.14/17.59 % (3002085)------------------------------
% 99.14/17.59 % (3002085)------------------------------
% 99.14/17.59 % (3002088)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3992310514:i=598:bs=on:bd=preordered:av=off:ss=axioms_2919 on theBenchmark for (2919ds/598Mi)
% 99.14/17.59 % (3002089)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=852569387:i=2989:sd=3:ss=axioms:sgt=60_2919 on theBenchmark for (2919ds/2989Mi)
% 99.14/17.59 % (3002088)Instruction limit reached!
% 99.14/17.59 % (3002088)------------------------------
% 99.14/17.59 % (3002088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002088)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002088)Termination reason: Instruction limit
% 99.14/17.59 % (3002088)Termination phase: Saturation
% 99.14/17.59 % (3002088)Time elapsed: 0.640 s
% 99.14/17.59 % (3002088)Peak memory usage: 94 MB
% 99.14/17.59 % (3002088)Instructions burned: 598 (million)
% 99.14/17.59 % (3002092)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=4090490224:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2910 on theBenchmark for (2910ds/1997Mi)
% 99.14/17.59 % (3002092)Instruction limit reached!
% 99.14/17.59 % (3002092)------------------------------
% 99.14/17.59 % (3002092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002092)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002092)Termination reason: Instruction limit
% 99.14/17.59 % (3002092)Termination phase: Saturation
% 99.14/17.59 % (3002092)Time elapsed: 2.112 s
% 99.14/17.59 % (3002092)Peak memory usage: 139 MB
% 99.14/17.59 % (3002092)Instructions burned: 1997 (million)
% 99.14/17.59 % (3002089)Instruction limit reached!
% 99.14/17.59 % (3002089)------------------------------
% 99.14/17.59 % (3002089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002089)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002089)Termination reason: Instruction limit
% 99.14/17.59 % (3002089)Termination phase: Saturation
% 99.14/17.59 % (3002089)Time elapsed: 3.079 s
% 99.14/17.59 % (3002089)Peak memory usage: 147 MB
% 99.14/17.59 % (3002089)Instructions burned: 2989 (million)
% 99.14/17.59 % (3002094)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2653749855:i=2088:bd=preordered:av=off_2885 on theBenchmark for (2885ds/2088Mi)
% 99.14/17.59 % (3002095)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2475525606:i=1098:nicw=on_2885 on theBenchmark for (2885ds/1098Mi)
% 99.14/17.59 % (3002095)Instruction limit reached!
% 99.14/17.59 % (3002095)------------------------------
% 99.14/17.59 % (3002095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002095)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002095)Termination reason: Instruction limit
% 99.14/17.59 % (3002095)Termination phase: Saturation
% 99.14/17.59 % (3002095)Time elapsed: 1.130 s
% 99.14/17.59 % (3002095)Peak memory usage: 102 MB
% 99.14/17.59 % (3002095)Instructions burned: 1098 (million)
% 99.14/17.59 % (3002098)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2662879764:i=433:bd=preordered_2870 on theBenchmark for (2870ds/433Mi)
% 99.14/17.59 % (3002098)Refutation not found, incomplete strategy
% 99.14/17.59 % (3002098)------------------------------
% 99.14/17.59 % (3002098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002098)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002098)Termination reason: Refutation not found, incomplete strategy
% 99.14/17.59 % (3002098)Time elapsed: 0.004 s
% 99.14/17.59 % (3002098)Peak memory usage: 88 MB
% 99.14/17.59 % (3002098)Instructions burned: 1 (million)
% 99.14/17.59 % (3002098)------------------------------
% 99.14/17.59 % (3002098)------------------------------
% 99.14/17.59 % (3002094)Instruction limit reached!
% 99.14/17.59 % (3002094)------------------------------
% 99.14/17.59 % (3002094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002094)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002094)Termination reason: Instruction limit
% 99.14/17.59 % (3002094)Termination phase: Saturation
% 99.14/17.59 % (3002094)Time elapsed: 2.207 s
% 99.14/17.59 % (3002094)Peak memory usage: 139 MB
% 99.14/17.59 % (3002094)Instructions burned: 2088 (million)
% 99.14/17.59 % (3002100)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1975552368:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2863 on theBenchmark for (2863ds/2942Mi)
% 99.14/17.59 % (3002101)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2310221118:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2861 on theBenchmark for (2861ds/6922Mi)
% 99.14/17.59 % (3002027)First to succeed.
% 99.14/17.59 % (3002027)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3002020"
% 99.14/17.59 % (3002082)Instruction limit reached!
% 99.14/17.59 % (3002082)------------------------------
% 99.14/17.59 % (3002082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 99.14/17.59 % (3002082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.14/17.59 % (3002082)CaDiCaL version: 2.1.3
% 99.14/17.59 % (3002082)Termination reason: Instruction limit
% 99.14/17.59 % (3002082)Termination phase: Saturation
% 99.14/17.59 % (3002082)Time elapsed: 10.106 s
% 99.14/17.59 % (3002082)Peak memory usage: 164 MB
% 99.14/17.59 % (3002082)Instructions burned: 8479 (million)
% 99.14/17.59 % (3002027)Refutation found. Thanks to Tanya!
% 99.14/17.59 % SZS status Unsatisfiable for theBenchmark
% 99.14/17.59 % SZS output start Proof for theBenchmark
% See solution above
% 116.28/17.99 % (3002027)------------------------------
% 116.28/17.99 % (3002027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.28/17.99 % (3002027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.28/17.99 % (3002027)CaDiCaL version: 2.1.3
% 116.28/17.99 % (3002027)Termination reason: Refutation
% 116.28/17.99 % (3002027)Time elapsed: 15.703 s
% 116.28/17.99 % (3002027)Peak memory usage: 276 MB
% 116.28/17.99 % (3002027)Instructions burned: 18576 (million)
% 116.28/17.99 % (3002027)------------------------------
% 116.28/17.99 % (3002027)------------------------------
% 116.28/17.99 % (3002020)Success in time 16.346 s
% 116.28/17.99 % Vampire exiting
%------------------------------------------------------------------------------