%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT184-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 : n002.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:10 AM UTC 2026
% Result : Unsatisfiable 40.58s 6.87s
% Output : Refutation 41.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 11
% Syntax : Number of formulae : 304 ( 289 unt; 0 def)
% Number of atoms : 322 ( 321 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 39 ( 21 ~; 18 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 10 ( 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 : 771 ( 771 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = join(meet(X0,X1),meet(X0,join(X1,meet(X2,join(X0,meet(X1,X2)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H8) ).
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(X1,join(X0,meet(X1,X2))) = join(meet(X0,X1),meet(X1,join(X0,meet(X2,join(X1,meet(X0,X2)))))),
inference(superposition,[],[f12,f5]) ).
fof(f40,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,join(X0,X2)))) = join(meet(X1,X0),meet(X1,join(X0,meet(join(X0,X2),join(X1,X0))))),
inference(superposition,[],[f12,f3]) ).
fof(f45,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,X1))) = join(meet(X2,X0),meet(X2,join(X0,meet(X1,join(meet(X0,X1),X2))))),
inference(superposition,[],[f12,f6]) ).
fof(f51,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(meet(X0,X1),meet(X0,join(X1,meet(X0,X2)))),
inference(superposition,[],[f3,f12]) ).
fof(f52,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,meet(X0,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f51,f7]) ).
fof(f82,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f83,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f15]) ).
fof(f89,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f91,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f96,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f15,f7]) ).
fof(f98,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),X3))) = join(meet(meet(X0,X1),X2),meet(X0,meet(X1,join(X2,meet(X3,join(meet(X0,X1),meet(X2,X3))))))),
inference(superposition,[],[f12,f7]) ).
fof(f99,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,meet(meet(X0,X1),X3))) = join(meet(X0,meet(X1,X2)),meet(X0,meet(X1,join(X2,meet(X3,join(meet(X0,X1),meet(X2,X3))))))),
inference(forward_demodulation,[],[f98,f7]) ).
fof(f102,plain,
! [X2,X3,X0,X1] : join(meet(X0,meet(X1,X2)),meet(X0,meet(X1,join(X2,meet(X3,join(meet(X0,X1),meet(X2,X3))))))) = meet(X0,meet(X1,join(X2,meet(meet(X0,X1),X3)))),
inference(forward_demodulation,[],[f99,f7]) ).
fof(f105,plain,
! [X2,X3,X0,X1] : join(meet(X0,meet(X1,X2)),meet(X0,meet(X1,join(X2,meet(X3,join(meet(X0,X1),meet(X2,X3))))))) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,X3))))),
inference(forward_demodulation,[],[f102,f7]) ).
fof(f109,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f110,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f17]) ).
fof(f118,plain,
! [X2,X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))),
inference(superposition,[],[f3,f8]) ).
fof(f120,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f124,plain,
! [X2,X3,X0,X1] : meet(X3,join(join(X0,X1),meet(X3,X2))) = join(meet(X3,join(X0,X1)),meet(X3,join(X0,join(X1,meet(X2,join(X3,meet(join(X0,X1),X2))))))),
inference(superposition,[],[f12,f8]) ).
fof(f125,plain,
! [X2,X3,X0,X1] : join(meet(X3,join(X0,X1)),meet(X3,join(X0,join(X1,meet(X2,join(X3,meet(join(X0,X1),X2))))))) = meet(X3,join(X0,join(X1,meet(X3,X2)))),
inference(forward_demodulation,[],[f124,f8]) ).
fof(f135,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f109,f6]) ).
fof(f141,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f15,f109]) ).
fof(f145,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f141,f5]) ).
fof(f156,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,one),
inference(superposition,[],[f109,f9]) ).
fof(f157,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f159,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f160,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f170,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f82,f5]) ).
fof(f179,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f17,f82]) ).
fof(f183,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f179,f6]) ).
fof(f198,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f203,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(zero,X1)),
inference(superposition,[],[f109,f10]) ).
fof(f204,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f227,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f159]) ).
fof(f231,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f159]) ).
fof(f249,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f231]) ).
fof(f288,plain,
zero = complement(one),
inference(superposition,[],[f10,f227]) ).
fof(f313,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f198]) ).
fof(f423,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X3,X0)) = meet(X1,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f82,f91]) ).
fof(f482,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X1,meet(X0,meet(X1,X2))),
inference(superposition,[],[f33,f91]) ).
fof(f533,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f110,f3]) ).
fof(f542,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f110,f6]) ).
fof(f547,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X1,X0))),
inference(superposition,[],[f110,f9]) ).
fof(f567,plain,
! [X0,X1] : one = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f547,f249]) ).
fof(f574,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f533,f120]) ).
fof(f580,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f574,f8]) ).
fof(f598,plain,
! [X2,X0,X1] : join(X0,join(complement(meet(X1,X0)),X2)) = join(one,X2),
inference(superposition,[],[f8,f567]) ).
fof(f610,plain,
! [X2,X0,X1] : one = join(X0,join(complement(meet(X1,X0)),X2)),
inference(forward_demodulation,[],[f598,f231]) ).
fof(f622,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f204,f5]) ).
fof(f710,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = join(zero,meet(complement(X0),join(X0,meet(X1,join(complement(X0),meet(X0,X1)))))),
inference(superposition,[],[f35,f10]) ).
fof(f724,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(X1)))) = join(meet(X1,X0),meet(X0,join(X1,meet(complement(X1),join(X0,zero))))),
inference(superposition,[],[f35,f10]) ).
fof(f757,plain,
! [X2,X3,X0,X1] : meet(meet(X1,X0),X3) = meet(meet(X1,X0),meet(meet(X0,join(X1,meet(X0,X2))),X3)),
inference(superposition,[],[f82,f35]) ).
fof(f758,plain,
! [X2,X3,X0,X1] : meet(meet(X1,X0),X3) = meet(X1,meet(X0,meet(meet(X0,join(X1,meet(X0,X2))),X3))),
inference(forward_demodulation,[],[f757,f7]) ).
fof(f785,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(X1)))) = join(meet(X1,X0),meet(X0,join(X1,meet(complement(X1),X0)))),
inference(forward_demodulation,[],[f724,f198]) ).
fof(f795,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(X1,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f710,f313]) ).
fof(f803,plain,
! [X2,X3,X0,X1] : meet(meet(X1,X0),X3) = meet(X1,meet(X0,meet(X0,meet(join(X1,meet(X0,X2)),X3)))),
inference(forward_demodulation,[],[f758,f7]) ).
fof(f835,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X0,meet(join(X1,meet(X0,X2)),X3))) = meet(meet(X1,X0),X3),
inference(forward_demodulation,[],[f803,f33]) ).
fof(f859,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X0,meet(join(X1,meet(X0,X2)),X3))) = meet(X1,meet(X0,X3)),
inference(forward_demodulation,[],[f835,f7]) ).
fof(f874,plain,
! [X3,X0,X1] : meet(X1,meet(X3,X0)) = meet(X1,meet(X0,X3)),
inference(forward_demodulation,[],[f859,f423]) ).
fof(f1290,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(join(X2,X0),X1),meet(X0,X1)),
inference(superposition,[],[f17,f83]) ).
fof(f1317,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(X0,X1),meet(join(X2,X0),X1)),
inference(forward_demodulation,[],[f1290,f6]) ).
fof(f1410,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,f160]) ).
fof(f1418,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1410]) ).
fof(f1452,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f1418,f6]) ).
fof(f1963,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f5,f874]) ).
fof(f2093,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),X1))) = join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),join(X0,meet(X1,one)))),
inference(superposition,[],[f45,f9]) ).
fof(f2152,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),X1))) = join(meet(complement(meet(X0,X1)),X0),meet(complement(meet(X0,X1)),join(X0,X1))),
inference(forward_demodulation,[],[f2093,f159]) ).
fof(f2213,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),X1))) = join(meet(complement(meet(X0,X1)),X0),meet(join(X0,X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f2152,f5]) ).
fof(f2259,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),X1))) = join(meet(X0,complement(meet(X0,X1))),meet(join(X0,X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f2213,f5]) ).
fof(f2289,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),X1))) = meet(join(X0,X1),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f2259,f183]) ).
fof(f2311,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,X1))) = meet(complement(meet(X0,X1)),join(X0,meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2289,f5]) ).
fof(f2365,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = join(meet(X0,X1),meet(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1)))))),
inference(superposition,[],[f12,f2311]) ).
fof(f2371,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(join(X0,meet(X1,complement(meet(X0,X1)))),meet(join(X0,X1),complement(meet(X0,X1)))),
inference(superposition,[],[f17,f2311]) ).
fof(f2396,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(meet(join(X0,X1),complement(meet(X0,X1))),join(X0,meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2371,f6]) ).
fof(f2427,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(meet(X1,complement(meet(X0,X1))),join(meet(join(X0,X1),complement(meet(X0,X1))),X0)),
inference(forward_demodulation,[],[f2396,f120]) ).
fof(f2449,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(X0,join(meet(X1,complement(meet(X0,X1))),meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2427,f120]) ).
fof(f2466,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(X0,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f2449,f1317]) ).
fof(f2509,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,meet(join(X0,one),complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f2466,f156]) ).
fof(f2598,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,meet(one,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2509,f249]) ).
fof(f2635,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2598,f227]) ).
fof(f2661,plain,
! [X0,X1] : join(X0,one) = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2635,f156]) ).
fof(f2682,plain,
! [X0,X1] : one = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2661,f249]) ).
fof(f3326,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(meet(X1,X0),meet(meet(X0,join(X1,meet(X0,complement(X1)))),X2)),
inference(superposition,[],[f82,f785]) ).
fof(f3341,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X1,meet(X0,meet(meet(X0,join(X1,meet(X0,complement(X1)))),X2))),
inference(forward_demodulation,[],[f3326,f7]) ).
fof(f3392,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X1,meet(X0,meet(X0,meet(join(X1,meet(X0,complement(X1))),X2)))),
inference(forward_demodulation,[],[f3341,f7]) ).
fof(f3437,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X1,meet(X0,meet(join(X1,meet(X0,complement(X1))),X2))),
inference(forward_demodulation,[],[f3392,f33]) ).
fof(f3474,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X1,meet(X2,X0)),
inference(forward_demodulation,[],[f3437,f423]) ).
fof(f3597,plain,
! [X2,X0,X1] : meet(X0,X2) = join(meet(X0,X2),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f3474]) ).
fof(f4868,plain,
! [X2,X3,X0,X1] : meet(X2,X3) = meet(X2,meet(X3,join(X0,join(X1,X2)))),
inference(superposition,[],[f170,f120]) ).
fof(f4941,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X2,join(meet(X0,X1),X3)))),
inference(superposition,[],[f7,f170]) ).
fof(f4953,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X2,join(meet(X0,X1),X3)))),
inference(forward_demodulation,[],[f4941,f7]) ).
fof(f5612,plain,
! [X2,X3,X0,X1] : join(meet(X1,X0),X3) = join(meet(X1,X0),join(meet(meet(X0,X1),X2),X3)),
inference(superposition,[],[f110,f1963]) ).
fof(f5721,plain,
! [X2,X3,X0,X1] : join(meet(X1,X0),X3) = join(meet(X1,X0),join(meet(X0,meet(X1,X2)),X3)),
inference(forward_demodulation,[],[f5612,f7]) ).
fof(f7463,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(superposition,[],[f1452,f9]) ).
fof(f7512,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f7463,f288]) ).
fof(f7535,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f7512,f198]) ).
fof(f7549,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f7535,f5]) ).
fof(f7559,plain,
! [X0] : join(X0,complement(one)) = complement(complement(X0)),
inference(forward_subsumption_resolution,[],[f7549,f10]) ).
fof(f7567,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f7559,f288]) ).
fof(f7572,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f7567,f198]) ).
fof(f7972,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X0,meet(X1,meet(X2,join(meet(X0,X1),meet(X2,X3)))))),
inference(superposition,[],[f52,f7]) ).
fof(f8008,plain,
! [X2,X0,X1] : one = join(meet(X1,meet(X0,join(X1,meet(X0,X2)))),complement(meet(X0,X1))),
inference(superposition,[],[f567,f52]) ).
fof(f8050,plain,
! [X2,X0,X1] : one = join(complement(meet(X0,X1)),meet(X1,meet(X0,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f8008,f6]) ).
fof(f8078,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f7972,f4953]) ).
fof(f8151,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X1,X0)),
inference(forward_demodulation,[],[f8050,f170]) ).
fof(f8206,plain,
! [X0,X1] : one = join(meet(X1,X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f8151,f6]) ).
fof(f8427,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,f8206]) ).
fof(f8447,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f8427]) ).
fof(f8462,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f8447,f7]) ).
fof(f8530,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f8462,f622]) ).
fof(f8792,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X1,meet(X0,meet(X1,X2))),
inference(superposition,[],[f8078,f874]) ).
fof(f12046,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(join(complement(X1),X0),X2)))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(join(complement(X1),X0),meet(join(join(complement(X1),X0),X2),join(one,X0))))),
inference(superposition,[],[f40,f157]) ).
fof(f12176,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(join(complement(X1),X0),X2)))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(X0,meet(join(join(complement(X1),X0),X2),join(one,X0)))))),
inference(forward_demodulation,[],[f12046,f8]) ).
fof(f12304,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(join(complement(X1),X0),X2)))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(X0,meet(join(one,X0),join(join(complement(X1),X0),X2)))))),
inference(forward_demodulation,[],[f12176,f5]) ).
fof(f12400,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(complement(X1),join(X0,X2))))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(X0,meet(join(one,X0),join(complement(X1),join(X0,X2))))))),
inference(forward_demodulation,[],[f12304,f8]) ).
fof(f12470,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(complement(X1),join(X0,X2))))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(X0,meet(one,join(complement(X1),join(X0,X2))))))),
inference(forward_demodulation,[],[f12400,f231]) ).
fof(f12524,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(complement(X1),join(X0,X2))))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(X0,join(complement(X1),join(X0,X2)))))),
inference(forward_demodulation,[],[f12470,f227]) ).
fof(f12562,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(complement(X1),join(X0,X2))))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(join(X0,X2),X0)))),
inference(forward_demodulation,[],[f12524,f580]) ).
fof(f12587,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(complement(X1),join(X0,X2))))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(X0,join(X0,X2))))),
inference(forward_demodulation,[],[f12562,f6]) ).
fof(f12609,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,join(complement(X1),join(X0,X2))))) = join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(X0,X2)))),
inference(forward_demodulation,[],[f12587,f24]) ).
fof(f12630,plain,
! [X2,X0,X1] : join(meet(X1,join(complement(X1),X0)),meet(X1,join(complement(X1),join(X0,X2)))) = meet(X1,join(complement(X1),join(X0,meet(X1,join(complement(X1),join(X0,X2)))))),
inference(forward_demodulation,[],[f12609,f8]) ).
fof(f12866,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),
inference(unit_resulting_resolution,[],[f11,f204,f2682]) ).
fof(f13476,plain,
! [X2,X3,X0,X1] : join(meet(X1,meet(X0,join(X1,meet(X0,X2)))),X3) = join(meet(X1,meet(X0,join(X1,meet(X0,X2)))),join(X3,meet(X0,X1))),
inference(superposition,[],[f542,f52]) ).
fof(f13641,plain,
! [X2,X3,X0,X1] : join(meet(X1,meet(X0,join(X1,meet(X0,X2)))),X3) = join(meet(X0,X1),join(meet(X1,meet(X0,join(X1,meet(X0,X2)))),X3)),
inference(forward_demodulation,[],[f13476,f120]) ).
fof(f13683,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),X3) = join(meet(X1,meet(X0,join(X1,meet(X0,X2)))),X3),
inference(forward_demodulation,[],[f13641,f5721]) ).
fof(f13706,plain,
! [X3,X0,X1] : join(meet(X0,X1),X3) = join(meet(X1,X0),X3),
inference(forward_demodulation,[],[f13683,f170]) ).
fof(f13945,plain,
! [X2,X0,X1] : join(X2,meet(X1,X0)) = join(meet(X0,X1),X2),
inference(superposition,[],[f6,f13706]) ).
fof(f13976,plain,
! [X2,X3,X0,X1] : join(X2,meet(X1,X0)) = join(X2,join(meet(X0,X1),meet(X2,X3))),
inference(superposition,[],[f135,f13706]) ).
fof(f14046,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f13976,f135]) ).
fof(f14368,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),meet(X2,X3)) = join(X0,join(X1,meet(X3,X2))),
inference(superposition,[],[f8,f14046]) ).
fof(f14376,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,meet(X2,X3))) = join(X0,join(X1,meet(X3,X2))),
inference(forward_demodulation,[],[f14368,f8]) ).
fof(f14647,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X3,X2),meet(X1,X0)),
inference(superposition,[],[f14046,f13945]) ).
fof(f15722,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,meet(X0,X1)))))) = join(meet(X0,meet(X1,X2)),meet(X0,meet(X1,join(X2,meet(X0,X1))))),
inference(superposition,[],[f105,f3]) ).
fof(f15862,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,meet(X0,X1)))))) = join(meet(X0,meet(X1,X2)),meet(X0,X1)),
inference(forward_demodulation,[],[f15722,f96]) ).
fof(f16060,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,meet(X0,X1)))))) = join(meet(X1,X0),meet(meet(X1,X2),X0)),
inference(forward_demodulation,[],[f15862,f14647]) ).
fof(f16220,plain,
! [X2,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,meet(X1,meet(X0,X1)))))) = join(meet(X1,X0),meet(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f16060,f7]) ).
fof(f16348,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X2,meet(X0,meet(X1,meet(X0,X1)))))),
inference(forward_demodulation,[],[f16220,f3597]) ).
fof(f16448,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X2,meet(X1,meet(X0,X1))))),
inference(forward_demodulation,[],[f16348,f482]) ).
fof(f16516,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f16448,f32]) ).
fof(f16730,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f145,f4]) ).
fof(f18243,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X1,meet(X0,join(X3,meet(join(X1,X2),X0)))),meet(X0,join(X1,X2))),
inference(superposition,[],[f183,f16516]) ).
fof(f18245,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X0,join(X1,X2))) = meet(X1,meet(X0,join(X3,meet(join(X1,X2),X0)))),
inference(superposition,[],[f82,f16516]) ).
fof(f18257,plain,
! [X2,X3,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X3,meet(join(X1,X2),X0)))),
inference(forward_demodulation,[],[f18245,f170]) ).
fof(f18259,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,X2)) = join(meet(join(X1,X2),X0),meet(meet(X0,join(X3,meet(join(X1,X2),X0))),X1)),
inference(forward_demodulation,[],[f18243,f14647]) ).
fof(f18398,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,X2)) = join(meet(join(X1,X2),X0),meet(X1,meet(X0,join(X3,meet(join(X1,X2),X0))))),
inference(forward_demodulation,[],[f18259,f14046]) ).
fof(f18488,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(join(X1,X2),X0),meet(X1,X0)),
inference(forward_demodulation,[],[f18398,f18257]) ).
fof(f18536,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f18488,f14647]) ).
fof(f21447,plain,
! [X2,X0,X1] : join(X2,join(X1,X0)) = join(X2,join(X0,join(zero,X1))),
inference(superposition,[],[f203,f120]) ).
fof(f21592,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f21447,f203]) ).
fof(f21807,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f6,f21592]) ).
fof(f22072,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f118,f31]) ).
fof(f22111,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,X1),meet(X2,join(X0,join(X1,X3))))) = join(meet(X2,join(X0,X1)),meet(X2,join(join(X0,X1),meet(join(X0,join(X1,X3)),join(join(X0,X1),X2))))),
inference(superposition,[],[f45,f118]) ).
fof(f22127,plain,
! [X2,X3,X0,X1] : meet(join(join(X0,X1),X2),join(X0,join(X1,X3))) = join(join(X0,X1),meet(join(join(X0,X1),X2),join(X0,join(X1,X3)))),
inference(superposition,[],[f183,f118]) ).
fof(f22188,plain,
! [X2,X3,X0,X1] : meet(join(join(X0,X1),X2),join(X0,join(X1,X3))) = join(X0,join(X1,meet(join(join(X0,X1),X2),join(X0,join(X1,X3))))),
inference(forward_demodulation,[],[f22127,f8]) ).
fof(f22198,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,X1),meet(X2,join(X0,join(X1,X3))))) = meet(X2,join(join(X0,X1),meet(join(X0,join(X1,X3)),join(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f22111,f18536]) ).
fof(f22302,plain,
! [X2,X3,X0,X1] : meet(join(X0,join(X1,X2)),join(X0,join(X1,X3))) = join(X0,join(X1,meet(join(X0,join(X1,X2)),join(X0,join(X1,X3))))),
inference(forward_demodulation,[],[f22188,f8]) ).
fof(f22309,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,X1),meet(X2,join(X0,join(X1,X3))))) = meet(X2,join(X0,join(X1,meet(join(X0,join(X1,X3)),join(join(X0,X1),X2))))),
inference(forward_demodulation,[],[f22198,f8]) ).
fof(f22367,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,X1),meet(X2,join(X0,join(X1,X3))))) = meet(X2,join(X0,join(X1,meet(join(X0,join(X1,X3)),join(X0,join(X1,X2)))))),
inference(forward_demodulation,[],[f22309,f8]) ).
fof(f22401,plain,
! [X2,X3,X0,X1] : meet(X2,join(join(X0,X1),meet(X2,join(X0,join(X1,X3))))) = meet(X2,meet(join(X0,join(X1,X3)),join(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f22367,f22302]) ).
fof(f22423,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,join(X1,X3))) = meet(X2,join(join(X0,X1),meet(X2,join(X0,join(X1,X3))))),
inference(forward_demodulation,[],[f22401,f4868]) ).
fof(f22437,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,join(X1,X3))) = meet(X2,join(X0,join(X1,meet(X2,join(X0,join(X1,X3)))))),
inference(forward_demodulation,[],[f22423,f8]) ).
fof(f22631,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f874,f22072]) ).
fof(f22692,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f22631,f22072]) ).
fof(f23330,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X2,X1))) = meet(X3,join(X0,meet(X1,X2))),
inference(superposition,[],[f22692,f13945]) ).
fof(f23333,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f22692,f8]) ).
fof(f26468,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X0,join(X2,X1))),
inference(superposition,[],[f22692,f21807]) ).
fof(f40293,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f4,f12866]) ).
fof(f40299,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f33,f12866]) ).
fof(f40438,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f40299,f5]) ).
fof(f40443,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f40293,f6]) ).
fof(f40776,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f40438,f8530]) ).
fof(f41096,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f40776,f15]) ).
fof(f41160,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f17,f40776]) ).
fof(f41182,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(meet(X1,X0)),join(complement(X0),X2)),
inference(superposition,[],[f110,f40776]) ).
fof(f41277,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(X0),join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f41182,f120]) ).
fof(f41292,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f41160,f6]) ).
fof(f41328,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f41096,f5]) ).
fof(f41493,plain,
! [X2,X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X1,meet(X0,join(X1,meet(X0,X2))))),complement(meet(X0,X1))),
inference(superposition,[],[f41292,f52]) ).
fof(f41505,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f41292,f3]) ).
fof(f41506,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f41292,f15]) ).
fof(f41654,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f41506,f6]) ).
fof(f41655,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f41505,f6]) ).
fof(f41664,plain,
! [X2,X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(meet(X1,meet(X0,join(X1,meet(X0,X2)))))),
inference(forward_demodulation,[],[f41493,f6]) ).
fof(f41707,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f41664,f170]) ).
fof(f41744,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f41655,f7572]) ).
fof(f41964,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(superposition,[],[f41654,f7572]) ).
fof(f42300,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f15,f41744]) ).
fof(f42394,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f42300,f5]) ).
fof(f42540,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f89,f42394]) ).
fof(f43721,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f42540,f41328]) ).
fof(f45389,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = join(X2,join(complement(meet(X1,X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f21592,f41707]) ).
fof(f45392,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,join(complement(meet(X1,X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f21807,f41707]) ).
fof(f45421,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f45392,f41707]) ).
fof(f45423,plain,
! [X2,X0,X1] : join(X2,complement(meet(X1,X0))) = join(X2,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f45389,f41707]) ).
fof(f46837,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X0,X1))),
inference(superposition,[],[f41292,f45423]) ).
fof(f48609,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),complement(join(complement(X1),complement(X0)))),
inference(superposition,[],[f43721,f7572]) ).
fof(f49389,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(join(complement(X1),complement(X0)),complement(meet(X0,X1))),
inference(superposition,[],[f41964,f48609]) ).
fof(f49474,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X1,X0)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f49389,f45421]) ).
fof(f49566,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(meet(X1,X0)),complement(X1))),
inference(forward_demodulation,[],[f49474,f120]) ).
fof(f49626,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(X1),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f49566,f21592]) ).
fof(f49672,plain,
! [X0,X1] : join(complement(meet(X1,X0)),complement(X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f49626,f41277]) ).
fof(f49707,plain,
! [X0,X1] : join(complement(X1),complement(meet(X1,X0))) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f49672,f6]) ).
fof(f49736,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f49707,f40443]) ).
fof(f49793,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(superposition,[],[f49736,f7572]) ).
fof(f49800,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(X1,complement(X0))),
inference(superposition,[],[f49736,f7572]) ).
fof(f50200,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(superposition,[],[f7572,f49793]) ).
fof(f50436,plain,
! [X2,X0,X1] : complement(meet(X2,join(X0,complement(X1)))) = join(complement(X2),meet(complement(X0),X1)),
inference(superposition,[],[f49800,f49793]) ).
fof(f50437,plain,
! [X2,X0,X1] : join(complement(X2),meet(X0,complement(X1))) = complement(meet(X2,join(complement(X0),X1))),
inference(superposition,[],[f49800,f49800]) ).
fof(f50726,plain,
! [X2,X0,X1] : complement(join(X2,meet(complement(X0),X1))) = meet(complement(X2),join(X0,complement(X1))),
inference(superposition,[],[f50200,f50200]) ).
fof(f50727,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f50200,f7572]) ).
fof(f50992,plain,
! [X2,X0,X1] : complement(join(X2,meet(X0,complement(X1)))) = meet(complement(X2),join(complement(X0),X1)),
inference(superposition,[],[f50727,f49800]) ).
fof(f51065,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f5,f50727]) ).
fof(f51750,plain,
! [X0,X1] : complement(complement(X1)) = meet(complement(complement(join(X0,X1))),complement(meet(complement(X1),complement(complement(join(X0,X1)))))),
inference(superposition,[],[f12866,f51065]) ).
fof(f51796,plain,
! [X0,X1] : complement(complement(X1)) = complement(join(complement(join(X0,X1)),meet(complement(X1),complement(complement(join(X0,X1)))))),
inference(forward_demodulation,[],[f51750,f50727]) ).
fof(f51932,plain,
! [X0,X1] : complement(complement(X1)) = meet(complement(complement(join(X0,X1))),join(complement(complement(X1)),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f51796,f50992]) ).
fof(f52020,plain,
! [X0,X1] : complement(complement(X1)) = meet(complement(complement(join(X0,X1))),complement(meet(complement(X1),join(X0,X1)))),
inference(forward_demodulation,[],[f51932,f49736]) ).
fof(f52085,plain,
! [X0,X1] : complement(complement(X1)) = complement(join(complement(join(X0,X1)),meet(complement(X1),join(X0,X1)))),
inference(forward_demodulation,[],[f52020,f50727]) ).
fof(f52124,plain,
! [X0,X1] : complement(complement(X1)) = meet(complement(complement(join(X0,X1))),join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f52085,f50726]) ).
fof(f52155,plain,
! [X0,X1] : complement(complement(X1)) = meet(join(X0,X1),join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f52124,f7572]) ).
fof(f52170,plain,
! [X0,X1] : meet(join(X0,X1),join(X1,complement(join(X0,X1)))) = X1,
inference(forward_demodulation,[],[f52155,f7572]) ).
fof(f52849,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),complement(X0))),
inference(superposition,[],[f52170,f4]) ).
fof(f52850,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(meet(X1,X0),complement(X0))),
inference(superposition,[],[f52170,f17]) ).
fof(f52950,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X1,X0)))),
inference(superposition,[],[f82,f52170]) ).
fof(f53214,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f52850,f22692]) ).
fof(f53215,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f52849,f22692]) ).
fof(f53579,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,meet(complement(X0),X1))),
inference(superposition,[],[f53215,f7572]) ).
fof(f54334,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(join(meet(X0,X2),X1),complement(join(X0,X1)))),
inference(superposition,[],[f52950,f109]) ).
fof(f54483,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))) = join(meet(X0,X1),meet(X0,join(join(X1,complement(join(X0,X1))),meet(join(X0,join(X1,complement(join(X0,X1)))),complement(meet(X0,X1)))))),
inference(superposition,[],[f2365,f52950]) ).
fof(f54497,plain,
! [X2,X0,X1] : meet(X0,meet(X2,meet(X0,X1))) = meet(X0,meet(X2,join(X1,complement(join(X0,X1))))),
inference(superposition,[],[f8792,f52950]) ).
fof(f54578,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X0,meet(X2,join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f54497,f482]) ).
fof(f54591,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))) = join(meet(X0,X1),meet(X0,join(join(X1,complement(join(X0,X1))),meet(complement(meet(X0,X1)),join(X0,join(X1,complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f54483,f23330]) ).
fof(f54703,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(complement(join(X0,X1)),join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f54334,f22692]) ).
fof(f54760,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))) = join(meet(X0,X1),meet(X0,join(X1,join(complement(join(X0,X1)),meet(complement(meet(X0,X1)),join(X0,join(X1,complement(join(X0,X1))))))))),
inference(forward_demodulation,[],[f54591,f8]) ).
fof(f54847,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(X1,join(complement(join(X0,X1)),meet(X0,X2)))),
inference(forward_demodulation,[],[f54703,f23333]) ).
fof(f54887,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,join(complement(join(X0,X1)),meet(complement(meet(X0,X1)),join(X0,join(X1,complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f54760,f18536]) ).
fof(f54962,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,join(complement(join(X0,X1)),meet(complement(meet(X0,X1)),one)))),
inference(forward_demodulation,[],[f54887,f160]) ).
fof(f55016,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,join(complement(join(X0,X1)),meet(one,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f54962,f14376]) ).
fof(f55060,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,join(complement(join(X0,X1)),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f55016,f227]) ).
fof(f55095,plain,
! [X0,X1] : meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,join(complement(meet(X0,X1)),complement(join(X0,X1))))),
inference(forward_demodulation,[],[f55060,f26468]) ).
fof(f55126,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(join(X1,complement(join(X0,X1))),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f55095,f610]) ).
fof(f55152,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(X1,join(complement(join(X0,X1)),meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f55126,f8]) ).
fof(f55171,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(meet(X0,complement(meet(X0,X1))),X1)),
inference(forward_demodulation,[],[f55152,f54847]) ).
fof(f55186,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f55171,f22692]) ).
fof(f55196,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = X0,
inference(forward_demodulation,[],[f55186,f159]) ).
fof(f55422,plain,
! [X0,X1] : join(complement(X1),complement(meet(X0,X1))) = complement(meet(join(complement(X1),meet(X0,X1)),X1)),
inference(superposition,[],[f46837,f53214]) ).
fof(f55465,plain,
! [X0,X1] : join(complement(X1),complement(meet(X0,X1))) = complement(meet(X1,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[],[f55422,f8530]) ).
fof(f55634,plain,
! [X0,X1] : join(complement(X1),meet(X1,complement(meet(X0,X1)))) = join(complement(X1),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f55465,f50437]) ).
fof(f55755,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f55634,f41292]) ).
fof(f56050,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(complement(X0)),meet(complement(X0),complement(complement(join(X0,X1))))),
inference(superposition,[],[f55755,f51065]) ).
fof(f56207,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(complement(complement(X0)),complement(join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f56050,f50727]) ).
fof(f56321,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = complement(meet(complement(X0),join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f56207,f49736]) ).
fof(f56400,plain,
! [X0,X1] : join(complement(complement(X0)),meet(complement(X0),join(X0,X1))) = complement(complement(join(X0,X1))),
inference(forward_demodulation,[],[f56321,f50436]) ).
fof(f56459,plain,
! [X0,X1] : join(X0,X1) = join(complement(complement(X0)),meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f56400,f7572]) ).
fof(f56510,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f56459,f7572]) ).
fof(f64849,plain,
! [X0,X1] : join(X1,meet(X0,complement(meet(X0,X1)))) = join(join(X1,meet(X0,complement(meet(X0,X1)))),X0),
inference(superposition,[],[f17,f55196]) ).
fof(f65064,plain,
! [X0,X1] : join(X1,meet(X0,complement(meet(X0,X1)))) = join(X0,join(X1,meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f64849,f6]) ).
fof(f65259,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f65064,f135]) ).
fof(f65732,plain,
! [X0,X1] :
( zero != meet(meet(X0,complement(meet(X0,X1))),join(X1,complement(join(X0,X1))))
| join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(superposition,[],[f1452,f65259]) ).
fof(f65828,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(X1,complement(join(X0,X1)))))
| join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f65732,f7]) ).
fof(f65968,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),meet(X0,X1))
| join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f65828,f54578]) ).
fof(f66066,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X0,X1)))
| join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))) ),
inference(forward_demodulation,[],[f65968,f5]) ).
fof(f66140,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = complement(meet(X0,complement(meet(X0,X1)))),
inference(forward_subsumption_resolution,[],[f66066,f10]) ).
fof(f66183,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f66140,f49800]) ).
fof(f66486,plain,
! [X0,X1] : meet(complement(X1),join(X1,meet(complement(X1),X0))) = meet(complement(X1),join(X1,meet(X0,join(X0,complement(join(X1,X0)))))),
inference(superposition,[],[f795,f66183]) ).
fof(f66635,plain,
! [X0,X1] : meet(complement(X1),join(X1,X0)) = meet(complement(X1),join(X1,meet(complement(X1),X0))),
inference(forward_demodulation,[],[f66486,f3]) ).
fof(f66862,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X1,X0)),
inference(forward_demodulation,[],[f66635,f53579]) ).
fof(f67634,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f66862,f7572]) ).
fof(f67736,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(superposition,[],[f56510,f66862]) ).
fof(f68731,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f67634,f120]) ).
fof(f84197,plain,
! [X2,X0,X1] : join(X0,meet(complement(X0),X1)) = join(X0,meet(join(complement(X0),X2),X1)),
inference(superposition,[],[f67736,f82]) ).
fof(f84542,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,meet(join(complement(X0),X2),X1)),
inference(forward_demodulation,[],[f84197,f67736]) ).
fof(f106078,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X2,meet(X0,X1)))) = join(meet(X0,join(complement(X0),X2)),meet(X0,join(complement(X0),join(X2,meet(X1,join(X0,X1)))))),
inference(superposition,[],[f125,f84542]) ).
fof(f106328,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X2,meet(X0,X1)))) = meet(X0,join(complement(X0),join(X2,meet(X0,join(complement(X0),join(X2,meet(X1,join(X0,X1)))))))),
inference(forward_demodulation,[],[f106078,f12630]) ).
fof(f106491,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X2,meet(X0,X1)))) = meet(X0,join(complement(X0),join(X2,meet(X1,join(X0,X1))))),
inference(forward_demodulation,[],[f106328,f22437]) ).
fof(f106583,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X2,meet(X0,X1)))) = meet(X0,join(X2,meet(X1,join(X0,X1)))),
inference(forward_demodulation,[],[f106491,f67634]) ).
fof(f106633,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(complement(X0),join(X2,meet(X0,X1)))),
inference(forward_demodulation,[],[f106583,f15]) ).
fof(f106663,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,join(X2,X1)),
inference(forward_demodulation,[],[f106633,f67634]) ).
fof(f112006,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,join(X2,join(complement(X0),X1))),
inference(superposition,[],[f106663,f67634]) ).
fof(f112199,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f16730,f106663]) ).
fof(f112660,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,join(X1,X2)),
inference(forward_demodulation,[],[f112006,f68731]) ).
fof(f113745,plain,
meet(a,join(b,c)) != meet(a,join(meet(a,b),c)),
inference(superposition,[],[f13,f112199]) ).
fof(f114067,plain,
meet(a,join(b,c)) != meet(a,join(c,meet(a,b))),
inference(forward_demodulation,[],[f113745,f22692]) ).
fof(f114390,plain,
$false,
inference(forward_subsumption_resolution,[],[f114067,f112660]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT184-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.40 % Computer : n002.cluster.edu
% 0.16/0.40 % Model : x86_64 x86_64
% 0.16/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.40 % Memory : 8046.5625MB
% 0.16/0.40 % OS : Linux 6.8.0-71-generic
% 0.16/0.40 % CPULimit : 300
% 0.16/0.40 % WCLimit : 300
% 0.16/0.40 % DateTime : Sun Sep 27 14:07:36 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.16/0.47 Running first-order theorem proving
% 0.16/0.47 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
% 17.93/3.70 % (3557233)Input is clausal, will run a generic CNF schedule.
% 17.93/3.70 % (3557244)dis-21_1_sil=8000:lcm=predicate:random_seed=2367712246: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)
% 17.93/3.70 % (3557244)Refutation not found, incomplete strategy
% 17.93/3.70 % (3557244)------------------------------
% 17.93/3.70 % (3557244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.93/3.70 % (3557244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.93/3.70 % (3557244)CaDiCaL version: 2.1.3
% 17.93/3.70 % (3557244)Termination reason: Refutation not found, incomplete strategy
% 17.93/3.70 % (3557244)Time elapsed: 0.002 s
% 17.93/3.70 % (3557244)Peak memory usage: 88 MB
% 17.93/3.70 % (3557244)Instructions burned: 1 (million)
% 17.93/3.70 % (3557241)lrs+10_1_sil=8000:sp=occurrence:random_seed=1816455498:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.93/3.70 % (3557240)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=907595313:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.93/3.71 % (3557239)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=871324383:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.93/3.71 % (3557238)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=3546659925:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.93/3.71 % (3557242)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1942586256:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.93/3.71 % (3557243)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=478659472:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.93/3.71 % (3557242)Instruction limit reached!
% 17.93/3.71 % (3557242)------------------------------
% 17.93/3.71 % (3557242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.93/3.71 % (3557242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.93/3.71 % (3557242)CaDiCaL version: 2.1.3
% 17.93/3.71 % (3557242)Termination reason: Instruction limit
% 17.93/3.71 % (3557242)Termination phase: Saturation
% 17.93/3.71 % (3557242)Time elapsed: 0.067 s
% 17.93/3.71 % (3557242)Peak memory usage: 89 MB
% 17.93/3.71 % (3557242)Instructions burned: 115 (million)
% 17.93/3.71 % (3557241)Instruction limit reached!
% 17.93/3.71 % (3557241)------------------------------
% 17.93/3.71 % (3557241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.93/3.71 % (3557241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.93/3.71 % (3557241)CaDiCaL version: 2.1.3
% 17.93/3.71 % (3557241)Termination reason: Instruction limit
% 17.93/3.71 % (3557241)Termination phase: Saturation
% 17.93/3.71 % (3557241)Time elapsed: 0.111 s
% 17.93/3.71 % (3557241)Peak memory usage: 88 MB
% 17.93/3.71 % (3557241)Instructions burned: 107 (million)
% 17.93/3.71 % (3557243)Instruction limit reached!
% 17.93/3.71 % (3557243)------------------------------
% 17.93/3.71 % (3557243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.93/3.71 % (3557243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.93/3.71 % (3557243)CaDiCaL version: 2.1.3
% 17.93/3.71 % (3557243)Termination reason: Instruction limit
% 17.93/3.71 % (3557243)Termination phase: Saturation
% 17.93/3.71 % (3557243)Time elapsed: 0.168 s
% 17.93/3.71 % (3557243)Peak memory usage: 89 MB
% 17.93/3.71 % (3557243)Instructions burned: 180 (million)
% 17.93/3.71 % (3557244)------------------------------
% 17.93/3.71 % (3557244)------------------------------
% 17.93/3.71 % (3557253)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=897313718:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 17.93/3.71 % (3557253)Refutation not found, incomplete strategy
% 17.93/3.71 % (3557253)------------------------------
% 17.93/3.71 % (3557253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.93/3.71 % (3557253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.93/3.71 % (3557253)CaDiCaL version: 2.1.3
% 17.93/3.71 % (3557253)Termination reason: Refutation not found, incomplete strategy
% 17.93/3.71 % (3557253)Time elapsed: 0.001 s
% 37.43/6.40 % (3557253)Peak memory usage: 88 MB
% 37.43/6.40 % (3557253)Instructions burned: 1 (million)
% 37.43/6.40 % (3557252)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=1702071798:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 37.43/6.40 % (3557252)Refutation not found, incomplete strategy
% 37.43/6.40 % (3557252)------------------------------
% 37.43/6.40 % (3557252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.43/6.40 % (3557252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.43/6.40 % (3557252)CaDiCaL version: 2.1.3
% 37.43/6.40 % (3557252)Termination reason: Refutation not found, incomplete strategy
% 37.43/6.40 % (3557252)Time elapsed: 0.002 s
% 37.43/6.40 % (3557252)Peak memory usage: 88 MB
% 37.43/6.40 % (3557254)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=946261265:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 37.43/6.40 % (3557254)Refutation not found, incomplete strategy
% 37.43/6.40 % (3557254)------------------------------
% 37.43/6.40 % (3557254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.43/6.40 % (3557254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.43/6.40 % (3557254)CaDiCaL version: 2.1.3
% 37.43/6.40 % (3557254)Termination reason: Refutation not found, incomplete strategy
% 37.43/6.40 % (3557254)Time elapsed: 0.001 s
% 37.43/6.40 % (3557254)Peak memory usage: 88 MB
% 37.43/6.40 % (3557253)------------------------------
% 37.43/6.40 % (3557253)------------------------------
% 37.43/6.40 % (3557255)lrs+10_64_to=lpo:sil=8000:random_seed=203243174:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 37.43/6.40 % (3557254)------------------------------
% 37.43/6.40 % (3557254)------------------------------
% 37.43/6.40 % (3557255)Instruction limit reached!
% 37.43/6.40 % (3557255)------------------------------
% 37.43/6.40 % (3557255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.43/6.40 % (3557255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.43/6.40 % (3557255)CaDiCaL version: 2.1.3
% 37.43/6.40 % (3557255)Termination reason: Instruction limit
% 37.43/6.40 % (3557255)Termination phase: Saturation
% 37.43/6.40 % (3557255)Time elapsed: 0.119 s
% 37.43/6.40 % (3557255)Peak memory usage: 88 MB
% 37.43/6.40 % (3557255)Instructions burned: 126 (million)
% 37.43/6.40 % (3557252)------------------------------
% 37.43/6.40 % (3557252)------------------------------
% 37.43/6.40 % (3557259)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1995883440:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 37.43/6.40 % (3557259)Instruction limit reached!
% 37.43/6.40 % (3557259)------------------------------
% 37.43/6.40 % (3557259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.43/6.40 % (3557259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.43/6.40 % (3557259)CaDiCaL version: 2.1.3
% 37.43/6.40 % (3557259)Termination reason: Instruction limit
% 37.43/6.40 % (3557259)Termination phase: Saturation
% 37.43/6.40 % (3557259)Time elapsed: 0.139 s
% 37.43/6.40 % (3557259)Peak memory usage: 89 MB
% 37.43/6.40 % (3557259)Instructions burned: 194 (million)
% 37.43/6.40 % (3557262)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3959715275:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 37.43/6.40 % (3557261)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4095181958:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 37.43/6.40 % (3557263)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=4021865494:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 37.43/6.40 % (3557263)Instruction limit reached!
% 37.43/6.40 % (3557263)------------------------------
% 37.43/6.40 % (3557263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 37.43/6.40 % (3557263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.43/6.40 % (3557263)CaDiCaL version: 2.1.3
% 37.43/6.40 % (3557263)Termination reason: Instruction limit
% 37.43/6.40 % (3557263)Termination phase: Saturation
% 37.43/6.40 % (3557263)Time elapsed: 0.106 s
% 37.43/6.40 % (3557263)Peak memory usage: 89 MB
% 37.43/6.40 % (3557263)Instructions burned: 106 (million)
% 37.43/6.40 % (3557261)Instruction limit reached!
% 37.43/6.40 % (3557261)------------------------------
% 40.58/6.87 % (3557261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557261)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557261)Termination reason: Instruction limit
% 40.58/6.87 % (3557261)Termination phase: Saturation
% 40.58/6.87 % (3557261)Time elapsed: 0.152 s
% 40.58/6.87 % (3557261)Peak memory usage: 90 MB
% 40.58/6.87 % (3557261)Instructions burned: 157 (million)
% 40.58/6.87 % (3557265)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1767264963:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 40.58/6.87 % (3557265)Refutation not found, incomplete strategy
% 40.58/6.87 % (3557265)------------------------------
% 40.58/6.87 % (3557265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557265)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557265)Termination reason: Refutation not found, incomplete strategy
% 40.58/6.87 % (3557265)Time elapsed: 0.002 s
% 40.58/6.87 % (3557265)Peak memory usage: 87 MB
% 40.58/6.87 % (3557269)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1098543263:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 40.58/6.87 % (3557270)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4179063683:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 40.58/6.87 % (3557269)Instruction limit reached!
% 40.58/6.87 % (3557269)------------------------------
% 40.58/6.87 % (3557269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557269)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557269)Termination reason: Instruction limit
% 40.58/6.87 % (3557269)Termination phase: Saturation
% 40.58/6.87 % (3557269)Time elapsed: 0.184 s
% 40.58/6.87 % (3557269)Peak memory usage: 90 MB
% 40.58/6.87 % (3557269)Instructions burned: 242 (million)
% 40.58/6.87 % (3557265)------------------------------
% 40.58/6.87 % (3557265)------------------------------
% 40.58/6.87 % (3557274)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2392006964:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 40.58/6.87 % (3557274)Instruction limit reached!
% 40.58/6.87 % (3557274)------------------------------
% 40.58/6.87 % (3557274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557274)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557274)Termination reason: Instruction limit
% 40.58/6.87 % (3557274)Termination phase: Saturation
% 40.58/6.87 % (3557274)Time elapsed: 0.123 s
% 40.58/6.87 % (3557274)Peak memory usage: 89 MB
% 40.58/6.87 % (3557274)Instructions burned: 134 (million)
% 40.58/6.87 % (3557275)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=419591181:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 40.58/6.87 % (3557277)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1295314551:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 40.58/6.87 % (3557277)Instruction limit reached!
% 40.58/6.87 % (3557277)------------------------------
% 40.58/6.87 % (3557277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557277)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557277)Termination reason: Instruction limit
% 40.58/6.87 % (3557277)Termination phase: Saturation
% 40.58/6.87 % (3557277)Time elapsed: 0.187 s
% 40.58/6.87 % (3557277)Peak memory usage: 91 MB
% 40.58/6.87 % (3557277)Instructions burned: 192 (million)
% 40.58/6.87 % (3557275)Instruction limit reached!
% 40.58/6.87 % (3557275)------------------------------
% 40.58/6.87 % (3557275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557275)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557275)Termination reason: Instruction limit
% 40.58/6.87 % (3557275)Termination phase: Saturation
% 40.58/6.87 % (3557275)Time elapsed: 0.511 s
% 40.58/6.87 % (3557275)Peak memory usage: 95 MB
% 40.58/6.87 % (3557275)Instructions burned: 500 (million)
% 40.58/6.87 % (3557280)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1631848714:i=264:kws=precedence:fsr=off_2974 on theBenchmark for (2974ds/264Mi)
% 40.58/6.87 % (3557281)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2604994368:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 40.58/6.87 % (3557281)Instruction limit reached!
% 40.58/6.87 % (3557281)------------------------------
% 40.58/6.87 % (3557281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557281)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557281)Termination reason: Instruction limit
% 40.58/6.87 % (3557281)Termination phase: Saturation
% 40.58/6.87 % (3557281)Time elapsed: 0.152 s
% 40.58/6.87 % (3557281)Peak memory usage: 89 MB
% 40.58/6.87 % (3557281)Instructions burned: 156 (million)
% 40.58/6.87 % (3557280)Instruction limit reached!
% 40.58/6.87 % (3557280)------------------------------
% 40.58/6.87 % (3557280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557280)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557280)Termination reason: Instruction limit
% 40.58/6.87 % (3557280)Termination phase: Saturation
% 40.58/6.87 % (3557280)Time elapsed: 0.251 s
% 40.58/6.87 % (3557280)Peak memory usage: 92 MB
% 40.58/6.87 % (3557280)Instructions burned: 264 (million)
% 40.58/6.87 % (3557284)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=2023481137:i=3256:kws=precedence:bd=preordered:av=off_2969 on theBenchmark for (2969ds/3256Mi)
% 40.58/6.87 % (3557285)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2073070813:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi)
% 40.58/6.87 % (3557285)Instruction limit reached!
% 40.58/6.87 % (3557285)------------------------------
% 40.58/6.87 % (3557285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557285)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557285)Termination reason: Instruction limit
% 40.58/6.87 % (3557285)Termination phase: Saturation
% 40.58/6.87 % (3557285)Time elapsed: 0.492 s
% 40.58/6.87 % (3557285)Peak memory usage: 93 MB
% 40.58/6.87 % (3557285)Instructions burned: 538 (million)
% 40.58/6.87 % (3557288)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3594687964:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi)
% 40.58/6.87 % (3557288)Instruction limit reached!
% 40.58/6.87 % (3557288)------------------------------
% 40.58/6.87 % (3557288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557288)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557288)Termination reason: Instruction limit
% 40.58/6.87 % (3557288)Termination phase: Saturation
% 40.58/6.87 % (3557288)Time elapsed: 0.169 s
% 40.58/6.87 % (3557288)Peak memory usage: 88 MB
% 40.58/6.87 % (3557288)Instructions burned: 180 (million)
% 40.58/6.87 % (3557290)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=1106679000:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi)
% 40.58/6.87 % (3557262)Instruction limit reached!
% 40.58/6.87 % (3557262)------------------------------
% 40.58/6.87 % (3557262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557262)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557262)Termination reason: Instruction limit
% 40.58/6.87 % (3557262)Termination phase: Saturation
% 40.58/6.87 % (3557262)Time elapsed: 3.408 s
% 40.58/6.87 % (3557262)Peak memory usage: 150 MB
% 40.58/6.87 % (3557262)Instructions burned: 3394 (million)
% 40.58/6.87 % (3557292)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=1617079952:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 40.58/6.87 % (3557292)Instruction limit reached!
% 40.58/6.87 % (3557292)------------------------------
% 40.58/6.87 % (3557292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.58/6.87 % (3557292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.58/6.87 % (3557292)CaDiCaL version: 2.1.3
% 40.58/6.87 % (3557292)Termination reason: Instruction limit
% 40.58/6.87 % (3557292)Termination phase: Saturation
% 40.58/6.87 % (3557292)Time elapsed: 0.389 s
% 40.58/6.87 % (3557292)Peak memory usage: 94 MB
% 40.58/6.87 % (3557292)Instructions burned: 413 (million)
% 40.58/6.87 % (3557239)First to succeed.
% 40.58/6.87 % (3557239)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3557233"
% 40.58/6.87 % (3557296)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=1606124525:s2pl=no:i=8478:s2at=4:nm=6_2946 on theBenchmark for (2946ds/8478Mi)
% 40.58/6.87 % (3557239)Refutation found. Thanks to Tanya!
% 40.58/6.87 % SZS status Unsatisfiable for theBenchmark
% 40.58/6.87 % SZS output start Proof for theBenchmark
% See solution above
% 41.48/7.01 % (3557239)------------------------------
% 41.48/7.01 % (3557239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.48/7.01 % (3557239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.48/7.01 % (3557239)CaDiCaL version: 2.1.3
% 41.48/7.01 % (3557239)Termination reason: Refutation
% 41.48/7.01 % (3557239)Time elapsed: 5.261 s
% 41.48/7.01 % (3557239)Peak memory usage: 194 MB
% 41.48/7.01 % (3557239)Instructions burned: 8732 (million)
% 41.48/7.01 % (3557239)------------------------------
% 41.48/7.01 % (3557239)------------------------------
% 41.48/7.01 % (3557233)Success in time 5.781 s
% 41.48/7.01 % Vampire exiting
%------------------------------------------------------------------------------