%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT064-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:45:56 AM UTC 2026
% Result : Unsatisfiable 33.90s 5.68s
% Output : Refutation 34.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 73
% Number of leaves : 18
% Syntax : Number of formulae : 517 ( 489 unt; 5 def)
% Number of atoms : 552 ( 551 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 72 ( 37 ~; 35 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 10 con; 0-2 aty)
% Number of variables : 972 ( 972 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
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)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',top) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bottom) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != n1
| meet(X0,X1) != n0
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complements_are_unique) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,meet(X1,X2))))) = meet(X0,join(X1,meet(X0,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c94_6) ).
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,definition,
sF0 = join(b,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f15,plain,
join(b,c) = sF0,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF1 = meet(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f17,plain,
meet(a,sF0) = sF1,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF2 = meet(a,b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f19,plain,
meet(a,b) = sF2,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF3 = meet(a,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f21,plain,
meet(a,c) = sF3,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF4 = join(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f23,plain,
join(sF2,sF3) = sF4,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
sF1 != sF4,
inference(definition_folding,[],[f13,f23,f21,f19,f17,f15]) ).
fof(f25,plain,
sF2 = meet(b,a),
inference(forward_demodulation,[],[f19,f5]) ).
fof(f26,plain,
sF3 = meet(c,a),
inference(forward_demodulation,[],[f21,f5]) ).
fof(f29,plain,
b = join(b,sF2),
inference(superposition,[],[f4,f25]) ).
fof(f32,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f34,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f36,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f32,f3]) ).
fof(f40,plain,
a = join(a,sF3),
inference(superposition,[],[f32,f26]) ).
fof(f42,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f36,f6]) ).
fof(f43,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f34,f4]) ).
fof(f44,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f34,f32]) ).
fof(f48,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f32,f34]) ).
fof(f50,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f48,f6]) ).
fof(f51,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f44,f5]) ).
fof(f52,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f43,f5]) ).
fof(f58,plain,
! [X0,X1] :
( join(X0,X1) != n1
| meet(X1,X0) != n0
| complement(X1) = X0 ),
inference(superposition,[],[f11,f6]) ).
fof(f75,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f76,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f32]) ).
fof(f78,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f8,f6]) ).
fof(f88,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f89,plain,
! [X2,X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))),
inference(superposition,[],[f3,f8]) ).
fof(f96,plain,
sF3 = meet(sF3,sF4),
inference(superposition,[],[f34,f23]) ).
fof(f97,plain,
sF2 = meet(sF2,sF4),
inference(superposition,[],[f3,f23]) ).
fof(f111,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f112,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f34]) ).
fof(f114,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f116,plain,
! [X0] : meet(a,meet(sF0,X0)) = meet(sF1,X0),
inference(superposition,[],[f7,f17]) ).
fof(f117,plain,
! [X0] : meet(b,meet(a,X0)) = meet(sF2,X0),
inference(superposition,[],[f7,f25]) ).
fof(f118,plain,
! [X0] : meet(c,meet(a,X0)) = meet(sF3,X0),
inference(superposition,[],[f7,f26]) ).
fof(f124,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
inference(superposition,[],[f34,f7]) ).
fof(f125,plain,
! [X2,X0,X1] : join(X2,meet(X0,meet(X1,X2))) = X2,
inference(superposition,[],[f32,f7]) ).
fof(f127,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f128,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f135,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(X2,X0))) = meet(X2,join(X1,meet(X0,join(X2,meet(X0,X1))))),
inference(superposition,[],[f12,f5]) ).
fof(f142,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(X2,X1))) = meet(X2,join(X0,meet(X1,join(meet(X0,X1),X2)))),
inference(superposition,[],[f12,f6]) ).
fof(f164,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(n1,X1),
inference(superposition,[],[f8,f9]) ).
fof(f166,plain,
! [X0] : meet(X0,n1) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f167,plain,
! [X0,X1] : n1 = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f173,plain,
! [X0] : n1 = join(n1,X0),
inference(superposition,[],[f32,f166]) ).
fof(f175,plain,
! [X0] : meet(n1,X0) = X0,
inference(superposition,[],[f5,f166]) ).
fof(f178,plain,
! [X0,X1] : n1 = join(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f164,f173]) ).
fof(f189,plain,
! [X0] : n1 = join(X0,n1),
inference(superposition,[],[f34,f175]) ).
fof(f243,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(n0,X1),
inference(superposition,[],[f7,f10]) ).
fof(f245,plain,
! [X0] : join(X0,n0) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f246,plain,
! [X0,X1] : n0 = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f300,plain,
! [X0] : n0 = meet(n0,X0),
inference(superposition,[],[f34,f245]) ).
fof(f302,plain,
! [X0] : join(n0,X0) = X0,
inference(superposition,[],[f6,f245]) ).
fof(f305,plain,
! [X0,X1] : n0 = meet(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f243,f300]) ).
fof(f385,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f111,f5]) ).
fof(f425,plain,
! [X2,X0,X1] : meet(X1,join(join(X0,X2),meet(X1,X0))) = meet(X1,join(join(X0,X2),meet(X0,join(X1,X0)))),
inference(superposition,[],[f135,f3]) ).
fof(f431,plain,
! [X0,X1] : meet(X0,join(complement(X1),meet(X0,X1))) = meet(X0,join(complement(X1),meet(X1,join(X0,n0)))),
inference(superposition,[],[f135,f10]) ).
fof(f491,plain,
! [X0,X1] : meet(X0,join(complement(X1),meet(X0,X1))) = meet(X0,join(complement(X1),meet(X1,X0))),
inference(forward_demodulation,[],[f431,f245]) ).
fof(f497,plain,
! [X2,X0,X1] : meet(X1,join(join(X0,X2),meet(X1,X0))) = meet(X1,join(X0,join(X2,meet(X0,join(X1,X0))))),
inference(forward_demodulation,[],[f425,f8]) ).
fof(f515,plain,
! [X2,X0,X1] : meet(X1,join(join(X0,X2),meet(X1,X0))) = meet(X1,join(X0,join(X2,X0))),
inference(forward_demodulation,[],[f497,f34]) ).
fof(f524,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(join(X0,X2),meet(X1,X0))),
inference(forward_demodulation,[],[f515,f50]) ).
fof(f527,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f524,f8]) ).
fof(f562,plain,
! [X0,X1] : join(complement(X1),meet(X1,X0)) = join(join(complement(X1),meet(X1,X0)),meet(X0,join(complement(X1),meet(X0,X1)))),
inference(superposition,[],[f32,f491]) ).
fof(f572,plain,
! [X0,X1] : join(complement(X1),meet(X1,X0)) = join(complement(X1),join(meet(X1,X0),meet(X0,join(complement(X1),meet(X0,X1))))),
inference(forward_demodulation,[],[f562,f8]) ).
fof(f640,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),X1))) = meet(complement(meet(X0,X1)),join(X0,meet(X1,n1))),
inference(superposition,[],[f142,f9]) ).
fof(f644,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(meet(X1,X0),X2))),join(X1,meet(meet(X2,join(X0,meet(meet(X1,X0),X2))),X0))) = meet(meet(X2,join(X0,meet(meet(X1,X0),X2))),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2))))),
inference(superposition,[],[f142,f12]) ).
fof(f645,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(X2,meet(X1,X0)))),join(X1,meet(meet(X2,join(X0,meet(X2,meet(X1,X0)))),X0))) = meet(meet(X2,join(X0,meet(X2,meet(X1,X0)))),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2))))),
inference(superposition,[],[f142,f135]) ).
fof(f684,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(X2,meet(X1,X0)))),join(X1,meet(meet(X2,join(X0,meet(X2,meet(X1,X0)))),X0))) = meet(X2,meet(join(X0,meet(X2,meet(X1,X0))),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))),
inference(forward_demodulation,[],[f645,f7]) ).
fof(f685,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(meet(X1,X0),X2))),join(X1,meet(meet(X2,join(X0,meet(meet(X1,X0),X2))),X0))) = meet(X2,meet(join(X0,meet(meet(X1,X0),X2)),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))),
inference(forward_demodulation,[],[f644,f7]) ).
fof(f688,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),X1))) = meet(complement(meet(X0,X1)),join(X0,X1)),
inference(forward_demodulation,[],[f640,f166]) ).
fof(f707,plain,
! [X2,X0,X1] : meet(meet(X2,X0),join(X1,meet(meet(X2,X0),X0))) = meet(X2,meet(X0,join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))),
inference(forward_demodulation,[],[f684,f125]) ).
fof(f708,plain,
! [X2,X0,X1] : meet(meet(X2,join(X0,meet(X1,meet(X0,X2)))),join(X1,meet(meet(X2,join(X0,meet(X1,meet(X0,X2)))),X0))) = meet(X2,meet(join(X0,meet(X1,meet(X0,X2))),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))),
inference(forward_demodulation,[],[f685,f7]) ).
fof(f710,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),join(X0,meet(complement(meet(X0,X1)),X1))) = meet(join(X0,X1),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f688,f5]) ).
fof(f721,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(X0,join(X1,meet(meet(X2,X0),X0)))),
inference(forward_demodulation,[],[f707,f7]) ).
fof(f722,plain,
! [X2,X0,X1] : meet(X2,meet(join(X0,meet(X1,meet(X0,X2))),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(join(X0,meet(X1,meet(X0,X2))),join(X1,meet(meet(X2,join(X0,meet(X1,meet(X0,X2)))),X0)))),
inference(forward_demodulation,[],[f708,f7]) ).
fof(f724,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(X0,X1))) = meet(complement(meet(X0,X1)),join(X0,meet(X1,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f710,f5]) ).
fof(f734,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(X0,join(X1,meet(X0,meet(X2,X0))))),
inference(forward_demodulation,[],[f721,f5]) ).
fof(f735,plain,
! [X2,X0,X1] : meet(X2,meet(join(X0,meet(X1,meet(X0,X2))),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(join(X0,meet(X1,meet(X0,X2))),join(X1,meet(X0,meet(X2,join(X0,meet(X1,meet(X0,X2)))))))),
inference(forward_demodulation,[],[f722,f5]) ).
fof(f741,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(X0,join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f734,f51]) ).
fof(f742,plain,
! [X2,X0,X1] : meet(X2,meet(join(X0,meet(X1,meet(X0,X2))),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(join(X0,meet(X1,meet(X0,X2))),join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f735,f385]) ).
fof(f748,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))),
inference(forward_demodulation,[],[f741,f124]) ).
fof(f749,plain,
! [X2,X0,X1] : meet(X2,meet(join(X0,meet(X1,meet(X0,X2))),join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(join(X1,meet(X0,X2)),join(X0,meet(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f742,f5]) ).
fof(f792,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(join(X0,meet(X1,complement(meet(X0,X1)))),meet(join(X0,X1),complement(meet(X0,X1)))),
inference(superposition,[],[f32,f724]) ).
fof(f796,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(X0,join(meet(X1,complement(meet(X0,X1))),meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f792,f8]) ).
fof(f1039,plain,
! [X2,X0,X1] : join(X0,meet(X0,X1)) = join(X0,meet(X2,meet(X0,X1))),
inference(superposition,[],[f75,f32]) ).
fof(f1041,plain,
! [X0,X1] : join(X0,n1) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f75,f9]) ).
fof(f1063,plain,
! [X0,X1] : n1 = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f1041,f189]) ).
fof(f1065,plain,
! [X2,X0,X1] : join(X0,meet(X2,meet(X0,X1))) = X0,
inference(forward_demodulation,[],[f1039,f4]) ).
fof(f1078,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(join(X1,meet(X0,X2)),X0)),
inference(backward_demodulation,[],[f749,f1065]) ).
fof(f1082,plain,
! [X2,X0,X1] : meet(X2,meet(X0,join(X1,meet(X0,join(meet(X1,X0),meet(X0,X2)))))) = meet(X2,meet(X0,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f1078,f5]) ).
fof(f1083,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,meet(X0,X2)))),
inference(forward_demodulation,[],[f1082,f748]) ).
fof(f1085,plain,
! [X0,X1] : n0 = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f246,f5]) ).
fof(f1209,plain,
! [X0,X1] : meet(complement(X0),X0) = meet(complement(X0),meet(X0,join(X1,n0))),
inference(superposition,[],[f1083,f10]) ).
fof(f1220,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(superposition,[],[f1083,f32]) ).
fof(f1241,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X1,join(X2,meet(X1,X0))),meet(X0,X1)),
inference(superposition,[],[f32,f1083]) ).
fof(f1259,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X0,X1),meet(X1,join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f1241,f6]) ).
fof(f1280,plain,
! [X0,X1] : meet(complement(X0),X0) = meet(X0,meet(join(X1,n0),complement(X0))),
inference(forward_demodulation,[],[f1209,f127]) ).
fof(f1298,plain,
! [X0,X1] : join(complement(X1),meet(X1,X0)) = join(complement(X1),meet(X0,join(complement(X1),meet(X0,X1)))),
inference(backward_demodulation,[],[f572,f1259]) ).
fof(f1314,plain,
! [X0,X1] : meet(complement(X0),X0) = meet(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f1280,f245]) ).
fof(f1337,plain,
! [X0,X1] : meet(X0,complement(X0)) = meet(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f1314,f5]) ).
fof(f1358,plain,
! [X0,X1] : n0 = meet(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f1337,f10]) ).
fof(f1376,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f1220,f111]) ).
fof(f1393,plain,
meet(sF0,a) = meet(sF0,sF1),
inference(superposition,[],[f1220,f17]) ).
fof(f1394,plain,
meet(a,b) = meet(a,sF2),
inference(superposition,[],[f1220,f25]) ).
fof(f1395,plain,
meet(a,c) = meet(a,sF3),
inference(superposition,[],[f1220,f26]) ).
fof(f1402,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(meet(X1,X0),X2)),
inference(superposition,[],[f7,f1220]) ).
fof(f1404,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f32,f1220]) ).
fof(f1425,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f1402,f7]) ).
fof(f1429,plain,
meet(c,a) = meet(a,sF3),
inference(forward_demodulation,[],[f1395,f5]) ).
fof(f1430,plain,
meet(b,a) = meet(a,sF2),
inference(forward_demodulation,[],[f1394,f5]) ).
fof(f1431,plain,
meet(a,sF0) = meet(sF0,sF1),
inference(forward_demodulation,[],[f1393,f5]) ).
fof(f1447,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f1376,f5]) ).
fof(f1456,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f1425,f7]) ).
fof(f1458,plain,
sF3 = meet(a,sF3),
inference(forward_demodulation,[],[f1429,f26]) ).
fof(f1459,plain,
sF2 = meet(a,sF2),
inference(forward_demodulation,[],[f1430,f25]) ).
fof(f1460,plain,
sF1 = meet(sF0,sF1),
inference(forward_demodulation,[],[f1431,f17]) ).
fof(f1474,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(meet(X0,X1),join(X0,X2))),
inference(forward_demodulation,[],[f1447,f127]) ).
fof(f1486,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f1474,f7]) ).
fof(f1494,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,join(X0,X2))),
inference(forward_demodulation,[],[f1486,f1456]) ).
fof(f1498,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(meet(join(X0,X2),X1),X0),
inference(forward_demodulation,[],[f1494,f3]) ).
fof(f1499,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f1498,f5]) ).
fof(f1803,plain,
! [X0,X1] :
( n1 != n1
| n0 != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(superposition,[],[f11,f167]) ).
fof(f1812,plain,
! [X0,X1] :
( n0 != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1803]) ).
fof(f1846,plain,
! [X0] : join(a,X0) = join(a,join(sF2,X0)),
inference(superposition,[],[f75,f1459]) ).
fof(f1879,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f112,f4]) ).
fof(f1891,plain,
! [X0] : meet(c,X0) = meet(c,meet(sF0,X0)),
inference(superposition,[],[f112,f15]) ).
fof(f1894,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f112,f5]) ).
fof(f1928,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(join(X2,X0),X1),meet(X0,X1)),
inference(superposition,[],[f32,f112]) ).
fof(f1952,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = join(meet(X0,X1),meet(join(X2,X0),X1)),
inference(forward_demodulation,[],[f1928,f6]) ).
fof(f1988,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f1879,f127]) ).
fof(f1994,plain,
! [X0,X1] : join(X0,meet(X1,complement(meet(X0,X1)))) = join(X0,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f796,f1952]) ).
fof(f2009,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f1988,f1456]) ).
fof(f2024,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,meet(n1,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f1994,f1063]) ).
fof(f2030,plain,
join(sF2,meet(sF3,complement(meet(sF2,sF3)))) = join(sF2,meet(sF4,complement(meet(sF2,sF3)))),
inference(superposition,[],[f1994,f23]) ).
fof(f2033,plain,
! [X0,X1] : join(X1,meet(X0,complement(meet(X0,X1)))) = join(X1,meet(join(X1,X0),complement(meet(X0,X1)))),
inference(superposition,[],[f1994,f5]) ).
fof(f2034,plain,
! [X2,X0,X1] : join(X0,meet(meet(join(X0,X2),X1),complement(meet(X0,X1)))) = join(X0,meet(join(X0,meet(join(X0,X2),X1)),complement(meet(X0,X1)))),
inference(superposition,[],[f1994,f111]) ).
fof(f2120,plain,
! [X2,X0,X1] : join(X0,meet(meet(join(X0,X2),X1),complement(meet(X0,X1)))) = join(X0,meet(complement(meet(X0,X1)),join(X0,meet(join(X0,X2),X1)))),
inference(forward_demodulation,[],[f2034,f5]) ).
fof(f2126,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2024,f175]) ).
fof(f2162,plain,
! [X2,X0,X1] : join(X0,meet(complement(meet(X0,X1)),meet(join(X0,X2),X1))) = join(X0,meet(complement(meet(X0,X1)),join(X0,meet(join(X0,X2),X1)))),
inference(forward_demodulation,[],[f2120,f5]) ).
fof(f2167,plain,
! [X0,X1] : n1 = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2126,f1063]) ).
fof(f2191,plain,
! [X2,X0,X1] : join(X0,meet(X1,meet(complement(meet(X0,X1)),join(X0,X2)))) = join(X0,meet(complement(meet(X0,X1)),join(X0,meet(join(X0,X2),X1)))),
inference(forward_demodulation,[],[f2162,f127]) ).
fof(f2748,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f76,f6]) ).
fof(f2804,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,X2)),
inference(backward_demodulation,[],[f527,f2748]) ).
fof(f2860,plain,
meet(sF3,sF0) = meet(c,sF1),
inference(superposition,[],[f118,f17]) ).
fof(f2861,plain,
meet(sF3,sF2) = meet(c,sF2),
inference(superposition,[],[f118,f1459]) ).
fof(f2862,plain,
meet(sF3,sF3) = meet(c,sF3),
inference(superposition,[],[f118,f1458]) ).
fof(f2962,plain,
sF3 = meet(c,sF3),
inference(forward_demodulation,[],[f2862,f1]) ).
fof(f2963,plain,
meet(sF2,sF3) = meet(c,sF2),
inference(forward_demodulation,[],[f2861,f5]) ).
fof(f2964,plain,
meet(c,sF1) = meet(sF0,sF3),
inference(forward_demodulation,[],[f2860,f5]) ).
fof(f2990,plain,
join(sF2,meet(sF3,complement(meet(c,sF2)))) = join(sF2,meet(sF4,complement(meet(c,sF2)))),
inference(backward_demodulation,[],[f2030,f2963]) ).
fof(f3005,plain,
meet(sF2,sF0) = meet(b,sF1),
inference(superposition,[],[f117,f17]) ).
fof(f3007,plain,
meet(sF2,sF3) = meet(b,sF3),
inference(superposition,[],[f117,f1458]) ).
fof(f3107,plain,
meet(c,sF2) = meet(b,sF3),
inference(backward_demodulation,[],[f2963,f3007]) ).
fof(f3109,plain,
meet(b,sF1) = meet(sF0,sF2),
inference(forward_demodulation,[],[f3005,f5]) ).
fof(f3135,plain,
join(sF2,meet(sF3,complement(meet(b,sF3)))) = join(sF2,meet(sF4,complement(meet(b,sF3)))),
inference(backward_demodulation,[],[f2990,f3107]) ).
fof(f3278,plain,
! [X0,X1] : join(complement(X1),meet(X1,X0)) = join(complement(X1),meet(X0,join(complement(X1),meet(X1,X0)))),
inference(superposition,[],[f1298,f491]) ).
fof(f3470,plain,
! [X0] : meet(sF2,X0) = meet(sF2,meet(b,X0)),
inference(superposition,[],[f112,f29]) ).
fof(f3479,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(X0,sF2)),
inference(forward_demodulation,[],[f3470,f127]) ).
fof(f3745,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f2804]) ).
fof(f3746,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X2,X1),X3)) = meet(meet(X0,join(X1,X2)),X3),
inference(superposition,[],[f7,f2804]) ).
fof(f3784,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X1,X2),X3)) = meet(X0,meet(join(X2,X1),X3)),
inference(forward_demodulation,[],[f3746,f7]) ).
fof(f4176,plain,
meet(sF2,sF0) = meet(sF2,meet(b,sF1)),
inference(superposition,[],[f1220,f3109]) ).
fof(f4182,plain,
meet(sF2,sF0) = meet(sF1,meet(sF2,b)),
inference(forward_demodulation,[],[f4176,f127]) ).
fof(f4191,plain,
meet(sF2,sF0) = meet(b,meet(sF1,sF2)),
inference(forward_demodulation,[],[f4182,f127]) ).
fof(f4195,plain,
meet(sF2,sF0) = meet(sF2,sF1),
inference(forward_demodulation,[],[f4191,f3479]) ).
fof(f4198,plain,
meet(sF2,sF0) = meet(sF1,sF2),
inference(forward_demodulation,[],[f4195,f5]) ).
fof(f4201,plain,
meet(sF0,sF2) = meet(sF1,sF2),
inference(forward_demodulation,[],[f4198,f5]) ).
fof(f4203,plain,
meet(b,sF1) = meet(sF1,sF2),
inference(forward_demodulation,[],[f4201,f3109]) ).
fof(f4662,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),join(X3,X2)) = join(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f88,f88]) ).
fof(f4848,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X0,join(X1,join(X3,X2))),
inference(forward_demodulation,[],[f4662,f8]) ).
fof(f5265,plain,
! [X0,X1] : join(X0,meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1))))) = join(X0,meet(n1,complement(meet(X0,join(complement(X0),X1))))),
inference(superposition,[],[f1994,f178]) ).
fof(f5278,plain,
! [X0,X1] : join(X0,meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1))))) = join(X0,complement(meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f5265,f175]) ).
fof(f5296,plain,
! [X0,X1] : n1 = join(X0,meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1))))),
inference(forward_demodulation,[],[f5278,f1063]) ).
fof(f5428,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))) = meet(X0,join(X1,meet(meet(complement(X1),X2),join(n0,X0)))),
inference(superposition,[],[f142,f305]) ).
fof(f5460,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))) = meet(X0,join(X1,meet(complement(X1),meet(X2,join(n0,X0))))),
inference(forward_demodulation,[],[f5428,f7]) ).
fof(f5480,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X1),meet(X2,X0)))) = meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))),
inference(forward_demodulation,[],[f5460,f302]) ).
fof(f6660,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,X1)),
inference(superposition,[],[f7,f2009]) ).
fof(f7776,plain,
! [X0,X1] :
( n1 != n1
| n0 != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(superposition,[],[f58,f167]) ).
fof(f7784,plain,
! [X0] :
( n1 != n1
| n0 != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f58,f9]) ).
fof(f7804,plain,
! [X0] :
( n0 != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f7784]) ).
fof(f7807,plain,
! [X0,X1] :
( n0 != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(trivial_inequality_removal,[],[f7776]) ).
fof(f7818,plain,
! [X0] :
( meet(X0,complement(X0)) != n0
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f7804,f5]) ).
fof(f7824,plain,
! [X0,X1] :
( n0 != meet(X0,join(X1,complement(join(X0,X1))))
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(forward_demodulation,[],[f7807,f5]) ).
fof(f7835,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f7818,f10]) ).
fof(f8140,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),complement(X0)) = join(join(complement(X0),meet(X1,X0)),join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f2748,f1298]) ).
fof(f8227,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),complement(X0)) = join(meet(X0,X1),join(join(complement(X0),meet(X1,X0)),complement(X0))),
inference(forward_demodulation,[],[f8140,f88]) ).
fof(f8273,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),complement(X0)) = join(complement(X0),join(meet(X0,X1),join(complement(X0),meet(X1,X0)))),
inference(forward_demodulation,[],[f8227,f88]) ).
fof(f8296,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),complement(X0)) = join(complement(X0),join(complement(X0),join(meet(X0,X1),meet(X1,X0)))),
inference(forward_demodulation,[],[f8273,f4848]) ).
fof(f8302,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),complement(X0)) = join(complement(X0),join(meet(X0,X1),meet(X1,X0))),
inference(forward_demodulation,[],[f8296,f42]) ).
fof(f8303,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(join(complement(X0),meet(X1,X0)),complement(X0)),
inference(forward_demodulation,[],[f8302,f1404]) ).
fof(f8304,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(complement(X0),join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f8303,f6]) ).
fof(f8305,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[],[f8304,f42]) ).
fof(f8318,plain,
! [X0,X1] : join(X0,meet(complement(X0),X1)) = join(X0,meet(X1,complement(X0))),
inference(superposition,[],[f8305,f7835]) ).
fof(f8498,plain,
! [X2,X0,X1] : join(X1,meet(X0,meet(complement(X1),X2))) = join(X1,meet(complement(X1),meet(X0,X2))),
inference(superposition,[],[f8318,f2009]) ).
fof(f8578,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),meet(complement(meet(X0,X1)),X2))) = join(X0,meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f75,f8318]) ).
fof(f8590,plain,
! [X2,X0,X1] : join(X0,meet(complement(meet(X0,X1)),X2)) = join(X0,meet(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f8578,f75]) ).
fof(f9302,plain,
! [X0,X1] :
( n1 != n1
| n0 != meet(X0,meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1)))))
| complement(X0) = meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1)))) ),
inference(superposition,[],[f11,f5296]) ).
fof(f9335,plain,
! [X0,X1] :
( n0 != meet(X0,meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1)))))
| complement(X0) = meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1)))) ),
inference(trivial_inequality_removal,[],[f9302]) ).
fof(f9361,plain,
! [X0,X1] : complement(X0) = meet(join(complement(X0),X1),complement(meet(X0,join(complement(X0),X1)))),
inference(forward_subsumption_resolution,[],[f9335,f246]) ).
fof(f9495,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))) = X0,
inference(superposition,[],[f9361,f7835]) ).
fof(f11879,plain,
! [X0,X1] :
( n1 != n1
| n0 != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(superposition,[],[f11,f2167]) ).
fof(f11916,plain,
! [X0,X1] :
( n0 != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(trivial_inequality_removal,[],[f11879]) ).
fof(f11945,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_subsumption_resolution,[],[f11916,f246]) ).
fof(f12152,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(complement(X0)),complement(meet(join(complement(X0),X1),complement(complement(X0))))),
inference(superposition,[],[f11945,f9361]) ).
fof(f12157,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(complement(complement(X0)),complement(meet(complement(meet(X0,X1)),complement(complement(X0))))),
inference(superposition,[],[f11945,f11945]) ).
fof(f12193,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f52,f11945]) ).
fof(f12232,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f12193,f5]) ).
fof(f12260,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(complement(complement(X0)),complement(meet(complement(complement(X0)),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f12157,f5]) ).
fof(f12263,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(complement(X0)),complement(meet(complement(complement(X0)),join(complement(X0),X1)))),
inference(forward_demodulation,[],[f12152,f5]) ).
fof(f12308,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f12260,f7835]) ).
fof(f12311,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(meet(X0,join(complement(X0),X1)))),
inference(forward_demodulation,[],[f12263,f7835]) ).
fof(f12341,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f12308,f7835]) ).
fof(f12468,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),X2)),
inference(superposition,[],[f7,f12341]) ).
fof(f12532,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),X2)),
inference(forward_demodulation,[],[f12468,f7]) ).
fof(f12637,plain,
! [X0,X1] : meet(X0,complement(meet(complement(X0),X1))) = X0,
inference(superposition,[],[f12232,f7835]) ).
fof(f12654,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f12232,f1499]) ).
fof(f12683,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),complement(complement(X0))),
inference(superposition,[],[f12232,f9361]) ).
fof(f12765,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(complement(X0)),complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f12683,f5]) ).
fof(f12790,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f12765,f7835]) ).
fof(f12866,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(complement(X0),X1)),X0),
inference(superposition,[],[f32,f12637]) ).
fof(f12925,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f12866,f6]) ).
fof(f12995,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(X1,complement(meet(X0,complement(X1)))),
inference(superposition,[],[f12925,f1499]) ).
fof(f13117,plain,
! [X0,X1] : complement(meet(X1,X0)) = meet(complement(meet(X1,X0)),complement(meet(X0,X1))),
inference(superposition,[],[f12654,f1220]) ).
fof(f13132,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f12654,f3]) ).
fof(f13133,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f12654,f34]) ).
fof(f13199,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f32,f12654]) ).
fof(f13239,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f13199,f6]) ).
fof(f13260,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f13133,f5]) ).
fof(f13261,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f13132,f5]) ).
fof(f14175,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(meet(complement(X0),complement(complement(join(X0,X1)))))),
inference(superposition,[],[f12341,f13261]) ).
fof(f14178,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(meet(complement(X0),join(X0,X1)))),
inference(forward_demodulation,[],[f14175,f7835]) ).
fof(f14426,plain,
! [X0,X1] : complement(join(X0,complement(X1))) = meet(X1,complement(join(X0,complement(X1)))),
inference(superposition,[],[f12790,f50]) ).
fof(f15260,plain,
! [X2,X0,X1] : join(complement(X2),meet(X0,meet(X1,X2))) = join(complement(X2),meet(X2,meet(X1,X0))),
inference(superposition,[],[f8305,f114]) ).
fof(f16315,plain,
! [X0,X1] : complement(join(complement(X0),meet(X1,X0))) = meet(complement(meet(X0,X1)),complement(join(complement(X0),meet(X1,X0)))),
inference(superposition,[],[f13260,f8305]) ).
fof(f16370,plain,
! [X0,X1] : complement(complement(X1)) = meet(complement(complement(join(X0,X1))),complement(meet(complement(X1),complement(complement(join(X0,X1)))))),
inference(superposition,[],[f11945,f13260]) ).
fof(f16379,plain,
! [X0,X1] : complement(complement(X1)) = meet(join(X0,X1),complement(meet(complement(X1),join(X0,X1)))),
inference(forward_demodulation,[],[f16370,f7835]) ).
fof(f16430,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X1),join(X0,X1)))) = X1,
inference(forward_demodulation,[],[f16379,f7835]) ).
fof(f17517,plain,
join(a,sF3) = join(a,sF4),
inference(superposition,[],[f1846,f23]) ).
fof(f17650,plain,
a = join(a,sF4),
inference(forward_demodulation,[],[f17517,f40]) ).
fof(f17687,plain,
sF4 = meet(sF4,a),
inference(superposition,[],[f34,f17650]) ).
fof(f17731,plain,
sF4 = meet(a,sF4),
inference(forward_demodulation,[],[f17687,f5]) ).
fof(f17742,plain,
meet(sF2,sF4) = meet(b,sF4),
inference(superposition,[],[f117,f17731]) ).
fof(f17743,plain,
meet(sF3,sF4) = meet(c,sF4),
inference(superposition,[],[f118,f17731]) ).
fof(f17798,plain,
sF3 = meet(c,sF4),
inference(forward_demodulation,[],[f17743,f96]) ).
fof(f17799,plain,
sF2 = meet(b,sF4),
inference(forward_demodulation,[],[f17742,f97]) ).
fof(f18272,plain,
meet(c,sF3) = meet(c,meet(c,sF1)),
inference(superposition,[],[f1891,f2964]) ).
fof(f18458,plain,
meet(c,sF1) = meet(c,sF3),
inference(forward_demodulation,[],[f18272,f52]) ).
fof(f18498,plain,
sF3 = meet(c,sF1),
inference(forward_demodulation,[],[f18458,f2962]) ).
fof(f19383,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f128,f12790]) ).
fof(f19813,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f19383,f13260]) ).
fof(f21381,plain,
! [X2,X0,X1] : join(X2,X0) = meet(join(X2,X0),join(X2,complement(meet(complement(X0),X1)))),
inference(superposition,[],[f89,f12925]) ).
fof(f21811,plain,
! [X0,X1] : join(complement(X1),X0) = meet(join(complement(X1),X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f21381,f13239]) ).
fof(f22107,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = meet(join(complement(X1),complement(X0)),complement(meet(X0,X1))),
inference(superposition,[],[f21811,f7835]) ).
fof(f22122,plain,
! [X0,X1] : join(complement(meet(X1,complement(X0))),X0) = meet(join(complement(meet(X1,complement(X0))),X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f21811,f1220]) ).
fof(f22211,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = join(complement(complement(meet(complement(X1),X0))),complement(join(complement(X0),X1))),
inference(superposition,[],[f13239,f21811]) ).
fof(f22217,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = join(complement(join(complement(X0),X1)),complement(complement(meet(complement(X1),X0)))),
inference(forward_demodulation,[],[f22211,f6]) ).
fof(f22285,plain,
! [X0,X1] : join(complement(meet(X1,complement(X0))),X0) = meet(complement(meet(complement(X0),X1)),join(complement(meet(X1,complement(X0))),X0)),
inference(forward_demodulation,[],[f22122,f5]) ).
fof(f22298,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = meet(complement(meet(X0,X1)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f22107,f5]) ).
fof(f22323,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = join(complement(join(complement(X0),X1)),meet(complement(X1),X0)),
inference(forward_demodulation,[],[f22217,f7835]) ).
fof(f22382,plain,
! [X0,X1] : join(complement(meet(X1,complement(X0))),X0) = meet(complement(meet(complement(X0),X1)),join(X0,complement(meet(X1,complement(X0))))),
inference(forward_demodulation,[],[f22285,f2804]) ).
fof(f22407,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f22323,f6]) ).
fof(f22454,plain,
! [X0,X1] : join(complement(meet(X1,complement(X0))),X0) = meet(complement(meet(complement(X0),X1)),complement(meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f22382,f12995]) ).
fof(f22474,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(forward_demodulation,[],[f22407,f19813]) ).
fof(f22504,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(X1,complement(X0))),X0),
inference(forward_demodulation,[],[f22454,f13117]) ).
fof(f22544,plain,
! [X0,X1] : meet(complement(meet(X1,X0)),X0) = meet(complement(meet(X0,X1)),meet(complement(meet(X1,X0)),X0)),
inference(backward_demodulation,[],[f16315,f22474]) ).
fof(f22548,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,join(complement(X0),X1)))),
inference(backward_demodulation,[],[f12311,f22474]) ).
fof(f22679,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f22504,f6]) ).
fof(f22741,plain,
! [X0,X1] : meet(complement(meet(X1,X0)),X0) = meet(X0,meet(complement(meet(X0,X1)),complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f22544,f127]) ).
fof(f22793,plain,
! [X0,X1] : meet(complement(meet(X1,X0)),X0) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f22741,f13117]) ).
fof(f22822,plain,
! [X0,X1] : meet(X0,complement(meet(X1,X0))) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f22793,f5]) ).
fof(f22866,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = meet(complement(X0),complement(meet(complement(X0),join(X0,X1)))),
inference(superposition,[],[f22548,f7835]) ).
fof(f22870,plain,
! [X0,X1] : meet(complement(meet(X1,join(complement(X0),meet(X0,X1)))),X0) = meet(X0,complement(meet(X0,join(complement(X0),meet(X0,X1))))),
inference(superposition,[],[f22548,f3278]) ).
fof(f22888,plain,
! [X0,X1] : meet(X1,complement(meet(X1,join(X0,complement(X1))))) = meet(complement(join(X0,complement(X1))),X1),
inference(superposition,[],[f22548,f50]) ).
fof(f22915,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,join(X1,complement(X0))))),
inference(superposition,[],[f22548,f2804]) ).
fof(f22926,plain,
! [X0,X1] : meet(X1,complement(meet(complement(X0),X1))) = meet(X1,join(complement(X1),X0)),
inference(superposition,[],[f12341,f22548]) ).
fof(f22933,plain,
! [X2,X0,X1] : meet(meet(complement(X0),X1),X2) = meet(X1,meet(complement(meet(X1,join(complement(X1),X0))),X2)),
inference(superposition,[],[f7,f22548]) ).
fof(f23034,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,X2)) = meet(X1,meet(complement(meet(X1,join(complement(X1),X0))),X2)),
inference(forward_demodulation,[],[f22933,f7]) ).
fof(f23043,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X0)) = X0,
inference(backward_demodulation,[],[f9495,f22926]) ).
fof(f23044,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X1)) = X1,
inference(backward_demodulation,[],[f16430,f22926]) ).
fof(f23076,plain,
! [X0,X1] : meet(X1,complement(meet(X1,join(X0,complement(X1))))) = meet(X1,complement(join(X0,complement(X1)))),
inference(forward_demodulation,[],[f22888,f5]) ).
fof(f23092,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = meet(complement(meet(X1,join(complement(X0),meet(X0,X1)))),X0),
inference(forward_demodulation,[],[f22870,f22548]) ).
fof(f23096,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f22866,f14178]) ).
fof(f23123,plain,
! [X0,X1] : meet(join(X0,X1),join(X1,complement(join(X0,X1)))) = X1,
inference(forward_demodulation,[],[f23044,f2804]) ).
fof(f23124,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f23043,f2804]) ).
fof(f23148,plain,
! [X0,X1] : complement(join(X0,complement(X1))) = meet(X1,complement(meet(X1,join(X0,complement(X1))))),
inference(forward_demodulation,[],[f23076,f14426]) ).
fof(f23164,plain,
! [X0,X1] : meet(complement(meet(X0,X1)),X0) = meet(X0,complement(meet(X1,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f23092,f5]) ).
fof(f23185,plain,
! [X0,X1] : complement(meet(X1,X0)) = complement(join(meet(X0,X1),meet(X1,X0))),
inference(backward_demodulation,[],[f13117,f23096]) ).
fof(f23320,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(forward_demodulation,[],[f23148,f22915]) ).
fof(f23334,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,complement(meet(X1,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f23164,f5]) ).
fof(f23435,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_demodulation,[],[f23185,f1404]) ).
fof(f23500,plain,
! [X0,X1] :
( meet(complement(X1),join(X0,X1)) = X0
| n0 != meet(X0,join(X1,complement(join(X0,X1)))) ),
inference(backward_demodulation,[],[f7824,f23320]) ).
fof(f23639,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(X1,complement(X0))),
inference(superposition,[],[f23096,f7835]) ).
fof(f23664,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(X0,meet(complement(X0),complement(X1))),
inference(superposition,[],[f8318,f23096]) ).
fof(f23684,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(X1)),
inference(superposition,[],[f5,f23096]) ).
fof(f23796,plain,
! [X0,X1] : join(X0,complement(join(X1,X0))) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f23664,f23096]) ).
fof(f23996,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f112,f23124]) ).
fof(f24200,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f23996,f6]) ).
fof(f24437,plain,
! [X0,X1] :
( meet(complement(X1),join(X0,X1)) = X0
| meet(X0,X1) != n0 ),
inference(backward_demodulation,[],[f23500,f24200]) ).
fof(f24440,plain,
! [X0,X1] :
( complement(X0) = join(X1,complement(join(X0,X1)))
| meet(X0,X1) != n0 ),
inference(backward_demodulation,[],[f1812,f24200]) ).
fof(f24618,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(meet(X0,X1),complement(X0))),
inference(superposition,[],[f23123,f4]) ).
fof(f24619,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(meet(X1,X0),complement(X0))),
inference(superposition,[],[f23123,f32]) ).
fof(f24652,plain,
! [X0,X1] : meet(X1,X0) = meet(join(complement(X0),meet(X0,X1)),join(meet(X1,X0),complement(join(complement(X0),meet(X0,X1))))),
inference(superposition,[],[f23123,f8305]) ).
fof(f24785,plain,
! [X0,X1] : meet(X1,X0) = meet(join(complement(X0),meet(X0,X1)),join(meet(X1,X0),meet(complement(meet(X0,X1)),X0))),
inference(forward_demodulation,[],[f24652,f22474]) ).
fof(f24804,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(complement(X0),meet(X1,X0))),
inference(forward_demodulation,[],[f24619,f2804]) ).
fof(f24805,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f24618,f2804]) ).
fof(f24845,plain,
! [X0,X1] : meet(X1,X0) = meet(join(complement(X0),meet(X0,X1)),join(meet(X1,X0),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f24785,f5]) ).
fof(f24940,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(complement(X0),X1)),
inference(superposition,[],[f23639,f6]) ).
fof(f24972,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f7835,f23639]) ).
fof(f25016,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,join(X0,complement(X1))),
inference(backward_demodulation,[],[f22679,f24972]) ).
fof(f25034,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(join(meet(X0,X1),complement(X0)),X2)),
inference(backward_demodulation,[],[f12532,f24972]) ).
fof(f25199,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(join(complement(X0),meet(X0,X1)),X2)),
inference(forward_demodulation,[],[f25034,f3784]) ).
fof(f25214,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(X1)),
inference(forward_demodulation,[],[f25016,f42]) ).
fof(f26175,plain,
! [X2,X0,X1] : complement(join(X2,meet(X0,complement(X1)))) = meet(complement(X2),join(X1,complement(X0))),
inference(superposition,[],[f23320,f23639]) ).
fof(f26206,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X0,meet(complement(X0),X1))),
inference(superposition,[],[f23996,f23320]) ).
fof(f26220,plain,
! [X2,X0,X1] : join(join(X0,complement(X1)),meet(X2,meet(complement(X0),X1))) = join(join(X0,complement(X1)),meet(meet(complement(X0),X1),X2)),
inference(superposition,[],[f8318,f23320]) ).
fof(f26238,plain,
! [X2,X0,X1] : join(join(X0,complement(X1)),meet(X2,meet(complement(X0),X1))) = join(X0,join(complement(X1),meet(meet(complement(X0),X1),X2))),
inference(forward_demodulation,[],[f26220,f8]) ).
fof(f26286,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = complement(join(meet(X0,X1),meet(X0,complement(complement(X1))))),
inference(backward_demodulation,[],[f22298,f26175]) ).
fof(f26292,plain,
! [X2,X0,X1] : join(join(X0,complement(X1)),meet(X2,meet(complement(X0),X1))) = join(X0,join(complement(X1),meet(complement(X0),meet(X1,X2)))),
inference(forward_demodulation,[],[f26238,f7]) ).
fof(f26305,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = complement(join(meet(X0,X1),meet(X0,X1))),
inference(forward_demodulation,[],[f26286,f7835]) ).
fof(f26322,plain,
! [X2,X0,X1] : join(X0,join(complement(X1),meet(complement(X0),meet(X1,X2)))) = join(X0,join(complement(X1),meet(X2,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f26292,f8]) ).
fof(f26329,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f26305,f2]) ).
fof(f26622,plain,
! [X2,X0,X1] : complement(meet(join(X0,complement(X1)),X2)) = join(complement(X2),meet(complement(X0),X1)),
inference(superposition,[],[f26329,f23320]) ).
fof(f26623,plain,
! [X2,X0,X1] : complement(meet(join(X1,complement(X0)),X2)) = join(complement(X2),meet(X0,complement(X1))),
inference(superposition,[],[f26329,f23639]) ).
fof(f26683,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),X2) = meet(X2,join(complement(X0),complement(X1))),
inference(superposition,[],[f3745,f26329]) ).
fof(f26694,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),X2) = meet(X2,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f26683,f26329]) ).
fof(f26803,plain,
! [X2,X0,X1] : join(X0,join(complement(X1),meet(X2,meet(complement(X0),X1)))) = join(X0,complement(meet(join(X0,complement(meet(X1,X2))),X1))),
inference(backward_demodulation,[],[f26322,f26622]) ).
fof(f26912,plain,
! [X2,X0,X1] : join(X0,join(complement(X1),meet(X2,meet(complement(X0),X1)))) = join(X0,complement(meet(X1,join(X0,complement(meet(X1,X2)))))),
inference(forward_demodulation,[],[f26803,f23435]) ).
fof(f27281,plain,
! [X2,X0,X1] : complement(join(X2,meet(X0,complement(X1)))) = meet(complement(X2),join(complement(X0),X1)),
inference(superposition,[],[f23320,f24940]) ).
fof(f27621,plain,
! [X0,X1] :
( complement(complement(X0)) = join(meet(X1,X0),complement(join(complement(X0),meet(X0,X1))))
| n0 != meet(complement(X0),meet(X1,X0)) ),
inference(superposition,[],[f24440,f8305]) ).
fof(f27622,plain,
! [X0,X1] :
( complement(complement(X0)) = join(meet(X0,X1),complement(join(complement(X0),meet(X1,X0))))
| n0 != meet(complement(X0),meet(X0,X1)) ),
inference(superposition,[],[f24440,f8305]) ).
fof(f27757,plain,
! [X0,X1] :
( complement(complement(X0)) = join(meet(X0,X1),meet(complement(meet(X1,X0)),X0))
| n0 != meet(complement(X0),meet(X0,X1)) ),
inference(forward_demodulation,[],[f27622,f22474]) ).
fof(f27758,plain,
! [X0,X1] :
( complement(complement(X0)) = join(meet(X1,X0),meet(complement(meet(X0,X1)),X0))
| n0 != meet(complement(X0),meet(X1,X0)) ),
inference(forward_demodulation,[],[f27621,f22474]) ).
fof(f27813,plain,
! [X0,X1] :
( complement(complement(X0)) = join(meet(X0,X1),meet(X0,complement(meet(X1,X0))))
| n0 != meet(complement(X0),meet(X0,X1)) ),
inference(forward_demodulation,[],[f27757,f5]) ).
fof(f27814,plain,
! [X0,X1] :
( complement(complement(X0)) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1))))
| n0 != meet(complement(X0),meet(X1,X0)) ),
inference(forward_demodulation,[],[f27758,f5]) ).
fof(f27860,plain,
! [X0,X1] :
( join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = X0
| n0 != meet(complement(X0),meet(X0,X1)) ),
inference(forward_demodulation,[],[f27813,f7835]) ).
fof(f27861,plain,
! [X0,X1] :
( join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0
| n0 != meet(complement(X0),meet(X1,X0)) ),
inference(forward_demodulation,[],[f27814,f7835]) ).
fof(f27892,plain,
! [X0,X1] :
( n0 != meet(X0,meet(X1,complement(X0)))
| join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = X0 ),
inference(forward_demodulation,[],[f27860,f127]) ).
fof(f27893,plain,
! [X0,X1] :
( n0 != meet(X0,meet(complement(X0),X1))
| join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0 ),
inference(forward_demodulation,[],[f27861,f127]) ).
fof(f27910,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X1,X0)))) = X0,
inference(forward_subsumption_resolution,[],[f27892,f1358]) ).
fof(f27911,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_subsumption_resolution,[],[f27893,f305]) ).
fof(f27926,plain,
! [X0,X1] : meet(X1,X0) = meet(join(complement(X0),meet(X0,X1)),X0),
inference(backward_demodulation,[],[f24845,f27911]) ).
fof(f27936,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(forward_demodulation,[],[f27926,f5]) ).
fof(f28001,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),complement(meet(join(X0,complement(join(X0,X1))),join(X0,X1))))),
inference(superposition,[],[f27910,f23124]) ).
fof(f28046,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(meet(X1,join(X2,meet(X1,X0))),X0),meet(meet(X1,join(X2,meet(X1,X0))),complement(meet(X0,X1)))),
inference(superposition,[],[f27910,f1083]) ).
fof(f28047,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(meet(X1,join(X2,X0)),X0),meet(meet(X1,join(X2,X0)),complement(meet(X0,X1)))),
inference(superposition,[],[f27910,f1894]) ).
fof(f28131,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X1,X0)))),
inference(superposition,[],[f76,f27910]) ).
fof(f28222,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f1994,f28131]) ).
fof(f28344,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(meet(X1,join(X2,X0)),X0),meet(complement(meet(X1,X0)),meet(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f28047,f26694]) ).
fof(f28345,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(meet(X1,join(X2,meet(X1,X0))),X0),meet(complement(meet(X1,X0)),meet(X1,join(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f28046,f26694]) ).
fof(f28386,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),complement(meet(join(X0,X1),join(X0,complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f28001,f22822]) ).
fof(f28551,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(meet(X1,join(X2,X0)),X0),meet(X1,meet(join(X2,X0),complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f28344,f127]) ).
fof(f28552,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(meet(X1,join(X2,meet(X1,X0))),X0),meet(X1,meet(join(X2,meet(X1,X0)),complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f28345,f127]) ).
fof(f28589,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f28386,f22915]) ).
fof(f28697,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,meet(X1,join(X2,X0))),meet(X1,meet(join(X2,X0),complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f28551,f5]) ).
fof(f28698,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(meet(X1,join(X2,meet(X1,X0))),X0),meet(X1,meet(complement(meet(X1,X0)),join(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f28552,f6660]) ).
fof(f28780,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(X1,meet(join(X2,X0),complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f28697,f1894]) ).
fof(f28781,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X0,meet(X1,join(X2,meet(X1,X0)))),meet(X1,meet(complement(meet(X1,X0)),join(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f28698,f5]) ).
fof(f28828,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X0,X1),meet(X1,meet(complement(meet(X1,X0)),join(X2,meet(X1,X0))))),
inference(forward_demodulation,[],[f28781,f1083]) ).
fof(f28960,plain,
sF4 = join(sF2,meet(sF4,complement(meet(sF2,sF3)))),
inference(superposition,[],[f28222,f23]) ).
fof(f28964,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(join(X1,X0),complement(meet(X0,X1)))),
inference(superposition,[],[f28222,f5]) ).
fof(f28980,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X2),X1)) = join(X0,meet(join(X0,meet(join(X0,X2),X1)),complement(meet(X0,X1)))),
inference(superposition,[],[f28222,f111]) ).
fof(f29031,plain,
join(b,sF4) = join(b,meet(join(b,sF4),complement(sF2))),
inference(superposition,[],[f28222,f17799]) ).
fof(f29168,plain,
join(b,sF4) = join(b,meet(complement(sF2),join(b,sF4))),
inference(forward_demodulation,[],[f29031,f5]) ).
fof(f29217,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X2),X1)) = join(X0,meet(complement(meet(X0,X1)),join(X0,meet(join(X0,X2),X1)))),
inference(forward_demodulation,[],[f28980,f8590]) ).
fof(f29233,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f2033,f28964]) ).
fof(f29235,plain,
sF4 = join(sF2,meet(sF4,complement(meet(b,sF3)))),
inference(forward_demodulation,[],[f28960,f3007]) ).
fof(f29349,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X2),X1)) = join(X0,meet(X1,meet(complement(meet(X0,X1)),join(X0,X2)))),
inference(backward_demodulation,[],[f2191,f29217]) ).
fof(f29403,plain,
sF4 = join(sF2,meet(sF3,complement(meet(b,sF3)))),
inference(backward_demodulation,[],[f3135,f29235]) ).
fof(f31012,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(join(X2,X0),complement(join(X0,join(X1,X2))))),
inference(superposition,[],[f24200,f88]) ).
fof(f31225,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X2,join(X0,complement(join(X0,join(X1,X2)))))),
inference(forward_demodulation,[],[f31012,f8]) ).
fof(f31903,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(join(complement(complement(X0)),meet(complement(X0),X1)))),
inference(superposition,[],[f25214,f24805]) ).
fof(f31910,plain,
! [X0,X1] : complement(meet(complement(X0),complement(X1))) = join(X1,complement(complement(meet(complement(X1),join(complement(complement(X1)),X0))))),
inference(superposition,[],[f25214,f22548]) ).
fof(f31948,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(meet(complement(X0),X1),join(join(X0,complement(X1)),meet(X2,meet(complement(X0),X1)))),
inference(superposition,[],[f24804,f25214]) ).
fof(f31959,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(complement(X0),meet(X1,join(join(X0,complement(X1)),meet(X2,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f31948,f7]) ).
fof(f31985,plain,
! [X0,X1] : complement(meet(complement(X0),complement(X1))) = join(X1,meet(complement(X1),join(complement(complement(X1)),X0))),
inference(forward_demodulation,[],[f31910,f7835]) ).
fof(f31992,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(meet(complement(X0),X1)),complement(X0))),
inference(forward_demodulation,[],[f31903,f22474]) ).
fof(f32037,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(complement(X0),meet(X1,join(X0,join(complement(X1),meet(X2,meet(complement(X0),X1)))))),
inference(forward_demodulation,[],[f31959,f8]) ).
fof(f32057,plain,
! [X0,X1] : complement(meet(complement(X0),complement(X1))) = join(X1,complement(join(X1,meet(complement(X1),complement(X0))))),
inference(forward_demodulation,[],[f31985,f27281]) ).
fof(f32064,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(X0),complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f31992,f8318]) ).
fof(f32095,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(complement(X0),meet(X1,join(X0,complement(meet(X1,join(X0,complement(meet(X1,X2)))))))),
inference(forward_demodulation,[],[f32037,f26912]) ).
fof(f32108,plain,
! [X0,X1] : complement(meet(complement(X0),complement(X1))) = join(X1,complement(join(X1,complement(join(X0,X1))))),
inference(forward_demodulation,[],[f32057,f23096]) ).
fof(f32110,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(join(meet(complement(X0),X1),X0))),
inference(forward_demodulation,[],[f32064,f23096]) ).
fof(f32137,plain,
! [X0,X1] : join(X1,meet(complement(X1),join(X0,X1))) = complement(meet(complement(X0),complement(X1))),
inference(forward_demodulation,[],[f32108,f23320]) ).
fof(f32139,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(join(X0,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f32110,f23796]) ).
fof(f32156,plain,
! [X0,X1] : join(X1,meet(complement(X1),join(X0,X1))) = join(X1,complement(complement(X0))),
inference(forward_demodulation,[],[f32137,f24972]) ).
fof(f32158,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f32139,f25214]) ).
fof(f32167,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(complement(X1),join(X0,X1))),
inference(forward_demodulation,[],[f32156,f7835]) ).
fof(f32257,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(meet(complement(X0),join(X1,X0)),join(X0,X2)),
inference(superposition,[],[f78,f32167]) ).
fof(f32331,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f32257,f88]) ).
fof(f32421,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,meet(complement(X0),join(X1,X0)))),
inference(forward_demodulation,[],[f32331,f8]) ).
fof(f34723,plain,
! [X2,X0,X1] : join(join(X0,complement(join(X0,X1))),X2) = join(complement(join(X1,X0)),join(X0,X2)),
inference(superposition,[],[f78,f23796]) ).
fof(f34786,plain,
! [X2,X0,X1] : join(X0,join(complement(join(X0,X1)),X2)) = join(X2,join(X0,complement(join(X1,X0)))),
inference(superposition,[],[f88,f23796]) ).
fof(f34900,plain,
! [X2,X0,X1] : join(join(X0,complement(join(X0,X1))),X2) = join(X0,join(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f34723,f88]) ).
fof(f34974,plain,
! [X2,X0,X1] : join(X0,join(complement(join(X0,X1)),X2)) = join(X0,join(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f34900,f8]) ).
fof(f36038,plain,
join(sF2,sF1) = join(sF2,meet(sF1,complement(meet(b,sF1)))),
inference(superposition,[],[f29233,f4203]) ).
fof(f36050,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,complement(join(X0,meet(complement(X0),X1)))),
inference(superposition,[],[f29233,f23684]) ).
fof(f36093,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(join(X0,X1),join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1)))),
inference(superposition,[],[f23123,f29233]) ).
fof(f36097,plain,
! [X0,X1] :
( meet(complement(meet(X1,complement(meet(X1,X0)))),join(X0,X1)) = X0
| n0 != meet(X0,meet(X1,complement(meet(X1,X0)))) ),
inference(superposition,[],[f24437,f29233]) ).
fof(f36141,plain,
! [X0,X1] : meet(complement(meet(X1,complement(meet(X1,X0)))),join(X0,X1)) = X0,
inference(forward_subsumption_resolution,[],[f36097,f1085]) ).
fof(f36144,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(join(X0,X1),join(complement(join(X0,X1)),meet(X1,complement(meet(X1,X0))))),
inference(forward_demodulation,[],[f36093,f2804]) ).
fof(f36180,plain,
join(sF1,sF2) = join(sF2,meet(sF1,complement(meet(b,sF1)))),
inference(forward_demodulation,[],[f36038,f6]) ).
fof(f36295,plain,
! [X0,X1] : meet(join(X1,X0),complement(meet(X1,complement(meet(X1,X0))))) = X0,
inference(forward_demodulation,[],[f36141,f3745]) ).
fof(f36298,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(join(X0,X1),complement(meet(join(meet(X1,X0),complement(X1)),join(X0,X1)))),
inference(forward_demodulation,[],[f36144,f26623]) ).
fof(f36425,plain,
! [X0,X1] : meet(join(X1,X0),join(meet(X1,X0),complement(X1))) = X0,
inference(forward_demodulation,[],[f36295,f24972]) ).
fof(f36427,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(join(X0,X1),complement(meet(join(X0,X1),join(meet(X1,X0),complement(X1))))),
inference(forward_demodulation,[],[f36298,f22822]) ).
fof(f36489,plain,
! [X0,X1] : meet(join(X1,X0),join(complement(X1),meet(X1,X0))) = X0,
inference(forward_demodulation,[],[f36425,f2804]) ).
fof(f36491,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(join(X0,X1),complement(meet(join(X0,X1),join(complement(X1),meet(X1,X0))))),
inference(forward_demodulation,[],[f36427,f2804]) ).
fof(f36571,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(X1),meet(X1,X0))) = X0,
inference(superposition,[],[f36489,f6]) ).
fof(f36575,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),join(complement(X0),meet(X0,meet(X1,complement(meet(X0,X1)))))),
inference(superposition,[],[f36489,f28131]) ).
fof(f36576,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(join(X0,X1),join(complement(X0),meet(X0,meet(X1,complement(meet(X1,X0)))))),
inference(superposition,[],[f36489,f29233]) ).
fof(f36747,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X1,X0)),
inference(superposition,[],[f385,f36489]) ).
fof(f36752,plain,
! [X0,X1] : meet(join(complement(X1),meet(X1,X0)),X0) = X0,
inference(superposition,[],[f51,f36489]) ).
fof(f36827,plain,
! [X0,X1] : meet(X0,join(complement(X1),meet(X1,X0))) = X0,
inference(forward_demodulation,[],[f36752,f5]) ).
fof(f36846,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f28589,f36747]) ).
fof(f36971,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(join(X0,X1),join(complement(X0),n0)),
inference(forward_demodulation,[],[f36576,f1085]) ).
fof(f36972,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),join(complement(X0),n0)),
inference(forward_demodulation,[],[f36575,f246]) ).
fof(f36980,plain,
! [X0,X1] : meet(join(X0,X1),complement(X0)) = meet(X1,complement(meet(X1,X0))),
inference(backward_demodulation,[],[f36491,f36571]) ).
fof(f37020,plain,
! [X0,X1] : join(complement(X1),meet(X1,X0)) = join(complement(X1),X0),
inference(backward_demodulation,[],[f3278,f36827]) ).
fof(f37042,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(X0,complement(meet(X0,X1))),
inference(backward_demodulation,[],[f23334,f36827]) ).
fof(f37131,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),join(X0,X1)),
inference(backward_demodulation,[],[f26206,f36846]) ).
fof(f37143,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(backward_demodulation,[],[f32158,f36846]) ).
fof(f37146,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(backward_demodulation,[],[f36050,f36846]) ).
fof(f37151,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,meet(X0,meet(complement(X1),X2)))),
inference(backward_demodulation,[],[f5480,f36846]) ).
fof(f37153,plain,
! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,meet(X0,meet(complement(X1),X2))),
inference(backward_demodulation,[],[f8498,f36846]) ).
fof(f37277,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(join(X0,X1),join(n0,complement(X0))),
inference(forward_demodulation,[],[f36971,f2804]) ).
fof(f37278,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),join(n0,complement(X0))),
inference(forward_demodulation,[],[f36972,f2804]) ).
fof(f37281,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f36980,f5]) ).
fof(f37335,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(X0,complement(meet(X1,X0))),
inference(backward_demodulation,[],[f22822,f37042]) ).
fof(f37511,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(join(complement(X0),X1),X2)),
inference(backward_demodulation,[],[f25199,f37020]) ).
fof(f37519,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f27936,f37020]) ).
fof(f37548,plain,
! [X2,X0,X1] : join(complement(X2),meet(X0,meet(X1,X2))) = join(complement(X2),meet(X1,X0)),
inference(backward_demodulation,[],[f15260,f37020]) ).
fof(f37685,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f37151,f37153]) ).
fof(f37715,plain,
! [X2,X0,X1] : join(X0,join(complement(join(X0,X1)),X2)) = join(X2,join(X0,complement(X1))),
inference(backward_demodulation,[],[f34786,f37146]) ).
fof(f37797,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X2,join(X0,complement(join(X1,X2))))),
inference(backward_demodulation,[],[f31225,f37143]) ).
fof(f37832,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,meet(complement(X0),X1))),
inference(backward_demodulation,[],[f32421,f37131]) ).
fof(f37838,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X0,X1),meet(X1,meet(complement(meet(X1,X0)),X2))),
inference(backward_demodulation,[],[f28828,f37131]) ).
fof(f38012,plain,
! [X0,X1] : meet(join(X0,X1),complement(X0)) = meet(X1,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f37277,f302]) ).
fof(f38013,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),complement(X0)),
inference(forward_demodulation,[],[f37278,f302]) ).
fof(f38016,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(X1,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f37281,f36747]) ).
fof(f38219,plain,
join(sF1,sF2) = join(sF2,meet(sF1,complement(b))),
inference(backward_demodulation,[],[f36180,f37335]) ).
fof(f38220,plain,
sF4 = join(sF2,meet(sF3,complement(b))),
inference(backward_demodulation,[],[f29403,f37335]) ).
fof(f38314,plain,
! [X2,X0,X1] : join(X0,complement(meet(X1,join(X0,complement(meet(X1,X2)))))) = join(X0,join(complement(X1),meet(complement(X0),X2))),
inference(backward_demodulation,[],[f26912,f37548]) ).
fof(f38344,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,X2)) = meet(X1,meet(complement(meet(X0,X1)),X2)),
inference(backward_demodulation,[],[f23034,f37519]) ).
fof(f38515,plain,
! [X2,X0,X1] : join(X2,join(X0,complement(X1))) = join(X0,join(X2,complement(join(X1,X0)))),
inference(backward_demodulation,[],[f34974,f37715]) ).
fof(f38761,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(join(X0,X1),complement(X0)),
inference(forward_demodulation,[],[f38012,f37042]) ).
fof(f38762,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f38013,f5]) ).
fof(f38825,plain,
sF4 = join(sF2,meet(complement(b),sF3)),
inference(forward_demodulation,[],[f38220,f5]) ).
fof(f38826,plain,
join(sF1,sF2) = join(sF2,meet(complement(b),sF1)),
inference(forward_demodulation,[],[f38219,f5]) ).
fof(f38905,plain,
! [X2,X0,X1] : join(X0,complement(meet(X1,join(X0,complement(meet(X1,X2)))))) = join(X0,join(X2,complement(X1))),
inference(forward_demodulation,[],[f38314,f37832]) ).
fof(f38959,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X2),X1)) = join(X0,meet(complement(X0),meet(X1,join(X0,X2)))),
inference(backward_demodulation,[],[f29349,f38344]) ).
fof(f39060,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,join(X2,complement(X1)))),
inference(backward_demodulation,[],[f37797,f38515]) ).
fof(f39224,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f38761,f5]) ).
fof(f39225,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f38762,f36747]) ).
fof(f39314,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(complement(X0),meet(X1,join(X0,join(X2,complement(X1))))),
inference(backward_demodulation,[],[f32095,f38905]) ).
fof(f39335,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X0,X2))) = join(X0,meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f38959,f36846]) ).
fof(f39534,plain,
! [X2,X0,X1] : meet(X2,meet(complement(X0),X1)) = meet(complement(X0),meet(X1,join(X2,X0))),
inference(forward_demodulation,[],[f39314,f39060]) ).
fof(f41533,plain,
! [X2,X0,X1] : meet(X1,meet(complement(meet(X1,X0)),X2)) = meet(X2,meet(complement(X0),X1)),
inference(superposition,[],[f127,f38016]) ).
fof(f41545,plain,
! [X2,X0,X1] : meet(meet(complement(X0),X1),X2) = meet(X1,meet(X2,complement(meet(X1,X0)))),
inference(superposition,[],[f2009,f38016]) ).
fof(f41596,plain,
! [X2,X0,X1] : meet(complement(X0),meet(X1,X2)) = meet(X1,meet(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f41545,f7]) ).
fof(f41604,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = join(meet(X0,X1),meet(X2,meet(complement(X0),X1))),
inference(backward_demodulation,[],[f37838,f41533]) ).
fof(f41736,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(complement(X0),meet(X1,join(X2,X0)))),
inference(backward_demodulation,[],[f28780,f41596]) ).
fof(f41833,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(X2,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f41736,f39534]) ).
fof(f41876,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X2,meet(X1,X0))),
inference(backward_demodulation,[],[f41604,f41833]) ).
fof(f41972,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,X2)),
inference(backward_demodulation,[],[f37685,f41876]) ).
fof(f45450,plain,
meet(sF4,complement(sF2)) = meet(complement(b),sF4),
inference(superposition,[],[f39225,f17799]) ).
fof(f45465,plain,
meet(sF3,complement(meet(b,sF3))) = meet(complement(sF2),sF3),
inference(superposition,[],[f39225,f3007]) ).
fof(f45578,plain,
meet(sF3,complement(meet(b,sF3))) = meet(sF3,complement(sF2)),
inference(forward_demodulation,[],[f45465,f5]) ).
fof(f45663,plain,
meet(sF3,complement(b)) = meet(sF3,complement(sF2)),
inference(forward_demodulation,[],[f45578,f37335]) ).
fof(f45729,plain,
meet(complement(b),sF3) = meet(sF3,complement(sF2)),
inference(forward_demodulation,[],[f45663,f5]) ).
fof(f48414,plain,
meet(complement(sF2),sF4) = meet(sF3,complement(sF2)),
inference(superposition,[],[f39224,f23]) ).
fof(f48504,plain,
meet(complement(sF2),sF4) = meet(complement(b),sF3),
inference(forward_demodulation,[],[f48414,f45729]) ).
fof(f48581,plain,
meet(sF4,complement(sF2)) = meet(complement(b),sF3),
inference(forward_demodulation,[],[f48504,f5]) ).
fof(f48642,plain,
meet(complement(b),sF3) = meet(complement(b),sF4),
inference(backward_demodulation,[],[f45450,f48581]) ).
fof(f50921,plain,
! [X2,X0,X1] : join(X0,meet(complement(X0),meet(X1,X2))) = join(X0,meet(join(complement(complement(X0)),X1),X2)),
inference(superposition,[],[f36846,f37511]) ).
fof(f50940,plain,
! [X2,X0,X1] : join(X0,meet(complement(X0),meet(X1,X2))) = join(X0,meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f50921,f7835]) ).
fof(f51057,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f50940,f36846]) ).
fof(f51137,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X0,X2))) = join(X0,meet(X2,X1)),
inference(backward_demodulation,[],[f39335,f51057]) ).
fof(f51304,plain,
join(b,sF4) = join(b,meet(sF4,complement(sF2))),
inference(backward_demodulation,[],[f29168,f51137]) ).
fof(f51434,plain,
join(b,sF4) = join(b,meet(complement(b),sF3)),
inference(forward_demodulation,[],[f51304,f48581]) ).
fof(f51572,plain,
join(b,sF4) = join(b,sF3),
inference(forward_demodulation,[],[f51434,f36846]) ).
fof(f52509,plain,
sF4 = meet(sF4,join(b,sF3)),
inference(superposition,[],[f34,f51572]) ).
fof(f53042,plain,
! [X0] : meet(sF4,join(X0,sF3)) = meet(sF4,join(X0,c)),
inference(superposition,[],[f41972,f17798]) ).
fof(f53237,plain,
sF4 = meet(sF4,join(b,c)),
inference(backward_demodulation,[],[f52509,f53042]) ).
fof(f53458,plain,
sF4 = meet(sF4,sF0),
inference(forward_demodulation,[],[f53237,f15]) ).
fof(f53588,plain,
sF4 = meet(sF0,sF4),
inference(forward_demodulation,[],[f53458,f5]) ).
fof(f53713,plain,
meet(a,sF4) = meet(sF1,sF4),
inference(superposition,[],[f116,f53588]) ).
fof(f53761,plain,
sF4 = meet(sF1,sF4),
inference(forward_demodulation,[],[f53713,f17731]) ).
fof(f53772,plain,
sF1 = join(sF1,sF4),
inference(superposition,[],[f4,f53761]) ).
fof(f54466,plain,
! [X0] : join(b,meet(c,X0)) = join(b,meet(sF0,X0)),
inference(superposition,[],[f51057,f15]) ).
fof(f58544,plain,
join(b,sF1) = join(b,meet(c,sF1)),
inference(superposition,[],[f54466,f1460]) ).
fof(f58694,plain,
join(b,sF1) = join(b,sF3),
inference(forward_demodulation,[],[f58544,f18498]) ).
fof(f58725,plain,
join(b,sF4) = join(b,sF1),
inference(backward_demodulation,[],[f51572,f58694]) ).
fof(f58782,plain,
meet(complement(b),sF4) = meet(complement(b),join(b,sF1)),
inference(superposition,[],[f36747,f58725]) ).
fof(f58807,plain,
meet(complement(b),sF1) = meet(complement(b),sF4),
inference(forward_demodulation,[],[f58782,f36747]) ).
fof(f58824,plain,
meet(complement(b),sF3) = meet(complement(b),sF1),
inference(backward_demodulation,[],[f48642,f58807]) ).
fof(f58833,plain,
sF4 = join(sF2,meet(complement(b),sF1)),
inference(backward_demodulation,[],[f38825,f58824]) ).
fof(f58834,plain,
sF4 = join(sF1,sF2),
inference(backward_demodulation,[],[f38826,f58833]) ).
fof(f58841,plain,
sF4 = join(sF1,sF4),
inference(superposition,[],[f42,f58834]) ).
fof(f58893,plain,
sF1 = sF4,
inference(forward_demodulation,[],[f58841,f53772]) ).
fof(f58980,plain,
$false,
inference(forward_subsumption_resolution,[],[f58893,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT064-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 13:58:32 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 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
% 11.24/2.42 % (4007734)Input is clausal, will run a generic CNF schedule.
% 11.24/2.42 % (4007753)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1452347484:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.24/2.42 % (4007753)Instruction limit reached!
% 11.24/2.42 % (4007753)------------------------------
% 11.24/2.42 % (4007753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.24/2.42 % (4007753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.24/2.42 % (4007753)CaDiCaL version: 2.1.3
% 11.24/2.42 % (4007753)Termination reason: Instruction limit
% 11.24/2.42 % (4007753)Termination phase: Saturation
% 11.24/2.42 % (4007753)Time elapsed: 0.038 s
% 11.24/2.42 % (4007753)Peak memory usage: 89 MB
% 11.24/2.42 % (4007753)Instructions burned: 114 (million)
% 11.24/2.42 % (4007749)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=99017192:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.24/2.42 % (4007752)lrs+10_1_sil=8000:sp=occurrence:random_seed=1866256195:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.24/2.42 % (4007751)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2202734508:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.24/2.42 % (4007750)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1252818320:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.24/2.42 % (4007755)dis-21_1_sil=8000:lcm=predicate:random_seed=780437227: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)
% 11.24/2.42 % (4007754)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2640919607:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.24/2.42 % (4007755)Refutation not found, incomplete strategy
% 11.24/2.42 % (4007755)------------------------------
% 11.24/2.42 % (4007755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.24/2.42 % (4007755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.24/2.42 % (4007755)CaDiCaL version: 2.1.3
% 11.24/2.42 % (4007755)Termination reason: Refutation not found, incomplete strategy
% 11.24/2.42 % (4007755)Time elapsed: 0.002 s
% 11.24/2.42 % (4007755)Peak memory usage: 88 MB
% 11.24/2.42 % (4007755)Instructions burned: 1 (million)
% 11.24/2.42 % (4007752)Instruction limit reached!
% 11.24/2.42 % (4007752)------------------------------
% 11.24/2.42 % (4007752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.24/2.42 % (4007752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.24/2.42 % (4007752)CaDiCaL version: 2.1.3
% 11.24/2.42 % (4007752)Termination reason: Instruction limit
% 11.24/2.42 % (4007752)Termination phase: Saturation
% 11.24/2.42 % (4007752)Time elapsed: 0.063 s
% 11.24/2.42 % (4007752)Peak memory usage: 88 MB
% 11.24/2.42 % (4007752)Instructions burned: 107 (million)
% 11.24/2.42 % (4007754)Instruction limit reached!
% 11.24/2.42 % (4007754)------------------------------
% 11.24/2.42 % (4007754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.24/2.42 % (4007754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.24/2.42 % (4007754)CaDiCaL version: 2.1.3
% 11.24/2.42 % (4007754)Termination reason: Instruction limit
% 11.24/2.42 % (4007754)Termination phase: Saturation
% 11.24/2.42 % (4007754)Time elapsed: 0.102 s
% 11.24/2.42 % (4007754)Peak memory usage: 89 MB
% 11.24/2.42 % (4007754)Instructions burned: 182 (million)
% 11.24/2.42 % (4007761)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=510862284:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.24/2.42 % (4007761)Refutation not found, incomplete strategy
% 11.24/2.42 % (4007761)------------------------------
% 11.24/2.42 % (4007761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.24/2.42 % (4007761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.24/2.42 % (4007761)CaDiCaL version: 2.1.3
% 11.24/2.42 % (4007761)Termination reason: Refutation not found, incomplete strategy
% 11.24/2.42 % (4007761)Time elapsed: 0.001 s
% 11.24/2.42 % (4007761)Peak memory usage: 88 MB
% 11.24/2.42 % (4007764)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2209305313:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 20.25/3.75 % (4007764)Refutation not found, incomplete strategy
% 20.25/3.75 % (4007764)------------------------------
% 20.25/3.75 % (4007764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.75 % (4007764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.75 % (4007764)CaDiCaL version: 2.1.3
% 20.25/3.75 % (4007764)Termination reason: Refutation not found, incomplete strategy
% 20.25/3.75 % (4007764)Time elapsed: 0.002 s
% 20.25/3.75 % (4007764)Peak memory usage: 88 MB
% 20.25/3.75 % (4007764)Instructions burned: 1 (million)
% 20.25/3.75 % (4007755)------------------------------
% 20.25/3.75 % (4007755)------------------------------
% 20.25/3.75 % (4007761)------------------------------
% 20.25/3.75 % (4007761)------------------------------
% 20.25/3.75 % (4007765)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2024313047:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 20.25/3.75 % (4007765)Refutation not found, incomplete strategy
% 20.25/3.75 % (4007765)------------------------------
% 20.25/3.75 % (4007765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.75 % (4007765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.75 % (4007765)CaDiCaL version: 2.1.3
% 20.25/3.75 % (4007765)Termination reason: Refutation not found, incomplete strategy
% 20.25/3.75 % (4007765)Time elapsed: 0.001 s
% 20.25/3.75 % (4007765)Peak memory usage: 88 MB
% 20.25/3.75 % (4007768)lrs+10_64_to=lpo:sil=8000:random_seed=2123628723:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 20.25/3.75 % (4007770)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3080960774:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 20.25/3.75 % (4007764)------------------------------
% 20.25/3.75 % (4007764)------------------------------
% 20.25/3.75 % (4007768)Instruction limit reached!
% 20.25/3.75 % (4007768)------------------------------
% 20.25/3.75 % (4007768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.75 % (4007768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.75 % (4007768)CaDiCaL version: 2.1.3
% 20.25/3.75 % (4007768)Termination reason: Instruction limit
% 20.25/3.75 % (4007768)Termination phase: Saturation
% 20.25/3.75 % (4007768)Time elapsed: 0.072 s
% 20.25/3.75 % (4007768)Peak memory usage: 88 MB
% 20.25/3.75 % (4007768)Instructions burned: 128 (million)
% 20.25/3.75 % (4007765)------------------------------
% 20.25/3.75 % (4007765)------------------------------
% 20.25/3.75 % (4007770)Instruction limit reached!
% 20.25/3.75 % (4007770)------------------------------
% 20.25/3.75 % (4007770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.75 % (4007770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.75 % (4007770)CaDiCaL version: 2.1.3
% 20.25/3.75 % (4007770)Termination reason: Instruction limit
% 20.25/3.75 % (4007770)Termination phase: Saturation
% 20.25/3.75 % (4007770)Time elapsed: 0.082 s
% 20.25/3.75 % (4007770)Peak memory usage: 89 MB
% 20.25/3.75 % (4007770)Instructions burned: 196 (million)
% 20.25/3.75 % (4007773)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=738363850:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 20.25/3.75 % (4007775)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=3390817970:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 20.25/3.75 % (4007774)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4015688755:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 20.25/3.75 % (4007775)Instruction limit reached!
% 20.25/3.75 % (4007775)------------------------------
% 20.25/3.75 % (4007775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.25/3.75 % (4007775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.25/3.75 % (4007775)CaDiCaL version: 2.1.3
% 20.25/3.75 % (4007775)Termination reason: Instruction limit
% 20.25/3.75 % (4007775)Termination phase: Saturation
% 20.25/3.75 % (4007775)Time elapsed: 0.036 s
% 20.25/3.75 % (4007775)Peak memory usage: 89 MB
% 20.25/3.75 % (4007775)Instructions burned: 107 (million)
% 20.25/3.75 % (4007776)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1940697803:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 32.60/5.46 % (4007776)Refutation not found, incomplete strategy
% 32.60/5.46 % (4007776)------------------------------
% 32.60/5.46 % (4007776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.60/5.46 % (4007776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.60/5.46 % (4007776)CaDiCaL version: 2.1.3
% 32.60/5.46 % (4007776)Termination reason: Refutation not found, incomplete strategy
% 32.60/5.46 % (4007776)Time elapsed: 0.001 s
% 32.60/5.46 % (4007776)Peak memory usage: 87 MB
% 32.60/5.46 % (4007773)Instruction limit reached!
% 32.60/5.46 % (4007773)------------------------------
% 32.60/5.46 % (4007773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.60/5.46 % (4007773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.60/5.46 % (4007773)CaDiCaL version: 2.1.3
% 32.60/5.46 % (4007773)Termination reason: Instruction limit
% 32.60/5.46 % (4007773)Termination phase: Saturation
% 32.60/5.46 % (4007773)Time elapsed: 0.098 s
% 32.60/5.46 % (4007773)Peak memory usage: 90 MB
% 32.60/5.46 % (4007773)Instructions burned: 159 (million)
% 32.60/5.46 % (4007780)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4088368898:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 32.60/5.46 % (4007782)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=138670610:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 32.60/5.46 % (4007780)Instruction limit reached!
% 32.60/5.46 % (4007780)------------------------------
% 32.60/5.46 % (4007780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.60/5.46 % (4007780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.60/5.46 % (4007780)CaDiCaL version: 2.1.3
% 32.60/5.46 % (4007780)Termination reason: Instruction limit
% 32.60/5.46 % (4007780)Termination phase: Saturation
% 32.60/5.46 % (4007780)Time elapsed: 0.077 s
% 32.60/5.46 % (4007780)Peak memory usage: 90 MB
% 32.60/5.46 % (4007780)Instructions burned: 244 (million)
% 32.60/5.46 % (4007776)------------------------------
% 32.60/5.46 % (4007776)------------------------------
% 32.60/5.46 % (4007785)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3526012959:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 32.60/5.46 % (4007785)Instruction limit reached!
% 32.60/5.46 % (4007785)------------------------------
% 32.60/5.46 % (4007785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.60/5.46 % (4007785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.60/5.46 % (4007785)CaDiCaL version: 2.1.3
% 32.60/5.46 % (4007785)Termination reason: Instruction limit
% 32.60/5.46 % (4007785)Termination phase: Saturation
% 32.60/5.46 % (4007785)Time elapsed: 0.043 s
% 32.60/5.46 % (4007785)Peak memory usage: 89 MB
% 32.60/5.46 % (4007785)Instructions burned: 138 (million)
% 32.60/5.46 % (4007786)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1569465671:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 32.60/5.46 % (4007788)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2431721098:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 32.60/5.46 % (4007788)Instruction limit reached!
% 32.60/5.46 % (4007788)------------------------------
% 32.60/5.46 % (4007788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.60/5.46 % (4007788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.60/5.46 % (4007788)CaDiCaL version: 2.1.3
% 32.60/5.46 % (4007788)Termination reason: Instruction limit
% 32.60/5.46 % (4007788)Termination phase: Saturation
% 32.60/5.46 % (4007788)Time elapsed: 0.064 s
% 32.60/5.46 % (4007788)Peak memory usage: 91 MB
% 32.60/5.46 % (4007788)Instructions burned: 192 (million)
% 32.60/5.46 % (4007786)Instruction limit reached!
% 32.60/5.46 % (4007786)------------------------------
% 32.60/5.46 % (4007786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.60/5.46 % (4007786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.60/5.46 % (4007786)CaDiCaL version: 2.1.3
% 32.60/5.46 % (4007786)Termination reason: Instruction limit
% 32.60/5.46 % (4007786)Termination phase: Saturation
% 32.60/5.46 % (4007786)Time elapsed: 0.313 s
% 32.60/5.46 % (4007786)Peak memory usage: 94 MB
% 32.60/5.46 % (4007786)Instructions burned: 500 (million)
% 33.90/5.68 % (4007791)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=398571554:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 33.90/5.68 % (4007791)Instruction limit reached!
% 33.90/5.68 % (4007791)------------------------------
% 33.90/5.68 % (4007791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007791)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007791)Termination reason: Instruction limit
% 33.90/5.68 % (4007791)Termination phase: Saturation
% 33.90/5.68 % (4007791)Time elapsed: 0.085 s
% 33.90/5.68 % (4007791)Peak memory usage: 92 MB
% 33.90/5.68 % (4007791)Instructions burned: 264 (million)
% 33.90/5.68 % (4007793)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2170531312:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 33.90/5.68 % (4007794)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=4035076417:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 33.90/5.68 % (4007793)Instruction limit reached!
% 33.90/5.68 % (4007793)------------------------------
% 33.90/5.68 % (4007793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007793)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007793)Termination reason: Instruction limit
% 33.90/5.68 % (4007793)Termination phase: Saturation
% 33.90/5.68 % (4007793)Time elapsed: 0.094 s
% 33.90/5.68 % (4007793)Peak memory usage: 89 MB
% 33.90/5.68 % (4007793)Instructions burned: 157 (million)
% 33.90/5.68 % (4007797)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1212808129:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 33.90/5.68 % (4007797)Instruction limit reached!
% 33.90/5.68 % (4007797)------------------------------
% 33.90/5.68 % (4007797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007797)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007797)Termination reason: Instruction limit
% 33.90/5.68 % (4007797)Termination phase: Saturation
% 33.90/5.68 % (4007797)Time elapsed: 0.287 s
% 33.90/5.68 % (4007797)Peak memory usage: 91 MB
% 33.90/5.68 % (4007797)Instructions burned: 539 (million)
% 33.90/5.68 % (4007799)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2034167577:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 33.90/5.68 % (4007799)Instruction limit reached!
% 33.90/5.68 % (4007799)------------------------------
% 33.90/5.68 % (4007799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007799)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007799)Termination reason: Instruction limit
% 33.90/5.68 % (4007799)Termination phase: Saturation
% 33.90/5.68 % (4007799)Time elapsed: 0.101 s
% 33.90/5.68 % (4007799)Peak memory usage: 88 MB
% 33.90/5.68 % (4007799)Instructions burned: 182 (million)
% 33.90/5.68 % (4007801)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=3786146690:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 33.90/5.68 % (4007774)Instruction limit reached!
% 33.90/5.68 % (4007774)------------------------------
% 33.90/5.68 % (4007774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007774)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007774)Termination reason: Instruction limit
% 33.90/5.68 % (4007774)Termination phase: Saturation
% 33.90/5.68 % (4007774)Time elapsed: 2.072 s
% 33.90/5.68 % (4007774)Peak memory usage: 151 MB
% 33.90/5.68 % (4007774)Instructions burned: 3395 (million)
% 33.90/5.68 % (4007794)Instruction limit reached!
% 33.90/5.68 % (4007794)------------------------------
% 33.90/5.68 % (4007794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007794)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007794)Termination reason: Instruction limit
% 33.90/5.68 % (4007794)Termination phase: Saturation
% 33.90/5.68 % (4007794)Time elapsed: 1.103 s
% 33.90/5.68 % (4007794)Peak memory usage: 150 MB
% 33.90/5.68 % (4007794)Instructions burned: 3258 (million)
% 33.90/5.68 % (4007804)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=3774658363:s2pl=no:i=8478:s2at=4:nm=6_2970 on theBenchmark for (2970ds/8478Mi)
% 33.90/5.68 % (4007803)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=2017264913:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 33.90/5.68 % (4007803)Instruction limit reached!
% 33.90/5.68 % (4007803)------------------------------
% 33.90/5.68 % (4007803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007803)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007803)Termination reason: Instruction limit
% 33.90/5.68 % (4007803)Termination phase: Saturation
% 33.90/5.68 % (4007803)Time elapsed: 0.241 s
% 33.90/5.68 % (4007803)Peak memory usage: 94 MB
% 33.90/5.68 % (4007803)Instructions burned: 412 (million)
% 33.90/5.68 % (4007807)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=1668953858:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2967 on theBenchmark for (2967ds/303Mi)
% 33.90/5.68 % (4007807)Refutation not found, incomplete strategy
% 33.90/5.68 % (4007807)------------------------------
% 33.90/5.68 % (4007807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007807)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007807)Termination reason: Refutation not found, incomplete strategy
% 33.90/5.68 % (4007807)Time elapsed: 0.002 s
% 33.90/5.68 % (4007807)Peak memory usage: 88 MB
% 33.90/5.68 % (4007807)Instructions burned: 1 (million)
% 33.90/5.68 % (4007807)------------------------------
% 33.90/5.68 % (4007807)------------------------------
% 33.90/5.68 % (4007809)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2720206858:st=4:i=720:sd=3:fsr=off:ss=axioms_2963 on theBenchmark for (2963ds/720Mi)
% 33.90/5.68 % (4007809)Refutation not found, incomplete strategy
% 33.90/5.68 % (4007809)------------------------------
% 33.90/5.68 % (4007809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007809)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007809)Termination reason: Refutation not found, incomplete strategy
% 33.90/5.68 % (4007809)Time elapsed: 0.001 s
% 33.90/5.68 % (4007809)Peak memory usage: 88 MB
% 33.90/5.68 % (4007809)------------------------------
% 33.90/5.68 % (4007809)------------------------------
% 33.90/5.68 % (4007782)Instruction limit reached!
% 33.90/5.68 % (4007782)------------------------------
% 33.90/5.68 % (4007782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007782)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007782)Termination reason: Instruction limit
% 33.90/5.68 % (4007782)Termination phase: Saturation
% 33.90/5.68 % (4007782)Time elapsed: 3.078 s
% 33.90/5.68 % (4007782)Peak memory usage: 169 MB
% 33.90/5.68 % (4007782)Instructions burned: 5210 (million)
% 33.90/5.68 % (4007811)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=783177518:i=598:bs=on:bd=preordered:av=off:ss=axioms_2959 on theBenchmark for (2959ds/598Mi)
% 33.90/5.68 % (4007812)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3052320009:i=2989:sd=3:ss=axioms:sgt=60_2958 on theBenchmark for (2958ds/2989Mi)
% 33.90/5.68 % (4007751)First to succeed.
% 33.90/5.68 % (4007751)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4007734"
% 33.90/5.68 % (4007811)Instruction limit reached!
% 33.90/5.68 % (4007811)------------------------------
% 33.90/5.68 % (4007811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.90/5.68 % (4007811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.90/5.68 % (4007811)CaDiCaL version: 2.1.3
% 33.90/5.68 % (4007811)Termination reason: Instruction limit
% 33.90/5.68 % (4007811)Termination phase: Saturation
% 33.90/5.68 % (4007811)Time elapsed: 0.369 s
% 33.90/5.68 % (4007811)Peak memory usage: 94 MB
% 33.90/5.68 % (4007811)Instructions burned: 599 (million)
% 33.90/5.68 % (4007815)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=2524935275:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2953 on theBenchmark for (2953ds/1997Mi)
% 33.90/5.68 % (4007751)Refutation found. Thanks to Tanya!
% 33.90/5.68 % SZS status Unsatisfiable for theBenchmark
% 33.90/5.68 % SZS output start Proof for theBenchmark
% See solution above
% 34.68/5.87 % (4007751)------------------------------
% 34.68/5.87 % (4007751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.68/5.87 % (4007751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.68/5.87 % (4007751)CaDiCaL version: 2.1.3
% 34.68/5.87 % (4007751)Termination reason: Refutation
% 34.68/5.87 % (4007751)Time elapsed: 4.387 s
% 34.68/5.87 % (4007751)Peak memory usage: 174 MB
% 34.68/5.87 % (4007751)Instructions burned: 6971 (million)
% 34.68/5.87 % (4007751)------------------------------
% 34.68/5.87 % (4007751)------------------------------
% 34.68/5.87 % (4007734)Success in time 4.827 s
% 34.68/5.87 % Vampire exiting
%------------------------------------------------------------------------------