%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT178-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:09 AM UTC 2026
% Result : Unsatisfiable 83.21s 20.30s
% Output : Refutation 97.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 18
% Syntax : Number of formulae : 340 ( 319 unt; 5 def)
% Number of atoms : 367 ( 366 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 56 ( 29 ~; 27 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 7 ( 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 : 611 ( 611 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_meet) ).
fof(f2,axiom,
! [X0] : join(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
fof(f4,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
fof(f6,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
fof(f7,axiom,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_meet) ).
fof(f8,axiom,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_join) ).
fof(f9,axiom,
! [X0] : join(X0,complement(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_join) ).
fof(f10,axiom,
! [X0] : meet(X0,complement(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement_meet) ).
fof(f11,axiom,
! [X0,X1] :
( join(X0,X1) != one
| meet(X0,X1) != zero
| complement(X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',meet_join_complement) ).
fof(f12,axiom,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,X3)))) = meet(X0,join(X1,meet(X2,join(X0,meet(X2,X3))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',equation_H1) ).
fof(f13,negated_conjecture,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_distributivity) ).
fof(f14,definition,
sF0 = join(b,c),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f15,plain,
join(b,c) = sF0,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF1 = meet(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f17,plain,
meet(a,sF0) = sF1,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF2 = meet(a,b),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f19,plain,
meet(a,b) = sF2,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF3 = meet(a,c),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f21,plain,
meet(a,c) = sF3,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF4 = join(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f23,plain,
join(sF2,sF3) = sF4,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
sF1 != sF4,
inference(definition_folding,[],[f13,f23,f21,f19,f17,f15]) ).
fof(f25,plain,
sF2 = meet(b,a),
inference(forward_demodulation,[],[f19,f5]) ).
fof(f26,plain,
sF3 = meet(c,a),
inference(forward_demodulation,[],[f21,f5]) ).
fof(f32,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f34,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f36,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f34,f4]) ).
fof(f41,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f36,f5]) ).
fof(f42,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f32,f3]) ).
fof(f43,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f32,f34]) ).
fof(f47,plain,
a = join(a,sF3),
inference(superposition,[],[f32,f26]) ).
fof(f51,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f43,f6]) ).
fof(f52,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f42,f6]) ).
fof(f55,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f56,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f32]) ).
fof(f58,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f8,f6]) ).
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(f68,plain,
! [X2,X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X0,join(X1,X2))),
inference(superposition,[],[f3,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(f100,plain,
! [X0] : meet(b,meet(a,X0)) = meet(sF2,X0),
inference(superposition,[],[f7,f25]) ).
fof(f101,plain,
! [X0] : meet(c,meet(a,X0)) = meet(sF3,X0),
inference(superposition,[],[f7,f26]) ).
fof(f110,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f117,plain,
sF2 = meet(sF2,sF4),
inference(superposition,[],[f3,f23]) ).
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,
! [X0] : one = join(one,X0),
inference(superposition,[],[f32,f159]) ).
fof(f171,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f159]) ).
fof(f176,plain,
! [X0,X1] : one = join(X0,join(complement(X0),X1)),
inference(backward_demodulation,[],[f160,f169]) ).
fof(f189,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f34,f171]) ).
fof(f220,plain,
! [X0,X1] : meet(X0,meet(complement(X0),X1)) = meet(zero,X1),
inference(superposition,[],[f7,f10]) ).
fof(f222,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f223,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f224,plain,
! [X0,X1] : meet(X0,complement(join(X0,X1))) = meet(X0,zero),
inference(superposition,[],[f94,f10]) ).
fof(f225,plain,
zero = complement(one),
inference(superposition,[],[f171,f10]) ).
fof(f232,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f222]) ).
fof(f235,plain,
! [X0] : zero = meet(zero,X0),
inference(superposition,[],[f34,f222]) ).
fof(f238,plain,
! [X0,X1] : zero = meet(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f220,f235]) ).
fof(f252,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f32,f232]) ).
fof(f255,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(backward_demodulation,[],[f224,f252]) ).
fof(f310,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X1,join(X2,X0)))) = meet(X2,join(X3,meet(X1,join(X2,meet(X0,X1))))),
inference(superposition,[],[f12,f5]) ).
fof(f316,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,zero)))) = meet(X0,join(X1,meet(X2,join(X0,complement(join(X2,X3)))))),
inference(superposition,[],[f12,f255]) ).
fof(f338,plain,
! [X2,X3,X0,X1] : meet(X1,join(X3,meet(X0,join(X1,X2)))) = meet(X1,join(meet(X0,join(X1,meet(X0,X2))),X3)),
inference(superposition,[],[f12,f6]) ).
fof(f375,plain,
! [X2,X3,X0,X1] : meet(X0,join(X1,meet(X2,X0))) = meet(X0,join(X1,meet(X2,join(X0,complement(join(X2,X3)))))),
inference(forward_demodulation,[],[f316,f222]) ).
fof(f429,plain,
! [X2,X0,X1] : meet(X1,join(zero,meet(X0,X1))) = meet(X1,meet(X0,join(X1,complement(join(X0,X2))))),
inference(superposition,[],[f375,f232]) ).
fof(f453,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(zero,meet(X0,X1))),
inference(forward_demodulation,[],[f429,f141]) ).
fof(f465,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f453,f232]) ).
fof(f472,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f465,f94]) ).
fof(f481,plain,
meet(sF0,a) = meet(sF0,sF1),
inference(superposition,[],[f465,f17]) ).
fof(f482,plain,
meet(a,b) = meet(a,sF2),
inference(superposition,[],[f465,f25]) ).
fof(f483,plain,
meet(a,c) = meet(a,sF3),
inference(superposition,[],[f465,f26]) ).
fof(f490,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(meet(X1,X0),X2)),
inference(superposition,[],[f7,f465]) ).
fof(f492,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f32,f465]) ).
fof(f500,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f490,f7]) ).
fof(f504,plain,
meet(c,a) = meet(a,sF3),
inference(forward_demodulation,[],[f483,f5]) ).
fof(f505,plain,
meet(b,a) = meet(a,sF2),
inference(forward_demodulation,[],[f482,f5]) ).
fof(f506,plain,
meet(a,sF0) = meet(sF0,sF1),
inference(forward_demodulation,[],[f481,f5]) ).
fof(f514,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f472,f5]) ).
fof(f516,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X0,X2))),
inference(forward_demodulation,[],[f500,f7]) ).
fof(f518,plain,
sF3 = meet(a,sF3),
inference(forward_demodulation,[],[f504,f26]) ).
fof(f519,plain,
sF2 = meet(a,sF2),
inference(forward_demodulation,[],[f505,f25]) ).
fof(f520,plain,
sF1 = meet(sF0,sF1),
inference(forward_demodulation,[],[f506,f17]) ).
fof(f526,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(meet(X0,X1),join(X0,X2))),
inference(forward_demodulation,[],[f514,f110]) ).
fof(f532,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f526,f7]) ).
fof(f535,plain,
! [X2,X0,X1] : meet(meet(join(X0,X2),X1),X0) = meet(X1,meet(X0,join(X0,X2))),
inference(forward_demodulation,[],[f532,f516]) ).
fof(f536,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(meet(join(X0,X2),X1),X0),
inference(forward_demodulation,[],[f535,f3]) ).
fof(f537,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f536,f5]) ).
fof(f675,plain,
! [X0] : join(a,X0) = join(a,join(sF2,X0)),
inference(superposition,[],[f55,f519]) ).
fof(f677,plain,
! [X0] : join(b,X0) = join(b,join(sF2,X0)),
inference(superposition,[],[f55,f25]) ).
fof(f685,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f55,f9]) ).
fof(f707,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f685,f189]) ).
fof(f717,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f223,f5]) ).
fof(f798,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X2),join(X0,X2)))) = meet(X0,join(X1,meet(complement(X2),join(X0,zero)))),
inference(superposition,[],[f310,f10]) ).
fof(f872,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(X2),join(X0,X2)))) = meet(X0,join(X1,meet(complement(X2),X0))),
inference(forward_demodulation,[],[f798,f222]) ).
fof(f948,plain,
! [X0,X1] : one = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f707,f5]) ).
fof(f1007,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f95,f4]) ).
fof(f1017,plain,
! [X0] : meet(c,X0) = meet(c,meet(sF0,X0)),
inference(superposition,[],[f95,f15]) ).
fof(f1020,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f95,f5]) ).
fof(f1087,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f1007,f110]) ).
fof(f1102,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f1087,f516]) ).
fof(f1109,plain,
! [X0,X1] : one = join(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f163,f6]) ).
fof(f1178,plain,
! [X0,X1] : one = join(meet(X1,X0),complement(meet(X0,X1))),
inference(superposition,[],[f948,f465]) ).
fof(f1299,plain,
! [X2,X0,X1] : meet(X0,zero) = meet(X0,meet(X1,complement(meet(X1,join(X2,X0))))),
inference(superposition,[],[f95,f717]) ).
fof(f1304,plain,
! [X2,X0,X1] : zero = meet(X0,meet(X1,complement(meet(X1,join(X2,X0))))),
inference(forward_demodulation,[],[f1299,f252]) ).
fof(f1416,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(complement(X0),X1))) = meet(X1,join(X2,meet(complement(X0),join(X0,X1)))),
inference(superposition,[],[f872,f6]) ).
fof(f1519,plain,
meet(sF3,sF0) = meet(c,sF1),
inference(superposition,[],[f101,f17]) ).
fof(f1521,plain,
meet(sF3,sF3) = meet(c,sF3),
inference(superposition,[],[f101,f518]) ).
fof(f1588,plain,
sF3 = meet(c,sF3),
inference(forward_demodulation,[],[f1521,f1]) ).
fof(f1590,plain,
meet(c,sF1) = meet(sF0,sF3),
inference(forward_demodulation,[],[f1519,f5]) ).
fof(f1617,plain,
meet(sF2,sF0) = meet(b,sF1),
inference(superposition,[],[f100,f17]) ).
fof(f1618,plain,
meet(sF2,sF2) = meet(b,sF2),
inference(superposition,[],[f100,f519]) ).
fof(f1687,plain,
sF2 = meet(b,sF2),
inference(forward_demodulation,[],[f1618,f1]) ).
fof(f1688,plain,
meet(b,sF1) = meet(sF0,sF2),
inference(forward_demodulation,[],[f1617,f5]) ).
fof(f2031,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(join(X1,X0),join(X0,X2)),
inference(superposition,[],[f56,f34]) ).
fof(f2056,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f56,f6]) ).
fof(f2114,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X0,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f2031,f67]) ).
fof(f2133,plain,
! [X2,X0,X1] : join(X1,join(X0,X2)) = join(X0,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f2114,f8]) ).
fof(f2223,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,join(X1,complement(join(X1,X0))))
| complement(X0) = join(X1,complement(join(X1,X0))) ),
inference(superposition,[],[f11,f1109]) ).
fof(f2238,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X1,X0))))
| complement(X0) = join(X1,complement(join(X1,X0))) ),
inference(trivial_inequality_removal,[],[f2223]) ).
fof(f2628,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(join(X1,X2),X0),meet(X0,X1)),
inference(superposition,[],[f32,f537]) ).
fof(f2659,plain,
! [X2,X0,X1] : meet(join(X1,X2),X0) = join(meet(X0,X1),meet(join(X1,X2),X0)),
inference(forward_demodulation,[],[f2628,f6]) ).
fof(f3265,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(join(X1,X0),X1)),
inference(superposition,[],[f2,f67]) ).
fof(f3334,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,join(X1,X0))),
inference(forward_demodulation,[],[f3265,f6]) ).
fof(f3388,plain,
! [X0,X1] : join(X1,X0) = join(X1,join(X0,X1)),
inference(forward_demodulation,[],[f3334,f2133]) ).
fof(f3599,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(join(complement(X0),X2)),X0))) = meet(X0,join(X1,meet(complement(join(complement(X0),X2)),one))),
inference(superposition,[],[f872,f176]) ).
fof(f3616,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(join(complement(X0),X2)),X0))) = meet(X0,join(X1,meet(one,complement(join(complement(X0),X2))))),
inference(forward_demodulation,[],[f3599,f5]) ).
fof(f3633,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(complement(join(complement(X0),X2)),X0))) = meet(X0,join(X1,complement(join(complement(X0),X2)))),
inference(forward_demodulation,[],[f3616,f171]) ).
fof(f3643,plain,
! [X2,X0,X1] : meet(X0,join(X1,complement(join(complement(X0),X2)))) = meet(X0,join(X1,meet(X0,complement(join(complement(X0),X2))))),
inference(forward_demodulation,[],[f3633,f5]) ).
fof(f3977,plain,
! [X2,X0,X1] : meet(X1,join(X2,meet(X0,join(X1,X0)))) = meet(X1,join(meet(X0,join(X1,X0)),X2)),
inference(superposition,[],[f338,f1]) ).
fof(f4001,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(meet(X2,join(X0,zero)),X1)),
inference(superposition,[],[f338,f10]) ).
fof(f4198,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,complement(X2))))) = meet(X0,join(meet(X2,X0),X1)),
inference(forward_demodulation,[],[f4001,f222]) ).
fof(f4218,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,X2)),
inference(forward_demodulation,[],[f3977,f34]) ).
fof(f4506,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = meet(X1,join(meet(X0,join(X1,complement(X0))),X2)),
inference(superposition,[],[f4198,f6]) ).
fof(f4968,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f5,f4218]) ).
fof(f5062,plain,
sF4 = join(sF2,sF4),
inference(superposition,[],[f52,f23]) ).
fof(f5197,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X1,join(X2,X0)),meet(X0,X1)),
inference(superposition,[],[f32,f1020]) ).
fof(f5244,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(X1,join(X2,X0))),
inference(forward_demodulation,[],[f5197,f6]) ).
fof(f5609,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,X1)),
inference(superposition,[],[f7,f1102]) ).
fof(f6074,plain,
! [X0] :
( one != one
| zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(superposition,[],[f76,f9]) ).
fof(f6093,plain,
! [X0] :
( zero != meet(complement(X0),X0)
| complement(complement(X0)) = X0 ),
inference(trivial_inequality_removal,[],[f6074]) ).
fof(f6106,plain,
! [X0] :
( meet(X0,complement(X0)) != zero
| complement(complement(X0)) = X0 ),
inference(forward_demodulation,[],[f6093,f5]) ).
fof(f6121,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_subsumption_resolution,[],[f6106,f10]) ).
fof(f6681,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),join(X2,meet(complement(X0),complement(meet(X0,X1))))) = meet(complement(meet(X0,X1)),join(X2,meet(complement(X0),one))),
inference(superposition,[],[f1416,f707]) ).
fof(f6823,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),join(X2,meet(complement(X0),complement(meet(X0,X1))))) = meet(complement(meet(X0,X1)),join(X2,meet(one,complement(X0)))),
inference(forward_demodulation,[],[f6681,f5]) ).
fof(f6868,plain,
! [X2,X0,X1] : meet(complement(meet(X0,X1)),join(X2,meet(complement(X0),complement(meet(X0,X1))))) = meet(complement(meet(X0,X1)),join(X2,complement(X0))),
inference(forward_demodulation,[],[f6823,f171]) ).
fof(f7002,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f2659,f222]) ).
fof(f7544,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(meet(X0,X1),join(X2,meet(X1,X0))),
inference(superposition,[],[f67,f7002]) ).
fof(f9266,plain,
join(a,sF3) = join(a,sF4),
inference(superposition,[],[f675,f23]) ).
fof(f9364,plain,
a = join(a,sF4),
inference(forward_demodulation,[],[f9266,f47]) ).
fof(f9397,plain,
sF4 = meet(sF4,a),
inference(superposition,[],[f34,f9364]) ).
fof(f9426,plain,
sF4 = meet(a,sF4),
inference(forward_demodulation,[],[f9397,f5]) ).
fof(f9431,plain,
meet(sF2,sF4) = meet(b,sF4),
inference(superposition,[],[f100,f9426]) ).
fof(f9468,plain,
sF2 = meet(b,sF4),
inference(forward_demodulation,[],[f9431,f117]) ).
fof(f12348,plain,
meet(c,sF3) = meet(c,meet(c,sF1)),
inference(superposition,[],[f1017,f1590]) ).
fof(f12517,plain,
meet(c,sF1) = meet(c,sF3),
inference(forward_demodulation,[],[f12348,f41]) ).
fof(f12549,plain,
sF3 = meet(c,sF1),
inference(forward_demodulation,[],[f12517,f1588]) ).
fof(f12862,plain,
! [X0] : meet(sF0,X0) = join(meet(b,X0),meet(sF0,X0)),
inference(superposition,[],[f149,f15]) ).
fof(f13589,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(meet(X1,X0),complement(meet(X1,join(X0,complement(X1)))))),
inference(superposition,[],[f4506,f9]) ).
fof(f13773,plain,
! [X0,X1] : meet(X0,join(meet(X1,X0),complement(meet(X1,join(X0,complement(X1)))))) = X0,
inference(forward_demodulation,[],[f13589,f159]) ).
fof(f16454,plain,
meet(sF0,a) = join(sF2,meet(sF0,a)),
inference(superposition,[],[f12862,f25]) ).
fof(f16456,plain,
meet(sF0,sF2) = join(sF2,meet(sF0,sF2)),
inference(superposition,[],[f12862,f1687]) ).
fof(f16701,plain,
sF2 = meet(sF0,sF2),
inference(forward_demodulation,[],[f16456,f32]) ).
fof(f16703,plain,
meet(a,sF0) = join(sF2,meet(a,sF0)),
inference(forward_demodulation,[],[f16454,f5]) ).
fof(f16756,plain,
sF2 = meet(b,sF1),
inference(backward_demodulation,[],[f1688,f16701]) ).
fof(f16757,plain,
sF1 = join(sF2,sF1),
inference(forward_demodulation,[],[f16703,f17]) ).
fof(f16809,plain,
sF1 = join(sF1,sF2),
inference(forward_demodulation,[],[f16757,f6]) ).
fof(f19493,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,f1178]) ).
fof(f19527,plain,
! [X0,X1] :
( zero != meet(meet(X0,X1),complement(meet(X1,X0)))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(trivial_inequality_removal,[],[f19493]) ).
fof(f19555,plain,
! [X0,X1] :
( zero != meet(X0,meet(X1,complement(meet(X1,X0))))
| complement(meet(X0,X1)) = complement(meet(X1,X0)) ),
inference(forward_demodulation,[],[f19527,f7]) ).
fof(f19722,plain,
! [X0,X1] : complement(meet(X0,X1)) = complement(meet(X1,X0)),
inference(forward_subsumption_resolution,[],[f19555,f717]) ).
fof(f20293,plain,
! [X0,X1] : meet(X1,join(meet(X0,X1),complement(meet(X0,join(complement(X0),X1))))) = X1,
inference(superposition,[],[f13773,f4218]) ).
fof(f25161,plain,
! [X2,X0,X1] : meet(complement(X0),join(X1,complement(join(X0,X2)))) = meet(complement(X0),join(X1,meet(complement(X0),complement(join(X0,X2))))),
inference(superposition,[],[f3643,f6121]) ).
fof(f25530,plain,
! [X2,X0,X1] : meet(complement(meet(X1,X0)),join(X2,complement(meet(X0,X1)))) = meet(complement(meet(X1,X0)),join(X2,meet(complement(meet(X1,X0)),complement(meet(X0,X1))))),
inference(superposition,[],[f25161,f7002]) ).
fof(f25995,plain,
join(b,sF3) = join(b,sF4),
inference(superposition,[],[f677,f23]) ).
fof(f37089,plain,
! [X0,X1] : join(meet(X1,X0),complement(meet(X1,join(complement(X1),X0)))) = join(join(meet(X1,X0),complement(meet(X1,join(complement(X1),X0)))),X0),
inference(superposition,[],[f32,f20293]) ).
fof(f37196,plain,
! [X0,X1] : join(meet(X1,X0),complement(meet(X1,join(complement(X1),X0)))) = join(X0,join(meet(X1,X0),complement(meet(X1,join(complement(X1),X0))))),
inference(forward_demodulation,[],[f37089,f6]) ).
fof(f37355,plain,
! [X0,X1] : join(meet(X1,X0),complement(meet(X1,join(complement(X1),X0)))) = join(X0,complement(meet(X1,join(complement(X1),X0)))),
inference(forward_demodulation,[],[f37196,f56]) ).
fof(f38886,plain,
! [X2,X0,X1] : join(X2,meet(complement(X0),complement(meet(X0,X1)))) = join(join(X2,meet(complement(X0),complement(meet(X0,X1)))),meet(complement(meet(X0,X1)),join(X2,complement(X0)))),
inference(superposition,[],[f32,f6868]) ).
fof(f38955,plain,
! [X2,X0,X1] : join(X2,meet(complement(X0),complement(meet(X0,X1)))) = join(X2,join(meet(complement(X0),complement(meet(X0,X1))),meet(complement(meet(X0,X1)),join(X2,complement(X0))))),
inference(forward_demodulation,[],[f38886,f8]) ).
fof(f39033,plain,
! [X2,X0,X1] : join(X2,meet(complement(X0),complement(meet(X0,X1)))) = join(X2,meet(complement(meet(X0,X1)),join(X2,complement(X0)))),
inference(forward_demodulation,[],[f38955,f5244]) ).
fof(f41286,plain,
! [X2,X3,X0,X1] : join(join(X1,join(X2,X0)),X3) = join(join(X1,join(X2,X0)),join(X0,X3)),
inference(superposition,[],[f56,f65]) ).
fof(f41404,plain,
! [X2,X3,X0,X1] : join(join(X1,join(X2,X0)),X3) = join(X0,join(X3,join(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f41286,f67]) ).
fof(f41481,plain,
! [X2,X3,X0,X1] : join(X1,join(join(X2,X0),X3)) = join(X0,join(X3,join(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f41404,f8]) ).
fof(f41493,plain,
! [X2,X3,X0,X1] : join(X1,join(X2,join(X0,X3))) = join(X0,join(X3,join(X1,join(X2,X0)))),
inference(forward_demodulation,[],[f41481,f8]) ).
fof(f42930,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,join(X2,join(X0,X1)))),
inference(superposition,[],[f58,f3388]) ).
fof(f42978,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X2,join(X0,join(X1,X0))),
inference(forward_demodulation,[],[f42930,f41493]) ).
fof(f43088,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X2,join(X1,X0)),
inference(forward_demodulation,[],[f42978,f51]) ).
fof(f43269,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f43088,f492]) ).
fof(f43893,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f43269,f492]) ).
fof(f44481,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X2,X1)),
inference(superposition,[],[f6,f43893]) ).
fof(f44522,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(X1,X2)),X3) = meet(X3,join(X0,meet(X2,X1))),
inference(superposition,[],[f4968,f43893]) ).
fof(f48522,plain,
! [X0,X1] : join(X0,meet(complement(X0),complement(meet(X0,X1)))) = join(X0,meet(complement(meet(X0,X1)),one)),
inference(superposition,[],[f39033,f9]) ).
fof(f48747,plain,
! [X0,X1] : join(X0,meet(complement(X0),complement(meet(X0,X1)))) = join(X0,meet(one,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f48522,f44481]) ).
fof(f48839,plain,
! [X0,X1] : join(X0,complement(meet(X0,X1))) = join(X0,meet(complement(X0),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f48747,f171]) ).
fof(f48875,plain,
! [X0,X1] : one = join(X0,meet(complement(X0),complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f48839,f707]) ).
fof(f49081,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,meet(complement(X0),complement(meet(X0,X1))))
| complement(X0) = meet(complement(X0),complement(meet(X0,X1))) ),
inference(superposition,[],[f11,f48875]) ).
fof(f49171,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(X0),complement(meet(X0,X1))))
| complement(X0) = meet(complement(X0),complement(meet(X0,X1))) ),
inference(trivial_inequality_removal,[],[f49081]) ).
fof(f49248,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(forward_subsumption_resolution,[],[f49171,f238]) ).
fof(f49618,plain,
! [X0,X1] : meet(X0,complement(meet(complement(X0),X1))) = X0,
inference(superposition,[],[f49248,f6121]) ).
fof(f49749,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f49248,f19722]) ).
fof(f50046,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(complement(X0),X1)),X0),
inference(superposition,[],[f32,f49618]) ).
fof(f50165,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f50046,f6]) ).
fof(f50302,plain,
! [X0,X1] : complement(meet(X0,complement(X1))) = join(X1,complement(meet(X0,complement(X1)))),
inference(superposition,[],[f50165,f19722]) ).
fof(f50326,plain,
! [X2,X0,X1] : join(X2,X0) = meet(join(X2,X0),join(X2,complement(meet(complement(X0),X1)))),
inference(superposition,[],[f68,f50165]) ).
fof(f50519,plain,
! [X0,X1] : complement(meet(X1,X0)) = meet(complement(meet(X1,X0)),complement(meet(X0,X1))),
inference(superposition,[],[f49749,f465]) ).
fof(f50539,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f49749,f3]) ).
fof(f50653,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f32,f49749]) ).
fof(f50720,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f50653,f6]) ).
fof(f50757,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f50539,f5]) ).
fof(f50773,plain,
! [X2,X0,X1] : meet(complement(meet(X1,X0)),join(X2,complement(meet(X0,X1)))) = meet(complement(meet(X1,X0)),join(X2,complement(meet(X1,X0)))),
inference(backward_demodulation,[],[f25530,f50519]) ).
fof(f50872,plain,
! [X2,X0,X1] : complement(meet(X1,X0)) = meet(complement(meet(X1,X0)),join(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f50773,f34]) ).
fof(f50930,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f50720,f3]) ).
fof(f50931,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f50720,f34]) ).
fof(f51171,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f50931,f6]) ).
fof(f51172,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f50930,f6]) ).
fof(f51510,plain,
! [X2,X0,X1] : meet(complement(join(X1,X0)),X2) = meet(complement(join(X1,X0)),meet(complement(X0),X2)),
inference(superposition,[],[f95,f51171]) ).
fof(f51561,plain,
! [X2,X0,X1] : meet(complement(join(X1,X0)),X2) = meet(complement(X0),meet(X2,complement(join(X1,X0)))),
inference(forward_demodulation,[],[f51510,f110]) ).
fof(f51721,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f51172,f6121]) ).
fof(f52089,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f34,f51721]) ).
fof(f52222,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f52089,f5]) ).
fof(f53482,plain,
! [X0,X1] : join(complement(X1),X0) = meet(join(complement(X1),X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f50326,f50720]) ).
fof(f53754,plain,
! [X2,X0,X1] : complement(join(X0,meet(X1,X2))) = meet(complement(meet(X2,X1)),complement(join(X0,meet(X1,X2)))),
inference(superposition,[],[f50757,f43893]) ).
fof(f54021,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = meet(join(complement(X1),complement(X0)),complement(meet(X0,X1))),
inference(superposition,[],[f53482,f6121]) ).
fof(f54033,plain,
! [X0,X1] : join(complement(meet(X1,complement(X0))),X0) = meet(join(complement(meet(X1,complement(X0))),X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f53482,f465]) ).
fof(f54147,plain,
! [X0,X1] : complement(complement(meet(complement(X1),X0))) = meet(complement(complement(meet(complement(X1),X0))),complement(join(complement(X0),X1))),
inference(superposition,[],[f49749,f53482]) ).
fof(f54151,plain,
! [X0,X1] : complement(complement(meet(complement(X1),X0))) = meet(complement(join(complement(X0),X1)),complement(complement(meet(complement(X1),X0)))),
inference(forward_demodulation,[],[f54147,f5]) ).
fof(f54235,plain,
! [X0,X1] : join(complement(meet(X1,complement(X0))),X0) = meet(complement(meet(complement(X0),X1)),join(complement(meet(X1,complement(X0))),X0)),
inference(forward_demodulation,[],[f54033,f5]) ).
fof(f54245,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = meet(complement(meet(X0,X1)),join(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f54021,f5]) ).
fof(f54265,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(join(complement(X0),X1)),meet(complement(X1),X0)),
inference(forward_demodulation,[],[f54151,f6121]) ).
fof(f54336,plain,
! [X0,X1] : join(complement(meet(X1,complement(X0))),X0) = meet(complement(meet(complement(X0),X1)),join(X0,complement(meet(X1,complement(X0))))),
inference(forward_demodulation,[],[f54235,f4218]) ).
fof(f54360,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f54265,f5]) ).
fof(f54420,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(X1,complement(X0))),X0),
inference(forward_demodulation,[],[f54336,f50872]) ).
fof(f54439,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(X1),meet(X0,complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f54360,f7]) ).
fof(f54462,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f54420,f6]) ).
fof(f54479,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(complement(join(complement(X0),X1)),X0),
inference(forward_demodulation,[],[f54439,f51561]) ).
fof(f54504,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f54479,f5]) ).
fof(f54522,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(backward_demodulation,[],[f52222,f54504]) ).
fof(f54813,plain,
! [X2,X0,X1] : complement(join(meet(complement(X0),X1),X2)) = meet(complement(X2),join(complement(X1),X0)),
inference(superposition,[],[f54522,f54522]) ).
fof(f54814,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(superposition,[],[f54522,f6121]) ).
fof(f54823,plain,
! [X0,X1] : meet(complement(X0),X1) = complement(join(X0,complement(X1))),
inference(superposition,[],[f54522,f6]) ).
fof(f54863,plain,
! [X0,X1] : one = join(X0,join(complement(X1),meet(complement(X0),X1))),
inference(superposition,[],[f1109,f54522]) ).
fof(f54895,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f6121,f54522]) ).
fof(f54995,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(meet(X1,complement(X0)))),
inference(backward_demodulation,[],[f54462,f54895]) ).
fof(f55356,plain,
! [X2,X0,X1] : complement(join(X0,meet(X1,X2))) = complement(join(join(X0,meet(X1,X2)),meet(X2,X1))),
inference(backward_demodulation,[],[f53754,f54814]) ).
fof(f55445,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = complement(join(meet(complement(complement(X0)),X1),meet(X0,X1))),
inference(backward_demodulation,[],[f54245,f54813]) ).
fof(f55570,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(backward_demodulation,[],[f50302,f54995]) ).
fof(f55752,plain,
! [X2,X0,X1] : complement(join(X0,meet(X1,X2))) = complement(join(meet(X2,X1),join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f55356,f6]) ).
fof(f55793,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = complement(join(meet(X0,X1),meet(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f55445,f6]) ).
fof(f56002,plain,
! [X2,X0,X1] : complement(join(X0,meet(X1,X2))) = complement(join(X0,meet(X2,X1))),
inference(forward_demodulation,[],[f55752,f7544]) ).
fof(f56007,plain,
! [X0,X1] : join(complement(X1),complement(X0)) = complement(join(meet(X0,X1),meet(X0,X1))),
inference(forward_demodulation,[],[f55793,f6121]) ).
fof(f56075,plain,
! [X0,X1] : complement(meet(X0,X1)) = join(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f56007,f2]) ).
fof(f56762,plain,
! [X0,X1] : meet(X0,complement(X1)) = complement(join(X1,complement(X0))),
inference(superposition,[],[f54814,f6121]) ).
fof(f56832,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,meet(complement(X0),complement(X1))),
inference(superposition,[],[f5609,f54814]) ).
fof(f56855,plain,
! [X2,X0,X1] : meet(X2,complement(join(X0,X1))) = meet(X2,complement(join(X1,X0))),
inference(forward_demodulation,[],[f56832,f54814]) ).
fof(f57021,plain,
! [X2,X0,X1] : join(complement(X2),meet(complement(X1),X0)) = complement(meet(join(complement(X0),X1),X2)),
inference(superposition,[],[f54895,f54895]) ).
fof(f57124,plain,
! [X2,X0,X1] : meet(join(complement(X0),X1),complement(X2)) = complement(join(X2,meet(complement(X1),X0))),
inference(superposition,[],[f54814,f54895]) ).
fof(f57234,plain,
! [X0,X1] : one = join(X0,complement(meet(join(complement(X1),X0),X1))),
inference(backward_demodulation,[],[f54863,f57021]) ).
fof(f57391,plain,
! [X0,X1] : one = join(X0,complement(meet(X1,join(complement(X1),X0)))),
inference(forward_demodulation,[],[f57234,f19722]) ).
fof(f57483,plain,
! [X0,X1] : one = join(meet(X1,X0),complement(meet(X1,join(complement(X1),X0)))),
inference(backward_demodulation,[],[f37355,f57391]) ).
fof(f57681,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X1),complement(X0)),
inference(superposition,[],[f55570,f6121]) ).
fof(f57928,plain,
! [X2,X0,X1] : complement(join(X2,join(complement(X0),X1))) = meet(meet(X0,complement(X1)),complement(X2)),
inference(superposition,[],[f56762,f55570]) ).
fof(f58152,plain,
! [X2,X0,X1] : complement(join(X2,join(complement(X0),X1))) = meet(X0,meet(complement(X1),complement(X2))),
inference(forward_demodulation,[],[f57928,f7]) ).
fof(f58263,plain,
! [X2,X0,X1] : meet(X0,complement(join(X2,X1))) = complement(join(X2,join(complement(X0),X1))),
inference(forward_demodulation,[],[f58152,f54814]) ).
fof(f58345,plain,
! [X0,X1] : join(X0,complement(X1)) = complement(meet(complement(X0),X1)),
inference(superposition,[],[f57681,f6121]) ).
fof(f74709,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,join(complement(X0),X1))),join(meet(X0,X1),complement(one)))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(superposition,[],[f2238,f57483]) ).
fof(f74757,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,join(complement(X0),X1))),join(complement(one),meet(X0,X1)))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(forward_demodulation,[],[f74709,f4218]) ).
fof(f74989,plain,
! [X0,X1] :
( zero != meet(join(complement(one),meet(X1,X0)),complement(meet(X0,join(complement(X0),X1))))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(forward_demodulation,[],[f74757,f44522]) ).
fof(f75159,plain,
! [X0,X1] :
( zero != complement(join(meet(X0,join(complement(X0),X1)),meet(complement(meet(X1,X0)),one)))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(forward_demodulation,[],[f74989,f57124]) ).
fof(f75271,plain,
! [X0,X1] :
( zero != complement(join(meet(X0,join(complement(X0),X1)),meet(one,complement(meet(X1,X0)))))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(forward_demodulation,[],[f75159,f56002]) ).
fof(f75363,plain,
! [X0,X1] :
( zero != complement(join(meet(X0,join(complement(X0),X1)),complement(meet(X1,X0))))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(forward_demodulation,[],[f75271,f171]) ).
fof(f75432,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,join(complement(X0),X1))),meet(X1,X0))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(forward_demodulation,[],[f75363,f54823]) ).
fof(f75497,plain,
! [X0,X1] :
( zero != meet(meet(X1,X0),complement(meet(X0,join(complement(X0),X1))))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(forward_demodulation,[],[f75432,f5]) ).
fof(f75542,plain,
! [X0,X1] :
( zero != meet(X1,meet(X0,complement(meet(X0,join(complement(X0),X1)))))
| join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))) ),
inference(forward_demodulation,[],[f75497,f7]) ).
fof(f75569,plain,
! [X0,X1] : join(meet(X0,X1),complement(one)) = complement(complement(meet(X0,join(complement(X0),X1)))),
inference(forward_subsumption_resolution,[],[f75542,f1304]) ).
fof(f75587,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = join(meet(X0,X1),complement(one)),
inference(forward_demodulation,[],[f75569,f6121]) ).
fof(f75600,plain,
! [X0,X1] : meet(X0,join(complement(X0),X1)) = join(complement(one),meet(X0,X1)),
inference(forward_demodulation,[],[f75587,f6]) ).
fof(f75605,plain,
! [X0,X1] : join(zero,meet(X0,X1)) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f75600,f225]) ).
fof(f75606,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),X1)),
inference(forward_demodulation,[],[f75605,f232]) ).
fof(f76095,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(join(complement(complement(X0)),X1))),
inference(superposition,[],[f58345,f75606]) ).
fof(f76130,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f76095,f54522]) ).
fof(f76979,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = complement(meet(complement(X0),X1)),
inference(forward_demodulation,[],[f76130,f54814]) ).
fof(f77404,plain,
! [X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(X1),X0),
inference(forward_demodulation,[],[f76979,f54895]) ).
fof(f78922,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,X1))) = join(complement(join(meet(X2,X0),X1)),X0),
inference(superposition,[],[f77404,f56]) ).
fof(f78955,plain,
! [X0,X1] : join(complement(complement(X0)),complement(X1)) = join(complement(X1),complement(complement(meet(X0,X1)))),
inference(superposition,[],[f77404,f56075]) ).
fof(f78974,plain,
join(b,complement(join(b,sF3))) = join(complement(sF4),b),
inference(superposition,[],[f77404,f25995]) ).
fof(f79008,plain,
! [X2,X0,X1] : join(complement(join(complement(X0),X2)),X1) = join(X1,meet(X0,complement(join(X1,X2)))),
inference(superposition,[],[f77404,f58263]) ).
fof(f79079,plain,
! [X2,X0,X1] : join(X2,complement(join(meet(X1,X2),X0))) = join(X2,join(complement(X0),meet(X1,X2))),
inference(superposition,[],[f56,f77404]) ).
fof(f79138,plain,
! [X2,X0,X1] : join(X2,complement(X0)) = join(X2,complement(join(meet(X1,X2),X0))),
inference(forward_demodulation,[],[f79079,f2056]) ).
fof(f79248,plain,
! [X2,X0,X1] : join(meet(complement(X2),X0),X1) = join(X1,meet(X0,complement(join(X1,X2)))),
inference(forward_demodulation,[],[f79008,f54522]) ).
fof(f79273,plain,
join(b,complement(join(b,sF3))) = join(b,complement(sF4)),
inference(forward_demodulation,[],[f78974,f6]) ).
fof(f79290,plain,
! [X0,X1] : join(complement(complement(X0)),complement(X1)) = complement(meet(complement(meet(X0,X1)),X1)),
inference(forward_demodulation,[],[f78955,f56075]) ).
fof(f79317,plain,
! [X2,X0,X1] : join(X0,complement(join(X0,X1))) = join(X0,complement(join(meet(X2,X0),X1))),
inference(forward_demodulation,[],[f78922,f6]) ).
fof(f79590,plain,
join(b,complement(sF4)) = join(complement(sF3),b),
inference(forward_demodulation,[],[f79273,f77404]) ).
fof(f79607,plain,
! [X0,X1] : join(complement(complement(X0)),complement(X1)) = complement(meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f79290,f19722]) ).
fof(f79633,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f79317,f79138]) ).
fof(f79785,plain,
join(b,complement(sF4)) = join(b,complement(sF3)),
inference(forward_demodulation,[],[f79590,f6]) ).
fof(f79796,plain,
! [X0,X1] : join(complement(X1),meet(X0,X1)) = join(complement(complement(X0)),complement(X1)),
inference(forward_demodulation,[],[f79607,f55570]) ).
fof(f79915,plain,
! [X0,X1] : complement(meet(X1,complement(X0))) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f79796,f56075]) ).
fof(f79991,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),meet(X0,X1)),
inference(forward_demodulation,[],[f79915,f55570]) ).
fof(f80248,plain,
join(complement(sF1),sF2) = join(complement(sF1),b),
inference(superposition,[],[f79991,f16756]) ).
fof(f80250,plain,
join(complement(sF4),b) = join(complement(sF4),sF2),
inference(superposition,[],[f79991,f9468]) ).
fof(f80424,plain,
join(sF2,complement(sF4)) = join(complement(sF4),b),
inference(forward_demodulation,[],[f80250,f6]) ).
fof(f80426,plain,
join(complement(sF1),sF2) = join(b,complement(sF1)),
inference(forward_demodulation,[],[f80248,f6]) ).
fof(f80571,plain,
join(sF2,complement(sF4)) = join(b,complement(sF4)),
inference(forward_demodulation,[],[f80424,f6]) ).
fof(f80573,plain,
join(sF2,complement(sF1)) = join(b,complement(sF1)),
inference(forward_demodulation,[],[f80426,f6]) ).
fof(f80684,plain,
join(sF2,complement(sF4)) = join(b,complement(sF3)),
inference(forward_demodulation,[],[f80571,f79785]) ).
fof(f92030,plain,
join(complement(complement(sF1)),sF2) = join(sF2,complement(join(b,complement(sF1)))),
inference(superposition,[],[f77404,f80573]) ).
fof(f92041,plain,
join(complement(complement(sF1)),sF2) = join(sF2,meet(complement(b),sF1)),
inference(forward_demodulation,[],[f92030,f54823]) ).
fof(f92076,plain,
join(sF2,complement(complement(sF1))) = join(sF2,meet(complement(b),sF1)),
inference(forward_demodulation,[],[f92041,f6]) ).
fof(f92112,plain,
join(sF2,sF1) = join(sF2,meet(complement(b),sF1)),
inference(forward_demodulation,[],[f92076,f6121]) ).
fof(f92130,plain,
join(sF1,sF2) = join(sF2,meet(complement(b),sF1)),
inference(forward_demodulation,[],[f92112,f6]) ).
fof(f92148,plain,
sF1 = join(sF2,meet(complement(b),sF1)),
inference(forward_demodulation,[],[f92130,f16809]) ).
fof(f98614,plain,
! [X2,X0,X1] : join(X1,meet(X2,complement(join(complement(X0),X1)))) = join(meet(complement(complement(join(X1,X0))),X2),X1),
inference(superposition,[],[f79248,f77404]) ).
fof(f98700,plain,
! [X2,X0,X1] : join(meet(complement(X1),X0),X2) = join(X2,meet(X0,complement(join(X1,X2)))),
inference(superposition,[],[f79248,f56855]) ).
fof(f99015,plain,
! [X2,X0,X1] : join(X1,meet(X2,complement(join(complement(X0),X1)))) = join(X1,meet(complement(complement(join(X1,X0))),X2)),
inference(forward_demodulation,[],[f98614,f6]) ).
fof(f99183,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X0),X2)) = join(X1,meet(X2,complement(join(complement(X0),X1)))),
inference(forward_demodulation,[],[f99015,f6121]) ).
fof(f99291,plain,
! [X2,X0,X1] : join(X1,meet(join(X1,X0),X2)) = join(meet(complement(complement(X0)),X2),X1),
inference(forward_demodulation,[],[f99183,f98700]) ).
fof(f99360,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = join(X1,meet(join(X1,X0),X2)),
inference(forward_demodulation,[],[f99291,f6121]) ).
fof(f100408,plain,
! [X0] : join(b,meet(sF0,X0)) = join(meet(c,X0),b),
inference(superposition,[],[f99360,f15]) ).
fof(f100950,plain,
! [X0] : join(b,meet(sF0,X0)) = join(b,meet(c,X0)),
inference(forward_demodulation,[],[f100408,f6]) ).
fof(f105579,plain,
join(b,meet(c,sF1)) = join(b,sF1),
inference(superposition,[],[f100950,f520]) ).
fof(f105776,plain,
join(b,sF3) = join(b,sF1),
inference(forward_demodulation,[],[f105579,f12549]) ).
fof(f105944,plain,
join(b,complement(sF3)) = join(b,complement(join(b,sF1))),
inference(superposition,[],[f79633,f105776]) ).
fof(f105953,plain,
join(complement(sF1),b) = join(b,complement(sF3)),
inference(forward_demodulation,[],[f105944,f77404]) ).
fof(f105977,plain,
join(b,complement(sF1)) = join(b,complement(sF3)),
inference(forward_demodulation,[],[f105953,f6]) ).
fof(f105999,plain,
join(sF2,complement(sF4)) = join(b,complement(sF1)),
inference(backward_demodulation,[],[f80684,f105977]) ).
fof(f106263,plain,
join(sF2,complement(complement(sF4))) = join(sF2,complement(join(b,complement(sF1)))),
inference(superposition,[],[f79633,f105999]) ).
fof(f106274,plain,
join(sF2,complement(complement(sF4))) = join(sF2,meet(complement(b),sF1)),
inference(forward_demodulation,[],[f106263,f54823]) ).
fof(f106317,plain,
sF1 = join(sF2,complement(complement(sF4))),
inference(forward_demodulation,[],[f106274,f92148]) ).
fof(f106352,plain,
sF1 = join(sF2,sF4),
inference(forward_demodulation,[],[f106317,f6121]) ).
fof(f106379,plain,
sF1 = sF4,
inference(backward_demodulation,[],[f5062,f106352]) ).
fof(f106401,plain,
$false,
inference(forward_subsumption_resolution,[],[f106379,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT178-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/5.51 % Computer : n019.cluster.edu
% 0.25/5.51 % Model : x86_64 x86_64
% 0.25/5.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/5.51 % Memory : 8046.5625MB
% 0.25/5.51 % OS : Linux 6.8.0-71-generic
% 0.25/5.51 % CPULimit : 300
% 0.25/5.51 % WCLimit : 300
% 0.25/5.51 % DateTime : Sun Sep 27 14:04:25 UTC 2026
% 0.25/5.51 % CPUTime :
% 0.25/5.51 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/5.57 Running first-order theorem proving
% 0.25/5.57 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.92/9.24 % (3119128)Input is clausal, will run a generic CNF schedule.
% 20.92/9.24 % (3119133)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=2656036471:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 20.92/9.24 % (3119134)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2320010973:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 20.92/9.24 % (3119136)lrs+10_1_sil=8000:sp=occurrence:random_seed=1055121895:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 20.92/9.24 % (3119137)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=332495997:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 20.92/9.24 % (3119135)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1750768149:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 20.92/9.24 % (3119138)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=275014819:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 20.92/9.24 % (3119139)dis-21_1_sil=8000:lcm=predicate:random_seed=3316154283: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)
% 20.92/9.24 % (3119139)Refutation not found, incomplete strategy
% 20.92/9.24 % (3119139)------------------------------
% 20.92/9.24 % (3119139)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.92/9.24 % (3119139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.92/9.24 % (3119139)CaDiCaL version: 2.1.3
% 20.92/9.24 % (3119139)Termination reason: Refutation not found, incomplete strategy
% 20.92/9.24 % (3119139)Time elapsed: 0.003 s
% 20.92/9.24 % (3119139)Peak memory usage: 88 MB
% 20.92/9.24 % (3119139)Instructions burned: 1 (million)
% 20.92/9.24 % (3119136)Instruction limit reached!
% 20.92/9.24 % (3119136)------------------------------
% 20.92/9.24 % (3119136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.92/9.24 % (3119136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.92/9.24 % (3119136)CaDiCaL version: 2.1.3
% 20.92/9.24 % (3119136)Termination reason: Instruction limit
% 20.92/9.24 % (3119136)Termination phase: Saturation
% 20.92/9.24 % (3119136)Time elapsed: 0.105 s
% 20.92/9.24 % (3119136)Peak memory usage: 88 MB
% 20.92/9.24 % (3119136)Instructions burned: 107 (million)
% 20.92/9.24 % (3119137)Instruction limit reached!
% 20.92/9.24 % (3119137)------------------------------
% 20.92/9.24 % (3119137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.92/9.24 % (3119137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.92/9.24 % (3119137)CaDiCaL version: 2.1.3
% 20.92/9.24 % (3119137)Termination reason: Instruction limit
% 20.92/9.24 % (3119137)Termination phase: Saturation
% 20.92/9.24 % (3119137)Time elapsed: 0.112 s
% 20.92/9.24 % (3119137)Peak memory usage: 89 MB
% 20.92/9.24 % (3119137)Instructions burned: 115 (million)
% 20.92/9.24 % (3119138)Instruction limit reached!
% 20.92/9.24 % (3119138)------------------------------
% 20.92/9.24 % (3119138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.92/9.24 % (3119138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.92/9.24 % (3119138)CaDiCaL version: 2.1.3
% 20.92/9.24 % (3119138)Termination reason: Instruction limit
% 20.92/9.24 % (3119138)Termination phase: Saturation
% 20.92/9.24 % (3119138)Time elapsed: 0.167 s
% 20.92/9.24 % (3119138)Peak memory usage: 89 MB
% 20.92/9.24 % (3119138)Instructions burned: 181 (million)
% 20.92/9.24 % (3119147)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=2091338194:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 20.92/9.24 % (3119147)Refutation not found, incomplete strategy
% 20.92/9.24 % (3119147)------------------------------
% 20.92/9.24 % (3119147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.92/9.24 % (3119147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.92/9.24 % (3119147)CaDiCaL version: 2.1.3
% 20.92/9.24 % (3119147)Termination reason: Refutation not found, incomplete strategy
% 20.92/9.24 % (3119147)Time elapsed: 0.002 s
% 20.92/9.24 % (3119147)Peak memory usage: 88 MB
% 20.92/9.24 % (3119139)------------------------------
% 20.92/9.24 % (3119139)------------------------------
% 32.39/11.02 % (3119148)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=104124719: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)
% 32.39/11.02 % (3119148)Refutation not found, incomplete strategy
% 32.39/11.02 % (3119148)------------------------------
% 32.39/11.02 % (3119148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.39/11.02 % (3119148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.39/11.02 % (3119148)CaDiCaL version: 2.1.3
% 32.39/11.02 % (3119148)Termination reason: Refutation not found, incomplete strategy
% 32.39/11.02 % (3119148)Time elapsed: 0.003 s
% 32.39/11.02 % (3119148)Peak memory usage: 88 MB
% 32.39/11.02 % (3119148)Instructions burned: 1 (million)
% 32.39/11.02 % (3119149)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2918459354:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 32.39/11.02 % (3119149)Refutation not found, incomplete strategy
% 32.39/11.02 % (3119149)------------------------------
% 32.39/11.02 % (3119149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.39/11.02 % (3119149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.39/11.02 % (3119149)CaDiCaL version: 2.1.3
% 32.39/11.02 % (3119149)Termination reason: Refutation not found, incomplete strategy
% 32.39/11.02 % (3119149)Time elapsed: 0.019 s
% 32.39/11.02 % (3119149)Peak memory usage: 88 MB
% 32.39/11.02 % (3119152)lrs+10_64_to=lpo:sil=8000:random_seed=3536341626:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 32.39/11.02 % (3119147)------------------------------
% 32.39/11.02 % (3119147)------------------------------
% 32.39/11.02 % (3119148)------------------------------
% 32.39/11.02 % (3119148)------------------------------
% 32.39/11.02 % (3119152)Instruction limit reached!
% 32.39/11.02 % (3119152)------------------------------
% 32.39/11.02 % (3119152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.39/11.02 % (3119152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.39/11.02 % (3119152)CaDiCaL version: 2.1.3
% 32.39/11.02 % (3119152)Termination reason: Instruction limit
% 32.39/11.02 % (3119152)Termination phase: Saturation
% 32.39/11.02 % (3119152)Time elapsed: 0.123 s
% 32.39/11.02 % (3119152)Peak memory usage: 88 MB
% 32.39/11.02 % (3119152)Instructions burned: 126 (million)
% 32.39/11.02 % (3119149)------------------------------
% 32.39/11.02 % (3119149)------------------------------
% 32.39/11.02 % (3119155)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1026287285:avsq=on:i=194:fgj=on:bd=preordered_2989 on theBenchmark for (2989ds/194Mi)
% 32.39/11.02 % (3119156)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3528893683:i=157:gtg=all_2988 on theBenchmark for (2988ds/157Mi)
% 32.39/11.02 % (3119155)Instruction limit reached!
% 32.39/11.02 % (3119155)------------------------------
% 32.39/11.02 % (3119155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.39/11.02 % (3119155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.39/11.02 % (3119155)CaDiCaL version: 2.1.3
% 32.39/11.02 % (3119155)Termination reason: Instruction limit
% 32.39/11.02 % (3119155)Termination phase: Saturation
% 32.39/11.02 % (3119155)Time elapsed: 0.105 s
% 32.39/11.02 % (3119155)Peak memory usage: 90 MB
% 32.39/11.02 % (3119155)Instructions burned: 195 (million)
% 32.39/11.02 % (3119157)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3820984301:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 32.39/11.02 % (3119158)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=262848564:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 32.39/11.02 % (3119156)Instruction limit reached!
% 32.39/11.02 % (3119156)------------------------------
% 32.39/11.02 % (3119156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.39/11.02 % (3119156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.39/11.02 % (3119156)CaDiCaL version: 2.1.3
% 32.39/11.02 % (3119156)Termination reason: Instruction limit
% 32.39/11.02 % (3119156)Termination phase: Saturation
% 32.39/11.02 % (3119156)Time elapsed: 0.161 s
% 32.39/11.02 % (3119156)Peak memory usage: 90 MB
% 32.39/11.02 % (3119156)Instructions burned: 158 (million)
% 32.39/11.02 % (3119158)Instruction limit reached!
% 32.39/11.02 % (3119158)------------------------------
% 66.07/15.85 % (3119158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.07/15.85 % (3119158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.07/15.85 % (3119158)CaDiCaL version: 2.1.3
% 66.07/15.85 % (3119158)Termination reason: Instruction limit
% 66.07/15.85 % (3119158)Termination phase: Saturation
% 66.07/15.85 % (3119158)Time elapsed: 0.111 s
% 66.07/15.85 % (3119158)Peak memory usage: 89 MB
% 66.07/15.85 % (3119158)Instructions burned: 106 (million)
% 66.07/15.85 % (3119161)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1890218931:i=107_2985 on theBenchmark for (2985ds/107Mi)
% 66.07/15.85 % (3119161)Refutation not found, incomplete strategy
% 66.07/15.85 % (3119161)------------------------------
% 66.07/15.85 % (3119161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.07/15.85 % (3119161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.07/15.85 % (3119161)CaDiCaL version: 2.1.3
% 66.07/15.85 % (3119161)Termination reason: Refutation not found, incomplete strategy
% 66.07/15.85 % (3119161)Time elapsed: 0.001 s
% 66.07/15.85 % (3119161)Peak memory usage: 87 MB
% 66.07/15.85 % (3119164)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3523083681:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2984 on theBenchmark for (2984ds/242Mi)
% 66.07/15.85 % (3119161)------------------------------
% 66.07/15.85 % (3119161)------------------------------
% 66.07/15.85 % (3119165)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4163217229:cond=fast:i=5208:av=off_2983 on theBenchmark for (2983ds/5208Mi)
% 66.07/15.85 % (3119164)Instruction limit reached!
% 66.07/15.85 % (3119164)------------------------------
% 66.07/15.85 % (3119164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.07/15.85 % (3119164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.07/15.85 % (3119164)CaDiCaL version: 2.1.3
% 66.07/15.85 % (3119164)Termination reason: Instruction limit
% 66.07/15.85 % (3119164)Termination phase: Saturation
% 66.07/15.85 % (3119164)Time elapsed: 0.240 s
% 66.07/15.85 % (3119164)Peak memory usage: 90 MB
% 66.07/15.85 % (3119164)Instructions burned: 243 (million)
% 66.07/15.85 % (3119168)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1967393963:i=134:sd=2:doe=on:ss=axioms:sgt=14_2981 on theBenchmark for (2981ds/134Mi)
% 66.07/15.85 % (3119168)Instruction limit reached!
% 66.07/15.85 % (3119168)------------------------------
% 66.07/15.85 % (3119168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.07/15.85 % (3119168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.07/15.85 % (3119168)CaDiCaL version: 2.1.3
% 66.07/15.85 % (3119168)Termination reason: Instruction limit
% 66.07/15.85 % (3119168)Termination phase: Saturation
% 66.07/15.85 % (3119168)Time elapsed: 0.071 s
% 66.07/15.85 % (3119168)Peak memory usage: 89 MB
% 66.07/15.85 % (3119168)Instructions burned: 136 (million)
% 66.07/15.85 % (3119170)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1719090823:i=499:bd=all_2978 on theBenchmark for (2978ds/499Mi)
% 66.07/15.85 % (3119172)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1138875622:i=191:fgj=on:bd=all_2977 on theBenchmark for (2977ds/191Mi)
% 66.07/15.85 % (3119172)Instruction limit reached!
% 66.07/15.85 % (3119172)------------------------------
% 66.07/15.85 % (3119172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.07/15.85 % (3119172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.07/15.85 % (3119172)CaDiCaL version: 2.1.3
% 66.07/15.85 % (3119172)Termination reason: Instruction limit
% 66.07/15.85 % (3119172)Termination phase: Saturation
% 66.07/15.85 % (3119172)Time elapsed: 0.199 s
% 66.07/15.85 % (3119172)Peak memory usage: 90 MB
% 66.07/15.85 % (3119172)Instructions burned: 191 (million)
% 66.07/15.85 % (3119170)Instruction limit reached!
% 66.07/15.85 % (3119170)------------------------------
% 66.07/15.85 % (3119170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.07/15.85 % (3119170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.07/15.85 % (3119170)CaDiCaL version: 2.1.3
% 66.07/15.85 % (3119170)Termination reason: Instruction limit
% 66.07/15.85 % (3119170)Termination phase: Saturation
% 66.07/15.85 % (3119170)Time elapsed: 0.523 s
% 66.07/15.85 % (3119170)Peak memory usage: 94 MB
% 66.07/15.85 % (3119170)Instructions burned: 499 (million)
% 87.70/18.97 % (3119175)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1053266783:i=264:kws=precedence:fsr=off_2972 on theBenchmark for (2972ds/264Mi)
% 87.70/18.97 % (3119176)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4111043153:cond=on:i=156:bs=on:gtg=exists_all:er=known_2970 on theBenchmark for (2970ds/156Mi)
% 87.70/18.97 % (3119175)Instruction limit reached!
% 87.70/18.97 % (3119175)------------------------------
% 87.70/18.97 % (3119175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.70/18.97 % (3119175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/18.97 % (3119175)CaDiCaL version: 2.1.3
% 87.70/18.97 % (3119175)Termination reason: Instruction limit
% 87.70/18.97 % (3119175)Termination phase: Saturation
% 87.70/18.97 % (3119175)Time elapsed: 0.264 s
% 87.70/18.97 % (3119175)Peak memory usage: 92 MB
% 87.70/18.97 % (3119175)Instructions burned: 264 (million)
% 87.70/18.97 % (3119176)Instruction limit reached!
% 87.70/18.97 % (3119176)------------------------------
% 87.70/18.97 % (3119176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.70/18.97 % (3119176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/18.97 % (3119176)CaDiCaL version: 2.1.3
% 87.70/18.97 % (3119176)Termination reason: Instruction limit
% 87.70/18.97 % (3119176)Termination phase: Saturation
% 87.70/18.97 % (3119176)Time elapsed: 0.157 s
% 87.70/18.97 % (3119176)Peak memory usage: 89 MB
% 87.70/18.97 % (3119176)Instructions burned: 156 (million)
% 87.70/18.97 % (3119179)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=157263619:i=3256:kws=precedence:bd=preordered:av=off_2966 on theBenchmark for (2966ds/3256Mi)
% 87.70/18.97 % (3119180)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3059807830:i=537:av=off:ss=included_2966 on theBenchmark for (2966ds/537Mi)
% 87.70/18.97 % (3119157)Instruction limit reached!
% 87.70/18.97 % (3119157)------------------------------
% 87.70/18.97 % (3119157)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.70/18.97 % (3119157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/18.97 % (3119157)CaDiCaL version: 2.1.3
% 87.70/18.97 % (3119157)Termination reason: Instruction limit
% 87.70/18.97 % (3119157)Termination phase: Saturation
% 87.70/18.97 % (3119157)Time elapsed: 2.408 s
% 87.70/18.97 % (3119157)Peak memory usage: 149 MB
% 87.70/18.97 % (3119157)Instructions burned: 3396 (million)
% 87.70/18.97 % (3119183)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1345336233:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi)
% 87.70/18.97 % (3119180)Instruction limit reached!
% 87.70/18.97 % (3119180)------------------------------
% 87.70/18.97 % (3119180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.70/18.97 % (3119180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/18.97 % (3119180)CaDiCaL version: 2.1.3
% 87.70/18.97 % (3119180)Termination reason: Instruction limit
% 87.70/18.97 % (3119180)Termination phase: Saturation
% 87.70/18.97 % (3119180)Time elapsed: 0.500 s
% 87.70/18.97 % (3119180)Peak memory usage: 93 MB
% 87.70/18.97 % (3119180)Instructions burned: 537 (million)
% 87.70/18.97 % (3119183)Instruction limit reached!
% 87.70/18.97 % (3119183)------------------------------
% 87.70/18.97 % (3119183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.70/18.97 % (3119183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.70/18.97 % (3119183)CaDiCaL version: 2.1.3
% 87.70/18.97 % (3119183)Termination reason: Instruction limit
% 87.70/18.97 % (3119183)Termination phase: Saturation
% 87.70/18.97 % (3119183)Time elapsed: 0.091 s
% 87.70/18.97 % (3119183)Peak memory usage: 88 MB
% 87.70/18.97 % (3119183)Instructions burned: 180 (million)
% 87.70/18.97 % (3119186)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=3079948185:i=412:gtgl=4:gtg=exists_all_2957 on theBenchmark for (2957ds/412Mi)
% 87.70/18.97 % (3119185)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=2247318215:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi)
% 87.70/18.97 % (3119186)Instruction limit reached!
% 87.70/18.97 % (3119186)------------------------------
% 87.70/18.97 % (3119186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119186)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119186)Termination reason: Instruction limit
% 83.21/20.30 % (3119186)Termination phase: Saturation
% 83.21/20.30 % (3119186)Time elapsed: 0.219 s
% 83.21/20.30 % (3119186)Peak memory usage: 94 MB
% 83.21/20.30 % (3119186)Instructions burned: 414 (million)
% 83.21/20.30 % (3119189)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=3640055892:s2pl=no:i=8478:s2at=4:nm=6_2952 on theBenchmark for (2952ds/8478Mi)
% 83.21/20.30 % (3119179)Instruction limit reached!
% 83.21/20.30 % (3119179)------------------------------
% 83.21/20.30 % (3119179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119179)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119179)Termination reason: Instruction limit
% 83.21/20.30 % (3119179)Termination phase: Saturation
% 83.21/20.30 % (3119179)Time elapsed: 3.430 s
% 83.21/20.30 % (3119179)Peak memory usage: 149 MB
% 83.21/20.30 % (3119179)Instructions burned: 3256 (million)
% 83.21/20.30 % (3119165)Instruction limit reached!
% 83.21/20.30 % (3119165)------------------------------
% 83.21/20.30 % (3119165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119165)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119165)Termination reason: Instruction limit
% 83.21/20.30 % (3119165)Termination phase: Saturation
% 83.21/20.30 % (3119165)Time elapsed: 5.401 s
% 83.21/20.30 % (3119165)Peak memory usage: 169 MB
% 83.21/20.30 % (3119165)Instructions burned: 5208 (million)
% 83.21/20.30 % (3119191)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=4103102437:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2929 on theBenchmark for (2929ds/303Mi)
% 83.21/20.30 % (3119191)Refutation not found, incomplete strategy
% 83.21/20.30 % (3119191)------------------------------
% 83.21/20.30 % (3119191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119191)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119191)Termination reason: Refutation not found, incomplete strategy
% 83.21/20.30 % (3119191)Time elapsed: 0.003 s
% 83.21/20.30 % (3119191)Peak memory usage: 88 MB
% 83.21/20.30 % (3119191)Instructions burned: 1 (million)
% 83.21/20.30 % (3119193)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=805132802:st=4:i=720:sd=3:fsr=off:ss=axioms_2926 on theBenchmark for (2926ds/720Mi)
% 83.21/20.30 % (3119193)Refutation not found, incomplete strategy
% 83.21/20.30 % (3119193)------------------------------
% 83.21/20.30 % (3119193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119193)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119193)Termination reason: Refutation not found, incomplete strategy
% 83.21/20.30 % (3119193)Time elapsed: 0.002 s
% 83.21/20.30 % (3119193)Peak memory usage: 88 MB
% 83.21/20.30 % (3119191)------------------------------
% 83.21/20.30 % (3119191)------------------------------
% 83.21/20.30 % (3119195)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4039980320:i=598:bs=on:bd=preordered:av=off:ss=axioms_2922 on theBenchmark for (2922ds/598Mi)
% 83.21/20.30 % (3119193)------------------------------
% 83.21/20.30 % (3119193)------------------------------
% 83.21/20.30 % (3119195)Instruction limit reached!
% 83.21/20.30 % (3119195)------------------------------
% 83.21/20.30 % (3119195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119195)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119195)Termination reason: Instruction limit
% 83.21/20.30 % (3119195)Termination phase: Saturation
% 83.21/20.30 % (3119195)Time elapsed: 0.627 s
% 83.21/20.30 % (3119195)Peak memory usage: 94 MB
% 83.21/20.30 % (3119195)Instructions burned: 598 (million)
% 83.21/20.30 % (3119199)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=1890256570:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2913 on theBenchmark for (2913ds/1997Mi)
% 83.21/20.30 % (3119198)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=352933744:i=2989:sd=3:ss=axioms:sgt=60_2914 on theBenchmark for (2914ds/2989Mi)
% 83.21/20.30 % (3119189)Instruction limit reached!
% 83.21/20.30 % (3119189)------------------------------
% 83.21/20.30 % (3119189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119189)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119189)Termination reason: Instruction limit
% 83.21/20.30 % (3119189)Termination phase: Saturation
% 83.21/20.30 % (3119189)Time elapsed: 5.012 s
% 83.21/20.30 % (3119189)Peak memory usage: 192 MB
% 83.21/20.30 % (3119189)Instructions burned: 8480 (million)
% 83.21/20.30 % (3119202)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=840701834:i=2088:bd=preordered:av=off_2900 on theBenchmark for (2900ds/2088Mi)
% 83.21/20.30 % (3119202)Instruction limit reached!
% 83.21/20.30 % (3119202)------------------------------
% 83.21/20.30 % (3119202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119202)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119202)Termination reason: Instruction limit
% 83.21/20.30 % (3119202)Termination phase: Saturation
% 83.21/20.30 % (3119202)Time elapsed: 1.226 s
% 83.21/20.30 % (3119202)Peak memory usage: 139 MB
% 83.21/20.30 % (3119202)Instructions burned: 2089 (million)
% 83.21/20.30 % (3119199)Instruction limit reached!
% 83.21/20.30 % (3119199)------------------------------
% 83.21/20.30 % (3119199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119199)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119199)Termination reason: Instruction limit
% 83.21/20.30 % (3119199)Termination phase: Saturation
% 83.21/20.30 % (3119199)Time elapsed: 2.104 s
% 83.21/20.30 % (3119199)Peak memory usage: 138 MB
% 83.21/20.30 % (3119199)Instructions burned: 1997 (million)
% 83.21/20.30 % (3119204)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2917327955:i=1098:nicw=on_2884 on theBenchmark for (2884ds/1098Mi)
% 83.21/20.30 % (3119205)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=953648502:i=433:bd=preordered_2883 on theBenchmark for (2883ds/433Mi)
% 83.21/20.30 % (3119205)Refutation not found, incomplete strategy
% 83.21/20.30 % (3119205)------------------------------
% 83.21/20.30 % (3119205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119205)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119205)Termination reason: Refutation not found, incomplete strategy
% 83.21/20.30 % (3119205)Time elapsed: 0.003 s
% 83.21/20.30 % (3119205)Peak memory usage: 88 MB
% 83.21/20.30 % (3119205)Instructions burned: 1 (million)
% 83.21/20.30 % (3119205)------------------------------
% 83.21/20.30 % (3119205)------------------------------
% 83.21/20.30 % (3119204)Instruction limit reached!
% 83.21/20.30 % (3119204)------------------------------
% 83.21/20.30 % (3119204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119204)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119204)Termination reason: Instruction limit
% 83.21/20.30 % (3119204)Termination phase: Saturation
% 83.21/20.30 % (3119204)Time elapsed: 0.595 s
% 83.21/20.30 % (3119204)Peak memory usage: 102 MB
% 83.21/20.30 % (3119204)Instructions burned: 1098 (million)
% 83.21/20.30 % (3119198)Instruction limit reached!
% 83.21/20.30 % (3119198)------------------------------
% 83.21/20.30 % (3119198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119198)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119198)Termination reason: Instruction limit
% 83.21/20.30 % (3119198)Termination phase: Saturation
% 83.21/20.30 % (3119198)Time elapsed: 3.060 s
% 83.21/20.30 % (3119198)Peak memory usage: 147 MB
% 83.21/20.30 % (3119198)Instructions burned: 2989 (million)
% 83.21/20.30 % (3119208)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=692555567:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2876 on theBenchmark for (2876ds/2942Mi)
% 83.21/20.30 % (3119209)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3655213364:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2875 on theBenchmark for (2875ds/6922Mi)
% 83.21/20.30 % (3119210)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1723715966:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2873 on theBenchmark for (2873ds/596Mi)
% 83.21/20.30 % (3119210)Refutation not found, incomplete strategy
% 83.21/20.30 % (3119210)------------------------------
% 83.21/20.30 % (3119210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.21/20.30 % (3119210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.21/20.30 % (3119210)CaDiCaL version: 2.1.3
% 83.21/20.30 % (3119210)Termination reason: Refutation not found, incomplete strategy
% 83.21/20.30 % (3119210)Time elapsed: 0.003 s
% 83.21/20.30 % (3119210)Peak memory usage: 88 MB
% 83.21/20.30 % (3119210)Instructions burned: 1 (million)
% 83.21/20.30 % (3119210)------------------------------
% 83.21/20.30 % (3119210)------------------------------
% 83.21/20.30 % (3119135)First to succeed.
% 83.21/20.30 % (3119135)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3119128"
% 83.21/20.30 % (3119134)Also succeeded, but the first one will report.
% 83.21/20.30 % (3119214)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1544674762:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2866 on theBenchmark for (2866ds/4123Mi)
% 83.21/20.30 % (3119135)Refutation found. Thanks to Tanya!
% 83.21/20.30 % SZS status Unsatisfiable for theBenchmark
% 83.21/20.30 % SZS output start Proof for theBenchmark
% See solution above
% 97.95/20.69 % (3119135)------------------------------
% 97.95/20.69 % (3119135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 97.95/20.69 % (3119135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.95/20.69 % (3119135)CaDiCaL version: 2.1.3
% 97.95/20.69 % (3119135)Termination reason: Refutation
% 97.95/20.69 % (3119135)Time elapsed: 13.176 s
% 97.95/20.69 % (3119135)Peak memory usage: 211 MB
% 97.95/20.69 % (3119135)Instructions burned: 12288 (million)
% 97.95/20.69 % (3119135)------------------------------
% 97.95/20.69 % (3119135)------------------------------
% 97.95/20.69 % (3119128)Success in time 13.979 s
% 97.95/20.69 % Vampire exiting
%------------------------------------------------------------------------------