%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT217-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 : n014.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:17 AM UTC 2026
% Result : Unsatisfiable 148.18s 31.08s
% Output : Refutation 215.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 98
% Number of leaves : 12
% Syntax : Number of formulae : 493 ( 467 unt; 0 def)
% Number of atoms : 522 ( 521 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 60 ( 31 ~; 29 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 12 ( 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 : 1216 (1216 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H82) ).
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(f14,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,X2)),X0),meet(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = meet(meet(X1,join(X0,X2)),join(join(meet(X0,X1),meet(X0,X2)),meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,X2)),X0)))),
inference(superposition,[],[f12,f12]) ).
fof(f19,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(X0,X2)),meet(join(X0,X1),X2))),
inference(superposition,[],[f12,f5]) ).
fof(f23,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,X2)),X0),meet(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = meet(X1,meet(join(X0,X2),join(join(meet(X0,X1),meet(X0,X2)),meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,X2)),X0))))),
inference(forward_demodulation,[],[f14,f7]) ).
fof(f25,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,X2)),X0),meet(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = meet(X1,meet(join(X0,X2),join(meet(X0,X1),join(meet(X0,X2),meet(meet(X2,join(X0,X1)),join(meet(X1,join(X0,X2)),X0)))))),
inference(forward_demodulation,[],[f23,f8]) ).
fof(f27,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,X2)),X0),meet(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = meet(X1,meet(join(X0,X2),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(meet(X1,join(X0,X2)),X0))))))),
inference(forward_demodulation,[],[f25,f7]) ).
fof(f29,plain,
! [X2,X0,X1] : join(meet(meet(X1,join(X0,X2)),X0),meet(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))) = meet(X1,meet(join(X0,X2),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X1,join(X0,X2))))))))),
inference(forward_demodulation,[],[f27,f6]) ).
fof(f31,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,X2),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X1,join(X0,X2))))))))) = join(meet(meet(X1,join(X0,X2)),X0),meet(X1,meet(join(X0,X2),meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f29,f7]) ).
fof(f33,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,X2),join(meet(X0,X1),join(meet(X0,X2),meet(X2,meet(join(X0,X1),join(X0,meet(X1,join(X0,X2))))))))) = join(meet(X0,meet(X1,join(X0,X2))),meet(X1,meet(join(X0,X2),meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f31,f5]) ).
fof(f39,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,join(X1,X2)),meet(X2,join(X1,X0)))) = join(meet(X1,X2),meet(X1,X0)),
inference(superposition,[],[f12,f6]) ).
fof(f40,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,X2)) = meet(X1,join(meet(X0,join(X1,X2)),meet(X2,join(X0,X1)))),
inference(superposition,[],[f12,f6]) ).
fof(f41,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(X1,X0)) = meet(X1,join(meet(X2,join(X0,X1)),meet(X0,join(X1,X2)))),
inference(superposition,[],[f12,f6]) ).
fof(f43,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f53,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f64,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f43,f4]) ).
fof(f70,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f64,f5]) ).
fof(f75,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f53,f43]) ).
fof(f76,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f43,f53]) ).
fof(f82,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f76,f5]) ).
fof(f83,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f75,f6]) ).
fof(f96,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f97,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f43]) ).
fof(f107,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f121,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f122,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f53]) ).
fof(f128,plain,
! [X2,X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))),
inference(superposition,[],[f3,f8]) ).
fof(f130,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f135,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(X2,join(X0,X1)))),
inference(superposition,[],[f53,f8]) ).
fof(f146,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f96,f5]) ).
fof(f169,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f170,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f172,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(X0))) = meet(X0,join(meet(X1,one),meet(complement(X0),join(X0,X1)))),
inference(superposition,[],[f12,f9]) ).
fof(f173,plain,
! [X0] : complement(X0) = meet(complement(X0),one),
inference(superposition,[],[f43,f9]) ).
fof(f174,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(one,X1)),
inference(superposition,[],[f96,f9]) ).
fof(f175,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f176,plain,
! [X0] : complement(X0) = meet(one,complement(X0)),
inference(forward_demodulation,[],[f173,f5]) ).
fof(f177,plain,
! [X0,X1] : meet(X0,join(meet(X1,one),meet(complement(X0),join(X0,X1)))) = join(meet(X0,X1),zero),
inference(forward_demodulation,[],[f172,f10]) ).
fof(f179,plain,
! [X0,X1] : meet(X0,join(meet(X1,one),meet(complement(X0),join(X0,X1)))) = join(zero,meet(X0,X1)),
inference(forward_demodulation,[],[f177,f6]) ).
fof(f181,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = meet(X0,join(X1,meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f179,f169]) ).
fof(f191,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f121,f6]) ).
fof(f219,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f221,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f222,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f238,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f53,f169]) ).
fof(f241,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f169]) ).
fof(f251,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f6,f238]) ).
fof(f294,plain,
zero = complement(one),
inference(superposition,[],[f10,f241]) ).
fof(f322,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f221]) ).
fof(f325,plain,
! [X0,X1] : join(meet(X0,zero),meet(X0,X1)) = meet(X0,join(meet(zero,join(X0,X1)),meet(X1,X0))),
inference(superposition,[],[f12,f221]) ).
fof(f327,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f43,f221]) ).
fof(f333,plain,
! [X0,X1] : join(meet(X0,zero),meet(X0,X1)) = meet(X0,join(meet(X1,X0),meet(zero,join(X0,X1)))),
inference(forward_demodulation,[],[f325,f6]) ).
fof(f335,plain,
! [X0,X1] : join(meet(X0,zero),meet(X0,X1)) = meet(X0,join(meet(X1,X0),zero)),
inference(forward_demodulation,[],[f333,f327]) ).
fof(f337,plain,
! [X0,X1] : join(meet(X0,zero),meet(X0,X1)) = meet(X0,join(zero,meet(X1,X0))),
inference(forward_demodulation,[],[f335,f6]) ).
fof(f339,plain,
! [X0,X1] : meet(X0,meet(X1,X0)) = join(meet(X0,zero),meet(X0,X1)),
inference(forward_demodulation,[],[f337,f322]) ).
fof(f340,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X0,zero),meet(X0,X1)),
inference(forward_demodulation,[],[f339,f82]) ).
fof(f358,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f53,f322]) ).
fof(f537,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,f175]) ).
fof(f538,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,complement(join(X0,X1)))),meet(X0,X2)) = meet(X0,join(meet(join(X1,complement(join(X0,X1))),join(X0,X2)),meet(X2,one))),
inference(superposition,[],[f12,f175]) ).
fof(f545,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f537]) ).
fof(f550,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,complement(join(X0,X1)))),meet(X0,X2)) = meet(X0,join(meet(X2,one),meet(join(X1,complement(join(X0,X1))),join(X0,X2)))),
inference(forward_demodulation,[],[f538,f6]) ).
fof(f567,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,complement(join(X0,X1)))),meet(X0,X2)) = meet(X0,join(X2,meet(join(X1,complement(join(X0,X1))),join(X0,X2)))),
inference(forward_demodulation,[],[f550,f169]) ).
fof(f576,plain,
! [X0,X1] :
( zero != meet(X1,join(X0,complement(join(X0,X1))))
| complement(X1) = join(X0,complement(join(X0,X1))) ),
inference(superposition,[],[f545,f6]) ).
fof(f630,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X1,meet(X0,meet(X1,X2))),
inference(superposition,[],[f70,f107]) ).
fof(f673,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f222,f5]) ).
fof(f963,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f97,f5]) ).
fof(f967,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X3,X0)) = meet(X2,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f97,f107]) ).
fof(f1235,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f122,f6]) ).
fof(f1243,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X1,X0))),
inference(superposition,[],[f122,f9]) ).
fof(f1289,plain,
! [X0,X1] : one = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f1243,f251]) ).
fof(f1364,plain,
! [X0,X1] : join(zero,meet(X0,complement(meet(X1,X0)))) = meet(X0,join(complement(meet(X1,X0)),meet(complement(X0),one))),
inference(superposition,[],[f181,f1289]) ).
fof(f1377,plain,
! [X0,X1] : join(zero,meet(X0,complement(meet(X1,X0)))) = meet(X0,join(meet(complement(X0),one),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f1364,f6]) ).
fof(f1397,plain,
! [X0,X1] : join(zero,meet(X0,complement(meet(X1,X0)))) = meet(X0,join(meet(one,complement(X0)),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f1377,f5]) ).
fof(f1409,plain,
! [X0,X1] : join(zero,meet(X0,complement(meet(X1,X0)))) = meet(X0,join(complement(X0),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f1397,f176]) ).
fof(f1415,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(X0,join(complement(X0),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f1409,f322]) ).
fof(f1571,plain,
! [X0,X1] : meet(X0,join(meet(complement(X0),join(X0,X1)),meet(X1,one))) = join(meet(X0,X1),meet(X0,complement(X0))),
inference(superposition,[],[f39,f9]) ).
fof(f1647,plain,
! [X0,X1] : meet(X0,join(meet(complement(X0),join(X0,X1)),meet(X1,one))) = join(meet(X0,X1),zero),
inference(forward_demodulation,[],[f1571,f10]) ).
fof(f1701,plain,
! [X0,X1] : meet(X0,join(meet(complement(X0),join(X0,X1)),meet(X1,one))) = join(zero,meet(X0,X1)),
inference(forward_demodulation,[],[f1647,f6]) ).
fof(f1737,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(complement(X0),join(X0,X1)),meet(X1,one))),
inference(forward_demodulation,[],[f1701,f322]) ).
fof(f1768,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X1,one),meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f1737,f6]) ).
fof(f1791,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f1768,f169]) ).
fof(f2143,plain,
! [X0,X1] :
( one != join(one,X0)
| zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(superposition,[],[f11,f170]) ).
fof(f2182,plain,
! [X0,X1] :
( zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(forward_subsumption_resolution,[],[f2143,f238]) ).
fof(f3045,plain,
! [X0,X1] : join(meet(X1,X0),meet(X1,meet(complement(X0),join(X0,X1)))) = meet(X1,join(meet(X0,X1),meet(meet(complement(X0),join(X0,X1)),join(X0,X1)))),
inference(superposition,[],[f40,f1791]) ).
fof(f3070,plain,
! [X0,X1] : join(meet(complement(X0),X0),meet(complement(X0),X1)) = meet(complement(X0),join(meet(X0,join(complement(X0),X1)),meet(X1,one))),
inference(superposition,[],[f40,f9]) ).
fof(f3164,plain,
! [X0,X1] : join(meet(complement(X0),X0),meet(complement(X0),X1)) = meet(complement(X0),join(meet(X1,one),meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f3070,f6]) ).
fof(f3186,plain,
! [X0,X1] : join(meet(X1,X0),meet(X1,meet(complement(X0),join(X0,X1)))) = meet(X1,join(meet(X0,X1),meet(join(X0,X1),meet(complement(X0),join(X0,X1))))),
inference(forward_demodulation,[],[f3045,f5]) ).
fof(f3237,plain,
! [X0,X1] : join(meet(complement(X0),X0),meet(complement(X0),X1)) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f3164,f169]) ).
fof(f3255,plain,
! [X0,X1] : join(meet(X1,X0),meet(X1,meet(complement(X0),join(X0,X1)))) = meet(X1,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f3186,f82]) ).
fof(f3295,plain,
! [X0,X1] : meet(complement(X0),join(X1,meet(X0,join(complement(X0),X1)))) = join(meet(X0,complement(X0)),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f3237,f5]) ).
fof(f3313,plain,
! [X0,X1] : join(meet(X1,X0),meet(X1,complement(X0))) = meet(X1,join(meet(X0,X1),meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f3255,f963]) ).
fof(f3342,plain,
! [X0,X1] : join(zero,meet(complement(X0),X1)) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f3295,f10]) ).
fof(f3376,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f3342,f322]) ).
fof(f3517,plain,
! [X0,X1] : meet(complement(X0),join(X1,complement(join(complement(X0),X1)))) = meet(complement(X0),join(join(X1,complement(join(complement(X0),X1))),meet(X0,one))),
inference(superposition,[],[f3376,f175]) ).
fof(f3546,plain,
! [X0,X1] : join(meet(X1,complement(X0)),meet(X1,meet(X0,join(complement(X0),X1)))) = meet(X1,join(meet(complement(X0),X1),meet(meet(X0,join(complement(X0),X1)),join(complement(X0),X1)))),
inference(superposition,[],[f40,f3376]) ).
fof(f3575,plain,
! [X0,X1] : join(meet(X1,complement(X0)),meet(X1,meet(X0,join(complement(X0),X1)))) = meet(X1,join(meet(complement(X0),X1),meet(join(complement(X0),X1),meet(X0,join(complement(X0),X1))))),
inference(forward_demodulation,[],[f3546,f5]) ).
fof(f3596,plain,
! [X0,X1] : meet(complement(X0),join(X1,complement(join(complement(X0),X1)))) = meet(complement(X0),join(meet(X0,one),join(X1,complement(join(complement(X0),X1))))),
inference(forward_demodulation,[],[f3517,f6]) ).
fof(f3608,plain,
! [X0,X1] : join(meet(X1,complement(X0)),meet(X1,meet(X0,join(complement(X0),X1)))) = meet(X1,join(meet(complement(X0),X1),meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f3575,f82]) ).
fof(f3624,plain,
! [X0,X1] : meet(complement(X0),join(X1,complement(join(complement(X0),X1)))) = meet(complement(X0),join(X0,join(X1,complement(join(complement(X0),X1))))),
inference(forward_demodulation,[],[f3596,f169]) ).
fof(f3633,plain,
! [X0,X1] : meet(X1,join(meet(complement(X0),X1),meet(X0,join(complement(X0),X1)))) = join(meet(X1,complement(X0)),meet(X1,X0)),
inference(forward_demodulation,[],[f3608,f963]) ).
fof(f3651,plain,
! [X0,X1] : join(meet(X1,X0),meet(X1,complement(X0))) = meet(X1,join(meet(complement(X0),X1),meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f3633,f6]) ).
fof(f3694,plain,
! [X0,X1] : join(meet(meet(complement(X1),X0),X1),meet(meet(complement(X1),X0),complement(X1))) = meet(meet(complement(X1),X0),join(meet(zero,X0),meet(complement(X1),join(X1,meet(complement(X1),X0))))),
inference(superposition,[],[f3313,f219]) ).
fof(f3838,plain,
! [X0,X1] : join(meet(meet(complement(X1),X0),X1),meet(meet(complement(X1),X0),complement(X1))) = meet(complement(X1),meet(X0,join(meet(zero,X0),meet(complement(X1),join(X1,meet(complement(X1),X0)))))),
inference(forward_demodulation,[],[f3694,f7]) ).
fof(f3900,plain,
! [X0,X1] : join(meet(meet(complement(X1),X0),X1),meet(meet(complement(X1),X0),complement(X1))) = meet(complement(X1),meet(X0,join(zero,meet(complement(X1),join(X1,meet(complement(X1),X0)))))),
inference(forward_demodulation,[],[f3838,f327]) ).
fof(f3955,plain,
! [X0,X1] : join(meet(meet(complement(X1),X0),X1),meet(meet(complement(X1),X0),complement(X1))) = meet(complement(X1),meet(X0,meet(complement(X1),join(X1,meet(complement(X1),X0))))),
inference(forward_demodulation,[],[f3900,f322]) ).
fof(f4000,plain,
! [X0,X1] : join(meet(meet(complement(X1),X0),X1),meet(meet(complement(X1),X0),complement(X1))) = meet(X0,meet(complement(X1),join(X1,meet(complement(X1),X0)))),
inference(forward_demodulation,[],[f3955,f630]) ).
fof(f4040,plain,
! [X0,X1] : meet(X0,meet(complement(X1),join(X1,meet(complement(X1),X0)))) = join(meet(meet(complement(X1),X0),X1),meet(complement(X1),meet(complement(X1),X0))),
inference(forward_demodulation,[],[f4000,f5]) ).
fof(f4070,plain,
! [X0,X1] : meet(X0,meet(complement(X1),join(X1,meet(complement(X1),X0)))) = join(meet(meet(complement(X1),X0),X1),meet(complement(X1),X0)),
inference(forward_demodulation,[],[f4040,f70]) ).
fof(f4092,plain,
! [X0,X1] : meet(X0,meet(complement(X1),join(X1,meet(complement(X1),X0)))) = join(meet(complement(X1),X0),meet(meet(complement(X1),X0),X1)),
inference(forward_demodulation,[],[f4070,f6]) ).
fof(f4109,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,meet(complement(X1),join(X1,meet(complement(X1),X0)))),
inference(forward_demodulation,[],[f4092,f4]) ).
fof(f5816,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,complement(one)))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(superposition,[],[f576,f9]) ).
fof(f5817,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),join(X1,complement(one)))
| join(X1,complement(one)) = complement(complement(meet(X0,X1))) ),
inference(superposition,[],[f576,f1289]) ).
fof(f5844,plain,
! [X0,X1] :
( zero != meet(join(X1,complement(one)),complement(meet(X0,X1)))
| join(X1,complement(one)) = complement(complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f5817,f5]) ).
fof(f5845,plain,
! [X0] :
( zero != meet(complement(X0),join(X0,zero))
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f5816,f294]) ).
fof(f5862,plain,
! [X0,X1] :
( zero != meet(join(X1,zero),complement(meet(X0,X1)))
| join(X1,complement(one)) = complement(complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f5844,f294]) ).
fof(f5863,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f5845,f221]) ).
fof(f5874,plain,
! [X0,X1] :
( zero != meet(X1,complement(meet(X0,X1)))
| join(X1,complement(one)) = complement(complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f5862,f221]) ).
fof(f5875,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| join(X0,complement(one)) = complement(complement(X0)) ),
inference(forward_demodulation,[],[f5863,f5]) ).
fof(f5883,plain,
! [X0,X1] :
( join(X1,zero) = complement(complement(meet(X0,X1)))
| zero != meet(X1,complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f5874,f294]) ).
fof(f5884,plain,
! [X0] : join(X0,complement(one)) = complement(complement(X0)),
inference(forward_subsumption_resolution,[],[f5875,f10]) ).
fof(f5890,plain,
! [X0,X1] :
( zero != meet(X1,complement(meet(X0,X1)))
| complement(complement(meet(X0,X1))) = X1 ),
inference(forward_demodulation,[],[f5883,f221]) ).
fof(f5891,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f5884,f294]) ).
fof(f5896,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f5891,f221]) ).
fof(f6150,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,zero),join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f340]) ).
fof(f6163,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f83,f340]) ).
fof(f6167,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(meet(X1,zero),join(meet(X1,X0),X2)),
inference(superposition,[],[f130,f340]) ).
fof(f6175,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),join(meet(X1,zero),complement(meet(X0,X1))))
| complement(meet(X1,X0)) = join(meet(X1,zero),complement(meet(X0,X1))) ),
inference(superposition,[],[f576,f340]) ).
fof(f6186,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(meet(X1,zero),complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(meet(X1,zero),complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f6175,f7]) ).
fof(f6194,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(zero,join(meet(X1,X0),X2)),
inference(forward_demodulation,[],[f6167,f358]) ).
fof(f6210,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(zero,join(meet(X1,X0),X2)),
inference(forward_demodulation,[],[f6150,f358]) ).
fof(f6265,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(zero,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(meet(X1,zero),complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f6186,f358]) ).
fof(f6273,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(meet(X1,X0),X2),
inference(forward_demodulation,[],[f6194,f322]) ).
fof(f6288,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X1,X0),X2),
inference(forward_demodulation,[],[f6210,f322]) ).
fof(f6330,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X0,X1))))
| complement(meet(X1,X0)) = join(meet(X1,zero),complement(meet(X0,X1))) ),
inference(forward_demodulation,[],[f6265,f322]) ).
fof(f6377,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(meet(X1,zero),complement(meet(X0,X1))),
inference(forward_subsumption_resolution,[],[f6330,f673]) ).
fof(f6398,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(zero,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f6377,f358]) ).
fof(f6414,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_demodulation,[],[f6398,f322]) ).
fof(f6684,plain,
! [X2,X3,X0,X1] : join(X3,join(meet(X0,X1),X2)) = join(X2,join(X3,meet(X1,X0))),
inference(superposition,[],[f130,f6288]) ).
fof(f6700,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,join(meet(X0,X1),meet(complement(X2),join(X2,meet(X1,X0))))),
inference(superposition,[],[f1791,f6288]) ).
fof(f6705,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),join(X2,X3)) = join(X2,join(X3,meet(X1,X0))),
inference(superposition,[],[f130,f6288]) ).
fof(f6956,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X1,X0),meet(X3,X2)),
inference(superposition,[],[f6273,f6273]) ).
fof(f7017,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X2,X1)),
inference(superposition,[],[f6,f6273]) ).
fof(f7049,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),meet(X2,X3)) = join(X0,join(X1,meet(X3,X2))),
inference(superposition,[],[f130,f6273]) ).
fof(f7055,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,meet(X2,X3))) = join(X0,join(X1,meet(X3,X2))),
inference(forward_demodulation,[],[f7049,f8]) ).
fof(f7385,plain,
! [X2,X0,X1] : join(zero,meet(X0,meet(X2,X1))) = meet(X0,join(meet(X2,X1),meet(complement(X0),join(X0,meet(X1,X2))))),
inference(superposition,[],[f181,f7017]) ).
fof(f7420,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = join(zero,meet(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f7385,f6700]) ).
fof(f7464,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f7420,f322]) ).
fof(f7578,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f5,f7464]) ).
fof(f7854,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X0,meet(X2,X1))),
inference(superposition,[],[f7017,f7578]) ).
fof(f8499,plain,
! [X2,X3,X0,X1] : join(X2,X3) = join(X2,join(X3,meet(X0,meet(X1,X2)))),
inference(superposition,[],[f191,f107]) ).
fof(f11617,plain,
! [X0,X1] : meet(join(X0,X1),complement(X0)) = meet(join(X0,X1),join(complement(join(X0,X1)),complement(X0))),
inference(superposition,[],[f1415,f3]) ).
fof(f11762,plain,
! [X0,X1] : meet(join(X0,X1),complement(X0)) = meet(join(X0,X1),join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f11617,f6]) ).
fof(f11831,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(join(X0,X1),join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f11762,f5]) ).
fof(f12688,plain,
! [X2,X0,X1] : meet(X2,join(meet(one,X0),meet(one,X1))) = meet(X2,join(meet(X0,join(one,X1)),meet(join(one,X0),X1))),
inference(superposition,[],[f174,f19]) ).
fof(f12848,plain,
! [X2,X0,X1] : meet(X2,join(meet(one,X0),meet(one,X1))) = meet(X2,join(meet(X0,join(one,X1)),meet(one,X1))),
inference(forward_demodulation,[],[f12688,f238]) ).
fof(f12908,plain,
! [X2,X0,X1] : meet(X2,join(meet(one,X0),meet(one,X1))) = meet(X2,join(meet(one,X1),meet(X0,join(one,X1)))),
inference(forward_demodulation,[],[f12848,f6]) ).
fof(f12934,plain,
! [X2,X0,X1] : meet(X2,join(meet(one,X0),meet(one,X1))) = meet(X2,join(meet(one,X1),meet(X0,one))),
inference(forward_demodulation,[],[f12908,f238]) ).
fof(f12950,plain,
! [X2,X0,X1] : meet(X2,join(meet(one,X0),meet(one,X1))) = meet(X2,join(meet(one,X1),X0)),
inference(forward_demodulation,[],[f12934,f169]) ).
fof(f12962,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(meet(one,X0),X1)),
inference(forward_demodulation,[],[f12950,f241]) ).
fof(f12972,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f12962,f241]) ).
fof(f13022,plain,
! [X2,X3,X0,X1] : meet(X3,join(meet(X0,X1),X2)) = meet(X3,join(X2,meet(X1,X0))),
inference(superposition,[],[f12972,f6288]) ).
fof(f13140,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f1,f12972]) ).
fof(f13143,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f12972]) ).
fof(f13145,plain,
! [X2,X0,X1] : join(X2,X1) = join(join(X2,X1),meet(X0,join(X1,X2))),
inference(superposition,[],[f53,f12972]) ).
fof(f13149,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X2,X1),X3)) = meet(X3,meet(X0,join(X1,X2))),
inference(superposition,[],[f107,f12972]) ).
fof(f13157,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = join(meet(X0,zero),meet(X0,join(X1,X2))),
inference(superposition,[],[f340,f12972]) ).
fof(f13167,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),X3) = join(X3,meet(join(X2,X1),X0)),
inference(superposition,[],[f6273,f12972]) ).
fof(f13176,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,join(X1,X2))) = meet(X3,meet(join(X2,X1),X0)),
inference(superposition,[],[f7464,f12972]) ).
fof(f13207,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(join(X2,X1),X0),
inference(forward_demodulation,[],[f13157,f340]) ).
fof(f13210,plain,
! [X2,X0,X1] : join(X2,X1) = join(X2,join(X1,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f13145,f8]) ).
fof(f13932,plain,
! [X0,X1] : zero = meet(join(X0,X1),complement(join(X1,X0))),
inference(superposition,[],[f10,f13207]) ).
fof(f14226,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f6273,f13140]) ).
fof(f14230,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f6414,f13140]) ).
fof(f14233,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f7017,f13140]) ).
fof(f14242,plain,
! [X2,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f14233,f13140]) ).
fof(f14244,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f14230,f13140]) ).
fof(f14248,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f14226,f13140]) ).
fof(f14681,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X0,join(X2,X1))),
inference(superposition,[],[f12972,f14248]) ).
fof(f15244,plain,
! [X2,X3,X0,X1,X4] : join(X4,join(X0,meet(join(X1,X2),X3))) = join(X0,join(X4,meet(X3,join(X2,X1)))),
inference(superposition,[],[f130,f13167]) ).
fof(f15261,plain,
! [X2,X3,X0,X1,X4] : meet(X4,join(X0,meet(join(X1,X2),X3))) = meet(X4,join(X0,meet(X3,join(X2,X1)))),
inference(superposition,[],[f12972,f13167]) ).
fof(f16737,plain,
! [X2,X3,X0,X1] : join(X3,join(X2,join(X0,X1))) = join(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f14242,f8]) ).
fof(f17094,plain,
! [X2,X3,X0,X1,X4] : meet(X4,meet(X0,meet(X1,join(X2,X3)))) = meet(X4,meet(join(X3,X2),meet(X0,X1))),
inference(superposition,[],[f13176,f7]) ).
fof(f32709,plain,
! [X0,X1] : meet(X0,meet(complement(X0),join(X0,X1))) = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(superposition,[],[f96,f11831]) ).
fof(f32838,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f32709,f146]) ).
fof(f32901,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f32838,f10]) ).
fof(f43570,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),complement(join(X0,X1))) ),
inference(superposition,[],[f2182,f32901]) ).
fof(f43663,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(trivial_inequality_removal,[],[f43570]) ).
fof(f44127,plain,
! [X2,X0,X1] : complement(meet(X2,X1)) = join(complement(meet(X2,X1)),complement(join(X0,meet(X1,X2)))),
inference(superposition,[],[f43663,f6273]) ).
fof(f44146,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f43663,f14244]) ).
fof(f44176,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f43,f43663]) ).
fof(f44263,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f44176,f5]) ).
fof(f44390,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f44263,f5896]) ).
fof(f44433,plain,
! [X0,X1] : complement(meet(X0,X1)) = meet(complement(meet(X1,X0)),complement(meet(X0,X1))),
inference(superposition,[],[f44263,f6163]) ).
fof(f44444,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f44263,f14244]) ).
fof(f44452,plain,
! [X2,X0,X1] : join(meet(complement(X0),meet(complement(join(X0,X1)),join(complement(X0),X2))),meet(complement(join(X0,X1)),meet(join(complement(X0),X2),meet(X2,join(complement(X0),complement(join(X0,X1))))))) = meet(complement(join(X0,X1)),meet(join(complement(X0),X2),join(complement(join(X0,X1)),join(meet(complement(X0),X2),meet(X2,meet(join(complement(X0),complement(join(X0,X1))),join(complement(X0),meet(complement(join(X0,X1)),join(complement(X0),X2))))))))),
inference(superposition,[],[f33,f44263]) ).
fof(f44470,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f191,f44263]) ).
fof(f44540,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(complement(X0),X2)) = join(meet(complement(X0),meet(complement(join(X0,X1)),join(complement(X0),X2))),meet(complement(join(X0,X1)),meet(join(complement(X0),X2),meet(X2,join(complement(X0),complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f44452,f146]) ).
fof(f44585,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(complement(X0),X2)) = join(meet(complement(X0),meet(complement(join(X0,X1)),join(complement(X0),X2))),meet(complement(join(X0,X1)),meet(X2,meet(join(complement(X0),complement(join(X0,X1))),join(X2,complement(X0)))))),
inference(forward_demodulation,[],[f44540,f17094]) ).
fof(f44605,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(complement(X0),X2)) = join(meet(complement(X0),meet(complement(join(X0,X1)),join(complement(X0),X2))),meet(complement(join(X0,X1)),meet(join(X2,complement(X0)),X2))),
inference(forward_demodulation,[],[f44585,f967]) ).
fof(f44615,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(complement(X0),X2)) = join(meet(complement(X0),meet(complement(join(X0,X1)),join(complement(X0),X2))),meet(complement(join(X0,X1)),meet(X2,join(X2,complement(X0))))),
inference(forward_demodulation,[],[f44605,f7854]) ).
fof(f44621,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(complement(X0),X2)) = join(meet(complement(X0),meet(complement(join(X0,X1)),join(complement(X0),X2))),meet(complement(join(X0,X1)),X2)),
inference(forward_demodulation,[],[f44615,f3]) ).
fof(f44625,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(complement(X0),X2)) = join(meet(complement(join(X0,X1)),X2),meet(complement(X0),meet(complement(join(X0,X1)),join(complement(X0),X2)))),
inference(forward_demodulation,[],[f44621,f6]) ).
fof(f44629,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(complement(X0),X2)) = join(meet(complement(join(X0,X1)),X2),meet(complement(X0),complement(join(X0,X1)))),
inference(forward_demodulation,[],[f44625,f146]) ).
fof(f44632,plain,
! [X2,X0,X1] : meet(complement(join(X0,X1)),join(complement(X0),X2)) = join(meet(complement(join(X0,X1)),X2),complement(join(X0,X1))),
inference(forward_demodulation,[],[f44629,f44263]) ).
fof(f44634,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),meet(complement(join(X0,X1)),X2)) = meet(complement(join(X0,X1)),join(complement(X0),X2)),
inference(forward_demodulation,[],[f44632,f6]) ).
fof(f44636,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),join(complement(X0),X2)),
inference(forward_demodulation,[],[f44634,f4]) ).
fof(f45014,plain,
! [X2,X0,X1] : join(meet(X0,meet(complement(join(complement(X0),X1)),join(X0,X2))),meet(complement(join(complement(X0),X1)),meet(join(X0,X2),meet(X2,join(X0,complement(join(complement(X0),X1))))))) = meet(complement(join(complement(X0),X1)),meet(join(X0,X2),join(complement(join(complement(X0),X1)),join(meet(X0,X2),meet(X2,meet(join(X0,complement(join(complement(X0),X1))),join(X0,meet(complement(join(complement(X0),X1)),join(X0,X2))))))))),
inference(superposition,[],[f33,f44390]) ).
fof(f45121,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(meet(X0,meet(complement(join(complement(X0),X1)),join(X0,X2))),meet(complement(join(complement(X0),X1)),meet(join(X0,X2),meet(X2,join(X0,complement(join(complement(X0),X1))))))),
inference(forward_demodulation,[],[f45014,f146]) ).
fof(f45172,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(meet(X0,meet(complement(join(complement(X0),X1)),join(X0,X2))),meet(complement(join(complement(X0),X1)),meet(X2,meet(join(X0,complement(join(complement(X0),X1))),join(X2,X0))))),
inference(forward_demodulation,[],[f45121,f17094]) ).
fof(f45193,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(meet(X0,meet(complement(join(complement(X0),X1)),join(X0,X2))),meet(complement(join(complement(X0),X1)),meet(join(X2,X0),X2))),
inference(forward_demodulation,[],[f45172,f967]) ).
fof(f45202,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(meet(X0,meet(complement(join(complement(X0),X1)),join(X0,X2))),meet(complement(join(complement(X0),X1)),meet(X2,join(X2,X0)))),
inference(forward_demodulation,[],[f45193,f7854]) ).
fof(f45207,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(meet(X0,meet(complement(join(complement(X0),X1)),join(X0,X2))),meet(complement(join(complement(X0),X1)),X2)),
inference(forward_demodulation,[],[f45202,f3]) ).
fof(f45211,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(meet(complement(join(complement(X0),X1)),X2),meet(X0,meet(complement(join(complement(X0),X1)),join(X0,X2)))),
inference(forward_demodulation,[],[f45207,f6]) ).
fof(f45214,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(meet(complement(join(complement(X0),X1)),X2),meet(X0,complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f45211,f146]) ).
fof(f45217,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(meet(complement(join(complement(X0),X1)),X2),complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f45214,f44390]) ).
fof(f45220,plain,
! [X2,X0,X1] : meet(complement(join(complement(X0),X1)),join(X0,X2)) = join(complement(join(complement(X0),X1)),meet(complement(join(complement(X0),X1)),X2)),
inference(forward_demodulation,[],[f45217,f6]) ).
fof(f45223,plain,
! [X2,X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),join(X0,X2)),
inference(forward_demodulation,[],[f45220,f4]) ).
fof(f45233,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f44146,f4]) ).
fof(f45234,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f44146,f53]) ).
fof(f45319,plain,
! [X2,X0,X1] : meet(complement(join(X1,X0)),X2) = meet(complement(join(X1,X0)),meet(complement(X0),X2)),
inference(superposition,[],[f97,f44146]) ).
fof(f45399,plain,
! [X2,X0,X1] : meet(complement(join(X1,X0)),X2) = meet(complement(X0),meet(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f45319,f107]) ).
fof(f45452,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f45234,f6]) ).
fof(f45453,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f45233,f6]) ).
fof(f45576,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(superposition,[],[f45453,f5896]) ).
fof(f45929,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,complement(meet(X1,complement(X0)))),
inference(superposition,[],[f45452,f5896]) ).
fof(f46026,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f3,f45452]) ).
fof(f46451,plain,
! [X2,X0,X1] : join(X2,X0) = meet(join(X2,X0),join(X2,complement(meet(complement(X0),X1)))),
inference(superposition,[],[f128,f45576]) ).
fof(f47015,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = X0,
inference(superposition,[],[f46026,f5896]) ).
fof(f48439,plain,
! [X2,X0,X1] : complement(join(complement(complement(X0)),X2)) = meet(complement(join(complement(complement(X0)),X2)),complement(meet(X0,X1))),
inference(superposition,[],[f45223,f45453]) ).
fof(f48631,plain,
! [X2,X0,X1] : complement(join(X0,X2)) = meet(complement(join(X0,X2)),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f48439,f5896]) ).
fof(f50716,plain,
! [X2,X0,X1] : complement(meet(X0,X2)) = join(complement(meet(X0,X2)),complement(join(X0,X1))),
inference(superposition,[],[f53,f48631]) ).
fof(f51064,plain,
! [X2,X3,X0,X1] : complement(meet(X1,X3)) = join(complement(meet(X1,X3)),complement(join(X0,join(X1,X2)))),
inference(superposition,[],[f50716,f130]) ).
fof(f51111,plain,
! [X2,X0,X1] : complement(meet(X1,X2)) = join(complement(meet(X1,X2)),complement(join(X0,X1))),
inference(superposition,[],[f50716,f14244]) ).
fof(f52540,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),join(X2,complement(X0))),
inference(superposition,[],[f12972,f44636]) ).
fof(f52541,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = meet(join(X2,complement(X0)),complement(join(X0,X1))),
inference(superposition,[],[f13143,f44636]) ).
fof(f54105,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,meet(complement(meet(X0,X1)),complement(meet(X1,X0)))),
inference(superposition,[],[f6273,f44433]) ).
fof(f54107,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(meet(complement(meet(X0,X1)),complement(meet(X1,X0))),X2),
inference(superposition,[],[f6288,f44433]) ).
fof(f54112,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = join(X2,meet(complement(meet(X0,X1)),complement(meet(X1,X0)))),
inference(superposition,[],[f7017,f44433]) ).
fof(f54114,plain,
! [X2,X0,X1] : meet(X2,complement(meet(X0,X1))) = meet(X2,meet(complement(meet(X0,X1)),complement(meet(X1,X0)))),
inference(superposition,[],[f7464,f44433]) ).
fof(f54116,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),X2) = meet(X2,meet(complement(meet(X0,X1)),complement(meet(X1,X0)))),
inference(superposition,[],[f7578,f44433]) ).
fof(f54149,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),X2) = meet(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f54116,f44433]) ).
fof(f54151,plain,
! [X2,X0,X1] : meet(X2,complement(meet(X0,X1))) = meet(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f54114,f44433]) ).
fof(f54153,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,X1))) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f54112,f44433]) ).
fof(f54158,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(meet(X0,X1)),X2),
inference(forward_demodulation,[],[f54107,f44433]) ).
fof(f54160,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f54105,f44433]) ).
fof(f54664,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,complement(meet(join(X1,X0),join(X0,X1)))),
inference(superposition,[],[f54151,f13140]) ).
fof(f54990,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f54664,f13140]) ).
fof(f55411,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X1,X0))),
inference(superposition,[],[f45453,f54153]) ).
fof(f57095,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,X1))) = join(complement(meet(join(X1,X0),join(X0,X1))),X2),
inference(superposition,[],[f54160,f13140]) ).
fof(f57133,plain,
! [X2,X0,X1] : complement(meet(X1,X2)) = join(complement(join(X0,X1)),complement(meet(X2,X1))),
inference(superposition,[],[f51111,f54160]) ).
fof(f57458,plain,
! [X2,X0,X1] : join(complement(join(X1,X0)),X2) = join(X2,complement(join(X0,X1))),
inference(forward_demodulation,[],[f57095,f13140]) ).
fof(f62373,plain,
! [X2,X0,X1] : meet(complement(join(X2,X1)),X0) = meet(X0,complement(join(X1,X2))),
inference(superposition,[],[f5,f54990]) ).
fof(f62377,plain,
! [X2,X0,X1] : complement(join(X2,X1)) = join(complement(join(X2,X1)),meet(X0,complement(join(X1,X2)))),
inference(superposition,[],[f53,f54990]) ).
fof(f62480,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f44444,f54990]) ).
fof(f63318,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f62480,f5896]) ).
fof(f65294,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),complement(meet(complement(X0),complement(X1)))),
inference(superposition,[],[f46451,f45929]) ).
fof(f65327,plain,
! [X2,X0,X1] : meet(X1,join(X0,X1)) = meet(X1,join(X0,complement(meet(complement(X1),X2)))),
inference(superposition,[],[f97,f46451]) ).
fof(f65511,plain,
! [X2,X0,X1] : meet(X1,join(X0,complement(meet(complement(X1),X2)))) = X1,
inference(forward_demodulation,[],[f65327,f43]) ).
fof(f66013,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(meet(complement(X1),complement(X0)),complement(join(X0,X1))),
inference(superposition,[],[f47015,f65294]) ).
fof(f66149,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(join(X1,X0)),meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f66013,f62373]) ).
fof(f66260,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(X0),meet(complement(join(X1,X0)),complement(X1))),
inference(forward_demodulation,[],[f66149,f107]) ).
fof(f66333,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(X0),meet(complement(X1),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f66260,f7464]) ).
fof(f66384,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(join(X1,X0)),complement(X1)),
inference(forward_demodulation,[],[f66333,f45399]) ).
fof(f66423,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(X1),complement(join(X1,X0))),
inference(forward_demodulation,[],[f66384,f5]) ).
fof(f66458,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f66423,f44263]) ).
fof(f66558,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(superposition,[],[f66458,f5896]) ).
fof(f66564,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(X1,complement(X0))),
inference(superposition,[],[f66458,f5896]) ).
fof(f66630,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f5,f66458]) ).
fof(f66644,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(complement(X0),meet(complement(X1),X2)),
inference(superposition,[],[f107,f66458]) ).
fof(f66645,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(complement(X1),meet(X2,complement(X0))),
inference(superposition,[],[f107,f66458]) ).
fof(f67096,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(superposition,[],[f5896,f66564]) ).
fof(f67128,plain,
! [X2,X0,X1] : complement(join(join(X0,complement(X1)),X2)) = meet(meet(complement(X0),X1),complement(X2)),
inference(superposition,[],[f66458,f66564]) ).
fof(f67129,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,complement(X2))) = complement(join(join(X0,complement(X1)),X2)),
inference(forward_demodulation,[],[f67128,f7]) ).
fof(f67234,plain,
! [X2,X0,X1] : complement(join(X0,join(complement(X1),X2))) = meet(complement(X0),meet(X1,complement(X2))),
inference(forward_demodulation,[],[f67129,f8]) ).
fof(f67290,plain,
! [X2,X0,X1] : meet(X1,complement(join(X2,X0))) = complement(join(X0,join(complement(X1),X2))),
inference(forward_demodulation,[],[f67234,f66645]) ).
fof(f67406,plain,
! [X0,X1] : meet(complement(X0),join(X1,meet(X0,complement(X1)))) = meet(complement(X0),join(X0,join(X1,meet(X0,complement(X1))))),
inference(superposition,[],[f3624,f66558]) ).
fof(f67470,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f5896,f66558]) ).
fof(f67503,plain,
! [X2,X0,X1] : complement(join(X2,meet(X0,complement(X1)))) = meet(complement(X2),join(complement(X0),X1)),
inference(superposition,[],[f66564,f66558]) ).
fof(f67570,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X1,meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f67406,f191]) ).
fof(f67766,plain,
! [X2,X0,X1] : complement(meet(X2,join(complement(X0),X1))) = join(complement(X2),meet(X0,complement(X1))),
inference(superposition,[],[f67470,f67470]) ).
fof(f67771,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X1),complement(X0)),
inference(superposition,[],[f67470,f5896]) ).
fof(f68152,plain,
! [X2,X0,X1] : complement(meet(X2,join(X0,complement(X1)))) = join(complement(X2),meet(complement(X0),X1)),
inference(superposition,[],[f67771,f66564]) ).
fof(f68249,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(superposition,[],[f6,f67771]) ).
fof(f68808,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(X1),join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f3376,f68249]) ).
fof(f68809,plain,
! [X0,X1] : meet(complement(X1),join(complement(X0),complement(complement(meet(X0,X1))))) = meet(complement(X1),join(X1,join(complement(X0),complement(complement(meet(X0,X1)))))),
inference(superposition,[],[f3624,f68249]) ).
fof(f69085,plain,
! [X0,X1] : meet(complement(X1),complement(meet(X0,complement(meet(X0,X1))))) = meet(complement(X1),join(X1,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f68809,f67771]) ).
fof(f69086,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f68808,f66458]) ).
fof(f69232,plain,
! [X0,X1] : meet(complement(X1),join(complement(X0),meet(X0,X1))) = meet(complement(X1),join(X1,join(complement(X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f69085,f67470]) ).
fof(f69312,plain,
! [X0,X1] : meet(complement(X1),join(X1,complement(X0))) = meet(complement(X1),join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f69232,f1235]) ).
fof(f81441,plain,
! [X2,X0,X1] : meet(join(X2,complement(X0)),complement(join(X0,X1))) = join(meet(complement(join(X0,X1)),zero),complement(join(X0,X1))),
inference(superposition,[],[f340,f52540]) ).
fof(f81558,plain,
! [X2,X0,X1] : meet(join(X2,complement(X0)),complement(join(X0,X1))) = join(complement(join(X1,X0)),meet(complement(join(X0,X1)),zero)),
inference(forward_demodulation,[],[f81441,f57458]) ).
fof(f81699,plain,
! [X2,X0,X1] : meet(join(X2,complement(X0)),complement(join(X0,X1))) = join(complement(join(X1,X0)),meet(zero,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f81558,f7017]) ).
fof(f81796,plain,
! [X2,X0,X1] : complement(join(X1,X0)) = meet(join(X2,complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f81699,f62377]) ).
fof(f89818,plain,
! [X2,X0,X1] : zero = meet(join(X0,meet(X2,X1)),complement(join(X0,meet(X1,X2)))),
inference(superposition,[],[f13932,f6273]) ).
fof(f105243,plain,
! [X2,X0,X1] : join(X2,complement(meet(complement(X0),join(X0,complement(X1))))) = join(complement(meet(join(complement(X1),meet(X1,X0)),complement(X0))),X2),
inference(superposition,[],[f54160,f69312]) ).
fof(f105264,plain,
! [X2,X0,X1] : join(X2,complement(meet(complement(X0),join(X0,complement(X1))))) = join(complement(meet(complement(X0),join(complement(X1),meet(X1,X0)))),X2),
inference(forward_demodulation,[],[f105243,f54158]) ).
fof(f105473,plain,
! [X2,X0,X1] : join(X2,complement(meet(complement(X0),join(X0,complement(X1))))) = join(join(complement(complement(X0)),meet(X1,complement(meet(X1,X0)))),X2),
inference(forward_demodulation,[],[f105264,f67766]) ).
fof(f105640,plain,
! [X2,X0,X1] : join(X2,complement(meet(complement(X0),join(X0,complement(X1))))) = join(complement(complement(X0)),join(meet(X1,complement(meet(X1,X0))),X2)),
inference(forward_demodulation,[],[f105473,f8]) ).
fof(f105774,plain,
! [X2,X0,X1] : join(X2,complement(meet(complement(X0),join(X0,complement(X1))))) = join(X0,join(meet(X1,complement(meet(X1,X0))),X2)),
inference(forward_demodulation,[],[f105640,f5896]) ).
fof(f105896,plain,
! [X2,X0,X1] : join(X2,join(complement(complement(X0)),meet(complement(X0),X1))) = join(X0,join(meet(X1,complement(meet(X1,X0))),X2)),
inference(forward_demodulation,[],[f105774,f68152]) ).
fof(f106005,plain,
! [X2,X0,X1] : join(X2,join(X0,meet(complement(X0),X1))) = join(X0,join(meet(X1,complement(meet(X1,X0))),X2)),
inference(forward_demodulation,[],[f105896,f5896]) ).
fof(f111443,plain,
! [X0,X1] : join(meet(X0,complement(X1)),X1) = join(meet(X0,complement(X1)),join(X1,meet(complement(X0),join(X0,X1)))),
inference(superposition,[],[f13210,f67570]) ).
fof(f111622,plain,
! [X0,X1] : join(meet(X0,complement(X1)),X1) = join(X1,join(meet(X0,complement(X1)),meet(join(X1,X0),complement(X0)))),
inference(forward_demodulation,[],[f111443,f15244]) ).
fof(f111772,plain,
! [X0,X1] : join(meet(X0,complement(X1)),X1) = join(X1,join(meet(X0,complement(X1)),meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f111622,f7055]) ).
fof(f111879,plain,
! [X0,X1] : join(X1,meet(X0,complement(X1))) = join(X1,join(meet(X0,complement(X1)),meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f111772,f6]) ).
fof(f118707,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(X0,complement(join(complement(X1),meet(X0,complement(meet(X1,X0)))))),
inference(superposition,[],[f67096,f69086]) ).
fof(f118948,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(X0,meet(complement(complement(X1)),join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f118707,f67503]) ).
fof(f119234,plain,
! [X0,X1] : complement(complement(join(X0,X1))) = join(X0,meet(X1,join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f118948,f5896]) ).
fof(f119459,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f119234,f5896]) ).
fof(f209492,plain,
! [X0,X1] :
( zero != meet(meet(complement(X0),join(X0,meet(complement(X0),X1))),complement(meet(complement(X0),X1)))
| meet(complement(X0),join(X0,meet(complement(X0),X1))) = complement(complement(meet(complement(X0),X1))) ),
inference(superposition,[],[f5890,f4109]) ).
fof(f209712,plain,
! [X0,X1] :
( zero != meet(complement(meet(X1,complement(X0))),meet(complement(X0),join(X0,meet(complement(X0),X1))))
| meet(complement(X0),join(X0,meet(complement(X0),X1))) = complement(complement(meet(complement(X0),X1))) ),
inference(forward_demodulation,[],[f209492,f54149]) ).
fof(f209983,plain,
! [X0,X1] :
( zero != meet(complement(X0),meet(join(meet(complement(X0),X1),X0),complement(meet(X1,complement(X0)))))
| meet(complement(X0),join(X0,meet(complement(X0),X1))) = complement(complement(meet(complement(X0),X1))) ),
inference(forward_demodulation,[],[f209712,f13149]) ).
fof(f210198,plain,
! [X0,X1] :
( zero != meet(complement(X0),meet(complement(meet(X1,complement(X0))),join(X0,meet(complement(X0),X1))))
| meet(complement(X0),join(X0,meet(complement(X0),X1))) = complement(complement(meet(complement(X0),X1))) ),
inference(forward_demodulation,[],[f209983,f13176]) ).
fof(f210372,plain,
! [X0,X1] :
( zero != meet(join(X0,meet(complement(X0),X1)),complement(join(X0,meet(X1,complement(X0)))))
| meet(complement(X0),join(X0,meet(complement(X0),X1))) = complement(complement(meet(complement(X0),X1))) ),
inference(forward_demodulation,[],[f210198,f66644]) ).
fof(f210501,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = complement(complement(meet(complement(X0),X1))),
inference(forward_subsumption_resolution,[],[f210372,f89818]) ).
fof(f210611,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f210501,f5896]) ).
fof(f210860,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f210611,f5896]) ).
fof(f212287,plain,
! [X0,X1] : join(complement(join(complement(X0),meet(X0,X1))),complement(meet(X0,X1))) = complement(meet(join(complement(X0),meet(X0,X1)),X0)),
inference(superposition,[],[f55411,f210860]) ).
fof(f212390,plain,
! [X0,X1] : complement(meet(X0,join(complement(X0),meet(X0,X1)))) = join(complement(join(complement(X0),meet(X0,X1))),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f212287,f6414]) ).
fof(f212597,plain,
! [X0,X1] : complement(meet(X0,join(complement(X0),meet(X0,X1)))) = join(complement(meet(X1,X0)),complement(join(complement(X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f212390,f54160]) ).
fof(f212766,plain,
! [X0,X1] : complement(meet(X1,X0)) = complement(meet(X0,join(complement(X0),meet(X0,X1)))),
inference(forward_demodulation,[],[f212597,f44127]) ).
fof(f212878,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f212766,f67766]) ).
fof(f213301,plain,
! [X0,X1] : complement(meet(join(complement(X1),meet(X0,complement(meet(X1,X0)))),complement(X0))) = join(complement(complement(X0)),meet(complement(X0),complement(complement(join(X0,X1))))),
inference(superposition,[],[f212878,f69086]) ).
fof(f213746,plain,
! [X0,X1] : complement(meet(join(complement(X1),meet(X0,complement(meet(X1,X0)))),complement(X0))) = join(complement(complement(X0)),complement(join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f213301,f66458]) ).
fof(f214071,plain,
! [X0,X1] : complement(meet(join(complement(X1),meet(X0,complement(meet(X1,X0)))),complement(X0))) = complement(meet(complement(X0),join(X0,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f213746,f67771]) ).
fof(f214352,plain,
! [X0,X1] : join(complement(complement(X0)),meet(complement(X0),join(X0,X1))) = complement(meet(join(complement(X1),meet(X0,complement(meet(X1,X0)))),complement(X0))),
inference(forward_demodulation,[],[f214071,f68152]) ).
fof(f214563,plain,
! [X0,X1] : join(complement(complement(X0)),meet(complement(X0),join(X0,X1))) = complement(meet(complement(X0),join(complement(X1),meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f214352,f6414]) ).
fof(f214739,plain,
! [X0,X1] : join(complement(complement(X0)),meet(complement(X0),join(X0,X1))) = join(complement(complement(X0)),meet(X1,complement(meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f214563,f67766]) ).
fof(f214861,plain,
! [X0,X1] : join(complement(complement(X0)),meet(complement(X0),join(X0,X1))) = join(complement(complement(X0)),meet(X1,join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f214739,f67470]) ).
fof(f214955,plain,
! [X0,X1] : join(X0,meet(complement(X0),join(X0,X1))) = join(X0,meet(X1,join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f214861,f5896]) ).
fof(f215019,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f214955,f119459]) ).
fof(f215324,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),join(X1,X0))),
inference(superposition,[],[f215019,f12972]) ).
fof(f216337,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(X0,X1),meet(complement(meet(X0,X1)),X0)),
inference(superposition,[],[f215324,f4]) ).
fof(f216921,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f216337,f7017]) ).
fof(f217133,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f216921,f6]) ).
fof(f217291,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f217133,f4]) ).
fof(f217792,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f122,f217291]) ).
fof(f218777,plain,
! [X0,X1] : join(join(X1,meet(complement(X0),join(X0,X1))),X0) = join(join(X1,meet(complement(X0),join(X0,X1))),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f217792,f1791]) ).
fof(f219088,plain,
! [X2,X0,X1] : meet(join(X2,complement(X0)),complement(join(X0,X1))) = complement(join(meet(X1,complement(meet(X1,X0))),X0)),
inference(superposition,[],[f81796,f217792]) ).
fof(f219136,plain,
! [X0,X1] : meet(X0,complement(join(complement(X0),X1))) = complement(join(meet(X1,complement(meet(X1,complement(X0)))),complement(X0))),
inference(superposition,[],[f63318,f217792]) ).
fof(f219163,plain,
! [X0,X1] : meet(X0,complement(join(complement(X0),X1))) = complement(join(complement(X0),meet(X1,complement(meet(X1,complement(X0)))))),
inference(forward_demodulation,[],[f219136,f14244]) ).
fof(f219196,plain,
! [X2,X0,X1] : meet(join(X2,complement(X0)),complement(join(X0,X1))) = complement(join(X0,meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f219088,f14244]) ).
fof(f219444,plain,
! [X0,X1] : join(join(X1,meet(complement(X0),join(X0,X1))),X0) = join(meet(X0,complement(meet(X0,X1))),join(X1,meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f218777,f6]) ).
fof(f219475,plain,
! [X0,X1] : meet(X0,complement(join(complement(X0),X1))) = meet(complement(complement(X0)),join(complement(X1),meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f219163,f67503]) ).
fof(f219497,plain,
! [X2,X0,X1] : meet(join(X2,complement(X0)),complement(join(X0,X1))) = meet(complement(X0),join(complement(X1),meet(X1,X0))),
inference(forward_demodulation,[],[f219196,f67503]) ).
fof(f219705,plain,
! [X0,X1] : join(join(X1,meet(complement(X0),join(X0,X1))),X0) = join(X1,join(meet(X0,complement(meet(X0,X1))),meet(join(X1,X0),complement(X0)))),
inference(forward_demodulation,[],[f219444,f15244]) ).
fof(f219725,plain,
! [X0,X1] : meet(X0,complement(join(complement(X0),X1))) = meet(complement(complement(X0)),join(complement(X0),complement(X1))),
inference(forward_demodulation,[],[f219475,f69312]) ).
fof(f219744,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,complement(X1))) = meet(join(X2,complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f219497,f69312]) ).
fof(f219904,plain,
! [X0,X1] : join(join(X1,meet(complement(X0),join(X0,X1))),X0) = join(meet(join(X1,X0),complement(X0)),join(X1,meet(complement(X1),X0))),
inference(forward_demodulation,[],[f219705,f106005]) ).
fof(f219913,plain,
! [X0,X1] : meet(X0,complement(join(complement(X0),X1))) = meet(complement(complement(X0)),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f219725,f67771]) ).
fof(f219932,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),join(X0,complement(X1))),
inference(forward_demodulation,[],[f219744,f52541]) ).
fof(f220055,plain,
! [X0,X1] : join(join(X1,meet(complement(X0),join(X0,X1))),X0) = join(meet(X0,complement(X1)),join(meet(join(X1,X0),complement(X0)),X1)),
inference(forward_demodulation,[],[f219904,f6705]) ).
fof(f220059,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f219913,f66458]) ).
fof(f220153,plain,
! [X0,X1] : join(X1,join(meet(X0,complement(X1)),meet(complement(X0),join(X1,X0)))) = join(join(X1,meet(complement(X0),join(X0,X1))),X0),
inference(forward_demodulation,[],[f220055,f6684]) ).
fof(f220155,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = complement(join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f220059,f44390]) ).
fof(f220219,plain,
! [X0,X1] : join(X0,join(X1,meet(complement(X0),join(X0,X1)))) = join(X1,join(meet(X0,complement(X1)),meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f220153,f6]) ).
fof(f220221,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = complement(join(complement(X0),X1)),
inference(forward_demodulation,[],[f220155,f66558]) ).
fof(f220263,plain,
! [X0,X1] : join(X0,join(X1,meet(complement(X0),join(X0,X1)))) = join(X1,meet(X0,complement(X1))),
inference(forward_demodulation,[],[f220219,f111879]) ).
fof(f220265,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,complement(X1)),
inference(forward_demodulation,[],[f220221,f66558]) ).
fof(f220304,plain,
! [X0,X1] : join(X0,X1) = join(X1,meet(X0,complement(X1))),
inference(forward_demodulation,[],[f220263,f135]) ).
fof(f220436,plain,
! [X2,X0,X1] : meet(X2,complement(meet(X0,meet(X1,X2)))) = meet(X2,complement(meet(X0,X1))),
inference(superposition,[],[f220265,f107]) ).
fof(f220556,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = meet(complement(X0),complement(join(complement(X1),meet(X0,complement(meet(X1,X0)))))),
inference(superposition,[],[f220265,f69086]) ).
fof(f220566,plain,
! [X0,X1] : meet(complement(X1),complement(complement(join(X0,X1)))) = meet(complement(X1),complement(complement(X0))),
inference(superposition,[],[f220265,f66630]) ).
fof(f220567,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = meet(complement(X0),complement(complement(X1))),
inference(superposition,[],[f220265,f66458]) ).
fof(f220586,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,complement(complement(X1))),
inference(superposition,[],[f220265,f67470]) ).
fof(f220635,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f67470,f220265]) ).
fof(f220747,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,complement(X1)))) = join(complement(meet(complement(meet(X0,X1)),X0)),X2),
inference(superposition,[],[f54160,f220265]) ).
fof(f220756,plain,
! [X2,X0,X1] : complement(meet(complement(meet(X0,X1)),X0)) = join(complement(join(X2,complement(meet(X0,X1)))),complement(meet(X0,complement(X1)))),
inference(superposition,[],[f57133,f220265]) ).
fof(f220804,plain,
! [X0,X1] : join(meet(complement(meet(complement(X0),X1)),X0),meet(complement(meet(complement(X0),X1)),complement(X0))) = meet(complement(meet(complement(X0),X1)),join(meet(complement(X0),complement(X1)),meet(X0,join(complement(X0),complement(meet(complement(X0),X1)))))),
inference(superposition,[],[f3651,f220265]) ).
fof(f220811,plain,
! [X0,X1] : join(X0,complement(complement(meet(complement(X0),X1)))) = complement(meet(complement(X0),complement(X1))),
inference(superposition,[],[f67096,f220265]) ).
fof(f220834,plain,
! [X0,X1] : join(complement(complement(X0)),X1) = join(X0,complement(complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f220811,f67470]) ).
fof(f220837,plain,
! [X0,X1] : join(meet(complement(meet(complement(X0),X1)),X0),meet(complement(meet(complement(X0),X1)),complement(X0))) = meet(complement(meet(complement(X0),X1)),join(meet(complement(X0),complement(X1)),X0)),
inference(forward_demodulation,[],[f220804,f65511]) ).
fof(f220873,plain,
! [X2,X0,X1] : complement(meet(complement(meet(X0,X1)),X0)) = join(complement(meet(complement(X1),X0)),complement(join(X2,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f220756,f54160]) ).
fof(f220882,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,complement(X1)))) = join(complement(meet(X0,complement(meet(X0,X1)))),X2),
inference(forward_demodulation,[],[f220747,f54158]) ).
fof(f220961,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f220635,f67470]) ).
fof(f220989,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f220586,f5896]) ).
fof(f221006,plain,
! [X0,X1] : complement(join(X0,complement(X1))) = meet(complement(X0),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f220567,f66458]) ).
fof(f221007,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(complement(X1),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f220566,f66458]) ).
fof(f221017,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = complement(join(X0,join(complement(X1),meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f220556,f66458]) ).
fof(f221119,plain,
! [X0,X1] : join(X0,meet(complement(X0),X1)) = join(complement(complement(X0)),X1),
inference(forward_demodulation,[],[f220834,f5896]) ).
fof(f221122,plain,
! [X0,X1] : join(meet(complement(meet(complement(X0),X1)),X0),meet(complement(meet(complement(X0),X1)),complement(X0))) = meet(complement(meet(complement(X0),X1)),join(X0,meet(complement(X1),complement(X0)))),
inference(forward_demodulation,[],[f220837,f13022]) ).
fof(f221153,plain,
! [X2,X0,X1] : complement(meet(complement(meet(X0,X1)),X0)) = complement(meet(meet(complement(X1),X0),join(X2,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f220873,f67771]) ).
fof(f221162,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,complement(X1)))) = join(join(complement(X0),meet(X0,X1)),X2),
inference(forward_demodulation,[],[f220882,f67470]) ).
fof(f221256,plain,
! [X0,X1] : complement(join(X0,complement(join(X0,X1)))) = complement(join(X0,complement(X1))),
inference(forward_demodulation,[],[f221006,f66458]) ).
fof(f221257,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = complement(join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f221007,f66458]) ).
fof(f221267,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = meet(X1,complement(join(meet(X0,complement(meet(X1,X0))),X0))),
inference(forward_demodulation,[],[f221017,f67290]) ).
fof(f221345,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f221119,f5896]) ).
fof(f221348,plain,
! [X0,X1] : join(meet(complement(meet(complement(X0),X1)),X0),meet(complement(meet(complement(X0),X1)),complement(X0))) = meet(complement(meet(complement(X0),X1)),join(complement(X1),X0)),
inference(forward_demodulation,[],[f221122,f220304]) ).
fof(f221375,plain,
! [X2,X0,X1] : complement(meet(complement(meet(X0,X1)),X0)) = join(complement(meet(complement(X1),X0)),meet(complement(X2),meet(X0,X1))),
inference(forward_demodulation,[],[f221153,f68152]) ).
fof(f221384,plain,
! [X2,X0,X1] : join(X2,complement(meet(X0,complement(X1)))) = join(complement(X0),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f221162,f8]) ).
fof(f221458,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f221256,f66564]) ).
fof(f221459,plain,
! [X0,X1] : meet(complement(X1),join(X0,X1)) = complement(join(X1,complement(X0))),
inference(forward_demodulation,[],[f221257,f66564]) ).
fof(f221469,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = meet(X1,complement(join(X0,meet(X0,complement(meet(X1,X0)))))),
inference(forward_demodulation,[],[f221267,f54990]) ).
fof(f221532,plain,
! [X0,X1] : join(meet(complement(meet(complement(X0),X1)),X0),meet(complement(meet(complement(X0),X1)),complement(X0))) = meet(join(X0,complement(X1)),complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f221348,f13143]) ).
fof(f221554,plain,
! [X2,X0,X1] : complement(meet(complement(meet(X0,X1)),X0)) = join(join(X1,complement(X0)),meet(complement(X2),meet(X0,X1))),
inference(forward_demodulation,[],[f221375,f67096]) ).
fof(f221563,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),X1)) = join(complement(X0),join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f221384,f67470]) ).
fof(f221616,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f221458,f66564]) ).
fof(f221617,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X0,X1)),
inference(forward_demodulation,[],[f221459,f66564]) ).
fof(f221627,plain,
! [X0,X1] : meet(complement(X0),complement(complement(join(X0,X1)))) = meet(X1,meet(complement(X0),join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f221469,f67503]) ).
fof(f221666,plain,
! [X0,X1] : meet(join(X0,complement(X1)),join(X0,complement(X1))) = join(meet(join(X0,complement(X1)),X0),meet(join(X0,complement(X1)),complement(X0))),
inference(forward_demodulation,[],[f221532,f67096]) ).
fof(f221682,plain,
! [X2,X0,X1] : complement(meet(complement(meet(X0,X1)),X0)) = join(X1,join(complement(X0),meet(complement(X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f221554,f8]) ).
fof(f221722,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),complement(complement(join(X0,X1)))),
inference(forward_demodulation,[],[f221627,f3]) ).
fof(f221746,plain,
! [X0,X1] : meet(join(X0,complement(X1)),join(X0,complement(X1))) = join(meet(join(X0,complement(X1)),X0),meet(complement(X0),join(X0,complement(X1)))),
inference(forward_demodulation,[],[f221666,f7017]) ).
fof(f221758,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(complement(meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f221682,f8499]) ).
fof(f221786,plain,
! [X0,X1] : meet(X1,complement(X0)) = complement(join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f221722,f66458]) ).
fof(f221800,plain,
! [X0,X1] : meet(join(X0,complement(X1)),join(X0,complement(X1))) = join(meet(X0,join(X0,complement(X1))),meet(join(X0,complement(X1)),complement(X0))),
inference(forward_demodulation,[],[f221746,f6956]) ).
fof(f221807,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f221758,f6414]) ).
fof(f221827,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(X1,complement(X0)),
inference(forward_demodulation,[],[f221786,f66564]) ).
fof(f221839,plain,
! [X0,X1] : meet(join(X0,complement(X1)),join(X0,complement(X1))) = join(meet(X0,join(X0,complement(X1))),meet(complement(X0),join(X0,complement(X1)))),
inference(forward_demodulation,[],[f221800,f7017]) ).
fof(f221842,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(X1,complement(X0)),
inference(forward_demodulation,[],[f221807,f67470]) ).
fof(f221859,plain,
! [X0,X1] : meet(join(X0,complement(X1)),join(X0,complement(X1))) = join(meet(X0,join(X0,complement(X1))),complement(join(X0,X1))),
inference(forward_demodulation,[],[f221839,f219932]) ).
fof(f221874,plain,
! [X0,X1] : meet(join(X0,complement(X1)),join(X0,complement(X1))) = join(complement(join(X1,X0)),meet(X0,join(X0,complement(X1)))),
inference(forward_demodulation,[],[f221859,f57458]) ).
fof(f221885,plain,
! [X0,X1] : join(complement(join(X1,X0)),X0) = meet(join(X0,complement(X1)),join(X0,complement(X1))),
inference(forward_demodulation,[],[f221874,f3]) ).
fof(f221895,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(join(X1,X0)),X0),
inference(forward_demodulation,[],[f221885,f1]) ).
fof(f221901,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(X0,complement(X1)),
inference(forward_demodulation,[],[f221895,f6]) ).
fof(f221918,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(complement(X0),X1)),
inference(superposition,[],[f221827,f5896]) ).
fof(f221948,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(join(X1,meet(X0,X2)),complement(X0)),
inference(superposition,[],[f221827,f191]) ).
fof(f221955,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(join(meet(X0,X2),X1),complement(X0)),
inference(superposition,[],[f221827,f121]) ).
fof(f222007,plain,
! [X0,X1] : meet(complement(complement(X1)),complement(meet(X0,X1))) = meet(complement(X0),complement(complement(X1))),
inference(superposition,[],[f221827,f68249]) ).
fof(f222009,plain,
! [X2,X0,X1] : meet(complement(complement(X0)),join(complement(X0),X1)) = meet(join(X1,complement(join(X0,X2))),complement(complement(X0))),
inference(superposition,[],[f221827,f44470]) ).
fof(f222520,plain,
! [X2,X0,X1] : meet(complement(complement(X0)),join(complement(X0),X1)) = meet(complement(complement(X0)),join(X1,complement(join(X0,X2)))),
inference(forward_demodulation,[],[f222009,f5]) ).
fof(f222522,plain,
! [X0,X1] : complement(join(X0,complement(X1))) = meet(complement(complement(X1)),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f222007,f66458]) ).
fof(f222556,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f221955,f5]) ).
fof(f222563,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f221948,f5]) ).
fof(f222771,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),X1)) = meet(X0,join(X1,complement(join(X0,X2)))),
inference(forward_demodulation,[],[f222520,f5896]) ).
fof(f222773,plain,
! [X0,X1] : complement(join(X0,complement(X1))) = complement(join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[],[f222522,f66458]) ).
fof(f222804,plain,
! [X2,X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f222556,f221616]) ).
fof(f222811,plain,
! [X2,X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f222563,f221616]) ).
fof(f222978,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X2)))),
inference(forward_demodulation,[],[f222771,f220989]) ).
fof(f222980,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = complement(join(X0,complement(X1))),
inference(forward_demodulation,[],[f222773,f66558]) ).
fof(f223144,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f222980,f66564]) ).
fof(f223603,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f221918,f130]) ).
fof(f223878,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,X2))) = meet(X2,join(complement(join(X1,X2)),X0)),
inference(superposition,[],[f97,f221918]) ).
fof(f223957,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,join(complement(join(X1,X2)),X0)),
inference(forward_demodulation,[],[f223878,f963]) ).
fof(f225176,plain,
! [X2,X0,X1] : complement(meet(join(X1,X0),complement(X0))) = join(complement(join(X2,join(X1,X0))),complement(meet(complement(X0),X1))),
inference(superposition,[],[f57133,f221617]) ).
fof(f225223,plain,
! [X2,X0,X1] : complement(meet(join(X1,X0),complement(X0))) = join(complement(meet(X1,complement(X0))),complement(join(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f225176,f54160]) ).
fof(f225446,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = complement(meet(join(X1,X0),complement(X0))),
inference(forward_demodulation,[],[f225223,f51064]) ).
fof(f225611,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = complement(meet(complement(X0),join(X1,X0))),
inference(forward_demodulation,[],[f225446,f6414]) ).
fof(f225741,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = complement(meet(X1,complement(X0))),
inference(forward_demodulation,[],[f225611,f67096]) ).
fof(f225834,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(complement(X1),X0),
inference(forward_demodulation,[],[f225741,f67470]) ).
fof(f227594,plain,
! [X2,X0,X1] : join(X2,complement(join(X0,join(X1,X2)))) = join(X2,complement(join(X0,X1))),
inference(superposition,[],[f221901,f8]) ).
fof(f232049,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X0,X1),meet(X0,X2))) = join(complement(X0),join(meet(X1,join(X2,X0)),meet(X2,join(X0,X1)))),
inference(superposition,[],[f220961,f41]) ).
fof(f232319,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),X1)) = join(join(meet(X0,X1),complement(X0)),X2),
inference(superposition,[],[f14248,f220961]) ).
fof(f232426,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),X1)) = join(meet(X0,X1),join(complement(X0),X2)),
inference(forward_demodulation,[],[f232319,f8]) ).
fof(f232622,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,join(X2,X0)),meet(X2,join(X0,X1)))) = join(meet(X0,X2),join(complement(X0),X1)),
inference(forward_demodulation,[],[f232049,f221563]) ).
fof(f232708,plain,
! [X2,X0,X1] : join(X2,join(complement(X0),X1)) = join(complement(X0),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f232426,f130]) ).
fof(f232863,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X1,join(X2,X0)),meet(X2,join(X0,X1)))) = join(complement(X0),join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f232622,f130]) ).
fof(f233034,plain,
! [X2,X0,X1] : join(X1,join(complement(X0),X2)) = join(complement(X0),join(meet(X1,join(X2,X0)),meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f232863,f232708]) ).
fof(f233597,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,meet(complement(X1),X2))),
inference(superposition,[],[f221345,f107]) ).
fof(f236697,plain,
! [X2,X0,X1] : join(X1,join(X2,complement(join(X0,join(X1,X2))))) = join(complement(X0),join(X1,X2)),
inference(superposition,[],[f8,f225834]) ).
fof(f236759,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,X2)) = join(X1,join(X2,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f236697,f227594]) ).
fof(f240616,plain,
! [X2,X0,X1] : meet(X1,meet(X2,complement(meet(X0,meet(X1,X2))))) = meet(complement(X0),meet(X1,X2)),
inference(superposition,[],[f7,f223144]) ).
fof(f240687,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,X2)) = meet(X1,meet(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f240616,f220436]) ).
fof(f241893,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X0,X1),meet(X0,X2))) = join(join(meet(X1,join(X2,X0)),meet(X2,join(X0,X1))),complement(X0)),
inference(superposition,[],[f221842,f41]) ).
fof(f242497,plain,
! [X2,X0,X1] : join(complement(X0),join(meet(X0,X1),meet(X0,X2))) = join(complement(X0),join(meet(X1,join(X2,X0)),meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f241893,f6]) ).
fof(f242771,plain,
! [X2,X0,X1] : join(X1,join(complement(X0),X2)) = join(complement(X0),join(meet(X0,X1),meet(X0,X2))),
inference(forward_demodulation,[],[f242497,f233034]) ).
fof(f242984,plain,
! [X2,X0,X1] : join(X1,join(complement(X0),X2)) = join(meet(X0,X1),join(complement(X0),X2)),
inference(forward_demodulation,[],[f242771,f232708]) ).
fof(f243144,plain,
! [X2,X0,X1] : join(X1,join(complement(X0),X2)) = join(complement(X0),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f242984,f130]) ).
fof(f286063,plain,
! [X2,X3,X0,X1] : meet(X1,X3) = meet(X1,join(X3,complement(join(X0,join(X1,X2))))),
inference(superposition,[],[f222978,f130]) ).
fof(f290695,plain,
! [X2,X3,X0,X1] : join(complement(join(X0,X1)),join(X2,X3)) = join(X2,join(X3,complement(join(X0,join(X1,X2))))),
inference(superposition,[],[f236759,f8]) ).
fof(f326765,plain,
! [X2,X0,X1] : join(X1,meet(X2,complement(meet(X0,complement(X1))))) = join(X1,meet(complement(X0),meet(complement(X1),X2))),
inference(superposition,[],[f221345,f240687]) ).
fof(f326779,plain,
! [X2,X0,X1] : join(X1,meet(X2,complement(X0))) = join(X1,meet(X2,complement(meet(X0,complement(X1))))),
inference(forward_demodulation,[],[f326765,f233597]) ).
fof(f327171,plain,
! [X2,X0,X1] : join(X1,meet(X2,complement(X0))) = join(X1,meet(X2,join(complement(X0),X1))),
inference(forward_demodulation,[],[f326779,f67470]) ).
fof(f354312,plain,
! [X2,X3,X0,X1] : meet(complement(X1),join(X3,X0)) = meet(complement(X1),join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f222804,f130]) ).
fof(f361907,plain,
! [X2,X0,X1] : meet(X1,join(X0,join(complement(X1),X2))) = meet(X1,join(X2,meet(X1,X0))),
inference(superposition,[],[f220989,f243144]) ).
fof(f361979,plain,
! [X2,X3,X0,X1] : meet(complement(X1),join(X3,meet(join(join(X2,meet(X1,X0)),complement(join(X0,join(complement(X1),X2)))),join(complement(X1),X3)))) = join(meet(complement(X1),join(join(X2,meet(X1,X0)),complement(join(X0,join(complement(X1),X2))))),meet(complement(X1),X3)),
inference(superposition,[],[f567,f243144]) ).
fof(f362179,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(X3,meet(join(join(X2,meet(X1,X0)),complement(join(X0,join(complement(X1),X2)))),join(complement(X1),X3)))),
inference(forward_demodulation,[],[f361979,f286063]) ).
fof(f362231,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f361907,f223603]) ).
fof(f362570,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(X3,meet(join(join(X2,meet(X1,X0)),complement(join(X0,join(complement(X1),X2)))),complement(X1)))),
inference(forward_demodulation,[],[f362179,f327171]) ).
fof(f362884,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(X3,meet(complement(X1),join(complement(join(X0,join(complement(X1),X2))),join(X2,meet(X1,X0)))))),
inference(forward_demodulation,[],[f362570,f15261]) ).
fof(f363124,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(join(X3,join(complement(join(X0,join(complement(X1),X2))),join(X2,meet(X1,X0)))),complement(X1)),
inference(forward_demodulation,[],[f362884,f362231]) ).
fof(f363292,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(X3,join(complement(join(X0,join(complement(X1),X2))),join(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f363124,f5]) ).
fof(f363422,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(X3,join(join(X2,meet(X1,X0)),complement(join(X0,join(complement(X1),X2)))))),
inference(forward_demodulation,[],[f363292,f14681]) ).
fof(f363522,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(X3,join(X2,join(meet(X1,X0),complement(join(X0,join(complement(X1),X2))))))),
inference(forward_demodulation,[],[f363422,f8]) ).
fof(f363591,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(X3,join(complement(join(X0,complement(X1))),join(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f363522,f290695]) ).
fof(f363632,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(X3,join(meet(X1,X0),join(complement(join(X0,complement(X1))),X2)))),
inference(forward_demodulation,[],[f363591,f16737]) ).
fof(f363667,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(join(complement(join(X0,complement(X1))),X2),X3)),
inference(forward_demodulation,[],[f363632,f354312]) ).
fof(f363687,plain,
! [X2,X3,X0,X1] : join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)) = meet(complement(X1),join(complement(join(X0,complement(X1))),join(X2,X3))),
inference(forward_demodulation,[],[f363667,f8]) ).
fof(f363699,plain,
! [X2,X3,X0,X1] : meet(complement(X1),join(X2,X3)) = join(meet(complement(X1),join(X2,meet(X1,X0))),meet(complement(X1),X3)),
inference(forward_demodulation,[],[f363687,f223957]) ).
fof(f363708,plain,
! [X2,X3,X1] : join(meet(complement(X1),X2),meet(complement(X1),X3)) = meet(complement(X1),join(X2,X3)),
inference(forward_demodulation,[],[f363699,f222811]) ).
fof(f363906,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X1,X2)),
inference(superposition,[],[f363708,f5896]) ).
fof(f366968,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(superposition,[],[f13,f363906]) ).
fof(f367242,plain,
$false,
inference(trivial_inequality_removal,[],[f366968]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT217-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.13/0.42 % Computer : n014.cluster.edu
% 0.13/0.42 % Model : x86_64 x86_64
% 0.13/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.42 % Memory : 8046.5625MB
% 0.13/0.42 % OS : Linux 6.8.0-71-generic
% 0.13/0.42 % CPULimit : 300
% 0.13/0.42 % WCLimit : 300
% 0.13/0.42 % DateTime : Sun Sep 27 14:06:17 UTC 2026
% 0.13/0.42 % CPUTime :
% 0.13/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.21/0.49 Running first-order theorem proving
% 0.21/0.49 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
% 16.11/3.10 % (845651)Input is clausal, will run a generic CNF schedule.
% 16.11/3.10 % (845666)dis-21_1_sil=8000:lcm=predicate:random_seed=707667862:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 16.11/3.10 % (845666)Refutation not found, incomplete strategy
% 16.11/3.10 % (845666)------------------------------
% 16.11/3.10 % (845666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.11/3.10 % (845666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/3.10 % (845666)CaDiCaL version: 2.1.3
% 16.11/3.10 % (845666)Termination reason: Refutation not found, incomplete strategy
% 16.11/3.10 % (845666)Time elapsed: 0.001 s
% 16.11/3.10 % (845666)Peak memory usage: 88 MB
% 16.11/3.10 % (845666)Instructions burned: 1 (million)
% 16.11/3.10 % (845661)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3247140281:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 16.11/3.10 % (845665)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3859840104:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 16.11/3.10 % (845663)lrs+10_1_sil=8000:sp=occurrence:random_seed=545875159:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 16.11/3.10 % (845660)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=2163015618:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 16.11/3.10 % (845662)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1681550731:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 16.11/3.10 % (845664)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3828992529:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 16.11/3.10 % (845663)Instruction limit reached!
% 16.11/3.10 % (845663)------------------------------
% 16.11/3.10 % (845663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.11/3.10 % (845663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/3.10 % (845663)CaDiCaL version: 2.1.3
% 16.11/3.10 % (845663)Termination reason: Instruction limit
% 16.11/3.10 % (845663)Termination phase: Saturation
% 16.11/3.10 % (845663)Time elapsed: 0.104 s
% 16.11/3.10 % (845663)Peak memory usage: 88 MB
% 16.11/3.10 % (845663)Instructions burned: 108 (million)
% 16.11/3.10 % (845666)------------------------------
% 16.11/3.10 % (845666)------------------------------
% 16.11/3.10 % (845664)Instruction limit reached!
% 16.11/3.10 % (845664)------------------------------
% 16.11/3.10 % (845664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.11/3.10 % (845664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/3.10 % (845664)CaDiCaL version: 2.1.3
% 16.11/3.10 % (845664)Termination reason: Instruction limit
% 16.11/3.10 % (845664)Termination phase: Saturation
% 16.11/3.10 % (845664)Time elapsed: 0.118 s
% 16.11/3.10 % (845664)Peak memory usage: 88 MB
% 16.11/3.10 % (845664)Instructions burned: 115 (million)
% 16.11/3.10 % (845665)Instruction limit reached!
% 16.11/3.10 % (845665)------------------------------
% 16.11/3.10 % (845665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.11/3.10 % (845665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/3.10 % (845665)CaDiCaL version: 2.1.3
% 16.11/3.10 % (845665)Termination reason: Instruction limit
% 16.11/3.10 % (845665)Termination phase: Saturation
% 16.11/3.10 % (845665)Time elapsed: 0.168 s
% 16.11/3.10 % (845665)Peak memory usage: 89 MB
% 16.11/3.10 % (845665)Instructions burned: 180 (million)
% 16.11/3.10 % (845677)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3617639489: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)
% 16.11/3.10 % (845677)Refutation not found, incomplete strategy
% 16.11/3.10 % (845677)------------------------------
% 16.11/3.10 % (845677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.11/3.10 % (845677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.11/3.10 % (845677)CaDiCaL version: 2.1.3
% 16.11/3.10 % (845677)Termination reason: Refutation not found, incomplete strategy
% 16.11/3.10 % (845677)Time elapsed: 0.001 s
% 16.11/3.10 % (845677)Peak memory usage: 88 MB
% 16.11/3.10 % (845677)Instructions burned: 1 (million)
% 26.35/4.69 % (845676)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=3836620385:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 26.35/4.69 % (845676)Refutation not found, incomplete strategy
% 26.35/4.69 % (845676)------------------------------
% 26.35/4.69 % (845676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.69 % (845676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.69 % (845676)CaDiCaL version: 2.1.3
% 26.35/4.69 % (845676)Termination reason: Refutation not found, incomplete strategy
% 26.35/4.69 % (845676)Time elapsed: 0.002 s
% 26.35/4.69 % (845676)Peak memory usage: 87 MB
% 26.35/4.69 % (845678)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1330855435:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 26.35/4.69 % (845678)Refutation not found, incomplete strategy
% 26.35/4.69 % (845678)------------------------------
% 26.35/4.69 % (845678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.69 % (845678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.69 % (845678)CaDiCaL version: 2.1.3
% 26.35/4.69 % (845678)Termination reason: Refutation not found, incomplete strategy
% 26.35/4.69 % (845678)Time elapsed: 0.002 s
% 26.35/4.69 % (845678)Peak memory usage: 87 MB
% 26.35/4.69 % (845680)lrs+10_64_to=lpo:sil=8000:random_seed=1895156989:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 26.35/4.69 % (845677)------------------------------
% 26.35/4.69 % (845677)------------------------------
% 26.35/4.69 % (845680)Instruction limit reached!
% 26.35/4.69 % (845680)------------------------------
% 26.35/4.69 % (845680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.69 % (845680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.69 % (845680)CaDiCaL version: 2.1.3
% 26.35/4.69 % (845680)Termination reason: Instruction limit
% 26.35/4.69 % (845680)Termination phase: Saturation
% 26.35/4.69 % (845680)Time elapsed: 0.124 s
% 26.35/4.69 % (845680)Peak memory usage: 88 MB
% 26.35/4.69 % (845680)Instructions burned: 127 (million)
% 26.35/4.69 % (845686)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1286988967:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 26.35/4.69 % (845676)------------------------------
% 26.35/4.69 % (845676)------------------------------
% 26.35/4.69 % (845687)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3405578353:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 26.35/4.69 % (845678)------------------------------
% 26.35/4.69 % (845678)------------------------------
% 26.35/4.69 % (845687)Instruction limit reached!
% 26.35/4.69 % (845687)------------------------------
% 26.35/4.69 % (845687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.69 % (845687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.69 % (845687)CaDiCaL version: 2.1.3
% 26.35/4.69 % (845687)Termination reason: Instruction limit
% 26.35/4.69 % (845687)Termination phase: Saturation
% 26.35/4.69 % (845687)Time elapsed: 0.081 s
% 26.35/4.69 % (845687)Peak memory usage: 90 MB
% 26.35/4.69 % (845687)Instructions burned: 157 (million)
% 26.35/4.69 % (845690)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2433140609:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 26.35/4.69 % (845686)Instruction limit reached!
% 26.35/4.69 % (845686)------------------------------
% 26.35/4.69 % (845686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.69 % (845686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.35/4.69 % (845686)CaDiCaL version: 2.1.3
% 26.35/4.69 % (845686)Termination reason: Instruction limit
% 26.35/4.69 % (845686)Termination phase: Saturation
% 26.35/4.69 % (845686)Time elapsed: 0.198 s
% 26.35/4.69 % (845686)Peak memory usage: 89 MB
% 26.35/4.69 % (845686)Instructions burned: 194 (million)
% 26.35/4.69 % (845692)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4019584270:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 26.35/4.69 % (845692)Refutation not found, incomplete strategy
% 26.35/4.69 % (845692)------------------------------
% 26.35/4.69 % (845692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.35/4.69 % (845692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.67/8.57 % (845692)CaDiCaL version: 2.1.3
% 54.67/8.57 % (845692)Termination reason: Refutation not found, incomplete strategy
% 54.67/8.57 % (845692)Time elapsed: 0.001 s
% 54.67/8.57 % (845692)Peak memory usage: 87 MB
% 54.67/8.57 % (845691)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=3778389641:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 54.67/8.57 % (845691)Instruction limit reached!
% 54.67/8.57 % (845691)------------------------------
% 54.67/8.57 % (845691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.67/8.57 % (845691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.67/8.57 % (845691)CaDiCaL version: 2.1.3
% 54.67/8.57 % (845691)Termination reason: Instruction limit
% 54.67/8.57 % (845691)Termination phase: Saturation
% 54.67/8.57 % (845691)Time elapsed: 0.107 s
% 54.67/8.57 % (845691)Peak memory usage: 89 MB
% 54.67/8.57 % (845691)Instructions burned: 106 (million)
% 54.67/8.57 % (845694)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=671900300:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2989 on theBenchmark for (2989ds/242Mi)
% 54.67/8.57 % (845692)------------------------------
% 54.67/8.57 % (845692)------------------------------
% 54.67/8.57 % (845698)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3514452197:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 54.67/8.57 % (845694)Instruction limit reached!
% 54.67/8.57 % (845694)------------------------------
% 54.67/8.57 % (845694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.67/8.57 % (845694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.67/8.57 % (845694)CaDiCaL version: 2.1.3
% 54.67/8.57 % (845694)Termination reason: Instruction limit
% 54.67/8.57 % (845694)Termination phase: Saturation
% 54.67/8.57 % (845694)Time elapsed: 0.242 s
% 54.67/8.57 % (845694)Peak memory usage: 90 MB
% 54.67/8.57 % (845694)Instructions burned: 243 (million)
% 54.67/8.57 % (845700)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2060827061:i=134:sd=2:doe=on:ss=axioms:sgt=14_2986 on theBenchmark for (2986ds/134Mi)
% 54.67/8.57 % (845700)Instruction limit reached!
% 54.67/8.57 % (845700)------------------------------
% 54.67/8.57 % (845700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.67/8.57 % (845700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.67/8.57 % (845700)CaDiCaL version: 2.1.3
% 54.67/8.57 % (845700)Termination reason: Instruction limit
% 54.67/8.57 % (845700)Termination phase: Saturation
% 54.67/8.57 % (845700)Time elapsed: 0.129 s
% 54.67/8.57 % (845700)Peak memory usage: 89 MB
% 54.67/8.57 % (845700)Instructions burned: 134 (million)
% 54.67/8.57 % (845703)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3187212847:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 54.67/8.57 % (845704)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2765003501:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 54.67/8.57 % (845704)Instruction limit reached!
% 54.67/8.57 % (845704)------------------------------
% 54.67/8.57 % (845704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.67/8.57 % (845704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.67/8.57 % (845704)CaDiCaL version: 2.1.3
% 54.67/8.57 % (845704)Termination reason: Instruction limit
% 54.67/8.57 % (845704)Termination phase: Saturation
% 54.67/8.57 % (845704)Time elapsed: 0.194 s
% 54.67/8.57 % (845704)Peak memory usage: 91 MB
% 54.67/8.57 % (845704)Instructions burned: 191 (million)
% 54.67/8.57 % (845709)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=472522492:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 54.67/8.57 % (845703)Instruction limit reached!
% 54.67/8.57 % (845703)------------------------------
% 54.67/8.57 % (845703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 54.67/8.57 % (845703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.67/8.57 % (845703)CaDiCaL version: 2.1.3
% 54.67/8.57 % (845703)Termination reason: Instruction limit
% 54.67/8.57 % (845703)Termination phase: Saturation
% 54.67/8.57 % (845703)Time elapsed: 0.523 s
% 54.67/8.57 % (845703)Peak memory usage: 93 MB
% 54.67/8.57 % (845703)Instructions burned: 499 (million)
% 78.34/12.04 % (845711)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=189180460:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 78.34/12.04 % (845709)Instruction limit reached!
% 78.34/12.04 % (845709)------------------------------
% 78.34/12.04 % (845709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.34/12.04 % (845709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.34/12.04 % (845709)CaDiCaL version: 2.1.3
% 78.34/12.04 % (845709)Termination reason: Instruction limit
% 78.34/12.04 % (845709)Termination phase: Saturation
% 78.34/12.04 % (845709)Time elapsed: 0.246 s
% 78.34/12.04 % (845709)Peak memory usage: 91 MB
% 78.34/12.04 % (845709)Instructions burned: 264 (million)
% 78.34/12.04 % (845711)Instruction limit reached!
% 78.34/12.04 % (845711)------------------------------
% 78.34/12.04 % (845711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.34/12.04 % (845711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.34/12.04 % (845711)CaDiCaL version: 2.1.3
% 78.34/12.04 % (845711)Termination reason: Instruction limit
% 78.34/12.04 % (845711)Termination phase: Saturation
% 78.34/12.04 % (845711)Time elapsed: 0.150 s
% 78.34/12.04 % (845711)Peak memory usage: 89 MB
% 78.34/12.04 % (845711)Instructions burned: 156 (million)
% 78.34/12.04 % (845713)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=3692819412:i=3256:kws=precedence:bd=preordered:av=off_2974 on theBenchmark for (2974ds/3256Mi)
% 78.34/12.04 % (845714)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=259001318:i=537:av=off:ss=included_2973 on theBenchmark for (2973ds/537Mi)
% 78.34/12.04 % (845690)Instruction limit reached!
% 78.34/12.04 % (845690)------------------------------
% 78.34/12.04 % (845690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.34/12.04 % (845690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.34/12.04 % (845690)CaDiCaL version: 2.1.3
% 78.34/12.04 % (845690)Termination reason: Instruction limit
% 78.34/12.04 % (845690)Termination phase: Saturation
% 78.34/12.04 % (845690)Time elapsed: 2.196 s
% 78.34/12.04 % (845690)Peak memory usage: 148 MB
% 78.34/12.04 % (845690)Instructions burned: 3396 (million)
% 78.34/12.04 % (845714)Instruction limit reached!
% 78.34/12.04 % (845714)------------------------------
% 78.34/12.04 % (845714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.34/12.04 % (845714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.34/12.04 % (845714)CaDiCaL version: 2.1.3
% 78.34/12.04 % (845714)Termination reason: Instruction limit
% 78.34/12.04 % (845714)Termination phase: Saturation
% 78.34/12.04 % (845714)Time elapsed: 0.441 s
% 78.34/12.04 % (845714)Peak memory usage: 93 MB
% 78.34/12.04 % (845714)Instructions burned: 537 (million)
% 78.34/12.04 % (845717)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3291514508:i=180:bd=preordered:av=off_2967 on theBenchmark for (2967ds/180Mi)
% 78.34/12.04 % (845717)Instruction limit reached!
% 78.34/12.04 % (845717)------------------------------
% 78.34/12.04 % (845717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.34/12.04 % (845717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.34/12.04 % (845717)CaDiCaL version: 2.1.3
% 78.34/12.04 % (845717)Termination reason: Instruction limit
% 78.34/12.04 % (845717)Termination phase: Saturation
% 78.34/12.04 % (845717)Time elapsed: 0.089 s
% 78.34/12.04 % (845717)Peak memory usage: 89 MB
% 78.34/12.04 % (845717)Instructions burned: 182 (million)
% 78.34/12.04 % (845718)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=3561100451:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2967 on theBenchmark for (2967ds/10307Mi)
% 78.34/12.04 % (845720)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=1503955602:i=412:gtgl=4:gtg=exists_all_2964 on theBenchmark for (2964ds/412Mi)
% 78.34/12.04 % (845720)Instruction limit reached!
% 78.34/12.04 % (845720)------------------------------
% 78.34/12.04 % (845720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 78.34/12.04 % (845720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 78.34/12.04 % (845720)CaDiCaL version: 2.1.3
% 78.34/12.04 % (845720)Termination reason: Instruction limit
% 119.39/17.77 % (845720)Termination phase: Saturation
% 119.39/17.77 % (845720)Time elapsed: 0.212 s
% 119.39/17.77 % (845720)Peak memory usage: 94 MB
% 119.39/17.77 % (845720)Instructions burned: 414 (million)
% 119.39/17.77 % (845723)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=644242192:s2pl=no:i=8478:s2at=4:nm=6_2961 on theBenchmark for (2961ds/8478Mi)
% 119.39/17.77 % (845713)Instruction limit reached!
% 119.39/17.77 % (845713)------------------------------
% 119.39/17.77 % (845713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.39/17.77 % (845713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.39/17.77 % (845713)CaDiCaL version: 2.1.3
% 119.39/17.77 % (845713)Termination reason: Instruction limit
% 119.39/17.77 % (845713)Termination phase: Saturation
% 119.39/17.77 % (845713)Time elapsed: 3.295 s
% 119.39/17.77 % (845713)Peak memory usage: 149 MB
% 119.39/17.77 % (845713)Instructions burned: 3256 (million)
% 119.39/17.77 % (845698)Instruction limit reached!
% 119.39/17.77 % (845698)------------------------------
% 119.39/17.77 % (845698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.39/17.77 % (845698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.39/17.77 % (845698)CaDiCaL version: 2.1.3
% 119.39/17.77 % (845698)Termination reason: Instruction limit
% 119.39/17.77 % (845698)Termination phase: Saturation
% 119.39/17.77 % (845698)Time elapsed: 4.774 s
% 119.39/17.77 % (845698)Peak memory usage: 165 MB
% 119.39/17.77 % (845698)Instructions burned: 5209 (million)
% 119.39/17.77 % (845727)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=1924478596:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2939 on theBenchmark for (2939ds/303Mi)
% 119.39/17.77 % (845727)Refutation not found, incomplete strategy
% 119.39/17.77 % (845727)------------------------------
% 119.39/17.77 % (845727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.39/17.77 % (845727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.39/17.77 % (845727)CaDiCaL version: 2.1.3
% 119.39/17.77 % (845727)Termination reason: Refutation not found, incomplete strategy
% 119.39/17.77 % (845727)Time elapsed: 0.002 s
% 119.39/17.77 % (845727)Peak memory usage: 88 MB
% 119.39/17.77 % (845727)Instructions burned: 1 (million)
% 119.39/17.77 % (845728)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=645209608:st=4:i=720:sd=3:fsr=off:ss=axioms_2937 on theBenchmark for (2937ds/720Mi)
% 119.39/17.77 % (845728)Refutation not found, incomplete strategy
% 119.39/17.77 % (845728)------------------------------
% 119.39/17.77 % (845728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.39/17.77 % (845728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.39/17.77 % (845728)CaDiCaL version: 2.1.3
% 119.39/17.77 % (845728)Termination reason: Refutation not found, incomplete strategy
% 119.39/17.77 % (845728)Time elapsed: 0.002 s
% 119.39/17.77 % (845728)Peak memory usage: 87 MB
% 119.39/17.77 % (845727)------------------------------
% 119.39/17.77 % (845727)------------------------------
% 119.39/17.77 % (845728)------------------------------
% 119.39/17.77 % (845728)------------------------------
% 119.39/17.77 % (845733)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3807261718:i=598:bs=on:bd=preordered:av=off:ss=axioms_2933 on theBenchmark for (2933ds/598Mi)
% 119.39/17.77 % (845738)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3222592373:i=2989:sd=3:ss=axioms:sgt=60_2931 on theBenchmark for (2931ds/2989Mi)
% 119.39/17.77 % (845733)Instruction limit reached!
% 119.39/17.77 % (845733)------------------------------
% 119.39/17.77 % (845733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 119.39/17.77 % (845733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.39/17.77 % (845733)CaDiCaL version: 2.1.3
% 119.39/17.77 % (845733)Termination reason: Instruction limit
% 119.39/17.77 % (845733)Termination phase: Saturation
% 119.39/17.77 % (845733)Time elapsed: 0.635 s
% 119.39/17.77 % (845733)Peak memory usage: 94 MB
% 119.39/17.77 % (845733)Instructions burned: 599 (million)
% 119.39/17.77 % (845743)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=4168406218:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2924 on theBenchmark for (2924ds/1997Mi)
% 166.23/24.29 % (845723)Instruction limit reached!
% 166.23/24.29 % (845723)------------------------------
% 166.23/24.29 % (845723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.23/24.29 % (845723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.23/24.29 % (845723)CaDiCaL version: 2.1.3
% 166.23/24.29 % (845723)Termination reason: Instruction limit
% 166.23/24.29 % (845723)Termination phase: Saturation
% 166.23/24.29 % (845723)Time elapsed: 4.711 s
% 166.23/24.29 % (845723)Peak memory usage: 198 MB
% 166.23/24.29 % (845723)Instructions burned: 8478 (million)
% 166.23/24.29 % (845747)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=613806205:i=2088:bd=preordered:av=off_2912 on theBenchmark for (2912ds/2088Mi)
% 166.23/24.29 % (845743)Instruction limit reached!
% 166.23/24.29 % (845743)------------------------------
% 166.23/24.29 % (845743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.23/24.29 % (845743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.23/24.29 % (845743)CaDiCaL version: 2.1.3
% 166.23/24.29 % (845743)Termination reason: Instruction limit
% 166.23/24.29 % (845743)Termination phase: Saturation
% 166.23/24.29 % (845743)Time elapsed: 2.154 s
% 166.23/24.29 % (845743)Peak memory usage: 138 MB
% 166.23/24.29 % (845743)Instructions burned: 1997 (million)
% 166.23/24.29 % (845747)Instruction limit reached!
% 166.23/24.29 % (845747)------------------------------
% 166.23/24.29 % (845747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.23/24.29 % (845747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.23/24.29 % (845747)CaDiCaL version: 2.1.3
% 166.23/24.29 % (845747)Termination reason: Instruction limit
% 166.23/24.29 % (845747)Termination phase: Saturation
% 166.23/24.29 % (845747)Time elapsed: 1.163 s
% 166.23/24.29 % (845747)Peak memory usage: 139 MB
% 166.23/24.29 % (845747)Instructions burned: 2097 (million)
% 166.23/24.29 % (845738)Instruction limit reached!
% 166.23/24.29 % (845738)------------------------------
% 166.23/24.29 % (845738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.23/24.29 % (845738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.23/24.29 % (845738)CaDiCaL version: 2.1.3
% 166.23/24.29 % (845738)Termination reason: Instruction limit
% 166.23/24.29 % (845738)Termination phase: Saturation
% 166.23/24.29 % (845738)Time elapsed: 3.055 s
% 166.23/24.29 % (845738)Peak memory usage: 147 MB
% 166.23/24.29 % (845738)Instructions burned: 2989 (million)
% 166.23/24.29 % (845749)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3783509296:i=1098:nicw=on_2900 on theBenchmark for (2900ds/1098Mi)
% 166.23/24.29 % (845752)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=304076708:i=433:bd=preordered_2898 on theBenchmark for (2898ds/433Mi)
% 166.23/24.29 % (845752)Refutation not found, incomplete strategy
% 166.23/24.29 % (845752)------------------------------
% 166.23/24.29 % (845752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.23/24.29 % (845752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.23/24.29 % (845752)CaDiCaL version: 2.1.3
% 166.23/24.29 % (845752)Termination reason: Refutation not found, incomplete strategy
% 166.23/24.29 % (845752)Time elapsed: 0.001 s
% 166.23/24.29 % (845752)Peak memory usage: 88 MB
% 166.23/24.29 % (845752)Instructions burned: 1 (million)
% 166.23/24.29 % (845753)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1082332095:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2898 on theBenchmark for (2898ds/2942Mi)
% 166.23/24.29 % (845752)------------------------------
% 166.23/24.29 % (845752)------------------------------
% 166.23/24.29 % (845759)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=959329700:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2895 on theBenchmark for (2895ds/6922Mi)
% 166.23/24.29 % (845749)Instruction limit reached!
% 166.23/24.29 % (845749)------------------------------
% 166.23/24.29 % (845749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 166.23/24.29 % (845749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 166.23/24.29 % (845749)CaDiCaL version: 2.1.3
% 166.23/24.29 % (845749)Termination reason: Instruction limit
% 166.23/24.29 % (845749)Termination phase: Saturation
% 166.23/24.29 % (845749)Time elapsed: 1.062 s
% 193.74/28.05 % (845749)Peak memory usage: 99 MB
% 193.74/28.05 % (845749)Instructions burned: 1099 (million)
% 193.74/28.05 % (845763)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3099723696:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2887 on theBenchmark for (2887ds/596Mi)
% 193.74/28.05 % (845763)Refutation not found, incomplete strategy
% 193.74/28.05 % (845763)------------------------------
% 193.74/28.05 % (845763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.74/28.05 % (845763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.74/28.05 % (845763)CaDiCaL version: 2.1.3
% 193.74/28.05 % (845763)Termination reason: Refutation not found, incomplete strategy
% 193.74/28.05 % (845763)Time elapsed: 0.003 s
% 193.74/28.05 % (845763)Peak memory usage: 88 MB
% 193.74/28.05 % (845763)Instructions burned: 1 (million)
% 193.74/28.05 % (845763)------------------------------
% 193.74/28.05 % (845763)------------------------------
% 193.74/28.05 % (845767)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=372389829:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2881 on theBenchmark for (2881ds/4123Mi)
% 193.74/28.05 % (845753)Instruction limit reached!
% 193.74/28.05 % (845753)------------------------------
% 193.74/28.05 % (845753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.74/28.05 % (845753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.74/28.05 % (845753)CaDiCaL version: 2.1.3
% 193.74/28.05 % (845753)Termination reason: Instruction limit
% 193.74/28.05 % (845753)Termination phase: Saturation
% 193.74/28.05 % (845753)Time elapsed: 2.097 s
% 193.74/28.05 % (845753)Peak memory usage: 137 MB
% 193.74/28.05 % (845753)Instructions burned: 2942 (million)
% 193.74/28.05 % (845769)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=557795130:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2875 on theBenchmark for (2875ds/16411Mi)
% 193.74/28.05 % (845718)Instruction limit reached!
% 193.74/28.05 % (845718)------------------------------
% 193.74/28.05 % (845718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.74/28.05 % (845718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.74/28.05 % (845718)CaDiCaL version: 2.1.3
% 193.74/28.05 % (845718)Termination reason: Instruction limit
% 193.74/28.05 % (845718)Termination phase: Saturation
% 193.74/28.05 % (845718)Time elapsed: 11.163 s
% 193.74/28.05 % (845718)Peak memory usage: 209 MB
% 193.74/28.05 % (845718)Instructions burned: 10307 (million)
% 193.74/28.05 % (845773)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1070293444:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2852 on theBenchmark for (2852ds/1670Mi)
% 193.74/28.05 % (845767)Instruction limit reached!
% 193.74/28.05 % (845767)------------------------------
% 193.74/28.05 % (845767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.74/28.05 % (845767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.74/28.05 % (845767)CaDiCaL version: 2.1.3
% 193.74/28.05 % (845767)Termination reason: Instruction limit
% 193.74/28.05 % (845767)Termination phase: Saturation
% 193.74/28.05 % (845767)Time elapsed: 4.124 s
% 193.74/28.05 % (845767)Peak memory usage: 158 MB
% 193.74/28.05 % (845767)Instructions burned: 4123 (million)
% 193.74/28.05 % (845777)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=705291153:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2837 on theBenchmark for (2837ds/1722Mi)
% 193.74/28.05 % (845773)Instruction limit reached!
% 193.74/28.05 % (845773)------------------------------
% 193.74/28.05 % (845773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 193.74/28.05 % (845773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 193.74/28.05 % (845773)CaDiCaL version: 2.1.3
% 193.74/28.05 % (845773)Termination reason: Instruction limit
% 193.74/28.05 % (845773)Termination phase: Saturation
% 193.74/28.05 % (845773)Time elapsed: 1.763 s
% 193.74/28.05 % (845773)Peak memory usage: 135 MB
% 193.74/28.05 % (845773)Instructions burned: 1670 (million)
% 193.74/28.05 % (845780)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1910860635:cts=off:cond=on:i=9530:bs=on:fsd=on_2832 on theBenchmark for (2832ds/9530Mi)
% 209.67/30.35 % (845759)Instruction limit reached!
% 209.67/30.35 % (845759)------------------------------
% 209.67/30.35 % (845759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.67/30.35 % (845759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.67/30.35 % (845759)CaDiCaL version: 2.1.3
% 209.67/30.35 % (845759)Termination reason: Instruction limit
% 209.67/30.35 % (845759)Termination phase: Saturation
% 209.67/30.35 % (845759)Time elapsed: 6.911 s
% 209.67/30.35 % (845759)Peak memory usage: 175 MB
% 209.67/30.35 % (845759)Instructions burned: 6923 (million)
% 209.67/30.35 % (845782)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2117205852:st=2:i=4495:sd=10:ss=included_2824 on theBenchmark for (2824ds/4495Mi)
% 209.67/30.35 % (845777)Instruction limit reached!
% 209.67/30.35 % (845777)------------------------------
% 209.67/30.35 % (845777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.67/30.35 % (845777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.67/30.35 % (845777)CaDiCaL version: 2.1.3
% 209.67/30.35 % (845777)Termination reason: Instruction limit
% 209.67/30.35 % (845777)Termination phase: Saturation
% 209.67/30.35 % (845777)Time elapsed: 1.694 s
% 209.67/30.35 % (845777)Peak memory usage: 134 MB
% 209.67/30.35 % (845777)Instructions burned: 1723 (million)
% 209.67/30.35 % (845784)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3598117311:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2818 on theBenchmark for (2818ds/4920Mi)
% 209.67/30.35 % (845769)Instruction limit reached!
% 209.67/30.35 % (845769)------------------------------
% 209.67/30.35 % (845769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.67/30.35 % (845769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.67/30.35 % (845769)CaDiCaL version: 2.1.3
% 209.67/30.35 % (845769)Termination reason: Instruction limit
% 209.67/30.35 % (845769)Termination phase: Saturation
% 209.67/30.35 % (845769)Time elapsed: 9.299 s
% 209.67/30.35 % (845769)Peak memory usage: 251 MB
% 209.67/30.35 % (845769)Instructions burned: 16412 (million)
% 209.67/30.35 % (845788)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=3100311226:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2780 on theBenchmark for (2780ds/2083Mi)
% 209.67/30.35 % (845782)Instruction limit reached!
% 209.67/30.35 % (845782)------------------------------
% 209.67/30.35 % (845782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.67/30.35 % (845782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.67/30.35 % (845782)CaDiCaL version: 2.1.3
% 209.67/30.35 % (845782)Termination reason: Instruction limit
% 209.67/30.35 % (845782)Termination phase: Saturation
% 209.67/30.35 % (845782)Time elapsed: 4.681 s
% 209.67/30.35 % (845782)Peak memory usage: 157 MB
% 209.67/30.35 % (845782)Instructions burned: 4497 (million)
% 209.67/30.35 % (845790)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2165228746:i=4629:av=off:gsp=on_2774 on theBenchmark for (2774ds/4629Mi)
% 209.67/30.35 % (845784)Instruction limit reached!
% 209.67/30.35 % (845784)------------------------------
% 209.67/30.35 % (845784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.67/30.35 % (845784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.67/30.35 % (845784)CaDiCaL version: 2.1.3
% 209.67/30.35 % (845784)Termination reason: Instruction limit
% 209.67/30.35 % (845784)Termination phase: Saturation
% 209.67/30.35 % (845784)Time elapsed: 4.858 s
% 209.67/30.35 % (845784)Peak memory usage: 164 MB
% 209.67/30.35 % (845784)Instructions burned: 4921 (million)
% 209.67/30.35 % (845788)Instruction limit reached!
% 209.67/30.35 % (845788)------------------------------
% 209.67/30.35 % (845788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 209.67/30.35 % (845788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 209.67/30.35 % (845788)CaDiCaL version: 2.1.3
% 209.67/30.35 % (845788)Termination reason: Instruction limit
% 209.67/30.35 % (845788)Termination phase: Saturation
% 209.67/30.35 % (845788)Time elapsed: 1.243 s
% 209.67/30.35 % (845788)Peak memory usage: 139 MB
% 209.67/30.35 % (845788)Instructions burned: 2084 (million)
% 209.67/30.35 % (845792)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2788150240:i=1258:av=off_2767 on theBenchmark for (2767ds/1258Mi)
% 148.18/31.08 % (845793)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1550327685:i=7343:av=off:ss=included_2766 on theBenchmark for (2766ds/7343Mi)
% 148.18/31.08 % (845790)Refutation not found, incomplete strategy
% 148.18/31.08 % (845790)------------------------------
% 148.18/31.08 % (845790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845790)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845790)Termination reason: Refutation not found, incomplete strategy
% 148.18/31.08 % (845790)Time elapsed: 0.962 s
% 148.18/31.08 % (845790)Peak memory usage: 127 MB
% 148.18/31.08 % (845790)Instructions burned: 858 (million)
% 148.18/31.08 % (845790)------------------------------
% 148.18/31.08 % (845790)------------------------------
% 148.18/31.08 % (845796)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3018501563:i=1325:sd=2:ss=axioms:sgt=16_2758 on theBenchmark for (2758ds/1325Mi)
% 148.18/31.08 % (845796)Refutation not found, incomplete strategy
% 148.18/31.08 % (845796)------------------------------
% 148.18/31.08 % (845796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845796)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845796)Termination reason: Refutation not found, incomplete strategy
% 148.18/31.08 % (845796)Time elapsed: 0.002 s
% 148.18/31.08 % (845796)Peak memory usage: 87 MB
% 148.18/31.08 % (845792)Instruction limit reached!
% 148.18/31.08 % (845792)------------------------------
% 148.18/31.08 % (845792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845792)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845792)Termination reason: Instruction limit
% 148.18/31.08 % (845792)Termination phase: Saturation
% 148.18/31.08 % (845792)Time elapsed: 0.980 s
% 148.18/31.08 % (845792)Peak memory usage: 94 MB
% 148.18/31.08 % (845792)Instructions burned: 1259 (million)
% 148.18/31.08 % (845798)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=2276817031:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2755 on theBenchmark for (2755ds/2646Mi)
% 148.18/31.08 % (845796)------------------------------
% 148.18/31.08 % (845796)------------------------------
% 148.18/31.08 % (845800)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=4211630336:i=1489:sd=2:ep=R:ss=axioms_2752 on theBenchmark for (2752ds/1489Mi)
% 148.18/31.08 % (845800)Refutation not found, incomplete strategy
% 148.18/31.08 % (845800)------------------------------
% 148.18/31.08 % (845800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845800)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845800)Termination reason: Refutation not found, incomplete strategy
% 148.18/31.08 % (845800)Time elapsed: 0.940 s
% 148.18/31.08 % (845800)Peak memory usage: 127 MB
% 148.18/31.08 % (845800)Instructions burned: 857 (million)
% 148.18/31.08 % (845800)------------------------------
% 148.18/31.08 % (845800)------------------------------
% 148.18/31.08 % (845802)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=113244105:i=1503_2737 on theBenchmark for (2737ds/1503Mi)
% 148.18/31.08 % (845780)Instruction limit reached!
% 148.18/31.08 % (845780)------------------------------
% 148.18/31.08 % (845780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845780)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845780)Termination reason: Instruction limit
% 148.18/31.08 % (845780)Termination phase: Saturation
% 148.18/31.08 % (845780)Time elapsed: 9.803 s
% 148.18/31.08 % (845780)Peak memory usage: 187 MB
% 148.18/31.08 % (845780)Instructions burned: 9531 (million)
% 148.18/31.08 % (845804)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=2565332632:i=13942:kws=frequency_2732 on theBenchmark for (2732ds/13942Mi)
% 148.18/31.08 % (845798)Instruction limit reached!
% 148.18/31.08 % (845798)------------------------------
% 148.18/31.08 % (845798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845798)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845798)Termination reason: Instruction limit
% 148.18/31.08 % (845798)Termination phase: Saturation
% 148.18/31.08 % (845798)Time elapsed: 2.557 s
% 148.18/31.08 % (845798)Peak memory usage: 145 MB
% 148.18/31.08 % (845798)Instructions burned: 2647 (million)
% 148.18/31.08 % (845793)Instruction limit reached!
% 148.18/31.08 % (845793)------------------------------
% 148.18/31.08 % (845793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845793)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845793)Termination reason: Instruction limit
% 148.18/31.08 % (845793)Termination phase: Saturation
% 148.18/31.08 % (845793)Time elapsed: 3.768 s
% 148.18/31.08 % (845793)Peak memory usage: 177 MB
% 148.18/31.08 % (845793)Instructions burned: 7346 (million)
% 148.18/31.08 % (845806)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=2572683615:i=3604:fsr=off:er=filter_2727 on theBenchmark for (2727ds/3604Mi)
% 148.18/31.08 % (845802)Refutation not found, incomplete strategy
% 148.18/31.08 % (845802)------------------------------
% 148.18/31.08 % (845802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845802)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845802)Termination reason: Refutation not found, incomplete strategy
% 148.18/31.08 % (845802)Time elapsed: 0.903 s
% 148.18/31.08 % (845802)Peak memory usage: 127 MB
% 148.18/31.08 % (845802)Instructions burned: 857 (million)
% 148.18/31.08 % (845807)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1625974168:i=1876:sd=1:ss=included:sgt=32_2727 on theBenchmark for (2727ds/1876Mi)
% 148.18/31.08 % (845802)------------------------------
% 148.18/31.08 % (845802)------------------------------
% 148.18/31.08 % (845810)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1614018084:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2723 on theBenchmark for (2723ds/1932Mi)
% 148.18/31.08 % (845810)Refutation not found, incomplete strategy
% 148.18/31.08 % (845810)------------------------------
% 148.18/31.08 % (845810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845810)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845810)Termination reason: Refutation not found, incomplete strategy
% 148.18/31.08 % (845810)Time elapsed: 0.509 s
% 148.18/31.08 % (845810)Peak memory usage: 127 MB
% 148.18/31.08 % (845810)Instructions burned: 860 (million)
% 148.18/31.08 % (845810)------------------------------
% 148.18/31.08 % (845810)------------------------------
% 148.18/31.08 % (845807)Instruction limit reached!
% 148.18/31.08 % (845807)------------------------------
% 148.18/31.08 % (845807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845807)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845807)Termination reason: Instruction limit
% 148.18/31.08 % (845807)Termination phase: Saturation
% 148.18/31.08 % (845807)Time elapsed: 1.374 s
% 148.18/31.08 % (845807)Peak memory usage: 136 MB
% 148.18/31.08 % (845807)Instructions burned: 1877 (million)
% 148.18/31.08 % (845812)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=3021996549:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2712 on theBenchmark for (2712ds/1980Mi)
% 148.18/31.08 % (845813)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=2954908294:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2710 on theBenchmark for (2710ds/3902Mi)
% 148.18/31.08 % (845813)Refutation not found, incomplete strategy
% 148.18/31.08 % (845813)------------------------------
% 148.18/31.08 % (845813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 148.18/31.08 % (845813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 148.18/31.08 % (845813)CaDiCaL version: 2.1.3
% 148.18/31.08 % (845813)Termination reason: Refutation not found, incomplete strategy
% 148.18/31.08 % (845813)Time elapsed: 0.473 s
% 148.18/31.08 % (845813)Peak memory usage: 127 MB
% 148.18/31.08 % (845813)Instructions burned: 859 (million)
% 148.18/31.08 % (845661)First to succeed.
% 148.18/31.08 % (845661)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-845651"
% 148.18/31.08 % (845813)------------------------------
% 148.18/31.08 % (845813)------------------------------
% 148.18/31.08 % (845816)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=3353947750:avsq=on:i=3916:aac=none:amm=off_2702 on theBenchmark for (2702ds/3916Mi)
% 148.18/31.08 % (845661)Refutation found. Thanks to Tanya!
% 148.18/31.08 % SZS status Unsatisfiable for theBenchmark
% 148.18/31.08 % SZS output start Proof for theBenchmark
% See solution above
% 215.25/31.32 % (845661)------------------------------
% 215.25/31.32 % (845661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.25/31.32 % (845661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.25/31.32 % (845661)CaDiCaL version: 2.1.3
% 215.25/31.32 % (845661)Termination reason: Refutation
% 215.25/31.32 % (845661)Time elapsed: 29.529 s
% 215.25/31.32 % (845661)Peak memory usage: 326 MB
% 215.25/31.32 % (845661)Instructions burned: 28332 (million)
% 215.25/31.32 % (845661)------------------------------
% 215.25/31.32 % (845661)------------------------------
% 215.25/31.32 % (845651)Success in time 30.276 s
% 215.25/31.32 % Vampire exiting
%------------------------------------------------------------------------------