%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT188-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:11 AM UTC 2026
% Result : Unsatisfiable 52.55s 8.74s
% Output : Refutation 53.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 92
% Number of leaves : 16
% Syntax : Number of formulae : 412 ( 378 unt; 5 def)
% Number of atoms : 453 ( 452 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 84 ( 43 ~; 41 |; 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 : 909 ( 909 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(X1,meet(X2,join(X0,X1)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H16) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox/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(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(f35,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f32,f3]) ).
fof(f38,plain,
a = join(a,sF2),
inference(superposition,[],[f32,f25]) ).
fof(f39,plain,
a = join(a,sF3),
inference(superposition,[],[f32,f26]) ).
fof(f41,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f35,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(f53,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f54,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f32]) ).
fof(f65,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(X1,X2))) = X2,
inference(superposition,[],[f34,f8]) ).
fof(f67,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f76,plain,
! [X0,X1] :
( join(X0,X1) != one
| meet(X1,X0) != zero
| complement(X1) = X0 ),
inference(superposition,[],[f11,f6]) ).
fof(f94,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f95,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f34]) ).
fof(f97,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f108,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f109,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f141,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f94,f5]) ).
fof(f145,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f32,f94]) ).
fof(f149,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f145,f6]) ).
fof(f159,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f160,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(one,X1),
inference(superposition,[],[f8,f9]) ).
fof(f163,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f169,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),meet(X1,X2))) = meet(X1,join(meet(X0,X1),meet(X2,join(X0,meet(X2,join(X1,X0)))))),
inference(superposition,[],[f12,f5]) ).
fof(f175,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,meet(X0,X1)),meet(X0,X2))) = meet(X0,join(meet(X0,meet(X0,X1)),meet(X2,join(meet(X0,X1),meet(X2,X0))))),
inference(superposition,[],[f12,f4]) ).
fof(f178,plain,
! [X2,X0,X1] : meet(X1,join(meet(X1,X0),meet(X1,X2))) = meet(X1,join(meet(X1,X0),meet(X2,join(X0,meet(X2,join(X0,X1)))))),
inference(superposition,[],[f12,f6]) ).
fof(f187,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(X1,meet(join(X0,X1),X2))))),
inference(superposition,[],[f12,f5]) ).
fof(f214,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(meet(X0,X1),meet(X2,X0))))),
inference(forward_demodulation,[],[f175,f52]) ).
fof(f249,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f250,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f251,plain,
! [X0,X1] : meet(X0,complement(join(X0,X1))) = meet(X0,zero),
inference(superposition,[],[f94,f10]) ).
fof(f260,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f249]) ).
fof(f286,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f32,f260]) ).
fof(f287,plain,
! [X0,X1] : meet(X1,join(meet(X1,zero),meet(X1,X0))) = meet(X1,join(meet(X1,zero),meet(X0,meet(X0,join(X1,zero))))),
inference(superposition,[],[f12,f260]) ).
fof(f289,plain,
! [X0,X1] : meet(X1,join(meet(X1,zero),meet(X1,X0))) = meet(X1,join(meet(X1,zero),meet(X0,join(X1,zero)))),
inference(forward_demodulation,[],[f287,f52]) ).
fof(f292,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(backward_demodulation,[],[f251,f286]) ).
fof(f297,plain,
! [X0,X1] : meet(X1,join(meet(X1,zero),meet(X1,X0))) = meet(X1,join(meet(X1,zero),meet(X0,X1))),
inference(forward_demodulation,[],[f289,f249]) ).
fof(f300,plain,
! [X0,X1] : meet(X1,join(zero,meet(X1,X0))) = meet(X1,join(zero,meet(X0,X1))),
inference(forward_demodulation,[],[f297,f286]) ).
fof(f302,plain,
! [X0,X1] : meet(X1,join(zero,meet(X1,X0))) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f300,f260]) ).
fof(f303,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(zero,meet(X1,X0))),
inference(forward_demodulation,[],[f302,f51]) ).
fof(f304,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,meet(X1,X0)),
inference(forward_demodulation,[],[f303,f260]) ).
fof(f340,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f32,f304]) ).
fof(f401,plain,
! [X0,X1] : zero = meet(X1,complement(join(X0,X1))),
inference(superposition,[],[f292,f6]) ).
fof(f431,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f159]) ).
fof(f434,plain,
! [X0] : one = join(one,X0),
inference(superposition,[],[f32,f159]) ).
fof(f440,plain,
! [X0,X1] : one = join(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f160,f434]) ).
fof(f461,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f34,f431]) ).
fof(f570,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f53,f6]) ).
fof(f574,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f53,f9]) ).
fof(f583,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f34,f53]) ).
fof(f590,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f583,f5]) ).
fof(f595,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f574,f461]) ).
fof(f708,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,complement(meet(X0,X1))),meet(X0,X2))) = meet(X0,join(meet(X0,complement(meet(X0,X1))),meet(X2,join(complement(meet(X0,X1)),meet(X2,one))))),
inference(superposition,[],[f12,f595]) ).
fof(f721,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,complement(meet(X0,X1))),meet(X0,X2))) = meet(X0,join(meet(X0,complement(meet(X0,X1))),meet(X2,join(complement(meet(X0,X1)),X2)))),
inference(forward_demodulation,[],[f708,f159]) ).
fof(f730,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,complement(meet(X0,X1))),meet(X0,X2))) = meet(X0,join(meet(X0,complement(meet(X0,X1))),X2)),
inference(forward_demodulation,[],[f721,f34]) ).
fof(f747,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f95,f5]) ).
fof(f812,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f54,f304]) ).
fof(f826,plain,
! [X0] : join(a,X0) = join(a,join(sF2,X0)),
inference(superposition,[],[f54,f25]) ).
fof(f831,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f54,f6]) ).
fof(f939,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X1)) = join(meet(X1,X0),meet(X2,meet(X0,X1))),
inference(superposition,[],[f812,f32]) ).
fof(f942,plain,
! [X0,X1] : join(meet(X0,X1),one) = join(meet(X0,X1),complement(meet(X1,X0))),
inference(superposition,[],[f812,f9]) ).
fof(f963,plain,
! [X0,X1] : join(meet(X0,X1),complement(meet(X1,X0))) = join(one,meet(X0,X1)),
inference(forward_demodulation,[],[f942,f6]) ).
fof(f966,plain,
! [X2,X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f939,f340]) ).
fof(f1002,plain,
! [X0,X1] : one = join(meet(X0,X1),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f963,f434]) ).
fof(f1061,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f250,f5]) ).
fof(f1186,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,f163]) ).
fof(f1199,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1186]) ).
fof(f1296,plain,
! [X0,X1] :
( one != one
| zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(superposition,[],[f11,f1002]) ).
fof(f1304,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f1296]) ).
fof(f1311,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f1304,f7]) ).
fof(f1353,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f1311,f1061]) ).
fof(f1550,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X3,X0)) = meet(X2,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f95,f108]) ).
fof(f3568,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X2,join(X3,meet(X0,X1))))),
inference(superposition,[],[f7,f747]) ).
fof(f3584,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X2,join(X3,meet(X0,X1))))),
inference(forward_demodulation,[],[f3568,f7]) ).
fof(f3896,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,join(complement(X0),X1)),meet(X0,X2))) = meet(X0,join(meet(X0,join(complement(X0),X1)),meet(X2,join(join(complement(X0),X1),meet(X2,one))))),
inference(superposition,[],[f12,f440]) ).
fof(f3931,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,join(complement(X0),X1)),meet(X0,X2))) = meet(X0,join(meet(X0,join(complement(X0),X1)),meet(X2,join(complement(X0),join(X1,meet(X2,one)))))),
inference(forward_demodulation,[],[f3896,f8]) ).
fof(f3943,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,join(complement(X0),X1)),meet(X0,X2))) = meet(X0,join(meet(X0,join(complement(X0),X1)),meet(X2,join(complement(X0),join(X1,X2))))),
inference(forward_demodulation,[],[f3931,f159]) ).
fof(f3949,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,join(complement(X0),X1)),meet(X0,X2))) = meet(X0,join(meet(X0,join(complement(X0),X1)),X2)),
inference(forward_demodulation,[],[f3943,f65]) ).
fof(f4367,plain,
! [X0] :
( one != one
| zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f76,f9]) ).
fof(f4389,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f4367]) ).
fof(f4404,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f4389,f5]) ).
fof(f4422,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f4404,f10]) ).
fof(f4958,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X0,X1))),zero)) = meet(X0,join(meet(X0,complement(meet(X0,X1))),complement(X0))),
inference(superposition,[],[f730,f10]) ).
fof(f5064,plain,
! [X0,X1] : meet(X0,join(meet(X0,complement(meet(X0,X1))),zero)) = meet(X0,join(complement(X0),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4958,f6]) ).
fof(f5132,plain,
! [X0,X1] : meet(X0,join(zero,meet(X0,complement(meet(X0,X1))))) = meet(X0,join(complement(X0),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f5064,f6]) ).
fof(f5174,plain,
! [X0,X1] : meet(X0,meet(X0,complement(meet(X0,X1)))) = meet(X0,join(complement(X0),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f5132,f260]) ).
fof(f5207,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(X0,join(complement(X0),meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f5174,f52]) ).
fof(f5425,plain,
! [X2,X0,X1] : meet(meet(X0,complement(meet(X0,X1))),X2) = meet(join(complement(X0),meet(X0,complement(meet(X0,X1)))),meet(X0,X2)),
inference(superposition,[],[f97,f5207]) ).
fof(f5522,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X2,meet(X1,X0)))),
inference(superposition,[],[f34,f97]) ).
fof(f5615,plain,
! [X2,X0,X1] : meet(meet(X0,complement(meet(X0,X1))),X2) = meet(X0,meet(X2,join(complement(X0),meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f5425,f108]) ).
fof(f5666,plain,
! [X2,X0,X1] : meet(X0,meet(complement(meet(X0,X1)),X2)) = meet(X0,meet(X2,join(complement(X0),meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f5615,f7]) ).
fof(f6214,plain,
join(a,sF3) = join(a,sF4),
inference(superposition,[],[f826,f23]) ).
fof(f6307,plain,
a = join(a,sF4),
inference(forward_demodulation,[],[f6214,f39]) ).
fof(f6339,plain,
sF4 = meet(sF4,a),
inference(superposition,[],[f34,f6307]) ).
fof(f6364,plain,
sF4 = meet(a,sF4),
inference(forward_demodulation,[],[f6339,f5]) ).
fof(f7593,plain,
! [X0] : meet(a,join(sF2,meet(a,X0))) = meet(a,join(sF2,meet(X0,join(b,meet(X0,join(a,b)))))),
inference(superposition,[],[f169,f25]) ).
fof(f7599,plain,
! [X0] : meet(a,join(sF3,meet(a,X0))) = meet(a,join(sF3,meet(X0,join(c,meet(X0,join(a,c)))))),
inference(superposition,[],[f169,f26]) ).
fof(f7818,plain,
! [X0] : meet(a,join(sF3,meet(a,X0))) = meet(a,join(sF3,meet(X0,join(c,meet(X0,join(c,a)))))),
inference(forward_demodulation,[],[f7599,f6]) ).
fof(f7824,plain,
! [X0] : meet(a,join(sF2,meet(a,X0))) = meet(a,join(sF2,meet(X0,join(b,meet(X0,join(b,a)))))),
inference(forward_demodulation,[],[f7593,f6]) ).
fof(f8337,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X0,X1),join(meet(join(X0,X1),X2),meet(join(X0,X1),X3)))) = meet(X0,join(meet(join(X0,X1),X2),meet(X3,join(X2,meet(X3,join(X2,join(X0,X1))))))),
inference(superposition,[],[f94,f178]) ).
fof(f8348,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(join(X0,X1),X2),meet(join(X0,X1),X3))) = meet(X0,join(meet(join(X0,X1),X2),meet(X3,join(X2,meet(X3,join(X2,join(X0,X1))))))),
inference(forward_demodulation,[],[f8337,f94]) ).
fof(f9332,plain,
! [X2,X0,X1] : meet(join(X1,X2),meet(X1,X0)) = join(meet(X0,X1),meet(join(X1,X2),meet(X1,X0))),
inference(superposition,[],[f149,f304]) ).
fof(f9561,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(join(X1,X2),meet(X1,X0)),
inference(forward_demodulation,[],[f9332,f966]) ).
fof(f9611,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X1,meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f9561,f108]) ).
fof(f9760,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,X2)),meet(X0,X1)),
inference(superposition,[],[f32,f9611]) ).
fof(f9835,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f9760,f6]) ).
fof(f9919,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f590,f4]) ).
fof(f9948,plain,
! [X0] : join(meet(a,X0),sF2) = meet(a,join(meet(a,X0),sF2)),
inference(superposition,[],[f590,f38]) ).
fof(f9949,plain,
! [X0] : join(meet(a,X0),sF3) = meet(a,join(meet(a,X0),sF3)),
inference(superposition,[],[f590,f39]) ).
fof(f10042,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),meet(X0,join(meet(X0,X1),X2)))) = meet(X0,join(meet(X0,X2),meet(join(meet(X0,X1),X2),join(X2,join(meet(X0,X1),X2))))),
inference(superposition,[],[f187,f590]) ).
fof(f10102,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),meet(X0,join(meet(X0,X1),X2)))) = meet(X0,join(meet(X0,X2),join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f10042,f34]) ).
fof(f10146,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(sF3,meet(a,X0))),
inference(forward_demodulation,[],[f9949,f6]) ).
fof(f10147,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(sF2,meet(a,X0))),
inference(forward_demodulation,[],[f9948,f6]) ).
fof(f10159,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X2,join(X1,meet(X2,join(X0,X1)))))),
inference(backward_demodulation,[],[f12,f9919]) ).
fof(f10164,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X2,join(meet(X0,X1),meet(X2,X0))))),
inference(backward_demodulation,[],[f214,f9919]) ).
fof(f10213,plain,
! [X2,X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X2)) = meet(X0,join(meet(X0,complement(meet(X0,X1))),X2)),
inference(backward_demodulation,[],[f730,f9919]) ).
fof(f10217,plain,
! [X2,X0,X1] : join(meet(X0,join(complement(X0),X1)),meet(X0,X2)) = meet(X0,join(meet(X0,join(complement(X0),X1)),X2)),
inference(backward_demodulation,[],[f3949,f9919]) ).
fof(f10304,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),meet(X0,join(meet(X0,X1),X2)))) = meet(X0,join(X2,join(meet(X0,X2),meet(X0,X1)))),
inference(forward_demodulation,[],[f10102,f67]) ).
fof(f10349,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(sF3,meet(X0,join(c,meet(X0,join(c,a)))))),
inference(backward_demodulation,[],[f7818,f10146]) ).
fof(f10352,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(sF2,meet(X0,join(b,meet(X0,join(b,a)))))),
inference(backward_demodulation,[],[f7824,f10147]) ).
fof(f10447,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,join(meet(X0,X2),meet(X0,join(meet(X0,X1),X2)))),
inference(forward_demodulation,[],[f10304,f54]) ).
fof(f10541,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X2),meet(X0,join(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f10447,f9919]) ).
fof(f11421,plain,
! [X0,X1] : meet(X0,one) = join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f10213,f9]) ).
fof(f11526,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = X0,
inference(forward_demodulation,[],[f11421,f159]) ).
fof(f14563,plain,
! [X0,X1] : join(complement(meet(X0,X1)),X0) = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(superposition,[],[f54,f11526]) ).
fof(f14589,plain,
! [X0,X1] :
( zero != meet(meet(X0,complement(meet(X0,X1))),join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(X0)))
| complement(meet(X0,complement(meet(X0,X1)))) = join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(X0)) ),
inference(superposition,[],[f1199,f11526]) ).
fof(f14598,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(X0))))
| complement(meet(X0,complement(meet(X0,X1)))) = join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(X0)) ),
inference(forward_demodulation,[],[f14589,f7]) ).
fof(f14622,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f14563,f6]) ).
fof(f14658,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),join(complement(X0),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))))
| complement(meet(X0,complement(meet(X0,X1)))) = join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(X0)) ),
inference(forward_demodulation,[],[f14598,f6]) ).
fof(f14672,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f14622,f595]) ).
fof(f14704,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))
| complement(meet(X0,complement(meet(X0,X1)))) = join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(X0)) ),
inference(forward_demodulation,[],[f14658,f5666]) ).
fof(f14721,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(meet(X0,complement(meet(X0,X1)))) = join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(X0)) ),
inference(forward_demodulation,[],[f14704,f5]) ).
fof(f14727,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),complement(X0)),
inference(forward_subsumption_resolution,[],[f14721,f250]) ).
fof(f14732,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = join(complement(X0),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f14727,f6]) ).
fof(f14815,plain,
! [X0,X1] :
( one != one
| zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))) ),
inference(superposition,[],[f11,f14672]) ).
fof(f14841,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))) ),
inference(trivial_inequality_removal,[],[f14815]) ).
fof(f14862,plain,
! [X0,X1] : complement(complement(meet(X0,X1))) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_subsumption_resolution,[],[f14841,f1061]) ).
fof(f14912,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f14862,f4422]) ).
fof(f14938,plain,
! [X0,X1] : join(meet(X0,complement(meet(X0,X1))),meet(X0,X1)) = X0,
inference(backward_demodulation,[],[f11526,f14912]) ).
fof(f14944,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = complement(meet(X0,complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f14732,f14912]) ).
fof(f14964,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(backward_demodulation,[],[f14912,f14944]) ).
fof(f14971,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f14938,f6]) ).
fof(f15071,plain,
! [X0,X1] : join(meet(X1,X0),X0) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f812,f14971]) ).
fof(f15072,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f54,f14971]) ).
fof(f15160,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f15071,f6]) ).
fof(f15225,plain,
! [X0,X1] : join(meet(X1,X0),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f15160,f32]) ).
fof(f15286,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(complement(X1),meet(X0,X1))),
inference(superposition,[],[f14964,f9611]) ).
fof(f15343,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f10217,f14964]) ).
fof(f15351,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(join(complement(X0),meet(X0,X1)),X2)),
inference(superposition,[],[f7,f14964]) ).
fof(f15388,plain,
! [X2,X0,X1] : meet(X1,meet(join(X0,X1),X2)) = meet(X1,join(complement(join(X0,X1)),meet(join(X0,X1),X2))),
inference(superposition,[],[f95,f14964]) ).
fof(f15402,plain,
! [X2,X0,X1] : meet(X1,X2) = meet(X1,join(complement(join(X0,X1)),meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f15388,f95]) ).
fof(f15425,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(join(complement(X0),meet(X0,X1)),X2)),
inference(forward_demodulation,[],[f15351,f7]) ).
fof(f15435,plain,
! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X2),join(meet(X0,X1),meet(X0,X2))),
inference(backward_demodulation,[],[f10541,f15343]) ).
fof(f15489,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X0,meet(X2,join(X1,meet(X2,join(X0,X1)))))),
inference(backward_demodulation,[],[f10159,f15343]) ).
fof(f15520,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X0,meet(X2,join(meet(X0,X1),meet(X2,X0))))),
inference(backward_demodulation,[],[f10164,f15343]) ).
fof(f15671,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X2,X0)),
inference(forward_demodulation,[],[f15520,f5522]) ).
fof(f15683,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f15435,f50]) ).
fof(f15789,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(join(X0,X1),X2),meet(join(X0,X1),X3))) = meet(X0,join(meet(join(X0,X1),X2),join(meet(X3,join(X2,join(X0,X1))),meet(X3,X2)))),
inference(backward_demodulation,[],[f8348,f15683]) ).
fof(f15820,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X0,join(meet(X2,join(X0,X1)),meet(X2,X1)))),
inference(backward_demodulation,[],[f15489,f15683]) ).
fof(f15877,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(sF2,join(meet(X0,join(b,a)),meet(X0,b)))),
inference(backward_demodulation,[],[f10352,f15683]) ).
fof(f15882,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(sF3,join(meet(X0,join(c,a)),meet(X0,c)))),
inference(backward_demodulation,[],[f10349,f15683]) ).
fof(f15975,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(sF3,join(meet(X0,c),meet(X0,join(c,a))))),
inference(forward_demodulation,[],[f15882,f6]) ).
fof(f15980,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(sF2,join(meet(X0,b),meet(X0,join(b,a))))),
inference(forward_demodulation,[],[f15877,f6]) ).
fof(f16036,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X1),meet(X0,join(meet(X2,X1),meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f15820,f6]) ).
fof(f16065,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(join(X0,X1),X2),meet(join(X0,X1),X3))) = meet(X0,join(meet(join(X0,X1),X2),join(meet(X3,X2),meet(X3,join(X2,join(X0,X1)))))),
inference(forward_demodulation,[],[f15789,f6]) ).
fof(f16145,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(sF3,meet(X0,join(c,a)))),
inference(forward_demodulation,[],[f15975,f9835]) ).
fof(f16148,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(sF2,meet(X0,join(b,a)))),
inference(forward_demodulation,[],[f15980,f9835]) ).
fof(f16174,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(join(X0,X1),X2),meet(join(X0,X1),X3))) = meet(X0,join(meet(join(X0,X1),X2),meet(X3,join(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f16065,f9835]) ).
fof(f16492,plain,
! [X2,X3,X0,X1] : meet(meet(X0,join(meet(X2,X1),meet(X2,join(X0,X1)))),X3) = meet(meet(X0,join(meet(X2,X1),meet(X2,join(X0,X1)))),meet(X3,join(meet(X0,X1),meet(X0,X2)))),
inference(superposition,[],[f747,f16036]) ).
fof(f16500,plain,
! [X2,X3,X0,X1] : meet(meet(X0,join(meet(X2,X1),meet(X2,join(X0,X1)))),X3) = meet(join(meet(X0,X1),meet(X0,X2)),meet(meet(X0,join(meet(X2,X1),meet(X2,join(X0,X1)))),X3)),
inference(forward_demodulation,[],[f16492,f108]) ).
fof(f16646,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),X3)) = meet(join(meet(X0,X1),meet(X0,X2)),meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),X3))),
inference(forward_demodulation,[],[f16500,f7]) ).
fof(f16733,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),X3)) = meet(X0,meet(meet(join(meet(X2,X1),meet(X2,join(X0,X1))),X3),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f16646,f108]) ).
fof(f16787,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),X3)) = meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),meet(X3,join(meet(X0,X1),meet(X0,X2))))),
inference(forward_demodulation,[],[f16733,f7]) ).
fof(f16914,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f15072,f1353]) ).
fof(f17249,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f54,f15671]) ).
fof(f17295,plain,
! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,X2)),
inference(forward_demodulation,[],[f17249,f54]) ).
fof(f18014,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,meet(join(X0,X1),complement(X0))),
inference(superposition,[],[f16914,f3]) ).
fof(f18160,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f18014,f17295]) ).
fof(f18209,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),join(X0,X1))),
inference(forward_demodulation,[],[f18160,f41]) ).
fof(f18341,plain,
! [X0,X1] :
( zero != meet(X0,join(meet(complement(X0),join(X0,X1)),complement(join(X0,X1))))
| complement(X0) = join(meet(complement(X0),join(X0,X1)),complement(join(X0,X1))) ),
inference(superposition,[],[f1199,f18209]) ).
fof(f18372,plain,
! [X0,X1] :
( zero != meet(X0,join(complement(join(X0,X1)),meet(complement(X0),join(X0,X1))))
| complement(X0) = join(meet(complement(X0),join(X0,X1)),complement(join(X0,X1))) ),
inference(forward_demodulation,[],[f18341,f6]) ).
fof(f18413,plain,
! [X0,X1] :
( complement(X0) = join(complement(join(X0,X1)),meet(complement(X0),join(X0,X1)))
| zero != meet(X0,join(complement(join(X0,X1)),meet(complement(X0),join(X0,X1)))) ),
inference(forward_demodulation,[],[f18372,f6]) ).
fof(f18550,plain,
! [X2,X3,X0,X1] : join(meet(X0,meet(X1,X2)),meet(X1,X3)) = meet(X1,join(meet(X0,meet(X1,X2)),X3)),
inference(superposition,[],[f15343,f108]) ).
fof(f18644,plain,
! [X2,X3,X0,X1] : meet(join(meet(X0,X1),meet(X0,X2)),X3) = meet(X0,meet(join(meet(X0,X1),X2),X3)),
inference(superposition,[],[f7,f15343]) ).
fof(f18683,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(join(X0,X1),X2),meet(join(X0,X1),X3))) = meet(X0,join(meet(join(X0,X1),X2),X3)),
inference(superposition,[],[f94,f15343]) ).
fof(f18708,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(join(X0,X1),X2),meet(X3,join(X2,join(X0,X1))))) = meet(X0,join(meet(join(X0,X1),X2),X3)),
inference(backward_demodulation,[],[f16174,f18683]) ).
fof(f18755,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),meet(X3,join(meet(X0,X1),meet(X0,X2))))) = meet(X0,meet(X2,meet(join(meet(X2,X1),join(X0,X1)),X3))),
inference(backward_demodulation,[],[f16787,f18644]) ).
fof(f19061,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),meet(X3,join(meet(X0,X1),meet(X0,X2))))) = meet(X0,meet(X2,meet(join(X1,join(meet(X2,X1),X0)),X3))),
inference(forward_demodulation,[],[f18755,f67]) ).
fof(f19211,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),meet(X3,join(meet(X0,X1),meet(X0,X2))))) = meet(X0,meet(X2,meet(join(X1,X0),X3))),
inference(forward_demodulation,[],[f19061,f54]) ).
fof(f19292,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X3,X2)) = meet(X0,meet(join(meet(X2,X1),meet(X2,join(X0,X1))),meet(X3,join(meet(X0,X1),meet(X0,X2))))),
inference(forward_demodulation,[],[f19211,f1550]) ).
fof(f19334,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X3,X2)) = meet(X0,meet(X2,meet(join(meet(X2,X1),join(X0,X1)),meet(X3,join(meet(X0,X1),meet(X0,X2)))))),
inference(forward_demodulation,[],[f19292,f18644]) ).
fof(f19356,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X3,X2)) = meet(X0,meet(X2,meet(join(X1,join(meet(X2,X1),X0)),meet(X3,join(meet(X0,X1),meet(X0,X2)))))),
inference(forward_demodulation,[],[f19334,f67]) ).
fof(f19370,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X3,X2)) = meet(X0,meet(X2,meet(join(X1,X0),meet(X3,join(meet(X0,X1),meet(X0,X2)))))),
inference(forward_demodulation,[],[f19356,f54]) ).
fof(f19380,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X3,X2)) = meet(X0,meet(meet(X3,join(meet(X0,X1),meet(X0,X2))),X2)),
inference(forward_demodulation,[],[f19370,f1550]) ).
fof(f19386,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X3,X2)) = meet(X0,meet(X2,meet(X3,join(meet(X0,X1),meet(X0,X2))))),
inference(forward_demodulation,[],[f19380,f5]) ).
fof(f19391,plain,
! [X2,X3,X0] : meet(X0,meet(X2,X3)) = meet(X0,meet(X3,X2)),
inference(forward_demodulation,[],[f19386,f3584]) ).
fof(f19839,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),join(meet(X0,complement(meet(X0,X1))),complement(X0)))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(superposition,[],[f1199,f15225]) ).
fof(f19846,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,join(meet(X0,complement(meet(X0,X1))),complement(X0))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f19839,f7]) ).
fof(f19966,plain,
! [X0,X1] :
( zero != meet(X1,join(meet(X0,complement(meet(X0,X1))),meet(X0,complement(X0))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f19846,f15343]) ).
fof(f20061,plain,
! [X0,X1] :
( zero != meet(X1,join(meet(X0,complement(X0)),meet(X0,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f19966,f6]) ).
fof(f20113,plain,
! [X0,X1] :
( zero != meet(X1,join(zero,meet(X0,complement(meet(X0,X1)))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f20061,f10]) ).
fof(f20147,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X0,X1))))
| complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)) ),
inference(forward_demodulation,[],[f20113,f260]) ).
fof(f20167,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(meet(X0,complement(meet(X0,X1))),complement(X0)),
inference(forward_subsumption_resolution,[],[f20147,f1061]) ).
fof(f20183,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f20167,f6]) ).
fof(f20209,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X0)) = X0,
inference(superposition,[],[f15286,f3]) ).
fof(f20210,plain,
! [X0,X1] : meet(join(X1,X0),join(complement(join(X1,X0)),X0)) = X0,
inference(superposition,[],[f15286,f34]) ).
fof(f20291,plain,
! [X2,X0,X1] : meet(X1,meet(X0,join(X1,X2))) = meet(X1,join(complement(join(X1,X2)),meet(X0,join(X1,X2)))),
inference(superposition,[],[f94,f15286]) ).
fof(f20302,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,join(complement(join(X1,X2)),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f20291,f141]) ).
fof(f20351,plain,
! [X0,X1] : meet(join(X1,X0),join(X0,complement(join(X1,X0)))) = X0,
inference(forward_demodulation,[],[f20210,f6]) ).
fof(f20352,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f20209,f6]) ).
fof(f20375,plain,
! [X0,X1] :
( meet(X0,complement(X0)) != zero
| complement(X0) = join(complement(join(X0,X1)),meet(complement(X0),join(X0,X1))) ),
inference(backward_demodulation,[],[f18413,f20302]) ).
fof(f20419,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),meet(complement(X0),join(X0,X1))),
inference(forward_subsumption_resolution,[],[f20375,f10]) ).
fof(f20508,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f95,f20352]) ).
fof(f20774,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f20508,f6]) ).
fof(f20979,plain,
! [X0,X1] :
( complement(X0) = join(X1,complement(join(X0,X1)))
| meet(X0,X1) != zero ),
inference(backward_demodulation,[],[f1199,f20774]) ).
fof(f21129,plain,
! [X0,X1] :
( complement(X0) = join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1)))
| zero != meet(X0,meet(X1,complement(meet(X1,X0)))) ),
inference(superposition,[],[f20979,f15072]) ).
fof(f21146,plain,
! [X0,X1] :
( complement(X1) = join(complement(join(X0,X1)),complement(complement(X0)))
| zero != meet(X1,complement(join(X0,X1)))
| meet(X0,X1) != zero ),
inference(superposition,[],[f20979,f20979]) ).
fof(f21262,plain,
! [X0,X1] :
( complement(X1) = join(complement(join(X0,X1)),complement(complement(X0)))
| meet(X0,X1) != zero ),
inference(forward_subsumption_resolution,[],[f21146,f401]) ).
fof(f21279,plain,
! [X0,X1] : complement(X0) = join(meet(X1,complement(meet(X1,X0))),complement(join(X0,X1))),
inference(forward_subsumption_resolution,[],[f21129,f1061]) ).
fof(f21299,plain,
! [X0,X1] :
( complement(X1) = join(complement(complement(X0)),complement(join(X0,X1)))
| meet(X0,X1) != zero ),
inference(forward_demodulation,[],[f21262,f6]) ).
fof(f21314,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),meet(X1,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f21279,f6]) ).
fof(f21324,plain,
! [X0,X1] :
( complement(X1) = join(X0,complement(join(X0,X1)))
| meet(X0,X1) != zero ),
inference(forward_demodulation,[],[f21299,f4422]) ).
fof(f21723,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,[],[f20351,f15072]) ).
fof(f21816,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = meet(join(X1,X0),join(X0,X2)),
inference(superposition,[],[f15343,f20351]) ).
fof(f21902,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,[],[f21723,f6]) ).
fof(f21997,plain,
! [X0,X1] : meet(join(X0,X1),complement(X0)) = meet(X1,complement(meet(X1,X0))),
inference(forward_demodulation,[],[f21902,f21314]) ).
fof(f22042,plain,
! [X0,X1] : meet(X1,complement(meet(X1,X0))) = meet(complement(X0),join(X0,X1)),
inference(forward_demodulation,[],[f21997,f5]) ).
fof(f22164,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f3,f20183]) ).
fof(f22168,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f41,f20183]) ).
fof(f22185,plain,
! [X2,X0,X1] : meet(X2,complement(X1)) = meet(complement(X1),meet(X2,complement(meet(X0,X1)))),
inference(superposition,[],[f9611,f20183]) ).
fof(f22420,plain,
! [X0,X1] :
( join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X1,X0))))
| zero != meet(X0,meet(X1,complement(meet(X1,X0)))) ),
inference(superposition,[],[f21324,f15072]) ).
fof(f22584,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(X1,complement(meet(X1,X0)))),
inference(forward_subsumption_resolution,[],[f22420,f1061]) ).
fof(f23561,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X2,meet(X0,X1))),
inference(superposition,[],[f17295,f7]) ).
fof(f23846,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = complement(join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f4422,f14944]) ).
fof(f24644,plain,
! [X0,X1] : meet(X0,complement(meet(X1,complement(X0)))) = X0,
inference(superposition,[],[f22164,f4422]) ).
fof(f24668,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f22164,f3]) ).
fof(f24669,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f22164,f34]) ).
fof(f24706,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(superposition,[],[f22164,f1353]) ).
fof(f24721,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(meet(X1,X0)),join(complement(X0),X2)),
inference(superposition,[],[f54,f22164]) ).
fof(f24776,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(X0),join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f24721,f67]) ).
fof(f24798,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f24669,f5]) ).
fof(f24799,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f24668,f5]) ).
fof(f24865,plain,
! [X0,X1] : meet(X0,complement(meet(complement(X0),X1))) = X0,
inference(superposition,[],[f24706,f4422]) ).
fof(f24957,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(meet(X0,X1)),join(X2,complement(X0))),
inference(superposition,[],[f831,f24706]) ).
fof(f24967,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),meet(complement(meet(X0,X1)),complement(meet(complement(meet(X0,X1)),complement(X0))))),
inference(superposition,[],[f15225,f24706]) ).
fof(f24983,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f24967,f15072]) ).
fof(f24990,plain,
! [X2,X0,X1] : join(complement(meet(X0,X1)),X2) = join(complement(X0),join(complement(meet(X0,X1)),X2)),
inference(forward_demodulation,[],[f24957,f67]) ).
fof(f25136,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(meet(complement(X0),X1)),complement(meet(complement(meet(complement(X0),X1)),X0)))),
inference(superposition,[],[f15225,f24865]) ).
fof(f25170,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f25136,f15072]) ).
fof(f25279,plain,
! [X2,X0,X1] : join(complement(meet(X1,complement(X0))),X2) = join(complement(meet(X1,complement(X0))),join(X0,X2)),
inference(superposition,[],[f54,f24644]) ).
fof(f25356,plain,
! [X2,X0,X1] : join(complement(meet(X1,complement(X0))),X2) = join(X0,join(X2,complement(meet(X1,complement(X0))))),
inference(forward_demodulation,[],[f25279,f67]) ).
fof(f25562,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(superposition,[],[f24799,f4422]) ).
fof(f25633,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f4,f24799]) ).
fof(f25668,plain,
! [X2,X0,X1] : join(complement(join(X0,X1)),meet(complement(X0),X2)) = meet(complement(X0),join(complement(join(X0,X1)),X2)),
inference(superposition,[],[f15343,f24799]) ).
fof(f25776,plain,
! [X0,X1] : complement(join(X0,complement(X1))) = meet(X1,complement(join(X0,complement(X1)))),
inference(superposition,[],[f25562,f50]) ).
fof(f25812,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f109,f25562]) ).
fof(f26253,plain,
! [X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,X1))),
inference(superposition,[],[f25633,f50]) ).
fof(f27806,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f25812,f24798]) ).
fof(f27826,plain,
! [X2,X0,X1] : join(complement(X1),X2) = join(complement(X1),join(X2,complement(join(X0,X1)))),
inference(superposition,[],[f570,f24798]) ).
fof(f27990,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X0,X1),complement(join(complement(X1),complement(X0)))),
inference(superposition,[],[f27806,f4422]) ).
fof(f28034,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = join(meet(complement(X1),complement(X0)),complement(join(X0,X1))),
inference(superposition,[],[f27806,f4422]) ).
fof(f28160,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = join(complement(join(X0,X1)),meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f28034,f6]) ).
fof(f28452,plain,
! [X0,X1] : meet(X1,complement(X0)) = join(meet(X1,complement(X0)),complement(join(X0,complement(X1)))),
inference(superposition,[],[f27990,f4422]) ).
fof(f28766,plain,
! [X0,X1] : meet(meet(X0,complement(X1)),complement(join(X1,complement(X0)))) = meet(meet(X0,complement(X1)),join(complement(join(X1,complement(X0))),complement(meet(X0,complement(X1))))),
inference(superposition,[],[f20774,f28452]) ).
fof(f28774,plain,
! [X0,X1] : meet(meet(X0,complement(X1)),complement(join(X1,complement(X0)))) = meet(X0,meet(complement(X1),join(complement(join(X1,complement(X0))),complement(meet(X0,complement(X1)))))),
inference(forward_demodulation,[],[f28766,f7]) ).
fof(f28820,plain,
! [X0,X1] : meet(meet(X0,complement(X1)),complement(join(X1,complement(X0)))) = meet(X0,join(complement(join(X1,complement(X0))),meet(complement(X1),complement(meet(X0,complement(X1)))))),
inference(forward_demodulation,[],[f28774,f25668]) ).
fof(f28855,plain,
! [X0,X1] : meet(X0,meet(complement(X1),complement(join(X1,complement(X0))))) = meet(X0,join(complement(join(X1,complement(X0))),meet(complement(X1),complement(meet(X0,complement(X1)))))),
inference(forward_demodulation,[],[f28820,f7]) ).
fof(f28884,plain,
! [X0,X1] : meet(X0,complement(join(X1,complement(X0)))) = meet(X0,join(complement(join(X1,complement(X0))),meet(complement(X1),complement(meet(X0,complement(X1)))))),
inference(forward_demodulation,[],[f28855,f24799]) ).
fof(f28902,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(X0,join(complement(join(X1,complement(X0))),meet(complement(X1),complement(meet(X0,complement(X1)))))),
inference(forward_demodulation,[],[f28884,f25776]) ).
fof(f28947,plain,
! [X2,X0,X1] : complement(join(X1,meet(X2,X0))) = join(complement(join(X1,meet(X2,X0))),complement(join(X0,X1))),
inference(superposition,[],[f26253,f831]) ).
fof(f28973,plain,
! [X0,X1] : complement(complement(join(complement(X1),complement(X0)))) = join(complement(complement(join(complement(X1),complement(X0)))),complement(meet(X0,X1))),
inference(superposition,[],[f26253,f27990]) ).
fof(f28974,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(complement(complement(join(complement(X1),X0))),complement(meet(complement(X0),X1))),
inference(superposition,[],[f26253,f27806]) ).
fof(f28975,plain,
! [X0,X1] : complement(complement(join(X1,complement(X0)))) = join(complement(complement(join(X1,complement(X0)))),complement(meet(X0,complement(X1)))),
inference(superposition,[],[f26253,f28452]) ).
fof(f29079,plain,
! [X0,X1] : complement(complement(join(X1,complement(X0)))) = join(complement(meet(X0,complement(X1))),complement(complement(join(X1,complement(X0))))),
inference(forward_demodulation,[],[f28975,f6]) ).
fof(f29080,plain,
! [X0,X1] : complement(complement(join(complement(X1),X0))) = join(complement(meet(complement(X0),X1)),complement(complement(join(complement(X1),X0)))),
inference(forward_demodulation,[],[f28974,f6]) ).
fof(f29081,plain,
! [X0,X1] : complement(complement(join(complement(X1),complement(X0)))) = join(complement(meet(X0,X1)),complement(complement(join(complement(X1),complement(X0))))),
inference(forward_demodulation,[],[f28973,f6]) ).
fof(f29100,plain,
! [X2,X0,X1] : complement(join(X1,meet(X2,X0))) = join(complement(join(X0,X1)),complement(join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f28947,f6]) ).
fof(f29126,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(meet(X0,complement(X1))),join(X1,complement(X0))),
inference(forward_demodulation,[],[f29079,f4422]) ).
fof(f29127,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(meet(complement(X0),X1)),join(complement(X1),X0)),
inference(forward_demodulation,[],[f29080,f4422]) ).
fof(f29128,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(meet(X0,X1)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f29081,f4422]) ).
fof(f29153,plain,
! [X0,X1] : join(X1,complement(X0)) = join(join(X1,complement(X0)),complement(meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f29126,f6]) ).
fof(f29154,plain,
! [X0,X1] : join(complement(X1),X0) = join(join(complement(X1),X0),complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f29127,f6]) ).
fof(f29155,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = join(complement(X0),join(complement(meet(X0,X1)),complement(X1))),
inference(forward_demodulation,[],[f29128,f67]) ).
fof(f29172,plain,
! [X0,X1] : join(X1,complement(X0)) = join(X1,join(complement(X0),complement(meet(X0,complement(X1))))),
inference(forward_demodulation,[],[f29153,f8]) ).
fof(f29173,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),join(X0,complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f29154,f8]) ).
fof(f29174,plain,
! [X0,X1] : join(complement(meet(X0,X1)),complement(X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f29155,f24990]) ).
fof(f29182,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(meet(X0,complement(X1))),complement(X0)),
inference(forward_demodulation,[],[f29172,f25356]) ).
fof(f29183,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(meet(complement(X0),X1)),X0),
inference(forward_demodulation,[],[f29173,f24776]) ).
fof(f29184,plain,
! [X0,X1] : join(complement(X1),complement(meet(X0,X1))) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f29174,f6]) ).
fof(f29187,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),complement(meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f29182,f6]) ).
fof(f29188,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f29183,f6]) ).
fof(f29189,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f29184,f22168]) ).
fof(f29192,plain,
! [X0,X1] : join(X1,complement(X0)) = complement(meet(X0,complement(X1))),
inference(forward_demodulation,[],[f29187,f24983]) ).
fof(f29194,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(backward_demodulation,[],[f25170,f29188]) ).
fof(f29247,plain,
! [X2,X0,X1] : complement(join(X1,meet(X2,X0))) = complement(meet(join(X1,meet(X2,X0)),join(X0,X1))),
inference(backward_demodulation,[],[f29100,f29189]) ).
fof(f29305,plain,
! [X0,X1] : complement(join(X1,complement(X0))) = meet(X0,join(complement(join(X1,complement(X0))),meet(complement(X1),join(X1,complement(X0))))),
inference(backward_demodulation,[],[f28902,f29192]) ).
fof(f29314,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(meet(X1,X0),complement(X1)),
inference(backward_demodulation,[],[f22584,f29192]) ).
fof(f29401,plain,
! [X2,X0,X1] : complement(join(X1,meet(X2,X0))) = complement(meet(join(X0,X1),join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f29247,f1353]) ).
fof(f29457,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),meet(X1,X0)),
inference(forward_demodulation,[],[f29314,f6]) ).
fof(f29462,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(X1,complement(X0))),
inference(forward_demodulation,[],[f29305,f20419]) ).
fof(f29498,plain,
! [X2,X0,X1] : complement(join(X1,meet(X2,X0))) = complement(join(X1,meet(join(X0,X1),meet(X2,X0)))),
inference(forward_demodulation,[],[f29401,f21816]) ).
fof(f29593,plain,
! [X2,X0,X1] : complement(join(X1,meet(X2,X0))) = complement(join(X1,meet(X0,meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f29498,f23561]) ).
fof(f29634,plain,
! [X2,X0,X1] : complement(join(X1,meet(X2,X0))) = complement(join(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f29593,f94]) ).
fof(f29656,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(complement(X0),meet(X0,X1)),
inference(superposition,[],[f29457,f6]) ).
fof(f29674,plain,
! [X0,X1] : join(X1,complement(join(X1,complement(X0)))) = join(X0,meet(complement(X0),X1)),
inference(superposition,[],[f29457,f4422]) ).
fof(f29701,plain,
! [X0,X1] : join(complement(X0),meet(X0,X1)) = join(X1,join(complement(X0),meet(X0,X1))),
inference(superposition,[],[f41,f29457]) ).
fof(f29726,plain,
! [X0,X1] : complement(join(complement(X0),meet(X0,X1))) = meet(complement(X1),complement(join(complement(X0),meet(X0,X1)))),
inference(superposition,[],[f24799,f29457]) ).
fof(f29760,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f41,f29457]) ).
fof(f29804,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),X0),
inference(forward_demodulation,[],[f29760,f27826]) ).
fof(f29828,plain,
! [X0,X1] : meet(X0,complement(meet(X0,X1))) = meet(complement(X1),meet(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f29726,f23846]) ).
fof(f29844,plain,
! [X0,X1] : join(X1,complement(X0)) = join(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f29701,f831]) ).
fof(f29857,plain,
! [X0,X1] : join(X0,meet(complement(X0),X1)) = join(X1,meet(X0,complement(X1))),
inference(forward_demodulation,[],[f29674,f29462]) ).
fof(f29889,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(complement(X1),X0)),
inference(backward_demodulation,[],[f20508,f29804]) ).
fof(f29912,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X1,X0)),
inference(backward_demodulation,[],[f29457,f29804]) ).
fof(f29988,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f29828,f22185]) ).
fof(f30008,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(join(X1,complement(X0)),X2)),
inference(backward_demodulation,[],[f15425,f29844]) ).
fof(f30037,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(backward_demodulation,[],[f29656,f29844]) ).
fof(f30051,plain,
! [X2,X0,X1] : meet(X1,X2) = meet(X1,join(X2,complement(join(X0,X1)))),
inference(backward_demodulation,[],[f15402,f29844]) ).
fof(f30287,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(X1))),
inference(backward_demodulation,[],[f15072,f29988]) ).
fof(f30311,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,X1)),
inference(backward_demodulation,[],[f22042,f29988]) ).
fof(f30660,plain,
! [X0,X1] : join(X1,X0) = join(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f29857,f30287]) ).
fof(f31222,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(superposition,[],[f29912,f4422]) ).
fof(f32114,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(X0))),
inference(superposition,[],[f30051,f260]) ).
fof(f32763,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X1,X0)),
inference(superposition,[],[f32114,f4422]) ).
fof(f32959,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,X1)),
inference(superposition,[],[f32763,f6]) ).
fof(f33806,plain,
! [X0,X1] : meet(complement(X0),complement(join(X1,X0))) = meet(complement(X0),join(X0,complement(X1))),
inference(superposition,[],[f32959,f30037]) ).
fof(f33840,plain,
! [X0,X1] : meet(complement(X0),complement(join(X1,X0))) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f33806,f30311]) ).
fof(f33908,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f33840,f24798]) ).
fof(f33968,plain,
! [X0,X1] : complement(join(X1,X0)) = join(complement(join(X0,X1)),complement(join(X1,X0))),
inference(backward_demodulation,[],[f28160,f33908]) ).
fof(f34100,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(meet(join(X1,X0),join(X0,X1))),
inference(forward_demodulation,[],[f33968,f29189]) ).
fof(f34140,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,meet(join(X1,X0),X1))),
inference(forward_demodulation,[],[f34100,f21816]) ).
fof(f34176,plain,
! [X0,X1] : complement(join(X1,X0)) = complement(join(X0,meet(X1,join(X1,X0)))),
inference(forward_demodulation,[],[f34140,f29634]) ).
fof(f34288,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f34176,f3]) ).
fof(f36404,plain,
! [X2,X0,X1] : complement(meet(complement(join(X0,X1)),X2)) = join(complement(X2),join(X1,X0)),
inference(superposition,[],[f29194,f34288]) ).
fof(f36531,plain,
! [X2,X0,X1] : join(complement(X2),join(X0,X1)) = join(complement(X2),join(X1,X0)),
inference(forward_demodulation,[],[f36404,f29194]) ).
fof(f36731,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(complement(X0),join(X1,X2))),
inference(superposition,[],[f29889,f36531]) ).
fof(f36791,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,join(X1,X2)),
inference(forward_demodulation,[],[f36731,f29889]) ).
fof(f39071,plain,
! [X2,X0,X1] : meet(complement(complement(X0)),join(complement(X0),join(X1,X2))) = meet(join(X2,X1),complement(complement(X0))),
inference(superposition,[],[f30311,f36531]) ).
fof(f39200,plain,
! [X2,X0,X1] : meet(join(X2,X1),X0) = meet(X0,join(complement(X0),join(X1,X2))),
inference(forward_demodulation,[],[f39071,f4422]) ).
fof(f39281,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(forward_demodulation,[],[f39200,f29889]) ).
fof(f39465,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,X2)),X3) = meet(X3,join(meet(X2,X1),X0)),
inference(superposition,[],[f39281,f17295]) ).
fof(f48304,plain,
! [X2,X0,X1] : join(X0,meet(complement(X0),meet(X1,X2))) = join(X0,meet(join(X1,complement(complement(X0))),X2)),
inference(superposition,[],[f31222,f30008]) ).
fof(f48327,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = join(X0,meet(complement(X0),meet(X1,X2))),
inference(forward_demodulation,[],[f48304,f4422]) ).
fof(f48442,plain,
! [X2,X0,X1] : join(X0,meet(join(X1,X0),X2)) = join(meet(X1,X2),X0),
inference(forward_demodulation,[],[f48327,f30660]) ).
fof(f48531,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X1,X0),join(X0,X2)),
inference(backward_demodulation,[],[f21816,f48442]) ).
fof(f48700,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X1,X2))) = join(meet(X2,X0),X1),
inference(superposition,[],[f48442,f39281]) ).
fof(f48766,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = meet(meet(join(X0,X2),X1),join(meet(X0,X1),X2)),
inference(superposition,[],[f34,f48442]) ).
fof(f48866,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = meet(join(X2,meet(X1,X0)),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f48766,f39465]) ).
fof(f49068,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = meet(X1,meet(join(X2,meet(X1,X0)),join(X0,X2))),
inference(forward_demodulation,[],[f48866,f108]) ).
fof(f49204,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = meet(X1,meet(join(X0,X2),join(X2,meet(X1,X0)))),
inference(forward_demodulation,[],[f49068,f19391]) ).
fof(f49279,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = meet(X1,join(meet(X0,meet(X1,X0)),X2)),
inference(forward_demodulation,[],[f49204,f48531]) ).
fof(f49321,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,meet(X1,X0)),meet(X1,X2)),
inference(forward_demodulation,[],[f49279,f18550]) ).
fof(f49334,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X1,X0),meet(X1,X2)),
inference(forward_demodulation,[],[f49321,f51]) ).
fof(f49358,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = meet(X0,join(meet(X0,X1),X2)),
inference(backward_demodulation,[],[f15343,f49334]) ).
fof(f49361,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(X2,X0)),
inference(backward_demodulation,[],[f15671,f49334]) ).
fof(f49452,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(join(X0,X1),X2),X3)) = meet(X0,meet(join(X2,X3),join(X0,X1))),
inference(backward_demodulation,[],[f18683,f49334]) ).
fof(f49782,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,X3)) = meet(X0,join(meet(join(X0,X1),X2),X3)),
inference(forward_demodulation,[],[f49452,f141]) ).
fof(f50109,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,X3)) = meet(X0,join(meet(join(X0,X1),X2),meet(X3,join(X2,join(X0,X1))))),
inference(backward_demodulation,[],[f18708,f49782]) ).
fof(f50465,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,X3)) = meet(X0,join(X2,meet(X3,join(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f50109,f49782]) ).
fof(f50778,plain,
! [X2,X3,X0,X1] : meet(X0,join(X2,X3)) = meet(X0,join(meet(join(X0,X1),X3),X2)),
inference(forward_demodulation,[],[f50465,f48700]) ).
fof(f52349,plain,
! [X0] : meet(join(X0,b),a) = join(meet(a,X0),sF2),
inference(superposition,[],[f49361,f25]) ).
fof(f52355,plain,
! [X0] : meet(join(X0,c),a) = join(meet(a,X0),sF3),
inference(superposition,[],[f49361,f26]) ).
fof(f52487,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(join(X0,c),a),
inference(forward_demodulation,[],[f52355,f6]) ).
fof(f52493,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(join(X0,b),a),
inference(forward_demodulation,[],[f52349,f6]) ).
fof(f52665,plain,
! [X0] : join(sF3,meet(a,X0)) = meet(a,join(X0,c)),
inference(forward_demodulation,[],[f52487,f5]) ).
fof(f52671,plain,
! [X0] : join(sF2,meet(a,X0)) = meet(a,join(X0,b)),
inference(forward_demodulation,[],[f52493,f5]) ).
fof(f52805,plain,
! [X0] : meet(a,join(X0,c)) = meet(a,join(sF3,meet(X0,join(c,a)))),
inference(backward_demodulation,[],[f16145,f52665]) ).
fof(f52813,plain,
! [X0] : meet(a,join(X0,b)) = meet(a,join(sF2,meet(X0,join(b,a)))),
inference(backward_demodulation,[],[f16148,f52671]) ).
fof(f55158,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(meet(X0,X2),X1)),
inference(superposition,[],[f50778,f249]) ).
fof(f55691,plain,
! [X2,X3,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(X1,join(X3,X0)))),
inference(superposition,[],[f55158,f747]) ).
fof(f56033,plain,
! [X2,X3,X0,X1] : meet(join(X1,X2),X0) = meet(X0,join(X2,meet(X1,join(X3,X0)))),
inference(forward_demodulation,[],[f55691,f49358]) ).
fof(f56133,plain,
! [X0] : meet(a,join(X0,b)) = meet(join(X0,sF2),a),
inference(backward_demodulation,[],[f52813,f56033]) ).
fof(f56134,plain,
! [X0] : meet(a,join(X0,c)) = meet(join(X0,sF3),a),
inference(backward_demodulation,[],[f52805,f56033]) ).
fof(f56192,plain,
! [X0] : meet(a,join(X0,c)) = meet(a,join(X0,sF3)),
inference(forward_demodulation,[],[f56134,f5]) ).
fof(f56193,plain,
! [X0] : meet(a,join(X0,b)) = meet(a,join(X0,sF2)),
inference(forward_demodulation,[],[f56133,f5]) ).
fof(f56428,plain,
meet(a,sF4) = meet(a,join(sF2,c)),
inference(superposition,[],[f56192,f23]) ).
fof(f56527,plain,
meet(a,sF4) = meet(a,join(c,sF2)),
inference(forward_demodulation,[],[f56428,f36791]) ).
fof(f56567,plain,
meet(a,sF4) = meet(a,join(c,b)),
inference(forward_demodulation,[],[f56527,f56193]) ).
fof(f56591,plain,
meet(a,join(b,c)) = meet(a,sF4),
inference(forward_demodulation,[],[f56567,f36791]) ).
fof(f56603,plain,
meet(a,join(b,c)) = sF4,
inference(forward_demodulation,[],[f56591,f6364]) ).
fof(f56608,plain,
meet(a,sF0) = sF4,
inference(forward_demodulation,[],[f56603,f15]) ).
fof(f56611,plain,
sF1 = sF4,
inference(forward_demodulation,[],[f56608,f17]) ).
fof(f56612,plain,
$false,
inference(forward_subsumption_resolution,[],[f56611,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT188-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.22/0.48 % Computer : n007.cluster.edu
% 0.22/0.48 % Model : x86_64 x86_64
% 0.22/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.48 % Memory : 8046.5625MB
% 0.22/0.48 % OS : Linux 6.8.0-71-generic
% 0.22/0.48 % CPULimit : 300
% 0.22/0.48 % WCLimit : 300
% 0.22/0.48 % DateTime : Sun Sep 27 14:03:25 UTC 2026
% 0.22/0.48 % CPUTime :
% 0.22/0.48 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.25/0.54 Running first-order theorem proving
% 0.25/0.54 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.30/4.03 % (1436097)Input is clausal, will run a generic CNF schedule.
% 18.30/4.03 % (1436108)dis-21_1_sil=8000:lcm=predicate:random_seed=2045624772: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)
% 18.30/4.03 % (1436108)Refutation not found, incomplete strategy
% 18.30/4.03 % (1436108)------------------------------
% 18.30/4.03 % (1436108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/4.03 % (1436108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/4.03 % (1436108)CaDiCaL version: 2.1.3
% 18.30/4.03 % (1436108)Termination reason: Refutation not found, incomplete strategy
% 18.30/4.03 % (1436108)Time elapsed: 0.002 s
% 18.30/4.03 % (1436108)Peak memory usage: 88 MB
% 18.30/4.03 % (1436108)Instructions burned: 1 (million)
% 18.30/4.03 % (1436104)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3635256258:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.30/4.03 % (1436103)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3534631942:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.30/4.03 % (1436105)lrs+10_1_sil=8000:sp=occurrence:random_seed=1724938668:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.30/4.03 % (1436102)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=891185436:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.30/4.03 % (1436106)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1262013611:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.30/4.03 % (1436107)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=133277759:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.30/4.03 % (1436105)Instruction limit reached!
% 18.30/4.03 % (1436105)------------------------------
% 18.30/4.03 % (1436105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/4.03 % (1436105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/4.03 % (1436105)CaDiCaL version: 2.1.3
% 18.30/4.03 % (1436105)Termination reason: Instruction limit
% 18.30/4.03 % (1436105)Termination phase: Saturation
% 18.30/4.03 % (1436105)Time elapsed: 0.105 s
% 18.30/4.03 % (1436105)Peak memory usage: 88 MB
% 18.30/4.03 % (1436105)Instructions burned: 108 (million)
% 18.30/4.03 % (1436106)Instruction limit reached!
% 18.30/4.03 % (1436106)------------------------------
% 18.30/4.03 % (1436106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/4.03 % (1436106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/4.03 % (1436106)CaDiCaL version: 2.1.3
% 18.30/4.03 % (1436106)Termination reason: Instruction limit
% 18.30/4.03 % (1436106)Termination phase: Saturation
% 18.30/4.03 % (1436106)Time elapsed: 0.110 s
% 18.30/4.03 % (1436106)Peak memory usage: 89 MB
% 18.30/4.03 % (1436106)Instructions burned: 115 (million)
% 18.30/4.03 % (1436108)------------------------------
% 18.30/4.03 % (1436108)------------------------------
% 18.30/4.03 % (1436107)Instruction limit reached!
% 18.30/4.03 % (1436107)------------------------------
% 18.30/4.03 % (1436107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/4.03 % (1436107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/4.03 % (1436107)CaDiCaL version: 2.1.3
% 18.30/4.03 % (1436107)Termination reason: Instruction limit
% 18.30/4.03 % (1436107)Termination phase: Saturation
% 18.30/4.03 % (1436107)Time elapsed: 0.166 s
% 18.30/4.03 % (1436107)Peak memory usage: 89 MB
% 18.30/4.03 % (1436107)Instructions burned: 180 (million)
% 18.30/4.03 % (1436120)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=167553967:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 18.30/4.03 % (1436120)Refutation not found, incomplete strategy
% 18.30/4.03 % (1436120)------------------------------
% 18.30/4.03 % (1436120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.30/4.03 % (1436120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.30/4.03 % (1436120)CaDiCaL version: 2.1.3
% 18.30/4.03 % (1436120)Termination reason: Refutation not found, incomplete strategy
% 18.30/4.03 % (1436120)Time elapsed: 0.001 s
% 18.30/4.03 % (1436120)Peak memory usage: 88 MB
% 18.30/4.03 % (1436118)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=940969594:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 35.42/6.27 % (1436119)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1230477577: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)
% 35.42/6.27 % (1436118)Refutation not found, incomplete strategy
% 35.42/6.27 % (1436118)------------------------------
% 35.42/6.27 % (1436118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/6.27 % (1436118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/6.27 % (1436118)CaDiCaL version: 2.1.3
% 35.42/6.27 % (1436118)Termination reason: Refutation not found, incomplete strategy
% 35.42/6.27 % (1436118)Time elapsed: 0.002 s
% 35.42/6.27 % (1436118)Peak memory usage: 87 MB
% 35.42/6.27 % (1436119)Refutation not found, incomplete strategy
% 35.42/6.27 % (1436119)------------------------------
% 35.42/6.27 % (1436119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/6.27 % (1436119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/6.27 % (1436119)CaDiCaL version: 2.1.3
% 35.42/6.27 % (1436119)Termination reason: Refutation not found, incomplete strategy
% 35.42/6.27 % (1436119)Time elapsed: 0.002 s
% 35.42/6.27 % (1436119)Peak memory usage: 88 MB
% 35.42/6.27 % (1436119)Instructions burned: 1 (million)
% 35.42/6.27 % (1436121)lrs+10_64_to=lpo:sil=8000:random_seed=2121278181:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 35.42/6.27 % (1436121)Instruction limit reached!
% 35.42/6.27 % (1436121)------------------------------
% 35.42/6.27 % (1436121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/6.27 % (1436121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/6.27 % (1436121)CaDiCaL version: 2.1.3
% 35.42/6.27 % (1436121)Termination reason: Instruction limit
% 35.42/6.27 % (1436121)Termination phase: Saturation
% 35.42/6.27 % (1436121)Time elapsed: 0.126 s
% 35.42/6.27 % (1436121)Peak memory usage: 88 MB
% 35.42/6.27 % (1436121)Instructions burned: 126 (million)
% 35.42/6.27 % (1436120)------------------------------
% 35.42/6.27 % (1436120)------------------------------
% 35.42/6.27 % (1436119)------------------------------
% 35.42/6.27 % (1436119)------------------------------
% 35.42/6.27 % (1436118)------------------------------
% 35.42/6.27 % (1436118)------------------------------
% 35.42/6.27 % (1436127)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3093122453:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 35.42/6.27 % (1436126)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3438046684:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 35.42/6.27 % (1436127)Instruction limit reached!
% 35.42/6.27 % (1436127)------------------------------
% 35.42/6.27 % (1436127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/6.27 % (1436127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/6.27 % (1436127)CaDiCaL version: 2.1.3
% 35.42/6.27 % (1436127)Termination reason: Instruction limit
% 35.42/6.27 % (1436127)Termination phase: Saturation
% 35.42/6.27 % (1436127)Time elapsed: 0.084 s
% 35.42/6.27 % (1436127)Peak memory usage: 90 MB
% 35.42/6.27 % (1436127)Instructions burned: 158 (million)
% 35.42/6.27 % (1436126)Instruction limit reached!
% 35.42/6.27 % (1436126)------------------------------
% 35.42/6.27 % (1436126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.42/6.27 % (1436126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.42/6.27 % (1436126)CaDiCaL version: 2.1.3
% 35.42/6.27 % (1436126)Termination reason: Instruction limit
% 35.42/6.27 % (1436126)Termination phase: Saturation
% 35.42/6.27 % (1436126)Time elapsed: 0.197 s
% 35.42/6.27 % (1436126)Peak memory usage: 89 MB
% 35.42/6.27 % (1436126)Instructions burned: 194 (million)
% 35.42/6.27 % (1436129)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=30979098:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 35.42/6.27 % (1436130)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=3651261617:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 35.42/6.27 % (1436130)Instruction limit reached!
% 35.42/6.27 % (1436130)------------------------------
% 45.36/8.47 % (1436130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/8.47 % (1436130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/8.47 % (1436130)CaDiCaL version: 2.1.3
% 45.36/8.47 % (1436130)Termination reason: Instruction limit
% 45.36/8.47 % (1436130)Termination phase: Saturation
% 45.36/8.47 % (1436130)Time elapsed: 0.110 s
% 45.36/8.47 % (1436130)Peak memory usage: 89 MB
% 45.36/8.47 % (1436130)Instructions burned: 106 (million)
% 45.36/8.47 % (1436133)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2153010583:i=107_2987 on theBenchmark for (2987ds/107Mi)
% 45.36/8.47 % (1436133)Refutation not found, incomplete strategy
% 45.36/8.47 % (1436133)------------------------------
% 45.36/8.47 % (1436133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/8.47 % (1436133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/8.47 % (1436133)CaDiCaL version: 2.1.3
% 45.36/8.47 % (1436133)Termination reason: Refutation not found, incomplete strategy
% 45.36/8.47 % (1436133)Time elapsed: 0.001 s
% 45.36/8.47 % (1436133)Peak memory usage: 87 MB
% 45.36/8.47 % (1436134)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3701091812:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 45.36/8.47 % (1436133)------------------------------
% 45.36/8.47 % (1436133)------------------------------
% 45.36/8.47 % (1436138)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=435741109:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 45.36/8.47 % (1436134)Instruction limit reached!
% 45.36/8.47 % (1436134)------------------------------
% 45.36/8.47 % (1436134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/8.47 % (1436134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/8.47 % (1436134)CaDiCaL version: 2.1.3
% 45.36/8.47 % (1436134)Termination reason: Instruction limit
% 45.36/8.47 % (1436134)Termination phase: Saturation
% 45.36/8.47 % (1436134)Time elapsed: 0.242 s
% 45.36/8.47 % (1436134)Peak memory usage: 90 MB
% 45.36/8.47 % (1436134)Instructions burned: 242 (million)
% 45.36/8.47 % (1436140)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2367777952:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 45.36/8.47 % (1436140)Instruction limit reached!
% 45.36/8.47 % (1436140)------------------------------
% 45.36/8.47 % (1436140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/8.47 % (1436140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/8.47 % (1436140)CaDiCaL version: 2.1.3
% 45.36/8.47 % (1436140)Termination reason: Instruction limit
% 45.36/8.47 % (1436140)Termination phase: Saturation
% 45.36/8.47 % (1436140)Time elapsed: 0.069 s
% 45.36/8.47 % (1436140)Peak memory usage: 89 MB
% 45.36/8.47 % (1436140)Instructions burned: 135 (million)
% 45.36/8.47 % (1436142)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2817999833:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 45.36/8.47 % (1436144)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3134544529:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 45.36/8.47 % (1436144)Instruction limit reached!
% 45.36/8.47 % (1436144)------------------------------
% 45.36/8.47 % (1436144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/8.47 % (1436144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/8.47 % (1436144)CaDiCaL version: 2.1.3
% 45.36/8.47 % (1436144)Termination reason: Instruction limit
% 45.36/8.47 % (1436144)Termination phase: Saturation
% 45.36/8.47 % (1436144)Time elapsed: 0.104 s
% 45.36/8.47 % (1436144)Peak memory usage: 91 MB
% 45.36/8.47 % (1436144)Instructions burned: 191 (million)
% 45.36/8.47 % (1436142)Instruction limit reached!
% 45.36/8.47 % (1436142)------------------------------
% 45.36/8.47 % (1436142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/8.47 % (1436142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/8.47 % (1436142)CaDiCaL version: 2.1.3
% 45.36/8.47 % (1436142)Termination reason: Instruction limit
% 45.36/8.47 % (1436142)Termination phase: Saturation
% 45.36/8.47 % (1436142)Time elapsed: 0.510 s
% 45.36/8.47 % (1436142)Peak memory usage: 95 MB
% 45.36/8.47 % (1436142)Instructions burned: 499 (million)
% 52.55/8.74 % (1436147)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3924956856:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 52.55/8.74 % (1436147)Instruction limit reached!
% 52.55/8.74 % (1436147)------------------------------
% 52.55/8.74 % (1436147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436147)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436147)Termination reason: Instruction limit
% 52.55/8.74 % (1436147)Termination phase: Saturation
% 52.55/8.74 % (1436147)Time elapsed: 0.139 s
% 52.55/8.74 % (1436147)Peak memory usage: 91 MB
% 52.55/8.74 % (1436147)Instructions burned: 265 (million)
% 52.55/8.74 % (1436149)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3567353701:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi)
% 52.55/8.74 % (1436150)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=3775828975:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 52.55/8.74 % (1436149)Instruction limit reached!
% 52.55/8.74 % (1436149)------------------------------
% 52.55/8.74 % (1436149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436149)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436149)Termination reason: Instruction limit
% 52.55/8.74 % (1436149)Termination phase: Saturation
% 52.55/8.74 % (1436149)Time elapsed: 0.161 s
% 52.55/8.74 % (1436149)Peak memory usage: 89 MB
% 52.55/8.74 % (1436149)Instructions burned: 157 (million)
% 52.55/8.74 % (1436153)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=470767176:i=537:av=off:ss=included_2968 on theBenchmark for (2968ds/537Mi)
% 52.55/8.74 % (1436153)Instruction limit reached!
% 52.55/8.74 % (1436153)------------------------------
% 52.55/8.74 % (1436153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436153)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436153)Termination reason: Instruction limit
% 52.55/8.74 % (1436153)Termination phase: Saturation
% 52.55/8.74 % (1436153)Time elapsed: 0.504 s
% 52.55/8.74 % (1436153)Peak memory usage: 93 MB
% 52.55/8.74 % (1436153)Instructions burned: 537 (million)
% 52.55/8.74 % (1436155)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=204187390:i=180:bd=preordered:av=off_2959 on theBenchmark for (2959ds/180Mi)
% 52.55/8.74 % (1436155)Instruction limit reached!
% 52.55/8.74 % (1436155)------------------------------
% 52.55/8.74 % (1436155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436155)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436155)Termination reason: Instruction limit
% 52.55/8.74 % (1436155)Termination phase: Saturation
% 52.55/8.74 % (1436155)Time elapsed: 0.171 s
% 52.55/8.74 % (1436155)Peak memory usage: 88 MB
% 52.55/8.74 % (1436155)Instructions burned: 180 (million)
% 52.55/8.74 % (1436157)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=1455888561:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2955 on theBenchmark for (2955ds/10307Mi)
% 52.55/8.74 % (1436129)Instruction limit reached!
% 52.55/8.74 % (1436129)------------------------------
% 52.55/8.74 % (1436129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436129)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436129)Termination reason: Instruction limit
% 52.55/8.74 % (1436129)Termination phase: Saturation
% 52.55/8.74 % (1436129)Time elapsed: 3.513 s
% 52.55/8.74 % (1436129)Peak memory usage: 148 MB
% 52.55/8.74 % (1436129)Instructions burned: 3395 (million)
% 52.55/8.74 % (1436150)Instruction limit reached!
% 52.55/8.74 % (1436150)------------------------------
% 52.55/8.74 % (1436150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436150)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436150)Termination reason: Instruction limit
% 52.55/8.74 % (1436150)Termination phase: Saturation
% 52.55/8.74 % (1436150)Time elapsed: 1.816 s
% 52.55/8.74 % (1436150)Peak memory usage: 148 MB
% 52.55/8.74 % (1436150)Instructions burned: 3257 (million)
% 52.55/8.74 % (1436159)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=3316846161:i=412:gtgl=4:gtg=exists_all_2950 on theBenchmark for (2950ds/412Mi)
% 52.55/8.74 % (1436160)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=1291163656:s2pl=no:i=8478:s2at=4:nm=6_2950 on theBenchmark for (2950ds/8478Mi)
% 52.55/8.74 % (1436159)Instruction limit reached!
% 52.55/8.74 % (1436159)------------------------------
% 52.55/8.74 % (1436159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436159)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436159)Termination reason: Instruction limit
% 52.55/8.74 % (1436159)Termination phase: Saturation
% 52.55/8.74 % (1436159)Time elapsed: 0.407 s
% 52.55/8.74 % (1436159)Peak memory usage: 94 MB
% 52.55/8.74 % (1436159)Instructions burned: 412 (million)
% 52.55/8.74 % (1436163)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3187937023:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2944 on theBenchmark for (2944ds/303Mi)
% 52.55/8.74 % (1436163)Refutation not found, incomplete strategy
% 52.55/8.74 % (1436163)------------------------------
% 52.55/8.74 % (1436163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436163)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436163)Termination reason: Refutation not found, incomplete strategy
% 52.55/8.74 % (1436163)Time elapsed: 0.002 s
% 52.55/8.74 % (1436163)Peak memory usage: 88 MB
% 52.55/8.74 % (1436163)Instructions burned: 1 (million)
% 52.55/8.74 % (1436163)------------------------------
% 52.55/8.74 % (1436163)------------------------------
% 52.55/8.74 % (1436165)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3854394395:st=4:i=720:sd=3:fsr=off:ss=axioms_2938 on theBenchmark for (2938ds/720Mi)
% 52.55/8.74 % (1436165)Refutation not found, incomplete strategy
% 52.55/8.74 % (1436165)------------------------------
% 52.55/8.74 % (1436165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436165)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436165)Termination reason: Refutation not found, incomplete strategy
% 52.55/8.74 % (1436165)Time elapsed: 0.001 s
% 52.55/8.74 % (1436165)Peak memory usage: 88 MB
% 52.55/8.74 % (1436165)------------------------------
% 52.55/8.74 % (1436165)------------------------------
% 52.55/8.74 % (1436167)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=795388920:i=598:bs=on:bd=preordered:av=off:ss=axioms_2933 on theBenchmark for (2933ds/598Mi)
% 52.55/8.74 % (1436167)Instruction limit reached!
% 52.55/8.74 % (1436167)------------------------------
% 52.55/8.74 % (1436167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436167)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436167)Termination reason: Instruction limit
% 52.55/8.74 % (1436167)Termination phase: Saturation
% 52.55/8.74 % (1436167)Time elapsed: 0.199 s
% 52.55/8.74 % (1436167)Peak memory usage: 94 MB
% 52.55/8.74 % (1436167)Instructions burned: 600 (million)
% 52.55/8.74 % (1436138)Instruction limit reached!
% 52.55/8.74 % (1436138)------------------------------
% 52.55/8.74 % (1436138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.55/8.74 % (1436138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.55/8.74 % (1436138)CaDiCaL version: 2.1.3
% 52.55/8.74 % (1436138)Termination reason: Instruction limit
% 52.55/8.74 % (1436138)Termination phase: Saturation
% 52.55/8.74 % (1436138)Time elapsed: 5.292 s
% 52.55/8.74 % (1436138)Peak memory usage: 166 MB
% 52.55/8.74 % (1436138)Instructions burned: 5209 (million)
% 52.55/8.74 % (1436104)First to succeed.
% 52.55/8.74 % (1436104)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1436097"
% 52.55/8.74 % (1436229)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3334302868:i=2989:sd=3:ss=axioms:sgt=60_2929 on theBenchmark for (2929ds/2989Mi)
% 52.55/8.74 % (1436245)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3238004575:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2929 on theBenchmark for (2929ds/1997Mi)
% 52.55/8.74 % (1436104)Refutation found. Thanks to Tanya!
% 52.55/8.74 % SZS status Unsatisfiable for theBenchmark
% 52.55/8.74 % SZS output start Proof for theBenchmark
% See solution above
% 53.65/8.96 % (1436104)------------------------------
% 53.65/8.96 % (1436104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.65/8.96 % (1436104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.65/8.96 % (1436104)CaDiCaL version: 2.1.3
% 53.65/8.96 % (1436104)Termination reason: Refutation
% 53.65/8.96 % (1436104)Time elapsed: 6.873 s
% 53.65/8.96 % (1436104)Peak memory usage: 172 MB
% 53.65/8.96 % (1436104)Instructions burned: 6644 (million)
% 53.65/8.96 % (1436104)------------------------------
% 53.65/8.96 % (1436104)------------------------------
% 53.65/8.96 % (1436097)Success in time 7.431 s
% 53.65/8.96 % Vampire exiting
%------------------------------------------------------------------------------