%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT194-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 : n017.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:13 AM UTC 2026
% Result : Unsatisfiable 30.26s 5.39s
% Output : Refutation 31.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 98
% Number of leaves : 12
% Syntax : Number of formulae : 308 ( 303 unt; 0 def)
% Number of atoms : 315 ( 314 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 16 ( 9 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 757 ( 757 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X0,meet(X2,X3)))) = meet(X0,join(X1,meet(X2,join(meet(X0,X3),meet(X1,X3))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H32) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f15,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f17,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f21,plain,
! [X2,X3,X0,X1] : meet(X1,join(X2,meet(X1,meet(X3,X0)))) = meet(X1,join(X2,meet(X3,join(meet(X0,X1),meet(X2,X0))))),
inference(superposition,[],[f12,f5]) ).
fof(f25,plain,
! [X2,X3,X0,X1] : meet(X2,join(X1,meet(X2,meet(X3,X0)))) = meet(X2,join(X1,meet(X3,join(meet(X2,X0),meet(X0,X1))))),
inference(superposition,[],[f12,f5]) ).
fof(f28,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,meet(X2,X1)))) = meet(X0,join(meet(X0,X1),meet(X2,meet(X0,X1)))),
inference(superposition,[],[f12,f4]) ).
fof(f30,plain,
! [X2,X3,X0,X1] : meet(X2,join(X0,meet(X2,meet(X3,X1)))) = meet(X2,join(X0,meet(X3,join(meet(X0,X1),meet(X2,X1))))),
inference(superposition,[],[f12,f6]) ).
fof(f33,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,meet(X0,meet(X3,X1)))) = meet(X0,join(X2,meet(join(meet(X0,X1),meet(X2,X1)),X3))),
inference(superposition,[],[f12,f5]) ).
fof(f34,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,join(X0,meet(X1,meet(X0,X2)))),
inference(superposition,[],[f12,f4]) ).
fof(f39,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,meet(X2,X1)))) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f28,f17]) ).
fof(f43,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f17,f3]) ).
fof(f47,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f43,f6]) ).
fof(f50,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f59,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f81,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f15,f4]) ).
fof(f86,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f15]) ).
fof(f95,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f81,f5]) ).
fof(f100,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f8,f4]) ).
fof(f110,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f123,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f50,f5]) ).
fof(f155,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f100,f6]) ).
fof(f157,plain,
! [X2,X0,X1] : join(X0,meet(X0,X1)) = join(X0,meet(X2,meet(X0,X1))),
inference(superposition,[],[f100,f17]) ).
fof(f170,plain,
! [X2,X0,X1] : join(X0,meet(X2,meet(X0,X1))) = X0,
inference(forward_demodulation,[],[f157,f4]) ).
fof(f218,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f220,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f221,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f223,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f227,plain,
! [X0] : complement(X0) = join(complement(X0),zero),
inference(superposition,[],[f17,f10]) ).
fof(f230,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f232,plain,
! [X0] : complement(X0) = join(zero,complement(X0)),
inference(forward_demodulation,[],[f227,f6]) ).
fof(f239,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f220]) ).
fof(f242,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,meet(X2,one)))) = meet(X1,join(X0,meet(X2,join(meet(X1,one),X0)))),
inference(superposition,[],[f12,f220]) ).
fof(f243,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f17,f220]) ).
fof(f249,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,meet(X2,one)))) = meet(X1,join(X0,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f242,f220]) ).
fof(f251,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X2,join(X1,X0)))) = meet(X1,join(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f249,f220]) ).
fof(f289,plain,
zero = complement(one),
inference(superposition,[],[f10,f239]) ).
fof(f307,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,meet(X2,join(X0,X1)))),
inference(superposition,[],[f251,f6]) ).
fof(f308,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f251,f4]) ).
fof(f311,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),meet(X1,one))),
inference(superposition,[],[f251,f9]) ).
fof(f320,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f251,f5]) ).
fof(f354,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f311,f220]) ).
fof(f371,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(superposition,[],[f354,f5]) ).
fof(f446,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(X1,one))),
inference(superposition,[],[f307,f9]) ).
fof(f502,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f446,f220]) ).
fof(f748,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f223]) ).
fof(f751,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f15,f223]) ).
fof(f773,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f5,f751]) ).
fof(f778,plain,
! [X2,X0,X1] : meet(X0,join(zero,meet(X0,meet(X1,X2)))) = meet(X0,join(zero,meet(X1,join(zero,meet(X0,X2))))),
inference(superposition,[],[f30,f751]) ).
fof(f803,plain,
! [X2,X0,X1] : meet(X0,join(zero,meet(X0,meet(X1,X2)))) = meet(X0,meet(X1,join(zero,meet(X0,X2)))),
inference(forward_demodulation,[],[f778,f748]) ).
fof(f809,plain,
! [X2,X0,X1] : meet(X0,join(zero,meet(X0,meet(X1,X2)))) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f803,f748]) ).
fof(f811,plain,
! [X2,X0,X1] : meet(X0,meet(X1,meet(X0,X2))) = meet(X0,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f809,f748]) ).
fof(f813,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f811,f95]) ).
fof(f840,plain,
one = complement(zero),
inference(superposition,[],[f9,f748]) ).
fof(f908,plain,
! [X2,X0,X1] : meet(X2,join(zero,meet(X2,meet(X0,X1)))) = meet(X2,meet(X0,join(meet(X1,X2),meet(zero,X1)))),
inference(superposition,[],[f21,f748]) ).
fof(f946,plain,
! [X2,X0,X1] : meet(X2,join(zero,meet(X2,meet(X0,X1)))) = meet(X2,meet(X0,join(meet(X1,X2),zero))),
inference(forward_demodulation,[],[f908,f751]) ).
fof(f986,plain,
! [X2,X0,X1] : meet(X2,join(zero,meet(X2,meet(X0,X1)))) = meet(X2,meet(X0,join(zero,meet(X1,X2)))),
inference(forward_demodulation,[],[f946,f6]) ).
fof(f1016,plain,
! [X2,X0,X1] : meet(X2,join(zero,meet(X2,meet(X0,X1)))) = meet(X2,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f986,f748]) ).
fof(f1025,plain,
! [X2,X0,X1] : meet(X2,meet(X2,meet(X0,X1))) = meet(X2,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f1016,f748]) ).
fof(f1029,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f1025,f95]) ).
fof(f1080,plain,
! [X2,X0,X1] : meet(X1,join(join(X0,meet(X1,X2)),meet(X1,meet(X0,X2)))) = meet(X1,join(join(X0,meet(X1,X2)),meet(X0,join(meet(X1,X2),meet(X0,X2))))),
inference(superposition,[],[f25,f251]) ).
fof(f1141,plain,
! [X2,X0,X1] : meet(X1,join(join(X0,meet(X1,X2)),meet(X1,meet(X0,X2)))) = meet(X1,join(X0,join(meet(X1,X2),meet(X0,join(meet(X1,X2),meet(X0,X2)))))),
inference(forward_demodulation,[],[f1080,f8]) ).
fof(f1183,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(join(X0,meet(X1,X2)),meet(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f1141,f155]) ).
fof(f1217,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(meet(X1,meet(X0,X2)),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f1183,f6]) ).
fof(f1229,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(meet(X1,X2),join(meet(X1,meet(X0,X2)),X0))),
inference(forward_demodulation,[],[f1217,f110]) ).
fof(f1236,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(meet(X1,X2),join(X0,meet(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f1229,f6]) ).
fof(f1238,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(meet(X1,X2),X0)),
inference(forward_demodulation,[],[f1236,f170]) ).
fof(f1302,plain,
! [X2,X3,X0,X1] : meet(meet(X0,join(X1,meet(X0,X2))),X3) = meet(X0,meet(join(meet(X0,X2),X1),X3)),
inference(superposition,[],[f7,f1238]) ).
fof(f1328,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X1,meet(X0,X2)),X3)) = meet(X0,meet(join(meet(X0,X2),X1),X3)),
inference(forward_demodulation,[],[f1302,f7]) ).
fof(f1720,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X1,X0))),
inference(superposition,[],[f86,f10]) ).
fof(f1770,plain,
! [X0,X1] : zero = meet(X0,complement(join(X1,X0))),
inference(forward_demodulation,[],[f1720,f773]) ).
fof(f1893,plain,
! [X2,X0,X1] : meet(X0,join(zero,meet(X0,meet(X2,X1)))) = meet(X0,meet(join(meet(X0,X1),meet(zero,X1)),X2)),
inference(superposition,[],[f33,f748]) ).
fof(f1940,plain,
! [X2,X0,X1] : meet(one,join(X0,meet(one,meet(X1,X2)))) = join(X0,meet(join(meet(one,X2),meet(X0,X2)),X1)),
inference(superposition,[],[f239,f33]) ).
fof(f1942,plain,
! [X2,X0,X1] : meet(one,join(X0,meet(one,meet(X1,X2)))) = join(X0,meet(join(X2,meet(X0,X2)),X1)),
inference(forward_demodulation,[],[f1940,f239]) ).
fof(f1967,plain,
! [X2,X0,X1] : meet(X0,join(zero,meet(X0,meet(X2,X1)))) = meet(X0,meet(join(meet(X0,X1),zero),X2)),
inference(forward_demodulation,[],[f1893,f751]) ).
fof(f2012,plain,
! [X2,X0,X1] : meet(one,join(X0,meet(one,meet(X1,X2)))) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f1942,f17]) ).
fof(f2026,plain,
! [X2,X0,X1] : meet(X0,join(zero,meet(X0,meet(X2,X1)))) = meet(X0,meet(join(zero,meet(X0,X1)),X2)),
inference(forward_demodulation,[],[f1967,f1328]) ).
fof(f2053,plain,
! [X2,X0,X1] : join(X0,meet(one,meet(X1,X2))) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f2012,f239]) ).
fof(f2063,plain,
! [X2,X0,X1] : meet(X0,meet(meet(X0,X1),X2)) = meet(X0,join(zero,meet(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f2026,f748]) ).
fof(f2083,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f2053,f239]) ).
fof(f2087,plain,
! [X2,X0,X1] : meet(X0,meet(meet(X0,X1),X2)) = meet(X0,meet(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f2063,f748]) ).
fof(f2092,plain,
! [X2,X0,X1] : meet(X0,meet(X2,X1)) = meet(X0,meet(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f2087,f95]) ).
fof(f2094,plain,
! [X2,X0,X1] : meet(X0,meet(X2,X1)) = meet(X0,meet(X0,meet(X1,X2))),
inference(forward_demodulation,[],[f2092,f7]) ).
fof(f2096,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f2094,f95]) ).
fof(f2173,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f6,f2083]) ).
fof(f2299,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f5,f2096]) ).
fof(f2316,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),meet(X2,X1))) = meet(X0,join(complement(X0),meet(X0,meet(X1,X2)))),
inference(superposition,[],[f354,f2096]) ).
fof(f2337,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),meet(X1,X2))) = meet(X0,join(complement(X0),meet(X2,X1))),
inference(forward_demodulation,[],[f2316,f354]) ).
fof(f2551,plain,
! [X2,X3,X0,X1] : meet(X1,join(join(X3,X0),meet(X1,X2))) = meet(X1,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f1238,f110]) ).
fof(f2580,plain,
! [X2,X3,X0,X1] : meet(X1,join(X0,join(meet(X1,X2),X3))) = meet(X1,join(X3,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f2551,f8]) ).
fof(f2716,plain,
! [X0,X1] : meet(X0,join(complement(X0),zero)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(superposition,[],[f354,f230]) ).
fof(f2733,plain,
! [X0,X1] : meet(X0,join(zero,complement(X0))) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2716,f6]) ).
fof(f2784,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2733,f232]) ).
fof(f2805,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2784,f10]) ).
fof(f3083,plain,
! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X1,X0),meet(X3,X2)),
inference(superposition,[],[f2173,f2173]) ).
fof(f3354,plain,
! [X0,X1] : one = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f221,f6]) ).
fof(f3691,plain,
! [X0,X1] : meet(X0,zero) = meet(meet(complement(X1),X1),X0),
inference(superposition,[],[f2299,f10]) ).
fof(f3941,plain,
! [X0,X1] : meet(X0,zero) = meet(complement(X1),meet(X1,X0)),
inference(forward_demodulation,[],[f3691,f7]) ).
fof(f4038,plain,
! [X0,X1] : meet(X0,zero) = meet(X1,meet(X0,complement(X1))),
inference(forward_demodulation,[],[f3941,f59]) ).
fof(f4086,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(X1))),
inference(forward_demodulation,[],[f4038,f773]) ).
fof(f4898,plain,
! [X0,X1] :
( one != join(one,X0)
| zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(superposition,[],[f11,f218]) ).
fof(f4907,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,X2))) = meet(X1,join(join(complement(X1),X0),meet(join(one,X0),X2))),
inference(superposition,[],[f320,f218]) ).
fof(f4918,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,X2))) = meet(X1,join(complement(X1),join(X0,meet(join(one,X0),X2)))),
inference(forward_demodulation,[],[f4907,f8]) ).
fof(f4927,plain,
! [X0,X1] :
( zero != meet(X1,join(complement(X1),X0))
| complement(X1) = join(complement(X1),X0) ),
inference(forward_subsumption_resolution,[],[f4898,f243]) ).
fof(f4953,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,X2))) = meet(X1,join(complement(X1),join(X0,meet(one,X2)))),
inference(forward_demodulation,[],[f4918,f243]) ).
fof(f4963,plain,
! [X2,X0,X1] : meet(X1,join(join(complement(X1),X0),meet(X1,X2))) = meet(X1,join(complement(X1),join(X0,X2))),
inference(forward_demodulation,[],[f4953,f239]) ).
fof(f4970,plain,
! [X2,X0,X1] : meet(X1,join(complement(X1),join(X0,X2))) = meet(X1,join(complement(X1),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f4963,f8]) ).
fof(f5177,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(X0,meet(X1,complement(X0)))),
inference(superposition,[],[f502,f2083]) ).
fof(f5640,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),meet(complement(join(X1,X0)),complement(zero)))),
inference(superposition,[],[f2805,f1770]) ).
fof(f5646,plain,
! [X0,X1] : meet(complement(X0),join(X0,zero)) = meet(complement(X0),join(X0,complement(join(X1,complement(X0))))),
inference(superposition,[],[f502,f1770]) ).
fof(f5651,plain,
! [X0,X1] : meet(complement(X0),X0) = meet(complement(X0),join(X0,complement(join(X1,complement(X0))))),
inference(forward_demodulation,[],[f5646,f223]) ).
fof(f5656,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),meet(complement(zero),complement(join(X1,X0))))),
inference(forward_demodulation,[],[f5640,f2337]) ).
fof(f5694,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(complement(X0),join(X0,complement(join(X1,complement(X0))))),
inference(forward_demodulation,[],[f5651,f5]) ).
fof(f5697,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),meet(one,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f5656,f840]) ).
fof(f5722,plain,
! [X0,X1] : zero = meet(complement(X0),join(X0,complement(join(X1,complement(X0))))),
inference(forward_demodulation,[],[f5694,f10]) ).
fof(f5723,plain,
! [X0,X1] : zero = meet(X0,join(complement(X0),complement(join(X1,X0)))),
inference(forward_demodulation,[],[f5697,f239]) ).
fof(f6389,plain,
! [X2,X0,X1] : meet(X2,join(complement(X2),meet(X1,X0))) = meet(X2,join(meet(X0,X1),complement(X2))),
inference(superposition,[],[f2337,f6]) ).
fof(f7785,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(join(X0,complement(X0)))),
inference(unit_resulting_resolution,[],[f11,f5722,f3354]) ).
fof(f7898,plain,
! [X0] : complement(complement(X0)) = join(X0,complement(one)),
inference(forward_demodulation,[],[f7785,f9]) ).
fof(f7924,plain,
! [X0] : join(X0,zero) = complement(complement(X0)),
inference(forward_demodulation,[],[f7898,f289]) ).
fof(f7939,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f7924,f223]) ).
fof(f8468,plain,
! [X2,X3,X0,X1] : join(X2,X3) = join(X2,join(X3,meet(X0,meet(X1,X2)))),
inference(superposition,[],[f155,f59]) ).
fof(f9607,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))) ),
inference(superposition,[],[f4927,f2805]) ).
fof(f9611,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(complement(X0),complement(join(X1,X0))) ),
inference(superposition,[],[f4927,f5723]) ).
fof(f9627,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(trivial_inequality_removal,[],[f9611]) ).
fof(f9629,plain,
! [X0,X1] : complement(X0) = join(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(trivial_inequality_removal,[],[f9607]) ).
fof(f9669,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f9627,f4]) ).
fof(f9670,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f9627,f17]) ).
fof(f9702,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f15,f9627]) ).
fof(f9729,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f9702,f5]) ).
fof(f9746,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f9670,f6]) ).
fof(f9747,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f9669,f6]) ).
fof(f10020,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(X0),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f123,f9747]) ).
fof(f10576,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(X0,complement(meet(X1,complement(X0)))),
inference(superposition,[],[f9746,f7939]) ).
fof(f10837,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(meet(X1,complement(meet(X0,X1))),complement(X0)),
inference(superposition,[],[f15,f9629]) ).
fof(f10869,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f10837,f5]) ).
fof(f10916,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f10869,f10020]) ).
fof(f10966,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(superposition,[],[f10916,f5]) ).
fof(f11056,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X0,X1)))) = meet(X1,join(complement(X1),meet(complement(X0),X1))),
inference(superposition,[],[f354,f10916]) ).
fof(f11082,plain,
! [X0,X1] : meet(complement(X1),join(X1,complement(meet(X0,complement(X1))))) = meet(complement(X1),join(X1,meet(complement(X0),complement(X1)))),
inference(superposition,[],[f502,f10916]) ).
fof(f11088,plain,
! [X0,X1] : meet(complement(X1),join(X1,complement(meet(X0,complement(X1))))) = meet(complement(X1),join(X1,complement(X0))),
inference(forward_demodulation,[],[f11082,f5177]) ).
fof(f11105,plain,
! [X0,X1] : meet(X1,join(complement(X1),complement(meet(X0,X1)))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f11056,f371]) ).
fof(f11159,plain,
! [X0,X1] : meet(complement(X1),complement(meet(X0,complement(X1)))) = meet(complement(X1),join(X1,complement(X0))),
inference(forward_demodulation,[],[f11088,f10576]) ).
fof(f11170,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f11105,f9746]) ).
fof(f11204,plain,
! [X0,X1] : meet(complement(X0),complement(X1)) = meet(complement(X1),join(X1,complement(X0))),
inference(forward_demodulation,[],[f11159,f10916]) ).
fof(f11210,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(X1,join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f11170,f10916]) ).
fof(f11254,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),X0)),
inference(superposition,[],[f11210,f7939]) ).
fof(f11453,plain,
! [X2,X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(complement(join(X1,meet(X0,meet(X1,X2)))),X0),
inference(superposition,[],[f10966,f34]) ).
fof(f11627,plain,
! [X2,X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,complement(join(X1,meet(X0,meet(X1,X2))))),
inference(forward_demodulation,[],[f11453,f5]) ).
fof(f11694,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f11627,f170]) ).
fof(f12159,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(superposition,[],[f11254,f7939]) ).
fof(f12167,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(X0,complement(X1))),
inference(superposition,[],[f11254,f6]) ).
fof(f12179,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(X1,join(X0,join(complement(X1),X2))),
inference(superposition,[],[f11254,f110]) ).
fof(f12259,plain,
! [X0,X1] : meet(join(complement(X1),X0),join(complement(join(complement(X1),X0)),X1)) = meet(join(complement(X1),X0),join(complement(join(complement(X1),X0)),meet(X0,X1))),
inference(superposition,[],[f371,f11254]) ).
fof(f12260,plain,
! [X2,X0,X1] : meet(X1,meet(X2,meet(X0,X1))) = meet(X1,meet(X2,join(complement(X1),X0))),
inference(superposition,[],[f813,f11254]) ).
fof(f12280,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(X1,complement(join(complement(X1),X0))),
inference(superposition,[],[f11694,f11254]) ).
fof(f12297,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(X1,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f12280,f10916]) ).
fof(f12311,plain,
! [X2,X0,X1] : meet(X1,meet(X2,X0)) = meet(X1,meet(X2,join(complement(X1),X0))),
inference(forward_demodulation,[],[f12260,f1029]) ).
fof(f12312,plain,
! [X0,X1] : meet(join(complement(X1),X0),join(complement(join(complement(X1),X0)),X1)) = meet(join(complement(X1),X0),join(meet(X1,X0),complement(join(complement(X1),X0)))),
inference(forward_demodulation,[],[f12259,f6389]) ).
fof(f12397,plain,
! [X0,X1] : meet(join(complement(X1),X0),join(complement(join(complement(X1),X0)),X1)) = meet(meet(X1,X0),join(complement(X1),X0)),
inference(forward_demodulation,[],[f12312,f12167]) ).
fof(f12461,plain,
! [X0,X1] : meet(join(complement(X1),X0),join(complement(join(complement(X1),X0)),X1)) = meet(X1,meet(X0,join(complement(X1),X0))),
inference(forward_demodulation,[],[f12397,f7]) ).
fof(f12491,plain,
! [X0,X1] : meet(X1,meet(X0,X0)) = meet(join(complement(X1),X0),join(complement(join(complement(X1),X0)),X1)),
inference(forward_demodulation,[],[f12461,f12311]) ).
fof(f12512,plain,
! [X0,X1] : meet(X1,join(complement(X1),X0)) = meet(X1,meet(X0,X0)),
inference(forward_demodulation,[],[f12491,f11254]) ).
fof(f12518,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(complement(X1),X0)),
inference(forward_demodulation,[],[f12512,f1]) ).
fof(f12521,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(superposition,[],[f12518,f7939]) ).
fof(f12647,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,join(complement(complement(X0)),X1))),
inference(superposition,[],[f502,f12518]) ).
fof(f12653,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(join(X1,X0),complement(X0)),
inference(forward_demodulation,[],[f12647,f12179]) ).
fof(f12746,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f12653,f5]) ).
fof(f12793,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = meet(meet(complement(X0),X1),complement(X0)),
inference(forward_demodulation,[],[f12746,f12159]) ).
fof(f12821,plain,
! [X0,X1] : meet(complement(X0),join(X1,X0)) = meet(complement(X0),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f12793,f5]) ).
fof(f12831,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f12821,f95]) ).
fof(f12846,plain,
! [X0,X1] : meet(complement(join(complement(X1),X0)),X1) = meet(complement(join(complement(X1),X0)),join(one,X0)),
inference(superposition,[],[f12831,f218]) ).
fof(f12918,plain,
! [X0,X1] : meet(complement(X0),join(complement(complement(X0)),meet(complement(X0),X1))) = meet(complement(X0),join(complement(complement(X0)),join(X1,X0))),
inference(superposition,[],[f354,f12831]) ).
fof(f12938,plain,
! [X0,X1] : meet(complement(complement(X0)),join(X1,X0)) = meet(join(X1,X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f10916,f12831]) ).
fof(f12940,plain,
! [X0,X1] : meet(complement(X0),complement(join(X1,X0))) = meet(complement(X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f11694,f12831]) ).
fof(f12941,plain,
! [X0,X1] : meet(complement(X0),complement(join(X1,X0))) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f12940,f10966]) ).
fof(f12943,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = meet(join(X1,X0),complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f12938,f7939]) ).
fof(f12956,plain,
! [X0,X1] : meet(join(X1,X0),complement(X0)) = meet(complement(X0),join(complement(complement(X0)),meet(complement(X0),X1))),
inference(forward_demodulation,[],[f12918,f11254]) ).
fof(f13005,plain,
! [X0,X1] : meet(complement(join(complement(X1),X0)),X1) = meet(join(one,X0),complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f12846,f5]) ).
fof(f13007,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f12941,f9729]) ).
fof(f13009,plain,
! [X0,X1] : meet(join(X1,X0),complement(meet(complement(X0),X1))) = X0,
inference(forward_demodulation,[],[f12943,f15]) ).
fof(f13020,plain,
! [X0,X1] : meet(join(X1,X0),complement(X0)) = meet(complement(X0),join(complement(complement(X0)),X1)),
inference(forward_demodulation,[],[f12956,f354]) ).
fof(f13046,plain,
! [X0,X1] : meet(complement(join(complement(X1),X0)),X1) = meet(one,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f13005,f243]) ).
fof(f13053,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(join(X1,X0),complement(X0)),
inference(forward_demodulation,[],[f13020,f11254]) ).
fof(f13071,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = meet(complement(join(complement(X1),X0)),X1),
inference(forward_demodulation,[],[f13046,f239]) ).
fof(f13077,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X1,X0)),
inference(forward_demodulation,[],[f13053,f5]) ).
fof(f13087,plain,
! [X0,X1] : complement(join(complement(X1),X0)) = meet(X1,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f13071,f5]) ).
fof(f13097,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(complement(X1),X0)),
inference(forward_demodulation,[],[f13087,f12297]) ).
fof(f13220,plain,
! [X0,X1] : meet(complement(complement(X1)),join(X0,X1)) = meet(join(X0,X1),complement(meet(X0,complement(X1)))),
inference(superposition,[],[f10916,f13077]) ).
fof(f13225,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = meet(join(X0,X1),complement(meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f13220,f7939]) ).
fof(f13300,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,complement(X1)))) = X1,
inference(forward_demodulation,[],[f13225,f15]) ).
fof(f13462,plain,
! [X2,X0,X1] : join(complement(X0),X2) = join(complement(X0),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f155,f13007]) ).
fof(f13465,plain,
! [X0,X1] : meet(complement(X0),join(complement(complement(X0)),complement(X1))) = meet(complement(X0),join(complement(complement(X0)),complement(join(X0,X1)))),
inference(superposition,[],[f354,f13007]) ).
fof(f13525,plain,
! [X0,X1] : meet(complement(join(X0,X1)),complement(X0)) = meet(complement(X0),join(complement(complement(X0)),complement(X1))),
inference(forward_demodulation,[],[f13465,f11210]) ).
fof(f13574,plain,
! [X0,X1] : meet(complement(join(X0,X1)),complement(X0)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f13525,f11210]) ).
fof(f13602,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X0,X1)),complement(X0)),
inference(forward_demodulation,[],[f13574,f13007]) ).
fof(f13619,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f13602,f5]) ).
fof(f13628,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,join(X0,X1))),
inference(forward_demodulation,[],[f13619,f13007]) ).
fof(f13634,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f13628,f47]) ).
fof(f13696,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f7939,f13097]) ).
fof(f13986,plain,
! [X2,X0,X1] : meet(complement(X2),join(X1,X0)) = complement(join(complement(join(X0,X1)),X2)),
inference(superposition,[],[f13097,f13634]) ).
fof(f13987,plain,
! [X2,X0,X1] : meet(complement(X2),join(X0,X1)) = meet(complement(X2),join(X1,X0)),
inference(forward_demodulation,[],[f13986,f13097]) ).
fof(f14375,plain,
! [X0,X1] : meet(join(X1,complement(X0)),complement(meet(complement(X0),complement(X1)))) = meet(complement(complement(X1)),join(X1,complement(X0))),
inference(superposition,[],[f10916,f11204]) ).
fof(f14380,plain,
! [X0,X1] : meet(join(X1,complement(X0)),complement(meet(complement(X0),complement(X1)))) = meet(X1,join(X1,complement(X0))),
inference(forward_demodulation,[],[f14375,f7939]) ).
fof(f14440,plain,
! [X0,X1] : meet(join(X1,complement(X0)),complement(meet(complement(X0),complement(X1)))) = X1,
inference(forward_demodulation,[],[f14380,f3]) ).
fof(f14484,plain,
! [X0,X1] : meet(join(X1,complement(X0)),join(complement(complement(X1)),X0)) = X1,
inference(forward_demodulation,[],[f14440,f13696]) ).
fof(f14508,plain,
! [X0,X1] : meet(join(X1,complement(X0)),join(X1,X0)) = X1,
inference(forward_demodulation,[],[f14484,f7939]) ).
fof(f14523,plain,
! [X0,X1] : meet(join(X1,X0),join(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f14508,f5]) ).
fof(f14581,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X2,X1)),
inference(superposition,[],[f13987,f7939]) ).
fof(f14742,plain,
! [X2,X0,X1] : meet(complement(X0),join(complement(complement(X0)),join(X2,X1))) = meet(complement(X0),join(complement(complement(X0)),meet(complement(X0),join(X1,X2)))),
inference(superposition,[],[f354,f13987]) ).
fof(f14792,plain,
! [X2,X0,X1] : meet(complement(X0),join(complement(complement(X0)),join(X2,X1))) = meet(complement(X0),join(complement(complement(X0)),join(X1,X2))),
inference(forward_demodulation,[],[f14742,f354]) ).
fof(f14850,plain,
! [X2,X0,X1] : meet(join(X1,X2),complement(X0)) = meet(complement(X0),join(complement(complement(X0)),join(X2,X1))),
inference(forward_demodulation,[],[f14792,f11254]) ).
fof(f14885,plain,
! [X2,X0,X1] : meet(join(X1,X2),complement(X0)) = meet(join(X2,X1),complement(X0)),
inference(forward_demodulation,[],[f14850,f11254]) ).
fof(f14927,plain,
! [X0,X1] : meet(join(X0,X1),join(X1,complement(X0))) = X1,
inference(superposition,[],[f14523,f6]) ).
fof(f15210,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),complement(meet(complement(join(X1,meet(X0,X2))),X0))),
inference(superposition,[],[f13009,f155]) ).
fof(f15211,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = meet(one,complement(meet(complement(join(X1,complement(join(X0,X1)))),X0))),
inference(superposition,[],[f13009,f221]) ).
fof(f15478,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = complement(meet(complement(join(X1,complement(join(X0,X1)))),X0)),
inference(forward_demodulation,[],[f15211,f239]) ).
fof(f15479,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(complement(X0),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f15210,f13696]) ).
fof(f15598,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),join(X1,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f15478,f13696]) ).
fof(f15684,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),X1),
inference(forward_demodulation,[],[f15598,f13462]) ).
fof(f15896,plain,
! [X0,X1] : join(X0,meet(complement(X0),X1)) = join(complement(complement(X1)),X0),
inference(superposition,[],[f15684,f13097]) ).
fof(f15986,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f15896,f7939]) ).
fof(f16379,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(X1,complement(X0)),
inference(superposition,[],[f15986,f7939]) ).
fof(f16380,plain,
! [X2,X0,X1] : join(join(complement(X1),X0),meet(meet(complement(X0),X1),X2)) = join(X2,join(complement(X1),X0)),
inference(superposition,[],[f15986,f13097]) ).
fof(f16421,plain,
! [X2,X0,X1] : join(X0,meet(complement(X0),X1)) = join(join(X1,meet(complement(X0),meet(X1,X2))),X0),
inference(superposition,[],[f15986,f34]) ).
fof(f16603,plain,
! [X2,X0,X1] : join(X0,meet(complement(X0),X1)) = join(X0,join(X1,meet(complement(X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f16421,f6]) ).
fof(f16634,plain,
! [X2,X0,X1] : join(X2,join(complement(X1),X0)) = join(complement(X1),join(X0,meet(meet(complement(X0),X1),X2))),
inference(forward_demodulation,[],[f16380,f8]) ).
fof(f16701,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(forward_demodulation,[],[f16603,f170]) ).
fof(f16727,plain,
! [X2,X0,X1] : join(X2,join(complement(X1),X0)) = join(complement(X1),join(X0,meet(complement(X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f16634,f7]) ).
fof(f16798,plain,
! [X2,X0,X1] : join(X2,join(complement(X1),X0)) = join(complement(X1),join(meet(X1,X2),X0)),
inference(forward_demodulation,[],[f16727,f15986]) ).
fof(f16847,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X0,X1)),
inference(superposition,[],[f16701,f7939]) ).
fof(f17260,plain,
! [X2,X0,X1] : join(complement(X1),meet(X2,X0)) = join(complement(X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f16847,f59]) ).
fof(f17275,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,join(X1,meet(X0,X2)))) = join(complement(X0),join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f16847,f320]) ).
fof(f17279,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,meet(X0,X1))) = join(complement(X0),join(meet(X0,X1),meet(X0,meet(X2,X1)))),
inference(superposition,[],[f16847,f39]) ).
fof(f17334,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X1,X0)),
inference(superposition,[],[f2083,f16847]) ).
fof(f17449,plain,
! [X2,X0,X1] : join(complement(X0),meet(X0,meet(X0,X1))) = join(X1,join(complement(X0),meet(X0,meet(X2,X1)))),
inference(forward_demodulation,[],[f17279,f16798]) ).
fof(f17453,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,meet(join(X0,X1),X2))) = join(join(X1,meet(X0,X2)),complement(X0)),
inference(forward_demodulation,[],[f17275,f16379]) ).
fof(f17524,plain,
! [X0,X1] : join(complement(X0),meet(X0,meet(X0,X1))) = join(X1,complement(X0)),
inference(forward_demodulation,[],[f17449,f8468]) ).
fof(f17528,plain,
! [X2,X0,X1] : join(complement(X0),join(X1,meet(X0,X2))) = join(complement(X0),join(X1,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f17453,f6]) ).
fof(f17569,plain,
! [X0,X1] : join(complement(X0),meet(X1,X0)) = join(X1,complement(X0)),
inference(forward_demodulation,[],[f17524,f17260]) ).
fof(f17898,plain,
! [X0,X1] : join(complement(complement(meet(X0,X1))),meet(complement(X0),X1)) = join(X1,complement(complement(meet(X0,X1)))),
inference(superposition,[],[f17569,f10916]) ).
fof(f18037,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = join(meet(X0,X1),meet(complement(X0),X1)),
inference(forward_demodulation,[],[f17898,f7939]) ).
fof(f18116,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X0),X1)) = X1,
inference(forward_demodulation,[],[f18037,f17]) ).
fof(f19686,plain,
! [X2,X0,X1] : meet(complement(X2),join(X1,X0)) = meet(join(X0,X1),complement(meet(join(X1,X0),X2))),
inference(superposition,[],[f10966,f14885]) ).
fof(f19750,plain,
! [X2,X0,X1] : meet(join(X1,X0),complement(meet(join(X0,X1),complement(X2)))) = meet(join(X1,X0),complement(complement(X2))),
inference(superposition,[],[f11694,f14885]) ).
fof(f19758,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = meet(join(X1,X0),complement(meet(join(X0,X1),complement(X2)))),
inference(forward_demodulation,[],[f19750,f7939]) ).
fof(f19848,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = meet(complement(complement(X2)),join(X0,X1)),
inference(forward_demodulation,[],[f19758,f19686]) ).
fof(f19906,plain,
! [X2,X0,X1] : meet(join(X1,X0),X2) = meet(X2,join(X0,X1)),
inference(forward_demodulation,[],[f19848,f7939]) ).
fof(f20228,plain,
! [X2,X0,X1] : join(complement(X2),join(X1,X0)) = join(complement(X2),meet(join(X0,X1),X2)),
inference(superposition,[],[f16847,f19906]) ).
fof(f20255,plain,
! [X2,X0,X1] : join(complement(X2),join(X0,X1)) = join(complement(X2),join(X1,X0)),
inference(forward_demodulation,[],[f20228,f17334]) ).
fof(f28560,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X2,join(X0,X1))),
inference(superposition,[],[f14581,f8]) ).
fof(f28564,plain,
! [X2,X3,X0,X1] : meet(X3,join(complement(X0),join(X1,X2))) = meet(X3,join(join(X2,X1),complement(X0))),
inference(superposition,[],[f14581,f20255]) ).
fof(f28897,plain,
! [X2,X3,X0,X1] : meet(X3,join(complement(X0),join(X1,X2))) = meet(X3,join(X2,join(X1,complement(X0)))),
inference(forward_demodulation,[],[f28564,f8]) ).
fof(f30329,plain,
! [X2,X0,X1] : meet(complement(X0),join(X0,X1)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(superposition,[],[f12521,f100]) ).
fof(f30601,plain,
! [X2,X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f30329,f12159]) ).
fof(f80476,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,join(meet(X0,X1),meet(X2,X0))),meet(complement(X0),join(meet(X0,X1),meet(X0,X2)))),
inference(superposition,[],[f18116,f308]) ).
fof(f80562,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),meet(X0,join(meet(X0,X1),meet(X0,X2))))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,X0)))),
inference(superposition,[],[f354,f308]) ).
fof(f80719,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),meet(X2,X0)),X0) = meet(X0,join(complement(X0),meet(X0,join(meet(X0,X1),meet(X0,X2))))),
inference(forward_demodulation,[],[f80562,f11254]) ).
fof(f80764,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,join(meet(X0,X1),meet(X2,X0))),meet(meet(X0,X2),complement(X0))),
inference(forward_demodulation,[],[f80476,f30601]) ).
fof(f80896,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),meet(X2,X0)),X0) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f80719,f354]) ).
fof(f80925,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(meet(X0,X2),complement(X0)),meet(X0,join(meet(X0,X1),meet(X2,X0)))),
inference(forward_demodulation,[],[f80764,f6]) ).
fof(f81015,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X0,X1),X2))) = meet(join(meet(X0,X1),meet(X2,X0)),X0),
inference(forward_demodulation,[],[f80896,f4970]) ).
fof(f81038,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(complement(X0),meet(X0,X2)),meet(join(meet(X0,X1),meet(X2,X0)),X0)),
inference(forward_demodulation,[],[f80925,f3083]) ).
fof(f81100,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X2,X0))) = meet(X0,join(complement(X0),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f81015,f5]) ).
fof(f81119,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(complement(X0),meet(X0,X2)),meet(X0,join(meet(X0,X1),meet(X2,X0)))),
inference(forward_demodulation,[],[f81038,f2083]) ).
fof(f81168,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X2,X0))) = meet(join(meet(X0,X1),X2),X0),
inference(forward_demodulation,[],[f81100,f11254]) ).
fof(f81185,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,meet(X2,complement(X0))),meet(X0,join(meet(X0,X1),meet(X2,X0)))),
inference(forward_demodulation,[],[f81119,f59]) ).
fof(f81219,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X2,X0))) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f81168,f5]) ).
fof(f81234,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(zero,meet(X0,join(meet(X0,X1),meet(X2,X0)))),
inference(forward_demodulation,[],[f81185,f4086]) ).
fof(f81266,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(forward_demodulation,[],[f81234,f748]) ).
fof(f81284,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f81266,f81219]) ).
fof(f81499,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,join(complement(X0),X1))) = meet(X0,join(meet(X0,X2),join(complement(X0),meet(X0,X1)))),
inference(superposition,[],[f81284,f354]) ).
fof(f81536,plain,
! [X2,X0,X1] : meet(join(X1,X0),join(meet(join(X1,X0),X2),join(X0,complement(X1)))) = join(meet(join(X1,X0),X2),X0),
inference(superposition,[],[f81284,f14927]) ).
fof(f81642,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f6,f81284]) ).
fof(f81851,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(meet(join(X1,X0),X2),join(X0,complement(X1)))),
inference(forward_demodulation,[],[f81536,f6]) ).
fof(f81888,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,join(complement(X0),X1))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f81499,f2580]) ).
fof(f82057,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(complement(X1),join(X0,meet(join(X1,X0),X2)))),
inference(forward_demodulation,[],[f81851,f28897]) ).
fof(f82085,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X0,X1),X2))) = join(meet(X0,X2),meet(X0,join(complement(X0),X1))),
inference(forward_demodulation,[],[f81888,f4970]) ).
fof(f82168,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(complement(X1),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f82057,f17528]) ).
fof(f82193,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X0,X1),X2))) = meet(X0,join(meet(X0,X2),join(complement(X0),X1))),
inference(forward_demodulation,[],[f82085,f81284]) ).
fof(f82246,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(join(X1,X0),X2)),
inference(forward_demodulation,[],[f82168,f15479]) ).
fof(f82263,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X1,meet(X0,X2)))) = meet(X0,join(complement(X0),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f82193,f28560]) ).
fof(f82310,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X1,meet(X0,X2)))) = meet(join(meet(X0,X1),X2),X0),
inference(forward_demodulation,[],[f82263,f11254]) ).
fof(f82344,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(X1,meet(X0,X2)))) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f82310,f5]) ).
fof(f82365,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(join(X1,meet(X0,X2)),X0),
inference(forward_demodulation,[],[f82344,f11254]) ).
fof(f82378,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f82365,f5]) ).
fof(f82468,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(meet(join(X1,X0),X2),complement(meet(X1,complement(X0))))),
inference(superposition,[],[f81642,f13300]) ).
fof(f82974,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(X2,meet(join(X1,X0),complement(meet(X1,complement(X0)))))),
inference(forward_demodulation,[],[f82468,f82378]) ).
fof(f83181,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(X2,X0)),
inference(forward_demodulation,[],[f82974,f13300]) ).
fof(f83331,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X1,X0),join(X2,X0)),
inference(forward_demodulation,[],[f83181,f82246]) ).
fof(f83663,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(join(X2,meet(X1,X0)),X0),
inference(superposition,[],[f83331,f17]) ).
fof(f83774,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f123,f83331]) ).
fof(f84092,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(X0,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f83663,f5]) ).
fof(f84279,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(X0,join(X1,X2)),
inference(forward_demodulation,[],[f84092,f83774]) ).
fof(f84586,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X0)) = meet(X0,join(X1,X2)),
inference(superposition,[],[f84279,f5]) ).
fof(f92648,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f2083,f84586]) ).
fof(f102934,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(superposition,[],[f13,f92648]) ).
fof(f103073,plain,
$false,
inference(trivial_inequality_removal,[],[f102934]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT194-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.15/0.40 % Computer : n017.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Sun Sep 27 14:01:05 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.15/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.46 Running first-order theorem proving
% 0.15/0.46 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.52/3.56 % (2579124)Input is clausal, will run a generic CNF schedule.
% 17.52/3.56 % (2579145)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=736582670:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.52/3.56 % (2579148)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1253155130:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.52/3.56 % (2579144)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=884296401:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.52/3.56 % (2579147)lrs+10_1_sil=8000:sp=occurrence:random_seed=2409419767:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.52/3.56 % (2579149)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1517433614:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.52/3.56 % (2579146)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=617548648:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.52/3.56 % (2579150)dis-21_1_sil=8000:lcm=predicate:random_seed=2800078611:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 17.52/3.56 % (2579150)Refutation not found, incomplete strategy
% 17.52/3.56 % (2579150)------------------------------
% 17.52/3.56 % (2579150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.56 % (2579150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.56 % (2579150)CaDiCaL version: 2.1.3
% 17.52/3.56 % (2579150)Termination reason: Refutation not found, incomplete strategy
% 17.52/3.56 % (2579150)Time elapsed: 0.003 s
% 17.52/3.56 % (2579150)Peak memory usage: 88 MB
% 17.52/3.56 % (2579150)Instructions burned: 1 (million)
% 17.52/3.56 % (2579148)Instruction limit reached!
% 17.52/3.56 % (2579148)------------------------------
% 17.52/3.56 % (2579148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.56 % (2579148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.56 % (2579148)CaDiCaL version: 2.1.3
% 17.52/3.56 % (2579148)Termination reason: Instruction limit
% 17.52/3.56 % (2579148)Termination phase: Saturation
% 17.52/3.56 % (2579148)Time elapsed: 0.077 s
% 17.52/3.56 % (2579148)Peak memory usage: 89 MB
% 17.52/3.56 % (2579148)Instructions burned: 114 (million)
% 17.52/3.56 % (2579147)Instruction limit reached!
% 17.52/3.56 % (2579147)------------------------------
% 17.52/3.56 % (2579147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.56 % (2579147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.56 % (2579147)CaDiCaL version: 2.1.3
% 17.52/3.56 % (2579147)Termination reason: Instruction limit
% 17.52/3.56 % (2579147)Termination phase: Saturation
% 17.52/3.56 % (2579147)Time elapsed: 0.104 s
% 17.52/3.56 % (2579147)Peak memory usage: 89 MB
% 17.52/3.56 % (2579147)Instructions burned: 108 (million)
% 17.52/3.56 % (2579149)Instruction limit reached!
% 17.52/3.56 % (2579149)------------------------------
% 17.52/3.56 % (2579149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.56 % (2579149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.56 % (2579149)CaDiCaL version: 2.1.3
% 17.52/3.56 % (2579149)Termination reason: Instruction limit
% 17.52/3.56 % (2579149)Termination phase: Saturation
% 17.52/3.56 % (2579149)Time elapsed: 0.168 s
% 17.52/3.56 % (2579149)Peak memory usage: 89 MB
% 17.52/3.56 % (2579149)Instructions burned: 180 (million)
% 17.52/3.56 % (2579161)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=808307675:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 17.52/3.56 % (2579161)Refutation not found, incomplete strategy
% 17.52/3.56 % (2579161)------------------------------
% 17.52/3.56 % (2579161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.52/3.56 % (2579161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.52/3.56 % (2579161)CaDiCaL version: 2.1.3
% 17.52/3.56 % (2579161)Termination reason: Refutation not found, incomplete strategy
% 17.52/3.56 % (2579161)Time elapsed: 0.002 s
% 17.52/3.56 % (2579161)Peak memory usage: 88 MB
% 17.52/3.56 % (2579162)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2973354999:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 30.26/5.39 % (2579162)Refutation not found, incomplete strategy
% 30.26/5.39 % (2579162)------------------------------
% 30.26/5.39 % (2579162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579162)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579162)Termination reason: Refutation not found, incomplete strategy
% 30.26/5.39 % (2579162)Time elapsed: 0.002 s
% 30.26/5.39 % (2579162)Peak memory usage: 88 MB
% 30.26/5.39 % (2579162)Instructions burned: 1 (million)
% 30.26/5.39 % (2579150)------------------------------
% 30.26/5.39 % (2579150)------------------------------
% 30.26/5.39 % (2579164)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1092795616:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 30.26/5.39 % (2579164)Refutation not found, incomplete strategy
% 30.26/5.39 % (2579164)------------------------------
% 30.26/5.39 % (2579164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579164)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579164)Termination reason: Refutation not found, incomplete strategy
% 30.26/5.39 % (2579164)Time elapsed: 0.002 s
% 30.26/5.39 % (2579164)Peak memory usage: 87 MB
% 30.26/5.39 % (2579162)------------------------------
% 30.26/5.39 % (2579162)------------------------------
% 30.26/5.39 % (2579161)------------------------------
% 30.26/5.39 % (2579161)------------------------------
% 30.26/5.39 % (2579169)lrs+10_64_to=lpo:sil=8000:random_seed=3533436669:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 30.26/5.39 % (2579169)Instruction limit reached!
% 30.26/5.39 % (2579169)------------------------------
% 30.26/5.39 % (2579169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579169)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579169)Termination reason: Instruction limit
% 30.26/5.39 % (2579169)Termination phase: Saturation
% 30.26/5.39 % (2579169)Time elapsed: 0.122 s
% 30.26/5.39 % (2579169)Peak memory usage: 88 MB
% 30.26/5.39 % (2579169)Instructions burned: 127 (million)
% 30.26/5.39 % (2579171)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2310534054:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 30.26/5.39 % (2579174)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1062802627:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 30.26/5.39 % (2579164)------------------------------
% 30.26/5.39 % (2579164)------------------------------
% 30.26/5.39 % (2579174)Instruction limit reached!
% 30.26/5.39 % (2579174)------------------------------
% 30.26/5.39 % (2579174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579174)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579174)Termination reason: Instruction limit
% 30.26/5.39 % (2579174)Termination phase: Saturation
% 30.26/5.39 % (2579174)Time elapsed: 0.139 s
% 30.26/5.39 % (2579174)Peak memory usage: 90 MB
% 30.26/5.39 % (2579174)Instructions burned: 157 (million)
% 30.26/5.39 % (2579171)Instruction limit reached!
% 30.26/5.39 % (2579171)------------------------------
% 30.26/5.39 % (2579171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579171)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579171)Termination reason: Instruction limit
% 30.26/5.39 % (2579171)Termination phase: Saturation
% 30.26/5.39 % (2579171)Time elapsed: 0.175 s
% 30.26/5.39 % (2579171)Peak memory usage: 90 MB
% 30.26/5.39 % (2579171)Instructions burned: 195 (million)
% 30.26/5.39 % (2579176)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=615573788:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 30.26/5.39 % (2579180)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=2373329691:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 30.26/5.39 % (2579181)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2142804371:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 30.26/5.39 % (2579181)Refutation not found, incomplete strategy
% 30.26/5.39 % (2579181)------------------------------
% 30.26/5.39 % (2579181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579181)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579181)Termination reason: Refutation not found, incomplete strategy
% 30.26/5.39 % (2579181)Time elapsed: 0.001 s
% 30.26/5.39 % (2579181)Peak memory usage: 87 MB
% 30.26/5.39 % (2579182)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4244747475:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 30.26/5.39 % (2579180)Instruction limit reached!
% 30.26/5.39 % (2579180)------------------------------
% 30.26/5.39 % (2579180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579180)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579180)Termination reason: Instruction limit
% 30.26/5.39 % (2579180)Termination phase: Saturation
% 30.26/5.39 % (2579180)Time elapsed: 0.112 s
% 30.26/5.39 % (2579180)Peak memory usage: 89 MB
% 30.26/5.39 % (2579180)Instructions burned: 107 (million)
% 30.26/5.39 % (2579182)Instruction limit reached!
% 30.26/5.39 % (2579182)------------------------------
% 30.26/5.39 % (2579182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579182)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579182)Termination reason: Instruction limit
% 30.26/5.39 % (2579182)Termination phase: Saturation
% 30.26/5.39 % (2579182)Time elapsed: 0.209 s
% 30.26/5.39 % (2579182)Peak memory usage: 90 MB
% 30.26/5.39 % (2579182)Instructions burned: 243 (million)
% 30.26/5.39 % (2579190)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=387968479:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 30.26/5.39 % (2579181)------------------------------
% 30.26/5.39 % (2579181)------------------------------
% 30.26/5.39 % (2579191)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3108499631:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 30.26/5.39 % (2579191)Instruction limit reached!
% 30.26/5.39 % (2579191)------------------------------
% 30.26/5.39 % (2579191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579191)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579191)Termination reason: Instruction limit
% 30.26/5.39 % (2579191)Termination phase: Saturation
% 30.26/5.39 % (2579191)Time elapsed: 0.116 s
% 30.26/5.39 % (2579191)Peak memory usage: 89 MB
% 30.26/5.39 % (2579191)Instructions burned: 134 (million)
% 30.26/5.39 % (2579194)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1571963980:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 30.26/5.39 % (2579196)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3906391471:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi)
% 30.26/5.39 % (2579196)Instruction limit reached!
% 30.26/5.39 % (2579196)------------------------------
% 30.26/5.39 % (2579196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579196)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579196)Termination reason: Instruction limit
% 30.26/5.39 % (2579196)Termination phase: Saturation
% 30.26/5.39 % (2579196)Time elapsed: 0.164 s
% 30.26/5.39 % (2579196)Peak memory usage: 91 MB
% 30.26/5.39 % (2579196)Instructions burned: 191 (million)
% 30.26/5.39 % (2579201)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4101223238:i=264:kws=precedence:fsr=off_2977 on theBenchmark for (2977ds/264Mi)
% 30.26/5.39 % (2579194)Instruction limit reached!
% 30.26/5.39 % (2579194)------------------------------
% 30.26/5.39 % (2579194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579194)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579194)Termination reason: Instruction limit
% 30.26/5.39 % (2579194)Termination phase: Saturation
% 30.26/5.39 % (2579194)Time elapsed: 0.514 s
% 30.26/5.39 % (2579194)Peak memory usage: 93 MB
% 30.26/5.39 % (2579194)Instructions burned: 499 (million)
% 30.26/5.39 % (2579201)Instruction limit reached!
% 30.26/5.39 % (2579201)------------------------------
% 30.26/5.39 % (2579201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579201)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579201)Termination reason: Instruction limit
% 30.26/5.39 % (2579201)Termination phase: Saturation
% 30.26/5.39 % (2579201)Time elapsed: 0.203 s
% 30.26/5.39 % (2579201)Peak memory usage: 92 MB
% 30.26/5.39 % (2579201)Instructions burned: 264 (million)
% 30.26/5.39 % (2579204)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4213755446:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi)
% 30.26/5.39 % (2579204)Instruction limit reached!
% 30.26/5.39 % (2579204)------------------------------
% 30.26/5.39 % (2579204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579204)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579204)Termination reason: Instruction limit
% 30.26/5.39 % (2579204)Termination phase: Saturation
% 30.26/5.39 % (2579204)Time elapsed: 0.157 s
% 30.26/5.39 % (2579204)Peak memory usage: 89 MB
% 30.26/5.39 % (2579204)Instructions burned: 157 (million)
% 30.26/5.39 % (2579205)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=851019026:i=3256:kws=precedence:bd=preordered:av=off_2973 on theBenchmark for (2973ds/3256Mi)
% 30.26/5.39 % (2579209)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1527941503:i=537:av=off:ss=included_2971 on theBenchmark for (2971ds/537Mi)
% 30.26/5.39 % (2579209)Instruction limit reached!
% 30.26/5.39 % (2579209)------------------------------
% 30.26/5.39 % (2579209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579209)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579209)Termination reason: Instruction limit
% 30.26/5.39 % (2579209)Termination phase: Saturation
% 30.26/5.39 % (2579209)Time elapsed: 0.502 s
% 30.26/5.39 % (2579209)Peak memory usage: 93 MB
% 30.26/5.39 % (2579209)Instructions burned: 537 (million)
% 30.26/5.39 % (2579213)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=77136689:i=180:bd=preordered:av=off_2964 on theBenchmark for (2964ds/180Mi)
% 30.26/5.39 % (2579213)Instruction limit reached!
% 30.26/5.39 % (2579213)------------------------------
% 30.26/5.39 % (2579213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.26/5.39 % (2579213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.26/5.39 % (2579213)CaDiCaL version: 2.1.3
% 30.26/5.39 % (2579213)Termination reason: Instruction limit
% 30.26/5.39 % (2579213)Termination phase: Saturation
% 30.26/5.39 % (2579213)Time elapsed: 0.168 s
% 30.26/5.39 % (2579213)Peak memory usage: 88 MB
% 30.26/5.39 % (2579213)Instructions burned: 181 (million)
% 30.26/5.39 % (2579145)First to succeed.
% 30.26/5.39 % (2579145)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2579124"
% 30.26/5.39 % (2579217)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=443824230:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2959 on theBenchmark for (2959ds/10307Mi)
% 30.26/5.39 % (2579145)Refutation found. Thanks to Tanya!
% 30.26/5.39 % SZS status Unsatisfiable for theBenchmark
% 30.26/5.39 % SZS output start Proof for theBenchmark
% See solution above
% 31.18/5.58 % (2579145)------------------------------
% 31.18/5.58 % (2579145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.18/5.58 % (2579145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.18/5.58 % (2579145)CaDiCaL version: 2.1.3
% 31.18/5.58 % (2579145)Termination reason: Refutation
% 31.18/5.58 % (2579145)Time elapsed: 3.948 s
% 31.18/5.58 % (2579145)Peak memory usage: 180 MB
% 31.18/5.58 % (2579145)Instructions burned: 7208 (million)
% 31.18/5.58 % (2579145)------------------------------
% 31.18/5.58 % (2579145)------------------------------
% 31.18/5.58 % (2579124)Success in time 4.291 s
% 31.18/5.58 % Vampire exiting
%------------------------------------------------------------------------------