%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT185-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:10 AM UTC 2026
% Result : Unsatisfiable 34.63s 9.04s
% Output : Refutation 55.34s
% 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)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X0,meet(X1,X2))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H10) ).
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) != one
| meet(X1,X0) != zero
| 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(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f166,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f167,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f173,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f32,f166]) ).
fof(f175,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f166]) ).
fof(f178,plain,
! [X0,X1] : one = join(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f164,f173]) ).
fof(f189,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f34,f175]) ).
fof(f243,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f245,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f246,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f300,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f34,f245]) ).
fof(f302,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f245]) ).
fof(f305,plain,
! [X0,X1] : zero = 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,zero)))),
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,one))),
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,one) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f75,f9]) ).
fof(f1063,plain,
! [X0,X1] : one = 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] : zero = 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,zero))),
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,zero),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] : zero = 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] :
( one != one
| zero != 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] :
( zero != 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(one,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] : one = 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(one,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] : one = 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(zero,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(zero,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] :
( one != one
| zero != meet(join(X1,complement(join(X0,X1))),X0)
| complement(join(X1,complement(join(X0,X1)))) = X0 ),
inference(superposition,[],[f58,f167]) ).
fof(f7784,plain,
! [X0] :
( one != one
| zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f58,f9]) ).
fof(f7804,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f7784]) ).
fof(f7807,plain,
! [X0,X1] :
( zero != 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)) != zero
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f7804,f5]) ).
fof(f7824,plain,
! [X0,X1] :
( zero != 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] :
( one != one
| zero != 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] :
( zero != 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] :
( one != one
| zero != 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] :
( zero != 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
| zero != 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) != zero ),
inference(backward_demodulation,[],[f23500,f24200]) ).
fof(f24440,plain,
! [X0,X1] :
( complement(X0) = join(X1,complement(join(X0,X1)))
| meet(X0,X1) != zero ),
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))))
| zero != 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))))
| zero != 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))
| zero != 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))
| zero != 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))))
| zero != 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))))
| zero != 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
| zero != 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
| zero != meet(complement(X0),meet(X1,X0)) ),
inference(forward_demodulation,[],[f27814,f7835]) ).
fof(f27892,plain,
! [X0,X1] :
( zero != 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] :
( zero != 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
| zero != 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),zero)),
inference(forward_demodulation,[],[f36576,f1085]) ).
fof(f36972,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),join(complement(X0),zero)),
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(zero,complement(X0))),
inference(forward_demodulation,[],[f36971,f2804]) ).
fof(f37278,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(join(X0,X1),join(zero,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.05 % Problem : LAT185-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.50 % Computer : n004.cluster.edu
% 0.25/0.50 % Model : x86_64 x86_64
% 0.25/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/0.50 % Memory : 8046.5625MB
% 0.25/0.50 % OS : Linux 6.8.0-71-generic
% 0.25/0.50 % CPULimit : 300
% 0.25/0.50 % WCLimit : 300
% 0.25/0.50 % DateTime : Sun Sep 27 14:05:22 UTC 2026
% 0.25/0.50 % CPUTime :
% 0.25/0.50 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.28/0.56 Running first-order theorem proving
% 0.28/0.56 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.41/4.48 % (3550364)Input is clausal, will run a generic CNF schedule.
% 22.41/4.48 % (3550371)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=591775149:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 22.41/4.48 % (3550369)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=2528964287:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 22.41/4.48 % (3550370)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4075087651:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 22.41/4.48 % (3550374)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3405610583:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 22.41/4.48 % (3550373)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1383806210:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 22.41/4.48 % (3550372)lrs+10_1_sil=8000:sp=occurrence:random_seed=4207669617:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 22.41/4.48 % (3550375)dis-21_1_sil=8000:lcm=predicate:random_seed=2716319872:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 22.41/4.48 % (3550375)Refutation not found, incomplete strategy
% 22.41/4.48 % (3550375)------------------------------
% 22.41/4.48 % (3550375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.48 % (3550375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.48 % (3550375)CaDiCaL version: 2.1.3
% 22.41/4.48 % (3550375)Termination reason: Refutation not found, incomplete strategy
% 22.41/4.48 % (3550375)Time elapsed: 0.003 s
% 22.41/4.48 % (3550375)Peak memory usage: 88 MB
% 22.41/4.48 % (3550375)Instructions burned: 1 (million)
% 22.41/4.48 % (3550372)Instruction limit reached!
% 22.41/4.48 % (3550372)------------------------------
% 22.41/4.48 % (3550372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.48 % (3550372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.48 % (3550372)CaDiCaL version: 2.1.3
% 22.41/4.48 % (3550372)Termination reason: Instruction limit
% 22.41/4.48 % (3550372)Termination phase: Saturation
% 22.41/4.48 % (3550372)Time elapsed: 0.105 s
% 22.41/4.48 % (3550372)Peak memory usage: 88 MB
% 22.41/4.48 % (3550372)Instructions burned: 108 (million)
% 22.41/4.48 % (3550373)Instruction limit reached!
% 22.41/4.48 % (3550373)------------------------------
% 22.41/4.48 % (3550373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.48 % (3550373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.48 % (3550373)CaDiCaL version: 2.1.3
% 22.41/4.48 % (3550373)Termination reason: Instruction limit
% 22.41/4.48 % (3550373)Termination phase: Saturation
% 22.41/4.48 % (3550373)Time elapsed: 0.112 s
% 22.41/4.48 % (3550373)Peak memory usage: 88 MB
% 22.41/4.48 % (3550373)Instructions burned: 114 (million)
% 22.41/4.48 % (3550374)Instruction limit reached!
% 22.41/4.48 % (3550374)------------------------------
% 22.41/4.48 % (3550374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.48 % (3550374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.48 % (3550374)CaDiCaL version: 2.1.3
% 22.41/4.48 % (3550374)Termination reason: Instruction limit
% 22.41/4.48 % (3550374)Termination phase: Saturation
% 22.41/4.48 % (3550374)Time elapsed: 0.173 s
% 22.41/4.48 % (3550374)Peak memory usage: 89 MB
% 22.41/4.48 % (3550374)Instructions burned: 181 (million)
% 22.41/4.48 % (3550384)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4199072065:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 22.41/4.48 % (3550384)Refutation not found, incomplete strategy
% 22.41/4.48 % (3550384)------------------------------
% 22.41/4.48 % (3550384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.41/4.48 % (3550384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.41/4.48 % (3550384)CaDiCaL version: 2.1.3
% 22.41/4.48 % (3550384)Termination reason: Refutation not found, incomplete strategy
% 22.41/4.48 % (3550384)Time elapsed: 0.003 s
% 22.41/4.48 % (3550384)Peak memory usage: 88 MB
% 22.41/4.48 % (3550384)Instructions burned: 1 (million)
% 40.16/7.16 % (3550383)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=3064592307:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 40.16/7.16 % (3550383)Refutation not found, incomplete strategy
% 40.16/7.16 % (3550383)------------------------------
% 40.16/7.16 % (3550383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.16/7.16 % (3550383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.16/7.16 % (3550383)CaDiCaL version: 2.1.3
% 40.16/7.16 % (3550383)Termination reason: Refutation not found, incomplete strategy
% 40.16/7.16 % (3550383)Time elapsed: 0.003 s
% 40.16/7.16 % (3550383)Peak memory usage: 88 MB
% 40.16/7.16 % (3550375)------------------------------
% 40.16/7.16 % (3550375)------------------------------
% 40.16/7.16 % (3550385)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3032977417:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 40.16/7.16 % (3550385)Refutation not found, incomplete strategy
% 40.16/7.16 % (3550385)------------------------------
% 40.16/7.16 % (3550385)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.16/7.16 % (3550385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.16/7.16 % (3550385)CaDiCaL version: 2.1.3
% 40.16/7.16 % (3550385)Termination reason: Refutation not found, incomplete strategy
% 40.16/7.16 % (3550385)Time elapsed: 0.002 s
% 40.16/7.16 % (3550385)Peak memory usage: 88 MB
% 40.16/7.16 % (3550388)lrs+10_64_to=lpo:sil=8000:random_seed=3699323667:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 40.16/7.16 % (3550384)------------------------------
% 40.16/7.16 % (3550384)------------------------------
% 40.16/7.16 % (3550383)------------------------------
% 40.16/7.16 % (3550383)------------------------------
% 40.16/7.16 % (3550385)------------------------------
% 40.16/7.16 % (3550385)------------------------------
% 40.16/7.16 % (3550388)Instruction limit reached!
% 40.16/7.16 % (3550388)------------------------------
% 40.16/7.16 % (3550388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.16/7.16 % (3550388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.16/7.16 % (3550388)CaDiCaL version: 2.1.3
% 40.16/7.16 % (3550388)Termination reason: Instruction limit
% 40.16/7.16 % (3550388)Termination phase: Saturation
% 40.16/7.16 % (3550388)Time elapsed: 0.125 s
% 40.16/7.16 % (3550388)Peak memory usage: 88 MB
% 40.16/7.16 % (3550388)Instructions burned: 126 (million)
% 40.16/7.16 % (3550391)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=282752555:avsq=on:i=194:fgj=on:bd=preordered_2988 on theBenchmark for (2988ds/194Mi)
% 40.16/7.16 % (3550392)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3995988207:i=157:gtg=all_2988 on theBenchmark for (2988ds/157Mi)
% 40.16/7.16 % (3550394)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=3465596352:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 40.16/7.16 % (3550393)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=721729881:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 40.16/7.16 % (3550394)Instruction limit reached!
% 40.16/7.16 % (3550394)------------------------------
% 40.16/7.16 % (3550394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.16/7.16 % (3550394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.16/7.16 % (3550394)CaDiCaL version: 2.1.3
% 40.16/7.16 % (3550394)Termination reason: Instruction limit
% 40.16/7.16 % (3550394)Termination phase: Saturation
% 40.16/7.16 % (3550394)Time elapsed: 0.115 s
% 40.16/7.16 % (3550394)Peak memory usage: 89 MB
% 40.16/7.16 % (3550394)Instructions burned: 107 (million)
% 40.16/7.16 % (3550392)Instruction limit reached!
% 40.16/7.16 % (3550392)------------------------------
% 40.16/7.16 % (3550392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.16/7.16 % (3550392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.16/7.16 % (3550392)CaDiCaL version: 2.1.3
% 40.16/7.16 % (3550392)Termination reason: Instruction limit
% 40.16/7.16 % (3550392)Termination phase: Saturation
% 40.16/7.16 % (3550392)Time elapsed: 0.162 s
% 40.16/7.16 % (3550392)Peak memory usage: 90 MB
% 40.16/7.16 % (3550392)Instructions burned: 157 (million)
% 40.16/7.16 % (3550391)Instruction limit reached!
% 40.16/7.16 % (3550391)------------------------------
% 34.63/9.04 % (3550391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550391)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550391)Termination reason: Instruction limit
% 34.63/9.04 % (3550391)Termination phase: Saturation
% 34.63/9.04 % (3550391)Time elapsed: 0.196 s
% 34.63/9.04 % (3550391)Peak memory usage: 89 MB
% 34.63/9.04 % (3550391)Instructions burned: 194 (million)
% 34.63/9.04 % (3550400)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2052079252:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2984 on theBenchmark for (2984ds/242Mi)
% 34.63/9.04 % (3550399)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2291044239:i=107_2984 on theBenchmark for (2984ds/107Mi)
% 34.63/9.04 % (3550399)Refutation not found, incomplete strategy
% 34.63/9.04 % (3550399)------------------------------
% 34.63/9.04 % (3550399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550399)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550399)Termination reason: Refutation not found, incomplete strategy
% 34.63/9.04 % (3550399)Time elapsed: 0.002 s
% 34.63/9.04 % (3550399)Peak memory usage: 87 MB
% 34.63/9.04 % (3550401)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=152717800:cond=fast:i=5208:av=off_2983 on theBenchmark for (2983ds/5208Mi)
% 34.63/9.04 % (3550400)Instruction limit reached!
% 34.63/9.04 % (3550400)------------------------------
% 34.63/9.04 % (3550400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550400)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550400)Termination reason: Instruction limit
% 34.63/9.04 % (3550400)Termination phase: Saturation
% 34.63/9.04 % (3550400)Time elapsed: 0.251 s
% 34.63/9.04 % (3550400)Peak memory usage: 90 MB
% 34.63/9.04 % (3550400)Instructions burned: 243 (million)
% 34.63/9.04 % (3550399)------------------------------
% 34.63/9.04 % (3550399)------------------------------
% 34.63/9.04 % (3550405)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2813939838:i=134:sd=2:doe=on:ss=axioms:sgt=14_2978 on theBenchmark for (2978ds/134Mi)
% 34.63/9.04 % (3550406)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3263862011:i=499:bd=all_2977 on theBenchmark for (2977ds/499Mi)
% 34.63/9.04 % (3550405)Instruction limit reached!
% 34.63/9.04 % (3550405)------------------------------
% 34.63/9.04 % (3550405)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550405)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550405)Termination reason: Instruction limit
% 34.63/9.04 % (3550405)Termination phase: Saturation
% 34.63/9.04 % (3550405)Time elapsed: 0.134 s
% 34.63/9.04 % (3550405)Peak memory usage: 89 MB
% 34.63/9.04 % (3550405)Instructions burned: 134 (million)
% 34.63/9.04 % (3550409)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=45580963:i=191:fgj=on:bd=all_2974 on theBenchmark for (2974ds/191Mi)
% 34.63/9.04 % (3550406)Instruction limit reached!
% 34.63/9.04 % (3550406)------------------------------
% 34.63/9.04 % (3550406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550406)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550406)Termination reason: Instruction limit
% 34.63/9.04 % (3550406)Termination phase: Saturation
% 34.63/9.04 % (3550406)Time elapsed: 0.522 s
% 34.63/9.04 % (3550406)Peak memory usage: 94 MB
% 34.63/9.04 % (3550406)Instructions burned: 499 (million)
% 34.63/9.04 % (3550409)Instruction limit reached!
% 34.63/9.04 % (3550409)------------------------------
% 34.63/9.04 % (3550409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550409)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550409)Termination reason: Instruction limit
% 34.63/9.04 % (3550409)Termination phase: Saturation
% 34.63/9.04 % (3550409)Time elapsed: 0.203 s
% 34.63/9.04 % (3550409)Peak memory usage: 91 MB
% 34.63/9.04 % (3550409)Instructions burned: 191 (million)
% 34.63/9.04 % (3550411)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3654260722:i=264:kws=precedence:fsr=off_2968 on theBenchmark for (2968ds/264Mi)
% 34.63/9.04 % (3550412)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1183445912:cond=on:i=156:bs=on:gtg=exists_all:er=known_2968 on theBenchmark for (2968ds/156Mi)
% 34.63/9.04 % (3550412)Instruction limit reached!
% 34.63/9.04 % (3550412)------------------------------
% 34.63/9.04 % (3550412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550412)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550412)Termination reason: Instruction limit
% 34.63/9.04 % (3550412)Termination phase: Saturation
% 34.63/9.04 % (3550412)Time elapsed: 0.160 s
% 34.63/9.04 % (3550412)Peak memory usage: 89 MB
% 34.63/9.04 % (3550412)Instructions burned: 156 (million)
% 34.63/9.04 % (3550411)Instruction limit reached!
% 34.63/9.04 % (3550411)------------------------------
% 34.63/9.04 % (3550411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550411)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550411)Termination reason: Instruction limit
% 34.63/9.04 % (3550411)Termination phase: Saturation
% 34.63/9.04 % (3550411)Time elapsed: 0.262 s
% 34.63/9.04 % (3550411)Peak memory usage: 91 MB
% 34.63/9.04 % (3550411)Instructions burned: 264 (million)
% 34.63/9.04 % (3550415)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=1679970724:i=3256:kws=precedence:bd=preordered:av=off_2963 on theBenchmark for (2963ds/3256Mi)
% 34.63/9.04 % (3550416)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=986064373:i=537:av=off:ss=included_2962 on theBenchmark for (2962ds/537Mi)
% 34.63/9.04 % (3550416)Instruction limit reached!
% 34.63/9.04 % (3550416)------------------------------
% 34.63/9.04 % (3550416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550416)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550416)Termination reason: Instruction limit
% 34.63/9.04 % (3550416)Termination phase: Saturation
% 34.63/9.04 % (3550416)Time elapsed: 0.509 s
% 34.63/9.04 % (3550416)Peak memory usage: 93 MB
% 34.63/9.04 % (3550416)Instructions burned: 537 (million)
% 34.63/9.04 % (3550419)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1266955708:i=180:bd=preordered:av=off_2954 on theBenchmark for (2954ds/180Mi)
% 34.63/9.04 % (3550419)Instruction limit reached!
% 34.63/9.04 % (3550419)------------------------------
% 34.63/9.04 % (3550419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550419)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550419)Termination reason: Instruction limit
% 34.63/9.04 % (3550419)Termination phase: Saturation
% 34.63/9.04 % (3550419)Time elapsed: 0.176 s
% 34.63/9.04 % (3550419)Peak memory usage: 88 MB
% 34.63/9.04 % (3550419)Instructions burned: 183 (million)
% 34.63/9.04 % (3550393)Instruction limit reached!
% 34.63/9.04 % (3550393)------------------------------
% 34.63/9.04 % (3550393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550393)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550393)Termination reason: Instruction limit
% 34.63/9.04 % (3550393)Termination phase: Saturation
% 34.63/9.04 % (3550393)Time elapsed: 3.634 s
% 34.63/9.04 % (3550393)Peak memory usage: 151 MB
% 34.63/9.04 % (3550393)Instructions burned: 3394 (million)
% 34.63/9.04 % (3550421)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=1946407285:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2949 on theBenchmark for (2949ds/10307Mi)
% 34.63/9.04 % (3550422)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=79491466:i=412:gtgl=4:gtg=exists_all_2948 on theBenchmark for (2948ds/412Mi)
% 34.63/9.04 % (3550422)Instruction limit reached!
% 34.63/9.04 % (3550422)------------------------------
% 34.63/9.04 % (3550422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550422)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550422)Termination reason: Instruction limit
% 34.63/9.04 % (3550422)Termination phase: Saturation
% 34.63/9.04 % (3550422)Time elapsed: 0.410 s
% 34.63/9.04 % (3550422)Peak memory usage: 94 MB
% 34.63/9.04 % (3550422)Instructions burned: 412 (million)
% 34.63/9.04 % (3550425)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=339266392:s2pl=no:i=8478:s2at=4:nm=6_2941 on theBenchmark for (2941ds/8478Mi)
% 34.63/9.04 % (3550371)First to succeed.
% 34.63/9.04 % (3550371)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3550364"
% 34.63/9.04 % (3550401)Instruction limit reached!
% 34.63/9.04 % (3550401)------------------------------
% 34.63/9.04 % (3550401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550401)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550401)Termination reason: Instruction limit
% 34.63/9.04 % (3550401)Termination phase: Saturation
% 34.63/9.04 % (3550401)Time elapsed: 5.471 s
% 34.63/9.04 % (3550401)Peak memory usage: 169 MB
% 34.63/9.04 % (3550401)Instructions burned: 5209 (million)
% 34.63/9.04 % (3550415)Instruction limit reached!
% 34.63/9.04 % (3550415)------------------------------
% 34.63/9.04 % (3550415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.63/9.04 % (3550415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.63/9.04 % (3550415)CaDiCaL version: 2.1.3
% 34.63/9.04 % (3550415)Termination reason: Instruction limit
% 34.63/9.04 % (3550415)Termination phase: Saturation
% 34.63/9.04 % (3550415)Time elapsed: 3.486 s
% 34.63/9.04 % (3550415)Peak memory usage: 150 MB
% 34.63/9.04 % (3550415)Instructions burned: 3257 (million)
% 34.63/9.04 % (3550371)Refutation found. Thanks to Tanya!
% 34.63/9.04 % SZS status Unsatisfiable for theBenchmark
% 34.63/9.04 % SZS output start Proof for theBenchmark
% See solution above
% 55.34/9.44 % (3550371)------------------------------
% 55.34/9.44 % (3550371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 55.34/9.44 % (3550371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 55.34/9.44 % (3550371)CaDiCaL version: 2.1.3
% 55.34/9.44 % (3550371)Termination reason: Refutation
% 55.34/9.44 % (3550371)Time elapsed: 6.990 s
% 55.34/9.44 % (3550371)Peak memory usage: 175 MB
% 55.34/9.44 % (3550371)Instructions burned: 6970 (million)
% 55.34/9.44 % (3550371)------------------------------
% 55.34/9.44 % (3550371)------------------------------
% 55.34/9.44 % (3550364)Success in time 7.708 s
% 55.34/9.44 % Vampire exiting
%------------------------------------------------------------------------------