%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT186-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 : n009.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 33.97s 5.74s
% Output : Refutation 35.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 17
% Syntax : Number of formulae : 329 ( 320 unt; 5 def)
% Number of atoms : 342 ( 341 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 28 ( 15 ~; 13 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 10 ( 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 : 627 ( 627 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : meet(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_meet) ).
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(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X0,meet(X1,join(X2,meet(X0,X1))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equation_H11) ).
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,
sF1 = meet(sF0,a),
inference(forward_demodulation,[],[f17,f5]) ).
fof(f26,plain,
sF2 = meet(b,a),
inference(forward_demodulation,[],[f19,f5]) ).
fof(f27,plain,
sF3 = meet(c,a),
inference(forward_demodulation,[],[f21,f5]) ).
fof(f31,plain,
b = join(b,sF2),
inference(superposition,[],[f4,f26]) ).
fof(f32,plain,
c = join(c,sF3),
inference(superposition,[],[f4,f27]) ).
fof(f35,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f4,f5]) ).
fof(f37,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f3,f6]) ).
fof(f50,plain,
! [X2,X0,X1] : join(X0,join(meet(X0,X1),X2)) = join(X0,X2),
inference(superposition,[],[f8,f4]) ).
fof(f51,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f8,f35]) ).
fof(f53,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f8,f6]) ).
fof(f55,plain,
! [X0] : join(b,join(c,X0)) = join(sF0,X0),
inference(superposition,[],[f8,f15]) ).
fof(f64,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f6,f8]) ).
fof(f68,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f37,f4]) ).
fof(f69,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f37,f35]) ).
fof(f78,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f69,f5]) ).
fof(f79,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f68,f5]) ).
fof(f80,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f7,f3]) ).
fof(f81,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f7,f37]) ).
fof(f83,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f7,f5]) ).
fof(f85,plain,
! [X0] : meet(b,meet(a,X0)) = meet(sF2,X0),
inference(superposition,[],[f7,f26]) ).
fof(f86,plain,
! [X0] : meet(c,meet(a,X0)) = meet(sF3,X0),
inference(superposition,[],[f7,f27]) ).
fof(f94,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f95,plain,
! [X2,X0,X1] : meet(X0,X1) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f4,f7]) ).
fof(f103,plain,
! [X0] : meet(X0,one) = X0,
inference(superposition,[],[f3,f9]) ).
fof(f104,plain,
! [X0,X1] : one = join(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f8,f9]) ).
fof(f117,plain,
! [X0] : join(X0,zero) = X0,
inference(superposition,[],[f4,f10]) ).
fof(f118,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f7,f10]) ).
fof(f123,plain,
! [X2,X0,X1] : meet(X1,join(X0,meet(X1,X2))) = meet(X1,join(X0,meet(X2,join(X1,meet(X0,join(X2,meet(X0,X1))))))),
inference(superposition,[],[f12,f5]) ).
fof(f124,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),meet(X1,join(X0,meet(complement(X0),join(X1,zero)))))),
inference(superposition,[],[f12,f10]) ).
fof(f132,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X0,meet(X1,join(meet(X0,X1),X2)))))),
inference(superposition,[],[f12,f6]) ).
fof(f158,plain,
! [X0,X1] : meet(X0,join(complement(X0),meet(X0,X1))) = meet(X0,join(complement(X0),meet(X1,join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f124,f117]) ).
fof(f183,plain,
! [X0] : meet(one,X0) = X0,
inference(superposition,[],[f5,f103]) ).
fof(f201,plain,
! [X0] : one = join(X0,one),
inference(superposition,[],[f37,f183]) ).
fof(f267,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f6,f117]) ).
fof(f283,plain,
! [X0] : zero = meet(X0,zero),
inference(superposition,[],[f35,f267]) ).
fof(f287,plain,
one = complement(zero),
inference(superposition,[],[f9,f267]) ).
fof(f347,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f80,f5]) ).
fof(f350,plain,
! [X2,X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X2,join(X0,X1))),
inference(superposition,[],[f80,f37]) ).
fof(f352,plain,
! [X0,X1] : meet(X0,zero) = meet(X0,complement(join(X0,X1))),
inference(superposition,[],[f80,f10]) ).
fof(f370,plain,
! [X0,X1] : zero = meet(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f352,f283]) ).
fof(f372,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(X0,X1))) = X0,
inference(forward_demodulation,[],[f350,f3]) ).
fof(f420,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f50,f6]) ).
fof(f424,plain,
! [X0,X1] : join(X0,one) = join(X0,complement(meet(X0,X1))),
inference(superposition,[],[f50,f9]) ).
fof(f442,plain,
! [X0,X1] : one = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[],[f424,f201]) ).
fof(f452,plain,
! [X0,X1] : one = join(X1,complement(meet(X0,X1))),
inference(superposition,[],[f442,f5]) ).
fof(f488,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f51,f3]) ).
fof(f501,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f51,f6]) ).
fof(f540,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f488,f64]) ).
fof(f549,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f540,f8]) ).
fof(f552,plain,
! [X0,X1] : zero = meet(X1,complement(join(X0,X1))),
inference(superposition,[],[f370,f6]) ).
fof(f640,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(X0,a)),
inference(superposition,[],[f85,f5]) ).
fof(f677,plain,
! [X0] : meet(sF3,X0) = meet(c,meet(X0,a)),
inference(superposition,[],[f86,f5]) ).
fof(f750,plain,
! [X0,X1] : zero = meet(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f118,f5]) ).
fof(f962,plain,
! [X0,X1] : zero = meet(meet(X0,X1),complement(X0)),
inference(superposition,[],[f552,f4]) ).
fof(f1013,plain,
! [X0,X1] : zero = meet(complement(X0),meet(X0,X1)),
inference(forward_demodulation,[],[f962,f5]) ).
fof(f1023,plain,
! [X0,X1] : zero = meet(X0,meet(X1,complement(X0))),
inference(forward_demodulation,[],[f1013,f94]) ).
fof(f1053,plain,
! [X0] : meet(sF2,X0) = meet(sF2,meet(b,X0)),
inference(superposition,[],[f81,f31]) ).
fof(f1118,plain,
! [X0] : meet(sF2,X0) = meet(b,meet(X0,sF2)),
inference(forward_demodulation,[],[f1053,f94]) ).
fof(f1142,plain,
join(b,c) = join(sF0,sF3),
inference(superposition,[],[f55,f32]) ).
fof(f1154,plain,
sF0 = join(sF0,sF3),
inference(forward_demodulation,[],[f1142,f15]) ).
fof(f1249,plain,
! [X2,X3,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X0,join(X1,meet(X2,X3)))),
inference(superposition,[],[f50,f64]) ).
fof(f1401,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X0,meet(X1,X2))),
inference(superposition,[],[f35,f94]) ).
fof(f1572,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,f104]) ).
fof(f1586,plain,
! [X0,X1] :
( zero != meet(X0,join(X1,complement(join(X0,X1))))
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(trivial_inequality_removal,[],[f1572]) ).
fof(f2064,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(X0,meet(meet(X0,X1),join(X2,meet(X0,X1))))))),
inference(superposition,[],[f12,f79]) ).
fof(f2084,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(X0,meet(X0,X1))))),
inference(forward_demodulation,[],[f2064,f37]) ).
fof(f2097,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(forward_demodulation,[],[f2084,f4]) ).
fof(f2146,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,meet(complement(meet(X0,X1)),join(X0,meet(X1,one))))),
inference(superposition,[],[f132,f9]) ).
fof(f2226,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,meet(complement(meet(X0,X1)),join(X0,X1)))),
inference(forward_demodulation,[],[f2146,f103]) ).
fof(f2280,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(meet(X0,X1))))) = meet(X0,join(X1,meet(join(X0,X1),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f2226,f5]) ).
fof(f2341,plain,
! [X0,X1] : meet(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))) = meet(X0,join(complement(meet(X0,X1)),meet(one,complement(meet(X0,complement(meet(X0,X1))))))),
inference(superposition,[],[f2280,f442]) ).
fof(f2351,plain,
! [X0,X1] : meet(X1,join(X0,meet(X1,complement(meet(X0,X1))))) = meet(X1,join(X0,meet(join(X1,X0),complement(meet(X0,X1))))),
inference(superposition,[],[f2280,f5]) ).
fof(f2461,plain,
! [X0,X1] : meet(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))) = meet(X0,join(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f2341,f183]) ).
fof(f2500,plain,
! [X0,X1] : meet(X0,one) = meet(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f2461,f452]) ).
fof(f2530,plain,
! [X0,X1] : meet(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))) = X0,
inference(forward_demodulation,[],[f2500,f103]) ).
fof(f2757,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(X1,join(complement(X0),meet(X0,join(X1,zero)))))),
inference(superposition,[],[f123,f10]) ).
fof(f2886,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(X1,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f2757,f117]) ).
fof(f3017,plain,
! [X0,X1] : meet(X0,join(X1,meet(X0,complement(X0)))) = meet(X0,join(X1,meet(complement(X0),join(X0,meet(complement(X0),X1))))),
inference(superposition,[],[f12,f2886]) ).
fof(f3049,plain,
! [X0,X1] : meet(X0,join(X1,zero)) = meet(X0,join(X1,meet(complement(X0),join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f3017,f10]) ).
fof(f3089,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,meet(complement(X0),join(X0,meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f3049,f117]) ).
fof(f3504,plain,
meet(sF2,c) = meet(b,sF3),
inference(superposition,[],[f640,f27]) ).
fof(f3552,plain,
meet(c,sF2) = meet(b,sF3),
inference(forward_demodulation,[],[f3504,f5]) ).
fof(f3607,plain,
meet(sF3,sF0) = meet(c,sF1),
inference(superposition,[],[f677,f25]) ).
fof(f3653,plain,
meet(c,sF1) = meet(sF0,sF3),
inference(forward_demodulation,[],[f3607,f5]) ).
fof(f3905,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(X0,X2)),X3) = join(meet(X1,join(X0,X2)),join(meet(X0,X1),X3)),
inference(superposition,[],[f51,f347]) ).
fof(f3948,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(X0,X2)),X3) = join(meet(X0,X1),join(X3,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f3905,f64]) ).
fof(f4031,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),join(complement(meet(X0,complement(meet(X0,X1)))),X0)))),
inference(superposition,[],[f123,f2530]) ).
fof(f4035,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = join(join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),X0),
inference(superposition,[],[f35,f2530]) ).
fof(f4037,plain,
! [X2,X0,X1] : join(join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),X2) = join(join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),join(X0,X2)),
inference(superposition,[],[f51,f2530]) ).
fof(f4071,plain,
! [X2,X0,X1] : join(join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),X2) = join(X0,join(X2,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))))),
inference(forward_demodulation,[],[f4037,f64]) ).
fof(f4072,plain,
! [X0,X1] : join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f4035,f6]) ).
fof(f4074,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),join(X0,complement(meet(X0,complement(meet(X0,X1)))))))),
inference(forward_demodulation,[],[f4031,f6]) ).
fof(f4103,plain,
! [X2,X0,X1] : join(join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),X2) = join(X0,join(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f4071,f1249]) ).
fof(f4104,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,[],[f4072,f420]) ).
fof(f4106,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),one))),
inference(forward_demodulation,[],[f4074,f442]) ).
fof(f4131,plain,
! [X2,X0,X1] : join(X0,join(X2,complement(meet(X0,X1)))) = join(complement(meet(X0,X1)),join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),X2)),
inference(forward_demodulation,[],[f4103,f8]) ).
fof(f4132,plain,
! [X0,X1] : one = join(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f4104,f442]) ).
fof(f4133,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(one,complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4106,f5]) ).
fof(f4159,plain,
! [X0,X1] : meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f4133,f183]) ).
fof(f4168,plain,
! [X0,X1] : meet(join(X0,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),complement(meet(X0,X1))))),
inference(forward_demodulation,[],[f4159,f5]) ).
fof(f4174,plain,
! [X0,X1] : meet(join(X0,complement(meet(X0,X1))),complement(meet(X0,complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f4168,f5]) ).
fof(f4178,plain,
! [X0,X1] : meet(one,complement(meet(X0,complement(meet(X0,X1))))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f4174,f442]) ).
fof(f4182,plain,
! [X0,X1] : complement(meet(X0,complement(meet(X0,X1)))) = meet(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f4178,f183]) ).
fof(f4241,plain,
! [X0,X1] :
( one != one
| zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| meet(X0,complement(meet(X0,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))) ),
inference(superposition,[],[f11,f4132]) ).
fof(f4244,plain,
! [X2,X0,X1] : join(X2,one) = join(complement(meet(X0,X1)),join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),X2)),
inference(superposition,[],[f64,f4132]) ).
fof(f4257,plain,
! [X0,X1] :
( zero != meet(complement(meet(X0,X1)),meet(X0,complement(meet(X0,complement(meet(X0,X1))))))
| meet(X0,complement(meet(X0,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))) ),
inference(trivial_inequality_removal,[],[f4241]) ).
fof(f4270,plain,
! [X2,X0,X1] : one = join(complement(meet(X0,X1)),join(meet(X0,complement(meet(X0,complement(meet(X0,X1))))),X2)),
inference(forward_demodulation,[],[f4244,f201]) ).
fof(f4271,plain,
! [X0,X1] : meet(X0,complement(meet(X0,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))),
inference(forward_subsumption_resolution,[],[f4257,f750]) ).
fof(f4318,plain,
! [X2,X0,X1] : one = join(X0,join(X2,complement(meet(X0,X1)))),
inference(backward_demodulation,[],[f4131,f4270]) ).
fof(f4533,plain,
! [X0,X1] : meet(X1,complement(meet(X1,complement(meet(X0,X1))))) = complement(complement(meet(X0,X1))),
inference(superposition,[],[f4271,f5]) ).
fof(f4553,plain,
! [X0] : meet(X0,complement(meet(X0,complement(X0)))) = complement(complement(X0)),
inference(superposition,[],[f4271,f103]) ).
fof(f4584,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X0,complement(meet(X0,X1)))),meet(X0,X2))) = meet(X0,join(complement(meet(X0,complement(meet(X0,X1)))),meet(X2,join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,complement(complement(meet(X0,X1))))))))),
inference(superposition,[],[f12,f4271]) ).
fof(f4637,plain,
! [X0] : meet(X0,complement(zero)) = complement(complement(X0)),
inference(forward_demodulation,[],[f4553,f10]) ).
fof(f4664,plain,
! [X0] : meet(X0,one) = complement(complement(X0)),
inference(forward_demodulation,[],[f4637,f287]) ).
fof(f4681,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f4664,f103]) ).
fof(f4698,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,complement(meet(X0,complement(meet(X0,X1))))),
inference(backward_demodulation,[],[f4271,f4681]) ).
fof(f4699,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,complement(meet(X1,complement(meet(X0,X1))))),
inference(backward_demodulation,[],[f4533,f4681]) ).
fof(f4703,plain,
! [X2,X0,X1] : meet(X0,join(complement(meet(X0,complement(meet(X0,X1)))),meet(X0,X2))) = meet(X0,join(complement(meet(X0,complement(meet(X0,X1)))),meet(X2,join(X0,meet(complement(meet(X0,complement(meet(X0,X1)))),join(X2,meet(X0,X1))))))),
inference(backward_demodulation,[],[f4584,f4681]) ).
fof(f4909,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(join(X0,X1),complement(X0)))) = X0,
inference(superposition,[],[f4699,f3]) ).
fof(f5020,plain,
! [X0,X1] : meet(join(X0,X1),complement(meet(complement(X0),join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f4909,f5]) ).
fof(f5274,plain,
meet(b,sF3) = meet(sF2,meet(b,sF3)),
inference(superposition,[],[f78,f3552]) ).
fof(f5353,plain,
meet(b,sF3) = meet(b,meet(sF3,sF2)),
inference(forward_demodulation,[],[f5274,f94]) ).
fof(f5401,plain,
meet(sF2,sF3) = meet(b,sF3),
inference(forward_demodulation,[],[f5353,f1118]) ).
fof(f6239,plain,
! [X0,X1] : meet(complement(X0),join(X1,meet(complement(X0),X0))) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(superposition,[],[f12,f158]) ).
fof(f6297,plain,
! [X0,X1] : meet(complement(X0),join(X1,meet(X0,complement(X0)))) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f6239,f5]) ).
fof(f6342,plain,
! [X0,X1] : meet(complement(X0),join(X1,zero)) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f6297,f10]) ).
fof(f6362,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X1,meet(X0,join(complement(X0),meet(X0,X1))))),
inference(forward_demodulation,[],[f6342,f117]) ).
fof(f6459,plain,
! [X0,X1] : meet(X1,join(X0,meet(complement(X0),X1))) = meet(X1,join(X0,meet(X1,complement(X0)))),
inference(superposition,[],[f123,f6362]) ).
fof(f7382,plain,
meet(sF3,join(sF0,meet(sF3,complement(meet(c,sF1))))) = meet(sF3,join(sF0,meet(join(sF3,sF0),complement(meet(c,sF1))))),
inference(superposition,[],[f2351,f3653]) ).
fof(f7462,plain,
meet(sF3,join(sF0,meet(sF3,complement(meet(c,sF1))))) = meet(sF3,join(sF0,meet(join(sF0,sF3),complement(meet(c,sF1))))),
inference(forward_demodulation,[],[f7382,f6]) ).
fof(f7554,plain,
meet(sF3,join(sF0,meet(sF3,complement(meet(c,sF1))))) = meet(sF3,join(sF0,meet(sF0,complement(meet(c,sF1))))),
inference(forward_demodulation,[],[f7462,f1154]) ).
fof(f7625,plain,
meet(sF3,sF0) = meet(sF3,join(sF0,meet(sF3,complement(meet(c,sF1))))),
inference(forward_demodulation,[],[f7554,f4]) ).
fof(f7688,plain,
meet(sF0,sF3) = meet(sF3,join(sF0,meet(sF3,complement(meet(c,sF1))))),
inference(forward_demodulation,[],[f7625,f5]) ).
fof(f7727,plain,
meet(c,sF1) = meet(sF3,join(sF0,meet(sF3,complement(meet(c,sF1))))),
inference(forward_demodulation,[],[f7688,f3653]) ).
fof(f8272,plain,
! [X0,X1] : meet(X1,join(complement(X0),meet(X0,X1))) = meet(X1,join(complement(X0),meet(X1,X0))),
inference(superposition,[],[f123,f3089]) ).
fof(f8822,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),meet(X1,complement(X0))))) = meet(complement(X0),join(X0,meet(meet(X1,complement(X0)),join(complement(X0),zero)))),
inference(superposition,[],[f2886,f1023]) ).
fof(f8855,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),meet(X1,complement(X0))))) = meet(complement(X0),join(X0,meet(join(complement(X0),zero),meet(X1,complement(X0))))),
inference(forward_demodulation,[],[f8822,f5]) ).
fof(f8888,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),meet(X1,complement(X0))))) = meet(complement(X0),join(X0,meet(complement(X0),meet(join(complement(X0),zero),X1)))),
inference(forward_demodulation,[],[f8855,f94]) ).
fof(f8907,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(complement(X0),meet(X1,complement(X0))))),
inference(forward_demodulation,[],[f8888,f80]) ).
fof(f8917,plain,
! [X0,X1] : meet(complement(X0),join(X0,meet(complement(X0),X1))) = meet(complement(X0),join(X0,meet(X1,complement(X0)))),
inference(forward_demodulation,[],[f8907,f78]) ).
fof(f9708,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(join(X1,meet(complement(X0),join(X0,meet(complement(X0),X1)))),meet(X0,X2)),
inference(superposition,[],[f83,f3089]) ).
fof(f9979,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X2,join(X1,meet(complement(X0),join(X0,meet(complement(X0),X1)))))),
inference(forward_demodulation,[],[f9708,f94]) ).
fof(f10057,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,join(X1,meet(complement(X0),join(X0,meet(complement(X0),X1)))))),
inference(forward_demodulation,[],[f9979,f7]) ).
fof(f11187,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),complement(meet(X0,complement(meet(X0,X1))))),
inference(superposition,[],[f35,f4182]) ).
fof(f11232,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(complement(meet(X0,complement(meet(X0,X1)))),join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))),
inference(forward_demodulation,[],[f11187,f6]) ).
fof(f11280,plain,
! [X0,X1] : join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))) = join(X0,join(meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f11232,f64]) ).
fof(f11318,plain,
! [X0,X1] : one = join(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f11280,f4318]) ).
fof(f11501,plain,
! [X0,X1] :
( one != one
| zero != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(superposition,[],[f11,f11318]) ).
fof(f11538,plain,
! [X0,X1] :
( zero != meet(X0,meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))))
| complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))) ),
inference(trivial_inequality_removal,[],[f11501]) ).
fof(f11567,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(meet(X0,complement(meet(X0,X1))))),
inference(forward_subsumption_resolution,[],[f11538,f118]) ).
fof(f11852,plain,
! [X0,X1] : complement(X0) = meet(complement(meet(X0,X1)),complement(X0)),
inference(superposition,[],[f79,f11567]) ).
fof(f11896,plain,
! [X0,X1] : complement(X0) = meet(complement(X0),complement(meet(X0,X1))),
inference(forward_demodulation,[],[f11852,f5]) ).
fof(f12055,plain,
! [X0,X1] : meet(X0,complement(meet(complement(X0),X1))) = X0,
inference(superposition,[],[f11896,f4681]) ).
fof(f12092,plain,
! [X0,X1] : complement(X1) = meet(complement(X1),complement(meet(X0,X1))),
inference(superposition,[],[f11896,f4699]) ).
fof(f12139,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(meet(X0,X1)),meet(complement(X0),X2)),
inference(superposition,[],[f83,f11896]) ).
fof(f12176,plain,
! [X2,X0,X1] : meet(complement(X0),X2) = meet(complement(X0),meet(X2,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f12139,f94]) ).
fof(f12257,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f12092,f37]) ).
fof(f12317,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(meet(X1,X0)),complement(X0)),
inference(superposition,[],[f35,f12092]) ).
fof(f12319,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(meet(X1,X0)),join(complement(X0),X2)),
inference(superposition,[],[f51,f12092]) ).
fof(f12362,plain,
! [X2,X0,X1] : join(complement(meet(X1,X0)),X2) = join(complement(X0),join(X2,complement(meet(X1,X0)))),
inference(forward_demodulation,[],[f12319,f64]) ).
fof(f12363,plain,
! [X0,X1] : complement(meet(X1,X0)) = join(complement(X0),complement(meet(X1,X0))),
inference(forward_demodulation,[],[f12317,f6]) ).
fof(f12401,plain,
! [X0,X1] : complement(join(X1,X0)) = meet(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f12257,f5]) ).
fof(f12491,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(X0)),
inference(superposition,[],[f12363,f3]) ).
fof(f12492,plain,
! [X0,X1] : complement(X0) = join(complement(join(X1,X0)),complement(X0)),
inference(superposition,[],[f12363,f37]) ).
fof(f12622,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(forward_demodulation,[],[f12492,f6]) ).
fof(f12623,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(forward_demodulation,[],[f12491,f6]) ).
fof(f12677,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f12623,f4681]) ).
fof(f12803,plain,
! [X0,X1] : join(X0,complement(join(X1,complement(X0)))) = X0,
inference(superposition,[],[f12622,f4681]) ).
fof(f12997,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(complement(join(complement(X0),X1)),X0),
inference(superposition,[],[f37,f12677]) ).
fof(f13051,plain,
! [X0,X1] : complement(join(complement(X0),X1)) = meet(X0,complement(join(complement(X0),X1))),
inference(forward_demodulation,[],[f12997,f5]) ).
fof(f13148,plain,
! [X2,X0,X1] : meet(X2,X0) = join(meet(X2,X0),meet(X2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f95,f13051]) ).
fof(f13774,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(meet(complement(X0),X1)),X0),
inference(superposition,[],[f35,f12055]) ).
fof(f13845,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f13774,f6]) ).
fof(f14269,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = meet(complement(join(meet(X0,X2),X1)),complement(join(X0,X1))),
inference(superposition,[],[f12401,f50]) ).
fof(f14319,plain,
! [X0,X1] : meet(complement(X1),X0) = join(meet(complement(X1),X0),complement(join(complement(X0),X1))),
inference(superposition,[],[f13148,f12401]) ).
fof(f14402,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = meet(complement(join(X0,X1)),complement(join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f14269,f5]) ).
fof(f14649,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = join(meet(complement(X1),complement(X0)),complement(join(X0,X1))),
inference(superposition,[],[f14319,f4681]) ).
fof(f14685,plain,
! [X0,X1] : join(complement(X1),X0) = join(join(complement(X1),X0),complement(meet(complement(X0),X1))),
inference(superposition,[],[f12803,f14319]) ).
fof(f14731,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(X1),join(X0,complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f14685,f8]) ).
fof(f14763,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = join(complement(join(X0,X1)),meet(complement(X1),complement(X0))),
inference(forward_demodulation,[],[f14649,f6]) ).
fof(f14807,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(meet(complement(X0),X1)),X0),
inference(forward_demodulation,[],[f14731,f12362]) ).
fof(f14862,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(meet(complement(X0),X1))),
inference(forward_demodulation,[],[f14807,f6]) ).
fof(f14901,plain,
! [X0,X1] : join(complement(X1),X0) = complement(meet(complement(X0),X1)),
inference(backward_demodulation,[],[f13845,f14862]) ).
fof(f14984,plain,
! [X0,X1] : meet(join(X0,X1),join(complement(join(X0,X1)),X0)) = X0,
inference(backward_demodulation,[],[f5020,f14901]) ).
fof(f15031,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,complement(join(X0,X1)))) = X0,
inference(forward_demodulation,[],[f14984,f6]) ).
fof(f15156,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(X0,complement(join(X0,X1)))),
inference(superposition,[],[f81,f15031]) ).
fof(f15349,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(join(X0,X1)))),
inference(superposition,[],[f15156,f6]) ).
fof(f15375,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(join(X1,X0),complement(join(X0,join(X1,X2))))),
inference(superposition,[],[f15156,f53]) ).
fof(f15522,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X1,join(X0,complement(join(X0,join(X1,X2)))))),
inference(forward_demodulation,[],[f15375,f8]) ).
fof(f15550,plain,
! [X0,X1] :
( meet(X0,X1) != zero
| complement(X0) = join(X1,complement(join(X0,X1))) ),
inference(backward_demodulation,[],[f1586,f15349]) ).
fof(f15682,plain,
! [X2,X0,X1] : complement(meet(join(complement(X0),X1),X2)) = join(complement(X2),meet(complement(X1),X0)),
inference(superposition,[],[f14901,f14901]) ).
fof(f15690,plain,
! [X0,X1] : complement(complement(X0)) = join(complement(complement(meet(X0,complement(meet(X0,X1))))),meet(X0,X1)),
inference(superposition,[],[f14901,f11567]) ).
fof(f15697,plain,
! [X0,X1] : join(complement(X0),X1) = complement(meet(X0,complement(X1))),
inference(superposition,[],[f14901,f5]) ).
fof(f15745,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,join(complement(X0),X1)))),
inference(superposition,[],[f4699,f14901]) ).
fof(f15752,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(complement(complement(meet(complement(X0),X1))),X0)),
inference(superposition,[],[f4698,f14901]) ).
fof(f15753,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(complement(X1),join(complement(complement(meet(X0,complement(X1)))),X1)),
inference(superposition,[],[f4699,f14901]) ).
fof(f15765,plain,
! [X0,X1] : meet(complement(X1),X0) = complement(join(complement(X0),X1)),
inference(superposition,[],[f4681,f14901]) ).
fof(f15917,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(complement(X1),join(X1,complement(complement(meet(X0,complement(X1)))))),
inference(forward_demodulation,[],[f15753,f6]) ).
fof(f15918,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,complement(complement(meet(complement(X0),X1))))),
inference(forward_demodulation,[],[f15752,f6]) ).
fof(f15986,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(complement(X0),meet(X0,X1))),
inference(backward_demodulation,[],[f4698,f15697]) ).
fof(f15987,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),meet(X0,X1)),meet(X0,X2))) = meet(X0,join(join(complement(X0),meet(X0,X1)),meet(X2,join(X0,meet(join(complement(X0),meet(X0,X1)),join(X2,meet(X0,X1))))))),
inference(backward_demodulation,[],[f4703,f15697]) ).
fof(f16080,plain,
! [X0,X1] : complement(complement(X0)) = join(meet(X0,X1),complement(complement(meet(X0,complement(meet(X0,X1)))))),
inference(forward_demodulation,[],[f15690,f6]) ).
fof(f16175,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(complement(complement(X0)),X1),join(X0,X1))),
inference(backward_demodulation,[],[f14763,f15682]) ).
fof(f16262,plain,
! [X0,X1] : meet(X0,complement(X1)) = meet(complement(X1),join(X1,meet(X0,complement(X1)))),
inference(forward_demodulation,[],[f15917,f4681]) ).
fof(f16263,plain,
! [X0,X1] : meet(complement(X0),X1) = meet(complement(X0),join(X0,meet(complement(X0),X1))),
inference(forward_demodulation,[],[f15918,f4681]) ).
fof(f16369,plain,
! [X2,X0,X1] : meet(X0,join(join(complement(X0),meet(X0,X1)),meet(X0,X2))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(X0,meet(join(complement(X0),meet(X0,X1)),join(X2,meet(X0,X1)))))))),
inference(forward_demodulation,[],[f15987,f8]) ).
fof(f16440,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = complement(complement(X0)),
inference(forward_demodulation,[],[f16080,f4681]) ).
fof(f16510,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(X0,X1),join(complement(complement(X0)),X1))),
inference(forward_demodulation,[],[f16175,f5]) ).
fof(f16562,plain,
! [X0,X1] : meet(X1,complement(X0)) = meet(complement(X0),join(X0,meet(complement(X0),X1))),
inference(backward_demodulation,[],[f8917,f16262]) ).
fof(f16597,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,join(X1,meet(complement(X0),X1)))),
inference(backward_demodulation,[],[f10057,f16263]) ).
fof(f16692,plain,
! [X2,X0,X1] : meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(X0,meet(join(complement(X0),meet(X0,X1)),join(X2,meet(X0,X1)))))))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f16369,f8]) ).
fof(f16723,plain,
! [X0,X1] : join(meet(X0,X1),meet(X0,complement(meet(X0,X1)))) = X0,
inference(forward_demodulation,[],[f16440,f4681]) ).
fof(f16760,plain,
! [X0,X1] : meet(complement(X1),complement(X0)) = complement(meet(join(X0,X1),join(X0,X1))),
inference(forward_demodulation,[],[f16510,f4681]) ).
fof(f16801,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f16597,f35]) ).
fof(f16887,plain,
! [X0,X1] : complement(join(X0,X1)) = meet(complement(X1),complement(X0)),
inference(forward_demodulation,[],[f16760,f1]) ).
fof(f17005,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = complement(join(join(meet(X0,X2),X1),join(X0,X1))),
inference(backward_demodulation,[],[f14402,f16887]) ).
fof(f17074,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = complement(join(join(X0,X1),join(meet(X0,X2),X1))),
inference(forward_demodulation,[],[f17005,f6]) ).
fof(f17147,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = complement(join(X1,join(join(X0,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f17074,f64]) ).
fof(f17188,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = complement(join(X1,join(X0,join(X1,meet(X0,X2))))),
inference(forward_demodulation,[],[f17147,f8]) ).
fof(f17215,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = complement(join(X1,join(meet(X0,X2),X0))),
inference(forward_demodulation,[],[f17188,f549]) ).
fof(f17230,plain,
! [X2,X0,X1] : complement(join(X0,X1)) = complement(join(X1,join(X0,meet(X0,X2)))),
inference(forward_demodulation,[],[f17215,f6]) ).
fof(f17237,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f17230,f4]) ).
fof(f17363,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(complement(join(complement(complement(X0)),meet(complement(X0),X1))),X0),
inference(superposition,[],[f14901,f15986]) ).
fof(f17376,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(join(complement(complement(X0)),meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f17363,f6]) ).
fof(f17439,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(meet(complement(X0),X1)),complement(X0))),
inference(forward_demodulation,[],[f17376,f15765]) ).
fof(f17473,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,meet(complement(X0),complement(meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f17439,f5]) ).
fof(f17481,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(join(meet(complement(X0),X1),X0))),
inference(forward_demodulation,[],[f17473,f16887]) ).
fof(f17489,plain,
! [X0,X1] : complement(meet(complement(X0),X1)) = join(X0,complement(join(X0,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f17481,f17237]) ).
fof(f17495,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,meet(complement(X0),X1)))),
inference(forward_demodulation,[],[f17489,f14901]) ).
fof(f18126,plain,
! [X0,X1] :
( zero != zero
| complement(X0) = join(meet(X1,complement(meet(X0,X1))),complement(join(X0,meet(X1,complement(meet(X0,X1)))))) ),
inference(superposition,[],[f15550,f118]) ).
fof(f18187,plain,
! [X0,X1] : complement(X0) = join(meet(X1,complement(meet(X0,X1))),complement(join(X0,meet(X1,complement(meet(X0,X1)))))),
inference(trivial_inequality_removal,[],[f18126]) ).
fof(f18543,plain,
! [X0,X1] : join(X1,X0) = join(X1,meet(X0,complement(meet(X0,X1)))),
inference(superposition,[],[f51,f16723]) ).
fof(f18892,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,complement(meet(X0,X1)))),
inference(superposition,[],[f18543,f5]) ).
fof(f18916,plain,
! [X0,X1] : join(join(complement(X1),meet(X1,X0)),meet(X0,complement(meet(X0,join(complement(X1),meet(X0,X1)))))) = join(join(complement(X1),meet(X1,X0)),X0),
inference(superposition,[],[f18543,f8272]) ).
fof(f18948,plain,
join(sF3,sF2) = join(sF3,meet(sF2,complement(meet(b,sF3)))),
inference(superposition,[],[f18543,f5401]) ).
fof(f19049,plain,
join(sF2,sF3) = join(sF3,meet(sF2,complement(meet(b,sF3)))),
inference(forward_demodulation,[],[f18948,f6]) ).
fof(f19080,plain,
! [X0,X1] : join(X0,join(complement(X1),meet(X1,X0))) = join(join(complement(X1),meet(X1,X0)),meet(X0,complement(meet(X0,join(complement(X1),meet(X0,X1)))))),
inference(forward_demodulation,[],[f18916,f6]) ).
fof(f19123,plain,
! [X0,X1] : complement(X0) = join(meet(X1,complement(meet(X0,X1))),complement(join(X0,X1))),
inference(backward_demodulation,[],[f18187,f18892]) ).
fof(f19197,plain,
sF4 = join(sF3,meet(sF2,complement(meet(b,sF3)))),
inference(forward_demodulation,[],[f19049,f23]) ).
fof(f19224,plain,
! [X0,X1] : join(X0,join(complement(X1),meet(X1,X0))) = join(complement(X1),join(meet(X1,X0),meet(X0,complement(meet(X0,join(complement(X1),meet(X0,X1))))))),
inference(forward_demodulation,[],[f19080,f8]) ).
fof(f19266,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f19123,f6]) ).
fof(f19345,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),join(meet(X1,X0),meet(X0,complement(meet(X0,join(complement(X1),meet(X0,X1))))))),
inference(forward_demodulation,[],[f19224,f501]) ).
fof(f19574,plain,
! [X0,X1] : join(X1,complement(join(X0,X1))) = join(X1,complement(X0)),
inference(superposition,[],[f420,f19266]) ).
fof(f19580,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(meet(X1,complement(meet(X0,X1))),complement(X0)),
inference(superposition,[],[f37,f19266]) ).
fof(f19618,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),meet(X1,complement(meet(X0,X1)))),
inference(forward_demodulation,[],[f19580,f5]) ).
fof(f19628,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,join(X1,complement(X0))),
inference(backward_demodulation,[],[f15349,f19574]) ).
fof(f19769,plain,
! [X0,X1] : meet(X1,complement(meet(X0,X1))) = meet(complement(X0),X1),
inference(forward_demodulation,[],[f19618,f12176]) ).
fof(f19907,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(complement(X0),X1)),
inference(backward_demodulation,[],[f18892,f19769]) ).
fof(f20052,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = meet(X1,join(X0,meet(X1,complement(X0)))),
inference(backward_demodulation,[],[f6459,f19907]) ).
fof(f20072,plain,
! [X0,X1] : meet(complement(X0),join(X0,X1)) = meet(X1,complement(X0)),
inference(backward_demodulation,[],[f16562,f19907]) ).
fof(f20077,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(backward_demodulation,[],[f17495,f19907]) ).
fof(f20219,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,join(complement(X1),X0)),
inference(backward_demodulation,[],[f15156,f20077]) ).
fof(f20266,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X1,join(complement(join(X1,X2)),X0))),
inference(backward_demodulation,[],[f15522,f20077]) ).
fof(f20340,plain,
! [X0,X1] : meet(X1,join(X0,meet(X1,complement(X0)))) = X1,
inference(forward_demodulation,[],[f20052,f37]) ).
fof(f20518,plain,
! [X0,X1] : meet(complement(X1),X0) = meet(X0,complement(meet(X0,X1))),
inference(backward_demodulation,[],[f15745,f20219]) ).
fof(f20528,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(complement(X0),join(meet(X0,X1),meet(X2,join(X0,meet(join(complement(X0),meet(X0,X1)),join(X2,meet(X0,X1)))))))),
inference(backward_demodulation,[],[f16692,f20219]) ).
fof(f20698,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(X0,meet(join(complement(X0),meet(X0,X1)),join(X2,meet(X0,X1))))))),
inference(forward_demodulation,[],[f20528,f20219]) ).
fof(f20714,plain,
! [X0,X1] : join(meet(X0,X1),meet(complement(X1),X0)) = X0,
inference(backward_demodulation,[],[f16723,f20518]) ).
fof(f20749,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),join(meet(X1,X0),meet(complement(join(complement(X1),meet(X0,X1))),X0))),
inference(backward_demodulation,[],[f19345,f20518]) ).
fof(f20869,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),join(meet(X1,X0),meet(X0,complement(join(complement(X1),meet(X0,X1)))))),
inference(forward_demodulation,[],[f20749,f5]) ).
fof(f20976,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),join(meet(X1,X0),meet(X0,meet(complement(meet(X0,X1)),X1)))),
inference(forward_demodulation,[],[f20869,f15765]) ).
fof(f21035,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(X1),meet(X1,X0)),
inference(forward_demodulation,[],[f20976,f1401]) ).
fof(f21146,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(X0,meet(join(X1,complement(X0)),join(X2,meet(X0,X1))))))),
inference(backward_demodulation,[],[f20698,f21035]) ).
fof(f21777,plain,
meet(sF2,complement(meet(b,sF3))) = meet(complement(c),sF2),
inference(superposition,[],[f19769,f3552]) ).
fof(f21783,plain,
meet(sF3,complement(meet(c,sF1))) = meet(complement(sF0),sF3),
inference(superposition,[],[f19769,f3653]) ).
fof(f21854,plain,
meet(sF3,complement(meet(c,sF1))) = meet(sF3,complement(sF0)),
inference(forward_demodulation,[],[f21783,f5]) ).
fof(f21860,plain,
meet(sF2,complement(meet(b,sF3))) = meet(sF2,complement(c)),
inference(forward_demodulation,[],[f21777,f5]) ).
fof(f21921,plain,
meet(c,sF1) = meet(sF3,join(sF0,meet(sF3,complement(sF0)))),
inference(backward_demodulation,[],[f7727,f21854]) ).
fof(f21933,plain,
sF4 = join(sF3,meet(sF2,complement(c))),
inference(backward_demodulation,[],[f19197,f21860]) ).
fof(f21987,plain,
sF3 = meet(c,sF1),
inference(forward_demodulation,[],[f21921,f20340]) ).
fof(f22149,plain,
! [X2,X0,X1] : join(X1,join(complement(join(X1,X0)),X2)) = join(X2,join(complement(X0),X1)),
inference(superposition,[],[f64,f20077]) ).
fof(f22188,plain,
! [X2,X0,X1] : meet(X2,join(X1,X0)) = meet(X2,join(X0,join(complement(X2),X1))),
inference(backward_demodulation,[],[f20266,f22149]) ).
fof(f24793,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,complement(X0)),meet(X0,X2))) = meet(X0,join(join(X1,complement(X0)),meet(X2,join(X0,meet(join(X1,complement(X0)),join(X2,meet(X0,X1))))))),
inference(superposition,[],[f12,f19628]) ).
fof(f24858,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,complement(X0)),meet(X0,X2))) = meet(X0,join(X1,join(complement(X0),meet(X2,join(X0,meet(join(X1,complement(X0)),join(X2,meet(X0,X1)))))))),
inference(forward_demodulation,[],[f24793,f8]) ).
fof(f24906,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,complement(X0)),meet(X0,X2))) = meet(X0,join(meet(X2,join(X0,meet(join(X1,complement(X0)),join(X2,meet(X0,X1))))),X1)),
inference(forward_demodulation,[],[f24858,f22188]) ).
fof(f24940,plain,
! [X2,X0,X1] : meet(X0,join(join(X1,complement(X0)),meet(X0,X2))) = meet(X0,join(X1,meet(X2,join(X0,meet(join(X1,complement(X0)),join(X2,meet(X0,X1))))))),
inference(forward_demodulation,[],[f24906,f6]) ).
fof(f24979,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(X2,join(X0,meet(join(X1,complement(X0)),join(X2,meet(X0,X1))))))) = meet(X0,join(X1,join(complement(X0),meet(X0,X2)))),
inference(forward_demodulation,[],[f24940,f8]) ).
fof(f24985,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(X1,meet(X2,join(X0,meet(join(X1,complement(X0)),join(X2,meet(X0,X1))))))),
inference(forward_demodulation,[],[f24979,f22188]) ).
fof(f25977,plain,
! [X2,X0,X1] : join(X0,meet(X2,X1)) = join(X0,meet(complement(X0),meet(X1,X2))),
inference(superposition,[],[f19907,f16801]) ).
fof(f25986,plain,
! [X2,X0,X1] : join(X0,meet(complement(X0),X1)) = join(X0,meet(join(X2,complement(X0)),X1)),
inference(superposition,[],[f19907,f81]) ).
fof(f26125,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,meet(join(X2,complement(X0)),X1)),
inference(forward_demodulation,[],[f25986,f19907]) ).
fof(f26132,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X2,X1)),
inference(forward_demodulation,[],[f25977,f19907]) ).
fof(f26192,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = meet(X0,join(X1,meet(X2,join(X0,join(X2,meet(X0,X1)))))),
inference(backward_demodulation,[],[f24985,f26125]) ).
fof(f26193,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),meet(X0,X2))) = meet(X0,join(meet(X0,X1),meet(X2,join(X0,join(X2,meet(X0,X1)))))),
inference(backward_demodulation,[],[f21146,f26125]) ).
fof(f26228,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(forward_demodulation,[],[f26193,f372]) ).
fof(f26229,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f26192,f372]) ).
fof(f26252,plain,
! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(meet(X0,X1),meet(X2,X0))),
inference(backward_demodulation,[],[f2097,f26228]) ).
fof(f26483,plain,
! [X2,X0,X1] : meet(X0,join(meet(X2,X0),X1)) = meet(X0,join(meet(X0,X1),X2)),
inference(forward_demodulation,[],[f26252,f26229]) ).
fof(f26539,plain,
! [X2,X0,X1] : meet(X0,join(meet(X2,X0),X1)) = meet(X0,join(X2,X1)),
inference(forward_demodulation,[],[f26483,f26229]) ).
fof(f28625,plain,
! [X0,X1] : join(meet(X1,complement(X0)),meet(X0,X1)) = X1,
inference(superposition,[],[f20714,f4681]) ).
fof(f28747,plain,
! [X0,X1] : join(meet(X0,X1),meet(X1,complement(X0))) = X1,
inference(forward_demodulation,[],[f28625,f6]) ).
fof(f29050,plain,
sF1 = join(sF3,meet(sF1,complement(c))),
inference(superposition,[],[f28747,f21987]) ).
fof(f35239,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(join(meet(X1,X0),X2),meet(X0,join(X1,X2))),
inference(superposition,[],[f35,f26539]) ).
fof(f35330,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(X2,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f35239,f8]) ).
fof(f35457,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X0,join(X1,X2)),X2),
inference(forward_demodulation,[],[f35330,f3948]) ).
fof(f35535,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(X2,meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f35457,f6]) ).
fof(f36430,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(join(X0,X2),X1)),
inference(superposition,[],[f26132,f35535]) ).
fof(f54833,plain,
! [X0] : join(c,meet(sF0,X0)) = join(meet(b,X0),c),
inference(superposition,[],[f36430,f15]) ).
fof(f55140,plain,
! [X0] : join(c,meet(sF0,X0)) = join(c,meet(b,X0)),
inference(forward_demodulation,[],[f54833,f6]) ).
fof(f55386,plain,
join(c,meet(b,a)) = join(c,sF1),
inference(superposition,[],[f55140,f25]) ).
fof(f55569,plain,
join(c,sF2) = join(c,sF1),
inference(forward_demodulation,[],[f55386,f26]) ).
fof(f55666,plain,
meet(sF2,complement(c)) = meet(complement(c),join(c,sF1)),
inference(superposition,[],[f20072,f55569]) ).
fof(f55695,plain,
meet(sF2,complement(c)) = meet(sF1,complement(c)),
inference(forward_demodulation,[],[f55666,f20072]) ).
fof(f55711,plain,
sF4 = join(sF3,meet(sF1,complement(c))),
inference(backward_demodulation,[],[f21933,f55695]) ).
fof(f55747,plain,
sF1 = sF4,
inference(forward_demodulation,[],[f55711,f29050]) ).
fof(f55752,plain,
$false,
inference(forward_subsumption_resolution,[],[f55747,f24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT186-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n009.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 14:05:30 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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
% 9.45/2.14 % (2064075)Input is clausal, will run a generic CNF schedule.
% 9.45/2.14 % (2064084)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=172255192:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.45/2.14 % (2064086)dis-21_1_sil=8000:lcm=predicate:random_seed=2505590292: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)
% 9.45/2.14 % (2064086)Refutation not found, incomplete strategy
% 9.45/2.14 % (2064086)------------------------------
% 9.45/2.14 % (2064086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.45/2.14 % (2064086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.45/2.14 % (2064086)CaDiCaL version: 2.1.3
% 9.45/2.14 % (2064086)Termination reason: Refutation not found, incomplete strategy
% 9.45/2.14 % (2064086)Time elapsed: 0.002 s
% 9.45/2.14 % (2064086)Peak memory usage: 88 MB
% 9.45/2.14 % (2064086)Instructions burned: 1 (million)
% 9.45/2.14 % (2064080)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=2210208702:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.45/2.14 % (2064082)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=134488767:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.45/2.14 % (2064081)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3220283699:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.45/2.14 % (2064083)lrs+10_1_sil=8000:sp=occurrence:random_seed=4232989889:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.45/2.14 % (2064085)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2283625202:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.45/2.14 % (2064084)Instruction limit reached!
% 9.45/2.14 % (2064084)------------------------------
% 9.45/2.14 % (2064084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.45/2.14 % (2064084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.45/2.14 % (2064084)CaDiCaL version: 2.1.3
% 9.45/2.14 % (2064084)Termination reason: Instruction limit
% 9.45/2.14 % (2064084)Termination phase: Saturation
% 9.45/2.14 % (2064084)Time elapsed: 0.039 s
% 9.45/2.14 % (2064084)Peak memory usage: 89 MB
% 9.45/2.14 % (2064084)Instructions burned: 117 (million)
% 9.45/2.14 % (2064083)Instruction limit reached!
% 9.45/2.14 % (2064083)------------------------------
% 9.45/2.14 % (2064083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.45/2.14 % (2064083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.45/2.14 % (2064083)CaDiCaL version: 2.1.3
% 9.45/2.14 % (2064083)Termination reason: Instruction limit
% 9.45/2.14 % (2064083)Termination phase: Saturation
% 9.45/2.14 % (2064083)Time elapsed: 0.063 s
% 9.45/2.14 % (2064083)Peak memory usage: 88 MB
% 9.45/2.14 % (2064083)Instructions burned: 107 (million)
% 9.45/2.14 % (2064094)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=1605753220:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 9.45/2.14 % (2064085)Instruction limit reached!
% 9.45/2.14 % (2064085)------------------------------
% 9.45/2.14 % (2064085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.45/2.14 % (2064085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.45/2.14 % (2064085)CaDiCaL version: 2.1.3
% 9.45/2.14 % (2064085)Termination reason: Instruction limit
% 9.45/2.14 % (2064085)Termination phase: Saturation
% 9.45/2.14 % (2064085)Time elapsed: 0.101 s
% 9.45/2.14 % (2064085)Peak memory usage: 89 MB
% 9.45/2.14 % (2064085)Instructions burned: 181 (million)
% 9.45/2.14 % (2064094)Refutation not found, incomplete strategy
% 9.45/2.14 % (2064094)------------------------------
% 9.45/2.14 % (2064094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.45/2.14 % (2064094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.45/2.14 % (2064094)CaDiCaL version: 2.1.3
% 9.45/2.14 % (2064094)Termination reason: Refutation not found, incomplete strategy
% 9.45/2.14 % (2064094)Time elapsed: 0.001 s
% 9.45/2.14 % (2064094)Peak memory usage: 88 MB
% 9.45/2.14 % (2064095)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2138711167:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 18.10/3.41 % (2064095)Refutation not found, incomplete strategy
% 18.10/3.41 % (2064095)------------------------------
% 18.10/3.41 % (2064095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.10/3.41 % (2064095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.41 % (2064095)CaDiCaL version: 2.1.3
% 18.10/3.41 % (2064095)Termination reason: Refutation not found, incomplete strategy
% 18.10/3.41 % (2064095)Time elapsed: 0.001 s
% 18.10/3.41 % (2064095)Peak memory usage: 88 MB
% 18.10/3.41 % (2064095)Instructions burned: 1 (million)
% 18.10/3.41 % (2064086)------------------------------
% 18.10/3.41 % (2064086)------------------------------
% 18.10/3.41 % (2064097)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2478828125:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 18.10/3.41 % (2064097)Refutation not found, incomplete strategy
% 18.10/3.41 % (2064097)------------------------------
% 18.10/3.41 % (2064097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.10/3.41 % (2064097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.41 % (2064097)CaDiCaL version: 2.1.3
% 18.10/3.41 % (2064097)Termination reason: Refutation not found, incomplete strategy
% 18.10/3.41 % (2064097)Time elapsed: 0.001 s
% 18.10/3.41 % (2064097)Peak memory usage: 88 MB
% 18.10/3.41 % (2064094)------------------------------
% 18.10/3.41 % (2064094)------------------------------
% 18.10/3.41 % (2064101)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2419834296:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.10/3.41 % (2064099)lrs+10_64_to=lpo:sil=8000:random_seed=3893864676:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 18.10/3.41 % (2064101)Instruction limit reached!
% 18.10/3.41 % (2064101)------------------------------
% 18.10/3.41 % (2064101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.10/3.41 % (2064101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.41 % (2064101)CaDiCaL version: 2.1.3
% 18.10/3.41 % (2064101)Termination reason: Instruction limit
% 18.10/3.41 % (2064101)Termination phase: Saturation
% 18.10/3.41 % (2064101)Time elapsed: 0.061 s
% 18.10/3.41 % (2064101)Peak memory usage: 89 MB
% 18.10/3.41 % (2064101)Instructions burned: 194 (million)
% 18.10/3.41 % (2064095)------------------------------
% 18.10/3.41 % (2064095)------------------------------
% 18.10/3.41 % (2064099)Instruction limit reached!
% 18.10/3.41 % (2064099)------------------------------
% 18.10/3.41 % (2064099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.10/3.41 % (2064099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.41 % (2064099)CaDiCaL version: 2.1.3
% 18.10/3.41 % (2064099)Termination reason: Instruction limit
% 18.10/3.41 % (2064099)Termination phase: Saturation
% 18.10/3.41 % (2064099)Time elapsed: 0.073 s
% 18.10/3.41 % (2064099)Peak memory usage: 88 MB
% 18.10/3.41 % (2064099)Instructions burned: 126 (million)
% 18.10/3.41 % (2064097)------------------------------
% 18.10/3.41 % (2064097)------------------------------
% 18.10/3.41 % (2064104)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3837003737:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 18.10/3.41 % (2064104)Instruction limit reached!
% 18.10/3.41 % (2064104)------------------------------
% 18.10/3.41 % (2064104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.10/3.41 % (2064104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.41 % (2064104)CaDiCaL version: 2.1.3
% 18.10/3.41 % (2064104)Termination reason: Instruction limit
% 18.10/3.41 % (2064104)Termination phase: Saturation
% 18.10/3.41 % (2064104)Time elapsed: 0.051 s
% 18.10/3.41 % (2064104)Peak memory usage: 90 MB
% 18.10/3.41 % (2064104)Instructions burned: 158 (million)
% 18.10/3.41 % (2064105)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1557391602:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 18.10/3.41 % (2064106)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=2964281892:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 18.10/3.41 % (2064109)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1592419978:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 31.88/5.37 % (2064108)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=172453791:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 31.88/5.37 % (2064108)Refutation not found, incomplete strategy
% 31.88/5.37 % (2064108)------------------------------
% 31.88/5.37 % (2064108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.37 % (2064108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.37 % (2064108)CaDiCaL version: 2.1.3
% 31.88/5.37 % (2064108)Termination reason: Refutation not found, incomplete strategy
% 31.88/5.37 % (2064108)Time elapsed: 0.001 s
% 31.88/5.37 % (2064108)Peak memory usage: 87 MB
% 31.88/5.37 % (2064106)Instruction limit reached!
% 31.88/5.37 % (2064106)------------------------------
% 31.88/5.37 % (2064106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.37 % (2064106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.37 % (2064106)CaDiCaL version: 2.1.3
% 31.88/5.37 % (2064106)Termination reason: Instruction limit
% 31.88/5.37 % (2064106)Termination phase: Saturation
% 31.88/5.37 % (2064106)Time elapsed: 0.067 s
% 31.88/5.37 % (2064106)Peak memory usage: 89 MB
% 31.88/5.37 % (2064106)Instructions burned: 107 (million)
% 31.88/5.37 % (2064109)Instruction limit reached!
% 31.88/5.37 % (2064109)------------------------------
% 31.88/5.37 % (2064109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.37 % (2064109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.37 % (2064109)CaDiCaL version: 2.1.3
% 31.88/5.37 % (2064109)Termination reason: Instruction limit
% 31.88/5.37 % (2064109)Termination phase: Saturation
% 31.88/5.37 % (2064109)Time elapsed: 0.077 s
% 31.88/5.37 % (2064109)Peak memory usage: 90 MB
% 31.88/5.37 % (2064109)Instructions burned: 245 (million)
% 31.88/5.37 % (2064114)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3295062457:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 31.88/5.37 % (2064115)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3148524521:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 31.88/5.37 % (2064115)Instruction limit reached!
% 31.88/5.37 % (2064115)------------------------------
% 31.88/5.37 % (2064115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.37 % (2064115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.37 % (2064115)CaDiCaL version: 2.1.3
% 31.88/5.37 % (2064115)Termination reason: Instruction limit
% 31.88/5.37 % (2064115)Termination phase: Saturation
% 31.88/5.37 % (2064115)Time elapsed: 0.042 s
% 31.88/5.37 % (2064115)Peak memory usage: 89 MB
% 31.88/5.37 % (2064115)Instructions burned: 135 (million)
% 31.88/5.37 % (2064108)------------------------------
% 31.88/5.37 % (2064108)------------------------------
% 31.88/5.37 % (2064118)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1783763264:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 31.88/5.37 % (2064119)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=842768599:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 31.88/5.37 % (2064118)Instruction limit reached!
% 31.88/5.37 % (2064118)------------------------------
% 31.88/5.37 % (2064118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.37 % (2064118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.37 % (2064118)CaDiCaL version: 2.1.3
% 31.88/5.37 % (2064118)Termination reason: Instruction limit
% 31.88/5.37 % (2064118)Termination phase: Saturation
% 31.88/5.37 % (2064118)Time elapsed: 0.163 s
% 31.88/5.37 % (2064118)Peak memory usage: 95 MB
% 31.88/5.37 % (2064118)Instructions burned: 501 (million)
% 31.88/5.37 % (2064119)Instruction limit reached!
% 31.88/5.37 % (2064119)------------------------------
% 31.88/5.37 % (2064119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.88/5.37 % (2064119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.88/5.37 % (2064119)CaDiCaL version: 2.1.3
% 31.88/5.37 % (2064119)Termination reason: Instruction limit
% 31.88/5.37 % (2064119)Termination phase: Saturation
% 31.88/5.37 % (2064119)Time elapsed: 0.120 s
% 31.88/5.37 % (2064119)Peak memory usage: 91 MB
% 31.88/5.37 % (2064119)Instructions burned: 192 (million)
% 33.97/5.74 % (2064122)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1494142933:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 33.97/5.74 % (2064123)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=97181374:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 33.97/5.74 % (2064123)Instruction limit reached!
% 33.97/5.74 % (2064123)------------------------------
% 33.97/5.74 % (2064123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064123)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064123)Termination reason: Instruction limit
% 33.97/5.74 % (2064123)Termination phase: Saturation
% 33.97/5.74 % (2064123)Time elapsed: 0.092 s
% 33.97/5.74 % (2064123)Peak memory usage: 89 MB
% 33.97/5.74 % (2064123)Instructions burned: 157 (million)
% 33.97/5.74 % (2064122)Instruction limit reached!
% 33.97/5.74 % (2064122)------------------------------
% 33.97/5.74 % (2064122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064122)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064122)Termination reason: Instruction limit
% 33.97/5.74 % (2064122)Termination phase: Saturation
% 33.97/5.74 % (2064122)Time elapsed: 0.155 s
% 33.97/5.74 % (2064122)Peak memory usage: 92 MB
% 33.97/5.74 % (2064122)Instructions burned: 264 (million)
% 33.97/5.74 % (2064126)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=3404975029:i=3256:kws=precedence:bd=preordered:av=off_2984 on theBenchmark for (2984ds/3256Mi)
% 33.97/5.74 % (2064127)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=715229928:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi)
% 33.97/5.74 % (2064127)Instruction limit reached!
% 33.97/5.74 % (2064127)------------------------------
% 33.97/5.74 % (2064127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064127)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064127)Termination reason: Instruction limit
% 33.97/5.74 % (2064127)Termination phase: Saturation
% 33.97/5.74 % (2064127)Time elapsed: 0.285 s
% 33.97/5.74 % (2064127)Peak memory usage: 93 MB
% 33.97/5.74 % (2064127)Instructions burned: 538 (million)
% 33.97/5.74 % (2064130)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3347813741:i=180:bd=preordered:av=off_2980 on theBenchmark for (2980ds/180Mi)
% 33.97/5.74 % (2064105)Instruction limit reached!
% 33.97/5.74 % (2064105)------------------------------
% 33.97/5.74 % (2064105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064105)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064105)Termination reason: Instruction limit
% 33.97/5.74 % (2064105)Termination phase: Saturation
% 33.97/5.74 % (2064105)Time elapsed: 1.357 s
% 33.97/5.74 % (2064105)Peak memory usage: 150 MB
% 33.97/5.74 % (2064105)Instructions burned: 3395 (million)
% 33.97/5.74 % (2064132)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=426779911:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2978 on theBenchmark for (2978ds/10307Mi)
% 33.97/5.74 % (2064130)Instruction limit reached!
% 33.97/5.74 % (2064130)------------------------------
% 33.97/5.74 % (2064130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064130)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064130)Termination reason: Instruction limit
% 33.97/5.74 % (2064130)Termination phase: Saturation
% 33.97/5.74 % (2064130)Time elapsed: 0.103 s
% 33.97/5.74 % (2064130)Peak memory usage: 88 MB
% 33.97/5.74 % (2064130)Instructions burned: 181 (million)
% 33.97/5.74 % (2064134)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=2053566447:i=412:gtgl=4:gtg=exists_all_2978 on theBenchmark for (2978ds/412Mi)
% 33.97/5.74 % (2064134)Instruction limit reached!
% 33.97/5.74 % (2064134)------------------------------
% 33.97/5.74 % (2064134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064134)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064134)Termination reason: Instruction limit
% 33.97/5.74 % (2064134)Termination phase: Saturation
% 33.97/5.74 % (2064134)Time elapsed: 0.236 s
% 33.97/5.74 % (2064134)Peak memory usage: 94 MB
% 33.97/5.74 % (2064134)Instructions burned: 412 (million)
% 33.97/5.74 % (2064136)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=3610677810:s2pl=no:i=8478:s2at=4:nm=6_2974 on theBenchmark for (2974ds/8478Mi)
% 33.97/5.74 % (2064126)Instruction limit reached!
% 33.97/5.74 % (2064126)------------------------------
% 33.97/5.74 % (2064126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064126)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064126)Termination reason: Instruction limit
% 33.97/5.74 % (2064126)Termination phase: Saturation
% 33.97/5.74 % (2064126)Time elapsed: 1.985 s
% 33.97/5.74 % (2064126)Peak memory usage: 151 MB
% 33.97/5.74 % (2064126)Instructions burned: 3257 (million)
% 33.97/5.74 % (2064138)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=3418712496:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2963 on theBenchmark for (2963ds/303Mi)
% 33.97/5.74 % (2064138)Refutation not found, incomplete strategy
% 33.97/5.74 % (2064138)------------------------------
% 33.97/5.74 % (2064138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064138)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064138)Termination reason: Refutation not found, incomplete strategy
% 33.97/5.74 % (2064138)Time elapsed: 0.001 s
% 33.97/5.74 % (2064138)Peak memory usage: 88 MB
% 33.97/5.74 % (2064138)Instructions burned: 1 (million)
% 33.97/5.74 % (2064114)Instruction limit reached!
% 33.97/5.74 % (2064114)------------------------------
% 33.97/5.74 % (2064114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064114)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064114)Termination reason: Instruction limit
% 33.97/5.74 % (2064114)Termination phase: Saturation
% 33.97/5.74 % (2064114)Time elapsed: 3.059 s
% 33.97/5.74 % (2064114)Peak memory usage: 168 MB
% 33.97/5.74 % (2064114)Instructions burned: 5209 (million)
% 33.97/5.74 % (2064138)------------------------------
% 33.97/5.74 % (2064138)------------------------------
% 33.97/5.74 % (2064141)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2722845338:i=598:bs=on:bd=preordered:av=off:ss=axioms_2959 on theBenchmark for (2959ds/598Mi)
% 33.97/5.74 % (2064140)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2645721229:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi)
% 33.97/5.74 % (2064140)Refutation not found, incomplete strategy
% 33.97/5.74 % (2064140)------------------------------
% 33.97/5.74 % (2064140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064140)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064140)Termination reason: Refutation not found, incomplete strategy
% 33.97/5.74 % (2064140)Time elapsed: 0.001 s
% 33.97/5.74 % (2064140)Peak memory usage: 88 MB
% 33.97/5.74 % (2064140)------------------------------
% 33.97/5.74 % (2064140)------------------------------
% 33.97/5.74 % (2064141)Instruction limit reached!
% 33.97/5.74 % (2064141)------------------------------
% 33.97/5.74 % (2064141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.97/5.74 % (2064141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.97/5.74 % (2064141)CaDiCaL version: 2.1.3
% 33.97/5.74 % (2064141)Termination reason: Instruction limit
% 33.97/5.74 % (2064141)Termination phase: Saturation
% 33.97/5.74 % (2064141)Time elapsed: 0.373 s
% 33.97/5.74 % (2064141)Peak memory usage: 95 MB
% 33.97/5.74 % (2064141)Instructions burned: 599 (million)
% 33.97/5.74 % (2064144)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=959016017:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi)
% 33.97/5.74 % (2064146)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=822323892:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2954 on theBenchmark for (2954ds/1997Mi)
% 33.97/5.74 % (2064132)First to succeed.
% 33.97/5.74 % (2064132)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2064075"
% 33.97/5.74 % (2064082)Also succeeded, but the first one will report.
% 33.97/5.74 % (2064132)Refutation found. Thanks to Tanya!
% 33.97/5.74 % SZS status Unsatisfiable for theBenchmark
% 33.97/5.74 % SZS output start Proof for theBenchmark
% See solution above
% 35.20/5.93 % (2064132)------------------------------
% 35.20/5.93 % (2064132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.20/5.93 % (2064132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.20/5.93 % (2064132)CaDiCaL version: 2.1.3
% 35.20/5.93 % (2064132)Termination reason: Refutation
% 35.20/5.93 % (2064132)Time elapsed: 2.522 s
% 35.20/5.93 % (2064132)Peak memory usage: 175 MB
% 35.20/5.93 % (2064132)Instructions burned: 7156 (million)
% 35.20/5.93 % (2064132)------------------------------
% 35.20/5.93 % (2064132)------------------------------
% 35.20/5.93 % (2064075)Success in time 4.888 s
% 35.20/5.93 % Vampire exiting
%------------------------------------------------------------------------------